kintersecton -----> EMPTY CLAUSE at 17.48 sec ----> 923 [para_into,837.1.1.2.1,23.2.1,unit_del,8,53] $F. Length of proof is 5. Level of proof is 5.
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. 14 [reference] abst x y z=x k(z) (y z). 19 [reference] p2!=p1. 20 [reference] p1 x!=p2 x |eq x =p1. 21 [reference] p1 x=p2 x |eq x =p2. 23 [reference] x y=p1|isp1 x y =p2. 49 [reference] abst k(x) k(y)=k(x y). 50 [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)))). 51 [assumption to refute] p. 52 [assumption to refute] badf badz=p1. 53 [assumption to refute] badz badx!=p1. 54 [assumption to refute] -p|kintersection badf bad badx !=p2. 55 [ur,54,51,demod,50,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)!=p2. 161 [para_into,55.1.1.1.1,21.2.1,demod,3,3,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). 307 [para_from,161.1.1,14.1.1.1,demod,1,1,4,1,4,6,6,1,49,1,49,flip.1] eq pair(pair(p1,k(p2)),pair(badf x,k(isp1 x badx)))=p2. 824 [para_into,307.1.1,20.2.1,demod,2,3,unit_del,19,flip.1] pair(badf x,k(isp1 x badx))!=pair(p1,k(p2)). 837 [para_into,824.1.1.1,52.1.1] pair(p1,k(isp1 badz badx))!=pair(p1,k(p2)). 923 [para_into,837.1.1.2.1,23.2.1,unit_del,8,53] $F.
up | previous | next | detailed contents | brief contents | OTTER output file