============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11480 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:56 2006 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 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 (F,wt=6): 51 k = m | p(m,k). [xx_res(24,b)]. given #19 (T,wt=6): 54 k = b | p(b,k). [xx_res(26,b)]. given #20 (T,wt=6): 65 j = k | p(k,j). [xx_res(33,c)]. given #21 (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 #22 (F,wt=6): 75 p(b,k) | p(m,k). [para(54(a,1),51(a,1)),flip(b),unit_del(b,27)]. given #23 (F,wt=6): 98 p(b,k) | p(m,b). [para(54(a,1),75(b,2)),merge(b)]. given #24 (T,wt=7): 57 p(m,b) | p(g(m),m). [resolve(27,a,22,a(flip))]. given #25 (T,wt=7): 58 p(m,b) | p(m,g(m)). [resolve(27,a,20,a(flip))]. given #26 (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 #27 (F,wt=9): 62 j = m | p(m,j) | k = b. [resolve(33,c,29,b)]. given #28 (F,wt=9): 67 p(m,k) | j = m | p(m,j). [resolve(51,a,33,c)]. given #29 (T,wt=9): 70 p(b,k) | j = b | p(b,j). [resolve(54,a,33,c)]. given #30 (T,wt=9): 76 k = b | j = m | p(k,j). [para(29(b,1),65(a,2))]. given #31 (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 #32 (F,wt=9): 78 p(m,k) | j = m | p(k,j). [para(51(a,1),65(a,2))]. given #33 (F,wt=9): 79 p(b,k) | j = b | p(k,j). [para(54(a,1),65(a,2))]. given #34 (T,wt=10): 59 p(x,b) | p(x,g(x)) | m != x. [para(20(a,1),27(a,2))]. given #35 (T,wt=10): 60 p(x,b) | p(g(x),x) | m != x. [para(22(a,1),27(a,2))]. given #36 (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 #37 (F,wt=10): 136 p(k,b) | p(k,g(k)) | p(m,k). [resolve(59,c,51,a(flip))]. given #38 (F,wt=10): 137 p(k,b) | p(k,g(k)) | k = b. [resolve(59,c,29,b(flip))]. given #39 (T,wt=10): 142 p(k,b) | p(g(k),k) | p(m,k). [resolve(60,c,51,a(flip))]. given #40 (T,wt=10): 143 p(k,b) | p(g(k),k) | k = b. [resolve(60,c,29,b(flip))]. given #41 (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 #42 (F,wt=10): 150 p(m,k) | p(k,b) | p(m,g(k)). [para(51(a,1),136(b,1)),merge(d)]. given #43 (F,wt=10): 151 p(m,k) | p(k,b) | p(k,g(m)). [para(51(a,1),136(b,2,1)),merge(d)]. given #44 (T,wt=10): 161 p(m,k) | p(k,b) | p(g(m),k). [para(51(a,1),142(b,1,1)),merge(d)]. given #45 (T,wt=10): 162 p(m,k) | p(k,b) | p(g(k),m). [para(51(a,1),142(b,2)),merge(d)]. given #46 (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 #47 (F,wt=10): 173 p(m,k) | p(m,b) | p(m,g(k)). [para(51(a,1),150(b,1)),merge(b)]. given #48 (F,wt=10): 180 p(m,k) | p(k,b) | p(m,g(m)). [para(51(a,1),151(c,1)),merge(b)]. given #49 (T,wt=10): 186 p(m,k) | p(k,b) | p(g(m),m). [para(51(a,1),161(c,2)),merge(b)]. given #50 (T,wt=12): 66 k = b | j = x | p(x,j) | m != x. [para(29(b,1),33(c,1))]. given #51 (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 #52 (F,wt=12): 69 p(m,k) | j = x | p(x,j) | m != x. [para(51(a,1),33(c,1))]. given #53 (F,wt=12): 74 p(b,k) | j = x | p(x,j) | b != x. [para(54(a,1),33(c,1))]. given #54 (T,wt=12): 77 p(k,j) | j = x | -p(x,k) | k = x. [para(65(a,1),31(b,2))]. given #55 (T,wt=12): 111 p(m,j) | k = b | j = k | p(j,k). [resolve(62,a,24,b(flip)),flip(c)]. given #56 (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 #57 (F,wt=12): 113 p(m,j) | k = b | j = b | -p(b,m). [factor(112,b,e)]. given #58 (F,wt=12): 114 p(m,k) | p(m,j) | j = k | p(j,k). [resolve(67,b,24,b(flip)),flip(c)]. given #59 (T,wt=12): 116 p(b,k) | p(b,j) | j = k | p(j,k). [resolve(70,b,26,b(flip)),flip(c)]. given #60 (T,wt=12): 122 k = b | p(k,j) | j = b | -p(b,m). [factor(121,a,e)]. given #61 (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 #62 (F,wt=12): 256 p(k,j) | j = m | k = m | p(b,k). [resolve(77,c,75,b)]. given #63 (F,wt=9): 298 p(k,j) | k = m | p(b,k). [para(256(b,1),65(a,1)),flip(d),merge(d),merge(e)]. given #64 (T,wt=6): 304 p(k,j) | p(b,k). [para(298(b,1),54(a,1)),merge(d),unit_del(c,27)]. given #65 (T,wt=6): 307 p(b,k) | p(b,j). [para(54(a,1),304(a,1)),merge(c)]. given #66 (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 #67 (F,wt=13): 52 k = x | p(x,k) | p(x,b) | p(g(x),x). [resolve(26,b,22,a)]. given #68 (F,wt=13): 53 k = x | p(x,k) | p(x,b) | p(x,g(x)). [resolve(26,b,20,a)]. given #69 (T,wt=13): 63 j = b | p(b,j) | p(k,b) | p(g(k),k). [resolve(33,c,22,a(flip))]. given #70 (T,wt=13): 64 j = b | p(b,j) | p(k,b) | p(k,g(k)). [resolve(33,c,20,a(flip))]. given #71 (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 #72 (F,wt=13): 72 p(x,b) | p(x,g(x)) | k = x | p(b,k). [para(20(a,1),54(a,2))]. given #73 (F,wt=13): 73 p(x,b) | p(g(x),x) | k = x | p(b,k). [para(22(a,1),54(a,2))]. given #74 (T,wt=13): 82 p(g(m),b) | p(g(m),g(g(m))) | p(m,b). [resolve(34,c,27,a(flip))]. given #75 (T,wt=13): 100 p(x,b) | p(x,g(x)) | p(b,k) | p(m,x). [para(20(a,1),98(b,2))]. given #76 (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 #77 (F,wt=13): 101 p(x,b) | p(g(x),x) | p(b,k) | p(m,x). [para(22(a,1),98(b,2))]. given #78 (F,wt=13): 103 p(m,b) | g(m) = m | p(f(g(m)),g(m)). [resolve(57,b,14,b),flip(b)]. given #79 (T,wt=9): 405 p(m,b) | p(f(g(m)),g(m)). [resolve(103,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #80 (T,wt=13): 104 p(m,b) | g(m) = m | p(g(m),f(g(m))). [resolve(57,b,12,b),flip(b)]. given #81 (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 #82 (F,wt=9): 415 p(m,b) | p(g(m),f(g(m))). [resolve(104,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #83 (F,wt=13): 132 p(j,b) | p(j,g(j)) | p(m,k) | p(k,j). [resolve(59,c,78,b(flip))]. given #84 (T,wt=13): 133 p(j,b) | p(j,g(j)) | k = b | p(k,j). [resolve(59,c,76,b(flip))]. given #85 (T,wt=13): 134 p(j,b) | p(j,g(j)) | p(m,k) | p(m,j). [resolve(59,c,67,b(flip))]. given #86 (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 #87 (F,wt=13): 135 p(j,b) | p(j,g(j)) | p(m,j) | k = b. [resolve(59,c,62,a(flip))]. given #88 (F,wt=13): 138 p(j,b) | p(g(j),j) | p(m,k) | p(k,j). [resolve(60,c,78,b(flip))]. given #89 (T,wt=13): 139 p(j,b) | p(g(j),j) | k = b | p(k,j). [resolve(60,c,76,b(flip))]. given #90 (T,wt=13): 140 p(j,b) | p(g(j),j) | p(m,k) | p(m,j). [resolve(60,c,67,b(flip))]. given #91 (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 #92 (F,wt=13): 141 p(j,b) | p(g(j),j) | p(m,j) | k = b. [resolve(60,c,62,a(flip))]. given #93 (F,wt=13): 154 p(k,b) | p(k,g(k)) | j = b | p(k,j). [para(137(c,1),65(a,2))]. given #94 (T,wt=13): 165 p(k,b) | p(g(k),k) | j = b | p(k,j). [para(143(c,1),65(a,2))]. given #95 (T,wt=13): 200 p(g(m),b) | p(g(g(m)),g(m)) | p(m,b). [resolve(39,c,27,a(flip))]. given #96 (A,wt=15): 61 k = b | k = x | m = x | b = x | -p(x,m). [para(29(b,1),6(d,2))]. given #97 (F,wt=13): 310 p(x,b) | p(x,g(x)) | p(b,k) | p(x,j). [para(20(a,1),307(b,1))]. given #98 (F,wt=13): 311 p(x,b) | p(g(x),x) | p(b,k) | p(x,j). [para(22(a,1),307(b,1))]. given #99 (T,wt=13): 365 p(k,b) | p(g(k),k) | j = k | p(b,j). [factor(360,a,e),merge(e)]. given #100 (T,wt=13): 372 p(k,b) | p(k,g(k)) | j = k | p(b,j). [factor(367,a,e),merge(e)]. given #101 (A,wt=15): 68 p(m,k) | k = x | m = x | b = x | -p(x,m). [para(51(a,1),6(d,2))]. given #102 (F,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 (F,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 #104 (T,wt=13): 450 p(m,k) | p(k,j) | p(j,b) | p(m,g(j)). [para(78(b,1),132(b,1)),merge(e),merge(f)]. given #105 (T,wt=13): 451 p(m,k) | p(k,j) | p(j,b) | p(j,g(m)). [para(78(b,1),132(b,2,1)),merge(e),merge(f)]. given #106 (A,wt=15): 71 p(b,k) | k = x | m = x | b = x | -p(x,b). [para(54(a,1),6(d,2))]. given #107 (F,wt=13): 457 p(j,b) | p(j,g(j)) | p(k,j) | j = b. [para(133(c,1),65(a,2)),merge(e)]. given #108 (F,wt=13): 470 p(m,k) | p(m,j) | p(j,b) | p(m,g(j)). [para(67(b,1),134(b,1)),merge(e),merge(f)]. given #109 (T,wt=13): 471 p(m,k) | p(m,j) | p(j,b) | p(j,g(m)). [para(67(b,1),134(b,2,1)),merge(e),merge(f)]. given #110 (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 #111 (A,wt=19): 80 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | k = x | p(x,k). [resolve(34,c,26,b)]. given #112 (F,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 (F,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 #114 (T,wt=13): 498 p(m,k) | p(k,j) | p(j,b) | p(g(m),j). [para(78(b,1),138(b,1,1)),merge(e),merge(f)]. given #115 (T,wt=13): 499 p(m,k) | p(k,j) | p(j,b) | p(g(j),m). [para(78(b,1),138(b,2)),merge(e),merge(f)]. given #116 (A,wt=19): 81 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 #117 (F,wt=13): 505 p(j,b) | p(g(j),j) | p(k,j) | j = b. [para(139(c,1),65(a,2)),merge(e)]. given #118 (F,wt=13): 518 p(m,k) | p(m,j) | p(j,b) | p(g(m),j). [para(67(b,1),140(b,1,1)),merge(e),merge(f)]. given #119 (T,wt=13): 519 p(m,k) | p(m,j) | p(j,b) | p(g(j),m). [para(67(b,1),140(b,2)),merge(e),merge(f)]. given #120 (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 #121 (A,wt=23): 83 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 #122 (F,wt=13): 570 p(x,b) | p(x,g(x)) | p(x,k) | p(x,j). [factor(556,a,c),merge(c)]. given #123 (F,wt=13): 573 p(k,b) | p(k,g(k)) | p(b,b) | p(k,j). [factor(561,a,c),merge(c)]. given #124 (T,wt=13): 602 p(k,j) | p(k,b) | p(k,g(j)) | p(m,k). [para(65(a,1),442(b,1)),merge(b)]. given #125 (T,wt=13): 607 p(m,k) | p(k,j) | p(m,b) | p(k,g(j)). [para(78(b,1),442(b,1)),merge(c),merge(f)]. given #126 (A,wt=20): 84 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 #127 (F,wt=13): 616 p(k,j) | p(j,b) | p(k,g(k)) | p(m,k). [para(65(a,1),443(c,1)),merge(b)]. given #128 (F,wt=13): 620 p(m,k) | p(k,j) | p(j,b) | p(m,g(k)). [para(78(b,1),443(c,1)),merge(c),merge(f)]. given #129 (T,wt=13): 628 p(k,j) | p(m,k) | p(k,b) | p(m,g(j)). [para(65(a,1),450(c,1)),merge(c)]. given #130 (T,wt=13): 633 p(m,k) | p(k,j) | p(m,b) | p(m,g(j)). [para(78(b,1),450(c,1)),merge(c),merge(d)]. given #131 (A,wt=31): 85 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 #132 (F,wt=13): 642 p(k,j) | p(m,k) | p(j,b) | p(k,g(m)). [para(65(a,1),451(d,1)),merge(c)]. given #133 (F,wt=13): 646 p(m,k) | p(k,j) | p(j,b) | p(m,g(m)). [para(78(b,1),451(d,1)),merge(c),merge(d)]. given #134 (T,wt=13): 656 p(m,k) | p(m,j) | p(m,b) | p(m,g(j)). [para(67(b,1),470(c,1)),merge(c),merge(d)]. given #135 (T,wt=13): 668 p(m,k) | p(m,j) | p(j,b) | p(m,g(m)). [para(67(b,1),471(d,1)),merge(c),merge(d)]. given #136 (A,wt=23): 86 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 #137 (F,wt=13): 674 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 (F,wt=13): 702 p(k,j) | p(j,b) | p(g(k),k) | p(m,k). [para(65(a,1),490(c,2)),merge(b)]. given #139 (T,wt=13): 706 p(m,k) | p(k,j) | p(j,b) | p(g(k),m). [para(78(b,1),490(c,2)),merge(c),merge(f)]. given #140 (T,wt=13): 721 p(m,k) | p(k,j) | p(j,b) | p(g(m),k). [para(78(b,1),491(c,1,1)),merge(c),merge(f)]. given #141 (A,wt=23): 87 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 #142 (F,wt=13): 736 p(m,k) | p(k,j) | p(j,b) | p(g(m),m). [para(78(b,1),498(d,2)),merge(c),merge(d)]. given #143 (F,wt=13): 770 p(m,k) | p(m,j) | p(j,b) | p(g(m),m). [para(67(b,1),518(d,2)),merge(c),merge(d)]. given #144 (T,wt=13): 791 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 #145 (T,wt=13): 903 p(k,j) | p(m,k) | p(m,b) | p(k,g(k)). [para(65(a,1),607(d,2,1)),merge(c)]. given #146 (A,wt=23): 88 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 #147 (F,wt=13): 907 p(m,k) | p(k,j) | p(m,b) | p(k,g(m)). [para(78(b,1),607(d,2,1)),merge(c),merge(d)]. given #148 (F,wt=13): 942 p(m,k) | p(m,j) | p(k,b) | p(m,g(j)). [para(51(a,1),628(a,1)),merge(c)]. given #149 (T,wt=14): 110 p(f(b),b) | p(f(b),g(f(b))) | -p(f(b),m). [factor(107,a,c),merge(c)]. given #150 (T,wt=14): 244 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(b),m). [factor(241,a,c),merge(c)]. given #151 (A,wt=23): 89 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 #152 (F,wt=15): 99 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 #153 (F,wt=15): 112 p(m,j) | k = b | j = x | -p(x,m) | k = x. [para(62(a,1),31(b,2))]. given #154 (T,wt=15): 115 p(m,k) | p(m,j) | j = x | -p(x,m) | k = x. [para(67(b,1),31(b,2))]. given #155 (T,wt=15): 121 k = b | p(k,j) | j = x | -p(x,m) | k = x. [para(76(b,1),31(b,2))]. given #156 (A,wt=23): 90 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 #157 (F,wt=15): 127 p(m,k) | p(k,j) | j = x | -p(x,m) | k = x. [para(78(b,1),31(b,2))]. given #158 (F,wt=15): 260 p(m,j) | k = b | p(j,k) | j = b | -p(b,k). [factor(259,b,f)]. given #159 (T,wt=15): 308 p(b,k) | j = m | p(j,m) | j = b | -p(j,b). [resolve(307,b,2,f),flip(b),flip(e),unit_del(d,27)]. given #160 (T,wt=15): 309 p(b,k) | p(b,m) | j = m | j = b | -p(j,b). [resolve(307,b,2,e),flip(d),unit_del(b,27)]. given #161 (A,wt=22): 91 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 #162 (F,wt=15): 1256 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(b)),m). [factor(1251,a,c),merge(c)]. given #163 (F,wt=15): 1262 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(b)),m). [factor(1258,a,c),merge(c)]. given #164 (T,wt=16): 92 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | m != x. [para(34(c,1),27(a,2))]. given #165 (T,wt=16): 153 p(k,b) | p(k,g(k)) | j = x | p(x,j) | b != x. [para(137(c,1),33(c,1))]. given #166 (A,wt=19): 93 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 #167 (F,wt=16): 164 p(k,b) | p(g(k),k) | j = x | p(x,j) | b != x. [para(143(c,1),33(c,1))]. given #168 (F,wt=16): 190 p(m,k) | p(k,b) | g(k) = m | p(f(g(k)),g(k)). [resolve(162,c,14,b),flip(c)]. given #169 (T,wt=12): 1334 p(m,k) | p(k,b) | p(f(g(k)),g(k)). [para(190(c,1),142(b,1)),merge(d),merge(e),merge(f)]. given #170 (T,wt=12): 1348 p(m,k) | p(k,b) | p(f(g(m)),g(k)). [para(51(a,1),1334(c,1,1,1)),merge(b)]. given #171 (A,wt=29): 94 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 #172 (F,wt=12): 1349 p(m,k) | p(k,b) | p(f(g(k)),g(m)). [para(51(a,1),1334(c,2,1)),merge(b)]. given #173 (F,wt=12): 1372 p(m,k) | p(k,b) | p(f(g(m)),g(m)). [para(51(a,1),1348(c,2,1)),merge(b)]. given #174 (T,wt=16): 191 p(m,k) | p(k,b) | g(k) = m | p(g(k),f(g(k))). [resolve(162,c,12,b),flip(c)]. given #175 (T,wt=12): 1422 p(m,k) | p(k,b) | p(g(k),f(g(k))). [para(191(c,1),142(b,1)),merge(d),merge(e),merge(f)]. given #176 (A,wt=22): 95 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = b | g(g(x)) != x. [factor(86,a,e),flip(d)]. given #177 (F,wt=12): 1437 p(m,k) | p(k,b) | p(g(m),f(g(k))). [para(51(a,1),1422(c,1,1)),merge(b)]. given #178 (F,wt=12): 1438 p(m,k) | p(k,b) | p(g(k),f(g(m))). [para(51(a,1),1422(c,2,1,1)),merge(b)]. given #179 (T,wt=12): 1464 p(m,k) | p(k,b) | p(g(m),f(g(m))). [para(51(a,1),1437(c,2,1,1)),merge(b)]. given #180 (T,wt=16): 210 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | m != x. [para(39(c,1),27(a,2))]. given #181 (A,wt=17): 96 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | g(x) = x. [factor(87,a,e),flip(d),merge(e)]. given #182 (F,wt=16): 318 p(x,k) | p(x,b) | p(g(x),x) | j = x | p(x,j). [resolve(52,a,33,c)]. given #183 (F,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 #184 (T,wt=13): 1538 p(x,k) | p(x,b) | p(g(x),x) | k = b. [resolve(321,e,60,c),merge(e),merge(f)]. given #185 (T,wt=13): 1564 p(x,k) | p(x,b) | p(g(x),x) | p(m,k). [para(1538(d,1),51(a,1)),flip(d),unit_del(d,27)]. given #186 (A,wt=19): 102 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 #187 (F,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 #188 (F,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 #189 (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 #190 (T,wt=13): 1624 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 #191 (A,wt=19): 105 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 #192 (F,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 #193 (F,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 #194 (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 #195 (T,wt=16): 392 p(j,b) | p(j,g(j)) | p(b,k) | j = m | k = m. [resolve(100,d,31,b)]. given #196 (A,wt=19): 106 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 #197 (F,wt=13): 1712 p(j,b) | p(j,g(j)) | p(b,k) | k = m. [resolve(392,d,59,c(flip)),merge(e),merge(f)]. given #198 (F,wt=10): 1723 p(j,b) | p(j,g(j)) | p(b,k). [para(1712(d,1),54(a,1)),merge(e),unit_del(d,27)]. given #199 (T,wt=15): 1714 p(m,b) | g(m) = b | -p(g(m),b) | g(m) = m. [resolve(106,e,57,b),merge(e)]. given #200 (T,wt=16): 474 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(j)). [para(114(c,1),134(b,1)),merge(f),merge(g)]. given #201 (A,wt=20): 107 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 #202 (F,wt=13): 1751 p(m,k) | p(m,j) | p(j,b) | p(k,g(j)). [para(67(b,1),474(c,1)),merge(c),merge(d),merge(e)]. given #203 (F,wt=13): 1764 p(m,k) | p(m,j) | p(m,b) | p(k,g(j)). [para(67(b,1),1751(c,1)),merge(c),merge(d)]. given #204 (T,wt=13): 1781 p(m,k) | p(m,j) | p(m,b) | p(k,g(m)). [para(67(b,1),1764(d,2,1)),merge(c),merge(d)]. given #205 (T,wt=16): 475 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(j,g(k)). [para(114(c,1),134(b,2,1)),merge(f),merge(g)]. given #206 (A,wt=20): 108 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 #207 (F,wt=16): 522 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),j). [para(114(c,1),140(b,1,1)),merge(f),merge(g)]. given #208 (F,wt=16): 523 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(j),k). [para(114(c,1),140(b,2)),merge(f),merge(g)]. given #209 (T,wt=16): 558 k = b | p(x,b) | p(x,g(x)) | p(b,m) | p(x,j). [para(29(b,1),310(c,2))]. given #210 (T,wt=13): 1854 p(b,b) | p(b,g(b)) | p(b,m) | p(b,j). [factor(1852,a,e)]. given #211 (A,wt=26): 109 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 #212 (F,wt=16): 559 p(m,k) | p(x,b) | p(x,g(x)) | p(b,m) | p(x,j). [para(51(a,1),310(c,2))]. given #213 (F,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 #214 (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 #215 (T,wt=16): 670 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(m)). [para(114(c,1),471(d,1)),merge(d),merge(e)]. given #216 (A,wt=25): 123 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 #217 (F,wt=13): 1985 p(m,k) | p(m,j) | p(j,b) | p(k,g(m)). [para(67(b,1),670(c,1)),merge(c),merge(d),merge(e)]. given #218 (F,wt=16): 772 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(m),k). [para(114(c,1),518(d,2)),merge(d),merge(e)]. given #219 (T,wt=16): 785 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),m). [para(114(c,1),519(d,1,1)),merge(d),merge(e)]. given #220 (T,wt=16): 871 k = b | p(k,b) | p(m,g(k)) | p(b,b) | p(k,j). [para(29(b,1),573(b,1))]. given #221 (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 #222 (F,wt=16): 872 k = b | p(k,b) | p(k,g(m)) | p(b,b) | p(k,j). [para(29(b,1),573(b,2,1))]. given #223 (F,wt=16): 1299 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(b))),m). [factor(1294,a,c),merge(c)]. given #224 (T,wt=16): 1305 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(b))),m). [factor(1301,a,c),merge(c)]. given #225 (T,wt=16): 1310 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(m,k). [resolve(92,d,51,a(flip))]. given #226 (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 #227 (F,wt=16): 1311 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | k = b. [resolve(92,d,29,b(flip))]. given #228 (F,wt=16): 1508 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | p(m,k). [resolve(210,d,51,a(flip))]. given #229 (T,wt=16): 1509 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | k = b. [resolve(210,d,29,b(flip))]. given #230 (T,wt=16): 1534 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | j = k. [factor(1516,a,f)]. given #231 (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 #232 (F,wt=16): 1559 p(x,k) | p(x,b) | p(g(x),x) | j = b | p(b,j). [resolve(1538,d,33,c)]. given #233 (F,wt=16): 1565 p(x,k) | p(x,b) | p(g(x),x) | j = b | p(k,j). [para(1538(d,1),65(a,2))]. given #234 (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 #235 (T,wt=16): 1625 p(x,k) | p(x,b) | p(x,g(x)) | j = b | p(k,j). [para(1605(d,1),65(a,2))]. given #236 (A,wt=19): 152 p(k,b) | p(k,g(k)) | k = x | m = x | b = x | -p(x,b). [para(137(c,1),6(d,2))]. given #237 (F,wt=16): 1684 p(j,k) | p(j,b) | p(j,g(j)) | j = m | k = m. [resolve(1665,d,31,b)]. given #238 (F,wt=13): 2217 p(j,k) | p(j,b) | p(j,g(j)) | k = m. [resolve(1684,d,59,c(flip)),merge(e),merge(f)]. given #239 (T,wt=10): 2235 p(j,k) | p(j,b) | p(j,g(j)). [factor(2231,a,d),merge(d),merge(e)]. given #240 (T,wt=13): 2248 p(k,j) | p(j,k) | p(j,b) | p(k,g(j)). [para(65(a,1),2235(c,1))]. given #241 (A,wt=18): 157 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 #242 (F,wt=13): 2249 p(k,j) | p(j,k) | p(j,b) | p(j,g(k)). [para(65(a,1),2235(c,2,1))]. given #243 (F,wt=13): 2295 p(k,j) | p(k,k) | p(j,b) | p(k,g(j)). [para(65(a,1),2248(b,1)),merge(b)]. given #244 (T,wt=13): 2327 p(k,j) | p(j,k) | p(j,b) | p(k,g(k)). [para(65(a,1),2249(d,1)),merge(b)]. given #245 (T,wt=13): 2356 p(k,j) | p(k,k) | p(k,b) | p(k,g(j)). [para(65(a,1),2295(c,1)),merge(b)]. given #246 (A,wt=19): 163 p(k,b) | p(g(k),k) | k = x | m = x | b = x | -p(x,b). [para(143(c,1),6(d,2))]. given #247 (F,wt=13): 2366 p(k,j) | p(k,k) | p(j,b) | p(k,g(k)). [para(65(a,1),2327(b,1)),merge(b)]. given #248 (F,wt=13): 2367 p(k,b) | p(k,g(k)) | p(k,j) | p(j,b). [para(137(c,1),2327(b,2)),merge(e),merge(f)]. given #249 (T,wt=10): 2439 p(k,j) | p(k,b) | p(k,g(k)). [para(65(a,1),2367(d,1)),merge(d),merge(e)]. given #250 (T,wt=13): 2450 k = b | p(k,j) | p(k,b) | p(m,g(k)). [para(29(b,1),2439(c,1))]. given #251 (A,wt=20): 166 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 #252 (F,wt=13): 2451 k = b | p(k,j) | p(k,b) | p(k,g(m)). [para(29(b,1),2439(c,2,1))]. given #253 (F,wt=13): 2479 p(k,j) | p(k,b) | p(m,g(k)) | j = b. [para(2450(a,1),65(a,2)),merge(e)]. given #254 (T,wt=13): 2502 p(k,j) | p(k,b) | p(k,g(m)) | j = b. [para(2451(a,1),65(a,2)),merge(e)]. given #255 (T,wt=14): 2300 p(j,b) | p(j,g(j)) | p(k,j) | p(k,g(j)). [para(133(c,1),2248(b,2)),merge(d),merge(e),merge(f)]. given #256 (A,wt=23): 167 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 #257 (F,wt=10): 2540 p(k,j) | p(j,b) | p(k,g(j)). [para(65(a,1),2300(b,1)),merge(d),merge(e)]. given #258 (F,wt=10): 2554 p(k,j) | p(k,b) | p(k,g(j)). [para(65(a,1),2540(b,1)),merge(b)]. given #259 (T,wt=13): 2557 k = b | p(k,j) | p(m,b) | p(k,g(j)). [para(76(b,1),2540(b,1)),merge(c)]. given #260 (T,wt=13): 2575 k = b | p(k,j) | p(k,b) | p(m,g(j)). [para(29(b,1),2554(c,1))]. given #261 (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 #262 (F,wt=13): 2595 p(k,j) | p(m,b) | p(k,g(j)) | j = b. [para(2557(a,1),65(a,2)),merge(e)]. given #263 (F,wt=13): 2607 p(k,j) | p(k,b) | p(m,g(j)) | j = b. [para(2575(a,1),65(a,2)),merge(e)]. given #264 (T,wt=13): 2626 p(k,j) | p(m,b) | p(k,g(j)) | p(b,b). [para(2595(d,1),2540(b,1)),merge(d),merge(f)]. given #265 (T,wt=13): 2647 p(k,j) | p(m,b) | p(k,g(k)) | p(b,b). [para(65(a,1),2626(c,2,1)),merge(b)]. given #266 (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 #267 (F,wt=14): 2314 p(m,k) | p(k,b) | g(k) = m | g(k) = b. [para(51(a,1),157(c,2)),merge(c),merge(e)]. given #268 (F,wt=10): 2703 p(m,k) | p(k,b) | g(k) = b. [para(2314(c,1),142(b,1)),merge(d),merge(e),merge(f)]. given #269 (T,wt=6): 2712 p(m,k) | p(k,b). [para(2703(c,1),136(b,2)),merge(c),merge(d),merge(e)]. given #270 (T,wt=6): 2720 p(m,k) | p(m,b). [para(51(a,1),2712(b,1)),merge(b)]. given #271 (A,wt=19): 195 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | k = x | p(x,k). [resolve(39,c,26,b)]. given #272 (F,wt=9): 2729 k = b | p(m,m) | p(m,b). [para(29(b,1),2720(a,2))]. given #273 (F,wt=6): 2795 p(m,m) | p(m,b). [para(2729(a,1),2720(a,2)),merge(c),merge(d)]. given #274 (T,wt=10): 2730 p(k,b) | p(k,g(k)) | p(m,b). [para(137(c,1),2720(a,2)),merge(d)]. given #275 (T,wt=10): 2731 p(k,b) | p(g(k),k) | p(m,b). [para(143(c,1),2720(a,2)),merge(d)]. given #276 (A,wt=19): 199 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 #277 (F,wt=10): 2743 p(k,j) | p(m,b) | p(k,g(j)). [para(2557(a,1),2720(a,2)),merge(d),merge(e)]. given #278 (F,wt=10): 2857 p(k,j) | p(m,b) | p(k,g(k)). [para(65(a,1),2743(c,2,1)),merge(b)]. given #279 (T,wt=12): 2726 p(m,b) | p(k,j) | j = m | k = m. [resolve(2720,a,77,c)]. given #280 (T,wt=9): 2883 p(m,b) | p(k,j) | k = m. [para(2726(c,1),65(a,1)),flip(d),merge(d),merge(e)]. given #281 (A,wt=23): 201 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 #282 (F,wt=9): 2887 p(m,b) | p(k,j) | j = m. [para(2883(c,1),65(a,2)),merge(d)]. given #283 (F,wt=10): 2894 p(m,b) | p(k,j) | p(m,g(j)). [para(2883(c,1),2743(c,1)),merge(c),merge(d)]. given #284 (T,wt=10): 2895 p(m,b) | p(k,j) | p(m,g(k)). [para(2883(c,1),2857(c,1)),merge(c),merge(d)]. given #285 (T,wt=10): 2896 p(m,b) | p(k,j) | p(k,g(m)). [para(2883(c,1),2857(c,2,1)),merge(c),merge(d)]. given #286 (A,wt=20): 202 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 #287 (F,wt=13): 2717 p(x,b) | p(x,g(x)) | p(m,k) | p(k,x). [para(20(a,1),2712(b,2))]. given #288 (F,wt=13): 2718 p(x,b) | p(g(x),x) | p(m,k) | p(k,x). [para(22(a,1),2712(b,2))]. given #289 (T,wt=13): 2733 p(j,b) | p(j,g(j)) | p(k,j) | p(m,b). [para(133(c,1),2720(a,2)),merge(e)]. given #290 (T,wt=13): 2734 p(j,b) | p(j,g(j)) | p(m,j) | p(m,b). [para(135(d,1),2720(a,2)),merge(e)]. given #291 (A,wt=31): 203 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 #292 (F,wt=13): 2735 p(j,b) | p(g(j),j) | p(k,j) | p(m,b). [para(139(c,1),2720(a,2)),merge(e)]. given #293 (F,wt=13): 2736 p(j,b) | p(g(j),j) | p(m,j) | p(m,b). [para(141(d,1),2720(a,2)),merge(e)]. given #294 (T,wt=13): 2738 p(x,k) | p(x,b) | p(g(x),x) | p(m,b). [para(1538(d,1),2720(a,2)),merge(e)]. given #295 (T,wt=13): 2806 k = b | p(k,b) | p(m,g(k)) | p(m,b). [para(29(b,1),2730(b,1))]. given #296 (A,wt=23): 204 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 #297 (F,wt=10): 3311 p(k,b) | p(m,g(k)) | p(m,b). [para(2806(a,1),2720(a,2)),merge(d),merge(e)]. given #298 (F,wt=10): 3319 k = b | p(m,b) | p(m,g(k)). [para(29(b,1),3311(a,1)),merge(d)]. given #299 (T,wt=7): 3335 p(m,b) | p(m,g(k)). [para(3319(a,1),2720(a,2)),merge(c),merge(d)]. given #300 (T,wt=13): 2807 k = b | p(k,b) | p(k,g(m)) | p(m,b). [para(29(b,1),2730(b,2,1))]. given #301 (A,wt=23): 205 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 #302 (F,wt=10): 3360 p(k,b) | p(k,g(m)) | p(m,b). [para(2807(a,1),2720(a,2)),merge(d),merge(e)]. given #303 (F,wt=13): 2823 k = b | p(k,b) | p(g(m),k) | p(m,b). [para(29(b,1),2731(b,1,1))]. given #304 (T,wt=10): 3386 p(k,b) | p(g(m),k) | p(m,b). [para(2823(a,1),2720(a,2)),merge(d),merge(e)]. given #305 (T,wt=13): 2824 k = b | p(k,b) | p(g(k),m) | p(m,b). [para(29(b,1),2731(b,2))]. given #306 (A,wt=23): 206 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 #307 (F,wt=10): 3410 p(k,b) | p(g(k),m) | p(m,b). [para(2824(a,1),2720(a,2)),merge(d),merge(e)]. given #308 (F,wt=13): 3020 k = b | p(m,b) | p(m,j) | p(m,g(j)). [para(29(b,1),2894(b,1))]. given #309 (T,wt=10): 3437 p(m,b) | p(m,j) | p(m,g(j)). [para(3020(a,1),2720(a,2)),merge(d),merge(e)]. given #310 (T,wt=13): 3067 p(m,k) | p(x,b) | p(x,g(x)) | p(m,x). [para(51(a,1),2717(d,1)),merge(d)]. given #311 (A,wt=23): 207 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 #312 (F,wt=13): 3087 p(k,j) | p(j,b) | p(j,g(k)) | p(m,b). [para(65(a,1),2733(b,2,1)),merge(d)]. given #313 (F,wt=13): 3090 p(m,b) | p(k,j) | p(j,b) | p(j,g(m)). [para(2887(c,1),2733(b,2,1)),merge(e),merge(f)]. given #314 (T,wt=13): 3261 p(k,j) | p(j,b) | p(g(k),j) | p(m,b). [para(65(a,1),2735(b,1,1)),merge(d)]. given #315 (T,wt=13): 3262 p(k,j) | p(j,b) | p(g(j),k) | p(m,b). [para(65(a,1),2735(b,2)),merge(d)]. given #316 (A,wt=23): 208 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 #317 (F,wt=13): 3267 p(m,b) | p(k,j) | p(j,b) | p(g(m),j). [para(2887(c,1),2735(b,1,1)),merge(e),merge(f)]. given #318 (F,wt=13): 3268 p(m,b) | p(k,j) | p(j,b) | p(g(j),m). [para(2887(c,1),2735(b,2)),merge(e),merge(f)]. given #319 (T,wt=13): 3520 p(k,j) | p(j,b) | p(g(k),k) | p(m,b). [para(65(a,1),3261(c,2)),merge(b)]. given #320 (T,wt=13): 3524 p(m,b) | p(k,j) | p(j,b) | p(g(k),m). [para(2887(c,1),3261(c,2)),merge(c),merge(f)]. given #321 (A,wt=22): 209 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 #322 (F,wt=13): 3544 p(m,b) | p(k,j) | p(j,b) | p(g(m),k). [para(2887(c,1),3262(c,1,1)),merge(c),merge(f)]. given #323 (F,wt=14): 2370 p(j,b) | p(j,g(j)) | p(k,j) | p(k,g(k)). [para(133(c,1),2327(b,2)),merge(d),merge(e),merge(f)]. given #324 (T,wt=14): 2371 p(j,b) | p(g(j),j) | p(k,j) | p(k,g(k)). [para(139(c,1),2327(b,2)),merge(d),merge(e),merge(f)]. given #325 (T,wt=14): 2452 p(k,b) | p(g(k),k) | p(k,j) | p(b,g(k)). [para(143(c,1),2439(c,1)),merge(d)]. given #326 (A,wt=19): 211 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 #327 (F,wt=14): 2453 p(k,b) | p(g(k),k) | p(k,j) | p(k,g(b)). [para(143(c,1),2439(c,2,1)),merge(d)]. given #328 (F,wt=14): 2487 p(k,j) | p(k,b) | p(m,g(k)) | p(b,g(k)). [para(2450(a,1),2439(c,1)),merge(d),merge(e)]. given #329 (T,wt=14): 2488 p(k,j) | p(k,b) | p(m,g(k)) | p(k,g(b)). [para(2450(a,1),2439(c,2,1)),merge(d),merge(e)]. given #330 (T,wt=14): 2510 p(k,j) | p(k,b) | p(k,g(m)) | p(b,g(k)). [para(2451(a,1),2439(c,1)),merge(d),merge(e)]. given #331 (A,wt=29): 212 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 #332 (F,wt=14): 2511 p(k,j) | p(k,b) | p(k,g(m)) | p(k,g(b)). [para(2451(a,1),2439(c,2,1)),merge(d),merge(e)]. given #333 (F,wt=14): 2576 p(k,b) | p(g(k),k) | p(k,j) | p(b,g(j)). [para(143(c,1),2554(c,1)),merge(d)]. given #334 (T,wt=14): 2588 p(k,j) | p(k,b) | p(m,g(k)) | p(b,g(j)). [para(2450(a,1),2554(c,1)),merge(d),merge(e)]. given #335 (T,wt=14): 2589 p(k,j) | p(k,b) | p(k,g(m)) | p(b,g(j)). [para(2451(a,1),2554(c,1)),merge(d),merge(e)]. given #336 (A,wt=29): 213 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 #337 (F,wt=14): 2614 p(k,j) | p(k,b) | p(m,g(j)) | p(b,g(k)). [para(2575(a,1),2439(c,1)),merge(d),merge(e)]. given #338 (F,wt=14): 2615 p(k,j) | p(k,b) | p(m,g(j)) | p(k,g(b)). [para(2575(a,1),2439(c,2,1)),merge(d),merge(e)]. given #339 (T,wt=14): 2616 p(k,j) | p(k,b) | p(m,g(j)) | p(b,g(j)). [para(2575(a,1),2554(c,1)),merge(d),merge(e)]. given #340 (T,wt=14): 3637 p(k,j) | p(j,b) | p(j,g(k)) | p(k,g(k)). [para(65(a,1),2370(b,2,1)),merge(d)]. given #341 (A,wt=19): 214 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 #342 (F,wt=10): 3971 p(k,j) | p(j,b) | p(k,g(k)). [para(65(a,1),3637(c,1)),merge(b),merge(e)]. given #343 (F,wt=14): 3752 p(k,j) | p(k,b) | p(m,g(k)) | p(b,g(b)). [para(2450(a,1),2488(d,1)),merge(d),merge(e),merge(f)]. given #344 (T,wt=14): 3919 p(k,j) | p(k,b) | p(m,g(j)) | p(b,g(b)). [para(2575(a,1),2615(d,1)),merge(d),merge(e),merge(f)]. given #345 (T,wt=15): 2886 p(m,b) | p(k,j) | j = x | p(x,j) | m != x. [para(2883(c,1),33(c,1))]. given #346 (A,wt=26): 215 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 #347 (F,wt=15): 2888 p(m,b) | p(k,j) | j = x | -p(x,m) | k = x. [para(2883(c,1),77(c,2)),merge(c)]. given #348 (F,wt=14): 4075 p(m,b) | p(k,j) | g(m) = j | g(m) = k. [resolve(2888,d,57,b),flip(c),flip(d),merge(e)]. given #349 (T,wt=10): 4078 p(k,j) | p(m,b) | g(m) = k. [para(65(a,1),4075(c,2)),merge(c),merge(e)]. given #350 (T,wt=9): 4080 p(k,j) | p(m,b) | k != b. [para(4078(c,1),16(c,1)),flip(c),merge(d),unit_del(c,27)]. given #351 (A,wt=29): 219 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 #352 (F,wt=9): 4081 p(k,j) | p(m,b) | k != m. [para(4078(c,1),18(c,1)),flip(c),merge(d),unit_del(c,27)]. given #353 (F,wt=6): 4111 p(k,j) | p(m,b). [resolve(4081,c,2883,c),merge(c),merge(d)]. given #354 (T,wt=9): 4128 k = b | p(m,j) | p(m,b). [para(29(b,1),4111(a,1))]. given #355 (T,wt=6): 4140 p(m,j) | p(m,b). [para(4128(a,1),2720(a,2)),merge(c),merge(d)]. given #356 (A,wt=22): 220 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | g(x) = b | g(g(x)) != x. [factor(204,a,e),flip(d)]. given #357 (F,wt=9): 4153 p(m,b) | j = m | k = m. [resolve(4140,a,31,b)]. given #358 (F,wt=9): 4170 p(m,b) | k = m | p(k,m). [para(4153(b,1),4111(a,2)),merge(d)]. given #359 (T,wt=12): 4163 p(m,b) | k = m | j = k | p(j,k). [resolve(4153,b,24,b(flip)),flip(c)]. given #360 (T,wt=9): 4184 p(m,b) | k = m | p(j,k). [para(4163(c,1),4153(b,1)),merge(d),merge(e),merge(f)]. given #361 (A,wt=17): 221 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | g(x) = x. [factor(207,a,e),flip(d),merge(e)]. given #362 (F,wt=13): 4161 p(m,b) | k = m | p(j,b) | p(g(j),j). [resolve(4153,b,60,c(flip))]. given #363 (F,wt=13): 4162 p(m,b) | k = m | p(j,b) | p(j,g(j)). [resolve(4153,b,59,c(flip))]. given #364 (T,wt=15): 4154 p(m,b) | j = b | -p(j,b) | j = m | -p(j,m). [resolve(4140,a,4,f),flip(b),flip(d),flip(e),unit_del(d,27)]. given #365 (T,wt=15): 4164 p(m,b) | k = m | j = x | -p(x,m) | k = x. [para(4153(b,1),31(b,2))]. given #366 (A,wt=20): 240 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 #367 (F,wt=14): 4222 p(m,b) | k = m | g(m) = j | g(m) = k. [resolve(4164,d,57,b),flip(c),flip(d),merge(e)]. given #368 (F,wt=13): 4227 p(m,b) | k = m | g(m) = k | j != b. [para(4222(c,1),16(c,1)),flip(d),merge(e),unit_del(d,27)]. given #369 (T,wt=13): 4228 p(m,b) | k = m | g(m) = k | j != m. [para(4222(c,1),18(c,1)),flip(d),merge(e),unit_del(d,27)]. given #370 (T,wt=10): 4248 p(m,b) | k = m | g(m) = k. [resolve(4228,d,4153,b),merge(d),merge(e)]. given #371 (A,wt=20): 241 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 #372 (F,wt=9): 4250 p(m,b) | k = m | k != b. [para(4248(c,1),16(c,1)),flip(c),merge(d),unit_del(c,27)]. given #373 (F,wt=11): 4255 p(m,b) | k = m | p(f(k),g(m)). [para(4248(c,1),405(b,1,1)),merge(c)]. given #374 (T,wt=11): 4256 p(m,b) | k = m | p(f(g(m)),k). [para(4248(c,1),405(b,2)),merge(c)]. given #375 (T,wt=11): 4257 p(m,b) | k = m | p(k,f(g(m))). [para(4248(c,1),415(b,1)),merge(c)]. given #376 (A,wt=26): 242 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 #377 (F,wt=11): 4258 p(m,b) | k = m | p(g(m),f(k)). [para(4248(c,1),415(b,2,1)),merge(c)]. given #378 (F,wt=12): 4266 p(m,b) | k = m | p(k,b) | p(k,k). [para(4248(c,1),3360(b,2)),merge(e)]. given #379 (T,wt=14): 4249 p(m,b) | k = m | g(m) = j | p(g(m),j). [resolve(4248,c,33,c(flip)),flip(c)]. given #380 (T,wt=13): 4305 p(m,b) | k = m | p(g(m),j) | j != b. [para(4249(c,1),16(c,1)),flip(d),merge(e),unit_del(d,27)]. given #381 (A,wt=26): 243 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 #382 (F,wt=13): 4306 p(m,b) | k = m | p(g(m),j) | j != m. [para(4249(c,1),18(c,1)),flip(d),merge(e),unit_del(d,27)]. given #383 (F,wt=10): 4333 p(m,b) | k = m | p(g(m),j). [resolve(4306,d,4153,b),merge(d),merge(e)]. given #384 (T,wt=15): 4172 p(m,b) | p(k,m) | j = x | p(x,j) | m != x. [para(4170(b,1),33(c,1))]. given #385 (T,wt=15): 4186 p(m,b) | p(j,k) | j = x | p(x,j) | m != x. [para(4184(b,1),33(c,1))]. given #386 (A,wt=19): 250 p(x,b) | p(x,g(x)) | p(b,k) | j = y | p(y,j) | x != y. [para(20(a,1),74(d,1))]. given #387 (F,wt=15): 4253 p(m,b) | k = m | p(g(m),b) | p(k,g(g(m))). [para(4248(c,1),82(b,1)),merge(e)]. given #388 (F,wt=15): 4254 p(m,b) | k = m | p(g(m),b) | p(g(m),g(k)). [para(4248(c,1),82(b,2,1)),merge(e)]. given #389 (T,wt=15): 4259 p(m,b) | k = m | p(g(m),b) | p(g(k),g(m)). [para(4248(c,1),200(b,1,1)),merge(e)]. given #390 (T,wt=15): 4260 p(m,b) | k = m | p(g(m),b) | p(g(g(m)),k). [para(4248(c,1),200(b,2)),merge(e)]. given #391 (A,wt=19): 251 p(x,b) | p(g(x),x) | p(b,k) | j = y | p(y,j) | x != y. [para(22(a,1),74(d,1))]. given #392 (F,wt=15): 4338 p(m,b) | p(g(m),j) | g(m) = j | g(m) != m. [factor(4335,b,d),flip(c),flip(d)]. given #393 (F,wt=16): 1805 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(m,g(k)). [para(67(b,1),475(e,1)),merge(c),merge(d)]. given #394 (T,wt=13): 4369 p(m,k) | p(m,j) | p(j,b) | p(m,g(k)). [para(67(b,1),1805(c,1)),merge(c),merge(d),merge(e)]. given #395 (T,wt=16): 1807 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(k,g(k)). [para(114(c,1),475(e,1)),merge(d),merge(e),merge(f)]. given #396 (A,wt=25): 252 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),74(d,1))]. given #397 (F,wt=13): 4393 p(m,k) | p(m,j) | p(j,b) | p(k,g(k)). [para(67(b,1),1807(c,1)),merge(c),merge(d),merge(e)]. given #398 (F,wt=16): 1822 p(m,k) | p(m,j) | p(j,k) | p(j,b) | p(g(k),k). [para(114(c,1),522(e,2)),merge(d),merge(e),merge(f)]. given #399 (T,wt=16): 1848 p(x,b) | p(x,g(x)) | k = x | p(b,m) | p(x,j). [factor(1838,a,d),merge(d)]. given #400 (T,wt=16): 1852 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | p(b,b). [factor(1845,a,e),merge(e),merge(g)]. given #401 (A,wt=25): 253 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),74(d,1))]. given #402 (F,wt=14): 4481 p(b,b) | p(b,g(b)) | p(b,j) | p(f(b),b). [factor(4467,a,d)]. given #403 (F,wt=14): 4482 p(b,b) | p(b,g(b)) | p(b,j) | p(b,f(b)). [factor(4468,a,d)]. given #404 (T,wt=16): 1908 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | p(m,b). [factor(1895,a,f),merge(f),merge(g)]. given #405 (T,wt=16): 1922 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 #406 (A,wt=19): 258 p(k,b) | p(g(k),k) | p(k,j) | j = x | -p(x,b) | k = x. [para(143(c,1),77(c,2))]. given #407 (F,wt=16): 2143 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | j = b. [factor(2142,a,d),merge(d),merge(e)]. given #408 (F,wt=16): 2165 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | j = k. [factor(2152,a,f)]. given #409 (T,wt=16): 2167 p(x,b) | p(g(x),x) | p(x,k) | j = x | p(b,j). [factor(2154,a,d),merge(d)]. given #410 (T,wt=16): 2197 p(x,b) | p(x,g(x)) | p(x,k) | j = x | p(b,j). [factor(2184,a,d),merge(d)]. given #411 (A,wt=18): 259 p(m,j) | k = b | p(j,k) | j = x | -p(x,k) | k = x. [para(111(c,1),31(b,2))]. given #412 (F,wt=16): 2250 p(m,j) | k = b | p(j,k) | p(j,b) | p(m,g(j)). [para(62(a,1),2235(c,1))]. given #413 (F,wt=16): 2251 p(m,j) | k = b | p(j,k) | p(j,b) | p(j,g(m)). [para(62(a,1),2235(c,2,1))]. given #414 (T,wt=16): 2252 k = b | p(k,j) | p(j,k) | p(j,b) | p(m,g(j)). [para(76(b,1),2235(c,1))]. given #415 (T,wt=16): 2253 k = b | p(k,j) | p(j,k) | p(j,b) | p(j,g(m)). [para(76(b,1),2235(c,2,1))]. given #416 (A,wt=25): 271 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 #417 (F,wt=16): 2254 p(m,j) | k = b | p(j,k) | p(j,b) | p(k,g(j)). [para(111(c,1),2235(c,1)),merge(d)]. given #418 (F,wt=16): 2255 p(m,j) | k = b | p(j,k) | p(j,b) | p(j,g(k)). [para(111(c,1),2235(c,2,1)),merge(d)]. given #419 (T,wt=16): 2329 k = b | p(k,j) | p(j,k) | p(j,b) | p(m,g(k)). [para(76(b,1),2249(d,1)),merge(c)]. given #420 (T,wt=16): 2739 p(g(k),b) | p(g(k),g(g(k))) | p(k,b) | p(m,b). [para(1311(d,1),2720(a,2)),merge(e)]. given #421 (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 #422 (F,wt=16): 2740 p(g(k),b) | p(g(g(k)),g(k)) | p(k,b) | p(m,b). [para(1509(d,1),2720(a,2)),merge(e)]. given #423 (F,wt=16): 3421 p(k,b) | p(m,b) | g(k) = m | p(f(g(k)),g(k)). [resolve(3410,b,14,b),flip(c)]. given #424 (T,wt=15): 4848 p(k,b) | p(m,b) | p(f(g(k)),g(k)) | p(k,m). [para(3421(c,1),2730(b,2)),merge(d),merge(f)]. given #425 (T,wt=15): 4885 p(m,b) | p(k,m) | p(k,b) | p(f(g(m)),g(k)). [para(4170(b,1),4848(c,1,1,1)),merge(d),merge(f)]. given #426 (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 #427 (F,wt=15): 4886 p(m,b) | p(k,m) | p(k,b) | p(f(g(k)),g(m)). [para(4170(b,1),4848(c,2,1)),merge(d),merge(f)]. given #428 (F,wt=16): 3422 p(k,b) | p(m,b) | g(k) = m | p(g(k),f(g(k))). [resolve(3410,b,12,b),flip(c)]. given #429 (T,wt=15): 4940 p(k,b) | p(m,b) | p(g(k),f(g(k))) | p(k,m). [para(3422(c,1),2730(b,2)),merge(d),merge(f)]. given #430 (T,wt=15): 4979 p(m,b) | p(k,m) | p(k,b) | p(g(m),f(g(k))). [para(4170(b,1),4940(c,1,1)),merge(d),merge(f)]. given #431 (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 #432 (F,wt=15): 4980 p(m,b) | p(k,m) | p(k,b) | p(g(k),f(g(m))). [para(4170(b,1),4940(c,2,1,1)),merge(d),merge(f)]. given #433 (F,wt=16): 3472 k = b | p(m,m) | p(x,b) | p(x,g(x)) | p(m,x). [para(29(b,1),3067(a,2))]. given #434 (T,wt=16): 4251 p(m,b) | k = m | p(x,b) | p(x,g(x)) | k != x. [para(4248(c,1),37(e,1)),flip(e),merge(f),unit_del(e,27)]. given #435 (T,wt=16): 4252 p(m,b) | k = m | p(x,b) | p(g(x),x) | k != x. [para(4248(c,1),42(e,1)),flip(e),merge(f),unit_del(e,27)]. given #436 (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 #437 (F,wt=16): 4335 p(m,b) | p(g(m),j) | j = x | p(x,j) | m != x. [para(4333(b,1),33(c,1))]. given #438 (F,wt=16): 4419 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | j = x. [resolve(1848,c,33,c),merge(f)]. given #439 (T,wt=16): 4439 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | p(b,x). [factor(4424,a,e),merge(e),merge(g)]. given #440 (T,wt=13): 5118 p(j,b) | p(j,g(j)) | p(b,m) | p(j,j). [factor(5100,f,g),merge(c),merge(d)]. given #441 (A,wt=18): 289 p(m,k) | p(m,j) | p(j,k) | j = x | -p(x,k) | k = x. [para(114(c,1),31(b,2))]. given #442 (F,wt=16): 4440 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | p(m,x). [factor(4425,a,f),merge(f),merge(g)]. given #443 (F,wt=16): 4483 p(x,b) | p(x,g(x)) | p(x,m) | p(x,j) | p(b,b). [factor(4469,a,c),merge(c)]. given #444 (T,wt=13): 5223 p(x,b) | p(x,g(x)) | p(x,m) | p(x,j). [factor(5218,a,c),merge(c)]. given #445 (T,wt=16): 4660 p(k,j) | p(j,k) | p(j,b) | p(m,g(j)) | j = b. [para(2252(a,1),65(a,2)),merge(f)]. given #446 (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),122(d,1))]. given #447 (F,wt=16): 4674 p(k,j) | p(j,k) | p(j,b) | p(j,g(m)) | j = b. [para(2253(a,1),65(a,2)),merge(f)]. given #448 (F,wt=16): 4730 p(k,j) | p(j,k) | p(j,b) | p(m,g(k)) | j = b. [para(2329(a,1),65(a,2)),merge(f)]. given #449 (T,wt=16): 5046 p(x,b) | p(x,g(x)) | k = x | p(m,m) | p(m,x). [factor(5025,a,e),merge(e)]. given #450 (T,wt=13): 5286 p(x,b) | p(x,g(x)) | p(m,m) | p(m,x). [factor(5282,a,e),merge(e),merge(f)]. given #451 (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),122(d,1))]. given #452 (F,wt=16): 5116 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j) | p(x,x). [factor(5100,a,c),merge(c)]. given #453 (F,wt=14): 5337 p(j,b) | p(j,g(j)) | p(j,j) | p(f(b),b). [factor(5325,c,d)]. given #454 (T,wt=14): 5338 p(j,b) | p(j,g(j)) | p(j,j) | p(b,f(b)). [factor(5326,c,d)]. given #455 (T,wt=14): 5369 p(j,b) | p(j,g(j)) | p(j,j) | p(f(j),b). [factor(5357,a,c),merge(c)]. given #456 (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),122(d,1))]. given #457 (F,wt=14): 5370 p(j,b) | p(j,g(j)) | p(j,j) | p(f(b),j). [factor(5358,a,c),merge(c)]. given #458 (F,wt=14): 5454 p(j,b) | p(j,g(j)) | p(j,j) | p(f(j),j). [factor(5446,a,c),merge(c)]. given #459 (T,wt=16): 5140 p(k,j) | p(j,b) | p(j,g(k)) | p(b,m) | p(j,j). [para(65(a,1),5118(b,2,1))]. given #460 (T,wt=16): 5303 p(j,b) | p(j,g(j)) | p(m,m) | j = m | k = m. [resolve(5286,d,31,b)]. given #461 (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),122(d,1))]. given #462 (F,wt=13): 5529 p(j,b) | p(j,g(j)) | p(m,m) | k = m. [resolve(5303,d,59,c(flip)),merge(e),merge(f)]. given #463 (F,wt=13): 5542 p(j,b) | p(j,g(j)) | p(m,m) | p(k,j). [para(5529(d,1),133(c,1)),merge(d),merge(e),unit_del(d,27)]. given #464 (T,wt=13): 5563 p(k,j) | p(j,b) | p(j,g(k)) | p(m,m). [para(65(a,1),5542(b,2,1)),merge(e)]. given #465 (T,wt=16): 5566 k = b | p(k,j) | p(j,b) | p(m,g(j)) | p(m,m). [para(76(b,1),5542(b,1)),merge(f)]. given #466 (A,wt=18): 305 p(b,k) | j = m | p(j,m) | k = m | j = k | -p(j,k). [resolve(304,a,2,f),flip(b),flip(d),flip(e)]. given #467 (F,wt=16): 5567 k = b | p(k,j) | p(j,b) | p(j,g(m)) | p(m,m). [para(76(b,1),5542(b,2,1)),merge(f)]. given #468 (F,wt=16): 5611 k = b | p(k,j) | p(j,b) | p(m,g(k)) | p(m,m). [para(76(b,1),5563(c,1)),merge(c)]. given #469 (T,wt=16): 5633 p(k,j) | p(j,b) | p(m,g(j)) | p(m,m) | j = b. [para(5566(a,1),65(a,2)),merge(f)]. given #470 (T,wt=16): 5658 p(k,j) | p(j,b) | p(j,g(m)) | p(m,m) | j = b. [para(5567(a,1),65(a,2)),merge(f)]. given #471 (A,wt=18): 306 p(b,k) | k = m | p(k,m) | j = m | j = k | -p(j,k). [resolve(304,a,2,e),flip(b),flip(d)]. given #472 (F,wt=16): 5677 p(k,j) | p(j,b) | p(m,g(k)) | p(m,m) | j = b. [para(5611(a,1),65(a,2)),merge(f)]. given #473 (F,wt=17): 400 p(j,b) | p(b,k) | p(m,j) | g(j) = j | g(j) = k. [resolve(101,b,31,b),flip(d),flip(e)]. given #474 (T,wt=16): 5736 p(j,b) | p(b,k) | p(m,j) | g(j) = k | j = b. [resolve(400,d,18,c),flip(e),merge(f)]. given #475 (T,wt=15): 5745 p(j,b) | p(b,k) | p(m,j) | j = b | k != b. [para(5736(d,1),16(c,1)),flip(e),merge(e),merge(f)]. given #476 (A,wt=19): 312 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,k) | p(x,j). [para(34(c,1),307(b,1))]. given #477 (F,wt=12): 5771 p(j,b) | p(b,k) | p(m,j) | j = b. [resolve(5745,e,54,a),merge(e)]. given #478 (F,wt=12): 5797 p(j,b) | p(b,k) | p(m,j) | p(k,b). [para(5771(d,1),304(a,2)),merge(e)]. given #479 (T,wt=12): 5798 p(j,b) | p(b,k) | p(m,j) | p(b,b). [para(5771(d,1),307(b,2)),merge(d)]. given #480 (T,wt=13): 5800 p(j,b) | p(b,k) | p(m,j) | p(b,g(j)). [para(5771(d,1),1723(b,1)),merge(d),merge(f)]. given #481 (A,wt=19): 313 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,k) | p(x,j). [para(39(c,1),307(b,1))]. given #482 (F,wt=13): 5801 p(j,b) | p(b,k) | p(m,j) | p(j,g(b)). [para(5771(d,1),1723(b,2,1)),merge(d),merge(f)]. given #483 (F,wt=13): 5872 p(j,b) | p(b,k) | p(m,j) | p(b,g(b)). [para(5771(d,1),5801(d,1)),merge(d),merge(e),merge(f)]. given #484 (T,wt=15): 5791 p(j,b) | p(b,k) | p(m,j) | j = k | p(j,k). [resolve(5771,d,26,b(flip)),flip(d)]. given #485 (T,wt=12): 5885 p(j,b) | p(b,k) | p(m,j) | p(j,k). [para(5791(d,1),307(b,2)),merge(e),merge(f)]. given #486 (A,wt=20): 314 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 #487 (F,wt=9): 5888 p(b,k) | p(j,b) | p(m,j). [para(54(a,1),5885(d,2)),merge(c),merge(e)]. given #488 (F,wt=15): 5911 p(b,k) | p(m,j) | p(b,m) | j = m | j = b. [resolve(5888,b,309,e),merge(c)]. given #489 (T,wt=12): 5924 p(b,k) | p(m,j) | p(b,m) | j = b. [para(5911(d,1),307(b,2)),merge(e),merge(f)]. given #490 (T,wt=12): 5935 p(b,k) | p(m,j) | p(b,m) | p(k,b). [para(5924(d,1),304(a,2)),merge(e)]. given #491 (A,wt=23): 315 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 #492 (F,wt=12): 5936 p(b,k) | p(m,j) | p(b,m) | p(b,b). [para(5924(d,1),307(b,2)),merge(d)]. given #493 (F,wt=15): 5912 p(b,k) | p(m,j) | j = m | p(j,m) | j = b. [resolve(5888,b,308,e),merge(c)]. given #494 (T,wt=15): 5913 p(b,k) | p(m,j) | j = k | j = m | j = b. [resolve(5888,b,71,e),flip(d),flip(e),flip(f),merge(c)]. given #495 (T,wt=12): 5958 p(b,k) | p(m,j) | j = b | j = m. [para(54(a,1),5913(c,2)),merge(b),merge(f)]. given #496 (A,wt=20): 316 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 #497 (F,wt=12): 5961 p(b,k) | p(m,j) | j = b | p(k,m). [para(5958(d,1),304(a,2)),merge(e)]. given #498 (F,wt=12): 5998 p(b,k) | p(m,j) | p(k,m) | p(k,b). [para(5961(c,1),304(a,2)),merge(e)]. given #499 (T,wt=12): 5999 p(b,k) | p(m,j) | p(k,m) | p(b,b). [para(5961(c,1),307(b,2)),merge(d)]. given #500 (T,wt=15): 5929 p(b,k) | p(m,j) | p(b,m) | j = k | p(j,k). [resolve(5924,d,26,b(flip)),flip(d)]. given #501 (A,wt=23): 317 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 #502 (F,wt=12): 6034 p(b,k) | p(m,j) | p(b,m) | p(j,k). [para(5929(d,1),307(b,2)),merge(e),merge(f)]. given #503 (F,wt=9): 6043 p(b,k) | p(m,j) | p(b,m). [para(5924(d,1),6034(d,1)),merge(d),merge(e),merge(f),merge(g)]. given #504 (T,wt=12): 6046 p(b,k) | p(b,m) | j = m | k = m. [resolve(6043,b,31,b)]. given #505 (T,wt=9): 6053 p(b,k) | p(b,m) | k = m. [para(6046(c,1),307(b,2)),merge(d),merge(e)]. given #506 (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 #507 (F,wt=6): 6060 p(b,k) | p(b,m). [para(6053(c,1),54(a,1)),merge(d),unit_del(c,27)]. given #508 (F,wt=6): 6084 k = b | p(b,m). [para(29(b,1),6060(a,2)),merge(c)]. given #509 (T,wt=6): 6085 p(m,k) | p(b,m). [para(51(a,1),6060(a,2)),merge(c)]. given #510 (T,wt=6): 6143 p(b,m) | p(m,b). [para(6084(a,1),2720(a,2)),merge(c)]. given #511 (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 #512 (F,wt=6): 6154 p(b,m) | p(b,b). [para(6084(a,1),6060(a,2)),merge(c)]. given #513 (F,wt=7): 6191 p(b,b) | p(f(b),b). [resolve(6154,a,14,b),unit_del(b,27)]. given #514 (T,wt=7): 6192 p(b,b) | p(b,f(b)). [resolve(6154,a,12,b),unit_del(b,27)]. given #515 (T,wt=9): 6129 p(b,m) | j = b | p(b,j). [resolve(6084,a,33,c)]. given #516 (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 #517 (F,wt=9): 6134 p(b,m) | j = b | p(k,j). [para(6084(a,1),65(a,2))]. given #518 (F,wt=12): 6133 p(b,m) | j = x | p(x,j) | b != x. [para(6084(a,1),33(c,1))]. given #519 (T,wt=12): 6157 p(b,m) | p(k,j) | j = m | k = m. [resolve(6085,a,77,c)]. given #520 (T,wt=9): 6290 p(b,m) | p(k,j) | k = m. [para(6157(c,1),65(a,1)),flip(d),merge(d),merge(e)]. given #521 (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),77(c,2))]. given #522 (F,wt=6): 6313 p(b,m) | p(k,j). [para(6290(c,1),6060(a,2)),merge(c),merge(d)]. given #523 (F,wt=6): 6326 p(b,m) | p(b,j). [para(6084(a,1),6313(b,1)),merge(b)]. given #524 (T,wt=12): 6185 p(b,b) | k = b | p(k,j) | j = b. [resolve(6154,a,122,d)]. given #525 (T,wt=9): 6339 p(b,b) | k = b | p(k,j). [para(6185(d,1),65(a,1)),flip(d),merge(d),merge(e)]. given #526 (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 #527 (F,wt=9): 6345 p(b,b) | p(k,j) | p(m,k). [para(6339(b,1),51(a,1)),flip(c),unit_del(c,27)]. given #528 (F,wt=9): 6346 p(b,b) | p(k,j) | j = b. [para(6339(b,1),65(a,2)),merge(d)]. given #529 (T,wt=9): 6389 p(m,k) | p(b,b) | p(m,j). [para(51(a,1),6345(b,1)),merge(d)]. given #530 (T,wt=10): 6398 p(b,b) | p(k,j) | p(k,g(j)). [para(6346(c,1),2540(b,1)),merge(c),merge(d)]. given #531 (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 #532 (F,wt=10): 6400 p(b,b) | p(k,j) | p(k,g(k)). [para(6346(c,1),3971(b,1)),merge(c),merge(d)]. given #533 (F,wt=10): 6443 p(b,b) | p(k,j) | p(b,g(j)). [para(6339(b,1),6398(c,1)),merge(c),merge(d)]. given #534 (T,wt=10): 6444 p(b,b) | p(k,j) | p(k,g(b)). [para(6346(c,1),6398(c,2,1)),merge(c),merge(d)]. given #535 (T,wt=10): 6459 p(b,b) | p(k,j) | p(b,g(k)). [para(6339(b,1),6400(c,1)),merge(c),merge(d)]. given #536 (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 #537 (F,wt=10): 6528 p(b,b) | p(k,j) | p(b,g(b)). [para(6339(b,1),6444(c,1)),merge(c),merge(d)]. given #538 (F,wt=12): 6187 p(b,b) | p(m,j) | k = b | j = b. [resolve(6154,a,113,d)]. given #539 (T,wt=9): 6608 p(b,b) | p(m,j) | k = b. [para(6187(d,1),62(a,1)),flip(d),merge(e),merge(f),unit_del(d,27)]. given #540 (T,wt=12): 6329 p(b,m) | j = m | j = b | -p(j,b). [resolve(6326,b,2,e),flip(d),merge(c),unit_del(b,27)]. given #541 (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),77(c,2))]. given #542 (F,wt=12): 6609 p(b,b) | p(m,j) | j = b | p(b,j). [resolve(6608,c,33,c)]. given #543 (F,wt=13): 6082 p(x,b) | p(x,g(x)) | p(x,k) | p(b,m). [para(20(a,1),6060(a,1))]. given #544 (T,wt=13): 6083 p(x,b) | p(g(x),x) | p(x,k) | p(b,m). [para(22(a,1),6060(a,1))]. given #545 (T,wt=13): 6122 p(j,b) | p(j,g(j)) | p(m,m) | p(b,m). [para(5529(d,1),6060(a,2)),merge(e)]. given #546 (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 #547 (F,wt=13): 6131 p(x,b) | p(x,g(x)) | k = x | p(b,m). [para(20(a,1),6084(a,2))]. given #548 (F,wt=13): 6132 p(x,b) | p(g(x),x) | k = x | p(b,m). [para(22(a,1),6084(a,2))]. given #549 (T,wt=13): 6161 p(x,b) | p(x,g(x)) | p(b,m) | p(m,x). [para(20(a,1),6143(b,2))]. given #550 (T,wt=13): 6162 p(x,b) | p(g(x),x) | p(b,m) | p(m,x). [para(22(a,1),6143(b,2))]. given #551 (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 #552 (F,wt=13): 6193 p(x,b) | p(x,g(x)) | p(x,m) | p(b,b). [para(20(a,1),6154(a,1))]. given #553 (F,wt=10): 6769 p(x,b) | p(x,g(x)) | p(x,m). [factor(6767,a,c),merge(c)]. given #554 (T,wt=13): 6194 p(x,b) | p(g(x),x) | p(x,m) | p(b,b). [para(22(a,1),6154(a,1))]. given #555 (T,wt=13): 6330 p(x,b) | p(x,g(x)) | p(b,m) | p(x,j). [para(20(a,1),6326(b,1))]. given #556 (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 #557 (F,wt=13): 6331 p(x,b) | p(g(x),x) | p(b,m) | p(x,j). [para(22(a,1),6326(b,1))]. given #558 (F,wt=13): 6623 p(b,b) | p(m,j) | p(b,j) | p(b,g(j)). [para(6608(c,1),6443(b,1)),merge(c)]. given #559 (T,wt=13): 6624 p(b,b) | p(m,j) | p(b,j) | p(b,g(k)). [para(6608(c,1),6459(b,1)),merge(c)]. given #560 (T,wt=13): 6625 p(b,b) | p(m,j) | p(b,j) | p(b,g(b)). [para(6608(c,1),6528(b,1)),merge(c)]. given #561 (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 #562 (F,wt=13): 6716 p(x,b) | p(x,g(x)) | p(b,m) | p(b,x). [para(6131(c,1),6060(a,2)),merge(e)]. given #563 (F,wt=13): 6719 p(x,b) | p(g(x),x) | p(b,m) | p(b,x). [para(6132(c,1),6060(a,2)),merge(e)]. given #564 (T,wt=13): 6934 p(x,b) | p(x,g(x)) | p(b,m) | p(x,x). [factor(6920,a,c),merge(c)]. given #565 (T,wt=14): 6210 p(x,b) | p(x,g(x)) | p(b,b) | p(f(x),b). [para(20(a,1),6191(b,1,1))]. given #566 (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 #567 (F,wt=14): 6211 p(x,b) | p(x,g(x)) | p(b,b) | p(f(b),x). [para(20(a,1),6191(b,2))]. given #568 (F,wt=14): 6212 p(x,b) | p(g(x),x) | p(b,b) | p(f(x),b). [para(22(a,1),6191(b,1,1))]. given #569 (T,wt=14): 6213 p(x,b) | p(g(x),x) | p(b,b) | p(f(b),x). [para(22(a,1),6191(b,2))]. given #570 (T,wt=14): 6223 p(x,b) | p(x,g(x)) | p(b,b) | p(x,f(b)). [para(20(a,1),6192(b,1))]. given #571 (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 #572 (F,wt=11): 7086 p(x,b) | p(x,g(x)) | p(x,f(b)). [factor(7084,a,c),merge(c)]. given #573 (F,wt=14): 6224 p(x,b) | p(x,g(x)) | p(b,b) | p(b,f(x)). [para(20(a,1),6192(b,2,1))]. given #574 (T,wt=14): 6225 p(x,b) | p(g(x),x) | p(b,b) | p(x,f(b)). [para(22(a,1),6192(b,1))]. given #575 (T,wt=14): 6226 p(x,b) | p(g(x),x) | p(b,b) | p(b,f(x)). [para(22(a,1),6192(b,2,1))]. given #576 (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 #577 (F,wt=14): 6659 p(x,b) | p(x,g(x)) | p(x,k) | p(f(b),b). [resolve(6082,d,14,b),unit_del(d,27)]. given #578 (F,wt=14): 6660 p(x,b) | p(x,g(x)) | p(x,k) | p(b,f(b)). [resolve(6082,d,12,b),unit_del(d,27)]. given #579 (T,wt=14): 6668 p(f(b),b) | p(f(b),g(f(b))) | p(f(b),k). [factor(6658,a,d),merge(d)]. given #580 (T,wt=14): 6813 p(x,b) | p(x,g(x)) | p(x,j) | p(f(b),b). [resolve(6330,c,14,b),unit_del(d,27)]. given #581 (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 #582 (F,wt=14): 6814 p(x,b) | p(x,g(x)) | p(x,j) | p(b,f(b)). [resolve(6330,c,12,b),unit_del(d,27)]. given #583 (F,wt=14): 6821 p(f(b),b) | p(f(b),g(f(b))) | p(f(b),j). [factor(6812,a,d),merge(d)]. given #584 (T,wt=14): 6918 p(x,b) | p(x,g(x)) | p(b,x) | p(f(b),b). [resolve(6716,c,14,b),unit_del(d,27)]. given #585 (T,wt=14): 6919 p(x,b) | p(x,g(x)) | p(b,x) | p(b,f(b)). [resolve(6716,c,12,b),unit_del(d,27)]. given #586 (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 #587 (F,wt=14): 6933 p(f(b),b) | p(f(b),g(f(b))) | p(b,f(b)). [factor(6917,a,d),merge(d)]. given #588 (F,wt=14): 6970 p(x,b) | p(x,g(x)) | p(x,x) | p(f(b),b). [resolve(6934,c,14,b),unit_del(d,27)]. given #589 (T,wt=14): 6971 p(x,b) | p(x,g(x)) | p(x,x) | p(b,f(b)). [resolve(6934,c,12,b),unit_del(d,27)]. given #590 (T,wt=14): 7004 p(x,b) | p(x,g(x)) | p(b,b) | p(f(x),x). [factor(6995,a,c),merge(c)]. given #591 (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 #592 (F,wt=14): 7124 p(x,b) | p(x,g(x)) | p(b,b) | p(x,f(x)). [factor(7117,a,c),merge(c)]. given #593 (F,wt=11): 7702 p(x,b) | p(x,g(x)) | p(x,f(x)). [factor(7698,a,c),merge(c)]. given #594 (T,wt=14): 7215 p(x,b) | p(x,g(x)) | p(x,k) | p(f(x),b). [factor(7176,a,c),merge(c)]. given #595 (T,wt=14): 7217 p(x,b) | p(x,g(x)) | p(x,k) | p(f(b),x). [factor(7177,a,c),merge(c)]. given #596 (A,wt=19): 373 p(f(k),b) | p(f(k),g(f(k))) | p(b,k) | k = m | -p(k,m). [resolve(72,c,10,c(flip)),flip(d)]. given #597 (F,wt=14): 7256 p(x,b) | p(x,g(x)) | p(x,k) | p(b,f(x)). [factor(7242,a,c),merge(c)]. given #598 (F,wt=14): 7343 p(x,b) | p(x,g(x)) | p(x,j) | p(f(x),b). [factor(7310,a,c),merge(c)]. given #599 (T,wt=14): 7345 p(x,b) | p(x,g(x)) | p(x,j) | p(f(b),x). [factor(7311,a,c),merge(c)]. given #600 (T,wt=14): 7396 p(x,b) | p(x,g(x)) | p(x,j) | p(b,f(x)). [factor(7382,a,c),merge(c)]. given #601 (A,wt=22): 374 p(x,b) | p(x,g(x)) | p(b,k) | k = y | m = y | b = y | -p(y,x). [para(72(c,1),6(d,2))]. given #602 (F,wt=14): 7495 p(x,b) | p(x,g(x)) | p(b,x) | p(f(x),b). [factor(7452,a,c),merge(c)]. given #603 (F,wt=14): 7497 p(x,b) | p(x,g(x)) | p(b,x) | p(f(b),x). [factor(7453,a,c),merge(c)]. given #604 (T,wt=14): 7552 p(x,b) | p(x,g(x)) | p(b,x) | p(b,f(x)). [factor(7533,a,c),merge(c)]. given #605 (T,wt=14): 7640 p(x,b) | p(x,g(x)) | p(x,x) | p(f(x),b). [factor(7608,a,c),merge(c)]. given #606 (A,wt=19): 375 p(f(k),b) | p(g(f(k)),f(k)) | p(b,k) | k = m | -p(k,m). [resolve(73,c,10,c(flip)),flip(d)]. given #607 (F,wt=14): 7642 p(x,b) | p(x,g(x)) | p(x,x) | p(f(b),x). [factor(7609,a,c),merge(c)]. given #608 (F,wt=14): 7676 p(x,b) | p(x,g(x)) | p(x,x) | p(b,f(x)). [factor(7663,a,c),merge(c)]. given #609 (T,wt=14): 7735 p(x,b) | p(x,g(x)) | p(x,k) | p(f(x),x). [factor(7723,a,c),merge(c)]. given #610 (T,wt=14): 7818 p(x,b) | p(x,g(x)) | p(x,j) | p(f(x),x). [factor(7812,a,c),merge(c)]. given #611 (A,wt=22): 376 p(x,b) | p(g(x),x) | p(b,k) | k = y | m = y | b = y | -p(y,x). [para(73(c,1),6(d,2))]. given #612 (F,wt=14): 7896 p(x,b) | p(x,g(x)) | p(b,x) | p(f(x),x). [factor(7886,a,c),merge(c)]. given #613 (F,wt=14): 7958 p(x,b) | p(x,g(x)) | p(x,x) | p(f(x),x). [factor(7952,a,c),merge(c)]. given #614 (T,wt=15): 5959 p(b,k) | p(m,j) | j = b | j = k | p(j,k). [resolve(5958,d,24,b(flip)),flip(d)]. given #615 (T,wt=12): 8029 p(b,k) | p(m,j) | j = b | p(j,k). [para(54(a,1),5959(d,2)),merge(b),merge(e)]. given #616 (A,wt=40): 377 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(82,b,41,h),flip(e),flip(g),flip(h)]. given #617 (F,wt=12): 8034 p(b,k) | p(m,j) | p(j,k) | j = k. [resolve(8029,c,26,b(flip)),flip(d),merge(e)]. given #618 (F,wt=9): 8053 p(b,k) | p(m,j) | p(j,k). [para(8034(d,1),307(b,2)),merge(d),merge(e)]. given #619 (T,wt=9): 8056 p(b,k) | p(m,j) | p(k,m). [para(5961(c,1),8053(c,1)),merge(d),merge(e),merge(f)]. given #620 (T,wt=13): 8059 p(b,k) | p(m,j) | k = m | p(f(k),k). [resolve(8056,c,14,b),flip(c)]. given #621 (A,wt=39): 378 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(82,b,41,g),flip(e),flip(g)]. given #622 (F,wt=10): 8077 p(b,k) | p(m,j) | p(f(k),k). [para(8059(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #623 (F,wt=10): 8093 p(b,k) | p(m,j) | p(f(b),k). [para(54(a,1),8077(c,1,1)),merge(b)]. given #624 (T,wt=10): 8094 p(b,k) | p(m,j) | p(f(k),b). [para(54(a,1),8077(c,2)),merge(b)]. given #625 (T,wt=10): 8117 p(b,k) | p(m,j) | p(f(b),b). [para(54(a,1),8093(c,2)),merge(b)]. given #626 (A,wt=40): 380 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(82,b,36,h),flip(e),flip(g),flip(h)]. given #627 (F,wt=13): 8060 p(b,k) | p(m,j) | k = m | p(k,f(k)). [resolve(8056,c,12,b),flip(c)]. given #628 (F,wt=10): 8165 p(b,k) | p(m,j) | p(k,f(k)). [para(8060(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #629 (T,wt=10): 8167 p(b,k) | p(m,j) | p(b,f(k)). [para(54(a,1),8165(c,1)),merge(b)]. given #630 (T,wt=10): 8168 p(b,k) | p(m,j) | p(k,f(b)). [para(54(a,1),8165(c,2,1)),merge(b)]. given #631 (A,wt=39): 381 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(82,b,36,g),flip(e),flip(g)]. given #632 (F,wt=10): 8190 p(b,k) | p(m,j) | p(b,f(b)). [para(54(a,1),8168(c,1)),merge(b)]. given #633 (F,wt=13): 8188 p(b,k) | p(b,f(k)) | j = m | k = m. [resolve(8167,b,31,b)]. given #634 (T,wt=13): 8211 p(b,k) | p(b,f(b)) | j = m | k = m. [resolve(8190,b,31,b)]. given #635 (T,wt=13): 8217 p(b,k) | p(b,f(k)) | k = m | p(k,m). [para(8188(c,1),304(a,2)),merge(e)]. given #636 (A,wt=33): 383 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(82,b,4,f),flip(c),flip(e),flip(f)]. given #637 (F,wt=10): 8235 p(b,k) | p(b,f(k)) | p(k,m). [para(8217(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #638 (F,wt=13): 8220 p(b,k) | p(b,f(k)) | k = m | p(m,m). [para(8188(c,1),8167(b,2)),merge(d),merge(f)]. given #639 (T,wt=10): 8266 p(b,k) | p(b,f(k)) | p(m,m). [para(8220(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #640 (T,wt=13): 8226 p(b,k) | p(b,f(b)) | k = m | p(k,m). [para(8211(c,1),304(a,2)),merge(e)]. given #641 (A,wt=33): 384 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(82,b,2,f),flip(c),flip(e),flip(f)]. given #642 (F,wt=10): 8272 p(b,k) | p(b,f(b)) | p(k,m). [para(8226(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #643 (F,wt=13): 8229 p(b,k) | p(b,f(b)) | k = m | p(m,m). [para(8211(c,1),8190(b,2)),merge(d),merge(f)]. given #644 (T,wt=10): 8297 p(b,k) | p(b,f(b)) | p(m,m). [para(8229(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #645 (T,wt=14): 8253 p(b,k) | p(b,f(k)) | k = m | p(f(k),k). [resolve(8235,c,14,b),flip(c)]. given #646 (A,wt=35): 385 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(100,b,41,h),flip(f),flip(i)]. given #647 (F,wt=11): 8303 p(b,k) | p(b,f(k)) | p(f(k),k). [para(8253(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #648 (F,wt=11): 8330 p(b,k) | p(b,f(k)) | p(f(b),k). [para(54(a,1),8303(c,1,1)),merge(b)]. given #649 (T,wt=11): 8331 p(b,k) | p(b,f(k)) | p(f(k),b). [para(54(a,1),8303(c,2)),merge(b)]. given #650 (T,wt=11): 8354 p(b,k) | p(b,f(k)) | p(f(b),b). [para(54(a,1),8330(c,2)),merge(b)]. given #651 (A,wt=34): 386 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(100,b,41,g),flip(h)]. given #652 (F,wt=14): 8254 p(b,k) | p(b,f(k)) | k = m | p(k,f(k)). [resolve(8235,c,12,b),flip(c)]. given #653 (F,wt=11): 8399 p(b,k) | p(b,f(k)) | p(k,f(k)). [para(8254(c,1),54(a,1)),merge(e),unit_del(d,27)]. given #654 (T,wt=7): 8401 p(b,k) | p(b,f(k)). [para(54(a,1),8399(c,1)),merge(b),merge(d)]. given #655 (T,wt=7): 8405 p(b,k) | p(b,f(b)). [para(54(a,1),8401(b,2,1)),merge(b)]. given #656 (A,wt=35): 387 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(100,b,36,h),flip(f),flip(i)]. given #657 (F,wt=14): 8403 p(x,b) | p(x,g(x)) | p(b,k) | p(x,f(k)). [para(20(a,1),8401(b,1))]. given #658 (F,wt=14): 8404 p(x,b) | p(g(x),x) | p(b,k) | p(x,f(k)). [para(22(a,1),8401(b,1))]. given #659 (T,wt=14): 8409 p(x,b) | p(x,g(x)) | p(b,k) | p(b,f(x)). [para(72(c,1),8401(b,2,1)),merge(d)]. given #660 (T,wt=14): 8410 p(x,b) | p(g(x),x) | p(b,k) | p(b,f(x)). [para(73(c,1),8401(b,2,1)),merge(d)]. given #661 (A,wt=34): 388 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(100,b,36,g),flip(h)]. given #662 (F,wt=14): 8418 p(x,b) | p(g(x),x) | p(b,k) | p(x,f(b)). [para(22(a,1),8405(b,1))]. given #663 (F,wt=14): 8477 p(x,b) | p(x,g(x)) | p(x,k) | p(x,f(k)). [factor(8447,a,c),merge(c)]. given #664 (T,wt=14): 8482 p(b,b) | p(m,j) | p(b,g(b)) | p(b,f(k)). [factor(8474,a,c)]. given #665 (T,wt=15): 6130 p(b,m) | k = x | m = x | b = x | -p(x,b). [para(6084(a,1),6(d,2))]. given #666 (A,wt=28): 389 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(100,b,4,f),flip(d),flip(g)]. given #667 (F,wt=15): 6160 p(b,m) | b = x | m = x | -p(m,x) | -p(x,m). [resolve(6143,b,4,b),flip(b),flip(d),unit_del(b,27)]. given #668 (F,wt=15): 6344 p(b,b) | p(k,j) | j = x | p(x,j) | b != x. [para(6339(b,1),33(c,1))]. given #669 (T,wt=15): 6349 p(b,b) | p(k,j) | j = x | -p(x,b) | k = x. [para(6339(b,1),77(c,2)),merge(c)]. given #670 (T,wt=14): 8613 p(b,b) | p(k,j) | f(b) = j | f(b) = k. [resolve(6349,d,6191,b),flip(c),flip(d),merge(e)]. given #671 (A,wt=28): 390 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(100,b,2,f),flip(d),flip(g)]. given #672 (F,wt=10): 8626 p(k,j) | p(b,b) | f(b) = k. [para(65(a,1),8613(c,2)),merge(c),merge(e)]. given #673 (F,wt=9): 8669 p(k,j) | p(b,b) | p(k,b). [para(8626(c,1),6191(b,1)),merge(c)]. given #674 (T,wt=10): 8670 p(b,b) | p(k,j) | f(b) = b. [para(6339(b,1),8626(c,2)),merge(c),merge(d)]. given #675 (T,wt=6): 8723 p(b,b) | p(k,j). [para(8670(c,1),6191(b,1)),merge(c),merge(d)]. given #676 (A,wt=20): 394 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 #677 (F,wt=9): 8753 p(b,b) | p(m,j) | p(b,j). [para(6608(c,1),8723(b,1)),merge(c)]. given #678 (F,wt=12): 8786 p(b,b) | p(b,j) | j = m | k = m. [resolve(8753,b,31,b)]. given #679 (T,wt=12): 8804 p(b,b) | p(b,j) | k = m | p(k,m). [para(8786(c,1),8723(b,2)),merge(d)]. given #680 (T,wt=12): 8805 p(b,b) | p(b,j) | k = m | p(m,m). [para(8786(c,1),8753(b,2)),merge(d),merge(f)]. given #681 (A,wt=23): 395 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 #682 (F,wt=13): 8688 p(k,b) | p(k,g(k)) | p(b,j) | p(b,b). [para(137(c,1),8669(a,1)),merge(e)]. given #683 (F,wt=13): 8689 p(k,b) | p(g(k),k) | p(b,j) | p(b,b). [para(143(c,1),8669(a,1)),merge(e)]. given #684 (T,wt=15): 6613 p(b,b) | p(m,j) | j = x | p(x,j) | b != x. [para(6608(c,1),33(c,1))]. given #685 (T,wt=15): 8793 p(b,b) | p(b,j) | k = m | j = k | p(j,k). [resolve(8786,c,24,b(flip)),flip(d)]. given #686 (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(101,b,2,f),flip(f)]. given #687 (F,wt=12): 8901 p(b,b) | p(b,j) | k = m | p(j,k). [para(8793(d,1),8786(c,1)),merge(e),merge(f),merge(g),merge(h)]. given #688 (F,wt=16): 5915 p(x,b) | p(x,g(x)) | p(b,k) | p(j,x) | p(m,j). [para(20(a,1),5888(b,2))]. given #689 (T,wt=16): 5916 p(x,b) | p(g(x),x) | p(b,k) | p(j,x) | p(m,j). [para(22(a,1),5888(b,2))]. given #690 (T,wt=16): 6611 p(x,b) | p(x,g(x)) | p(b,b) | p(m,j) | k = x. [para(20(a,1),6608(c,2))]. given #691 (A,wt=35): 406 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(405,b,41,h),flip(d),flip(f)]. given #692 (F,wt=13): 8960 p(j,b) | p(j,g(j)) | p(b,b) | p(m,j). [factor(8959,d,e)]. given #693 (F,wt=16): 6612 p(x,b) | p(g(x),x) | p(b,b) | p(m,j) | k = x. [para(22(a,1),6608(c,2))]. given #694 (T,wt=16): 6616 p(b,b) | p(m,j) | p(x,b) | p(x,g(x)) | p(x,j). [para(6608(c,1),310(c,2)),merge(e)]. given #695 (T,wt=16): 6731 p(j,b) | p(j,g(j)) | p(b,m) | j = m | k = m. [resolve(6161,d,31,b)]. given #696 (A,wt=36): 407 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(405,b,41,g),flip(d),flip(f),flip(g)]. given #697 (F,wt=13): 9041 p(j,b) | p(j,g(j)) | p(b,m) | k = m. [resolve(6731,d,59,c(flip)),merge(e),merge(f)]. given #698 (F,wt=10): 9051 p(j,b) | p(j,g(j)) | p(b,m). [para(9041(d,1),6060(a,2)),merge(d),merge(e)]. given #699 (T,wt=16): 8062 p(x,b) | p(g(x),x) | p(b,k) | p(m,j) | p(x,m). [para(73(c,1),8056(c,1)),merge(d)]. given #700 (T,wt=16): 8698 p(j,b) | p(g(j),j) | p(m,j) | p(k,b) | p(b,b). [para(791(d,1),8669(a,2)),merge(f)]. given #701 (A,wt=35): 408 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(405,b,36,h),flip(d),flip(f)]. given #702 (F,wt=16): 8740 p(x,k) | p(x,b) | p(g(x),x) | p(b,b) | p(x,j). [para(52(a,1),8723(b,1))]. given #703 (F,wt=16): 8745 p(j,b) | p(g(j),j) | p(m,j) | p(b,b) | p(k,k). [para(531(d,1),8723(b,2))]. given #704 (T,wt=16): 8746 p(x,k) | p(x,b) | p(g(x),x) | p(b,b) | p(b,j). [para(1538(d,1),8723(b,1))]. given #705 (T,wt=16): 8747 p(x,k) | p(x,b) | p(x,g(x)) | p(b,b) | p(b,j). [para(1605(d,1),8723(b,1))]. given #706 (A,wt=36): 409 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(405,b,36,g),flip(d),flip(f),flip(g)]. given #707 (F,wt=16): 8791 p(b,b) | p(b,j) | k = m | p(j,b) | p(g(j),j). [resolve(8786,c,60,c(flip))]. given #708 (F,wt=16): 8792 p(b,b) | p(b,j) | k = m | p(j,b) | p(j,g(j)). [resolve(8786,c,59,c(flip))]. given #709 (T,wt=16): 8830 k = b | p(k,b) | p(m,g(k)) | p(b,j) | p(b,b). [para(29(b,1),8688(b,1))]. given #710 (T,wt=13): 9199 p(k,b) | p(m,g(k)) | p(b,j) | p(b,b). [para(8830(a,1),8723(b,1)),merge(e),merge(f)]. given #711 (A,wt=28): 410 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(405,b,4,f),flip(b),flip(d)]. given #712 (F,wt=16): 8831 k = b | p(k,b) | p(k,g(m)) | p(b,j) | p(b,b). [para(29(b,1),8688(b,2,1))]. given #713 (F,wt=13): 9233 p(k,b) | p(k,g(m)) | p(b,j) | p(b,b). [para(8831(a,1),8723(b,1)),merge(e),merge(f)]. given #714 (T,wt=16): 8853 k = b | p(k,b) | p(g(m),k) | p(b,j) | p(b,b). [para(29(b,1),8689(b,1,1))]. given #715 (T,wt=13): 9271 p(k,b) | p(g(m),k) | p(b,j) | p(b,b). [para(8853(a,1),8723(b,1)),merge(e),merge(f)]. given #716 (A,wt=29): 411 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(405,b,4,e),flip(b),flip(d),flip(e)]. given #717 (F,wt=16): 8854 k = b | p(k,b) | p(g(k),m) | p(b,j) | p(b,b). [para(29(b,1),8689(b,2))]. given #718 (F,wt=13): 9315 p(k,b) | p(g(k),m) | p(b,j) | p(b,b). [para(8854(a,1),8723(b,1)),merge(e),merge(f)]. given #719 (T,wt=16): 8959 p(x,b) | p(x,g(x)) | p(b,b) | p(m,j) | p(m,x). [factor(8956,a,f),merge(f),merge(g)]. given #720 (T,wt=16): 8998 p(x,b) | p(g(x),x) | p(b,b) | p(m,j) | p(x,j). [para(6612(e,1),8723(b,1)),merge(e)]. given #721 (A,wt=29): 412 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(405,b,2,e),flip(b),flip(d),flip(e)]. given #722 (F,wt=16): 9248 k = b | p(k,b) | p(m,g(m)) | p(b,j) | p(b,b). [para(29(b,1),9233(b,1))]. given #723 (F,wt=13): 9403 p(k,b) | p(m,g(m)) | p(b,j) | p(b,b). [para(9248(a,1),8723(b,1)),merge(e),merge(f)]. given #724 (T,wt=16): 9283 k = b | p(k,b) | p(g(m),m) | p(b,j) | p(b,b). [para(29(b,1),9271(b,2))]. given #725 (T,wt=13): 9431 p(k,b) | p(g(m),m) | p(b,j) | p(b,b). [para(9283(a,1),8723(b,1)),merge(e),merge(f)]. given #726 (A,wt=32): 416 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 #727 (F,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 #728 (F,wt=13): 9457 p(k,j) | p(j,b) | p(m,k) | g(j) = k. [para(65(a,1),488(d,2)),merge(d),merge(f)]. given #729 (T,wt=9): 9475 p(k,j) | p(j,b) | p(m,k). [para(9457(d,1),2718(b,1)),merge(d),merge(e),merge(f),merge(g)]. given #730 (T,wt=16): 9477 p(x,b) | p(x,g(x)) | p(k,j) | p(j,x) | p(m,k). [para(20(a,1),9475(b,2))]. given #731 (A,wt=32): 417 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 #732 (F,wt=16): 9478 p(x,b) | p(g(x),x) | p(k,j) | p(j,x) | p(m,k). [para(22(a,1),9475(b,2))]. given #733 (F,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 #734 (T,wt=16): 9510 p(j,b) | p(m,k) | p(m,j) | g(j) = k | j = b. [resolve(514,d,18,c),flip(e),merge(f)]. given #735 (T,wt=15): 9521 p(j,b) | p(m,k) | p(m,j) | j = b | k != b. [para(9510(d,1),16(c,1)),flip(e),merge(e),merge(f)]. given #736 (A,wt=23): 418 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 #737 (F,wt=15): 9522 p(j,b) | p(m,k) | p(m,j) | j = b | j != k. [para(9510(d,1),18(c,1)),flip(e),flip(g),merge(e),merge(f)]. given #738 (F,wt=15): 9531 p(j,b) | p(m,k) | p(m,j) | j = b | p(k,m). [para(9510(d,1),519(d,1)),merge(e),merge(f),merge(g)]. given #739 (T,wt=12): 9564 p(j,b) | p(m,k) | p(m,j) | p(k,m). [para(9531(d,1),67(b,1)),flip(f),merge(e),merge(g),unit_del(e,27)]. given #740 (T,wt=15): 9534 p(j,b) | p(m,k) | p(m,j) | j = b | p(j,k). [para(9510(d,1),1624(c,2)),merge(f),merge(g),merge(h)]. given #741 (A,wt=23): 419 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 #742 (F,wt=12): 9577 p(j,b) | p(m,k) | p(m,j) | p(j,k). [para(9534(d,1),67(b,1)),flip(f),merge(e),merge(g),unit_del(e,27)]. given #743 (F,wt=9): 9597 p(m,k) | p(m,j) | p(j,b). [para(67(b,1),9577(d,1)),merge(d),merge(e),merge(f)]. given #744 (T,wt=16): 9599 p(x,b) | p(x,g(x)) | p(m,k) | p(m,j) | p(j,x). [para(20(a,1),9597(c,2))]. given #745 (T,wt=16): 9600 p(x,b) | p(g(x),x) | p(m,k) | p(m,j) | p(j,x). [para(22(a,1),9597(c,2))]. given #746 (A,wt=23): 420 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 #747 (F,wt=17): 588 p(j,b) | p(b,k) | p(j,j) | g(j) = j | g(j) = k. [resolve(311,b,31,b),flip(d),flip(e)]. given #748 (F,wt=13): 9641 p(j,b) | p(b,k) | p(j,j) | g(j) = k. [para(588(d,1),310(b,2)),merge(e),merge(f),merge(g),merge(h)]. given #749 (T,wt=12): 9655 p(j,b) | p(b,k) | p(j,j) | p(j,k). [para(9641(d,1),310(b,2)),merge(d),merge(f),merge(g)]. given #750 (T,wt=13): 9648 p(b,k) | p(j,b) | p(j,j) | g(j) = b. [para(54(a,1),9641(d,2)),merge(c)]. given #751 (A,wt=23): 421 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 #752 (F,wt=9): 9673 p(b,k) | p(j,b) | p(j,j). [para(9648(d,1),310(b,2)),merge(d),merge(e),merge(f),merge(g)]. given #753 (F,wt=17): 1584 p(j,k) | p(j,b) | p(m,k) | g(j) = j | g(j) = k. [resolve(1564,c,31,b),flip(d),flip(e)]. given #754 (T,wt=16): 9683 p(j,k) | p(j,b) | p(m,k) | g(j) = k | j = b. [resolve(1584,d,18,c),flip(e),merge(f)]. given #755 (T,wt=12): 9693 p(j,k) | p(j,b) | p(m,k) | j = b. [para(9683(d,1),1624(c,2)),merge(e),merge(f),merge(g),merge(h)]. given #756 (A,wt=29): 422 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 #757 (F,wt=12): 9698 p(j,k) | p(j,b) | p(m,k) | j = k. [resolve(9693,d,26,b(flip)),flip(d),merge(e)]. given #758 (F,wt=12): 9716 p(m,k) | p(j,k) | p(j,b) | j = m. [para(51(a,1),9698(d,2)),merge(d)]. given #759 (T,wt=9): 9726 p(m,k) | p(j,k) | p(j,b). [para(9716(d,1),9693(d,1)),merge(d),merge(e),merge(f),unit_del(d,27)]. given #760 (T,wt=9): 9738 p(m,k) | p(j,m) | p(j,b). [para(51(a,1),9726(b,2)),merge(b)]. given #761 (A,wt=29): 423 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 #762 (F,wt=13): 9763 p(m,k) | p(j,b) | j = m | p(f(j),j). [resolve(9738,b,14,b),flip(c)]. given #763 (F,wt=10): 9778 p(m,k) | p(j,b) | p(f(j),j). [para(9763(c,1),9726(b,1)),merge(d),merge(e),merge(f)]. given #764 (T,wt=13): 9764 p(m,k) | p(j,b) | j = m | p(j,f(j)). [resolve(9738,b,12,b),flip(c)]. given #765 (T,wt=10): 9812 p(m,k) | p(j,b) | p(j,f(j)). [para(9764(c,1),9726(b,1)),merge(d),merge(e),merge(f)]. given #766 (A,wt=29): 424 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 #767 (F,wt=14): 9791 p(m,k) | p(j,b) | f(j) = j | f(j) = k. [resolve(9778,c,31,b),flip(c),flip(d)]. given #768 (F,wt=13): 9842 p(m,k) | p(j,b) | f(j) = k | p(j,j). [para(9791(c,1),9778(c,1)),merge(d),merge(e)]. given #769 (T,wt=13): 9846 p(m,k) | p(j,b) | f(j) = m | p(j,j). [para(51(a,1),9842(c,2)),merge(b)]. given #770 (T,wt=15): 9735 p(m,k) | p(j,b) | j = k | j = m | j = b. [resolve(9726,b,6,d),flip(c),flip(d),flip(e)]. given #771 (A,wt=29): 425 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 #772 (F,wt=12): 9854 p(m,k) | p(j,b) | j = m | j = b. [para(51(a,1),9735(c,2)),merge(b),merge(e)]. given #773 (F,wt=9): 9862 p(m,k) | p(j,b) | j = b. [para(9854(c,1),9726(b,1)),merge(d),merge(e),merge(f)]. given #774 (T,wt=10): 9870 p(m,k) | p(j,b) | p(f(b),j). [para(9862(c,1),9778(c,1,1)),merge(c),merge(d)]. given #775 (T,wt=10): 9871 p(m,k) | p(j,b) | p(f(j),b). [para(9862(c,1),9778(c,2)),merge(c),merge(d)]. given #776 (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(415,b,41,h),flip(d),flip(f),flip(g)]. given #777 (F,wt=10): 9872 p(m,k) | p(j,b) | p(b,f(j)). [para(9862(c,1),9812(c,1)),merge(c),merge(d)]. given #778 (F,wt=10): 9873 p(m,k) | p(j,b) | p(j,f(b)). [para(9862(c,1),9812(c,2,1)),merge(c),merge(d)]. given #779 (T,wt=10): 9890 p(m,k) | p(j,b) | p(f(b),b). [para(9862(c,1),9870(c,2)),merge(c),merge(d)]. given #780 (T,wt=10): 9903 p(m,k) | p(j,b) | f(j) = k. [para(9791(c,1),9871(c,1)),merge(d),merge(e),merge(f)]. given #781 (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(415,b,41,d),flip(d),flip(f)]. given #782 (F,wt=10): 9943 p(m,k) | p(j,b) | p(b,f(b)). [para(9862(c,1),9873(c,1)),merge(c),merge(d)]. given #783 (F,wt=10): 9961 p(m,k) | p(j,b) | f(j) = m. [para(51(a,1),9903(c,2)),merge(b)]. given #784 (T,wt=10): 9962 p(m,k) | p(j,b) | f(b) = k. [para(9862(c,1),9903(c,1,1)),merge(c),merge(d)]. given #785 (T,wt=10): 10000 p(m,k) | p(j,b) | f(b) = m. [para(9862(c,1),9961(c,1,1)),merge(c),merge(d)]. given #786 (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(415,b,36,h),flip(d),flip(f),flip(g)]. given #787 (F,wt=9): 10009 p(m,k) | p(j,b) | -p(b,m). [resolve(10000,c,8,c),unit_del(c,27)]. given #788 (F,wt=9): 10039 p(m,k) | p(j,b) | p(b,b). [resolve(10009,c,6154,a)]. given #789 (T,wt=12): 9999 p(m,k) | p(j,b) | j = m | -p(j,m). [resolve(9961,c,8,c),flip(c)]. given #790 (T,wt=9): 10066 p(m,k) | p(j,b) | j = m. [resolve(9999,d,9738,b),merge(d),merge(e)]. given #791 (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(415,b,36,d),flip(d),flip(f)]. given #792 (F,wt=6): 10072 p(m,k) | p(j,b). [para(10066(c,1),9726(b,1)),merge(c),merge(d),merge(e)]. given #793 (F,wt=13): 10103 p(x,b) | p(x,g(x)) | p(m,k) | p(j,x). [para(20(a,1),10072(b,2))]. given #794 (T,wt=13): 10104 p(x,b) | p(g(x),x) | p(m,k) | p(j,x). [para(22(a,1),10072(b,2))]. given #795 (T,wt=15): 10102 p(m,k) | j = m | p(j,m) | j = b | -p(b,j). [resolve(10072,b,2,e),flip(b),flip(e),unit_del(d,27)]. given #796 (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(415,b,4,f),flip(b),flip(d),flip(e)]. given #797 (F,wt=17): 2070 p(f(b),b) | p(f(b),g(f(b))) | -p(f(f(f(f(b)))),m). [factor(2065,a,c),merge(c)]. given #798 (F,wt=17): 2076 p(f(b),b) | p(g(f(b)),f(b)) | -p(f(f(f(f(b)))),m). [factor(2072,a,c),merge(c)]. given #799 (T,wt=17): 2270 p(j,b) | p(g(j),j) | p(k,j) | p(j,k) | p(b,g(j)). [para(505(d,1),2235(c,1)),merge(e)]. given #800 (T,wt=17): 2271 p(j,b) | p(g(j),j) | p(k,j) | p(j,k) | p(j,g(b)). [para(505(d,1),2235(c,2,1)),merge(e)]. given #801 (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 #802 (F,wt=17): 2272 p(j,b) | p(g(j),j) | p(m,j) | p(j,k) | p(k,g(j)). [para(531(d,1),2235(c,1)),merge(e)]. given #803 (F,wt=17): 2273 p(j,b) | p(g(j),j) | p(m,j) | p(j,k) | p(j,g(k)). [para(531(d,1),2235(c,2,1)),merge(e)]. given #804 (T,wt=17): 2274 p(j,b) | p(g(j),j) | p(m,j) | p(j,k) | p(b,g(j)). [para(791(d,1),2235(c,1)),merge(e)]. given #805 (T,wt=17): 2275 p(j,b) | p(g(j),j) | p(m,j) | p(j,k) | p(j,g(b)). [para(791(d,1),2235(c,2,1)),merge(e)]. given #806 (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 #807 (F,wt=13): 10362 p(j,b) | p(j,g(j)) | p(k,j) | p(k,b). [factor(10352,a,c),merge(c),merge(f)]. given #808 (F,wt=13): 10371 p(j,b) | p(j,g(j)) | p(k,j) | p(m,j). [factor(10363,a,e),merge(e),merge(f)]. given #809 (T,wt=13): 10386 p(k,j) | p(j,b) | p(j,g(k)) | p(k,b). [para(65(a,1),10362(b,2,1)),merge(d)]. given #810 (T,wt=13): 10431 p(k,j) | p(j,b) | p(j,g(k)) | p(m,j). [para(65(a,1),10371(b,2,1)),merge(d)]. given #811 (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 #812 (F,wt=16): 10370 p(j,b) | p(j,g(j)) | p(k,j) | p(b,j) | p(j,j). [factor(10358,a,d),merge(d)]. given #813 (F,wt=16): 10388 k = b | p(k,j) | p(j,b) | p(j,g(m)) | p(k,b). [para(76(b,1),10362(b,2,1)),merge(e)]. given #814 (T,wt=16): 10432 p(m,j) | k = b | p(j,b) | p(m,g(j)) | p(k,j). [para(62(a,1),10371(b,1)),merge(f)]. given #815 (T,wt=16): 10433 p(m,j) | k = b | p(j,b) | p(j,g(m)) | p(k,j). [para(62(a,1),10371(b,2,1)),merge(f)]. given #816 (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 #817 (F,wt=16): 10490 p(m,j) | k = b | p(k,j) | p(j,b) | p(m,g(k)). [para(62(a,1),10431(c,1)),merge(f)]. given #818 (F,wt=16): 10528 p(k,j) | p(j,b) | p(j,g(k)) | p(b,j) | p(j,j). [para(65(a,1),10370(b,2,1)),merge(d)]. given #819 (T,wt=16): 10550 p(k,j) | p(j,b) | p(j,g(m)) | p(k,b) | j = b. [para(10388(a,1),65(a,2)),merge(f)]. given #820 (T,wt=16): 10565 p(m,j) | p(j,b) | p(m,g(j)) | p(k,j) | j = b. [para(10432(b,1),65(a,2)),merge(f)]. given #821 (A,wt=26): 458 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 #822 (F,wt=16): 10577 p(m,j) | p(j,b) | p(j,g(m)) | p(k,j) | j = b. [para(10433(b,1),65(a,2)),merge(f)]. given #823 (F,wt=16): 10593 p(m,j) | p(k,j) | p(j,b) | p(m,g(k)) | j = b. [para(10490(b,1),65(a,2)),merge(f)]. given #824 (T,wt=17): 2282 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | p(k,g(j)). [para(1534(e,1),2235(c,1)),merge(e),merge(f)]. given #825 (T,wt=17): 2283 p(j,k) | p(j,b) | p(g(j),j) | p(j,j) | p(j,g(k)). [para(1534(e,1),2235(c,2,1)),merge(e),merge(f)]. given #826 (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 #827 (F,wt=17): 2292 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(b,g(j)). [factor(2284,a,e),merge(e)]. given #828 (F,wt=17): 2293 p(j,k) | p(j,b) | p(g(j),j) | p(b,j) | p(j,g(b)). [factor(2285,a,e),merge(e)]. given #829 (T,wt=17): 2334 p(j,b) | p(g(j),j) | p(k,j) | p(j,k) | p(b,g(k)). [para(505(d,1),2249(d,1)),merge(d),merge(f)]. given #830 (T,wt=17): 2460 p(j,b) | p(g(j),j) | p(k,j) | p(k,b) | p(b,g(k)). [para(139(c,1),2439(c,1)),merge(d)]. given #831 (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),77(c,2)),merge(d)]. given #832 (F,wt=17): 2461 p(j,b) | p(g(j),j) | p(k,j) | p(k,b) | p(k,g(b)). [para(139(c,1),2439(c,2,1)),merge(d)]. given #833 (F,wt=17): 2552 p(x,b) | p(x,g(x)) | p(k,j) | p(j,x) | p(k,g(j)). [para(20(a,1),2540(b,2))]. given #834 (T,wt=17): 2553 p(x,b) | p(g(x),x) | p(k,j) | p(j,x) | p(k,g(j)). [para(22(a,1),2540(b,2))]. given #835 (T,wt=17): 2561 p(x,k) | p(x,b) | p(g(x),x) | p(k,j) | p(k,g(j)). [para(324(d,1),2540(b,1)),merge(e),merge(f)]. given #836 (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 #837 (F,wt=17): 2562 p(x,k) | p(x,b) | p(x,g(x)) | p(k,j) | p(k,g(j)). [para(344(d,1),2540(b,1)),merge(e),merge(f)]. given #838 (F,wt=17): 2580 p(j,b) | p(g(j),j) | p(k,j) | p(k,b) | p(b,g(j)). [para(139(c,1),2554(c,1)),merge(d)]. given #839 (T,wt=17): 3297 p(j,k) | p(j,b) | p(m,b) | g(j) = j | g(j) = k. [resolve(2738,c,31,b),flip(d),flip(e)]. given #840 (T,wt=16): 10963 p(j,k) | p(j,b) | p(m,b) | g(j) = k | j = b. [resolve(3297,d,18,c),flip(e),merge(f)]. given #841 (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 #842 (F,wt=10): 10990 p(j,b) | p(j,g(j)) | p(m,j). [factor(10985,a,d),merge(d),merge(e)]. given #843 (F,wt=12): 10975 p(j,k) | p(j,b) | p(m,b) | j = b. [para(10963(d,1),1669(c,2)),merge(e),merge(f),merge(g),merge(h)]. given #844 (T,wt=9): 11078 p(j,k) | p(j,b) | p(m,b). [para(10975(d,1),4140(a,2)),merge(d),merge(e)]. given #845 (T,wt=12): 11089 k = b | p(j,m) | p(j,b) | p(m,b). [para(29(b,1),11078(a,2))]. given #846 (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 #847 (F,wt=9): 11120 p(j,m) | p(j,b) | p(m,b). [para(11089(a,1),2720(a,2)),merge(d),merge(e)]. given #848 (F,wt=13): 11007 p(m,j) | k = b | p(j,b) | p(m,g(j)). [para(62(a,1),10990(b,1)),merge(e)]. given #849 (T,wt=13): 11008 p(m,j) | k = b | p(j,b) | p(j,g(m)). [para(62(a,1),10990(b,2,1)),merge(e)]. given #850 (T,wt=13): 11156 p(j,b) | p(m,b) | j = m | p(f(j),j). [resolve(11120,a,14,b),flip(c)]. given #851 (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 #852 (F,wt=13): 11157 p(j,b) | p(m,b) | j = m | p(j,f(j)). [resolve(11120,a,12,b),flip(c)]. given #853 (F,wt=13): 11205 p(j,b) | p(m,b) | p(f(j),j) | p(k,m). [para(11156(c,1),4111(a,2)),merge(e)]. given #854 (T,wt=13): 11238 p(j,b) | p(m,b) | p(j,f(j)) | p(k,m). [para(11157(c,1),4111(a,2)),merge(e)]. given #855 (T,wt=14): 11019 p(j,b) | p(g(j),j) | p(m,j) | p(k,g(j)). [para(531(d,1),10990(b,1)),merge(d),merge(f)]. given #856 (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 #857 (F,wt=14): 11020 p(j,b) | p(g(j),j) | p(m,j) | p(j,g(k)). [para(531(d,1),10990(b,2,1)),merge(d),merge(f)]. given #858 (F,wt=14): 11021 p(j,b) | p(g(j),j) | p(m,j) | p(b,g(j)). [para(791(d,1),10990(b,1)),merge(d),merge(f)]. given #859 (T,wt=14): 11022 p(j,b) | p(g(j),j) | p(m,j) | p(j,g(b)). [para(791(d,1),10990(b,2,1)),merge(d),merge(f)]. given #860 (T,wt=14): 11199 p(j,b) | p(m,b) | p(f(j),j) | p(g(j),j). [resolve(11156,c,60,c(flip)),merge(d)]. given #861 (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 #862 (F,wt=14): 11200 p(j,b) | p(m,b) | p(f(j),j) | p(j,g(j)). [resolve(11156,c,59,c(flip)),merge(d)]. given #863 (F,wt=14): 11233 p(j,b) | p(m,b) | p(j,f(j)) | p(g(j),j). [resolve(11157,c,60,c(flip)),merge(d)]. given #864 (T,wt=14): 11455 p(j,b) | p(m,b) | p(f(j),j) | p(g(m),j). [para(11156(c,1),11199(d,1,1)),merge(d),merge(e),merge(f)]. given #865 (T,wt=14): 11456 p(j,b) | p(m,b) | p(f(j),j) | p(g(j),m). [para(11156(c,1),11199(d,2)),merge(d),merge(e),merge(f)]. given #866 (A,wt=26): 506 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 #867 (F,wt=14): 11495 p(j,b) | p(m,b) | p(j,f(j)) | p(g(m),j). [para(11157(c,1),11233(d,1,1)),merge(d),merge(e),merge(f)]. given #868 (F,wt=14): 11496 p(j,b) | p(m,b) | p(j,f(j)) | p(g(j),m). [para(11157(c,1),11233(d,2)),merge(d),merge(e),merge(f)]. given #869 (T,wt=15): 11087 p(j,b) | p(m,b) | j = k | j = m | j = b. [resolve(11078,a,6,d),flip(c),flip(d),flip(e)]. given #870 (T,wt=15): 11578 k = b | p(j,b) | p(m,b) | j = m | j = b. [para(29(b,1),11087(c,2)),merge(e)]. given #871 (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 #872 (F,wt=15): 11585 p(j,b) | p(m,b) | j = m | j = b | p(k,k). [para(11087(c,1),4111(a,2)),merge(f)]. given #873 (F,wt=15): 11586 p(m,b) | p(k,m) | p(j,b) | j = m | j = b. [para(4170(b,1),11087(c,2)),merge(d),merge(f)]. given #874 (T,wt=12): 11644 p(m,b) | p(k,m) | p(j,b) | j = b. [para(11586(d,1),4111(a,2)),merge(e),merge(f)]. given #875 (T,wt=9): 11656 p(m,b) | p(k,m) | p(j,b). [para(11644(d,1),4140(a,2)),merge(d),merge(e)]. given #876 (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),77(c,2)),merge(d)]. given #877 (F,wt=15): 11608 k = b | p(j,b) | p(m,b) | j = b | -p(b,m). [factor(11603,a,g),merge(e)]. given #878 (F,wt=15): 11682 k = b | p(j,b) | p(m,b) | j = b | p(b,b). [resolve(11608,e,6154,a)]. given #879 (T,wt=12): 11702 k = b | p(j,b) | p(m,b) | p(b,b). [para(11682(d,1),4140(a,2)),merge(e),merge(f)]. given #880 (T,wt=9): 11715 p(j,b) | p(m,b) | p(b,b). [para(11702(a,1),2720(a,2)),merge(d),merge(e)]. given #881 (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 #882 (F,wt=9): 11728 p(m,b) | k = m | p(b,b). [para(4153(b,1),11715(a,1)),merge(c),merge(d)]. given #883 (F,wt=15): 11745 p(m,b) | p(b,b) | j = x | p(x,j) | m != x. [para(11728(b,1),33(c,1))]. given #884 (T,wt=16): 11162 p(m,j) | p(j,b) | p(m,g(j)) | j = b | p(b,j). [resolve(11007,b,33,c)]. given #885 (T,wt=16): 11181 p(m,j) | p(j,b) | p(j,g(m)) | j = b | p(b,j). [resolve(11008,b,33,c)]. given #886 (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 #887 (F,wt=16): 11587 p(m,b) | p(j,b) | p(g(j),j) | j = m | j = b. [para(4161(b,1),11087(c,2)),merge(d),merge(e),merge(g)]. given #888 (F,wt=13): 11816 p(m,b) | p(j,b) | p(g(j),j) | j = b. [resolve(11587,d,60,c(flip)),merge(e),merge(f)]. given #889 (T,wt=10): 11822 p(m,b) | p(j,b) | p(g(j),j). [para(11816(d,1),4140(a,2)),merge(d),merge(e)]. given #890 (T,wt=13): 11838 p(m,b) | k = m | p(j,b) | p(g(j),m). [para(4153(b,1),11822(c,2)),merge(c)]. given #891 (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 #892 (F,wt=14): 11834 p(m,b) | p(j,b) | g(j) = j | g(j) = k. [resolve(11822,c,31,b),flip(c),flip(d)]. given #893 (F,wt=13): 11871 p(m,b) | p(j,b) | g(j) = k | j = b. [resolve(11834,c,18,c),flip(d),merge(e)]. given #894 (T,wt=12): 11886 p(m,b) | p(j,b) | j = b | k != b. [para(11871(c,1),16(c,1)),flip(d),merge(d),merge(e)]. given #895 (T,wt=12): 11887 p(m,b) | p(j,b) | j = b | j != k. [para(11871(c,1),18(c,1)),flip(d),flip(f),merge(d),merge(e)]. given #896 (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 #897 (F,wt=12): 11922 p(m,b) | p(j,b) | j = b | j = m. [resolve(11887,d,11087,c),merge(d),merge(e),merge(g)]. given #898 (F,wt=12): 11961 p(m,b) | p(j,b) | j = b | k != m. [para(11922(d,1),11887(d,1)),flip(g),merge(d),merge(e),merge(f)]. given #899 (T,wt=12): 11971 p(m,b) | p(j,b) | j = b | k = b. [resolve(11961,d,29,b)]. given #900 (T,wt=9): 11983 p(m,b) | p(j,b) | k = b. [para(11971(c,1),4140(a,2)),merge(d),merge(e)]. given #901 (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 #902 (F,wt=6): 11993 p(m,b) | p(j,b). [para(11983(c,1),2720(a,2)),merge(c),merge(d)]. given #903 (F,wt=6): 12010 p(m,b) | k = m. [para(4153(b,1),11993(b,1)),merge(c),merge(d)]. given #904 (T,wt=12): 12012 p(m,b) | j = x | p(x,j) | m != x. [para(12010(b,1),33(c,1))]. given #905 (T,wt=13): 12004 p(x,b) | p(x,g(x)) | p(m,b) | p(j,x). [para(20(a,1),11993(b,2))]. given #906 (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 #907 (F,wt=13): 12005 p(x,b) | p(g(x),x) | p(m,b) | p(j,x). [para(22(a,1),11993(b,2))]. given #908 (F,wt=15): 12003 p(m,b) | j = m | p(j,m) | j = b | -p(b,j). [resolve(11993,b,2,e),flip(b),flip(e),unit_del(d,27)]. given #909 (T,wt=15): 12011 p(m,b) | k = x | m = x | b = x | -p(x,m). [para(12010(b,1),6(d,2))]. given #910 (T,wt=15): 12067 p(m,b) | g(m) = k | g(m) = m | g(m) = b. [resolve(12011,e,57,b),flip(b),flip(c),flip(d),merge(e)]. given #911 (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 #912 (F,wt=11): 12094 p(m,b) | g(m) = m | g(m) = b. [para(12010(b,1),12067(b,2)),merge(b),merge(d)]. given #913 (F,wt=7): 12103 p(m,b) | g(m) = b. [resolve(12094,b,18,c),flip(c),merge(d),unit_del(c,27)]. given #914 (T,wt=3): 12108 p(m,b). [resolve(12103,b,16,c),flip(b),merge(c),unit_del(b,27)]. given #915 (T,wt=10): 12126 p(x,b) | p(x,g(x)) | p(m,x). [para(20(a,1),12108(a,2))]. given #916 (A,wt=20): 537 p(x,b) | p(x,g(x)) | p(k,b) | p(g(k),k) | j = x | p(k,j). [para(20(a,1),165(c,2))]. given #917 (F,wt=10): 12127 p(x,b) | p(g(x),x) | p(m,x). [para(22(a,1),12108(a,2))]. given #918 (F,wt=12): 12125 b = x | m = x | -p(m,x) | -p(x,m). [resolve(12108,a,4,b),flip(a),flip(c),unit_del(a,27)]. given #919 (T,wt=13): 12142 p(j,b) | p(j,g(j)) | j = m | k = m. [resolve(12126,c,31,b)]. given #920 (T,wt=10): 12172 p(j,b) | p(j,g(j)) | k = m. [resolve(12142,c,59,c(flip)),merge(d),merge(e)]. given #921 (A,wt=20): 538 p(x,b) | p(g(x),x) | p(k,b) | p(g(k),k) | j = x | p(k,j). [para(22(a,1),165(c,2))]. given #922 (F,wt=10): 12183 p(j,b) | p(j,g(j)) | p(k,j). [para(12172(c,1),133(c,1)),merge(c),merge(d),unit_del(c,27)]. given #923 (F,wt=10): 12211 p(k,j) | p(j,b) | p(j,g(k)). [para(65(a,1),12183(b,2,1)),merge(d)]. given #924 (T,wt=13): 12212 k = b | p(k,j) | p(j,b) | p(m,g(j)). [para(76(b,1),12183(b,1)),merge(e)]. given #925 (T,wt=13): 12213 k = b | p(k,j) | p(j,b) | p(j,g(m)). [para(76(b,1),12183(b,2,1)),merge(e)]. given #926 (A,wt=26): 539 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),165(c,2))]. given #927 (F,wt=13): 12246 k = b | p(k,j) | p(j,b) | p(m,g(k)). [para(76(b,1),12211(c,1)),merge(c)]. given #928 (F,wt=13): 12268 p(k,j) | p(j,b) | p(m,g(j)) | j = b. [para(12212(a,1),65(a,2)),merge(e)]. given #929 (T,wt=13): 12280 p(k,j) | p(j,b) | p(j,g(m)) | j = b. [para(12213(a,1),65(a,2)),merge(e)]. given #930 (T,wt=13): 12300 p(k,j) | p(j,b) | p(m,g(k)) | j = b. [para(12246(a,1),65(a,2)),merge(e)]. given #931 (A,wt=26): 540 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),165(c,2))]. given #932 (F,wt=14): 12164 p(j,b) | p(m,j) | g(j) = j | g(j) = k. [resolve(12127,b,31,b),flip(c),flip(d)]. given #933 (F,wt=13): 12339 p(j,b) | p(m,j) | g(j) = k | j = b. [resolve(12164,c,18,c),flip(d),merge(e)]. given #934 (T,wt=12): 12398 p(j,b) | p(m,j) | j = b | k != b. [para(12339(c,1),16(c,1)),flip(d),merge(d),merge(e)]. given #935 (T,wt=12): 12399 p(j,b) | p(m,j) | j = b | j != k. [para(12339(c,1),18(c,1)),flip(d),flip(f),merge(d),merge(e)]. given #936 (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(310,b,41,h),flip(f),flip(i)]. given #937 (F,wt=12): 12414 p(j,b) | p(m,j) | j = b | p(j,k). [para(12339(c,1),2235(c,2)),merge(e),merge(f)]. given #938 (F,wt=12): 12427 p(j,b) | p(m,j) | j = b | p(k,j). [para(12339(c,1),12127(b,1)),merge(d),merge(f)]. given #939 (T,wt=12): 12432 p(j,b) | p(m,j) | j = b | p(b,b). [resolve(12398,d,6608,c),merge(e)]. given #940 (T,wt=12): 12433 p(j,b) | p(m,j) | j = b | p(b,m). [resolve(12398,d,6084,a)]. given #941 (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(310,b,41,g),flip(h)]. given #942 (F,wt=12): 12484 p(j,b) | p(m,j) | p(j,k) | j = k. [resolve(12414,c,26,b(flip)),flip(d),merge(e)]. given #943 (F,wt=12): 12490 p(j,b) | p(m,j) | p(j,k) | k = b. [para(12414(c,1),62(a,1)),flip(d),merge(e),unit_del(d,27)]. given #944 (T,wt=12): 12514 p(j,b) | p(m,j) | p(k,j) | k = b. [para(12427(c,1),65(a,1)),flip(d),merge(e)]. given #945 (T,wt=12): 12536 p(j,b) | p(m,j) | p(b,b) | p(k,b). [para(12432(c,1),8723(b,2)),merge(d)]. given #946 (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(310,b,36,h),flip(f),flip(i)]. given #947 (F,wt=12): 12553 p(j,b) | p(m,j) | p(b,m) | p(k,b). [para(12433(c,1),6313(b,2)),merge(d)]. given #948 (F,wt=13): 12341 p(k,j) | p(j,b) | p(m,j) | g(j) = k. [para(65(a,1),12164(c,2)),merge(e)]. given #949 (T,wt=9): 12677 p(k,j) | p(j,b) | p(m,j). [para(12341(d,1),12127(b,1)),merge(d),merge(e),merge(f)]. given #950 (T,wt=9): 12682 p(k,j) | p(k,b) | p(m,j). [para(65(a,1),12677(b,1)),merge(b)]. given #951 (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(310,b,36,g),flip(h)]. given #952 (F,wt=9): 12701 k = b | p(m,j) | p(k,b). [para(29(b,1),12682(a,1)),merge(d)]. given #953 (F,wt=9): 12748 p(m,j) | p(k,b) | p(b,j). [para(12701(a,1),12682(a,1)),merge(d),merge(e)]. given #954 (T,wt=12): 12717 p(j,b) | p(m,j) | p(j,k) | p(k,b). [para(12414(c,1),12682(a,2)),merge(e),merge(f)]. given #955 (T,wt=9): 12774 p(m,j) | p(k,b) | p(j,b). [para(12701(a,1),12717(c,2)),merge(d),merge(e),merge(f)]. given #956 (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(310,b,4,f),flip(d),flip(g)]. given #957 (F,wt=13): 12393 p(j,b) | p(m,j) | g(j) = k | p(j,j). [para(12164(c,1),12126(b,2)),merge(d),merge(f)]. given #958 (F,wt=12): 12814 p(j,b) | p(m,j) | p(j,j) | p(j,k). [para(12393(c,1),570(b,2)),merge(d),merge(f),merge(g)]. given #959 (T,wt=9): 12831 p(j,b) | p(m,j) | p(j,k). [para(12414(c,1),12814(c,2)),merge(d),merge(e),merge(f),merge(g)]. given #960 (T,wt=9): 12852 p(b,m) | p(j,b) | p(m,j). [para(6084(a,1),12831(c,2)),merge(d)]. given #961 (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(310,b,2,f),flip(d),flip(g)]. given #962 (F,wt=9): 12853 p(b,b) | p(m,j) | p(j,b). [para(6608(c,1),12831(c,2)),merge(d),merge(e)]. given #963 (F,wt=10): 12854 p(m,j) | p(j,b) | p(m,g(j)). [para(11007(b,1),12831(c,2)),merge(d),merge(e),merge(f)]. given #964 (T,wt=10): 12855 p(m,j) | p(j,b) | p(j,g(m)). [para(11008(b,1),12831(c,2)),merge(d),merge(e),merge(f)]. given #965 (T,wt=12): 12844 k = b | p(j,b) | p(m,j) | p(j,m). [para(29(b,1),12831(c,2))]. given #966 (A,wt=19): 555 p(x,b) | p(x,g(x)) | p(x,j) | p(k,j) | j = b | k = b. [resolve(310,c,77,c)]. given #967 (F,wt=9): 12923 p(j,b) | p(m,j) | p(j,m). [para(12844(a,1),12831(c,2)),merge(d),merge(e),merge(f)]. given #968 (F,wt=12): 12856 p(b,m) | p(m,j) | j = m | j = b. [resolve(12852,b,6329,d),merge(c)]. given #969 (T,wt=9): 12940 p(b,m) | p(m,j) | j = b. [para(12856(c,1),6326(b,2)),merge(d),merge(e)]. given #970 (T,wt=9): 12955 p(b,m) | p(m,j) | p(k,b). [para(12940(c,1),6313(b,2)),merge(c)]. given #971 (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),310(c,1))]. given #972 (F,wt=12): 12930 p(m,j) | k = b | p(j,b) | p(m,m). [para(62(a,1),12923(c,1)),merge(d)]. given #973 (F,wt=9): 13020 p(m,j) | p(j,b) | p(m,m). [para(12930(b,1),12831(c,2)),merge(d),merge(e),merge(f)]. given #974 (T,wt=12): 12941 p(b,m) | p(m,j) | j = k | p(j,k). [resolve(12940,c,26,b(flip)),flip(c)]. given #975 (T,wt=12): 13031 p(b,m) | p(m,j) | p(j,k) | p(k,k). [para(12941(c,1),6313(b,2)),merge(d)]. given #976 (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),310(c,1))]. given #977 (F,wt=13): 12789 p(k,b) | p(k,g(k)) | p(m,j) | p(j,k). [factor(12779,a,d)]. given #978 (F,wt=13): 12790 p(k,b) | p(g(k),k) | p(m,j) | p(j,k). [factor(12780,a,d)]. given #979 (T,wt=13): 12912 p(m,j) | k = b | p(j,b) | p(m,g(m)). [para(62(a,1),12855(c,1)),merge(c)]. given #980 (T,wt=10): 13136 p(m,j) | p(j,b) | p(m,g(m)). [para(12912(b,1),12831(c,2)),merge(d),merge(e),merge(f)]. given #981 (A,wt=26): 560 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),310(c,1))]. given #982 (F,wt=13): 12928 p(j,b) | p(m,j) | j = m | p(f(j),j). [resolve(12923,c,14,b),flip(c)]. given #983 (F,wt=13): 12929 p(j,b) | p(m,j) | j = m | p(j,f(j)). [resolve(12923,c,12,b),flip(c)]. given #984 (T,wt=13): 12962 p(x,b) | p(x,g(x)) | p(b,m) | p(m,j). [para(6131(c,1),12955(c,1)),merge(d),merge(f)]. given #985 (T,wt=13): 12963 p(x,b) | p(g(x),x) | p(b,m) | p(m,j). [para(6132(c,1),12955(c,1)),merge(d),merge(f)]. given #986 (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),310(c,2))]. given #987 (F,wt=13): 13124 p(m,j) | p(k,b) | p(g(b),k) | p(j,k). [para(12701(a,1),12790(b,1,1)),merge(c),merge(e)]. given #988 (F,wt=13): 13125 p(m,j) | p(k,b) | p(g(k),b) | p(j,k). [para(12701(a,1),12790(b,2)),merge(c),merge(e)]. given #989 (T,wt=13): 13291 p(m,j) | p(k,b) | p(g(b),b) | p(j,k). [para(12701(a,1),13124(c,2)),merge(c),merge(d)]. given #990 (T,wt=14): 12175 p(j,b) | p(j,g(j)) | p(k,b) | p(g(k),k). [resolve(12172,c,60,c(flip))]. given #991 (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),310(c,2))]. given #992 (F,wt=14): 12176 p(j,b) | p(j,g(j)) | p(k,b) | p(k,g(k)). [resolve(12172,c,59,c(flip))]. given #993 (F,wt=14): 12214 p(j,b) | p(g(j),j) | p(k,j) | p(b,g(j)). [para(505(d,1),12183(b,1)),merge(d),merge(f)]. given #994 (T,wt=14): 12215 p(j,b) | p(g(j),j) | p(k,j) | p(j,g(b)). [para(505(d,1),12183(b,2,1)),merge(d),merge(f)]. given #995 (T,wt=14): 12248 p(j,b) | p(g(j),j) | p(k,j) | p(b,g(k)). [para(505(d,1),12211(c,1)),merge(d),merge(e)]. given #996 (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),310(c,1))]. given #997 (F,wt=14): 12274 p(k,j) | p(j,b) | p(m,g(j)) | p(j,g(b)). [para(12212(a,1),12211(c,2,1)),merge(d),merge(e)]. given #998 (F,wt=14): 12286 p(k,j) | p(j,b) | p(j,g(m)) | p(j,g(b)). [para(12213(a,1),12211(c,2,1)),merge(d),merge(e)]. given #999 (T,wt=14): 12306 p(k,j) | p(j,b) | p(m,g(k)) | p(j,g(b)). [para(12246(a,1),12211(c,2,1)),merge(d),merge(e)]. given #1000 (T,wt=14): 12313 p(k,j) | p(j,b) | p(m,g(j)) | p(b,g(j)). [para(12268(d,1),12183(b,1)),merge(d),merge(f)]. given #1001 (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(560,a,d),merge(d)]. given #1002 (F,wt=14): 12314 p(k,j) | p(j,b) | p(m,g(j)) | p(b,g(k)). [para(12268(d,1),12211(c,1)),merge(d),merge(e)]. given #1003 (F,wt=14): 12321 p(k,j) | p(j,b) | p(j,g(m)) | p(b,g(j)). [para(12280(d,1),12183(b,1)),merge(d),merge(f)]. given #1004 (T,wt=14): 12322 p(k,j) | p(j,b) | p(j,g(m)) | p(b,g(k)). [para(12280(d,1),12211(c,1)),merge(d),merge(e)]. given #1005 (T,wt=14): 12329 p(k,j) | p(j,b) | p(m,g(k)) | p(b,g(j)). [para(12300(d,1),12183(b,1)),merge(d),merge(f)]. given #1006 (A,wt=27): 590 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(311,b,2,f),flip(f)]. given #1007 (F,wt=14): 12330 p(k,j) | p(j,b) | p(m,g(k)) | p(b,g(k)). [para(12300(d,1),12211(c,1)),merge(d),merge(e)]. given #1008 (F,wt=14): 13330 p(j,b) | p(j,g(j)) | p(k,b) | p(g(m),k). [para(12172(c,1),12175(d,1,1)),merge(c),merge(d)]. given #1009 (T,wt=14): 13331 p(j,b) | p(j,g(j)) | p(k,b) | p(g(k),m). [para(12172(c,1),12175(d,2)),merge(c),merge(d)]. given #1010 (T,wt=14): 13445 p(k,j) | p(j,b) | p(g(k),j) | p(b,g(j)). [para(65(a,1),12214(b,1,1)),merge(d)]. given #1011 (A,wt=19): 594 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 #1012 (F,wt=14): 13446 p(k,j) | p(j,b) | p(g(j),k) | p(b,g(j)). [para(65(a,1),12214(b,2)),merge(d)]. given #1013 (F,wt=14): 13463 p(k,j) | p(j,b) | p(g(k),j) | p(j,g(b)). [para(65(a,1),12215(b,1,1)),merge(d)]. given #1014 (T,wt=14): 13464 p(k,j) | p(j,b) | p(g(j),k) | p(j,g(b)). [para(65(a,1),12215(b,2)),merge(d)]. given #1015 (T,wt=14): 13481 p(k,j) | p(j,b) | p(g(k),j) | p(b,g(k)). [para(65(a,1),12248(b,1,1)),merge(d)]. given #1016 (A,wt=19): 595 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 #1017 (F,wt=14): 13482 p(k,j) | p(j,b) | p(g(j),k) | p(b,g(k)). [para(65(a,1),12248(b,2)),merge(d)]. given #1018 (F,wt=14): 13541 p(k,j) | p(j,b) | p(m,g(j)) | p(k,g(b)). [para(65(a,1),12274(d,1)),merge(b)]. given #1019 (T,wt=14): 13563 p(k,j) | p(j,b) | p(m,g(j)) | p(b,g(b)). [para(12268(d,1),12274(d,1)),merge(d),merge(e),merge(f)]. given #1020 (T,wt=14): 13580 p(k,j) | p(j,b) | p(k,g(m)) | p(j,g(b)). [para(65(a,1),12286(c,1)),merge(b)]. given #1021 (A,wt=28): 647 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(b,k) | k = y | m = y | b = y | -p(y,x). [para(34(c,1),71(e,2))]. given #1022 (F,wt=14): 13588 p(k,j) | p(j,b) | p(m,g(k)) | p(k,g(b)). [para(65(a,1),12306(d,1)),merge(b)]. given #1023 (F,wt=14): 13611 p(k,j) | p(j,b) | p(m,g(k)) | p(b,g(b)). [para(12300(d,1),12306(d,1)),merge(d),merge(e),merge(f)]. given #1024 (T,wt=14): 13681 p(k,j) | p(j,b) | p(k,g(m)) | p(b,g(j)). [para(65(a,1),12321(c,1)),merge(b)]. given #1025 (T,wt=14): 13700 p(k,j) | p(j,b) | p(k,g(m)) | p(b,g(k)). [para(65(a,1),12322(c,1)),merge(b)]. given #1026 (A,wt=28): 648 p(g(x),b) | p(g(g(x)),g(x)) | p(x,b) | p(b,k) | k = y | m = y | b = y | -p(y,x). [para(39(c,1),71(e,2))]. given #1027 (F,wt=14): 13754 p(j,b) | p(j,g(j)) | p(k,b) | p(g(m),m). [para(12172(c,1),13330(d,2)),merge(c),merge(d)]. given #1028 (F,wt=14): 13785 p(k,j) | p(j,b) | p(g(k),k) | p(b,g(j)). [para(65(a,1),13445(c,2)),merge(b)]. given #1029 (T,wt=14): 13828 p(k,j) | p(j,b) | p(g(k),k) | p(j,g(b)). [para(65(a,1),13463(c,2)),merge(b)]. given #1030 (T,wt=14): 13871 p(k,j) | p(j,b) | p(g(k),k) | p(b,g(k)). [para(65(a,1),13481(c,2)),merge(b)]. given #1031 (A,wt=22): 675 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | j = x | p(x,j). [resolve(80,d,33,c)]. given #1032 (F,wt=14): 13938 p(k,j) | p(j,b) | p(k,g(m)) | p(k,g(b)). [para(65(a,1),13580(d,1)),merge(b)]. given #1033 (F,wt=15): 12113 p(b,b) | p(b,j) | j = b | j = m | -p(j,m). [back_unit_del(8788),unit_del(c,12108)]. given #1034 (T,wt=15): 12115 p(m,k) | p(b,b) | j = b | j = m | -p(j,m). [back_unit_del(6415),unit_del(c,12108)]. given #1035 (T,wt=15): 12442 k = b | p(j,b) | p(m,j) | j = b | j != m. [para(29(b,1),12399(d,2))]. given #1036 (A,wt=27): 676 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(80,d,10,c(flip)),flip(e)]. given #1037 (F,wt=12): 14150 k = b | p(j,b) | p(m,j) | j = b. [resolve(12442,e,62,a),merge(e),merge(f)]. given #1038 (F,wt=9): 14194 k = b | p(j,b) | p(m,j). [para(14150(d,1),62(a,1)),flip(d),merge(e),merge(f),unit_del(d,27)]. given #1039 (T,wt=6): 14205 p(j,b) | p(m,j). [para(14194(a,1),12831(c,2)),merge(c),merge(d),merge(e)]. given #1040 (T,wt=13): 14208 p(x,b) | p(x,g(x)) | p(j,x) | p(m,j). [para(20(a,1),14205(a,2))]. given #1041 (A,wt=28): 677 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(80(d,1),6(d,2))]. given #1042 (F,wt=13): 14209 p(x,b) | p(g(x),x) | p(j,x) | p(m,j). [para(22(a,1),14205(a,2))]. given #1043 (F,wt=15): 12737 p(m,j) | p(k,b) | j = x | p(x,j) | b != x. [para(12701(a,1),33(c,1))]. given #1044 (T,wt=15): 12944 p(b,m) | p(m,j) | j = x | -p(x,b) | k = x. [para(12940(c,1),31(b,2))]. given #1045 (T,wt=12): 14264 p(b,m) | p(m,j) | j = m | k = m. [resolve(12944,d,12108,a)]. given #1046 (A,wt=22): 678 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | k = b | m = x. [para(80(d,1),29(b,1)),flip(f)]. given #1047 (F,wt=9): 14267 p(b,m) | p(m,j) | k = m. [para(14264(c,1),6326(b,2)),merge(d),merge(e)]. given #1048 (F,wt=6): 14309 p(b,m) | p(m,j). [para(14267(c,1),6060(a,2)),merge(c),merge(d)]. given #1049 (T,wt=9): 14311 p(b,m) | j = m | k = m. [resolve(14309,b,31,b)]. given #1050 (T,wt=6): 14326 p(b,m) | k = m. [para(14311(b,1),6326(b,2)),merge(c),merge(d)]. given #1051 (A,wt=25): 679 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | j = y | p(y,j) | x != y. [para(80(d,1),33(c,1))]. given #1052 (F,wt=3): 14333 p(b,m). [para(14326(b,1),6060(a,2)),merge(b),merge(c)]. given #1053 (F,wt=4): 14377 f(b) != b. [ur(10,a,27,a,b,14333,a)]. given #1054 (T,wt=4): 14375 p(f(b),b). [resolve(14333,a,14,b),unit_del(a,27)]. given #1055 (T,wt=4): 14376 p(b,f(b)). [resolve(14333,a,12,b),unit_del(a,27)]. given #1056 (A,wt=22): 681 p(g(x),b) | p(g(x),g(g(x))) | p(x,b) | p(x,k) | j = x | p(k,j). [para(80(d,1),65(a,2))]. given #1057 (F,wt=4): 14378 f(b) != m. [ur(8,a,27,a,b,14333,a)]. given #1058 (F,wt=4): 14436 p(f(b),m). [resolve(14375,a,2,e),flip(a),flip(d),unit_del(a,14378),unit_del(c,27),unit_del(d,14377),unit_del(e,14376)]. given #1059 (T,wt=6): 14502 p(f(f(b)),f(b)). [resolve(14436,a,14,b),flip(a),unit_del(a,14378)]. given #1060 (T,wt=5): 14520 f(f(b)) = b. [resolve(14502,a,4,f),flip(a),flip(c),unit_del(a,14377),unit_del(b,14375),unit_del(d,14504),unit_del(e,14503)]. given #1061 (A,wt=28): 692 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(80(d,1),77(c,2))]. given #1062 (F,wt=4): 14495 -p(m,f(b)). [resolve(14436,a,12125,d),flip(a),flip(b),unit_del(a,14377),unit_del(b,14378)]. given #1063 (F,wt=7): 14434 p(b,k) | f(b) = k. [resolve(14375,a,71,e),flip(b),flip(c),flip(d),unit_del(c,14378),unit_del(d,14377)]. given #1064 (T,wt=3): 14557 p(b,k). [para(54(a,1),14434(b,2)),merge(b),unit_del(b,14377)]. given #1065 (T,wt=6): 14568 p(b,b) | p(m,j). [para(6608(c,1),14557(a,2)),merge(c)]. given #1066 (A,wt=26): 752 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),81(d,2))]. given #1067 (F,wt=7): 14500 p(m,k) | f(b) = k. [resolve(14436,a,68,e),flip(b),flip(c),flip(d),unit_del(c,14378),unit_del(d,14377)]. given #1068 (F,wt=3): 14597 p(m,k). [para(51(a,1),14500(b,2)),merge(b),unit_del(b,14378)]. given #1069 (T,wt=6): 14599 k = b | p(m,m). [para(29(b,1),14597(a,2))]. given #1070 (T,wt=6): 14632 p(m,m) | p(b,b). [para(14599(a,1),14557(a,2))]. given #1071 (A,wt=26): 753 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),81(d,2))]. given #1072 (F,wt=7): 14501 k = b | f(b) = k. [resolve(14436,a,61,e),flip(b),flip(c),flip(d),unit_del(c,14378),unit_del(d,14377)]. given #1073 (F,wt=3): 14645 k = b. [para(29(b,1),14501(b,2)),merge(b),unit_del(b,14378)]. given #1074 (T,wt=3): 14690 p(b,b). [back_rewrite(14557),rewrite(14645(2))]. given #1075 (T,wt=6): 14663 p(b,j) | j = m. [back_rewrite(14598),rewrite(14645(1),14645(7)),flip(c),unit_del(c,27)]. given #1076 (A,wt=25): 6778 p(x,b) | p(x,m) | g(x) = b | -p(g(x),b) | b = x | g(x) = x | -p(g(x),x). [resolve(6769,b,4,f),flip(c),flip(f)]. given #1077 (F,wt=6): 14789 j = b | p(b,j). [back_rewrite(65),rewrite(14645(2),14645(4))]. given #1078 (F,wt=3): 14794 p(b,j). [para(14789(a,1),14663(b,1)),flip(c),merge(b),unit_del(b,27)]. given #1079 (T,wt=7): 14688 p(x,b) | p(g(x),x). [back_rewrite(14559),rewrite(14645(5)),merge(c)]. given #1080 (T,wt=7): 14689 p(x,b) | p(x,g(x)). [back_rewrite(14558),rewrite(14645(5)),merge(c)]. given #1081 (A,wt=21): 6780 p(x,b) | p(x,m) | m = x | g(x) = m | g(x) = x | -p(g(x),x). [resolve(6769,b,2,e),flip(e),merge(d)]. given #1082 (F,wt=9): 14790 j = x | p(x,j) | b != x. [back_rewrite(33),rewrite(14645(5))]. given #1083 (F,wt=9): 14791 j = x | -p(x,j) | b = x. [back_rewrite(31),rewrite(14645(5))]. given #1084 (T,wt=9): 14792 b = x | m != x | p(x,b). [back_rewrite(24),rewrite(14645(1),14645(5))]. given #1085 (T,wt=9): 14793 b = x | m = x | -p(x,b). [back_rewrite(6),rewrite(14645(1),14645(7)),merge(c)]. ============================== PROOF ================================= % Proof 1 at 10.17 (+ 0.06) seconds. % Length of proof is 155. % Level of proof is 57. % Maximum clause weight is 23. % Given clauses 1085. 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)]. 75 p(b,k) | p(m,k). [para(54(a,1),51(a,1)),flip(b),unit_del(b,27)]. 77 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),75(b,2)),merge(b)]. 101 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))]. 157 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)]. 256 p(k,j) | j = m | k = m | p(b,k). [resolve(77,c,75,b)]. 298 p(k,j) | k = m | p(b,k). [para(256(b,1),65(a,1)),flip(d),merge(d),merge(e)]. 304 p(k,j) | p(b,k). [para(298(b,1),54(a,1)),merge(d),unit_del(c,27)]. 307 p(b,k) | p(b,j). [para(54(a,1),304(a,1)),merge(c)]. 309 p(b,k) | p(b,m) | j = m | j = b | -p(j,b). [resolve(307,b,2,e),flip(d),unit_del(b,27)]. 310 p(x,b) | p(x,g(x)) | p(b,k) | p(x,j). [para(20(a,1),307(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(101,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),310(c,1))]. 570 p(x,b) | p(x,g(x)) | p(x,k) | p(x,j). [factor(556,a,c),merge(c)]. 1538 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)]. 1624 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),1624(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),1624(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)]. 1684 p(j,k) | p(j,b) | p(j,g(j)) | j = m | k = m. [resolve(1665,d,31,b)]. 2217 p(j,k) | p(j,b) | p(j,g(j)) | k = m. [resolve(1684,d,59,c(flip)),merge(e),merge(f)]. 2231 p(j,k) | p(j,b) | p(j,g(j)) | p(x,k) | p(x,b) | p(x,g(x)). [para(2217(d,1),1605(d,1)),unit_del(g,27)]. 2235 p(j,k) | p(j,b) | p(j,g(j)). [factor(2231,a,d),merge(d),merge(e)]. 2314 p(m,k) | p(k,b) | g(k) = m | g(k) = b. [para(51(a,1),157(c,2)),merge(c),merge(e)]. 2703 p(m,k) | p(k,b) | g(k) = b. [para(2314(c,1),142(b,1)),merge(d),merge(e),merge(f)]. 2712 p(m,k) | p(k,b). [para(2703(c,1),136(b,2)),merge(c),merge(d),merge(e)]. 2720 p(m,k) | p(m,b). [para(51(a,1),2712(b,1)),merge(b)]. 2726 p(m,b) | p(k,j) | j = m | k = m. [resolve(2720,a,77,c)]. 2738 p(x,k) | p(x,b) | p(g(x),x) | p(m,b). [para(1538(d,1),2720(a,2)),merge(e)]. 2883 p(m,b) | p(k,j) | k = m. [para(2726(c,1),65(a,1)),flip(d),merge(d),merge(e)]. 2888 p(m,b) | p(k,j) | j = x | -p(x,m) | k = x. [para(2883(c,1),77(c,2)),merge(c)]. 3297 p(j,k) | p(j,b) | p(m,b) | g(j) = j | g(j) = k. [resolve(2738,c,31,b),flip(d),flip(e)]. 4075 p(m,b) | p(k,j) | g(m) = j | g(m) = k. [resolve(2888,d,57,b),flip(c),flip(d),merge(e)]. 4078 p(k,j) | p(m,b) | g(m) = k. [para(65(a,1),4075(c,2)),merge(c),merge(e)]. 4081 p(k,j) | p(m,b) | k != m. [para(4078(c,1),18(c,1)),flip(c),merge(d),unit_del(c,27)]. 4111 p(k,j) | p(m,b). [resolve(4081,c,2883,c),merge(c),merge(d)]. 4128 k = b | p(m,j) | p(m,b). [para(29(b,1),4111(a,1))]. 4140 p(m,j) | p(m,b). [para(4128(a,1),2720(a,2)),merge(c),merge(d)]. 4153 p(m,b) | j = m | k = m. [resolve(4140,a,31,b)]. 4161 p(m,b) | k = m | p(j,b) | p(g(j),j). [resolve(4153,b,60,c(flip))]. 5736 p(j,b) | p(b,k) | p(m,j) | g(j) = k | j = b. [resolve(400,d,18,c),flip(e),merge(f)]. 5745 p(j,b) | p(b,k) | p(m,j) | j = b | k != b. [para(5736(d,1),16(c,1)),flip(e),merge(e),merge(f)]. 5771 p(j,b) | p(b,k) | p(m,j) | j = b. [resolve(5745,e,54,a),merge(e)]. 5791 p(j,b) | p(b,k) | p(m,j) | j = k | p(j,k). [resolve(5771,d,26,b(flip)),flip(d)]. 5885 p(j,b) | p(b,k) | p(m,j) | p(j,k). [para(5791(d,1),307(b,2)),merge(e),merge(f)]. 5888 p(b,k) | p(j,b) | p(m,j). [para(54(a,1),5885(d,2)),merge(c),merge(e)]. 5911 p(b,k) | p(m,j) | p(b,m) | j = m | j = b. [resolve(5888,b,309,e),merge(c)]. 5924 p(b,k) | p(m,j) | p(b,m) | j = b. [para(5911(d,1),307(b,2)),merge(e),merge(f)]. 5929 p(b,k) | p(m,j) | p(b,m) | j = k | p(j,k). [resolve(5924,d,26,b(flip)),flip(d)]. 6034 p(b,k) | p(m,j) | p(b,m) | p(j,k). [para(5929(d,1),307(b,2)),merge(e),merge(f)]. 6043 p(b,k) | p(m,j) | p(b,m). [para(5924(d,1),6034(d,1)),merge(d),merge(e),merge(f),merge(g)]. 6046 p(b,k) | p(b,m) | j = m | k = m. [resolve(6043,b,31,b)]. 6053 p(b,k) | p(b,m) | k = m. [para(6046(c,1),307(b,2)),merge(d),merge(e)]. 6060 p(b,k) | p(b,m). [para(6053(c,1),54(a,1)),merge(d),unit_del(c,27)]. 6084 k = b | p(b,m). [para(29(b,1),6060(a,2)),merge(c)]. 6085 p(m,k) | p(b,m). [para(51(a,1),6060(a,2)),merge(c)]. 6157 p(b,m) | p(k,j) | j = m | k = m. [resolve(6085,a,77,c)]. 6290 p(b,m) | p(k,j) | k = m. [para(6157(c,1),65(a,1)),flip(d),merge(d),merge(e)]. 6313 p(b,m) | p(k,j). [para(6290(c,1),6060(a,2)),merge(c),merge(d)]. 6326 p(b,m) | p(b,j). [para(6084(a,1),6313(b,1)),merge(b)]. 6329 p(b,m) | j = m | j = b | -p(j,b). [resolve(6326,b,2,e),flip(d),merge(c),unit_del(b,27)]. 10963 p(j,k) | p(j,b) | p(m,b) | g(j) = k | j = b. [resolve(3297,d,18,c),flip(e),merge(f)]. 10975 p(j,k) | p(j,b) | p(m,b) | j = b. [para(10963(d,1),1669(c,2)),merge(e),merge(f),merge(g),merge(h)]. 11078 p(j,k) | p(j,b) | p(m,b). [para(10975(d,1),4140(a,2)),merge(d),merge(e)]. 11087 p(j,b) | p(m,b) | j = k | j = m | j = b. [resolve(11078,a,6,d),flip(c),flip(d),flip(e)]. 11587 p(m,b) | p(j,b) | p(g(j),j) | j = m | j = b. [para(4161(b,1),11087(c,2)),merge(d),merge(e),merge(g)]. 11816 p(m,b) | p(j,b) | p(g(j),j) | j = b. [resolve(11587,d,60,c(flip)),merge(e),merge(f)]. 11822 p(m,b) | p(j,b) | p(g(j),j). [para(11816(d,1),4140(a,2)),merge(d),merge(e)]. 11834 p(m,b) | p(j,b) | g(j) = j | g(j) = k. [resolve(11822,c,31,b),flip(c),flip(d)]. 11871 p(m,b) | p(j,b) | g(j) = k | j = b. [resolve(11834,c,18,c),flip(d),merge(e)]. 11887 p(m,b) | p(j,b) | j = b | j != k. [para(11871(c,1),18(c,1)),flip(d),flip(f),merge(d),merge(e)]. 11922 p(m,b) | p(j,b) | j = b | j = m. [resolve(11887,d,11087,c),merge(d),merge(e),merge(g)]. 11961 p(m,b) | p(j,b) | j = b | k != m. [para(11922(d,1),11887(d,1)),flip(g),merge(d),merge(e),merge(f)]. 11971 p(m,b)