============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11476 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:42 2006 The command was "/home/mccune/bin/prover9 -f wang.in wang2.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 wang2.in formulas(sos). -(m == b). b == k | k == m. y == j | -p(y,j) | y == k. y == j | p(y,j) | -(y == k). 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 | k == m. [assumption]. x == j | -p(x,j) | x == k. [assumption]. x == j | p(x,j) | -(x == k). [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, j, 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 | k == m. [assumption]. 23 x == j | -p(x,j) | x == k. [assumption]. 24 x == j | p(x,j) | -(x == k). [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=6): 22 b == k | k == m. [assumption]. given #23 (I,wt=9): 23 x == j | -p(x,j) | x == k. [assumption]. given #24 (I,wt=9): 24 x == j | p(x,j) | -(x == k). [assumption]. given #25 (T,wt=6): 36 b == k | p(b,k). [resolve(14,a,13,b)]. given #26 (A,wt=22): 25 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): 42 -(b == m). [ur(15,b,21,a)]. given #28 (F,wt=6): 37 m == k | p(m,k). [resolve(14,a,12,b)]. given #29 (T,wt=6): 47 b == k | m == k. [resolve(22,b,15,a)]. given #30 (T,wt=6): 49 k == j | p(k,j). [resolve(24,c,14,a)]. given #31 (A,wt=25): 26 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=8): 43 b == k | g(k) == g(m). [resolve(22,b,20,a)]. given #33 (F,wt=8): 44 b == k | f(k) == f(m). [resolve(22,b,19,a)]. given #34 (T,wt=8): 58 b == k | g(m) == g(k). [resolve(47,b,20,a)]. given #35 (T,wt=8): 59 b == k | f(m) == f(k). [resolve(47,b,19,a)]. given #36 (A,wt=24): 27 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=9): 45 b == k | -(x == k) | x == m. [resolve(22,b,16,b)]. given #38 (F,wt=9): 46 b == k | -(m == x) | k == x. [resolve(22,b,16,a)]. given #39 (T,wt=9): 50 b == k | -(k == x) | p(b,x). [resolve(36,b,18,b)]. given #40 (T,wt=6): 86 b == k | p(b,m). [resolve(50,b,22,b),merge(c)]. given #41 (A,wt=13): 28 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=7): 89 b == k | p(f(b),b). [resolve(86,b,7,b),unit_del(b,42)]. given #43 (F,wt=7): 90 b == k | p(b,f(b)). [resolve(86,b,6,b),unit_del(b,42)]. given #44 (T,wt=7): 91 b == k | -(f(b) == b). [resolve(86,b,5,b),unit_del(b,42)]. given #45 (T,wt=7): 92 b == k | -(f(b) == m). [resolve(86,b,4,b),unit_del(b,42)]. given #46 (A,wt=13): 29 p(m,b) | g(m) == m | p(g(m),f(g(m))). [resolve(11,c,6,b),unit_del(a,21)]. given #47 (F,wt=9): 51 b == k | -(b == x) | p(x,k). [resolve(36,b,17,b)]. given #48 (F,wt=9): 53 m == k | -(k == x) | p(m,x). [resolve(37,b,18,b)]. given #49 (T,wt=9): 54 m == k | -(m == x) | p(x,k). [resolve(37,b,17,b)]. given #50 (T,wt=9): 57 b == k | m == j | p(m,j). [resolve(47,b,24,c)]. given #51 (A,wt=13): 30 p(m,b) | g(m) == m | -(f(g(m)) == g(m)). [resolve(11,c,5,b),unit_del(a,21)]. given #52 (F,wt=9): 60 b == k | -(x == m) | x == k. [resolve(47,b,16,b)]. given #53 (F,wt=9): 61 b == k | -(k == x) | m == x. [resolve(47,b,16,a)]. given #54 (T,wt=9): 62 k == j | -(j == x) | p(k,x). [resolve(49,b,18,b)]. given #55 (T,wt=9): 63 k == j | -(k == x) | p(x,j). [resolve(49,b,17,b)]. given #56 (A,wt=12): 31 p(m,b) | g(m) == m | -(f(g(m)) == m). [resolve(11,c,4,b),unit_del(a,21)]. given #57 (F,wt=9): 87 b == k | -(m == x) | p(b,x). [resolve(86,b,18,b)]. given #58 (F,wt=9): 88 b == k | -(b == x) | p(x,m). [resolve(86,b,17,b)]. given #59 (T,wt=9): 116 k == j | p(m,j) | b == k. [resolve(63,b,22,b)]. given #60 (T,wt=10): 69 b == k | g(g(k)) == g(g(m)). [resolve(43,b,20,a)]. given #61 (A,wt=18): 32 k == b | p(k,b) | g(k) == k | g(k) == m | g(k) == b. [resolve(11,c,3,d)]. given #62 (F,wt=10): 70 b == k | f(g(k)) == f(g(m)). [resolve(43,b,19,a)]. given #63 (F,wt=10): 73 b == k | g(f(k)) == g(f(m)). [resolve(44,b,20,a)]. given #64 (T,wt=10): 74 b == k | f(f(k)) == f(f(m)). [resolve(44,b,19,a)]. given #65 (T,wt=10): 77 b == k | g(g(m)) == g(g(k)). [resolve(58,b,20,a)]. given #66 (A,wt=13): 38 -(g(x) == y) | p(y,x) | x == b | p(x,b). [resolve(17,b,11,c)]. given #67 (F,wt=10): 78 b == k | f(g(m)) == f(g(k)). [resolve(58,b,19,a)]. given #68 (F,wt=10): 81 b == k | g(f(m)) == g(f(k)). [resolve(59,b,20,a)]. given #69 (T,wt=10): 82 b == k | f(f(m)) == f(f(k)). [resolve(59,b,19,a)]. given #70 (T,wt=10): 99 b == k | -(b == x) | p(f(b),x). [resolve(89,b,18,b)]. given #71 (A,wt=13): 39 -(x == y) | p(y,g(x)) | x == b | p(x,b). [resolve(17,b,10,c)]. given #72 (F,wt=10): 100 b == k | -(f(b) == x) | p(x,b). [resolve(89,b,17,b)]. given #73 (F,wt=10): 103 b == k | -(f(b) == x) | p(b,x). [resolve(90,b,18,b)]. given #74 (T,wt=10): 104 b == k | -(b == x) | p(x,f(b)). [resolve(90,b,17,b)]. given #75 (T,wt=10): 147 p(g(k),m) | p(m,b) | b == k. [resolve(38,a,58,b),unit_del(b,21)]. given #76 (A,wt=13): 40 -(x == y) | p(g(x),y) | x == b | p(x,b). [resolve(18,b,11,c)]. given #77 (F,wt=10): 172 p(k,g(m)) | p(m,b) | b == k. [resolve(39,a,47,b),unit_del(b,21)]. given #78 (F,wt=10): 193 p(g(m),k) | p(m,b) | b == k. [resolve(40,a,47,b),unit_del(b,21)]. given #79 (T,wt=11): 71 b == k | -(x == g(k)) | x == g(m). [resolve(43,b,16,b)]. given #80 (T,wt=11): 72 b == k | -(g(m) == x) | g(k) == x. [resolve(43,b,16,a)]. given #81 (A,wt=13): 41 -(g(x) == y) | p(x,y) | x == b | p(x,b). [resolve(18,b,10,c)]. given #82 (F,wt=10): 210 p(m,g(k)) | p(m,b) | b == k. [resolve(41,a,58,b),unit_del(b,21)]. given #83 (F,wt=10): 215 p(m,b) | b == k | -(g(k) == b). [factor(212,a,d)]. given #84 (T,wt=11): 75 b == k | -(x == f(k)) | x == f(m). [resolve(44,b,16,b)]. given #85 (T,wt=11): 76 b == k | -(f(m) == x) | f(k) == x. [resolve(44,b,16,a)]. given #86 (A,wt=14): 48 g(j) == j | g(j) == k | j == b | p(j,b). [resolve(23,b,11,c)]. given #87 (F,wt=11): 79 b == k | -(x == g(m)) | x == g(k). [resolve(58,b,16,b)]. given #88 (F,wt=11): 80 b == k | -(g(k) == x) | g(m) == x. [resolve(58,b,16,a)]. given #89 (T,wt=11): 83 b == k | -(x == f(m)) | x == f(k). [resolve(59,b,16,b)]. given #90 (T,wt=11): 84 b == k | -(f(k) == x) | f(m) == x. [resolve(59,b,16,a)]. given #91 (A,wt=18): 52 x == b | p(x,b) | g(x) == b | -p(g(x),b) | x == g(x). [resolve(25,f,11,c),merge(f),merge(g)]. given #92 (F,wt=12): 55 m == k | k == b | -p(k,b) | -p(k,m). [resolve(37,b,2,f),merge(e),unit_del(d,21)]. given #93 (F,wt=12): 112 b == k | m == j | -(j == x) | p(m,x). [resolve(57,c,18,b)]. given #94 (T,wt=12): 113 b == k | m == j | -(m == x) | p(x,j). [resolve(57,c,17,b)]. given #95 (T,wt=9): 221 b == k | m == j | p(k,j). [resolve(113,c,47,b),merge(d)]. given #96 (A,wt=15): 56 m == k | -p(m,b) | k == b | k == m | -p(k,m). [resolve(37,b,2,e),unit_del(b,21)]. given #97 (F,wt=12): 117 k == j | b == k | -(j == x) | p(m,x). [resolve(116,b,18,b)]. given #98 (F,wt=12): 118 k == j | b == k | -(m == x) | p(x,j). [resolve(116,b,17,b)]. given #99 (T,wt=12): 120 b == k | g(g(g(k))) == g(g(g(m))). [resolve(69,b,20,a)]. given #100 (T,wt=12): 121 b == k | f(g(g(k))) == f(g(g(m))). [resolve(69,b,19,a)]. given #101 (A,wt=15): 64 k == j | j == b | -p(j,b) | k == b | -p(j,k). [resolve(49,b,2,f),merge(e)]. given #102 (F,wt=12): 128 b == k | g(f(g(k))) == g(f(g(m))). [resolve(70,b,20,a)]. given #103 (F,wt=12): 129 b == k | f(f(g(k))) == f(f(g(m))). [resolve(70,b,19,a)]. given #104 (T,wt=12): 132 b == k | g(g(f(k))) == g(g(f(m))). [resolve(73,b,20,a)]. given #105 (T,wt=12): 133 b == k | f(g(f(k))) == f(g(f(m))). [resolve(73,b,19,a)]. given #106 (A,wt=18): 65 k == j | k == b | -p(k,b) | j == b | j == k | -p(j,k). [resolve(49,b,2,e)]. given #107 (F,wt=12): 136 b == k | g(f(f(k))) == g(f(f(m))). [resolve(74,b,20,a)]. given #108 (F,wt=12): 137 b == k | f(f(f(k))) == f(f(f(m))). [resolve(74,b,19,a)]. given #109 (T,wt=12): 140 b == k | g(g(g(m))) == g(g(g(k))). [resolve(77,b,20,a)]. given #110 (T,wt=12): 141 b == k | f(g(g(m))) == f(g(g(k))). [resolve(77,b,19,a)]. given #111 (A,wt=15): 66 k == j | j == m | p(j,m) | k == m | -p(j,k). [resolve(49,b,1,f),merge(e)]. given #112 (F,wt=12): 149 b == k | g(f(g(m))) == g(f(g(k))). [resolve(78,b,20,a)]. given #113 (F,wt=12): 150 b == k | f(f(g(m))) == f(f(g(k))). [resolve(78,b,19,a)]. given #114 (T,wt=12): 154 b == k | g(g(f(m))) == g(g(f(k))). [resolve(81,b,20,a)]. given #115 (T,wt=12): 155 b == k | f(g(f(m))) == f(g(f(k))). [resolve(81,b,19,a)]. given #116 (A,wt=18): 67 k == j | k == m | p(k,m) | j == m | j == k | -p(j,k). [resolve(49,b,1,e)]. given #117 (F,wt=12): 158 b == k | g(f(f(m))) == g(f(f(k))). [resolve(82,b,20,a)]. given #118 (F,wt=12): 159 b == k | f(f(f(m))) == f(f(f(k))). [resolve(82,b,19,a)]. given #119 (T,wt=12): 222 b == k | m == j | -(j == x) | p(k,x). [resolve(221,c,18,b)]. given #120 (T,wt=12): 223 b == k | m == j | -(k == x) | p(x,j). [resolve(221,c,17,b)]. given #121 (A,wt=21): 68 x == b | p(x,b) | g(x) == m | p(g(x),m) | x == m | x == g(x). [resolve(26,g,11,c),merge(g),merge(h)]. given #122 (F,wt=13): 122 b == k | -(x == g(g(k))) | x == g(g(m)). [resolve(69,b,16,b)]. given #123 (F,wt=13): 123 b == k | -(g(g(m)) == x) | g(g(k)) == x. [resolve(69,b,16,a)]. given #124 (T,wt=13): 130 b == k | -(x == f(g(k))) | x == f(g(m)). [resolve(70,b,16,b)]. given #125 (T,wt=13): 131 b == k | -(f(g(m)) == x) | f(g(k)) == x. [resolve(70,b,16,a)]. given #126 (A,wt=20): 85 x == b | p(x,b) | x == m | p(x,m) | g(x) == m | g(x) == x. [resolve(27,g,11,c),merge(g),merge(h)]. given #127 (F,wt=13): 134 b == k | -(x == g(f(k))) | x == g(f(m)). [resolve(73,b,16,b)]. given #128 (F,wt=13): 135 b == k | -(g(f(m)) == x) | g(f(k)) == x. [resolve(73,b,16,a)]. given #129 (T,wt=13): 138 b == k | -(x == f(f(k))) | x == f(f(m)). [resolve(74,b,16,b)]. given #130 (T,wt=13): 139 b == k | -(f(f(m)) == x) | f(f(k)) == x. [resolve(74,b,16,a)]. given #131 (A,wt=16): 93 p(m,b) | g(m) == m | -(g(m) == x) | p(f(g(m)),x). [resolve(28,c,18,b)]. given #132 (F,wt=13): 142 b == k | -(x == g(g(m))) | x == g(g(k)). [resolve(77,b,16,b)]. given #133 (F,wt=13): 143 b == k | -(g(g(k)) == x) | g(g(m)) == x. [resolve(77,b,16,a)]. given #134 (T,wt=13): 148 p(g(m),k) | k == b | p(k,b) | b == k. [resolve(38,a,43,b)]. given #135 (T,wt=13): 151 b == k | -(x == f(g(m))) | x == f(g(k)). [resolve(78,b,16,b)]. given #136 (A,wt=16): 94 p(m,b) | g(m) == m | -(f(g(m)) == x) | p(x,g(m)). [resolve(28,c,17,b)]. given #137 (F,wt=13): 152 b == k | -(f(g(k)) == x) | f(g(m)) == x. [resolve(78,b,16,a)]. given #138 (F,wt=13): 156 b == k | -(x == g(f(m))) | x == g(f(k)). [resolve(81,b,16,b)]. given #139 (T,wt=13): 157 b == k | -(g(f(k)) == x) | g(f(m)) == x. [resolve(81,b,16,a)]. given #140 (T,wt=13): 160 b == k | -(x == f(f(m))) | x == f(f(k)). [resolve(82,b,16,b)]. given #141 (A,wt=32): 95 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(28,c,2,f)]. given #142 (F,wt=13): 161 b == k | -(f(f(k)) == x) | f(f(m)) == x. [resolve(82,b,16,a)]. given #143 (F,wt=13): 175 p(m,g(k)) | k == b | p(k,b) | b == k. [resolve(39,a,22,b)]. given #144 (T,wt=13): 176 p(m,b) | b == k | -(m == x) | p(g(k),x). [resolve(147,a,18,b)]. given #145 (T,wt=10): 362 p(m,b) | b == k | p(g(k),k). [resolve(176,c,47,b),merge(d)]. given #146 (A,wt=33): 96 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(28,c,2,e)]. given #147 (F,wt=13): 177 p(m,b) | b == k | -(g(k) == x) | p(x,m). [resolve(147,a,17,b)]. given #148 (F,wt=10): 368 p(m,b) | b == k | p(g(m),m). [resolve(177,c,43,b),merge(d)]. given #149 (T,wt=13): 196 p(g(k),m) | k == b | p(k,b) | b == k. [resolve(40,a,22,b)]. given #150 (T,wt=13): 197 p(m,b) | b == k | -(g(m) == x) | p(k,x). [resolve(172,a,18,b)]. given #151 (A,wt=28): 97 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(28,c,1,f),merge(c)]. given #152 (F,wt=10): 380 p(m,b) | b == k | p(k,g(k)). [resolve(197,c,58,b),merge(d)]. given #153 (F,wt=13): 198 p(m,b) | b == k | -(k == x) | p(x,g(m)). [resolve(172,a,17,b)]. given #154 (T,wt=10): 386 p(m,b) | b == k | p(m,g(m)). [resolve(198,c,22,b),merge(d)]. given #155 (T,wt=10): 390 p(m,b) | b == k | -(g(m) == b). [factor(387,a,d)]. given #156 (A,wt=29): 98 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(28,c,1,e),merge(e)]. given #157 (F,wt=13): 201 p(m,b) | b == k | -(k == x) | p(g(m),x). [resolve(193,a,18,b)]. given #158 (F,wt=13): 202 p(m,b) | b == k | -(g(m) == x) | p(x,k). [resolve(193,a,17,b)]. given #159 (T,wt=13): 211 p(k,g(m)) | k == b | p(k,b) | b == k. [resolve(41,a,43,b)]. given #160 (T,wt=13): 212 p(m,b) | b == k | -(g(k) == x) | p(m,x). [resolve(210,a,18,b)]. given #161 (A,wt=22): 101 b == k | f(b) == b | x == b | x == f(b) | -p(f(b),x) | -p(x,f(b)). [resolve(89,b,2,b)]. given #162 (F,wt=13): 213 p(m,b) | b == k | -(m == x) | p(x,g(k)). [resolve(210,a,17,b)]. given #163 (F,wt=13): 363 p(m,b) | b == k | -(k == x) | p(g(k),x). [resolve(362,c,18,b)]. given #164 (T,wt=13): 364 p(m,b) | b == k | -(g(k) == x) | p(x,k). [resolve(362,c,17,b)]. given #165 (T,wt=13): 369 p(m,b) | b == k | -(m == x) | p(g(m),x). [resolve(368,c,18,b)]. given #166 (A,wt=19): 102 b == k | f(b) == m | p(f(b),m) | b == f(b) | -p(b,f(b)). [resolve(89,b,1,e),unit_del(d,42)]. given #167 (F,wt=13): 370 p(m,b) | b == k | -(g(m) == x) | p(x,m). [resolve(368,c,17,b)]. given #168 (F,wt=13): 382 p(m,b) | b == k | -(g(k) == x) | p(k,x). [resolve(380,c,18,b)]. given #169 (T,wt=13): 383 p(m,b) | b == k | -(k == x) | p(x,g(k)). [resolve(380,c,17,b)]. given #170 (T,wt=13): 387 p(m,b) | b == k | -(g(m) == x) | p(m,x). [resolve(386,c,18,b)]. given #171 (A,wt=16): 106 p(m,b) | g(m) == m | -(f(g(m)) == x) | p(g(m),x). [resolve(29,c,18,b)]. given #172 (F,wt=13): 388 p(m,b) | b == k | -(m == x) | p(x,g(m)). [resolve(386,c,17,b)]. given #173 (F,wt=13): 395 k == b | p(k,b) | b == k | -(g(m) == b). [factor(392,b,e)]. given #174 (T,wt=14): 229 b == k | g(g(g(g(k)))) == g(g(g(g(m)))). [resolve(120,b,20,a)]. given #175 (T,wt=14): 230 b == k | f(g(g(g(k)))) == f(g(g(g(m)))). [resolve(120,b,19,a)]. given #176 (A,wt=16): 107 p(m,b) | g(m) == m | -(g(m) == x) | p(x,f(g(m))). [resolve(29,c,17,b)]. given #177 (F,wt=14): 235 b == k | g(f(g(g(k)))) == g(f(g(g(m)))). [resolve(121,b,20,a)]. given #178 (F,wt=14): 236 b == k | f(f(g(g(k)))) == f(f(g(g(m)))). [resolve(121,b,19,a)]. given #179 (T,wt=14): 243 b == k | g(g(f(g(k)))) == g(g(f(g(m)))). [resolve(128,b,20,a)]. given #180 (T,wt=14): 244 b == k | f(g(f(g(k)))) == f(g(f(g(m)))). [resolve(128,b,19,a)]. given #181 (A,wt=33): 108 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(29,c,2,f)]. given #182 (F,wt=14): 249 b == k | g(f(f(g(k)))) == g(f(f(g(m)))). [resolve(129,b,20,a)]. given #183 (F,wt=14): 250 b == k | f(f(f(g(k)))) == f(f(f(g(m)))). [resolve(129,b,19,a)]. given #184 (T,wt=14): 257 b == k | g(g(g(f(k)))) == g(g(g(f(m)))). [resolve(132,b,20,a)]. given #185 (T,wt=14): 258 b == k | f(g(g(f(k)))) == f(g(g(f(m)))). [resolve(132,b,19,a)]. given #186 (A,wt=15): 114 b == k | m == j | j == b | -p(j,b) | -p(j,m). [resolve(57,c,2,f),merge(f),unit_del(e,21)]. given #187 (F,wt=14): 263 b == k | g(f(g(f(k)))) == g(f(g(f(m)))). [resolve(133,b,20,a)]. given #188 (F,wt=14): 264 b == k | f(f(g(f(k)))) == f(f(g(f(m)))). [resolve(133,b,19,a)]. given #189 (T,wt=14): 271 b == k | g(g(f(f(k)))) == g(g(f(f(m)))). [resolve(136,b,20,a)]. given #190 (T,wt=14): 272 b == k | f(g(f(f(k)))) == f(g(f(f(m)))). [resolve(136,b,19,a)]. given #191 (A,wt=18): 115 b == k | m == j | -p(m,b) | j == b | j == m | -p(j,m). [resolve(57,c,2,e),unit_del(c,21)]. given #192 (F,wt=14): 277 b == k | g(f(f(f(k)))) == g(f(f(f(m)))). [resolve(137,b,20,a)]. given #193 (F,wt=14): 278 b == k | f(f(f(f(k)))) == f(f(f(f(m)))). [resolve(137,b,19,a)]. given #194 (T,wt=14): 285 b == k | g(g(g(g(m)))) == g(g(g(g(k)))). [resolve(140,b,20,a)]. given #195 (T,wt=14): 286 b == k | f(g(g(g(m)))) == f(g(g(g(k)))). [resolve(140,b,19,a)]. given #196 (A,wt=18): 119 k == j | b == k | -p(m,b) | j == b | j == m | -p(j,m). [resolve(116,b,2,e),unit_del(c,21)]. given #197 (F,wt=14): 291 b == k | g(f(g(g(m)))) == g(f(g(g(k)))). [resolve(141,b,20,a)]. given #198 (F,wt=14): 292 b == k | f(f(g(g(m)))) == f(f(g(g(k)))). [resolve(141,b,19,a)]. given #199 (T,wt=14): 299 b == k | g(g(f(g(m)))) == g(g(f(g(k)))). [resolve(149,b,20,a)]. given #200 (T,wt=14): 300 b == k | f(g(f(g(m)))) == f(g(f(g(k)))). [resolve(149,b,19,a)]. given #201 (A,wt=21): 124 k == b | g(k) == k | g(k) == m | g(k) == b | -(b == x) | p(k,x). [resolve(32,b,18,b)]. given #202 (F,wt=14): 305 b == k | g(f(f(g(m)))) == g(f(f(g(k)))). [resolve(150,b,20,a)]. given #203 (F,wt=14): 306 b == k | f(f(f(g(m)))) == f(f(f(g(k)))). [resolve(150,b,19,a)]. given #204 (T,wt=14): 313 b == k | g(g(g(f(m)))) == g(g(g(f(k)))). [resolve(154,b,20,a)]. given #205 (T,wt=14): 314 b == k | f(g(g(f(m)))) == f(g(g(f(k)))). [resolve(154,b,19,a)]. given #206 (A,wt=21): 125 k == b | g(k) == k | g(k) == m | g(k) == b | -(k == x) | p(x,b). [resolve(32,b,17,b)]. given #207 (F,wt=14): 319 b == k | g(f(g(f(m)))) == g(f(g(f(k)))). [resolve(155,b,20,a)]. given #208 (F,wt=14): 320 b == k | f(f(g(f(m)))) == f(f(g(f(k)))). [resolve(155,b,19,a)]. given #209 (T,wt=14): 327 b == k | g(g(f(f(m)))) == g(g(f(f(k)))). [resolve(158,b,20,a)]. given #210 (T,wt=14): 328 b == k | f(g(f(f(m)))) == f(g(f(f(k)))). [resolve(158,b,19,a)]. given #211 (A,wt=27): 126 k == b | g(k) == k | g(k) == m | g(k) == b | x == b | x == k | -p(k,x) | -p(x,k). [resolve(32,b,2,b),merge(e)]. given #212 (F,wt=14): 333 b == k | g(f(f(f(m)))) == g(f(f(f(k)))). [resolve(159,b,20,a)]. given #213 (F,wt=14): 334 b == k | f(f(f(f(m)))) == f(f(f(f(k)))). [resolve(159,b,19,a)]. given #214 (T,wt=15): 181 p(m,b) | b == k | g(k) == m | -(f(g(k)) == m). [resolve(147,a,4,b)]. given #215 (T,wt=15): 231 b == k | -(x == g(g(g(k)))) | x == g(g(g(m))). [resolve(120,b,16,b)]. given #216 (A,wt=24): 127 k == b | g(k) == k | g(k) == m | g(k) == b | p(b,m) | k == m | -p(b,k). [resolve(32,b,1,f),merge(h),unit_del(e,42)]. given #217 (F,wt=15): 232 b == k | -(g(g(g(m))) == x) | g(g(g(k))) == x. [resolve(120,b,16,a)]. given #218 (F,wt=15): 237 b == k | -(x == f(g(g(k)))) | x == f(g(g(m))). [resolve(121,b,16,b)]. given #219 (T,wt=15): 238 b == k | -(f(g(g(m))) == x) | f(g(g(k))) == x. [resolve(121,b,16,a)]. given #220 (T,wt=15): 245 b == k | -(x == g(f(g(k)))) | x == g(f(g(m))). [resolve(128,b,16,b)]. given #221 (A,wt=17): 144 p(g(g(k)),g(m)) | g(m) == b | p(g(m),b) | b == k. [resolve(38,a,77,b)]. given #222 (F,wt=15): 246 b == k | -(g(f(g(m))) == x) | g(f(g(k))) == x. [resolve(128,b,16,a)]. given #223 (F,wt=15): 251 b == k | -(x == f(f(g(k)))) | x == f(f(g(m))). [resolve(129,b,16,b)]. given #224 (T,wt=15): 252 b == k | -(f(f(g(m))) == x) | f(f(g(k))) == x. [resolve(129,b,16,a)]. given #225 (T,wt=15): 259 b == k | -(x == g(g(f(k)))) | x == g(g(f(m))). [resolve(132,b,16,b)]. given #226 (A,wt=17): 145 p(g(f(m)),f(k)) | f(k) == b | p(f(k),b) | b == k. [resolve(38,a,73,b)]. given #227 (F,wt=15): 260 b == k | -(g(g(f(m))) == x) | g(g(f(k))) == x. [resolve(132,b,16,a)]. given #228 (F,wt=15): 265 b == k | -(x == f(g(f(k)))) | x == f(g(f(m))). [resolve(133,b,16,b)]. given #229 (T,wt=15): 266 b == k | -(f(g(f(m))) == x) | f(g(f(k))) == x. [resolve(133,b,16,a)]. given #230 (T,wt=15): 273 b == k | -(x == g(f(f(k)))) | x == g(f(f(m))). [resolve(136,b,16,b)]. given #231 (A,wt=17): 146 p(g(g(m)),g(k)) | g(k) == b | p(g(k),b) | b == k. [resolve(38,a,69,b)]. given #232 (F,wt=15): 274 b == k | -(g(f(f(m))) == x) | g(f(f(k))) == x. [resolve(136,b,16,a)]. given #233 (F,wt=15): 279 b == k | -(x == f(f(f(k)))) | x == f(f(f(m))). [resolve(137,b,16,b)]. given #234 (T,wt=15): 280 b == k | -(f(f(f(m))) == x) | f(f(f(k))) == x. [resolve(137,b,16,a)]. given #235 (T,wt=15): 287 b == k | -(x == g(g(g(m)))) | x == g(g(g(k))). [resolve(140,b,16,b)]. given #236 (A,wt=17): 153 b == k | p(g(f(k)),f(m)) | f(m) == b | p(f(m),b). [resolve(81,b,38,a)]. given #237 (F,wt=15): 288 b == k | -(g(g(g(k))) == x) | g(g(g(m))) == x. [resolve(140,b,16,a)]. given #238 (F,wt=15): 293 b == k | -(x == f(g(g(m)))) | x == f(g(g(k))). [resolve(141,b,16,b)]. given #239 (T,wt=15): 294 b == k | -(f(g(g(k))) == x) | f(g(g(m))) == x. [resolve(141,b,16,a)]. given #240 (T,wt=15): 301 b == k | -(x == g(f(g(m)))) | x == g(f(g(k))). [resolve(149,b,16,b)]. given #241 (A,wt=21): 162 p(f(f(k)),g(f(f(m)))) | f(f(m)) == b | p(f(f(m)),b) | b == k. [resolve(39,a,82,b)]. given #242 (F,wt=15): 302 b == k | -(g(f(g(k))) == x) | g(f(g(m))) == x. [resolve(149,b,16,a)]. given #243 (F,wt=15): 307 b == k | -(x == f(f(g(m)))) | x == f(f(g(k))). [resolve(150,b,16,b)]. given #244 (T,wt=15): 308 b == k | -(f(f(g(k))) == x) | f(f(g(m))) == x. [resolve(150,b,16,a)]. given #245 (T,wt=15): 315 b == k | -(x == g(g(f(m)))) | x == g(g(f(k))). [resolve(154,b,16,b)]. given #246 (A,wt=21): 163 p(g(f(k)),g(g(f(m)))) | g(f(m)) == b | p(g(f(m)),b) | b == k. [resolve(39,a,81,b)]. given #247 (F,wt=15): 316 b == k | -(g(g(f(k))) == x) | g(g(f(m))) == x. [resolve(154,b,16,a)]. given #248 (F,wt=15): 321 b == k | -(x == f(g(f(m)))) | x == f(g(f(k))). [resolve(155,b,16,b)]. given #249 (T,wt=15): 322 b == k | -(f(g(f(k))) == x) | f(g(f(m))) == x. [resolve(155,b,16,a)]. given #250 (T,wt=15): 329 b == k | -(x == g(f(f(m)))) | x == g(f(f(k))). [resolve(158,b,16,b)]. given #251 (A,wt=21): 164 p(f(g(k)),g(f(g(m)))) | f(g(m)) == b | p(f(g(m)),b) | b == k. [resolve(39,a,78,b)]. given #252 (F,wt=15): 330 b == k | -(g(f(f(k))) == x) | g(f(f(m))) == x. [resolve(158,b,16,a)]. given #253 (F,wt=15): 335 b == k | -(x == f(f(f(m)))) | x == f(f(f(k))). [resolve(159,b,16,b)]. given #254 (T,wt=15): 336 b == k | -(f(f(f(k))) == x) | f(f(f(m))) == x. [resolve(159,b,16,a)]. given #255 (T,wt=15): 396 b == k | f(b) == m | p(f(b),m) | b == f(b). [resolve(102,e,90,b),merge(e)]. given #256 (A,wt=21): 165 p(g(g(k)),g(g(g(m)))) | g(g(m)) == b | p(g(g(m)),b) | b == k. [resolve(39,a,77,b)]. given #257 (F,wt=16): 178 p(m,b) | b == k | g(k) == m | p(f(g(k)),g(k)). [resolve(147,a,7,b)]. given #258 (F,wt=16): 179 p(m,b) | b == k | g(k) == m | p(g(k),f(g(k))). [resolve(147,a,6,b)]. given #259 (T,wt=16): 180 p(m,b) | b == k | g(k) == m | -(f(g(k)) == g(k)). [resolve(147,a,5,b)]. given #260 (T,wt=16): 352 p(m,b) | g(m) == m | p(f(g(m)),g(k)) | b == k. [resolve(93,c,58,b)]. given #261 (A,wt=21): 166 p(f(f(m)),g(f(f(k)))) | f(f(k)) == b | p(f(f(k)),b) | b == k. [resolve(39,a,74,b)]. given #262 (F,wt=16): 353 k == b | p(k,b) | b == k | -(k == x) | p(g(m),x). [resolve(148,a,18,b)]. given #263 (F,wt=13): 700 k == b | p(k,b) | b == k | p(g(m),m). [resolve(353,d,22,b),merge(e)]. given #264 (T,wt=16): 354 k == b | p(k,b) | b == k | -(g(m) == x) | p(x,k). [resolve(148,a,17,b)]. given #265 (T,wt=16): 357 p(m,b) | g(m) == m | p(f(g(k)),g(m)) | b == k. [resolve(94,c,78,b)]. given #266 (A,wt=21): 167 p(g(f(m)),g(g(f(k)))) | g(f(k)) == b | p(g(f(k)),b) | b == k. [resolve(39,a,73,b)]. given #267 (F,wt=16): 359 p(m,g(k)) | k == b | b == k | -(b == x) | p(k,x). [resolve(175,c,18,b)]. given #268 (F,wt=16): 360 p(m,g(k)) | k == b | b == k | -(k == x) | p(x,b). [resolve(175,c,17,b)]. given #269 (T,wt=16): 372 k == b | p(k,b) | b == k | -(m == x) | p(g(k),x). [resolve(196,a,18,b)]. given #270 (T,wt=16): 373 k == b | p(k,b) | b == k | -(g(k) == x) | p(x,m). [resolve(196,a,17,b)]. given #271 (A,wt=21): 168 p(f(g(m)),g(f(g(k)))) | f(g(k)) == b | p(f(g(k)),b) | b == k. [resolve(39,a,70,b)]. given #272 (F,wt=16): 392 k == b | p(k,b) | b == k | -(g(m) == x) | p(k,x). [resolve(211,a,18,b)]. given #273 (F,wt=16): 393 k == b | p(k,b) | b == k | -(k == x) | p(x,g(m)). [resolve(211,a,17,b)]. given #274 (T,wt=13): 723 k == b | p(k,b) | b == k | p(m,g(m)). [resolve(393,d,22,b),merge(e)]. given #275 (T,wt=16): 397 p(m,b) | g(m) == m | p(g(m),f(g(k))) | b == k. [resolve(106,c,78,b)]. given #276 (A,wt=21): 169 p(g(g(m)),g(g(g(k)))) | g(g(k)) == b | p(g(g(k)),b) | b == k. [resolve(39,a,69,b)]. given #277 (F,wt=16): 402 b == k | g(g(g(g(g(k))))) == g(g(g(g(g(m))))). [resolve(229,b,20,a)]. given #278 (F,wt=16): 403 b == k | f(g(g(g(g(k))))) == f(g(g(g(g(m))))). [resolve(229,b,19,a)]. given #279 (T,wt=16): 408 b == k | g(f(g(g(g(k))))) == g(f(g(g(g(m))))). [resolve(230,b,20,a)]. given #280 (T,wt=16): 409 b == k | f(f(g(g(g(k))))) == f(f(g(g(g(m))))). [resolve(230,b,19,a)]. given #281 (A,wt=17): 170 p(f(k),g(f(m))) | f(m) == b | p(f(m),b) | b == k. [resolve(39,a,59,b)]. given #282 (F,wt=16): 412 p(m,b) | g(m) == m | p(g(k),f(g(m))) | b == k. [resolve(107,c,58,b)]. given #283 (F,wt=16): 417 b == k | g(g(f(g(g(k))))) == g(g(f(g(g(m))))). [resolve(235,b,20,a)]. given #284 (T,wt=16): 418 b == k | f(g(f(g(g(k))))) == f(g(f(g(g(m))))). [resolve(235,b,19,a)]. given #285 (T,wt=16): 423 b == k | g(f(f(g(g(k))))) == g(f(f(g(g(m))))). [resolve(236,b,20,a)]. given #286 (A,wt=17): 171 p(g(k),g(g(m))) | g(m) == b | p(g(m),b) | b == k. [resolve(39,a,58,b)]. given #287 (F,wt=16): 424 b == k | f(f(f(g(g(k))))) == f(f(f(g(g(m))))). [resolve(236,b,19,a)]. given #288 (F,wt=16): 431 b == k | g(g(g(f(g(k))))) == g(g(g(f(g(m))))). [resolve(243,b,20,a)]. given #289 (T,wt=16): 432 b == k | f(g(g(f(g(k))))) == f(g(g(f(g(m))))). [resolve(243,b,19,a)]. given #290 (T,wt=16): 437 b == k | g(f(g(f(g(k))))) == g(f(g(f(g(m))))). [resolve(244,b,20,a)]. given #291 (A,wt=17): 173 p(f(m),g(f(k))) | f(k) == b | p(f(k),b) | b == k. [resolve(39,a,44,b)]. given #292 (F,wt=16): 438 b == k | f(f(g(f(g(k))))) == f(f(g(f(g(m))))). [resolve(244,b,19,a)]. given #293 (F,wt=16): 446 b == k | g(g(f(f(g(k))))) == g(g(f(f(g(m))))). [resolve(249,b,20,a)]. given #294 (T,wt=16): 447 b == k | f(g(f(f(g(k))))) == f(g(f(f(g(m))))). [resolve(249,b,19,a)]. given #295 (T,wt=16): 452 b == k | g(f(f(f(g(k))))) == g(f(f(f(g(m))))). [resolve(250,b,20,a)]. given #296 (A,wt=17): 174 p(g(m),g(g(k))) | g(k) == b | p(g(k),b) | b == k. [resolve(39,a,43,b)]. given #297 (F,wt=16): 453 b == k | f(f(f(f(g(k))))) == f(f(f(f(g(m))))). [resolve(250,b,19,a)]. given #298 (F,wt=16): 460 b == k | g(g(g(g(f(k))))) == g(g(g(g(f(m))))). [resolve(257,b,20,a)]. given #299 (T,wt=16): 461 b == k | f(g(g(g(f(k))))) == f(g(g(g(f(m))))). [resolve(257,b,19,a)]. given #300 (T,wt=16): 466 b == k | g(f(g(g(f(k))))) == g(f(g(g(f(m))))). [resolve(258,b,20,a)]. given #301 (A,wt=22): 182 p(m,b) | b == k | g(k) == b | -p(g(k),b) | m == g(k) | -p(m,g(k)). [resolve(147,a,2,e),unit_del(e,21)]. given #302 (F,wt=16): 467 b == k | f(f(g(g(f(k))))) == f(f(g(g(f(m))))). [resolve(258,b,19,a)]. given #303 (F,wt=16): 474 b == k | g(g(f(g(f(k))))) == g(g(f(g(f(m))))). [resolve(263,b,20,a)]. given #304 (T,wt=16): 475 b == k | f(g(f(g(f(k))))) == f(g(f(g(f(m))))). [resolve(263,b,19,a)]. given #305 (T,wt=16): 480 b == k | g(f(f(g(f(k))))) == g(f(f(g(f(m))))). [resolve(264,b,20,a)]. given #306 (A,wt=21): 183 p(g(f(f(m))),f(f(k))) | f(f(m)) == b | p(f(f(m)),b) | b == k. [resolve(40,a,82,b)]. given #307 (F,wt=16): 481 b == k | f(f(f(g(f(k))))) == f(f(f(g(f(m))))). [resolve(264,b,19,a)]. given #308 (F,wt=16): 488 b == k | g(g(g(f(f(k))))) == g(g(g(f(f(m))))). [resolve(271,b,20,a)]. given #309 (T,wt=16): 489 b == k | f(g(g(f(f(k))))) == f(g(g(f(f(m))))). [resolve(271,b,19,a)]. given #310 (T,wt=16): 494 b == k | g(f(g(f(f(k))))) == g(f(g(f(f(m))))). [resolve(272,b,20,a)]. given #311 (A,wt=21): 184 p(g(g(f(m))),g(f(k))) | g(f(m)) == b | p(g(f(m)),b) | b == k. [resolve(40,a,81,b)]. given #312 (F,wt=16): 495 b == k | f(f(g(f(f(k))))) == f(f(g(f(f(m))))). [resolve(272,b,19,a)]. given #313 (F,wt=16): 503 b == k | g(g(f(f(f(k))))) == g(g(f(f(f(m))))). [resolve(277,b,20,a)]. given #314 (T,wt=16): 504 b == k | f(g(f(f(f(k))))) == f(g(f(f(f(m))))). [resolve(277,b,19,a)]. given #315 (T,wt=16): 509 b == k | g(f(f(f(f(k))))) == g(f(f(f(f(m))))). [resolve(278,b,20,a)]. given #316 (A,wt=21): 185 p(g(f(g(m))),f(g(k))) | f(g(m)) == b | p(f(g(m)),b) | b == k. [resolve(40,a,78,b)]. given #317 (F,wt=16): 510 b == k | f(f(f(f(f(k))))) == f(f(f(f(f(m))))). [resolve(278,b,19,a)]. given #318 (F,wt=16): 517 b == k | g(g(g(g(g(m))))) == g(g(g(g(g(k))))). [resolve(285,b,20,a)]. given #319 (T,wt=16): 518 b == k | f(g(g(g(g(m))))) == f(g(g(g(g(k))))). [resolve(285,b,19,a)]. given #320 (T,wt=16): 523 b == k | g(f(g(g(g(m))))) == g(f(g(g(g(k))))). [resolve(286,b,20,a)]. given #321 (A,wt=21): 186 p(g(g(g(m))),g(g(k))) | g(g(m)) == b | p(g(g(m)),b) | b == k. [resolve(40,a,77,b)]. given #322 (F,wt=16): 524 b == k | f(f(g(g(g(m))))) == f(f(g(g(g(k))))). [resolve(286,b,19,a)]. given #323 (F,wt=16): 532 b == k | g(g(f(g(g(m))))) == g(g(f(g(g(k))))). [resolve(291,b,20,a)]. given #324 (T,wt=16): 533 b == k | f(g(f(g(g(m))))) == f(g(f(g(g(k))))). [resolve(291,b,19,a)]. given #325 (T,wt=16): 538 b == k | g(f(f(g(g(m))))) == g(f(f(g(g(k))))). [resolve(292,b,20,a)]. given #326 (A,wt=21): 187 p(g(f(f(k))),f(f(m))) | f(f(k)) == b | p(f(f(k)),b) | b == k. [resolve(40,a,74,b)]. given #327 (F,wt=16): 539 b == k | f(f(f(g(g(m))))) == f(f(f(g(g(k))))). [resolve(292,b,19,a)]. given #328 (F,wt=16): 546 b == k | g(g(g(f(g(m))))) == g(g(g(f(g(k))))). [resolve(299,b,20,a)]. given #329 (T,wt=16): 547 b == k | f(g(g(f(g(m))))) == f(g(g(f(g(k))))). [resolve(299,b,19,a)]. given #330 (T,wt=16): 552 b == k | g(f(g(f(g(m))))) == g(f(g(f(g(k))))). [resolve(300,b,20,a)]. given #331 (A,wt=21): 188 p(g(g(f(k))),g(f(m))) | g(f(k)) == b | p(g(f(k)),b) | b == k. [resolve(40,a,73,b)]. given #332 (F,wt=16): 553 b == k | f(f(g(f(g(m))))) == f(f(g(f(g(k))))). [resolve(300,b,19,a)]. given #333 (F,wt=16): 560 b == k | g(g(f(f(g(m))))) == g(g(f(f(g(k))))). [resolve(305,b,20,a)]. given #334 (T,wt=16): 561 b == k | f(g(f(f(g(m))))) == f(g(f(f(g(k))))). [resolve(305,b,19,a)]. given #335 (T,wt=16): 566 b == k | g(f(f(f(g(m))))) == g(f(f(f(g(k))))). [resolve(306,b,20,a)]. given #336 (A,wt=21): 189 p(g(f(g(k))),f(g(m))) | f(g(k)) == b | p(f(g(k)),b) | b == k. [resolve(40,a,70,b)]. given #337 (F,wt=16): 567 b == k | f(f(f(f(g(m))))) == f(f(f(f(g(k))))). [resolve(306,b,19,a)]. given #338 (F,wt=16): 574 b == k | g(g(g(g(f(m))))) == g(g(g(g(f(k))))). [resolve(313,b,20,a)]. given #339 (T,wt=16): 575 b == k | f(g(g(g(f(m))))) == f(g(g(g(f(k))))). [resolve(313,b,19,a)]. given #340 (T,wt=16): 580 b == k | g(f(g(g(f(m))))) == g(f(g(g(f(k))))). [resolve(314,b,20,a)]. given #341 (A,wt=21): 190 p(g(g(g(k))),g(g(m))) | g(g(k)) == b | p(g(g(k)),b) | b == k. [resolve(40,a,69,b)]. given #342 (F,wt=16): 581 b == k | f(f(g(g(f(m))))) == f(f(g(g(f(k))))). [resolve(314,b,19,a)]. given #343 (F,wt=16): 588 b == k | g(g(f(g(f(m))))) == g(g(f(g(f(k))))). [resolve(319,b,20,a)]. given #344 (T,wt=16): 589 b == k | f(g(f(g(f(m))))) == f(g(f(g(f(k))))). [resolve(319,b,19,a)]. given #345 (T,wt=16): 594 b == k | g(f(f(g(f(m))))) == g(f(f(g(f(k))))). [resolve(320,b,20,a)]. given #346 (A,wt=17): 191 p(g(f(m)),f(k)) | f(m) == b | p(f(m),b) | b == k. [resolve(40,a,59,b)]. given #347 (F,wt=16): 595 b == k | f(f(f(g(f(m))))) == f(f(f(g(f(k))))). [resolve(320,b,19,a)]. given #348 (F,wt=16): 602 b == k | g(g(g(f(f(m))))) == g(g(g(f(f(k))))). [resolve(327,b,20,a)]. given #349 (T,wt=16): 603 b == k | f(g(g(f(f(m))))) == f(g(g(f(f(k))))). [resolve(327,b,19,a)]. given #350 (T,wt=16): 608 b == k | g(f(g(f(f(m))))) == g(f(g(f(f(k))))). [resolve(328,b,20,a)]. given #351 (A,wt=17): 192 p(g(g(m)),g(k)) | g(m) == b | p(g(m),b) | b == k. [resolve(40,a,58,b)]. given #352 (F,wt=16): 609 b == k | f(f(g(f(f(m))))) == f(f(g(f(f(k))))). [resolve(328,b,19,a)]. given #353 (F,wt=16): 619 b == k | g(g(f(f(f(m))))) == g(g(f(f(f(k))))). [resolve(333,b,20,a)]. given #354 (T,wt=16): 620 b == k | f(g(f(f(f(m))))) == f(g(f(f(f(k))))). [resolve(333,b,19,a)]. given #355 (T,wt=16): 625 b == k | g(f(f(f(f(m))))) == g(f(f(f(f(k))))). [resolve(334,b,20,a)]. given #356 (A,wt=17): 194 p(g(f(k)),f(m)) | f(k) == b | p(f(k),b) | b == k. [resolve(40,a,44,b)]. given #357 (F,wt=16): 626 b == k | f(f(f(f(f(m))))) == f(f(f(f(f(k))))). [resolve(334,b,19,a)]. given #358 (F,wt=16): 673 b == k | f(b) == m | b == f(b) | -(f(f(b)) == m). [resolve(396,c,4,b),merge(d)]. given #359 (T,wt=16): 701 k == b | p(k,b) | b == k | -(m == x) | p(g(m),x). [resolve(700,d,18,b)]. given #360 (T,wt=16): 702 k == b | p(k,b) | b == k | -(g(m) == x) | p(x,m). [resolve(700,d,17,b)]. given #361 (A,wt=17): 195 p(g(g(k)),g(m)) | g(k) == b | p(g(k),b) | b == k. [resolve(40,a,43,b)]. given #362 (F,wt=16): 724 k == b | b == k | p(m,g(m)) | -(b == x) | p(k,x). [resolve(723,b,18,b)]. given #363 (F,wt=16): 725 k == b | b == k | p(m,g(m)) | -(k == x) | p(x,b). [resolve(723,b,17,b)]. given #364 (T,wt=17): 206 p(f(m),g(f(k))) | f(m) == b | p(f(m),b) | b == k. [resolve(41,a,81,b)]. given #365 (T,wt=16): 1289 f(m) == b | p(f(m),b) | b == k | -(g(f(k)) == b). [factor(1284,b,e)]. given #366 (A,wt=25): 199 p(m,b) | b == k | g(m) == b | -p(g(m),b) | k == b | k == g(m) | -p(g(m),k). [resolve(172,a,2,f)]. given #367 (F,wt=17): 207 p(g(m),g(g(k))) | g(m) == b | p(g(m),b) | b == k. [resolve(41,a,77,b)]. given #368 (F,wt=16): 1296 g(m) == b | p(g(m),b) | b == k | -(g(g(k)) == b). [factor(1291,b,e)]. given #369 (T,wt=17): 208 p(f(k),g(f(m))) | f(k) == b | p(f(k),b) | b == k. [resolve(41,a,73,b)]. given #370 (T,wt=16): 1302 f(k) == b | p(f(k),b) | b == k | -(g(f(m)) == b). [factor(1297,b,e)]. given #371 (A,wt=24): 200 p(m,b) | b == k | k == b | -p(k,b) | g(m) == b | g(m) == k | -p(g(m),k). [resolve(172,a,2,e)]. given #372 (F,wt=17): 209 p(g(k),g(g(m))) | g(k) == b | p(g(k),b) | b == k. [resolve(41,a,69,b)]. given #373 (F,wt=16): 1309 g(k) == b | p(g(k),b) | b == k | -(g(g(m)) == b). [factor(1304,b,e)]. given #374 (T,wt=17): 216 g(j) == j | g(j) == k | j == b | -(b == x) | p(j,x). [resolve(48,d,18,b)]. given #375 (T,wt=17): 217 g(j) == j | g(j) == k | j == b | -(j == x) | p(x,b). [resolve(48,d,17,b)]. given #376 (A,wt=18): 203 p(m,b) | b == k | g(m) == k | g(m) == m | g(m) == b. [resolve(193,a,3,d)]. given #377 (F,wt=17): 404 b == k | -(x == g(g(g(g(k))))) | x == g(g(g(g(m)))). [resolve(229,b,16,b)]. given #378 (F,wt=17): 405 b == k | -(g(g(g(g(m)))) == x) | g(g(g(g(k)))) == x. [resolve(229,b,16,a)]. given #379 (T,wt=17): 410 b == k | -(x == f(g(g(g(k))))) | x == f(g(g(g(m)))). [resolve(230,b,16,b)]. given #380 (T,wt=17): 411 b == k | -(f(g(g(g(m)))) == x) | f(g(g(g(k)))) == x. [resolve(230,b,16,a)]. given #381 (A,wt=22): 214 p(m,b) | b == k | g(k) == b | -p(g(k),b) | m == g(k) | -p(g(k),m). [resolve(210,a,2,f),unit_del(e,21)]. given #382 (F,wt=17): 419 b == k | -(x == g(f(g(g(k))))) | x == g(f(g(g(m)))). [resolve(235,b,16,b)]. given #383 (F,wt=17): 420 b == k | -(g(f(g(g(m)))) == x) | g(f(g(g(k)))) == x. [resolve(235,b,16,a)]. given #384 (T,wt=17): 425 b == k | -(x == f(f(g(g(k))))) | x == f(f(g(g(m)))). [resolve(236,b,16,b)]. given #385 (T,wt=17): 426 b == k | -(f(f(g(g(m)))) == x) | f(f(g(g(k)))) == x. [resolve(236,b,16,a)]. given #386 (A,wt=23): 218 g(j) == j | g(j) == k | j == b | x == b | x == j | -p(j,x) | -p(x,j). [resolve(48,d,2,b),merge(d)]. given #387 (F,wt=17): 433 b == k | -(x == g(g(f(g(k))))) | x == g(g(f(g(m)))). [resolve(243,b,16,b)]. given #388 (F,wt=17): 434 b == k | -(g(g(f(g(m)))) == x) | g(g(f(g(k)))) == x. [resolve(243,b,16,a)]. given #389 (T,wt=17): 439 b == k | -(x == f(g(f(g(k))))) | x == f(g(f(g(m)))). [resolve(244,b,16,b)]. given #390 (T,wt=17): 440 b == k | -(f(g(f(g(m)))) == x) | f(g(f(g(k)))) == x. [resolve(244,b,16,a)]. given #391 (A,wt=20): 219 g(j) == j | g(j) == k | j == b | p(b,m) | j == m | -p(b,j). [resolve(48,d,1,f),merge(g),unit_del(d,42)]. given #392 (F,wt=17): 448 b == k | -(x == g(f(f(g(k))))) | x == g(f(f(g(m)))). [resolve(249,b,16,b)]. given #393 (F,wt=17): 449 b == k | -(g(f(f(g(m)))) == x) | g(f(f(g(k)))) == x. [resolve(249,b,16,a)]. given #394 (T,wt=17): 454 b == k | -(x == f(f(f(g(k))))) | x == f(f(f(g(m)))). [resolve(250,b,16,b)]. given #395 (T,wt=17): 455 b == k | -(f(f(f(g(m)))) == x) | f(f(f(g(k)))) == x. [resolve(250,b,16,a)]. given #396 (A,wt=23): 220 g(j) == j | g(j) == k | j == b | j == m | p(j,m) | b == j | -p(b,j). [resolve(48,d,1,e),unit_del(f,42)]. given #397 (F,wt=17): 462 b == k | -(x == g(g(g(f(k))))) | x == g(g(g(f(m)))). [resolve(257,b,16,b)]. given #398 (F,wt=17): 463 b == k | -(g(g(g(f(m)))) == x) | g(g(g(f(k)))) == x. [resolve(257,b,16,a)]. given #399 (T,wt=17): 468 b == k | -(x == f(g(g(f(k))))) | x == f(g(g(f(m)))). [resolve(258,b,16,b)]. given #400 (T,wt=17): 469 b == k | -(f(g(g(f(m)))) == x) | f(g(g(f(k)))) == x. [resolve(258,b,16,a)]. given #401 (A,wt=21): 224 b == k | m == j | k == b | -p(k,b) | j == b | j == k | -p(j,k). [resolve(221,c,2,e)]. given #402 (F,wt=17): 476 b == k | -(x == g(f(g(f(k))))) | x == g(f(g(f(m)))). [resolve(263,b,16,b)]. given #403 (F,wt=17): 477 b == k | -(g(f(g(f(m)))) == x) | g(f(g(f(k)))) == x. [resolve(263,b,16,a)]. given #404 (T,wt=17): 482 b == k | -(x == f(f(g(f(k))))) | x == f(f(g(f(m)))). [resolve(264,b,16,b)]. given #405 (T,wt=17): 483 b == k | -(f(f(g(f(m)))) == x) | f(f(g(f(k)))) == x. [resolve(264,b,16,a)]. given #406 (A,wt=21): 225 b == k | p(g(g(k)),g(g(g(m)))) | g(g(k)) == b | p(g(g(k)),b). [resolve(120,b,41,a)]. given #407 (F,wt=17): 490 b == k | -(x == g(g(f(f(k))))) | x == g(g(f(f(m)))). [resolve(271,b,16,b)]. given #408 (F,wt=17): 491 b == k | -(g(g(f(f(m)))) == x) | g(g(f(f(k)))) == x. [resolve(271,b,16,a)]. given #409 (T,wt=17): 496 b == k | -(x == f(g(f(f(k))))) | x == f(g(f(f(m)))). [resolve(272,b,16,b)]. given #410 (T,wt=17): 497 b == k | -(f(g(f(f(m)))) == x) | f(g(f(f(k)))) == x. [resolve(272,b,16,a)]. given #411 (A,wt=25): 226 b == k | p(g(g(g(g(k)))),g(g(g(m)))) | g(g(g(k))) == b | p(g(g(g(k))),b). [resolve(120,b,40,a)]. given #412 (F,wt=17): 505 b == k | -(x == g(f(f(f(k))))) | x == g(f(f(f(m)))). [resolve(277,b,16,b)]. given #413 (F,wt=17): 506 b == k | -(g(f(f(f(m)))) == x) | g(f(f(f(k)))) == x. [resolve(277,b,16,a)]. given #414 (T,wt=17): 511 b == k | -(x == f(f(f(f(k))))) | x == f(f(f(f(m)))). [resolve(278,b,16,b)]. given #415 (T,wt=17): 512 b == k | -(f(f(f(f(m)))) == x) | f(f(f(f(k)))) == x. [resolve(278,b,16,a)]. given #416 (A,wt=25): 227 b == k | p(g(g(g(m))),g(g(g(g(k))))) | g(g(g(k))) == b | p(g(g(g(k))),b). [resolve(120,b,39,a)]. given #417 (F,wt=17): 519 b == k | -(x == g(g(g(g(m))))) | x == g(g(g(g(k)))). [resolve(285,b,16,b)]. given #418 (F,wt=17): 520 b == k | -(g(g(g(g(k)))) == x) | g(g(g(g(m)))) == x. [resolve(285,b,16,a)]. given #419 (T,wt=17): 525 b == k | -(x == f(g(g(g(m))))) | x == f(g(g(g(k)))). [resolve(286,b,16,b)]. given #420 (T,wt=17): 526 b == k | -(f(g(g(g(k)))) == x) | f(g(g(g(m)))) == x. [resolve(286,b,16,a)]. given #421 (A,wt=21): 228 b == k | p(g(g(g(m))),g(g(k))) | g(g(k)) == b | p(g(g(k)),b). [resolve(120,b,38,a)]. given #422 (F,wt=17): 534 b == k | -(x == g(f(g(g(m))))) | x == g(f(g(g(k)))). [resolve(291,b,16,b)]. given #423 (F,wt=17): 535 b == k | -(g(f(g(g(k)))) == x) | g(f(g(g(m)))) == x. [resolve(291,b,16,a)]. given #424 (T,wt=17): 540 b == k | -(x == f(f(g(g(m))))) | x == f(f(g(g(k)))). [resolve(292,b,16,b)]. given #425 (T,wt=17): 541 b == k | -(f(f(g(g(k)))) == x) | f(f(g(g(m)))) == x. [resolve(292,b,16,a)]. given #426 (A,wt=25): 233 b == k | p(g(f(g(g(k)))),f(g(g(m)))) | f(g(g(k))) == b | p(f(g(g(k))),b). [resolve(121,b,40,a)]. given #427 (F,wt=17): 548 b == k | -(x == g(g(f(g(m))))) | x == g(g(f(g(k)))). [resolve(299,b,16,b)]. given #428 (F,wt=17): 549 b == k | -(g(g(f(g(k)))) == x) | g(g(f(g(m)))) == x. [resolve(299,b,16,a)]. given #429 (T,wt=17): 554 b == k | -(x == f(g(f(g(m))))) | x == f(g(f(g(k)))). [resolve(300,b,16,b)]. given #430 (T,wt=17): 555 b == k | -(f(g(f(g(k)))) == x) | f(g(f(g(m)))) == x. [resolve(300,b,16,a)]. given #431 (A,wt=25): 234 b == k | p(f(g(g(m))),g(f(g(g(k))))) | f(g(g(k))) == b | p(f(g(g(k))),b). [resolve(121,b,39,a)]. given #432 (F,wt=17): 562 b == k | -(x == g(f(f(g(m))))) | x == g(f(f(g(k)))). [resolve(305,b,16,b)]. given #433 (F,wt=17): 563 b == k | -(g(f(f(g(k)))) == x) | g(f(f(g(m)))) == x. [resolve(305,b,16,a)]. given #434 (T,wt=17): 568 b == k | -(x == f(f(f(g(m))))) | x == f(f(f(g(k)))). [resolve(306,b,16,b)]. given #435 (T,wt=17): 569 b == k | -(f(f(f(g(k)))) == x) | f(f(f(g(m)))) == x. [resolve(306,b,16,a)]. given #436 (A,wt=21): 239 b == k | p(f(g(k)),g(f(g(m)))) | f(g(k)) == b | p(f(g(k)),b). [resolve(128,b,41,a)]. given #437 (F,wt=17): 576 b == k | -(x == g(g(g(f(m))))) | x == g(g(g(f(k)))). [resolve(313,b,16,b)]. given #438 (F,wt=17): 577 b == k | -(g(g(g(f(k)))) == x) | g(g(g(f(m)))) == x. [resolve(313,b,16,a)]. given #439 (T,wt=17): 582 b == k | -(x == f(g(g(f(m))))) | x == f(g(g(f(k)))). [resolve(314,b,16,b)]. given #440 (T,wt=17): 583 b == k | -(f(g(g(f(k)))) == x) | f(g(g(f(m)))) == x. [resolve(314,b,16,a)]. given #441 (A,wt=25): 240 b == k | p(g(g(f(g(k)))),g(f(g(m)))) | g(f(g(k))) == b | p(g(f(g(k))),b). [resolve(128,b,40,a)]. given #442 (F,wt=17): 590 b == k | -(x == g(f(g(f(m))))) | x == g(f(g(f(k)))). [resolve(319,b,16,b)]. given #443 (F,wt=17): 591 b == k | -(g(f(g(f(k)))) == x) | g(f(g(f(m)))) == x. [resolve(319,b,16,a)]. given #444 (T,wt=17): 596 b == k | -(x == f(f(g(f(m))))) | x == f(f(g(f(k)))). [resolve(320,b,16,b)]. given #445 (T,wt=17): 597 b == k | -(f(f(g(f(k)))) == x) | f(f(g(f(m)))) == x. [resolve(320,b,16,a)]. given #446 (A,wt=25): 241 b == k | p(g(f(g(m))),g(g(f(g(k))))) | g(f(g(k))) == b | p(g(f(g(k))),b). [resolve(128,b,39,a)]. given #447 (F,wt=17): 604 b == k | -(x == g(g(f(f(m))))) | x == g(g(f(f(k)))). [resolve(327,b,16,b)]. given #448 (F,wt=17): 605 b == k | -(g(g(f(f(k)))) == x) | g(g(f(f(m)))) == x. [resolve(327,b,16,a)]. given #449 (T,wt=17): 610 b == k | -(x == f(g(f(f(m))))) | x == f(g(f(f(k)))). [resolve(328,b,16,b)]. given #450 (T,wt=17): 611 b == k | -(f(g(f(f(k)))) == x) | f(g(f(f(m)))) == x. [resolve(328,b,16,a)]. given #451 (A,wt=21): 242 b == k | p(g(f(g(m))),f(g(k))) | f(g(k)) == b | p(f(g(k)),b). [resolve(128,b,38,a)]. given #452 (F,wt=17): 621 b == k | -(x == g(f(f(f(m))))) | x == g(f(f(f(k)))). [resolve(333,b,16,b)]. given #453 (F,wt=17): 622 b == k | -(g(f(f(f(k)))) == x) | g(f(f(f(m)))) == x. [resolve(333,b,16,a)]. given #454 (T,wt=17): 627 b == k | -(x == f(f(f(f(m))))) | x == f(f(f(f(k)))). [resolve(334,b,16,b)]. given #455 (T,wt=17): 628 b == k | -(f(f(f(f(k)))) == x) | f(f(f(f(m)))) == x. [resolve(334,b,16,a)]. given #456 (A,wt=25): 247 b == k | p(g(f(f(g(k)))),f(f(g(m)))) | f(f(g(k))) == b | p(f(f(g(k))),b). [resolve(129,b,40,a)]. given #457 (F,wt=17): 670 b == k | f(b) == m | b == f(b) | p(f(f(b)),f(b)). [resolve(396,c,7,b),merge(d)]. given #458 (F,wt=17): 671 b == k | f(b) == m | b == f(b) | p(f(b),f(f(b))). [resolve(396,c,6,b),merge(d)]. given #459 (T,wt=17): 672 b == k | f(b) == m | b == f(b) | -(f(f(b)) == f(b)). [resolve(396,c,5,b),merge(d)]. given #460 (T,wt=18): 365 p(m,b) | b == k | g(k) == k | g(k) == m | g(k) == b. [resolve(362,c,3,d)]. given #461 (A,wt=25): 248 b == k | p(f(f(g(m))),g(f(f(g(k))))) | f(f(g(k))) == b | p(f(f(g(k))),b). [resolve(129,b,39,a)]. given #462 (F,wt=18): 377 k == b | p(k,b) | b == k | g(k) == m | -(f(g(k)) == m). [resolve(196,a,4,b)]. given #463 (F,wt=18): 668 b == k | f(b) == m | b == f(b) | -(m == x) | p(f(b),x). [resolve(396,c,18,b)]. given #464 (T,wt=15): 1398 b == k | f(b) == m | b == f(b) | p(f(b),k). [resolve(668,d,47,b),merge(e)]. given #465 (T,wt=18): 669 b == k | f(b) == m | b == f(b) | -(f(b) == x) | p(x,m). [resolve(396,c,17,b)]. given #466 (A,wt=21): 253 b == k | p(g(f(k)),g(g(f(m)))) | g(f(k)) == b | p(g(f(k)),b). [resolve(132,b,41,a)]. given #467 (F,wt=18): 706 k == b | p(k,b) | b == k | g(m) == m | -(f(g(m)) == m). [resolve(700,d,4,b)]. given #468 (F,wt=18): 741 b == k | g(g(g(g(g(g(k)))))) == g(g(g(g(g(g(m)))))). [resolve(402,b,20,a)]. given #469 (T,wt=18): 742 b == k | f(g(g(g(g(g(k)))))) == f(g(g(g(g(g(m)))))). [resolve(402,b,19,a)]. given #470 (T,wt=18): 747 b == k | g(f(g(g(g(g(k)))))) == g(f(g(g(g(g(m)))))). [resolve(403,b,20,a)]. given #471 (A,wt=25): 254 b == k | p(g(g(g(f(k)))),g(g(f(m)))) | g(g(f(k))) == b | p(g(g(f(k))),b). [resolve(132,b,40,a)]. given #472 (F,wt=18): 748 b == k | f(f(g(g(g(g(k)))))) == f(f(g(g(g(g(m)))))). [resolve(403,b,19,a)]. given #473 (F,wt=18): 755 b == k | g(g(f(g(g(g(k)))))) == g(g(f(g(g(g(m)))))). [resolve(408,b,20,a)]. given #474 (T,wt=18): 756 b == k | f(g(f(g(g(g(k)))))) == f(g(f(g(g(g(m)))))). [resolve(408,b,19,a)]. given #475 (T,wt=18): 761 b == k | g(f(f(g(g(g(k)))))) == g(f(f(g(g(g(m)))))). [resolve(409,b,20,a)]. given #476 (A,wt=25): 255 b == k | p(g(g(f(m))),g(g(g(f(k))))) | g(g(f(k))) == b | p(g(g(f(k))),b). [resolve(132,b,39,a)]. given #477 (F,wt=18): 762 b == k | f(f(f(g(g(g(k)))))) == f(f(f(g(g(g(m)))))). [resolve(409,b,19,a)]. given #478 (F,wt=18): 780 b == k | g(g(g(f(g(g(k)))))) == g(g(g(f(g(g(m)))))). [resolve(417,b,20,a)]. given #479 (T,wt=18): 781 b == k | f(g(g(f(g(g(k)))))) == f(g(g(f(g(g(m)))))). [resolve(417,b,19,a)]. given #480 (T,wt=18): 786 b == k | g(f(g(f(g(g(k)))))) == g(f(g(f(g(g(m)))))). [resolve(418,b,20,a)]. given #481 (A,wt=21): 256 b == k | p(g(g(f(m))),g(f(k))) | g(f(k)) == b | p(g(f(k)),b). [resolve(132,b,38,a)]. given #482 (F,wt=18): 787 b == k | f(f(g(f(g(g(k)))))) == f(f(g(f(g(g(m)))))). [resolve(418,b,19,a)]. given #483 (F,wt=18): 794 b == k | g(g(f(f(g(g(k)))))) == g(g(f(f(g(g(m)))))). [resolve(423,b,20,a)]. given #484 (T,wt=18): 795 b == k | f(g(f(f(g(g(k)))))) == f(g(f(f(g(g(m)))))). [resolve(423,b,19,a)]. given #485 (T,wt=18): 806 b == k | g(f(f(f(g(g(k)))))) == g(f(f(f(g(g(m)))))). [resolve(424,b,20,a)]. given #486 (A,wt=25): 261 b == k | p(g(f(g(f(k)))),f(g(f(m)))) | f(g(f(k))) == b | p(f(g(f(k))),b). [resolve(133,b,40,a)]. given #487 (F,wt=18): 807 b == k | f(f(f(f(g(g(k)))))) == f(f(f(f(g(g(m)))))). [resolve(424,b,19,a)]. given #488 (F,wt=18): 814 b == k | g(g(g(g(f(g(k)))))) == g(g(g(g(f(g(m)))))). [resolve(431,b,20,a)]. given #489 (T,wt=18): 815 b == k | f(g(g(g(f(g(k)))))) == f(g(g(g(f(g(m)))))). [resolve(431,b,19,a)]. given #490 (T,wt=18): 820 b == k | g(f(g(g(f(g(k)))))) == g(f(g(g(f(g(m)))))). [resolve(432,b,20,a)]. given #491 (A,wt=25): 262 b == k | p(f(g(f(m))),g(f(g(f(k))))) | f(g(f(k))) == b | p(f(g(f(k))),b). [resolve(133,b,39,a)]. given #492 (F,wt=18): 821 b == k | f(f(g(g(f(g(k)))))) == f(f(g(g(f(g(m)))))). [resolve(432,b,19,a)]. given #493 (F,wt=18): 828 b == k | g(g(f(g(f(g(k)))))) == g(g(f(g(f(g(m)))))). [resolve(437,b,20,a)]. given #494 (T,wt=18): 829 b == k | f(g(f(g(f(g(k)))))) == f(g(f(g(f(g(m)))))). [resolve(437,b,19,a)]. given #495 (T,wt=18): 838 b == k | g(f(f(g(f(g(k)))))) == g(f(f(g(f(g(m)))))). [resolve(438,b,20,a)]. given #496 (A,wt=21): 267 b == k | p(f(f(k)),g(f(f(m)))) | f(f(k)) == b | p(f(f(k)),b). [resolve(136,b,41,a)]. given #497 (F,wt=18): 839 b == k | f(f(f(g(f(g(k)))))) == f(f(f(g(f(g(m)))))). [resolve(438,b,19,a)]. given #498 (F,wt=18): 846 b == k | g(g(g(f(f(g(k)))))) == g(g(g(f(f(g(m)))))). [resolve(446,b,20,a)]. given #499 (T,wt=18): 847 b == k | f(g(g(f(f(g(k)))))) == f(g(g(f(f(g(m)))))). [resolve(446,b,19,a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 62 (0.00 of 0.12 sec). given #500 (T,wt=18): 852 b == k | g(f(g(f(f(g(k)))))) == g(f(g(f(f(g(m)))))). [resolve(447,b,20,a)]. given #501 (A,wt=25): 268 b == k | p(g(g(f(f(k)))),g(f(f(m)))) | g(f(f(k))) == b | p(g(f(f(k))),b). [resolve(136,b,40,a)]. given #502 (F,wt=18): 853 b == k | f(f(g(f(f(g(k)))))) == f(f(g(f(f(g(m)))))). [resolve(447,b,19,a)]. given #503 (F,wt=18): 860 b == k | g(g(f(f(f(g(k)))))) == g(g(f(f(f(g(m)))))). [resolve(452,b,20,a)]. given #504 (T,wt=18): 861 b == k | f(g(f(f(f(g(k)))))) == f(g(f(f(f(g(m)))))). [resolve(452,b,19,a)]. given #505 (T,wt=18): 871 b == k | g(f(f(f(f(g(k)))))) == g(f(f(f(f(g(m)))))). [resolve(453,b,20,a)]. given #506 (A,wt=25): 269 b == k | p(g(f(f(m))),g(g(f(f(k))))) | g(f(f(k))) == b | p(g(f(f(k))),b). [resolve(136,b,39,a)]. given #507 (F,wt=18): 872 b == k | f(f(f(f(f(g(k)))))) == f(f(f(f(f(g(m)))))). [resolve(453,b,19,a)]. given #508 (F,wt=18): 879 b == k | g(g(g(g(g(f(k)))))) == g(g(g(g(g(f(m)))))). [resolve(460,b,20,a)]. given #509 (T,wt=18): 880 b == k | f(g(g(g(g(f(k)))))) == f(g(g(g(g(f(m)))))). [resolve(460,b,19,a)]. given #510 (T,wt=18): 885 b == k | g(f(g(g(g(f(k)))))) == g(f(g(g(g(f(m)))))). [resolve(461,b,20,a)]. given #511 (A,wt=21): 270 b == k | p(g(f(f(m))),f(f(k))) | f(f(k)) == b | p(f(f(k)),b). [resolve(136,b,38,a)]. given #512 (F,wt=18): 886 b == k | f(f(g(g(g(f(k)))))) == f(f(g(g(g(f(m)))))). [resolve(461,b,19,a)]. given #513 (F,wt=18): 893 b == k | g(g(f(g(g(f(k)))))) == g(g(f(g(g(f(m)))))). [resolve(466,b,20,a)]. given #514 (T,wt=18): 894 b == k | f(g(f(g(g(f(k)))))) == f(g(f(g(g(f(m)))))). [resolve(466,b,19,a)]. given #515 (T,wt=18): 900 b == k | g(f(f(g(g(f(k)))))) == g(f(f(g(g(f(m)))))). [resolve(467,b,20,a)]. given #516 (A,wt=25): 275 b == k | p(g(f(f(f(k)))),f(f(f(m)))) | f(f(f(k))) == b | p(f(f(f(k))),b). [resolve(137,b,40,a)]. given #517 (F,wt=18): 901 b == k | f(f(f(g(g(f(k)))))) == f(f(f(g(g(f(m)))))). [resolve(467,b,19,a)]. given #518 (F,wt=18): 908 b == k | g(g(g(f(g(f(k)))))) == g(g(g(f(g(f(m)))))). [resolve(474,b,20,a)]. given #519 (T,wt=18): 909 b == k | f(g(g(f(g(f(k)))))) == f(g(g(f(g(f(m)))))). [resolve(474,b,19,a)]. given #520 (T,wt=18): 914 b == k | g(f(g(f(g(f(k)))))) == g(f(g(f(g(f(m)))))). [resolve(475,b,20,a)]. given #521 (A,wt=25): 276 b == k | p(f(f(f(m))),g(f(f(f(k))))) | f(f(f(k))) == b | p(f(f(f(k))),b). [resolve(137,b,39,a)]. given #522 (F,wt=18): 915 b == k | f(f(g(f(g(f(k)))))) == f(f(g(f(g(f(m)))))). [resolve(475,b,19,a)]. given #523 (F,wt=18): 922 b == k | g(g(f(f(g(f(k)))))) == g(g(f(f(g(f(m)))))). [resolve(480,b,20,a)]. given #524 (T,wt=18): 923 b == k | f(g(f(f(g(f(k)))))) == f(g(f(f(g(f(m)))))). [resolve(480,b,19,a)]. given #525 (T,wt=18): 934 b == k | g(f(f(f(g(f(k)))))) == g(f(f(f(g(f(m)))))). [resolve(481,b,20,a)]. given #526 (A,wt=21): 281 b == k | p(g(g(m)),g(g(g(k)))) | g(g(m)) == b | p(g(g(m)),b). [resolve(140,b,41,a)]. given #527 (F,wt=18): 935 b == k | f(f(f(f(g(f(k)))))) == f(f(f(f(g(f(m)))))). [resolve(481,b,19,a)]. given #528 (F,wt=18): 942 b == k | g(g(g(g(f(f(k)))))) == g(g(g(g(f(f(m)))))). [resolve(488,b,20,a)]. given #529 (T,wt=18): 943 b == k | f(g(g(g(f(f(k)))))) == f(g(g(g(f(f(m)))))). [resolve(488,b,19,a)]. given #530 (T,wt=18): 948 b == k | g(f(g(g(f(f(k)))))) == g(f(g(g(f(f(m)))))). [resolve(489,b,20,a)]. given #531 (A,wt=25): 282 b == k | p(g(g(g(g(m)))),g(g(g(k)))) | g(g(g(m))) == b | p(g(g(g(m))),b). [resolve(140,b,40,a)]. given #532 (F,wt=18): 949 b == k | f(f(g(g(f(f(k)))))) == f(f(g(g(f(f(m)))))). [resolve(489,b,19,a)]. given #533 (F,wt=18): 956 b == k | g(g(f(g(f(f(k)))))) == g(g(f(g(f(f(m)))))). [resolve(494,b,20,a)]. given #534 (T,wt=18): 957 b == k | f(g(f(g(f(f(k)))))) == f(g(f(g(f(f(m)))))). [resolve(494,b,19,a)]. given #535 (T,wt=18): 968 b == k | g(f(f(g(f(f(k)))))) == g(f(f(g(f(f(m)))))). [resolve(495,b,20,a)]. given #536 (A,wt=25): 283 b == k | p(g(g(g(k))),g(g(g(g(m))))) | g(g(g(m))) == b | p(g(g(g(m))),b). [resolve(140,b,39,a)]. given #537 (F,wt=18): 969 b == k | f(f(f(g(f(f(k)))))) == f(f(f(g(f(f(m)))))). [resolve(495,b,19,a)]. given #538 (F,wt=18): 976 b == k | g(g(g(f(f(f(k)))))) == g(g(g(f(f(f(m)))))). [resolve(503,b,20,a)]. given #539 (T,wt=18): 977 b == k | f(g(g(f(f(f(k)))))) == f(g(g(f(f(f(m)))))). [resolve(503,b,19,a)]. given #540 (T,wt=18): 982 b == k | g(f(g(f(f(f(k)))))) == g(f(g(f(f(f(m)))))). [resolve(504,b,20,a)]. given #541 (A,wt=21): 284 b == k | p(g(g(g(k))),g(g(m))) | g(g(m)) == b | p(g(g(m)),b). [resolve(140,b,38,a)]. given #542 (F,wt=18): 983 b == k | f(f(g(f(f(f(k)))))) == f(f(g(f(f(f(m)))))). [resolve(504,b,19,a)]. given #543 (F,wt=18): 990 b == k | g(g(f(f(f(f(k)))))) == g(g(f(f(f(f(m)))))). [resolve(509,b,20,a)]. given #544 (T,wt=18): 991 b == k | f(g(f(f(f(f(k)))))) == f(g(f(f(f(f(m)))))). [resolve(509,b,19,a)]. given #545 (T,wt=18): 1002 b == k | g(f(f(f(f(f(k)))))) == g(f(f(f(f(f(m)))))). [resolve(510,b,20,a)]. given #546 (A,wt=25): 289 b == k | p(g(f(g(g(m)))),f(g(g(k)))) | f(g(g(m))) == b | p(f(g(g(m))),b). [resolve(141,b,40,a)]. given #547 (F,wt=18): 1003 b == k | f(f(f(f(f(f(k)))))) == f(f(f(f(f(f(m)))))). [resolve(510,b,19,a)]. given #548 (F,wt=18): 1010 b == k | g(g(g(g(g(g(m)))))) == g(g(g(g(g(g(k)))))). [resolve(517,b,20,a)]. given #549 (T,wt=18): 1011 b == k | f(g(g(g(g(g(m)))))) == f(g(g(g(g(g(k)))))). [resolve(517,b,19,a)]. given #550 (T,wt=18): 1016 b == k | g(f(g(g(g(g(m)))))) == g(f(g(g(g(g(k)))))). [resolve(518,b,20,a)]. given #551 (A,wt=25): 290 b == k | p(f(g(g(k))),g(f(g(g(m))))) | f(g(g(m))) == b | p(f(g(g(m))),b). [resolve(141,b,39,a)]. given #552 (F,wt=18): 1017 b == k | f(f(g(g(g(g(m)))))) == f(f(g(g(g(g(k)))))). [resolve(518,b,19,a)]. given #553 (F,wt=18): 1024 b == k | g(g(f(g(g(g(m)))))) == g(g(f(g(g(g(k)))))). [resolve(523,b,20,a)]. given #554 (T,wt=18): 1025 b == k | f(g(f(g(g(g(m)))))) == f(g(f(g(g(g(k)))))). [resolve(523,b,19,a)]. given #555 (T,wt=18): 1036 b == k | g(f(f(g(g(g(m)))))) == g(f(f(g(g(g(k)))))). [resolve(524,b,20,a)]. given #556 (A,wt=21): 295 b == k | p(f(g(m)),g(f(g(k)))) | f(g(m)) == b | p(f(g(m)),b). [resolve(149,b,41,a)]. given #557 (F,wt=18): 1037 b == k | f(f(f(g(g(g(m)))))) == f(f(f(g(g(g(k)))))). [resolve(524,b,19,a)]. given #558 (F,wt=18): 1044 b == k | g(g(g(f(g(g(m)))))) == g(g(g(f(g(g(k)))))). [resolve(532,b,20,a)]. given #559 (T,wt=18): 1045 b == k | f(g(g(f(g(g(m)))))) == f(g(g(f(g(g(k)))))). [resolve(532,b,19,a)]. given #560 (T,wt=18): 1050 b == k | g(f(g(f(g(g(m)))))) == g(f(g(f(g(g(k)))))). [resolve(533,b,20,a)]. given #561 (A,wt=25): 296 b == k | p(g(g(f(g(m)))),g(f(g(k)))) | g(f(g(m))) == b | p(g(f(g(m))),b). [resolve(149,b,40,a)]. given #562 (F,wt=18): 1051 b == k | f(f(g(f(g(g(m)))))) == f(f(g(f(g(g(k)))))). [resolve(533,b,19,a)]. given #563 (F,wt=18): 1058 b == k | g(g(f(f(g(g(m)))))) == g(g(f(f(g(g(k)))))). [resolve(538,b,20,a)]. given #564 (T,wt=18): 1059 b == k | f(g(f(f(g(g(m)))))) == f(g(f(f(g(g(k)))))). [resolve(538,b,19,a)]. given #565 (T,wt=18): 1070 b == k | g(f(f(f(g(g(m)))))) == g(f(f(f(g(g(k)))))). [resolve(539,b,20,a)]. given #566 (A,wt=25): 297 b == k | p(g(f(g(k))),g(g(f(g(m))))) | g(f(g(m))) == b | p(g(f(g(m))),b). [resolve(149,b,39,a)]. given #567 (F,wt=18): 1071 b == k | f(f(f(f(g(g(m)))))) == f(f(f(f(g(g(k)))))). [resolve(539,b,19,a)]. given #568 (F,wt=18): 1078 b == k | g(g(g(g(f(g(m)))))) == g(g(g(g(f(g(k)))))). [resolve(546,b,20,a)]. given #569 (T,wt=18): 1079 b == k | f(g(g(g(f(g(m)))))) == f(g(g(g(f(g(k)))))). [resolve(546,b,19,a)]. given #570 (T,wt=18): 1084 b == k | g(f(g(g(f(g(m)))))) == g(f(g(g(f(g(k)))))). [resolve(547,b,20,a)]. given #571 (A,wt=21): 298 b == k | p(g(f(g(k))),f(g(m))) | f(g(m)) == b | p(f(g(m)),b). [resolve(149,b,38,a)]. given #572 (F,wt=18): 1085 b == k | f(f(g(g(f(g(m)))))) == f(f(g(g(f(g(k)))))). [resolve(547,b,19,a)]. given #573 (F,wt=18): 1092 b == k | g(g(f(g(f(g(m)))))) == g(g(f(g(f(g(k)))))). [resolve(552,b,20,a)]. given #574 (T,wt=18): 1093 b == k | f(g(f(g(f(g(m)))))) == f(g(f(g(f(g(k)))))). [resolve(552,b,19,a)]. given #575 (T,wt=18): 1104 b == k | g(f(f(g(f(g(m)))))) == g(f(f(g(f(g(k)))))). [resolve(553,b,20,a)]. given #576 (A,wt=25): 303 b == k | p(g(f(f(g(m)))),f(f(g(k)))) | f(f(g(m))) == b | p(f(f(g(m))),b). [resolve(150,b,40,a)]. given #577 (F,wt=18): 1105 b == k | f(f(f(g(f(g(m)))))) == f(f(f(g(f(g(k)))))). [resolve(553,b,19,a)]. given #578 (F,wt=18): 1112 b == k | g(g(g(f(f(g(m)))))) == g(g(g(f(f(g(k)))))). [resolve(560,b,20,a)]. given #579 (T,wt=18): 1113 b == k | f(g(g(f(f(g(m)))))) == f(g(g(f(f(g(k)))))). [resolve(560,b,19,a)]. given #580 (T,wt=18): 1118 b == k | g(f(g(f(f(g(m)))))) == g(f(g(f(f(g(k)))))). [resolve(561,b,20,a)]. given #581 (A,wt=25): 304 b == k | p(f(f(g(k))),g(f(f(g(m))))) | f(f(g(m))) == b | p(f(f(g(m))),b). [resolve(150,b,39,a)]. given #582 (F,wt=18): 1119 b == k | f(f(g(f(f(g(m)))))) == f(f(g(f(f(g(k)))))). [resolve(561,b,19,a)]. given #583 (F,wt=18): 1126 b == k | g(g(f(f(f(g(m)))))) == g(g(f(f(f(g(k)))))). [resolve(566,b,20,a)]. given #584 (T,wt=18): 1127 b == k | f(g(f(f(f(g(m)))))) == f(g(f(f(f(g(k)))))). [resolve(566,b,19,a)]. given #585 (T,wt=18): 1138 b == k | g(f(f(f(f(g(m)))))) == g(f(f(f(f(g(k)))))). [resolve(567,b,20,a)]. given #586 (A,wt=21): 309 b == k | p(g(f(m)),g(g(f(k)))) | g(f(m)) == b | p(g(f(m)),b). [resolve(154,b,41,a)]. given #587 (F,wt=18): 1139 b == k | f(f(f(f(f(g(m)))))) == f(f(f(f(f(g(k)))))). [resolve(567,b,19,a)]. given #588 (F,wt=18): 1146 b == k | g(g(g(g(g(f(m)))))) == g(g(g(g(g(f(k)))))). [resolve(574,b,20,a)]. given #589 (T,wt=18): 1147 b == k | f(g(g(g(g(f(m)))))) == f(g(g(g(g(f(k)))))). [resolve(574,b,19,a)]. given #590 (T,wt=18): 1152 b == k | g(f(g(g(g(f(m)))))) == g(f(g(g(g(f(k)))))). [resolve(575,b,20,a)]. given #591 (A,wt=25): 310 b == k | p(g(g(g(f(m)))),g(g(f(k)))) | g(g(f(m))) == b | p(g(g(f(m))),b). [resolve(154,b,40,a)]. given #592 (F,wt=18): 1153 b == k | f(f(g(g(g(f(m)))))) == f(f(g(g(g(f(k)))))). [resolve(575,b,19,a)]. given #593 (F,wt=18): 1160 b == k | g(g(f(g(g(f(m)))))) == g(g(f(g(g(f(k)))))). [resolve(580,b,20,a)]. given #594 (T,wt=18): 1161 b == k | f(g(f(g(g(f(m)))))) == f(g(f(g(g(f(k)))))). [resolve(580,b,19,a)]. given #595 (T,wt=18): 1172 b == k | g(f(f(g(g(f(m)))))) == g(f(f(g(g(f(k)))))). [resolve(581,b,20,a)]. given #596 (A,wt=25): 311 b == k | p(g(g(f(k))),g(g(g(f(m))))) | g(g(f(m))) == b | p(g(g(f(m))),b). [resolve(154,b,39,a)]. given #597 (F,wt=18): 1173 b == k | f(f(f(g(g(f(m)))))) == f(f(f(g(g(f(k)))))). [resolve(581,b,19,a)]. given #598 (F,wt=18): 1180 b == k | g(g(g(f(g(f(m)))))) == g(g(g(f(g(f(k)))))). [resolve(588,b,20,a)]. given #599 (T,wt=18): 1181 b == k | f(g(g(f(g(f(m)))))) == f(g(g(f(g(f(k)))))). [resolve(588,b,19,a)]. given #600 (T,wt=18): 1186 b == k | g(f(g(f(g(f(m)))))) == g(f(g(f(g(f(k)))))). [resolve(589,b,20,a)]. given #601 (A,wt=21): 312 b == k | p(g(g(f(k))),g(f(m))) | g(f(m)) == b | p(g(f(m)),b). [resolve(154,b,38,a)]. given #602 (F,wt=18): 1187 b == k | f(f(g(f(g(f(m)))))) == f(f(g(f(g(f(k)))))). [resolve(589,b,19,a)]. given #603 (F,wt=18): 1194 b == k | g(g(f(f(g(f(m)))))) == g(g(f(f(g(f(k)))))). [resolve(594,b,20,a)]. given #604 (T,wt=18): 1195 b == k | f(g(f(f(g(f(m)))))) == f(g(f(f(g(f(k)))))). [resolve(594,b,19,a)]. given #605 (T,wt=18): 1206 b == k | g(f(f(f(g(f(m)))))) == g(f(f(f(g(f(k)))))). [resolve(595,b,20,a)]. given #606 (A,wt=25): 317 b == k | p(g(f(g(f(m)))),f(g(f(k)))) | f(g(f(m))) == b | p(f(g(f(m))),b). [resolve(155,b,40,a)]. given #607 (F,wt=18): 1207 b == k | f(f(f(f(g(f(m)))))) == f(f(f(f(g(f(k)))))). [resolve(595,b,19,a)]. given #608 (F,wt=18): 1214 b == k | g(g(g(g(f(f(m)))))) == g(g(g(g(f(f(k)))))). [resolve(602,b,20,a)]. given #609 (T,wt=18): 1215 b == k | f(g(g(g(f(f(m)))))) == f(g(g(g(f(f(k)))))). [resolve(602,b,19,a)]. given #610 (T,wt=18): 1220 b == k | g(f(g(g(f(f(m)))))) == g(f(g(g(f(f(k)))))). [resolve(603,b,20,a)]. given #611 (A,wt=25): 318 b == k | p(f(g(f(k))),g(f(g(f(m))))) | f(g(f(m))) == b | p(f(g(f(m))),b). [resolve(155,b,39,a)]. given #612 (F,wt=18): 1221 b == k | f(f(g(g(f(f(m)))))) == f(f(g(g(f(f(k)))))). [resolve(603,b,19,a)]. given #613 (F,wt=18): 1228 b == k | g(g(f(g(f(f(m)))))) == g(g(f(g(f(f(k)))))). [resolve(608,b,20,a)]. given #614 (T,wt=18): 1229 b == k | f(g(f(g(f(f(m)))))) == f(g(f(g(f(f(k)))))). [resolve(608,b,19,a)]. given #615 (T,wt=18): 1240 b == k | g(f(f(g(f(f(m)))))) == g(f(f(g(f(f(k)))))). [resolve(609,b,20,a)]. given #616 (A,wt=21): 323 b == k | p(f(f(m)),g(f(f(k)))) | f(f(m)) == b | p(f(f(m)),b). [resolve(158,b,41,a)]. given #617 (F,wt=18): 1241 b == k | f(f(f(g(f(f(m)))))) == f(f(f(g(f(f(k)))))). [resolve(609,b,19,a)]. given #618 (F,wt=18): 1248 b == k | g(g(g(f(f(f(m)))))) == g(g(g(f(f(f(k)))))). [resolve(619,b,20,a)]. given #619 (T,wt=18): 1249 b == k | f(g(g(f(f(f(m)))))) == f(g(g(f(f(f(k)))))). [resolve(619,b,19,a)]. given #620 (T,wt=18): 1254 b == k | g(f(g(f(f(f(m)))))) == g(f(g(f(f(f(k)))))). [resolve(620,b,20,a)]. given #621 (A,wt=25): 324 b == k | p(g(g(f(f(m)))),g(f(f(k)))) | g(f(f(m))) == b | p(g(f(f(m))),b). [resolve(158,b,40,a)]. given #622 (F,wt=18): 1255 b == k | f(f(g(f(f(f(m)))))) == f(f(g(f(f(f(k)))))). [resolve(620,b,19,a)]. given #623 (F,wt=18): 1262 b == k | g(g(f(f(f(f(m)))))) == g(g(f(f(f(f(k)))))). [resolve(625,b,20,a)]. given #624 (T,wt=18): 1263 b == k | f(g(f(f(f(f(m)))))) == f(g(f(f(f(f(k)))))). [resolve(625,b,19,a)]. given #625 (T,wt=18): 1274 b == k | g(f(f(f(f(f(m)))))) == g(f(f(f(f(f(k)))))). [resolve(626,b,20,a)]. given #626 (A,wt=25): 325 b == k | p(g(f(f(k))),g(g(f(f(m))))) | g(f(f(m))) == b | p(g(f(f(m))),b). [resolve(158,b,39,a)]. given #627 (F,wt=18): 1275 b == k | f(f(f(f(f(f(m)))))) == f(f(f(f(f(f(k)))))). [resolve(626,b,19,a)]. given #628 (F,wt=18): 1315 p(m,b) | b == k | g(k) == b | -p(g(k),b) | m == g(k). [resolve(214,f,147,a),merge(f),merge(g)]. given #629 (T,wt=18): 1401 b == k | f(b) == m | b == f(b) | -(k == x) | p(f(b),x). [resolve(1398,d,18,b)]. given #630 (T,wt=18): 1402 b == k | f(b) == m | b == f(b) | -(f(b) == x) | p(x,k). [resolve(1398,d,17,b)]. given #631 (A,wt=21): 326 b == k | p(g(f(f(k))),f(f(m))) | f(f(m)) == b | p(f(f(m)),b). [resolve(158,b,38,a)]. given #632 (F,wt=19): 374 k == b | p(k,b) | b == k | g(k) == m | p(f(g(k)),g(k)). [resolve(196,a,7,b)]. given #633 (F,wt=19): 375 k == b | p(k,b) | b == k | g(k) == m | p(g(k),f(g(k))). [resolve(196,a,6,b)]. given #634 (T,wt=19): 376 k == b | p(k,b) | b == k | g(k) == m | -(f(g(k)) == g(k)). [resolve(196,a,5,b)]. given #635 (T,wt=19): 681 p(m,b) | b == k | g(k) == m | -(g(k) == x) | p(f(g(k)),x). [resolve(178,d,18,b)]. given #636 (A,wt=25): 331 b == k | p(g(f(f(f(m)))),f(f(f(k)))) | f(f(f(m))) == b | p(f(f(f(m))),b). [resolve(159,b,40,a)]. given #637 (F,wt=16): 2503 p(m,b) | b == k | g(k) == m | p(f(g(k)),g(m)). [resolve(681,d,43,b),merge(e)]. given #638 (F,wt=19): 682 p(m,b) | b == k | g(k) == m | -(f(g(k)) == x) | p(x,g(k)). [resolve(178,d,17,b)]. given #639 (T,wt=16): 2514 p(m,b) | b == k | g(k) == m | p(f(g(m)),g(k)). [resolve(682,d,70,b),merge(e)]. given #640 (T,wt=19): 686 p(m,b) | b == k | g(k) == m | -(f(g(k)) == x) | p(g(k),x). [resolve(179,d,18,b)]. given #641 (A,wt=25): 332 b == k | p(f(f(f(k))),g(f(f(f(m))))) | f(f(f(m))) == b | p(f(f(f(m))),b). [resolve(159,b,39,a)]. given #642 (F,wt=16): 2520 p(m,b) | b == k | g(k) == m | p(g(k),f(g(m))). [resolve(686,d,70,b),merge(e)]. given #643 (F,wt=19): 687 p(m,b) | b == k | g(k) == m | -(g(k) == x) | p(x,f(g(k))). [resolve(179,d,17,b)]. given #644 (T,wt=16): 2532 p(m,b) | b == k | g(k) == m | p(g(m),f(g(k))). [resolve(687,d,43,b),merge(e)]. given #645 (T,wt=19): 691 p(m,b) | g(m) == m | b == k | -(g(k) == x) | p(f(g(m)),x). [resolve(352,c,18,b)]. given #646 (A,wt=24): 337 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(m == y) | p(g(x),y). [resolve(68,d,18,b)]. given #647 (F,wt=19): 692 p(m,b) | g(m) == m | b == k | -(f(g(m)) == x) | p(x,g(k)). [resolve(352,c,17,b)]. given #648 (F,wt=16): 2538 p(m,b) | g(m) == m | b == k | p(f(g(k)),g(k)). [resolve(692,d,78,b),merge(e)]. given #649 (T,wt=19): 703 k == b | p(k,b) | b == k | g(m) == m | p(f(g(m)),g(m)). [resolve(700,d,7,b)]. given #650 (T,wt=19): 704 k == b | p(k,b) | b == k | g(m) == m | p(g(m),f(g(m))). [resolve(700,d,6,b)]. given #651 (A,wt=24): 338 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(g(x) == y) | p(y,m). [resolve(68,d,17,b)]. given #652 (F,wt=19): 705 k == b | p(k,b) | b == k | g(m) == m | -(f(g(m)) == g(m)). [resolve(700,d,5,b)]. given #653 (F,wt=19): 709 p(m,b) | g(m) == m | b == k | -(g(m) == x) | p(f(g(k)),x). [resolve(357,c,18,b)]. given #654 (T,wt=19): 710 p(m,b) | g(m) == m | b == k | -(f(g(k)) == x) | p(x,g(m)). [resolve(357,c,17,b)]. given #655 (T,wt=19): 727 p(m,b) | g(m) == m | b == k | -(f(g(k)) == x) | p(g(m),x). [resolve(397,c,18,b)]. given #656 (A,wt=23): 339 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | p(f(g(x)),g(x)). [resolve(68,d,7,b),merge(f)]. given #657 (F,wt=19): 728 p(m,b) | g(m) == m | b == k | -(g(m) == x) | p(x,f(g(k))). [resolve(397,c,17,b)]. given #658 (F,wt=16): 2681 p(m,b) | g(m) == m | b == k | p(g(k),f(g(k))). [resolve(728,d,58,b),merge(e)]. given #659 (T,wt=19): 743 b == k | -(x == g(g(g(g(g(k)))))) | x == g(g(g(g(g(m))))). [resolve(402,b,16,b)]. given #660 (T,wt=19): 744 b == k | -(g(g(g(g(g(m))))) == x) | g(g(g(g(g(k))))) == x. [resolve(402,b,16,a)]. given #661 (A,wt=23): 340 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | p(g(x),f(g(x))). [resolve(68,d,6,b),merge(f)]. given #662 (F,wt=19): 749 b == k | -(x == f(g(g(g(g(k)))))) | x == f(g(g(g(g(m))))). [resolve(403,b,16,b)]. given #663 (F,wt=19): 750 b == k | -(f(g(g(g(g(m))))) == x) | f(g(g(g(g(k))))) == x. [resolve(403,b,16,a)]. given #664 (T,wt=19): 757 b == k | -(x == g(f(g(g(g(k)))))) | x == g(f(g(g(g(m))))). [resolve(408,b,16,b)]. given #665 (T,wt=19): 758 b == k | -(g(f(g(g(g(m))))) == x) | g(f(g(g(g(k))))) == x. [resolve(408,b,16,a)]. given #666 (A,wt=23): 341 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == g(x)). [resolve(68,d,5,b),merge(f)]. given #667 (F,wt=19): 763 b == k | -(x == f(f(g(g(g(k)))))) | x == f(f(g(g(g(m))))). [resolve(409,b,16,b)]. given #668 (F,wt=19): 764 b == k | -(f(f(g(g(g(m))))) == x) | f(f(g(g(g(k))))) == x. [resolve(409,b,16,a)]. given #669 (T,wt=19): 771 p(m,b) | g(m) == m | b == k | -(f(g(m)) == x) | p(g(k),x). [resolve(412,c,18,b)]. given #670 (T,wt=19): 772 p(m,b) | g(m) == m | b == k | -(g(k) == x) | p(x,f(g(m))). [resolve(412,c,17,b)]. given #671 (A,wt=22): 342 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == m). [resolve(68,d,4,b),merge(f)]. given #672 (F,wt=19): 782 b == k | -(x == g(g(f(g(g(k)))))) | x == g(g(f(g(g(m))))). [resolve(417,b,16,b)]. given #673 (F,wt=19): 783 b == k | -(g(g(f(g(g(m))))) == x) | g(g(f(g(g(k))))) == x. [resolve(417,b,16,a)]. given #674 (T,wt=19): 788 b == k | -(x == f(g(f(g(g(k)))))) | x == f(g(f(g(g(m))))). [resolve(418,b,16,b)]. given #675 (T,wt=19): 789 b == k | -(f(g(f(g(g(m))))) == x) | f(g(f(g(g(k))))) == x. [resolve(418,b,16,a)]. given #676 (A,wt=28): 343 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -p(m,b) | g(x) == b | -p(m,g(x)). [resolve(68,d,2,f),merge(i),unit_del(f,21)]. given #677 (F,wt=19): 796 b == k | -(x == g(f(f(g(g(k)))))) | x == g(f(f(g(g(m))))). [resolve(423,b,16,b)]. given #678 (F,wt=19): 797 b == k | -(g(f(f(g(g(m))))) == x) | g(f(f(g(g(k))))) == x. [resolve(423,b,16,a)]. given #679 (T,wt=19): 808 b == k | -(x == f(f(f(g(g(k)))))) | x == f(f(f(g(g(m))))). [resolve(424,b,16,b)]. given #680 (T,wt=19): 809 b == k | -(f(f(f(g(g(m))))) == x) | f(f(f(g(g(k))))) == x. [resolve(424,b,16,a)]. given #681 (A,wt=23): 344 k == b | p(k,b) | k == m | g(k) == m | g(k) == k | m == k | -p(m,b). [resolve(85,d,56,e),merge(h),merge(i)]. given #682 (F,wt=19): 816 b == k | -(x == g(g(g(f(g(k)))))) | x == g(g(g(f(g(m))))). [resolve(431,b,16,b)]. given #683 (F,wt=19): 817 b == k | -(g(g(g(f(g(m))))) == x) | g(g(g(f(g(k))))) == x. [resolve(431,b,16,a)]. given #684 (T,wt=19): 822 b == k | -(x == f(g(g(f(g(k)))))) | x == f(g(g(f(g(m))))). [resolve(432,b,16,b)]. given #685 (T,wt=19): 823 b == k | -(f(g(g(f(g(m))))) == x) | f(g(g(f(g(k))))) == x. [resolve(432,b,16,a)]. given #686 (A,wt=23): 345 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(m == y) | p(x,y). [resolve(85,d,18,b)]. given #687 (F,wt=19): 830 b == k | -(x == g(f(g(f(g(k)))))) | x == g(f(g(f(g(m))))). [resolve(437,b,16,b)]. given #688 (F,wt=19): 831 b == k | -(g(f(g(f(g(m))))) == x) | g(f(g(f(g(k))))) == x. [resolve(437,b,16,a)]. given #689 (T,wt=19): 840 b == k | -(x == f(f(g(f(g(k)))))) | x == f(f(g(f(g(m))))). [resolve(438,b,16,b)]. given #690 (T,wt=19): 841 b == k | -(f(f(g(f(g(m))))) == x) | f(f(g(f(g(k))))) == x. [resolve(438,b,16,a)]. given #691 (A,wt=23): 346 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(x == y) | p(y,m). [resolve(85,d,17,b)]. given #692 (F,wt=19): 848 b == k | -(x == g(g(f(f(g(k)))))) | x == g(g(f(f(g(m))))). [resolve(446,b,16,b)]. given #693 (F,wt=19): 849 b == k | -(g(g(f(f(g(m))))) == x) | g(g(f(f(g(k))))) == x. [resolve(446,b,16,a)]. given #694 (T,wt=19): 854 b == k | -(x == f(g(f(f(g(k)))))) | x == f(g(f(f(g(m))))). [resolve(447,b,16,b)]. given #695 (T,wt=19): 855 b == k | -(f(g(f(f(g(m))))) == x) | f(g(f(f(g(k))))) == x. [resolve(447,b,16,a)]. given #696 (A,wt=21): 347 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | p(f(x),x). [resolve(85,d,7,b),merge(f)]. given #697 (F,wt=19): 862 b == k | -(x == g(f(f(f(g(k)))))) | x == g(f(f(f(g(m))))). [resolve(452,b,16,b)]. given #698 (F,wt=19): 863 b == k | -(g(f(f(f(g(m))))) == x) | g(f(f(f(g(k))))) == x. [resolve(452,b,16,a)]. given #699 (T,wt=19): 873 b == k | -(x == f(f(f(f(g(k)))))) | x == f(f(f(f(g(m))))). [resolve(453,b,16,b)]. given #700 (T,wt=19): 874 b == k | -(f(f(f(f(g(m))))) == x) | f(f(f(f(g(k))))) == x. [resolve(453,b,16,a)]. given #701 (A,wt=21): 348 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | p(x,f(x)). [resolve(85,d,6,b),merge(f)]. given #702 (F,wt=19): 881 b == k | -(x == g(g(g(g(f(k)))))) | x == g(g(g(g(f(m))))). [resolve(460,b,16,b)]. given #703 (F,wt=19): 882 b == k | -(g(g(g(g(f(m))))) == x) | g(g(g(g(f(k))))) == x. [resolve(460,b,16,a)]. given #704 (T,wt=19): 887 b == k | -(x == f(g(g(g(f(k)))))) | x == f(g(g(g(f(m))))). [resolve(461,b,16,b)]. given #705 (T,wt=19): 888 b == k | -(f(g(g(g(f(m))))) == x) | f(g(g(g(f(k))))) == x. [resolve(461,b,16,a)]. given #706 (A,wt=21): 349 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == x). [resolve(85,d,5,b),merge(f)]. given #707 (F,wt=19): 895 b == k | -(x == g(f(g(g(f(k)))))) | x == g(f(g(g(f(m))))). [resolve(466,b,16,b)]. given #708 (F,wt=19): 896 b == k | -(g(f(g(g(f(m))))) == x) | g(f(g(g(f(k))))) == x. [resolve(466,b,16,a)]. given #709 (T,wt=19): 902 b == k | -(x == f(f(g(g(f(k)))))) | x == f(f(g(g(f(m))))). [resolve(467,b,16,b)]. given #710 (T,wt=19): 903 b == k | -(f(f(g(g(f(m))))) == x) | f(f(g(g(f(k))))) == x. [resolve(467,b,16,a)]. given #711 (A,wt=21): 350 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == m). [resolve(85,d,4,b),merge(f)]. given #712 (F,wt=19): 910 b == k | -(x == g(g(f(g(f(k)))))) | x == g(g(f(g(f(m))))). [resolve(474,b,16,b)]. given #713 (F,wt=19): 911 b == k | -(g(g(f(g(f(m))))) == x) | g(g(f(g(f(k))))) == x. [resolve(474,b,16,a)]. given #714 (T,wt=19): 916 b == k | -(x == f(g(f(g(f(k)))))) | x == f(g(f(g(f(m))))). [resolve(475,b,16,b)]. given #715 (T,wt=19): 917 b == k | -(f(g(f(g(f(m))))) == x) | f(g(f(g(f(k))))) == x. [resolve(475,b,16,a)]. given #716 (A,wt=23): 351 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -p(m,b) | -p(m,x). [resolve(85,d,2,f),merge(h),merge(i),unit_del(f,21)]. given #717 (F,wt=19): 924 b == k | -(x == g(f(f(g(f(k)))))) | x == g(f(f(g(f(m))))). [resolve(480,b,16,b)]. given #718 (F,wt=19): 925 b == k | -(g(f(f(g(f(m))))) == x) | g(f(f(g(f(k))))) == x. [resolve(480,b,16,a)]. given #719 (T,wt=19): 936 b == k | -(x == f(f(f(g(f(k)))))) | x == f(f(f(g(f(m))))). [resolve(481,b,16,b)]. given #720 (T,wt=19): 937 b == k | -(f(f(f(g(f(m))))) == x) | f(f(f(g(f(k))))) == x. [resolve(481,b,16,a)]. given #721 (A,wt=21): 355 k == b | p(k,b) | b == k | g(m) == k | g(m) == m | g(m) == b. [resolve(148,a,3,d)]. given #722 (F,wt=19): 944 b == k | -(x == g(g(g(f(f(k)))))) | x == g(g(g(f(f(m))))). [resolve(488,b,16,b)]. given #723 (F,wt=19): 945 b == k | -(g(g(g(f(f(m))))) == x) | g(g(g(f(f(k))))) == x. [resolve(488,b,16,a)]. given #724 (T,wt=19): 950 b == k | -(x == f(g(g(f(f(k)))))) | x == f(g(g(f(f(m))))). [resolve(489,b,16,b)]. given #725 (T,wt=19): 951 b == k | -(f(g(g(f(f(m))))) == x) | f(g(g(f(f(k))))) == x. [resolve(489,b,16,a)]. given #726 (A,wt=25): 356 k == b | p(k,b) | b == k | g(m) == b | -p(g(m),b) | k == g(m) | -p(k,g(m)). [resolve(148,a,2,e),merge(f)]. given #727 (F,wt=19): 958 b == k | -(x == g(f(g(f(f(k)))))) | x == g(f(g(f(f(m))))). [resolve(494,b,16,b)]. given #728 (F,wt=19): 959 b == k | -(g(f(g(f(f(m))))) == x) | g(f(g(f(f(k))))) == x. [resolve(494,b,16,a)]. given #729 (T,wt=19): 970 b == k | -(x == f(f(g(f(f(k)))))) | x == f(f(g(f(f(m))))). [resolve(495,b,16,b)]. given #730 (T,wt=19): 971 b == k | -(f(f(g(f(f(m))))) == x) | f(f(g(f(f(k))))) == x. [resolve(495,b,16,a)]. given #731 (A,wt=26): 358 p(m,b) | g(m) == m | g(m) == b | -p(g(m),b) | f(g(m)) == b | f(g(m)) == g(m). [resolve(95,g,29,c),merge(g),merge(h)]. given #732 (F,wt=19): 978 b == k | -(x == g(g(f(f(f(k)))))) | x == g(g(f(f(f(m))))). [resolve(503,b,16,b)]. given #733 (F,wt=19): 979 b == k | -(g(g(f(f(f(m))))) == x) | g(g(f(f(f(k))))) == x. [resolve(503,b,16,a)]. given #734 (T,wt=19): 984 b == k | -(x == f(g(f(f(f(k)))))) | x == f(g(f(f(f(m))))). [resolve(504,b,16,b)]. given #735 (T,wt=19): 985 b == k | -(f(g(f(f(f(m))))) == x) | f(g(f(f(f(k))))) == x. [resolve(504,b,16,a)]. given #736 (A,wt=22): 361 p(m,g(k)) | k == b | b == k | x == b | x == k | -p(k,x) | -p(x,k). [resolve(175,c,2,b),merge(d)]. given #737 (F,wt=19): 992 b == k | -(x == g(f(f(f(f(k)))))) | x == g(f(f(f(f(m))))). [resolve(509,b,16,b)]. given #738 (F,wt=19): 993 b == k | -(g(f(f(f(f(m))))) == x) | g(f(f(f(f(k))))) == x. [resolve(509,b,16,a)]. given #739 (T,wt=19): 1004 b == k | -(x == f(f(f(f(f(k)))))) | x == f(f(f(f(f(m))))). [resolve(510,b,16,b)]. given #740 (T,wt=19): 1005 b == k | -(f(f(f(f(f(m))))) == x) | f(f(f(f(f(k))))) == x. [resolve(510,b,16,a)]. given #741 (A,wt=24): 366 p(m,b) | b == k | k == b | -p(k,b) | g(k) == b | g(k) == k | -p(k,g(k)). [resolve(362,c,2,f)]. given #742 (F,wt=19): 1012 b == k | -(x == g(g(g(g(g(m)))))) | x == g(g(g(g(g(k))))). [resolve(517,b,16,b)]. given #743 (F,wt=19): 1013 b == k | -(g(g(g(g(g(k))))) == x) | g(g(g(g(g(m))))) == x. [resolve(517,b,16,a)]. given #744 (T,wt=19): 1018 b == k | -(x == f(g(g(g(g(m)))))) | x == f(g(g(g(g(k))))). [resolve(518,b,16,b)]. given #745 (T,wt=19): 1019 b == k | -(f(g(g(g(g(k))))) == x) | f(g(g(g(g(m))))) == x. [resolve(518,b,16,a)]. given #746 (A,wt=25): 367 p(m,b) | b == k | g(k) == b | -p(g(k),b) | k == b | k == g(k) | -p(k,g(k)). [resolve(362,c,2,e)]. given #747 (F,wt=19): 1026 b == k | -(x == g(f(g(g(g(m)))))) | x == g(f(g(g(g(k))))). [resolve(523,b,16,b)]. given #748 (F,wt=19): 1027 b == k | -(g(f(g(g(g(k))))) == x) | g(f(g(g(g(m))))) == x. [resolve(523,b,16,a)]. given #749 (T,wt=19): 1038 b == k | -(x == f(f(g(g(g(m)))))) | x == f(f(g(g(g(k))))). [resolve(524,b,16,b)]. given #750 (T,wt=19): 1039 b == k | -(f(f(g(g(g(k))))) == x) | f(f(g(g(g(m))))) == x. [resolve(524,b,16,a)]. given #751 (A,wt=22): 371 p(m,b) | b == k | g(m) == b | -p(g(m),b) | m == g(m) | -p(m,g(m)). [resolve(368,c,2,e),unit_del(e,21)]. given #752 (F,wt=19): 1046 b == k | -(x == g(g(f(g(g(m)))))) | x == g(g(f(g(g(k))))). [resolve(532,b,16,b)]. given #753 (F,wt=19): 1047 b == k | -(g(g(f(g(g(k))))) == x) | g(g(f(g(g(m))))) == x. [resolve(532,b,16,a)]. given #754 (T,wt=19): 1052 b == k | -(x == f(g(f(g(g(m)))))) | x == f(g(f(g(g(k))))). [resolve(533,b,16,b)]. given #755 (T,wt=19): 1053 b == k | -(f(g(f(g(g(k))))) == x) | f(g(f(g(g(m))))) == x. [resolve(533,b,16,a)]. given #756 (A,wt=24): 378 k == b | p(k,b) | b == k | -p(m,b) | g(k) == b | g(k) == m | -p(m,g(k)). [resolve(196,a,2,f),unit_del(d,21)]. given #757 (F,wt=19): 1060 b == k | -(x == g(f(f(g(g(m)))))) | x == g(f(f(g(g(k))))). [resolve(538,b,16,b)]. given #758 (F,wt=19): 1061 b == k | -(g(f(f(g(g(k))))) == x) | g(f(f(g(g(m))))) == x. [resolve(538,b,16,a)]. given #759 (T,wt=19): 1072 b == k | -(x == f(f(f(g(g(m)))))) | x == f(f(f(g(g(k))))). [resolve(539,b,16,b)]. given #760 (T,wt=19): 1073 b == k | -(f(f(f(g(g(k))))) == x) | f(f(f(g(g(m))))) == x. [resolve(539,b,16,a)]. given #761 (A,wt=25): 379 k == b | p(k,b) | b == k | g(k) == b | -p(g(k),b) | m == g(k) | -p(m,g(k)). [resolve(196,a,2,e),unit_del(f,21)]. given #762 (F,wt=19): 1080 b == k | -(x == g(g(g(f(g(m)))))) | x == g(g(g(f(g(k))))). [resolve(546,b,16,b)]. given #763 (F,wt=19): 1081 b == k | -(g(g(g(f(g(k))))) == x) | g(g(g(f(g(m))))) == x. [resolve(546,b,16,a)]. given #764 (T,wt=19): 1086 b == k | -(x == f(g(g(f(g(m)))))) | x == f(g(g(f(g(k))))). [resolve(547,b,16,b)]. given #765 (T,wt=19): 1087 b == k | -(f(g(g(f(g(k))))) == x) | f(g(g(f(g(m))))) == x. [resolve(547,b,16,a)]. given #766 (A,wt=22): 381 p(m,b) | g(m) == m | p(g(m),m) | f(g(m)) == m | f(g(m)) == g(m). [resolve(97,f,29,c),merge(f),merge(g)]. given #767 (F,wt=19): 1094 b == k | -(x == g(f(g(f(g(m)))))) | x == g(f(g(f(g(k))))). [resolve(552,b,16,b)]. given #768 (F,wt=19): 1095 b == k | -(g(f(g(f(g(k))))) == x) | g(f(g(f(g(m))))) == x. [resolve(552,b,16,a)]. given #769 (T,wt=19): 1106 b == k | -(x == f(f(g(f(g(m)))))) | x == f(f(g(f(g(k))))). [resolve(553,b,16,b)]. given #770 (T,wt=19): 1107 b == k | -(f(f(g(f(g(k))))) == x) | f(f(g(f(g(m))))) == x. [resolve(553,b,16,a)]. given #771 (A,wt=25): 384 p(m,b) | b == k | g(k) == b | -p(g(k),b) | k == b | k == g(k) | -p(g(k),k). [resolve(380,c,2,f)]. given #772 (F,wt=19): 1114 b == k | -(x == g(g(f(f(g(m)))))) | x == g(g(f(f(g(k))))). [resolve(560,b,16,b)]. given #773 (F,wt=19): 1115 b == k | -(g(g(f(f(g(k))))) == x) | g(g(f(f(g(m))))) == x. [resolve(560,b,16,a)]. given #774 (T,wt=19): 1120 b == k | -(x == f(g(f(f(g(m)))))) | x == f(g(f(f(g(k))))). [resolve(561,b,16,b)]. given #775 (T,wt=19): 1121 b == k | -(f(g(f(f(g(k))))) == x) | f(g(f(f(g(m))))) == x. [resolve(561,b,16,a)]. given #776 (A,wt=24): 385 p(m,b) | b == k | k == b | -p(k,b) | g(k) == b | g(k) == k | -p(g(k),k). [resolve(380,c,2,e)]. given #777 (F,wt=19): 1128 b == k | -(x == g(f(f(f(g(m)))))) | x == g(f(f(f(g(k))))). [resolve(566,b,16,b)]. given #778 (F,wt=19): 1129 b == k | -(g(f(f(f(g(k))))) == x) | g(f(f(f(g(m))))) == x. [resolve(566,b,16,a)]. given #779 (T,wt=19): 1140 b == k | -(x == f(f(f(f(g(m)))))) | x == f(f(f(f(g(k))))). [resolve(567,b,16,b)]. given #780 (T,wt=19): 1141 b == k | -(f(f(f(f(g(k))))) == x) | f(f(f(f(g(m))))) == x. [resolve(567,b,16,a)]. given #781 (A,wt=22): 389 p(m,b) | b == k | g(m) == b | -p(g(m),b) | m == g(m) | -p(g(m),m). [resolve(386,c,2,f),unit_del(e,21)]. given #782 (F,wt=18): 2972 p(m,b) | b == k | g(m) == b | -p(g(m),b) | m == g(m). [resolve(389,f,368,c),merge(f),merge(g)]. given #783 (F,wt=19): 1148 b == k | -(x == g(g(g(g(f(m)))))) | x == g(g(g(g(f(k))))). [resolve(574,b,16,b)]. given #784 (T,wt=19): 1149 b == k | -(g(g(g(g(f(k))))) == x) | g(g(g(g(f(m))))) == x. [resolve(574,b,16,a)]. given #785 (T,wt=19): 1154 b == k | -(x == f(g(g(g(f(m)))))) | x == f(g(g(g(f(k))))). [resolve(575,b,16,b)]. given #786 (A,wt=23): 391 p(m,b) | g(m) == m | f(g(m)) == m | p(f(g(m)),m) | g(m) == f(g(m)). [resolve(98,f,29,c),merge(f),merge(g)]. given #787 (F,wt=19): 1155 b == k | -(f(g(g(g(f(k))))) == x) | f(g(g(g(f(m))))) == x. [resolve(575,b,16,a)]. given #788 (F,wt=19): 1162 b == k | -(x == g(f(g(g(f(m)))))) | x == g(f(g(g(f(k))))). [resolve(580,b,16,b)]. given #789 (T,wt=19): 1163 b == k | -(g(f(g(g(f(k))))) == x) | g(f(g(g(f(m))))) == x. [resolve(580,b,16,a)]. given #790 (T,wt=19): 1174 b == k | -(x == f(f(g(g(f(m)))))) | x == f(f(g(g(f(k))))). [resolve(581,b,16,b)]. given #791 (A,wt=25): 394 k == b | p(k,b) | b == k | g(m) == b | -p(g(m),b) | k == g(m) | -p(g(m),k). [resolve(211,a,2,f),merge(f)]. given #792 (F,wt=19): 1175 b == k | -(f(f(g(g(f(k))))) == x) | f(f(g(g(f(m))))) == x. [resolve(581,b,16,a)]. given #793 (F,wt=19): 1182 b == k | -(x == g(g(f(g(f(m)))))) | x == g(g(f(g(f(k))))). [resolve(588,b,16,b)]. given #794 (T,wt=19): 1183 b == k | -(g(g(f(g(f(k))))) == x) | g(g(f(g(f(m))))) == x. [resolve(588,b,16,a)]. given #795 (T,wt=19): 1188 b == k | -(x == f(g(f(g(f(m)))))) | x == f(g(f(g(f(k))))). [resolve(589,b,16,b)]. given #796 (A,wt=25): 398 b == k | p(g(g(g(k))),g(g(g(g(m))))) | g(g(g(k))) == b | p(g(g(g(k))),b). [resolve(229,b,41,a)]. given #797 (F,wt=19): 1189 b == k | -(f(g(f(g(f(k))))) == x) | f(g(f(g(f(m))))) == x. [resolve(589,b,16,a)]. given #798 (F,wt=19): 1196 b == k | -(x == g(f(f(g(f(m)))))) | x == g(f(f(g(f(k))))). [resolve(594,b,16,b)]. given #799 (T,wt=19): 1197 b == k | -(g(f(f(g(f(k))))) == x) | g(f(f(g(f(m))))) == x. [resolve(594,b,16,a)]. given #800 (T,wt=19): 1208 b == k | -(x == f(f(f(g(f(m)))))) | x == f(f(f(g(f(k))))). [resolve(595,b,16,b)]. given #801 (A,wt=29): 399 b == k | p(g(g(g(g(g(k))))),g(g(g(g(m))))) | g(g(g(g(k)))) == b | p(g(g(g(g(k)))),b). [resolve(229,b,40,a)]. given #802 (F,wt=19): 1209 b == k | -(f(f(f(g(f(k))))) == x) | f(f(f(g(f(m))))) == x. [resolve(595,b,16,a)]. given #803 (F,wt=19): 1216 b == k | -(x == g(g(g(f(f(m)))))) | x == g(g(g(f(f(k))))). [resolve(602,b,16,b)]. given #804 (T,wt=19): 1217 b == k | -(g(g(g(f(f(k))))) == x) | g(g(g(f(f(m))))) == x. [resolve(602,b,16,a)]. given #805 (T,wt=19): 1222 b == k | -(x == f(g(g(f(f(m)))))) | x == f(g(g(f(f(k))))). [resolve(603,b,16,b)]. given #806 (A,wt=29): 400 b == k | p(g(g(g(g(m)))),g(g(g(g(g(k)))))) | g(g(g(g(k)))) == b | p(g(g(g(g(k)))),b). [resolve(229,b,39,a)]. given #807 (F,wt=19): 1223 b == k | -(f(g(g(f(f(k))))) == x) | f(g(g(f(f(m))))) == x. [resolve(603,b,16,a)]. given #808 (F,wt=19): 1230 b == k | -(x == g(f(g(f(f(m)))))) | x == g(f(g(f(f(k))))). [resolve(608,b,16,b)]. given #809 (T,wt=19): 1231 b == k | -(g(f(g(f(f(k))))) == x) | g(f(g(f(f(m))))) == x. [resolve(608,b,16,a)]. given #810 (T,wt=19): 1242 b == k | -(x == f(f(g(f(f(m)))))) | x == f(f(g(f(f(k))))). [resolve(609,b,16,b)]. given #811 (A,wt=25): 401 b == k | p(g(g(g(g(m)))),g(g(g(k)))) | g(g(g(k))) == b | p(g(g(g(k))),b). [resolve(229,b,38,a)]. given #812 (F,wt=19): 1243 b == k | -(f(f(g(f(f(k))))) == x) | f(f(g(f(f(m))))) == x. [resolve(609,b,16,a)]. given #813 (F,wt=19): 1250 b == k | -(x == g(g(f(f(f(m)))))) | x == g(g(f(f(f(k))))). [resolve(619,b,16,b)]. given #814 (T,wt=19): 1251 b == k | -(g(g(f(f(f(k))))) == x) | g(g(f(f(f(m))))) == x. [resolve(619,b,16,a)]. given #815 (T,wt=19): 1256 b == k | -(x == f(g(f(f(f(m)))))) | x == f(g(f(f(f(k))))). [resolve(620,b,16,b)]. given #816 (A,wt=29): 406 b == k | p(g(f(g(g(g(k))))),f(g(g(g(m))))) | f(g(g(g(k)))) == b | p(f(g(g(g(k)))),b). [resolve(230,b,40,a)]. given #817 (F,wt=19): 1257 b == k | -(f(g(f(f(f(k))))) == x) | f(g(f(f(f(m))))) == x. [resolve(620,b,16,a)]. given #818 (F,wt=19): 1264 b == k | -(x == g(f(f(f(f(m)))))) | x == g(f(f(f(f(k))))). [resolve(625,b,16,b)]. given #819 (T,wt=19): 1265 b == k | -(g(f(f(f(f(k))))) == x) | g(f(f(f(f(m))))) == x. [resolve(625,b,16,a)]. given #820 (T,wt=19): 1276 b == k | -(x == f(f(f(f(f(m)))))) | x == f(f(f(f(f(k))))). [resolve(626,b,16,b)]. given #821 (A,wt=29): 407 b == k | p(f(g(g(g(m)))),g(f(g(g(g(k)))))) | f(g(g(g(k)))) == b | p(f(g(g(g(k)))),b). [resolve(230,b,39,a)]. given #822 (F,wt=19): 1277 b == k | -(f(f(f(f(f(k))))) == x) | f(f(f(f(f(m))))) == x. [resolve(626,b,16,a)]. given #823 (F,wt=19): 1325 b == k | g(g(k)) == b | p(g(g(k)),b) | -(g(g(g(m))) == b). [factor(1320,c,e)]. given #824 (T,wt=19): 1357 b == k | f(g(k)) == b | p(f(g(k)),b) | -(g(f(g(m))) == b). [factor(1352,c,e)]. given #825 (T,wt=19): 1403 b == k | f(b) == m | b == f(b) | f(b) == k | f(b) == b. [resolve(1398,d,3,d),merge(e)]. given #826 (A,wt=25): 413 b == k | p(f(g(g(k))),g(f(g(g(m))))) | f(g(g(k))) == b | p(f(g(g(k))),b). [resolve(235,b,41,a)]. given #827 (F,wt=15): 3016 b == k | f(b) == m | b == f(b) | f(b) == b. [resolve(1403,d,45,b),merge(e),merge(f)]. given #828 (F,wt=11): 3024 b == k | b == f(b) | f(b) == b. [resolve(3016,b,92,b),merge(d)]. given #829 (T,wt=7): 3026 b == k | b == f(b). [resolve(3024,c,91,b),merge(c)]. given #830 (T,wt=7): 3032 b == k | p(f(b),m). [resolve(3026,b,88,b),merge(b)]. given #831 (A,wt=29): 414 b == k | p(g(g(f(g(g(k))))),g(f(g(g(m))))) | g(f(g(g(k)))) == b | p(g(f(g(g(k)))),b). [resolve(235,b,40,a)]. given #832 (F,wt=7): 3033 b == k | p(f(b),k). [resolve(3026,b,51,b),merge(b)]. given #833 (F,wt=7): 3038 b == k | f(b) == b. [resolve(3026,b,15,a)]. given #834 (T,wt=3): 3055 b == k. [resolve(3038,b,91,b),merge(b)]. given #835 (T,wt=3): 3063 k == b. [resolve(3055,a,15,a)]. given #836 (A,wt=29): 415 b == k | p(g(f(g(g(m)))),g(g(f(g(g(k)))))) | g(f(g(g(k)))) == b | p(g(f(g(g(k)))),b). [resolve(235,b,39,a)]. given #837 (F,wt=3): 3064 -(k == m). [ur(16,a,3055,a,c,42,a)]. given #838 (F,wt=3): 3073 -(m == k). [ur(16,b,3063,a,c,21,a)]. given #839 (T,wt=3): 3074 p(m,b). [back_unit_del(3068),unit_del(a,3073)]. given #840 (T,wt=3): 3077 p(m,k). [back_unit_del(37),unit_del(a,3073)]. given #841 (A,wt=25): 416 b == k | p(g(f(g(g(m)))),f(g(g(k)))) | f(g(g(k))) == b | p(f(g(g(k))),b). [resolve(235,b,38,a)]. given #842 (F,wt=5): 3059 g(b) == g(k). [resolve(3055,a,20,a)]. given #843 (F,wt=5): 3060 f(b) == f(k). [resolve(3055,a,19,a)]. given #844 (T,wt=5): 3069 g(k) == g(b). [resolve(3063,a,20,a)]. given #845 (T,wt=5): 3070 f(k) == f(b). [resolve(3063,a,19,a)]. given #846 (A,wt=29): 421 b == k | p(g(f(f(g(g(k))))),f(f(g(g(m))))) | f(f(g(g(k)))) == b | p(f(f(g(g(k)))),b). [resolve(236,b,40,a)]. given #847 (F,wt=6): 3054 b == k | p(b,b). [resolve(3038,b,103,b),merge(b)]. given #848 (F,wt=6): 3058 b == j | p(b,j). [resolve(3055,a,24,c)]. given #849 (T,wt=6): 3061 -(x == b) | x == k. [resolve(3055,a,16,b)]. given #850 (T,wt=6): 3062 -(k == x) | b == x. [resolve(3055,a,16,a)]. given #851 (A,wt=29): 422 b == k | p(f(f(g(g(m)))),g(f(f(g(g(k)))))) | f(f(g(g(k)))) == b | p(f(f(g(g(k)))),b). [resolve(236,b,39,a)]. given #852 (F,wt=6): 3067 k == j | p(b,j). [resolve(3063,a,63,b)]. given #853 (F,wt=6): 3071 -(x == k) | x == b. [resolve(3063,a,16,b)]. given #854 (T,wt=6): 3072 -(b == x) | k == x. [resolve(3063,a,16,a)]. given #855 (T,wt=6): 3075 -(m == x) | p(x,k). [back_unit_del(54),unit_del(a,3073)]. given #856 (A,wt=25): 427 b == k | p(g(f(g(k))),g(g(f(g(m))))) | g(f(g(k))) == b | p(g(f(g(k))),b). [resolve(243,b,41,a)]. given #857 (F,wt=6): 3076 -(k == x) | p(m,x). [back_unit_del(53),unit_del(a,3073)]. given #858 (F,wt=6): 3080 -(b == x) | p(m,x). [resolve(3074,a,18,b)]. given #859 (T,wt=6): 3081 -(m == x) | p(x,b). [resolve(3074,a,17,b)]. given #860 (T,wt=7): 3039 b == k | -(f(b) == k). [factor(3037,a,c)]. given #861 (A,wt=29): 428 b == k | p(g(g(g(f(g(k))))),g(g(f(g(m))))) | g(g(f(g(k)))) == b | p(g(g(f(g(k)))),b). [resolve(243,b,40,a)]. given #862 (F,wt=7): 3086 g(g(b)) == g(g(k)). [resolve(3059,a,20,a)]. given #863 (F,wt=7): 3087 f(g(b)) == f(g(k)). [resolve(3059,a,19,a)]. given #864 (T,wt=7): 3093 g(f(b)) == g(f(k)). [resolve(3060,a,20,a)]. given #865 (T,wt=7): 3094 f(f(b)) == f(f(k)). [resolve(3060,a,19,a)]. given #866 (A,wt=29): 429 b == k | p(g(g(f(g(m)))),g(g(g(f(g(k)))))) | g(g(f(g(k)))) == b | p(g(g(f(g(k)))),b). [resolve(243,b,39,a)]. given #867 (F,wt=7): 3100 g(g(k)) == g(g(b)). [resolve(3069,a,20,a)]. given #868 (F,wt=7): 3101 f(g(k)) == f(g(b)). [resolve(3069,a,19,a)]. given #869 (T,wt=7): 3107 g(f(k)) == g(f(b)). [resolve(3070,a,20,a)]. given #870 (T,wt=7): 3108 f(f(k)) == f(f(b)). [resolve(3070,a,19,a)]. given #871 (A,wt=25): 430 b == k | p(g(g(f(g(m)))),g(f(g(k)))) | g(f(g(k))) == b | p(g(f(g(k))),b). [resolve(243,b,38,a)]. given #872 (F,wt=8): 3031 b == k | p(f(b),f(b)). [resolve(3026,b,104,b),merge(b)]. given #873 (F,wt=8): 3088 -(x == g(b)) | x == g(k). [resolve(3059,a,16,b)]. given #874 (T,wt=8): 3089 -(g(k) == x) | g(b) == x. [resolve(3059,a,16,a)]. given #875 (T,wt=8): 3095 -(x == f(b)) | x == f(k). [resolve(3060,a,16,b)]. given #876 (A,wt=29): 435 b == k | p(g(f(g(f(g(k))))),f(g(f(g(m))))) | f(g(f(g(k)))) == b | p(f(g(f(g(k)))),b). [resolve(244,b,40,a)]. given #877 (F,wt=8): 3096 -(f(k) == x) | f(b) == x. [resolve(3060,a,16,a)]. given #878 (F,wt=8): 3102 -(x == g(k)) | x == g(b). [resolve(3069,a,16,b)]. given #879 (T,wt=8): 3103 -(g(b) == x) | g(k) == x. [resolve(3069,a,16,a)]. given #880 (T,wt=8): 3109 -(x == f(k)) | x == f(b). [resolve(3070,a,16,b)]. given #881 (A,wt=29): 436 b == k | p(f(g(f(g(m)))),g(f(g(f(g(k)))))) | f(g(f(g(k)))) == b | p(f(g(f(g(k)))),b). [resolve(244,b,39,a)]. given #882 (F,wt=8): 3110 -(f(b) == x) | f(k) == x. [resolve(3070,a,16,a)]. given #883 (F,wt=9): 3034 b == k | g(b) == g(f(b)). [resolve(3026,b,20,a)]. given #884 (T,wt=9): 3035 b == k | f(b) == f(f(b)). [resolve(3026,b,19,a)]. given #885 (T,wt=9): 3113 b == j | -(j == x) | p(b,x). [resolve(3058,b,18,b)]. given #886 (A,wt=27): 441 p(m,b) | g(m) == m | f(g(m)) == b | -p(f(g(m)),b) | g(m) == b | g(m) == f(g(m)). [resolve(108,g,28,c),merge(g),merge(h)]. given #887 (F,wt=9): 3114 b == j | -(b == x) | p(x,j). [resolve(3058,b,17,b)]. given #888 (F,wt=6): 3189 b == j | p(k,j). [resolve(3114,b,3055,a)]. given #889 (T,wt=9): 3118 k == j | -(j == x) | p(b,x). [resolve(3067,b,18,b)]. given #890 (T,wt=9): 3119 k == j | -(b == x) | p(x,j). [resolve(3067,b,17,b)]. given #891 (A,wt=25): 442 b == k | p(f(f(g(k))),g(f(f(g(m))))) | f(f(g(k))) == b | p(f(f(g(k))),b). [resolve(249,b,41,a)]. given #892 (F,wt=9): 3127 g(g(g(b))) == g(g(g(k))). [resolve(3086,a,20,a)]. given #893 (F,wt=9): 3128 f(g(g(b))) == f(g(g(k))). [resolve(3086,a,19,a)]. given #894 (T,wt=9): 3134 g(f(g(b))) == g(f(g(k))). [resolve(3087,a,20,a)]. given #895 (T,wt=9): 3135 f(f(g(b))) == f(f(g(k))). [resolve(3087,a,19,a)]. given #896 (A,wt=29): 443 b == k | p(g(g(f(f(g(k))))),g(f(f(g(m))))) | g(f(f(g(k)))) == b | p(g(f(f(g(k)))),b). [resolve(249,b,40,a)]. given #897 (F,wt=9): 3144 g(g(f(b))) == g(g(f(k))). [resolve(3093,a,20,a)]. given #898 (F,wt=9): 3145 f(g(f(b))) == f(g(f(k))). [resolve(3093,a,19,a)]. given #899 (T,wt=9): 3151 g(f(f(b))) == g(f(f(k))). [resolve(3094,a,20,a)]. given #900 (T,wt=9): 3152 f(f(f(b))) == f(f(f(k))). [resolve(3094,a,19,a)]. given #901 (A,wt=29): 444 b == k | p(g(f(f(g(m)))),g(g(f(f(g(k)))))) | g(f(f(g(k)))) == b | p(g(f(f(g(k)))),b). [resolve(249,b,39,a)]. given #902 (F,wt=9): 3161 g(g(g(k))) == g(g(g(b))). [resolve(3100,a,20,a)]. given #903 (F,wt=9): 3162 f(g(g(k))) == f(g(g(b))). [resolve(3100,a,19,a)]. given #904 (T,wt=9): 3168 g(f(g(k))) == g(f(g(b))). [resolve(3101,a,20,a)]. given #905 (T,wt=9): 3169 f(f(g(k))) == f(f(g(b))). [resolve(3101,a,19,a)]. given #906 (A,wt=25): 445 b == k | p(g(f(f(g(m)))),f(f(g(k)))) | f(f(g(k))) == b | p(f(f(g(k))),b). [resolve(249,b,38,a)]. given #907 (F,wt=9): 3178 g(g(f(k))) == g(g(f(b))). [resolve(3107,a,20,a)]. given #908 (F,wt=9): 3179 f(g(f(k))) == f(g(f(b))). [resolve(3107,a,19,a)]. given #909 (T,wt=9): 3185 g(f(f(k))) == g(f(f(b))). [resolve(3108,a,20,a)]. given #910 (T,wt=9): 3186 f(f(f(k))) == f(f(f(b))). [resolve(3108,a,19,a)]. given #911 (A,wt=29): 450 b == k | p(g(f(f(f(g(k))))),f(f(f(g(m))))) | f(f(f(g(k)))) == b | p(f(f(f(g(k)))),b). [resolve(250,b,40,a)]. given #912 (F,wt=9): 3190 b == j | -(j == x) | p(k,x). [resolve(3189,b,18,b)]. given #913 (F,wt=9): 3191 b == j | -(k == x) | p(x,j). [resolve(3189,b,17,b)]. given #914 (T,wt=10): 3025 b == k | b == f(b) | p(b,b). [resolve(3024,c,103,b),merge(c)]. given #915 (T,wt=10): 3036 b == k | -(x == b) | x == f(b). [resolve(3026,b,16,b)]. given #916 (A,wt=29): 451 b == k | p(f(f(f(g(m)))),g(f(f(f(g(k)))))) | f(f(f(g(k)))) == b | p(f(f(f(g(k)))),b). [resolve(250,b,39,a)]. given #917 (F,wt=10): 3037 b == k | -(f(b) == x) | b == x. [resolve(3026,b,16,a)]. given #918 (F,wt=10): 3040 b == k | -(m == x) | p(f(b),x). [resolve(3032,b,18,b)]. given #919 (T,wt=10): 3041 b == k | -(f(b) == x) | p(x,m). [resolve(3032,b,17,b)]. given #920 (T,wt=10): 3052 b == k | -(k == x) | p(f(b),x). [resolve(3033,b,18,b)]. given #921 (A,wt=25): 456 b == k | p(g(g(f(k))),g(g(g(f(m))))) | g(g(f(k))) == b | p(g(g(f(k))),b). [resolve(257,b,41,a)]. given #922 (F,wt=10): 3053 b == k | -(f(b) == x) | p(x,k). [resolve(3033,b,17,b)]. given #923 (F,wt=10): 3129 -(x == g(g(b))) | x == g(g(k)). [resolve(3086,a,16,b)]. given #924 (T,wt=10): 3130 -(g(g(k)) == x) | g(g(b)) == x. [resolve(3086,a,16,a)]. given #925 (T,wt=10): 3136 -(x == f(g(b))) | x == f(g(k)). [resolve(3087,a,16,b)]. given #926 (A,wt=29): 457 b == k | p(g(g(g(g(f(k))))),g(g(g(f(m))))) | g(g(g(f(k)))) == b | p(g(g(g(f(k)))),b). [resolve(257,b,40,a)]. given #927 (F,wt=10): 3137 -(f(g(k)) == x) | f(g(b)) == x. [resolve(3087,a,16,a)]. given #928 (F,wt=10): 3146 -(x == g(f(b))) | x == g(f(k)). [resolve(3093,a,16,b)]. given #929 (T,wt=10): 3147 -(g(f(k)) == x) | g(f(b)) == x. [resolve(3093,a,16,a)]. given #930 (T,wt=10): 3153 -(x == f(f(b))) | x == f(f(k)). [resolve(3094,a,16,b)]. given #931 (A,wt=29): 458 b == k | p(g(g(g(f(m)))),g(g(g(g(f(k)))))) | g(g(g(f(k)))) == b | p(g(g(g(f(k)))),b). [resolve(257,b,39,a)]. given #932 (F,wt=10): 3154 -(f(f(k)) == x) | f(f(b)) == x. [resolve(3094,a,16,a)]. given #933 (F,wt=10): 3163 -(x == g(g(k))) | x == g(g(b)). [resolve(3100,a,16,b)]. given #934 (T,wt=10): 3164 -(g(g(b)) == x) | g(g(k)) == x. [resolve(3100,a,16,a)]. given #935 (T,wt=10): 3170 -(x == f(g(k))) | x == f(g(b)). [resolve(3101,a,16,b)]. given #936 (A,wt=25): 459 b == k | p(g(g(g(f(m)))),g(g(f(k)))) | g(g(f(k))) == b | p(g(g(f(k))),b). [resolve(257,b,38,a)]. given #937 (F,wt=10): 3171 -(f(g(b)) == x) | f(g(k)) == x. [resolve(3101,a,16,a)]. given #938 (F,wt=10): 3180 -(x == g(f(k))) | x == g(f(b)). [resolve(3107,a,16,b)]. given #939 (T,wt=10): 3181 -(g(f(b)) == x) | g(f(k)) == x. [resolve(3107,a,16,a)]. given #940 (T,wt=10): 3187 -(x == f(f(k))) | x == f(f(b)). [resolve(3108,a,16,b)]. given #941 (A,wt=29): 464 b == k | p(g(f(g(g(f(k))))),f(g(g(f(m))))) | f(g(g(f(k)))) == b | p(f(g(g(f(k)))),b). [resolve(258,b,40,a)]. given #942 (F,wt=10): 3188 -(f(f(b)) == x) | f(f(k)) == x. [resolve(3108,a,16,a)]. given #943 (F,wt=11): 3199 g(g(g(g(b)))) == g(g(g(g(k)))). [resolve(3127,a,20,a)]. given #944 (T,wt=11): 3200 f(g(g(g(b)))) == f(g(g(g(k)))). [resolve(3127,a,19,a)]. given #945 (T,wt=11): 3206 g(f(g(g(b)))) == g(f(g(g(k)))). [resolve(3128,a,20,a)]. given #946 (A,wt=29): 465 b == k | p(f(g(g(f(m)))),g(f(g(g(f(k)))))) | f(g(g(f(k)))) == b | p(f(g(g(f(k)))),b). [resolve(258,b,39,a)]. given #947 (F,wt=11): 3207 f(f(g(g(b)))) == f(f(g(g(k)))). [resolve(3128,a,19,a)]. given #948 (F,wt=11): 3216 g(g(f(g(b)))) == g(g(f(g(k)))). [resolve(3134,a,20,a)]. given #949 (T,wt=11): 3217 f(g(f(g(b)))) == f(g(f(g(k)))). [resolve(3134,a,19,a)]. given #950 (T,wt=11): 3223 g(f(f(g(b)))) == g(f(f(g(k)))). [resolve(3135,a,20,a)]. given #951 (A,wt=25): 470 b == k | p(f(g(f(k))),g(f(g(f(m))))) | f(g(f(k))) == b | p(f(g(f(k))),b). [resolve(263,b,41,a)]. given #952 (F,wt=11): 3224 f(f(f(g(b)))) == f(f(f(g(k)))). [resolve(3135,a,19,a)]. given #953 (F,wt=11): 3233 g(g(g(f(b)))) == g(g(g(f(k)))). [resolve(3144,a,20,a)]. given #954 (T,wt=11): 3234 f(g(g(f(b)))) == f(g(g(f(k)))). [resolve(3144,a,19,a)]. given #955 (T,wt=11): 3240 g(f(g(f(b)))) == g(f(g(f(k)))). [resolve(3145,a,20,a)]. given #956 (A,wt=29): 471 b == k | p(g(g(f(g(f(k))))),g(f(g(f(m))))) | g(f(g(f(k)))) == b | p(g(f(g(f(k)))),b). [resolve(263,b,40,a)]. given #957 (F,wt=11): 3241 f(f(g(f(b)))) == f(f(g(f(k)))). [resolve(3145,a,19,a)]. given #958 (F,wt=11): 3250 g(g(f(f(b)))) == g(g(f(f(k)))). [resolve(3151,a,20,a)]. given #959 (T,wt=11): 3251 f(g(f(f(b)))) == f(g(f(f(k)))). [resolve(3151,a,19,a)]. given #960 (T,wt=11): 3257 g(f(f(f(b)))) == g(f(f(f(k)))). [resolve(3152,a,20,a)]. given #961 (A,wt=29): 472 b == k | p(g(f(g(f(m)))),g(g(f(g(f(k)))))) | g(f(g(f(k)))) == b | p(g(f(g(f(k)))),b). [resolve(263,b,39,a)]. given #962 (F,wt=11): 3258 f(f(f(f(b)))) == f(f(f(f(k)))). [resolve(3152,a,19,a)]. given #963 (F,wt=11): 3267 g(g(g(g(k)))) == g(g(g(g(b)))). [resolve(3161,a,20,a)]. given #964 (T,wt=11): 3268 f(g(g(g(k)))) == f(g(g(g(b)))). [resolve(3161,a,19,a)]. given #965 (T,wt=11): 3274 g(f(g(g(k)))) == g(f(g(g(b)))). [resolve(3162,a,20,a)]. given #966 (A,wt=25): 473 b == k | p(g(f(g(f(m)))),f(g(f(k)))) | f(g(f(k))) == b | p(f(g(f(k))),b). [resolve(263,b,38,a)]. given #967 (F,wt=11): 3275 f(f(g(g(k)))) == f(f(g(g(b)))). [resolve(3162,a,19,a)]. given #968 (F,wt=11): 3284 g(g(f(g(k)))) == g(g(f(g(b)))). [resolve(3168,a,20,a)]. given #969 (T,wt=11): 3285 f(g(f(g(k)))) == f(g(f(g(b)))). [resolve(3168,a,19,a)]. given #970 (T,wt=11): 3291 g(f(f(g(k)))) == g(f(f(g(b)))). [resolve(3169,a,20,a)]. given #971 (A,wt=29): 478 b == k | p(g(f(f(g(f(k))))),f(f(g(f(m))))) | f(f(g(f(k)))) == b | p(f(f(g(f(k)))),b). [resolve(264,b,40,a)]. given #972 (F,wt=11): 3292 f(f(f(g(k)))) == f(f(f(g(b)))). [resolve(3169,a,19,a)]. given #973 (F,wt=11): 3301 g(g(g(f(k)))) == g(g(g(f(b)))). [resolve(3178,a,20,a)]. given #974 (T,wt=11): 3302 f(g(g(f(k)))) == f(g(g(f(b)))). [resolve(3178,a,19,a)]. given #975 (T,wt=11): 3308 g(f(g(f(k)))) == g(f(g(f(b)))). [resolve(3179,a,20,a)]. given #976 (A,wt=29): 479 b == k | p(f(f(g(f(m)))),g(f(f(g(f(k)))))) | f(f(g(f(k)))) == b | p(f(f(g(f(k)))),b). [resolve(264,b,39,a)]. given #977 (F,wt=11): 3309 f(f(g(f(k)))) == f(f(g(f(b)))). [resolve(3179,a,19,a)]. given #978 (F,wt=11): 3318 g(g(f(f(k)))) == g(g(f(f(b)))). [resolve(3185,a,20,a)]. given #979 (T,wt=11): 3319 f(g(f(f(k)))) == f(g(f(f(b)))). [resolve(3185,a,19,a)]. given #980 (T,wt=11): 3325 g(f(f(f(k)))) == g(f(f(f(b)))). [resolve(3186,a,20,a)]. given #981 (A,wt=25): 484 b == k | p(g(f(f(k))),g(g(f(f(m))))) | g(f(f(k))) == b | p(g(f(f(k))),b). [resolve(271,b,41,a)]. given #982 (F,wt=11): 3326 f(f(f(f(k)))) == f(f(f(f(b)))). [resolve(3186,a,19,a)]. given #983 (F,wt=12): 3045 b == k | f(b) == m | -(f(f(b)) == m). [resolve(3032,b,4,b)]. given #984 (T,wt=12): 3066 k == j | j == m | p(j,m) | -p(j,k). [back_unit_del(66),unit_del(d,3064)]. given #985 (T,wt=12): 3082 x == b | x == m | -p(m,x) | -p(x,m). [resolve(3074,a,2,b),unit_del(a,21)]. given #986 (A,wt=29): 485 b == k | p(g(g(g(f(f(k))))),g(g(f(f(m))))) | g(g(f(f(k)))) == b | p(g(g(f(f(k)))),b). [resolve(271,b,40,a)]. given #987 (F,wt=12): 3115 b == j | j == m | p(j,m) | -p(j,b). [resolve(3058,b,1,f),merge(e),unit_del(d,42)]. given #988 (F,wt=12): 3201 -(x == g(g(g(b)))) | x == g(g(g(k))). [resolve(3127,a,16,b)]. given #989 (T,wt=12): 3202 -(g(g(g(k))) == x) | g(g(g(b))) == x. [resolve(3127,a,16,a)]. given #990 (T,wt=12): 3208 -(x == f(g(g(b)))) | x == f(g(g(k))). [resolve(3128,a,16,b)]. given #991 (A,wt=29): 486 b == k | p(g(g(f(f(m)))),g(g(g(f(f(k)))))) | g(g(f(f(k)))) == b | p(g(g(f(f(k)))),b). [resolve(271,b,39,a)]. given #992 (F,wt=12): 3209 -(f(g(g(k))) == x) | f(g(g(b))) == x. [resolve(3128,a,16,a)]. given #993 (F,wt=12): 3218 -(x == g(f(g(b)))) | x == g(f(g(k))). [resolve(3134,a,16,b)]. given #994 (T,wt=12): 3219 -(g(f(g(k))) == x) | g(f(g(b))) == x. [resolve(3134,a,16,a)]. given #995 (T,wt=12): 3225 -(x == f(f(g(b)))) | x == f(f(g(k))). [resolve(3135,a,16,b)]. given #996 (A,wt=25): 487 b == k | p(g(g(f(f(m)))),g(f(f(k)))) | g(f(f(k))) == b | p(g(f(f(k))),b). [resolve(271,b,38,a)]. given #997 (F,wt=12): 3226 -(f(f(g(k))) == x) | f(f(g(b))) == x. [resolve(3135,a,16,a)]. given #998 (F,wt=12): 3235 -(x == g(g(f(b)))) | x == g(g(f(k))). [resolve(3144,a,16,b)]. given #999 (T,wt=12): 3236 -(g(g(f(k))) == x) | g(g(f(b))) == x. [resolve(3144,a,16,a)]. given #1000 (T,wt=12): 3242 -(x == f(g(f(b)))) | x == f(g(f(k))). [resolve(3145,a,16,b)]. given #1001 (A,wt=29): 492 b == k | p(g(f(g(f(f(k))))),f(g(f(f(m))))) | f(g(f(f(k)))) == b | p(f(g(f(f(k)))),b). [resolve(272,b,40,a)]. given #1002 (F,wt=12): 3243 -(f(g(f(k))) == x) | f(g(f(b))) == x. [resolve(3145,a,16,a)]. given #1003 (F,wt=12): 3252 -(x == g(f(f(b)))) | x == g(f(f(k))). [resolve(3151,a,16,b)]. given #1004 (T,wt=12): 3253 -(g(f(f(k))) == x) | g(f(f(b))) == x. [resolve(3151,a,16,a)]. given #1005 (T,wt=12): 3259 -(x == f(f(f(b)))) | x == f(f(f(k))). [resolve(3152,a,16,b)]. given #1006 (A,wt=29): 493 b == k | p(f(g(f(f(m)))),g(f(g(f(f(k)))))) | f(g(f(f(k)))) == b | p(f(g(f(f(k)))),b). [resolve(272,b,39,a)]. given #1007 (F,wt=12): 3260 -(f(f(f(k))) == x) | f(f(f(b))) == x. [resolve(3152,a,16,a)]. given #1008 (F,wt=12): 3269 -(x == g(g(g(k)))) | x == g(g(g(b))). [resolve(3161,a,16,b)]. given #1009 (T,wt=12): 3270 -(g(g(g(b))) == x) | g(g(g(k))) == x. [resolve(3161,a,16,a)]. given #1010 (T,wt=12): 3276 -(x == f(g(g(k)))) | x == f(g(g(b))). [resolve(3162,a,16,b)]. given #1011 (A,wt=25): 499 b == k | p(f(f(f(k))),g(f(f(f(m))))) | f(f(f(k))) == b | p(f(f(f(k))),b). [resolve(277,b,41,a)]. given #1012 (F,wt=12): 3277 -(f(g(g(b))) == x) | f(g(g(k))) == x. [resolve(3162,a,16,a)]. given #1013 (F,wt=12): 3286 -(x == g(f(g(k)))) | x == g(f(g(b))). [resolve(3168,a,16,b)]. given #1014 (T,wt=12): 3287 -(g(f(g(b))) == x) | g(f(g(k))) == x. [resolve(3168,a,16,a)]. given #1015 (T,wt=12): 3293 -(x == f(f(g(k)))) | x == f(f(g(b))). [resolve(3169,a,16,b)]. given #1016 (A,wt=29): 500 b == k | p(g(g(f(f(f(k))))),g(f(f(f(m))))) | g(f(f(f(k)))) == b | p(g(f(f(f(k)))),b). [resolve(277,b,40,a)]. given #1017 (F,wt=12): 3294 -(f(f(g(b))) == x) | f(f(g(k))) == x. [resolve(3169,a,16,a)]. given #1018 (F,wt=12): 3303 -(x == g(g(f(k)))) | x == g(g(f(b))). [resolve(3178,a,16,b)]. given #1019 (T,wt=12): 3304 -(g(g(f(b))) == x) | g(g(f(k))) == x. [resolve(3178,a,16,a)]. given #1020 (T,wt=12): 3310 -(x == f(g(f(k)))) | x == f(g(f(b))). [resolve(3179,a,16,b)]. given #1021 (A,wt=29): 501 b == k | p(g(f(f(f(m)))),g(g(f(f(f(k)))))) | g(f(f(f(k)))) == b | p(g(f(f(f(k)))),b). [resolve(277,b,39,a)]. given #1022 (F,wt=12): 3311 -(f(g(f(b))) == x) | f(g(f(k))) == x. [resolve(3179,a,16,a)]. given #1023 (F,wt=12): 3320 -(x == g(f(f(k)))) | x == g(f(f(b))). [resolve(3185,a,16,b)]. given #1024 (T,wt=12): 3321 -(g(f(f(b))) == x) | g(f(f(k))) == x. [resolve(3185,a,16,a)]. given #1025 (T,wt=12): 3327 -(x == f(f(f(k)))) | x == f(f(f(b))). [resolve(3186,a,16,b)]. given #1026 (A,wt=25): 502 b == k | p(g(f(f(f(m)))),f(f(f(k)))) | f(f(f(k))) == b | p(f(f(f(k))),b). [resolve(277,b,38,a)]. given #1027 (F,wt=12): 3328 -(f(f(f(b))) == x) | f(f(f(k))) == x. [resolve(3186,a,16,a)]. given #1028 (F,wt=13): 3042 b == k | f(b) == m | p(f(f(b)),f(b)). [resolve(3032,b,7,b)]. given #1029 (T,wt=13): 3043 b == k | f(b) == m | p(f(b),f(f(b))). [resolve(3032,b,6,b)]. given #1030 (T,wt=13): 3044 b == k | f(b) == m | -(f(f(b)) == f(b)). [resolve(3032,b,5,b)]. given #1031 (A,wt=29): 507 b == k | p(g(f(f(f(f(k))))),f(f(f(f(m))))) | f(f(f(f(k)))) == b | p(f(f(f(f(k)))),b). [resolve(278,b,40,a)]. given #1032 (F,wt=13): 3335 g(g(g(g(g(b))))) == g(g(g(g(g(k))))). [resolve(3199,a,20,a)]. given #1033 (F,wt=13): 3336 f(g(g(g(g(b))))) == f(g(g(g(g(k))))). [resolve(3199,a,19,a)]. given #1034 (T,wt=13): 3342 g(f(g(g(g(b))))) == g(f(g(g(g(k))))). [resolve(3200,a,20,a)]. given #1035 (T,wt=13): 3343 f(f(g(g(g(b))))) == f(f(g(g(g(k))))). [resolve(3200,a,19,a)]. given #1036 (A,wt=29): 508 b == k | p(f(f(f(f(m)))),g(f(f(f(f(k)))))) | f(f(f(f(k)))) == b | p(f(f(f(f(k)))),b). [resolve(278,b,39,a)]. given #1037 (F,wt=13): 3352 g(g(f(g(g(b))))) == g(g(f(g(g(k))))). [resolve(3206,a,20,a)]. given #1038 (F,wt=13): 3353 f(g(f(g(g(b))))) == f(g(f(g(g(k))))). [resolve(3206,a,19,a)]. given #1039 (T,wt=13): 3359 g(f(f(g(g(b))))) == g(f(f(g(g(k))))). [resolve(3207,a,20,a)]. given #1040 (T,wt=13): 3360 f(f(f(g(g(b))))) == f(f(f(g(g(k))))). [resolve(3207,a,19,a)]. given #1041 (A,wt=25): 513 b == k | p(g(g(g(m))),g(g(g(g(k))))) | g(g(g(m))) == b | p(g(g(g(m))),b). [resolve(285,b,41,a)]. given #1042 (F,wt=13): 3369 g(g(g(f(g(b))))) == g(g(g(f(g(k))))). [resolve(3216,a,20,a)]. given #1043 (F,wt=13): 3370 f(g(g(f(g(b))))) == f(g(g(f(g(k))))). [resolve(3216,a,19,a)]. given #1044 (T,wt=13): 3376 g(f(g(f(g(b))))) == g(f(g(f(g(k))))). [resolve(3217,a,20,a)]. given #1045 (T,wt=13): 3377 f(f(g(f(g(b))))) == f(f(g(f(g(k))))). [resolve(3217,a,19,a)]. given #1046 (A,wt=29): 514 b == k | p(g(g(g(g(g(m))))),g(g(g(g(k))))) | g(g(g(g(m)))) == b | p(g(g(g(g(m)))),b). [resolve(285,b,40,a)]. given #1047 (F,wt=13): 3386 g(g(f(f(g(b))))) == g(g(f(f(g(k))))). [resolve(3223,a,20,a)]. given #1048 (F,wt=13): 3387 f(g(f(f(g(b))))) == f(g(f(f(g(k))))). [resolve(3223,a,19,a)]. given #1049 (T,wt=13): 3393 g(f(f(f(g(b))))) == g(f(f(f(g(k))))). [resolve(3224,a,20,a)]. given #1050 (T,wt=13): 3394 f(f(f(f(g(b))))) == f(f(f(f(g(k))))). [resolve(3224,a,19,a)]. given #1051 (A,wt=29): 515 b == k | p(g(g(g(g(k)))),g(g(g(g(g(m)))))) | g(g(g(g(m)))) == b | p(g(g(g(g(m)))),b). [resolve(285,b,39,a)]. given #1052 (F,wt=13): 3403 g(g(g(g(f(b))))) == g(g(g(g(f(k))))). [resolve(3233,a,20,a)]. given #1053 (F,wt=13): 3404 f(g(g(g(f(b))))) == f(g(g(g(f(k))))). [resolve(3233,a,19,a)]. given #1054 (T,wt=13): 3410 g(f(g(g(f(b))))) == g(f(g(g(f(k))))). [resolve(3234,a,20,a)]. given #1055 (T,wt=13): 3411 f(f(g(g(f(b))))) == f(f(g(g(f(k))))). [resolve(3234,a,19,a)]. given #1056 (A,wt=25): 516 b == k | p(g(g(g(g(k)))),g(g(g(m)))) | g(g(g(m))) == b | p(g(g(g(m))),b). [resolve(285,b,38,a)]. given #1057 (F,wt=13): 3420 g(g(f(g(f(b))))) == g(g(f(g(f(k))))). [resolve(3240,a,20,a)]. given #1058 (F,wt=13): 3421 f(g(f(g(f(b))))) == f(g(f(g(f(k))))). [resolve(3240,a,19,a)]. given #1059 (T,wt=13): 3427 g(f(f(g(f(b))))) == g(f(f(g(f(k))))). [resolve(3241,a,20,a)]. given #1060 (T,wt=13): 3428 f(f(f(g(f(b))))) == f(f(f(g(f(k))))). [resolve(3241,a,19,a)]. given #1061 (A,wt=29): 521 b == k | p(g(f(g(g(g(m))))),f(g(g(g(k))))) | f(g(g(g(m)))) == b | p(f(g(g(g(m)))),b). [resolve(286,b,40,a)]. given #1062 (F,wt=13): 3437 g(g(g(f(f(b))))) == g(g(g(f(f(k))))). [resolve(3250,a,20,a)]. given #1063 (F,wt=13): 3438 f(g(g(f(f(b))))) == f(g(g(f(f(k))))). [resolve(3250,a,19,a)]. given #1064 (T,wt=13): 3444 g(f(g(f(f(b))))) == g(f(g(f(f(k))))). [resolve(3251,a,20,a)]. given #1065 (T,wt=13): 3445 f(f(g(f(f(b))))) == f(f(g(f(f(k))))). [resolve(3251,a,19,a)]. given #1066 (A,wt=29): 522 b == k | p(f(g(g(g(k)))),g(f(g(g(g(m)))))) | f(g(g(g(m)))) == b | p(f(g(g(g(m)))),b). [resolve(286,b,39,a)]. given #1067 (F,wt=13): 3454 g(g(f(f(f(b))))) == g(g(f(f(f(k))))). [resolve(3257,a,20,a)]. given #1068 (F,wt=13): 3455 f(g(f(f(f(b))))) == f(g(f(f(f(k))))). [resolve(3257,a,19,a)]. given #1069 (T,wt=13): 3461 g(f(f(f(f(b))))) == g(f(f(f(f(k))))). [resolve(3258,a,20,a)]. given #1070 (T,wt=13): 3462 f(f(f(f(f(b))))) == f(f(f(f(f(k))))). [resolve(3258,a,19,a)]. given #1071 (A,wt=25): 528 b == k | p(f(g(g(m))),g(f(g(g(k))))) | f(g(g(m))) == b | p(f(g(g(m))),b). [resolve(291,b,41,a)]. given #1072 (F,wt=13): 3471 g(g(g(g(g(k))))) == g(g(g(g(g(b))))). [resolve(3267,a,20,a)]. given #1073 (F,wt=13): 3472 f(g(g(g(g(k))))) == f(g(g(g(g(b))))). [resolve(3267,a,19,a)]. given #1074 (T,wt=13): 3478 g(f(g(g(g(k))))) == g(f(g(g(g(b))))). [resolve(3268,a,20,a)]. given #1075 (T,wt=13): 3479 f(f(g(g(g(k))))) == f(f(g(g(g(b))))). [resolve(3268,a,19,a)]. given #1076 (A,wt=29): 529 b == k | p(g(g(f(g(g(m))))),g(f(g(g(k))))) | g(f(g(g(m)))) == b | p(g(f(g(g(m)))),b). [resolve(291,b,40,a)]. given #1077 (F,wt=13): 3488 g(g(f(g(g(k))))) == g(g(f(g(g(b))))). [resolve(3274,a,20,a)]. given #1078 (F,wt=13): 3489 f(g(f(g(g(k))))) == f(g(f(g(g(b))))). [resolve(3274,a,19,a)]. given #1079 (T,wt=13): 3495 g(f(f(g(g(k))))) == g(f(f(g(g(b))))). [resolve(3275,a,20,a)]. given #1080 (T,wt=13): 3496 f(f(f(g(g(k))))) == f(f(f(g(g(b))))). [resolve(3275,a,19,a)]. given #1081 (A,wt=29): 530 b == k | p(g(f(g(g(k)))),g(g(f(g(g(m)))))) | g(f(g(g(m)))) == b | p(g(f(g(g(m)))),b). [resolve(291,b,39,a)]. given #1082 (F,wt=13): 3505 g(g(g(f(g(k))))) == g(g(g(f(g(b))))). [resolve(3284,a,20,a)]. given #1083 (F,wt=13): 3506 f(g(g(f(g(k))))) == f(g(g(f(g(b))))). [resolve(3284,a,19,a)]. given #1084 (T,wt=13): 3512 g(f(g(f(g(k))))) == g(f(g(f(g(b))))). [resolve(3285,a,20,a)]. given #1085 (T,wt=13): 3513 f(f(g(f(g(k))))) == f(f(g(f(g(b))))). [resolve(3285,a,19,a)]. given #1086 (A,wt=25): 531 b == k | p(g(f(g(g(k)))),f(g(g(m)))) | f(g(g(m))) == b | p(f(g(g(m))),b). [resolve(291,b,38,a)]. given #1087 (F,wt=13): 3522 g(g(f(f(g(k))))) == g(g(f(f(g(b))))). [resolve(3291,a,20,a)]. given #1088 (F,wt=13): 3523 f(g(f(f(g(k))))) == f(g(f(f(g(b))))). [resolve(3291,a,19,a)]. given #1089 (T,wt=13): 3529 g(f(f(f(g(k))))) == g(f(f(f(g(b))))). [resolve(3292,a,20,a)]. given #1090 (T,wt=13): 3530 f(f(f(f(g(k))))) == f(f(f(f(g(b))))). [resolve(3292,a,19,a)]. given #1091 (A,wt=29): 536 b == k | p(g(f(f(g(g(m))))),f(f(g(g(k))))) | f(f(g(g(m)))) == b | p(f(f(g(g(m)))),b). [resolve(292,b,40,a)]. given #1092 (F,wt=13): 3539 g(g(g(g(f(k))))) == g(g(g(g(f(b))))). [resolve(3301,a,20,a)]. given #1093 (F,wt=13): 3540 f(g(g(g(f(k))))) == f(g(g(g(f(b))))). [resolve(3301,a,19,a)]. given #1094 (T,wt=13): 3546 g(f(g(g(f(k))))) == g(f(g(g(f(b))))). [resolve(3302,a,20,a)]. given #1095 (T,wt=13): 3547 f(f(g(g(f(k))))) == f(f(g(g(f(b))))). [resolve(3302,a,19,a)]. given #1096 (A,wt=29): 537 b == k | p(f(f(g(g(k)))),g(f(f(g(g(m)))))) | f(f(g(g(m)))) == b | p(f(f(g(g(m)))),b). [resolve(292,b,39,a)]. given #1097 (F,wt=13): 3556 g(g(f(g(f(k))))) == g(g(f(g(f(b))))). [resolve(3308,a,20,a)]. given #1098 (F,wt=13): 3557 f(g(f(g(f(k))))) == f(g(f(g(f(b))))). [resolve(3308,a,19,a)]. given #1099 (T,wt=13): 3563 g(f(f(g(f(k))))) == g(f(f(g(f(b))))). [resolve(3309,a,20,a)]. given #1100 (T,wt=13): 3564 f(f(f(g(f(k))))) == f(f(f(g(f(b))))). [resolve(3309,a,19,a)]. given #1101 (A,wt=25): 542 b == k | p(g(f(g(m))),g(g(f(g(k))))) | g(f(g(m))) == b | p(g(f(g(m))),b). [resolve(299,b,41,a)]. given #1102 (F,wt=13): 3573 g(g(g(f(f(k))))) == g(g(g(f(f(b))))). [resolve(3318,a,20,a)]. given #1103 (F,wt=13): 3574 f(g(g(f(f(k))))) == f(g(g(f(f(b))))). [resolve(3318,a,19,a)]. given #1104 (T,wt=13): 3580 g(f(g(f(f(k))))) == g(f(g(f(f(b))))). [resolve(3319,a,20,a)]. given #1105 (T,wt=13): 3581 f(f(g(f(f(k))))) == f(f(g(f(f(b))))). [resolve(3319,a,19,a)]. given #1106 (A,wt=29): 543 b == k | p(g(g(g(f(g(m))))),g(g(f(g(k))))) | g(g(f(g(m)))) == b | p(g(g(f(g(m)))),b). [resolve(299,b,40,a)]. given #1107 (F,wt=13): 3590 g(g(f(f(f(k))))) == g(g(f(f(f(b))))). [resolve(3325,a,20,a)]. given #1108 (F,wt=13): 3591 f(g(f(f(f(k))))) == f(g(f(f(f(b))))). [resolve(3325,a,19,a)]. given #1109 (T,wt=13): 3597 g(f(f(f(f(k))))) == g(f(f(f(f(b))))). [resolve(3326,a,20,a)]. given #1110 (T,wt=13): 3598 f(f(f(f(f(k))))) == f(f(f(f(f(b))))). [resolve(3326,a,19,a)]. given #1111 (A,wt=29): 544 b == k | p(g(g(f(g(k)))),g(g(g(f(g(m)))))) | g(g(f(g(m)))) == b | p(g(g(f(g(m)))),b). [resolve(299,b,39,a)]. given #1112 (F,wt=14): 3023 b == k | b == f(b) | f(b) == b | p(m,b). [resolve(3016,b,100,b),merge(d)]. given #1113 (F,wt=14): 3027 b == k | k == b | p(m,g(m)) | p(k,f(b)). [resolve(3026,b,724,d),merge(c)]. given #1114 (T,wt=14): 3028 b == k | p(m,g(k)) | k == b | p(k,f(b)). [resolve(3026,b,359,d),merge(d)]. given #1115 (T,wt=14): 3056 g(j) == j | g(j) == k | j == b | p(j,k). [resolve(3055,a,216,d)]. given #1116 (A,wt=25): 545 b == k | p(g(g(f(g(k)))),g(f(g(m)))) | g(f(g(m))) == b | p(g(f(g(m))),b). [resolve(299,b,38,a)]. given #1117 (F,wt=14): 3084 p(g(g(b)),g(k)) | g(b) == b | p(g(b),b). [resolve(3059,a,40,a)]. given #1118 (F,wt=14): 3085 p(g(k),g(g(b))) | g(b) == b | p(g(b),b). [resolve(3059,a,39,a)]. given #1119 (T,wt=14): 3091 p(g(f(b)),f(k)) | f(b) == b | p(f(b),b). [resolve(3060,a,40,a)]. given #1120 (T,wt=14): 3092 p(f(k),g(f(b))) | f(b) == b | p(f(b),b). [resolve(3060,a,39,a)]. given #1121 (A,wt=29): 550 b == k | p(g(f(g(f(g(m))))),f(g(f(g(k))))) | f(g(f(g(m)))) == b | p(f(g(f(g(m)))),b). [resolve(300,b,40,a)]. given #1122 (F,wt=14): 3098 p(g(g(k)),g(b)) | g(k) == b | p(g(k),b). [resolve(3069,a,40,a)]. given #1123 (F,wt=14): 3099 p(g(b),g(g(k))) | g(k) == b | p(g(k),b). [resolve(3069,a,39,a)]. given #1124 (T,wt=14): 3105 p(g(f(k)),f(b)) | f(k) == b | p(f(k),b). [resolve(3070,a,40,a)]. given #1125 (T,wt=14): 3106 p(f(b),g(f(k))) | f(k) == b | p(f(k),b). [resolve(3070,a,39,a)]. given #1126 (A,wt=29): 551 b == k | p(f(g(f(g(k)))),g(f(g(f(g(m)))))) | f(g(f(g(m)))) == b | p(f(g(f(g(m)))),b). [resolve(300,b,39,a)]. given #1127 (F,wt=14): 3123 p(g(b),g(g(k))) | g(b) == b | p(g(b),b). [resolve(3086,a,41,a)]. given #1128 (F,wt=13): 4200 g(b) == b | p(g(b),b) | -(g(g(k)) == b). [factor(4195,b,d)]. given #1129 (T,wt=14): 3126 p(g(g(k)),g(b)) | g(b) == b | p(g(b),b). [resolve(3086,a,38,a)]. given #1130 (T,wt=14): 3140 p(f(b),g(f(k))) | f(b) == b | p(f(b),b). [resolve(3093,a,41,a)]. given #1131 (A,wt=25): 556 b == k | p(f(f(g(m))),g(f(f(g(k))))) | f(f(g(m))) == b | p(f(f(g(m))),b). [resolve(305,b,41,a)]. given #1132 (F,wt=13): 4211 f(b) == b | p(f(b),b) | -(g(f(k)) == b). [factor(4206,b,d)]. given #1133 (F,wt=14): 3143 p(g(f(k)),f(b)) | f(b) == b | p(f(b),b). [resolve(3093,a,38,a)]. given #1134 (T,wt=14): 3157 p(g(k),g(g(b))) | g(k) == b | p(g(k),b). [resolve(3100,a,41,a)]. given #1135 (T,wt=13): 4222 g(k) == b | p(g(k),b) | -(g(g(b)) == b). [factor(4217,b,d)]. given #1136 (A,wt=29): 557 b == k | p(g(g(f(f(g(m))))),g(f(f(g(k))))) | g(f(f(g(m)))) == b | p(g(f(f(g(m)))),b). [resolve(305,b,40,a)]. given #1137 (F,wt=14): 3160 p(g(g(b)),g(k)) | g(k) == b | p(g(k),b). [resolve(3100,a,38,a)]. given #1138 (F,wt=14): 3174 p(f(k),g(f(b))) | f(k) == b | p(f(k),b). [resolve(3107,a,41,a)]. given #1139 (T,wt=13): 4233 f(k) == b | p(f(k),b) | -(g(f(b)) == b). [factor(4228,b,d)]. given #1140 (T,wt=14): 3177 p(g(f(b)),f(k)) | f(k) == b | p(f(k),b). [resolve(3107,a,38,a)]. given #1141 (A,wt=29): 558 b == k | p(g(f(f(g(k)))),g(g(f(f(g(m)))))) | g(f(f(g(m)))) == b | p(g(f(f(g(m)))),b). [resolve(305,b,39,a)]. given #1142 (F,wt=14): 3337 -(x == g(g(g(g(b))))) | x == g(g(g(g(k)))). [resolve(3199,a,16,b)]. given #1143 (F,wt=14): 3338 -(g(g(g(g(k)))) == x) | g(g(g(g(b)))) == x. [resolve(3199,a,16,a)]. given #1144 (T,wt=14): 3344 -(x == f(g(g(g(b))))) | x == f(g(g(g(k)))). [resolve(3200,a,16,b)]. given #1145 (T,wt=14): 3345 -(f(g(g(g(k)))) == x) | f(g(g(g(b)))) == x. [resolve(3200,a,16,a)]. given #1146 (A,wt=25): 559 b == k | p(g(f(f(g(k)))),f(f(g(m)))) | f(f(g(m))) == b | p(f(f(g(m))),b). [resolve(305,b,38,a)]. given #1147 (F,wt=14): 3354 -(x == g(f(g(g(b))))) | x == g(f(g(g(k)))). [resolve(3206,a,16,b)]. given #1148 (F,wt=14): 3355 -(g(f(g(g(k)))) == x) | g(f(g(g(b)))) == x. [resolve(3206,a,16,a)]. given #1149 (T,wt=14): 3361 -(x == f(f(g(g(b))))) | x == f(f(g(g(k)))). [resolve(3207,a,16,b)]. given #1150 (T,wt=14): 3362 -(f(f(g(g(k)))) == x) | f(f(g(g(b)))) == x. [resolve(3207,a,16,a)]. given #1151 (A,wt=29): 564 b == k | p(g(f(f(f(g(m))))),f(f(f(g(k))))) | f(f(f(g(m)))) == b | p(f(f(f(g(m)))),b). [resolve(306,b,40,a)]. given #1152 (F,wt=14): 3371 -(x == g(g(f(g(b))))) | x == g(g(f(g(k)))). [resolve(3216,a,16,b)]. given #1153 (F,wt=14): 3372 -(g(g(f(g(k)))) == x) | g(g(f(g(b)))) == x. [resolve(3216,a,16,a)]. given #1154 (T,wt=14): 3378 -(x == f(g(f(g(b))))) | x == f(g(f(g(k)))). [resolve(3217,a,16,b)]. given #1155 (T,wt=14): 3379 -(f(g(f(g(k)))) == x) | f(g(f(g(b)))) == x. [resolve(3217,a,16,a)]. given #1156 (A,wt=29): 565 b == k | p(f(f(f(g(k)))),g(f(f(f(g(m)))))) | f(f(f(g(m)))) == b | p(f(f(f(g(m)))),b). [resolve(306,b,39,a)]. given #1157 (F,wt=14): 3388 -(x == g(f(f(g(b))))) | x == g(f(f(g(k)))). [resolve(3223,a,16,b)]. given #1158 (F,wt=14): 3389 -(g(f(f(g(k)))) == x) | g(f(f(g(b)))) == x. [resolve(3223,a,16,a)]. given #1159 (T,wt=14): 3395 -(x == f(f(f(g(b))))) | x == f(f(f(g(k)))). [resolve(3224,a,16,b)]. given #1160 (T,wt=14): 3396 -(f(f(f(g(k)))) == x) | f(f(f(g(b)))) == x. [resolve(3224,a,16,a)]. given #1161 (A,wt=25): 570 b == k | p(g(g(f(m))),g(g(g(f(k))))) | g(g(f(m))) == b | p(g(g(f(m))),b). [resolve(313,b,41,a)]. given #1162 (F,wt=14): 3405 -(x == g(g(g(f(b))))) | x == g(g(g(f(k)))). [resolve(3233,a,16,b)]. given #1163 (F,wt=14): 3406 -(g(g(g(f(k)))) == x) | g(g(g(f(b)))) == x. [resolve(3233,a,16,a)]. given #1164 (T,wt=14): 3412 -(x == f(g(g(f(b))))) | x == f(g(g(f(k)))). [resolve(3234,a,16,b)]. given #1165 (T,wt=14): 3413 -(f(g(g(f(k)))) == x) | f(g(g(f(b)))) == x. [resolve(3234,a,16,a)]. given #1166 (A,wt=29): 571 b == k | p(g(g(g(g(f(m))))),g(g(g(f(k))))) | g(g(g(f(m)))) == b | p(g(g(g(f(m)))),b). [resolve(313,b,40,a)]. given #1167 (F,wt=14): 3422 -(x == g(f(g(f(b))))) | x == g(f(g(f(k)))). [resolve(3240,a,16,b)]. given #1168 (F,wt=14): 3423 -(g(f(g(f(k)))) == x) | g(f(g(f(b)))) == x. [resolve(3240,a,16,a)]. given #1169 (T,wt=14): 3429 -(x == f(f(g(f(b))))) | x == f(f(g(f(k)))). [resolve(3241,a,16,b)]. given #1170 (T,wt=14): 3430 -(f(f(g(f(k)))) == x) | f(f(g(f(b)))) == x. [resolve(3241,a,16,a)]. given #1171 (A,wt=29): 572 b == k | p(g(g(g(f(k)))),g(g(g(g(f(m)))))) | g(g(g(f(m)))) == b | p(g(g(g(f(m)))),b). [resolve(313,b,39,a)]. given #1172 (F,wt=14): 3439 -(x == g(g(f(f(b))))) | x == g(g(f(f(k)))). [resolve(3250,a,16,b)]. given #1173 (F,wt=14): 3440 -(g(g(f(f(k)))) == x) | g(g(f(f(b)))) == x. [resolve(3250,a,16,a)]. given #1174 (T,wt=14): 3446 -(x == f(g(f(f(b))))) | x == f(g(f(f(k)))). [resolve(3251,a,16,b)]. given #1175 (T,wt=14): 3447 -(f(g(f(f(k)))) == x) | f(g(f(f(b)))) == x. [resolve(3251,a,16,a)]. given #1176 (A,wt=25): 573 b == k | p(g(g(g(f(k)))),g(g(f(m)))) | g(g(f(m))) == b | p(g(g(f(m))),b). [resolve(313,b,38,a)]. given #1177 (F,wt=14): 3456 -(x == g(f(f(f(b))))) | x == g(f(f(f(k)))). [resolve(3257,a,16,b)]. given #1178 (F,wt=14): 3457 -(g(f(f(f(k)))) == x) | g(f(f(f(b)))) == x. [resolve(3257,a,16,a)]. given #1179 (T,wt=14): 3463 -(x == f(f(f(f(b))))) | x == f(f(f(f(k)))). [resolve(3258,a,16,b)]. given #1180 (T,wt=14): 3464 -(f(f(f(f(k)))) == x) | f(f(f(f(b)))) == x. [resolve(3258,a,16,a)]. given #1181 (A,wt=29): 578 b == k | p(g(f(g(g(f(m))))),f(g(g(f(k))))) | f(g(g(f(m)))) == b | p(f(g(g(f(m)))),b). [resolve(314,b,40,a)]. given #1182 (F,wt=14): 3473 -(x == g(g(g(g(k))))) | x == g(g(g(g(b)))). [resolve(3267,a,16,b)]. given #1183 (F,wt=14): 3474 -(g(g(g(g(b)))) == x) | g(g(g(g(k)))) == x. [resolve(3267,a,16,a)]. given #1184 (T,wt=14): 3480 -(x == f(g(g(g(k))))) | x == f(g(g(g(b)))). [resolve(3268,a,16,b)]. given #1185 (T,wt=14): 3481 -(f(g(g(g(b)))) == x) | f(g(g(g(k)))) == x. [resolve(3268,a,16,a)]. given #1186 (A,wt=29): 579 b == k | p(f(g(g(f(k)))),g(f(g(g(f(m)))))) | f(g(g(f(m)))) == b | p(f(g(g(f(m)))),b). [resolve(314,b,39,a)]. given #1187 (F,wt=14): 3490 -(x == g(f(g(g(k))))) | x == g(f(g(g(b)))). [resolve(3274,a,16,b)]. given #1188 (F,wt=14): 3491 -(g(f(g(g(b)))) == x) | g(f(g(g(k)))) == x. [resolve(3274,a,16,a)]. given #1189 (T,wt=14): 3497 -(x == f(f(g(g(k))))) | x == f(f(g(g(b)))). [resolve(3275,a,16,b)]. given #1190 (T,wt=14): 3498 -(f(f(g(g(b)))) == x) | f(f(g(g(k)))) == x. [resolve(3275,a,16,a)]. given #1191 (A,wt=25): 584 b == k | p(f(g(f(m))),g(f(g(f(k))))) | f(g(f(m))) == b | p(f(g(f(m))),b). [resolve(319,b,41,a)]. given #1192 (F,wt=14): 3507 -(x == g(g(f(g(k))))) | x == g(g(f(g(b)))). [resolve(3284,a,16,b)]. given #1193 (F,wt=14): 3508 -(g(g(f(g(b)))) == x) | g(g(f(g(k)))) == x. [resolve(3284,a,16,a)]. given #1194 (T,wt=14): 3514 -(x == f(g(f(g(k))))) | x == f(g(f(g(b)))). [resolve(3285,a,16,b)]. given #1195 (T,wt=14): 3515 -(f(g(f(g(b)))) == x) | f(g(f(g(k)))) == x. [resolve(3285,a,16,a)]. given #1196 (A,wt=29): 585 b == k | p(g(g(f(g(f(m))))),g(f(g(f(k))))) | g(f(g(f(m)))) == b | p(g(f(g(f(m)))),b). [resolve(319,b,40,a)]. given #1197 (F,wt=14): 3524 -(x == g(f(f(g(k))))) | x == g(f(f(g(b)))). [resolve(3291,a,16,b)]. given #1198 (F,wt=14): 3525 -(g(f(f(g(b)))) == x) | g(f(f(g(k)))) == x. [resolve(3291,a,16,a)]. given #1199 (T,wt=14): 3531 -(x == f(f(f(g(k))))) | x == f(f(f(g(b)))). [resolve(3292,a,16,b)]. given #1200 (T,wt=14): 3532 -(f(f(f(g(b)))) == x) | f(f(f(g(k)))) == x. [resolve(3292,a,16,a)]. given #1201 (A,wt=29): 586 b == k | p(g(f(g(f(k)))),g(g(f(g(f(m)))))) | g(f(g(f(m)))) == b | p(g(f(g(f(m)))),b). [resolve(319,b,39,a)]. given #1202 (F,wt=14): 3541 -(x == g(g(g(f(k))))) | x == g(g(g(f(b)))). [resolve(3301,a,16,b)]. given #1203 (F,wt=14): 3542 -(g(g(g(f(b)))) == x) | g(g(g(f(k)))) == x. [resolve(3301,a,16,a)]. given #1204 (T,wt=14): 3548 -(x == f(g(g(f(k))))) | x == f(g(g(f(b)))). [resolve(3302,a,16,b)]. given #1205 (T,wt=14): 3549 -(f(g(g(f(b)))) == x) | f(g(g(f(k)))) == x. [resolve(3302,a,16,a)]. given #1206 (A,wt=25): 587 b == k | p(g(f(g(f(k)))),f(g(f(m)))) | f(g(f(m))) == b | p(f(g(f(m))),b). [resolve(319,b,38,a)]. given #1207 (F,wt=14): 3558 -(x == g(f(g(f(k))))) | x == g(f(g(f(b)))). [resolve(3308,a,16,b)]. given #1208 (F,wt=14): 3559 -(g(f(g(f(b)))) == x) | g(f(g(f(k)))) == x. [resolve(3308,a,16,a)]. given #1209 (T,wt=14): 3565 -(x == f(f(g(f(k))))) | x == f(f(g(f(b)))). [resolve(3309,a,16,b)]. given #1210 (T,wt=14): 3566 -(f(f(g(f(b)))) == x) | f(f(g(f(k)))) == x. [resolve(3309,a,16,a)]. given #1211 (A,wt=29): 592 b == k | p(g(f(f(g(f(m))))),f(f(g(f(k))))) | f(f(g(f(m)))) == b | p(f(f(g(f(m)))),b). [resolve(320,b,40,a)]. given #1212 (F,wt=14): 3575 -(x == g(g(f(f(k))))) | x == g(g(f(f(b)))). [resolve(3318,a,16,b)]. given #1213 (F,wt=14): 3576 -(g(g(f(f(b)))) == x) | g(g(f(f(k)))) == x. [resolve(3318,a,16,a)]. given #1214 (T,wt=14): 3582 -(x == f(g(f(f(k))))) | x == f(g(f(f(b)))). [resolve(3319,a,16,b)]. given #1215 (T,wt=14): 3583 -(f(g(f(f(b)))) == x) | f(g(f(f(k)))) == x. [resolve(3319,a,16,a)]. given #1216 (A,wt=29): 593 b == k | p(f(f(g(f(k)))),g(f(f(g(f(m)))))) | f(f(g(f(m)))) == b | p(f(f(g(f(m)))),b). [resolve(320,b,39,a)]. given #1217 (F,wt=14): 3592 -(x == g(f(f(f(k))))) | x == g(f(f(f(b)))). [resolve(3325,a,16,b)]. given #1218 (F,wt=14): 3593 -(g(f(f(f(b)))) == x) | g(f(f(f(k)))) == x. [resolve(3325,a,16,a)]. given #1219 (T,wt=14): 3599 -(x == f(f(f(f(k))))) | x == f(f(f(f(b)))). [resolve(3326,a,16,b)]. given #1220 (T,wt=14): 3600 -(f(f(f(f(b)))) == x) | f(f(f(f(k)))) == x. [resolve(3326,a,16,a)]. given #1221 (A,wt=25): 598 b == k | p(g(f(f(m))),g(g(f(f(k))))) | g(f(f(m))) == b | p(g(f(f(m))),b). [resolve(327,b,41,a)]. given #1222 (F,wt=15): 3065 k == j | p(k,m) | j == m | j == k | -p(j,k). [back_unit_del(67),unit_del(b,3064)]. given #1223 (F,wt=15): 3116 b == j | p(b,m) | j == m | j == b | -p(j,b). [resolve(3058,b,1,e),unit_del(b,42)]. given #1224 (T,wt=15): 3120 k == j | p(b,m) | j == m | j == b | -p(j,b). [resolve(3067,b,1,e),unit_del(b,42)]. given #1225 (T,wt=15): 3192 b == j | p(k,m) | j == m | j == k | -p(j,k). [resolve(3189,b,1,e),unit_del(b,3064)]. given #1226 (A,wt=29): 599 b == k | p(g(g(g(f(f(m))))),g(g(f(f(k))))) | g(g(f(f(m)))) == b | p(g(g(f(f(m)))),b). [resolve(327,b,40,a)]. given #1227 (F,wt=15): 3607 g(g(g(g(g(g(b)))))) == g(g(g(g(g(g(k)))))). [resolve(3335,a,20,a)]. given #1228 (F,wt=15): 3608 f(g(g(g(g(g(b)))))) == f(g(g(g(g(g(k)))))). [resolve(3335,a,19,a)]. given #1229 (T,wt=15): 3614 g(f(g(g(g(g(b)))))) == g(f(g(g(g(g(k)))))). [resolve(3336,a,20,a)]. given #1230 (T,wt=15): 3615 f(f(g(g(g(g(b)))))) == f(f(g(g(g(g(k)))))). [resolve(3336,a,19,a)]. given #1231 (A,wt=29): 600 b == k | p(g(g(f(f(k)))),g(g(g(f(f(m)))))) | g(g(f(f(m)))) == b | p(g(g(f(f(m)))),b). [resolve(327,b,39,a)]. given #1232 (F,wt=15): 3624 g(g(f(g(g(g(b)))))) == g(g(f(g(g(g(k)))))). [resolve(3342,a,20,a)]. given #1233 (F,wt=15): 3625 f(g(f(g(g(g(b)))))) == f(g(f(g(g(g(k)))))). [resolve(3342,a,19,a)]. given #1234 (T,wt=15): 3631 g(f(f(g(g(g(b)))))) == g(f(f(g(g(g(k)))))). [resolve(3343,a,20,a)]. given #1235 (T,wt=15): 3632 f(f(f(g(g(g(b)))))) == f(f(f(g(g(g(k)))))). [resolve(3343,a,19,a)]. given #1236 (A,wt=25): 601 b == k | p(g(g(f(f(k)))),g(f(f(m)))) | g(f(f(m))) == b | p(g(f(f(m))),b). [resolve(327,b,38,a)]. given #1237 (F,wt=15): 3641 g(g(g(f(g(g(b)))))) == g(g(g(f(g(g(k)))))). [resolve(3352,a,20,a)]. given #1238 (F,wt=15): 3642 f(g(g(f(g(g(b)))))) == f(g(g(f(g(g(k)))))). [resolve(3352,a,19,a)]. given