----- Otter 3.1-b0, May 2000 ----- The process was started by wos on jaguar.mcs.anl.gov, Tue Jul 4 18:33:13 2000 The command was "otter". The process ID is 29790. ----> UNIT CONFLICT at 210.48 sec ----> 24983 [binary,24982.1,3.1] $ANS(SING_1). Length of proof is 68. Level of proof is 41. ---------------- PROOF ---------------- 2 [] f(f(f(x,f(y,x)),x),f(y,f(z,x)))=y. 3 [] f(f(f(a,b),c),f(f(a,f(a,c)),a))!=c|$ANS(SING_1). 85 [para_into,2.1.1.1.1.2,2.1.1] f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),f(f(f(z,f(x,z)),z),f(u,f(x,f(y,z)))))=f(f(z,f(x,z)),z). 86 [para_into,2.1.1.2,2.1.1] f(f(f(f(x,y),f(f(f(y,f(z,y)),y),f(x,y))),f(x,y)),z)=f(f(y,f(z,y)),y). 97 [para_from,86.1.1,2.1.1.2.2] f(f(f(x,f(y,x)),x),f(y,f(f(z,f(x,z)),z)))=y. 109 [para_into,97.1.1.1.1,2.1.1] f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(z,f(f(f(y,f(x,y)),y),z)),z)))=x. 134 [para_into,85.1.1.2.2,2.1.1] f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),f(f(f(z,f(x,z)),z),x))=f(f(z,f(x,z)),z). 161 [para_into,134.1.1.1,2.1.1] f(x,f(f(f(x,f(x,x)),x),x))=f(f(x,f(x,x)),x). 188 [para_into,161.1.1.2.1,161.1.2] f(x,f(f(x,f(f(f(x,f(x,x)),x),x)),x))=f(f(x,f(x,x)),x). 198 [para_from,161.1.1,134.1.1.1.1.1] f(f(f(f(f(x,f(x,x)),x),x),f(x,f(f(f(x,f(x,x)),x),x))),f(f(f(x,f(x,x)),x),x))=f(f(x,f(x,x)),x). 209 [para_from,161.1.1,2.1.1.2] f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))=x. 250 [para_from,209.1.1,97.1.1.2] f(f(f(x,f(f(f(x,f(x,x)),x),x)),x),x)=f(f(x,f(x,x)),x). 252 [para_from,209.1.1,86.1.1.1.1.2] f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),x)=f(f(x,f(x,x)),x). 253 [para_from,209.1.1,2.1.1.2.2] f(f(f(f(f(x,f(x,x)),x),f(y,f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)),f(y,x))=y. 284 [para_from,188.1.1,109.1.1.2] f(f(x,f(f(x,f(x,x)),x)),f(f(x,f(x,x)),x))=x. 341 [para_into,250.1.1.1.1,161.1.1] f(f(f(f(x,f(x,x)),x),x),x)=f(f(x,f(x,x)),x). 418 [para_from,341.1.1,2.1.1.1.1.2] f(f(f(x,f(f(x,f(x,x)),x)),x),f(f(f(f(x,f(x,x)),x),x),f(y,x)))=f(f(f(x,f(x,x)),x),x). 525 [para_into,253.1.1.1.1.2,284.1.1] f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(x,f(x,x)),x)),x))=f(x,f(f(x,f(x,x)),x)). 526 [para_into,253.1.1.1.1.2,209.1.1] f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),x))=f(f(x,f(x,x)),x). 546 [para_from,253.1.1,2.1.1.2.2] f(f(f(f(x,y),f(z,f(x,y))),f(x,y)),f(z,x))=z. 694 [para_from,546.1.1,109.1.1.2.2.1.2] f(f(x,f(f(f(y,z),f(x,f(y,z))),f(y,z))),f(x,f(f(f(x,y),x),f(x,y))))=x. 698 [para_from,546.1.1,2.1.1.2] f(f(f(x,f(f(f(f(x,y),f(z,f(x,y))),f(x,y)),x)),x),z)=f(f(f(x,y),f(z,f(x,y))),f(x,y)). 847 [para_from,526.1.1,694.1.1.2.2] f(f(f(f(x,f(x,x)),x),f(f(f(x,y),f(f(f(x,f(x,x)),x),f(x,y))),f(x,y))),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x)))=f(f(x,f(x,x)),x). 971 [para_from,198.1.1,97.1.1.1] f(f(f(x,f(x,x)),x),f(x,f(f(y,f(f(f(f(x,f(x,x)),x),x),y)),y)))=x. 1030 [para_into,971.1.1.2.2.1,418.1.1] f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x))))=x. 1263 [para_into,847.1.1.2,209.1.1] f(f(f(f(x,f(x,x)),x),f(f(f(x,y),f(f(f(x,f(x,x)),x),f(x,y))),f(x,y))),x)=f(f(x,f(x,x)),x). 1290 [para_into,1263.1.1.1.2.1.1,1030.1.1] f(f(f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)),f(f(x,f(f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)). 1364 [para_into,1290.1.1.1.1.1.2,209.1.1] f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)). 1384 [para_into,1364.1.1.1.2.1.2.1.1.2,209.1.1] f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)). 1385 [para_into,1384.1.1.1.2.1.2.2,1030.1.1] f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),x)),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)). 1386 [para_into,1385.1.1.1.2.1.2,252.1.1] f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)). 1402 [para_into,1386.1.1.1.2.2,1030.1.1] f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(x,f(x,x)),x)),x)),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)). 1403 [para_into,1402.1.1.1,525.1.1,flip.1] f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x))=f(f(x,f(f(x,f(x,x)),x)),f(f(x,f(x,x)),x)). 1434 [para_into,1403.1.2,284.1.1] f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x))=x. 1525 [para_from,1434.1.1,86.1.1.1,flip.1] f(f(x,f(x,x)),x)=f(x,x). 1527 [para_into,1525.1.1.1.2,1525.1.2] f(f(x,f(f(x,f(x,x)),x)),x)=f(x,x). 1599 [para_from,1525.1.1,209.1.1.1] f(f(x,x),f(f(x,f(x,x)),x))=x. 1679 [para_from,1525.1.1,2.1.1.1] f(f(x,x),f(x,f(y,x)))=x. 1900 [para_from,1679.1.1,97.1.1.2.2.1] f(f(f(x,f(y,x)),x),f(y,f(x,f(x,x))))=y. 1916 [para_from,1679.1.1,2.1.1.2] f(f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y)),y)=f(y,y). 2027 [para_from,1527.1.1,86.1.1.1.1.2.1] f(f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y)),f(y,f(y,y)))=f(f(y,f(f(y,f(y,y)),y)),y). 2334 [para_from,1916.1.1,1900.1.1.1.1.2] f(f(f(x,f(x,x)),x),f(f(f(f(y,x),f(f(x,x),f(y,x))),f(y,x)),f(x,f(x,x))))=f(f(f(y,x),f(f(x,x),f(y,x))),f(y,x)). 2515 [para_into,2027.1.2,1527.1.1] f(f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y)),f(y,f(y,y)))=f(y,y). 2753 [para_into,2334.1.1.1,1525.1.1] f(f(x,x),f(f(f(f(y,x),f(f(x,x),f(y,x))),f(y,x)),f(x,f(x,x))))=f(f(f(y,x),f(f(x,x),f(y,x))),f(y,x)). 2889 [para_into,2753.1.1.2,2515.1.1,flip.1] f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y))=f(f(y,y),f(y,y)). 3477 [para_into,1599.1.1.2,1525.1.1] f(f(x,x),f(x,x))=x. 3539 [para_into,3477.1.1,2889.1.2] f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y))=y. 3804 [para_from,3539.1.1,546.1.1.1] f(x,f(f(x,x),y))=f(x,x). 3858 [para_into,3804.1.1.2.1,3477.1.1] f(f(x,x),f(x,y))=f(f(x,x),f(x,x)). 4410 [para_into,3858.1.2,3477.1.1] f(f(x,x),f(x,y))=x. 4419 [para_into,4410.1.1.1,1525.1.2] f(f(f(x,f(x,x)),x),f(x,y))=x. 4456 [para_from,4410.1.1,698.1.1.1.1.2.1.1.2] f(f(f(x,f(f(f(f(x,y),x),f(x,y)),x)),x),f(x,x))=f(f(f(x,y),f(f(x,x),f(x,y))),f(x,y)). 4512 [para_from,4410.1.1,2.1.1.2] f(f(f(x,f(f(y,y),x)),x),y)=f(y,y). 4869 [para_into,4512.1.1.1.1.2,4410.1.1] f(f(f(f(x,y),x),f(x,y)),x)=f(x,x). 8432 [para_into,4456.1.2.1.2,4410.1.1] f(f(f(x,f(f(f(f(x,y),x),f(x,y)),x)),x),f(x,x))=f(f(f(x,y),x),f(x,y)). 8565 [para_into,8432.1.1.1.1.2,4869.1.1] f(f(f(x,f(x,x)),x),f(x,x))=f(f(f(x,y),x),f(x,y)). 8711 [para_into,8565.1.1,4419.1.1,flip.1] f(f(f(x,y),x),f(x,y))=x. 8971 [para_into,8711.1.1.1,3539.1.1] f(x,f(f(y,x),f(f(x,x),f(y,x))))=f(y,x). 9370 [para_from,8971.1.1,4410.1.1.2] f(f(x,x),f(y,x))=x. 9777 [para_from,9370.1.1,3539.1.1.1.2] f(f(f(x,y),y),f(x,y))=y. 10834 [para_into,9777.1.1.1.1,9777.1.1] f(f(x,f(y,x)),f(f(f(y,x),x),f(y,x)))=f(y,x). 13378 [para_into,10834.1.1.2,9777.1.1] f(f(x,f(y,x)),x)=f(y,x). 13842 [para_into,13378.1.1.1.2,13378.1.2] f(f(x,f(f(x,f(y,x)),x)),x)=f(y,x). 14181 [para_from,13378.1.1,97.1.1.2.2] f(f(f(x,f(y,x)),x),f(y,f(x,z)))=y. 14297 [para_from,13378.1.1,2.1.1.1] f(f(x,y),f(x,f(z,y)))=x. 14724 [para_into,14297.1.1.1,8711.1.1] f(x,f(f(f(x,y),x),f(z,f(x,y))))=f(f(x,y),x). 22219 [para_into,14724.1.1.2,14181.1.1,flip.1] f(f(x,f(y,x)),x)=f(x,y). 22906 [para_from,22219.1.1,546.1.1.1] f(f(f(x,y),z),f(z,x))=z. 22996 [para_from,22219.1.1,13842.1.1.1.2] f(f(x,f(x,y)),x)=f(y,x). 24982 [para_from,22996.1.2,22906.1.1.2] f(f(f(x,y),z),f(f(x,f(x,z)),x))=z. 24983 [binary,24982.1,3.1] $ANS(SING_1). ------------ end of proof ------------- given clause #145: (wt=59) 135 [para_into,85.1.2,85.1.2] f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),f(f(f(z,f(x,z)),z),f(u,f(x,f(y,z)))))=f(f(f(f(x,f(v,z)),x),f(x,f(v,z))),f(f(f(z,f(x,z)),z),f(w,f(x,f(v,z))))). given clause #146: (wt=-1013) 23099 [para_from,22219.1.1,2.1.1.1] f(f(x,y),f(y,f(z,x)))=y. given clause #147: (wt=-1011) 25318 [para_from,22996.1.2,14855.1.1.1] f(f(f(x,f(x,y)),x),f(y,y))=y. given clause #148: (wt=-1009) 22595 [para_into,22219.1.1.1.2,22219.1.2] f(f(x,f(f(y,f(x,y)),y)),x)=f(x,y). given clause #149: (wt=51) 136 [para_into,85.1.2,86.1.2] f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),f(f(f(z,f(x,z)),z),f(u,f(x,f(y,z)))))=f(f(f(f(v,z),f(f(f(z,f(x,z)),z),f(v,z))),f(v,z)),x). given clause #150: (wt=-1009) 22621 [para_into,22219.1.1.1.2,13378.1.2] f(f(x,f(f(x,f(y,x)),x)),x)=f(x,y). given clause #151: (wt=-1009) 22719 [para_into,22219.1.1,4411.1.1] f(f(x,x),f(x,y))=f(f(z,x),f(x,x)). Search stopped by max_seconds option. ============ end of search ============ -------------- statistics ------------- clauses given 151 clauses generated 162416 para_from generated 89865 para_into generated 72551 demod & eval rewrites 270 clauses wt,lit,sk delete 119582 tautologies deleted 0 clauses forward subsumed 14644 (subsumed by sos) 10850 unit deletions 0 factor simplifications 0 clauses kept 28190 new demodulators 0 empty clauses 1 clauses back demodulated 0 clauses back subsumed 6669 usable size 98 sos size 21425 demodulators size 10 passive size 1 hot size 0 Kbytes malloced 23311 ----------- times (seconds) ----------- user CPU time 244.67 (0 hr, 4 min, 4 sec) system CPU time 3.12 (0 hr, 0 min, 3 sec) wall-clock time 491 (0 hr, 8 min, 11 sec) input time 0.05 clausify time 0.00 pick given time 0.43 para_into time 4.24 para_from time 5.47 pre_process time 64.05 renumber time 3.90 demod time 13.88 order equalities 6.35 unit deleletion 0.00 factor simplify 0.00 weigh cl time 6.08 hints keep time 17.44 sort lits time 0.00 forward subsume 2.72 delete cl time 4.65 keep cl time 7.94 hints time 4.02 print_cl time 0.00 conflict time 0.23 new demod time 0.00 post_process time 170.17 back demod time 0.00 back subsume 87.46 factor time 0.00 unindex time 82.66 That finishes the proof of the theorem. Process 29790 finished Tue Jul 4 18:41:24 2000