----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Wed Aug 6 14:26:48 2003 The command was "../../bin/otter". The process ID is 6355. set(para_from). set(para_into). set(order_eq). set(geometric_rule). set(geometric_rewrite_before). set(lrpo). lex([A,B,C,D,E,F,e,f(x,x),g(x)]). assign(pick_given_ratio,1). assign(max_weight,17). assign(max_mem,1500). clear(print_kept). list(usable). 1 [] x=x. end_of_list. list(sos). 2 [] f(x,f(e,x))=e. end_of_list. list(passive). 3 [] f(f(A,B),f(C,D))!=f(f(A,C),f(B,D)). end_of_list. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=7) 2 [] f(x,f(e,x))=e. given clause #2: (wt=7) 5 [para_into,2.1.1.2,2.1.1] f(f(e,e),e)=e. given clause #3: (wt=11) 4 [para_into,2.1.1.2.1,2.1.2] f(x,f(f(y,f(e,y)),x))=e. given clause #4: (wt=11) 6 [para_into,2.1.2,2.1.2,gL-id] f(x,f(y,x))=f(z,f(y,z)). 30 back subsumes 13. 33 back subsumes 14. 36 back subsumes 12. given clause #5: (wt=11) 7 [para_into,5.1.1.1.1,5.1.2] f(f(f(f(e,e),e),e),e)=e. given clause #6: (wt=11) 8 [para_into,5.1.1.1.1,2.1.2] f(f(f(x,f(e,x)),e),e)=e. 55 back subsumes 42. given clause #7: (wt=11) 9 [para_into,5.1.1.1.2,5.1.2] f(f(e,f(f(e,e),e)),e)=e. 67 back subsumes 9. given clause #8: (wt=11) 10 [para_into,5.1.1.1.2,2.1.2] f(f(e,f(x,f(e,x))),e)=e. 73 back subsumes 66. given clause #9: (wt=11) 11 [para_into,5.1.1.2,5.1.2] f(f(e,e),f(f(e,e),e))=e. given clause #10: (wt=11) 15 [para_from,5.1.2,2.1.1.2.1] f(x,f(f(f(e,e),e),x))=e. 91 back subsumes 69. 94 back subsumes 50. 95 back subsumes 48. given clause #11: (wt=15) 16 [para_into,4.1.1.2.1.2.1,5.1.2] f(x,f(f(y,f(f(f(e,e),e),y)),x))=e. given clause #12: (wt=11) 29 [para_into,6.1.1.2,5.1.1,flip.1] f(x,f(f(e,e),x))=f(e,e). 99 back subsumes 98. 122 back subsumes 68. 123 back subsumes 90. 124 back subsumes 81. 125 back subsumes 39. given clause #13: (wt=15) 17 [para_into,4.1.1.2.1.2.1,2.1.2] f(x,f(f(y,f(f(z,f(e,z)),y)),x))=e. given clause #14: (wt=11) 30 [para_into,6.1.1.2,2.1.1] f(f(e,x),e)=f(y,f(x,y)). 127 back subsumes 87. 128 back subsumes 71. 130 back subsumes 85. 143 back subsumes 108. 147 back subsumes 65. 148 back subsumes 41. 149 back subsumes 88. 150 back subsumes 130. 151 back subsumes 89. 152 back subsumes 74. 153 back subsumes 11. given clause #15: (wt=15) 18 [para_into,4.1.1.2.1.2,4.1.1] f(x,f(f(f(f(y,f(e,y)),e),e),x))=e. given clause #16: (wt=11) 33 [para_into,6.1.2.2,2.1.1] f(x,f(y,x))=f(f(e,y),e). 158 back subsumes 86. 160 back subsumes 106. given clause #17: (wt=15) 19 [para_into,4.1.1.2,4.1.1] f(f(f(x,f(e,x)),f(y,f(e,y))),e)=e. given clause #18: (wt=11) 36 [para_from,6.1.1,2.1.1.2] f(f(x,e),f(y,f(x,y)))=e. 166 back subsumes 82. 169 back subsumes 51. 173 back subsumes 83. 174 back subsumes 61. 175 back subsumes 62. 177 back subsumes 105. given clause #19: (wt=15) 20 [para_into,4.1.2,5.1.2] f(x,f(f(y,f(e,y)),x))=f(f(e,e),e). given clause #20: (wt=11) 67 [para_into,9.1.1.1,6.1.2] f(f(x,f(f(e,e),x)),e)=e. 181 back subsumes 52. 182 back subsumes 63. 183 back subsumes 64. 184 back subsumes 182. 189 back subsumes 178. 189 back subsumes 176. given clause #21: (wt=15) 21 [para_into,4.1.2,2.1.2] f(x,f(f(y,f(e,y)),x))=f(z,f(e,z)). given clause #22: (wt=11) 84 [para_into,11.1.2,5.1.2,gL-id] f(x,f(f(e,e),e))=f(x,e). 199 back subsumes 197. given clause #23: (wt=15) 22 [para_from,4.1.2,5.1.2] f(f(e,e),e)=f(x,f(f(y,f(e,y)),x)). given clause #24: (wt=11) 102 [para_into,29.1.1.2,11.1.1,gL-id] f(f(f(e,e),e),x)=f(e,x). 219 back subsumes 217. 222 back subsumes 137. 223 back subsumes 135. given clause #25: (wt=15) 23 [para_from,4.1.2,2.1.2] f(x,f(e,x))=f(y,f(f(z,f(e,z)),y)). given clause #26: (wt=11) 116 [para_from,29.1.1,2.1.1.2] f(f(f(e,e),e),f(e,e))=e. given clause #27: (wt=15) 24 [para_from,4.1.2,5.1.1.2] f(f(e,e),f(x,f(f(y,f(e,y)),x)))=e. given clause #28: (wt=11) 126 [para_from,29.1.2,2.1.1.2] f(e,f(x,f(f(e,e),x)))=e. given clause #29: (wt=15) 25 [para_from,4.1.2,5.1.1.1.2] f(f(e,f(x,f(f(y,f(e,y)),x))),e)=e. given clause #30: (wt=11) 141 [para_from,30.1.1,29.1.1.2,gL-id] f(x,f(y,f(e,y)))=f(x,e). 238 back subsumes 200. 239 back subsumes 236. 240 back subsumes 201. 252 back subsumes 232. given clause #31: (wt=15) 26 [para_from,4.1.2,5.1.1.1.1] f(f(f(x,f(f(y,f(e,y)),x)),e),e)=e. given clause #32: (wt=11) 153 [para_from,30.1.2,2.1.1.2] f(f(x,e),f(f(e,x),e))=e. 266 back subsumes 205. given clause #33: (wt=15) 27 [para_into,6.1.1.2,6.1.2] f(f(x,y),f(z,f(x,z)))=f(u,f(y,u)). -------- PROOF -------- ----> UNIT CONFLICT at 0.07 sec ----> 270 [binary,269.1,3.1] $F. Length of proof is 3. Level of proof is 3. ---------------- PROOF ---------------- 2 [] f(x,f(e,x))=e. 3 [] f(f(A,B),f(C,D))!=f(f(A,C),f(B,D)). 6 [para_into,2.1.2,2.1.2,gL-id] f(x,f(y,x))=f(z,f(y,z)). 27 [para_into,6.1.1.2,6.1.2] f(f(x,y),f(z,f(x,z)))=f(u,f(y,u)). 269 [gL,27] f(f(x,y),f(z,u))=f(f(x,z),f(y,u)). 270 [binary,269.1,3.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 33 clauses generated 4623 para_from generated 2120 para_into generated 2481 gL rule generated 22 demod & eval rewrites 0 clauses wt,lit,sk delete 3053 tautologies deleted 0 clauses forward subsumed 1304 (subsumed by sos) 734 unit deletions 0 factor simplifications 0 clauses kept 266 new demodulators 0 empty clauses 1 clauses back demodulated 0 clauses back subsumed 48 usable size 32 sos size 188 demodulators size 0 passive size 1 hot size 0 Kbytes malloced 383 ----------- times (seconds) ----------- user CPU time 0.07 (0 hr, 0 min, 0 sec) system CPU time 0.04 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) input time 0.01 clausify time 0.00 pick given time 0.00 para_into time 0.00 para_from time 0.02 pre_process time 0.04 renumber time 0.01 demod time 0.00 order equalities 0.02 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.00 delete cl time 0.00 keep cl time 0.00 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 6355 finished Wed Aug 6 14:26:48 2003