----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:35:11 2003 The command was "otter". The process ID is 26026. 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 v (x^y)=x. 0 [] x^y=c(c(x) v c(y)). 0 [] c(c(x))=x. 0 [] x v c(x)=y v c(y). 0 [] x v (y^ (x v z))=x v (z^ (x v y)). 0 [] f(x,y)=c(x) v c(y). end_of_list. lex([D,C,B,A,0,1,f(x,x),x v x,c(x),x^x]). assign(max_proofs,7). 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,A),f(A,B))!=A|$Ans(B_SS). 3 [] f(A,f(A,A))!=f(B,f(B,B))|$Ans(ONE_SS). 4 [] f(A,f(B,f(A,f(C,C))))!=f(A,f(C,f(A,f(B,B))))|$Ans(MOD_SS). 5 [] A v B!=f(f(A,A),f(B,B))|$Ans(DEF_J). 6 [] A^B!=f(f(A,B),f(A,B))|$Ans(DEF_M). 7 [] c(A)!=f(A,A)|$Ans(DEF_C). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 8 [] x=x. Following clause subsumed by 8 during input processing: 0 [copy,8,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=11): 9 [] x v (y v z)=y v (x v z). ** KEPT (pick-wt=7): 10 [] x v (x^y)=x. ---> New Demodulator: 11 [new_demod,10] x v (x^y)=x. ** KEPT (pick-wt=10): 12 [] x^y=c(c(x) v c(y)). ---> New Demodulator: 13 [new_demod,12] x^y=c(c(x) v c(y)). ** KEPT (pick-wt=5): 14 [] c(c(x))=x. ---> New Demodulator: 15 [new_demod,14] c(c(x))=x. ** KEPT (pick-wt=9): 16 [] x v c(x)=y v c(y). ** KEPT (pick-wt=21): 18 [copy,17,demod,13,13] x v c(c(y) v c(x v z))=x v c(c(z) v c(x v y)). ** KEPT (pick-wt=9): 20 [copy,19,flip.1] c(x) v c(y)=f(x,y). ---> New Demodulator: 21 [new_demod,20] c(x) v c(y)=f(x,y). Following clause subsumed by 9 during input processing: 0 [copy,9,flip.1] x v (y v z)=y v (x v z). >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 13. >> back demodulating 10 with 13. >>>> Starting back demodulation with 15. Following clause subsumed by 16 during input processing: 0 [copy,16,flip.1] x v c(x)=y v c(y). ** KEPT (pick-wt=17): 24 [copy,18,flip.1,demod,21,21] x v c(f(y,x v z))=x v c(f(z,x v y)). >>>> Starting back demodulation with 21. >> back demodulating 18 with 21. >> back demodulating 12 with 21. >>>> Starting back demodulation with 23. Following clause subsumed by 24 during input processing: 0 [copy,24,flip.1] x v c(f(y,x v z))=x v c(f(z,x v y)). >>>> Starting back demodulation with 26. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 9 [] x v (y v z)=y v (x v z). given clause #2: (wt=5) 14 [] c(c(x))=x. given clause #3: (wt=8) 22 [back_demod,10,demod,13,21] x v c(f(x,y))=x. given clause #4: (wt=8) 25 [back_demod,12,demod,21] x^y=c(f(x,y)). given clause #5: (wt=9) 16 [] x v c(x)=y v c(y). given clause #6: (wt=9) 20 [copy,19,flip.1] c(x) v c(y)=f(x,y). given clause #7: (wt=9) 31 [para_into,16,14] c(x) v x=y v c(y). given clause #8: (wt=9) 32 [copy,31,flip.1] x v c(x)=c(y) v y. given clause #9: (wt=17) 24 [copy,18,flip.1,demod,21,21] x v c(f(y,x v z))=x v c(f(z,x v y)). given clause #10: (wt=9) 35 [para_into,20,14] x v c(y)=f(c(x),y). given clause #11: (wt=8) 77 [para_into,35,22,flip.1] f(c(x),f(x,y))=x. ----> UNIT CONFLICT at 0.01 sec ----> 94 [binary,92,7] $Ans(DEF_C). Length of proof is 5. Level of proof is 4. ---------------- PROOF ---------------- 7 [] c(A)!=f(A,A)|$Ans(DEF_C). 10 [] x v (x^y)=x. 13,12 [] x^y=c(c(x) v c(y)). 15,14 [] c(c(x))=x. 19 [] f(x,y)=c(x) v c(y). 21,20 [copy,19,flip.1] c(x) v c(y)=f(x,y). 22 [back_demod,10,demod,13,21] x v c(f(x,y))=x. 35 [para_into,20,14] x v c(y)=f(c(x),y). 77 [para_into,35,22,flip.1] f(c(x),f(x,y))=x. 92 [para_into,77,77,demod,15,flip.1] c(x)=f(x,x). 94 [binary,92,7] $Ans(DEF_C). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 101 [binary,99,5] $Ans(DEF_J). Length of proof is 8. Level of proof is 5. ---------------- PROOF ---------------- 5 [] A v B!=f(f(A,A),f(B,B))|$Ans(DEF_J). 10 [] x v (x^y)=x. 13,12 [] x^y=c(c(x) v c(y)). 15,14 [] c(c(x))=x. 19 [] f(x,y)=c(x) v c(y). 21,20 [copy,19,flip.1] c(x) v c(y)=f(x,y). 22 [back_demod,10,demod,13,21] x v c(f(x,y))=x. 35 [para_into,20,14] x v c(y)=f(c(x),y). 73 [para_into,35,14] x v y=f(c(x),c(y)). 77 [para_into,35,22,flip.1] f(c(x),f(x,y))=x. 79 [copy,73,flip.1] f(c(x),c(y))=x v y. 93,92 [para_into,77,77,demod,15,flip.1] c(x)=f(x,x). 99 [back_demod,79,demod,93,93,flip.1] x v y=f(f(x,x),f(y,y)). 101 [binary,99,5] $Ans(DEF_J). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 104 [binary,102,2] $Ans(B_SS). Length of proof is 6. Level of proof is 5. ---------------- PROOF ---------------- 2 [] f(f(A,A),f(A,B))!=A|$Ans(B_SS). 10 [] x v (x^y)=x. 13,12 [] x^y=c(c(x) v c(y)). 15,14 [] c(c(x))=x. 19 [] f(x,y)=c(x) v c(y). 21,20 [copy,19,flip.1] c(x) v c(y)=f(x,y). 22 [back_demod,10,demod,13,21] x v c(f(x,y))=x. 35 [para_into,20,14] x v c(y)=f(c(x),y). 77 [para_into,35,22,flip.1] f(c(x),f(x,y))=x. 93,92 [para_into,77,77,demod,15,flip.1] c(x)=f(x,x). 102 [back_demod,77,demod,93] f(f(x,x),f(x,y))=x. 104 [binary,102,2] $Ans(B_SS). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 109 [binary,108,4] $Ans(MOD_SS). Length of proof is 13. Level of proof is 6. ---------------- PROOF ---------------- 4 [] f(A,f(B,f(A,f(C,C))))!=f(A,f(C,f(A,f(B,B))))|$Ans(MOD_SS). 10 [] x v (x^y)=x. 13,12 [] x^y=c(c(x) v c(y)). 15,14 [] c(c(x))=x. 17 [] x v (y^ (x v z))=x v (z^ (x v y)). 18 [copy,17,demod,13,13] x v c(c(y) v c(x v z))=x v c(c(z) v c(x v y)). 19 [] f(x,y)=c(x) v c(y). 21,20 [copy,19,flip.1] c(x) v c(y)=f(x,y). 22 [back_demod,10,demod,13,21] x v c(f(x,y))=x. 24 [copy,18,flip.1,demod,21,21] x v c(f(y,x v z))=x v c(f(z,x v y)). 35 [para_into,20,14] x v c(y)=f(c(x),y). 65 [para_into,24,20,demod,21] f(x,f(y,c(x) v z))=f(x,f(z,c(x) v y)). 73 [para_into,35,14] x v y=f(c(x),c(y)). 77 [para_into,35,22,flip.1] f(c(x),f(x,y))=x. 79 [copy,73,flip.1] f(c(x),c(y))=x v y. 93,92 [para_into,77,77,demod,15,flip.1] c(x)=f(x,x). 100,99 [back_demod,79,demod,93,93,flip.1] x v y=f(f(x,x),f(y,y)). 103,102 [back_demod,77,demod,93] f(f(x,x),f(x,y))=x. 108 [back_demod,65,demod,93,100,103,93,100,103] f(x,f(y,f(x,f(z,z))))=f(x,f(z,f(x,f(y,y)))). 109 [binary,108,4] $Ans(MOD_SS). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 113 [binary,112,3] $Ans(ONE_SS). Length of proof is 14. Level of proof is 6. ---------------- PROOF ---------------- 3 [] f(A,f(A,A))!=f(B,f(B,B))|$Ans(ONE_SS). 10 [] x v (x^y)=x. 13,12 [] x^y=c(c(x) v c(y)). 15,14 [] c(c(x))=x. 16 [] x v c(x)=y v c(y). 19 [] f(x,y)=c(x) v c(y). 21,20 [copy,19,flip.1] c(x) v c(y)=f(x,y). 22 [back_demod,10,demod,13,21] x v c(f(x,y))=x. 31 [para_into,16,14] c(x) v x=y v c(y). 32 [copy,31,flip.1] x v c(x)=c(y) v y. 35 [para_into,20,14] x v c(y)=f(c(x),y). 52 [para_into,32,20] f(x,c(x))=c(y) v y. 53 [copy,52,flip.1] c(x) v x=f(y,c(y)). 73 [para_into,35,14] x v y=f(c(x),c(y)). 77 [para_into,35,22,flip.1] f(c(x),f(x,y))=x. 79 [copy,73,flip.1] f(c(x),c(y))=x v y. 93,92 [para_into,77,77,demod,15,flip.1] c(x)=f(x,x). 100,99 [back_demod,79,demod,93,93,flip.1] x v y=f(f(x,x),f(y,y)). 103,102 [back_demod,77,demod,93] f(f(x,x),f(x,y))=x. 112 [back_demod,53,demod,93,100,103,93] f(x,f(x,x))=f(y,f(y,y)). 113 [binary,112,3] $Ans(ONE_SS). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 122 [binary,120,6] $Ans(DEF_M). Length of proof is 7. Level of proof is 5. ---------------- PROOF ---------------- 6 [] A^B!=f(f(A,B),f(A,B))|$Ans(DEF_M). 10 [] x v (x^y)=x. 13,12 [] x^y=c(c(x) v c(y)). 15,14 [] c(c(x))=x. 19 [] f(x,y)=c(x) v c(y). 21,20 [copy,19,flip.1] c(x) v c(y)=f(x,y). 22 [back_demod,10,demod,13,21] x v c(f(x,y))=x. 25 [back_demod,12,demod,21] x^y=c(f(x,y)). 35 [para_into,20,14] x v c(y)=f(c(x),y). 77 [para_into,35,22,flip.1] f(c(x),f(x,y))=x. 93,92 [para_into,77,77,demod,15,flip.1] c(x)=f(x,x). 120 [back_demod,25,demod,93] x^y=f(f(x,y),f(x,y)). 122 [binary,120,6] $Ans(DEF_M). ------------ end of proof ------------- given clause #12: (wt=6) 92 [para_into,77,77,demod,15,flip.1] c(x)=f(x,x). given clause #13: (wt=11) 99 [back_demod,79,demod,93,93,flip.1] x v y=f(f(x,x),f(y,y)). given clause #14: (wt=9) 102 [back_demod,77,demod,93] f(f(x,x),f(x,y))=x. given clause #15: (wt=11) 105 [back_demod,74,demod,93,100,103,93] f(x,f(x,x))=f(f(y,y),y). given clause #16: (wt=11) 112 [back_demod,53,demod,93,100,103,93] f(x,f(x,x))=f(y,f(y,y)). given clause #17: (wt=19) 106 [back_demod,68,demod,93,93,100,103] f(x,f(f(y,y),f(x,f(z,z))))=f(x,f(z,f(x,y))). given clause #18: (wt=11) 114 [back_demod,47,demod,93,100,103,93] f(f(x,x),x)=f(f(y,y),y). given clause #19: (wt=11) 117 [back_demod,39,demod,93,100,103,93] f(f(x,x),x)=f(y,f(y,y)). given clause #20: (wt=11) 118 [back_demod,37,demod,93,93] f(x,f(f(x,x),y))=f(x,x). given clause #21: (wt=19) 108 [back_demod,65,demod,93,100,103,93,100,103] f(x,f(y,f(x,f(z,z))))=f(x,f(z,f(x,f(y,y)))). given clause #22: (wt=9) 145 [para_into,108,106,demod,103,103,103,119,103] f(f(x,x),f(y,x))=x. given clause #23: (wt=11) 120 [back_demod,25,demod,93] x^y=f(f(x,y),f(x,y)). given clause #24: (wt=11) 123 [para_from,105,102] f(f(x,x),f(f(y,y),y))=x. given clause #25: (wt=19) 110 [back_demod,60,demod,93,93,100,103] f(x,f(y,f(x,z)))=f(x,f(f(z,z),f(x,f(y,y)))). given clause #26: (wt=11) 125 [para_from,112,102] f(f(x,x),f(y,f(y,y)))=x. given clause #27: (wt=11) 128 [para_into,106,112,demod,126,flip.1] f(x,f(x,f(x,y)))=f(x,y). given clause #28: (wt=11) 132 [para_into,106,102,flip.1] f(x,f(y,f(x,x)))=f(x,x). given clause #29: (wt=25) 115 [back_demod,44,demod,93,93,100,103,100,103,100] 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.02 sec ----> 177 [binary,176,1] $Ans(A_SS). Length of proof is 23. Level of proof is 8. ---------------- PROOF ---------------- 1 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C)))|$Ans(A_SS). 9 [] x v (y v z)=y v (x v z). 10 [] x v (x^y)=x. 13,12 [] x^y=c(c(x) v c(y)). 15,14 [] c(c(x))=x. 17 [] x v (y^ (x v z))=x v (z^ (x v y)). 18 [copy,17,demod,13,13] x v c(c(y) v c(x v z))=x v c(c(z) v c(x v y)). 19 [] f(x,y)=c(x) v c(y). 21,20 [copy,19,flip.1] c(x) v c(y)=f(x,y). 22 [back_demod,10,demod,13,21] x v c(f(x,y))=x. 24 [copy,18,flip.1,demod,21,21] x v c(f(y,x v z))=x v c(f(z,x v y)). 35 [para_into,20,14] x v c(y)=f(c(x),y). 37 [para_into,20,22,flip.1] f(x,f(c(x),y))=c(x). 43 [para_from,20,9] x v f(y,z)=c(y) v (x v c(z)). 44 [copy,43,flip.1] c(x) v (y v c(z))=y v f(x,z). 60 [para_into,24,20,demod,21,21] f(x,f(y,f(x,z)))=f(x,f(c(z),c(x) v y)). 65 [para_into,24,20,demod,21] f(x,f(y,c(x) v z))=f(x,f(z,c(x) v y)). 68 [copy,60,flip.1] f(x,f(c(y),c(x) v z))=f(x,f(z,f(x,y))). 73 [para_into,35,14] x v y=f(c(x),c(y)). 77 [para_into,35,22,flip.1] f(c(x),f(x,y))=x. 79 [copy,73,flip.1] f(c(x),c(y))=x v y. 93,92 [para_into,77,77,demod,15,flip.1] c(x)=f(x,x). 100,99 [back_demod,79,demod,93,93,flip.1] x v y=f(f(x,x),f(y,y)). 103,102 [back_demod,77,demod,93] f(f(x,x),f(x,y))=x. 106 [back_demod,68,demod,93,93,100,103] f(x,f(f(y,y),f(x,f(z,z))))=f(x,f(z,f(x,y))). 108 [back_demod,65,demod,93,100,103,93,100,103] f(x,f(y,f(x,f(z,z))))=f(x,f(z,f(x,f(y,y)))). 115 [back_demod,44,demod,93,93,100,103,100,103,100] f(x,f(f(f(y,y),z),f(f(y,y),z)))=f(f(y,y),f(f(x,z),f(x,z))). 119,118 [back_demod,37,demod,93,93] f(x,f(f(x,x),y))=f(x,x). 145 [para_into,108,106,demod,103,103,103,119,103] f(f(x,x),f(y,x))=x. 176 [para_into,115,145,demod,103,103] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 177 [binary,176,1] $Ans(A_SS). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 29 clauses generated 398 clauses kept 125 clauses forward subsumed 397 clauses back subsumed 1 Kbytes malloced 351 ----------- times (seconds) ----------- user CPU time 0.02 (0 hr, 0 min, 0 sec) system CPU time 0.00 (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 26026 finished Fri Sep 12 16:35:11 2003