----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:34:39 2003 The command was "otter". The process ID is 26009. include("ortholattice-header"). ------- start included file ortholattice-header------- op(400,infix,^). op(400,infix,v). lex([A,B,C,D,0,1,x v x,c(x),x^x,f(x,x)]). set(anl_eq). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(process_input). dependent: set(lrpo). assign(pick_given_ratio,3). assign(max_weight,25). clear(detailed_history). assign(max_seconds,60). assign(max_mem,100000). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). clear(print_kept). assign(stats_level,1). list(usable). 0 [] x=x. end_of_list. ------- end included file ortholattice-header------- list(sos). 0 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 0 [] f(f(x,x),f(x,y))=x. 0 [] f(x,f(x,x))=f(y,f(y,y)). 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 c(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=19): 8 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). ** KEPT (pick-wt=9): 9 [] f(f(x,x),f(x,y))=x. ---> New Demodulator: 10 [new_demod,9] f(f(x,x),f(x,y))=x. ** KEPT (pick-wt=11): 11 [] f(x,f(x,x))=f(y,f(y,y)). ** KEPT (pick-wt=11): 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. ---> New Demodulator: 14 [new_demod,13] f(f(x,x),f(y,y))=x v y. ** KEPT (pick-wt=11): 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. ---> New Demodulator: 17 [new_demod,16] f(f(x,y),f(x,y))=x^y. ** KEPT (pick-wt=6): 19 [copy,18,flip.1] f(x,x)=c(x). ---> New Demodulator: 20 [new_demod,19] f(x,x)=c(x). ** KEPT (pick-wt=13): 21 [copy,8,flip.1,demod,20,20] f(x,c(f(y,z)))=f(y,c(f(x,z))). >>>> Starting back demodulation with 10. ** KEPT (pick-wt=9): 22 [copy,11,flip.1,demod,20,20] f(x,c(x))=f(y,c(y)). >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 17. >> back demodulating 8 with 17. >>>> Starting back demodulation with 20. >> back demodulating 16 with 20. >> back demodulating 13 with 20. >> back demodulating 11 with 20. >> back demodulating 9 with 20. ** KEPT (pick-wt=11): 29 [copy,21,flip.1,demod,24,24] f(x,y^z)=f(y,x^z). Following clause subsumed by 22 during input processing: 0 [copy,22,flip.1] f(x,c(x))=f(y,c(y)). >>>> Starting back demodulation with 24. >> back demodulating 21 with 24. >>>> Starting back demodulation with 26. >>>> Starting back demodulation with 28. Following clause subsumed by 29 during input processing: 0 [copy,29,flip.1] f(x,y^z)=f(y,x^z). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=6) 19 [copy,18,flip.1] f(x,x)=c(x). given clause #2: (wt=8) 23 [back_demod,16,demod,20] c(f(x,y))=x^y. given clause #3: (wt=7) 30 [para_into,23,19,flip.1] x^x=c(c(x)). given clause #4: (wt=8) 27 [back_demod,9,demod,20] f(c(x),f(x,y))=x. ----> UNIT CONFLICT at 0.01 sec ----> 38 [binary,36,4] $Ans(CC). Length of proof is 3. Level of proof is 3. ---------------- PROOF ---------------- 4 [] c(c(A))!=A|$Ans(CC). 9 [] f(f(x,x),f(x,y))=x. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 27 [back_demod,9,demod,20] f(c(x),f(x,y))=x. 36 [para_into,27,19,demod,20] c(c(x))=x. 38 [binary,36,4] $Ans(CC). ------------ end of proof ------------- given clause #5: (wt=9) 22 [copy,11,flip.1,demod,20,20] f(x,c(x))=f(y,c(y)). given clause #6: (wt=5) 36 [para_into,27,19,demod,20] c(c(x))=x. given clause #7: (wt=5) 39 [back_demod,30,demod,37] x^x=x. given clause #8: (wt=8) 48 [para_into,36,23,flip.1] f(x,y)=c(x^y). given clause #9: (wt=9) 47 [para_from,22,23,demod,24] x^c(x)=y^c(y). given clause #10: (wt=8) 62 [back_demod,50,demod,60] x v (y^c(y))=x. given clause #11: (wt=8) 66 [para_into,62,36] x v (c(y)^y)=x. given clause #12: (wt=9) 64 [para_into,47,36] c(x)^x=y^c(y). given clause #13: (wt=15) 52 [back_demod,44,demod,49,49,49] c(x^c(x))=c(c(y^z)^ (y^z)). given clause #14: (wt=9) 65 [copy,64,flip.1] x^c(x)=c(y)^y. given clause #15: (wt=9) 81 [para_into,65,36] c(x)^x=c(y)^y. given clause #16: (wt=10) 54 [back_demod,41,demod,49] c(x)^c(x^y)=c(x). given clause #17: (wt=15) 53 [back_demod,43,demod,49,49,49] c(c(x^y)^ (x^y))=c(z^c(z)). given clause #18: (wt=9) 87 [para_into,54,36,demod,37] x^c(c(x)^y)=x. given clause #19: (wt=9) 89 [para_into,54,81,demod,37,37] x^c(c(y)^y)=x. given clause #20: (wt=9) 91 [para_into,54,64,demod,37,37] x^c(y^c(y))=x. given clause #21: (wt=13) 58 [back_demod,29,demod,49,49] c(x^ (y^z))=c(y^ (x^z)). given clause #22: (wt=9) 103 [para_into,58,91,demod,92] c(x^y)=c(y^x). given clause #23: (wt=7) 158 [para_into,103,54,demod,37,60,flip.1] (x^y) v x=x. given clause #24: (wt=5) 187 [para_into,158,91] x v x=x. given clause #25: (wt=10) 59 [back_demod,25,demod,49] c(c(x)^c(y))=x v y. ----> UNIT CONFLICT at 0.02 sec ----> 215 [binary,214,5] $Ans(ONE). Length of proof is 15. Level of proof is 7. ---------------- PROOF ---------------- 5 [] A v c(A)!=B v c(B)|$Ans(ONE). 9 [] f(f(x,x),f(x,y))=x. 11 [] f(x,f(x,x))=f(y,f(y,y)). 12 [] x v y=f(f(x,x),f(y,y)). 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] x^y=f(f(x,y),f(x,y)). 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 22 [copy,11,flip.1,demod,20,20] f(x,c(x))=f(y,c(y)). 24,23 [back_demod,16,demod,20] c(f(x,y))=x^y. 25 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. 27 [back_demod,9,demod,20] f(c(x),f(x,y))=x. 36 [para_into,27,19,demod,20] c(c(x))=x. 47 [para_from,22,23,demod,24] x^c(x)=y^c(y). 49,48 [para_into,36,23,flip.1] f(x,y)=c(x^y). 59 [back_demod,25,demod,49] c(c(x)^c(y))=x v y. 64 [para_into,47,36] c(x)^x=y^c(y). 65 [copy,64,flip.1] x^c(x)=c(y)^y. 210,209 [para_into,59,36] c(c(x)^y)=x v c(y). 214 [para_into,59,65,demod,210] x v c(x)=y v c(y). 215 [binary,214,5] $Ans(ONE). ------------ end of proof ------------- given clause #26: (wt=7) 182 [para_from,103,36,demod,37] x^y=y^x. given clause #27: (wt=7) 211 [para_into,59,87,demod,37,37,flip.1] x v (x^y)=x. given clause #28: (wt=7) 218 [para_into,59,103,demod,205,37] x v y=y v x. given clause #29: (wt=15) 107 [para_into,58,65] c(x^ (c(y)^y))=c(z^ (x^c(z))). given clause #30: (wt=7) 269 [para_from,182,158] (x^y) v y=y. given clause #31: (wt=7) 273 [para_into,211,182] x v (y^x)=x. given clause #32: (wt=8) 191 [para_into,158,65] (c(x)^x) v y=y. given clause #33: (wt=11) 112 [para_into,58,39,flip.1] c(x^ (y^x))=c(y^x). given clause #34: (wt=8) 195 [para_into,158,47] (x^c(x)) v y=y. given clause #35: (wt=8) 223 [back_demod,162,demod,205] x^ (c(y) v x)=x. given clause #36: (wt=7) 330 [para_into,223,36] x^ (y v x)=x. given clause #37: (wt=13) 124 [para_from,58,89] x^c(y^ (c(y^z)^z))=x. given clause #38: (wt=7) 340 [para_into,330,218] x^ (x v y)=x. given clause #39: (wt=7) 344 [para_into,330,182] (x v y)^y=y. given clause #40: (wt=7) 380 [para_into,340,182] (x v y)^x=x. given clause #41: (wt=11) 126 [para_from,58,87] x^c(y^ (c(x)^z))=x. given clause #42: (wt=8) 233 [back_demod,91,demod,205] x^ (c(y) v y)=x. given clause #43: (wt=8) 257 [back_demod,89,demod,210] x^ (y v c(y))=x. given clause #44: (wt=8) 422 [para_into,233,182] (c(x) v x)^y=y. given clause #45: (wt=12) 128 [para_from,58,54] c(x)^c(y^ (x^z))=c(x). given clause #46: (wt=8) 436 [para_into,257,182] (x v c(x))^y=y. given clause #47: (wt=9) 213 [para_into,59,81,demod,210] x v c(x)=c(y) v y. given clause #48: (wt=9) 214 [para_into,59,65,demod,210] x v c(x)=y v c(y). given clause #49: (wt=16) 132 [para_from,58,66] x v (c(y^ (z^u))^ (z^ (y^u)))=x. given clause #50: (wt=9) 216 [para_into,59,64,demod,205] c(x) v x=c(y) v y. given clause #51: (wt=9) 217 [para_into,59,47,demod,205] c(x) v x=y v c(y). given clause #52: (wt=9) 324 [para_from,112,36,demod,37,flip.1] x^ (y^x)=y^x. given clause #53: (wt=16) 134 [para_from,58,62] x v ((y^ (z^u))^c(z^ (y^u)))=x. given clause #54: (wt=9) 338 [para_into,330,273] (x^y)^y=x^y. given clause #55: (wt=9) 342 [para_into,330,211] (x^y)^x=x^y. given clause #56: (wt=9) 348 [para_from,330,273] (x v y) v y=x v y. given clause #57: (wt=17) 140 [para_from,58,81] c(x^ (y^z))^ (y^ (x^z))=c(u)^u. given clause #58: (wt=9) 350 [para_from,330,269] x v (y v x)=y v x. given clause #59: (wt=9) 382 [para_from,340,273] (x v y) v x=x v y. given clause #60: (wt=9) 384 [para_from,340,269] x v (x v y)=x v y. given clause #61: (wt=17) 141 [para_from,58,65] (x^ (y^z))^c(y^ (x^z))=c(u)^u. given clause #62: (wt=9) 388 [para_into,344,211] x^ (x^y)=x^y. given clause #63: (wt=9) 428 [para_from,233,191] c(c(x) v x) v y=y. given clause #64: (wt=9) 430 [para_from,233,66] x v c(c(y) v y)=x. given clause #65: (wt=17) 142 [para_from,58,64] c(x^ (y^z))^ (y^ (x^z))=u^c(u). given clause #66: (wt=9) 442 [para_from,257,191] c(x v c(x)) v y=y. given clause #67: (wt=9) 444 [para_from,257,66] x v c(y v c(y))=x. given clause #68: (wt=10) 164 [para_from,103,54] c(x)^c(y^x)=c(x). given clause #69: (wt=22) 143 [para_from,58,54] c(x^ (y^z))^c((y^ (x^z))^u)=c(y^ (x^z)). given clause #70: (wt=10) 204 [para_into,59,36] c(x^c(y))=c(x) v y. ----> UNIT CONFLICT at 0.11 sec ----> 1362 [binary,1360,6] $Ans(DEF_SS). Length of proof is 12. Level of proof is 8. ---------------- PROOF ---------------- 6 [] f(A,B)!=c(A) v c(B)|$Ans(DEF_SS). 9 [] f(f(x,x),f(x,y))=x. 12 [] x v y=f(f(x,x),f(y,y)). 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] x^y=f(f(x,y),f(x,y)). 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 23 [back_demod,16,demod,20] c(f(x,y))=x^y. 25 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. 27 [back_demod,9,demod,20] f(c(x),f(x,y))=x. 36 [para_into,27,19,demod,20] c(c(x))=x. 49,48 [para_into,36,23,flip.1] f(x,y)=c(x^y). 59 [back_demod,25,demod,49] c(c(x)^c(y))=x v y. 204 [para_into,59,36] c(x^c(y))=c(x) v y. 913,912 [para_into,204,36] c(x^y)=c(x) v c(y). 1360 [back_demod,48,demod,913] f(x,y)=c(x) v c(y). 1362 [binary,1360,6] $Ans(DEF_SS). ------------ end of proof ------------- given clause #71: (wt=9) 914 [para_into,204,380,demod,37,flip.1] c(c(x) v y) v x=x. ----> UNIT CONFLICT at 0.13 sec ----> 1367 [binary,1365,2] $Ans(B1_rewritten). Length of proof is 30. Level of proof is 14. ---------------- PROOF ---------------- 2 [] A v c(c(A) v c(B))!=A|$Ans(B1_rewritten). 8 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 9 [] f(f(x,x),f(x,y))=x. 11 [] f(x,f(x,x))=f(y,f(y,y)). 12 [] x v y=f(f(x,x),f(y,y)). 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] x^y=f(f(x,y),f(x,y)). 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 21 [copy,8,flip.1,demod,20,20] f(x,c(f(y,z)))=f(y,c(f(x,z))). 22 [copy,11,flip.1,demod,20,20] f(x,c(x))=f(y,c(y)). 24,23 [back_demod,16,demod,20] c(f(x,y))=x^y. 25 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. 27 [back_demod,9,demod,20] f(c(x),f(x,y))=x. 29 [copy,21,flip.1,demod,24,24] f(x,y^z)=f(y,x^z). 37,36 [para_into,27,19,demod,20] c(c(x))=x. 41 [para_from,27,23,flip.1] c(x)^f(x,y)=c(x). 47 [para_from,22,23,demod,24] x^c(x)=y^c(y). 49,48 [para_into,36,23,flip.1] f(x,y)=c(x^y). 54 [back_demod,41,demod,49] c(x)^c(x^y)=c(x). 58 [back_demod,29,demod,49,49] c(x^ (y^z))=c(y^ (x^z)). 59 [back_demod,25,demod,49] c(c(x)^c(y))=x v y. 64 [para_into,47,36] c(x)^x=y^c(y). 87 [para_into,54,36,demod,37] x^c(c(x)^y)=x. 92,91 [para_into,54,64,demod,37,37] x^c(y^c(y))=x. 103 [para_into,58,91,demod,92] c(x^y)=c(y^x). 162 [para_from,103,87] x^c(y^c(x))=x. 182 [para_from,103,36,demod,37] x^y=y^x. 205,204 [para_into,59,36] c(x^c(y))=c(x) v y. 218 [para_into,59,103,demod,205,37] x v y=y v x. 223 [back_demod,162,demod,205] x^ (c(y) v x)=x. 330 [para_into,223,36] x^ (y v x)=x. 340 [para_into,330,218] x^ (x v y)=x. 380 [para_into,340,182] (x v y)^x=x. 914 [para_into,204,380,demod,37,flip.1] c(c(x) v y) v x=x. 1365 [para_into,914,218] x v c(c(x) v y)=x. 1367 [binary,1365,2] $Ans(B1_rewritten). ------------ end of proof ------------- given clause #72: (wt=9) 916 [para_into,204,344,demod,37,flip.1] c(x v c(y)) v y=y. given clause #73: (wt=11) 146 [para_from,58,36,demod,37] x^ (y^z)=y^ (x^z). given clause #74: (wt=9) 919 [para_into,204,128,demod,37,37,flip.1] x v (y^ (x^z))=x. given clause #75: (wt=9) 1360 [back_demod,48,demod,913] f(x,y)=c(x) v c(y). given clause #76: (wt=9) 1365 [para_into,914,218] x v c(c(x) v y)=x. given clause #77: (wt=11) 197 [para_into,158,66] (c(x)^x)^y=c(x)^x. given clause #78: (wt=9) 1374 [para_into,916,218] x v c(y v c(x))=x. given clause #79: (wt=9) 1447 [para_from,146,158] (x^ (y^z)) v y=y. given clause #80: (wt=9) 1454 [para_into,919,324] x v (y^ (z^x))=x. given clause #81: (wt=11) 199 [para_into,158,62] (x^c(x))^y=x^c(x). given clause #82: (wt=9) 1458 [para_into,919,342] x v ((x^y)^z)=x. given clause #83: (wt=9) 1470 [para_into,1447,324] (x^ (y^z)) v z=z. given clause #84: (wt=9) 1474 [para_into,1447,342] ((x^y)^z) v x=x. given clause #85: (wt=11) 201 [para_into,59,103,demod,60] (x^y) v z= (y^x) v z. given clause #86: (wt=9) 1478 [para_into,1454,342] x v ((y^x)^z)=x. given clause #87: (wt=9) 1496 [para_into,1470,342] ((x^y)^z) v y=y. given clause #88: (wt=10) 424 [para_into,233,81] c(x)^x=c(c(y) v y). given clause #89: (wt=15) 203 [para_into,59,58,demod,60] (x^ (y^z)) v u= (y^ (x^z)) v u. given clause #90: (wt=10) 425 [para_into,233,64] x^c(x)=c(c(y) v y). given clause #91: (wt=10) 426 [copy,424,flip.1] c(c(x) v x)=c(y)^y. given clause #92: (wt=10) 427 [copy,425,flip.1] c(c(x) v x)=y^c(y). given clause #93: (wt=11) 206 [para_into,59,103,demod,205,37] x v (y^z)=x v (z^y). given clause #94: (wt=10) 438 [para_into,257,81] c(x)^x=c(y v c(y)). given clause #95: (wt=10) 439 [para_into,257,64] x^c(x)=c(y v c(y)). given clause #96: (wt=10) 440 [copy,438,flip.1] c(x v c(x))=c(y)^y. given clause #97: (wt=15) 208 [para_into,59,58,demod,205,37] x v (y^ (z^u))=x v (z^ (y^u)). given clause #98: (wt=10) 441 [copy,439,flip.1] c(x v c(x))=y^c(y). given clause #99: (wt=10) 504 [para_into,132,81,demod,295,210,437] x v (c(y)^ (z^y))=x. given clause #100: (wt=10) 506 [para_into,132,65,demod,295,210,437] x v (y^ (z^c(y)))=x. given clause #101: (wt=14) 219 [copy,202,flip.1,demod,205] (c(x)^c(y)) v z=c(x v y) v z. given clause #102: (wt=10) 912 [para_into,204,36] c(x^y)=c(x) v c(y). ----> UNIT CONFLICT at 0.17 sec ----> 1812 [binary,1810,3] $Ans(DM). Length of proof is 12. Level of proof is 8. ---------------- PROOF ---------------- 3 [] A^B!=c(c(A) v c(B))|$Ans(DM). 9 [] f(f(x,x),f(x,y))=x. 12 [] x v y=f(f(x,x),f(y,y)). 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] x^y=f(f(x,y),f(x,y)). 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 23 [back_demod,16,demod,20] c(f(x,y))=x^y. 25 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. 27 [back_demod,9,demod,20] f(c(x),f(x,y))=x. 36 [para_into,27,19,demod,20] c(c(x))=x. 49,48 [para_into,36,23,flip.1] f(x,y)=c(x^y). 59 [back_demod,25,demod,49] c(c(x)^c(y))=x v y. 204 [para_into,59,36] c(x^c(y))=c(x) v y. 912 [para_into,204,36] c(x^y)=c(x) v c(y). 1810 [para_from,912,36,flip.1] x^y=c(c(x) v c(y)). 1812 [binary,1810,3] $Ans(DM). ------------ end of proof ------------- given clause #103: (wt=10) 1363 [para_into,914,36] c(x v y) v c(x)=c(x). given clause #104: (wt=10) 1372 [para_into,916,36] c(x v y) v c(y)=c(y). given clause #105: (wt=11) 418 [para_into,233,380,flip.1] (c(x) v x) v y=c(x) v x. given clause #106: (wt=10) 1460 [para_into,1365,36] c(x) v c(x v y)=c(x). given clause #107: (wt=10) 1464 [para_into,1374,36] c(x) v c(y v x)=c(x). given clause #108: (wt=10) 1810 [para_from,912,36,flip.1] x^y=c(c(x) v c(y)). given clause #109: (wt=11) 420 [para_into,233,344,flip.1] x v (c(y) v y)=c(y) v y. given clause #110: (wt=11) 432 [para_into,257,380,flip.1] (x v c(x)) v y=x v c(x). given clause #111: (wt=11) 434 [para_into,257,344,flip.1] x v (y v c(y))=y v c(y). given clause #112: (wt=11) 746 [para_into,430,428] c(c(x) v x)=c(c(y) v y). given clause #113: (wt=11) 807 [para_into,442,430] c(x v c(x))=c(c(y) v y). given clause #114: (wt=11) 814 [copy,807,flip.1] c(c(x) v x)=c(y v c(y)). given clause #115: (wt=11) 819 [para_into,444,442] c(x v c(x))=c(y v c(y)). given clause #116: (wt=11) 1837 [back_demod,1686,demod,1811,37] x v c((y v z) v c(z))=x. given clause #117: (wt=18) 927 [back_demod,877,demod,913,913,913,37,913,913,37] (c(x) v (c(y) v x)) v c(z)=c(x) v (c(y) v x). given clause #118: (wt=11) 1839 [back_demod,1684,demod,1811,37] x v c((y v z) v c(y))=x. given clause #119: (wt=11) 2104 [para_into,1837,1464,demod,37] x v c(c(y) v (z v y))=x. given clause #120: (wt=11) 2106 [para_into,1837,1460,demod,37] x v c(c(y) v (y v z))=x. given clause #121: (wt=18) 929 [back_demod,875,demod,913,913,37,913,913] (x v (c(y) v c(x))) v c(z)=x v (c(y) v c(x)). given clause #122: (wt=11) 2108 [para_into,1837,1374,demod,37] x v c(y v (z v c(y)))=x. given clause #123: (wt=11) 2110 [para_into,1837,1365,demod,37] x v c(y v (c(y) v z))=x. given clause #124: (wt=11) 2112 [para_into,1837,36] x v c((y v c(z)) v z)=x. given clause #125: (wt=23) 966 [back_demod,803,demod,913,913,913,913,913] c(x) v (c(c(y) v (c(x) v c(z))) v (c(y) v c(z)))=c(u) v u. given clause #126: (wt=11) 2120 [para_into,1837,218] c((x v y) v c(y)) v z=z. given clause #127: (wt=11) 2122 [para_into,1837,217,demod,37] x v c(x)= (y v z) v c(z). given clause #128: (wt=11) 2123 [para_into,1837,216,demod,37] c(x) v x= (y v z) v c(z). given clause #129: (wt=23) 1076 [back_demod,664,demod,913,913,913,913,913] c(x) v (c(c(y) v (c(x) v c(z))) v (c(y) v c(z)))=u v c(u). given clause #130: (wt=11) 2126 [copy,2122,flip.1] (x v y) v c(y)=z v c(z). given clause #131: (wt=11) 2127 [copy,2123,flip.1] (x v y) v c(y)=c(z) v z. given clause #132: (wt=11) 2144 [para_into,1839,36] x v c((c(y) v z) v y)=x. given clause #133: (wt=20) 1121 [back_demod,607,demod,913,913,913,913,913] (c(x) v c(y)) v (c(z) v c(x))=c(z) v (c(x) v c(y)). given clause #134: (wt=11) 2154 [para_into,1839,218] c((x v y) v c(x)) v z=z. given clause #135: (wt=11) 2156 [para_into,1839,217,demod,37] x v c(x)= (y v z) v c(y). given clause #136: (wt=11) 2157 [para_into,1839,216,demod,37] c(x) v x= (y v z) v c(y). given clause #137: (wt=23) 1125 [back_demod,602,demod,913,913,913,913,913,913] c(x) v (((c(x) v c(y)) v c(z)) v c(y))= (c(x) v c(y)) v c(z). given clause #138: (wt=11) 2160 [copy,2156,flip.1] (x v y) v c(x)=z v c(z). given clause #139: (wt=11) 2161 [copy,2157,flip.1] (x v y) v c(x)=c(z) v z. given clause #140: (wt=11) 2174 [para_into,2104,218] c(c(x) v (y v x)) v z=z. given clause #141: (wt=20) 1139 [back_demod,585,demod,913,913,913,913,913] (c(x) v c(y)) v (c(z) v c(y))=c(z) v (c(x) v c(y)). given clause #142: (wt=11) 2176 [para_into,2104,217,demod,37] x v c(x)=c(y) v (z v y). given clause #143: (wt=11) 2177 [para_into,2104,216,demod,37] c(x) v x=c(y) v (z v y). given clause #144: (wt=11) 2180 [copy,2176,flip.1] c(x) v (y v x)=z v c(z). given clause #145: (wt=23) 1143 [back_demod,580,demod,913,913,913,913,913,913] c(x) v ((c(y) v (c(x) v c(z))) v c(z))=c(y) v (c(x) v c(z)). given clause #146: (wt=11) 2181 [copy,2177,flip.1] c(x) v (y v x)=c(z) v z. given clause #147: (wt=11) 2192 [para_into,2106,218] c(c(x) v (x v y)) v z=z. given clause #148: (wt=11) 2194 [para_into,2106,217,demod,37] x v c(x)=c(y) v (y v z). given clause #149: (wt=20) 1185 [back_demod,532,demod,913,913,913,913,913] c(x) v (c(y) v (c(z) v c(x)))=c(y) v (c(z) v c(x)). given clause #150: (wt=11) 2195 [para_into,2106,216,demod,37] c(x) v x=c(y) v (y v z). given clause #151: (wt=11) 2198 [copy,2194,flip.1] c(x) v (x v y)=z v c(z). given clause #152: (wt=11) 2199 [copy,2195,flip.1] c(x) v (x v y)=c(z) v z. given clause #153: (wt=20) 1246 [back_demod,416,demod,913,913,37,913,913,913] c(x) v (c(y) v c(c(z) v (x v c(u))))=c(y) v c(x). given clause #154: (wt=11) 2226 [para_into,2108,218] c(x v (y v c(x))) v z=z. given clause #155: (wt=11) 2228 [para_into,2108,217,demod,37] x v c(x)=y v (z v c(y)). given clause #156: (wt=11) 2229 [para_into,2108,216,demod,37] c(x) v x=y v (z v c(y)). given clause #157: (wt=17) 1248 [back_demod,414,demod,913,913,37,913,913,37] x v (c(y) v (x v c(z)))=c(y) v (x v c(z)). given clause #158: (wt=11) 2232 [copy,2228,flip.1] x v (y v c(x))=z v c(z). given clause #159: (wt=11) 2233 [copy,2229,flip.1] x v (y v c(x))=c(z) v z. given clause #160: (wt=11) 2244 [para_into,2110,218] c(x v (c(x) v y)) v z=z. given clause #161: (wt=17) 1250 [back_demod,412,demod,913,913,37,913,913,37] (c(x) v (y v c(z))) v y=c(x) v (y v c(z)). given clause #162: (wt=11) 2246 [para_into,2110,217,demod,37] x v c(x)=y v (c(y) v z). given clause #163: (wt=11) 2247 [para_into,2110,216,demod,37] c(x) v x=y v (c(y) v z). given clause #164: (wt=11) 2250 [copy,2246,flip.1] x v (c(x) v y)=z v c(z). given clause #165: (wt=16) 1260 [back_demod,400,demod,913,913,913] c(x v y) v (c(z) v c(x))=c(z) v c(x). given clause #166: (wt=11) 2251 [copy,2247,flip.1] x v (c(x) v y)=c(z) v z. given clause #167: (wt=11) 2268 [para_into,2112,218] c((x v c(y)) v y) v z=z. given clause #168: (wt=11) 2270 [para_into,2112,217,demod,37] x v c(x)= (y v c(z)) v z. given clause #169: (wt=16) 1264 [back_demod,394,demod,913,913,913] c(x v y) v (c(z) v c(y))=c(z) v c(y). given clause #170: (wt=11) 2271 [para_into,2112,216,demod,37] c(x) v x= (y v c(z)) v z. given clause #171: (wt=11) 2274 [copy,2270,flip.1] (x v c(y)) v y=z v c(z). given clause #172: (wt=11) 2275 [copy,2271,flip.1] (x v c(y)) v y=c(z) v z. given clause #173: (wt=16) 1268 [back_demod,386,demod,913,913,913] c(x) v (c(y) v c(x v z))=c(y) v c(x). given clause #174: (wt=11) 2364 [para_into,2144,218] c((c(x) v y) v x) v z=z. given clause #175: (wt=11) 2366 [para_into,2144,217,demod,37] x v c(x)= (c(y) v z) v y. given clause #176: (wt=11) 2367 [para_into,2144,216,demod,37] c(x) v x= (c(y) v z) v y. given clause #177: (wt=16) 1288 [back_demod,352,demod,913,913,913] c(x) v (c(y) v c(z v x))=c(y) v c(x). given clause #178: (wt=11) 2374 [copy,2366,flip.1] (c(x) v y) v x=z v c(z). given clause #179: (wt=11) 2375 [copy,2367,flip.1] (c(x) v y) v x=c(z) v z. given clause #180: (wt=12) 2611 [para_into,1260,1464,demod,1465] c((x v y) v z) v c(y)=c(y). given clause #181: (wt=23) 1306 [back_demod,285,demod,913,913,37,913,913,913,913] c(x) v (c(y) v x)=c(y) v (c(c(z) v c(u)) v (c(u) v c(z))). given clause #182: (wt=11) 2653 [para_into,2611,36,demod,37] c((x v c(y)) v z) v y=y. given clause #183: (wt=11) 2706 [para_into,2653,382] c((c(x) v y) v z) v x=x. given clause #184: (wt=11) 2708 [para_into,2653,350] c(x v (y v c(z))) v z=z. given clause #185: (wt=17) 1311 [back_demod,272,demod,913,913,913,913] c(x) v (c(y) v c(z))=c(y) v (c(z) v c(x)). given clause #186: (wt=11) 2710 [para_into,2653,218] x v c((y v c(x)) v z)=x. given clause #187: (wt=11) 2734 [para_into,2706,350] c(x v (c(y) v z)) v y=y. given clause #188: (wt=11) 2736 [para_into,2706,218] x v c((c(x) v y) v z)=x. given clause #189: (wt=17) 1313 [back_demod,252,demod,913,913,913] x v c(x)=c(y) v (c(c(y) v c(z)) v c(z)). given clause #190: (wt=11) 2764 [para_into,2708,218] x v c(y v (z v c(x)))=x. given clause #191: (wt=11) 2892 [para_into,2734,218] x v c(y v (c(x) v z))=x. given clause #192: (wt=12) 2613 [para_into,1260,1460,demod,1461] c((x v y) v z) v c(x)=c(x). given clause #193: (wt=17) 1314 [back_demod,249,demod,913,913,913] c(x) v (c(c(x) v c(y)) v c(y))=z v c(z). given clause #194: (wt=12) 2625 [para_into,1264,1464,demod,1465] c(x v (y v z)) v c(z)=c(z). given clause #195: (wt=12) 2627 [para_into,1264,1460,demod,1461] c(x v (y v z)) v c(y)=c(y). given clause #196: (wt=12) 2655 [para_into,2611,218] c(x) v c((y v x) v z)=c(x). given clause #197: (wt=17) 1319 [back_demod,230,demod,913,913,913] c(x) v x=c(y) v (c(c(y) v c(z)) v c(z)). given clause #198: (wt=12) 2916 [para_into,2736,36] c(x) v c((x v y) v z)=c(x). given clause #199: (wt=12) 2959 [para_into,2764,36] c(x) v c(y v (z v x))=c(x). given clause #200: (wt=12) 2975 [para_into,2892,36] c(x) v c(y v (x v z))=c(x). given clause #201: (wt=17) 1320 [back_demod,229,demod,913,913,913] c(x) v (c(c(x) v c(y)) v c(y))=c(z) v z. given clause #202: (wt=13) 1756 [para_into,219,182,demod,1753,37] c(x v y) v z=c(y v x) v z. given clause #203: (wt=9) 3093 [para_into,1756,2144,demod,2145] c(x v y)=c(y v x). given clause #204: (wt=13) 2118 [para_into,1837,442] c((x v y) v c(y))=c(z v c(z)). given clause #205: (wt=17) 1359 [back_demod,58,demod,913,913,913,913] c(x) v (c(y) v c(z))=c(y) v (c(x) v c(z)). given clause #206: (wt=13) 2119 [para_into,1837,428] c((x v y) v c(y))=c(c(z) v z). given clause #207: (wt=13) 2124 [copy,2118,flip.1] c(x v c(x))=c((y v z) v c(z)). given clause #208: (wt=13) 2125 [copy,2119,flip.1] c(c(x) v x)=c((y v z) v c(z)). given clause #209: (wt=20) 1835 [back_demod,1688,demod,1811,1811,37,1811,37] x v c(c(c(y) v c(z)) v (c(y) v (c(u) v c(z))))=x. given clause #210: (wt=13) 2152 [para_into,1839,442] c((x v y) v c(x))=c(z v c(z)). given clause #211: (wt=13) 2153 [para_into,1839,428] c((x v y) v c(x))=c(c(z) v z). given clause #212: (wt=13) 2158 [copy,2152,flip.1] c(x v c(x))=c((y v z) v c(y)). given clause #213: (wt=25) 1844 [back_demod,1680,demod,1811,37,1811,1811,37] c(c(x) v x)=c(c(c(y) v (c(z) v c(u))) v (c(z) v (c(y) v c(u)))). given clause #214: (wt=13) 2159 [copy,2153,flip.1] c(c(x) v x)=c((y v z) v c(y)). given clause #215: (wt=13) 2172 [para_into,2104,442] c(c(x) v (y v x))=c(z v c(z)). given clause #216: (wt=13) 2173 [para_into,2104,428] c(c(x) v (y v x))=c(c(z) v z). given clause #217: (wt=25) 1846 [back_demod,1678,demod,1811,1811,37,1811,37] c(c(c(x) v (c(y) v c(z))) v (c(y) v (c(x) v c(z))))=c(c(u) v u). given clause #218: (wt=13) 2178 [copy,2172,flip.1] c(x v c(x))=c(c(y) v (z v y)). given clause #219: (wt=13) 2179 [copy,2173,flip.1] c(c(x) v x)=c(c(y) v (z v y)). given clause #220: (wt=13) 2190 [para_into,2106,442] c(c(x) v (x v y))=c(z v c(z)). given clause #221: (wt=25) 1847 [back_demod,1677,demod,1811,37,1811,1811,37] c(x v c(x))=c((c(y) v (c(z) v c(u))) v c(c(z) v (c(y) v c(u)))). given clause #222: (wt=13) 2191 [para_into,2106,428] c(c(x) v (x v y))=c(c(z) v z). given clause #223: (wt=13) 2196 [copy,2190,flip.1] c(x v c(x))=c(c(y) v (y v z)). given clause #224: (wt=13) 2197 [copy,2191,flip.1] c(c(x) v x)=c(c(y) v (y v z)). given clause #225: (wt=25) 1848 [back_demod,1676,demod,1811,37,1811,1811,37] c(c(x) v x)=c((c(y) v (c(z) v c(u))) v c(c(z) v (c(y) v c(u)))). given clause #226: (wt=13) 2224 [para_into,2108,442] c(x v (y v c(x)))=c(z v c(z)). given clause #227: (wt=13) 2225 [para_into,2108,428] c(x v (y v c(x)))=c(c(z) v z). given clause #228: (wt=13) 2230 [copy,2224,flip.1] c(x v c(x))=c(y v (z v c(y))). given clause #229: (wt=25) 1849 [back_demod,1673,demod,1811,1811,37,1811,37] c((c(x) v (c(y) v c(z))) v c(c(y) v (c(x) v c(z))))=c(u v c(u)). given clause #230: (wt=13) 2231 [copy,2225,flip.1] c(c(x) v x)=c(y v (z v c(y))). given clause #231: (wt=13) 2242 [para_into,2110,442] c(x v (c(x) v y))=c(z v c(z)). given clause #232: (wt=13) 2243 [para_into,2110,428] c(x v (c(x) v y))=c(c(z) v z). given clause #233: (wt=25) 1850 [back_demod,1672,demod,1811,1811,37,1811,37] c((c(x) v (c(y) v c(z))) v c(c(y) v (c(x) v c(z))))=c(c(u) v u). given clause #234: (wt=13) 2248 [copy,2242,flip.1] c(x v c(x))=c(y v (c(y) v z)). given clause #235: (wt=13) 2249 [copy,2243,flip.1] c(c(x) v x)=c(y v (c(y) v z)). given clause #236: (wt=13) 2266 [para_into,2112,442] c((x v c(y)) v y)=c(z v c(z)). given clause #237: (wt=23) 1851 [back_demod,1666,demod,1811,1811,37,1811,1811,37] x v c(c(y) v (c(z) v c(u)))=x v c(c(z) v (c(u) v c(y))). given clause #238: (wt=13) 2267 [para_into,2112,428] c((x v c(y)) v y)=c(c(z) v z). given clause #239: (wt=13) 2272 [copy,2266,flip.1] c(x v c(x))=c((y v c(z)) v z). given clause #240: (wt=13) 2273 [copy,2267,flip.1] c(c(x) v x)=c((y v c(z)) v z). given clause #241: (wt=25) 1854 [back_demod,1638,demod,1811,37,1811,1811,37] c(x v c(x))=c(c(c(y) v (c(z) v c(u))) v (c(z) v (c(y) v c(u)))). given clause #242: (wt=13) 2317 [para_into,2122,2122] (x v y) v c(y)= (z v u) v c(u). given clause #243: (wt=13) 2318 [para_into,2122,2112] (x v c(y)) v y= (z v u) v c(u). given clause #244: (wt=13) 2319 [para_into,2122,2110] x v (c(x) v y)= (z v u) v c(u). given clause #245: (wt=25) 1856 [back_demod,1636,demod,1811,1811,37,1811,37] c(c(c(x) v (c(y) v c(z))) v (c(y) v (c(x) v c(z))))=c(u v c(u)). given clause #246: (wt=13) 2320 [para_into,2122,2108] x v (y v c(x))= (z v u) v c(u). given clause #247: (wt=13) 2321 [para_into,2122,2106] c(x) v (x v y)= (z v u) v c(u). given clause #248: (wt=13) 2322 [para_into,2122,2104] c(x) v (y v x)= (z v u) v c(u). given clause #249: (wt=19) 1857 [back_demod,1631,demod,1811,1811,37] c(x v c(x))=c(c(y) v (c(c(y) v c(z)) v c(z))). given clause #250: (wt=13) 2323 [para_into,2122,1839] (x v y) v c(x)= (z v u) v c(u). given clause #251: (wt=13) 2324 [copy,2318,flip.1] (x v y) v c(y)= (z v c(u)) v u. given clause #252: (wt=13) 2325 [copy,2319,flip.1] (x v y) v c(y)=z v (c(z) v u). given clause #253: (wt=19) 1858 [back_demod,1630,demod,1811,1811,37] c(c(x) v (c(c(x) v c(y)) v c(y)))=c(z v c(z)). given clause #254: (wt=13) 2326 [copy,2320,flip.1] (x v y) v c(y)=z v (u v c(z)). given clause #255: (wt=13) 2327 [copy,2321,flip.1] (x v y) v c(y)=c(z) v (z v u). given clause #256: (wt=13) 2328 [copy,2322,flip.1] (x v y) v c(y)=c(z) v (u v z). given clause #257: (wt=24) 1872 [back_demod,1611,demod,1811,1811,1811] (x v c(c(y) v c(z))) v c(c(z) v c(y))=x v c(c(y) v c(z)). given clause #258: (wt=13) 2329 [copy,2323,flip.1] (x v y) v c(y)= (z v u) v c(z). given clause #259: (wt=13) 2356 [para_into,2144,2123,demod,37] (x v y) v c(y)= (c(z) v u) v z. given clause #260: (wt=13) 2362 [para_into,2144,442] c((c(x) v y) v x)=c(z v c(z)). given clause #261: (wt=24) 1874 [back_demod,1609,demod,1811,1811,1811] (c(c(x) v c(y)) v z) v c(c(y) v c(x))=c(c(x) v c(y)) v z. given clause #262: (wt=13) 2363 [para_into,2144,428] c((c(x) v y) v x)=c(c(z) v z). given clause #263: (wt=13) 2370 [copy,2356,flip.1] (c(x) v y) v x= (z v u) v c(u). given clause #264: (wt=13) 2372 [copy,2362,flip.1] c(x v c(x))=c((c(y) v z) v y). given clause #265: (wt=23) 1877 [back_demod,1589,demod,1811,1811,37,1811,1811,37] c(c(x) v (c(y) v c(z))) v u=u v c(c(y) v (c(x) v c(z))). given clause #266: (wt=13) 2373 [copy,2363,flip.1] c(c(x) v x)=c((c(y) v z) v y). given clause #267: (wt=13) 2411 [para_into,2156,2156] (x v y) v c(x)= (z v u) v c(z). given clause #268: (wt=13) 2412 [para_into,2156,2144] (c(x) v y) v x= (z v u) v c(z). given clause #269: (wt=23) 1878 [back_demod,1585,demod,1811,1811,37,1811,1811,37] c(c(x) v (c(y) v c(z))) v u=c(c(y) v (c(z) v c(x))) v u. given clause #270: (wt=13) 2413 [para_into,2156,2112] (x v c(y)) v y= (z v u) v c(z). given clause #271: (wt=13) 2414 [para_into,2156,2110] x v (c(x) v y)= (z v u) v c(z). given clause #272: (wt=13) 2415 [para_into,2156,2108] x v (y v c(x))= (z v u) v c(z). given clause #273: (wt=19) 1881 [back_demod,1551,demod,1811,1811,37] c(c(x) v x)=c(c(y) v (c(c(y) v c(z)) v c(z))). given clause #274: (wt=13) 2416 [para_into,2156,2106] c(x) v (x v y)= (z v u) v c(z). given clause #275: (wt=13) 2417 [para_into,2156,2104] c(x) v (y v x)= (z v u) v c(z). given clause #276: (wt=13) 2418 [copy,2412,flip.1] (x v y) v c(x)= (c(z) v u) v z. given clause #277: (wt=19) 1882 [back_demod,1550,demod,1811,1811,37] c(c(x) v (c(c(x) v c(y)) v c(y)))=c(c(z) v z). given clause #278: (wt=13) 2419 [copy,2413,flip.1] (x v y) v c(x)= (z v c(u)) v u. given clause #279: (wt=13) 2420 [copy,2414,flip.1] (x v y) v c(x)=z v (c(z) v u). given clause #280: (wt=13) 2421 [copy,2415,flip.1] (x v y) v c(x)=z v (u v c(z)). given clause #281: (wt=16) 1911 [back_demod,1502,demod,1811,1811,37,1811,37] c((c(x) v (c(y) v c(z))) v c(u)) v y=y. given clause #282: (wt=13) 2422 [copy,2416,flip.1] (x v y) v c(x)=c(z) v (z v u). given clause #283: (wt=13) 2423 [copy,2417,flip.1] (x v y) v c(x)=c(z) v (u v z). given clause #284: (wt=13) 2465 [para_into,2176,2176] c(x) v (y v x)=c(z) v (u v z). given clause #285: (wt=16) 1925 [back_demod,1486,demod,1811,1811,37,1811,37] x v c((c(y) v (c(x) v c(z))) v c(u))=x. given clause #286: (wt=13) 2466 [para_into,2176,2144] (c(x) v y) v x=c(z) v (u v z). given clause #287: (wt=13) 2467 [para_into,2176,2112] (x v c(y)) v y=c(z) v (u v z). given clause #288: (wt=13) 2468 [para_into,2176,2110] x v (c(x) v y)=c(z) v (u v z). given clause #289: (wt=16) 1937 [back_demod,1472,demod,1811,1811,37,1811,37] c(c(x) v (c(y) v (c(z) v c(u)))) v z=z. given clause #290: (wt=13) 2469 [para_into,2176,2108] x v (y v c(x))=c(z) v (u v z). given clause #291: (wt=13) 2470 [para_into,2176,2106] c(x) v (x v y)=c(z) v (u v z). given clause #292: (wt=13) 2471 [copy,2466,flip.1] c(x) v (y v x)= (c(z) v u) v z. given clause #293: (wt=16) 1947 [back_demod,1456,demod,1811,1811,37,1811,37] x v c(c(y) v (c(z) v (c(x) v c(u))))=x. given clause #294: (wt=13) 2472 [copy,2467,flip.1] c(x) v (y v x)= (z v c(u)) v u. given clause #295: (wt=13) 2473 [copy,2468,flip.1] c(x) v (y v x)=z v (c(z) v u). given clause #296: (wt=13) 2474 [copy,2469,flip.1] c(x) v (y v x)=z v (u v c(z)). given clause #297: (wt=25) 1955 [back_demod,1449,demod,1811,1811,37,1811,1811,1811,37,1811,37,37] c(c(x) v (c(y) v c(z)))=c((c(y) v c(z)) v (c(y) v (c(x) v c(z)))). given clause #298: (wt=13) 2475 [copy,2470,flip.1] c(x) v (y v x)=c(z) v (z v u). given clause #299: (wt=13) 2498 [para_into,2194,2194] c(x) v (x v y)=c(z) v (z v u). given clause #300: (wt=13) 2499 [para_into,2194,2144] (c(x) v y) v x=c(z) v (z v u). given clause #301: (wt=23) 1958 [back_demod,1445,demod,1811,1811,37,1811,1811] c(c(x) v (c(y) v c(z))) v c(c(x) v c(z))=c(c(x) v c(z)). given clause #302: (wt=13) 2500 [para_into,2194,2112] (x v c(y)) v y=c(z) v (z v u). given clause #303: (wt=13) 2501 [para_into,2194,2110] x v (c(x) v y)=c(z) v (z v u). given clause #304: (wt=13) 2502 [para_into,2194,2108] x v (y v c(x))=c(z) v (z v u). given clause #305: (wt=25) 1960 [back_demod,1443,demod,1811,1811,37,1811,1811,37,37,1811,1811,37] c((c(x) v (c(y) v c(z))) v (c(x) v c(z)))=c(c(y) v (c(x) v c(z))). given clause #306: (wt=13) 2503 [copy,2499,flip.1] c(x) v (x v y)= (c(z) v u) v z. given clause #307: (wt=13) 2504 [copy,2500,flip.1] c(x) v (x v y)= (z v c(u)) v u. given clause #308: (wt=13) 2505 [copy,2501,flip.1] c(x) v (x v y)=z v (c(z) v u). given clause #309: (wt=23) 1962 [back_demod,1441,demod,1811,1811,1811,37,1811] c(c(x) v c(y)) v c(c(x) v (c(z) v c(y)))=c(c(x) v c(y)). given clause #310: (wt=13) 2506 [copy,2502,flip.1] c(x) v (x v y)=z v (u v c(z)). given clause #311: (wt=13) 2562 [para_into,2228,2228] x v (y v c(x))=z v (u v c(z)). given clause #312: (wt=13) 2563 [para_into,2228,2144] (c(x) v y) v x=z v (u v c(z)). given clause #313: (wt=25) 1966 [back_demod,1422,demod,1811,1811,37,1811,37,1811,1811,37,1811,37] c(c(x) v (c(y) v (c(z) v c(u))))=c(c(y) v (c(z) v (c(x) v c(u)))). given clause #314: (wt=13) 2564 [para_into,2228,2112] (x v c(y)) v y=z v (u v c(z)). given clause #315: (wt=13) 2565 [para_into,2228,2110] x v (c(x) v y)=z v (u v c(z)). given clause #316: (wt=13) 2566 [copy,2563,flip.1] x v (y v c(x))= (c(z) v u) v z. given clause #317: (wt=19) 1967 [back_demod,1421,demod,1811,1811,37,1811,1811,37] c(c(x) v (c(y) v c(z)))=c(c(y) v (c(z) v c(x))). given clause #318: (wt=13) 2567 [copy,2564,flip.1] x v (y v c(x))= (z v c(u)) v u. given clause #319: (wt=13) 2568 [copy,2565,flip.1] x v (y v c(x))=z v (c(z) v u). given clause #320: (wt=13) 2598 [para_into,2246,2246] x v (c(x) v y)=z v (c(z) v u). given clause #321: (wt=22) 1969 [back_demod,1413,demod,1811,1811,1811,37,37,1811,1811,37] c((c(x) v c(y)) v (c(z) v c(x)))=c(c(z) v (c(x) v c(y))). given clause #322: (wt=13) 2599 [para_into,2246,2144] (c(x) v y) v x=z v (c(z) v u). given clause #323: (wt=13) 2600 [para_into,2246,2112] (x v c(y)) v y=z v (c(z) v u). given clause #324: (wt=13) 2601 [copy,2599,flip.1] x v (c(x) v y)= (c(z) v u) v z. given clause #325: (wt=23) 1983 [back_demod,1351,demod,1811,1811,37,1811,37] x v c(c(c(y) v (c(z) v c(u))) v (c(z) v (c(y) v c(u))))=x. given clause #326: (wt=13) 2602 [copy,2600,flip.1] x v (c(x) v y)= (z v c(u)) v u. given clause #327: (wt=13) 2618 [para_into,2270,2270] (x v c(y)) v y= (z v c(u)) v u. given clause #328: (wt=13) 2619 [para_into,2270,2144] (c(x) v y) v x= (z v c(u)) v u. given clause #329: (wt=23) 1985 [back_demod,1349,demod,1811,1811,37,1811,37] x v c((c(y) v (c(z) v c(u))) v c(c(z) v (c(y) v c(u))))=x. given clause #330: (wt=13) 2620 [copy,2619,flip.1] (x v c(y)) v y= (c(z) v u) v z. given clause #331: (wt=13) 2640 [para_into,2366,2366] (c(x) v y) v x= (c(z) v u) v z. given clause #332: (wt=13) 2647 [para_into,2611,1464,demod,37,37] c(c(x) v y) v (z v x)=z v x. given clause #333: (wt=23) 1993 [back_demod,1294,demod,1811,1811,37,1811,37] c(c(c(x) v (c(y) v c(z))) v (c(y) v (c(x) v c(z)))) v u=u. given clause #334: (wt=13) 2649 [para_into,2611,1460,demod,37,37] c(c(x) v y) v (x v z)=x v z. given clause #335: (wt=13) 2657 [para_from,2611,2144] x v c(c(y) v ((z v y) v u))=x. given clause #336: (wt=13) 2659 [para_from,2611,2110] x v c(((y v z) v u) v c(z))=x. given clause #337: (wt=23) 1997 [back_demod,1290,demod,1811,1811,37,1811,37] c((c(x) v (c(y) v c(z))) v c(c(y) v (c(x) v c(z)))) v u=u. given clause #338: (wt=13) 2661 [para_from,2611,2375] c(x) v ((y v x) v z)=c(u) v u. given clause #339: (wt=13) 2662 [para_from,2611,2374] c(x) v ((y v x) v z)=u v c(u). given clause #340: (wt=13) 2663 [para_from,2611,2364] c(c(x) v ((y v x) v z)) v u=u. given clause #341: (wt=19) 1999 [back_demod,1286,demod,1811] c(c(x) v c(c(y) v (c(c(z) v c(y)) v c(z))))=x. given clause #342: (wt=13) 2665 [para_from,2611,2251] ((x v y) v z) v c(y)=c(u) v u. given clause #343: (wt=13) 2666 [para_from,2611,2250] ((x v y) v z) v c(y)=u v c(u). given clause #344: (wt=13) 2667 [para_from,2611,2244] c(((x v y) v z) v c(y)) v u=u. given clause #345: (wt=17) 2009 [back_demod,1272,demod,1811,1811,37] c(c(x) v (c(c(x) v c(y)) v c(y))) v z=z. given clause #346: (wt=13) 2669 [para_from,2611,1365,demod,37] ((x v y) v z) v y= (x v y) v z. given clause #347: (wt=11) 5126 [para_into,2669,218,demod,3002] (x v y) v z= (y v x) v z. given clause #348: (wt=11) 5169 [para_into,5126,218] x v (y v z)= (z v y) v x. given clause #349: (wt=17) 2011 [back_demod,1270,demod,1811,1811,37] x v c(c(y) v (c(c(y) v c(z)) v c(z)))=x. given clause #350: (wt=11) 5170 [para_into,5126,187,flip.1] (x v y) v (y v x)=y v x. given clause #351: (wt=11) 5174 [copy,5169,flip.1] (x v y) v z=z v (y v x). given clause #352: (wt=11) 5245 [para_into,5174,218] x v (y v z)=x v (z v y). given clause #353: (wt=21) 2013 [back_demod,1266,demod,1811] c(x) v (c(y v c(c(x) v c(z))) v c(z))=c(x) v c(z). given clause #354: (wt=13) 2671 [para_from,2611,914,demod,37] x v ((y v x) v z)= (y v x) v z. given clause #355: (wt=13) 2673 [copy,2661,flip.1] c(x) v x=c(y) v ((z v y) v u). given clause #356: (wt=13) 2674 [copy,2662,flip.1] x v c(x)=c(y) v ((z v y) v u). given clause #357: (wt=21) 2015 [back_demod,1262,demod,1811] c(x) v (c(c(c(x) v c(y)) v z) v c(y))=c(x) v c(y). given clause #358: (wt=13) 2675 [copy,2665,flip.1] c(x) v x= ((y v z) v u) v c(z). given clause #359: (wt=13) 2676 [copy,2666,flip.1] x v c(x)= ((y v z) v u) v c(z). given clause #360: (wt=13) 2712 [para_from,2653,2144] x v c(y v ((z v c(y)) v u))=x. given clause #361: (wt=23) 2024 [back_demod,1222,demod,1811,1811,37] c(c(x) v (c(y) v c(z))) v (c(y) v (c(x) v c(z)))=c(u) v u. given clause #362: (wt=13) 2714 [para_from,2653,2110] x v c(((y v c(z)) v u) v z)=x. given clause #363: (wt=13) 2716 [para_from,2653,2375] x v ((y v c(x)) v z)=c(u) v u. given clause #364: (wt=13) 2717 [para_from,2653,2374] x v ((y v c(x)) v z)=u v c(u). given clause #365: (wt=23) 2028 [back_demod,1218,demod,1811,1811,37] c(c(x) v (c(y) v c(z))) v (c(y) v (c(x) v c(z)))=u v c(u). given clause #366: (wt=13) 2718 [para_from,2653,2364] c(x v ((y v c(x)) v z)) v u=u. given clause #367: (wt=13) 2720 [para_from,2653,2251] ((x v c(y)) v z) v y=c(u) v u. given clause #368: (wt=13) 2721 [para_from,2653,2250] ((x v c(y)) v z) v y=u v c(u). given clause #369: (wt=23) 2031 [back_demod,1210,demod,1811,1811,37,1811,37] x v c(c(c(y) v (c(z) v c(u))) v (c(u) v (c(y) v c(z))))=x. given clause #370: (wt=13) 2722 [para_from,2653,2244] c(((x v c(y)) v z) v y) v u=u. given clause #371: (wt=13) 2724 [copy,2716,flip.1] c(x) v x=y v ((z v c(y)) v u). given clause #372: (wt=13) 2725 [copy,2717,flip.1] x v c(x)=y v ((z v c(y)) v u). given clause #373: (wt=23) 2037 [back_demod,1196,demod,1811,1811,37,1811,37] x v c(c(c(y) v (c(z) v c(u))) v (c(z) v (c(u) v c(y))))=x. given clause #374: (wt=13) 2726 [copy,2720,flip.1] c(x) v x= ((y v c(z)) v u) v z. given clause #375: (wt=13) 2727 [copy,2721,flip.1] x v c(x)= ((y v c(z)) v u) v z. given clause #376: (wt=13) 2738 [para_from,2706,2144] x v c(y v ((c(y) v z) v u))=x. given clause #377: (wt=23) 2042 [back_demod,1192,demod,1811,1811,37] (c(x) v (c(y) v c(z))) v c(c(y) v (c(x) v c(z)))=c(u) v u. given clause #378: (wt=13) 2740 [para_from,2706,2110] x v c(((c(y) v z) v u) v y)=x. given clause #379: (wt=13) 2742 [para_from,2706,2375] x v ((c(x) v y) v z)=c(u) v u. given clause #380: (wt=13) 2743 [para_from,2706,2374] x v ((c(x) v y) v z)=u v c(u). given clause #381: (wt=23) 2046 [back_demod,1188,demod,1811,1811,37] (c(x) v (c(y) v c(z))) v c(c(y) v (c(x) v c(z)))=u v c(u). given clause #382: (wt=13) 2744 [para_from,2706,2364] c(x v ((c(x) v y) v z)) v u=u. given clause #383: (wt=13) 2746 [para_from,2706,2251] ((c(x) v y) v z) v x=c(u) v u. given clause #384: (wt=13) 2747 [para_from,2706,2250] ((c(x) v y) v z) v x=u v c(u). given clause #385: (wt=23) 2048 [back_demod,1183,demod,1811,1811,37,1811,37] x v c((c(y) v (c(z) v c(u))) v c(c(u) v (c(y) v c(z))))=x. given clause #386: (wt=13) 2748 [para_from,2706,2244] c(((c(x) v y) v z) v x) v u=u. given clause #387: (wt=13) 2754 [copy,2742,flip.1] c(x) v x=y v ((c(y) v z) v u). given clause #388: (wt=13) 2755 [copy,2743,flip.1] x v c(x)=y v ((c(y) v z) v u). given clause #389: (wt=23) 2052 [back_demod,1169,demod,1811,1811,37,1811,37] x v c((c(y) v (c(z) v c(u))) v c(c(z) v (c(u) v c(y))))=x. given clause #390: (wt=13) 2756 [copy,2746,flip.1] c(x) v x= ((c(y) v z) v u) v y. given clause #391: (wt=13) 2757 [copy,2747,flip.1] x v c(x)= ((c(y) v z) v u) v y. given clause #392: (wt=13) 2758 [para_into,2708,1464] c(x v c(y)) v (z v y)=z v y. given clause #393: (wt=25) 2058 [back_demod,1116,demod,1811,1811,37,1811,37,1811,37] c(c(c(x) v (c(y) v c(z))) v (c(z) v (c(x) v c(y))))=c(u v c(u)). given clause #394: (wt=13) 2760 [para_into,2708,1460] c(x v c(y)) v (y v z)=y v z. given clause #395: (wt=13) 2766 [para_from,2708,2144] x v c(y v (z v (u v c(y))))=x. given clause #396: (wt=13) 2768 [para_from,2708,2110] x v c((y v (z v c(u))) v u)=x. given clause #397: (wt=25) 2060 [back_demod,1106,demod,1811,1811,37,1811,37,1811,37] c(c(x) v (c(c(y) v (c(x) v c(z))) v (c(y) v c(z))))=c(u v c(u)). given clause #398: (wt=13) 2772 [para_from,2708,2375] x v (y v (z v c(x)))=c(u) v u. given clause #399: (wt=13) 2773 [para_from,2708,2374] x v (y v (z v c(x)))=u v c(u). given clause #400: (wt=13) 2774 [para_from,2708,2364] c(x v (y v (z v c(x)))) v u=u. given clause #401: (wt=25) 2061 [back_demod,1103,demod,1811,1811,37,1811,37,1811,37] c(c(c(x) v (c(y) v c(z))) v (c(y) v (c(z) v c(x))))=c(u v c(u)). given clause #402: (wt=13) 2776 [para_from,2708,2251] (x v (y v c(z))) v z=c(u) v u. given clause #403: (wt=13) 2777 [para_from,2708,2250] (x v (y v c(z))) v z=u v c(u). given clause #404: (wt=13) 2778 [para_from,2708,2244] c((x v (y v c(z))) v z) v u=u. given clause #405: (wt=23) 2068 [back_demod,1081,demod,1811,1811,37,1811,37] x v c(c(y) v (c(c(z) v (c(y) v c(u))) v (c(z) v c(u))))=x. given clause #406: (wt=13) 2784 [copy,2772,flip.1] c(x) v x=y v (z v (u v c(y))). given clause #407: (wt=13) 2785 [copy,2773,flip.1] x v c(x)=y v (z v (u v c(y))). given clause #408: (wt=13) 2786 [copy,2776,flip.1] c(x) v x= (y v (z v c(u))) v u. given clause #409: (wt=25) 2070 [back_demod,1072,demod,1811,1811,37,1811,37,1811,37] c((c(x) v (c(y) v c(z))) v c(c(z) v (c(x) v c(y))))=c(u v c(u)). given clause #410: (wt=13) 2787 [copy,2777,flip.1] x v c(x)= (y v (z v c(u))) v u. given clause #411: (wt=13) 2874 [para_into,2710,1464] (x v y) v c(c(y) v z)=x v y. given clause #412: (wt=13) 2876 [para_into,2710,1460] (x v y) v c(c(x) v z)=x v y. given clause #413: (wt=25) 2072 [back_demod,1063,demod,1811,1811,37,1811,37,1811,37] c((c(x) v (c(y) v c(z))) v c(c(y) v (c(z) v c(x))))=c(u v c(u)). given clause #414: (wt=13) 2894 [para_from,2734,2144] x v c(y v (z v (c(y) v u)))=x. given clause #415: (wt=13) 2896 [para_from,2734,2110] x v c((y v (c(z) v u)) v z)=x. given clause #416: (wt=13) 2900 [para_from,2734,2375] x v (y v (c(x) v z))=c(u) v u. given clause #417: (wt=25) 2078 [back_demod,1004,demod,1811,1811,37,1811,37,1811,37] c(c(c(x) v (c(y) v c(z))) v (c(z) v (c(x) v c(y))))=c(c(u) v u). given clause #418: (wt=13) 2901 [para_from,2734,2374] x v (y v (c(x) v z))=u v c(u). given clause #419: (wt=13) 2902 [para_from,2734,2364] c(x v (y v (c(x) v z))) v u=u. given clause #420: (wt=13) 2904 [para_from,2734,2251] (x v (c(y) v z)) v y=c(u) v u. given clause #421: (wt=25) 2080 [back_demod,993,demod,1811,1811,37,1811,37,1811,37] c(c(x) v (c(c(y) v (c(x) v c(z))) v (c(y) v c(z))))=c(c(u) v u). given clause #422: (wt=13) 2905 [para_from,2734,2250] (x v (c(y) v z)) v y=u v c(u). given clause #423: (wt=13) 2906 [para_from,2734,2244] c((x v (c(y) v z)) v y) v u=u. given clause #424: (wt=13) 2912 [copy,2900,flip.1] c(x) v x=y v (z v (c(y) v u)). given clause #425: (wt=25) 2081 [back_demod,990,demod,1811,1811,37,1811,37,1811,37] c(c(c(x) v (c(y) v c(z))) v (c(y) v (c(z) v c(x))))=c(c(u) v u). given clause #426: (wt=13) 2913 [copy,2901,flip.1] x v c(x)=y v (z v (c(y) v u)). given clause #427: (wt=13) 2914 [copy,2904,flip.1] c(x) v x= (y v (c(z) v u)) v z. given clause #428: (wt=13) 2915 [copy,2905,flip.1] x v c(x)= (y v (c(z) v u)) v z. given clause #429: (wt=19) 2093 [back_demod,472,demod,1811,1811,37] x v (c(y) v c(c(z) v (c(x) v c(u))))=c(y) v x. given clause #430: (wt=13) 2967 [para_into,2764,1464] (x v y) v c(z v c(y))=x v y. given clause #431: (wt=13) 2969 [para_into,2764,1460] (x v y) v c(z v c(x))=x v y. given clause #432: (wt=13) 2987 [para_from,2613,2144] x v c(c(y) v ((y v z) v u))=x. given clause #433: (wt=23) 2097 [back_demod,208,demod,1811,1811,37,1811,1811,37] x v c(c(y) v (c(z) v c(u)))=x v c(c(z) v (c(y) v c(u))). given clause #434: (wt=13) 2989 [para_from,2613,2110] x v c(((y v z) v u) v c(y))=x. given clause #435: (wt=13) 2993 [para_from,2613,2375] c(x) v ((x v y) v z)=c(u) v u. given clause #436: (wt=13) 2994 [para_from,2613,2374] c(x) v ((x v y) v z)=u v c(u). given clause #437: (wt=17) 2098 [back_demod,206,demod,1811,1811] x v c(c(y) v c(z))=x v c(c(z) v c(y)). given clause #438: (wt=13) 2995 [para_from,2613,2364] c(c(x) v ((x v y) v z)) v u=u. given clause #439: (wt=13) 2997 [para_from,2613,2251] ((x v y) v z) v c(x)=c(u) v u. given clause #440: (wt=13) 2998 [para_from,2613,2250] ((x v y) v z) v c(x)=u v c(u). given clause #441: (wt=23) 2099 [back_demod,203,demod,1811,1811,37,1811,1811,37] c(c(x) v (c(y) v c(z))) v u=c(c(y) v (c(x) v c(z))) v u. given clause #442: (wt=13) 2999 [para_from,2613,2244] c(((x v y) v z) v c(x)) v u=u. given clause #443: (wt=13) 3001 [para_from,2613,1365,demod,37] ((x v y) v z) v x= (x v y) v z. given clause #444: (wt=13) 3003 [para_from,2613,914,demod,37] x v ((x v y) v z)= (x v y) v z. given clause #445: (wt=19) 2101 [back_demod,146,demod,1811,1811,37,1811,1811,37] c(c(x) v (c(y) v c(z)))=c(c(y) v (c(x) v c(z))). given clause #446: (wt=13) 3005 [copy,2993,flip.1] c(x) v x=c(y) v ((y v z) v u). given clause #447: (wt=13) 3006 [copy,2994,flip.1] x v c(x)=c(y) v ((y v z) v u). given clause #448: (wt=13) 3007 [copy,2997,flip.1] c(x) v x= ((y v z) v u) v c(y). given clause #449: (wt=15) 2130 [para_from,1837,434,demod,1838] x v ((y v z) v c(z))= (y v z) v c(z). given clause #450: (wt=13) 3008 [copy,2998,flip.1] x v c(x)= ((y v z) v u) v c(y). given clause #451: (wt=13) 3017 [para_from,2625,2144] x v c(c(y) v (z v (u v y)))=x. given clause #452: (wt=13) 3019 [para_from,2625,2110] x v c((y v (z v u)) v c(u))=x. given clause #453: (wt=15) 2132 [para_from,1837,432,demod,1838] ((x v y) v c(y)) v z= (x v y) v c(y). given clause #454: (wt=13) 3025 [para_from,2625,2375] c(x) v (y v (z v x))=c(u) v u. given clause #455: (wt=13) 3026 [para_from,2625,2374] c(x) v (y v (z v x))=u v c(u). given clause #456: (wt=13) 3027 [para_from,2625,2364] c(c(x) v (y v (z v x))) v u=u. given clause #457: (wt=15) 2162 [para_from,1839,434,demod,1840] x v ((y v z) v c(y))= (y v z) v c(y). given clause #458: (wt=13) 3029 [para_from,2625,2251] (x v (y v z)) v c(z)=c(u) v u. given clause #459: (wt=13) 3030 [para_from,2625,2250] (x v (y v z)) v c(z)=u v c(u). given clause #460: (wt=13) 3031 [para_from,2625,2244] c((x v (y v z)) v c(z)) v u=u. given clause #461: (wt=15) 2164 [para_from,1839,432,demod,1840] ((x v y) v c(x)) v z= (x v y) v c(x). given clause #462: (wt=13) 3033 [para_from,2625,1365,demod,37] (x v (y v z)) v z=x v (y v z). given clause #463: (wt=13) 3035 [para_from,2625,914,demod,37] x v (y v (z v x))=y v (z v x). given clause #464: (wt=13) 3037 [copy,3025,flip.1] c(x) v x=c(y) v (z v (u v y)). given clause #465: (wt=15) 2182 [para_from,2104,434,demod,2105] x v (c(y) v (z v y))=c(y) v (z v y). given clause #466: (wt=13) 3038 [copy,3026,flip.1] x v c(x)=c(y) v (z v (u v y)). given clause #467: (wt=13) 3039 [copy,3029,flip.1] c(x) v x= (y v (z v u)) v c(u). given clause #468: (wt=13) 3040 [copy,3030,flip.1] x v c(x)= (y v (z v u)) v c(u). given clause #469: (wt=15) 2184 [para_from,2104,432,demod,2105] (c(x) v (y v x)) v z=c(x) v (y v x). given clause #470: (wt=13) 3045 [para_from,2627,2144] x v c(c(y) v (z v (y v u)))=x. given clause #471: (wt=13) 3047 [para_from,2627,2110] x v c((y v (z v u)) v c(z))=x. given clause #472: (wt=13) 3053 [para_from,2627,2375] c(x) v (y v (x v z))=c(u) v u. given clause #473: (wt=15) 2202 [para_from,2106,434,demod,2107] x v (c(y) v (y v z))=c(y) v (y v z). given clause #474: (wt=13) 3054 [para_from,2627,2374] c(x) v (y v (x v z))=u v c(u). given clause #475: (wt=13) 3055 [para_from,2627,2364] c(c(x) v (y v (x v z))) v u=u. given clause #476: (wt=13) 3057 [para_from,2627,2251] (x v (y v z)) v c(y)=c(u) v u. given clause #477: (wt=15) 2204 [para_from,2106,432,demod,2107] (c(x) v (x v y)) v z=c(x) v (x v y). given clause #478: (wt=13) 3058 [para_from,2627,2250] (x v (y v z)) v c(y)=u v c(u). given clause #479: (wt=13) 3059 [para_from,2627,2244] c((x v (y v z)) v c(y)) v u=u. given clause #480: (wt=13) 3061 [para_from,2627,1365,demod,37] (x v (y v z)) v y=x v (y v z). given clause #481: (wt=15) 2234 [para_from,2108,434,demod,2109] x v (y v (z v c(y)))=y v (z v c(y)). given clause #482: (wt=13) 3063 [para_from,2627,914,demod,37] x v (y v (x v z))=y v (x v z). given clause #483: (wt=13) 3065 [copy,3053,flip.1] c(x) v x=c(y) v (z v (y v u)). given clause #484: (wt=13) 3066 [copy,3054,flip.1] x v c(x)=c(y) v (z v (y v u)). given clause #485: (wt=15) 2236 [para_from,2108,432,demod,2109] (x v (y v c(x))) v z=x v (y v c(x)). given clause #486: (wt=13) 3067 [copy,3057,flip.1] c(x) v x= (y v (z v u)) v c(z). given clause #487: (wt=13) 3068 [copy,3058,flip.1] x v c(x)= (y v (z v u)) v c(z). given clause #488: (wt=13) 3103 [para_into,1756,218] x v c(y v z)=c(z v y) v x. given clause #489: (wt=15) 2254 [para_from,2110,434,demod,2111] x v (y v (c(y) v z))=y v (c(y) v z). given clause #490: (wt=13) 3104 [para_into,1756,217] x v c(x)=c(y v z) v (z v y). given clause #491: (wt=13) 3105 [para_into,1756,216] c(x) v x=c(y v z) v (z v y). given clause #492: (wt=13) 3121 [copy,3103,flip.1] c(x v y) v z=z v c(y v x). given clause #493: (wt=15) 2256 [para_from,2110,432,demod,2111] (x v (c(x) v y)) v z=x v (c(x) v y). given clause #494: (wt=13) 3122 [copy,3104,flip.1] c(x v y) v (y v x)=z v c(z). given clause #495: (wt=13) 3123 [copy,3105,flip.1] c(x v y) v (y v x)=c(z) v z. given clause #496: (wt=13) 3156 [para_from,1756,444,demod,37] x v c(c(y v z) v (z v y))=x. given clause #497: (wt=15) 2278 [para_from,2112,434,demod,2113] x v ((y v c(z)) v z)= (y v c(z)) v z. given clause #498: (wt=13) 3161 [para_from,1756,442,demod,37] c(c(x v y) v (y v x)) v z=z. given clause #499: (wt=13) 3198 [para_from,3093,444] x v c((y v z) v c(z v y))=x. given clause #500: (wt=13) 3237 [para_from,3093,442] c((x v y) v c(y v x)) v z=z. given clause #501: (wt=15) 2280 [para_from,2112,432,demod,2113] ((x v c(y)) v y) v z= (x v c(y)) v y. given clause #502: (wt=13) 3240 [para_from,3093,214] (x v y) v c(y v x)=z v c(z). given clause #503: (wt=13) 3241 [para_from,3093,213] (x v y) v c(y v x)=c(z) v z. given clause #504: (wt=13) 3262 [copy,3240,flip.1] x v c(x)= (y v z) v c(z v y). given clause #505: (wt=21) 2282 [para_into,966,36,demod,37] x v (c(c(y) v (x v c(z))) v (c(y) v c(z)))=c(u) v u. given clause #506: (wt=13) 3263 [copy,3241,flip.1] c(x) v x= (y v z) v c(z v y). given clause #507: (wt=13) 4503 [para_into,2647,2892,demod,37,2893] c((x v (c(y) v z)) v u) v y=y. given clause #508: (wt=13) 4505 [para_into,2647,2764,demod,37,2765] c((x v (y v c(z))) v u) v z=z. given clause #509: (wt=22) 2286 [para_into,966,1464] c(x) v (c(c(y) v c(x)) v (c(y) v c(z v x)))=c(u) v u. given clause #510: (wt=13) 4507 [para_into,2647,2736,demod,37,2737] c(((c(x) v y) v z) v u) v x=x. given clause #511: (wt=13) 4509 [para_into,2647,2710,demod,37,2711] c(((x v c(y)) v z) v u) v y=y. given clause #512: (wt=13) 4517 [para_from,2647,2144] x v c((y v z) v (c(z) v u))=x. given clause #513: (wt=22) 2287 [para_into,966,1460] c(x) v (c(c(y) v c(x)) v (c(y) v c(x v z)))=c(u) v u. given clause #514: (wt=13) 4519 [para_from,2647,2110] x v c((c(y) v z) v (u v y))=x. given clause #515: (wt=13) 4539 [para_from,2647,2375] (x v y) v (c(y) v z)=c(u) v u. given clause #516: (wt=13) 4540 [para_from,2647,2374] (x v y) v (c(y) v z)=u v c(u). given clause #517: (wt=15) 2304 [para_into,2120,2112] c((x v y) v c(y))=c((z v c(u)) v u). given clause #518: (wt=13) 4542 [para_from,2647,2364] c((x v y) v (c(y) v z)) v u=u. given clause #519: (wt=13) 4547 [para_from,2647,2251] (c(x) v y) v (z v x)=c(u) v u. given clause #520: (wt=13) 4548 [para_from,2647,2250] (c(x) v y) v (z v x)=u v c(u). given clause #521: (wt=15) 2305 [para_into,2120,2110] c((x v y) v c(y))=c(z v (c(z) v u)). given clause #522: (wt=13) 4549 [para_from,2647,2244] c((c(x) v y) v (z v x)) v u=u. given clause #523: (wt=13) 4567 [copy,4539,flip.1] c(x) v x= (y v z) v (c(z) v u). given clause #524: (wt=13) 4568 [copy,4540,flip.1] x v c(x)= (y v z) v (c(z) v u). given clause #525: (wt=15) 2306 [para_into,2120,2108] c((x v y) v c(y))=c(z v (u v c(z))). given clause #526: (wt=13) 4573 [copy,4547,flip.1] c(x) v x= (c(y) v z) v (u v y). given clause #527: (wt=13) 4574 [copy,4548,flip.1] x v c(x)= (c(y) v z) v (u v y). given clause #528: (wt=13) 4617 [para_from,2649,2144] x v c((y v z) v (c(y) v u))=x. given clause #529: (wt=15) 2307 [para_into,2120,2106] c((x v y) v c(y))=c(c(z) v (z v u)). given clause #530: (wt=13) 4619 [para_from,2649,2110] x v c((c(y) v z) v (y v u))=x. given clause #531: (wt=13) 4639 [para_from,2649,2375] (x v y) v (c(x) v z)=c(u) v u. given clause #532: (wt=13) 4640 [para_from,2649,2374] (x v y) v (c(x) v z)=u v c(u). given clause #533: (wt=15) 2308 [para_into,2120,2104] c((x v y) v c(y))=c(c(z) v (u v z)). given clause #534: (wt=13) 4642 [para_from,2649,2364] c((x v y) v (c(x) v z)) v u=u. given clause #535: (wt=13) 4647 [para_from,2649,2251] (c(x) v y) v (x v z)=c(u) v u. given clause #536: (wt=13) 4648 [para_from,2649,2250] (c(x) v y) v (x v z)=u v c(u). given clause #537: (wt=15) 2309 [para_into,2120,1839] c((x v y) v c(y))=c((z v u) v c(z)). given clause #538: (wt=13) 4649 [para_from,2649,2244] c((c(x) v y) v (x v z)) v u=u. given clause #539: (wt=13) 4667 [copy,4639,flip.1] c(x) v x= (y v z) v (c(y) v u). given clause #540: (wt=13) 4668 [copy,4640,flip.1] x v c(x)= (y v z) v (c(y) v u). given clause #541: (wt=15) 2310 [para_into,2120,1837] c((x v y) v c(y))=c((z v u) v c(u)). given clause #542: (wt=13) 4673 [copy,4647,flip.1] c(x) v x= (c(y) v z) v (y v u). given clause #543: (wt=13) 4674 [copy,4648,flip.1] x v c(x)= (c(y) v z) v (y v u). given clause #544: (wt=13) 4697 [para_into,2657,1374,demod,37] x v c((y v c(z)) v (z v u))=x. given clause #545: (wt=15) 2311 [copy,2304,flip.1] c((x v c(y)) v y)=c((z v u) v c(u)). given clause #546: (wt=13) 4795 [para_into,2659,1374,demod,37] x v c((y v z) v (u v c(y)))=x. given clause #547: (wt=13) 4904 [para_into,2661,1374,demod,37] (x v c(y)) v (y v z)=c(u) v u. given clause #548: (wt=13) 4914 [copy,4904,flip.1] c(x) v x= (y v c(z)) v (z v u). given clause #549: (wt=15) 2312 [copy,2305,flip.1] c(x v (c(x) v y))=c((z v u) v c(u)). given clause #550: (wt=13) 4924 [para_into,2662,1374,demod,37] (x v c(y)) v (y v z)=u v c(u). given clause #551: (wt=13) 4934 [copy,4924,flip.1] x v c(x)= (y v c(z)) v (z v u). given clause #552: (wt=13) 4953 [para_into,2663,1374,demod,37] c((x v c(y)) v (y v z)) v u=u. given clause #553: (wt=15) 2313 [copy,2306,flip.1] c(x v (y v c(x)))=c((z v u) v c(u)). given clause #554: (wt=13) 5012 [para_into,2665,1374,demod,37] (x v y) v (z v c(x))=c(u) v u. given clause #555: (wt=13) 5022 [copy,5012,flip.1] c(x) v x= (y v z) v (u v c(y)). given clause #556: (wt=13) 5032 [para_into,2666,1374,demod,37] (x v y) v (z v c(x))=u v c(u). given clause #557: (wt=15) 2314 [copy,2307,flip.1] c(c(x) v (x v y))=c((z v u) v c(u)). given clause #558: (wt=13) 5042 [copy,5032,flip.1] x v c(x)= (y v z) v (u v c(y)). given clause #559: (wt=13) 5060 [para_into,2667,1374,demod,37] c((x v y) v (z v c(x))) v u=u. given clause #560: (wt=13) 5131 [para_from,2669,2892] x v c((y v (c(x) v z)) v u)=x. given clause #561: (wt=15) 2315 [copy,2308,flip.1] c(c(x) v (y v x))=c((z v u) v c(u)). given clause #562: (wt=13) 5133 [para_from,2669,2764] x v c((y v (z v c(x))) v u)=x. given clause #563: (wt=13) 5135 [para_from,2669,2764] x v c(y v ((z v c(x)) v u))=x. given clause #564: (wt=13) 5137 [para_from,2669,2710] x v c(((y v c(x)) v z) v u)=x. given clause #565: (wt=15) 2316 [copy,2309,flip.1] c((x v y) v c(x))=c((z v u) v c(u)). given clause #566: (wt=13) 5139 [para_from,2669,2708] c(x v ((y v c(z)) v u)) v z=z. given clause #567: (wt=13) 5178 [para_from,5126,3093] c((x v y) v z)=c(z v (y v x)). given clause #568: (wt=13) 5184 [copy,5178,flip.1] c(x v (y v z))=c((z v y) v x). given clause #569: (wt=21) 2330 [para_into,1076,36,demod,37] x v (c(c(y) v (x v c(z))) v (c(y) v c(z)))=u v c(u). given clause #570: (wt=13) 5206 [para_from,5169,3093] c((x v y) v z)=c((y v x) v z). given clause #571: (wt=13) 5256 [para_from,5174,3093] c(x v (y v z))=c(x v (z v y)). given clause #572: (wt=13) 5986 [para_into,2758,2892,demod,37,2893] c(x v (y v (c(z) v u))) v z=z. given clause #573: (wt=22) 2334 [para_into,1076,1464] c(x) v (c(c(y) v c(x)) v (c(y) v c(z v x)))=u v c(u). given clause #574: (wt=13) 5988 [para_into,2758,2764,demod,37,2765] c(x v (y v (z v c(u)))) v u=u. given clause #575: (wt=13) 5990 [para_into,2758,2736,demod,37,2737] c(x v ((c(y) v z) v u)) v y=y. given clause #576: (wt=13) 6001 [para_from,2758,2144] x v c((y v z) v (u v c(z)))=x. given clause #577: (wt=22) 2335 [para_into,1076,1460] c(x) v (c(c(y) v c(x)) v (c(y) v c(x v z)))=u v c(u). given clause #578: (wt=13) 6003 [para_from,2758,2110] x v c((y v c(z)) v (u v z))=x. given clause #579: (wt=13) 6031 [para_from,2758,2375] (x v y) v (z v c(y))=c(u) v u. given clause #580: (wt=13) 6032 [para_from,2758,2374] (x v y) v (z v c(y))=u v c(u). given clause #581: (wt=15) 2357 [para_into,2144,2120] c((c(x) v y) v x)=c((z v u) v c(u)). given clause #582: (wt=13) 6034 [para_from,2758,2364] c((x v y) v (z v c(y))) v u=u. given clause #583: (wt=13) 6039 [para_from,2758,2251] (x v c(y)) v (z v y)=c(u) v u. given clause #584: (wt=13) 6040 [para_from,2758,2250] (x v c(y)) v (z v y)=u v c(u). given clause #585: (wt=15) 2371 [copy,2357,flip.1] c((x v y) v c(y))=c((c(z) v u) v z). given clause #586: (wt=13) 6041 [para_from,2758,2244] c((x v c(y)) v (z v y)) v u=u. given clause #587: (wt=13) 6063 [copy,6031,flip.1] c(x) v x= (y v z) v (u v c(z)). given clause #588: (wt=13) 6064 [copy,6032,flip.1] x v c(x)= (y v z) v (u v c(z)). given clause #589: (wt=15) 2378 [para_from,2144,434,demod,2145] x v ((c(y) v z) v y)= (c(y) v z) v y. given clause #590: (wt=13) 6069 [copy,6039,flip.1] c(x) v x= (y v c(z)) v (u v z). given clause #591: (wt=13) 6070 [copy,6040,flip.1] x v c(x)= (y v c(z)) v (u v z). given clause #592: (wt=13) 6643 [para_into,2874,2736,demod,37,2737] x v c(((c(x) v y) v z) v u)=x. given clause #593: (wt=15) 2380 [para_from,2144,432,demod,2145] ((c(x) v y) v x) v z= (c(x) v y) v x. given clause #594: (wt=13) 7055 [para_into,2967,2892,demod,37,2893] x v c(y v (z v (c(x) v u)))=x. given clause #595: (wt=13) 7059 [para_into,2967,2764,demod,37,2765] x v c(y v (z v (u v c(x))))=x. given clause #596: (wt=13) 7061 [para_into,2967,2736,demod,37,2737] x v c(y v ((c(x) v z) v u))=x. given clause #597: (wt=18) 2385 [para_into,1121,36,demod,37] (c(x) v c(y)) v (z v c(x))=z v (c(x) v c(y)). given clause #598: (wt=13) 8236 [para_into,3121,218] x v c(y v z)=x v c(z v y). given clause #599: (wt=14) 2607 [para_into,1260,36,demod,37] c(x v y) v (z v c(x))=z v c(x). given clause #600: (wt=14) 2621 [para_into,1264,36,demod,37] c(x v y) v (z v c(y))=z v c(y). given clause #601: (wt=15) 2398 [para_into,2154,2144] c((x v y) v c(x))=c((c(z) v u) v z). given clause #602: (wt=14) 2631 [para_into,1268,36,demod,37] c(x) v (y v c(x v z))=y v c(x). given clause #603: (wt=13) 14543 [para_into,2631,36,demod,37] x v (y v c(c(x) v z))=y v x. given clause #604: (wt=13) 14564 [para_into,2631,2631,demod,37,37] x v (y v c(z v c(x)))=y v x. given clause #605: (wt=15) 2399 [para_into,2154,2112] c((x v y) v c(x))=c((z v c(u)) v u). given clause #606: (wt=13) 14574 [para_into,2631,1372,demod,37,37,37] (x v y) v (z v y)=z v (x v y). ----> UNIT CONFLICT at 10.85 sec ----> 15297 [binary,15296,1] $Ans(AJ). Length of proof is 51. Level of proof is 21. ---------------- PROOF ---------------- 1 [] A v (B v C)!=B v (A v C)|$Ans(AJ). 8 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 9 [] f(f(x,x),f(x,y))=x. 11 [] f(x,f(x,x))=f(y,f(y,y)). 12 [] x v y=f(f(x,x),f(y,y)). 13 [copy,12,flip.1] f(f(x,x),f(y,y))=x v y. 15 [] x^y=f(f(x,y),f(x,y)). 16 [copy,15,flip.1] f(f(x,y),f(x,y))=x^y. 18 [] c(x)=f(x,x). 20,19 [copy,18,flip.1] f(x,x)=c(x). 21 [copy,8,flip.1,demod,20,20] f(x,c(f(y,z)))=f(y,c(f(x,z))). 22 [copy,11,flip.1,demod,20,20] f(x,c(x))=f(y,c(y)). 24,23 [back_demod,16,demod,20] c(f(x,y))=x^y. 25 [back_demod,13,demod,20,20] f(c(x),c(y))=x v y. 27 [back_demod,9,demod,20] f(c(x),f(x,y))=x. 29 [copy,21,flip.1,demod,24,24] f(x,y^z)=f(y,x^z). 37,36 [para_into,27,19,demod,20] c(c(x))=x. 41 [para_from,27,23,flip.1] c(x)^f(x,y)=c(x). 47 [para_from,22,23,demod,24] x^c(x)=y^c(y). 49,48 [para_into,36,23,flip.1] f(x,y)=c(x^y). 54 [back_demod,41,demod,49] c(x)^c(x^y)=c(x). 58 [back_demod,29,demod,49,49] c(x^ (y^z))=c(y^ (x^z)). 59 [back_demod,25,demod,49] c(c(x)^c(y))=x v y. 64 [para_into,47,36] c(x)^x=y^c(y). 87 [para_into,54,36,demod,37] x^c(c(x)^y)=x. 92,91 [para_into,54,64,demod,37,37] x^c(y^c(y))=x. 103 [para_into,58,91,demod,92] c(x^y)=c(y^x). 162 [para_from,103,87] x^c(y^c(x))=x. 182 [para_from,103,36,demod,37] x^y=y^x. 205,204 [para_into,59,36] c(x^c(y))=c(x) v y. 218 [para_into,59,103,demod,205,37] x v y=y v x. 223 [back_demod,162,demod,205] x^ (c(y) v x)=x. 330 [para_into,223,36] x^ (y v x)=x. 340 [para_into,330,218] x^ (x v y)=x. 344 [para_into,330,182] (x v y)^y=y. 380 [para_into,340,182] (x v y)^x=x. 386 [para_from,340,58,flip.1] c(x^ (y^ (x v z)))=c(y^x). 400 [para_from,380,58,flip.1] c((x v y)^ (z^x))=c(z^x). 913,912 [para_into,204,36] c(x^y)=c(x) v c(y). 914 [para_into,204,380,demod,37,flip.1] c(c(x) v y) v x=x. 916 [para_into,204,344,demod,37,flip.1] c(x v c(y)) v y=y. 1260 [back_demod,400,demod,913,913,913] c(x v y) v (c(z) v c(x))=c(z) v c(x). 1268 [back_demod,386,demod,913,913,913] c(x) v (c(y) v c(x v z))=c(y) v c(x). 1365 [para_into,914,218] x v c(c(x) v y)=x. 1372 [para_into,916,36] c(x v y) v c(y)=c(y). 1374 [para_into,916,218] x v c(y v c(x))=x. 1461,1460 [para_into,1365,36] c(x) v c(x v y)=c(x). 1465,1464 [para_into,1374,36] c(x) v c(y v x)=c(x). 2611 [para_into,1260,1464,demod,1465] c((x v y) v z) v c(y)=c(y). 2613 [para_into,1260,1460,demod,1461] c((x v y) v z) v c(x)=c(x). 2631 [para_into,1268,36,demod,37] c(x) v (y v c(x v z))=y v c(x). 2669 [para_from,2611,1365,demod,37] ((x v y) v z) v y= (x v y) v z. 3002,3001 [para_from,2613,1365,demod,37] ((x v y) v z) v x= (x v y) v z. 5126 [para_into,2669,218,demod,3002] (x v y) v z= (y v x) v z. 5169 [para_into,5126,218] x v (y v z)= (z v y) v x. 14574 [para_into,2631,1372,demod,37,37,37] (x v y) v (z v y)=z v (x v y). 15295,15294 [para_into,14574,5169] (x v y) v (z v x)=y v (z v x). 15296 [para_into,14574,5126,demod,15295] x v (y v z)=y v (x v z). 15297 [binary,15296,1] $Ans(AJ). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 606 clauses generated 290057 clauses kept 12422 clauses forward subsumed 287496 clauses back subsumed 328 Kbytes malloced 9612 ----------- times (seconds) ----------- user CPU time 10.85 (0 hr, 0 min, 10 sec) system CPU time 2.92 (0 hr, 0 min, 2 sec) wall-clock time 14 (0 hr, 0 min, 14 sec) para_into time 0.62 para_from time 0.62 for_sub time 0.83 back_sub time 1.17 conflict time 0.03 demod time 2.62 That finishes the proof of the theorem. Process 26009 finished Fri Sep 12 16:34:53 2003