kintersecton -----> EMPTY CLAUSE at 77.87 sec ----> 5815 [para_into,5716.1.1,22.2.1,unit_del,19,5750] $ans(noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))). Length of proof is 8. Level of proof is 6.
1 [reference] k(x) y=x. 2 [reference] p1 pair(x,y)=x. 3 [reference] p2 pair(x,y)=y. 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. 9 [reference] k(x) y=x. 17 [reference] x=y|x noteq(x,y) !=y noteq(x,y). 19 [reference] p2!=p1. 20 [reference] p1 x!=p2 x |eq x =p1. 21 [reference] p1 x=p2 x |eq x =p2. 22 [reference] x y!=p1|isp1 x y =p1. 51 [reference] abst k(x) k(y)=k(x y). 52 [reference] pair(x1,y1)!=pair(x2,y2)|x1=x2. 53 [reference] pair(x1,y1)!=pair(x2,y2)|y1=y2. 54 [reference] kintersection=abst (abst k(abst) (abst k(abst k(abst)) (abst (abst k(abst) (abst k(abst k(abst)) (abst k(abst k(abst k(eq))) pair(k(k(k(k(p2)))),abst k(abst k(abst k(abst k(eq)))) pair(k(k(k(k(pair(p1,k(p2)))))),pair(pair(p1,p2),k(k(abst (abst k(abst) (abst k(isp1))))))))))) k(k(k(pair(p1,p2))))))) k(k(k(pair(p1,p2)))). 56 [assumption to refute] p. 57 [assumption to refute] badf z!=p1|z badx =p1|$ans(z). 58 [assumption to refute] -p|kintersection badf bady badx !=p1. 59 [ur,58,56,demod,54,6,6,1,6,1,6,6,1,6,1,6,1,4,1,6,1,4,1,4,4,5,1,1,1,6,6,1,6,6,1,6,1,4,1,6,1,4,1,4,1,1,1,1,6,6,6,1,4,1,6,1,4,1,4,1,1,1] eq pair(k(p2),abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx))))) pair(p1,p2) pair(p1,p2)!=p1. 78 [para_into,59.1.1.1.1,20.2.1,demod,2,2,2,3,unit_del,8,flip.1] abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx))))!=k(p2). 109 [ur,78,17,demod,6,1,4,1,4,6,6,1,51,1,51,1] eq pair(pair(p1,k(p2)),pair(badf noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)),k(isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx)))!=p2. 376 [ur,109,21,demod,2,3,flip.1] pair(badf noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)),k(isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx))=pair(p1,k(p2)). 5612 [ur,376,53] k(isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx)=k(p2). 5613 [ur,376,52] badf noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))=p1. 5716 [para_from,5612.1.1,9.1.1.1,demod,1,flip.1] isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx=p2. 5750 [ur,5613,57] noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx=p1|$ans(noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))). 5815 [para_into,5716.1.1,22.2.1,unit_del,19,5750] $ans(noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))).
up | previous | next | detailed contents | brief contents | OTTER output file