----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Oct 17 13:41:56 2003 The command was "otter". The process ID is 11083. op(400,infix,^). op(400,infix,v). op(400,infix,|). lex([A,B,C,D,0,1,x v x,c(x),x^x,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). 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. assign(max_proofs,2). 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 [] x v (c(x)^ (x v y))=x v y. end_of_list. list(passive). 1 [] c(c(A))!=A. 2 [] A v c(A)!=B v c(B). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 3 [] x=x. Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=11): 4 [] x v (y v z)=y v (x v z). ** KEPT (pick-wt=7): 5 [] x v (x^y)=x. ---> New Demodulator: 6 [new_demod,5] x v (x^y)=x. ** KEPT (pick-wt=10): 7 [] x^y=c(c(x) v c(y)). ---> New Demodulator: 8 [new_demod,7] x^y=c(c(x) v c(y)). ** KEPT (pick-wt=15): 10 [copy,9,demod,8] x v c(c(c(x)) v c(x v y))=x v y. ---> New Demodulator: 11 [new_demod,10] x v c(c(c(x)) v c(x v y))=x v y. Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] x v (y v z)=y v (x v z). >>>> Starting back demodulation with 6. >>>> Starting back demodulation with 8. >> back demodulating 5 with 8. >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 13. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 4 [] x v (y v z)=y v (x v z). given clause #2: (wt=10) 7 [] x^y=c(c(x) v c(y)). given clause #3: (wt=10) 12 [back_demod,5,demod,8] x v c(c(x) v c(y))=x. given clause #4: (wt=7) 16 [para_into,12.1.1.2.1,12.1.1] x v c(c(x))=x. given clause #5: (wt=15) 10 [copy,9,demod,8] x v c(c(c(x)) v c(x v y))=x v y. given clause #6: (wt=9) 26 [para_from,10.1.1,12.1.1.2.1] x v c(c(x) v y)=x. given clause #7: (wt=11) 20 [para_from,16.1.1,4.1.1.2,flip.1] x v (y v c(c(x)))=y v x. given clause #8: (wt=9) 34 [para_from,20.1.1,26.1.1.2.1] x v c(y v c(x))=x. given clause #9: (wt=15) 14 [para_into,4.1.1.2,4.1.1] x v (y v (z v u))=z v (x v (y v u)). given clause #10: (wt=8) 44 [para_into,34.1.1.2.1,16.1.1] c(x) v c(x)=c(x). given clause #11: (wt=7) 66 [para_from,44.1.1,20.1.1.2,demod,17,flip.1] c(c(x)) v x=x. given clause #12: (wt=9) 76 [para_from,66.1.1,20.1.1.2,demod,17,flip.1] c(c(c(c(x)))) v x=x. given clause #13: (wt=15) 15 [copy,14,flip.1] x v (y v (z v u))=y v (z v (x v u)). given clause #14: (wt=7) 90 [para_from,76.1.1,26.1.1.2.1,demod,67,flip.1] c(c(c(x)))=c(x). ----> UNIT CONFLICT at 0.01 sec ----> 120 [binary,118.1,1.1] $F. Length of proof is 13. Level of proof is 10. ---------------- PROOF ---------------- 1 [] c(c(A))!=A. 4 [] x v (y v z)=y v (x v z). 5 [] x v (x^y)=x. 8,7 [] x^y=c(c(x) v c(y)). 9 [] x v (c(x)^ (x v y))=x v y. 10 [copy,9,demod,8] x v c(c(c(x)) v c(x v y))=x v y. 12 [back_demod,5,demod,8] x v c(c(x) v c(y))=x. 17,16 [para_into,12.1.1.2.1,12.1.1] x v c(c(x))=x. 20 [para_from,16.1.1,4.1.1.2,flip.1] x v (y v c(c(x)))=y v x. 26 [para_from,10.1.1,12.1.1.2.1] x v c(c(x) v y)=x. 34 [para_from,20.1.1,26.1.1.2.1] x v c(y v c(x))=x. 44 [para_into,34.1.1.2.1,16.1.1] c(x) v c(x)=c(x). 67,66 [para_from,44.1.1,20.1.1.2,demod,17,flip.1] c(c(x)) v x=x. 76 [para_from,66.1.1,20.1.1.2,demod,17,flip.1] c(c(c(c(x)))) v x=x. 91,90 [para_from,76.1.1,26.1.1.2.1,demod,67,flip.1] c(c(c(x)))=c(x). 92 [para_from,76.1.1,10.1.1.2.1.2.1,demod,91,91,91,91,67] c(c(x)) v c(c(c(x)) v c(x))=x. 115,114 [para_from,90.1.1,34.1.1.2.1.2] c(c(x)) v c(y v c(x))=c(c(x)). 118 [back_demod,92,demod,115] c(c(x))=x. 120 [binary,118.1,1.1] $F. ------------ end of proof ------------- given clause #15: (wt=5) 118 [back_demod,92,demod,115] c(c(x))=x. given clause #16: (wt=5) 137 [back_demod,66,demod,119] x v x=x. given clause #17: (wt=11) 30 [para_into,26.1.1.2.1,4.1.1] x v c(y v (c(x) v z))=x. given clause #18: (wt=9) 127 [back_demod,84,demod,119] x v (y v x)=y v x. given clause #19: (wt=9) 166 [para_into,127.1.1.2,34.1.1,demod,35] c(x v c(y)) v y=y. given clause #20: (wt=9) 170 [para_into,127.1.1.2,26.1.1,demod,27] c(c(x) v y) v x=x. given clause #21: (wt=13) 32 [para_from,26.1.1,4.1.1.2,flip.1] x v (y v c(c(x) v z))=y v x. given clause #22: (wt=7) 232 [para_into,32.1.1.2,34.1.1] x v y=y v x. given clause #23: (wt=9) 239 [para_into,232.1.1,127.1.1,flip.1] (x v y) v y=x v y. given clause #24: (wt=9) 246 [back_demod,133,demod,240] x v (x v y)=x v y. given clause #25: (wt=13) 46 [para_from,34.1.1,4.1.1.2,flip.1] x v (y v c(z v c(x)))=y v x. given clause #26: (wt=9) 267 [para_into,239.1.1.1,232.1.1] (x v y) v x=y v x. given clause #27: (wt=10) 151 [para_from,118.1.1,34.1.1.2.1.2] c(x) v c(y v x)=c(x). given clause #28: (wt=10) 153 [para_from,118.1.1,26.1.1.2.1.1] c(x) v c(x v y)=c(x). given clause #29: (wt=17) 48 [para_into,14.1.1.2.2,34.1.1,flip.1] x v (y v (z v c(u v c(x))))=y v (z v x). given clause #30: (wt=10) 180 [para_into,166.1.1.1.1.2,118.1.1] c(x v y) v c(y)=c(y). given clause #31: (wt=10) 203 [para_into,170.1.1.1.1.1,118.1.1] c(x v y) v c(x)=c(x). given clause #32: (wt=9) 411 [para_into,203.1.1.1.1,267.1.1,demod,354] c(x v y)=c(y v x). given clause #33: (wt=17) 50 [para_into,14.1.1.2.2,26.1.1,flip.1] x v (y v (z v c(c(x) v u)))=y v (z v x). given clause #34: (wt=11) 168 [para_into,127.1.1.2,30.1.1,demod,31] c(x v (c(y) v z)) v y=y. given clause #35: (wt=11) 178 [para_from,127.1.1,30.1.1.2.1.2] x v c(y v (z v c(x)))=x. given clause #36: (wt=11) 230 [para_into,32.1.1.2,170.1.1,demod,27,119,flip.1] c((c(x) v y) v z) v x=x. given clause #37: (wt=23) 54 [para_into,14.1.1.2.2,14.1.1] x v (y v (z v (u v (v v w))))=u v (x v (y v (v v (z v w)))). given clause #38: (wt=11) 245 [para_into,232.1.1,4.1.1] x v (y v z)= (x v z) v y. given clause #39: (wt=11) 260 [para_from,232.1.1,4.1.1.2] x v (y v z)=z v (x v y). given clause #40: (wt=11) 266 [copy,260,flip.1] x v (y v z)=y v (z v x). given clause #41: (wt=19) 57 [para_into,14.1.1.2.2,4.1.1] x v (y v (z v (u v v)))=u v (x v (y v (z v v))). given clause #42: (wt=11) 303 [para_into,46.1.1.2,166.1.1,demod,35,119,flip.1] c(x v (y v c(z))) v z=z. given clause #43: (wt=11) 373 [para_into,48.1.1.2,32.1.1] x v (y v z)=z v (y v x). given clause #44: (wt=11) 641 [para_into,245.1.1.2,232.1.1,flip.1] (x v y) v z=x v (y v z). given clause #45: (wt=19) 58 [para_into,14.1.1.2,14.1.1] x v (y v (z v (u v v)))=u v (x v (z v (y v v))). given clause #46: (wt=11) 646 [para_into,245.1.1,267.1.1,demod,642,642,268,268,642] x v (y v z)=x v (z v y). given clause #47: (wt=12) 155 [para_into,30.1.1.2.1.2.1,118.1.1] c(x) v c(y v (x v z))=c(x). given clause #48: (wt=12) 392 [para_from,48.1.1,153.1.1.2.1] c(x) v c(y v (z v x))=c(x). given clause #49: (wt=15) 59 [para_into,14.1.1,4.1.1] x v (y v (z v u))=z v (y v (x v u)). given clause #50: (wt=12) 412 [para_into,203.1.1.1.1,48.1.1] c(x v (y v z)) v c(z)=c(z). given clause #51: (wt=12) 418 [para_into,203.1.1.1.1,4.1.1] c(x v (y v z)) v c(y)=c(y). given clause #52: (wt=13) 105 [para_from,15.1.1,26.1.1.2.1] x v c(y v (z v (c(x) v u)))=x. given clause #53: (wt=23) 60 [copy,54,flip.1] x v (y v (z v (u v (v v w))))=y v (z v (v v (x v (u v w)))). given clause #54: (wt=13) 129 [back_demod,80,demod,119] x v (y v (z v x))=y v (z v x). given clause #55: (wt=13) 143 [back_demod,36,demod,119] x v c(x v c(y v x))=y v x. given clause #56: (wt=11) 1231 [para_from,143.1.1,32.1.1.2] x v (y v c(x))=c(x) v x. given clause #57: (wt=19) 61 [copy,57,flip.1] x v (y v (z v (u v v)))=y v (z v (u v (x v v))). given clause #58: (wt=9) 1282 [para_from,1231.1.1,168.1.1.1.1] c(c(x) v x) v y=y. given clause #59: (wt=9) 1284 [para_from,1231.1.1,105.1.1.2.1.2,demod,1266] x v c(c(y) v y)=x. given clause #60: (wt=9) 1355 [para_into,1282.1.1.1.1.1,118.1.1] c(x v c(x)) v y=y. given clause #61: (wt=19) 62 [copy,58,flip.1] x v (y v (z v (u v v)))=y v (u v (z v (x v v))). given clause #62: (wt=9) 1383 [para_into,1284.1.1.2.1.1,118.1.1] x v c(y v c(y))=x. given clause #63: (wt=11) 1243 [copy,1231,flip.1] c(x) v x=x v (y v c(x)). ----> UNIT CONFLICT at 0.19 sec ----> 1486 [binary,1485.1,2.1] $F. Length of proof is 37. Level of proof is 18. ---------------- PROOF ---------------- 2 [] A v c(A)!=B v c(B). 4 [] x v (y v z)=y v (x v z). 5 [] x v (x^y)=x. 8,7 [] x^y=c(c(x) v c(y)). 9 [] x v (c(x)^ (x v y))=x v y. 10 [copy,9,demod,8] x v c(c(c(x)) v c(x v y))=x v y. 12 [back_demod,5,demod,8] x v c(c(x) v c(y))=x. 17,16 [para_into,12.1.1.2.1,12.1.1] x v c(c(x))=x. 21,20 [para_from,16.1.1,4.1.1.2,flip.1] x v (y v c(c(x)))=y v x. 27,26 [para_from,10.1.1,12.1.1.2.1] x v c(c(x) v y)=x. 32 [para_from,26.1.1,4.1.1.2,flip.1] x v (y v c(c(x) v z))=y v x. 34 [para_from,20.1.1,26.1.1.2.1] x v c(y v c(x))=x. 36 [para_from,20.1.1,10.1.1.2.1.2.1,demod,21] x v c(c(c(x)) v c(y v x))=y v x. 44 [para_into,34.1.1.2.1,16.1.1] c(x) v c(x)=c(x). 67,66 [para_from,44.1.1,20.1.1.2,demod,17,flip.1] c(c(x)) v x=x. 76 [para_from,66.1.1,20.1.1.2,demod,17,flip.1] c(c(c(c(x)))) v x=x. 84 [para_from,66.1.1,4.1.1.2,flip.1] c(c(x)) v (y v x)=y v x. 91,90 [para_from,76.1.1,26.1.1.2.1,demod,67,flip.1] c(c(c(x)))=c(x). 92 [para_from,76.1.1,10.1.1.2.1.2.1,demod,91,91,91,91,67] c(c(x)) v c(c(c(x)) v c(x))=x. 115,114 [para_from,90.1.1,34.1.1.2.1.2] c(c(x)) v c(y v c(x))=c(c(x)). 119,118 [back_demod,92,demod,115] c(c(x))=x. 127 [back_demod,84,demod,119] x v (y v x)=y v x. 143 [back_demod,36,demod,119] x v c(x v c(y v x))=y v x. 153 [para_from,118.1.1,26.1.1.2.1.1] c(x) v c(x v y)=c(x). 170 [para_into,127.1.1.2,26.1.1,demod,27] c(c(x) v y) v x=x. 203 [para_into,170.1.1.1.1.1,118.1.1] c(x v y) v c(x)=c(x). 232 [para_into,32.1.1.2,34.1.1] x v y=y v x. 239 [para_into,232.1.1,127.1.1,flip.1] (x v y) v y=x v y. 245 [para_into,232.1.1,4.1.1] x v (y v z)= (x v z) v y. 268,267 [para_into,239.1.1.1,232.1.1] (x v y) v x=y v x. 354,353 [para_into,153.1.1.2.1,267.1.1] c(x v y) v c(y v x)=c(x v y). 411 [para_into,203.1.1.1.1,267.1.1,demod,354] c(x v y)=c(y v x). 642,641 [para_into,245.1.1.2,232.1.1,flip.1] (x v y) v z=x v (y v z). 646 [para_into,245.1.1,267.1.1,demod,642,642,268,268,642] x v (y v z)=x v (z v y). 1231 [para_from,143.1.1,32.1.1.2] x v (y v c(x))=c(x) v x. 1243 [copy,1231,flip.1] c(x) v x=x v (y v c(x)). 1255,1254 [para_into,1231.1.1.2,153.1.1,demod,642,flip.1] c(x v y) v (x v y)=x v (y v c(x)). 1264,1263 [para_into,1231.1.1,641.1.1,demod,1255] x v (y v (z v c(x v y)))=x v (y v c(x)). 1472,1471 [para_into,1243.1.1.1,411.1.1,demod,642,1264] c(x v y) v (y v x)=y v (x v c(y)). 1474 [para_into,1243.1.1,646.1.1,demod,1472,642,1264] x v (y v c(x))=y v (x v c(y)). 1482,1481 [para_into,1243.1.1,232.1.1,flip.1] x v (y v c(x))=x v c(x). 1485 [copy,1474,flip.1,demod,1482,1482] x v c(x)=y v c(y). 1486 [binary,1485.1,2.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 63 clauses generated 4402 clauses kept 1022 clauses forward subsumed 3905 clauses back subsumed 8 Kbytes malloced 1309 ----------- times (seconds) ----------- user CPU time 0.20 (0 hr, 0 min, 0 sec) system CPU time 0.08 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) para_into time 0.00 para_from time 0.01 for_sub time 0.03 back_sub time 0.04 conflict time 0.01 demod time 0.06 That finishes the proof of the theorem. Process 11083 finished Fri Oct 17 13:41:57 2003