----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:35:28 2003 The command was "otter". The process ID is 26069. 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^z)=y^ (x^z). 0 [] x v (x^y)=x. 0 [] x^ (x v y)=x. 0 [] x v (y^ (x v z))= (x v y)^ (x v z). 0 [] A v (B^ (A v C))!=A v (C^ (A v B))|$Ans(MOD). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 1 [] x=x. Following clause subsumed by 1 during input processing: 0 [copy,1,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=11): 2 [] x v (y v z)=y v (x v z). ** KEPT (pick-wt=11): 3 [] x^ (y^z)=y^ (x^z). ** KEPT (pick-wt=7): 4 [] x v (x^y)=x. ---> New Demodulator: 5 [new_demod,4] x v (x^y)=x. ** KEPT (pick-wt=7): 6 [] x^ (x v y)=x. ---> New Demodulator: 7 [new_demod,6] x^ (x v y)=x. ** KEPT (pick-wt=15): 9 [copy,8,flip.1] (x v y)^ (x v z)=x v (y^ (x v z)). ---> New Demodulator: 10 [new_demod,9] (x v y)^ (x v z)=x v (y^ (x v z)). ** KEPT (pick-wt=15): 12 [copy,11,flip.1] A v (C^ (A v B))!=A v (B^ (A v C))|$Ans(MOD). Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] x v (y v z)=y v (x v z). Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] x^ (y^z)=y^ (x^z). >>>> Starting back demodulation with 5. >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 10. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 2 [] x v (y v z)=y v (x v z). given clause #2: (wt=7) 4 [] x v (x^y)=x. given clause #3: (wt=7) 6 [] x^ (x v y)=x. given clause #4: (wt=5) 17 [para_into,6,4] x^x=x. given clause #5: (wt=11) 3 [] x^ (y^z)=y^ (x^z). given clause #6: (wt=5) 21 [para_from,6,4] x v x=x. given clause #7: (wt=9) 19 [para_into,6,2] x^ (y v (x v z))=x. given clause #8: (wt=7) 37 [para_into,19,21] x^ (y v x)=x. given clause #9: (wt=15) 9 [copy,8,flip.1] (x v y)^ (x v z)=x v (y^ (x v z)). given clause #10: (wt=9) 23 [para_into,3,17,flip.1] x^ (y^x)=y^x. given clause #11: (wt=7) 63 [para_into,23,37,demod,38] (x v y)^y=y. given clause #12: (wt=7) 69 [para_into,23,6,demod,54,7] x v (y^x)=x. given clause #13: (wt=15) 12 [copy,11,flip.1] A v (C^ (A v B))!=A v (B^ (A v C))|$Ans(MOD). given clause #14: (wt=7) 72 [back_demod,53,demod,70] (x v y)^x=x. given clause #15: (wt=9) 31 [para_from,3,4] x v (y^ (x^z))=x. given clause #16: (wt=9) 35 [para_from,21,2,flip.1] x v (y v x)=y v x. given clause #17: (wt=15) 13 [para_into,2,2] x v (y v (z v u))=z v (x v (y v u)). given clause #18: (wt=7) 125 [para_into,35,69,demod,70] (x^y) v y=y. given clause #19: (wt=7) 129 [para_into,35,4,demod,5] (x^y) v x=x. given clause #20: (wt=9) 43 [para_into,37,4] (x^y)^x=x^y. given clause #21: (wt=15) 14 [copy,13,flip.1] x v (y v (z v u))=y v (z v (x v u)). given clause #22: (wt=9) 65 [para_into,23,19,demod,20] (x v (y v z))^y=y. given clause #23: (wt=9) 77 [para_into,63,4] x^ (x^y)=x^y. given clause #24: (wt=9) 81 [para_into,63,9,demod,18] x v (x v y)=x v y. given clause #25: (wt=11) 15 [para_from,4,2,flip.1] x v (y v (x^z))=y v x. given clause #26: (wt=7) 272 [para_into,15,69] x v y=y v x. given clause #27: (wt=9) 85 [para_from,63,4] (x v y) v y=x v y. given clause #28: (wt=9) 93 [para_into,69,6] (x v y) v x=x v y. given clause #29: (wt=11) 25 [para_into,3,6,flip.1] x^ (y^ (x v z))=y^x. given clause #30: (wt=7) 363 [para_into,25,37] x^y=y^x. ----> UNIT CONFLICT at 0.03 sec ----> 376 [binary,375,12] $Ans(MOD). Length of proof is 8. Level of proof is 4. ---------------- PROOF ---------------- 2 [] x v (y v z)=y v (x v z). 3 [] x^ (y^z)=y^ (x^z). 4 [] x v (x^y)=x. 6 [] x^ (x v y)=x. 8 [] x v (y^ (x v z))= (x v y)^ (x v z). 10,9 [copy,8,flip.1] (x v y)^ (x v z)=x v (y^ (x v z)). 11 [] A v (B^ (A v C))!=A v (C^ (A v B))|$Ans(MOD). 12 [copy,11,flip.1] A v (C^ (A v B))!=A v (B^ (A v C))|$Ans(MOD). 19 [para_into,6,2] x^ (y v (x v z))=x. 21 [para_from,6,4] x v x=x. 25 [para_into,3,6,flip.1] x^ (y^ (x v z))=y^x. 37 [para_into,19,21] x^ (y v x)=x. 363 [para_into,25,37] x^y=y^x. 375 [para_into,363,9,demod,10] x v (y^ (x v z))=x v (z^ (x v y)). 376 [binary,375,12] $Ans(MOD). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 30 clauses generated 656 clauses kept 233 clauses forward subsumed 533 clauses back subsumed 1 Kbytes malloced 447 ----------- times (seconds) ----------- user CPU time 0.03 (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.00 back_sub time 0.00 conflict time 0.00 demod time 0.02 That finishes the proof of the theorem. Process 26069 finished Fri Sep 12 16:35:28 2003