closure x is a characteristic function ----> UNIT CONFLICT at 114.06 sec ----> 3075 [binary,3074.1,8.1] $F. Length of proof is 5. Level of proof is 3.
1 [reference] k(x) y=x. 4 [reference] pair(x,y) z=pair(x z,y z). 5 [reference] pair(p1 x,p2 x)=x. 6 [reference] abst x y z=x k(z) (y z). 8 [reference] x=x. 51 [reference] abst k(x) k(y)=k(x y). 54 [reference] kintersection xf y x=p2|xf z !=p1|z x =p1. 56 [reference] kintersection xf y x=p1|xf notinint(xf,x) =p1. 57 [reference] kintersection xf y x=p1|notinint(xf,x) x !=p1. 72 [reference] closure=abst (abst k(kintersection) (abst k(abst k(eq)) pair(k(k(pair(p1,p1))),pair(abst k(abst k(subset)) pair(abst k(p1),k(pair(p1,p2))),abst k(abst k(closedunder)) pair(k(pair(p1,p2)),abst k(p2)))))) pair(p1,p2). 76 [assumption to refute] p. 77 [assumption to refute] -p|closure bad1 bad2 !=p1. 78 [assumption to refute] -p|closure bad1 bad2 !=p2. 79 [ur,77,76,demod,72,6,6,1,6,1,4,1,4,6,1,4,51,1,6,1,4,1,51,4,5] kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset ) pair(k(p1 bad1),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(p2 bad1))))) bad1 bad2!=p1. 92 [ur,78,76,demod,72,6,6,1,6,1,4,1,4,6,1,4,51,1,6,1,4,1,51,4,5] kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset ) pair(k(p1 bad1),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(p2 bad1))))) bad1 bad2!=p2. 103 [ur,79,57] notinint(abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(p1 bad1),pair(p1,p2)),abst k(closedunder) pair( pair(p1,p2),k(p2 bad1)))),bad2) bad2!=p1. 105,104 [ur,79,56,demod,6,1,4,1,4,6,1,4,1,4,5,6,1,4,4,5,1] eq pair(pair(p1,p1),pair(subset pair(p1 bad1,notinint(abst k(eq) pair( k(pair(p1,p1)),pair(abst k(subset) pair(k(p1 bad1),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(p2 bad1)))),bad2)),closedu nder pair(notinint(abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(p1 bad1),pair(p1,p2)),abst k(closedunder) pair(pair( p1,p2),k(p2 bad1)))),bad2),p2 bad1)))=p1. 3074 [ur,103,54,92,demod,6,1,4,1,4,6,1,4,1,4,5,6,1,4,4,5,1,105] p1!=p1. 3075 [binary,3074.1,8.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file