============================== Prover9 ===============================
Prover9 (32) version September-2006, September 2006.
Process 26742 was started by mccune on cleo.thornwood,
Wed Sep 13 14:36:54 2006
The command was "/home/mccune/LADR/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


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:
Relation symbol precedence:  lex([ ==, p ]).
Function symbol precedence:  lex([ b, m, k, j, f, g ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(binary_resolution).  % (non-Horn)
  % set(neg_ur_resolution).  % (non-Horn, less than 100 clauses)

Auto_process settings:
  % set(factor).  % (non-Horn)
  % set(back_unit_deletion).  % (non-Horn)
    % set(back_unit_deletion) -> set(unit_deletion).

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
1 x == m | p(x,m) | y == m | y == x | -p(x,y) | -p(y,x).  [assumption].
2 x == b | -p(x,b) | y == b | y == x | -p(x,y) | -p(y,x).  [assumption].
3 x == k | x == m | x == b | -p(x,k).  [assumption].
4 x == m | -p(x,m) | -(f(x) == m).  [assumption].
5 x == m | -p(x,m) | -(f(x) == x).  [assumption].
6 x == m | -p(x,m) | p(x,f(x)).  [assumption].
7 x == m | -p(x,m) | p(f(x),x).  [assumption].
8 x == b | p(x,b) | -(g(x) == b).  [assumption].
9 x == b | p(x,b) | -(g(x) == x).  [assumption].
10 x == b | p(x,b) | p(x,g(x)).  [assumption].
11 x == b | p(x,b) | p(g(x),x).  [assumption].
12 x == k | -(x == m) | p(x,k).  [assumption].
13 x == k | -(x == b) | p(x,k).  [assumption].
14 x == x.  [assumption].
15 -(x == y) | y == x.  [assumption].
16 -(x == y) | -(y == z) | x == z.  [assumption].
17 -(x == y) | -p(x,z) | p(y,z).  [assumption].
18 -(x == y) | -p(z,x) | p(z,y).  [assumption].
19 -(x == y) | f(x) == f(y).  [assumption].
20 -(x == y) | g(x) == g(y).  [assumption].
21 -(m == b).  [assumption].
22 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 (T,wt=6): 35 b == k | p(b,k).  [resolve(14,a,13,b)].

given #25 (T,wt=6): 36 m == k | p(m,k).  [resolve(14,a,12,b)].

given #26 (A,wt=22): 24 x == b | p(x,b) | g(x) == b | -p(g(x),b) | x == g(x) | -p(g(x),x).  [resolve(10,c,2,f),merge(e)].

given #27 (F,wt=3): 41 -(b == m).  [ur(15,b,21,a)].

given #28 (F,wt=6): 43 k == j | p(k,j).  [resolve(23,c,14,a)].

given #29 (T,wt=9): 44 b == k | -(k == x) | p(b,x).  [resolve(35,b,18,b)].

given #30 (T,wt=9): 45 b == k | -(b == x) | p(x,k).  [resolve(35,b,17,b)].

given #31 (A,wt=25): 25 x == b | p(x,b) | g(x) == m | p(g(x),m) | x == m | x == g(x) | -p(g(x),x).  [resolve(10,c,1,f)].

given #32 (F,wt=9): 48 m == k | -(k == x) | p(m,x).  [resolve(36,b,18,b)].

given #33 (F,wt=9): 49 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 (T,wt=9): 54 k == j | -(k == x) | p(x,j).  [resolve(43,b,17,b)].

given #36 (A,wt=24): 26 x == b | p(x,b) | x == m | p(x,m) | g(x) == m | g(x) == x | -p(g(x),x).  [resolve(10,c,1,e)].

given #37 (F,wt=12): 30 p(m,b) | g(m) == m | -(f(g(m)) == m).  [resolve(11,c,4,b),unit_del(a,21)].

given #38 (F,wt=12): 46 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): 50 m == k | k == b | -p(k,b) | -p(k,m).  [resolve(36,b,2,f),merge(e),unit_del(d,21)].

given #40 (T,wt=13): 27 p(m,b) | g(m) == m | p(f(g(m)),g(m)).  [resolve(11,c,7,b),unit_del(a,21)].

given #41 (A,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 (F,wt=13): 29 p(m,b) | g(m) == m | -(f(g(m)) == g(m)).  [resolve(11,c,5,b),unit_del(a,21)].

given #43 (F,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 (T,wt=13): 39 -(x == y) | p(g(x),y) | x == b | p(x,b).  [resolve(18,b,11,c)].

given #46 (A,wt=18): 31 k == b | p(k,b) | g(k) == k | g(k) == m | g(k) == b.  [resolve(11,c,3,d)].

given #47 (F,wt=13): 40 -(g(x) == y) | p(x,y) | x == b | p(x,b).  [resolve(18,b,10,c)].

given #48 (F,wt=14): 42 g(j) == j | g(j) == k | j == b | p(j,b).  [resolve(22,b,11,c)].

given #49 (T,wt=15): 47 b == k | p(b,m) | k == m | k == b | -p(k,b).  [resolve(35,b,1,e),unit_del(b,41)].

given #50 (T,wt=15): 51 m == k | -p(m,b) | k == b | k == m | -p(k,m).  [resolve(36,b,2,e),unit_del(b,21)].

given #51 (A,wt=18): 52 x == b | p(x,b) | g(x) == b | -p(g(x),b) | x == g(x).  [resolve(24,f,11,c),merge(f),merge(g)].

given #52 (F,wt=15): 55 k == j | j == b | -p(j,b) | k == b | -p(j,k).  [resolve(43,b,2,f),merge(e)].

given #53 (F,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 (T,wt=16): 62 p(m,b) | g(m) == m | -(f(g(m)) == x) | p(x,g(m)).  [resolve(27,c,17,b)].

given #56 (A,wt=18): 56 k == j | k == b | -p(k,b) | j == b | j == k | -p(j,k).  [resolve(43,b,2,e)].

given #57 (F,wt=16): 67 p(m,b) | g(m) == m | -(f(g(m)) == x) | p(g(m),x).  [resolve(28,c,18,b)].

given #58 (F,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 (T,wt=17): 79 g(j) == j | g(j) == k | j == b | -(j == x) | p(x,b).  [resolve(42,d,17,b)].

given #61 (A,wt=18): 58 k == j | k == m | p(k,m) | j == m | j == k | -p(j,k).  [resolve(43,b,1,e)].

given #62 (F,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 (F,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 (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 #66 (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 #67 (F,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 (F,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 (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 #71 (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 #72 (F,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 (F,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 (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 #76 (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 #77 (F,wt=20): 111 g(j) == j | g(j) == k | j == b | k == b | k == j | -p(j,k).  [resolve(80,g,43,b),merge(g)].

given #78 (F,wt=22): 112 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 #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 (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,51,e),merge(h),merge(i)].

given #81 (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 #82 (F,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 (F,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 (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 #86 (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 #87 (F,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 (F,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 (T,wt=24): 73 k == b | g(k) == k | g(k) == m | g(k) == b | b == k | k == m | p(k,m).  [resolve(31,b,46,d)].

given #91 (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 #92 (F,wt=21): 146 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 #93 (F,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 #94 (T,wt=24): 83 b == k | p(b,m) | k == m | k == b | g(k) == k | g(k) == m | g(k) == b.  [resolve(47,e,31,b),merge(e)].

given #95 (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 #96 (A,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 #97 (F,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 (F,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 (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 #101 (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 #102 (F,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 (F,wt=24): 147 k == b | g(k) == k | g(k) == m | g(k) == b | m == k | b == k | k == m.  [resolve(146,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(147,b,9,c),merge(g)].

given #105 (T,wt=23): 168 k == b | g(k) == m | g(k) == b | m == k | b == k | k == m | p(b,m).  [resolve(167,g,47,e),merge(g),merge(i),merge(j)].

given #106 (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 #107 (F,wt=23): 169 k == b | g(k) == m | g(k) == b | m == k | b == k | k == m | p(k,m).  [resolve(167,g,46,d),merge(g),merge(h)].

given #108 (F,wt=23): 180 k == b | g(k) == m | g(k) == b | m == k | b == k | k == m | -p(m,b).  [resolve(169,g,51,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,50,d),merge(g),merge(h)].

given #110 (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 #111 (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 #112 (F,wt=20): 196 k == b | g(k) == b | m == k | b == k | k == m | m == g(k).  [resolve(188,b,15,a)].

given #113 (F,wt=19): 206 k == b | m == k | b == k | k == m | m == g(k) | p(k,b).  [resolve(196,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,47,e),merge(f),merge(h),merge(i)].

given #115 (T,wt=19): 215 k == b | m == k | b == k | k == m | m == g(k) | p(k,m).  [resolve(206,f,46,d),merge(f),merge(g)].

given #116 (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 #117 (F,wt=19): 226 k == b | m == k | b == k | k == m | m == g(k) | -p(m,b).  [resolve(215,f,51,e),merge(f),merge(h),merge(i)].

given #118 (F,wt=19): 227 k == b | m == k | b == k | k == m | m == g(k) | -p(k,b).  [resolve(215,f,50,d),merge(f),merge(g)].

given #119 (T,wt=16): 240 k == b | m == k | b == k | k == m | m == g(k).  [resolve(227,f,206,f),merge(f),merge(g),merge(h),merge(i),merge(j)].

given #120 (T,wt=13): 251 k == b | m == k | b == k | m == g(k).  [resolve(240,d,15,a),merge(e)].

given #121 (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 #122 (F,wt=10): 259 m == k | b == k | m == g(k).  [resolve(251,a,15,a),merge(d)].

given #123 (F,wt=10): 262 m == k | b == k | p(g(k),k).  [resolve(259,c,49,b),merge(c)].

given #124 (T,wt=10): 269 m == k | b == k | g(k) == m.  [resolve(259,c,15,a)].

given #125 (T,wt=10): 270 m == k | b == k | -(g(k) == k).  [factor(268,a,d)].

given #126 (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 #127 (F,wt=12): 265 m == k | b == k | g(m) == g(g(k)).  [resolve(259,c,20,a)].

given #128 (F,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 (T,wt=12): 279 m == k | b == k | f(g(k)) == f(m).  [resolve(269,c,19,a)].

given #131 (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 #132 (F,wt=13): 267 m == k | b == k | -(x == m) | x == g(k).  [resolve(259,c,16,b)].

given #133 (F,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 (T,wt=13): 272 m == k | b == k | -(g(k) == x) | p(x,k).  [resolve(262,c,17,b)].

given #136 (A,wt=25): 113 p(m,b) | g(m) == m | f(g(m)) == m | f(g(m)) == g(m) | -(m == x) | p(g(m),x).  [resolve(112,c,18,b)].

given #137 (F,wt=13): 280 m == k | b == k | -(x == g(k)) | x == m.  [resolve(269,c,16,b)].

given #138 (F,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 (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 #141 (A,wt=25): 114 p(m,b) | g(m) == m | f(g(m)) == m | f(g(m)) == g(m) | -(g(m) == x) | p(x,m).  [resolve(112,c,17,b)].

given #142 (F,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 (F,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 (T,wt=14): 294 m == k | b == k | f(g(m)) == f(g(g(k))).  [resolve(265,c,19,a)].

given #146 (A,wt=34): 115 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(112,c,2,e),unit_del(g,21)].

given #147 (F,wt=14): 302 m == k | b == k | g(f(m)) == g(f(g(k))).  [resolve(266,c,20,a)].

given #148 (F,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 (T,wt=14): 314 m == k | b == k | f(g(g(k))) == f(g(m)).  [resolve(278,c,19,a)].

given #151 (A,wt=26): 118 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 #152 (F,wt=14): 322 m == k | b == k | g(f(g(k))) == g(f(m)).  [resolve(279,c,20,a)].

given #153 (F,wt=14): 323 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 (T,wt=15): 275 m == k | b == k | p(k,m) | k == b | p(k,b).  [resolve(269,c,40,a)].

given #156 (A,wt=26): 119 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 #157 (F,wt=15): 295 m == k | b == k | -(x == g(m)) | x == g(g(k)).  [resolve(265,c,16,b)].

given #158 (F,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 (T,wt=15): 305 m == k | b == k | -(f(g(k)) == x) | f(m) == x.  [resolve(266,c,16,a)].

given #161 (A,wt=43): 120 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 #162 (F,wt=15): 315 m == k | b == k | -(x == g(g(k))) | x == g(m).  [resolve(278,c,16,b)].

given #163 (F,wt=15): 316 m == k | b == k | -(g(m) == x) | g(g(k)) == x.  [resolve(278,c,16,a)].

given #164 (T,wt=15): 324 m == k | b == k | -(x == f(g(k))) | x == f(m).  [resolve(279,c,16,b)].

given #165 (T,wt=15): 325 m == k | b == k | -(f(m) == x) | f(g(k)) == x.  [resolve(279,c,16,a)].

given #166 (A,wt=39): 121 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 #167 (F,wt=16): 355 m == k | b == k | g(g(g(m))) == g(g(g(g(k)))).  [resolve(293,c,20,a)].

given #168 (F,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 (T,wt=16): 369 m == k | b == k | f(f(g(m))) == f(f(g(g(k)))).  [resolve(294,c,19,a)].

given #171 (A,wt=27): 123 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 #172 (F,wt=16): 380 m == k | b == k | g(g(f(m))) == g(g(f(g(k)))).  [resolve(302,c,20,a)].

given #173 (F,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 (T,wt=16): 392 m == k | b == k | f(f(f(m))) == f(f(f(g(k)))).  [resolve(303,c,19,a)].

given #176 (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 #177 (F,wt=16): 403 m == k | b == k | g(g(g(g(k)))) == g(g(g(m))).  [resolve(313,c,20,a)].

given #178 (F,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 (T,wt=16): 415 m == k | b == k | f(f(g(g(k)))) == f(f(g(m))).  [resolve(314,c,19,a)].

given #181 (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 #182 (F,wt=16): 430 m == k | b == k | g(g(f(g(k)))) == g(g(f(m))).  [resolve(322,c,20,a)].

given #183 (F,wt=16): 431 m == k | b == k | f(g(f(g(k)))) == f(g(f(m))).  [resolve(322,c,19,a)].

given #184 (T,wt=16): 441 m == k | b == k | g(f(f(g(k)))) == g(f(f(m))).  [resolve(323,c,20,a)].

given #185 (T,wt=16): 442 m == k | b == k | f(f(f(g(k)))) == f(f(f(m))).  [resolve(323,c,19,a)].

given #186 (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 #187 (F,wt=17): 328 m == k | b == k | p(m,b) | -(g(k) == x) | p(g(m),x).  [resolve(263,c,18,b)].

given #188 (F,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 (T,wt=16): 668 m == k | b == k | p(m,b) | -(g(m) == x) | p(x,m).  [resolve(666,d,17,b)].

given #191 (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 #192 (F,wt=17): 329 m == k | b == k | p(m,b) | -(g(m) == x) | p(x,g(k)).  [resolve(263,c,17,b)].

given #193 (F,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 (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 #196 (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 #197 (F,wt=17): 333 m == k | b == k | p(m,b) | -(g(k) == x) | p(x,g(m)).  [resolve(264,c,17,b)].

given #198 (F,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 (T,wt=16): 683 m == k | b == k | p(m,b) | -(g(m) == x) | p(m,x).  [resolve(682,d,18,b)].

given #201 (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 #202 (F,wt=16): 684 m == k | b == k | p(m,b) | -(m == x) | p(x,g(m)).  [resolve(682,d,17,b)].

given #203 (F,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 (T,wt=17): 340 m == k | b == k | p(m,b) | -(m == x) | p(g(g(k)),x).  [resolve(292,c,18,b)].

given #206 (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 #207 (F,wt=17): 341 m == k | b == k | p(m,b) | -(g(g(k)) == x) | p(x,m).  [resolve(292,c,17,b)].

given #208 (F,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 (T,wt=17): 370 m == k | b == k | -(x == f(g(m))) | x == f(g(g(k))).  [resolve(294,c,16,b)].

given #211 (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 #212 (F,wt=17): 371 m == k | b == k | -(f(g(g(k))) == x) | f(g(m)) == x.  [resolve(294,c,16,a)].

given #213 (F,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 (T,wt=17): 393 m == k | b == k | -(x == f(f(m))) | x == f(f(g(k))).  [resolve(303,c,16,b)].

given #216 (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 #217 (F,wt=17): 394 m == k | b == k | -(f(f(g(k))) == x) | f(f(m)) == x.  [resolve(303,c,16,a)].

given #218 (F,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 (T,wt=17): 416 m == k | b == k | -(x == f(g(g(k)))) | x == f(g(m)).  [resolve(314,c,16,b)].

given #221 (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 #222 (F,wt=17): 417 m == k | b == k | -(f(g(m)) == x) | f(g(g(k))) == x.  [resolve(314,c,16,a)].

given #223 (F,wt=17): 432 m == k | b == k | -(x == g(f(g(k)))) | x == g(f(m)).  [resolve(322,c,16,b)].

given #224 (T,wt=17): 433 m == k | b == k | -(g(f(m)) == x) | g(f(g(k))) == x.  [resolve(322,c,16,a)].

given #225 (T,wt=17): 443 m == k | b == k | -(x == f(f(g(k)))) | x == f(f(m)).  [resolve(323,c,16,b)].

given #226 (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 #227 (F,wt=17): 444 m == k | b == k | -(f(f(m)) == x) | f(f(g(k))) == x.  [resolve(323,c,16,a)].

given #228 (F,wt=18): 445 m == k | b == k | k == b | p(k,b) | -p(m,b) | k == m.  [resolve(275,c,51,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 (T,wt=18): 447 m == k | b == k | k == b | p(k,b) | -(k == x) | p(x,m).  [resolve(275,c,17,b)].

given #231 (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 #232 (F,wt=18): 462 m == k | b == k | g(g(g(g(m)))) == g(g(g(g(g(k))))).  [resolve(355,c,20,a)].

given #233 (F,wt=18): 463 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): 474 m == k | b == k | g(f(g(g(m)))) == g(f(g(g(g(k))))).  [resolve(356,c,20,a)].

given #235 (T,wt=18): 475 m == k | b == k | f(f(g(g(m)))) == f(f(g(g(g(k))))).  [resolve(356,c,19,a)].

given #236 (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 #237 (F,wt=18): 487 m == k | b == k | g(g(f(g(m)))) == g(g(f(g(g(k))))).  [resolve(368,c,20,a)].

given #238 (F,wt=18): 488 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 (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 #241 (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 #242 (F,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 (F,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 (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 #246 (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 #247 (F,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 (F,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): 547 m == k | b == k | g(f(f(f(m)))) == g(f(f(f(g(k))))).  [resolve(392,c,20,a)].

given #250 (T,wt=18): 548 m == k | b == k | f(f(f(f(m)))) == f(f(f(f(g(k))))).  [resolve(392,c,19,a)].

given #251 (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 #252 (F,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 (F,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 (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 #256 (A,wt=27): 145 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 #257 (F,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 (F,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): 599 m == k | b == k | g(f(f(g(g(k))))) == g(f(f(g(m)))).  [resolve(415,c,20,a)].

given #260 (T,wt=18): 600 m == k | b == k | f(f(f(g(g(k))))) == f(f(f(g(m)))).  [resolve(415,c,19,a)].

given #261 (A,wt=27): 148 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 #262 (F,wt=18): 623 m == k | b == k | g(g(g(f(g(k))))) == g(g(g(f(m)))).  [resolve(430,c,20,a)].

given #263 (F,wt=18): 624 m == k | b == k | f(g(g(f(g(k))))) == f(g(g(f(m)))).  [resolve(430,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(431,c,20,a)].

given #265 (T,wt=18): 637 m == k | b == k | f(f(g(f(g(k))))) == f(f(g(f(m)))).  [resolve(431,c,19,a)].

given #266 (A,wt=27): 149 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 #267 (F,wt=18): 650 m == k | b == k | g(g(f(f(g(k))))) == g(g(f(f(m)))).  [resolve(441,c,20,a)].

given #268 (F,wt=18): 651 m == k | b == k | f(g(f(f(g(k))))) == f(g(f(f(m)))).  [resolve(441,c,19,a)].

given #269 (T,wt=18): 661 m == k | b == k | g(f(f(f(g(k))))) == g(f(f(f(m)))).  [resolve(442,c,20,a)].

given #270 (T,wt=18): 662 m == k | b == k | f(f(f(f(g(k))))) == f(f(f(f(m)))).  [resolve(442,c,19,a)].

given #271 (A,wt=25): 150 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 #272 (F,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 (F,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): 677 m == k | b == k | p(m,b) | -(g(g(k)) == x) | p(g(k),x).  [resolve(676,d,18,b)].

given #275 (T,wt=18): 678 m == k | b == k | p(m,b) | -(g(k) == x) | p(x,g(g(k))).  [resolve(676,d,17,b)].

given #276 (A,wt=25): 151 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 #277 (F,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 (F,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 (T,wt=18): 1148 m == k | b == k | g(k) == b | p(g(k),b) | -(g(m) == b).  [factor(1145,d,f)].

given #281 (A,wt=25): 152 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 #282 (F,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 (F,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 (T,wt=19): 450 m == k | b == k | k == b | p(k,b) | k == m | -(f(k) == k).  [resolve(275,c,5,b)].

given #286 (A,wt=25): 153 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 #287 (F,wt=19): 451 m == k | b == k | k == b | p(k,b) | k == m | -(f(k) == m).  [resolve(275,c,4,b)].

given #288 (F,wt=19): 464 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): 465 m == k | b == k | -(g(g(g(g(k)))) == x) | g(g(g(m))) == x.  [resolve(355,c,16,a)].

given #290 (T,wt=19): 476 m == k | b == k | -(x == f(g(g(m)))) | x == f(g(g(g(k)))).  [resolve(356,c,16,b)].

given #291 (A,wt=28): 199 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 #292 (F,wt=19): 477 m == k | b == k | -(f(g(g(g(k)))) == x) | f(g(g(m))) == x.  [resolve(356,c,16,a)].

given #293 (F,wt=19): 489 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): 490 m == k | b == k | -(g(f(g(g(k)))) == x) | g(f(g(m))) == x.  [resolve(368,c,16,a)].

given #295 (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 #296 (A,wt=28): 200 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 #297 (F,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 (F,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 (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 #301 (A,wt=34): 201 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 #302 (F,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 (F,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 (T,wt=19): 549 m == k | b == k | -(x == f(f(f(m)))) | x == f(f(f(g(k)))).  [resolve(392,c,16,b)].

given #306 (A,wt=28): 202 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 #307 (F,wt=19): 550 m == k | b == k | -(f(f(f(g(k)))) == x) | f(f(f(m))) == x.  [resolve(392,c,16,a)].

given #308 (F,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 (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 #311 (A,wt=31): 203 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 #312 (F,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 (F,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 (T,wt=19): 601 m == k | b == k | -(x == f(f(g(g(k))))) | x == f(f(g(m))).  [resolve(415,c,16,b)].

given #316 (A,wt=34): 204 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(201,d,h)].

given #317 (F,wt=19): 602 m == k | b == k | -(f(f(g(m))) == x) | f(f(g(g(k)))) == x.  [resolve(415,c,16,a)].

given #318 (F,wt=19): 625 m == k | b == k | -(x == g(g(f(g(k))))) | x == g(g(f(m))).  [resolve(430,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(430,c,16,a)].

given #320 (T,wt=19): 638 m == k | b == k | -(x == f(g(f(g(k))))) | x == f(g(f(m))).  [resolve(431,c,16,b)].

given #321 (A,wt=32): 234 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,47,e),merge(j),merge(k)].

given #322 (F,wt=19): 639 m == k | b == k | -(f(g(f(m))) == x) | f(g(f(g(k)))) == x.  [resolve(431,c,16,a)].

given #323 (F,wt=19): 652 m == k | b == k | -(x == g(f(f(g(k))))) | x == g(f(f(m))).  [resolve(441,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(441,c,16,a)].

given #325 (T,wt=19): 663 m == k | b == k | -(x == f(f(f(g(k))))) | x == f(f(f(m))).  [resolve(442,c,16,b)].

given #326 (A,wt=32): 235 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,46,d),merge(i)].

given #327 (F,wt=19): 664 m == k | b == k | -(f(f(f(m))) == x) | f(f(f(g(k)))) == x.  [resolve(442,c,16,a)].

given #328 (F,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 (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 #331 (A,wt=32): 236 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 #332 (F,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 (F,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 (T,wt=20): 713 m == k | b == k | g(g(g(g(g(m))))) == g(g(g(g(g(g(k)))))).  [resolve(462,c,20,a)].

given #336 (A,wt=32): 237 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 #337 (F,wt=20): 714 m == k | b == k | f(g(g(g(g(m))))) == f(g(g(g(g(g(k)))))).  [resolve(462,c,19,a)].

given #338 (F,wt=20): 726 m == k | b == k | g(f(g(g(g(m))))) == g(f(g(g(g(g(k)))))).  [resolve(463,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(463,c,19,a)].

given #340 (T,wt=20): 740 m == k | b == k | g(g(f(g(g(m))))) == g(g(f(g(g(g(k)))))).  [resolve(474,c,20,a)].

given #341 (A,wt=38): 238 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 #342 (F,wt=20): 741 m == k | b == k | f(g(f(g(g(m))))) == f(g(f(g(g(g(k)))))).  [resolve(474,c,19,a)].

given #343 (F,wt=20): 751 m == k | b == k | g(f(f(g(g(m))))) == g(f(f(g(g(g(k)))))).  [resolve(475,c,20,a)].

given #344 (T,wt=20): 752 m == k | b == k | f(f(f(g(g(m))))) == f(f(f(g(g(g(k)))))).  [resolve(475,c,19,a)].

given #345 (T,wt=20): 770 m == k | b == k | g(g(g(f(g(m))))) == g(g(g(f(g(g(k)))))).  [resolve(487,c,20,a)].

given #346 (A,wt=32): 239 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 #347 (F,wt=20): 771 m == k | b == k | f(g(g(f(g(m))))) == f(g(g(f(g(g(k)))))).  [resolve(487,c,19,a)].

given #348 (F,wt=20): 783 m == k | b == k | g(f(g(f(g(m))))) == g(f(g(f(g(g(k)))))).  [resolve(488,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(488,c,19,a)].

given #350 (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 #351 (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 #352 (F,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 (F,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 (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 #356 (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 #357 (F,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 (F,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 (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 #361 (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 #362 (F,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 (F,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 (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 #366 (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 #367 (F,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 (F,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 (T,wt=20): 901 m == k | b == k | g(g(f(f(f(m))))) == g(g(f(f(f(g(k)))))).  [resolve(547,c,20,a)].

given #371 (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 #372 (F,wt=20): 902 m == k | b == k | f(g(f(f(f(m))))) == f(g(f(f(f(g(k)))))).  [resolve(547,c,19,a)].

given #373 (F,wt=20): 912 m == k | b == k | g(f(f(f(f(m))))) == g(f(f(f(f(g(k)))))).  [resolve(548,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(548,c,19,a)].

given #375 (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 #376 (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 #377 (F,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 (F,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 (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 #381 (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 #382 (F,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 (F,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 (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 #386 (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 #387 (F,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 (F,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 (T,wt=20): 1005 m == k | b == k | g(g(f(f(g(g(k)))))) == g(g(f(f(g(m))))).  [resolve(599,c,20,a)].

given #391 (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 #392 (F,wt=20): 1006 m == k | b == k | f(g(f(f(g(g(k)))))) == f(g(f(f(g(m))))).  [resolve(599,c,19,a)].

given #393 (F,wt=20): 1016 m == k | b == k | g(f(f(f(g(g(k)))))) == g(f(f(f(g(m))))).  [resolve(600,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(600,c,19,a)].

given #395 (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 #396 (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 #397 (F,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 (F,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 (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 #401 (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 #402 (F,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 (F,wt=20): 1068 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): 1069 m == k | b == k | f(f(f(g(f(g(k)))))) == f(f(f(g(f(m))))).  [resolve(637,c,19,a)].

given #405 (T,wt=20): 1082 m == k | b == k | g(g(g(f(f(g(k)))))) == g(g(g(f(f(m))))).  [resolve(650,c,20,a)].

given #406 (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 #407 (F,wt=20): 1083 m == k | b == k | f(g(g(f(f(g(k)))))) == f(g(g(f(f(m))))).  [resolve(650,c,19,a)].

given #408 (F,wt=20): 1095 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): 1096 m == k | b == k | f(f(g(f(f(g(k)))))) == f(f(g(f(f(m))))).  [resolve(651,c,19,a)].

given #410 (T,wt=20): 1109 m == k | b == k | g(g(f(f(f(g(k)))))) == g(g(f(f(f(m))))).  [resolve(661,c,20,a)].

given #411 (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 #412 (F,wt=20): 1110 m == k | b == k | f(g(f(f(f(g(k)))))) == f(g(f(f(f(m))))).  [resolve(661,c,19,a)].

given #413 (F,wt=20): 1120 m == k | b == k | g(f(f(f(f(g(k)))))) == g(f(f(f(f(m))))).  [resolve(662,c,20,a)].

given #414 (T,wt=20): 1121 m == k | b == k | f(f(f(f(f(g(k)))))) == f(f(f(f(f(m))))).  [resolve(662,c,19,a)].

given #415 (T,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 (A,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 (F,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 (F,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 (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 #421 (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 #422 (F,wt=20): 2121 m == k | b == k | f(m) == b | p(f(m),b) | -(g(f(g(k))) == b).  [factor(2116,d,f)].

given #423 (F,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(462,c,16,b)].

given #425 (T,wt=21): 716 m == k | b == k | -(g(g(g(g(g(k))))) == x) | g(g(g(g(m)))) == x.  [resolve(462,c,16,a)].

given #426 (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 #427 (F,wt=21): 728 m == k | b == k | -(x == f(g(g(g(m))))) | x == f(g(g(g(g(k))))).  [resolve(463,c,16,b)].

given #428 (F,wt=21): 729 m == k | b == k | -(f(g(g(g(g(k))))) == x) | f(g(g(g(m)))) == x.  [resolve(463,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(474,c,16,b)].

given #430 (T,wt=21): 743 m == k | b == k | -(g(f(g(g(g(k))))) == x) | g(f(g(g(m)))) == x.  [resolve(474,c,16,a)].

given #431 (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 #432 (F,wt=21): 753 m == k | b == k | -(x == f(f(g(g(m))))) | x == f(f(g(g(g(k))))).  [resolve(475,c,16,b)].

given #433 (F,wt=21): 754 m == k | b == k | -(f(f(g(g(g(k))))) == x) | f(f(g(g(m)))) == x.  [resolve(475,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(487,c,16,b)].

given #435 (T,wt=21): 773 m == k | b == k | -(g(g(f(g(g(k))))) == x) | g(g(f(g(m)))) == x.  [resolve(487,c,16,a)].

given #436 (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 #437 (F,wt=21): 785 m == k | b == k | -(x == f(g(f(g(m))))) | x == f(g(f(g(g(k))))).  [resolve(488,c,16,b)].

given #438 (F,wt=21): 786 m == k | b == k | -(f(g(f(g(g(k))))) == x) | f(g(f(g(m)))) == x.  [resolve(488,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 (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 #441 (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 #442 (F,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 (F,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 (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 #446 (A,wt=42): 317 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 #447 (F,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 (F,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 (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 #451 (A,wt=42): 318 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 #452 (F,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 (F,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 (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 #456 (A,wt=39): 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),m).  [resolve(279,c,86,f)].

given #457 (F,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 (F,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(547,c,16,b)].

given #460 (T,wt=21): 904 m == k | b == k | -(g(f(f(f(g(k))))) == x) | g(f(f(f(m)))) == x.  [resolve(547,c,16,a)].

given #461 (A,wt=23): 320 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 #462 (F,wt=21): 914 m == k | b == k | -(x == f(f(f(f(m))))) | x == f(f(f(f(g(k))))).  [resolve(548,c,16,b)].

given #463 (F,wt=21): 915 m == k | b == k | -(f(f(f(f(g(k))))) == x) | f(f(f(f(m)))) == x.  [resolve(548,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 (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 #466 (A,wt=23): 321 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 #467 (F,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 (F,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 (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 #471 (A,wt=29): 327 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 #472 (F,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 (F,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 (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 #476 (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 #477 (F,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 (F,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(599,c,16,b)].

given #480 (T,wt=21): 1008 m == k | b == k | -(g(f(f(g(m)))) == x) | g(f(f(g(g(k))))) == x.  [resolve(599,c,16,a)].

given #481 (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 #482 (F,wt=21): 1018 m == k | b == k | -(x == f(f(f(g(g(k)))))) | x == f(f(f(g(m)))).  [resolve(600,c,16,b)].

given #483 (F,wt=21): 1019 m == k | b == k | -(f(f(f(g(m)))) == x) | f(f(f(g(g(k))))) == x.  [resolve(600,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 (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 #486 (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 #487 (F,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 (F,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 (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 #491 (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 #492 (F,wt=21): 1070 m == k | b == k | -(x == f(f(g(f(g(k)))))) | x == f(f(g(f(m)))).  [resolve(637,c,16,b)].

given #493 (F,wt=21): 1071 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): 1084 m == k | b == k | -(x == g(g(f(f(g(k)))))) | x == g(g(f(f(m)))).  [resolve(650,c,16,b)].

given #495 (T,wt=21): 1085 m == k | b == k | -(g(g(f(f(m)))) == x) | g(g(f(f(g(k))))) == x.  [resolve(650,c,16,a)].

given #496 (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 #497 (F,wt=21): 1097 m == k | b == k | -(x == f(g(f(f(g(k)))))) | x == f(g(f(f(m)))).  [resolve(651,c,16,b)].

given #498 (F,wt=21): 1098 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): 1111 m == k | b == k | -(x == g(f(f(f(g(k)))))) | x == g(f(f(f(m)))).  [resolve(661,c,16,b)].

given #500 (T,wt=21): 1112 m == k | b == k | -(g(f(f(f(m)))) == x) | g(f(f(f(g(k))))) == x.  [resolve(661,c,16,a)].

given #501 (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 #502 (F,wt=21): 1122 m == k | b == k | -(x == f(f(f(f(g(k)))))) | x == f(f(f(f(m)))).  [resolve(662,c,16,b)].

given #503 (F,wt=21): 1123 m == k | b == k | -(f(f(f(f(m)))) == x) | f(f(f(f(g(k))))) == x.  [resolve(662,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 (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 #506 (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 #507 (F,wt=18): 2200 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 (F,wt=21): 2208 m == k | b == k | g(k) == b | p(g(m),m) | -(b == x) | p(g(k),x).  [resolve(2200,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(2200,d,17,b)].

given #510 (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 #511 (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 #512 (F,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 (F,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 (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 #516 (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 #517 (F,wt=21): 2219 m == k | b == k | g(k) == b | p(m,g(m)) | -(b == x) | p(g(k),x).  [resolve(2216,d,18,b)].

given #518 (F,wt=21): 2220 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 (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 #521 (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 #522 (F,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 (F,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 (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 #526 (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 #527 (F,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 (F,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 (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 #531 (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 #532 (F,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 (F,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 (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 #536 (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 #537 (F,wt=22): 1257 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 (F,wt=22): 1258 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 (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 #541 (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 #542 (F,wt=22): 1286 m == k | b == k | g(g(f(f(g(g(m)))))) == g(g(f(f(g(g(g(k))))))).  [resolve(751,c,20,a)].

given #543 (F,wt=22): 1287 m == k | b == k | f(g(f(f(g(g(m)))))) == f(g(f(f(g(g(g(k))))))).  [resolve(751,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(752,c,20,a)].

given #545 (T,wt=22): 1298 m == k | b == k | f(f(f(f(g(g(m)))))) == f(f(f(f(g(g(g(k))))))).  [resolve(752,c,19,a)].

given #546 (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 #547 (F,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 (F,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 (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 #551 (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 #552 (F,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 (F,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 (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 #556 (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 #557 (F,wt=22): 1363 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 (F,wt=22): 1364 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 (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 #561 (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 #562 (F,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 (F,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 (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 #566 (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 #567 (F,wt=22): 1418 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 (F,wt=22): 1419 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 (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 #571 (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 #572 (F,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 (F,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 (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 #576 (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 #577 (F,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 (F,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 (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 #581 (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 #582 (F,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 (F,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 (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 #586 (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 #587 (F,wt=22): 1526 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 (F,wt=22): 1527 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 (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 #591 (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 #592 (F,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 (F,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 (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 #596 (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 #597 (F,wt=22): 1580 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 (F,wt=22): 1581 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 (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 #601 (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 #602 (F,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 (F,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 (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 #606 (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 #607 (F,wt=22): 1639 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 (F,wt=22): 1640 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 (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 #611 (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 #612 (F,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 (F,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 (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 #616 (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 #617 (F,wt=22): 1696 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 (F,wt=22): 1697 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 (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 #621 (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 #622 (F,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 (F,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 (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 #626 (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 #627 (F,wt=22): 1753 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 (F,wt=22): 1754 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 (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 #631 (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 #632 (F,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 (F,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 (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 #636 (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 #637 (F,wt=22): 1813 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 (F,wt=22): 1814 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 (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 #641 (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 #642 (F,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 (F,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 (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 #646 (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 #647 (F,wt=22): 1871 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 (F,wt=22): 1872 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 (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 #651 (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 #652 (F,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 (F,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 (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 #656 (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 #657 (F,wt=21): 3748 m == k | b == k | g(g(k)) == b | p(g(g(k)),b) | -(g(g(m)) == b).  [factor(3743,d,f)].

given #658 (F,wt=22): 1929 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): 1930 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 (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 #661 (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 #662 (F,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 (F,wt=22): 1961 m == k | b == k | g(g(f(f(g(f(g(k))))))) == g(g(f(f(g(f(m)))))).  [resolve(1068,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(1068,c,19,a)].

given #665 (T,wt=22): 1972 m == k | b == k | g(f(f(f(g(f(g(k))))))) == g(f(f(f(g(f(m)))))).  [resolve(1069,c,20,a)].

given #666 (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 #667 (F,wt=22): 1973 m == k | b == k | f(f(f(f(g(f(g(k))))))) == f(f(f(f(g(f(m)))))).  [resolve(1069,c,19,a)].

given #668 (F,wt=22): 1986 m == k | b == k | g(g(g(g(f(f(g(k))))))) == g(g(g(g(f(f(m)))))).  [resolve(1082,c,20,a)].

given #669 (T,wt=22): 1987 m == k | b == k | f(g(g(g(f(f(g(k))))))) == f(g(g(g(f(f(m)))))).  [resolve(1082,c,19,a)].

given #670 (T,wt=22): 2004 m == k | b == k | g(f(g(g(f(f(g(k))))))) == g(f(g(g(f(f(m)))))).  [resolve(1083,c,20,a)].

given #671 (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 #672 (F,wt=22): 2005 m == k | b == k | f(f(g(g(f(f(g(k))))))) == f(f(g(g(f(f(m)))))).  [resolve(1083,c,19,a)].

given #673 (F,wt=22): 2018 m == k | b == k | g(g(f(g(f(f(g(k))))))) == g(g(f(g(f(f(m)))))).  [resolve(1095,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(1095,c,19,a)].

given #675 (T,wt=22): 2029 m == k | b == k | g(f(f(g(f(f(g(k))))))) == g(f(f(g(f(f(m)))))).  [resolve(1096,c,20,a)].

given #676 (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 #677 (F,wt=22): 2030 m == k | b == k | f(f(f(g(f(f(g(k))))))) == f(f(f(g(f(f(m)))))).  [resolve(1096,c,19,a)].

given #678 (F,wt=22): 2043 m == k | b == k | g(g(g(f(f(f(g(k))))))) == g(g(g(f(f(f(m)))))).  [resolve(1109,c,20,a)].

given #679 (T,wt=22): 2044 m == k | b == k | f(g(g(f(f(f(g(k))))))) == f(g(g(f(f(f(m)))))).  [resolve(1109,c,19,a)].

given #680 (T,wt=22): 2064 m == k | b == k | g(f(g(f(f(f(g(k))))))) == g(f(g(f(f(f(m)))))).  [resolve(1110,c,20,a)].

given #681 (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 #682 (F,wt=22): 2065 m == k | b == k | f(f(g(f(f(f(g(k))))))) == f(f(g(f(f(f(m)))))).  [resolve(1110,c,19,a)].

given #683 (F,wt=22): 2078 m == k | b == k | g(g(f(f(f(f(g(k))))))) == g(g(f(f(f(f(m)))))).  [resolve(1120,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(1120,c,19,a)].

given #685 (T,wt=22): 2089 m == k | b == k | g(f(f(f(f(f(g(k))))))) == g(f(f(f(f(f(m)))))).  [resolve(1121,c,20,a)].

given #686 (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 #687 (F,wt=22): 2090 m == k | b == k | f(f(f(f(f(f(g(k))))))) == f(f(f(f(f(f(m)))))).  [resolve(1121,c,19,a)].

given #688 (F,wt=23): 426 m == k | b == k | p(f(g(k)),g(f(m))) | f(g(k)) == b | p(f(g(k)),b).  [resolve(322,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 (T,wt=23): 429 m == k | b == k | p(g(f(m)),f(g(k))) | f(g(k)) == b | p(f(g(k)),b).  [resolve(322,c,37,a)].

given #691 (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 #692 (F,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 (F,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 (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 #696 (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 #697 (F,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 (F,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 (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 #701 (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 #702 (F,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 (F,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 (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 #706 (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 #707 (F,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 (F,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 (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 #711 (A,wt=44): 418 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(118,f,313,c)].

given #712 (F,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 (F,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): 1259 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 (T,wt=23): 1260 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 #716 (A,wt=38): 419 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(118,f,302,c)].

given #717 (F,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 (F,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(751,c,16,b)].

given #720 (T,wt=23): 1289 m == k | b == k | -(g(f(f(g(g(g(k)))))) == x) | g(f(f(g(g(m))))) == x.  [resolve(751,c,16,a)].

given #721 (A,wt=38): 420 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(118,f,293,c)].

given #722 (F,wt=23): 1299 m == k | b == k | -(x == f(f(f(g(g(m)))))) | x == f(f(f(g(g(g(k)))))).  [resolve(752,c,16,b)].

given #723 (F,wt=23): 1300 m == k | b == k | -(f(f(f(g(g(g(k)))))) == x) | f(f(f(g(g(m))))) == x.  [resolve(752,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 (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 #726 (A,wt=44): 421 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(f(g(f(g(k)))),g(f(m))).  [resolve(322,c,118,f)].

given #727 (F,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 (F,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 (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 #731 (A,wt=50): 422 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(322,c,107,f)].

given #732 (F,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 (F,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): 1365 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 (T,wt=23): 1366 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 #736 (A,wt=50): 423 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(322,c,101,f)].

given #737 (F,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 (F,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 (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 #741 (A,wt=40): 424 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(322,c,93,f)].

given #742 (F,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 (F,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): 1420 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 (T,wt=23): 1421 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 #746 (A,wt=46): 425 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(322,c,86,f)].

given #747 (F,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 (F,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 (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 #751 (A,wt=27): 427 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(322,c,39,a)].

given #752 (F,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 (F,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 (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 #756 (A,wt=27): 428 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(322,c,38,a)].

given #757 (F,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 (F,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 (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 #761 (A,wt=50): 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)),f(f(f(g(k))))).  [resolve(323,c,107,f)].

given #762 (F,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 (F,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): 1528 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 (T,wt=23): 1529 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 #766 (A,wt=42): 435 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(323,c,106,f)].

given #767 (F,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 (F,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 (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 #771 (A,wt=42): 436 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(323,c,102,f)].

given #772 (F,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 (F,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): 1582 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 (T,wt=23): 1583 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 #776 (A,wt=50): 437 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(323,c,101,f)].

given #777 (F,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 (F,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 (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 #781 (A,wt=46): 438 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(323,c,86,f)].

given #782 (F,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 (F,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): 1641 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 (T,wt=23): 1642 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 #786 (A,wt=27): 439 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(323,c,39,a)].

given #787 (F,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 (F,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 (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 #791 (A,wt=27): 440 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(323,c,38,a)].

given #792 (F,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 (F,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): 1698 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 (T,wt=23): 1699 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 #796 (A,wt=33): 452 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(121,i,95,f),merge(i),merge(j),merge(k),merge(l),merge(m)].

given #797 (F,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 (F,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 (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 #801 (A,wt=46): 453 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,118,f)].

given #802 (F,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 (F,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): 1755 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 (T,wt=23): 1756 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 #806 (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(g(g(g(g(k)))),f(g(g(g(m))))).  [resolve(355,c,107,f)].

given #807 (F,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 (F,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 (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 #811 (A,wt=52): 455 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 #812 (F,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 (F,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): 1815 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 (T,wt=23): 1816 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 #816 (A,wt=42): 456 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 #817 (F,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 (F,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 (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 #821 (A,wt=48): 457 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 #822 (F,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 (F,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): 1873 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 (T,wt=23): 1874 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 #826 (A,wt=25): 458 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 #827 (F,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 (F,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 (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 #831 (A,wt=29): 459 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 #832 (F,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 (F,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): 1931 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 (T,wt=23): 1932 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 #836 (A,wt=29): 460 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 #837 (F,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 (F,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(1068,c,16,b)].

given #840 (T,wt=23): 1964 m == k | b == k | -(g(f(f(g(f(m))))) == x) | g(f(f(g(f(g(k)))))) == x.  [resolve(1068,c,16,a)].

given #841 (A,wt=25): 461 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 #842 (F,wt=23): 1974 m == k | b == k | -(x == f(f(f(g(f(g(k))))))) | x == f(f(f(g(f(m))))).  [resolve(1069,c,16,b)].

given #843 (F,wt=23): 1975 m == k | b == k | -(f(f(f(g(f(m))))) == x) | f(f(f(g(f(g(k)))))) == x.  [resolve(1069,c,16,a)].

given #844 (T,wt=23): 1988 m == k | b == k | -(x == g(g(g(f(f(g(k))))))) | x == g(g(g(f(f(m))))).  [resolve(1082,c,16,b)].

given #845 (T,wt=23): 1989 m == k | b == k | -(g(g(g(f(f(m))))) == x) | g(g(g(f(f(g(k)))))) == x.  [resolve(1082,c,16,a)].

given #846 (A,wt=38): 466 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,119,f)].

given #847 (F,wt=23): 2006 m == k | b == k | -(x == f(g(g(f(f(g(k))))))) | x == f(g(g(f(f(m))))).  [resolve(1083,c,16,b)].

given #848 (F,wt=23): 2007 m == k | b == k | -(f(g(g(f(f(m))))) == x) | f(g(g(f(f(g(k)))))) == x.  [resolve(1083,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(1095,c,16,b)].

given #850 (T,wt=23): 2021 m == k | b == k | -(g(f(g(f(f(m))))) == x) | g(f(g(f(f(g(k)))))) == x.  [resolve(1095,c,16,a)].

given #851 (A,wt=52): 467 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 #852 (F,wt=23): 2031 m == k | b == k | -(x == f(f(g(f(f(g(k))))))) | x == f(f(g(f(f(m))))).  [resolve(1096,c,16,b)].

given #853 (F,wt=23): 2032 m == k | b == k | -(f(f(g(f(f(m))))) == x) | f(f(g(f(f(g(k)))))) == x.  [resolve(1096,c,16,a)].

given #854 (T,wt=23): 2045 m == k | b == k | -(x == g(g(f(f(f(g(k))))))) | x == g(g(f(f(f(m))))).  [resolve(1109,c,16,b)].

given #855 (T,wt=23): 2046 m == k | b == k | -(g(g(f(f(f(m))))) == x) | g(g(f(f(f(g(k)))))) == x.  [resolve(1109,c,16,a)].

given #856 (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(g(g(m)),f(g(g(g(k))))).  [resolve(356,c,106,f)].

given #857 (F,wt=23): 2066 m == k | b == k | -(x == f(g(f(f(f(g(k))))))) | x == f(g(f(f(f(m))))).  [resolve(1110,c,16,b)].

given #858 (F,wt=23): 2067 m == k | b == k | -(f(g(f(f(f(m))))) == x) | f(g(f(f(f(g(k)))))) == x.  [resolve(1110,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(1120,c,16,b)].

given #860 (T,wt=23): 2081 m == k | b == k | -(g(f(f(f(f(m))))) == x) | g(f(f(f(f(g(k)))))) == x.  [resolve(1120,c,16,a)].

given #861 (A,wt=44): 469 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 #862 (F,wt=23): 2091 m == k | b == k | -(x == f(f(f(f(f(g(k))))))) | x == f(f(f(f(f(m))))).  [resolve(1121,c,16,b)].

given #863 (F,wt=23): 2092 m == k | b == k | -(f(f(f(f(f(m))))) == x) | f(f(f(f(f(g(k)))))) == x.  [resolve(1121,c,16,a)].

given #864 (T,wt=23): 4288 m == k | b == k | g(g(m)) == b | p(g(g(m)),b) | -(g(g(g(g(k)))) == b).  [factor(4283,d,f)].

given #865 (T,wt=24): 1817 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 #866 (A,wt=52): 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(f(g(g(m)))),f(g(g(g(k))))).  [resolve(356,c,101,f)].

given #867 (F,wt=24): 1818 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 (F,wt=22): 4329 m == k | b == k | g(m) == b | p(g(m),b) | p(g(g(g(k))),g(g(k))).  [resolve(1818,e,293,c),merge(f),merge(g)].

given #869 (T,wt=24): 1875 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 (T,wt=22): 4336 m == k | b == k | g(m) == b | p(g(m),b) | p(g(g(k)),g(g(g(k)))).  [resolve(1875,e,293,c),merge(f),merge(g)].

given #871 (A,wt=48): 471 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 #872 (F,wt=24): 1876 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 (F,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 (T,wt=22): 4351 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 #876 (A,wt=29): 472 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 #877 (F,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 (F,wt=22): 4364 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 (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 #881 (A,wt=29): 473 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 #882 (F,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 (F,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 (T,wt=24): 2116 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 #886 (A,wt=46): 478 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,118,f)].

given #887 (F,wt=24): 2117 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 (F,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 (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 #891 (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(g(f(g(g(k)))),f(g(f(g(m))))).  [resolve(368,c,107,f)].

given #892 (F,wt=24): 2207 m == k | b == k | g(k) == b | p(g(m),m) | k == b | p(k,b) | k == g(k).  [resolve(2200,d,52,d),merge(g)].

given #893 (F,wt=24): 2218 m == k | b == k | g(k) == b | p(m,g(m)) | k == b | p(k,b) | k == g(k).  [resolve(2216,d,52,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 (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 #896 (A,wt=52): 480 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 #897 (F,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 (F,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 (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 #901 (A,wt=42): 481 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 #902 (F,wt=24): 2292 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 (F,wt=24): 2293 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 (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 #906 (A,wt=48): 482 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 #907 (F,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 #908 (F,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 #909 (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 #910 (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 #911 (A,wt=25): 483 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 #912 (F,wt=23): 4615 m == k | b == k | f(g(m)) == b | p(f(g(m)),b) | -(g(f(g(g(k)))) == b).  [factor(4610,d,f)].

given #913 (F,wt=24): 2350 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): 2351 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 (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(1257,c,20,a)].

given #916 (A,wt=29): 484 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 #917 (F,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(1257,c,19,a)].

given #918 (F,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(1258,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(1258,c,19,a)].

given #920 (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 #921 (A,wt=29): 485 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 #922 (F,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 (F,wt=24): 2407 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): 2408 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 (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 #926 (A,wt=25): 486 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 #927 (F,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 (F,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 (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 #931 (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 #932 (F,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 (F,wt=24): 2464 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): 2465 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 (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 #936 (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 #937 (F,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 (F,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 (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 #941 (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 #942 (F,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 (F,wt=24): 2520 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): 2521 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 (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 #946 (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 #947 (F,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 (F,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 (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 #951 (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 #952 (F,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 (F,wt=24): 2577 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): 2578 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 (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(1363,c,20,a)].

given #956 (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 #957 (F,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(1363,c,19,a)].

given #958 (F,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(1364,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(1364,c,19,a)].

given #960 (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 #961 (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 #962 (F,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 (F,wt=24): 2637 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): 2638 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 (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 #966 (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,118,f)].

given #967 (F,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 (F,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 (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 #971 (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 #972 (F,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 (F,wt=24): 2695 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): 2696 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 (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(1418,c,20,a)].

given #976 (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 #977 (F,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(1418,c,19,a)].

given #978 (F,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(1419,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(1419,c,19,a)].

given #980 (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 #981 (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 #982 (F,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 (F,wt=24): 2753 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): 2754 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 (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 #986 (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 #987 (F,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 (F,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 (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 #991 (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 #992 (F,wt=23): 5527 m == k | b == k | g(f(m)) == b | p(g(f(m)),b) | -(g(g(f(g(k)))) == b).  [factor(5522,d,f)].

given #993 (F,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): 2810 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 (T,wt=24): 2811 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 #996 (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 #997 (F,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 (F,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 (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 #1001 (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 #1002 (F,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 (F,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): 2867 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 (T,wt=24): 2868 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 #1006 (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 #1007 (F,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 (F,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 (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 #1011 (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,119,f)].

given #1012 (F,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 (F,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): 2927 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 (T,wt=24): 2928 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 #1016 (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 #1017 (F,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(1526,c,20,a)].

given #1018 (F,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(1526,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(1527,c,20,a)].

given #1020 (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(1527,c,19,a)].

given #1021 (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 #1022 (F,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 (F,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): 2987 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 (T,wt=24): 2988 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 #1026 (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 #1027 (F,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 (F,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 m == k | b == k | g(f(g(f(