============================== Prover9 =============================== Prover9 (32) version 22-May-2007, May 2007. Process 27610 was started by mccune on cleo, Tue May 22 14:49:14 2007 The command was "/home/mccune/bin/prover9 -f wang.in wang3.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 wang3.in assign(max_seconds,120). formulas(sos). -(m == b). 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]. 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: Predicate symbol precedence: predicate_order([ ==, p ]). Function symbol precedence: function_order([ 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 x == j | -p(x,j) | x == k. [assumption]. 23 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=9): 22 x == j | -p(x,j) | x == k. [assumption]. given #23 (I,wt=9): 23 x == j | p(x,j) | -(x == k). [assumption]. given #24 (A,wt=22): 24 x == b | p(x,b) | g(x) == b | -p(g(x),b) | x == g(x) | -p(g(x),x). [resolve(10,c,2,f),merge(e)]. given #25 (F,wt=3): 41 -(b == m). [ur(15,b,21,a)]. given #26 (T,wt=6): 35 b == k | p(b,k). [resolve(14,a,13,b)]. given #27 (T,wt=6): 36 m == k | p(m,k). [resolve(14,a,12,b)]. given #28 (T,wt=6): 43 k == j | p(k,j). [resolve(23,c,14,a)]. given #29 (T,wt=9): 45 b == k | -(k == x) | p(b,x). [resolve(35,b,18,b)]. given #30 (A,wt=25): 25 x == b | p(x,b) | g(x) == m | p(g(x),m) | x == m | x == g(x) | -p(g(x),x). [resolve(10,c,1,f)]. given #31 (T,wt=9): 46 b == k | -(b == x) | p(x,k). [resolve(35,b,17,b)]. given #32 (T,wt=9): 49 m == k | -(k == x) | p(m,x). [resolve(36,b,18,b)]. given #33 (T,wt=9): 50 m == k | -(m == x) | p(x,k). [resolve(36,b,17,b)]. given #34 (T,wt=9): 53 k == j | -(j == x) | p(k,x). [resolve(43,b,18,b)]. given #35 (A,wt=24): 26 x == b | p(x,b) | x == m | p(x,m) | g(x) == m | g(x) == x | -p(g(x),x). [resolve(10,c,1,e)]. given #36 (T,wt=9): 54 k == j | -(k == x) | p(x,j). [resolve(43,b,17,b)]. given #37 (T,wt=12): 30 p(m,b) | g(m) == m | -(f(g(m)) == m). [resolve(11,c,4,b),unit_del(a,21)]. given #38 (T,wt=12): 47 b == k | k == m | p(k,m) | -p(k,b). [resolve(35,b,1,f),merge(e),unit_del(d,41)]. given #39 (T,wt=12): 51 m == k | k == b | -p(k,b) | -p(k,m). [resolve(36,b,2,f),merge(e),unit_del(d,21)]. given #40 (A,wt=13): 27 p(m,b) | g(m) == m | p(f(g(m)),g(m)). [resolve(11,c,7,b),unit_del(a,21)]. given #41 (T,wt=13): 28 p(m,b) | g(m) == m | p(g(m),f(g(m))). [resolve(11,c,6,b),unit_del(a,21)]. given #42 (T,wt=13): 29 p(m,b) | g(m) == m | -(f(g(m)) == g(m)). [resolve(11,c,5,b),unit_del(a,21)]. given #43 (T,wt=13): 37 -(g(x) == y) | p(y,x) | x == b | p(x,b). [resolve(17,b,11,c)]. given #44 (T,wt=13): 38 -(x == y) | p(y,g(x)) | x == b | p(x,b). [resolve(17,b,10,c)]. given #45 (A,wt=18): 31 k == b | p(k,b) | g(k) == k | g(k) == m | g(k) == b. [resolve(11,c,3,d)]. given #46 (T,wt=13): 39 -(x == y) | p(g(x),y) | x == b | p(x,b). [resolve(18,b,11,c)]. given #47 (T,wt=13): 40 -(g(x) == y) | p(x,y) | x == b | p(x,b). [resolve(18,b,10,c)]. given #48 (T,wt=14): 42 g(j) == j | g(j) == k | j == b | p(j,b). [resolve(22,b,11,c)]. given #49 (T,wt=15): 48 b == k | p(b,m) | k == m | k == b | -p(k,b). [resolve(35,b,1,e),unit_del(b,41)]. given #50 (A,wt=18): 44 x == b | p(x,b) | g(x) == b | -p(g(x),b) | x == g(x). [resolve(24,f,11,c),merge(f),merge(g)]. given #51 (T,wt=15): 52 m == k | -p(m,b) | k == b | k == m | -p(k,m). [resolve(36,b,2,e),unit_del(b,21)]. given #52 (T,wt=15): 55 k == j | j == b | -p(j,b) | k == b | -p(j,k). [resolve(43,b,2,f),merge(e)]. given #53 (T,wt=15): 57 k == j | j == m | p(j,m) | k == m | -p(j,k). [resolve(43,b,1,f),merge(e)]. given #54 (T,wt=16): 61 p(m,b) | g(m) == m | -(g(m) == x) | p(f(g(m)),x). [resolve(27,c,18,b)]. given #55 (A,wt=18): 56 k == j | k == b | -p(k,b) | j == b | j == k | -p(j,k). [resolve(43,b,2,e)]. given #56 (T,wt=16): 62 p(m,b) | g(m) == m | -(f(g(m)) == x) | p(x,g(m)). [resolve(27,c,17,b)]. given #57 (T,wt=16): 67 p(m,b) | g(m) == m | -(f(g(m)) == x) | p(g(m),x). [resolve(28,c,18,b)]. given #58 (T,wt=16): 68 p(m,b) | g(m) == m | -(g(m) == x) | p(x,f(g(m))). [resolve(28,c,17,b)]. given #59 (T,wt=17): 78 g(j) == j | g(j) == k | j == b | -(b == x) | p(j,x). [resolve(42,d,18,b)]. given #60 (A,wt=18): 58 k == j | k == m | p(k,m) | j == m | j == k | -p(j,k). [resolve(43,b,1,e)]. given #61 (T,wt=17): 79 g(j) == j | g(j) == k | j == b | -(j == x) | p(x,b). [resolve(42,d,17,b)]. given #62 (T,wt=20): 60 x == b | p(x,b) | x == m | p(x,m) | g(x) == m | g(x) == x. [resolve(26,g,11,c),merge(g),merge(h)]. given #63 (T,wt=20): 81 g(j) == j | g(j) == k | j == b | p(b,m) | j == m | -p(b,j). [resolve(42,d,1,f),merge(g),unit_del(d,41)]. given #64 (T,wt=21): 59 x == b | p(x,b) | g(x) == m | p(g(x),m) | x == m | x == g(x). [resolve(25,g,11,c),merge(g),merge(h)]. given #65 (A,wt=32): 63 p(m,b) | g(m) == m | g(m) == b | -p(g(m),b) | f(g(m)) == b | f(g(m)) == g(m) | -p(g(m),f(g(m))). [resolve(27,c,2,f)]. given #66 (T,wt=21): 74 k == b | g(k) == k | g(k) == m | g(k) == b | -(b == x) | p(k,x). [resolve(31,b,18,b)]. given #67 (T,wt=21): 75 k == b | g(k) == k | g(k) == m | g(k) == b | -(k == x) | p(x,b). [resolve(31,b,17,b)]. given #68 (T,wt=21): 87 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | p(f(x),x). [resolve(60,d,7,b),merge(f)]. given #69 (T,wt=21): 88 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | p(x,f(x)). [resolve(60,d,6,b),merge(f)]. given #70 (A,wt=33): 64 p(m,b) | g(m) == m | f(g(m)) == b | -p(f(g(m)),b) | g(m) == b | g(m) == f(g(m)) | -p(g(m),f(g(m))). [resolve(27,c,2,e)]. given #71 (T,wt=21): 89 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == x). [resolve(60,d,5,b),merge(f)]. given #72 (T,wt=21): 90 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == m). [resolve(60,d,4,b),merge(f)]. given #73 (T,wt=21): 110 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == b). [factor(106,b,g)]. given #74 (T,wt=22): 97 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == m). [resolve(59,d,4,b),merge(f)]. given #75 (A,wt=28): 65 p(m,b) | g(m) == m | p(g(m),m) | f(g(m)) == m | f(g(m)) == g(m) | -p(g(m),f(g(m))). [resolve(27,c,1,f),merge(c)]. given #76 (T,wt=22): 111 p(m,b) | g(m) == m | p(g(m),m) | f(g(m)) == m | f(g(m)) == g(m). [resolve(65,f,28,c),merge(f),merge(g)]. given #77 (T,wt=23): 80 g(j) == j | g(j) == k | j == b | x == b | x == j | -p(j,x) | -p(x,j). [resolve(42,d,2,b),merge(d)]. given #78 (T,wt=20): 115 g(j) == j | g(j) == k | j == b | k == b | k == j | -p(j,k). [resolve(80,g,43,b),merge(g)]. given #79 (T,wt=23): 82 g(j) == j | g(j) == k | j == b | j == m | p(j,m) | b == j | -p(b,j). [resolve(42,d,1,e),unit_del(f,41)]. given #80 (A,wt=29): 66 p(m,b) | g(m) == m | f(g(m)) == m | p(f(g(m)),m) | g(m) == f(g(m)) | -p(g(m),f(g(m))). [resolve(27,c,1,e),merge(e)]. given #81 (T,wt=23): 84 k == b | p(k,b) | k == m | g(k) == m | g(k) == k | m == k | -p(m,b). [resolve(60,d,52,e),merge(h),merge(i)]. given #82 (T,wt=23): 85 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(m == y) | p(x,y). [resolve(60,d,18,b)]. given #83 (T,wt=23): 86 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(x == y) | p(y,m). [resolve(60,d,17,b)]. given #84 (T,wt=23): 91 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -p(m,b) | -p(m,x). [resolve(60,d,2,f),merge(h),merge(i),unit_del(f,21)]. given #85 (A,wt=33): 69 p(m,b) | g(m) == m | f(g(m)) == b | -p(f(g(m)),b) | g(m) == b | g(m) == f(g(m)) | -p(f(g(m)),g(m)). [resolve(28,c,2,f)]. given #86 (T,wt=23): 94 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | p(f(g(x)),g(x)). [resolve(59,d,7,b),merge(f)]. given #87 (T,wt=23): 95 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | p(g(x),f(g(x))). [resolve(59,d,6,b),merge(f)]. given #88 (T,wt=23): 96 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == g(x)). [resolve(59,d,5,b),merge(f)]. given #89 (T,wt=23): 117 p(m,b) | g(m) == m | f(g(m)) == m | p(f(g(m)),m) | g(m) == f(g(m)). [resolve(66,f,28,c),merge(f),merge(g)]. given #90 (A,wt=24): 73 k == b | g(k) == k | g(k) == m | g(k) == b | b == k | k == m | p(k,m). [resolve(31,b,47,d)]. given #91 (T,wt=24): 77 k == b | g(k) == k | g(k) == m | g(k) == b | p(b,m) | k == m | -p(b,k). [resolve(31,b,1,f),merge(h),unit_del(e,41)]. given #92 (T,wt=24): 83 b == k | p(b,m) | k == m | k == b | g(k) == k | g(k) == m | g(k) == b. [resolve(48,e,31,b),merge(e)]. given #93 (T,wt=24): 92 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(m == y) | p(g(x),y). [resolve(59,d,18,b)]. given #94 (T,wt=24): 93 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(g(x) == y) | p(y,m). [resolve(59,d,17,b)]. given #95 (A,wt=27): 76 k == b | g(k) == k | g(k) == m | g(k) == b | x == b | x == k | -p(k,x) | -p(x,k). [resolve(31,b,2,b),merge(e)]. given #96 (T,wt=21): 152 k == b | g(k) == k | g(k) == m | g(k) == b | m == k | -p(k,m). [resolve(76,h,36,b),merge(h),unit_del(e,21)]. given #97 (T,wt=24): 101 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(x == y) | p(f(x),y). [resolve(87,f,18,b)]. given #98 (T,wt=24): 102 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == y) | p(y,x). [resolve(87,f,17,b)]. given #99 (T,wt=24): 106 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(f(x) == y) | p(x,y). [resolve(88,f,18,b)]. given #100 (A,wt=28): 98 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -p(m,b) | g(x) == b | -p(m,g(x)). [resolve(59,d,2,f),merge(i),unit_del(f,21)]. given #101 (T,wt=24): 107 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | -(x == y) | p(y,f(x)). [resolve(88,f,17,b)]. given #102 (T,wt=24): 133 p(m,b) | g(m) == m | f(g(m)) == m | g(m) == f(g(m)) | -(f(f(g(m))) == m). [resolve(117,d,4,b),merge(e)]. given #103 (T,wt=24): 153 k == b | g(k) == k | g(k) == m | g(k) == b | m == k | b == k | k == m. [resolve(152,f,73,g),merge(f),merge(g),merge(h),merge(i)]. given #104 (T,wt=23): 167 k == b | g(k) == m | g(k) == b | m == k | b == k | k == m | p(k,b). [resolve(153,b,9,c),merge(g)]. given #105 (A,wt=26): 99 p(m,b) | g(m) == m | g(m) == b | -p(g(m),b) | f(g(m)) == b | f(g(m)) == g(m). [resolve(63,g,28,c),merge(g),merge(h)]. given #106 (T,wt=23): 168 k == b | g(k) == m | g(k) == b | m == k | b == k | k == m | p(b,m). [resolve(167,g,48,e),merge(g),merge(i),merge(j)]. given #107 (T,wt=23): 169 k == b | g(k) == m | g(k) == b | m == k | b == k | k == m | p(k,m). [resolve(167,g,47,d),merge(g),merge(h)]. given #108 (T,wt=23): 180 k == b | g(k) == m | g(k) == b | m == k | b == k | k == m | -p(m,b). [resolve(169,g,52,e),merge(g),merge(i),merge(j)]. given #109 (T,wt=23): 181 k == b | g(k) == m | g(k) == b | m == k | b == k | k == m | -p(k,b). [resolve(169,g,51,d),merge(g),merge(h)]. given #110 (A,wt=25): 100 j == b | p(j,b) | j == m | g(j) == m | g(j) == j | f(j) == j | f(j) == k. [resolve(87,f,22,b)]. given #111 (T,wt=20): 188 k == b | g(k) == m | g(k) == b | m == k | b == k | k == m. [resolve(181,g,167,g),merge(g),merge(h),merge(i),merge(j),merge(k),merge(l)]. given #112 (T,wt=20): 202 k == b | g(k) == b | m == k | b == k | k == m | m == g(k). [resolve(188,b,15,a)]. given #113 (T,wt=19): 206 k == b | m == k | b == k | k == m | m == g(k) | p(k,b). [resolve(202,b,40,a),merge(g),merge(h)]. given #114 (T,wt=19): 214 k == b | m == k | b == k | k == m | m == g(k) | p(b,m). [resolve(206,f,48,e),merge(f),merge(h),merge(i)]. given #115 (A,wt=29): 103 k == b | p(k,b) | k == m | g(k) == m | g(k) == k | f(k) == k | f(k) == m | f(k) == b. [resolve(87,f,3,d)]. given #116 (T,wt=19): 215 k == b | m == k | b == k | k == m | m == g(k) | p(k,m). [resolve(206,f,47,d),merge(f),merge(g)]. given #117 (T,wt=19): 232 k == b | m == k | b == k | k == m | m == g(k) | -p(m,b). [resolve(215,f,52,e),merge(f),merge(h),merge(i)]. given #118 (T,wt=19): 233 k == b | m == k | b == k | k == m | m == g(k) | -p(k,b). [resolve(215,f,51,d),merge(f),merge(g)]. given #119 (T,wt=16): 240 k == b | m == k | b == k | k == m | m == g(k). [resolve(233,f,206,f),merge(f),merge(g),merge(h),merge(i),merge(j)]. given #120 (A,wt=33): 104 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | f(x) == b | -p(f(x),b) | x == f(x) | -p(x,f(x)). [resolve(87,f,2,e),merge(h)]. given #121 (T,wt=13): 251 k == b | m == k | b == k | m == g(k). [resolve(240,d,15,a),merge(e)]. given #122 (T,wt=10): 259 m == k | b == k | m == g(k). [resolve(251,a,15,a),merge(d)]. given #123 (T,wt=10): 262 m == k | b == k | p(g(k),k). [resolve(259,c,50,b),merge(c)]. given #124 (T,wt=10): 269 m == k | b == k | g(k) == m. [resolve(259,c,15,a)]. given #125 (A,wt=33): 105 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | f(x) == m | p(f(x),m) | x == f(x) | -p(x,f(x)). [resolve(87,f,1,e),merge(h)]. given #126 (T,wt=10): 270 m == k | b == k | -(g(k) == k). [factor(268,a,d)]. given #127 (T,wt=12): 265 m == k | b == k | g(m) == g(g(k)). [resolve(259,c,20,a)]. given #128 (T,wt=12): 266 m == k | b == k | f(m) == f(g(k)). [resolve(259,c,19,a)]. given #129 (T,wt=12): 278 m == k | b == k | g(g(k)) == g(m). [resolve(269,c,20,a)]. given #130 (A,wt=33): 108 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | f(x) == b | -p(f(x),b) | x == f(x) | -p(f(x),x). [resolve(88,f,2,f),merge(h)]. given #131 (T,wt=12): 279 m == k | b == k | f(g(k)) == f(m). [resolve(269,c,19,a)]. given #132 (T,wt=13): 267 m == k | b == k | -(x == m) | x == g(k). [resolve(259,c,16,b)]. given #133 (T,wt=13): 268 m == k | b == k | -(g(k) == x) | m == x. [resolve(259,c,16,a)]. given #134 (T,wt=13): 271 m == k | b == k | -(k == x) | p(g(k),x). [resolve(262,c,18,b)]. given #135 (A,wt=25): 112 p(m,b) | g(m) == m | f(g(m)) == m | f(g(m)) == g(m) | -(m == x) | p(g(m),x). [resolve(111,c,18,b)]. given #136 (T,wt=13): 272 m == k | b == k | -(g(k) == x) | p(x,k). [resolve(262,c,17,b)]. given #137 (T,wt=13): 280 m == k | b == k | -(x == g(k)) | x == m. [resolve(269,c,16,b)]. given #138 (T,wt=13): 281 m == k | b == k | -(m == x) | g(k) == x. [resolve(269,c,16,a)]. given #139 (T,wt=14): 263 m == k | b == k | p(g(m),g(k)) | p(m,b). [resolve(259,c,39,a),unit_del(d,21)]. given #140 (A,wt=25): 113 p(m,b) | g(m) == m | f(g(m)) == m | f(g(m)) == g(m) | -(g(m) == x) | p(x,m). [resolve(111,c,17,b)]. given #141 (T,wt=14): 264 m == k | b == k | p(g(k),g(m)) | p(m,b). [resolve(259,c,38,a),unit_del(d,21)]. given #142 (T,wt=14): 289 m == k | b == k | p(m,g(g(k))) | p(m,b). [resolve(265,c,40,a),unit_del(d,21)]. given #143 (T,wt=14): 292 m == k | b == k | p(g(g(k)),m) | p(m,b). [resolve(265,c,37,a),unit_del(d,21)]. given #144 (T,wt=14): 293 m == k | b == k | g(g(m)) == g(g(g(k))). [resolve(265,c,20,a)]. given #145 (A,wt=34): 114 p(m,b) | g(m) == m | f(g(m)) == m | f(g(m)) == g(m) | g(m) == b | -p(g(m),b) | m == g(m) | -p(m,g(m)). [resolve(111,c,2,e),unit_del(g,21)]. given #146 (T,wt=14): 294 m == k | b == k | f(g(m)) == f(g(g(k))). [resolve(265,c,19,a)]. given #147 (T,wt=14): 302 m == k | b == k | g(f(m)) == g(f(g(k))). [resolve(266,c,20,a)]. given #148 (T,wt=14): 303 m == k | b == k | f(f(m)) == f(f(g(k))). [resolve(266,c,19,a)]. given #149 (T,wt=14): 313 m == k | b == k | g(g(g(k))) == g(g(m)). [resolve(278,c,20,a)]. given #150 (A,wt=27): 119 p(m,b) | g(m) == m | f(g(m)) == b | -p(f(g(m)),b) | g(m) == b | g(m) == f(g(m)). [resolve(69,g,27,c),merge(g),merge(h)]. given #151 (T,wt=14): 314 m == k | b == k | f(g(g(k))) == f(g(m)). [resolve(278,c,19,a)]. given #152 (T,wt=14): 324 m == k | b == k | g(f(g(k))) == g(f(m)). [resolve(279,c,20,a)]. given #153 (T,wt=14): 325 m == k | b == k | f(f(g(k))) == f(f(m)). [resolve(279,c,19,a)]. given #154 (T,wt=14): 339 m == k | b == k | p(m,b) | -(g(g(k)) == b). [factor(336,c,e)]. given #155 (A,wt=26): 120 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(g(x) == y) | p(f(g(x)),y). [resolve(94,f,18,b)]. given #156 (T,wt=15): 275 m == k | b == k | p(k,m) | k == b | p(k,b). [resolve(269,c,40,a)]. given #157 (T,wt=15): 295 m == k | b == k | -(x == g(m)) | x == g(g(k)). [resolve(265,c,16,b)]. given #158 (T,wt=15): 296 m == k | b == k | -(g(g(k)) == x) | g(m) == x. [resolve(265,c,16,a)]. given #159 (T,wt=15): 304 m == k | b == k | -(x == f(m)) | x == f(g(k)). [resolve(266,c,16,b)]. given #160 (A,wt=26): 121 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == y) | p(y,g(x)). [resolve(94,f,17,b)]. given #161 (T,wt=15): 305 m == k | b == k | -(f(g(k)) == x) | f(m) == x. [resolve(266,c,16,a)]. given #162 (T,wt=15): 315 m == k | b == k | -(x == g(g(k))) | x == g(m). [resolve(278,c,16,b)]. given #163 (T,wt=15): 316 m == k | b == k | -(g(m) == x) | g(g(k)) == x. [resolve(278,c,16,a)]. given #164 (T,wt=15): 326 m == k | b == k | -(x == f(g(k))) | x == f(m). [resolve(279,c,16,b)]. given #165 (A,wt=43): 122 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | f(g(x)) == b | -p(f(g(x)),b) | g(x) == b | g(x) == f(g(x)) | -p(g(x),f(g(x))). [resolve(94,f,2,e)]. given #166 (T,wt=15): 327 m == k | b == k | -(f(m) == x) | f(g(k)) == x. [resolve(279,c,16,a)]. given #167 (T,wt=16): 355 m == k | b == k | g(g(g(m))) == g(g(g(g(k)))). [resolve(293,c,20,a)]. given #168 (T,wt=16): 356 m == k | b == k | f(g(g(m))) == f(g(g(g(k)))). [resolve(293,c,19,a)]. given #169 (T,wt=16): 368 m == k | b == k | g(f(g(m))) == g(f(g(g(k)))). [resolve(294,c,20,a)]. given #170 (A,wt=39): 123 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | f(g(x)) == m | p(f(g(x)),m) | g(x) == f(g(x)) | -p(g(x),f(g(x))). [resolve(94,f,1,e),merge(h)]. given #171 (T,wt=16): 369 m == k | b == k | f(f(g(m))) == f(f(g(g(k)))). [resolve(294,c,19,a)]. given #172 (T,wt=16): 380 m == k | b == k | g(g(f(m))) == g(g(f(g(k)))). [resolve(302,c,20,a)]. given #173 (T,wt=16): 381 m == k | b == k | f(g(f(m))) == f(g(f(g(k)))). [resolve(302,c,19,a)]. given #174 (T,wt=16): 391 m == k | b == k | g(f(f(m))) == g(f(f(g(k)))). [resolve(303,c,20,a)]. given #175 (A,wt=26): 124 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(f(g(x)) == y) | p(g(x),y). [resolve(95,f,18,b)]. given #176 (T,wt=16): 392 m == k | b == k | f(f(f(m))) == f(f(f(g(k)))). [resolve(303,c,19,a)]. given #177 (T,wt=16): 403 m == k | b == k | g(g(g(g(k)))) == g(g(g(m))). [resolve(313,c,20,a)]. given #178 (T,wt=16): 404 m == k | b == k | f(g(g(g(k)))) == f(g(g(m))). [resolve(313,c,19,a)]. given #179 (T,wt=16): 414 m == k | b == k | g(f(g(g(k)))) == g(f(g(m))). [resolve(314,c,20,a)]. given #180 (A,wt=26): 125 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | -(g(x) == y) | p(y,f(g(x))). [resolve(95,f,17,b)]. given #181 (T,wt=16): 415 m == k | b == k | f(f(g(g(k)))) == f(f(g(m))). [resolve(314,c,19,a)]. given #182 (T,wt=16): 426 m == k | b == k | g(g(f(g(k)))) == g(g(f(m))). [resolve(324,c,20,a)]. given #183 (T,wt=16): 427 m == k | b == k | f(g(f(g(k)))) == f(g(f(m))). [resolve(324,c,19,a)]. given #184 (T,wt=16): 437 m == k | b == k | g(f(f(g(k)))) == g(f(f(m))). [resolve(325,c,20,a)]. given #185 (A,wt=43): 126 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | f(g(x)) == b | -p(f(g(x)),b) | g(x) == b | g(x) == f(g(x)) | -p(f(g(x)),g(x)). [resolve(95,f,2,f)]. given #186 (T,wt=16): 438 m == k | b == k | f(f(f(g(k)))) == f(f(f(m))). [resolve(325,c,19,a)]. given #187 (T,wt=17): 328 m == k | b == k | p(m,b) | -(g(k) == x) | p(g(m),x). [resolve(263,c,18,b)]. given #188 (T,wt=13): 666 m == k | b == k | p(m,b) | p(g(m),m). [resolve(328,d,269,c),merge(e),merge(f)]. given #189 (T,wt=16): 667 m == k | b == k | p(m,b) | -(m == x) | p(g(m),x). [resolve(666,d,18,b)]. given #190 (A,wt=26): 128 p(m,b) | g(m) == m | f(g(m)) == m | g(m) == f(g(m)) | -(m == x) | p(f(g(m)),x). [resolve(117,d,18,b)]. given #191 (T,wt=16): 668 m == k | b == k | p(m,b) | -(g(m) == x) | p(x,m). [resolve(666,d,17,b)]. given #192 (T,wt=17): 329 m == k | b == k | p(m,b) | -(g(m) == x) | p(x,g(k)). [resolve(263,c,17,b)]. given #193 (T,wt=15): 671 m == k | b == k | p(m,b) | p(g(g(k)),g(k)). [resolve(329,d,265,c),merge(e),merge(f)]. given #194 (T,wt=17): 332 m == k | b == k | p(m,b) | -(g(m) == x) | p(g(k),x). [resolve(264,c,18,b)]. given #195 (A,wt=26): 129 p(m,b) | g(m) == m | f(g(m)) == m | g(m) == f(g(m)) | -(f(g(m)) == x) | p(x,m). [resolve(117,d,17,b)]. given #196 (T,wt=15): 676 m == k | b == k | p(m,b) | p(g(k),g(g(k))). [resolve(332,d,265,c),merge(e),merge(f)]. given #197 (T,wt=17): 333 m == k | b == k | p(m,b) | -(g(k) == x) | p(x,g(m)). [resolve(264,c,17,b)]. given #198 (T,wt=13): 682 m == k | b == k | p(m,b) | p(m,g(m)). [resolve(333,d,269,c),merge(e),merge(f)]. given #199 (T,wt=13): 686 m == k | b == k | p(m,b) | -(g(m) == b). [factor(683,c,e)]. given #200 (A,wt=26): 130 p(m,b) | g(m) == m | f(g(m)) == m | g(m) == f(g(m)) | p(f(f(g(m))),f(g(m))). [resolve(117,d,7,b),merge(e)]. given #201 (T,wt=16): 683 m == k | b == k | p(m,b) | -(g(m) == x) | p(m,x). [resolve(682,d,18,b)]. given #202 (T,wt=16): 684 m == k | b == k | p(m,b) | -(m == x) | p(x,g(m)). [resolve(682,d,17,b)]. given #203 (T,wt=17): 336 m == k | b == k | p(m,b) | -(g(g(k)) == x) | p(m,x). [resolve(289,c,18,b)]. given #204 (T,wt=17): 337 m == k | b == k | p(m,b) | -(m == x) | p(x,g(g(k))). [resolve(289,c,17,b)]. given #205 (A,wt=26): 131 p(m,b) | g(m) == m | f(g(m)) == m | g(m) == f(g(m)) | p(f(g(m)),f(f(g(m)))). [resolve(117,d,6,b),merge(e)]. given #206 (T,wt=17): 340 m == k | b == k | p(m,b) | -(m == x) | p(g(g(k)),x). [resolve(292,c,18,b)]. given #207 (T,wt=17): 341 m == k | b == k | p(m,b) | -(g(g(k)) == x) | p(x,m). [resolve(292,c,17,b)]. given #208 (T,wt=17): 357 m == k | b == k | -(x == g(g(m))) | x == g(g(g(k))). [resolve(293,c,16,b)]. given #209 (T,wt=17): 358 m == k | b == k | -(g(g(g(k))) == x) | g(g(m)) == x. [resolve(293,c,16,a)]. given #210 (A,wt=26): 132 p(m,b) | g(m) == m | f(g(m)) == m | g(m) == f(g(m)) | -(f(f(g(m))) == f(g(m))). [resolve(117,d,5,b),merge(e)]. given #211 (T,wt=17): 370 m == k | b == k | -(x == f(g(m))) | x == f(g(g(k))). [resolve(294,c,16,b)]. given #212 (T,wt=17): 371 m == k | b == k | -(f(g(g(k))) == x) | f(g(m)) == x. [resolve(294,c,16,a)]. given #213 (T,wt=17): 382 m == k | b == k | -(x == g(f(m))) | x == g(f(g(k))). [resolve(302,c,16,b)]. given #214 (T,wt=17): 383 m == k | b == k | -(g(f(g(k))) == x) | g(f(m)) == x. [resolve(302,c,16,a)]. given #215 (A,wt=38): 134 p(m,b) | g(m) == m | f(g(m)) == m | g(m) == f(g(m)) | f(g(m)) == b | -p(f(g(m)),b) | m == f(g(m)) | -p(m,f(g(m))). [resolve(117,d,2,e),unit_del(g,21)]. given #216 (T,wt=17): 393 m == k | b == k | -(x == f(f(m))) | x == f(f(g(k))). [resolve(303,c,16,b)]. given #217 (T,wt=17): 394 m == k | b == k | -(f(f(g(k))) == x) | f(f(m)) == x. [resolve(303,c,16,a)]. given #218 (T,wt=17): 405 m == k | b == k | -(x == g(g(g(k)))) | x == g(g(m)). [resolve(313,c,16,b)]. given #219 (T,wt=17): 406 m == k | b == k | -(g(g(m)) == x) | g(g(g(k))) == x. [resolve(313,c,16,a)]. given #220 (A,wt=27): 137 k == b | g(k) == k | g(k) == m | g(k) == b | b == k | k == m | -(m == x) | p(k,x). [resolve(73,g,18,b)]. given #221 (T,wt=17): 416 m == k | b == k | -(x == f(g(g(k)))) | x == f(g(m)). [resolve(314,c,16,b)]. given #222 (T,wt=17): 417 m == k | b == k | -(f(g(m)) == x) | f(g(g(k))) == x. [resolve(314,c,16,a)]. given #223 (T,wt=17): 428 m == k | b == k | -(x == g(f(g(k)))) | x == g(f(m)). [resolve(324,c,16,b)]. given #224 (T,wt=17): 429 m == k | b == k | -(g(f(m)) == x) | g(f(g(k))) == x. [resolve(324,c,16,a)]. given #225 (A,wt=27): 138 k == b | g(k) == k | g(k) == m | g(k) == b | b == k | k == m | -(k == x) | p(x,m). [resolve(73,g,17,b)]. given #226 (T,wt=17): 439 m == k | b == k | -(x == f(f(g(k)))) | x == f(f(m)). [resolve(325,c,16,b)]. given #227 (T,wt=17): 440 m == k | b == k | -(f(f(m)) == x) | f(f(g(k))) == x. [resolve(325,c,16,a)]. given #228 (T,wt=18): 445 m == k | b == k | k == b | p(k,b) | -p(m,b) | k == m. [resolve(275,c,52,e),merge(e),merge(g)]. given #229 (T,wt=18): 446 m == k | b == k | k == b | p(k,b) | -(m == x) | p(k,x). [resolve(275,c,18,b)]. given #230 (A,wt=25): 139 k == b | g(k) == k | g(k) == m | g(k) == b | b == k | k == m | p(f(k),k). [resolve(73,g,7,b),merge(g)]. given #231 (T,wt=18): 447 m == k | b == k | k == b | p(k,b) | -(k == x) | p(x,m). [resolve(275,c,17,b)]. given #232 (T,wt=18): 461 m == k | b == k | g(g(g(g(m)))) == g(g(g(g(g(k))))). [resolve(355,c,20,a)]. given #233 (T,wt=18): 462 m == k | b == k | f(g(g(g(m)))) == f(g(g(g(g(k))))). [resolve(355,c,19,a)]. given #234 (T,wt=18): 473 m == k | b == k | g(f(g(g(m)))) == g(f(g(g(g(k))))). [resolve(356,c,20,a)]. given #235 (A,wt=25): 140 k == b | g(k) == k | g(k) == m | g(k) == b | b == k | k == m | p(k,f(k)). [resolve(73,g,6,b),merge(g)]. given #236 (T,wt=18): 474 m == k | b == k | f(f(g(g(m)))) == f(f(g(g(g(k))))). [resolve(356,c,19,a)]. given #237 (T,wt=18): 486 m == k | b == k | g(g(f(g(m)))) == g(g(f(g(g(k))))). [resolve(368,c,20,a)]. given #238 (T,wt=18): 487 m == k | b == k | f(g(f(g(m)))) == f(g(f(g(g(k))))). [resolve(368,c,19,a)]. given #239 (T,wt=18): 498 m == k | b == k | g(f(f(g(m)))) == g(f(f(g(g(k))))). [resolve(369,c,20,a)]. given #240 (A,wt=25): 141 k == b | g(k) == k | g(k) == m | g(k) == b | b == k | k == m | -(f(k) == k). [resolve(73,g,5,b),merge(g)]. given #241 (T,wt=18): 499 m == k | b == k | f(f(f(g(m)))) == f(f(f(g(g(k))))). [resolve(369,c,19,a)]. given #242 (T,wt=18): 511 m == k | b == k | g(g(g(f(m)))) == g(g(g(f(g(k))))). [resolve(380,c,20,a)]. given #243 (T,wt=18): 512 m == k | b == k | f(g(g(f(m)))) == f(g(g(f(g(k))))). [resolve(380,c,19,a)]. given #244 (T,wt=18): 523 m == k | b == k | g(f(g(f(m)))) == g(f(g(f(g(k))))). [resolve(381,c,20,a)]. given #245 (A,wt=25): 142 k == b | g(k) == k | g(k) == m | g(k) == b | b == k | k == m | -(f(k) == m). [resolve(73,g,4,b),merge(g)]. given #246 (T,wt=18): 524 m == k | b == k | f(f(g(f(m)))) == f(f(g(f(g(k))))). [resolve(381,c,19,a)]. given #247 (T,wt=18): 536 m == k | b == k | g(g(f(f(m)))) == g(g(f(f(g(k))))). [resolve(391,c,20,a)]. given #248 (T,wt=18): 537 m == k | b == k | f(g(f(f(m)))) == f(g(f(f(g(k))))). [resolve(391,c,19,a)]. given #249 (T,wt=18): 549 m == k | b == k | g(f(f(f(m)))) == g(f(f(f(g(k))))). [resolve(392,c,20,a)]. given #250 (A,wt=27): 143 k == b | g(k) == k | g(k) == m | g(k) == b | b == k | k == m | -p(m,b) | -p(m,k). [resolve(73,g,2,f),merge(i),merge(j),unit_del(g,21)]. given #251 (T,wt=18): 550 m == k | b == k | f(f(f(f(m)))) == f(f(f(f(g(k))))). [resolve(392,c,19,a)]. given #252 (T,wt=18): 562 m == k | b == k | g(g(g(g(g(k))))) == g(g(g(g(m)))). [resolve(403,c,20,a)]. given #253 (T,wt=18): 563 m == k | b == k | f(g(g(g(g(k))))) == f(g(g(g(m)))). [resolve(403,c,19,a)]. given #254 (T,wt=18): 575 m == k | b == k | g(f(g(g(g(k))))) == g(f(g(g(m)))). [resolve(404,c,20,a)]. given #255 (A,wt=27): 144 b == k | k == m | k == b | g(k) == k | g(k) == m | g(k) == b | -(m == x) | p(b,x). [resolve(83,b,18,b)]. given #256 (T,wt=18): 576 m == k | b == k | f(f(g(g(g(k))))) == f(f(g(g(m)))). [resolve(404,c,19,a)]. given #257 (T,wt=18): 588 m == k | b == k | g(g(f(g(g(k))))) == g(g(f(g(m)))). [resolve(414,c,20,a)]. given #258 (T,wt=18): 589 m == k | b == k | f(g(f(g(g(k))))) == f(g(f(g(m)))). [resolve(414,c,19,a)]. given #259 (T,wt=18): 609 m == k | b == k | g(f(f(g(g(k))))) == g(f(f(g(m)))). [resolve(415,c,20,a)]. given #260 (A,wt=27): 145 b == k | k == m | k == b | g(k) == k | g(k) == m | g(k) == b | -(b == x) | p(x,m). [resolve(83,b,17,b)]. given #261 (T,wt=18): 610 m == k | b == k | f(f(f(g(g(k))))) == f(f(f(g(m)))). [resolve(415,c,19,a)]. given #262 (T,wt=18): 623 m == k | b == k | g(g(g(f(g(k))))) == g(g(g(f(m)))). [resolve(426,c,20,a)]. given #263 (T,wt=18): 624 m == k | b == k | f(g(g(f(g(k))))) == f(g(g(f(m)))). [resolve(426,c,19,a)]. given #264 (T,wt=18): 636 m == k | b == k | g(f(g(f(g(k))))) == g(f(g(f(m)))). [resolve(427,c,20,a)]. given #265 (A,wt=25): 146 b == k | k == m | k == b | g(k) == k | g(k) == m | g(k) == b | p(f(b),b). [resolve(83,b,7,b),unit_del(g,41)]. given #266 (T,wt=18): 637 m == k | b == k | f(f(g(f(g(k))))) == f(f(g(f(m)))). [resolve(427,c,19,a)]. given #267 (T,wt=18): 650 m == k | b == k | g(g(f(f(g(k))))) == g(g(f(f(m)))). [resolve(437,c,20,a)]. given #268 (T,wt=18): 651 m == k | b == k | f(g(f(f(g(k))))) == f(g(f(f(m)))). [resolve(437,c,19,a)]. given #269 (T,wt=18): 662 m == k | b == k | g(f(f(f(g(k))))) == g(f(f(f(m)))). [resolve(438,c,20,a)]. given #270 (A,wt=25): 147 b == k | k == m | k == b | g(k) == k | g(k) == m | g(k) == b | p(b,f(b)). [resolve(83,b,6,b),unit_del(g,41)]. given #271 (T,wt=18): 663 m == k | b == k | f(f(f(f(g(k))))) == f(f(f(f(m)))). [resolve(438,c,19,a)]. given #272 (T,wt=18): 672 m == k | b == k | p(m,b) | -(g(k) == x) | p(g(g(k)),x). [resolve(671,d,18,b)]. given #273 (T,wt=18): 673 m == k | b == k | p(m,b) | -(g(g(k)) == x) | p(x,g(k)). [resolve(671,d,17,b)]. given #274 (T,wt=18): 678 m == k | b == k | p(m,b) | -(g(g(k)) == x) | p(g(k),x). [resolve(676,d,18,b)]. given #275 (A,wt=25): 148 b == k | k == m | k == b | g(k) == k | g(k) == m | g(k) == b | -(f(b) == b). [resolve(83,b,5,b),unit_del(g,41)]. given #276 (T,wt=18): 679 m == k | b == k | p(m,b) | -(g(k) == x) | p(x,g(g(k))). [resolve(676,d,17,b)]. given #277 (T,wt=19): 276 m == k | b == k | p(g(g(k)),m) | g(k) == b | p(g(k),b). [resolve(269,c,39,a)]. given #278 (T,wt=19): 277 m == k | b == k | p(m,g(g(k))) | g(k) == b | p(g(k),b). [resolve(269,c,38,a)]. given #279 (T,wt=19): 309 m == k | b == k | p(g(k),g(m)) | g(k) == b | p(g(k),b). [resolve(278,c,40,a)]. given #280 (A,wt=25): 149 b == k | k == m | k == b | g(k) == k | g(k) == m | g(k) == b | -(f(b) == m). [resolve(83,b,4,b),unit_del(g,41)]. given #281 (T,wt=18): 1148 m == k | b == k | g(k) == b | p(g(k),b) | -(g(m) == b). [factor(1145,d,f)]. given #282 (T,wt=19): 312 m == k | b == k | p(g(m),g(k)) | g(k) == b | p(g(k),b). [resolve(278,c,37,a)]. given #283 (T,wt=19): 448 m == k | b == k | k == b | p(k,b) | k == m | p(f(k),k). [resolve(275,c,7,b)]. given #284 (T,wt=19): 449 m == k | b == k | k == b | p(k,b) | k == m | p(k,f(k)). [resolve(275,c,6,b)]. given #285 (A,wt=27): 151 k == b | g(k) == k | g(k) == m | g(k) == b | j == b | j == k | -p(j,k) | k == j. [resolve(76,g,43,b)]. given #286 (T,wt=19): 450 m == k | b == k | k == b | p(k,b) | k == m | -(f(k) == k). [resolve(275,c,5,b)]. given #287 (T,wt=19): 451 m == k | b == k | k == b | p(k,b) | k == m | -(f(k) == m). [resolve(275,c,4,b)]. given #288 (T,wt=19): 463 m == k | b == k | -(x == g(g(g(m)))) | x == g(g(g(g(k)))). [resolve(355,c,16,b)]. given #289 (T,wt=19): 464 m == k | b == k | -(g(g(g(g(k)))) == x) | g(g(g(m))) == x. [resolve(355,c,16,a)]. given #290 (A,wt=28): 189 j == b | j == m | g(j) == m | g(j) == j | f(j) == j | f(j) == k | -(b == x) | p(j,x). [resolve(100,b,18,b)]. given #291 (T,wt=19): 475 m == k | b == k | -(x == f(g(g(m)))) | x == f(g(g(g(k)))). [resolve(356,c,16,b)]. given #292 (T,wt=19): 476 m == k | b == k | -(f(g(g(g(k)))) == x) | f(g(g(m))) == x. [resolve(356,c,16,a)]. given #293 (T,wt=19): 488 m == k | b == k | -(x == g(f(g(m)))) | x == g(f(g(g(k)))). [resolve(368,c,16,b)]. given #294 (T,wt=19): 489 m == k | b == k | -(g(f(g(g(k)))) == x) | g(f(g(m))) == x. [resolve(368,c,16,a)]. given #295 (A,wt=28): 190 j == b | j == m | g(j) == m | g(j) == j | f(j) == j | f(j) == k | -(j == x) | p(x,b). [resolve(100,b,17,b)]. given #296 (T,wt=19): 500 m == k | b == k | -(x == f(f(g(m)))) | x == f(f(g(g(k)))). [resolve(369,c,16,b)]. given #297 (T,wt=19): 501 m == k | b == k | -(f(f(g(g(k)))) == x) | f(f(g(m))) == x. [resolve(369,c,16,a)]. given #298 (T,wt=19): 513 m == k | b == k | -(x == g(g(f(m)))) | x == g(g(f(g(k)))). [resolve(380,c,16,b)]. given #299 (T,wt=19): 514 m == k | b == k | -(g(g(f(g(k)))) == x) | g(g(f(m))) == x. [resolve(380,c,16,a)]. given #300 (A,wt=34): 191 j == b | j == m | g(j) == m | g(j) == j | f(j) == j | f(j) == k | x == b | x == j | -p(j,x) | -p(x,j). [resolve(100,b,2,b),merge(g)]. given #301 (T,wt=19): 525 m == k | b == k | -(x == f(g(f(m)))) | x == f(g(f(g(k)))). [resolve(381,c,16,b)]. given #302 (T,wt=19): 526 m == k | b == k | -(f(g(f(g(k)))) == x) | f(g(f(m))) == x. [resolve(381,c,16,a)]. given #303 (T,wt=19): 538 m == k | b == k | -(x == g(f(f(m)))) | x == g(f(f(g(k)))). [resolve(391,c,16,b)]. given #304 (T,wt=19): 539 m == k | b == k | -(g(f(f(g(k)))) == x) | g(f(f(m))) == x. [resolve(391,c,16,a)]. given #305 (A,wt=28): 192 j == b | j == m | g(j) == m | g(j) == j | f(j) == j | f(j) == k | p(b,m) | -p(b,j). [resolve(100,b,1,f),merge(i),merge(j),unit_del(g,41)]. given #306 (T,wt=19): 551 m == k | b == k | -(x == f(f(f(m)))) | x == f(f(f(g(k)))). [resolve(392,c,16,b)]. given #307 (T,wt=19): 552 m == k | b == k | -(f(f(f(g(k)))) == x) | f(f(f(m))) == x. [resolve(392,c,16,a)]. given #308 (T,wt=19): 564 m == k | b == k | -(x == g(g(g(g(k))))) | x == g(g(g(m))). [resolve(403,c,16,b)]. given #309 (T,wt=19): 565 m == k | b == k | -(g(g(g(m))) == x) | g(g(g(g(k)))) == x. [resolve(403,c,16,a)]. given #310 (A,wt=31): 193 j == b | j == m | g(j) == m | g(j) == j | f(j) == j | f(j) == k | p(j,m) | b == j | -p(b,j). [resolve(100,b,1,e),merge(g),unit_del(h,41)]. given #311 (T,wt=19): 577 m == k | b == k | -(x == f(g(g(g(k))))) | x == f(g(g(m))). [resolve(404,c,16,b)]. given #312 (T,wt=19): 578 m == k | b == k | -(f(g(g(m))) == x) | f(g(g(g(k)))) == x. [resolve(404,c,16,a)]. given #313 (T,wt=19): 590 m == k | b == k | -(x == g(f(g(g(k))))) | x == g(f(g(m))). [resolve(414,c,16,b)]. given #314 (T,wt=19): 591 m == k | b == k | -(g(f(g(m))) == x) | g(f(g(g(k)))) == x. [resolve(414,c,16,a)]. given #315 (A,wt=34): 194 j == b | j == m | g(j) == m | g(j) == j | f(j) == j | f(j) == k | g(j) == b | -p(j,g(j)) | -p(g(j),j). [factor(191,d,h)]. given #316 (T,wt=19): 611 m == k | b == k | -(x == f(f(g(g(k))))) | x == f(f(g(m))). [resolve(415,c,16,b)]. given #317 (T,wt=19): 612 m == k | b == k | -(f(f(g(m))) == x) | f(f(g(g(k)))) == x. [resolve(415,c,16,a)]. given #318 (T,wt=19): 625 m == k | b == k | -(x == g(g(f(g(k))))) | x == g(g(f(m))). [resolve(426,c,16,b)]. given #319 (T,wt=19): 626 m == k | b == k | -(g(g(f(m))) == x) | g(g(f(g(k)))) == x. [resolve(426,c,16,a)]. given #320 (A,wt=32): 226 k == b | k == m | g(k) == m | g(k) == k | f(k) == k | f(k) == m | f(k) == b | b == k | p(b,m). [resolve(103,b,48,e),merge(j),merge(k)]. given #321 (T,wt=19): 638 m == k | b == k | -(x == f(g(f(g(k))))) | x == f(g(f(m))). [resolve(427,c,16,b)]. given #322 (T,wt=19): 639 m == k | b == k | -(f(g(f(m))) == x) | f(g(f(g(k)))) == x. [resolve(427,c,16,a)]. given #323 (T,wt=19): 652 m == k | b == k | -(x == g(f(f(g(k))))) | x == g(f(f(m))). [resolve(437,c,16,b)]. given #324 (T,wt=19): 653 m == k | b == k | -(g(f(f(m))) == x) | g(f(f(g(k)))) == x. [resolve(437,c,16,a)]. given #325 (A,wt=32): 227 k == b | k == m | g(k) == m | g(k) == k | f(k) == k | f(k) == m | f(k) == b | b == k | p(k,m). [resolve(103,b,47,d),merge(i)]. given #326 (T,wt=19): 664 m == k | b == k | -(x == f(f(f(g(k))))) | x == f(f(f(m))). [resolve(438,c,16,b)]. given #327 (T,wt=19): 665 m == k | b == k | -(f(f(f(m))) == x) | f(f(f(g(k)))) == x. [resolve(438,c,16,a)]. given #328 (T,wt=19): 1162 m == k | b == k | k == b | p(k,b) | k == m | -(f(k) == b). [factor(1158,d,g)]. given #329 (T,wt=20): 287 m == k | b == k | p(m,b) | g(m) == m | p(g(g(k)),f(g(m))). [resolve(265,c,68,c)]. given #330 (A,wt=32): 228 k == b | k == m | g(k) == m | g(k) == k | f(k) == k | f(k) == m | f(k) == b | -(b == x) | p(k,x). [resolve(103,b,18,b)]. given #331 (T,wt=20): 288 m == k | b == k | p(m,b) | g(m) == m | p(f(g(m)),g(g(k))). [resolve(265,c,61,c)]. given #332 (T,wt=20): 345 m == k | b == k | p(m,b) | g(g(k)) == m | -(f(g(g(k))) == m). [resolve(292,c,4,b)]. given #333 (T,wt=20): 364 m == k | b == k | p(m,b) | g(m) == m | p(g(m),f(g(g(k)))). [resolve(294,c,67,c)]. given #334 (T,wt=20): 365 m == k | b == k | p(m,b) | g(m) == m | p(f(g(g(k))),g(m)). [resolve(294,c,62,c)]. given #335 (A,wt=32): 229 k == b | k == m | g(k) == m | g(k) == k | f(k) == k | f(k) == m | f(k) == b | -(k == x) | p(x,b). [resolve(103,b,17,b)]. given #336 (T,wt=20): 713 m == k | b == k | g(g(g(g(g(m))))) == g(g(g(g(g(g(k)))))). [resolve(461,c,20,a)]. given #337 (T,wt=20): 714 m == k | b == k | f(g(g(g(g(m))))) == f(g(g(g(g(g(k)))))). [resolve(461,c,19,a)]. given #338 (T,wt=20): 726 m == k | b == k | g(f(g(g(g(m))))) == g(f(g(g(g(g(k)))))). [resolve(462,c,20,a)]. given #339 (T,wt=20): 727 m == k | b == k | f(f(g(g(g(m))))) == f(f(g(g(g(g(k)))))). [resolve(462,c,19,a)]. given #340 (A,wt=38): 230 k == b | k == m | g(k) == m | g(k) == k | f(k) == k | f(k) == m | f(k) == b | x == b | x == k | -p(k,x) | -p(x,k). [resolve(103,b,2,b),merge(h)]. given #341 (T,wt=20): 740 m == k | b == k | g(g(f(g(g(m))))) == g(g(f(g(g(g(k)))))). [resolve(473,c,20,a)]. given #342 (T,wt=20): 741 m == k | b == k | f(g(f(g(g(m))))) == f(g(f(g(g(g(k)))))). [resolve(473,c,19,a)]. given #343 (T,wt=20): 756 m == k | b == k | g(f(f(g(g(m))))) == g(f(f(g(g(g(k)))))). [resolve(474,c,20,a)]. given #344 (T,wt=20): 757 m == k | b == k | f(f(f(g(g(m))))) == f(f(f(g(g(g(k)))))). [resolve(474,c,19,a)]. given #345 (A,wt=32): 231 k == b | k == m | g(k) == m | g(k) == k | f(k) == k | f(k) == m | f(k) == b | p(b,m) | -p(b,k). [resolve(103,b,1,f),merge(j),merge(k),unit_del(h,41)]. given #346 (T,wt=20): 770 m == k | b == k | g(g(g(f(g(m))))) == g(g(g(f(g(g(k)))))). [resolve(486,c,20,a)]. given #347 (T,wt=20): 771 m == k | b == k | f(g(g(f(g(m))))) == f(g(g(f(g(g(k)))))). [resolve(486,c,19,a)]. given #348 (T,wt=20): 783 m == k | b == k | g(f(g(f(g(m))))) == g(f(g(f(g(g(k)))))). [resolve(487,c,20,a)]. given #349 (T,wt=20): 784 m == k | b == k | f(f(g(f(g(m))))) == f(f(g(f(g(g(k)))))). [resolve(487,c,19,a)]. given #350 (A,wt=28): 260 m == k | b == k | x == b | p(x,b) | g(x) == m | x == m | x == g(x) | p(g(x),g(k)). [resolve(259,c,92,f)]. given #351 (T,wt=20): 797 m == k | b == k | g(g(f(f(g(m))))) == g(g(f(f(g(g(k)))))). [resolve(498,c,20,a)]. given #352 (T,wt=20): 798 m == k | b == k | f(g(f(f(g(m))))) == f(g(f(f(g(g(k)))))). [resolve(498,c,19,a)]. given #353 (T,wt=20): 808 m == k | b == k | g(f(f(f(g(m))))) == g(f(f(f(g(g(k)))))). [resolve(499,c,20,a)]. given #354 (T,wt=20): 809 m == k | b == k | f(f(f(f(g(m))))) == f(f(f(f(g(g(k)))))). [resolve(499,c,19,a)]. given #355 (A,wt=27): 261 m == k | b == k | x == b | p(x,b) | x == m | g(x) == m | g(x) == x | p(x,g(k)). [resolve(259,c,85,f)]. given #356 (T,wt=20): 822 m == k | b == k | g(g(g(g(f(m))))) == g(g(g(g(f(g(k)))))). [resolve(511,c,20,a)]. given #357 (T,wt=20): 823 m == k | b == k | f(g(g(g(f(m))))) == f(g(g(g(f(g(k)))))). [resolve(511,c,19,a)]. given #358 (T,wt=20): 835 m == k | b == k | g(f(g(g(f(m))))) == g(f(g(g(f(g(k)))))). [resolve(512,c,20,a)]. given #359 (T,wt=20): 836 m == k | b == k | f(f(g(g(f(m))))) == f(f(g(g(f(g(k)))))). [resolve(512,c,19,a)]. given #360 (A,wt=24): 273 m == k | b == k | k == b | -p(k,b) | g(k) == b | g(k) == k | -p(k,g(k)). [resolve(262,c,2,f)]. given #361 (T,wt=20): 849 m == k | b == k | g(g(f(g(f(m))))) == g(g(f(g(f(g(k)))))). [resolve(523,c,20,a)]. given #362 (T,wt=20): 850 m == k | b == k | f(g(f(g(f(m))))) == f(g(f(g(f(g(k)))))). [resolve(523,c,19,a)]. given #363 (T,wt=20): 860 m == k | b == k | g(f(f(g(f(m))))) == g(f(f(g(f(g(k)))))). [resolve(524,c,20,a)]. given #364 (T,wt=20): 861 m == k | b == k | f(f(f(g(f(m))))) == f(f(f(g(f(g(k)))))). [resolve(524,c,19,a)]. given #365 (A,wt=25): 274 m == k | b == k | g(k) == b | -p(g(k),b) | k == b | k == g(k) | -p(k,g(k)). [resolve(262,c,2,e)]. given #366 (T,wt=20): 874 m == k | b == k | g(g(g(f(f(m))))) == g(g(g(f(f(g(k)))))). [resolve(536,c,20,a)]. given #367 (T,wt=20): 875 m == k | b == k | f(g(g(f(f(m))))) == f(g(g(f(f(g(k)))))). [resolve(536,c,19,a)]. given #368 (T,wt=20): 887 m == k | b == k | g(f(g(f(f(m))))) == g(f(g(f(f(g(k)))))). [resolve(537,c,20,a)]. given #369 (T,wt=20): 888 m == k | b == k | f(f(g(f(f(m))))) == f(f(g(f(f(g(k)))))). [resolve(537,c,19,a)]. given #370 (A,wt=29): 283 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | f(x) == m | p(f(x),m) | x == f(x). [resolve(105,i,88,f),merge(i),merge(j),merge(k),merge(l),merge(m)]. given #371 (T,wt=20): 901 m == k | b == k | g(g(f(f(f(m))))) == g(g(f(f(f(g(k)))))). [resolve(549,c,20,a)]. given #372 (T,wt=20): 902 m == k | b == k | f(g(f(f(f(m))))) == f(g(f(f(f(g(k)))))). [resolve(549,c,19,a)]. given #373 (T,wt=20): 912 m == k | b == k | g(f(f(f(f(m))))) == g(f(f(f(f(g(k)))))). [resolve(550,c,20,a)]. given #374 (T,wt=20): 913 m == k | b == k | f(f(f(f(f(m))))) == f(f(f(f(f(g(k)))))). [resolve(550,c,19,a)]. given #375 (A,wt=36): 284 m == k | b == k | g(m) == b | p(g(m),b) | g(m) == m | g(g(m)) == m | g(g(m)) == g(m) | p(g(g(k)),f(g(m))). [resolve(265,c,107,f)]. given #376 (T,wt=20): 926 m == k | b == k | g(g(g(g(g(g(k)))))) == g(g(g(g(g(m))))). [resolve(562,c,20,a)]. given #377 (T,wt=20): 927 m == k | b == k | f(g(g(g(g(g(k)))))) == f(g(g(g(g(m))))). [resolve(562,c,19,a)]. given #378 (T,wt=20): 939 m == k | b == k | g(f(g(g(g(g(k)))))) == g(f(g(g(g(m))))). [resolve(563,c,20,a)]. given #379 (T,wt=20): 940 m == k | b == k | f(f(g(g(g(g(k)))))) == f(f(g(g(g(m))))). [resolve(563,c,19,a)]. given #380 (A,wt=36): 285 m == k | b == k | g(m) == b | p(g(m),b) | g(m) == m | g(g(m)) == m | g(g(m)) == g(m) | p(f(g(m)),g(g(k))). [resolve(265,c,101,f)]. given #381 (T,wt=20): 953 m == k | b == k | g(g(f(g(g(g(k)))))) == g(g(f(g(g(m))))). [resolve(575,c,20,a)]. given #382 (T,wt=20): 954 m == k | b == k | f(g(f(g(g(g(k)))))) == f(g(f(g(g(m))))). [resolve(575,c,19,a)]. given #383 (T,wt=20): 964 m == k | b == k | g(f(f(g(g(g(k)))))) == g(f(f(g(g(m))))). [resolve(576,c,20,a)]. given #384 (T,wt=20): 965 m == k | b == k | f(f(f(g(g(g(k)))))) == f(f(f(g(g(m))))). [resolve(576,c,19,a)]. given #385 (A,wt=34): 286 m == k | b == k | g(m) == b | p(g(m),b) | g(m) == m | g(g(m)) == m | g(g(m)) == g(m) | p(g(g(k)),m). [resolve(265,c,86,f)]. given #386 (T,wt=20): 978 m == k | b == k | g(g(g(f(g(g(k)))))) == g(g(g(f(g(m))))). [resolve(588,c,20,a)]. given #387 (T,wt=20): 979 m == k | b == k | f(g(g(f(g(g(k)))))) == f(g(g(f(g(m))))). [resolve(588,c,19,a)]. given #388 (T,wt=20): 991 m == k | b == k | g(f(g(f(g(g(k)))))) == g(f(g(f(g(m))))). [resolve(589,c,20,a)]. given #389 (T,wt=20): 992 m == k | b == k | f(f(g(f(g(g(k)))))) == f(f(g(f(g(m))))). [resolve(589,c,19,a)]. given #390 (A,wt=21): 290 m == k | b == k | p(g(g(m)),g(g(k))) | g(m) == b | p(g(m),b). [resolve(265,c,39,a)]. given #391 (T,wt=20): 1005 m == k | b == k | g(g(f(f(g(g(k)))))) == g(g(f(f(g(m))))). [resolve(609,c,20,a)]. given #392 (T,wt=20): 1006 m == k | b == k | f(g(f(f(g(g(k)))))) == f(g(f(f(g(m))))). [resolve(609,c,19,a)]. given #393 (T,wt=20): 1016 m == k | b == k | g(f(f(f(g(g(k)))))) == g(f(f(f(g(m))))). [resolve(610,c,20,a)]. given #394 (T,wt=20): 1017 m == k | b == k | f(f(f(f(g(g(k)))))) == f(f(f(f(g(m))))). [resolve(610,c,19,a)]. given #395 (A,wt=21): 291 m == k | b == k | p(g(g(k)),g(g(m))) | g(m) == b | p(g(m),b). [resolve(265,c,38,a)]. given #396 (T,wt=20): 1030 m == k | b == k | g(g(g(g(f(g(k)))))) == g(g(g(g(f(m))))). [resolve(623,c,20,a)]. given #397 (T,wt=20): 1031 m == k | b == k | f(g(g(g(f(g(k)))))) == f(g(g(g(f(m))))). [resolve(623,c,19,a)]. given #398 (T,wt=20): 1043 m == k | b == k | g(f(g(g(f(g(k)))))) == g(f(g(g(f(m))))). [resolve(624,c,20,a)]. given #399 (T,wt=20): 1044 m == k | b == k | f(f(g(g(f(g(k)))))) == f(f(g(g(f(m))))). [resolve(624,c,19,a)]. given #400 (A,wt=36): 297 m == k | b == k | f(m) == b | p(f(m),b) | f(m) == m | g(f(m)) == m | g(f(m)) == f(m) | p(f(g(k)),f(f(m))). [resolve(266,c,107,f)]. given #401 (T,wt=20): 1057 m == k | b == k | g(g(f(g(f(g(k)))))) == g(g(f(g(f(m))))). [resolve(636,c,20,a)]. given #402 (T,wt=20): 1058 m == k | b == k | f(g(f(g(f(g(k)))))) == f(g(f(g(f(m))))). [resolve(636,c,19,a)]. given #403 (T,wt=20): 1074 m == k | b == k | g(f(f(g(f(g(k)))))) == g(f(f(g(f(m))))). [resolve(637,c,20,a)]. given #404 (T,wt=20): 1075 m == k | b == k | f(f(f(g(f(g(k)))))) == f(f(f(g(f(m))))). [resolve(637,c,19,a)]. given #405 (A,wt=36): 298 m == k | b == k | f(m) == b | p(f(m),b) | f(m) == m | g(f(m)) == m | g(f(m)) == f(m) | p(f(f(m)),f(g(k))). [resolve(266,c,101,f)]. given #406 (T,wt=20): 1088 m == k | b == k | g(g(g(f(f(g(k)))))) == g(g(g(f(f(m))))). [resolve(650,c,20,a)]. given #407 (T,wt=20): 1089 m == k | b == k | f(g(g(f(f(g(k)))))) == f(g(g(f(f(m))))). [resolve(650,c,19,a)]. given #408 (T,wt=20): 1101 m == k | b == k | g(f(g(f(f(g(k)))))) == g(f(g(f(f(m))))). [resolve(651,c,20,a)]. given #409 (T,wt=20): 1102 m == k | b == k | f(f(g(f(f(g(k)))))) == f(f(g(f(f(m))))). [resolve(651,c,19,a)]. given #410 (A,wt=34): 299 m == k | b == k | f(m) == b | p(f(m),b) | f(m) == m | g(f(m)) == m | g(f(m)) == f(m) | p(f(g(k)),m). [resolve(266,c,86,f)]. given #411 (T,wt=20): 1115 m == k | b == k | g(g(f(f(f(g(k)))))) == g(g(f(f(f(m))))). [resolve(662,c,20,a)]. given #412 (T,wt=20): 1116 m == k | b == k | f(g(f(f(f(g(k)))))) == f(g(f(f(f(m))))). [resolve(662,c,19,a)]. given #413 (T,wt=20): 1129 m == k | b == k | g(f(f(f(f(g(k)))))) == g(f(f(f(f(m))))). [resolve(663,c,20,a)]. given #414 (T,wt=20): 1130 m == k | b == k | f(f(f(f(f(g(k)))))) == f(f(f(f(f(m))))). [resolve(663,c,19,a)]. given #415 (A,wt=21): 300 m == k | b == k | p(g(f(m)),f(g(k))) | f(m) == b | p(f(m),b). [resolve(266,c,39,a)]. given #416 (T,wt=21): 301 m == k | b == k | p(f(g(k)),g(f(m))) | f(m) == b | p(f(m),b). [resolve(266,c,38,a)]. given #417 (T,wt=21): 351 m == k | b == k | p(g(m),g(g(g(k)))) | g(m) == b | p(g(m),b). [resolve(293,c,40,a)]. given #418 (T,wt=20): 2110 m == k | b == k | g(m) == b | p(g(m),b) | -(g(g(g(k))) == b). [factor(2105,d,f)]. given #419 (T,wt=21): 354 m == k | b == k | p(g(g(g(k))),g(m)) | g(m) == b | p(g(m),b). [resolve(293,c,37,a)]. given #420 (A,wt=42): 306 m == k | b == k | g(g(k)) == b | p(g(g(k)),b) | g(g(k)) == m | g(g(g(k))) == m | g(g(g(k))) == g(g(k)) | p(g(m),f(g(g(k)))). [resolve(278,c,107,f)]. given #421 (T,wt=21): 376 m == k | b == k | p(f(m),g(f(g(k)))) | f(m) == b | p(f(m),b). [resolve(302,c,40,a)]. given #422 (T,wt=20): 2128 m == k | b == k | f(m) == b | p(f(m),b) | -(g(f(g(k))) == b). [factor(2123,d,f)]. given #423 (T,wt=21): 379 m == k | b == k | p(g(f(g(k))),f(m)) | f(m) == b | p(f(m),b). [resolve(302,c,37,a)]. given #424 (T,wt=21): 715 m == k | b == k | -(x == g(g(g(g(m))))) | x == g(g(g(g(g(k))))). [resolve(461,c,16,b)]. given #425 (A,wt=42): 307 m == k | b == k | g(g(k)) == b | p(g(g(k)),b) | g(g(k)) == m | g(g(g(k))) == m | g(g(g(k))) == g(g(k)) | p(f(g(g(k))),g(m)). [resolve(278,c,101,f)]. given #426 (T,wt=21): 716 m == k | b == k | -(g(g(g(g(g(k))))) == x) | g(g(g(g(m)))) == x. [resolve(461,c,16,a)]. given #427 (T,wt=21): 728 m == k | b == k | -(x == f(g(g(g(m))))) | x == f(g(g(g(g(k))))). [resolve(462,c,16,b)]. given #428 (T,wt=21): 729 m == k | b == k | -(f(g(g(g(g(k))))) == x) | f(g(g(g(m)))) == x. [resolve(462,c,16,a)]. given #429 (T,wt=21): 742 m == k | b == k | -(x == g(f(g(g(m))))) | x == g(f(g(g(g(k))))). [resolve(473,c,16,b)]. given #430 (A,wt=39): 308 m == k | b == k | g(g(k)) == b | p(g(g(k)),b) | g(g(k)) == m | g(g(g(k))) == m | g(g(g(k))) == g(g(k)) | p(g(m),m). [resolve(278,c,86,f)]. given #431 (T,wt=21): 743 m == k | b == k | -(g(f(g(g(g(k))))) == x) | g(f(g(g(m)))) == x. [resolve(473,c,16,a)]. given #432 (T,wt=21): 758 m == k | b == k | -(x == f(f(g(g(m))))) | x == f(f(g(g(g(k))))). [resolve(474,c,16,b)]. given #433 (T,wt=21): 759 m == k | b == k | -(f(f(g(g(g(k))))) == x) | f(f(g(g(m)))) == x. [resolve(474,c,16,a)]. given #434 (T,wt=21): 772 m == k | b == k | -(x == g(g(f(g(m))))) | x == g(g(f(g(g(k))))). [resolve(486,c,16,b)]. given #435 (A,wt=23): 310 m == k | b == k | p(g(g(g(k))),g(m)) | g(g(k)) == b | p(g(g(k)),b). [resolve(278,c,39,a)]. given #436 (T,wt=21): 773 m == k | b == k | -(g(g(f(g(g(k))))) == x) | g(g(f(g(m)))) == x. [resolve(486,c,16,a)]. given #437 (T,wt=21): 785 m == k | b == k | -(x == f(g(f(g(m))))) | x == f(g(f(g(g(k))))). [resolve(487,c,16,b)]. given #438 (T,wt=21): 786 m == k | b == k | -(f(g(f(g(g(k))))) == x) | f(g(f(g(m)))) == x. [resolve(487,c,16,a)]. given #439 (T,wt=21): 799 m == k | b == k | -(x == g(f(f(g(m))))) | x == g(f(f(g(g(k))))). [resolve(498,c,16,b)]. given #440 (A,wt=23): 311 m == k | b == k | p(g(m),g(g(g(k)))) | g(g(k)) == b | p(g(g(k)),b). [resolve(278,c,38,a)]. given #441 (T,wt=21): 800 m == k | b == k | -(g(f(f(g(g(k))))) == x) | g(f(f(g(m)))) == x. [resolve(498,c,16,a)]. given #442 (T,wt=21): 810 m == k | b == k | -(x == f(f(f(g(m))))) | x == f(f(f(g(g(k))))). [resolve(499,c,16,b)]. given #443 (T,wt=21): 811 m == k | b == k | -(f(f(f(g(g(k))))) == x) | f(f(f(g(m)))) == x. [resolve(499,c,16,a)]. given #444 (T,wt=21): 824 m == k | b == k | -(x == g(g(g(f(m))))) | x == g(g(g(f(g(k))))). [resolve(511,c,16,b)]. given #445 (A,wt=29): 318 x == b | p(x,b) | x == m | g(x) == m | g(x) == x | f(x) == b | -p(f(x),b) | x == f(x). [resolve(108,i,87,f),merge(i),merge(j),merge(k),merge(l),merge(m)]. given #446 (T,wt=21): 825 m == k | b == k | -(g(g(g(f(g(k))))) == x) | g(g(g(f(m)))) == x. [resolve(511,c,16,a)]. given #447 (T,wt=21): 837 m == k | b == k | -(x == f(g(g(f(m))))) | x == f(g(g(f(g(k))))). [resolve(512,c,16,b)]. given #448 (T,wt=21): 838 m == k | b == k | -(f(g(g(f(g(k))))) == x) | f(g(g(f(m)))) == x. [resolve(512,c,16,a)]. given #449 (T,wt=21): 851 m == k | b == k | -(x == g(f(g(f(m))))) | x == g(f(g(f(g(k))))). [resolve(523,c,16,b)]. given #450 (A,wt=42): 319 m == k | b == k | f(g(k)) == b | p(f(g(k)),b) | f(g(k)) == m | g(f(g(k))) == m | g(f(g(k))) == f(g(k)) | p(f(m),f(f(g(k)))). [resolve(279,c,107,f)]. given #451 (T,wt=21): 852 m == k | b == k | -(g(f(g(f(g(k))))) == x) | g(f(g(f(m)))) == x. [resolve(523,c,16,a)]. given #452 (T,wt=21): 862 m == k | b == k | -(x == f(f(g(f(m))))) | x == f(f(g(f(g(k))))). [resolve(524,c,16,b)]. given #453 (T,wt=21): 863 m == k | b == k | -(f(f(g(f(g(k))))) == x) | f(f(g(f(m)))) == x. [resolve(524,c,16,a)]. given #454 (T,wt=21): 876 m == k | b == k | -(x == g(g(f(f(m))))) | x == g(g(f(f(g(k))))). [resolve(536,c,16,b)]. given #455 (A,wt=42): 320 m == k | b == k | f(g(k)) == b | p(f(g(k)),b) | f(g(k)) == m | g(f(g(k))) == m | g(f(g(k))) == f(g(k)) | p(f(f(g(k))),f(m)). [resolve(279,c,101,f)]. given #456 (T,wt=21): 877 m == k | b == k | -(g(g(f(f(g(k))))) == x) | g(g(f(f(m)))) == x. [resolve(536,c,16,a)]. given #457 (T,wt=21): 889 m == k | b == k | -(x == f(g(f(f(m))))) | x == f(g(f(f(g(k))))). [resolve(537,c,16,b)]. given #458 (T,wt=21): 890 m == k | b == k | -(f(g(f(f(g(k))))) == x) | f(g(f(f(m)))) == x. [resolve(537,c,16,a)]. given #459 (T,wt=21): 903 m == k | b == k | -(x == g(f(f(f(m))))) | x == g(f(f(f(g(k))))). [resolve(549,c,16,b)]. given #460 (A,wt=39): 321 m == k | b == k | f(g(k)) == b | p(f(g(k)),b) | f(g(k)) == m | g(f(g(k))) == m | g(f(g(k))) == f(g(k)) | p(f(m),m). [resolve(279,c,86,f)]. given #461 (T,wt=21): 904 m == k | b == k | -(g(f(f(f(g(k))))) == x) | g(f(f(f(m)))) == x. [resolve(549,c,16,a)]. given #462 (T,wt=21): 914 m == k | b == k | -(x == f(f(f(f(m))))) | x == f(f(f(f(g(k))))). [resolve(550,c,16,b)]. given #463 (T,wt=21): 915 m == k | b == k | -(f(f(f(f(g(k))))) == x) | f(f(f(f(m)))) == x. [resolve(550,c,16,a)]. given #464 (T,wt=21): 928 m == k | b == k | -(x == g(g(g(g(g(k)))))) | x == g(g(g(g(m)))). [resolve(562,c,16,b)]. given #465 (A,wt=23): 322 m == k | b == k | p(g(f(g(k))),f(m)) | f(g(k)) == b | p(f(g(k)),b). [resolve(279,c,39,a)]. given #466 (T,wt=21): 929 m == k | b == k | -(g(g(g(g(m)))) == x) | g(g(g(g(g(k))))) == x. [resolve(562,c,16,a)]. given #467 (T,wt=21): 941 m == k | b == k | -(x == f(g(g(g(g(k)))))) | x == f(g(g(g(m)))). [resolve(563,c,16,b)]. given #468 (T,wt=21): 942 m == k | b == k | -(f(g(g(g(m)))) == x) | f(g(g(g(g(k))))) == x. [resolve(563,c,16,a)]. given #469 (T,wt=21): 955 m == k | b == k | -(x == g(f(g(g(g(k)))))) | x == g(f(g(g(m)))). [resolve(575,c,16,b)]. given #470 (A,wt=23): 323 m == k | b == k | p(f(m),g(f(g(k)))) | f(g(k)) == b | p(f(g(k)),b). [resolve(279,c,38,a)]. given #471 (T,wt=21): 956 m == k | b == k | -(g(f(g(g(m)))) == x) | g(f(g(g(g(k))))) == x. [resolve(575,c,16,a)]. given #472 (T,wt=21): 966 m == k | b == k | -(x == f(f(g(g(g(k)))))) | x == f(f(g(g(m)))). [resolve(576,c,16,b)]. given #473 (T,wt=21): 967 m == k | b == k | -(f(f(g(g(m)))) == x) | f(f(g(g(g(k))))) == x. [resolve(576,c,16,a)]. given #474 (T,wt=21): 980 m == k | b == k | -(x == g(g(f(g(g(k)))))) | x == g(g(f(g(m)))). [resolve(588,c,16,b)]. given #475 (A,wt=31): 330 m == k | b == k | p(m,b) | g(k) == b | -p(g(k),b) | g(m) == b | g(m) == g(k) | -p(g(k),g(m)). [resolve(263,c,2,f)]. given #476 (T,wt=21): 981 m == k | b == k | -(g(g(f(g(m)))) == x) | g(g(f(g(g(k))))) == x. [resolve(588,c,16,a)]. given #477 (T,wt=21): 993 m == k | b == k | -(x == f(g(f(g(g(k)))))) | x == f(g(f(g(m)))). [resolve(589,c,16,b)]. given #478 (T,wt=21): 994 m == k | b == k | -(f(g(f(g(m)))) == x) | f(g(f(g(g(k))))) == x. [resolve(589,c,16,a)]. given #479 (T,wt=21): 1007 m == k | b == k | -(x == g(f(f(g(g(k)))))) | x == g(f(f(g(m)))). [resolve(609,c,16,b)]. given #480 (A,wt=31): 331 m == k | b == k | p(m,b) | g(m) == b | -p(g(m),b) | g(k) == b | g(k) == g(m) | -p(g(k),g(m)). [resolve(263,c,2,e)]. given #481 (T,wt=21): 1008 m == k | b == k | -(g(f(f(g(m)))) == x) | g(f(f(g(g(k))))) == x. [resolve(609,c,16,a)]. given #482 (T,wt=21): 1018 m == k | b == k | -(x == f(f(f(g(g(k)))))) | x == f(f(f(g(m)))). [resolve(610,c,16,b)]. given #483 (T,wt=21): 1019 m == k | b == k | -(f(f(f(g(m)))) == x) | f(f(f(g(g(k))))) == x. [resolve(610,c,16,a)]. given #484 (T,wt=21): 1032 m == k | b == k | -(x == g(g(g(f(g(k)))))) | x == g(g(g(f(m)))). [resolve(623,c,16,b)]. given #485 (A,wt=29): 338 m == k | b == k | p(m,b) | g(g(k)) == b | -p(g(g(k)),b) | m == g(g(k)) | -p(g(g(k)),m). [resolve(289,c,2,f),unit_del(f,21)]. given #486 (T,wt=21): 1033 m == k | b == k | -(g(g(g(f(m)))) == x) | g(g(g(f(g(k))))) == x. [resolve(623,c,16,a)]. given #487 (T,wt=21): 1045 m == k | b == k | -(x == f(g(g(f(g(k)))))) | x == f(g(g(f(m)))). [resolve(624,c,16,b)]. given #488 (T,wt=21): 1046 m == k | b == k | -(f(g(g(f(m)))) == x) | f(g(g(f(g(k))))) == x. [resolve(624,c,16,a)]. given #489 (T,wt=21): 1059 m == k | b == k | -(x == g(f(g(f(g(k)))))) | x == g(f(g(f(m)))). [resolve(636,c,16,b)]. given #490 (A,wt=22): 342 m == k | b == k | p(m,b) | g(g(k)) == m | p(f(g(g(k))),g(g(k))). [resolve(292,c,7,b)]. given #491 (T,wt=21): 1060 m == k | b == k | -(g(f(g(f(m)))) == x) | g(f(g(f(g(k))))) == x. [resolve(636,c,16,a)]. given #492 (T,wt=21): 1076 m == k | b == k | -(x == f(f(g(f(g(k)))))) | x == f(f(g(f(m)))). [resolve(637,c,16,b)]. given #493 (T,wt=21): 1077 m == k | b == k | -(f(f(g(f(m)))) == x) | f(f(g(f(g(k))))) == x. [resolve(637,c,16,a)]. given #494 (T,wt=21): 1090 m == k | b == k | -(x == g(g(f(f(g(k)))))) | x == g(g(f(f(m)))). [resolve(650,c,16,b)]. given #495 (A,wt=22): 343 m == k | b == k | p(m,b) | g(g(k)) == m | p(g(g(k)),f(g(g(k)))). [resolve(292,c,6,b)]. given #496 (T,wt=21): 1091 m == k | b == k | -(g(g(f(f(m)))) == x) | g(g(f(f(g(k))))) == x. [resolve(650,c,16,a)]. given #497 (T,wt=21): 1103 m == k | b == k | -(x == f(g(f(f(g(k)))))) | x == f(g(f(f(m)))). [resolve(651,c,16,b)]. given #498 (T,wt=21): 1104 m == k | b == k | -(f(g(f(f(m)))) == x) | f(g(f(f(g(k))))) == x. [resolve(651,c,16,a)]. given #499 (T,wt=21): 1117 m == k | b == k | -(x == g(f(f(f(g(k)))))) | x == g(f(f(f(m)))). [resolve(662,c,16,b)]. given #500 (A,wt=22): 344 m == k | b == k | p(m,b) | g(g(k)) == m | -(f(g(g(k))) == g(g(k))). [resolve(292,c,5,b)]. given #501 (T,wt=21): 1118 m == k | b == k | -(g(f(f(f(m)))) == x) | g(f(f(f(g(k))))) == x. [resolve(662,c,16,a)]. given #502 (T,wt=21): 1131 m == k | b == k | -(x == f(f(f(f(g(k)))))) | x == f(f(f(f(m)))). [resolve(663,c,16,b)]. given #503 (T,wt=21): 1132 m == k | b == k | -(f(f(f(f(m)))) == x) | f(f(f(f(g(k))))) == x. [resolve(663,c,16,a)]. given #504 (T,wt=22): 1133 m == k | b == k | g(k) == b | p(g(k),b) | -(m == x) | p(g(g(k)),x). [resolve(276,c,18,b)]. given #505 (A,wt=44): 347 m == k | b == k | g(g(m)) == b | p(g(g(m)),b) | g(g(m)) == m | g(g(g(m))) == m | g(g(g(m))) == g(g(m)) | p(g(g(g(k))),f(g(g(m)))). [resolve(293,c,107,f)]. given #506 (T,wt=22): 1134 m == k | b == k | g(k) == b | p(g(k),b) | -(g(g(k)) == x) | p(x,m). [resolve(276,c,17,b)]. given #507 (T,wt=18): 2205 m == k | b == k | g(k) == b | p(g(k),b) | p(g(m),m). [resolve(1134,e,278,c),merge(f),merge(g)]. given #508 (T,wt=21): 2208 m == k | b == k | g(k) == b | p(g(m),m) | -(b == x) | p(g(k),x). [resolve(2205,d,18,b)]. given #509 (T,wt=21): 2209 m == k | b == k | g(k) == b | p(g(m),m) | -(g(k) == x) | p(x,b). [resolve(2205,d,17,b)]. given #510 (A,wt=44): 348 m == k | b == k | g(g(m)) == b | p(g(g(m)),b) | g(g(m)) == m | g(g(g(m))) == m | g(g(g(m))) == g(g(m)) | p(f(g(g(m))),g(g(g(k)))). [resolve(293,c,101,f)]. given #511 (T,wt=22): 1142 m == k | b == k | p(m,g(g(k))) | g(k) == b | -(b == x) | p(g(k),x). [resolve(277,e,18,b)]. given #512 (T,wt=22): 1143 m == k | b == k | p(m,g(g(k))) | g(k) == b | -(g(k) == x) | p(x,b). [resolve(277,e,17,b)]. given #513 (T,wt=22): 1145 m == k | b == k | g(k) == b | p(g(k),b) | -(g(m) == x) | p(g(k),x). [resolve(309,c,18,b)]. given #514 (T,wt=22): 1146 m == k | b == k | g(k) == b | p(g(k),b) | -(g(k) == x) | p(x,g(m)). [resolve(309,c,17,b)]. given #515 (A,wt=35): 349 m == k | b == k | g(m) == b | p(g(m),b) | g(g(m)) == m | g(m) == m | g(m) == g(g(m)) | p(g(g(g(k))),m). [resolve(293,c,93,f)]. given #516 (T,wt=18): 2216 m == k | b == k | g(k) == b | p(g(k),b) | p(m,g(m)). [resolve(1146,e,269,c),merge(f),merge(g)]. given #517 (T,wt=21): 2227 m == k | b == k | g(k) == b | p(m,g(m)) | -(b == x) | p(g(k),x). [resolve(2216,d,18,b)]. given #518 (T,wt=21): 2228 m == k | b == k | g(k) == b | p(m,g(m)) | -(g(k) == x) | p(x,b). [resolve(2216,d,17,b)]. given #519 (T,wt=22): 1150 m == k | b == k | p(g(m),g(k)) | g(k) == b | -(b == x) | p(g(k),x). [resolve(312,e,18,b)]. given #520 (A,wt=41): 350 m == k | b == k | g(g(m)) == b | p(g(g(m)),b) | g(g(m)) == m | g(g(g(m))) == m | g(g(g(m))) == g(g(m)) | p(g(g(g(k))),m). [resolve(293,c,86,f)]. given #521 (T,wt=22): 1151 m == k | b == k | p(g(m),g(k)) | g(k) == b | -(g(k) == x) | p(x,b). [resolve(312,e,17,b)]. given #522 (T,wt=22): 1153 m == k | b == k | k == b | p(k,b) | k == m | -(k == x) | p(f(k),x). [resolve(448,f,18,b)]. given #523 (T,wt=22): 1154 m == k | b == k | k == b | p(k,b) | k == m | -(f(k) == x) | p(x,k). [resolve(448,f,17,b)]. given #524 (T,wt=22): 1158 m == k | b == k | k == b | p(k,b) | k == m | -(f(k) == x) | p(k,x). [resolve(449,f,18,b)]. given #525 (A,wt=25): 352 m == k | b == k | p(g(g(g(m))),g(g(g(k)))) | g(g(m)) == b | p(g(g(m)),b). [resolve(293,c,39,a)]. given #526 (T,wt=22): 1159 m == k | b == k | k == b | p(k,b) | k == m | -(k == x) | p(x,f(k)). [resolve(449,f,17,b)]. given #527 (T,wt=22): 1205 m == k | b == k | g(g(g(g(g(g(m)))))) == g(g(g(g(g(g(g(k))))))). [resolve(713,c,20,a)]. given #528 (T,wt=22): 1206 m == k | b == k | f(g(g(g(g(g(m)))))) == f(g(g(g(g(g(g(k))))))). [resolve(713,c,19,a)]. given #529 (T,wt=22): 1218 m == k | b == k | g(f(g(g(g(g(m)))))) == g(f(g(g(g(g(g(k))))))). [resolve(714,c,20,a)]. given #530 (A,wt=25): 353 m == k | b == k | p(g(g(g(k))),g(g(g(m)))) | g(g(m)) == b | p(g(g(m)),b). [resolve(293,c,38,a)]. given #531 (T,wt=22): 1219 m == k | b == k | f(f(g(g(g(g(m)))))) == f(f(g(g(g(g(g(k))))))). [resolve(714,c,19,a)]. given #532 (T,wt=22): 1232 m == k | b == k | g(g(f(g(g(g(m)))))) == g(g(f(g(g(g(g(k))))))). [resolve(726,c,20,a)]. given #533 (T,wt=22): 1233 m == k | b == k | f(g(f(g(g(g(m)))))) == f(g(f(g(g(g(g(k))))))). [resolve(726,c,19,a)]. given #534 (T,wt=22): 1243 m == k | b == k | g(f(f(g(g(g(m)))))) == g(f(f(g(g(g(g(k))))))). [resolve(727,c,20,a)]. given #535 (A,wt=44): 359 m == k | b == k | f(g(m)) == b | p(f(g(m)),b) | f(g(m)) == m | g(f(g(m))) == m | g(f(g(m))) == f(g(m)) | p(f(g(g(k))),f(f(g(m)))). [resolve(294,c,107,f)]. given #536 (T,wt=22): 1244 m == k | b == k | f(f(f(g(g(g(m)))))) == f(f(f(g(g(g(g(k))))))). [resolve(727,c,19,a)]. given #537 (T,wt=22): 1259 m == k | b == k | g(g(g(f(g(g(m)))))) == g(g(g(f(g(g(g(k))))))). [resolve(740,c,20,a)]. given #538 (T,wt=22): 1260 m == k | b == k | f(g(g(f(g(g(m)))))) == f(g(g(f(g(g(g(k))))))). [resolve(740,c,19,a)]. given #539 (T,wt=22): 1272 m == k | b == k | g(f(g(f(g(g(m)))))) == g(f(g(f(g(g(g(k))))))). [resolve(741,c,20,a)]. given #540 (A,wt=36): 360 m == k | b == k | g(m) == b | p(g(m),b) | g(m) == m | g(g(m)) == m | g(g(m)) == g(m) | p(g(m),f(g(g(k)))). [resolve(294,c,106,f)]. given #541 (T,wt=22): 1273 m == k | b == k | f(f(g(f(g(g(m)))))) == f(f(g(f(g(g(g(k))))))). [resolve(741,c,19,a)]. given #542 (T,wt=22): 1286 m == k | b == k | g(g(f(f(g(g(m)))))) == g(g(f(f(g(g(g(k))))))). [resolve(756,c,20,a)]. given #543 (T,wt=22): 1287 m == k | b == k | f(g(f(f(g(g(m)))))) == f(g(f(f(g(g(g(k))))))). [resolve(756,c,19,a)]. given #544 (T,wt=22): 1297 m == k | b == k | g(f(f(f(g(g(m)))))) == g(f(f(f(g(g(g(k))))))). [resolve(757,c,20,a)]. given #545 (A,wt=36): 361 m == k | b == k | g(m) == b | p(g(m),b) | g(m) == m | g(g(m)) == m | g(g(m)) == g(m) | p(f(g(g(k))),g(m)). [resolve(294,c,102,f)]. given #546 (T,wt=22): 1298 m == k | b == k | f(f(f(f(g(g(m)))))) == f(f(f(f(g(g(g(k))))))). [resolve(757,c,19,a)]. given #547 (T,wt=22): 1311 m == k | b == k | g(g(g(g(f(g(m)))))) == g(g(g(g(f(g(g(k))))))). [resolve(770,c,20,a)]. given #548 (T,wt=22): 1312 m == k | b == k | f(g(g(g(f(g(m)))))) == f(g(g(g(f(g(g(k))))))). [resolve(770,c,19,a)]. given #549 (T,wt=22): 1324 m == k | b == k | g(f(g(g(f(g(m)))))) == g(f(g(g(f(g(g(k))))))). [resolve(771,c,20,a)]. given #550 (A,wt=44): 362 m == k | b == k | f(g(m)) == b | p(f(g(m)),b) | f(g(m)) == m | g(f(g(m))) == m | g(f(g(m))) == f(g(m)) | p(f(f(g(m))),f(g(g(k)))). [resolve(294,c,101,f)]. given #551 (T,wt=22): 1325 m == k | b == k | f(f(g(g(f(g(m)))))) == f(f(g(g(f(g(g(k))))))). [resolve(771,c,19,a)]. given #552 (T,wt=22): 1338 m == k | b == k | g(g(f(g(f(g(m)))))) == g(g(f(g(f(g(g(k))))))). [resolve(783,c,20,a)]. given #553 (T,wt=22): 1339 m == k | b == k | f(g(f(g(f(g(m)))))) == f(g(f(g(f(g(g(k))))))). [resolve(783,c,19,a)]. given #554 (T,wt=22): 1349 m == k | b == k | g(f(f(g(f(g(m)))))) == g(f(f(g(f(g(g(k))))))). [resolve(784,c,20,a)]. given #555 (A,wt=41): 363 m == k | b == k | f(g(m)) == b | p(f(g(m)),b) | f(g(m)) == m | g(f(g(m))) == m | g(f(g(m))) == f(g(m)) | p(f(g(g(k))),m). [resolve(294,c,86,f)]. given #556 (T,wt=22): 1350 m == k | b == k | f(f(f(g(f(g(m)))))) == f(f(f(g(f(g(g(k))))))). [resolve(784,c,19,a)]. given #557 (T,wt=22): 1366 m == k | b == k | g(g(g(f(f(g(m)))))) == g(g(g(f(f(g(g(k))))))). [resolve(797,c,20,a)]. given #558 (T,wt=22): 1367 m == k | b == k | f(g(g(f(f(g(m)))))) == f(g(g(f(f(g(g(k))))))). [resolve(797,c,19,a)]. given #559 (T,wt=22): 1379 m == k | b == k | g(f(g(f(f(g(m)))))) == g(f(g(f(f(g(g(k))))))). [resolve(798,c,20,a)]. given #560 (A,wt=25): 366 m == k | b == k | p(g(f(g(m))),f(g(g(k)))) | f(g(m)) == b | p(f(g(m)),b). [resolve(294,c,39,a)]. given #561 (T,wt=22): 1380 m == k | b == k | f(f(g(f(f(g(m)))))) == f(f(g(f(f(g(g(k))))))). [resolve(798,c,19,a)]. given #562 (T,wt=22): 1393 m == k | b == k | g(g(f(f(f(g(m)))))) == g(g(f(f(f(g(g(k))))))). [resolve(808,c,20,a)]. given #563 (T,wt=22): 1394 m == k | b == k | f(g(f(f(f(g(m)))))) == f(g(f(f(f(g(g(k))))))). [resolve(808,c,19,a)]. given #564 (T,wt=22): 1404 m == k | b == k | g(f(f(f(f(g(m)))))) == g(f(f(f(f(g(g(k))))))). [resolve(809,c,20,a)]. given #565 (A,wt=25): 367 m == k | b == k | p(f(g(g(k))),g(f(g(m)))) | f(g(m)) == b | p(f(g(m)),b). [resolve(294,c,38,a)]. given #566 (T,wt=22): 1405 m == k | b == k | f(f(f(f(f(g(m)))))) == f(f(f(f(f(g(g(k))))))). [resolve(809,c,19,a)]. given #567 (T,wt=22): 1422 m == k | b == k | g(g(g(g(g(f(m)))))) == g(g(g(g(g(f(g(k))))))). [resolve(822,c,20,a)]. given #568 (T,wt=22): 1423 m == k | b == k | f(g(g(g(g(f(m)))))) == f(g(g(g(g(f(g(k))))))). [resolve(822,c,19,a)]. given #569 (T,wt=22): 1435 m == k | b == k | g(f(g(g(g(f(m)))))) == g(f(g(g(g(f(g(k))))))). [resolve(823,c,20,a)]. given #570 (A,wt=44): 372 m == k | b == k | g(f(m)) == b | p(g(f(m)),b) | g(f(m)) == m | g(g(f(m))) == m | g(g(f(m))) == g(f(m)) | p(g(f(g(k))),f(g(f(m)))). [resolve(302,c,107,f)]. given #571 (T,wt=22): 1436 m == k | b == k | f(f(g(g(g(f(m)))))) == f(f(g(g(g(f(g(k))))))). [resolve(823,c,19,a)]. given #572 (T,wt=22): 1449 m == k | b == k | g(g(f(g(g(f(m)))))) == g(g(f(g(g(f(g(k))))))). [resolve(835,c,20,a)]. given #573 (T,wt=22): 1450 m == k | b == k | f(g(f(g(g(f(m)))))) == f(g(f(g(g(f(g(k))))))). [resolve(835,c,19,a)]. given #574 (T,wt=22): 1460 m == k | b == k | g(f(f(g(g(f(m)))))) == g(f(f(g(g(f(g(k))))))). [resolve(836,c,20,a)]. given #575 (A,wt=44): 373 m == k | b == k | g(f(m)) == b | p(g(f(m)),b) | g(f(m)) == m | g(g(f(m))) == m | g(g(f(m))) == g(f(m)) | p(f(g(f(m))),g(f(g(k)))). [resolve(302,c,101,f)]. given #576 (T,wt=22): 1461 m == k | b == k | f(f(f(g(g(f(m)))))) == f(f(f(g(g(f(g(k))))))). [resolve(836,c,19,a)]. given #577 (T,wt=22): 1474 m == k | b == k | g(g(g(f(g(f(m)))))) == g(g(g(f(g(f(g(k))))))). [resolve(849,c,20,a)]. given #578 (T,wt=22): 1475 m == k | b == k | f(g(g(f(g(f(m)))))) == f(g(g(f(g(f(g(k))))))). [resolve(849,c,19,a)]. given #579 (T,wt=22): 1487 m == k | b == k | g(f(g(f(g(f(m)))))) == g(f(g(f(g(f(g(k))))))). [resolve(850,c,20,a)]. given #580 (A,wt=35): 374 m == k | b == k | f(m) == b | p(f(m),b) | g(f(m)) == m | f(m) == m | f(m) == g(f(m)) | p(g(f(g(k))),m). [resolve(302,c,93,f)]. given #581 (T,wt=22): 1488 m == k | b == k | f(f(g(f(g(f(m)))))) == f(f(g(f(g(f(g(k))))))). [resolve(850,c,19,a)]. given #582 (T,wt=22): 1501 m == k | b == k | g(g(f(f(g(f(m)))))) == g(g(f(f(g(f(g(k))))))). [resolve(860,c,20,a)]. given #583 (T,wt=22): 1502 m == k | b == k | f(g(f(f(g(f(m)))))) == f(g(f(f(g(f(g(k))))))). [resolve(860,c,19,a)]. given #584 (T,wt=22): 1512 m == k | b == k | g(f(f(f(g(f(m)))))) == g(f(f(f(g(f(g(k))))))). [resolve(861,c,20,a)]. given #585 (A,wt=41): 375 m == k | b == k | g(f(m)) == b | p(g(f(m)),b) | g(f(m)) == m | g(g(f(m))) == m | g(g(f(m))) == g(f(m)) | p(g(f(g(k))),m). [resolve(302,c,86,f)]. given #586 (T,wt=22): 1513 m == k | b == k | f(f(f(f(g(f(m)))))) == f(f(f(f(g(f(g(k))))))). [resolve(861,c,19,a)]. given #587 (T,wt=22): 1528 m == k | b == k | g(g(g(g(f(f(m)))))) == g(g(g(g(f(f(g(k))))))). [resolve(874,c,20,a)]. given #588 (T,wt=22): 1529 m == k | b == k | f(g(g(g(f(f(m)))))) == f(g(g(g(f(f(g(k))))))). [resolve(874,c,19,a)]. given #589 (T,wt=22): 1541 m == k | b == k | g(f(g(g(f(f(m)))))) == g(f(g(g(f(f(g(k))))))). [resolve(875,c,20,a)]. given #590 (A,wt=25): 377 m == k | b == k | p(g(g(f(m))),g(f(g(k)))) | g(f(m)) == b | p(g(f(m)),b). [resolve(302,c,39,a)]. given #591 (T,wt=22): 1542 m == k | b == k | f(f(g(g(f(f(m)))))) == f(f(g(g(f(f(g(k))))))). [resolve(875,c,19,a)]. given #592 (T,wt=22): 1555 m == k | b == k | g(g(f(g(f(f(m)))))) == g(g(f(g(f(f(g(k))))))). [resolve(887,c,20,a)]. given #593 (T,wt=22): 1556 m == k | b == k | f(g(f(g(f(f(m)))))) == f(g(f(g(f(f(g(k))))))). [resolve(887,c,19,a)]. given #594 (T,wt=22): 1566 m == k | b == k | g(f(f(g(f(f(m)))))) == g(f(f(g(f(f(g(k))))))). [resolve(888,c,20,a)]. given #595 (A,wt=25): 378 m == k | b == k | p(g(f(g(k))),g(g(f(m)))) | g(f(m)) == b | p(g(f(m)),b). [resolve(302,c,38,a)]. given #596 (T,wt=22): 1567 m == k | b == k | f(f(f(g(f(f(m)))))) == f(f(f(g(f(f(g(k))))))). [resolve(888,c,19,a)]. given #597 (T,wt=22): 1587 m == k | b == k | g(g(g(f(f(f(m)))))) == g(g(g(f(f(f(g(k))))))). [resolve(901,c,20,a)]. given #598 (T,wt=22): 1588 m == k | b == k | f(g(g(f(f(f(m)))))) == f(g(g(f(f(f(g(k))))))). [resolve(901,c,19,a)]. given #599 (T,wt=22): 1600 m == k | b == k | g(f(g(f(f(f(m)))))) == g(f(g(f(f(f(g(k))))))). [resolve(902,c,20,a)]. given #600 (A,wt=44): 384 m == k | b == k | f(f(m)) == b | p(f(f(m)),b) | f(f(m)) == m | g(f(f(m))) == m | g(f(f(m))) == f(f(m)) | p(f(f(g(k))),f(f(f(m)))). [resolve(303,c,107,f)]. given #601 (T,wt=22): 1601 m == k | b == k | f(f(g(f(f(f(m)))))) == f(f(g(f(f(f(g(k))))))). [resolve(902,c,19,a)]. given #602 (T,wt=22): 1614 m == k | b == k | g(g(f(f(f(f(m)))))) == g(g(f(f(f(f(g(k))))))). [resolve(912,c,20,a)]. given #603 (T,wt=22): 1615 m == k | b == k | f(g(f(f(f(f(m)))))) == f(g(f(f(f(f(g(k))))))). [resolve(912,c,19,a)]. given #604 (T,wt=22): 1625 m == k | b == k | g(f(f(f(f(f(m)))))) == g(f(f(f(f(f(g(k))))))). [resolve(913,c,20,a)]. given #605 (A,wt=36): 385 m == k | b == k | f(m) == b | p(f(m),b) | f(m) == m | g(f(m)) == m | g(f(m)) == f(m) | p(f(m),f(f(g(k)))). [resolve(303,c,106,f)]. given #606 (T,wt=22): 1626 m == k | b == k | f(f(f(f(f(f(m)))))) == f(f(f(f(f(f(g(k))))))). [resolve(913,c,19,a)]. given #607 (T,wt=22): 1644 m == k | b == k | g(g(g(g(g(g(g(k))))))) == g(g(g(g(g(g(m)))))). [resolve(926,c,20,a)]. given #608 (T,wt=22): 1645 m == k | b == k | f(g(g(g(g(g(g(k))))))) == f(g(g(g(g(g(m)))))). [resolve(926,c,19,a)]. given #609 (T,wt=22): 1657 m == k | b == k | g(f(g(g(g(g(g(k))))))) == g(f(g(g(g(g(m)))))). [resolve(927,c,20,a)]. given #610 (A,wt=36): 386 m == k | b == k | f(m) == b | p(f(m),b) | f(m) == m | g(f(m)) == m | g(f(m)) == f(m) | p(f(f(g(k))),f(m)). [resolve(303,c,102,f)]. given #611 (T,wt=22): 1658 m == k | b == k | f(f(g(g(g(g(g(k))))))) == f(f(g(g(g(g(m)))))). [resolve(927,c,19,a)]. given #612 (T,wt=22): 1671 m == k | b == k | g(g(f(g(g(g(g(k))))))) == g(g(f(g(g(g(m)))))). [resolve(939,c,20,a)]. given #613 (T,wt=22): 1672 m == k | b == k | f(g(f(g(g(g(g(k))))))) == f(g(f(g(g(g(m)))))). [resolve(939,c,19,a)]. given #614 (T,wt=22): 1682 m == k | b == k | g(f(f(g(g(g(g(k))))))) == g(f(f(g(g(g(m)))))). [resolve(940,c,20,a)]. given #615 (A,wt=44): 387 m == k | b == k | f(f(m)) == b | p(f(f(m)),b) | f(f(m)) == m | g(f(f(m))) == m | g(f(f(m))) == f(f(m)) | p(f(f(f(m))),f(f(g(k)))). [resolve(303,c,101,f)]. given #616 (T,wt=22): 1683 m == k | b == k | f(f(f(g(g(g(g(k))))))) == f(f(f(g(g(g(m)))))). [resolve(940,c,19,a)]. given #617 (T,wt=22): 1701 m == k | b == k | g(g(g(f(g(g(g(k))))))) == g(g(g(f(g(g(m)))))). [resolve(953,c,20,a)]. given #618 (T,wt=22): 1702 m == k | b == k | f(g(g(f(g(g(g(k))))))) == f(g(g(f(g(g(m)))))). [resolve(953,c,19,a)]. given #619 (T,wt=22): 1714 m == k | b == k | g(f(g(f(g(g(g(k))))))) == g(f(g(f(g(g(m)))))). [resolve(954,c,20,a)]. given #620 (A,wt=41): 388 m == k | b == k | f(f(m)) == b | p(f(f(m)),b) | f(f(m)) == m | g(f(f(m))) == m | g(f(f(m))) == f(f(m)) | p(f(f(g(k))),m). [resolve(303,c,86,f)]. given #621 (T,wt=22): 1715 m == k | b == k | f(f(g(f(g(g(g(k))))))) == f(f(g(f(g(g(m)))))). [resolve(954,c,19,a)]. given #622 (T,wt=22): 1728 m == k | b == k | g(g(f(f(g(g(g(k))))))) == g(g(f(f(g(g(m)))))). [resolve(964,c,20,a)]. given #623 (T,wt=22): 1729 m == k | b == k | f(g(f(f(g(g(g(k))))))) == f(g(f(f(g(g(m)))))). [resolve(964,c,19,a)]. given #624 (T,wt=22): 1739 m == k | b == k | g(f(f(f(g(g(g(k))))))) == g(f(f(f(g(g(m)))))). [resolve(965,c,20,a)]. given #625 (A,wt=25): 389 m == k | b == k | p(g(f(f(m))),f(f(g(k)))) | f(f(m)) == b | p(f(f(m)),b). [resolve(303,c,39,a)]. given #626 (T,wt=22): 1740 m == k | b == k | f(f(f(f(g(g(g(k))))))) == f(f(f(f(g(g(m)))))). [resolve(965,c,19,a)]. given #627 (T,wt=22): 1761 m == k | b == k | g(g(g(g(f(g(g(k))))))) == g(g(g(g(f(g(m)))))). [resolve(978,c,20,a)]. given #628 (T,wt=22): 1762 m == k | b == k | f(g(g(g(f(g(g(k))))))) == f(g(g(g(f(g(m)))))). [resolve(978,c,19,a)]. given #629 (T,wt=22): 1774 m == k | b == k | g(f(g(g(f(g(g(k))))))) == g(f(g(g(f(g(m)))))). [resolve(979,c,20,a)]. given #630 (A,wt=25): 390 m == k | b == k | p(f(f(g(k))),g(f(f(m)))) | f(f(m)) == b | p(f(f(m)),b). [resolve(303,c,38,a)]. given #631 (T,wt=22): 1775 m == k | b == k | f(f(g(g(f(g(g(k))))))) == f(f(g(g(f(g(m)))))). [resolve(979,c,19,a)]. given #632 (T,wt=22): 1788 m == k | b == k | g(g(f(g(f(g(g(k))))))) == g(g(f(g(f(g(m)))))). [resolve(991,c,20,a)]. given #633 (T,wt=22): 1789 m == k | b == k | f(g(f(g(f(g(g(k))))))) == f(g(f(g(f(g(m)))))). [resolve(991,c,19,a)]. given #634 (T,wt=22): 1799 m == k | b == k | g(f(f(g(f(g(g(k))))))) == g(f(f(g(f(g(m)))))). [resolve(992,c,20,a)]. given #635 (A,wt=50): 395 m == k | b == k | g(g(g(k))) == b | p(g(g(g(k))),b) | g(g(g(k))) == m | g(g(g(g(k)))) == m | g(g(g(g(k)))) == g(g(g(k))) | p(g(g(m)),f(g(g(g(k))))). [resolve(313,c,107,f)]. given #636 (T,wt=22): 1800 m == k | b == k | f(f(f(g(f(g(g(k))))))) == f(f(f(g(f(g(m)))))). [resolve(992,c,19,a)]. given #637 (T,wt=22): 1819 m == k | b == k | g(g(g(f(f(g(g(k))))))) == g(g(g(f(f(g(m)))))). [resolve(1005,c,20,a)]. given #638 (T,wt=22): 1820 m == k | b == k | f(g(g(f(f(g(g(k))))))) == f(g(g(f(f(g(m)))))). [resolve(1005,c,19,a)]. given #639 (T,wt=22): 1832 m == k | b == k | g(f(g(f(f(g(g(k))))))) == g(f(g(f(f(g(m)))))). [resolve(1006,c,20,a)]. given #640 (A,wt=50): 396 m == k | b == k | g(g(g(k))) == b | p(g(g(g(k))),b) | g(g(g(k))) == m | g(g(g(g(k)))) == m | g(g(g(g(k)))) == g(g(g(k))) | p(f(g(g(g(k)))),g(g(m))). [resolve(313,c,101,f)]. given #641 (T,wt=22): 1833 m == k | b == k | f(f(g(f(f(g(g(k))))))) == f(f(g(f(f(g(m)))))). [resolve(1006,c,19,a)]. given #642 (T,wt=22): 1846 m == k | b == k | g(g(f(f(f(g(g(k))))))) == g(g(f(f(f(g(m)))))). [resolve(1016,c,20,a)]. given #643 (T,wt=22): 1847 m == k | b == k | f(g(f(f(f(g(g(k))))))) == f(g(f(f(f(g(m)))))). [resolve(1016,c,19,a)]. given #644 (T,wt=22): 1857 m == k | b == k | g(f(f(f(f(g(g(k))))))) == g(f(f(f(f(g(m)))))). [resolve(1017,c,20,a)]. given #645 (A,wt=40): 397 m == k | b == k | g(g(k)) == b | p(g(g(k)),b) | g(g(g(k))) == m | g(g(k)) == m | g(g(k)) == g(g(g(k))) | p(g(g(m)),m). [resolve(313,c,93,f)]. given #646 (T,wt=22): 1858 m == k | b == k | f(f(f(f(f(g(g(k))))))) == f(f(f(f(f(g(m)))))). [resolve(1017,c,19,a)]. given #647 (T,wt=22): 1877 m == k | b == k | g(g(g(g(g(f(g(k))))))) == g(g(g(g(g(f(m)))))). [resolve(1030,c,20,a)]. given #648 (T,wt=22): 1878 m == k | b == k | f(g(g(g(g(f(g(k))))))) == f(g(g(g(g(f(m)))))). [resolve(1030,c,19,a)]. given #649 (T,wt=22): 1890 m == k | b == k | g(f(g(g(g(f(g(k))))))) == g(f(g(g(g(f(m)))))). [resolve(1031,c,20,a)]. given #650 (A,wt=46): 398 m == k | b == k | g(g(g(k))) == b | p(g(g(g(k))),b) | g(g(g(k))) == m | g(g(g(g(k)))) == m | g(g(g(g(k)))) == g(g(g(k))) | p(g(g(m)),m). [resolve(313,c,86,f)]. given #651 (T,wt=22): 1891 m == k | b == k | f(f(g(g(g(f(g(k))))))) == f(f(g(g(g(f(m)))))). [resolve(1031,c,19,a)]. given #652 (T,wt=22): 1904 m == k | b == k | g(g(f(g(g(f(g(k))))))) == g(g(f(g(g(f(m)))))). [resolve(1043,c,20,a)]. given #653 (T,wt=22): 1905 m == k | b == k | f(g(f(g(g(f(g(k))))))) == f(g(f(g(g(f(m)))))). [resolve(1043,c,19,a)]. given #654 (T,wt=22): 1915 m == k | b == k | g(f(f(g(g(f(g(k))))))) == g(f(f(g(g(f(m)))))). [resolve(1044,c,20,a)]. given #655 (A,wt=23): 399 m == k | b == k | p(g(g(k)),g(g(m))) | g(g(k)) == b | p(g(g(k)),b). [resolve(313,c,40,a)]. given #656 (T,wt=21): 3737 m == k | b == k | g(g(k)) == b | p(g(g(k)),b) | -(g(g(m)) == b). [factor(3732,d,f)]. given #657 (T,wt=22): 1916 m == k | b == k | f(f(f(g(g(f(g(k))))))) == f(f(f(g(g(f(m)))))). [resolve(1044,c,19,a)]. given #658 (T,wt=22): 1934 m == k | b == k | g(g(g(f(g(f(g(k))))))) == g(g(g(f(g(f(m)))))). [resolve(1057,c,20,a)]. given #659 (T,wt=22): 1935 m == k | b == k | f(g(g(f(g(f(g(k))))))) == f(g(g(f(g(f(m)))))). [resolve(1057,c,19,a)]. given #660 (A,wt=27): 400 m == k | b == k | p(g(g(g(g(k)))),g(g(m))) | g(g(g(k))) == b | p(g(g(g(k))),b). [resolve(313,c,39,a)]. given #661 (T,wt=22): 1947 m == k | b == k | g(f(g(f(g(f(g(k))))))) == g(f(g(f(g(f(m)))))). [resolve(1058,c,20,a)]. given #662 (T,wt=22): 1948 m == k | b == k | f(f(g(f(g(f(g(k))))))) == f(f(g(f(g(f(m)))))). [resolve(1058,c,19,a)]. given #663 (T,wt=22): 1961 m == k | b == k | g(g(f(f(g(f(g(k))))))) == g(g(f(f(g(f(m)))))). [resolve(1074,c,20,a)]. given #664 (T,wt=22): 1962 m == k | b == k | f(g(f(f(g(f(g(k))))))) == f(g(f(f(g(f(m)))))). [resolve(1074,c,19,a)]. given #665 (A,wt=27): 401 m == k | b == k | p(g(g(m)),g(g(g(g(k))))) | g(g(g(k))) == b | p(g(g(g(k))),b). [resolve(313,c,38,a)]. given #666 (T,wt=22): 1972 m == k | b == k | g(f(f(f(g(f(g(k))))))) == g(f(f(f(g(f(m)))))). [resolve(1075,c,20,a)]. given #667 (T,wt=22): 1973 m == k | b == k | f(f(f(f(g(f(g(k))))))) == f(f(f(f(g(f(m)))))). [resolve(1075,c,19,a)]. given #668 (T,wt=22): 1991 m == k | b == k | g(g(g(g(f(f(g(k))))))) == g(g(g(g(f(f(m)))))). [resolve(1088,c,20,a)]. given #669 (T,wt=22): 1992 m == k | b == k | f(g(g(g(f(f(g(k))))))) == f(g(g(g(f(f(m)))))). [resolve(1088,c,19,a)]. given #670 (A,wt=23): 402 m == k | b == k | p(g(g(m)),g(g(k))) | g(g(k)) == b | p(g(g(k)),b). [resolve(313,c,37,a)]. given #671 (T,wt=22): 2004 m == k | b == k | g(f(g(g(f(f(g(k))))))) == g(f(g(g(f(f(m)))))). [resolve(1089,c,20,a)]. given #672 (T,wt=22): 2005 m == k | b == k | f(f(g(g(f(f(g(k))))))) == f(f(g(g(f(f(m)))))). [resolve(1089,c,19,a)]. given #673 (T,wt=22): 2018 m == k | b == k | g(g(f(g(f(f(g(k))))))) == g(g(f(g(f(f(m)))))). [resolve(1101,c,20,a)]. given #674 (T,wt=22): 2019 m == k | b == k | f(g(f(g(f(f(g(k))))))) == f(g(f(g(f(f(m)))))). [resolve(1101,c,19,a)]. given #675 (A,wt=50): 407 m == k | b == k | f(g(g(k))) == b | p(f(g(g(k))),b) | f(g(g(k))) == m | g(f(g(g(k)))) == m | g(f(g(g(k)))) == f(g(g(k))) | p(f(g(m)),f(f(g(g(k))))). [resolve(314,c,107,f)]. given #676 (T,wt=22): 2029 m == k | b == k | g(f(f(g(f(f(g(k))))))) == g(f(f(g(f(f(m)))))). [resolve(1102,c,20,a)]. given #677 (T,wt=22): 2030 m == k | b == k | f(f(f(g(f(f(g(k))))))) == f(f(f(g(f(f(m)))))). [resolve(1102,c,19,a)]. given #678 (T,wt=22): 2051 m == k | b == k | g(g(g(f(f(f(g(k))))))) == g(g(g(f(f(f(m)))))). [resolve(1115,c,20,a)]. given #679 (T,wt=22): 2052 m == k | b == k | f(g(g(f(f(f(g(k))))))) == f(g(g(f(f(f(m)))))). [resolve(1115,c,19,a)]. given #680 (A,wt=42): 408 m == k | b == k | g(g(k)) == b | p(g(g(k)),b) | g(g(k)) == m | g(g(g(k))) == m | g(g(g(k))) == g(g(k)) | p(g(g(k)),f(g(m))). [resolve(314,c,106,f)]. given #681 (T,wt=22): 2064 m == k | b == k | g(f(g(f(f(f(g(k))))))) == g(f(g(f(f(f(m)))))). [resolve(1116,c,20,a)]. given #682 (T,wt=22): 2065 m == k | b == k | f(f(g(f(f(f(g(k))))))) == f(f(g(f(f(f(m)))))). [resolve(1116,c,19,a)]. given #683 (T,wt=22): 2078 m == k | b == k | g(g(f(f(f(f(g(k))))))) == g(g(f(f(f(f(m)))))). [resolve(1129,c,20,a)]. given #684 (T,wt=22): 2079 m == k | b == k | f(g(f(f(f(f(g(k))))))) == f(g(f(f(f(f(m)))))). [resolve(1129,c,19,a)]. given #685 (A,wt=42): 409 m == k | b == k | g(g(k)) == b | p(g(g(k)),b) | g(g(k)) == m | g(g(g(k))) == m | g(g(g(k))) == g(g(k)) | p(f(g(m)),g(g(k))). [resolve(314,c,102,f)]. given #686 (T,wt=22): 2089 m == k | b == k | g(f(f(f(f(f(g(k))))))) == g(f(f(f(f(f(m)))))). [resolve(1130,c,20,a)]. given #687 (T,wt=22): 2090 m == k | b == k | f(f(f(f(f(f(g(k))))))) == f(f(f(f(f(f(m)))))). [resolve(1130,c,19,a)]. given #688 (T,wt=23): 422 m == k | b == k | p(f(g(k)),g(f(m))) | f(g(k)) == b | p(f(g(k)),b). [resolve(324,c,40,a)]. given #689 (T,wt=21): 4103 m == k | b == k | f(g(k)) == b | p(f(g(k)),b) | -(g(f(m)) == b). [factor(4098,d,f)]. given #690 (A,wt=50): 410 m == k | b == k | f(g(g(k))) == b | p(f(g(g(k))),b) | f(g(g(k))) == m | g(f(g(g(k)))) == m | g(f(g(g(k)))) == f(g(g(k))) | p(f(f(g(g(k)))),f(g(m))). [resolve(314,c,101,f)]. given #691 (T,wt=23): 425 m == k | b == k | p(g(f(m)),f(g(k))) | f(g(k)) == b | p(f(g(k)),b). [resolve(324,c,37,a)]. given #692 (T,wt=23): 1175 m == k | b == k | p(m,b) | g(m) == m | -(f(g(m)) == x) | p(g(g(k)),x). [resolve(287,e,18,b)]. given #693 (T,wt=21): 4114 m == k | b == k | p(m,b) | g(m) == m | p(g(g(k)),f(g(g(k)))). [resolve(1175,e,294,c),merge(f),merge(g)]. given #694 (T,wt=23): 1176 m == k | b == k | p(m,b) | g(m) == m | -(g(g(k)) == x) | p(x,f(g(m))). [resolve(287,e,17,b)]. given #695 (A,wt=46): 411 m == k | b == k | f(g(g(k))) == b | p(f(g(g(k))),b) | f(g(g(k))) == m | g(f(g(g(k)))) == m | g(f(g(g(k)))) == f(g(g(k))) | p(f(g(m)),m). [resolve(314,c,86,f)]. given #696 (T,wt=23): 1180 m == k | b == k | p(m,b) | g(m) == m | -(g(g(k)) == x) | p(f(g(m)),x). [resolve(288,e,18,b)]. given #697 (T,wt=23): 1181 m == k | b == k | p(m,b) | g(m) == m | -(f(g(m)) == x) | p(x,g(g(k))). [resolve(288,e,17,b)]. given #698 (T,wt=21): 4126 m == k | b == k | p(m,b) | g(m) == m | p(f(g(g(k))),g(g(k))). [resolve(1181,e,294,c),merge(f),merge(g)]. given #699 (T,wt=23): 1185 m == k | b == k | p(m,b) | g(m) == m | -(f(g(g(k))) == x) | p(g(m),x). [resolve(364,e,18,b)]. given #700 (A,wt=27): 412 m == k | b == k | p(g(f(g(g(k)))),f(g(m))) | f(g(g(k))) == b | p(f(g(g(k))),b). [resolve(314,c,39,a)]. given #701 (T,wt=23): 1186 m == k | b == k | p(m,b) | g(m) == m | -(g(m) == x) | p(x,f(g(g(k)))). [resolve(364,e,17,b)]. given #702 (T,wt=23): 1190 m == k | b == k | p(m,b) | g(m) == m | -(g(m) == x) | p(f(g(g(k))),x). [resolve(365,e,18,b)]. given #703 (T,wt=23): 1191 m == k | b == k | p(m,b) | g(m) == m | -(f(g(g(k))) == x) | p(x,g(m)). [resolve(365,e,17,b)]. given #704 (T,wt=23): 1207 m == k | b == k | -(x == g(g(g(g(g(m)))))) | x == g(g(g(g(g(g(k)))))). [resolve(713,c,16,b)]. given #705 (A,wt=27): 413 m == k | b == k | p(f(g(m)),g(f(g(g(k))))) | f(g(g(k))) == b | p(f(g(g(k))),b). [resolve(314,c,38,a)]. given #706 (T,wt=23): 1208 m == k | b == k | -(g(g(g(g(g(g(k)))))) == x) | g(g(g(g(g(m))))) == x. [resolve(713,c,16,a)]. given #707 (T,wt=23): 1220 m == k | b == k | -(x == f(g(g(g(g(m)))))) | x == f(g(g(g(g(g(k)))))). [resolve(714,c,16,b)]. given #708 (T,wt=23): 1221 m == k | b == k | -(f(g(g(g(g(g(k)))))) == x) | f(g(g(g(g(m))))) == x. [resolve(714,c,16,a)]. given #709 (T,wt=23): 1234 m == k | b == k | -(x == g(f(g(g(g(m)))))) | x == g(f(g(g(g(g(k)))))). [resolve(726,c,16,b)]. given #710 (A,wt=50): 418 m == k | b == k | g(f(g(k))) == b | p(g(f(g(k))),b) | g(f(g(k))) == m | g(g(f(g(k)))) == m | g(g(f(g(k)))) == g(f(g(k))) | p(g(f(m)),f(g(f(g(k))))). [resolve(324,c,107,f)]. given #711 (T,wt=23): 1235 m == k | b == k | -(g(f(g(g(g(g(k)))))) == x) | g(f(g(g(g(m))))) == x. [resolve(726,c,16,a)]. given #712 (T,wt=23): 1245 m == k | b == k | -(x == f(f(g(g(g(m)))))) | x == f(f(g(g(g(g(k)))))). [resolve(727,c,16,b)]. given #713 (T,wt=23): 1246 m == k | b == k | -(f(f(g(g(g(g(k)))))) == x) | f(f(g(g(g(m))))) == x. [resolve(727,c,16,a)]. given #714 (T,wt=23): 1261 m == k | b == k | -(x == g(g(f(g(g(m)))))) | x == g(g(f(g(g(g(k)))))). [resolve(740,c,16,b)]. given #715 (A,wt=50): 419 m == k | b == k | g(f(g(k))) == b | p(g(f(g(k))),b) | g(f(g(k))) == m | g(g(f(g(k)))) == m | g(g(f(g(k)))) == g(f(g(k))) | p(f(g(f(g(k)))),g(f(m))). [resolve(324,c,101,f)]. given #716 (T,wt=23): 1262 m == k | b == k | -(g(g(f(g(g(g(k)))))) == x) | g(g(f(g(g(m))))) == x. [resolve(740,c,16,a)]. given #717 (T,wt=23): 1274 m == k | b == k | -(x == f(g(f(g(g(m)))))) | x == f(g(f(g(g(g(k)))))). [resolve(741,c,16,b)]. given #718 (T,wt=23): 1275 m == k | b == k | -(f(g(f(g(g(g(k)))))) == x) | f(g(f(g(g(m))))) == x. [resolve(741,c,16,a)]. given #719 (T,wt=23): 1288 m == k | b == k | -(x == g(f(f(g(g(m)))))) | x == g(f(f(g(g(g(k)))))). [resolve(756,c,16,b)]. given #720 (A,wt=40): 420 m == k | b == k | f(g(k)) == b | p(f(g(k)),b) | g(f(g(k))) == m | f(g(k)) == m | f(g(k)) == g(f(g(k))) | p(g(f(m)),m). [resolve(324,c,93,f)]. given #721 (T,wt=23): 1289 m == k | b == k | -(g(f(f(g(g(g(k)))))) == x) | g(f(f(g(g(m))))) == x. [resolve(756,c,16,a)]. given #722 (T,wt=23): 1299 m == k | b == k | -(x == f(f(f(g(g(m)))))) | x == f(f(f(g(g(g(k)))))). [resolve(757,c,16,b)]. given #723 (T,wt=23): 1300 m == k | b == k | -(f(f(f(g(g(g(k)))))) == x) | f(f(f(g(g(m))))) == x. [resolve(757,c,16,a)]. given #724 (T,wt=23): 1313 m == k | b == k | -(x == g(g(g(f(g(m)))))) | x == g(g(g(f(g(g(k)))))). [resolve(770,c,16,b)]. given #725 (A,wt=46): 421 m == k | b == k | g(f(g(k))) == b | p(g(f(g(k))),b) | g(f(g(k))) == m | g(g(f(g(k)))) == m | g(g(f(g(k)))) == g(f(g(k))) | p(g(f(m)),m). [resolve(324,c,86,f)]. given #726 (T,wt=23): 1314 m == k | b == k | -(g(g(g(f(g(g(k)))))) == x) | g(g(g(f(g(m))))) == x. [resolve(770,c,16,a)]. given #727 (T,wt=23): 1326 m == k | b == k | -(x == f(g(g(f(g(m)))))) | x == f(g(g(f(g(g(k)))))). [resolve(771,c,16,b)]. given #728 (T,wt=23): 1327 m == k | b == k | -(f(g(g(f(g(g(k)))))) == x) | f(g(g(f(g(m))))) == x. [resolve(771,c,16,a)]. given #729 (T,wt=23): 1340 m == k | b == k | -(x == g(f(g(f(g(m)))))) | x == g(f(g(f(g(g(k)))))). [resolve(783,c,16,b)]. given #730 (A,wt=27): 423 m == k | b == k | p(g(g(f(g(k)))),g(f(m))) | g(f(g(k))) == b | p(g(f(g(k))),b). [resolve(324,c,39,a)]. given #731 (T,wt=23): 1341 m == k | b == k | -(g(f(g(f(g(g(k)))))) == x) | g(f(g(f(g(m))))) == x. [resolve(783,c,16,a)]. given #732 (T,wt=23): 1351 m == k | b == k | -(x == f(f(g(f(g(m)))))) | x == f(f(g(f(g(g(k)))))). [resolve(784,c,16,b)]. given #733 (T,wt=23): 1352 m == k | b == k | -(f(f(g(f(g(g(k)))))) == x) | f(f(g(f(g(m))))) == x. [resolve(784,c,16,a)]. given #734 (T,wt=23): 1368 m == k | b == k | -(x == g(g(f(f(g(m)))))) | x == g(g(f(f(g(g(k)))))). [resolve(797,c,16,b)]. given #735 (A,wt=27): 424 m == k | b == k | p(g(f(m)),g(g(f(g(k))))) | g(f(g(k))) == b | p(g(f(g(k))),b). [resolve(324,c,38,a)]. given #736 (T,wt=23): 1369 m == k | b == k | -(g(g(f(f(g(g(k)))))) == x) | g(g(f(f(g(m))))) == x. [resolve(797,c,16,a)]. given #737 (T,wt=23): 1381 m == k | b == k | -(x == f(g(f(f(g(m)))))) | x == f(g(f(f(g(g(k)))))). [resolve(798,c,16,b)]. given #738 (T,wt=23): 1382 m == k | b == k | -(f(g(f(f(g(g(k)))))) == x) | f(g(f(f(g(m))))) == x. [resolve(798,c,16,a)]. given #739 (T,wt=23): 1395 m == k | b == k | -(x == g(f(f(f(g(m)))))) | x == g(f(f(f(g(g(k)))))). [resolve(808,c,16,b)]. given #740 (A,wt=50): 430 m == k | b == k | f(f(g(k))) == b | p(f(f(g(k))),b) | f(f(g(k))) == m | g(f(f(g(k)))) == m | g(f(f(g(k)))) == f(f(g(k))) | p(f(f(m)),f(f(f(g(k))))). [resolve(325,c,107,f)]. given #741 (T,wt=23): 1396 m == k | b == k | -(g(f(f(f(g(g(k)))))) == x) | g(f(f(f(g(m))))) == x. [resolve(808,c,16,a)]. given #742 (T,wt=23): 1406 m == k | b == k | -(x == f(f(f(f(g(m)))))) | x == f(f(f(f(g(g(k)))))). [resolve(809,c,16,b)]. given #743 (T,wt=23): 1407 m == k | b == k | -(f(f(f(f(g(g(k)))))) == x) | f(f(f(f(g(m))))) == x. [resolve(809,c,16,a)]. given #744 (T,wt=23): 1424 m == k | b == k | -(x == g(g(g(g(f(m)))))) | x == g(g(g(g(f(g(k)))))). [resolve(822,c,16,b)]. given #745 (A,wt=42): 431 m == k | b == k | f(g(k)) == b | p(f(g(k)),b) | f(g(k)) == m | g(f(g(k))) == m | g(f(g(k))) == f(g(k)) | p(f(g(k)),f(f(m))). [resolve(325,c,106,f)]. given #746 (T,wt=23): 1425 m == k | b == k | -(g(g(g(g(f(g(k)))))) == x) | g(g(g(g(f(m))))) == x. [resolve(822,c,16,a)]. given #747 (T,wt=23): 1437 m == k | b == k | -(x == f(g(g(g(f(m)))))) | x == f(g(g(g(f(g(k)))))). [resolve(823,c,16,b)]. given #748 (T,wt=23): 1438 m == k | b == k | -(f(g(g(g(f(g(k)))))) == x) | f(g(g(g(f(m))))) == x. [resolve(823,c,16,a)]. given #749 (T,wt=23): 1451 m == k | b == k | -(x == g(f(g(g(f(m)))))) | x == g(f(g(g(f(g(k)))))). [resolve(835,c,16,b)]. given #750 (A,wt=42): 432 m == k | b == k | f(g(k)) == b | p(f(g(k)),b) | f(g(k)) == m | g(f(g(k))) == m | g(f(g(k))) == f(g(k)) | p(f(f(m)),f(g(k))). [resolve(325,c,102,f)]. given #751 (T,wt=23): 1452 m == k | b == k | -(g(f(g(g(f(g(k)))))) == x) | g(f(g(g(f(m))))) == x. [resolve(835,c,16,a)]. given #752 (T,wt=23): 1462 m == k | b == k | -(x == f(f(g(g(f(m)))))) | x == f(f(g(g(f(g(k)))))). [resolve(836,c,16,b)]. given #753 (T,wt=23): 1463 m == k | b == k | -(f(f(g(g(f(g(k)))))) == x) | f(f(g(g(f(m))))) == x. [resolve(836,c,16,a)]. given #754 (T,wt=23): 1476 m == k | b == k | -(x == g(g(f(g(f(m)))))) | x == g(g(f(g(f(g(k)))))). [resolve(849,c,16,b)]. given #755 (A,wt=50): 433 m == k | b == k | f(f(g(k))) == b | p(f(f(g(k))),b) | f(f(g(k))) == m | g(f(f(g(k)))) == m | g(f(f(g(k)))) == f(f(g(k))) | p(f(f(f(g(k)))),f(f(m))). [resolve(325,c,101,f)]. given #756 (T,wt=23): 1477 m == k | b == k | -(g(g(f(g(f(g(k)))))) == x) | g(g(f(g(f(m))))) == x. [resolve(849,c,16,a)]. given #757 (T,wt=23): 1489 m == k | b == k | -(x == f(g(f(g(f(m)))))) | x == f(g(f(g(f(g(k)))))). [resolve(850,c,16,b)]. given #758 (T,wt=23): 1490 m == k | b == k | -(f(g(f(g(f(g(k)))))) == x) | f(g(f(g(f(m))))) == x. [resolve(850,c,16,a)]. given #759 (T,wt=23): 1503 m == k | b == k | -(x == g(f(f(g(f(m)))))) | x == g(f(f(g(f(g(k)))))). [resolve(860,c,16,b)]. given #760 (A,wt=46): 434 m == k | b == k | f(f(g(k))) == b | p(f(f(g(k))),b) | f(f(g(k))) == m | g(f(f(g(k)))) == m | g(f(f(g(k)))) == f(f(g(k))) | p(f(f(m)),m). [resolve(325,c,86,f)]. given #761 (T,wt=23): 1504 m == k | b == k | -(g(f(f(g(f(g(k)))))) == x) | g(f(f(g(f(m))))) == x. [resolve(860,c,16,a)]. given #762 (T,wt=23): 1514 m == k | b == k | -(x == f(f(f(g(f(m)))))) | x == f(f(f(g(f(g(k)))))). [resolve(861,c,16,b)]. given #763 (T,wt=23): 1515 m == k | b == k | -(f(f(f(g(f(g(k)))))) == x) | f(f(f(g(f(m))))) == x. [resolve(861,c,16,a)]. given #764 (T,wt=23): 1530 m == k | b == k | -(x == g(g(g(f(f(m)))))) | x == g(g(g(f(f(g(k)))))). [resolve(874,c,16,b)]. given #765 (A,wt=27): 435 m == k | b == k | p(g(f(f(g(k)))),f(f(m))) | f(f(g(k))) == b | p(f(f(g(k))),b). [resolve(325,c,39,a)]. given #766 (T,wt=23): 1531 m == k | b == k | -(g(g(g(f(f(g(k)))))) == x) | g(g(g(f(f(m))))) == x. [resolve(874,c,16,a)]. given #767 (T,wt=23): 1543 m == k | b == k | -(x == f(g(g(f(f(m)))))) | x == f(g(g(f(f(g(k)))))). [resolve(875,c,16,b)]. given #768 (T,wt=23): 1544 m == k | b == k | -(f(g(g(f(f(g(k)))))) == x) | f(g(g(f(f(m))))) == x. [resolve(875,c,16,a)]. given #769 (T,wt=23): 1557 m == k | b == k | -(x == g(f(g(f(f(m)))))) | x == g(f(g(f(f(g(k)))))). [resolve(887,c,16,b)]. given #770 (A,wt=27): 436 m == k | b == k | p(f(f(m)),g(f(f(g(k))))) | f(f(g(k))) == b | p(f(f(g(k))),b). [resolve(325,c,38,a)]. given #771 (T,wt=23): 1558 m == k | b == k | -(g(f(g(f(f(g(k)))))) == x) | g(f(g(f(f(m))))) == x. [resolve(887,c,16,a)]. given #772 (T,wt=23): 1568 m == k | b == k | -(x == f(f(g(f(f(m)))))) | x == f(f(g(f(f(g(k)))))). [resolve(888,c,16,b)]. given #773 (T,wt=23): 1569 m == k | b == k | -(f(f(g(f(f(g(k)))))) == x) | f(f(g(f(f(m))))) == x. [resolve(888,c,16,a)]. given #774 (T,wt=23): 1589 m == k | b == k | -(x == g(g(f(f(f(m)))))) | x == g(g(f(f(f(g(k)))))). [resolve(901,c,16,b)]. given #775 (A,wt=44): 441 f(g(k)) == b | p(f(g(k)),b) | g(f(g(k))) == m | f(g(k)) == m | f(g(k)) == g(f(g(k))) | p(f(g(f(g(k)))),g(f(m))) | m == k | b == k. [resolve(120,f,324,c)]. given #776 (T,wt=23): 1590 m == k | b == k | -(g(g(f(f(f(g(k)))))) == x) | g(g(f(f(f(m))))) == x. [resolve(901,c,16,a)]. given #777 (T,wt=23): 1602 m == k | b == k | -(x == f(g(f(f(f(m)))))) | x == f(g(f(f(f(g(k)))))). [resolve(902,c,16,b)]. given #778 (T,wt=23): 1603 m == k | b == k | -(f(g(f(f(f(g(k)))))) == x) | f(g(f(f(f(m))))) == x. [resolve(902,c,16,a)]. given #779 (T,wt=23): 1616 m == k | b == k | -(x == g(f(f(f(f(m)))))) | x == g(f(f(f(f(g(k)))))). [resolve(912,c,16,b)]. given #780 (A,wt=44): 442 g(g(k)) == b | p(g(g(k)),b) | g(g(g(k))) == m | g(g(k)) == m | g(g(k)) == g(g(g(k))) | p(f(g(g(g(k)))),g(g(m))) | m == k | b == k. [resolve(120,f,313,c)]. given #781 (T,wt=23): 1617 m == k | b == k | -(g(f(f(f(f(g(k)))))) == x) | g(f(f(f(f(m))))) == x. [resolve(912,c,16,a)]. given #782 (T,wt=23): 1627 m == k | b == k | -(x == f(f(f(f(f(m)))))) | x == f(f(f(f(f(g(k)))))). [resolve(913,c,16,b)]. given #783 (T,wt=23): 1628 m == k | b == k | -(f(f(f(f(f(g(k)))))) == x) | f(f(f(f(f(m))))) == x. [resolve(913,c,16,a)]. given #784 (T,wt=23): 1646 m == k | b == k | -(x == g(g(g(g(g(g(k))))))) | x == g(g(g(g(g(m))))). [resolve(926,c,16,b)]. given #785 (A,wt=38): 443 f(m) == b | p(f(m),b) | g(f(m)) == m | f(m) == m | f(m) == g(f(m)) | p(f(g(f(m))),g(f(g(k)))) | m == k | b == k. [resolve(120,f,302,c)]. given #786 (T,wt=23): 1647 m == k | b == k | -(g(g(g(g(g(m))))) == x) | g(g(g(g(g(g(k)))))) == x. [resolve(926,c,16,a)]. given #787 (T,wt=23): 1659 m == k | b == k | -(x == f(g(g(g(g(g(k))))))) | x == f(g(g(g(g(m))))). [resolve(927,c,16,b)]. given #788 (T,wt=23): 1660 m == k | b == k | -(f(g(g(g(g(m))))) == x) | f(g(g(g(g(g(k)))))) == x. [resolve(927,c,16,a)]. given #789 (T,wt=23): 1673 m == k | b == k | -(x == g(f(g(g(g(g(k))))))) | x == g(f(g(g(g(m))))). [resolve(939,c,16,b)]. given #790 (A,wt=38): 444 g(m) == b | p(g(m),b) | g(g(m)) == m | g(m) == m | g(m) == g(g(m)) | p(f(g(g(m))),g(g(g(k)))) | m == k | b == k. [resolve(120,f,293,c)]. given #791 (T,wt=23): 1674 m == k | b == k | -(g(f(g(g(g(m))))) == x) | g(f(g(g(g(g(k)))))) == x. [resolve(939,c,16,a)]. given #792 (T,wt=23): 1684 m == k | b == k | -(x == f(f(g(g(g(g(k))))))) | x == f(f(g(g(g(m))))). [resolve(940,c,16,b)]. given #793 (T,wt=23): 1685 m == k | b == k | -(f(f(g(g(g(m))))) == x) | f(f(g(g(g(g(k)))))) == x. [resolve(940,c,16,a)]. given #794 (T,wt=23): 1703 m == k | b == k | -(x == g(g(f(g(g(g(k))))))) | x == g(g(f(g(g(m))))). [resolve(953,c,16,b)]. given #795 (A,wt=46): 452 m == k | b == k | g(g(m)) == b | p(g(g(m)),b) | g(g(g(m))) == m | g(g(m)) == m | g(g(m)) == g(g(g(m))) | p(f(g(g(g(m)))),g(g(g(g(k))))). [resolve(355,c,120,f)]. given #796 (T,wt=23): 1704 m == k | b == k | -(g(g(f(g(g(m))))) == x) | g(g(f(g(g(g(k)))))) == x. [resolve(953,c,16,a)]. given #797 (T,wt=23): 1716 m == k | b == k | -(x == f(g(f(g(g(g(k))))))) | x == f(g(f(g(g(m))))). [resolve(954,c,16,b)]. given #798 (T,wt=23): 1717 m == k | b == k | -(f(g(f(g(g(m))))) == x) | f(g(f(g(g(g(k)))))) == x. [resolve(954,c,16,a)]. given #799 (T,wt=23): 1730 m == k | b == k | -(x == g(f(f(g(g(g(k))))))) | x == g(f(f(g(g(m))))). [resolve(964,c,16,b)]. given #800 (A,wt=52): 453 m == k | b == k | g(g(g(m))) == b | p(g(g(g(m))),b) | g(g(g(m))) == m | g(g(g(g(m)))) == m | g(g(g(g(m)))) == g(g(g(m))) | p(g(g(g(g(k)))),f(g(g(g(m))))). [resolve(355,c,107,f)]. given #801 (T,wt=23): 1731 m == k | b == k | -(g(f(f(g(g(m))))) == x) | g(f(f(g(g(g(k)))))) == x. [resolve(964,c,16,a)]. given #802 (T,wt=23): 1741 m == k | b == k | -(x == f(f(f(g(g(g(k))))))) | x == f(f(f(g(g(m))))). [resolve(965,c,16,b)]. given #803 (T,wt=23): 1742 m == k | b == k | -(f(f(f(g(g(m))))) == x) | f(f(f(g(g(g(k)))))) == x. [resolve(965,c,16,a)]. given #804 (T,wt=23): 1763 m == k | b == k | -(x == g(g(g(f(g(g(k))))))) | x == g(g(g(f(g(m))))). [resolve(978,c,16,b)]. given #805 (A,wt=52): 454 m == k | b == k | g(g(g(m))) == b | p(g(g(g(m))),b) | g(g(g(m))) == m | g(g(g(g(m)))) == m | g(g(g(g(m)))) == g(g(g(m))) | p(f(g(g(g(m)))),g(g(g(g(k))))). [resolve(355,c,101,f)]. given #806 (T,wt=23): 1764 m == k | b == k | -(g(g(g(f(g(m))))) == x) | g(g(g(f(g(g(k)))))) == x. [resolve(978,c,16,a)]. given #807 (T,wt=23): 1776 m == k | b == k | -(x == f(g(g(f(g(g(k))))))) | x == f(g(g(f(g(m))))). [resolve(979,c,16,b)]. given #808 (T,wt=23): 1777 m == k | b == k | -(f(g(g(f(g(m))))) == x) | f(g(g(f(g(g(k)))))) == x. [resolve(979,c,16,a)]. given #809 (T,wt=23): 1790 m == k | b == k | -(x == g(f(g(f(g(g(k))))))) | x == g(f(g(f(g(m))))). [resolve(991,c,16,b)]. given #810 (A,wt=42): 455 m == k | b == k | g(g(m)) == b | p(g(g(m)),b) | g(g(g(m))) == m | g(g(m)) == m | g(g(m)) == g(g(g(m))) | p(g(g(g(g(k)))),m). [resolve(355,c,93,f)]. given #811 (T,wt=23): 1791 m == k | b == k | -(g(f(g(f(g(m))))) == x) | g(f(g(f(g(g(k)))))) == x. [resolve(991,c,16,a)]. given #812 (T,wt=23): 1801 m == k | b == k | -(x == f(f(g(f(g(g(k))))))) | x == f(f(g(f(g(m))))). [resolve(992,c,16,b)]. given #813 (T,wt=23): 1802 m == k | b == k | -(f(f(g(f(g(m))))) == x) | f(f(g(f(g(g(k)))))) == x. [resolve(992,c,16,a)]. given #814 (T,wt=23): 1821 m == k | b == k | -(x == g(g(f(f(g(g(k))))))) | x == g(g(f(f(g(m))))). [resolve(1005,c,16,b)]. given #815 (A,wt=48): 456 m == k | b == k | g(g(g(m))) == b | p(g(g(g(m))),b) | g(g(g(m))) == m | g(g(g(g(m)))) == m | g(g(g(g(m)))) == g(g(g(m))) | p(g(g(g(g(k)))),m). [resolve(355,c,86,f)]. given #816 (T,wt=23): 1822 m == k | b == k | -(g(g(f(f(g(m))))) == x) | g(g(f(f(g(g(k)))))) == x. [resolve(1005,c,16,a)]. given #817 (T,wt=23): 1834 m == k | b == k | -(x == f(g(f(f(g(g(k))))))) | x == f(g(f(f(g(m))))). [resolve(1006,c,16,b)]. given #818 (T,wt=23): 1835 m == k | b == k | -(f(g(f(f(g(m))))) == x) | f(g(f(f(g(g(k)))))) == x. [resolve(1006,c,16,a)]. given #819 (T,wt=23): 1848 m == k | b == k | -(x == g(f(f(f(g(g(k))))))) | x == g(f(f(f(g(m))))). [resolve(1016,c,16,b)]. given #820 (A,wt=25): 457 m == k | b == k | p(g(g(m)),g(g(g(g(k))))) | g(g(m)) == b | p(g(g(m)),b). [resolve(355,c,40,a)]. given #821 (T,wt=23): 1849 m == k | b == k | -(g(f(f(f(g(m))))) == x) | g(f(f(f(g(g(k)))))) == x. [resolve(1016,c,16,a)]. given #822 (T,wt=23): 1859 m == k | b == k | -(x == f(f(f(f(g(g(k))))))) | x == f(f(f(f(g(m))))). [resolve(1017,c,16,b)]. given #823 (T,wt=23): 1860 m == k | b == k | -(f(f(f(f(g(m))))) == x) | f(f(f(f(g(g(k)))))) == x. [resolve(1017,c,16,a)]. given #824 (T,wt=23): 1879 m == k | b == k | -(x == g(g(g(g(f(g(k))))))) | x == g(g(g(g(f(m))))). [resolve(1030,c,16,b)]. given #825 (A,wt=29): 458 m == k | b == k | p(g(g(g(g(m)))),g(g(g(g(k))))) | g(g(g(m))) == b | p(g(g(g(m))),b). [resolve(355,c,39,a)]. given #826 (T,wt=23): 1880 m == k | b == k | -(g(g(g(g(f(m))))) == x) | g(g(g(g(f(g(k)))))) == x. [resolve(1030,c,16,a)]. given #827 (T,wt=23): 1892 m == k | b == k | -(x == f(g(g(g(f(g(k))))))) | x == f(g(g(g(f(m))))). [resolve(1031,c,16,b)]. given #828 (T,wt=23): 1893 m == k | b == k | -(f(g(g(g(f(m))))) == x) | f(g(g(g(f(g(k)))))) == x. [resolve(1031,c,16,a)]. given #829 (T,wt=23): 1906 m == k | b == k | -(x == g(f(g(g(f(g(k))))))) | x == g(f(g(g(f(m))))). [resolve(1043,c,16,b)]. given #830 (A,wt=29): 459 m == k | b == k | p(g(g(g(g(k)))),g(g(g(g(m))))) | g(g(g(m))) == b | p(g(g(g(m))),b). [resolve(355,c,38,a)]. given #831 (T,wt=23): 1907 m == k | b == k | -(g(f(g(g(f(m))))) == x) | g(f(g(g(f(g(k)))))) == x. [resolve(1043,c,16,a)]. given #832 (T,wt=23): 1917 m == k | b == k | -(x == f(f(g(g(f(g(k))))))) | x == f(f(g(g(f(m))))). [resolve(1044,c,16,b)]. given #833 (T,wt=23): 1918 m == k | b == k | -(f(f(g(g(f(m))))) == x) | f(f(g(g(f(g(k)))))) == x. [resolve(1044,c,16,a)]. given #834 (T,wt=23): 1936 m == k | b == k | -(x == g(g(f(g(f(g(k))))))) | x == g(g(f(g(f(m))))). [resolve(1057,c,16,b)]. given #835 (A,wt=25): 460 m == k | b == k | p(g(g(g(g(k)))),g(g(m))) | g(g(m)) == b | p(g(g(m)),b). [resolve(355,c,37,a)]. given #836 (T,wt=23): 1937 m == k | b == k | -(g(g(f(g(f(m))))) == x) | g(g(f(g(f(g(k)))))) == x. [resolve(1057,c,16,a)]. given #837 (T,wt=23): 1949 m == k | b == k | -(x == f(g(f(g(f(g(k))))))) | x == f(g(f(g(f(m))))). [resolve(1058,c,16,b)]. given #838 (T,wt=23): 1950 m == k | b == k | -(f(g(f(g(f(m))))) == x) | f(g(f(g(f(g(k)))))) == x. [resolve(1058,c,16,a)]. given #839 (T,wt=23): 1963 m == k | b == k | -(x == g(f(f(g(f(g(k))))))) | x == g(f(f(g(f(m))))). [resolve(1074,c,16,b)]. given #840 (A,wt=38): 465 m == k | b == k | g(m) == b | p(g(m),b) | g(g(m)) == m | g(m) == m | g(m) == g(g(m)) | p(f(g(g(g(k)))),g(g(m))). [resolve(356,c,121,f)]. given #841 (T,wt=23): 1964 m == k | b == k | -(g(f(f(g(f(m))))) == x) | g(f(f(g(f(g(k)))))) == x. [resolve(1074,c,16,a)]. given #842 (T,wt=23): 1974 m == k | b == k | -(x == f(f(f(g(f(g(k))))))) | x == f(f(f(g(f(m))))). [resolve(1075,c,16,b)]. given #843 (T,wt=23): 1975 m == k | b == k | -(f(f(f(g(f(m))))) == x) | f(f(f(g(f(g(k)))))) == x. [resolve(1075,c,16,a)]. given #844 (T,wt=23): 1993 m == k | b == k | -(x == g(g(g(f(f(g(k))))))) | x == g(g(g(f(f(m))))). [resolve(1088,c,16,b)]. given #845 (A,wt=52): 466 m == k | b == k | f(g(g(m))) == b | p(f(g(g(m))),b) | f(g(g(m))) == m | g(f(g(g(m)))) == m | g(f(g(g(m)))) == f(g(g(m))) | p(f(g(g(g(k)))),f(f(g(g(m))))). [resolve(356,c,107,f)]. given #846 (T,wt=23): 1994 m == k | b == k | -(g(g(g(f(f(m))))) == x) | g(g(g(f(f(g(k)))))) == x. [resolve(1088,c,16,a)]. given #847 (T,wt=23): 2006 m == k | b == k | -(x == f(g(g(f(f(g(k))))))) | x == f(g(g(f(f(m))))). [resolve(1089,c,16,b)]. given #848 (T,wt=23): 2007 m == k | b == k | -(f(g(g(f(f(m))))) == x) | f(g(g(f(f(g(k)))))) == x. [resolve(1089,c,16,a)]. given #849 (T,wt=23): 2020 m == k | b == k | -(x == g(f(g(f(f(g(k))))))) | x == g(f(g(f(f(m))))). [resolve(1101,c,16,b)]. given #850 (A,wt=44): 467 m == k | b == k | g(g(m)) == b | p(g(g(m)),b) | g(g(m)) == m | g(g(g(m))) == m | g(g(g(m))) == g(g(m)) | p(g(g(m)),f(g(g(g(k))))). [resolve(356,c,106,f)]. given #851 (T,wt=23): 2021 m == k | b == k | -(g(f(g(f(f(m))))) == x) | g(f(g(f(f(g(k)))))) == x. [resolve(1101,c,16,a)]. given #852 (T,wt=23): 2031 m == k | b == k | -(x == f(f(g(f(f(g(k))))))) | x == f(f(g(f(f(m))))). [resolve(1102,c,16,b)]. given #853 (T,wt=23): 2032 m == k | b == k | -(f(f(g(f(f(m))))) == x) | f(f(g(f(f(g(k)))))) == x. [resolve(1102,c,16,a)]. given #854 (T,wt=23): 2053 m == k | b == k | -(x == g(g(f(f(f(g(k))))))) | x == g(g(f(f(f(m))))). [resolve(1115,c,16,b)]. given #855 (A,wt=44): 468 m == k | b == k | g(g(m)) == b | p(g(g(m)),b) | g(g(m)) == m | g(g(g(m))) == m | g(g(g(m))) == g(g(m)) | p(f(g(g(g(k)))),g(g(m))). [resolve(356,c,102,f)]. given #856 (T,wt=23): 2054 m == k | b == k | -(g(g(f(f(f(m))))) == x) | g(g(f(f(f(g(k)))))) == x. [resolve(1115,c,16,a)]. given #857 (T,wt=23): 2066 m == k | b == k | -(x == f(g(f(f(f(g(k))))))) | x == f(g(f(f(f(m))))). [resolve(1116,c,16,b)]. given #858 (T,wt=23): 2067 m == k | b == k | -(f(g(f(f(f(m))))) == x) | f(g(f(f(f(g(k)))))) == x. [resolve(1116,c,16,a)]. given #859 (T,wt=23): 2080 m == k | b == k | -(x == g(f(f(f(f(g(k))))))) | x == g(f(f(f(f(m))))). [resolve(1129,c,16,b)]. given #860 (A,wt=52): 469 m == k | b == k | f(g(g(m))) == b | p(f(g(g(m))),b) | f(g(g(m))) == m | g(f(g(g(m)))) == m | g(f(g(g(m)))) == f(g(g(m))) | p(f(f(g(g(m)))),f(g(g(g(k))))). [resolve(356,c,101,f)]. given #861 (T,wt=23): 2081 m == k | b == k | -(g(f(f(f(f(m))))) == x) | g(f(f(f(f(g(k)))))) == x. [resolve(1129,c,16,a)]. given #862 (T,wt=23): 2091 m == k | b == k | -(x == f(f(f(f(f(g(k))))))) | x == f(f(f(f(f(m))))). [resolve(1130,c,16,b)]. given #863 (T,wt=23): 2092 m == k | b == k | -(f(f(f(f(f(m))))) == x) | f(f(f(f(f(g(k)))))) == x. [resolve(1130,c,16,a)]. given #864 (T,wt=23): 4280 m == k | b == k | g(g(m)) == b | p(g(g(m)),b) | -(g(g(g(g(k)))) == b). [factor(4275,d,f)]. given #865 (A,wt=48): 470 m == k | b == k | f(g(g(m))) == b | p(f(g(g(m))),b) | f(g(g(m))) == m | g(f(g(g(m)))) == m | g(f(g(g(m)))) == f(g(g(m))) | p(f(g(g(g(k)))),m). [resolve(356,c,86,f)]. given #866 (T,wt=24): 1803 m == k | b == k | g(m) == b | p(g(m),b) | -(g(g(k)) == x) | p(g(g(m)),x). [resolve(290,c,18,b)]. given #867 (T,wt=24): 1804 m == k | b == k | g(m) == b | p(g(m),b) | -(g(g(m)) == x) | p(x,g(g(k))). [resolve(290,c,17,b)]. given #868 (T,wt=22): 4329 m == k | b == k | g(m) == b | p(g(m),b) | p(g(g(g(k))),g(g(k))). [resolve(1804,e,293,c),merge(f),merge(g)]. given #869 (T,wt=24): 1861 m == k | b == k | g(m) == b | p(g(m),b) | -(g(g(m)) == x) | p(g(g(k)),x). [resolve(291,c,18,b)]. given #870 (A,wt=29): 471 m == k | b == k | p(g(f(g(g(m)))),f(g(g(g(k))))) | f(g(g(m))) == b | p(f(g(g(m))),b). [resolve(356,c,39,a)]. given #871 (T,wt=22): 4336 m == k | b == k | g(m) == b | p(g(m),b) | p(g(g(k)),g(g(g(k)))). [resolve(1861,e,293,c),merge(f),merge(g)]. given #872 (T,wt=24): 1862 m == k | b == k | g(m) == b | p(g(m),b) | -(g(g(k)) == x) | p(x,g(g(m))). [resolve(291,c,17,b)]. given #873 (T,wt=24): 2093 m == k | b == k | f(m) == b | p(f(m),b) | -(f(g(k)) == x) | p(g(f(m)),x). [resolve(300,c,18,b)]. given #874 (T,wt=24): 2094 m == k | b == k | f(m) == b | p(f(m),b) | -(g(f(m)) == x) | p(x,f(g(k))). [resolve(300,c,17,b)]. given #875 (A,wt=29): 472 m == k | b == k | p(f(g(g(g(k)))),g(f(g(g(m))))) | f(g(g(m))) == b | p(f(g(g(m))),b). [resolve(356,c,38,a)]. given #876 (T,wt=22): 4349 m == k | b == k | f(m) == b | p(f(m),b) | p(g(f(g(k))),f(g(k))). [resolve(2094,e,302,c),merge(f),merge(g)]. given #877 (T,wt=24): 2099 m == k | b == k | f(m) == b | p(f(m),b) | -(g(f(m)) == x) | p(f(g(k)),x). [resolve(301,c,18,b)]. given #878 (T,wt=22): 4362 m == k | b == k | f(m) == b | p(f(m),b) | p(f(g(k)),g(f(g(k)))). [resolve(2099,e,302,c),merge(f),merge(g)]. given #879 (T,wt=24): 2100 m == k | b == k | f(m) == b | p(f(m),b) | -(f(g(k)) == x) | p(x,g(f(m))). [resolve(301,c,17,b)]. given #880 (A,wt=46): 477 m == k | b == k | f(g(m)) == b | p(f(g(m)),b) | g(f(g(m))) == m | f(g(m)) == m | f(g(m)) == g(f(g(m))) | p(f(g(f(g(m)))),g(f(g(g(k))))). [resolve(368,c,120,f)]. given #881 (T,wt=24): 2105 m == k | b == k | g(m) == b | p(g(m),b) | -(g(g(g(k))) == x) | p(g(m),x). [resolve(351,c,18,b)]. given #882 (T,wt=24): 2106 m == k | b == k | g(m) == b | p(g(m),b) | -(g(m) == x) | p(x,g(g(g(k)))). [resolve(351,c,17,b)]. given #883 (T,wt=24): 2111 m == k | b == k | g(m) == b | p(g(m),b) | -(g(m) == x) | p(g(g(g(k))),x). [resolve(354,c,18,b)]. given #884 (T,wt=24): 2112 m == k | b == k | g(m) == b | p(g(m),b) | -(g(g(g(k))) == x) | p(x,g(m)). [resolve(354,c,17,b)]. given #885 (A,wt=52): 478 m == k | b == k | g(f(g(m))) == b | p(g(f(g(m))),b) | g(f(g(m))) == m | g(g(f(g(m)))) == m | g(g(f(g(m)))) == g(f(g(m))) | p(g(f(g(g(k)))),f(g(f(g(m))))). [resolve(368,c,107,f)]. given #886 (T,wt=24): 2123 m == k | b == k | f(m) == b | p(f(m),b) | -(g(f(g(k))) == x) | p(f(m),x). [resolve(376,c,18,b)]. given #887 (T,wt=24): 2124 m == k | b == k | f(m) == b | p(f(m),b) | -(f(m) == x) | p(x,g(f(g(k)))). [resolve(376,c,17,b)]. given #888 (T,wt=24): 2129 m == k | b == k | f(m) == b | p(f(m),b) | -(f(m) == x) | p(g(f(g(k))),x). [resolve(379,c,18,b)]. given #889 (T,wt=24): 2130 m == k | b == k | f(m) == b | p(f(m),b) | -(g(f(g(k))) == x) | p(x,f(m)). [resolve(379,c,17,b)]. given #890 (A,wt=52): 479 m == k | b == k | g(f(g(m))) == b | p(g(f(g(m))),b) | g(f(g(m))) == m | g(g(f(g(m)))) == m | g(g(f(g(m)))) == g(f(g(m))) | p(f(g(f(g(m)))),g(f(g(g(k))))). [resolve(368,c,101,f)]. given #891 (T,wt=24): 2189 m == k | b == k | p(m,b) | g(g(k)) == b | -p(g(g(k)),b) | m == g(g(k)). [resolve(338,g,292,c),merge(g),merge(h),merge(i)]. given #892 (T,wt=24): 2207 m == k | b == k | g(k) == b | p(g(m),m) | k == b | p(k,b) | k == g(k). [resolve(2205,d,44,d),merge(g)]. given #893 (T,wt=24): 2226 m == k | b == k | g(k) == b | p(m,g(m)) | k == b | p(k,b) | k == g(k). [resolve(2216,d,44,d),merge(g)]. given #894 (T,wt=24): 2254 m == k | b == k | g(g(g(g(g(g(g(m))))))) == g(g(g(g(g(g(g(g(k)))))))). [resolve(1205,c,20,a)]. given #895 (A,wt=42): 480 m == k | b == k | f(g(m)) == b | p(f(g(m)),b) | g(f(g(m))) == m | f(g(m)) == m | f(g(m)) == g(f(g(m))) | p(g(f(g(g(k)))),m). [resolve(368,c,93,f)]. given #896 (T,wt=24): 2255 m == k | b == k | f(g(g(g(g(g(g(m))))))) == f(g(g(g(g(g(g(g(k)))))))). [resolve(1205,c,19,a)]. given #897 (T,wt=24): 2267 m == k | b == k | g(f(g(g(g(g(g(m))))))) == g(f(g(g(g(g(g(g(k)))))))). [resolve(1206,c,20,a)]. given #898 (T,wt=24): 2268 m == k | b == k | f(f(g(g(g(g(g(m))))))) == f(f(g(g(g(g(g(g(k)))))))). [resolve(1206,c,19,a)]. given #899 (T,wt=24): 2281 m == k | b == k | g(g(f(g(g(g(g(m))))))) == g(g(f(g(g(g(g(g(k)))))))). [resolve(1218,c,20,a)]. given #900 (A,wt=48): 481 m == k | b == k | g(f(g(m))) == b | p(g(f(g(m))),b) | g(f(g(m))) == m | g(g(f(g(m)))) == m | g(g(f(g(m)))) == g(f(g(m))) | p(g(f(g(g(k)))),m). [resolve(368,c,86,f)]. given #901 (T,wt=24): 2282 m == k | b == k | f(g(f(g(g(g(g(m))))))) == f(g(f(g(g(g(g(g(k)))))))). [resolve(1218,c,19,a)]. given #902 (T,wt=24): 2298 m == k | b == k | g(f(f(g(g(g(g(m))))))) == g(f(f(g(g(g(g(g(k)))))))). [resolve(1219,c,20,a)]. given #903 (T,wt=24): 2299 m == k | b == k | f(f(f(g(g(g(g(m))))))) == f(f(f(g(g(g(g(g(k)))))))). [resolve(1219,c,19,a)]. given #904 (T,wt=24): 2312 m == k | b == k | g(g(g(f(g(g(g(m))))))) == g(g(g(f(g(g(g(g(k)))))))). [resolve(1232,c,20,a)]. given #905 (A,wt=25): 482 m == k | b == k | p(f(g(m)),g(f(g(g(k))))) | f(g(m)) == b | p(f(g(m)),b). [resolve(368,c,40,a)]. given #906 (T,wt=23): 4542 m == k | b == k | f(g(m)) == b | p(f(g(m)),b) | -(g(f(g(g(k)))) == b). [factor(4537,d,f)]. given #907 (T,wt=24): 2313 m == k | b == k | f(g(g(f(g(g(g(m))))))) == f(g(g(f(g(g(g(g(k)))))))). [resolve(1232,c,19,a)]. given #908 (T,wt=24): 2325 m == k | b == k | g(f(g(f(g(g(g(m))))))) == g(f(g(f(g(g(g(g(k)))))))). [resolve(1233,c,20,a)]. given #909 (T,wt=24): 2326 m == k | b == k | f(f(g(f(g(g(g(m))))))) == f(f(g(f(g(g(g(g(k)))))))). [resolve(1233,c,19,a)]. given #910 (A,wt=29): 483 m == k | b == k | p(g(g(f(g(m)))),g(f(g(g(k))))) | g(f(g(m))) == b | p(g(f(g(m))),b). [resolve(368,c,39,a)]. given #911 (T,wt=24): 2339 m == k | b == k | g(g(f(f(g(g(g(m))))))) == g(g(f(f(g(g(g(g(k)))))))). [resolve(1243,c,20,a)]. given #912 (T,wt=24): 2340 m == k | b == k | f(g(f(f(g(g(g(m))))))) == f(g(f(f(g(g(g(g(k)))))))). [resolve(1243,c,19,a)]. given #913 (T,wt=24): 2355 m == k | b == k | g(f(f(f(g(g(g(m))))))) == g(f(f(f(g(g(g(g(k)))))))). [resolve(1244,c,20,a)]. given #914 (T,wt=24): 2356 m == k | b == k | f(f(f(f(g(g(g(m))))))) == f(f(f(f(g(g(g(g(k)))))))). [resolve(1244,c,19,a)]. given #915 (A,wt=29): 484 m == k | b == k | p(g(f(g(g(k)))),g(g(f(g(m))))) | g(f(g(m))) == b | p(g(f(g(m))),b). [resolve(368,c,38,a)]. given #916 (T,wt=24): 2369 m == k | b == k | g(g(g(g(f(g(g(m))))))) == g(g(g(g(f(g(g(g(k)))))))). [resolve(1259,c,20,a)]. given #917 (T,wt=24): 2370 m == k | b == k | f(g(g(g(f(g(g(m))))))) == f(g(g(g(f(g(g(g(k)))))))). [resolve(1259,c,19,a)]. given #918 (T,wt=24): 2382 m == k | b == k | g(f(g(g(f(g(g(m))))))) == g(f(g(g(f(g(g(g(k)))))))). [resolve(1260,c,20,a)]. given #919 (T,wt=24): 2383 m == k | b == k | f(f(g(g(f(g(g(m))))))) == f(f(g(g(f(g(g(g(k)))))))). [resolve(1260,c,19,a)]. given #920 (A,wt=25): 485 m == k | b == k | p(g(f(g(g(k)))),f(g(m))) | f(g(m)) == b | p(f(g(m)),b). [resolve(368,c,37,a)]. given #921 (T,wt=24): 2396 m == k | b == k | g(g(f(g(f(g(g(m))))))) == g(g(f(g(f(g(g(g(k)))))))). [resolve(1272,c,20,a)]. given #922 (T,wt=24): 2397 m == k | b == k | f(g(f(g(f(g(g(m))))))) == f(g(f(g(f(g(g(g(k)))))))). [resolve(1272,c,19,a)]. given #923 (T,wt=24): 2412 m == k | b == k | g(f(f(g(f(g(g(m))))))) == g(f(f(g(f(g(g(g(k)))))))). [resolve(1273,c,20,a)]. given #924 (T,wt=24): 2413 m == k | b == k | f(f(f(g(f(g(g(m))))))) == f(f(f(g(f(g(g(g(k)))))))). [resolve(1273,c,19,a)]. given #925 (A,wt=33): 490 x == b | p(x,b) | g(x) == m | x == m | x == g(x) | f(g(x)) == m | p(f(g(x)),m) | g(x) == f(g(x)). [resolve(123,i,95,f),merge(i),merge(j),merge(k),merge(l),merge(m)]. given #926 (T,wt=24): 2426 m == k | b == k | g(g(g(f(f(g(g(m))))))) == g(g(g(f(f(g(g(g(k)))))))). [resolve(1286,c,20,a)]. given #927 (T,wt=24): 2427 m == k | b == k | f(g(g(f(f(g(g(m))))))) == f(g(g(f(f(g(g(g(k)))))))). [resolve(1286,c,19,a)]. given #928 (T,wt=24): 2439 m == k | b == k | g(f(g(f(f(g(g(m))))))) == g(f(g(f(f(g(g(g(k)))))))). [resolve(1287,c,20,a)]. given #929 (T,wt=24): 2440 m == k | b == k | f(f(g(f(f(g(g(m))))))) == f(f(g(f(f(g(g(g(k)))))))). [resolve(1287,c,19,a)]. given #930 (A,wt=52): 491 m == k | b == k | f(f(g(m))) == b | p(f(f(g(m))),b) | f(f(g(m))) == m | g(f(f(g(m)))) == m | g(f(f(g(m)))) == f(f(g(m))) | p(f(f(g(g(k)))),f(f(f(g(m))))). [resolve(369,c,107,f)]. given #931 (T,wt=24): 2453 m == k | b == k | g(g(f(f(f(g(g(m))))))) == g(g(f(f(f(g(g(g(k)))))))). [resolve(1297,c,20,a)]. given #932 (T,wt=24): 2454 m == k | b == k | f(g(f(f(f(g(g(m))))))) == f(g(f(f(f(g(g(g(k)))))))). [resolve(1297,c,19,a)]. given #933 (T,wt=24): 2468 m == k | b == k | g(f(f(f(f(g(g(m))))))) == g(f(f(f(f(g(g(g(k)))))))). [resolve(1298,c,20,a)]. given #934 (T,wt=24): 2469 m == k | b == k | f(f(f(f(f(g(g(m))))))) == f(f(f(f(f(g(g(g(k)))))))). [resolve(1298,c,19,a)]. given #935 (A,wt=44): 492 m == k | b == k | f(g(m)) == b | p(f(g(m)),b) | f(g(m)) == m | g(f(g(m))) == m | g(f(g(m))) == f(g(m)) | p(f(g(m)),f(f(g(g(k))))). [resolve(369,c,106,f)]. given #936 (T,wt=24): 2482 m == k | b == k | g(g(g(g(g(f(g(m))))))) == g(g(g(g(g(f(g(g(k)))))))). [resolve(1311,c,20,a)]. given #937 (T,wt=24): 2483 m == k | b == k | f(g(g(g(g(f(g(m))))))) == f(g(g(g(g(f(g(g(k)))))))). [resolve(1311,c,19,a)]. given #938 (T,wt=24): 2495 m == k | b == k | g(f(g(g(g(f(g(m))))))) == g(f(g(g(g(f(g(g(k)))))))). [resolve(1312,c,20,a)]. given #939 (T,wt=24): 2496 m == k | b == k | f(f(g(g(g(f(g(m))))))) == f(f(g(g(g(f(g(g(k)))))))). [resolve(1312,c,19,a)]. given #940 (A,wt=44): 493 m == k | b == k | f(g(m)) == b | p(f(g(m)),b) | f(g(m)) == m | g(f(g(m))) == m | g(f(g(m))) == f(g(m)) | p(f(f(g(g(k)))),f(g(m))). [resolve(369,c,102,f)]. given #941 (T,wt=24): 2509 m == k | b == k | g(g(f(g(g(f(g(m))))))) == g(g(f(g(g(f(g(g(k)))))))). [resolve(1324,c,20,a)]. given #942 (T,wt=24): 2510 m == k | b == k | f(g(f(g(g(f(g(m))))))) == f(g(f(g(g(f(g(g(k)))))))). [resolve(1324,c,19,a)]. given #943 (T,wt=24): 2525 m == k | b == k | g(f(f(g(g(f(g(m))))))) == g(f(f(g(g(f(g(g(k)))))))). [resolve(1325,c,20,a)]. given #944 (T,wt=24): 2526 m == k | b == k | f(f(f(g(g(f(g(m))))))) == f(f(f(g(g(f(g(g(k)))))))). [resolve(1325,c,19,a)]. given #945 (A,wt=52): 494 m == k | b == k | f(f(g(m))) == b | p(f(f(g(m))),b) | f(f(g(m))) == m | g(f(f(g(m)))) == m | g(f(f(g(m)))) == f(f(g(m))) | p(f(f(f(g(m)))),f(f(g(g(k))))). [resolve(369,c,101,f)]. given #946 (T,wt=24): 2539 m == k | b == k | g(g(g(f(g(f(g(m))))))) == g(g(g(f(g(f(g(g(k)))))))). [resolve(1338,c,20,a)]. given #947 (T,wt=24): 2540 m == k | b == k | f(g(g(f(g(f(g(m))))))) == f(g(g(f(g(f(g(g(k)))))))). [resolve(1338,c,19,a)]. given #948 (T,wt=24): 2552 m == k | b == k | g(f(g(f(g(f(g(m))))))) == g(f(g(f(g(f(g(g(k)))))))). [resolve(1339,c,20,a)]. given #949 (T,wt=24): 2553 m == k | b == k | f(f(g(f(g(f(g(m))))))) == f(f(g(f(g(f(g(g(k)))))))). [resolve(1339,c,19,a)]. given #950 (A,wt=48): 495 m == k | b == k | f(f(g(m))) == b | p(f(f(g(m))),b) | f(f(g(m))) == m | g(f(f(g(m)))) == m | g(f(f(g(m)))) == f(f(g(m))) | p(f(f(g(g(k)))),m). [resolve(369,c,86,f)]. given #951 (T,wt=24): 2566 m == k | b == k | g(g(f(f(g(f(g(m))))))) == g(g(f(f(g(f(g(g(k)))))))). [resolve(1349,c,20,a)]. given #952 (T,wt=24): 2567 m == k | b == k | f(g(f(f(g(f(g(m))))))) == f(g(f(f(g(f(g(g(k)))))))). [resolve(1349,c,19,a)]. given #953 (T,wt=24): 2585 m == k | b == k | g(f(f(f(g(f(g(m))))))) == g(f(f(f(g(f(g(g(k)))))))). [resolve(1350,c,20,a)]. given #954 (T,wt=24): 2586 m == k | b == k | f(f(f(f(g(f(g(m))))))) == f(f(f(f(g(f(g(g(k)))))))). [resolve(1350,c,19,a)]. given #955 (A,wt=29): 496 m == k | b == k | p(g(f(f(g(m)))),f(f(g(g(k))))) | f(f(g(m))) == b | p(f(f(g(m))),b). [resolve(369,c,39,a)]. given #956 (T,wt=24): 2599 m == k | b == k | g(g(g(g(f(f(g(m))))))) == g(g(g(g(f(f(g(g(k)))))))). [resolve(1366,c,20,a)]. given #957 (T,wt=24): 2600 m == k | b == k | f(g(g(g(f(f(g(m))))))) == f(g(g(g(f(f(g(g(k)))))))). [resolve(1366,c,19,a)]. given #958 (T,wt=24): 2612 m == k | b == k | g(f(g(g(f(f(g(m))))))) == g(f(g(g(f(f(g(g(k)))))))). [resolve(1367,c,20,a)]. given #959 (T,wt=24): 2613 m == k | b == k | f(f(g(g(f(f(g(m))))))) == f(f(g(g(f(f(g(g(k)))))))). [resolve(1367,c,19,a)]. given #960 (A,wt=29): 497 m == k | b == k | p(f(f(g(g(k)))),g(f(f(g(m))))) | f(f(g(m))) == b | p(f(f(g(m))),b). [resolve(369,c,38,a)]. given #961 (T,wt=24): 2626 m == k | b == k | g(g(f(g(f(f(g(m))))))) == g(g(f(g(f(f(g(g(k)))))))). [resolve(1379,c,20,a)]. given #962 (T,wt=24): 2627 m == k | b == k | f(g(f(g(f(f(g(m))))))) == f(g(f(g(f(f(g(g(k)))))))). [resolve(1379,c,19,a)]. given #963 (T,wt=24): 2643 m == k | b == k | g(f(f(g(f(f(g(m))))))) == g(f(f(g(f(f(g(g(k)))))))). [resolve(1380,c,20,a)]. given #964 (T,wt=24): 2644 m == k | b == k | f(f(f(g(f(f(g(m))))))) == f(f(f(g(f(f(g(g(k)))))))). [resolve(1380,c,19,a)]. given #965 (A,wt=46): 502 m == k | b == k | g(f(m)) == b | p(g(f(m)),b) | g(g(f(m))) == m | g(f(m)) == m | g(f(m)) == g(g(f(m))) | p(f(g(g(f(m)))),g(g(f(g(k))))). [resolve(380,c,120,f)]. given #966 (T,wt=24): 2657 m == k | b == k | g(g(g(f(f(f(g(m))))))) == g(g(g(f(f(f(g(g(k)))))))). [resolve(1393,c,20,a)]. given #967 (T,wt=24): 2658 m == k | b == k | f(g(g(f(f(f(g(m))))))) == f(g(g(f(f(f(g(g(k)))))))). [resolve(1393,c,19,a)]. given #968 (T,wt=24): 2670 m == k | b == k | g(f(g(f(f(f(g(m))))))) == g(f(g(f(f(f(g(g(k)))))))). [resolve(1394,c,20,a)]. given #969 (T,wt=24): 2671 m == k | b == k | f(f(g(f(f(f(g(m))))))) == f(f(g(f(f(f(g(g(k)))))))). [resolve(1394,c,19,a)]. given #970 (A,wt=52): 503 m == k | b == k | g(g(f(m))) == b | p(g(g(f(m))),b) | g(g(f(m))) == m | g(g(g(f(m)))) == m | g(g(g(f(m)))) == g(g(f(m))) | p(g(g(f(g(k)))),f(g(g(f(m))))). [resolve(380,c,107,f)]. given #971 (T,wt=24): 2684 m == k | b == k | g(g(f(f(f(f(g(m))))))) == g(g(f(f(f(f(g(g(k)))))))). [resolve(1404,c,20,a)]. given #972 (T,wt=24): 2685 m == k | b == k | f(g(f(f(f(f(g(m))))))) == f(g(f(f(f(f(g(g(k)))))))). [resolve(1404,c,19,a)]. given #973 (T,wt=24): 2701 m == k | b == k | g(f(f(f(f(f(g(m))))))) == g(f(f(f(f(f(g(g(k)))))))). [resolve(1405,c,20,a)]. given #974 (T,wt=24): 2702 m == k | b == k | f(f(f(f(f(f(g(m))))))) == f(f(f(f(f(f(g(g(k)))))))). [resolve(1405,c,19,a)]. given #975 (A,wt=52): 504 m == k | b == k | g(g(f(m))) == b | p(g(g(f(m))),b) | g(g(f(m))) == m | g(g(g(f(m)))) == m | g(g(g(f(m)))) == g(g(f(m))) | p(f(g(g(f(m)))),g(g(f(g(k))))). [resolve(380,c,101,f)]. given #976 (T,wt=24): 2715 m == k | b == k | g(g(g(g(g(g(f(m))))))) == g(g(g(g(g(g(f(g(k)))))))). [resolve(1422,c,20,a)]. given #977 (T,wt=24): 2716 m == k | b == k | f(g(g(g(g(g(f(m))))))) == f(g(g(g(g(g(f(g(k)))))))). [resolve(1422,c,19,a)]. given #978 (T,wt=24): 2728 m == k | b == k | g(f(g(g(g(g(f(m))))))) == g(f(g(g(g(g(f(g(k)))))))). [resolve(1423,c,20,a)]. given #979 (T,wt=24): 2729 m == k | b == k | f(f(g(g(g(g(f(m))))))) == f(f(g(g(g(g(f(g(k)))))))). [resolve(1423,c,19,a)]. given #980 (A,wt=42): 505 m == k | b == k | g(f(m)) == b | p(g(f(m)),b) | g(g(f(m))) == m | g(f(m)) == m | g(f(m)) == g(g(f(m))) | p(g(g(f(g(k)))),m). [resolve(380,c,93,f)]. given #981 (T,wt=24): 2742 m == k | b == k | g(g(f(g(g(g(f(m))))))) == g(g(f(g(g(g(f(g(k)))))))). [resolve(1435,c,20,a)]. given #982 (T,wt=24): 2743 m == k | b == k | f(g(f(g(g(g(f(m))))))) == f(g(f(g(g(g(f(g(k)))))))). [resolve(1435,c,19,a)]. given #983 (T,wt=24): 2758 m == k | b == k | g(f(f(g(g(g(f(m))))))) == g(f(f(g(g(g(f(g(k)))))))). [resolve(1436,c,20,a)]. given #984 (T,wt=24): 2759 m == k | b == k | f(f(f(g(g(g(f(m))))))) == f(f(f(g(g(g(f(g(k)))))))). [resolve(1436,c,19,a)]. given #985 (A,wt=48): 506 m == k | b == k | g(g(f(m))) == b | p(g(g(f(m))),b) | g(g(f(m))) == m | g(g(g(f(m)))) == m | g(g(g(f(m)))) == g(g(f(m))) | p(g(g(f(g(k)))),m). [resolve(380,c,86,f)]. given #986 (T,wt=24): 2772 m == k | b == k | g(g(g(f(g(g(f(m))))))) == g(g(g(f(g(g(f(g(k)))))))). [resolve(1449,c,20,a)]. given #987 (T,wt=24): 2773 m == k | b == k | f(g(g(f(g(g(f(m))))))) == f(g(g(f(g(g(f(g(k)))))))). [resolve(1449,c,19,a)]. given #988 (T,wt=24): 2785 m == k | b == k | g(f(g(f(g(g(f(m))))))) == g(f(g(f(g(g(f(g(k)))))))). [resolve(1450,c,20,a)]. given #989 (T,wt=24): 2786 m == k | b == k | f(f(g(f(g(g(f(m))))))) == f(f(g(f(g(g(f(g(k)))))))). [resolve(1450,c,19,a)]. given #990 (A,wt=25): 507 m == k | b == k | p(g(f(m)),g(g(f(g(k))))) | g(f(m)) == b | p(g(f(m)),b). [resolve(380,c,40,a)]. given #991 (T,wt=23): 5513 m == k | b == k | g(f(m)) == b | p(g(f(m)),b) | -(g(g(f(g(k)))) == b). [factor(5508,d,f)]. given #992 (T,wt=24): 2799 m == k | b == k | g(g(f(f(g(g(f(m))))))) == g(g(f(f(g(g(f(g(k)))))))). [resolve(1460,c,20,a)]. given #993 (T,wt=24): 2800 m == k | b == k | f(g(f(f(g(g(f(m))))))) == f(g(f(f(g(g(f(g(k)))))))). [resolve(1460,c,19,a)]. given #994 (T,wt=24): 2815 m == k | b == k | g(f(f(f(g(g(f(m))))))) == g(f(f(f(g(g(f(g(k)))))))). [resolve(1461,c,20,a)]. given #995 (A,wt=29): 508 m == k | b == k | p(g(g(g(f(m)))),g(g(f(g(k))))) | g(g(f(m))) == b | p(g(g(f(m))),b). [resolve(380,c,39,a)]. given #996 (T,wt=24): 2816 m == k | b == k | f(f(f(f(g(g(f(m))))))) == f(f(f(f(g(g(f(g(k)))))))). [resolve(1461,c,19,a)]. given #997 (T,wt=24): 2829 m == k | b == k | g(g(g(g(f(g(f(m))))))) == g(g(g(g(f(g(f(g(k)))))))). [resolve(1474,c,20,a)]. given #998 (T,wt=24): 2830 m == k | b == k | f(g(g(g(f(g(f(m))))))) == f(g(g(g(f(g(f(g(k)))))))). [resolve(1474,c,19,a)]. given #999 (T,wt=24): 2842 m == k | b == k | g(f(g(g(f(g(f(m))))))) == g(f(g(g(f(g(f(g(k)))))))). [resolve(1475,c,20,a)]. given #1000 (A,wt=29): 509 m == k | b == k | p(g(g(f(g(k)))),g(g(g(f(m))))) | g(g(f(m))) == b | p(g(g(f(m))),b). [resolve(380,c,38,a)]. given #1001 (T,wt=24): 2843 m == k | b == k | f(f(g(g(f(g(f(m))))))) == f(f(g(g(f(g(f(g(k)))))))). [resolve(1475,c,19,a)]. given #1002 (T,wt=24): 2856 m == k | b == k | g(g(f(g(f(g(f(m))))))) == g(g(f(g(f(g(f(g(k)))))))). [resolve(1487,c,20,a)]. given #1003 (T,wt=24): 2857 m == k | b == k | f(g(f(g(f(g(f(m))))))) == f(g(f(g(f(g(f(g(k)))))))). [resolve(1487,c,19,a)]. given #1004 (T,wt=24): 2875 m == k | b == k | g(f(f(g(f(g(f(m))))))) == g(f(f(g(f(g(f(g(k)))))))). [resolve(1488,c,20,a)]. given #1005 (A,wt=25): 510 m == k | b == k | p(g(g(f(g(k)))),g(f(m))) | g(f(m)) == b | p(g(f(m)),b). [resolve(380,c,37,a)]. given #1006 (T,wt=24): 2876 m == k | b == k | f(f(f(g(f(g(f(m))))))) == f(f(f(g(f(g(f(g(k)))))))). [resolve(1488,c,19,a)]. given #1007 (T,wt=24): 2889 m == k | b == k | g(g(g(f(f(g(f(m))))))) == g(g(g(f(f(g(f(g(k)))))))). [resolve(1501,c,20,a)]. given #1008 (T,wt=24): 2890 m == k | b == k | f(g(g(f(f(g(f(m))))))) == f(g(g(f(f(g(f(g(k)))))))). [resolve(1501,c,19,a)]. given #1009 (T,wt=24): 2902 m == k | b == k | g(f(g(f(f(g(f(m))))))) == g(f(g(f(f(g(f(g(k)))))))). [resolve(1502,c,20,a)]. given #1010 (A,wt=38): 515 m == k | b == k | f(m) == b | p(f(m),b) | g(f(m)) == m | f(m) == m | f(m) == g(f(m)) | p(f(g(f(g(k)))),g(f(m))). [resolve(381,c,121,f)]. given #1011 (T,wt=24): 2903 m == k | b == k | f(f(g(f(f(g(f(m))))))) == f(f(g(f(f(g(f(g(k)))))))). [resolve(1502,c,19,a)]. given #1012 (T,wt=24): 2916 m == k | b == k | g(g(f(f(f(g(f(m))))))) == g(g(f(f(f(g(f(g(k)))))))). [resolve(1512,c,20,a)]. given #1013 (T,wt=24): 2917 m == k | b == k | f(g(f(f(f(g(f(m))))))) == f(g(f(f(f(g(f(g(k)))))))). [resolve(1512,c,19,a)]. given #1014 (T,wt=24): 2935 m == k | b == k | g(f(f(f(f(g(f(m))))))) == g(f(f(f(f(g(f(g(k)))))))). [resolve(1513,c,20,a)]. given #1015 (A,wt=52): 516 m == k | b == k | f(g(f(m))) == b | p(f(g(f(m))),b) | f(g(f(m))) == m | g(f(g(f(m)))) == m | g(f(g(f(m)))) == f(g(f(m))) | p(f(g(f(g(k)))),f(f(g(f(m))))). [resolve(381,c,107,f)]. given #1016 (T,wt=24): 2936 m == k | b == k | f(f(f(f(f(g(f(m))))))) == f(f(f(f(f(g(f(g(k)))))))). [resolve(1513,c,19,a)]. given #1017 (T,wt=24): 2949 m == k | b == k | g(g(g(g(g(f(f(m))))))) == g(g(g(g(g(f(f(g(k)))))))). [resolve(1528,c,20,a)]. given #1018 (T,wt=24): 2950 m == k | b == k | f(g(g(g(g(f(f(m))))))) == f(g(g(g(g(f(f(g(k)))))))). [resolve(1528,c,19,a)]. given #1019 (T,wt=24): 2962 m == k | b == k | g(f(g(g(g(f(f(m))))))) == g(f(g(g(g(f(f(g(k)))))))). [resolve(1529,c,20,a)]. given #1020 (A,wt=44): 517 m == k | b == k | g(f(m)) == b | p(g(f(m)),b) | g(f(m)) == m | g(g(f(m))) == m | g(g(f(m))) == g(f(m)) | p(g(f(m)),f(g(f(g(k))))). [resolve(381,c,106,f)]. given #1021 (T,wt=24): 2963 m == k | b == k | f(f(g(g(g(f(f(m))))))) == f(f(g(g(g(f(f(g(k)))))))). [resolve(1529,c,19,a)]. given #1022 (T,wt=24): 2976 m == k | b == k | g(g(f(g(g(f(f(m))))))) == g(g(f(g(g(f(f(g(k)))))))). [resolve(1541,c,20,a)]. given #1023 (T,wt=24): 2977 m == k | b == k | f(g(f(g(g(f(f(m))))))) == f(g(f(g(g(f(f(g(k)))))))). [resolve(1541,c,19,a)]. given #1024 (T,wt=24): 2993 m == k | b == k | g(f(f(g(g(f(f(m))))))) == g(f(f(g(g(f(f(g(k)))))))). [resolve(1542,c,20,a)]. given #1025 (A,wt=44): 518 m == k | b == k | g(f(m)) == b | p(g(f(m)),b) | g(f(m)) == m | g(g(f(m))) == m | g(g(f(m))) == g(f(m)) | p(f(g(f(g(k)))),g(f(m))). [resolve(381,c,102,f)]. given #1026 (T,wt=24): 2994 m == k | b == k | f(f(f(g(g(f(f(m))))))) == f(f(f(g(g(f(f(g(k)))))))). [resolve(1542,c,19,a)]. given #1027 (T,wt=24): 3007 m == k | b == k | g(g(g(f(g(f(f(m))))))) == g(g(g(f(g(f(f(g(k)))))))). [resolve(1555,c,20,a)]. given #1028 (T,wt=24): 3008 m == k | b == k | f(g(g(f(g(f(f(m))))))) == f(g(g(f(g(f(f(g(k)))))))). [resolve(1555,c,19,a)]. given #1029 (T,wt=24): 3020