a(isp1,a(isp1,x)) = a(isp1,x). -----> EMPTY CLAUSE at 28.66 sec ----> 3055 [back_demod,2051,demod,3047,7,unit_del,33,3048] $F. Length of proof is 8. Level of proof is 3.
7 [reference] eq pair(x,x)=p1. 16 [reference] x=y|eq pair(x,y) =p2. 17 [reference] x=y|x noteq(x,y) !=y noteq(x,y). 18 [reference] p1!=p2. 19 [reference] x y!=p1|isp1 x y =p1. 20 [reference] x y=p1|isp1 x y =p2. 21 [assumption to refute] isp1 (isp1 bad)!=isp1 bad. 22 [ur,21,17] isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad)!=isp1 bad noteq(isp1 (isp1 bad),isp1 bad). 24,23 [ur,21,16] eq pair(isp1 (isp1 bad),isp1 bad)=p2. 33 [para_from,23.1.2,18.1.2,demod,24,flip.1] p2!=p1. 50 [ur,22,16] eq pair(isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad),isp1 bad noteq(isp1 (isp1 bad),isp1 bad))=p2. 59 [para_into,22.1.1,19.2.1,flip.1] isp1 bad noteq(isp1 (isp1 bad),isp1 bad)!=p1. 2051 [para_into,50.1.1.2.2,20.2.1] eq pair(isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad),p2)=p2|bad noteq(isp1 (isp1 bad),isp1 bad) =p1. 3047,3046 [ur,59,20] isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad)=p2. 3048 [ur,59,19] bad noteq(isp1 (isp1 bad),isp1 bad)!=p1. 3055 [back_demod,2051,demod,3047,7,unit_del,33,3048] $F.
up | previous | next | detailed contents | brief contents | OTTER output file