============================== Prover9 =============================== Prover9 (32) version June-2007-, 4 June 2007. Process 16627 was started by mccune on cleo, Mon Jun 11 15:16:13 2007 The command was "prover9 -f h1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file h1.in assign(sos_limit,40000). assign(max_weight,35). assign(max_vars,3). set(restrict_denials). assign(max_hours,1). % assign(max_hours, 1) -> assign(max_seconds, 3600). assign(eq_defs,fold). assign(pick_given_ratio,8). % assign(pick_given_ratio, 8) -> assign(age_part, 1). % assign(pick_given_ratio, 8) -> assign(weight_part, 8). % assign(pick_given_ratio, 8) -> assign(false_part, 0). % assign(pick_given_ratio, 8) -> assign(true_part, 0). % assign(pick_given_ratio, 8) -> assign(random_part, 0). list(weights). weight(h(_)) = 1. weight(h(x)) = 1000. end_of_list. formulas(assumptions). x + y = y + x # label(Commutativity). (x + y) + z = x + (y + z) # label(Associativity). ((x + y)' + (x + y')')' = x # label(Robbins). end_of_list. formulas(assumptions). h(x) = x + (x + x')' # label(definition_h). end_of_list. formulas(goals). (x + y')' + (x' + y')' = y # answer(Huntington). (exists a exists b a + b = a) # answer(Winker1a). (exists a exists b a + b = b) # answer(Winker1b). (exists a exists b (a + b)' = a') # answer(Winker2a). (exists a exists b (a + b)' = b') # answer(Winker2b). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (x + y')' + (x' + y')' = y # answer(Huntington) # label(non_clause) # label(goal). [goal]. 2 (exists a exists b a + b = a) # answer(Winker1a) # label(non_clause) # label(goal). [goal]. 3 (exists a exists b a + b = b) # answer(Winker1b) # label(non_clause) # label(goal). [goal]. 4 (exists a exists b (a + b)' = a') # answer(Winker2a) # label(non_clause) # label(goal). [goal]. 5 (exists a exists b (a + b)' = b') # answer(Winker2b) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x + y = y + x # label(Commutativity). [assumption]. (x + y) + z = x + (y + z) # label(Associativity). [assumption]. ((x + y)' + (x + y')')' = x # label(Robbins). [assumption]. h(x) = x + (x + x')' # label(definition_h). [assumption]. (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [deny(1)]. x + y != x # answer(Winker1a). [deny(2)]. x + y != y # answer(Winker1b). [deny(3)]. (x + y)' != x' # answer(Winker2a). [deny(4)]. (x + y)' != y' # answer(Winker2b). [deny(5)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 5). % (Horn set with more than one neg. clause) Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, +, ', h ]). After inverse_order: (no changes). Folding symbols: h/1. After fold_eq: Function symbol precedence: function_order([ c1, c2, h, +, ' ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). % Operation + is commutative; C redundancy checks enabled. restricted denial: (wt=14): 11 (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [deny(1)]. restricted denial: (wt=5): 12 x + y != x # answer(Winker1a). [deny(2)]. restricted denial: (wt=5): 13 x + y != y # answer(Winker1b). [deny(3)]. restricted denial: (wt=7): 14 (x + y)' != x' # answer(Winker2a). [deny(4)]. restricted denial: (wt=7): 15 (x + y)' != y' # answer(Winker2b). [deny(5)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 11 (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [deny(1)]. 12 x + y != x # answer(Winker1a). [deny(2)]. 13 x + y != y # answer(Winker1b). [deny(3)]. 14 (x + y)' != x' # answer(Winker2a). [deny(4)]. 15 (x + y)' != y' # answer(Winker2b). [deny(5)]. end_of_list. formulas(sos). 6 x + y = y + x # label(Commutativity). [assumption]. 7 (x + y) + z = x + (y + z) # label(Associativity). [assumption]. 8 ((x + y)' + (x + y')')' = x # label(Robbins). [assumption]. 10 x + (x + x')' = h(x). [copy(9),flip(a)]. end_of_list. formulas(demodulators). 6 x + y = y + x # label(Commutativity). [assumption]. % (lex-dep) 7 (x + y) + z = x + (y + z) # label(Associativity). [assumption]. 8 ((x + y)' + (x + y')')' = x # label(Robbins). [assumption]. 10 x + (x + x')' = h(x). [copy(9),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 6 x + y = y + x # label(Commutativity). [assumption]. given #2 (I,wt=11): 7 (x + y) + z = x + (y + z) # label(Associativity). [assumption]. % Operation + is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 16 x + (y + z) = z + (x + y). [para(7(a,1),6(a,1))]. given #3 (I,wt=13): 8 ((x + y)' + (x + y')')' = x # label(Robbins). [assumption]. given #4 (I,wt=9): 10 x + (x + x')' = h(x). [copy(9),flip(a)]. given #5 (A,wt=11): 17 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),rewrite([7(2)])]. given #6 (W,wt=13): 18 ((x + y)' + (y + x')')' = y. [para(6(a,1),8(a,1,1,1,1))]. given #7 (W,wt=13): 19 ((x + y)' + (y' + x)')' = x. [para(6(a,1),8(a,1,1,2,1))]. given #8 (W,wt=13): 24 x + ((x + x')' + y) = h(x) + y. [para(10(a,1),7(a,1,1)),flip(a)]. given #9 (W,wt=13): 26 (h(x)' + (x + (x + x'))')' = x. [para(10(a,1),8(a,1,1,2,1)),rewrite([6(7)])]. given #10 (W,wt=13): 28 x + (y + (x + x')') = y + h(x). [para(10(a,1),17(a,1,2)),flip(a)]. given #11 (W,wt=13): 29 ((x + y)' + (x' + y)')' = y. [para(6(a,1),18(a,1,1,2,1))]. given #12 (W,wt=13): 30 ((x + y')' + (y + x)')' = x. [para(6(a,1),18(a,1,1))]. given #13 (W,wt=13): 42 ((x' + y)' + (y + x)')' = y. [para(6(a,1),19(a,1,1))]. given #14 (A,wt=19): 20 ((x + (y + z))' + (x + (y + z'))')' = x + y. [para(7(a,1),8(a,1,1,1,1)),rewrite([7(6)])]. given #15 (W,wt=15): 25 (h(x)' + (x + (x + x')'')')' = x. [para(10(a,1),8(a,1,1,1,1))]. given #16 (W,wt=16): 62 (x + (x + (x + (x' + h(x)')))')' = h(x)'. [para(26(a,1),8(a,1,1,2)),rewrite([6(6),7(6),7(5),6(8)])]. given #17 (W,wt=17): 27 ((x + (y + z))' + (y + (x + z)')')' = y. [para(17(a,1),8(a,1,1,1,1))]. given #18 (W,wt=17): 31 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),18(a,1,1,1,1))]. given #19 (W,wt=17): 49 ((x + (y + z))' + ((x + z)' + y)')' = y. [para(17(a,1),19(a,1,1,1,1))]. given #20 (W,wt=17): 58 x + (y + ((x + x')' + z)) = y + (h(x) + z). [para(24(a,1),17(a,1,2)),flip(a)]. given #21 (W,wt=17): 67 x + (y + (z + (x + x')')) = y + (z + h(x)). [para(7(a,1),28(a,1,2)),rewrite([7(9)])]. given #22 (W,wt=17): 70 ((x + (y + z))' + ((x + y)' + z)')' = z. [para(7(a,1),29(a,1,1,1,1))]. given #23 (A,wt=20): 21 (x + ((x + y)' + (x + y')'')')' = (x + y)'. [para(8(a,1),8(a,1,1,1))]. given #24 (W,wt=17): 86 ((x + (y + z)')' + (y + (z + x))')' = x. [para(7(a,1),30(a,1,1,2,1))]. given #25 (W,wt=17): 102 (((x + y)' + z)' + (x + (z + y))')' = z. [para(17(a,1),42(a,1,1,2,1))]. given #26 (W,wt=17): 148 ((x + (y + z))' + (x + (z + y)')')' = x. [para(6(a,1),27(a,1,1,1,1)),rewrite([7(2)])]. given #27 (W,wt=17): 149 ((x + (y + z))' + (y + (z + x)')')' = y. [para(6(a,1),27(a,1,1,2,1,2,1))]. given #28 (W,wt=17): 150 ((x + (y + z)')' + (y + (x + z))')' = x. [para(6(a,1),27(a,1,1))]. given #29 (W,wt=17): 167 ((x + (y + z))' + (z + (y + x)')')' = z. [para(6(a,1),31(a,1,1,2,1,2,1))]. given #30 (W,wt=17): 176 ((x + (y + z))' + ((z + y)' + x)')' = x. [para(6(a,1),49(a,1,1,1,1)),rewrite([7(2)])]. given #31 (W,wt=17): 177 ((x + (y + z))' + ((z + x)' + y)')' = y. [para(6(a,1),49(a,1,1,2,1,1,1))]. given #32 (A,wt=21): 22 ((x + y)' + (x + ((y + z)' + (y + z')'))')' = x. [para(8(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #33 (W,wt=15): 346 ((x + x)' + (h(x) + (x + x)')')' = x. [para(28(a,1),22(a,1,1,2,1)),rewrite([6(6)])]. given #34 (W,wt=17): 198 ((x + (y + z))' + ((y + x)' + z)')' = z. [para(6(a,1),70(a,1,1,2,1,1,1))]. given #35 (W,wt=17): 246 ((x + (y + z)')' + (z + (y + x))')' = x. [para(6(a,1),86(a,1,1,1,1,2,1))]. given #36 (W,wt=17): 247 ((x + (y + z)')' + (z + (x + y))')' = x. [para(6(a,1),86(a,1,1,2,1)),rewrite([7(6)])]. given #37 (W,wt=17): 253 (((x + y)' + z)' + (y + (z + x))')' = z. [para(6(a,1),102(a,1,1,1,1,1,1))]. given #38 (W,wt=17): 254 (((x + y)' + z)' + (z + (y + x))')' = z. [para(6(a,1),102(a,1,1,2,1)),rewrite([7(6)])]. given #39 (W,wt=17): 340 ((x + x)' + (h(x) + (x + x'')')')' = x. [para(24(a,1),22(a,1,1,2,1))]. given #40 (W,wt=18): 23 (x + (x + (y' + (x + y)'))')' = (x + y)'. [para(8(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #41 (A,wt=19): 32 ((x + (y + z))' + (y + (z + x'))')' = y + z. [para(7(a,1),18(a,1,1,2,1))]. given #42 (W,wt=15): 435 (x + (h(x) + x'')')' = (x + x')'. [para(28(a,1),23(a,1,1,2,1)),rewrite([6(4)])]. given #43 (W,wt=17): 504 ((x + x')' + (x + (h(x) + x''))')' = x. [para(435(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #44 (W,wt=17): 528 (x + (h(x) + (h(x) + x''))')' = (x + x')'. [para(504(a,1),8(a,1,1,2)),rewrite([6(9),7(9),7(8),67(9),6(5),6(8)])]. given #45 (W,wt=18): 35 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(18(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #46 (W,wt=18): 46 (x + (y' + (x + (x + y)'))')' = (x + y)'. [para(19(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #47 (W,wt=18): 60 (x + (h(x)' + (x + (x + x'))'')')' = h(x)'. [para(26(a,1),8(a,1,1,1))]. given #48 (W,wt=18): 73 (x + (y' + (x + (y + x)'))')' = (y + x)'. [para(29(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #49 (W,wt=18): 129 (x + (x + (h(x)' + (x + x')''))')' = h(x)'. [para(25(a,1),8(a,1,1,2)),rewrite([17(8),6(10)])]. given #50 (A,wt=20): 33 (x + ((y + x)' + (x + y')'')')' = (y + x)'. [para(18(a,1),8(a,1,1,1))]. given #51 (W,wt=18): 140 (h(x)' + (x + (x + (x + (x' + h(x)'))))')' = x. [para(62(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #52 (W,wt=19): 38 (h(x)' + (x' + (x + x')')')' = (x + x')'. [para(10(a,1),18(a,1,1,1,1)),rewrite([6(7)])]. given #53 (W,wt=19): 39 ((x + (y + z))' + (x + (z + y'))')' = x + z. [para(17(a,1),18(a,1,1,1,1)),rewrite([7(6)])]. given #54 (W,wt=19): 43 ((x + (y + z))' + (z' + (x + y))')' = x + y. [para(7(a,1),19(a,1,1,1,1))]. given #55 (W,wt=19): 48 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #56 (W,wt=13): 846 (x + (x + h(x))')' = (x + x')'. [para(10(a,1),48(a,1,1,2,1,2))]. given #57 (W,wt=15): 923 ((x + (x + h(x)))' + (x + x')')' = x. [para(846(a,1),8(a,1,1,2))]. given #58 (W,wt=15): 958 (x + (x + (h(x) + h(x)))')' = (x + x')'. [para(846(a,1),48(a,1,1,2,1,2,2)),rewrite([7(6),28(6),846(12)])]. given #59 (A,wt=21): 34 ((x + y)' + (x + ((z + y)' + (y + z')'))')' = x. [para(18(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #60 (W,wt=17): 921 ((x + x')' + (x + (x + h(x))'')')' = x. [para(846(a,1),8(a,1,1,1))]. given #61 (W,wt=17): 947 (x + (h(x) + (x + h(x))'')')' = (x + x')'. [para(846(a,1),23(a,1,1,2,1,2,2)),rewrite([6(8),24(9),846(14)])]. given #62 (W,wt=17): 985 ((x + (x + (h(x) + h(x))))' + (x + x')')' = x. [para(958(a,1),8(a,1,1,2))]. given #63 (W,wt=17): 1018 (x + (x + (h(x) + (h(x) + h(x))))')' = (x + x')'. [para(958(a,1),48(a,1,1,2,1,2,2)),rewrite([7(8),7(7),67(8),958(16)])]. given #64 (W,wt=18): 1028 ((x + x')' + (h(x) + (x' + x')')')' = x. [para(24(a,1),34(a,1,1,2,1))]. given #65 (W,wt=19): 50 ((x + (y + z))' + (x + (z' + y))')' = x + y. [para(17(a,1),19(a,1,1,2,1)),rewrite([7(2)])]. given #66 (W,wt=19): 54 (x + (y + (x + (x + y')'))')' = (x + y')'. [para(18(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #67 (W,wt=19): 56 (x + (x + (y + (y' + x)'))')' = (y' + x)'. [para(19(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #68 (A,wt=21): 36 (x + ((x + y')' + (x + y)'')')' = (x + y')'. [para(8(a,1),18(a,1,1,1))]. given #69 (W,wt=19): 57 ((h(x) + y)' + (x + ((x + x')' + y)')')' = x. [para(24(a,1),8(a,1,1,1,1))]. given #70 (W,wt=17): 1487 ((x + x')' + (h(x) + (x + x)'')')' = x. [para(36(a,1),57(a,1,1,2)),rewrite([6(10)])]. given #71 (W,wt=19): 68 ((x + h(y))' + (y + (x + (y + y')')')')' = y. [para(28(a,1),8(a,1,1,1,1))]. given #72 (W,wt=17): 1541 ((x + x)' + (h(x) + (x + (x + h(x)))')')' = x. [para(923(a,1),68(a,1,1,2,1,2)),rewrite([6(6),6(10)])]. given #73 (W,wt=19): 75 ((x + (y + z))' + (y' + (x + z))')' = x + z. [para(17(a,1),29(a,1,1,1,1))]. given #74 (W,wt=19): 76 ((x + (y + z))' + (y + (x' + z))')' = y + z. [para(17(a,1),29(a,1,1,2,1))]. given #75 (W,wt=19): 81 (x + (y + (x + (y' + x)'))')' = (y' + x)'. [para(29(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #76 (W,wt=19): 85 ((x + (y + z'))' + (z + (x + y))')' = x + y. [para(7(a,1),30(a,1,1,1,1))]. given #77 (A,wt=21): 37 (((x + y)' + ((x + y')' + z))' + (z + x)')' = z. [para(8(a,1),18(a,1,1,2,1,2)),rewrite([7(7)])]. given #78 (W,wt=19): 89 ((x + (y + z'))' + (x + (z + y))')' = x + y. [para(17(a,1),30(a,1,1,2,1)),rewrite([7(3)])]. given #79 (W,wt=19): 98 ((x' + (y + z))' + (y + (z + x))')' = y + z. [para(7(a,1),42(a,1,1,2,1))]. given #80 (W,wt=19): 101 ((x + (y' + z))' + (x + (z + y))')' = x + z. [para(17(a,1),42(a,1,1,1,1)),rewrite([7(6)])]. given #81 (W,wt=19): 113 ((x + (y + z))' + (z + (x + y'))')' = z + x. [para(6(a,1),20(a,1,1,1,1)),rewrite([7(2)])]. given #82 (W,wt=19): 114 ((x + (y + z))' + (y + (z' + x))')' = x + y. [para(6(a,1),20(a,1,1,2,1)),rewrite([7(6)])]. given #83 (W,wt=19): 118 ((x + h(y))' + (x + (y + (y + y')))')' = x + y. [para(10(a,1),20(a,1,1,2,1,2)),rewrite([6(9)])]. given #84 (W,wt=19): 119 ((x + (y + z))' + (y + (x + z'))')' = y + x. [para(17(a,1),20(a,1,1,1,1))]. given #85 (W,wt=19): 126 ((x + h(y))' + (y + (x + (y + y')))')' = y + x. [para(28(a,1),20(a,1,1,2,1)),rewrite([6(9)])]. given #86 (A,wt=21): 40 (x + ((x + y')' + (y + x)'')')' = (x + y')'. [para(18(a,1),18(a,1,1,1))]. given #87 (W,wt=19): 263 ((h(x) + y)' + (x + (y + (x + x')')')')' = x. [para(24(a,1),148(a,1,1,1,1))]. given #88 (W,wt=19): 264 ((x + h(y))' + (y + ((y + y')' + x)')')' = y. [para(28(a,1),148(a,1,1,1,1))]. given #89 (W,wt=19): 276 (((x + x')' + (y + x))' + (y + h(x)')')' = y. [para(10(a,1),149(a,1,1,2,1,2,1))]. given #90 (W,wt=19): 312 ((h(x)' + y)' + ((x + x')' + (y + x))')' = y. [para(10(a,1),177(a,1,1,2,1,1,1)),rewrite([6(11)])]. given #91 (W,wt=19): 393 ((x + h(y)')' + ((y + y')' + (x + y))')' = x. [para(10(a,1),247(a,1,1,1,1,2,1))]. given #92 (W,wt=19): 482 ((x + (y + z))' + (z + (y + x'))')' = z + y. [para(6(a,1),32(a,1,1,1,1,2))]. given #93 (W,wt=19): 483 ((x + (y + z))' + (z + (x' + y))')' = y + z. [para(6(a,1),32(a,1,1,2,1)),rewrite([7(6)])]. given #94 (W,wt=19): 486 ((x + (x' + (y + x)))' + (y + h(x))')' = y + x. [para(10(a,1),32(a,1,1,2,1,2)),rewrite([7(4)])]. given #95 (A,wt=21): 41 (((x + y)' + ((y + x')' + z))' + (z + y)')' = z. [para(18(a,1),18(a,1,1,2,1,2)),rewrite([7(7)])]. given #96 (W,wt=19): 492 ((x + (x + (x' + y)))' + (y + h(x))')' = x + y. [para(28(a,1),32(a,1,1,2,1)),rewrite([17(4),7(3)])]. given #97 (W,wt=19): 502 ((x + x')' + (x + (h(x) + x'')'')')' = x. [para(435(a,1),8(a,1,1,1))]. given #98 (W,wt=19): 525 (x + (h(x) + (h(x) + x'')'')')' = (x + x')'. [para(435(a,1),23(a,1,1,2,1,2,2)),rewrite([6(10),24(11),435(18)])]. given #99 (W,wt=19): 548 ((x + x')' + (x + (h(x) + (h(x) + x'')))')' = x. [para(528(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #100 (W,wt=19): 792 ((x + (y + z))' + (x + (y' + z))')' = x + z. [para(6(a,1),39(a,1,1,2,1,2))]. given #101 (W,wt=19): 793 ((x + (y + z))' + (z + (y' + x))')' = x + z. [para(6(a,1),39(a,1,1,2,1)),rewrite([7(6)])]. given #102 (W,wt=19): 815 ((x + (y + z))' + (y' + (z + x))')' = z + x. [para(6(a,1),43(a,1,1,1,1)),rewrite([7(2)])]. given #103 (W,wt=19): 816 ((x + (y + z))' + (z' + (y + x))')' = x + y. [para(6(a,1),43(a,1,1,2,1,2))]. given #104 (A,wt=20): 44 (x + ((x + y)' + (y' + x)'')')' = (x + y)'. [para(19(a,1),8(a,1,1,1))]. given #105 (W,wt=19): 977 ((x + x')' + (h(x) + (x + (x + h(x)))'')')' = x. [para(923(a,1),35(a,1,1,2,1,2,2)),rewrite([6(12),17(13),24(13),923(22)])]. given #106 (W,wt=19): 983 ((x + x')' + (x + (x + (h(x) + h(x)))'')')' = x. [para(958(a,1),8(a,1,1,1))]. given #107 (W,wt=19): 1008 (x + (h(x) + (x + (h(x) + h(x)))'')')' = (x + x')'. [para(958(a,1),23(a,1,1,2,1,2,2)),rewrite([6(10),24(11),958(18)])]. given #108 (W,wt=19): 1090 ((x + x')' + (x + (h(x) + (x + h(x))''))')' = x. [para(921(a,1),48(a,1,1,2,1,2,2)),rewrite([6(12),17(13),17(12),24(12),921(24)])]. given #109 (W,wt=19): 1116 (x + (h(x) + (h(x) + (x + h(x))''))')' = (x + x')'. [para(947(a,1),48(a,1,1,2,1,2,2)),rewrite([6(10),17(10),58(11),947(20)])]. given #110 (W,wt=19): 1145 ((x + (x + (h(x) + (h(x) + h(x)))))' + (x + x')')' = x. [para(1018(a,1),8(a,1,1,2))]. given #111 (W,wt=19): 1206 ((x + (y + (x + x')))' + (h(x) + y)')' = x + y. [para(24(a,1),50(a,1,1,2,1))]. given #112 (W,wt=19): 1271 (x + (h(x) + (h(x) + (h(x) + x'')))')' = (x + x')'. [para(528(a,1),54(a,1,1,2,1,2,2)),rewrite([10(10),6(8),528(20)])]. given #113 (A,wt=21): 45 ((x + y)' + (x + ((y + z)' + (z' + y)'))')' = x. [para(19(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #114 (W,wt=19): 1289 (x + (x + (h(x) + (h(x) + (h(x) + h(x)))))')' = (x + x')'. [para(1018(a,1),54(a,1,1,2,1,2,2)),rewrite([10(10),6(8),17(8),1018(20)])]. given #115 (W,wt=19): 1458 ((x + x')' + (h(x) + (x + x'')'')')' = x. [para(21(a,1),57(a,1,1,2)),rewrite([6(12)])]. given #116 (W,wt=19): 1467 ((x + x)' + (h(x) + (x + (h(x) + x''))')')' = x. [para(504(a,1),57(a,1,1,2,1,2)),rewrite([6(12)])]. given #117 (W,wt=19): 1477 ((x + x)' + (h(x) + (x + (x + h(x))'')')')' = x. [para(921(a,1),57(a,1,1,2,1,2)),rewrite([6(12)])]. given #118 (W,wt=19): 1514 ((x + x')' + (h(x) + (h(x) + (x + x)''))')' = x. [para(1487(a,1),48(a,1,1,2,1,2,2)),rewrite([6(12),17(13),17(12),58(13),1487(24)])]. given #119 (W,wt=19): 1522 ((x + x)' + (h(x) + (h(x) + (x + x)'')')')' = x. [para(1487(a,1),57(a,1,1,2,1,2)),rewrite([6(12)])]. given #120 (W,wt=19): 1542 ((x + x)' + (h(x) + (x + (x + (h(x) + h(x))))')')' = x. [para(985(a,1),68(a,1,1,2,1,2)),rewrite([6(8),6(12)])]. given #121 (W,wt=19): 1582 ((x + (y + z))' + (x' + (z + y))')' = z + y. [para(6(a,1),75(a,1,1,1,1)),rewrite([7(2)])]. given #122 (A,wt=21): 47 ((x + ((y + z)' + (y + z')'))' + (y + x)')' = x. [para(8(a,1),19(a,1,1,2,1,1))]. given #123 (W,wt=19): 1583 ((x' + (y + z))' + (y + (x + z))')' = y + z. [para(6(a,1),75(a,1,1))]. given #124 (W,wt=19): 1618 ((x + (y' + z))' + (y + (x + z))')' = x + z. [para(6(a,1),76(a,1,1))]. given #125 (W,wt=19): 1623 ((h(x) + y)' + (x + (x + (x' + y)))')' = x + y. [para(24(a,1),76(a,1,1,2,1)),rewrite([17(4),7(3),6(9)])]. given #126 (W,wt=19): 1713 ((x + (y' + z))' + (y + (z + x))')' = z + x. [para(6(a,1),85(a,1,1,1,1)),rewrite([7(3)])]. given #127 (W,wt=19): 1714 ((x + (y + z'))' + (z + (y + x))')' = x + y. [para(6(a,1),85(a,1,1,2,1,2))]. given #128 (W,wt=19): 1715 ((x + h(y))' + (y + (y' + (x + y)))')' = x + y. [para(10(a,1),85(a,1,1,1,1,2)),rewrite([7(7)])]. given #129 (W,wt=19): 1717 ((x + h(y))' + (y + (y + (y' + x)))')' = y + x. [para(28(a,1),85(a,1,1,1,1)),rewrite([17(7),7(6)])]. given #130 (W,wt=19): 1832 ((x + (y' + z))' + (z + (y + x))')' = z + x. [para(6(a,1),89(a,1,1,1,1)),rewrite([7(3)])]. given #131 (A,wt=21): 51 (x + ((y' + x)' + (x + y)'')')' = (y' + x)'. [para(19(a,1),18(a,1,1,1))]. given #132 (W,wt=19): 1833 ((x + (y + z'))' + (y + (z + x))')' = y + x. [para(17(a,1),89(a,1,1,1,1))]. given #133 (W,wt=19): 1858 ((x' + (y + z))' + (z + (y + x))')' = z + y. [para(6(a,1),98(a,1,1,1,1,2))]. given #134 (W,wt=19): 1859 ((x' + (y + z))' + (z + (x + y))')' = y + z. [para(6(a,1),98(a,1,1,2,1)),rewrite([7(6)])]. given #135 (W,wt=19): 1889 ((x + (y' + z))' + (z + (x + y))')' = x + z. [para(17(a,1),101(a,1,1,2,1))]. given #136 (W,wt=19): 1890 ((h(x) + y)' + (x + (y + (x + x')))')' = x + y. [para(24(a,1),101(a,1,1,1,1))]. given #137 (W,wt=19): 1917 (((x + x')' + (y + x))' + (h(x) + y')')' = h(x). [para(10(a,1),113(a,2)),rewrite([24(12)])]. given #138 (W,wt=19): 1955 ((h(x) + y)' + ((x + x')' + (y' + x))')' = h(x). [para(10(a,1),114(a,2)),rewrite([24(5)])]. given #139 (W,wt=19): 1958 ((x + (y + (y + y')))' + (h(y) + x)')' = x + y. [para(24(a,1),114(a,1,1,2,1))]. given #140 (A,wt=21): 52 (((x + y)' + ((y' + x)' + z))' + (z + x)')' = z. [para(19(a,1),18(a,1,1,2,1,2)),rewrite([7(7)])]. given #141 (W,wt=19): 1991 ((h(x) + y)' + (y + (x + (x + x')))')' = y + x. [para(6(a,1),118(a,1,1,1,1))]. given #142 (W,wt=19): 2025 ((x + (y + z'))' + (y + (x + z))')' = x + y. [para(6(a,1),119(a,1,1))]. given #143 (W,wt=19): 2064 ((x + h(y))' + (y + (y + (x + y')))')' = y + x. [para(17(a,1),126(a,1,1,2,1,2))]. given #144 (W,wt=19): 2333 ((x + h(y))' + ((y + y')' + (x' + y))')' = h(y). [para(10(a,1),483(a,1,1,1,1,2)),rewrite([10(16)])]. given #145 (W,wt=19): 2337 ((h(x) + y)' + (x + (x' + (y + x)))')' = y + x. [para(24(a,1),483(a,1,1,2,1)),rewrite([7(4),6(9)])]. given #146 (W,wt=19): 2663 (((x + x')' + (y + x))' + (y' + h(x))')' = h(x). [para(28(a,1),793(a,1,1,2,1)),rewrite([6(16),10(16)])]. given #147 (W,wt=19): 3091 ((x + (x + (y + x')))' + (h(x) + y)')' = x + y. [para(17(a,1),1206(a,1,1,1,1,2))]. given #148 (W,wt=19): 3620 ((x' + (y + z))' + (x + (z + y))')' = y + z. [para(6(a,1),1582(a,1,1))]. given #149 (A,wt=21): 53 ((x + ((y + z)' + (z + y')'))' + (z + x)')' = x. [para(18(a,1),19(a,1,1,2,1,1))]. given #150 (W,wt=19): 3909 ((h(x) + y)' + (x + (x + (y + x')))')' = x + y. [para(6(a,1),1623(a,1,1,2,1,2,2))]. given #151 (W,wt=19): 4052 ((x' + h(y))' + ((y + y')' + (x + y))')' = h(y). [para(28(a,1),1832(a,1,1,1,1)),rewrite([6(16),10(16)])]. given #152 (W,wt=19): 4205 ((h(x) + y')' + ((x + x')' + (y + x))')' = h(x). [para(24(a,1),1833(a,1,1,1,1)),rewrite([6(16),10(16)])]. given #153 (W,wt=20): 71 (x + ((y + x)' + (y' + x)'')')' = (y + x)'. [para(29(a,1),8(a,1,1,1))]. given #154 (W,wt=20): 127 (x + (h(x)' + (x + (x + x')'')'')')' = h(x)'. [para(25(a,1),8(a,1,1,1))]. given #155 (W,wt=20): 138 (h(x)' + (x + (x + (x + (x' + h(x)')))'')')' = x. [para(62(a,1),8(a,1,1,1))]. given #156 (W,wt=20): 370 (x + (h(x) + ((x + x)' + (x + x)'))')' = (x + x)'. [para(346(a,1),8(a,1,1,2)),rewrite([17(7),6(9)])]. given #157 (W,wt=20): 423 ((x + y)' + (x + (x + (y' + (x + y)')))')' = x. [para(23(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #158 (A,wt=21): 55 ((x + ((y + z)' + (z' + y)'))' + (y + x)')' = x. [para(19(a,1),19(a,1,1,2,1,1))]. given #159 (W,wt=20): 433 (h(x)' + (x + (h(x)' + (x + (x + x'))''))')' = x. [para(26(a,1),23(a,1,1,2,1,2,2)),rewrite([6(10),17(11),26(22)])]. given #160 (W,wt=20): 569 ((x + y)' + (y + (y + (x' + (x + y)')))')' = y. [para(35(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #161 (W,wt=20): 616 ((x + y)' + (x + (y' + (x + (x + y)')))')' = x. [para(46(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #162 (W,wt=20): 630 ((x + y)' + (y' + (x + (x + (x + y)')))')' = x. [para(46(a,1),27(a,1,1,2)),rewrite([6(10)])]. given #163 (W,wt=20): 667 ((x + y)' + (y + (x' + (y + (x + y)')))')' = y. [para(73(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #164 (W,wt=20): 683 ((x + y)' + (x' + (y + (y + (x + y)')))')' = y. [para(73(a,1),27(a,1,1,2)),rewrite([6(10)])]. given #165 (W,wt=20): 698 (h(x)' + (x + (x + (h(x)' + (x + x')'')))')' = x. [para(129(a,1),8(a,1,1,2)),rewrite([6(13)])]. given #166 (W,wt=20): 924 ((x + x')' + (x' + (x + h(x))')')' = (x + h(x))'. [para(846(a,1),18(a,1,1,1)),rewrite([6(8)])]. given #167 (A,wt=25): 59 ((h(x) + y)' + (x' + ((x + x')' + y))')' = (x + x')' + y. [para(24(a,1),18(a,1,1,1,1)),rewrite([6(9)])]. given #168 (W,wt=20): 1200 ((x + x')' + (h(x) + (h(x) + (x' + x')'))')' = x. [para(1028(a,1),48(a,1,1,2,1,2,2)),rewrite([6(13),17(14),17(13),58(14),1028(26)])]. given #169 (W,wt=20): 1478 ((x + x)' + (h(x) + (h(x) + (x' + x')')')')' = x. [para(1028(a,1),57(a,1,1,2,1,2)),rewrite([6(13)])]. given #170 (W,wt=20): 5516 ((x + y)' + (y + (y + (x' + (y + x)')))')' = y. [para(6(a,1),423(a,1,1,1,1))]. given #171 (W,wt=20): 5517 ((x + y)' + (x + (x + (y' + (y + x)')))')' = x. [para(6(a,1),423(a,1,1,2,1,2,2,2,1))]. given #172 (W,wt=20): 5814 ((x + y)' + (y + (x' + (y + (y + x)')))')' = y. [para(6(a,1),616(a,1,1,1,1))]. given #173 (W,wt=20): 5815 ((x + y)' + (x + (y' + (x + (y + x)')))')' = x. [para(6(a,1),616(a,1,1,2,1,2,2,2,1))]. given #174 (W,wt=20): 5851 ((x + y)' + (x' + (y + (y + (y + x)')))')' = y. [para(6(a,1),630(a,1,1,1,1))]. given #175 (W,wt=20): 5852 ((x + y)' + (y' + (x + (x + (y + x)')))')' = x. [para(6(a,1),630(a,1,1,2,1,2,2,2,1))]. given #176 (A,wt=21): 61 ((x + y)' + (x + (h(y)' + (y + (y + y'))'))')' = x. [para(26(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])]. given #177 (W,wt=20): 6052 ((x + x')' + (h(x) + (x' + (x + h(x))')')')' = x. [para(924(a,1),57(a,1,1,2,1,2)),rewrite([846(14),6(13)])]. given #178 (W,wt=21): 64 ((h(x)' + ((x + (x + x'))' + y))' + (y + x)')' = y. [para(26(a,1),18(a,1,1,2,1,2)),rewrite([7(8)])]. given #179 (W,wt=21): 65 ((x + (h(y)' + (y + (y + y'))'))' + (y + x)')' = x. [para(26(a,1),19(a,1,1,2,1,1))]. given #180 (W,wt=21): 66 (x + (h(x) + (x + (x + x'))')')' = (x + (x + x'))'. [para(26(a,1),19(a,1,1,2)),rewrite([6(6),6(8)])]. given #181 (W,wt=21): 72 ((x + y)' + (x + ((z + y)' + (z' + y)'))')' = x. [para(29(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #182 (W,wt=21): 74 ((x + y)' + ((x + z)' + ((x + z')' + y))')' = y. [para(8(a,1),29(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #183 (W,wt=21): 77 (x + ((y' + x)' + (y + x)'')')' = (y' + x)'. [para(29(a,1),18(a,1,1,1))]. given #184 (W,wt=21): 78 (((x + y)' + ((x' + y)' + z))' + (z + y)')' = z. [para(29(a,1),18(a,1,1,2,1,2)),rewrite([7(7)])]. given #185 (A,wt=23): 63 (x + ((x + (x + x'))' + h(x)'')')' = (x + (x + x'))'. [para(26(a,1),18(a,1,1,1))]. given #186 (W,wt=21): 79 ((x + y)' + ((z + x)' + ((x + z')' + y))')' = y. [para(18(a,1),29(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #187 (W,wt=21): 80 ((x + ((y + z)' + (y' + z)'))' + (z + x)')' = x. [para(29(a,1),19(a,1,1,2,1,1))]. given #188 (W,wt=21): 82 ((x + y)' + ((x + z)' + ((z' + x)' + y))')' = y. [para(19(a,1),29(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #189 (W,wt=21): 83 ((x + y)' + (h(x)' + ((x + (x + x'))' + y))')' = y. [para(26(a,1),29(a,1,1,2,1,1)),rewrite([7(8),6(12)])]. given #190 (W,wt=21): 84 ((x + y)' + ((z + x)' + ((z' + x)' + y))')' = y. [para(29(a,1),29(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #191 (W,wt=21): 87 ((x + y)' + (x + ((y + z')' + (z + y)'))')' = x. [para(30(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #192 (W,wt=21): 88 ((x + y)' + ((y + z)' + ((y + z')' + x))')' = x. [para(8(a,1),30(a,1,1,1,1,2)),rewrite([7(9)])]. given #193 (W,wt=21): 90 (((x + y')' + ((y + x)' + z))' + (z + x)')' = z. [para(30(a,1),18(a,1,1,2,1,2)),rewrite([7(7)])]. given #194 (A,wt=25): 69 ((x + h(y))' + (y' + (x + (y + y')'))')' = x + (y + y')'. [para(28(a,1),18(a,1,1,1,1)),rewrite([6(9)])]. given #195 (W,wt=21): 91 ((x + y)' + ((z + y)' + ((y + z')' + x))')' = x. [para(18(a,1),30(a,1,1,1,1,2)),rewrite([7(9)])]. given #196 (W,wt=21): 92 ((x + ((y + z')' + (z + y)'))' + (y + x)')' = x. [para(30(a,1),19(a,1,1,2,1,1))]. given #197 (W,wt=21): 93 ((x + y)' + ((y + z)' + ((z' + y)' + x))')' = x. [para(19(a,1),30(a,1,1,1,1,2)),rewrite([7(9)])]. given #198 (W,wt=21): 94 ((x + y)' + (h(y)' + ((y + (y + y'))' + x))')' = x. [para(26(a,1),30(a,1,1,1,1,2)),rewrite([7(10)])]. given #199 (W,wt=21): 95 ((x + y)' + ((x + z')' + ((z + x)' + y))')' = y. [para(30(a,1),29(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #200 (W,wt=21): 96 ((x + y)' + ((z + y)' + ((z' + y)' + x))')' = x. [para(29(a,1),30(a,1,1,1,1,2)),rewrite([7(9)])]. given #201 (W,wt=21): 97 ((x + y)' + ((y + z')' + ((z + y)' + x))')' = x. [para(30(a,1),30(a,1,1,1,1,2)),rewrite([7(9)])]. given #202 (W,wt=21): 99 ((x + y)' + (x + ((z' + y)' + (y + z)'))')' = x. [para(42(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #203 (A,wt=21): 100 ((x + y)' + (y + ((x + z)' + (x + z')'))')' = y. [para(8(a,1),42(a,1,1,1,1,1))]. given #204 (W,wt=21): 103 (((x' + y)' + ((y + x)' + z))' + (z + y)')' = z. [para(42(a,1),18(a,1,1,2,1,2)),rewrite([7(7)])]. given #205 (W,wt=21): 104 ((x + y)' + (y + ((z + x)' + (x + z')'))')' = y. [para(18(a,1),42(a,1,1,1,1,1))]. given #206 (W,wt=21): 105 ((x + ((y' + z)' + (z + y)'))' + (z + x)')' = x. [para(42(a,1),19(a,1,1,2,1,1))]. given #207 (W,wt=21): 106 ((x + y)' + (y + ((x + z)' + (z' + x)'))')' = y. [para(19(a,1),42(a,1,1,1,1,1))]. given #208 (W,wt=21): 107 ((x + y)' + (y + (h(x)' + (x + (x + x'))'))')' = y. [para(26(a,1),42(a,1,1,1,1,1))]. given #209 (W,wt=21): 108 ((x + y)' + ((z' + x)' + ((x + z)' + y))')' = y. [para(42(a,1),29(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #210 (W,wt=21): 109 ((x + y)' + (y + ((z + x)' + (z' + x)'))')' = y. [para(29(a,1),42(a,1,1,1,1,1))]. given #211 (W,wt=21): 110 ((x + y)' + ((z' + y)' + ((y + z)' + x))')' = x. [para(42(a,1),30(a,1,1,1,1,2)),rewrite([7(9)])]. given #212 (A,wt=21): 111 ((x + y)' + (y + ((x + z')' + (z + x)'))')' = y. [para(30(a,1),42(a,1,1,1,1,1))]. given #213 (W,wt=21): 112 ((x + y)' + (y + ((z' + x)' + (x + z)'))')' = y. [para(42(a,1),42(a,1,1,1,1,1))]. given #214 (W,wt=21): 117 ((x + h(y))' + (x + (y + (y + y')''))')' = x + y. [para(10(a,1),20(a,1,1,1,1,2))]. given #215 (W,wt=21): 125 ((x + h(y))' + (y + (x + (y + y')''))')' = y + x. [para(28(a,1),20(a,1,1,1,1))]. given #216 (W,wt=21): 153 ((x + y)' + ((y + z)' + (x + (y + z')'))')' = x. [para(8(a,1),27(a,1,1,2,1,2)),rewrite([6(11)])]. given #217 (W,wt=21): 155 ((x + y)' + ((z + y)' + (x + (y + z')'))')' = x. [para(18(a,1),27(a,1,1,2,1,2)),rewrite([6(11)])]. given #218 (W,wt=21): 157 ((x + y)' + ((y + z)' + (x + (z' + y)'))')' = x. [para(19(a,1),27(a,1,1,2,1,2)),rewrite([6(11)])]. given #219 (W,wt=21): 160 ((x + y)' + (h(y)' + (x + (y + (y + y'))'))')' = x. [para(26(a,1),27(a,1,1,2,1,2)),rewrite([6(12)])]. given #220 (W,wt=21): 162 ((x + y)' + ((z + y)' + (x + (z' + y)'))')' = x. [para(29(a,1),27(a,1,1,2,1,2)),rewrite([6(11)])]. given #221 (A,wt=28): 115 (x + (y + ((x + (y + z))' + (x + (y + z'))'')'))' = (x + (y + z))'. [para(20(a,1),8(a,1,1,1)),rewrite([7(12)])]. given #222 (W,wt=21): 163 ((x + y)' + ((y + z')' + (x + (z + y)'))')' = x. [para(30(a,1),27(a,1,1,2,1,2)),rewrite([6(11)])]. given #223 (W,wt=21): 164 ((x + y)' + ((z' + y)' + (x + (y + z)'))')' = x. [para(42(a,1),27(a,1,1,2,1,2)),rewrite([6(11)])]. given #224 (W,wt=21): 180 ((x + y)' + ((x + z)' + (y + (x + z')'))')' = y. [para(8(a,1),49(a,1,1,2,1,1)),rewrite([6(11)])]. given #225 (W,wt=21): 182 ((x + y)' + ((z + x)' + (y + (x + z')'))')' = y. [para(18(a,1),49(a,1,1,2,1,1)),rewrite([6(11)])]. given #226 (W,wt=21): 184 ((x + y)' + ((x + z)' + (y + (z' + x)'))')' = y. [para(19(a,1),49(a,1,1,2,1,1)),rewrite([6(11)])]. given #227 (W,wt=21): 186 ((x + y)' + (h(x)' + (y + (x + (x + x'))'))')' = y. [para(26(a,1),49(a,1,1,2,1,1)),rewrite([6(12)])]. given #228 (W,wt=21): 187 ((x + y)' + ((z + x)' + (y + (z' + x)'))')' = y. [para(29(a,1),49(a,1,1,2,1,1)),rewrite([6(11)])]. given #229 (W,wt=21): 188 ((x + y)' + ((x + z')' + (y + (z + x)'))')' = y. [para(30(a,1),49(a,1,1,2,1,1)),rewrite([6(11)])]. given #230 (A,wt=26): 116 (x + (y + (x + (y + (z' + (x + (y + z))')))'))' = (x + (y + z))'. [para(20(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(10),7(10)])]. given #231 (W,wt=21): 189 ((x + y)' + ((z' + x)' + (y + (x + z)'))')' = y. [para(42(a,1),49(a,1,1,2,1,1)),rewrite([6(11)])]. given #232 (W,wt=21): 275 ((x + y)' + ((y + z')' + (x + (y + z)'))')' = x. [para(8(a,1),149(a,1,1,2,1,2)),rewrite([6(11)])]. given #233 (W,wt=21): 281 ((x + y)' + ((y + (y + y'))' + (x + h(y)'))')' = x. [para(26(a,1),149(a,1,1,2,1,2)),rewrite([6(12)])]. given #234 (W,wt=21): 284 ((x + y)' + ((z' + y)' + (x + (z + y)'))')' = x. [para(29(a,1),149(a,1,1,2,1,2)),rewrite([6(11)])]. given #235 (W,wt=21): 311 ((x + y)' + ((x + z')' + (y + (x + z)'))')' = y. [para(8(a,1),177(a,1,1,2,1,1)),rewrite([6(11)])]. given #236 (W,wt=21): 316 ((x + y)' + ((x + (x + x'))' + (y + h(x)'))')' = y. [para(26(a,1),177(a,1,1,2,1,1)),rewrite([6(12)])]. given #237 (W,wt=21): 319 ((x + y)' + ((z' + x)' + (y + (z + x)'))')' = y. [para(29(a,1),177(a,1,1,2,1,1)),rewrite([6(11)])]. given #238 (W,wt=21): 545 ((x + x')' + (h(x) + (x + (h(x) + x''))'')')' = x. [para(504(a,1),23(a,1,1,2,1,2,2)),rewrite([6(14),17(15),24(15),504(26)])]. given #239 (A,wt=29): 120 (x + (y + ((x + (y + z'))' + (x + (y + z))'')'))' = (x + (y + z'))'. [para(20(a,1),18(a,1,1,1)),rewrite([7(12)])]. given #240 (W,wt=21): 547 ((x + x')' + (x + (h(x) + (h(x) + x''))'')')' = x. [para(528(a,1),8(a,1,1,1))]. given #241 (W,wt=21): 566 (x + (h(x) + (h(x) + (h(x) + x''))'')')' = (x + x')'. [para(528(a,1),23(a,1,1,2,1,2,2)),rewrite([6(12),24(13),528(22)])]. given #242 (W,wt=21): 752 (x + (x + (x + (x + (x' + (h(x)' + h(x)')))))')' = h(x)'. [para(140(a,1),8(a,1,1,2)),rewrite([17(10),17(9),17(8),17(7),6(12)])]. given #243 (W,wt=21): 796 ((h(x) + y)' + (x + (y + (x + x')''))')' = x + y. [para(24(a,1),39(a,1,1,1,1))]. given #244 (W,wt=21): 818 ((x + h(y))' + ((y + y')'' + (x + y))')' = x + y. [para(10(a,1),43(a,1,1,1,1,2))]. given #245 (W,wt=21): 824 ((x + h(y))' + (y + ((y + y')'' + x))')' = y + x. [para(28(a,1),43(a,1,1,1,1)),rewrite([17(9)])]. given #246 (W,wt=21): 845 ((x + y')' + (x + (x + (y + (x + y')')))')' = x. [para(48(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #247 (W,wt=21): 857 ((x + y')' + (x + (y + (x + (x + y')')))')' = x. [para(30(a,1),48(a,1,1,2,1,2,2)),rewrite([6(8),6(9),7(9),7(8),30(19)])]. given #248 (A,wt=27): 121 (x + (y + (x + (y + (z + (x + (y + z'))')))'))' = (x + (y + z'))'. [para(20(a,1),19(a,1,1,2)),rewrite([6(7),7(7),7(6),6(10),7(10)])]. given #249 (W,wt=21): 860 ((x' + y)' + (y + (y + (x + (x' + y)')))')' = y. [para(42(a,1),48(a,1,1,2,1,2,2)),rewrite([6(8),6(9),7(9),7(8),42(19)])]. given #250 (W,wt=21): 922 ((x + (y + (y + h(y))'))' + (x + (y + y')')')' = x. [para(846(a,1),8(a,1,1,2,1,2))]. given #251 (W,wt=15): 11677 (h(x)' + (x + (x + (x + h(x))'))')' = x. [para(10(a,1),922(a,1,1,2,1)),rewrite([6(9)])]. given #252 (W,wt=18): 11696 (x + (x + (x + (h(x)' + (x + h(x))')))')' = h(x)'. [para(11677(a,1),8(a,1,1,2)),rewrite([17(8),17(7),6(10)])]. given #253 (W,wt=20): 11676 (x + (x + ((x + x)' + (x + h(x))'))')' = (x + x)'. [para(8(a,1),922(a,1,1,2)),rewrite([17(7),6(9)])]. given #254 (W,wt=20): 11694 (x + (h(x)' + (x + (x + (x + h(x))'))'')')' = h(x)'. [para(11677(a,1),8(a,1,1,1))]. given #255 (W,wt=20): 11721 (h(x)' + (x + (x + (x + (h(x)' + (x + h(x))'))))')' = x. [para(11677(a,1),48(a,1,1,2,1,2,2)),rewrite([6(10),17(11),17(10),17(9),11677(24)])]. given #256 (W,wt=21): 925 ((x + ((x + h(x))' + y))' + (y + (x + x')')')' = y. [para(846(a,1),18(a,1,1,2,1,2)),rewrite([7(5)])]. given #257 (A,wt=25): 122 ((x + (h(y) + z))' + (x + (y + ((y + y')' + z)'))')' = x + y. [para(24(a,1),20(a,1,1,1,1,2))]. given #258 (W,wt=21): 926 ((x + (y + (y + h(y))'))' + ((y + y')' + x)')' = x. [para(846(a,1),19(a,1,1,2,1,1))]. given #259 (W,wt=21): 927 ((x + ((x + h(x))' + y))' + ((x + x')' + y)')' = y. [para(846(a,1),29(a,1,1,2,1,1)),rewrite([7(5)])]. given #260 (W,wt=21): 928 ((x + (y + y')')' + (y + ((y + h(y))' + x))')' = x. [para(846(a,1),30(a,1,1,1,1,2)),rewrite([7(10)])]. given #261 (W,wt=21): 929 (((x + x')' + y)' + (y + (x + (x + h(x))'))')' = y. [para(846(a,1),42(a,1,1,1,1,1))]. given #262 (W,wt=21): 931 ((x + (y + (x + h(x))'))' + (y + (x + x')')')' = y. [para(846(a,1),27(a,1,1,2,1,2))]. given #263 (W,wt=21): 932 ((x + (y + (x + h(x))'))' + ((x + x')' + y)')' = y. [para(846(a,1),49(a,1,1,2,1,1))]. given #264 (W,wt=21): 936 (((x + x')' + y)' + (x + (y + (x + h(x))'))')' = y. [para(846(a,1),102(a,1,1,1,1,1))]. given #265 (W,wt=21): 937 (((x + h(x))' + (y + x))' + (y + (x + x')')')' = y. [para(846(a,1),149(a,1,1,2,1,2))]. given #266 (A,wt=27): 123 ((x + (y + z))' + (x + (y + (h(z)' + (z + (z + z'))')))')' = x + y. [para(26(a,1),20(a,1,1,2,1,2,2)),rewrite([6(14)])]. given #267 (W,wt=21): 938 ((x + (y + y')')' + (y + (x + (y + h(y))'))')' = x. [para(846(a,1),150(a,1,1,1,1,2))]. given #268 (W,wt=21): 939 (((x + h(x))' + (y + x))' + ((x + x')' + y)')' = y. [para(846(a,1),177(a,1,1,2,1,1))]. given #269 (W,wt=21): 944 ((x + (y + y')')' + ((y + h(y))' + (x + y))')' = x. [para(846(a,1),247(a,1,1,1,1,2))]. given #270 (W,wt=21): 945 (((x + x')' + y)' + ((x + h(x))' + (y + x))')' = y. [para(846(a,1),253(a,1,1,1,1,1))]. given #271 (W,wt=21): 1083 ((x + x')' + (h(x) + (x + (x + h(x))'')'')')' = x. [para(921(a,1),23(a,1,1,2,1,2,2)),rewrite([6(14),17(15),24(15),921(26)])]. given #272 (W,wt=21): 1092 ((x + x')' + (x + (h(x) + (x + h(x))'')'')')' = x. [para(947(a,1),8(a,1,1,1))]. given #273 (W,wt=21): 1110 (x + (h(x) + (h(x) + (x + h(x))'')'')')' = (x + x')'. [para(947(a,1),23(a,1,1,2,1,2,2)),rewrite([6(12),24(13),947(22)])]. given #274 (W,wt=21): 1135 ((x + x')' + (h(x) + (x + (x + (h(x) + h(x))))'')')' = x. [para(985(a,1),35(a,1,1,2,1,2,2)),rewrite([6(14),17(15),24(15),985(26)])]. given #275 (A,wt=25): 124 ((x + (y + h(z)))' + (x + (z + (y + (z + z')')'))')' = x + z. [para(28(a,1),20(a,1,1,1,1,2))]. given #276 (W,wt=21): 1143 ((x + x')' + (x + (x + (h(x) + (h(x) + h(x))))'')')' = x. [para(1018(a,1),8(a,1,1,1))]. given #277 (W,wt=21): 1166 (x + (h(x) + (x + (h(x) + (h(x) + h(x))))'')')' = (x + x')'. [para(1018(a,1),23(a,1,1,2,1,2,2)),rewrite([6(12),24(13),1018(22)])]. given #278 (W,wt=21): 1248 ((x + y')' + (y + (x + (x + (x + y')')))')' = x. [para(54(a,1),27(a,1,1,2)),rewrite([6(11)])]. given #279 (W,wt=21): 1303 ((x' + y)' + (y + (x + (y + (x' + y)')))')' = y. [para(29(a,1),56(a,1,1,2,1,2,2)),rewrite([6(8),6(9),7(9),7(8),29(19)])]. given #280 (W,wt=21): 1507 ((x + x')' + (h(x) + (h(x) + (x + x)'')'')')' = x. [para(1487(a,1),23(a,1,1,2,1,2,2)),rewrite([6(14),17(15),24(15),1487(26)])]. given #281 (W,wt=21): 1587 ((h(x) + y)' + (x + ((x + x')'' + y))')' = x + y. [para(24(a,1),75(a,1,1,1,1)),rewrite([17(9)])]. given #282 (W,wt=21): 1674 ((x' + y)' + (x + (y + (y + (x' + y)')))')' = y. [para(81(a,1),27(a,1,1,2)),rewrite([6(11)])]. given #283 (W,wt=21): 1834 ((x + (y + (x + x')''))' + (h(x) + y)')' = x + y. [para(24(a,1),89(a,1,1,2,1))]. given #284 (A,wt=23): 128 ((x + y)' + (x + (h(y)' + (y + (y + y')'')'))')' = x. [para(25(a,1),8(a,1,1,2,1,2)),rewrite([6(14)])]. given #285 (W,wt=21): 1860 (((x + x')'' + (y + x))' + (y + h(x))')' = y + x. [para(10(a,1),98(a,1,1,2,1,2))]. given #286 (W,wt=21): 1864 ((x + ((x + x')'' + y))' + (y + h(x))')' = x + y. [para(28(a,1),98(a,1,1,2,1)),rewrite([17(6)])]. given #287 (W,wt=21): 1920 ((h(x) + y)' + (y + (x + (x + x')''))')' = y + x. [para(24(a,1),113(a,1,1,1,1))]. given #288 (W,wt=21): 2508 ((x + x')' + (x + (h(x) + (h(x) + x'')''))')' = x. [para(502(a,1),48(a,1,1,2,1,2,2)),rewrite([6(14),17(15),17(14),24(14),502(28)])]. given #289 (W,wt=21): 2516 ((x + x)' + (h(x) + (x + (h(x) + x'')'')')')' = x. [para(502(a,1),57(a,1,1,2,1,2)),rewrite([6(14)])]. given #290 (W,wt=21): 2553 (x + (h(x) + (h(x) + (h(x) + x'')''))')' = (x + x')'. [para(525(a,1),48(a,1,1,2,1,2,2)),rewrite([6(12),17(12),58(13),525(24)])]. given #291 (W,wt=21): 2596 ((x + x')' + (x + (h(x) + (h(x) + (h(x) + x''))))')' = x. [para(548(a,1),54(a,1,1,2,1,2,2)),rewrite([6(14),10(14),6(12),17(12),548(28)])]. given #292 (W,wt=21): 2601 ((x + x)' + (h(x) + (x + (h(x) + (h(x) + x'')))')')' = x. [para(548(a,1),57(a,1,1,2,1,2)),rewrite([6(14)])]. given #293 (A,wt=27): 130 (x + (h(x)'' + (x + (x + x')'')')')' = (x + (x + x')'')'. [para(25(a,1),18(a,1,1,1)),rewrite([6(10)])]. given #294 (W,wt=21): 2702 ((h(x) + y)' + ((x + x')'' + (y + x))')' = y + x. [para(24(a,1),815(a,1,1,1,1))]. given #295 (W,wt=21): 2822 ((x + x')' + (h(x) + (h(x) + (x + (x + h(x)))''))')' = x. [para(977(a,1),48(a,1,1,2,1,2,2)),rewrite([6(14),17(15),17(14),58(15),977(28)])]. given #296 (W,wt=21): 2830 ((x + x)' + (h(x) + (h(x) + (x + (x + h(x)))'')')')' = x. [para(977(a,1),57(a,1,1,2,1,2)),rewrite([6(14)])]. given #297 (W,wt=21): 2873 ((x + x')' + (x + (h(x) + (x + (h(x) + h(x)))''))')' = x. [para(983(a,1),48(a,1,1,2,1,2,2)),rewrite([6(14),17(15),17(14),24(14),983(28)])]. given #298 (W,wt=21): 2881 ((x + x)' + (h(x) + (x + (x + (h(x) + h(x)))'')')')' = x. [para(983(a,1),57(a,1,1,2,1,2)),rewrite([6(14)])]. given #299 (W,wt=21): 2922 (x + (h(x) + (h(x) + (x + (h(x) + h(x)))''))')' = (x + x')'. [para(1008(a,1),48(a,1,1,2,1,2,2)),rewrite([6(12),17(12),58(13),1008(24)])]. given #300 (W,wt=21): 2966 ((x + x')' + (x + (h(x) + (h(x) + (x + h(x))'')))')' = x. [para(1090(a,1),48(a,1,1,2,1,2,2)),rewrite([6(14),17(15),17(14),17(13),58(14),1090(28)])]. given #301 (W,wt=21): 2974 ((x + x)' + (h(x) + (x + (h(x) + (x + h(x))''))')')' = x. [para(1090(a,1),57(a,1,1,2,1,2)),rewrite([6(14)])]. given #302 (A,wt=23): 131 ((h(x)' + ((x + (x + x')'')' + y))' + (y + x)')' = y. [para(25(a,1),18(a,1,1,2,1,2)),rewrite([7(10)])]. given #303 (W,wt=21): 3018 (x + (h(x) + (h(x) + (h(x) + (x + h(x))'')))')' = (x + x')'. [para(1116(a,1),54(a,1,1,2,1,2,2)),rewrite([10(12),6(10),1116(24)])]. given #304 (W,wt=21): 3066 ((x + x)' + (h(x) + (x + (x + (h(x) + (h(x) + h(x)))))')')' = x. [para(1145(a,1),68(a,1,1,2,1,2)),rewrite([6(10),6(14)])]. given #305 (W,wt=21): 3070 ((x + (x + (h(x) + (h(x) + (h(x) + h(x))))))' + (x + x')')' = x. [para(1145(a,1),81(a,1,1,2,1,2,2)),rewrite([6(14),10(14),6(12),17(12),17(11),6(14),1145(28)])]. given #306 (W,wt=21): 3150 (x + (h(x) + (h(x) + (h(x) + (h(x) + x''))))')' = (x + x')'. [para(1271(a,1),54(a,1,1,2,1,2,2)),rewrite([10(12),6(10),1271(24)])]. given #307 (W,wt=21): 3265 (x + (x + (h(x) + (h(x) + (h(x) + (h(x) + h(x))))))')' = (x + x')'. [para(1289(a,1),54(a,1,1,2,1,2,2)),rewrite([10(12),6(10),17(10),1289(24)])]. given #308 (W,wt=21): 3312 ((x + x')' + (h(x) + (h(x) + (x + x'')''))')' = x. [para(1458(a,1),48(a,1,1,2,1,2,2)),rewrite([6(14),17(15),17(14),58(15),1458(28)])]. given #309 (W,wt=21): 3320 ((x + x)' + (h(x) + (h(x) + (x + x'')'')')')' = x. [para(1458(a,1),57(a,1,1,2,1,2)),rewrite([6(14)])]. given #310 (W,wt=21): 3482 ((x + x')' + (h(x) + (h(x) + (h(x) + (x + x)'')))')' = x. [para(1514(a,1),54(a,1,1,2,1,2,2)),rewrite([6(14),10(14),6(12),1514(28)])]. given #311 (A,wt=23): 132 ((x + (h(y)' + (y + (y + y')'')'))' + (y + x)')' = x. [para(25(a,1),19(a,1,1,2,1,1))]. given #312 (W,wt=21): 3487 ((x + x)' + (h(x) + (h(x) + (h(x) + (x + x)''))')')' = x. [para(1514(a,1),57(a,1,1,2,1,2)),rewrite([6(14)])]. given #313 (W,wt=21): 4050 ((x + (y + (y + y')''))' + (h(y) + x)')' = y + x. [para(24(a,1),1832(a,1,1,2,1)),rewrite([6(5)])]. given #314 (W,wt=21): 11170 ((x' + y)' + (y + (y + (x + (y + x')')))')' = y. [para(6(a,1),845(a,1,1,1,1))]. given #315 (W,wt=21): 11171 ((x + y')' + (x + (x + (y + (y' + x)')))')' = x. [para(6(a,1),845(a,1,1,2,1,2,2,2,1))]. given #316 (W,wt=21): 11401 ((x' + y)' + (y + (x + (y + (y + x')')))')' = y. [para(6(a,1),857(a,1,1,1,1))]. given #317 (W,wt=21): 11402 ((x + y')' + (x + (y + (x + (y' + x)')))')' = x. [para(6(a,1),857(a,1,1,2,1,2,2,2,1))]. given #318 (W,wt=21): 12225 ((x + (y + y))' + (x + (h(y) + (y + y)'))')' = x + y. [para(30(a,1),122(a,1,1,2,1,2,2)),rewrite([6(10)])]. given #319 (W,wt=21): 12890 ((x' + y)' + (x + (y + (y + (y + x')')))')' = y. [para(6(a,1),1248(a,1,1,1,1))]. given #320 (A,wt=25): 133 (x + (h(x) + (x + (x + x')'')')')' = (x + (x + x')'')'. [para(25(a,1),19(a,1,1,2)),rewrite([6(8),6(10)])]. given #321 (W,wt=21): 12891 ((x + y')' + (y + (x + (x + (y' + x)')))')' = x. [para(6(a,1),1248(a,1,1,2,1,2,2,2,1))]. given #322 (W,wt=21): 15528 ((x + (x + y))' + (y + (h(x) + (x + x)'))')' = y + x. [para(6(a,1),12225(a,1,1,1,1)),rewrite([7(2)])]. given #323 (W,wt=21): 15529 ((x + (y + y))' + (h(y) + ((y + y)' + x))')' = x + y. [para(6(a,1),12225(a,1,1,2,1)),rewrite([7(8)])]. given #324 (W,wt=21): 15534 ((x + (y + x))' + (y + (h(x) + (x + x)'))')' = y + x. [para(17(a,1),12225(a,1,1,1,1))]. given #325 (W,wt=21): 15535 ((x + (y + y))' + (h(y) + (x + (y + y)'))')' = x + y. [para(17(a,1),12225(a,1,1,2,1))]. given #326 (W,wt=21): 15817 ((x + (x + y))' + (h(x) + ((x + x)' + y))')' = y + x. [para(6(a,1),15528(a,1,1,2,1)),rewrite([7(8)])]. given #327 (W,wt=21): 15818 ((x + (h(y) + (y + y)'))' + (y + (y + x))')' = x + y. [para(6(a,1),15528(a,1,1))]. given #328 (W,wt=21): 15824 ((x + (x + y))' + (h(x) + (y + (x + x)'))')' = y + x. [para(17(a,1),15528(a,1,1,2,1))]. given #329 (A,wt=23): 134 ((x + y)' + (h(x)' + ((x + (x + x')'')' + y))')' = y. [para(25(a,1),29(a,1,1,2,1,1)),rewrite([7(10),6(14)])]. given #330 (W,wt=21): 15855 ((h(x) + ((x + x)' + y))' + (y + (x + x))')' = y + x. [para(6(a,1),15529(a,1,1))]. given #331 (W,wt=21): 15859 ((x + (y + x))' + (h(x) + ((x + x)' + y))')' = y + x. [para(17(a,1),15529(a,1,1,1,1))]. given #332 (W,wt=21): 15888 ((x + (h(y) + (y + y)'))' + (y + (x + y))')' = x + y. [para(6(a,1),15534(a,1,1))]. given #333 (W,wt=21): 15893 ((x + (y + x))' + (h(x) + (y + (x + x)'))')' = y + x. [para(17(a,1),15534(a,1,1,2,1))]. given #334 (W,wt=21): 16012 ((h(x) + ((x + x)' + y))' + (x + (y + x))')' = y + x. [para(17(a,1),15855(a,1,1,2,1))]. given #335 (W,wt=22): 211 ((x + y)' + (x + ((x + y)' + (x + y')''))')' = x. [para(21(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #336 (W,wt=22): 221 (h(x)' + (x + (h(x)' + (x + (x + x'))'')'')')' = x. [para(26(a,1),21(a,1,1,2,1,1)),rewrite([26(24)])]. given #337 (W,wt=22): 368 (x + ((x + x)' + (h(x) + (x + x)')'')')' = (x + x)'. [para(346(a,1),8(a,1,1,1))]. given #338 (A,wt=23): 135 ((x + y)' + (h(y)' + ((y + (y + y')'')' + x))')' = x. [para(25(a,1),30(a,1,1,1,1,2)),rewrite([7(12)])]. given #339 (W,wt=22): 405 (x + (h(x) + ((x + x)' + (x + x'')'))')' = (x + x)'. [para(340(a,1),8(a,1,1,2)),rewrite([17(9),6(11)])]. given #340 (W,wt=22): 422 ((x + y)' + (x + (x + (y' + (x + y)'))'')')' = x. [para(23(a,1),8(a,1,1,1))]. given #341 (W,wt=22): 426 ((x + y)' + (y + ((x + y)' + (y + x')''))')' = y. [para(18(a,1),23(a,1,1,2,1,2,2)),rewrite([6(9),17(10),18(20)])]. given #342 (W,wt=22): 430 ((x + y)' + (x + ((x + y)' + (y' + x)''))')' = x. [para(19(a,1),23(a,1,1,2,1,2,2)),rewrite([6(9),17(10),19(20)])]. given #343 (W,wt=22): 438 ((x + y)' + (y + ((x + y)' + (x' + y)''))')' = y. [para(29(a,1),23(a,1,1,2,1,2,2)),rewrite([6(9),17(10),29(20)])]. given #344 (W,wt=22): 446 (h(x)' + (x + (h(x)' + (x + (x + x')'')''))')' = x. [para(25(a,1),23(a,1,1,2,1,2,2)),rewrite([6(12),17(13),25(26)])]. given #345 (W,wt=22): 568 ((x + y)' + (y + (y + (x' + (x + y)'))'')')' = y. [para(35(a,1),8(a,1,1,1))]. given #346 (W,wt=22): 572 ((x + x')' + (x' + (h(x)' + (x + x')'))')' = h(x)'. [para(10(a,1),35(a,1,1,2,1,2,2,1)),rewrite([6(11),7(11),10(18)])]. given #347 (A,wt=23): 136 ((x + y)' + (y + (h(x)' + (x + (x + x')'')'))')' = y. [para(25(a,1),42(a,1,1,1,1,1))]. given #348 (W,wt=22): 615 ((x + y)' + (x + (y' + (x + (x + y)'))'')')' = x. [para(46(a,1),8(a,1,1,1))]. given #349 (W,wt=22): 666 ((x + y)' + (y + (x' + (y + (x + y)'))'')')' = y. [para(73(a,1),8(a,1,1,1))]. given #350 (W,wt=22): 697 (h(x)' + (x + (x + (h(x)' + (x + x')''))'')')' = x. [para(129(a,1),8(a,1,1,1))]. given #351 (W,wt=22): 887 ((x + x)' + (x + (h(x) + ((x + x)' + (x + x)')))')' = x. [para(346(a,1),48(a,1,1,2,1,2,2)),rewrite([6(9),17(10),17(9),346(22)])]. given #352 (W,wt=22): 959 (x + (x + (x' + (x + (x + h(x)))'))')' = (x + (x + h(x)))'. [para(923(a,1),8(a,1,1,2)),rewrite([6(7),7(7),6(9)])]. given #353 (W,wt=22): 1193 ((x + x')' + (h(x) + (h(x) + (x' + x')')'')')' = x. [para(1028(a,1),23(a,1,1,2,1,2,2)),rewrite([6(15),17(16),24(16),1028(28)])]. given #354 (W,wt=22): 1550 (x + (h(x) + ((x + x)' + (x + (x + h(x)))'))')' = (x + x)'. [para(1541(a,1),8(a,1,1,2)),rewrite([17(9),6(11)])]. given #355 (W,wt=22): 6123 ((x + x')' + (h(x) + (h(x) + (h(x) + (x' + x')')))')' = x. [para(1200(a,1),54(a,1,1,2,1,2,2)),rewrite([6(15),10(15),6(13),1200(30)])]. given #356 (A,wt=29): 137 ((x + (y + z))' + (x + (y + (h(z)' + (z + (z + z')'')')))')' = x + y. [para(25(a,1),20(a,1,1,2,1,2,2)),rewrite([6(16)])]. given #357 (W,wt=22): 6128 ((x + x)' + (h(x) + (h(x) + (h(x) + (x' + x')'))')')' = x. [para(1200(a,1),57(a,1,1,2,1,2)),rewrite([6(15)])]. given #358 (W,wt=22): 6569 ((x + x')' + (h(x) + (h(x) + (x' + (x + h(x))')'))')' = x. [para(6052(a,1),48(a,1,1,2,1,2,2)),rewrite([6(15),17(16),17(15),58(16),6052(30)])]. given #359 (W,wt=22): 6576 ((x + x)' + (h(x) + (h(x) + (x' + (x + h(x))')')')')' = x. [para(6052(a,1),57(a,1,1,2,1,2)),rewrite([6(15)])]. given #360 (W,wt=22): 11714 (h(x)' + (x + (h(x)' + (x + (x + (x + h(x))'))''))')' = x. [para(11677(a,1),23(a,1,1,2,1,2,2)),rewrite([6(12),17(13),11677(26)])]. given #361 (W,wt=22): 11729 (h(x)' + (x + (x + (x + (h(x)' + (x + h(x))')))'')')' = x. [para(11677(a,1),36(a,1,1,2,1,1)),rewrite([17(10),17(9),11677(26)])]. given #362 (W,wt=22): 11986 ((x + x)' + (x + (x + ((x + x)' + (x + h(x))')))')' = x. [para(11676(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #363 (W,wt=22): 16081 ((x + y)' + (y + ((y + x)' + (y + x')''))')' = y. [para(6(a,1),211(a,1,1,1,1))]. given #364 (W,wt=22): 16082 ((x + y)' + (x + ((y + x)' + (x + y')''))')' = x. [para(6(a,1),211(a,1,1,2,1,2,1,1))]. given #365 (A,wt=24): 139 ((x + h(y)')' + (x + (y + (y + (y + (y' + h(y)')))'))')' = x. [para(62(a,1),8(a,1,1,2,1,2)),rewrite([6(15)])]. given #366 (W,wt=22): 16274 ((x + y)' + (y + (y + (x' + (y + x)'))'')')' = y. [para(6(a,1),422(a,1,1,1,1))]. given #367 (W,wt=22): 16275 ((x + y)' + (x + (x + (y' + (y + x)'))'')')' = x. [para(6(a,1),422(a,1,1,2,1,2,1,1,2,2,1))]. given #368 (W,wt=22): 16404 ((x + y)' + (y + ((y + x)' + (x' + y)''))')' = y. [para(6(a,1),430(a,1,1,1,1))]. given #369 (W,wt=22): 16405 ((x + y)' + (x + ((y + x)' + (y' + x)''))')' = x. [para(6(a,1),430(a,1,1,2,1,2,1,1))]. given #370 (W,wt=22): 16506 ((x + y)' + (y + (x' + (y + (y + x)'))'')')' = y. [para(6(a,1),615(a,1,1,1,1))]. given #371 (W,wt=22): 16507 ((x + y)' + (x + (y' + (x + (y + x)'))'')')' = x. [para(6(a,1),615(a,1,1,2,1,2,1,1,2,2,1))]. given #372 (W,wt=23): 158 ((x + (h(y) + z))' + (y + (x + ((y + y')' + z))')')' = y. [para(24(a,1),27(a,1,1,1,1,2))]. given #373 (W,wt=23): 159 ((h(x) + y)' + ((x + x')' + (x + y)')')' = (x + x')'. [para(24(a,1),27(a,1,1,1,1))]. given #374 (A,wt=29): 141 (h(x)' + (x' + (x + (x + (x' + h(x)')))')')' = (x + (x + (x' + h(x)')))'. [para(62(a,1),18(a,1,1,1)),rewrite([6(11)])]. given #375 (W,wt=15): 17256 (x + (x + (x + h(x)))')' = (x + x')'. [para(1550(a,1),159(a,1,1,2,1,2)),rewrite([169(13),6(10),8(11),6(5)])]. given #376 (W,wt=17): 17259 ((x + (x + (x + h(x))))' + (x + x')')' = x. [para(17256(a,1),8(a,1,1,2))]. given #377 (W,wt=17): 17292 (x + (x + (x + (h(x) + h(x))))')' = (x + x')'. [para(17256(a,1),48(a,1,1,2,1,2,2)),rewrite([7(7),7(6),28(6),17256(14)])]. given #378 (W,wt=19): 17257 ((x + x')' + (x + (x + (x + h(x)))'')')' = x. [para(17256(a,1),8(a,1,1,1))]. given #379 (W,wt=19): 17282 (x + (h(x) + (x + (x + h(x)))'')')' = (x + x')'. [para(17256(a,1),23(a,1,1,2,1,2,2)),rewrite([6(9),24(10),17256(16)])]. given #380 (W,wt=19): 17443 ((x + (x + (x + (h(x) + h(x)))))' + (x + x')')' = x. [para(17256(a,1),845(a,1,1,1)),rewrite([17256(12),7(10),7(9),28(9),6(11)])]. given #381 (W,wt=19): 17479 ((x + x)' + (h(x) + (x + (x + (x + h(x))))')')' = x. [para(17259(a,1),68(a,1,1,2,1,2)),rewrite([6(7),6(11)])]. given #382 (W,wt=19): 17599 (x + (x + (x + (h(x) + (h(x) + h(x)))))')' = (x + x')'. [para(17259(a,1),860(a,1,1,1)),rewrite([17259(20),6(11),6(12),7(12),7(11),7(10),7(9),28(9),6(10),7(10),7(9),7(8),7(7),67(8)])]. given #383 (A,wt=24): 142 ((x + ((x + (x + (x' + h(x)')))' + y))' + (y + h(x)')')' = y. [para(62(a,1),18(a,1,1,2,1,2)),rewrite([7(9)])]. given #384 (W,wt=21): 17353 ((x + x')' + (x + (h(x) + (x + (x + h(x)))''))')' = x. [para(17256(a,1),423(a,1,1,1)),rewrite([17256(14),6(12),24(13)])]. given #385 (W,wt=21): 17466 ((x + x')' + (h(x) + (x + (x + (x + h(x))))'')')' = x. [para(17259(a,1),35(a,1,1,2,1,2,2)),rewrite([6(13),17(14),24(14),17259(24)])]. given #386 (W,wt=21): 17513 ((x + x')' + (x + (x + (x + (h(x) + h(x))))'')')' = x. [para(17259(a,1),51(a,1,1,2,1,1)),rewrite([6(11),7(11),7(10),7(9),28(9),17259(24)])]. given #387 (W,wt=21): 17624 (x + (h(x) + (x + (x + (h(x) + h(x))))'')')' = (x + x')'. [para(17292(a,1),23(a,1,1,2,1,2,2)),rewrite([6(11),24(12),17292(20)])]. given #388 (W,wt=21): 17737 ((x + (x + (x + (h(x) + (h(x) + h(x))))))' + (x + x')')' = x. [para(17292(a,1),845(a,1,1,1)),rewrite([17292(16),7(12),7(11),7(10),67(11),6(13)])]. given #389 (W,wt=21): 17760 ((x + x)' + (h(x) + (x + (x + (x + h(x)))'')')')' = x. [para(17257(a,1),57(a,1,1,2,1,2)),rewrite([6(13)])]. given #390 (W,wt=21): 17867 (x + (h(x) + (h(x) + (x + (x + h(x)))''))')' = (x + x')'. [para(17257(a,1),845(a,1,1,1)),rewrite([17257(24),6(13),17(14),17(13),24(13),17(12),17(11),58(12)])]. given #391 (W,wt=21): 18018 ((x + x)' + (h(x) + (x + (x + (x + (h(x) + h(x)))))')')' = x. [para(17443(a,1),68(a,1,1,2,1,2)),rewrite([6(9),6(13)])]. given #392 (A,wt=24): 143 ((x + (y + (y + (y + (y' + h(y)')))'))' + (h(y)' + x)')' = x. [para(62(a,1),19(a,1,1,2,1,1))]. given #393 (W,wt=21): 18135 (x + (x + (x + (h(x) + (h(x) + (h(x) + h(x))))))')' = (x + x')'. [para(17443(a,1),1674(a,1,1,1)),rewrite([17443(24),6(13),10(13),6(11),17(12),7(11),7(10),7(9),7(8),67(9),17(9),17(8)])]. given #394 (W,wt=23): 161 ((x + (y + h(z)))' + (z + (x + (y + (z + z')'))')')' = z. [para(28(a,1),27(a,1,1,1,1,2))]. given #395 (W,wt=23): 165 ((x + y)' + (h(y)' + (x + (y + (y + y')'')'))')' = x. [para(25(a,1),27(a,1,1,2,1,2)),rewrite([6(14)])]. given #396 (W,wt=23): 170 ((x + h(y))' + ((y + y')' + (x + y)')')' = (y + y')'. [para(10(a,1),31(a,1,1,1,1,2))]. given #397 (W,wt=23): 175 ((x + h(y))' + ((y + y')' + (y + x)')')' = (y + y')'. [para(28(a,1),31(a,1,1,1,1))]. given #398 (W,wt=23): 185 ((h(x) + y)' + ((x + y)' + (x + x')')')' = (x + x')'. [para(24(a,1),49(a,1,1,1,1))]. given #399 (W,wt=23): 190 ((x + y)' + (h(x)' + (y + (x + (x + x')'')'))')' = y. [para(25(a,1),49(a,1,1,2,1,1)),rewrite([6(14)])]. given #400 (W,wt=23): 201 ((x + h(y))' + ((x + y)' + (y + y')')')' = (y + y')'. [para(10(a,1),70(a,1,1,1,1,2))]. given #401 (A,wt=24): 144 ((h(x)' + y)' + (x + ((x + (x + (x' + h(x)')))' + y))')' = y. [para(62(a,1),29(a,1,1,2,1,1)),rewrite([7(9),6(15)])]. given #402 (W,wt=23): 206 ((x + h(y))' + ((y + x)' + (y + y')')')' = (y + y')'. [para(28(a,1),70(a,1,1,1,1))]. given #403 (W,wt=23): 267 ((x + (h(y) + z))' + (y + ((y + y')' + (z + x))')')' = y. [para(58(a,1),148(a,1,1,1,1)),rewrite([7(9)])]. given #404 (W,wt=23): 268 ((x + (y + h(z)))' + (z + (y + ((z + z')' + x))')')' = z. [para(67(a,1),148(a,1,1,1,1)),rewrite([7(9)])]. given #405 (W,wt=23): 279 ((h(x) + y)' + ((x + x')' + (y + x)')')' = (x + x')'. [para(24(a,1),149(a,1,1,1,1))]. given #406 (W,wt=23): 280 (((x + x')' + (y + (z + x)))' + (z + (h(x) + y)')')' = z. [para(24(a,1),149(a,1,1,2,1,2,1)),rewrite([7(6)])]. given #407 (W,wt=23): 282 ((x + ((y + y')' + (z + y)))' + (z + (x + h(y))')')' = z. [para(28(a,1),149(a,1,1,2,1,2,1)),rewrite([7(6)])]. given #408 (W,wt=23): 285 ((x + y)' + ((y + (y + y')'')' + (x + h(y)'))')' = x. [para(25(a,1),149(a,1,1,2,1,2)),rewrite([6(14)])]. given #409 (W,wt=23): 314 ((h(x) + y)' + ((y + x)' + (x + x')')')' = (x + x')'. [para(24(a,1),177(a,1,1,1,1))]. given #410 (A,wt=24): 145 ((x + h(y)')' + (y + ((y + (y + (y' + h(y)')))' + x))')' = x. [para(62(a,1),30(a,1,1,1,1,2)),rewrite([7(13)])]. given #411 (W,wt=23): 315 (((x + x')' + (y + (z + x)))' + ((h(x) + y)' + z)')' = z. [para(24(a,1),177(a,1,1,2,1,1,1)),rewrite([7(6)])]. given #412 (W,wt=23): 317 ((x + ((y + y')' + (z + y)))' + ((x + h(y))' + z)')' = z. [para(28(a,1),177(a,1,1,2,1,1,1)),rewrite([7(6)])]. given #413 (W,wt=23): 320 ((x + y)' + ((x + (x + x')'')' + (y + h(x)'))')' = y. [para(25(a,1),177(a,1,1,2,1,1)),rewrite([6(14)])]. given #414 (W,wt=23): 369 ((x + y)' + (x + ((y + y)' + (h(y) + (y + y)')'))')' = x. [para(346(a,1),8(a,1,1,2,1,2)),rewrite([6(13)])]. given #415 (W,wt=23): 372 (((x + x)' + ((h(x) + (x + x)')' + y))' + (y + x)')' = y. [para(346(a,1),18(a,1,1,2,1,2)),rewrite([7(9)])]. given #416 (W,wt=23): 373 ((x + ((y + y)' + (h(y) + (y + y)')'))' + (y + x)')' = x. [para(346(a,1),19(a,1,1,2,1,1))]. given #417 (W,wt=23): 374 (x + (x + (x + (h(x) + (x + x)')'))')' = (h(x) + (x + x)')'. [para(346(a,1),19(a,1,1,2)),rewrite([6(7),7(7),6(9)])]. given #418 (W,wt=23): 375 ((x + y)' + ((x + x)' + ((h(x) + (x + x)')' + y))')' = y. [para(346(a,1),29(a,1,1,2,1,1)),rewrite([7(9),6(13)])]. given #419 (A,wt=24): 146 ((h(x)' + y)' + (y + (x + (x + (x + (x' + h(x)')))'))')' = y. [para(62(a,1),42(a,1,1,1,1,1))]. given #420 (W,wt=23): 376 ((x + y)' + ((y + y)' + ((h(y) + (y + y)')' + x))')' = x. [para(346(a,1),30(a,1,1,1,1,2)),rewrite([7(11)])]. given #421 (W,wt=23): 377 ((x + y)' + (y + ((x + x)' + (h(x) + (x + x)')'))')' = y. [para(346(a,1),42(a,1,1,1,1,1))]. given #422 (W,wt=23): 379 ((x + y)' + ((y + y)' + (x + (h(y) + (y + y)')'))')' = x. [para(346(a,1),27(a,1,1,2,1,2)),rewrite([6(13)])]. given #423 (W,wt=23): 380 ((x + y)' + ((x + x)' + (y + (h(x) + (x + x)')'))')' = y. [para(346(a,1),49(a,1,1,2,1,1)),rewrite([6(13)])]. given #424 (W,wt=23): 383 ((x + y)' + ((h(y) + (y + y)')' + (x + (y + y)'))')' = x. [para(346(a,1),149(a,1,1,2,1,2)),rewrite([6(13)])]. given #425 (W,wt=23): 384 ((x + y)' + ((h(x) + (x + x)')' + (y + (x + x)'))')' = y. [para(346(a,1),177(a,1,1,2,1,1)),rewrite([6(13)])]. given #426 (W,wt=23): 394 ((x + (h(y) + z)')' + ((y + y')' + (z + (x + y)))')' = x. [para(24(a,1),247(a,1,1,1,1,2,1)),rewrite([7(11)])]. given #427 (W,wt=23): 395 ((x + (y + h(z))')' + (y + ((z + z')' + (x + z)))')' = x. [para(28(a,1),247(a,1,1,1,1,2,1)),rewrite([7(11)])]. given #428 (A,wt=30): 147 ((x + (y + h(z)'))' + (x + (y + (z + (z + (z + (z' + h(z)')))')))')' = x + y. [para(62(a,1),20(a,1,1,2,1,2,2)),rewrite([6(17)])]. given #429 (W,wt=23): 399 (((h(x) + y)' + z)' + ((x + x')' + (y + (z + x)))')' = z. [para(24(a,1),253(a,1,1,1,1,1,1)),rewrite([7(11)])]. given #430 (W,wt=23): 400 (((x + h(y))' + z)' + (x + ((y + y')' + (z + y)))')' = z. [para(28(a,1),253(a,1,1,1,1,1,1)),rewrite([7(11)])]. given #431 (W,wt=23): 441 ((x + y')' + (x + ((x + y')' + (y + x)''))')' = x. [para(30(a,1),23(a,1,1,2,1,2,2)),rewrite([6(10),17(11),30(21)])]. given #432 (W,wt=23): 444 ((x' + y)' + (y + ((x' + y)' + (y + x)''))')' = y. [para(42(a,1),23(a,1,1,2,1,2,2)),rewrite([6(10),17(11),42(21)])]. given #433 (W,wt=23): 447 (x + (x + (h(x)' + (x + (x + (x' + h(x)')))''))')' = h(x)'. [para(62(a,1),23(a,1,1,2,1,2,2)),rewrite([6(11),62(24)])]. given #434 (W,wt=23): 503 ((x + (y + y')')' + (x + (y + (h(y) + y'')'))')' = x. [para(435(a,1),8(a,1,1,2,1,2)),rewrite([6(14)])]. given #435 (W,wt=17): 19923 (h(x)' + (x + (x + (h(x) + x'')'))')' = x. [para(10(a,1),503(a,1,1,1,1))]. given #436 (W,wt=20): 19933 (x + (x + (x + (h(x)' + (h(x) + x'')')))')' = h(x)'. [para(19923(a,1),8(a,1,1,2)),rewrite([17(10),17(9),6(12)])]. given #437 (A,wt=26): 151 (x + ((y + (x + z))' + (x + (y + z)')'')')' = (y + (x + z))'. [para(27(a,1),8(a,1,1,1))]. given #438 (W,wt=22): 19922 (x + (x + ((x + x)' + (h(x) + x'')'))')' = (x + x)'. [para(8(a,1),503(a,1,1,1)),rewrite([17(9)])]. given #439 (W,wt=22): 19931 (x + (h(x)' + (x + (x + (h(x) + x'')'))'')')' = h(x)'. [para(19923(a,1),8(a,1,1,1))]. given #440 (W,wt=22): 19957 (h(x)' + (x + (x + (x + (h(x)' + (h(x) + x'')'))))')' = x. [para(19923(a,1),48(a,1,1,2,1,2,2)),rewrite([6(12),17(13),17(12),17(11),19923(28)])]. given #441 (W,wt=23): 506 ((x + ((h(x) + x'')' + y))' + (y + (x + x')')')' = y. [para(435(a,1),18(a,1,1,2,1,2)),rewrite([7(7)])]. given #442 (W,wt=23): 507 ((x + (y + (h(y) + y'')'))' + ((y + y')' + x)')' = x. [para(435(a,1),19(a,1,1,2,1,1))]. given #443 (W,wt=23): 508 (((x + x')' + y)' + (x + ((h(x) + x'')' + y))')' = y. [para(435(a,1),29(a,1,1,2,1,1)),rewrite([7(7),6(14)])]. given #444 (W,wt=23): 509 ((x + (y + y')')' + (y + ((h(y) + y'')' + x))')' = x. [para(435(a,1),30(a,1,1,1,1,2)),rewrite([7(12)])]. given #445 (W,wt=23): 510 (((x + x')' + y)' + (y + (x + (h(x) + x'')'))')' = y. [para(435(a,1),42(a,1,1,1,1,1))]. given #446 (A,wt=24): 152 (x + (x + ((y + z)' + (y + (x + z))'))')' = (y + (x + z))'. [para(27(a,1),8(a,1,1,2)),rewrite([6(7),7(7),6(9)])]. given #447 (W,wt=23): 512 ((x + (y + y')')' + (y + (x + (h(y) + y'')'))')' = x. [para(435(a,1),27(a,1,1,2,1,2)),rewrite([6(14)])]. given #448 (W,wt=23): 513 ((x + (y + (h(x) + x'')'))' + ((x + x')' + y)')' = y. [para(435(a,1),49(a,1,1,2,1,1))]. given #449 (W,wt=23): 516 (((x + x')' + y)' + (x + (y + (h(x) + x'')'))')' = y. [para(435(a,1),102(a,1,1,1,1,1))]. given #450 (W,wt=23): 517 (((h(x) + x'')' + (y + x))' + (y + (x + x')')')' = y. [para(435(a,1),149(a,1,1,2,1,2))]. given #451 (W,wt=23): 518 (((x + x')' + y)' + ((h(x) + x'')' + (y + x))')' = y. [para(435(a,1),177(a,1,1,2,1,1)),rewrite([6(14)])]. given #452 (W,wt=23): 523 ((x + (y + y')')' + ((h(y) + y'')' + (x + y))')' = x. [para(435(a,1),247(a,1,1,1,1,2))]. given #453 (W,wt=23): 571 ((x + y')' + (x + ((x + y')' + (x + y)''))')' = x. [para(8(a,1),35(a,1,1,2,1,2,2)),rewrite([6(10),17(11),8(21)])]. given #454 (W,wt=23): 585 ((x' + y)' + (y + ((x' + y)' + (x + y)''))')' = y. [para(29(a,1),35(a,1,1,2,1,2,2)),rewrite([6(10),17(11),29(21)])]. given #455 (A,wt=27): 154 (x + ((x + (y + z)')' + (y + (x + z))'')')' = (x + (y + z)')'. [para(27(a,1),18(a,1,1,1))]. given #456 (W,wt=23): 751 (x + (h(x)' + (x + (x + (x + (x' + h(x)'))))'')')' = h(x)'. [para(140(a,1),8(a,1,1,1))]. Low Water (keep, Weight): wt=35 given #457 (W,wt=23): 843 ((x + y')' + (x + (x + (y + (x + y')'))'')')' = x. [para(48(a,1),8(a,1,1,1))]. given #458 (W,wt=23): 909 (x + (x + (h(x)' + (h(x)' + (x + (x + x'))'')))')' = h(x)'. [para(60(a,1),48(a,1,1,2,1,2,2)),rewrite([6(11),60(26)])]. given #459 (W,wt=23): 913 (x + (x + (x + (h(x)' + (h(x)' + (x + x')''))))')' = h(x)'. [para(129(a,1),48(a,1,1,2,1,2,2)),rewrite([6(11),17(11),129(26)])]. given #460 (W,wt=23): 916 (h(x)' + (x + (x + (x + (x + (x' + (h(x)' + h(x)'))))))')' = x. [para(140(a,1),48(a,1,1,2,1,2,2)),rewrite([6(12),17(13),17(12),17(11),17(10),17(9),140(28)])]. given #461 (W,wt=23): 943 ((x + y)' + (x + ((y + (y + h(y)))' + (y + y')'))')' = x. [para(846(a,1),22(a,1,1,2,1,2,2))]. given #462 (W,wt=23): 960 (x + ((x + x')' + (x + (x + h(x)))'')')' = (x + x')'. [para(923(a,1),18(a,1,1,1))]. given #463 (W,wt=23): 961 (((x + (x + h(x)))' + ((x + x')' + y))' + (y + x)')' = y. [para(923(a,1),18(a,1,1,2,1,2)),rewrite([7(9)])]. given #464 (A,wt=25): 156 (x + (y + (x + (z + (x + (y + z)')')))')' = (x + (y + z)')'. [para(27(a,1),19(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #465 (W,wt=23): 962 ((x + ((y + (y + h(y)))' + (y + y')'))' + (y + x)')' = x. [para(923(a,1),19(a,1,1,2,1,1))]. given #466 (W,wt=23): 963 ((x + y)' + ((x + (x + h(x)))' + ((x + x')' + y))')' = y. [para(923(a,1),29(a,1,1,2,1,1)),rewrite([7(9),6(13)])]. given #467 (W,wt=23): 964 ((x + y)' + ((y + (y + h(y)))' + ((y + y')' + x))')' = x. [para(923(a,1),30(a,1,1,1,1,2)),rewrite([7(11)])]. given #468 (W,wt=23): 965 ((x + y)' + (y + ((x + (x + h(x)))' + (x + x')'))')' = y. [para(923(a,1),42(a,1,1,1,1,1))]. given #469 (W,wt=23): 967 ((x + y)' + ((y + (y + h(y)))' + (x + (y + y')'))')' = x. [para(923(a,1),27(a,1,1,2,1,2)),rewrite([6(13)])]. given #470 (W,wt=23): 968 ((x + y)' + ((x + (x + h(x)))' + (y + (x + x')'))')' = y. [para(923(a,1),49(a,1,1,2,1,1)),rewrite([6(13)])]. given #471 (W,wt=23): 970 ((x + y)' + ((y + y')' + (x + (y + (y + h(y)))'))')' = x. [para(923(a,1),149(a,1,1,2,1,2)),rewrite([6(13)])]. given #472 (W,wt=23): 971 ((x + y)' + ((x + x')' + (y + (x + (x + h(x)))'))')' = y. [para(923(a,1),177(a,1,1,2,1,1)),rewrite([6(13)])]. given #473 (A,wt=24): 166 ((x + h(y)')' + (y + (x + (y + (y + (y' + h(y)')))'))')' = x. [para(62(a,1),27(a,1,1,2,1,2)),rewrite([6(15)])]. given #474 (W,wt=23): 984 ((x + (y + (y + (h(y) + h(y)))'))' + (x + (y + y')')')' = x. [para(958(a,1),8(a,1,1,2,1,2))]. given #475 (W,wt=17): 21117 (h(x)' + (x + (x + (x + (h(x) + h(x)))'))')' = x. [para(10(a,1),984(a,1,1,2,1)),rewrite([6(11)])]. given #476 (W,wt=20): 21126 (x + (x + (x + (h(x)' + (x + (h(x) + h(x)))')))')' = h(x)'. [para(21117(a,1),8(a,1,1,2)),rewrite([17(10),17(9),6(12)])]. given #477 (W,wt=22): 21116 (x + (x + ((x + x)' + (x + (h(x) + h(x)))'))')' = (x + x)'. [para(8(a,1),984(a,1,1,2)),rewrite([17(9),6(11)])]. given #478 (W,wt=22): 21124 (x + (h(x)' + (x + (x + (x + (h(x) + h(x)))'))'')')' = h(x)'. [para(21117(a,1),8(a,1,1,1))]. given #479 (W,wt=22): 21149 (h(x)' + (x + (x + (x + (h(x)' + (x + (h(x) + h(x)))'))))')' = x. [para(21117(a,1),48(a,1,1,2,1,2,2)),rewrite([6(12),17(13),17(12),17(11),21117(28)])]. given #480 (W,wt=23): 987 ((x + ((x + (h(x) + h(x)))' + y))' + (y + (x + x')')')' = y. [para(958(a,1),18(a,1,1,2,1,2)),rewrite([7(7)])]. given #481 (W,wt=23): 988 ((x + (y + (y + (h(y) + h(y)))'))' + ((y + y')' + x)')' = x. [para(958(a,1),19(a,1,1,2,1,1))]. given #482 (A,wt=26): 168 (x + ((y + (z + x))' + (x + (y + z)')'')')' = (y + (z + x))'. [para(31(a,1),8(a,1,1,1))]. given #483 (W,wt=23): 989 ((x + ((x + (h(x) + h(x)))' + y))' + ((x + x')' + y)')' = y. [para(958(a,1),29(a,1,1,2,1,1)),rewrite([7(7)])]. given #484 (W,wt=23): 990 ((x + (y + y')')' + (y + ((y + (h(y) + h(y)))' + x))')' = x. [para(958(a,1),30(a,1,1,1,1,2)),rewrite([7(12)])]. given #485 (W,wt=23): 991 (((x + x')' + y)' + (y + (x + (x + (h(x) + h(x)))'))')' = y. [para(958(a,1),42(a,1,1,1,1,1))]. given #486 (W,wt=23): 993 ((x + (y + (x + (h(x) + h(x)))'))' + (y + (x + x')')')' = y. [para(958(a,1),27(a,1,1,2,1,2))]. given #487 (W,wt=23): 994 ((x + (y + (x + (h(x) + h(x)))'))' + ((x + x')' + y)')' = y. [para(958(a,1),49(a,1,1,2,1,1))]. given #488 (W,wt=23): 997 (((x + x')' + y)' + (x + (y + (x + (h(x) + h(x)))'))')' = y. [para(958(a,1),102(a,1,1,1,1,1))]. given #489 (W,wt=23): 998 (((x + (h(x) + h(x)))' + (y + x))' + (y + (x + x')')')' = y. [para(958(a,1),149(a,1,1,2,1,2))]. given #490 (W,wt=23): 999 ((x + (y + y')')' + (y + (x + (y + (h(y) + h(y)))'))')' = x. [para(958(a,1),150(a,1,1,1,1,2))]. given #491 (A,wt=24): 169 (x + (x + ((y + z)' + (y + (z + x))'))')' = (y + (z + x))'. [para(31(a,1),8(a,1,1,2)),rewrite([6(7),7(7),6(9)])]. given #492 (W,wt=23): 1000 (((x + (h(x) + h(x)))' + (y + x))' + ((x + x')' + y)')' = y. [para(958(a,1),177(a,1,1,2,1,1))]. given #493 (W,wt=23): 1005 ((x + (y + y')')' + ((y + (h(y) + h(y)))' + (x + y))')' = x. [para(958(a,1),247(a,1,1,1,1,2))]. given #494 (W,wt=23): 1006 (((x + x')' + y)' + ((x + (h(x) + h(x)))' + (y + x))')' = y. [para(958(a,1),253(a,1,1,1,1,1))]. given #495 (W,wt=23): 1234 ((x + y')' + (x + (y + (x + (x + y')'))'')')' = x. [para(54(a,1),8(a,1,1,1))]. given #496 (W,wt=23): 1293 ((x' + y)' + (y + (y + (x + (x' + y)'))'')')' = y. [para(56(a,1),8(a,1,1,1))]. given #497 (W,wt=23): 1300 ((x + (x + x'))' + (x + (h(x) + (x + (x + x'))'))')' = x. [para(26(a,1),56(a,1,1,2,1,2,2)),rewrite([6(10),6(11),7(11),26(22)])]. given #498 (W,wt=23): 1446 ((x + (h(y) + z))' + (y + ((y + y')' + (x + z))')')' = y. [para(17(a,1),57(a,1,1,1,1))]. given #499 (W,wt=23): 1447 ((h(x) + (y + z))' + (x + (y + ((x + x')' + z))')')' = x. [para(17(a,1),57(a,1,1,2,1,2,1))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 21611 (0.00 of 55.76 sec). given #500 (A,wt=27): 171 (x + ((x + (y + z)')' + (y + (z + x))'')')' = (x + (y + z)')'. [para(31(a,1),18(a,1,1,1))]. given #501 (W,wt=23): 1490 (x + (h(x) + ((x + x')' + (x + x)''))')' = (x + x')'. [para(1487(a,1),8(a,1,1,2)),rewrite([17(9),6(11)])]. given #502 (W,wt=23): 1656 ((x' + y)' + (y + (x + (y + (x' + y)'))'')')' = y. [para(81(a,1),8(a,1,1,1))]. given #503 (W,wt=23): 2147 ((h(x) + (y + z))' + (x + (y + (z + (x + x')'))')')' = x. [para(7(a,1),263(a,1,1,2,1,2,1))]. given #504 (W,wt=23): 2151 ((x + (h(y) + z))' + (y + (x + (z + (y + y')'))')')' = y. [para(17(a,1),263(a,1,1,1,1)),rewrite([7(9)])]. given #505 (W,wt=23): 2184 ((x + (y + h(z)))' + (z + ((z + z')' + (x + y))')')' = z. [para(7(a,1),264(a,1,1,1,1))]. given #506 (W,wt=23): 2188 ((x + (y + h(z)))' + (z + (x + ((z + z')' + y))')')' = z. [para(17(a,1),264(a,1,1,2,1,2,1)),rewrite([7(3)])]. given #507 (W,wt=23): 2502 ((x + x')' + (h(x) + (x + (h(x) + x'')'')'')')' = x. [para(502(a,1),23(a,1,1,2,1,2,2)),rewrite([6(16),17(17),24(17),502(30)])]. given #508 (W,wt=23): 2515 ((x + x')' + (x + (h(x) + (h(x) + x'')'')'')')' = x. [para(502(a,1),36(a,1,1,2,1,1)),rewrite([17(14),24(14),502(30)])]. given #509 (A,wt=25): 172 (x + (y + (z + (x + (x + (y + z)')')))')' = (x + (y + z)')'. [para(31(a,1),19(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #510 (W,wt=23): 2549 (x + (h(x) + (h(x) + (h(x) + x'')'')'')')' = (x + x')'. [para(525(a,1),23(a,1,1,2,1,2,2)),rewrite([6(14),24(15),525(26)])]. given #511 (W,wt=23): 2586 ((x + x')' + (h(x) + (x + (h(x) + (h(x) + x'')))'')')' = x. [para(548(a,1),23(a,1,1,2,1,2,2)),rewrite([6(16),17(17),24(17),548(30)])]. given #512 (W,wt=23): 2816 ((x + x')' + (h(x) + (h(x) + (x + (x + h(x)))'')'')')' = x. [para(977(a,1),23(a,1,1,2,1,2,2)),rewrite([6(16),17(17),24(17),977(30)])]. given #513 (W,wt=23): 2867 ((x + x')' + (h(x) + (x + (x + (h(x) + h(x)))'')'')')' = x. [para(983(a,1),23(a,1,1,2,1,2,2)),rewrite([6(16),17(17),24(17),983(30)])]. given #514 (W,wt=23): 2880 ((x + x')' + (x + (h(x) + (x + (h(x) + h(x)))'')'')')' = x. [para(983(a,1),36(a,1,1,2,1,1)),rewrite([17(14),24(14),983(30)])]. given #515 (W,wt=23): 2918 (x + (h(x) + (h(x) + (x + (h(x) + h(x)))'')'')')' = (x + x')'. [para(1008(a,1),23(a,1,1,2,1,2,2)),rewrite([6(14),24(15),1008(26)])]. given #516 (W,wt=23): 2960 ((x + x')' + (h(x) + (x + (h(x) + (x + h(x))''))'')')' = x. [para(1090(a,1),23(a,1,1,2,1,2,2)),rewrite([6(16),17(17),24(17),1090(30)])]. given #517 (W,wt=23): 2973 ((x + x')' + (x + (h(x) + (h(x) + (x + h(x))''))'')')' = x. [para(1090(a,1),36(a,1,1,2,1,1)),rewrite([17(14),17(13),58(14),1090(30)])]. given #518 (A,wt=29): 173 ((x + (h(y) + z))' + ((y + y')' + (z + (x + y)'))')' = (y + y')' + z. [para(24(a,1),31(a,1,1,1,1,2)),rewrite([7(11)])]. given #519 (W,wt=23): 3011 (x + (h(x) + (h(x) + (h(x) + (x + h(x))''))'')')' = (x + x')'. [para(1116(a,1),23(a,1,1,2,1,2,2)),rewrite([6(14),24(15),1116(26)])]. given #520 (W,wt=23): 3052 ((x + x')' + (h(x) + (x + (x + (h(x) + (h(x) + h(x)))))'')')' = x. [para(1145(a,1),35(a,1,1,2,1,2,2)),rewrite([6(16),17(17),24(17),1145(30)])]. given #521 (W,wt=23): 3124 ((x + x')' + (x + (h(x) + (h(x) + (h(x) + x'')))'')')' = x. [para(1271(a,1),8(a,1,1,1))]. given #522 (W,wt=23): 3143 (x + (h(x) + (h(x) + (h(x) + (h(x) + x'')))'')')' = (x + x')'. [para(1271(a,1),23(a,1,1,2,1,2,2)),rewrite([6(14),24(15),1271(26)])]. given #523 (W,wt=23): 3237 ((x + x')' + (x + (x + (h(x) + (h(x) + (h(x) + h(x)))))'')')' = x. [para(1289(a,1),8(a,1,1,1))]. given #524 (W,wt=23): 3258 (x + (h(x) + (x + (h(x) + (h(x) + (h(x) + h(x)))))'')')' = (x + x')'. [para(1289(a,1),23(a,1,1,2,1,2,2)),rewrite([6(14),24(15),1289(26)])]. given #525 (W,wt=23): 3306 ((x + x')' + (h(x) + (h(x) + (x + x'')'')'')')' = x. [para(1458(a,1),23(a,1,1,2,1,2,2)),rewrite([6(16),17(17),24(17),1458(30)])]. given #526 (W,wt=23): 3472 ((x + x')' + (h(x) + (h(x) + (h(x) + (x + x)''))'')')' = x. [para(1514(a,1),23(a,1,1,2,1,2,2)),rewrite([6(16),17(17),24(17),1514(30)])]. given #527 (A,wt=29): 174 ((x + (y + h(z)))' + (y + ((z + z')' + (x + z)'))')' = y + (z + z')'. [para(28(a,1),31(a,1,1,1,1,2)),rewrite([7(11)])]. given #528 (W,wt=23): 4395 (((x + x')' + (y + (z + x)))' + (h(x) + (y + z)')')' = h(x). [para(7(a,1),1917(a,1,1,1,1,2))]. given #529 (W,wt=23): 4518 ((x + (h(y) + z))' + ((y + y')' + ((x + z)' + y))')' = h(y). [para(17(a,1),1955(a,1,1,1,1))]. given #530 (W,wt=23): 4817 ((x + (y + h(z)))' + ((z + z')' + ((x + y)' + z))')' = h(z). [para(7(a,1),2333(a,1,1,1,1))]. given #531 (W,wt=23): 4977 (((x + x')' + (y + (z + x)))' + ((y + z)' + h(x))')' = h(x). [para(7(a,1),2663(a,1,1,1,1,2))]. given #532 (W,wt=23): 5271 (((x + y)' + h(z))' + ((z + z')' + (x + (y + z)))')' = h(z). [para(7(a,1),4052(a,1,1,2,1,2))]. given #533 (W,wt=23): 5292 ((h(x) + (y + z)')' + ((x + x')' + (y + (z + x)))')' = h(x). [para(7(a,1),4205(a,1,1,2,1,2))]. given #534 (W,wt=23): 5551 ((x + x')' + (x + (h(x) + (h(x) + (h(x) + x''))''))')' = x. [para(528(a,1),423(a,1,1,1)),rewrite([528(20),6(15),24(16)])]. given #535 (W,wt=23): 5567 ((x + x')' + (x + (h(x) + (h(x) + (x + h(x))'')''))')' = x. [para(947(a,1),423(a,1,1,1)),rewrite([947(20),6(15),24(16)])]. given #536 (A,wt=26): 178 (x + ((y + (x + z))' + ((y + z)' + x)'')')' = (y + (x + z))'. [para(49(a,1),8(a,1,1,1))]. given #537 (W,wt=23): 5568 ((x + x')' + (x + (h(x) + (x + (h(x) + (h(x) + h(x))))''))')' = x. [para(1018(a,1),423(a,1,1,1)),rewrite([1018(20),6(15),24(16)])]. given #538 (W,wt=23): 10768 ((x + x')' + (h(x) + (h(x) + (x + (h(x) + x''))''))')' = x. [para(545(a,1),48(a,1,1,2,1,2,2)),rewrite([6(16),17(17),17(16),58(17),545(32)])]. given #539 (W,wt=23): 10773 ((x + x)' + (h(x) + (h(x) + (x + (h(x) + x''))'')')')' = x. [para(545(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #540 (W,wt=23): 10835 ((x + x)' + (h(x) + (x + (h(x) + (h(x) + x''))'')')')' = x. [para(547(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #541 (W,wt=23): 10888 (x + (h(x) + (h(x) + (h(x) + (h(x) + x''))''))')' = (x + x')'. [para(566(a,1),48(a,1,1,2,1,2,2)),rewrite([6(14),17(14),58(15),566(28)])]. given #542 (W,wt=23): 11248 ((x + x')' + (x + (h(x) + (h(x) + (h(x) + x'')'')))')' = x. [para(525(a,1),845(a,1,1,1)),rewrite([525(22),6(15),17(15),58(16)])]. given #543 (W,wt=23): 11255 ((x + x')' + (x + (h(x) + (h(x) + (x + (h(x) + h(x)))'')))')' = x. [para(1008(a,1),845(a,1,1,1)),rewrite([1008(22),6(15),17(15),58(16)])]. given #544 (W,wt=23): 11457 ((x + x')' + (x + (h(x) + (h(x) + (h(x) + (x + h(x))''))))')' = x. [para(1116(a,1),857(a,1,1,1)),rewrite([1116(22),10(15),6(13)])]. given #545 (A,wt=24): 179 (x + ((y + z)' + (x + (y + (x + z))'))')' = (y + (x + z))'. [para(49(a,1),8(a,1,1,2)),rewrite([6(7),7(7),6(9)])]. given #546 (W,wt=23): 11459 ((x + x')' + (x + (h(x) + (h(x) + (h(x) + (h(x) + x'')))))')' = x. [para(1271(a,1),857(a,1,1,1)),rewrite([1271(22),10(15),6(13)])]. given #547 (W,wt=23): 11461 ((x + (x + (h(x) + (h(x) + (h(x) + (h(x) + h(x)))))))' + (x + x')')' = x. [para(1289(a,1),857(a,1,1,1)),rewrite([1289(22),10(15),6(13),17(13),6(16)])]. given #548 (W,wt=23): 11695 ((x + y)' + (x + (h(y)' + (y + (y + (y + h(y))'))'))')' = x. [para(11677(a,1),8(a,1,1,2,1,2)),rewrite([6(14)])]. given #549 (W,wt=23): 11698 ((h(x)' + ((x + (x + (x + h(x))'))' + y))' + (y + x)')' = y. [para(11677(a,1),18(a,1,1,2,1,2)),rewrite([7(10)])]. given #550 (W,wt=23): 11699 ((x + (h(y)' + (y + (y + (y + h(y))'))'))' + (y + x)')' = x. [para(11677(a,1),19(a,1,1,2,1,1))]. given #551 (W,wt=23): 11701 ((x + y)' + (h(x)' + ((x + (x + (x + h(x))'))' + y))')' = y. [para(11677(a,1),29(a,1,1,2,1,1)),rewrite([7(10),6(14)])]. given #552 (W,wt=23): 11702 ((x + y)' + (h(y)' + ((y + (y + (y + h(y))'))' + x))')' = x. [para(11677(a,1),30(a,1,1,1,1,2)),rewrite([7(12)])]. given #553 (W,wt=23): 11703 ((x + y)' + (y + (h(x)' + (x + (x + (x + h(x))'))'))')' = y. [para(11677(a,1),42(a,1,1,1,1,1))]. given #554 (A,wt=27): 181 (x + (((y + z)' + x)' + (y + (x + z))'')')' = ((y + z)' + x)'. [para(49(a,1),18(a,1,1,1))]. given #555 (W,wt=23): 11705 ((x + y)' + (h(y)' + (x + (y + (y + (y + h(y))'))'))')' = x. [para(11677(a,1),27(a,1,1,2,1,2)),rewrite([6(14)])]. given #556 (W,wt=23): 11706 ((x + y)' + (h(x)' + (y + (x + (x + (x + h(x))'))'))')' = y. [para(11677(a,1),49(a,1,1,2,1,1)),rewrite([6(14)])]. given #557 (W,wt=23): 11709 ((x + y)' + ((y + (y + (y + h(y))'))' + (x + h(y)'))')' = x. [para(11677(a,1),149(a,1,1,2,1,2)),rewrite([6(14)])]. given #558 (W,wt=23): 11710 ((x + y)' + ((x + (x + (x + h(x))'))' + (y + h(x)'))')' = y. [para(11677(a,1),177(a,1,1,2,1,1)),rewrite([6(14)])]. given #559 (W,wt=23): 11855 (x + (x + (x + (x + (h(x)' + (h(x)' + (x + h(x))')))))')' = h(x)'. [para(11677(a,1),845(a,1,1,1)),rewrite([11677(19),6(10),17(11),17(10),17(9),17(12),17(11),17(10)])]. given #560 (W,wt=23): 12221 ((x + (y + y))' + (x + (h(y) + (y + y'')'))')' = x + y. [para(8(a,1),122(a,1,1,2,1,2,2)),rewrite([6(12)])]. given #561 (W,wt=23): 12260 ((x + (y + y))' + (x + (h(y) + (y + (y + h(y)))'))')' = x + y. [para(845(a,1),122(a,1,1,2,1,2,2)),rewrite([10(5),6(12)])]. given #562 (W,wt=23): 12520 ((x + x')' + (h(x) + (h(x) + (x + (x + h(x))'')''))')' = x. [para(1083(a,1),48(a,1,1,2,1,2,2)),rewrite([6(16),17(17),17(16),58(17),1083(32)])]. given #563 (A,wt=25): 183 (x + (y + (x + (z + ((y + z)' + x)')))')' = ((y + z)' + x)'. [para(49(a,1),19(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #564 (W,wt=23): 12525 ((x + x)' + (h(x) + (h(x) + (x + (x + h(x))'')'')')')' = x. [para(1083(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #565 (W,wt=23): 12583 ((x + x)' + (h(x) + (x + (h(x) + (x + h(x))'')'')')')' = x. [para(1092(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #566 (W,wt=23): 12626 (x + (h(x) + (h(x) + (h(x) + (x + h(x))'')''))')' = (x + x')'. [para(1092(a,1),845(a,1,1,1)),rewrite([1092(30),6(16),17(17),17(16),24(16),17(15),17(14),58(15)])]. given #567 (W,wt=23): 12711 ((x + x')' + (h(x) + (h(x) + (x + (x + (h(x) + h(x))))''))')' = x. [para(1135(a,1),48(a,1,1,2,1,2,2)),rewrite([6(16),17(17),17(16),58(17),1135(32)])]. given #568 (W,wt=23): 12716 ((x + x)' + (h(x) + (h(x) + (x + (x + (h(x) + h(x))))'')')')' = x. [para(1135(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #569 (W,wt=23): 12782 ((x + x)' + (h(x) + (x + (x + (h(x) + (h(x) + h(x))))'')')')' = x. [para(1143(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #570 (W,wt=23): 12825 (x + (h(x) + (h(x) + (x + (h(x) + (h(x) + h(x))))''))')' = (x + x')'. [para(1143(a,1),845(a,1,1,1)),rewrite([1143(30),6(16),17(17),17(16),24(16),17(15),17(14),58(15)])]. given #571 (W,wt=23): 13180 ((x + x')' + (h(x) + (h(x) + (h(x) + (x + x)'')''))')' = x. [para(1507(a,1),48(a,1,1,2,1,2,2)),rewrite([6(16),17(17),17(16),58(17),1507(32)])]. given #572 (A,wt=24): 191 ((x + (y + (x + (x + (x' + h(x)')))'))' + (h(x)' + y)')' = y. [para(62(a,1),49(a,1,1,2,1,1))]. given #573 (W,wt=23): 13185 ((x + x)' + (h(x) + (h(x) + (h(x) + (x + x)'')'')')')' = x. [para(1507(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #574 (W,wt=23): 13489 ((x + x)' + (h(x) + (x + (h(x) + (h(x) + x'')''))')')' = x. [para(2508(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #575 (W,wt=23): 13614 (x + (h(x) + (h(x) + (h(x) + (h(x) + x'')'')))')' = (x + x')'. [para(2553(a,1),54(a,1,1,2,1,2,2)),rewrite([10(14),6(12),2553(28)])]. given #576 (W,wt=23): 13681 ((x + x)' + (h(x) + (x + (h(x) + (h(x) + (h(x) + x''))))')')' = x. [para(2596(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #577 (W,wt=23): 13871 ((x + x')' + (h(x) + (h(x) + (h(x) + (x + (x + h(x)))'')))')' = x. [para(2822(a,1),54(a,1,1,2,1,2,2)),rewrite([6(16),10(16),6(14),2822(32)])]. given #578 (W,wt=23): 13874 ((x + x)' + (h(x) + (h(x) + (h(x) + (x + (x + h(x)))''))')')' = x. [para(2822(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #579 (W,wt=23): 14002 ((x + x)' + (h(x) + (x + (h(x) + (x + (h(x) + h(x)))''))')')' = x. [para(2873(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #580 (W,wt=23): 14127 (x + (h(x) + (h(x) + (h(x) + (x + (h(x) + h(x)))'')))')' = (x + x')'. [para(2922(a,1),54(a,1,1,2,1,2,2)),rewrite([10(14),6(12),2922(28)])]. given #581 (A,wt=31): 192 ((x + (h(y) + z))' + (y' + (x + ((y + y')' + z)))')' = x + ((y + y')' + z). [para(58(a,1),18(a,1,1,1,1)),rewrite([6(11)])]. given #582 (W,wt=23): 14194 ((x + x)' + (h(x) + (x + (h(x) + (h(x) + (x + h(x))'')))')')' = x. [para(2966(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #583 (W,wt=23): 14340 (x + (h(x) + (h(x) + (h(x) + (h(x) + (x + h(x))''))))')' = (x + x')'. [para(3018(a,1),54(a,1,1,2,1,2,2)),rewrite([10(14),6(12),3018(28)])]. given #584 (W,wt=23): 14474 ((x + x)' + (h(x) + (x + (x + (h(x) + (h(x) + (h(x) + h(x))))))')')' = x. [para(3070(a,1),68(a,1,1,2,1,2)),rewrite([6(12),6(16)])]. given #585 (W,wt=23): 14544 (x + (h(x) + (h(x) + (h(x) + (h(x) + (h(x) + x'')))))')' = (x + x')'. [para(3150(a,1),54(a,1,1,2,1,2,2)),rewrite([10(14),6(12),3150(28)])]. given #586 (W,wt=23): 14622 (x + (x + (h(x) + (h(x) + (h(x) + (h(x) + (h(x) + h(x)))))))')' = (x + x')'. [para(3265(a,1),54(a,1,1,2,1,2,2)),rewrite([10(14),6(12),17(12),3265(28)])]. given #587 (W,wt=23): 14701 ((x + x')' + (h(x) + (h(x) + (h(x) + (x + x'')'')))')' = x. [para(3312(a,1),54(a,1,1,2,1,2,2)),rewrite([6(16),10(16),6(14),3312(32)])]. given #588 (W,wt=23): 14704 ((x + x)' + (h(x) + (h(x) + (h(x) + (x + x'')''))')')' = x. [para(3312(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #589 (W,wt=23): 14842 ((x + x')' + (h(x) + (h(x) + (h(x) + (h(x) + (x + x)''))))')' = x. [para(3482(a,1),54(a,1,1,2,1,2,2)),rewrite([6(16),10(16),6(14),3482(32)])]. given #590 (A,wt=25): 193 ((x + (h(y) + z))' + (y + (x + ((y + y')' + z)'))')' = y + x. [para(58(a,1),20(a,1,1,1,1))]. given #591 (W,wt=23): 14845 ((x + x)' + (h(x) + (h(x) + (h(x) + (h(x) + (x + x)'')))')')' = x. [para(3482(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #592 (W,wt=23): 17161 ((h(x) + (y + z))' + (x + (z + ((x + x')' + y))')')' = x. [para(6(a,1),158(a,1,1,1,1)),rewrite([7(3)])]. given #593 (W,wt=23): 17258 ((x + (y + (y + (y + h(y)))'))' + (x + (y + y')')')' = x. [para(17256(a,1),8(a,1,1,2,1,2))]. given #594 (W,wt=17): 23450 (h(x)' + (x + (x + (x + (x + h(x)))'))')' = x. [para(10(a,1),17258(a,1,1,2,1)),rewrite([6(10)])]. given #595 (W,wt=20): 23459 (x + (x + (x + (h(x)' + (x + (x + h(x)))')))')' = h(x)'. [para(23450(a,1),8(a,1,1,2)),rewrite([17(9),17(8),6(11)])]. given #596 (W,wt=22): 23449 (x + (x + ((x + x)' + (x + (x + h(x)))'))')' = (x + x)'. [para(8(a,1),17258(a,1,1,2)),rewrite([17(8),6(10)])]. given #597 (W,wt=22): 23457 (x + (h(x)' + (x + (x + (x + (x + h(x)))'))'')')' = h(x)'. [para(23450(a,1),8(a,1,1,1))]. given #598 (W,wt=22): 23482 (h(x)' + (x + (x + (x + (h(x)' + (x + (x + h(x)))'))))')' = x. [para(23450(a,1),48(a,1,1,2,1,2,2)),rewrite([6(11),17(12),17(11),17(10),23450(26)])]. given #599 (A,wt=29): 194 ((x + (h(y) + z))' + ((y + y')' + (z + (y + x)'))')' = (y + y')' + z. [para(58(a,1),31(a,1,1,1,1)),rewrite([7(11)])]. given #600 (W,wt=23): 17261 ((x + ((x + (x + h(x)))' + y))' + (y + (x + x')')')' = y. [para(17256(a,1),18(a,1,1,2,1,2)),rewrite([7(6)])]. given #601 (W,wt=23): 17262 ((x + (y + (y + (y + h(y)))'))' + ((y + y')' + x)')' = x. [para(17256(a,1),19(a,1,1,2,1,1))]. given #602 (W,wt=23): 17263 ((x + ((x + (x + h(x)))' + y))' + ((x + x')' + y)')' = y. [para(17256(a,1),29(a,1,1,2,1,1)),rewrite([7(6)])]. given #603 (W,wt=23): 17264 ((x + (y + y')')' + (y + ((y + (y + h(y)))' + x))')' = x. [para(17256(a,1),30(a,1,1,1,1,2)),rewrite([7(11)])]. given #604 (W,wt=23): 17265 (((x + x')' + y)' + (y + (x + (x + (x + h(x)))'))')' = y. [para(17256(a,1),42(a,1,1,1,1,1))]. given #605 (W,wt=23): 17267 ((x + (y + (x + (x + h(x)))'))' + (y + (x + x')')')' = y. [para(17256(a,1),27(a,1,1,2,1,2))]. given #606 (W,wt=23): 17268 ((x + (y + (x + (x + h(x)))'))' + ((x + x')' + y)')' = y. [para(17256(a,1),49(a,1,1,2,1,1))]. given #607 (W,wt=23): 17271 (((x + x')' + y)' + (x + (y + (x + (x + h(x)))'))')' = y. [para(17256(a,1),102(a,1,1,1,1,1))]. given #608 (A,wt=31): 195 ((x + (y + h(z)))' + (z' + (x + (y + (z + z')')))')' = x + (y + (z + z')'). [para(67(a,1),18(a,1,1,1,1)),rewrite([6(11)])]. given #609 (W,wt=23): 17272 (((x + (x + h(x)))' + (y + x))' + (y + (x + x')')')' = y. [para(17256(a,1),149(a,1,1,2,1,2))]. given #610 (W,wt=23): 17273 ((x + (y + y')')' + (y + (x + (y + (y + h(y)))'))')' = x. [para(17256(a,1),150(a,1,1,1,1,2))]. given #611 (W,wt=23): 17274 (((x + (x + h(x)))' + (y + x))' + ((x + x')' + y)')' = y. [para(17256(a,1),177(a,1,1,2,1,1))]. given #612 (W,wt=23): 17279 ((x + (y + y')')' + ((y + (y + h(y)))' + (x + y))')' = x. [para(17256(a,1),247(a,1,1,1,1,2))]. given #613 (W,wt=23): 17280 (((x + x')' + y)' + ((x + (x + h(x)))' + (y + x))')' = y. [para(17256(a,1),253(a,1,1,1,1,1))]. given #614 (W,wt=23): 17456 ((x + x')' + (h(x) + (x + (x + (x + h(x)))'')'')')' = x. [para(17256(a,1),211(a,1,1,1)),rewrite([17256(9),24(16)])]. given #615 (W,wt=23): 17458 ((x + x')' + (x + (h(x) + (x + (x + h(x)))'')'')')' = x. [para(17256(a,1),422(a,1,1,1)),rewrite([17256(14),6(12),24(13)])]. given #616 (W,wt=23): 17678 ((x + x')' + (x + (h(x) + (x + (x + (h(x) + h(x))))''))')' = x. [para(17292(a,1),423(a,1,1,1)),rewrite([17292(18),6(14),24(15)])]. given #617 (A,wt=25): 196 ((x + (y + h(z)))' + (z + (x + (y + (z + z')')'))')' = z + x. [para(67(a,1),20(a,1,1,1,1))]. given #618 (W,wt=23): 17890 (x + (h(x) + (h(x) + (x + (x + h(x)))'')'')')' = (x + x')'. [para(17282(a,1),23(a,1,1,2,1,2,2)),rewrite([6(13),24(14),17282(24)])]. given #619 (W,wt=23): 17997 ((x + x')' + (x + (h(x) + (h(x) + (x + (x + h(x)))'')))')' = x. [para(17282(a,1),845(a,1,1,1)),rewrite([17282(20),6(14),17(14),58(15)])]. given #620 (W,wt=23): 18005 ((x + x')' + (h(x) + (x + (x + (x + (h(x) + h(x)))))'')')' = x. [para(17443(a,1),35(a,1,1,2,1,2,2)),rewrite([6(15),17(16),24(16),17443(28)])]. given #621 (W,wt=23): 18050 ((x + x')' + (x + (x + (x + (h(x) + (h(x) + h(x)))))'')')' = x. [para(17443(a,1),51(a,1,1,2,1,1)),rewrite([6(13),7(13),7(12),7(11),7(10),67(11),17443(28)])]. given #622 (W,wt=23): 18306 (x + (h(x) + (x + (x + (h(x) + (h(x) + h(x)))))'')')' = (x + x')'. [para(17599(a,1),23(a,1,1,2,1,2,2)),rewrite([6(13),24(14),17599(24)])]. given #623 (W,wt=23): 18416 ((x + (x + (x + (h(x) + (h(x) + (h(x) + h(x)))))))' + (x + x')')' = x. [para(17599(a,1),857(a,1,1,1)),rewrite([17599(20),10(14),6(12),17(12),17(11),6(15)])]. given #624 (W,wt=23): 18438 ((x + x)' + (h(x) + (x + (h(x) + (x + (x + h(x)))''))')')' = x. [para(17353(a,1),57(a,1,1,2,1,2)),rewrite([6(15)])]. given #625 (W,wt=23): 18504 ((x + x')' + (h(x) + (h(x) + (x + (x + (x + h(x))))''))')' = x. [para(17466(a,1),48(a,1,1,2,1,2,2)),rewrite([6(15),17(16),17(15),58(16),17466(30)])]. given #626 (A,wt=29): 197 ((x + (y + h(z)))' + (y + ((z + z')' + (z + x)'))')' = y + (z + z')'. [para(67(a,1),31(a,1,1,1,1)),rewrite([7(11)])]. given #627 (W,wt=23): 18509 ((x + x)' + (h(x) + (h(x) + (x + (x + (x + h(x))))'')')')' = x. [para(17466(a,1),57(a,1,1,2,1,2)),rewrite([6(15)])]. given #628 (W,wt=23): 18567 ((x + x)' + (h(x) + (x + (x + (x + (h(x) + h(x))))'')')')' = x. [para(17513(a,1),57(a,1,1,2,1,2)),rewrite([6(15)])]. given #629 (W,wt=23): 18610 (x + (h(x) + (h(x) + (x + (x + (h(x) + h(x))))''))')' = (x + x')'. [para(17513(a,1),845(a,1,1,1)),rewrite([17513(28),6(15),17(16),17(15),24(15),17(14),17(13),58(14)])]. given #630 (W,wt=23): 18691 ((x + x)' + (h(x) + (x + (x + (x + (h(x) + (h(x) + h(x))))))')')' = x. [para(17737(a,1),68(a,1,1,2,1,2)),rewrite([6(11),6(15)])]. given #631 (W,wt=23): 18821 (x + (h(x) + (h(x) + (h(x) + (x + (x + h(x)))'')))')' = (x + x')'. [para(17867(a,1),54(a,1,1,2,1,2,2)),rewrite([10(13),6(11),17867(26)])]. given #632 (W,wt=23): 18974 (x + (x + (x + (h(x) + (h(x) + (h(x) + (h(x) + h(x)))))))')' = (x + x')'. [para(18135(a,1),54(a,1,1,2,1,2,2)),rewrite([10(13),6(11),17(11),17(10),18135(26)])]. given #633 (W,wt=23): 19033 ((x + (h(y) + z))' + (y + (z + (x + (y + y')'))')')' = y. [para(6(a,1),161(a,1,1,1,1)),rewrite([7(3)])]. given #634 (W,wt=23): 19034 ((x + (y + h(z)))' + (z + (y + (x + (z + z')'))')')' = z. [para(17(a,1),161(a,1,1,1,1))]. given #635 (A,wt=26): 199 (x + ((y + (z + x))' + ((y + z)' + x)'')')' = (y + (z + x))'. [para(70(a,1),8(a,1,1,1))]. given #636 (W,wt=23): 19202 ((x + (y + h(z)))' + (z + ((z + z')' + (y + x))')')' = z. [para(6(a,1),267(a,1,1,1,1,2))]. given #637 (W,wt=23): 19206 ((h(x) + (y + z))' + (x + ((x + x')' + (z + y))')')' = x. [para(17(a,1),267(a,1,1,1,1))]. given #638 (W,wt=23): 19207 ((x + (h(y) + z))' + (y + (z + ((y + y')' + x))')')' = y. [para(17(a,1),267(a,1,1,2,1,2,1))]. given #639 (W,wt=23): 19248 (((x + x')' + (y + (x + z)))' + (z + (h(x) + y)')')' = z. [para(6(a,1),280(a,1,1,1,1,2,2))]. given #640 (W,wt=23): 19249 (((x + x')' + (y + (x + z)))' + (y + (h(x) + z)')')' = y. [para(6(a,1),280(a,1,1,1,1,2)),rewrite([7(5)])]. given #641 (W,wt=23): 19250 (((x + x')' + (y + (z + x)))' + (z + (y + h(x))')')' = z. [para(6(a,1),280(a,1,1,2,1,2,1))]. given #642 (W,wt=23): 19251 (((x + x')' + (y + (z + x)))' + (y + (h(x) + z)')')' = y. [para(17(a,1),280(a,1,1,1,1,2))]. given #643 (W,wt=23): 19252 ((x + ((y + y')' + (z + y)))' + (z + (h(y) + x)')')' = z. [para(17(a,1),280(a,1,1,1,1))]. given #644 (A,wt=24): 200 (x + ((y + z)' + (x + (y + (z + x))'))')' = (y + (z + x))'. [para(70(a,1),8(a,1,1,2)),rewrite([6(7),7(7),6(9)])]. given #645 (W,wt=23): 19345 (((x + x')' + (y + (x + z)))' + (y + (z + h(x))')')' = y. [para(6(a,1),282(a,1,1,1,1)),rewrite([7(6),7(5)])]. given #646 (W,wt=23): 19394 (((x + x')' + (y + (x + z)))' + ((h(x) + y)' + z)')' = z. [para(6(a,1),315(a,1,1,1,1,2,2))]. given #647 (W,wt=23): 19395 (((x + x')' + (y + (x + z)))' + ((h(x) + z)' + y)')' = y. [para(6(a,1),315(a,1,1,1,1,2)),rewrite([7(5)])]. given #648 (W,wt=23): 19396 (((x + x')' + (y + (z + x)))' + ((y + h(x))' + z)')' = z. [para(6(a,1),315(a,1,1,2,1,1,1))]. given #649 (W,wt=23): 19397 (((x + x')' + (y + (z + x)))' + ((h(x) + z)' + y)')' = y. [para(17(a,1),315(a,1,1,1,1,2))]. given #650 (W,wt=23): 19398 ((x + ((y + y')' + (z + y)))' + ((h(y) + x)' + z)')' = z. [para(17(a,1),315(a,1,1,1,1))]. given #651 (W,wt=23): 19435 (((x + x')' + (y + (x + z)))' + ((z + h(x))' + y)')' = y. [para(6(a,1),317(a,1,1,1,1)),rewrite([7(6),7(5)])]. given #652 (W,wt=23): 19648 ((x + (y + h(z))')' + ((z + z')' + (y + (x + z)))')' = x. [para(6(a,1),394(a,1,1,1,1,2,1))]. given #653 (A,wt=27): 202 (x + (((y + z)' + x)' + (y + (z + x))'')')' = ((y + z)' + x)'. [para(70(a,1),18(a,1,1,1))]. given #654 (W,wt=23): 19649 ((x + (h(y) + z)')' + ((y + y')' + (z + (y + x)))')' = x. [para(6(a,1),394(a,1,1,2,1,2,2))]. given #655 (W,wt=23): 19650 ((x + (h(y) + z)')' + ((y + y')' + (x + (y + z)))')' = x. [para(6(a,1),394(a,1,1,2,1,2)),rewrite([7(10)])]. given #656 (W,wt=23): 19651 ((x + (h(y) + z)')' + ((y + y')' + (x + (z + y)))')' = x. [para(17(a,1),394(a,1,1,2,1,2))]. given #657 (W,wt=23): 19652 ((x + (h(y) + z)')' + (z + ((y + y')' + (x + y)))')' = x. [para(17(a,1),394(a,1,1,2,1))]. given #658 (W,wt=23): 19670 ((x + (y + h(z))')' + ((z + z')' + (x + (z + y)))')' = x. [para(6(a,1),395(a,1,1,2,1)),rewrite([7(11),7(10)])]. given #659 (W,wt=23): 19673 (((x + h(y))' + z)' + ((y + y')' + (x + (z + y)))')' = z. [para(6(a,1),399(a,1,1,1,1,1,1))]. given #660 (W,wt=23): 19674 (((h(x) + y)' + z)' + ((x + x')' + (y + (x + z)))')' = z. [para(6(a,1),399(a,1,1,2,1,2,2))]. given #661 (W,wt=23): 19675 (((h(x) + y)' + z)' + ((x + x')' + (z + (x + y)))')' = z. [para(6(a,1),399(a,1,1,2,1,2)),rewrite([7(10)])]. given #662 (A,wt=25): 203 (x + (y + (z + (x + ((y + z)' + x)')))')' = ((y + z)' + x)'. [para(70(a,1),19(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #663 (W,wt=23): 19676 (((h(x) + y)' + z)' + ((x + x')' + (z + (y + x)))')' = z. [para(17(a,1),399(a,1,1,2,1,2))]. given #664 (W,wt=23): 19677 (((h(x) + y)' + z)' + (y + ((x + x')' + (z + x)))')' = z. [para(17(a,1),399(a,1,1,2,1))]. given #665 (W,wt=23): 19679 (((x + h(y))' + z)' + ((y + y')' + (z + (y + x)))')' = z. [para(6(a,1),400(a,1,1,2,1)),rewrite([7(11),7(10)])]. given #666 (W,wt=23): 19681 ((x' + y)' + (y + ((y + x')' + (x + y)''))')' = y. [para(6(a,1),441(a,1,1,1,1))]. given #667 (W,wt=23): 19682 ((x + y')' + (x + ((y' + x)' + (y + x)''))')' = x. [para(6(a,1),441(a,1,1,2,1,2,1,1))]. given #668 (W,wt=23): 19853 ((x + y')' + (x + ((y' + x)' + (x + y)''))')' = x. [para(6(a,1),444(a,1,1,1,1))]. given #669 (W,wt=23): 19854 ((x' + y)' + (y + ((y + x')' + (y + x)''))')' = y. [para(6(a,1),444(a,1,1,2,1,2,1,1))]. given #670 (W,wt=23): 20555 ((x' + y)' + (y + (y + (x + (y + x')'))'')')' = y. [para(6(a,1),843(a,1,1,1,1))]. given #671 (A,wt=29): 204 ((x + (h(y) + z))' + ((x + y)' + ((y + y')' + z))')' = (y + y')' + z. [para(24(a,1),70(a,1,1,1,1,2))]. given #672 (W,wt=23): 20556 ((x + y')' + (x + (x + (y + (y' + x)'))'')')' = x. [para(6(a,1),843(a,1,1,2,1,2,1,1,2,2,1))]. given #673 (W,wt=23): 21553 ((x' + y)' + (y + (x + (y + (y + x')'))'')')' = y. [para(6(a,1),1234(a,1,1,1,1))]. given #674 (W,wt=23): 21554 ((x + y')' + (x + (y + (x + (y' + x)'))'')')' = x. [para(6(a,1),1234(a,1,1,2,1,2,1,1,2,2,1))]. given #675 (W,wt=23): 21636 ((h(x) + (y + z))' + (x + (z + (y + (x + x')'))')')' = x. [para(6(a,1),2147(a,1,1,1,1,2))]. given #676 (W,wt=23): 22069 (((x + x')' + (y + (x + z)))' + (h(x) + (y + z)')')' = h(x). [para(6(a,1),4395(a,1,1,1,1,2,2))]. given #677 (W,wt=23): 22070 (((x + x')' + (y + (x + z)))' + (h(x) + (z + y)')')' = h(x). [para(6(a,1),4395(a,1,1,1,1,2)),rewrite([7(5)])]. given #678 (W,wt=23): 22071 (((x + x')' + (y + (z + x)))' + (h(x) + (z + y)')')' = h(x). [para(6(a,1),4395(a,1,1,2,1,2,1))]. given #679 (W,wt=23): 22072 ((x + ((y + y')' + (z + y)))' + (h(y) + (x + z)')')' = h(y). [para(17(a,1),4395(a,1,1,1,1))]. given #680 (A,wt=29): 205 ((x + (y + h(z)))' + ((x + z)' + (y + (z + z')'))')' = y + (z + z')'. [para(28(a,1),70(a,1,1,1,1,2))]. given #681 (W,wt=23): 22084 ((h(x) + (y + z))' + ((x + x')' + ((z + y)' + x))')' = h(x). [para(6(a,1),4518(a,1,1,1,1)),rewrite([7(3)])]. given #682 (W,wt=23): 22085 ((x + (h(y) + z))' + ((y + y')' + ((z + x)' + y))')' = h(y). [para(6(a,1),4518(a,1,1,2,1,2,1,1))]. given #683 (W,wt=23): 22086 (((x + x')' + ((y + z)' + x))' + (y + (h(x) + z))')' = h(x). [para(6(a,1),4518(a,1,1))]. given #684 (W,wt=23): 22217 ((x + (y + h(z)))' + ((z + z')' + ((y + x)' + z))')' = h(z). [para(6(a,1),4817(a,1,1,2,1,2,1,1))]. given #685 (W,wt=23): 22225 (((x + x')' + (y + (x + z)))' + ((y + z)' + h(x))')' = h(x). [para(6(a,1),4977(a,1,1,1,1,2,2))]. given #686 (W,wt=23): 22226 (((x + x')' + (y + (x + z)))' + ((z + y)' + h(x))')' = h(x). [para(6(a,1),4977(a,1,1,1,1,2)),rewrite([7(5)])]. given #687 (W,wt=23): 22227 (((x + x')' + (y + (z + x)))' + ((z + y)' + h(x))')' = h(x). [para(6(a,1),4977(a,1,1,2,1,1,1))]. given #688 (W,wt=23): 22228 ((x + ((y + y')' + (z + y)))' + ((x + z)' + h(y))')' = h(y). [para(17(a,1),4977(a,1,1,1,1))]. given #689 (A,wt=29): 207 ((x + (h(y) + z))' + ((y + x)' + ((y + y')' + z))')' = (y + y')' + z. [para(58(a,1),70(a,1,1,1,1))]. given #690 (W,wt=23): 22234 (((x + y)' + h(z))' + ((z + z')' + (y + (x + z)))')' = h(z). [para(6(a,1),5271(a,1,1,1,1,1,1))]. given #691 (W,wt=23): 22235 (((x + y)' + h(z))' + ((z + z')' + (x + (z + y)))')' = h(z). [para(6(a,1),5271(a,1,1,2,1,2,2))]. given #692 (W,wt=23): 22236 (((x + y)' + h(z))' + ((z + z')' + (y + (z + x)))')' = h(z). [para(6(a,1),5271(a,1,1,2,1,2)),rewrite([7(10)])]. given #693 (W,wt=23): 22237 (((x + y)' + h(z))' + (x + ((z + z')' + (y + z)))')' = h(z). [para(17(a,1),5271(a,1,1,2,1))]. given #694 (W,wt=23): 22238 ((h(x) + (y + z)')' + ((x + x')' + (z + (y + x)))')' = h(x). [para(6(a,1),5292(a,1,1,1,1,2,1))]. given #695 (W,wt=23): 22239 ((h(x) + (y + z)')' + ((x + x')' + (y + (x + z)))')' = h(x). [para(6(a,1),5292(a,1,1,2,1,2,2))]. given #696 (W,wt=23): 22240 ((h(x) + (y + z)')' + ((x + x')' + (z + (x + y)))')' = h(x). [para(6(a,1),5292(a,1,1,2,1,2)),rewrite([7(10)])]. given #697 (W,wt=23): 22241 ((h(x) + (y + z)')' + (y + ((x + x')' + (z + x)))')' = h(x). [para(17(a,1),5292(a,1,1,2,1))]. given #698 (A,wt=29): 208 ((x + (y + h(z)))' + ((z + x)' + (y + (z + z')'))')' = y + (z + z')'. [para(67(a,1),70(a,1,1,1,1))]. given #699 (W,wt=23): 22576 ((x + (x + y))' + (y + (h(x) + (x + x'')'))')' = y + x. [para(6(a,1),12221(a,1,1,1,1)),rewrite([7(2)])]. given #700 (W,wt=23): 22577 ((x + (y + y))' + (h(y) + ((y + y'')' + x))')' = x + y. [para(6(a,1),12221(a,1,1,2,1)),rewrite([7(10)])]. given #701 (W,wt=23): 22582 ((x + (y + x))' + (y + (h(x) + (x + x'')'))')' = y + x. [para(17(a,1),12221(a,1,1,1,1))]. given #702 (W,wt=23): 22583 ((x + (y + y))' + (h(y) + (x + (y + y'')'))')' = x + y. [para(17(a,1),12221(a,1,1,2,1))]. given #703 (W,wt=23): 22600 ((x + (x + y))' + (y + (h(x) + (x + (x + h(x)))'))')' = y + x. [para(6(a,1),12260(a,1,1,1,1)),rewrite([7(2)])]. given #704 (W,wt=23): 22601 ((x + (y + y))' + (h(y) + ((y + (y + h(y)))' + x))')' = x + y. [para(6(a,1),12260(a,1,1,2,1)),rewrite([7(10)])]. given #705 (W,wt=23): 22606 ((x + (y + x))' + (y + (h(x) + (x + (x + h(x)))'))')' = y + x. [para(17(a,1),12260(a,1,1,1,1))]. given #706 (W,wt=23): 22607 ((x + (y + y))' + (h(y) + (x + (y + (y + h(y)))'))')' = x + y. [para(17(a,1),12260(a,1,1,2,1))]. given #707 (A,wt=24): 209 ((x + y)' + (x + ((x + y)' + (x + y')'')'')')' = x. [para(21(a,1),8(a,1,1,1))]. given #708 (W,wt=23): 23334 ((x + (h(y) + (y + y'')'))' + (y + (x + y))')' = y + x. [para(8(a,1),193(a,1,1,2,1,2,2))]. given #709 (W,wt=23): 23370 ((x + (h(y) + (y + (y + h(y)))'))' + (y + (x + y))')' = y + x. [para(845(a,1),193(a,1,1,2,1,2,2)),rewrite([10(5)])]. given #710 (W,wt=23): 24269 (((x + x')' + (y + (x + z)))' + (z + (y + h(x))')')' = z. [para(6(a,1),19248(a,1,1,2,1,2,1))]. given #711 (W,wt=23): 24295 (((x + x')' + (y + (z + x)))' + (y + (z + h(x))')')' = y. [para(17(a,1),19250(a,1,1,1,1,2))]. given #712 (W,wt=23): 24299 ((x + ((y + y')' + (z + y)))' + (x + (h(y) + z)')')' = x. [para(17(a,1),19251(a,1,1,1,1))]. given #713 (W,wt=23): 24343 (((x + x')' + (y + (x + z)))' + ((y + h(x))' + z)')' = z. [para(6(a,1),19394(a,1,1,2,1,1,1))]. given #714 (W,wt=23): 24364 (((x + x')' + (y + (z + x)))' + ((z + h(x))' + y)')' = y. [para(17(a,1),19396(a,1,1,1,1,2))]. given #715 (W,wt=23): 24368 ((x + ((y + y')' + (z + y)))' + ((h(y) + z)' + x)')' = x. [para(17(a,1),19397(a,1,1,1,1))]. given #716 (A,wt=28): 210 ((x + (y + z)')' + (x + (y + ((y + z)' + (y + z')'')'))')' = x. [para(21(a,1),8(a,1,1,2,1,2)),rewrite([6(16)])]. given #717 (W,wt=23): 24382 ((x + (y + h(z))')' + ((z + z')' + (y + (z + x)))')' = x. [para(6(a,1),19648(a,1,1,2,1,2,2))]. given #718 (W,wt=23): 24383 ((x + (y + h(z))')' + ((z + z')' + (x + (y + z)))')' = x. [para(17(a,1),19648(a,1,1,2,1,2))]. given #719 (W,wt=23): 24386 ((x + (h(y) + z)')' + (x + ((y + y')' + (z + y)))')' = x. [para(17(a,1),19651(a,1,1,2,1))]. given #720 (W,wt=23): 24388 (((x + h(y))' + z)' + ((y + y')' + (x + (y + z)))')' = z. [para(6(a,1),19673(a,1,1,2,1,2,2))]. given #721 (W,wt=23): 24389 (((x + h(y))' + z)' + ((y + y')' + (z + (x + y)))')' = z. [para(17(a,1),19673(a,1,1,2,1,2))]. given #722 (W,wt=23): 24407 (((h(x) + y)' + z)' + (z + ((x + x')' + (y + x)))')' = z. [para(17(a,1),19676(a,1,1,2,1))]. given #723 (W,wt=23): 24998 ((x + ((y + y')' + (z + y)))' + (h(y) + (z + x)')')' = h(y). [para(17(a,1),22071(a,1,1,1,1))]. given #724 (W,wt=23): 25149 (((x + x')' + ((y + z)' + x))' + (z + (h(x) + y))')' = h(x). [para(6(a,1),22085(a,1,1))]. given #725 (A,wt=31): 212 ((x + y)' + (x' + (x + (y' + (x + y)'))')')' = (x + (y' + (x + y)'))'. [para(8(a,1),21(a,1,1,2,1,2,1)),rewrite([6(7),7(7),6(10),6(18),7(18)])]. given #726 (W,wt=22): 26511 ((x + x')' + (h(x) + (x' + (h(x) + x'')')')')' = x. [para(212(a,1),57(a,1,1,2,1,2)),rewrite([28(9),6(6),28(18),6(15),435(18),6(15)])]. given #727 (W,wt=23): 25644 ((x + ((y + y')' + (z + y)))' + ((z + x)' + h(y))')' = h(y). [para(17(a,1),22227(a,1,1,1,1))]. given #728 (W,wt=23): 25787 (((x + y)' + h(z))' + (y + ((z + z')' + (x + z)))')' = h(z). [para(17(a,1),22234(a,1,1,2,1))]. given #729 (W,wt=23): 25844 ((h(x) + (y + z)')' + (z + ((x + x')' + (y + x)))')' = h(x). [para(17(a,1),22238(a,1,1,2,1))]. given #730 (W,wt=23): 25871 ((x + (x + y))' + (h(x) + ((x + x'')' + y))')' = y + x. [para(6(a,1),22576(a,1,1,2,1)),rewrite([7(10)])]. given #731 (W,wt=23): 25872 ((x + (h(y) + (y + y'')'))' + (y + (y + x))')' = x + y. [para(6(a,1),22576(a,1,1))]. given #732 (W,wt=23): 25878 ((x + (x + y))' + (h(x) + (y + (x + x'')'))')' = y + x. [para(17(a,1),22576(a,1,1,2,1))]. given #733 (W,wt=23): 25903 ((h(x) + ((x + x'')' + y))' + (y + (x + x))')' = y + x. [para(6(a,1),22577(a,1,1))]. given #734 (A,wt=35): 213 ((x + y)' + (x' + ((x + y)' + (x + y')'')')')' = ((x + y)' + (x + y')'')'. [para(21(a,1),18(a,1,1,1)),rewrite([6(12)])]. given #735 (W,wt=23): 25907 ((x + (y + x))' + (h(x) + ((x + x'')' + y))')' = y + x. [para(17(a,1),22577(a,1,1,1,1))]. given #736 (W,wt=23): 25932 ((x + (y + x))' + (h(x) + (y + (x + x'')'))')' = y + x. [para(17(a,1),22582(a,1,1,2,1))]. given #737 (W,wt=23): 25972 ((x + (x + y))' + (h(x) + ((x + (x + h(x)))' + y))')' = y + x. [para(6(a,1),22600(a,1,1,2,1)),rewrite([7(10)])]. given #738 (W,wt=23): 25973 ((x + (h(y) + (y + (y + h(y)))'))' + (y + (y + x))')' = x + y. [para(6(a,1),22600(a,1,1))]. given #739 (W,wt=23): 25979 ((x + (x + y))' + (h(x) + (y + (x + (x + h(x)))'))')' = y + x. [para(17(a,1),22600(a,1,1,2,1))]. given #740 (W,wt=23): 26003 ((h(x) + ((x + (x + h(x)))' + y))' + (y + (x + x))')' = y + x. [para(6(a,1),22601(a,1,1))]. given #741 (W,wt=23): 26007 ((x + (y + x))' + (h(x) + ((x + (x + h(x)))' + y))')' = y + x. [para(17(a,1),22601(a,1,1,1,1))]. given #742 (W,wt=23): 26032 ((x + (y + x))' + (h(x) + (y + (x + (x + h(x)))'))')' = y + x. [para(17(a,1),22606(a,1,1,2,1))]. given #743 (A,wt=28): 214 ((x + (((x + y)' + (x + y')'')' + z))' + (z + (x + y)')')' = z. [para(21(a,1),18(a,1,1,2,1,2)),rewrite([7(10)])]. given #744 (W,wt=23): 26088 ((h(x) + ((x + x'')' + y))' + (x + (y + x))')' = x + y. [para(6(a,1),23334(a,1,1,1,1)),rewrite([7(7)])]. given #745 (W,wt=23): 26115 ((h(x) + ((x + (x + h(x)))' + y))' + (x + (y + x))')' = x + y. [para(6(a,1),23370(a,1,1,1,1)),rewrite([7(7)])]. given #746 (W,wt=23): 26146 ((x + ((y + y')' + (z + y)))' + (x + (z + h(y))')')' = x. [para(17(a,1),24295(a,1,1,1,1))]. given #747 (W,wt=23): 26209 ((x + ((y + y')' + (z + y)))' + ((z + h(y))' + x)')' = x. [para(17(a,1),24364(a,1,1,1,1))]. given #748 (W,wt=23): 26280 ((x + (y + h(z))')' + (x + ((z + z')' + (y + z)))')' = x. [para(17(a,1),24383(a,1,1,2,1))]. given #749 (W,wt=23): 26282 (((x + h(y))' + z)' + (z + ((y + y')' + (x + y)))')' = z. [para(17(a,1),24389(a,1,1,2,1))]. given #750 (W,wt=24): 215 ((x + y)' + (y + ((x + y)' + (y + x')'')'')')' = y. [para(18(a,1),21(a,1,1,2,1,1)),rewrite([18(22)])]. given #751 (W,wt=24): 218 ((x + y)' + (x + ((x + y)' + (y' + x)'')'')')' = x. [para(19(a,1),21(a,1,1,2,1,1)),rewrite([19(22)])]. given #752 (A,wt=31): 216 ((x + y)' + (y' + (y + (x' + (x + y)'))')')' = (y + (x' + (x + y)'))'. [para(18(a,1),21(a,1,1,2,1,2,1)),rewrite([6(7),7(7),6(10),6(18),7(18)])]. given #753 (W,wt=24): 224 ((x + y)' + (y + ((x + y)' + (x' + y)'')'')')' = y. [para(29(a,1),21(a,1,1,2,1,1)),rewrite([29(22)])]. given #754 (W,wt=24): 233 (h(x)' + (x + (h(x)' + (x + (x + x')'')'')'')')' = x. [para(25(a,1),21(a,1,1,2,1,1)),rewrite([25(28)])]. given #755 (W,wt=24): 255 ((h(x)' + y)' + (x + (y + (x + (x + (x' + h(x)')))'))')' = y. [para(62(a,1),102(a,1,1,1,1,1))]. given #756 (W,wt=24): 259 (x + (x + ((x + (y + z))' + (z + y)'))')' = (x + (y + z))'. [para(148(a,1),8(a,1,1,2)),rewrite([17(7),6(9)])]. given #757 (W,wt=24): 261 (x + (x + ((y + z)' + (x + (z + y))'))')' = (x + (z + y))'. [para(148(a,1),18(a,1,1,2)),rewrite([7(7),6(9)])]. given #758 (W,wt=24): 272 (x + ((x + (y + z))' + ((z + y)' + x))')' = (x + (y + z))'. [para(148(a,1),148(a,1,1,2)),rewrite([6(9)])]. given #759 (W,wt=24): 274 (x + (x + ((y + (x + z))' + (z + y)'))')' = (y + (x + z))'. [para(149(a,1),8(a,1,1,2)),rewrite([17(7),6(9)])]. given #760 (W,wt=24): 278 (x + (x + ((y + z)' + (z + (x + y))'))')' = (z + (x + y))'. [para(149(a,1),18(a,1,1,2)),rewrite([7(7),6(9)])]. given #761 (A,wt=28): 217 ((x + (y + ((y + z)' + (y + z')'')'))' + ((y + z)' + x)')' = x. [para(21(a,1),19(a,1,1,2,1,1))]. given #762 (W,wt=24): 286 (((x + (x + (x' + h(x)')))' + (y + x))' + (y + h(x)')')' = y. [para(62(a,1),149(a,1,1,2,1,2))]. given #763 (W,wt=24): 289 (x + ((y + (x + z))' + ((z + y)' + x))')' = (y + (x + z))'. [para(149(a,1),148(a,1,1,2)),rewrite([6(9)])]. given #764 (W,wt=24): 290 (x + ((y + z)' + (x + (x + (z + y))'))')' = (x + (z + y))'. [para(148(a,1),149(a,1,1,2)),rewrite([6(6),6(9)])]. given #765 (W,wt=24): 291 (x + ((y + z)' + (x + (z + (x + y))'))')' = (z + (x + y))'. [para(149(a,1),149(a,1,1,2)),rewrite([6(6),6(9)])]. given #766 (W,wt=24): 294 (x + (x + ((y + (z + x))' + (z + y)'))')' = (y + (z + x))'. [para(167(a,1),8(a,1,1,2)),rewrite([17(7),6(9)])]. given #767 (W,wt=24): 296 (x + (x + ((y + z)' + (z + (y + x))'))')' = (z + (y + x))'. [para(167(a,1),18(a,1,1,2)),rewrite([7(7),6(9)])]. given #768 (W,wt=24): 300 (x + ((y + (z + x))' + ((z + y)' + x))')' = (y + (z + x))'. [para(167(a,1),148(a,1,1,2)),rewrite([6(9)])]. given #769 (W,wt=24): 301 (x + ((y + z)' + (x + (z + (y + x))'))')' = (z + (y + x))'. [para(167(a,1),149(a,1,1,2)),rewrite([6(6),6(9)])]. given #770 (A,wt=31): 219 ((x + y)' + (x' + (y' + (x + (x + y)'))')')' = (y' + (x + (x + y)'))'. [para(19(a,1),21(a,1,1,2,1,2,1)),rewrite([6(7),7(7),6(10),6(18),7(18)])]. given #771 (W,wt=24): 321 ((h(x)' + y)' + ((x + (x + (x' + h(x)')))' + (y + x))')' = y. [para(62(a,1),177(a,1,1,2,1,1)),rewrite([6(15)])]. given #772 (W,wt=24): 396 ((x + h(y)')' + ((y + (y + (y' + h(y)')))' + (x + y))')' = x. [para(62(a,1),247(a,1,1,1,1,2))]. given #773 (W,wt=24): 403 (x + ((x + x)' + (h(x) + (x + x'')')'')')' = (x + x)'. [para(340(a,1),8(a,1,1,1))]. given #774 (W,wt=24): 431 (x + (x + ((h(x) + y)' + ((x + x')' + y)'))')' = (h(x) + y)'. [para(24(a,1),23(a,1,1,2,1,2,2,1)),rewrite([6(9),24(18)])]. given #775 (W,wt=24): 434 (x + (x + ((y + h(x))' + (y + (x + x')')'))')' = (y + h(x))'. [para(28(a,1),23(a,1,1,2,1,2,2,1)),rewrite([6(9),28(18)])]. given #776 (W,wt=24): 473 ((x + x)' + (x + ((x + x)' + (h(x) + (x + x)')''))')' = x. [para(346(a,1),23(a,1,1,2,1,2,2)),rewrite([6(11),17(12),346(24)])]. given #777 (W,wt=24): 505 ((x + x')' + (x' + (h(x) + x'')')')' = (h(x) + x'')'. [para(435(a,1),18(a,1,1,1)),rewrite([6(10)])]. given #778 (W,wt=24): 718 ((x + x')' + (h(x)' + (x' + (x + x')')'')')' = h(x)'. [para(10(a,1),33(a,1,1,2,1,1,1)),rewrite([6(10),10(20)])]. given #779 (A,wt=26): 220 (x + ((h(x) + y)' + (x + ((x + x')' + y)')'')')' = (h(x) + y)'. [para(24(a,1),21(a,1,1,2,1,1,1)),rewrite([24(20)])]. given #780 (W,wt=24): 895 ((x + x)' + (x + (h(x) + ((x + x)' + (x + x'')')))')' = x. [para(340(a,1),48(a,1,1,2,1,2,2)),rewrite([6(11),17(12),17(11),340(26)])]. given #781 (W,wt=24): 935 (x + ((x + (x + h(x)))' + (x + x')'')')' = (x + (x + h(x)))'. [para(846(a,1),21(a,1,1,2,1,2,1))]. given #782 (W,wt=24): 982 ((x + (x + h(x)))' + (x + (x + (x' + (x + (x + h(x)))')))')' = x. [para(923(a,1),48(a,1,1,2,1,2,2)),rewrite([6(11),6(12),7(12),7(11),923(24)])]. given #783 (W,wt=24): 986 ((x + x')' + (x' + (x + (h(x) + h(x)))')')' = (x + (h(x) + h(x)))'. [para(958(a,1),18(a,1,1,1)),rewrite([6(10)])]. given #784 (W,wt=22): 27073 ((x + x')' + (h(x) + (x' + (x + (h(x) + h(x)))')')')' = x. [para(986(a,1),57(a,1,1,2,1,2)),rewrite([958(18),6(15)])]. given #785 (W,wt=24): 1398 ((x + x)' + (x + (h(x) + ((x + x)' + (x + x)'))'')')' = x. [para(346(a,1),36(a,1,1,2,1,1)),rewrite([17(9),346(24)])]. given #786 (W,wt=24): 1548 (x + ((x + x)' + (h(x) + (x + (x + h(x)))')'')')' = (x + x)'. [para(1541(a,1),8(a,1,1,1))]. given #787 (W,wt=24): 1574 ((x + x)' + (x + (h(x) + ((x + x)' + (x + (x + h(x)))')))')' = x. [para(1541(a,1),48(a,1,1,2,1,2,2)),rewrite([6(11),17(12),17(11),1541(26)])]. given #788 (A,wt=26): 222 (x + ((y + h(x))' + (x + (y + (x + x')')')'')')' = (y + h(x))'. [para(28(a,1),21(a,1,1,2,1,1,1)),rewrite([28(20)])]. given #789 (W,wt=24): 1995 (x + (y + (x + (y + (y + (y' + (x + h(y))'))))'))' = (x + h(y))'. [para(118(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),7(6),6(11),7(11)])]. given #790 (W,wt=24): 2006 (x + (y + (y + (y + (y' + (x + (x + h(y))'))))'))' = (x + h(y))'. [para(118(a,1),148(a,1,1,2)),rewrite([7(7),7(6),6(8),7(8),7(7),7(6),6(11),7(11)])]. given #791 (W,wt=24): 2063 (x + (y + (x + (y + (x + (x' + (y + h(x))'))))'))' = (y + h(x))'. [para(126(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),7(6),6(11),7(11)])]. given #792 (W,wt=24): 2150 (x + (x + ((h(x) + y)' + (y + (x + x')')'))')' = (h(x) + y)'. [para(263(a,1),8(a,1,1,2)),rewrite([17(10),6(12)])]. given #793 (W,wt=24): 2154 (x + (x + ((y + (x + x')')' + (h(x) + y)'))')' = (h(x) + y)'. [para(263(a,1),18(a,1,1,2)),rewrite([7(10),6(12)])]. given #794 (W,wt=24): 2187 (x + (x + ((y + h(x))' + ((x + x')' + y)'))')' = (y + h(x))'. [para(264(a,1),8(a,1,1,2)),rewrite([17(10),6(12)])]. given #795 (W,wt=24): 2191 (x + (x + (((x + x')' + y)' + (y + h(x))'))')' = (y + h(x))'. [para(264(a,1),18(a,1,1,2)),rewrite([7(10),6(12)])]. given #796 (W,wt=24): 2378 (x + (y + (y + (y' + (x + (y + (x + h(y))'))))'))' = (x + h(y))'. [para(486(a,1),19(a,1,1,2)),rewrite([6(8),7(8),7(7),7(6),6(11),7(11)])]. given #797 (A,wt=28): 223 (((x + y)' + z)' + (x + (((x + y)' + (x + y')'')' + z))')' = z. [para(21(a,1),29(a,1,1,2,1,1)),rewrite([7(10),6(16)])]. given #798 (W,wt=24): 2458 (x + (y + (x + (x + (x' + (y + (y + h(x))'))))'))' = (y + h(x))'. [para(492(a,1),19(a,1,1,2)),rewrite([6(8),7(8),7(7),7(6),6(11),7(11)])]. given #799 (W,wt=24): 3096 (x + (y + (x + (y + (x + (x' + (h(x) + y)'))))'))' = (h(x) + y)'. [para(1206(a,1),19(a,1,1,2)),rewrite([6(8),7(8),7(7),7(6),6(11),7(11)])]. given #800 (W,wt=24): 3345 (x + (h(x) + ((x + x)' + (x + (h(x) + x''))'))')' = (x + x)'. [para(1467(a,1),8(a,1,1,2)),rewrite([17(11),6(13)])]. given #801 (W,wt=24): 3400 (x + (h(x) + ((x + x)' + (x + (x + h(x))'')'))')' = (x + x)'. [para(1477(a,1),8(a,1,1,2)),rewrite([17(11),6(13)])]. given #802 (W,wt=24): 3512 (x + (h(x) + ((x + x)' + (h(x) + (x + x)'')'))')' = (x + x)'. [para(1522(a,1),8(a,1,1,2)),rewrite([17(11),6(13)])]. given #803 (W,wt=17): 27307 (x + (h(x) + (x + x)'')')' = (x + x')'. [para(3512(a,1),159(a,1,1,2,1,2)),rewrite([48(15),6(12),8(13),6(7)])]. given #804 (W,wt=19): 27310 ((x + x')' + (x + (h(x) + (x + x)''))')' = x. [para(27307(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #805 (W,wt=19): 27335 (x + (h(x) + (h(x) + (x + x)''))')' = (x + x')'. [para(27307(a,1),48(a,1,1,2,1,2,2)),rewrite([6(9),17(9),58(10),27307(18)])]. given #806 (A,wt=31): 225 ((x + y)' + (y' + (x' + (y + (x + y)'))')')' = (x' + (y + (x + y)'))'. [para(29(a,1),21(a,1,1,2,1,2,1)),rewrite([6(7),7(7),6(10),6(18),7(18)])]. given #807 (W,wt=21): 27308 ((x + x')' + (x + (h(x) + (x + x)'')'')')' = x. [para(27307(a,1),8(a,1,1,1))]. given #808 (W,wt=21): 27329 (x + (h(x) + (h(x) + (x + x)'')'')')' = (x + x')'. [para(27307(a,1),23(a,1,1,2,1,2,2)),rewrite([6(11),24(12),27307(20)])]. given #809 (W,wt=21): 27442 ((x + x')' + (x + (h(x) + (h(x) + (x + x)'')))')' = x. [para(27307(a,1),845(a,1,1,1)),rewrite([27307(16),6(12),17(12),58(13)])]. given #810 (W,wt=21): 27481 ((x + x)' + (h(x) + (x + (h(x) + (x + x)''))')')' = x. [para(27310(a,1),57(a,1,1,2,1,2)),rewrite([6(13)])]. given #811 (W,wt=21): 27578 (x + (h(x) + (h(x) + (h(x) + (x + x)'')))')' = (x + x')'. [para(27335(a,1),54(a,1,1,2,1,2,2)),rewrite([10(11),6(9),27335(22)])]. given #812 (W,wt=23): 27383 ((x + x')' + (x + (h(x) + (h(x) + (x + x)'')''))')' = x. [para(27307(a,1),423(a,1,1,1)),rewrite([27307(18),6(14),24(15)])]. given #813 (W,wt=23): 27447 ((x + x')' + (h(x) + (x + (h(x) + (x + x)''))'')')' = x. [para(27307(a,1),441(a,1,1,1)),rewrite([27307(11),6(12),24(16)])]. given #814 (W,wt=23): 27448 ((x + x')' + (x + (h(x) + (h(x) + (x + x)''))'')')' = x. [para(27307(a,1),843(a,1,1,1)),rewrite([27307(16),6(12),17(12),58(13)])]. given #815 (A,wt=28): 226 ((x + (y + z)')' + (y + (((y + z)' + (y + z')'')' + x))')' = x. [para(21(a,1),30(a,1,1,1,1,2)),rewrite([7(14)])]. given #816 (W,wt=23): 27545 (x + (h(x) + (h(x) + (h(x) + (x + x)''))'')')' = (x + x')'. [para(27310(a,1),441(a,1,1,1)),rewrite([27310(15),6(13),17(13),17(12),58(13),17(14),24(14)])]. given #817 (W,wt=23): 27630 ((x + x')' + (x + (h(x) + (h(x) + (h(x) + (x + x)''))))')' = x. [para(27335(a,1),857(a,1,1,1)),rewrite([27335(20),10(14),6(12)])]. given #818 (W,wt=23): 27656 ((x + x)' + (h(x) + (x + (h(x) + (x + x)'')'')')')' = x. [para(27308(a,1),57(a,1,1,2,1,2)),rewrite([6(15)])]. given #819 (W,wt=23): 27668 (x + (h(x) + (h(x) + (h(x) + (x + x)'')''))')' = (x + x')'. [para(27308(a,1),845(a,1,1,1)),rewrite([27308(28),6(15),17(16),17(15),24(15),17(14),17(13),58(14)])]. given #820 (W,wt=23): 27711 ((x + x)' + (h(x) + (x + (h(x) + (h(x) + (x + x)'')))')')' = x. [para(27442(a,1),57(a,1,1,2,1,2)),rewrite([6(15)])]. given #821 (W,wt=23): 27773 (x + (h(x) + (h(x) + (h(x) + (h(x) + (x + x)''))))')' = (x + x')'. [para(27578(a,1),54(a,1,1,2,1,2,2)),rewrite([10(13),6(11),27578(26)])]. given #822 (W,wt=24): 3567 (x + (h(x) + ((x + x)' + (x + (x + (h(x) + h(x))))'))')' = (x + x)'. [para(1542(a,1),8(a,1,1,2)),rewrite([17(11),6(13)])]. given #823 (W,wt=24): 3912 (x + (y + (x + (x + (x' + (y + (h(x) + y)'))))'))' = (h(x) + y)'. [para(1623(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),7(6),6(11),7(11)])]. given #824 (A,wt=25): 227 ((x + y')' + (x + ((x + y')' + (y + x)'')'')')' = x. [para(30(a,1),21(a,1,1,2,1,1)),rewrite([30(23)])]. given #825 (W,wt=24): 4516 (h(x) + ((h(x) + y)' + ((x + x')' + (y' + x)))')' = (h(x) + y)'. [para(1955(a,1),8(a,1,1,2)),rewrite([6(13)])]. given #826 (W,wt=24): 4521 (h(x) + ((x + x')' + (y' + (x + (h(x) + y)')))')' = (h(x) + y)'. [para(1955(a,1),18(a,1,1,2)),rewrite([7(10),7(9),6(13)])]. given #827 (W,wt=24): 4642 (x + (y + (x + (y + (y + (y' + (h(y) + x)'))))'))' = (h(y) + x)'. [para(1958(a,1),19(a,1,1,2)),rewrite([6(8),7(8),7(7),7(6),6(11),7(11)])]. given #828 (W,wt=24): 4652 (x + (y + (y + (y + (y' + (x + (h(y) + x)'))))'))' = (h(y) + x)'. [para(1958(a,1),176(a,1,1,2)),rewrite([7(7),7(6),6(8),7(8),7(7),7(6),6(11),7(11)])]. given #829 (W,wt=24): 4785 (x + (y + (x + (x + (y + (x' + (y + h(x))'))))'))' = (y + h(x))'. [para(2064(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),7(6),6(11),7(11)])]. given #830 (W,wt=24): 4820 (h(x) + ((y + h(x))' + ((x + x')' + (y' + x)))')' = (y + h(x))'. [para(2333(a,1),8(a,1,1,2)),rewrite([6(13)])]. given #831 (W,wt=24): 4824 (h(x) + ((x + x')' + (y' + (x + (y + h(x))')))')' = (y + h(x))'. [para(2333(a,1),18(a,1,1,2)),rewrite([7(10),7(9),6(13)])]. given #832 (W,wt=24): 4944 (x + (y + (y + (y' + (x + (y + (h(y) + x)'))))'))' = (h(y) + x)'. [para(2337(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),7(6),6(11),7(11)])]. given #833 (A,wt=32): 228 ((x + y')' + (x' + (y + (x + (x + y')'))')')' = (y + (x + (x + y')'))'. [para(30(a,1),21(a,1,1,2,1,2,1)),rewrite([6(8),7(8),6(11),6(19),7(19)])]. given #834 (W,wt=24): 5112 (x + (y + (x + (x + (y + (x' + (h(x) + y)'))))'))' = (h(x) + y)'. [para(3091(a,1),19(a,1,1,2)),rewrite([6(8),7(8),7(7),7(6),6(11),7(11)])]. given #835 (W,wt=24): 6115 ((x + x')' + (h(x) + (h(x) + (h(x) + (x' + x')'))'')')' = x. [para(1200(a,1),23(a,1,1,2,1,2,2)),rewrite([6(17),17(18),24(18),1200(32)])]. given #836 (W,wt=24): 6564 ((x + x')' + (h(x) + (h(x) + (x' + (x + h(x))')')'')')' = x. [para(6052(a,1),23(a,1,1,2,1,2,2)),rewrite([6(17),17(18),24(18),6052(32)])]. given #837 (W,wt=24): 11679 (x + (x + ((x + h(x))' + (x + x'')'))')' = (x + x'')'. [para(42(a,1),922(a,1,1,2)),rewrite([6(3),6(9),7(9),6(11),6(15)])]. given #838 (W,wt=24): 11707 (h(x)' + (x + (h(x)' + (x + (x + (x + h(x))'))'')'')')' = x. [para(11677(a,1),21(a,1,1,2,1,1)),rewrite([11677(28)])]. given #839 (W,wt=24): 11984 ((x + x)' + (x + (x + ((x + x)' + (x + h(x))'))'')')' = x. [para(11676(a,1),8(a,1,1,1))]. given #840 (W,wt=24): 12223 ((x + (y + y'))' + (x + (h(y) + (y' + y')'))')' = x + y. [para(18(a,1),122(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #841 (W,wt=24): 16504 ((x + h(x)')' + (h(x) + (x' + (h(x)' + (x + x')'))')')' = x. [para(572(a,1),57(a,1,1,2,1,2)),rewrite([6(17)])]. given #842 (A,wt=28): 229 (((x + y)' + z)' + (z + (x + ((x + y)' + (x + y')'')'))')' = z. [para(21(a,1),42(a,1,1,1,1,1))]. given #843 (W,wt=24): 16632 ((x + x')' + (h(x) + (h(x) + (h(x) + (x' + x')')''))')' = x. [para(1193(a,1),48(a,1,1,2,1,2,2)),rewrite([6(17),17(18),17(17),58(18),1193(34)])]. Low Water (keep, Weight): wt=34 given #844 (W,wt=24): 16636 ((x + x)' + (h(x) + (h(x) + (h(x) + (x' + x')')'')')')' = x. [para(1193(a,1),57(a,1,1,2,1,2)),rewrite([6(17)])]. given #845 (W,wt=24): 16688 ((x + x')' + (h(x) + (h(x) + (h(x) + (h(x) + (x' + x')'))))')' = x. [para(6123(a,1),54(a,1,1,2,1,2,2)),rewrite([6(17),10(17),6(15),6123(34)])]. given #846 (W,wt=24): 16691 ((x + x)' + (h(x) + (h(x) + (h(x) + (h(x) + (x' + x')')))')')' = x. [para(6123(a,1),57(a,1,1,2,1,2)),rewrite([6(17)])]. given #847 (W,wt=24): 16746 ((x + x')' + (h(x) + (h(x) + (h(x) + (x' + (x + h(x))')')))')' = x. [para(6569(a,1),54(a,1,1,2,1,2,2)),rewrite([6(17),10(17),6(15),6569(34)])]. given #848 (W,wt=24): 16749 ((x + x)' + (h(x) + (h(x) + (h(x) + (x' + (x + h(x))')'))')')' = x. [para(6569(a,1),57(a,1,1,2,1,2)),rewrite([6(17)])]. given #849 (W,wt=24): 17187 (x + (h(x) + ((x' + y)' + (x' + y')'))')' = (x + x')'. [para(22(a,1),159(a,1,1,2)),rewrite([6(12)])]. given #850 (W,wt=24): 17207 (x + (h(x) + ((y + x')' + (x' + y')'))')' = (x + x')'. [para(34(a,1),159(a,1,1,2)),rewrite([6(12)])]. given #851 (A,wt=25): 230 ((x' + y)' + (y + ((x' + y)' + (y + x)'')'')')' = y. [para(42(a,1),21(a,1,1,2,1,1)),rewrite([42(23)])]. given #852 (W,wt=24): 17227 (x + (h(x) + ((x' + y)' + (y' + x')'))')' = (x + x')'. [para(45(a,1),159(a,1,1,2)),rewrite([6(12)])]. given #853 (W,wt=24): 17234 (x + (h(x) + (h(x) + ((x + x)' + (x + x)'))')')' = (x + x')'. [para(370(a,1),159(a,1,1,2,1,2)),rewrite([6(17),8(18),6(12)])]. given #854 (W,wt=24): 17236 (x + (h(x) + ((y + x')' + (y' + x')'))')' = (x + x')'. [para(72(a,1),159(a,1,1,2)),rewrite([6(12)])]. given #855 (W,wt=24): 17239 (x + (h(x) + ((x' + y')' + (y + x')'))')' = (x + x')'. [para(87(a,1),159(a,1,1,2)),rewrite([6(12)])]. given #856 (W,wt=24): 17240 (x + (h(x) + ((y' + x')' + (x' + y)'))')' = (x + x')'. [para(99(a,1),159(a,1,1,2)),rewrite([6(12)])]. given #857 (W,wt=24): 17244 (x + (h(x) + (x + ((x + x)' + (x + h(x))'))')')' = (x + x')'. [para(11676(a,1),159(a,1,1,2,1,2)),rewrite([6(17),8(18),6(12)])]. given #858 (W,wt=24): 17255 (x + (h(x) + (x + (x' + (x + (x + h(x)))'))')')' = (x + x')'. [para(959(a,1),159(a,1,1,2,1,2)),rewrite([6(19),923(20),6(12)])]. given #859 (W,wt=24): 17260 ((x + x')' + (x' + (x + (x + h(x)))')')' = (x + (x + h(x)))'. [para(17256(a,1),18(a,1,1,1)),rewrite([6(9)])]. given #860 (A,wt=32): 231 ((x' + y)' + (y' + (y + (x + (x' + y)'))')')' = (y + (x + (x' + y)'))'. [para(42(a,1),21(a,1,1,2,1,2,1)),rewrite([6(8),7(8),6(11),6(19),7(19)])]. given #861 (W,wt=22): 28617 ((x + x')' + (h(x) + (x' + (x + (x + h(x)))')')')' = x. [para(17260(a,1),57(a,1,1,2,1,2)),rewrite([17256(16),6(14)])]. given #862 (W,wt=24): 18146 (x + (h(x) + ((x + x)' + (x + (x + (x + h(x))))'))')' = (x + x)'. [para(17479(a,1),8(a,1,1,2)),rewrite([17(10),6(12)])]. given #863 (W,wt=24): 19950 (h(x)' + (x + (h(x)' + (x + (x + (h(x) + x'')'))''))')' = x. [para(19923(a,1),23(a,1,1,2,1,2,2)),rewrite([6(14),17(15),19923(30)])]. given #864 (W,wt=24): 19964 (h(x)' + (x + (x + (x + (h(x)' + (h(x) + x'')')))'')')' = x. [para(19923(a,1),36(a,1,1,2,1,1)),rewrite([17(12),17(11),19923(30)])]. given #865 (W,wt=24): 20160 ((x + x)' + (x + (x + ((x + x)' + (h(x) + x'')')))')' = x. [para(19922(a,1),8(a,1,1,2)),rewrite([6(14)])]. given #866 (W,wt=24): 21143 (h(x)' + (x + (h(x)' + (x + (x + (x + (h(x) + h(x)))'))''))')' = x. [para(21117(a,1),23(a,1,1,2,1,2,2)),rewrite([6(14),17(15),21117(30)])]. given #867 (W,wt=24): 21156 (h(x)' + (x + (x + (x + (h(x)' + (x + (h(x) + h(x)))')))'')')' = x. [para(21117(a,1),36(a,1,1,2,1,1)),rewrite([17(12),17(11),21117(30)])]. given #868 (W,wt=24): 21359 ((x + x)' + (x + (x + ((x + x)' + (x + (h(x) + h(x)))')))')' = x. [para(21116(a,1),8(a,1,1,2)),rewrite([6(14)])]. given #869 (A,wt=34): 232 ((x + (y + z))' + (x + (y + ((x + (y + z))' + (x + (y + z'))'')''))')' = x + y. [para(20(a,1),21(a,1,1,2,1,1)),rewrite([7(16),20(28)])]. given #870 (W,wt=24): 23336 ((x + (h(y) + (y' + y')'))' + (y + (x + y'))')' = y + x. [para(18(a,1),193(a,1,1,2,1,2,2))]. given #871 (W,wt=24): 23476 (h(x)' + (x + (h(x)' + (x + (x + (x + (x + h(x)))'))''))')' = x. [para(23450(a,1),23(a,1,1,2,1,2,2)),rewrite([6(13),17(14),23450(28)])]. given #872 (W,wt=24): 23489 (h(x)' + (x + (x + (x + (h(x)' + (x + (x + h(x)))')))'')')' = x. [para(23450(a,1),36(a,1,1,2,1,1)),rewrite([17(11),17(10),23450(28)])]. given #873 (W,wt=24): 23700 ((x + x)' + (x + (x + ((x + x)' + (x + (x + h(x)))')))')' = x. [para(23449(a,1),8(a,1,1,2)),rewrite([6(13)])]. given #874 (W,wt=24): 26072 ((x + y)' + (y + ((y + x)' + (y + x')'')'')')' = y. [para(6(a,1),209(a,1,1,1,1))]. given #875 (W,wt=24): 26073 ((x + y)' + (x + ((y + x)' + (x + y')'')'')')' = x. [para(6(a,1),209(a,1,1,2,1,2,1,1,1,1))]. given #876 (W,wt=24): 26230 (x + (x + (h(x)' + ((x + (x + x'))' + h(x)'')'))')' = h(x)'. [para(26(a,1),210(a,1,1,1)),rewrite([10(10),17(13)])]. given #877 (W,wt=24): 26528 ((x + x')' + (h(x) + (h(x) + (x' + (h(x) + x'')')'))')' = x. [para(26511(a,1),48(a,1,1,2,1,2,2)),rewrite([6(17),17(18),17(17),58(18),26511(34)])]. given #878 (A,wt=33): 234 (h(x)' + (x' + (x + (h(x)' + (x + x')''))')')' = (x + (h(x)' + (x + x')''))'. [para(25(a,1),21(a,1,1,2,1,2,1)),rewrite([17(10),6(13),17(24)])]. given #879 (W,wt=24): 26530 ((x + x)' + (h(x) + (h(x) + (x' + (h(x) + x'')')')')')' = x. [para(26511(a,1),57(a,1,1,2,1,2)),rewrite([6(17)])]. given #880 (W,wt=24): 26918 ((x + y)' + (y + ((y + x)' + (x' + y)'')'')')' = y. [para(6(a,1),218(a,1,1,1,1))]. given #881 (W,wt=24): 26919 ((x + y)' + (x + ((y + x)' + (y' + x)'')'')')' = x. [para(6(a,1),218(a,1,1,2,1,2,1,1,1,1))]. given #882 (W,wt=24): 27090 ((x + x')' + (h(x) + (h(x) + (x' + (x + (h(x) + h(x)))')'))')' = x. [para(27073(a,1),48(a,1,1,2,1,2,2)),rewrite([6(17),17(18),17(17),58(18),27073(34)])]. given #883 (W,wt=24): 27092 ((x + x)' + (h(x) + (h(x) + (x' + (x + (h(x) + h(x)))')')')')' = x. [para(27073(a,1),57(a,1,1,2,1,2)),rewrite([6(17)])]. given #884 (W,wt=24): 27119 (x + (y + (y + (x + (y + (y' + (x + h(y))'))))'))' = (x + h(y))'. [para(17(a,1),1995(a,1,1,2,2,1))]. given #885 (W,wt=24): 27120 (x + (y + (y + (x + (x + (x' + (y + h(x))'))))'))' = (y + h(x))'. [para(17(a,1),1995(a,1,1))]. given #886 (W,wt=24): 27138 (x + (y + (y + (y + (x + (y' + (x + h(y))'))))'))' = (x + h(y))'. [para(17(a,1),2006(a,1,1,2,2,1,2,2))]. given #887 (A,wt=25): 235 (x + (h(x)' + (x + (x + (x + (x' + h(x)')))'')'')')' = h(x)'. [para(62(a,1),21(a,1,1,2,1,1)),rewrite([62(26)])]. given #888 (W,wt=24): 27226 (x + (y + (x + (x' + (y + (x + (y + h(x))'))))'))' = (y + h(x))'. [para(17(a,1),2378(a,1,1))]. given #889 (W,wt=24): 27252 (x + (y + (y + (x + (x + (x' + (h(x) + y)'))))'))' = (h(x) + y)'. [para(17(a,1),3096(a,1,1,2,2,1))]. given #890 (W,wt=24): 27253 (x + (y + (y + (x + (y + (y' + (h(y) + x)'))))'))' = (h(y) + x)'. [para(17(a,1),3096(a,1,1))]. given #891 (W,wt=24): 28066 (x + (y + (y + (y + (x + (y' + (h(y) + x)'))))'))' = (h(y) + x)'. [para(17(a,1),4652(a,1,1,2,2,1,2,2))]. given #892 (W,wt=24): 28124 (x + (y + (x + (x' + (y + (x + (h(x) + y)'))))'))' = (h(x) + y)'. [para(17(a,1),4944(a,1,1))]. given #893 (W,wt=24): 28225 ((x + (x' + y))' + (y + (h(x) + (x' + x')'))')' = y + x. [para(6(a,1),12223(a,1,1,1,1)),rewrite([7(3)])]. given #894 (W,wt=24): 28226 ((x + (y + y'))' + (h(y) + ((y' + y')' + x))')' = x + y. [para(6(a,1),12223(a,1,1,2,1)),rewrite([7(11)])]. given #895 (W,wt=24): 28231 ((x + (y + x'))' + (y + (h(x) + (x' + x')'))')' = y + x. [para(17(a,1),12223(a,1,1,1,1))]. given #896 (A,wt=33): 236 (x + (h(x)'' + (x + (x + (x + (x' + h(x)'))))')')' = (x + (x + (x + (x' + h(x)'))))'. [para(62(a,1),21(a,1,1,2,1,2,1)),rewrite([6(12)])]. given #897 (W,wt=24): 28232 ((x + (y + y'))' + (h(y) + (x + (y' + y')'))')' = x + y. [para(17(a,1),12223(a,1,1,2,1))]. given #898 (W,wt=24): 28635 ((x + x')' + (h(x) + (h(x) + (x' + (x + (x + h(x)))')'))')' = x. [para(28617(a,1),48(a,1,1,2,1,2,2)),rewrite([6(16),17(17),17(16),58(17),28617(32)])]. given #899 (W,wt=24): 28637 ((x + x)' + (h(x) + (h(x) + (x' + (x + (x + h(x)))')')')')' = x. [para(28617(a,1),57(a,1,1,2,1,2)),rewrite([6(16)])]. given #900 (W,wt=24): 28652 ((h(x) + ((x' + x')' + y))' + (x + (y + x'))')' = x + y. [para(6(a,1),23336(a,1,1,1,1)),rewrite([7(7)])]. given #901 (W,wt=24): 28653 ((x + (h(y) + (y' + y')'))' + (y + (y' + x))')' = y + x. [para(6(a,1),23336(a,1,1,2,1,2))]. given #902 (W,wt=24): 28656 ((x + (y + x'))' + (h(x) + (y + (x' + x')'))')' = x + y. [para(17(a,1),23336(a,1,1,1,1)),rewrite([6(13)])]. given #903 (W,wt=24): 28951 ((x + (x' + y))' + (h(x) + ((x' + x')' + y))')' = y + x. [para(6(a,1),28225(a,1,1,2,1)),rewrite([7(11)])]. given #904 (W,wt=24): 28956 ((x + (x' + y))' + (h(x) + (y + (x' + x')'))')' = y + x. [para(17(a,1),28225(a,1,1,2,1))]. given #905 (A,wt=28): 237 ((x + (y + z)')' + (y + (x + ((y + z)' + (y + z')'')'))')' = x. [para(21(a,1),27(a,1,1,2,1,2)),rewrite([6(16)])]. given #906 (W,wt=24): 28976 ((h(x) + ((x' + x')' + y))' + (y + (x + x'))')' = y + x. [para(6(a,1),28226(a,1,1))]. given #907 (W,wt=24): 28979 ((x + (y + x'))' + (h(x) + ((x' + x')' + y))')' = y + x. [para(17(a,1),28226(a,1,1,1,1))]. given #908 (W,wt=24): 29084 ((h(x) + (y + (x' + x')'))' + (x + (x' + y))')' = x + y. [para(17(a,1),28653(a,1,1,1,1))]. given #909 (W,wt=25): 262 (x + (x + (y + (z + (x + (z + y)')')))')' = (x + (z + y)')'. [para(148(a,1),19(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #910 (W,wt=25): 270 (x + (y + (x + (z + (x + (z + y)')')))')' = (x + (z + y)')'. [para(86(a,1),148(a,1,1,2)),rewrite([7(6),6(7),7(7),7(6),6(9)])]. given #911 (W,wt=25): 271 (x + (x + (y + (z + ((z + y)' + x)')))')' = ((z + y)' + x)'. [para(102(a,1),148(a,1,1,2)),rewrite([7(6),6(7),7(7),7(6),6(9)])]. given #912 (W,wt=25): 297 (x + (y + (z + (x + (x + (z + y)')')))')' = (x + (z + y)')'. [para(167(a,1),19(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #913 (W,wt=25): 306 (x + (y + (x + (z + ((z + y)' + x)')))')' = ((z + y)' + x)'. [para(70(a,1),176(a,1,1,2)),rewrite([7(6),6(7),7(7),7(6),6(9)])]. given #914 (A,wt=30): 238 ((x + (y + z))' + (y + ((x + (y + z))' + (y + (x + z)')'')'')')' = y. [para(27(a,1),21(a,1,1,2,1,1)),rewrite([27(27)])]. given #915 (W,wt=25): 308 (x + (x + (y + (z + (x + (y + z)')')))')' = (x + (y + z)')'. [para(149(a,1),176(a,1,1,2)),rewrite([7(6),6(7),7(7),7(6),6(9)])]. given #916 (W,wt=25): 309 (x + (y + (z + (x + ((z + y)' + x)')))')' = ((z + y)' + x)'. [para(176(a,1),176(a,1,1,2)),rewrite([7(6),6(7),7(7),7(6),6(9)])]. given #917 (W,wt=25): 324 (x + (x + (y + (z + ((y + z)' + x)')))')' = ((y + z)' + x)'. [para(177(a,1),176(a,1,1,2)),rewrite([7(6),6(7),7(7),7(6),6(9)])]. given #918 (W,wt=25): 371 (x + ((x + x)'' + (h(x) + (x + x)')')')' = (h(x) + (x + x)')'. [para(346(a,1),18(a,1,1,1)),rewrite([6(9)])]. given #919 (W,wt=25): 404 ((x + y)' + (x + ((y + y)' + (h(y) + (y + y'')')'))')' = x. [para(340(a,1),8(a,1,1,2,1,2)),rewrite([6(15)])]. given #920 (W,wt=25): 407 (((x + x)' + ((h(x) + (x + x'')')' + y))' + (y + x)')' = y. [para(340(a,1),18(a,1,1,2,1,2)),rewrite([7(11)])]. given #921 (W,wt=25): 408 ((x + ((y + y)' + (h(y) + (y + y'')')'))' + (y + x)')' = x. [para(340(a,1),19(a,1,1,2,1,1))]. given #922 (W,wt=25): 410 ((x + y)' + ((x + x)' + ((h(x) + (x + x'')')' + y))')' = y. [para(340(a,1),29(a,1,1,2,1,1)),rewrite([7(11),6(15)])]. given #923 (A,wt=30): 239 ((x + (y + z))' + (z + ((x + (y + z))' + (z + (x + y)')'')'')')' = z. [para(31(a,1),21(a,1,1,2,1,1)),rewrite([31(27)])]. given #924 (W,wt=25): 411 ((x + y)' + ((y + y)' + ((h(y) + (y + y'')')' + x))')' = x. [para(340(a,1),30(a,1,1,1,1,2)),rewrite([7(13)])]. given #925 (W,wt=25): 412 ((x + y)' + (y + ((x + x)' + (h(x) + (x + x'')')'))')' = y. [para(340(a,1),42(a,1,1,1,1,1))]. given #926 (W,wt=25): 414 ((x + y)' + ((y + y)' + (x + (h(y) + (y + y'')')'))')' = x. [para(340(a,1),27(a,1,1,2,1,2)),rewrite([6(15)])]. given #927 (W,wt=25): 415 ((x + y)' + ((x + x)' + (y + (h(x) + (x + x'')')'))')' = y. [para(340(a,1),49(a,1,1,2,1,1)),rewrite([6(15)])]. given #928 (W,wt=25): 417 ((x + y)' + ((h(y) + (y + y'')')' + (x + (y + y)'))')' = x. [para(340(a,1),149(a,1,1,2,1,2)),rewrite([6(15)])]. given #929 (W,wt=25): 418 ((x + y)' + ((h(x) + (x + x'')')' + (y + (x + x)'))')' = y. [para(340(a,1),177(a,1,1,2,1,1)),rewrite([6(15)])]. given #930 (W,wt=25): 489 ((h(x) + y)' + ((x + x')' + (y + x'))')' = (x + x')' + y. [para(24(a,1),32(a,1,1,1,1))]. given #931 (W,wt=25): 491 ((x + h(y))' + (x + (y' + (y + y')'))')' = x + (y + y')'. [para(28(a,1),32(a,1,1,1,1)),rewrite([6(8)])]. given #932 (A,wt=28): 240 ((x + (y + ((x + z)' + (x + z')'')'))' + ((x + z)' + y)')' = y. [para(21(a,1),49(a,1,1,2,1,1))]. given #933 (W,wt=25): 522 ((x + y)' + (x + ((y + y')' + (y + (h(y) + y''))'))')' = x. [para(435(a,1),22(a,1,1,2,1,2,2)),rewrite([6(12)])]. given #934 (W,wt=25): 527 (x + ((x + x')' + (x + (h(x) + x''))'')')' = (x + x')'. [para(504(a,1),8(a,1,1,1))]. given #935 (W,wt=25): 529 (((x + x')' + ((x + (h(x) + x''))' + y))' + (y + x)')' = y. [para(504(a,1),18(a,1,1,2,1,2)),rewrite([7(11)])]. given #936 (W,wt=25): 530 ((x + ((y + y')' + (y + (h(y) + y''))'))' + (y + x)')' = x. [para(504(a,1),19(a,1,1,2,1,1))]. given #937 (W,wt=25): 532 ((x + y)' + ((x + x')' + ((x + (h(x) + x''))' + y))')' = y. [para(504(a,1),29(a,1,1,2,1,1)),rewrite([7(11),6(15)])]. given #938 (W,wt=25): 533 ((x + y)' + ((y + y')' + ((y + (h(y) + y''))' + x))')' = x. [para(504(a,1),30(a,1,1,1,1,2)),rewrite([7(13)])]. given #939 (W,wt=25): 534 (