a(charq,xf) = p2 | a(a(xf,x),pair(p1,p2)) = a(xf,x). -----> EMPTY CLAUSE at 1.56 sec ----> 606 [back_demod,556,demod,595,2,7,595,unit_del,65,65] $F. Length of proof is 7. Level of proof is 3.
2 [reference] p1 pair(x,y)=x. 3 [reference] p2 pair(x,y)=y. 7 [reference] eq pair(x,x)=p1. 8 [reference] x=x. 16 [reference] x=y|eq pair(x,y) =p2. 18 [reference] p1!=p2. 32 [reference] charq xf=p2|xf x =p1|xf x =p2. 45 [assumption to refute] charq badf!=p2. 46 [assumption to refute] badf badx pair(p1,p2)!=badf badx. 56 [para_into,45.1.1,32.2.1,unit_del,45,flip.1] p2!=p1|charq charq =p2. 64 [para_from,56.2.2,18.1.2,flip.1] charq charq!=p1|p2!=p1. 65 [para_into,64.1.1,56.2.1] p2!=p1. 76 [ur,46,16] eq pair(badf badx pair(p1,p2),badf badx)=p2. 78 [para_into,46.1.1.1,32.3.1,demod,3,unit_del,45,flip.1] badf badx!=p2|badf badx =p1. 556 [para_into,76.1.1.2.2,32.2.1,unit_del,45] eq pair(badf badx pair(p1,p2),p1)=p2|badf badx =p2. 595,594 [para_into,78.1.1,32.3.1,unit_del,8,45] badf badx=p1. 606 [back_demod,556,demod,595,2,7,595,unit_del,65,65] $F.
up | previous | next | detailed contents | brief contents | OTTER output file