----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:34:53 2003 The command was "otter". The process ID is 26014. 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 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 0 [] f(f(x,x),f(x,y))=x. 0 [] f(x,f(x,f(x,y)))=f(x,y). 0 [] x v y=f(f(x,x),f(y,y)). 0 [] x^y=f(f(x,y),f(x,y)). 0 [] c(x)=f(x,x). end_of_list. assign(max_proofs,5). list(passive). 1 [] A v (B v C)!=B v (A v C)|$Ans(AJ). 2 [] A v (A^B)!=A|$Ans(B1). 3 [] A^B!=c(c(A) v c(B))|$Ans(DM). 4 [] A v c(A v c(A v B))!=A v B|$Ans(OM_rewritten). 5 [] f(A,B)!=c(A) v c(B)|$Ans(DEF_SS). 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=19): 7 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). ** KEPT (pick-wt=9): 8 [] f(f(x,x),f(x,y))=x. ---> New Demodulator: 9 [new_demod,8] f(f(x,x),f(x,y))=x. ** KEPT (pick-wt=11): 10 [] f(x,f(x,f(x,y)))=f(x,y). ---> New Demodulator: 11 [new_demod,10] f(x,f(x,f(x,y)))=f(x,y). ** KEPT (pick-wt=11): 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. ---> New Demodulator: 14 [new_demod,13] f(f(x,x),f(y,y))=x v y. ** KEPT (pick-wt=11): 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. ---> New Demodulator: 17 [new_demod,16] f(f(x,y),f(x,y))=x^y. ** KEPT (pick-wt=6): 19 [copy,18,flip.1] f(x,x)=c(x). ---> New Demodulator: 20 [new_demod,19] f(x,x)=c(x). ** KEPT (pick-wt=13): 21 [copy,7,flip.1,demod,20,20] f(x,c(f(y,z)))=f(y,c(f(x,z))). >>>> Starting back demodulation with 9. >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 17. >> back demodulating 7 with 17. >>>> Starting back demodulation with 20. >> back demodulating 16 with 20. >> back demodulating 13 with 20. >> back demodulating 8 with 20. ** KEPT (pick-wt=11): 28 [copy,21,flip.1,demod,23,23] f(x,y^z)=f(y,x^z). >>>> Starting back demodulation with 23. >> back demodulating 21 with 23. >>>> Starting back demodulation with 25. >>>> Starting back demodulation with 27. Following clause subsumed by 28 during input processing: 0 [copy,28,flip.1] f(x,y^z)=f(y,x^z). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 10 [] f(x,f(x,f(x,y)))=f(x,y). given clause #2: (wt=6) 19 [copy,18,flip.1] f(x,x)=c(x). given clause #3: (wt=8) 22 [back_demod,16,demod,20] c(f(x,y))=x^y. given clause #4: (wt=7) 31 [para_into,22,19,flip.1] x^x=c(c(x)). given clause #5: (wt=9) 24 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. given clause #6: (wt=7) 38 [para_into,24,19] c(c(x))=x v x. given clause #7: (wt=7) 41 [back_demod,31,demod,39] x^x=x v x. given clause #8: (wt=8) 26 [back_demod,8,demod,20] f(c(x),f(x,y))=x. ----> UNIT CONFLICT at 0.00 sec ----> 91 [binary,89,2] $Ans(B1). Length of proof is 13. Level of proof is 6. ---------------- PROOF ---------------- 2 [] A v (A^B)!=A|$Ans(B1). 8 [] f(f(x,x),f(x,y))=x. 12 [] x v y=f(f(x,x),f(y,y)). 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] x^y=f(f(x,y),f(x,y)). 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 22 [back_demod,16,demod,20] c(f(x,y))=x^y. 24 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. 26 [back_demod,8,demod,20] f(c(x),f(x,y))=x. 39,38 [para_into,24,19] c(c(x))=x v x. 44,43 [para_from,24,22,flip.1] c(x)^c(y)=c(x v y). 49 [para_into,38,22,flip.1] f(x,y) v f(x,y)=c(x^y). 64,63 [para_into,26,19,demod,20,39] x v x=x. 74,73 [back_demod,49,demod,64] f(x,y)=c(x^y). 78,77 [back_demod,38,demod,64] c(c(x))=x. 89 [back_demod,26,demod,74,74,44,78] x v (x^y)=x. 91 [binary,89,2] $Ans(B1). ------------ end of proof ------------- given clause #9: (wt=10) 43 [para_from,24,22,flip.1] c(x)^c(y)=c(x v y). given clause #10: (wt=5) 63 [para_into,26,19,demod,20,39] x v x=x. given clause #11: (wt=5) 75 [back_demod,41,demod,64] x^x=x. given clause #12: (wt=5) 77 [back_demod,38,demod,64] c(c(x))=x. ----> UNIT CONFLICT at 0.00 sec ----> 109 [binary,107,4] $Ans(OM_rewritten). Length of proof is 16. Level of proof is 7. ---------------- PROOF ---------------- 4 [] A v c(A v c(A v B))!=A v B|$Ans(OM_rewritten). 8 [] f(f(x,x),f(x,y))=x. 10 [] f(x,f(x,f(x,y)))=f(x,y). 12 [] x v y=f(f(x,x),f(y,y)). 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] x^y=f(f(x,y),f(x,y)). 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 22 [back_demod,16,demod,20] c(f(x,y))=x^y. 25,24 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. 26 [back_demod,8,demod,20] f(c(x),f(x,y))=x. 39,38 [para_into,24,19] c(c(x))=x v x. 44,43 [para_from,24,22,flip.1] c(x)^c(y)=c(x v y). 45 [para_from,24,10,demod,25] f(c(x),f(c(x),x v y))=x v y. 49 [para_into,38,22,flip.1] f(x,y) v f(x,y)=c(x^y). 64,63 [para_into,26,19,demod,20,39] x v x=x. 74,73 [back_demod,49,demod,64] f(x,y)=c(x^y). 78,77 [back_demod,38,demod,64] c(c(x))=x. 85 [back_demod,45,demod,74,74,44,78] x v (c(x)^ (x v y))=x v y. 104,103 [para_from,77,43] c(x)^y=c(x v c(y)). 107 [back_demod,85,demod,104] x v c(x v c(x v y))=x v y. 109 [binary,107,4] $Ans(OM_rewritten). ------------ end of proof ------------- given clause #13: (wt=8) 73 [back_demod,49,demod,64] f(x,y)=c(x^y). given clause #14: (wt=7) 89 [back_demod,26,demod,74,74,44,78] x v (x^y)=x. given clause #15: (wt=9) 96 [back_demod,65,demod,74] c(x^ (x v y))=c(x). given clause #16: (wt=7) 110 [para_from,96,77,demod,78,flip.1] x^ (x v y)=x. given clause #17: (wt=12) 98 [back_demod,33,demod,74,74,95] x^ (c(x) v (x^y))=x^y. given clause #18: (wt=8) 112 [para_into,98,110,demod,111] x^ (c(x) v x)=x. given clause #19: (wt=10) 103 [para_from,77,43] c(x)^y=c(x v c(y)). ----> UNIT CONFLICT at 0.00 sec ----> 118 [binary,116,3] $Ans(DM). Length of proof is 12. Level of proof is 7. ---------------- PROOF ---------------- 3 [] A^B!=c(c(A) v c(B))|$Ans(DM). 8 [] f(f(x,x),f(x,y))=x. 12 [] x v y=f(f(x,x),f(y,y)). 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] x^y=f(f(x,y),f(x,y)). 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 22 [back_demod,16,demod,20] c(f(x,y))=x^y. 24 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. 26 [back_demod,8,demod,20] f(c(x),f(x,y))=x. 39,38 [para_into,24,19] c(c(x))=x v x. 43 [para_from,24,22,flip.1] c(x)^c(y)=c(x v y). 64,63 [para_into,26,19,demod,20,39] x v x=x. 77 [back_demod,38,demod,64] c(c(x))=x. 103 [para_from,77,43] c(x)^y=c(x v c(y)). 116 [para_into,103,77] x^y=c(c(x) v c(y)). 118 [binary,116,3] $Ans(DM). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.00 sec ----> 130 [binary,128,5] $Ans(DEF_SS). Length of proof is 15. Level of proof is 8. ---------------- PROOF ---------------- 5 [] f(A,B)!=c(A) v c(B)|$Ans(DEF_SS). 8 [] f(f(x,x),f(x,y))=x. 12 [] x v y=f(f(x,x),f(y,y)). 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] x^y=f(f(x,y),f(x,y)). 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 22 [back_demod,16,demod,20] c(f(x,y))=x^y. 24 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. 26 [back_demod,8,demod,20] f(c(x),f(x,y))=x. 39,38 [para_into,24,19] c(c(x))=x v x. 43 [para_from,24,22,flip.1] c(x)^c(y)=c(x v y). 49 [para_into,38,22,flip.1] f(x,y) v f(x,y)=c(x^y). 64,63 [para_into,26,19,demod,20,39] x v x=x. 73 [back_demod,49,demod,64] f(x,y)=c(x^y). 78,77 [back_demod,38,demod,64] c(c(x))=x. 103 [para_from,77,43] c(x)^y=c(x v c(y)). 117,116 [para_into,103,77] x^y=c(c(x) v c(y)). 128 [back_demod,73,demod,117,78] f(x,y)=c(x) v c(y). 130 [binary,128,5] $Ans(DEF_SS). ------------ end of proof ------------- given clause #20: (wt=9) 128 [back_demod,73,demod,117,78] f(x,y)=c(x) v c(y). given clause #21: (wt=13) 107 [back_demod,85,demod,104] x v c(x v c(x v y))=x v y. given clause #22: (wt=9) 131 [para_into,107,63,demod,64] x v c(x v c(x))=x. given clause #23: (wt=10) 116 [para_into,103,77] x^y=c(c(x) v c(y)). given clause #24: (wt=10) 123 [back_demod,110,demod,117] c(c(x) v c(x v y))=x. given clause #25: (wt=11) 119 [para_into,103,110,flip.1] c(x v c(c(x) v y))=c(x). given clause #26: (wt=9) 141 [para_from,119,107,demod,132,flip.1] x v c(c(x) v y)=x. given clause #27: (wt=10) 137 [para_from,123,107,demod,134,flip.1] c(x) v c(x v y)=c(x). given clause #28: (wt=11) 133 [para_into,131,77] c(x) v c(c(x) v x)=c(x). given clause #29: (wt=17) 125 [back_demod,100,demod,117,117,78,78,117,117,78,78] c(x) v (c(y) v c(z))=c(y) v (c(x) v c(z)). given clause #30: (wt=14) 152 [para_into,125,63,flip.1] c(x) v (c(y) v c(x))=c(y) v c(x). given clause #31: (wt=10) 158 [para_into,152,141,demod,78,78,138] c(x v y) v c(x)=c(x). given clause #32: (wt=9) 164 [para_into,158,158,demod,78,78,78] x v (x v y)=x v y. given clause #33: (wt=15) 143 [para_into,125,77,demod,78] x v (c(y) v c(z))=c(y) v (x v c(z)). given clause #34: (wt=9) 166 [para_into,158,77,demod,78] c(c(x) v y) v x=x. given clause #35: (wt=9) 168 [para_from,158,141,demod,78] (x v y) v x=x v y. given clause #36: (wt=11) 154 [para_into,152,77,demod,78,78] x v (c(y) v x)=c(y) v x. given clause #37: (wt=11) 160 [para_into,152,133,demod,134] c(c(x) v x) v c(x)=c(x). given clause #38: (wt=9) 185 [para_into,154,77,demod,78] x v (y v x)=y v x. given clause #39: (wt=9) 193 [para_from,185,166] c(x v c(y)) v y=y. given clause #40: (wt=9) 195 [para_from,185,141] x v c(y v c(x))=x. given clause #41: (wt=15) 170 [para_from,158,107,demod,78,159] c(x v y) v c(c(x v y) v x)=c(x). given clause #42: (wt=9) 197 [para_from,185,168,demod,186] (x v y) v y=x v y. given clause #43: (wt=10) 199 [para_from,185,158] c(x v y) v c(y)=c(y). given clause #44: (wt=10) 201 [para_from,185,137] c(x) v c(y v x)=c(x). given clause #45: (wt=13) 172 [para_into,143,77,demod,78] x v (y v c(z))=y v (x v c(z)). ----> UNIT CONFLICT at 0.01 sec ----> 210 [binary,209,1] $Ans(AJ). Length of proof is 21. Level of proof is 11. ---------------- PROOF ---------------- 1 [] A v (B v C)!=B v (A v C)|$Ans(AJ). 7 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 8 [] f(f(x,x),f(x,y))=x. 12 [] x v y=f(f(x,x),f(y,y)). 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] x^y=f(f(x,y),f(x,y)). 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 21 [copy,7,flip.1,demod,20,20] f(x,c(f(y,z)))=f(y,c(f(x,z))). 23,22 [back_demod,16,demod,20] c(f(x,y))=x^y. 24 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. 26 [back_demod,8,demod,20] f(c(x),f(x,y))=x. 28 [copy,21,flip.1,demod,23,23] f(x,y^z)=f(y,x^z). 39,38 [para_into,24,19] c(c(x))=x v x. 43 [para_from,24,22,flip.1] c(x)^c(y)=c(x v y). 49 [para_into,38,22,flip.1] f(x,y) v f(x,y)=c(x^y). 64,63 [para_into,26,19,demod,20,39] x v x=x. 74,73 [back_demod,49,demod,64] f(x,y)=c(x^y). 78,77 [back_demod,38,demod,64] c(c(x))=x. 100 [back_demod,28,demod,74,74] c(x^ (y^z))=c(y^ (x^z)). 103 [para_from,77,43] c(x)^y=c(x v c(y)). 117,116 [para_into,103,77] x^y=c(c(x) v c(y)). 125 [back_demod,100,demod,117,117,78,78,117,117,78,78] c(x) v (c(y) v c(z))=c(y) v (c(x) v c(z)). 143 [para_into,125,77,demod,78] x v (c(y) v c(z))=c(y) v (x v c(z)). 172 [para_into,143,77,demod,78] x v (y v c(z))=y v (x v c(z)). 209 [para_into,172,77,demod,78] x v (y v z)=y v (x v z). 210 [binary,209,1] $Ans(AJ). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 45 clauses generated 495 clauses kept 106 clauses forward subsumed 483 clauses back subsumed 4 Kbytes malloced 319 ----------- times (seconds) ----------- user CPU time 0.01 (0 hr, 0 min, 0 sec) system CPU time 0.02 (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.00 back_sub time 0.00 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 26014 finished Fri Sep 12 16:34:53 2003