----- Otter 3.1-b0, May 2000 ----- -----> EMPTY CLAUSE at 1.09 sec ----> 592 [back_demod,6,demod,591,589,unit_del,4,4] $F. Length of proof is 52. Level of proof is 22. ---------------- PROOF ---------------- 1 [] (x# (y# (y#z)))# ((y# (y#x))#z)=p(x,y,z). 2 [] (x#z)# (x# (y#z))=f1(x,y,z). 3 [] (y#x)# (x#x)=f2(x,y). 4 [] x=x. 5 [] (X#Z)# (X# (Y#Z))!=X| (Y#X)# (X#X)!=X. 6 [copy,5,demod,2,3] f1(X,Y,Z)!=X|f2(X,Y)!=X. 7 [] (((((x#y)# (x# (z#y)))# (x# (x# ((u#v)# (v#v)))))# ((x# (x# ((x#y)# (x# (z#y)))))# ((u#v)# (v#v))))# (v# (v# ((w# (v6# (v6# ((w# (v7# (v7#v7)))# ((v7# (v7#w))#v7)))))# ((v6# (v6#w))# ((w# (v7# (v7#v7)))# ((v7# (v7#w))#v7)))))))# ((v# (v# ((((x#y)# (x# (z#y)))# (x# (x# ((u#v)# (v#v)))))# ((x# (x# ((x#y)# (x# (z#y)))))# ((u#v)# (v#v))))))# ((w# (v6# (v6# ((w# (v7# (v7#v7)))# ((v7# (v7#w))#v7)))))# ((v6# (v6#w))# ((w# (v7# (v7#v7)))# ((v7# (v7#w))#v7)))))=w. 9,8 [copy,7,demod,2,3,2,3,1,1,1,1,2,3,2,3,1,1,1,1,1] p(p(f1(x,y,z),x,f2(u,v)),u,p(w,v6,p(w,v7,v7)))=w. 10 [para_into,8.1.1.3.3,8.1.1] p(p(f1(x,y,z),x,f2(u,v)),u,p(p(f1(w,v6,v7),w,f2(p(v8,v9,p(v8,v10,v10)),v11)),v12,v8))=p(f1(w,v6,v7),w,f2(p(v8,v9,p(v8,v10,v10)),v11)). 13,12 [para_into,8.1.1.3,8.1.1] p(p(f1(x,y,z),x,f2(u,v)),u,p(f1(w,v6,v7),w,f2(v8,v9)))=p(f1(w,v6,v7),w,f2(v8,v9)). 15,14 [para_from,12.1.1,8.1.1.3.3] p(p(f1(x,y,z),x,f2(u,v)),u,p(p(f1(w,v6,v7),w,f2(p(f1(v8,v9,v10),v8,f2(v11,v12)),v13)),v14,p(f1(v8,v9,v10),v8,f2(v11,v12))))=p(f1(w,v6,v7),w,f2(p(f1(v8,v9,v10),v8,f2(v11,v12)),v13)). 20 [para_into,10.1.1.3.1.3.1.3,8.1.1,demod,9] p(p(f1(x,y,z),x,f2(u,v)),u,p(p(f1(w,v6,v7),w,f2(p(p(f1(v8,v9,v10),v8,f2(p(v11,v12,p(v11,v13,v13)),v14)),v15,v11),v16)),v17,p(f1(v8,v9,v10),v8,f2(p(v11,v12,p(v11,v13,v13)),v14))))=p(f1(w,v6,v7),w,f2(p(p(f1(v8,v9,v10),v8,f2(p(v11,v12,p(v11,v13,v13)),v14)),v15,v11),v16)). 23,22 [para_into,10.1.1.3,12.1.1,demod,13,flip.1] p(f1(x,y,z),x,f2(p(p(f1(u,v,w),u,f2(v6,v7)),v8,p(p(f1(u,v,w),u,f2(v6,v7)),v9,v9)),v10))=p(f1(u,v,w),u,f2(v6,v7)). 26 [para_into,10.1.1.3,8.1.1] p(p(f1(x,y,z),x,f2(u,v)),u,w)=p(f1(v6,v7,v8),v6,f2(p(p(w,v9,p(w,v10,v10)),v11,p(p(w,v9,p(w,v10,v10)),v12,v12)),v13)). 27 [copy,26,flip.1] p(f1(x,y,z),x,f2(p(p(u,v,p(u,w,w)),v6,p(p(u,v,p(u,w,w)),v7,v7)),v8))=p(p(f1(v9,v10,v11),v9,f2(v12,v13)),v12,u). 34,33 [para_into,26.1.1,8.1.1,flip.1] p(f1(x,y,z),x,f2(p(p(p(u,v,p(u,w,w)),v6,p(p(u,v,p(u,w,w)),v7,v7)),v8,p(p(p(u,v,p(u,w,w)),v6,p(p(u,v,p(u,w,w)),v7,v7)),v9,v9)),v10))=u. 36 [para_from,26.1.1,10.1.1.3.1.3.1,demod,23] p(p(f1(x,y,z),x,f2(u,v)),u,p(p(f1(w,v6,v7),w,f2(p(f1(v8,v9,v10),v8,f2(p(p(p(p(f1(v11,v12,v13),v11,f2(v14,v15)),v16,v16),v17,p(p(p(f1(v11,v12,v13),v11,f2(v14,v15)),v16,v16),v18,v18)),v19,p(p(p(p(f1(v11,v12,v13),v11,f2(v14,v15)),v16,v16),v17,p(p(p(f1(v11,v12,v13),v11,f2(v14,v15)),v16,v16),v18,v18)),v20,v20)),v21)),v22)),v23,p(f1(v11,v12,v13),v11,f2(v14,v15))))=p(f1(v11,v12,v13),v11,f2(v14,v15)). 41,40 [para_from,26.1.1,8.1.1.3,demod,13] p(f1(x,y,z),x,f2(p(p(p(p(f1(u,v,w),u,f2(v6,v7)),v8,v8),v9,p(p(p(f1(u,v,w),u,f2(v6,v7)),v8,v8),v10,v10)),v11,p(p(p(p(f1(u,v,w),u,f2(v6,v7)),v8,v8),v9,p(p(p(f1(u,v,w),u,f2(v6,v7)),v8,v8),v10,v10)),v12,v12)),v13))=p(f1(u,v,w),u,f2(v6,v7)). 46,45 [back_demod,36,demod,41,15] p(f1(x,y,z),x,f2(p(f1(u,v,w),u,f2(v6,v7)),v8))=p(f1(u,v,w),u,f2(v6,v7)). 57,56 [para_from,45.1.1,12.1.1.1] p(p(f1(x,y,z),x,f2(u,v)),p(f1(x,y,z),x,f2(u,v)),p(f1(w,v6,v7),w,f2(v8,v9)))=p(f1(w,v6,v7),w,f2(v8,v9)). 60 [para_from,45.1.1,8.1.1.1] p(p(f1(x,y,z),x,f2(u,v)),p(f1(x,y,z),x,f2(u,v)),p(w,v6,p(w,v7,v7)))=w. 129 [para_into,27.1.1.3.1.3.1.3,26.1.1,demod,13] p(f1(x,y,z),x,f2(p(p(p(f1(u,v,w),u,f2(v6,v7)),v8,p(p(f1(u,v,w),u,f2(v6,v7)),v6,v6)),v9,p(p(p(f1(u,v,w),u,f2(v6,v7)),v8,p(f1(v10,v11,v12),v10,f2(p(p(v6,v13,p(v6,v14,v14)),v15,p(p(v6,v13,p(v6,v14,v14)),v16,v16)),v17))),v18,v18)),v19))=p(f1(u,v,w),u,f2(v6,v7)). 133 [para_into,27.1.1,27.1.1] p(p(f1(x,y,z),x,f2(u,v)),u,w)=p(p(f1(v6,v7,v8),v6,f2(v9,v10)),v9,w). 137 [para_from,27.1.1,45.1.1.3.1] p(f1(x,y,z),x,f2(p(p(f1(u,v,w),u,f2(v6,v7)),v6,v8),v9))=p(f1(v10,v11,v12),v10,f2(p(p(v8,v13,p(v8,v14,v14)),v15,p(p(v8,v13,p(v8,v14,v14)),v16,v16)),v17)). 148 [para_from,27.1.1,60.1.1.1] p(p(p(f1(x,y,z),x,f2(u,v)),u,w),p(f1(v6,v7,v8),v6,f2(p(p(w,v9,p(w,v10,v10)),v11,p(p(w,v9,p(w,v10,v10)),v12,v12)),v13)),p(v14,v15,p(v14,v16,v16)))=v14. 152 [para_from,27.1.1,56.1.1.1] p(p(p(f1(x,y,z),x,f2(u,v)),u,w),p(f1(v6,v7,v8),v6,f2(p(p(w,v9,p(w,v10,v10)),v11,p(p(w,v9,p(w,v10,v10)),v12,v12)),v13)),p(f1(v14,v15,v16),v14,f2(v17,v18)))=p(f1(v14,v15,v16),v14,f2(v17,v18)). 154 [para_from,27.1.1,26.1.1.1] p(p(p(f1(x,y,z),x,f2(u,v)),u,w),p(p(w,v6,p(w,v7,v7)),v8,p(p(w,v6,p(w,v7,v7)),v9,v9)),v10)=p(f1(v11,v12,v13),v11,f2(p(p(v10,v14,p(v10,v15,v15)),v16,p(p(v10,v14,p(v10,v15,v15)),v17,v17)),v18)). 155 [para_from,27.1.1,12.1.1.1] p(p(p(f1(x,y,z),x,f2(u,v)),u,w),p(p(w,v6,p(w,v7,v7)),v8,p(p(w,v6,p(w,v7,v7)),v9,v9)),p(f1(v10,v11,v12),v10,f2(v13,v14)))=p(f1(v10,v11,v12),v10,f2(v13,v14)). 167 [para_into,133.1.1.1,45.1.1] p(p(f1(x,y,z),x,f2(u,v)),p(f1(x,y,z),x,f2(u,v)),w)=p(p(f1(v6,v7,v8),v6,f2(v9,v10)),v9,w). 169 [copy,167,flip.1] p(p(f1(x,y,z),x,f2(u,v)),u,w)=p(p(f1(v6,v7,v8),v6,f2(v9,v10)),p(f1(v6,v7,v8),v6,f2(v9,v10)),w). 179 [para_from,133.1.1,10.1.1.3] p(p(f1(x,y,z),x,f2(u,v)),u,p(p(f1(w,v6,v7),w,f2(v8,v9)),v8,v10))=p(f1(v11,v12,v13),v11,f2(p(v10,v14,p(v10,v15,v15)),v16)). 205 [para_into,20.1.1.3.1.3.1,133.1.1] p(p(f1(x,y,z),x,f2(u,v)),u,p(p(f1(w,v6,v7),w,f2(p(p(f1(v8,v9,v10),v8,f2(v11,v12)),v11,v13),v14)),v15,p(f1(v16,v17,v18),v16,f2(p(v13,v19,p(v13,v20,v20)),v21))))=p(f1(w,v6,v7),w,f2(p(p(f1(v16,v17,v18),v16,f2(p(v13,v19,p(v13,v20,v20)),v21)),p(v13,v19,p(v13,v20,v20)),v13),v14)). 224,223 [para_into,20.1.1.3,133.1.1,demod,13,13,flip.1] p(f1(x,y,z),x,f2(p(p(f1(u,v,w),u,f2(p(v6,v7,p(v6,v8,v8)),v9)),v10,v6),v11))=p(f1(u,v,w),u,f2(p(v6,v7,p(v6,v8,v8)),v9)). 232,231 [copy,205,flip.1,demod,224,flip.1] p(p(f1(x,y,z),x,f2(u,v)),u,p(p(f1(w,v6,v7),w,f2(p(p(f1(v8,v9,v10),v8,f2(v11,v12)),v11,v13),v14)),v15,p(f1(v16,v17,v18),v16,f2(p(v13,v19,p(v13,v20,v20)),v21))))=p(f1(v16,v17,v18),v16,f2(p(v13,v19,p(v13,v20,v20)),v21)). 313 [para_from,179.1.1,60.1.1.3,demod,57] p(f1(x,y,z),x,f2(p(u,v,p(u,w,w)),v6))=p(f1(v7,v8,v9),v7,f2(u,v10)). 316 [para_from,179.1.1,8.1.1.3.3,demod,232] p(f1(x,y,z),x,f2(p(u,v,p(u,w,w)),v6))=p(f1(v7,v8,v9),v7,f2(p(p(f1(v10,v11,v12),v10,f2(v13,v14)),v13,u),v15)). 317 [copy,313,flip.1] p(f1(x,y,z),x,f2(u,v))=p(f1(w,v6,v7),w,f2(p(u,v8,p(u,v9,v9)),v10)). 318 [copy,316,flip.1] p(f1(x,y,z),x,f2(p(p(f1(u,v,w),u,f2(v6,v7)),v6,v8),v9))=p(f1(v10,v11,v12),v10,f2(p(v8,v13,p(v8,v14,v14)),v15)). 330 [para_into,313.1.1.3.1,169.1.1,demod,46] p(f1(x,y,z),x,f2(p(p(f1(u,v,w),u,f2(v6,v7)),p(f1(u,v,w),u,f2(v6,v7)),p(p(f1(v8,v9,v10),v8,f2(v11,v12)),v13,v13)),v14))=p(f1(v8,v9,v10),v8,f2(v11,v12)). 397 [para_from,22.1.1,179.1.1.1] p(p(f1(x,y,z),x,f2(u,v)),p(p(f1(x,y,z),x,f2(u,v)),w,p(p(f1(x,y,z),x,f2(u,v)),v6,v6)),p(p(f1(v7,v8,v9),v7,f2(v10,v11)),v10,v12))=p(f1(v13,v14,v15),v13,f2(p(v12,v16,p(v12,v17,v17)),v18)). 399 [para_from,22.1.1,133.1.1.1] p(p(f1(x,y,z),x,f2(u,v)),p(p(f1(x,y,z),x,f2(u,v)),w,p(p(f1(x,y,z),x,f2(u,v)),v6,v6)),v7)=p(p(f1(v8,v9,v10),v8,f2(v11,v12)),v11,v7). 410 [copy,397,flip.1] p(f1(x,y,z),x,f2(p(u,v,p(u,w,w)),v6))=p(p(f1(v7,v8,v9),v7,f2(v10,v11)),p(p(f1(v7,v8,v9),v7,f2(v10,v11)),v12,p(p(f1(v7,v8,v9),v7,f2(v10,v11)),v13,v13)),p(p(f1(v14,v15,v16),v14,f2(v17,v18)),v17,u)). 412 [copy,399,flip.1] p(p(f1(x,y,z),x,f2(u,v)),u,w)=p(p(f1(v6,v7,v8),v6,f2(v9,v10)),p(p(f1(v6,v7,v8),v6,f2(v9,v10)),v11,p(p(f1(v6,v7,v8),v6,f2(v9,v10)),v12,v12)),w). 436,435 [para_into,317.1.1,27.1.1,demod,34] p(p(f1(x,y,z),x,f2(u,v)),u,w)=w. 452,451 [back_demod,412,demod,436,flip.1] p(p(f1(x,y,z),x,f2(u,v)),p(p(f1(x,y,z),x,f2(u,v)),w,p(p(f1(x,y,z),x,f2(u,v)),v6,v6)),v7)=v7. 454,453 [back_demod,410,demod,436,452] p(f1(x,y,z),x,f2(p(u,v,p(u,w,w)),v6))=u. 486,485 [back_demod,318,demod,436,454] p(f1(x,y,z),x,f2(u,v))=u. 555,554 [back_demod,155,demod,486,486,486] p(p(x,x,y),p(p(y,z,p(y,u,u)),v,p(p(y,z,p(y,u,u)),w,w)),v6)=v6. 557,556 [back_demod,154,demod,486,555,486,flip.1] p(p(x,y,p(x,z,z)),u,p(p(x,y,p(x,z,z)),v,v))=x. 559,558 [back_demod,152,demod,486,557,486,486,486] p(p(x,x,y),y,z)=z. 563,562 [back_demod,148,demod,486,557,486,559] p(x,y,p(x,z,z))=x. 573,572 [back_demod,137,demod,486,486,563,563,563,486] p(x,x,y)=y. 578 [back_demod,129,demod,486,486,573,486,563,563,563,486,563,486,486] p(x,y,x)=x. 582 [back_demod,330,demod,486,486,486,573,486,486] p(x,y,y)=x. 584 [para_into,582.1.1,485.1.1,flip.1] f1(f2(x,y),z,u)=x. 586 [para_from,584.1.1,485.1.1.1] p(x,f2(x,y),f2(z,u))=z. 589,588 [para_into,586.1.1,578.1.1] f2(x,y)=x. 591,590 [back_demod,584,demod,589] f1(x,y,z)=x. 592 [back_demod,6,demod,591,589,unit_del,4,4] $F. ------------ end of proof -------------