a(notp1,a(isp1,x)) = a(notp1,x). ----> UNIT CONFLICT at 1.93 sec ----> 820 [binary,818.1,806.1] $F. Length of proof is 6. Level of proof is 5.
14 [reference] x=y|x noteq(x,y) !=y noteq(x,y). 16 [reference] x y!=p1|isp1 x y =p1. 17 [reference] x y=p1|isp1 x y =p2. 23 [reference] notp1 x y=p1|notp1 x y =p2. 24 [reference] notp1 (notp1 x)=isp1 x. 25 [assumption to refute] notp1 (isp1 bad)!=notp1 bad. 26 [ur,25,14] notp1 (isp1 bad) noteq(notp1 (isp1 bad),notp1 bad)!=notp1 bad noteq(notp1 (isp1 bad),notp1 bad). 36 [para_into,26.1.1.1.2,24.1.2] notp1 (notp1 (notp1 bad)) noteq(notp1 (isp1 bad),notp1 bad)!=notp1 bad noteq(notp1 (isp1 bad),n otp1 bad). 746 [para_into,36.1.1.1,24.1.1] isp1 (notp1 bad) noteq(notp1 (isp1 bad),notp1 bad)!=notp1 bad noteq(notp1 (isp1 bad),notp1 bad). 794 [para_into,746.1.1,16.2.1,flip.1] notp1 bad noteq(notp1 (isp1 bad),notp1 bad)!=p1. 806 [para_into,746.1.2,23.2.1,unit_del,794] isp1 (notp1 bad) noteq(notp1 (isp1 bad),notp1 bad)!=p2. 818 [ur,794,17] isp1 (notp1 bad) noteq(notp1 (isp1 bad),notp1 bad)=p2. 820 [binary,818.1,806.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file