subset para_into_units_only and para_from_units_only options.----> UNIT CONFLICT at 4.36 sec ----> 356 [binary,355.1,19.1] $ans(noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))). Length of proof is 8. Level of proof is 7.
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). 6 [reference] abst x y z=x k(z) (y z). 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. 52 [reference] pair(x1,y1)!=pair(x2,y2)|x1=x2. 53 [reference] pair(x1,y1)!=pair(x2,y2)|y1=y2. 57 [reference] subset=abst k(eq) pair(k(k(p2)),abst k(abst k(eq)) pair(k(k(pair(p1,p2))),pair(p1,abst k(isp1) p2))). 59 [assumption to refute] -p|subset pair(bad1,bad2) !=p1. 60 [assumption to refute] bad1 x!=p1|bad2 x =p1|$ans(x). 61 [assumption to refute] p. 62 [ur,59,61,demod,57,6,1,4,1,6,1,4,1,4,2,6,1,3] eq pair(k(p2),abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)))!=p1. 72 [ur,62,20,demod,2,3,flip.1] abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2))!=k(p2). 87 [ur,72,17,demod,6,1,4,1,4,1] eq pair(pair(p1,p2),pair(bad1 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)), isp1 bad2 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))))!=p2. 199 [ur,87,21,demod,2,3,flip.1] pair(bad1 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)),isp1 bad2 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)))=pair(p1,p2). 295,294 [ur,199,53] isp1 bad2 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))=p2. 296 [ur,199,52] bad1 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))=p1. 344 [ur,296,60] bad2 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))=p1|$ans(noteq(abst k(eq) pair(k(pair(p1,p 2)),pair(bad1,isp1 bad2)),k(p2))). 355 [ur,344,22,demod,295] $ans(noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)))|p2=p1. 356 [binary,355.1,19.1] $ans(noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))).
up | previous | next | detailed contents | brief contents | OTTER output file