a(isp1,a(isp1,x)) = a(isp1,x). ----> UNIT CONFLICT at 178.00 sec ----> 6295 [binary,6294.1,8.1] $F. Length of proof is 5. Level of proof is 4.
8 [reference] x=x. 15 [reference] x=y|x noteq(x,y) !=y noteq(x,y). 17 [reference] x y!=p1|isp1 x y =p1. 18 [reference] x y=p1|isp1 x y =p2. 19 [assumption to refute] isp1 (isp1 bad)!=isp1 bad. 20 [ur,19,15] isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad)!=isp1 bad noteq(isp1 (isp1 bad),isp1 bad). 74 [para_into,20.1.1,18.2.1,flip.1] isp1 bad noteq(isp1 (isp1 bad),isp1 bad)!=p2|isp1 bad noteq(isp1 (isp1 bad),isp1 bad) =p1. 76 [para_into,20.1.1,17.2.1,flip.1] isp1 bad noteq(isp1 (isp1 bad),isp1 bad)!=p1. 6168,6167 [para_into,74.1.1,18.2.1,unit_del,8,76] bad noteq(isp1 (isp1 bad),isp1 bad)=p1. 6294 [ur,76,17,demod,6168] p1!=p1. 6295 [binary,6294.1,8.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file