----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Wed Aug 6 14:26:25 2003 The command was "../../bin/otter". The process ID is 5977. set(knuth_bendix). dependent: set(anl_eq). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(process_input). dependent: set(lrpo). clear(eq_units_both_ways). WARNING: set(index_for_back_demod) flag already set. set(index_for_back_demod). set(dynamic_demod_lex_dep). WARNING: set(lrpo) flag already set. set(lrpo). WARNING: set(process_input) flag already set. set(process_input). set(display_terms). clear(print_kept). clear(print_new_demod). clear(print_back_demod). assign(max_weight,20). assign(max_mem,8000). lex($cons(A,$cons(B,$cons(C,$cons(D,$cons(E,$cons(F,$cons(g(x),$cons(n(x),$cons(+(x,x),$nil)))))))))). weight_list(pick_and_purge). weight(EQ(+(C,C),C),2). weight(EQ(+(C,+(C,x)),+(C,x)),2). weight(EQ(+(C,+(x,C)),+(C,x)),2). weight(EQ(+(C,+(x,+(y,C))),+(C,+(x,y))),2). weight(EQ(+(C,+(x,+(C,y))),+(C,+(x,y))),2). weight(EQ(n(+(n(+(C,x)),n(+(C,n(+(x,C)))))),C),2). weight(EQ(n(+(n(+(C,x)),n(+(C,n(+(C,x)))))),C),2). weight(EQ(n(+(n(C),n(+(C,n(C))))),C),2). weight(EQ(n(+(n(+(x,y)),n(+(y,n(x))))),y),2). weight(EQ(n(+(n(+(x,y)),n(+(n(y),x)))),x),2). weight(EQ(n(+(C,n(+(n(C),+(C,n(C)))))),n(C)),2). weight(EQ(+(C,+(x,y)),+(C,+(y,x))),2). weight(EQ(n(+(n(+(C,+(x,y))),n(+(C,n(+(y,x)))))),C),2). weight(EQ(n(+(n(+(C,x)),n(+(n(C),+(x,C))))),+(x,C)),2). weight(EQ(n(+(n(+(x,+(y,z))),n(+(z,n(+(x,y)))))),z),2). weight(EQ(n(+(n(+(x,y)),n(+(n(x),y)))),y),2). weight(EQ(n(+(n(+(x,n(y))),n(+(y,x)))),x),2). weight(EQ(n(+(n(+(n(x),y)),n(+(y,x)))),y),2). weight(EQ(n(+(n(+(x,+(y,z))),n(+(n(+(x,y)),z)))),z),2). weight(EQ(n(+(n(+(x,C)),n(+(C,n(+(C,x)))))),C),2). weight(EQ(n(+(C,n(+(C,+(n(+(C,x)),n(+(x,C))))))),n(+(x,C))),2). weight(EQ(n(+(n(C),n(+(C,+(n(C),n(+(C,n(C)))))))),C),2). weight(EQ(n(+(n(+(x,+(y,z))),n(+(y,n(+(x,z)))))),y),2). weight(EQ(n(+(n(C),n(+(n(C),+(C,n(C)))))),C),2). weight(EQ(n(+(n(C),+(C,n(C)))),n(+(C,n(C)))),2). weight(EQ(n(+(C,n(+(C,n(C))))),n(C)),2). weight(EQ(n(+(n(+(x,+(y,z))),n(+(n(+(x,z)),y)))),y),2). weight(EQ(n(+(x,C)),n(+(C,x))),2). weight(EQ(n(+(x,+(y,C))),n(+(C,+(x,y)))),2). weight(EQ(n(+(n(+(C,x)),n(+(C,+(n(C),x))))),+(x,C)),2). weight(EQ(n(+(n(+(C,x)),n(+(n(C),+(x,n(+(C,n(C)))))))),x),2). weight(EQ(+(C,n(+(C,n(C)))),C),2). weight(EQ(+(C,+(x,n(+(C,n(C))))),+(C,x)),2). weight(EQ(+(x,n(+(C,n(C)))),x),2). weight(EQ(+(n(+(C,n(C))),x),x),2). weight(EQ(n(+(n(x),n(+(C,+(x,n(C)))))),x),2). weight(EQ(n(+(n(x),n(n(x)))),n(+(C,n(C)))),2). weight(EQ(n(+(x,n(x))),n(+(C,n(C)))),2). weight(EQ(n(n(+(x,n(n(x))))),n(n(x))),2). weight(EQ(n(n(x)),x),2). weight(EQ(+(n(+(y,x)),n(+(n(y),x))),n(x)),2). end_of_list. list(usable). 0 [] EQ(x,x). 0 [] EQ(+(x,y),+(y,x)). 0 [] EQ(+(+(x,y),z),+(x,+(y,z))). end_of_list. list(sos). 0 [] EQ(n(+(n(+(x,y)),n(+(x,n(y))))),x). 0 [] EQ(+(C,C),C). 0 [] -(EQ(+(n(+(A,n(B))),n(+(n(A),n(B)))),B)). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 1 [] EQ(x,x). ** KEPT (pick-wt=7): 2 [] EQ(+(x,y),+(y,x)). ---> New Demodulator: (lex-dependent) 3 [new_demod,2] EQ(+(x,y),+(y,x)). ** KEPT (pick-wt=11): 4 [] EQ(+(+(x,y),z),+(x,+(y,z))). ---> New Demodulator: 5 [new_demod,4] EQ(+(+(x,y),z),+(x,+(y,z))). >>>> Starting back demodulation with 3. >>>> Starting back demodulation with 5. ------------> process sos: ** KEPT (pick-wt=2): 6 [] EQ(n(+(n(+(x,y)),n(+(x,n(y))))),x). ---> New Demodulator: 7 [new_demod,6] EQ(n(+(n(+(x,y)),n(+(x,n(y))))),x). ** KEPT (pick-wt=2): 8 [] EQ(+(C,C),C). ---> New Demodulator: 9 [new_demod,8] EQ(+(C,C),C). ** KEPT (pick-wt=14): 10 [] -(EQ(+(n(+(A,n(B))),n(+(n(A),n(B)))),B)). >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 9. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=2) 6 [] EQ(n(+(n(+(x,y)),n(+(x,n(y))))),x). given clause #2: (wt=2) 8 [] EQ(+(C,C),C). given clause #3: (wt=2) 13 [para_into,6.1.1.1.1.1,2.1.1] EQ(n(+(n(+(x,y)),n(+(y,n(x))))),y). given clause #4: (wt=2) 17 [para_into,6.1.1.1.2.1,2.1.1] EQ(n(+(n(+(x,y)),n(+(n(y),x)))),x). given clause #5: (wt=2) 21 [para_from,8.1.1,6.1.1.1.1.1] EQ(n(+(n(C),n(+(C,n(C))))),C). given clause #6: (wt=2) 23 [para_from,8.1.1,4.1.1.1,flip.1] EQ(+(C,+(C,x)),+(C,x)). given clause #7: (wt=2) 25 [para_into,13.1.1.1.1.1,4.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(z,n(+(x,y)))))),z). given clause #8: (wt=2) 29 [para_into,13.1.1.1.2.1,2.1.1] EQ(n(+(n(+(x,y)),n(+(n(x),y)))),y). given clause #9: (wt=2) 33 [para_into,13.1.1.1,2.1.1] EQ(n(+(n(+(x,n(y))),n(+(y,x)))),x). given clause #10: (wt=2) 51 [para_into,17.1.1.1,2.1.1] EQ(n(+(n(+(n(x),y)),n(+(y,x)))),y). given clause #11: (wt=2) 61 [para_from,21.1.1,13.1.1.1.2,demod,3,3] EQ(n(+(C,n(+(n(C),+(C,n(C)))))),n(C)). given clause #12: (wt=2) 73 [para_into,23.1.1.2,2.1.1] EQ(+(C,+(x,C)),+(C,x)). given clause #13: (wt=2) 75 [para_from,23.1.1,17.1.1.1.1.1,demod,3] EQ(n(+(n(+(C,x)),n(+(C,n(+(C,x)))))),C). given clause #14: (wt=2) 81 [para_into,25.1.1.1.1.1.2,2.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(y,n(+(x,z)))))),y). given clause #15: (wt=2) 83 [para_into,25.1.1.1.1.1,2.1.1,demod,5] EQ(n(+(n(+(x,+(y,z))),n(+(y,n(+(z,x)))))),y). given clause #16: (wt=2) 85 [para_into,25.1.1.1.2.1.2.1,2.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(z,n(+(y,x)))))),z). given clause #17: (wt=2) 87 [para_into,25.1.1.1.2.1,2.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(n(+(x,y)),z)))),z). given clause #18: (wt=2) 123 [para_from,61.1.1,29.1.1.1.1,demod,120,3,flip.1] EQ(n(+(n(C),+(C,n(C)))),n(+(C,n(C)))). given clause #19: (wt=2) 129 [back_demod,61,demod,124] EQ(n(+(C,n(+(C,n(C))))),n(C)). given clause #20: (wt=2) 131 [para_into,73.1.1.2,4.1.1] EQ(+(C,+(x,+(y,C))),+(C,+(x,y))). given clause #21: (wt=2) 133 [para_from,73.1.1,51.1.1.1.2.1,demod,3,3] EQ(n(+(n(+(C,x)),n(+(C,n(+(x,C)))))),C). given clause #22: (wt=2) 135 [para_from,73.1.1,33.1.1.1.2.1,demod,3,3] EQ(n(+(n(+(C,x)),n(+(n(C),+(x,C))))),+(x,C)). given clause #23: (wt=2) 139 [para_from,73.1.1,4.1.1.1,demod,5,5,flip.1] EQ(+(C,+(x,+(C,y))),+(C,+(x,y))). given clause #24: (wt=2) 143 [para_into,75.1.1.1.1.1,2.1.1] EQ(n(+(n(+(x,C)),n(+(C,n(+(C,x)))))),C). given clause #25: (wt=2) 153 [para_into,81.1.1.1.1.1,2.1.1,demod,5] EQ(n(+(n(+(x,+(y,z))),n(+(x,n(+(z,y)))))),x). given clause #26: (wt=2) 157 [para_into,81.1.1.1.2.1,2.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(n(+(x,z)),y)))),y). given clause #27: (wt=2) 167 [para_into,83.1.1.1.2.1,2.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(n(+(z,x)),y)))),y). given clause #28: (wt=2) 173 [para_into,85.1.1.1.2.1,2.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(n(+(y,x)),z)))),z). given clause #29: (wt=2) 199 [para_into,131.1.1.2,2.1.1,demod,5,140] EQ(+(C,+(x,y)),+(C,+(y,x))). given clause #30: (wt=2) 227 [para_into,153.1.1.1.2.1,2.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(n(+(z,y)),x)))),x). given clause #31: (wt=2) 233 [para_into,157.1.1.1.2.1.1,21.1.1,demod,3] EQ(n(+(n(+(C,x)),n(+(n(C),+(x,n(+(C,n(C)))))))),x). given clause #32: (wt=9) 221 [para_from,143.1.1,85.1.1.1.2,demod,3,212] EQ(n(+(C,x)),n(+(x,C))). given clause #33: (wt=13) 261 [para_into,221.1.1.1,199.1.1,demod,3] EQ(n(+(C,+(x,y))),n(+(C,+(y,x)))). given clause #34: (wt=14) 10 [] -(EQ(+(n(+(A,n(B))),n(+(n(A),n(B)))),B)). given clause #35: (wt=14) 89 [para_into,25.1.1.1.2,21.1.1,demod,3] EQ(n(+(C,n(+(C,+(n(C),n(C)))))),n(C)). given clause #36: (wt=14) 267 [para_from,89.1.1,33.1.1.1.2,demod,3,142,flip.1] EQ(n(+(C,+(n(C),n(C)))),n(+(C,n(C)))). given clause #37: (wt=15) 79 [para_into,25.1.1.1.1.1.2,8.1.1] EQ(n(+(n(+(x,C)),n(+(C,n(+(x,C)))))),C). given clause #38: (wt=15) 127 [para_from,61.1.1,17.1.1.1.1,demod,124,3] EQ(n(+(n(C),n(+(C,n(n(+(C,n(C)))))))),C). given clause #39: (wt=15) 219 [para_into,143.1.1.1,2.1.1] EQ(n(+(n(+(C,n(+(C,x)))),n(+(x,C)))),C). given clause #40: (wt=15) 247 [para_into,199.1.1.2,4.1.1] EQ(+(C,+(x,+(y,z))),+(C,+(z,+(x,y)))). given clause #41: (wt=15) 249 [para_from,199.1.1,139.1.1.2.2,demod,140] EQ(+(C,+(x,+(y,z))),+(C,+(x,+(z,y)))). given clause #42: (wt=15) 255 [para_from,199.1.1,4.1.1.1,demod,5,5,5] EQ(+(C,+(x,+(y,z))),+(C,+(y,+(x,z)))). given clause #43: (wt=15) 283 [para_into,247.1.1.2.2,199.1.1,demod,140,5,198] EQ(+(C,+(x,+(y,z))),+(C,+(z,+(y,x)))). given clause #44: (wt=15) 285 [para_into,247.1.1.2.2,139.1.1,demod,140,5,5,132,140] EQ(+(C,+(x,+(y,z))),+(C,+(y,+(z,x)))). given clause #45: (wt=16) 69 [para_from,21.1.1,17.1.1.1.1,demod,3] EQ(n(+(C,n(+(n(C),n(n(+(C,n(C)))))))),n(C)). given clause #46: (wt=17) 77 [para_from,23.1.1,13.1.1.1.1.1,demod,3] EQ(n(+(n(+(C,x)),n(+(n(C),+(C,x))))),+(C,x)). given clause #47: (wt=2) 337 [para_into,77.1.1.1.1,129.1.1,demod,260,flip.1] EQ(+(C,n(+(C,n(C)))),C). given clause #48: (wt=2) 339 [para_from,337.1.1,139.1.1.2.2,demod,74,flip.1] EQ(+(C,+(x,n(+(C,n(C))))),+(C,x)). given clause #49: (wt=2) 351 [para_from,339.1.1,33.1.1.1.2.1,demod,3,3,234,flip.1] EQ(+(x,n(+(C,n(C)))),x). given clause #50: (wt=2) 365 [para_into,351.1.1,2.1.1] EQ(+(n(+(C,n(C))),x),x). given clause #51: (wt=2) 379 [para_from,351.1.1,81.1.1.1.2.1,demod,3] EQ(n(+(n(x),n(+(C,+(x,n(C)))))),x). given clause #52: (wt=2) 385 [para_from,351.1.1,33.1.1.1.2.1,demod,366,3] EQ(n(+(n(x),n(n(x)))),n(+(C,n(C)))). given clause #53: (wt=2) 403 [para_into,385.1.1.1.1,379.1.1,demod,380] EQ(n(+(x,n(x))),n(+(C,n(C)))). given clause #54: (wt=2) 451 [para_from,403.1.1,51.1.1.1.1,demod,3,366,448,flip.1] EQ(n(n(x)),x). -------- PROOF -------- ----> UNIT CONFLICT at 0.15 sec ----> 519 [binary,518.1,1.1] $F. Length of proof is 30. Level of proof is 16. ---------------- PROOF ---------------- 1 [] EQ(x,x). 3,2 [] EQ(+(x,y),+(y,x)). 5,4 [] EQ(+(+(x,y),z),+(x,+(y,z))). 6 [] EQ(n(+(n(+(x,y)),n(+(x,n(y))))),x). 8 [] EQ(+(C,C),C). 10 [] -(EQ(+(n(+(A,n(B))),n(+(n(A),n(B)))),B)). 13 [para_into,6.1.1.1.1.1,2.1.1] EQ(n(+(n(+(x,y)),n(+(y,n(x))))),y). 17 [para_into,6.1.1.1.2.1,2.1.1] EQ(n(+(n(+(x,y)),n(+(n(y),x)))),x). 21 [para_from,8.1.1,6.1.1.1.1.1] EQ(n(+(n(C),n(+(C,n(C))))),C). 24,23 [para_from,8.1.1,4.1.1.1,flip.1] EQ(+(C,+(C,x)),+(C,x)). 25 [para_into,13.1.1.1.1.1,4.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(z,n(+(x,y)))))),z). 29 [para_into,13.1.1.1.2.1,2.1.1] EQ(n(+(n(+(x,y)),n(+(n(x),y)))),y). 33 [para_into,13.1.1.1,2.1.1] EQ(n(+(n(+(x,n(y))),n(+(y,x)))),x). 51 [para_into,17.1.1.1,2.1.1] EQ(n(+(n(+(n(x),y)),n(+(y,x)))),y). 61 [para_from,21.1.1,13.1.1.1.2,demod,3,3] EQ(n(+(C,n(+(n(C),+(C,n(C)))))),n(C)). 74,73 [para_into,23.1.1.2,2.1.1] EQ(+(C,+(x,C)),+(C,x)). 77 [para_from,23.1.1,13.1.1.1.1.1,demod,3] EQ(n(+(n(+(C,x)),n(+(n(C),+(C,x))))),+(C,x)). 81 [para_into,25.1.1.1.1.1.2,2.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(y,n(+(x,z)))))),y). 120,119 [para_from,61.1.1,25.1.1.1.2,demod,3,24,3] EQ(n(+(n(C),n(+(n(C),+(C,n(C)))))),C). 124,123 [para_from,61.1.1,29.1.1.1.1,demod,120,3,flip.1] EQ(n(+(n(C),+(C,n(C)))),n(+(C,n(C)))). 129 [back_demod,61,demod,124] EQ(n(+(C,n(+(C,n(C))))),n(C)). 139 [para_from,73.1.1,4.1.1.1,demod,5,5,flip.1] EQ(+(C,+(x,+(C,y))),+(C,+(x,y))). 157 [para_into,81.1.1.1.2.1,2.1.1] EQ(n(+(n(+(x,+(y,z))),n(+(n(+(x,z)),y)))),y). 234,233 [para_into,157.1.1.1.2.1.1,21.1.1,demod,3] EQ(n(+(n(+(C,x)),n(+(n(C),+(x,n(+(C,n(C)))))))),x). 260,259 [para_into,233.1.1.1.1.1,8.1.1] EQ(n(+(n(C),n(+(n(C),+(C,n(+(C,n(C)))))))),C). 337 [para_into,77.1.1.1.1,129.1.1,demod,260,flip.1] EQ(+(C,n(+(C,n(C)))),C). 339 [para_from,337.1.1,139.1.1.2.2,demod,74,flip.1] EQ(+(C,+(x,n(+(C,n(C))))),+(C,x)). 352,351 [para_from,339.1.1,33.1.1.1.2.1,demod,3,3,234,flip.1] EQ(+(x,n(+(C,n(C)))),x). 366,365 [para_into,351.1.1,2.1.1] EQ(+(n(+(C,n(C))),x),x). 380,379 [para_from,351.1.1,81.1.1.1.2.1,demod,3] EQ(n(+(n(x),n(+(C,+(x,n(C)))))),x). 385 [para_from,351.1.1,33.1.1.1.2.1,demod,366,3] EQ(n(+(n(x),n(n(x)))),n(+(C,n(C)))). 403 [para_into,385.1.1.1.1,379.1.1,demod,380] EQ(n(+(x,n(x))),n(+(C,n(C)))). 448,447 [para_from,403.1.1,51.1.1.1.2,demod,3,352] EQ(n(n(+(x,n(n(x))))),x). 452,451 [para_from,403.1.1,51.1.1.1.1,demod,3,366,448,flip.1] EQ(n(n(x)),x). 509,508 [para_into,451.1.1.1,29.1.1,flip.1] EQ(+(n(+(x,y)),n(+(n(x),y))),n(y)). 518 [back_demod,10,demod,509,452] -(EQ(B,B)). 519 [binary,518.1,1.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 54 clauses generated 3114 para_from generated 1853 para_into generated 1261 demod & eval rewrites 4872 clauses wt,lit,sk delete 1340 tautologies deleted 0 clauses forward subsumed 1635 (subsumed by sos) 95 unit deletions 0 factor simplifications 0 clauses kept 261 new demodulators 257 empty clauses 1 clauses back demodulated 116 clauses back subsumed 0 usable size 23 sos size 122 demodulators size 142 passive size 0 hot size 0 Kbytes malloced 606 ----------- times (seconds) ----------- user CPU time 0.15 (0 hr, 0 min, 0 sec) system CPU time 0.05 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) input time 0.00 clausify time 0.00 process input 0.00 pick given time 0.00 para_into time 0.02 para_from time 0.00 pre_process time 0.12 renumber time 0.00 demod time 0.09 order equalities 0.00 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.00 hints keep time 0.00 sort lits time 0.00 forward subsume 0.01 delete cl time 0.00 keep cl time 0.01 hints time 0.00 print_cl time 0.00 conflict time 0.00 new demod time 0.00 post_process time 0.00 back demod time 0.00 back subsume 0.00 factor time 0.00 unindex time 0.00 That finishes the proof of the theorem. Process 5977 finished Wed Aug 6 14:26:26 2003