----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:36:19 2003 The command was "otter". The process ID is 26080. 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------- lex([A,B,C,D,0,1,x v x,x^x,c(x),f(x,x)]). assign(max_proofs,2). list(sos). 0 [] x v (y v z)=y v (x v z). 0 [] x^y=c(c(x) v c(y)). 0 [] x v c(x)=y v c(y). 0 [] (x v c(y))^ (x v y)=x. 0 [] x v c(x)=1. 0 [] c(1)=0. end_of_list. list(passive). 1 [] A v (A^B)!=A|$Ans(B1). 2 [] c(c(A))!=A|$Ans(CC). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 3 [] x=x. Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=11): 4 [] x v (y v z)=y v (x v z). ** KEPT (pick-wt=10): 6 [copy,5,flip.1] c(c(x) v c(y))=x^y. ---> New Demodulator: 7 [new_demod,6] c(c(x) v c(y))=x^y. ** KEPT (pick-wt=9): 8 [] x v c(x)=y v c(y). ** KEPT (pick-wt=10): 9 [] (x v c(y))^ (x v y)=x. ---> New Demodulator: 10 [new_demod,9] (x v c(y))^ (x v y)=x. ** KEPT (pick-wt=6): 11 [] x v c(x)=1. ---> New Demodulator: 12 [new_demod,11] x v c(x)=1. ** KEPT (pick-wt=4): 13 [] c(1)=0. ---> New Demodulator: 14 [new_demod,13] c(1)=0. Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] x v (y v z)=y v (x v z). >>>> Starting back demodulation with 7. Following clause subsumed by 3 during input processing: 0 [copy,8,flip.1,demod,12,12] 1=1. >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 12. >> back demodulating 8 with 12. >>>> Starting back demodulation with 14. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 4 [] x v (y v z)=y v (x v z). given clause #2: (wt=4) 13 [] c(1)=0. given clause #3: (wt=6) 11 [] x v c(x)=1. given clause #4: (wt=5) 17 [para_into,11,13] 1 v 0=1. given clause #5: (wt=10) 6 [copy,5,flip.1] c(c(x) v c(y))=x^y. given clause #6: (wt=6) 31 [para_into,6,11,demod,14,flip.1] x^c(x)=0. given clause #7: (wt=5) 35 [para_into,31,13] 1^0=0. given clause #8: (wt=9) 21 [para_from,17,4] x v 1=1 v (x v 0). given clause #9: (wt=10) 9 [] (x v c(y))^ (x v y)=x. given clause #10: (wt=7) 45 [para_into,9,11] 1^ (x v x)=x. given clause #11: (wt=8) 49 [para_into,9,17] (1 v c(0))^1=1. given clause #12: (wt=9) 22 [copy,21,flip.1] 1 v (x v 0)=x v 1. given clause #13: (wt=15) 15 [para_into,4,4] x v (y v (z v u))=z v (x v (y v u)). given clause #14: (wt=9) 23 [para_into,6,13] c(0 v c(x))=1^x. given clause #15: (wt=8) 82 [para_into,23,13] c(0 v 0)=1^1. given clause #16: (wt=9) 27 [para_into,6,13] c(c(x) v 0)=x^1. given clause #17: (wt=15) 16 [copy,15,flip.1] x v (y v (z v u))=y v (z v (x v u)). given clause #18: (wt=9) 41 [para_into,9,13] (x v 0)^ (x v 1)=x. given clause #19: (wt=9) 51 [para_into,9,11] (x v c(c(x)))^1=x. given clause #20: (wt=9) 94 [para_from,82,31] (0 v 0)^ (1^1)=0. given clause #21: (wt=10) 19 [para_from,11,4,flip.1] x v (y v c(x))=y v 1. given clause #22: (wt=9) 96 [para_from,82,11] (0 v 0) v (1^1)=1. given clause #23: (wt=10) 88 [para_from,23,31] (0 v c(x))^ (1^x)=0. given clause #24: (wt=9) 155 [para_into,88,82,demod,46] (0 v (1^1))^0=0. given clause #25: (wt=15) 25 [para_into,6,6] c((x^y) v c(z))= (c(x) v c(y))^z. given clause #26: (wt=10) 90 [para_from,23,11] (0 v c(x)) v (1^x)=1. given clause #27: (wt=9) 192 [para_into,90,82,demod,46] (0 v (1^1)) v 0=1. given clause #28: (wt=7) 209 [back_demod,200,demod,203,46,flip.1] 0 v (1^1)=1. given clause #29: (wt=15) 29 [para_into,6,6] c(c(x) v (y^z))=x^ (c(y) v c(z)). given clause #30: (wt=10) 108 [para_from,27,31] (c(x) v 0)^ (x^1)=0. given clause #31: (wt=10) 110 [para_from,27,11] (c(x) v 0) v (x^1)=1. given clause #32: (wt=10) 163 [para_into,88,45] (0 v c(x v x))^x=0. given clause #33: (wt=11) 33 [para_from,6,11] (c(x) v c(y)) v (x^y)=1. given clause #34: (wt=10) 196 [para_into,90,45] (0 v c(x v x)) v x=1. given clause #35: (wt=10) 214 [para_from,209,9] (0 v c(1^1))^1=0. given clause #36: (wt=11) 37 [para_into,31,6] (c(x) v c(y))^ (x^y)=0. given clause #37: (wt=13) 39 [para_from,21,4] x v (1 v (y v 0))=y v (x v 1). given clause #38: (wt=11) 47 [para_into,9,21,demod,14] (x v 0)^ (1 v (x v 0))=x. given clause #39: (wt=11) 216 [para_from,209,4,flip.1] 0 v (x v (1^1))=x v 1. given clause #40: (wt=9) 366 [para_into,216,196,demod,181,14,14,14,14,305,flip.1] (0 v 0) v 1=0 v 1. given clause #41: (wt=13) 40 [copy,39,flip.1] x v (y v 1)=y v (1 v (x v 0)). given clause #42: (wt=11) 304 [para_from,196,19,demod,169,28,220,226,flip.1] (0 v (x^x)) v 1=x v 1. given clause #43: (wt=11) 320 [para_from,214,110,demod,169,83,171] ((1^ (1^1)) v 0) v 0=1. given clause #44: (wt=9) 419 [para_from,320,47,demod,321,46,flip.1] (1^ (1^1)) v 0=1. given clause #45: (wt=15) 43 [para_into,9,6] (x v (y^z))^ (x v (c(y) v c(z)))=x. given clause #46: (wt=7) 422 [para_from,419,47,demod,420,46,flip.1] 1^ (1^1)=1. given clause #47: (wt=9) 438 [para_into,43,209,demod,14,14] 1^ (0 v (0 v 0))=0. given clause #48: (wt=10) 462 [para_from,422,90] (0 v c(1^1)) v 1=1. given clause #49: (wt=14) 53 [para_into,9,4] (x v c(y v z))^ (y v (x v z))=x. given clause #50: (wt=11) 372 [para_into,366,21] 1 v ((0 v 0) v 0)=0 v 1. given clause #51: (wt=12) 57 [para_from,22,9] (1 v c(x v 0))^ (x v 1)=1. given clause #52: (wt=11) 568 [para_into,57,82] (1 v (1^1))^ (0 v 1)=1. given clause #53: (wt=13) 55 [para_into,45,4] 1^ (x v ((x v y) v y))=x v y. given clause #54: (wt=12) 294 [para_into,196,21] 1 v ((0 v c(1 v 1)) v 0)=1. given clause #55: (wt=12) 452 [para_into,43,19] (x v (y^x))^ (c(y) v 1)=x. given clause #56: (wt=11) 663 [para_into,452,13] (x v (1^x))^ (0 v 1)=x. given clause #57: (wt=13) 59 [para_from,22,4] x v (y v 1)=1 v (x v (y v 0)). given clause #58: (wt=12) 468 [para_from,438,90] (0 v c(0 v (0 v 0))) v 0=1. given clause #59: (wt=10) 714 [para_from,468,47,demod,469,46,flip.1] 0 v c(0 v (0 v 0))=1. given clause #60: (wt=11) 716 [para_from,714,53] 1^ (0 v (0 v (0 v 0)))=0. given clause #61: (wt=13) 60 [copy,59,flip.1] 1 v (x v (y v 0))=x v (y v 1). given clause #62: (wt=11) 718 [para_from,714,19] (0 v (0 v 0)) v 1=0 v 1. given clause #63: (wt=12) 476 [para_into,462,21] 1 v ((0 v c(1^1)) v 0)=1. given clause #64: (wt=13) 92 [para_from,82,9] (x v (1^1))^ (x v (0 v 0))=x. given clause #65: (wt=17) 61 [para_into,15,22] x v (y v (z v 1))=1 v (x v (y v (z v 0))). given clause #66: (wt=13) 116 [para_into,16,22] x v (y v 1)=1 v (y v (x v 0)). given clause #67: (wt=13) 124 [copy,116,flip.1] 1 v (x v (y v 0))=y v (x v 1). given clause #68: (wt=13) 141 [para_into,19,82] (0 v 0) v (x v (1^1))=x v 1. given clause #69: (wt=17) 62 [para_into,15,21] x v (y v (1 v (z v 0)))=z v (x v (y v 1)). given clause #70: (wt=13) 244 [para_into,108,82] ((1^1) v 0)^ ((0 v 0)^1)=0. given clause #71: (wt=13) 252 [para_into,110,82] ((1^1) v 0) v ((0 v 0)^1)=1. given clause #72: (wt=13) 282 [para_into,33,41] (c(x v 0) v c(x v 1)) v x=1. given clause #73: (wt=23) 63 [para_into,15,15] x v (y v (z v (u v (v v w))))=u v (x v (y v (v v (z v w)))). given clause #74: (wt=10) 946 [para_from,282,47,demod,83,903,46,83,flip.1] (1^1) v c(0 v 1)=1. given clause #75: (wt=7) 1036 [back_demod,1017,demod,1020,56,flip.1] 1^1=0 v 1. given clause #76: (wt=7) 1114 [back_demod,422,demod,1037] 1^ (0 v 1)=1. given clause #77: (wt=14) 64 [para_into,15,11,flip.1] x v (y v (z v c(x)))=y v (z v 1). given clause #78: (wt=7) 1138 [back_demod,209,demod,1037] 0 v (0 v 1)=1. given clause #79: (wt=8) 1150 [back_demod,82,demod,1037] c(0 v 0)=0 v 1. given clause #80: (wt=9) 1146 [back_demod,96,demod,1037] (0 v 0) v (0 v 1)=1. given clause #81: (wt=19) 66 [para_into,15,4] x v (y v (z v (u v v)))=u v (x v (y v (z v v))). given clause #82: (wt=9) 1168 [para_into,1114,21] 1^ (1 v (0 v 0))=1. given clause #83: (wt=9) 1181 [para_into,1138,21] 0 v (1 v (0 v 0))=1. given clause #84: (wt=9) 1183 [para_into,1138,116] 1 v (0 v (0 v 0))=1. given clause #85: (wt=19) 67 [para_into,15,15] x v (y v (z v (u v v)))=u v (x v (z v (y v v))). given clause #86: (wt=10) 1108 [back_demod,462,demod,1037] (0 v c(0 v 1)) v 1=1. given clause #87: (wt=10) 1134 [back_demod,214,demod,1037] (0 v c(0 v 1))^1=0. given clause #88: (wt=11) 1132 [back_demod,216,demod,1037] 0 v (x v (0 v 1))=x v 1. given clause #89: (wt=15) 68 [para_into,15,4] x v (y v (z v u))=z v (y v (x v u)). given clause #90: (wt=11) 1164 [para_from,1036,452,demod,14] (1 v (0 v 1))^ (0 v 1)=1. given clause #91: (wt=11) 1189 [para_from,1138,16,flip.1] 0 v (0 v (x v 1))=x v 1. given clause #92: (wt=11) 1195 [para_into,1146,21] (0 v 0) v (1 v (0 v 0))=1. given clause #93: (wt=17) 69 [copy,61,flip.1] 1 v (x v (y v (z v 0)))=x v (y v (z v 1)). given clause #94: (wt=11) 1197 [para_into,1146,59] 1 v ((0 v 0) v (0 v 0))=1. given clause #95: (wt=11) 1458 [para_into,1164,40,demod,18] (0 v (1 v 1))^ (0 v 1)=1. given clause #96: (wt=12) 1044 [back_demod,1015,demod,1037] (0 v 1) v c(1 v (0 v 0))=1. given clause #97: (wt=17) 70 [copy,62,flip.1] x v (y v (z v 1))=y v (z v (1 v (x v 0))). given clause #98: (wt=12) 1102 [back_demod,476,demod,1037] 1 v ((0 v c(0 v 1)) v 0)=1. given clause #99: (wt=12) 1193 [para_from,1150,27] c((0 v 1) v 0)= (0 v 0)^1. given clause #100: (wt=12) 1269 [para_from,1168,90] (0 v c(1 v (0 v 0))) v 1=1. given clause #101: (wt=23) 71 [copy,63,flip.1] x v (y v (z v (u v (v v w))))=y v (z v (v v (x v (u v w)))). given clause #102: (wt=12) 1271 [para_from,1168,88] (0 v c(1 v (0 v 0)))^1=0. given clause #103: (wt=12) 1284 [para_from,1181,53] (1 v c(0 v (0 v 0)))^1=1. given clause #104: (wt=13) 338 [para_into,37,41] (c(x v 0) v c(x v 1))^x=0. given clause #105: (wt=19) 72 [copy,66,flip.1] x v (y v (z v (u v v)))=y v (z v (u v (x v v))). given clause #106: (wt=13) 378 [para_from,366,4] x v (0 v 1)= (0 v 0) v (x v 1). given clause #107: (wt=13) 386 [para_into,40,4] x v (y v 1)=x v (1 v (y v 0)). given clause #108: (wt=13) 389 [copy,386,flip.1] x v (1 v (y v 0))=x v (y v 1). given clause #109: (wt=19) 73 [copy,67,flip.1] x v (y v (z v (u v v)))=y v (u v (z v (x v v))). given clause #110: (wt=13) 406 [para_into,304,21] 1 v ((0 v (x^x)) v 0)=x v 1. given clause #111: (wt=13) 651 [para_into,452,45,demod,14] ((x v x) v x)^ (0 v 1)=x v x. given clause #112: (wt=13) 671 [para_into,663,21] (x v (1^x))^ (1 v (0 v 0))=x. given clause #113: (wt=19) 74 [para_from,15,45] 1^ (x v ((y v (x v z)) v (y v z)))=y v (x v z). given clause #114: (wt=13) 725 [para_from,714,9] (0 v c(c(0 v (0 v 0))))^1=0. given clause #115: (wt=13) 761 [para_into,718,21] 1 v ((0 v (0 v 0)) v 0)=0 v 1. given clause #116: (wt=13) 1042 [back_demod,639,demod,1037,1037] ((0 v 1) v 1)^ (0 v 1)=0 v 1. given clause #117: (wt=18) 76 [para_from,15,9] (x v c(y v (z v u)))^ (z v (x v (y v u)))=x. given clause #118: (wt=13) 1092 [back_demod,503,demod,1037] (x v (0 v 1))^ (0 v (x v 0))=x. given clause #119: (wt=13) 1128 [back_demod,252,demod,1037] ((0 v 1) v 0) v ((0 v 0)^1)=1. given clause #120: (wt=13) 1130 [back_demod,244,demod,1037] ((0 v 1) v 0)^ ((0 v 0)^1)=0. given clause #121: (wt=19) 78 [para_from,15,4] x v (y v (z v (u v v)))=z v (x v (u v (y v v))). given clause #122: (wt=13) 1142 [back_demod,141,demod,1037] (0 v 0) v (x v (0 v 1))=x v 1. given clause #123: (wt=13) 1148 [back_demod,92,demod,1037] (x v (0 v 1))^ (x v (0 v 0))=x. given clause #124: (wt=13) 1166 [para_from,1036,29,demod,14,14] c(c(x) v (0 v 1))=x^ (0 v 0). given clause #125: (wt=19) 79 [copy,78,flip.1] x v (y v (z v (u v v)))=y v (u v (x v (z v v))). given clause #126: (wt=13) 1187 [para_from,1138,61,flip.1] 1 v (x v (0 v (0 v 0)))=x v 1. given clause #127: (wt=13) 1203 [para_from,1146,16,flip.1] (0 v 0) v (0 v (x v 1))=x v 1. given clause #128: (wt=13) 1286 [para_from,1181,16,flip.1] 0 v (1 v (x v (0 v 0)))=x v 1. given clause #129: (wt=14) 84 [para_into,23,6] c(0 v (x^y))=1^ (c(x) v c(y)). given clause #130: (wt=13) 1295 [para_from,1181,4,flip.1] 0 v (x v (1 v (0 v 0)))=x v 1. given clause #131: (wt=13) 1301 [para_from,1183,16,flip.1] 1 v (0 v (x v (0 v 0)))=x v 1. given clause #132: (wt=13) 1387 [para_into,1132,116] 0 v (1 v (0 v (x v 0)))=x v 1. given clause #133: (wt=14) 86 [para_from,23,9] (x v (1^y))^ (x v (0 v c(y)))=x. given clause #134: (wt=13) 1388 [para_into,1132,40] 0 v (0 v (1 v (x v 0)))=x v 1. given clause #135: (wt=13) 1389 [copy,1387,flip.1] x v 1=0 v (1 v (0 v (x v 0))). given clause #136: (wt=13) 1390 [copy,1388,flip.1] x v 1=0 v (0 v (1 v (x v 0))). given clause #137: (wt=14) 104 [para_into,27,6] c((x^y) v 0)= (c(x) v c(y))^1. given clause #138: (wt=13) 1456 [para_into,1164,21] (1 v (1 v (0 v 0)))^ (0 v 1)=1. given clause #139: (wt=13) 1470 [para_into,1189,61] 1 v (0 v (0 v (x v 0)))=x v 1. given clause #140: (wt=13) 1559 [para_from,1044,19] (1 v (0 v 0)) v 1= (0 v 1) v 1. given clause #141: (wt=14) 106 [para_from,27,9] (x v (y^1))^ (x v (c(y) v 0))=x. given clause #142: (wt=13) 2135 [para_into,1092,4] (0 v (x v 1))^ (0 v (x v 0))=x. given clause #143: (wt=13) 2213 [para_into,1148,4] (0 v (x v 1))^ (x v (0 v 0))=x. given clause #144: (wt=13) 2235 [para_into,1166,4] c(0 v (c(x) v 1))=x^ (0 v 0). given clause #145: (wt=17) 112 [para_into,16,22] x v (y v (z v 1))=y v (1 v (x v (z v 0))). given clause #146: (wt=13) 2362 [para_into,1286,196,demod,2216,flip.1] ((1 v 1)^1) v 1=0 v (1 v 1). given clause #147: (wt=13) 2383 [para_into,84,1458,demod,1550,flip.1] 1^ (0 v c(0 v 1))=c(0 v 1). given clause #148: (wt=13) 2405 [para_into,84,45,demod,14] c(0 v x)=1^ (0 v c(x v x)). given clause #149: (wt=17) 113 [para_into,16,21] x v (y v (1 v (z v 0)))=y v (z v (x v 1)). given clause #150: (wt=9) 3027 [para_into,2405,11,demod,14,169,28,1163,1161,flip.1] 1^ (0 v (0^0))=0. given clause #151: (wt=11) 3107 [para_from,2405,714,demod,2216] 0 v (1^ ((1 v 1)^1))=1. given clause #152: (wt=12) 3185 [para_from,3107,84,demod,14,14,flip.1] 1^ (0 v c((1 v 1)^1))=0. given clause #153: (wt=23) 114 [para_into,16,16] x v (y v (z v (u v (v v w))))=y v (v v (x v (z v (u v w)))). given clause #154: (wt=13) 2411 [copy,2405,flip.1] 1^ (0 v c(x v x))=c(0 v x). given clause #155: (wt=13) 2619 [para_into,104,45,demod,14] c(x v 0)= (0 v c(x v x))^1. given clause #156: (wt=11) 3258 [para_into,2619,27,demod,169,28,1163,1161,flip.1] (0 v (x^x))^1=x^1. given clause #157: (wt=23) 115 [para_into,16,15] x v (y v (z v (u v (v v w))))=y v (u v (x v (v v (z v w)))). given clause #158: (wt=13) 2628 [copy,2619,flip.1] (0 v c(x v x))^1=c(x v 0). given clause #159: (wt=13) 2996 [para_into,2405,1138,demod,14,2222,flip.1] 1^ (0 v ((0 v 0)^ (0 v 0)))=0. given clause #160: (wt=13) 3012 [para_into,2405,64,demod,3009,12] c(x v (y v 1))=c(y v (x v 1)). given clause #161: (wt=19) 117 [para_into,16,16] x v (y v (z v (u v v)))=u v (y v (x v (z v v))). given clause #162: (wt=13) 3105 [para_from,2405,1284,demod,2216] (1 v (1^ ((1 v 1)^1)))^1=1. given clause #163: (wt=14) 143 [para_into,19,27] (c(x) v 0) v (y v (x^1))=y v 1. given clause #164: (wt=14) 145 [para_into,19,23] (0 v c(x)) v (y v (1^x))=y v 1. given clause #165: (wt=19) 118 [para_into,16,15] x v (y v (z v (u v v)))=z v (u v (x v (y v v))). given clause #166: (wt=14) 157 [para_into,88,27] (0 v (x^1))^ (1^ (c(x) v 0))=0. given clause #167: (wt=14) 159 [para_into,88,23] (0 v (1^x))^ (1^ (0 v c(x)))=0. given clause #168: (wt=14) 194 [para_into,90,27] (0 v (x^1)) v (1^ (c(x) v 0))=1. given clause #169: (wt=15) 119 [para_into,16,4] x v (y v (z v u))=x v (z v (y v u)). given clause #170: (wt=14) 221 [para_into,29,45,demod,14] c(c(x) v y)=x^ (0 v c(y v y)). given clause #171: (wt=11) 3736 [para_into,221,11,demod,14,169,28,1163,1161,flip.1] x^ (0 v (c(x)^c(x)))=0. given clause #172: (wt=14) 227 [copy,221,flip.1] x^ (0 v c(y v y))=c(c(x) v y). given clause #173: (wt=17) 120 [copy,112,flip.1] x v (1 v (y v (z v 0)))=y v (x v (z v 1)). given clause #174: (wt=11) 3870 [para_into,227,9,demod,169,1151,12,flip.1] c((1^c(x v x)) v x)=0. given clause #175: (wt=11) 3880 [back_demod,3021,demod,3867,2384] c(1 v (0 v 0))=c(0 v 1). given clause #176: (wt=12) 3996 [para_from,3870,31] ((1^c(x v x)) v x)^0=0. given clause #177: (wt=17) 121 [copy,113,flip.1] x v (y v (z v 1))=z v (x v (1 v (y v 0))). given clause #178: (wt=12) 4021 [para_from,3870,11] ((1^c(x v x)) v x) v 0=1. given clause #179: (wt=10) 4229 [para_from,4021,2135,demod,4226,1459,flip.1] (1^c(x v x)) v x=1. given clause #180: (wt=11) 4377 [para_from,4229,19,demod,169,28,1163,1161,flip.1] (1^ (x^x)) v 1=x v 1. given clause #181: (wt=23) 122 [copy,114,flip.1] x v (y v (z v (u v (v v w))))=z v (x v (u v (v v (y v w)))). given clause #182: (wt=12) 4051 [para_from,3880,31] (1 v (0 v 0))^c(0 v 1)=0. given clause #183: (wt=12) 4069 [para_from,3880,11] (1 v (0 v 0)) v c(0 v 1)=1. given clause #184: (wt=12) 4287 [para_into,4229,21] 1 v ((1^c(1 v 1)) v 0)=1. given clause #185: (wt=23) 123 [copy,115,flip.1] x v (y v (z v (u v (v v w))))=z v (x v (v v (y v (u v w)))). given clause #186: (wt=13) 4065 [para_from,3880,27,demod,28,flip.1] (1 v (0 v 0))^1= (0 v 1)^1. given clause #187: (wt=13) 4430 [para_into,4377,21] 1 v ((1^ (x^x)) v 0)=x v 1. given clause #188: (wt=14) 248 [para_into,108,27] ((x^1) v 0)^ ((c(x) v 0)^1)=0. given clause #189: (wt=19) 125 [copy,117,flip.1] x v (y v (z v (u v v)))=z v (y v (u v (x v v))). given clause #190: (wt=14) 256 [para_into,110,27] ((x^1) v 0) v ((c(x) v 0)^1)=1. given clause #191: (wt=14) 260 [para_into,110,49,demod,169,18,14] (((0 v c(1 v 1))^0) v 0) v 1=1. given clause #192: (wt=14) 315 [para_from,196,4] x v 1= (0 v c(y v y)) v (x v y). given clause #193: (wt=19) 126 [para_from,16,45] 1^ (x v (y v ((x v (y v z)) v z)))=x v (y v z). given clause #194: (wt=14) 319 [copy,315,flip.1] (0 v c(x v x)) v (y v x)=y v 1. given clause #195: (wt=14) 430 [para_into,43,45,demod,14] (x v y)^ (x v (0 v c(y v y)))=x. given clause #196: (wt=11) 5012 [para_into,430,11,demod,169,28,1163,1161] 1^ (x v (0 v (x^x)))=x. given clause #197: (wt=19) 128 [para_from,16,15] x v (y v (z v (u v v)))=y v (x v (u v (z v v))). given clause #198: (wt=11) 5048 [para_into,5012,4] 1^ (0 v (x v (x^x)))=x. given clause #199: (wt=14) 507 [para_into,53,27] (x v (y^1))^ (c(y) v (x v 0))=x. given clause #200: (wt=14) 559 [para_from,372,9] (1 v c((0 v 0) v 0))^ (0 v 1)=1. given clause #201: (wt=23) 129 [para_from,16,15] x v (y v (z v (u v (v v w))))=v v (x v (y v (z v (u v w)))). given clause #202: (wt=14) 592 [para_into,55,196,demod,197] 1^ ((0 v c(x v x)) v (1 v x))=1. given clause #203: (wt=14) 665 [para_into,452,21] (x v (y^x))^ (1 v (c(y) v 0))=x. given clause #204: (wt=14) 731 [para_from,714,4,flip.1] 0 v (x v c(0 v (0 v 0)))=x v 1. given clause #205: (wt=18) 130 [para_from,16,9] (x v c(y v (z v u)))^ (y v (z v (x v u)))=x. given clause #206: (wt=14) 735 [para_from,716,90] (0 v c(0 v (0 v (0 v 0)))) v 0=1. given clause #207: (wt=12) 5400 [para_from,735,2135,demod,5395,1459,flip.1] 0 v c(0 v (0 v (0 v 0)))=1. given clause #208: (wt=13) 5404 [para_from,5400,319,demod,169,28,1163,1161,305] (0 v (0 v (0 v 0))) v 1=0 v 1. given clause #209: (wt=23) 132 [copy,129,flip.1] x v (y v (z v (u v (v v w))))=y v (z v (u v (v v (x v w)))). given clause #210: (wt=13) 5406 [para_from,5400,130] 1^ (0 v (0 v (0 v (0 v 0))))=0. given clause #211: (wt=14) 1095 [back_demod,484,demod,1037] (0 v c(0 v 1)) v (x v 1)=x v 1. given clause #212: (wt=14) 1106 [back_demod,464,demod,1037] (x v 1)^ (x v (0 v c(0 v 1)))=x. given clause #213: (wt=16) 135 [para_into,51,27] ((c(x) v 0) v c(x^1))^1=c(x) v 0. given clause #214: (wt=13) 5587 [para_into,1106,319,demod,169,28,1163,1161,305,1043,169,28,1163,1161,flip.1] 0 v ((0 v 1)^ (0 v 1))=0 v 1. given clause #215: (wt=14) 1116 [back_demod,370,demod,1037] (0 v c(x v (0 v 1)))^ (x v 1)=0. given clause #216: (wt=14) 1120 [back_demod,332,demod,1037] (c(x) v (0 v 1))^ (x^ (0 v 0))=0. given clause #217: (wt=16) 137 [para_into,51,23] ((0 v c(x)) v c(1^x))^1=0 v c(x). given clause #218: (wt=14) 1122 [back_demod,326,demod,1037] ((0 v 1) v c(x))^ ((0 v 0)^x)=0. given clause #219: (wt=14) 1124 [back_demod,276,demod,1037] (c(x) v (0 v 1)) v (x^ (0 v 0))=1. given clause #220: (wt=14) 1126 [back_demod,270,demod,1037] ((0 v 1) v c(x)) v ((0 v 0)^x)=1. given clause #221: (wt=18) 139 [para_into,51,6] ((c(x) v c(y)) v c(x^y))^1=c(x) v c(y). given clause #222: (wt=14) 1144 [back_demod,133,demod,1037] ((0 v 0) v c(0 v 1))^1=0 v 0. given clause #223: (wt=14) 1162 [back_demod,219,demod,1105] c(c(x) v 1)=x^ (0 v c(0 v 1)). given clause #224: (wt=14) 1479 [para_from,1189,53] (0 v c(0 v (x v 1)))^ (x v 1)=0. given clause #225: (wt=15) 147 [para_into,19,6] (c(x) v c(y)) v (z v (x^y))=z v 1. given clause #226: (wt=14) 1494 [para_from,1195,53] (1 v c((0 v 0) v (0 v 0)))^1=1. given clause #227: (wt=14) 1623 [para_into,1193,21] c((1 v (0 v 0)) v 0)= (0 v 0)^1. given clause #228: (wt=14) 1974 [para_from,725,452,demod,18,169,1151,12] 1^ ((1^c(0 v (0 v 0))) v 1)=1. given clause #229: (wt=18) 149 [para_from,19,15,flip.1] x v (y v (z v (u v c(x))))=y v (z v (u v 1)). given clause #230: (wt=14) 1976 [para_from,725,110,demod,169,1151,12] ((1^c(0 v (0 v 0))) v 0) v 0=1. given clause #231: (wt=12) 6205 [para_from,1976,55,demod,1975,flip.1] (1^c(0 v (0 v 0))) v 0=1. given clause #232: (wt=10) 6225 [para_from,6205,2135,demod,6210,1459,flip.1] 1^c(0 v (0 v 0))=1. given clause #233: (wt=15) 161 [para_into,88,6] (0 v (x^y))^ (1^ (c(x) v c(y)))=0. given clause #234: (wt=10) 6319 [para_into,161,45] (0 v (x^x))^c(x)=0. given clause #235: (wt=11) 6227 [para_into,6225,2405,demod,2216] 1^ (1^ ((1 v 1)^1))=1. given clause #236: (wt=13) 6239 [para_from,6225,90] (0 v c(c(0 v (0 v 0)))) v 1=1. given clause #237: (wt=17) 168 [para_into,25,41] c(x v c(y))= (c(x v 0) v c(x v 1))^y. given clause #238: (wt=10) 6434 [back_demod,4261,demod,6423] (1^ (x^x)) v c(x)=1. given clause #239: (wt=10) 6436 [back_demod,3770,demod,6423] (0 v (x^x)) v c(x)=1. given clause #240: (wt=11) 6422 [para_into,168,221,demod,169,28,1163,1161,28,1163,1161] x^ (0 v (y^y))=x^y. given clause #241: (wt=20) 180 [para_into,25,6] c((x^y) v (z^u))= (c(x) v c(y))^ (c(z) v c(u)). given clause #242: (wt=10) 6582 [para_into,6422,9,flip.1] (0 v c(x^x))^x=0. given clause #243: (wt=14) 2107 [para_into,76,1195] (1 v c(0 v ((0 v 0) v 0)))^1=1. given clause #244: (wt=14) 2535 [para_into,86,4] (x v (1^y))^ (0 v (x v c(y)))=x. given clause #245: (wt=21) 182 [copy,166,flip.1,demod,169,18,14,169,18,14] (((0 v c(1 v 1))^0) v 0)^x= (0 v c(1 v 1))^x. given clause #246: (wt=14) 2869 [para_from,2235,31] (0 v (c(x) v 1))^ (x^ (0 v 0))=0. given clause #247: (wt=14) 2885 [para_from,2235,11] (0 v (c(x) v 1)) v (x^ (0 v 0))=1. given clause #248: (wt=14) 3103 [para_from,2405,725,demod,2216] (0 v c(1^ ((1 v 1)^1)))^1=0. given clause #249: (wt=20) 184 [copy,167,flip.1,demod,169] (0 v c(x v x))^y= (c(x v 0) v c(x v 1))^y. given clause #250: (wt=11) 6799 [para_into,184,221,demod,169,28,1163,1161,6423,28,1163,1161] (0 v (x^x))^y=x^y. given clause #251: (wt=8) 6831 [para_into,6799,452,flip.1] 0^ (c(0) v 1)=0. given clause #252: (wt=10) 6829 [para_into,6799,665,flip.1] 0^ (1 v (c(0) v 0))=0. given clause #253: (wt=20) 185 [back_demod,167,demod,169] (c(x v 0) v c(x v 1))^y= (0 v c(x v x))^y. given clause #254: (wt=11) 6812 [back_demod,5967,demod,6800] (0 v 0)^ ((0 v 1) v 1)=0. given clause #255: (wt=11) 6835 [para_into,6799,43,flip.1] x^ (0 v (c(x) v c(x)))=0. given clause #256: (wt=11) 6951 [para_into,6835,4] x^ (c(x) v (0 v c(x)))=0. given clause #257: (wt=19) 186 [back_demod,151,demod,169] (x v ((c(y v 0) v c(y v 1))^x))^ (y v 1)=x. given clause #258: (wt=13) 6903 [para_into,6812,21] (0 v 0)^ (1 v ((0 v 1) v 0))=0. given clause #259: (wt=14) 3135 [para_from,2405,31] (0 v x)^ (1^ (0 v c(x v x)))=0. given clause #260: (wt=14) 3147 [para_from,2405,11] (0 v x) v (1^ (0 v c(x v x)))=1. given clause #261: (wt=18) 198 [para_from,90,15,flip.1] (0 v c(x)) v (y v (z v (1^x)))=y v (z v 1). given clause #262: (wt=14) 3183 [para_from,3107,86] 1^ (0 v (0 v c((1 v 1)^1)))=0. given clause #263: (wt=14) 3288 [para_from,2619,31] (x v 0)^ ((0 v c(x v x))^1)=0. given clause #264: (wt=14) 3300 [para_from,2619,11] (x v 0) v ((0 v c(x v x))^1)=1. given clause #265: (wt=22) 218 [para_into,29,51,demod,169,14] c(c(x) v y)=x^ (((c(y v 0) v c(y v 1))^c(y)) v 0). given clause #266: (wt=12) 7244 [para_into,218,2619,demod,169,28,1163,1161,6800,1151,12,flip.1] x^ ((1^c(0)) v 0)=x^1. given clause #267: (wt=11) 7257 [para_into,7244,338,demod,2623,flip.1] c(((1^c(0)) v 0) v 0)=0. given clause #268: (wt=12) 7273 [para_from,7244,4430,demod,7272,flip.1] ((1^c(0)) v 0) v 1=1 v 1. given clause #269: (wt=17) 222 [para_into,29,41] c(c(x) v y)=x^ (c(y v 0) v c(y v 1)). given clause #270: (wt=12) 7346 [para_from,7257,31] (((1^c(0)) v 0) v 0)^0=0. given clause #271: (wt=12) 7379 [para_from,7257,11] (((1^c(0)) v 0) v 0) v 0=1. given clause #272: (wt=8) 7553 [back_demod,7425,demod,7552,46,flip.1] (1^c(0)) v 0=1. given clause #273: (wt=24) 223 [para_into,29,9,demod,169] c(c(x) v y)=x^ (((c(y v 0) v c(y v 1))^z) v c(y v z)). given clause #274: (wt=6) 7587 [para_from,7553,2135,demod,7556,1459,flip.1] 1^c(0)=1. given clause #275: (wt=9) 7615 [para_from,7587,90] (0 v c(c(0))) v 1=1. given clause #276: (wt=11) 7603 [para_from,7587,452,demod,14] (c(0) v 1)^ (0 v 1)=c(0). given clause #277: (wt=22) 224 [copy,218,flip.1] x^ (((c(y v 0) v c(y v 1))^c(y)) v 0)=c(c(x) v y). given clause #278: (wt=11) 7621 [para_into,7615,21] 1 v ((0 v c(c(0))) v 0)=1. given clause #279: (wt=13) 7247 [para_into,218,168,demod,28,1163,1161,28,1163,1161,flip.1] x^ ((y^c(c(y))) v 0)=x^y. given clause #280: (wt=13) 7601 [para_from,7587,665,demod,14] (c(0) v 1)^ (1 v (0 v 0))=c(0). given clause #281: (wt=17) 228 [copy,222,flip.1] x^ (c(y v 0) v c(y v 1))=c(c(x) v y). given clause #282: (wt=13) 7605 [para_from,7587,2535] (x v 1)^ (0 v (x v c(c(0))))=x. given clause #283: (wt=10) 7850 [para_into,7605,6436,demod,305,7604,flip.1] 0 v (c(0)^c(0))=c(0). given clause #284: (wt=10) 7852 [para_into,7605,6434,demod,4378,7604,flip.1] 1^ (c(0)^c(0))=c(0). given clause #285: (wt=24) 229 [copy,223,flip.1] x^ (((c(y v 0) v c(y v 1))^z) v c(y v z))=c(c(x) v y). given clause #286: (wt=13) 7607 [para_from,7587,86] (x v 1)^ (x v (0 v c(c(0))))=x. given clause #287: (wt=13) 7611 [para_from,7587,145] (0 v c(c(0))) v (x v 1)=x v 1. given clause #288: (wt=13) 7617 [para_from,7587,159] (0 v 1)^ (1^ (0 v c(c(0))))=0. given clause #289: (wt=20) 230 [para_from,29,9] (x v (y^ (c(z) v c(u))))^ (x v (c(y) v (z^u)))=x. given clause #290: (wt=13) 7664 [para_into,7603,21] (1 v (c(0) v 0))^ (0 v 1)=c(0). given clause #291: (wt=13) 7912 [para_from,7852,90] (0 v c(c(0)^c(0))) v c(0)=1. given clause #292: (wt=13) 7956 [para_into,229,27,demod,28,1163,1161,169,28,1163,1161] x^ ((y^0) v (y^1))=x^y. given clause #293: (wt=24) 232 [para_from,29,51] ((c(x) v (y^z)) v c(x^ (c(y) v c(z))))^1=c(x) v (y^z). given clause #294: (wt=14) 3387 [para_from,3012,31] (x v (y v 1))^c(y v (x v 1))=0. given clause #295: (wt=14) 3401 [para_from,3012,11] (x v (y v 1)) v c(y v (x v 1))=1. given clause #296: (wt=14) 3512 [para_into,145,3107] (0 v c((1 v 1)^1)) v 1=0 v 1. given clause #297: (wt=16) 234 [para_from,29,31] (c(x) v (y^z))^ (x^ (c(y) v c(z)))=0. given clause #298: (wt=13) 8446 [para_into,234,9,demod,169,28,1163,1161] ((x^c(y)) v (x^y))^c(x)=0. given clause #299: (wt=11) 8504 [para_into,8446,7587,demod,14] ((1^c(c(0))) v 1)^0=0. given clause #300: (wt=12) 8476 [para_into,8446,13] ((x^0) v (x^1))^c(x)=0. given clause #301: (wt=20) 236 [para_from,29,90] (0 v (x^ (c(y) v c(z)))) v (1^ (c(x) v (y^z)))=1. given clause #302: (wt=12) 8546 [para_into,8446,2411,demod,169,1151,12,46,14] ((1^x) v c(0 v x))^0=0. given clause #303: (wt=12) 8558 [para_into,8446,1168,demod,3881,14] ((1^c(0 v 1)) v 1)^0=0. given clause #304: (wt=12) 8604 [para_into,8446,31] ((x^c(c(x))) v 0)^c(x)=0. given clause #305: (wt=20) 238 [para_from,29,88] (0 v (x^ (c(y) v c(z))))^ (1^ (c(x) v (y^z)))=0. given clause #306: (wt=12) 8626 [para_into,8446,13] ((1^c(x)) v (1^x))^0=0. given clause #307: (wt=12) 8750 [para_into,8546,45] (x v c(0 v (x v x)))^0=0. given clause #308: (wt=12) 8990 [para_into,8750,4] (x v c(x v (0 v x)))^0=0. given clause #309: (wt=20) 240 [para_from,29,19] (c(x) v (y^z)) v (u v (x^ (c(y) v c(z))))=u v 1. given clause #310: (wt=13) 8630 [para_into,8504,21] (1 v ((1^c(c(0))) v 0))^0=0. given clause #311: (wt=14) 4391 [para_from,4229,55,demod,4230] 1^ ((1^c(x v x)) v (1 v x))=1. given clause #312: (wt=14) 4401 [para_from,4229,4] x v 1= (1^c(y v y)) v (x v y). given clause #313: (wt=16) 242 [para_from,29,11] (c(x) v (y^z)) v (x^ (c(y) v c(z)))=1. given clause #314: (wt=13) 9519 [para_into,242,9,demod,169,28,1163,1161] ((x^c(y)) v (x^y)) v c(x)=1. given clause #315: (wt=11) 9591 [para_into,9519,7587,demod,14] ((1^c(c(0))) v 1) v 0=1. given clause #316: (wt=9) 9771 [para_from,9591,2135,demod,9746,1459,flip.1] (1^c(c(0))) v 1=1. given clause #317: (wt=20) 246 [para_into,108,29] ((x^ (c(y) v c(z))) v 0)^ ((c(x) v (y^z))^1)=0. given clause #318: (wt=11) 9777 [para_into,9771,21] 1 v ((1^c(c(0))) v 0)=1. given clause #319: (wt=12) 9549 [para_into,9519,13] ((x^0) v (x^1)) v c(x)=1. given clause #320: (wt=12) 9633 [para_into,9519,2411,demod,169,1151,12,46,14] ((1^x) v c(0 v x)) v 0=1. given clause #321: (wt=18) 250 [para_into,108,51,demod,169] (((c(x v 0) v c(x v 1))^c(x)) v 0)^x=0. given clause #322: (wt=10) 10150 [para_from,9633,2135,demod,10131,1459,flip.1] (1^x) v c(0 v x)=1. given clause #323: (wt=10) 10220 [para_into,10150,45] x v c(0 v (x v x))=1. given clause #324: (wt=10) 10298 [para_into,10150,168,demod,1151,12] (1^c(x)) v (1^x)=1. given clause #325: (wt=20) 254 [para_into,110,29] ((x^ (c(y) v c(z))) v 0) v ((c(x) v (y^z))^1)=1. given clause #326: (wt=10) 10436 [para_into,10220,4] x v c(x v (0 v x))=1. given clause #327: (wt=11) 10300 [para_from,10150,319,demod,169,28,1163,1161,305,flip.1] (1^x) v 1= (0 v x) v 1. given clause #328: (wt=11) 10440 [para_from,10220,319,demod,169,28,1163,1161,305] (0 v (x v x)) v 1=x v 1. given clause #329: (wt=18) 258 [para_into,110,51,demod,169] (((c(x v 0) v c(x v 1))^c(x)) v 0) v x=1. given clause #330: (wt=7) 10903 [para_from,10440,126,demod,10444,flip.1] 0 v (1 v 1)=1. given clause #331: (wt=7) 11097 [para_from,258,1286,demod,10904,5845,367,5849,1151,11096,flip.1] 1 v (0 v 1)=1. given clause #332: (wt=7) 11130 [para_from,10903,1203,demod,367,flip.1] 1 v 1=0 v 1. given clause #333: (wt=18) 262 [para_from,110,15,flip.1] (c(x) v 0) v (y v (z v (x^1)))=y v (z v 1). given clause #334: (wt=9) 11124 [para_into,10903,116] 1 v (1 v (0 v 0))=1. given clause #335: (wt=9) 11172 [back_demod,11049,demod,11131] ((0 v 1)^1) v 1=1. given clause #336: (wt=10) 11160 [para_from,10903,53] (1 v c(0 v 1))^1=1. given clause #337: (wt=22) 264 [para_into,163,16] (0 v c(x v (y v ((x v (y v z)) v z))))^ (x v (y v z))=0. given clause #338: (wt=11) 10443 [para_from,10220,130] 1^ (0 v (x v (x v x)))=x. given clause #339: (wt=11) 10445 [para_from,10220,76] 1^ (x v (x v (0 v x)))=x. given clause #340: (wt=4) 12355 [back_demod,11458,demod,12354,12354,12140,1037,12140,12140,1037,12140,18,1037,12140] c(0)=1. given clause #341: (wt=22) 266 [para_into,163,15] (0 v c(x v ((y v (x v z)) v (y v z))))^ (y v (x v z))=0. given clause #342: (wt=5) 12139 [back_demod,5883,demod,12052,5612] 0 v 1=1. given clause #343: (wt=5) 12353 [back_demod,11460,demod,12140,1037,12140,12140,1037,12140,18,1037,12140,12255] 0 v 0=0. given clause #344: (wt=5) 12375 [back_demod,11428,demod,12140,1037,12140,1037,12140,14,12354,12354,12140,1037,12140,1037,12140,14,12354] 0^1=0. given clause #345: (wt=16) 268 [para_into,163,4] (0 v c(x v ((x v y) v y)))^ (x v y)=0. given clause #346: (wt=5) 12405 [back_demod,11130,demod,12140] 1 v 1=1. given clause #347: (wt=5) 12840 [back_demod,1036,demod,12140] 1^1=1. given clause #348: (wt=5) 13027 [back_demod,12075,demod,12354,12354] 0^0=0. given clause #349: (wt=21) 272 [para_into,33,29] ((x^ (c(y) v c(z))) v c(u)) v ((c(x) v (y^z))^u)=1. given clause #350: (wt=8) 13316 [back_demod,10212,demod,13257,105,169,28,12827,12829,42,52] c(0 v x) v x=1. given clause #351: (wt=8) 13318 [back_demod,10186,demod,13257,105,52] (1^x) v c(x)=1. given clause #352: (wt=8) 14031 [para_into,13318,45] x v c(x v x)=1. given clause #353: (wt=15) 274 [para_into,33,27] ((x^1) v c(y)) v ((c(x) v 0)^y)=1. given clause #354: (wt=7) 14185 [para_from,14031,2535,demod,46,12140] (x v x)^1=x. given clause #355: (wt=8) 14109 [para_into,14031,223,demod,28,12827,12829,7596] c(x) v (x^x)=1. given clause #356: (wt=9) 12183 [back_demod,11774,demod,12140] 1 v (x v 1)=x v 1. given clause #357: (wt=21) 278 [para_into,33,29] (c(x) v (y^ (c(z) v c(u)))) v (x^ (c(y) v (z^u)))=1. given clause #358: (wt=9) 12252 [back_demod,11598,demod,12140,1037,12140,1037,12140] 0 v (x v 1)=x v 1. given clause #359: (wt=9) 12373 [back_demod,11432,demod,12140,1037,12140,1037,12140,14,12354] (x v 1)^ (x v 0)=x. given clause #360: (wt=9) 12377 [back_demod,11386,demod,12140,14,12356,12140,1037,12140,18] (x v (1^x))^1=x. given clause #361: (wt=15) 280 [para_into,33,27] (c(x) v (y^1)) v (x^ (c(y) v 0))=1. given clause #362: (wt=9) 12764 [back_demod,5248,demod,12354,12140,18,12406] (x v (0^x))^1=x. given clause #363: (wt=9) 12826 [back_demod,1162,demod,12140,14,12354] c(c(x) v 1)=x^0. given clause #364: (wt=9) 13256 [para_from,12353,4,flip.1] 0 v (x v 0)=x v 0. given clause #365: (wt=20) 284 [para_into,33,9,demod,169] (((c(x v 0) v c(x v 1))^y) v c(x v y)) v x=1. given clause #366: (wt=9) 13314 [back_demod,10688,demod,13257,11101,flip.1] (0 v x) v 1=x v 1. given clause #367: (wt=9) 13448 [back_demod,10690,demod,13315,13315,13315] (x^x) v 1=x v 1. given clause #368: (wt=9) 13452 [back_demod,10440,demod,13315] (x v x) v 1=x v 1. given clause #369: (wt=19) 286 [para_from,33,15,flip.1] (c(x) v c(y)) v (z v (u v (x^y)))=z v (u v 1). given clause #370: (wt=9) 13460 [back_demod,10300,demod,13315] (1^x) v 1=x v 1. given clause #371: (wt=9) 14146 [para_from,14031,53] 1^ (x v (x v x))=x. given clause #372: (wt=9) 15135 [back_demod,14214,demod,15048] x^ (c(x) v c(x))=0. given clause #373: (wt=22) 288 [para_into,196,16] (0 v c(x v (y v ((x v (y v z)) v z)))) v (x v (y v z))=1. given clause #374: (wt=9) 15354 [para_from,286,74,demod,34,15158,34] 1^ (x v 1)=x v 1. given clause #375: (wt=9) 15604 [para_from,15354,665,demod,15158,14,12354,18] (x v 1)^1=x v 1. given clause #376: (wt=10) 12387 [back_demod,11298,demod,12140,14,12354,12354,12354,12354,12384] (c(x) v 1)^ (x^0)=0. given clause #377: (wt=22) 290 [para_into,196,15] (0 v c(x v ((y v (x v z)) v (y v z)))) v (y v (x v z))=1. given clause #378: (wt=10) 12399 [back_demod,11258,demod,12140,14,12354,12354,12354,12354,12384] (c(x) v 1) v (x^0)=1. given clause #379: (wt=10) 12832 [back_demod,1126,demod,12140,12354] (1 v c(x)) v (0^x)=1. given clause #380: (wt=10) 12834 [back_demod,1122,demod,12140,12354] (1 v c(x))^ (0^x)=0. given clause #381: (wt=16) 292 [para_into,196,4] (0 v c(x v ((x v y) v y))) v (x v y)=1. given clause #382: (wt=10) 13630 [para_into,13316,40,demod,12354,18] c(x v 1) v (x v 1)=1. given clause #383: (wt=10) 13859 [para_from,13316,124,demod,12406,13257,flip.1] x v (c(x v 0) v 1)=1. given clause #384: (wt=10) 13861 [para_from,13316,60,demod,12406,13257,flip.1] c(x v 0) v (x v 1)=1. given clause #385: (wt=22) 296 [para_into,196,16] x v (y v ((0 v c((x v (y v z)) v (x v (y v z)))) v z))=1. given clause #386: (wt=8) 16209 [para_into,13861,13448,demod,105,14186] c(x) v (x v 1)=1. given clause #387: (wt=8) 16363 [para_into,16209,4] x v (c(x) v 1)=1. given clause #388: (wt=9) 16416 [para_from,16209,53,demod,12827] (x v (x^0))^1=x. given clause #389: (wt=22) 298 [para_into,196,15] x v ((0 v c((y v (x v z)) v (y v (x v z)))) v (y v z))=1. given clause #390: (wt=9) 16500 [para_from,16363,319,demod,15158,12827,13315] (x^0) v 1=x v 1. given clause #391: (wt=9) 16526 [back_demod,16121,demod,16501] (x v 0) v 1=x v 1. given clause #392: (wt=10) 13953 [para_from,13316,37] 1^ ((0 v c(x))^x)=0. given clause #393: (wt=16) 300 [para_into,196,4] x v ((0 v c((x v y) v (x v y))) v y)=1. given clause #394: (wt=10) 13955 [para_from,13316,33] 1 v ((0 v c(x))^x)=1. given clause #395: (wt=10) 14332 [para_from,14185,110] (c(x v x) v 0) v x=1. given clause #396: (wt=10) 14334 [para_from,14185,108] (c(x v x) v 0)^x=0. given clause #397: (wt=20) 306 [para_from,196,16] x v 1= (0 v c((y v z) v (y v z))) v (y v (x v z)). given clause #398: (wt=10) 14719 [para_from,13256,13316] c(x v 0) v (x v 0)=1. given clause #399: (wt=10) 15076 [para_from,13448,57,demod,105,14186] (1 v c(x))^ (x v 1)=1. given clause #400: (wt=10) 15434 [para_from,14146,13318] x v c(x v (x v x))=1. given clause #401: (wt=20) 307 [para_from,196,15,flip.1] x v (y v ((0 v c((x v z) v (x v z))) v z))=y v 1. given clause #402: (wt=5) 17917 [back_demod,15842,demod,17916,12406,17905,17907,flip.1] x v 1=1. given clause #403: (wt=5) 17921 [back_demod,3877,demod,17916,17918,14,17916,17918,17918,14,12354,flip.1] x^0=0. given clause #404: (wt=5) 18405 [back_demod,17643,demod,17918,14,17980] 0^x=0. given clause #405: (wt=18) 311 [para_from,196,9] ((0 v c(x v x)) v c(x))^1=0 v c(x v x). given clause #406: (wt=6) 18702 [back_demod,13177,demod,17918,14,18406,flip.1] c(1 v x)=0. given clause #407: (wt=5) 19449 [para_from,18702,51,demod,12356,17918,12841,flip.1] 1 v x=1. given clause #408: (wt=7) 17919 [back_demod,5028,demod,17916,17918,17916,17918,17918,14,12354] 1^ (x v 0)=x. given clause #409: (wt=15) 313 [para_from,196,9,demod,169,28,220,226,169,28,220,226] 1^ ((0 v (x^x)) v x)=0 v (x^x). given clause #410: (wt=7) 17979 [back_demod,16469,demod,17918,17918,17918,14,17918,17918] (x v 0)^1=x. given clause #411: (wt=8) 17923 [back_demod,17681,demod,17918,14147] x^ (c(x) v 0)=0. given clause #412: (wt=8) 19118 [back_demod,19,demod,17918] x v (y v c(x))=1. given clause #413: (wt=21) 328 [para_into,37,29] ((x^ (c(y) v c(z))) v c(u))^ ((c(x) v (y^z))^u)=0. given clause #414: (wt=8) 19124 [back_demod,14049,demod,17920] c(x) v (x^1)=1. given clause #415: (wt=8) 19329 [back_demod,18644,demod,19205] (0 v c(x))^x=0. given clause #416: (wt=8) 19453 [para_from,17919,13318] x v c(x v 0)=1. given clause #417: (wt=15) 330 [para_into,37,27] ((x^1) v c(y))^ ((c(x) v 0)^y)=0. given clause #418: (wt=8) 19487 [para_into,17923,27,demod,18486] (c(x) v 0)^x=0. given clause #419: (wt=8) 19545 [para_into,19124,27,demod,17980] (x^1) v c(x)=1. given clause #420: (wt=8) 19547 [para_into,19124,17979] c(x v 0) v x=1. given clause #421: (wt=21) 334 [para_into,37,29] (c(x) v (y^ (c(z) v c(u))))^ (x^ (c(y) v (z^u)))=0. given clause #422: (wt=8) 19549 [para_into,19124,14185] c(x v x) v x=1. given clause #423: (wt=8) 19949 [para_into,19549,221,demod,19111,28,19205,6423] (x^x) v c(x)=1. given clause #424: (wt=9) 17989 [back_demod,12896,demod,17922,17918,17918,14,17920] c(0 v x)=c(x v 0). given clause #425: (wt=15) 336 [para_into,37,27] (c(x) v (y^1))^ (x^ (c(y) v 0))=0. given clause #426: (wt=7) 20575 [para_from,17989,27,demod,28,17980,flip.1] (0 v x)^1=x. ----> UNIT CONFLICT at 8.75 sec ----> 21863 [binary,21861,2] $Ans(CC). Length of proof is 234. Level of proof is 47. ---------------- PROOF ---------------- 2 [] c(c(A))!=A|$Ans(CC). 4 [] x v (y v z)=y v (x v z). 5 [] x^y=c(c(x) v c(y)). 6 [copy,5,flip.1] c(c(x) v c(y))=x^y. 9 [] (x v c(y))^ (x v y)=x. 12,11 [] x v c(x)=1. 14,13 [] c(1)=0. 15 [para_into,4,4] x v (y v (z v u))=z v (x v (y v u)). 16 [copy,15,flip.1] x v (y v (z v u))=y v (z v (x v u)). 18,17 [para_into,11,13] 1 v 0=1. 19 [para_from,11,4,flip.1] x v (y v c(x))=y v 1. 21 [para_from,17,4] x v 1=1 v (x v 0). 22 [copy,21,flip.1] 1 v (x v 0)=x v 1. 23 [para_into,6,13] c(0 v c(x))=1^x. 25 [para_into,6,6] c((x^y) v c(z))= (c(x) v c(y))^z. 28,27 [para_into,6,13] c(c(x) v 0)=x^1. 29 [para_into,6,6] c(c(x) v (y^z))=x^ (c(y) v c(z)). 31 [para_into,6,11,demod,14,flip.1] x^c(x)=0. 34,33 [para_from,6,11] (c(x) v c(y)) v (x^y)=1. 35 [para_into,31,13] 1^0=0. 39 [para_from,21,4] x v (1 v (y v 0))=y v (x v 1). 40 [copy,39,flip.1] x v (y v 1)=y v (1 v (x v 0)). 42,41 [para_into,9,13] (x v 0)^ (x v 1)=x. 43 [para_into,9,6] (x v (y^z))^ (x v (c(y) v c(z)))=x. 46,45 [para_into,9,11] 1^ (x v x)=x. 47 [para_into,9,21,demod,14] (x v 0)^ (1 v (x v 0))=x. 49 [para_into,9,17] (1 v c(0))^1=1. 52,51 [para_into,9,11] (x v c(c(x)))^1=x. 53 [para_into,9,4] (x v c(y v z))^ (y v (x v z))=x. 56,55 [para_into,45,4] 1^ (x v ((x v y) v y))=x v y. 59 [para_from,22,4] x v (y v 1)=1 v (x v (y v 0)). 60 [copy,59,flip.1] 1 v (x v (y v 0))=x v (y v 1). 62 [para_into,15,21] x v (y v (1 v (z v 0)))=z v (x v (y v 1)). 64 [para_into,15,11,flip.1] x v (y v (z v c(x)))=y v (z v 1). 70 [copy,62,flip.1] x v (y v (z v 1))=y v (z v (1 v (x v 0))). 74 [para_from,15,45] 1^ (x v ((y v (x v z)) v (y v z)))=y v (x v z). 76 [para_from,15,9] (x v c(y v (z v u)))^ (z v (x v (y v u)))=x. 83,82 [para_into,23,13] c(0 v 0)=1^1. 84 [para_into,23,6] c(0 v (x^y))=1^ (c(x) v c(y)). 86 [para_from,23,9] (x v (1^y))^ (x v (0 v c(y)))=x. 90 [para_from,23,11] (0 v c(x)) v (1^x)=1. 92 [para_from,82,9] (x v (1^1))^ (x v (0 v 0))=x. 96 [para_from,82,11] (0 v 0) v (1^1)=1. 105,104 [para_into,27,6] c((x^y) v 0)= (c(x) v c(y))^1. 108 [para_from,27,31] (c(x) v 0)^ (x^1)=0. 110 [para_from,27,11] (c(x) v 0) v (x^1)=1. 116 [para_into,16,22] x v (y v 1)=1 v (y v (x v 0)). 124 [copy,116,flip.1] 1 v (x v (y v 0))=y v (x v 1). 126 [para_from,16,45] 1^ (x v (y v ((x v (y v z)) v z)))=x v (y v z). 130 [para_from,16,9] (x v c(y v (z v u)))^ (y v (z v (x v u)))=x. 133 [para_into,51,82] ((0 v 0) v c(1^1))^1=0 v 0. 167 [para_into,25,45,demod,14] c(x v c(y))= (0 v c(x v x))^y. 169,168 [para_into,25,41] c(x v c(y))= (c(x v 0) v c(x v 1))^y. 171,170 [para_into,25,35,demod,169,83,14,12] ((1^1) v c(0 v 1))^x=1^x. 181,180 [para_into,25,6] c((x^y) v (z^u))= (c(x) v c(y))^ (c(z) v c(u)). 184 [copy,167,flip.1,demod,169] (0 v c(x v x))^y= (c(x v 0) v c(x v 1))^y. 190 [back_demod,6,demod,169,28] ((x^1) v c(c(x) v 1))^y=x^y. 192 [para_into,90,82,demod,46] (0 v (1^1)) v 0=1. 196 [para_into,90,45] (0 v c(x v x)) v x=1. 200 [para_from,192,41] 1^ ((0 v (1^1)) v 1)=0 v (1^1). 203,202 [para_from,192,22,flip.1] (0 v (1^1)) v 1=1 v 1. 209 [back_demod,200,demod,203,46,flip.1] 0 v (1^1)=1. 214 [para_from,209,9] (0 v c(1^1))^1=0. 216 [para_from,209,4,flip.1] 0 v (x v (1^1))=x v 1. 218 [para_into,29,51,demod,169,14] c(c(x) v y)=x^ (((c(y v 0) v c(y v 1))^c(y)) v 0). 220,219 [para_into,29,49,demod,169,18,14,14] c(c(x) v 1)=x^ (((0 v c(1 v 1))^0) v 0). 221 [para_into,29,45,demod,14] c(c(x) v y)=x^ (0 v c(y v y)). 222 [para_into,29,41] c(c(x) v y)=x^ (c(y v 0) v c(y v 1)). 224 [copy,218,flip.1] x^ (((c(y v 0) v c(y v 1))^c(y)) v 0)=c(c(x) v y). 226,225 [back_demod,190,demod,220] ((x^1) v (x^ (((0 v c(1 v 1))^0) v 0)))^y=x^y. 227 [copy,221,flip.1] x^ (0 v c(y v y))=c(c(x) v y). 242 [para_from,29,11] (c(x) v (y^z)) v (x^ (c(y) v c(z)))=1. 248 [para_into,108,27] ((x^1) v 0)^ ((c(x) v 0)^1)=0. 258 [para_into,110,51,demod,169] (((c(x v 0) v c(x v 1))^c(x)) v 0) v x=1. 282 [para_into,33,41] (c(x v 0) v c(x v 1)) v x=1. 286 [para_from,33,15,flip.1] (c(x) v c(y)) v (z v (u v (x^y)))=z v (u v 1). 290 [para_into,196,15] (0 v c(x v ((y v (x v z)) v (y v z)))) v (y v (x v z))=1. 305,304 [para_from,196,19,demod,169,28,220,226,flip.1] (0 v (x^x)) v 1=x v 1. 307 [para_from,196,15,flip.1] x v (y v ((0 v c((x v z) v (x v z))) v z))=y v 1. 315 [para_from,196,4] x v 1= (0 v c(y v y)) v (x v y). 319 [copy,315,flip.1] (0 v c(x v x)) v (y v x)=y v 1. 321,320 [para_from,214,110,demod,169,83,171] ((1^ (1^1)) v 0) v 0=1. 367,366 [para_into,216,196,demod,181,14,14,14,14,305,flip.1] (0 v 0) v 1=0 v 1. 386 [para_into,40,4] x v (y v 1)=x v (1 v (y v 0)). 420,419 [para_from,320,47,demod,321,46,flip.1] (1^ (1^1)) v 0=1. 422 [para_from,419,47,demod,420,46,flip.1] 1^ (1^1)=1. 430 [para_into,43,45,demod,14] (x v y)^ (x v (0 v c(y v y)))=x. 438 [para_into,43,209,demod,14,14] 1^ (0 v (0 v 0))=0. 452 [para_into,43,19] (x v (y^x))^ (c(y) v 1)=x. 464 [para_from,422,43,demod,14] (x v 1)^ (x v (0 v c(1^1)))=x. 466 [para_from,422,29,demod,220,14,flip.1] x^ (0 v c(1^1))=x^ (((0 v c(1 v 1))^0) v 0). 469,468 [para_from,438,90] (0 v c(0 v (0 v 0))) v 0=1. 503 [para_into,53,82] (x v (1^1))^ (0 v (x v 0))=x. 639 [para_into,452,422,demod,14] ((1^1) v 1)^ (0 v 1)=1^1. 651 [para_into,452,45,demod,14] ((x v x) v x)^ (0 v 1)=x v x. 714 [para_from,468,47,demod,469,46,flip.1] 0 v c(0 v (0 v 0))=1. 744,743 [para_into,60,196,flip.1] (0 v c((x v 0) v (x v 0))) v (x v 1)=1 v 1. 903,902 [para_into,282,82] ((1^1) v c(0 v 1)) v 0=1. 946 [para_from,282,47,demod,83,903,46,83,flip.1] (1^1) v c(0 v 1)=1. 1015 [para_into,946,21] (1^1) v c(1 v (0 v 0))=1. 1017 [para_from,946,53] 1^ (0 v ((1^1) v 1))=1^1. 1020,1019 [para_from,946,19,flip.1] (1^1) v 1= (0 v 1) v 1. 1037,1036 [back_demod,1017,demod,1020,56,flip.1] 1^1=0 v 1. 1043,1042 [back_demod,639,demod,1037,1037] ((0 v 1) v 1)^ (0 v 1)=0 v 1. 1044 [back_demod,1015,demod,1037] (0 v 1) v c(1 v (0 v 0))=1. 1092 [back_demod,503,demod,1037] (x v (0 v 1))^ (0 v (x v 0))=x. 1105,1104 [back_demod,466,demod,1037,flip.1] x^ (((0 v c(1 v 1))^0) v 0)=x^ (0 v c(0 v 1)). 1106 [back_demod,464,demod,1037] (x v 1)^ (x v (0 v c(0 v 1)))=x. 1139,1138 [back_demod,209,demod,1037] 0 v (0 v 1)=1. 1144 [back_demod,133,demod,1037] ((0 v 0) v c(0 v 1))^1=0 v 0. 1146 [back_demod,96,demod,1037] (0 v 0) v (0 v 1)=1. 1148 [back_demod,92,demod,1037] (x v (0 v 1))^ (x v (0 v 0))=x. 1151,1150 [back_demod,82,demod,1037] c(0 v 0)=0 v 1. 1161,1160 [back_demod,225,demod,1105] ((x^1) v (x^ (0 v c(0 v 1))))^y=x^y. 1163,1162 [back_demod,219,demod,1105] c(c(x) v 1)=x^ (0 v c(0 v 1)). 1164 [para_from,1036,452,demod,14] (1 v (0 v 1))^ (0 v 1)=1. 1166 [para_from,1036,29,demod,14,14] c(c(x) v (0 v 1))=x^ (0 v 0). 1181 [para_into,1138,21] 0 v (1 v (0 v 0))=1. 1190,1189 [para_from,1138,16,flip.1] 0 v (0 v (x v 1))=x v 1. 1203 [para_from,1146,16,flip.1] (0 v 0) v (0 v (x v 1))=x v 1. 1286 [para_from,1181,16,flip.1] 0 v (1 v (x v (0 v 0)))=x v 1. 1295 [para_from,1181,4,flip.1] 0 v (x v (1 v (0 v 0)))=x v 1. 1459,1458 [para_into,1164,40,demod,18] (0 v (1 v 1))^ (0 v 1)=1. 1550,1549 [para_from,1458,29,demod,1163,flip.1] x^ (c(0 v (1 v 1)) v c(0 v 1))=x^ (0 v c(0 v 1)). 1560,1559 [para_from,1044,19] (1 v (0 v 0)) v 1= (0 v 1) v 1. 1896 [para_into,651,40] (x v (1 v (((x v 1) v (x v 1)) v 0)))^ (0 v 1)= (x v 1) v (x v 1). 2005 [para_from,1042,33] (c((0 v 1) v 1) v c(0 v 1)) v (0 v 1)=1. 2135 [para_into,1092,4] (0 v (x v 1))^ (0 v (x v 0))=x. 2213 [para_into,1148,4] (0 v (x v 1))^ (x v (0 v 0))=x. 2216,2215 [para_into,1148,196,demod,744,flip.1] 0 v c((0 v 0) v (0 v 0))= (1 v 1)^1. 2235 [para_into,1166,4] c(0 v (c(x) v 1))=x^ (0 v 0). 2361,2360 [para_into,1286,282,demod,367,flip.1] (c((0 v 0) v 0) v c(0 v 1)) v 1=0 v (1 v 1). 2384,2383 [para_into,84,1458,demod,1550,flip.1] 1^ (0 v c(0 v 1))=c(0 v 1). 2405 [para_into,84,45,demod,14] c(0 v x)=1^ (0 v c(x v x)). 2411 [copy,2405,flip.1] 1^ (0 v c(x v x))=c(0 v x). 2535 [para_into,86,4] (x v (1^y))^ (0 v (x v c(y)))=x. 2733 [para_from,1559,55,demod,1560] 1^ ((1 v (0 v 0)) v (((0 v 1) v 1) v 1))= (0 v 1) v 1. 2816,2815 [para_into,2213,282,demod,367,2361,1190,367,flip.1] c((0 v 0) v 0) v c(0 v 1)= (1 v 1)^1. 3021 [para_into,2405,21] c(1 v (0 v 0))=1^ (0 v c(1 v 1)). 3107 [para_from,2405,714,demod,2216] 0 v (1^ ((1 v 1)^1))=1. 3185 [para_from,3107,84,demod,14,14,flip.1] 1^ (0 v c((1 v 1)^1))=0. 3208 [para_from,3107,4,flip.1] 0 v (x v (1^ ((1 v 1)^1)))=x v 1. 3210 [para_from,3185,452,demod,14] ((0 v c((1 v 1)^1)) v 0)^ (0 v 1)=0 v c((1 v 1)^1). 3865 [para_into,227,39] x^ (0 v c(y v ((1 v (y v 0)) v 1)))=c(c(x) v (1 v (y v 0))). 3867,3866 [para_into,227,21,demod,18,1163] x^ (0 v c(1 v 1))=x^ (0 v c(0 v 1)). 3877 [copy,3865,flip.1] c(c(x) v (1 v (y v 0)))=x^ (0 v c(y v ((1 v (y v 0)) v 1))). 3881,3880 [back_demod,3021,demod,3867,2384] c(1 v (0 v 0))=c(0 v 1). 4923,4922 [para_from,319,64,demod,169,28,1163,1161,flip.1] (0 v (x^x)) v (y v 1)=x v (y v 1). 5028 [para_into,430,39] (x v (1 v (y v 0)))^ (x v (0 v c(y v ((1 v (y v 0)) v 1))))=x. 5587 [para_into,1106,319,demod,169,28,1163,1161,305,1043,169,28,1163,1161,flip.1] 0 v ((0 v 1)^ (0 v 1))=0 v 1. 5612,5611 [para_from,5587,319,demod,181,4923] (c(0 v 1) v c(0 v 1)) v (0 v 1)=0 v 1. 5840 [para_from,1144,248,demod,169,367,2816] ((0 v 0) v 0)^ (((((1 v 1)^1)^ (0 v 1)) v 0)^1)=0. 5844 [para_from,1144,104,demod,169,367,2816,14] c((0 v 0) v 0)= ((((1 v 1)^1)^ (0 v 1)) v 0)^1. 5866,5865 [para_into,1162,1150] c((0 v 1) v 1)= (0 v 0)^ (0 v c(0 v 1)). 5883 [back_demod,2005,demod,5866] (((0 v 0)^ (0 v c(0 v 1))) v c(0 v 1)) v (0 v 1)=1. 6410 [para_into,168,1150] c(x v (0 v 1))= (c(x v 0) v c(x v 1))^ (0 v 0). 6422 [para_into,168,221,demod,169,28,1163,1161,28,1163,1161] x^ (0 v (y^y))=x^y. 7247 [para_into,218,168,demod,28,1163,1161,28,1163,1161,flip.1] x^ ((y^c(c(y))) v 0)=x^y. 7474 [para_into,222,2235] c((x^ (0 v 0)) v y)= (0 v (c(x) v 1))^ (c(y v 0) v c(y v 1)). 9519 [para_into,242,9,demod,169,28,1163,1161] ((x^c(y)) v (x^y)) v c(x)=1. 9633 [para_into,9519,2411,demod,169,1151,12,46,14] ((1^x) v c(0 v x)) v 0=1. 10131,10130 [para_from,9633,319,demod,1151,1139,flip.1] ((1^x) v c(0 v x)) v 1=1 v 1. 10150 [para_from,9633,2135,demod,10131,1459,flip.1] (1^x) v c(0 v x)=1. 10186 [para_into,10150,7247] (1^x) v c(0 v ((x^c(c(x))) v 0))=1. 10212 [para_into,10150,224,demod,14] c(0 v x) v c(0 v (((c(x v 0) v c(x v 1))^c(x)) v 0))=1. 10220 [para_into,10150,45] x v c(0 v (x v x))=1. 10301,10300 [para_from,10150,319,demod,169,28,1163,1161,305,flip.1] (1^x) v 1= (0 v x) v 1. 10440 [para_from,10220,319,demod,169,28,1163,1161,305] (0 v (x v x)) v 1=x v 1. 10444,10443 [para_from,10220,130] 1^ (0 v (x v (x v x)))=x. 10445 [para_from,10220,76] 1^ (x v (x v (0 v x)))=x. 10688 [para_into,10300,7247,demod,10301,flip.1] (0 v ((x^c(c(x))) v 0)) v 1= (0 v x) v 1. 10690 [para_into,10300,6422,demod,10301,flip.1] (0 v (0 v (x^x))) v 1= (0 v x) v 1. 10848,10847 [para_into,10440,1295,demod,1560,1560] ((0 v 1) v 1) v 1= (0 v 1) v 1. 10902,10901 [back_demod,2733,demod,10848] 1^ ((1 v (0 v 0)) v ((0 v 1) v 1))= (0 v 1) v 1. 10903 [para_from,10440,126,demod,10444,flip.1] 0 v (1 v 1)=1. 11101,11100 [para_from,258,19,demod,28,1163,1161,flip.1] ((x^c(c(x))) v 0) v 1=x v 1. 11131,11130 [para_from,10903,1203,demod,367,flip.1] 1 v 1=0 v 1. 11458 [back_demod,5844,demod,11131] c((0 v 0) v 0)= ((((0 v 1)^1)^ (0 v 1)) v 0)^1. 11460 [back_demod,5840,demod,11131] ((0 v 0) v 0)^ (((((0 v 1)^1)^ (0 v 1)) v 0)^1)=0. 11596 [back_demod,3210,demod,11131,11131] ((0 v c((0 v 1)^1)) v 0)^ (0 v 1)=0 v c((0 v 1)^1). 11598 [back_demod,3208,demod,11131] 0 v (x v (1^ ((0 v 1)^1)))=x v 1. 11992,11991 [para_into,10445,1181,demod,1560,10902] (0 v 1) v 1=1 v (0 v 0). 12052,12051 [back_demod,5865,demod,11992,3881,flip.1] (0 v 0)^ (0 v c(0 v 1))=c(0 v 1). 12140,12139 [back_demod,5883,demod,12052,5612] 0 v 1=1. 12253,12252 [back_demod,11598,demod,12140,1037,12140,1037,12140] 0 v (x v 1)=x v 1. 12255,12254 [back_demod,11596,demod,12140,1037,12140,14,12140,12140,1037,12140,14] ((0 v 0) v 0)^1=0 v 0. 12354,12353 [back_demod,11460,demod,12140,1037,12140,12140,1037,12140,18,1037,12140,12255] 0 v 0=0. 12356,12355 [back_demod,11458,demod,12354,12354,12140,1037,12140,12140,1037,12140,18,1037,12140] c(0)=1. 12406,12405 [back_demod,11130,demod,12140] 1 v 1=1. 12584,12583 [back_demod,6410,demod,12140,12354,flip.1] (c(x v 0) v c(x v 1))^0=c(x v 1). 12810 [back_demod,1896,demod,12140] (x v (1 v (((x v 1) v (x v 1)) v 0)))^1= (x v 1) v (x v 1). 12827,12826 [back_demod,1162,demod,12140,14,12354] c(c(x) v 1)=x^0. 12829,12828 [back_demod,1160,demod,12140,14,12354] ((x^1) v (x^0))^y=x^y. 12896 [back_demod,7474,demod,12354,12253] c((x^0) v y)= (c(x) v 1)^ (c(y v 0) v c(y v 1)). 13249,13248 [para_from,12353,15,flip.1] 0 v (x v (y v 0))=x v (y v 0). 13257,13256 [para_from,12353,4,flip.1] 0 v (x v 0)=x v 0. 13315,13314 [back_demod,10688,demod,13257,11101,flip.1] (0 v x) v 1=x v 1. 13316 [back_demod,10212,demod,13257,105,169,28,12827,12829,42,52] c(0 v x) v x=1. 13318 [back_demod,10186,demod,13257,105,52] (1^x) v c(x)=1. 13448 [back_demod,10690,demod,13315,13315,13315] (x^x) v 1=x v 1. 13452 [back_demod,10440,demod,13315] (x v x) v 1=x v 1. 13859 [para_from,13316,124,demod,12406,13257,flip.1] x v (c(x v 0) v 1)=1. 13861 [para_from,13316,60,demod,12406,13257,flip.1] c(x v 0) v (x v 1)=1. 14031 [para_into,13318,45] x v c(x v x)=1. 14186,14185 [para_from,14031,2535,demod,46,12140] (x v x)^1=x. 14305,14304 [para_into,14185,4] (x v ((x v y) v y))^1=x v y. 14332 [para_from,14185,110] (c(x v x) v 0) v x=1. 14843 [para_into,13314,386,demod,13249] (1 v (x v 0)) v 1= (x v 1) v 1. 14882,14881 [para_into,13314,21] 1 v ((0 v x) v 0)=x v 1. 15156,15155 [para_into,13452,21] 1 v ((x v x) v 0)=x v 1. 15158,15157 [back_demod,12810,demod,15156,14305,flip.1] (x v 1) v (x v 1)=x v 1. 15355,15354 [para_from,286,74,demod,34,15158,34] 1^ (x v 1)=x v 1. 15822 [para_into,290,70,demod,14882] x v (y v (c(y v ((x v (y v 1)) v (x v 1))) v 1))=1. 15828 [para_into,290,39,demod,18,13315] x v (c(x v ((1 v (x v 0)) v 1)) v 1)=1. 15842 [para_from,290,62,demod,18,13315,flip.1] x v (y v (c(x v ((1 v (x v 0)) v 1)) v 1))=y v 1. 16165 [para_from,13859,130] (x v c(y v (z v (c(x v 0) v 1))))^ (y v (z v 1))=x. 16209 [para_into,13861,13448,demod,105,14186] c(x) v (x v 1)=1. 16220,16219 [para_from,13861,319,demod,15158,13315] c(x v 1) v 1=c(x v 0) v 1. 16363 [para_into,16209,4] x v (c(x) v 1)=1. 16366,16365 [para_from,16209,319,demod,15158,13315,16220] c(x v 0) v 1=c(x) v 1. 16466,16465 [back_demod,16219,demod,16366] c(x v 1) v 1=c(x) v 1. 16469 [back_demod,16165,demod,16366] (x v c(y v (z v (c(x) v 1))))^ (y v (z v 1))=x. 16500 [para_from,16363,319,demod,15158,12827,13315] (x^0) v 1=x v 1. 16723,16722 [para_into,16500,184,demod,12584,16466,13315,flip.1] c(x v x) v 1=c(x) v 1. 17210 [para_into,14332,39] (c(x v ((1 v (x v 0)) v 1)) v 0) v (1 v (x v 0))=1. 17794,17793 [para_into,307,16209,demod,15158,169,12354,12356,12140,14,18,15355,flip.1] (x v 1) v 1=x v 1. 17796,17795 [para_into,307,319,demod,13315,16723,13315,16723] x v (c(x v y) v 1)=c(y) v 1. 17875,17874 [back_demod,14843,demod,17794] (1 v (x v 0)) v 1=x v 1. 17905,17904 [back_demod,15828,demod,17875,17796,16466] c(x) v 1=1. 17907,17906 [back_demod,15822,demod,17905] x v (y v 1)=1. 17916,17915 [back_demod,17210,demod,17875,17907,14,12354,13249] 1 v (x v 0)=1. 17918,17917 [back_demod,15842,demod,17916,12406,17905,17907,flip.1] x v 1=1. 17920,17919 [back_demod,5028,demod,17916,17918,17916,17918,17918,14,12354] 1^ (x v 0)=x. 17922,17921 [back_demod,3877,demod,17916,17918,14,17916,17918,17918,14,12354,flip.1] x^0=0. 17980,17979 [back_demod,16469,demod,17918,17918,17918,14,17918,17918] (x v 0)^1=x. 17989 [back_demod,12896,demod,17922,17918,17918,14,17920] c(0 v x)=c(x v 0). 20575 [para_from,17989,27,demod,28,17980,flip.1] (0 v x)^1=x. 20873,20872 [para_into,20575,13256,demod,17980,flip.1] x v 0=x. 21688,21687 [back_demod,17979,demod,20873] x^1=x. 21861 [back_demod,27,demod,20873,21688] c(c(x))=x. 21863 [binary,21861,2] $Ans(CC). ------------ end of proof ------------- given clause #427: (wt=5) 20872 [para_into,20575,13256,demod,17980,flip.1] x v 0=x. given clause #428: (wt=5) 21249 [back_demod,20339,demod,20926,19111,20873,12356,20873,46,20873,20926,19111,20873,12356,20873,46] x^x=x. given clause #429: (wt=25) 442 [para_into,43,29] (x v ((c(y) v (z^u))^v))^ (x v ((y^ (c(z) v c(u))) v c(v)))=x. given clause #430: (wt=5) 21687 [back_demod,17979,demod,20873] x^1=x. given clause #431: (wt=5) 21691 [back_demod,17919,demod,20873] 1^x=x. given clause #432: (wt=5) 21695 [back_demod,17343,demod,21250,20873,21692,21250,20873] x v x=x. given clause #433: (wt=25) 448 [para_into,43,29] (x v (y^ (c(z) v (u^v))))^ (x v (c(y) v (z^ (c(u) v c(v)))))=x. given clause #434: (wt=5) 21761 [back_demod,13256,demod,20873,20873] 0 v x=x. given clause #435: (wt=5) 21861 [back_demod,27,demod,20873,21688] c(c(x))=x. given clause #436: (wt=6) 21321 [back_demod,19547,demod,20873] c(x) v x=1. given clause #437: (wt=15) 454 [para_into,43,4] (x v (y^z))^ (c(y) v (x v c(z)))=x. given clause #438: (wt=6) 21341 [back_demod,19487,demod,20873] c(x)^x=0. given clause #439: (wt=7) 21964 [back_demod,17995,demod,21250,21762,21688,21250,21762] x v (y^x)=x. given clause #440: (wt=7) 22292 [para_from,20872,4,demod,20873] x v y=y v x. given clause #441: (wt=20) 505 [para_into,53,29] (x v (y^ (c(z) v c(u))))^ (c(y) v (x v (z^u)))=x. given clause #442: (wt=7) 22499 [para_into,22292,21964,flip.1] (x^y) v y=y. given clause #443: (wt=8) 21275 [back_demod,19903,demod,20873] c(x) v (y v x)=1. given clause #444: (wt=8) 21639 [back_demod,18409,demod,20873,20873] x v (c(x) v y)=1. ----> UNIT CONFLICT at 9.87 sec ----> 22977 [binary,22975,1] $Ans(B1). Length of proof is 242. Level of proof is 48. ---------------- PROOF ---------------- 1 [] A v (A^B)!=A|$Ans(B1). 4 [] x v (y v z)=y v (x v z). 5 [] x^y=c(c(x) v c(y)). 6 [copy,5,flip.1] c(c(x) v c(y))=x^y. 9 [] (x v c(y))^ (x v y)=x. 12,11 [] x v c(x)=1. 14,13 [] c(1)=0. 15 [para_into,4,4] x v (y v (z v u))=z v (x v (y v u)). 16 [copy,15,flip.1] x v (y v (z v u))=y v (z v (x v u)). 18,17 [para_into,11,13] 1 v 0=1. 19 [para_from,11,4,flip.1] x v (y v c(x))=y v 1. 21 [para_from,17,4] x v 1=1 v (x v 0). 22 [copy,21,flip.1] 1 v (x v 0)=x v 1. 23 [para_into,6,13] c(0 v c(x))=1^x. 25 [para_into,6,6] c((x^y) v c(z))= (c(x) v c(y))^z. 28,27 [para_into,6,13] c(c(x) v 0)=x^1. 29 [para_into,6,6] c(c(x) v (y^z))=x^ (c(y) v c(z)). 31 [para_into,6,11,demod,14,flip.1] x^c(x)=0. 34,33 [para_from,6,11] (c(x) v c(y)) v (x^y)=1. 35 [para_into,31,13] 1^0=0. 39 [para_from,21,4] x v (1 v (y v 0))=y v (x v 1). 40 [copy,39,flip.1] x v (y v 1)=y v (1 v (x v 0)). 42,41 [para_into,9,13] (x v 0)^ (x v 1)=x. 43 [para_into,9,6] (x v (y^z))^ (x v (c(y) v c(z)))=x. 46,45 [para_into,9,11] 1^ (x v x)=x. 47 [para_into,9,21,demod,14] (x v 0)^ (1 v (x v 0))=x. 49 [para_into,9,17] (1 v c(0))^1=1. 52,51 [para_into,9,11] (x v c(c(x)))^1=x. 53 [para_into,9,4] (x v c(y v z))^ (y v (x v z))=x. 56,55 [para_into,45,4] 1^ (x v ((x v y) v y))=x v y. 59 [para_from,22,4] x v (y v 1)=1 v (x v (y v 0)). 60 [copy,59,flip.1] 1 v (x v (y v 0))=x v (y v 1). 62 [para_into,15,21] x v (y v (1 v (z v 0)))=z v (x v (y v 1)). 64 [para_into,15,11,flip.1] x v (y v (z v c(x)))=y v (z v 1). 68 [para_into,15,4] x v (y v (z v u))=z v (y v (x v u)). 70 [copy,62,flip.1] x v (y v (z v 1))=y v (z v (1 v (x v 0))). 74 [para_from,15,45] 1^ (x v ((y v (x v z)) v (y v z)))=y v (x v z). 76 [para_from,15,9] (x v c(y v (z v u)))^ (z v (x v (y v u)))=x. 83,82 [para_into,23,13] c(0 v 0)=1^1. 84 [para_into,23,6] c(0 v (x^y))=1^ (c(x) v c(y)). 86 [para_from,23,9] (x v (1^y))^ (x v (0 v c(y)))=x. 90 [para_from,23,11] (0 v c(x)) v (1^x)=1. 92 [para_from,82,9] (x v (1^1))^ (x v (0 v 0))=x. 96 [para_from,82,11] (0 v 0) v (1^1)=1. 105,104 [para_into,27,6] c((x^y) v 0)= (c(x) v c(y))^1. 108 [para_from,27,31] (c(x) v 0)^ (x^1)=0. 110 [para_from,27,11] (c(x) v 0) v (x^1)=1. 116 [para_into,16,22] x v (y v 1)=1 v (y v (x v 0)). 124 [copy,116,flip.1] 1 v (x v (y v 0))=y v (x v 1). 126 [para_from,16,45] 1^ (x v (y v ((x v (y v z)) v z)))=x v (y v z). 130 [para_from,16,9] (x v c(y v (z v u)))^ (y v (z v (x v u)))=x. 133 [para_into,51,82] ((0 v 0) v c(1^1))^1=0 v 0. 167 [para_into,25,45,demod,14] c(x v c(y))= (0 v c(x v x))^y. 169,168 [para_into,25,41] c(x v c(y))= (c(x v 0) v c(x v 1))^y. 171,170 [para_into,25,35,demod,169,83,14,12] ((1^1) v c(0 v 1))^x=1^x. 181,180 [para_into,25,6] c((x^y) v (z^u))= (c(x) v c(y))^ (c(z) v c(u)). 184 [copy,167,flip.1,demod,169] (0 v c(x v x))^y= (c(x v 0) v c(x v 1))^y. 190 [back_demod,6,demod,169,28] ((x^1) v c(c(x) v 1))^y=x^y. 192 [para_into,90,82,demod,46] (0 v (1^1)) v 0=1. 196 [para_into,90,45] (0 v c(x v x)) v x=1. 200 [para_from,192,41] 1^ ((0 v (1^1)) v 1)=0 v (1^1). 203,202 [para_from,192,22,flip.1] (0 v (1^1)) v 1=1 v 1. 209 [back_demod,200,demod,203,46,flip.1] 0 v (1^1)=1. 214 [para_from,209,9] (0 v c(1^1))^1=0. 216 [para_from,209,4,flip.1] 0 v (x v (1^1))=x v 1. 218 [para_into,29,51,demod,169,14] c(c(x) v y)=x^ (((c(y v 0) v c(y v 1))^c(y)) v 0). 220,219 [para_into,29,49,demod,169,18,14,14] c(c(x) v 1)=x^ (((0 v c(1 v 1))^0) v 0). 221 [para_into,29,45,demod,14] c(c(x) v y)=x^ (0 v c(y v y)). 222 [para_into,29,41] c(c(x) v y)=x^ (c(y v 0) v c(y v 1)). 224 [copy,218,flip.1] x^ (((c(y v 0) v c(y v 1))^c(y)) v 0)=c(c(x) v y). 226,225 [back_demod,190,demod,220] ((x^1) v (x^ (((0 v c(1 v 1))^0) v 0)))^y=x^y. 227 [copy,221,flip.1] x^ (0 v c(y v y))=c(c(x) v y). 242 [para_from,29,11] (c(x) v (y^z)) v (x^ (c(y) v c(z)))=1. 248 [para_into,108,27] ((x^1) v 0)^ ((c(x) v 0)^1)=0. 258 [para_into,110,51,demod,169] (((c(x v 0) v c(x v 1))^c(x)) v 0) v x=1. 282 [para_into,33,41] (c(x v 0) v c(x v 1)) v x=1. 286 [para_from,33,15,flip.1] (c(x) v c(y)) v (z v (u v (x^y)))=z v (u v 1). 290 [para_into,196,15] (0 v c(x v ((y v (x v z)) v (y v z)))) v (y v (x v z))=1. 305,304 [para_from,196,19,demod,169,28,220,226,flip.1] (0 v (x^x)) v 1=x v 1. 307 [para_from,196,15,flip.1] x v (y v ((0 v c((x v z) v (x v z))) v z))=y v 1. 315 [para_from,196,4] x v 1= (0 v c(y v y)) v (x v y). 319 [copy,315,flip.1] (0 v c(x v x)) v (y v x)=y v 1. 321,320 [para_from,214,110,demod,169,83,171] ((1^ (1^1)) v 0) v 0=1. 367,366 [para_into,216,196,demod,181,14,14,14,14,305,flip.1] (0 v 0) v 1=0 v 1. 386 [para_into,40,4] x v (y v 1)=x v (1 v (y v 0)). 420,419 [para_from,320,47,demod,321,46,flip.1] (1^ (1^1)) v 0=1. 422 [para_from,419,47,demod,420,46,flip.1] 1^ (1^1)=1. 430 [para_into,43,45,demod,14] (x v y)^ (x v (0 v c(y v y)))=x. 438 [para_into,43,209,demod,14,14] 1^ (0 v (0 v 0))=0. 452 [para_into,43,19] (x v (y^x))^ (c(y) v 1)=x. 454 [para_into,43,4] (x v (y^z))^ (c(y) v (x v c(z)))=x. 464 [para_from,422,43,demod,14] (x v 1)^ (x v (0 v c(1^1)))=x. 466 [para_from,422,29,demod,220,14,flip.1] x^ (0 v c(1^1))=x^ (((0 v c(1 v 1))^0) v 0). 469,468 [para_from,438,90] (0 v c(0 v (0 v 0))) v 0=1. 503 [para_into,53,82] (x v (1^1))^ (0 v (x v 0))=x. 639 [para_into,452,422,demod,14] ((1^1) v 1)^ (0 v 1)=1^1. 651 [para_into,452,45,demod,14] ((x v x) v x)^ (0 v 1)=x v x. 714 [para_from,468,47,demod,469,46,flip.1] 0 v c(0 v (0 v 0))=1. 744,743 [para_into,60,196,flip.1] (0 v c((x v 0) v (x v 0))) v (x v 1)=1 v 1. 903,902 [para_into,282,82] ((1^1) v c(0 v 1)) v 0=1. 946 [para_from,282,47,demod,83,903,46,83,flip.1] (1^1) v c(0 v 1)=1. 1015 [para_into,946,21] (1^1) v c(1 v (0 v 0))=1. 1017 [para_from,946,53] 1^ (0 v ((1^1) v 1))=1^1. 1020,1019 [para_from,946,19,flip.1] (1^1) v 1= (0 v 1) v 1. 1037,1036 [back_demod,1017,demod,1020,56,flip.1] 1^1=0 v 1. 1043,1042 [back_demod,639,demod,1037,1037] ((0 v 1) v 1)^ (0 v 1)=0 v 1. 1044 [back_demod,1015,demod,1037] (0 v 1) v c(1 v (0 v 0))=1. 1092 [back_demod,503,demod,1037] (x v (0 v 1))^ (0 v (x v 0))=x. 1105,1104 [back_demod,466,demod,1037,flip.1] x^ (((0 v c(1 v 1))^0) v 0)=x^ (0 v c(0 v 1)). 1106 [back_demod,464,demod,1037] (x v 1)^ (x v (0 v c(0 v 1)))=x. 1139,1138 [back_demod,209,demod,1037] 0 v (0 v 1)=1. 1144 [back_demod,133,demod,1037] ((0 v 0) v c(0 v 1))^1=0 v 0. 1146 [back_demod,96,demod,1037] (0 v 0) v (0 v 1)=1. 1148 [back_demod,92,demod,1037] (x v (0 v 1))^ (x v (0 v 0))=x. 1151,1150 [back_demod,82,demod,1037] c(0 v 0)=0 v 1. 1161,1160 [back_demod,225,demod,1105] ((x^1) v (x^ (0 v c(0 v 1))))^y=x^y. 1163,1162 [back_demod,219,demod,1105] c(c(x) v 1)=x^ (0 v c(0 v 1)). 1164 [para_from,1036,452,demod,14] (1 v (0 v 1))^ (0 v 1)=1. 1166 [para_from,1036,29,demod,14,14] c(c(x) v (0 v 1))=x^ (0 v 0). 1181 [para_into,1138,21] 0 v (1 v (0 v 0))=1. 1190,1189 [para_from,1138,16,flip.1] 0 v (0 v (x v 1))=x v 1. 1203 [para_from,1146,16,flip.1] (0 v 0) v (0 v (x v 1))=x v 1. 1286 [para_from,1181,16,flip.1] 0 v (1 v (x v (0 v 0)))=x v 1. 1295 [para_from,1181,4,flip.1] 0 v (x v (1 v (0 v 0)))=x v 1. 1459,1458 [para_into,1164,40,demod,18] (0 v (1 v 1))^ (0 v 1)=1. 1550,1549 [para_from,1458,29,demod,1163,flip.1] x^ (c(0 v (1 v 1)) v c(0 v 1))=x^ (0 v c(0 v 1)). 1560,1559 [para_from,1044,19] (1 v (0 v 0)) v 1= (0 v 1) v 1. 1896 [para_into,651,40] (x v (1 v (((x v 1) v (x v 1)) v 0)))^ (0 v 1)= (x v 1) v (x v 1). 2005 [para_from,1042,33] (c((0 v 1) v 1) v c(0 v 1)) v (0 v 1)=1. 2135 [para_into,1092,4] (0 v (x v 1))^ (0 v (x v 0))=x. 2213 [para_into,1148,4] (0 v (x v 1))^ (x v (0 v 0))=x. 2216,2215 [para_into,1148,196,demod,744,flip.1] 0 v c((0 v 0) v (0 v 0))= (1 v 1)^1. 2235 [para_into,1166,4] c(0 v (c(x) v 1))=x^ (0 v 0). 2361,2360 [para_into,1286,282,demod,367,flip.1] (c((0 v 0) v 0) v c(0 v 1)) v 1=0 v (1 v 1). 2384,2383 [para_into,84,1458,demod,1550,flip.1] 1^ (0 v c(0 v 1))=c(0 v 1). 2405 [para_into,84,45,demod,14] c(0 v x)=1^ (0 v c(x v x)). 2411 [copy,2405,flip.1] 1^ (0 v c(x v x))=c(0 v x). 2535 [para_into,86,4] (x v (1^y))^ (0 v (x v c(y)))=x. 2733 [para_from,1559,55,demod,1560] 1^ ((1 v (0 v 0)) v (((0 v 1) v 1) v 1))= (0 v 1) v 1. 2816,2815 [para_into,2213,282,demod,367,2361,1190,367,flip.1] c((0 v 0) v 0) v c(0 v 1)= (1 v 1)^1. 3021 [para_into,2405,21] c(1 v (0 v 0))=1^ (0 v c(1 v 1)). 3107 [para_from,2405,714,demod,2216] 0 v (1^ ((1 v 1)^1))=1. 3185 [para_from,3107,84,demod,14,14,flip.1] 1^ (0 v c((1 v 1)^1))=0. 3208 [para_from,3107,4,flip.1] 0 v (x v (1^ ((1 v 1)^1)))=x v 1. 3210 [para_from,3185,452,demod,14] ((0 v c((1 v 1)^1)) v 0)^ (0 v 1)=0 v c((1 v 1)^1). 3865 [para_into,227,39] x^ (0 v c(y v ((1 v (y v 0)) v 1)))=c(c(x) v (1 v (y v 0))). 3867,3866 [para_into,227,21,demod,18,1163] x^ (0 v c(1 v 1))=x^ (0 v c(0 v 1)). 3877 [copy,3865,flip.1] c(c(x) v (1 v (y v 0)))=x^ (0 v c(y v ((1 v (y v 0)) v 1))). 3881,3880 [back_demod,3021,demod,3867,2384] c(1 v (0 v 0))=c(0 v 1). 4923,4922 [para_from,319,64,demod,169,28,1163,1161,flip.1] (0 v (x^x)) v (y v 1)=x v (y v 1). 5028 [para_into,430,39] (x v (1 v (y v 0)))^ (x v (0 v c(y v ((1 v (y v 0)) v 1))))=x. 5587 [para_into,1106,319,demod,169,28,1163,1161,305,1043,169,28,1163,1161,flip.1] 0 v ((0 v 1)^ (0 v 1))=0 v 1. 5612,5611 [para_from,5587,319,demod,181,4923] (c(0 v 1) v c(0 v 1)) v (0 v 1)=0 v 1. 5840 [para_from,1144,248,demod,169,367,2816] ((0 v 0) v 0)^ (((((1 v 1)^1)^ (0 v 1)) v 0)^1)=0. 5844 [para_from,1144,104,demod,169,367,2816,14] c((0 v 0) v 0)= ((((1 v 1)^1)^ (0 v 1)) v 0)^1. 5866,5865 [para_into,1162,1150] c((0 v 1) v 1)= (0 v 0)^ (0 v c(0 v 1)). 5883 [back_demod,2005,demod,5866] (((0 v 0)^ (0 v c(0 v 1))) v c(0 v 1)) v (0 v 1)=1. 6410 [para_into,168,1150] c(x v (0 v 1))= (c(x v 0) v c(x v 1))^ (0 v 0). 6422 [para_into,168,221,demod,169,28,1163,1161,28,1163,1161] x^ (0 v (y^y))=x^y. 7247 [para_into,218,168,demod,28,1163,1161,28,1163,1161,flip.1] x^ ((y^c(c(y))) v 0)=x^y. 7474 [para_into,222,2235] c((x^ (0 v 0)) v y)= (0 v (c(x) v 1))^ (c(y v 0) v c(y v 1)). 9519 [para_into,242,9,demod,169,28,1163,1161] ((x^c(y)) v (x^y)) v c(x)=1. 9633 [para_into,9519,2411,demod,169,1151,12,46,14] ((1^x) v c(0 v x)) v 0=1. 10131,10130 [para_from,9633,319,demod,1151,1139,flip.1] ((1^x) v c(0 v x)) v 1=1 v 1. 10150 [para_from,9633,2135,demod,10131,1459,flip.1] (1^x) v c(0 v x)=1. 10186 [para_into,10150,7247] (1^x) v c(0 v ((x^c(c(x))) v 0))=1. 10212 [para_into,10150,224,demod,14] c(0 v x) v c(0 v (((c(x v 0) v c(x v 1))^c(x)) v 0))=1. 10220 [para_into,10150,45] x v c(0 v (x v x))=1. 10301,10300 [para_from,10150,319,demod,169,28,1163,1161,305,flip.1] (1^x) v 1= (0 v x) v 1. 10440 [para_from,10220,319,demod,169,28,1163,1161,305] (0 v (x v x)) v 1=x v 1. 10444,10443 [para_from,10220,130] 1^ (0 v (x v (x v x)))=x. 10445 [para_from,10220,76] 1^ (x v (x v (0 v x)))=x. 10688 [para_into,10300,7247,demod,10301,flip.1] (0 v ((x^c(c(x))) v 0)) v 1= (0 v x) v 1. 10690 [para_into,10300,6422,demod,10301,flip.1] (0 v (0 v (x^x))) v 1= (0 v x) v 1. 10848,10847 [para_into,10440,1295,demod,1560,1560] ((0 v 1) v 1) v 1= (0 v 1) v 1. 10902,10901 [back_demod,2733,demod,10848] 1^ ((1 v (0 v 0)) v ((0 v 1) v 1))= (0 v 1) v 1. 10903 [para_from,10440,126,demod,10444,flip.1] 0 v (1 v 1)=1. 11101,11100 [para_from,258,19,demod,28,1163,1161,flip.1] ((x^c(c(x))) v 0) v 1=x v 1. 11131,11130 [para_from,10903,1203,demod,367,flip.1] 1 v 1=0 v 1. 11458 [back_demod,5844,demod,11131] c((0 v 0) v 0)= ((((0 v 1)^1)^ (0 v 1)) v 0)^1. 11460 [back_demod,5840,demod,11131] ((0 v 0) v 0)^ (((((0 v 1)^1)^ (0 v 1)) v 0)^1)=0. 11596 [back_demod,3210,demod,11131,11131] ((0 v c((0 v 1)^1)) v 0)^ (0 v 1)=0 v c((0 v 1)^1). 11598 [back_demod,3208,demod,11131] 0 v (x v (1^ ((0 v 1)^1)))=x v 1. 11992,11991 [para_into,10445,1181,demod,1560,10902] (0 v 1) v 1=1 v (0 v 0). 12052,12051 [back_demod,5865,demod,11992,3881,flip.1] (0 v 0)^ (0 v c(0 v 1))=c(0 v 1). 12140,12139 [back_demod,5883,demod,12052,5612] 0 v 1=1. 12253,12252 [back_demod,11598,demod,12140,1037,12140,1037,12140] 0 v (x v 1)=x v 1. 12255,12254 [back_demod,11596,demod,12140,1037,12140,14,12140,12140,1037,12140,14] ((0 v 0) v 0)^1=0 v 0. 12354,12353 [back_demod,11460,demod,12140,1037,12140,12140,1037,12140,18,1037,12140,12255] 0 v 0=0. 12356,12355 [back_demod,11458,demod,12354,12354,12140,1037,12140,12140,1037,12140,18,1037,12140] c(0)=1. 12406,12405 [back_demod,11130,demod,12140] 1 v 1=1. 12584,12583 [back_demod,6410,demod,12140,12354,flip.1] (c(x v 0) v c(x v 1))^0=c(x v 1). 12810 [back_demod,1896,demod,12140] (x v (1 v (((x v 1) v (x v 1)) v 0)))^1= (x v 1) v (x v 1). 12827,12826 [back_demod,1162,demod,12140,14,12354] c(c(x) v 1)=x^0. 12829,12828 [back_demod,1160,demod,12140,14,12354] ((x^1) v (x^0))^y=x^y. 12896 [back_demod,7474,demod,12354,12253] c((x^0) v y)= (c(x) v 1)^ (c(y v 0) v c(y v 1)). 13249,13248 [para_from,12353,15,flip.1] 0 v (x v (y v 0))=x v (y v 0). 13257,13256 [para_from,12353,4,flip.1] 0 v (x v 0)=x v 0. 13315,13314 [back_demod,10688,demod,13257,11101,flip.1] (0 v x) v 1=x v 1. 13316 [back_demod,10212,demod,13257,105,169,28,12827,12829,42,52] c(0 v x) v x=1. 13318 [back_demod,10186,demod,13257,105,52] (1^x) v c(x)=1. 13448 [back_demod,10690,demod,13315,13315,13315] (x^x) v 1=x v 1. 13452 [back_demod,10440,demod,13315] (x v x) v 1=x v 1. 13859 [para_from,13316,124,demod,12406,13257,flip.1] x v (c(x v 0) v 1)=1. 13861 [para_from,13316,60,demod,12406,13257,flip.1] c(x v 0) v (x v 1)=1. 14031 [para_into,13318,45] x v c(x v x)=1. 14186,14185 [para_from,14031,2535,demod,46,12140] (x v x)^1=x. 14305,14304 [para_into,14185,4] (x v ((x v y) v y))^1=x v y. 14332 [para_from,14185,110] (c(x v x) v 0) v x=1. 14719 [para_from,13256,13316] c(x v 0) v (x v 0)=1. 14843 [para_into,13314,386,demod,13249] (1 v (x v 0)) v 1= (x v 1) v 1. 14882,14881 [para_into,13314,21] 1 v ((0 v x) v 0)=x v 1. 15156,15155 [para_into,13452,21] 1 v ((x v x) v 0)=x v 1. 15158,15157 [back_demod,12810,demod,15156,14305,flip.1] (x v 1) v (x v 1)=x v 1. 15355,15354 [para_from,286,74,demod,34,15158,34] 1^ (x v 1)=x v 1. 15822 [para_into,290,70,demod,14882] x v (y v (c(y v ((x v (y v 1)) v (x v 1))) v 1))=1. 15828 [para_into,290,39,demod,18,13315] x v (c(x v ((1 v (x v 0)) v 1)) v 1)=1. 15842 [para_from,290,62,demod,18,13315,flip.1] x v (y v (c(x v ((1 v (x v 0)) v 1)) v 1))=y v 1. 16165 [para_from,13859,130] (x v c(y v (z v (c(x v 0) v 1))))^ (y v (z v 1))=x. 16209 [para_into,13861,13448,demod,105,14186] c(x) v (x v 1)=1. 16220,16219 [para_from,13861,319,demod,15158,13315] c(x v 1) v 1=c(x v 0) v 1. 16363 [para_into,16209,4] x v (c(x) v 1)=1. 16366,16365 [para_from,16209,319,demod,15158,13315,16220] c(x v 0) v 1=c(x) v 1. 16466,16465 [back_demod,16219,demod,16366] c(x v 1) v 1=c(x) v 1. 16469 [back_demod,16165,demod,16366] (x v c(y v (z v (c(x) v 1))))^ (y v (z v 1))=x. 16500 [para_from,16363,319,demod,15158,12827,13315] (x^0) v 1=x v 1. 16723,16722 [para_into,16500,184,demod,12584,16466,13315,flip.1] c(x v x) v 1=c(x) v 1. 17210 [para_into,14332,39] (c(x v ((1 v (x v 0)) v 1)) v 0) v (1 v (x v 0))=1. 17536 [para_from,14719,68] x v 1=y v (c(y v 0) v (x v 0)). 17573 [copy,17536,flip.1] x v (c(x v 0) v (y v 0))=y v 1. 17794,17793 [para_into,307,16209,demod,15158,169,12354,12356,12140,14,18,15355,flip.1] (x v 1) v 1=x v 1. 17796,17795 [para_into,307,319,demod,13315,16723,13315,16723] x v (c(x v y) v 1)=c(y) v 1. 17875,17874 [back_demod,14843,demod,17794] (1 v (x v 0)) v 1=x v 1. 17905,17904 [back_demod,15828,demod,17875,17796,16466] c(x) v 1=1. 17907,17906 [back_demod,15822,demod,17905] x v (y v 1)=1. 17916,17915 [back_demod,17210,demod,17875,17907,14,12354,13249] 1 v (x v 0)=1. 17918,17917 [back_demod,15842,demod,17916,12406,17905,17907,flip.1] x v 1=1. 17920,17919 [back_demod,5028,demod,17916,17918,17916,17918,17918,14,12354] 1^ (x v 0)=x. 17922,17921 [back_demod,3877,demod,17916,17918,14,17916,17918,17918,14,12354,flip.1] x^0=0. 17980,17979 [back_demod,16469,demod,17918,17918,17918,14,17918,17918] (x v 0)^1=x. 17989 [back_demod,12896,demod,17922,17918,17918,14,17920] c(0 v x)=c(x v 0). 18409 [back_demod,17573,demod,17918] x v (c(x v 0) v (y v 0))=1. 20575 [para_from,17989,27,demod,28,17980,flip.1] (0 v x)^1=x. 20873,20872 [para_into,20575,13256,demod,17980,flip.1] x v 0=x. 21639 [back_demod,18409,demod,20873,20873] x v (c(x) v y)=1. 21688,21687 [back_demod,17979,demod,20873] x^1=x. 21862,21861 [back_demod,27,demod,20873,21688] c(c(x))=x. 22975 [para_from,21639,454,demod,21862,21688,21862] x v (x^y)=x. 22977 [binary,22975,1] $Ans(B1). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 444 clauses generated 41188 clauses kept 13469 clauses forward subsumed 32740 clauses back subsumed 53 Kbytes malloced 12837 ----------- times (seconds) ----------- user CPU time 9.88 (0 hr, 0 min, 9 sec) system CPU time 0.71 (0 hr, 0 min, 0 sec) wall-clock time 11 (0 hr, 0 min, 11 sec) para_into time 0.10 para_from time 0.15 for_sub time 0.18 back_sub time 0.32 conflict time 0.05 demod time 0.75 That finishes the proof of the theorem. Process 26080 finished Fri Sep 12 16:36:30 2003