----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:34:53 2003 The command was "otter". The process ID is 26015. include("ortholattice-header"). ------- start included file ortholattice-header------- op(400,infix,^). op(400,infix,v). lex([A,B,C,D,0,1,x v x,c(x),x^x,f(x,x)]). set(anl_eq). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(process_input). dependent: set(lrpo). assign(pick_given_ratio,3). assign(max_weight,25). clear(detailed_history). assign(max_seconds,60). assign(max_mem,100000). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). clear(print_kept). assign(stats_level,1). list(usable). 0 [] x=x. end_of_list. ------- end included file ortholattice-header------- list(sos). 0 [] x v (y v z)=y v (x v z). 0 [] x v (x^y)=x. 0 [] x^y=c(c(x) v c(y)). 0 [] x v (c(x)^ (x v y))=x v y. 0 [] f(x,y)=c(x) v c(y). end_of_list. lex([D,C,B,A,0,1,f(x,x),x v x,c(x),x^x]). assign(max_proofs,6). assign(max_weight,21). assign(pick_given_ratio,4). list(passive). 1 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C)))|$Ans(A_SS). 2 [] f(f(A,A),f(A,B))!=A|$Ans(B_SS). 3 [] f(A,f(A,f(A,B)))!=f(A,B)|$Ans(OM_SS). 4 [] A v B!=f(f(A,A),f(B,B))|$Ans(DEF_J). 5 [] A^B!=f(f(A,B),f(A,B))|$Ans(DEF_M). 6 [] c(A)!=f(A,A)|$Ans(DEF_C). 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=11): 8 [] x v (y v z)=y v (x v z). ** KEPT (pick-wt=7): 9 [] x v (x^y)=x. ---> New Demodulator: 10 [new_demod,9] x v (x^y)=x. ** KEPT (pick-wt=10): 11 [] x^y=c(c(x) v c(y)). ---> New Demodulator: 12 [new_demod,11] x^y=c(c(x) v c(y)). ** KEPT (pick-wt=15): 14 [copy,13,demod,12] x v c(c(c(x)) v c(x v y))=x v y. ---> New Demodulator: 15 [new_demod,14] x v c(c(c(x)) v c(x v y))=x v y. ** KEPT (pick-wt=9): 17 [copy,16,flip.1] c(x) v c(y)=f(x,y). ---> New Demodulator: 18 [new_demod,17] c(x) v c(y)=f(x,y). Following clause subsumed by 8 during input processing: 0 [copy,8,flip.1] x v (y v z)=y v (x v z). >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 12. >> back demodulating 9 with 12. >>>> Starting back demodulation with 15. >>>> Starting back demodulation with 18. >> back demodulating 14 with 18. >> back demodulating 11 with 18. >>>> Starting back demodulation with 20. >>>> Starting back demodulation with 22. >>>> Starting back demodulation with 24. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 8 [] x v (y v z)=y v (x v z). given clause #2: (wt=8) 19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. given clause #3: (wt=8) 23 [back_demod,11,demod,18] x^y=c(f(x,y)). given clause #4: (wt=9) 17 [copy,16,flip.1] c(x) v c(y)=f(x,y). given clause #5: (wt=9) 29 [para_into,17,19,flip.1] f(x,f(c(x),y))=c(x). given clause #6: (wt=13) 21 [back_demod,14,demod,18] x v c(f(c(x),x v y))=x v y. given clause #7: (wt=7) 35 [para_from,29,19] x v c(c(x))=x. given clause #8: (wt=8) 33 [para_into,29,29] f(x,c(c(x)))=c(x). given clause #9: (wt=9) 37 [para_into,21,19,demod,20] x v c(f(c(x),x))=x. given clause #10: (wt=11) 47 [para_from,35,8,flip.1] x v (y v c(c(x)))=y v x. given clause #11: (wt=15) 25 [para_into,8,8] x v (y v (z v u))=z v (x v (y v u)). given clause #12: (wt=11) 49 [para_into,37,17] f(x,f(c(c(x)),c(x)))=c(x). given clause #13: (wt=11) 53 [para_into,47,17] x v f(y,c(x))=c(y) v x. given clause #14: (wt=11) 54 [copy,53,flip.1] c(x) v y=y v f(x,c(y)). given clause #15: (wt=12) 27 [para_from,19,8,flip.1] x v (y v c(f(x,z)))=y v x. given clause #16: (wt=15) 26 [copy,25,flip.1] x v (y v (z v u))=y v (z v (x v u)). given clause #17: (wt=9) 104 [para_into,27,37] c(x) v x=x v c(x). given clause #18: (wt=9) 127 [para_into,104,17,demod,18] f(c(x),x)=f(x,c(x)). given clause #19: (wt=9) 145 [para_from,127,29] f(x,f(x,c(x)))=c(x). given clause #20: (wt=11) 106 [para_into,27,21] c(x) v (x v y)=x v c(x). given clause #21: (wt=13) 31 [para_from,17,8] x v f(y,z)=c(y) v (x v c(z)). given clause #22: (wt=9) 173 [back_demod,149,demod,170] x v c(x)=f(x,c(x)). given clause #23: (wt=9) 199 [back_demod,104,demod,174] c(x) v x=f(x,c(x)). given clause #24: (wt=11) 175 [back_demod,144,demod,156,174,174,flip.1] x v f(y,c(y))=f(y,c(y)). given clause #25: (wt=11) 183 [back_demod,171,demod,174] x v (c(x) v y)=f(x,c(x)). given clause #26: (wt=13) 32 [copy,31,flip.1] c(x) v (y v c(z))=y v f(x,z). given clause #27: (wt=9) 237 [para_into,183,175,demod,176] f(x,c(x))=f(y,c(y)). given clause #28: (wt=7) 274 [copy,270,flip.1,demod,272] x v y=y v x. given clause #29: (wt=7) 283 [para_into,274,35,flip.1] c(c(x)) v x=x. given clause #30: (wt=7) 296 [para_into,274,17,demod,18] f(x,y)=f(y,x). given clause #31: (wt=13) 39 [para_into,21,17,demod,18,18] f(x,f(c(c(x)),f(x,y)))=f(x,y). given clause #32: (wt=8) 294 [para_into,274,19,flip.1] c(f(x,y)) v x=x. given clause #33: (wt=8) 330 [para_into,283,17] f(c(c(x)),x)=c(x). given clause #34: (wt=8) 361 [para_from,296,19] x v c(f(y,x))=x. given clause #35: (wt=8) 375 [para_into,294,296] c(f(x,y)) v y=y. given clause #36: (wt=17) 41 [para_into,21,8] x v c(f(c(x),y v (x v z)))=x v (y v z). given clause #37: (wt=9) 269 [para_from,237,145] f(x,f(y,c(y)))=c(x). given clause #38: (wt=9) 271 [para_from,237,19] x v c(f(y,c(y)))=x. given clause #39: (wt=9) 273 [copy,269,flip.1] c(x)=f(x,f(y,c(y))). given clause #40: (wt=9) 320 [para_into,283,54] x v f(c(x),c(x))=x. given clause #41: (wt=17) 45 [para_from,21,8,flip.1] x v (y v c(f(c(x),x v z)))=y v (x v z). given clause #42: (wt=9) 351 [para_into,296,29,flip.1] f(f(c(x),y),x)=c(x). given clause #43: (wt=9) 355 [para_from,296,29] f(x,f(y,c(x)))=c(x). given clause #44: (wt=9) 377 [para_into,294,237] c(f(x,c(x))) v y=y. given clause #45: (wt=9) 408 [para_from,330,29,flip.1] c(c(x))=f(c(x),c(x)). given clause #46: (wt=13) 55 [para_from,47,21,demod,48] x v c(f(c(x),y v x))=y v x. given clause #47: (wt=9) 444 [back_demod,283,demod,409] f(c(x),c(x)) v x=x. given clause #48: (wt=9) 480 [para_into,375,237,demod,18] f(f(x,c(x)),y)=c(y). given clause #49: (wt=9) 493 [para_into,375,17] f(f(x,c(y)),y)=c(y). given clause #50: (wt=9) 497 [copy,480,flip.1] c(x)=f(f(y,c(y)),x). given clause #51: (wt=21) 63 [para_into,25,21,flip.1] x v (y v (z v c(f(c(x),x v u))))=y v (z v (x v u)). given clause #52: (wt=10) 239 [para_into,183,53,demod,18] x v f(y,x)=f(x,c(x)). given clause #53: (wt=10) 243 [para_into,183,17] x v f(x,y)=f(x,c(x)). given clause #54: (wt=10) 247 [copy,239,flip.1] f(x,c(x))=x v f(y,x). given clause #55: (wt=10) 249 [copy,243,flip.1] f(x,c(x))=x v f(x,y). given clause #56: (wt=16) 65 [para_into,25,19,flip.1] x v (y v (z v c(f(x,u))))=y v (z v x). given clause #57: (wt=10) 379 [para_into,294,54] x v f(f(x,y),c(x))=x. given clause #58: (wt=10) 483 [para_into,375,54] x v f(f(y,x),c(x))=x. given clause #59: (wt=10) 822 [para_into,239,274] f(x,y) v y=f(y,c(y)). given clause #60: (wt=10) 825 [copy,822,flip.1] f(x,c(x))=f(y,x) v x. given clause #61: (wt=17) 67 [para_into,25,17] x v (y v f(z,u))=c(z) v (x v (y v c(u))). given clause #62: (wt=10) 836 [para_into,243,274] f(x,y) v x=f(x,c(x)). given clause #63: (wt=10) 839 [copy,836,flip.1] f(x,c(x))=f(x,y) v x. given clause #64: (wt=10) 853 [para_into,247,237] f(x,c(x))=y v f(z,y). given clause #65: (wt=10) 856 [copy,853,flip.1] x v f(y,x)=f(z,c(z)). given clause #66: (wt=19) 68 [para_into,25,8] x v (y v (z v (u v v)))=u v (x v (y v (z v v))). given clause #67: (wt=10) 862 [para_into,249,237] f(x,c(x))=y v f(y,z). given clause #68: (wt=10) 865 [copy,862,flip.1] x v f(x,y)=f(z,c(z)). given clause #69: (wt=10) 898 [para_into,379,296] x v f(c(x),f(x,y))=x. given clause #70: (wt=10) 900 [para_into,379,274] f(f(x,y),c(x)) v x=x. given clause #71: (wt=19) 69 [para_into,25,25] x v (y v (z v (u v v)))=u v (x v (z v (y v v))). given clause #72: (wt=10) 913 [para_into,483,296] x v f(c(x),f(y,x))=x. given clause #73: (wt=10) 915 [para_into,483,274] f(f(x,y),c(y)) v y=y. given clause #74: (wt=10) 951 [para_into,825,237] f(x,c(x))=f(y,z) v z. given clause #75: (wt=10) 954 [copy,951,flip.1] f(x,y) v y=f(z,c(z)). given clause #76: (wt=15) 70 [para_into,25,8] x v (y v (z v u))=z v (y v (x v u)). given clause #77: (wt=10) 1009 [para_into,839,237] f(x,c(x))=f(y,z) v y. given clause #78: (wt=10) 1012 [copy,1009,flip.1] f(x,y) v x=f(z,c(z)). given clause #79: (wt=10) 1022 [para_from,853,483,demod,409,463] f(x v f(y,x),z)=c(z). given clause #80: (wt=10) 1023 [para_from,853,361,demod,18] f(x,y v f(z,y))=c(x). given clause #81: (wt=17) 71 [copy,67,flip.1] c(x) v (y v (z v c(u)))=y v (z v f(x,u)). given clause #82: (wt=10) 1024 [para_from,853,271] x v c(y v f(z,y))=x. given clause #83: (wt=10) 1027 [para_from,853,377] c(x v f(y,x)) v z=z. given clause #84: (wt=10) 1033 [copy,1022,flip.1] c(x)=f(y v f(z,y),x). given clause #85: (wt=10) 1034 [copy,1023,flip.1] c(x)=f(x,y v f(z,y)). given clause #86: (wt=19) 72 [copy,68,flip.1] x v (y v (z v (u v v)))=y v (z v (u v (x v v))). given clause #87: (wt=10) 1089 [para_from,862,483,demod,409,463] f(x v f(x,y),z)=c(z). given clause #88: (wt=10) 1090 [para_from,862,361,demod,18] f(x,y v f(y,z))=c(x). given clause #89: (wt=10) 1091 [para_from,862,271] x v c(y v f(y,z))=x. given clause #90: (wt=10) 1094 [para_from,862,377] c(x v f(x,y)) v z=z. given clause #91: (wt=19) 73 [copy,69,flip.1] x v (y v (z v (u v v)))=y v (u v (z v (x v v))). given clause #92: (wt=10) 1101 [copy,1089,flip.1] c(x)=f(y v f(y,z),x). given clause #93: (wt=10) 1102 [copy,1090,flip.1] c(x)=f(x,y v f(y,z)). given clause #94: (wt=10) 1132 [para_into,898,274] f(c(x),f(x,y)) v x=x. given clause #95: (wt=10) 1196 [para_into,913,274] f(c(x),f(y,x)) v x=x. given clause #96: (wt=15) 74 [para_from,25,21,demod,42] x v (y v (z v u))=x v (z v (y v u)). given clause #97: (wt=10) 1244 [para_from,951,483,demod,409,463] f(f(x,y) v y,z)=c(z). given clause #98: (wt=10) 1245 [para_from,951,361,demod,18] f(x,f(y,z) v z)=c(x). given clause #99: (wt=10) 1246 [para_from,951,271] x v c(f(y,z) v z)=x. given clause #100: (wt=10) 1249 [para_from,951,377] c(f(x,y) v y) v z=z. given clause #101: (wt=19) 75 [para_from,25,8] x v (y v (z v (u v v)))=z v (x v (u v (y v v))). given clause #102: (wt=10) 1262 [copy,1244,flip.1] c(x)=f(f(y,z) v z,x). given clause #103: (wt=10) 1263 [copy,1245,flip.1] c(x)=f(x,f(y,z) v z). given clause #104: (wt=10) 1366 [para_from,1009,483,demod,409,463] f(f(x,y) v x,z)=c(z). given clause #105: (wt=10) 1367 [para_from,1009,361,demod,18] f(x,f(y,z) v y)=c(x). given clause #106: (wt=19) 76 [copy,75,flip.1] x v (y v (z v (u v v)))=y v (u v (x v (z v v))). given clause #107: (wt=10) 1368 [para_from,1009,271] x v c(f(y,z) v y)=x. given clause #108: (wt=10) 1371 [para_from,1009,377] c(f(x,y) v x) v z=z. given clause #109: (wt=10) 1385 [copy,1366,flip.1] c(x)=f(f(y,z) v y,x). given clause #110: (wt=10) 1386 [copy,1367,flip.1] c(x)=f(x,f(y,z) v y). given clause #111: (wt=19) 77 [para_from,53,25] x v (y v (c(z) v u))=u v (x v (y v f(z,c(u)))). given clause #112: (wt=11) 193 [back_demod,155,demod,174] c(x) v (y v x)=f(x,c(x)). given clause #113: (wt=11) 197 [back_demod,106,demod,174] c(x) v (x v y)=f(x,c(x)). given clause #114: (wt=11) 223 [para_from,173,8,demod,176,flip.1] x v (y v c(x))=f(x,c(x)). given clause #115: (wt=11) 275 [para_into,274,183,flip.1] (c(x) v y) v x=f(x,c(x)). given clause #116: (wt=15) 78 [para_from,53,8] x v (c(y) v z)=z v (x v f(y,c(z))). given clause #117: (wt=11) 277 [para_into,274,175,flip.1] f(x,c(x)) v y=f(x,c(x)). given clause #118: (wt=11) 279 [para_into,274,54] x v f(y,c(x))=x v c(y). given clause #119: (wt=11) 280 [para_into,274,53] c(x) v y=f(x,c(y)) v y. given clause #120: (wt=11) 297 [para_into,274,8] x v (y v z)= (x v z) v y. given clause #121: (wt=19) 79 [copy,77,flip.1] x v (y v (z v f(u,c(x))))=y v (z v (c(u) v x)). given clause #122: (wt=11) 298 [copy,279,flip.1] x v c(y)=x v f(y,c(x)). given clause #123: (wt=11) 299 [copy,280,flip.1] f(x,c(y)) v y=c(x) v y. given clause #124: (wt=11) 311 [para_from,274,8] x v (y v z)=z v (x v y). given clause #125: (wt=11) 319 [copy,311,flip.1] x v (y v z)=y v (z v x). given clause #126: (wt=15) 80 [copy,78,flip.1] x v (y v f(z,c(x)))=y v (c(z) v x). given clause #127: (wt=11) 353 [para_from,296,53] x v f(c(x),y)=c(y) v x. given clause #128: (wt=11) 363 [copy,353,flip.1] c(x) v y=y v f(c(y),x). given clause #129: (wt=11) 395 [para_from,294,27,demod,20,flip.1] c(f(c(f(x,y)),z)) v x=x. given clause #130: (wt=11) 501 [para_from,375,27,demod,20,flip.1] c(f(x,c(f(y,z)))) v y=y. given clause #131: (wt=19) 96 [para_from,54,25] x v (y v (z v f(u,c(z))))=c(u) v (x v (y v z)). given clause #132: (wt=11) 600 [para_into,45,27,demod,594,28] x v (y v z)=x v (z v y). given clause #133: (wt=11) 632 [para_into,377,271] c(f(x,c(x)))=c(f(y,c(y))). given clause #134: (wt=11) 633 [para_into,377,54] x v f(f(y,c(y)),c(x))=x. given clause #135: (wt=11) 1016 [para_into,853,853] x v f(y,x)=z v f(u,z). given clause #136: (wt=15) 98 [para_from,54,8] x v (y v f(z,c(y)))=c(z) v (x v y). given clause #137: (wt=11) 1080 [para_into,862,862] x v f(x,y)=z v f(z,u). given clause #138: (wt=11) 1081 [para_into,862,853] x v f(y,x)=z v f(z,u). given clause #139: (wt=11) 1086 [copy,1081,flip.1] x v f(x,y)=z v f(u,z). given clause #140: (wt=11) 1130 [para_into,898,237] x v f(c(x),f(y,c(y)))=x. given clause #141: (wt=19) 100 [copy,96,flip.1] c(x) v (y v (z v u))=y v (z v (u v f(x,c(u)))). given clause #142: (wt=11) 1231 [para_into,951,951] f(x,y) v y=f(z,u) v u. given clause #143: (wt=11) 1232 [para_into,951,862] x v f(x,y)=f(z,u) v u. given clause #144: (wt=11) 1233 [para_into,951,853] x v f(y,x)=f(z,u) v u. given clause #145: (wt=11) 1238 [copy,1232,flip.1] f(x,y) v y=z v f(z,u). given clause #146: (wt=15) 102 [copy,98,flip.1] c(x) v (y v z)=y v (z v f(x,c(z))). given clause #147: (wt=11) 1239 [copy,1233,flip.1] f(x,y) v y=z v f(u,z). given clause #148: (wt=11) 1314 [para_into,70,271,demod,272] x v (y v z)=z v (y v x). given clause #149: (wt=11) 1351 [para_into,1009,1009] f(x,y) v x=f(z,u) v z. given clause #150: (wt=11) 1352 [para_into,1009,951] f(x,y) v y=f(z,u) v z. given clause #151: (wt=12) 103 [para_into,27,54,demod,92] x v f(y,f(x,z))=c(y) v x. given clause #152: (wt=11) 1353 [para_into,1009,862] x v f(x,y)=f(z,u) v z. given clause #153: (wt=11) 1354 [para_into,1009,853] x v f(y,x)=f(z,u) v z. given clause #154: (wt=11) 1359 [copy,1352,flip.1] f(x,y) v x=f(z,u) v u. given clause #155: (wt=11) 1360 [copy,1353,flip.1] f(x,y) v x=z v f(z,u). given clause #156: (wt=12) 108 [copy,103,flip.1] c(x) v y=y v f(x,f(y,z)). given clause #157: (wt=11) 1361 [copy,1354,flip.1] f(x,y) v x=z v f(u,z). given clause #158: (wt=11) 2140 [para_into,1132,237] f(c(x),f(y,c(y))) v x=x. given clause #159: (wt=11) 3290 [para_into,279,296] x v f(c(x),y)=x v c(y). ----> UNIT CONFLICT at 0.96 sec ----> 5842 [binary,5840,6] $Ans(DEF_C). Length of proof is 52. Level of proof is 17. ---------------- PROOF ---------------- 6 [] c(A)!=f(A,A)|$Ans(DEF_C). 8 [] x v (y v z)=y v (x v z). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 13 [] x v (c(x)^ (x v y))=x v y. 14 [copy,13,demod,12] x v c(c(c(x)) v c(x v y))=x v y. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 20,19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 21 [back_demod,14,demod,18] x v c(f(c(x),x v y))=x v y. 25 [para_into,8,8] x v (y v (z v u))=z v (x v (y v u)). 27 [para_from,19,8,flip.1] x v (y v c(f(x,z)))=y v x. 29 [para_into,17,19,flip.1] f(x,f(c(x),y))=c(x). 31 [para_from,17,8] x v f(y,z)=c(y) v (x v c(z)). 32 [copy,31,flip.1] c(x) v (y v c(z))=y v f(x,z). 35 [para_from,29,19] x v c(c(x))=x. 37 [para_into,21,19,demod,20] x v c(f(c(x),x))=x. 47 [para_from,35,8,flip.1] x v (y v c(c(x)))=y v x. 53 [para_into,47,17] x v f(y,c(x))=c(y) v x. 54 [copy,53,flip.1] c(x) v y=y v f(x,c(y)). 104 [para_into,27,37] c(x) v x=x v c(x). 107,106 [para_into,27,21] c(x) v (x v y)=x v c(x). 140 [para_from,104,8] x v (y v c(y))=c(y) v (x v y). 144 [copy,140,flip.1] c(x) v (y v x)=y v (x v c(x)). 149 [para_into,106,106,demod,18] c(c(x)) v (x v c(x))=f(x,c(x)). 156,155 [para_into,106,47] c(x) v (y v x)=x v c(x). 170,169 [para_into,106,25,demod,107] x v (y v c(y))=y v c(y). 171 [para_into,106,8] x v (c(x) v y)=x v c(x). 174,173 [back_demod,149,demod,170] x v c(x)=f(x,c(x)). 176,175 [back_demod,144,demod,156,174,174,flip.1] x v f(y,c(y))=f(y,c(y)). 183 [back_demod,171,demod,174] x v (c(x) v y)=f(x,c(x)). 237 [para_into,183,175,demod,176] f(x,c(x))=f(y,c(y)). 270 [para_from,237,27] x v (y v c(f(z,c(z))))=y v x. 272,271 [para_from,237,19] x v c(f(y,c(y)))=x. 274 [copy,270,flip.1,demod,272] x v y=y v x. 279 [para_into,274,54] x v f(y,c(x))=x v c(y). 283 [para_into,274,35,flip.1] c(c(x)) v x=x. 294 [para_into,274,19,flip.1] c(f(x,y)) v x=x. 296 [para_into,274,17,demod,18] f(x,y)=f(y,x). 330 [para_into,283,17] f(c(c(x)),x)=c(x). 352,351 [para_into,296,29,flip.1] f(f(c(x),y),x)=c(x). 353 [para_from,296,53] x v f(c(x),y)=c(y) v x. 363 [copy,353,flip.1] c(x) v y=y v f(c(y),x). 375 [para_into,294,296] c(f(x,y)) v y=y. 378,377 [para_into,294,237] c(f(x,c(x))) v y=y. 379 [para_into,294,54] x v f(f(x,y),c(x))=x. 409,408 [para_from,330,29,flip.1] c(c(x))=f(c(x),c(x)). 480 [para_into,375,237,demod,18] f(f(x,c(x)),y)=c(y). 497 [copy,480,flip.1] c(x)=f(f(y,c(y)),x). 643 [para_into,377,21,demod,378,409,378,flip.1] c(f(f(c(f(x,c(x))),c(f(x,c(x)))),y))=y. 766,765 [para_from,497,408] c(f(f(x,c(x)),y))=f(c(y),c(y)). 900 [para_into,379,274] f(f(x,y),c(x)) v x=x. 1162,1161 [para_from,900,32,demod,18,409,flip.1] f(f(c(x),y),f(c(x),c(x))) v f(z,x)=f(z,x). 3290 [para_into,279,296] x v f(c(x),y)=x v c(y). 4012 [para_into,363,379,demod,409,409,1162,flip.1] f(c(f(f(c(x),y),f(c(x),c(x)))),x)=c(x). 5787,5786 [para_into,3290,377,demod,409,18] f(f(c(f(x,c(x))),c(f(x,c(x)))),y)=f(f(x,c(x)),y). 5806,5805 [back_demod,643,demod,5787,766] f(c(x),c(x))=x. 5840 [back_demod,4012,demod,5806,352,409,5806,flip.1] c(x)=f(x,x). 5842 [binary,5840,6] $Ans(DEF_C). ------------ end of proof ------------- ----> UNIT CONFLICT at 2.14 sec ----> 7709 [binary,7707,2] $Ans(B_SS). Length of proof is 61. Level of proof is 20. ---------------- PROOF ---------------- 2 [] f(f(A,A),f(A,B))!=A|$Ans(B_SS). 8 [] x v (y v z)=y v (x v z). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 13 [] x v (c(x)^ (x v y))=x v y. 14 [copy,13,demod,12] x v c(c(c(x)) v c(x v y))=x v y. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 20,19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 21 [back_demod,14,demod,18] x v c(f(c(x),x v y))=x v y. 25 [para_into,8,8] x v (y v (z v u))=z v (x v (y v u)). 27 [para_from,19,8,flip.1] x v (y v c(f(x,z)))=y v x. 29 [para_into,17,19,flip.1] f(x,f(c(x),y))=c(x). 31 [para_from,17,8] x v f(y,z)=c(y) v (x v c(z)). 32 [copy,31,flip.1] c(x) v (y v c(z))=y v f(x,z). 35 [para_from,29,19] x v c(c(x))=x. 37 [para_into,21,19,demod,20] x v c(f(c(x),x))=x. 47 [para_from,35,8,flip.1] x v (y v c(c(x)))=y v x. 53 [para_into,47,17] x v f(y,c(x))=c(y) v x. 54 [copy,53,flip.1] c(x) v y=y v f(x,c(y)). 104 [para_into,27,37] c(x) v x=x v c(x). 107,106 [para_into,27,21] c(x) v (x v y)=x v c(x). 140 [para_from,104,8] x v (y v c(y))=c(y) v (x v y). 144 [copy,140,flip.1] c(x) v (y v x)=y v (x v c(x)). 149 [para_into,106,106,demod,18] c(c(x)) v (x v c(x))=f(x,c(x)). 156,155 [para_into,106,47] c(x) v (y v x)=x v c(x). 170,169 [para_into,106,25,demod,107] x v (y v c(y))=y v c(y). 171 [para_into,106,8] x v (c(x) v y)=x v c(x). 174,173 [back_demod,149,demod,170] x v c(x)=f(x,c(x)). 176,175 [back_demod,144,demod,156,174,174,flip.1] x v f(y,c(y))=f(y,c(y)). 183 [back_demod,171,demod,174] x v (c(x) v y)=f(x,c(x)). 237 [para_into,183,175,demod,176] f(x,c(x))=f(y,c(y)). 270 [para_from,237,27] x v (y v c(f(z,c(z))))=y v x. 272,271 [para_from,237,19] x v c(f(y,c(y)))=x. 274 [copy,270,flip.1,demod,272] x v y=y v x. 279 [para_into,274,54] x v f(y,c(x))=x v c(y). 283 [para_into,274,35,flip.1] c(c(x)) v x=x. 294 [para_into,274,19,flip.1] c(f(x,y)) v x=x. 296 [para_into,274,17,demod,18] f(x,y)=f(y,x). 330 [para_into,283,17] f(c(c(x)),x)=c(x). 352,351 [para_into,296,29,flip.1] f(f(c(x),y),x)=c(x). 353 [para_from,296,53] x v f(c(x),y)=c(y) v x. 363 [copy,353,flip.1] c(x) v y=y v f(c(y),x). 375 [para_into,294,296] c(f(x,y)) v y=y. 378,377 [para_into,294,237] c(f(x,c(x))) v y=y. 379 [para_into,294,54] x v f(f(x,y),c(x))=x. 409,408 [para_from,330,29,flip.1] c(c(x))=f(c(x),c(x)). 480 [para_into,375,237,demod,18] f(f(x,c(x)),y)=c(y). 497 [copy,480,flip.1] c(x)=f(f(y,c(y)),x). 643 [para_into,377,21,demod,378,409,378,flip.1] c(f(f(c(f(x,c(x))),c(f(x,c(x)))),y))=y. 766,765 [para_from,497,408] c(f(f(x,c(x)),y))=f(c(y),c(y)). 898 [para_into,379,296] x v f(c(x),f(x,y))=x. 900 [para_into,379,274] f(f(x,y),c(x)) v x=x. 1132 [para_into,898,274] f(c(x),f(x,y)) v x=x. 1162,1161 [para_from,900,32,demod,18,409,flip.1] f(f(c(x),y),f(c(x),c(x))) v f(z,x)=f(z,x). 2138 [para_into,1132,351] f(c(f(c(x),y)),c(x)) v f(c(x),y)=f(c(x),y). 3290 [para_into,279,296] x v f(c(x),y)=x v c(y). 4012 [para_into,363,379,demod,409,409,1162,flip.1] f(c(f(f(c(x),y),f(c(x),c(x)))),x)=c(x). 5787,5786 [para_into,3290,377,demod,409,18] f(f(c(f(x,c(x))),c(f(x,c(x)))),y)=f(f(x,c(x)),y). 5788 [para_into,3290,274] f(c(x),y) v x=x v c(y). 5806,5805 [back_demod,643,demod,5787,766] f(c(x),c(x))=x. 5807 [copy,5788,flip.1] x v c(y)=f(c(x),y) v x. 5841,5840 [back_demod,4012,demod,5806,352,409,5806,flip.1] c(x)=f(x,x). 5963,5962 [copy,5807,flip.1,demod,5841,5841] f(f(x,x),y) v x=x v f(y,y). 5995,5994 [back_demod,5805,demod,5841,5841] f(f(x,x),f(x,x))=x. 7277,7276 [back_demod,2138,demod,5841,5841,5841,5841,5963,5995,5963,5841] x v f(y,y)=f(f(x,x),y). 7707 [back_demod,1132,demod,5841,5963,7277] f(f(x,x),f(x,y))=x. 7709 [binary,7707,2] $Ans(B_SS). ------------ end of proof ------------- ----> UNIT CONFLICT at 2.46 sec ----> 7962 [binary,7960,4] $Ans(DEF_J). Length of proof is 73. Level of proof is 22. ---------------- PROOF ---------------- 4 [] A v B!=f(f(A,A),f(B,B))|$Ans(DEF_J). 8 [] x v (y v z)=y v (x v z). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 13 [] x v (c(x)^ (x v y))=x v y. 14 [copy,13,demod,12] x v c(c(c(x)) v c(x v y))=x v y. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 20,19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 21 [back_demod,14,demod,18] x v c(f(c(x),x v y))=x v y. 25 [para_into,8,8] x v (y v (z v u))=z v (x v (y v u)). 27 [para_from,19,8,flip.1] x v (y v c(f(x,z)))=y v x. 29 [para_into,17,19,flip.1] f(x,f(c(x),y))=c(x). 31 [para_from,17,8] x v f(y,z)=c(y) v (x v c(z)). 32 [copy,31,flip.1] c(x) v (y v c(z))=y v f(x,z). 35 [para_from,29,19] x v c(c(x))=x. 37 [para_into,21,19,demod,20] x v c(f(c(x),x))=x. 47 [para_from,35,8,flip.1] x v (y v c(c(x)))=y v x. 53 [para_into,47,17] x v f(y,c(x))=c(y) v x. 54 [copy,53,flip.1] c(x) v y=y v f(x,c(y)). 104 [para_into,27,37] c(x) v x=x v c(x). 107,106 [para_into,27,21] c(x) v (x v y)=x v c(x). 140 [para_from,104,8] x v (y v c(y))=c(y) v (x v y). 144 [copy,140,flip.1] c(x) v (y v x)=y v (x v c(x)). 149 [para_into,106,106,demod,18] c(c(x)) v (x v c(x))=f(x,c(x)). 156,155 [para_into,106,47] c(x) v (y v x)=x v c(x). 170,169 [para_into,106,25,demod,107] x v (y v c(y))=y v c(y). 171 [para_into,106,8] x v (c(x) v y)=x v c(x). 174,173 [back_demod,149,demod,170] x v c(x)=f(x,c(x)). 176,175 [back_demod,144,demod,156,174,174,flip.1] x v f(y,c(y))=f(y,c(y)). 183 [back_demod,171,demod,174] x v (c(x) v y)=f(x,c(x)). 237 [para_into,183,175,demod,176] f(x,c(x))=f(y,c(y)). 270 [para_from,237,27] x v (y v c(f(z,c(z))))=y v x. 272,271 [para_from,237,19] x v c(f(y,c(y)))=x. 274 [copy,270,flip.1,demod,272] x v y=y v x. 279 [para_into,274,54] x v f(y,c(x))=x v c(y). 280 [para_into,274,53] c(x) v y=f(x,c(y)) v y. 283 [para_into,274,35,flip.1] c(c(x)) v x=x. 294 [para_into,274,19,flip.1] c(f(x,y)) v x=x. 296 [para_into,274,17,demod,18] f(x,y)=f(y,x). 306 [para_from,274,27] x v (c(f(x,y)) v z)=z v x. 314 [copy,306,flip.1] x v y=y v (c(f(y,z)) v x). 330 [para_into,283,17] f(c(c(x)),x)=c(x). 352,351 [para_into,296,29,flip.1] f(f(c(x),y),x)=c(x). 353 [para_from,296,53] x v f(c(x),y)=c(y) v x. 354 [para_from,296,31] x v f(y,z)=c(z) v (x v c(y)). 363 [copy,353,flip.1] c(x) v y=y v f(c(y),x). 375 [para_into,294,296] c(f(x,y)) v y=y. 378,377 [para_into,294,237] c(f(x,c(x))) v y=y. 379 [para_into,294,54] x v f(f(x,y),c(x))=x. 409,408 [para_from,330,29,flip.1] c(c(x))=f(c(x),c(x)). 480 [para_into,375,237,demod,18] f(f(x,c(x)),y)=c(y). 493 [para_into,375,17] f(f(x,c(y)),y)=c(y). 497 [copy,480,flip.1] c(x)=f(f(y,c(y)),x). 643 [para_into,377,21,demod,378,409,378,flip.1] c(f(f(c(f(x,c(x))),c(f(x,c(x)))),y))=y. 766,765 [para_from,497,408] c(f(f(x,c(x)),y))=f(c(y),c(y)). 898 [para_into,379,296] x v f(c(x),f(x,y))=x. 900 [para_into,379,274] f(f(x,y),c(x)) v x=x. 1132 [para_into,898,274] f(c(x),f(x,y)) v x=x. 1162,1161 [para_from,900,32,demod,18,409,flip.1] f(f(c(x),y),f(c(x),c(x))) v f(z,x)=f(z,x). 2136 [para_into,1132,493] f(c(f(x,c(y))),c(y)) v f(x,c(y))=f(x,c(y)). 2138 [para_into,1132,351] f(c(f(c(x),y)),c(x)) v f(c(x),y)=f(c(x),y). 3290 [para_into,279,296] x v f(c(x),y)=x v c(y). 4012 [para_into,363,379,demod,409,409,1162,flip.1] f(c(f(f(c(x),y),f(c(x),c(x)))),x)=c(x). 4016 [para_into,363,280] f(x,c(y)) v y=y v f(c(y),x). 5787,5786 [para_into,3290,377,demod,409,18] f(f(c(f(x,c(x))),c(f(x,c(x)))),y)=f(f(x,c(x)),y). 5788 [para_into,3290,274] f(c(x),y) v x=x v c(y). 5806,5805 [back_demod,643,demod,5787,766] f(c(x),c(x))=x. 5807 [copy,5788,flip.1] x v c(y)=f(c(x),y) v x. 5841,5840 [back_demod,4012,demod,5806,352,409,5806,flip.1] c(x)=f(x,x). 5963,5962 [copy,5807,flip.1,demod,5841,5841] f(f(x,x),y) v x=x v f(y,y). 5995,5994 [back_demod,5805,demod,5841,5841] f(f(x,x),f(x,x))=x. 6607,6606 [back_demod,4016,demod,5841,5841] f(x,f(y,y)) v y=y v f(f(y,y),x). 7277,7276 [back_demod,2138,demod,5841,5841,5841,5841,5963,5995,5963,5841] x v f(y,y)=f(f(x,x),y). 7279,7278 [back_demod,2136,demod,5841,5841,5841,5841,5963,5995,6607,5841] x v f(f(x,x),y)=f(y,f(x,x)). 7708,7707 [back_demod,1132,demod,5841,5963,7277] f(f(x,x),f(x,y))=x. 7950,7949 [back_demod,363,demod,5841,5841,7279] f(x,x) v y=f(x,f(y,y)). 7957,7956 [back_demod,354,demod,5841,5841,7277,7950] x v f(y,z)=f(z,f(f(f(x,x),y),f(f(x,x),y))). 7960 [back_demod,314,demod,5841,7950,7957,7708,7708] x v y=f(f(x,x),f(y,y)). 7962 [binary,7960,4] $Ans(DEF_J). ------------ end of proof ------------- ----> UNIT CONFLICT at 2.49 sec ----> 7968 [binary,7967,1] $Ans(A_SS). Length of proof is 76. Level of proof is 23. ---------------- PROOF ---------------- 1 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C)))|$Ans(A_SS). 8 [] x v (y v z)=y v (x v z). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 13 [] x v (c(x)^ (x v y))=x v y. 14 [copy,13,demod,12] x v c(c(c(x)) v c(x v y))=x v y. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 20,19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 21 [back_demod,14,demod,18] x v c(f(c(x),x v y))=x v y. 25 [para_into,8,8] x v (y v (z v u))=z v (x v (y v u)). 27 [para_from,19,8,flip.1] x v (y v c(f(x,z)))=y v x. 29 [para_into,17,19,flip.1] f(x,f(c(x),y))=c(x). 31 [para_from,17,8] x v f(y,z)=c(y) v (x v c(z)). 32 [copy,31,flip.1] c(x) v (y v c(z))=y v f(x,z). 35 [para_from,29,19] x v c(c(x))=x. 37 [para_into,21,19,demod,20] x v c(f(c(x),x))=x. 47 [para_from,35,8,flip.1] x v (y v c(c(x)))=y v x. 53 [para_into,47,17] x v f(y,c(x))=c(y) v x. 54 [copy,53,flip.1] c(x) v y=y v f(x,c(y)). 92,91 [para_into,54,17,flip.1] c(x) v f(y,c(c(x)))=f(y,x). 104 [para_into,27,37] c(x) v x=x v c(x). 107,106 [para_into,27,21] c(x) v (x v y)=x v c(x). 140 [para_from,104,8] x v (y v c(y))=c(y) v (x v y). 144 [copy,140,flip.1] c(x) v (y v x)=y v (x v c(x)). 149 [para_into,106,106,demod,18] c(c(x)) v (x v c(x))=f(x,c(x)). 156,155 [para_into,106,47] c(x) v (y v x)=x v c(x). 170,169 [para_into,106,25,demod,107] x v (y v c(y))=y v c(y). 171 [para_into,106,8] x v (c(x) v y)=x v c(x). 174,173 [back_demod,149,demod,170] x v c(x)=f(x,c(x)). 176,175 [back_demod,144,demod,156,174,174,flip.1] x v f(y,c(y))=f(y,c(y)). 183 [back_demod,171,demod,174] x v (c(x) v y)=f(x,c(x)). 237 [para_into,183,175,demod,176] f(x,c(x))=f(y,c(y)). 252 [para_into,32,54,demod,92] c(x) v f(y,z)=c(y) v f(x,z). 270 [para_from,237,27] x v (y v c(f(z,c(z))))=y v x. 272,271 [para_from,237,19] x v c(f(y,c(y)))=x. 274 [copy,270,flip.1,demod,272] x v y=y v x. 279 [para_into,274,54] x v f(y,c(x))=x v c(y). 280 [para_into,274,53] c(x) v y=f(x,c(y)) v y. 283 [para_into,274,35,flip.1] c(c(x)) v x=x. 294 [para_into,274,19,flip.1] c(f(x,y)) v x=x. 296 [para_into,274,17,demod,18] f(x,y)=f(y,x). 306 [para_from,274,27] x v (c(f(x,y)) v z)=z v x. 314 [copy,306,flip.1] x v y=y v (c(f(y,z)) v x). 330 [para_into,283,17] f(c(c(x)),x)=c(x). 352,351 [para_into,296,29,flip.1] f(f(c(x),y),x)=c(x). 353 [para_from,296,53] x v f(c(x),y)=c(y) v x. 354 [para_from,296,31] x v f(y,z)=c(z) v (x v c(y)). 363 [copy,353,flip.1] c(x) v y=y v f(c(y),x). 375 [para_into,294,296] c(f(x,y)) v y=y. 378,377 [para_into,294,237] c(f(x,c(x))) v y=y. 379 [para_into,294,54] x v f(f(x,y),c(x))=x. 409,408 [para_from,330,29,flip.1] c(c(x))=f(c(x),c(x)). 480 [para_into,375,237,demod,18] f(f(x,c(x)),y)=c(y). 493 [para_into,375,17] f(f(x,c(y)),y)=c(y). 497 [copy,480,flip.1] c(x)=f(f(y,c(y)),x). 643 [para_into,377,21,demod,378,409,378,flip.1] c(f(f(c(f(x,c(x))),c(f(x,c(x)))),y))=y. 766,765 [para_from,497,408] c(f(f(x,c(x)),y))=f(c(y),c(y)). 898 [para_into,379,296] x v f(c(x),f(x,y))=x. 900 [para_into,379,274] f(f(x,y),c(x)) v x=x. 1132 [para_into,898,274] f(c(x),f(x,y)) v x=x. 1162,1161 [para_from,900,32,demod,18,409,flip.1] f(f(c(x),y),f(c(x),c(x))) v f(z,x)=f(z,x). 2136 [para_into,1132,493] f(c(f(x,c(y))),c(y)) v f(x,c(y))=f(x,c(y)). 2138 [para_into,1132,351] f(c(f(c(x),y)),c(x)) v f(c(x),y)=f(c(x),y). 3290 [para_into,279,296] x v f(c(x),y)=x v c(y). 4012 [para_into,363,379,demod,409,409,1162,flip.1] f(c(f(f(c(x),y),f(c(x),c(x)))),x)=c(x). 4016 [para_into,363,280] f(x,c(y)) v y=y v f(c(y),x). 5787,5786 [para_into,3290,377,demod,409,18] f(f(c(f(x,c(x))),c(f(x,c(x)))),y)=f(f(x,c(x)),y). 5788 [para_into,3290,274] f(c(x),y) v x=x v c(y). 5806,5805 [back_demod,643,demod,5787,766] f(c(x),c(x))=x. 5807 [copy,5788,flip.1] x v c(y)=f(c(x),y) v x. 5841,5840 [back_demod,4012,demod,5806,352,409,5806,flip.1] c(x)=f(x,x). 5963,5962 [copy,5807,flip.1,demod,5841,5841] f(f(x,x),y) v x=x v f(y,y). 5995,5994 [back_demod,5805,demod,5841,5841] f(f(x,x),f(x,x))=x. 6607,6606 [back_demod,4016,demod,5841,5841] f(x,f(y,y)) v y=y v f(f(y,y),x). 7277,7276 [back_demod,2138,demod,5841,5841,5841,5841,5963,5995,5963,5841] x v f(y,y)=f(f(x,x),y). 7279,7278 [back_demod,2136,demod,5841,5841,5841,5841,5963,5995,6607,5841] x v f(f(x,x),y)=f(y,f(x,x)). 7708,7707 [back_demod,1132,demod,5841,5963,7277] f(f(x,x),f(x,y))=x. 7950,7949 [back_demod,363,demod,5841,5841,7279] f(x,x) v y=f(x,f(y,y)). 7957,7956 [back_demod,354,demod,5841,5841,7277,7950] x v f(y,z)=f(z,f(f(f(x,x),y),f(f(x,x),y))). 7961,7960 [back_demod,314,demod,5841,7950,7957,7708,7708] x v y=f(f(x,x),f(y,y)). 7967 [back_demod,252,demod,5841,7961,5995,5841,7961,5995] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 7968 [binary,7967,1] $Ans(A_SS). ------------ end of proof ------------- ----> UNIT CONFLICT at 2.58 sec ----> 7979 [binary,7977,5] $Ans(DEF_M). Length of proof is 54. Level of proof is 18. ---------------- PROOF ---------------- 5 [] A^B!=f(f(A,B),f(A,B))|$Ans(DEF_M). 8 [] x v (y v z)=y v (x v z). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 13 [] x v (c(x)^ (x v y))=x v y. 14 [copy,13,demod,12] x v c(c(c(x)) v c(x v y))=x v y. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 20,19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 21 [back_demod,14,demod,18] x v c(f(c(x),x v y))=x v y. 23 [back_demod,11,demod,18] x^y=c(f(x,y)). 25 [para_into,8,8] x v (y v (z v u))=z v (x v (y v u)). 27 [para_from,19,8,flip.1] x v (y v c(f(x,z)))=y v x. 29 [para_into,17,19,flip.1] f(x,f(c(x),y))=c(x). 31 [para_from,17,8] x v f(y,z)=c(y) v (x v c(z)). 32 [copy,31,flip.1] c(x) v (y v c(z))=y v f(x,z). 35 [para_from,29,19] x v c(c(x))=x. 37 [para_into,21,19,demod,20] x v c(f(c(x),x))=x. 47 [para_from,35,8,flip.1] x v (y v c(c(x)))=y v x. 53 [para_into,47,17] x v f(y,c(x))=c(y) v x. 54 [copy,53,flip.1] c(x) v y=y v f(x,c(y)). 104 [para_into,27,37] c(x) v x=x v c(x). 107,106 [para_into,27,21] c(x) v (x v y)=x v c(x). 140 [para_from,104,8] x v (y v c(y))=c(y) v (x v y). 144 [copy,140,flip.1] c(x) v (y v x)=y v (x v c(x)). 149 [para_into,106,106,demod,18] c(c(x)) v (x v c(x))=f(x,c(x)). 156,155 [para_into,106,47] c(x) v (y v x)=x v c(x). 170,169 [para_into,106,25,demod,107] x v (y v c(y))=y v c(y). 171 [para_into,106,8] x v (c(x) v y)=x v c(x). 174,173 [back_demod,149,demod,170] x v c(x)=f(x,c(x)). 176,175 [back_demod,144,demod,156,174,174,flip.1] x v f(y,c(y))=f(y,c(y)). 183 [back_demod,171,demod,174] x v (c(x) v y)=f(x,c(x)). 237 [para_into,183,175,demod,176] f(x,c(x))=f(y,c(y)). 270 [para_from,237,27] x v (y v c(f(z,c(z))))=y v x. 272,271 [para_from,237,19] x v c(f(y,c(y)))=x. 274 [copy,270,flip.1,demod,272] x v y=y v x. 279 [para_into,274,54] x v f(y,c(x))=x v c(y). 283 [para_into,274,35,flip.1] c(c(x)) v x=x. 294 [para_into,274,19,flip.1] c(f(x,y)) v x=x. 296 [para_into,274,17,demod,18] f(x,y)=f(y,x). 330 [para_into,283,17] f(c(c(x)),x)=c(x). 352,351 [para_into,296,29,flip.1] f(f(c(x),y),x)=c(x). 353 [para_from,296,53] x v f(c(x),y)=c(y) v x. 363 [copy,353,flip.1] c(x) v y=y v f(c(y),x). 375 [para_into,294,296] c(f(x,y)) v y=y. 378,377 [para_into,294,237] c(f(x,c(x))) v y=y. 379 [para_into,294,54] x v f(f(x,y),c(x))=x. 409,408 [para_from,330,29,flip.1] c(c(x))=f(c(x),c(x)). 480 [para_into,375,237,demod,18] f(f(x,c(x)),y)=c(y). 497 [copy,480,flip.1] c(x)=f(f(y,c(y)),x). 643 [para_into,377,21,demod,378,409,378,flip.1] c(f(f(c(f(x,c(x))),c(f(x,c(x)))),y))=y. 766,765 [para_from,497,408] c(f(f(x,c(x)),y))=f(c(y),c(y)). 900 [para_into,379,274] f(f(x,y),c(x)) v x=x. 1162,1161 [para_from,900,32,demod,18,409,flip.1] f(f(c(x),y),f(c(x),c(x))) v f(z,x)=f(z,x). 3290 [para_into,279,296] x v f(c(x),y)=x v c(y). 4012 [para_into,363,379,demod,409,409,1162,flip.1] f(c(f(f(c(x),y),f(c(x),c(x)))),x)=c(x). 5787,5786 [para_into,3290,377,demod,409,18] f(f(c(f(x,c(x))),c(f(x,c(x)))),y)=f(f(x,c(x)),y). 5806,5805 [back_demod,643,demod,5787,766] f(c(x),c(x))=x. 5841,5840 [back_demod,4012,demod,5806,352,409,5806,flip.1] c(x)=f(x,x). 7977 [back_demod,23,demod,5841] x^y=f(f(x,y),f(x,y)). 7979 [binary,7977,5] $Ans(DEF_M). ------------ end of proof ------------- ----> UNIT CONFLICT at 2.64 sec ----> 8026 [binary,8024,3] $Ans(OM_SS). Length of proof is 57. Level of proof is 19. ---------------- PROOF ---------------- 3 [] f(A,f(A,f(A,B)))!=f(A,B)|$Ans(OM_SS). 8 [] x v (y v z)=y v (x v z). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 13 [] x v (c(x)^ (x v y))=x v y. 14 [copy,13,demod,12] x v c(c(c(x)) v c(x v y))=x v y. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 20,19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 21 [back_demod,14,demod,18] x v c(f(c(x),x v y))=x v y. 25 [para_into,8,8] x v (y v (z v u))=z v (x v (y v u)). 27 [para_from,19,8,flip.1] x v (y v c(f(x,z)))=y v x. 29 [para_into,17,19,flip.1] f(x,f(c(x),y))=c(x). 31 [para_from,17,8] x v f(y,z)=c(y) v (x v c(z)). 32 [copy,31,flip.1] c(x) v (y v c(z))=y v f(x,z). 35 [para_from,29,19] x v c(c(x))=x. 37 [para_into,21,19,demod,20] x v c(f(c(x),x))=x. 39 [para_into,21,17,demod,18,18] f(x,f(c(c(x)),f(x,y)))=f(x,y). 47 [para_from,35,8,flip.1] x v (y v c(c(x)))=y v x. 53 [para_into,47,17] x v f(y,c(x))=c(y) v x. 54 [copy,53,flip.1] c(x) v y=y v f(x,c(y)). 104 [para_into,27,37] c(x) v x=x v c(x). 107,106 [para_into,27,21] c(x) v (x v y)=x v c(x). 140 [para_from,104,8] x v (y v c(y))=c(y) v (x v y). 144 [copy,140,flip.1] c(x) v (y v x)=y v (x v c(x)). 149 [para_into,106,106,demod,18] c(c(x)) v (x v c(x))=f(x,c(x)). 156,155 [para_into,106,47] c(x) v (y v x)=x v c(x). 170,169 [para_into,106,25,demod,107] x v (y v c(y))=y v c(y). 171 [para_into,106,8] x v (c(x) v y)=x v c(x). 174,173 [back_demod,149,demod,170] x v c(x)=f(x,c(x)). 176,175 [back_demod,144,demod,156,174,174,flip.1] x v f(y,c(y))=f(y,c(y)). 183 [back_demod,171,demod,174] x v (c(x) v y)=f(x,c(x)). 237 [para_into,183,175,demod,176] f(x,c(x))=f(y,c(y)). 270 [para_from,237,27] x v (y v c(f(z,c(z))))=y v x. 272,271 [para_from,237,19] x v c(f(y,c(y)))=x. 274 [copy,270,flip.1,demod,272] x v y=y v x. 279 [para_into,274,54] x v f(y,c(x))=x v c(y). 283 [para_into,274,35,flip.1] c(c(x)) v x=x. 294 [para_into,274,19,flip.1] c(f(x,y)) v x=x. 296 [para_into,274,17,demod,18] f(x,y)=f(y,x). 330 [para_into,283,17] f(c(c(x)),x)=c(x). 352,351 [para_into,296,29,flip.1] f(f(c(x),y),x)=c(x). 353 [para_from,296,53] x v f(c(x),y)=c(y) v x. 363 [copy,353,flip.1] c(x) v y=y v f(c(y),x). 375 [para_into,294,296] c(f(x,y)) v y=y. 378,377 [para_into,294,237] c(f(x,c(x))) v y=y. 379 [para_into,294,54] x v f(f(x,y),c(x))=x. 409,408 [para_from,330,29,flip.1] c(c(x))=f(c(x),c(x)). 472 [back_demod,39,demod,409] f(x,f(f(c(x),c(x)),f(x,y)))=f(x,y). 480 [para_into,375,237,demod,18] f(f(x,c(x)),y)=c(y). 497 [copy,480,flip.1] c(x)=f(f(y,c(y)),x). 643 [para_into,377,21,demod,378,409,378,flip.1] c(f(f(c(f(x,c(x))),c(f(x,c(x)))),y))=y. 766,765 [para_from,497,408] c(f(f(x,c(x)),y))=f(c(y),c(y)). 900 [para_into,379,274] f(f(x,y),c(x)) v x=x. 1162,1161 [para_from,900,32,demod,18,409,flip.1] f(f(c(x),y),f(c(x),c(x))) v f(z,x)=f(z,x). 3290 [para_into,279,296] x v f(c(x),y)=x v c(y). 4012 [para_into,363,379,demod,409,409,1162,flip.1] f(c(f(f(c(x),y),f(c(x),c(x)))),x)=c(x). 5787,5786 [para_into,3290,377,demod,409,18] f(f(c(f(x,c(x))),c(f(x,c(x)))),y)=f(f(x,c(x)),y). 5806,5805 [back_demod,643,demod,5787,766] f(c(x),c(x))=x. 5841,5840 [back_demod,4012,demod,5806,352,409,5806,flip.1] c(x)=f(x,x). 5938 [back_demod,472,demod,5841,5841] f(x,f(f(f(x,x),f(x,x)),f(x,y)))=f(x,y). 5995,5994 [back_demod,5805,demod,5841,5841] f(f(x,x),f(x,x))=x. 8024 [back_demod,5938,demod,5995] f(x,f(x,f(x,y)))=f(x,y). 8026 [binary,8024,3] $Ans(OM_SS). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 159 clauses generated 13289 clauses kept 6446 clauses forward subsumed 9707 clauses back subsumed 364 Kbytes malloced 4790 ----------- times (seconds) ----------- user CPU time 2.64 (0 hr, 0 min, 2 sec) system CPU time 0.20 (0 hr, 0 min, 0 sec) wall-clock time 3 (0 hr, 0 min, 3 sec) para_into time 0.03 para_from time 0.03 for_sub time 0.08 back_sub time 0.11 conflict time 0.02 demod time 0.18 That finishes the proof of the theorem. Process 26015 finished Fri Sep 12 16:34:56 2003