============================== Prover9 =============================== Prover9 (32) version June-2007-, 12 June 2007. Process 10669 was started by mccune on cleo, Wed Jun 13 10:39:44 2007 The command was "prover9 -f s1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file s1.in assign(max_weight,30). set(restrict_denials). assign(eq_defs,fold). list(weights). weight(g(_)) = 1. weight(g(x)) = 1000. 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). g(x) = (x + x')' # label(definition_g). h(x) = x + (x + (x + g(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]. g(x) = (x + x')' # label(definition_g). [assumption]. h(x) = x + (x + (x + g(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, +, ', g, h ]). After inverse_order: (no changes). Folding symbols: g/1 h/1. After fold_eq: Function symbol precedence: function_order([ c1, c2, g, 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): 13 (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [deny(1)]. restricted denial: (wt=5): 14 x + y != x # answer(Winker1a). [deny(2)]. restricted denial: (wt=5): 15 x + y != y # answer(Winker1b). [deny(3)]. restricted denial: (wt=7): 16 (x + y)' != x' # answer(Winker2a). [deny(4)]. restricted denial: (wt=7): 17 (x + y)' != y' # answer(Winker2b). [deny(5)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 13 (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [deny(1)]. 14 x + y != x # answer(Winker1a). [deny(2)]. 15 x + y != y # answer(Winker1b). [deny(3)]. 16 (x + y)' != x' # answer(Winker2a). [deny(4)]. 17 (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')' = g(x). [copy(9),flip(a)]. 12 x + (x + (x + g(x))) = h(x). [copy(11),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')' = g(x). [copy(9),flip(a)]. 12 x + (x + (x + g(x))) = h(x). [copy(11),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: 18 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=7): 10 (x + x')' = g(x). [copy(9),flip(a)]. given #5 (I,wt=9): 12 x + (x + (x + g(x))) = h(x). [copy(11),flip(a)]. given #6 (A,wt=11): 19 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),rewrite([7(2)])]. given #7 (T,wt=9): 28 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. given #8 (T,wt=7): 37 (g(x) + h(x)')' = x. [back_rewrite(31),rewrite([36(8),6(4)])]. given #9 (T,wt=9): 40 (x + (g(x) + h(x))')' = g(x). [para(37(a,1),8(a,1,1,2)),rewrite([6(5)])]. given #10 (T,wt=11): 26 (g(x) + (x + x'')')' = x. [para(10(a,1),8(a,1,1,1))]. given #11 (A,wt=13): 20 ((x + y)' + (y + x')')' = y. [para(6(a,1),8(a,1,1,1,1))]. given #12 (T,wt=11): 36 (x + (x + (x + g(x)))')' = g(x). [para(28(a,1),8(a,1,1,2)),rewrite([19(3),6(2),6(5)])]. given #13 (T,wt=11): 38 (x + (g(x) + h(x)'')')' = g(x). [para(37(a,1),8(a,1,1,1))]. given #14 (T,wt=11): 43 (g(x) + (x + (g(x) + h(x)))')' = x. [para(40(a,1),8(a,1,1,2)),rewrite([6(7)])]. given #15 (T,wt=12): 56 (g(x) + (x' + x')')' = x'. [para(10(a,1),20(a,1,1,1))]. given #16 (A,wt=13): 21 ((x + y)' + (y' + x)')' = x. [para(6(a,1),8(a,1,1,2,1))]. given #17 (T,wt=12): 62 (x + (g(x)' + h(x)')')' = h(x)'. [para(37(a,1),20(a,1,1,1)),rewrite([6(5)])]. given #18 (T,wt=13): 29 h(x) + y = x + (x + (x + (g(x) + y))). [para(12(a,1),7(a,1,1)),rewrite([7(6),7(5)])]. given #19 (T,wt=13): 30 x + h(y) = y + (y + (g(y) + (x + y))). [para(12(a,1),7(a,2,2)),rewrite([19(5),19(4),6(3)]),flip(a)]. given #20 (T,wt=13): 33 x + (y + (x + (x + g(x)))) = y + h(x). [para(12(a,1),19(a,1,2)),flip(a)]. given #21 (A,wt=19): 22 ((x + (y + z))' + (x + (y + z'))')' = x + y. [para(7(a,1),8(a,1,1,1,1)),rewrite([7(6)])]. given #22 (T,wt=13): 34 (x + (g(x) + (x + x)'')')' = g(x). [para(28(a,1),8(a,1,1,1))]. given #23 (T,wt=13): 41 (g(x) + (x + (g(x) + h(x))'')')' = x. [para(40(a,1),8(a,1,1,1))]. given #24 (T,wt=13): 46 (x + (x + (g(x) + x''))')' = g(x). [para(26(a,1),8(a,1,1,2)),rewrite([19(5),6(7)])]. given #25 (T,wt=13): 47 ((x + y)' + (x' + y)')' = y. [para(6(a,1),20(a,1,1,2,1))]. given #26 (A,wt=20): 23 (x + ((x + y)' + (x + y')'')')' = (x + y)'. [para(8(a,1),8(a,1,1,1))]. given #27 (T,wt=13): 48 ((x + y')' + (y + x)')' = x. [para(6(a,1),20(a,1,1))]. given #28 (T,wt=13): 76 (g(x) + (x + (g(x) + h(x)''))')' = x. [para(38(a,1),8(a,1,1,2)),rewrite([6(9)])]. given #29 (T,wt=13): 81 (x + (x + (g(x) + (g(x) + h(x))))')' = g(x). [para(43(a,1),8(a,1,1,2)),rewrite([19(6),6(8)])]. given #30 (T,wt=13): 89 ((x' + y)' + (y + x)')' = y. [para(6(a,1),21(a,1,1))]. given #31 (A,wt=21): 24 ((x + y)' + (x + ((y + z)' + (y + z')'))')' = x. [para(8(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #32 (T,wt=13): 119 x + h(y) = y + (y + (y + (g(y) + x))). [para(29(a,1),6(a,1)),flip(a)]. given #33 (T,wt=13): 131 x + (x + (y + (x + g(x)))) = y + h(x). [para(19(a,1),30(a,2,2,2)),rewrite([6(4)]),flip(a)]. given #34 (T,wt=13): 429 x + h(y) = y + (y + (y + (x + g(y)))). [para(6(a,1),119(a,2,2,2,2))]. given #35 (T,wt=14): 86 (x' + (g(x) + (x' + x'))')' = g(x). [para(56(a,1),8(a,1,1,2)),rewrite([6(8)])]. given #36 (A,wt=18): 25 (x + (x + (y' + (x + y)'))')' = (x + y)'. [para(8(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #37 (T,wt=14): 115 (h(x)' + (x + (g(x)' + h(x)'))')' = x. [para(62(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #38 (T,wt=15): 27 ((x + g(y))' + (x + (y + y'))')' = x. [para(10(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])]. given #39 (T,wt=15): 39 ((x + y)' + (x + (g(y) + h(y)'))')' = x. [para(37(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. given #40 (T,wt=15): 44 (x + (g(x) + (x + x'')'')')' = g(x). [para(26(a,1),8(a,1,1,1))]. given #41 (A,wt=17): 32 ((x + (y + z))' + (y + (x + z)')')' = y. [para(19(a,1),8(a,1,1,1,1))]. given #42 (T,wt=15): 57 ((x + (x' + y))' + (y + g(x))')' = y. [para(10(a,1),20(a,1,1,2,1,2)),rewrite([7(3)])]. given #43 (T,wt=15): 63 ((g(x) + (h(x)' + y))' + (y + x)')' = y. [para(37(a,1),20(a,1,1,2,1,2)),rewrite([7(5)])]. given #44 (T,wt=15): 70 (g(x) + (x + (x + (x + g(x)))'')')' = x. [para(36(a,1),8(a,1,1,1))]. given #45 (T,wt=15): 74 (g(x) + (x + (g(x) + h(x)'')'')')' = x. [para(38(a,1),8(a,1,1,1))]. given #46 (A,wt=17): 35 ((x + y)' + (x + (g(y) + (y + y)'))')' = x. [para(28(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. given #47 (T,wt=15): 79 (x + (g(x) + (x + (g(x) + h(x)))'')')' = g(x). [para(43(a,1),8(a,1,1,1))]. given #48 (T,wt=15): 96 ((x + (y + y'))' + (g(y) + x)')' = x. [para(10(a,1),21(a,1,1,2,1,1))]. given #49 (T,wt=14): 753 (x + (x + (x' + h(x)'))')' = h(x)'. [para(37(a,1),96(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #50 (T,wt=15): 100 ((x + (g(y) + h(y)'))' + (y + x)')' = x. [para(37(a,1),21(a,1,1,2,1,1))]. given #51 (A,wt=17): 42 ((x + g(y))' + (x + (y + (g(y) + h(y))'))')' = x. [para(40(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #52 (T,wt=14): 794 (g(x) + (g(x) + (x' + h(x)'))')' = x'. [para(10(a,1),100(a,1,1,2)),rewrite([19(6),6(9)])]. given #53 (T,wt=15): 132 (x + (x + (x + (x + (g(x) + g(x)))))')' = g(x). [para(30(a,1),40(a,1,1,2,1)),rewrite([6(3),19(4)])]. given #54 (T,wt=15): 178 (g(x) + (x + (g(x) + (x + x)''))')' = x. [para(34(a,1),8(a,1,1,2)),rewrite([6(9)])]. given #55 (T,wt=15): 185 (x + (x + (g(x) + (g(x) + h(x))''))')' = g(x). [para(41(a,1),8(a,1,1,2)),rewrite([19(8),6(10)])]. given #56 (A,wt=19): 45 ((x + y)' + (x + (g(y) + (y + y'')'))')' = x. [para(26(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #57 (T,wt=15): 193 (g(x) + (x + (x + (g(x) + x'')))')' = x. [para(46(a,1),8(a,1,1,2)),rewrite([6(9)])]. given #58 (T,wt=15): 203 ((g(x) + y)' + (x + (x' + y))')' = y. [para(10(a,1),47(a,1,1,2,1,1)),rewrite([7(3),6(8)])]. given #59 (T,wt=15): 207 ((x + y)' + (g(x) + (h(x)' + y))')' = y. [para(37(a,1),47(a,1,1,2,1,1)),rewrite([7(5),6(9)])]. given #60 (T,wt=15): 255 (x + h(y))' = (y + (y + (g(y) + (x + y))))'. [para(30(a,1),23(a,2,1)),rewrite([23(12)])]. given #61 (A,wt=17): 49 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),20(a,1,1,1,1))]. given #62 (T,wt=15): 269 ((x + g(y))' + (y + (y' + x))')' = x. [para(10(a,1),48(a,1,1,1,1,2)),rewrite([7(6)])]. given #63 (T,wt=15): 272 ((x + y)' + (g(y) + (h(y)' + x))')' = x. [para(37(a,1),48(a,1,1,1,1,2)),rewrite([7(7)])]. given #64 (T,wt=15): 299 (x + (x + (g(x) + (g(x) + h(x)'')))')' = g(x). [para(76(a,1),8(a,1,1,2)),rewrite([19(8),6(10)])]. given #65 (T,wt=15): 309 (g(x) + (x + (x + (g(x) + (g(x) + h(x)))))')' = x. [para(81(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #66 (A,wt=19): 50 ((x + (y + z))' + (y + (z + x'))')' = y + z. [para(7(a,1),20(a,1,1,2,1))]. given #67 (T,wt=15): 321 ((g(x) + y)' + (y + (x + x'))')' = y. [para(10(a,1),89(a,1,1,1,1,1))]. given #68 (T,wt=15): 325 ((x + y)' + (y + (g(x) + h(x)'))')' = y. [para(37(a,1),89(a,1,1,1,1,1))]. given #69 (T,wt=15): 446 (x + h(y))' = (y + (y + (y + (g(y) + x))))'. [para(119(a,1),23(a,2,1)),rewrite([23(12)])]. given #70 (T,wt=15): 479 (x + h(y))' = (y + (y + (y + (x + g(y)))))'. [para(429(a,1),23(a,2,1)),rewrite([23(12)])]. given #71 (A,wt=20): 51 (x + ((y + x)' + (x + y')'')')' = (y + x)'. [para(20(a,1),8(a,1,1,1))]. given #72 (T,wt=15): 559 ((x + g(y))' + (y + (x + y'))')' = x. [para(19(a,1),27(a,1,1,2,1))]. given #73 (T,wt=15): 573 ((x + y)' + (g(y) + (x + h(y)'))')' = x. [para(19(a,1),39(a,1,1,2,1))]. given #74 (T,wt=15): 751 ((x + (y + x'))' + (g(x) + y)')' = y. [para(19(a,1),96(a,1,1,1,1))]. given #75 (T,wt=15): 796 ((x + y)' + (g(x) + (y + h(x)'))')' = y. [para(19(a,1),100(a,1,1,1,1)),rewrite([6(9)])]. given #76 (A,wt=21): 52 ((x + y)' + (x + ((z + y)' + (y + z')'))')' = x. [para(20(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #77 (T,wt=15): 922 ((g(x) + y)' + (x + (y + x'))')' = y. [para(6(a,1),203(a,1,1,2,1,2))]. given #78 (T,wt=16): 60 (x + (g(x)' + (x + x)')')' = (x + x)'. [para(28(a,1),20(a,1,1,1)),rewrite([6(5)])]. given #79 (T,wt=16): 64 (g(x) + (x' + (g(x) + h(x))')')' = (g(x) + h(x))'. [para(40(a,1),20(a,1,1,1)),rewrite([6(7)])]. given #80 (T,wt=16): 84 (x' + (g(x) + (x' + x')'')')' = g(x). [para(56(a,1),8(a,1,1,1))]. given #81 (A,wt=18): 53 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(20(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #82 (T,wt=16): 113 (h(x)' + (x + (g(x)' + h(x)')'')')' = x. [para(62(a,1),8(a,1,1,1))]. given #83 (T,wt=16): 775 (h(x)' + (x + (x + (x' + h(x)')))')' = x. [para(753(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #84 (T,wt=16): 841 (x' + (g(x) + (g(x) + (x' + h(x)')))')' = g(x). [para(794(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #85 (T,wt=17): 61 ((g(x) + ((x + x)' + y))' + (y + x)')' = y. [para(28(a,1),20(a,1,1,2,1,2)),rewrite([7(5)])]. given #86 (A,wt=21): 54 (x + ((x + y')' + (x + y)'')')' = (x + y')'. [para(8(a,1),20(a,1,1,1))]. given #87 (T,wt=17): 65 ((x + ((g(x) + h(x))' + y))' + (y + g(x))')' = y. [para(40(a,1),20(a,1,1,2,1,2)),rewrite([7(6)])]. given #88 (T,wt=17): 97 ((x + (y + z))' + ((x + z)' + y)')' = y. [para(19(a,1),21(a,1,1,1,1))]. given #89 (T,wt=17): 99 ((x + (g(y) + (y + y)'))' + (y + x)')' = x. [para(28(a,1),21(a,1,1,2,1,1))]. given #90 (T,wt=16): 1811 (g(x) + (g(x) + (x' + (x + x)'))')' = x'. [para(10(a,1),99(a,1,1,2)),rewrite([19(6),6(9)])]. given #91 (A,wt=21): 55 (((x + y)' + ((x + y')' + z))' + (z + x)')' = z. [para(8(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #92 (T,wt=17): 101 ((x + (y + (g(y) + h(y))'))' + (g(y) + x)')' = x. [para(40(a,1),21(a,1,1,2,1,1))]. given #93 (T,wt=16): 1991 (x + (x + (h(x)' + (g(x) + h(x))'))')' = h(x)'. [para(37(a,1),101(a,1,1,2)),rewrite([19(8),6(10)])]. given #94 (T,wt=17): 124 x + (y + h(z)) = z + (z + (g(z) + (x + (y + z)))). [para(30(a,1),7(a,1)),rewrite([7(3)]),flip(a)]. given #95 (T,wt=17): 125 x + (y + h(z)) = x + (z + (z + (g(z) + (y + z)))). [para(30(a,1),7(a,2,2)),rewrite([7(3)])]. given #96 (A,wt=19): 58 (h(x)' + (x + (x + (g(x) + x')))')' = x + (x + g(x)). [para(12(a,1),20(a,1,1,1,1)),rewrite([7(7),7(6)])]. given #97 (T,wt=17): 126 x + (g(x) + (y + (x + (z + x)))) = y + (z + h(x)). [para(30(a,2),7(a,2,2)),rewrite([19(6),19(5),7(4)])]. given #98 (T,wt=17): 129 x + (y + h(z)) = y + (z + (z + (g(z) + (x + z)))). [para(30(a,1),19(a,1,2)),flip(a)]. given #99 (T,wt=17): 130 x + (y + h(z)) = z + (x + (z + (g(z) + (y + z)))). [para(30(a,2),19(a,1,2))]. given #100 (T,wt=17): 135 (g(x) + (x + (x + (x + (x + (g(x) + g(x))))))')' = x. [para(30(a,1),43(a,1,1,2,1,2)),rewrite([6(4),19(5)])]. given #101 (A,wt=19): 59 ((x + (y + z))' + (x + (z + y'))')' = x + z. [para(19(a,1),20(a,1,1,1,1)),rewrite([7(6)])]. given #102 (T,wt=17): 140 x + (y + (z + (x + (x + g(x))))) = y + (z + h(x)). [para(7(a,1),33(a,1,2)),rewrite([7(9)])]. given #103 (T,wt=17): 153 (h(x)' + (x + (x + (x + g(x))'))')' = x + x. [para(12(a,1),22(a,1,1,1,1))]. given #104 (T,wt=17): 176 (g(x) + (x + (g(x) + (x + x)'')'')')' = x. [para(34(a,1),8(a,1,1,1))]. given #105 (T,wt=17): 183 (x + (g(x) + (x + (g(x) + h(x))'')'')')' = g(x). [para(41(a,1),8(a,1,1,1))]. given #106 (A,wt=20): 66 (x + (g(x)' + (x + x'')')')' = (x + x'')'. [para(26(a,1),20(a,1,1,1)),rewrite([6(7)])]. given #107 (T,wt=17): 191 (g(x) + (x + (x + (g(x) + x''))'')')' = x. [para(46(a,1),8(a,1,1,1))]. given #108 (T,wt=17): 198 ((x + (y + z))' + ((x + y)' + z)')' = z. [para(7(a,1),47(a,1,1,1,1))]. given #109 (T,wt=17): 206 ((x + y)' + (g(x) + ((x + x)' + y))')' = y. [para(28(a,1),47(a,1,1,2,1,1)),rewrite([7(5),6(9)])]. given #110 (T,wt=17): 208 ((g(x) + y)' + (x + ((g(x) + h(x))' + y))')' = y. [para(40(a,1),47(a,1,1,2,1,1)),rewrite([7(6),6(11)])]. given #111 (A,wt=19): 67 ((g(x) + ((x + x'')' + y))' + (y + x)')' = y. [para(26(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #112 (T,wt=17): 266 ((x + (y + z)')' + (y + (z + x))')' = x. [para(7(a,1),48(a,1,1,2,1))]. given #113 (T,wt=17): 271 ((x + y)' + (g(y) + ((y + y)' + x))')' = x. [para(28(a,1),48(a,1,1,1,1,2)),rewrite([7(7)])]. given #114 (T,wt=17): 273 ((x + g(y))' + (y + ((g(y) + h(y))' + x))')' = x. [para(40(a,1),48(a,1,1,1,1,2)),rewrite([7(9)])]. given #115 (T,wt=17): 297 (x + (g(x) + (x + (g(x) + h(x)''))'')')' = g(x). [para(76(a,1),8(a,1,1,1))]. given #116 (A,wt=21): 68 (x + ((x + y')' + (y + x)'')')' = (x + y')'. [para(20(a,1),20(a,1,1,1))]. given #117 (T,wt=17): 307 (g(x) + (x + (x + (g(x) + (g(x) + h(x))))'')')' = x. [para(81(a,1),8(a,1,1,1))]. given #118 (T,wt=17): 323 (((x + y)' + z)' + (x + (z + y))')' = z. [para(19(a,1),89(a,1,1,2,1))]. given #119 (T,wt=17): 324 ((x + y)' + (y + (g(x) + (x + x)'))')' = y. [para(28(a,1),89(a,1,1,1,1,1))]. given #120 (T,wt=17): 326 ((g(x) + y)' + (y + (x + (g(x) + h(x))'))')' = y. [para(40(a,1),89(a,1,1,1,1,1))]. given #121 (A,wt=21): 69 (((x + y)' + ((y + x')' + z))' + (z + y)')' = z. [para(20(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #122 (T,wt=17): 430 x + (y + h(z)) = z + (z + (z + (g(z) + (x + y)))). [para(119(a,1),7(a,1)),flip(a)]. given #123 (T,wt=17): 431 x + (y + h(z)) = x + (z + (z + (z + (g(z) + y)))). [para(119(a,1),7(a,2,2)),rewrite([7(3)])]. given #124 (T,wt=17): 432 x + (y + h(z)) = z + (z + (g(z) + (x + (z + y)))). [para(119(a,2),7(a,2,2)),rewrite([19(6),19(5),19(4),7(3)]),flip(a)]. given #125 (T,wt=17): 434 x + (y + h(z)) = y + (z + (z + (z + (g(z) + x)))). [para(119(a,1),19(a,1,2)),flip(a)]. given #126 (A,wt=19): 71 ((x + g(y))' + (x + (y + (y + (y + g(y)))'))')' = x. [para(36(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #127 (T,wt=17): 435 x + (y + h(z)) = z + (x + (z + (z + (g(z) + y)))). [para(119(a,2),19(a,1,2))]. given #128 (T,wt=17): 436 x + (y + h(z)) = z + (z + (z + (x + (g(z) + y)))). [para(19(a,1),119(a,2,2,2,2)),rewrite([7(3)])]. given #129 (T,wt=17): 450 x + (y + (x + (z + (x + g(x))))) = y + (z + h(x)). [para(131(a,1),7(a,2,2)),rewrite([19(6),7(5)])]. given #130 (T,wt=17): 451 x + (x + (y + (z + (x + g(x))))) = y + (z + h(x)). [para(7(a,1),131(a,1,2,2)),rewrite([7(9)])]. given #131 (A,wt=20): 72 (g(x) + (x' + (x + (x + g(x)))')')' = (x + (x + g(x)))'. [para(36(a,1),20(a,1,1,1)),rewrite([6(7)])]. given #132 (T,wt=17): 460 x + (y + h(z)) = z + (z + (z + (x + (y + g(z))))). [para(429(a,1),7(a,1)),rewrite([7(3)]),flip(a)]. given #133 (T,wt=17): 461 x + (y + h(z)) = x + (z + (z + (z + (y + g(z))))). [para(429(a,1),7(a,2,2)),rewrite([7(3)])]. given #134 (T,wt=17): 462 x + (y + h(z)) = z + (z + (x + (z + (y + g(z))))). [para(429(a,2),7(a,2,2)),rewrite([19(6),19(5),7(4)]),flip(a)]. given #135 (T,wt=17): 465 x + (y + h(z)) = y + (z + (z + (z + (x + g(z))))). [para(429(a,1),19(a,1,2)),flip(a)]. given #136 (A,wt=19): 73 ((x + ((x + (x + g(x)))' + y))' + (y + g(x))')' = y. [para(36(a,1),20(a,1,1,2,1,2)),rewrite([7(6)])]. given #137 (T,wt=17): 466 x + (y + h(z)) = z + (x + (z + (z + (y + g(z))))). [para(429(a,2),19(a,1,2))]. given #138 (T,wt=17): 487 (g(x) + (g(x) + (x' + (x' + x')))')' = x'. [para(86(a,1),8(a,1,1,2)),rewrite([19(7),6(10)])]. given #139 (T,wt=17): 507 (g(x) + (x + (g(x) + (x + x'')''))')' = x. [para(26(a,1),25(a,1,1,2,1,2,2)),rewrite([6(8),19(9),26(19)])]. given #140 (T,wt=17): 510 (x + (x + (g(x) + (x + (x + g(x)))''))')' = g(x). [para(36(a,1),25(a,1,1,2,1,2,2)),rewrite([6(7),36(17)])]. given #141 (A,wt=19): 75 ((x + g(y))' + (x + (y + (g(y) + h(y)'')'))')' = x. [para(38(a,1),8(a,1,1,2,1,2)),rewrite([6(13)])]. given #142 (T,wt=17): 511 (x + (x + (g(x) + (g(x) + h(x)'')''))')' = g(x). [para(38(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),38(21)])]. given #143 (T,wt=17): 512 (g(x) + (x + (g(x) + (x + (g(x) + h(x)))''))')' = x. [para(43(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),19(10),43(21)])]. given #144 (T,wt=17): 544 (x + (x + (g(x)' + (h(x)' + h(x)')))')' = h(x)'. [para(115(a,1),8(a,1,1,2)),rewrite([19(9),19(8),6(11)])]. given #145 (T,wt=17): 596 ((x + (y + z))' + (x + (z + y)')')' = x. [para(6(a,1),32(a,1,1,1,1)),rewrite([7(2)])]. given #146 (A,wt=20): 77 (g(x) + (x' + (g(x) + h(x)'')')')' = (g(x) + h(x)'')'. [para(38(a,1),20(a,1,1,1)),rewrite([6(9)])]. given #147 (T,wt=17): 597 ((x + (y + z))' + (y + (z + x)')')' = y. [para(6(a,1),32(a,1,1,2,1,2,1))]. given #148 (T,wt=15): 3915 ((x' + (y + x))' + (y + g(x))')' = y. [para(10(a,1),597(a,1,1,2,1,2))]. given #149 (T,wt=15): 3919 ((x + y)' + (h(y)' + (x + g(y)))')' = x. [para(37(a,1),597(a,1,1,2,1,2)),rewrite([6(9)])]. given #150 (T,wt=15): 4071 ((g(x) + y)' + (x' + (y + x))')' = y. [para(6(a,1),3915(a,1,1,2,1)),rewrite([6(8)])]. given #151 (A,wt=19): 78 ((x + ((g(x) + h(x)'')' + y))' + (y + g(x))')' = y. [para(38(a,1),20(a,1,1,2,1,2)),rewrite([7(8)])]. given #152 (T,wt=15): 4072 ((x + g(y))' + (y' + (x + y))')' = x. [para(6(a,1),3915(a,1,1))]. given #153 (T,wt=15): 4101 ((x + y)' + (h(x)' + (y + g(x)))')' = y. [para(6(a,1),3919(a,1,1,1,1))]. given #154 (T,wt=17): 598 ((x + (y + z)')' + (y + (x + z))')' = x. [para(6(a,1),32(a,1,1))]. given #155 (T,wt=17): 602 ((x + y)' + (g(y) + (x + (y + y)'))')' = x. [para(28(a,1),32(a,1,1,2,1,2)),rewrite([6(9)])]. given #156 (A,wt=19): 80 ((x + y)' + (x + (g(y) + (y + (g(y) + h(y)))'))')' = x. [para(43(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])]. given #157 (T,wt=17): 603 ((x + g(y))' + (y + (x + (g(y) + h(y))'))')' = x. [para(40(a,1),32(a,1,1,2,1,2)),rewrite([6(11)])]. given #158 (T,wt=17): 870 (x + (x + (g(x) + (g(x) + (x + x)'')))')' = g(x). [para(178(a,1),8(a,1,1,2)),rewrite([19(8),6(10)])]. given #159 (T,wt=17): 884 (g(x) + (x + (x + (g(x) + (g(x) + h(x))'')))')' = x. [para(185(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #160 (T,wt=17): 909 (x + (x + (x + (g(x) + (g(x) + x''))))')' = g(x). [para(193(a,1),8(a,1,1,2)),rewrite([19(8),19(7),6(10)])]. given #161 (A,wt=20): 82 (x + (g(x)' + (x + (g(x) + h(x)))')')' = (x + (g(x) + h(x)))'. [para(43(a,1),20(a,1,1,1)),rewrite([6(8)])]. given #162 (T,wt=17): 993 ((x + (y + z))' + (z + (y + x)')')' = z. [para(6(a,1),49(a,1,1,2,1,2,1))]. given #163 (T,wt=17): 1000 (h(x)' + (x + (g(x) + (x + x)'))')' = x + g(x). [para(12(a,1),49(a,1,1,1,1)),rewrite([7(7)])]. given #164 (T,wt=17): 1064 (g(x) + (x + (x + (g(x) + (g(x) + h(x)''))))')' = x. [para(299(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #165 (T,wt=17): 1700 ((x + (y + z))' + ((z + y)' + x)')' = x. [para(6(a,1),97(a,1,1,1,1)),rewrite([7(2)])]. given #166 (A,wt=19): 83 ((g(x) + ((x + (g(x) + h(x)))' + y))' + (y + x)')' = y. [para(43(a,1),20(a,1,1,2,1,2)),rewrite([7(8)])]. given #167 (T,wt=17): 1701 ((x + (y + z))' + ((z + x)' + y)')' = y. [para(6(a,1),97(a,1,1,2,1,1,1))]. given #168 (T,wt=17): 1710 ((x + y)' + (g(x) + (y + (x + x)'))')' = y. [para(28(a,1),97(a,1,1,2,1,1)),rewrite([6(9)])]. given #169 (T,wt=17): 1711 ((x + (y + (g(x) + h(x))'))' + (g(x) + y)')' = y. [para(40(a,1),97(a,1,1,2,1,1))]. given #170 (T,wt=17): 2033 x + (y + h(z)) = z + (z + (g(z) + (y + (z + x)))). [para(6(a,1),124(a,2,2,2,2)),rewrite([7(6)])]. given #171 (A,wt=20): 85 ((x + y')' + (x + (g(y) + (y' + y')'))')' = x. [para(56(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])]. given #172 (T,wt=16): 4901 (g(x) + (x + (g(x) + (x' + x')'))')' = x. [para(10(a,1),85(a,1,1,1))]. given #173 (T,wt=17): 2040 x + (y + h(z)) = z + (z + (g(z) + (y + (x + z)))). [para(124(a,1),19(a,1)),flip(a)]. given #174 (T,wt=17): 2042 x + (y + h(z)) = z + (z + (x + (g(z) + (y + z)))). [para(19(a,1),124(a,2,2,2))]. given #175 (T,wt=17): 2112 x + (g(x) + (y + (x + (x + z)))) = y + (z + h(x)). [para(6(a,1),126(a,1,2,2,2,2))]. given #176 (A,wt=21): 87 (x' + (g(x)' + (x' + x')')')' = (x' + x')'. [para(56(a,1),20(a,1,1,1)),rewrite([6(8)])]. given #177 (T,wt=17): 2120 x + (g(x) + (y + (x + (z + x)))) = z + (y + h(x)). [para(126(a,2),19(a,1))]. given #178 (T,wt=17): 2121 x + (g(x) + (y + (z + (x + x)))) = y + (z + h(x)). [para(19(a,1),126(a,1,2,2,2))]. given #179 (T,wt=17): 2167 x + (y + h(z)) = z + (y + (z + (g(z) + (x + z)))). [para(129(a,2),19(a,1))]. given #180 (T,wt=17): 2344 x + (y + h(z)) = z + (y + (z + (z + (g(z) + x)))). [para(6(a,1),140(a,1,2)),rewrite([7(5),7(4),7(3)]),flip(a)]. given #181 (A,wt=20): 88 ((g(x) + ((x' + x')' + y))' + (y + x')')' = y. [para(56(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #182 (T,wt=17): 2423 ((x + (y + z))' + ((y + x)' + z)')' = z. [para(6(a,1),198(a,1,1,2,1,1,1))]. given #183 (T,wt=17): 2532 ((g(x) + y)' + (x + (y + (g(x) + h(x))'))')' = y. [para(6(a,1),208(a,1,1,2,1,2))]. given #184 (T,wt=17): 2590 ((x + (y + z)')' + (z + (y + x))')' = x. [para(6(a,1),266(a,1,1,1,1,2,1))]. given #185 (T,wt=17): 2591 ((x + (y + z)')' + (z + (x + y))')' = x. [para(6(a,1),266(a,1,1,2,1)),rewrite([7(6)])]. given #186 (A,wt=19): 90 ((x + (y + z))' + (z' + (x + y))')' = x + y. [para(7(a,1),21(a,1,1,1,1))]. given #187 (T,wt=17): 2747 (((x + y)' + z)' + (y + (z + x))')' = z. [para(6(a,1),323(a,1,1,1,1,1,1))]. given #188 (T,wt=17): 2748 (((x + y)' + z)' + (z + (y + x))')' = z. [para(6(a,1),323(a,1,1,2,1)),rewrite([7(6)])]. given #189 (T,wt=17): 2899 x + (y + h(z)) = z + (z + (z + (g(z) + (y + x)))). [para(6(a,1),430(a,2,2,2,2,2))]. given #190 (T,wt=17): 3003 x + (y + h(z)) = z + (z + (x + (z + (g(z) + y)))). [para(19(a,1),432(a,2,2,2)),rewrite([19(6)])]. given #191 (A,wt=20): 91 (x + ((x + y)' + (y' + x)'')')' = (x + y)'. [para(21(a,1),8(a,1,1,1))]. given #192 (T,wt=17): 3260 x + (y + h(z)) = z + (z + (z + (y + (g(z) + x)))). [para(436(a,1),19(a,1)),flip(a)]. given #193 (T,wt=17): 3331 x + (y + h(z)) = z + (z + (y + (z + (g(z) + x)))). [para(6(a,1),450(a,1,2)),rewrite([7(5),7(4),7(3)]),flip(a)]. given #194 (T,wt=17): 3379 x + (y + h(z)) = z + (z + (z + (y + (x + g(z))))). [para(460(a,1),19(a,1)),flip(a)]. given #195 (T,wt=17): 3485 x + (y + h(z)) = z + (z + (y + (z + (x + g(z))))). [para(462(a,1),19(a,1)),flip(a)]. given #196 (A,wt=21): 92 ((x + y)' + (x + ((y + z)' + (z' + y)'))')' = x. [para(21(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #197 (T,wt=17): 3571 x + (y + h(z)) = z + (y + (z + (z + (x + g(z))))). [para(465(a,2),19(a,1))]. given #198 (T,wt=17): 3918 ((x + y)' + ((y + y)' + (x + g(y)))')' = x. [para(28(a,1),597(a,1,1,2,1,2)),rewrite([6(9)])]. given #199 (T,wt=17): 3920 (((g(x) + h(x))' + (y + x))' + (y + g(x))')' = y. [para(40(a,1),597(a,1,1,2,1,2))]. given #200 (T,wt=17): 4610 ((x + y)' + ((x + x)' + (y + g(x)))')' = y. [para(28(a,1),1701(a,1,1,2,1,1)),rewrite([6(9)])]. given #201 (A,wt=18): 93 (x + (y' + (x + (x + y)'))')' = (x + y)'. [para(21(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #202 (T,wt=17): 4611 ((g(x) + y)' + ((g(x) + h(x))' + (y + x))')' = y. [para(40(a,1),1701(a,1,1,2,1,1)),rewrite([6(11)])]. given #203 (T,wt=17): 4946 x + (y + h(z)) = z + (z + (y + (g(z) + (x + z)))). [para(19(a,1),2040(a,2,2,2))]. given #204 (T,wt=17): 5087 x + (g(x) + (y + (x + (x + z)))) = z + (y + h(x)). [para(2112(a,2),19(a,1))]. given #205 (T,wt=17): 5302 x + (y + (g(x) + (z + (x + x)))) = y + (z + h(x)). [para(19(a,1),2121(a,1,2))]. given #206 (A,wt=21): 94 ((x + ((y + z)' + (y + z')'))' + (y + x)')' = x. [para(8(a,1),21(a,1,1,2,1,1))]. given #207 (T,wt=13): 7047 x + (g(x) + (y + (x + x))) = y + h(x). [para(5302(a,1),59(a,1,1,1,1)),rewrite([7(10),7(9),7(8),6944(14)]),flip(a)]. given #208 (T,wt=17): 5629 ((x + g(y))' + ((g(y) + h(y))' + (x + y))')' = x. [para(40(a,1),2591(a,1,1,1,1,2))]. given #209 (T,wt=17): 7251 g(x) + (y + (x + (z + (x + x)))) = y + (z + h(x)). [para(7047(a,1),7(a,2,2)),rewrite([19(6),7(5)])]. given #210 (T,wt=17): 7284 g(x) + (y + (x + (x + (x + z)))) = y + (z + h(x)). [para(6(a,1),7251(a,1,2,2,2)),rewrite([7(3)])]. given #211 (A,wt=19): 95 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #212 (T,wt=17): 7287 g(x) + (y + (x + (x + (z + x)))) = y + (z + h(x)). [para(19(a,1),7251(a,1,2,2,2))]. given #213 (T,wt=17): 7288 g(x) + (y + (z + (x + (x + x)))) = y + (z + h(x)). [para(19(a,1),7251(a,1,2,2))]. given #214 (T,wt=17): 7318 g(x) + (y + (x + (x + (x + z)))) = z + (y + h(x)). [para(7284(a,2),19(a,1))]. given #215 (T,wt=17): 7714 g(x) + (y + (x + (x + (z + x)))) = z + (y + h(x)). [para(7287(a,2),19(a,1))]. given #216 (A,wt=19): 98 ((x + (y + z))' + (x + (z' + y))')' = x + y. [para(19(a,1),21(a,1,1,2,1)),rewrite([7(2)])]. given #217 (T,wt=13): 8180 g(x) + (y + (x + (x + x))) = y + h(x). [para(7288(a,1),98(a,1,1,2,1)),rewrite([7(5),7(4),7(3),7856(14)]),flip(a)]. given #218 (T,wt=18): 201 (x + (y' + (x + (y + x)'))')' = (y + x)'. [para(47(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #219 (T,wt=18): 502 (x + (x + (h(x)' + (x + (x + g(x)))'))')' = h(x)'. [para(12(a,1),25(a,1,1,2,1,2,2,1)),rewrite([6(7),12(15)])]. given #220 (T,wt=18): 773 (h(x)' + (x + (x + (x' + h(x)'))'')')' = x. [para(753(a,1),8(a,1,1,1))]. given #221 (A,wt=19): 102 ((x + (g(y) + (y + y'')'))' + (y + x)')' = x. [para(26(a,1),21(a,1,1,2,1,1))]. given #222 (T,wt=18): 839 (x' + (g(x) + (g(x) + (x' + h(x)'))'')')' = g(x). [para(794(a,1),8(a,1,1,1))]. given #223 (T,wt=18): 1418 ((x + x)' + (x + (g(x)' + (x + x)'))')' = x. [para(60(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #224 (T,wt=18): 1433 ((g(x) + h(x))' + (g(x) + (x' + (g(x) + h(x))'))')' = g(x). [para(64(a,1),8(a,1,1,2)),rewrite([6(14)])]. given #225 (T,wt=18): 1843 (x' + (g(x) + (g(x) + (x' + (x + x)')))')' = g(x). [para(1811(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #226 (A,wt=21): 103 (x + ((y' + x)' + (x + y)'')')' = (y' + x)'. [para(21(a,1),20(a,1,1,1))]. given #227 (T,wt=18): 2014 (h(x)' + (x + (x + (h(x)' + (g(x) + h(x))')))')' = x. [para(1991(a,1),8(a,1,1,2)),rewrite([6(13)])]. given #228 (T,wt=18): 4918 (x + (x + (g(x) + (g(x) + (x' + x')')))')' = g(x). [para(4901(a,1),8(a,1,1,2)),rewrite([19(9),6(11)])]. given #229 (T,wt=18): 8275 (g(x) + (g(x) + (x' + (x + x'')'))')' = x'. [para(10(a,1),102(a,1,1,2)),rewrite([19(8),6(11)])]. given #230 (T,wt=19): 106 (x + (y + (x + (x + y')'))')' = (x + y')'. [para(20(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #231 (A,wt=21): 104 (((x + y)' + ((y' + x)' + z))' + (z + x)')' = z. [para(21(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #232 (T,wt=19): 107 ((x + (y + (y + (y + g(y)))'))' + (g(y) + x)')' = x. [para(36(a,1),21(a,1,1,2,1,1))]. given #233 (T,wt=19): 108 ((x + (y + (g(y) + h(y)'')'))' + (g(y) + x)')' = x. [para(38(a,1),21(a,1,1,2,1,1))]. given #234 (T,wt=18): 8731 (x + (x + (h(x)' + (g(x) + h(x)'')'))')' = h(x)'. [para(37(a,1),108(a,1,1,2)),rewrite([19(10),6(12)])]. given #235 (T,wt=19): 109 ((x + (g(y) + (y + (g(y) + h(y)))'))' + (y + x)')' = x. [para(43(a,1),21(a,1,1,2,1,1))]. given #236 (A,wt=21): 105 ((x + ((y + z)' + (z + y')'))' + (z + x)')' = x. [para(20(a,1),21(a,1,1,2,1,1))]. given #237 (T,wt=18): 8782 (g(x) + (g(x) + (x' + (x + (g(x) + h(x)))'))')' = x'. [para(10(a,1),109(a,1,1,2)),rewrite([19(9),6(12)])]. given #238 (T,wt=19): 112 (x + (x + (y + (y' + x)'))')' = (y' + x)'. [para(21(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #239 (T,wt=19): 121 ((x + (x + (x + (g(x) + y))))' + (y + h(x)')')' = y. [para(29(a,1),20(a,1,1,1,1))]. given #240 (T,wt=19): 122 ((x + h(y))' + (y + (y + (y + (g(y) + x'))))')' = h(y). [para(29(a,1),20(a,1,1,2,1))]. given #241 (A,wt=20): 110 ((x + (g(y) + (y' + y')'))' + (y' + x)')' = x. [para(56(a,1),21(a,1,1,2,1,1))]. given #242 (T,wt=19): 123 ((x + (x + (x + (g(x) + y))))' + (y' + h(x))')' = h(x). [para(29(a,1),21(a,1,1,1,1))]. given #243 (T,wt=19): 127 ((x + (x + (g(x) + (y + x))))' + (y + h(x)')')' = y. [para(30(a,1),8(a,1,1,1,1))]. given #244 (T,wt=19): 128 ((x + h(y))' + (y + (y + (g(y) + (x + y)))')')' = y. [para(30(a,2),8(a,1,1,1,1))]. given #245 (T,wt=19): 136 ((x + (x + (g(x) + (y + x))))' + (h(x)' + y)')' = y. [para(30(a,1),21(a,1,1,1,1))]. given #246 (A,wt=21): 111 ((x + ((y + z)' + (z' + y)'))' + (y + x)')' = x. [para(21(a,1),21(a,1,1,2,1,1))]. given #247 (T,wt=19): 141 ((x + h(y))' + (y + (x + (y + (y + g(y))))')')' = y. [para(33(a,1),8(a,1,1,1,1))]. given #248 (T,wt=19): 144 ((x + (y + z))' + (z + (x + y'))')' = z + x. [para(6(a,1),22(a,1,1,1,1)),rewrite([7(2)])]. given #249 (T,wt=19): 145 ((x + (y + z))' + (y + (z' + x))')' = x + y. [para(6(a,1),22(a,1,1,2,1)),rewrite([7(6)])]. given #250 (T,wt=19): 155 ((x + (y + z))' + (y + (x + z'))')' = y + x. [para(19(a,1),22(a,1,1,1,1))]. given #251 (A,wt=20): 114 ((x + h(y)')' + (x + (y + (g(y)' + h(y)')'))')' = x. [para(62(a,1),8(a,1,1,2,1,2)),rewrite([6(14)])]. given #252 (T,wt=16): 9821 (x + (x + (g(x) + (g(x)' + h(x)')'))')' = g(x). [para(37(a,1),114(a,1,1,1)),rewrite([19(9)])]. given #253 (T,wt=18): 9837 (g(x) + (x + (x + (g(x) + (g(x)' + h(x)')')))')' = x. [para(9821(a,1),8(a,1,1,2)),rewrite([6(13)])]. given #254 (T,wt=19): 189 (g(x) + (x + (x + (x + (x + (g(x) + g(x)))))'')')' = x. [para(30(a,1),41(a,1,1,2,1,2,1,1)),rewrite([6(4),19(5)])]. given #255 (T,wt=19): 204 ((x + (y + z))' + (y' + (x + z))')' = x + z. [para(19(a,1),47(a,1,1,1,1))]. given #256 (A,wt=21): 116 (h(x)' + (x' + (g(x)' + h(x)')')')' = (g(x)' + h(x)')'. [para(62(a,1),20(a,1,1,1)),rewrite([6(10)])]. given #257 (T,wt=19): 205 ((x + (y + z))' + (y + (x' + z))')' = y + z. [para(19(a,1),47(a,1,1,2,1))]. given #258 (T,wt=19): 209 ((x + y)' + (g(x) + ((x + x'')' + y))')' = y. [para(26(a,1),47(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #259 (T,wt=19): 213 ((g(x) + y)' + (x + ((x + (x + g(x)))' + y))')' = y. [para(36(a,1),47(a,1,1,2,1,1)),rewrite([7(6),6(11)])]. given #260 (T,wt=19): 214 ((g(x) + y)' + (x + ((g(x) + h(x)'')' + y))')' = y. [para(38(a,1),47(a,1,1,2,1,1)),rewrite([7(8),6(13)])]. given #261 (A,wt=20): 117 ((x + ((g(x)' + h(x)')' + y))' + (y + h(x)')')' = y. [para(62(a,1),20(a,1,1,2,1,2)),rewrite([7(8)])]. given #262 (T,wt=19): 215 ((x + y)' + (g(x) + ((x + (g(x) + h(x)))' + y))')' = y. [para(43(a,1),47(a,1,1,2,1,1)),rewrite([7(8),6(12)])]. given #263 (T,wt=19): 218 (x + (y + (x + (y' + x)'))')' = (y' + x)'. [para(47(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #264 (T,wt=19): 221 ((x + (x + (x + (g(x) + y))))' + (h(x)' + y)')' = y. [para(29(a,1),47(a,1,1,1,1))]. given #265 (T,wt=19): 222 ((x + (x + (g(x) + (y + x))))' + (y' + h(x))')' = h(x). [para(30(a,1),47(a,1,1,1,1))]. Low Water (keep, True_semantics): wt=30 given #266 (A,wt=20): 118 ((x + (y + (g(y)' + h(y)')'))' + (h(y)' + x)')' = x. [para(62(a,1),21(a,1,1,2,1,1))]. given #267 (T,wt=19): 223 ((x + h(y))' + (y + (y + (g(y) + (x' + y))))')' = h(y). [para(30(a,1),47(a,1,1,2,1))]. given #268 (T,wt=19): 240 (g(x) + (x + (g(x) + (x + x'')'')'')')' = x. [para(26(a,1),23(a,1,1,2,1,1)),rewrite([26(21)])]. given #269 (T,wt=19): 243 (x + (g(x) + (x + (x + (x + g(x)))'')'')')' = g(x). [para(36(a,1),23(a,1,1,2,1,1)),rewrite([36(19)])]. given #270 (T,wt=19): 244 (x + (g(x) + (x + (g(x) + h(x)'')'')'')')' = g(x). [para(38(a,1),23(a,1,1,2,1,1)),rewrite([38(23)])]. given #271 (A,wt=25): 120 ((x + (x + (x + (g(x) + y))))' + (x + (x + (x + (g(x) + y'))))')' = h(x). [para(29(a,1),8(a,1,1,1,1)),rewrite([29(9)])]. given #272 (T,wt=19): 246 (g(x) + (x + (g(x) + (x + (g(x) + h(x)))'')'')')' = x. [para(43(a,1),23(a,1,1,2,1,1)),rewrite([43(23)])]. given #273 (T,wt=19): 265 ((x + (y + z'))' + (z + (x + y))')' = x + y. [para(7(a,1),48(a,1,1,1,1))]. given #274 (T,wt=19): 270 ((x + (y + z'))' + (x + (z + y))')' = x + y. [para(19(a,1),48(a,1,1,2,1)),rewrite([7(3)])]. given #275 (T,wt=19): 274 ((x + y)' + (g(y) + ((y + y'')' + x))')' = x. [para(26(a,1),48(a,1,1,1,1,2)),rewrite([7(9)])]. given #276 (A,wt=25): 133 ((x + (x + (g(x) + (y + x))))' + (x + (x + (x + (g(x) + y'))))')' = h(x). [para(30(a,1),20(a,1,1,1,1)),rewrite([29(9)])]. given #277 (T,wt=19): 277 ((x + g(y))' + (y + ((y + (y + g(y)))' + x))')' = x. [para(36(a,1),48(a,1,1,1,1,2)),rewrite([7(9)])]. given #278 (T,wt=19): 278 ((x + g(y))' + (y + ((g(y) + h(y)'')' + x))')' = x. [para(38(a,1),48(a,1,1,1,1,2)),rewrite([7(11)])]. given #279 (T,wt=19): 279 ((x + y)' + (g(y) + ((y + (g(y) + h(y)))' + x))')' = x. [para(43(a,1),48(a,1,1,1,1,2)),rewrite([7(10)])]. given #280 (T,wt=19): 284 ((x + (x + (x + (g(x) + y'))))' + (y + h(x))')' = h(x). [para(29(a,1),48(a,1,1,1,1))]. given #281 (A,wt=25): 134 ((x + h(y))' + (y + (g(y) + (x + (y + y'))))')' = y + (g(y) + (x + y)). [para(30(a,2),20(a,1,1,1,1)),rewrite([7(9),7(8),7(7)])]. given #282 (T,wt=19): 285 ((x + h(y)')' + (y + (y + (y + (g(y) + x))))')' = x. [para(29(a,1),48(a,1,1,2,1))]. given #283 (T,wt=19): 312 (x + (x + (x + (x + (x + (g(x) + (g(x) + g(x)))))))')' = g(x). [para(30(a,1),81(a,1,1,2,1,2,2)),rewrite([6(4),19(5),19(8),19(7),19(6)])]. given #284 (T,wt=19): 318 ((x' + (y + z))' + (y + (z + x))')' = y + z. [para(7(a,1),89(a,1,1,2,1))]. given #285 (T,wt=19): 322 ((x + (y' + z))' + (x + (z + y))')' = x + z. [para(19(a,1),89(a,1,1,1,1)),rewrite([7(6)])]. given #286 (A,wt=25): 137 ((x + (x + (x + (g(x) + y))))' + (x + (x + (g(x) + (y' + x))))')' = h(x). [para(30(a,1),21(a,1,1,2,1)),rewrite([29(2)])]. given #287 (T,wt=19): 327 ((x + y)' + (y + (g(x) + (x + x'')'))')' = y. [para(26(a,1),89(a,1,1,1,1,1))]. given #288 (T,wt=19): 330 ((g(x) + y)' + (y + (x + (x + (x + g(x)))'))')' = y. [para(36(a,1),89(a,1,1,1,1,1))]. given #289 (T,wt=19): 331 ((g(x) + y)' + (y + (x + (g(x) + h(x)'')'))')' = y. [para(38(a,1),89(a,1,1,1,1,1))]. given #290 (T,wt=19): 332 ((x + y)' + (y + (g(x) + (x + (g(x) + h(x)))'))')' = y. [para(43(a,1),89(a,1,1,1,1,1))]. given #291 (A,wt=25): 142 ((x + h(y))' + (x + (y + (y + (g(y) + y'))))')' = x + (y + (y + g(y))). [para(33(a,1),20(a,1,1,1,1)),rewrite([7(9),7(8),7(7)])]. given #292 (T,wt=19): 337 ((x' + h(y))' + (y + (y + (y + (g(y) + x))))')' = h(y). [para(29(a,1),89(a,1,1,2,1))]. given #293 (T,wt=19): 338 ((h(x)' + y)' + (x + (x + (g(x) + (y + x))))')' = y. [para(30(a,1),89(a,1,1,2,1))]. given #294 (T,wt=19): 433 ((x + h(y))' + (y + (y + (y + (g(y) + x)))')')' = y. [para(119(a,2),8(a,1,1,1,1))]. given #295 (T,wt=19): 438 x + (x + (x + (g(x) + h(y)))) = y + (y + (y + (g(y) + h(x)))). [para(119(a,1),29(a,1))]. given #296 (A,wt=25): 143 x + (y + (y + (y + (g(y) + (x + (x + g(x))))))) = y + (y + (y + (g(y) + h(x)))). [para(29(a,1),33(a,1,2)),rewrite([29(12)])]. given #297 (T,wt=19): 452 ((x + h(y))' + (y + (y + (x + (y + g(y))))')')' = y. [para(131(a,1),8(a,1,1,1,1))]. given #298 (T,wt=19): 463 ((x + (x + (x + (y + g(x)))))' + (y + h(x)')')' = y. [para(429(a,1),8(a,1,1,1,1))]. given #299 (T,wt=19): 464 ((x + h(y))' + (y + (y + (y + (x + g(y))))')')' = y. [para(429(a,2),8(a,1,1,1,1))]. given #300 (T,wt=19): 469 ((x + (x + (x + (y + g(x)))))' + (h(x)' + y)')' = y. [para(429(a,1),21(a,1,1,1,1))]. given #301 (A,wt=25): 146 ((x + (y + (z + u)))' + (x + (y + (z + u')))')' = x + (y + z). [para(7(a,1),22(a,1,1,1,1,2)),rewrite([7(7)])]. given #302 (T,wt=19): 475 ((x + (x + (x + (y + g(x)))))' + (y' + h(x))')' = h(x). [para(429(a,1),47(a,1,1,1,1))]. given #303 (T,wt=19): 476 ((x + h(y))' + (y + (y + (y + (x' + g(y)))))')' = h(y). [para(429(a,1),47(a,1,1,2,1))]. given #304 (T,wt=19): 482 ((h(x)' + y)' + (x + (x + (x + (y + g(x)))))')' = y. [para(429(a,1),89(a,1,1,2,1))]. given #305 (T,wt=19): 486 (g(x) + (x' + (g(x) + (x' + x'))'')')' = x'. [para(86(a,1),8(a,1,1,1))]. given #306 (A,wt=28): 147 (x + (y + ((x + (y + z))' + (x + (y + z'))'')'))' = (x + (y + z))'. [para(22(a,1),8(a,1,1,1)),rewrite([7(12)])]. given #307 (T,wt=19): 513 (g(x) + (g(x) + (x' + (x' + x')''))')' = x'. [para(56(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),56(20)])]. given #308 (T,wt=19): 516 (x + (x + (h(x)' + (g(x)' + h(x)')''))')' = h(x)'. [para(62(a,1),25(a,1,1,2,1,2,2)),rewrite([6(10),62(22)])]. given #309 (T,wt=19): 520 (x + (x + (g(x) + (g(x) + (x + x)'')''))')' = g(x). [para(34(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),34(21)])]. given #310 (T,wt=19): 521 (g(x) + (x + (g(x) + (x + (g(x) + h(x))'')''))')' = x. [para(41(a,1),25(a,1,1,2,1,2,2)),rewrite([6(11),19(12),41(25)])]. given #311 (A,wt=27): 148 ((x + (y + z))' + (x + ((y + (z + u))' + (y + (z + u'))'))')' = x. [para(22(a,1),8(a,1,1,2,1,2)),rewrite([6(14)])]. given #312 (T,wt=19): 522 (x + (x + (g(x) + (x + (g(x) + x''))''))')' = g(x). [para(46(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),46(21)])]. given #313 (T,wt=19): 529 (g(x) + (x + (g(x) + (x + (g(x) + h(x)''))''))')' = x. [para(76(a,1),25(a,1,1,2,1,2,2)),rewrite([6(11),19(12),76(25)])]. given #314 (T,wt=19): 543 (x + (h(x)' + (x + (g(x)' + h(x)'))'')')' = h(x)'. [para(115(a,1),8(a,1,1,1))]. given #315 (T,wt=19): 604 ((x + y)' + (g(y) + (x + (y + y'')'))')' = x. [para(26(a,1),32(a,1,1,2,1,2)),rewrite([6(11)])]. given #316 (A,wt=26): 149 (x + (y + (x + (y + (z' + (x + (y + z))')))'))' = (x + (y + z))'. [para(22(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(10),7(10)])]. given #317 (T,wt=19): 608 ((x + g(y))' + (y + (x + (y + (y + g(y)))'))')' = x. [para(36(a,1),32(a,1,1,2,1,2)),rewrite([6(11)])]. given #318 (T,wt=19): 609 ((x + g(y))' + (y + (x + (g(y) + h(y)'')'))')' = x. [para(38(a,1),32(a,1,1,2,1,2)),rewrite([6(13)])]. given #319 (T,wt=19): 610 ((x + y)' + (g(y) + (x + (y + (g(y) + h(y)))'))')' = x. [para(43(a,1),32(a,1,1,2,1,2)),rewrite([6(12)])]. given #320 (T,wt=19): 869 (x + (g(x) + (x + (g(x) + (x + x)''))'')')' = g(x). [para(178(a,1),8(a,1,1,1))]. given #321 (A,wt=27): 150 ((x + (y + z))' + (x + (y + ((z + u)' + (z + u')')))')' = x + y. [para(8(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #322 (T,wt=19): 883 (g(x) + (x + (x + (g(x) + (g(x) + h(x))''))'')')' = x. [para(185(a,1),8(a,1,1,1))]. given #323 (T,wt=19): 908 (x + (g(x) + (x + (x + (g(x) + x'')))'')')' = g(x). [para(193(a,1),8(a,1,1,1))]. given #324 (T,wt=19): 976 (x + (y + h(z)))' = (z + (z + (g(z) + (x + (y + z)))))'. [para(7(a,1),255(a,1,1)),rewrite([7(7)])]. given #325 (T,wt=19): 1063 (g(x) + (x + (x + (g(x) + (g(x) + h(x)'')))'')')' = x. [para(299(a,1),8(a,1,1,1))]. given #326 (A,wt=21): 151 ((x + (y + g(z)))' + (x + (y + (z + z')))')' = x + y. [para(10(a,1),22(a,1,1,2,1,2,2)),rewrite([6(10)])]. given #327 (T,wt=19): 1092 ((x + (y + z))' + (z + (y + x'))')' = z + y. [para(6(a,1),50(a,1,1,1,1,2))]. given #328 (T,wt=19): 1093 ((x + (y + z))' + (z + (x' + y))')' = y + z. [para(6(a,1),50(a,1,1,2,1)),rewrite([7(6)])]. Low Water (keep, True_semantics): wt=29 given #329 (T,wt=19): 1191 (x + (y + h(z)))' = (z + (z + (z + (g(z) + (x + y)))))'. [para(7(a,1),446(a,1,1))]. given #330 (T,wt=19): 1194 (x + (y + h(z)))' = (z + (z + (z + (x + (g(z) + y)))))'. [para(19(a,1),446(a,2,1,2,2,2)),rewrite([7(3)])]. given #331 (A,wt=21): 152 ((x + h(y))' + (x + (y + (y + (y + g(y)))'))')' = x + y. [para(12(a,1),22(a,1,1,1,1,2))]. given #332 (T,wt=13): 12169 (x + (x + (g(x) + (g(x) + h(x))))')' = g(x). [para(1194(a,2),312(a,1,1,2)),rewrite([6(5),19(5),6(4)])]. given #333 (T,wt=17): 12176 (g(x) + (x + (x + (g(x) + (g(x) + h(x))))'')')' = x. [para(12169(a,1),8(a,1,1,1))]. given #334 (T,wt=19): 1211 (x + (y + h(z)))' = (z + (z + (z + (x + (y + g(z))))))'. [para(7(a,1),479(a,1,1)),rewrite([7(7)])]. given #335 (T,wt=19): 1531 (x + (x + (x + (x' + (h(x)' + h(x)'))))')' = h(x)'. [para(775(a,1),8(a,1,1,2)),rewrite([19(9),19(8),19(7),6(11)])]. given #336 (A,wt=23): 154 ((x + (y + (z + u)))' + (x + (z + (y + u)'))')' = x + z. [para(19(a,1),22(a,1,1,1,1,2))]. given #337 (T,wt=19): 1545 (g(x) + (g(x) + (g(x) + (x' + (x' + h(x)'))))')' = x'. [para(841(a,1),8(a,1,1,2)),rewrite([19(10),19(9),6(13)])]. given #338 (T,wt=19): 1712 ((x + y)' + (g(x) + (y + (x + x'')'))')' = y. [para(26(a,1),97(a,1,1,2,1,1)),rewrite([6(11)])]. given #339 (T,wt=19): 1716 ((x + (y + (x + (x + g(x)))'))' + (g(x) + y)')' = y. [para(36(a,1),97(a,1,1,2,1,1))]. given #340 (T,wt=19): 1717 ((x + (y + (g(x) + h(x)'')'))' + (g(x) + y)')' = y. [para(38(a,1),97(a,1,1,2,1,1))]. given #341 (A,wt=23): 156 ((x + (y + z))' + (x + (y + (g(z) + (z + z)')))')' = x + y. [para(28(a,1),22(a,1,1,2,1,2,2)),rewrite([6(11)])]. given #342 (T,wt=19): 1718 ((x + y)' + (g(x) + (y + (x + (g(x) + h(x)))'))')' = y. [para(43(a,1),97(a,1,1,2,1,1)),rewrite([6(12)])]. given #343 (T,wt=19): 2087 (x + (y + h(z)))' = (x + (z + (z + (g(z) + (y + z)))))'. [para(125(a,1),23(a,2,1)),rewrite([23(14)])]. given #344 (T,wt=19): 2134 (x + (g(x) + (y + (x + (z + x)))))' = (y + (z + h(x)))'. [para(126(a,1),23(a,2,1)),rewrite([23(20)])]. given #345 (T,wt=19): 2179 (x + (y + h(z)))' = (y + (z + (z + (g(z) + (x + z)))))'. [para(129(a,1),23(a,2,1)),rewrite([23(14)])]. given #346 (A,wt=21): 157 ((x + (y + z))' + (x + (y + (g(z) + h(z)')))')' = x + y. [para(37(a,1),22(a,1,1,2,1,2,2)),rewrite([6(11)])]. given #347 (T,wt=19): 2223 (x + (y + h(z)))' = (z + (x + (z + (g(z) + (y + z)))))'. [para(130(a,1),23(a,2,1)),rewrite([23(14)])]. given #348 (T,wt=19): 2266 ((x + (y + z))' + (x + (y' + z))')' = x + z. [para(6(a,1),59(a,1,1,2,1,2))]. given #349 (T,wt=19): 2267 ((x + (y + z))' + (z + (y' + x))')' = x + z. [para(6(a,1),59(a,1,1,2,1)),rewrite([7(6)])]. given #350 (T,wt=19): 2755 ((g(x) + y)' + (x + (y + (x + (x + g(x)))'))')' = y. [para(36(a,1),323(a,1,1,1,1,1))]. given #351 (A,wt=23): 158 ((x + (y + g(z)))' + (x + (y + (z + (g(z) + h(z))')))')' = x + y. [para(40(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #352 (T,wt=19): 2756 ((g(x) + y)' + (x + (y + (g(x) + h(x)'')'))')' = y. [para(38(a,1),323(a,1,1,1,1,1))]. given #353 (T,wt=19): 2965 (x + (y + h(z)))' = (x + (z + (z + (z + (g(z) + y)))))'. [para(431(a,1),23(a,2,1)),rewrite([23(14)])]. given #354 (T,wt=19): 3017 (x + (y + h(z)))' = (z + (z + (g(z) + (x + (z + y)))))'. [para(432(a,1),23(a,2,1)),rewrite([23(14)])]. given #355 (T,wt=19): 3105 (x + (y + h(z)))' = (y + (z + (z + (z + (g(z) + x)))))'. [para(434(a,1),23(a,2,1)),rewrite([23(14)])]. given #356 (A,wt=25): 159 ((x + (y + z))' + (x + (y + (g(z) + (z + z'')')))')' = x + y. [para(26(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #357 (T,wt=19): 3187 (x + (y + h(z)))' = (z + (x + (z + (z + (g(z) + y)))))'. [para(435(a,1),23(a,2,1)),rewrite([23(14)])]. given #358 (T,wt=19): 3453 (x + (y + h(z)))' = (x + (z + (z + (z + (y + g(z))))))'. [para(461(a,1),23(a,2,1)),rewrite([23(14)])]. given #359 (T,wt=19): 3497 (x + (y + h(z)))' = (z + (z + (x + (z + (y + g(z))))))'. [para(462(a,1),23(a,2,1)),rewrite([23(14)])]. given #360 (T,wt=19): 3582 (x + (y + h(z)))' = (y + (z + (z + (z + (x + g(z))))))'. [para(465(a,1),23(a,2,1)),rewrite([23(14)])]. given #361 (A,wt=29): 160 (x + (y + ((x + (y + z'))' + (x + (y + z))'')'))' = (x + (y + z'))'. [para(22(a,1),20(a,1,1,1)),rewrite([7(12)])]. given #362 (T,wt=19): 3660 (x + (y + h(z)))' = (z + (x + (z + (z + (y + g(z))))))'. [para(466(a,1),23(a,2,1)),rewrite([23(14)])]. given #363 (T,wt=19): 3717 (x' + (g(x) + (g(x) + (x' + (x' + x'))))')' = g(x). [para(487(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #364 (T,wt=19): 3732 (x + (x + (g(x) + (g(x) + (x + x'')'')))')' = g(x). [para(507(a,1),8(a,1,1,2)),rewrite([19(10),6(12)])]. given #365 (T,wt=19): 3746 (g(x) + (x + (x + (g(x) + (x + (x + g(x)))'')))')' = x. [para(510(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #366 (A,wt=27): 161 (((x + (y + z))' + ((x + (y + z'))' + u))' + (u + (x + y))')' = u. [para(22(a,1),20(a,1,1,2,1,2)),rewrite([7(9)])]. given #367 (T,wt=19): 3773 (g(x) + (x + (x + (g(x) + (g(x) + h(x)'')'')))')' = x. [para(511(a,1),8(a,1,1,2)),rewrite([6(14)])]. given #368 (T,wt=19): 3788 (x + (x + (g(x) + (g(x) + (x + (g(x) + h(x)))'')))')' = g(x). [para(512(a,1),8(a,1,1,2)),rewrite([19(11),6(13)])]. given #369 (T,wt=19): 3802 (h(x)' + (x + (x + (g(x)' + (h(x)' + h(x)'))))')' = x. [para(544(a,1),8(a,1,1,2)),rewrite([6(14)])]. given #370 (T,wt=19): 3921 ((x + y)' + ((y + y'')' + (x + g(y)))')' = x. [para(26(a,1),597(a,1,1,2,1,2)),rewrite([6(11)])]. given #371 (A,wt=27): 162 ((x + (y + z))' + (x + (y + ((u + z)' + (z + u')')))')' = x + y. [para(20(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #372 (T,wt=19): 3925 (((x + (x + g(x)))' + (y + x))' + (y + g(x))')' = y. [para(36(a,1),597(a,1,1,2,1,2))]. given #373 (T,wt=19): 3926 (((g(x) + h(x)'')' + (y + x))' + (y + g(x))')' = y. [para(38(a,1),597(a,1,1,2,1,2))]. given #374 (T,wt=19): 3927 ((x + y)' + ((y + (g(y) + h(y)))' + (x + g(y)))')' = x. [para(43(a,1),597(a,1,1,2,1,2)),rewrite([6(12)])]. given #375 (T,wt=19): 4354 (g(x) + (x + (x + (g(x) + (g(x) + (x + x)''))))')' = x. [para(870(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #376 (A,wt=25): 163 ((x + (y + g(z)))' + (x + (y + (z + (z + (z + g(z)))')))')' = x + y. [para(36(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #377 (T,wt=19): 4370 (x + (x + (x + (g(x) + (g(x) + (g(x) + h(x))''))))')' = g(x). [para(884(a,1),8(a,1,1,2)),rewrite([19(11),19(10),6(13)])]. given #378 (T,wt=19): 4386 (g(x) + (x + (x + (x + (g(x) + (g(x) + x'')))))')' = x. [para(909(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #379 (T,wt=19): 4487 (x + (x + (x + (g(x) + (g(x) + (g(x) + h(x)'')))))')' = g(x). [para(1064(a,1),8(a,1,1,2)),rewrite([19(11),19(10),6(13)])]. given #380 (T,wt=19): 4612 ((x + y)' + ((x + x'')' + (y + g(x)))')' = y. [para(26(a,1),1701(a,1,1,2,1,1)),rewrite([6(11)])]. given #381 (A,wt=25): 164 ((x + (y + g(z)))' + (x + (y + (z + (g(z) + h(z)'')')))')' = x + y. [para(38(a,1),22(a,1,1,2,1,2,2)),rewrite([6(15)])]. given #382 (T,wt=19): 4615 ((g(x) + y)' + ((x + (x + g(x)))' + (y + x))')' = y. [para(36(a,1),1701(a,1,1,2,1,1)),rewrite([6(11)])]. given #383 (T,wt=19): 4616 ((g(x) + y)' + ((g(x) + h(x)'')' + (y + x))')' = y. [para(38(a,1),1701(a,1,1,2,1,1)),rewrite([6(13)])]. given #384 (T,wt=19): 4617 ((x + y)' + ((x + (g(x) + h(x)))' + (y + g(x)))')' = y. [para(43(a,1),1701(a,1,1,2,1,1)),rewrite([6(12)])]. given #385 (T,wt=19): 4836 (x + (y + h(z)))' = (z + (z + (g(z) + (y + (z + x)))))'. [para(2033(a,1),23(a,2,1)),rewrite([23(14)])]. given #386 (A,wt=25): 165 ((x + (y + z))' + (x + (y + (g(z) + (z + (g(z) + h(z)))')))')' = x + y. [para(43(a,1),22(a,1,1,2,1,2,2)),rewrite([6(14)])]. given #387 (T,wt=19): 4954 (x + (y + h(z)))' = (z + (z + (g(z) + (y + (x + z)))))'. [para(2040(a,1),23(a,2,1)),rewrite([23(14)])]. given #388 (T,wt=19): 5016 (x + (y + h(z)))' = (z + (z + (x + (g(z) + (y + z)))))'. [para(2042(a,1),23(a,2,1)),rewrite([23(14)])]. given #389 (T,wt=19): 5102 (x + (g(x) + (y + (x + (x + z)))))' = (y + (z + h(x)))'. [para(2112(a,1),23(a,2,1)),rewrite([23(20)])]. given #390 (T,wt=19): 5242 (x + (g(x) + (y + (x + (z + x)))))' = (z + (y + h(x)))'. [para(2120(a,1),23(a,2,1)),rewrite([23(20)])]. given #391 (A,wt=26): 166 ((x + (y + z'))' + (x + (y + (g(z) + (z' + z')')))')' = x + y. [para(56(a,1),22(a,1,1,2,1,2,2)),rewrite([6(14)])]. given #392 (T,wt=19): 5332 (x + (y + h(z)))' = (z + (y + (z + (g(z) + (x + z)))))'. [para(2167(a,1),23(a,2,1)),rewrite([23(14)])]. given #393 (T,wt=19): 5400 (x + (y + h(z)))' = (z + (y + (z + (z + (g(z) + x)))))'. [para(2344(a,1),23(a,2,1)),rewrite([23(14)])]. given #394 (T,wt=19): 5626 ((x + h(y)')' + (y + (y + (g(y) + (x + y))))')' = x. [para(12(a,1),2591(a,1,1,1,1,2,1)),rewrite([7(9),7(8)])]. given #395 (T,wt=19): 5630 ((x + g(y))' + ((y + (y + g(y)))' + (x + y))')' = x. [para(36(a,1),2591(a,1,1,1,1,2))]. given #396 (A,wt=27): 167 ((x + ((y + (z + u))' + (y + (z + u'))'))' + (y + (z + x))')' = x. [para(22(a,1),21(a,1,1,2,1,1)),rewrite([7(12)])]. given #397 (T,wt=19): 5631 ((x + g(y))' + ((g(y) + h(y)'')' + (x + y))')' = x. [para(38(a,1),2591(a,1,1,1,1,2))]. given #398 (T,wt=19): 5716 ((x + (y + z))' + (y' + (z + x))')' = z + x. [para(6(a,1),90(a,1,1,1,1)),rewrite([7(2)])]. given #399 (T,wt=19): 5717 ((x + (y + z))' + (z' + (y + x))')' = x + y. [para(6(a,1),90(a,1,1,2,1,2))]. given #400 (T,wt=19): 6025 (x + (y + h(z)))' = (z + (z + (z + (g(z) + (y + x)))))'. [para(2899(a,1),23(a,2,1)),rewrite([23(14)])]. given #401 (A,wt=27): 168 (x + (y + (x + (y + (z + (x + (y + z'))')))'))' = (x + (y + z'))'. [para(22(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(10),7(10)])]. given #402 (T,wt=19): 6094 (x + (y + h(z)))' = (z + (z + (x + (z + (g(z) + y)))))'. [para(3003(a,1),23(a,2,1)),rewrite([23(14)])]. given #403 (T,wt=19): 6234 (x + (y + h(z)))' = (z + (z + (z + (y + (g(z) + x)))))'. [para(3260(a,1),23(a,2,1)),rewrite([23(14)])]. given #404 (T,wt=19): 6305 (x + (y + h(z)))' = (z + (z + (y + (z + (g(z) + x)))))'. [para(3331(a,1),23(a,2,1)),rewrite([23(14)])]. given #405 (T,wt=19): 6407 (x + (y + h(z)))' = (z + (z + (z + (y + (x + g(z))))))'. [para(3379(a,1),23(a,2,1)),rewrite([23(14)])]. given #406 (A,wt=27): 169 ((x + (y + z))' + (x + (y + ((z + u)' + (u' + z)')))')' = x + y. [para(21(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #407 (T,wt=19): 6474 (x + (y + h(z)))' = (z + (z + (y + (z + (x + g(z))))))'. [para(3485(a,1),23(a,2,1)),rewrite([23(14)])]. given #408 (T,wt=19): 6615 (x + (y + h(z)))' = (z + (y + (z + (z + (x + g(z))))))'. [para(3571(a,1),23(a,2,1)),rewrite([23(14)])]. given #409 (T,wt=19): 6866 (x + (y + h(z)))' = (z + (z + (y + (g(z) + (x + z)))))'. [para(4946(a,1),23(a,2,1)),rewrite([23(14)])]. given #410 (T,wt=19): 6945 (x + (g(x) + (y + (x + (x + z)))))' = (z + (y + h(x)))'. [para(5087(a,1),23(a,2,1)),rewrite([23(20)])]. given #411 (A,wt=26): 170 ((x + (y + h(z)'))' + (x + (y + (z + (g(z)' + h(z)')')))')' = x + y. [para(62(a,1),22(a,1,1,2,1,2,2)),rewrite([6(16)])]. given #412 (T,wt=19): 7252 ((x + h(y))' + (y + (g(y) + (x + (y + y)))')')' = y. [para(7047(a,1),8(a,1,1,1,1))]. given #413 (T,wt=19): 7261 ((x + h(y))' + (g(y) + (y + (x + (y + y)))')')' = g(y). [para(7047(a,1),32(a,1,1,1,1))]. given #414 (T,wt=19): 7335 (g(x) + (y + (x + (x + (x + z)))))' = (y + (z + h(x)))'. [para(7284(a,1),23(a,2,1)),rewrite([23(21)])]. given #415 (T,wt=19): 7726 (g(x) + (y + (x + (x + (z + x)))))' = (y + (z + h(x)))'. [para(7287(a,1),23(a,2,1)),rewrite([23(21)])]. given #416 (A,wt=25): 171 ((x + (y + (y + (g(y) + (z + y)))))' + (x + (z + h(y)'))')' = x + z. [para(30(a,1),22(a,1,1,1,1,2))]. given #417 (T,wt=19): 7858 (g(x) + (y + (x + (x + (x + z)))))' = (z + (y + h(x)))'. [para(7318(a,1),23(a,2,1)),rewrite([23(21)])]. given #418 (T,wt=19): 7960 (g(x) + (y + (x + (x + (z + x)))))' = (z + (y + h(x)))'. [para(7714(a,1),23(a,2,1)),rewrite([23(21)])]. given #419 (T,wt=19): 8185 ((x + h(y))' + (g(y) + (x + (y + (y + y)))')')' = g(y). [para(8180(a,1),8(a,1,1,1,1))]. given #420 (T,wt=19): 8203 ((x + h(y))' + (g(y) + (y + (y + (y + x)))')')' = g(y). [para(8180(a,1),596(a,1,1,1,1)),rewrite([7(7),7(6)])]. given #421 (A,wt=25): 172 ((x + (y + h(z)))' + (x + (z + (z + (g(z) + (y + z)))'))')' = x + z. [para(30(a,2),22(a,1,1,1,1,2))]. given #422 (T,wt=19): 9386 ((x + (y + z'))' + (y + (z + x))')' = x + y. [para(6(a,1),144(a,1,1))]. given #423 (T,wt=19): 9479 ((x + (y' + z))' + (z + (x + y))')' = z + x. [para(6(a,1),145(a,1,1))]. given #424 (T,wt=19): 9654 ((x + (y + z'))' + (y + (x + z))')' = x + y. [para(6(a,1),155(a,1,1))]. given #425 (T,wt=19): 9903 ((x + (y + z))' + (x' + (z + y))')' = z + y. [para(6(a,1),204(a,1,1,1,1)),rewrite([7(2)])]. given #426 (A,wt=21): 173 ((x + h(y))' + (y + (y + (g(y) + (x + y))'))')' = y + y. [para(30(a,2),22(a,1,1,1,1))]. given #427 (T,wt=19): 9904 ((x' + (y + z))' + (y + (x + z))')' = y + z. [para(6(a,1),204(a,1,1))]. given #428 (T,wt=19): 10039 ((x + (y' + z))' + (y + (x + z))')' = x + z. [para(6(a,1),205(a,1,1))]. given #429 (T,wt=19): 10563 ((x' + h(y))' + (y + (y + (g(y) + (x + y))))')' = h(y). [para(6(a,1),222(a,1,1))]. given #430 (T,wt=19): 10762 ((x + (y' + z))' + (y + (z + x))')' = z + x. [para(6(a,1),265(a,1,1,1,1)),rewrite([7(3)])]. given #431 (A,wt=25): 174 ((x + (y + h(z)))' + (x + (z + (y + (z + (z + g(z))))'))')' = x + z. [para(33(a,1),22(a,1,1,1,1,2))]. given #432 (T,wt=19): 10763 ((x + (y + z'))' + (z + (y + x))')' = x + y. [para(6(a,1),265(a,1,1,2,1,2))]. given #433 (T,wt=19): 10826 ((x + (y' + z))' + (z + (y + x))')' = z + x. [para(6(a,1),270(a,1,1,1,1)),rewrite([7(3)])]. given #434 (T,wt=19): 10949 ((x + h(y)')' + (y + (y + (y + (x + g(y)))))')' = x. [para(6(a,1),285(a,1,1,2,1,2,2,2))]. given #435 (T,wt=19): 10958 ((x' + (y + z))' + (z + (y + x))')' = z + y. [para(6(a,1),318(a,1,1,1,1,2))]. given #436 (A,wt=21): 175 ((x + h(y))' + (y + (x + (y + (y + g(y)))'))')' = y + x. [para(33(a,1),22(a,1,1,1,1))]. given #437 (T,wt=19): 10959 ((x' + (y + z))' + (z + (x + y))')' = y + z. [para(6(a,1),318(a,1,1,2,1)),rewrite([7(6)])]. given #438 (T,wt=19): 11293 ((x' + h(y))' + (y + (y + (y + (x + g(y)))))')' = h(y). [para(6(a,1),337(a,1,1,2,1,2,2,2))]. given #439 (T,wt=19): 11487 (h(x)' + (x + (x + (x + g(x)')))')' = x + (x + x). [para(12(a,1),146(a,1,1,1,1))]. given #440 (T,wt=19): 12186 (x + (x + (g(x) + (x + (g(x) + (g(x) + h(x))))''))')' = g(x). [para(12169(a,1),25(a,1,1,2,1,2,2)),rewrite([6(10),12169(23)])]. given #441 (A,wt=21): 177 ((x + g(y))' + (x + (y + (g(y) + (y + y)'')'))')' = x. [para(34(a,1),8(a,1,1,2,1,2)),rewrite([6(13)])]. given #442 (T,wt=19): 13125 ((x + h(y))' + (g(y) + (y + (y + (x + y)))')')' = g(y). [para(19(a,1),7261(a,1,1,2,1,2,1,2))]. given #443 (T,wt=19): 13294 ((x' + (y + z))' + (x + (z + y))')' = y + z. [para(6(a,1),9903(a,1,1))]. given #444 (T,wt=20): 199 (x + ((y + x)' + (y' + x)'')')' = (y + x)'. [para(47(a,1),8(a,1,1,1))]. given #445 (T,wt=20): 216 ((x' + y)' + (g(x) + ((x' + x')' + y))')' = y. [para(56(a,1),47(a,1,1,2,1,1)),rewrite([7(7),6(12)])]. given #446 (A,wt=24): 179 (g(x) + (x' + (g(x) + (x + x)'')')')' = (g(x) + (x + x)'')'. [para(34(a,1),20(a,1,1,1)),rewrite([6(9)])]. given #447 (T,wt=20): 220 ((h(x)' + y)' + (x + ((g(x)' + h(x)')' + y))')' = y. [para(62(a,1),47(a,1,1,2,1,1)),rewrite([7(8),6(14)])]. given #448 (T,wt=20): 280 ((x + y')' + (g(y) + ((y' + y')' + x))')' = x. [para(56(a,1),48(a,1,1,1,1,2)),rewrite([7(10)])]. given #449 (T,wt=20): 283 ((x + h(y)')' + (y + ((g(y)' + h(y)')' + x))')' = x. [para(62(a,1),48(a,1,1,1,1,2)),rewrite([7(12)])]. given #450 (T,wt=20): 333 ((x' + y)' + (y + (g(x) + (x' + x')'))')' = y. [para(56(a,1),89(a,1,1,1,1,1))]. given #451 (A,wt=21): 180 ((x + ((g(x) + (x + x)'')' + y))' + (y + g(x))')' = y. [para(34(a,1),20(a,1,1,2,1,2)),rewrite([7(8)])]. given #452 (T,wt=20): 336 ((h(x)' + y)' + (y + (x + (g(x)' + h(x)')'))')' = y. [para(62(a,1),89(a,1,1,1,1,1))]. given #453 (T,wt=20): 357 (g(x) + (x + ((x' + y)' + (x' + y')'))')' = x. [para(10(a,1),24(a,1,1,1))]. given #454 (T,wt=20): 365 (x + (g(x) + ((h(x)' + y)' + (h(x)' + y')'))')' = g(x). [para(37(a,1),24(a,1,1,1))]. given #455 (T,wt=20): 500 ((x + y)' + (x + (x + (y' + (x + y)')))')' = x. [para(25(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #456 (A,wt=21): 181 ((x + (y + (g(y) + (y + y)'')'))' + (g(y) + x)')' = x. [para(34(a,1),21(a,1,1,2,1,1))]. given #457 (T,wt=20): 558 (x + (x + (y + (y' + (x + g(y))')))')' = (x + g(y))'. [para(27(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #458 (T,wt=20): 572 (x + (x + (g(y) + (h(y)' + (x + y)')))')' = (x + y)'. [para(39(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. given #459 (T,wt=20): 611 ((x + y')' + (g(y) + (x + (y' + y')'))')' = x. [para(56(a,1),32(a,1,1,2,1,2)),rewrite([6(12)])]. given #460 (T,wt=20): 615 ((x + h(y)')' + (y + (x + (g(y)' + h(y)')'))')' = x. [para(62(a,1),32(a,1,1,2,1,2)),rewrite([6(14)])]. given #461 (A,wt=27): 182 ((x + (y + g(z)))' + (x + (y + (z + (g(z) + (z + z)'')')))')' = x + y. [para(34(a,1),22(a,1,1,2,1,2,2)),rewrite([6(15)])]. given #462 (T,wt=20): 663 (x + (y + (y' + (x + (x + g(y))')))')' = (x + g(y))'. [para(57(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #463 (T,wt=20): 684 (x + (g(y) + (h(y)' + (x + (x + y)')))')' = (x + y)'. [para(63(a,1),21(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. given #464 (T,wt=20): 758 (x + (x + (y + (y' + (g(y) + x)')))')' = (g(y) + x)'. [para(96(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #465 (T,wt=20): 802 (x + (x + (g(y) + (h(y)' + (y + x)')))')' = (y + x)'. [para(100(a,1),21(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. given #466 (A,wt=21): 184 ((x + y)' + (x + (g(y) + (y + (g(y) + h(y))'')'))')' = x. [para(41(a,1),8(a,1,1,2,1,2)),rewrite([6(14)])]. given #467 (T,wt=20): 925 (x + (y + (y' + (x + (g(y) + x)')))')' = (g(y) + x)'. [para(203(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #468 (T,wt=20): 949 (x + (g(y) + (h(y)' + (x + (y + x)')))')' = (y + x)'. [para(207(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. given #469 (T,wt=20): 1229 ((x + x)' + (x + (g(x)' + (x + x)')'')')' = x. [para(28(a,1),51(a,1,1,2,1,1)),rewrite([6(7),28(18)])]. given #470 (T,wt=20): 1231 ((g(x) + h(x))' + (g(x) + (x' + (g(x) + h(x))')'')')' = g(x). [para(40(a,1),51(a,1,1,2,1,1)),rewrite([6(11),40(23)])]. given #471 (A,wt=24): 186 (x + (g(x)' + (x + (g(x) + h(x))'')')')' = (x + (g(x) + h(x))'')'. [para(41(a,1),20(a,1,1,1)),rewrite([6(10)])]. given #472 (T,wt=20): 1264 (x + (y + (x + (y' + (x + g(y))')))')' = (x + g(y))'. [para(559(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #473 (T,wt=20): 1283 (x + (g(y) + (x + (h(y)' + (x + y)')))')' = (x + y)'. [para(573(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. given #474 (T,wt=20): 1307 (x + (y + (x + (y' + (g(y) + x)')))')' = (g(y) + x)'. [para(751(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #475 (T,wt=20): 1323 (x + (g(y) + (x + (h(y)' + (y + x)')))')' = (y + x)'. [para(796(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. given #476 (A,wt=21): 192 ((x + g(y))' + (x + (y + (y + (g(y) + y''))'))')' = x. [para(46(a,1),8(a,1,1,2,1,2)),rewrite([6(13)])]. given #477 (T,wt=20): 1346 (g(x) + (x + ((y + x')' + (x' + y')'))')' = x. [para(10(a,1),52(a,1,1,1))]. given #478 (T,wt=20): 1354 (x + (g(x) + ((y + h(x)')' + (h(x)' + y')'))')' = g(x). [para(37(a,1),52(a,1,1,1))]. given #479 (T,wt=20): 1463 ((x + y)' + (y + (y + (x' + (x + y)')))')' = y. [para(53(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #480 (T,wt=20): 1719 ((g(x) + (y + (x' + x')'))' + (x' + y)')' = y. [para(56(a,1),97(a,1,1,2,1,1))]. given #481 (A,wt=24): 194 (g(x) + (x' + (x + (g(x) + x''))')')' = (x + (g(x) + x''))'. [para(46(a,1),20(a,1,1,1)),rewrite([6(9)])]. given #482 (T,wt=20): 1723 ((x + (y + (g(x)' + h(x)')'))' + (h(x)' + y)')' = y. [para(62(a,1),97(a,1,1,2,1,1))]. given #483 (T,wt=20): 1814 (g(x) + (g(x) + ((x + x)' + (g(x) + h(x))'))')' = (g(x) + h(x))'. [para(40(a,1),99(a,1,1,2)),rewrite([6(9),7(9),6(12)])]. given #484 (T,wt=20): 1841 (x' + (g(x) + (g(x) + (x' + (x + x)'))'')')' = g(x). [para(1811(a,1),8(a,1,1,1))]. given #485 (T,wt=20): 1990 (x + (x + ((x + x)' + (g(x) + h(x))'))')' = (x + x)'. [para(28(a,1),101(a,1,1,2)),rewrite([19(8),6(10)])]. given #486 (A,wt=21): 195 ((x + ((x + (g(x) + x''))' + y))' + (y + g(x))')' = y. [para(46(a,1),20(a,1,1,2,1,2)),rewrite([7(8)])]. given #487 (T,wt=20): 2012 (h(x)' + (x + (x + (h(x)' + (g(x) + h(x))'))'')')' = x. [para(1991(a,1),8(a,1,1,1))]. given #488 (T,wt=20): 2359 (x + (x + (x + (x + (h(x)' + (x + g(x))')))'))' = h(x)'. [para(153(a,1),8(a,1,1,2)),rewrite([19(8),19(7),6(11),7(11)])]. given #489 (T,wt=20): 2757 ((x' + y)' + (g(x) + (y + (x' + x')'))')' = y. [para(56(a,1),323(a,1,1,1,1,1))]. given #490 (T,wt=20): 2759 ((h(x)' + y)' + (x + (y + (g(x)' + h(x)')'))')' = y. [para(62(a,1),323(a,1,1,1,1,1))]. given #491 (A,wt=21): 196 ((x + (y + (y + (g(y) + y''))'))' + (g(y) + x)')' = x. [para(46(a,1),21(a,1,1,2,1,1))]. given #492 (T,wt=20): 3928 (((x' + x')' + (y + g(x)))' + (y + x')')' = y. [para(56(a,1),597(a,1,1,2,1,2))]. given #493 (T,wt=20): 3930 (((g(x)' + h(x)')' + (y + x))' + (y + h(x)')')' = y. [para(62(a,1),597(a,1,1,2,1,2))]. given #494 (T,wt=20): 4080 (x + (y' + (x + (y + (x + g(y))')))')' = (x + g(y))'. [para(3915(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #495 (T,wt=20): 4105 (x + (h(y)' + (x + (g(y) + (x + y)')))')' = (x + y)'. [para(3919(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. given #496 (A,wt=27): 197 ((x + (y + g(z)))' + (x + (y + (z + (z + (g(z) + z''))')))')' = x + y. [para(46(a,1),22(a,1,1,2,1,2,2)),rewrite([6(15)])]. given #497 (T,wt=20): 4133 (x + (y' + (x + (y + (g(y) + x)')))')' = (g(y) + x)'. [para(4071(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #498 (T,wt=20): 4190 (x + (h(y)' + (x + (g(y) + (y + x)')))')' = (y + x)'. [para(4101(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. given #499 (T,wt=20): 4470 (x + (g(x) + (x + (g(x) + (h(x)' + (x + x)')))'))' = h(x)'. [para(1000(a,1),8(a,1,1,2)),rewrite([19(8),19(7),6(12),7(12)])]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 275 (0.00 of 25.08 sec). given #500 (T,wt=7): 14619 (x + h(x)')' = g(x). [para(4470(a,1),32(a,1,1,1)),rewrite([572(14),28(7),6(3)])]. given #501 (A,wt=21): 200 ((x + y)' + (x + ((z + y)' + (z' + y)'))')' = x. [para(47(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #502 (T,wt=9): 14629 (g(x) + (x + h(x))')' = x. [para(14619(a,1),8(a,1,1,2)),rewrite([6(5)])]. given #503 (T,wt=11): 14627 (g(x) + (x + h(x)'')')' = x. [para(14619(a,1),8(a,1,1,1))]. given #504 (T,wt=11): 14683 (x + (x + (g(x) + h(x)))')' = g(x). [para(14619(a,1),95(a,1,1,2,1,2,2)),rewrite([6(3),14619(11)])]. given #505 (T,wt=9): 14993 (x + (g(x) + h(x)))' = h(x)'. [para(14683(a,1),100(a,1,1,2)),rewrite([6(10),7(10),6(13),14690(14)]),flip(a)]. given #506 (A,wt=21): 202 ((x + y)' + ((x + z)' + ((x + z')' + y))')' = y. [para(8(a,1),47(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #507 (T,wt=12): 14630 (g(x) + (x' + h(x)')')' = h(x)'. [para(14619(a,1),20(a,1,1,1)),rewrite([6(5)])]. given #508 (T,wt=13): 14645 (x + (x + (g(x) + h(x)''))')' = g(x). [para(14619(a,1),25(a,1,1,2,1,2,2)),rewrite([6(5),14619(13)])]. given #509 (T,wt=13): 14657 (x + (g(x) + (x + h(x))'')')' = g(x). [para(14619(a,1),54(a,1,1,2,1,1)),rewrite([14619(13)])]. given #510 (T,wt=13): 14755 (h(x)' + (x + (x + g(x))')')' = x. [back_rewrite(14492),rewrite([14682(13)])]. given #511 (A,wt=21): 210 (x + ((y' + x)' + (y + x)'')')' = (y' + x)'. [para(47(a,1),20(a,1,1,1))]. given #512 (T,wt=13): 14817 (g(x) + (x + (x + (g(x) + h(x))))')' = x. [para(14629(a,1),95(a,1,1,2,1,2,2)),rewrite([6(5),19(6),19(5),14629(15)])]. given #513 (T,wt=14): 14647 (g(x) + (g(x) + (h(x)' + h(x)'))')' = h(x)'. [para(14619(a,1),100(a,1,1,2)),rewrite([19(7),6(10)])]. given #514 (T,wt=14): 14655 (h(x)' + (g(x) + (x' + h(x)'))')' = g(x). [para(14619(a,1),53(a,1,1,2,1,2,2)),rewrite([6(7),6(8),7(8),14619(15)])]. given #515 (T,wt=15): 14628 ((x + g(y))' + (x + (y + h(y)'))')' = x. [para(14619(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. given #516 (A,wt=21): 211 (((x + y)' + ((x' + y)' + z))' + (z + y)')' = z. [para(47(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #517 (T,wt=15): 14631 ((x + (h(x)' + y))' + (y + g(x))')' = y. [para(14619(a,1),20(a,1,1,2,1,2)),rewrite([7(4)])]. given #518 (T,wt=15): 14632 ((x + (y + h(y)'))' + (g(y) + x)')' = x. [para(14619(a,1),21(a,1,1,2,1,1))]. given #519 (T,wt=14): 15778 (x + (x + (h(x)' + h(x)'))')' = h(x)'. [para(37(a,1),14632(a,1,1,2)),rewrite([19(6),6(8)])]. given #520 (T,wt=15): 14634 ((g(x) + y)' + (x + (h(x)' + y))')' = y. [para(14619(a,1),47(a,1,1,2,1,1)),rewrite([7(4),6(9)])]. given #521 (A,wt=21): 212 ((x + y)' + ((z + x)' + ((x + z')' + y))')' = y. [para(20(a,1),47(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #522 (T,wt=15): 14635 (x + (g(x) + (x + h(x)'')'')')' = g(x). [para(14619(a,1),23(a,1,1,2,1,1)),rewrite([14619(15)])]. given #523 (T,wt=15): 14638 ((x + g(y))' + (y + (h(y)' + x))')' = x. [para(14619(a,1),48(a,1,1,1,1,2)),rewrite([7(7)])]. given #524 (T,wt=15): 14639 ((g(x) + y)' + (y + (x + h(x)'))')' = y. [para(14619(a,1),89(a,1,1,1,1,1))]. given #525 (T,wt=15): 14646 ((x + g(y))' + (y + (x + h(y)'))')' = x. [para(14619(a,1),32(a,1,1,2,1,2)),rewrite([6(9)])]. given #526 (A,wt=21): 217 ((x + ((y + z)' + (y' + z)'))' + (z + x)')' = x. [para(47(a,1),21(a,1,1,2,1,1))]. given #527 (T,wt=15): 14659 ((x + (y + h(x)'))' + (g(x) + y)')' = y. [para(14619(a,1),97(a,1,1,2,1,1))]. given #528 (T,wt=15): 14667 ((g(x) + y)' + (x + (y + h(x)'))')' = y. [para(14619(a,1),323(a,1,1,1,1,1))]. given #529 (T,wt=15): 14670 ((h(x)' + (y + x))' + (y + g(x))')' = y. [para(14619(a,1),597(a,1,1,2,1,2))]. given #530 (T,wt=15): 14671 ((g(x) + y)' + (h(x)' + (y + x))')' = y. [para(14619(a,1),1701(a,1,1,2,1,1)),rewrite([6(9)])]. given #531 (A,wt=21): 219 ((x + y)' + ((x + z)' + ((z' + x)' + y))')' = y. [para(21(a,1),47(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #532 (T,wt=15): 14672 ((x + g(y))' + (h(y)' + (x + y))')' = x. [para(14619(a,1),2591(a,1,1,1,1,2))]. given #533 (T,wt=15): 14746 (g(x) + (x + (x + (g(x) + h(x)'')))')' = x. [para(14619(a,1),500(a,1,1,1)),rewrite([14619(8),6(6)])]. given #534 (T,wt=15): 14783 (g(x) + (x + (g(x) + (x + h(x))''))')' = x. [para(14629(a,1),25(a,1,1,2,1,2,2)),rewrite([6(7),19(8),14629(17)])]. given #535 (T,wt=15): 15004 (x + (x + (x + (x + (g(x) + g(x))))))' = h(x)'. [para(30(a,1),14993(a,1,1,2)),rewrite([6(3),19(4)])]. ============================== PROOF ================================= % Proof 1 at 27.39 (+ 0.11) seconds: Winker2b. % Length of proof is 41. % Level of proof is 13. % Maximum clause weight is 30. % Given clauses 535. 5 (exists a exists b (a + b)' = b') # answer(Winker2b) # label(non_clause) # label(goal). [goal]. 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]. 9 g(x) = (x + x')' # label(definition_g). [assumption]. 10 (x + x')' = g(x). [copy(9),flip(a)]. 11 h(x) = x + (x + (x + g(x))) # label(definition_h). [assumption]. 12 x + (x + (x + g(x))) = h(x). [copy(11),flip(a)]. 17 (x + y)' != y' # answer(Winker2b). [deny(5)]. 19 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),rewrite([7(2)])]. 20 ((x + y)' + (y + x')')' = y. [para(6(a,1),8(a,1,1,1,1))]. 21 ((x + y)' + (y' + x)')' = x. [para(6(a,1),8(a,1,1,2,1))]. 28 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. 29 h(x) + y = x + (x + (x + (g(x) + y))). [para(12(a,1),7(a,1,1)),rewrite([7(6),7(5)])]. 30 x + h(y) = y + (y + (g(y) + (x + y))). [para(12(a,1),7(a,2,2)),rewrite([19(5),19(4),6(3)]),flip(a)]. 31 (h(x)' + (x + (x + (x + g(x)))')')' = x. [para(12(a,1),8(a,1,1,1,1))]. 32 ((x + (y + z))' + (y + (x + z)')')' = y. [para(19(a,1),8(a,1,1,1,1))]. 36 (x + (x + (x + g(x)))')' = g(x). [para(28(a,1),8(a,1,1,2)),rewrite([19(3),6(2),6(5)])]. 37 (g(x) + h(x)')' = x. [back_rewrite(31),rewrite([36(8),6(4)])]. 39 ((x + y)' + (x + (g(y) + h(y)'))')' = x. [para(37(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. 40 (x + (g(x) + h(x))')' = g(x). [para(37(a,1),8(a,1,1,2)),rewrite([6(5)])]. 43 (g(x) + (x + (g(x) + h(x)))')' = x. [para(40(a,1),8(a,1,1,2)),rewrite([6(7)])]. 49 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),20(a,1,1,1,1))]. 53 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(20(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 95 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 99 ((x + (g(y) + (y + y)'))' + (y + x)')' = x. [para(28(a,1),21(a,1,1,2,1,1))]. 100 ((x + (g(y) + h(y)'))' + (y + x)')' = x. [para(37(a,1),21(a,1,1,2,1,1))]. 109 ((x + (g(y) + (y + (g(y) + h(y)))'))' + (y + x)')' = x. [para(43(a,1),21(a,1,1,2,1,1))]. 572 (x + (x + (g(y) + (h(y)' + (x + y)')))')' = (x + y)'. [para(39(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. 1000 (h(x)' + (x + (g(x) + (x + x)'))')' = x + g(x). [para(12(a,1),49(a,1,1,1,1)),rewrite([7(7)])]. 1477 (x + (x + (x + (g(x) + (x + (x + (x + (g(x) + (y' + (y + h(x))')))))'))))' = (y + h(x))'. [para(29(a,1),53(a,1,1,2,1)),rewrite([29(13)])]. 1812 (h(x)' + (x + (x + (g(x) + (g(x) + (x + x)'))))')' = x + (x + g(x)). [para(12(a,1),99(a,1,1,2,1)),rewrite([19(8),7(7),7(6),19(8),19(7),6(12)])]. 4470 (x + (g(x) + (x + (g(x) + (h(x)' + (x + x)')))'))' = h(x)'. [para(1000(a,1),8(a,1,1,2)),rewrite([19(8),19(7),6(12),7(12)])]. 14619 (x + h(x)')' = g(x). [para(4470(a,1),32(a,1,1,1)),rewrite([572(14),28(7),6(3)])]. 14683 (x + (x + (g(x) + h(x)))')' = g(x). [para(14619(a,1),95(a,1,1,2,1,2,2)),rewrite([6(3),14619(11)])]. 14690 (g(x) + (g(x) + (h(x)' + (x + (g(x) + h(x)))'))')' = h(x)'. [para(14619(a,1),109(a,1,1,2)),rewrite([19(10),6(13)])]. 14993 (x + (g(x) + h(x)))' = h(x)'. [para(14683(a,1),100(a,1,1,2)),rewrite([6(10),7(10),6(13),14690(14)]),flip(a)]. 15004 (x + (x + (x + (x + (g(x) + g(x))))))' = h(x)'. [para(30(a,1),14993(a,1,1,2)),rewrite([6(3),19(4)])]. 16389 x + (x + (g(x) + g(x))) = x + (x + g(x)). [para(15004(a,1),49(a,1,1,1)),rewrite([7(10),7(9),7(8),1812(13)]),flip(a)]. 16397 (x + h(x))' = h(x)'. [para(15004(a,1),53(a,2)),rewrite([16389(5),12(4),16389(6),12(5),16389(8),12(7),29(8),29(13),1477(17)])]. 16398 $F # answer(Winker2b). [resolve(16397,a,17,a)]. ============================== end of proof ========================== % Redundant proof: 16499 $F # answer(Winker2b). [resolve(16498,a,17,a)]. % Disable descendants (x means already disabled): 17 given #536 (A,wt=25): 224 ((x + h(y))' + (y + (g(y) + (y' + (x + y))))')' = y + (g(y) + (x + y)). [para(30(a,2),47(a,1,1,1,1)),rewrite([19(9),19(8)])]. given #537 (T,wt=7): 16397 (x + h(x))' = h(x)'. [para(15004(a,1),53(a,2)),rewrite([16389(5),12(4),16389(6),12(5),16389(8),12(7),29(8),29(13),1477(17)])]. given #538 (T,wt=7): 16498 (g(x) + h(x))' = h(x)'. [back_rewrite(14441),rewrite([16389(9),12(8),6(7),14660(11)]),flip(a)]. given #539 (T,wt=11): 16497 (g(x) + (x + (x + h(x)))')' = x. [back_rewrite(15465),rewrite([16389(6),12(5)])]. given #540 (T,wt=13): 16389 x + (x + (g(x) + g(x))) = x + (x + g(x)). [para(15004(a,1),49(a,1,1,1)),rewrite([7(10),7(9),7(8),1812(13)]),flip(a)]. ============================== PROOF ================================= % Proof 2 at 28.11 (+ 0.11) seconds: Winker1b. % Length of proof is 39. % Level of proof is 13. % Maximum clause weight is 23. % Given clauses 540. 3 (exists a exists b a + b = b) # answer(Winker1b) # label(non_clause) # label(goal). [goal]. 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]. 9 g(x) = (x + x')' # label(definition_g). [assumption]. 10 (x + x')' = g(x). [copy(9),flip(a)]. 11 h(x) = x + (x + (x + g(x))) # label(definition_h). [assumption]. 12 x + (x + (x + g(x))) = h(x). [copy(11),flip(a)]. 15 x + y != y # answer(Winker1b). [deny(3)]. 19 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),rewrite([7(2)])]. 20 ((x + y)' + (y + x')')' = y. [para(6(a,1),8(a,1,1,1,1))]. 21 ((x + y)' + (y' + x)')' = x. [para(6(a,1),8(a,1,1,2,1))]. 28 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. 29 h(x) + y = x + (x + (x + (g(x) + y))). [para(12(a,1),7(a,1,1)),rewrite([7(6),7(5)])]. 30 x + h(y) = y + (y + (g(y) + (x + y))). [para(12(a,1),7(a,2,2)),rewrite([19(5),19(4),6(3)]),flip(a)]. 31 (h(x)' + (x + (x + (x + g(x)))')')' = x. [para(12(a,1),8(a,1,1,1,1))]. 32 ((x + (y + z))' + (y + (x + z)')')' = y. [para(19(a,1),8(a,1,1,1,1))]. 36 (x + (x + (x + g(x)))')' = g(x). [para(28(a,1),8(a,1,1,2)),rewrite([19(3),6(2),6(5)])]. 37 (g(x) + h(x)')' = x. [back_rewrite(31),rewrite([36(8),6(4)])]. 39 ((x + y)' + (x + (g(y) + h(y)'))')' = x. [para(37(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. 40 (x + (g(x) + h(x))')' = g(x). [para(37(a,1),8(a,1,1,2)),rewrite([6(5)])]. 43 (g(x) + (x + (g(x) + h(x)))')' = x. [para(40(a,1),8(a,1,1,2)),rewrite([6(7)])]. 49 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),20(a,1,1,1,1))]. 95 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 99 ((x + (g(y) + (y + y)'))' + (y + x)')' = x. [para(28(a,1),21(a,1,1,2,1,1))]. 100 ((x + (g(y) + h(y)'))' + (y + x)')' = x. [para(37(a,1),21(a,1,1,2,1,1))]. 109 ((x + (g(y) + (y + (g(y) + h(y)))'))' + (y + x)')' = x. [para(43(a,1),21(a,1,1,2,1,1))]. 572 (x + (x + (g(y) + (h(y)' + (x + y)')))')' = (x + y)'. [para(39(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. 1000 (h(x)' + (x + (g(x) + (x + x)'))')' = x + g(x). [para(12(a,1),49(a,1,1,1,1)),rewrite([7(7)])]. 1812 (h(x)' + (x + (x + (g(x) + (g(x) + (x + x)'))))')' = x + (x + g(x)). [para(12(a,1),99(a,1,1,2,1)),rewrite([19(8),7(7),7(6),19(8),19(7),6(12)])]. 4470 (x + (g(x) + (x + (g(x) + (h(x)' + (x + x)')))'))' = h(x)'. [para(1000(a,1),8(a,1,1,2)),rewrite([19(8),19(7),6(12),7(12)])]. 14619 (x + h(x)')' = g(x). [para(4470(a,1),32(a,1,1,1)),rewrite([572(14),28(7),6(3)])]. 14683 (x + (x + (g(x) + h(x)))')' = g(x). [para(14619(a,1),95(a,1,1,2,1,2,2)),rewrite([6(3),14619(11)])]. 14690 (g(x) + (g(x) + (h(x)' + (x + (g(x) + h(x)))'))')' = h(x)'. [para(14619(a,1),109(a,1,1,2)),rewrite([19(10),6(13)])]. 14993 (x + (g(x) + h(x)))' = h(x)'. [para(14683(a,1),100(a,1,1,2)),rewrite([6(10),7(10),6(13),14690(14)]),flip(a)]. 15004 (x + (x + (x + (x + (g(x) + g(x))))))' = h(x)'. [para(30(a,1),14993(a,1,1,2)),rewrite([6(3),19(4)])]. 16389 x + (x + (g(x) + g(x))) = x + (x + g(x)). [para(15004(a,1),49(a,1,1,1)),rewrite([7(10),7(9),7(8),1812(13)]),flip(a)]. 16824 g(x) + h(x) = h(x). [para(16389(a,1),29(a,2,2)),rewrite([6(3),12(7)])]. 16825 $F # answer(Winker1b). [resolve(16824,a,15,a)]. ============================== end of proof ========================== % Redundant proof: 16839 $F # answer(Winker1b). [resolve(16838,a,15,a)]. % Redundant proof: 16849 $F # answer(Winker1b). [resolve(16848,a,15,a)]. % Redundant proof: 16942 $F # answer(Winker1b). [resolve(16941,a,15,a)]. % Disable descendants (x means already disabled): 15 given #541 (A,wt=25): 225 ((x + h(y))' + (y' + (x + (y + (y + g(y)))))')' = x + (y + (y + g(y))). [para(33(a,1),47(a,1,1,1,1))]. given #542 (T,wt=5): 16824 g(x) + h(x) = h(x). [para(16389(a,1),29(a,2,2)),rewrite([6(3),12(7)])]. given #543 (T,wt=9): 16838 g(x) + (y + h(x)) = y + h(x). [para(16389(a,1),434(a,2,2,2)),rewrite([12(8)])]. given #544 (T,wt=11): 16899 (x + (x + (x + h(x)))')' = g(x). [back_rewrite(14997),rewrite([16819(7),16389(5),12(4)])]. given #545 (T,wt=13): 16894 (g(x) + (x + (x + (x + h(x))))')' = x. [back_rewrite(15489),rewrite([16819(8),16389(6),12(5)])]. given #546 (A,wt=27): 226 ((x + (y + z))' + (x + (y + ((u + z)' + (u' + z)')))')' = x + y. [para(47(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #547 (T,wt=13): 17089 g(x) + (y + (z + h(x))) = y + (z + h(x)). [para(7(a,1),16838(a,1,2)),rewrite([7(8)])]. given #548 (T,wt=13): 17191 (x + (x + (x + (x + h(x))))')' = g(x). [para(16899(a,1),95(a,1,1,2,1,2,2)),rewrite([6(5),19(5),19(4),16824(3),16899(13)])]. given #549 (T,wt=15): 15005 (h(x)' + (x + (g(x) + h(x)'))')' = x + g(x). [para(14993(a,1),22(a,1,1,1))]. given #550 (T,wt=15): 16400 ((x + (y + h(x)))' + (h(x)' + y)')' = y. [para(15004(a,1),97(a,1,1,2,1,1)),rewrite([16389(5),12(4)])]. given #551 (A,wt=27): 227 ((x + (y + z))' + ((x + (y + u))' + ((x + (y + u'))' + z))')' = z. [para(22(a,1),47(a,1,1,2,1,1)),rewrite([7(9),7(12),6(14)])]. given #552 (T,wt=15): 16407 ((h(x)' + y)' + (x + (y + h(x)))')' = y. [para(15004(a,1),323(a,1,1,1,1,1)),rewrite([16389(9),12(8)])]. given #553 (T,wt=15): 16409 ((x + (y + h(y)))' + (x + h(y)')')' = x. [para(15004(a,1),596(a,1,1,2,1,2)),rewrite([16389(5),12(4),6(2)])]. given #554 (T,wt=15): 16411 ((x + h(y)')' + (y + (x + h(y)))')' = x. [para(15004(a,1),598(a,1,1,1,1,2)),rewrite([16389(9),12(8)])]. given #555 (T,wt=15): 16412 ((x + (y + h(y)))' + (h(y)' + x)')' = x. [para(15004(a,1),1700(a,1,1,2,1,1)),rewrite([16389(5),12(4),6(2)])]. given #556 (A,wt=21): 228 ((g(x) + y)' + (x + ((g(x) + (x + x)'')' + y))')' = y. [para(34(a,1),47(a,1,1,2,1,1)),rewrite([7(8),6(13)])]. given #557 (T,wt=15): 16418 ((h(x)' + y)' + (y + (x + h(x)))')' = y. [para(15004(a,1),2748(a,1,1,1,1,1)),rewrite([16389(9),12(8),6(6)])]. given #558 (T,wt=15): 16495 ((x + (y + h(x)))' + (y + h(x)')')' = y. [back_rewrite(16388),rewrite([16389(5),12(4)])]. given #559 (T,wt=15): 16700 (x + (g(x) + (x + (x + h(x)))'')')' = g(x). [para(16497(a,1),8(a,1,1,1))]. given #560 (T,wt=15): 16895 (g(x) + (x + (x + (x + h(x)))'')')' = x. [back_rewrite(15478),rewrite([16819(8),16389(6),12(5)])]. given #561 (A,wt=21): 230 ((g(x) + y)' + (x + ((x + (g(x) + x''))' + y))')' = y. [para(46(a,1),47(a,1,1,2,1,1)),rewrite([7(8),6(13)])]. given #562 (T,wt=15): 16896 (x + (x + (x + (g(x) + h(x)'')))')' = g(x). [back_rewrite(15239),rewrite([16819(9)])]. given #563 (T,wt=15): 17022 (x + (x + (x + (g(x) + x'')))')' = g(x). [back_rewrite(909),rewrite([16819(8)])]. given #564 (T,wt=15): 17055 x + h(y) = y + (y + (y + (g(y) + (x + g(y))))). [para(16824(a,1),7(a,2,2)),rewrite([6(4),29(4)]),flip(a)]. given #565 (T,wt=15): 17057 ((x + h(y))' + (g(y) + (x + h(y))')')' = g(y). [para(16824(a,1),32(a,1,1,1,1,2))]. given #566 (A,wt=21): 231 ((x + y)' + ((z + x)' + ((z' + x)' + y))')' = y. [para(47(a,1),47(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #567 (T,wt=15): 17060 x + (x + (x + (y + (g(x) + g(x))))) = y + h(x). [para(16824(a,1),436(a,1,2)),flip(a)]. Low Water (keep, True_semantics): wt=28 given #568 (T,wt=15): 17287 (g(x) + (x + (x + (x + (x + h(x)))))')' = x. [para(16894(a,1),95(a,1,1,2,1,2,2)),rewrite([6(7),19(8),19(7),19(6),19(5),16824(4),16894(17)])]. given #569 (T,wt=15): 17460 (x + (x + (x + (x + (x + h(x)))))')' = g(x). [para(17191(a,1),95(a,1,1,2,1,2,2)),rewrite([6(6),19(6),19(5),19(4),16824(3),17191(15)])]. given #570 (T,wt=15): 17934 (h(x)' + (g(x) + (g(x) + h(x)'))')' = g(x) + g(x). [para(17060(a,1),121(a,1,1,1,1)),rewrite([16824(3),7(8)])]. given #571 (A,wt=24): 232 ((x + y)' + (x + ((x + y)' + (x + y')'')'')')' = x. [para(23(a,1),8(a,1,1,1))]. given #572 (T,wt=16): 14649 (h(x)' + (g(x) + (x' + h(x)')'')')' = g(x). [para(14619(a,1),51(a,1,1,2,1,1)),rewrite([6(7),14619(17)])]. given #573 (T,wt=16): 14660 (g(x) + (g(x) + (h(x)' + (x + x)'))')' = h(x)'. [para(14619(a,1),99(a,1,1,2)),rewrite([19(7),6(10)])]. given #574 (T,wt=16): 14702 (g(x) + (x + (x + (g(x)' + h(x)')'))')' = x. [para(14619(a,1),114(a,1,1,1))]. given #575 (T,wt=16): 14748 (h(x)' + (g(x) + (g(x) + (h(x)' + h(x)')))')' = g(x). [para(14619(a,1),802(a,1,1,2,1,2,2,2)),rewrite([6(9),19(11),19(10),14619(18)])]. given #576 (A,wt=28): 233 ((x + (y + z)')' + (x + (y + ((y + z)' + (y + z')'')'))')' = x. [para(23(a,1),8(a,1,1,2,1,2)),rewrite([6(16)])]. given #577 (T,wt=16): 14750 (x + (g(x) + (g(x) + (x' + h(x)')'))')' = g(x). [para(14619(a,1),1354(a,1,1,2,1,2,1)),rewrite([6(6)])]. given #578 (T,wt=16): 14754 (x + (x + (h(x)' + (x + g(x))'))')' = h(x)'. [back_rewrite(14496),rewrite([14682(13)])]. given #579 (T,wt=16): 15814 (h(x)' + (x + (x + (h(x)' + h(x)')))')' = x. [para(15778(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #580 (T,wt=17): 14752 (g(x) + (g(x) + (x' + (h(x)' + h(x)')))')' = h(x)'. [para(14619(a,1),1463(a,1,1,1)),rewrite([14619(10),6(8),6(9),7(9),19(10),19(9)])]. given #581 (A,wt=22): 234 ((x + y)' + (x + ((x + y)' + (x + y')''))')' = x. [para(23(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #582 (T,wt=17): 14890 (g(x) + (x + (g(x) + (x + h(x)'')''))')' = x. [para(14627(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),19(10),14627(21)])]. given #583 (T,wt=17): 14900 (g(x) + (x + (x + (g(x) + h(x)''))'')')' = x. [para(14627(a,1),54(a,1,1,2,1,1)),rewrite([19(7),14627(21)])]. given #584 (T,wt=17): 16391 (h(x)' + (x + (x + (x + (g(x) + x'))))')' = h(x). [para(15004(a,1),50(a,1,1,1)),rewrite([16389(7),7(7),7(6),16389(16),12(15)])]. given #585 (T,wt=17): 16593 (h(x)' + (g(x) + (x + (x + (x + x)))')')' = g(x). [para(16397(a,1),7261(a,1,1,1))]. given #586 (A,wt=25): 235 (x + ((x + (y + y'))' + (x + g(y))'')')' = (x + (y + y'))'. [para(10(a,1),23(a,1,1,2,1,2,1,1,2))]. given #587 (T,wt=17): 16595 (h(x)' + (x + (x + (x + (g(x) + g(x)'))))')' = h(x). [para(16498(a,1),20(a,1,1,1)),rewrite([29(6)])]. given #588 (T,wt=17): 16716 (g(x) + (x + (g(x) + (x + (x + h(x)))''))')' = x. [para(16497(a,1),25(a,1,1,2,1,2,2)),rewrite([6(8),19(9),16497(19)])]. given #589 (T,wt=17): 16819 x + (x + (g(x) + (g(x) + y))) = x + (x + (g(x) + y)). [para(16389(a,1),7(a,1,1)),rewrite([7(4),7(3),7(9),7(8)]),flip(a)]. given #590 (T,wt=17): 16820 x + (g(x) + (g(x) + (y + x))) = y + (x + (x + g(x))). [para(16389(a,1),7(a,2,2)),rewrite([19(6),19(5),6(4)])]. given #591 (A,wt=26): 236 (x + ((y + (x + z))' + (x + (y + z)')'')')' = (x + (y + z))'. [para(19(a,1),23(a,1,1,2,1,1,1))]. given #592 (T,wt=17): 16822 x + (y + (x + (g(x) + g(x)))) = y + (x + (x + g(x))). [para(16389(a,1),19(a,1,2)),flip(a)]. given #593 (T,wt=17): 16880 (x + (x + (x + (x + (g(x) + h(x)''))))')' = g(x). [back_rewrite(16552),rewrite([16819(11),16819(9)])]. given #594 (T,wt=17): 16886 (h(x)' + (x + (x + (x + (g(x) + h(x)'))))')' = h(x). [back_rewrite(16393),rewrite([16819(10)])]. given #595 (T,wt=17): 16888 (g(x) + (x + (x + (x + (g(x) + h(x)''))))')' = x. [back_rewrite(16355),rewrite([16819(10)])]. given #596 (A,wt=29): 237 (x + ((x + (g(y) + (y + y)'))' + (x + y)'')')' = (x + (g(y) + (y + y)'))'. [para(28(a,1),23(a,1,1,2,1,2,1,1,2))]. given #597 (T,wt=17): 16961 (x + (x + (x + (x + (g(x) + x''))))')' = g(x). [back_rewrite(7660),rewrite([16819(10),16819(8)])]. given #598 (T,wt=17): 16963 (x + (x + (x + (g(x) + (x + x)'')))')' = g(x). [back_rewrite(7656),rewrite([16819(11),16819(9)])]. given #599 (T,wt=17): 17010 (g(x) + (x + (x + (x + (g(x) + x''))))')' = x. [back_rewrite(4386),rewrite([16819(9)])]. given #600 (T,wt=17): 17014 (g(x) + (x + (x + (g(x) + (x + x)'')))')' = x. [back_rewrite(4354),rewrite([16819(10)])]. given #601 (A,wt=25): 238 (x + ((x + (g(y) + h(y)'))' + (x + y)'')')' = (x + (g(y) + h(y)'))'. [para(37(a,1),23(a,1,1,2,1,2,1,1,2))]. given #602 (T,wt=17): 17056 ((x + h(y))' + (x + (g(y) + h(y)'))')' = x + g(y). [para(16824(a,1),22(a,1,1,1,1,2))]. given #603 (T,wt=17): 17063 ((x + h(y))' + (h(y)' + (x + g(y)))')' = x + g(y). [para(16824(a,1),90(a,1,1,1,1,2))]. given #604 (T,wt=17): 17066 ((x + h(y))' + (g(y) + (h(y)' + x))')' = x + g(y). [para(16824(a,1),145(a,1,1,1,1,2))]. given #605 (T,wt=17): 17068 ((x + h(y))' + (g(y) + (x + h(y)'))')' = g(y) + x. [para(16824(a,1),155(a,1,1,1,1,2))]. given #606 (A,wt=28): 241 ((x + (((x + y)' + (x + y')'')' + z))' + (z + (x + y)')')' = z. [para(23(a,1),20(a,1,1,2,1,2)),rewrite([7(10)])]. given #607 (T,wt=17): 17069 ((x + h(y))' + (g(y)' + (x + h(y)))')' = x + h(y). [para(16824(a,1),204(a,1,1,1,1,2))]. given #608 (T,wt=17): 17070 ((h(x)' + (y + g(x)))' + (y + h(x))')' = y + g(x). [para(16824(a,1),318(a,1,1,2,1,2))]. given #609 (T,wt=17): 17085 ((g(x) + (h(x)' + y))' + (y + h(x))')' = y + g(x). [para(16824(a,1),9479(a,1,1,2,1,2))]. given #610 (T,wt=17): 17158 (x + (x + (g(x) + (x + (x + h(x)))''))')' = g(x). [para(16899(a,1),25(a,1,1,2,1,2,2)),rewrite([6(7),16899(17)])]. given #611 (A,wt=24): 242 ((x + y)' + (y + ((x + y)' + (y + x')'')'')')' = y. [para(20(a,1),23(a,1,1,2,1,1)),rewrite([20(22)])]. given #612 (T,wt=17): 17168 (x + (g(x) + (x + (x + (x + h(x))))'')')' = g(x). [para(16899(a,1),54(a,1,1,2,1,1)),rewrite([16899(17)])]. given #613 (T,wt=17): 17275 (g(x) + (x + (x + (x + (x + h(x))))'')')' = x. [para(16894(a,1),54(a,1,1,2,1,1)),rewrite([19(7),19(6),19(5),16824(4),16894(19)])]. given #614 (T,wt=17): 17343 g(x) + (y + (z + (u + h(x)))) = y + (z + (u + h(x))). [para(7(a,1),17089(a,1,2,2)),rewrite([7(9)])]. given #615 (T,wt=17): 17810 x + (x + (g(x) + (y + g(x)))) = x + (x + (y + g(x))). [para(17055(a,2),100(a,1,1,2,1)),rewrite([19(11),7(10),7(9),7(8),7(7),19(11),19(10),16819(11),6(14),818(15)]),flip(a)]. given #616 (A,wt=24): 245 (x + (g(x)' + (x + (g(x) + h(x)''))')')' = (x + (g(x) + h(x)''))'. [para(38(a,1),23(a,1,1,2,1,2,1)),rewrite([6(10)])]. given #617 (T,wt=17): 17960 (g(x) + (x + (x + (x + (x + (x + h(x))))))')' = x. [para(17287(a,1),95(a,1,1,2,1,2,2)),rewrite([6(8),19(9),19(8),19(7),19(6),19(5),16824(4),17287(19)])]. given #618 (T,wt=17): 17981 (x + (x + (x + (x + (x + (x + h(x))))))')' = g(x). [para(17460(a,1),95(a,1,1,2,1,2,2)),rewrite([6(7),19(7),19(6),19(5),19(4),16824(3),17460(17)])]. given #619 (T,wt=17): 18394 x + (g(x) + (g(x) + (y + x))) = x + (x + (g(x) + y)). [para(16820(a,2),6(a,1)),rewrite([7(10),7(9)])]. given #620 (T,wt=17): 18502 x + (x + (y + (g(x) + g(x)))) = y + (x + (x + g(x))). [para(19(a,1),16822(a,1,2))]. given #621 (A,wt=21): 248 (g(x) + (x' + (g(x) + (x' + x')'')'')')' = x'. [para(56(a,1),23(a,1,1,2,1,1)),rewrite([56(22)])]. given #622 (T,wt=17): 18875 x + (g(x) + (y + (x + g(x)))) = x + (x + (g(x) + y)). [para(19(a,1),18394(a,1,2,2)),rewrite([6(3)])]. given #623 (T,wt=18): 14686 (g(x) + (g(x) + (h(x)' + (x + x'')'))')' = h(x)'. [para(14619(a,1),102(a,1,1,2)),rewrite([19(9),6(12)])]. given #624 (T,wt=18): 15045 (x + (g(x) + (x + (g(x) + (h(x)' + h(x)')))'))' = h(x)'. [para(14993(a,1),149(a,1,1,2,2,1,2,2,2)),rewrite([14993(18)])]. given #625 (T,wt=18): 15366 (x + (h(x)' + (x + (x + g(x))')'')')' = h(x)'. [para(14755(a,1),8(a,1,1,1))]. given #626 (A,wt=25): 249 (g(x) + (x'' + (g(x) + (x' + x'))')')' = (g(x) + (x' + x'))'. [para(56(a,1),23(a,1,1,2,1,2,1)),rewrite([6(10)])]. given #627 (T,wt=18): 15396 (h(x)' + (x + (x + (h(x)' + (x + g(x))')))')' = x. [para(14755(a,1),95(a,1,1,2,1,2,2)),rewrite([6(9),19(10),19(9),14755(22)])]. given #628 (T,wt=18): 15539 (h(x)' + (g(x) + (g(x) + (h(x)' + h(x)'))'')')' = g(x). [para(14647(a,1),8(a,1,1,1))]. given #629 (T,wt=18): 15777 (x + (x + (h(x)' + (x + x)'))')' = (x + x)'. [para(28(a,1),14632(a,1,1,2)),rewrite([6(6),7(6),6(8)])]. given #630 (T,wt=18): 15812 (h(x)' + (x + (x + (h(x)' + h(x)'))'')')' = x. [para(15778(a,1),8(a,1,1,1))]. given #631 (A,wt=28): 250 ((x + (y + ((y + z)' + (y + z')'')'))' + ((y + z)' + x)')' = x. [para(23(a,1),21(a,1,1,2,1,1))]. given #632 (T,wt=18): 16538 (h(x)' + (g(x) + (g(x) + (h(x)' + (x + x)')))')' = g(x). [back_rewrite(14438),rewrite([16498(4),16498(10),6(9)])]. given #633 (T,wt=18): 16950 (x + (x + (x + (g(x) + (g(x)' + h(x)')')))')' = g(x). [back_rewrite(9864),rewrite([16819(12)])]. given #634 (T,wt=18): 16953 (x + (x + (x + (g(x) + (x' + x')')))')' = g(x). [back_rewrite(8480),rewrite([16819(12),16819(10)])]. given #635 (T,wt=18): 16959 (g(x) + (x + (x + (g(x) + (x' + x')')))')' = x. [back_rewrite(7678),rewrite([16819(11)])]. given #636 (A,wt=24): 251 ((x + y)' + (x + ((x + y)' + (y' + x)'')'')')' = x. [para(21(a,1),23(a,1,1,2,1,1)),rewrite([21(22)])]. given #637 (T,wt=18): 17987 (g(x) + (g(x) + (g(x) + (g(x) + (h(x)' + h(x)')))'))' = h(x)'. [para(17934(a,1),8(a,1,1,2)),rewrite([19(9),19(8),6(14),7(14)])]. given #638 (T,wt=18): 18073 (x + (x + (g(x) + (g(x)' + (x + x)')'))')' = g(x). [para(28(a,1),233(a,1,1,1)),rewrite([10(6),6(6),19(9)])]. given #639 (T,wt=18): 18104 (g(x) + (x + (g(x) + (g(x) + (x' + h(x)')')))')' = x. [para(14750(a,1),8(a,1,1,2)),rewrite([6(13)])]. given #640 (T,wt=18): 19103 (g(x) + (x + (x + (g(x) + (x' + h(x)')')))')' = x. [para(18104(a,1),95(a,1,1,2,1,2,2)),rewrite([6(13),16819(13),19(12),19(11),16819(12),18104(27)])]. given #641 (A,wt=21): 252 (x + (h(x)' + (x + (g(x)' + h(x)')'')'')')' = h(x)'. [para(62(a,1),23(a,1,1,2,1,1)),rewrite([62(24)])]. given #642 (T,wt=18): 19108 (x + (x + (x + (g(x) + (x' + h(x)')')))')' = g(x). [para(19103(a,1),8(a,1,1,2)),rewrite([19(11),19(10),16819(11),6(11)])]. given #643 (T,wt=19): 14641 ((x + y)' + (x + (g(y) + (y + h(y)'')'))')' = x. [para(14619(a,1),24(a,1,1,2,1,2,1))]. given #644 (T,wt=19): 14661 ((g(x) + ((x + h(x)'')' + y))' + (y + x)')' = y. [para(14619(a,1),55(a,1,1,1,1,1))]. given #645 (T,wt=19): 14678 ((x + (g(y) + (y + h(y)'')'))' + (y + x)')' = x. [para(14619(a,1),94(a,1,1,1,1,2,1))]. given #646 (A,wt=25): 253 (x + (h(x)'' + (x + (g(x)' + h(x)'))')')' = (x + (g(x)' + h(x)'))'. [para(62(a,1),23(a,1,1,2,1,2,1)),rewrite([6(11)])]. given #647 (T,wt=18): 19167 (g(x) + (g(x) + (x' + (x + h(x)'')'))')' = x'. [para(10(a,1),14678(a,1,1,2)),rewrite([19(9),6(12)])]. given #648 (T,wt=18): 19188 (g(x) + (g(x) + (h(x)' + (x + h(x)'')'))')' = h(x)'. [para(14619(a,1),14678(a,1,1,2)),rewrite([19(10),6(13)])]. given #649 (T,wt=19): 14881 ((x + y)' + (g(x) + ((x + h(x)'')' + y))')' = y. [para(14627(a,1),47(a,1,1,2,1,1)),rewrite([7(8),6(12)])]. given #650 (T,wt=19): 14882 (g(x) + (x + (g(x) + (x + h(x)'')'')'')')' = x. [para(14627(a,1),23(a,1,1,2,1,1)),rewrite([14627(23)])]. given #651 (A,wt=26): 254 (x + ((y + (y + (g(y) + (x + y))))' + (x + h(y)')'')')' = (x + h(y))'. [para(30(a,1),23(a,1,1,2,1,1,1))]. given #652 (T,wt=19): 14884 ((x + y)' + (g(y) + ((y + h(y)'')' + x))')' = x. [para(14627(a,1),48(a,1,1,1,1,2)),rewrite([7(10)])]. given #653 (T,wt=19): 14885 ((x + y)' + (y + (g(x) + (x + h(x)'')'))')' = y. [para(14627(a,1),89(a,1,1,1,1,1))]. given #654 (T,wt=19): 14891 ((x + y)' + (g(y) + (x + (y + h(y)'')'))')' = x. [para(14627(a,1),32(a,1,1,2,1,2)),rewrite([6(12)])]. given #655 (T,wt=19): 14902 ((x + y)' + (g(x) + (y + (x + h(x)'')'))')' = y. [para(14627(a,1),97(a,1,1,2,1,1)),rewrite([6(12)])]. given #656 (A,wt=26): 256 (x + ((y + h(x))' + (x + (y + (x + (x + g(x))))')'')')' = (y + h(x))'. [para(33(a,1),23(a,1,1,2,1,1,1)),rewrite([33(20)])]. given #657 (T,wt=19): 14911 ((x + y)' + ((y + h(y)'')' + (x + g(y)))')' = x. [para(14627(a,1),597(a,1,1,2,1,2)),rewrite([6(12)])]. given #658 (T,wt=19): 14912 ((x + y)' + ((x + h(x)'')' + (y + g(x)))')' = y. [para(14627(a,1),1701(a,1,1,2,1,1)),rewrite([6(12)])]. given #659 (T,wt=19): 14973 (x + (x + (g(x) + (g(x) + (x + h(x)'')'')))')' = g(x). [para(14627(a,1),500(a,1,1,1)),rewrite([14627(16),6(9),19(10),19(11)])]. given #660 (T,wt=19): 15015 (h(x)' + (x + (x + (x + (g(x) + (x + g(x))'))))')' = h(x). [para(14993(a,1),49(a,1,1,1)),rewrite([29(7)])]. given #661 (A,wt=21): 257 (x + (g(x) + (x + (g(x) + (x + x)'')'')'')')' = g(x). [para(34(a,1),23(a,1,1,2,1,1)),rewrite([34(23)])]. given #662 (T,wt=19): 15127 (g(x) + (g(x) + (h(x)' + (x' + h(x)')''))')' = h(x)'. [para(14630(a,1),25(a,1,1,2,1,2,2)),rewrite([6(11),14630(23)])]. given #663 (T,wt=19): 15135 (g(x) + (h(x)' + (g(x) + (x' + h(x)'))'')')' = h(x)'. [para(14630(a,1),54(a,1,1,2,1,1)),rewrite([14630(23)])]. given #664 (T,wt=19): 15217 (x + (x + (g(x) + (x + (g(x) + h(x)''))''))')' = g(x). [para(14645(a,1),25(a,1,1,2,1,2,2)),rewrite([6(10),14645(23)])]. given #665 (T,wt=19): 15224 (x + (g(x) + (x + (x + (g(x) + h(x)'')))'')')' = g(x). [para(14645(a,1),54(a,1,1,2,1,1)),rewrite([14645(23)])]. given #666 (A,wt=28): 258 (x + (g(x)' + (x + (g(x) + (x + x)''))')')' = (x + (g(x) + (x + x)''))'. [para(34(a,1),23(a,1,1,2,1,2,1)),rewrite([6(10)])]. given #667 (T,wt=19): 15569 (g(x) + (g(x) + (g(x) + (h(x)' + (h(x)' + h(x)'))))')' = h(x)'. [para(14647(a,1),95(a,1,1,2,1,2,2)),rewrite([6(12),19(12),14647(27)])]. given #668 (T,wt=19): 15633 (h(x)' + (g(x) + (g(x) + (x' + (h(x)' + h(x)'))))')' = g(x). [para(14655(a,1),95(a,1,1,2,1,2,2)),rewrite([6(12),19(13),19(12),19(11),14655(27)])]. given #669 (T,wt=19): 15842 (x + (x + (x + (h(x)' + (h(x)' + h(x)'))))')' = h(x)'. [para(15778(a,1),95(a,1,1,2,1,2,2)),rewrite([6(9),19(9),15778(22)])]. given #670 (T,wt=19): 16415 (h(x)' + (x + (x + (x + (x + g(x)))'))')' = x + x. [para(15004(a,1),90(a,1,1,1)),rewrite([16389(7),6(8),7(8)])]. given #671 (A,wt=21): 261 (x + (g(x) + (x + (x + (g(x) + x''))'')'')')' = g(x). [para(46(a,1),23(a,1,1,2,1,1)),rewrite([46(23)])]. given #672 (T,wt=19): 16491 (h(x)' + (x + ((y + h(x))' + (y' + h(x))'))')' = x. [para(15004(a,1),200(a,1,1,1)),rewrite([16389(7),12(6),16389(11),12(10)])]. given #673 (T,wt=19): 16606 (h(x)' + (x + (x + (x + (x + (g(x) + x')))))')' = h(x). [para(16498(a,1),96(a,1,1,2)),rewrite([19(4),29(3),6(11)])]. given #674 (T,wt=19): 16665 (h(x)' + (x + (g(x) + (x + (x + g(x)))'))')' = x + g(x). [para(16498(a,1),152(a,1,1,1)),rewrite([19(9),6(14)])]. given #675 (T,wt=19): 16675 (h(x)' + (x + (x + (x + (g(x) + g(x)))'))')' = x + x. [para(16498(a,1),173(a,1,1,1)),rewrite([6(5),19(6)])]. given #676 (A,wt=28): 262 (x + (g(x)' + (x + (x + (g(x) + x'')))')')' = (x + (x + (g(x) + x'')))'. [para(46(a,1),23(a,1,1,2,1,2,1)),rewrite([6(10)])]. given #677 (T,wt=19): 16695 (h(x)' + (g(x) + ((y + h(x))' + (y' + h(x))'))')' = g(x). [para(16498(a,1),200(a,1,1,1))]. given #678 (T,wt=19): 16697 (h(x)' + (x + (x + (x + (x + (g(x) + h(x)')))))')' = h(x). [para(16498(a,1),14632(a,1,1,2)),rewrite([19(5),29(4),6(12)])]. given #679 (T,wt=19): 16701 ((x + y)' + (x + (g(y) + (y + (y + h(y)))'))')' = x. [para(16497(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #680 (T,wt=19): 16704 ((g(x) + ((x + (x + h(x)))' + y))' + (y + x)')' = y. [para(16497(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #681 (A,wt=28): 263 (((x + y)' + z)' + (x + (((x + y)' + (x + y')'')' + z))')' = z. [para(23(a,1),47(a,1,1,2,1,1)),rewrite([7(10),6(16)])]. given #682 (T,wt=19): 16705 ((x + (g(y) + (y + (y + h(y)))'))' + (y + x)')' = x. [para(16497(a,1),21(a,1,1,2,1,1))]. given #683 (T,wt=9): 19643 (x + (x + h(x)))' = h(x)'. [para(14619(a,1),16705(a,1,1,2)),rewrite([19(9),6(12),17160(13)])]. given #684 (T,wt=5): 19645 x + h(x) = h(x). [para(19643(a,1),20(a,1,1,1)),rewrite([7(6),29(5),16606(12)]),flip(a)]. given #685 (T,wt=7): 19724 x + (x + g(x)) = h(x). [back_rewrite(16882),rewrite([19674(12),19674(12),19674(12),19715(12),17024(11)])]. given #686 (A,wt=24): 264 ((x + y)' + (y + ((x + y)' + (x' + y)'')'')')' = y. [para(47(a,1),23(a,1,1,2,1,1)),rewrite([47(22)])]. given #687 (T,wt=5): 20114 x + g(x) = h(x). [back_rewrite(19718),rewrite([20001(12),17527(14)])]. ============================== PROOF ================================= % Proof 3 at 43.29 (+ 0.15) seconds: Winker1a. % Length of proof is 93. % Level of proof is 23. % Maximum clause weight is 30. % Given clauses 687. 2 (exists a exists b a + b = a) # answer(Winker1a) # label(non_clause) # label(goal). [goal]. 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]. 9 g(x) = (x + x')' # label(definition_g). [assumption]. 10 (x + x')' = g(x). [copy(9),flip(a)]. 11 h(x) = x + (x + (x + g(x))) # label(definition_h). [assumption]. 12 x + (x + (x + g(x))) = h(x). [copy(11),flip(a)]. 14 x + y != x # answer(Winker1a). [deny(2)]. 19 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),rewrite([7(2)])]. 20 ((x + y)' + (y + x')')' = y. [para(6(a,1),8(a,1,1,1,1))]. 21 ((x + y)' + (y' + x)')' = x. [para(6(a,1),8(a,1,1,2,1))]. 22 ((x + (y + z))' + (x + (y + z'))')' = x + y. [para(7(a,1),8(a,1,1,1,1)),rewrite([7(6)])]. 23 (x + ((x + y)' + (x + y')'')')' = (x + y)'. [para(8(a,1),8(a,1,1,1))]. 28 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. 29 h(x) + y = x + (x + (x + (g(x) + y))). [para(12(a,1),7(a,1,1)),rewrite([7(6),7(5)])]. 30 x + h(y) = y + (y + (g(y) + (x + y))). [para(12(a,1),7(a,2,2)),rewrite([19(5),19(4),6(3)]),flip(a)]. 31 (h(x)' + (x + (x + (x + g(x)))')')' = x. [para(12(a,1),8(a,1,1,1,1))]. 32 ((x + (y + z))' + (y + (x + z)')')' = y. [para(19(a,1),8(a,1,1,1,1))]. 36 (x + (x + (x + g(x)))')' = g(x). [para(28(a,1),8(a,1,1,2)),rewrite([19(3),6(2),6(5)])]. 37 (g(x) + h(x)')' = x. [back_rewrite(31),rewrite([36(8),6(4)])]. 39 ((x + y)' + (x + (g(y) + h(y)'))')' = x. [para(37(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. 40 (x + (g(x) + h(x))')' = g(x). [para(37(a,1),8(a,1,1,2)),rewrite([6(5)])]. 43 (g(x) + (x + (g(x) + h(x)))')' = x. [para(40(a,1),8(a,1,1,2)),rewrite([6(7)])]. 49 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),20(a,1,1,1,1))]. 53 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(20(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 58 (h(x)' + (x + (x + (g(x) + x')))')' = x + (x + g(x)). [para(12(a,1),20(a,1,1,1,1)),rewrite([7(7),7(6)])]. 89 ((x' + y)' + (y + x)')' = y. [para(6(a,1),21(a,1,1))]. 95 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 96 ((x + (y + y'))' + (g(y) + x)')' = x. [para(10(a,1),21(a,1,1,2,1,1))]. 99 ((x + (g(y) + (y + y)'))' + (y + x)')' = x. [para(28(a,1),21(a,1,1,2,1,1))]. 100 ((x + (g(y) + h(y)'))' + (y + x)')' = x. [para(37(a,1),21(a,1,1,2,1,1))]. 109 ((x + (g(y) + (y + (g(y) + h(y)))'))' + (y + x)')' = x. [para(43(a,1),21(a,1,1,2,1,1))]. 119 x + h(y) = y + (y + (y + (g(y) + x))). [para(29(a,1),6(a,1)),flip(a)]. 121 ((x + (x + (x + (g(x) + y))))' + (y + h(x)')')' = y. [para(29(a,1),20(a,1,1,1,1))]. 325 ((x + y)' + (y + (g(x) + h(x)'))')' = y. [para(37(a,1),89(a,1,1,1,1,1))]. 429 x + h(y) = y + (y + (y + (x + g(y)))). [para(6(a,1),119(a,2,2,2,2))]. 435 x + (y + h(z)) = z + (x + (z + (z + (g(z) + y)))). [para(119(a,2),19(a,1,2))]. 436 x + (y + h(z)) = z + (z + (z + (x + (g(z) + y)))). [para(19(a,1),119(a,2,2,2,2)),rewrite([7(3)])]. 462 x + (y + h(z)) = z + (z + (x + (z + (y + g(z))))). [para(429(a,2),7(a,2,2)),rewrite([19(6),19(5),7(4)]),flip(a)]. 572 (x + (x + (g(y) + (h(y)' + (x + y)')))')' = (x + y)'. [para(39(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. 795 (h(x)' + (x + (x + (g(x) + (g(x) + h(x)'))))')' = x + (x + g(x)). [para(12(a,1),100(a,1,1,2,1)),rewrite([19(8),7(7),7(6),19(8),19(7),6(12)])]. 1000 (h(x)' + (x + (g(x) + (x + x)'))')' = x + g(x). [para(12(a,1),49(a,1,1,1,1)),rewrite([7(7)])]. 1463 ((x + y)' + (y + (y + (x' + (x + y)')))')' = y. [para(53(a,1),8(a,1,1,2)),rewrite([6(10)])]. 1477 (x + (x + (x + (g(x) + (x + (x + (x + (g(x) + (y' + (y + h(x))')))))'))))' = (y + h(x))'. [para(29(a,1),53(a,1,1,2,1)),rewrite([29(13)])]. 1812 (h(x)' + (x + (x + (g(x) + (g(x) + (x + x)'))))')' = x + (x + g(x)). [para(12(a,1),99(a,1,1,2,1)),rewrite([19(8),7(7),7(6),19(8),19(7),6(12)])]. 1814 (g(x) + (g(x) + ((x + x)' + (g(x) + h(x))'))')' = (g(x) + h(x))'. [para(40(a,1),99(a,1,1,2)),rewrite([6(9),7(9),6(12)])]. 3554 x + (y + (g(x) + (z + h(x)))) = y + (x + (x + (x + (x + (g(x) + (z + g(x))))))). [para(462(a,2),435(a,2,2,2)),rewrite([6(5),19(5),29(4)]),flip(a)]. 4470 (x + (g(x) + (x + (g(x) + (h(x)' + (x + x)')))'))' = h(x)'. [para(1000(a,1),8(a,1,1,2)),rewrite([19(8),19(7),6(12),7(12)])]. 7586 (h(x)' + (x + (x + (x + (x + (g(x) + (g(x) + (x' + h(x)')))))))')' = x + (x + g(x)). [para(58(a,1),95(a,1,1,2,1,2,2)),rewrite([6(13),19(13),19(12),19(11),7(10),7(9),19(11),19(10),6(14),7(14),7(13),7(12),7(11),7(10),7(9),58(27)])]. 14441 (g(x) + (g(x) + ((x + x)' + (x + (x + (x + (g(x) + g(x)))))'))')' = (g(x) + h(x))'. [para(30(a,1),1814(a,1,1,2,1,2,2,1)),rewrite([6(7),19(8)])]. 14619 (x + h(x)')' = g(x). [para(4470(a,1),32(a,1,1,1)),rewrite([572(14),28(7),6(3)])]. 14629 (g(x) + (x + h(x))')' = x. [para(14619(a,1),8(a,1,1,2)),rewrite([6(5)])]. 14660 (g(x) + (g(x) + (h(x)' + (x + x)'))')' = h(x)'. [para(14619(a,1),99(a,1,1,2)),rewrite([19(7),6(10)])]. 14683 (x + (x + (g(x) + h(x)))')' = g(x). [para(14619(a,1),95(a,1,1,2,1,2,2)),rewrite([6(3),14619(11)])]. 14690 (g(x) + (g(x) + (h(x)' + (x + (g(x) + h(x)))'))')' = h(x)'. [para(14619(a,1),109(a,1,1,2)),rewrite([19(10),6(13)])]. 14817 (g(x) + (x + (x + (g(x) + h(x))))')' = x. [para(14629(a,1),95(a,1,1,2,1,2,2)),rewrite([6(5),19(6),19(5),14629(15)])]. 14993 (x + (g(x) + h(x)))' = h(x)'. [para(14683(a,1),100(a,1,1,2)),rewrite([6(10),7(10),6(13),14690(14)]),flip(a)]. 14997 (x + (x + (x + (x + (x + (x + (g(x) + (g(x) + g(x))))))))')' = g(x). [para(14683(a,1),95(a,1,1,2,1,2,2)),rewrite([6(6),19(6),3554(7),14993(18),14619(17)])]. 15004 (x + (x + (x + (x + (g(x) + g(x))))))' = h(x)'. [para(30(a,1),14993(a,1,1,2)),rewrite([6(3),19(4)])]. 15005 (h(x)' + (x + (g(x) + h(x)'))')' = x + g(x). [para(14993(a,1),22(a,1,1,1))]. 15465 (g(x) + (x + (x + (x + (x + (x + (g(x) + g(x)))))))')' = x. [para(30(a,1),14817(a,1,1,2,1,2,2)),rewrite([6(4),19(5)])]. 16389 x + (x + (g(x) + g(x))) = x + (x + g(x)). [para(15004(a,1),49(a,1,1,1)),rewrite([7(10),7(9),7(8),1812(13)]),flip(a)]. 16393 (h(x)' + (x + (x + (x + (g(x) + (g(x) + h(x)')))))')' = h(x). [para(15004(a,1),325(a,1,1,1)),rewrite([16389(7),12(6),19(8),29(7),19(11),19(10),19(9),16389(19),12(18)])]. 16397 (x + h(x))' = h(x)'. [para(15004(a,1),53(a,2)),rewrite([16389(5),12(4),16389(6),12(5),16389(8),12(7),29(8),29(13),1477(17)])]. 16490 (h(x)' + (x + (x + (x + (x + (x + (x + (g(x) + (g(x) + (x' + h(x)')))))))))')' = h(x). [para(15004(a,1),1463(a,1,1,1)),rewrite([16389(7),12(6),16389(8),12(7),16389(10),12(9),16397(8),29(9),19(13),19(12),19(11),19(10),29(9),19(13),19(12),19(11),16389(24),12(23)])]. 16497 (g(x) + (x + (x + h(x)))')' = x. [back_rewrite(15465),rewrite([16389(6),12(5)])]. 16498 (g(x) + h(x))' = h(x)'. [back_rewrite(14441),rewrite([16389(9),12(8),6(7),14660(11)]),flip(a)]. 16606 (h(x)' + (x + (x + (x + (x + (g(x) + x')))))')' = h(x). [para(16498(a,1),96(a,1,1,2)),rewrite([19(4),29(3),6(11)])]. 16705 ((x + (g(y) + (y + (y + h(y)))'))' + (y + x)')' = x. [para(16497(a,1),21(a,1,1,2,1,1))]. 16819 x + (x + (g(x) + (g(x) + y))) = x + (x + (g(x) + y)). [para(16389(a,1),7(a,1,1)),rewrite([7(4),7(3),7(9),7(8)]),flip(a)]. 16824 g(x) + h(x) = h(x). [para(16389(a,1),29(a,2,2)),rewrite([6(3),12(7)])]. 16882 (h(x)' + (x + (x + (x + (x + (x + (x + (g(x) + (x' + h(x)'))))))))')' = h(x). [back_rewrite(16490),rewrite([16819(12)])]. 16886 (h(x)' + (x + (x + (x + (g(x) + h(x)'))))')' = h(x). [back_rewrite(16393),rewrite([16819(10)])]. 16899 (x + (x + (x + h(x)))')' = g(x). [back_rewrite(14997),rewrite([16819(7),16389(5),12(4)])]. 16967 (h(x)' + (x + (x + (x + (x + (g(x) + (x' + h(x)'))))))')' = x + (x + g(x)). [back_rewrite(7586),rewrite([16819(12)])]. 17024 (h(x)' + (x + (x + (g(x) + h(x)')))')' = x + (x + g(x)). [back_rewrite(795),rewrite([16819(10)])]. 17060 x + (x + (x + (y + (g(x) + g(x))))) = y + h(x). [para(16824(a,1),436(a,1,2)),flip(a)]. 17160 (g(x) + (g(x) + (h(x)' + (x + (x + h(x)))'))')' = (x + (x + h(x)))'. [para(16899(a,1),100(a,1,1,2)),rewrite([6(9),7(9),6(12)])]. 17527 (h(x)' + (x + (x + (g(x) + (h(x)' + h(x)'))))')' = x + g(x). [para(15005(a,1),95(a,1,1,2,1,2,2)),rewrite([6(12),19(12),19(11),7(10),19(11),16819(12),19(11),19(10),19(9),15005(24)])]. 17934 (h(x)' + (g(x) + (g(x) + h(x)'))')' = g(x) + g(x). [para(17060(a,1),121(a,1,1,1,1)),rewrite([16824(3),7(8)])]. 18543 (h(x)' + (x + (x + (x + (x + (x + (x + (g(x) + (h(x)' + h(x)'))))))))')' = h(x). [para(16886(a,1),95(a,1,1,2,1,2,2)),rewrite([6(13),19(13),19(12),19(11),19(10),29(9),19(13),19(12),19(11),16819(12),19(15),19(14),19(13),19(12),19(11),19(10),19(9),16886(30)])]. 19505 (x + (x + (x + (x + (g(x) + (x' + h(x)'))))))' = (x + (x + (g(x) + h(x)')))'. [para(16606(a,1),23(a,1,1,2,1,2,1)),rewrite([6(12),7(12),7(11),7(10),7(9),7(8),6(16),16967(17),6(6),7(6),7(5),6(17),7(17),7(16),7(15),7(14),7(13)]),flip(a)]. 19643 (x + (x + h(x)))' = h(x)'. [para(14619(a,1),16705(a,1,1,2)),rewrite([19(9),6(12),17160(13)])]. 19645 x + h(x) = h(x). [para(19643(a,1),20(a,1,1,1)),rewrite([7(6),29(5),16606(12)]),flip(a)]. 19674 x + (x + (x + (x + (g(x) + y)))) = x + (x + (x + (g(x) + y))). [para(19645(a,1),7(a,1,1)),rewrite([29(2),29(7)]),flip(a)]. 19715 (x + (x + (x + (g(x) + (x' + h(x)')))))' = (x + (x + (g(x) + h(x)')))'. [back_rewrite(19505),rewrite([19674(10)])]. 19718 (h(x)' + (x + (x + (x + (g(x) + (h(x)' + h(x)')))))')' = h(x). [back_rewrite(18543),rewrite([19674(13),19674(13),19674(13)])]. 19724 x + (x + g(x)) = h(x). [back_rewrite(16882),rewrite([19674(12),19674(12),19674(12),19715(12),17024(11)])]. 20001 x + (x + (x + (g(x) + y))) = x + (x + (g(x) + y)). [para(19724(a,1),7(a,1,1)),rewrite([29(2),7(8)])]. 20114 x + g(x) = h(x). [back_rewrite(19718),rewrite([20001(12),17527(14)])]. 21891 g(x) + g(x) = g(x). [para(20114(a,1),100(a,1,1,2,1)),rewrite([6(10),17934(11)])]. 21892 $F # answer(Winker1a). [resolve(21891,a,14,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 4 at 43.29 (+ 0.15) seconds: Winker2a. % Length of proof is 91. % Level of proof is 24. % Maximum clause weight is 30. % Given clauses 687. 4 (exists a exists b (a + b)' = a') # answer(Winker2a) # label(non_clause) # label(goal). [goal]. 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]. 9 g(x) = (x + x')' # label(definition_g). [assumption]. 10 (x + x')' = g(x). [copy(9),flip(a)]. 11 h(x) = x + (x + (x + g(x))) # label(definition_h). [assumption]. 12 x + (x + (x + g(x))) = h(x). [copy(11),flip(a)]. 16 (x + y)' != x' # answer(Winker2a). [deny(4)]. 19 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),rewrite([7(2)])]. 20 ((x + y)' + (y + x')')' = y. [para(6(a,1),8(a,1,1,1,1))]. 21 ((x + y)' + (y' + x)')' = x. [para(6(a,1),8(a,1,1,2,1))]. 22 ((x + (y + z))' + (x + (y + z'))')' = x + y. [para(7(a,1),8(a,1,1,1,1)),rewrite([7(6)])]. 23 (x + ((x + y)' + (x + y')'')')' = (x + y)'. [para(8(a,1),8(a,1,1,1))]. 28 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. 29 h(x) + y = x + (x + (x + (g(x) + y))). [para(12(a,1),7(a,1,1)),rewrite([7(6),7(5)])]. 30 x + h(y) = y + (y + (g(y) + (x + y))). [para(12(a,1),7(a,2,2)),rewrite([19(5),19(4),6(3)]),flip(a)]. 31 (h(x)' + (x + (x + (x + g(x)))')')' = x. [para(12(a,1),8(a,1,1,1,1))]. 32 ((x + (y + z))' + (y + (x + z)')')' = y. [para(19(a,1),8(a,1,1,1,1))]. 36 (x + (x + (x + g(x)))')' = g(x). [para(28(a,1),8(a,1,1,2)),rewrite([19(3),6(2),6(5)])]. 37 (g(x) + h(x)')' = x. [back_rewrite(31),rewrite([36(8),6(4)])]. 39 ((x + y)' + (x + (g(y) + h(y)'))')' = x. [para(37(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. 40 (x + (g(x) + h(x))')' = g(x). [para(37(a,1),8(a,1,1,2)),rewrite([6(5)])]. 43 (g(x) + (x + (g(x) + h(x)))')' = x. [para(40(a,1),8(a,1,1,2)),rewrite([6(7)])]. 49 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),20(a,1,1,1,1))]. 53 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(20(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 58 (h(x)' + (x + (x + (g(x) + x')))')' = x + (x + g(x)). [para(12(a,1),20(a,1,1,1,1)),rewrite([7(7),7(6)])]. 89 ((x' + y)' + (y + x)')' = y. [para(6(a,1),21(a,1,1))]. 91 (x + ((x + y)' + (y' + x)'')')' = (x + y)'. [para(21(a,1),8(a,1,1,1))]. 95 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 96 ((x + (y + y'))' + (g(y) + x)')' = x. [para(10(a,1),21(a,1,1,2,1,1))]. 99 ((x + (g(y) + (y + y)'))' + (y + x)')' = x. [para(28(a,1),21(a,1,1,2,1,1))]. 100 ((x + (g(y) + h(y)'))' + (y + x)')' = x. [para(37(a,1),21(a,1,1,2,1,1))]. 109 ((x + (g(y) + (y + (g(y) + h(y)))'))' + (y + x)')' = x. [para(43(a,1),21(a,1,1,2,1,1))]. 119 x + h(y) = y + (y + (y + (g(y) + x))). [para(29(a,1),6(a,1)),flip(a)]. 325 ((x + y)' + (y + (g(x) + h(x)'))')' = y. [para(37(a,1),89(a,1,1,1,1,1))]. 429 x + h(y) = y + (y + (y + (x + g(y)))). [para(6(a,1),119(a,2,2,2,2))]. 435 x + (y + h(z)) = z + (x + (z + (z + (g(z) + y)))). [para(119(a,2),19(a,1,2))]. 462 x + (y + h(z)) = z + (z + (x + (z + (y + g(z))))). [para(429(a,2),7(a,2,2)),rewrite([19(6),19(5),7(4)]),flip(a)]. 572 (x + (x + (g(y) + (h(y)' + (x + y)')))')' = (x + y)'. [para(39(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. 794 (g(x) + (g(x) + (x' + h(x)'))')' = x'. [para(10(a,1),100(a,1,1,2)),rewrite([19(6),6(9)])]. 795 (h(x)' + (x + (x + (g(x) + (g(x) + h(x)'))))')' = x + (x + g(x)). [para(12(a,1),100(a,1,1,2,1)),rewrite([19(8),7(7),7(6),19(8),19(7),6(12)])]. 1000 (h(x)' + (x + (g(x) + (x + x)'))')' = x + g(x). [para(12(a,1),49(a,1,1,1,1)),rewrite([7(7)])]. 1463 ((x + y)' + (y + (y + (x' + (x + y)')))')' = y. [para(53(a,1),8(a,1,1,2)),rewrite([6(10)])]. 1477 (x + (x + (x + (g(x) + (x + (x + (x + (g(x) + (y' + (y + h(x))')))))'))))' = (y + h(x))'. [para(29(a,1),53(a,1,1,2,1)),rewrite([29(13)])]. 1812 (h(x)' + (x + (x + (g(x) + (g(x) + (x + x)'))))')' = x + (x + g(x)). [para(12(a,1),99(a,1,1,2,1)),rewrite([19(8),7(7),7(6),19(8),19(7),6(12)])]. 1814 (g(x) + (g(x) + ((x + x)' + (g(x) + h(x))'))')' = (g(x) + h(x))'. [para(40(a,1),99(a,1,1,2)),rewrite([6(9),7(9),6(12)])]. 3554 x + (y + (g(x) + (z + h(x)))) = y + (x + (x + (x + (x + (g(x) + (z + g(x))))))). [para(462(a,2),435(a,2,2,2)),rewrite([6(5),19(5),29(4)]),flip(a)]. 4470 (x + (g(x) + (x + (g(x) + (h(x)' + (x + x)')))'))' = h(x)'. [para(1000(a,1),8(a,1,1,2)),rewrite([19(8),19(7),6(12),7(12)])]. 7586 (h(x)' + (x + (x + (x + (x + (g(x) + (g(x) + (x' + h(x)')))))))')' = x + (x + g(x)). [para(58(a,1),95(a,1,1,2,1,2,2)),rewrite([6(13),19(13),19(12),19(11),7(10),7(9),19(11),19(10),6(14),7(14),7(13),7(12),7(11),7(10),7(9),58(27)])]. 14441 (g(x) + (g(x) + ((x + x)' + (x + (x + (x + (g(x) + g(x)))))'))')' = (g(x) + h(x))'. [para(30(a,1),1814(a,1,1,2,1,2,2,1)),rewrite([6(7),19(8)])]. 14619 (x + h(x)')' = g(x). [para(4470(a,1),32(a,1,1,1)),rewrite([572(14),28(7),6(3)])]. 14629 (g(x) + (x + h(x))')' = x. [para(14619(a,1),8(a,1,1,2)),rewrite([6(5)])]. 14660 (g(x) + (g(x) + (h(x)' + (x + x)'))')' = h(x)'. [para(14619(a,1),99(a,1,1,2)),rewrite([19(7),6(10)])]. 14683 (x + (x + (g(x) + h(x)))')' = g(x). [para(14619(a,1),95(a,1,1,2,1,2,2)),rewrite([6(3),14619(11)])]. 14690 (g(x) + (g(x) + (h(x)' + (x + (g(x) + h(x)))'))')' = h(x)'. [para(14619(a,1),109(a,1,1,2)),rewrite([19(10),6(13)])]. 14817 (g(x) + (x + (x + (g(x) + h(x))))')' = x. [para(14629(a,1),95(a,1,1,2,1,2,2)),rewrite([6(5),19(6),19(5),14629(15)])]. 14993 (x + (g(x) + h(x)))' = h(x)'. [para(14683(a,1),100(a,1,1,2)),rewrite([6(10),7(10),6(13),14690(14)]),flip(a)]. 14997 (x + (x + (x + (x + (x + (x + (g(x) + (g(x) + g(x))))))))')' = g(x). [para(14683(a,1),95(a,1,1,2,1,2,2)),rewrite([6(6),19(6),3554(7),14993(18),14619(17)])]. 15004 (x + (x + (x + (x + (g(x) + g(x))))))' = h(x)'. [para(30(a,1),14993(a,1,1,2)),rewrite([6(3),19(4)])]. 15005 (h(x)' + (x + (g(x) + h(x)'))')' = x + g(x). [para(14993(a,1),22(a,1,1,1))]. 15465 (g(x) + (x + (x + (x + (x + (x + (g(x) + g(x)))))))')' = x. [para(30(a,1),14817(a,1,1,2,1,2,2)),rewrite([6(4),19(5)])]. 16389 x + (x + (g(x) + g(x))) = x + (x + g(x)). [para(15004(a,1),49(a,1,1,1)),rewrite([7(10),7(9),7(8),1812(13)]),flip(a)]. 16393 (h(x)' + (x + (x + (x + (g(x) + (g(x) + h(x)')))))')' = h(x). [para(15004(a,1),325(a,1,1,1)),rewrite([16389(7),12(6),19(8),29(7),19(11),19(10),19(9),16389(19),12(18)])]. 16397 (x + h(x))' = h(x)'. [para(15004(a,1),53(a,2)),rewrite([16389(5),12(4),16389(6),12(5),16389(8),12(7),29(8),29(13),1477(17)])]. 16490 (h(x)' + (x + (x + (x + (x + (x + (x + (g(x) + (g(x) + (x' + h(x)')))))))))')' = h(x). [para(15004(a,1),1463(a,1,1,1)),rewrite([16389(7),12(6),16389(8),12(7),16389(10),12(9),16397(8),29(9),19(13),19(12),19(11),19(10),29(9),19(13),19(12),19(11),16389(24),12(23)])]. 16497 (g(x) + (x + (x + h(x)))')' = x. [back_rewrite(15465),rewrite([16389(6),12(5)])]. 16498 (g(x) + h(x))' = h(x)'. [back_rewrite(14441),rewrite([16389(9),12(8),6(7),14660(11)]),flip(a)]. 16606 (h(x)' + (x + (x + (x + (x + (g(x) + x')))))')' = h(x). [para(16498(a,1),96(a,1,1,2)),rewrite([19(4),29(3),6(11)])]. 16705 ((x + (g(y) + (y + (y + h(y)))'))' + (y + x)')' = x. [para(16497(a,1),21(a,1,1,2,1,1))]. 16819 x + (x + (g(x) + (g(x) + y))) = x + (x + (g(x) + y)). [para(16389(a,1),7(a,1,1)),rewrite([7(4),7(3),7(9),7(8)]),flip(a)]. 16882 (h(x)' + (x + (x + (x + (x + (x + (x + (g(x) + (x' + h(x)'))))))))')' = h(x). [back_rewrite(16490),rewrite([16819(12)])]. 16886 (h(x)' + (x + (x + (x + (g(x) + h(x)'))))')' = h(x). [back_rewrite(16393),rewrite([16819(10)])]. 16899 (x + (x + (x + h(x)))')' = g(x). [back_rewrite(14997),rewrite([16819(7),16389(5),12(4)])]. 16967 (h(x)' + (x + (x + (x + (x + (g(x) + (x' + h(x)'))))))')' = x + (x + g(x)). [back_rewrite(7586),rewrite([16819(12)])]. 17024 (h(x)' + (x + (x + (g(x) + h(x)')))')' = x + (x + g(x)). [back_rewrite(795),rewrite([16819(10)])]. 17160 (g(x) + (g(x) + (h(x)' + (x + (x + h(x)))'))')' = (x + (x + h(x)))'. [para(16899(a,1),100(a,1,1,2)),rewrite([6(9),7(9),6(12)])]. 17527 (h(x)' + (x + (x + (g(x) + (h(x)' + h(x)'))))')' = x + g(x). [para(15005(a,1),95(a,1,1,2,1,2,2)),rewrite([6(12),19(12),19(11),7(10),19(11),16819(12),19(11),19(10),19(9),15005(24)])]. 18543 (h(x)' + (x + (x + (x + (x + (x + (x + (g(x) + (h(x)' + h(x)'))))))))')' = h(x). [para(16886(a,1),95(a,1,1,2,1,2,2)),rewrite([6(13),19(13),19(12),19(11),19(10),29(9),19(13),19(12),19(11),16819(12),19(15),19(14),19(13),19(12),19(11),19(10),19(9),16886(30)])]. 19505 (x + (x + (x + (x + (g(x) + (x' + h(x)'))))))' = (x + (x + (g(x) + h(x)')))'. [para(16606(a,1),23(a,1,1,2,1,2,1)),rewrite([6(12),7(12),7(11),7(10),7(9),7(8),6(16),16967(17),6(6),7(6),7(5),6(17),7(17),7(16),7(15),7(14),7(13)]),flip(a)]. 19643 (x + (x + h(x)))' = h(x)'. [para(14619(a,1),16705(a,1,1,2)),rewrite([19(9),6(12),17160(13)])]. 19645 x + h(x) = h(x). [para(19643(a,1),20(a,1,1,1)),rewrite([7(6),29(5),16606(12)]),flip(a)]. 19674 x + (x + (x + (x + (g(x) + y)))) = x + (x + (x + (g(x) + y))). [para(19645(a,1),7(a,1,1)),rewrite([29(2),29(7)]),flip(a)]. 19715 (x + (x + (x + (g(x) + (x' + h(x)')))))' = (x + (x + (g(x) + h(x)')))'. [back_rewrite(19505),rewrite([19674(10)])]. 19718 (h(x)' + (x + (x + (x + (g(x) + (h(x)' + h(x)')))))')' = h(x). [back_rewrite(18543),rewrite([19674(13),19674(13),19674(13)])]. 19724 x + (x + g(x)) = h(x). [back_rewrite(16882),rewrite([19674(12),19674(12),19674(12),19715(12),17024(11)])]. 20001 x + (x + (x + (g(x) + y))) = x + (x + (g(x) + y)). [para(19724(a,1),7(a,1,1)),rewrite([29(2),7(8)])]. 20114 x + g(x) = h(x). [back_rewrite(19718),rewrite([20001(12),17527(14)])]. 21899 h(x)' = x'. [para(20114(a,1),53(a,1,1,2,1,2,2,1)),rewrite([794(10),20114(3)]),flip(a)]. 21930 (x + (x' + (x + g(x)')'')')' = x'. [para(20114(a,1),91(a,1,1,2,1,1,1)),rewrite([21899(2),6(4),20114(12),21899(12)])]. 21931 $F # answer(Winker2a). [resolve(21930,a,16,a)]. ============================== end of proof ========================== % Redundant proof: 21935 $F # answer(Winker2a). [resolve(21934,a,16,a)]. % Redundant proof: 21986 $F # answer(Winker2a). [resolve(21985,a,16,a)]. % Redundant proof: 23298 $F # answer(Winker2a). [resolve(23297,a,16,a)]. % Redundant proof: 23302 $F # answer(Winker2a). [resolve(23301,a,16,a)]. % Redundant proof: 23365 $F # answer(Winker2a). [resolve(23364,a,16,a)]. % Redundant proof: 23497 $F # answer(Winker2a). [resolve(23496,a,16,a)]. % Redundant proof: 23499 $F # answer(Winker2a). [resolve(23498,a,16,a)]. % Redundant proof: 23667 $F # answer(Winker2a). [resolve(23666,a,16,a)]. % Redundant proof: 24567 $F # answer(Winker2a). [resolve(24566,a,16,a)]. % Redundant proof: 24627 $F # answer(Winker2a). [resolve(24626,a,16,a)]. % Redundant proof: 24645 $F # answer(Winker2a). [resolve(24644,a,16,a)]. % Redundant proof: 24686 $F # answer(Winker2a). [resolve(24685,a,16,a)]. % Redundant proof: 24689 $F # answer(Winker2a). [resolve(24688,a,16,a)]. % Redundant proof: 24691 $F # answer(Winker1a). [resolve(24690,a,14,a)]. % Redundant proof: 24755 $F # answer(Winker2a). [resolve(24754,a,16,a)]. % Redundant proof: 24758 $F # answer(Winker2a). [resolve(24757,a,16,a)]. % Redundant proof: 24761 $F # answer(Winker2a). [resolve(24760,a,16,a)]. % Redundant proof: 24768 $F # answer(Winker2a). [resolve(24767,a,16,a)]. % Redundant proof: 24771 $F # answer(Winker2a). [resolve(24770,a,16,a)]. % Redundant proof: 24816 $F # answer(Winker2a). [resolve(24815,a,16,a)]. % Redundant proof: 24820 $F # answer(Winker2a). [resolve(24819,a,16,a)]. % Redundant proof: 24829 $F # answer(Winker2a). [resolve(24828,a,16,a)]. % Redundant proof: 24833 $F # answer(Winker2a). [resolve(24832,a,16,a)]. % Redundant proof: 24911 $F # answer(Winker2a). [resolve(24910,a,16,a)]. % Redundant proof: 24915 $F # answer(Winker2a). [resolve(24914,a,16,a)]. % Redundant proof: 24950 $F # answer(Winker2a). [resolve(24949,a,16,a)]. % Redundant proof: 24981 $F # answer(Winker2a). [resolve(24980,a,16,a)]. % Redundant proof: 25001 $F # answer(Winker2a). [resolve(25000,a,16,a)]. % Redundant proof: 25020 $F # answer(Winker2a). [resolve(25019,a,16,a)]. % Redundant proof: 25024 $F # answer(Winker2a). [resolve(25023,a,16,a)]. % Redundant proof: 25110 $F # answer(Winker2a). [resolve(25109,a,16,a)]. % Redundant proof: 25161 $F # answer(Winker2a). [resolve(25160,a,16,a)]. % Redundant proof: 25309 $F # answer(Winker2a). [resolve(25308,a,16,a)]. % Redundant proof: 25311 $F # answer(Winker2a). [resolve(25310,a,16,a)]. % Redundant proof: 25394 $F # answer(Winker2a). [resolve(25393,a,16,a)]. % Redundant proof: 25397 $F # answer(Winker2a). [resolve(25396,a,16,a)]. % Redundant proof: 25484 $F # answer(Winker2a). [resolve(25483,a,16,a)]. % Redundant proof: 25488 $F # answer(Winker2a). [resolve(25487,a,16,a)]. % Redundant proof: 25498 $F # answer(Winker2a). [resolve(25497,a,16,a)]. % Redundant proof: 25507 $F # answer(Winker2a). [resolve(25506,a,16,a)]. % Redundant proof: 25510 $F # answer(Winker2a). [resolve(25509,a,16,a)]. % Redundant proof: 25515 $F # answer(Winker2a). [resolve(25514,a,16,a)]. % Redundant proof: 25834 $F # answer(Winker2a). [resolve(25833,a,16,a)]. % Redundant proof: 25864 $F # answer(Winker2a). [resolve(25863,a,16,a)]. % Redundant proof: 25957 $F # answer(Winker2a). [resolve(25956,a,16,a)]. % Redundant proof: 26010 $F # answer(Winker2a). [resolve(26009,a,16,a)]. % Redundant proof: 26154 $F # answer(Winker2a). [resolve(26153,a,16,a)]. % Redundant proof: 26691 $F # answer(Winker2a). [resolve(26690,a,16,a)]. % Redundant proof: 26835 $F # answer(Winker2a). [resolve(26834,a,16,a)]. % Redundant proof: 26853 $F # answer(Winker2a). [resolve(26852,a,16,a)]. % Redundant proof: 26875 $F # answer(Winker2a). [resolve(26874,a,16,a)]. % Redundant proof: 26942 $F # answer(Winker2a). [resolve(26941,a,16,a)]. % Redundant proof: 27041 $F # answer(Winker2a). [resolve(27040,a,16,a)]. % Redundant proof: 27735 $F # answer(Winker2a). [resolve(27734,a,16,a)]. % Redundant proof: 27967 $F # answer(Winker1a). [resolve(27966,a,14,a)]. % Redundant proof: 27969 $F # answer(Winker1a). [resolve(27968,a,14,a)]. % Redundant proof: 27972 $F # answer(Winker2a). [resolve(27971,a,16,a)]. % Redundant proof: 27975 $F # answer(Winker2a). [resolve(27974,a,16,a)]. % Redundant proof: 28284 $F # answer(Winker2a). [resolve(28283,a,16,a)]. % Redundant proof: 28286 $F # answer(Winker2a). [resolve(28285,a,16,a)]. % Redundant proof: 28305 $F # answer(Winker1a). [resolve(28304,a,14,a)]. % Redundant proof: 28329 $F # answer(Winker1a). [resolve(28328,a,14,a)]. % Redundant proof: 28375 $F # answer(Winker2a). [resolve(28374,a,16,a)]. % Redundant proof: 28377 $F # answer(Winker2a). [resolve(28376,a,16,a)]. % Redundant proof: 28379 $F # answer(Winker1a). [resolve(28378,a,14,a)]. % Redundant proof: 28391 $F # answer(Winker1a). [resolve(28390,a,14,a)]. % Redundant proof: 28395 $F # answer(Winker2a). [resolve(28394,a,16,a)]. % Redundant proof: 28397 $F # answer(Winker2a). [resolve(28396,a,16,a)]. % Redundant proof: 28399 $F # answer(Winker2a). [resolve(28398,a,16,a)]. % Redundant proof: 28401 $F # answer(Winker2a). [resolve(28400,a,16,a)]. % Redundant proof: 28403 $F # answer(Winker2a). [resolve(28402,a,16,a)]. % Redundant proof: 28539 $F # answer(Winker2a). [resolve(28538,a,16,a)]. % Redundant proof: 28545 $F # answer(Winker2a). [resolve(28544,a,16,a)]. % Redundant proof: 28563 $F # answer(Winker2a). [resolve(28562,a,16,a)]. % Redundant proof: 28574 $F # answer(Winker2a). [resolve(28573,a,16,a)]. % Redundant proof: 28593 $F # answer(Winker1a). [resolve(28592,a,14,a)]. % Redundant proof: 28595 $F # answer(Winker1a). [resolve(28594,a,14,a)]. % Redundant proof: 28597 $F # answer(Winker1a). [resolve(28596,a,14,a)]. % Redundant proof: 28599 $F # answer(Winker1a). [resolve(28598,a,14,a)]. % Redundant proof: 28601 $F # answer(Winker1a). [resolve(28600,a,14,a)]. % Redundant proof: 28603 $F # answer(Winker1a). [resolve(28602,a,14,a)]. % Redundant proof: 28605 $F # answer(Winker1a). [resolve(28604,a,14,a)]. % Redundant proof: 28607 $F # answer(Winker1a). [resolve(28606,a,14,a)]. % Redundant proof: 28609 $F # answer(Winker1a). [resolve(28608,a,14,a)]. % Redundant proof: 28611 $F # answer(Winker1a). [resolve(28610,a,14,a)]. % Redundant proof: 28613 $F # answer(Winker1a). [resolve(28612,a,14,a)]. % Redundant proof: 28615 $F # answer(Winker1a). [resolve(28614,a,14,a)]. % Redundant proof: 28617 $F # answer(Winker1a). [resolve(28616,a,14,a)]. % Redundant proof: 28619 $F # answer(Winker1a). [resolve(28618,a,14,a)]. % Redundant proof: 28621 $F # answer(Winker1a). [resolve(28620,a,14,a)]. % Redundant proof: 28623 $F # answer(Winker1a). [resolve(28622,a,14,a)]. % Redundant proof: 28625 $F # answer(Winker1a). [resolve(28624,a,14,a)]. % Redundant proof: 28627 $F # answer(Winker1a). [resolve(28626,a,14,a)]. % Redundant proof: 28629 $F # answer(Winker1a). [resolve(28628,a,14,a)]. % Redundant proof: 28631 $F # answer(Winker1a). [resolve(28630,a,14,a)]. % Redundant proof: 28633 $F # answer(Winker1a). [resolve(28632,a,14,a)]. % Redundant proof: 28635 $F # answer(Winker1a). [resolve(28634,a,14,a)]. % Redundant proof: 28637 $F # answer(Winker1a). [resolve(28636,a,14,a)]. % Disable descendants (x means already disabled): 16 14 given #688 (T,wt=3): 26707 h(x) = x. [back_rewrite(21918),rewrite([24690(1),21953(8)])]. given #689 (T,wt=3): 28160 g(x) = g(y). [back_rewrite(23313),rewrite([26707(1),27968(5),27968(6),28152(5),6(4),7(4),28156(5)])]. given #690 (T,wt=5): 24690 x + x = x. [back_rewrite(19646),rewrite([21899(2),21899(3),21917(7)]),flip(a)]. given #691 (A,wt=21): 267 ((x + y)' + (x + ((y + z')' + (z + y)'))')' = x. [para(48(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #692 (T,wt=5): 27966 x + g(y) = x. [back_rewrite(24892),rewrite([26707(1),26707(6),27965(9),27965(9),500(11)]),flip(a)]. given #693 (T,wt=5): 27968 g(x) + y = y. [back_rewrite(24840),rewrite([26707(1),26707(6),27965(10),27965(10),500(11)]),flip(a)]. given #694 (T,wt=5): 28152 x'' = x. [back_rewrite(23392),rewrite([27968(6),10(6),27968(7),24996(7),6(3),27968(3),26707(3)])]. ============================== PROOF ================================= % Proof 5 at 47.38 (+ 0.16) seconds: Huntington. % Length of proof is 138. % Level of proof is 30. % Maximum clause weight is 30. % Given clauses 694. 1 (x + y')' + (x' + y')' = y # answer(Huntington) # label(non_clause) # label(goal). [goal]. 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]. 9 g(x) = (x + x')' # label(definition_g). [assumption]. 10 (x + x')' = g(x). [copy(9),flip(a)]. 11 h(x) = x + (x + (x + g(x))) # label(definition_h). [assumption]. 12 x + (x + (x + g(x))) = h(x). [copy(11),flip(a)]. 13 (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [deny(1)]. 19 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),rewrite([7(2)])]. 20 ((x + y)' + (y + x')')' = y. [para(6(a,1),8(a,1,1,1,1))]. 21 ((x + y)' + (y' + x)')' = x. [para(6(a,1),8(a,1,1,2,1))]. 22 ((x + (y + z))' + (x + (y + z'))')' = x + y. [para(7(a,1),8(a,1,1,1,1)),rewrite([7(6)])]. 23 (x + ((x + y)' + (x + y')'')')' = (x + y)'. [para(8(a,1),8(a,1,1,1))]. 24 ((x + y)' + (x + ((y + z)' + (y + z')'))')' = x. [para(8(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. 25 (x + (x + (y' + (x + y)'))')' = (x + y)'. [para(8(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 28 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. 29 h(x) + y = x + (x + (x + (g(x) + y))). [para(12(a,1),7(a,1,1)),rewrite([7(6),7(5)])]. 30 x + h(y) = y + (y + (g(y) + (x + y))). [para(12(a,1),7(a,2,2)),rewrite([19(5),19(4),6(3)]),flip(a)]. 31 (h(x)' + (x + (x + (x + g(x)))')')' = x. [para(12(a,1),8(a,1,1,1,1))]. 32 ((x + (y + z))' + (y + (x + z)')')' = y. [para(19(a,1),8(a,1,1,1,1))]. 36 (x + (x + (x + g(x)))')' = g(x). [para(28(a,1),8(a,1,1,2)),rewrite([19(3),6(2),6(5)])]. 37 (g(x) + h(x)')' = x. [back_rewrite(31),rewrite([36(8),6(4)])]. 39 ((x + y)' + (x + (g(y) + h(y)'))')' = x. [para(37(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. 40 (x + (g(x) + h(x))')' = g(x). [para(37(a,1),8(a,1,1,2)),rewrite([6(5)])]. 43 (g(x) + (x + (g(x) + h(x)))')' = x. [para(40(a,1),8(a,1,1,2)),rewrite([6(7)])]. 47 ((x + y)' + (x' + y)')' = y. [para(6(a,1),20(a,1,1,2,1))]. 49 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),20(a,1,1,1,1))]. 53 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(20(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 58 (h(x)' + (x + (x + (g(x) + x')))')' = x + (x + g(x)). [para(12(a,1),20(a,1,1,1,1)),rewrite([7(7),7(6)])]. 62 (x + (g(x)' + h(x)')')' = h(x)'. [para(37(a,1),20(a,1,1,1)),rewrite([6(5)])]. 89 ((x' + y)' + (y + x)')' = y. [para(6(a,1),21(a,1,1))]. 95 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 96 ((x + (y + y'))' + (g(y) + x)')' = x. [para(10(a,1),21(a,1,1,2,1,1))]. 99 ((x + (g(y) + (y + y)'))' + (y + x)')' = x. [para(28(a,1),21(a,1,1,2,1,1))]. 100 ((x + (g(y) + h(y)'))' + (y + x)')' = x. [para(37(a,1),21(a,1,1,2,1,1))]. 101 ((x + (y + (g(y) + h(y))'))' + (g(y) + x)')' = x. [para(40(a,1),21(a,1,1,2,1,1))]. 109 ((x + (g(y) + (y + (g(y) + h(y)))'))' + (y + x)')' = x. [para(43(a,1),21(a,1,1,2,1,1))]. 115 (h(x)' + (x + (g(x)' + h(x)'))')' = x. [para(62(a,1),8(a,1,1,2)),rewrite([6(10)])]. 119 x + h(y) = y + (y + (y + (g(y) + x))). [para(29(a,1),6(a,1)),flip(a)]. 146 ((x + (y + (z + u)))' + (x + (y + (z + u')))')' = x + (y + z). [para(7(a,1),22(a,1,1,1,1,2)),rewrite([7(7)])]. 155 ((x + (y + z))' + (y + (x + z'))')' = y + x. [para(19(a,1),22(a,1,1,1,1))]. 325 ((x + y)' + (y + (g(x) + h(x)'))')' = y. [para(37(a,1),89(a,1,1,1,1,1))]. 365 (x + (g(x) + ((h(x)' + y)' +