============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 27095 was started by mccune on cleo, Fri Apr 13 09:20:32 2007 The command was "/home/mccune/bin/prover9 -f wang-eq.in wang2-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 wang2-eq.in assign(max_seconds,60). formulas(sos). m != b. b = k | k = m. y = j | -p(y,j) | y = k. y = j | p(y,j) | y != k. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x = m | p(x,m) | y = m | y = x | -p(x,y) | -p(y,x). [assumption]. x = b | -p(x,b) | y = b | y = x | -p(x,y) | -p(y,x). [assumption]. x = k | x = m | x = b | -p(x,k). [assumption]. x = m | -p(x,m) | f(x) != m. [assumption]. x = m | -p(x,m) | f(x) != x. [assumption]. x = m | -p(x,m) | p(x,f(x)). [assumption]. x = m | -p(x,m) | p(f(x),x). [assumption]. x = b | p(x,b) | g(x) != b. [assumption]. x = b | p(x,b) | g(x) != x. [assumption]. x = b | p(x,b) | p(x,g(x)). [assumption]. x = b | p(x,b) | p(g(x),x). [assumption]. x = k | x != m | p(x,k). [assumption]. x = k | x != b | p(x,k). [assumption]. m != b. [assumption]. b = k | k = m. [assumption]. x = j | -p(x,j) | x = k. [assumption]. x = j | p(x,j) | x != k. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ p, = ]). Function symbol precedence: lex([ b, m, k, j, f, g ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(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 k = b | k = m. [copy(28),flip(a)]. 31 j = x | -p(x,j) | k = x. [copy(30),flip(a),flip(c)]. 33 j = x | p(x,j) | k != x. [copy(32),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=6): 29 k = b | k = m. [copy(28),flip(a)]. given #16 (I,wt=9): 31 j = x | -p(x,j) | k = x. [copy(30),flip(a),flip(c)]. given #17 (I,wt=9): 33 j = x | p(x,j) | k != x. [copy(32),flip(a),flip(c)]. given #18 (A,wt=16): 34 p(g(x),b) | p(g(x),g(g(x))) | b = x | p(x,b). [resolve(20,a,16,c(flip))]. given #19 (T,wt=6): 51 k = m | p(m,k). [xx_res(24,b)]. given #20 (T,wt=6): 54 k = b | p(b,k). [xx_res(26,b)]. given #21 (T,wt=6): 65 j = k | p(k,j). [xx_res(33,c)]. given #22 (T,wt=6): 93 p(b,k) | p(m,k). [para(54(a,1),51(a,1)),flip(b),unit_del(b,27)]. given #23 (A,wt=13): 35 p(f(b),b) | p(f(b),g(f(b))) | -p(b,m). [resolve(20,a,10,c(flip)),unit_del(c,27)]. given #24 (T,wt=6): 98 p(b,k) | p(m,b). [para(54(a,1),93(b,2)),merge(b)]. given #25 (T,wt=7): 57 p(m,b) | p(g(m),m). [resolve(27,a,22,a(flip))]. given #26 (T,wt=7): 58 p(m,b) | p(m,g(m)). [resolve(27,a,20,a(flip))]. given #27 (T,wt=9): 62 j = m | p(m,j) | k = b. [resolve(33,c,29,b)]. given #28 (A,wt=25): 36 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 #29 (T,wt=9): 84 p(m,k) | j = m | p(m,j). [resolve(51,a,33,c)]. given #30 (T,wt=9): 87 p(b,k) | j = b | p(b,j). [resolve(54,a,33,c)]. given #31 (T,wt=9): 94 k = b | j = m | p(k,j). [para(29(b,1),65(a,2))]. given #32 (T,wt=9): 96 p(m,k) | j = m | p(k,j). [para(51(a,1),65(a,2))]. given #33 (A,wt=17): 37 p(x,b) | p(x,g(x)) | b = y | p(y,b) | g(y) != x. [para(20(a,1),16(c,2))]. given #34 (T,wt=9): 97 p(b,k) | j = b | p(k,j). [para(54(a,1),65(a,2))]. given #35 (T,wt=10): 59 p(x,b) | p(x,g(x)) | m != x. [para(20(a,1),27(a,2))]. given #36 (T,wt=10): 60 p(x,b) | p(g(x),x) | m != x. [para(22(a,1),27(a,2))]. given #37 (T,wt=10): 136 p(k,b) | p(k,g(k)) | p(m,k). [resolve(59,c,51,a(flip))]. given #38 (A,wt=17): 38 p(x,b) | p(x,g(x)) | x = y | p(y,b) | p(y,g(y)). [para(20(a,1),20(a,1))]. given #39 (T,wt=10): 137 p(k,b) | p(k,g(k)) | k = b. [resolve(59,c,29,b(flip))]. given #40 (T,wt=10): 142 p(k,b) | p(g(k),k) | p(m,k). [resolve(60,c,51,a(flip))]. given #41 (T,wt=10): 143 p(k,b) | p(g(k),k) | k = b. [resolve(60,c,29,b(flip))]. given #42 (T,wt=10): 150 p(m,k) | p(k,b) | p(m,g(k)). [para(51(a,1),136(b,1)),merge(d)]. given #43 (A,wt=16): 39 p(g(x),b) | p(g(g(x)),g(x)) | b = x | p(x,b). [resolve(22,a,16,c(flip))]. given #44 (T,wt=10): 151 p(m,k) | p(k,b) | p(k,g(m)). [para(51(a,1),136(b,2,1)),merge(d)]. given #45 (T,wt=10): 163 p(m,k) | p(k,b) | p(g(m),k). [para(51(a,1),142(b,1,1)),merge(d)]. given #46 (T,wt=10): 164 p(m,k) | p(k,b) | p(g(k),m). [para(51(a,1),142(b,2)),merge(d)]. given #47 (T,wt=10): 174 p(m,k) | p(m,b) | p(m,g(k)). [para(51(a,1),150(b,1)),merge(b)]. given #48 (A,wt=13): 40 p(f(b),b) | p(g(f(b)),f(b)) | -p(b,m). [resolve(22,a,10,c(flip)),unit_del(c,27)]. given #49 (T,wt=10): 208 p(m,k) | p(k,b) | p(m,g(m)). [para(51(a,1),151(c,1)),merge(b)]. given #50 (T,wt=10): 214 p(m,k) | p(k,b) | p(g(m),m). [para(51(a,1),163(c,2)),merge(b)]. given #51 (T,wt=12): 66 k = b | j = x | p(x,j) | m != x. [para(29(b,1),33(c,1))]. given #52 (T,wt=12): 86 p(m,k) | j = x | p(x,j) | m != x. [para(51(a,1),33(c,1))]. given #53 (A,wt=25): 41 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 #54 (T,wt=12): 91 p(b,k) | j = x | p(x,j) | b != x. [para(54(a,1),33(c,1))]. given #55 (T,wt=12): 95 p(k,j) | j = x | -p(x,k) | k = x. [para(65(a,1),31(b,2))]. given #56 (T,wt=12): 111 p(m,j) | k = b | j = k | p(j,k). [resolve(62,a,24,b(flip)),flip(c)]. given #57 (T,wt=12): 113 p(m,j) | k = b | j = b | -p(b,m). [factor(112,b,e)]. given #58 (A,wt=17): 42 p(x,b) | p(g(x),x) | b = y | p(y,b) | g(y) != x. [para(22(a,1),16(c,2))]. given #59 (T,wt=12): 118 p(m,k) | p(m,j) | j = k | p(j,k). [resolve(84,b,24,b(flip)),flip(c)]. given #60 (T,wt=12): 120 p(b,k) | p(b,j) | j = k | p(j,k). [resolve(87,b,26,b(flip)),flip(c)]. given #61 (T,wt=12): 126 k = b | p(k,j) | j = b | -p(b,m). [factor(125,a,e)]. given #62 (T,wt=12): 280 p(k,j) | j = m | k = m | p(b,k). [resolve(95,c,93,b)]. given #63 (A,wt=17): 43 p(x,b) | p(g(x),x) | x = y | p(y,b) | p(y,g(y)). [para(22(a,1),20(a,1))]. given #64 (T,wt=9): 298 p(k,j) | k = m | p(b,k). [para(280(b,1),65(a,1)),flip(d),merge(d),merge(e)]. given #65 (T,wt=6): 308 p(k,j) | p(b,k). [para(298(b,1),54(a,1)),merge(d),unit_del(c,27)]. given #66 (T,wt=6): 311 p(b,k) | p(b,j). [para(54(a,1),308(a,1)),merge(c)]. given #67 (T,wt=13): 52 k = x | p(x,k) | p(x,b) | p(g(x),x). [resolve(26,b,22,a)]. given #68 (A,wt=17): 44 p(x,b) | p(x,g(x)) | x = y | p(y,b) | p(g(y),y). [para(20(a,1),22(a,1))]. given #69 (T,wt=13): 53 k = x | p(x,k) | p(x,b) | p(x,g(x)). [resolve(26,b,20,a)]. given #70 (T,wt=13): 63 j = b | p(b,j) | p(k,b) | p(g(k),k). [resolve(33,c,22,a(flip))]. given #71 (T,wt=13): 64 j = b | p(b,j) | p(k,b) | p(k,g(k)). [resolve(33,c,20,a(flip))]. given #72 (T,wt=13): 69 p(g(m),b) | p(g(m),g(g(m))) | p(m,b). [resolve(34,c,27,a(flip))]. given #73 (A,wt=17): 45 p(x,b) | p(g(x),x) | x = y | p(y,b) | p(g(y),y). [para(22(a,1),22(a,1))]. given #74 (T,wt=13): 89 p(x,b) | p(x,g(x)) | k = x | p(b,k). [para(20(a,1),54(a,2))]. given #75 (T,wt=13): 90 p(x,b) | p(g(x),x) | k = x | p(b,k). [para(22(a,1),54(a,2))]. given #76 (T,wt=13): 104 p(x,b) | p(x,g(x)) | p(b,k) | p(m,x). [para(20(a,1),98(b,2))]. given #77 (T,wt=13): 105 p(x,b) | p(g(x),x) | p(b,k) | p(m,x). [para(22(a,1),98(b,2))]. given #78 (A,wt=16): 46 p(b,b) | p(g(b),b) | g(b) = b | g(g(b)) != b. [factor(42,b,d),flip(c)]. given #79 (T,wt=13): 107 p(m,b) | g(m) = m | p(f(g(m)),g(m)). [resolve(57,b,14,b),flip(b)]. given #80 (T,wt=9): 415 p(m,b) | p(f(g(m)),g(m)). [resolve(107,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #81 (T,wt=13): 108 p(m,b) | g(m) = m | p(g(m),f(g(m))). [resolve(57,b,12,b),flip(b)]. given #82 (T,wt=9): 425 p(m,b) | p(g(m),f(g(m))). [resolve(108,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #83 (A,wt=16): 55 p(x,b) | p(x,g(x)) | k = y | x != y | p(y,k). [para(20(a,1),26(b,1))]. given #84 (T,wt=13): 132 p(j,b) | p(j,g(j)) | p(m,k) | p(k,j). [resolve(59,c,96,b(flip))]. given #85 (T,wt=13): 133 p(j,b) | p(j,g(j)) | k = b | p(k,j). [resolve(59,c,94,b(flip))]. given #86 (T,wt=13): 134 p(j,b) | p(j,g(j)) | p(m,k) | p(m,j). [resolve(59,c,84,b(flip))]. given #87 (T,wt=13): 135 p(j,b) | p(j,g(j)) | p(m,j) | k = b. [resolve(59,c,62,a(flip))]. given #88 (A,wt=16): 56 p(x,b) | p(g(x),x) | k = y | x != y | p(y,k). [para(22(a,1),26(b,1))]. given #89 (T,wt=13): 138 p(j,b) | p(g(j),j) | p(m,k) | p(k,j). [resolve(60,c,96,b(flip))]. given #90 (T,wt=13): 139 p(j,b) | p(g(j),j) | k = b | p(k,j). [resolve(60,c,94,b(flip))]. given #91 (T,wt=13): 140 p(j,b) | p(g(j),j) | p(m,k) | p(m,j). [resolve(60,c,84,b(flip))]. given #92 (T,wt=13): 141 p(j,b) | p(g(j),j) | p(m,j) | k = b. [resolve(60,c,62,a(flip))]. given #93 (A,wt=15): 61 k = b | k = x | m = x | b = x | -p(x,m). [para(29(b,1),6(d,2))]. given #94 (T,wt=13): 156 p(k,b) | p(k,g(k)) | j = b | p(k,j). [para(137(c,1),65(a,2))]. given #95 (T,wt=13): 167 p(k,b) | p(g(k),k) | j = b | p(k,j). [para(143(c,1),65(a,2))]. given #96 (T,wt=13): 180 p(g(m),b) | p(g(g(m)),g(m)) | p(m,b). [resolve(39,c,27,a(flip))]. given #97 (T,wt=13): 314 p(x,b) | p(x,g(x)) | p(b,k) | p(x,j). [para(20(a,1),311(b,1))]. given #98 (A,wt=19): 67 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | k = x | p(x,k). [resolve(34,c,26,b)]. given #99 (T,wt=13): 315 p(x,b) | p(g(x),x) | p(b,k) | p(x,j). [para(22(a,1),311(b,1))]. given #100 (T,wt=13): 365 p(k,b) | p(g(k),k) | j = k | p(b,j). [factor(360,a,e),merge(e)]. given #101 (T,wt=13): 372 p(k,b) | p(k,g(k)) | j = k | p(b,j). [factor(367,a,e),merge(e)]. given #102 (T,wt=13): 442 p(k,j) | p(j,b) | p(k,g(j)) | p(m,k). [para(65(a,1),132(b,1)),merge(e)]. given #103 (A,wt=19): 68 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | j = b | p(b,j). [resolve(34,c,33,c(flip))]. given #104 (T,wt=13): 443 p(k,j) | p(j,b) | p(j,g(k)) | p(m,k). [para(65(a,1),132(b,2,1)),merge(e)]. given #105 (T,wt=13): 450 p(m,k) | p(k,j) | p(j,b) | p(m,g(j)). [para(96(b,1),132(b,1)),merge(e),merge(f)]. given #106 (T,wt=13): 451 p(m,k) | p(k,j) | p(j,b) | p(j,g(m)). [para(96(b,1),132(b,2,1)),merge(e),merge(f)]. given #107 (T,wt=13): 458 p(j,b) | p(j,g(j)) | p(k,j) | j = b. [para(133(c,1),65(a,2)),merge(e)]. given #108 (A,wt=23): 70 p(g(g(x)),b) | p(g(g(x)),g(g(g(x)))) | p(g(x),b) | b = x | p(x,b). [resolve(34,c,16,c(flip))]. given #109 (T,wt=13): 470 p(m,k) | p(m,j) | p(j,b) | p(m,g(j)). [para(84(b,1),134(b,1)),merge(e),merge(f)]. given #110 (T,wt=13): 471 p(m,k) | p(m,j) | p(j,b) | p(j,g(m)). [para(84(b,1),134(b,2,1)),merge(e),merge(f)]. given #111 (T,wt=13): 483 p(j,b) | p(j,g(j)) | p(m,j) | j = k. [factor(478,a,c),flip(e),merge(c)]. given #112 (T,wt=13): 490 p(k,j) | p(j,b) | p(g(k),j) | p(m,k). [para(65(a,1),138(b,1,1)),merge(e)]. given #113 (A,wt=20): 71 p(g(f(b)),b) | p(g(f(b)),g(g(f(b)))) | p(f(b),b) | -p(b,m). [resolve(34,c,10,c(flip)),unit_del(d,27)]. given #114 (T,wt=13): 491 p(k,j) | p(j,b) | p(g(j),k) | p(m,k). [para(65(a,1),138(b,2)),merge(e)]. given #115 (T,wt=13): 498 p(m,k) | p(k,j) | p(j,b) | p(g(m),j). [para(96(b,1),138(b,1,1)),merge(e),merge(f)]. given #116 (T,wt=13): 499 p(m,k) | p(k,j) | p(j,b) | p(g(j),m). [para(96(b,1),138(b,2)),merge(e),merge(f)]. given #117 (T,wt=13): 506 p(j,b) | p(g(j),j) | p(k,j) | j = b. [para(139(c,1),65(a,2)),merge(e)]. given #118 (A,wt=31): 72 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(34(c,1),4(b,2))]. given #119 (T,wt=13): 518 p(m,k) | p(m,j) | p(j,b) | p(g(m),j). [para(84(b,1),140(b,1,1)),merge(e),merge(f)]. given #120 (T,wt=13): 519 p(m,k) | p(m,j) | p(j,b) | p(g(j),m). [para(84(b,1),140(b,2)),merge(e),merge(f)]. given #121 (T,wt=13): 531 p(j,b) | p(g(j),j) | p(m,j) | j = k. [factor(527,a,c),flip(e),merge(c)]. given #122 (T,wt=13): 570 p(x,b) | p(x,g(x)) | p(x,k) | p(x,j). [factor(556,a,c),merge(c)]. given #123 (A,wt=23): 73 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | b = y | p(y,b) | g(y) != x. [para(34(c,1),16(c,2))]. given #124 (T,wt=13): 573 p(k,b) | p(k,g(k)) | p(b,b) | p(k,j). [factor(561,a,c),merge(c)]. given #125 (T,wt=13): 622 p(k,j) | p(k,b) | p(k,g(j)) | p(m,k). [para(65(a,1),442(b,1)),merge(b)]. given #126 (T,wt=13): 626 p(m,k) | p(k,j) | p(m,b) | p(k,g(j)). [para(96(b,1),442(b,1)),merge(c),merge(f)]. given #127 (T,wt=13): 649 p(k,j) | p(j,b) | p(k,g(k)) | p(m,k). [para(65(a,1),443(c,1)),merge(b)]. given #128 (A,wt=23): 74 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | x = y | p(y,b) | p(y,g(y)). [para(34(c,1),20(a,1))]. given #129 (T,wt=13): 653 p(m,k) | p(k,j) | p(j,b) | p(m,g(k)). [para(96(b,1),443(c,1)),merge(c),merge(f)]. given #130 (T,wt=13): 663 p(k,j) | p(m,k) | p(k,b) | p(m,g(j)). [para(65(a,1),450(c,1)),merge(c)]. given #131 (T,wt=13): 667 p(m,k) | p(k,j) | p(m,b) | p(m,g(j)). [para(96(b,1),450(c,1)),merge(c),merge(d)]. given #132 (T,wt=13): 676 p(k,j) | p(m,k) | p(j,b) | p(k,g(m)). [para(65(a,1),451(d,1)),merge(c)]. given #133 (A,wt=23): 75 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),34(c,1))]. given #134 (T,wt=13): 680 p(m,k) | p(k,j) | p(j,b) | p(m,g(m)). [para(96(b,1),451(d,1)),merge(c),merge(d)]. given #135 (T,wt=13): 746 p(m,k) | p(m,j) | p(m,b) | p(m,g(j)). [para(84(b,1),470(c,1)),merge(c),merge(d)]. given #136 (T,wt=13): 759 p(m,k) | p(m,j) | p(j,b) | p(m,g(m)). [para(84(b,1),471(d,1)),merge(c),merge(d)]. given #137 (T,wt=13): 765 p(j,b) | p(j,g(j)) | p(m,j) | j = b. [para(135(d,1),483(d,2)),merge(d),merge(e),merge(f)]. given #138 (A,wt=23): 76 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | x = y | p(y,b) | p(g(y),y). [para(34(c,1),22(a,1))]. given #139 (T,wt=13): 772 p(k,j) | p(j,b) | p(g(k),k) | p(m,k). [para(65(a,1),490(c,2)),merge(b)]. given #140 (T,wt=13): 776 p(m,k) | p(k,j) | p(j,b) | p(g(k),m). [para(96(b,1),490(c,2)),merge(c),merge(f)]. given #141 (T,wt=13): 798 p(m,k) | p(k,j) | p(j,b) | p(g(m),k). [para(96(b,1),491(c,1,1)),merge(c),merge(f)]. given #142 (T,wt=13): 813 p(m,k) | p(k,j) | p(j,b) | p(g(m),m). [para(96(b,1),498(d,2)),merge(c),merge(d)]. given #143 (A,wt=23): 77 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),34(c,1))]. given #144 (T,wt=13): 932 p(m,k) | p(m,j) | p(j,b) | p(g(m),m). [para(84(b,1),518(d,2)),merge(c),merge(d)]. given #145 (T,wt=13): 959 p(j,b) | p(g(j),j) | p(m,j) | j = b. [para(141(d,1),531(d,2)),merge(d),merge(e),merge(f)]. given #146 (T,wt=13): 1023 p(k,j) | p(m,k) | p(m,b) | p(k,g(k)). [para(65(a,1),626(d,2,1)),merge(c)]. given #147 (T,wt=13): 1027 p(m,k) | p(k,j) | p(m,b) | p(k,g(m)). [para(96(b,1),626(d,2,1)),merge(c),merge(d)]. given #148 (A,wt=22): 78 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | k = y | x != y | p(y,k). [para(34(c,1),26(b,1))]. given #149 (T,wt=13): 1065 p(m,k) | p(m,j) | p(k,b) | p(m,g(j)). [para(51(a,1),663(a,1)),merge(c)]. given #150 (T,wt=14): 102 p(f(b),b) | p(f(b),g(f(b))) | -p(f(b),m). [factor(99,a,c),merge(c)]. given #151 (T,wt=14): 231 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(b),m). [factor(228,a,c),merge(c)]. given #152 (T,wt=15): 85 p(m,k) | k = x | m = x | b = x | -p(x,m). [para(51(a,1),6(d,2))]. given #153 (A,wt=16): 79 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | m != x. [para(34(c,1),27(a,2))]. given #154 (T,wt=15): 88 p(b,k) | k = x | m = x | b = x | -p(x,b). [para(54(a,1),6(d,2))]. given #155 (T,wt=15): 103 p(b,k) | b = x | m = x | -p(m,x) | -p(x,m). [resolve(98,b,4,b),flip(b),flip(d),unit_del(b,27)]. given #156 (T,wt=15): 112 p(m,j) | k = b | j = x | -p(x,m) | k = x. [para(62(a,1),31(b,2))]. given #157 (T,wt=15): 119 p(m,k) | p(m,j) | j = x | -p(x,m) | k = x. [para(84(b,1),31(b,2))]. given #158 (A,wt=29): 80 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(34(c,1),34(c,1))]. given #159 (T,wt=15): 125 k = b | p(k,j) | j = x | -p(x,m) | k = x. [para(94(b,1),31(b,2))]. given #160 (T,wt=15): 127 p(m,k) | p(k,j) | j = x | -p(x,m) | k = x. [para(96(b,1),31(b,2))]. given #161 (T,wt=15): 284 p(m,j) | k = b | p(j,k) | j = b | -p(b,k). [factor(283,b,f)]. given #162 (T,wt=15): 312 p(b,k) | j = m | p(j,m) | j = b | -p(j,b). [resolve(311,b,2,f),flip(b),flip(e),unit_del(d,27)]. given #163 (A,wt=22): 81 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = b | g(g(x)) != x. [factor(73,a,e),flip(d)]. given #164 (T,wt=15): 313 p(b,k) | p(b,m) | j = m | j = b | -p(j,b). [resolve(311,b,2,e),flip(d),unit_del(b,27)]. given #165 (T,wt=15): 1254 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(b)),m). [factor(1249,a,c),merge(c)]. given #166 (T,wt=15): 1260 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(b)),m). [factor(1256,a,c),merge(c)]. given #167 (T,wt=16): 155 p(k,b) | p(k,g(k)) | j = x | p(x,j) | b != x. [para(137(c,1),33(c,1))]. given #168 (A,wt=17): 82 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = x. [factor(74,a,e),flip(d),merge(e)]. given #169 (T,wt=16): 166 p(k,b) | p(g(k),k) | j = x | p(x,j) | b != x. [para(143(c,1),33(c,1))]. given #170 (T,wt=16): 190 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | m != x. [para(39(c,1),27(a,2))]. given #171 (T,wt=16): 218 p(m,k) | p(k,b) | g(k) = m | p(f(g(k)),g(k)). [resolve(164,c,14,b),flip(c)]. given #172 (T,wt=12): 1349 p(m,k) | p(k,b) | p(f(g(k)),g(k)). [para(218(c,1),142(b,1)),merge(d),merge(e),merge(f)]. given #173 (A,wt=19): 92 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | k = x | p(b,k). [para(34(c,1),54(a,2))]. given #174 (T,wt=12): 1362 p(m,k) | p(k,b) | p(f(g(m)),g(k)). [para(51(a,1),1349(c,1,1,1)),merge(b)]. given #175 (T,wt=12): 1363 p(m,k) | p(k,b) | p(f(g(k)),g(m)). [para(51(a,1),1349(c,2,1)),merge(b)]. given #176 (T,wt=12): 1386 p(m,k) | p(k,b) | p(f(g(m)),g(m)). [para(51(a,1),1362(c,2,1)),merge(b)]. given #177 (T,wt=16): 219 p(m,k) | p(k,b) | g(k) = m | p(g(k),f(g(k))). [resolve(164,c,12,b),flip(c)]. given #178 (A,wt=20): 99 p(x,b) | p(x,g(x)) | p(f(b),b) | p(f(b),g(f(b))) | -p(x,m). [para(20(a,1),35(c,1))]. given #179 (T,wt=12): 1434 p(m,k) | p(k,b) | p(g(k),f(g(k))). [para(219(c,1),142(b,1)),merge(d),merge(e),merge(f)]. given #180 (T,wt=12): 1453 p(m,k) | p(k,b) | p(g(m),f(g(k))). [para(51(a,1),1434(c,1,1)),merge(b)]. given #181 (T,wt=12): 1454 p(m,k) | p(k,b) | p(g(k),f(g(m))). [para(51(a,1),1434(c,2,1,1)),merge(b)]. given #182 (T,wt=12): 1476 p(m,k) | p(k,b) | p(g(m),f(g(m))). [para(51(a,1),1453(c,2,1,1)),merge(b)]. given #183 (A,wt=20): 100 p(x,b) | p(g(x),x) | p(f(b),b) | p(f(b),g(f(b))) | -p(x,m). [para(22(a,1),35(c,1))]. given #184 (T,wt=16): 318 p(x,k) | p(x,b) | p(g(x),x) | j = x | p(x,j). [resolve(52,a,33,c)]. given #185 (T,wt=16): 321 p(x,k) | p(x,b) | p(g(x),x) | k = b | m = x. [para(52(a,1),29(b,1)),flip(e)]. given #186 (T,wt=13): 1542 p(x,k) | p(x,b) | p(g(x),x) | k = b. [resolve(321,e,60,c),merge(e),merge(f)]. given #187 (T,wt=13): 1569 p(x,k) | p(x,b) | p(g(x),x) | p(m,k). [para(1542(d,1),51(a,1)),flip(d),unit_del(d,27)]. given #188 (A,wt=26): 101 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(34(c,1),35(c,1))]. given #189 (T,wt=16): 324 p(x,k) | p(x,b) | p(g(x),x) | j = x | p(k,j). [para(52(a,1),65(a,2))]. given #190 (T,wt=16): 341 p(x,k) | p(x,b) | p(x,g(x)) | k = b | m = x. [para(53(a,1),29(b,1)),flip(e)]. given #191 (T,wt=13): 1605 p(x,k) | p(x,b) | p(x,g(x)) | k = b. [resolve(341,e,59,c),merge(e),merge(f)]. given #192 (T,wt=13): 1625 p(x,k) | p(x,b) | p(x,g(x)) | p(m,k). [para(1605(d,1),51(a,1)),flip(d),unit_del(d,27)]. given #193 (A,wt=19): 106 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,k) | p(m,x). [para(34(c,1),98(b,2))]. given #194 (T,wt=13): 1665 p(x,k) | p(x,b) | p(x,g(x)) | p(m,x). [factor(1650,a,d),merge(d),merge(e)]. given #195 (T,wt=13): 1669 p(x,k) | p(x,b) | p(x,g(x)) | p(m,b). [factor(1657,a,d),merge(d),merge(e)]. given #196 (T,wt=16): 344 p(x,k) | p(x,b) | p(x,g(x)) | j = x | p(k,j). [para(53(a,1),65(a,2))]. given #197 (T,wt=16): 394 p(j,b) | p(j,g(j)) | p(b,k) | j = m | k = m. [resolve(104,d,31,b)]. given #198 (A,wt=19): 109 p(m,b) | g(m) = b | -p(g(m),b) | g(m) = m | -p(m,g(m)). [resolve(57,b,4,e),flip(b),flip(d),flip(e),unit_del(d,27)]. given #199 (T,wt=13): 1721 p(j,b) | p(j,g(j)) | p(b,k) | k = m. [resolve(394,d,59,c(flip)),merge(e),merge(f)]. given #200 (T,wt=10): 1730 p(j,b) | p(j,g(j)) | p(b,k). [para(1721(d,1),54(a,1)),merge(e),unit_del(d,27)]. given #201 (T,wt=16): 474 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(j)). [para(118(c,1),134(b,1)),merge(f),merge(g)]. given #202 (T,wt=13): 1753 p(m,k) | p(m,j) | p(j,b) | p(k,g(j)). [para(84(b,1),474(c,1)),merge(c),merge(d),merge(e)]. given #203 (A,wt=19): 110 p(m,b) | g(m) = b | -p(g(m),b) | g(m) = m | -p(g(m),m). [resolve(58,b,4,f),flip(b),flip(d),flip(e),unit_del(d,27)]. given #204 (T,wt=13): 1762 p(m,k) | p(m,j) | p(m,b) | p(k,g(j)). [para(84(b,1),1753(c,1)),merge(c),merge(d)]. given #205 (T,wt=13): 1783 p(m,k) | p(m,j) | p(m,b) | p(k,g(m)). [para(84(b,1),1762(d,2,1)),merge(c),merge(d)]. given #206 (T,wt=15): 1768 p(m,b) | g(m) = b | -p(g(m),b) | g(m) = m. [resolve(110,e,57,b),merge(e)]. given #207 (T,wt=16): 475 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(j,g(k)). [para(118(c,1),134(b,2,1)),merge(f),merge(g)]. given #208 (A,wt=25): 114 p(x,b) | p(x,g(x)) | -p(m,x) | g(m) = b | g(m) = m | -p(g(m),m) | p(m,b). [resolve(36,g,58,b),flip(c),flip(e),unit_del(c,27)]. given #209 (T,wt=16): 522 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),j). [para(118(c,1),140(b,1,1)),merge(f),merge(g)]. given #210 (T,wt=16): 523 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(j),k). [para(118(c,1),140(b,2)),merge(f),merge(g)]. given #211 (T,wt=16): 558 k = b | p(x,b) | p(x,g(x)) | p(b,m) | p(x,j). [para(29(b,1),314(c,2))]. given #212 (T,wt=13): 1861 p(b,b) | p(b,g(b)) | p(b,m) | p(b,j). [factor(1859,a,e)]. given #213 (A,wt=32): 144 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(136,b,36,h),flip(e),flip(g),flip(h)]. given #214 (T,wt=16): 560 p(m,k) | p(x,b) | p(x,g(x)) | p(b,m) | p(x,j). [para(51(a,1),314(c,2))]. given #215 (T,wt=16): 576 p(j,b) | p(j,g(j)) | p(k,j) | p(b,b) | p(j,j). [factor(564,a,d),merge(d)]. given #216 (T,wt=16): 578 p(j,b) | p(j,g(j)) | p(m,j) | p(b,b) | p(j,j). [factor(565,a,d),merge(d)]. given #217 (T,wt=16): 761 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(m)). [para(118(c,1),471(d,1)),merge(d),merge(e)]. given #218 (A,wt=31): 145 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(136,b,36,g),flip(e),flip(g)]. given #219 (T,wt=13): 1993 p(m,k) | p(m,j) | p(j,b) | p(k,g(m)). [para(84(b,1),761(c,1)),merge(c),merge(d),merge(e)]. given #220 (T,wt=16): 934 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(m),k). [para(118(c,1),518(d,2)),merge(d),merge(e)]. given #221 (T,wt=16): 951 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),m). [para(118(c,1),519(d,1,1)),merge(d),merge(e)]. given #222 (T,wt=16): 984 k = b | p(k,b) | p(m,g(k)) | p(b,b) | p(k,j). [para(29(b,1),573(b,1))]. given #223 (A,wt=25): 147 p(k,b) | p(m,k) | g(k) = b | -p(g(k),b) | k = b | g(k) = k | -p(g(k),k). [resolve(136,b,4,f),flip(c),flip(e),flip(f)]. given #224 (T,wt=16): 985 k = b | p(k,b) | p(k,g(m)) | p(b,b) | p(k,j). [para(29(b,1),573(b,2,1))]. given #225 (T,wt=16): 1268 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(m,k). [resolve(79,d,51,a(flip))]. given #226 (T,wt=16): 1269 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | k = b. [resolve(79,d,29,b(flip))]. given #227 (T,wt=16): 1310 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(b))),m). [factor(1305,a,c),merge(c)]. given #228 (A,wt=20): 152 p(k,b) | p(k,g(k)) | p(x,b) | p(x,g(x)) | j = x | p(x,j). [resolve(38,c,33,c)]. given #229 (T,wt=16): 1316 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(b))),m). [factor(1312,a,c),merge(c)]. given #230 (T,wt=16): 1340 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | p(m,k). [resolve(190,d,51,a(flip))]. given #231 (T,wt=16): 1341 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | k = b. [resolve(190,d,29,b(flip))]. given #232 (T,wt=16): 1538 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | j = k. [factor(1520,a,f)]. given #233 (A,wt=23): 153 p(f(x),b) | p(f(x),g(f(x))) | p(x,b) | p(x,g(x)) | m = x | -p(x,m). [resolve(38,c,10,c)]. given #234 (T,wt=16): 1563 p(x,k) | p(x,b) | p(g(x),x) | j = b | p(b,j). [resolve(1542,d,33,c)]. given #235 (T,wt=16): 1570 p(x,k) | p(x,b) | p(g(x),x) | j = b | p(k,j). [para(1542(d,1),65(a,2))]. given #236 (T,wt=16): 1619 p(x,k) | p(x,b) | p(x,g(x)) | j = b | p(b,j). [resolve(1605,d,33,c)]. given #237 (T,wt=16): 1626 p(x,k) | p(x,b) | p(x,g(x)) | j = b | p(k,j). [para(1605(d,1),65(a,2))]. given #238 (A,wt=19): 154 p(k,b) | p(k,g(k)) | k = x | m = x | b = x | -p(x,b). [para(137(c,1),6(d,2))]. given #239 (T,wt=16): 1693 p(j,k) | p(j,b) | p(j,g(j)) | j = m | k = m. [resolve(1665,d,31,b)]. given #240 (T,wt=13): 2224 p(j,k) | p(j,b) | p(j,g(j)) | k = m. [resolve(1693,d,59,c(flip)),merge(e),merge(f)]. given #241 (T,wt=10): 2242 p(j,k) | p(j,b) | p(j,g(j)). [factor(2238,a,d),merge(d),merge(e)]. given #242 (T,wt=13): 2255 p(k,j) | p(j,k) | p(j,b) | p(k,g(j)). [para(65(a,1),2242(c,1))]. given #243 (A,wt=18): 159 p(k,b) | p(m,k) | g(k) = k | g(k) = m | g(k) = b. [resolve(142,b,6,d),flip(c),flip(d),flip(e)]. given #244 (T,wt=13): 2256 p(k,j) | p(j,k) | p(j,b) | p(j,g(k)). [para(65(a,1),2242(c,2,1))]. given #245 (T,wt=13): 2304 p(k,j) | p(k,k) | p(j,b) | p(k,g(j)). [para(65(a,1),2255(b,1)),merge(b)]. given #246 (T,wt=13): 2336 p(k,j) | p(j,k) | p(j,b) | p(k,g(k)). [para(65(a,1),2256(d,1)),merge(b)]. given #247 (T,wt=13): 2366 p(k,j) | p(k,k) | p(k,b) | p(k,g(j)). [para(65(a,1),2304(c,1)),merge(b)]. given #248 (A,wt=19): 165 p(k,b) | p(g(k),k) | k = x | m = x | b = x | -p(x,b). [para(143(c,1),6(d,2))]. given #249 (T,wt=13): 2375 p(k,j) | p(k,k) | p(j,b) | p(k,g(k)). [para(65(a,1),2336(b,1)),merge(b)]. given #250 (T,wt=13): 2376 p(k,b) | p(k,g(k)) | p(k,j) | p(j,b). [para(137(c,1),2336(b,2)),merge(e),merge(f)]. given #251 (T,wt=10): 2449 p(k,j) | p(k,b) | p(k,g(k)). [para(65(a,1),2376(d,1)),merge(d),merge(e)]. given #252 (T,wt=13): 2460 k = b | p(k,j) | p(k,b) | p(m,g(k)). [para(29(b,1),2449(c,1))]. given #253 (A,wt=22): 169 p(m,k) | p(m,g(k)) | k = b | b = x | k = x | -p(k,x) | -p(x,k). [resolve(150,b,4,b),flip(c),flip(e)]. given #254 (T,wt=13): 2461 k = b | p(k,j) | p(k,b) | p(k,g(m)). [para(29(b,1),2449(c,2,1))]. given #255 (T,wt=13): 2490 p(k,j) | p(k,b) | p(m,g(k)) | j = b. [para(2460(a,1),65(a,2)),merge(e)]. given #256 (T,wt=13): 2507 p(k,j) | p(k,b) | p(k,g(m)) | j = b. [para(2461(a,1),65(a,2)),merge(e)]. given #257 (T,wt=14): 2309 p(j,b) | p(j,g(j)) | p(k,j) | p(k,g(j)). [para(133(c,1),2255(b,2)),merge(d),merge(e),merge(f)]. given #258 (A,wt=17): 170 p(x,b) | p(x,g(x)) | p(m,k) | p(k,x) | p(m,g(k)). [para(20(a,1),150(b,2))]. given #259 (T,wt=10): 2544 p(k,j) | p(j,b) | p(k,g(j)). [para(65(a,1),2309(b,1)),merge(d),merge(e)]. given #260 (T,wt=10): 2568 p(k,j) | p(k,b) | p(k,g(j)). [para(65(a,1),2544(b,1)),merge(b)]. given #261 (T,wt=13): 2570 k = b | p(k,j) | p(m,b) | p(k,g(j)). [para(94(b,1),2544(b,1)),merge(c)]. given #262 (T,wt=13): 2588 k = b | p(k,j) | p(k,b) | p(m,g(j)). [para(29(b,1),2568(c,1))]. given #263 (A,wt=17): 171 p(x,b) | p(g(x),x) | p(m,k) | p(k,x) | p(m,g(k)). [para(22(a,1),150(b,2))]. given #264 (T,wt=13): 2609 p(k,j) | p(m,b) | p(k,g(j)) | j = b. [para(2570(a,1),65(a,2)),merge(e)]. given #265 (T,wt=13): 2621 p(k,j) | p(k,b) | p(m,g(j)) | j = b. [para(2588(a,1),65(a,2)),merge(e)]. given #266 (T,wt=13): 2647 p(k,j) | p(m,b) | p(k,g(j)) | p(b,b). [para(2609(d,1),2544(b,1)),merge(d),merge(f)]. given #267 (T,wt=13): 2668 p(k,j) | p(m,b) | p(k,g(k)) | p(b,b). [para(65(a,1),2647(c,2,1)),merge(b)]. given #268 (A,wt=23): 173 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(m,k) | p(k,x) | p(m,g(k)). [para(34(c,1),150(b,2))]. given #269 (T,wt=14): 2323 p(m,k) | p(k,b) | g(k) = m | g(k) = b. [para(51(a,1),159(c,2)),merge(c),merge(e)]. given #270 (T,wt=10): 2721 p(m,k) | p(k,b) | g(k) = b. [para(2323(c,1),142(b,1)),merge(d),merge(e),merge(f)]. given #271 (T,wt=6): 2730 p(m,k) | p(k,b). [para(2721(c,1),136(b,2)),merge(c),merge(d),merge(e)]. given #272 (T,wt=6): 2739 p(m,k) | p(m,b). [para(51(a,1),2730(b,1)),merge(b)]. given #273 (A,wt=19): 175 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | k = x | p(x,k). [resolve(39,c,26,b)]. given #274 (T,wt=9): 2747 k = b | p(m,m) | p(m,b). [para(29(b,1),2739(a,2))]. given #275 (T,wt=6): 2813 p(m,m) | p(m,b). [para(2747(a,1),2739(a,2)),merge(c),merge(d)]. given #276 (T,wt=10): 2748 p(k,b) | p(k,g(k)) | p(m,b). [para(137(c,1),2739(a,2)),merge(d)]. given #277 (T,wt=10): 2749 p(k,b) | p(g(k),k) | p(m,b). [para(143(c,1),2739(a,2)),merge(d)]. given #278 (A,wt=19): 179 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | j = b | p(b,j). [resolve(39,c,33,c(flip))]. given #279 (T,wt=10): 2761 p(k,j) | p(m,b) | p(k,g(j)). [para(2570(a,1),2739(a,2)),merge(d),merge(e)]. given #280 (T,wt=10): 2875 p(k,j) | p(m,b) | p(k,g(k)). [para(65(a,1),2761(c,2,1)),merge(b)]. given #281 (T,wt=12): 2743 p(m,b) | p(k,j) | j = m | k = m. [resolve(2739,a,95,c)]. given #282 (T,wt=9): 2901 p(m,b) | p(k,j) | k = m. [para(2743(c,1),65(a,1)),flip(d),merge(d),merge(e)]. given #283 (A,wt=23): 181 p(g(g(x)),b) | p(g(g(g(x))),g(g(x))) | p(g(x),b) | b = x | p(x,b). [resolve(39,c,16,c(flip))]. given #284 (T,wt=9): 2905 p(m,b) | p(k,j) | j = m. [para(2901(c,1),65(a,2)),merge(d)]. given #285 (T,wt=10): 2912 p(m,b) | p(k,j) | p(m,g(j)). [para(2901(c,1),2761(c,1)),merge(c),merge(d)]. given #286 (T,wt=10): 2913 p(m,b) | p(k,j) | p(m,g(k)). [para(2901(c,1),2875(c,1)),merge(c),merge(d)]. given #287 (T,wt=10): 2914 p(m,b) | p(k,j) | p(k,g(m)). [para(2901(c,1),2875(c,2,1)),merge(c),merge(d)]. given #288 (A,wt=20): 182 p(g(f(b)),b) | p(g(g(f(b))),g(f(b))) | p(f(b),b) | -p(b,m). [resolve(39,c,10,c(flip)),unit_del(d,27)]. given #289 (T,wt=13): 2735 p(x,b) | p(x,g(x)) | p(m,k) | p(k,x). [para(20(a,1),2730(b,2))]. given #290 (T,wt=13): 2736 p(x,b) | p(g(x),x) | p(m,k) | p(k,x). [para(22(a,1),2730(b,2))]. given #291 (T,wt=13): 2751 p(j,b) | p(j,g(j)) | p(k,j) | p(m,b). [para(133(c,1),2739(a,2)),merge(e)]. given #292 (T,wt=13): 2752 p(j,b) | p(j,g(j)) | p(m,j) | p(m,b). [para(135(d,1),2739(a,2)),merge(e)]. given #293 (A,wt=31): 183 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(39(c,1),4(b,2))]. given #294 (T,wt=13): 2753 p(j,b) | p(g(j),j) | p(k,j) | p(m,b). [para(139(c,1),2739(a,2)),merge(e)]. given #295 (T,wt=13): 2754 p(j,b) | p(g(j),j) | p(m,j) | p(m,b). [para(141(d,1),2739(a,2)),merge(e)]. given #296 (T,wt=13): 2756 p(x,k) | p(x,b) | p(g(x),x) | p(m,b). [para(1542(d,1),2739(a,2)),merge(e)]. given #297 (T,wt=13): 2824 k = b | p(k,b) | p(m,g(k)) | p(m,b). [para(29(b,1),2748(b,1))]. given #298 (A,wt=23): 184 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | b = y | p(y,b) | g(y) != x. [para(39(c,1),16(c,2))]. given #299 (T,wt=10): 3329 p(k,b) | p(m,g(k)) | p(m,b). [para(2824(a,1),2739(a,2)),merge(d),merge(e)]. given #300 (T,wt=10): 3337 k = b | p(m,b) | p(m,g(k)). [para(29(b,1),3329(a,1)),merge(d)]. given #301 (T,wt=7): 3353 p(m,b) | p(m,g(k)). [para(3337(a,1),2739(a,2)),merge(c),merge(d)]. given #302 (T,wt=13): 2825 k = b | p(k,b) | p(k,g(m)) | p(m,b). [para(29(b,1),2748(b,2,1))]. given #303 (A,wt=23): 185 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | x = y | p(y,b) | p(y,g(y)). [para(39(c,1),20(a,1))]. given #304 (T,wt=10): 3378 p(k,b) | p(k,g(m)) | p(m,b). [para(2825(a,1),2739(a,2)),merge(d),merge(e)]. given #305 (T,wt=13): 2841 k = b | p(k,b) | p(g(m),k) | p(m,b). [para(29(b,1),2749(b,1,1))]. given #306 (T,wt=10): 3404 p(k,b) | p(g(m),k) | p(m,b). [para(2841(a,1),2739(a,2)),merge(d),merge(e)]. given #307 (T,wt=13): 2842 k = b | p(k,b) | p(g(k),m) | p(m,b). [para(29(b,1),2749(b,2))]. given #308 (A,wt=23): 186 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),39(c,1))]. given #309 (T,wt=10): 3428 p(k,b) | p(g(k),m) | p(m,b). [para(2842(a,1),2739(a,2)),merge(d),merge(e)]. given #310 (T,wt=13): 3038 k = b | p(m,b) | p(m,j) | p(m,g(j)). [para(29(b,1),2912(b,1))]. given #311 (T,wt=10): 3455 p(m,b) | p(m,j) | p(m,g(j)). [para(3038(a,1),2739(a,2)),merge(d),merge(e)]. given #312 (T,wt=13): 3085 p(m,k) | p(x,b) | p(x,g(x)) | p(m,x). [para(51(a,1),2735(d,1)),merge(d)]. given #313 (A,wt=23): 187 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | x = y | p(y,b) | p(g(y),y). [para(39(c,1),22(a,1))]. given #314 (T,wt=13): 3105 p(k,j) | p(j,b) | p(j,g(k)) | p(m,b). [para(65(a,1),2751(b,2,1)),merge(d)]. given #315 (T,wt=13): 3108 p(m,b) | p(k,j) | p(j,b) | p(j,g(m)). [para(2905(c,1),2751(b,2,1)),merge(e),merge(f)]. given #316 (T,wt=13): 3279 p(k,j) | p(j,b) | p(g(k),j) | p(m,b). [para(65(a,1),2753(b,1,1)),merge(d)]. given #317 (T,wt=13): 3280 p(k,j) | p(j,b) | p(g(j),k) | p(m,b). [para(65(a,1),2753(b,2)),merge(d)]. given #318 (A,wt=23): 188 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),39(c,1))]. given #319 (T,wt=13): 3285 p(m,b) | p(k,j) | p(j,b) | p(g(m),j). [para(2905(c,1),2753(b,1,1)),merge(e),merge(f)]. given #320 (T,wt=13): 3286 p(m,b) | p(k,j) | p(j,b) | p(g(j),m). [para(2905(c,1),2753(b,2)),merge(e),merge(f)]. given #321 (T,wt=13): 3538 p(k,j) | p(j,b) | p(g(k),k) | p(m,b). [para(65(a,1),3279(c,2)),merge(b)]. given #322 (T,wt=13): 3542 p(m,b) | p(k,j) | p(j,b) | p(g(k),m). [para(2905(c,1),3279(c,2)),merge(c),merge(f)]. given #323 (A,wt=22): 189 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | k = y | x != y | p(y,k). [para(39(c,1),26(b,1))]. given #324 (T,wt=13): 3562 p(m,b) | p(k,j) | p(j,b) | p(g(m),k). [para(2905(c,1),3280(c,1,1)),merge(c),merge(f)]. given #325 (T,wt=14): 2379 p(j,b) | p(j,g(j)) | p(k,j) | p(k,g(k)). [para(133(c,1),2336(b,2)),merge(d),merge(e),merge(f)]. given #326 (T,wt=14): 2380 p(j,b) | p(g(j),j) | p(k,j) | p(k,g(k)). [para(139(c,1),2336(b,2)),merge(d),merge(e),merge(f)]. given #327 (T,wt=14): 2462 p(k,b) | p(g(k),k) | p(k,j) | p(b,g(k)). [para(143(c,1),2449(c,1)),merge(d)]. given #328 (A,wt=29): 191 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(39(c,1),34(c,1))]. given #329 (T,wt=14): 2463 p(k,b) | p(g(k),k) | p(k,j) | p(k,g(b)). [para(143(c,1),2449(c,2,1)),merge(d)]. given #330 (T,wt=14): 2497 p(k,j) | p(k,b) | p(m,g(k)) | p(b,g(k)). [para(2460(a,1),2449(c,1)),merge(d),merge(e)]. given #331 (T,wt=14): 2498 p(k,j) | p(k,b) | p(m,g(k)) | p(k,g(b)). [para(2460(a,1),2449(c,2,1)),merge(d),merge(e)]. given #332 (T,wt=14): 2514 p(k,j) | p(k,b) | p(k,g(m)) | p(b,g(k)). [para(2461(a,1),2449(c,1)),merge(d),merge(e)]. given #333 (A,wt=29): 192 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(34(c,1),39(c,1))]. given #334 (T,wt=14): 2515 p(k,j) | p(k,b) | p(k,g(m)) | p(k,g(b)). [para(2461(a,1),2449(c,2,1)),merge(d),merge(e)]. given #335 (T,wt=14): 2589 p(k,b) | p(g(k),k) | p(k,j) | p(b,g(j)). [para(143(c,1),2568(c,1)),merge(d)]. given #336 (T,wt=14): 2601 p(k,j) | p(k,b) | p(m,g(k)) | p(b,g(j)). [para(2460(a,1),2568(c,1)),merge(d),merge(e)]. given #337 (T,wt=14): 2602 p(k,j) | p(k,b) | p(k,g(m)) | p(b,g(j)). [para(2461(a,1),2568(c,1)),merge(d),merge(e)]. given #338 (A,wt=19): 193 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | k = x | p(b,k). [para(39(c,1),54(a,2))]. given #339 (T,wt=14): 2627 p(k,j) | p(k,b) | p(m,g(j)) | p(b,g(k)). [para(2588(a,1),2449(c,1)),merge(d),merge(e)]. given #340 (T,wt=14): 2628 p(k,j) | p(k,b) | p(m,g(j)) | p(k,g(b)). [para(2588(a,1),2449(c,2,1)),merge(d),merge(e)]. given #341 (T,wt=14): 2629 p(k,j) | p(k,b) | p(m,g(j)) | p(b,g(j)). [para(2588(a,1),2568(c,1)),merge(d),merge(e)]. given #342 (T,wt=14): 3655 p(k,j) | p(j,b) | p(j,g(k)) | p(k,g(k)). [para(65(a,1),2379(b,2,1)),merge(d)]. given #343 (A,wt=26): 194 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(39(c,1),35(c,1))]. given #344 (T,wt=10): 3988 p(k,j) | p(j,b) | p(k,g(k)). [para(65(a,1),3655(c,1)),merge(b),merge(e)]. given #345 (T,wt=14): 3773 p(k,j) | p(k,b) | p(m,g(k)) | p(b,g(b)). [para(2460(a,1),2498(d,1)),merge(d),merge(e),merge(f)]. given #346 (T,wt=14): 3936 p(k,j) | p(k,b) | p(m,g(j)) | p(b,g(b)). [para(2588(a,1),2628(d,1)),merge(d),merge(e),merge(f)]. given #347 (T,wt=15): 2904 p(m,b) | p(k,j) | j = x | p(x,j) | m != x. [para(2901(c,1),33(c,1))]. given #348 (A,wt=19): 195 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,k) | p(m,x). [para(39(c,1),98(b,2))]. given #349 (T,wt=15): 2906 p(m,b) | p(k,j) | j = x | -p(x,m) | k = x. [para(2901(c,1),95(c,2)),merge(c)]. given #350 (T,wt=14): 4092 p(m,b) | p(k,j) | g(m) = j | g(m) = k. [resolve(2906,d,57,b),flip(c),flip(d),merge(e)]. given #351 (T,wt=10): 4095 p(k,j) | p(m,b) | g(m) = k. [para(65(a,1),4092(c,2)),merge(c),merge(e)]. given #352 (T,wt=9): 4097 p(k,j) | p(m,b) | k != b. [para(4095(c,1),16(c,1)),flip(c),merge(d),unit_del(c,27)]. given #353 (A,wt=29): 199 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(39(c,1),39(c,1))]. given #354 (T,wt=9): 4098 p(k,j) | p(m,b) | k != m. [para(4095(c,1),18(c,1)),flip(c),merge(d),unit_del(c,27)]. given #355 (T,wt=6): 4128 p(k,j) | p(m,b). [resolve(4098,c,2901,c),merge(c),merge(d)]. given #356 (T,wt=9): 4145 k = b | p(m,j) | p(m,b). [para(29(b,1),4128(a,1))]. given #357 (T,wt=6): 4157 p(m,j) | p(m,b). [para(4145(a,1),2739(a,2)),merge(c),merge(d)]. given #358 (A,wt=22): 200 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | g(x) = b | g(g(x)) != x. [factor(184,a,e),flip(d)]. given #359 (T,wt=9): 4170 p(m,b) | j = m | k = m. [resolve(4157,a,31,b)]. given #360 (T,wt=9): 4187 p(m,b) | k = m | p(k,m). [para(4170(b,1),4128(a,2)),merge(d)]. given #361 (T,wt=12): 4180 p(m,b) | k = m | j = k | p(j,k). [resolve(4170,b,24,b(flip)),flip(c)]. given #362 (T,wt=9): 4201 p(m,b) | k = m | p(j,k). [para(4180(c,1),4170(b,1)),merge(d),merge(e),merge(f)]. given #363 (A,wt=17): 201 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | g(x) = x. [factor(187,a,e),flip(d),merge(e)]. given #364 (T,wt=13): 4178 p(m,b) | k = m | p(j,b) | p(g(j),j). [resolve(4170,b,60,c(flip))]. given #365 (T,wt=13): 4179 p(m,b) | k = m | p(j,b) | p(j,g(j)). [resolve(4170,b,59,c(flip))]. given #366 (T,wt=15): 4171 p(m,b) | j = b | -p(j,b) | j = m | -p(j,m). [resolve(4157,a,4,f),flip(b),flip(d),flip(e),unit_del(d,27)]. given #367 (T,wt=15): 4181 p(m,b) | k = m | j = x | -p(x,m) | k = x. [para(4170(b,1),31(b,2))]. given #368 (A,wt=20): 227 p(x,b) | p(x,g(x)) | p(f(b),b) | p(g(f(b)),f(b)) | -p(x,m). [para(20(a,1),40(c,1))]. given #369 (T,wt=14): 4239 p(m,b) | k = m | g(m) = j | g(m) = k. [resolve(4181,d,57,b),flip(c),flip(d),merge(e)]. given #370 (T,wt=13): 4244 p(m,b) | k = m | g(m) = k | j != b. [para(4239(c,1),16(c,1)),flip(d),merge(e),unit_del(d,27)]. given #371 (T,wt=13): 4245 p(m,b) | k = m | g(m) = k | j != m. [para(4239(c,1),18(c,1)),flip(d),merge(e),unit_del(d,27)]. given #372 (T,wt=10): 4265 p(m,b) | k = m | g(m) = k. [resolve(4245,d,4170,b),merge(d),merge(e)]. given #373 (A,wt=20): 228 p(x,b) | p(g(x),x) | p(f(b),b) | p(g(f(b)),f(b)) | -p(x,m). [para(22(a,1),40(c,1))]. given #374 (T,wt=9): 4267 p(m,b) | k = m | k != b. [para(4265(c,1),16(c,1)),flip(c),merge(d),unit_del(c,27)]. given #375 (T,wt=11): 4272 p(m,b) | k = m | p(f(k),g(m)). [para(4265(c,1),415(b,1,1)),merge(c)]. given #376 (T,wt=11): 4273 p(m,b) | k = m | p(f(g(m)),k). [para(4265(c,1),415(b,2)),merge(c)]. given #377 (T,wt=11): 4274 p(m,b) | k = m | p(k,f(g(m))). [para(4265(c,1),425(b,1)),merge(c)]. given #378 (A,wt=26): 229 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(34(c,1),40(c,1))]. given #379 (T,wt=11): 4275 p(m,b) | k = m | p(g(m),f(k)). [para(4265(c,1),425(b,2,1)),merge(c)]. given #380 (T,wt=12): 4283 p(m,b) | k = m | p(k,b) | p(k,k). [para(4265(c,1),3378(b,2)),merge(e)]. given #381 (T,wt=14): 4266 p(m,b) | k = m | g(m) = j | p(g(m),j). [resolve(4265,c,33,c(flip)),flip(c)]. given #382 (T,wt=13): 4322 p(m,b) | k = m | p(g(m),j) | j != b. [para(4266(c,1),16(c,1)),flip(d),merge(e),unit_del(d,27)]. given #383 (A,wt=26): 230 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(39(c,1),40(c,1))]. given #384 (T,wt=13): 4323 p(m,b) | k = m | p(g(m),j) | j != m. [para(4266(c,1),18(c,1)),flip(d),merge(e),unit_del(d,27)]. given #385 (T,wt=10): 4350 p(m,b) | k = m | p(g(m),j). [resolve(4323,d,4170,b),merge(d),merge(e)]. given #386 (T,wt=15): 4189 p(m,b) | p(k,m) | j = x | p(x,j) | m != x. [para(4187(b,1),33(c,1))]. given #387 (T,wt=15): 4203 p(m,b) | p(j,k) | j = x | p(x,j) | m != x. [para(4201(b,1),33(c,1))]. given #388 (A,wt=25): 255 p(x,b) | p(g(x),x) | -p(m,x) | g(m) = b | g(m) = m | -p(g(m),m) | p(m,b). [resolve(41,g,58,b),flip(c),flip(e),unit_del(c,27)]. given #389 (T,wt=15): 4270 p(m,b) | k = m | p(g(m),b) | p(k,g(g(m))). [para(4265(c,1),69(b,1)),merge(e)]. given #390 (T,wt=15): 4271 p(m,b) | k = m | p(g(m),b) | p(g(m),g(k)). [para(4265(c,1),69(b,2,1)),merge(e)]. given #391 (T,wt=15): 4276 p(m,b) | k = m | p(g(m),b) | p(g(k),g(m)). [para(4265(c,1),180(b,1,1)),merge(e)]. given #392 (T,wt=15): 4277 p(m,b) | k = m | p(g(m),b) | p(g(g(m)),k). [para(4265(c,1),180(b,2)),merge(e)]. given #393 (A,wt=19): 274 p(x,b) | p(x,g(x)) | p(b,k) | j = y | p(y,j) | x != y. [para(20(a,1),91(d,1))]. given #394 (T,wt=15): 4355 p(m,b) | p(g(m),j) | g(m) = j | g(m) != m. [factor(4352,b,d),flip(c),flip(d)]. given #395 (T,wt=16): 1812 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(m,g(k)). [para(84(b,1),475(e,1)),merge(c),merge(d)]. given #396 (T,wt=13): 4389 p(m,k) | p(m,j) | p(j,b) | p(m,g(k)). [para(84(b,1),1812(c,1)),merge(c),merge(d),merge(e)]. given #397 (T,wt=16): 1814 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(k)). [para(118(c,1),475(e,1)),merge(d),merge(e),merge(f)]. given #398 (A,wt=19): 275 p(x,b) | p(g(x),x) | p(b,k) | j = y | p(y,j) | x != y. [para(22(a,1),91(d,1))]. given #399 (T,wt=13): 4413 p(m,k) | p(m,j) | p(j,b) | p(k,g(k)). [para(84(b,1),1814(c,1)),merge(c),merge(d),merge(e)]. given #400 (T,wt=16): 1829 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),k). [para(118(c,1),522(e,2)),merge(d),merge(e),merge(f)]. given #401 (T,wt=16): 1855 p(x,b) | p(x,g(x)) | k = x | p(b,m) | p(x,j). [factor(1845,a,d),merge(d)]. given #402 (T,wt=16): 1859 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | p(b,b). [factor(1852,a,e),merge(e),merge(g)]. given #403 (A,wt=25): 276 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,k) | j = y | p(y,j) | x != y. [para(34(c,1),91(d,1))]. given #404 (T,wt=14): 4501 p(b,b) | p(b,g(b)) | p(b,j) | p(f(b),b). [factor(4487,a,d)]. given #405 (T,wt=14): 4502 p(b,b) | p(b,g(b)) | p(b,j) | p(b,f(b)). [factor(4488,a,d)]. given #406 (T,wt=16): 1916 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | p(m,b). [factor(1903,a,f),merge(f),merge(g)]. given #407 (T,wt=16): 1930 p(k,j) | p(j,b) | p(j,g(k)) | p(b,b) | p(j,j). [para(65(a,1),576(b,2,1)),merge(d)]. given #408 (A,wt=25): 277 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,k) | j = y | p(y,j) | x != y. [para(39(c,1),91(d,1))]. given #409 (T,wt=16): 2151 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | j = b. [factor(2150,a,d),merge(d),merge(e)]. given #410 (T,wt=16): 2172 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | j = k. [factor(2159,a,f)]. given #411 (T,wt=16): 2174 p(x,b) | p(g(x),x) | p(x,k) | j = x | p(b,j). [factor(2161,a,d),merge(d)]. given #412 (T,wt=16): 2204 p(x,b) | p(x,g(x)) | p(x,k) | j = x | p(b,j). [factor(2191,a,d),merge(d)]. given #413 (A,wt=19): 282 p(k,b) | p(g(k),k) | p(k,j) | j = x | -p(x,b) | k = x. [para(143(c,1),95(c,2))]. given #414 (T,wt=16): 2257 p(m,j) | k = b | p(j,k) | p(j,b) | p(m,g(j)). [para(62(a,1),2242(c,1))]. given #415 (T,wt=16): 2258 p(m,j) | k = b | p(j,k) | p(j,b) | p(j,g(m)). [para(62(a,1),2242(c,2,1))]. given #416 (T,wt=16): 2259 k = b | p(k,j) | p(j,k) | p(j,b) | p(m,g(j)). [para(94(b,1),2242(c,1))]. given #417 (T,wt=16): 2260 k = b | p(k,j) | p(j,k) | p(j,b) | p(j,g(m)). [para(94(b,1),2242(c,2,1))]. given #418 (A,wt=18): 283 p(m,j) | k = b | p(j,k) | j = x | -p(x,k) | k = x. [para(111(c,1),31(b,2))]. given #419 (T,wt=16): 2261 p(m,j) | k = b | p(j,k) | p(j,b) | p(k,g(j)). [para(111(c,1),2242(c,1)),merge(d)]. given #420 (T,wt=16): 2262 p(m,j) | k = b | p(j,k) | p(j,b) | p(j,g(k)). [para(111(c,1),2242(c,2,1)),merge(d)]. given #421 (T,wt=16): 2338 k = b | p(k,j) | p(j,k) | p(j,b) | p(m,g(k)). [para(94(b,1),2256(d,1)),merge(c)]. given #422 (T,wt=16): 2757 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(m,b). [para(1269(d,1),2739(a,2)),merge(e)]. given #423 (A,wt=19): 285 p(x,b) | p(x,g(x)) | p(m,j) | k = b | j = b | -p(x,m). [para(20(a,1),113(d,1))]. given #424 (T,wt=16): 2758 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | p(m,b). [para(1341(d,1),2739(a,2)),merge(e)]. given #425 (T,wt=16): 3439 p(k,b) | p(m,b) | g(k) = m | p(f(g(k)),g(k)). [resolve(3428,b,14,b),flip(c)]. given #426 (T,wt=15): 4865 p(k,b) | p(m,b) | p(f(g(k)),g(k)) | p(k,m). [para(3439(c,1),2748(b,2)),merge(d),merge(f)]. given #427 (T,wt=15): 4902 p(m,b) | p(k,m) | p(k,b) | p(f(g(m)),g(k)). [para(4187(b,1),4865(c,1,1,1)),merge(d),merge(f)]. given #428 (A,wt=19): 286 p(x,b) | p(g(x),x) | p(m,j) | k = b | j = b | -p(x,m). [para(22(a,1),113(d,1))]. given #429 (T,wt=15): 4903 p(m,b) | p(k,m) | p(k,b) | p(f(g(k)),g(m)). [para(4187(b,1),4865(c,2,1)),merge(d),merge(f)]. given #430 (T,wt=16): 3440 p(k,b) | p(m,b) | g(k) = m | p(g(k),f(g(k))). [resolve(3428,b,12,b),flip(c)]. given #431 (T,wt=15): 4957 p(k,b) | p(m,b) | p(g(k),f(g(k))) | p(k,m). [para(3440(c,1),2748(b,2)),merge(d),merge(f)]. given #432 (T,wt=15): 4996 p(m,b) | p(k,m) | p(k,b) | p(g(m),f(g(k))). [para(4187(b,1),4957(c,1,1)),merge(d),merge(f)]. given #433 (A,wt=25): 287 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(m,j) | k = b | j = b | -p(x,m). [para(34(c,1),113(d,1))]. given #434 (T,wt=15): 4997 p(m,b) | p(k,m) | p(k,b) | p(g(k),f(g(m))). [para(4187(b,1),4957(c,2,1,1)),merge(d),merge(f)]. given #435 (T,wt=16): 3490 k = b | p(m,m) | p(x,b) | p(x,g(x)) | p(m,x). [para(29(b,1),3085(a,2))]. given #436 (T,wt=16): 4268 p(m,b) | k = m | p(x,b) | p(x,g(x)) | k != x. [para(4265(c,1),37(e,1)),flip(e),merge(f),unit_del(e,27)]. given #437 (T,wt=16): 4269 p(m,b) | k = m | p(x,b) | p(g(x),x) | k != x. [para(4265(c,1),42(e,1)),flip(e),merge(f),unit_del(e,27)]. given #438 (A,wt=25): 288 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(m,j) | k = b | j = b | -p(x,m). [para(39(c,1),113(d,1))]. given #439 (T,wt=16): 4352 p(m,b) | p(g(m),j) | j = x | p(x,j) | m != x. [para(4350(b,1),33(c,1))]. given #440 (T,wt=16): 4439 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | j = x. [resolve(1855,c,33,c),merge(f)]. given #441 (T,wt=16): 4459 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | p(b,x). [factor(4444,a,e),merge(e),merge(g)]. given #442 (T,wt=13): 5135 p(j,b) | p(j,g(j)) | p(b,m) | p(j,j). [factor(5117,f,g),merge(c),merge(d)]. given #443 (A,wt=18): 289 p(m,k) | p(m,j) | p(j,k) | j = x | -p(x,k) | k = x. [para(118(c,1),31(b,2))]. given #444 (T,wt=16): 4460 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | p(m,x). [factor(4445,a,f),merge(f),merge(g)]. given #445 (T,wt=16): 4503 p(x,b) | p(x,g(x)) | p(x,m) | p(x,j) | p(b,b). [factor(4489,a,c),merge(c)]. given #446 (T,wt=13): 5240 p(x,b) | p(x,g(x)) | p(x,m) | p(x,j). [factor(5235,a,c),merge(c)]. given #447 (T,wt=16): 4679 p(k,j) | p(j,k) | p(j,b) | p(m,g(j)) | j = b. [para(2259(a,1),65(a,2)),merge(f)]. given #448 (A,wt=19): 291 p(x,b) | p(x,g(x)) | k = b | p(k,j) | j = b | -p(x,m). [para(20(a,1),126(d,1))]. given #449 (T,wt=16): 4693 p(k,j) | p(j,k) | p(j,b) | p(j,g(m)) | j = b. [para(2260(a,1),65(a,2)),merge(f)]. given #450 (T,wt=16): 4748 p(k,j) | p(j,k) | p(j,b) | p(m,g(k)) | j = b. [para(2338(a,1),65(a,2)),merge(f)]. given #451 (T,wt=16): 5063 p(x,b) | p(x,g(x)) | k = x | p(m,m) | p(m,x). [factor(5042,a,e),merge(e)]. given #452 (T,wt=13): 5303 p(x,b) | p(x,g(x)) | p(m,m) | p(m,x). [factor(5299,a,e),merge(e),merge(f)]. given #453 (A,wt=19): 292 p(x,b) | p(g(x),x) | k = b | p(k,j) | j = b | -p(x,m). [para(22(a,1),126(d,1))]. given #454 (T,wt=16): 5133 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | p(x,x). [factor(5117,a,c),merge(c)]. given #455 (T,wt=14): 5354 p(j,b) | p(j,g(j)) | p(j,j) | p(f(b),b). [factor(5342,c,d)]. given #456 (T,wt=14): 5355 p(j,b) | p(j,g(j)) | p(j,j) | p(b,f(b)). [factor(5343,c,d)]. given #457 (T,wt=14): 5386 p(j,b) | p(j,g(j)) | p(j,j) | p(f(j),b). [factor(5374,a,c),merge(c)]. given #458 (A,wt=25): 293 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | k = b | p(k,j) | j = b | -p(x,m). [para(34(c,1),126(d,1))]. given #459 (T,wt=14): 5387 p(j,b) | p(j,g(j)) | p(j,j) | p(f(b),j). [factor(5375,a,c),merge(c)]. given #460 (T,wt=14): 5471 p(j,b) | p(j,g(j)) | p(j,j) | p(f(j),j). [factor(5463,a,c),merge(c)]. given #461 (T,wt=16): 5157 p(k,j) | p(j,b) | p(j,g(k)) | p(b,m) | p(j,j). [para(65(a,1),5135(b,2,1))]. given #462 (T,wt=16): 5320 p(j,b) | p(j,g(j)) | p(m,m) | j = m | k = m. [resolve(5303,d,31,b)]. given #463 (A,wt=25): 294 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | k = b | p(k,j) | j = b | -p(x,m). [para(39(c,1),126(d,1))]. given #464 (T,wt=13): 5546 p(j,b) | p(j,g(j)) | p(m,m) | k = m. [resolve(5320,d,59,c(flip)),merge(e),merge(f)]. given #465 (T,wt=13): 5559 p(j,b) | p(j,g(j)) | p(m,m) | p(k,j). [para(5546(d,1),133(c,1)),merge(d),merge(e),unit_del(d,27)]. given #466 (T,wt=13): 5580 p(k,j) | p(j,b) | p(j,g(k)) | p(m,m). [para(65(a,1),5559(b,2,1)),merge(e)]. given #467 (T,wt=16): 5583 k = b | p(k,j) | p(j,b) | p(m,g(j)) | p(m,m). [para(94(b,1),5559(b,1)),merge(f)]. given #468 (A,wt=20): 299 p(k,b) | p(g(k),k) | p(x,b) | p(x,g(x)) | j = x | p(x,j). [resolve(43,c,33,c)]. given #469 (T,wt=16): 5584 k = b | p(k,j) | p(j,b) | p(j,g(m)) | p(m,m). [para(94(b,1),5559(b,2,1)),merge(f)]. given #470 (T,wt=16): 5628 k = b | p(k,j) | p(j,b) | p(m,g(k)) | p(m,m). [para(94(b,1),5580(c,1)),merge(c)]. given #471 (T,wt=16): 5651 p(k,j) | p(j,b) | p(m,g(j)) | p(m,m) | j = b. [para(5583(a,1),65(a,2)),merge(f)]. given #472 (T,wt=16): 5689 p(k,j) | p(j,b) | p(j,g(m)) | p(m,m) | j = b. [para(5584(a,1),65(a,2)),merge(f)]. given #473 (A,wt=23): 300 p(f(x),b) | p(g(f(x)),f(x)) | p(x,b) | p(x,g(x)) | m = x | -p(x,m). [resolve(43,c,10,c)]. given #474 (T,wt=16): 5708 p(k,j) | p(j,b) | p(m,g(k)) | p(m,m) | j = b. [para(5628(a,1),65(a,2)),merge(f)]. given #475 (T,wt=17): 400 p(j,b) | p(b,k) | p(m,j) | g(j) = j | g(j) = k. [resolve(105,b,31,b),flip(d),flip(e)]. given #476 (T,wt=16): 5761 p(j,b) | p(b,k) | p(m,j) | g(j) = k | j = b. [resolve(400,d,18,c),flip(e),merge(f)]. given #477 (T,wt=15): 5770 p(j,b) | p(b,k) | p(m,j) | j = b | k != b. [para(5761(d,1),16(c,1)),flip(e),merge(e),merge(f)]. given #478 (A,wt=20): 301 p(x,b) | p(g(x),x) | p(k,b) | p(k,g(k)) | j = x | p(x,j). [resolve(43,c,33,c(flip))]. given #479 (T,wt=12): 5796 p(j,b) | p(b,k) | p(m,j) | j = b. [resolve(5770,e,54,a),merge(e)]. given #480 (T,wt=12): 5833 p(j,b) | p(b,k) | p(m,j) | p(k,b). [para(5796(d,1),308(a,2)),merge(e)]. given #481 (T,wt=12): 5834 p(j,b) | p(b,k) | p(m,j) | p(b,b). [para(5796(d,1),311(b,2)),merge(d)]. given #482 (T,wt=13): 5836 p(j,b) | p(b,k) | p(m,j) | p(b,g(j)). [para(5796(d,1),1730(b,1)),merge(d),merge(f)]. given #483 (A,wt=23): 302 p(x,b) | p(g(x),x) | p(f(x),b) | p(f(x),g(f(x))) | m = x | -p(x,m). [resolve(43,c,10,c(flip))]. given #484 (T,wt=13): 5837 p(j,b) | p(b,k) | p(m,j) | p(j,g(b)). [para(5796(d,1),1730(b,2,1)),merge(d),merge(f)]. given #485 (T,wt=13): 5899 p(j,b) | p(b,k) | p(m,j) | p(b,g(b)). [para(5796(d,1),5837(d,1)),merge(d),merge(e),merge(f)]. given #486 (T,wt=15): 5827 p(j,b) | p(b,k) | p(m,j) | j = k | p(j,k). [resolve(5796,d,26,b(flip)),flip(d)]. given #487 (T,wt=12): 5912 p(j,b) | p(b,k) | p(m,j) | p(j,k). [para(5827(d,1),311(b,2)),merge(e),merge(f)]. given #488 (A,wt=18): 309 p(b,k) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(308,a,2,f),flip(b),flip(d),flip(e)]. given #489 (T,wt=9): 5915 p(b,k) | p(j,b) | p(m,j). [para(54(a,1),5912(d,2)),merge(c),merge(e)]. given #490 (T,wt=15): 5925 p(b,k) | p(m,j) | p(b,m) | j = m | j = b. [resolve(5915,b,313,e),merge(c)]. given #491 (T,wt=12): 5938 p(b,k) | p(m,j) | p(b,m) | j = b. [para(5925(d,1),311(b,2)),merge(e),merge(f)]. given #492 (T,wt=12): 5949 p(b,k) | p(m,j) | p(b,m) | p(k,b). [para(5938(d,1),308(a,2)),merge(e)]. given #493 (A,wt=18): 310 p(b,k) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(308,a,2,e),flip(b),flip(d)]. given #494 (T,wt=12): 5950 p(b,k) | p(m,j) | p(b,m) | p(b,b). [para(5938(d,1),311(b,2)),merge(d)]. given #495 (T,wt=15): 5926 p(b,k) | p(m,j) | j = m | p(j,m) | j = b. [resolve(5915,b,312,e),merge(c)]. given #496 (T,wt=15): 5927 p(b,k) | p(m,j) | j = k | j = m | j = b. [resolve(5915,b,88,e),flip(d),flip(e),flip(f),merge(c)]. given #497 (T,wt=12): 5977 p(b,k) | p(m,j) | j = b | j = m. [para(54(a,1),5927(c,2)),merge(b),merge(f)]. given #498 (A,wt=19): 316 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,k) | p(x,j). [para(34(c,1),311(b,1))]. given #499 (T,wt=12): 5980 p(b,k) | p(m,j) | j = b | p(k,m). [para(5977(d,1),308(a,2)),merge(e)]. given #500 (T,wt=12): 6006 p(b,k) | p(m,j) | p(k,m) | p(k,b). [para(5980(c,1),308(a,2)),merge(e)]. given #501 (T,wt=12): 6007 p(b,k) | p(m,j) | p(k,m) | p(b,b). [para(5980(c,1),311(b,2)),merge(d)]. given #502 (T,wt=15): 5943 p(b,k) | p(m,j) | p(b,m) | j = k | p(j,k). [resolve(5938,d,26,b(flip)),flip(d)]. given #503 (A,wt=19): 317 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,k) | p(x,j). [para(39(c,1),311(b,1))]. given #504 (T,wt=12): 6043 p(b,k) | p(m,j) | p(b,m) | p(j,k). [para(5943(d,1),311(b,2)),merge(e),merge(f)]. given #505 (T,wt=9): 6059 p(b,k) | p(m,j) | p(b,m). [para(5938(d,1),6043(d,1)),merge(d),merge(e),merge(f),merge(g)]. given #506 (T,wt=12): 6062 p(b,k) | p(b,m) | j = m | k = m. [resolve(6059,b,31,b)]. given #507 (T,wt=9): 6069 p(b,k) | p(b,m) | k = m. [para(6062(c,1),311(b,2)),merge(d),merge(e)]. given #508 (A,wt=20): 319 p(f(k),k) | p(f(k),b) | p(g(f(k)),f(k)) | k = m | -p(k,m). [resolve(52,a,10,c(flip)),flip(d)]. given #509 (T,wt=6): 6076 p(b,k) | p(b,m). [para(6069(c,1),54(a,1)),merge(d),unit_del(c,27)]. given #510 (T,wt=6): 6100 k = b | p(b,m). [para(29(b,1),6076(a,2)),merge(c)]. given #511 (T,wt=6): 6102 p(m,k) | p(b,m). [para(51(a,1),6076(a,2)),merge(c)]. given #512 (T,wt=6): 6159 p(b,m) | p(m,b). [para(6100(a,1),2739(a,2)),merge(c)]. given #513 (A,wt=22): 320 p(x,k) | p(x,b) | p(g(x),x) | k = y | m = y | b = y | -p(y,x). [para(52(a,1),6(d,2))]. given #514 (T,wt=6): 6170 p(b,m) | p(b,b). [para(6100(a,1),6076(a,2)),merge(c)]. given #515 (T,wt=7): 6207 p(b,b) | p(f(b),b). [resolve(6170,a,14,b),unit_del(b,27)]. given #516 (T,wt=7): 6208 p(b,b) | p(b,f(b)). [resolve(6170,a,12,b),unit_del(b,27)]. given #517 (T,wt=9): 6145 p(b,m) | j = b | p(b,j). [resolve(6100,a,33,c)]. given #518 (A,wt=19): 322 p(x,k) | p(x,b) | p(g(x),x) | j = y | p(y,j) | x != y. [para(52(a,1),33(c,1))]. given #519 (T,wt=9): 6151 p(b,m) | j = b | p(k,j). [para(6100(a,1),65(a,2))]. given #520 (T,wt=12): 6149 p(b,m) | j = x | p(x,j) | b != x. [para(6100(a,1),33(c,1))]. given #521 (T,wt=12): 6172 p(b,m) | p(k,j) | j = m | k = m. [resolve(6102,a,95,c)]. given #522 (T,wt=9): 6306 p(b,m) | p(k,j) | k = m. [para(6172(c,1),65(a,1)),flip(d),merge(d),merge(e)]. given #523 (A,wt=22): 335 p(x,k) | p(x,b) | p(g(x),x) | p(k,j) | j = y | -p(y,x) | k = y. [para(52(a,1),95(c,2))]. given #524 (T,wt=6): 6329 p(b,m) | p(k,j). [para(6306(c,1),6076(a,2)),merge(c),merge(d)]. given #525 (T,wt=6): 6342 p(b,m) | p(b,j). [para(6100(a,1),6329(b,1)),merge(b)]. given #526 (T,wt=12): 6201 p(b,b) | k = b | p(k,j) | j = b. [resolve(6170,a,126,d)]. given #527 (T,wt=9): 6356 p(b,b) | k = b | p(k,j). [para(6201(d,1),65(a,1)),flip(d),merge(d),merge(e)]. given #528 (A,wt=20): 339 p(f(k),k) | p(f(k),b) | p(f(k),g(f(k))) | k = m | -p(k,m). [resolve(53,a,10,c(flip)),flip(d)]. given #529 (T,wt=9): 6363 p(b,b) | p(k,j) | p(m,k). [para(6356(b,1),51(a,1)),flip(c),unit_del(c,27)]. given #530 (T,wt=9): 6364 p(b,b) | p(k,j) | j = b. [para(6356(b,1),65(a,2)),merge(d)]. given #531 (T,wt=9): 6406 p(m,k) | p(b,b) | p(m,j). [para(51(a,1),6363(b,1)),merge(d)]. given #532 (T,wt=10): 6415 p(b,b) | p(k,j) | p(k,g(j)). [para(6364(c,1),2544(b,1)),merge(c),merge(d)]. given #533 (A,wt=22): 340 p(x,k) | p(x,b) | p(x,g(x)) | k = y | m = y | b = y | -p(y,x). [para(53(a,1),6(d,2))]. given #534 (T,wt=10): 6417 p(b,b) | p(k,j) | p(k,g(k)). [para(6364(c,1),3988(b,1)),merge(c),merge(d)]. given #535 (T,wt=10): 6460 p(b,b) | p(k,j) | p(b,g(j)). [para(6356(b,1),6415(c,1)),merge(c),merge(d)]. given #536 (T,wt=10): 6461 p(b,b) | p(k,j) | p(k,g(b)). [para(6364(c,1),6415(c,2,1)),merge(c),merge(d)]. given #537 (T,wt=10): 6476 p(b,b) | p(k,j) | p(b,g(k)). [para(6356(b,1),6417(c,1)),merge(c),merge(d)]. given #538 (A,wt=19): 342 p(x,k) | p(x,b) | p(x,g(x)) | j = y | p(y,j) | x != y. [para(53(a,1),33(c,1))]. given #539 (T,wt=10): 6545 p(b,b) | p(k,j) | p(b,g(b)). [para(6356(b,1),6461(c,1)),merge(c),merge(d)]. given #540 (T,wt=12): 6203 p(b,b) | p(m,j) | k = b | j = b. [resolve(6170,a,113,d)]. given #541 (T,wt=9): 6625 p(b,b) | p(m,j) | k = b. [para(6203(d,1),62(a,1)),flip(d),merge(e),merge(f),unit_del(d,27)]. given #542 (T,wt=12): 6345 p(b,m) | j = m | j = b | -p(j,b). [resolve(6342,b,2,e),flip(d),merge(c),unit_del(b,27)]. given #543 (A,wt=22): 355 p(x,k) | p(x,b) | p(x,g(x)) | p(k,j) | j = y | -p(y,x) | k = y. [para(53(a,1),95(c,2))]. given #544 (T,wt=12): 6626 p(b,b) | p(m,j) | j = b | p(b,j). [resolve(6625,c,33,c)]. given #545 (T,wt=13): 6098 p(x,b) | p(x,g(x)) | p(x,k) | p(b,m). [para(20(a,1),6076(a,1))]. given #546 (T,wt=13): 6099 p(x,b) | p(g(x),x) | p(x,k) | p(b,m). [para(22(a,1),6076(a,1))]. given #547 (T,wt=13): 6138 p(j,b) | p(j,g(j)) | p(m,m) | p(b,m). [para(5546(d,1),6076(a,2)),merge(e)]. given #548 (A,wt=20): 359 p(x,b) | p(x,g(x)) | j = x | p(b,j) | p(k,b) | p(g(k),k). [para(20(a,1),63(a,2))]. given #549 (T,wt=13): 6147 p(x,b) | p(x,g(x)) | k = x | p(b,m). [para(20(a,1),6100(a,2))]. given #550 (T,wt=13): 6148 p(x,b) | p(g(x),x) | k = x | p(b,m). [para(22(a,1),6100(a,2))]. given #551 (T,wt=13): 6177 p(x,b) | p(x,g(x)) | p(b,m) | p(m,x). [para(20(a,1),6159(b,2))]. given #552 (T,wt=13): 6178 p(x,b) | p(g(x),x) | p(b,m) | p(m,x). [para(22(a,1),6159(b,2))]. given #553 (A,wt=20): 360 p(x,b) | p(g(x),x) | j = x | p(b,j) | p(k,b) | p(g(k),k). [para(22(a,1),63(a,2))]. given #554 (T,wt=13): 6209 p(x,b) | p(x,g(x)) | p(x,m) | p(b,b). [para(20(a,1),6170(a,1))]. given #555 (T,wt=10): 6786 p(x,b) | p(x,g(x)) | p(x,m). [factor(6784,a,c),merge(c)]. given #556 (T,wt=13): 6210 p(x,b) | p(g(x),x) | p(x,m) | p(b,b). [para(22(a,1),6170(a,1))]. given #557 (T,wt=13): 6346 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j). [para(20(a,1),6342(b,1))]. given #558 (A,wt=19): 361 p(b,j) | p(k,b) | p(g(k),k) | j = x | -p(x,b) | k = x. [para(63(a,1),31(b,2))]. given #559 (T,wt=13): 6347 p(x,b) | p(g(x),x) | p(b,m) | p(x,j). [para(22(a,1),6342(b,1))]. given #560 (T,wt=13): 6640 p(b,b) | p(m,j) | p(b,j) | p(b,g(j)). [para(6625(c,1),6460(b,1)),merge(c)]. given #561 (T,wt=13): 6641 p(b,b) | p(m,j) | p(b,j) | p(b,g(k)). [para(6625(c,1),6476(b,1)),merge(c)]. given #562 (T,wt=13): 6642 p(b,b) | p(m,j) | p(b,j) | p(b,g(b)). [para(6625(c,1),6545(b,1)),merge(c)]. given #563 (A,wt=26): 362 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(34(c,1),63(a,2))]. given #564 (T,wt=13): 6733 p(x,b) | p(x,g(x)) | p(b,m) | p(b,x). [para(6147(c,1),6076(a,2)),merge(e)]. given #565 (T,wt=13): 6736 p(x,b) | p(g(x),x) | p(b,m) | p(b,x). [para(6148(c,1),6076(a,2)),merge(e)]. given #566 (T,wt=13): 6951 p(x,b) | p(x,g(x)) | p(b,m) | p(x,x). [factor(6937,a,c),merge(c)]. given #567 (T,wt=14): 6226 p(x,b) | p(x,g(x)) | p(b,b) | p(f(x),b). [para(20(a,1),6207(b,1,1))]. given #568 (A,wt=26): 363 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(39(c,1),63(a,2))]. given #569 (T,wt=14): 6227 p(x,b) | p(x,g(x)) | p(b,b) | p(f(b),x). [para(20(a,1),6207(b,2))]. given #570 (T,wt=14): 6228 p(x,b) | p(g(x),x) | p(b,b) | p(f(x),b). [para(22(a,1),6207(b,1,1))]. given #571 (T,wt=14): 6229 p(x,b) | p(g(x),x) | p(b,b) | p(f(b),x). [para(22(a,1),6207(b,2))]. given #572 (T,wt=14): 6239 p(x,b) | p(x,g(x)) | p(b,b) | p(x,f(b)). [para(20(a,1),6208(b,1))]. given #573 (A,wt=20): 367 p(x,b) | p(x,g(x)) | j = x | p(b,j) | p(k,b) | p(k,g(k)). [para(20(a,1),64(a,2))]. given #574 (T,wt=11): 7103 p(x,b) | p(x,g(x)) | p(x,f(b)). [factor(7101,a,c),merge(c)]. given #575 (T,wt=14): 6240 p(x,b) | p(x,g(x)) | p(b,b) | p(b,f(x)). [para(20(a,1),6208(b,2,1))]. given #576 (T,wt=14): 6241 p(x,b) | p(g(x),x) | p(b,b) | p(x,f(b)). [para(22(a,1),6208(b,1))]. given #577 (T,wt=14): 6242 p(x,b) | p(g(x),x) | p(b,b) | p(b,f(x)). [para(22(a,1),6208(b,2,1))]. given #578 (A,wt=20): 368 p(x,b) | p(g(x),x) | j = x | p(b,j) | p(k,b) | p(k,g(k)). [para(22(a,1),64(a,2))]. given #579 (T,wt=14): 6676 p(x,b) | p(x,g(x)) | p(x,k) | p(f(b),b). [resolve(6098,d,14,b),unit_del(d,27)]. given #580 (T,wt=14): 6677 p(x,b) | p(x,g(x)) | p(x,k) | p(b,f(b)). [resolve(6098,d,12,b),unit_del(d,27)]. given #581 (T,wt=14): 6685 p(f(b),b) | p(f(b),g(f(b))) | p(f(b),k). [factor(6675,a,d),merge(d)]. given #582 (T,wt=14): 6830 p(x,b) | p(x,g(x)) | p(x,j) | p(f(b),b). [resolve(6346,c,14,b),unit_del(d,27)]. given #583 (A,wt=19): 369 p(b,j) | p(k,b) | p(k,g(k)) | j = x | -p(x,b) | k = x. [para(64(a,1),31(b,2))]. given #584 (T,wt=14): 6831 p(x,b) | p(x,g(x)) | p(x,j) | p(b,f(b)). [resolve(6346,c,12,b),unit_del(d,27)]. given #585 (T,wt=14): 6838 p(f(b),b) | p(f(b),g(f(b))) | p(f(b),j). [factor(6829,a,d),merge(d)]. given #586 (T,wt=14): 6935 p(x,b) | p(x,g(x)) | p(b,x) | p(f(b),b). [resolve(6733,c,14,b),unit_del(d,27)]. given #587 (T,wt=14): 6936 p(x,b) | p(x,g(x)) | p(b,x) | p(b,f(b)). [resolve(6733,c,12,b),unit_del(d,27)]. given #588 (A,wt=26): 370 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(34(c,1),64(a,2))]. given #589 (T,wt=14): 6950 p(f(b),b) | p(f(b),g(f(b))) | p(b,f(b)). [factor(6934,a,d),merge(d)]. given #590 (T,wt=14): 6987 p(x,b) | p(x,g(x)) | p(x,x) | p(f(b),b). [resolve(6951,c,14,b),unit_del(d,27)]. given #591 (T,wt=14): 6988 p(x,b) | p(x,g(x)) | p(x,x) | p(b,f(b)). [resolve(6951,c,12,b),unit_del(d,27)]. given #592 (T,wt=14): 7021 p(x,b) | p(x,g(x)) | p(b,b) | p(f(x),x). [factor(7012,a,c),merge(c)]. given #593 (A,wt=26): 371 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(39(c,1),64(a,2))]. given #594 (T,wt=14): 7141 p(x,b) | p(x,g(x)) | p(b,b) | p(x,f(x)). [factor(7134,a,c),merge(c)]. given #595 (T,wt=11): 7719 p(x,b) | p(x,g(x)) | p(x,f(x)). [factor(7715,a,c),merge(c)]. given #596 (T,wt=14): 7232 p(x,b) | p(x,g(x)) | p(x,k) | p(f(x),b). [factor(7193,a,c),merge(c)]. given #597 (T,wt=14): 7234 p(x,b) | p(x,g(x)) | p(x,k) | p(f(b),x). [factor(7194,a,c),merge(c)]. given #598 (A,wt=40): 373 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(69,b,41,h),flip(e),flip(g),flip(h)]. given #599 (T,wt=14): 7273 p(x,b) | p(x,g(x)) | p(x,k) | p(b,f(x)). [factor(7259,a,c),merge(c)]. given #600 (T,wt=14): 7360 p(x,b) | p(x,g(x)) | p(x,j) | p(f(x),b). [factor(7327,a,c),merge(c)]. given #601 (T,wt=14): 7362 p(x,b) | p(x,g(x)) | p(x,j) | p(f(b),x). [factor(7328,a,c),merge(c)]. given #602 (T,wt=14): 7413 p(x,b) | p(x,g(x)) | p(x,j) | p(b,f(x)). [factor(7399,a,c),merge(c)]. given #603 (A,wt=39): 374 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(69,b,41,g),flip(e),flip(g)]. given #604 (T,wt=14): 7512 p(x,b) | p(x,g(x)) | p(b,x) | p(f(x),b). [factor(7469,a,c),merge(c)]. given #605 (T,wt=14): 7514 p(x,b) | p(x,g(x)) | p(b,x) | p(f(b),x). [factor(7470,a,c),merge(c)]. given #606 (T,wt=14): 7569 p(x,b) | p(x,g(x)) | p(b,x) | p(b,f(x)). [factor(7550,a,c),merge(c)]. given #607 (T,wt=14): 7657 p(x,b) | p(x,g(x)) | p(x,x) | p(f(x),b). [factor(7625,a,c),merge(c)]. given #608 (A,wt=40): 376 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(69,b,36,h),flip(e),flip(g),flip(h)]. given #609 (T,wt=14): 7659 p(x,b) | p(x,g(x)) | p(x,x) | p(f(b),x). [factor(7626,a,c),merge(c)]. given #610 (T,wt=14): 7693 p(x,b) | p(x,g(x)) | p(x,x) | p(b,f(x)). [factor(7680,a,c),merge(c)]. given #611 (T,wt=14): 7752 p(x,b) | p(x,g(x)) | p(x,k) | p(f(x),x). [factor(7740,a,c),merge(c)]. given #612 (T,wt=14): 7830 p(x,b) | p(x,g(x)) | p(x,j) | p(f(x),x). [factor(7824,a,c),merge(c)]. given #613 (A,wt=39): 377 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(69,b,36,g),flip(e),flip(g)]. given #614 (T,wt=14): 7913 p(x,b) | p(x,g(x)) | p(b,x) | p(f(x),x). [factor(7903,a,c),merge(c)]. given #615 (T,wt=14): 7975 p(x,b) | p(x,g(x)) | p(x,x) | p(f(x),x). [factor(7969,a,c),merge(c)]. given #616 (T,wt=15): 5978 p(b,k) | p(m,j) | j = b | j = k | p(j,k). [resolve(5977,d,24,b(flip)),flip(d)]. given #617 (T,wt=12): 8046 p(b,k) | p(m,j) | j = b | p(j,k). [para(54(a,1),5978(d,2)),merge(b),merge(e)]. given #618 (A,wt=33): 379 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(69,b,4,f),flip(c),flip(e),flip(f)]. given #619 (T,wt=12): 8051 p(b,k) | p(m,j) | p(j,k) | j = k. [resolve(8046,c,26,b(flip)),flip(d),merge(e)]. given #620 (T,wt=9): 8072 p(b,k) | p(m,j) | p(j,k). [para(8051(d,1),311(b,2)),merge(d),merge(e)]. given #621 (T,wt=9): 8075 p(b,k) | p(m,j) | p(k,m). [para(5980(c,1),8072(c,1)),merge(d),merge(e),merge(f)]. given #622 (T,wt=13): 8078 p(b,k) | p(m,j) | k = m | p(f(k),k). [resolve(8075,c,14,b),flip(c)]. given #623 (A,wt=33): 380 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(69,b,2,f),flip(c),flip(e),flip(f)]. given #624 (T,wt=10): 8096 p(b,k) | p(m,j) | p(f(k),k). [para(8078(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #625 (T,wt=10): 8109 p(b,k) | p(m,j) | p(f(b),k). [para(54(a,1),8096(c,1,1)),merge(b)]. given #626 (T,wt=10): 8110 p(b,k) | p(m,j) | p(f(k),b). [para(54(a,1),8096(c,2)),merge(b)]. given #627 (T,wt=10): 8133 p(b,k) | p(m,j) | p(f(b),b). [para(54(a,1),8109(c,2)),merge(b)]. given #628 (A,wt=20): 381 p(k,b) | p(g(k),k) | p(x,b) | p(g(x),x) | j = x | p(x,j). [resolve(45,c,33,c)]. given #629 (T,wt=13): 8079 p(b,k) | p(m,j) | k = m | p(k,f(k)). [resolve(8075,c,12,b),flip(c)]. given #630 (T,wt=10): 8197 p(b,k) | p(m,j) | p(k,f(k)). [para(8079(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #631 (T,wt=10): 8199 p(b,k) | p(m,j) | p(b,f(k)). [para(54(a,1),8197(c,1)),merge(b)]. given #632 (T,wt=10): 8200 p(b,k) | p(m,j) | p(k,f(b)). [para(54(a,1),8197(c,2,1)),merge(b)]. given #633 (A,wt=23): 382 p(f(x),b) | p(g(f(x)),f(x)) | p(x,b) | p(g(x),x) | m = x | -p(x,m). [resolve(45,c,10,c)]. given #634 (T,wt=10): 8222 p(b,k) | p(m,j) | p(b,f(b)). [para(54(a,1),8200(c,1)),merge(b)]. given #635 (T,wt=13): 8220 p(b,k) | p(b,f(k)) | j = m | k = m. [resolve(8199,b,31,b)]. given #636 (T,wt=13): 8238 p(b,k) | p(b,f(b)) | j = m | k = m. [resolve(8222,b,31,b)]. given #637 (T,wt=13): 8244 p(b,k) | p(b,f(k)) | k = m | p(k,m). [para(8220(c,1),308(a,2)),merge(e)]. given #638 (A,wt=19): 383 p(f(k),b) | p(f(k),g(f(k))) | p(b,k) | k = m | -p(k,m). [resolve(89,c,10,c(flip)),flip(d)]. given #639 (T,wt=10): 8262 p(b,k) | p(b,f(k)) | p(k,m). [para(8244(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #640 (T,wt=13): 8247 p(b,k) | p(b,f(k)) | k = m | p(m,m). [para(8220(c,1),8199(b,2)),merge(d),merge(f)]. given #641 (T,wt=10): 8295 p(b,k) | p(b,f(k)) | p(m,m). [para(8247(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #642 (T,wt=13): 8253 p(b,k) | p(b,f(b)) | k = m | p(k,m). [para(8238(c,1),308(a,2)),merge(e)]. given #643 (A,wt=22): 384 p(x,b) | p(x,g(x)) | p(b,k) | k = y | m = y | b = y | -p(y,x). [para(89(c,1),6(d,2))]. given #644 (T,wt=10): 8301 p(b,k) | p(b,f(b)) | p(k,m). [para(8253(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #645 (T,wt=13): 8256 p(b,k) | p(b,f(b)) | k = m | p(m,m). [para(8238(c,1),8222(b,2)),merge(d),merge(f)]. given #646 (T,wt=10): 8325 p(b,k) | p(b,f(b)) | p(m,m). [para(8256(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #647 (T,wt=14): 8282 p(b,k) | p(b,f(k)) | k = m | p(f(k),k). [resolve(8262,c,14,b),flip(c)]. given #648 (A,wt=19): 385 p(f(k),b) | p(g(f(k)),f(k)) | p(b,k) | k = m | -p(k,m). [resolve(90,c,10,c(flip)),flip(d)]. given #649 (T,wt=11): 8331 p(b,k) | p(b,f(k)) | p(f(k),k). [para(8282(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #650 (T,wt=11): 8350 p(b,k) | p(b,f(k)) | p(f(b),k). [para(54(a,1),8331(c,1,1)),merge(b)]. given #651 (T,wt=11): 8351 p(b,k) | p(b,f(k)) | p(f(k),b). [para(54(a,1),8331(c,2)),merge(b)]. given #652 (T,wt=11): 8374 p(b,k) | p(b,f(k)) | p(f(b),b). [para(54(a,1),8350(c,2)),merge(b)]. given #653 (A,wt=22): 386 p(x,b) | p(g(x),x) | p(b,k) | k = y | m = y | b = y | -p(y,x). [para(90(c,1),6(d,2))]. given #654 (T,wt=14): 8283 p(b,k) | p(b,f(k)) | k = m | p(k,f(k)). [resolve(8262,c,12,b),flip(c)]. given #655 (T,wt=11): 8413 p(b,k) | p(b,f(k)) | p(k,f(k)). [para(8283(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #656 (T,wt=7): 8415 p(b,k) | p(b,f(k)). [para(54(a,1),8413(c,1)),merge(b),merge(d)]. given #657 (T,wt=7): 8420 p(b,k) | p(b,f(b)). [para(54(a,1),8415(b,2,1)),merge(b)]. given #658 (A,wt=35): 387 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(104,b,41,h),flip(f),flip(i)]. given #659 (T,wt=14): 8417 p(x,b) | p(x,g(x)) | p(b,k) | p(x,f(k)). [para(20(a,1),8415(b,1))]. given #660 (T,wt=14): 8418 p(x,b) | p(g(x),x) | p(b,k) | p(x,f(k)). [para(22(a,1),8415(b,1))]. given #661 (T,wt=14): 8423 p(x,b) | p(x,g(x)) | p(b,k) | p(b,f(x)). [para(89(c,1),8415(b,2,1)),merge(d)]. given #662 (T,wt=14): 8424 p(x,b) | p(g(x),x) | p(b,k) | p(b,f(x)). [para(90(c,1),8415(b,2,1)),merge(d)]. given #663 (A,wt=34): 388 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(104,b,41,g),flip(h)]. given #664 (T,wt=14): 8432 p(x,b) | p(g(x),x) | p(b,k) | p(x,f(b)). [para(22(a,1),8420(b,1))]. given #665 (T,wt=14): 8502 p(x,b) | p(x,g(x)) | p(x,k) | p(x,f(k)). [factor(8472,a,c),merge(c)]. given #666 (T,wt=14): 8507 p(b,b) | p(m,j) | p(b,g(b)) | p(b,f(k)). [factor(8499,a,c)]. given #667 (T,wt=15): 6146 p(b,m) | k = x | m = x | b = x | -p(x,b). [para(6100(a,1),6(d,2))]. given #668 (A,wt=35): 389 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(104,b,36,h),flip(f),flip(i)]. given #669 (T,wt=15): 6176 p(b,m) | b = x | m = x | -p(m,x) | -p(x,m). [resolve(6159,b,4,b),flip(b),flip(d),unit_del(b,27)]. given #670 (T,wt=15): 6361 p(b,b) | p(k,j) | j = x | p(x,j) | b != x. [para(6356(b,1),33(c,1))]. given #671 (T,wt=15): 6366 p(b,b) | p(k,j) | j = x | -p(x,b) | k = x. [para(6356(b,1),95(c,2)),merge(c)]. given #672 (T,wt=14): 8637 p(b,b) | p(k,j) | f(b) = j | f(b) = k. [resolve(6366,d,6207,b),flip(c),flip(d),merge(e)]. given #673 (A,wt=34): 390 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(104,b,36,g),flip(h)]. given #674 (T,wt=10): 8651 p(k,j) | p(b,b) | f(b) = k. [para(65(a,1),8637(c,2)),merge(c),merge(e)]. given #675 (T,wt=9): 8694 p(k,j) | p(b,b) | p(k,b). [para(8651(c,1),6207(b,1)),merge(c)]. given #676 (T,wt=10): 8695 p(b,b) | p(k,j) | f(b) = b. [para(6356(b,1),8651(c,2)),merge(c),merge(d)]. given #677 (T,wt=6): 8749 p(b,b) | p(k,j). [para(8695(c,1),6207(b,1)),merge(c),merge(d)]. given #678 (A,wt=28): 391 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(104,b,4,f),flip(d),flip(g)]. given #679 (T,wt=9): 8779 p(b,b) | p(m,j) | p(b,j). [para(6625(c,1),8749(b,1)),merge(c)]. given #680 (T,wt=12): 8804 p(b,b) | p(b,j) | j = m | k = m. [resolve(8779,b,31,b)]. given #681 (T,wt=12): 8822 p(b,b) | p(b,j) | k = m | p(k,m). [para(8804(c,1),8749(b,2)),merge(d)]. given #682 (T,wt=12): 8823 p(b,b) | p(b,j) | k = m | p(m,m). [para(8804(c,1),8779(b,2)),merge(d),merge(f)]. given #683 (A,wt=28): 392 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(104,b,2,f),flip(d),flip(g)]. given #684 (T,wt=13): 8713 p(k,b) | p(k,g(k)) | p(b,j) | p(b,b). [para(137(c,1),8694(a,1)),merge(e)]. given #685 (T,wt=13): 8714 p(k,b) | p(g(k),k) | p(b,j) | p(b,b). [para(143(c,1),8694(a,1)),merge(e)]. given #686 (T,wt=15): 6630 p(b,b) | p(m,j) | j = x | p(x,j) | b != x. [para(6625(c,1),33(c,1))]. given #687 (T,wt=15): 8811 p(b,b) | p(b,j) | k = m | j = k | p(j,k). [resolve(8804,c,24,b(flip)),flip(d)]. given #688 (A,wt=27): 402 p(x,b) | p(b,k) | p(m,x) | m = x | p(x,m) | g(x) = m | g(x) = x | -p(x,g(x)). [resolve(105,b,2,f),flip(f)]. given #689 (T,wt=12): 8925 p(b,b) | p(b,j) | k = m | p(j,k). [para(8811(d,1),8804(c,1)),merge(e),merge(f),merge(g),merge(h)]. given #690 (T,wt=16): 5929 p(x,b) | p(x,g(x)) | p(b,k) | p(j,x) | p(m,j). [para(20(a,1),5915(b,2))]. given #691 (T,wt=16): 5930 p(x,b) | p(g(x),x) | p(b,k) | p(j,x) | p(m,j). [para(22(a,1),5915(b,2))]. given #692 (T,wt=16): 6628 p(x,b) | p(x,g(x)) | p(b,b) | p(m,j) | k = x. [para(20(a,1),6625(c,2))]. given #693 (A,wt=32): 405 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(46,d,39,c(flip))]. given #694 (T,wt=13): 8984 p(j,b) | p(j,g(j)) | p(b,b) | p(m,j). [factor(8983,d,e)]. given #695 (T,wt=16): 6629 p(x,b) | p(g(x),x) | p(b,b) | p(m,j) | k = x. [para(22(a,1),6625(c,2))]. given #696 (T,wt=16): 6633 p(b,b) | p(m,j) | p(x,b) | p(x,g(x)) | p(x,j). [para(6625(c,1),314(c,2)),merge(e)]. given #697 (T,wt=16): 6748 p(j,b) | p(j,g(j)) | p(b,m) | j = m | k = m. [resolve(6177,d,31,b)]. given #698 (A,wt=32): 406 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(46,d,34,c(flip))]. given #699 (T,wt=13): 9069 p(j,b) | p(j,g(j)) | p(b,m) | k = m. [resolve(6748,d,59,c(flip)),merge(e),merge(f)]. given #700 (T,wt=10): 9082 p(j,b) | p(j,g(j)) | p(b,m). [para(9069(d,1),6076(a,2)),merge(d),merge(e)]. given #701 (T,wt=16): 8081 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(x,m). [para(90(c,1),8075(c,1)),merge(d)]. given #702 (T,wt=16): 8723 p(j,b) | p(g(j),j) | p(m,j) | p(k,b) | p(b,b). [para(959(d,1),8694(a,2)),merge(f)]. given #703 (A,wt=23): 407 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),46(d,1,1,1))]. given #704 (T,wt=16): 8766 p(x,k) | p(x,b) | p(g(x),x) | p(b,b) | p(x,j). [para(52(a,1),8749(b,1))]. given #705 (T,wt=16): 8771 p(j,b) | p(g(j),j) | p(m,j) | p(b,b) | p(k,k). [para(531(d,1),8749(b,2))]. given #706 (T,wt=16): 8772 p(x,k) | p(x,b) | p(g(x),x) | p(b,b) | p(b,j). [para(1542(d,1),8749(b,1))]. given #707 (T,wt=16): 8773 p(x,k) | p(x,b) | p(x,g(x)) | p(b,b) | p(b,j). [para(1605(d,1),8749(b,1))]. given #708 (A,wt=23): 408 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),46(d,2))]. given #709 (T,wt=16): 8809 p(b,b) | p(b,j) | k = m | p(j,b) | p(g(j),j). [resolve(8804,c,60,c(flip))]. given #710 (T,wt=16): 8810 p(b,b) | p(b,j) | k = m | p(j,b) | p(j,g(j)). [resolve(8804,c,59,c(flip))]. given #711 (T,wt=16): 8854 k = b | p(k,b) | p(m,g(k)) | p(b,j) | p(b,b). [para(29(b,1),8713(b,1))]. given #712 (T,wt=13): 9248 p(k,b) | p(m,g(k)) | p(b,j) | p(b,b). [para(8854(a,1),8749(b,1)),merge(e),merge(f)]. given #713 (A,wt=23): 409 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),46(d,1,1,1))]. given #714 (T,wt=16): 8855 k = b | p(k,b) | p(k,g(m)) | p(b,j) | p(b,b). [para(29(b,1),8713(b,2,1))]. given #715 (T,wt=13): 9290 p(k,b) | p(k,g(m)) | p(b,j) | p(b,b). [para(8855(a,1),8749(b,1)),merge(e),merge(f)]. given #716 (T,wt=16): 8877 k = b | p(k,b) | p(g(m),k) | p(b,j) | p(b,b). [para(29(b,1),8714(b,1,1))]. given #717 (T,wt=13): 9328 p(k,b) | p(g(m),k) | p(b,j) | p(b,b). [para(8877(a,1),8749(b,1)),merge(e),merge(f)]. given #718 (A,wt=23): 410 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),46(d,2))]. given #719 (T,wt=16): 8878 k = b | p(k,b) | p(g(k),m) | p(b,j) | p(b,b). [para(29(b,1),8714(b,2))]. given #720 (T,wt=13): 9372 p(k,b) | p(g(k),m) | p(b,j) | p(b,b). [para(8878(a,1),8749(b,1)),merge(e),merge(f)]. given #721 (T,wt=16): 8983 p(x,b) | p(x,g(x)) | p(b,b) | p(m,j) | p(m,x). [factor(8980,a,f),merge(f),merge(g)]. given #722 (T,wt=16): 9026 p(x,b) | p(g(x),x) | p(b,b) | p(m,j) | p(x,j). [para(6629(e,1),8749(b,1)),merge(e)]. given #723 (A,wt=29): 411 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(34(c,1),46(d,1,1,1))]. given #724 (T,wt=16): 9305 k = b | p(k,b) | p(m,g(m)) | p(b,j) | p(b,b). [para(29(b,1),9290(b,1))]. given #725 (T,wt=13): 9463 p(k,b) | p(m,g(m)) | p(b,j) | p(b,b). [para(9305(a,1),8749(b,1)),merge(e),merge(f)]. given #726 (T,wt=16): 9340 k = b | p(k,b) | p(g(m),m) | p(b,j) | p(b,b). [para(29(b,1),9328(b,2))]. given #727 (T,wt=13): 9491 p(k,b) | p(g(m),m) | p(b,j) | p(b,b). [para(9340(a,1),8749(b,1)),merge(e),merge(f)]. given #728 (A,wt=29): 412 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(34(c,1),46(d,2))]. given #729 (T,wt=17): 488 p(j,b) | p(m,k) | p(k,j) | g(j) = j | g(j) = k. [resolve(138,b,31,b),flip(d),flip(e)]. given #730 (T,wt=13): 9511 p(k,j) | p(j,b) | p(m,k) | g(j) = k. [para(65(a,1),488(d,2)),merge(d),merge(f)]. given #731 (T,wt=9): 9529 p(k,j) | p(j,b) | p(m,k). [para(9511(d,1),2736(b,1)),merge(d),merge(e),merge(f),merge(g)]. given #732 (T,wt=16): 9531 p(x,b) | p(x,g(x)) | p(k,j) | p(j,x) | p(m,k). [para(20(a,1),9529(b,2))]. given #733 (A,wt=29): 413 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(39(c,1),46(d,1,1,1))]. given #734 (T,wt=16): 9532 p(x,b) | p(g(x),x) | p(k,j) | p(j,x) | p(m,k). [para(22(a,1),9529(b,2))]. given #735 (T,wt=17): 514 p(j,b) | p(m,k) | p(m,j) | g(j) = j | g(j) = k. [resolve(140,b,31,b),flip(d),flip(e)]. given #736 (T,wt=16): 9561 p(j,b) | p(m,k) | p(m,j) | g(j) = k | j = b. [resolve(514,d,18,c),flip(e),merge(f)]. given #737 (T,wt=15): 9572 p(j,b) | p(m,k) | p(m,j) | j = b | k != b. [para(9561(d,1),16(c,1)),flip(e),merge(e),merge(f)]. given #738 (A,wt=29): 414 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(39(c,1),46(d,2))]. given #739 (T,wt=15): 9573 p(j,b) | p(m,k) | p(m,j) | j = b | j != k. [para(9561(d,1),18(c,1)),flip(e),flip(g),merge(e),merge(f)]. given #740 (T,wt=15): 9582 p(j,b) | p(m,k) | p(m,j) | j = b | p(k,m). [para(9561(d,1),519(d,1)),merge(e),merge(f),merge(g)]. given #741 (T,wt=12): 9598 p(j,b) | p(m,k) | p(m,j) | p(k,m). [para(9582(d,1),84(b,1)),flip(f),merge(e),merge(g),unit_del(e,27)]. given #742 (T,wt=15): 9585 p(j,b) | p(m,k) | p(m,j) | j = b | p(j,k). [para(9561(d,1),1625(c,2)),merge(f),merge(g),merge(h)]. given #743 (A,wt=35): 416 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(415,b,41,h),flip(d),flip(f)]. given #744 (T,wt=12): 9611 p(j,b) | p(m,k) | p(m,j) | p(j,k). [para(9585(d,1),84(b,1)),flip(f),merge(e),merge(g),unit_del(e,27)]. given #745 (T,wt=9): 9627 p(m,k) | p(m,j) | p(j,b). [para(84(b,1),9611(d,1)),merge(d),merge(e),merge(f)]. given #746 (T,wt=16): 9629 p(x,b) | p(x,g(x)) | p(m,k) | p(m,j) | p(j,x). [para(20(a,1),9627(c,2))]. given #747 (T,wt=16): 9630 p(x,b) | p(g(x),x) | p(m,k) | p(m,j) | p(j,x). [para(22(a,1),9627(c,2))]. given #748 (A,wt=36): 417 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(415,b,41,g),flip(d),flip(f),flip(g)]. given #749 (T,wt=17): 608 p(j,b) | p(b,k) | p(j,j) | g(j) = j | g(j) = k. [resolve(315,b,31,b),flip(d),flip(e)]. given #750 (T,wt=13): 9660 p(j,b) | p(b,k) | p(j,j) | g(j) = k. [para(608(d,1),314(b,2)),merge(e),merge(f),merge(g),merge(h)]. given #751 (T,wt=12): 9674 p(j,b) | p(b,k) | p(j,j) | p(j,k). [para(9660(d,1),314(b,2)),merge(d),merge(f),merge(g)]. given #752 (T,wt=13): 9667 p(b,k) | p(j,b) | p(j,j) | g(j) = b. [para(54(a,1),9660(d,2)),merge(c)]. given #753 (A,wt=35): 418 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(415,b,36,h),flip(d),flip(f)]. given #754 (T,wt=9): 9692 p(b,k) | p(j,b) | p(j,j). [para(9667(d,1),314(b,2)),merge(d),merge(e),merge(f),merge(g)]. given #755 (T,wt=17): 1588 p(j,k) | p(j,b) | p(m,k) | g(j) = j | g(j) = k. [resolve(1569,c,31,b),flip(d),flip(e)]. given #756 (T,wt=16): 9700 p(j,k) | p(j,b) | p(m,k) | g(j) = k | j = b. [resolve(1588,d,18,c),flip(e),merge(f)]. given #757 (T,wt=12): 9710 p(j,k) | p(j,b) | p(m,k) | j = b. [para(9700(d,1),1625(c,2)),merge(e),merge(f),merge(g),merge(h)]. given #758 (A,wt=36): 419 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(415,b,36,g),flip(d),flip(f),flip(g)]. given #759 (T,wt=12): 9715 p(j,k) | p(j,b) | p(m,k) | j = k. [resolve(9710,d,26,b(flip)),flip(d),merge(e)]. given #760 (T,wt=12): 9732 p(m,k) | p(j,k) | p(j,b) | j = m. [para(51(a,1),9715(d,2)),merge(d)]. given #761 (T,wt=9): 9742 p(m,k) | p(j,k) | p(j,b). [para(9732(d,1),9710(d,1)),merge(d),merge(e),merge(f),unit_del(d,27)]. given #762 (T,wt=9): 9754 p(m,k) | p(j,m) | p(j,b). [para(51(a,1),9742(b,2)),merge(b)]. given #763 (A,wt=28): 420 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(415,b,4,f),flip(b),flip(d)]. given #764 (T,wt=13): 9779 p(m,k) | p(j,b) | j = m | p(f(j),j). [resolve(9754,b,14,b),flip(c)]. given #765 (T,wt=10): 9799 p(m,k) | p(j,b) | p(f(j),j). [para(9779(c,1),9742(b,1)),merge(d),merge(e),merge(f)]. given #766 (T,wt=13): 9780 p(m,k) | p(j,b) | j = m | p(j,f(j)). [resolve(9754,b,12,b),flip(c)]. given #767 (T,wt=10): 9833 p(m,k) | p(j,b) | p(j,f(j)). [para(9780(c,1),9742(b,1)),merge(d),merge(e),merge(f)]. given #768 (A,wt=29): 421 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(415,b,4,e),flip(b),flip(d),flip(e)]. given #769 (T,wt=14): 9812 p(m,k) | p(j,b) | f(j) = j | f(j) = k. [resolve(9799,c,31,b),flip(c),flip(d)]. given #770 (T,wt=13): 9865 p(m,k) | p(j,b) | f(j) = k | p(j,j). [para(9812(c,1),9799(c,1)),merge(d),merge(e)]. given #771 (T,wt=13): 9869 p(m,k) | p(j,b) | f(j) = m | p(j,j). [para(51(a,1),9865(c,2)),merge(b)]. given #772 (T,wt=15): 9751 p(m,k) | p(j,b) | j = k | j = m | j = b. [resolve(9742,b,6,d),flip(c),flip(d),flip(e)]. given #773 (A,wt=29): 422 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(415,b,2,e),flip(b),flip(d),flip(e)]. given #774 (T,wt=12): 9877 p(m,k) | p(j,b) | j = m | j = b. [para(51(a,1),9751(c,2)),merge(b),merge(e)]. given #775 (T,wt=9): 9886 p(m,k) | p(j,b) | j = b. [para(9877(c,1),9742(b,1)),merge(d),merge(e),merge(f)]. given #776 (T,wt=10): 9894 p(m,k) | p(j,b) | p(f(b),j). [para(9886(c,1),9799(c,1,1)),merge(c),merge(d)]. given #777 (T,wt=10): 9895 p(m,k) | p(j,b) | p(f(j),b). [para(9886(c,1),9799(c,2)),merge(c),merge(d)]. given #778 (A,wt=36): 426 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(425,b,41,h),flip(d),flip(f),flip(g)]. given #779 (T,wt=10): 9896 p(m,k) | p(j,b) | p(b,f(j)). [para(9886(c,1),9833(c,1)),merge(c),merge(d)]. given #780 (T,wt=10): 9897 p(m,k) | p(j,b) | p(j,f(b)). [para(9886(c,1),9833(c,2,1)),merge(c),merge(d)]. given #781 (T,wt=10): 9914 p(m,k) | p(j,b) | p(f(b),b). [para(9886(c,1),9894(c,2)),merge(c),merge(d)]. given #782 (T,wt=10): 9927 p(m,k) | p(j,b) | f(j) = k. [para(9812(c,1),9895(c,1)),merge(d),merge(e),merge(f)]. given #783 (A,wt=35): 428 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(425,b,41,d),flip(d),flip(f)]. given #784 (T,wt=10): 9967 p(m,k) | p(j,b) | p(b,f(b)). [para(9886(c,1),9897(c,1)),merge(c),merge(d)]. given #785 (T,wt=10): 9985 p(m,k) | p(j,b) | f(j) = m. [para(51(a,1),9927(c,2)),merge(b)]. given #786 (T,wt=10): 9986 p(m,k) | p(j,b) | f(b) = k. [para(9886(c,1),9927(c,1,1)),merge(c),merge(d)]. given #787 (T,wt=10): 10024 p(m,k) | p(j,b) | f(b) = m. [para(9886(c,1),9985(c,1,1)),merge(c),merge(d)]. given #788 (A,wt=36): 429 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(425,b,36,h),flip(d),flip(f),flip(g)]. given #789 (T,wt=9): 10033 p(m,k) | p(j,b) | -p(b,m). [resolve(10024,c,8,c),unit_del(c,27)]. given #790 (T,wt=9): 10063 p(m,k) | p(j,b) | p(b,b). [resolve(10033,c,6170,a)]. given #791 (T,wt=12): 10023 p(m,k) | p(j,b) | j = m | -p(j,m). [resolve(9985,c,8,c),flip(c)]. given #792 (T,wt=9): 10090 p(m,k) | p(j,b) | j = m. [resolve(10023,d,9754,b),merge(d),merge(e)]. given #793 (A,wt=35): 431 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(425,b,36,d),flip(d),flip(f)]. given #794 (T,wt=6): 10096 p(m,k) | p(j,b). [para(10090(c,1),9742(b,1)),merge(c),merge(d),merge(e)]. given #795 (T,wt=13): 10127 p(x,b) | p(x,g(x)) | p(m,k) | p(j,x). [para(20(a,1),10096(b,2))]. given #796 (T,wt=13): 10128 p(x,b) | p(g(x),x) | p(m,k) | p(j,x). [para(22(a,1),10096(b,2))]. given #797 (T,wt=15): 10126 p(m,k) | j = m | p(j,m) | j = b | -p(b,j). [resolve(10096,b,2,e),flip(b),flip(e),unit_del(d,27)]. given #798 (A,wt=29): 432 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(425,b,4,f),flip(b),flip(d),flip(e)]. given #799 (T,wt=17): 2111 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(f(b)))),m). [factor(2106,a,c),merge(c)]. given #800 (T,wt=17): 2123 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(f(b)))),m). [factor(2119,a,c),merge(c)]. given #801 (T,wt=17): 2277 p(j,b) | p(g(j),j) | p(k,j) | p(j,k) | p(b,g(j)). [para(506(d,1),2242(c,1)),merge(e)]. given #802 (T,wt=17): 2278 p(j,b) | p(g(j),j) | p(k,j) | p(j,k) | p(j,g(b)). [para(506(d,1),2242(c,2,1)),merge(e)]. given #803 (A,wt=22): 453 p(j,b) | p(j,g(j)) | p(k,j) | k = x | m = x | b = x | -p(x,b). [para(133(c,1),6(d,2))]. given #804 (T,wt=17): 2279 p(j,b) | p(g(j),j) | p(m,j) | p(j,k) | p(k,g(j)). [para(531(d,1),2242(c,1)),merge(e)]. given #805 (T,wt=17): 2280 p(j,b) | p(g(j),j) | p(m,j) | p(j,k) | p(j,g(k)). [para(531(d,1),2242(c,2,1)),merge(e)]. given #806 (T,wt=17): 2281 p(j,b) | p(g(j),j) | p(m,j) | p(j,k) | p(b,g(j)). [para(959(d,1),2242(c,1)),merge(e)]. given #807 (T,wt=17): 2282 p(j,b) | p(g(j),j) | p(m,j) | p(j,k) | p(j,g(b)). [para(959(d,1),2242(c,2,1)),merge(e)]. given #808 (A,wt=20): 454 p(x,b) | p(x,g(x)) | p(j,b) | p(j,g(j)) | k = x | p(k,j). [para(20(a,1),133(c,2))]. given #809 (T,wt=13): 10386 p(j,b) | p(j,g(j)) | p(k,j) | p(k,b). [factor(10376,a,c),merge(c),merge(f)]. given #810 (T,wt=13): 10395 p(j,b) | p(j,g(j)) | p(k,j) | p(m,j). [factor(10387,a,e),merge(e),merge(f)]. given #811 (T,wt=13): 10410 p(k,j) | p(j,b) | p(j,g(k)) | p(k,b). [para(65(a,1),10386(b,2,1)),merge(d)]. given #812 (T,wt=13): 10455 p(k,j) | p(j,b) | p(j,g(k)) | p(m,j). [para(65(a,1),10395(b,2,1)),merge(d)]. given #813 (A,wt=20): 455 p(x,b) | p(g(x),x) | p(j,b) | p(j,g(j)) | k = x | p(k,j). [para(22(a,1),133(c,2))]. given #814 (T,wt=16): 10394 p(j,b) | p(j,g(j)) | p(k,j) | p(b,j) | p(j,j). [factor(10382,a,d),merge(d)]. given #815 (T,wt=16): 10412 k = b | p(k,j) | p(j,b) | p(j,g(m)) | p(k,b). [para(94(b,1),10386(b,2,1)),merge(e)]. given #816 (T,wt=16): 10456 p(m,j) | k = b | p(j,b) | p(m,g(j)) | p(k,j). [para(62(a,1),10395(b,1)),merge(f)]. given #817 (T,wt=16): 10457 p(m,j) | k = b | p(j,b) | p(j,g(m)) | p(k,j). [para(62(a,1),10395(b,2,1)),merge(f)]. given #818 (A,wt=19): 456 p(j,b) | p(j,g(j)) | p(k,j) | j = x | p(x,j) | b != x. [para(133(c,1),33(c,1))]. given #819 (T,wt=16): 10514 p(m,j) | k = b | p(k,j) | p(j,b) | p(m,g(k)). [para(62(a,1),10455(c,1)),merge(f)]. given #820 (T,wt=16): 10552 p(k,j) | p(j,b) | p(j,g(k)) | p(b,j) | p(j,j). [para(65(a,1),10394(b,2,1)),merge(d)]. given #821 (T,wt=16): 10575 p(k,j) | p(j,b) | p(j,g(m)) | p(k,b) | j = b. [para(10412(a,1),65(a,2)),merge(f)]. given #822 (T,wt=16): 10590 p(m,j) | p(j,b) | p(m,g(j)) | p(k,j) | j = b. [para(10456(b,1),65(a,2)),merge(f)]. given #823 (A,wt=26): 457 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(j,b) | p(j,g(j)) | k = x | p(k,j). [para(34(c,1),133(c,2))]. given #824 (T,wt=16): 10602 p(m,j) | p(j,b) | p(j,g(m)) | p(k,j) | j = b. [para(10457(b,1),65(a,2)),merge(f)]. given #825 (T,wt=16): 10618 p(m,j) | p(k,j) | p(j,b) | p(m,g(k)) | j = b. [para(10514(b,1),65(a,2)),merge(f)]. given #826 (T,wt=17): 2291 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | p(k,g(j)). [para(1538(e,1),2242(c,1)),merge(e),merge(f)]. given #827 (T,wt=17): 2292 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | p(j,g(k)). [para(1538(e,1),2242(c,2,1)),merge(e),merge(f)]. given #828 (A,wt=26): 459 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(j,b) | p(j,g(j)) | k = x | p(k,j). [para(39(c,1),133(c,2))]. given #829 (T,wt=17): 2301 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(b,g(j)). [factor(2293,a,e),merge(e)]. given #830 (T,wt=17): 2302 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(j,g(b)). [factor(2294,a,e),merge(e)]. given #831 (T,wt=17): 2343 p(j,b) | p(g(j),j) | p(k,j) | p(j,k) | p(b,g(k)). [para(506(d,1),2256(d,1)),merge(d),merge(f)]. given #832 (T,wt=17): 2470 p(j,b) | p(g(j),j) | p(k,j) | p(k,b) | p(b,g(k)). [para(139(c,1),2449(c,1)),merge(d)]. given #833 (A,wt=19): 460 p(j,b) | p(j,g(j)) | p(k,j) | j = x | -p(x,b) | k = x. [para(133(c,1),95(c,2)),merge(d)]. given #834 (T,wt=17): 2471 p(j,b) | p(g(j),j) | p(k,j) | p(k,b) | p(k,g(b)). [para(139(c,1),2449(c,2,1)),merge(d)]. given #835 (T,wt=17): 2565 p(x,b) | p(x,g(x)) | p(k,j) | p(j,x) | p(k,g(j)). [para(20(a,1),2544(b,2))]. given #836 (T,wt=17): 2566 p(x,b) | p(g(x),x) | p(k,j) | p(j,x) | p(k,g(j)). [para(22(a,1),2544(b,2))]. given #837 (T,wt=17): 2574 p(x,k) | p(x,b) | p(g(x),x) | p(k,j) | p(k,g(j)). [para(324(d,1),2544(b,1)),merge(e),merge(f)]. given #838 (A,wt=22): 477 p(j,b) | p(j,g(j)) | p(m,j) | k = x | m = x | b = x | -p(x,b). [para(135(d,1),6(d,2))]. given #839 (T,wt=17): 2575 p(x,k) | p(x,b) | p(x,g(x)) | p(k,j) | p(k,g(j)). [para(344(d,1),2544(b,1)),merge(e),merge(f)]. given #840 (T,wt=17): 2593 p(j,b) | p(g(j),j) | p(k,j) | p(k,b) | p(b,g(j)). [para(139(c,1),2568(c,1)),merge(d)]. given #841 (T,wt=17): 3315 p(j,k) | p(j,b) | p(m,b) | g(j) = j | g(j) = k. [resolve(2756,c,31,b),flip(d),flip(e)]. given #842 (T,wt=16): 10987 p(j,k) | p(j,b) | p(m,b) | g(j) = k | j = b. [resolve(3315,d,18,c),flip(e),merge(f)]. given #843 (A,wt=20): 478 p(x,b) | p(x,g(x)) | p(j,b) | p(j,g(j)) | p(m,j) | k = x. [para(20(a,1),135(d,2))]. given #844 (T,wt=10): 11014 p(j,b) | p(j,g(j)) | p(m,j). [factor(11009,a,d),merge(d),merge(e)]. given #845 (T,wt=12): 10999 p(j,k) | p(j,b) | p(m,b) | j = b. [para(10987(d,1),1669(c,2)),merge(e),merge(f),merge(g),merge(h)]. given #846 (T,wt=9): 11102 p(j,k) | p(j,b) | p(m,b). [para(10999(d,1),4157(a,2)),merge(d),merge(e)]. given #847 (T,wt=12): 11113 k = b | p(j,m) | p(j,b) | p(m,b). [para(29(b,1),11102(a,2))]. given #848 (A,wt=22): 501 p(j,b) | p(g(j),j) | p(k,j) | k = x | m = x | b = x | -p(x,b). [para(139(c,1),6(d,2))]. given #849 (T,wt=9): 11144 p(j,m) | p(j,b) | p(m,b). [para(11113(a,1),2739(a,2)),merge(d),merge(e)]. given #850 (T,wt=13): 11031 p(m,j) | k = b | p(j,b) | p(m,g(j)). [para(62(a,1),11014(b,1)),merge(e)]. given #851 (T,wt=13): 11032 p(m,j) | k = b | p(j,b) | p(j,g(m)). [para(62(a,1),11014(b,2,1)),merge(e)]. given #852 (T,wt=13): 11180 p(j,b) | p(m,b) | j = m | p(f(j),j). [resolve(11144,a,14,b),flip(c)]. given #853 (A,wt=20): 502 p(x,b) | p(x,g(x)) | p(j,b) | p(g(j),j) | k = x | p(k,j). [para(20(a,1),139(c,2))]. given #854 (T,wt=13): 11181 p(j,b) | p(m,b) | j = m | p(j,f(j)). [resolve(11144,a,12,b),flip(c)]. given #855 (T,wt=13): 11229 p(j,b) | p(m,b) | p(f(j),j) | p(k,m). [para(11180(c,1),4128(a,2)),merge(e)]. given #856 (T,wt=13): 11262 p(j,b) | p(m,b) | p(j,f(j)) | p(k,m). [para(11181(c,1),4128(a,2)),merge(e)]. given #857 (T,wt=14): 11043 p(j,b) | p(g(j),j) | p(m,j) | p(k,g(j)). [para(531(d,1),11014(b,1)),merge(d),merge(f)]. given #858 (A,wt=20): 503 p(x,b) | p(g(x),x) | p(j,b) | p(g(j),j) | k = x | p(k,j). [para(22(a,1),139(c,2))]. given #859 (T,wt=14): 11044 p(j,b) | p(g(j),j) | p(m,j) | p(j,g(k)). [para(531(d,1),11014(b,2,1)),merge(d),merge(f)]. given #860 (T,wt=14): 11045 p(j,b) | p(g(j),j) | p(m,j) | p(b,g(j)). [para(959(d,1),11014(b,1)),merge(d),merge(f)]. given #861 (T,wt=14): 11046 p(j,b) | p(g(j),j) | p(m,j) | p(j,g(b)). [para(959(d,1),11014(b,2,1)),merge(d),merge(f)]. given #862 (T,wt=14): 11223 p(j,b) | p(m,b) | p(f(j),j) | p(g(j),j). [resolve(11180,c,60,c(flip)),merge(d)]. given #863 (A,wt=19): 504 p(j,b) | p(g(j),j) | p(k,j) | j = x | p(x,j) | b != x. [para(139(c,1),33(c,1))]. given #864 (T,wt=14): 11224 p(j,b) | p(m,b) | p(f(j),j) | p(j,g(j)). [resolve(11180,c,59,c(flip)),merge(d)]. given #865 (T,wt=14): 11257 p(j,b) | p(m,b) | p(j,f(j)) | p(g(j),j). [resolve(11181,c,60,c(flip)),merge(d)]. given #866 (T,wt=14): 11479 p(j,b) | p(m,b) | p(f(j),j) | p(g(m),j). [para(11180(c,1),11223(d,1,1)),merge(d),merge(e),merge(f)]. given #867 (T,wt=14): 11480 p(j,b) | p(m,b) | p(f(j),j) | p(g(j),m). [para(11180(c,1),11223(d,2)),merge(d),merge(e),merge(f)]. given #868 (A,wt=26): 505 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(j,b) | p(g(j),j) | k = x | p(k,j). [para(34(c,1),139(c,2))]. given #869 (T,wt=14): 11519 p(j,b) | p(m,b) | p(j,f(j)) | p(g(m),j). [para(11181(c,1),11257(d,1,1)),merge(d),merge(e),merge(f)]. given #870 (T,wt=14): 11520 p(j,b) | p(m,b) | p(j,f(j)) | p(g(j),m). [para(11181(c,1),11257(d,2)),merge(d),merge(e),merge(f)]. given #871 (T,wt=15): 11111 p(j,b) | p(m,b) | j = k | j = m | j = b. [resolve(11102,a,6,d),flip(c),flip(d),flip(e)]. given #872 (T,wt=15): 11602 k = b | p(j,b) | p(m,b) | j = m | j = b. [para(29(b,1),11111(c,2)),merge(e)]. given #873 (A,wt=26): 507 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(j,b) | p(g(j),j) | k = x | p(k,j). [para(39(c,1),139(c,2))]. given #874 (T,wt=15): 11609 p(j,b) | p(m,b) | j = m | j = b | p(k,k). [para(11111(c,1),4128(a,2)),merge(f)]. given #875 (T,wt=15): 11610 p(m,b) | p(k,m) | p(j,b) | j = m | j = b. [para(4187(b,1),11111(c,2)),merge(d),merge(f)]. given #876 (T,wt=12): 11668 p(m,b) | p(k,m) | p(j,b) | j = b. [para(11610(d,1),4128(a,2)),merge(e),merge(f)]. given #877 (T,wt=9): 11680 p(m,b) | p(k,m) | p(j,b). [para(11668(d,1),4157(a,2)),merge(d),merge(e)]. given #878 (A,wt=19): 508 p(j,b) | p(g(j),j) | p(k,j) | j = x | -p(x,b) | k = x. [para(139(c,1),95(c,2)),merge(d)]. given #879 (T,wt=15): 11632 k = b | p(j,b) | p(m,b) | j = b | -p(b,m). [factor(11627,a,g),merge(e)]. given #880 (T,wt=15): 11706 k = b | p(j,b) | p(m,b) | j = b | p(b,b). [resolve(11632,e,6170,a)]. given #881 (T,wt=12): 11726 k = b | p(j,b) | p(m,b) | p(b,b). [para(11706(d,1),4157(a,2)),merge(e),merge(f)]. given #882 (T,wt=9): 11739 p(j,b) | p(m,b) | p(b,b). [para(11726(a,1),2739(a,2)),merge(d),merge(e)]. given #883 (A,wt=18): 509 p(j,b) | p(g(j),j) | p(k,j) | g(j) = j | g(j) != b. [factor(504,b,e),flip(d),flip(e)]. given #884 (T,wt=9): 11752 p(m,b) | k = m | p(b,b). [para(4170(b,1),11739(a,1)),merge(c),merge(d)]. given #885 (T,wt=15): 11769 p(m,b) | p(b,b) | j = x | p(x,j) | m != x. [para(11752(b,1),33(c,1))]. given #886 (T,wt=16): 11186 p(m,j) | p(j,b) | p(m,g(j)) | j = b | p(b,j). [resolve(11031,b,33,c)]. given #887 (T,wt=16): 11205 p(m,j) | p(j,b) | p(j,g(m)) | j = b | p(b,j). [resolve(11032,b,33,c)]. given #888 (A,wt=22): 525 p(j,b) | p(g(j),j) | p(m,j) | k = x | m = x | b = x | -p(x,b). [para(141(d,1),6(d,2))]. given #889 (T,wt=16): 11611 p(m,b) | p(j,b) | p(g(j),j) | j = m | j = b. [para(4178(b,1),11111(c,2)),merge(d),merge(e),merge(g)]. given #890 (T,wt=13): 11840 p(m,b) | p(j,b) | p(g(j),j) | j = b. [resolve(11611,d,60,c(flip)),merge(e),merge(f)]. given #891 (T,wt=10): 11846 p(m,b) | p(j,b) | p(g(j),j). [para(11840(d,1),4157(a,2)),merge(d),merge(e)]. given #892 (T,wt=13): 11862 p(m,b) | k = m | p(j,b) | p(g(j),m). [para(4170(b,1),11846(c,2)),merge(c)]. given #893 (A,wt=20): 526 p(x,b) | p(x,g(x)) | p(j,b) | p(g(j),j) | p(m,j) | k = x. [para(20(a,1),141(d,2))]. given #894 (T,wt=14): 11858 p(m,b) | p(j,b) | g(j) = j | g(j) = k. [resolve(11846,c,31,b),flip(c),flip(d)]. given #895 (T,wt=13): 11895 p(m,b) | p(j,b) | g(j) = k | j = b. [resolve(11858,c,18,c),flip(d),merge(e)]. given #896 (T,wt=12): 11910 p(m,b) | p(j,b) | j = b | k != b. [para(11895(c,1),16(c,1)),flip(d),merge(d),merge(e)]. given #897 (T,wt=12): 11911 p(m,b) | p(j,b) | j = b | j != k. [para(11895(c,1),18(c,1)),flip(d),flip(f),merge(d),merge(e)]. given #898 (A,wt=20): 527 p(x,b) | p(g(x),x) | p(j,b) | p(g(j),j) | p(m,j) | k = x. [para(22(a,1),141(d,2))]. given #899 (T,wt=12): 11946 p(m,b) | p(j,b) | j = b | j = m. [resolve(11911,d,11111,c),merge(d),merge(e),merge(g)]. given #900 (T,wt=12): 11985 p(m,b) | p(j,b) | j = b | k != m. [para(11946(d,1),11911(d,1)),flip(g),merge(d),merge(e),merge(f)]. given #901 (T,wt=12): 11995 p(m,b) | p(j,b) | j = b | k = b. [resolve(11985,d,29,b)]. given #902 (T,wt=9): 12007 p(m,b) | p(j,b) | k = b. [para(11995(c,1),4157(a,2)),merge(d),merge(e)]. given #903 (A,wt=19): 528 p(j,b) | p(g(j),j) | p(m,j) | j = x | p(x,j) | b != x. [para(141(d,1),33(c,1))]. given #904 (T,wt=6): 12017 p(m,b) | p(j,b). [para(12007(c,1),2739(a,2)),merge(c),merge(d)]. given #905 (T,wt=6): 12034 p(m,b) | k = m. [para(4170(b,1),12017(b,1)),merge(c),merge(d)]. given #906 (T,wt=12): 12036 p(m,b) | j = x | p(x,j) | m != x. [para(12034(b,1),33(c,1))]. given #907 (T,wt=13): 12028 p(x,b) | p(x,g(x)) | p(m,b) | p(j,x). [para(20(a,1),12017(b,2))]. given #908 (A,wt=26): 529 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(j,b) | p(g(j),j) | p(m,j) | k = x. [para(34(c,1),141(d,2))]. given #909 (T,wt=13): 12029 p(x,b) | p(g(x),x) | p(m,b) | p(j,x). [para(22(a,1),12017(b,2))]. given #910 (T,wt=15): 12027 p(m,b) | j = m | p(j,m) | j = b | -p(b,j). [resolve(12017,b,2,e),flip(b),flip(e),unit_del(d,27)]. given #911 (T,wt=15): 12035 p(m,b) | k = x | m = x | b = x | -p(x,m). [para(12034(b,1),6(d,2))]. given #912 (T,wt=15): 12091 p(m,b) | g(m) = k | g(m) = m | g(m) = b. [resolve(12035,e,57,b),flip(b),flip(c),flip(d),merge(e)]. given #913 (A,wt=26): 530 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(j,b) | p(g(j),j) | p(m,j) | k = x. [para(39(c,1),141(d,2))]. given #914 (T,wt=11): 12118 p(m,b) | g(m) = m | g(m) = b. [para(12034(b,1),12091(b,2)),merge(b),merge(d)]. given #915 (T,wt=7): 12127 p(m,b) | g(m) = b. [resolve(12118,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #916 (T,wt=3): 12132 p(m,b). [resolve(12127,b,16,c),flip(b),merge(c),unit_del(b,27)]. given #917 (T,wt=10): 12150 p(x,b) | p(x,g(x)) | p(m,x). [para(20(a,1),12132(a,2))]. given #918 (A,wt=20): 538 p(x,b) | p(x,g(x)) | p(k,b) | p(g(k),k) | j = x | p(k,j). [para(20(a,1),167(c,2))]. given #919 (T,wt=10): 12151 p(x,b) | p(g(x),x) | p(m,x). [para(22(a,1),12132(a,2))]. given #920 (T,wt=12): 12149 b = x | m = x | -p(m,x) | -p(x,m). [resolve(12132,a,4,b),flip(a),flip(c),unit_del(a,27)]. given #921 (T,wt=13): 12166 p(j,b) | p(j,g(j)) | j = m | k = m. [resolve(12150,c,31,b)]. given #922 (T,wt=10): 12196 p(j,b) | p(j,g(j)) | k = m. [resolve(12166,c,59,c(flip)),merge(d),merge(e)]. given #923 (A,wt=20): 539 p(x,b) | p(g(x),x) | p(k,b) | p(g(k),k) | j = x | p(k,j). [para(22(a,1),167(c,2))]. given #924 (T,wt=10): 12207 p(j,b) | p(j,g(j)) | p(k,j). [para(12196(c,1),133(c,1)),merge(c),merge(d),unit_del(c,27)]. given #925 (T,wt=10): 12235 p(k,j) | p(j,b) | p(j,g(k)). [para(65(a,1),12207(b,2,1)),merge(d)]. given #926 (T,wt=13): 12236 k = b | p(k,j) | p(j,b) | p(m,g(j)). [para(94(b,1),12207(b,1)),merge(e)]. given #927 (T,wt=13): 12237 k = b | p(k,j) | p(j,b) | p(j,g(m)). [para(94(b,1),12207(b,2,1)),merge(e)]. given #928 (A,wt=26): 540 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(k,b) | p(g(k),k) | j = x | p(k,j). [para(34(c,1),167(c,2))]. given #929 (T,wt=13): 12270 k = b | p(k,j) | p(j,b) | p(m,g(k)). [para(94(b,1),12235(c,1)),merge(c)]. given #930 (T,wt=13): 12293 p(k,j) | p(j,b) | p(m,g(j)) | j = b. [para(12236(a,1),65(a,2)),merge(e)]. given #931 (T,wt=13): 12305 p(k,j) | p(j,b) | p(j,g(m)) | j = b. [para(12237(a,1),65(a,2)),merge(e)]. given #932 (T,wt=13): 12325 p(k,j) | p(j,b) | p(m,g(k)) | j = b. [para(12270(a,1),65(a,2)),merge(e)]. given #933 (A,wt=26): 541 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(k,b) | p(g(k),k) | j = x | p(k,j). [para(39(c,1),167(c,2))]. given #934 (T,wt=14): 12188 p(j,b) | p(m,j) | g(j) = j | g(j) = k. [resolve(12151,b,31,b),flip(c),flip(d)]. given #935 (T,wt=13): 12363 p(j,b) | p(m,j) | g(j) = k | j = b. [resolve(12188,c,18,c),flip(d),merge(e)]. given #936 (T,wt=12): 12422 p(j,b) | p(m,j) | j = b | k != b. [para(12363(c,1),16(c,1)),flip(d),merge(d),merge(e)]. given #937 (T,wt=12): 12423 p(j,b) | p(m,j) | j = b | j != k. [para(12363(c,1),18(c,1)),flip(d),flip(f),merge(d),merge(e)]. given #938 (A,wt=35): 548 p(x,b) | p(b,k) | p(x,j) | p(y,b) | p(g(y),y) | g(x) = b | -p(g(x),y) | b = x | g(x) = x | -p(g(x),x). [resolve(314,b,41,h),flip(f),flip(i)]. given #939 (T,wt=12): 12438 p(j,b) | p(m,j) | j = b | p(j,k). [para(12363(c,1),2242(c,2)),merge(e),merge(f)]. given #940 (T,wt=12): 12451 p(j,b) | p(m,j) | j = b | p(k,j). [para(12363(c,1),12151(b,1)),merge(d),merge(f)]. given #941 (T,wt=12): 12456 p(j,b) | p(m,j) | j = b | p(b,b). [resolve(12422,d,6625,c),merge(e)]. given #942 (T,wt=12): 12457 p(j,b) | p(m,j) | j = b | p(b,m). [resolve(12422,d,6100,a)]. given #943 (A,wt=34): 549 p(x,b) | p(b,k) | p(x,j) | p(y,b) | p(g(y),y) | b = x | -p(x,y) | g(x) = b | g(x) = x | -p(g(x),x). [resolve(314,b,41,g),flip(h)]. given #944 (T,wt=12): 12508 p(j,b) | p(m,j) | p(j,k) | j = k. [resolve(12438,c,26,b(flip)),flip(d),merge(e)]. given #945 (T,wt=12): 12514 p(j,b) | p(m,j) | p(j,k) | k = b. [para(12438(c,1),62(a,1)),flip(d),merge(e),unit_del(d,27)]. given #946 (T,wt=12): 12539 p(j,b) | p(m,j) | p(k,j) | k = b. [para(12451(c,1),65(a,1)),flip(d),merge(e)]. given #947 (T,wt=12): 12560 p(j,b) | p(m,j) | p(b,b) | p(k,b). [para(12456(c,1),8749(b,2)),merge(d)]. given #948 (A,wt=35): 550 p(x,b) | p(b,k) | p(x,j) | p(y,b) | p(y,g(y)) | g(x) = b | -p(g(x),y) | b = x | g(x) = x | -p(g(x),x). [resolve(314,b,36,h),flip(f),flip(i)]. given #949 (T,wt=12): 12577 p(j,b) | p(m,j) | p(b,m) | p(k,b). [para(12457(c,1),6329(b,2)),merge(d)]. given #950 (T,wt=13): 12365 p(k,j) | p(j,b) | p(m,j) | g(j) = k. [para(65(a,1),12188(c,2)),merge(e)]. given #951 (T,wt=9): 12701 p(k,j) | p(j,b) | p(m,j). [para(12365(d,1),12151(b,1)),merge(d),merge(e),merge(f)]. given #952 (T,wt=9): 12707 p(k,j) | p(k,b) | p(m,j). [para(65(a,1),12701(b,1)),merge(b)]. given #953 (A,wt=34): 551 p(x,b) | p(b,k) | p(x,j) | p(y,b) | p(y,g(y)) | b = x | -p(x,y) | g(x) = b | g(x) = x | -p(g(x),x). [resolve(314,b,36,g),flip(h)]. given #954 (T,wt=9): 12725 k = b | p(m,j) | p(k,b). [para(29(b,1),12707(a,1)),merge(d)]. given #955 (T,wt=9): 12772 p(m,j) | p(k,b) | p(b,j). [para(12725(a,1),12707(a,1)),merge(d),merge(e)]. given #956 (T,wt=12): 12741 p(j,b) | p(m,j) | p(j,k) | p(k,b). [para(12438(c,1),12707(a,2)),merge(e),merge(f)]. given #957 (T,wt=9): 12798 p(m,j) | p(k,b) | p(j,b). [para(12725(a,1),12741(c,2)),merge(d),merge(e),merge(f)]. given #958 (A,wt=28): 552 p(x,b) | p(b,k) | p(x,j) | g(x) = b | -p(g(x),b) | b = x | g(x) = x | -p(g(x),x). [resolve(314,b,4,f),flip(d),flip(g)]. given #959 (T,wt=13): 12417 p(j,b) | p(m,j) | g(j) = k | p(j,j). [para(12188(c,1),12150(b,2)),merge(d),merge(f)]. given #960 (T,wt=12): 12838 p(j,b) | p(m,j) | p(j,j) | p(j,k). [para(12417(c,1),570(b,2)),merge(d),merge(f),merge(g)]. given #961 (T,wt=9): 12855 p(j,b) | p(m,j) | p(j,k). [para(12438(c,1),12838(c,2)),merge(d),merge(e),merge(f),merge(g)]. given #962 (T,wt=9): 12876 p(b,m) | p(j,b) | p(m,j). [para(6100(a,1),12855(c,2)),merge(d)]. given #963 (A,wt=28): 553 p(x,b) | p(b,k) | p(x,j) | g(x) = m | p(g(x),m) | m = x | g(x) = x | -p(g(x),x). [resolve(314,b,2,f),flip(d),flip(g)]. given #964 (T,wt=9): 12877 p(b,b) | p(m,j) | p(j,b). [para(6625(c,1),12855(c,2)),merge(d),merge(e)]. given #965 (T,wt=10): 12878 p(m,j) | p(j,b) | p(m,g(j)). [para(11031(b,1),12855(c,2)),merge(d),merge(e),merge(f)]. given #966 (T,wt=10): 12879 p(m,j) | p(j,b) | p(j,g(m)). [para(11032(b,1),12855(c,2)),merge(d),merge(e),merge(f)]. given #967 (T,wt=12): 12868 k = b | p(j,b) | p(m,j) | p(j,m). [para(29(b,1),12855(c,2))]. given #968 (A,wt=19): 555 p(x,b) | p(x,g(x)) | p(x,j) | p(k,j) | j = b | k = b. [resolve(314,c,95,c)]. given #969 (T,wt=9): 12947 p(j,b) | p(m,j) | p(j,m). [para(12868(a,1),12855(c,2)),merge(d),merge(e),merge(f)]. given #970 (T,wt=12): 12880 p(b,m) | p(m,j) | j = m | j = b. [resolve(12876,b,6345,d),merge(c)]. given #971 (T,wt=9): 12965 p(b,m) | p(m,j) | j = b. [para(12880(c,1),6342(b,2)),merge(d),merge(e)]. given #972 (T,wt=9): 12980 p(b,m) | p(m,j) | p(k,b). [para(12965(c,1),6329(b,2)),merge(c)]. given #973 (A,wt=20): 556 p(x,b) | p(x,g(x)) | p(y,b) | p(y,g(y)) | p(x,k) | p(y,j). [para(20(a,1),314(c,1))]. given #974 (T,wt=12): 12955 p(m,j) | k = b | p(j,b) | p(m,m). [para(62(a,1),12947(c,1)),merge(d)]. given #975 (T,wt=9): 13045 p(m,j) | p(j,b) | p(m,m). [para(12955(b,1),12855(c,2)),merge(d),merge(e),merge(f)]. given #976 (T,wt=12): 12966 p(b,m) | p(m,j) | j = k | p(j,k). [resolve(12965,c,26,b(flip)),flip(c)]. given #977 (T,wt=12): 13056 p(b,m) | p(m,j) | p(j,k) | p(k,k). [para(12966(c,1),6329(b,2)),merge(d)]. given #978 (A,wt=20): 557 p(x,b) | p(g(x),x) | p(y,b) | p(y,g(y)) | p(x,k) | p(y,j). [para(22(a,1),314(c,1))]. given #979 (T,wt=13): 12813 p(k,b) | p(k,g(k)) | p(m,j) | p(j,k). [factor(12803,a,d)]. given #980 (T,wt=13): 12814 p(k,b) | p(g(k),k) | p(m,j) | p(j,k). [factor(12804,a,d)]. given #981 (T,wt=13): 12936 p(m,j) | k = b | p(j,b) | p(m,g(m)). [para(62(a,1),12879(c,1)),merge(c)]. given #982 (T,wt=10): 13161 p(m,j) | p(j,b) | p(m,g(m)). [para(12936(b,1),12855(c,2)),merge(d),merge(e),merge(f)]. given #983 (A,wt=26): 559 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(y,b) | p(y,g(y)) | p(x,k) | p(y,j). [para(34(c,1),314(c,1))]. given #984 (T,wt=13): 12953 p(j,b) | p(m,j) | j = m | p(f(j),j). [resolve(12947,c,14,b),flip(c)]. given #985 (T,wt=13): 12954 p(j,b) | p(m,j) | j = m | p(j,f(j)). [resolve(12947,c,12,b),flip(c)]. given #986 (T,wt=13): 12987 p(x,b) | p(x,g(x)) | p(b,m) | p(m,j). [para(6147(c,1),12980(c,1)),merge(d),merge(f)]. given #987 (T,wt=13): 12988 p(x,b) | p(g(x),x) | p(b,m) | p(m,j). [para(6148(c,1),12980(c,1)),merge(d),merge(f)]. given #988 (A,wt=20): 561 p(k,b) | p(k,g(k)) | p(x,b) | p(x,g(x)) | p(b,b) | p(x,j). [para(137(c,1),314(c,2))]. given #989 (T,wt=13): 13149 p(m,j) | p(k,b) | p(g(b),k) | p(j,k). [para(12725(a,1),12814(b,1,1)),merge(c),merge(e)]. given #990 (T,wt=13): 13150 p(m,j) | p(k,b) | p(g(k),b) | p(j,k). [para(12725(a,1),12814(b,2)),merge(c),merge(e)]. given #991 (T,wt=13): 13316 p(m,j) | p(k,b) | p(g(b),b) | p(j,k). [para(12725(a,1),13149(c,2)),merge(c),merge(d)]. given #992 (T,wt=14): 12199 p(j,b) | p(j,g(j)) | p(k,b) | p(g(k),k). [resolve(12196,c,60,c(flip))]. given #993 (A,wt=20): 562 p(k,b) | p(g(k),k) | p(x,b) | p(x,g(x)) | p(b,b) | p(x,j). [para(143(c,1),314(c,2))]. given #994 (T,wt=14): 12200 p(j,b) | p(j,g(j)) | p(k,b) | p(k,g(k)). [resolve(12196,c,59,c(flip))]. given #995 (T,wt=14): 12238 p(j,b) | p(g(j),j) | p(k,j) | p(b,g(j)). [para(506(d,1),12207(b,1)),merge(d),merge(f)]. given #996 (T,wt=14): 12239 p(j,b) | p(g(j),j) | p(k,j) | p(j,g(b)). [para(506(d,1),12207(b,2,1)),merge(d),merge(f)]. given #997 (T,wt=14): 12272 p(j,b) | p(g(j),j) | p(k,j) | p(b,g(k)). [para(506(d,1),12235(c,1)),merge(d),merge(e)]. given #998 (A,wt=26): 563 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(y,b) | p(y,g(y)) | p(x,k) | p(y,j). [para(39(c,1),314(c,1))]. given #999 (T,wt=14): 12298 p(k,j) | p(j,b) | p(m,g(j)) | p(j,g(b)). [para(12236(a,1),12235(c,2,1)),merge(d),merge(e)]. given #1000 (T,wt=14): 12310 p(k,j) | p(j,b) | p(j,g(m)) | p(j,g(b)). [para(12237(a,1),12235(c,2,1)),merge(d),merge(e)]. given #1001 (T,wt=14): 12330 p(k,j) | p(j,b) | p(m,g(k)) | p(j,g(b)). [para(12270(a,1),12235(c,2,1)),merge(d),merge(e)]. given #1002 (T,wt=14): 12337 p(k,j) | p(j,b) | p(m,g(j)) | p(b,g(j)). [para(12293(d,1),12207(b,1)),merge(d),merge(f)]. given #1003 (A,wt=20): 572 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | p(g(x),j). [factor(559,a,d),merge(d)]. given #1004 (T,wt=14): 12338 p(k,j) | p(j,b) | p(m,g(j)) | p(b,g(k)). [para(12293(d,1),12235(c,1)),merge(d),merge(e)]. given #1005 (T,wt=14): 12345 p(k,j) | p(j,b) | p(j,g(m)) | p(b,g(j)). [para(12305(d,1),12207(b,1)),merge(d),merge(f)]. given #1006 (T,wt=14): 12346 p(k,j) | p(j,b) | p(j,g(m)) | p(b,g(k)). [para(12305(d,1),12235(c,1)),merge(d),merge(e)]. given #1007 (T,wt=14): 12353 p(k,j) | p(j,b) | p(m,g(k)) | p(b,g(j)). [para(12325(d,1),12207(b,1)),merge(d),merge(f)]. given #1008 (A,wt=22): 584 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | j = x | p(x,j). [resolve(67,d,33,c)]. given #1009 (T,wt=14): 12354 p(k,j) | p(j,b) | p(m,g(k)) | p(b,g(k)). [para(12325(d,1),12235(c,1)),merge(d),merge(e)]. given #1010 (T,wt=14): 13355 p(j,b) | p(j,g(j)) | p(k,b) | p(g(m),k). [para(12196(c,1),12199(d,1,1)),merge(c),merge(d)]. given #1011 (T,wt=14): 13356 p(j,b) | p(j,g(j)) | p(k,b) | p(g(k),m). [para(12196(c,1),12199(d,2)),merge(c),merge(d)]. given #1012 (T,wt=14): 13470 p(k,j) | p(j,b) | p(g(k),j) | p(b,g(j)). [para(65(a,1),12238(b,1,1)),merge(d)]. given #1013 (A,wt=27): 585 p(g(f(k)),b) | p(g(f(k)),g(g(f(k)))) | p(f(k),b) | p(f(k),k) | k = m | -p(k,m). [resolve(67,d,10,c(flip)),flip(e)]. given #1014 (T,wt=14): 13471 p(k,j) | p(j,b) | p(g(j),k) | p(b,g(j)). [para(65(a,1),12238(b,2)),merge(d)]. given #1015 (T,wt=14): 13488 p(k,j) | p(j,b) | p(g(k),j) | p(j,g(b)). [para(65(a,1),12239(b,1,1)),merge(d)]. given #1016 (T,wt=14): 13489 p(k,j) | p(j,b) | p(g(j),k) | p(j,g(b)). [para(65(a,1),12239(b,2)),merge(d)]. given #1017 (T,wt=14): 13506 p(k,j) | p(j,b) | p(g(k),j) | p(b,g(k)). [para(65(a,1),12272(b,1,1)),merge(d)]. given #1018 (A,wt=28): 586 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | k = y | m = y | b = y | -p(y,x). [para(67(d,1),6(d,2))]. given #1019 (T,wt=14): 13507 p(k,j) | p(j,b) | p(g(j),k) | p(b,g(k)). [para(65(a,1),12272(b,2)),merge(d)]. given #1020 (T,wt=14): 13567 p(k,j) | p(j,b) | p(m,g(j)) | p(k,g(b)). [para(65(a,1),12298(d,1)),merge(b)]. given #1021 (T,wt=14): 13588 p(k,j) | p(j,b) | p(m,g(j)) | p(b,g(b)). [para(12293(d,1),12298(d,1)),merge(d),merge(e),merge(f)]. given #1022 (T,wt=14): 13605 p(k,j) | p(j,b) | p(k,g(m)) | p(j,g(b)). [para(65(a,1),12310(c,1)),merge(b)]. given #1023 (A,wt=22): 587 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | k = b | m = x. [para(67(d,1),29(b,1)),flip(f)]. given #1024 (T,wt=14): 13614 p(k,j) | p(j,b) | p(m,g(k)) | p(k,g(b)). [para(65(a,1),12330(d,1)),merge(b)]. given #1025 (T,wt=14): 13636 p(k,j) | p(j,b) | p(m,g(k)) | p(b,g(b)). [para(12325(d,1),12330(d,1)),merge(d),merge(e),merge(f)]. given #1026 (T,wt=14): 13706 p(k,j) | p(j,b) | p(k,g(m)) | p(b,g(j)). [para(65(a,1),12345(c,1)),merge(b)]. given #1027 (T,wt=14): 13725 p(k,j) | p(j,b) | p(k,g(m)) | p(b,g(k)). [para(65(a,1),12346(c,1)),merge(b)]. given #1028 (A,wt=25): 588 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | j = y | p(y,j) | x != y. [para(67(d,1),33(c,1))]. given #1029 (T,wt=14): 13805 p(j,b) | p(j,g(j)) | p(k,b) | p(g(m),m). [para(12196(c,1),13355(d,2)),merge(c),merge(d)]. given #1030 (T,wt=14): 13836 p(k,j) | p(j,b) | p(g(k),k) | p(b,g(j)). [para(65(a,1),13470(c,2)),merge(b)]. given #1031 (T,wt=14): 13919 p(k,j) | p(j,b) | p(g(k),k) | p(j,g(b)). [para(65(a,1),13488(c,2)),merge(b)]. given #1032 (T,wt=14): 13963 p(k,j) | p(j,b) | p(g(k),k) | p(b,g(k)). [para(65(a,1),13506(c,2)),merge(b)]. given #1033 (A,wt=22): 590 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | j = x | p(k,j). [para(67(d,1),65(a,2))]. given #1034 (T,wt=14): 14047 p(k,j) | p(j,b) | p(k,g(m)) | p(k,g(b)). [para(65(a,1),13605(d,1)),merge(b)]. given #1035 (T,wt=15): 12137 p(b,b) | p(b,j) | j = b | j = m | -p(j,m). [back_unit_del(8806),unit_del(c,12132)]. given #1036 (T,wt=15): 12139 p(m,k) | p(b,b) | j = b | j = m | -p(j,m). [back_unit_del(6432),unit_del(c,12132)]. given #1037 (T,wt=15): 12466 k = b | p(j,b) | p(m,j) | j = b | j != m. [para(29(b,1),12423(d,2))]. given #1038 (A,wt=28): 601 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | p(k,j) | j = y | -p(y,x) | k = y. [para(67(d,1),95(c,2))]. given #1039 (T,wt=12): 14283 k = b | p(j,b) | p(m,j) | j = b. [resolve(12466,e,62,a),merge(e),merge(f)]. given #1040 (T,wt=9): 14312 k = b | p(j,b) | p(m,j). [para(14283(d,1),62(a,1)),flip(d),merge(e),merge(f),unit_del(d,27)]. given #1041 (T,wt=6): 14323 p(j,b) | p(m,j). [para(14312(a,1),12855(c,2)),merge(c),merge(d),merge(e)]. given #1042 (T,wt=13): 14326 p(x,b) | p(x,g(x)) | p(j,x) | p(m,j). [para(20(a,1),14323(a,2))]. given #1043 (A,wt=27): 610 p(x,b) | p(b,k) | p(x,j) | m = x | p(x,m) | g(x) = m | g(x) = x | -p(x,g(x)). [resolve(315,b,2,f),flip(f)]. given #1044 (T,wt=13): 14327 p(x,b) | p(g(x),x) | p(j,x) | p(m,j). [para(22(a,1),14323(a,2))]. given #1045 (T,wt=15): 12761 p(m,j) | p(k,b) | j = x | p(x,j) | b != x. [para(12725(a,1),33(c,1))]. given #1046 (T,wt=15): 12969 p(b,m) | p(m,j) | j = x | -p(x,b) | k = x. [para(12965(c,1),31(b,2))]. given #1047 (T,wt=12): 14391 p(b,m) | p(m,j) | j = m | k = m. [resolve(12969,d,12132,a)]. given #1048 (A,wt=19): 614 p(k,b) | p(g(k),k) | p(b,j) | j = x | -p(x,k) | k = x. [para(365(c,1),31(b,2))]. given #1049 (T,wt=9): 14394 p(b,m) | p(m,j) | k = m. [para(14391(c,1),6342(b,2)),merge(d),merge(e)]. given #1050 (T,wt=6): 14398 p(b,m) | p(m,j). [para(14394(c,1),6076(a,2)),merge(c),merge(d)]. given #1051 (T,wt=9): 14400 p(b,m) | j = m | k = m. [resolve(14398,b,31,b)]. given #1052 (T,wt=6): 14415 p(b,m) | k = m. [para(14400(b,1),6342(b,2)),merge(c),merge(d)]. given #1053 (A,wt=19): 615 p(k,b) | p(k,g(k)) | p(b,j) | j = x | -p(x,k) | k = x. [para(372(c,1),31(b,2))]. given #1054 (T,wt=3): 14422 p(b,m). [para(14415(b,1),6076(a,2)),merge(b),merge(c)]. given #1055 (T,wt=4): 14454 p(f(b),b). [resolve(14422,a,14,b),unit_del(a,27)]. given #1056 (T,wt=4): 14455 p(b,f(b)). [resolve(14422,a,12,b),unit_del(a,27)]. given #1057 (T,wt=4): 14503 p(f(b),m). [resolve(14454,a,2,e),flip(a),flip(d),unit_del(a,14457),unit_del(c,27),unit_del(d,14456),unit_del(e,14455)]. given #1058 (A,wt=26): 631 p(x,b) | p(x,g(x)) | p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | j = x | p(b,j). [para(20(a,1),68(d,2))]. given #1059 (F,wt=4): 14456 f(b) != b. [ur(10,a,27,a,b,14422,a)]. given #1060 (F,wt=4): 14457 f(b) != m. [ur(8,a,27,a,b,14422,a)]. given #1061 (F,wt=4): 14527 -p(m,f(b)). [resolve(14503,a,12149,d),flip(a),flip(b),unit_del(a,14456),unit_del(b,14457)]. given #1062 (F,wt=5): 14584 f(f(b)) != m. [ur(8,a,14457,a(flip),b,14503,a)]. given #1063 (T,wt=6): 14534 p(f(f(b)),f(b)). [resolve(14503,a,14,b),flip(a),unit_del(a,14457)]. given #1064 (T,wt=5): 14611 f(f(b)) = b. [resolve(14534,a,4,f),flip(a),flip(c),unit_del(a,14456),unit_del(b,14454),unit_del(d,14583),unit_del(e,14535)]. given #1065 (T,wt=7): 14501 p(b,k) | f(b) = k. [resolve(14454,a,88,e),flip(b),flip(c),flip(d),unit_del(c,14457),unit_del(d,14456)]. given #1066 (T,wt=3): 14637 p(b,k). [para(54(a,1),14501(b,2)),merge(b),unit_del(b,14456)]. given #1067 (A,wt=26): 632 p(x,b) | p(g(x),x) | p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | j = x | p(b,j). [para(22(a,1),68(d,2))]. given #1068 (T,wt=6): 14648 p(b,b) | p(m,j). [para(6625(c,1),14637(a,2)),merge(c)]. given #1069 (T,wt=7): 14532 p(m,k) | f(b) = k. [resolve(14503,a,85,e),flip(b),flip(c),flip(d),unit_del(c,14457),unit_del(d,14456)]. given #1070 (T,wt=3): 14671 p(m,k). [para(51(a,1),14532(b,2)),merge(b),unit_del(b,14457)]. given #1071 (T,wt=6): 14673 k = b | p(m,m). [para(29(b,1),14671(a,2))]. given #1072 (A,wt=25): 633 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(b,j) | j = x | -p(x,b) | k = x. [para(68(d,1),31(b,2))]. given #1073 (T,wt=6): 14706 p(m,m) | p(b,b). [para(14673(a,1),14637(a,2))]. given #1074 (T,wt=7): 14533 k = b | f(b) = k. [resolve(14503,a,61,e),flip(b),flip(c),flip(d),unit_del(c,14457),unit_del(d,14456)]. given #1075 (T,wt=3): 14718 k = b. [para(29(b,1),14533(b,2)),merge(b),unit_del(b,14457)]. given #1076 (T,wt=3): 14755 p(b,b). [back_rewrite(14637),rewrite(14718(2))]. given #1077 (A,wt=25): 6795 p(x,b) | p(x,m) | g(x) = b | -p(g(x),b) | b = x | g(x) = x | -p(g(x),x). [resolve(6786,b,4,f),flip(c),flip(f)]. given #1078 (T,wt=6): 14735 p(b,j) | j = m. [back_rewrite(14672),rewrite(14718(1),14718(7)),flip(c),unit_del(c,27)]. given #1079 (T,wt=6): 14854 j = b | p(b,j). [back_rewrite(65),rewrite(14718(2),14718(4))]. given #1080 (T,wt=3): 14859 p(b,j). [para(14854(a,1),14735(b,1)),flip(c),merge(b),unit_del(b,27)]. given #1081 (T,wt=7): 14753 p(x,b) | p(g(x),x). [back_rewrite(14639),rewrite(14718(5)),merge(c)]. given #1082 (A,wt=21): 6797 p(x,b) | p(x,m) | m = x | g(x) = m | g(x) = x | -p(g(x),x). [resolve(6786,b,2,e),flip(e),merge(d)]. given #1083 (T,wt=7): 14754 p(x,b) | p(x,g(x)). [back_rewrite(14638),rewrite(14718(5)),merge(c)]. given #1084 (T,wt=9): 14855 j = x | p(x,j) | b != x. [back_rewrite(33),rewrite(14718(5))]. given #1085 (T,wt=9): 14856 j = x | -p(x,j) | b = x. [back_rewrite(31),rewrite(14718(5))]. given #1086 (T,wt=9): 14857 b = x | m != x | p(x,b). [back_rewrite(24),rewrite(14718(1),14718(5))]. given #1087 (A,wt=15): 14502 b = x | f(b) = x | -p(f(b),x) | -p(x,f(b)). [resolve(14454,a,4,b),flip(a),flip(c),unit_del(a,14456)]. given #1088 (T,wt=9): 14858 b = x | m = x | -p(x,b). [back_rewrite(6),rewrite(14718(1),14718(7)),merge(c)]. ============================== PROOF ================================= % Proof 1 at 9.24 (+ 0.08) seconds. % Length of proof is 155. % Level of proof is 57. % Maximum clause weight is 23. % Given clauses 1088. 1 x = m | p(x,m) | y = m | y = x | -p(x,y) | -p(y,x). [assumption]. 2 m = x | p(x,m) | m = y | y = x | -p(x,y) | -p(y,x). [copy(1),flip(a),flip(c)]. 5 x = k | x = m | x = b | -p(x,k). [assumption]. 6 k = x | m = x | b = x | -p(x,k). [copy(5),flip(a),flip(b),flip(c)]. 7 x = m | -p(x,m) | f(x) != m. [assumption]. 8 m = x | -p(x,m) | f(x) != m. [copy(7),flip(a)]. 9 x = m | -p(x,m) | f(x) != x. [assumption]. 10 m = x | -p(x,m) | f(x) != x. [copy(9),flip(a)]. 11 x = m | -p(x,m) | p(x,f(x)). [assumption]. 12 m = x | -p(x,m) | p(x,f(x)). [copy(11),flip(a)]. 13 x = m | -p(x,m) | p(f(x),x). [assumption]. 14 m = x | -p(x,m) | p(f(x),x). [copy(13),flip(a)]. 15 x = b | p(x,b) | g(x) != b. [assumption]. 16 b = x | p(x,b) | g(x) != b. [copy(15),flip(a)]. 17 x = b | p(x,b) | g(x) != x. [assumption]. 18 b = x | p(x,b) | g(x) != x. [copy(17),flip(a)]. 19 x = b | p(x,b) | p(x,g(x)). [assumption]. 20 b = x | p(x,b) | p(x,g(x)). [copy(19),flip(a)]. 21 x = b | p(x,b) | p(g(x),x). [assumption]. 22 b = x | p(x,b) | p(g(x),x). [copy(21),flip(a)]. 23 x = k | x != m | p(x,k). [assumption]. 24 k = x | m != x | p(x,k). [copy(23),flip(a),flip(b)]. 25 x = k | x != b | p(x,k). [assumption]. 26 k = x | b != x | p(x,k). [copy(25),flip(a),flip(b)]. 27 m != b. [assumption]. 28 b = k | k = m. [assumption]. 29 k = b | k = m. [copy(28),flip(a)]. 30 x = j | -p(x,j) | x = k. [assumption]. 31 j = x | -p(x,j) | k = x. [copy(30),flip(a),flip(c)]. 32 x = j | p(x,j) | x != k. [assumption]. 33 j = x | p(x,j) | k != x. [copy(32),flip(a),flip(c)]. 51 k = m | p(m,k). [xx_res(24,b)]. 52 k = x | p(x,k) | p(x,b) | p(g(x),x). [resolve(26,b,22,a)]. 53 k = x | p(x,k) | p(x,b) | p(x,g(x)). [resolve(26,b,20,a)]. 54 k = b | p(b,k). [xx_res(26,b)]. 57 p(m,b) | p(g(m),m). [resolve(27,a,22,a(flip))]. 59 p(x,b) | p(x,g(x)) | m != x. [para(20(a,1),27(a,2))]. 60 p(x,b) | p(g(x),x) | m != x. [para(22(a,1),27(a,2))]. 61 k = b | k = x | m = x | b = x | -p(x,m). [para(29(b,1),6(d,2))]. 65 j = k | p(k,j). [xx_res(33,c)]. 93 p(b,k) | p(m,k). [para(54(a,1),51(a,1)),flip(b),unit_del(b,27)]. 95 p(k,j) | j = x | -p(x,k) | k = x. [para(65(a,1),31(b,2))]. 98 p(b,k) | p(m,b). [para(54(a,1),93(b,2)),merge(b)]. 105 p(x,b) | p(g(x),x) | p(b,k) | p(m,x). [para(22(a,1),98(b,2))]. 136 p(k,b) | p(k,g(k)) | p(m,k). [resolve(59,c,51,a(flip))]. 142 p(k,b) | p(g(k),k) | p(m,k). [resolve(60,c,51,a(flip))]. 159 p(k,b) | p(m,k) | g(k) = k | g(k) = m | g(k) = b. [resolve(142,b,6,d),flip(c),flip(d),flip(e)]. 280 p(k,j) | j = m | k = m | p(b,k). [resolve(95,c,93,b)]. 298 p(k,j) | k = m | p(b,k). [para(280(b,1),65(a,1)),flip(d),merge(d),merge(e)]. 308 p(k,j) | p(b,k). [para(298(b,1),54(a,1)),merge(d),unit_del(c,27)]. 311 p(b,k) | p(b,j). [para(54(a,1),308(a,1)),merge(c)]. 313 p(b,k) | p(b,m) | j = m | j = b | -p(j,b). [resolve(311,b,2,e),flip(d),unit_del(b,27)]. 314 p(x,b) | p(x,g(x)) | p(b,k) | p(x,j). [para(20(a,1),311(b,1))]. 321 p(x,k) | p(x,b) | p(g(x),x) | k = b | m = x. [para(52(a,1),29(b,1)),flip(e)]. 341 p(x,k) | p(x,b) | p(x,g(x)) | k = b | m = x. [para(53(a,1),29(b,1)),flip(e)]. 400 p(j,b) | p(b,k) | p(m,j) | g(j) = j | g(j) = k. [resolve(105,b,31,b),flip(d),flip(e)]. 556 p(x,b) | p(x,g(x)) | p(y,b) | p(y,g(y)) | p(x,k) | p(y,j). [para(20(a,1),314(c,1))]. 570 p(x,b) | p(x,g(x)) | p(x,k) | p(x,j). [factor(556,a,c),merge(c)]. 1542 p(x,k) | p(x,b) | p(g(x),x) | k = b. [resolve(321,e,60,c),merge(e),merge(f)]. 1605 p(x,k) | p(x,b) | p(x,g(x)) | k = b. [resolve(341,e,59,c),merge(e),merge(f)]. 1625 p(x,k) | p(x,b) | p(x,g(x)) | p(m,k). [para(1605(d,1),51(a,1)),flip(d),unit_del(d,27)]. 1650 p(x,k) | p(x,b) | p(x,g(x)) | p(y,k) | p(y,b) | p(y,g(y)) | p(m,x). [para(53(a,1),1625(d,2))]. 1657 p(x,k) | p(x,b) | p(x,g(x)) | p(y,k) | p(y,b) | p(y,g(y)) | p(m,b). [para(1605(d,1),1625(d,2))]. 1665 p(x,k) | p(x,b) | p(x,g(x)) | p(m,x). [factor(1650,a,d),merge(d),merge(e)]. 1669 p(x,k) | p(x,b) | p(x,g(x)) | p(m,b). [factor(1657,a,d),merge(d),merge(e)]. 1693 p(j,k) | p(j,b) | p(j,g(j)) | j = m | k = m. [resolve(1665,d,31,b)]. 2224 p(j,k) | p(j,b) | p(j,g(j)) | k = m. [resolve(1693,d,59,c(flip)),merge(e),merge(f)]. 2238 p(j,k) | p(j,b) | p(j,g(j)) | p(x,k) | p(x,b) | p(x,g(x)). [para(2224(d,1),1605(d,1)),unit_del(g,27)]. 2242 p(j,k) | p(j,b) | p(j,g(j)). [factor(2238,a,d),merge(d),merge(e)]. 2323 p(m,k) | p(k,b) | g(k) = m | g(k) = b. [para(51(a,1),159(c,2)),merge(c),merge(e)]. 2721 p(m,k) | p(k,b) | g(k) = b. [para(2323(c,1),142(b,1)),merge(d),merge(e),merge(f)]. 2730 p(m,k) | p(k,b). [para(2721(c,1),136(b,2)),merge(c),merge(d),merge(e)]. 2739 p(m,k) | p(m,b). [para(51(a,1),2730(b,1)),merge(b)]. 2743 p(m,b) | p(k,j) | j = m | k = m. [resolve(2739,a,95,c)]. 2756 p(x,k) | p(x,b) | p(g(x),x) | p(m,b). [para(1542(d,1),2739(a,2)),merge(e)]. 2901 p(m,b) | p(k,j) | k = m. [para(2743(c,1),65(a,1)),flip(d),merge(d),merge(e)]. 2906 p(m,b) | p(k,j) | j = x | -p(x,m) | k = x. [para(2901(c,1),95(c,2)),merge(c)]. 3315 p(j,k) | p(j,b) | p(m,b) | g(j) = j | g(j) = k. [resolve(2756,c,31,b),flip(d),flip(e)]. 4092 p(m,b) | p(k,j) | g(m) = j | g(m) = k. [resolve(2906,d,57,b),flip(c),flip(d),merge(e)]. 4095 p(k,j) | p(m,b) | g(m) = k. [para(65(a,1),4092(c,2)),merge(c),merge(e)]. 4098 p(k,j) | p(m,b) | k != m. [para(4095(c,1),18(c,1)),flip(c),merge(d),unit_del(c,27)]. 4128 p(k,j) | p(m,b). [resolve(4098,c,2901,c),merge(c),merge(d)]. 4145 k = b | p(m,j) | p(m,b). [para(29(b,1),4128(a,1))]. 4157 p(m,j) | p(m,b). [para(4145(a,1),2739(a,2)),merge(c),merge(d)]. 4170 p(m,b) | j = m | k = m. [resolve(4157,a,31,b)]. 4178 p(m,b) | k = m | p(j,b) | p(g(j),j). [resolve(4170,b,60,c(flip))]. 5761 p(j,b) | p(b,k) | p(m,j) | g(j) = k | j = b. [resolve(400,d,18,c),flip(e),merge(f)]. 5770 p(j,b) | p(b,k) | p(m,j) | j = b | k != b. [para(5761(d,1),16(c,1)),flip(e),merge(e),merge(f)]. 5796 p(j,b) | p(b,k) | p(m,j) | j = b. [resolve(5770,e,54,a),merge(e)]. 5827 p(j,b) | p(b,k) | p(m,j) | j = k | p(j,k). [resolve(5796,d,26,b(flip)),flip(d)]. 5912 p(j,b) | p(b,k) | p(m,j) | p(j,k). [para(5827(d,1),311(b,2)),merge(e),merge(f)]. 5915 p(b,k) | p(j,b) | p(m,j). [para(54(a,1),5912(d,2)),merge(c),merge(e)]. 5925 p(b,k) | p(m,j) | p(b,m) | j = m | j = b. [resolve(5915,b,313,e),merge(c)]. 5938 p(b,k) | p(m,j) | p(b,m) | j = b. [para(5925(d,1),311(b,2)),merge(e),merge(f)]. 5943 p(b,k) | p(m,j) | p(b,m) | j = k | p(j,k). [resolve(5938,d,26,b(flip)),flip(d)]. 6043 p(b,k) | p(m,j) | p(b,m) | p(j,k). [para(5943(d,1),311(b,2)),merge(e),merge(f)]. 6059 p(b,k) | p(m,j) | p(b,m). [para(5938(d,1),6043(d,1)),merge(d),merge(e),merge(f),merge(g)]. 6062 p(b,k) | p(b,m) | j = m | k = m. [resolve(6059,b,31,b)]. 6069 p(b,k) | p(b,m) | k = m. [para(6062(c,1),311(b,2)),merge(d),merge(e)]. 6076 p(b,k) | p(b,m). [para(6069(c,1),54(a,1)),merge(d),unit_del(c,27)]. 6100 k = b | p(b,m). [para(29(b,1),6076(a,2)),merge(c)]. 6102 p(m,k) | p(b,m). [para(51(a,1),6076(a,2)),merge(c)]. 6172 p(b,m) | p(k,j) | j = m | k = m. [resolve(6102,a,95,c)]. 6306 p(b,m) | p(k,j) | k = m. [para(6172(c,1),65(a,1)),flip(d),merge(d),merge(e)]. 6329 p(b,m) | p(k,j). [para(6306(c,1),6076(a,2)),merge(c),merge(d)]. 6342 p(b,m) | p(b,j). [para(6100(a,1),6329(b,1)),merge(b)]. 6345 p(b,m) | j = m | j = b | -p(j,b). [resolve(6342,b,2,e),flip(d),merge(c),unit_del(b,27)]. 10987 p(j,k) | p(j,b) | p(m,b) | g(j) = k | j = b. [resolve(3315,d,18,c),flip(e),merge(f)]. 10999 p(j,k) | p(j,b) | p(m,b) | j = b. [para(10987(d,1),1669(c,2)),merge(e),merge(f),merge(g),merge(h)]. 11102 p(j,k) | p(j,b) | p(m,b). [para(10999(d,1),4157(a,2)),merge(d),merge(e)]. 11111 p(j,b) | p(m,b) | j = k | j = m | j = b. [resolve(11102,a,6,d),flip(c),flip(d),flip(e)]. 11611 p(m,b) | p(j,b) | p(g(j),j) | j = m | j = b. [para(4178(b,1),11111(c,2)),merge(d),merge(e),merge(g)]. 11840 p(m,b) | p(j,b) | p(g(j),j) | j = b. [resolve(11611,d,60,c(flip)),merge(e),merge(f)]. 11846 p(m,b) | p(j,b) | p(g(j),j). [para(11840(d,1),4157(a,2)),merge(d),merge(e)]. 11858 p(m,b) | p(j,b) | g(j) = j | g(j) = k. [resolve(11846,c,31,b),flip(c),flip(d)]. 11895 p(m,b) | p(j,b) | g(j) = k | j = b. [resolve(11858,c,18,c),flip(d),merge(e)]. 11911