============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11482 was started by mccune on cleo.thornwood, Sat Aug 12 21:02:06 2006 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 (F,wt=6): 49 k = m | p(m,k). [xx_res(24,b)]. given #18 (F,wt=6): 52 k = b | p(b,k). [xx_res(26,b)]. given #19 (T,wt=6): 61 j = k | p(k,j). [xx_res(31,c)]. given #20 (T,wt=6): 70 p(b,k) | p(m,k). [para(52(a,1),49(a,1)),flip(b),unit_del(b,27)]. given #21 (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 #22 (F,wt=6): 74 p(b,k) | p(m,b). [para(52(a,1),70(b,2)),merge(b)]. given #23 (F,wt=7): 55 p(m,b) | p(g(m),m). [resolve(27,a,22,a(flip))]. given #24 (T,wt=7): 56 p(m,b) | p(m,g(m)). [resolve(27,a,20,a(flip))]. given #25 (T,wt=9): 62 p(m,k) | j = m | p(m,j). [resolve(49,a,31,c)]. given #26 (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 #27 (F,wt=9): 65 p(b,k) | j = b | p(b,j). [resolve(52,a,31,c)]. given #28 (F,wt=9): 72 p(m,k) | j = m | p(k,j). [para(49(a,1),61(a,2))]. given #29 (T,wt=9): 73 p(b,k) | j = b | p(k,j). [para(52(a,1),61(a,2))]. given #30 (T,wt=10): 57 p(x,b) | p(x,g(x)) | m != x. [para(20(a,1),27(a,2))]. given #31 (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 #32 (F,wt=10): 58 p(x,b) | p(g(x),x) | m != x. [para(22(a,1),27(a,2))]. given #33 (F,wt=10): 119 p(k,b) | p(k,g(k)) | p(m,k). [resolve(57,c,49,a(flip))]. given #34 (T,wt=10): 126 p(k,b) | p(g(k),k) | p(m,k). [resolve(58,c,49,a(flip))]. given #35 (T,wt=10): 131 p(m,k) | p(k,b) | p(m,g(k)). [para(49(a,1),119(b,1)),merge(d)]. given #36 (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 #37 (F,wt=10): 132 p(m,k) | p(k,b) | p(k,g(m)). [para(49(a,1),119(b,2,1)),merge(d)]. given #38 (F,wt=10): 137 p(m,k) | p(k,b) | p(g(m),k). [para(49(a,1),126(b,1,1)),merge(d)]. given #39 (T,wt=10): 138 p(m,k) | p(k,b) | p(g(k),m). [para(49(a,1),126(b,2)),merge(d)]. given #40 (T,wt=10): 143 p(m,k) | p(m,b) | p(m,g(k)). [para(49(a,1),131(b,1)),merge(b)]. given #41 (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 #42 (F,wt=10): 149 p(m,k) | p(k,b) | p(m,g(m)). [para(49(a,1),132(c,1)),merge(b)]. given #43 (F,wt=10): 154 p(m,k) | p(k,b) | p(g(m),m). [para(49(a,1),137(c,2)),merge(b)]. given #44 (T,wt=12): 64 p(m,k) | j = x | p(x,j) | m != x. [para(49(a,1),31(c,1))]. given #45 (T,wt=12): 69 p(b,k) | j = x | p(x,j) | b != x. [para(52(a,1),31(c,1))]. given #46 (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 #47 (F,wt=12): 71 p(k,j) | j = x | -p(x,k) | k = x. [para(61(a,1),29(b,2))]. given #48 (F,wt=12): 101 p(m,k) | p(m,j) | j = k | p(j,k). [resolve(62,b,24,b(flip)),flip(c)]. given #49 (T,wt=12): 107 p(b,k) | p(b,j) | j = k | p(j,k). [resolve(65,b,26,b(flip)),flip(c)]. given #50 (T,wt=12): 222 p(k,j) | j = m | k = m | p(b,k). [resolve(71,c,70,b)]. given #51 (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 #52 (F,wt=9): 228 p(k,j) | k = m | p(b,k). [para(222(b,1),61(a,1)),flip(d),merge(d),merge(e)]. given #53 (F,wt=6): 239 p(k,j) | p(b,k). [para(228(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #54 (T,wt=6): 242 p(b,k) | p(b,j). [para(52(a,1),239(a,1)),merge(c)]. given #55 (T,wt=13): 50 k = x | p(x,k) | p(x,b) | p(g(x),x). [resolve(26,b,22,a)]. given #56 (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 #57 (F,wt=13): 51 k = x | p(x,k) | p(x,b) | p(x,g(x)). [resolve(26,b,20,a)]. given #58 (F,wt=13): 59 j = b | p(b,j) | p(k,b) | p(g(k),k). [resolve(31,c,22,a(flip))]. given #59 (T,wt=13): 60 j = b | p(b,j) | p(k,b) | p(k,g(k)). [resolve(31,c,20,a(flip))]. given #60 (T,wt=13): 67 p(x,b) | p(x,g(x)) | k = x | p(b,k). [para(20(a,1),52(a,2))]. given #61 (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 #62 (F,wt=13): 68 p(x,b) | p(g(x),x) | k = x | p(b,k). [para(22(a,1),52(a,2))]. given #63 (F,wt=13): 77 p(g(m),b) | p(g(m),g(g(m))) | p(m,b). [resolve(32,c,27,a(flip))]. given #64 (T,wt=13): 94 p(x,b) | p(x,g(x)) | p(b,k) | p(m,x). [para(20(a,1),74(b,2))]. given #65 (T,wt=13): 95 p(x,b) | p(g(x),x) | p(b,k) | p(m,x). [para(22(a,1),74(b,2))]. given #66 (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 #67 (F,wt=13): 97 p(m,b) | g(m) = m | p(f(g(m)),g(m)). [resolve(55,b,14,b),flip(b)]. given #68 (F,wt=9): 362 p(m,b) | p(f(g(m)),g(m)). [resolve(97,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #69 (T,wt=13): 98 p(m,b) | g(m) = m | p(g(m),f(g(m))). [resolve(55,b,12,b),flip(b)]. given #70 (T,wt=9): 372 p(m,b) | p(g(m),f(g(m))). [resolve(98,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #71 (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 #72 (F,wt=13): 117 p(j,b) | p(j,g(j)) | p(m,k) | p(k,j). [resolve(57,c,72,b(flip))]. given #73 (F,wt=13): 118 p(j,b) | p(j,g(j)) | p(m,k) | p(m,j). [resolve(57,c,62,b(flip))]. given #74 (T,wt=13): 124 p(j,b) | p(g(j),j) | p(m,k) | p(k,j). [resolve(58,c,72,b(flip))]. given #75 (T,wt=13): 125 p(j,b) | p(g(j),j) | p(m,k) | p(m,j). [resolve(58,c,62,b(flip))]. given #76 (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 #77 (F,wt=13): 195 p(g(m),b) | p(g(g(m)),g(m)) | p(m,b). [resolve(37,c,27,a(flip))]. given #78 (F,wt=13): 245 p(x,b) | p(x,g(x)) | p(b,k) | p(x,j). [para(20(a,1),242(b,1))]. given #79 (T,wt=13): 246 p(x,b) | p(g(x),x) | p(b,k) | p(x,j). [para(22(a,1),242(b,1))]. given #80 (T,wt=13): 319 p(k,b) | p(g(k),k) | j = k | p(b,j). [factor(313,a,e),merge(e)]. given #81 (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 #82 (F,wt=13): 327 p(k,b) | p(k,g(k)) | j = k | p(b,j). [factor(321,a,e),merge(e)]. given #83 (F,wt=13): 389 p(k,j) | p(j,b) | p(k,g(j)) | p(m,k). [para(61(a,1),117(b,1)),merge(e)]. given #84 (T,wt=13): 390 p(k,j) | p(j,b) | p(j,g(k)) | p(m,k). [para(61(a,1),117(b,2,1)),merge(e)]. given #85 (T,wt=13): 393 p(m,k) | p(k,j) | p(j,b) | p(m,g(j)). [para(72(b,1),117(b,1)),merge(e),merge(f)]. given #86 (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 #87 (F,wt=13): 394 p(m,k) | p(k,j) | p(j,b) | p(j,g(m)). [para(72(b,1),117(b,2,1)),merge(e),merge(f)]. given #88 (F,wt=13): 402 p(m,k) | p(m,j) | p(j,b) | p(m,g(j)). [para(62(b,1),118(b,1)),merge(e),merge(f)]. given #89 (T,wt=13): 403 p(m,k) | p(m,j) | p(j,b) | p(j,g(m)). [para(62(b,1),118(b,2,1)),merge(e),merge(f)]. given #90 (T,wt=13): 412 p(k,j) | p(j,b) | p(g(k),j) | p(m,k). [para(61(a,1),124(b,1,1)),merge(e)]. given #91 (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 #92 (F,wt=13): 413 p(k,j) | p(j,b) | p(g(j),k) | p(m,k). [para(61(a,1),124(b,2)),merge(e)]. given #93 (F,wt=13): 416 p(m,k) | p(k,j) | p(j,b) | p(g(m),j). [para(72(b,1),124(b,1,1)),merge(e),merge(f)]. given #94 (T,wt=13): 417 p(m,k) | p(k,j) | p(j,b) | p(g(j),m). [para(72(b,1),124(b,2)),merge(e),merge(f)]. given #95 (T,wt=13): 424 p(m,k) | p(m,j) | p(j,b) | p(g(m),j). [para(62(b,1),125(b,1,1)),merge(e),merge(f)]. given #96 (A,wt=15): 63 p(m,k) | k = x | m = x | b = x | -p(x,m). [para(49(a,1),6(d,2))]. given #97 (F,wt=13): 425 p(m,k) | p(m,j) | p(j,b) | p(g(j),m). [para(62(b,1),125(b,2)),merge(e),merge(f)]. given #98 (F,wt=13): 454 p(x,b) | p(x,g(x)) | p(x,k) | p(x,j). [factor(446,a,c),merge(c)]. given #99 (T,wt=13): 468 p(k,b) | p(g(k),k) | p(b,j) | k = b. [para(319(c,1),59(a,1)),merge(e),merge(f),merge(g)]. given #100 (T,wt=13): 480 p(k,b) | p(k,g(k)) | p(b,j) | k = b. [para(327(c,1),60(a,1)),merge(e),merge(f),merge(g)]. given #101 (A,wt=15): 66 p(b,k) | k = x | m = x | b = x | -p(x,b). [para(52(a,1),6(d,2))]. given #102 (F,wt=13): 486 p(k,j) | p(k,b) | p(k,g(j)) | p(m,k). [para(61(a,1),389(b,1)),merge(b)]. given #103 (F,wt=13): 489 p(m,k) | p(k,j) | p(m,b) | p(k,g(j)). [para(72(b,1),389(b,1)),merge(c),merge(f)]. given #104 (T,wt=13): 498 p(k,j) | p(j,b) | p(k,g(k)) | p(m,k). [para(61(a,1),390(c,1)),merge(b)]. given #105 (T,wt=13): 500 p(m,k) | p(k,j) | p(j,b) | p(m,g(k)). [para(72(b,1),390(c,1)),merge(c),merge(f)]. given #106 (A,wt=19): 75 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | k = x | p(x,k). [resolve(32,c,26,b)]. given #107 (F,wt=13): 508 p(k,j) | p(m,k) | p(k,b) | p(m,g(j)). [para(61(a,1),393(c,1)),merge(c)]. given #108 (F,wt=13): 511 p(m,k) | p(k,j) | p(m,b) | p(m,g(j)). [para(72(b,1),393(c,1)),merge(c),merge(d)]. given #109 (T,wt=13): 520 p(k,j) | p(m,k) | p(j,b) | p(k,g(m)). [para(61(a,1),394(d,1)),merge(c)]. given #110 (T,wt=13): 522 p(m,k) | p(k,j) | p(j,b) | p(m,g(m)). [para(72(b,1),394(d,1)),merge(c),merge(d)]. given #111 (A,wt=19): 76 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 #112 (F,wt=13): 529 p(m,k) | p(m,j) | p(m,b) | p(m,g(j)). [para(62(b,1),402(c,1)),merge(c),merge(d)]. given #113 (F,wt=13): 539 p(m,k) | p(m,j) | p(j,b) | p(m,g(m)). [para(62(b,1),403(d,1)),merge(c),merge(d)]. given #114 (T,wt=13): 547 p(k,j) | p(j,b) | p(g(k),k) | p(m,k). [para(61(a,1),412(c,2)),merge(b)]. given #115 (T,wt=13): 549 p(m,k) | p(k,j) | p(j,b) | p(g(k),m). [para(72(b,1),412(c,2)),merge(c),merge(f)]. given #116 (A,wt=23): 78 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 #117 (F,wt=13): 562 p(m,k) | p(k,j) | p(j,b) | p(g(m),k). [para(72(b,1),413(c,1,1)),merge(c),merge(f)]. given #118 (F,wt=13): 574 p(m,k) | p(k,j) | p(j,b) | p(g(m),m). [para(72(b,1),416(d,2)),merge(c),merge(d)]. given #119 (T,wt=13): 593 p(m,k) | p(m,j) | p(j,b) | p(g(m),m). [para(62(b,1),424(d,2)),merge(c),merge(d)]. given #120 (T,wt=13): 649 p(k,j) | p(m,k) | p(m,b) | p(k,g(k)). [para(61(a,1),489(d,2,1)),merge(c)]. given #121 (A,wt=20): 79 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 #122 (F,wt=13): 651 p(m,k) | p(k,j) | p(m,b) | p(k,g(m)). [para(72(b,1),489(d,2,1)),merge(c),merge(d)]. given #123 (F,wt=13): 698 p(m,k) | p(m,j) | p(k,b) | p(m,g(j)). [para(49(a,1),508(a,1)),merge(c)]. given #124 (T,wt=14): 106 p(f(b),b) | p(f(b),g(f(b))) | -p(f(b),m). [factor(103,a,c),merge(c)]. given #125 (T,wt=14): 233 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(b),m). [factor(230,a,c),merge(c)]. given #126 (A,wt=31): 80 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 #127 (F,wt=15): 93 p(b,k) | b = x | m = x | -p(m,x) | -p(x,m). [resolve(74,b,4,b),flip(b),flip(d),unit_del(b,27)]. given #128 (F,wt=15): 102 p(m,k) | p(m,j) | j = x | -p(x,m) | k = x. [para(62(b,1),29(b,2))]. given #129 (T,wt=15): 112 p(m,k) | p(k,j) | j = x | -p(x,m) | k = x. [para(72(b,1),29(b,2))]. given #130 (T,wt=15): 243 p(b,k) | j = m | p(j,m) | j = b | -p(j,b). [resolve(242,b,2,f),flip(b),flip(e),unit_del(d,27)]. given #131 (A,wt=23): 81 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 #132 (F,wt=15): 244 p(b,k) | p(b,m) | j = m | j = b | -p(j,b). [resolve(242,b,2,e),flip(d),unit_del(b,27)]. given #133 (F,wt=15): 916 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(b)),m). [factor(911,a,c),merge(c)]. given #134 (T,wt=15): 922 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(b)),m). [factor(918,a,c),merge(c)]. given #135 (T,wt=16): 87 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | m != x. [para(32(c,1),27(a,2))]. given #136 (A,wt=23): 82 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 #137 (F,wt=16): 158 p(m,k) | p(k,b) | g(k) = m | p(f(g(k)),g(k)). [resolve(138,c,14,b),flip(c)]. given #138 (F,wt=12): 1121 p(m,k) | p(k,b) | p(f(g(k)),g(k)). [para(158(c,1),126(b,1)),merge(d),merge(e),merge(f)]. given #139 (T,wt=12): 1133 p(m,k) | p(k,b) | p(f(g(m)),g(k)). [para(49(a,1),1121(c,1,1,1)),merge(b)]. given #140 (T,wt=12): 1134 p(m,k) | p(k,b) | p(f(g(k)),g(m)). [para(49(a,1),1121(c,2,1)),merge(b)]. given #141 (A,wt=23): 83 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 #142 (F,wt=12): 1156 p(m,k) | p(k,b) | p(f(g(m)),g(m)). [para(49(a,1),1133(c,2,1)),merge(b)]. given #143 (F,wt=16): 159 p(m,k) | p(k,b) | g(k) = m | p(g(k),f(g(k))). [resolve(138,c,12,b),flip(c)]. given #144 (T,wt=12): 1203 p(m,k) | p(k,b) | p(g(k),f(g(k))). [para(159(c,1),126(b,1)),merge(d),merge(e),merge(f)]. given #145 (T,wt=12): 1216 p(m,k) | p(k,b) | p(g(m),f(g(k))). [para(49(a,1),1203(c,1,1)),merge(b)]. given #146 (A,wt=23): 84 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 #147 (F,wt=12): 1217 p(m,k) | p(k,b) | p(g(k),f(g(m))). [para(49(a,1),1203(c,2,1,1)),merge(b)]. given #148 (F,wt=12): 1239 p(m,k) | p(k,b) | p(g(m),f(g(m))). [para(49(a,1),1216(c,2,1,1)),merge(b)]. given #149 (T,wt=16): 205 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | m != x. [para(37(c,1),27(a,2))]. given #150 (T,wt=16): 249 p(x,k) | p(x,b) | p(g(x),x) | j = x | p(x,j). [resolve(50,a,31,c)]. given #151 (A,wt=23): 85 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 #152 (F,wt=16): 254 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 #153 (F,wt=13): 1307 p(x,k) | p(x,b) | p(g(x),x) | p(m,k). [resolve(254,d,58,c),merge(e),merge(f)]. given #154 (T,wt=16): 255 p(x,k) | p(x,b) | p(g(x),x) | j = x | p(k,j). [para(50(a,1),61(a,2))]. given #155 (T,wt=16): 297 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 #156 (A,wt=22): 86 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 #157 (F,wt=13): 1325 p(x,k) | p(x,b) | p(x,g(x)) | p(m,k). [resolve(297,d,57,c),merge(e),merge(f)]. given #158 (F,wt=13): 1363 p(x,k) | p(x,b) | p(x,g(x)) | p(m,x). [factor(1348,a,d),merge(d),merge(e)]. given #159 (T,wt=16): 298 p(x,k) | p(x,b) | p(x,g(x)) | j = x | p(k,j). [para(51(a,1),61(a,2))]. given #160 (T,wt=16): 347 p(j,b) | p(j,g(j)) | p(b,k) | j = m | k = m. [resolve(94,d,29,b)]. given #161 (A,wt=19): 88 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 #162 (F,wt=13): 1388 p(j,b) | p(j,g(j)) | p(b,k) | k = m. [resolve(347,d,57,c(flip)),merge(e),merge(f)]. given #163 (F,wt=10): 1396 p(j,b) | p(j,g(j)) | p(b,k). [para(1388(d,1),52(a,1)),merge(e),unit_del(d,27)]. given #164 (T,wt=16): 404 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(j)). [para(101(c,1),118(b,1)),merge(f),merge(g)]. given #165 (T,wt=13): 1417 p(m,k) | p(m,j) | p(j,b) | p(k,g(j)). [para(62(b,1),404(c,1)),merge(c),merge(d),merge(e)]. given #166 (A,wt=29): 89 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 #167 (F,wt=13): 1425 p(m,k) | p(m,j) | p(m,b) | p(k,g(j)). [para(62(b,1),1417(c,1)),merge(c),merge(d)]. given #168 (F,wt=13): 1442 p(m,k) | p(m,j) | p(m,b) | p(k,g(m)). [para(62(b,1),1425(d,2,1)),merge(c),merge(d)]. given #169 (T,wt=16): 405 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(j,g(k)). [para(101(c,1),118(b,2,1)),merge(f),merge(g)]. given #170 (T,wt=16): 426 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),j). [para(101(c,1),125(b,1,1)),merge(f),merge(g)]. given #171 (A,wt=22): 90 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = b | g(g(x)) != x. [factor(81,a,e),flip(d)]. given #172 (F,wt=16): 427 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(j),k). [para(101(c,1),125(b,2)),merge(f),merge(g)]. given #173 (F,wt=16): 448 p(m,k) | p(x,b) | p(x,g(x)) | p(b,m) | p(x,j). [para(49(a,1),245(c,2))]. given #174 (T,wt=16): 453 p(k,b) | p(k,g(k)) | p(k,j) | j = b | k = b. [factor(443,c,d)]. given #175 (T,wt=13): 1532 p(k,b) | p(k,g(k)) | p(k,j) | k = b. [para(453(d,1),61(a,1)),flip(e),merge(e),merge(f)]. given #176 (A,wt=17): 91 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = x. [factor(82,a,e),flip(d),merge(e)]. given #177 (F,wt=13): 1535 p(k,b) | p(k,g(k)) | p(k,j) | j = b. [para(1532(d,1),61(a,2)),merge(e)]. given #178 (F,wt=13): 1539 p(k,b) | p(k,g(k)) | p(k,j) | p(b,b). [factor(1537,a,d),merge(d),merge(f)]. given #179 (T,wt=16): 540 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(m)). [para(101(c,1),403(d,1)),merge(d),merge(e)]. given #180 (T,wt=13): 1584 p(m,k) | p(m,j) | p(j,b) | p(k,g(m)). [para(62(b,1),540(c,1)),merge(c),merge(d),merge(e)]. given #181 (A,wt=19): 96 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,k) | p(m,x). [para(32(c,1),74(b,2))]. given #182 (F,wt=16): 594 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(m),k). [para(101(c,1),424(d,2)),merge(d),merge(e)]. given #183 (F,wt=16): 607 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),m). [para(101(c,1),425(d,1,1)),merge(d),merge(e)]. given #184 (T,wt=16): 1100 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(b))),m). [factor(1095,a,c),merge(c)]. given #185 (T,wt=16): 1106 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(b))),m). [factor(1102,a,c),merge(c)]. given #186 (A,wt=19): 99 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 #187 (F,wt=16): 1109 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(m,k). [resolve(87,d,49,a(flip))]. given #188 (F,wt=16): 1285 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | p(m,k). [resolve(205,d,49,a(flip))]. given #189 (T,wt=16): 1304 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | j = k. [factor(1286,a,f)]. given #190 (T,wt=16): 1366 p(k,b) | p(k,g(k)) | p(b,j) | p(k,k) | p(m,b). [factor(1350,a,e),merge(e)]. given #191 (A,wt=19): 100 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 #192 (F,wt=15): 1699 p(m,b) | g(m) = b | -p(g(m),b) | g(m) = m. [resolve(100,e,55,b),merge(e)]. given #193 (F,wt=16): 1380 p(j,k) | p(j,b) | p(j,g(j)) | j = m | k = m. [resolve(1363,d,29,b)]. given #194 (T,wt=13): 1710 p(j,k) | p(j,b) | p(j,g(j)) | k = m. [resolve(1380,d,57,c(flip)),merge(e),merge(f)]. given #195 (T,wt=13): 1728 p(j,k) | p(j,b) | p(j,g(j)) | j = m. [factor(1720,a,e),flip(d),merge(e),merge(f)]. given #196 (A,wt=20): 103 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 #197 (F,wt=10): 1733 p(j,k) | p(j,b) | p(j,g(j)). [resolve(1728,d,57,c(flip)),merge(d),merge(e)]. given #198 (F,wt=13): 1751 p(k,j) | p(j,k) | p(j,b) | p(k,g(j)). [para(61(a,1),1733(c,1))]. given #199 (T,wt=13): 1752 p(k,j) | p(j,k) | p(j,b) | p(j,g(k)). [para(61(a,1),1733(c,2,1))]. given #200 (T,wt=13): 1775 p(k,j) | p(k,k) | p(j,b) | p(k,g(j)). [para(61(a,1),1751(b,1)),merge(b)]. given #201 (A,wt=20): 104 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 #202 (F,wt=13): 1797 p(k,j) | p(j,k) | p(j,b) | p(k,g(k)). [para(61(a,1),1752(d,1)),merge(b)]. given #203 (F,wt=13): 1815 p(k,j) | p(k,k) | p(k,b) | p(k,g(j)). [para(61(a,1),1775(c,1)),merge(b)]. given #204 (T,wt=13): 1827 p(k,j) | p(k,k) | p(j,b) | p(k,g(k)). [para(61(a,1),1797(b,1)),merge(b)]. given #205 (T,wt=13): 1836 p(k,b) | p(k,g(k)) | p(k,j) | p(j,b). [para(1532(d,1),1797(b,2)),merge(d),merge(f),merge(g)]. given #206 (A,wt=26): 105 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 #207 (F,wt=10): 1875 p(k,j) | p(k,b) | p(k,g(k)). [para(61(a,1),1836(d,1)),merge(d),merge(e)]. given #208 (F,wt=16): 1427 p(m,k) | p(m,j) | p(j,k) | p(k,b) | p(k,g(j)). [para(101(c,1),1417(c,1)),merge(d),merge(e)]. given #209 (T,wt=13): 1912 p(m,k) | p(m,j) | p(k,b) | p(k,g(j)). [para(62(b,1),1427(c,1)),merge(c),merge(d),merge(e)]. given #210 (T,wt=16): 1443 p(m,k) | p(m,j) | p(j,k) | p(m,b) | p(k,g(k)). [para(101(c,1),1425(d,2,1)),merge(d),merge(e)]. given #211 (A,wt=25): 120 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 #212 (F,wt=13): 1933 p(m,k) | p(m,j) | p(m,b) | p(k,g(k)). [para(62(b,1),1443(c,1)),merge(c),merge(d),merge(e)]. given #213 (F,wt=16): 1464 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(m,g(k)). [para(62(b,1),405(e,1)),merge(c),merge(d)]. given #214 (T,wt=13): 1961 p(m,k) | p(m,j) | p(j,b) | p(m,g(k)). [para(62(b,1),1464(c,1)),merge(c),merge(d),merge(e)]. given #215 (T,wt=16): 1465 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(k)). [para(101(c,1),405(e,1)),merge(d),merge(e),merge(f)]. given #216 (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(119,b,34,h),flip(e),flip(g),flip(h)]. given #217 (F,wt=13): 1979 p(m,k) | p(m,j) | p(j,b) | p(k,g(k)). [para(62(b,1),1465(c,1)),merge(c),merge(d),merge(e)]. given #218 (F,wt=16): 1475 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),k). [para(101(c,1),426(e,2)),merge(d),merge(e),merge(f)]. given #219 (T,wt=16): 1657 p(m,k) | p(g(k),b) | p(g(m),g(g(k))) | p(k,b). [para(49(a,1),1109(b,1,1)),merge(e)]. given #220 (T,wt=16): 1658 p(m,k) | p(g(k),b) | p(g(k),g(g(m))) | p(k,b). [para(49(a,1),1109(b,2,1,1)),merge(e)]. given #221 (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(119,b,34,g),flip(e),flip(g)]. given #222 (F,wt=16): 1671 p(m,k) | p(g(k),b) | p(g(g(m)),g(k)) | p(k,b). [para(49(a,1),1285(b,1,1,1)),merge(e)]. given #223 (F,wt=16): 1672 p(m,k) | p(g(k),b) | p(g(g(k)),g(m)) | p(k,b). [para(49(a,1),1285(b,2,1)),merge(e)]. given #224 (T,wt=16): 2016 p(m,k) | p(g(m),b) | p(g(m),g(g(k))) | p(k,b). [para(49(a,1),1657(b,1,1)),merge(b)]. given #225 (T,wt=16): 2032 p(m,k) | p(g(k),b) | p(g(m),g(g(m))) | p(k,b). [para(49(a,1),1658(c,1,1)),merge(b)]. given #226 (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(119,b,4,f),flip(c),flip(e),flip(f)]. given #227 (F,wt=16): 2059 p(m,k) | p(g(k),b) | p(g(g(m)),g(m)) | p(k,b). [para(49(a,1),1671(c,2,1)),merge(b)]. given #228 (F,wt=16): 2093 p(m,k) | p(g(m),b) | p(g(m),g(g(m))) | p(k,b). [para(49(a,1),2016(c,2,1,1)),merge(b)]. given #229 (T,wt=17): 141 p(x,b) | p(x,g(x)) | p(m,k) | p(k,x) | p(m,g(k)). [para(20(a,1),131(b,2))]. given #230 (T,wt=17): 142 p(x,b) | p(g(x),x) | p(m,k) | p(k,x) | p(m,g(k)). [para(22(a,1),131(b,2))]. given #231 (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 #232 (F,wt=14): 2169 p(m,k) | p(k,b) | g(k) = m | g(k) = b. [para(49(a,1),135(c,2)),merge(c),merge(e)]. given #233 (F,wt=10): 2176 p(m,k) | p(k,b) | g(k) = b. [para(2169(c,1),126(b,1)),merge(d),merge(e),merge(f)]. given #234 (T,wt=6): 2185 p(m,k) | p(k,b). [para(2176(c,1),119(b,2)),merge(c),merge(d),merge(e)]. given #235 (T,wt=6): 2192 p(m,k) | p(m,b). [para(49(a,1),2185(b,1)),merge(b)]. given #236 (A,wt=20): 167 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 #237 (F,wt=12): 2200 p(m,b) | p(k,j) | j = m | k = m. [resolve(2192,a,71,c)]. given #238 (F,wt=9): 2225 p(m,b) | p(k,j) | k = m. [para(2200(c,1),61(a,1)),flip(d),merge(d),merge(e)]. given #239 (T,wt=9): 2232 p(m,b) | p(k,j) | j = m. [para(2225(c,1),61(a,2)),merge(d)]. given #240 (T,wt=9): 2245 p(m,b) | p(k,j) | p(m,m). [para(2225(c,1),2192(a,2)),merge(d)]. given #241 (A,wt=23): 168 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 #242 (F,wt=13): 2190 p(x,b) | p(x,g(x)) | p(m,k) | p(k,x). [para(20(a,1),2185(b,2))]. given #243 (F,wt=13): 2191 p(x,b) | p(g(x),x) | p(m,k) | p(k,x). [para(22(a,1),2185(b,2))]. given #244 (T,wt=13): 2209 p(k,b) | p(g(k),k) | p(b,j) | p(m,b). [para(468(d,1),2192(a,2)),merge(e)]. given #245 (T,wt=13): 2210 p(k,b) | p(k,g(k)) | p(b,j) | p(m,b). [para(480(d,1),2192(a,2)),merge(e)]. given #246 (A,wt=19): 185 p(x,b) | p(x,g(x)) | p(b,k) | j = y | p(y,j) | x != y. [para(20(a,1),69(d,1))]. given #247 (F,wt=13): 2229 p(m,b) | p(k,j) | p(k,b) | p(g(k),k). [resolve(2225,c,58,c(flip))]. given #248 (F,wt=13): 2243 p(m,b) | p(k,j) | p(k,b) | p(m,g(k)). [para(2225(c,1),1875(c,1)),merge(c)]. given #249 (T,wt=13): 2244 p(m,b) | p(k,j) | p(k,b) | p(k,g(m)). [para(2225(c,1),1875(c,2,1)),merge(c)]. given #250 (T,wt=13): 2248 p(m,b) | p(k,j) | p(j,b) | p(g(j),j). [resolve(2232,c,58,c(flip))]. given #251 (A,wt=19): 186 p(x,b) | p(g(x),x) | p(b,k) | j = y | p(y,j) | x != y. [para(22(a,1),69(d,1))]. given #252 (F,wt=13): 2249 p(m,b) | p(k,j) | p(j,b) | p(j,g(j)). [resolve(2232,c,57,c(flip))]. given #253 (F,wt=13): 2252 p(m,b) | p(k,j) | p(k,k) | p(k,g(j)). [para(2232(c,1),1775(c,1)),merge(c),merge(e)]. given #254 (T,wt=13): 2253 p(m,b) | p(k,j) | p(k,k) | p(k,g(k)). [para(2232(c,1),1827(c,1)),merge(c),merge(e)]. given #255 (T,wt=13): 2288 p(m,k) | p(x,b) | p(x,g(x)) | p(m,x). [para(49(a,1),2190(d,1)),merge(d)]. given #256 (A,wt=25): 187 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),69(d,1))]. given #257 (F,wt=13): 2353 p(m,b) | p(k,j) | p(k,b) | p(g(m),k). [para(2225(c,1),2229(d,1,1)),merge(c),merge(d)]. given #258 (F,wt=13): 2354 p(m,b) | p(k,j) | p(k,b) | p(g(k),m). [para(2225(c,1),2229(d,2)),merge(c),merge(d)]. given #259 (T,wt=13): 2393 p(k,j) | p(m,b) | p(j,b) | p(g(k),j). [para(61(a,1),2248(d,1,1)),merge(c)]. given #260 (T,wt=13): 2394 p(k,j) | p(m,b) | p(j,b) | p(g(j),k). [para(61(a,1),2248(d,2)),merge(c)]. given #261 (A,wt=19): 189 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | k = x | p(x,k). [resolve(37,c,26,b)]. given #262 (F,wt=13): 2401 p(m,b) | p(k,j) | p(j,b) | p(g(m),j). [para(2232(c,1),2248(d,1,1)),merge(c),merge(d)]. given #263 (F,wt=13): 2402 p(m,b) | p(k,j) | p(j,b) | p(g(j),m). [para(2232(c,1),2248(d,2)),merge(c),merge(d)]. given #264 (T,wt=13): 2411 p(k,j) | p(m,b) | p(j,b) | p(k,g(j)). [para(61(a,1),2249(d,1)),merge(c)]. given #265 (T,wt=10): 2634 p(m,b) | p(k,j) | p(k,g(j)). [para(2232(c,1),2411(c,1)),merge(c),merge(d),merge(e)]. given #266 (A,wt=19): 194 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 #267 (F,wt=10): 2646 p(k,j) | p(m,b) | p(k,g(k)). [para(61(a,1),2634(c,2,1)),merge(c)]. given #268 (F,wt=10): 2653 p(m,b) | p(k,j) | p(m,g(j)). [para(2225(c,1),2634(c,1)),merge(c),merge(d)]. given #269 (T,wt=10): 2654 p(m,b) | p(k,j) | p(k,g(m)). [para(2232(c,1),2634(c,2,1)),merge(c),merge(d)]. given #270 (T,wt=10): 2691 p(m,b) | p(k,j) | p(m,g(k)). [para(2225(c,1),2646(c,1)),merge(c),merge(d)]. given #271 (A,wt=23): 196 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 #272 (F,wt=13): 2412 p(k,j) | p(m,b) | p(j,b) | p(j,g(k)). [para(61(a,1),2249(d,2,1)),merge(c)]. given #273 (F,wt=13): 2420 p(m,b) | p(k,j) | p(j,b) | p(j,g(m)). [para(2232(c,1),2249(d,2,1)),merge(c),merge(d)]. given #274 (T,wt=13): 2524 p(k,j) | p(m,b) | p(j,b) | p(g(k),k). [para(61(a,1),2393(d,2)),merge(b)]. given #275 (T,wt=13): 2528 p(m,b) | p(k,j) | p(j,b) | p(g(k),m). [para(2232(c,1),2393(d,2)),merge(c),merge(d)]. given #276 (A,wt=20): 197 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 #277 (F,wt=13): 2545 p(m,b) | p(k,j) | p(j,b) | p(g(m),k). [para(2232(c,1),2394(d,1,1)),merge(c),merge(d)]. given #278 (F,wt=15): 2207 p(m,b) | k = b | -p(k,b) | k = m | -p(k,m). [resolve(2192,a,4,f),flip(b),flip(d),flip(e),unit_del(d,27)]. given #279 (T,wt=15): 2231 p(m,b) | p(k,j) | j = x | p(x,j) | m != x. [para(2225(c,1),31(c,1))]. given #280 (T,wt=15): 2233 p(m,b) | p(k,j) | j = x | -p(x,m) | k = x. [para(2225(c,1),71(c,2)),merge(c)]. given #281 (A,wt=31): 198 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 #282 (F,wt=14): 2903 p(m,b) | p(k,j) | g(m) = j | g(m) = k. [resolve(2233,d,55,b),flip(c),flip(d),merge(e)]. given #283 (F,wt=10): 3097 p(k,j) | p(m,b) | g(m) = k. [para(61(a,1),2903(c,2)),merge(c),merge(e)]. given #284 (T,wt=9): 3099 p(k,j) | p(m,b) | k != b. [para(3097(c,1),16(c,1)),flip(c),merge(d),unit_del(c,27)]. given #285 (T,wt=9): 3100 p(k,j) | p(m,b) | k != m. [para(3097(c,1),18(c,1)),flip(c),merge(d),unit_del(c,27)]. given #286 (A,wt=23): 199 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 #287 (F,wt=6): 3131 p(k,j) | p(m,b). [resolve(3100,c,2225,c),merge(c),merge(d)]. given #288 (F,wt=16): 2208 p(x,k) | p(x,b) | p(g(x),x) | p(m,x) | p(m,b). [para(50(a,1),2192(a,2))]. given #289 (T,wt=16): 3148 p(x,k) | p(x,b) | p(g(x),x) | p(x,j) | p(m,b). [para(50(a,1),3131(a,1))]. given #290 (T,wt=17): 218 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | g(x) = x. [factor(202,a,e),flip(d),merge(e)]. given #291 (A,wt=23): 200 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 #292 (F,wt=17): 353 p(j,b) | p(b,k) | p(m,j) | g(j) = j | g(j) = k. [resolve(95,b,29,b),flip(d),flip(e)]. given #293 (F,wt=16): 3207 p(j,b) | p(b,k) | p(m,j) | g(j) = k | j = b. [resolve(353,d,18,c),flip(e),merge(f)]. given #294 (T,wt=15): 3215 p(j,b) | p(b,k) | p(m,j) | j = b | k != b. [para(3207(d,1),16(c,1)),flip(e),merge(e),merge(f)]. given #295 (T,wt=12): 3236 p(j,b) | p(b,k) | p(m,j) | j = b. [resolve(3215,e,52,a),merge(e)]. given #296 (A,wt=23): 201 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 #297 (F,wt=12): 3246 p(j,b) | p(b,k) | p(m,j) | p(k,b). [para(3236(d,1),239(a,2)),merge(e)]. given #298 (F,wt=12): 3247 p(j,b) | p(b,k) | p(m,j) | p(b,b). [para(3236(d,1),242(b,2)),merge(d)]. given #299 (T,wt=13): 3249 p(j,b) | p(b,k) | p(m,j) | p(b,g(j)). [para(3236(d,1),1396(b,1)),merge(d),merge(f)]. given #300 (T,wt=13): 3250 p(j,b) | p(b,k) | p(m,j) | p(j,g(b)). [para(3236(d,1),1396(b,2,1)),merge(d),merge(f)]. given #301 (A,wt=23): 202 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 #302 (F,wt=13): 3306 p(j,b) | p(b,k) | p(m,j) | p(b,g(b)). [para(3236(d,1),3250(d,1)),merge(d),merge(e),merge(f)]. given #303 (F,wt=15): 3240 p(j,b) | p(b,k) | p(m,j) | j = k | p(j,k). [resolve(3236,d,26,b(flip)),flip(d)]. given #304 (T,wt=12): 3324 p(j,b) | p(b,k) | p(m,j) | p(j,k). [para(3240(d,1),242(b,2)),merge(e),merge(f)]. given #305 (T,wt=9): 3327 p(b,k) | p(j,b) | p(m,j). [para(52(a,1),3324(d,2)),merge(c),merge(e)]. given #306 (A,wt=23): 203 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 #307 (F,wt=15): 3328 p(b,k) | p(m,j) | p(b,m) | j = m | j = b. [resolve(3327,b,244,e),merge(c)]. given #308 (F,wt=12): 3341 p(b,k) | p(m,j) | p(b,m) | j = b. [para(3328(d,1),242(b,2)),merge(e),merge(f)]. given #309 (T,wt=12): 3351 p(b,k) | p(m,j) | p(b,m) | p(k,b). [para(3341(d,1),239(a,2)),merge(e)]. given #310 (T,wt=12): 3352 p(b,k) | p(m,j) | p(b,m) | p(b,b). [para(3341(d,1),242(b,2)),merge(d)]. given #311 (A,wt=22): 204 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 #312 (F,wt=15): 3329 p(b,k) | p(m,j) | j = m | p(j,m) | j = b. [resolve(3327,b,243,e),merge(c)]. given #313 (F,wt=15): 3330 p(b,k) | p(m,j) | j = k | j = m | j = b. [resolve(3327,b,66,e),flip(d),flip(e),flip(f),merge(c)]. given #314 (T,wt=12): 3371 p(b,k) | p(m,j) | j = b | j = m. [para(52(a,1),3330(c,2)),merge(b),merge(f)]. given #315 (T,wt=12): 3374 p(b,k) | p(m,j) | j = b | p(k,m). [para(3371(d,1),239(a,2)),merge(e)]. given #316 (A,wt=19): 206 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 #317 (F,wt=12): 3385 p(b,k) | p(m,j) | p(k,m) | p(k,b). [para(3374(c,1),239(a,2)),merge(e)]. given #318 (F,wt=12): 3386 p(b,k) | p(m,j) | p(k,m) | p(b,b). [para(3374(c,1),242(b,2)),merge(d)]. given #319 (T,wt=15): 3345 p(b,k) | p(m,j) | p(b,m) | j = k | p(j,k). [resolve(3341,d,26,b(flip)),flip(d)]. given #320 (T,wt=12): 3417 p(b,k) | p(m,j) | p(b,m) | p(j,k). [para(3345(d,1),242(b,2)),merge(e),merge(f)]. given #321 (A,wt=29): 207 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 #322 (F,wt=9): 3420 p(b,k) | p(m,j) | p(b,m). [para(3341(d,1),3417(d,1)),merge(d),merge(e),merge(f),merge(g)]. given #323 (F,wt=12): 3428 p(b,k) | p(b,m) | j = m | k = m. [resolve(3420,b,29,b)]. given #324 (T,wt=9): 3435 p(b,k) | p(b,m) | k = m. [para(3428(c,1),242(b,2)),merge(d),merge(e)]. given #325 (T,wt=6): 3442 p(b,k) | p(b,m). [para(3435(c,1),52(a,1)),merge(d),unit_del(c,27)]. given #326 (A,wt=29): 208 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 #327 (F,wt=6): 3448 p(m,k) | p(b,m). [para(49(a,1),3442(a,2)),merge(c)]. given #328 (F,wt=12): 3443 p(b,m) | p(k,j) | j = b | k = b. [resolve(3442,a,71,c)]. given #329 (T,wt=9): 3472 p(b,m) | p(k,j) | k = b. [para(3443(c,1),61(a,1)),flip(d),merge(d),merge(e)]. given #330 (T,wt=9): 3478 p(b,m) | p(k,j) | j = b. [para(3472(c,1),61(a,2)),merge(d)]. given #331 (A,wt=19): 209 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,k) | p(m,x). [para(37(c,1),74(b,2))]. given #332 (F,wt=9): 3491 p(b,m) | p(k,j) | p(b,b). [para(3472(c,1),3442(a,2)),merge(d)]. given #333 (F,wt=12): 3445 p(b,m) | k = m | k = b | -p(k,b). [resolve(3442,a,2,e),flip(d),merge(c),unit_del(b,27)]. given #334 (T,wt=12): 3461 p(b,m) | p(k,j) | j = m | k = m. [resolve(3448,a,71,c)]. given #335 (T,wt=9): 3546 p(b,m) | p(k,j) | k = m. [para(3461(c,1),61(a,1)),flip(d),merge(d),merge(e)]. given #336 (A,wt=26): 210 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 #337 (F,wt=6): 3561 p(b,m) | p(k,j). [para(3546(c,1),3442(a,2)),merge(c),merge(d)]. given #338 (F,wt=13): 3446 p(x,b) | p(x,g(x)) | p(x,k) | p(b,m). [para(20(a,1),3442(a,1))]. given #339 (T,wt=13): 3447 p(x,b) | p(g(x),x) | p(x,k) | p(b,m). [para(22(a,1),3442(a,1))]. given #340 (T,wt=13): 3585 p(b,j) | p(k,b) | p(g(k),k) | p(b,m). [para(59(a,1),3561(b,2)),merge(e)]. given #341 (A,wt=25): 215 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),69(d,1))]. given #342 (F,wt=13): 3586 p(b,j) | p(k,b) | p(k,g(k)) | p(b,m). [para(60(a,1),3561(b,2)),merge(e)]. given #343 (F,wt=13): 3625 p(x,b) | p(x,g(x)) | p(x,k) | p(x,m). [factor(3616,a,c),merge(c)]. given #344 (T,wt=14): 3614 p(x,b) | p(x,g(x)) | p(x,k) | p(f(b),b). [resolve(3446,d,14,b),unit_del(d,27)]. given #345 (T,wt=14): 3615 p(x,b) | p(x,g(x)) | p(x,k) | p(b,f(b)). [resolve(3446,d,12,b),unit_del(d,27)]. given #346 (A,wt=29): 216 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 #347 (F,wt=14): 3624 p(f(b),b) | p(f(b),g(f(b))) | p(f(b),k). [factor(3613,a,d),merge(d)]. given #348 (F,wt=14): 3738 p(x,b) | p(x,g(x)) | p(x,k) | p(f(x),b). [factor(3703,a,c),merge(c)]. given #349 (T,wt=14): 3740 p(x,b) | p(x,g(x)) | p(x,k) | p(f(b),x). [factor(3704,a,c),merge(c)]. given #350 (T,wt=14): 3785 p(x,b) | p(x,g(x)) | p(x,k) | p(x,f(b)). [factor(3769,a,c),merge(c)]. given #351 (A,wt=22): 217 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | g(x) = b | g(g(x)) != x. [factor(199,a,e),flip(d)]. given #352 (F,wt=14): 3786 p(x,b) | p(x,g(x)) | p(x,k) | p(b,f(x)). [factor(3770,a,c),merge(c)]. given #353 (F,wt=14): 3839 p(x,b) | p(x,g(x)) | p(x,k) | p(f(x),x). [factor(3833,a,c),merge(c)]. given #354 (T,wt=14): 3915 p(x,b) | p(x,g(x)) | p(x,k) | p(x,f(x)). [factor(3905,a,c),merge(c)]. given #355 (T,wt=15): 3372 p(b,k) | p(m,j) | j = b | j = k | p(j,k). [resolve(3371,d,24,b(flip)),flip(d)]. given #356 (A,wt=18): 223 p(m,k) | p(m,j) | p(j,k) | j = x | -p(x,k) | k = x. [para(101(c,1),29(b,2))]. given #357 (F,wt=12): 3940 p(b,k) | p(m,j) | j = b | p(j,k). [para(52(a,1),3372(d,2)),merge(b),merge(e)]. given #358 (F,wt=12): 3946 p(b,k) | p(m,j) | p(j,k) | j = k. [resolve(3940,c,26,b(flip)),flip(d),merge(e)]. given #359 (T,wt=9): 3958 p(b,k) | p(m,j) | p(j,k). [para(3946(d,1),242(b,2)),merge(d),merge(e)]. given #360 (T,wt=9): 3961 p(b,k) | p(m,j) | p(k,m). [para(3374(c,1),3958(c,1)),merge(d),merge(e),merge(f)]. given #361 (A,wt=20): 229 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 #362 (F,wt=13): 3962 p(b,k) | p(m,j) | k = m | p(f(k),k). [resolve(3961,c,14,b),flip(c)]. given #363 (F,wt=10): 3987 p(b,k) | p(m,j) | p(f(k),k). [para(3962(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #364 (T,wt=10): 3994 p(b,k) | p(m,j) | p(f(b),k). [para(52(a,1),3987(c,1,1)),merge(b)]. given #365 (T,wt=10): 3995 p(b,k) | p(m,j) | p(f(k),b). [para(52(a,1),3987(c,2)),merge(b)]. given #366 (A,wt=20): 230 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 #367 (F,wt=10): 4018 p(b,k) | p(m,j) | p(f(b),b). [para(52(a,1),3994(c,2)),merge(b)]. given #368 (F,wt=13): 3963 p(b,k) | p(m,j) | k = m | p(k,f(k)). [resolve(3961,c,12,b),flip(c)]. given #369 (T,wt=10): 4067 p(b,k) | p(m,j) | p(k,f(k)). [para(3963(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #370 (T,wt=10): 4069 p(b,k) | p(m,j) | p(b,f(k)). [para(52(a,1),4067(c,1)),merge(b)]. given #371 (A,wt=26): 231 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 #372 (F,wt=10): 4070 p(b,k) | p(m,j) | p(k,f(b)). [para(52(a,1),4067(c,2,1)),merge(b)]. given #373 (F,wt=10): 4097 p(b,k) | p(m,j) | p(b,f(b)). [para(52(a,1),4070(c,1)),merge(b)]. given #374 (T,wt=13): 4090 p(b,k) | p(b,f(k)) | j = m | k = m. [resolve(4069,b,29,b)]. given #375 (T,wt=13): 4110 p(b,k) | p(b,f(b)) | j = m | k = m. [resolve(4097,b,29,b)]. given #376 (A,wt=26): 232 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 #377 (F,wt=13): 4116 p(b,k) | p(b,f(k)) | k = m | p(k,m). [para(4090(c,1),239(a,2)),merge(e)]. given #378 (F,wt=10): 4140 p(b,k) | p(b,f(k)) | p(k,m). [para(4116(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #379 (T,wt=13): 4119 p(b,k) | p(b,f(k)) | k = m | p(m,m). [para(4090(c,1),4069(b,2)),merge(d),merge(f)]. given #380 (T,wt=10): 4165 p(b,k) | p(b,f(k)) | p(m,m). [para(4119(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #381 (A,wt=18): 240 p(b,k) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(239,a,2,f),flip(b),flip(d),flip(e)]. given #382 (F,wt=13): 4125 p(b,k) | p(b,f(b)) | k = m | p(k,m). [para(4110(c,1),239(a,2)),merge(e)]. given #383 (F,wt=10): 4182 p(b,k) | p(b,f(b)) | p(k,m). [para(4125(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #384 (T,wt=13): 4128 p(b,k) | p(b,f(b)) | k = m | p(m,m). [para(4110(c,1),4097(b,2)),merge(d),merge(f)]. given #385 (T,wt=10): 4207 p(b,k) | p(b,f(b)) | p(m,m). [para(4128(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #386 (A,wt=18): 241 p(b,k) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(239,a,2,e),flip(b),flip(d)]. given #387 (F,wt=14): 4150 p(b,k) | p(b,f(k)) | k = m | p(f(k),k). [resolve(4140,c,14,b),flip(c)]. given #388 (F,wt=11): 4223 p(b,k) | p(b,f(k)) | p(f(k),k). [para(4150(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #389 (T,wt=11): 4230 p(b,k) | p(b,f(k)) | p(f(b),k). [para(52(a,1),4223(c,1,1)),merge(b)]. given #390 (T,wt=11): 4231 p(b,k) | p(b,f(k)) | p(f(k),b). [para(52(a,1),4223(c,2)),merge(b)]. given #391 (A,wt=19): 247 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,k) | p(x,j). [para(32(c,1),242(b,1))]. given #392 (F,wt=11): 4254 p(b,k) | p(b,f(k)) | p(f(b),b). [para(52(a,1),4230(c,2)),merge(b)]. given #393 (F,wt=14): 4151 p(b,k) | p(b,f(k)) | k = m | p(k,f(k)). [resolve(4140,c,12,b),flip(c)]. given #394 (T,wt=11): 4308 p(b,k) | p(b,f(k)) | p(k,f(k)). [para(4151(c,1),52(a,1)),merge(e),unit_del(d,27)]. given #395 (T,wt=7): 4310 p(b,k) | p(b,f(k)). [para(52(a,1),4308(c,1)),merge(b),merge(d)]. given #396 (A,wt=19): 248 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,k) | p(x,j). [para(37(c,1),242(b,1))]. given #397 (F,wt=7): 4314 p(b,k) | p(b,f(b)). [para(52(a,1),4310(b,2,1)),merge(b)]. given #398 (F,wt=14): 4312 p(x,b) | p(x,g(x)) | p(b,k) | p(x,f(k)). [para(20(a,1),4310(b,1))]. given #399 (T,wt=14): 4313 p(x,b) | p(g(x),x) | p(b,k) | p(x,f(k)). [para(22(a,1),4310(b,1))]. given #400 (T,wt=14): 4318 p(x,b) | p(x,g(x)) | p(b,k) | p(b,f(x)). [para(67(c,1),4310(b,2,1)),merge(d)]. given #401 (A,wt=20): 250 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 #402 (F,wt=14): 4319 p(x,b) | p(g(x),x) | p(b,k) | p(b,f(x)). [para(68(c,1),4310(b,2,1)),merge(d)]. given #403 (F,wt=14): 4340 p(x,b) | p(x,g(x)) | p(b,k) | p(x,f(b)). [para(20(a,1),4314(b,1))]. given #404 (T,wt=14): 4341 p(x,b) | p(g(x),x) | p(b,k) | p(x,f(b)). [para(22(a,1),4314(b,1))]. given #405 (T,wt=14): 4372 p(x,b) | p(x,g(x)) | p(x,k) | p(x,f(k)). [factor(4362,a,c),merge(c)]. given #406 (A,wt=20): 251 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 #407 (F,wt=14): 4412 p(x,b) | p(x,g(x)) | p(b,k) | p(x,f(x)). [factor(4405,a,c),merge(c)]. given #408 (F,wt=15): 3468 p(b,m) | -p(m,b) | k = b | k = m | -p(k,m). [resolve(3448,a,4,e),flip(b),flip(d),unit_del(b,27)]. given #409 (T,wt=16): 3332 p(x,b) | p(x,g(x)) | p(b,k) | p(j,x) | p(m,j). [para(20(a,1),3327(b,2))]. given #410 (T,wt=16): 3333 p(x,b) | p(g(x),x) | p(b,k) | p(j,x) | p(m,j). [para(22(a,1),3327(b,2))]. given #411 (A,wt=22): 252 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 #412 (F,wt=16): 3965 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(x,m). [para(67(c,1),3961(c,1)),merge(d)]. given #413 (F,wt=16): 3966 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(x,m). [para(68(c,1),3961(c,1)),merge(d)]. given #414 (T,wt=17): 410 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 #415 (T,wt=13): 4599 p(k,j) | p(j,b) | p(m,k) | g(j) = k. [para(61(a,1),410(d,2)),merge(d),merge(f)]. given #416 (A,wt=19): 253 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 #417 (F,wt=9): 4614 p(k,j) | p(j,b) | p(m,k). [para(4599(d,1),2191(b,1)),merge(d),merge(e),merge(f),merge(g)]. given #418 (F,wt=16): 4630 p(x,k) | p(x,b) | p(g(x),x) | j = b | p(b,j). [resolve(253,f,22,a(flip)),merge(f),merge(g)]. given #419 (T,wt=16): 4636 p(x,b) | p(x,g(x)) | p(k,j) | p(j,x) | p(m,k). [para(20(a,1),4614(b,2))]. given #420 (T,wt=16): 4637 p(x,b) | p(g(x),x) | p(k,j) | p(j,x) | p(m,k). [para(22(a,1),4614(b,2))]. given #421 (A,wt=22): 266 p(x,k) | p(x,b) | p(g(x),x) | p(k,j) | j = y | -p(y,x) | k = y. [para(50(a,1),71(c,2))]. given #422 (F,wt=16): 4663 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | j = k. [factor(4645,a,f)]. given #423 (F,wt=16): 4665 p(x,b) | p(g(x),x) | p(x,k) | j = x | p(b,j). [factor(4647,a,d),merge(d)]. given #424 (T,wt=16): 4708 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | k = b. [factor(4707,a,e),merge(e),merge(f)]. given #425 (T,wt=16): 4723 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(m,b). [para(4708(e,1),2192(a,2)),merge(f)]. given #426 (A,wt=25): 278 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 #427 (F,wt=17): 422 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 #428 (F,wt=16): 4750 p(j,b) | p(m,k) | p(m,j) | g(j) = k | j = b. [resolve(422,d,18,c),flip(e),merge(f)]. given #429 (T,wt=15): 4757 p(j,b) | p(m,k) | p(m,j) | j = b | k != b. [para(4750(d,1),16(c,1)),flip(e),merge(e),merge(f)]. given #430 (T,wt=15): 4758 p(j,b) | p(m,k) | p(m,j) | j = b | j != k. [para(4750(d,1),18(c,1)),flip(e),flip(g),merge(e),merge(f)]. given #431 (A,wt=20): 293 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 #432 (F,wt=15): 4764 p(j,b) | p(m,k) | p(m,j) | j = b | p(k,m). [para(4750(d,1),425(d,1)),merge(e),merge(f),merge(g)]. given #433 (F,wt=12): 4786 p(j,b) | p(m,k) | p(m,j) | p(k,m). [para(4764(d,1),62(b,1)),flip(f),merge(e),merge(g),unit_del(e,27)]. given #434 (T,wt=15): 4767 p(j,b) | p(m,k) | p(m,j) | j = b | p(j,k). [para(4750(d,1),1325(c,2)),merge(f),merge(g),merge(h)]. given #435 (T,wt=12): 4802 p(j,b) | p(m,k) | p(m,j) | p(j,k). [para(4767(d,1),62(b,1)),flip(f),merge(e),merge(g),unit_del(e,27)]. given #436 (A,wt=20): 294 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 #437 (F,wt=9): 4813 p(m,k) | p(m,j) | p(j,b). [para(62(b,1),4802(d,1)),merge(d),merge(e),merge(f)]. given #438 (F,wt=16): 4830 p(x,b) | p(x,g(x)) | p(m,k) | p(m,j) | p(j,x). [para(20(a,1),4813(c,2))]. given #439 (T,wt=16): 4831 p(x,b) | p(g(x),x) | p(m,k) | p(m,j) | p(j,x). [para(22(a,1),4813(c,2))]. given #440 (T,wt=17): 461 p(j,b) | p(b,k) | p(j,j) | g(j) = j | g(j) = k. [resolve(246,b,29,b),flip(d),flip(e)]. given #441 (A,wt=22): 295 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 #442 (F,wt=13): 4861 p(j,b) | p(b,k) | p(j,j) | g(j) = k. [para(461(d,1),245(b,2)),merge(e),merge(f),merge(g),merge(h)]. given #443 (F,wt=12): 4880 p(j,b) | p(b,k) | p(j,j) | p(j,k). [para(4861(d,1),245(b,2)),merge(d),merge(f),merge(g)]. given #444 (T,wt=13): 4873 p(b,k) | p(j,b) | p(j,j) | g(j) = b. [para(52(a,1),4861(d,2)),merge(c)]. given #445 (T,wt=9): 4898 p(b,k) | p(j,b) | p(j,j). [para(4873(d,1),245(b,2)),merge(d),merge(e),merge(f),merge(g)]. given #446 (A,wt=19): 296 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 #447 (F,wt=16): 4915 p(x,k) | p(x,b) | p(x,g(x)) | j = b | p(b,j). [resolve(296,f,20,a(flip)),merge(f),merge(g)]. given #448 (F,wt=16): 4935 p(x,b) | p(x,g(x)) | p(x,k) | j = x | p(b,j). [factor(4920,a,d),merge(d)]. given #449 (T,wt=17): 624 p(k,b) | p(g(k),k) | p(b,j) | p(b,b) | p(b,g(b)). [factor(622,c,g),merge(f)]. given #450 (T,wt=17): 629 p(k,b) | p(k,g(k)) | p(b,j) | p(b,b) | p(b,g(b)). [factor(627,c,g),merge(f)]. given #451 (A,wt=22): 309 p(x,k) | p(x,b) | p(x,g(x)) | p(k,j) | j = y | -p(y,x) | k = y. [para(51(a,1),71(c,2))]. given #452 (F,wt=17): 1316 p(j,k) | p(j,b) | p(m,k) | g(j) = j | g(j) = k. [resolve(1307,c,29,b),flip(d),flip(e)]. given #453 (F,wt=16): 4974 p(j,k) | p(j,b) | p(m,k) | g(j) = k | j = b. [resolve(1316,d,18,c),flip(e),merge(f)]. given #454 (T,wt=12): 4983 p(j,k) | p(j,b) | p(m,k) | j = b. [para(4974(d,1),1325(c,2)),merge(e),merge(f),merge(g),merge(h)]. given #455 (T,wt=12): 4988 p(j,k) | p(j,b) | p(m,k) | j = k. [resolve(4983,d,26,b(flip)),flip(d),merge(e)]. given #456 (A,wt=20): 312 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 #457 (F,wt=12): 5001 p(m,k) | p(j,k) | p(j,b) | j = m. [para(49(a,1),4988(d,2)),merge(d)]. given #458 (F,wt=9): 5016 p(m,k) | p(j,k) | p(j,b). [para(5001(d,1),4983(d,1)),merge(d),merge(e),merge(f),unit_del(d,27)]. given #459 (T,wt=9): 5027 p(m,k) | p(j,m) | p(j,b). [para(49(a,1),5016(b,2)),merge(b)]. given #460 (T,wt=13): 5049 p(m,k) | p(j,b) | j = m | p(f(j),j). [resolve(5027,b,14,b),flip(c)]. given #461 (A,wt=20): 313 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 #462 (F,wt=10): 5061 p(m,k) | p(j,b) | p(f(j),j). [para(5049(c,1),5016(b,1)),merge(d),merge(e),merge(f)]. given #463 (F,wt=13): 5050 p(m,k) | p(j,b) | j = m | p(j,f(j)). [resolve(5027,b,12,b),flip(c)]. given #464 (T,wt=10): 5100 p(m,k) | p(j,b) | p(j,f(j)). [para(5050(c,1),5016(b,1)),merge(d),merge(e),merge(f)]. given #465 (T,wt=14): 5080 p(m,k) | p(j,b) | f(j) = j | f(j) = k. [resolve(5061,c,29,b),flip(c),flip(d)]. given #466 (A,wt=19): 314 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 #467 (F,wt=13): 5124 p(m,k) | p(j,b) | f(j) = k | p(j,j). [para(5080(c,1),5061(c,1)),merge(d),merge(e)]. given #468 (F,wt=13): 5137 p(m,k) | p(j,b) | f(j) = m | p(j,j). [para(49(a,1),5124(c,2)),merge(b)]. given #469 (T,wt=15): 5025 p(m,k) | p(j,b) | j = k | j = m | j = b. [resolve(5016,b,6,d),flip(c),flip(d),flip(e)]. given #470 (T,wt=12): 5144 p(m,k) | p(j,b) | j = m | j = b. [para(49(a,1),5025(c,2)),merge(b),merge(e)]. given #471 (A,wt=26): 316 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 #472 (F,wt=9): 5150 p(m,k) | p(j,b) | j = b. [para(5144(c,1),5016(b,1)),merge(d),merge(e),merge(f)]. given #473 (F,wt=10): 5163 p(m,k) | p(j,b) | p(f(b),j). [para(5150(c,1),5061(c,1,1)),merge(c),merge(d)]. given #474 (T,wt=10): 5164 p(m,k) | p(j,b) | p(f(j),b). [para(5150(c,1),5061(c,2)),merge(c),merge(d)]. given #475 (T,wt=10): 5165 p(m,k) | p(j,b) | p(b,f(j)). [para(5150(c,1),5100(c,1)),merge(c),merge(d)]. given #476 (A,wt=26): 317 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 #477 (F,wt=10): 5166 p(m,k) | p(j,b) | p(j,f(b)). [para(5150(c,1),5100(c,2,1)),merge(c),merge(d)]. given #478 (F,wt=10): 5183 p(m,k) | p(j,b) | p(f(b),b). [para(5150(c,1),5163(c,2)),merge(c),merge(d)]. given #479 (T,wt=10): 5196 p(m,k) | p(j,b) | f(j) = k. [para(5080(c,1),5164(c,1)),merge(d),merge(e),merge(f)]. given #480 (T,wt=10): 5221 p(m,k) | p(j,b) | p(b,f(b)). [para(5150(c,1),5166(c,1)),merge(c),merge(d)]. given #481 (A,wt=20): 321 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 #482 (F,wt=10): 5242 p(m,k) | p(j,b) | f(j) = m. [para(49(a,1),5196(c,2)),merge(b)]. given #483 (F,wt=10): 5243 p(m,k) | p(j,b) | f(b) = k. [para(5150(c,1),5196(c,1,1)),merge(c),merge(d)]. given #484 (T,wt=10): 5261 p(m,k) | p(j,b) | f(b) = m. [para(5150(c,1),5242(c,1,1)),merge(c),merge(d)]. given #485 (T,wt=9): 5270 p(m,k) | p(j,b) | -p(b,m). [resolve(5261,c,8,c),unit_del(c,27)]. given #486 (A,wt=20): 322 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 #487 (F,wt=12): 5260 p(m,k) | p(j,b) | j = m | -p(j,m). [resolve(5242,c,8,c),flip(c)]. given #488 (F,wt=9): 5293 p(m,k) | p(j,b) | j = m. [resolve(5260,d,5027,b),merge(d),merge(e)]. given #489 (T,wt=6): 5299 p(m,k) | p(j,b). [para(5293(c,1),5016(b,1)),merge(c),merge(d),merge(e)]. given #490 (T,wt=13): 5306 p(x,b) | p(x,g(x)) | p(m,k) | p(j,x). [para(20(a,1),5299(b,2))]. given #491 (A,wt=19): 323 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 #492 (F,wt=13): 5307 p(x,b) | p(g(x),x) | p(m,k) | p(j,x). [para(22(a,1),5299(b,2))]. given #493 (F,wt=15): 5305 p(m,k) | j = m | p(j,m) | j = b | -p(b,j). [resolve(5299,b,2,e),flip(b),flip(e),unit_del(d,27)]. given #494 (T,wt=17): 1637 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(f(b)))),m). [factor(1632,a,c),merge(c)]. given #495 (T,wt=17): 1643 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(f(b)))),m). [factor(1639,a,c),merge(c)]. given #496 (A,wt=26): 325 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 #497 (F,wt=17): 1771 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | p(k,g(j)). [para(1304(e,1),1733(c,1)),merge(e),merge(f)]. given #498 (F,wt=17): 1772 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | p(j,g(k)). [para(1304(e,1),1733(c,2,1)),merge(e),merge(f)]. given #499 (T,wt=17): 1900 p(k,b) | p(g(k),k) | p(b,j) | p(k,j) | p(b,g(k)). [para(468(d,1),1875(c,1)),merge(e)]. given #500 (T,wt=17): 1901 p(k,b) | p(g(k),k) | p(b,j) | p(k,j) | p(k,g(b)). [para(468(d,1),1875(c,2,1)),merge(e)]. given #501 (A,wt=26): 326 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 #502 (F,wt=17): 3637 p(j,b) | p(j,k) | p(b,m) | g(j) = j | g(j) = k. [resolve(3447,b,29,b),flip(d),flip(e)]. given #503 (F,wt=16): 5474 p(j,b) | p(j,k) | p(b,m) | g(j) = k | j = b. [resolve(3637,d,18,c),flip(e),merge(f)]. given #504 (T,wt=12): 5489 p(j,b) | p(j,k) | p(b,m) | j = b. [para(5474(d,1),1733(c,2)),merge(e),merge(f),merge(g)]. given #505 (T,wt=12): 5494 p(j,b) | p(j,k) | p(b,m) | j = k. [resolve(5489,d,26,b(flip)),flip(d),merge(e)]. given #506 (A,wt=19): 328 p(f(k),b) | p(f(k),g(f(k))) | p(b,k) | k = m | -p(k,m). [resolve(67,c,10,c(flip)),flip(d)]. given #507 (F,wt=12): 5505 p(j,b) | p(j,k) | p(b,m) | p(k,b). [para(5489(d,1),3561(b,2)),merge(d)]. given #508 (F,wt=12): 5518 p(j,b) | p(j,k) | p(b,m) | p(k,k). [para(5494(d,1),3561(b,2)),merge(d)]. given #509 (T,wt=12): 5523 p(j,b) | p(j,k) | p(b,m) | k = b. [para(5494(d,1),5489(d,1)),merge(d),merge(e),merge(f)]. given #510 (T,wt=12): 5581 p(j,b) | p(j,k) | p(b,m) | p(m,b). [para(5523(d,1),2192(a,2)),merge(e)]. given #511 (A,wt=22): 329 p(x,b) | p(x,g(x)) | p(b,k) | k = y | m = y | b = y | -p(y,x). [para(67(c,1),6(d,2))]. given #512 (F,wt=12): 5583 p(j,b) | p(j,k) | p(b,m) | p(b,b). [para(5523(d,1),3442(a,2)),merge(e)]. given #513 (F,wt=12): 5584 p(j,b) | p(j,k) | p(b,m) | p(b,j). [para(5523(d,1),3561(b,1)),merge(d)]. given #514 (T,wt=13): 5501 p(j,b) | p(j,k) | p(b,m) | p(b,g(j)). [para(5489(d,1),1733(c,1)),merge(d),merge(e)]. given #515 (T,wt=13): 5502 p(j,b) | p(j,k) | p(b,m) | p(j,g(b)). [para(5489(d,1),1733(c,2,1)),merge(d),merge(e)]. given #516 (A,wt=19): 330 p(f(k),b) | p(g(f(k)),f(k)) | p(b,k) | k = m | -p(k,m). [resolve(68,c,10,c(flip)),flip(d)]. given #517 (F,wt=13): 5515 p(j,b) | p(j,k) | p(b,m) | p(k,g(j)). [para(5494(d,1),1733(c,1)),merge(d),merge(e)]. given #518 (F,wt=13): 5516 p(j,b) | p(j,k) | p(b,m) | p(j,g(k)). [para(5494(d,1),1733(c,2,1)),merge(d),merge(e)]. given #519 (T,wt=13): 5522 p(j,b) | p(j,k) | p(b,m) | g(j) = k. [para(5494(d,1),3637(d,2)),merge(d),merge(e),merge(f),merge(h)]. given #520 (T,wt=9): 5694 p(j,b) | p(j,k) | p(b,m). [para(5522(d,1),1733(c,2)),merge(d),merge(e),merge(f)]. given #521 (A,wt=22): 331 p(x,b) | p(g(x),x) | p(b,k) | k = y | m = y | b = y | -p(y,x). [para(68(c,1),6(d,2))]. given #522 (F,wt=15): 5703 p(j,b) | p(b,m) | j = k | j = m | j = b. [resolve(5694,b,6,d),flip(c),flip(d),flip(e)]. given #523 (F,wt=15): 5717 p(j,b) | p(b,m) | j = m | j = b | p(k,k). [para(5703(c,1),3561(b,2)),merge(e)]. given #524 (T,wt=15): 5726 p(j,b) | p(b,m) | j = b | p(k,k) | p(k,m). [para(5717(c,1),3561(b,2)),merge(e)]. given #525 (T,wt=15): 5735 p(j,b) | p(b,m) | p(k,k) | p(k,m) | p(k,b). [para(5726(c,1),3561(b,2)),merge(e)]. given #526 (A,wt=40): 332 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(77,b,39,h),flip(e),flip(g),flip(h)]. given #527 (F,wt=16): 5722 p(j,b) | p(b,m) | j = b | p(k,k) | p(g(j),j). [resolve(5717,c,58,c(flip)),merge(e)]. given #528 (F,wt=16): 5723 p(j,b) | p(b,m) | j = b | p(k,k) | p(j,g(j)). [resolve(5717,c,57,c(flip)),merge(e)]. given #529 (T,wt=16): 5753 p(j,b) | p(b,m) | p(k,k) | p(g(j),j) | p(k,b). [para(5722(c,1),3561(b,2)),merge(e)]. given #530 (T,wt=16): 5756 p(j,b) | p(b,m) | p(k,k) | p(j,g(j)) | p(k,b). [para(5723(c,1),3561(b,2)),merge(e)]. given #531 (A,wt=39): 333 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(77,b,39,g),flip(e),flip(g)]. given #532 (F,wt=17): 4000 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(f(x),k). [para(67(c,1),3987(c,1,1)),merge(d)]. given #533 (F,wt=17): 4001 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(f(k),x). [para(67(c,1),3987(c,2)),merge(d)]. given #534 (T,wt=17): 4002 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(f(x),k). [para(68(c,1),3987(c,1,1)),merge(d)]. given #535 (T,wt=17): 4003 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(f(k),x). [para(68(c,1),3987(c,2)),merge(d)]. given #536 (A,wt=40): 335 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(77,b,34,h),flip(e),flip(g),flip(h)]. given #537 (F,wt=17): 4020 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(f(b),x). [para(67(c,1),3994(c,2)),merge(d)]. given #538 (F,wt=17): 4021 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(f(b),x). [para(68(c,1),3994(c,2)),merge(d)]. given #539 (T,wt=17): 4035 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(f(x),b). [para(67(c,1),3995(c,1,1)),merge(d)]. given #540 (T,wt=17): 4036 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(f(x),b). [para(68(c,1),3995(c,1,1)),merge(d)]. given #541 (A,wt=39): 336 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(77,b,34,g),flip(e),flip(g)]. given #542 (F,wt=17): 4076 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(k,f(x)). [para(67(c,1),4067(c,2,1)),merge(d)]. given #543 (F,wt=17): 4078 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(k,f(x)). [para(68(c,1),4067(c,2,1)),merge(d)]. given #544 (T,wt=17): 4376 p(k,b) | p(k,g(k)) | p(b,j) | p(b,b) | p(k,f(k)). [factor(4367,a,d),merge(d)]. given #545 (T,wt=17): 4463 p(k,b) | p(k,g(k)) | p(b,j) | p(b,b) | p(k,f(b)). [factor(4455,a,d),merge(d)]. given #546 (A,wt=33): 338 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(77,b,4,f),flip(c),flip(e),flip(f)]. given #547 (F,wt=17): 4670 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(b,g(j)). [factor(4654,a,e),merge(e)]. given #548 (F,wt=17): 4671 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(j,g(b)). [factor(4655,a,e),merge(e)]. given #549 (T,wt=17): 4703 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(k,g(j)). [para(4663(e,1),1733(c,1)),merge(e),merge(f)]. given #550 (T,wt=17): 4704 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(j,g(k)). [para(4663(e,1),1733(c,2,1)),merge(e),merge(f)]. given #551 (A,wt=33): 339 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(77,b,2,f),flip(c),flip(e),flip(f)]. given #552 (F,wt=17): 5811 p(x,b) | p(x,g(x)) | p(b,k) | p(m,j) | p(f(x),x). [factor(5803,a,d),merge(d)]. given #553 (F,wt=18): 2189 p(m,k) | k = b | b = x | k = x | -p(k,x) | -p(x,k). [resolve(2185,b,4,b),flip(b),flip(d)]. given #554 (T,wt=18): 3144 p(m,b) | j = b | -p(j,b) | k = b | j = k | -p(j,k). [resolve(3131,a,4,f),flip(b),flip(d),flip(e)]. given #555 (T,wt=18): 3145 p(m,b) | k = b | -p(k,b) | j = b | j = k | -p(j,k). [resolve(3131,a,4,e),flip(b),flip(d)]. given #556 (A,wt=35): 340 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(94,b,39,h),flip(f),flip(i)]. given #557 (F,wt=18): 3146 p(m,b) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(3131,a,2,f),flip(b),flip(d),flip(e)]. given #558 (F,wt=18): 3147 p(m,b) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(3131,a,2,e),flip(b),flip(d)]. given #559 (T,wt=18): 3373 p(b,k) | p(m,j) | j = b | j = x | -p(x,m) | k = x. [para(3371(d,1),29(b,2))]. given #560 (T,wt=18): 3581 p(b,m) | j = b | -p(j,b) | k = b | j = k | -p(j,k). [resolve(3561,b,4,f),flip(b),flip(d),flip(e)]. given #561 (A,wt=34): 341 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(94,b,39,g),flip(h)]. given #562 (F,wt=18): 3582 p(b,m) | k = b | -p(k,b) | j = b | j = k | -p(j,k). [resolve(3561,b,4,e),flip(b),flip(d)]. given #563 (F,wt=18): 3583 p(b,m) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(3561,b,2,f),flip(b),flip(d),flip(e)]. given #564 (T,wt=18): 3584 p(b,m) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(3561,b,2,e),flip(b),flip(d)]. given #565 (T,wt=18): 3992 p(b,k) | p(m,j) | f(k) = k | f(k) = m | f(k) = b. [resolve(3987,c,6,d),flip(c),flip(d),flip(e)]. given #566 (A,wt=35): 342 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(94,b,34,h),flip(f),flip(i)]. given #567 (F,wt=14): 6198 p(b,k) | p(m,j) | f(k) = b | f(k) = m. [para(52(a,1),3992(c,2)),merge(b),merge(f)]. given #568 (F,wt=14): 6214 p(b,k) | p(m,j) | f(k) = b | f(b) = m. [para(52(a,1),6198(d,1,1)),merge(b)]. given #569 (T,wt=10): 6244 p(b,k) | p(m,j) | f(b) = m. [para(6214(c,1),3987(c,1)),merge(d),merge(e),merge(f)]. given #570 (T,wt=9): 6245 p(b,k) | p(m,j) | -p(b,m). [resolve(6244,c,8,c),unit_del(c,27)]. given #571 (A,wt=34): 343 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(94,b,34,g),flip(h)]. given #572 (F,wt=13): 6259 p(b,k) | p(m,j) | p(b,b) | p(b,g(b)). [factor(6252,a,e)]. given #573 (F,wt=16): 6213 p(b,k) | p(m,j) | f(k) = b | k = m | -p(k,m). [resolve(6198,d,8,c),flip(d)]. given #574 (T,wt=13): 6278 p(b,k) | p(m,j) | f(k) = b | k = m. [resolve(6213,e,3961,c),merge(e),merge(f)]. given #575 (T,wt=9): 6296 p(b,k) | p(m,j) | k = m. [para(6278(c,1),3987(c,1)),merge(d),merge(e),merge(f)]. given #576 (A,wt=28): 344 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(94,b,4,f),flip(d),flip(g)]. given #577 (F,wt=6): 6309 p(b,k) | p(m,j). [para(6296(c,1),52(a,1)),merge(d),unit_del(c,27)]. given #578 (F,wt=9): 6322 p(b,k) | j = m | k = m. [resolve(6309,b,29,b)]. given #579 (T,wt=9): 6328 p(b,k) | k = m | p(k,m). [para(6322(b,1),239(a,2)),merge(d)]. given #580 (T,wt=6): 6339 p(b,k) | p(k,m). [para(6328(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #581 (A,wt=28): 345 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(94,b,2,f),flip(d),flip(g)]. given #582 (F,wt=9): 6332 p(b,k) | k = m | p(m,m). [para(6322(b,1),6309(b,2)),merge(c)]. given #583 (F,wt=6): 6372 p(b,k) | p(m,m). [para(6332(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #584 (T,wt=10): 6350 p(b,k) | k = m | p(f(k),k). [resolve(6339,b,14,b),flip(b)]. given #585 (T,wt=7): 6379 p(b,k) | p(f(k),k). [para(6350(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #586 (A,wt=27): 346 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(94,b,2,e),flip(f)]. given #587 (F,wt=7): 6388 p(b,k) | p(f(b),k). [para(52(a,1),6379(b,1,1)),merge(b)]. given #588 (F,wt=7): 6389 p(b,k) | p(f(k),b). [para(52(a,1),6379(b,2)),merge(b)]. given #589 (T,wt=7): 6421 p(b,k) | p(f(b),b). [para(52(a,1),6388(b,2)),merge(b)]. given #590 (T,wt=10): 6351 p(b,k) | k = m | p(k,f(k)). [resolve(6339,b,12,b),flip(b)]. given #591 (A,wt=20): 358 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 #592 (F,wt=7): 6457 p(b,k) | p(k,f(k)). [para(6351(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #593 (F,wt=7): 6481 p(b,k) | p(k,f(b)). [para(52(a,1),6457(b,2,1)),merge(b)]. given #594 (T,wt=12): 6321 p(b,k) | j = b | j = m | -p(j,m). [resolve(6309,b,93,d),flip(c),flip(d),merge(b)]. given #595 (T,wt=12): 6326 p(b,k) | k = m | j = k | p(j,k). [resolve(6322,b,24,b(flip)),flip(c)]. given #596 (A,wt=23): 359 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 #597 (F,wt=9): 6496 p(b,k) | k = m | p(j,k). [para(6326(c,1),242(b,2)),merge(d),merge(e)]. given #598 (F,wt=6): 6503 p(b,k) | p(j,k). [para(6496(b,1),52(a,1)),merge(d),unit_del(c,27)]. given #599 (T,wt=6): 6511 p(b,k) | p(j,b). [para(52(a,1),6503(b,2)),merge(b)]. given #600 (T,wt=12): 6510 p(b,k) | j = k | j = m | j = b. [resolve(6503,b,6,d),flip(b),flip(c),flip(d)]. given #601 (A,wt=20): 360 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 #602 (F,wt=9): 6529 p(b,k) | j = b | j = m. [para(52(a,1),6510(b,2)),merge(b),merge(e)]. given #603 (F,wt=13): 6353 p(x,b) | p(x,g(x)) | p(b,k) | p(x,m). [para(67(c,1),6339(b,1)),merge(d)]. given #604 (T,wt=13): 6354 p(x,b) | p(g(x),x) | p(b,k) | p(x,m). [para(68(c,1),6339(b,1)),merge(d)]. given #605 (T,wt=13): 6514 p(x,b) | p(x,g(x)) | p(b,k) | p(j,x). [para(67(c,1),6503(b,2)),merge(d)]. given #606 (A,wt=23): 361 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 #607 (F,wt=13): 6515 p(x,b) | p(g(x),x) | p(b,k) | p(j,x). [para(68(c,1),6503(b,2)),merge(d)]. given #608 (F,wt=14): 6394 p(x,b) | p(x,g(x)) | p(b,k) | p(f(x),k). [para(67(c,1),6379(b,1,1)),merge(d)]. given #609 (T,wt=14): 6395 p(x,b) | p(x,g(x)) | p(b,k) | p(f(k),x). [para(67(c,1),6379(b,2)),merge(d)]. given #610 (T,wt=14): 6396 p(x,b) | p(g(x),x) | p(b,k) | p(f(x),k). [para(68(c,1),6379(b,1,1)),merge(d)]. given #611 (A,wt=35): 363 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(362,b,39,h),flip(d),flip(f)]. given #612 (F,wt=14): 6397 p(x,b) | p(g(x),x) | p(b,k) | p(f(k),x). [para(68(c,1),6379(b,2)),merge(d)]. given #613 (F,wt=14): 6423 p(x,b) | p(x,g(x)) | p(b,k) | p(f(b),x). [para(67(c,1),6388(b,2)),merge(d)]. given #614 (T,wt=14): 6424 p(x,b) | p(g(x),x) | p(b,k) | p(f(b),x). [para(68(c,1),6388(b,2)),merge(d)]. given #615 (T,wt=14): 6438 p(x,b) | p(x,g(x)) | p(b,k) | p(f(x),b). [para(67(c,1),6389(b,1,1)),merge(d)]. given #616 (A,wt=36): 364 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(362,b,39,g),flip(d),flip(f),flip(g)]. given #617 (F,wt=14): 6439 p(x,b) | p(g(x),x) | p(b,k) | p(f(x),b). [para(68(c,1),6389(b,1,1)),merge(d)]. given #618 (F,wt=14): 6484 p(x,b) | p(x,g(x)) | p(b,k) | p(k,f(x)). [para(67(c,1),6457(b,2,1)),merge(d)]. given #619 (T,wt=14): 6485 p(x,b) | p(g(x),x) | p(b,k) | p(k,f(x)). [para(68(c,1),6457(b,2,1)),merge(d)]. given #620 (T,wt=14): 6631 p(x,b) | p(x,g(x)) | p(b,k) | p(f(x),x). [factor(6623,a,d),merge(d)]. given #621 (A,wt=35): 365 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(362,b,34,h),flip(d),flip(f)]. given #622 (F,wt=15): 6327 p(b,k) | k = m | j = x | -p(x,m) | k = x. [para(6322(b,1),29(b,2))]. given #623 (F,wt=15): 6386 p(b,k) | f(k) = k | f(k) = m | f(k) = b. [resolve(6379,b,6,d),flip(b),flip(c),flip(d)]. given #624 (T,wt=11): 6765 p(b,k) | f(k) = b | f(k) = m. [para(52(a,1),6386(b,2)),merge(b),merge(e)]. given #625 (T,wt=11): 6767 p(b,k) | f(k) = b | f(b) = m. [para(52(a,1),6765(c,1,1)),merge(b)]. given #626 (A,wt=36): 366 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(362,b,34,g),flip(d),flip(f),flip(g)]. given #627 (F,wt=7): 6798 p(b,k) | f(b) = m. [para(6767(b,1),6379(b,1)),merge(c),merge(d)]. given #628 (F,wt=6): 6799 p(b,k) | -p(b,m). [resolve(6798,b,8,c),unit_del(b,27)]. given #629 (T,wt=10): 6813 p(b,k) | p(b,b) | p(b,g(b)). [factor(6806,a,d)]. given #630 (T,wt=13): 6766 p(b,k) | f(k) = b | k = m | -p(k,m). [resolve(6765,c,8,c),flip(c)]. given #631 (A,wt=28): 367 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(362,b,4,f),flip(b),flip(d)]. given #632 (F,wt=10): 6829 p(b,k) | f(k) = b | k = m. [resolve(6766,d,6339,b),merge(d)]. given #633 (F,wt=6): 6853 p(b,k) | k = m. [para(6829(b,1),6379(b,1)),merge(c),merge(d)]. given #634 (T,wt=3): 6860 p(b,k). [para(6853(b,1),52(a,1)),merge(c),unit_del(b,27)]. given #635 (T,wt=9): 6868 p(k,j) | j = b | k = b. [resolve(6860,a,71,c)]. given #636 (A,wt=29): 368 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(362,b,4,e),flip(b),flip(d),flip(e)]. given #637 (F,wt=6): 6881 p(k,j) | k = b. [para(6868(b,1),61(a,1)),flip(c),merge(c),merge(d)]. given #638 (F,wt=6): 6889 p(k,j) | p(m,k). [para(6881(b,1),49(a,1)),flip(b),unit_del(b,27)]. given #639 (T,wt=6): 6890 p(k,j) | j = b. [para(6881(b,1),61(a,2)),merge(c)]. given #640 (T,wt=6): 6902 p(k,j) | p(b,b). [para(6881(b,1),6860(a,2))]. given #641 (A,wt=29): 369 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(362,b,2,e),flip(b),flip(d),flip(e)]. given #642 (F,wt=6): 6904 p(m,k) | p(m,j). [para(49(a,1),6889(a,1)),merge(c)]. given #643 (F,wt=10): 6870 p(x,b) | p(x,g(x)) | p(x,k). [para(20(a,1),6860(a,1))]. given #644 (T,wt=10): 6871 p(x,b) | p(g(x),x) | p(x,k). [para(22(a,1),6860(a,1))]. given #645 (T,wt=10): 6895 p(k,j) | p(j,b) | p(k,g(j)). [para(6881(b,1),1751(b,2)),merge(b),merge(d)]. given #646 (A,wt=36): 373 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(372,b,39,h),flip(d),flip(f),flip(g)]. given #647 (F,wt=10): 6897 p(k,j) | p(j,b) | p(k,g(k)). [para(6881(b,1),1797(b,2)),merge(b),merge(d)]. given #648 (F,wt=10): 6899 p(k,j) | p(k,b) | p(b,g(k)). [para(6881(b,1),1875(c,1)),merge(b)]. given #649 (T,wt=10): 6900 p(k,j) | p(k,b) | p(k,g(b)). [para(6881(b,1),1875(c,2,1)),merge(b)]. given #650 (T,wt=10): 6980 p(k,j) | p(k,b) | p(k,g(j)). [para(61(a,1),6895(b,1)),merge(b)]. given #651 (A,wt=35): 375 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(372,b,39,d),flip(d),flip(f)]. given #652 (F,wt=10): 7029 p(k,j) | p(k,b) | p(b,g(b)). [para(6881(b,1),6900(c,1)),merge(b)]. given #653 (F,wt=10): 7035 p(k,j) | p(k,b) | p(b,g(j)). [para(6881(b,1),6980(c,1)),merge(b)]. given #654 (T,wt=12): 6869 k = m | p(k,m) | k = b | -p(k,b). [resolve(6860,a,2,f),flip(a),flip(d),unit_del(c,27)]. given #655 (T,wt=12): 6888 p(k,j) | j = x | p(x,j) | b != x. [para(6881(b,1),31(c,1))]. given #656 (A,wt=36): 376 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(372,b,34,h),flip(d),flip(f),flip(g)]. given #657 (F,wt=12): 6893 p(k,j) | j = x | -p(x,b) | k = x. [para(6881(b,1),71(c,2)),merge(b)]. given #658 (F,wt=13): 6874 p(k,b) | p(g(k),k) | p(b,j) | p(b,b). [para(468(d,1),6860(a,2))]. given #659 (T,wt=13): 6875 p(k,b) | p(k,g(k)) | p(b,j) | p(b,b). [para(480(d,1),6860(a,2))]. given #660 (T,wt=13): 6886 p(x,b) | p(x,g(x)) | p(k,j) | k = x. [para(20(a,1),6881(b,2))]. given #661 (A,wt=35): 378 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(372,b,34,d),flip(d),flip(f)]. given #662 (F,wt=13): 6887 p(x,b) | p(g(x),x) | p(k,j) | k = x. [para(22(a,1),6881(b,2))]. given #663 (F,wt=13): 6896 p(k,j) | p(j,k) | p(j,b) | p(j,g(b)). [para(6881(b,1),1752(d,2,1)),merge(b)]. given #664 (T,wt=13): 6905 p(x,b) | p(x,g(x)) | p(k,j) | j = x. [para(20(a,1),6890(b,2))]. given #665 (T,wt=13): 6906 p(x,b) | p(g(x),x) | p(k,j) | j = x. [para(22(a,1),6890(b,2))]. given #666 (A,wt=29): 379 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(372,b,4,f),flip(b),flip(d),flip(e)]. given #667 (F,wt=13): 6910 p(k,j) | p(j,k) | p(j,b) | p(b,g(k)). [para(6890(b,1),1752(d,1)),merge(b)]. given #668 (F,wt=10): 7189 p(k,j) | p(j,b) | p(b,g(k)). [para(6881(b,1),6910(b,2)),merge(b),merge(d)]. given #669 (T,wt=13): 7146 p(x,b) | p(x,g(x)) | p(k,j) | p(b,x). [para(6886(d,1),6860(a,2))]. given #670 (T,wt=13): 7149 p(x,b) | p(x,g(x)) | p(k,j) | p(m,x). [factor(7145,a,e),merge(e),merge(f)]. given #671 (A,wt=20): 428 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 #672 (F,wt=13): 7150 p(j,b) | p(j,g(j)) | p(k,j) | p(k,b). [factor(7148,b,e)]. given #673 (F,wt=13): 7160 p(x,b) | p(g(x),x) | p(k,j) | p(b,x). [para(6887(d,1),6860(a,2))]. given #674 (T,wt=13): 7165 p(k,j) | p(j,k) | p(j,b) | p(k,g(b)). [para(61(a,1),6896(d,1)),merge(b)]. given #675 (T,wt=10): 7382 p(k,j) | p(j,b) | p(k,g(b)). [para(6881(b,1),7165(b,2)),merge(b),merge(d)]. given #676 (A,wt=23): 429 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 #677 (F,wt=13): 7172 p(k,j) | p(j,k) | p(j,b) | p(b,g(b)). [para(6890(b,1),6896(d,1)),merge(b)]. given #678 (F,wt=10): 7392 p(k,j) | p(j,b) | p(b,g(b)). [para(6881(b,1),7172(b,2)),merge(b),merge(d)]. given #679 (T,wt=13): 7256 p(x,b) | p(x,g(x)) | p(k,j) | p(x,x). [factor(7225,a,c),merge(c)]. given #680 (T,wt=13): 7353 p(k,j) | p(j,b) | p(j,g(k)) | p(k,b). [para(61(a,1),7150(b,2,1)),merge(d)]. given #681 (A,wt=19): 467 p(k,b) | p(g(k),k) | p(b,j) | j = x | -p(x,k) | k = x. [para(319(c,1),29(b,2))]. given #682 (F,wt=13): 7364 p(k,j) | p(j,b) | p(j,g(b)) | p(k,b). [para(6890(b,1),7150(b,2,1)),merge(d)]. given #683 (F,wt=14): 6971 p(j,b) | p(j,k) | g(j) = j | g(j) = k. [resolve(6871,b,29,b),flip(c),flip(d)]. given #684 (T,wt=13): 7474 p(j,b) | p(j,k) | g(j) = k | j = b. [resolve(6971,c,18,c),flip(d),merge(e)]. given #685 (T,wt=9): 7508 p(j,b) | p(j,k) | j = b. [para(7474(c,1),6870(b,2)),merge(d),merge(e),merge(f)]. given #686 (A,wt=32): 469 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 #687 (F,wt=9): 7513 p(j,b) | p(j,k) | j = k. [resolve(7508,c,26,b(flip)),flip(c),merge(d)]. given #688 (F,wt=9): 7545 p(j,b) | p(j,k) | k = b. [para(7513(c,1),7508(c,1)),merge(c),merge(d)]. given #689 (T,wt=9): 7553 p(j,b) | p(j,k) | p(m,b). [para(7545(c,1),2192(a,2)),merge(d)]. given #690 (T,wt=9): 7555 p(j,b) | p(j,k) | p(b,b). [para(7545(c,1),6860(a,2))]. given #691 (A,wt=32): 470 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 #692 (F,wt=10): 7544 p(j,b) | p(j,k) | g(j) = k. [para(7513(c,1),6971(c,2)),merge(c),merge(d),merge(f)]. given #693 (F,wt=6): 7620 p(j,b) | p(j,k). [para(7544(c,1),6870(b,2)),merge(c),merge(d),merge(e)]. given #694 (T,wt=6): 7640 p(k,j) | p(j,b). [para(6881(b,1),7620(b,2)),merge(c)]. given #695 (T,wt=6): 7647 p(k,j) | p(k,b). [para(61(a,1),7640(b,1)),merge(b)]. given #696 (A,wt=23): 471 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 #697 (F,wt=10): 7652 p(x,b) | p(x,g(x)) | p(k,j). [para(6905(d,1),7640(b,1)),merge(d),merge(e)]. given #698 (F,wt=10): 7653 p(x,b) | p(g(x),x) | p(k,j). [para(6906(d,1),7640(b,1)),merge(d),merge(e)]. given #699 (T,wt=10): 7669 p(b,j) | p(k,b) | p(g(k),k). [para(59(a,1),7647(a,2)),merge(d),merge(e)]. given #700 (T,wt=10): 7670 p(b,j) | p(k,b) | p(k,g(k)). [para(60(a,1),7647(a,2)),merge(d),merge(e)]. given #701 (A,wt=23): 472 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 #702 (F,wt=12): 7633 p(j,b) | j = k | j = m | j = b. [resolve(7620,b,6,d),flip(b),flip(c),flip(d)]. given #703 (F,wt=12): 7769 p(j,b) | j = m | j = b | p(k,k). [para(7633(b,1),7620(b,1)),merge(d)]. given #704 (T,wt=12): 7771 p(j,b) | j = m | j = b | k = b. [factor(7766,c,d),unit_del(d,6860)]. given #705 (T,wt=12): 7797 p(j,b) | j = b | k = b | -p(b,m). [factor(7786,b,d),merge(e)]. given #706 (A,wt=23): 473 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 #707 (F,wt=13): 7774 p(j,b) | j = b | p(k,k) | p(g(j),j). [resolve(7769,b,58,c(flip)),merge(d)]. given #708 (F,wt=13): 7775 p(j,b) | j = b | p(k,k) | p(j,g(j)). [resolve(7769,b,57,c(flip)),merge(d)]. given #709 (T,wt=13): 7784 p(j,b) | j = b | k = b | p(g(j),j). [resolve(7771,b,58,c(flip)),merge(d)]. given #710 (T,wt=13): 7785 p(j,b) | j = b | k = b | p(j,g(j)). [resolve(7771,b,57,c(flip)),merge(d)]. given #711 (A,wt=23): 474 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 #712 (F,wt=13): 7823 p(j,b) | p(k,k) | p(g(j),j) | p(k,b). [para(7774(b,1),7647(a,2)),merge(e)]. given #713 (F,wt=13): 7827 p(j,b) | p(k,k) | p(j,g(j)) | p(k,b). [para(7775(b,1),7647(a,2)),merge(e)]. given #714 (T,wt=13): 7832 p(j,b) | k = b | p(g(j),j) | p(k,b). [para(7784(b,1),7647(a,2)),merge(e)]. given #715 (T,wt=10): 7888 p(j,b) | p(g(j),j) | p(k,b). [para(7832(b,1),7620(b,2)),merge(d),merge(e)]. given #716 (A,wt=29): 475 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 #717 (F,wt=13): 7837 p(j,b) | k = b | p(j,g(j)) | p(k,b). [para(7785(b,1),7647(a,2)),merge(e)]. given #718 (F,wt=10): 7942 p(j,b) | p(j,g(j)) | p(k,b). [para(7837(b,1),7620(b,2)),merge(d),merge(e)]. given #719 (T,wt=14): 7900 p(j,b) | p(k,b) | g(j) = j | g(j) = k. [resolve(7888,b,29,b),flip(c),flip(d)]. given #720 (T,wt=13): 7980 p(j,b) | p(k,b) | g(j) = k | j = b. [resolve(7900,c,18,c),flip(d),merge(e)]. given #721 (A,wt=29): 476 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 #722 (F,wt=12): 7994 p(j,b) | p(k,b) | j = b | k != b. [para(7980(c,1),16(c,1)),flip(d),merge(d),merge(e)]. given #723 (F,wt=12): 7995 p(j,b) | p(k,b) | j = b | j != k. [para(7980(c,1),18(c,1)),flip(d),flip(f),merge(d),merge(e)]. given #724 (T,wt=12): 8012 p(j,b) | p(k,b) | j = b | j = m. [resolve(7995,d,7633,b),merge(d),merge(f)]. given #725 (T,wt=12): 8021 p(j,b) | p(k,b) | j = b | p(k,m). [para(8012(d,1),7647(a,2)),merge(e)]. given #726 (A,wt=29): 477 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 #727 (F,wt=9): 8038 p(j,b) | p(k,b) | p(k,m). [para(8021(c,1),7647(a,2)),merge(d),merge(e)]. given #728 (F,wt=12): 8027 p(j,b) | p(k,b) | j = b | k != m. [para(8012(d,1),7995(d,1)),flip(g),merge(d),merge(e),merge(f)]. given #729 (T,wt=13): 7989 p(j,b) | p(k,b) | g(j) = k | p(j,j). [para(7900(c,1),7888(b,1)),merge(d),merge(f)]. given #730 (T,wt=13): 7992 p(j,b) | p(k,b) | j = b | p(g(k),k). [resolve(7980,c,40,e),flip(f),merge(d),merge(f),merge(g)]. given #731 (A,wt=29): 478 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 #732 (F,wt=10): 8079 p(j,b) | p(k,b) | p(g(k),k). [para(7992(c,1),7647(a,2)),merge(d),merge(e)]. given #733 (F,wt=13): 7993 p(j,b) | p(k,b) | j = b | p(k,g(k)). [resolve(7980,c,35,e),flip(f),merge(d),merge(f),merge(g)]. given #734 (T,wt=10): 8108 p(j,b) | p(k,b) | p(k,g(k)). [para(7993(c,1),7647(a,2)),merge(d),merge(e)]. given #735 (T,wt=10): 8124 p(k,b) | p(k,g(k)) | p(j,k). [factor(8116,a,d),merge(d)]. given #736 (A,wt=41): 619 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(610,c,e),flip(g)]. given #737 (F,wt=13): 8022 p(j,b) | p(k,b) | j = b | p(g(m),j). [para(8012(d,1),7888(b,1,1)),merge(d),merge(f)]. given #738 (F,wt=10): 8164 p(j,b) | p(k,b) | p(g(m),j). [para(8022(c,1),7647(a,2)),merge(d),merge(e)]. given #739 (T,wt=13): 8023 p(j,b) | p(k,b) | j = b | p(g(j),m). [para(8012(d,1),7888(b,2)),merge(d),merge(f)]. given #740 (T,wt=10): 8198 p(j,b) | p(k,b) | p(g(j),m). [para(8023(c,1),7647(a,2)),merge(d),merge(e)]. given #741 (A,wt=26): 791 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(78,d,31,c(flip))]. given #742 (F,wt=13): 8024 p(j,b) | p(k,b) | j = b | p(m,g(j)). [para(8012(d,1),7942(b,1)),merge(d),merge(f)]. given #743 (F,wt=10): 8262 p(j,b) | p(k,b) | p(m,g(j)). [para(8024(c,1),7647(a,2)),merge(d),merge(e)]. given #744 (T,wt=13): 8025 p(j,b) | p(k,b) | j = b | p(j,g(m)). [para(8012(d,1),7942(b,2,1)),merge(d),merge(f)]. given #745 (T,wt=10): 8293 p(j,b) | p(k,b) | p(j,g(m)). [para(8025(c,1),7647(a,2)),merge(d),merge(e)]. given #746 (A,wt=20): 792 p(g(g(m)),b) | p(g(g(m)),g(g(g(m)))) | p(g(m),b) | p(m,b). [resolve(78,d,27,a(flip))]. given #747 (F,wt=13): 8026 p(j,b) | p(k,b) | j = b | g(m) = k. [para(8012(d,1),7980(c,1,1)),merge(d),merge(e),merge(g)]. given #748 (F,wt=13): 8060 p(k,b) | p(g(k),k) | p(j,k) | p(k,m). [factor(8050,a,d)]. given #749 (T,wt=13): 8183 p(j,b) | p(k,b) | j = b | p(g(m),m). [para(8012(d,1),8164(c,2)),merge(d),merge(e)]. given #750 (T,wt=10): 8365 p(j,b) | p(k,b) | p(g(m),m). [para(8183(c,1),7647(a,2)),merge(d),merge(e)]. given #751 (A,wt=31): 793 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(78,d,16,c(flip))]. given #752 (F,wt=13): 8225 p(j,b) | p(k,b) | g(j) = k | p(j,m). [para(7900(c,1),8198(c,1)),merge(d),merge(e)]. given #753 (F,wt=13): 8313 p(j,b) | p(k,b) | j = b | p(m,g(m)). [para(8012(d,1),8293(c,1)),merge(d),merge(e)]. given #754 (T,wt=10): 8488 p(j,b) | p(k,b) | p(m,g(m)). [para(8313(c,1),7647(a,2)),merge(d),merge(e)]. given #755 (T,wt=14): 8177 p(j,b) | p(k,b) | g(m) = j | g(m) = k. [resolve(8164,c,29,b),flip(c),flip(d)]. given #756 (A,wt=28): 794 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(78,d,10,c(flip)),unit_del(e,27)]. given #757 (F,wt=13): 8535 p(j,b) | p(k,b) | g(m) = k | p(j,j). [para(8177(c,1),8164(c,1)),merge(d),merge(e)]. given #758 (F,wt=13): 8538 p(j,b) | p(k,b) | g(m) = k | p(j,m). [para(8177(c,1),8365(c,1)),merge(d),merge(e)]. given #759 (T,wt=14): 8278 p(k,b) | p(g(k),k) | p(j,k) | p(m,g(j)). [factor(8271,a,d)]. given #760 (T,wt=14): 8505 p(k,b) | p(g(k),k) | p(j,k) | p(m,g(m)). [factor(8497,a,d)]. given #761 (A,wt=38): 795 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(78(d,1),4(b,2))]. given #762 (F,wt=15): 6885 p(k,j) | k = x | m = x | b = x | -p(x,b). [para(6881(b,1),6(d,2))]. given #763 (F,wt=15): 6903 p(m,k) | k = b | j = b | j = k | -p(j,k). [resolve(6889,a,2189,e),flip(d),flip(e),merge(b)]. given #764 (T,wt=15): 6948 p(m,k) | j = b | -p(j,b) | j = m | -p(j,m). [resolve(6904,b,4,f),flip(b),flip(d),flip(e),unit_del(d,27)]. given #765 (T,wt=15): 6949 p(m,k) | -p(m,b) | j = b | j = m | -p(j,m). [resolve(6904,b,4,e),flip(b),flip(d),unit_del(b,27)]. given #766 (A,wt=30): 796 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(78(d,1),16(c,2))]. given #767 (F,wt=15): 7770 p(j,b) | j = m | j = b | -p(m,k) | k = m. [factor(7766,b,d)]. given #768 (F,wt=15): 7777 p(j,b) | j = b | p(k,k) | p(k,m) | p(m,b). [para(7769(b,1),3131(a,2))]. given #769 (T,wt=15): 7778 p(j,b) | j = b | p(k,k) | p(k,m) | p(b,b). [para(7769(b,1),6902(a,2))]. given #770 (T,wt=15): 7788 p(j,b) | j = b | k = b | p(k,m) | p(m,b). [para(7771(b,1),3131(a,2))]. given #771 (A,wt=30): 797 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(78(d,1),20(a,1))]. given #772 (F,wt=15): 7789 p(j,b) | j = b | k = b | p(b,m) | p(k,m). [para(7771(b,1),3561(b,2))]. given #773 (F,wt=15): 7793 p(j,b) | j = b | k = b | p(k,m) | p(b,b). [para(7771(b,1),6902(a,2))]. given #774 (T,wt=15): 8557 p(j,b) | p(k,b) | p(j,j) | p(m,b) | k != b. [para(8535(c,1),16(c,1)),flip(d),unit_del(d,27)]. given #775 (T,wt=15): 8558 p(j,b) | p(k,b) | p(j,j) | p(m,b) | k != m. [para(8535(c,1),18(c,1)),flip(d),unit_del(d,27)]. given #776 (A,wt=30): 798 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),78(d,1))]. given #777 (F,wt=15): 8579 p(j,b) | p(k,b) | p(j,m) | p(m,b) | k != b. [para(8538(c,1),16(c,1)),flip(d),unit_del(d,27)]. given #778 (F,wt=15): 8580 p(j,b) | p(k,b) | p(j,m) | p(m,b) | k != m. [para(8538(c,1),18(c,1)),flip(d),unit_del(d,27)]. given #779 (T,wt=15): 8724 p(m,k) | k = b | j = b | j = k | -p(j,m). [para(49(a,1),6903(e,2)),merge(b)]. given #780 (T,wt=15): 8738 p(j,b) | j = m | j = b | k = m | p(b,m). [resolve(7770,d,3448,a)]. given #781 (A,wt=30): 799 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(78(d,1),22(a,1))]. given #782 (F,wt=15): 8740 p(j,b) | j = m | j = b | k = m | p(m,b). [resolve(7770,d,2192,a)]. given #783 (F,wt=15): 8807 p(j,b) | j = b | k = m | p(b,m) | p(k,m). [para(8738(b,1),3561(b,2)),merge(e)]. given #784 (T,wt=15): 8819 p(j,b) | j = b | k = m | p(m,b) | p(k,m). [para(8740(b,1),3131(a,2)),merge(f)]. given #785 (T,wt=16): 6872 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k). [para(32(c,1),6860(a,1))]. given #786 (A,wt=30): 800 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),78(d,1))]. given #787 (F,wt=16): 6873 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(x,k). [para(37(c,1),6860(a,1))]. given #788 (F,wt=16): 7671 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(b,j). [para(76(d,1),7647(a,2)),merge(e),merge(f)]. given #789 (T,wt=16): 7673 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | p(b,j). [para(194(d,1),7647(a,2)),merge(e),merge(f)]. given #790 (T,wt=16): 8049 p(x,b) | p(x,g(x)) | p(j,x) | p(k,b) | p(k,m). [para(20(a,1),8038(a,2))]. given #791 (A,wt=29): 801 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(78(d,1),26(b,1))]. given #792 (F,wt=16): 8050 p(x,b) | p(g(x),x) | p(j,x) | p(k,b) | p(k,m). [para(22(a,1),8038(a,2))]. given #793 (F,wt=16): 8139 p(k,b) | p(k,g(k)) | j = k | j = m | j = b. [resolve(8124,c,6,d),flip(c),flip(d),flip(e)]. given #794 (T,wt=13): 8968 p(k,b) | p(k,g(k)) | j = m | j = b. [para(8139(c,1),8108(a,1)),merge(e),merge(f),merge(g)]. given #795 (T,wt=13): 8973 p(k,b) | p(k,g(k)) | j = b | p(k,m). [para(8968(c,1),7647(a,2)),merge(e)]. given #796 (A,wt=23): 802 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | m != x. [para(78(d,1),27(a,2))]. given #797 (F,wt=10): 8986 p(k,b) | p(k,g(k)) | p(k,m). [para(8973(c,1),7647(a,2)),merge(d),merge(e)]. given #798 (F,wt=13): 8974 p(k,b) | p(k,g(k)) | j = b | p(m,b). [para(8968(c,1),8108(a,1)),merge(e),merge(f)]. given #799 (T,wt=10): 9017 p(k,b) | p(k,g(k)) | p(m,b). [para(8974(c,1),3131(a,2)),merge(d),merge(e)]. given #800 (T,wt=16): 8219 p(j,b) | p(k,b) | g(j) = m | p(f(g(j)),g(j)). [resolve(8198,c,14,b),flip(c)]. given #801 (A,wt=36): 804 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(78(d,1),32(c,1))]. given #802 (F,wt=15): 9044 p(j,b) | p(k,b) | p(f(g(j)),g(j)) | p(m,j). [para(8219(c,1),7888(b,1)),merge(d),merge(f)]. given #803 (F,wt=15): 9045 p(j,b) | p(k,b) | p(f(g(j)),g(j)) | p(j,m). [para(8219(c,1),7942(b,2)),merge(d),merge(f)]. given #804 (T,wt=14): 9137 p(j,b) | p(k,b) | p(j,m) | p(f(k),g(j)). [para(8225(c,1),9045(c,1,1)),merge(d),merge(e),merge(g)]. given #805 (T,wt=13): 9173 p(j,b) | p(k,b) | p(j,m) | p(f(k),k). [para(8225(c,1),9137(d,2)),merge(d),merge(e),merge(f)]. given #806 (A,wt=36): 805 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),78(d,1))]. given #807 (F,wt=14): 9138 p(j,b) | p(k,b) | p(j,m) | p(f(g(j)),k). [para(8225(c,1),9045(c,2)),merge(d),merge(e),merge(g)]. given #808 (F,wt=15): 9050 p(j,b) | p(k,b) | p(f(g(j)),g(j)) | p(m,m). [para(8219(c,1),8198(c,1)),merge(d),merge(e)]. given #809 (T,wt=16): 8220 p(j,b) | p(k,b) | g(j) = m | p(g(j),f(g(j))). [resolve(8198,c,12,b),flip(c)]. given #810 (T,wt=15): 9308 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(m,j). [para(8220(c,1),7888(b,1)),merge(d),merge(f)]. given #811 (A,wt=33): 807 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(78(d,1),33(c,1))]. given #812 (F,wt=15): 9309 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(j,m). [para(8220(c,1),7942(b,2)),merge(d),merge(f)]. given #813 (F,wt=14): 9395 p(j,b) | p(k,b) | p(j,m) | p(k,f(g(j))). [para(8225(c,1),9309(c,1)),merge(d),merge(e),merge(g)]. given #814 (T,wt=14): 9396 p(j,b) | p(k,b) | p(j,m) | p(g(j),f(k)). [para(8225(c,1),9309(c,2,1)),merge(d),merge(e),merge(g)]. given #815 (T,wt=13): 9435 p(j,b) | p(k,b) | p(j,m) | p(k,f(k)). [para(8225(c,1),9396(d,1)),merge(d),merge(e),merge(f)]. given #816 (A,wt=36): 811 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(78(d,1),37(c,1))]. given #817 (F,wt=15): 9314 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(m,m). [para(8220(c,1),8198(c,1)),merge(d),merge(e)]. given #818 (F,wt=16): 8386 p(j,b) | p(k,b) | g(m) = m | p(f(g(m)),g(m)). [resolve(8365,c,14,b),flip(c)]. given #819 (T,wt=15): 9509 p(j,b) | p(k,b) | p(f(g(m)),g(m)) | p(m,j). [para(8386(c,1),8164(c,1)),merge(d),merge(e)]. given #820 (T,wt=15): 9510 p(j,b) | p(k,b) | p(f(g(m)),g(m)) | p(j,m). [para(8386(c,1),8293(c,2)),merge(d),merge(e)]. given #821 (A,wt=36): 812 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),78(d,1))]. given #822 (F,wt=14): 9578 p(j,b) | p(k,b) | p(j,m) | p(f(k),g(m)). [para(8538(c,1),9510(c,1,1)),merge(d),merge(e),merge(g)]. given #823 (F,wt=14): 9579 p(j,b) | p(k,b) | p(j,m) | p(f(g(m)),k). [para(8538(c,1),9510(c,2)),merge(d),merge(e),merge(g)]. given #824 (T,wt=15): 9512 p(j,b) | p(k,b) | p(f(g(m)),g(m)) | p(m,m). [para(8386(c,1),8365(c,1)),merge(d),merge(e)]. given #825 (T,wt=16): 8387 p(j,b) | p(k,b) | g(m) = m | p(g(m),f(g(m))). [resolve(8365,c,12,b),flip(c)]. given #826 (A,wt=33): 813 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(78(d,1),38(c,1))]. given #827 (F,wt=15): 9702 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(m,j). [para(8387(c,1),8164(c,1)),merge(d),merge(e)]. given #828 (F,wt=15): 9703 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(j,m). [para(8387(c,1),8293(c,2)),merge(d),merge(e)]. given #829 (T,wt=14): 9774 p(j,b) | p(k,b) | p(j,m) | p(k,f(g(m))). [para(8538(c,1),9703(c,1)),merge(d),merge(e),merge(g)]. given #830 (T,wt=14): 9775 p(j,b) | p(k,b) | p(j,m) | p(g(m),f(k)). [para(8538(c,1),9703(c,2,1)),merge(d),merge(e),merge(g)]. given #831 (A,wt=43): 830 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(78(d,1),78(d,1))]. given #832 (F,wt=15): 9705 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(m,m). [para(8387(c,1),8365(c,1)),merge(d),merge(e)]. given #833 (F,wt=16): 8515 p(j,b) | p(k,b) | g(m) = k | p(m,b) | j != b. [para(8177(c,1),16(c,1)),flip(d),unit_del(d,27)]. given #834 (T,wt=16): 8516 p(j,b) | p(k,b) | g(m) = k | p(m,b) | j != m. [para(8177(c,1),18(c,1)),flip(d),unit_del(d,27)]. given #835 (T,wt=16): 8518 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(m,j). [para(8177(c,1),56(b,2))]. given #836 (A,wt=31): 832 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(796,a,f),flip(e)]. given #837 (F,wt=15): 9878 p(j,b) | p(k,b) | p(m,b) | p(m,j) | k != b. [para(8518(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #838 (F,wt=15): 9879 p(j,b) | p(k,b) | p(m,b) | p(m,j) | k != m. [para(8518(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #839 (T,wt=16): 8803 p(j,b) | j = b | k = m | p(b,m) | p(g(j),j). [resolve(8738,b,58,c(flip)),merge(e)]. given #840 (T,wt=16): 8804 p(j,b) | j = b | k = m | p(b,m) | p(j,g(j)). [resolve(8738,b,57,c(flip)),merge(e)]. given #841 (A,wt=29): 833 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(796,c,f),flip(e)]. given #842 (F,wt=16): 8816 p(j,b) | j = b | k = m | p(m,b) | p(g(j),j). [resolve(8740,b,58,c(flip)),merge(e)]. given #843 (F,wt=16): 8817 p(j,b) | j = b | k = m | p(m,b) | p(j,g(j)). [resolve(8740,b,57,c(flip)),merge(e)]. given #844 (T,wt=16): 8975 p(k,b) | p(k,g(k)) | j = b | -p(b,m) | k = b. [factor(8969,c,d)]. given #845 (T,wt=16): 9450 p(j,b) | p(k,b) | j = b | p(m,m) | p(k,f(k)). [para(8012(d,1),9435(c,1)),merge(d),merge(e)]. given #846 (A,wt=25): 834 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(797,a,f),flip(e),merge(f)]. given #847 (F,wt=13): 9942 p(j,b) | p(k,b) | p(m,m) | p(k,f(k)). [para(9450(c,1),7647(a,2)),merge(e),merge(f)]. given #848 (F,wt=16): 9930 p(k,b) | p(k,g(k)) | j = b | -p(k,m) | k = b. [factor(9923,a,c),merge(c)]. given #849 (T,wt=17): 8116 p(x,b) | p(x,g(x)) | p(j,x) | p(k,b) | p(k,g(k)). [para(20(a,1),8108(a,2))]. given #850 (T,wt=17): 8117 p(x,b) | p(g(x),x) | p(j,x) | p(k,b) | p(k,g(k)). [para(22(a,1),8108(a,2))]. given #851 (A,wt=24): 835 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | p(x,b) | g(x) = x. [factor(804,a,e),flip(f),merge(e),merge(g)]. given #852 (F,wt=17): 8121 p(k,b) | p(k,g(k)) | p(x,b) | p(x,g(x)) | p(x,j). [para(167(e,1),8108(a,1)),merge(f),merge(g),merge(h)]. given #853 (F,wt=17): 8123 p(x,b) | p(g(x),x) | p(k,b) | p(k,g(k)) | p(x,j). [para(360(e,1),8108(a,1)),merge(f),merge(g),merge(h)]. given #854 (T,wt=17): 8270 p(x,b) | p(x,g(x)) | p(j,x) | p(k,b) | p(m,g(j)). [para(20(a,1),8262(a,2))]. given #855 (T,wt=17): 8271 p(x,b) | p(g(x),x) | p(j,x) | p(k,b) | p(m,g(j)). [para(22(a,1),8262(a,2))]. given #856 (A,wt=27): 884 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),79(d,1))]. given #857 (F,wt=17): 8333 p(j,b) | p(k,b) | j = b | p(m,b) | p(f(k),g(m)). [para(8026(d,1),362(b,1,1))]. given #858 (F,wt=14): 10168 p(j,b) | p(k,b) | p(m,b) | p(f(k),g(m)). [para(8333(c,1),3131(a,2)),merge(e),merge(f)]. given #859 (T,wt=16): 10184 p(j,b) | p(k,b) | j = b | p(m,b) | p(f(k),k). [para(8026(d,1),10168(d,2)),merge(d),merge(e)]. given #860 (T,wt=13): 10213 p(j,b) | p(k,b) | p(m,b) | p(f(k),k). [para(10184(c,1),3131(a,2)),merge(e),merge(f)]. given #861 (A,wt=27): 885 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),79(d,1))]. given #862 (F,wt=17): 8334 p(j,b) | p(k,b) | j = b | p(m,b) | p(f(g(m)),k). [para(8026(d,1),362(b,2))]. given #863 (F,wt=14): 10257 p(j,b) | p(k,b) | p(m,b) | p(f(g(m)),k). [para(8334(c,1),3131(a,2)),merge(e),merge(f)]. given #864 (T,wt=17): 8335 p(j,b) | p(k,b) | j = b | p(m,b) | p(k,f(g(m))). [para(8026(d,1),372(b,1))]. given #865 (T,wt=14): 10300 p(j,b) | p(k,b) | p(m,b) | p(k,f(g(m))). [para(8335(c,1),3131(a,2)),merge(e),merge(f)]. given #866 (A,wt=33): 886 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),79(d,1))]. given #867 (F,wt=17): 8336 p(j,b) | p(k,b) | j = b | p(m,b) | p(g(m),f(k)). [para(8026(d,1),372(b,2,1))]. given #868 (F,wt=14): 10334 p(j,b) | p(k,b) | p(m,b) | p(g(m),f(k)). [para(8336(c,1),3131(a,2)),merge(e),merge(f)]. given #869 (T,wt=16): 10355 p(j,b) | p(k,b) | j = b | p(m,b) | p(k,f(k)). [para(8026(d,1),10334(d,1)),merge(d),merge(e)]. given #870 (T,wt=13): 10379 p(j,b) | p(k,b) | p(m,b) | p(k,f(k)). [para(10355(c,1),3131(a,2)),merge(e),merge(f)]. given #871 (A,wt=33): 887 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),79(d,1))]. given #872 (F,wt=17): 8496 p(x,b) | p(x,g(x)) | p(j,x) | p(k,b) | p(m,g(m)). [para(20(a,1),8488(a,2))]. given #873 (F,wt=17): 8497 p(x,b) | p(g(x),x) | p(j,x) | p(k,b) | p(m,g(m)). [para(22(a,1),8488(a,2))]. given #874 (T,wt=17): 9086 p(j,b) | p(k,b) | j = b | p(f(k),g(j)) | p(m,j). [para(7980(c,1),9044(c,1,1)),merge(d),merge(e)]. given #875 (T,wt=14): 10473 p(j,b) | p(k,b) | p(f(k),g(j)) | p(m,j). [para(9086(c,1),7647(a,2)),merge(e),merge(f)]. given #876 (A,wt=40): 888 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(78(d,1),79(d,1))]. given #877 (F,wt=16): 10495 p(j,b) | p(k,b) | j = b | p(f(k),k) | p(m,j). [para(7980(c,1),10473(c,2)),merge(d),merge(e)]. given #878 (F,wt=13): 10524 p(j,b) | p(k,b) | p(f(k),k) | p(m,j). [para(10495(c,1),7647(a,2)),merge(e),merge(f)]. given #879 (T,wt=17): 9087 p(j,b) | p(k,b) | j = b | p(f(g(j)),k) | p(m,j). [para(7980(c,1),9044(c,2)),merge(d),merge(e)]. given #880 (T,wt=14): 10568 p(j,b) | p(k,b) | p(f(g(j)),k) | p(m,j). [para(9087(c,1),7647(a,2)),merge(e),merge(f)]. given #881 (A,wt=22): 889 p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(g(f(b)),m). [factor(884,a,c),merge(c)]. given #882 (F,wt=17): 9276 p(j,b) | p(k,b) | j = b | p(f(k),g(j)) | p(m,m). [para(7980(c,1),9050(c,1,1)),merge(d),merge(e)]. given #883 (F,wt=14): 10628 p(j,b) | p(k,b) | p(f(k),g(j)) | p(m,m). [para(9276(c,1),7647(a,2)),merge(e),merge(f)]. given #884 (T,wt=16): 10650 p(j,b) | p(k,b) | j = b | p(f(k),k) | p(m,m). [para(7980(c,1),10628(c,2)),merge(d),merge(e)]. given #885 (T,wt=13): 10677 p(j,b) | p(k,b) | p(f(k),k) | p(m,m). [para(10650(c,1),7647(a,2)),merge(e),merge(f)]. given #886 (A,wt=21): 890 p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(f(b),m). [factor(886,a,d),merge(d),merge(e)]. given #887 (F,wt=17): 9277 p(j,b) | p(k,b) | j = b | p(f(g(j)),k) | p(m,m). [para(7980(c,1),9050(c,2)),merge(d),merge(e)]. given #888 (F,wt=14): 10731 p(j,b) | p(k,b) | p(f(g(j)),k) | p(m,m). [para(9277(c,1),7647(a,2)),merge(e),merge(f)]. given #889 (T,wt=17): 9343 p(j,b) | p(k,b) | j = b | p(k,f(g(j))) | p(m,j). [para(7980(c,1),9308(c,1)),merge(d),merge(e)]. given #890 (T,wt=14): 10779 p(j,b) | p(k,b) | p(k,f(g(j))) | p(m,j). [para(9343(c,1),7647(a,2)),merge(e),merge(f)]. given #891 (A,wt=21): 911 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),106(c,1,1))]. given #892 (F,wt=17): 9344 p(j,b) | p(k,b) | j = b | p(g(j),f(k)) | p(m,j). [para(7980(c,1),9308(c,2,1)),merge(d),merge(e)]. given #893 (F,wt=14): 10813 p(j,b) | p(k,b) | p(g(j),f(k)) | p(m,j). [para(9344(c,1),7647(a,2)),merge(e),merge(f)]. given #894 (T,wt=16): 10835 p(j,b) | p(k,b) | j = b | p(k,f(k)) | p(m,j). [para(7980(c,1),10813(c,1)),merge(d),merge(e)]. given #895 (T,wt=13): 10859 p(j,b) | p(k,b) | p(k,f(k)) | p(m,j). [para(10835(c,1),7647(a,2)),merge(e),merge(f)]. given #896 (A,wt=21): 912 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),106(c,1,1))]. given #897 (F,wt=17): 9411 p(j,b) | p(k,b) | j = b | p(m,m) | p(k,f(g(j))). [para(8012(d,1),9395(c,1)),merge(d),merge(e)]. given #898 (F,wt=14): 10894 p(j,b) | p(k,b) | p(m,m) | p(k,f(g(j))). [para(9411(c,1),7647(a,2)),merge(e),merge(f)]. given #899 (T,wt=17): 9446 p(j,b) | p(k,b) | p(k,f(k)) | j = m | p(f(j),j). [resolve(9435,c,14,b),flip(d)]. given #900 (T,wt=17): 9447 p(j,b) | p(k,b) | p(k,f(k)) | j = m | p(j,f(j)). [resolve(9435,c,12,b),flip(d)]. given #901 (A,wt=27): 913 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),106(c,1,1))]. given #902 (F,wt=17): 9484 p(j,b) | p(k,b) | j = b | p(g(j),f(k)) | p(m,m). [para(7980(c,1),9314(c,2,1)),merge(d),merge(e)]. given #903 (F,wt=14): 10947 p(j,b) | p(k,b) | p(g(j),f(k)) | p(m,m). [para(9484(c,1),7647(a,2)),merge(e),merge(f)]. given #904 (T,wt=17): 9533 p(j,b) | p(k,b) | j = b | p(f(k),g(m)) | p(m,j). [para(8026(d,1),9509(c,1,1)),merge(d),merge(e)]. given #905 (T,wt=14): 10991 p(j,b) | p(k,b) | p(f(k),g(m)) | p(m,j). [para(9533(c,1),7647(a,2)),merge(e),merge(f)]. given #906 (A,wt=27): 914 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),106(c,1,1))]. given #907 (F,wt=17): 9534 p(j,b) | p(k,b) | j = b | p(f(g(m)),k) | p(m,j). [para(8026(d,1),9509(c,2)),merge(d),merge(e)]. given #908 (F,wt=14): 11037 p(j,b) | p(k,b) | p(f(g(m)),k) | p(m,j). [para(9534(c,1),7647(a,2)),merge(e),merge(f)]. given #909 (T,wt=17): 9673 p(j,b) | p(k,b) | j = b | p(f(k),g(m)) | p(m,m). [para(8026(d,1),9512(c,1,1)),merge(d),merge(e)]. given #910 (T,wt=14): 11081 p(j,b) | p(k,b) | p(f(k),g(m)) | p(m,m). [para(9673(c,1),7647(a,2)),merge(e),merge(f)]. given #911 (A,wt=34): 915 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(78(d,1),106(c,1,1))]. given #912 (F,wt=17): 9674 p(j,b) | p(k,b) | j = b | p(f(g(m)),k) | p(m,m). [para(8026(d,1),9512(c,2)),merge(d),merge(e)]. given #913 (F,wt=14): 11127 p(j,b) | p(k,b) | p(f(g(m)),k) | p(m,m). [para(9674(c,1),7647(a,2)),merge(e),merge(f)]. given #914 (T,wt=17): 9728 p(j,b) | p(k,b) | j = b | p(k,f(g(m))) | p(m,j). [para(8026(d,1),9702(c,1)),merge(d),merge(e)]. given #915 (T,wt=14): 11171 p(j,b) | p(k,b) | p(k,f(g(m))) | p(m,j). [para(9728(c,1),7647(a,2)),merge(e),merge(f)]. given #916 (A,wt=21): 917 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),233(c,1,1))]. given #917 (F,wt=17): 9729 p(j,b) | p(k,b) | j = b | p(g(m),f(k)) | p(m,j). [para(8026(d,1),9702(c,2,1)),merge(d),merge(e)]. given #918 (F,wt=14): 11204 p(j,b) | p(k,b) | p(g(m),f(k)) | p(m,j). [para(9729(c,1),7647(a,2)),merge(e),merge(f)]. given #919 (T,wt=17): 9793 p(j,b) | p(k,b) | j = b | p(m,m) | p(k,f(g(m))). [para(8012(d,1),9774(c,1)),merge(d),merge(e)]. given #920 (T,wt=14): 11250 p(j,b) | p(k,b) | p(m,m) | p(k,f(g(m))). [para(9793(c,1),7647(a,2)),merge(e),merge(f)]. given #921 (A,wt=21): 918 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),233(c,1,1))]. given #922 (F,wt=17): 9847 p(j,b) | p(k,b) | j = b | p(g(m),f(k)) | p(m,m). [para(8026(d,1),9705(c,2,1)),merge(d),merge(e)]. given #923 (F,wt=14): 11283 p(j,b) | p(k,b) | p(g(m),f(k)) | p(m,m). [para(9847(c,1),7647(a,2)),merge(e),merge(f)]. given #924 (T,wt=17): 9965 p(k,b) | p(g(k),k) | p(j,k) | p(m,m) | p(k,f(k)). [factor(9957,a,d)]. given #925 (T,wt=17): 10185 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(f(k),j). [para(8177(c,1),10168(d,2)),merge(d),merge(e)]. given #926 (A,wt=27): 919 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),233(c,1,1))]. given #927 (F,wt=16): 11336 p(j,b) | p(k,b) | p(m,b) | p(f(k),j) | k != b. [para(10185(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #928 (F,wt=16): 11337 p(j,b) | p(k,b) | p(m,b) | p(f(k),j) | k != m. [para(10185(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #929 (T,wt=17): 10274 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(f(j),k). [para(8177(c,1),10257(d,1,1)),merge(d),merge(e)]. given #930 (T,wt=16): 11365 p(j,b) | p(k,b) | p(m,b) | p(f(j),k) | k != b. [para(10274(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #931 (A,wt=27): 920 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),233(c,1,1))]. given #932 (F,wt=16): 11366 p(j,b) | p(k,b) | p(m,b) | p(f(j),k) | k != m. [para(10274(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #933 (F,wt=17): 10356 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(j,f(k)). [para(8177(c,1),10334(d,1)),merge(d),merge(e)]. given #934 (T,wt=16): 11394 p(j,b) | p(k,b) | p(m,b) | p(j,f(k)) | k != b. [para(10356(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #935 (T,wt=16): 11395 p(j,b) | p(k,b) | p(m,b) | p(j,f(k)) | k != m. [para(10356(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #936 (A,wt=34): 921 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(78(d,1),233(c,1,1))]. given #937 (F,wt=17): 10397 p(k,b) | p(g(k),k) | p(j,k) | p(m,b) | p(k,f(k)). [factor(10389,a,d)]. given #938 (F,wt=17): 10494 p(j,b) | p(k,b) | g(j) = k | p(f(k),j) | p(m,j). [para(7900(c,1),10473(c,2)),merge(d),merge(e)]. given #939 (T,wt=17): 10587 p(j,b) | p(k,b) | g(j) = k | p(f(j),k) | p(m,j). [para(7900(c,1),10568(c,1,1)),merge(d),merge(e)]. given #940 (T,wt=17): 10649 p(j,b) | p(k,b) | g(j) = k | p(f(k),j) | p(m,m). [para(7900(c,1),10628(c,2)),merge(d),merge(e)]. given #941 (A,wt=43): 938 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(80,e,372,b),flip(d),flip(f)]. given #942 (F,wt=17): 10750 p(j,b) | p(k,b) | g(j) = k | p(f(j),k) | p(m,m). [para(7900(c,1),10731(c,1,1)),merge(d),merge(e)]. given #943 (F,wt=17): 10834 p(j,b) | p(k,b) | g(j) = k | p(j,f(k)) | p(m,j). [para(7900(c,1),10813(c,1)),merge(d),merge(e)]. given #944 (T,wt=17): 10877 p(k,b) | p(g(k),k) | p(j,k) | p(k,f(k)) | p(m,j). [factor(10869,a,d)]. given #945 (T,wt=17): 10968 p(j,b) | p(k,b) | g(j) = k | p(j,f(k)) | p(m,m). [para(7900(c,1),10947(c,1)),merge(d),merge(e)]. given #946 (A,wt=41): 971 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(80,h,372,b),flip(d),flip(f)]. given #947 (F,wt=17): 11010 p(j,b) | p(k,b) | g(m) = k | p(f(k),j) | p(m,j). [para(8177(c,1),10991(c,2)),merge(d),merge(e)]. given #948 (F,wt=17): 11054 p(j,b) | p(k,b) | g(m) = k | p(f(j),k) | p(m,j). [para(8177(c,1),11037(c,1,1)),merge(d),merge(e)]. given #949 (T,wt=17): 11100 p(j,b) | p(k,b) | g(m) = k | p(f(k),j) | p(m,m). [para(8177(c,1),11081(c,2)),merge(d),merge(e)]. given #950 (T,wt=17): 11144 p(j,b) | p(k,b) | g(m) = k | p(f(j),k) | p(m,m). [para(8177(c,1),11127(c,1,1)),merge(d),merge(e)]. given #951 (A,wt=42): 972 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(80,h,362,b),flip(d),flip(f),flip(g)]. given #952 (F,wt=17): 11223 p(j,b) | p(k,b) | g(m) = k | p(j,f(k)) | p(m,j). [para(8177(c,1),11204(c,1)),merge(d),merge(e)]. given #953 (F,wt=17): 11302 p(j,b) | p(k,b) | g(m) = k | p(j,f(k)) | p(m,m). [para(8177(c,1),11283(c,1)),merge(d),merge(e)]. given #954 (T,wt=18): 5304 p(m,k) | j = b | b = x | j = x | -p(j,x) | -p(x,j). [resolve(5299,b,4,b),flip(b),flip(d)]. given #955 (T,wt=12): 11547 p(m,k) | j = b | j = m | -p(j,m). [resolve(5304,f,6904,b),flip(c),merge(f),unit_del(c,27)]. given #956 (A,wt=46): 975 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(80,h,195,b),flip(d),flip(f),flip(g)]. given #957 (F,wt=18): 5358 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(f(f(b))))),m). [factor(5352,a,c),merge(c)]. given #958 (F,wt=18): 5365 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(f(f(b))))),m). [factor(5360,a,c),merge(c)]. given #959 (T,wt=18): 6095 p(m,k) | k = b | b = x | k = x | -p(m,x) | -p(x,k). [para(49(a,1),2189(e,1)),merge(b)]. given #960 (T,wt=18): 6096 p(m,k) | k = b | b = x | k = x | -p(k,x) | -p(x,m). [para(49(a,1),2189(f,2)),merge(b)]. given #961 (A,wt=45): 989 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(80,h,77,b),flip(d),flip(f)]. given #962 (F,wt=18): 6182 p(b,m) | k = b | -p(k,b) | j = b | j = k | p(j,b). [resolve(3582,f,5694,b),merge(g)]. given #963 (F,wt=18): 6185 p(b,m) | j = m | p(j,m) | k = m | j = k | p(j,b). [resolve(3583,f,5694,b),merge(g)]. given #964 (T,wt=18): 6187 p(b,m) | k = m | p(k,m) | j = m | j = k | p(j,b). [resolve(3584,f,5694,b),merge(g)]. given #965 (T,wt=18): 6924 p(b,b) | j = b | -p(j,b) | k = b | j = k | -p(j,k). [resolve(6902,a,4,f),flip(b),flip(d),flip(e)]. given #966 (A,wt=31): 990 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(80,h,56,b),flip(d),flip(f),unit_del(d,27)]. given #967 (F,wt=18): 6925 p(b,b) | k = b | -p(k,b) | j = b | j = k | -p(j,k). [resolve(6902,a,4,e),flip(b),flip(d)]. given #968 (F,wt=18): 6926 p(b,b) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(6902,a,2,f),flip(b),flip(d),flip(e)]. given #969 (T,wt=18): 6927 p(b,b) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(6902,a,2,e),flip(b),flip(d)]. given #970 (T,wt=18): 6972 p(k,b) | p(k,k) | g(k) = k | g(k) = m | g(k) = b. [resolve(6871,b,6,d),flip(c),flip(d),flip(e)]. given #971 (A,wt=42): 1014 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(80,i,372,b),flip(d),flip(f),flip(g)]. given #972 (F,wt=14): 11696 p(k,b) | p(k,k) | g(k) = m | g(k) = b. [para(6972(c,1),6870(b,2)),merge(e),merge(f),merge(g)]. given #973 (F,wt=13): 11712 p(k,b) | p(k,k) | g(k) = b | p(k,m). [para(11696(c,1),6870(b,2)),merge(d),merge(f)]. given #974 (T,wt=9): 11729 p(k,b) | p(k,k) | p(k,m). [para(11712(c,1),6870(b,2)),merge(d),merge(e),merge(f)]. given #975 (T,wt=16): 11711 p(k,b) | p(k,k) | g(k) = b | k = b | k != m. [para(11696(c,1),18(c,1)),flip(d),flip(f),merge(e)]. given #976 (A,wt=46): 1032 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(80,i,77,b),flip(d),flip(f),flip(g)]. given #977 (F,wt=18): 7559 p(j,b) | p(m,b) | k = m | p(k,m) | j = m | j = k. [resolve(7553,b,3147,f),merge(c)]. given #978 (F,wt=18): 7560 p(j,b) | p(m,b) | j = m | p(j,m) | k = m | j = k. [resolve(7553,b,3146,f),merge(c)]. given #979 (T,wt=18): 7561 p(j,b) | p(m,b) | k = b | -p(k,b) | j = b | j = k. [resolve(7553,b,3145,f),merge(c)]. given #980 (T,wt=18): 7634 p(j,b) | k = b | -p(k,b) | j = b | j = k | -p(k,j). [resolve(7620,b,4,f),flip(b),flip(d)]. given #981 (A,wt=22): 1095 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),916(c,1,1,1))]. given #982 (F,wt=18): 7635 p(j,b) | k = m | p(k,m) | j = m | j = k | -p(k,j). [resolve(7620,b,2,f),flip(b),flip(d)]. given #983 (F,wt=18): 7636 p(j,b) | j = m | p(j,m) | k = m | j = k | -p(k,j). [resolve(7620,b,2,e),flip(b),flip(d),flip(e)]. given #984 (T,wt=18): 7666 p(k,b) | j = b | -p(j,b) | k = b | j = k | -p(j,k). [resolve(7647,a,4,f),flip(b),flip(d),flip(e)]. given #985 (T,wt=18): 7667 p(k,b) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(7647,a,2,f),flip(b),flip(d),flip(e)]. given #986 (A,wt=22): 1096 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),916(c,1,1,1))]. given #987 (F,wt=18): 7668 p(k,b) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(7647,a,2,e),flip(b),flip(d)]. given #988 (F,wt=18): 7742 p(b,j) | p(k,b) | g(k) = k | g(k) = m | g(k) = b. [resolve(7669,c,6,d),flip(c),flip(d),flip(e)]. given #989 (T,wt=17): 11818 p(b,j) | p(k,b) | g(k) = m | g(k) = b | k = b. [resolve(7742,c,18,c),flip(e),merge(f)]. given #990 (T,wt=16): 11825 p(b,j) | p(k,b) | g(k) = b | k = b | k != m. [para(11818(c,1),18(c,1)),flip(e),flip(g),merge(e),merge(f)]. given #991 (A,wt=28): 1097 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),916(c,1,1,1))]. given #992 (F,wt=16): 11826 p(b,j) | p(k,b) | g(k) = b | k = b | p(k,m). [para(11818(c,1),7670(c,2)),merge(e),merge(f)]. given #993 (F,wt=12): 11836 p(b,j) | p(k,b) | k = b | p(k,m). [resolve(11826,c,16,c),flip(e),merge(e),merge(f)]. given #994 (T,wt=9): 11849 p(b,j) | p(k,b) | p(k,m). [para(11836(c,1),7647(a,1)),merge(d),merge(e)]. given #995 (T,wt=13): 11861 p(b,j) | p(k,b) | k = m | p(f(k),k). [resolve(11849,c,14,b),flip(c)]. given #996 (A,wt=28): 1098 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),916(c,1,1,1))]. given #997 (F,wt=13): 11862 p(b,j) | p(k,b) | k = m | p(k,f(k)). [resolve(11849,c,12,b),flip(c)]. given #998 (F,wt=13): 11877 p(b,j) | p(k,b) | p(f(k),k) | p(b,m). [para(11861(c,1),6860(a,2))]. given #999 (T,wt=13): 11879 p(b,j) | p(k,b) | p(f(k),k) | p(m,j). [para(11861(c,1),7647(a,1)),merge(e)]. given #1000 (T,wt=13): 11896 p(b,j) | p(k,b) | p(f(k),k) | p(m,m). [para(11861(c,1),11849(c,1)),merge(d),merge(e)]. given #1001 (A,wt=35): 1099 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(78(d,1),916(c,1,1,1))]. given #1002 (F,wt=13): 11910 p(b,j) | p(k,b) | p(k,f(k)) | p(b,m). [para(11862(c,1),6860(a,2))]. given #1003 (F,wt=13): 11912 p(b,j) | p(k,b) | p(k,f(k)) | p(m,j). [para(11862(c,1),7647(a,1)),merge(e)]. given #1004 (T,wt=13): 11929 p(b,j) | p(k,b) | p(k,f(k)) | p(m,m). [para(11862(c,1),11849(c,1)),merge(d),merge(e)]. given #1005 (T,wt=14): 11880 p(b,j) | p(k,b) | p(f(k),k) | p(g(m),k). [para(11861(c,1),7669(c,1,1)),merge(d),merge(e)]. given #1006 (A,wt=22): 1101 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),922(c,1,1,1))]. given #1007 (F,wt=14): 11881 p(b,j) | p(k,b) | p(f(k),k) | p(g(k),m). [para(11861(c,1),7669(c,2)),merge(d),merge(e)]. given #1008 (F,wt=14): 11882 p(b,j) | p(k,b) | p(f(k),k) | p(m,g(k)). [para(11861(c,1),7670(c,1)),merge(d),merge(e)]. given #1009 (T,wt=14): 11883 p(b,j) | p(k,b) | p(f(k),k) | p(k,g(m)). [para(11861(c,1),7670(c,2,1)),merge(d),merge(e)]. given #1010 (T,wt=14): 11913 p(b,j) | p(k,b) | p(k,f(k)) | p(g(m),k). [para(11862(c,1),7669(c,1,1)),merge(d),merge(e)]. given #1011 (A,wt=22): 1102 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),922(c,1,1,1))]. given #1012 (F,wt=14): 11914 p(b,j) | p(k,b) | p(k,f(k)) | p(g(k),m). [para(11862(c,1),7669(c,2)),merge(d),merge(e)]. given #1013 (F,wt=14): 11915 p(b,j) | p(k,b) | p(k,f(k)) | p(m,g(k)). [para(11862(c,1),7670(c,1)),merge(d),merge(e)]. given #1014 (T,wt=14): 11916 p(b,j) | p(k,b) | p(k,f(k)) | p(k,g(m)). [para(11862(c,1),7670(c,2,1)),merge(d),merge(e)]. given #1015 (T,wt=14): 12051 p(b,j) | p(k,b) | p(f(k),k) | p(g(m),m). [para(11861(c,1),11880(d,2)),merge(d),merge(e),merge(f)]. given #1016 (A,wt=28): 1103 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),922(c,1,1,1))]. given #1017 (F,wt=14): 12117 p(b,j) | p(k,b) | p(k,f(k)) | p(g(m),m). [para(11862(c,1),11913(d,2)),merge(d),merge(e),merge(f)]. given #1018 (F,wt=14): 12168 p(b,j) | p(k,b) | p(k,f(k)) | p(m,g(m)). [para(11862(c,1),11916(d,1)),merge(d),merge(e),merge(f)]. given #1019 (T,wt=16): 11865 p(b,j) | p(k,b) | p(f(k),k) | p(j,b) | j = b. [resolve(11861,c,8027,d),merge(e)]. given #1020 (T,wt=13): 12272 p(b,j) | p(k,b) | p(f(k),k) | p(j,b). [para(11865(e,1),7647(a,2)),merge(e),merge(f)]. given #1021 (A,wt=28): 1104 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),922(c,1,1,1))]. given #1022 (F,wt=16): 11898 p(b,j) | p(k,b) | p(k,f(k)) | p(j,b) | j = b. [resolve(11862,c,8027,d),merge(e)]. given #1023 (F,wt=13): 12307 p(b,j) | p(k,b) | p(k,f(k)) | p(j,b). [para(11898(e,1),7647(a,2)),merge(e),merge(f)]. given #1024 (T,wt=17): 11864 p(b,j) | p(k,b) | p(f(k),k) | g(k) = b | k = b. [resolve(11861,c,11825,e),merge(d),merge(e)]. given #1025 (T,wt=13): 12328 p(b,j) | p(k,b) | p(f(k),k) | k = b. [resolve(11864,d,16,c),flip(e),merge(e),merge(f)]. given #1026 (A,wt=35): 1105 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(78(d,1),922(c,1,1,1))]. given #1027 (F,wt=10): 12340 p(b,j) | p(k,b) | p(f(k),k). [para(12328(d,1),7647(a,1)),merge(d),merge(e)]. given #1028 (F,wt=14): 12354 p(b,j) | p(k,b) | p(k,f(k)) | p(f(m),k). [para(11862(c,1),12340(c,1,1)),merge(d),merge(e)]. given #1029 (T,wt=14): 12355 p(b,j) | p(k,b) | p(k,f(k)) | p(f(k),m). [para(11862(c,1),12340(c,2)),merge(d),merge(e)]. given #1030 (T,wt=14): 12373 p(b,j) | p(k,b) | p(k,f(k)) | p(f(m),m). [para(11862(c,1),12354(d,2)),merge(d),merge(e),merge(f)]. given #1031 (A,wt=26): 1110 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(82,d,31,c)]. given #1032 (F,wt=17): 11897 p(b,j) | p(k,b) | p(k,f(k)) | g(k) = b | k = b. [resolve(11862,c,11825,e),merge(d),merge(e)]. given #1033 (F,wt=13): 12617 p(b,j) | p(k,b) | p(k,f(k)) | k = b. [resolve(11897,d,16,c),flip(e),merge(e),merge(f)]. given #1034 (T,wt=10): 12629 p(b,j) | p(k,b) | p(k,f(k)). [para(12617(d,1),7647(a,1)),merge(d),merge(e)]. given #1035 (T,wt=18): 7766 p(j,b) | j = m | j = b | j = x | -p(x,k) | k = x. [para(7633(b,1),29(b,2))]. given #1036 (A,wt=30): 1111 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(82,d,10,c)]. given #1037 (F,wt=18): 7776 p(j,b) | j = b | p(k,k) | j = x | -p(x,m) | k = x. [para(7769(b,1),29(b,2))]. given #1038 (F,wt=18): 7786 p(j,b) | j = b | k = b | j = x | -p(x,m) | k = x. [para(7771(b,1),29(b,2))]. given #1039 (T,wt=18): 8017 p(j,b) | p(k,b) | j = b | j = x | -p(x,m) | k = x. [para(8012(d,1),29(b,2))]. given #1040 (T,wt=18): 8047 p(k,b) | p(k,m) | p(b,m) | j = m | j = b | -p(b,j). [resolve(8038,a,2,f),flip(e),unit_del(c,27)]. given #1041 (A,wt=26): 1112 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(82,d,31,c(flip))]. given #1042 (F,wt=18): 8048 p(k,b) | p(k,m) | j = m | p(j,m) | j = b | -p(b,j). [resolve(8038,a,2,e),flip(c),flip(f),unit_del(e,27)]. given #1043 (F,wt=18): 8091 p(j,b) | p(k,b) | g(k) = k | g(k) = m | g(k) = b. [resolve(8079,c,6,d),flip(c),flip(d),flip(e)]. given #1044 (T,wt=17): 12685 p(j,b) | p(k,b) | g(k) = m | g(k) = b | k = b. [resolve(8091,c,18,c),flip(e),merge(f)]. given #1045 (T,wt=16): 12691 p(j,b) | p(k,b) | g(k) = b | k = b | k != m. [para(12685(c,1),18(c,1)),flip(e),flip(g),merge(e),merge(f)]. given #1046 (A,wt=29): 1113 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(82,d,10,c(flip))]. given #1047 (F,wt=18): 8523 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(f(j),g(m)). [para(8177(c,1),362(b,1,1))]. given #1048 (F,wt=17): 12700 p(j,b) | p(k,b) | p(m,b) | p(f(j),g(m)) | k != b. [para(8523(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1049 (T,wt=17): 12701 p(j,b) | p(k,b) | p(m,b) | p(f(j),g(m)) | k != m. [para(8523(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1050 (T,wt=18): 8524 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(f(g(m)),j). [para(8177(c,1),362(b,2))]. given #1051 (A,wt=21): 1114 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | g(k) = j | p(g(k),j). [factor(1110,a,d),flip(e),merge(d)]. given #1052 (F,wt=17): 12731 p(j,b) | p(k,b) | p(m,b) | p(f(g(m)),j) | k != b. [para(8524(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1053 (F,wt=17): 12732 p(j,b) | p(k,b) | p(m,b) | p(f(g(m)),j) | k != m. [para(8524(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1054 (T,wt=18): 8525 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(j,f(g(m))). [para(8177(c,1),372(b,1))]. given #1055 (T,wt=17): 12777 p(j,b) | p(k,b) | p(m,b) | p(j,f(g(m))) | k != b. [para(8525(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1056 (A,wt=26): 1246 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(84,d,31,c)]. given #1057 (F,wt=17): 12778 p(j,b) | p(k,b) | p(m,b) | p(j,f(g(m))) | k != m. [para(8525(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1058 (F,wt=18): 8526 p(j,b) | p(k,b) | g(m) = k | p(m,b) | p(g(m),f(j)). [para(8177(c,1),372(b,2,1))]. given #1059 (T,wt=17): 12893 p(j,b) | p(k,b) | p(m,b) | p(g(m),f(j)) | k != b. [para(8526(c,1),16(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1060 (T,wt=17): 12894 p(j,b) | p(k,b) | p(m,b) | p(g(m),f(j)) | k != m. [para(8526(c,1),18(c,1)),flip(e),merge(f),unit_del(e,27)]. given #1061 (A,wt=30): 1247 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(84,d,10,c)]. given #1062 (F,wt=18): 8828 p(j,b) | k = m | p(b,m) | p(k,m) | j = m | -p(m,b). [factor(8822,b,g)]. given #1063 (F,wt=18): 9041 p(j,b) | p(k,b) | p(f(g(j)),g(j)) | j = b | j != m. [para(8219(c,1),18(c,1)),flip(d),flip(f),merge(e)]. given #1064 (T,wt=15): 12932 p(j,b) | p(k,b) | p(f(g(j)),g(j)) | j = b. [resolve(9041,e,8012,d),merge(e),merge(f),merge(g)]. given #1065 (T,wt=12): 12944 p(j,b) | p(k,b) | p(f(g(j)),g(j)). [para(12932(d,1),7647(a,2)),merge(d),merge(e)]. given #1066 (A,wt=26): 1248 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(84,d,31,c(flip))]. given #1067 (F,wt=14): 12973 p(j,b) | p(k,b) | j = b | p(f(k),g(j)). [para(7980(c,1),12944(c,1,1)),merge(d),merge(e)]. given #1068 (F,wt=11): 13050 p(j,b) | p(k,b) | p(f(k),g(j)). [para(12973(c,1),7647(a,2)),merge(d),merge(e)]. given #1069 (T,wt=13): 13074 p(j,b) | p(k,b) | j = b | p(f(k),k). [para(7980(c,1),13050(c,2)),merge(d),merge(e)]. given #1070 (T,wt=10): 13109 p(j,b) | p(k,b) | p(f(k),k). [para(13074(c,1),7647(a,2)),merge(d),merge(e)]. given #1071 (A,wt=29): 1249 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(84,d,10,c(flip))]. given #1072 (F,wt=14): 12974 p(j,b) | p(k,b) | j = b | p(f(g(j)),k). [para(7980(c,1),12944(c,2)),merge(d),merge(e)]. given #1073 (F,wt=11): 13159 p(j,b) | p(k,b) | p(f(g(j)),k). [para(12974(c,1),7647(a,2)),merge(d),merge(e)]. given #1074 (T,wt=14): 13073 p(j,b) | p(k,b) | g(j) = k | p(f(k),j). [para(7900(c,1),13050(c,2)),merge(d),merge(e)]. given #1075 (T,wt=14): 13075 p(j,b) | p(k,b) | j = b | p(f(k),g(m)). [para(8012(d,1),13050(c,2,1)),merge(d),merge(e)]. given #1076 (A,wt=32): 1429 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(89,f,31,c)]. given #1077 (F,wt=11): 13222 p(j,b) | p(k,b) | p(f(k),g(m)). [para(13075(c,1),7647(a,2)),merge(d),merge(e)]. given #1078 (F,wt=14): 13180 p(j,b) | p(k,b) | g(j) = k | p(f(j),k). [para(7900(c,1),13159(c,1,1)),merge(d),merge(e)]. given #1079 (T,wt=14): 13181 p(j,b) | p(k,b) | j = b | p(f(g(m)),k). [para(8012(d,1),13159(c,1,1,1)),merge(d),merge(e)]. given #1080 (T,wt=11): 13337 p(j,b) | p(k,b) | p(f(g(m)),k). [para(13181(c,1),7647(a,2)),merge(d),merge(e)]. given #1081 (A,wt=36): 1430 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(89,f,10,c)]. given #1082 (F,wt=14): 13302 p(j,b) | p(k,b) | g(m) = k | p(f(k),j). [para(8177(c,1),13222(c,2)),merge(d),merge(e)]. given #1083 (F,wt=14): 13354 p(j,b) | p(k,b) | g(m) = k | p(f(j),k). [para(8177(c,1),13337(c,1,1)),merge(d),merge(e)]. given #1084 (T,wt=15): 12971 p(j,b) | p(k,b) | g(j) = k | p(f(j),g(j)). [para(7900(c,1),12944(c,1,1)),merge(d),merge(e)]. given #1085 (T,wt=15): 12972 p(j,b) | p(k,b) | g(j) = k | p(f(g(j)),j). [para(7900(c,1),12944(c,2)),merge(d),merge(e)]. given #1086 (A,wt=38): 1479 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(90,e,89,f),merge(h),merge(i),merge(j)]. given #1087 (F,wt=15): 12975 p(j,b) | p(k,b) | j = b | p(f(g(m)),g(j)). [para(8012(d,1),12944(c,1,1,1)),merge(d),merge(e)]. given #1088 (F,wt=12): 13418 p(j,b) | p(k,b) | p(f(g(m)),g(j)). [para(12975(c,1),7647(a,2)),merge(d),merge(e)]. given #1089 (T,wt=15): 12976 p(j,b) | p(k,b) | j = b | p(f(g(j)),g(m)). [para(8012(d,1),12944(c,2,1)),merge(d),merge(e)]. given #1090 (T,wt=12): 13483 p(j,b) | p(k,b) | p(f(g(j)),g(m)). [para(12976(c,1),7647(a,2)),merge(d),merge(e)]. given #1091 (A,wt=30): 1480 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(90,e,85,e),merge(g),merge(h),merge(i)]. given #1092 (F,wt=15): 13441 p(j,b) | p(k,b) | g(j) = k | p(f(g(m)),j). [para(7900(c,1),13418(c,2)),merge(d),merge(e)]. given #1093 (F,wt=15): 13442 p(j,b) | p(k,b) | j = b | p(f(g(m)),g(m)). [para(8012(d,1),13418(c,2,1)),merge(d),merge(e)]. given #1094 (T,wt=12): 13562 p(j,b) | p(k,b) | p(f(g(m)),g(m)). [para(13442(c,1),7647(a,2)),merge(d),merge(e)]. given #1095 (T,wt=15): 13443 p(j,b) | p(k,b) | g(m) = k | p(f(j),g(j)). [para(8177(c,1),13418(c,1,1)),merge(d),merge(e)]. given #1096 (A,wt=21): 1545 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = b | g(x) != x. [para(91(d,1),90(e,1,1)),merge(d),merge(e),merge(f)]. given #1097 (F,wt=15): 13507 p(j,b) | p(k,b) | g(j) = k | p(f(j),g(m)). [para(7900(c,1),13483(c,1,1)),merge(d),merge(e)]. given #1098 (F,wt=15): 13508 p(j,b) | p(k,b) | g(m) = k | p(f(g(j)),j). [para(8177(c,1),13483(c,2)),merge(d),merge(e)]. given #1099 (T,wt=15): 13581 p(j,b) | p(k,b) | g(m) = k | p(f(j),g(m)). [para(8177(c,1),13562(c,1,1)),merge(d),merge(e)]. given #1100 (T,wt=15): 13582 p(j,b) | p(k,b) | g(m) = k | p(f(g(m)),j). [para(8177(c,1),13562(c,2)),merge(d),merge(e)]. given #1101 (A,wt=23): 1632 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),1100(c,1,1,1,1))]. given #1102 (F,wt=16): 13077 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(k),m). [para(8220(c,1),13050(c,2)),merge(d),merge(e)]. given #1103 (F,wt=16): 13182 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(m),k). [para(8220(c,1),13159(c,1,1)),merge(d),merge(e)]. given #1104 (T,wt=16): 13304 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(f(k),m). [para(8387(c,1),13222(c,2)),merge(d),merge(e)]. given #1105 (T,wt=16): 13356 p(j,b) | p(k,b) | p(g(m),f(g(m))) | p(f(m),k). [para(8387(c,1),13337(c,1,1)),merge(d),merge(e)]. given #1106 (A,wt=23): 1633 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),1100(c,1,1,1,1))]. given #1107 (F,wt=17): 12979 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(m),g(j)). [para(8220(c,1),12944(c,1,1)),merge(d),merge(e)]. given #1108 (F,wt=17): 12980 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(g(j)),m). [para(8220(c,1),12944(c,2)),merge(d),merge(e)]. given #1109 (T,wt=16): 14017 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(m),m). [para(8220(c,1),12980(d,1,1)),merge(d),merge(e),merge(f)]. given #1110 (T,wt=17): 13444 p(j,b) | p(k,b) | p(g(j),f(g(j))) | p(f(g(m)),m). [para(8220(c,1),13418(c,2)),merge(d),merge(e)]. given #1111 (A,wt=29): 1634 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),1100(c,1,1,1,1))]. given #1112 (F,wt=17): 13446 p(j,b) | p(k,b) | p(g(m),f(g