----- Otter 3.3, August 2003 ----- The process was started by mccune on lemma.mcs.anl.gov, Mon Sep 15 12:17:26 2003 The command was "otter". The process ID is 2353. 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(x,f(f(y,y),y)),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,6). 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 [] c(c(A))!=A|$Ans(CC). 5 [] A v c(A)!=B v c(B)|$Ans(ONE). 6 [] f(A,B)!=c(A) v c(B)|$Ans(DEF_SS). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 7 [] x=x. Following clause subsumed by 7 during input processing: 0 [copy,7,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=23): 8 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. ---> New Demodulator: 9 [new_demod,8] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. ** KEPT (pick-wt=11): 11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y. ---> New Demodulator: 12 [new_demod,11] f(f(x,x),f(y,y))=x v y. ** KEPT (pick-wt=11): 14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y. ---> New Demodulator: 15 [new_demod,14] f(f(x,y),f(x,y))=x^y. ** KEPT (pick-wt=6): 17 [copy,16,flip.1] f(x,x)=c(x). ---> New Demodulator: 18 [new_demod,17] f(x,x)=c(x). >>>> Starting back demodulation with 9. >>>> Starting back demodulation with 12. >>>> Starting back demodulation with 15. >>>> Starting back demodulation with 18. >> back demodulating 14 with 18. >> back demodulating 11 with 18. >> back demodulating 8 with 18. >>>> Starting back demodulation with 20. >>>> Starting back demodulation with 22. >>>> Starting back demodulation with 24. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=6) 17 [copy,16,flip.1] f(x,x)=c(x). given clause #2: (wt=8) 19 [back_demod,14,demod,18] c(f(x,y))=x^y. given clause #3: (wt=7) 25 [para_into,19,17,flip.1] x^x=c(c(x)). given clause #4: (wt=9) 21 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y. given clause #5: (wt=7) 30 [para_into,21,17] c(c(x))=x v x. given clause #6: (wt=22) 23 [back_demod,8,demod,18] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(c(x),x)),z)))=y. given clause #7: (wt=7) 33 [back_demod,25,demod,31] x^x=x v x. given clause #8: (wt=10) 35 [para_from,21,19,flip.1] c(x)^c(y)=c(x v y). given clause #9: (wt=10) 37 [para_into,30,30] c(x v x)=c(x) v c(x). given clause #10: (wt=11) 41 [para_from,30,21] f(c(x),y v y)=x v c(y). given clause #11: (wt=12) 27 [para_into,21,19] f(x^y,c(z))=f(x,y) v z. given clause #12: (wt=11) 43 [para_from,30,21] f(x v x,c(y))=c(x) v y. given clause #13: (wt=12) 29 [para_into,21,19] f(c(x),y^z)=x v f(y,z). given clause #14: (wt=12) 32 [copy,29,flip.1] x v f(y,z)=f(c(x),y^z). given clause #15: (wt=12) 39 [para_into,30,19,flip.1] f(x,y) v f(x,y)=c(x^y). given clause #16: (wt=26) 45 [para_into,23,21,demod,31,44] f(f(f(x v y,f(c(y),z)),u),f(c(y),f(f(c(y),c(x) v x),z)))=c(y). given clause #17: (wt=12) 71 [para_into,35,30] (x v x)^c(y)=c(c(x) v y). given clause #18: (wt=12) 74 [para_into,35,30] c(x)^ (y v y)=c(x v c(y)). given clause #19: (wt=13) 73 [para_into,35,19] (x^y)^c(z)=c(f(x,y) v z). given clause #20: (wt=13) 76 [para_into,35,19] c(x)^ (y^z)=c(x v f(y,z)). given clause #21: (wt=21) 47 [para_into,23,17] f(f(f(c(x),f(x,y)),z),f(x,f(f(x,f(c(x),x)),y)))=x. given clause #22: (wt=13) 77 [copy,73,flip.1] c(f(x,y) v z)= (x^y)^c(z). given clause #23: (wt=13) 78 [copy,76,flip.1] c(x v f(y,z))=c(x)^ (y^z). given clause #24: (wt=13) 83 [para_into,41,30] f(x v x,y v y)=c(x) v c(y). given clause #25: (wt=14) 85 [para_into,41,19] f(x^y,z v z)=f(x,y) v c(z). given clause #26: (wt=27) 49 [para_into,23,21] f(f(f(f(x,c(y)),y v z),u),f(c(y),f(f(c(y),f(c(x),x)),c(z))))=c(y). given clause #27: (wt=14) 99 [para_into,43,19] f(x v x,y^z)=c(x) v f(y,z). given clause #28: (wt=14) 100 [copy,99,flip.1] c(x) v f(y,z)=f(x v x,y^z). given clause #29: (wt=14) 151 [para_into,71,30] (x v x)^ (y v y)=c(c(x) v c(y)). given clause #30: (wt=15) 93 [para_into,27,19] f(x^y,z^u)=f(x,y) v f(z,u). given clause #31: (wt=21) 51 [para_into,23,17] f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(x),x)),y)))=y. given clause #32: (wt=15) 94 [copy,93,flip.1] f(x,y) v f(z,u)=f(x^y,z^u). given clause #33: (wt=15) 153 [para_into,71,19] (x v x)^ (y^z)=c(c(x) v f(y,z)). given clause #34: (wt=15) 154 [copy,153,flip.1] c(c(x) v f(y,z))= (x v x)^ (y^z). given clause #35: (wt=15) 155 [para_into,74,19] (x^y)^ (z v z)=c(f(x,y) v c(z)). given clause #36: (wt=34) 53 [para_into,23,23,demod,20] f(f(x,y),f(x,f(f(x,f(f(z,x)^f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(c(z),z)),u))))=x. given clause #37: (wt=15) 156 [copy,155,flip.1] c(f(x,y) v c(z))= (x^y)^ (z v z). given clause #38: (wt=15) 467 [para_from,53,47] f(c(x),f(x,f(f(x,f(c(x),x)),y)))=x. ----> UNIT CONFLICT at 0.07 sec ----> 701 [binary,699,3] $Ans(DM). Length of proof is 15. Level of proof is 6. ---------------- PROOF ---------------- 3 [] A^B!=c(c(A) v c(B))|$Ans(DM). 8 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. 10 [] x v y=f(f(x,x),f(y,y)). 11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y. 13 [] x^y=f(f(x,y),f(x,y)). 14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y. 16 [] c(x)=f(x,x). 18,17 [copy,16,flip.1] f(x,x)=c(x). 20,19 [back_demod,14,demod,18] c(f(x,y))=x^y. 21 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y. 23 [back_demod,8,demod,18] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(c(x),x)),z)))=y. 31,30 [para_into,21,17] c(c(x))=x v x. 35 [para_from,21,19,flip.1] c(x)^c(y)=c(x v y). 47 [para_into,23,17] f(f(f(c(x),f(x,y)),z),f(x,f(f(x,f(c(x),x)),y)))=x. 53 [para_into,23,23,demod,20] f(f(x,y),f(x,f(f(x,f(f(z,x)^f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(c(z),z)),u))))=x. 71 [para_into,35,30] (x v x)^c(y)=c(c(x) v y). 151 [para_into,71,30] (x v x)^ (y v y)=c(c(x) v c(y)). 467 [para_from,53,47] f(c(x),f(x,f(f(x,f(c(x),x)),y)))=x. 526,525 [para_into,467,53,demod,18,18,31] x v x=x. 699 [back_demod,151,demod,526,526] x^y=c(c(x) v c(y)). 701 [binary,699,3] $Ans(DM). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.07 sec ----> 726 [binary,724,6] $Ans(DEF_SS). Length of proof is 14. Level of proof is 6. ---------------- PROOF ---------------- 6 [] f(A,B)!=c(A) v c(B)|$Ans(DEF_SS). 8 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. 10 [] x v y=f(f(x,x),f(y,y)). 11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y. 13 [] x^y=f(f(x,y),f(x,y)). 14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y. 16 [] c(x)=f(x,x). 18,17 [copy,16,flip.1] f(x,x)=c(x). 20,19 [back_demod,14,demod,18] c(f(x,y))=x^y. 21 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y. 23 [back_demod,8,demod,18] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(c(x),x)),z)))=y. 31,30 [para_into,21,17] c(c(x))=x v x. 41 [para_from,30,21] f(c(x),y v y)=x v c(y). 47 [para_into,23,17] f(f(f(c(x),f(x,y)),z),f(x,f(f(x,f(c(x),x)),y)))=x. 53 [para_into,23,23,demod,20] f(f(x,y),f(x,f(f(x,f(f(z,x)^f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(c(z),z)),u))))=x. 83 [para_into,41,30] f(x v x,y v y)=c(x) v c(y). 467 [para_from,53,47] f(c(x),f(x,f(f(x,f(c(x),x)),y)))=x. 526,525 [para_into,467,53,demod,18,18,31] x v x=x. 724 [back_demod,83,demod,526,526] f(x,y)=c(x) v c(y). 726 [binary,724,6] $Ans(DEF_SS). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.07 sec ----> 731 [binary,729,4] $Ans(CC). Length of proof is 12. Level of proof is 6. ---------------- PROOF ---------------- 4 [] c(c(A))!=A|$Ans(CC). 8 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. 10 [] x v y=f(f(x,x),f(y,y)). 11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y. 13 [] x^y=f(f(x,y),f(x,y)). 14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y. 16 [] c(x)=f(x,x). 18,17 [copy,16,flip.1] f(x,x)=c(x). 20,19 [back_demod,14,demod,18] c(f(x,y))=x^y. 21 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y. 23 [back_demod,8,demod,18] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(c(x),x)),z)))=y. 31,30 [para_into,21,17] c(c(x))=x v x. 47 [para_into,23,17] f(f(f(c(x),f(x,y)),z),f(x,f(f(x,f(c(x),x)),y)))=x. 53 [para_into,23,23,demod,20] f(f(x,y),f(x,f(f(x,f(f(z,x)^f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(c(z),z)),u))))=x. 467 [para_from,53,47] f(c(x),f(x,f(f(x,f(c(x),x)),y)))=x. 526,525 [para_into,467,53,demod,18,18,31] x v x=x. 729 [back_demod,30,demod,526] c(c(x))=x. 731 [binary,729,4] $Ans(CC). ------------ end of proof ------------- given clause #39: (wt=5) 525 [para_into,467,53,demod,18,18,31] x v x=x. given clause #40: (wt=5) 729 [back_demod,30,demod,526] c(c(x))=x. given clause #41: (wt=10) 699 [back_demod,151,demod,526,526] x^y=c(c(x) v c(y)). given clause #42: (wt=9) 724 [back_demod,83,demod,526,526] f(x,y)=c(x) v c(y). given clause #43: (wt=16) 736 [back_demod,537,demod,725,730,700,725,730,725,730] x v c(c(x) v (c(x) v c(x v c(x))))=x. given clause #44: (wt=16) 802 [para_into,736,729,demod,730,730] c(x) v c(x v (x v c(c(x) v x)))=c(x). given clause #45: (wt=21) 790 [back_demod,539,demod,725,725,725,725,730] x v c(c(x) v c(c(c(x) v c(x v c(x))) v c(y)))=x. given clause #46: (wt=26) 727 [back_demod,55,demod,526,725,725,31,526,725,725,725,725] 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) 816 [back_demod,810,demod,813] c(c(x) v y) v x=x. given clause #48: (wt=10) 818 [para_into,816,729] c(x v y) v c(x)=c(x). given clause #49: (wt=9) 830 [para_into,818,818,demod,730,730,730] x v (x v y)=x v y. given clause #50: (wt=13) 828 [back_demod,736,demod,821] x v c(c(x) v c(x v c(x)))=x. given clause #51: (wt=36) 738 [back_demod,533,demod,725,730,700,725,730,725,725,730,725,730,725,730,725] (c(x v y) v c(y v c(z))) v c(c(c(x v y) v c(y v c(z))) v y)=c(x v y) v c(y v c(z)). given clause #52: (wt=14) 832 [back_demod,802,demod,831] c(x) v c(x v c(c(x) v x))=c(x). given clause #53: (wt=19) 812 [para_into,727,525] c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. given clause #54: (wt=17) 850 [para_into,812,729,demod,730,730,730] c(x v c(c(x v c(c(x) v x)) v x))=c(x). given clause #55: (wt=15) 860 [para_from,850,729,demod,730,flip.1] x v c(c(x v c(c(x) v x)) v x)=x. given clause #56: (wt=29) 748 [back_demod,371,demod,700,725,725,730,725,730,725,725,730,725] c(x) v c(x v c(c(x v c((c(y) v c(x)) v c(c(y) v c(x)))) v c(z)))=c(x). given clause #57: (wt=19) 822 [back_demod,740,demod,819,730] (x v c(c(x) v c(y))) v x=x v c(c(x) v c(y)). given clause #58: (wt=15) 872 [para_into,822,818,demod,730,819,730] ((x v y) v x) v (x v y)= (x v y) v x. given clause #59: (wt=17) 870 [para_into,822,729,demod,730] (x v c(c(x) v y)) v x=x v c(c(x) v y). given clause #60: (wt=18) 874 [para_into,872,818,demod,819,819] (c(x) v c(x v y)) v c(x)=c(x) v c(x v y). given clause #61: (wt=28) 750 [back_demod,353,demod,725,700,730,725,730,725,725,725,725,730] (c(c(x) v c(y)) v y) v c(c(y) v c(c(c(y) v c(x v c(x))) v c(y)))=y. given clause #62: (wt=12) 886 [para_from,750,830,demod,751] (c(c(x) v c(y)) v y) v y=y. given clause #63: (wt=11) 892 [para_into,886,729] (c(x v c(y)) v y) v y=y. given clause #64: (wt=13) 898 [para_into,892,729] (c(x v y) v c(y)) v c(y)=c(y). given clause #65: (wt=19) 848 [para_into,738,818,demod,819,730,819] c(x v c(y)) v c((x v c(y)) v x)=c(x v c(y)). given clause #66: (wt=33) 752 [back_demod,279,demod,700,730,725,730,725,730,725,725,725,725,730] x v c(c(x v y) v c(c(c(x v y) v c((c(z) v x) v c(c(z) v x))) v c(u)))=x v y. given clause #67: (wt=12) 918 [para_into,848,818,demod,730,819,819,730] x v c(c(x) v c(x v y))=x. given clause #68: (wt=14) 934 [para_into,918,729] c(x) v c(x v c(c(x) v y))=c(x). given clause #69: (wt=15) 916 [para_into,848,898,demod,730,899,899,730] x v c(c(x) v (c(y v x) v c(x)))=x. given clause #70: (wt=16) 914 [para_into,848,729,demod,730,730] c(x v y) v c((x v y) v x)=c(x v y). given clause #71: (wt=28) 754 [back_demod,263,demod,725,730,700,725,730,725,730,725,730,725,730,725,730] (c(c(x) v y) v c(y v z)) v c(y v c(c(y v c(x v c(x))) v z))=c(y). given clause #72: (wt=16) 936 [para_into,916,729,demod,730] c(x) v c(x v (c(y v c(x)) v x))=c(x). given clause #73: (wt=16) 972 [para_into,754,816,demod,526,730,730] (c(c(x) v c(y)) v c(c(y) v y)) v y=y. given clause #74: (wt=9) 994 [para_into,972,818,demod,730,871] x v c(c(x) v x)=x. given clause #75: (wt=11) 998 [para_into,994,729] c(x) v c(x v c(x))=c(x). given clause #76: (wt=33) 782 [back_demod,661,demod,725,725,725,730,725,730,725,730,725] c(c(c(c(x) v y) v c(y v z)) v c(u)) v c(y v c(c(y v c(x v c(x))) v z))=c(y). given clause #77: (wt=15) 988 [para_into,972,729] (c(x v c(y)) v c(c(y) v y)) v y=y. given clause #78: (wt=16) 980 [para_from,754,830,demod,755] (c(c(x) v y) v c(y v z)) v c(y)=c(y). ----> UNIT CONFLICT at 0.13 sec ----> 1074 [binary,1072,2] $Ans(B1_rewritten). Length of proof is 35. Level of proof is 13. ---------------- PROOF ---------------- 2 [] A v c(c(A) v B)!=A|$Ans(B1_rewritten). 8 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. 10 [] x v y=f(f(x,x),f(y,y)). 11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y. 13 [] x^y=f(f(x,y),f(x,y)). 14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y. 16 [] c(x)=f(x,x). 18,17 [copy,16,flip.1] f(x,x)=c(x). 20,19 [back_demod,14,demod,18] c(f(x,y))=x^y. 21 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y. 23 [back_demod,8,demod,18] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(c(x),x)),z)))=y. 31,30 [para_into,21,17] c(c(x))=x v x. 35 [para_from,21,19,flip.1] c(x)^c(y)=c(x v y). 41 [para_from,30,21] f(c(x),y v y)=x v c(y). 47 [para_into,23,17] f(f(f(c(x),f(x,y)),z),f(x,f(f(x,f(c(x),x)),y)))=x. 49 [para_into,23,21] f(f(f(f(x,c(y)),y v z),u),f(c(y),f(f(c(y),f(c(x),x)),c(z))))=c(y). 53 [para_into,23,23,demod,20] f(f(x,y),f(x,f(f(x,f(f(z,x)^f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(c(z),z)),u))))=x. 55 [para_into,23,17,demod,18,31] f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x)))=x. 71 [para_into,35,30] (x v x)^c(y)=c(c(x) v y). 83 [para_into,41,30] f(x v x,y v y)=c(x) v c(y). 151 [para_into,71,30] (x v x)^ (y v y)=c(c(x) v c(y)). 263 [para_into,49,17,demod,20] f(f(x,c(y))^ (y v z),f(c(y),f(f(c(y),f(c(x),x)),c(z))))=c(y). 467 [para_from,53,47] f(c(x),f(x,f(f(x,f(c(x),x)),y)))=x. 526,525 [para_into,467,53,demod,18,18,31] x v x=x. 531 [para_into,467,47,demod,20] f(c(x)^f(x,y),f(f(c(x),f(x,y)),x))=f(c(x),f(x,y)). 700,699 [back_demod,151,demod,526,526] x^y=c(c(x) v c(y)). 725,724 [back_demod,83,demod,526,526] f(x,y)=c(x) v c(y). 727 [back_demod,55,demod,526,725,725,31,526,725,725,725,725] 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. 730,729 [back_demod,30,demod,526] c(c(x))=x. 740 [back_demod,531,demod,725,700,730,725,725,730,725,725,730,725,725,730] (x v c(c(x) v c(y))) v c(c(x v c(c(x) v c(y))) v c(x))=x v c(c(x) v c(y)). 755,754 [back_demod,263,demod,725,730,700,725,730,725,730,725,730,725,730,725,730] (c(c(x) v y) v c(y v z)) v c(y v c(c(y v c(x v c(x))) v z))=c(y). 810 [para_into,727,729] c(c(x) v y) v c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 813,812 [para_into,727,525] c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 816 [back_demod,810,demod,813] c(c(x) v y) v x=x. 819,818 [para_into,816,729] c(x v y) v c(x)=c(x). 822 [back_demod,740,demod,819,730] (x v c(c(x) v c(y))) v x=x v c(c(x) v c(y)). 830 [para_into,818,818,demod,730,730,730] x v (x v y)=x v y. 871,870 [para_into,822,729,demod,730] (x v c(c(x) v y)) v x=x v c(c(x) v y). 980 [para_from,754,830,demod,755] (c(c(x) v y) v c(y v z)) v c(y)=c(y). 1072 [para_into,980,818,demod,730,730,871,730] x v c(c(x) v y)=x. 1074 [binary,1072,2] $Ans(B1_rewritten). ------------ end of proof ------------- given clause #79: (wt=9) 1072 [para_into,980,818,demod,730,730,871,730] x v c(c(x) v y)=x. given clause #80: (wt=9) 1093 [para_into,1072,818,demod,730] (x v y) v x=x v y. given clause #81: (wt=33) 784 [back_demod,625,demod,725,730,725,725,725,725,725] c(c(c(c(x) v c(y)) v y) v c(z)) v c(c(y) v c(c(c(y) v c(x v c(x))) v c(y)))=y. given clause #82: (wt=10) 1075 [para_into,980,816,demod,875] c(x) v c(x v y)=c(x). given clause #83: (wt=11) 1107 [para_into,1093,892,demod,893] x v (c(y v c(x)) v x)=x. given clause #84: (wt=13) 1105 [para_into,1093,898,demod,899] c(x) v (c(y v x) v c(x))=c(x). given clause #85: (wt=15) 1060 [para_into,980,729] (c(x v y) v c(y v z)) v c(y)=c(y). given clause #86: (wt=32) 786 [back_demod,623,demod,725,730,725,725,725,725,725] c(c(c(x v c(y)) v y) v c(z)) v c(c(y) v c(c(c(y) v c(c(x) v x)) v c(y)))=y. given clause #87: (wt=15) 1103 [para_into,1093,988,demod,989] x v (c(y v c(x)) v c(c(x) v x))=x. given clause #88: (wt=15) 1111 [para_from,1093,988] (c(c(x) v y) v c(c(x) v x)) v x=x. given clause #89: (wt=15) 1141 [para_into,1060,1093] (c(x v y) v c(x v z)) v c(x)=c(x). given clause #90: (wt=15) 1153 [para_into,1060,729,demod,730] (c(x v c(y)) v c(c(y) v z)) v y=y. given clause #91: (wt=23) 794 [back_demod,469,demod,725,730,725,725,730,725] c(x v y) v c(y v c(c(y v c(c(x) v x)) v c(z)))=c(y). given clause #92: (wt=10) 1219 [para_into,794,818,demod,730,526] c(x v y) v c(y)=c(y). given clause #93: (wt=9) 1243 [para_into,1219,729,demod,730] c(x v c(y)) v y=y. given clause #94: (wt=9) 1251 [para_from,1219,1072,demod,730] (x v y) v y=x v y. given clause #95: (wt=9) 1253 [para_from,1219,816,demod,730] x v (y v x)=y v x. given clause #96: (wt=32) 800 [back_demod,131,demod,725,725,725,730,725,730,725,730,725] c(c(c(x v y) v c(y v z)) v c(u)) v c(y v c(c(y v c(c(x) v x)) v z))=c(y). given clause #97: (wt=9) 1263 [para_from,1243,1093,demod,1244] x v c(y v c(x))=x. given clause #98: (wt=10) 1257 [para_from,1219,1093,demod,1220] c(x) v c(y v x)=c(x). given clause #99: (wt=13) 1335 [back_demod,1030,demod,1322] c((x v y) v c(z)) v c(x)=c(x). given clause #100: (wt=12) 1359 [para_into,1335,729] c((x v y) v z) v c(x)=c(x). given clause #101: (wt=33) 834 [back_demod,762,demod,831] c(c(c(x v y) v c(y v c(y v c(c(x) v x)))) v c(z)) v c(y v c(c(x) v x))=c(y). given clause #102: (wt=11) 1383 [para_into,1359,729,demod,730] c((c(x) v y) v z) v x=x. given clause #103: (wt=11) 1429 [para_into,834,1243] c(x v c(c(y) v y))=c(x). given clause #104: (wt=9) 1475 [para_from,1429,729,demod,730,flip.1] x v c(c(y) v y)=x. given clause #105: (wt=9) 1477 [para_into,1475,729] x v c(y v c(y))=x. given clause #106: (wt=17) 1143 [para_into,1060,1075,demod,730,730,730] (x v c(c(x v y) v z)) v (x v y)=x v y. given clause #107: (wt=9) 1479 [para_from,1475,1253,demod,1476] c(c(x) v x) v y=y. given clause #108: (wt=9) 1489 [para_from,1477,1253,demod,1478] c(x v c(x)) v y=y. given clause #109: (wt=11) 1439 [para_into,1383,1253] c((x v c(y)) v z) v y=y. given clause #110: (wt=11) 1441 [para_into,1383,1253] c(x v (c(y) v z)) v y=y. given clause #111: (wt=36) 1145 [para_into,1060,1060,demod,730] (c(x v (c(y v z) v c(z v u))) v z) v c(c(y v z) v c(z v u))=c(c(y v z) v c(z v u)). given clause #112: (wt=11) 1443 [para_from,1383,1093,demod,1384] x v c((c(x) v y) v z)=x. given clause #113: (wt=11) 1453 [para_into,1429,1243,demod,730,730,730,flip.1] x v (c(y) v y)=c(y) v y. given clause #114: (wt=11) 1457 [para_into,1429,818,demod,730,730,flip.1] (c(x) v x) v y=c(x) v x. given clause #115: (wt=9) 1617 [para_into,1457,1453] c(x) v x=c(y) v y. given clause #116: (wt=17) 1151 [para_into,1060,818,demod,730,730,730] (c(x v c(y v z)) v y) v (y v z)=y v z. given clause #117: (wt=9) 1618 [para_into,1617,729] x v c(x)=c(y) v y. given clause #118: (wt=9) 1619 [copy,1618,flip.1] c(x) v x=y v c(y). ----> UNIT CONFLICT at 0.23 sec ----> 1657 [binary,1656,5] $Ans(ONE). Length of proof is 42. Level of proof is 18. ---------------- PROOF ---------------- 5 [] A v c(A)!=B v c(B)|$Ans(ONE). 8 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. 10 [] x v y=f(f(x,x),f(y,y)). 11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y. 13 [] x^y=f(f(x,y),f(x,y)). 14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y. 16 [] c(x)=f(x,x). 18,17 [copy,16,flip.1] f(x,x)=c(x). 20,19 [back_demod,14,demod,18] c(f(x,y))=x^y. 21 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y. 23 [back_demod,8,demod,18] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(c(x),x)),z)))=y. 31,30 [para_into,21,17] c(c(x))=x v x. 35 [para_from,21,19,flip.1] c(x)^c(y)=c(x v y). 41 [para_from,30,21] f(c(x),y v y)=x v c(y). 44,43 [para_from,30,21] f(x v x,c(y))=c(x) v y. 45 [para_into,23,21,demod,31,44] f(f(f(x v y,f(c(y),z)),u),f(c(y),f(f(c(y),c(x) v x),z)))=c(y). 47 [para_into,23,17] f(f(f(c(x),f(x,y)),z),f(x,f(f(x,f(c(x),x)),y)))=x. 53 [para_into,23,23,demod,20] f(f(x,y),f(x,f(f(x,f(f(z,x)^f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(c(z),z)),u))))=x. 55 [para_into,23,17,demod,18,31] f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x)))=x. 71 [para_into,35,30] (x v x)^c(y)=c(c(x) v y). 83 [para_into,41,30] f(x v x,y v y)=c(x) v c(y). 139 [para_into,45,17,demod,20] f(f(f(x v y,f(c(y),f(c(y),c(x) v x))),z),f(c(y),c(y)^ (c(x) v x)))=c(y). 151 [para_into,71,30] (x v x)^ (y v y)=c(c(x) v c(y)). 467 [para_from,53,47] f(c(x),f(x,f(f(x,f(c(x),x)),y)))=x. 469 [para_from,53,45] f(x v y,f(c(y),f(f(c(y),c(x) v x),z)))=c(y). 526,525 [para_into,467,53,demod,18,18,31] x v x=x. 700,699 [back_demod,151,demod,526,526] x^y=c(c(x) v c(y)). 725,724 [back_demod,83,demod,526,526] f(x,y)=c(x) v c(y). 727 [back_demod,55,demod,526,725,725,31,526,725,725,725,725] 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. 730,729 [back_demod,30,demod,526] c(c(x))=x. 762 [back_demod,139,demod,725,730,725,730,725,725,700,730,725,730,730,725] c(c(c(x v y) v c(y v c(y v c(c(x) v x)))) v c(z)) v c(y v (y v c(c(x) v x)))=c(y). 794 [back_demod,469,demod,725,730,725,725,730,725] c(x v y) v c(y v c(c(y v c(c(x) v x)) v c(z)))=c(y). 810 [para_into,727,729] c(c(x) v y) v c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 813,812 [para_into,727,525] c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 816 [back_demod,810,demod,813] c(c(x) v y) v x=x. 818 [para_into,816,729] c(x v y) v c(x)=c(x). 831,830 [para_into,818,818,demod,730,730,730] x v (x v y)=x v y. 834 [back_demod,762,demod,831] c(c(c(x v y) v c(y v c(y v c(c(x) v x)))) v c(z)) v c(y v c(c(x) v x))=c(y). 1219 [para_into,794,818,demod,730,526] c(x v y) v c(y)=c(y). 1243 [para_into,1219,729,demod,730] c(x v c(y)) v y=y. 1429 [para_into,834,1243] c(x v c(c(y) v y))=c(x). 1453 [para_into,1429,1243,demod,730,730,730,flip.1] x v (c(y) v y)=c(y) v y. 1457 [para_into,1429,818,demod,730,730,flip.1] (c(x) v x) v y=c(x) v x. 1617 [para_into,1457,1453] c(x) v x=c(y) v y. 1618 [para_into,1617,729] x v c(x)=c(y) v y. 1619 [copy,1618,flip.1] c(x) v x=y v c(y). 1656 [para_into,1619,729] x v c(x)=y v c(y). 1657 [binary,1656,5] $Ans(ONE). ------------ end of proof ------------- given clause #119: (wt=9) 1656 [para_into,1619,729] x v c(x)=y v c(y). given clause #120: (wt=11) 1525 [para_into,1479,1477] c(c(x) v x)=c(y v c(y)). given clause #121: (wt=15) 1155 [para_from,1060,1093,demod,1061] c(x) v (c(y v x) v c(x v z))=c(x). given clause #122: (wt=11) 1526 [para_into,1479,1475] c(c(x) v x)=c(c(y) v y). given clause #123: (wt=11) 1527 [copy,1525,flip.1] c(x v c(x))=c(c(y) v y). given clause #124: (wt=11) 1528 [para_into,1489,1477] c(x v c(x))=c(y v c(y)). given clause #125: (wt=11) 1531 [para_into,1439,1253] c(x v (y v c(z))) v z=z. given clause #126: (wt=23) 1157 [para_from,1060,1075,demod,730] c(c(x v y) v c(y v z)) v y=c(c(x v y) v c(y v z)). given clause #127: (wt=11) 1547 [para_from,1439,1093,demod,1440] x v c((y v c(x)) v z)=x. given clause #128: (wt=11) 1583 [para_from,1441,1093,demod,1442] x v c(y v (c(x) v z))=x. given clause #129: (wt=11) 1613 [para_into,1453,729,demod,730] x v (y v c(y))=y v c(y). given clause #130: (wt=11) 1615 [para_into,1457,729,demod,730] (x v c(x)) v y=x v c(x). given clause #131: (wt=23) 1159 [para_from,1060,818,demod,730] x v c(c(y v x) v c(x v z))=c(c(y v x) v c(x v z)). given clause #132: (wt=11) 1640 [para_into,1151,1257,demod,730] (x v y) v (y v x)=y v x. given clause #133: (wt=7) 1846 [para_from,1640,1093,demod,1641,1641] x v y=y v x. given clause #134: (wt=11) 1710 [para_from,1531,1093,demod,1532] x v c(y v (z v c(x)))=x. given clause #135: (wt=12) 1365 [para_into,1359,1253] c((x v y) v z) v c(y)=c(y). given clause #136: (wt=36) 1179 [para_into,1141,1141,demod,730] (x v c((c(x v y) v c(x v z)) v u)) v c(c(x v y) v c(x v z))=c(c(x v y) v c(x v z)). given clause #137: (wt=12) 1381 [para_into,1359,1253] c(x v (y v z)) v c(y)=c(y). given clause #138: (wt=12) 1393 [para_from,1359,1093,demod,1360] c(x) v c((x v y) v z)=c(x). given clause #139: (wt=12) 1686 [para_into,1531,729] c(x v (y v z)) v c(z)=c(z). given clause #140: (wt=12) 1750 [para_into,1547,729] c(x) v c((y v x) v z)=c(x). given clause #141: (wt=36) 1181 [para_into,1141,1060,demod,730] (x v c((c(y v x) v c(x v z)) v u)) v c(c(y v x) v c(x v z))=c(c(y v x) v c(x v z)). given clause #142: (wt=12) 1758 [para_into,1583,729] c(x) v c(y v (x v z))=c(x). given clause #143: (wt=12) 1881 [para_into,1710,729] c(x) v c(y v (z v x))=c(x). given clause #144: (wt=13) 1369 [para_into,1359,1219,demod,730,730] c(c(x) v y) v (z v x)=z v x. given clause #145: (wt=13) 1377 [para_into,1359,818,demod,730,730] c(c(x) v y) v (x v z)=x v z. given clause #146: (wt=36) 1183 [para_into,1141,1141,demod,730] (c((c(x v y) v c(x v z)) v u) v x) v c(c(x v y) v c(x v z))=c(c(x v y) v c(x v z)). given clause #147: (wt=13) 1389 [para_from,1359,1072,demod,730] ((x v y) v z) v x= (x v y) v z. given clause #148: (wt=13) 1391 [para_from,1359,816,demod,730] x v ((x v y) v z)= (x v y) v z. given clause #149: (wt=13) 1561 [para_into,1441,1219] c(x v c(y)) v (z v y)=z v y. given clause #150: (wt=13) 1563 [para_into,1441,818] c(x v c(y)) v (y v z)=y v z. given clause #151: (wt=36) 1185 [para_into,1141,1060,demod,730] (c((c(x v y) v c(y v z)) v u) v y) v c(c(x v y) v c(y v z))=c(c(x v y) v c(y v z)). given clause #152: (wt=13) 1607 [para_into,1443,1219] (x v y) v c(c(y) v z)=x v y. given clause #153: (wt=13) 1609 [para_into,1443,818] (x v y) v c(c(x) v z)=x v y. given clause #154: (wt=13) 1772 [para_into,1583,1219] (x v y) v c(z v c(y))=x v y. given clause #155: (wt=13) 1774 [para_into,1583,818] (x v y) v c(z v c(x))=x v y. given clause #156: (wt=17) 1191 [para_into,1141,818,demod,730,730,730] (c(c(x v y) v z) v x) v (x v y)=x v y. given clause #157: (wt=13) 1909 [para_from,1365,1072,demod,730] ((x v y) v z) v y= (x v y) v z. given clause #158: (wt=13) 1911 [para_from,1365,816,demod,730] x v ((y v x) v z)= (y v x) v z. given clause #159: (wt=13) 1977 [para_from,1381,1072,demod,730] (x v (y v z)) v y=x v (y v z). given clause #160: (wt=13) 1979 [para_from,1381,816,demod,730] x v (y v (x v z))=y v (x v z). given clause #161: (wt=15) 1193 [para_into,1141,729,demod,730] (c(c(x) v y) v c(c(x) v z)) v x=x. given clause #162: (wt=13) 2029 [para_from,1686,1072,demod,730] (x v (y v z)) v z=x v (y v z). given clause #163: (wt=13) 2031 [para_from,1686,816,demod,730] x v (y v (z v x))=y v (z v x). given clause #164: (wt=13) 2115 [para_into,1369,1710,demod,730,1711] c((x v (y v c(z))) v u) v z=z. given clause #165: (wt=13) 2117 [para_into,1369,1583,demod,730,1584] c((x v (c(y) v z)) v u) v y=y. given clause #166: (wt=36) 1195 [para_from,1141,1060,demod,730] (c(x v (c(y v z) v c(y v u))) v y) v c(c(y v z) v c(y v u))=c(c(y v z) v c(y v u)). given clause #167: (wt=13) 2119 [para_into,1369,1547,demod,730,1548] c(((x v c(y)) v z) v u) v y=y. given clause #168: (wt=13) 2121 [para_into,1369,1443,demod,730,1444] c(((c(x) v y) v z) v u) v x=x. given clause #169: (wt=13) 2267 [para_from,1389,1710] x v c(((y v c(x)) v z) v u)=x. given clause #170: (wt=13) 2269 [para_from,1389,1583] x v c(((c(x) v y) v z) v u)=x. given clause #171: (wt=15) 1197 [para_from,1141,1093,demod,1142] c(x) v (c(x v y) v c(x v z))=c(x). given clause #172: (wt=13) 2271 [para_from,1389,1710] x v c(y v ((c(x) v z) v u))=x. given clause #173: (wt=13) 2283 [para_from,1389,1531] c(x v ((c(y) v z) v u)) v y=y. given clause #174: (wt=13) 2341 [para_into,1561,1710,demod,730,1711] c(x v (y v (z v c(u)))) v u=u. given clause #175: (wt=13) 2343 [para_into,1561,1583,demod,730,1584] c(x v (y v (c(z) v u))) v z=z. given clause #176: (wt=23) 1199 [para_from,1141,1075,demod,730] c(c(x v y) v c(x v z)) v x=c(c(x v y) v c(x v z)). given clause #177: (wt=13) 2345 [para_into,1561,1547,demod,730,1548] c(x v ((y v c(z)) v u)) v z=z. given clause #178: (wt=13) 2449 [para_into,1607,1710,demod,730,1711] x v c((y v (z v c(x))) v u)=x. given clause #179: (wt=13) 2453 [para_into,1607,1583,demod,730,1584] x v c((y v (c(x) v z)) v u)=x. given clause #180: (wt=13) 2519 [para_into,1772,1710,demod,730,1711] x v c(y v (z v (u v c(x))))=x. given clause #181: (wt=23) 1201 [para_from,1141,818,demod,730] x v c(c(x v y) v c(x v z))=c(c(x v y) v c(x v z)). given clause #182: (wt=13) 2523 [para_into,1772,1583,demod,730,1584] x v c(y v (z v (c(x) v u)))=x. given clause #183: (wt=13) 2525 [para_into,1772,1547,demod,730,1548] x v c(y v ((z v c(x)) v u))=x. given clause #184: (wt=14) 1367 [para_into,1359,1243,demod,730,730] c(x v y) v (z v c(x))=z v c(x). given clause #185: (wt=14) 1379 [para_into,1359,816,demod,730,730] c(x v y) v (c(x) v z)=c(x) v z. given clause #186: (wt=15) 1203 [para_from,1153,1093,demod,1154] x v (c(y v c(x)) v c(c(x) v z))=x. given clause #187: (wt=14) 1559 [para_into,1441,1243] c(x v y) v (z v c(y))=z v c(y). given clause #188: (wt=14) 1565 [para_into,1441,816] c(x v y) v (c(y) v z)=c(y) v z. given clause #189: (wt=14) 1605 [para_into,1443,1243] (x v c(y)) v c(y v z)=x v c(y). given clause #190: (wt=14) 1611 [para_into,1443,816] (c(x) v y) v c(x v z)=c(x) v y. given clause #191: (wt=17) 1247 [para_from,1219,1141,demod,730,730,730] (c(c(x v y) v z) v y) v (x v y)=x v y. given clause #192: (wt=14) 1770 [para_into,1583,1243] (x v c(y)) v c(z v y)=x v c(y). given clause #193: (wt=14) 1776 [para_into,1583,816] (c(x) v y) v c(z v x)=c(x) v y. given clause #194: (wt=14) 1849 [para_from,1640,1075] c(x v y) v c(y v x)=c(x v y). given clause #195: (wt=14) 2109 [para_into,1369,1881,demod,730,1882] c((x v (y v z)) v u) v c(z)=c(z). given clause #196: (wt=17) 1249 [para_from,1219,1153,demod,730] (c(x v c(y v z)) v z) v (y v z)=y v z. given clause #197: (wt=14) 2111 [para_into,1369,1758,demod,730,1759] c((x v (y v z)) v u) v c(y)=c(y). given clause #198: (wt=14) 2113 [para_into,1369,1750,demod,730,1751] c(((x v y) v z) v u) v c(y)=c(y). given clause #199: (wt=14) 2123 [para_into,1369,1393,demod,730,1394] c(((x v y) v z) v u) v c(x)=c(x). given clause #200: (wt=14) 2263 [para_from,1389,1881] c(x) v c(((y v x) v z) v u)=c(x). given clause #201: (wt=17) 1259 [para_from,1219,1141,demod,730,730,730] (x v c(c(y v x) v z)) v (y v x)=y v x. given clause #202: (wt=14) 2265 [para_from,1389,1758] c(x) v c(((x v y) v z) v u)=c(x). given clause #203: (wt=14) 2281 [para_from,1389,1881] c(x) v c(y v ((x v z) v u))=c(x). given clause #204: (wt=14) 2285 [para_from,1389,1686] c(x v ((y v z) v u)) v c(y)=c(y). given clause #205: (wt=14) 2335 [para_into,1561,1881,demod,730,1882] c(x v (y v (z v u))) v c(u)=c(u). given clause #206: (wt=15) 1267 [para_from,1253,1141] (c(x v y) v c(z v x)) v c(x)=c(x). given clause #207: (wt=14) 2337 [para_into,1561,1758,demod,730,1759] c(x v (y v (z v u))) v c(z)=c(z). given clause #208: (wt=14) 2339 [para_into,1561,1750,demod,730,1751] c(x v ((y v z) v u)) v c(z)=c(z). given clause #209: (wt=14) 2445 [para_into,1607,1881,demod,730,1882] c(x) v c((y v (z v x)) v u)=c(x). given clause #210: (wt=14) 2447 [para_into,1607,1758,demod,730,1759] c(x) v c((y v (x v z)) v u)=c(x). given clause #211: (wt=15) 1269 [para_from,1253,1153] (c(x v c(y)) v c(z v c(y))) v y=y. given clause #212: (wt=14) 2511 [para_into,1772,1881,demod,730,1882] c(x) v c(y v (z v (u v x)))=c(x). given clause #213: (wt=14) 2515 [para_into,1772,1758,demod,730,1759] c(x) v c(y v (z v (x v u)))=c(x). given clause #214: (wt=14) 2517 [para_into,1772,1750,demod,730,1751] c(x) v c(y v ((z v x) v u))=c(x). given clause #215: (wt=15) 1271 [para_from,1253,1060] (c(x v y) v c(z v y)) v c(y)=c(y). given clause #216: (wt=19) 1325 [back_demod,1305,demod,1322] c(c(c(x v y) v c(y v z)) v u) v c(y)=c(y). given clause #217: (wt=15) 1674 [para_into,1155,1253] c(x) v (c(y v x) v c(z v x))=c(x). given clause #218: (wt=15) 1852 [para_from,1846,1155] c(x) v (c(x v y) v c(z v x))=c(x). given clause #219: (wt=15) 1854 [para_from,1846,1153] (c(c(x) v y) v c(z v c(x))) v x=x. given clause #220: (wt=15) 1943 [para_from,1179,1443,demod,730] x v (c(c(x) v y) v c(c(x) v z))=x. given clause #221: (wt=17) 1363 [para_into,1359,1359,demod,730,730] c(c(x) v y) v ((x v z) v u)= (x v z) v u. given clause #222: (wt=15) 1961 [para_from,1381,1143,demod,730] (x v y) v (x v (y v z))=x v (y v z). given clause #223: (wt=11) 5965 [para_into,1961,1615,flip.1] x v (c(x) v y)=x v c(x). given clause #224: (wt=11) 5967 [para_into,1961,1457,flip.1] c(x) v (x v y)=c(x) v x. given clause #225: (wt=11) 6097 [para_into,5965,1846] x v (y v c(x))=x v c(x). given clause #226: (wt=30) 1371 [para_into,1359,1153] c(x v y) v c(c(z v c(x)) v c(c(x) v u))=c(c(z v c(x)) v c(c(x) v u)). given clause #227: (wt=11) 6131 [para_into,5965,2031] c(x) v (y v x)=x v c(x). given clause #228: (wt=11) 6133 [para_into,5965,1846] (c(x) v y) v x=x v c(x). given clause #229: (wt=11) 6207 [para_from,5965,1911,demod,6124,6098,5966,6124,flip.1] (x v y) v c(y)=y v c(y). given clause #230: (wt=11) 6412 [para_from,5967,1640,demod,6229,flip.1] (x v y) v c(x)=x v c(x). given clause #231: (wt=27) 1373 [para_into,1359,1141] c(c(x) v y) v c(c(x v z) v c(x v u))=c(c(x v z) v c(x v u)). given clause #232: (wt=11) 6495 [para_into,6097,1846] (x v c(y)) v y=y v c(y). given clause #233: (wt=13) 6091 [para_into,5965,2031] x v (y v (z v c(x)))=x v c(x). given clause #234: (wt=13) 6093 [para_into,5965,1979] x v (y v (c(x) v z))=x v c(x). given clause #235: (wt=13) 6095 [para_into,5965,1911] x v ((y v c(x)) v z)=x v c(x). given clause #236: (wt=27) 1375 [para_into,1359,1060] c(c(x) v y) v c(c(z v x) v c(x v u))=c(c(z v x) v c(x v u)). given clause #237: (wt=13) 6108 [para_into,5965,1391] x v ((c(x) v y) v z)=x v c(x). given clause #238: (wt=13) 6170 [copy,6114,flip.1,demod,6124,6140,flip.1] (c(x) v y) v (x v z)=x v c(x). given clause #239: (wt=13) 6172 [copy,6115,flip.1,demod,6124,6140,flip.1] (c(x) v y) v (z v x)=x v c(x). given clause #240: (wt=13) 6217 [back_demod,6185,demod,6208,6124,6208,flip.1] (x v (y v z)) v c(z)=z v c(z). given clause #241: (wt=23) 1385 [para_from,1359,1141,demod,730,730,730] (c(c((x v y) v z) v u) v x) v ((x v y) v z)= (x v y) v z. given clause #242: (wt=13) 6228 [back_demod,6165,demod,6208] (x v y) v (z v c(y))=y v c(y). given clause #243: (wt=13) 6230 [back_demod,6159,demod,6208] (x v y) v (c(y) v z)=y v c(y). given clause #244: (wt=13) 6263 [para_into,5967,2031] c(x) v (y v (z v x))=c(x) v x. given clause #245: (wt=13) 6265 [para_into,5967,1979] c(x) v (y v (x v z))=c(x) v x. given clause #246: (wt=23) 1387 [para_from,1359,1153,demod,730] (c(x v c((y v z) v u)) v y) v ((y v z) v u)= (y v z) v u. given clause #247: (wt=13) 6269 [para_into,5967,1911] c(x) v ((y v x) v z)=c(x) v x. given clause #248: (wt=13) 6281 [para_into,5967,1391] c(x) v ((x v y) v z)=c(x) v x. given clause #249: (wt=13) 6455 [back_demod,6339,demod,6413] (x v y) v (z v c(x))=x v c(x). given clause #250: (wt=13) 6457 [back_demod,6337,demod,6413] (x v y) v (c(x) v z)=x v c(x). given clause #251: (wt=23) 1395 [para_from,1359,1141,demod,730,730,730] (x v c(c((x v y) v z) v u)) v ((x v y) v z)= (x v y) v z. given clause #252: (wt=13) 6507 [back_demod,6163,demod,6496] (x v c(y)) v (z v y)=y v c(y). given clause #253: (wt=13) 6509 [back_demod,6161,demod,6496] (x v c(y)) v (y v z)=y v c(y). given clause #254: (wt=13) 6762 [para_into,6133,2031] (x v (y v c(z))) v z=z v c(z). given clause #255: (wt=13) 6764 [para_into,6133,1979] (x v (c(y) v z)) v y=y v c(y). given clause #256: (wt=18) 1437 [para_into,1383,1383] c(x v y) v ((c(x) v z) v u)= (c(x) v z) v u. given clause #257: (wt=13) 6766 [para_into,6133,1911] ((x v c(y)) v z) v y=y v c(y). given clause #258: (wt=13) 6771 [para_into,6133,1391] ((c(x) v y) v z) v x=x v c(x). given clause #259: (wt=13) 6792 [para_into,6207,1977] (x v (y v z)) v c(y)=y v c(y). given clause #260: (wt=13) 6794 [para_into,6207,1909] ((x v y) v z) v c(y)=y v c(y). given clause #261: (wt=17) 1497 [para_into,1143,1383,demod,1384,1384] (c((c(x) v y) v z) v c(c(x) v u)) v x=x. given clause #262: (wt=13) 6800 [para_into,6207,1389] ((x v y) v z) v c(x)=x v c(x). given clause #263: (wt=13) 7256 [para_into,6093,1219,demod,6229,7136,flip.1] x v (y v c(x v y))=y v c(y). given clause #264: (wt=13) 9611 [para_into,7256,1846] x v (y v c(y v x))=y v c(y). given clause #265: (wt=13) 9613 [para_into,7256,1846] x v (c(x v y) v y)=y v c(y). given clause #266: (wt=17) 1499 [para_into,1143,1359,demod,730,1360,1360] (c((x v y) v z) v c(x v u)) v c(x)=c(x). given clause #267: (wt=13) 9615 [para_into,7256,1846] (x v c(y v x)) v y=x v c(x). given clause #268: (wt=13) 9619 [para_into,9611,9611,demod,1478] (x v c(x v y)) v y=y v c(y). given clause #269: (wt=13) 9621 [para_into,9611,1846] x v (c(y v x) v y)=y v c(y). given clause #270: (wt=13) 9625 [para_into,9613,1846] (c(x v y) v y) v x=y v c(y). given clause #271: (wt=21) 1501 [para_into,1143,1153,demod,1154,1154] ((c(x v c(y)) v c(c(y) v z)) v c(c(y) v u)) v y=y. given clause #272: (wt=13) 9733 [para_into,9619,1846] (c(x v y) v x) v y=y v c(y). given clause #273: (wt=15) 2011 [para_from,1686,1143,demod,730] (x v y) v (x v (z v y))=x v (z v y). given clause #274: (wt=15) 2081 [para_from,1758,1151,demod,730] (x v y) v (y v (x v z))=y v (x v z). given clause #275: (wt=15) 2089 [para_from,1881,1151,demod,730] (x v y) v (y v (z v x))=y v (z v x). given clause #276: (wt=25) 1503 [para_into,1143,1143,demod,1144,1144] ((x v c(c(x v y) v z)) v c(c(x v y) v u)) v (x v y)=x v y. given clause #277: (wt=13) 10439 [para_into,2089,2011,demod,10276,2012] (x v y) v (z v y)=z v (x v y). ----> UNIT CONFLICT at 4.34 sec ----> 11001 [binary,11000,1] $Ans(AJ). Length of proof is 79. Level of proof is 24. ---------------- PROOF ---------------- 1 [] A v (B v C)!=B v (A v C)|$Ans(AJ). 8 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. 10 [] x v y=f(f(x,x),f(y,y)). 11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y. 13 [] x^y=f(f(x,y),f(x,y)). 14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y. 16 [] c(x)=f(x,x). 18,17 [copy,16,flip.1] f(x,x)=c(x). 20,19 [back_demod,14,demod,18] c(f(x,y))=x^y. 21 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y. 23 [back_demod,8,demod,18] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(c(x),x)),z)))=y. 31,30 [para_into,21,17] c(c(x))=x v x. 35 [para_from,21,19,flip.1] c(x)^c(y)=c(x v y). 38,37 [para_into,30,30] c(x v x)=c(x) v c(x). 41 [para_from,30,21] f(c(x),y v y)=x v c(y). 44,43 [para_from,30,21] f(x v x,c(y))=c(x) v y. 45 [para_into,23,21,demod,31,44] f(f(f(x v y,f(c(y),z)),u),f(c(y),f(f(c(y),c(x) v x),z)))=c(y). 47 [para_into,23,17] f(f(f(c(x),f(x,y)),z),f(x,f(f(x,f(c(x),x)),y)))=x. 49 [para_into,23,21] f(f(f(f(x,c(y)),y v z),u),f(c(y),f(f(c(y),f(c(x),x)),c(z))))=c(y). 53 [para_into,23,23,demod,20] f(f(x,y),f(x,f(f(x,f(f(z,x)^f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(c(z),z)),u))))=x. 55 [para_into,23,17,demod,18,31] f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x)))=x. 71 [para_into,35,30] (x v x)^c(y)=c(c(x) v y). 84,83 [para_into,41,30] f(x v x,y v y)=c(x) v c(y). 131 [para_into,45,21] f(f(f(x v y,y v z),u),f(c(y),f(f(c(y),c(x) v x),c(z))))=c(y). 151 [para_into,71,30] (x v x)^ (y v y)=c(c(x) v c(y)). 259 [para_into,49,43,demod,38,84,31] f(f(f(c(x) v y,y v z),u),f(c(y),f(f(c(y),(x v x) v c(x)),c(z))))=c(y). 263 [para_into,49,17,demod,20] f(f(x,c(y))^ (y v z),f(c(y),f(f(c(y),f(c(x),x)),c(z))))=c(y). 467 [para_from,53,47] f(c(x),f(x,f(f(x,f(c(x),x)),y)))=x. 469 [para_from,53,45] f(x v y,f(c(y),f(f(c(y),c(x) v x),z)))=c(y). 526,525 [para_into,467,53,demod,18,18,31] x v x=x. 531 [para_into,467,47,demod,20] f(c(x)^f(x,y),f(f(c(x),f(x,y)),x))=f(c(x),f(x,y)). 661 [back_demod,259,demod,526] f(f(f(c(x) v y,y v z),u),f(c(y),f(f(c(y),x v c(x)),c(z))))=c(y). 700,699 [back_demod,151,demod,526,526] x^y=c(c(x) v c(y)). 725,724 [back_demod,83,demod,526,526] f(x,y)=c(x) v c(y). 727 [back_demod,55,demod,526,725,725,31,526,725,725,725,725] 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. 730,729 [back_demod,30,demod,526] c(c(x))=x. 740 [back_demod,531,demod,725,700,730,725,725,730,725,725,730,725,725,730] (x v c(c(x) v c(y))) v c(c(x v c(c(x) v c(y))) v c(x))=x v c(c(x) v c(y)). 755,754 [back_demod,263,demod,725,730,700,725,730,725,730,725,730,725,730,725,730] (c(c(x) v y) v c(y v z)) v c(y v c(c(y v c(x v c(x))) v z))=c(y). 782 [back_demod,661,demod,725,725,725,730,725,730,725,730,725] c(c(c(c(x) v y) v c(y v z)) v c(u)) v c(y v c(c(y v c(x v c(x))) v z))=c(y). 794 [back_demod,469,demod,725,730,725,725,730,725] c(x v y) v c(y v c(c(y v c(c(x) v x)) v c(z)))=c(y). 800 [back_demod,131,demod,725,725,725,730,725,730,725,730,725] c(c(c(x v y) v c(y v z)) v c(u)) v c(y v c(c(y v c(c(x) v x)) v z))=c(y). 810 [para_into,727,729] c(c(x) v y) v c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 813,812 [para_into,727,525] c(c(x) v c(c(c(x) v c(x v c(x))) v c(x)))=x. 816 [back_demod,810,demod,813] c(c(x) v y) v x=x. 819,818 [para_into,816,729] c(x v y) v c(x)=c(x). 822 [back_demod,740,demod,819,730] (x v c(c(x) v c(y))) v x=x v c(c(x) v c(y)). 830 [para_into,818,818,demod,730,730,730] x v (x v y)=x v y. 871,870 [para_into,822,729,demod,730] (x v c(c(x) v y)) v x=x v c(c(x) v y). 872 [para_into,822,818,demod,730,819,730] ((x v y) v x) v (x v y)= (x v y) v x. 875,874 [para_into,872,818,demod,819,819] (c(x) v c(x v y)) v c(x)=c(x) v c(x v y). 980 [para_from,754,830,demod,755] (c(c(x) v y) v c(y v z)) v c(y)=c(y). 1030 [para_into,782,816,demod,730,730] c((x v y) v c(z)) v c(x v c(c(x v c(c(x v y) v (x v y))) v y))=c(x). 1060 [para_into,980,729] (c(x v y) v c(y v z)) v c(y)=c(y). 1072 [para_into,980,818,demod,730,730,871,730] x v c(c(x) v y)=x. 1075 [para_into,980,816,demod,875] c(x) v c(x v y)=c(x). 1093 [para_into,1072,818,demod,730] (x v y) v x=x v y. 1143 [para_into,1060,1075,demod,730,730,730] (x v c(c(x v y) v z)) v (x v y)=x v y. 1151 [para_into,1060,818,demod,730,730,730] (c(x v c(y v z)) v y) v (y v z)=y v z. 1220,1219 [para_into,794,818,demod,730,526] c(x v y) v c(y)=c(y). 1243 [para_into,1219,729,demod,730] c(x v c(y)) v y=y. 1253 [para_from,1219,816,demod,730] x v (y v x)=y v x. 1257 [para_from,1219,1093,demod,1220] c(x) v c(y v x)=c(x). 1322,1321 [para_into,800,1243] c(x v c(c(x v c(c(y) v y)) v z))=c(x). 1335 [back_demod,1030,demod,1322] c((x v y) v c(z)) v c(x)=c(x). 1359 [para_into,1335,729] c((x v y) v z) v c(x)=c(x). 1383 [para_into,1359,729,demod,730] c((c(x) v y) v z) v x=x. 1439 [para_into,1383,1253] c((x v c(y)) v z) v y=y. 1442,1441 [para_into,1383,1253] c(x v (c(y) v z)) v y=y. 1532,1531 [para_into,1439,1253] c(x v (y v c(z))) v z=z. 1583 [para_from,1441,1093,demod,1442] x v c(y v (c(x) v z))=x. 1641,1640 [para_into,1151,1257,demod,730] (x v y) v (y v x)=y v x. 1686 [para_into,1531,729] c(x v (y v z)) v c(z)=c(z). 1710 [para_from,1531,1093,demod,1532] x v c(y v (z v c(x)))=x. 1758 [para_into,1583,729] c(x) v c(y v (x v z))=c(x). 1846 [para_from,1640,1093,demod,1641,1641] x v y=y v x. 1881 [para_into,1710,729] c(x) v c(y v (z v x))=c(x). 2012,2011 [para_from,1686,1143,demod,730] (x v y) v (x v (z v y))=x v (z v y). 2081 [para_from,1758,1151,demod,730] (x v y) v (y v (x v z))=y v (x v z). 2089 [para_from,1881,1151,demod,730] (x v y) v (y v (z v x))=y v (z v x). 10276,10275 [para_into,2081,1846] (x v (y v z)) v (y v x)=x v (y v z). 10439 [para_into,2089,2011,demod,10276,2012] (x v y) v (z v y)=z v (x v y). 10467 [copy,10439,flip.1] x v (y v z)= (y v z) v (x v z). 10981,10980 [para_into,10439,1846] (x v y) v (z v y)=x v (z v y). 11000 [back_demod,10467,demod,10981] x v (y v z)=y v (x v z). 11001 [binary,11000,1] $Ans(AJ). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 277 clauses generated 69324 para_from generated 30777 para_into generated 38547 demod & eval rewrites 172418 clauses wt,lit,sk delete 3873 tautologies deleted 0 clauses forward subsumed 63478 (subsumed by sos) 1285 unit deletions 0 factor simplifications 0 clauses kept 6319 new demodulators 4667 empty clauses 6 clauses back demodulated 2708 clauses back subsumed 8 usable size 173 sos size 3430 demodulators size 3011 passive size 6 hot size 0 Kbytes malloced 8302 ----------- times (seconds) ----------- user CPU time 4.34 (0 hr, 0 min, 4 sec) system CPU time 0.27 (0 hr, 0 min, 0 sec) wall-clock time 4 (0 hr, 0 min, 4 sec) input time 0.00 clausify time 0.00 process input 0.00 pick given time 0.04 para_into time 0.20 para_from time 0.22 pre_process time 2.16 renumber time 0.11 demod time 1.16 order equalities 0.09 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.10 hints keep time 0.00 sort lits time 0.00 forward subsume 0.17 delete cl time 0.07 keep cl time 0.26 hints time 0.00 print_cl time 0.00 conflict time 0.01 new demod time 0.10 post_process time 1.67 back demod time 1.44 back subsume 0.21 factor time 0.00 unindex time 0.32 That finishes the proof of the theorem. Process 2353 finished Mon Sep 15 12:17:30 2003