----> UNIT CONFLICT at 1.18 sec ----> 650 [binary,649.1,8.1] $F. Length of proof is 2. Level of proof is 2.
8 [reference] x=x. 13 [reference] pair(p1 x,p2 x)=x. 72 [reference] subset pair(xs,closure pair(xs,xf))=p1. 76 [assumption to refute] subset pair(p1 bad,closure bad)!=p1. 104 [para_into,76.1.2,72.1.2] subset pair(p1 bad,closure bad)!=subset pair(x,closure pair(x,y)). 649 [para_into,104.1.2.2.2.2,13.1.1] subset pair(p1 bad,closure bad)!=subset pair(p1 x,closure x). 650 [binary,649.1,8.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file