----- Otter 3.1-b0, May 2000 ----- The process was started by wos on jaguar.mcs.anl.gov, Tue Jul 4 08:56:01 2000 The command was "otter". The process ID is 17597. ----> UNIT CONFLICT at 131.24 sec ----> 18271 [binary,18270.1,3.1] $ANS(SING_4). Length of proof is 66. Level of proof is 40. ---------------- PROOF ---------------- 2 [] f(f(f(x,y),z),f(x,f(f(x,z),x)))=z. 3 [] f(f(f(a,f(b,a)),a),f(b,f(c,a)))!=b|$ANS(SING_4). 73 [para_into,2.1.1.1.1,2.1.1] f(f(x,y),f(f(f(z,u),x),f(f(f(f(z,u),x),y),f(f(z,u),x))))=y. 74 [para_into,2.1.1.1,2.1.1] f(x,f(f(y,z),f(f(f(y,z),f(y,f(f(y,x),y))),f(y,z))))=f(y,f(f(y,x),y)). 76 [para_into,2.1.1.2.2,2.1.1] f(f(f(f(x,f(f(x,y),x)),z),y),f(f(x,f(f(x,y),x)),y))=y. 86 [para_into,73.1.1.2.2.1,2.1.1] f(f(x,f(y,f(f(y,x),y))),f(f(f(y,z),x),f(x,f(f(y,z),x))))=f(y,f(f(y,x),y)). 91 [para_from,73.1.1,2.1.1.1.1] f(f(x,y),f(f(z,x),f(f(f(z,x),y),f(z,x))))=y. 95 [para_from,74.1.1,2.1.1.1.1] f(f(f(x,f(f(x,y),x)),z),f(y,f(f(y,z),y)))=z. 103 [para_into,91.1.1.2.2.1,91.1.1] f(f(x,f(f(y,z),f(f(f(y,z),x),f(y,z)))),f(f(z,x),f(x,f(z,x))))=f(f(y,z),f(f(f(y,z),x),f(y,z))). 105 [para_from,91.1.1,2.1.1.2.2.1] f(f(f(f(x,y),z),f(f(u,x),f(f(f(u,x),y),f(u,x)))),f(f(x,y),f(y,f(x,y))))=f(f(u,x),f(f(f(u,x),y),f(u,x))). 116 [para_from,95.1.1,2.1.1.1] f(x,f(f(y,f(f(y,z),y)),f(f(f(y,f(f(y,z),y)),f(z,f(f(z,x),z))),f(y,f(f(y,z),y)))))=f(z,f(f(z,x),z)). 127 [para_into,86.1.1.2,2.1.1] f(f(x,f(x,f(f(x,x),x))),x)=f(x,f(f(x,x),x)). 158 [para_from,127.1.1,2.1.1.2.2] f(f(f(x,y),f(x,f(f(x,x),x))),f(x,f(x,f(f(x,x),x))))=f(x,f(f(x,x),x)). 159 [para_from,127.1.1,2.1.1.1] f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x)))=x. 171 [para_from,127.1.2,74.1.1.2.2.1.2] f(x,f(f(x,y),f(f(f(x,y),f(f(x,f(x,f(f(x,x),x))),x)),f(x,y))))=f(x,f(f(x,x),x)). 200 [para_from,159.1.1,2.1.1.1.1] f(f(x,y),f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),y),f(x,f(f(x,x),x)))))=y. 207 [para_into,158.1.1.1,159.1.1] f(x,f(x,f(x,f(f(x,x),x))))=f(x,f(f(x,x),x)). 217 [para_from,158.1.1,76.1.1.1] f(f(x,f(f(x,x),x)),f(f(x,f(f(x,f(x,f(x,f(f(x,x),x)))),x)),f(x,f(x,f(f(x,x),x)))))=f(x,f(x,f(f(x,x),x))). 331 [para_from,103.1.1,2.1.1.1] f(f(f(x,y),f(f(f(x,y),z),f(x,y))),f(z,f(f(z,f(f(y,z),f(z,f(y,z)))),z)))=f(f(y,z),f(z,f(y,z))). 363 [para_into,116.1.1.2.2.1,200.1.1] f(f(f(x,f(x,f(f(x,x),x))),x),f(f(x,f(f(x,f(x,f(f(x,x),x))),x)),f(f(f(x,f(x,f(f(x,x),x))),x),f(x,f(f(x,f(x,f(f(x,x),x))),x)))))=f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(f(x,f(x,f(f(x,x),x))),x)),f(x,f(f(x,x),x)))). 381 [para_into,217.1.1.2.1.2.1,207.1.1] f(f(x,f(f(x,x),x)),f(f(x,f(f(x,f(f(x,x),x)),x)),f(x,f(x,f(f(x,x),x)))))=f(x,f(x,f(f(x,x),x))). 399 [para_into,363.1.1.1,127.1.1] f(f(x,f(f(x,x),x)),f(f(x,f(f(x,f(x,f(f(x,x),x))),x)),f(f(f(x,f(x,f(f(x,x),x))),x),f(x,f(f(x,f(x,f(f(x,x),x))),x)))))=f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(f(x,f(x,f(f(x,x),x))),x)),f(x,f(f(x,x),x)))). 402 [para_into,399.1.1.2.1.2,127.1.1] f(f(x,f(f(x,x),x)),f(f(x,f(x,f(f(x,x),x))),f(f(f(x,f(x,f(f(x,x),x))),x),f(x,f(f(x,f(x,f(f(x,x),x))),x)))))=f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(f(x,f(x,f(f(x,x),x))),x)),f(x,f(f(x,x),x)))). 403 [para_into,402.1.1.2,86.1.1,flip.1] f(f(x,f(f(x,x),x)),f(f(f(x,f(f(x,x),x)),f(f(x,f(x,f(f(x,x),x))),x)),f(x,f(f(x,x),x))))=f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))). 407 [para_from,403.1.1,171.1.1.2] f(x,f(f(x,f(f(x,x),x)),f(x,f(f(x,x),x))))=f(x,f(f(x,x),x)). 426 [para_into,407.1.1.2,159.1.1,flip.1] f(x,f(f(x,x),x))=f(x,x). 487 [para_from,426.1.1,381.1.1.1] f(f(x,x),f(f(x,f(f(x,f(f(x,x),x)),x)),f(x,f(x,f(f(x,x),x)))))=f(x,f(x,f(f(x,x),x))). 492 [para_from,426.1.1,159.1.1.2] f(f(x,f(f(x,x),x)),f(x,x))=x. 517 [para_from,426.1.1,91.1.1.2] f(f(x,f(y,x)),f(f(y,x),f(y,x)))=f(y,x). 561 [para_from,426.1.1,2.1.1.2] f(f(f(x,y),x),f(x,x))=x. 649 [para_into,561.1.1.1,561.1.1] f(x,f(f(x,x),f(x,x)))=f(x,x). 687 [para_into,492.1.1.1,426.1.1] f(f(x,x),f(x,x))=x. 718 [para_from,687.1.1,426.1.1.2.1] f(f(x,x),f(x,f(x,x)))=f(f(x,x),f(x,x)). 733 [para_from,687.1.1,91.1.1.2.2.1] f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x))))=f(x,x). 1116 [para_into,718.1.2,687.1.1] f(f(x,x),f(x,f(x,x)))=x. 1137 [para_from,718.1.2,649.1.1.2] f(x,f(f(x,x),f(x,f(x,x))))=f(x,x). 1175 [para_into,1116.1.1.2.2,426.1.2] f(f(x,x),f(x,f(x,f(f(x,x),x))))=x. 1262 [para_from,1137.1.2,426.1.1.2.1] f(x,f(f(x,f(f(x,x),f(x,f(x,x)))),x))=f(x,x). 1321 [para_into,1175.1.1.1,426.1.2] f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x))))=x. 1494 [para_from,1262.1.1,331.1.1.2] f(f(f(x,y),f(f(f(x,y),y),f(x,y))),f(y,y))=f(f(y,y),f(y,f(y,y))). 1811 [para_into,1494.1.2,1116.1.1] f(f(f(x,y),f(f(f(x,y),y),f(x,y))),f(y,y))=y. 1888 [para_from,1811.1.1,2.1.1.1] f(x,f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x))))=f(x,x). 2078 [para_into,487.1.1.2.1.2.1,426.1.1] f(f(x,x),f(f(x,f(f(x,x),x)),f(x,f(x,f(f(x,x),x)))))=f(x,f(x,f(f(x,x),x))). 2155 [para_into,2078.1.1.2,1321.1.1,flip.1] f(x,f(x,f(f(x,x),x)))=f(f(x,x),x). 2197 [para_into,2155.1.1.2,426.1.1,flip.1] f(f(x,x),x)=f(x,f(x,x)). 2543 [para_from,2197.1.1,561.1.1.1] f(f(x,f(x,x)),f(x,x))=x. 2667 [para_from,2543.1.1,105.1.1.1.1] f(f(x,f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x)))),f(f(x,f(x,x)),f(f(x,x),f(x,f(x,x)))))=f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x))). 2753 [para_into,2667.1.1.2,733.1.1] f(f(x,f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x)))),f(x,x))=f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x))). 2780 [para_into,2753.1.1.1,1888.1.1,flip.1] f(f(x,y),f(f(f(x,y),f(y,y)),f(x,y)))=f(f(y,y),f(y,y)). 2912 [para_into,2780.1.2,687.1.1] f(f(x,y),f(f(f(x,y),f(y,y)),f(x,y)))=y. 3041 [para_into,2912.1.1.2.1,517.1.1] f(f(x,f(y,x)),f(f(y,x),f(x,f(y,x))))=f(y,x). 3043 [para_into,2912.1.1.2.1,561.1.1] f(f(f(x,y),x),f(x,f(f(x,y),x)))=x. 3261 [para_into,3041.1.1.1,2912.1.1] f(x,f(f(f(f(y,x),f(x,x)),f(y,x)),f(f(y,x),f(f(f(y,x),f(x,x)),f(y,x)))))=f(f(f(y,x),f(x,x)),f(y,x)). 3761 [para_into,3261.1.1.2,3043.1.1,flip.1] f(f(f(x,y),f(y,y)),f(x,y))=f(y,f(x,y)). 3888 [para_from,3761.1.1,2912.1.1.2] f(f(x,y),f(y,f(x,y)))=y. 4108 [para_into,3888.1.1.2,3888.1.1] f(f(x,f(y,x)),x)=f(y,x). 4266 [para_from,4108.1.1,116.1.1.2.2.1] f(x,f(f(f(y,f(f(y,x),y)),f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y)))),f(f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y))),f(f(y,f(f(y,x),y)),f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y)))))))=f(y,f(f(y,x),y)). 8181 [para_into,4266.1.1.2.1.2.1,4108.1.1] f(x,f(f(f(y,f(f(y,x),y)),f(f(f(y,x),y),f(y,f(f(y,x),y)))),f(f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y))),f(f(y,f(f(y,x),y)),f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y)))))))=f(y,f(f(y,x),y)). 8254 [para_into,8181.1.1.2.1,3888.1.1] f(x,f(f(f(y,x),y),f(f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y))),f(f(y,f(f(y,x),y)),f(f(f(y,f(f(y,x),y)),y),f(y,f(f(y,x),y)))))))=f(y,f(f(y,x),y)). 8258 [para_into,8254.1.1.2.2,3888.1.1] f(x,f(f(f(y,x),y),f(y,f(f(y,x),y))))=f(y,f(f(y,x),y)). 8359 [para_into,8258.1.1.2,3888.1.1,flip.1] f(x,f(f(x,y),x))=f(y,x). 8805 [para_from,8359.1.1,91.1.1.2] f(f(x,y),f(y,f(z,x)))=y. 8949 [para_from,8359.1.1,2.1.1.2] f(f(f(x,y),z),f(z,x))=z. 10966 [para_into,8949.1.1.1.1,8359.1.1] f(f(f(x,y),z),f(z,y))=z. 12952 [para_into,10966.1.1.1,10966.1.1] f(x,f(f(x,y),x))=f(x,y). 14373 [para_into,12952.1.1,8359.1.1] f(x,y)=f(y,x). 15042 [para_into,14373.1.1,4108.1.2] f(f(x,f(y,x)),x)=f(x,y). 18270 [para_from,15042.1.2,8805.1.1.1] f(f(f(x,f(y,x)),x),f(y,f(z,x)))=y. 18271 [binary,18270.1,3.1] $ANS(SING_4). ------------ end of proof -------------