============================== Prover9 =============================== Prover9 (32) version March-2007, March 2007. Process 21147 was started by mccune on cleo, Mon Mar 19 17:05:59 2007 The command was "/home/mccune/bin/prover9 -f wang-eq.in wang3-eq.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file wang-eq.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). end_of_list. % Reading from file wang3-eq.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]. 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(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % 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). 2 m = x | p(x,m) | m = y | y = x | -p(x,y) | -p(y,x). [copy(1),flip(a),flip(c)]. 4 b = x | -p(x,b) | b = y | y = x | -p(x,y) | -p(y,x). [copy(3),flip(a),flip(c)]. 6 k = x | m = x | b = x | -p(x,k). [copy(5),flip(a),flip(b),flip(c)]. 8 m = x | -p(x,m) | f(x) != m. [copy(7),flip(a)]. 10 m = x | -p(x,m) | f(x) != x. [copy(9),flip(a)]. 12 m = x | -p(x,m) | p(x,f(x)). [copy(11),flip(a)]. 14 m = x | -p(x,m) | p(f(x),x). [copy(13),flip(a)]. 16 b = x | p(x,b) | g(x) != b. [copy(15),flip(a)]. 18 b = x | p(x,b) | g(x) != x. [copy(17),flip(a)]. 20 b = x | p(x,b) | p(x,g(x)). [copy(19),flip(a)]. 22 b = x | p(x,b) | p(g(x),x). [copy(21),flip(a)]. 24 k = x | m != x | p(x,k). [copy(23),flip(a),flip(b)]. 26 k = x | b != x | p(x,k). [copy(25),flip(a),flip(b)]. 27 m != b. [assumption]. 29 j = x | -p(x,j) | k = x. [copy(28),flip(a),flip(c)]. 31 j = x | p(x,j) | k != x. [copy(30),flip(a),flip(c)]. 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): 2 m = x | p(x,m) | m = y | y = x | -p(x,y) | -p(y,x). [copy(1),flip(a),flip(c)]. given #2 (I,wt=18): 4 b = x | -p(x,b) | b = y | y = x | -p(x,y) | -p(y,x). [copy(3),flip(a),flip(c)]. given #3 (I,wt=12): 6 k = x | m = x | b = x | -p(x,k). [copy(5),flip(a),flip(b),flip(c)]. given #4 (I,wt=10): 8 m = x | -p(x,m) | f(x) != m. [copy(7),flip(a)]. given #5 (I,wt=10): 10 m = x | -p(x,m) | f(x) != x. [copy(9),flip(a)]. given #6 (I,wt=10): 12 m = x | -p(x,m) | p(x,f(x)). [copy(11),flip(a)]. given #7 (I,wt=10): 14 m = x | -p(x,m) | p(f(x),x). [copy(13),flip(a)]. given #8 (I,wt=10): 16 b = x | p(x,b) | g(x) != b. [copy(15),flip(a)]. given #9 (I,wt=10): 18 b = x | p(x,b) | g(x) != x. [copy(17),flip(a)]. given #10 (I,wt=10): 20 b = x | p(x,b) | p(x,g(x)). [copy(19),flip(a)]. given #11 (I,wt=10): 22 b = x | p(x,b) | p(g(x),x). [copy(21),flip(a)]. given #12 (I,wt=9): 24 k = x | m != x | p(x,k). [copy(23),flip(a),flip(b)]. given #13 (I,wt=9): 26 k = x | b != x | p(x,k). [copy(25),flip(a),flip(b)]. given #14 (I,wt=3): 27 m != b. [assumption]. given #15 (I,wt=9): 29 j = x | -p(x,j) | k = x. [copy(28),flip(a),flip(c)]. given #16 (I,wt=9): 31 j = x | p(x,j) | k != x. [copy(30),flip(a),flip(c)]. given #17 (A,wt=16): 32 p(g(x),b) | p(g(x),g(g(x))) | b = x | p(x,b). [resolve(20,a,16,c(flip))]. given #18 (T,wt=6): 49 k = m | p(m,k). [xx_res(24,b)]. given #19 (T,wt=6): 52 k = b | p(b,k). [xx_res(26,b)]. given #20 (T,wt=6): 61 j = k | p(k,j). [xx_res(31,c)]. given #21 (T,wt=6): 88 p(b,k) | p(m,k). [para(52(a,1),49(a,1)),flip(b),unit_del(b,27)]. given #22 (A,wt=13): 33 p(f(b),b) | p(f(b),g(f(b))) | -p(b,m). [resolve(20,a,10,c(flip)),unit_del(c,27)]. given #23 (T,wt=6): 92 p(b,k) | p(m,b). [para(52(a,1),88(b,2)),merge(b)]. given #24 (T,wt=7): 55 p(m,b) | p(g(m),m). [resolve(27,a,22,a(flip))]. given #25 (T,wt=7): 56 p(m,b) | p(m,g(m)). [resolve(27,a,20,a(flip))]. given #26 (T,wt=9): 79 p(m,k) | j = m | p(m,j). [resolve(49,a,31,c)]. given #27 (A,wt=25): 34 p(x,b) | p(x,g(x)) | b = y | -p(y,x) | b = z | z = y | -p(y,z) | -p(z,y). [para(20(a,1),4(b,2))]. given #28 (T,wt=9): 82 p(b,k) | j = b | p(b,j). [resolve(52,a,31,c)]. given #29 (T,wt=9): 90 p(m,k) | j = m | p(k,j). [para(49(a,1),61(a,2))]. given #30 (T,wt=9): 91 p(b,k) | j = b | p(k,j). [para(52(a,1),61(a,2))]. given #31 (T,wt=10): 57 p(x,b) | p(x,g(x)) | m != x. [para(20(a,1),27(a,2))]. given #32 (A,wt=17): 35 p(x,b) | p(x,g(x)) | b = y | p(y,b) | g(y) != x. [para(20(a,1),16(c,2))]. given #33 (T,wt=10): 58 p(x,b) | p(g(x),x) | m != x. [para(22(a,1),27(a,2))]. given #34 (T,wt=10): 123 p(k,b) | p(k,g(k)) | p(m,k). [resolve(57,c,49,a(flip))]. given #35 (T,wt=10): 126 p(k,b) | p(g(k),k) | p(m,k). [resolve(58,c,49,a(flip))]. given #36 (T,wt=10): 131 p(m,k) | p(k,b) | p(m,g(k)). [para(49(a,1),123(b,1)),merge(d)]. given #37 (A,wt=17): 36 p(x,b) | p(x,g(x)) | x = y | p(y,b) | p(y,g(y)). [para(20(a,1),20(a,1))]. given #38 (T,wt=10): 132 p(m,k) | p(k,b) | p(k,g(m)). [para(49(a,1),123(b,2,1)),merge(d)]. given #39 (T,wt=10): 137 p(m,k) | p(k,b) | p(g(m),k). [para(49(a,1),126(b,1,1)),merge(d)]. given #40 (T,wt=10): 138 p(m,k) | p(k,b) | p(g(k),m). [para(49(a,1),126(b,2)),merge(d)]. given #41 (T,wt=10): 144 p(m,k) | p(m,b) | p(m,g(k)). [para(49(a,1),131(b,1)),merge(b)]. given #42 (A,wt=16): 37 p(g(x),b) | p(g(g(x)),g(x)) | b = x | p(x,b). [resolve(22,a,16,c(flip))]. given #43 (T,wt=10): 151 p(m,k) | p(k,b) | p(m,g(m)). [para(49(a,1),132(c,1)),merge(b)]. given #44 (T,wt=10): 156 p(m,k) | p(k,b) | p(g(m),m). [para(49(a,1),137(c,2)),merge(b)]. given #45 (T,wt=12): 81 p(m,k) | j = x | p(x,j) | m != x. [para(49(a,1),31(c,1))]. given #46 (T,wt=12): 86 p(b,k) | j = x | p(x,j) | b != x. [para(52(a,1),31(c,1))]. given #47 (A,wt=13): 38 p(f(b),b) | p(g(f(b)),f(b)) | -p(b,m). [resolve(22,a,10,c(flip)),unit_del(c,27)]. given #48 (T,wt=12): 89 p(k,j) | j = x | -p(x,k) | k = x. [para(61(a,1),29(b,2))]. given #49 (T,wt=12): 105 p(m,k) | p(m,j) | j = k | p(j,k). [resolve(79,b,24,b(flip)),flip(c)]. given #50 (T,wt=12): 111 p(b,k) | p(b,j) | j = k | p(j,k). [resolve(82,b,26,b(flip)),flip(c)]. given #51 (T,wt=12): 226 p(k,j) | j = m | k = m | p(b,k). [resolve(89,c,88,b)]. given #52 (A,wt=25): 39 p(x,b) | p(g(x),x) | b = y | -p(y,x) | b = z | z = y | -p(y,z) | -p(z,y). [para(22(a,1),4(b,2))]. given #53 (T,wt=9): 232 p(k,j) | k = m | p(b,k). [para(226(b,1),61(a,1)),flip(d),merge(d),merge(e)]. given #54 (T,wt=6): 262 p(k,j) | p(b,k). [para(232(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #55 (T,wt=6): 265 p(b,k) | p(b,j). [para(52(a,1),262(a,1)),merge(c)]. given #56 (T,wt=13): 50 k = x | p(x,k) | p(x,b) | p(g(x),x). [resolve(26,b,22,a)]. given #57 (A,wt=17): 40 p(x,b) | p(g(x),x) | b = y | p(y,b) | g(y) != x. [para(22(a,1),16(c,2))]. given #58 (T,wt=13): 51 k = x | p(x,k) | p(x,b) | p(x,g(x)). [resolve(26,b,20,a)]. given #59 (T,wt=13): 59 j = b | p(b,j) | p(k,b) | p(g(k),k). [resolve(31,c,22,a(flip))]. given #60 (T,wt=13): 60 j = b | p(b,j) | p(k,b) | p(k,g(k)). [resolve(31,c,20,a(flip))]. given #61 (T,wt=13): 64 p(g(m),b) | p(g(m),g(g(m))) | p(m,b). [resolve(32,c,27,a(flip))]. given #62 (A,wt=17): 41 p(x,b) | p(g(x),x) | x = y | p(y,b) | p(y,g(y)). [para(22(a,1),20(a,1))]. given #63 (T,wt=13): 84 p(x,b) | p(x,g(x)) | k = x | p(b,k). [para(20(a,1),52(a,2))]. given #64 (T,wt=13): 85 p(x,b) | p(g(x),x) | k = x | p(b,k). [para(22(a,1),52(a,2))]. given #65 (T,wt=13): 98 p(x,b) | p(x,g(x)) | p(b,k) | p(m,x). [para(20(a,1),92(b,2))]. given #66 (T,wt=13): 99 p(x,b) | p(g(x),x) | p(b,k) | p(m,x). [para(22(a,1),92(b,2))]. given #67 (A,wt=17): 42 p(x,b) | p(x,g(x)) | x = y | p(y,b) | p(g(y),y). [para(20(a,1),22(a,1))]. given #68 (T,wt=13): 101 p(m,b) | g(m) = m | p(f(g(m)),g(m)). [resolve(55,b,14,b),flip(b)]. given #69 (T,wt=9): 361 p(m,b) | p(f(g(m)),g(m)). [resolve(101,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #70 (T,wt=13): 102 p(m,b) | g(m) = m | p(g(m),f(g(m))). [resolve(55,b,12,b),flip(b)]. given #71 (T,wt=9): 371 p(m,b) | p(g(m),f(g(m))). [resolve(102,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #72 (A,wt=17): 43 p(x,b) | p(g(x),x) | x = y | p(y,b) | p(g(y),y). [para(22(a,1),22(a,1))]. given #73 (T,wt=13): 121 p(j,b) | p(j,g(j)) | p(m,k) | p(k,j). [resolve(57,c,90,b(flip))]. given #74 (T,wt=13): 122 p(j,b) | p(j,g(j)) | p(m,k) | p(m,j). [resolve(57,c,79,b(flip))]. given #75 (T,wt=13): 124 p(j,b) | p(g(j),j) | p(m,k) | p(k,j). [resolve(58,c,90,b(flip))]. given #76 (T,wt=13): 125 p(j,b) | p(g(j),j) | p(m,k) | p(m,j). [resolve(58,c,79,b(flip))]. given #77 (A,wt=16): 44 p(b,b) | p(g(b),b) | g(b) = b | g(g(b)) != b. [factor(40,b,d),flip(c)]. given #78 (T,wt=13): 174 p(g(m),b) | p(g(g(m)),g(m)) | p(m,b). [resolve(37,c,27,a(flip))]. given #79 (T,wt=13): 268 p(x,b) | p(x,g(x)) | p(b,k) | p(x,j). [para(20(a,1),265(b,1))]. given #80 (T,wt=13): 269 p(x,b) | p(g(x),x) | p(b,k) | p(x,j). [para(22(a,1),265(b,1))]. given #81 (T,wt=13): 318 p(k,b) | p(g(k),k) | j = k | p(b,j). [factor(312,a,e),merge(e)]. given #82 (A,wt=16): 53 p(x,b) | p(x,g(x)) | k = y | x != y | p(y,k). [para(20(a,1),26(b,1))]. given #83 (T,wt=13): 326 p(k,b) | p(k,g(k)) | j = k | p(b,j). [factor(320,a,e),merge(e)]. given #84 (T,wt=13): 390 p(k,j) | p(j,b) | p(k,g(j)) | p(m,k). [para(61(a,1),121(b,1)),merge(e)]. given #85 (T,wt=13): 391 p(k,j) | p(j,b) | p(j,g(k)) | p(m,k). [para(61(a,1),121(b,2,1)),merge(e)]. given #86 (T,wt=13): 394 p(m,k) | p(k,j) | p(j,b) | p(m,g(j)). [para(90(b,1),121(b,1)),merge(e),merge(f)]. given #87 (A,wt=16): 54 p(x,b) | p(g(x),x) | k = y | x != y | p(y,k). [para(22(a,1),26(b,1))]. given #88 (T,wt=13): 395 p(m,k) | p(k,j) | p(j,b) | p(j,g(m)). [para(90(b,1),121(b,2,1)),merge(e),merge(f)]. given #89 (T,wt=13): 403 p(m,k) | p(m,j) | p(j,b) | p(m,g(j)). [para(79(b,1),122(b,1)),merge(e),merge(f)]. given #90 (T,wt=13): 404 p(m,k) | p(m,j) | p(j,b) | p(j,g(m)). [para(79(b,1),122(b,2,1)),merge(e),merge(f)]. given #91 (T,wt=13): 413 p(k,j) | p(j,b) | p(g(k),j) | p(m,k). [para(61(a,1),124(b,1,1)),merge(e)]. given #92 (A,wt=19): 62 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | k = x | p(x,k). [resolve(32,c,26,b)]. given #93 (T,wt=13): 414 p(k,j) | p(j,b) | p(g(j),k) | p(m,k). [para(61(a,1),124(b,2)),merge(e)]. given #94 (T,wt=13): 417 p(m,k) | p(k,j) | p(j,b) | p(g(m),j). [para(90(b,1),124(b,1,1)),merge(e),merge(f)]. given #95 (T,wt=13): 418 p(m,k) | p(k,j) | p(j,b) | p(g(j),m). [para(90(b,1),124(b,2)),merge(e),merge(f)]. given #96 (T,wt=13): 425 p(m,k) | p(m,j) | p(j,b) | p(g(m),j). [para(79(b,1),125(b,1,1)),merge(e),merge(f)]. given #97 (A,wt=19): 63 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | j = b | p(b,j). [resolve(32,c,31,c(flip))]. given #98 (T,wt=13): 426 p(m,k) | p(m,j) | p(j,b) | p(g(j),m). [para(79(b,1),125(b,2)),merge(e),merge(f)]. given #99 (T,wt=13): 463 p(x,b) | p(x,g(x)) | p(x,k) | p(x,j). [factor(455,a,c),merge(c)]. given #100 (T,wt=13): 477 p(k,b) | p(g(k),k) | p(b,j) | k = b. [para(318(c,1),59(a,1)),merge(e),merge(f),merge(g)]. given #101 (T,wt=13): 479 p(k,b) | p(k,g(k)) | p(b,j) | k = b. [para(326(c,1),60(a,1)),merge(e),merge(f),merge(g)]. given #102 (A,wt=23): 65 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | b = x | p(x,b). [resolve(32,c,16,c(flip))]. given #103 (T,wt=13): 486 p(k,j) | p(k,b) | p(k,g(j)) | p(m,k). [para(61(a,1),390(b,1)),merge(b)]. given #104 (T,wt=13): 488 p(m,k) | p(k,j) | p(m,b) | p(k,g(j)). [para(90(b,1),390(b,1)),merge(c),merge(f)]. given #105 (T,wt=13): 497 p(k,j) | p(j,b) | p(k,g(k)) | p(m,k). [para(61(a,1),391(c,1)),merge(b)]. given #106 (T,wt=13): 499 p(m,k) | p(k,j) | p(j,b) | p(m,g(k)). [para(90(b,1),391(c,1)),merge(c),merge(f)]. given #107 (A,wt=20): 66 p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(b,m). [resolve(32,c,10,c(flip)),unit_del(d,27)]. given #108 (T,wt=13): 508 p(k,j) | p(m,k) | p(k,b) | p(m,g(j)). [para(61(a,1),394(c,1)),merge(c)]. given #109 (T,wt=13): 510 p(m,k) | p(k,j) | p(m,b) | p(m,g(j)). [para(90(b,1),394(c,1)),merge(c),merge(d)]. given #110 (T,wt=13): 519 p(k,j) | p(m,k) | p(j,b) | p(k,g(m)). [para(61(a,1),395(d,1)),merge(c)]. given #111 (T,wt=13): 521 p(m,k) | p(k,j) | p(j,b) | p(m,g(m)). [para(90(b,1),395(d,1)),merge(c),merge(d)]. given #112 (A,wt=31): 67 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | b = y | -p(y,x) | b = z | z = y | -p(y,z) | -p(z,y). [para(32(c,1),4(b,2))]. given #113 (T,wt=13): 528 p(m,k) | p(m,j) | p(m,b) | p(m,g(j)). [para(79(b,1),403(c,1)),merge(c),merge(d)]. given #114 (T,wt=13): 538 p(m,k) | p(m,j) | p(j,b) | p(m,g(m)). [para(79(b,1),404(d,1)),merge(c),merge(d)]. given #115 (T,wt=13): 546 p(k,j) | p(j,b) | p(g(k),k) | p(m,k). [para(61(a,1),413(c,2)),merge(b)]. given #116 (T,wt=13): 548 p(m,k) | p(k,j) | p(j,b) | p(g(k),m). [para(90(b,1),413(c,2)),merge(c),merge(f)]. given #117 (A,wt=23): 68 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | b = y | p(y,b) | g(y) != x. [para(32(c,1),16(c,2))]. given #118 (T,wt=13): 581 p(m,k) | p(k,j) | p(j,b) | p(g(m),k). [para(90(b,1),414(c,1,1)),merge(c),merge(f)]. given #119 (T,wt=13): 594 p(m,k) | p(k,j) | p(j,b) | p(g(m),m). [para(90(b,1),417(d,2)),merge(c),merge(d)]. given #120 (T,wt=13): 613 p(m,k) | p(m,j) | p(j,b) | p(g(m),m). [para(79(b,1),425(d,2)),merge(c),merge(d)]. given #121 (T,wt=13): 729 p(k,j) | p(m,k) | p(m,b) | p(k,g(k)). [para(61(a,1),488(d,2,1)),merge(c)]. given #122 (A,wt=23): 69 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | x = y | p(y,b) | p(y,g(y)). [para(32(c,1),20(a,1))]. given #123 (T,wt=13): 731 p(m,k) | p(k,j) | p(m,b) | p(k,g(m)). [para(90(b,1),488(d,2,1)),merge(c),merge(d)]. given #124 (T,wt=13): 765 p(m,k) | p(m,j) | p(k,b) | p(m,g(j)). [para(49(a,1),508(a,1)),merge(c)]. given #125 (T,wt=14): 96 p(f(b),b) | p(f(b),g(f(b))) | -p(f(b),m). [factor(93,a,c),merge(c)]. given #126 (T,wt=14): 223 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(b),m). [factor(220,a,c),merge(c)]. given #127 (A,wt=23): 70 p(x,b) | p(x,g(x)) | p(g(y),b) | p(g(y),g(g(y))) | x = y | p(y,b). [para(20(a,1),32(c,1))]. given #128 (T,wt=15): 80 p(m,k) | k = x | m = x | b = x | -p(x,m). [para(49(a,1),6(d,2))]. given #129 (T,wt=15): 83 p(b,k) | k = x | m = x | b = x | -p(x,b). [para(52(a,1),6(d,2))]. given #130 (T,wt=15): 97 p(b,k) | b = x | m = x | -p(m,x) | -p(x,m). [resolve(92,b,4,b),flip(b),flip(d),unit_del(b,27)]. given #131 (T,wt=15): 106 p(m,k) | p(m,j) | j = x | -p(x,m) | k = x. [para(79(b,1),29(b,2))]. given #132 (A,wt=23): 71 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | x = y | p(y,b) | p(g(y),y). [para(32(c,1),22(a,1))]. given #133 (T,wt=15): 116 p(m,k) | p(k,j) | j = x | -p(x,m) | k = x. [para(90(b,1),29(b,2))]. given #134 (T,wt=15): 266 p(b,k) | j = m | p(j,m) | j = b | -p(j,b). [resolve(265,b,2,f),flip(b),flip(e),unit_del(d,27)]. given #135 (T,wt=15): 267 p(b,k) | p(b,m) | j = m | j = b | -p(j,b). [resolve(265,b,2,e),flip(d),unit_del(b,27)]. given #136 (T,wt=15): 1071 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(b)),m). [factor(1066,a,c),merge(c)]. given #137 (A,wt=23): 72 p(x,b) | p(g(x),x) | p(g(y),b) | p(g(y),g(g(y))) | x = y | p(y,b). [para(22(a,1),32(c,1))]. given #138 (T,wt=15): 1077 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(b)),m). [factor(1073,a,c),merge(c)]. given #139 (T,wt=16): 74 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | m != x. [para(32(c,1),27(a,2))]. given #140 (T,wt=16): 160 p(m,k) | p(k,b) | g(k) = m | p(f(g(k)),g(k)). [resolve(138,c,14,b),flip(c)]. given #141 (T,wt=12): 1123 p(m,k) | p(k,b) | p(f(g(k)),g(k)). [para(160(c,1),126(b,1)),merge(d),merge(e),merge(f)]. given #142 (A,wt=22): 73 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | k = y | x != y | p(y,k). [para(32(c,1),26(b,1))]. given #143 (T,wt=12): 1135 p(m,k) | p(k,b) | p(f(g(m)),g(k)). [para(49(a,1),1123(c,1,1,1)),merge(b)]. given #144 (T,wt=12): 1136 p(m,k) | p(k,b) | p(f(g(k)),g(m)). [para(49(a,1),1123(c,2,1)),merge(b)]. given #145 (T,wt=12): 1158 p(m,k) | p(k,b) | p(f(g(m)),g(m)). [para(49(a,1),1135(c,2,1)),merge(b)]. given #146 (T,wt=16): 161 p(m,k) | p(k,b) | g(k) = m | p(g(k),f(g(k))). [resolve(138,c,12,b),flip(c)]. given #147 (A,wt=29): 75 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(g(y),b) | p(g(y),g(g(y))) | x = y | p(y,b). [para(32(c,1),32(c,1))]. given #148 (T,wt=12): 1205 p(m,k) | p(k,b) | p(g(k),f(g(k))). [para(161(c,1),126(b,1)),merge(d),merge(e),merge(f)]. given #149 (T,wt=12): 1220 p(m,k) | p(k,b) | p(g(m),f(g(k))). [para(49(a,1),1205(c,1,1)),merge(b)]. given #150 (T,wt=12): 1221 p(m,k) | p(k,b) | p(g(k),f(g(m))). [para(49(a,1),1205(c,2,1,1)),merge(b)]. given #151 (T,wt=12): 1243 p(m,k) | p(k,b) | p(g(m),f(g(m))). [para(49(a,1),1220(c,2,1,1)),merge(b)]. given #152 (A,wt=22): 76 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = b | g(g(x)) != x. [factor(68,a,e),flip(d)]. given #153 (T,wt=16): 184 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | m != x. [para(37(c,1),27(a,2))]. given #154 (T,wt=16): 272 p(x,k) | p(x,b) | p(g(x),x) | j = x | p(x,j). [resolve(50,a,31,c)]. given #155 (T,wt=16): 277 p(x,k) | p(x,b) | p(g(x),x) | m = x | p(m,k). [para(50(a,1),49(a,1)),flip(d)]. given #156 (T,wt=13): 1311 p(x,k) | p(x,b) | p(g(x),x) | p(m,k). [resolve(277,d,58,c),merge(e),merge(f)]. given #157 (A,wt=17): 77 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = x. [factor(69,a,e),flip(d),merge(e)]. given #158 (T,wt=16): 278 p(x,k) | p(x,b) | p(g(x),x) | j = x | p(k,j). [para(50(a,1),61(a,2))]. given #159 (T,wt=16): 296 p(x,k) | p(x,b) | p(x,g(x)) | m = x | p(m,k). [para(51(a,1),49(a,1)),flip(d)]. given #160 (T,wt=13): 1335 p(x,k) | p(x,b) | p(x,g(x)) | p(m,k). [resolve(296,d,57,c),merge(e),merge(f)]. given #161 (T,wt=13): 1373 p(x,k) | p(x,b) | p(x,g(x)) | p(m,x). [factor(1358,a,d),merge(d),merge(e)]. given #162 (A,wt=19): 87 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | k = x | p(b,k). [para(32(c,1),52(a,2))]. given #163 (T,wt=16): 297 p(x,k) | p(x,b) | p(x,g(x)) | j = x | p(k,j). [para(51(a,1),61(a,2))]. given #164 (T,wt=16): 350 p(j,b) | p(j,g(j)) | p(b,k) | j = m | k = m. [resolve(98,d,29,b)]. given #165 (T,wt=13): 1400 p(j,b) | p(j,g(j)) | p(b,k) | k = m. [resolve(350,d,57,c(flip)),merge(e),merge(f)]. given #166 (T,wt=10): 1407 p(j,b) | p(j,g(j)) | p(b,k). [para(1400(d,1),52(a,1)),merge(e),unit_del(d,27)]. given #167 (A,wt=20): 93 p(x,b) | p(x,g(x)) | p(f(b),b) | p(f(b),g(f(b))) | -p(x,m). [para(20(a,1),33(c,1))]. given #168 (T,wt=16): 405 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(j)). [para(105(c,1),122(b,1)),merge(f),merge(g)]. given #169 (T,wt=13): 1432 p(m,k) | p(m,j) | p(j,b) | p(k,g(j)). [para(79(b,1),405(c,1)),merge(c),merge(d),merge(e)]. given #170 (T,wt=13): 1440 p(m,k) | p(m,j) | p(m,b) | p(k,g(j)). [para(79(b,1),1432(c,1)),merge(c),merge(d)]. given #171 (T,wt=13): 1455 p(m,k) | p(m,j) | p(m,b) | p(k,g(m)). [para(79(b,1),1440(d,2,1)),merge(c),merge(d)]. given #172 (A,wt=20): 94 p(x,b) | p(g(x),x) | p(f(b),b) | p(f(b),g(f(b))) | -p(x,m). [para(22(a,1),33(c,1))]. given #173 (T,wt=16): 406 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(j,g(k)). [para(105(c,1),122(b,2,1)),merge(f),merge(g)]. given #174 (T,wt=16): 427 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),j). [para(105(c,1),125(b,1,1)),merge(f),merge(g)]. given #175 (T,wt=16): 428 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(j),k). [para(105(c,1),125(b,2)),merge(f),merge(g)]. given #176 (T,wt=16): 458 p(m,k) | p(x,b) | p(x,g(x)) | p(b,m) | p(x,j). [para(49(a,1),268(c,2))]. given #177 (A,wt=26): 95 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(x,m). [para(32(c,1),33(c,1))]. given #178 (T,wt=16): 462 p(k,b) | p(k,g(k)) | p(k,j) | j = b | k = b. [factor(452,c,d)]. given #179 (T,wt=13): 1557 p(k,b) | p(k,g(k)) | p(k,j) | k = b. [para(462(d,1),61(a,1)),flip(e),merge(e),merge(f)]. given #180 (T,wt=13): 1560 p(k,b) | p(k,g(k)) | p(k,j) | j = b. [para(1557(d,1),61(a,2)),merge(e)]. given #181 (T,wt=13): 1564 p(k,b) | p(k,g(k)) | p(k,j) | p(b,b). [factor(1562,a,d),merge(d),merge(f)]. given #182 (A,wt=19): 100 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,k) | p(m,x). [para(32(c,1),92(b,2))]. given #183 (T,wt=16): 539 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(m)). [para(105(c,1),404(d,1)),merge(d),merge(e)]. given #184 (T,wt=13): 1610 p(m,k) | p(m,j) | p(j,b) | p(k,g(m)). [para(79(b,1),539(c,1)),merge(c),merge(d),merge(e)]. given #185 (T,wt=16): 614 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(m),k). [para(105(c,1),425(d,2)),merge(d),merge(e)]. given #186 (T,wt=16): 638 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),m). [para(105(c,1),426(d,1,1)),merge(d),merge(e)]. given #187 (A,wt=19): 103 p(m,b) | g(m) = b | -p(g(m),b) | g(m) = m | -p(m,g(m)). [resolve(55,b,4,e),flip(b),flip(d),flip(e),unit_del(d,27)]. given #188 (T,wt=16): 1107 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(b))),m). [factor(1102,a,c),merge(c)]. given #189 (T,wt=16): 1113 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(b))),m). [factor(1109,a,c),merge(c)]. given #190 (T,wt=16): 1116 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(m,k). [resolve(74,d,49,a(flip))]. given #191 (T,wt=16): 1288 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | p(m,k). [resolve(184,d,49,a(flip))]. given #192 (A,wt=19): 104 p(m,b) | g(m) = b | -p(g(m),b) | g(m) = m | -p(g(m),m). [resolve(56,b,4,f),flip(b),flip(d),flip(e),unit_del(d,27)]. given #193 (T,wt=15): 1694 p(m,b) | g(m) = b | -p(g(m),b) | g(m) = m. [resolve(104,e,55,b),merge(e)]. given #194 (T,wt=16): 1308 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | j = k. [factor(1290,a,f)]. given #195 (T,wt=16): 1377 p(k,b) | p(k,g(k)) | p(b,j) | p(k,k) | p(m,b). [factor(1361,a,e),merge(e)]. given #196 (T,wt=16): 1390 p(j,k) | p(j,b) | p(j,g(j)) | j = m | k = m. [resolve(1373,d,29,b)]. given #197 (A,wt=25): 107 p(x,b) | p(x,g(x)) | -p(m,x) | g(m) = b | g(m) = m | -p(g(m),m) | p(m,b). [resolve(34,g,56,b),flip(c),flip(e),unit_del(c,27)]. given #198 (T,wt=13): 1728 p(j,k) | p(j,b) | p(j,g(j)) | k = m. [resolve(1390,d,57,c(flip)),merge(e),merge(f)]. given #199 (T,wt=13): 1752 p(j,k) | p(j,b) | p(j,g(j)) | j = m. [factor(1744,a,e),flip(d),merge(e),merge(f)]. given #200 (T,wt=10): 1757 p(j,k) | p(j,b) | p(j,g(j)). [resolve(1752,d,57,c(flip)),merge(d),merge(e)]. given #201 (T,wt=13): 1770 p(k,j) | p(j,k) | p(j,b) | p(k,g(j)). [para(61(a,1),1757(c,1))]. given #202 (A,wt=32): 127 p(k,b) | p(m,k) | p(x,b) | p(x,g(x)) | g(k) = b | -p(g(k),x) | k = b | g(k) = k | -p(g(k),k). [resolve(123,b,34,h),flip(e),flip(g),flip(h)]. given #203 (T,wt=13): 1771 p(k,j) | p(j,k) | p(j,b) | p(j,g(k)). [para(61(a,1),1757(c,2,1))]. given #204 (T,wt=13): 1794 p(k,j) | p(k,k) | p(j,b) | p(k,g(j)). [para(61(a,1),1770(b,1)),merge(b)]. given #205 (T,wt=13): 1824 p(k,j) | p(j,k) | p(j,b) | p(k,g(k)). [para(61(a,1),1771(d,1)),merge(b)]. given #206 (T,wt=13): 1843 p(k,j) | p(k,k) | p(k,b) | p(k,g(j)). [para(61(a,1),1794(c,1)),merge(b)]. given #207 (A,wt=31): 128 p(k,b) | p(m,k) | p(x,b) | p(x,g(x)) | k = b | -p(k,x) | g(k) = b | g(k) = k | -p(g(k),k). [resolve(123,b,34,g),flip(e),flip(g)]. given #208 (T,wt=13): 1849 p(k,j) | p(k,k) | p(j,b) | p(k,g(k)). [para(61(a,1),1824(b,1)),merge(b)]. given #209 (T,wt=13): 1858 p(k,b) | p(k,g(k)) | p(k,j) | p(j,b). [para(1557(d,1),1824(b,2)),merge(d),merge(f),merge(g)]. given #210 (T,wt=10): 1911 p(k,j) | p(k,b) | p(k,g(k)). [para(61(a,1),1858(d,1)),merge(d),merge(e)]. given #211 (T,wt=16): 1442 p(m,k) | p(m,j) | p(j,k) | p(k,b) | p(k,g(j)). [para(105(c,1),1432(c,1)),merge(d),merge(e)]. given #212 (A,wt=25): 130 p(k,b) | p(m,k) | g(k) = b | -p(g(k),b) | k = b | g(k) = k | -p(g(k),k). [resolve(123,b,4,f),flip(c),flip(e),flip(f)]. given #213 (T,wt=13): 1940 p(m,k) | p(m,j) | p(k,b) | p(k,g(j)). [para(79(b,1),1442(c,1)),merge(c),merge(d),merge(e)]. given #214 (T,wt=16): 1456 p(m,k) | p(m,j) | p(j,k) | p(m,b) | p(k,g(k)). [para(105(c,1),1440(d,2,1)),merge(d),merge(e)]. given #215 (T,wt=13): 1967 p(m,k) | p(m,j) | p(m,b) | p(k,g(k)). [para(79(b,1),1456(c,1)),merge(c),merge(d),merge(e)]. given #216 (T,wt=16): 1481 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(m,g(k)). [para(79(b,1),406(e,1)),merge(c),merge(d)]. given #217 (A,wt=18): 135 p(k,b) | p(m,k) | g(k) = k | g(k) = m | g(k) = b. [resolve(126,b,6,d),flip(c),flip(d),flip(e)]. given #218 (T,wt=13): 1989 p(m,k) | p(m,j) | p(j,b) | p(m,g(k)). [para(79(b,1),1481(c,1)),merge(c),merge(d),merge(e)]. given #219 (T,wt=14): 1993 p(m,k) | p(k,b) | g(k) = m | g(k) = b. [para(49(a,1),135(c,2)),merge(c),merge(e)]. given #220 (T,wt=10): 2009 p(m,k) | p(k,b) | g(k) = b. [para(1993(c,1),126(b,1)),merge(d),merge(e),merge(f)]. given #221 (T,wt=6): 2018 p(m,k) | p(k,b). [para(2009(c,1),123(b,2)),merge(c),merge(d),merge(e)]. given #222 (A,wt=20): 145 p(k,b) | p(k,g(k)) | p(x,b) | p(x,g(x)) | j = x | p(x,j). [resolve(36,c,31,c)]. given #223 (T,wt=6): 2026 p(m,k) | p(m,b). [para(49(a,1),2018(b,1)),merge(b)]. given #224 (T,wt=12): 2038 p(m,b) | p(k,j) | j = m | k = m. [resolve(2026,a,89,c)]. given #225 (T,wt=9): 2058 p(m,b) | p(k,j) | k = m. [para(2038(c,1),61(a,1)),flip(d),merge(d),merge(e)]. given #226 (T,wt=9): 2065 p(m,b) | p(k,j) | j = m. [para(2058(c,1),61(a,2)),merge(d)]. given #227 (A,wt=23): 146 p(f(x),b) | p(f(x),g(f(x))) | p(x,b) | p(x,g(x)) | m = x | -p(x,m). [resolve(36,c,10,c)]. given #228 (T,wt=9): 2078 p(m,b) | p(k,j) | p(m,m). [para(2058(c,1),2026(a,2)),merge(d)]. given #229 (T,wt=13): 2023 p(x,b) | p(x,g(x)) | p(m,k) | p(k,x). [para(20(a,1),2018(b,2))]. given #230 (T,wt=13): 2024 p(x,b) | p(g(x),x) | p(m,k) | p(k,x). [para(22(a,1),2018(b,2))]. given #231 (T,wt=13): 2051 p(k,b) | p(g(k),k) | p(b,j) | p(m,b). [para(477(d,1),2026(a,2)),merge(e)]. given #232 (A,wt=19): 169 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | k = x | p(x,k). [resolve(37,c,26,b)]. given #233 (T,wt=13): 2052 p(k,b) | p(k,g(k)) | p(b,j) | p(m,b). [para(479(d,1),2026(a,2)),merge(e)]. given #234 (T,wt=13): 2062 p(m,b) | p(k,j) | p(k,b) | p(g(k),k). [resolve(2058,c,58,c(flip))]. given #235 (T,wt=13): 2076 p(m,b) | p(k,j) | p(k,b) | p(m,g(k)). [para(2058(c,1),1911(c,1)),merge(c)]. given #236 (T,wt=13): 2077 p(m,b) | p(k,j) | p(k,b) | p(k,g(m)). [para(2058(c,1),1911(c,2,1)),merge(c)]. given #237 (A,wt=19): 173 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | j = b | p(b,j). [resolve(37,c,31,c(flip))]. given #238 (T,wt=13): 2081 p(m,b) | p(k,j) | p(j,b) | p(g(j),j). [resolve(2065,c,58,c(flip))]. given #239 (T,wt=13): 2082 p(m,b) | p(k,j) | p(j,b) | p(j,g(j)). [resolve(2065,c,57,c(flip))]. given #240 (T,wt=13): 2085 p(m,b) | p(k,j) | p(k,k) | p(k,g(j)). [para(2065(c,1),1794(c,1)),merge(c),merge(e)]. given #241 (T,wt=13): 2086 p(m,b) | p(k,j) | p(k,k) | p(k,g(k)). [para(2065(c,1),1849(c,1)),merge(c),merge(e)]. given #242 (A,wt=23): 175 p(g(g(x)),b) | p(g(g(g(x))),g(g(x))) | p(g(x),b) | b = x | p(x,b). [resolve(37,c,16,c(flip))]. given #243 (T,wt=13): 2121 p(m,k) | p(x,b) | p(x,g(x)) | p(m,x). [para(49(a,1),2023(d,1)),merge(d)]. given #244 (T,wt=13): 2222 p(m,b) | p(k,j) | p(k,b) | p(g(m),k). [para(2058(c,1),2062(d,1,1)),merge(c),merge(d)]. given #245 (T,wt=13): 2223 p(m,b) | p(k,j) | p(k,b) | p(g(k),m). [para(2058(c,1),2062(d,2)),merge(c),merge(d)]. given #246 (T,wt=13): 2286 p(k,j) | p(m,b) | p(j,b) | p(g(k),j). [para(61(a,1),2081(d,1,1)),merge(c)]. given #247 (A,wt=20): 176 p(g(f(b)),b) | p(g(g(f(b))),g(f(b))) | p(f(b),b) | -p(b,m). [resolve(37,c,10,c(flip)),unit_del(d,27)]. given #248 (T,wt=13): 2287 p(k,j) | p(m,b) | p(j,b) | p(g(j),k). [para(61(a,1),2081(d,2)),merge(c)]. given #249 (T,wt=13): 2294 p(m,b) | p(k,j) | p(j,b) | p(g(m),j). [para(2065(c,1),2081(d,1,1)),merge(c),merge(d)]. given #250 (T,wt=13): 2295 p(m,b) | p(k,j) | p(j,b) | p(g(j),m). [para(2065(c,1),2081(d,2)),merge(c),merge(d)]. given #251 (T,wt=13): 2304 p(k,j) | p(m,b) | p(j,b) | p(k,g(j)). [para(61(a,1),2082(d,1)),merge(c)]. given #252 (A,wt=31): 177 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | b = y | -p(y,x) | b = z | z = y | -p(y,z) | -p(z,y). [para(37(c,1),4(b,2))]. given #253 (T,wt=10): 2569 p(m,b) | p(k,j) | p(k,g(j)). [para(2065(c,1),2304(c,1)),merge(c),merge(d),merge(e)]. given #254 (T,wt=10): 2754 p(k,j) | p(m,b) | p(k,g(k)). [para(61(a,1),2569(c,2,1)),merge(c)]. given #255 (T,wt=10): 2761 p(m,b) | p(k,j) | p(m,g(j)). [para(2058(c,1),2569(c,1)),merge(c),merge(d)]. given #256 (T,wt=10): 2762 p(m,b) | p(k,j) | p(k,g(m)). [para(2065(c,1),2569(c,2,1)),merge(c),merge(d)]. given #257 (A,wt=23): 178 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | b = y | p(y,b) | g(y) != x. [para(37(c,1),16(c,2))]. given #258 (T,wt=10): 2782 p(m,b) | p(k,j) | p(m,g(k)). [para(2058(c,1),2754(c,1)),merge(c),merge(d)]. given #259 (T,wt=13): 2305 p(k,j) | p(m,b) | p(j,b) | p(j,g(k)). [para(61(a,1),2082(d,2,1)),merge(c)]. given #260 (T,wt=13): 2313 p(m,b) | p(k,j) | p(j,b) | p(j,g(m)). [para(2065(c,1),2082(d,2,1)),merge(c),merge(d)]. given #261 (T,wt=13): 2498 p(k,j) | p(m,b) | p(j,b) | p(g(k),k). [para(61(a,1),2286(d,2)),merge(b)]. given #262 (A,wt=23): 179 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | x = y | p(y,b) | p(y,g(y)). [para(37(c,1),20(a,1))]. given #263 (T,wt=13): 2502 p(m,b) | p(k,j) | p(j,b) | p(g(k),m). [para(2065(c,1),2286(d,2)),merge(c),merge(d)]. given #264 (T,wt=13): 2528 p(m,b) | p(k,j) | p(j,b) | p(g(m),k). [para(2065(c,1),2287(d,1,1)),merge(c),merge(d)]. given #265 (T,wt=15): 2048 p(m,b) | k = b | -p(k,b) | k = m | -p(k,m). [resolve(2026,a,4,f),flip(b),flip(d),flip(e),unit_del(d,27)]. given #266 (T,wt=15): 2064 p(m,b) | p(k,j) | j = x | p(x,j) | m != x. [para(2058(c,1),31(c,1))]. given #267 (A,wt=23): 180 p(x,b) | p(x,g(x)) | p(g(y),b) | p(g(g(y)),g(y)) | x = y | p(y,b). [para(20(a,1),37(c,1))]. given #268 (T,wt=15): 2066 p(m,b) | p(k,j) | j = x | -p(x,m) | k = x. [para(2058(c,1),89(c,2)),merge(c)]. given #269 (T,wt=14): 2933 p(m,b) | p(k,j) | g(m) = j | g(m) = k. [resolve(2066,d,55,b),flip(c),flip(d),merge(e)]. given #270 (T,wt=10): 2936 p(k,j) | p(m,b) | g(m) = k. [para(61(a,1),2933(c,2)),merge(c),merge(e)]. given #271 (T,wt=9): 2938 p(k,j) | p(m,b) | k != b. [para(2936(c,1),16(c,1)),flip(c),merge(d),unit_del(c,27)]. given #272 (A,wt=23): 181 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | x = y | p(y,b) | p(g(y),y). [para(37(c,1),22(a,1))]. given #273 (T,wt=9): 2939 p(k,j) | p(m,b) | k != m. [para(2936(c,1),18(c,1)),flip(c),merge(d),unit_del(c,27)]. given #274 (T,wt=6): 2976 p(k,j) | p(m,b). [resolve(2939,c,2058,c),merge(c),merge(d)]. given #275 (T,wt=16): 1482 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(k)). [para(105(c,1),406(e,1)),merge(d),merge(e),merge(f)]. given #276 (T,wt=13): 3014 p(m,k) | p(m,j) | p(j,b) | p(k,g(k)). [para(79(b,1),1482(c,1)),merge(c),merge(d),merge(e)]. given #277 (A,wt=23): 182 p(x,b) | p(g(x),x) | p(g(y),b) | p(g(g(y)),g(y)) | x = y | p(y,b). [para(22(a,1),37(c,1))]. given #278 (T,wt=16): 1492 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),k). [para(105(c,1),427(e,2)),merge(d),merge(e),merge(f)]. given #279 (T,wt=16): 2049 p(x,k) | p(x,b) | p(g(x),x) | p(m,x) | p(m,b). [para(50(a,1),2026(a,2))]. given #280 (T,wt=16): 2993 p(x,k) | p(x,b) | p(g(x),x) | p(x,j) | p(m,b). [para(50(a,1),2976(a,1))]. given #281 (T,wt=17): 195 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | g(x) = x. [factor(181,a,e),flip(d),merge(e)]. given #282 (A,wt=22): 183 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | k = y | x != y | p(y,k). [para(37(c,1),26(b,1))]. given #283 (T,wt=17): 356 p(j,b) | p(b,k) | p(m,j) | g(j) = j | g(j) = k. [resolve(99,b,29,b),flip(d),flip(e)]. given #284 (T,wt=16): 3083 p(j,b) | p(b,k) | p(m,j) | g(j) = k | j = b. [resolve(356,d,18,c),flip(e),merge(f)]. given #285 (T,wt=15): 3091 p(j,b) | p(b,k) | p(m,j) | j = b | k != b. [para(3083(d,1),16(c,1)),flip(e),merge(e),merge(f)]. given #286 (T,wt=12): 3112 p(j,b) | p(b,k) | p(m,j) | j = b. [resolve(3091,e,52,a),merge(e)]. given #287 (A,wt=29): 185 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(g(y),b) | p(g(y),g(g(y))) | x = y | p(y,b). [para(37(c,1),32(c,1))]. given #288 (T,wt=12): 3123 p(j,b) | p(b,k) | p(m,j) | p(k,b). [para(3112(d,1),262(a,2)),merge(e)]. given #289 (T,wt=12): 3124 p(j,b) | p(b,k) | p(m,j) | p(b,b). [para(3112(d,1),265(b,2)),merge(d)]. given #290 (T,wt=13): 3126 p(j,b) | p(b,k) | p(m,j) | p(b,g(j)). [para(3112(d,1),1407(b,1)),merge(d),merge(f)]. given #291 (T,wt=13): 3127 p(j,b) | p(b,k) | p(m,j) | p(j,g(b)). [para(3112(d,1),1407(b,2,1)),merge(d),merge(f)]. given #292 (A,wt=29): 186 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(g(y),b) | p(g(g(y)),g(y)) | x = y | p(y,b). [para(32(c,1),37(c,1))]. given #293 (T,wt=13): 3188 p(j,b) | p(b,k) | p(m,j) | p(b,g(b)). [para(3112(d,1),3127(d,1)),merge(d),merge(e),merge(f)]. given #294 (T,wt=15): 3117 p(j,b) | p(b,k) | p(m,j) | j = k | p(j,k). [resolve(3112,d,26,b(flip)),flip(d)]. given #295 (T,wt=12): 3201 p(j,b) | p(b,k) | p(m,j) | p(j,k). [para(3117(d,1),265(b,2)),merge(e),merge(f)]. given #296 (T,wt=9): 3204 p(b,k) | p(j,b) | p(m,j). [para(52(a,1),3201(d,2)),merge(c),merge(e)]. given #297 (A,wt=19): 187 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | k = x | p(b,k). [para(37(c,1),52(a,2))]. given #298 (T,wt=15): 3205 p(b,k) | p(m,j) | p(b,m) | j = m | j = b. [resolve(3204,b,267,e),merge(c)]. given #299 (T,wt=12): 3219 p(b,k) | p(m,j) | p(b,m) | j = b. [para(3205(d,1),265(b,2)),merge(e),merge(f)]. given #300 (T,wt=12): 3230 p(b,k) | p(m,j) | p(b,m) | p(k,b). [para(3219(d,1),262(a,2)),merge(e)]. given #301 (T,wt=12): 3231 p(b,k) | p(m,j) | p(b,m) | p(b,b). [para(3219(d,1),265(b,2)),merge(d)]. given #302 (A,wt=26): 188 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(x,m). [para(37(c,1),33(c,1))]. given #303 (T,wt=15): 3206 p(b,k) | p(m,j) | j = m | p(j,m) | j = b. [resolve(3204,b,266,e),merge(c)]. given #304 (T,wt=15): 3207 p(b,k) | p(m,j) | j = k | j = m | j = b. [resolve(3204,b,83,e),flip(d),flip(e),flip(f),merge(c)]. given #305 (T,wt=12): 3254 p(b,k) | p(m,j) | j = b | j = m. [para(52(a,1),3207(c,2)),merge(b),merge(f)]. given #306 (T,wt=12): 3257 p(b,k) | p(m,j) | j = b | p(k,m). [para(3254(d,1),262(a,2)),merge(e)]. given #307 (A,wt=19): 189 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,k) | p(m,x). [para(37(c,1),92(b,2))]. given #308 (T,wt=12): 3268 p(b,k) | p(m,j) | p(k,m) | p(k,b). [para(3257(c,1),262(a,2)),merge(e)]. given #309 (T,wt=12): 3269 p(b,k) | p(m,j) | p(k,m) | p(b,b). [para(3257(c,1),265(b,2)),merge(d)]. given #310 (T,wt=15): 3224 p(b,k) | p(m,j) | p(b,m) | j = k | p(j,k). [resolve(3219,d,26,b(flip)),flip(d)]. given #311 (T,wt=12): 3310 p(b,k) | p(m,j) | p(b,m) | p(j,k). [para(3224(d,1),265(b,2)),merge(e),merge(f)]. given #312 (A,wt=29): 193 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(g(y),b) | p(g(g(y)),g(y)) | x = y | p(y,b). [para(37(c,1),37(c,1))]. given #313 (T,wt=9): 3313 p(b,k) | p(m,j) | p(b,m). [para(3219(d,1),3310(d,1)),merge(d),merge(e),merge(f),merge(g)]. given #314 (T,wt=12): 3318 p(b,k) | p(b,m) | j = m | k = m. [resolve(3313,b,29,b)]. given #315 (T,wt=9): 3325 p(b,k) | p(b,m) | k = m. [para(3318(c,1),265(b,2)),merge(d),merge(e)]. given #316 (T,wt=6): 3332 p(b,k) | p(b,m). [para(3325(c,1),52(a,1)),merge(d),unit_del(c,27)]. given #317 (A,wt=22): 194 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | g(x) = b | g(g(x)) != x. [factor(178,a,e),flip(d)]. given #318 (T,wt=6): 3339 p(m,k) | p(b,m). [para(49(a,1),3332(a,2)),merge(c)]. given #319 (T,wt=12): 3333 p(b,m) | p(k,j) | j = b | k = b. [resolve(3332,a,89,c)]. given #320 (T,wt=9): 3368 p(b,m) | p(k,j) | k = b. [para(3333(c,1),61(a,1)),flip(d),merge(d),merge(e)]. given #321 (T,wt=9): 3375 p(b,m) | p(k,j) | j = b. [para(3368(c,1),61(a,2)),merge(d)]. given #322 (A,wt=19): 215 p(x,b) | p(x,g(x)) | p(b,k) | j = y | p(y,j) | x != y. [para(20(a,1),86(d,1))]. given #323 (T,wt=9): 3387 p(b,m) | p(k,j) | p(b,b). [para(3368(c,1),3332(a,2)),merge(d)]. given #324 (T,wt=12): 3335 p(b,m) | k = m | k = b | -p(k,b). [resolve(3332,a,2,e),flip(d),merge(c),unit_del(b,27)]. given #325 (T,wt=12): 3353 p(b,m) | p(k,j) | j = m | k = m. [resolve(3339,a,89,c)]. given #326 (T,wt=9): 3431 p(b,m) | p(k,j) | k = m. [para(3353(c,1),61(a,1)),flip(d),merge(d),merge(e)]. given #327 (A,wt=19): 216 p(x,b) | p(g(x),x) | p(b,k) | j = y | p(y,j) | x != y. [para(22(a,1),86(d,1))]. given #328 (T,wt=6): 3446 p(b,m) | p(k,j). [para(3431(c,1),3332(a,2)),merge(c),merge(d)]. given #329 (T,wt=13): 3336 p(x,b) | p(x,g(x)) | p(x,k) | p(b,m). [para(20(a,1),3332(a,1))]. given #330 (T,wt=13): 3337 p(x,b) | p(g(x),x) | p(x,k) | p(b,m). [para(22(a,1),3332(a,1))]. given #331 (T,wt=13): 3463 p(b,j) | p(k,b) | p(g(k),k) | p(b,m). [para(59(a,1),3446(b,2)),merge(e)]. given #332 (A,wt=25): 217 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,k) | j = y | p(y,j) | x != y. [para(32(c,1),86(d,1))]. given #333 (T,wt=13): 3464 p(b,j) | p(k,b) | p(k,g(k)) | p(b,m). [para(60(a,1),3446(b,2)),merge(e)]. given #334 (T,wt=13): 3503 p(x,b) | p(x,g(x)) | p(x,k) | p(x,m). [factor(3494,a,c),merge(c)]. given #335 (T,wt=14): 3492 p(x,b) | p(x,g(x)) | p(x,k) | p(f(b),b). [resolve(3336,d,14,b),unit_del(d,27)]. given #336 (T,wt=14): 3493 p(x,b) | p(x,g(x)) | p(x,k) | p(b,f(b)). [resolve(3336,d,12,b),unit_del(d,27)]. given #337 (A,wt=25): 218 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,k) | j = y | p(y,j) | x != y. [para(37(c,1),86(d,1))]. given #338 (T,wt=14): 3502 p(f(b),b) | p(f(b),g(f(b))) | p(f(b),k). [factor(3491,a,d),merge(d)]. given #339 (T,wt=14): 3616 p(x,b) | p(x,g(x)) | p(x,k) | p(f(x),b). [factor(3581,a,c),merge(c)]. given #340 (T,wt=14): 3618 p(x,b) | p(x,g(x)) | p(x,k) | p(f(b),x). [factor(3582,a,c),merge(c)]. given #341 (T,wt=14): 3663 p(x,b) | p(x,g(x)) | p(x,k) | p(x,f(b)). [factor(3647,a,c),merge(c)]. given #342 (A,wt=20): 219 p(x,b) | p(x,g(x)) | p(f(b),b) | p(g(f(b)),f(b)) | -p(x,m). [para(20(a,1),38(c,1))]. given #343 (T,wt=14): 3664 p(x,b) | p(x,g(x)) | p(x,k) | p(b,f(x)). [factor(3648,a,c),merge(c)]. given #344 (T,wt=14): 3715 p(x,b) | p(x,g(x)) | p(x,k) | p(f(x),x). [factor(3709,a,c),merge(c)]. given #345 (T,wt=14): 3792 p(x,b) | p(x,g(x)) | p(x,k) | p(x,f(x)). [factor(3782,a,c),merge(c)]. given #346 (T,wt=15): 3255 p(b,k) | p(m,j) | j = b | j = k | p(j,k). [resolve(3254,d,24,b(flip)),flip(d)]. given #347 (A,wt=20): 220 p(x,b) | p(g(x),x) | p(f(b),b) | p(g(f(b)),f(b)) | -p(x,m). [para(22(a,1),38(c,1))]. given #348 (T,wt=12): 3817 p(b,k) | p(m,j) | j = b | p(j,k). [para(52(a,1),3255(d,2)),merge(b),merge(e)]. given #349 (T,wt=12): 3828 p(b,k) | p(m,j) | p(j,k) | j = k. [resolve(3817,c,26,b(flip)),flip(d),merge(e)]. given #350 (T,wt=9): 3840 p(b,k) | p(m,j) | p(j,k). [para(3828(d,1),265(b,2)),merge(d),merge(e)]. given #351 (T,wt=9): 3843 p(b,k) | p(m,j) | p(k,m). [para(3257(c,1),3840(c,1)),merge(d),merge(e),merge(f)]. given #352 (A,wt=26): 221 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(f(b),b) | p(g(f(b)),f(b)) | -p(x,m). [para(32(c,1),38(c,1))]. given #353 (T,wt=13): 3844 p(b,k) | p(m,j) | k = m | p(f(k),k). [resolve(3843,c,14,b),flip(c)]. given #354 (T,wt=10): 3870 p(b,k) | p(m,j) | p(f(k),k). [para(3844(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #355 (T,wt=10): 3877 p(b,k) | p(m,j) | p(f(b),k). [para(52(a,1),3870(c,1,1)),merge(b)]. given #356 (T,wt=10): 3878 p(b,k) | p(m,j) | p(f(k),b). [para(52(a,1),3870(c,2)),merge(b)]. given #357 (A,wt=26): 222 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(f(b),b) | p(g(f(b)),f(b)) | -p(x,m). [para(37(c,1),38(c,1))]. given #358 (T,wt=10): 3901 p(b,k) | p(m,j) | p(f(b),b). [para(52(a,1),3877(c,2)),merge(b)]. given #359 (T,wt=13): 3845 p(b,k) | p(m,j) | k = m | p(k,f(k)). [resolve(3843,c,12,b),flip(c)]. given #360 (T,wt=10): 3951 p(b,k) | p(m,j) | p(k,f(k)). [para(3845(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #361 (T,wt=10): 3953 p(b,k) | p(m,j) | p(b,f(k)). [para(52(a,1),3951(c,1)),merge(b)]. given #362 (A,wt=18): 227 p(m,k) | p(m,j) | p(j,k) | j = x | -p(x,k) | k = x. [para(105(c,1),29(b,2))]. given #363 (T,wt=10): 3954 p(b,k) | p(m,j) | p(k,f(b)). [para(52(a,1),3951(c,2,1)),merge(b)]. given #364 (T,wt=10): 3977 p(b,k) | p(m,j) | p(b,f(b)). [para(52(a,1),3954(c,1)),merge(b)]. given #365 (T,wt=13): 3974 p(b,k) | p(b,f(k)) | j = m | k = m. [resolve(3953,b,29,b)]. given #366 (T,wt=13): 3990 p(b,k) | p(b,f(b)) | j = m | k = m. [resolve(3977,b,29,b)]. given #367 (A,wt=25): 243 p(x,b) | p(g(x),x) | -p(m,x) | g(m) = b | g(m) = m | -p(g(m),m) | p(m,b). [resolve(39,g,56,b),flip(c),flip(e),unit_del(c,27)]. given #368 (T,wt=13): 3996 p(b,k) | p(b,f(k)) | k = m | p(k,m). [para(3974(c,1),262(a,2)),merge(e)]. given #369 (T,wt=10): 4019 p(b,k) | p(b,f(k)) | p(k,m). [para(3996(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #370 (T,wt=13): 3999 p(b,k) | p(b,f(k)) | k = m | p(m,m). [para(3974(c,1),3953(b,2)),merge(d),merge(f)]. given #371 (T,wt=10): 4044 p(b,k) | p(b,f(k)) | p(m,m). [para(3999(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #372 (A,wt=18): 263 p(b,k) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(262,a,2,f),flip(b),flip(d),flip(e)]. given #373 (T,wt=13): 4005 p(b,k) | p(b,f(b)) | k = m | p(k,m). [para(3990(c,1),262(a,2)),merge(e)]. given #374 (T,wt=10): 4061 p(b,k) | p(b,f(b)) | p(k,m). [para(4005(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #375 (T,wt=13): 4008 p(b,k) | p(b,f(b)) | k = m | p(m,m). [para(3990(c,1),3977(b,2)),merge(d),merge(f)]. given #376 (T,wt=10): 4086 p(b,k) | p(b,f(b)) | p(m,m). [para(4008(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #377 (A,wt=18): 264 p(b,k) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(262,a,2,e),flip(b),flip(d)]. given #378 (T,wt=14): 4029 p(b,k) | p(b,f(k)) | k = m | p(f(k),k). [resolve(4019,c,14,b),flip(c)]. given #379 (T,wt=11): 4102 p(b,k) | p(b,f(k)) | p(f(k),k). [para(4029(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #380 (T,wt=11): 4109 p(b,k) | p(b,f(k)) | p(f(b),k). [para(52(a,1),4102(c,1,1)),merge(b)]. given #381 (T,wt=11): 4110 p(b,k) | p(b,f(k)) | p(f(k),b). [para(52(a,1),4102(c,2)),merge(b)]. given #382 (A,wt=19): 270 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,k) | p(x,j). [para(32(c,1),265(b,1))]. given #383 (T,wt=11): 4133 p(b,k) | p(b,f(k)) | p(f(b),b). [para(52(a,1),4109(c,2)),merge(b)]. given #384 (T,wt=14): 4030 p(b,k) | p(b,f(k)) | k = m | p(k,f(k)). [resolve(4019,c,12,b),flip(c)]. given #385 (T,wt=11): 4187 p(b,k) | p(b,f(k)) | p(k,f(k)). [para(4030(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #386 (T,wt=7): 4189 p(b,k) | p(b,f(k)). [para(52(a,1),4187(c,1)),merge(b),merge(d)]. given #387 (A,wt=19): 271 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,k) | p(x,j). [para(37(c,1),265(b,1))]. given #388 (T,wt=7): 4194 p(b,k) | p(b,f(b)). [para(52(a,1),4189(b,2,1)),merge(b)]. given #389 (T,wt=14): 4191 p(x,b) | p(x,g(x)) | p(b,k) | p(x,f(k)). [para(20(a,1),4189(b,1))]. given #390 (T,wt=14): 4192 p(x,b) | p(g(x),x) | p(b,k) | p(x,f(k)). [para(22(a,1),4189(b,1))]. given #391 (T,wt=14): 4197 p(x,b) | p(x,g(x)) | p(b,k) | p(b,f(x)). [para(84(c,1),4189(b,2,1)),merge(d)]. given #392 (A,wt=20): 273 p(g(k),k) | p(g(k),b) | p(g(g(k)),g(k)) | k = b | p(k,b). [resolve(50,a,18,c(flip)),flip(d)]. given #393 (T,wt=14): 4198 p(x,b) | p(g(x),x) | p(b,k) | p(b,f(x)). [para(85(c,1),4189(b,2,1)),merge(d)]. given #394 (T,wt=14): 4219 p(x,b) | p(x,g(x)) | p(b,k) | p(x,f(b)). [para(20(a,1),4194(b,1))]. given #395 (T,wt=14): 4220 p(x,b) | p(g(x),x) | p(b,k) | p(x,f(b)). [para(22(a,1),4194(b,1))]. given #396 (T,wt=14): 4251 p(x,b) | p(x,g(x)) | p(x,k) | p(x,f(k)). [factor(4241,a,c),merge(c)]. given #397 (A,wt=20): 274 p(f(k),k) | p(f(k),b) | p(g(f(k)),f(k)) | k = m | -p(k,m). [resolve(50,a,10,c(flip)),flip(d)]. given #398 (T,wt=14): 4291 p(x,b) | p(x,g(x)) | p(b,k) | p(x,f(x)). [factor(4284,a,c),merge(c)]. given #399 (T,wt=15): 3363 p(b,m) | -p(m,b) | k = b | k = m | -p(k,m). [resolve(3339,a,4,e),flip(b),flip(d),unit_del(b,27)]. given #400 (T,wt=16): 3209 p(x,b) | p(x,g(x)) | p(b,k) | p(j,x) | p(m,j). [para(20(a,1),3204(b,2))]. given #401 (T,wt=16): 3210 p(x,b) | p(g(x),x) | p(b,k) | p(j,x) | p(m,j). [para(22(a,1),3204(b,2))]. given #402 (A,wt=22): 275 p(x,k) | p(x,b) | p(g(x),x) | k = y | m = y | b = y | -p(y,x). [para(50(a,1),6(d,2))]. given #403 (T,wt=16): 3847 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(x,m). [para(84(c,1),3843(c,1)),merge(d)]. given #404 (T,wt=16): 3848 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(x,m). [para(85(c,1),3843(c,1)),merge(d)]. given #405 (T,wt=17): 411 p(j,b) | p(m,k) | p(k,j) | g(j) = j | g(j) = k. [resolve(124,b,29,b),flip(d),flip(e)]. given #406 (T,wt=13): 4478 p(k,j) | p(j,b) | p(m,k) | g(j) = k. [para(61(a,1),411(d,2)),merge(d),merge(f)]. given #407 (A,wt=19): 276 p(x,k) | p(x,b) | p(g(x),x) | j = y | p(y,j) | x != y. [para(50(a,1),31(c,1))]. given #408 (T,wt=9): 4493 p(k,j) | p(j,b) | p(m,k). [para(4478(d,1),2024(b,1)),merge(d),merge(e),merge(f),merge(g)]. given #409 (T,wt=16): 4509 p(x,k) | p(x,b) | p(g(x),x) | j = b | p(b,j). [resolve(276,f,22,a(flip)),merge(f),merge(g)]. given #410 (T,wt=16): 4515 p(x,b) | p(x,g(x)) | p(k,j) | p(j,x) | p(m,k). [para(20(a,1),4493(b,2))]. given #411 (T,wt=16): 4516 p(x,b) | p(g(x),x) | p(k,j) | p(j,x) | p(m,k). [para(22(a,1),4493(b,2))]. given #412 (A,wt=22): 289 p(x,k) | p(x,b) | p(g(x),x) | p(k,j) | j = y | -p(y,x) | k = y. [para(50(a,1),89(c,2))]. given #413 (T,wt=16): 4542 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | j = k. [factor(4524,a,f)]. given #414 (T,wt=16): 4544 p(x,b) | p(g(x),x) | p(x,k) | j = x | p(b,j). [factor(4526,a,d),merge(d)]. given #415 (T,wt=16): 4587 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | k = b. [factor(4586,a,e),merge(e),merge(f)]. given #416 (T,wt=16): 4602 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(m,b). [para(4587(e,1),2026(a,2)),merge(f)]. given #417 (A,wt=20): 292 p(g(k),k) | p(g(k),b) | p(g(k),g(g(k))) | k = b | p(k,b). [resolve(51,a,18,c(flip)),flip(d)]. given #418 (T,wt=17): 423 p(j,b) | p(m,k) | p(m,j) | g(j) = j | g(j) = k. [resolve(125,b,29,b),flip(d),flip(e)]. given #419 (T,wt=16): 4634 p(j,b) | p(m,k) | p(m,j) | g(j) = k | j = b. [resolve(423,d,18,c),flip(e),merge(f)]. given #420 (T,wt=15): 4641 p(j,b) | p(m,k) | p(m,j) | j = b | k != b. [para(4634(d,1),16(c,1)),flip(e),merge(e),merge(f)]. given #421 (T,wt=15): 4642 p(j,b) | p(m,k) | p(m,j) | j = b | j != k. [para(4634(d,1),18(c,1)),flip(e),flip(g),merge(e),merge(f)]. given #422 (A,wt=20): 293 p(f(k),k) | p(f(k),b) | p(f(k),g(f(k))) | k = m | -p(k,m). [resolve(51,a,10,c(flip)),flip(d)]. given #423 (T,wt=15): 4648 p(j,b) | p(m,k) | p(m,j) | j = b | p(k,m). [para(4634(d,1),426(d,1)),merge(e),merge(f),merge(g)]. given #424 (T,wt=12): 4672 p(j,b) | p(m,k) | p(m,j) | p(k,m). [para(4648(d,1),79(b,1)),flip(f),merge(e),merge(g),unit_del(e,27)]. given #425 (T,wt=15): 4651 p(j,b) | p(m,k) | p(m,j) | j = b | p(j,k). [para(4634(d,1),1335(c,2)),merge(f),merge(g),merge(h)]. given #426 (T,wt=12): 4688 p(j,b) | p(m,k) | p(m,j) | p(j,k). [para(4651(d,1),79(b,1)),flip(f),merge(e),merge(g),unit_del(e,27)]. given #427 (A,wt=22): 294 p(x,k) | p(x,b) | p(x,g(x)) | k = y | m = y | b = y | -p(y,x). [para(51(a,1),6(d,2))]. given #428 (T,wt=9): 4699 p(m,k) | p(m,j) | p(j,b). [para(79(b,1),4688(d,1)),merge(d),merge(e),merge(f)]. given #429 (T,wt=16): 4710 p(x,b) | p(x,g(x)) | p(m,k) | p(m,j) | p(j,x). [para(20(a,1),4699(c,2))]. given #430 (T,wt=16): 4711 p(x,b) | p(g(x),x) | p(m,k) | p(m,j) | p(j,x). [para(22(a,1),4699(c,2))]. given #431 (T,wt=17): 470 p(j,b) | p(b,k) | p(j,j) | g(j) = j | g(j) = k. [resolve(269,b,29,b),flip(d),flip(e)]. given #432 (A,wt=19): 295 p(x,k) | p(x,b) | p(x,g(x)) | j = y | p(y,j) | x != y. [para(51(a,1),31(c,1))]. given #433 (T,wt=13): 4741 p(j,b) | p(b,k) | p(j,j) | g(j) = k. [para(470(d,1),268(b,2)),merge(e),merge(f),merge(g),merge(h)]. given #434 (T,wt=12): 4771 p(j,b) | p(b,k) | p(j,j) | p(j,k). [para(4741(d,1),268(b,2)),merge(d),merge(f),merge(g)]. given #435 (T,wt=13): 4764 p(b,k) | p(j,b) | p(j,j) | g(j) = b. [para(52(a,1),4741(d,2)),merge(c)]. given #436 (T,wt=9): 4789 p(b,k) | p(j,b) | p(j,j). [para(4764(d,1),268(b,2)),merge(d),merge(e),merge(f),merge(g)]. given #437 (A,wt=22): 308 p(x,k) | p(x,b) | p(x,g(x)) | p(k,j) | j = y | -p(y,x) | k = y. [para(51(a,1),89(c,2))]. given #438 (T,wt=16): 4757 p(x,k) | p(x,b) | p(x,g(x)) | j = b | p(b,j). [resolve(295,f,20,a(flip)),merge(f),merge(g)]. given #439 (T,wt=16): 4812 p(x,b) | p(x,g(x)) | p(x,k) | j = x | p(b,j). [factor(4797,a,d),merge(d)]. given #440 (T,wt=17): 655 p(k,b) | p(g(k),k) | p(b,j) | p(b,b) | p(b,g(b)). [factor(653,c,g),merge(f)]. given #441 (T,wt=17): 660 p(k,b) | p(k,g(k)) | p(b,j) | p(b,b) | p(b,g(b)). [factor(658,c,g),merge(f)]. given #442 (A,wt=20): 311 p(x,b) | p(x,g(x)) | j = x | p(b,j) | p(k,b) | p(g(k),k). [para(20(a,1),59(a,2))]. given #443 (T,wt=17): 1320 p(j,k) | p(j,b) | p(m,k) | g(j) = j | g(j) = k. [resolve(1311,c,29,b),flip(d),flip(e)]. given #444 (T,wt=16): 4855 p(j,k) | p(j,b) | p(m,k) | g(j) = k | j = b. [resolve(1320,d,18,c),flip(e),merge(f)]. given #445 (T,wt=12): 4864 p(j,k) | p(j,b) | p(m,k) | j = b. [para(4855(d,1),1335(c,2)),merge(e),merge(f),merge(g),merge(h)]. given #446 (T,wt=12): 4869 p(j,k) | p(j,b) | p(m,k) | j = k. [resolve(4864,d,26,b(flip)),flip(d),merge(e)]. given #447 (A,wt=20): 312 p(x,b) | p(g(x),x) | j = x | p(b,j) | p(k,b) | p(g(k),k). [para(22(a,1),59(a,2))]. given #448 (T,wt=12): 4882 p(m,k) | p(j,k) | p(j,b) | j = m. [para(49(a,1),4869(d,2)),merge(d)]. given #449 (T,wt=9): 4897 p(m,k) | p(j,k) | p(j,b). [para(4882(d,1),4864(d,1)),merge(d),merge(e),merge(f),unit_del(d,27)]. given #450 (T,wt=9): 4908 p(m,k) | p(j,m) | p(j,b). [para(49(a,1),4897(b,2)),merge(b)]. given #451 (T,wt=13): 4930 p(m,k) | p(j,b) | j = m | p(f(j),j). [resolve(4908,b,14,b),flip(c)]. given #452 (A,wt=19): 313 p(b,j) | p(k,b) | p(g(k),k) | j = x | -p(x,b) | k = x. [para(59(a,1),29(b,2))]. given #453 (T,wt=10): 4942 p(m,k) | p(j,b) | p(f(j),j). [para(4930(c,1),4897(b,1)),merge(d),merge(e),merge(f)]. given #454 (T,wt=13): 4931 p(m,k) | p(j,b) | j = m | p(j,f(j)). [resolve(4908,b,12,b),flip(c)]. given #455 (T,wt=10): 4985 p(m,k) | p(j,b) | p(j,f(j)). [para(4931(c,1),4897(b,1)),merge(d),merge(e),merge(f)]. given #456 (T,wt=14): 4965 p(m,k) | p(j,b) | f(j) = j | f(j) = k. [resolve(4942,c,29,b),flip(c),flip(d)]. given #457 (A,wt=26): 314 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | j = x | p(b,j) | p(k,b) | p(g(k),k). [para(32(c,1),59(a,2))]. given #458 (T,wt=13): 5009 p(m,k) | p(j,b) | f(j) = k | p(j,j). [para(4965(c,1),4942(c,1)),merge(d),merge(e)]. given #459 (T,wt=13): 5017 p(m,k) | p(j,b) | f(j) = m | p(j,j). [para(49(a,1),5009(c,2)),merge(b)]. given #460 (T,wt=15): 4906 p(m,k) | p(j,b) | j = k | j = m | j = b. [resolve(4897,b,6,d),flip(c),flip(d),flip(e)]. given #461 (T,wt=12): 5024 p(m,k) | p(j,b) | j = m | j = b. [para(49(a,1),4906(c,2)),merge(b),merge(e)]. given #462 (A,wt=26): 316 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | j = x | p(b,j) | p(k,b) | p(g(k),k). [para(37(c,1),59(a,2))]. given #463 (T,wt=9): 5030 p(m,k) | p(j,b) | j = b. [para(5024(c,1),4897(b,1)),merge(d),merge(e),merge(f)]. given #464 (T,wt=10): 5043 p(m,k) | p(j,b) | p(f(b),j). [para(5030(c,1),4942(c,1,1)),merge(c),merge(d)]. given #465 (T,wt=10): 5044 p(m,k) | p(j,b) | p(f(j),b). [para(5030(c,1),4942(c,2)),merge(c),merge(d)]. given #466 (T,wt=10): 5045 p(m,k) | p(j,b) | p(b,f(j)). [para(5030(c,1),4985(c,1)),merge(c),merge(d)]. given #467 (A,wt=20): 320 p(x,b) | p(x,g(x)) | j = x | p(b,j) | p(k,b) | p(k,g(k)). [para(20(a,1),60(a,2))]. given #468 (T,wt=10): 5046 p(m,k) | p(j,b) | p(j,f(b)). [para(5030(c,1),4985(c,2,1)),merge(c),merge(d)]. given #469 (T,wt=10): 5063 p(m,k) | p(j,b) | p(f(b),b). [para(5030(c,1),5043(c,2)),merge(c),merge(d)]. given #470 (T,wt=10): 5076 p(m,k) | p(j,b) | f(j) = k. [para(4965(c,1),5044(c,1)),merge(d),merge(e),merge(f)]. given #471 (T,wt=10): 5100 p(m,k) | p(j,b) | p(b,f(b)). [para(5030(c,1),5046(c,1)),merge(c),merge(d)]. given #472 (A,wt=20): 321 p(x,b) | p(g(x),x) | j = x | p(b,j) | p(k,b) | p(k,g(k)). [para(22(a,1),60(a,2))]. given #473 (T,wt=10): 5121 p(m,k) | p(j,b) | f(j) = m. [para(49(a,1),5076(c,2)),merge(b)]. given #474 (T,wt=10): 5122 p(m,k) | p(j,b) | f(b) = k. [para(5030(c,1),5076(c,1,1)),merge(c),merge(d)]. given #475 (T,wt=10): 5140 p(m,k) | p(j,b) | f(b) = m. [para(5030(c,1),5121(c,1,1)),merge(c),merge(d)]. given #476 (T,wt=9): 5149 p(m,k) | p(j,b) | -p(b,m). [resolve(5140,c,8,c),unit_del(c,27)]. given #477 (A,wt=19): 322 p(b,j) | p(k,b) | p(k,g(k)) | j = x | -p(x,b) | k = x. [para(60(a,1),29(b,2))]. given #478 (T,wt=12): 5139 p(m,k) | p(j,b) | j = m | -p(j,m). [resolve(5121,c,8,c),flip(c)]. given #479 (T,wt=9): 5176 p(m,k) | p(j,b) | j = m. [resolve(5139,d,4908,b),merge(d),merge(e)]. given #480 (T,wt=6): 5182 p(m,k) | p(j,b). [para(5176(c,1),4897(b,1)),merge(c),merge(d),merge(e)]. given #481 (T,wt=13): 5189 p(x,b) | p(x,g(x)) | p(m,k) | p(j,x). [para(20(a,1),5182(b,2))]. given #482 (A,wt=26): 323 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | j = x | p(b,j) | p(k,b) | p(k,g(k)). [para(32(c,1),60(a,2))]. given #483 (T,wt=13): 5190 p(x,b) | p(g(x),x) | p(m,k) | p(j,x). [para(22(a,1),5182(b,2))]. given #484 (T,wt=15): 5188 p(m,k) | j = m | p(j,m) | j = b | -p(b,j). [resolve(5182,b,2,e),flip(b),flip(e),unit_del(d,27)]. given #485 (T,wt=17): 1657 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(f(b)))),m). [factor(1652,a,c),merge(c)]. given #486 (T,wt=17): 1663 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(f(b)))),m). [factor(1659,a,c),merge(c)]. given #487 (A,wt=26): 325 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | j = x | p(b,j) | p(k,b) | p(k,g(k)). [para(37(c,1),60(a,2))]. given #488 (T,wt=17): 1790 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | p(k,g(j)). [para(1308(e,1),1757(c,1)),merge(e),merge(f)]. given #489 (T,wt=17): 1791 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | p(j,g(k)). [para(1308(e,1),1757(c,2,1)),merge(e),merge(f)]. given #490 (T,wt=17): 1930 p(k,b) | p(g(k),k) | p(b,j) | p(k,j) | p(b,g(k)). [para(477(d,1),1911(c,1)),merge(e)]. given #491 (T,wt=17): 1931 p(k,b) | p(g(k),k) | p(b,j) | p(k,j) | p(k,g(b)). [para(477(d,1),1911(c,2,1)),merge(e)]. given #492 (A,wt=40): 327 p(g(m),b) | p(m,b) | p(x,b) | p(g(x),x) | g(g(m)) = b | -p(g(g(m)),x) | g(m) = b | g(g(m)) = g(m) | -p(g(g(m)),g(m)). [resolve(64,b,39,h),flip(e),flip(g),flip(h)]. given #493 (T,wt=17): 3515 p(j,b) | p(j,k) | p(b,m) | g(j) = j | g(j) = k. [resolve(3337,b,29,b),flip(d),flip(e)]. given #494 (T,wt=16): 5352 p(j,b) | p(j,k) | p(b,m) | g(j) = k | j = b. [resolve(3515,d,18,c),flip(e),merge(f)]. given #495 (T,wt=12): 5367 p(j,b) | p(j,k) | p(b,m) | j = b. [para(5352(d,1),1757(c,2)),merge(e),merge(f),merge(g)]. given #496 (T,wt=12): 5372 p(j,b) | p(j,k) | p(b,m) | j = k. [resolve(5367,d,26,b(flip)),flip(d),merge(e)]. given #497 (A,wt=39): 328 p(g(m),b) | p(m,b) | p(x,b) | p(g(x),x) | g(m) = b | -p(g(m),x) | g(g(m)) = b | g(g(m)) = g(m) | -p(g(g(m)),g(m)). [resolve(64,b,39,g),flip(e),flip(g)]. given #498 (T,wt=12): 5383 p(j,b) | p(j,k) | p(b,m) | p(k,b). [para(5367(d,1),3446(b,2)),merge(d)]. given #499 (T,wt=12): 5396 p(j,b) | p(j,k) | p(b,m) | p(k,k). [para(5372(d,1),3446(b,2)),merge(d)]. given #500 (T,wt=12): 5401 p(j,b) | p(j,k) | p(b,m) | k = b. [para(5372(d,1),5367(d,1)),merge(d),merge(e),merge(f)]. given #501 (T,wt=12): 5453 p(j,b) | p(j,k) | p(b,m) | p(m,b). [para(5401(d,1),2026(a,2)),merge(e)]. given #502 (A,wt=40): 330 p(g(m),b) | p(m,b) | p(x,b) | p(x,g(x)) | g(g(m)) = b | -p(g(g(m)),x) | g(m) = b | g(g(m)) = g(m) | -p(g(g(m)),g(m)). [resolve(64,b,34,h),flip(e),flip(g),flip(h)]. given #503 (T,wt=12): 5455 p(j,b) | p(j,k) | p(b,m) | p(b,b). [para(5401(d,1),3332(a,2)),merge(e)]. given #504 (T,wt=12): 5456 p(j,b) | p(j,k) | p(b,m) | p(b,j). [para(5401(d,1),3446(b,1)),merge(d)]. given #505 (T,wt=13): 5379 p(j,b) | p(j,k) | p(b,m) | p(b,g(j)). [para(5367(d,1),1757(c,1)),merge(d),merge(e)]. given #506 (T,wt=13): 5380 p(j,b) | p(j,k) | p(b,m) | p(j,g(b)). [para(5367(d,1),1757(c,2,1)),merge(d),merge(e)]. given #507 (A,wt=39): 331 p(g(m),b) | p(m,b) | p(x,b) | p(x,g(x)) | g(m) = b | -p(g(m),x) | g(g(m)) = b | g(g(m)) = g(m) | -p(g(g(m)),g(m)). [resolve(64,b,34,g),flip(e),flip(g)]. given #508 (T,wt=13): 5393 p(j,b) | p(j,k) | p(b,m) | p(k,g(j)). [para(5372(d,1),1757(c,1)),merge(d),merge(e)]. given #509 (T,wt=13): 5394 p(j,b) | p(j,k) | p(b,m) | p(j,g(k)). [para(5372(d,1),1757(c,2,1)),merge(d),merge(e)]. given #510 (T,wt=13): 5400 p(j,b) | p(j,k) | p(b,m) | g(j) = k. [para(5372(d,1),3515(d,2)),merge(d),merge(e),merge(f),merge(h)]. given #511 (T,wt=9): 5560 p(j,b) | p(j,k) | p(b,m). [para(5400(d,1),1757(c,2)),merge(d),merge(e),merge(f)]. given #512 (A,wt=33): 333 p(g(m),b) | p(m,b) | g(g(m)) = b | -p(g(g(m)),b) | g(m) = b | g(g(m)) = g(m) | -p(g(g(m)),g(m)). [resolve(64,b,4,f),flip(c),flip(e),flip(f)]. given #513 (T,wt=15): 5569 p(j,b) | p(b,m) | j = k | j = m | j = b. [resolve(5560,b,6,d),flip(c),flip(d),flip(e)]. given #514 (T,wt=15): 5584 p(j,b) | p(b,m) | j = m | j = b | p(k,k). [para(5569(c,1),3446(b,2)),merge(e)]. given #515 (T,wt=15): 5593 p(j,b) | p(b,m) | j = b | p(k,k) | p(k,m). [para(5584(c,1),3446(b,2)),merge(e)]. given #516 (T,wt=15): 5602 p(j,b) | p(b,m) | p(k,k) | p(k,m) | p(k,b). [para(5593(c,1),3446(b,2)),merge(e)]. given #517 (A,wt=33): 334 p(g(m),b) | p(m,b) | g(g(m)) = m | p(g(g(m)),m) | g(m) = m | g(g(m)) = g(m) | -p(g(g(m)),g(m)). [resolve(64,b,2,f),flip(c),flip(e),flip(f)]. given #518 (T,wt=16): 5589 p(j,b) | p(b,m) | j = b | p(k,k) | p(g(j),j). [resolve(5584,c,58,c(flip)),merge(e)]. given #519 (T,wt=16): 5590 p(j,b) | p(b,m) | j = b | p(k,k) | p(j,g(j)). [resolve(5584,c,57,c(flip)),merge(e)]. given #520 (T,wt=16): 5620 p(j,b) | p(b,m) | p(k,k) | p(g(j),j) | p(k,b). [para(5589(c,1),3446(b,2)),merge(e)]. given #521 (T,wt=16): 5623 p(j,b) | p(b,m) | p(k,k) | p(j,g(j)) | p(k,b). [para(5590(c,1),3446(b,2)),merge(e)]. given #522 (A,wt=20): 335 p(k,b) | p(g(k),k) | p(x,b) | p(x,g(x)) | j = x | p(x,j). [resolve(41,c,31,c)]. given #523 (T,wt=17): 3883 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(f(x),k). [para(84(c,1),3870(c,1,1)),merge(d)]. given #524 (T,wt=17): 3884 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(f(k),x). [para(84(c,1),3870(c,2)),merge(d)]. given #525 (T,wt=17): 3885 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(f(x),k). [para(85(c,1),3870(c,1,1)),merge(d)]. given #526 (T,wt=17): 3886 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(f(k),x). [para(85(c,1),3870(c,2)),merge(d)]. given #527 (A,wt=23): 336 p(f(x),b) | p(g(f(x)),f(x)) | p(x,b) | p(x,g(x)) | m = x | -p(x,m). [resolve(41,c,10,c)]. given #528 (T,wt=17): 3903 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(f(b),x). [para(84(c,1),3877(c,2)),merge(d)]. given #529 (T,wt=17): 3904 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(f(b),x). [para(85(c,1),3877(c,2)),merge(d)]. given #530 (T,wt=17): 3918 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(f(x),b). [para(84(c,1),3878(c,1,1)),merge(d)]. given #531 (T,wt=17): 3919 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(f(x),b). [para(85(c,1),3878(c,1,1)),merge(d)]. given #532 (A,wt=20): 337 p(x,b) | p(g(x),x) | p(k,b) | p(k,g(k)) | j = x | p(x,j). [resolve(41,c,31,c(flip))]. given #533 (T,wt=17): 3960 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(k,f(x)). [para(84(c,1),3951(c,2,1)),merge(d)]. given #534 (T,wt=17): 3962 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(k,f(x)). [para(85(c,1),3951(c,2,1)),merge(d)]. given #535 (T,wt=17): 4255 p(k,b) | p(k,g(k)) | p(b,j) | p(b,b) | p(k,f(k)). [factor(4246,a,d),merge(d)]. given #536 (T,wt=17): 4342 p(k,b) | p(k,g(k)) | p(b,j) | p(b,b) | p(k,f(b)). [factor(4334,a,d),merge(d)]. given #537 (A,wt=23): 338 p(x,b) | p(g(x),x) | p(f(x),b) | p(f(x),g(f(x))) | m = x | -p(x,m). [resolve(41,c,10,c(flip))]. given #538 (T,wt=17): 4549 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(b,g(j)). [factor(4533,a,e),merge(e)]. given #539 (T,wt=17): 4550 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(j,g(b)). [factor(4534,a,e),merge(e)]. given #540 (T,wt=17): 4582 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(k,g(j)). [para(4542(e,1),1757(c,1)),merge(e),merge(f)]. given #541 (T,wt=17): 4583 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(j,g(k)). [para(4542(e,1),1757(c,2,1)),merge(e),merge(f)]. given #542 (A,wt=19): 339 p(f(k),b) | p(f(k),g(f(k))) | p(b,k) | k = m | -p(k,m). [resolve(84,c,10,c(flip)),flip(d)]. given #543 (T,wt=17): 5690 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(f(x),x). [factor(5682,a,d),merge(d)]. given #544 (T,wt=18): 2022 p(m,k) | k = b | b = x | k = x | -p(k,x) | -p(x,k). [resolve(2018,b,4,b),flip(b),flip(d)]. given #545 (T,wt=18): 2989 p(m,b) | j = b | -p(j,b) | k = b | j = k | -p(j,k). [resolve(2976,a,4,f),flip(b),flip(d),flip(e)]. given #546 (T,wt=18): 2990 p(m,b) | k = b | -p(k,b) | j = b | j = k | -p(j,k). [resolve(2976,a,4,e),flip(b),flip(d)]. given #547 (A,wt=22): 340 p(x,b) | p(x,g(x)) | p(b,k) | k = y | m = y | b = y | -p(y,x). [para(84(c,1),6(d,2))]. given #548 (T,wt=18): 2991 p(m,b) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(2976,a,2,f),flip(b),flip(d),flip(e)]. given #549 (T,wt=18): 2992 p(m,b) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(2976,a,2,e),flip(b),flip(d)]. given #550 (T,wt=18): 3256 p(b,k) | p(m,j) | j = b | j = x | -p(x,m) | k = x. [para(3254(d,1),29(b,2))]. given #551 (T,wt=18): 3459 p(b,m) | j = b | -p(j,b) | k = b | j = k | -p(j,k). [resolve(3446,b,4,f),flip(b),flip(d),flip(e)]. given #552 (A,wt=19): 341 p(f(k),b) | p(g(f(k)),f(k)) | p(b,k) | k = m | -p(k,m). [resolve(85,c,10,c(flip)),flip(d)]. given #553 (T,wt=18): 3460 p(b,m) | k = b | -p(k,b) | j = b | j = k | -p(j,k). [resolve(3446,b,4,e),flip(b),flip(d)]. given #554 (T,wt=18): 3461 p(b,m) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(3446,b,2,f),flip(b),flip(d),flip(e)]. given #555 (T,wt=18): 3462 p(b,m) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(3446,b,2,e),flip(b),flip(d)]. given #556 (T,wt=18): 3875 p(b,k) | p(m,j) | f(k) = k | f(k) = m | f(k) = b. [resolve(3870,c,6,d),flip(c),flip(d),flip(e)]. given #557 (A,wt=22): 342 p(x,b) | p(g(x),x) | p(b,k) | k = y | m = y | b = y | -p(y,x). [para(85(c,1),6(d,2))]. given #558 (T,wt=14): 6066 p(b,k) | p(m,j) | f(k) = b | f(k) = m. [para(52(a,1),3875(c,2)),merge(b),merge(f)]. given #559 (T,wt=14): 6072 p(b,k) | p(m,j) | f(k) = b | f(b) = m. [para(52(a,1),6066(d,1,1)),merge(b)]. given #560 (T,wt=10): 6102 p(b,k) | p(m,j) | f(b) = m. [para(6072(c,1),3870(c,1)),merge(d),merge(e),merge(f)]. given #561 (T,wt=9): 6103 p(b,k) | p(m,j) | -p(b,m). [resolve(6102,c,8,c),unit_del(c,27)]. given #562 (A,wt=35): 343 p(x,b) | p(b,k) | p(m,x) | p(y,b) | p(g(y),y) | g(x) = b | -p(g(x),y) | b = x | g(x) = x | -p(g(x),x). [resolve(98,b,39,h),flip(f),flip(i)]. given #563 (T,wt=13): 6117 p(b,k) | p(m,j) | p(b,b) | p(b,g(b)). [factor(6110,a,e)]. given #564 (T,wt=16): 6071 p(b,k) | p(m,j) | f(k) = b | k = m | -p(k,m). [resolve(6066,d,8,c),flip(d)]. given #565 (T,wt=13): 6154 p(b,k) | p(m,j) | f(k) = b | k = m. [resolve(6071,e,3843,c),merge(e),merge(f)]. given #566 (T,wt=9): 6172 p(b,k) | p(m,j) | k = m. [para(6154(c,1),3870(c,1)),merge(d),merge(e),merge(f)]. given #567 (A,wt=34): 344 p(x,b) | p(b,k) | p(m,x) | p(y,b) | p(g(y),y) | b = x | -p(x,y) | g(x) = b | g(x) = x | -p(g(x),x). [resolve(98,b,39,g),flip(h)]. given #568 (T,wt=6): 6185 p(b,k) | p(m,j). [para(6172(c,1),52(a,1)),merge(d),unit_del(c,27)]. given #569 (T,wt=9): 6197 p(b,k) | j = m | k = m. [resolve(6185,b,29,b)]. given #570 (T,wt=9): 6203 p(b,k) | k = m | p(k,m). [para(6197(b,1),262(a,2)),merge(d)]. given #571 (T,wt=6): 6214 p(b,k) | p(k,m). [para(6203(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #572 (A,wt=35): 345 p(x,b) | p(b,k) | p(m,x) | p(y,b) | p(y,g(y)) | g(x) = b | -p(g(x),y) | b = x | g(x) = x | -p(g(x),x). [resolve(98,b,34,h),flip(f),flip(i)]. given #573 (T,wt=9): 6207 p(b,k) | k = m | p(m,m). [para(6197(b,1),6185(b,2)),merge(c)]. given #574 (T,wt=6): 6247 p(b,k) | p(m,m). [para(6207(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #575 (T,wt=10): 6225 p(b,k) | k = m | p(f(k),k). [resolve(6214,b,14,b),flip(b)]. given #576 (T,wt=7): 6254 p(b,k) | p(f(k),k). [para(6225(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #577 (A,wt=34): 346 p(x,b) | p(b,k) | p(m,x) | p(y,b) | p(y,g(y)) | b = x | -p(x,y) | g(x) = b | g(x) = x | -p(g(x),x). [resolve(98,b,34,g),flip(h)]. given #578 (T,wt=7): 6263 p(b,k) | p(f(b),k). [para(52(a,1),6254(b,1,1)),merge(b)]. given #579 (T,wt=7): 6264 p(b,k) | p(f(k),b). [para(52(a,1),6254(b,2)),merge(b)]. given #580 (T,wt=7): 6296 p(b,k) | p(f(b),b). [para(52(a,1),6263(b,2)),merge(b)]. given #581 (T,wt=10): 6226 p(b,k) | k = m | p(k,f(k)). [resolve(6214,b,12,b),flip(b)]. given #582 (A,wt=28): 347 p(x,b) | p(b,k) | p(m,x) | g(x) = b | -p(g(x),b) | b = x | g(x) = x | -p(g(x),x). [resolve(98,b,4,f),flip(d),flip(g)]. given #583 (T,wt=7): 6332 p(b,k) | p(k,f(k)). [para(6226(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #584 (T,wt=7): 6343 p(b,k) | p(k,f(b)). [para(52(a,1),6332(b,2,1)),merge(b)]. given #585 (T,wt=12): 6196 p(b,k) | j = b | j = m | -p(j,m). [resolve(6185,b,97,d),flip(c),flip(d),merge(b)]. given #586 (T,wt=12): 6201 p(b,k) | k = m | j = k | p(j,k). [resolve(6197,b,24,b(flip)),flip(c)]. given #587 (A,wt=28): 348 p(x,b) | p(b,k) | p(m,x) | g(x) = m | p(g(x),m) | m = x | g(x) = x | -p(g(x),x). [resolve(98,b,2,f),flip(d),flip(g)]. given #588 (T,wt=9): 6358 p(b,k) | k = m | p(j,k). [para(6201(c,1),265(b,2)),merge(d),merge(e)]. given #589 (T,wt=6): 6372 p(b,k) | p(j,k). [para(6358(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #590 (T,wt=6): 6380 p(b,k) | p(j,b). [para(52(a,1),6372(b,2)),merge(b)]. given #591 (T,wt=12): 6379 p(b,k) | j = k | j = m | j = b. [resolve(6372,b,6,d),flip(b),flip(c),flip(d)]. given #592 (A,wt=27): 349 p(x,b) | p(b,k) | p(m,x) | m = x | p(x,m) | g(x) = m | g(x) = x | -p(g(x),x). [resolve(98,b,2,e),flip(f)]. given #593 (T,wt=9): 6398 p(b,k) | j = b | j = m. [para(52(a,1),6379(b,2)),merge(b),merge(e)]. given #594 (T,wt=13): 6228 p(x,b) | p(x,g(x)) | p(b,k) | p(x,m). [para(84(c,1),6214(b,1)),merge(d)]. given #595 (T,wt=13): 6229 p(x,b) | p(g(x),x) | p(b,k) | p(x,m). [para(85(c,1),6214(b,1)),merge(d)]. given #596 (T,wt=13): 6383 p(x,b) | p(x,g(x)) | p(b,k) | p(j,x). [para(84(c,1),6372(b,2)),merge(d)]. given #597 (A,wt=35): 362 p(m,b) | p(x,b) | p(g(x),x) | g(m) = b | -p(g(m),x) | f(g(m)) = b | f(g(m)) = g(m) | -p(g(m),f(g(m))). [resolve(361,b,39,h),flip(d),flip(f)]. given #598 (T,wt=13): 6384 p(x,b) | p(g(x),x) | p(b,k) | p(j,x). [para(85(c,1),6372(b,2)),merge(d)]. given #599 (T,wt=14): 6269 p(x,b) | p(x,g(x)) | p(b,k) | p(f(x),k). [para(84(c,1),6254(b,1,1)),merge(d)]. given #600 (T,wt=14): 6270 p(x,b) | p(x,g(x)) | p(b,k) | p(f(k),x). [para(84(c,1),6254(b,2)),merge(d)]. given #601 (T,wt=14): 6271 p(x,b) | p(g(x),x) | p(b,k) | p(f(x),k). [para(85(c,1),6254(b,1,1)),merge(d)]. given #602 (A,wt=36): 363 p(m,b) | p(x,b) | p(g(x),x) | f(g(m)) = b | -p(f(g(m)),x) | g(m) = b | f(g(m)) = g(m) | -p(g(m),f(g(m))). [resolve(361,b,39,g),flip(d),flip(f),flip(g)]. given #603 (T,wt=14): 6272 p(x,b) | p(g(x),x) | p(b,k) | p(f(k),x). [para(85(c,1),6254(b,2)),merge(d)]. given #604 (T,wt=14): 6298 p(x,b) | p(x,g(x)) | p(b,k) | p(f(b),x). [para(84(c,1),6263(b,2)),merge(d)]. given #605 (T,wt=14): 6299 p(x,b) | p(g(x),x) | p(b,k) | p(f(b),x). [para(85(c,1),6263(b,2)),merge(d)]. given #606 (T,wt=14): 6313 p(x,b) | p(x,g(x)) | p(b,k) | p(f(x),b). [para(84(c,1),6264(b,1,1)),merge(d)]. given #607 (A,wt=35): 364 p(m,b) | p(x,b) | p(x,g(x)) | g(m) = b | -p(g(m),x) | f(g(m)) = b | f(g(m)) = g(m) | -p(g(m),f(g(m))). [resolve(361,b,34,h),flip(d),flip(f)]. given #608 (T,wt=14): 6314 p(x,b) | p(g(x),x) | p(b,k) | p(f(x),b). [para(85(c,1),6264(b,1,1)),merge(d)]. given #609 (T,wt=14): 6346 p(x,b) | p(x,g(x)) | p(b,k) | p(k,f(x)). [para(84(c,1),6332(b,2,1)),merge(d)]. given #610 (T,wt=14): 6347 p(x,b) | p(g(x),x) | p(b,k) | p(k,f(x)). [para(85(c,1),6332(b,2,1)),merge(d)]. given #611 (T,wt=14): 6486 p(x,b) | p(x,g(x)) | p(b,k) | p(f(x),x). [factor(6478,a,d),merge(d)]. given #612 (A,wt=36): 365 p(m,b) | p(x,b) | p(x,g(x)) | f(g(m)) = b | -p(f(g(m)),x) | g(m) = b | f(g(m)) = g(m) | -p(g(m),f(g(m))). [resolve(361,b,34,g),flip(d),flip(f),flip(g)]. given #613 (T,wt=15): 6202 p(b,k) | k = m | j = x | -p(x,m) | k = x. [para(6197(b,1),29(b,2))]. given #614 (T,wt=15): 6261 p(b,k) | f(k) = k | f(k) = m | f(k) = b. [resolve(6254,b,6,d),flip(b),flip(c),flip(d)]. given #615 (T,wt=11): 6619 p(b,k) | f(k) = b | f(k) = m. [para(52(a,1),6261(b,2)),merge(b),merge(e)]. given #616 (T,wt=11): 6621 p(b,k) | f(k) = b | f(b) = m. [para(52(a,1),6619(c,1,1)),merge(b)]. given #617 (A,wt=28): 366 p(m,b) | g(m) = b | -p(g(m),b) | f(g(m)) = b | f(g(m)) = g(m) | -p(g(m),f(g(m))). [resolve(361,b,4,f),flip(b),flip(d)]. given #618 (T,wt=7): 6652 p(b,k) | f(b) = m. [para(6621(b,1),6254(b,1)),merge(c),merge(d)]. given #619 (T,wt=6): 6658 p(b,k) | -p(b,m). [resolve(6652,b,8,c),unit_del(b,27)]. given #620 (T,wt=10): 6672 p(b,k) | p(b,b) | p(b,g(b)). [factor(6665,a,d)]. given #621 (T,wt=13): 6620 p(b,k) | f(k) = b | k = m | -p(k,m). [resolve(6619,c,8,c),flip(c)]. given #622 (A,wt=29): 367 p(m,b) | f(g(m)) = b | -p(f(g(m)),b) | g(m) = b | f(g(m)) = g(m) | -p(g(m),f(g(m))). [resolve(361,b,4,e),flip(b),flip(d),flip(e)]. given #623 (T,wt=10): 6688 p(b,k) | f(k) = b | k = m. [resolve(6620,d,6214,b),merge(d)]. given #624 (T,wt=6): 6709 p(b,k) | k = m. [para(6688(b,1),6254(b,1)),merge(c),merge(d)]. given #625 (T,wt=3): 6716 p(b,k). [para(6709(b,1),52(a,1)),merge(c),unit_del(b,27)]. given #626 (T,wt=9): 6724 p(k,j) | j = b | k = b. [resolve(6716,a,89,c)]. given #627 (A,wt=29): 368 p(m,b) | f(g(m)) = m | p(f(g(m)),m) | g(m) = m | f(g(m)) = g(m) | -p(g(m),f(g(m))). [resolve(361,b,2,e),flip(b),flip(d),flip(e)]. given #628 (T,wt=6): 6738 p(k,j) | k = b. [para(6724(b,1),61(a,1)),flip(c),merge(c),merge(d)]. given #629 (T,wt=6): 6746 p(k,j) | p(m,k). [para(6738(b,1),49(a,1)),flip(b),unit_del(b,27)]. given #630 (T,wt=6): 6747 p(k,j) | j = b. [para(6738(b,1),61(a,2)),merge(c)]. given #631 (T,wt=6): 6758 p(k,j) | p(b,b). [para(6738(b,1),6716(a,2))]. given #632 (A,wt=36): 372 p(m,b) | p(x,b) | p(g(x),x) | f(g(m)) = b | -p(f(g(m)),x) | g(m) = b | f(g(m)) = g(m) | -p(f(g(m)),g(m)). [resolve(371,b,39,h),flip(d),flip(f),flip(g)]. given #633 (T,wt=6): 6760 p(m,k) | p(m,j). [para(49(a,1),6746(a,1)),merge(c)]. given #634 (T,wt=10): 6726 p(x,b) | p(x,g(x)) | p(x,k). [para(20(a,1),6716(a,1))]. given #635 (T,wt=10): 6727 p(x,b) | p(g(x),x) | p(x,k). [para(22(a,1),6716(a,1))]. given #636 (T,wt=10): 6751 p(k,j) | p(j,b) | p(k,g(j)). [para(6738(b,1),1770(b,2)),merge(b),merge(d)]. given #637 (A,wt=35): 374 p(m,b) | p(f(g(m)),b) | p(g(f(g(m))),f(g(m))) | g(m) = b | b = x | g(m) = x | -p(g(m),x) | -p(x,g(m)). [resolve(371,b,39,d),flip(d),flip(f)]. given #638 (T,wt=10): 6753 p(k,j) | p(j,b) | p(k,g(k)). [para(6738(b,1),1824(b,2)),merge(b),merge(d)]. given #639 (T,wt=10): 6755 p(k,j) | p(k,b) | p(b,g(k)). [para(6738(b,1),1911(c,1)),merge(b)]. given #640 (T,wt=10): 6756 p(k,j) | p(k,b) | p(k,g(b)). [para(6738(b,1),1911(c,2,1)),merge(b)]. given #641 (T,wt=10): 6837 p(k,j) | p(k,b) | p(k,g(j)). [para(61(a,1),6751(b,1)),merge(b)]. given #642 (A,wt=36): 375 p(m,b) | p(x,b) | p(x,g(x)) | f(g(m)) = b | -p(f(g(m)),x) | g(m) = b | f(g(m)) = g(m) | -p(f(g(m)),g(m)). [resolve(371,b,34,h),flip(d),flip(f),flip(g)]. given #643 (T,wt=10): 6889 p(k,j) | p(k,b) | p(b,g(b)). [para(6738(b,1),6756(c,1)),merge(b)]. given #644 (T,wt=10): 6895 p(k,j) | p(k,b) | p(b,g(j)). [para(6738(b,1),6837(c,1)),merge(b)]. given #645 (T,wt=12): 6725 k = m | p(k,m) | k = b | -p(k,b). [resolve(6716,a,2,f),flip(a),flip(d),unit_del(c,27)]. given #646 (T,wt=12): 6744 p(k,j) | j = x | p(x,j) | b != x. [para(6738(b,1),31(c,1))]. given #647 (A,wt=35): 377 p(m,b) | p(f(g(m)),b) | p(f(g(m)),g(f(g(m)))) | g(m) = b | b = x | g(m) = x | -p(g(m),x) | -p(x,g(m)). [resolve(371,b,34,d),flip(d),flip(f)]. given #648 (T,wt=12): 6749 p(k,j) | j = x | -p(x,b) | k = x. [para(6738(b,1),89(c,2)),merge(b)]. given #649 (T,wt=13): 6730 p(k,b) | p(g(k),k) | p(b,j) | p(b,b). [para(477(d,1),6716(a,2))]. given #650 (T,wt=13): 6731 p(k,b) | p(k,g(k)) | p(b,j) | p(b,b). [para(479(d,1),6716(a,2))]. given #651 (T,wt=13): 6742 p(x,b) | p(x,g(x)) | p(k,j) | k = x. [para(20(a,1),6738(b,2))]. given #652 (A,wt=29): 378 p(m,b) | f(g(m)) = b | -p(f(g(m)),b) | g(m) = b | f(g(m)) = g(m) | -p(f(g(m)),g(m)). [resolve(371,b,4,f),flip(b),flip(d),flip(e)]. given #653 (T,wt=13): 6743 p(x,b) | p(g(x),x) | p(k,j) | k = x. [para(22(a,1),6738(b,2))]. given #654 (T,wt=13): 6752 p(k,j) | p(j,k) | p(j,b) | p(j,g(b)). [para(6738(b,1),1771(d,2,1)),merge(b)]. given #655 (T,wt=13): 6761 p(x,b) | p(x,g(x)) | p(k,j) | j = x. [para(20(a,1),6747(b,2))]. given #656 (T,wt=13): 6762 p(x,b) | p(g(x),x) | p(k,j) | j = x. [para(22(a,1),6747(b,2))]. given #657 (A,wt=20): 381 p(k,b) | p(g(k),k) | p(x,b) | p(g(x),x) | j = x | p(x,j). [resolve(43,c,31,c)]. given #658 (T,wt=13): 6766 p(k,j) | p(j,k) | p(j,b) | p(b,g(k)). [para(6747(b,1),1771(d,1)),merge(b)]. given #659 (T,wt=10): 7062 p(k,j) | p(j,b) | p(b,g(k)). [para(6738(b,1),6766(b,2)),merge(b),merge(d)]. given #660 (T,wt=13): 7006 p(x,b) | p(x,g(x)) | p(k,j) | p(b,x). [para(6742(d,1),6716(a,2))]. given #661 (T,wt=13): 7009 p(x,b) | p(x,g(x)) | p(k,j) | p(m,x). [factor(7005,a,e),merge(e),merge(f)]. given #662 (A,wt=23): 382 p(f(x),b) | p(g(f(x)),f(x)) | p(x,b) | p(g(x),x) | m = x | -p(x,m). [resolve(43,c,10,c)]. given #663 (T,wt=13): 7010 p(j,b) | p(j,g(j)) | p(k,j) | p(k,b). [factor(7008,b,e)]. given #664 (T,wt=13): 7020 p(x,b) | p(g(x),x) | p(k,j) | p(b,x). [para(6743(d,1),6716(a,2))]. given #665 (T,wt=13): 7026 p(k,j) | p(j,k) | p(j,b) | p(k,g(b)). [para(61(a,1),6752(d,1)),merge(b)]. given #666 (T,wt=10): 7237 p(k,j) | p(j,b) | p(k,g(b)). [para(6738(b,1),7026(b,2)),merge(b),merge(d)]. given #667 (A,wt=32): 429 p(b,b) | p(g(b),b) | g(b) = b | p(g(g(g(b))),b) | p(g(g(g(g(b)))),g(g(g(b)))) | p(g(g(b)),b). [resolve(44,d,37,c(flip))]. given #668 (T,wt=13): 7032 p(k,j) | p(j,k) | p(j,b) | p(b,g(b)). [para(6747(b,1),6752(d,1)),merge(b)]. given #669 (T,wt=10): 7251 p(k,j) | p(j,b) | p(b,g(b)). [para(6738(b,1),7032(b,2)),merge(b),merge(d)]. given #670 (T,wt=13): 7130 p(x,b) | p(x,g(x)) | p(k,j) | p(x,x). [factor(7098,a,c),merge(c)]. given #671 (T,wt=13): 7208 p(k,j) | p(j,b) | p(j,g(k)) | p(k,b). [para(61(a,1),7010(b,2,1)),merge(d)]. given #672 (A,wt=32): 430 p(b,b) | p(g(b),b) | g(b) = b | p(g(g(g(b))),b) | p(g(g(g(b))),g(g(g(g(b))))) | p(g(g(b)),b). [resolve(44,d,32,c(flip))]. given #673 (T,wt=13): 7219 p(k,j) | p(j,b) | p(j,g(b)) | p(k,b). [para(6747(b,1),7010(b,2,1)),merge(d)]. given #674 (T,wt=14): 6827 p(j,b) | p(j,k) | g(j) = j | g(j) = k. [resolve(6727,b,29,b),flip(c),flip(d)]. given #675 (T,wt=13): 7336 p(j,b) | p(j,k) | g(j) = k | j = b. [resolve(6827,c,18,c),flip(d),merge(e)]. given #676 (T,wt=9): 7370 p(j,b) | p(j,k) | j = b. [para(7336(c,1),6726(b,2)),merge(d),merge(e),merge(f)]. given #677 (A,wt=23): 431 p(x,b) | p(x,g(x)) | p(b,b) | p(g(b),b) | g(b) = b | g(g(x)) != b. [para(20(a,1),44(d,1,1,1))]. given #678 (T,wt=9): 7375 p(j,b) | p(j,k) | j = k. [resolve(7370,c,26,b(flip)),flip(c),merge(d)]. given #679 (T,wt=9): 7420 p(j,b) | p(j,k) | k = b. [para(7375(c,1),7370(c,1)),merge(c),merge(d)]. given #680 (T,wt=9): 7428 p(j,b) | p(j,k) | p(m,b). [para(7420(c,1),2026(a,2)),merge(d)]. given #681 (T,wt=9): 7430 p(j,b) | p(j,k) | p(b,b). [para(7420(c,1),6716(a,2))]. given #682 (A,wt=23): 432 p(x,b) | p(x,g(x)) | p(b,b) | p(g(b),b) | g(b) = b | g(g(b)) != x. [para(20(a,1),44(d,2))]. given #683 (T,wt=10): 7419 p(j,b) | p(j,k) | g(j) = k. [para(7375(c,1),6827(c,2)),merge(c),merge(d),merge(f)]. given #684 (T,wt=6): 7499 p(j,b) | p(j,k). [para(7419(c,1),6726(b,2)),merge(c),merge(d),merge(e)]. given #685 (T,wt=6): 7519 p(k,j) | p(j,b). [para(6738(b,1),7499(b,2)),merge(c)]. given #686 (T,wt=6): 7527 p(k,j) | p(k,b). [para(61(a,1),7519(b,1)),merge(b)]. given #687 (A,wt=23): 433 p(x,b) | p(g(x),x) | p(b,b) | p(g(b),b) | g(b) = b | g(g(x)) != b. [para(22(a,1),44(d,1,1,1))]. given #688 (T,wt=10): 7531 p(x,b) | p(x,g(x)) | p(k,j). [para(6761(d,1),7519(b,1)),merge(d),merge(e)]. given #689 (T,wt=10): 7532 p(x,b) | p(g(x),x) | p(k,j). [para(6762(d,1),7519(b,1)),merge(d),merge(e)]. given #690 (T,wt=10): 7548 p(b,j) | p(k,b) | p(g(k),k). [para(59(a,1),7527(a,2)),merge(d),merge(e)]. given #691 (T,wt=10): 7549 p(b,j) | p(k,b) | p(k,g(k)). [para(60(a,1),7527(a,2)),merge(d),merge(e)]. given #692 (A,wt=23): 434 p(x,b) | p(g(x),x) | p(b,b) | p(g(b),b) | g(b) = b | g(g(b)) != x. [para(22(a,1),44(d,2))]. given #693 (T,wt=12): 7512 p(j,b) | j = k | j = m | j = b. [resolve(7499,b,6,d),flip(b),flip(c),flip(d)]. given #694 (T,wt=12): 7643 p(j,b) | j = m | j = b | p(k,k). [para(7512(b,1),7499(b,1)),merge(d)]. given #695 (T,wt=12): 7645 p(j,b) | j = m | j = b | k = b. [factor(7640,c,d),unit_del(d,6716)]. given #696 (T,wt=12): 7671 p(j,b) | j = b | k = b | -p(b,m). [factor(7660,b,d),merge(e)]. given #697 (A,wt=29): 435 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,b) | p(g(b),b) | g(b) = b | g(g(x)) != b. [para(32(c,1),44(d,1,1,1))]. given #698 (T,wt=13): 7648 p(j,b) | j = b | p(k,k) | p(g(j),j). [resolve(7643,b,58,c(flip)),merge(d)]. given #699 (T,wt=13): 7649 p(j,b) | j = b | p(k,k) | p(j,g(j)). [resolve(7643,b,57,c(flip)),merge(d)]. given #700 (T,wt=13): 7658 p(j,b) | j = b | k = b | p(g(j),j). [resolve(7645,b,58,c(flip)),merge(d)]. given #701 (T,wt=13): 7659 p(j,b) | j = b | k = b | p(j,g(j)). [resolve(7645,b,57,c(flip)),merge(d)]. given #702 (A,wt=29): 436 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,b) | p(g(b),b) | g(b) = b | g(g(b)) != x. [para(32(c,1),44(d,2))]. given #703 (T,wt=13): 7687 p(j,b) | p(k,k) | p(g(j),j) | p(k,b). [para(7648(b,1),7527(a,2)),merge(e)]. given #704 (T,wt=13): 7691 p(j,b) | p(k,k) | p(j,g(j)) | p(k,b). [para(7649(b,1),7527(a,2)),merge(e)]. given #705 (T,wt=13): 7696 p(j,b) | k = b | p(g(j),j) | p(k,b). [para(7658(b,1),7527(a,2)),merge(e)]. given #706 (T,wt=10): 7748 p(j,b) | p(g(j),j) | p(k,b). [para(7696(b,1),7499(b,2)),merge(d),merge(e)]. given #707 (A,wt=29): 437 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,b) | p(g(b),b) | g(b) = b | g(g(x)) != b. [para(37(c,1),44(d,1,1,1))]. given #708 (T,wt=13): 7701 p(j,b) | k = b | p(j,g(j)) | p(k,b). [para(7659(b,1),7527(a,2)),merge(e)]. given #709 (T,wt=10): 7801 p(j,b) | p(j,g(j)) | p(k,b). [para(7701(b,1),7499(b,2)),merge(d),merge(e)]. given #710 (T,wt=14): 7760 p(j,b) | p(k,b) | g(j) = j | g(j) = k. [resolve(7748,b,29,b),flip(c),flip(d)]. given #711 (T,wt=13): 7839 p(j,b) | p(k,b) | g(j) = k | j = b. [resolve(7760,c,18,c),flip(d),merge(e)]. given #712 (A,wt=29): 438 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,b) | p(g(b),b) | g(b) = b | g(g(b)) != x. [para(37(c,1),44(d,2))]. given #713 (T,wt=12): 7853 p(j,b) | p(k,b) | j = b | k != b. [para(7839(c,1),16(c,1)),flip(d),merge(d),merge(e)]. given #714 (T,wt=12): 7854 p(j,b) | p(k,b) | j = b | j != k. [para(7839(c,1),18(c,1)),flip(d),flip(f),merge(d),merge(e)]. given #715 (T,wt=12): 7870 p(j,b) | p(k,b) | j = b | j = m. [resolve(7854,d,7512,b),merge(d),merge(f)]. given #716 (T,wt=12): 7879 p(j,b) | p(k,b) | j = b | p(k,m). [para(7870(d,1),7527(a,2)),merge(e)]. given #717 (A,wt=41): 650 p(g(j),b) | p(g(j),k) | p(g(j),j) | p(j,b) | g(g(j)) = b | -p(g(g(j)),j) | g(j) = b | g(g(j)) = g(j) | -p(g(g(j)),g(j)). [factor(641,c,e),flip(g)]. given #718 (T,wt=9): 7896 p(j,b) | p(k,b) | p(k,m). [para(7879(c,1),7527(a,2)),merge(d),merge(e)]. given #719 (T,wt=12): 7885 p(j,b) | p(k,b) | j = b | k != m. [para(7870(d,1),7854(d,1)),flip(g),merge(d),merge(e),merge(f)]. given #720 (T,wt=13): 7848 p(j,b) | p(k,b) | g(j) = k | p(j,j). [para(7760(c,1),7748(b,1)),merge(d),merge(f)]. given #721 (T,wt=13): 7851 p(j,b) | p(k,b) | j = b | p(g(k),k). [resolve(7839,c,40,e),flip(f),merge(d),merge(f),merge(g)]. given #722 (A,wt=26): 671 p(g(g(k)),b) | p(g(g(k)),g(g(g(k)))) | p(g(k),b) | p(k,b) | j = b | p(b,j). [resolve(65,d,31,c(flip))]. given #723 (T,wt=10): 7943 p(j,b) | p(k,b) | p(g(k),k). [para(7851(c,1),7527(a,2)),merge(d),merge(e)]. given #724 (T,wt=13): 7852 p(j,b) | p(k,b) | j = b | p(k,g(k)). [resolve(7839,c,35,e),flip(f),merge(d),merge(f),merge(g)]. given #725 (T,wt=10): 7988 p(j,b) | p(k,b) | p(k,g(k)). [para(7852(c,1),7527(a,2)),merge(d),merge(e)]. given #726 (T,wt=10): 8004 p(k,b) | p(k,g(k)) | p(j,k). [factor(7996,a,d),merge(d)]. given #727 (A,wt=20): 672 p(g(g(m)),b) | p(g(g(m)),g(g(g(m)))) | p(g(m),b) | p(m,b). [resolve(65,d,27,a(flip))]. given #728 (T,wt=13): 7880 p(j,b) | p(k,b) | j = b | p(g(m),j). [para(7870(d,1),7748(b,1,1)),merge(d),merge(f)]. given #729 (T,wt=10): 8052 p(j,b) | p(k,b) | p(g(m),j). [para(7880(c,1),7527(a,2)),merge(d),merge(e)]. given #730 (T,wt=13): 7881 p(j,b) | p(k,b) | j = b | p(g(j),m). [para(7870(d,1),7748(b,2)),merge(d),merge(f)]. given #731 (T,wt=10): 8086 p(j,b) | p(k,b) | p(g(j),m). [para(7881(c,1),7527(a,2)),merge(d),merge(e)]. given #732 (A,wt=31): 673 p(g(g(g(x))),b) | p(g(g(g(x))),g(g(g(g(x))))) | p(g(g(x)),b) | p(g(x),b) | b = x | p(x,b). [resolve(65,d,16,c(flip))]. given #733 (T,wt=13): 7882 p(j,b) | p(k,b) | j = b | p(m,g(j)). [para(7870(d,1),7801(b,1)),merge(d),merge(f)]. given #734 (T,wt=10): 8209 p(j,b) | p(k,b) | p(m,g(j)). [para(7882(c,1),7527(a,2)),merge(d),merge(e)]. given #735 (T,wt=13): 7883 p(j,b) | p(k,b) | j = b | p(j,g(m)). [para(7870(d,1),7801(b,2,1)),merge(d),merge(f)]. given #736 (T,wt=10): 8242 p(j,b) | p(k,b) | p(j,g(m)). [para(7883(c,1),7527(a,2)),merge(d),merge(e)]. given #737 (A,wt=28): 674 p(g(g(f(b))),b) | p(g(g(f(b))),g(g(g(f(b))))) | p(g(f(b)),b) | p(f(b),b) | -p(b,m). [resolve(65,d,10,c(flip)),unit_del(e,27)]. given #738 (T,wt=13): 7884 p(j,b) | p(k,b) | j = b | g(m) = k. [para(7870(d,1),7839(c,1,1)),merge(d),merge(e),merge(g)]. given #739 (T,wt=13): 7924 p(k,b) | p(g(k),k) | p(j,k) | p(k,m). [factor(7914,a,d)]. given #740 (T,wt=13): 8071 p(j,b) | p(k,b) | j = b | p(g(m),m). [para(7870(d,1),8052(c,2)),merge(d),merge(e)]. given #741 (T,wt=10): 8307 p(j,b) | p(k,b) | p(g(m),m). [para(8071(c,1),7527(a,2)),merge(d),merge(e)]. given #742 (A,wt=38): 675 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | b = y | -p(y,x) | b = z | z = y | -p(y,z) | -p(z,y). [para(65(d,1),4(b,2))]. given #743 (T,wt=13): 8113 p(j,b) | p(k,b) | g(j) = k | p(j,m). [para(7760(c,1),8086(c,1)),merge(d),merge(e)]. given #744 (T,wt=13): 8262 p(j,b) | p(k,b) | j = b | p(m,g(m)). [para(7870(d,1),8242(c,1)),merge(d),merge(e)]. given #745 (T,wt=10): 8452 p(j,b) | p(k,b) | p(m,g(m)). [para(8262(c,1),7527(a,2)),merge(d),merge(e)]. given #746 (T,wt=14): 8065 p(j,b) | p(k,b) | g(m) = j | g(m) = k. [resolve(8052,c,29,b),flip(c),flip(d)]. given #747 (A,wt=30): 676 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | b = y | p(y,b) | g(y) != x. [para(65(d,1),16(c,2))]. given #748 (T,wt=13): 8502 p(j,b) | p(k,b) | g(m) = k | p(j,j). [para(8065(c,1),8052(c,1)),merge(d),merge(e)]. given #749 (T,wt=13): 8503 p(j,b) | p(k,b) | g(m) = k | p(j,m). [para(8065(c,1),8307(c,1)),merge(d),merge(e)]. given #750 (T,wt=14): 8226 p(k,b) | p(g(k),k) | p(j,k) | p(m,g(j)). [factor(8218,a,d)]. given #751 (T,wt=14): 8470 p(k,b) | p(g(k),k) | p(j,k) | p(m,g(m)). [factor(8462,a,d)]. given #752 (A,wt=30): 677 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | x = y | p(y,b) | p(y,g(y)). [para(65(d,1),20(a,1))]. given #753 (T,wt=15): 6741 p(k,j) | k = x | m = x | b = x | -p(x,b). [para(6738(b,1),6(d,2))]. given #754 (T,wt=15): 6759 p(m,k) | k = b | j = b | j = k | -p(j,k). [resolve(6746,a,2022,e),flip(d),flip(e),merge(b)]. given #755 (T,wt=15): 6804 p(m,k) | j = b | -p(j,b) | j = m | -p(j,m). [resolve(6760,b,4,f),flip(b),flip(d),flip(e),unit_del(d,27)]. given #756 (T,wt=15): 6805 p(m,k) | -p(m,b) | j = b | j = m | -p(j,m). [resolve(6760,b,4,e),flip(b),flip(d),unit_del(b,27)]. given #757 (A,wt=30): 678 p(x,b) | p(x,g(x)) | p(g(g(y)),b) | p(g(g(y)),g(g(g(y)))) | p(g(y),b) | x = y | p(y,b). [para(20(a,1),65(d,1))]. given #758 (T,wt=15): 7644 p(j,b) | j = m | j = b | -p(m,k) | k = m. [factor(7640,b,d)]. given #759 (T,wt=15): 7651 p(j,b) | j = b | p(k,k) | p(k,m) | p(m,b). [para(7643(b,1),2976(a,2))]. given #760 (T,wt=15): 7652 p(j,b) | j = b | p(k,k) | p(k,m) | p(b,b). [para(7643(b,1),6758(a,2))]. given #761 (T,wt=15): 7662 p(j,b) | j = b | k = b | p(k,m) | p(m,b). [para(7645(b,1),2976(a,2))]. given #762 (A,wt=30): 679 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | x = y | p(y,b) | p(g(y),y). [para(65(d,1),22(a,1))]. given #763 (T,wt=15): 7663 p(j,b) | j = b | k = b | p(b,m) | p(k,m). [para(7645(b,1),3446(b,2))]. given #764 (T,wt=15): 7667 p(j,b) | j = b | k = b | p(k,m) | p(b,b). [para(7645(b,1),6758(a,2))]. given #765 (T,wt=15): 8516 p(j,b) | p(k,b) | p(j,j) | p(m,b) | k != b. [para(8502(c,1),16(c,1)),flip(d),unit_del(d,27)]. given #766 (T,wt=15): 8517 p(j,b) | p(k,b) | p(j,j) | p(m,b) | k != m. [para(8502(c,1),18(c,1)),flip(d),unit_del(d,27)]. given #767 (A,wt=30): 680 p(x,b) | p(g(x),x) | p(g(g(y)),b) | p(g(g(y)),g(g(g(y)))) | p(g(y),b) | x = y | p(y,b). [para(22(a,1),65(d,1))]. given #768 (T,wt=15): 8541 p(j,b) | p(k,b) | p(j,m) | p(m,b) | k != b. [para(8503(c,1),16(c,1)),flip(d),unit_del(d,27)]. given #769 (T,wt=15): 8542 p(j,b) | p(k,b) | p(j,m) | p(m,b) | k != m. [para(8503(c,1),18(c,1)),flip(d),unit_del(d,27)]. given #770 (T,wt=15): 8596 p(m,k) | k = b | j = b | j = k | -p(j,m). [para(49(a,1),6759(e,2)),merge(b)]. given #771 (T,wt=15): 8601 p(j,b) | j = m | j = b | k = m | p(b,m). [resolve(7644,d,3339,a)]. given #772 (A,wt=29): 681 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | k = y | x != y | p(y,k). [para(65(d,1),26(b,1))]. given #773 (T,wt=15): 8603 p(j,b) | j = m | j = b | k = m | p(m,b). [resolve(7644,d,2026,a)]. given #774 (T,wt=15): 8669 p(j,b) | j = b | k = m | p(b,m) | p(k,m). [para(8601(b,1),3446(b,2)),merge(e)]. given #775 (T,wt=15): 8676 p(j,b) | j = b | k = m | p(m,b) | p(k,m). [para(8603(b,1),2976(a,2)),merge(f)]. given #776 (T,wt=16): 6728 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k). [para(32(c,1),6716(a,1))]. given #777 (A,wt=23): 682 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | m != x. [para(65(d,1),27(a,2))]. given #778 (T,wt=16): 6729 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(x,k). [para(37(c,1),6716(a,1))]. given #779 (T,wt=16): 7550 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(b,j). [para(63(d,1),7527(a,2)),merge(e),merge(f)]. given #780 (T,wt=16): 7552 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | p(b,j). [para(173(d,1),7527(a,2)),merge(e),merge(f)]. given #781 (T,wt=16): 7913 p(x,b) | p(x,g(x)) | p(j,x) | p(k,b) | p(k,m). [para(20(a,1),7896(a,2))]. given #782 (A,wt=36): 683 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(g(y),b) | p(g(y),g(g(y))) | x = y | p(y,b). [para(65(d,1),32(c,1))]. given #783 (T,wt=16): 7914 p(x,b) | p(g(x),x) | p(j,x) | p(k,b) | p(k,m). [para(22(a,1),7896(a,2))]. given #784 (T,wt=16): 8019 p(k,b) | p(k,g(k)) | j = k | j = m | j = b. [resolve(8004,c,6,d),flip(c),flip(d),flip(e)]. given #785 (T,wt=13): 8836 p(k,b) | p(k,g(k)) | j = m | j = b. [para(8019(c,1),7988(a,1)),merge(e),merge(f),merge(g)]. given #786 (T,wt=13): 8841 p(k,b) | p(k,g(k)) | j = b | p(k,m). [para(8836(c,1),7527(a,2)),merge(e)]. given #787 (A,wt=36): 684 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(g(g(y)),b) | p(g(g(y)),g(g(g(y)))) | p(g(y),b) | x = y | p(y,b). [para(32(c,1),65(d,1))]. given #788 (T,wt=10): 8854 p(k,b) | p(k,g(k)) | p(k,m). [para(8841(c,1),7527(a,2)),merge(d),merge(e)]. given #789 (T,wt=13): 8842 p(k,b) | p(k,g(k)) | j = b | p(m,b). [para(8836(c,1),7988(a,1)),merge(e),merge(f)]. given #790 (T,wt=10): 8880 p(k,b) | p(k,g(k)) | p(m,b). [para(8842(c,1),2976(a,2)),merge(d),merge(e)]. given #791 (T,wt=16): 8107 p(j,b) | p(k,b) | g(j) = m | p(f(g(j)),g(j)). [resolve(8086,c,14,b),flip(c)]. given #792 (A,wt=33): 686 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(x,m). [para(65(d,1),33(c,1))]. given #793 (T,wt=15): 8907 p(j,b) | p(k,b) | p(f(g(j)),g(j)) | p(m,j). [para(8107(c,1),7748(b,1)),merge(d),merge(f)]. given #794 (T,wt=15): 8908 p(j,b) | p(k,b) | p(f(g(j)),g(j)) | p(j,m). [para(8107(c,1),7801(b,2)),merge(d),merge(f)]. given #795 (T,wt=14): 8995 p(j,b) | p(k,b) | p(j,m) | p(f(k),g(j)). [para(8113(c,1),8908(c,1,1)),merge(d),merge(e),merge(g)]. given #796 (T,wt=13): 9031 p(j,b) | p(k,b) | p(j,m) | p(f(k),k). [para(8113(c,1),8995(d,2)),merge(d),merge(e),merge(f)]. given #797 (A,wt=36): 689 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(g(y),b) | p(g(g(y)),g(y)) | x = y | p(y,b). [para(65(d,1),37(c,1))]. given #798 (T,wt=14): 8996 p(j,b) | p(k,b) | p(j,m) | p(f(g(j)),k). [para(8113(c,1),8908(c,2)),merge(d),merge(e),merge(g)]. given #799 (T,wt=15): 8913 p(j,b) | p(k,b) | p(f(g(j)),g(j)) | p(m,m). [para(8107(c,1),8086(c,1)),merge(d),merge(e)]. given #800 (T,wt=16): 8108 p(j,b) | p(k,b) | g(j) = m | p(g(j),f(g(j))). [resolve(8086,c,12,b),flip(c)]. given #801 (T,wt=15): 9171 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(m,j). [para(8108(c,1),7748(b,1)),merge(d),merge(f)]. given #802 (A,wt=36): 690 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(g(g(y)),b) | p(g(g(y)),g(g(g(y)))) | p(g(y),b) | x = y | p(y,b). [para(37(c,1),65(d,1))]. given #803 (T,wt=15): 9172 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(j,m). [para(8108(c,1),7801(b,2)),merge(d),merge(f)]. given #804 (T,wt=14): 9256 p(j,b) | p(k,b) | p(j,m) | p(k,f(g(j))). [para(8113(c,1),9172(c,1)),merge(d),merge(e),merge(g)]. given #805 (T,wt=14): 9257 p(j,b) | p(k,b) | p(j,m) | p(g(j),f(k)). [para(8113(c,1),9172(c,2,1)),merge(d),merge(e),merge(g)]. given #806 (T,wt=13): 9296 p(j,b) | p(k,b) | p(j,m) | p(k,f(k)). [para(8113(c,1),9257(d,1)),merge(d),merge(e),merge(f)]. given #807 (A,wt=33): 693 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(f(b),b) | p(g(f(b)),f(b)) | -p(x,m). [para(65(d,1),38(c,1))]. given #808 (T,wt=15): 9177 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(m,m). [para(8108(c,1),8086(c,1)),merge(d),merge(e)]. given #809 (T,wt=16): 8328 p(j,b) | p(k,b) | g(m) = m | p(f(g(m)),g(m)). [resolve(8307,c,14,b),flip(c)]. given #810 (T,wt=15): 9367 p(j,b) | p(k,b) | p(f(g(m)),g(m)) | p(m,j). [para(8328(c,1),8052(c,1)),merge(d),merge(e)]. given #811 (T,wt=15): 9368 p(j,b) | p(k,b) | p(f(g(m)),g(m)) | p(j,m). [para(8328(c,1),8242(c,2)),merge(d),merge(e)]. given #812 (A,wt=43): 704 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(g(g(y)),b) | p(g(g(y)),g(g(g(y)))) | p(g(y),b) | x = y | p(y,b). [para(65(d,1),65(d,1))]. given #813 (T,wt=14): 9436 p(j,b) | p(k,b) | p(j,m) | p(f(k),g(m)). [para(8503(c,1),9368(c,1,1)),merge(d),merge(e),merge(g)]. given #814 (T,wt=14): 9437 p(j,b) | p(k,b) | p(j,m) | p(f(g(m)),k). [para(8503(c,1),9368(c,2)),merge(d),merge(e),merge(g)]. given #815 (T,wt=15): 9370 p(j,b) | p(k,b) | p(f(g(m)),g(m)) | p(m,m). [para(8328(c,1),8307(c,1)),merge(d),merge(e)]. given #816 (T,wt=16): 8329 p(j,b) | p(k,b) | g(m) = m | p(g(m),f(g(m))). [resolve(8307,c,12,b),flip(c)]. given #817 (A,wt=31): 706 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | g(g(x)) = b | g(g(g(x))) != x. [factor(676,a,f),flip(e)]. given #818 (T,wt=15): 9562 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(m,j). [para(8329(c,1),8052(c,1)),merge(d),merge(e)]. given #819 (T,wt=15): 9563 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(j,m). [para(8329(c,1),8242(c,2)),merge(d),merge(e)]. given #820 (T,wt=14): 9636 p(j,b) | p(k,b) | p(j,m) | p(k,f(g(m))). [para(8503(c,1),9563(c,1)),merge(d),merge(e),merge(g)]. given #821 (T,wt=14): 9637 p(j,b) | p(k,b) | p(j,m) | p(g(m),f(k)). [para(8503(c,1),9563(c,2,1)),merge(d),merge(e),merge(g)]. given #822 (A,wt=29): 707 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | g(x) = b | g(g(x)) != x. [factor(676,c,f),flip(e)]. given #823 (T,wt=15): 9565 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(m,m). [para(8329(c,1),8307(c,1)),merge(d),merge(e)]. given #824 (T,wt=16): 8480 p(j,b) | p(k,b) | g(m) = k | p(m,b) | j != b. [para(8065(c,1),16(c,1)),flip(d),unit_del(d,27)]. given #825 (T,wt=16): 8481 p(j,b) | p(k,b) | g(m) = k | p(m,b) | j != m. [para(8065(c,1),18(c,1)),flip(d),unit_del(d,27)]. given #826 (T,wt=16): 8483 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(m,j). [para(8065(c,1),56(b,2))]. given #827 (A,wt=25): 708 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | g(g(x)) = x. [factor(677,a,f),flip(e),merge(f)]. given #828 (T,wt=15): 9743 p(j,b) | p(k,b) | p(m,b) | p(m,j) | k != b. [para(8483(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #829 (T,wt=15): 9744 p(j,b) | p(k,b) | p(m,b) | p(m,j) | k != m. [para(8483(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #830 (T,wt=16): 8665 p(j,b) | j = b | k = m | p(b,m) | p(g(j),j). [resolve(8601,b,58,c(flip)),merge(e)]. given #831 (T,wt=16): 8666 p(j,b) | j = b | k = m | p(b,m) | p(j,g(j)). [resolve(8601,b,57,c(flip)),merge(e)]. given #832 (A,wt=24): 709 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | g(x) = x. [factor(683,a,e),flip(f),merge(e),merge(g)]. given #833 (T,wt=16): 8673 p(j,b) | j = b | k = m | p(m,b) | p(g(j),j). [resolve(8603,b,58,c(flip)),merge(e)]. given #834 (T,wt=16): 8674 p(j,b) | j = b | k = m | p(m,b) | p(j,g(j)). [resolve(8603,b,57,c(flip)),merge(e)]. given #835 (T,wt=16): 8843 p(k,b) | p(k,g(k)) | j = b | -p(b,m) | k = b. [factor(8837,c,d)]. given #836 (T,wt=16): 9311 p(j,b) | p(k,b) | j = b | p(m,m) | p(k,f(k)). [para(7870(d,1),9296(c,1)),merge(d),merge(e)]. given #837 (A,wt=27): 751 p(x,b) | p(x,g(x)) | p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(x,m). [para(20(a,1),66(d,1))]. given #838 (T,wt=13): 9816 p(j,b) | p(k,b) | p(m,m) | p(k,f(k)). [para(9311(c,1),7527(a,2)),merge(e),merge(f)]. given #839 (T,wt=16): 9804 p(k,b) | p(k,g(k)) | j = b | -p(k,m) | k = b. [factor(9797,a,c),merge(c)]. given #840 (T,wt=17): 7996 p(x,b) | p(x,g(x)) | p(j,x) | p(k,b) | p(k,g(k)). [para(20(a,1),7988(a,2))]. given #841 (T,wt=17): 7997 p(x,b) | p(g(x),x) | p(j,x) | p(k,b) | p(k,g(k)). [para(22(a,1),7988(a,2))]. given #842 (A,wt=27): 752 p(x,b) | p(g(x),x) | p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(x,m). [para(22(a,1),66(d,1))]. given #843 (T,wt=17): 8001 p(k,b) | p(k,g(k)) | p(x,b) | p(x,g(x)) | p(x,j). [para(145(e,1),7988(a,1)),merge(f),merge(g),merge(h)]. given #844 (T,wt=17): 8003 p(x,b) | p(g(x),x) | p(k,b) | p(k,g(k)) | p(x,j). [para(337(e,1),7988(a,1)),merge(f),merge(g),merge(h)]. given #845 (T,wt=17): 8217 p(x,b) | p(x,g(x)) | p(j,x) | p(k,b) | p(m,g(j)). [para(20(a,1),8209(a,2))]. given #846 (T,wt=17): 8218 p(x,b) | p(g(x),x) | p(j,x) | p(k,b) | p(m,g(j)). [para(22(a,1),8209(a,2))]. given #847 (A,wt=33): 753 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(x,m). [para(32(c,1),66(d,1))]. given #848 (T,wt=17): 8275 p(j,b) | p(k,b) | j = b | p(m,b) | p(f(k),g(m)). [para(7884(d,1),361(b,1,1))]. given #849 (T,wt=14): 10028 p(j,b) | p(k,b) | p(m,b) | p(f(k),g(m)). [para(8275(c,1),2976(a,2)),merge(e),merge(f)]. given #850 (T,wt=16): 10044 p(j,b) | p(k,b) | j = b | p(m,b) | p(f(k),k). [para(7884(d,1),10028(d,2)),merge(d),merge(e)]. given #851 (T,wt=13): 10073 p(j,b) | p(k,b) | p(m,b) | p(f(k),k). [para(10044(c,1),2976(a,2)),merge(e),merge(f)]. given #852 (A,wt=33): 754 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(x,m). [para(37(c,1),66(d,1))]. given #853 (T,wt=17): 8276 p(j,b) | p(k,b) | j = b | p(m,b) | p(f(g(m)),k). [para(7884(d,1),361(b,2))]. given #854 (T,wt=14): 10117 p(j,b) | p(k,b) | p(m,b) | p(f(g(m)),k). [para(8276(c,1),2976(a,2)),merge(e),merge(f)]. given #855 (T,wt=17): 8277 p(j,b) | p(k,b) | j = b | p(m,b) | p(k,f(g(m))). [para(7884(d,1),371(b,1))]. given #856 (T,wt=14): 10160 p(j,b) | p(k,b) | p(m,b) | p(k,f(g(m))). [para(8277(c,1),2976(a,2)),merge(e),merge(f)]. given #857 (A,wt=40): 755 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(x,m). [para(65(d,1),66(d,1))]. given #858 (T,wt=17): 8278 p(j,b) | p(k,b) | j = b | p(m,b) | p(g(m),f(k)). [para(7884(d,1),371(b,2,1))]. given #859 (T,wt=14): 10194 p(j,b) | p(k,b) | p(m,b) | p(g(m),f(k)). [para(8278(c,1),2976(a,2)),merge(e),merge(f)]. given #860 (T,wt=16): 10215 p(j,b) | p(k,b) | j = b | p(m,b) | p(k,f(k)). [para(7884(d,1),10194(d,1)),merge(d),merge(e)]. given #861 (T,wt=13): 10239 p(j,b) | p(k,b) | p(m,b) | p(k,f(k)). [para(10215(c,1),2976(a,2)),merge(e),merge(f)]. given #862 (A,wt=22): 756 p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(g(f(b)),m). [factor(751,a,c),merge(c)]. given #863 (T,wt=17): 8461 p(x,b) | p(x,g(x)) | p(j,x) | p(k,b) | p(m,g(m)). [para(20(a,1),8452(a,2))]. given #864 (T,wt=17): 8462 p(x,b) | p(g(x),x) | p(j,x) | p(k,b) | p(m,g(m)). [para(22(a,1),8452(a,2))]. given #865 (T,wt=17): 8944 p(j,b) | p(k,b) | j = b | p(f(k),g(j)) | p(m,j). [para(7839(c,1),8907(c,1,1)),merge(d),merge(e)]. given #866 (T,wt=14): 10342 p(j,b) | p(k,b) | p(f(k),g(j)) | p(m,j). [para(8944(c,1),7527(a,2)),merge(e),merge(f)]. given #867 (A,wt=21): 757 p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(f(b),m). [factor(753,a,d),merge(d),merge(e)]. given #868 (T,wt=16): 10364 p(j,b) | p(k,b) | j = b | p(f(k),k) | p(m,j). [para(7839(c,1),10342(c,2)),merge(d),merge(e)]. given #869 (T,wt=13): 10400 p(j,b) | p(k,b) | p(f(k),k) | p(m,j). [para(10364(c,1),7527(a,2)),merge(e),merge(f)]. given #870 (T,wt=17): 8945 p(j,b) | p(k,b) | j = b | p(f(g(j)),k) | p(m,j). [para(7839(c,1),8907(c,2)),merge(d),merge(e)]. given #871 (T,wt=14): 10444 p(j,b) | p(k,b) | p(f(g(j)),k) | p(m,j). [para(8945(c,1),7527(a,2)),merge(e),merge(f)]. given #872 (A,wt=43): 806 p(g(f(g(m))),b) | p(g(f(g(m))),g(g(f(g(m))))) | p(f(g(m)),b) | g(m) = b | b = x | g(m) = x | -p(g(m),x) | -p(x,g(m)) | p(m,b). [resolve(67,e,371,b),flip(d),flip(f)]. given #873 (T,wt=17): 9139 p(j,b) | p(k,b) | j = b | p(f(k),g(j)) | p(m,m). [para(7839(c,1),8913(c,1,1)),merge(d),merge(e)]. given #874 (T,wt=14): 10528 p(j,b) | p(k,b) | p(f(k),g(j)) | p(m,m). [para(9139(c,1),7527(a,2)),merge(e),merge(f)]. given #875 (T,wt=16): 10550 p(j,b) | p(k,b) | j = b | p(f(k),k) | p(m,m). [para(7839(c,1),10528(c,2)),merge(d),merge(e)]. given #876 (T,wt=13): 10577 p(j,b) | p(k,b) | p(f(k),k) | p(m,m). [para(10550(c,1),7527(a,2)),merge(e),merge(f)]. given #877 (A,wt=41): 831 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(m) = b | -p(g(m),x) | f(g(m)) = b | f(g(m)) = g(m) | -p(f(g(m)),g(m)) | p(m,b). [resolve(67,h,371,b),flip(d),flip(f)]. given #878 (T,wt=17): 9140 p(j,b) | p(k,b) | j = b | p(f(g(j)),k) | p(m,m). [para(7839(c,1),8913(c,2)),merge(d),merge(e)]. given #879 (T,wt=14): 10634 p(j,b) | p(k,b) | p(f(g(j)),k) | p(m,m). [para(9140(c,1),7527(a,2)),merge(e),merge(f)]. given #880 (T,wt=17): 9206 p(j,b) | p(k,b) | j = b | p(k,f(g(j))) | p(m,j). [para(7839(c,1),9171(c,1)),merge(d),merge(e)]. given #881 (T,wt=14): 10682 p(j,b) | p(k,b) | p(k,f(g(j))) | p(m,j). [para(9206(c,1),7527(a,2)),merge(e),merge(f)]. given #882 (A,wt=42): 832 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | f(g(m)) = b | -p(f(g(m)),x) | g(m) = b | f(g(m)) = g(m) | -p(g(m),f(g(m))) | p(m,b). [resolve(67,h,361,b),flip(d),flip(f),flip(g)]. given #883 (T,wt=17): 9207 p(j,b) | p(k,b) | j = b | p(g(j),f(k)) | p(m,j). [para(7839(c,1),9171(c,2,1)),merge(d),merge(e)]. given #884 (T,wt=14): 10737 p(j,b) | p(k,b) | p(g(j),f(k)) | p(m,j). [para(9207(c,1),7527(a,2)),merge(e),merge(f)]. given #885 (T,wt=16): 10759 p(j,b) | p(k,b) | j = b | p(k,f(k)) | p(m,j). [para(7839(c,1),10737(c,1)),merge(d),merge(e)]. given #886 (T,wt=13): 10783 p(j,b) | p(k,b) | p(k,f(k)) | p(m,j). [para(10759(c,1),7527(a,2)),merge(e),merge(f)]. given #887 (A,wt=46): 835 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(g(m)) = b | -p(g(g(m)),x) | g(m) = b | g(g(m)) = g(m) | -p(g(m),g(g(m))) | p(g(m),b) | p(m,b). [resolve(67,h,174,b),flip(d),flip(f),flip(g)]. given #888 (T,wt=17): 9272 p(j,b) | p(k,b) | j = b | p(m,m) | p(k,f(g(j))). [para(7870(d,1),9256(c,1)),merge(d),merge(e)]. given #889 (T,wt=14): 10839 p(j,b) | p(k,b) | p(m,m) | p(k,f(g(j))). [para(9272(c,1),7527(a,2)),merge(e),merge(f)]. given #890 (T,wt=17): 9307 p(j,b) | p(k,b) | p(k,f(k)) | j = m | p(f(j),j). [resolve(9296,c,14,b),flip(d)]. given #891 (T,wt=17): 9308 p(j,b) | p(k,b) | p(k,f(k)) | j = m | p(j,f(j)). [resolve(9296,c,12,b),flip(d)]. given #892 (A,wt=45): 849 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(m) = b | -p(g(m),x) | g(g(m)) = b | g(g(m)) = g(m) | -p(g(g(m)),g(m)) | p(g(m),b) | p(m,b). [resolve(67,h,64,b),flip(d),flip(f)]. given #893 (T,wt=17): 9342 p(j,b) | p(k,b) | j = b | p(g(j),f(k)) | p(m,m). [para(7839(c,1),9177(c,2,1)),merge(d),merge(e)]. given #894 (T,wt=14): 10904 p(j,b) | p(k,b) | p(g(j),f(k)) | p(m,m). [para(9342(c,1),7527(a,2)),merge(e),merge(f)]. given #895 (T,wt=17): 9391 p(j,b) | p(k,b) | j = b | p(f(k),g(m)) | p(m,j). [para(7884(d,1),9367(c,1,1)),merge(d),merge(e)]. given #896 (T,wt=14): 10948 p(j,b) | p(k,b) | p(f(k),g(m)) | p(m,j). [para(9391(c,1),7527(a,2)),merge(e),merge(f)]. given #897 (A,wt=31): 850 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | -p(m,x) | g(m) = b | g(m) = m | -p(g(m),m) | p(m,b). [resolve(67,h,56,b),flip(d),flip(f),unit_del(d,27)]. given #898 (T,wt=17): 9392 p(j,b) | p(k,b) | j = b | p(f(g(m)),k) | p(m,j). [para(7884(d,1),9367(c,2)),merge(d),merge(e)]. given #899 (T,wt=14): 11001 p(j,b) | p(k,b) | p(f(g(m)),k) | p(m,j). [para(9392(c,1),7527(a,2)),merge(e),merge(f)]. given #900 (T,wt=17): 9533 p(j,b) | p(k,b) | j = b | p(f(k),g(m)) | p(m,m). [para(7884(d,1),9370(c,1,1)),merge(d),merge(e)]. given #901 (T,wt=14): 11045 p(j,b) | p(k,b) | p(f(k),g(m)) | p(m,m). [para(9533(c,1),7527(a,2)),merge(e),merge(f)]. given #902 (A,wt=42): 866 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | f(g(m)) = b | -p(f(g(m)),x) | g(m) = b | f(g(m)) = g(m) | -p(f(g(m)),g(m)) | p(m,b). [resolve(67,i,371,b),flip(d),flip(f),flip(g)]. given #903 (T,wt=17): 9534 p(j,b) | p(k,b) | j = b | p(f(g(m)),k) | p(m,m). [para(7884(d,1),9370(c,2)),merge(d),merge(e)]. given #904 (T,wt=14): 11101 p(j,b) | p(k,b) | p(f(g(m)),k) | p(m,m). [para(9534(c,1),7527(a,2)),merge(e),merge(f)]. given #905 (T,wt=17): 9590 p(j,b) | p(k,b) | j = b | p(k,f(g(m))) | p(m,j). [para(7884(d,1),9562(c,1)),merge(d),merge(e)]. given #906 (T,wt=14): 11145 p(j,b) | p(k,b) | p(k,f(g(m))) | p(m,j). [para(9590(c,1),7527(a,2)),merge(e),merge(f)]. given #907 (A,wt=46): 884 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(g(m)) = b | -p(g(g(m)),x) | g(m) = b | g(g(m)) = g(m) | -p(g(g(m)),g(m)) | p(g(m),b) | p(m,b). [resolve(67,i,64,b),flip(d),flip(f),flip(g)]. given #908 (T,wt=17): 9591 p(j,b) | p(k,b) | j = b | p(g(m),f(k)) | p(m,j). [para(7884(d,1),9562(c,2,1)),merge(d),merge(e)]. given #909 (T,wt=14): 11188 p(j,b) | p(k,b) | p(g(m),f(k)) | p(m,j). [para(9591(c,1),7527(a,2)),merge(e),merge(f)]. given #910 (T,wt=17): 9655 p(j,b) | p(k,b) | j = b | p(m,m) | p(k,f(g(m))). [para(7870(d,1),9636(c,1)),merge(d),merge(e)]. given #911 (T,wt=14): 11234 p(j,b) | p(k,b) | p(m,m) | p(k,f(g(m))). [para(9655(c,1),7527(a,2)),merge(e),merge(f)]. given #912 (A,wt=26): 1038 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(x,b) | p(x,g(x)) | j = x | p(x,j). [resolve(69,d,31,c)]. given #913 (T,wt=17): 9712 p(j,b) | p(k,b) | j = b | p(g(m),f(k)) | p(m,m). [para(7884(d,1),9565(c,2,1)),merge(d),merge(e)]. given #914 (T,wt=14): 11404 p(j,b) | p(k,b) | p(g(m),f(k)) | p(m,m). [para(9712(c,1),7527(a,2)),merge(e),merge(f)]. given #915 (T,wt=17): 9836 p(k,b) | p(g(k),k) | p(j,k) | p(m,m) | p(k,f(k)). [factor(9828,a,d)]. given #916 (T,wt=17): 10045 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(f(k),j). [para(8065(c,1),10028(d,2)),merge(d),merge(e)]. given #917 (A,wt=30): 1039 p(g(f(x)),b) | p(g(f(x)),g(g(f(x)))) | p(f(x),b) | p(x,b) | p(x,g(x)) | m = x | -p(x,m). [resolve(69,d,10,c)]. given #918 (T,wt=16): 11457 p(j,b) | p(k,b) | p(m,b) | p(f(k),j) | k != b. [para(10045(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #919 (T,wt=16): 11458 p(j,b) | p(k,b) | p(m,b) | p(f(k),j) | k != m. [para(10045(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #920 (T,wt=17): 10134 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(f(j),k). [para(8065(c,1),10117(d,1,1)),merge(d),merge(e)]. given #921 (T,wt=16): 11490 p(j,b) | p(k,b) | p(m,b) | p(f(j),k) | k != b. [para(10134(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #922 (A,wt=26): 1040 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(k,b) | p(k,g(k)) | j = x | p(x,j). [resolve(69,d,31,c(flip))]. given #923 (T,wt=16): 11491 p(j,b) | p(k,b) | p(m,b) | p(f(j),k) | k != m. [para(10134(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #924 (T,wt=17): 10216 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(j,f(k)). [para(8065(c,1),10194(d,1)),merge(d),merge(e)]. given #925 (T,wt=16): 11527 p(j,b) | p(k,b) | p(m,b) | p(j,f(k)) | k != b. [para(10216(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #926 (T,wt=16): 11528 p(j,b) | p(k,b) | p(m,b) | p(j,f(k)) | k != m. [para(10216(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #927 (A,wt=29): 1041 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(f(x),b) | p(f(x),g(f(x))) | m = x | -p(x,m). [resolve(69,d,10,c(flip))]. given #928 (T,wt=17): 10257 p(k,b) | p(g(k),k) | p(j,k) | p(m,b) | p(k,f(k)). [factor(10249,a,d)]. given #929 (T,wt=17): 10363 p(j,b) | p(k,b) | g(j) = k | p(f(k),j) | p(m,j). [para(7760(c,1),10342(c,2)),merge(d),merge(e)]. given #930 (T,wt=17): 10463 p(j,b) | p(k,b) | g(j) = k | p(f(j),k) | p(m,j). [para(7760(c,1),10444(c,1,1)),merge(d),merge(e)]. given #931 (T,wt=17): 10549 p(j,b) | p(k,b) | g(j) = k | p(f(k),j) | p(m,m). [para(7760(c,1),10528(c,2)),merge(d),merge(e)]. given #932 (A,wt=21): 1042 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | g(k) = j | p(g(k),j). [factor(1038,a,d),flip(e),merge(d)]. given #933 (T,wt=17): 10653 p(j,b) | p(k,b) | g(j) = k | p(f(j),k) | p(m,m). [para(7760(c,1),10634(c,1,1)),merge(d),merge(e)]. given #934 (T,wt=17): 10758 p(j,b) | p(k,b) | g(j) = k | p(j,f(k)) | p(m,j). [para(7760(c,1),10737(c,1)),merge(d),merge(e)]. given #935 (T,wt=17): 10801 p(k,b) | p(g(k),k) | p(j,k) | p(k,f(k)) | p(m,j). [factor(10793,a,d)]. given #936 (T,wt=17): 10925 p(j,b) | p(k,b) | g(j) = k | p(j,f(k)) | p(m,m). [para(7760(c,1),10904(c,1)),merge(d),merge(e)]. given #937 (A,wt=21): 1066 p(x,b) | p(x,g(x)) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(x),m). [para(20(a,1),96(c,1,1))]. given #938 (T,wt=17): 10967 p(j,b) | p(k,b) | g(m) = k | p(f(k),j) | p(m,j). [para(8065(c,1),10948(c,2)),merge(d),merge(e)]. given #939 (T,wt=17): 11018 p(j,b) | p(k,b) | g(m) = k | p(f(j),k) | p(m,j). [para(8065(c,1),11001(c,1,1)),merge(d),merge(e)]. given #940 (T,wt=17): 11064 p(j,b) | p(k,b) | g(m) = k | p(f(k),j) | p(m,m). [para(8065(c,1),11045(c,2)),merge(d),merge(e)]. given #941 (T,wt=17): 11118 p(j,b) | p(k,b) | g(m) = k | p(f(j),k) | p(m,m). [para(8065(c,1),11101(c,1,1)),merge(d),merge(e)]. given #942 (A,wt=21): 1067 p(x,b) | p(g(x),x) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(x),m). [para(22(a,1),96(c,1,1))]. given #943 (T,wt=17): 11207 p(j,b) | p(k,b) | g(m) = k | p(j,f(k)) | p(m,j). [para(8065(c,1),11188(c,1)),merge(d),merge(e)]. given #944 (T,wt=17): 11423 p(j,b) | p(k,b) | g(m) = k | p(j,f(k)) | p(m,m). [para(8065(c,1),11404(c,1)),merge(d),merge(e)]. given #945 (T,wt=18): 5187 p(m,k) | j = b | b = x | j = x | -p(j,x) | -p(x,j). [resolve(5182,b,4,b),flip(b),flip(d)]. given #946 (T,wt=12): 11613 p(m,k) | j = b | j = m | -p(j,m). [resolve(5187,f,6760,b),flip(c),merge(f),unit_del(c,27)]. given #947 (A,wt=27): 1068 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(x),m). [para(32(c,1),96(c,1,1))]. given #948 (T,wt=18): 5236 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(f(f(b))))),m). [factor(5230,a,c),merge(c)]. given #949 (T,wt=18): 5243 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(f(f(b))))),m). [factor(5238,a,c),merge(c)]. given #950 (T,wt=18): 5985 p(m,k) | k = b | b = x | k = x | -p(m,x) | -p(x,k). [para(49(a,1),2022(e,1)),merge(b)]. given #951 (T,wt=18): 5986 p(m,k) | k = b | b = x | k = x | -p(k,x) | -p(x,m). [para(49(a,1),2022(f,2)),merge(b)]. given #952 (A,wt=27): 1069 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(x),m). [para(37(c,1),96(c,1,1))]. given #953 (T,wt=18): 6046 p(b,m) | k = b | -p(k,b) | j = b | j = k | p(j,b). [resolve(3460,f,5560,b),merge(g)]. given #954 (T,wt=18): 6049 p(b,m) | j = m | p(j,m) | k = m | j = k | p(j,b). [resolve(3461,f,5560,b),merge(g)]. given #955 (T,wt=18): 6053 p(b,m) | k = m | p(k,m) | j = m | j = k | p(j,b). [resolve(3462,f,5560,b),merge(g)]. given #956 (T,wt=18): 6780 p(b,b) | j = b | -p(j,b) | k = b | j = k | -p(j,k). [resolve(6758,a,4,f),flip(b),flip(d),flip(e)]. given #957 (A,wt=34): 1070 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(x),m). [para(65(d,1),96(c,1,1))]. given #958 (T,wt=18): 6781 p(b,b) | k = b | -p(k,b) | j = b | j = k | -p(j,k). [resolve(6758,a,4,e),flip(b),flip(d)]. given #959 (T,wt=18): 6782 p(b,b) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(6758,a,2,f),flip(b),flip(d),flip(e)]. given #960 (T,wt=18): 6783 p(b,b) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(6758,a,2,e),flip(b),flip(d)]. given #961 (T,wt=18): 6828 p(k,b) | p(k,k) | g(k) = k | g(k) = m | g(k) = b. [resolve(6727,b,6,d),flip(c),flip(d),flip(e)]. given #962 (A,wt=21): 1072 p(x,b) | p(x,g(x)) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(x),m). [para(20(a,1),223(c,1,1))]. given #963 (T,wt=14): 11701 p(k,b) | p(k,k) | g(k) = m | g(k) = b. [para(6828(c,1),6726(b,2)),merge(e),merge(f),merge(g)]. given #964 (T,wt=13): 11703 p(k,b) | p(k,k) | g(k) = b | p(k,m). [para(11701(c,1),6726(b,2)),merge(d),merge(f)]. given #965 (T,wt=9): 11720 p(k,b) | p(k,k) | p(k,m). [para(11703(c,1),6726(b,2)),merge(d),merge(e),merge(f)]. given #966 (T,wt=16): 11702 p(k,b) | p(k,k) | g(k) = b | k = b | k != m. [para(11701(c,1),18(c,1)),flip(d),flip(f),merge(e)]. given #967 (A,wt=21): 1073 p(x,b) | p(g(x),x) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(x),m). [para(22(a,1),223(c,1,1))]. given #968 (T,wt=18): 7434 p(j,b) | p(m,b) | k = m | p(k,m) | j = m | j = k. [resolve(7428,b,2992,f),merge(c)]. given #969 (T,wt=18): 7435 p(j,b) | p(m,b) | j = m | p(j,m) | k = m | j = k. [resolve(7428,b,2991,f),merge(c)]. given #970 (T,wt=18): 7436 p(j,b) | p(m,b) | k = b | -p(k,b) | j = b | j = k. [resolve(7428,b,2990,f),merge(c)]. given #971 (T,wt=18): 7513 p(j,b) | k = b | -p(k,b) | j = b | j = k | -p(k,j). [resolve(7499,b,4,f),flip(b),flip(d)]. given #972 (A,wt=27): 1074 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(x),m). [para(32(c,1),223(c,1,1))]. given #973 (T,wt=18): 7514 p(j,b) | k = m | p(k,m) | j = m | j = k | -p(k,j). [resolve(7499,b,2,f),flip(b),flip(d)]. given #974 (T,wt=18): 7515 p(j,b) | j = m | p(j,m) | k = m | j = k | -p(k,j). [resolve(7499,b,2,e),flip(b),flip(d),flip(e)]. given #975 (T,wt=18): 7545 p(k,b) | j = b | -p(j,b) | k = b | j = k | -p(j,k). [resolve(7527,a,4,f),flip(b),flip(d),flip(e)]. given #976 (T,wt=18): 7546 p(k,b) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(7527,a,2,f),flip(b),flip(d),flip(e)]. given #977 (A,wt=27): 1075 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(x),m). [para(37(c,1),223(c,1,1))]. given #978 (T,wt=18): 7547 p(k,b) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(7527,a,2,e),flip(b),flip(d)]. given #979 (T,wt=18): 7618 p(b,j) | p(k,b) | g(k) = k | g(k) = m | g(k) = b. [resolve(7548,c,6,d),flip(c),flip(d),flip(e)]. given #980 (T,wt=17): 11798 p(b,j) | p(k,b) | g(k) = m | g(k) = b | k = b. [resolve(7618,c,18,c),flip(e),merge(f)]. given #981 (T,wt=16): 11805 p(b,j) | p(k,b) | g(k) = b | k = b | k != m. [para(11798(c,1),18(c,1)),flip(e),flip(g),merge(e),merge(f)]. given #982 (A,wt=34): 1076 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(x),m). [para(65(d,1),223(c,1,1))]. given #983 (T,wt=16): 11806 p(b,j) | p(k,b) | g(k) = b | k = b | p(k,m). [para(11798(c,1),7549(c,2)),merge(e),merge(f)]. given #984 (T,wt=12): 11816 p(b,j) | p(k,b) | k = b | p(k,m). [resolve(11806,c,16,c),flip(e),merge(e),merge(f)]. given #985 (T,wt=9): 11829 p(b,j) | p(k,b) | p(k,m). [para(11816(c,1),7527(a,1)),merge(d),merge(e)]. given #986 (T,wt=13): 11841 p(b,j) | p(k,b) | k = m | p(f(k),k). [resolve(11829,c,14,b),flip(c)]. given #987 (A,wt=26): 1087 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(x,b) | p(g(x),x) | j = x | p(x,j). [resolve(71,d,31,c)]. given #988 (T,wt=13): 11842 p(b,j) | p(k,b) | k = m | p(k,f(k)). [resolve(11829,c,12,b),flip(c)]. given #989 (T,wt=13): 11857 p(b,j) | p(k,b) | p(f(k),k) | p(b,m). [para(11841(c,1),6716(a,2))]. given #990 (T,wt=13): 11859 p(b,j) | p(k,b) | p(f(k),k) | p(m,j). [para(11841(c,1),7527(a,1)),merge(e)]. given #991 (T,wt=13): 11876 p(b,j) | p(k,b) | p(f(k),k) | p(m,m). [para(11841(c,1),11829(c,1)),merge(d),merge(e)]. given #992 (A,wt=30): 1088 p(g(f(x)),b) | p(g(f(x)),g(g(f(x)))) | p(f(x),b) | p(x,b) | p(g(x),x) | m = x | -p(x,m). [resolve(71,d,10,c)]. given #993 (T,wt=13): 11975 p(b,j) | p(k,b) | p(k,f(k)) | p(b,m). [para(11842(c,1),6716(a,2))]. given #994 (T,wt=13): 11977 p(b,j) | p(k,b) | p(k,f(k)) | p(m,j). [para(11842(c,1),7527(a,1)),merge(e)]. given #995 (T,wt=13): 11994 p(b,j) | p(k,b) | p(k,f(k)) | p(m,m). [para(11842(c,1),11829(c,1)),merge(d),merge(e)]. given #996 (T,wt=14): 11860 p(b,j) | p(k,b) | p(f(k),k) | p(g(m),k). [para(11841(c,1),7548(c,1,1)),merge(d),merge(e)]. given #997 (A,wt=26): 1089 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(k,b) | p(g(k),k) | j = x | p(x,j). [resolve(71,d,31,c(flip))]. given #998 (T,wt=14): 11861 p(b,j) | p(k,b) | p(f(k),k) | p(g(k),m). [para(11841(c,1),7548(c,2)),merge(d),merge(e)]. given #999 (T,wt=14): 11862 p(b,j) | p(k,b) | p(f(k),k) | p(m,g(k)). [para(11841(c,1),7549(c,1)),merge(d),merge(e)]. given #1000 (T,wt=14): 11863 p(b,j) | p(k,b) | p(f(k),k) | p(k,g(m)). [para(11841(c,1),7549(c,2,1)),merge(d),merge(e)]. given #1001 (T,wt=14): 11978 p(b,j) | p(k,b) | p(k,f(k)) | p(g(m),k). [para(11842(c,1),7548(c,1,1)),merge(d),merge(e)]. given #1002 (A,wt=29): 1090 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(f(x),b) | p(g(f(x)),f(x)) | m = x | -p(x,m). [resolve(71,d,10,c(flip))]. given #1003 (T,wt=14): 11979 p(b,j) | p(k,b) | p(k,f(k)) | p(g(k),m). [para(11842(c,1),7548(c,2)),merge(d),merge(e)]. given #1004 (T,wt=14): 11980 p(b,j) | p(k,b) | p(k,f(k)) | p(m,g(k)). [para(11842(c,1),7549(c,1)),merge(d),merge(e)]. given #1005 (T,wt=14): 11981 p(b,j) | p(k,b) | p(k,f(k)) | p(k,g(m)). [para(11842(c,1),7549(c,2,1)),merge(d),merge(e)]. given #1006 (T,wt=14): 12118 p(b,j) | p(k,b) | p(f(k),k) | p(g(m),m). [para(11841(c,1),11860(d,2)),merge(d),merge(e),merge(f)]. given #1007 (A,wt=22): 1102 p(x,b) | p(x,g(x)) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(x)),m). [para(20(a,1),1071(c,1,1,1))]. given #1008 (T,wt=14): 12214 p(b,j) | p(k,b) | p(k,f(k)) | p(g(m),m). [para(11842(c,1),11978(d,2)),merge(d),merge(e),merge(f)]. given #1009 (T,wt=14): 12270 p(b,j) | p(k,b) | p(k,f(k)) | p(m,g(m)). [para(11842(c,1),11981(d,1)),merge(d),merge(e),merge(f)]. given #1010 (T,wt=16): 11845 p(b,j) | p(k,b) | p(f(k),k) | p(j,b) | j = b. [resolve(11841,c,7885,d),merge(e)]. given #1011 (T,wt=13): 12382 p(b,j) | p(k,b) | p(f(k),k) | p(j,b). [para(11845(e,1),7527(a,2)),merge(e),merge(f)]. given #1012 (A,wt=22): 1103 p(x,b) | p(g(x),x) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(x)),m). [para(22(a,1),1071(c,1,1,1))]. given #1013 (T,wt=16): 11963 p(b,j) | p(k,b) | p(k,f(k)) | p(j,b) | j = b. [resolve(11842,c,7885,d),merge(e)]. given #1014 (T,wt=13): 12417 p(b,j) | p(k,b) | p(k,f(k)) | p(j,b). [para(11963(e,1),7527(a,2)),merge(e),merge(f)]. given #1015 (T,wt=17): 11844 p(b,j) | p(k,b) | p(f(k),k) | g(k) = b | k = b. [resolve(11841,c,11805,e),merge(d),merge(e)]. given #1016 (T,wt=13): 12438 p(b,j) | p(k,b) | p(f(k),k) | k = b. [resolve(11844,d,16,c),flip(e),merge(e),merge(f)]. given #1017 (A,wt=28): 1104 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(x)),m). [para(32(c,1),1071(c,1,1,1))]. given #1018 (T,wt=10): 12450 p(b,j) | p(k,b) | p(f(k),k). [para(12438(d,1),7527(a,1)),merge(d),merge(e)]. given #1019 (T,wt=14): 12464 p(b,j) | p(k,b) | p(k,f(k)) | p(f(m),k). [para(11842(c,1),12450(c,1,1)),merge(d),merge(e)]. given #1020 (T,wt=14): 12465 p(b,j) | p(k,b) | p(k,f(k)) | p(f(k),m). [para(11842(c,1),12450(c,2)),merge(d),merge(e)]. given #1021 (T,wt=14): 12483 p(b,j) | p(k,b) | p(k,f(k)) | p(f(m),m). [para(11842(c,1),12464(d,2)),merge(d),merge(e),merge(f)]. given #1022 (A,wt=28): 1105 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(x)),m). [para(37(c,1),1071(c,1,1,1))]. given #1023 (T,wt=17): 11962 p(b,j) | p(k,b) | p(k,f(k)) | g(k) = b | k = b. [resolve(11842,c,11805,e),merge(d),merge(e)]. given #1024 (T,wt=13): 12578 p(b,j) | p(k,b) | p(k,f(k)) | k = b. [resolve(11962,d,16,c),flip(e),merge(e),merge(f)]. given #1025 (T,wt=10): 12590 p(b,j) | p(k,b) | p(k,f(k)). [para(12578(d,1),7527(a,1)),merge(d),merge(e)]. given #1026 (T,wt=18): 7640 p(j,b) | j = m | j = b | j = x | -p(x,k) | k = x. [para(7512(b,1),29(b,2))]. given #1027 (A,wt=35): 1106 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(x)),m). [para(65(d,1),1071(c,1,1,1))]. given #1028 (T,wt=18): 7650 p(j,b) | j = b | p(k,k) | j = x | -p(x,m) | k = x. [para(7643(b,1),29(b,2))]. given #1029 (T,wt=18): 7660 p(j,b) | j = b | k = b | j = x | -p(x,m) | k = x. [para(7645(b,1),29(b,2))]. given #1030 (T,wt=18): 7875 p(j,b) | p(k,b) | j = b | j = x | -p(x,m) | k = x. [para(7870(d,1),29(b,2))]. given #1031 (T,wt=18): 7911 p(k,b) | p(k,m) | p(b,m) | j = m | j = b | -p(b,j). [resolve(7896,a,2,f),flip(e),unit_del(c,27)]. given #1032 (A,wt=22): 1108 p(x,b) | p(x,g(x)) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(x)),m). [para(20(a,1),1077(c,1,1,1))]. given #1033 (T,wt=18): 7912 p(k,b) | p(k,m) | j = m | p(j,m) | j = b | -p(b,j). [resolve(7896,a,2,e),flip(c),flip(f),unit_del(e,27)]. given #1034 (T,wt=18): 7971 p(j,b) | p(k,b) | g(k) = k | g(k) = m | g(k) = b. [resolve(7943,c,6,d),flip(c),flip(d),flip(e)]. given #1035 (T,wt=17): 12638 p(j,b) | p(k,b) | g(k) = m | g(k) = b | k = b. [resolve(7971,c,18,c),flip(e),merge(f)]. given #1036 (T,wt=16): 12644 p(j,b) | p(k,b) | g(k) = b | k = b | k != m. [para(12638(c,1),18(c,1)),flip(e),flip(g),merge(e),merge(f)]. given #1037 (A,wt=22): 1109 p(x,b) | p(g(x),x) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(x)),m). [para(22(a,1),1077(c,1,1,1))]. given #1038 (T,wt=18): 8488 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(f(j),g(m)). [para(8065(c,1),361(b,1,1))]. given #1039 (T,wt=17): 12648 p(j,b) | p(k,b) | p(m,b) | p(f(j),g(m)) | k != b. [para(8488(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1040 (T,wt=17): 12649 p(j,b) | p(k,b) | p(m,b) | p(f(j),g(m)) | k != m. [para(8488(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1041 (T,wt=18): 8489 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(f(g(m)),j). [para(8065(c,1),361(b,2))]. given #1042 (A,wt=28): 1110 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(x)),m). [para(32(c,1),1077(c,1,1,1))]. given #1043 (T,wt=17): 12679 p(j,b) | p(k,b) | p(m,b) | p(f(g(m)),j) | k != b. [para(8489(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1044 (T,wt=17): 12680 p(j,b) | p(k,b) | p(m,b) | p(f(g(m)),j) | k != m. [para(8489(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1045 (T,wt=18): 8490 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(j,f(g(m))). [para(8065(c,1),371(b,1))]. given #1046 (T,wt=17): 12710 p(j,b) | p(k,b) | p(m,b) | p(j,f(g(m))) | k != b. [para(8490(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1047 (A,wt=28): 1111 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(x)),m). [para(37(c,1),1077(c,1,1,1))]. given #1048 (T,wt=17): 12711 p(j,b) | p(k,b) | p(m,b) | p(j,f(g(m))) | k != m. [para(8490(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1049 (T,wt=18): 8491 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(g(m),f(j)). [para(8065(c,1),371(b,2,1))]. given #1050 (T,wt=17): 12741 p(j,b) | p(k,b) | p(m,b) | p(g(m),f(j)) | k != b. [para(8491(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1051 (T,wt=17): 12742 p(j,b) | p(k,b) | p(m,b) | p(g(m),f(j)) | k != m. [para(8491(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1052 (A,wt=35): 1112 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(x)),m). [para(65(d,1),1077(c,1,1,1))]. given #1053 (T,wt=18): 8685 p(j,b) | k = m | p(b,m) | p(k,m) | j = m | -p(m,b). [factor(8679,b,g)]. given #1054 (T,wt=18): 8904 p(j,b) | p(k,b) | p(f(g(j)),g(j)) | j = b | j != m. [para(8107(c,1),18(c,1)),flip(d),flip(f),merge(e)]. given #1055 (T,wt=15): 12778 p(j,b) | p(k,b) | p(f(g(j)),g(j)) | j = b. [resolve(8904,e,7870,d),merge(e),merge(f),merge(g)]. given #1056 (T,wt=12): 12790 p(j,b) | p(k,b) | p(f(g(j)),g(j)). [para(12778(d,1),7527(a,2)),merge(d),merge(e)]. given #1057 (A,wt=32): 1206 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | j = x | p(x,j). [resolve(75,f,31,c)]. given #1058 (T,wt=14): 12819 p(j,b) | p(k,b) | j = b | p(f(k),g(j)). [para(7839(c,1),12790(c,1,1)),merge(d),merge(e)]. given #1059 (T,wt=11): 12931 p(j,b) | p(k,b) | p(f(k),g(j)). [para(12819(c,1),7527(a,2)),merge(d),merge(e)]. given #1060 (T,wt=13): 12955 p(j,b) | p(k,b) | j = b | p(f(k),k). [para(7839(c,1),12931(c,2)),merge(d),merge(e)]. given #1061 (T,wt=10): 12991 p(j,b) | p(k,b) | p(f(k),k). [para(12955(c,1),7527(a,2)),merge(d),merge(e)]. given #1062 (A,wt=36): 1207 p(g(f(x)),b) | p(g(f(x)),g(g(f(x)))) | p(f(x),b) | p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | m = x | -p(x,m). [resolve(75,f,10,c)]. given #1063 (T,wt=14): 12820 p(j,b) | p(k,b) | j = b | p(f(g(j)),k). [para(7839(c,1),12790(c,2)),merge(d),merge(e)]. given #1064 (T,wt=11): 13041 p(j,b) | p(k,b) | p(f(g(j)),k). [para(12820(c,1),7527(a,2)),merge(d),merge(e)]. given #1065 (T,wt=14): 12954 p(j,b) | p(k,b) | g(j) = k | p(f(k),j). [para(7760(c,1),12931(c,2)),merge(d),merge(e)]. given #1066 (T,wt=14): 12956 p(j,b) | p(k,b) | j = b | p(f(k),g(m)). [para(7870(d,1),12931(c,2,1)),merge(d),merge(e)]. given #1067 (A,wt=38): 1283 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = b | p(g(g(g(x))),b) | p(g(g(g(x))),g(g(g(g(x))))) | p(g(g(x)),b). [resolve(76,e,75,f),merge(h),merge(i),merge(j)]. given #1068 (T,wt=11): 13105 p(j,b) | p(k,b) | p(f(k),g(m)). [para(12956(c,1),7527(a,2)),merge(d),merge(e)]. given #1069 (T,wt=14): 13062 p(j,b) | p(k,b) | g(j) = k | p(f(j),k). [para(7760(c,1),13041(c,1,1)),merge(d),merge(e)]. given #1070 (T,wt=14): 13063 p(j,b) | p(k,b) | j = b | p(f(g(m)),k). [para(7870(d,1),13041(c,1,1,1)),merge(d),merge(e)]. given #1071 (T,wt=11): 13170 p(j,b) | p(k,b) | p(f(g(m)),k). [para(13063(c,1),7527(a,2)),merge(d),merge(e)]. given #1072 (A,wt=30): 1284 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = b | p(g(g(x)),b) | p(g(g(g(x))),g(g(x))). [resolve(76,e,72,e),merge(g),merge(h),merge(i)]. given #1073 (T,wt=14): 13135 p(j,b) | p(k,b) | g(m) = k | p(f(k),j). [para(8065(c,1),13105(c,2)),merge(d),merge(e)]. given #1074 (T,wt=14): 13187 p(j,b) | p(k,b) | g(m) = k | p(f(j),k). [para(8065(c,1),13170(c,1,1)),merge(d),merge(e)]. given #1075 (T,wt=15): 12817 p(j,b) | p(k,b) | g(j) = k | p(f(j),g(j)). [para(7760(c,1),12790(c,1,1)),merge(d),merge(e)]. given #1076 (T,wt=15): 12818 p(j,b) | p(k,b) | g(j) = k | p(f(g(j)),j). [para(7760(c,1),12790(c,2)),merge(d),merge(e)]. given #1077 (A,wt=21): 1327 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = b | g(x) != x. [para(77(d,1),76(e,1,1)),merge(d),merge(e),merge(f)]. given #1078 (T,wt=15): 12821 p(j,b) | p(k,b) | j = b | p(f(g(m)),g(j)). [para(7870(d,1),12790(c,1,1,1)),merge(d),merge(e)]. given #1079 (T,wt=12): 13249 p(j,b) | p(k,b) | p(f(g(m)),g(j)). [para(12821(c,1),7527(a,2)),merge(d),merge(e)]. given #1080 (T,wt=15): 12822 p(j,b) | p(k,b) | j = b | p(f(g(j)),g(m)). [para(7870(d,1),12790(c,2,1)),merge(d),merge(e)]. given #1081 (T,wt=12): 13312 p(j,b) | p(k,b) | p(f(g(j)),g(m)). [para(12822(c,1),7527(a,2)),merge(d),merge(e)]. given #1082 (A,wt=23): 1652 p(x,b) | p(x,g(x)) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(x))),m). [para(20(a,1),1107(c,1,1,1,1))]. given #1083 (T,wt=15): 13272 p(j,b) | p(k,b) | g(j) = k | p(f(g(m)),j). [para(7760(c,1),13249(c,2)),merge(d),merge(e)]. given #1084 (T,wt=15): 13273 p(j,b) | p(k,b) | j = b | p(f(g(m)),g(m)). [para(7870(d,1),13249(c,2,1)),merge(d),merge(e)]. given #1085 (T,wt=12): 13381 p(j,b) | p(k,b) | p(f(g(m)),g(m)). [para(13273(c,1),7527(a,2)),merge(d),merge(e)]. given #1086 (T,wt=15): 13274 p(j,b) | p(k,b) | g(m) = k | p(f(j),g(j)). [para(8065(c,1),13249(c,1,1)),merge(d),merge(e)]. given #1087 (A,wt=23): 1653 p(x,b) | p(g(x),x) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(x))),m). [para(22(a,1),1107(c,1,1,1,1))]. given #1088 (T,wt=15): 13336 p(j,b) | p(k,b) | g(j) = k | p(f(j),g(m)). [para(7760(c,1),13312(c,1,1)),merge(d),merge(e)]. given #1089 (T,wt=15): 13337 p(j,b) | p(k,b) | g(m) = k | p(f(g(j)),j). [para(8065(c,1),13312(c,2)),merge(d),merge(e)]. given #1090 (T,wt=15): 13400 p(j,b) | p(k,b) | g(m) = k | p(f(j),g(m)). [para(8065(c,1),13381(c,1,1)),merge(d),merge(e)]. given #1091 (T,wt=15): 13401 p(j,b) | p(k,b) | g(m) = k | p(f(g(m)),j). [para(8065(c,1),13381(c,2)),merge(d),merge(e)]. given #1092 (A,wt=29): 1654 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(x))),m). [para(32(c,1),1107(c,1,1,1,1))]. given #1093 (T,wt=16): 12958 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(k),m). [para(8108(c,1),12931(c,2)),merge(d),merge(e)]. given #1094 (T,wt=16): 13064 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(m),k). [para(8108(c,1),13041(c,1,1)),merge(d),merge(e)]. given #1095 (T,wt=16): 13137 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(f(k),m). [para(8329(c,1),13105(c,2)),merge(d),merge(e)]. given #1096 (T,wt=16): 13189 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(f(m),k). [para(8329(c,1),13170(c,1,1)),merge(d),merge(e)]. given #1097 (A,wt=29): 1655 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(x))),m). [para(37(c,1),1107(c,1,1,1,1))]. given #1098 (T,wt=17): 12825 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(m),g(j)). [para(8108(c,1),12790(c,1,1)),merge(d),merge(e)]. given #1099 (T,wt=17): 12826 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(g(j)),m). [para(8108(c,1),12790(c,2)),merge(d),merge(e)]. given #1100 (T,wt=16): 13832 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(m),m). [para(8108(c,1),12826(d,1,1)),merge(d),merge(e),merge(f)]. given #1101 (T,wt=17): 13237 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = b. [resolve(1327,e,77,d),merge(e),merge(f),merge(g)]. given #1102 (A,wt=36): 1656 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(x))),m). [para(65(d,1),1107(c,1,1,1,1))]. given #1103 (T,wt=16): 13921 p(g(j),b) | p(g(j),g(g(j))) | p(j,b) | p(k,b). [para(13237(d,1),7801(b,2)),merge(d),merge(e)]. given #1104 (T,wt=16): 13922 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(k,m). [para(13237(d,1),8854(b,2)),merge(d),merge(e)]. given #1105 (T,wt=16): 13923 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(m,b). [para(13237(d,1),8880(b,2)),merge(d),merge(e)]. given #1106 (T,wt=17): 13275 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(g(m)),m). [para(8108(c,1),13249(c,2)),merge(d),merge(e)]. given #1107 (A,wt=23): 1658 p(x,b) | p(x,g(x)) | p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(x))),m). [para(20(a,1),1113(c,1,1,1,1))]. given #1108 (T,wt=17): 13277 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(f(m),g(j)). [para(8329(c,1),13249(c,1,1)),merge(d),merge(e)]. given #1109 (T,wt=17): 13338 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(m),g(m)). [para(8108(c,1),13312(c,1,1)),merge(d),merge(e)]. given #1110 (T,wt=17): 13340 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(f(g(j))