----- Otter 3.3, August 2003 ----- The process was started by mccune on lemma.mcs.anl.gov, Mon Sep 15 12:19:36 2003 The command was "otter". The process ID is 2367. op(400,infix,^). op(400,infix,v). lex([C,B,A,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,4). assign(max_weight,40). set(discard_commutativity_consequences). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). clear(sigint_interact). clear(detailed_history). list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z)))=x. 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 c(c(A) v B)!=A|$Ans(B1_rewritten). 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=23): 7 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z)))=y. ---> New Demodulator: 8 [new_demod,7] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z)))=y. ** KEPT (pick-wt=11): 10 [copy,9,flip.1] f(f(x,x),f(y,y))=x v y. ---> New Demodulator: 11 [new_demod,10] f(f(x,x),f(y,y))=x v y. ** KEPT (pick-wt=11): 13 [copy,12,flip.1] f(f(x,y),f(x,y))=x^y. ---> New Demodulator: 14 [new_demod,13] f(f(x,y),f(x,y))=x^y. ** KEPT (pick-wt=6): 16 [copy,15,flip.1] f(x,x)=c(x). ---> New Demodulator: 17 [new_demod,16] f(x,x)=c(x). >>>> Starting back demodulation with 8. >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 17. >> back demodulating 13 with 17. >> back demodulating 10 with 17. >> back demodulating 7 with 17. >>>> Starting back demodulation with 19. >>>> Starting back demodulation with 21. >>>> Starting back demodulation with 23. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=6) 16 [copy,15,flip.1] f(x,x)=c(x). given clause #2: (wt=8) 18 [back_demod,13,demod,17] c(f(x,y))=x^y. given clause #3: (wt=7) 24 [para_into,18,16,flip.1] x^x=c(c(x)). given clause #4: (wt=9) 20 [back_demod,10,demod,17,17] f(c(x),c(y))=x v y. given clause #5: (wt=7) 29 [para_into,20,16] c(c(x))=x v x. given clause #6: (wt=22) 22 [back_demod,7,demod,17] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z)))=y. given clause #7: (wt=7) 32 [back_demod,24,demod,30] x^x=x v x. given clause #8: (wt=10) 34 [para_from,20,18,flip.1] c(x)^c(y)=c(x v y). given clause #9: (wt=10) 36 [para_into,29,29] c(x v x)=c(x) v c(x). given clause #10: (wt=11) 40 [para_from,29,20] f(c(x),y v y)=x v c(y). given clause #11: (wt=12) 26 [para_into,20,18] f(x^y,c(z))=f(x,y) v z. given clause #12: (wt=11) 42 [para_from,29,20] f(x v x,c(y))=c(x) v y. given clause #13: (wt=12) 28 [para_into,20,18] f(c(x),y^z)=x v f(y,z). given clause #14: (wt=12) 31 [copy,28,flip.1] x v f(y,z)=f(c(x),y^z). given clause #15: (wt=12) 38 [para_into,29,18,flip.1] f(x,y) v f(x,y)=c(x^y). given clause #16: (wt=26) 44 [para_into,22,20,demod,30] f(f(f(x v y,f(c(y),z)),u),f(c(y),f(f(z,f(y v y,z)),z)))=c(y). given clause #17: (wt=12) 70 [para_into,34,29] (x v x)^c(y)=c(c(x) v y). given clause #18: (wt=12) 73 [para_into,34,29] c(x)^ (y v y)=c(x v c(y)). given clause #19: (wt=13) 72 [para_into,34,18] (x^y)^c(z)=c(f(x,y) v z). given clause #20: (wt=13) 75 [para_into,34,18] c(x)^ (y^z)=c(x v f(y,z)). given clause #21: (wt=21) 46 [para_into,22,16] f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y)))=x. given clause #22: (wt=13) 76 [copy,72,flip.1] c(f(x,y) v z)= (x^y)^c(z). given clause #23: (wt=13) 77 [copy,75,flip.1] c(x v f(y,z))=c(x)^ (y^z). given clause #24: (wt=13) 82 [para_into,40,29] f(x v x,y v y)=c(x) v c(y). given clause #25: (wt=14) 84 [para_into,40,18] f(x^y,z v z)=f(x,y) v c(z). given clause #26: (wt=27) 48 [para_into,22,20,demod,30,43] f(f(f(f(x,c(y)),y v z),u),f(c(y),f(f(c(z),c(y) v z),c(z))))=c(y). given clause #27: (wt=14) 96 [para_into,42,18] f(x v x,y^z)=c(x) v f(y,z). given clause #28: (wt=14) 97 [copy,96,flip.1] c(x) v f(y,z)=f(x v x,y^z). given clause #29: (wt=14) 136 [para_into,70,29] (x v x)^ (y v y)=c(c(x) v c(y)). given clause #30: (wt=15) 92 [para_into,26,18] f(x^y,z^u)=f(x,y) v f(z,u). given clause #31: (wt=21) 50 [para_into,22,16] f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y)))=y. given clause #32: (wt=15) 93 [copy,92,flip.1] f(x,y) v f(z,u)=f(x^y,z^u). given clause #33: (wt=15) 138 [para_into,70,18] (x v x)^ (y^z)=c(c(x) v f(y,z)). given clause #34: (wt=15) 139 [copy,138,flip.1] c(c(x) v f(y,z))= (x v x)^ (y^z). given clause #35: (wt=15) 140 [para_into,73,18] (x^y)^ (z v z)=c(f(x,y) v c(z)). given clause #36: (wt=37) 52 [para_into,22,22] f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z))))=x. given clause #37: (wt=15) 141 [copy,140,flip.1] c(f(x,y) v c(z))= (x^y)^ (z v z). given clause #38: (wt=15) 398 [para_from,52,46] f(c(x),f(x,f(f(y,f(c(x),y)),y)))=x. ----> UNIT CONFLICT at 0.05 sec ----> 604 [binary,602,3] $Ans(DM). Length of proof is 16. Level of proof is 6. ---------------- PROOF ---------------- 3 [] A^B!=c(c(A) v c(B))|$Ans(DM). 7 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z)))=y. 9 [] x v y=f(f(x,x),f(y,y)). 10 [copy,9,flip.1] f(f(x,x),f(y,y))=x v y. 12 [] x^y=f(f(x,y),f(x,y)). 13 [copy,12,flip.1] f(f(x,y),f(x,y))=x^y. 15 [] c(x)=f(x,x). 17,16 [copy,15,flip.1] f(x,x)=c(x). 18 [back_demod,13,demod,17] c(f(x,y))=x^y. 20 [back_demod,10,demod,17,17] f(c(x),c(y))=x v y. 22 [back_demod,7,demod,17] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z)))=y. 30,29 [para_into,20,16] c(c(x))=x v x. 34 [para_from,20,18,flip.1] c(x)^c(y)=c(x v y). 46 [para_into,22,16] f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y)))=x. 52 [para_into,22,22] f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z))))=x. 70 [para_into,34,29] (x v x)^c(y)=c(c(x) v y). 136 [para_into,70,29] (x v x)^ (y v y)=c(c(x) v c(y)). 398 [para_from,52,46] f(c(x),f(x,f(f(y,f(c(x),y)),y)))=x. 403,402 [para_from,52,22] f(f(x,y),f(y,f(f(z,f(c(y),z)),z)))=y. 451,450 [para_into,398,398,demod,403,17,17,30] x v x=x. 602 [back_demod,136,demod,451,451] x^y=c(c(x) v c(y)). 604 [binary,602,3] $Ans(DM). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.05 sec ----> 633 [binary,631,5] $Ans(DEF_SS). Length of proof is 13. Level of proof is 6. ---------------- PROOF ---------------- 5 [] f(A,B)!=c(A) v c(B)|$Ans(DEF_SS). 7 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z)))=y. 9 [] x v y=f(f(x,x),f(y,y)). 10 [copy,9,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] c(x)=f(x,x). 17,16 [copy,15,flip.1] f(x,x)=c(x). 20 [back_demod,10,demod,17,17] f(c(x),c(y))=x v y. 22 [back_demod,7,demod,17] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z)))=y. 30,29 [para_into,20,16] c(c(x))=x v x. 40 [para_from,29,20] f(c(x),y v y)=x v c(y). 46 [para_into,22,16] f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y)))=x. 52 [para_into,22,22] f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z))))=x. 82 [para_into,40,29] f(x v x,y v y)=c(x) v c(y). 398 [para_from,52,46] f(c(x),f(x,f(f(y,f(c(x),y)),y)))=x. 403,402 [para_from,52,22] f(f(x,y),f(y,f(f(z,f(c(y),z)),z)))=y. 451,450 [para_into,398,398,demod,403,17,17,30] x v x=x. 631 [back_demod,82,demod,451,451] f(x,y)=c(x) v c(y). 633 [binary,631,5] $Ans(DEF_SS). ------------ end of proof ------------- given clause #39: (wt=5) 450 [para_into,398,398,demod,403,17,17,30] x v x=x. given clause #40: (wt=5) 642 [back_demod,29,demod,451] c(c(x))=x. given clause #41: (wt=10) 602 [back_demod,136,demod,451,451] x^y=c(c(x) v c(y)). given clause #42: (wt=9) 631 [back_demod,82,demod,451,451] f(x,y)=c(x) v c(y). given clause #43: (wt=16) 680 [back_demod,458,demod,632,643,632,643,632,632,643] x v c(c(x) v c(c(x v c(x)) v x))=x. given clause #44: (wt=18) 682 [back_demod,456,demod,632,643,632,643,632,632,643] x v c(c(x) v c(c(y v c(x v y)) v y))=x. given clause #45: (wt=18) 698 [para_into,680,642,demod,643] c(x) v c(x v c(c(c(x) v x) v c(x)))=c(x). given clause #46: (wt=26) 638 [back_demod,54,demod,451,632,632,30,451,632,632,632,632] c(c(x) v c(y)) v c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. given clause #47: (wt=9) 712 [back_demod,706,demod,709] c(c(x) v y) v x=x. given clause #48: (wt=10) 718 [para_into,712,642] c(x v y) v c(x)=c(x). given clause #49: (wt=9) 724 [para_into,718,718,demod,643,643,643] x v (x v y)=x v y. given clause #50: (wt=12) 716 [back_demod,652,demod,709] (c(c(x) v c(y)) v y) v y=y. given clause #51: (wt=28) 654 [back_demod,234,demod,632,643,603,632,643,632,643,632,643,632,643] (c(c(x) v y) v c(y v z)) v c(y v c(c(z v c(c(y) v z)) v z))=c(y). given clause #52: (wt=11) 730 [para_into,716,642] (c(x v c(y)) v y) v y=y. given clause #53: (wt=11) 776 [back_demod,680,demod,767,643] x v (c(x v c(x)) v x)=x. given clause #54: (wt=13) 764 [para_into,730,642] (c(x v y) v c(y)) v c(y)=c(y). given clause #55: (wt=14) 778 [para_into,776,642] c(x) v (c(c(x) v x) v c(x))=c(x). given clause #56: (wt=37) 666 [back_demod,623,demod,632,632,632,632,643,632,632,632,632] c(c(c(x v c(y)) v c(c(y) v c(z))) v c(u)) v c(c(y) v c(c(c(z) v c(y v c(z))) v c(z)))=y. given clause #57: (wt=16) 714 [back_demod,674,demod,709] c(c(c(x v c(y)) v y) v c(z)) v y=y. given clause #58: (wt=9) 808 [para_into,714,718,demod,643] c(x v c(y)) v y=y. given clause #59: (wt=10) 822 [para_into,808,642] c(x v y) v c(y)=c(y). given clause #60: (wt=9) 838 [para_from,822,712,demod,643] x v (y v x)=y v x. given clause #61: (wt=29) 672 [back_demod,600,demod,632,643,632,632,643,632,643,632,632] c(c(x v c(c(x) v y)) v c(z)) v c(c(x) v c(c(y v c(x v y)) v y))=x. given clause #62: (wt=11) 908 [back_demod,738,demod,877] (x v c(c(x) v y)) v x=x. given clause #63: (wt=11) 912 [para_into,908,838] (x v c(y v c(x))) v x=x. given clause #64: (wt=12) 818 [back_demod,728,demod,809] x v c(c(x) v c(x v y))=x. ----> UNIT CONFLICT at 0.08 sec ----> 930 [binary,928,2] $Ans(B1_rewritten). Length of proof is 51. Level of proof is 16. ---------------- PROOF ---------------- 2 [] A v c(c(A) v B)!=A|$Ans(B1_rewritten). 7 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z)))=y. 9 [] x v y=f(f(x,x),f(y,y)). 10 [copy,9,flip.1] f(f(x,x),f(y,y))=x v y. 12 [] x^y=f(f(x,y),f(x,y)). 13 [copy,12,flip.1] f(f(x,y),f(x,y))=x^y. 15 [] c(x)=f(x,x). 17,16 [copy,15,flip.1] f(x,x)=c(x). 19,18 [back_demod,13,demod,17] c(f(x,y))=x^y. 20 [back_demod,10,demod,17,17] f(c(x),c(y))=x v y. 22 [back_demod,7,demod,17] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z)))=y. 30,29 [para_into,20,16] c(c(x))=x v x. 34 [para_from,20,18,flip.1] c(x)^c(y)=c(x v y). 37,36 [para_into,29,29] c(x v x)=c(x) v c(x). 40 [para_from,29,20] f(c(x),y v y)=x v c(y). 43,42 [para_from,29,20] f(x v x,c(y))=c(x) v y. 46 [para_into,22,16] f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y)))=x. 48 [para_into,22,20,demod,30,43] f(f(f(f(x,c(y)),y v z),u),f(c(y),f(f(c(z),c(y) v z),c(z))))=c(y). 50 [para_into,22,16] f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y)))=y. 52 [para_into,22,22] f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z))))=x. 54 [para_into,22,16,demod,17,30] f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x)))=x. 70 [para_into,34,29] (x v x)^c(y)=c(c(x) v y). 83,82 [para_into,40,29] f(x v x,y v y)=c(x) v c(y). 136 [para_into,70,29] (x v x)^ (y v y)=c(c(x) v c(y)). 158 [para_into,46,42,demod,37,37,43,30] f(f(f(c(x) v c(x),c(x) v y),z),f(x v x,f(f(c(y),(x v x) v y),c(y))))=x v x. 234 [para_into,48,16,demod,19] f(f(x,c(y))^ (y v z),f(c(y),f(f(c(z),c(y) v z),c(z))))=c(y). 306 [para_into,50,40,demod,37,37,83,30] f(f(f(x v c(y),c(y) v c(y)),z),f(y v y,f(f(y v y,(y v y) v c(y)),y v y)))=y v y. 398 [para_from,52,46] f(c(x),f(x,f(f(y,f(c(x),y)),y)))=x. 403,402 [para_from,52,22] f(f(x,y),f(y,f(f(z,f(c(y),z)),z)))=y. 451,450 [para_into,398,398,demod,403,17,17,30] x v x=x. 456 [para_into,398,20] f(c(x),f(x,f(f(c(y),x v y),c(y))))=x. 536 [back_demod,306,demod,451,451,451,451,451,451] f(f(f(x v c(y),c(y)),z),f(y,f(f(y,y v c(y)),y)))=y. 600 [back_demod,158,demod,451,451,451,451] f(f(f(c(x),c(x) v y),z),f(x,f(f(c(y),x v y),c(y))))=x. 603,602 [back_demod,136,demod,451,451] x^y=c(c(x) v c(y)). 632,631 [back_demod,82,demod,451,451] f(x,y)=c(x) v c(y). 638 [back_demod,54,demod,451,632,632,30,451,632,632,632,632] c(c(x) v c(y)) v c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 643,642 [back_demod,29,demod,451] c(c(x))=x. 654 [back_demod,234,demod,632,643,603,632,643,632,643,632,643,632,643] (c(c(x) v y) v c(y v z)) v c(y v c(c(z v c(c(y) v z)) v z))=c(y). 672 [back_demod,600,demod,632,643,632,632,643,632,643,632,632] c(c(x v c(c(x) v y)) v c(z)) v c(c(x) v c(c(y v c(x v y)) v y))=x. 674 [back_demod,536,demod,632,643,632,632,632,632,632] c(c(c(x v c(y)) v y) v c(z)) v c(c(y) v c(c(c(y) v c(y v c(y))) v c(y)))=y. 682 [back_demod,456,demod,632,643,632,643,632,632,643] x v c(c(x) v c(c(y v c(x v y)) v y))=x. 706 [para_into,638,642] c(c(x) v y) v c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 709,708 [para_into,638,450] c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 712 [back_demod,706,demod,709] c(c(x) v y) v x=x. 714 [back_demod,674,demod,709] c(c(c(x v c(y)) v y) v c(z)) v y=y. 718 [para_into,712,642] c(x v y) v c(x)=c(x). 724 [para_into,718,718,demod,643,643,643] x v (x v y)=x v y. 728 [para_from,724,682] x v c(c(x) v c(c((x v y) v c(x v y)) v (x v y)))=x. 738 [para_into,654,718,demod,643,643,643] (x v c(c(x) v y)) v c(c(x) v c(c(y v c(x v y)) v y))=x. 809,808 [para_into,714,718,demod,643] c(x v c(y)) v y=y. 818 [back_demod,728,demod,809] x v c(c(x) v c(x v y))=x. 877,876 [para_into,672,808] c(c(x) v c(c(y v c(x v y)) v y))=x. 909,908 [back_demod,738,demod,877] (x v c(c(x) v y)) v x=x. 919,918 [para_from,908,718] c(x) v c(x v c(c(x) v y))=c(x v c(c(x) v y)). 925,924 [para_into,818,642,demod,919] c(x v c(c(x) v y))=c(x). 928 [para_into,818,908,demod,925,451,643,909,flip.1] x v c(c(x) v y)=x. 930 [binary,928,2] $Ans(B1_rewritten). ------------ end of proof ------------- given clause #65: (wt=9) 926 [para_into,818,912,demod,719,643,913,flip.1] x v c(y v c(x))=x. given clause #66: (wt=25) 678 [back_demod,490,demod,632,632,632,632,643,632] c(x v y) v c(y v c(c(c(z) v c(c(y) v c(z))) v c(z)))=c(y). given clause #67: (wt=9) 928 [para_into,818,908,demod,925,451,643,909,flip.1] x v c(c(x) v y)=x. given clause #68: (wt=9) 955 [para_into,928,822,demod,643] (x v y) v y=x v y. given clause #69: (wt=9) 957 [para_into,928,718,demod,643] (x v y) v x=x v y. given clause #70: (wt=10) 937 [para_into,926,642] c(x) v c(y v x)=c(x). given clause #71: (wt=32) 694 [back_demod,122,demod,632,632,632,643,632,643,632,643,632] c(c(c(x v y) v c(y v z)) v c(u)) v c(y v c(c(z v c(c(y) v z)) v z))=c(y). given clause #72: (wt=10) 953 [para_into,928,642] c(x) v c(x v y)=c(x). given clause #73: (wt=13) 896 [back_demod,794,demod,877] c((c(x) v c(y)) v c(z)) v x=x. given clause #74: (wt=12) 1017 [para_into,896,642] c((c(x) v y) v c(z)) v x=x. given clause #75: (wt=11) 1035 [para_into,1017,642] c((c(x) v y) v z) v x=x. given clause #76: (wt=16) 876 [para_into,672,808] c(c(x) v c(c(y v c(x v y)) v y))=x. given clause #77: (wt=11) 1041 [para_into,1035,838] c((x v c(y)) v z) v y=y. given clause #78: (wt=11) 1051 [para_into,1035,838] c(x v (c(y) v z)) v y=y. given clause #79: (wt=11) 1057 [para_from,1035,957,demod,1036] x v c((c(x) v y) v z)=x. given clause #80: (wt=11) 1085 [para_into,1041,838] c(x v (y v c(z))) v z=z. given clause #81: (wt=16) 892 [back_demod,800,demod,877] (c(x v c(y)) v c(c(y) v c(z))) v y=y. given clause #82: (wt=11) 1093 [para_from,1041,957,demod,1042] x v c((y v c(x)) v z)=x. given clause #83: (wt=11) 1117 [para_from,1051,957,demod,1052] x v c(y v (c(x) v z))=x. given clause #84: (wt=11) 1147 [para_from,1085,957,demod,1086] x v c(y v (z v c(x)))=x. given clause #85: (wt=12) 1037 [para_into,1035,642] c((x v y) v z) v c(x)=c(x). given clause #86: (wt=20) 894 [back_demod,796,demod,877] c(c(c(x v c(y)) v c(c(y) v c(z))) v u) v y=y. given clause #87: (wt=12) 1083 [para_into,1041,642] c((x v y) v z) v c(y)=c(y). given clause #88: (wt=12) 1095 [para_into,1051,642] c(x v (y v z)) v c(y)=c(y). given clause #89: (wt=12) 1119 [para_into,1057,642] c(x) v c((x v y) v z)=c(x). given clause #90: (wt=12) 1135 [para_into,1085,642] c(x v (y v z)) v c(z)=c(z). given clause #91: (wt=22) 969 [para_into,694,937,demod,643,643,877,643] c(c(x v c(c(y v x) v z)) v c(u)) v (y v x)=y v x. given clause #92: (wt=12) 1171 [para_into,1093,642] c(x) v c((y v x) v z)=c(x). given clause #93: (wt=12) 1173 [para_into,1117,642] c(x) v c(y v (x v z))=c(x). given clause #94: (wt=12) 1191 [para_into,1147,642] c(x) v c(y v (z v x))=c(x). given clause #95: (wt=13) 1043 [para_into,1035,822] c(c(x) v y) v (z v x)=z v x. given clause #96: (wt=17) 999 [para_into,694,808] c(x v c(c(y v c(c(x) v y)) v y))=c(x). given clause #97: (wt=13) 1047 [para_into,1035,718] c(c(x) v y) v (x v z)=x v z. given clause #98: (wt=13) 1103 [para_into,1051,822] c(x v c(y)) v (z v y)=z v y. given clause #99: (wt=13) 1107 [para_into,1051,718] c(x v c(y)) v (y v z)=y v z. given clause #100: (wt=13) 1127 [para_into,1057,822] (x v y) v c(c(y) v z)=x v y. given clause #101: (wt=19) 1003 [back_demod,983,demod,1000] c(c(c(x v y) v c(y v z)) v u) v c(y)=c(y). given clause #102: (wt=13) 1131 [para_into,1057,718] (x v y) v c(c(x) v z)=x v y. given clause #103: (wt=13) 1183 [para_into,1117,822] (x v y) v c(z v c(y))=x v y. given clause #104: (wt=13) 1187 [para_into,1117,718] (x v y) v c(z v c(x))=x v y. given clause #105: (wt=13) 1199 [para_from,1037,928,demod,643] ((x v y) v z) v x= (x v y) v z. given clause #106: (wt=15) 1015 [back_demod,734,demod,1000] (c(x v y) v c(y v z)) v c(y)=c(y). given clause #107: (wt=13) 1201 [para_from,1037,712,demod,643] x v ((x v y) v z)= (x v y) v z. given clause #108: (wt=13) 1241 [para_from,1083,928,demod,643] ((x v y) v z) v y= (x v y) v z. given clause #109: (wt=13) 1243 [para_from,1083,712,demod,643] x v ((y v x) v z)= (y v x) v z. given clause #110: (wt=13) 1255 [para_from,1095,928,demod,643] (x v (y v z)) v y=x v (y v z). given clause #111: (wt=18) 1039 [para_into,1035,1035] c(x v y) v ((c(x) v z) v u)= (c(x) v z) v u. given clause #112: (wt=13) 1257 [para_from,1095,712,demod,643] x v (y v (x v z))=y v (x v z). given clause #113: (wt=13) 1265 [para_from,1135,928,demod,643] (x v (y v z)) v z=x v (y v z). given clause #114: (wt=13) 1267 [para_from,1135,712,demod,643] x v (y v (z v x))=y v (z v x). given clause #115: (wt=13) 1313 [para_into,1043,1147,demod,643,1148] c((x v (y v c(z))) v u) v z=z. given clause #116: (wt=14) 1045 [para_into,1035,808] c(x v y) v (z v c(x))=z v c(x). given clause #117: (wt=13) 1317 [para_into,1043,1117,demod,643,1118] c((x v (c(y) v z)) v u) v y=y. given clause #118: (wt=13) 1319 [para_into,1043,1093,demod,643,1094] c(((x v c(y)) v z) v u) v y=y. given clause #119: (wt=13) 1321 [para_into,1043,1057,demod,643,1058] c(((c(x) v y) v z) v u) v x=x. given clause #120: (wt=13) 1393 [para_into,1103,1147,demod,643,1148] c(x v (y v (z v c(u)))) v u=u. given clause #121: (wt=14) 1049 [para_into,1035,712] c(x v y) v (c(x) v z)=c(x) v z. given clause #122: (wt=13) 1397 [para_into,1103,1117,demod,643,1118] c(x v (y v (c(z) v u))) v z=z. given clause #123: (wt=13) 1399 [para_into,1103,1093,demod,643,1094] c(x v ((y v c(z)) v u)) v z=z. given clause #124: (wt=13) 1401 [para_into,1103,1057,demod,643,1058] c(x v ((c(y) v z) v u)) v y=y. given clause #125: (wt=13) 1437 [para_into,1127,1147,demod,643,1148] x v c((y v (z v c(x))) v u)=x. given clause #126: (wt=20) 1061 [para_into,876,957] c(c(x v y) v c(c(x v c(x v y)) v x))=x v y. given clause #127: (wt=13) 1443 [para_into,1127,1117,demod,643,1118] x v c((y v (c(x) v z)) v u)=x. given clause #128: (wt=13) 1445 [para_into,1127,1093,demod,643,1094] x v c(((y v c(x)) v z) v u)=x. given clause #129: (wt=13) 1447 [para_into,1127,1057,demod,643,1058] x v c(((c(x) v y) v z) v u)=x. given clause #130: (wt=13) 1535 [para_into,1183,1147,demod,643,1148] x v c(y v (z v (u v c(x))))=x. given clause #131: (wt=20) 1063 [para_into,876,955] c(c(x v y) v c(c(y v c(x v y)) v y))=x v y. given clause #132: (wt=13) 1543 [para_into,1183,1117,demod,643,1118] x v c(y v (z v (c(x) v u)))=x. given clause #133: (wt=13) 1545 [para_into,1183,1093,demod,643,1094] x v c(y v ((z v c(x)) v u))=x. given clause #134: (wt=13) 1547 [para_into,1183,1057,demod,643,1058] x v c(y v ((c(x) v z) v u))=x. given clause #135: (wt=13) 2405 [para_from,1063,937,demod,643,1168,643,flip.1] c(x v c(y v x)) v x=y v x. given clause #136: (wt=18) 1087 [para_from,1041,1035] c(x v y) v ((z v c(x)) v u)= (z v c(x)) v u. given clause #137: (wt=11) 2523 [para_into,2405,1171,demod,643,flip.1] (x v y) v c(y)=y v c(y). given clause #138: (wt=9) 2655 [para_from,2523,1445] x v c(y v c(y))=x. given clause #139: (wt=9) 2657 [para_from,2523,1321] c(x v c(x)) v y=y. given clause #140: (wt=9) 2699 [para_into,2655,642] x v c(c(y) v y)=x. given clause #141: (wt=18) 1097 [para_into,1051,1051] c(x v y) v (z v (c(y) v u))=z v (c(y) v u). given clause #142: (wt=9) 2701 [para_into,2657,642] c(c(x) v x) v y=y. given clause #143: (wt=11) 2528 [para_into,2405,1119,demod,643,flip.1] (x v y) v c(x)=x v c(x). given clause #144: (wt=9) 2803 [para_into,2528,2523,demod,2668,2802] x v c(x)=y v c(y). given clause #145: (wt=9) 2835 [para_into,2528,1183,demod,2531,2802] c(x) v x=y v c(y). given clause #146: (wt=18) 1099 [para_into,1051,1041] c(x v y) v ((z v c(y)) v u)= (z v c(y)) v u. given clause #147: (wt=9) 2850 [copy,2835,flip.1] x v c(x)=c(y) v y. given clause #148: (wt=9) 2881 [para_into,2850,642] c(x) v x=c(y) v y. given clause #149: (wt=11) 2530 [para_into,2405,1093,flip.1] (x v c(y)) v y=c(y) v y. given clause #150: (wt=11) 2532 [para_into,2405,1057,flip.1] (c(x) v y) v x=c(x) v x. given clause #151: (wt=18) 1101 [para_into,1051,1035] c(x v y) v ((c(y) v z) v u)= (c(y) v z) v u. given clause #152: (wt=11) 2665 [para_from,2523,1201,demod,2524] x v (y v c(y))=y v c(y). given clause #153: (wt=11) 2667 [para_from,2523,1199,demod,2524] (x v c(x)) v y=x v c(x). given clause #154: (wt=11) 2669 [back_demod,2538,demod,2658,643] c(x) v (x v y)=x v c(x). given clause #155: (wt=11) 2703 [para_into,2657,2655] c(x v c(x))=c(y v c(y)). given clause #156: (wt=14) 1105 [para_into,1051,808] c(x v y) v (z v c(y))=z v c(y). given clause #157: (wt=11) 2704 [para_into,2699,2657] c(c(x) v x)=c(y v c(y)). given clause #158: (wt=11) 2705 [para_into,2699,2523,demod,2700,flip.1] x v (c(y) v y)=c(y) v y. given clause #159: (wt=11) 2721 [copy,2704,flip.1] c(x v c(x))=c(c(y) v y). given clause #160: (wt=11) 2798 [para_into,2701,2699] c(c(x) v x)=c(c(y) v y). given clause #161: (wt=14) 1109 [para_into,1051,712] c(x v y) v (c(y) v z)=c(y) v z. given clause #162: (wt=11) 2829 [para_into,2528,2699,demod,2700] (c(x) v x) v y=c(x) v x. given clause #163: (wt=11) 2831 [para_into,2528,1265] x v (y v c(x))=x v c(x). given clause #164: (wt=11) 2833 [para_into,2528,1255] x v (c(x) v y)=x v c(x). given clause #165: (wt=11) 2882 [para_into,2532,1265] c(x) v (y v x)=c(x) v x. given clause #166: (wt=18) 1111 [para_from,1051,1035] c(x v y) v (z v (c(x) v u))=z v (c(x) v u). given clause #167: (wt=13) 2511 [para_into,2405,957,demod,958] c(x v c(x v y)) v x=x v y. given clause #168: (wt=13) 2515 [para_into,2405,1447,flip.1] ((c(x) v y) v z) v x=c(x) v x. given clause #169: (wt=13) 2517 [para_into,2405,1445,flip.1] ((x v c(y)) v z) v y=c(y) v y. given clause #170: (wt=13) 2519 [para_into,2405,1443,flip.1] (x v (c(y) v z)) v y=c(y) v y. given clause #171: (wt=18) 1121 [para_into,1057,1051] (x v (c(y) v z)) v c(y v u)=x v (c(y) v z). given clause #172: (wt=13) 2521 [para_into,2405,1437,flip.1] (x v (y v c(z))) v z=c(z) v z. given clause #173: (wt=13) 2607 [para_into,2523,1265] (x v (y v z)) v c(z)=z v c(z). given clause #174: (wt=13) 2609 [para_into,2523,1255] (x v (y v z)) v c(y)=y v c(y). given clause #175: (wt=13) 2611 [para_into,2523,1241] ((x v y) v z) v c(y)=y v c(y). given clause #176: (wt=18) 1123 [para_into,1057,1041] ((x v c(y)) v z) v c(y v u)= (x v c(y)) v z. given clause #177: (wt=13) 2613 [para_into,2523,1199] ((x v y) v z) v c(x)=x v c(x). given clause #178: (wt=13) 2813 [para_into,2528,1049,demod,643,643,2697] (c(x) v y) v (x v z)=x v c(x). given clause #179: (wt=13) 2816 [para_into,2528,1045,demod,643,643,2697] (x v c(y)) v (y v z)=y v c(y). given clause #180: (wt=13) 2821 [para_into,2528,1037,demod,643,643,2697,2802] c(x) v ((x v y) v z)=x v c(x). given clause #181: (wt=18) 1125 [para_into,1057,1035] ((c(x) v y) v z) v c(x v u)= (c(x) v y) v z. given clause #182: (wt=13) 2823 [para_into,2528,1035,demod,643,643,2697,2802,643] x v ((c(x) v y) v z)=c(x) v x. given clause #183: (wt=13) 2846 [back_demod,2624,demod,2834] (x v y) v (c(y) v z)=y v c(y). given clause #184: (wt=13) 2848 [back_demod,2622,demod,2834] (x v y) v (c(x) v z)=x v c(x). given clause #185: (wt=13) 2917 [para_into,2669,1267] c(x) v (y v (z v x))=x v c(x). given clause #186: (wt=14) 1129 [para_into,1057,808] (x v c(y)) v c(y v z)=x v c(y). given clause #187: (wt=13) 2919 [para_into,2669,1257] c(x) v (y v (x v z))=x v c(x). given clause #188: (wt=13) 2921 [para_into,2669,1243] c(x) v ((y v x) v z)=x v c(x). given clause #189: (wt=13) 2929 [para_into,2669,1045,demod,643,643,2697] (x v y) v (z v c(x))=x v c(x). given clause #190: (wt=13) 2931 [para_into,2669,1043,demod,643,643,2697,643] (c(x) v y) v (z v x)=c(x) v x. given clause #191: (wt=14) 1133 [para_into,1057,712] (c(x) v y) v c(x v z)=c(x) v y. given clause #192: (wt=13) 2976 [para_into,2831,1265] x v (y v (z v c(x)))=x v c(x). given clause #193: (wt=13) 2978 [para_into,2831,1255] x v (y v (c(x) v z))=x v c(x). given clause #194: (wt=13) 2980 [para_into,2831,1241] x v ((y v c(x)) v z)=x v c(x). given clause #195: (wt=13) 3116 [para_into,2517,1265] (x v c(y)) v (z v y)=c(y) v y. given clause #196: (wt=18) 1137 [para_from,1085,1057] (x v (y v c(z))) v c(z v u)=x v (y v c(z)). given clause #197: (wt=13) 3256 [para_into,2611,1265] (x v y) v (z v c(y))=y v c(y). given clause #198: (wt=14) 1185 [para_into,1117,808] (x v c(y)) v c(z v y)=x v c(y). given clause #199: (wt=14) 1189 [para_into,1117,712] (c(x) v y) v c(z v x)=c(x) v y. given clause #200: (wt=14) 1307 [para_into,1043,1191,demod,643,1192] c((x v (y v z)) v u) v c(z)=c(z). given clause #201: (wt=18) 1139 [para_from,1085,1035] c(x v y) v (z v (u v c(x)))=z v (u v c(x)). given clause #202: (wt=14) 1309 [para_into,1043,1173,demod,643,1174] c((x v (y v z)) v u) v c(y)=c(y). given clause #203: (wt=14) 1311 [para_into,1043,1171,demod,643,1172] c(((x v y) v z) v u) v c(y)=c(y). given clause #204: (wt=14) 1315 [para_into,1043,1119,demod,643,1120] c(((x v y) v z) v u) v c(x)=c(x). given clause #205: (wt=14) 1387 [para_into,1103,1191,demod,643,1192] c(x v (y v (z v u))) v c(u)=c(u). given clause #206: (wt=18) 1145 [para_from,1085,1051] c(x v y) v (z v (u v c(y)))=z v (u v c(y)). given clause #207: (wt=14) 1389 [para_into,1103,1173,demod,643,1174] c(x v (y v (z v u))) v c(z)=c(z). given clause #208: (wt=14) 1391 [para_into,1103,1171,demod,643,1172] c(x v ((y v z) v u)) v c(z)=c(z). given clause #209: (wt=14) 1395 [para_into,1103,1119,demod,643,1120] c(x v ((y v z) v u)) v c(y)=c(y). given clause #210: (wt=14) 1431 [para_into,1127,1191,demod,643,1192] c(x) v c((y v (z v x)) v u)=c(x). given clause #211: (wt=16) 1151 [para_into,892,957] (c(c(x) v y) v c(c(x) v c(z))) v x=x. given clause #212: (wt=14) 1433 [para_into,1127,1173,demod,643,1174] c(x) v c((y v (x v z)) v u)=c(x). given clause #213: (wt=14) 1435 [para_into,1127,1171,demod,643,1172] c(x) v c(((y v x) v z) v u)=c(x). given clause #214: (wt=14) 1441 [para_into,1127,1119,demod,643,1120] c(x) v c(((x v y) v z) v u)=c(x). given clause #215: (wt=14) 1527 [para_into,1183,1191,demod,643,1192] c(x) v c(y v (z v (u v x)))=c(x). given clause #216: (wt=15) 1157 [para_into,892,642] (c(x v c(y)) v c(c(y) v z)) v y=y. given clause #217: (wt=14) 1531 [para_into,1183,1173,demod,643,1174] c(x) v c(y v (z v (x v u)))=c(x). given clause #218: (wt=14) 1533 [para_into,1183,1171,demod,643,1172] c(x) v c(y v ((z v x) v u))=c(x). given clause #219: (wt=14) 1541 [para_into,1183,1119,demod,643,1120] c(x) v c(y v ((x v z) v u))=c(x). given clause #220: (wt=15) 1375 [para_into,1047,1047,demod,643,1048] c((c(x) v y) v z) v (x v u)=x v u. given clause #221: (wt=23) 1159 [para_into,892,1085,demod,643,643,643,643] (c(x v c(y v (z v u))) v u) v (y v (z v u))=y v (z v u). given clause #222: (wt=15) 1377 [para_into,1047,1043,demod,643,1044] c((c(x) v y) v z) v (u v x)=u v x. given clause #223: (wt=15) 1405 [para_from,1103,1047,demod,643,1104] c((x v c(y)) v z) v (u v y)=u v y. given clause #224: (wt=15) 1413 [para_into,1107,1107,demod,643,1108] c(x v (y v c(z))) v (z v u)=z v u. given clause #225: (wt=15) 1415 [para_into,1107,1103,demod,643,1104] c(x v (y v c(z))) v (u v z)=u v z. given clause #226: (wt=23) 1161 [para_into,892,1051,demod,643,643,643,643] (c(x v c(y v (z v u))) v z) v (y v (z v u))=y v (z v u). given clause #227: (wt=15) 1417 [para_into,1107,1047,demod,643,1048] c(x v (c(y) v z)) v (y v u)=y v u. given clause #228: (wt=15) 1419 [para_into,1107,1043,demod,643,1044] c(x v (c(y) v z)) v (u v y)=u v y. given clause #229: (wt=15) 1423 [para_from,1107,1047,demod,643,1108] c((x v c(y)) v z) v (y v u)=y v u. given clause #230: (wt=15) 1439 [para_into,1127,1127,demod,643,1128] (x v y) v c((c(y) v z) v u)=x v y. given clause #231: (wt=23) 1163 [para_into,892,1041,demod,643,643,643,643] (c(x v c((y v z) v u)) v z) v ((y v z) v u)= (y v z) v u. given clause #232: (wt=15) 1507 [para_into,1131,1107,demod,643,1108] (x v y) v c((z v c(x)) v u)=x v y. given clause #233: (wt=15) 1509 [para_into,1131,1103,demod,643,1104] (x v y) v c((z v c(y)) v u)=x v y. given clause #234: (wt=15) 1511 [para_into,1131,1047,demod,643,1048] (x v y) v c((c(x) v z) v u)=x v y. given clause #235: (wt=15) 1529 [para_into,1183,1183,demod,643,1184] (x v y) v c(z v (u v c(y)))=x v y. given clause #236: (wt=23) 1165 [para_into,892,1035,demod,643,643,643,643] (c(x v c((y v z) v u)) v y) v ((y v z) v u)= (y v z) v u. given clause #237: (wt=15) 1537 [para_into,1183,1131,demod,643,1132] (x v y) v c(z v (c(x) v u))=x v y. given clause #238: (wt=15) 1539 [para_into,1183,1127,demod,643,1128] (x v y) v c(z v (c(y) v u))=x v y. given clause #239: (wt=15) 1551 [para_into,1187,1107,demod,643,1108] (x v y) v c(z v (u v c(x)))=x v y. given clause #240: (wt=15) 1579 [para_into,1015,957] (c(x v y) v c(x v z)) v c(x)=c(x). given clause #241: (wt=17) 1167 [para_into,892,822,demod,643] (c(x v c(y v z)) v z) v (y v z)=y v z. given clause #242: (wt=15) 1593 [para_into,1015,838] (c(x v y) v c(z v y)) v c(y)=c(y). given clause #243: (wt=15) 1609 [para_from,1015,957,demod,1016] c(x) v (c(y v x) v c(x v z))=c(x). given clause #244: (wt=15) 1615 [back_demod,1065,demod,1614,643] c(c(x v y) v x) v c(x v y)=c(x). given clause #245: (wt=13) 7188 [para_into,1615,1615,demod,643,643] x v c(c(x v y) v x)=x v y. given clause #246: (wt=17) 1169 [para_into,892,718,demod,643] (c(x v c(y v z)) v y) v (y v z)=y v z. given clause #247: (wt=11) 7372 [para_into,1169,937,demod,643] (x v y) v (y v x)=y v x. given clause #248: (wt=7) 7594 [para_from,7372,957,demod,7373,7373] x v y=y v x. ----> UNIT CONFLICT at 2.11 sec ----> 7611 [binary,7609,4] $Ans(OM_rewritten). Length of proof is 71. Level of proof is 21. ---------------- PROOF ---------------- 4 [] A v c(A v c(A v B))!=A v B|$Ans(OM_rewritten). 7 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z)))=y. 9 [] x v y=f(f(x,x),f(y,y)). 10 [copy,9,flip.1] f(f(x,x),f(y,y))=x v y. 12 [] x^y=f(f(x,y),f(x,y)). 13 [copy,12,flip.1] f(f(x,y),f(x,y))=x^y. 15 [] c(x)=f(x,x). 17,16 [copy,15,flip.1] f(x,x)=c(x). 19,18 [back_demod,13,demod,17] c(f(x,y))=x^y. 20 [back_demod,10,demod,17,17] f(c(x),c(y))=x v y. 22 [back_demod,7,demod,17] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z)))=y. 30,29 [para_into,20,16] c(c(x))=x v x. 34 [para_from,20,18,flip.1] c(x)^c(y)=c(x v y). 37,36 [para_into,29,29] c(x v x)=c(x) v c(x). 40 [para_from,29,20] f(c(x),y v y)=x v c(y). 43,42 [para_from,29,20] f(x v x,c(y))=c(x) v y. 46 [para_into,22,16] f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y)))=x. 48 [para_into,22,20,demod,30,43] f(f(f(f(x,c(y)),y v z),u),f(c(y),f(f(c(z),c(y) v z),c(z))))=c(y). 50 [para_into,22,16] f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y)))=y. 52 [para_into,22,22] f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z))))=x. 54 [para_into,22,16,demod,17,30] f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x)))=x. 70 [para_into,34,29] (x v x)^c(y)=c(c(x) v y). 83,82 [para_into,40,29] f(x v x,y v y)=c(x) v c(y). 90 [para_from,40,22,demod,37] f(f(f(x v c(y),f(y v y,z)),u),f(y v y,f(f(z,f(c(y) v c(y),z)),z)))=y v y. 136 [para_into,70,29] (x v x)^ (y v y)=c(c(x) v c(y)). 158 [para_into,46,42,demod,37,37,43,30] f(f(f(c(x) v c(x),c(x) v y),z),f(x v x,f(f(c(y),(x v x) v y),c(y))))=x v x. 234 [para_into,48,16,demod,19] f(f(x,c(y))^ (y v z),f(c(y),f(f(c(z),c(y) v z),c(z))))=c(y). 306 [para_into,50,40,demod,37,37,83,30] f(f(f(x v c(y),c(y) v c(y)),z),f(y v y,f(f(y v y,(y v y) v c(y)),y v y)))=y v y. 398 [para_from,52,46] f(c(x),f(x,f(f(y,f(c(x),y)),y)))=x. 403,402 [para_from,52,22] f(f(x,y),f(y,f(f(z,f(c(y),z)),z)))=y. 451,450 [para_into,398,398,demod,403,17,17,30] x v x=x. 456 [para_into,398,20] f(c(x),f(x,f(f(c(y),x v y),c(y))))=x. 536 [back_demod,306,demod,451,451,451,451,451,451] f(f(f(x v c(y),c(y)),z),f(y,f(f(y,y v c(y)),y)))=y. 600 [back_demod,158,demod,451,451,451,451] f(f(f(c(x),c(x) v y),z),f(x,f(f(c(y),x v y),c(y))))=x. 603,602 [back_demod,136,demod,451,451] x^y=c(c(x) v c(y)). 623 [back_demod,90,demod,451,451,451,451] f(f(f(x v c(y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z)))=y. 632,631 [back_demod,82,demod,451,451] f(x,y)=c(x) v c(y). 638 [back_demod,54,demod,451,632,632,30,451,632,632,632,632] c(c(x) v c(y)) v c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 643,642 [back_demod,29,demod,451] c(c(x))=x. 654 [back_demod,234,demod,632,643,603,632,643,632,643,632,643,632,643] (c(c(x) v y) v c(y v z)) v c(y v c(c(z v c(c(y) v z)) v z))=c(y). 666 [back_demod,623,demod,632,632,632,632,643,632,632,632,632] c(c(c(x v c(y)) v c(c(y) v c(z))) v c(u)) v c(c(y) v c(c(c(z) v c(y v c(z))) v c(z)))=y. 672 [back_demod,600,demod,632,643,632,632,643,632,643,632,632] c(c(x v c(c(x) v y)) v c(z)) v c(c(x) v c(c(y v c(x v y)) v y))=x. 674 [back_demod,536,demod,632,643,632,632,632,632,632] c(c(c(x v c(y)) v y) v c(z)) v c(c(y) v c(c(c(y) v c(y v c(y))) v c(y)))=y. 682 [back_demod,456,demod,632,643,632,643,632,632,643] x v c(c(x) v c(c(y v c(x v y)) v y))=x. 706 [para_into,638,642] c(c(x) v y) v c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 709,708 [para_into,638,450] c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 712 [back_demod,706,demod,709] c(c(x) v y) v x=x. 714 [back_demod,674,demod,709] c(c(c(x v c(y)) v y) v c(z)) v y=y. 719,718 [para_into,712,642] c(x v y) v c(x)=c(x). 724 [para_into,718,718,demod,643,643,643] x v (x v y)=x v y. 728 [para_from,724,682] x v c(c(x) v c(c((x v y) v c(x v y)) v (x v y)))=x. 738 [para_into,654,718,demod,643,643,643] (x v c(c(x) v y)) v c(c(x) v c(c(y v c(x v y)) v y))=x. 800 [para_into,666,682,demod,643] (c(x v c(y)) v c(c(y) v c(z))) v c(c(y) v c(c(c(z) v c(y v c(z))) v c(z)))=y. 809,808 [para_into,714,718,demod,643] c(x v c(y)) v y=y. 818 [back_demod,728,demod,809] x v c(c(x) v c(x v y))=x. 822 [para_into,808,642] c(x v y) v c(y)=c(y). 838 [para_from,822,712,demod,643] x v (y v x)=y v x. 877,876 [para_into,672,808] c(c(x) v c(c(y v c(x v y)) v y))=x. 892 [back_demod,800,demod,877] (c(x v c(y)) v c(c(y) v c(z))) v y=y. 909,908 [back_demod,738,demod,877] (x v c(c(x) v y)) v x=x. 913,912 [para_into,908,838] (x v c(y v c(x))) v x=x. 919,918 [para_from,908,718] c(x) v c(x v c(c(x) v y))=c(x v c(c(x) v y)). 925,924 [para_into,818,642,demod,919] c(x v c(c(x) v y))=c(x). 926 [para_into,818,912,demod,719,643,913,flip.1] x v c(y v c(x))=x. 928 [para_into,818,908,demod,925,451,643,909,flip.1] x v c(c(x) v y)=x. 937 [para_into,926,642] c(x) v c(y v x)=c(x). 955 [para_into,928,822,demod,643] (x v y) v y=x v y. 958,957 [para_into,928,718,demod,643] (x v y) v x=x v y. 1063 [para_into,876,955] c(c(x v y) v c(c(y v c(x v y)) v y))=x v y. 1168,1167 [para_into,892,822,demod,643] (c(x v c(y v z)) v z) v (y v z)=y v z. 1169 [para_into,892,718,demod,643] (c(x v c(y v z)) v y) v (y v z)=y v z. 2405 [para_from,1063,937,demod,643,1168,643,flip.1] c(x v c(y v x)) v x=y v x. 2511 [para_into,2405,957,demod,958] c(x v c(x v y)) v x=x v y. 7373,7372 [para_into,1169,937,demod,643] (x v y) v (y v x)=y v x. 7594 [para_from,7372,957,demod,7373,7373] x v y=y v x. 7609 [para_into,7594,2511,flip.1] x v c(x v c(x v y))=x v y. 7611 [binary,7609,4] $Ans(OM_rewritten). ------------ end of proof ------------- given clause #249: (wt=13) 7306 [para_into,7188,838,demod,839] x v c(c(y v x) v x)=y v x. given clause #250: (wt=13) 7566 [para_from,7372,2669,demod,2802] c(x v y) v (y v x)=x v c(x). given clause #251: (wt=18) 1175 [para_into,1117,1085] (x v (y v c(z))) v c(u v z)=x v (y v c(z)). given clause #252: (wt=13) 7568 [para_from,7372,2528,demod,2802] (x v y) v c(y v x)=y v c(y). given clause #253: (wt=13) 7607 [para_into,7594,7188,flip.1] c(c(x v y) v x) v x=x v y. given clause #254: (wt=13) 7609 [para_into,7594,2511,flip.1] x v c(x v c(x v y))=x v y. given clause #255: (wt=13) 7612 [para_into,7594,2405,flip.1] x v c(x v c(y v x))=y v x. given clause #256: (wt=18) 1177 [para_into,1117,1051] (x v (c(y) v z)) v c(u v y)=x v (c(y) v z). given clause #257: (wt=13) 7626 [para_from,7594,2405] c(c(x v y) v y) v y=x v y. given clause #258: (wt=14) 7558 [para_from,7372,1015,demod,7555] c(x v y) v c(y v x)=c(y v x). given clause #259: (wt=15) 1749 [para_into,1313,1265] c((x v (y v (z v c(u)))) v v) v u=u. given clause #260: (wt=15) 1751 [para_into,1313,1255] c((x v (y v (c(z) v u))) v v) v z=z. given clause #261: (wt=18) 1179 [para_into,1117,1041] ((x v c(y)) v z) v c(u v y)= (x v c(y)) v z. given clause #262: (wt=15) 1753 [para_into,1313,1241] c((x v ((y v c(z)) v u)) v v) v z=z. given clause #263: (wt=15) 1755 [para_into,1313,1199] c((x v ((c(y) v z) v u)) v v) v y=y. given clause #264: (wt=15) 1771 [para_into,1313,1241] c(((x v (y v c(z))) v u) v v) v z=z. given clause #265: (wt=15) 1773 [para_into,1313,1199] c((((x v c(y)) v z) v u) v v) v y=y. given clause #266: (wt=18) 1181 [para_into,1117,1035] ((c(x) v y) v z) v c(u v x)= (c(x) v y) v z. given clause #267: (wt=15) 1775 [para_into,1313,1267] c(x v (y v (z v (u v c(v))))) v v=v. given clause #268: (wt=15) 1777 [para_into,1313,1257] c(x v ((y v (z v c(u))) v v)) v u=u. given clause #269: (wt=15) 1801 [para_from,1313,1187,demod,643,1314] x v c(y v ((z v (u v c(x))) v v))=x. given clause #270: (wt=15) 1803 [para_from,1313,1131,demod,643,1314] x v c(((y v (z v c(x))) v u) v v)=x. given clause #271: (wt=17) 1193 [para_into,1037,1037,demod,643,643] c(c(x) v y) v ((x v z) v u)= (x v z) v u. given clause #272: (wt=15) 1827 [para_into,1317,1241] c(((x v (c(y) v z)) v u) v v) v y=y. given clause #273: (wt=15) 1829 [para_into,1317,1199] c((((c(x) v y) v z) v u) v v) v x=x. given clause #274: (wt=15) 1831 [para_into,1317,1267] c(x v (y v (z v (c(u) v v)))) v u=u. given clause #275: (wt=15) 1833 [para_into,1317,1257] c(x v ((y v (c(z) v u)) v v)) v z=z. given clause #276: (wt=17) 1195 [para_from,1037,1117] ((x v y) v z) v c(u v c(x))= (x v y) v z. given clause #277: (wt=15) 1857 [para_from,1317,1187,demod,643,1318] x v c(y v ((z v (c(x) v u)) v v))=x. given clause #278: (wt=15) 1859 [para_from,1317,1131,demod,643,1318] x v c(((y v (c(x) v z)) v u) v v)=x. given clause #279: (wt=15) 1875 [para_into,1319,1267] c(x v (y v ((z v c(u)) v v))) v u=u. given clause #280: (wt=15) 1877 [para_into,1319,1257] c(x v (((y v c(z)) v u) v v)) v z=z. given clause #281: (wt=17) 1197 [para_from,1037,1057] ((x v y) v z) v c(c(x) v u)= (x v y) v z. given clause #282: (wt=15) 1901 [para_from,1319,1187,demod,643,1320] x v c(y v (((z v c(x)) v u) v v))=x. given clause #283: (wt=15) 1903 [para_from,1319,1131,demod,643,1320] x v c((((y v c(x)) v z) v u) v v)=x. given clause #284: (wt=15) 1919 [para_into,1321,1267] c(x v (y v ((c(z) v u) v v))) v z=z. given clause #285: (wt=15) 1921 [para_into,1321,1257] c(x v (((c(y) v z) v u) v v)) v y=y. given clause #286: (wt=17) 1203 [para_from,1037,1051] c(x v c(y)) v ((y v z) v u)= (y v z) v u. given clause #287: (wt=15) 1941 [para_from,1321,1187,demod,643,1322] x v c(y v (((c(x) v z) v u) v v))=x. given clause #288: (wt=15) 1943 [para_from,1321,1131,demod,643,1322] x v c((((c(x) v y) v z) v u) v v)=x. given clause #289: (wt=15) 1999 [para_from,1393,1187,demod,643,1394] x v c(y v (z v (u v (v v c(x)))))=x. given clause #290: (wt=15) 2001 [para_from,1393,1131,demod,643,1394] x v c((y v (z v (u v c(x)))) v v)=x. given clause #291: (wt=20) 1213 [para_into,894,957] c(c(c(c(x) v y) v c(c(x) v c(z))) v u) v x=x. given clause #292: (wt=15) 2061 [para_from,1397,1187,demod,643,1398] x v c(y v (z v (u v (c(x) v v))))=x. given clause #293: (wt=15) 2063 [para_from,1397,1131,demod,643,1398] x v c((y v (z v (c(x) v u))) v v)=x. given clause #294: (wt=15) 2123 [para_from,1399,1187,demod,643,1400] x v c(y v (z v ((u v c(x)) v v)))=x. given clause #295: (wt=15) 2125 [para_from,1399,1131,demod,643,1400] x v c((y v ((z v c(x)) v u)) v v)=x. given clause #296: (wt=19) 1219 [para_into,894,642] c(c(c(x v c(y)) v c(c(y) v z)) v u) v y=y. given clause #297: (wt=15) 2179 [para_from,1401,1187,demod,643,1402] x v c(y v (z v ((c(x) v u) v v)))=x. given clause #298: (wt=15) 2181 [para_from,1401,1131,demod,643,1402] x v c((y v ((c(x) v z) v u)) v v)=x. given clause #299: (wt=15) 2513 [para_into,2405,937,demod,643,938] c(c(x v y) v y) v c(x v y)=c(y). given clause #300: (wt=15) 2804 [para_into,2528,1321,demod,643,643,2697,2802,2802,643] x v (((c(x) v y) v z) v u)=c(x) v x. given clause #301: (wt=27) 1221 [para_into,894,1085,demod,643,643,643,643] c(c(c(x v c(y v (z v u))) v u) v v) v (y v (z v u))=y v (z v u). given clause #302: (wt=15) 2810 [para_into,2528,1087,demod,643,643,2697] ((x v c(y)) v z) v (y v u)=y v c(y). given clause #303: (wt=15) 2819 [para_into,2528,1039,demod,643,643,2697] ((c(x) v y) v z) v (x v u)=x v c(x). given clause #304: (wt=15) 2912 [para_into,2669,1321,demod,643,643,2697,2802,2802,643] (((c(x) v y) v z) v u) v x=c(x) v x. given clause #305: (wt=15) 2927 [para_into,2669,1087,demod,643,643,2697] (x v y) v ((z v c(x)) v u)=x v c(x). given clause #306: (wt=27) 1223 [para_into,894,1051,demod,643,643,643,643] c(c(c(x v c(y v (z v u))) v z) v v) v (y v (z v u))=y v (z v u). given clause #307: (wt=15) 2933 [para_into,2669,1039,demod,643,643,2697] (x v y) v ((c(x) v z) v u)=x v c(x). given clause #308: (wt=15) 2948 [back_demod,2644,demod,2922,2802,643,flip.1] x v ((y v (c(x) v z)) v u)=c(x) v x. given clause #309: (wt=15) 3016 [para_from,1111,2833,demod,2802] (x v y) v (z v (c(x) v u))=x v c(x). given clause #310: (wt=15) 3018 [para_from,1111,2532,demod,2697] (x v (c(y) v z)) v (y v u)=y v c(y). given clause #311: (wt=27) 1225 [para_into,894,1041,demod,643,643,643,643] c(c(c(x v c((y v z) v u)) v z) v v) v ((y v z) v u)= (y v z) v u. given clause #312: (wt=15) 3063 [para_into,2515,1267] ((x v (y v c(z))) v u) v z=c(z) v z. given clause #313: (wt=15) 3065 [para_into,2515,1257] ((x v (c(y) v z)) v u) v y=c(y) v y. given clause #314: (wt=15) 3067 [para_into,2515,1243] (((x v c(y)) v z) v u) v y=c(y) v y. given clause #315: (wt=15) 3086 [para_into,2515,1037,demod,2697,2802] (c(x) v y) v ((x v z) v u)=x v c(x). given clause #316: (wt=27) 1227 [para_into,894,1037,demod,643] c(c(c(x v c((y v z) v u)) v y) v v) v ((y v z) v u)= (y v z) v u. given clause #317: (wt=15) 3090 [para_into,2515,1267] (x v (y v (c(z) v u))) v z=c(z) v z. given clause #318: (wt=15) 3092 [para_into,2515,1257] (x v ((c(y) v z) v u)) v y=c(y) v y. given clause #319: (wt=15) 3112 [para_into,2517,1267] (x v (y v (z v c(u)))) v u=c(u) v u. given clause #320: (wt=15) 3114 [para_into,2517,1257] (x v ((y v c(z)) v u)) v z=c(z) v z. given clause #321: (wt=21) 1229 [para_into,894,822,demod,643] c(c(c(x v c(y v z)) v z) v u) v (y v z)=y v z. given clause #322: (wt=15) 3143 [para_into,2519,1045,demod,2697] (x v (y v c(z))) v (z v u)=z v c(z). given clause #323: (wt=15) 3149 [para_into,2519,1037,demod,2697,2802] (x v c(y)) v ((y v z) v u)=y v c(y). given clause #324: (wt=15) 3151 [para_into,2519,1035,demod,2697,2802,643] (x v y) v ((c(y) v z) v u)=c(y) v y. given clause #325: (wt=15) 3228 [para_into,1121,2517,demod,643,2802,643,flip.1] (x v (y v z)) v (c(y) v u)=y v c(y). given clause #326: (wt=21) 1231 [para_into,894,718,demod,643] c(c(c(x v c(y v z)) v y) v u) v (y v z)=y v z. given clause #327: (wt=15) 3230 [para_into,1121,2515,demod,643,2802,643,flip.1] ((x v y) v z) v (c(x) v u)=x v c(x). given clause #328: (wt=15) 3238 [para_into,2607,1265] (x v (y v (z v u))) v c(u)=u v c(u). given clause #329: (wt=15) 3240 [para_into,2607,1255] (x v (y v (z v u))) v c(z)=z v c(z). given clause #330: (wt=15) 3242 [para_into,2607,1241] (x v ((y v z) v u)) v c(z)=z v c(z). given clause #331: (wt=17) 1235 [para_from,1083,1117] ((x v y) v z) v c(u v c(y))= (x v y) v z. given clause #332: (wt=15) 3244 [para_into,2607,1199] (x v ((y v z) v u)) v c(y)=y v c(y). given clause #333: (wt=15) 3246 [para_into,2607,1241] ((x v (y v z)) v u) v c(z)=z v c(z). given clause #334: (wt=15) 3248 [para_into,2607,1199] (((x v y) v z) v u) v c(y)=y v c(y). given clause #335: (wt=15) 3252 [para_into,2609,1241] ((x v (y v z)) v u) v c(y)=y v c(y). given clause #336: (wt=17) 1237 [para_from,1083,1057] ((x v y) v z) v c(c(y) v u)= (x v y) v z. given clause #337: (wt=15) 3254 [para_into,2609,1199] (((x v y) v z) v u) v c(x)=x v c(x). given clause #338: (wt=15) 3310 [para_into,1123,2607,demod,2802,flip.1] (x v c(y)) v (z v (y v u))=y v c(y). given clause #339: (wt=15) 3339 [para_into,2813,1037,demod,2802,2802] c(x) v (((x v y) v z) v u)=x v c(x). given clause #340: (wt=15) 3352 [para_into,2813,1267] (c(x) v y) v (z v (u v x))=x v c(x). given clause #341: (wt=17) 1239 [para_from,1083,1035] c(c(x) v y) v ((z v x) v u)= (z v x) v u. given clause #342: (wt=15) 3354 [para_into,2813,1257] (c(x) v y) v (z v (x v u))=x v c(x). given clause #343: (wt=15) 3356 [para_into,2813,1243] (c(x) v y) v ((z v x) v u)=x v c(x). given clause #344: (wt=15) 3368 [para_into,2813,1045,demod,643,643,2697] ((x v y) v z) v (u v c(x))=x v c(x). given clause #345: (wt=15) 3370 [para_into,2813,1043,demod,643,643,2697,643] ((c(x) v y) v z) v (u v x)=c(x) v x. given clause #346: (wt=17) 1245 [para_from,1083,1051] c(x v c(y)) v ((z v y) v u)= (z v y) v u. given clause #347: (wt=15) 3411 [para_into,2816,1267] (x v c(y)) v (z v (u v y))=y v c(y). given clause #348: (wt=15) 3413 [para_into,2816,1243] (x v c(y)) v ((z v y) v u)=y v c(y). given clause #349: (wt=15) 3425 [para_into,2816,1045,demod,643,643,2697] (x v (y v z)) v (u v c(y))=y v c(y). given clause #350: (wt=15) 3427 [para_into,2816,1043,demod,643,643,2697,643] (x v (c(y) v z)) v (u v y)=c(y) v y. given clause #351: (wt=17) 1247 [para_into,1095,1095,demod,643,643] c(x v c(y)) v (z v (y v u))=z v (y v u). given clause #352: (wt=15) 3450 [para_into,2821,1267] c(x) v ((y v (z v x)) v u)=x v c(x). given clause #353: (wt=15) 3452 [para_into,2821,1257] c(x) v ((y v (x v z)) v u)=x v c(x). given clause #354: (wt=15) 3454 [para_into,2821,1243] c(x) v (((y v x) v z) v u)=x v c(x). given clause #355: (wt=15) 3467 [para_into,2821,1267] c(x) v (y v (z v (x v u)))=x v c(x). given clause #356: (wt=17) 1249 [para_from,1095,1117] (x v (y v z)) v c(u v c(y))=x v (y v z). given clause #357: (wt=15) 3469 [para_into,2821,1257] c(x) v (y v ((x v z) v u))=x v c(x). given clause #358: (wt=15) 3528 [para_into,2823,1267] x v ((y v (z v c(x))) v u)=c(x) v x. given clause #359: (wt=15) 3530 [para_into,2823,1243] x v (((y v c(x)) v z) v u)=c(x) v x. given clause #360: (wt=15) 3533 [para_into,2823,1257] x v (y v ((c(x) v z) v u))=c(x) v x. given clause #361: (wt=17) 1251 [para_from,1095,1057] (x v (y v z)) v c(c(y) v u)=x v (y v z). given clause #362: (wt=15) 3536 [para_into,2846,1265] (x v (y v z)) v (c(z) v u)=z v c(z). given clause #363: (wt=15) 3538 [para_into,2846,1241] ((x v y) v z) v (c(y) v u)=y v c(y). given clause #364: (wt=15) 3540 [para_into,2846,1267] (x v y) v (z v (u v c(y)))=y v c(y). given clause #365: (wt=15) 3542 [para_into,2846,1257] (x v y) v (z v (c(y) v u))=y v c(y). given clause #366: (wt=17) 1253 [para_from,1095,1035] c(c(x) v y) v (z v (x v u))=z v (x v u). given clause #367: (wt=15) 3544 [para_into,2846,1243] (x v y) v ((z v c(y)) v u)=y v c(y). given clause #368: (wt=15) 3546 [para_into,2848,1267] (x v y) v (z v (u v c(x)))=x v c(x). given clause #369: (wt=15) 3557 [para_into,2917,1265] c(x) v (y v (z v (u v x)))=x v c(x). given clause #370: (wt=15) 3559 [para_into,2917,1241] c(x) v (y v ((z v x) v u))=x v c(x). given clause #371: (wt=17) 1259 [para_from,1135,1117] (x v (y v z)) v c(u v c(z))=x v (y v z). given clause #372: (wt=15) 3603 [para_into,2929,1267] (x v (y v z)) v (u v c(z))=z v c(z). given clause #373: (wt=15) 3605 [para_into,2929,1243] ((x v y) v z) v (u v c(y))=y v c(y). given clause #374: (wt=15) 3636 [para_into,2931,1267] (x v (y v c(z))) v (u v z)=c(z) v z. given clause #375: (wt=15) 3638 [para_into,2931,1243] ((x v c(y)) v z) v (u v y)=c(y) v y. given clause #376: (wt=17) 1261 [para_from,1135,1057] (x v (y v z)) v c(c(z) v u)=x v (y v z). given clause #377: (wt=15) 3644 [para_into,2976,1265] x v (y v (z v (u v c(x))))=x v c(x). given clause #378: (wt=15) 3646 [para_into,2976,1255] x v (y v (z v (c(x) v u)))=x v c(x). given clause #379: (wt=15) 3648 [para_into,2976,1241] x v (y v ((z v c(x)) v u))=x v c(x). given clause #380: (wt=15) 4348 [para_into,1151,642] (c(c(x) v y) v c(c(x) v z)) v x=x. given clause #381: (wt=17) 1263 [para_from,1135,1035] c(c(x) v y) v (z v (u v x))=z v (u v x). given clause #382: (wt=15) 4418 [para_into,1157,838] (c(x v c(y)) v c(z v c(y))) v y=y. given clause #383: (wt=15) 4474 [para_from,1157,957,demod,1158] x v (c(y v c(x)) v c(c(x) v z))=x. given clause #384: (wt=15) 4760 [para_into,1159,953,demod,643] (x v y) v (x v (z v y))=x v (z v y). given clause #385: (wt=13) 17819 [para_into,4760,2978,demod,2802,flip.1] x v (c(x v y) v y)=x v c(x). given clause #386: (wt=17) 1269 [para_from,1135,1051] c(x v c(y)) v (z v (u v y))=z v (u v y). given clause #387: (wt=13) 18019 [para_into,17819,7594] x v (c(y v x) v y)=x v c(x). given clause #388: (wt=13) 18021 [para_into,17819,7594] x v (y v c(x v y))=x v c(x). given clause #389: (wt=13) 18023 [para_into,17819,7594] (c(x v y) v y) v x=x v c(x). given clause #390: (wt=13) 18031 [para_into,18019,18019,demod,2658,2802,643,2697] (c(x v y) v x) v y=x v c(x). given clause #391: (wt=40) 1289 [para_into,969,969] c(c(c(x) v c(y v z)) v c(u)) v (c(z v c(c(y v z) v v)) v c(x))=c(z v c(c(y v z) v v)) v c(x). given clause #392: (wt=13) 18033 [para_into,18019,7594] x v (y v c(y v x))=x v c(x). given clause #393: (wt=13) 18037 [para_into,18021,7594] (x v c(y v x)) v y=y v c(y). given clause #394: (wt=13) 18043 [para_into,18031,7594] (x v c(x v y)) v y=x v c(x). given clause #395: (wt=15) 5286 [para_into,1161,1191,demod,643] (x v y) v (z v (y v x))=z v (y v x). given clause #396: (wt=21) 1295 [para_into,969,642] c(c(x v c(c(y v x) v z)) v u) v (y v x)=y v x. given clause #397: (wt=15) 5312 [para_into,1161,953,demod,643] (x v y) v (x v (y v z))=x v (y v z). given clause #398: (wt=15) 5738 [para_into,1163,937,demod,643] (x v y) v ((z v y) v x)= (z v y) v x. given clause #399: (wt=15) 6088 [para_into,1165,1171,demod,643] (x v y) v ((y v x) v z)= (y v x) v z. given clause #400: (wt=15) 6102 [para_into,1165,937,demod,643] (x v y) v ((y v z) v x)= (y v z) v x. given clause #401: (wt=17) 1297 [para_into,969,1147,demod,643] (x v c(c(y v x) v z)) v (y v x)=y v x. given clause #402: (wt=13) 19779 [back_demod,19351,demod,19774] (x v y) v (z v y)= (z v y) v x. given clause #403: (wt=11) 20466 [back_demod,19780,demod,20410] (x v y) v z= (z v y) v x. given clause #404: (wt=11) 20648 [back_demod,20422,demod,20614] (x v y) v z= (y v z) v x. ----> UNIT CONFLICT at 18.02 sec ----> 22050 [binary,22049,1] $Ans(AJ). Length of proof is 98. Level of proof is 26. ---------------- PROOF ---------------- 1 [] A v (B v C)!=B v (A v C)|$Ans(AJ). 7 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z)))=y. 9 [] x v y=f(f(x,x),f(y,y)). 10 [copy,9,flip.1] f(f(x,x),f(y,y))=x v y. 12 [] x^y=f(f(x,y),f(x,y)). 13 [copy,12,flip.1] f(f(x,y),f(x,y))=x^y. 15 [] c(x)=f(x,x). 17,16 [copy,15,flip.1] f(x,x)=c(x). 19,18 [back_demod,13,demod,17] c(f(x,y))=x^y. 20 [back_demod,10,demod,17,17] f(c(x),c(y))=x v y. 22 [back_demod,7,demod,17] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z)))=y. 30,29 [para_into,20,16] c(c(x))=x v x. 34 [para_from,20,18,flip.1] c(x)^c(y)=c(x v y). 37,36 [para_into,29,29] c(x v x)=c(x) v c(x). 40 [para_from,29,20] f(c(x),y v y)=x v c(y). 43,42 [para_from,29,20] f(x v x,c(y))=c(x) v y. 46 [para_into,22,16] f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y)))=x. 48 [para_into,22,20,demod,30,43] f(f(f(f(x,c(y)),y v z),u),f(c(y),f(f(c(z),c(y) v z),c(z))))=c(y). 50 [para_into,22,16] f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y)))=y. 52 [para_into,22,22] f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z))))=x. 54 [para_into,22,16,demod,17,30] f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x)))=x. 70 [para_into,34,29] (x v x)^c(y)=c(c(x) v y). 83,82 [para_into,40,29] f(x v x,y v y)=c(x) v c(y). 90 [para_from,40,22,demod,37] f(f(f(x v c(y),f(y v y,z)),u),f(y v y,f(f(z,f(c(y) v c(y),z)),z)))=y v y. 136 [para_into,70,29] (x v x)^ (y v y)=c(c(x) v c(y)). 158 [para_into,46,42,demod,37,37,43,30] f(f(f(c(x) v c(x),c(x) v y),z),f(x v x,f(f(c(y),(x v x) v y),c(y))))=x v x. 234 [para_into,48,16,demod,19] f(f(x,c(y))^ (y v z),f(c(y),f(f(c(z),c(y) v z),c(z))))=c(y). 306 [para_into,50,40,demod,37,37,83,30] f(f(f(x v c(y),c(y) v c(y)),z),f(y v y,f(f(y v y,(y v y) v c(y)),y v y)))=y v y. 398 [para_from,52,46] f(c(x),f(x,f(f(y,f(c(x),y)),y)))=x. 403,402 [para_from,52,22] f(f(x,y),f(y,f(f(z,f(c(y),z)),z)))=y. 451,450 [para_into,398,398,demod,403,17,17,30] x v x=x. 456 [para_into,398,20] f(c(x),f(x,f(f(c(y),x v y),c(y))))=x. 536 [back_demod,306,demod,451,451,451,451,451,451] f(f(f(x v c(y),c(y)),z),f(y,f(f(y,y v c(y)),y)))=y. 600 [back_demod,158,demod,451,451,451,451] f(f(f(c(x),c(x) v y),z),f(x,f(f(c(y),x v y),c(y))))=x. 603,602 [back_demod,136,demod,451,451] x^y=c(c(x) v c(y)). 623 [back_demod,90,demod,451,451,451,451] f(f(f(x v c(y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z)))=y. 632,631 [back_demod,82,demod,451,451] f(x,y)=c(x) v c(y). 638 [back_demod,54,demod,451,632,632,30,451,632,632,632,632] c(c(x) v c(y)) v c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 643,642 [back_demod,29,demod,451] c(c(x))=x. 654 [back_demod,234,demod,632,643,603,632,643,632,643,632,643,632,643] (c(c(x) v y) v c(y v z)) v c(y v c(c(z v c(c(y) v z)) v z))=c(y). 666 [back_demod,623,demod,632,632,632,632,643,632,632,632,632] c(c(c(x v c(y)) v c(c(y) v c(z))) v c(u)) v c(c(y) v c(c(c(z) v c(y v c(z))) v c(z)))=y. 672 [back_demod,600,demod,632,643,632,632,643,632,643,632,632] c(c(x v c(c(x) v y)) v c(z)) v c(c(x) v c(c(y v c(x v y)) v y))=x. 674 [back_demod,536,demod,632,643,632,632,632,632,632] c(c(c(x v c(y)) v y) v c(z)) v c(c(y) v c(c(c(y) v c(y v c(y))) v c(y)))=y. 682 [back_demod,456,demod,632,643,632,643,632,632,643] x v c(c(x) v c(c(y v c(x v y)) v y))=x. 706 [para_into,638,642] c(c(x) v y) v c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 709,708 [para_into,638,450] c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 712 [back_demod,706,demod,709] c(c(x) v y) v x=x. 714 [back_demod,674,demod,709] c(c(c(x v c(y)) v y) v c(z)) v y=y. 719,718 [para_into,712,642] c(x v y) v c(x)=c(x). 724 [para_into,718,718,demod,643,643,643] x v (x v y)=x v y. 728 [para_from,724,682] x v c(c(x) v c(c((x v y) v c(x v y)) v (x v y)))=x. 738 [para_into,654,718,demod,643,643,643] (x v c(c(x) v y)) v c(c(x) v c(c(y v c(x v y)) v y))=x. 794 [para_into,666,718,demod,643] c((c(x) v c(y)) v c(z)) v c(c(x) v c(c(c(y) v c(x v c(y))) v c(y)))=x. 800 [para_into,666,682,demod,643] (c(x v c(y)) v c(c(y) v c(z))) v c(c(y) v c(c(c(z) v c(y v c(z))) v c(z)))=y. 809,808 [para_into,714,718,demod,643] c(x v c(y)) v y=y. 818 [back_demod,728,demod,809] x v c(c(x) v c(x v y))=x. 822 [para_into,808,642] c(x v y) v c(y)=c(y). 839,838 [para_from,822,712,demod,643] x v (y v x)=y v x. 877,876 [para_into,672,808] c(c(x) v c(c(y v c(x v y)) v y))=x. 892 [back_demod,800,demod,877] (c(x v c(y)) v c(c(y) v c(z))) v y=y. 896 [back_demod,794,demod,877] c((c(x) v c(y)) v c(z)) v x=x. 909,908 [back_demod,738,demod,877] (x v c(c(x) v y)) v x=x. 913,912 [para_into,908,838] (x v c(y v c(x))) v x=x. 919,918 [para_from,908,718] c(x) v c(x v c(c(x) v y))=c(x v c(c(x) v y)). 925,924 [para_into,818,642,demod,919] c(x v c(c(x) v y))=c(x). 926 [para_into,818,912,demod,719,643,913,flip.1] x v c(y v c(x))=x. 928 [para_into,818,908,demod,925,451,643,909,flip.1] x v c(c(x) v y)=x. 937 [para_into,926,642] c(x) v c(y v x)=c(x). 953 [para_into,928,642] c(x) v c(x v y)=c(x). 957 [para_into,928,718,demod,643] (x v y) v x=x v y. 1017 [para_into,896,642] c((c(x) v y) v c(z)) v x=x. 1035 [para_into,1017,642] c((c(x) v y) v z) v x=x. 1037 [para_into,1035,642] c((x v y) v z) v c(x)=c(x). 1041 [para_into,1035,838] c((x v c(y)) v z) v y=y. 1051 [para_into,1035,838] c(x v (c(y) v z)) v y=y. 1085 [para_into,1041,838] c(x v (y v c(z))) v z=z. 1095 [para_into,1051,642] c(x v (y v z)) v c(y)=c(y). 1159 [para_into,892,1085,demod,643,643,643,643] (c(x v c(y v (z v u))) v u) v (y v (z v u))=y v (z v u). 1161 [para_into,892,1051,demod,643,643,643,643] (c(x v c(y v (z v u))) v z) v (y v (z v u))=y v (z v u). 1163 [para_into,892,1041,demod,643,643,643,643] (c(x v c((y v z) v u)) v z) v ((y v z) v u)= (y v z) v u. 1165 [para_into,892,1035,demod,643,643,643,643] (c(x v c((y v z) v u)) v y) v ((y v z) v u)= (y v z) v u. 1169 [para_into,892,718,demod,643] (c(x v c(y v z)) v y) v (y v z)=y v z. 1200,1199 [para_from,1037,928,demod,643] ((x v y) v z) v x= (x v y) v z. 1258,1257 [para_from,1095,712,demod,643] x v (y v (x v z))=y v (x v z). 4760 [para_into,1159,953,demod,643] (x v y) v (x v (z v y))=x v (z v y). 5313,5312 [para_into,1161,953,demod,643] (x v y) v (x v (y v z))=x v (y v z). 5739,5738 [para_into,1163,937,demod,643] (x v y) v ((z v y) v x)= (z v y) v x. 6102 [para_into,1165,937,demod,643] (x v y) v ((y v z) v x)= (y v z) v x. 7373,7372 [para_into,1169,937,demod,643] (x v y) v (y v x)=y v x. 7594 [para_from,7372,957,demod,7373,7373] x v y=y v x. 17813 [para_into,4760,7594] (x v (y v z)) v (x v z)=x v (y v z). 18921 [para_from,5312,4760,demod,5313] ((x v y) v (y v z)) v (x v (y v z))=x v (y v z). 19351 [para_from,5738,5312,demod,5739] ((x v y) v (z v y)) v ((z v y) v x)= (z v y) v x. 19774,19773 [para_into,6102,7594] ((x v y) v z) v (z v x)= (x v y) v z. 19779 [back_demod,19351,demod,19774] (x v y) v (z v y)= (z v y) v x. 20260 [para_into,19779,7594] (x v y) v (z v x)= (z v x) v y. 20410,20409 [para_into,19779,7594] (x v y) v (z v y)= (x v y) v z. 20422 [copy,20260,flip.1] (x v y) v z= (y v z) v (x v y). 20472,20471 [back_demod,18921,demod,20410,1200] (x v y) v (y v z)=x v (y v z). 20614,20613 [back_demod,19773,demod,20472] (x v y) v (z v x)= (x v y) v z. 20648 [back_demod,20422,demod,20614] (x v y) v z= (y v z) v x. 21300,21299 [para_from,20648,724,demod,20614,20472,flip.1] (x v y) v z=x v (y v z). 22049 [back_demod,17813,demod,21300,21300,839,1258] x v (y v z)=y v (x v z). 22050 [binary,22049,1] $Ans(AJ). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 404 clauses generated 223978 para_from generated 99614 para_into generated 124364 demod & eval rewrites 485257 clauses wt,lit,sk delete 1023 tautologies deleted 0 clauses forward subsumed 217918 (subsumed by sos) 6281 unit deletions 0 factor simplifications 0 clauses kept 12603 new demodulators 9434 empty clauses 5 clauses back demodulated 4441 clauses back subsumed 12 usable size 313 sos size 7837 demodulators size 6531 passive size 5 hot size 0 Kbytes malloced 15775 ----------- times (seconds) ----------- user CPU time 18.03 (0 hr, 0 min, 18 sec) system CPU time 1.33 (0 hr, 0 min, 1 sec) wall-clock time 19 (0 hr, 0 min, 19 sec) input time 0.00 clausify time 0.00 process input 0.00 pick given time 0.28 para_into time 0.51 para_from time 0.72 pre_process time 5.28 renumber time 0.35 demod time 2.86 order equalities 0.19 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.33 hints keep time 0.00 sort lits time 0.00 forward subsume 0.52 delete cl time 0.18 keep cl time 0.37 hints time 0.00 print_cl time 0.00 conflict time 0.06 new demod time 0.17 post_process time 11.08 back demod time 9.70 back subsume 1.35 factor time 0.00 unindex time 3.47 That finishes the proof of the theorem. Process 2367 finished Mon Sep 15 12:19:55 2003