============================== Prover9 =============================== Prover9 (32) version March-2007, March 2007. Process 21129 was started by mccune on cleo, Mon Mar 19 17:05:28 2007 The command was "/home/mccune/bin/prover9 -f wang.in wang1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file wang.in formulas(sos). y == m | p(y,m) | v1 == m | v1 == y | -p(y,v1) | -p(v1,y). y == b | -p(y,b) | v == b | v == y | -p(y,v) | -p(v,y). y == k | y == m | y == b | -p(y,k). y == m | -p(y,m) | -(f(y) == m). y == m | -p(y,m) | -(f(y) == y). y == m | -p(y,m) | p(y,f(y)). y == m | -p(y,m) | p(f(y),y). y == b | p(y,b) | -(g(y) == b). y == b | p(y,b) | -(g(y) == y). y == b | p(y,b) | p(y,g(y)). y == b | p(y,b) | p(g(y),y). y == k | -(y == m) | p(y,k). y == k | -(y == b) | p(y,k). x == x. -(x == y) | y == x. -(x == y) | -(y == z) | x == z. -(x == y) | -p(x,z) | p(y,z). -(x == y) | -p(z,x) | p(z,y). -(x == y) | f(x) == f(y). -(x == y) | g(x) == g(y). end_of_list. % Reading from file wang1.in formulas(sos). -(m == b). -(b == k). -(k == m). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x == m | p(x,m) | y == m | y == x | -p(x,y) | -p(y,x). [assumption]. x == b | -p(x,b) | y == b | y == x | -p(x,y) | -p(y,x). [assumption]. x == k | x == m | x == b | -p(x,k). [assumption]. x == m | -p(x,m) | -(f(x) == m). [assumption]. x == m | -p(x,m) | -(f(x) == x). [assumption]. x == m | -p(x,m) | p(x,f(x)). [assumption]. x == m | -p(x,m) | p(f(x),x). [assumption]. x == b | p(x,b) | -(g(x) == b). [assumption]. x == b | p(x,b) | -(g(x) == x). [assumption]. x == b | p(x,b) | p(x,g(x)). [assumption]. x == b | p(x,b) | p(g(x),x). [assumption]. x == k | -(x == m) | p(x,k). [assumption]. x == k | -(x == b) | p(x,k). [assumption]. x == x. [assumption]. -(x == y) | y == x. [assumption]. -(x == y) | -(y == z) | x == z. [assumption]. -(x == y) | -p(x,z) | p(y,z). [assumption]. -(x == y) | -p(z,x) | p(z,y). [assumption]. -(x == y) | f(x) == f(y). [assumption]. -(x == y) | g(x) == g(y). [assumption]. -(m == b). [assumption]. -(b == k). [assumption]. -(k == m). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ ==, p ]). Function symbol precedence: lex([ b, m, k, f, g ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 x == m | p(x,m) | y == m | y == x | -p(x,y) | -p(y,x). [assumption]. 2 x == b | -p(x,b) | y == b | y == x | -p(x,y) | -p(y,x). [assumption]. 3 x == k | x == m | x == b | -p(x,k). [assumption]. 4 x == m | -p(x,m) | -(f(x) == m). [assumption]. 5 x == m | -p(x,m) | -(f(x) == x). [assumption]. 6 x == m | -p(x,m) | p(x,f(x)). [assumption]. 7 x == m | -p(x,m) | p(f(x),x). [assumption]. 8 x == b | p(x,b) | -(g(x) == b). [assumption]. 9 x == b | p(x,b) | -(g(x) == x). [assumption]. 10 x == b | p(x,b) | p(x,g(x)). [assumption]. 11 x == b | p(x,b) | p(g(x),x). [assumption]. 12 x == k | -(x == m) | p(x,k). [assumption]. 13 x == k | -(x == b) | p(x,k). [assumption]. 14 x == x. [assumption]. 15 -(x == y) | y == x. [assumption]. 16 -(x == y) | -(y == z) | x == z. [assumption]. 17 -(x == y) | -p(x,z) | p(y,z). [assumption]. 18 -(x == y) | -p(z,x) | p(z,y). [assumption]. 19 -(x == y) | f(x) == f(y). [assumption]. 20 -(x == y) | g(x) == g(y). [assumption]. 21 -(m == b). [assumption]. 22 -(b == k). [assumption]. 23 -(k == m). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=18): 1 x == m | p(x,m) | y == m | y == x | -p(x,y) | -p(y,x). [assumption]. given #2 (I,wt=18): 2 x == b | -p(x,b) | y == b | y == x | -p(x,y) | -p(y,x). [assumption]. given #3 (I,wt=12): 3 x == k | x == m | x == b | -p(x,k). [assumption]. given #4 (I,wt=10): 4 x == m | -p(x,m) | -(f(x) == m). [assumption]. given #5 (I,wt=10): 5 x == m | -p(x,m) | -(f(x) == x). [assumption]. given #6 (I,wt=10): 6 x == m | -p(x,m) | p(x,f(x)). [assumption]. given #7 (I,wt=10): 7 x == m | -p(x,m) | p(f(x),x). [assumption]. given #8 (I,wt=10): 8 x == b | p(x,b) | -(g(x) == b). [assumption]. given #9 (I,wt=10): 9 x == b | p(x,b) | -(g(x) == x). [assumption]. given #10 (I,wt=10): 10 x == b | p(x,b) | p(x,g(x)). [assumption]. given #11 (I,wt=10): 11 x == b | p(x,b) | p(g(x),x). [assumption]. given #12 (I,wt=9): 12 x == k | -(x == m) | p(x,k). [assumption]. given #13 (I,wt=9): 13 x == k | -(x == b) | p(x,k). [assumption]. given #14 (I,wt=3): 14 x == x. [assumption]. given #15 (I,wt=6): 15 -(x == y) | y == x. [assumption]. given #16 (I,wt=9): 16 -(x == y) | -(y == z) | x == z. [assumption]. given #17 (I,wt=9): 17 -(x == y) | -p(x,z) | p(y,z). [assumption]. given #18 (I,wt=9): 18 -(x == y) | -p(z,x) | p(z,y). [assumption]. given #19 (I,wt=8): 19 -(x == y) | f(x) == f(y). [assumption]. given #20 (I,wt=8): 20 -(x == y) | g(x) == g(y). [assumption]. given #21 (I,wt=3): 21 -(m == b). [assumption]. given #22 (I,wt=3): 22 -(b == k). [assumption]. given #23 (I,wt=3): 23 -(k == m). [assumption]. given #24 (A,wt=22): 24 x == b | p(x,b) | g(x) == b | -p(g(x),b) | x == g(x) | -p(g(x),x). [resolve(10,c,2,f),merge(e)]. given #25 (F,wt=3): 41 -(b == m). [ur(15,b,21,a)]. given #26 (F,wt=3): 42 -(k == b). [ur(15,b,22,a)]. given #27 (F,wt=3): 44 -(m == k). [ur(15,b,23,a)]. given #28 (T,wt=3): 35 p(b,k). [resolve(14,a,13,b),unit_del(a,22)]. given #29 (T,wt=3): 45 p(m,k). [back_unit_del(36),unit_del(a,44)]. given #30 (T,wt=6): 47 -(k == x) | p(b,x). [resolve(35,a,18,b)]. given #31 (T,wt=6): 48 -(b == x) | p(x,k). [resolve(35,a,17,b)]. given #32 (A,wt=25): 25 x == b | p(x,b) | g(x) == m | p(g(x),m) | x == m | x == g(x) | -p(g(x),x). [resolve(10,c,1,f)]. given #33 (F,wt=6): 53 -p(k,b) | -p(k,m). [resolve(45,a,2,f),unit_del(a,42),unit_del(c,21),unit_del(d,44)]. given #34 (F,wt=6): 54 -p(m,b) | -p(k,m). [resolve(45,a,2,e),unit_del(a,21),unit_del(c,42),unit_del(d,23)]. given #35 (T,wt=6): 49 p(k,m) | -p(k,b). [resolve(35,a,1,f),unit_del(a,23),unit_del(c,41),unit_del(d,22)]. given #36 (T,wt=6): 50 p(b,m) | -p(k,b). [resolve(35,a,1,e),unit_del(a,41),unit_del(c,23),unit_del(d,42)]. given #37 (T,wt=6): 51 -(k == x) | p(m,x). [resolve(45,a,18,b)]. given #38 (T,wt=6): 52 -(m == x) | p(x,k). [resolve(45,a,17,b)]. given #39 (A,wt=24): 26 x == b | p(x,b) | x == m | p(x,m) | g(x) == m | g(x) == x | -p(g(x),x). [resolve(10,c,1,e)]. given #40 (T,wt=12): 30 p(m,b) | g(m) == m | -(f(g(m)) == m). [resolve(11,c,4,b),unit_del(a,21)]. given #41 (T,wt=13): 27 p(m,b) | g(m) == m | p(f(g(m)),g(m)). [resolve(11,c,7,b),unit_del(a,21)]. given #42 (T,wt=13): 28 p(m,b) | g(m) == m | p(g(m),f(g(m))). [resolve(11,c,6,b),unit_del(a,21)]. given #43 (T,wt=13): 29 p(m,b) | g(m) == m | -(f(g(m)) == g(m)). [resolve(11,c,5,b),unit_del(a,21)]. given #44 (A,wt=13): 37 -(g(x) == y) | p(y,x) | x == b | p(x,b). [resolve(17,b,11,c)]. given #45 (T,wt=13): 38 -(x == y) | p(y,g(x)) | x == b | p(x,b). [resolve(17,b,10,c)]. given #46 (T,wt=13): 39 -(x == y) | p(g(x),y) | x == b | p(x,b). [resolve(18,b,11,c)]. given #47 (T,wt=13): 40 -(g(x) == y) | p(x,y) | x == b | p(x,b). [resolve(18,b,10,c)]. given #48 (T,wt=15): 43 p(k,b) | g(k) == k | g(k) == m | g(k) == b. [back_unit_del(31),unit_del(a,42)]. given #49 (A,wt=18): 46 x == b | p(x,b) | g(x) == b | -p(g(x),b) | x == g(x). [resolve(24,f,11,c),merge(f),merge(g)]. given #50 (T,wt=15): 69 g(k) == k | g(k) == m | g(k) == b | p(b,m). [resolve(43,a,50,b)]. given #51 (T,wt=15): 70 g(k) == k | g(k) == m | g(k) == b | p(k,m). [resolve(43,a,49,b)]. given #52 (T,wt=15): 80 g(k) == k | g(k) == m | g(k) == b | -p(m,b). [resolve(70,d,54,b)]. given #53 (T,wt=15): 81 g(k) == k | g(k) == m | g(k) == b | -p(k,b). [resolve(70,d,53,b)]. given #54 (A,wt=21): 55 x == b | p(x,b) | g(x) == m | p(g(x),m) | x == m | x == g(x). [resolve(25,g,11,c),merge(g),merge(h)]. given #55 (T,wt=12): 88 g(k) == k | g(k) == m | g(k) == b. [resolve(81,d,43,a),merge(d),merge(e),merge(f)]. given #56 (T,wt=11): 104 g(k) == m | g(k) == b | p(k,b). [resolve(88,a,9,c),unit_del(c,42)]. given #57 (T,wt=11): 105 g(k) == m | g(k) == b | p(b,m). [resolve(104,c,50,b)]. given #58 (T,wt=11): 106 g(k) == m | g(k) == b | p(k,m). [resolve(104,c,49,b)]. given #59 (A,wt=20): 56 x == b | p(x,b) | x == m | p(x,m) | g(x) == m | g(x) == x. [resolve(26,g,11,c),merge(g),merge(h)]. given #60 (T,wt=11): 116 g(k) == m | g(k) == b | -p(m,b). [resolve(106,c,54,b)]. given #61 (T,wt=11): 117 g(k) == m | g(k) == b | -p(k,b). [resolve(106,c,53,b)]. given #62 (T,wt=8): 132 g(k) == m | g(k) == b. [resolve(117,c,104,c),merge(c),merge(d)]. given #63 (T,wt=8): 140 g(k) == b | m == g(k). [resolve(132,a,15,a)]. given #64 (A,wt=16): 57 p(m,b) | g(m) == m | -(g(m) == x) | p(f(g(m)),x). [resolve(27,c,18,b)]. given #65 (T,wt=7): 142 m == g(k) | p(k,b). [resolve(140,a,40,a),merge(d),unit_del(c,42)]. given #66 (T,wt=7): 149 m == g(k) | p(b,m). [resolve(142,b,50,b)]. given #67 (T,wt=7): 150 m == g(k) | p(k,m). [resolve(142,b,49,b)]. given #68 (T,wt=7): 160 m == g(k) | -p(m,b). [resolve(150,b,54,b)]. given #69 (A,wt=16): 58 p(m,b) | g(m) == m | -(f(g(m)) == x) | p(x,g(m)). [resolve(27,c,17,b)]. given #70 (T,wt=7): 161 m == g(k) | -p(k,b). [resolve(150,b,53,b)]. given #71 (T,wt=4): 168 m == g(k). [resolve(161,b,142,b),merge(b)]. given #72 (T,wt=4): 169 p(g(k),k). [resolve(168,a,52,a)]. given #73 (T,wt=4): 176 g(k) == m. [resolve(168,a,15,a)]. given #74 (A,wt=32): 59 p(m,b) | g(m) == m | g(m) == b | -p(g(m),b) | f(g(m)) == b | f(g(m)) == g(m) | -p(g(m),f(g(m))). [resolve(27,c,2,f)]. given #75 (F,wt=4): 177 -(g(k) == k). [ur(16,a,168,a,c,44,a)]. given #76 (F,wt=4): 178 -(g(k) == b). [ur(16,a,168,a,c,21,a)]. given #77 (F,wt=4): 190 -(b == g(k)). [ur(16,b,176,a,c,41,a)]. given #78 (F,wt=4): 191 -(k == g(k)). [ur(16,b,176,a,c,23,a)]. given #79 (T,wt=6): 172 g(m) == g(g(k)). [resolve(168,a,20,a)]. given #80 (T,wt=6): 173 f(m) == f(g(k)). [resolve(168,a,19,a)]. given #81 (T,wt=6): 181 f(g(k)) == f(m). [back_unit_del(137),unit_del(a,178)]. given #82 (T,wt=6): 182 g(g(k)) == g(m). [back_unit_del(136),unit_del(a,178)]. given #83 (A,wt=33): 60 p(m,b) | g(m) == m | f(g(m)) == b | -p(f(g(m)),b) | g(m) == b | g(m) == f(g(m)) | -p(g(m),f(g(m))). [resolve(27,c,2,e)]. given #84 (F,wt=7): 188 -p(k,b) | -p(k,g(k)). [resolve(169,a,2,f),unit_del(a,42),unit_del(c,178),unit_del(d,177)]. given #85 (F,wt=8): 192 -p(g(k),b) | -p(k,g(k)). [back_unit_del(189),unit_del(b,191)]. given #86 (T,wt=6): 185 p(k,m) | p(k,b). [back_unit_del(133),unit_del(a,178)]. given #87 (T,wt=6): 223 p(k,b) | -p(m,b). [resolve(185,a,54,b)]. given #88 (T,wt=7): 174 -(x == m) | x == g(k). [resolve(168,a,16,b)]. given #89 (T,wt=7): 175 -(g(k) == x) | m == x. [resolve(168,a,16,a)]. given #90 (A,wt=28): 61 p(m,b) | g(m) == m | p(g(m),m) | f(g(m)) == m | f(g(m)) == g(m) | -p(g(m),f(g(m))). [resolve(27,c,1,f),merge(c)]. given #91 (T,wt=7): 179 -(m == x) | g(k) == x. [back_unit_del(139),unit_del(a,178)]. given #92 (T,wt=7): 180 -(x == g(k)) | x == m. [back_unit_del(138),unit_del(a,178)]. given #93 (T,wt=7): 186 -(k == x) | p(g(k),x). [resolve(169,a,18,b)]. given #94 (T,wt=7): 187 -(g(k) == x) | p(x,k). [resolve(169,a,17,b)]. given #95 (A,wt=29): 62 p(m,b) | g(m) == m | f(g(m)) == m | p(f(g(m)),m) | g(m) == f(g(m)) | -p(g(m),f(g(m))). [resolve(27,c,1,e),merge(e)]. given #96 (T,wt=7): 226 p(k,b) | p(f(k),k). [resolve(185,a,7,b),unit_del(b,23)]. given #97 (T,wt=7): 227 p(k,b) | p(k,f(k)). [resolve(185,a,6,b),unit_del(b,23)]. given #98 (T,wt=7): 228 p(k,b) | -(f(k) == k). [resolve(185,a,5,b),unit_del(b,23)]. given #99 (T,wt=7): 229 p(k,b) | -(f(k) == m). [resolve(185,a,4,b),unit_del(b,23)]. given #100 (A,wt=16): 63 p(m,b) | g(m) == m | -(f(g(m)) == x) | p(g(m),x). [resolve(28,c,18,b)]. given #101 (T,wt=7): 241 p(k,b) | -(f(k) == b). [factor(237,a,c)]. given #102 (T,wt=8): 170 p(g(m),g(k)) | p(m,b). [resolve(168,a,39,a),unit_del(b,21)]. given #103 (T,wt=8): 171 p(g(k),g(m)) | p(m,b). [resolve(168,a,38,a),unit_del(b,21)]. given #104 (T,wt=8): 195 p(m,g(g(k))) | p(m,b). [resolve(172,a,40,a),unit_del(b,21)]. given #105 (A,wt=16): 64 p(m,b) | g(m) == m | -(g(m) == x) | p(x,f(g(m))). [resolve(28,c,17,b)]. given #106 (T,wt=8): 198 p(g(g(k)),m) | p(m,b). [resolve(172,a,37,a),unit_del(b,21)]. given #107 (T,wt=8): 199 g(g(m)) == g(g(g(k))). [resolve(172,a,20,a)]. given #108 (T,wt=8): 200 f(g(m)) == f(g(g(k))). [resolve(172,a,19,a)]. given #109 (T,wt=8): 205 g(f(m)) == g(f(g(k))). [resolve(173,a,20,a)]. given #110 (A,wt=33): 65 p(m,b) | g(m) == m | f(g(m)) == b | -p(f(g(m)),b) | g(m) == b | g(m) == f(g(m)) | -p(f(g(m)),g(m)). [resolve(28,c,2,f)]. given #111 (T,wt=8): 206 f(f(m)) == f(f(g(k))). [resolve(173,a,19,a)]. given #112 (T,wt=8): 211 g(f(g(k))) == g(f(m)). [resolve(181,a,20,a)]. given #113 (T,wt=8): 212 f(f(g(k))) == f(f(m)). [resolve(181,a,19,a)]. given #114 (T,wt=8): 219 g(g(g(k))) == g(g(m)). [resolve(182,a,20,a)]. given #115 (A,wt=24): 89 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(m == y) | p(g(x),y). [resolve(55,d,18,b)]. given #116 (T,wt=8): 220 f(g(g(k))) == f(g(m)). [resolve(182,a,19,a)]. given #117 (T,wt=8): 253 p(m,b) | -(g(g(k)) == b). [factor(250,a,c)]. given #118 (T,wt=9): 183 p(m,g(g(k))) | p(g(k),b). [back_unit_del(135),unit_del(a,178)]. given #119 (T,wt=8): 323 p(m,g(g(k))) | p(k,b). [resolve(183,b,46,d),unit_del(b,42),unit_del(d,178),unit_del(e,191)]. given #120 (A,wt=24): 90 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(g(x) == y) | p(y,m). [resolve(55,d,17,b)]. given #121 (T,wt=8): 327 p(m,g(g(k))) | p(b,m). [resolve(323,b,50,b)]. given #122 (T,wt=8): 328 p(m,g(g(k))) | p(k,m). [resolve(323,b,49,b)]. given #123 (T,wt=8): 340 p(m,g(g(k))) | -p(m,b). [resolve(328,b,54,b)]. given #124 (T,wt=8): 341 p(m,g(g(k))) | -p(k,b). [resolve(328,b,53,b)]. given #125 (A,wt=23): 91 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | p(f(g(x)),g(x)). [resolve(55,d,7,b),merge(f)]. given #126 (T,wt=5): 348 p(m,g(g(k))). [resolve(341,b,323,b),merge(b)]. given #127 (T,wt=8): 354 -(g(g(k)) == x) | p(m,x). [resolve(348,a,18,b)]. given #128 (T,wt=4): 358 p(m,g(m)). [resolve(354,a,182,a)]. given #129 (T,wt=7): 359 -(g(m) == x) | p(m,x). [resolve(358,a,18,b)]. given #130 (A,wt=23): 92 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | p(g(x),f(g(x))). [resolve(55,d,6,b),merge(f)]. given #131 (T,wt=7): 360 -(m == x) | p(x,g(m)). [resolve(358,a,17,b)]. given #132 (T,wt=5): 367 p(g(k),g(m)). [resolve(360,a,168,a)]. given #133 (T,wt=8): 355 -(m == x) | p(x,g(g(k))). [resolve(348,a,17,b)]. given #134 (T,wt=6): 374 p(g(k),g(g(k))). [resolve(355,a,168,a)]. given #135 (A,wt=23): 93 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == g(x)). [resolve(55,d,5,b),merge(f)]. given #136 (T,wt=8): 370 -(g(m) == x) | p(g(k),x). [resolve(367,a,18,b)]. given #137 (T,wt=8): 371 -(g(k) == x) | p(x,g(m)). [resolve(367,a,17,b)]. given #138 (T,wt=9): 184 p(g(g(k)),m) | p(g(k),b). [back_unit_del(134),unit_del(a,178)]. given #139 (T,wt=9): 201 -(x == g(m)) | x == g(g(k)). [resolve(172,a,16,b)]. given #140 (A,wt=22): 94 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == m). [resolve(55,d,4,b),merge(f)]. given #141 (T,wt=9): 202 -(g(g(k)) == x) | g(m) == x. [resolve(172,a,16,a)]. given #142 (T,wt=9): 207 -(x == f(m)) | x == f(g(k)). [resolve(173,a,16,b)]. given #143 (T,wt=9): 208 -(f(g(k)) == x) | f(m) == x. [resolve(173,a,16,a)]. given #144 (T,wt=9): 213 -(x == f(g(k))) | x == f(m). [resolve(181,a,16,b)]. given #145 (A,wt=28): 95 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -p(m,b) | g(x) == b | -p(m,g(x)). [resolve(55,d,2,f),merge(i),unit_del(f,21)]. given #146 (T,wt=9): 214 -(f(m) == x) | f(g(k)) == x. [resolve(181,a,16,a)]. given #147 (T,wt=9): 218 p(g(m),g(k)) | p(g(k),b). [resolve(182,a,37,a),unit_del(b,178)]. given #148 (T,wt=8): 388 p(g(m),g(k)) | p(k,b). [resolve(218,b,46,d),unit_del(b,42),unit_del(d,178),unit_del(e,191)]. given #149 (T,wt=9): 221 -(x == g(g(k))) | x == g(m). [resolve(182,a,16,b)]. given #150 (A,wt=23): 125 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(m == y) | p(x,y). [resolve(56,d,18,b)]. given #151 (T,wt=9): 222 -(g(m) == x) | g(g(k)) == x. [resolve(182,a,16,a)]. given #152 (T,wt=9): 224 p(k,b) | -(m == x) | p(k,x). [resolve(185,a,18,b)]. given #153 (T,wt=7): 397 p(k,b) | p(k,g(k)). [resolve(224,b,168,a)]. given #154 (T,wt=7): 400 p(k,b) | -p(g(k),b). [resolve(397,b,2,f),unit_del(b,178),unit_del(d,42),unit_del(e,191),unit_del(f,169)]. given #155 (A,wt=23): 126 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(x == y) | p(y,m). [resolve(56,d,17,b)]. given #156 (T,wt=9): 225 p(k,b) | -(k == x) | p(x,m). [resolve(185,a,17,b)]. given #157 (T,wt=9): 375 -(g(g(k)) == x) | p(g(k),x). [resolve(374,a,18,b)]. given #158 (T,wt=9): 376 -(g(k) == x) | p(x,g(g(k))). [resolve(374,a,17,b)]. given #159 (T,wt=9): 387 p(g(m),g(k)) | -p(k,g(k)). [resolve(218,b,192,a)]. given #160 (A,wt=21): 127 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | p(f(x),x). [resolve(56,d,7,b),merge(f)]. given #161 (T,wt=10): 232 p(k,b) | -(k == x) | p(f(k),x). [resolve(226,b,18,b)]. given #162 (T,wt=10): 233 p(k,b) | -(f(k) == x) | p(x,k). [resolve(226,b,17,b)]. given #163 (T,wt=10): 237 p(k,b) | -(f(k) == x) | p(k,x). [resolve(227,b,18,b)]. given #164 (T,wt=10): 238 p(k,b) | -(k == x) | p(x,f(k)). [resolve(227,b,17,b)]. given #165 (A,wt=21): 128 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | p(x,f(x)). [resolve(56,d,6,b),merge(f)]. given #166 (T,wt=10): 266 g(g(g(m))) == g(g(g(g(k)))). [resolve(199,a,20,a)]. given #167 (T,wt=10): 267 f(g(g(m))) == f(g(g(g(k)))). [resolve(199,a,19,a)]. given #168 (T,wt=10): 274 g(f(g(m))) == g(f(g(g(k)))). [resolve(200,a,20,a)]. given #169 (T,wt=10): 275 f(f(g(m))) == f(f(g(g(k)))). [resolve(200,a,19,a)]. given #170 (A,wt=21): 129 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == x). [resolve(56,d,5,b),merge(f)]. given #171 (T,wt=10): 282 g(g(f(m))) == g(g(f(g(k)))). [resolve(205,a,20,a)]. given #172 (T,wt=10): 283 f(g(f(m))) == f(g(f(g(k)))). [resolve(205,a,19,a)]. given #173 (T,wt=10): 289 g(f(f(m))) == g(f(f(g(k)))). [resolve(206,a,20,a)]. given #174 (T,wt=10): 290 f(f(f(m))) == f(f(f(g(k)))). [resolve(206,a,19,a)]. given #175 (A,wt=21): 130 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == m). [resolve(56,d,4,b),merge(f)]. given #176 (T,wt=10): 297 g(g(f(g(k)))) == g(g(f(m))). [resolve(211,a,20,a)]. given #177 (T,wt=10): 298 f(g(f(g(k)))) == f(g(f(m))). [resolve(211,a,19,a)]. given #178 (T,wt=10): 303 g(f(f(g(k)))) == g(f(f(m))). [resolve(212,a,20,a)]. given #179 (T,wt=10): 304 f(f(f(g(k)))) == f(f(f(m))). [resolve(212,a,19,a)]. given #180 (A,wt=23): 131 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -p(m,b) | -p(m,x). [resolve(56,d,2,f),merge(h),merge(i),unit_del(f,21)]. given #181 (T,wt=10): 311 g(g(g(g(k)))) == g(g(g(m))). [resolve(219,a,20,a)]. given #182 (T,wt=10): 312 f(g(g(g(k)))) == f(g(g(m))). [resolve(219,a,19,a)]. given #183 (T,wt=10): 318 g(f(g(g(k)))) == g(f(g(m))). [resolve(220,a,20,a)]. given #184 (T,wt=10): 319 f(f(g(g(k)))) == f(f(g(m))). [resolve(220,a,19,a)]. given #185 (A,wt=26): 193 p(m,b) | g(m) == m | g(m) == b | -p(g(m),b) | f(g(m)) == b | f(g(m)) == g(m). [resolve(59,g,28,c),merge(g),merge(h)]. given #186 (T,wt=10): 398 p(k,b) | -(g(k) == x) | p(k,x). [resolve(397,b,18,b)]. given #187 (T,wt=10): 399 p(k,b) | -(k == x) | p(x,g(k)). [resolve(397,b,17,b)]. given #188 (T,wt=11): 242 p(m,b) | -(g(k) == x) | p(g(m),x). [resolve(170,a,18,b)]. given #189 (T,wt=7): 560 p(m,b) | p(g(m),m). [resolve(242,b,176,a)]. given #190 (A,wt=14): 194 p(m,b) | g(m) == m | p(f(g(m)),g(g(k))). [resolve(172,a,57,c)]. given #191 (T,wt=10): 561 p(m,b) | -(m == x) | p(g(m),x). [resolve(560,b,18,b)]. given #192 (T,wt=10): 562 p(m,b) | -(g(m) == x) | p(x,m). [resolve(560,b,17,b)]. given #193 (T,wt=11): 243 p(m,b) | -(g(m) == x) | p(x,g(k)). [resolve(170,a,17,b)]. given #194 (T,wt=9): 569 p(m,b) | p(g(g(k)),g(k)). [resolve(243,b,172,a)]. given #195 (A,wt=15): 196 p(g(g(m)),g(g(k))) | g(m) == b | p(g(m),b). [resolve(172,a,39,a)]. given #196 (T,wt=11): 255 p(m,b) | -(m == x) | p(g(g(k)),x). [resolve(198,a,18,b)]. given #197 (T,wt=11): 256 p(m,b) | -(g(g(k)) == x) | p(x,m). [resolve(198,a,17,b)]. given #198 (T,wt=11): 268 -(x == g(g(m))) | x == g(g(g(k))). [resolve(199,a,16,b)]. given #199 (T,wt=11): 269 -(g(g(g(k))) == x) | g(g(m)) == x. [resolve(199,a,16,a)]. given #200 (A,wt=15): 197 p(g(g(k)),g(g(m))) | g(m) == b | p(g(m),b). [resolve(172,a,38,a)]. given #201 (T,wt=11): 276 -(x == f(g(m))) | x == f(g(g(k))). [resolve(200,a,16,b)]. given #202 (T,wt=11): 277 -(f(g(g(k))) == x) | f(g(m)) == x. [resolve(200,a,16,a)]. given #203 (T,wt=11): 284 -(x == g(f(m))) | x == g(f(g(k))). [resolve(205,a,16,b)]. given #204 (T,wt=11): 285 -(g(f(g(k))) == x) | g(f(m)) == x. [resolve(205,a,16,a)]. given #205 (A,wt=15): 203 p(g(f(m)),f(g(k))) | f(m) == b | p(f(m),b). [resolve(173,a,39,a)]. given #206 (T,wt=11): 291 -(x == f(f(m))) | x == f(f(g(k))). [resolve(206,a,16,b)]. given #207 (T,wt=11): 292 -(f(f(g(k))) == x) | f(f(m)) == x. [resolve(206,a,16,a)]. given #208 (T,wt=11): 299 -(x == g(f(g(k)))) | x == g(f(m)). [resolve(211,a,16,b)]. given #209 (T,wt=11): 300 -(g(f(m)) == x) | g(f(g(k))) == x. [resolve(211,a,16,a)]. given #210 (A,wt=15): 204 p(f(g(k)),g(f(m))) | f(m) == b | p(f(m),b). [resolve(173,a,38,a)]. given #211 (T,wt=11): 305 -(x == f(f(g(k)))) | x == f(f(m)). [resolve(212,a,16,b)]. given #212 (T,wt=11): 306 -(f(f(m)) == x) | f(f(g(k))) == x. [resolve(212,a,16,a)]. given #213 (T,wt=11): 313 -(x == g(g(g(k)))) | x == g(g(m)). [resolve(219,a,16,b)]. given #214 (T,wt=11): 314 -(g(g(m)) == x) | g(g(g(k))) == x. [resolve(219,a,16,a)]. given #215 (A,wt=17): 209 p(g(f(g(k))),f(m)) | f(g(k)) == b | p(f(g(k)),b). [resolve(181,a,39,a)]. given #216 (T,wt=11): 320 -(x == f(g(g(k)))) | x == f(g(m)). [resolve(220,a,16,b)]. given #217 (T,wt=11): 321 -(f(g(m)) == x) | f(g(g(k))) == x. [resolve(220,a,16,a)]. given #218 (T,wt=11): 392 p(k,b) | -(g(k) == x) | p(g(m),x). [resolve(388,a,18,b)]. given #219 (T,wt=7): 604 p(k,b) | p(g(m),m). [resolve(392,b,176,a)]. given #220 (A,wt=17): 210 p(f(m),g(f(g(k)))) | f(g(k)) == b | p(f(g(k)),b). [resolve(181,a,38,a)]. given #221 (T,wt=10): 605 p(k,b) | -(m == x) | p(g(m),x). [resolve(604,b,18,b)]. given #222 (T,wt=10): 606 p(k,b) | -(g(m) == x) | p(x,m). [resolve(604,b,17,b)]. given #223 (T,wt=8): 617 p(k,b) | p(g(g(k)),m). [resolve(606,b,172,a)]. given #224 (T,wt=11): 393 p(k,b) | -(g(m) == x) | p(x,g(k)). [resolve(388,a,17,b)]. given #225 (A,wt=17): 216 p(g(g(g(k))),g(m)) | g(g(k)) == b | p(g(g(k)),b). [resolve(182,a,39,a)]. given #226 (T,wt=9): 625 p(k,b) | p(g(g(k)),g(k)). [resolve(393,b,172,a)]. given #227 (T,wt=11): 618 p(k,b) | -(m == x) | p(g(g(k)),x). [resolve(617,b,18,b)]. given #228 (T,wt=11): 619 p(k,b) | -(g(g(k)) == x) | p(x,m). [resolve(617,b,17,b)]. given #229 (T,wt=12): 379 p(g(k),b) | -(m == x) | p(g(g(k)),x). [resolve(184,a,18,b)]. given #230 (A,wt=17): 217 p(g(m),g(g(g(k)))) | g(g(k)) == b | p(g(g(k)),b). [resolve(182,a,38,a)]. given #231 (T,wt=10): 635 p(g(k),b) | p(g(g(k)),g(k)). [resolve(379,b,168,a)]. given #232 (T,wt=12): 380 p(g(k),b) | -(g(g(k)) == x) | p(x,m). [resolve(184,a,17,b)]. given #233 (T,wt=8): 645 p(g(k),b) | p(g(m),m). [resolve(380,b,182,a)]. given #234 (T,wt=8): 646 p(g(m),m) | -p(k,g(k)). [resolve(645,a,192,a)]. given #235 (A,wt=23): 231 p(m,b) | g(m) == m | f(g(m)) == m | p(f(g(m)),m) | g(m) == f(g(m)). [resolve(62,f,28,c),merge(f),merge(g)]. given #236 (T,wt=11): 647 p(g(m),m) | -(b == x) | p(g(k),x). [resolve(645,a,18,b)]. given #237 (T,wt=11): 648 p(g(m),m) | -(g(k) == x) | p(x,b). [resolve(645,a,17,b)]. given #238 (T,wt=12): 389 p(g(m),g(k)) | -(b == x) | p(g(k),x). [resolve(218,b,18,b)]. given #239 (T,wt=12): 390 p(g(m),g(k)) | -(g(k) == x) | p(x,b). [resolve(218,b,17,b)]. given #240 (A,wt=15): 234 p(k,b) | f(k) == k | f(k) == m | f(k) == b. [resolve(226,b,3,d)]. given #241 (T,wt=12): 428 g(g(g(g(m)))) == g(g(g(g(g(k))))). [resolve(266,a,20,a)]. given #242 (T,wt=12): 429 f(g(g(g(m)))) == f(g(g(g(g(k))))). [resolve(266,a,19,a)]. given #243 (T,wt=12): 435 g(f(g(g(m)))) == g(f(g(g(g(k))))). [resolve(267,a,20,a)]. given #244 (T,wt=12): 436 f(f(g(g(m)))) == f(f(g(g(g(k))))). [resolve(267,a,19,a)]. given #245 (A,wt=19): 235 p(k,b) | f(k) == b | -p(f(k),b) | k == f(k) | -p(k,f(k)). [resolve(226,b,2,e),unit_del(d,42)]. given #246 (T,wt=12): 445 g(g(f(g(m)))) == g(g(f(g(g(k))))). [resolve(274,a,20,a)]. given #247 (T,wt=12): 446 f(g(f(g(m)))) == f(g(f(g(g(k))))). [resolve(274,a,19,a)]. given #248 (T,wt=12): 452 g(f(f(g(m)))) == g(f(f(g(g(k))))). [resolve(275,a,20,a)]. given #249 (T,wt=12): 453 f(f(f(g(m)))) == f(f(f(g(g(k))))). [resolve(275,a,19,a)]. given #250 (A,wt=19): 236 p(k,b) | f(k) == m | p(f(k),m) | k == f(k) | -p(k,f(k)). [resolve(226,b,1,e),unit_del(d,23)]. given #251 (T,wt=12): 462 g(g(g(f(m)))) == g(g(g(f(g(k))))). [resolve(282,a,20,a)]. given #252 (T,wt=12): 463 f(g(g(f(m)))) == f(g(g(f(g(k))))). [resolve(282,a,19,a)]. given #253 (T,wt=12): 469 g(f(g(f(m)))) == g(f(g(f(g(k))))). [resolve(283,a,20,a)]. given #254 (T,wt=12): 470 f(f(g(f(m)))) == f(f(g(f(g(k))))). [resolve(283,a,19,a)]. given #255 (A,wt=19): 239 p(k,b) | f(k) == b | -p(f(k),b) | k == f(k) | -p(f(k),k). [resolve(227,b,2,f),unit_del(d,42)]. given #256 (T,wt=12): 479 g(g(f(f(m)))) == g(g(f(f(g(k))))). [resolve(289,a,20,a)]. given #257 (T,wt=12): 480 f(g(f(f(m)))) == f(g(f(f(g(k))))). [resolve(289,a,19,a)]. given #258 (T,wt=12): 486 g(f(f(f(m)))) == g(f(f(f(g(k))))). [resolve(290,a,20,a)]. given #259 (T,wt=12): 487 f(f(f(f(m)))) == f(f(f(f(g(k))))). [resolve(290,a,19,a)]. given #260 (A,wt=14): 254 p(m,b) | g(m) == m | p(g(g(k)),f(g(m))). [resolve(64,c,172,a)]. given #261 (T,wt=12): 496 g(g(g(f(g(k))))) == g(g(g(f(m)))). [resolve(297,a,20,a)]. given #262 (T,wt=12): 497 f(g(g(f(g(k))))) == f(g(g(f(m)))). [resolve(297,a,19,a)]. given #263 (T,wt=12): 503 g(f(g(f(g(k))))) == g(f(g(f(m)))). [resolve(298,a,20,a)]. given #264 (T,wt=12): 504 f(f(g(f(g(k))))) == f(f(g(f(m)))). [resolve(298,a,19,a)]. given #265 (A,wt=16): 257 p(m,b) | g(g(k)) == m | p(f(g(g(k))),g(g(k))). [resolve(198,a,7,b)]. given #266 (T,wt=12): 513 g(g(f(f(g(k))))) == g(g(f(f(m)))). [resolve(303,a,20,a)]. given #267 (T,wt=12): 514 f(g(f(f(g(k))))) == f(g(f(f(m)))). [resolve(303,a,19,a)]. given #268 (T,wt=12): 520 g(f(f(f(g(k))))) == g(f(f(f(m)))). [resolve(304,a,20,a)]. given #269 (T,wt=12): 521 f(f(f(f(g(k))))) == f(f(f(f(m)))). [resolve(304,a,19,a)]. given #270 (A,wt=16): 258 p(m,b) | g(g(k)) == m | p(g(g(k)),f(g(g(k)))). [resolve(198,a,6,b)]. given #271 (T,wt=12): 532 g(g(g(g(g(k))))) == g(g(g(g(m)))). [resolve(311,a,20,a)]. given #272 (T,wt=12): 533 f(g(g(g(g(k))))) == f(g(g(g(m)))). [resolve(311,a,19,a)]. given #273 (T,wt=12): 539 g(f(g(g(g(k))))) == g(f(g(g(m)))). [resolve(312,a,20,a)]. given #274 (T,wt=12): 540 f(f(g(g(g(k))))) == f(f(g(g(m)))). [resolve(312,a,19,a)]. given #275 (A,wt=16): 259 p(m,b) | g(g(k)) == m | -(f(g(g(k))) == g(g(k))). [resolve(198,a,5,b)]. given #276 (T,wt=12): 549 g(g(f(g(g(k))))) == g(g(f(g(m)))). [resolve(318,a,20,a)]. given #277 (T,wt=12): 550 f(g(f(g(g(k))))) == f(g(f(g(m)))). [resolve(318,a,19,a)]. given #278 (T,wt=12): 556 g(f(f(g(g(k))))) == g(f(f(g(m)))). [resolve(319,a,20,a)]. given #279 (T,wt=12): 557 f(f(f(g(g(k))))) == f(f(f(g(m)))). [resolve(319,a,19,a)]. given #280 (A,wt=14): 260 p(m,b) | g(g(k)) == m | -(f(g(g(k))) == m). [resolve(198,a,4,b)]. given #281 (T,wt=12): 570 p(m,b) | -(g(k) == x) | p(g(g(k)),x). [resolve(569,b,18,b)]. given #282 (T,wt=12): 571 p(m,b) | -(g(g(k)) == x) | p(x,g(k)). [resolve(569,b,17,b)]. given #283 (T,wt=12): 610 p(k,b) | g(m) == m | -(f(g(m)) == m). [resolve(604,b,4,b)]. given #284 (T,wt=12): 632 p(k,b) | -(g(k) == x) | p(g(g(k)),x). [resolve(625,b,18,b)]. given #285 (A,wt=15): 262 p(g(m),g(g(g(k)))) | g(m) == b | p(g(m),b). [resolve(199,a,40,a)]. given #286 (T,wt=12): 633 p(k,b) | -(g(g(k)) == x) | p(x,g(k)). [resolve(625,b,17,b)]. given #287 (T,wt=13): 430 -(x == g(g(g(m)))) | x == g(g(g(g(k)))). [resolve(266,a,16,b)]. given #288 (T,wt=13): 431 -(g(g(g(g(k)))) == x) | g(g(g(m))) == x. [resolve(266,a,16,a)]. given #289 (T,wt=13): 437 -(x == f(g(g(m)))) | x == f(g(g(g(k)))). [resolve(267,a,16,b)]. given #290 (A,wt=19): 263 p(g(g(g(m))),g(g(g(k)))) | g(g(m)) == b | p(g(g(m)),b). [resolve(199,a,39,a)]. given #291 (T,wt=13): 438 -(f(g(g(g(k)))) == x) | f(g(g(m))) == x. [resolve(267,a,16,a)]. given #292 (T,wt=13): 447 -(x == g(f(g(m)))) | x == g(f(g(g(k)))). [resolve(274,a,16,b)]. given #293 (T,wt=13): 448 -(g(f(g(g(k)))) == x) | g(f(g(m))) == x. [resolve(274,a,16,a)]. given #294 (T,wt=13): 454 -(x == f(f(g(m)))) | x == f(f(g(g(k)))). [resolve(275,a,16,b)]. given #295 (A,wt=19): 264 p(g(g(g(k))),g(g(g(m)))) | g(g(m)) == b | p(g(g(m)),b). [resolve(199,a,38,a)]. given #296 (T,wt=13): 455 -(f(f(g(g(k)))) == x) | f(f(g(m))) == x. [resolve(275,a,16,a)]. given #297 (T,wt=13): 464 -(x == g(g(f(m)))) | x == g(g(f(g(k)))). [resolve(282,a,16,b)]. given #298 (T,wt=13): 465 -(g(g(f(g(k)))) == x) | g(g(f(m))) == x. [resolve(282,a,16,a)]. given #299 (T,wt=13): 471 -(x == f(g(f(m)))) | x == f(g(f(g(k)))). [resolve(283,a,16,b)]. given #300 (A,wt=15): 265 p(g(g(g(k))),g(m)) | g(m) == b | p(g(m),b). [resolve(199,a,37,a)]. given #301 (T,wt=13): 472 -(f(g(f(g(k)))) == x) | f(g(f(m))) == x. [resolve(283,a,16,a)]. given #302 (T,wt=13): 481 -(x == g(f(f(m)))) | x == g(f(f(g(k)))). [resolve(289,a,16,b)]. given #303 (T,wt=13): 482 -(g(f(f(g(k)))) == x) | g(f(f(m))) == x. [resolve(289,a,16,a)]. given #304 (T,wt=13): 488 -(x == f(f(f(m)))) | x == f(f(f(g(k)))). [resolve(290,a,16,b)]. given #305 (A,wt=14): 270 p(m,b) | g(m) == m | p(g(m),f(g(g(k)))). [resolve(200,a,63,c)]. given #306 (T,wt=13): 489 -(f(f(f(g(k)))) == x) | f(f(f(m))) == x. [resolve(290,a,16,a)]. given #307 (T,wt=13): 498 -(x == g(g(f(g(k))))) | x == g(g(f(m))). [resolve(297,a,16,b)]. given #308 (T,wt=13): 499 -(g(g(f(m))) == x) | g(g(f(g(k)))) == x. [resolve(297,a,16,a)]. given #309 (T,wt=13): 505 -(x == f(g(f(g(k))))) | x == f(g(f(m))). [resolve(298,a,16,b)]. given #310 (A,wt=14): 271 p(m,b) | g(m) == m | p(f(g(g(k))),g(m)). [resolve(200,a,58,c)]. given #311 (T,wt=13): 506 -(f(g(f(m))) == x) | f(g(f(g(k)))) == x. [resolve(298,a,16,a)]. given #312 (T,wt=13): 515 -(x == g(f(f(g(k))))) | x == g(f(f(m))). [resolve(303,a,16,b)]. given #313 (T,wt=13): 516 -(g(f(f(m))) == x) | g(f(f(g(k)))) == x. [resolve(303,a,16,a)]. given #314 (T,wt=13): 522 -(x == f(f(f(g(k))))) | x == f(f(f(m))). [resolve(304,a,16,b)]. given #315 (A,wt=19): 272 p(g(f(g(m))),f(g(g(k)))) | f(g(m)) == b | p(f(g(m)),b). [resolve(200,a,39,a)]. given #316 (T,wt=13): 523 -(f(f(f(m))) == x) | f(f(f(g(k)))) == x. [resolve(304,a,16,a)]. given #317 (T,wt=13): 534 -(x == g(g(g(g(k))))) | x == g(g(g(m))). [resolve(311,a,16,b)]. given #318 (T,wt=13): 535 -(g(g(g(m))) == x) | g(g(g(g(k)))) == x. [resolve(311,a,16,a)]. given #319 (T,wt=13): 541 -(x == f(g(g(g(k))))) | x == f(g(g(m))). [resolve(312,a,16,b)]. given #320 (A,wt=19): 273 p(f(g(g(k))),g(f(g(m)))) | f(g(m)) == b | p(f(g(m)),b). [resolve(200,a,38,a)]. given #321 (T,wt=13): 542 -(f(g(g(m))) == x) | f(g(g(g(k)))) == x. [resolve(312,a,16,a)]. given #322 (T,wt=13): 551 -(x == g(f(g(g(k))))) | x == g(f(g(m))). [resolve(318,a,16,b)]. given #323 (T,wt=13): 552 -(g(f(g(m))) == x) | g(f(g(g(k)))) == x. [resolve(318,a,16,a)]. given #324 (T,wt=13): 558 -(x == f(f(g(g(k))))) | x == f(f(g(m))). [resolve(319,a,16,b)]. given #325 (A,wt=15): 278 p(f(m),g(f(g(k)))) | f(m) == b | p(f(m),b). [resolve(205,a,40,a)]. given #326 (T,wt=13): 559 -(f(f(g(m))) == x) | f(f(g(g(k)))) == x. [resolve(319,a,16,a)]. given #327 (T,wt=13): 607 p(k,b) | g(m) == m | p(f(g(m)),g(m)). [resolve(604,b,7,b)]. given #328 (T,wt=13): 608 p(k,b) | g(m) == m | p(g(m),f(g(m))). [resolve(604,b,6,b)]. given #329 (T,wt=13): 609 p(k,b) | g(m) == m | -(f(g(m)) == g(m)). [resolve(604,b,5,b)]. given #330 (A,wt=19): 279 p(g(g(f(m))),g(f(g(k)))) | g(f(m)) == b | p(g(f(m)),b). [resolve(205,a,39,a)]. given #331 (T,wt=13): 642 p(g(k),b) | -(g(k) == x) | p(g(g(k)),x). [resolve(635,b,18,b)]. given #332 (T,wt=13): 643 p(g(k),b) | -(g(g(k)) == x) | p(x,g(k)). [resolve(635,b,17,b)]. given #333 (T,wt=14): 623 p(k,b) | g(g(k)) == m | -(f(g(g(k))) == m). [resolve(617,b,4,b)]. given #334 (T,wt=14): 668 g(g(g(g(g(m))))) == g(g(g(g(g(g(k)))))). [resolve(428,a,20,a)]. given #335 (A,wt=19): 280 p(g(f(g(k))),g(g(f(m)))) | g(f(m)) == b | p(g(f(m)),b). [resolve(205,a,38,a)]. given #336 (T,wt=14): 669 f(g(g(g(g(m))))) == f(g(g(g(g(g(k)))))). [resolve(428,a,19,a)]. given #337 (T,wt=14): 675 g(f(g(g(g(m))))) == g(f(g(g(g(g(k)))))). [resolve(429,a,20,a)]. given #338 (T,wt=14): 676 f(f(g(g(g(m))))) == f(f(g(g(g(g(k)))))). [resolve(429,a,19,a)]. given #339 (T,wt=14): 685 g(g(f(g(g(m))))) == g(g(f(g(g(g(k)))))). [resolve(435,a,20,a)]. given #340 (A,wt=15): 281 p(g(f(g(k))),f(m)) | f(m) == b | p(f(m),b). [resolve(205,a,37,a)]. given #341 (T,wt=14): 686 f(g(f(g(g(m))))) == f(g(f(g(g(g(k)))))). [resolve(435,a,19,a)]. given #342 (T,wt=14): 692 g(f(f(g(g(m))))) == g(f(f(g(g(g(k)))))). [resolve(436,a,20,a)]. given #343 (T,wt=14): 693 f(f(f(g(g(m))))) == f(f(f(g(g(g(k)))))). [resolve(436,a,19,a)]. given #344 (T,wt=14): 702 g(g(g(f(g(m))))) == g(g(g(f(g(g(k)))))). [resolve(445,a,20,a)]. given #345 (A,wt=27): 286 p(m,b) | g(m) == m | f(g(m)) == b | -p(f(g(m)),b) | g(m) == b | g(m) == f(g(m)). [resolve(65,g,27,c),merge(g),merge(h)]. given #346 (T,wt=14): 703 f(g(g(f(g(m))))) == f(g(g(f(g(g(k)))))). [resolve(445,a,19,a)]. given #347 (T,wt=14): 709 g(f(g(f(g(m))))) == g(f(g(f(g(g(k)))))). [resolve(446,a,20,a)]. given #348 (T,wt=14): 710 f(f(g(f(g(m))))) == f(f(g(f(g(g(k)))))). [resolve(446,a,19,a)]. given #349 (T,wt=14): 719 g(g(f(f(g(m))))) == g(g(f(f(g(g(k)))))). [resolve(452,a,20,a)]. given #350 (A,wt=19): 287 p(g(f(f(m))),f(f(g(k)))) | f(f(m)) == b | p(f(f(m)),b). [resolve(206,a,39,a)]. given #351 (T,wt=14): 720 f(g(f(f(g(m))))) == f(g(f(f(g(g(k)))))). [resolve(452,a,19,a)]. given #352 (T,wt=14): 726 g(f(f(f(g(m))))) == g(f(f(f(g(g(k)))))). [resolve(453,a,20,a)]. given #353 (T,wt=14): 727 f(f(f(f(g(m))))) == f(f(f(f(g(g(k)))))). [resolve(453,a,19,a)]. given #354 (T,wt=14): 737 g(g(g(g(f(m))))) == g(g(g(g(f(g(k)))))). [resolve(462,a,20,a)]. given #355 (A,wt=19): 288 p(f(f(g(k))),g(f(f(m)))) | f(f(m)) == b | p(f(f(m)),b). [resolve(206,a,38,a)]. given #356 (T,wt=14): 738 f(g(g(g(f(m))))) == f(g(g(g(f(g(k)))))). [resolve(462,a,19,a)]. given #357 (T,wt=14): 744 g(f(g(g(f(m))))) == g(f(g(g(f(g(k)))))). [resolve(463,a,20,a)]. given #358 (T,wt=14): 745 f(f(g(g(f(m))))) == f(f(g(g(f(g(k)))))). [resolve(463,a,19,a)]. given #359 (T,wt=14): 754 g(g(f(g(f(m))))) == g(g(f(g(f(g(k)))))). [resolve(469,a,20,a)]. given #360 (A,wt=17): 293 p(f(g(k)),g(f(m))) | f(g(k)) == b | p(f(g(k)),b). [resolve(211,a,40,a)]. given #361 (T,wt=14): 755 f(g(f(g(f(m))))) == f(g(f(g(f(g(k)))))). [resolve(469,a,19,a)]. given #362 (T,wt=14): 761 g(f(f(g(f(m))))) == g(f(f(g(f(g(k)))))). [resolve(470,a,20,a)]. given #363 (T,wt=14): 762 f(f(f(g(f(m))))) == f(f(f(g(f(g(k)))))). [resolve(470,a,19,a)]. given #364 (T,wt=14): 772 g(g(g(f(f(m))))) == g(g(g(f(f(g(k)))))). [resolve(479,a,20,a)]. given #365 (A,wt=21): 294 p(g(g(f(g(k)))),g(f(m))) | g(f(g(k))) == b | p(g(f(g(k))),b). [resolve(211,a,39,a)]. given #366 (T,wt=14): 773 f(g(g(f(f(m))))) == f(g(g(f(f(g(k)))))). [resolve(479,a,19,a)]. given #367 (T,wt=14): 779 g(f(g(f(f(m))))) == g(f(g(f(f(g(k)))))). [resolve(480,a,20,a)]. given #368 (T,wt=14): 780 f(f(g(f(f(m))))) == f(f(g(f(f(g(k)))))). [resolve(480,a,19,a)]. given #369 (T,wt=14): 789 g(g(f(f(f(m))))) == g(g(f(f(f(g(k)))))). [resolve(486,a,20,a)]. given #370 (A,wt=21): 295 p(g(f(m)),g(g(f(g(k))))) | g(f(g(k))) == b | p(g(f(g(k))),b). [resolve(211,a,38,a)]. given #371 (T,wt=14): 790 f(g(f(f(f(m))))) == f(g(f(f(f(g(k)))))). [resolve(486,a,19,a)]. given #372 (T,wt=14): 796 g(f(f(f(f(m))))) == g(f(f(f(f(g(k)))))). [resolve(487,a,20,a)]. given #373 (T,wt=14): 797 f(f(f(f(f(m))))) == f(f(f(f(f(g(k)))))). [resolve(487,a,19,a)]. given #374 (T,wt=14): 811 g(g(g(g(f(g(k)))))) == g(g(g(g(f(m))))). [resolve(496,a,20,a)]. given #375 (A,wt=17): 296 p(g(f(m)),f(g(k))) | f(g(k)) == b | p(f(g(k)),b). [resolve(211,a,37,a)]. given #376 (T,wt=14): 812 f(g(g(g(f(g(k)))))) == f(g(g(g(f(m))))). [resolve(496,a,19,a)]. given #377 (T,wt=14): 818 g(f(g(g(f(g(k)))))) == g(f(g(g(f(m))))). [resolve(497,a,20,a)]. given #378 (T,wt=14): 819 f(f(g(g(f(g(k)))))) == f(f(g(g(f(m))))). [resolve(497,a,19,a)]. given #379 (T,wt=14): 828 g(g(f(g(f(g(k)))))) == g(g(f(g(f(m))))). [resolve(503,a,20,a)]. given #380 (A,wt=21): 301 p(g(f(f(g(k)))),f(f(m))) | f(f(g(k))) == b | p(f(f(g(k))),b). [resolve(212,a,39,a)]. given #381 (T,wt=14): 829 f(g(f(g(f(g(k)))))) == f(g(f(g(f(m))))). [resolve(503,a,19,a)]. given #382 (T,wt=14): 835 g(f(f(g(f(g(k)))))) == g(f(f(g(f(m))))). [resolve(504,a,20,a)]. given #383 (T,wt=14): 836 f(f(f(g(f(g(k)))))) == f(f(f(g(f(m))))). [resolve(504,a,19,a)]. given #384 (T,wt=14): 850 g(g(g(f(f(g(k)))))) == g(g(g(f(f(m))))). [resolve(513,a,20,a)]. given #385 (A,wt=21): 302 p(f(f(m)),g(f(f(g(k))))) | f(f(g(k))) == b | p(f(f(g(k))),b). [resolve(212,a,38,a)]. given #386 (T,wt=14): 851 f(g(g(f(f(g(k)))))) == f(g(g(f(f(m))))). [resolve(513,a,19,a)]. given #387 (T,wt=14): 857 g(f(g(f(f(g(k)))))) == g(f(g(f(f(m))))). [resolve(514,a,20,a)]. given #388 (T,wt=14): 858 f(f(g(f(f(g(k)))))) == f(f(g(f(f(m))))). [resolve(514,a,19,a)]. given #389 (T,wt=14): 867 g(g(f(f(f(g(k)))))) == g(g(f(f(f(m))))). [resolve(520,a,20,a)]. given #390 (A,wt=17): 307 p(g(g(k)),g(g(m))) | g(g(k)) == b | p(g(g(k)),b). [resolve(219,a,40,a)]. given #391 (T,wt=14): 868 f(g(f(f(f(g(k)))))) == f(g(f(f(f(m))))). [resolve(520,a,19,a)]. given #392 (T,wt=14): 874 g(f(f(f(f(g(k)))))) == g(f(f(f(f(m))))). [resolve(521,a,20,a)]. given #393 (T,wt=14): 875 f(f(f(f(f(g(k)))))) == f(f(f(f(f(m))))). [resolve(521,a,19,a)]. given #394 (T,wt=14): 889 g(g(g(g(g(g(k)))))) == g(g(g(g(g(m))))). [resolve(532,a,20,a)]. given #395 (A,wt=21): 308 p(g(g(g(g(k)))),g(g(m))) | g(g(g(k))) == b | p(g(g(g(k))),b). [resolve(219,a,39,a)]. given #396 (T,wt=14): 890 f(g(g(g(g(g(k)))))) == f(g(g(g(g(m))))). [resolve(532,a,19,a)]. given #397 (T,wt=14): 896 g(f(g(g(g(g(k)))))) == g(f(g(g(g(m))))). [resolve(533,a,20,a)]. given #398 (T,wt=14): 897 f(f(g(g(g(g(k)))))) == f(f(g(g(g(m))))). [resolve(533,a,19,a)]. given #399 (T,wt=14): 906 g(g(f(g(g(g(k)))))) == g(g(f(g(g(m))))). [resolve(539,a,20,a)]. given #400 (A,wt=21): 309 p(g(g(m)),g(g(g(g(k))))) | g(g(g(k))) == b | p(g(g(g(k))),b). [resolve(219,a,38,a)]. given #401 (T,wt=14): 907 f(g(f(g(g(g(k)))))) == f(g(f(g(g(m))))). [resolve(539,a,19,a)]. given #402 (T,wt=14): 913 g(f(f(g(g(g(k)))))) == g(f(f(g(g(m))))). [resolve(540,a,20,a)]. given #403 (T,wt=14): 914 f(f(f(g(g(g(k)))))) == f(f(f(g(g(m))))). [resolve(540,a,19,a)]. given #404 (T,wt=14): 923 g(g(g(f(g(g(k)))))) == g(g(g(f(g(m))))). [resolve(549,a,20,a)]. given #405 (A,wt=17): 310 p(g(g(m)),g(g(k))) | g(g(k)) == b | p(g(g(k)),b). [resolve(219,a,37,a)]. given #406 (T,wt=14): 924 f(g(g(f(g(g(k)))))) == f(g(g(f(g(m))))). [resolve(549,a,19,a)]. given #407 (T,wt=14): 930 g(f(g(f(g(g(k)))))) == g(f(g(f(g(m))))). [resolve(550,a,20,a)]. given #408 (T,wt=14): 931 f(f(g(f(g(g(k)))))) == f(f(g(f(g(m))))). [resolve(550,a,19,a)]. given #409 (T,wt=14): 940 g(g(f(f(g(g(k)))))) == g(g(f(f(g(m))))). [resolve(556,a,20,a)]. given #410 (A,wt=22): 315 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | p(g(x),g(k)). [resolve(89,f,168,a)]. given #411 (T,wt=14): 941 f(g(f(f(g(g(k)))))) == f(g(f(f(g(m))))). [resolve(556,a,19,a)]. given #412 (T,wt=14): 947 g(f(f(f(g(g(k)))))) == g(f(f(f(g(m))))). [resolve(557,a,20,a)]. given #413 (T,wt=14): 948 f(f(f(f(g(g(k)))))) == f(f(f(f(g(m))))). [resolve(557,a,19,a)]. given #414 (T,wt=14): 956 g(m) == b | p(g(m),b) | -(g(g(g(k))) == b). [factor(951,b,d)]. given #415 (A,wt=21): 316 p(g(f(g(g(k)))),f(g(m))) | f(g(g(k))) == b | p(f(g(g(k))),b). [resolve(220,a,39,a)]. given #416 (T,wt=14): 1001 f(m) == b | p(f(m),b) | -(g(f(g(k))) == b). [factor(996,b,d)]. given #417 (T,wt=15): 362 -p(m,b) | g(m) == b | g(m) == m | -p(g(m),m). [resolve(358,a,2,e),unit_del(a,21)]. given #418 (T,wt=15): 384 p(g(k),b) | g(g(k)) == m | -(f(g(g(k))) == m). [resolve(184,a,4,b)]. given #419 (T,wt=15): 563 p(m,b) | g(m) == b | -p(g(m),b) | m == g(m). [resolve(560,b,2,e),unit_del(d,21),unit_del(f,358)]. given #420 (A,wt=21): 317 p(f(g(m)),g(f(g(g(k))))) | f(g(g(k))) == b | p(f(g(g(k))),b). [resolve(220,a,38,a)]. given #421 (T,wt=15): 611 p(k,b) | g(m) == b | -p(g(m),b) | m == g(m). [resolve(604,b,2,e),unit_del(d,21),unit_del(f,358)]. given #422 (T,wt=15): 657 f(k) == k | f(k) == m | f(k) == b | p(b,m). [resolve(234,a,50,b)]. given #423 (T,wt=15): 658 f(k) == k | f(k) == m | f(k) == b | p(k,m). [resolve(234,a,49,b)]. given #424 (T,wt=15): 670 -(x == g(g(g(g(m))))) | x == g(g(g(g(g(k))))). [resolve(428,a,16,b)]. given #425 (A,wt=34): 332 g(g(k)) == b | p(g(g(k)),b) | g(g(g(k))) == m | g(g(k)) == m | g(g(k)) == g(g(g(k))) | p(g(g(m)),m). [resolve(90,f,219,a)]. given #426 (T,wt=15): 671 -(g(g(g(g(g(k))))) == x) | g(g(g(g(m)))) == x. [resolve(428,a,16,a)]. given #427 (T,wt=15): 677 -(x == f(g(g(g(m))))) | x == f(g(g(g(g(k))))). [resolve(429,a,16,b)]. given #428 (T,wt=15): 678 -(f(g(g(g(g(k))))) == x) | f(g(g(g(m)))) == x. [resolve(429,a,16,a)]. given #429 (T,wt=15): 687 -(x == g(f(g(g(m))))) | x == g(f(g(g(g(k))))). [resolve(435,a,16,b)]. given #430 (A,wt=34): 333 f(g(k)) == b | p(f(g(k)),b) | g(f(g(k))) == m | f(g(k)) == m | f(g(k)) == g(f(g(k))) | p(g(f(m)),m). [resolve(90,f,211,a)]. given #431 (T,wt=15): 688 -(g(f(g(g(g(k))))) == x) | g(f(g(g(m)))) == x. [resolve(435,a,16,a)]. given #432 (T,wt=15): 694 -(x == f(f(g(g(m))))) | x == f(f(g(g(g(k))))). [resolve(436,a,16,b)]. given #433 (T,wt=15): 695 -(f(f(g(g(g(k))))) == x) | f(f(g(g(m)))) == x. [resolve(436,a,16,a)]. given #434 (T,wt=15): 704 -(x == g(g(f(g(m))))) | x == g(g(f(g(g(k))))). [resolve(445,a,16,b)]. given #435 (A,wt=29): 334 f(m) == b | p(f(m),b) | g(f(m)) == m | f(m) == m | f(m) == g(f(m)) | p(g(f(g(k))),m). [resolve(90,f,205,a)]. given #436 (T,wt=15): 705 -(g(g(f(g(g(k))))) == x) | g(g(f(g(m)))) == x. [resolve(445,a,16,a)]. given #437 (T,wt=15): 711 -(x == f(g(f(g(m))))) | x == f(g(f(g(g(k))))). [resolve(446,a,16,b)]. given #438 (T,wt=15): 712 -(f(g(f(g(g(k))))) == x) | f(g(f(g(m)))) == x. [resolve(446,a,16,a)]. given #439 (T,wt=15): 721 -(x == g(f(f(g(m))))) | x == g(f(f(g(g(k))))). [resolve(452,a,16,b)]. given #440 (A,wt=29): 335 g(m) == b | p(g(m),b) | g(g(m)) == m | g(m) == m | g(m) == g(g(m)) | p(g(g(g(k))),m). [resolve(90,f,199,a)]. given #441 (T,wt=15): 722 -(g(f(f(g(g(k))))) == x) | g(f(f(g(m)))) == x. [resolve(452,a,16,a)]. given #442 (T,wt=15): 728 -(x == f(f(f(g(m))))) | x == f(f(f(g(g(k))))). [resolve(453,a,16,b)]. given #443 (T,wt=15): 729 -(f(f(f(g(g(k))))) == x) | f(f(f(g(m)))) == x. [resolve(453,a,16,a)]. given #444 (T,wt=15): 730 p(k,b) | f(k) == m | p(f(k),m) | k == f(k). [resolve(236,e,227,b),merge(e)]. given #445 (A,wt=18): 349 p(m,b) | g(g(k)) == b | -p(g(g(k)),b) | m == g(g(k)). [back_unit_del(261),unit_del(e,348)]. given #446 (T,wt=15): 739 -(x == g(g(g(f(m))))) | x == g(g(g(f(g(k))))). [resolve(462,a,16,b)]. given #447 (T,wt=15): 740 -(g(g(g(f(g(k))))) == x) | g(g(g(f(m)))) == x. [resolve(462,a,16,a)]. given #448 (T,wt=15): 746 -(x == f(g(g(f(m))))) | x == f(g(g(f(g(k))))). [resolve(463,a,16,b)]. given #449 (T,wt=15): 747 -(f(g(g(f(g(k))))) == x) | f(g(g(f(m)))) == x. [resolve(463,a,16,a)]. given #450 (A,wt=26): 350 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(g(x) == y) | p(f(g(x)),y). [resolve(91,f,18,b)]. given #451 (T,wt=15): 756 -(x == g(f(g(f(m))))) | x == g(f(g(f(g(k))))). [resolve(469,a,16,b)]. given #452 (T,wt=15): 757 -(g(f(g(f(g(k))))) == x) | g(f(g(f(m)))) == x. [resolve(469,a,16,a)]. given #453 (T,wt=15): 763 -(x == f(f(g(f(m))))) | x == f(f(g(f(g(k))))). [resolve(470,a,16,b)]. given #454 (T,wt=15): 764 -(f(f(g(f(g(k))))) == x) | f(f(g(f(m)))) == x. [resolve(470,a,16,a)]. given #455 (A,wt=26): 351 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == y) | p(y,g(x)). [resolve(91,f,17,b)]. given #456 (T,wt=15): 765 p(k,b) | f(k) == b | -p(f(k),b) | k == f(k). [resolve(239,e,226,b),merge(e)]. given #457 (T,wt=15): 774 -(x == g(g(f(f(m))))) | x == g(g(f(f(g(k))))). [resolve(479,a,16,b)]. given #458 (T,wt=15): 775 -(g(g(f(f(g(k))))) == x) | g(g(f(f(m)))) == x. [resolve(479,a,16,a)]. given #459 (T,wt=15): 781 -(x == f(g(f(f(m))))) | x == f(g(f(f(g(k))))). [resolve(480,a,16,b)]. given #460 (A,wt=43): 352 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | f(g(x)) == b | -p(f(g(x)),b) | g(x) == b | g(x) == f(g(x)) | -p(g(x),f(g(x))). [resolve(91,f,2,e)]. given #461 (T,wt=15): 782 -(f(g(f(f(g(k))))) == x) | f(g(f(f(m)))) == x. [resolve(480,a,16,a)]. given #462 (T,wt=15): 791 -(x == g(f(f(f(m))))) | x == g(f(f(f(g(k))))). [resolve(486,a,16,b)]. given #463 (T,wt=15): 792 -(g(f(f(f(g(k))))) == x) | g(f(f(f(m)))) == x. [resolve(486,a,16,a)]. given #464 (T,wt=15): 798 -(x == f(f(f(f(m))))) | x == f(f(f(f(g(k))))). [resolve(487,a,16,b)]. given #465 (A,wt=39): 353 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | f(g(x)) == m | p(f(g(x)),m) | g(x) == f(g(x)) | -p(g(x),f(g(x))). [resolve(91,f,1,e),merge(h)]. given #466 (T,wt=15): 799 -(f(f(f(f(g(k))))) == x) | f(f(f(f(m)))) == x. [resolve(487,a,16,a)]. given #467 (T,wt=15): 813 -(x == g(g(g(f(g(k)))))) | x == g(g(g(f(m)))). [resolve(496,a,16,b)]. given #468 (T,wt=15): 814 -(g(g(g(f(m)))) == x) | g(g(g(f(g(k))))) == x. [resolve(496,a,16,a)]. given #469 (T,wt=15): 820 -(x == f(g(g(f(g(k)))))) | x == f(g(g(f(m)))). [resolve(497,a,16,b)]. given #470 (A,wt=20): 356 g(g(k)) == b | -p(g(g(k)),b) | m == g(g(k)) | -p(g(g(k)),m). [resolve(348,a,2,f),unit_del(c,21)]. given #471 (T,wt=15): 821 -(f(g(g(f(m)))) == x) | f(g(g(f(g(k))))) == x. [resolve(497,a,16,a)]. given #472 (T,wt=15): 830 -(x == g(f(g(f(g(k)))))) | x == g(f(g(f(m)))). [resolve(503,a,16,b)]. given #473 (T,wt=15): 831 -(g(f(g(f(m)))) == x) | g(f(g(f(g(k))))) == x. [resolve(503,a,16,a)]. given #474 (T,wt=15): 837 -(x == f(f(g(f(g(k)))))) | x == f(f(g(f(m)))). [resolve(504,a,16,b)]. given #475 (A,wt=18): 357 -p(m,b) | g(g(k)) == b | g(g(k)) == m | -p(g(g(k)),m). [resolve(348,a,2,e),unit_del(a,21)]. given #476 (T,wt=15): 838 -(f(f(g(f(m)))) == x) | f(f(g(f(g(k))))) == x. [resolve(504,a,16,a)]. given #477 (T,wt=15): 852 -(x == g(g(f(f(g(k)))))) | x == g(g(f(f(m)))). [resolve(513,a,16,b)]. given #478 (T,wt=15): 853 -(g(g(f(f(m)))) == x) | g(g(f(f(g(k))))) == x. [resolve(513,a,16,a)]. given #479 (T,wt=15): 859 -(x == f(g(f(f(g(k)))))) | x == f(g(f(f(m)))). [resolve(514,a,16,b)]. given #480 (A,wt=16): 361 g(m) == b | -p(g(m),b) | m == g(m) | -p(g(m),m). [resolve(358,a,2,f),unit_del(c,21)]. given #481 (T,wt=15): 860 -(f(g(f(f(m)))) == x) | f(g(f(f(g(k))))) == x. [resolve(514,a,16,a)]. given #482 (T,wt=15): 869 -(x == g(f(f(f(g(k)))))) | x == g(f(f(f(m)))). [resolve(520,a,16,b)]. given #483 (T,wt=15): 870 -(g(f(f(f(m)))) == x) | g(f(f(f(g(k))))) == x. [resolve(520,a,16,a)]. given #484 (T,wt=15): 876 -(x == f(f(f(f(g(k)))))) | x == f(f(f(f(m)))). [resolve(521,a,16,b)]. given #485 (A,wt=26): 363 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == y) | p(g(x),y). [resolve(92,f,18,b)]. given #486 (T,wt=15): 877 -(f(f(f(f(m)))) == x) | f(f(f(f(g(k))))) == x. [resolve(521,a,16,a)]. given #487 (T,wt=15): 891 -(x == g(g(g(g(g(k)))))) | x == g(g(g(g(m)))). [resolve(532,a,16,b)]. given #488 (T,wt=15): 892 -(g(g(g(g(m)))) == x) | g(g(g(g(g(k))))) == x. [resolve(532,a,16,a)]. given #489 (T,wt=15): 898 -(x == f(g(g(g(g(k)))))) | x == f(g(g(g(m)))). [resolve(533,a,16,b)]. given #490 (A,wt=26): 364 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(g(x) == y) | p(y,f(g(x))). [resolve(92,f,17,b)]. given #491 (T,wt=15): 899 -(f(g(g(g(m)))) == x) | f(g(g(g(g(k))))) == x. [resolve(533,a,16,a)]. given #492 (T,wt=15): 908 -(x == g(f(g(g(g(k)))))) | x == g(f(g(g(m)))). [resolve(539,a,16,b)]. given #493 (T,wt=15): 909 -(g(f(g(g(m)))) == x) | g(f(g(g(g(k))))) == x. [resolve(539,a,16,a)]. given #494 (T,wt=15): 915 -(x == f(f(g(g(g(k)))))) | x == f(f(g(g(m)))). [resolve(540,a,16,b)]. given #495 (A,wt=43): 365 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | f(g(x)) == b | -p(f(g(x)),b) | g(x) == b | g(x) == f(g(x)) | -p(f(g(x)),g(x)). [resolve(92,f,2,f)]. given #496 (T,wt=15): 916 -(f(f(g(g(m)))) == x) | f(f(g(g(g(k))))) == x. [resolve(540,a,16,a)]. given #497 (T,wt=15): 925 -(x == g(g(f(g(g(k)))))) | x == g(g(f(g(m)))). [resolve(549,a,16,b)]. given #498 (T,wt=15): 926 -(g(g(f(g(m)))) == x) | g(g(f(g(g(k))))) == x. [resolve(549,a,16,a)]. given #499 (T,wt=15): 932 -(x == f(g(f(g(g(k)))))) | x == f(g(f(g(m)))). [resolve(550,a,16,b)]. given #500 (A,wt=16): 368 p(m,b) | g(m) == b | -p(g(m),b) | g(k) == g(m). [back_unit_del(245),unit_del(e,367)]. given #501 (T,wt=15): 933 -(f(g(f(g(m)))) == x) | f(g(f(g(g(k))))) == x. [resolve(550,a,16,a)]. given #502 (T,wt=15): 942 -(x == g(f(f(g(g(k)))))) | x == g(f(f(g(m)))). [resolve(556,a,16,b)]. given #503 (T,wt=15): 943 -(g(f(f(g(m)))) == x) | g(f(f(g(g(k))))) == x. [resolve(556,a,16,a)]. given #504 (T,wt=15): 949 -(x == f(f(f(g(g(k)))))) | x == f(f(f(g(m)))). [resolve(557,a,16,b)]. given #505 (A,wt=16): 369 p(m,b) | -p(g(k),b) | g(m) == b | g(m) == g(k). [back_unit_del(244),unit_del(e,367)]. given #506 (T,wt=15): 950 -(f(f(f(g(m)))) == x) | f(f(f(g(g(k))))) == x. [resolve(557,a,16,a)]. given #507 (T,wt=15): 1226 f(g(k)) == b | p(f(g(k)),b) | -(g(f(m)) == b). [factor(1221,b,d)]. given #508 (T,wt=15): 1464 g(g(k)) == b | p(g(g(k)),b) | -(g(g(m)) == b). [factor(1459,b,d)]. given #509 (T,wt=15): 1663 f(k) == k | f(k) == m | f(k) == b | -p(m,b). [resolve(658,d,54,b)]. given #510 (A,wt=18): 372 g(m) == b | -p(g(m),b) | g(k) == g(m) | -p(g(m),g(k)). [resolve(367,a,2,f),unit_del(c,178)]. given #511 (T,wt=15): 1664 f(k) == k | f(k) == m | f(k) == b | -p(k,b). [resolve(658,d,53,b)]. given #512 (T,wt=12): 1888 f(k) == k | f(k) == m | f(k) == b. [resolve(1664,d,234,a),merge(d),merge(e),merge(f)]. given #513 (T,wt=11): 1890 f(k) == m | f(k) == b | p(k,b). [resolve(1888,a,228,b)]. given #514 (T,wt=11): 1899 f(k) == m | f(k) == b | p(b,m). [resolve(1890,c,50,b)]. given #515 (A,wt=18): 373 -p(g(k),b) | g(m) == b | g(m) == g(k) | -p(g(m),g(k)). [resolve(367,a,2,e),unit_del(a,178)]. given #516 (T,wt=11): 1900 f(k) == m | f(k) == b | p(k,m). [resolve(1890,c,49,b)]. given #517 (T,wt=11): 1911 f(k) == m | f(k) == b | -p(m,b). [resolve(1900,c,54,b)]. given #518 (T,wt=11): 1912 f(k) == m | f(k) == b | -p(k,b). [resolve(1900,c,53,b)]. given #519 (T,wt=8): 1918 f(k) == m | f(k) == b. [resolve(1912,c,1890,c),merge(c),merge(d)]. given #520 (A,wt=22): 377 g(g(k)) == b | -p(g(g(k)),b) | g(k) == g(g(k)) | -p(g(g(k)),g(k)). [resolve(374,a,2,f),unit_del(c,178)]. given #521 (T,wt=7): 1919 f(k) == b | p(k,b). [resolve(1918,a,229,b)]. given #522 (T,wt=7): 1929 f(k) == b | p(b,m). [resolve(1919,b,50,b)]. given #523 (T,wt=7): 1930 f(k) == b | p(k,m). [resolve(1919,b,49,b)]. given #524 (T,wt=7): 1941 f(k) == b | -p(m,b). [resolve(1930,b,54,b)]. given #525 (A,wt=21): 378 -p(g(k),b) | g(g(k)) == b | g(g(k)) == g(k) | -p(g(g(k)),g(k)). [resolve(374,a,2,e),unit_del(a,178)]. given #526 (T,wt=7): 1942 f(k) == b | -p(k,b). [resolve(1930,b,53,b)]. ============================== PROOF ================================= % Proof 1 at 0.14 (+ 0.01) seconds. % Length of proof is 66. % Level of proof is 32. % Maximum clause weight is 18. % Given clauses 526. 1 x == m | p(x,m) | y == m | y == x | -p(x,y) | -p(y,x). [assumption]. 2 x == b | -p(x,b) | y == b | y == x | -p(x,y) | -p(y,x). [assumption]. 3 x == k | x == m | x == b | -p(x,k). [assumption]. 4 x == m | -p(x,m) | -(f(x) == m). [assumption]. 5 x == m | -p(x,m) | -(f(x) == x). [assumption]. 6 x == m | -p(x,m) | p(x,f(x)). [assumption]. 7 x == m | -p(x,m) | p(f(x),x). [assumption]. 9 x == b | p(x,b) | -(g(x) == x). [assumption]. 10 x == b | p(x,b) | p(x,g(x)). [assumption]. 11 x == b | p(x,b) | p(g(x),x). [assumption]. 12 x == k | -(x == m) | p(x,k). [assumption]. 13 x == k | -(x == b) | p(x,k). [assumption]. 14 x == x. [assumption]. 15 -(x == y) | y == x. [assumption]. 16 -(x == y) | -(y == z) | x == z. [assumption]. 18 -(x == y) | -p(z,x) | p(z,y). [assumption]. 21 -(m == b). [assumption]. 22 -(b == k). [assumption]. 23 -(k == m). [assumption]. 31 k == b | p(k,b) | g(k) == k | g(k) == m | g(k) == b. [resolve(11,c,3,d)]. 35 p(b,k). [resolve(14,a,13,b),unit_del(a,22)]. 36 m == k | p(m,k). [resolve(14,a,12,b)]. 40 -(g(x) == y) | p(x,y) | x == b | p(x,b). [resolve(18,b,10,c)]. 41 -(b == m). [ur(15,b,21,a)]. 42 -(k == b). [ur(15,b,22,a)]. 43 p(k,b) | g(k) == k | g(k) == m | g(k) == b. [back_unit_del(31),unit_del(a,42)]. 44 -(m == k). [ur(15,b,23,a)]. 45 p(m,k). [back_unit_del(36),unit_del(a,44)]. 49 p(k,m) | -p(k,b). [resolve(35,a,1,f),unit_del(a,23),unit_del(c,41),unit_del(d,22)]. 53 -p(k,b) | -p(k,m). [resolve(45,a,2,f),unit_del(a,42),unit_del(c,21),unit_del(d,44)]. 70 g(k) == k | g(k) == m | g(k) == b | p(k,m). [resolve(43,a,49,b)]. 81 g(k) == k | g(k) == m | g(k) == b | -p(k,b). [resolve(70,d,53,b)]. 88 g(k) == k | g(k) == m | g(k) == b. [resolve(81,d,43,a),merge(d),merge(e),merge(f)]. 104 g(k) == m | g(k) == b | p(k,b). [resolve(88,a,9,c),unit_del(c,42)]. 106 g(k) == m | g(k) == b | p(k,m). [resolve(104,c,49,b)]. 117 g(k) == m | g(k) == b | -p(k,b). [resolve(106,c,53,b)]. 132 g(k) == m | g(k) == b. [resolve(117,c,104,c),merge(c),merge(d)]. 133 g(k) == b | p(k,m) | p(k,b). [resolve(132,a,40,a),unit_del(c,42)]. 140 g(k) == b | m == g(k). [resolve(132,a,15,a)]. 142 m == g(k) | p(k,b). [resolve(140,a,40,a),merge(d),unit_del(c,42)]. 150 m == g(k) | p(k,m). [resolve(142,b,49,b)]. 161 m == g(k) | -p(k,b). [resolve(150,b,53,b)]. 168 m == g(k). [resolve(161,b,142,b),merge(b)]. 178 -(g(k) == b). [ur(16,a,168,a,c,21,a)]. 185 p(k,m) | p(k,b). [back_unit_del(133),unit_del(a,178)]. 226 p(k,b) | p(f(k),k). [resolve(185,a,7,b),unit_del(b,23)]. 227 p(k,b) | p(k,f(k)). [resolve(185,a,6,b),unit_del(b,23)]. 228 p(k,b) | -(f(k) == k). [resolve(185,a,5,b),unit_del(b,23)]. 229 p(k,b) | -(f(k) == m). [resolve(185,a,4,b),unit_del(b,23)]. 234 p(k,b) | f(k) == k | f(k) == m | f(k) == b. [resolve(226,b,3,d)]. 237 p(k,b) | -(f(k) == x) | p(k,x). [resolve(227,b,18,b)]. 241 p(k,b) | -(f(k) == b). [factor(237,a,c)]. 658 f(k) == k | f(k) == m | f(k) == b | p(k,m). [resolve(234,a,49,b)]. 1664 f(k) == k | f(k) == m | f(k) == b | -p(k,b). [resolve(658,d,53,b)]. 1888 f(k) == k | f(k) == m | f(k) == b. [resolve(1664,d,234,a),merge(d),merge(e),merge(f)]. 1890 f(k) == m | f(k) == b | p(k,b). [resolve(1888,a,228,b)]. 1900 f(k) == m | f(k) == b | p(k,m). [resolve(1890,c,49,b)]. 1912 f(k) == m | f(k) == b | -p(k,b). [resolve(1900,c,53,b)]. 1918 f(k) == m | f(k) == b. [resolve(1912,c,1890,c),merge(c),merge(d)]. 1919 f(k) == b | p(k,b). [resolve(1918,a,229,b)]. 1930 f(k) == b | p(k,m). [resolve(1919,b,49,b)]. 1942 f(k) == b | -p(k,b). [resolve(1930,b,53,b)]. 1949 f(k) == b. [resolve(1942,b,1919,b),merge(b)]. 1950 p(k,b). [back_unit_del(241),unit_del(b,1949)]. 1952 -p(k,m). [back_unit_del(53),unit_del(a,1950)]. 1954 $F. [back_unit_del(49),unit_del(a,1952),unit_del(b,1950)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=526. Generated=2867. Kept=1953. proofs=1. Usable=427. Sos=1229. Demods=0. Limbo=4, Disabled=316. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=913. Back_subsumed=275. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=18. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=87946. Nonunit_bsub_feature_tests=23394. Megabytes=1.99. User_CPU=0.14, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 21129 exit (max_proofs) Mon Mar 19 17:05:28 2007