============================== Prover9 =============================== Prover9 (32) version September-2006, September 2006. Process 26740 was started by mccune on cleo.thornwood, Wed Sep 13 14:36:53 2006 The command was "/home/mccune/LADR/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 (T,wt=3): 35 p(b,k). [resolve(14,a,13,b),unit_del(a,22)]. given #25 (T,wt=3): 45 p(m,k). [back_unit_del(36),unit_del(a,44)]. given #26 (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 #27 (F,wt=3): 41 -(b == m). [ur(15,b,21,a)]. given #28 (F,wt=3): 42 -(k == b). [ur(15,b,22,a)]. given #29 (T,wt=6): 46 -(k == x) | p(b,x). [resolve(35,a,18,b)]. given #30 (T,wt=6): 47 -(b == x) | p(x,k). [resolve(35,a,17,b)]. given #31 (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 #32 (F,wt=3): 44 -(m == k). [ur(15,b,23,a)]. given #33 (F,wt=6): 52 -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 (T,wt=6): 48 p(k,m) | -p(k,b). [resolve(35,a,1,f),unit_del(a,23),unit_del(c,41),unit_del(d,22)]. given #35 (T,wt=6): 49 p(b,m) | -p(k,b). [resolve(35,a,1,e),unit_del(a,41),unit_del(c,23),unit_del(d,42)]. given #36 (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 #37 (F,wt=6): 53 -p(m,b) | -p(k,m). [resolve(45,a,2,e),unit_del(a,21),unit_del(c,42),unit_del(d,23)]. given #38 (F,wt=6): 50 -(k == x) | p(m,x). [resolve(45,a,18,b)]. given #39 (T,wt=6): 51 -(m == x) | p(x,k). [resolve(45,a,17,b)]. 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 (A,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 (F,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 (F,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 (T,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 (A,wt=13): 39 -(x == y) | p(g(x),y) | x == b | p(x,b). [resolve(18,b,11,c)]. given #47 (F,wt=13): 40 -(g(x) == y) | p(x,y) | x == b | p(x,b). [resolve(18,b,10,c)]. given #48 (F,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 (T,wt=15): 69 g(k) == k | g(k) == m | g(k) == b | p(b,m). [resolve(43,a,49,b)]. given #50 (T,wt=15): 70 g(k) == k | g(k) == m | g(k) == b | p(k,m). [resolve(43,a,48,b)]. given #51 (A,wt=18): 54 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 #52 (F,wt=15): 80 g(k) == k | g(k) == m | g(k) == b | -p(m,b). [resolve(70,d,53,b)]. given #53 (F,wt=15): 81 g(k) == k | g(k) == m | g(k) == b | -p(k,b). [resolve(70,d,52,b)]. given #54 (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 #55 (T,wt=11): 97 g(k) == m | g(k) == b | p(k,b). [resolve(88,a,9,c),unit_del(c,42)]. given #56 (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 #57 (F,wt=11): 98 g(k) == m | g(k) == b | p(b,m). [resolve(97,c,49,b)]. given #58 (F,wt=11): 99 g(k) == m | g(k) == b | p(k,m). [resolve(97,c,48,b)]. given #59 (T,wt=11): 116 g(k) == m | g(k) == b | -p(m,b). [resolve(99,c,53,b)]. given #60 (T,wt=11): 117 g(k) == m | g(k) == b | -p(k,b). [resolve(99,c,52,b)]. given #61 (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 #62 (F,wt=8): 124 g(k) == m | g(k) == b. [resolve(117,c,97,c),merge(c),merge(d)]. given #63 (F,wt=8): 140 g(k) == b | m == g(k). [resolve(124,a,15,a)]. given #64 (T,wt=7): 142 m == g(k) | p(k,b). [resolve(140,a,40,a),merge(d),unit_del(c,42)]. given #65 (T,wt=7): 149 m == g(k) | p(b,m). [resolve(142,b,49,b)]. given #66 (A,wt=16): 57 p(m,b) | g(m) == m | -(g(m) == x) | p(f(g(m)),x). [resolve(27,c,18,b)]. given #67 (F,wt=7): 150 m == g(k) | p(k,m). [resolve(142,b,48,b)]. given #68 (F,wt=7): 160 m == g(k) | -p(m,b). [resolve(150,b,53,b)]. given #69 (T,wt=7): 161 m == g(k) | -p(k,b). [resolve(150,b,52,b)]. given #70 (T,wt=4): 168 m == g(k). [resolve(161,b,142,b),merge(b)]. given #71 (A,wt=16): 58 p(m,b) | g(m) == m | -(f(g(m)) == x) | p(x,g(m)). [resolve(27,c,17,b)]. given #72 (F,wt=4): 177 -(g(k) == k). [ur(16,a,168,a,c,44,a)]. given #73 (F,wt=4): 178 -(g(k) == b). [ur(16,a,168,a,c,21,a)]. given #74 (T,wt=4): 169 p(g(k),k). [resolve(168,a,51,a)]. given #75 (T,wt=4): 176 g(k) == m. [resolve(168,a,15,a)]. given #76 (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 #77 (F,wt=4): 186 -(k == g(k)). [ur(15,b,177,a)]. given #78 (F,wt=4): 187 -(b == g(k)). [ur(15,b,178,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 (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 #82 (F,wt=7): 190 -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 #83 (F,wt=8): 191 -p(g(k),b) | -p(k,g(k)). [resolve(169,a,2,e),unit_del(a,178),unit_del(c,42),unit_del(d,186)]. given #84 (T,wt=6): 181 f(g(k)) == f(m). [back_unit_del(137),unit_del(a,178)]. given #85 (T,wt=6): 182 g(g(k)) == g(m). [back_unit_del(136),unit_del(a,178)]. given #86 (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 #87 (F,wt=6): 185 p(k,m) | p(k,b). [back_unit_del(133),unit_del(a,178)]. given #88 (F,wt=6): 223 p(k,b) | -p(m,b). [resolve(185,a,53,b)]. given #89 (T,wt=7): 174 -(x == m) | x == g(k). [resolve(168,a,16,b)]. given #90 (T,wt=7): 175 -(g(k) == x) | m == x. [resolve(168,a,16,a)]. given #91 (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 #92 (F,wt=7): 179 -(m == x) | g(k) == x. [back_unit_del(139),unit_del(a,178)]. given #93 (F,wt=7): 180 -(x == g(k)) | x == m. [back_unit_del(138),unit_del(a,178)]. given #94 (T,wt=7): 188 -(k == x) | p(g(k),x). [resolve(169,a,18,b)]. given #95 (T,wt=7): 189 -(g(k) == x) | p(x,k). [resolve(169,a,17,b)]. given #96 (A,wt=16): 63 p(m,b) | g(m) == m | -(f(g(m)) == x) | p(g(m),x). [resolve(28,c,18,b)]. given #97 (F,wt=7): 226 p(k,b) | p(f(k),k). [resolve(185,a,7,b),unit_del(b,23)]. given #98 (F,wt=7): 227 p(k,b) | p(k,f(k)). [resolve(185,a,6,b),unit_del(b,23)]. given #99 (T,wt=7): 228 p(k,b) | -(f(k) == k). [resolve(185,a,5,b),unit_del(b,23)]. given #100 (T,wt=7): 229 p(k,b) | -(f(k) == m). [resolve(185,a,4,b),unit_del(b,23)]. given #101 (A,wt=16): 64 p(m,b) | g(m) == m | -(g(m) == x) | p(x,f(g(m))). [resolve(28,c,17,b)]. given #102 (F,wt=7): 240 p(k,b) | -(f(k) == b). [factor(236,a,c)]. given #103 (F,wt=8): 170 p(g(m),g(k)) | p(m,b). [resolve(168,a,39,a),unit_del(b,21)]. given #104 (T,wt=8): 171 p(g(k),g(m)) | p(m,b). [resolve(168,a,38,a),unit_del(b,21)]. given #105 (T,wt=8): 194 p(m,g(g(k))) | p(m,b). [resolve(172,a,40,a),unit_del(b,21)]. given #106 (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 #107 (F,wt=8): 197 p(g(g(k)),m) | p(m,b). [resolve(172,a,37,a),unit_del(b,21)]. given #108 (F,wt=8): 198 g(g(m)) == g(g(g(k))). [resolve(172,a,20,a)]. given #109 (T,wt=8): 199 f(g(m)) == f(g(g(k))). [resolve(172,a,19,a)]. given #110 (T,wt=8): 204 g(f(m)) == g(f(g(k))). [resolve(173,a,20,a)]. given #111 (A,wt=24): 103 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 #112 (F,wt=8): 205 f(f(m)) == f(f(g(k))). [resolve(173,a,19,a)]. given #113 (F,wt=8): 210 g(f(g(k))) == g(f(m)). [resolve(181,a,20,a)]. given #114 (T,wt=8): 211 f(f(g(k))) == f(f(m)). [resolve(181,a,19,a)]. given #115 (T,wt=8): 218 g(g(g(k))) == g(g(m)). [resolve(182,a,20,a)]. given #116 (A,wt=24): 104 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 #117 (F,wt=8): 219 f(g(g(k))) == f(g(m)). [resolve(182,a,19,a)]. given #118 (F,wt=8): 253 p(m,b) | -(g(g(k)) == b). [factor(250,a,c)]. given #119 (T,wt=9): 183 p(m,g(g(k))) | p(g(k),b). [back_unit_del(135),unit_del(a,178)]. given #120 (T,wt=8): 326 p(m,g(g(k))) | p(k,b). [resolve(183,b,54,d),unit_del(b,42),unit_del(d,178),unit_del(e,186)]. given #121 (A,wt=23): 105 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 #122 (F,wt=8): 330 p(m,g(g(k))) | p(b,m). [resolve(326,b,49,b)]. given #123 (F,wt=8): 331 p(m,g(g(k))) | p(k,m). [resolve(326,b,48,b)]. given #124 (T,wt=8): 343 p(m,g(g(k))) | -p(m,b). [resolve(331,b,53,b)]. given #125 (T,wt=8): 344 p(m,g(g(k))) | -p(k,b). [resolve(331,b,52,b)]. given #126 (A,wt=23): 106 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 #127 (F,wt=5): 351 p(m,g(g(k))). [resolve(344,b,326,b),merge(b)]. given #128 (F,wt=8): 357 -(g(g(k)) == x) | p(m,x). [resolve(351,a,18,b)]. given #129 (T,wt=4): 361 p(m,g(m)). [resolve(357,a,182,a)]. given #130 (T,wt=7): 362 -(g(m) == x) | p(m,x). [resolve(361,a,18,b)]. given #131 (A,wt=23): 107 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 #132 (F,wt=7): 363 -(m == x) | p(x,g(m)). [resolve(361,a,17,b)]. given #133 (F,wt=5): 366 p(g(k),g(m)). [resolve(363,a,168,a)]. given #134 (T,wt=8): 358 -(m == x) | p(x,g(g(k))). [resolve(351,a,17,b)]. given #135 (T,wt=6): 373 p(g(k),g(g(k))). [resolve(358,a,168,a)]. given #136 (A,wt=22): 108 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 #137 (F,wt=8): 369 -(g(m) == x) | p(g(k),x). [resolve(366,a,18,b)]. given #138 (F,wt=8): 370 -(g(k) == x) | p(x,g(m)). [resolve(366,a,17,b)]. given #139 (T,wt=9): 184 p(g(g(k)),m) | p(g(k),b). [back_unit_del(134),unit_del(a,178)]. given #140 (T,wt=9): 200 -(x == g(m)) | x == g(g(k)). [resolve(172,a,16,b)]. given #141 (A,wt=28): 109 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 #142 (F,wt=9): 201 -(g(g(k)) == x) | g(m) == x. [resolve(172,a,16,a)]. given #143 (F,wt=9): 206 -(x == f(m)) | x == f(g(k)). [resolve(173,a,16,b)]. given #144 (T,wt=9): 207 -(f(g(k)) == x) | f(m) == x. [resolve(173,a,16,a)]. given #145 (T,wt=9): 212 -(x == f(g(k))) | x == f(m). [resolve(181,a,16,b)]. given #146 (A,wt=23): 126 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(m == y) | p(x,y). [resolve(56,d,18,b)]. given #147 (F,wt=9): 213 -(f(m) == x) | f(g(k)) == x. [resolve(181,a,16,a)]. given #148 (F,wt=9): 217 p(g(m),g(k)) | p(g(k),b). [resolve(182,a,37,a),unit_del(b,178)]. given #149 (T,wt=8): 388 p(g(m),g(k)) | p(k,b). [resolve(217,b,54,d),unit_del(b,42),unit_del(d,178),unit_del(e,186)]. given #150 (T,wt=9): 220 -(x == g(g(k))) | x == g(m). [resolve(182,a,16,b)]. given #151 (A,wt=23): 127 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(x == y) | p(y,m). [resolve(56,d,17,b)]. given #152 (F,wt=9): 221 -(g(m) == x) | g(g(k)) == x. [resolve(182,a,16,a)]. given #153 (F,wt=9): 224 p(k,b) | -(m == x) | p(k,x). [resolve(185,a,18,b)]. given #154 (T,wt=7): 408 p(k,b) | p(k,g(k)). [resolve(224,b,168,a)]. given #155 (T,wt=7): 411 p(k,b) | -p(g(k),b). [resolve(408,b,2,f),unit_del(b,178),unit_del(d,42),unit_del(e,186),unit_del(f,169)]. given #156 (A,wt=21): 128 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 #157 (F,wt=9): 225 p(k,b) | -(k == x) | p(x,m). [resolve(185,a,17,b)]. given #158 (F,wt=9): 374 -(g(g(k)) == x) | p(g(k),x). [resolve(373,a,18,b)]. given #159 (T,wt=9): 375 -(g(k) == x) | p(x,g(g(k))). [resolve(373,a,17,b)]. given #160 (T,wt=9): 387 p(g(m),g(k)) | -p(k,g(k)). [resolve(217,b,191,a)]. given #161 (A,wt=21): 129 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 #162 (F,wt=10): 231 p(k,b) | -(k == x) | p(f(k),x). [resolve(226,b,18,b)]. given #163 (F,wt=10): 232 p(k,b) | -(f(k) == x) | p(x,k). [resolve(226,b,17,b)]. given #164 (T,wt=10): 236 p(k,b) | -(f(k) == x) | p(k,x). [resolve(227,b,18,b)]. given #165 (T,wt=10): 237 p(k,b) | -(k == x) | p(x,f(k)). [resolve(227,b,17,b)]. given #166 (A,wt=21): 130 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == x). [resolve(56,d,5,b),merge(f)]. given #167 (F,wt=10): 266 g(g(g(m))) == g(g(g(g(k)))). [resolve(198,a,20,a)]. given #168 (F,wt=10): 267 f(g(g(m))) == f(g(g(g(k)))). [resolve(198,a,19,a)]. given #169 (T,wt=10): 274 g(f(g(m))) == g(f(g(g(k)))). [resolve(199,a,20,a)]. given #170 (T,wt=10): 275 f(f(g(m))) == f(f(g(g(k)))). [resolve(199,a,19,a)]. given #171 (A,wt=21): 131 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == m). [resolve(56,d,4,b),merge(f)]. given #172 (F,wt=10): 282 g(g(f(m))) == g(g(f(g(k)))). [resolve(204,a,20,a)]. given #173 (F,wt=10): 283 f(g(f(m))) == f(g(f(g(k)))). [resolve(204,a,19,a)]. given #174 (T,wt=10): 289 g(f(f(m))) == g(f(f(g(k)))). [resolve(205,a,20,a)]. given #175 (T,wt=10): 290 f(f(f(m))) == f(f(f(g(k)))). [resolve(205,a,19,a)]. given #176 (A,wt=23): 132 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 #177 (F,wt=10): 297 g(g(f(g(k)))) == g(g(f(m))). [resolve(210,a,20,a)]. given #178 (F,wt=10): 298 f(g(f(g(k)))) == f(g(f(m))). [resolve(210,a,19,a)]. given #179 (T,wt=10): 303 g(f(f(g(k)))) == g(f(f(m))). [resolve(211,a,20,a)]. given #180 (T,wt=10): 304 f(f(f(g(k)))) == f(f(f(m))). [resolve(211,a,19,a)]. given #181 (A,wt=26): 192 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 #182 (F,wt=10): 311 g(g(g(g(k)))) == g(g(g(m))). [resolve(218,a,20,a)]. given #183 (F,wt=10): 312 f(g(g(g(k)))) == f(g(g(m))). [resolve(218,a,19,a)]. given #184 (T,wt=10): 321 g(f(g(g(k)))) == g(f(g(m))). [resolve(219,a,20,a)]. given #185 (T,wt=10): 322 f(f(g(g(k)))) == f(f(g(m))). [resolve(219,a,19,a)]. given #186 (A,wt=14): 193 p(m,b) | g(m) == m | p(f(g(m)),g(g(k))). [resolve(172,a,57,c)]. given #187 (F,wt=10): 409 p(k,b) | -(g(k) == x) | p(k,x). [resolve(408,b,18,b)]. given #188 (F,wt=10): 410 p(k,b) | -(k == x) | p(x,g(k)). [resolve(408,b,17,b)]. given #189 (T,wt=11): 242 p(m,b) | -(g(k) == x) | p(g(m),x). [resolve(170,a,18,b)]. given #190 (T,wt=7): 564 p(m,b) | p(g(m),m). [resolve(242,b,176,a)]. given #191 (A,wt=15): 195 p(g(g(m)),g(g(k))) | g(m) == b | p(g(m),b). [resolve(172,a,39,a)]. given #192 (F,wt=10): 565 p(m,b) | -(m == x) | p(g(m),x). [resolve(564,b,18,b)]. given #193 (F,wt=10): 566 p(m,b) | -(g(m) == x) | p(x,m). [resolve(564,b,17,b)]. given #194 (T,wt=11): 243 p(m,b) | -(g(m) == x) | p(x,g(k)). [resolve(170,a,17,b)]. given #195 (T,wt=9): 574 p(m,b) | p(g(g(k)),g(k)). [resolve(243,b,172,a)]. given #196 (A,wt=15): 196 p(g(g(k)),g(g(m))) | g(m) == b | p(g(m),b). [resolve(172,a,38,a)]. given #197 (F,wt=11): 255 p(m,b) | -(m == x) | p(g(g(k)),x). [resolve(197,a,18,b)]. given #198 (F,wt=11): 256 p(m,b) | -(g(g(k)) == x) | p(x,m). [resolve(197,a,17,b)]. given #199 (T,wt=11): 268 -(x == g(g(m))) | x == g(g(g(k))). [resolve(198,a,16,b)]. given #200 (T,wt=11): 269 -(g(g(g(k))) == x) | g(g(m)) == x. [resolve(198,a,16,a)]. given #201 (A,wt=15): 202 p(g(f(m)),f(g(k))) | f(m) == b | p(f(m),b). [resolve(173,a,39,a)]. given #202 (F,wt=11): 276 -(x == f(g(m))) | x == f(g(g(k))). [resolve(199,a,16,b)]. given #203 (F,wt=11): 277 -(f(g(g(k))) == x) | f(g(m)) == x. [resolve(199,a,16,a)]. given #204 (T,wt=11): 284 -(x == g(f(m))) | x == g(f(g(k))). [resolve(204,a,16,b)]. given #205 (T,wt=11): 285 -(g(f(g(k))) == x) | g(f(m)) == x. [resolve(204,a,16,a)]. given #206 (A,wt=15): 203 p(f(g(k)),g(f(m))) | f(m) == b | p(f(m),b). [resolve(173,a,38,a)]. given #207 (F,wt=11): 291 -(x == f(f(m))) | x == f(f(g(k))). [resolve(205,a,16,b)]. given #208 (F,wt=11): 292 -(f(f(g(k))) == x) | f(f(m)) == x. [resolve(205,a,16,a)]. given #209 (T,wt=11): 299 -(x == g(f(g(k)))) | x == g(f(m)). [resolve(210,a,16,b)]. given #210 (T,wt=11): 300 -(g(f(m)) == x) | g(f(g(k))) == x. [resolve(210,a,16,a)]. given #211 (A,wt=17): 208 p(g(f(g(k))),f(m)) | f(g(k)) == b | p(f(g(k)),b). [resolve(181,a,39,a)]. given #212 (F,wt=11): 305 -(x == f(f(g(k)))) | x == f(f(m)). [resolve(211,a,16,b)]. given #213 (F,wt=11): 306 -(f(f(m)) == x) | f(f(g(k))) == x. [resolve(211,a,16,a)]. given #214 (T,wt=11): 313 -(x == g(g(g(k)))) | x == g(g(m)). [resolve(218,a,16,b)]. given #215 (T,wt=11): 314 -(g(g(m)) == x) | g(g(g(k))) == x. [resolve(218,a,16,a)]. given #216 (A,wt=17): 209 p(f(m),g(f(g(k)))) | f(g(k)) == b | p(f(g(k)),b). [resolve(181,a,38,a)]. given #217 (F,wt=11): 323 -(x == f(g(g(k)))) | x == f(g(m)). [resolve(219,a,16,b)]. given #218 (F,wt=11): 324 -(f(g(m)) == x) | f(g(g(k))) == x. [resolve(219,a,16,a)]. given #219 (T,wt=11): 392 p(k,b) | -(g(k) == x) | p(g(m),x). [resolve(388,a,18,b)]. given #220 (T,wt=7): 608 p(k,b) | p(g(m),m). [resolve(392,b,176,a)]. given #221 (A,wt=17): 215 p(g(g(g(k))),g(m)) | g(g(k)) == b | p(g(g(k)),b). [resolve(182,a,39,a)]. given #222 (F,wt=10): 609 p(k,b) | -(m == x) | p(g(m),x). [resolve(608,b,18,b)]. given #223 (F,wt=10): 610 p(k,b) | -(g(m) == x) | p(x,m). [resolve(608,b,17,b)]. given #224 (T,wt=8): 622 p(k,b) | p(g(g(k)),m). [resolve(610,b,172,a)]. given #225 (T,wt=11): 393 p(k,b) | -(g(m) == x) | p(x,g(k)). [resolve(388,a,17,b)]. given #226 (A,wt=17): 216 p(g(m),g(g(g(k)))) | g(g(k)) == b | p(g(g(k)),b). [resolve(182,a,38,a)]. given #227 (F,wt=9): 630 p(k,b) | p(g(g(k)),g(k)). [resolve(393,b,172,a)]. given #228 (F,wt=11): 623 p(k,b) | -(m == x) | p(g(g(k)),x). [resolve(622,b,18,b)]. given #229 (T,wt=11): 624 p(k,b) | -(g(g(k)) == x) | p(x,m). [resolve(622,b,17,b)]. given #230 (T,wt=12): 378 p(g(k),b) | -(m == x) | p(g(g(k)),x). [resolve(184,a,18,b)]. given #231 (A,wt=23): 230 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 #232 (F,wt=10): 640 p(g(k),b) | p(g(g(k)),g(k)). [resolve(378,b,168,a)]. given #233 (F,wt=12): 379 p(g(k),b) | -(g(g(k)) == x) | p(x,m). [resolve(184,a,17,b)]. given #234 (T,wt=8): 651 p(g(k),b) | p(g(m),m). [resolve(379,b,182,a)]. given #235 (T,wt=8): 652 p(g(m),m) | -p(k,g(k)). [resolve(651,a,191,a)]. given #236 (A,wt=15): 233 p(k,b) | f(k) == k | f(k) == m | f(k) == b. [resolve(226,b,3,d)]. given #237 (F,wt=11): 653 p(g(m),m) | -(b == x) | p(g(k),x). [resolve(651,a,18,b)]. given #238 (F,wt=11): 654 p(g(m),m) | -(g(k) == x) | p(x,b). [resolve(651,a,17,b)]. given #239 (T,wt=12): 389 p(g(m),g(k)) | -(b == x) | p(g(k),x). [resolve(217,b,18,b)]. given #240 (T,wt=12): 390 p(g(m),g(k)) | -(g(k) == x) | p(x,b). [resolve(217,b,17,b)]. given #241 (A,wt=19): 234 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 #242 (F,wt=12): 427 g(g(g(g(m)))) == g(g(g(g(g(k))))). [resolve(266,a,20,a)]. given #243 (F,wt=12): 428 f(g(g(g(m)))) == f(g(g(g(g(k))))). [resolve(266,a,19,a)]. given #244 (T,wt=12): 434 g(f(g(g(m)))) == g(f(g(g(g(k))))). [resolve(267,a,20,a)]. given #245 (T,wt=12): 435 f(f(g(g(m)))) == f(f(g(g(g(k))))). [resolve(267,a,19,a)]. given #246 (A,wt=19): 235 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 #247 (F,wt=12): 444 g(g(f(g(m)))) == g(g(f(g(g(k))))). [resolve(274,a,20,a)]. given #248 (F,wt=12): 445 f(g(f(g(m)))) == f(g(f(g(g(k))))). [resolve(274,a,19,a)]. given #249 (T,wt=12): 451 g(f(f(g(m)))) == g(f(f(g(g(k))))). [resolve(275,a,20,a)]. given #250 (T,wt=12): 452 f(f(f(g(m)))) == f(f(f(g(g(k))))). [resolve(275,a,19,a)]. given #251 (A,wt=19): 238 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 #252 (F,wt=12): 461 g(g(g(f(m)))) == g(g(g(f(g(k))))). [resolve(282,a,20,a)]. given #253 (F,wt=12): 462 f(g(g(f(m)))) == f(g(g(f(g(k))))). [resolve(282,a,19,a)]. given #254 (T,wt=12): 468 g(f(g(f(m)))) == g(f(g(f(g(k))))). [resolve(283,a,20,a)]. given #255 (T,wt=12): 469 f(f(g(f(m)))) == f(f(g(f(g(k))))). [resolve(283,a,19,a)]. given #256 (A,wt=14): 241 p(m,b) | g(m) == m | p(g(g(k)),f(g(m))). [resolve(64,c,172,a)]. given #257 (F,wt=12): 478 g(g(f(f(m)))) == g(g(f(f(g(k))))). [resolve(289,a,20,a)]. given #258 (F,wt=12): 479 f(g(f(f(m)))) == f(g(f(f(g(k))))). [resolve(289,a,19,a)]. given #259 (T,wt=12): 485 g(f(f(f(m)))) == g(f(f(f(g(k))))). [resolve(290,a,20,a)]. given #260 (T,wt=12): 486 f(f(f(f(m)))) == f(f(f(f(g(k))))). [resolve(290,a,19,a)]. given #261 (A,wt=27): 254 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 #262 (F,wt=12): 497 g(g(g(f(g(k))))) == g(g(g(f(m)))). [resolve(297,a,20,a)]. given #263 (F,wt=12): 498 f(g(g(f(g(k))))) == f(g(g(f(m)))). [resolve(297,a,19,a)]. given #264 (T,wt=12): 504 g(f(g(f(g(k))))) == g(f(g(f(m)))). [resolve(298,a,20,a)]. given #265 (T,wt=12): 505 f(f(g(f(g(k))))) == f(f(g(f(m)))). [resolve(298,a,19,a)]. given #266 (A,wt=16): 257 p(m,b) | g(g(k)) == m | p(f(g(g(k))),g(g(k))). [resolve(197,a,7,b)]. given #267 (F,wt=12): 514 g(g(f(f(g(k))))) == g(g(f(f(m)))). [resolve(303,a,20,a)]. given #268 (F,wt=12): 515 f(g(f(f(g(k))))) == f(g(f(f(m)))). [resolve(303,a,19,a)]. given #269 (T,wt=12): 521 g(f(f(f(g(k))))) == g(f(f(f(m)))). [resolve(304,a,20,a)]. given #270 (T,wt=12): 522 f(f(f(f(g(k))))) == f(f(f(f(m)))). [resolve(304,a,19,a)]. given #271 (A,wt=16): 258 p(m,b) | g(g(k)) == m | p(g(g(k)),f(g(g(k)))). [resolve(197,a,6,b)]. given #272 (F,wt=12): 531 g(g(g(g(g(k))))) == g(g(g(g(m)))). [resolve(311,a,20,a)]. given #273 (F,wt=12): 532 f(g(g(g(g(k))))) == f(g(g(g(m)))). [resolve(311,a,19,a)]. given #274 (T,wt=12): 538 g(f(g(g(g(k))))) == g(f(g(g(m)))). [resolve(312,a,20,a)]. given #275 (T,wt=12): 539 f(f(g(g(g(k))))) == f(f(g(g(m)))). [resolve(312,a,19,a)]. given #276 (A,wt=16): 259 p(m,b) | g(g(k)) == m | -(f(g(g(k))) == g(g(k))). [resolve(197,a,5,b)]. given #277 (F,wt=12): 548 g(g(f(g(g(k))))) == g(g(f(g(m)))). [resolve(321,a,20,a)]. given #278 (F,wt=12): 549 f(g(f(g(g(k))))) == f(g(f(g(m)))). [resolve(321,a,19,a)]. given #279 (T,wt=12): 555 g(f(f(g(g(k))))) == g(f(f(g(m)))). [resolve(322,a,20,a)]. given #280 (T,wt=12): 556 f(f(f(g(g(k))))) == f(f(f(g(m)))). [resolve(322,a,19,a)]. given #281 (A,wt=14): 260 p(m,b) | g(g(k)) == m | -(f(g(g(k))) == m). [resolve(197,a,4,b)]. given #282 (F,wt=12): 575 p(m,b) | -(g(k) == x) | p(g(g(k)),x). [resolve(574,b,18,b)]. given #283 (F,wt=12): 576 p(m,b) | -(g(g(k)) == x) | p(x,g(k)). [resolve(574,b,17,b)]. given #284 (T,wt=12): 614 p(k,b) | g(m) == m | -(f(g(m)) == m). [resolve(608,b,4,b)]. given #285 (T,wt=12): 637 p(k,b) | -(g(k) == x) | p(g(g(k)),x). [resolve(630,b,18,b)]. given #286 (A,wt=15): 262 p(g(m),g(g(g(k)))) | g(m) == b | p(g(m),b). [resolve(198,a,40,a)]. given #287 (F,wt=12): 638 p(k,b) | -(g(g(k)) == x) | p(x,g(k)). [resolve(630,b,17,b)]. given #288 (F,wt=13): 429 -(x == g(g(g(m)))) | x == g(g(g(g(k)))). [resolve(266,a,16,b)]. given #289 (T,wt=13): 430 -(g(g(g(g(k)))) == x) | g(g(g(m))) == x. [resolve(266,a,16,a)]. given #290 (T,wt=13): 436 -(x == f(g(g(m)))) | x == f(g(g(g(k)))). [resolve(267,a,16,b)]. given #291 (A,wt=19): 263 p(g(g(g(m))),g(g(g(k)))) | g(g(m)) == b | p(g(g(m)),b). [resolve(198,a,39,a)]. given #292 (F,wt=13): 437 -(f(g(g(g(k)))) == x) | f(g(g(m))) == x. [resolve(267,a,16,a)]. given #293 (F,wt=13): 446 -(x == g(f(g(m)))) | x == g(f(g(g(k)))). [resolve(274,a,16,b)]. given #294 (T,wt=13): 447 -(g(f(g(g(k)))) == x) | g(f(g(m))) == x. [resolve(274,a,16,a)]. given #295 (T,wt=13): 453 -(x == f(f(g(m)))) | x == f(f(g(g(k)))). [resolve(275,a,16,b)]. given #296 (A,wt=19): 264 p(g(g(g(k))),g(g(g(m)))) | g(g(m)) == b | p(g(g(m)),b). [resolve(198,a,38,a)]. given #297 (F,wt=13): 454 -(f(f(g(g(k)))) == x) | f(f(g(m))) == x. [resolve(275,a,16,a)]. given #298 (F,wt=13): 463 -(x == g(g(f(m)))) | x == g(g(f(g(k)))). [resolve(282,a,16,b)]. given #299 (T,wt=13): 464 -(g(g(f(g(k)))) == x) | g(g(f(m))) == x. [resolve(282,a,16,a)]. given #300 (T,wt=13): 470 -(x == f(g(f(m)))) | x == f(g(f(g(k)))). [resolve(283,a,16,b)]. given #301 (A,wt=15): 265 p(g(g(g(k))),g(m)) | g(m) == b | p(g(m),b). [resolve(198,a,37,a)]. given #302 (F,wt=13): 471 -(f(g(f(g(k)))) == x) | f(g(f(m))) == x. [resolve(283,a,16,a)]. given #303 (F,wt=13): 480 -(x == g(f(f(m)))) | x == g(f(f(g(k)))). [resolve(289,a,16,b)]. given #304 (T,wt=13): 481 -(g(f(f(g(k)))) == x) | g(f(f(m))) == x. [resolve(289,a,16,a)]. given #305 (T,wt=13): 487 -(x == f(f(f(m)))) | x == f(f(f(g(k)))). [resolve(290,a,16,b)]. given #306 (A,wt=14): 270 p(m,b) | g(m) == m | p(g(m),f(g(g(k)))). [resolve(199,a,63,c)]. given #307 (F,wt=13): 488 -(f(f(f(g(k)))) == x) | f(f(f(m))) == x. [resolve(290,a,16,a)]. given #308 (F,wt=13): 499 -(x == g(g(f(g(k))))) | x == g(g(f(m))). [resolve(297,a,16,b)]. given #309 (T,wt=13): 500 -(g(g(f(m))) == x) | g(g(f(g(k)))) == x. [resolve(297,a,16,a)]. given #310 (T,wt=13): 506 -(x == f(g(f(g(k))))) | x == f(g(f(m))). [resolve(298,a,16,b)]. given #311 (A,wt=14): 271 p(m,b) | g(m) == m | p(f(g(g(k))),g(m)). [resolve(199,a,58,c)]. given #312 (F,wt=13): 507 -(f(g(f(m))) == x) | f(g(f(g(k)))) == x. [resolve(298,a,16,a)]. given #313 (F,wt=13): 516 -(x == g(f(f(g(k))))) | x == g(f(f(m))). [resolve(303,a,16,b)]. given #314 (T,wt=13): 517 -(g(f(f(m))) == x) | g(f(f(g(k)))) == x. [resolve(303,a,16,a)]. given #315 (T,wt=13): 523 -(x == f(f(f(g(k))))) | x == f(f(f(m))). [resolve(304,a,16,b)]. given #316 (A,wt=19): 272 p(g(f(g(m))),f(g(g(k)))) | f(g(m)) == b | p(f(g(m)),b). [resolve(199,a,39,a)]. given #317 (F,wt=13): 524 -(f(f(f(m))) == x) | f(f(f(g(k)))) == x. [resolve(304,a,16,a)]. given #318 (F,wt=13): 533 -(x == g(g(g(g(k))))) | x == g(g(g(m))). [resolve(311,a,16,b)]. given #319 (T,wt=13): 534 -(g(g(g(m))) == x) | g(g(g(g(k)))) == x. [resolve(311,a,16,a)]. given #320 (T,wt=13): 540 -(x == f(g(g(g(k))))) | x == f(g(g(m))). [resolve(312,a,16,b)]. given #321 (A,wt=19): 273 p(f(g(g(k))),g(f(g(m)))) | f(g(m)) == b | p(f(g(m)),b). [resolve(199,a,38,a)]. given #322 (F,wt=13): 541 -(f(g(g(m))) == x) | f(g(g(g(k)))) == x. [resolve(312,a,16,a)]. given #323 (F,wt=13): 550 -(x == g(f(g(g(k))))) | x == g(f(g(m))). [resolve(321,a,16,b)]. given #324 (T,wt=13): 551 -(g(f(g(m))) == x) | g(f(g(g(k)))) == x. [resolve(321,a,16,a)]. given #325 (T,wt=13): 557 -(x == f(f(g(g(k))))) | x == f(f(g(m))). [resolve(322,a,16,b)]. given #326 (A,wt=15): 278 p(f(m),g(f(g(k)))) | f(m) == b | p(f(m),b). [resolve(204,a,40,a)]. given #327 (F,wt=13): 558 -(f(f(g(m))) == x) | f(f(g(g(k)))) == x. [resolve(322,a,16,a)]. given #328 (F,wt=13): 611 p(k,b) | g(m) == m | p(f(g(m)),g(m)). [resolve(608,b,7,b)]. given #329 (T,wt=13): 612 p(k,b) | g(m) == m | p(g(m),f(g(m))). [resolve(608,b,6,b)]. given #330 (T,wt=13): 613 p(k,b) | g(m) == m | -(f(g(m)) == g(m)). [resolve(608,b,5,b)]. given #331 (A,wt=19): 279 p(g(g(f(m))),g(f(g(k)))) | g(f(m)) == b | p(g(f(m)),b). [resolve(204,a,39,a)]. given #332 (F,wt=13): 648 p(g(k),b) | -(g(k) == x) | p(g(g(k)),x). [resolve(640,b,18,b)]. given #333 (F,wt=13): 649 p(g(k),b) | -(g(g(k)) == x) | p(x,g(k)). [resolve(640,b,17,b)]. given #334 (T,wt=14): 628 p(k,b) | g(g(k)) == m | -(f(g(g(k))) == m). [resolve(622,b,4,b)]. given #335 (T,wt=14): 667 g(g(g(g(g(m))))) == g(g(g(g(g(g(k)))))). [resolve(427,a,20,a)]. given #336 (A,wt=19): 280 p(g(f(g(k))),g(g(f(m)))) | g(f(m)) == b | p(g(f(m)),b). [resolve(204,a,38,a)]. given #337 (F,wt=14): 668 f(g(g(g(g(m))))) == f(g(g(g(g(g(k)))))). [resolve(427,a,19,a)]. given #338 (F,wt=14): 674 g(f(g(g(g(m))))) == g(f(g(g(g(g(k)))))). [resolve(428,a,20,a)]. given #339 (T,wt=14): 675 f(f(g(g(g(m))))) == f(f(g(g(g(g(k)))))). [resolve(428,a,19,a)]. given #340 (T,wt=14): 684 g(g(f(g(g(m))))) == g(g(f(g(g(g(k)))))). [resolve(434,a,20,a)]. given #341 (A,wt=15): 281 p(g(f(g(k))),f(m)) | f(m) == b | p(f(m),b). [resolve(204,a,37,a)]. given #342 (F,wt=14): 685 f(g(f(g(g(m))))) == f(g(f(g(g(g(k)))))). [resolve(434,a,19,a)]. given #343 (F,wt=14): 691 g(f(f(g(g(m))))) == g(f(f(g(g(g(k)))))). [resolve(435,a,20,a)]. given #344 (T,wt=14): 692 f(f(f(g(g(m))))) == f(f(f(g(g(g(k)))))). [resolve(435,a,19,a)]. given #345 (T,wt=14): 702 g(g(g(f(g(m))))) == g(g(g(f(g(g(k)))))). [resolve(444,a,20,a)]. given #346 (A,wt=22): 286 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | p(g(x),g(k)). [resolve(103,f,168,a)]. given #347 (F,wt=14): 703 f(g(g(f(g(m))))) == f(g(g(f(g(g(k)))))). [resolve(444,a,19,a)]. given #348 (F,wt=14): 709 g(f(g(f(g(m))))) == g(f(g(f(g(g(k)))))). [resolve(445,a,20,a)]. given #349 (T,wt=14): 710 f(f(g(f(g(m))))) == f(f(g(f(g(g(k)))))). [resolve(445,a,19,a)]. given #350 (T,wt=14): 719 g(g(f(f(g(m))))) == g(g(f(f(g(g(k)))))). [resolve(451,a,20,a)]. given #351 (A,wt=19): 287 p(g(f(f(m))),f(f(g(k)))) | f(f(m)) == b | p(f(f(m)),b). [resolve(205,a,39,a)]. given #352 (F,wt=14): 720 f(g(f(f(g(m))))) == f(g(f(f(g(g(k)))))). [resolve(451,a,19,a)]. given #353 (F,wt=14): 726 g(f(f(f(g(m))))) == g(f(f(f(g(g(k)))))). [resolve(452,a,20,a)]. given #354 (T,wt=14): 727 f(f(f(f(g(m))))) == f(f(f(f(g(g(k)))))). [resolve(452,a,19,a)]. given #355 (T,wt=14): 737 g(g(g(g(f(m))))) == g(g(g(g(f(g(k)))))). [resolve(461,a,20,a)]. given #356 (A,wt=19): 288 p(f(f(g(k))),g(f(f(m)))) | f(f(m)) == b | p(f(f(m)),b). [resolve(205,a,38,a)]. given #357 (F,wt=14): 738 f(g(g(g(f(m))))) == f(g(g(g(f(g(k)))))). [resolve(461,a,19,a)]. given #358 (F,wt=14): 744 g(f(g(g(f(m))))) == g(f(g(g(f(g(k)))))). [resolve(462,a,20,a)]. given #359 (T,wt=14): 745 f(f(g(g(f(m))))) == f(f(g(g(f(g(k)))))). [resolve(462,a,19,a)]. given #360 (T,wt=14): 754 g(g(f(g(f(m))))) == g(g(f(g(f(g(k)))))). [resolve(468,a,20,a)]. given #361 (A,wt=17): 293 p(f(g(k)),g(f(m))) | f(g(k)) == b | p(f(g(k)),b). [resolve(210,a,40,a)]. given #362 (F,wt=14): 755 f(g(f(g(f(m))))) == f(g(f(g(f(g(k)))))). [resolve(468,a,19,a)]. given #363 (F,wt=14): 761 g(f(f(g(f(m))))) == g(f(f(g(f(g(k)))))). [resolve(469,a,20,a)]. given #364 (T,wt=14): 762 f(f(f(g(f(m))))) == f(f(f(g(f(g(k)))))). [resolve(469,a,19,a)]. given #365 (T,wt=14): 776 g(g(g(f(f(m))))) == g(g(g(f(f(g(k)))))). [resolve(478,a,20,a)]. given #366 (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(210,a,39,a)]. given #367 (F,wt=14): 777 f(g(g(f(f(m))))) == f(g(g(f(f(g(k)))))). [resolve(478,a,19,a)]. given #368 (F,wt=14): 783 g(f(g(f(f(m))))) == g(f(g(f(f(g(k)))))). [resolve(479,a,20,a)]. given #369 (T,wt=14): 784 f(f(g(f(f(m))))) == f(f(g(f(f(g(k)))))). [resolve(479,a,19,a)]. given #370 (T,wt=14): 793 g(g(f(f(f(m))))) == g(g(f(f(f(g(k)))))). [resolve(485,a,20,a)]. given #371 (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(210,a,38,a)]. given #372 (F,wt=14): 794 f(g(f(f(f(m))))) == f(g(f(f(f(g(k)))))). [resolve(485,a,19,a)]. given #373 (F,wt=14): 800 g(f(f(f(f(m))))) == g(f(f(f(f(g(k)))))). [resolve(486,a,20,a)]. given #374 (T,wt=14): 801 f(f(f(f(f(m))))) == f(f(f(f(f(g(k)))))). [resolve(486,a,19,a)]. given #375 (T,wt=14): 810 g(g(g(g(f(g(k)))))) == g(g(g(g(f(m))))). [resolve(497,a,20,a)]. given #376 (A,wt=17): 296 p(g(f(m)),f(g(k))) | f(g(k)) == b | p(f(g(k)),b). [resolve(210,a,37,a)]. given #377 (F,wt=14): 811 f(g(g(g(f(g(k)))))) == f(g(g(g(f(m))))). [resolve(497,a,19,a)]. given #378 (F,wt=14): 817 g(f(g(g(f(g(k)))))) == g(f(g(g(f(m))))). [resolve(498,a,20,a)]. given #379 (T,wt=14): 818 f(f(g(g(f(g(k)))))) == f(f(g(g(f(m))))). [resolve(498,a,19,a)]. given #380 (T,wt=14): 827 g(g(f(g(f(g(k)))))) == g(g(f(g(f(m))))). [resolve(504,a,20,a)]. given #381 (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(211,a,39,a)]. given #382 (F,wt=14): 828 f(g(f(g(f(g(k)))))) == f(g(f(g(f(m))))). [resolve(504,a,19,a)]. given #383 (F,wt=14): 834 g(f(f(g(f(g(k)))))) == g(f(f(g(f(m))))). [resolve(505,a,20,a)]. given #384 (T,wt=14): 835 f(f(f(g(f(g(k)))))) == f(f(f(g(f(m))))). [resolve(505,a,19,a)]. given #385 (T,wt=14): 849 g(g(g(f(f(g(k)))))) == g(g(g(f(f(m))))). [resolve(514,a,20,a)]. given #386 (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(211,a,38,a)]. given #387 (F,wt=14): 850 f(g(g(f(f(g(k)))))) == f(g(g(f(f(m))))). [resolve(514,a,19,a)]. given #388 (F,wt=14): 856 g(f(g(f(f(g(k)))))) == g(f(g(f(f(m))))). [resolve(515,a,20,a)]. given #389 (T,wt=14): 857 f(f(g(f(f(g(k)))))) == f(f(g(f(f(m))))). [resolve(515,a,19,a)]. given #390 (T,wt=14): 866 g(g(f(f(f(g(k)))))) == g(g(f(f(f(m))))). [resolve(521,a,20,a)]. given #391 (A,wt=17): 307 p(g(g(k)),g(g(m))) | g(g(k)) == b | p(g(g(k)),b). [resolve(218,a,40,a)]. given #392 (F,wt=14): 867 f(g(f(f(f(g(k)))))) == f(g(f(f(f(m))))). [resolve(521,a,19,a)]. given #393 (F,wt=14): 873 g(f(f(f(f(g(k)))))) == g(f(f(f(f(m))))). [resolve(522,a,20,a)]. given #394 (T,wt=14): 874 f(f(f(f(f(g(k)))))) == f(f(f(f(f(m))))). [resolve(522,a,19,a)]. given #395 (T,wt=14): 888 g(g(g(g(g(g(k)))))) == g(g(g(g(g(m))))). [resolve(531,a,20,a)]. given #396 (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(218,a,39,a)]. given #397 (F,wt=14): 889 f(g(g(g(g(g(k)))))) == f(g(g(g(g(m))))). [resolve(531,a,19,a)]. given #398 (F,wt=14): 895 g(f(g(g(g(g(k)))))) == g(f(g(g(g(m))))). [resolve(532,a,20,a)]. given #399 (T,wt=14): 896 f(f(g(g(g(g(k)))))) == f(f(g(g(g(m))))). [resolve(532,a,19,a)]. given #400 (T,wt=14): 905 g(g(f(g(g(g(k)))))) == g(g(f(g(g(m))))). [resolve(538,a,20,a)]. given #401 (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(218,a,38,a)]. given #402 (F,wt=14): 906 f(g(f(g(g(g(k)))))) == f(g(f(g(g(m))))). [resolve(538,a,19,a)]. given #403 (F,wt=14): 912 g(f(f(g(g(g(k)))))) == g(f(f(g(g(m))))). [resolve(539,a,20,a)]. given #404 (T,wt=14): 913 f(f(f(g(g(g(k)))))) == f(f(f(g(g(m))))). [resolve(539,a,19,a)]. given #405 (T,wt=14): 922 g(g(g(f(g(g(k)))))) == g(g(g(f(g(m))))). [resolve(548,a,20,a)]. given #406 (A,wt=17): 310 p(g(g(m)),g(g(k))) | g(g(k)) == b | p(g(g(k)),b). [resolve(218,a,37,a)]. given #407 (F,wt=14): 923 f(g(g(f(g(g(k)))))) == f(g(g(f(g(m))))). [resolve(548,a,19,a)]. given #408 (F,wt=14): 929 g(f(g(f(g(g(k)))))) == g(f(g(f(g(m))))). [resolve(549,a,20,a)]. given #409 (T,wt=14): 930 f(f(g(f(g(g(k)))))) == f(f(g(f(g(m))))). [resolve(549,a,19,a)]. given #410 (T,wt=14): 939 g(g(f(f(g(g(k)))))) == g(g(f(f(g(m))))). [resolve(555,a,20,a)]. given #411 (A,wt=34): 315 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(104,f,218,a)]. given #412 (F,wt=14): 940 f(g(f(f(g(g(k)))))) == f(g(f(f(g(m))))). [resolve(555,a,19,a)]. given #413 (F,wt=14): 946 g(f(f(f(g(g(k)))))) == g(f(f(f(g(m))))). [resolve(556,a,20,a)]. given #414 (T,wt=14): 947 f(f(f(f(g(g(k)))))) == f(f(f(f(g(m))))). [resolve(556,a,19,a)]. given #415 (T,wt=14): 955 g(m) == b | p(g(m),b) | -(g(g(g(k))) == b). [factor(950,b,d)]. given #416 (A,wt=34): 316 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(104,f,210,a)]. given #417 (F,wt=14): 1000 f(m) == b | p(f(m),b) | -(g(f(g(k))) == b). [factor(995,b,d)]. given #418 (F,wt=15): 365 -p(m,b) | g(m) == b | g(m) == m | -p(g(m),m). [resolve(361,a,2,e),unit_del(a,21)]. given #419 (T,wt=15): 383 p(g(k),b) | g(g(k)) == m | -(f(g(g(k))) == m). [resolve(184,a,4,b)]. given #420 (T,wt=15): 567 p(m,b) | g(m) == b | -p(g(m),b) | m == g(m). [resolve(564,b,2,e),unit_del(d,21),unit_del(f,361)]. given #421 (A,wt=29): 317 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(104,f,204,a)]. given #422 (F,wt=15): 615 p(k,b) | g(m) == b | -p(g(m),b) | m == g(m). [resolve(608,b,2,e),unit_del(d,21),unit_del(f,361)]. given #423 (F,wt=15): 656 f(k) == k | f(k) == m | f(k) == b | p(b,m). [resolve(233,a,49,b)]. given #424 (T,wt=15): 657 f(k) == k | f(k) == m | f(k) == b | p(k,m). [resolve(233,a,48,b)]. given #425 (T,wt=15): 669 -(x == g(g(g(g(m))))) | x == g(g(g(g(g(k))))). [resolve(427,a,16,b)]. given #426 (A,wt=29): 318 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(104,f,198,a)]. given #427 (F,wt=15): 670 -(g(g(g(g(g(k))))) == x) | g(g(g(g(m)))) == x. [resolve(427,a,16,a)]. given #428 (F,wt=15): 676 -(x == f(g(g(g(m))))) | x == f(g(g(g(g(k))))). [resolve(428,a,16,b)]. given #429 (T,wt=15): 677 -(f(g(g(g(g(k))))) == x) | f(g(g(g(m)))) == x. [resolve(428,a,16,a)]. given #430 (T,wt=15): 686 -(x == g(f(g(g(m))))) | x == g(f(g(g(g(k))))). [resolve(434,a,16,b)]. given #431 (A,wt=21): 319 p(g(f(g(g(k)))),f(g(m))) | f(g(g(k))) == b | p(f(g(g(k))),b). [resolve(219,a,39,a)]. given #432 (F,wt=15): 687 -(g(f(g(g(g(k))))) == x) | g(f(g(g(m)))) == x. [resolve(434,a,16,a)]. given #433 (F,wt=15): 693 -(x == f(f(g(g(m))))) | x == f(f(g(g(g(k))))). [resolve(435,a,16,b)]. given #434 (T,wt=15): 694 -(f(f(g(g(g(k))))) == x) | f(f(g(g(m)))) == x. [resolve(435,a,16,a)]. given #435 (T,wt=15): 695 p(k,b) | f(k) == m | p(f(k),m) | k == f(k). [resolve(235,e,227,b),merge(e)]. given #436 (A,wt=21): 320 p(f(g(m)),g(f(g(g(k))))) | f(g(g(k))) == b | p(f(g(g(k))),b). [resolve(219,a,38,a)]. given #437 (F,wt=15): 704 -(x == g(g(f(g(m))))) | x == g(g(f(g(g(k))))). [resolve(444,a,16,b)]. given #438 (F,wt=15): 705 -(g(g(f(g(g(k))))) == x) | g(g(f(g(m)))) == x. [resolve(444,a,16,a)]. given #439 (T,wt=15): 711 -(x == f(g(f(g(m))))) | x == f(g(f(g(g(k))))). [resolve(445,a,16,b)]. given #440 (T,wt=15): 712 -(f(g(f(g(g(k))))) == x) | f(g(f(g(m)))) == x. [resolve(445,a,16,a)]. given #441 (A,wt=26): 335 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(g(x) == y) | p(f(g(x)),y). [resolve(105,f,18,b)]. given #442 (F,wt=15): 721 -(x == g(f(f(g(m))))) | x == g(f(f(g(g(k))))). [resolve(451,a,16,b)]. given #443 (F,wt=15): 722 -(g(f(f(g(g(k))))) == x) | g(f(f(g(m)))) == x. [resolve(451,a,16,a)]. given #444 (T,wt=15): 728 -(x == f(f(f(g(m))))) | x == f(f(f(g(g(k))))). [resolve(452,a,16,b)]. given #445 (T,wt=15): 729 -(f(f(f(g(g(k))))) == x) | f(f(f(g(m)))) == x. [resolve(452,a,16,a)]. given #446 (A,wt=26): 336 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == y) | p(y,g(x)). [resolve(105,f,17,b)]. given #447 (F,wt=15): 730 p(k,b) | f(k) == b | -p(f(k),b) | k == f(k). [resolve(238,e,226,b),merge(e)]. given #448 (F,wt=15): 739 -(x == g(g(g(f(m))))) | x == g(g(g(f(g(k))))). [resolve(461,a,16,b)]. given #449 (T,wt=15): 740 -(g(g(g(f(g(k))))) == x) | g(g(g(f(m)))) == x. [resolve(461,a,16,a)]. given #450 (T,wt=15): 746 -(x == f(g(g(f(m))))) | x == f(g(g(f(g(k))))). [resolve(462,a,16,b)]. given #451 (A,wt=43): 337 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(105,f,2,e)]. given #452 (F,wt=15): 747 -(f(g(g(f(g(k))))) == x) | f(g(g(f(m)))) == x. [resolve(462,a,16,a)]. given #453 (F,wt=15): 756 -(x == g(f(g(f(m))))) | x == g(f(g(f(g(k))))). [resolve(468,a,16,b)]. given #454 (T,wt=15): 757 -(g(f(g(f(g(k))))) == x) | g(f(g(f(m)))) == x. [resolve(468,a,16,a)]. given #455 (T,wt=15): 763 -(x == f(f(g(f(m))))) | x == f(f(g(f(g(k))))). [resolve(469,a,16,b)]. given #456 (A,wt=39): 338 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(105,f,1,e),merge(h)]. given #457 (F,wt=15): 764 -(f(f(g(f(g(k))))) == x) | f(f(g(f(m)))) == x. [resolve(469,a,16,a)]. given #458 (F,wt=15): 778 -(x == g(g(f(f(m))))) | x == g(g(f(f(g(k))))). [resolve(478,a,16,b)]. given #459 (T,wt=15): 779 -(g(g(f(f(g(k))))) == x) | g(g(f(f(m)))) == x. [resolve(478,a,16,a)]. given #460 (T,wt=15): 785 -(x == f(g(f(f(m))))) | x == f(g(f(f(g(k))))). [resolve(479,a,16,b)]. given #461 (A,wt=18): 352 p(m,b) | g(g(k)) == b | -p(g(g(k)),b) | m == g(g(k)). [back_unit_del(261),unit_del(e,351)]. given #462 (F,wt=15): 786 -(f(g(f(f(g(k))))) == x) | f(g(f(f(m)))) == x. [resolve(479,a,16,a)]. given #463 (F,wt=15): 795 -(x == g(f(f(f(m))))) | x == g(f(f(f(g(k))))). [resolve(485,a,16,b)]. given #464 (T,wt=15): 796 -(g(f(f(f(g(k))))) == x) | g(f(f(f(m)))) == x. [resolve(485,a,16,a)]. given #465 (T,wt=15): 802 -(x == f(f(f(f(m))))) | x == f(f(f(f(g(k))))). [resolve(486,a,16,b)]. given #466 (A,wt=26): 353 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == y) | p(g(x),y). [resolve(106,f,18,b)]. given #467 (F,wt=15): 803 -(f(f(f(f(g(k))))) == x) | f(f(f(f(m)))) == x. [resolve(486,a,16,a)]. given #468 (F,wt=15): 812 -(x == g(g(g(f(g(k)))))) | x == g(g(g(f(m)))). [resolve(497,a,16,b)]. given #469 (T,wt=15): 813 -(g(g(g(f(m)))) == x) | g(g(g(f(g(k))))) == x. [resolve(497,a,16,a)]. given #470 (T,wt=15): 819 -(x == f(g(g(f(g(k)))))) | x == f(g(g(f(m)))). [resolve(498,a,16,b)]. given #471 (A,wt=26): 354 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(g(x) == y) | p(y,f(g(x))). [resolve(106,f,17,b)]. given #472 (F,wt=15): 820 -(f(g(g(f(m)))) == x) | f(g(g(f(g(k))))) == x. [resolve(498,a,16,a)]. given #473 (F,wt=15): 829 -(x == g(f(g(f(g(k)))))) | x == g(f(g(f(m)))). [resolve(504,a,16,b)]. given #474 (T,wt=15): 830 -(g(f(g(f(m)))) == x) | g(f(g(f(g(k))))) == x. [resolve(504,a,16,a)]. given #475 (T,wt=15): 836 -(x == f(f(g(f(g(k)))))) | x == f(f(g(f(m)))). [resolve(505,a,16,b)]. given #476 (A,wt=43): 355 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(106,f,2,f)]. given #477 (F,wt=15): 837 -(f(f(g(f(m)))) == x) | f(f(g(f(g(k))))) == x. [resolve(505,a,16,a)]. given #478 (F,wt=15): 851 -(x == g(g(f(f(g(k)))))) | x == g(g(f(f(m)))). [resolve(514,a,16,b)]. given #479 (T,wt=15): 852 -(g(g(f(f(m)))) == x) | g(g(f(f(g(k))))) == x. [resolve(514,a,16,a)]. given #480 (T,wt=15): 858 -(x == f(g(f(f(g(k)))))) | x == f(g(f(f(m)))). [resolve(515,a,16,b)]. given #481 (A,wt=20): 359 g(g(k)) == b | -p(g(g(k)),b) | m == g(g(k)) | -p(g(g(k)),m). [resolve(351,a,2,f),unit_del(c,21)]. given #482 (F,wt=15): 859 -(f(g(f(f(m)))) == x) | f(g(f(f(g(k))))) == x. [resolve(515,a,16,a)]. given #483 (F,wt=15): 868 -(x == g(f(f(f(g(k)))))) | x == g(f(f(f(m)))). [resolve(521,a,16,b)]. given #484 (T,wt=15): 869 -(g(f(f(f(m)))) == x) | g(f(f(f(g(k))))) == x. [resolve(521,a,16,a)]. given #485 (T,wt=15): 875 -(x == f(f(f(f(g(k)))))) | x == f(f(f(f(m)))). [resolve(522,a,16,b)]. given #486 (A,wt=18): 360 -p(m,b) | g(g(k)) == b | g(g(k)) == m | -p(g(g(k)),m). [resolve(351,a,2,e),unit_del(a,21)]. given #487 (F,wt=15): 876 -(f(f(f(f(m)))) == x) | f(f(f(f(g(k))))) == x. [resolve(522,a,16,a)]. given #488 (F,wt=15): 890 -(x == g(g(g(g(g(k)))))) | x == g(g(g(g(m)))). [resolve(531,a,16,b)]. given #489 (T,wt=15): 891 -(g(g(g(g(m)))) == x) | g(g(g(g(g(k))))) == x. [resolve(531,a,16,a)]. given #490 (T,wt=15): 897 -(x == f(g(g(g(g(k)))))) | x == f(g(g(g(m)))). [resolve(532,a,16,b)]. given #491 (A,wt=16): 364 g(m) == b | -p(g(m),b) | m == g(m) | -p(g(m),m). [resolve(361,a,2,f),unit_del(c,21)]. given #492 (F,wt=15): 898 -(f(g(g(g(m)))) == x) | f(g(g(g(g(k))))) == x. [resolve(532,a,16,a)]. given #493 (F,wt=15): 907 -(x == g(f(g(g(g(k)))))) | x == g(f(g(g(m)))). [resolve(538,a,16,b)]. given #494 (T,wt=15): 908 -(g(f(g(g(m)))) == x) | g(f(g(g(g(k))))) == x. [resolve(538,a,16,a)]. given #495 (T,wt=15): 914 -(x == f(f(g(g(g(k)))))) | x == f(f(g(g(m)))). [resolve(539,a,16,b)]. given #496 (A,wt=16): 367 p(m,b) | g(m) == b | -p(g(m),b) | g(k) == g(m). [back_unit_del(245),unit_del(e,366)]. given #497 (F,wt=15): 915 -(f(f(g(g(m)))) == x) | f(f(g(g(g(k))))) == x. [resolve(539,a,16,a)]. given #498 (F,wt=15): 924 -(x == g(g(f(g(g(k)))))) | x == g(g(f(g(m)))). [resolve(548,a,16,b)]. given #499 (T,wt=15): 925 -(g(g(f(g(m)))) == x) | g(g(f(g(g(k))))) == x. [resolve(548,a,16,a)]. given #500 (T,wt=15): 931 -(x == f(g(f(g(g(k)))))) | x == f(g(f(g(m)))). [resolve(549,a,16,b)]. given #501 (A,wt=16): 368 p(m,b) | -p(g(k),b) | g(m) == b | g(m) == g(k). [back_unit_del(244),unit_del(e,366)]. given #502 (F,wt=15): 932 -(f(g(f(g(m)))) == x) | f(g(f(g(g(k))))) == x. [resolve(549,a,16,a)]. given #503 (F,wt=15): 941 -(x == g(f(f(g(g(k)))))) | x == g(f(f(g(m)))). [resolve(555,a,16,b)]. given #504 (T,wt=15): 942 -(g(f(f(g(m)))) == x) | g(f(f(g(g(k))))) == x. [resolve(555,a,16,a)]. given #505 (T,wt=15): 948 -(x == f(f(f(g(g(k)))))) | x == f(f(f(g(m)))). [resolve(556,a,16,b)]. given #506 (A,wt=18): 371 g(m) == b | -p(g(m),b) | g(k) == g(m) | -p(g(m),g(k)). [resolve(366,a,2,f),unit_del(c,178)]. given #507 (F,wt=15): 949 -(f(f(f(g(m)))) == x) | f(f(f(g(g(k))))) == x. [resolve(556,a,16,a)]. given #508 (F,wt=15): 1228 f(g(k)) == b | p(f(g(k)),b) | -(g(f(m)) == b). [factor(1223,b,d)]. given #509 (T,wt=15): 1466 g(g(k)) == b | p(g(g(k)),b) | -(g(g(m)) == b). [factor(1461,b,d)]. given #510 (T,wt=15): 1673 f(k) == k | f(k) == m | f(k) == b | -p(m,b). [resolve(657,d,53,b)]. given #511 (A,wt=18): 372 -p(g(k),b) | g(m) == b | g(m) == g(k) | -p(g(m),g(k)). [resolve(366,a,2,e),unit_del(a,178)]. given #512 (F,wt=15): 1674 f(k) == k | f(k) == m | f(k) == b | -p(k,b). [resolve(657,d,52,b)]. given #513 (F,wt=12): 1888 f(k) == k | f(k) == m | f(k) == b. [resolve(1674,d,233,a),merge(d),merge(e),merge(f)]. given #514 (T,wt=11): 1890 f(k) == m | f(k) == b | p(k,b). [resolve(1888,a,228,b)]. given #515 (T,wt=11): 1899 f(k) == m | f(k) == b | p(b,m). [resolve(1890,c,49,b)]. given #516 (A,wt=22): 376 g(g(k)) == b | -p(g(g(k)),b) | g(k) == g(g(k)) | -p(g(g(k)),g(k)). [resolve(373,a,2,f),unit_del(c,178)]. given #517 (F,wt=11): 1900 f(k) == m | f(k) == b | p(k,m). [resolve(1890,c,48,b)]. given #518 (F,wt=11): 1910 f(k) == m | f(k) == b | -p(m,b). [resolve(1900,c,53,b)]. given #519 (T,wt=11): 1911 f(k) == m | f(k) == b | -p(k,b). [resolve(1900,c,52,b)]. given #520 (T,wt=8): 1917 f(k) == m | f(k) == b. [resolve(1911,c,1890,c),merge(c),merge(d)]. given #521 (A,wt=21): 377 -p(g(k),b) | g(g(k)) == b | g(g(k)) == g(k) | -p(g(g(k)),g(k)). [resolve(373,a,2,e),unit_del(a,178)]. given #522 (F,wt=7): 1918 f(k) == b | p(k,b). [resolve(1917,a,229,b)]. given #523 (F,wt=7): 1928 f(k) == b | p(b,m). [resolve(1918,b,49,b)]. given #524 (T,wt=7): 1929 f(k) == b | p(k,m). [resolve(1918,b,48,b)]. given #525 (T,wt=7): 1940 f(k) == b | -p(m,b). [resolve(1929,b,53,b)]. given #526 (A,wt=17): 380 p(g(k),b) | g(g(k)) == m | p(f(g(g(k))),g(g(k))). [resolve(184,a,7,b)]. given #527 (F,wt=7): 1941 f(k) == b | -p(k,b). [resolve(1929,b,52,b)]. ============================== PROOF ================================= % Proof 1 at 0.15 (+ 0.00) seconds. % Length of proof is 66. % Level of proof is 32. % Maximum clause weight is 18. % Given clauses 527. 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)]. 48 p(k,m) | -p(k,b). [resolve(35,a,1,f),unit_del(a,23),unit_del(c,41),unit_del(d,22)]. 52 -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,48,b)]. 81 g(k) == k | g(k) == m | g(k) == b | -p(k,b). [resolve(70,d,52,b)]. 88 g(k) == k | g(k) == m | g(k) == b. [resolve(81,d,43,a),merge(d),merge(e),merge(f)]. 97 g(k) == m | g(k) == b | p(k,b). [resolve(88,a,9,c),unit_del(c,42)]. 99 g(k) == m | g(k) == b | p(k,m). [resolve(97,c,48,b)]. 117 g(k) == m | g(k) == b | -p(k,b). [resolve(99,c,52,b)]. 124 g(k) == m | g(k) == b. [resolve(117,c,97,c),merge(c),merge(d)]. 133 g(k) == b | p(k,m) | p(k,b). [resolve(124,a,40,a),unit_del(c,42)]. 140 g(k) == b | m == g(k). [resolve(124,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,48,b)]. 161 m == g(k) | -p(k,b). [resolve(150,b,52,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)]. 233 p(k,b) | f(k) == k | f(k) == m | f(k) == b. [resolve(226,b,3,d)]. 236 p(k,b) | -(f(k) == x) | p(k,x). [resolve(227,b,18,b)]. 240 p(k,b) | -(f(k) == b). [factor(236,a,c)]. 657 f(k) == k | f(k) == m | f(k) == b | p(k,m). [resolve(233,a,48,b)]. 1674 f(k) == k | f(k) == m | f(k) == b | -p(k,b). [resolve(657,d,52,b)]. 1888 f(k) == k | f(k) == m | f(k) == b. [resolve(1674,d,233,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,48,b)]. 1911 f(k) == m | f(k) == b | -p(k,b). [resolve(1900,c,52,b)]. 1917 f(k) == m | f(k) == b. [resolve(1911,c,1890,c),merge(c),merge(d)]. 1918 f(k) == b | p(k,b). [resolve(1917,a,229,b)]. 1929 f(k) == b | p(k,m). [resolve(1918,b,48,b)]. 1941 f(k) == b | -p(k,b). [resolve(1929,b,52,b)]. 1953 f(k) == b. [resolve(1941,b,1918,b),merge(b)]. 1954 p(k,b). [back_unit_del(240),unit_del(b,1953)]. 1956 -p(k,m). [back_unit_del(52),unit_del(a,1954)]. 1958 $F. [back_unit_del(48),unit_del(a,1956),unit_del(b,1954)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=527. Generated=2872. Kept=1957. proofs=1. Usable=428. Sos=1233. Demods=0. Limbo=4, Disabled=315. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=914. Back_subsumed=275. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=17. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=87945. Nonunit_bsub_feature_tests=23558. Megabytes=1.90. User_CPU=0.15, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 26740 exit (max_proofs) Wed Sep 13 14:36:53 2006