----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:35:17 2003 The command was "otter". The process ID is 26032. include("ortholattice-header"). ------- start included file ortholattice-header------- op(400,infix,^). op(400,infix,v). lex([A,B,C,D,0,1,x v x,c(x),x^x,f(x,x)]). 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). assign(pick_given_ratio,3). assign(max_weight,25). clear(detailed_history). assign(max_seconds,60). assign(max_mem,100000). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). clear(print_kept). assign(stats_level,1). list(usable). 0 [] x=x. end_of_list. ------- end included file ortholattice-header------- list(sos). 0 [] x v (y v z)=y v (x v z). 0 [] x^y=c(c(x) v c(y)). 0 [] x v c(x)=y v c(y). 0 [] (x v c(y))^ (x v y)=x. 0 [] f(x,y)=c(x) v c(y). 0 [] x v (x^y)=x. 0 [] c(c(x))=x. end_of_list. lex([D,C,B,A,0,1,f(x,x),x v x,c(x),x^x]). assign(max_proofs,5). list(passive). 1 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C)))|$Ans(A_SS). 2 [] f(f(A,f(B,B)),f(A,B))!=A|$Ans(CUT_SS). 3 [] A v B!=f(f(A,A),f(B,B))|$Ans(DEF_J). 4 [] A^B!=f(f(A,B),f(A,B))|$Ans(DEF_M). 5 [] c(A)!=f(A,A)|$Ans(DEF_C). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 6 [] x=x. Following clause subsumed by 6 during input processing: 0 [copy,6,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=11): 7 [] x v (y v z)=y v (x v z). ** KEPT (pick-wt=10): 8 [] x^y=c(c(x) v c(y)). ---> New Demodulator: 9 [new_demod,8] x^y=c(c(x) v c(y)). ** KEPT (pick-wt=9): 10 [] x v c(x)=y v c(y). ** KEPT (pick-wt=13): 12 [copy,11,demod,9] c(c(x v c(y)) v c(x v y))=x. ---> New Demodulator: 13 [new_demod,12] c(c(x v c(y)) v c(x v y))=x. ** KEPT (pick-wt=9): 15 [copy,14,flip.1] c(x) v c(y)=f(x,y). ---> New Demodulator: 16 [new_demod,15] c(x) v c(y)=f(x,y). ** KEPT (pick-wt=8): 18 [copy,17,demod,9,16] x v c(f(x,y))=x. ---> New Demodulator: 19 [new_demod,18] x v c(f(x,y))=x. ** KEPT (pick-wt=5): 20 [] c(c(x))=x. ---> New Demodulator: 21 [new_demod,20] c(c(x))=x. Following clause subsumed by 7 during input processing: 0 [copy,7,flip.1] x v (y v z)=y v (x v z). >>>> Starting back demodulation with 9. Following clause subsumed by 10 during input processing: 0 [copy,10,flip.1] x v c(x)=y v c(y). >>>> Starting back demodulation with 13. >>>> Starting back demodulation with 16. >> back demodulating 12 with 16. >> back demodulating 8 with 16. >>>> Starting back demodulation with 19. >>>> Starting back demodulation with 21. >>>> Starting back demodulation with 23. >>>> Starting back demodulation with 25. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 7 [] x v (y v z)=y v (x v z). given clause #2: (wt=5) 20 [] c(c(x))=x. given clause #3: (wt=8) 18 [copy,17,demod,9,16] x v c(f(x,y))=x. given clause #4: (wt=8) 24 [back_demod,8,demod,16] x^y=c(f(x,y)). given clause #5: (wt=9) 10 [] x v c(x)=y v c(y). given clause #6: (wt=9) 15 [copy,14,flip.1] c(x) v c(y)=f(x,y). given clause #7: (wt=9) 30 [para_into,10,20] c(x) v x=y v c(y). given clause #8: (wt=9) 31 [copy,30,flip.1] x v c(x)=c(y) v y. given clause #9: (wt=11) 22 [back_demod,12,demod,16] c(f(x v c(y),x v y))=x. given clause #10: (wt=9) 34 [para_into,15,20] x v c(y)=f(c(x),y). given clause #11: (wt=8) 96 [para_into,34,18,flip.1] f(c(x),f(x,y))=x. ----> UNIT CONFLICT at 0.01 sec ----> 111 [binary,109,5] $Ans(DEF_C). Length of proof is 5. Level of proof is 4. ---------------- PROOF ---------------- 5 [] c(A)!=f(A,A)|$Ans(DEF_C). 9,8 [] x^y=c(c(x) v c(y)). 14 [] f(x,y)=c(x) v c(y). 16,15 [copy,14,flip.1] c(x) v c(y)=f(x,y). 17 [] x v (x^y)=x. 18 [copy,17,demod,9,16] x v c(f(x,y))=x. 21,20 [] c(c(x))=x. 34 [para_into,15,20] x v c(y)=f(c(x),y). 96 [para_into,34,18,flip.1] f(c(x),f(x,y))=x. 109 [para_into,96,96,demod,21,flip.1] c(x)=f(x,x). 111 [binary,109,5] $Ans(DEF_C). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 123 [binary,121,3] $Ans(DEF_J). Length of proof is 8. Level of proof is 5. ---------------- PROOF ---------------- 3 [] A v B!=f(f(A,A),f(B,B))|$Ans(DEF_J). 9,8 [] x^y=c(c(x) v c(y)). 14 [] f(x,y)=c(x) v c(y). 16,15 [copy,14,flip.1] c(x) v c(y)=f(x,y). 17 [] x v (x^y)=x. 18 [copy,17,demod,9,16] x v c(f(x,y))=x. 21,20 [] c(c(x))=x. 34 [para_into,15,20] x v c(y)=f(c(x),y). 94 [para_into,34,20] x v y=f(c(x),c(y)). 96 [para_into,34,18,flip.1] f(c(x),f(x,y))=x. 99 [copy,94,flip.1] f(c(x),c(y))=x v y. 110,109 [para_into,96,96,demod,21,flip.1] c(x)=f(x,x). 121 [back_demod,99,demod,110,110,flip.1] x v y=f(f(x,x),f(y,y)). 123 [binary,121,3] $Ans(DEF_J). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 156 [binary,154,4] $Ans(DEF_M). Length of proof is 7. Level of proof is 5. ---------------- PROOF ---------------- 4 [] A^B!=f(f(A,B),f(A,B))|$Ans(DEF_M). 9,8 [] x^y=c(c(x) v c(y)). 14 [] f(x,y)=c(x) v c(y). 16,15 [copy,14,flip.1] c(x) v c(y)=f(x,y). 17 [] x v (x^y)=x. 18 [copy,17,demod,9,16] x v c(f(x,y))=x. 21,20 [] c(c(x))=x. 24 [back_demod,8,demod,16] x^y=c(f(x,y)). 34 [para_into,15,20] x v c(y)=f(c(x),y). 96 [para_into,34,18,flip.1] f(c(x),f(x,y))=x. 110,109 [para_into,96,96,demod,21,flip.1] c(x)=f(x,x). 154 [back_demod,24,demod,110] x^y=f(f(x,y),f(x,y)). 156 [binary,154,4] $Ans(DEF_M). ------------ end of proof ------------- given clause #12: (wt=6) 109 [para_into,96,96,demod,21,flip.1] c(x)=f(x,x). given clause #13: (wt=11) 121 [back_demod,99,demod,110,110,flip.1] x v y=f(f(x,x),f(y,y)). given clause #14: (wt=9) 124 [back_demod,96,demod,110] f(f(x,x),f(x,y))=x. given clause #15: (wt=11) 126 [back_demod,95,demod,110,122,125,110] f(x,f(x,x))=f(f(y,y),y). given clause #16: (wt=11) 133 [back_demod,89,demod,110,122,125,110,122,125,122,132,122,125] f(f(x,x),x)=f(f(y,y),y). given clause #17: (wt=17) 131 [back_demod,90,demod,110,122,125,122,110] f(f(f(x,x),y),f(f(x,x),f(y,y)))=f(x,x). given clause #18: (wt=11) 134 [back_demod,88,demod,110,122,125,110,122,125,122,132,122,125] f(x,f(x,x))=f(y,f(y,y)). given clause #19: (wt=11) 151 [back_demod,38,demod,110,122,125,110] f(f(x,x),x)=f(y,f(y,y)). given clause #20: (wt=11) 152 [back_demod,36,demod,110,110] f(x,f(f(x,x),y))=f(x,x). given clause #21: (wt=21) 135 [back_demod,79,demod,110,122,125,122,110,122,125] f(f(f(f(x,x),y),f(f(x,x),y)),f(x,x))=f(f(x,x),y). given clause #22: (wt=11) 154 [back_demod,24,demod,110] x^y=f(f(x,y),f(x,y)). given clause #23: (wt=11) 157 [para_from,126,124] f(f(x,x),f(f(y,y),y))=x. given clause #24: (wt=11) 159 [para_from,133,124,demod,125] f(x,f(f(y,y),y))=f(x,x). given clause #25: (wt=17) 137 [back_demod,75,demod,122,125,110,122,125,110] f(f(x,f(f(y,y),y)),f(x,f(f(y,y),y)))=x. given clause #26: (wt=11) 160 [copy,159,flip.1] f(x,x)=f(x,f(f(y,y),y)). given clause #27: (wt=11) 161 [para_into,131,124,demod,125,125] f(f(x,y),f(x,f(y,y)))=x. ----> UNIT CONFLICT at 0.02 sec ----> 223 [binary,221,2] $Ans(CUT_SS). Length of proof is 16. Level of proof is 8. ---------------- PROOF ---------------- 2 [] f(f(A,f(B,B)),f(A,B))!=A|$Ans(CUT_SS). 9,8 [] x^y=c(c(x) v c(y)). 11 [] (x v c(y))^ (x v y)=x. 12 [copy,11,demod,9] c(c(x v c(y)) v c(x v y))=x. 14 [] f(x,y)=c(x) v c(y). 16,15 [copy,14,flip.1] c(x) v c(y)=f(x,y). 17 [] x v (x^y)=x. 18 [copy,17,demod,9,16] x v c(f(x,y))=x. 21,20 [] c(c(x))=x. 22 [back_demod,12,demod,16] c(f(x v c(y),x v y))=x. 34 [para_into,15,20] x v c(y)=f(c(x),y). 84 [para_from,22,20] c(x)=f(x v c(y),x v y). 90 [copy,84,flip.1] f(x v c(y),x v y)=c(x). 94 [para_into,34,20] x v y=f(c(x),c(y)). 96 [para_into,34,18,flip.1] f(c(x),f(x,y))=x. 99 [copy,94,flip.1] f(c(x),c(y))=x v y. 110,109 [para_into,96,96,demod,21,flip.1] c(x)=f(x,x). 122,121 [back_demod,99,demod,110,110,flip.1] x v y=f(f(x,x),f(y,y)). 125,124 [back_demod,96,demod,110] f(f(x,x),f(x,y))=x. 131 [back_demod,90,demod,110,122,125,122,110] f(f(f(x,x),y),f(f(x,x),f(y,y)))=f(x,x). 161 [para_into,131,124,demod,125,125] f(f(x,y),f(x,f(y,y)))=x. 221 [para_into,161,124] f(f(x,f(y,y)),f(x,y))=x. 223 [binary,221,2] $Ans(CUT_SS). ------------ end of proof ------------- given clause #28: (wt=11) 163 [para_into,131,133,demod,125] f(f(f(x,x),x),y)=f(y,y). given clause #29: (wt=17) 141 [back_demod,67,demod,122,125,110,122,125,110] f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y))))=x. given clause #30: (wt=11) 166 [copy,163,flip.1] f(x,x)=f(f(f(y,y),y),x). given clause #31: (wt=11) 167 [para_from,134,124] f(f(x,x),f(y,f(y,y)))=x. given clause #32: (wt=11) 169 [para_from,151,124,demod,125] f(x,f(y,f(y,y)))=f(x,x). given clause #33: (wt=17) 145 [back_demod,61,demod,110,122,125,122,125,110] f(f(f(f(x,x),x),y),f(f(f(x,x),x),y))=y. given clause #34: (wt=11) 170 [copy,169,flip.1] f(x,x)=f(x,f(y,f(y,y))). given clause #35: (wt=11) 214 [para_into,161,151,demod,125] f(f(x,f(x,x)),y)=f(y,y). given clause #36: (wt=11) 215 [para_into,161,134,demod,125] f(f(x,f(x,x)),f(y,y))=y. given clause #37: (wt=17) 147 [back_demod,59,demod,110,122,125,122,125,110] f(f(f(x,f(x,x)),y),f(f(x,f(x,x)),y))=y. given clause #38: (wt=11) 217 [para_into,161,126,demod,125] f(f(f(x,x),x),f(y,y))=y. given clause #39: (wt=11) 221 [para_into,161,124] f(f(x,f(y,y)),f(x,y))=x. given clause #40: (wt=11) 224 [copy,214,flip.1] f(x,x)=f(f(y,f(y,y)),x). given clause #41: (wt=25) 149 [back_demod,43,demod,110,110,122,125,122,125,122] f(x,f(f(f(y,y),z),f(f(y,y),z)))=f(f(y,y),f(f(x,z),f(x,z))). ----> UNIT CONFLICT at 0.04 sec ----> 425 [binary,424,1] $Ans(A_SS). Length of proof is 13. Level of proof is 7. ---------------- PROOF ---------------- 1 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C)))|$Ans(A_SS). 7 [] x v (y v z)=y v (x v z). 9,8 [] x^y=c(c(x) v c(y)). 14 [] f(x,y)=c(x) v c(y). 16,15 [copy,14,flip.1] c(x) v c(y)=f(x,y). 17 [] x v (x^y)=x. 18 [copy,17,demod,9,16] x v c(f(x,y))=x. 21,20 [] c(c(x))=x. 34 [para_into,15,20] x v c(y)=f(c(x),y). 42 [para_from,15,7] x v f(y,z)=c(y) v (x v c(z)). 43 [copy,42,flip.1] c(x) v (y v c(z))=y v f(x,z). 94 [para_into,34,20] x v y=f(c(x),c(y)). 96 [para_into,34,18,flip.1] f(c(x),f(x,y))=x. 99 [copy,94,flip.1] f(c(x),c(y))=x v y. 110,109 [para_into,96,96,demod,21,flip.1] c(x)=f(x,x). 122,121 [back_demod,99,demod,110,110,flip.1] x v y=f(f(x,x),f(y,y)). 125,124 [back_demod,96,demod,110] f(f(x,x),f(x,y))=x. 149 [back_demod,43,demod,110,110,122,125,122,125,122] f(x,f(f(f(y,y),z),f(f(y,y),z)))=f(f(y,y),f(f(x,z),f(x,z))). 424 [para_into,149,124,demod,125,125] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 425 [binary,424,1] $Ans(A_SS). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 41 clauses generated 854 clauses kept 270 clauses forward subsumed 786 clauses back subsumed 2 Kbytes malloced 479 ----------- times (seconds) ----------- user CPU time 0.04 (0 hr, 0 min, 0 sec) system CPU time 0.01 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) para_into time 0.00 para_from time 0.00 for_sub time 0.02 back_sub time 0.00 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 26032 finished Fri Sep 12 16:35:17 2003