============================== Prover9 =============================== Prover9 (32) version June-2007-, 12 June 2007. Process 10345 was started by mccune on cleo, Wed Jun 13 10:27:47 2007 The command was "prover9 -f winner.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file winner.in assign(max_minutes,5). % assign(max_minutes, 5) -> assign(max_seconds, 300). assign(max_weight,35). set(restrict_denials). assign(eq_defs,fold). formulas(assumptions). x + y = y + x # label(Commutativity). (x + y) + z = x + (y + z) # label(Associativity). ((x + y)' + (x + y')')' = x # label(Robbins). end_of_list. formulas(goals). (exists a exists b (a + b)' = a') # answer(Winker2a). (exists a exists b (a + b)' = b') # answer(Winker2b). (exists a exists b a + b = a) # answer(Winker1a). (exists a exists b a + b = b) # answer(Winker1b). (x + y')' + (x' + y')' = y # answer(Huntington). end_of_list. formulas(assumptions). g(x) = (x + x')'. h(x) = (x + (x + (x + g(x))))'. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (exists a exists b (a + b)' = a') # answer(Winker2a) # label(non_clause) # label(goal). [goal]. 2 (exists a exists b (a + b)' = b') # answer(Winker2b) # label(non_clause) # label(goal). [goal]. 3 (exists a exists b a + b = a) # answer(Winker1a) # label(non_clause) # label(goal). [goal]. 4 (exists a exists b a + b = b) # answer(Winker1b) # label(non_clause) # label(goal). [goal]. 5 (x + y')' + (x' + y')' = y # answer(Huntington) # 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')'. [assumption]. h(x) = (x + (x + (x + g(x))))'. [assumption]. (x + y)' != x' # answer(Winker2a). [deny(1)]. (x + y)' != y' # answer(Winker2b). [deny(2)]. x + y != x # answer(Winker1a). [deny(3)]. x + y != y # answer(Winker1b). [deny(4)]. (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [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=7): 13 (x + y)' != x' # answer(Winker2a). [deny(1)]. restricted denial: (wt=7): 14 (x + y)' != y' # answer(Winker2b). [deny(2)]. restricted denial: (wt=5): 15 x + y != x # answer(Winker1a). [deny(3)]. restricted denial: (wt=5): 16 x + y != y # answer(Winker1b). [deny(4)]. restricted denial: (wt=14): 17 (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [deny(5)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 13 (x + y)' != x' # answer(Winker2a). [deny(1)]. 14 (x + y)' != y' # answer(Winker2b). [deny(2)]. 15 x + y != x # answer(Winker1a). [deny(3)]. 16 x + y != y # answer(Winker1b). [deny(4)]. 17 (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [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=8): 10 (x + x')' = g(x). [copy(9),flip(a)]. given #5 (I,wt=12): 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=10): 29 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. given #8 (T,wt=8): 42 (g(x) + h(x))' = x. [back_rewrite(33),rewrite([40(7),6(3)])]. given #9 (T,wt=12): 27 (g(x) + (x + x'')')' = x. [para(10(a,1),8(a,1,1,1))]. given #10 (T,wt=13): 20 ((x + y)' + (y + x')')' = y. [para(6(a,1),8(a,1,1,1,1))]. given #11 (A,wt=13): 21 ((x + y)' + (y' + x)')' = x. [para(6(a,1),8(a,1,1,2,1))]. given #12 (T,wt=13): 40 (x + (x + (x + g(x)))')' = g(x). [para(29(a,1),8(a,1,1,2)),rewrite([19(3),6(2),6(5)])]. given #13 (T,wt=13): 43 (x + (g(x) + h(x)')')' = g(x). [para(42(a,1),8(a,1,1,1))]. given #14 (T,wt=13): 56 ((x + y)' + (x' + y)')' = y. [para(6(a,1),20(a,1,1,2,1))]. given #15 (T,wt=13): 57 ((x + y')' + (y + x)')' = x. [para(6(a,1),20(a,1,1))]. given #16 (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 #17 (T,wt=13): 66 (g(x) + (x' + x')')' = x'. [para(10(a,1),20(a,1,1,1))]. given #18 (T,wt=13): 73 (x + (h(x) + g(x)')')' = h(x). [para(42(a,1),20(a,1,1,1))]. given #19 (T,wt=13): 79 ((x' + y)' + (y + x)')' = y. [para(6(a,1),21(a,1,1))]. given #20 (T,wt=14): 26 (x + (y + (x + y)'))' = g(x + y). [para(7(a,1),10(a,1,1))]. given #21 (A,wt=20): 23 (x + ((x + y)' + (x + y')'')')' = (x + y)'. [para(8(a,1),8(a,1,1,1))]. given #22 (T,wt=14): 31 (x + (g(x) + x'))' = g(x + x'). [para(10(a,1),10(a,1,1,2)),rewrite([6(4),19(4)])]. given #23 (T,wt=14): 198 (g(g(x) + h(x)) + (x + x)')' = x. [para(42(a,1),66(a,1,1,2,1,1)),rewrite([42(8),42(12)])]. given #24 (T,wt=14): 254 (x + (y + (y + x)'))' = g(x + y). [para(6(a,1),26(a,1,1,2,2,1))]. given #25 (T,wt=15): 38 (x + (g(x) + (x + x)'')')' = g(x). [para(29(a,1),8(a,1,1,1))]. given #26 (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 #27 (T,wt=15): 45 (x + (g(x) + h(x)))' = g(g(x) + h(x)). [para(42(a,1),10(a,1,1,2)),rewrite([6(4)])]. given #28 (T,wt=15): 49 (x + (x + (g(x) + x''))')' = g(x). [para(27(a,1),8(a,1,1,2)),rewrite([19(5),6(7)])]. given #29 (T,wt=15): 88 (g(x') + (x + x'')')' = x''. [para(10(a,1),21(a,1,1,2)),rewrite([6(3),6(7)])]. given #30 (T,wt=15): 113 (g(x) + (x + (g(x) + h(x)'))')' = x. [para(43(a,1),8(a,1,1,2)),rewrite([6(8)])]. given #31 (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 #32 (T,wt=15): 217 (h(x) + (x + (h(x) + g(x)'))')' = x. [para(73(a,1),8(a,1,1,2)),rewrite([6(8)])]. given #33 (T,wt=16): 28 ((x + g(y))' + (x + (y + y'))')' = x. [para(10(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])]. given #34 (T,wt=16): 44 ((x + y)' + (x + (g(y) + h(y)))')' = x. [para(42(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])]. given #35 (T,wt=16): 67 ((x + (x' + y))' + (y + g(x))')' = y. [para(10(a,1),20(a,1,1,2,1,2)),rewrite([7(3)])]. given #36 (A,wt=25): 30 (x + ((x + y)' + (x + y')'))' = g((x + y)' + (x + y')'). [para(8(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #37 (T,wt=16): 74 ((g(x) + (h(x) + y))' + (y + x)')' = y. [para(42(a,1),20(a,1,1,2,1,2)),rewrite([7(4)])]. given #38 (T,wt=16): 87 ((x + (y + y'))' + (g(y) + x)')' = x. [para(10(a,1),21(a,1,1,2,1,1))]. given #39 (T,wt=14): 837 (x + (x + (h(x) + x'))')' = h(x). [para(42(a,1),87(a,1,1,2)),rewrite([19(4),6(6)])]. given #40 (T,wt=16): 94 ((x + (g(y) + h(y)))' + (y + x)')' = x. [para(42(a,1),21(a,1,1,2,1,1))]. given #41 (A,wt=22): 32 (x + (y + (x + (y + (x + (y + g(x + y)))))))' = h(x + y). [para(7(a,1),12(a,1,1,2,2)),rewrite([19(7),19(6),7(5),19(8),19(7),19(6),19(5),7(4)])]. given #42 (T,wt=16): 125 ((g(x) + y)' + (x + (x' + y))')' = y. [para(10(a,1),56(a,1,1,2,1,1)),rewrite([7(3),6(8)])]. given #43 (T,wt=16): 130 ((x + y)' + (g(x) + (h(x) + y))')' = y. [para(42(a,1),56(a,1,1,2,1,1)),rewrite([7(4),6(8)])]. given #44 (T,wt=16): 146 ((x + g(y))' + (y + (y' + x))')' = x. [para(10(a,1),57(a,1,1,1,1,2)),rewrite([7(6)])]. given #45 (T,wt=16): 150 ((x + y)' + (g(y) + (h(y) + x))')' = x. [para(42(a,1),57(a,1,1,1,1,2)),rewrite([7(6)])]. given #46 (A,wt=20): 34 ((x + h(y))' + (x + (y + (y + (y + g(y)))))')' = x. [para(12(a,1),8(a,1,1,2,1,2)),rewrite([6(10)])]. given #47 (T,wt=16): 192 (x' + (g(x) + (x' + x'))')' = g(x). [para(66(a,1),8(a,1,1,2)),rewrite([6(8)])]. given #48 (T,wt=16): 195 (g(x + x') + (g(x) + g(x))')' = g(x). [para(10(a,1),66(a,1,1,2,1,1)),rewrite([10(7),10(12)])]. given #49 (T,wt=16): 197 ((x + x)' + g(g(x) + (x + x)'))' = x. [para(29(a,1),66(a,1,1,2,1,1)),rewrite([29(10),6(8),29(14)])]. given #50 (T,wt=16): 231 ((g(x) + y)' + (y + (x + x'))')' = y. [para(10(a,1),79(a,1,1,1,1,1))]. given #51 (A,wt=22): 35 (x + (x + (x + (g(x) + h(x)))))' = g(x + (x + (x + g(x)))). [para(12(a,1),10(a,1,1,2)),rewrite([6(6),19(6),19(5),19(4),6(3)])]. given #52 (T,wt=16): 236 ((x + y)' + (y + (g(x) + h(x)))')' = y. [para(42(a,1),79(a,1,1,1,1,1))]. given #53 (T,wt=16): 512 (g(x) + (g(x) + (h(x) + x'))')' = x'. [para(42(a,1),88(a,1,1,1,1)),rewrite([42(8),7(6),42(13)])]. given #54 (T,wt=16): 647 ((x + g(y))' + (y + (x + y'))')' = x. [para(19(a,1),28(a,1,1,2,1))]. given #55 (T,wt=16): 682 (g(x) + (x + (g(x') + h(x')))')' = x. [para(10(a,1),44(a,1,1,1))]. given #56 (A,wt=17): 36 ((x + (y + z))' + (y + (x + z)')')' = y. [para(19(a,1),8(a,1,1,1,1))]. given #57 (T,wt=16): 685 ((x + y)' + (g(y) + (x + h(y)))')' = x. [para(19(a,1),44(a,1,1,2,1))]. given #58 (T,wt=16): 834 ((x + (y + x'))' + (g(x) + y)')' = y. [para(19(a,1),87(a,1,1,1,1))]. given #59 (T,wt=16): 883 (h(x) + (x + (x + (h(x) + x')))')' = x. [para(837(a,1),8(a,1,1,2)),rewrite([6(8)])]. given #60 (T,wt=16): 919 ((x + y)' + (g(x) + (y + h(x)))')' = y. [para(19(a,1),94(a,1,1,1,1)),rewrite([6(8)])]. given #61 (A,wt=18): 37 (g(x + y) + (x + (y + (x + y)))')' = x + y. [para(7(a,1),29(a,1,1,2,1))]. given #62 (T,wt=16): 982 ((g(x) + y)' + (x + (y + x'))')' = y. [para(6(a,1),125(a,1,1,2,1,2))]. given #63 (T,wt=17): 47 (x + (g(x) + (x + x'')'')')' = g(x). [para(27(a,1),8(a,1,1,1))]. given #64 (T,wt=17): 58 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),20(a,1,1,1,1))]. given #65 (T,wt=17): 71 (x + (g(x)' + (x + x)')')' = (x + x)'. [para(29(a,1),20(a,1,1,1)),rewrite([6(5)])]. given #66 (A,wt=18): 39 ((x + y)' + (x + (g(y) + (y + y)'))')' = x. [para(29(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. given #67 (T,wt=17): 91 ((x + (y + z))' + ((x + z)' + y)')' = y. [para(19(a,1),21(a,1,1,1,1))]. given #68 (T,wt=17): 103 (g(x) + (x + (x + (x + g(x)))'')')' = x. [para(40(a,1),8(a,1,1,1))]. given #69 (T,wt=17): 111 (g(x) + (x + (g(x) + h(x)')'')')' = x. [para(43(a,1),8(a,1,1,1))]. given #70 (T,wt=17): 119 ((x + (y + z))' + ((x + y)' + z)')' = z. [para(7(a,1),56(a,1,1,1,1))]. given #71 (A,wt=19): 41 (x + (g(x) + (x + x)'))' = g(g(x) + (x + x)'). [para(29(a,1),10(a,1,1,2)),rewrite([6(5)])]. given #72 (T,wt=17): 142 ((x + (y + z)')' + (y + (z + x))')' = x. [para(7(a,1),57(a,1,1,2,1))]. given #73 (T,wt=17): 215 (h(x) + (x + (h(x) + g(x)')'')')' = x. [para(73(a,1),8(a,1,1,1))]. given #74 (T,wt=17): 234 (((x + y)' + z)' + (x + (z + y))')' = z. [para(19(a,1),79(a,1,1,2,1))]. given #75 (T,wt=17): 369 (g(x) + (x + (g(x) + (x + x)''))')' = x. [para(38(a,1),8(a,1,1,2)),rewrite([6(9)])]. given #76 (A,wt=20): 46 (g(x + y) + (x + (y + (x + y)''))')' = x + y. [para(7(a,1),27(a,1,1,2,1))]. given #77 (T,wt=17): 485 (g(x) + (x + (x + (g(x) + x'')))')' = x. [para(49(a,1),8(a,1,1,2)),rewrite([6(9)])]. given #78 (T,wt=17): 687 (x + (g(x) + (g(h(x)) + h(h(x))))')' = g(x). [para(42(a,1),44(a,1,1,1))]. given #79 (T,wt=17): 922 (x + (g(g(x)) + (h(x) + h(g(x))))')' = h(x). [para(42(a,1),94(a,1,1,2)),rewrite([19(7),6(9)])]. given #80 (T,wt=17): 1344 ((x + (y + z))' + (x + (z + y)')')' = x. [para(6(a,1),36(a,1,1,1,1)),rewrite([7(2)])]. given #81 (A,wt=20): 48 ((x + y)' + (x + (g(y) + (y + y'')'))')' = x. [para(27(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #82 (T,wt=17): 1345 ((x + (y + z))' + (y + (z + x)')')' = y. [para(6(a,1),36(a,1,1,2,1,2,1))]. given #83 (T,wt=16): 2198 ((x' + (y + x))' + (y + g(x))')' = y. [para(10(a,1),1345(a,1,1,2,1,2))]. given #84 (T,wt=16): 2203 ((x + y)' + (h(y) + (x + g(y)))')' = x. [para(42(a,1),1345(a,1,1,2,1,2)),rewrite([6(8)])]. given #85 (T,wt=16): 2293 ((g(x) + y)' + (x' + (y + x))')' = y. [para(6(a,1),2198(a,1,1,2,1)),rewrite([6(8)])]. given #86 (A,wt=23): 50 (x + (g(x) + (x + x'')'))' = g(g(x) + (x + x'')'). [para(27(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #87 (T,wt=16): 2294 ((x + g(y))' + (y' + (x + y))')' = x. [para(6(a,1),2198(a,1,1))]. given #88 (T,wt=16): 2347 ((x + y)' + (h(x) + (y + g(x)))')' = y. [para(6(a,1),2203(a,1,1,1,1))]. given #89 (T,wt=17): 1346 ((x + (y + z)')' + (y + (x + z))')' = x. [para(6(a,1),36(a,1,1))]. given #90 (T,wt=17): 1646 ((x + (y + z))' + (z + (y + x)')')' = z. [para(6(a,1),58(a,1,1,2,1,2,1))]. given #91 (A,wt=21): 51 (g(x + x') + (x + (x' + g(x)'))')' = x + x'. [para(10(a,1),27(a,1,1,2,1,2,1)),rewrite([7(8)])]. given #92 (T,wt=17): 1653 (h(x) + g(g(x) + (x + x)'))' = x + g(x). [para(12(a,1),58(a,1,1,1)),rewrite([7(6),41(7)])]. given #93 (T,wt=17): 1745 ((x + (y + z))' + ((z + y)' + x)')' = x. [para(6(a,1),91(a,1,1,1,1)),rewrite([7(2)])]. given #94 (T,wt=17): 1746 ((x + (y + z))' + ((z + x)' + y)')' = y. [para(6(a,1),91(a,1,1,2,1,1,1))]. given #95 (T,wt=17): 1882 ((x + (y + z))' + ((y + x)' + z)')' = z. [para(6(a,1),119(a,1,1,2,1,1,1))]. given #96 (A,wt=33): 52 (g(x + (x + (x + g(x)))) + (x + (x + (x + (g(x) + h(x)'))))')' = x + (x + (x + g(x))). [para(12(a,1),27(a,1,1,2,1,2,1)),rewrite([7(12),7(11),7(10)])]. given #97 (T,wt=17): 1918 ((x + (y + z)')' + (z + (y + x))')' = x. [para(6(a,1),142(a,1,1,1,1,2,1))]. given #98 (T,wt=17): 1919 ((x + (y + z)')' + (z + (x + y))')' = x. [para(6(a,1),142(a,1,1,2,1)),rewrite([7(6)])]. given #99 (T,wt=17): 1959 (((x + y)' + z)' + (y + (z + x))')' = z. [para(6(a,1),234(a,1,1,1,1,1,1))]. given #100 (T,wt=17): 1960 (((x + y)' + z)' + (z + (y + x))')' = z. [para(6(a,1),234(a,1,1,2,1)),rewrite([7(6)])]. given #101 (A,wt=29): 53 (g(g(x) + (x + x)') + (g(x) + (x' + (x + x)'))')' = g(x) + (x + x)'. [para(29(a,1),27(a,1,1,2,1,2,1)),rewrite([6(11),19(11)])]. given #102 (T,wt=18): 62 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(20(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #103 (T,wt=18): 72 ((g(x) + ((x + x)' + y))' + (y + x)')' = y. [para(29(a,1),20(a,1,1,2,1,2)),rewrite([7(5)])]. given #104 (T,wt=18): 83 (x + (y' + (x + (x + y)'))')' = (x + y)'. [para(21(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #105 (T,wt=18): 93 ((x + (g(y) + (y + y)'))' + (y + x)')' = x. [para(29(a,1),21(a,1,1,2,1,1))]. given #106 (A,wt=23): 54 (g(g(x) + h(x)) + (g(x) + (h(x) + x'))')' = g(x) + h(x). [para(42(a,1),27(a,1,1,2,1,2,1)),rewrite([7(9)])]. given #107 (T,wt=18): 122 (x + (y' + (x + (y + x)'))')' = (y + x)'. [para(56(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #108 (T,wt=18): 129 ((x + y)' + (g(x) + ((x + x)' + y))')' = y. [para(29(a,1),56(a,1,1,2,1,1)),rewrite([7(5),6(9)])]. given #109 (T,wt=18): 149 ((x + y)' + (g(y) + ((y + y)' + x))')' = x. [para(29(a,1),57(a,1,1,1,1,2)),rewrite([7(7)])]. given #110 (T,wt=18): 170 (h(x) + (x + (x + (x + g(x))'))')' = x + x. [para(12(a,1),22(a,1,1,1))]. given #111 (A,wt=35): 55 (g(g(x) + (x + x'')') + (g(x) + (x' + (x + x'')'))')' = g(x) + (x + x'')'. [para(27(a,1),27(a,1,1,2,1,2,1)),rewrite([6(15),19(15)])]. given #112 (T,wt=18): 190 (x' + (g(x) + (x' + x')'')')' = g(x). [para(66(a,1),8(a,1,1,1))]. given #113 (T,wt=18): 199 ((x + x)' + g(g(x) + (x + x'')'))' = x. [para(27(a,1),66(a,1,1,2,1,1)),rewrite([27(14),6(10),27(18)])]. given #114 (T,wt=18): 235 ((x + y)' + (y + (g(x) + (x + x)'))')' = y. [para(29(a,1),79(a,1,1,1,1,1))]. given #115 (T,wt=18): 256 (g(x + y) + (x + (y + (x + y)')')')' = x. [para(26(a,1),8(a,1,1,1))]. given #116 (A,wt=19): 59 ((x + (y + z))' + (y + (z + x'))')' = y + z. [para(7(a,1),20(a,1,1,2,1))]. given #117 (T,wt=18): 311 (g(x + x') + (x + (g(x) + x')')')' = x. [para(31(a,1),8(a,1,1,1))]. given #118 (T,wt=18): 348 (g(x + y) + (x + (y + (y + x)')')')' = x. [para(254(a,1),8(a,1,1,1))]. given #119 (T,wt=18): 361 (g(x + y) + (x + (y + (y + x)))')' = x + y. [para(254(a,1),22(a,1,1,2)),rewrite([6(7)])]. given #120 (T,wt=18): 509 (g(g(x)) + (x + (x' + g(x)'))')' = g(x)'. [para(10(a,1),88(a,1,1,1,1)),rewrite([10(7),7(7),10(13)])]. given #121 (A,wt=20): 60 (x + ((y + x)' + (x + y')'')')' = (y + x)'. [para(20(a,1),8(a,1,1,1))]. given #122 (T,wt=18): 511 (g(x) + (g(x) + (x' + (x + x)'))')' = x'. [para(29(a,1),88(a,1,1,1,1)),rewrite([29(10),6(7),19(7),29(15)])]. given #123 (T,wt=18): 550 (x + (x + (g(x) + (g(x) + h(x)')))')' = g(x). [para(113(a,1),8(a,1,1,2)),rewrite([19(7),6(9)])]. given #124 (T,wt=18): 626 (x + (x + (h(x) + (h(x) + g(x)')))')' = h(x). [para(217(a,1),8(a,1,1,2)),rewrite([19(7),6(9)])]. given #125 (T,wt=18): 881 (h(x) + (x + (x + (h(x) + x'))'')')' = x. [para(837(a,1),8(a,1,1,1))]. given #126 (A,wt=21): 61 ((x + y)' + (x + ((z + y)' + (y + z')'))')' = x. [para(20(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #127 (T,wt=18): 1108 (x + (x + (x + (x + (g(x) + g(x)))))')' = g(x). [para(42(a,1),34(a,1,1,1)),rewrite([19(6),19(5),19(4)])]. given #128 (T,wt=18): 1350 ((x + y)' + (g(y) + (x + (y + y)'))')' = x. [para(29(a,1),36(a,1,1,2,1,2)),rewrite([6(9)])]. given #129 (T,wt=18): 1371 (g(x + y) + (y + (x + (x + y)')')')' = y. [para(26(a,1),36(a,1,1,1))]. given #130 (T,wt=18): 1378 (g(x + y) + (y + (x + (y + x)')')')' = y. [para(254(a,1),36(a,1,1,1))]. given #131 (A,wt=21): 63 (x + ((x + y')' + (x + y)'')')' = (x + y')'. [para(8(a,1),20(a,1,1,1))]. given #132 (T,wt=18): 1561 (g(x + y) + (y + (x + (y + x)))')' = y + x. [para(6(a,1),37(a,1,1,1,1))]. given #133 (T,wt=18): 1567 (g(x + y) + (x + (x + (y + y)))')' = x + y. [para(19(a,1),37(a,1,1,2,1,2))]. given #134 (T,wt=18): 1568 (g(x + y) + (y + (x + (x + y)))')' = x + y. [para(19(a,1),37(a,1,1,2,1))]. given #135 (T,wt=18): 1757 ((x + y)' + (g(x) + (y + (x + x)'))')' = y. [para(29(a,1),91(a,1,1,2,1,1)),rewrite([6(9)])]. given #136 (A,wt=21): 64 (((x + y)' + ((x + y')' + z))' + (z + x)')' = z. [para(8(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #137 (T,wt=18): 2202 ((x + y)' + ((y + y)' + (x + g(y)))')' = x. [para(29(a,1),1345(a,1,1,2,1,2)),rewrite([6(9)])]. given #138 (T,wt=18): 2678 ((x + y)' + ((x + x)' + (y + g(x)))')' = y. [para(29(a,1),1746(a,1,1,2,1,1)),rewrite([6(9)])]. given #139 (T,wt=18): 4333 (g(x + y) + (y + (y + (x + x)))')' = y + x. [para(19(a,1),1561(a,1,1,2,1,2))]. given #140 (T,wt=19): 70 ((x + (y + z))' + (x + (z + y'))')' = x + z. [para(19(a,1),20(a,1,1,1,1)),rewrite([7(6)])]. given #141 (A,wt=25): 65 (x + ((y + x)' + (x + y')'))' = g((y + x)' + (x + y')'). [para(20(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #142 (T,wt=19): 80 ((x + (y + z))' + (z' + (x + y))')' = x + y. [para(7(a,1),21(a,1,1,1,1))]. given #143 (T,wt=19): 85 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #144 (T,wt=14): 5499 (g(x + y) + h(y + x))' = y + x. [para(1561(a,1),85(a,1,1,2,1,2,2)),rewrite([6(9),19(9),19(8),19(7),6(6),19(10),19(9),19(8),19(7),19(6),6(5),963(11),1561(14)])]. given #145 (T,wt=14): 5521 (h(x + y) + g(y + x))' = x + y. [para(6(a,1),5499(a,1,1))]. given #146 (A,wt=21): 68 (h(x) + (x + (x + (g(x) + x')))')' = x + (x + g(x)). [para(12(a,1),20(a,1,1,1)),rewrite([7(6),7(5)])]. given #147 (T,wt=19): 92 ((x + (y + z))' + (x + (z' + y))')' = x + y. [para(19(a,1),21(a,1,1,2,1)),rewrite([7(2)])]. given #148 (T,wt=19): 99 (x + (y + (x + (x + y')'))')' = (x + y')'. [para(20(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #149 (T,wt=19): 101 (x + (x + (y + (y' + x)'))')' = (y' + x)'. [para(21(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #150 (T,wt=19): 127 ((x + (y + z))' + (y' + (x + z))')' = x + z. [para(19(a,1),56(a,1,1,1,1))]. given #151 (A,wt=20): 69 ((x + (x + (x + (g(x) + y))))' + (y + h(x))')' = y. [para(12(a,1),20(a,1,1,2,1,2)),rewrite([7(5),7(4),7(3)])]. given #152 (T,wt=19): 128 ((x + (y + z))' + (y + (x' + z))')' = y + z. [para(19(a,1),56(a,1,1,2,1))]. given #153 (T,wt=19): 136 (x + (y + (x + (y' + x)'))')' = (y' + x)'. [para(56(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #154 (T,wt=19): 141 ((x + (y + z'))' + (z + (x + y))')' = x + y. [para(7(a,1),57(a,1,1,1,1))]. given #155 (T,wt=19): 148 ((x + (y + z'))' + (x + (z + y))')' = x + y. [para(19(a,1),57(a,1,1,2,1)),rewrite([7(3)])]. given #156 (A,wt=21): 75 (x + (g(x)' + (x + x'')')')' = (x + x'')'. [para(27(a,1),20(a,1,1,1)),rewrite([6(7)])]. given #157 (T,wt=19): 161 ((x + (y + z))' + (z + (x + y'))')' = z + x. [para(6(a,1),22(a,1,1,1,1)),rewrite([7(2)])]. given #158 (T,wt=19): 162 ((x + (y + z))' + (y + (z' + x))')' = x + y. [para(6(a,1),22(a,1,1,2,1)),rewrite([7(6)])]. given #159 (T,wt=19): 173 ((x + (y + z))' + (y + (x + z'))')' = y + x. [para(19(a,1),22(a,1,1,1,1))]. given #160 (T,wt=19): 193 (g((x + y)' + (x + y')') + (x + x)')' = x. [para(8(a,1),66(a,1,1,2,1,1)),rewrite([8(14),8(18)])]. given #161 (A,wt=20): 76 ((g(x) + ((x + x'')' + y))' + (y + x)')' = y. [para(27(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #162 (T,wt=19): 202 (g((x + y)' + (y + x')') + (y + y)')' = y. [para(20(a,1),66(a,1,1,2,1,1)),rewrite([20(14),20(18)])]. given #163 (T,wt=19): 204 (g((x + y)' + (y' + x)') + (x + x)')' = x. [para(21(a,1),66(a,1,1,2,1,1)),rewrite([21(14),21(18)])]. given #164 (T,wt=19): 208 (g((x + y)' + (x' + y)') + (y + y)')' = y. [para(56(a,1),66(a,1,1,2,1,1)),rewrite([56(14),56(18)])]. given #165 (T,wt=19): 210 (g((x + y')' + (y + x)') + (x + x)')' = x. [para(57(a,1),66(a,1,1,2,1,1)),rewrite([57(14),57(18)])]. given #166 (A,wt=21): 77 (x + ((x + y')' + (y + x)'')')' = (x + y')'. [para(20(a,1),20(a,1,1,1))]. given #167 (T,wt=19): 227 ((x' + (y + z))' + (y + (z + x))')' = y + z. [para(7(a,1),79(a,1,1,2,1))]. given #168 (T,wt=19): 233 ((x + (y' + z))' + (x + (z + y))')' = x + z. [para(19(a,1),79(a,1,1,1,1)),rewrite([7(6)])]. given #169 (T,wt=19): 250 (g((x' + y)' + (y + x)') + (y + y)')' = y. [para(79(a,1),66(a,1,1,2,1,1)),rewrite([79(14),79(18)])]. given #170 (T,wt=19): 277 (g(x) + (x + (g(x) + (x + x)'')'')')' = x. [para(29(a,1),23(a,1,1,2,1,1)),rewrite([29(17)])]. given #171 (A,wt=21): 78 (((x + y)' + ((y + x')' + z))' + (z + y)')' = z. [para(20(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #172 (T,wt=19): 326 (g(x + x') + (x + (x + g(x)))')' = x + g(x). [para(31(a,1),22(a,1,1,2)),rewrite([6(2),6(8)])]. given #173 (T,wt=19): 484 (g(x) + (x + (x + (g(x) + x''))'')')' = x. [para(49(a,1),8(a,1,1,1))]. given #174 (T,wt=19): 506 (x'' + (x + (g(x') + x''))')' = g(x'). [para(88(a,1),8(a,1,1,2)),rewrite([19(6),6(10)])]. given #175 (T,wt=19): 570 (x + (x + (h(x) + (x + (x + g(x)))'))')' = h(x). [para(12(a,1),25(a,1,1,2,1,2,2)),rewrite([6(6),12(15)])]. Low Water (keep, True_semantics): wt=35 given #176 (A,wt=20): 81 (x + ((x + y)' + (y' + x)'')')' = (x + y)'. [para(21(a,1),8(a,1,1,1))]. given #177 (T,wt=19): 575 (g(x) + (x + (g(x) + (x + x'')''))')' = x. [para(27(a,1),25(a,1,1,2,1,2,2)),rewrite([6(8),19(9),27(19)])]. given #178 (T,wt=19): 784 ((x + x)' + g((x + y)' + (x + y')'))' = x. [para(30(a,1),79(a,1,1,2)),rewrite([8(7)])]. given #179 (T,wt=19): 1121 (g(x) + (g(x) + (x' + (x' + x')))')' = x'. [para(192(a,1),8(a,1,1,2)),rewrite([19(7),6(10)])]. given #180 (T,wt=19): 1254 (x' + (g(x) + (g(x) + (h(x) + x')))')' = g(x). [para(512(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #181 (A,wt=21): 82 ((x + y)' + (x + ((y + z)' + (z' + y)'))')' = x. [para(21(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #182 (T,wt=19): 1323 (x + (x + (g(x) + (g(x') + h(x'))))')' = g(x). [para(682(a,1),8(a,1,1,2)),rewrite([19(8),6(10)])]. given #183 (T,wt=19): 1514 (x + (x + (x + (h(x) + (h(x) + x'))))')' = h(x). [para(883(a,1),8(a,1,1,2)),rewrite([19(7),19(6),6(9)])]. given #184 (T,wt=19): 1666 (g(x + x') + (x' + (x + g(x))')')' = x'. [para(31(a,1),58(a,1,1,1))]. given #185 (T,wt=19): 1686 ((x + x)' + (x + (g(x)' + (x + x)'))')' = x. [para(71(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #186 (A,wt=21): 84 ((x + ((y + z)' + (y + z')'))' + (y + x)')' = x. [para(8(a,1),21(a,1,1,2,1,1))]. given #187 (T,wt=19): 1709 (g(x) + (x + (g(x') + (x' + x')'))')' = x. [para(10(a,1),39(a,1,1,1))]. given #188 (T,wt=19): 2069 (g(x) + (x + (g(x) + (g(h(x)) + h(h(x)))))')' = x. [para(687(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #189 (T,wt=19): 2093 (h(x) + (x + (g(g(x)) + (h(x) + h(g(x)))))')' = x. [para(922(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #190 (T,wt=19): 3351 ((x + (y + z))' + (z + (y + x'))')' = z + y. [para(6(a,1),59(a,1,1,1,1,2))]. Low Water (keep, True_semantics): wt=34 given #191 (A,wt=25): 86 (x + ((x + y)' + (y' + x)'))' = g((x + y)' + (y' + x)'). [para(21(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #192 (T,wt=19): 3352 ((x + (y + z))' + (z + (x' + y))')' = y + z. [para(6(a,1),59(a,1,1,2,1)),rewrite([7(6)])]. given #193 (T,wt=19): 4915 ((x + (y + z))' + (x + (y' + z))')' = x + z. [para(6(a,1),70(a,1,1,2,1,2))]. given #194 (T,wt=19): 4916 ((x + (y + z))' + (z + (y' + x))')' = x + z. [para(6(a,1),70(a,1,1,2,1)),rewrite([7(6)])]. given #195 (T,wt=19): 5092 ((x + x)' + g((y + x)' + (x + y')'))' = x. [para(65(a,1),79(a,1,1,2)),rewrite([20(7)])]. given #196 (A,wt=20): 89 ((x + (y + (y + (y + g(y)))))' + (h(y) + x)')' = x. [para(12(a,1),21(a,1,1,2,1,1))]. given #197 (T,wt=19): 5099 ((x + (y + z))' + (y' + (z + x))')' = z + x. [para(6(a,1),80(a,1,1,1,1)),rewrite([7(2)])]. given #198 (T,wt=19): 5100 ((x + (y + z))' + (z' + (y + x))')' = x + y. [para(6(a,1),80(a,1,1,2,1,2))]. Low Water (keep, True_semantics): wt=33 given #199 (T,wt=19): 6214 ((x + (y + z))' + (x' + (z + y))')' = z + y. [para(6(a,1),127(a,1,1,1,1)),rewrite([7(2)])]. given #200 (T,wt=19): 6215 ((x' + (y + z))' + (y + (x + z))')' = y + z. [para(6(a,1),127(a,1,1))]. given #201 (A,wt=27): 90 (h(x') + (x + (x' + (x' + g(x'))))')' = x' + (x' + g(x')). [para(12(a,1),21(a,1,1,2)),rewrite([6(7),6(11)])]. given #202 (T,wt=19): 6438 ((x + (y' + z))' + (y + (x + z))')' = x + z. [para(6(a,1),128(a,1,1))]. given #203 (T,wt=19): 6802 ((x + (y' + z))' + (y + (z + x))')' = z + x. [para(6(a,1),141(a,1,1,1,1)),rewrite([7(3)])]. given #204 (T,wt=19): 6803 ((x + (y + z'))' + (z + (y + x))')' = x + y. [para(6(a,1),141(a,1,1,2,1,2))]. given #205 (T,wt=19): 6964 ((x + (y' + z))' + (z + (y + x))')' = z + x. [para(6(a,1),148(a,1,1,1,1)),rewrite([7(3)])]. given #206 (A,wt=20): 95 ((x + (g(y) + (y + y'')'))' + (y + x)')' = x. [para(27(a,1),21(a,1,1,2,1,1))]. given #207 (T,wt=19): 6971 ((x + (y + z'))' + (y + (z + x))')' = y + x. [para(19(a,1),148(a,1,1,1,1))]. given #208 (T,wt=19): 7359 ((x + (y' + z))' + (z + (x + y))')' = z + x. [para(6(a,1),162(a,1,1))]. given #209 (T,wt=19): 7561 ((x + (y + z'))' + (y + (x + z))')' = x + y. [para(6(a,1),173(a,1,1))]. given #210 (T,wt=19): 8317 ((x + x)' + g((x + y)' + (y' + x)'))' = x. [para(6(a,1),204(a,1,1))]. given #211 (A,wt=21): 96 (x + ((y' + x)' + (x + y)'')')' = (y' + x)'. [para(21(a,1),20(a,1,1,1))]. given #212 (T,wt=19): 8516 ((x + x)' + g((y + x)' + (y' + x)'))' = x. [para(6(a,1),208(a,1,1))]. given #213 (T,wt=19): 8718 ((x + x)' + g((x + y')' + (y + x)'))' = x. [para(6(a,1),210(a,1,1))]. given #214 (T,wt=19): 9092 ((x' + (y + z))' + (z + (y + x))')' = z + y. [para(6(a,1),227(a,1,1,1,1,2))]. given #215 (T,wt=19): 9093 ((x' + (y + z))' + (z + (x + y))')' = y + z. [para(6(a,1),227(a,1,1,2,1)),rewrite([7(6)])]. given #216 (A,wt=21): 97 (((x + y)' + ((y' + x)' + z))' + (z + x)')' = z. [para(21(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #217 (T,wt=19): 9464 ((x + x)' + g((y' + x)' + (x + y)'))' = x. [para(6(a,1),250(a,1,1))]. given #218 (T,wt=19): 13041 ((x' + (y + z))' + (x + (z + y))')' = y + z. [para(6(a,1),6214(a,1,1))]. Low Water (keep, True_semantics): wt=32 given #219 (T,wt=20): 120 (x + ((y + x)' + (y' + x)'')')' = (y + x)'. [para(56(a,1),8(a,1,1,1))]. given #220 (T,wt=20): 126 ((x + (x + (x + (g(x) + y))))' + (h(x) + y)')' = y. [para(12(a,1),56(a,1,1,2,1,1)),rewrite([7(5),7(4),7(3)])]. given #221 (A,wt=21): 98 ((x + ((y + z)' + (z + y')'))' + (z + x)')' = x. [para(20(a,1),21(a,1,1,2,1,1))]. given #222 (T,wt=20): 131 ((x + y)' + (g(x) + ((x + x'')' + y))')' = y. [para(27(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #223 (T,wt=20): 147 ((x + h(y))' + (y + (y + (y + (g(y) + x))))')' = x. [para(12(a,1),57(a,1,1,1,1,2)),rewrite([7(8),7(7),7(6)])]. given #224 (T,wt=20): 151 ((x + y)' + (g(y) + ((y + y'')' + x))')' = x. [para(27(a,1),57(a,1,1,1,1,2)),rewrite([7(9)])]. given #225 (T,wt=20): 196 (g(x + (x + (x + g(x)))) + (h(x) + h(x))')' = h(x). [para(12(a,1),66(a,1,1,2,1,1)),rewrite([12(11),12(16)])]. given #226 (A,wt=21): 100 ((x + ((y + z)' + (z' + y)'))' + (y + x)')' = x. [para(21(a,1),21(a,1,1,2,1,1))]. given #227 (T,wt=20): 232 ((h(x) + y)' + (y + (x + (x + (x + g(x)))))')' = y. [para(12(a,1),79(a,1,1,1,1,1))]. given #228 (T,wt=20): 237 ((x + y)' + (y + (g(x) + (x + x'')'))')' = y. [para(27(a,1),79(a,1,1,1,1,1))]. given #229 (T,wt=20): 255 (x + (y + (z + (x + (y + z))')))' = g(x + (y + z)). [para(7(a,1),26(a,1,1,2,2,1)),rewrite([7(6),7(9)])]. given #230 (T,wt=20): 259 (x + (y + (z + (y + (x + z))')))' = g(x + (y + z)). [para(19(a,1),26(a,1,1,2,2,1)),rewrite([7(5)])]. given #231 (A,wt=23): 102 (x + (y + (x + (y + (x + (y + g(x + y)))))'))' = g(x + y). [para(7(a,1),40(a,1,1,2,1,2)),rewrite([19(7),19(6),7(5),7(9)])]. given #232 (T,wt=20): 342 ((x + x)' + g(g(g(x) + h(x)) + (x + x)'))' = x. [para(198(a,1),66(a,1,1,2,1,1)),rewrite([198(16),6(11),198(20)])]. given #233 (T,wt=20): 346 (x + (y + (z + (y + (z + x))')))' = g(x + (y + z)). [para(7(a,1),254(a,1,1,2,2,1)),rewrite([7(5)])]. given #234 (T,wt=20): 347 (x + (y + (z + (z + (x + y))')))' = g(x + (y + z)). [para(7(a,1),254(a,1,1)),rewrite([7(9)])]. given #235 (T,wt=20): 351 (x + (y + (z + (x + (z + y))')))' = g(x + (y + z)). [para(19(a,1),254(a,1,1,2,2,1)),rewrite([7(6),7(9)])]. given #236 (A,wt=21): 104 ((x + g(y))' + (x + (y + (y + (y + g(y)))'))')' = x. [para(40(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #237 (T,wt=20): 359 (g(x + y) + (x + (y + (y + x)''))')' = x + y. [para(254(a,1),22(a,1,1,1))]. given #238 (T,wt=20): 513 (g(x) + (g(x) + (x' + (x + x'')'))')' = x'. [para(27(a,1),88(a,1,1,1,1)),rewrite([27(14),6(9),19(9),27(19)])]. given #239 (T,wt=20): 549 (x + (g(x) + (x + (g(x) + h(x)'))'')')' = g(x). [para(113(a,1),8(a,1,1,1))]. given #240 (T,wt=20): 566 ((x + y)' + (x + (x + (y' + (x + y)')))')' = x. [para(25(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #241 (A,wt=24): 105 (x + (g(x) + (x + (x + g(x)))'))' = g(x + (x + (x + g(x)))'). [para(40(a,1),10(a,1,1,2)),rewrite([6(7),19(7)])]. given #242 (T,wt=20): 584 (x + (x + (g(x) + (x + (x + g(x)))''))')' = g(x). [para(40(a,1),25(a,1,1,2,1,2,2)),rewrite([6(7),40(17)])]. given #243 (T,wt=20): 586 (x + (x + (g(x) + (g(x) + h(x)')''))')' = g(x). [para(43(a,1),25(a,1,1,2,1,2,2)),rewrite([6(8),43(19)])]. given #244 (T,wt=20): 599 (x + (x + (h(x) + (h(x) + g(x)')''))')' = h(x). [para(73(a,1),25(a,1,1,2,1,2,2)),rewrite([6(8),73(19)])]. given #245 (T,wt=20): 625 (x + (h(x) + (x + (h(x) + g(x)'))'')')' = h(x). [para(217(a,1),8(a,1,1,1))]. given #246 (A,wt=23): 106 (g(x) + (x' + (x + (x + g(x)))')')' = (x + (x + g(x)))'. [para(40(a,1),20(a,1,1,1)),rewrite([6(7)])]. given #247 (T,wt=20): 1107 ((x + h(y))' + (y + (x + (y + (y + g(y)))))')' = x. [para(19(a,1),34(a,1,1,2,1))]. given #248 (T,wt=20): 1351 ((x + y)' + (g(y) + (x + (y + y'')'))')' = x. [para(27(a,1),36(a,1,1,2,1,2)),rewrite([6(11)])]. given #249 (T,wt=20): 1385 (g(g(x) + h(x)) + (g(x) + (x + h(x))')')' = g(x). [para(45(a,1),36(a,1,1,1))]. given #250 (T,wt=20): 1672 (g(g(x) + h(x)) + (h(x) + (x + g(x))')')' = h(x). [para(45(a,1),58(a,1,1,1))]. given #251 (A,wt=21): 107 ((x + ((x + (x + g(x)))' + y))' + (y + g(x))')' = y. [para(40(a,1),20(a,1,1,2,1,2)),rewrite([7(6)])]. given #252 (T,wt=20): 1713 (x + (g(x) + (g(h(x)) + (h(x) + h(x))'))')' = g(x). [para(42(a,1),39(a,1,1,1))]. given #253 (T,wt=20): 1754 ((x + (y + (x + (x + g(x)))))' + (h(x) + y)')' = y. [para(12(a,1),91(a,1,1,2,1,1))]. given #254 (T,wt=20): 1758 ((x + y)' + (g(x) + (y + (x + x'')'))')' = y. [para(27(a,1),91(a,1,1,2,1,1)),rewrite([6(11)])]. given #255 (T,wt=20): 1964 ((h(x) + y)' + (x + (y + (x + (x + g(x)))))')' = y. [para(12(a,1),234(a,1,1,1,1,1))]. given #256 (A,wt=21): 108 ((x + (y + (y + (y + g(y)))'))' + (g(y) + x)')' = x. [para(40(a,1),21(a,1,1,2,1,1))]. given #257 (T,wt=20): 2004 (x + (x + (g(x) + (g(x) + (x + x)'')))')' = g(x). [para(369(a,1),8(a,1,1,2)),rewrite([19(8),6(10)])]. given #258 (T,wt=20): 2023 (g(x + y) + (y + (x + (y + x)''))')' = y + x. [para(6(a,1),46(a,1,1,1,1))]. given #259 (T,wt=20): 2028 (g(x + y) + (y + (x + (x + y)''))')' = x + y. [para(19(a,1),46(a,1,1,2,1))]. given #260 (T,wt=20): 2046 (x + (x + (x + (g(x) + (g(x) + x''))))')' = g(x). [para(485(a,1),8(a,1,1,2)),rewrite([19(8),19(7),6(10)])]. given #261 (A,wt=29): 109 (g(x') + (x + (x' + (x' + g(x')))')')' = (x' + (x' + g(x')))'. [para(40(a,1),21(a,1,1,2)),rewrite([6(8),6(12)])]. given #262 (T,wt=20): 2199 ((x + (x + (g(x) + (y + x))))' + (y + h(x))')' = y. [para(12(a,1),1345(a,1,1,2,1,2)),rewrite([7(5),7(4)])]. given #263 (T,wt=20): 2204 ((x + y)' + ((y + y'')' + (x + g(y)))')' = x. [para(27(a,1),1345(a,1,1,2,1,2)),rewrite([6(11)])]. given #264 (T,wt=20): 2674 ((x + (x + (g(x) + (y + x))))' + (h(x) + y)')' = y. [para(12(a,1),1746(a,1,1,2,1,1)),rewrite([7(5),7(4)])]. given #265 (T,wt=20): 2679 ((x + y)' + ((x + x'')' + (y + g(x)))')' = y. [para(27(a,1),1746(a,1,1,2,1,1)),rewrite([6(11)])]. given #266 (A,wt=21): 110 (x + (y + (g(x + y) + h(x + y)')'))' = g(x + y). [para(7(a,1),43(a,1,1))]. given #267 (T,wt=20): 2824 ((x + h(y))' + (y + (y + (g(y) + (x + y))))')' = x. [para(12(a,1),1919(a,1,1,1,1,2)),rewrite([7(8),7(7)])]. given #268 (T,wt=20): 2860 ((h(x) + y)' + (x + (x + (g(x) + (y + x))))')' = y. [para(12(a,1),1959(a,1,1,1,1,1)),rewrite([7(8),7(7)])]. given #269 (T,wt=20): 2892 ((x + y)' + (y + (y + (x' + (x + y)')))')' = y. [para(62(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #270 (T,wt=20): 3022 ((x + y)' + (x + (y' + (x + (x + y)')))')' = x. [para(83(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #271 (A,wt=21): 112 ((x + g(y))' + (x + (y + (g(y) + h(y)')'))')' = x. [para(43(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])]. given #272 (T,wt=20): 3054 ((x + y)' + (y' + (x + (x + (x + y)')))')' = x. [para(83(a,1),36(a,1,1,2)),rewrite([6(10)])]. given #273 (T,wt=20): 3073 (x + (g(g(x)) + (h(x) + (g(x) + g(x))'))')' = h(x). [para(42(a,1),93(a,1,1,2)),rewrite([19(9),6(11)])]. given #274 (T,wt=20): 3134 ((x + y)' + (y + (x' + (y + (x + y)')))')' = y. [para(122(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #275 (T,wt=20): 3172 ((x + y)' + (x' + (y + (y + (x + y)')))')' = y. [para(122(a,1),36(a,1,1,2)),rewrite([6(10)])]. given #276 (A,wt=24): 114 (x + (g(x) + (g(x) + h(x)')'))' = g(x + (g(x) + h(x)')'). [para(43(a,1),10(a,1,1,2)),rewrite([6(8),19(8)])]. given #277 (T,wt=20): 3721 (g(x) + (x + (x + (g(x) + (g(x) + h(x)'))))')' = x. [para(550(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #278 (T,wt=20): 3744 (h(x) + (x + (x + (h(x) + (h(x) + g(x)'))))')' = x. [para(626(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #279 (T,wt=20): 3987 (g(x) + (x + (x + (x + (x + (g(x) + g(x))))))')' = x. [para(1108(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #280 (T,wt=20): 5522 (g(x + (y + z)) + h(z + (x + y)))' = z + (x + y). [para(7(a,1),5499(a,1,1,1,1))]. given #281 (A,wt=23): 115 (g(x) + (x' + (g(x) + h(x)')')')' = (g(x) + h(x)')'. [para(43(a,1),20(a,1,1,1)),rewrite([6(8)])]. given #282 (T,wt=20): 5523 (g(x + (y + z)) + h(y + (z + x)))' = y + (z + x). [para(7(a,1),5499(a,1,1,2,1)),rewrite([7(10)])]. given #283 (T,wt=20): 5527 (g(x + (y + z)) + h(x + (z + y)))' = x + (z + y). [para(19(a,1),5499(a,1,1,1,1)),rewrite([7(5),7(10)])]. given #284 (T,wt=20): 5603 (h(x + (y + z)) + g(z + (x + y)))' = x + (y + z). [para(7(a,1),5521(a,1,1,1,1)),rewrite([7(10)])]. given #285 (T,wt=20): 5604 (h(x + (y + z)) + g(y + (z + x)))' = x + (y + z). [para(7(a,1),5521(a,1,1,2,1))]. given #286 (A,wt=21): 116 ((x + ((g(x) + h(x)')' + y))' + (y + g(x))')' = y. [para(43(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #287 (T,wt=20): 5605 (h(x + (y + z)) + g(x + (z + y)))' = y + (x + z). [para(19(a,1),5521(a,1,1,1,1)),rewrite([7(5)])]. given #288 (T,wt=20): 6403 ((x + (x + (x + (y + g(x)))))' + (y + h(x))')' = y. [para(6(a,1),69(a,1,1,1,1,2,2,2))]. given #289 (T,wt=20): 15320 ((x + (x + (x + (y + g(x)))))' + (h(x) + y)')' = y. [para(6(a,1),126(a,1,1,1,1,2,2,2))]. given #290 (T,wt=20): 15429 ((x + h(y))' + (y + (y + (y + (x + g(y)))))')' = x. [para(6(a,1),147(a,1,1,2,1,2,2,2))]. given #291 (A,wt=21): 117 ((x + (y + (g(y) + h(y)')'))' + (g(y) + x)')' = x. [para(43(a,1),21(a,1,1,2,1,1))]. given #292 (T,wt=19): 16707 (x + (x + (h(x) + (g(x) + h(x)')'))')' = h(x). [para(42(a,1),117(a,1,1,2)),rewrite([19(8),6(10)])]. given #293 (T,wt=20): 15584 (x + (y + (z + (z + (y + x))')))' = g(x + (y + z)). [para(19(a,1),346(a,1,1,2,2,2,1))]. given #294 (T,wt=20): 15726 ((x + y)' + (y + (y + (x' + (y + x)')))')' = y. [para(6(a,1),566(a,1,1,1,1))]. given #295 (T,wt=20): 15727 ((x + y)' + (x + (x + (y' + (y + x)')))')' = x. [para(6(a,1),566(a,1,1,2,1,2,2,2,1))]. given #296 (A,wt=27): 118 (g(x') + (x + (g(x') + h(x')')')')' = (g(x') + h(x')')'. [para(43(a,1),21(a,1,1,2)),rewrite([6(8),6(12)])]. given #297 (T,wt=20): 15898 ((x + h(y))' + (y + (y + (x + (y + g(y)))))')' = x. [para(19(a,1),1107(a,1,1,2,1,2))]. given #298 (T,wt=20): 16016 ((x + (x + (y + (x + g(x)))))' + (h(x) + y)')' = y. [para(19(a,1),1754(a,1,1,1,1,2))]. given #299 (T,wt=20): 16068 ((h(x) + y)' + (x + (x + (y + (x + g(x)))))')' = y. [para(19(a,1),1964(a,1,1,2,1,2))]. given #300 (T,wt=20): 16336 ((x + y)' + (y + (x' + (y + (y + x)')))')' = y. [para(6(a,1),3022(a,1,1,1,1))]. given #301 (A,wt=21): 121 ((x + y)' + (x + ((z + y)' + (z' + y)'))')' = x. [para(56(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #302 (T,wt=20): 16337 ((x + y)' + (x + (y' + (x + (y + x)')))')' = x. [para(6(a,1),3022(a,1,1,2,1,2,2,2,1))]. given #303 (T,wt=20): 16369 ((x + y)' + (x' + (y + (y + (y + x)')))')' = y. [para(6(a,1),3054(a,1,1,1,1))]. given #304 (T,wt=20): 16370 ((x + y)' + (y' + (x + (x + (y + x)')))')' = x. [para(6(a,1),3054(a,1,1,2,1,2,2,2,1))]. given #305 (T,wt=20): 16518 (g(x + (y + z)) + h(y + (x + z)))' = y + (x + z). [para(6(a,1),5522(a,1,1,1,1,2))]. given #306 (A,wt=21): 123 ((x + y)' + ((x + z)' + ((x + z')' + y))')' = y. [para(8(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #307 (T,wt=20): 16519 (g(x + (y + z)) + h(z + (y + x)))' = z + (x + y). [para(6(a,1),5522(a,1,1,2,1,2))]. given #308 (T,wt=20): 16596 (h(x + (y + z)) + g(y + (x + z)))' = x + (z + y). [para(6(a,1),5603(a,1,1,1,1,2))]. given #309 (T,wt=20): 16597 (h(x + (y + z)) + g(z + (y + x)))' = x + (y + z). [para(6(a,1),5603(a,1,1,2,1,2))]. given #310 (T,wt=20): 16673 ((h(x) + y)' + (x + (x + (x + (y + g(x)))))')' = y. [para(6(a,1),15320(a,1,1))]. Low Water (keep, True_semantics): wt=31 given #311 (A,wt=25): 124 (x + ((y + x)' + (y' + x)'))' = g((y + x)' + (y' + x)'). [para(56(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #312 (T,wt=21): 132 (x + ((y' + x)' + (y + x)'')')' = (y' + x)'. [para(56(a,1),20(a,1,1,1))]. given #313 (T,wt=21): 133 (((x + y)' + ((x' + y)' + z))' + (z + y)')' = z. [para(56(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #314 (T,wt=21): 134 ((x + y)' + ((z + x)' + ((x + z')' + y))')' = y. [para(20(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #315 (T,wt=21): 135 ((x + ((y + z)' + (y' + z)'))' + (z + x)')' = x. [para(56(a,1),21(a,1,1,2,1,1))]. given #316 (A,wt=21): 137 ((x + y)' + ((x + z)' + ((z' + x)' + y))')' = y. [para(21(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #317 (T,wt=21): 138 ((g(x) + y)' + (x + ((x + (x + g(x)))' + y))')' = y. [para(40(a,1),56(a,1,1,2,1,1)),rewrite([7(6),6(11)])]. given #318 (T,wt=21): 139 ((g(x) + y)' + (x + ((g(x) + h(x)')' + y))')' = y. [para(43(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(12)])]. given #319 (T,wt=21): 140 ((x + y)' + ((z + x)' + ((z' + x)' + y))')' = y. [para(56(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #320 (T,wt=21): 143 ((x + y)' + (x + ((y + z')' + (z + y)'))')' = x. [para(57(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #321 (A,wt=21): 144 ((x + y)' + ((y + z)' + ((y + z')' + x))')' = x. [para(8(a,1),57(a,1,1,1,1,2)),rewrite([7(9)])]. given #322 (T,wt=21): 152 (((x + y')' + ((y + x)' + z))' + (z + x)')' = z. [para(57(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #323 (T,wt=21): 153 ((x + y)' + ((z + y)' + ((y + z')' + x))')' = x. [para(20(a,1),57(a,1,1,1,1,2)),rewrite([7(9)])]. given #324 (T,wt=21): 154 ((x + ((y + z')' + (z + y)'))' + (y + x)')' = x. [para(57(a,1),21(a,1,1,2,1,1))]. given #325 (T,wt=21): 155 ((x + y)' + ((y + z)' + ((z' + y)' + x))')' = x. [para(21(a,1),57(a,1,1,1,1,2)),rewrite([7(9)])]. given #326 (A,wt=25): 145 (x + ((x + y')' + (y + x)'))' = g((x + y')' + (y + x)'). [para(57(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #327 (T,wt=21): 156 ((x + g(y))' + (y + ((y + (y + g(y)))' + x))')' = x. [para(40(a,1),57(a,1,1,1,1,2)),rewrite([7(9)])]. given #328 (T,wt=21): 157 ((x + g(y))' + (y + ((g(y) + h(y)')' + x))')' = x. [para(43(a,1),57(a,1,1,1,1,2)),rewrite([7(10)])]. given #329 (T,wt=21): 158 ((x + y)' + ((x + z')' + ((z + x)' + y))')' = y. [para(57(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #330 (T,wt=21): 159 ((x + y)' + ((z + y)' + ((z' + y)' + x))')' = x. [para(56(a,1),57(a,1,1,1,1,2)),rewrite([7(9)])]. given #331 (A,wt=21): 160 ((x + y)' + ((y + z')' + ((z + y)' + x))')' = x. [para(57(a,1),57(a,1,1,1,1,2)),rewrite([7(9)])]. given #332 (T,wt=21): 191 ((x + y')' + (x + (g(y) + (y' + y')'))')' = x. [para(66(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])]. given #333 (T,wt=18): 17830 (g(x) + (x + (g(x) + (x' + x')'))')' = x. [para(10(a,1),191(a,1,1,1))]. given #334 (T,wt=21): 201 ((g(x) + ((x' + x')' + y))' + (y + x')')' = y. [para(66(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #335 (T,wt=21): 203 ((x + (g(y) + (y' + y')'))' + (y' + x)')' = x. [para(66(a,1),21(a,1,1,2,1,1))]. given #336 (A,wt=25): 163 ((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 #337 (T,wt=20): 17994 (h(x) + (x + (x + (x + g(x)')))')' = x + (x + x). [para(12(a,1),163(a,1,1,1))]. given #338 (T,wt=21): 205 (g(x + (x + (x + g(x)))') + (g(x) + g(x))')' = g(x). [para(40(a,1),66(a,1,1,2,1,1)),rewrite([40(13),40(18)])]. given #339 (T,wt=21): 206 ((g(x) + g(x))' + g(x + (g(x) + h(x)')'))' = g(x). [para(43(a,1),66(a,1,1,2,1,1)),rewrite([43(15),6(12),43(20)])]. given #340 (T,wt=21): 207 ((x' + y)' + (g(x) + ((x' + x')' + y))')' = y. [para(66(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(12)])]. given #341 (A,wt=28): 164 (x + (y + ((x + (y + z))' + (x + (y + z'))'')'))' = (x + (y + z))'. [para(22(a,1),8(a,1,1,1)),rewrite([7(12)])]. given #342 (T,wt=21): 209 ((x + y')' + (g(y) + ((y' + y')' + x))')' = x. [para(66(a,1),57(a,1,1,1,1,2)),rewrite([7(10)])]. given #343 (T,wt=21): 213 ((x' + x')' + g(g(x) + (x' + x')'))' = x'. [para(66(a,1),66(a,1,1,2,1,1)),rewrite([66(15),6(12),66(20)])]. given #344 (T,wt=21): 214 (x + (y + (h(x + y) + g(x + y)')'))' = h(x + y). [para(7(a,1),73(a,1,1))]. given #345 (T,wt=21): 216 ((x + h(y))' + (x + (y + (h(y) + g(y)')'))')' = x. [para(73(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])]. given #346 (A,wt=27): 165 ((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 #347 (T,wt=19): 18209 (x + (x + (g(x) + (h(x) + g(x)')'))')' = g(x). [para(42(a,1),216(a,1,1,1)),rewrite([19(8)])]. given #348 (T,wt=21): 220 ((x + ((h(x) + g(x)')' + y))' + (y + h(x))')' = y. [para(73(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #349 (T,wt=21): 221 ((x + (y + (h(y) + g(y)')'))' + (h(y) + x)')' = x. [para(73(a,1),21(a,1,1,2,1,1))]. given #350 (T,wt=21): 223 ((h(x) + y)' + (x + ((h(x) + g(x)')' + y))')' = y. [para(73(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(12)])]. given #351 (A,wt=26): 166 (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 #352 (T,wt=21): 224 ((x + h(y))' + (y + ((h(y) + g(y)')' + x))')' = x. [para(73(a,1),57(a,1,1,1,1,2)),rewrite([7(10)])]. given #353 (T,wt=21): 226 ((h(x) + h(x))' + g(x + (h(x) + g(x)')'))' = h(x). [para(73(a,1),66(a,1,1,2,1,1)),rewrite([73(15),6(12),73(20)])]. given #354 (T,wt=21): 228 ((x + y)' + (x + ((z' + y)' + (y + z)'))')' = x. [para(79(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #355 (T,wt=21): 229 ((x + y)' + (y + ((x + z)' + (x + z')'))')' = y. [para(8(a,1),79(a,1,1,1,1,1))]. given #356 (A,wt=27): 167 ((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 #357 (T,wt=21): 238 (((x' + y)' + ((y + x)' + z))' + (z + y)')' = z. [para(79(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #358 (T,wt=21): 239 ((x + y)' + (y + ((z + x)' + (x + z')'))')' = y. [para(20(a,1),79(a,1,1,1,1,1))]. given #359 (T,wt=21): 240 ((x + ((y' + z)' + (z + y)'))' + (z + x)')' = x. [para(79(a,1),21(a,1,1,2,1,1))]. given #360 (T,wt=21): 241 ((x + y)' + (y + ((x + z)' + (z' + x)'))')' = y. [para(21(a,1),79(a,1,1,1,1,1))]. given #361 (A,wt=35): 168 (x + (y + ((x + (y + z))' + (x + (y + z'))')))' = g((x + (y + z))' + (x + (y + z'))'). [para(22(a,1),10(a,1,1,2)),rewrite([6(10),7(10)])]. given #362 (T,wt=21): 242 ((g(x) + y)' + (y + (x + (x + (x + g(x)))'))')' = y. [para(40(a,1),79(a,1,1,1,1,1))]. given #363 (T,wt=21): 243 ((g(x) + y)' + (y + (x + (g(x) + h(x)')'))')' = y. [para(43(a,1),79(a,1,1,1,1,1))]. given #364 (T,wt=21): 244 ((x + y)' + ((z' + x)' + ((x + z)' + y))')' = y. [para(79(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #365 (T,wt=21): 245 ((x + y)' + (y + ((z + x)' + (z' + x)'))')' = y. [para(56(a,1),79(a,1,1,1,1,1))]. given #366 (A,wt=22): 169 ((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 #367 (T,wt=21): 246 ((x + y)' + ((z' + y)' + ((y + z)' + x))')' = x. [para(79(a,1),57(a,1,1,1,1,2)),rewrite([7(9)])]. given #368 (T,wt=21): 247 ((x + y)' + (y + ((x + z')' + (z + x)'))')' = y. [para(57(a,1),79(a,1,1,1,1,1))]. given #369 (T,wt=21): 251 ((x' + y)' + (y + (g(x) + (x' + x')'))')' = y. [para(66(a,1),79(a,1,1,1,1,1))]. given #370 (T,wt=21): 252 ((h(x) + y)' + (y + (x + (h(x) + g(x)')'))')' = y. [para(73(a,1),79(a,1,1,1,1,1))]. given #371 (A,wt=26): 171 ((x + (y + h(z)))' + (x + (y + (z + (z + (z + g(z))))))')' = x + y. [para(12(a,1),22(a,1,1,2,1,2,2)),rewrite([6(12)])]. given #372 (T,wt=21): 253 ((x + y)' + (y + ((z' + x)' + (x + z)'))')' = y. [para(79(a,1),79(a,1,1,1,1,1))]. given #373 (T,wt=21): 280 (g(x) + (x + (g(x) + (x + x'')'')'')')' = x. [para(27(a,1),23(a,1,1,2,1,1)),rewrite([27(21)])]. given #374 (T,wt=21): 324 (g(x + x') + (x + (g(x) + x''))')' = x + g(x). [para(31(a,1),22(a,1,1,1))]. given #375 (T,wt=21): 334 (x + (x + (x + g(g(x) + h(x))))')' = g(g(x) + h(x)). [para(198(a,1),8(a,1,1,2)),rewrite([6(6),7(6),6(8)])]. given #376 (A,wt=23): 172 ((x + (y + (z + u)))' + (x + (z + (y + u)'))')' = x + z. [para(19(a,1),22(a,1,1,1,1,2))]. given #377 (T,wt=21): 336 (x + ((x + x)' + g(g(x) + h(x))')')' = (x + x)'. [para(198(a,1),20(a,1,1,1))]. given #378 (T,wt=21): 387 (g(x) + (x + ((x' + y)' + (x' + y')'))')' = x. [para(10(a,1),24(a,1,1,1))]. given #379 (T,wt=21): 393 ((x + y)' + ((y + z)' + (x + (y + z')'))')' = x. [para(19(a,1),24(a,1,1,2,1))]. given #380 (T,wt=21): 504 (x'' + (g(x') + (x + x'')'')')' = g(x'). [para(88(a,1),8(a,1,1,1))]. given #381 (A,wt=24): 174 ((x + (y + z))' + (x + (y + (g(z) + (z + z)')))')' = x + y. [para(29(a,1),22(a,1,1,2,1,2,2)),rewrite([6(11)])]. given #382 (T,wt=21): 507 (g(x) + (x' + ((x + y)' + (x + y')'))')' = x'. [para(8(a,1),88(a,1,1,1,1)),rewrite([8(14),6(9),8(19)])]. given #383 (T,wt=21): 516 (g(x) + (x' + ((y + x)' + (x + y')'))')' = x'. [para(20(a,1),88(a,1,1,1,1)),rewrite([20(14),6(9),20(19)])]. given #384 (T,wt=21): 518 (g(x) + (x' + ((x + y)' + (y' + x)'))')' = x'. [para(21(a,1),88(a,1,1,1,1)),rewrite([21(14),6(9),21(19)])]. given #385 (T,wt=21): 522 (g(x) + (x' + ((y + x)' + (y' + x)'))')' = x'. [para(56(a,1),88(a,1,1,1,1)),rewrite([56(14),6(9),56(19)])]. Low Water (keep, True_semantics): wt=30 given #386 (A,wt=22): 175 ((x + (y + z))' + (x + (y + (g(z) + h(z))))')' = x + y. [para(42(a,1),22(a,1,1,2,1,2,2)),rewrite([6(10)])]. given #387 (T,wt=21): 524 (g(x) + (x' + ((x + y')' + (y + x)'))')' = x'. [para(57(a,1),88(a,1,1,1,1)),rewrite([57(14),6(9),57(19)])]. given #388 (T,wt=21): 531 (g(x) + (x' + ((y' + x)' + (x + y)'))')' = x'. [para(79(a,1),88(a,1,1,1,1)),rewrite([79(14),6(9),79(19)])]. given #389 (T,wt=21): 557 ((x + x)' + g(g(x) + (x + (g(x) + h(x)'))'))' = x. [para(113(a,1),66(a,1,1,2,1,1)),rewrite([113(18),6(12),113(22)])]. given #390 (T,wt=21): 597 (g(x) + (g(x) + (x' + (x' + x')''))')' = x'. [para(66(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),66(20)])]. given #391 (A,wt=26): 176 ((x + (y + z))' + (x + (y + (g(z) + (z + z'')')))')' = x + y. [para(27(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #392 (T,wt=21): 633 ((x + x)' + g(h(x) + (x + (h(x) + g(x)'))'))' = x. [para(217(a,1),66(a,1,1,2,1,1)),rewrite([217(18),6(12),217(22)])]. given #393 (T,wt=21): 679 (x + (x + (g(y) + (h(y) + (x + y)')))')' = (x + y)'. [para(44(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #394 (T,wt=21): 686 (x + (g(x) + (g((x + x)') + h((x + x)')))')' = g(x). [para(29(a,1),44(a,1,1,1))]. given #395 (T,wt=21): 808 (x + (g(y) + (h(y) + (x + (x + y)')))')' = (x + y)'. [para(74(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #396 (A,wt=29): 177 (x + (y + ((x + (y + z'))' + (x + (y + z))'')'))' = (x + (y + z'))'. [para(22(a,1),20(a,1,1,1)),rewrite([7(12)])]. given #397 (T,wt=21): 903 (x + (x + (h(x) + (x + (h(x) + x'))''))')' = h(x). [para(837(a,1),25(a,1,1,2,1,2,2)),rewrite([6(8),837(19)])]. given #398 (T,wt=21): 921 (x + (g(g(x)) + (h(g(x)) + (x + x)'))')' = (x + x)'. [para(29(a,1),94(a,1,1,2)),rewrite([6(8),7(8),6(10)])]. given #399 (T,wt=21): 927 (x + (x + (g(y) + (h(y) + (y + x)')))')' = (y + x)'. [para(94(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #400 (T,wt=21): 1028 (x + (g(y) + (h(y) + (x + (y + x)')))')' = (y + x)'. [para(130(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #401 (A,wt=27): 178 (((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 #402 (T,wt=21): 1120 (g(x) + (x' + (g(x) + (x' + x'))'')')' = x'. [para(192(a,1),8(a,1,1,1))]. given #403 (T,wt=21): 1252 (x' + (g(x) + (g(x) + (h(x) + x'))'')')' = g(x). [para(512(a,1),8(a,1,1,1))]. given #404 (T,wt=21): 1321 (x + (g(x) + (x + (g(x') + h(x')))'')')' = g(x). [para(682(a,1),8(a,1,1,1))]. given #405 (T,wt=21): 1348 ((x + (y + (z + u)))' + (z + (x + (y + u))')')' = z. [para(7(a,1),36(a,1,1,1,1)),rewrite([7(6)])]. given #406 (A,wt=27): 179 ((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 #407 (T,wt=21): 1349 ((x + (y + (z + u)))' + (y + (z + (x + u))')')' = y. [para(19(a,1),36(a,1,1,2,1,2,1))]. given #408 (T,wt=21): 1354 ((x + y)' + ((z + y)' + (x + (y + z')'))')' = x. [para(20(a,1),36(a,1,1,2,1,2)),rewrite([6(11)])]. given #409 (T,wt=21): 1357 ((x + y)' + ((y + z)' + (x + (z' + y)'))')' = x. [para(21(a,1),36(a,1,1,2,1,2)),rewrite([6(11)])]. given #410 (T,wt=21): 1358 ((x + g(y))' + (y + (x + (y + (y + g(y)))'))')' = x. [para(40(a,1),36(a,1,1,2,1,2)),rewrite([6(11)])]. given #411 (A,wt=27): 180 ((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 #412 (T,wt=21): 1359 ((x + g(y))' + (y + (x + (g(y) + h(y)')'))')' = x. [para(43(a,1),36(a,1,1,2,1,2)),rewrite([6(12)])]. given #413 (T,wt=21): 1361 ((x + y)' + ((z + y)' + (x + (z' + y)'))')' = x. [para(56(a,1),36(a,1,1,2,1,2)),rewrite([6(11)])]. given #414 (T,wt=21): 1363 ((x + y)' + ((y + z')' + (x + (z + y)'))')' = x. [para(57(a,1),36(a,1,1,2,1,2)),rewrite([6(11)])]. given #415 (T,wt=21): 1367 ((x + y')' + (g(y) + (x + (y' + y')'))')' = x. [para(66(a,1),36(a,1,1,2,1,2)),rewrite([6(12)])]. given #416 (A,wt=27): 181 (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 #417 (T,wt=21): 1368 ((x + h(y))' + (y + (x + (h(y) + g(y)')'))')' = x. [para(73(a,1),36(a,1,1,2,1,2)),rewrite([6(12)])]. given #418 (T,wt=21): 1370 ((x + y)' + ((z' + y)' + (x + (y + z)'))')' = x. [para(79(a,1),36(a,1,1,2,1,2)),rewrite([6(11)])]. given #419 (T,wt=21): 1427 (x + (g(y) + (x + (h(y) + (x + y)')))')' = (x + y)'. [para(685(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #420 (T,wt=21): 1513 (x + (h(x) + (x + (x + (h(x) + x')))'')')' = h(x). [para(883(a,1),8(a,1,1,1))]. given #421 (A,wt=27): 182 ((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 #422 (T,wt=21): 1538 (x + (g(y) + (x + (h(y) + (y + x)')))')' = (y + x)'. [para(919(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #423 (T,wt=21): 1647 ((x + (y + (z + u)))' + (u + (x + (y + z))')')' = u. [para(7(a,1),58(a,1,1,1,1,2))]. given #424 (T,wt=17): 19633 (h(x) + (g(x) + (x + (x + x))')')' = g(x). [para(12(a,1),1647(a,1,1,1))]. given #425 (T,wt=20): 19661 (g(x) + (g(x) + (h(x) + (x + (x + x))'))')' = h(x). [para(19633(a,1),8(a,1,1,2)),rewrite([19(7),6(10)])]. given #426 (A,wt=27): 183 ((x + (y + g(z)))' + (x + (y + (z + (z + (z + g(z)))')))')' = x + y. [para(40(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #427 (T,wt=21): 1655 ((x + (y + (z + u)))' + (u + (y + (x + z))')')' = u. [para(19(a,1),58(a,1,1,2,1,2,1)),rewrite([7(2)])]. given #428 (T,wt=21): 1668 (g(x + y) + ((y + x)' + (x + y)')')' = (y + x)'. [para(254(a,1),58(a,1,1,1))]. given #429 (T,wt=21): 1684 ((x + x)' + (x + (g(x)' + (x + x)')'')')' = x. [para(71(a,1),8(a,1,1,1))]. given #430 (T,wt=21): 1748 ((x + (y + (z + u)))' + ((x + (y + u))' + z)')' = z. [para(7(a,1),91(a,1,1,1,1)),rewrite([7(6)])]. given #431 (A,wt=27): 184 ((x + (y + g(z)))' + (x + (y + (z + (g(z) + h(z)')')))')' = x + y. [para(43(a,1),22(a,1,1,2,1,2,2)),rewrite([6(14)])]. given #432 (T,wt=21): 1752 ((x + y)' + ((x + z)' + (y + (x + z')'))')' = y. [para(8(a,1),91(a,1,1,2,1,1)),rewrite([6(11)])]. given #433 (T,wt=21): 1755 ((x + (y + (z + u)))' + ((z + (x + u))' + y)')' = y. [para(19(a,1),91(a,1,1,2,1,1,1))]. given #434 (T,wt=21): 1761 ((x + y)' + ((z + x)' + (y + (x + z')'))')' = y. [para(20(a,1),91(a,1,1,2,1,1)),rewrite([6(11)])]. given #435 (T,wt=21): 1764 ((x + y)' + ((x + z)' + (y + (z' + x)'))')' = y. [para(21(a,1),91(a,1,1,2,1,1)),rewrite([6(11)])]. given #436 (A,wt=27): 185 ((x + (y + z))' + ((x + (y + u))' + ((x + (y + u'))' + z))')' = z. [para(22(a,1),56(a,1,1,2,1,1)),rewrite([7(9),7(12),6(14)])]. given #437 (T,wt=21): 1765 ((x + (y + (x + (x + g(x)))'))' + (g(x) + y)')' = y. [para(40(a,1),91(a,1,1,2,1,1))]. given #438 (T,wt=21): 1766 ((x + (y + (g(x) + h(x)')'))' + (g(x) + y)')' = y. [para(43(a,1),91(a,1,1,2,1,1))]. given #439 (T,wt=21): 1768 ((x + y)' + ((z + x)' + (y + (z' + x)'))')' = y. [para(56(a,1),91(a,1,1,2,1,1)),rewrite([6(11)])]. given #440 (T,wt=21): 1770 ((x + y)' + ((x + z')' + (y + (z + x)'))')' = y. [para(57(a,1),91(a,1,1,2,1,1)),rewrite([6(11)])]. given #441 (A,wt=27): 186 ((x + (y + z))' + (x + (y + ((u + z)' + (u' + z)')))')' = x + y. [para(56(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #442 (T,wt=21): 1774 ((g(x) + (y + (x' + x')'))' + (x' + y)')' = y. [para(66(a,1),91(a,1,1,2,1,1))]. given #443 (T,wt=21): 1775 ((x + (y + (h(x) + g(x)')'))' + (h(x) + y)')' = y. [para(73(a,1),91(a,1,1,2,1,1))]. given #444 (T,wt=21): 1777 ((x + y)' + ((z' + x)' + (y + (x + z)'))')' = y. [para(79(a,1),91(a,1,1,2,1,1)),rewrite([6(11)])]. given #445 (T,wt=21): 1883 ((x + (y + (z + u)))' + ((x + (y + z))' + u)')' = u. [para(7(a,1),119(a,1,1,1,1,2))]. given #446 (A,wt=27): 187 ((x + (y + z))' + ((y + (z + u))' + ((y + (z + u'))' + x))')' = x. [para(22(a,1),57(a,1,1,1,1,2)),rewrite([7(12)])]. given #447 (T,wt=21): 1889 ((x + (y + (z + u)))' + ((y + (x + z))' + u)')' = u. [para(19(a,1),119(a,1,1,2,1,1,1)),rewrite([7(2)])]. given #448 (T,wt=21): 1901 (g(x + y) + ((x + y)' + (y + x)')')' = (y + x)'. [para(254(a,1),119(a,1,1,1))]. given #449 (T,wt=21): 1920 ((x + (y + (z + u))')' + (y + (z + (u + x)))')' = x. [para(7(a,1),142(a,1,1,1,1,2,1)),rewrite([7(8)])]. given #450 (T,wt=21): 1923 ((x + (y + (z + u))')' + (z + (y + (u + x)))')' = x. [para(19(a,1),142(a,1,1,1,1,2,1)),rewrite([7(7)])]. given #451 (A,wt=27): 188 ((x + (y + z))' + (x + (y + ((z + u')' + (u + z)')))')' = x + y. [para(57(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #452 (T,wt=21): 1961 (((x + (y + z))' + u)' + (x + (y + (u + z)))')' = u. [para(7(a,1),234(a,1,1,1,1,1,1)),rewrite([7(8)])]. given #453 (T,wt=21): 1965 (((x + (y + z))' + u)' + (y + (u + (x + z)))')' = u. [para(19(a,1),234(a,1,1,1,1,1,1))]. given #454 (T,wt=21): 1969 ((g(x) + y)' + (x + (y + (x + (x + g(x)))'))')' = y. [para(40(a,1),234(a,1,1,1,1,1))]. given #455 (T,wt=21): 1970 ((g(x) + y)' + (x + (y + (g(x) + h(x)')'))')' = y. [para(43(a,1),234(a,1,1,1,1,1))]. given #456 (A,wt=33): 189 ((x + (y + (z + u)))' + (x + (y + ((z + (u + v))' + (z + (u + v'))')))')' = x + y. [para(22(a,1),22(a,1,1,2,1,2,2)),rewrite([6(16)])]. given #457 (T,wt=21): 1975 ((x' + y)' + (g(x) + (y + (x' + x')'))')' = y. [para(66(a,1),234(a,1,1,1,1,1))]. given #458 (T,wt=21): 1976 ((h(x) + y)' + (x + (y + (h(x) + g(x)')'))')' = y. [para(73(a,1),234(a,1,1,1,1,1))]. given #459 (T,wt=21): 2067 (g(x) + (x + (g(x) + (g(h(x)) + h(h(x))))'')')' = x. [para(687(a,1),8(a,1,1,1))]. given #460 (T,wt=21): 2091 (h(x) + (x + (g(g(x)) + (h(x) + h(g(x))))'')')' = x. [para(922(a,1),8(a,1,1,1))]. given #461 (A,wt=24): 194 (g(x) + (x' + (x' + x')'))' = g(g(x) + (x' + x')'). [para(66(a,1),10(a,1,1,2)),rewrite([6(8),19(8)])]. given #462 (T,wt=21): 2114 ((x + (y + (z + u)))' + (x + (u + (y + z))')')' = x. [para(7(a,1),1344(a,1,1,1,1,2))]. given #463 (T,wt=21): 2116 ((x + (y + (z + u)))' + (x + (z + (u + y))')')' = x. [para(7(a,1),1344(a,1,1,2,1,2,1))]. given #464 (T,wt=21): 2121 ((x + (y + (z + u)))' + (x + (y + (u + z))')')' = x. [para(19(a,1),1344(a,1,1,1,1,2)),rewrite([7(6)])]. given #465 (T,wt=21): 2154 (g(x) + (x + (g(x') + (x' + x''')'))')' = x. [para(10(a,1),48(a,1,1,1))]. given #466 (A,wt=22): 200 (x' + (g(x)' + (x' + x')')')' = (x' + x')'. [para(66(a,1),20(a,1,1,1)),rewrite([6(8)])]. given #467 (T,wt=21): 2191 ((x + (y + (z + u)))' + (z + (u + (x + y))')')' = z. [para(7(a,1),1345(a,1,1,1,1))]. given #468 (T,wt=21): 2192 ((x + (y + (z + u)))' + (y + (z + (u + x))')')' = y. [para(7(a,1),1345(a,1,1,2,1,2,1))]. given #469 (T,wt=20): 20395 ((x + h(y))' + (y + (g(y) + (x + (y + y))))')' = x. [para(12(a,1),2192(a,1,1,2,1,2)),rewrite([7(5),6(10)])]. given #470 (T,wt=20): 20426 ((h(x) + y)' + (x + (g(x) + (y + (x + x))))')' = y. [para(6(a,1),20395(a,1,1,1,1))]. given #471 (A,wt=27): 211 ((x + (y + z'))' + (x + (y + (g(z) + (z' + z')')))')' = x + y. [para(66(a,1),22(a,1,1,2,1,2,2)),rewrite([6(14)])]. given #472 (T,wt=20): 20443 ((x + (g(x) + (y + (x + x))))' + (h(x) + y)')' = y. [para(6(a,1),20426(a,1,1))]. given #473 (T,wt=21): 2196 ((x + y)' + ((y + z')' + (x + (y + z)'))')' = x. [para(8(a,1),1345(a,1,1,2,1,2)),rewrite([6(11)])]. given #474 (T,wt=21): 2200 ((x + (y + (z + u)))' + (z + (y + (u + x))')')' = z. [para(19(a,1),1345(a,1,1,1,1,2)),rewrite([7(6)])]. Low Water (displace, True_semantics): id=11577, wt=34 given #475 (T,wt=21): 2201 ((x + (y + (z + u)))' + (z + (x + (u + y))')')' = z. [para(19(a,1),1345(a,1,1,2,1,2,1)),rewrite([7(3)])]. given #476 (A,wt=29): 212 (g((x + (y + z))' + (x + (y + z'))') + (x + (y + (x + y)))')' = x + y. [para(22(a,1),66(a,1,1,2,1,1)),rewrite([22(19),19(12),6(11),22(24)])]. given #477 (T,wt=21): 2209 (((x + (x + g(x)))' + (y + x))' + (y + g(x))')' = y. [para(40(a,1),1345(a,1,1,2,1,2))]. given #478 (T,wt=21): 2210 (((g(x) + h(x)')' + (y + x))' + (y + g(x))')' = y. [para(43(a,1),1345(a,1,1,2,1,2))]. given #479 (T,wt=21): 2213 ((x + y)' + ((z' + y)' + (x + (z + y)'))')' = x. [para(56(a,1),1345(a,1,1,2,1,2)),rewrite([6(11)])]. given #480 (T,wt=21): 2218 (((x' + x')' + (y + g(x)))' + (y + x')')' = y. [para(66(a,1),1345(a,1,1,2,1,2))]. given #481 (A,wt=24): 218 (x + (h(x) + (h(x) + g(x)')'))' = g(x + (h(x) + g(x)')'). [para(73(a,1),10(a,1,1,2)),rewrite([6(8),19(8)])]. given #482 (T,wt=21): 2219 (((h(x) + g(x)')' + (y + x))' + (y + h(x))')' = y. [para(73(a,1),1345(a,1,1,2,1,2))]. Low Water (displace, True_semantics): id=12892, wt=33 given #483 (T,wt=21): 2351 (x + (h(y) + (x + (g(y) + (x + y)')))')' = (x + y)'. [para(2203(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #484 (T,wt=21): 2492 (x + (h(y) + (x + (g(y) + (y + x)')))')' = (y + x)'. [para(2347(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #485 (T,wt=21): 2517 ((x + (y + (z + u))')' + (y + (z + (x + u)))')' = x. [para(7(a,1),1346(a,1,1,1,1,2,1)),rewrite([7(8)])]. given #486 (A,wt=23): 219 (h(x) + (x' + (h(x) + g(x)')')')' = (h(x) + g(x)')'. [para(73(a,1),20(a,1,1,1)),rewrite([6(8)])]. given #487 (T,wt=21): 2519 ((x + (y + (z + u))')' + (z + (x + (y + u)))')' = x. [para(19(a,1),1346(a,1,1,1,1,2,1))]. given #488 (T,wt=21): 2534 ((x + (y + (z + u)))' + (u + (y + (z + x))')')' = u. [para(7(a,1),1646(a,1,1,1,1,2)),rewrite([7(6)])]. given #489 (T,wt=21): 2535 ((x + (y + (z + u)))' + (u + (z + (x + y))')')' = u. [para(7(a,1),1646(a,1,1,1,1))]. given #490 (T,wt=21): 2542 ((x + (y + (z + u)))' + (u + (x + (z + y))')')' = u. [para(19(a,1),1646(a,1,1,2,1,2,1)),rewrite([7(3)])]. given #491 (A,wt=27): 222 (h(x') + (x + (h(x') + g(x')')')')' = (h(x') + g(x')')'. [para(73(a,1),21(a,1,1,2)),rewrite([6(8),6(12)])]. given #492 (T,wt=21): 2556 (g(x + y) + ((y + x)' + (y + x)')')' = (y + x)'. [para(254(a,1),1646(a,1,1,1))]. given #493 (T,wt=21): 2616 ((x + (y + (z + u)))' + ((u + (y + z))' + x)')' = x. [para(7(a,1),1745(a,1,1,1,1,2))]. given #494 (T,wt=21): 2618 ((x + (y + (z + u)))' + ((z + (u + y))' + x)')' = x. [para(7(a,1),1745(a,1,1,2,1,1,1))]. given #495 (T,wt=21): 2623 ((x + (y + (z + u)))' + ((y + (u + z))' + x)')' = x. [para(19(a,1),1745(a,1,1,1,1,2)),rewrite([7(6)])]. given #496 (A,wt=27): 225 ((x + (y + h(z)))' + (x + (y + (z + (h(z) + g(z)')')))')' = x + y. [para(73(a,1),22(a,1,1,2,1,2,2)),rewrite([6(14)])]. given #497 (T,wt=21): 2668 ((x + (y + (z + u)))' + ((u + (x + y))' + z)')' = z. [para(7(a,1),1746(a,1,1,1,1))]. given #498 (T,wt=21): 2669 ((x + (y + (z + u)))' + ((z + (u + x))' + y)')' = y. [para(7(a,1),1746(a,1,1,2,1,1,1))]. given #499 (T,wt=21): 2672 ((x + y)' + ((x + z')' + (y + (x + z)'))')' = y. [para(8(a,1),1746(a,1,1,2,1,1)),rewrite([6(11)])]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 1746 (0.00 of 30.36 sec). given #500 (T,wt=21): 2675 ((x + (y + (z + u)))' + ((y + (u + x))' + z)')' = z. [para(19(a,1),1746(a,1,1,1,1,2)),rewrite([7(6)])]. given #501 (A,wt=25): 230 (x + ((y' + x)' + (x + y)'))' = g((y' + x)' + (x + y)'). [para(79(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #502 (T,wt=21): 2676 ((x + (y + (z + u)))' + ((x + (u + y))' + z)')' = z. [para(19(a,1),1746(a,1,1,2,1,1,1)),rewrite([7(3)])]. given #503 (T,wt=21): 2683 ((g(x) + y)' + ((x + (x + g(x)))' + (y + x))')' = y. [para(40(a,1),1746(a,1,1,2,1,1)),rewrite([6(11)])]. given #504 (T,wt=21): 2684 ((g(x) + y)' + ((g(x) + h(x)')' + (y + x))')' = y. [para(43(a,1),1746(a,1,1,2,1,1)),rewrite([6(12)])]. given #505 (T,wt=21): 2687 ((x + y)' + ((z' + x)' + (y + (z + x)'))')' = y. [para(56(a,1),1746(a,1,1,2,1,1)),rewrite([6(11)])]. given #506 (A,wt=27): 248 ((x + (y + z))' + (x + (y + ((u' + z)' + (z + u)')))')' = x + y. [para(79(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #507 (T,wt=21): 2692 ((x' + y)' + ((x' + x')' + (y + g(x)))')' = y. [para(66(a,1),1746(a,1,1,2,1,1)),rewrite([6(12)])]. given #508 (T,wt=21): 2693 ((h(x) + y)' + ((h(x) + g(x)')' + (y + x))')' = y. [para(73(a,1),1746(a,1,1,2,1,1)),rewrite([6(12)])]. given #509 (T,wt=21): 2770 ((x + (y + (z + u)))' + ((y + (z + x))' + u)')' = u. [para(7(a,1),1882(a,1,1,1,1,2)),rewrite([7(6)])]. given #510 (T,wt=21): 2771 ((x + (y + (z + u)))' + ((z + (x + y))' + u)')' = u. [para(7(a,1),1882(a,1,1,1,1))]. given #511 (A,wt=27): 249 ((x + (y + z))' + (z + ((x + (y + u))' + (x + (y + u'))'))')' = z. [para(22(a,1),79(a,1,1,1,1,1)),rewrite([7(2)])]. given #512 (T,wt=21): 2776 ((x + (y + (z + u)))' + ((x + (z + y))' + u)')' = u. [para(19(a,1),1882(a,1,1,2,1,1,1)),rewrite([7(3)])]. given #513 (T,wt=21): 2803 ((x + (y + (z + u))')' + (u + (y + (z + x)))')' = x. [para(7(a,1),1918(a,1,1,1,1,2,1)),rewrite([7(7)])]. given #514 (T,wt=21): 2805 ((x + (y + (z + u))')' + (z + (u + (y + x)))')' = x. [para(7(a,1),1918(a,1,1,2,1))]. given #515 (T,wt=21): 2806 ((x + (y + (z + u))')' + (y + (u + (z + x)))')' = x. [para(19(a,1),1918(a,1,1,1,1,2,1)),rewrite([7(8)])]. given #516 (A,wt=22): 257 ((x + g(y + z))' + (x + (y + (z + (y + z)')))')' = x. [para(26(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #517 (T,wt=21): 2821 ((x + (y + (z + u))')' + (u + (x + (y + z)))')' = x. [para(7(a,1),1919(a,1,1,1,1,2,1))]. given #518 (T,wt=21): 2823 ((x + (y + (z + u))')' + (z + (u + (x + y)))')' = x. [para(7(a,1),1919(a,1,1,2,1))]. given #519 (T,wt=21): 2825 ((x + (y + (z + u))')' + (y + (u + (x + z)))')' = x. [para(19(a,1),1919(a,1,1,1,1,2,1)),rewrite([7(8)])]. given #520 (T,wt=21): 2826 ((x + (y + (z + u))')' + (u + (y + (x + z)))')' = x. [para(19(a,1),1919(a,1,1,2,1,2)),rewrite([7(2)])]. given #521 (A,wt=24): 258 (x + (y + (g(x + y) + (x + y)')))' = g(x + (y + (x + y)')). [para(26(a,1),10(a,1,1,2)),rewrite([6(7),19(7),19(6)])]. given #522 (T,wt=21): 2827 ((x + g(y))' + ((y + (y + g(y)))' + (x + y))')' = x. [para(40(a,1),1919(a,1,1,1,1,2))]. given #523 (T,wt=21): 2828 ((x + g(y))' + ((g(y) + h(y)')' + (x + y))')' = x. [para(43(a,1),1919(a,1,1,1,1,2))]. given #524 (T,wt=21): 2831 ((x + y')' + ((y' + y')' + (x + g(y)))')' = x. [para(66(a,1),1919(a,1,1,1,1,2))]. given #525 (T,wt=21): 2832 ((x + h(y))' + ((h(y) + g(y)')' + (x + y))')' = x. [para(73(a,1),1919(a,1,1,1,1,2))]. given #526 (A,wt=35): 260 (g(x + (y + (x + y)')) + (x + (y + ((x + y)' + g(x + y)')))')' = x + (y + (x + y)'). [para(26(a,1),27(a,1,1,2,1,2,1)),rewrite([7(13),7(12)])]. given #527 (T,wt=21): 2857 (((x + (y + z))' + u)' + (z + (u + (x + y)))')' = u. [para(7(a,1),1959(a,1,1,1,1,1,1))]. given #528 (T,wt=21): 2859 (((x + (y + z))' + u)' + (y + (z + (u + x)))')' = u. [para(7(a,1),1959(a,1,1,2,1))]. given #529 (T,wt=21): 2861 (((x + (y + z))' + u)' + (x + (z + (u + y)))')' = u. [para(19(a,1),1959(a,1,1,1,1,1,1)),rewrite([7(8)])]. given #530 (T,wt=21): 2863 (((x + (y + z))' + u)' + (z + (x + (u + y)))')' = u. [para(19(a,1),1959(a,1,1,2,1,2)),rewrite([7(2)])]. given #531 (A,wt=23): 261 (g(x + y) + (x' + (y + (x + y)'))')' = y + (x + y)'. [para(26(a,1),20(a,1,1,1)),rewrite([6(7)])]. given #532 (T,wt=21): 2876 (((x + (y + z))' + u)' + (u + (z + (x + y)))')' = u. [para(7(a,1),1960(a,1,1,1,1,1,1))]. given #533 (T,wt=21): 2877 (((x + (y + z))' + u)' + (u + (y + (z + x)))')' = u. [para(7(a,1),1960(a,1,1,2,1,2))]. given #534 (T,wt=21): 2879 (((x + (y + z))' + u)' + (u + (x + (z + y)))')' = u. [para(19(a,1),1960(a,1,1,1,1,1,1)),rewrite([7(7)])]. Low Water (keep, True_semantics): wt=29 given #535 (T,wt=21): 3222 (x + (x + (x + (x + (h(x) + (x + g(x))')))'))' = h(x). [para(170(a,1),8(a,1,1,2)),rewrite([19(7),19(6),6(10),7(10)])]. given #536 (A,wt=22): 262 ((x + (y + ((x + y)' + z)))' + (z + g(x + y))')' = z. [para(26(a,1),20(a,1,1,2,1,2)),rewrite([7(5),7(4)])]. given #537 (T,wt=21): 3692 (x' + (g(x) + (g(x) + (x' + (x + x)')))')' = g(x). [para(511(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #538 (T,wt=21): 3792 (g(x) + (x + ((y + x')' + (x' + y')'))')' = x. [para(10(a,1),61(a,1,1,1))]. given #539 (T,wt=21): 5272 ((x + y')' + (x + (x + (y + (x + y')')))')' = x. [para(85(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #540 (T,wt=21): 5284 ((x + y')' + (x + (y + (x + (x + y')')))')' = x. [para(57(a,1),85(a,1,1,2,1,2,2)),rewrite([6(8),6(9),7(9),7(8),57(19)])]. given #541 (A,wt=22): 263 ((x + (y + (z + (y + z)')))' + (g(y + z) + x)')' = x. [para(26(a,1),21(a,1,1,2,1,1))]. given #542 (T,wt=21): 5293 ((x' + y)' + (y + (y + (x + (x' + y)')))')' = y. [para(79(a,1),85(a,1,1,2,1,2,2)),rewrite([6(8),6(9),7(9),7(8),79(19)])]. given #543 (T,wt=21): 5356 (g(x) + (x + (x + (g(x) + (g(x') + h(x')))))')' = x. [para(682(a,1),85(a,1,1,2,1,2,2)),rewrite([6(9),19(10),19(9),682(23)])]. given #544 (T,wt=21): 5365 (h(x) + (x + (x + (x + (h(x) + (h(x) + x')))))')' = x. [para(883(a,1),85(a,1,1,2,1,2,2)),rewrite([6(8),19(9),19(8),19(7),883(21)])]. given #545 (T,wt=21): 5524 (x + (y + (g(y + x) + h(x + y)')'))' = g(y + x). [para(5499(a,1),8(a,1,1,1)),rewrite([7(9)])]. given #546 (A,wt=25): 264 (g(x' + y) + (x + (y + (x' + y)'))')' = y + (x' + y)'. [para(26(a,1),21(a,1,1,2)),rewrite([6(5),6(10)])]. given #547 (T,wt=21): 5528 (x + (y + (h(x + y) + g(y + x)')'))' = h(x + y). [para(5499(a,1),20(a,1,1,1)),rewrite([7(9)])]. given #548 (T,wt=21): 5900 ((x + y')' + (y + (x + (x + (x + y')')))')' = x. [para(99(a,1),36(a,1,1,2)),rewrite([6(11)])]. given #549 (T,wt=21): 6030 ((x' + y)' + (y + (x + (y + (x' + y)')))')' = y. [para(56(a,1),101(a,1,1,2,1,2,2)),rewrite([6(8),6(9),7(9),7(8),56(19)])]. given #550 (T,wt=21): 6698 ((x' + y)' + (x + (y + (y + (x' + y)')))')' = y. [para(136(a,1),36(a,1,1,2)),rewrite([6(11)])]. given #551 (A,wt=22): 265 ((g(x + y) + z)' + (x + (y + ((x + y)' + z)))')' = z. [para(26(a,1),56(a,1,1,2,1,1)),rewrite([7(5),7(4),6(11)])]. given #552 (T,wt=21): 10244 (h(x) + (x + (x + (h(x) + (x + (x + g(x)))')))')' = x. [para(570(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #553 (T,wt=21): 10671 (g(x) + (x + ((x' + y)' + (y' + x')'))')' = x. [para(10(a,1),82(a,1,1,1))]. given #554 (T,wt=21): 16282 (x + (y + (g(x + y) + h(y + x)')'))' = g(x + y). [para(6(a,1),110(a,1,1,2,2,1,2,1,1))]. given #555 (T,wt=21): 16288 (x + (y + (g(y + x) + h(y + x)')'))' = g(y + x). [para(19(a,1),110(a,1,1))]. given #556 (A,wt=22): 266 ((x + g(y + z))' + (y + (z + ((y + z)' + x)))')' = x. [para(26(a,1),57(a,1,1,1,1,2)),rewrite([7(9),7(8)])]. given #557 (T,wt=21): 16733 (h(x) + (x + (x + (h(x) + (g(x) + h(x)')')))')' = x. [para(16707(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #558 (T,wt=21): 16931 (g(x) + (x + ((y + x')' + (y' + x')'))')' = x. [para(10(a,1),121(a,1,1,1))]. given #559 (T,wt=21): 17553 (g(x) + (x + ((x' + y')' + (y + x')'))')' = x. [para(10(a,1),143(a,1,1,1))]. given #560 (T,wt=21): 17876 (x + (x + (g(x) + (g(x) + (x' + x')')))')' = g(x). [para(17830(a,1),8(a,1,1,2)),rewrite([19(9),6(11)])]. given #561 (A,wt=28): 267 ((x + (y + g(z + u)))' + (x + (y + (z + (u + (z + u)'))))')' = x + y. [para(26(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #562 (T,wt=21): 18187 (x + (y + (h(y + x) + g(x + y)')'))' = h(x + y). [para(6(a,1),214(a,1,1,2,2,1,1,1))]. given #563 (T,wt=21): 18192 (x + (y + (h(y + x) + g(y + x)')'))' = h(y + x). [para(19(a,1),214(a,1,1))]. given #564 (T,wt=21): 18227 (g(x) + (x + (x + (g(x) + (h(x) + g(x)')')))')' = x. [para(18209(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #565 (T,wt=21): 18304 (g(x) + (x + ((y' + x')' + (x' + y)'))')' = x. [para(10(a,1),228(a,1,1,1))]. given #566 (A,wt=26): 268 (g(x + (y + (x + y)')) + (g(x + y) + g(x + y))')' = g(x + y). [para(26(a,1),66(a,1,1,2,1,1)),rewrite([26(12),26(18)])]. given #567 (T,wt=21): 19288 ((x + (y + (z + u)))' + (y + (x + (u + z))')')' = y. [para(6(a,1),1348(a,1,1,1,1,2)),rewrite([7(2)])]. given #568 (T,wt=21): 19289 ((x + (y + (z + u)))' + (y + (u + (x + z))')')' = y. [para(6(a,1),1348(a,1,1,1,1)),rewrite([7(3),7(2)])]. given #569 (T,wt=21): 19293 ((x + (y + (z + u)))' + (z + (y + (x + u))')')' = z. [para(19(a,1),1348(a,1,1,1,1))]. Low Water (displace, True_semantics): id=15208, wt=32 given #570 (T,wt=21): 19349 ((x + (y + (z + u)))' + (x + (z + (y + u))')')' = x. [para(19(a,1),1349(a,1,1,1,1))]. given #571 (A,wt=22): 269 ((g(x + y) + z)' + (z + (x + (y + (x + y)')))')' = z. [para(26(a,1),79(a,1,1,1,1,1))]. given #572 (T,wt=21): 19762 ((x + (y + (z + u)))' + ((x + (u + z))' + y)')' = y. [para(6(a,1),1748(a,1,1,1,1,2)),rewrite([7(2)])]. given #573 (T,wt=21): 19763 ((x + (y + (z + u)))' + ((u + (x + z))' + y)')' = y. [para(6(a,1),1748(a,1,1,1,1)),rewrite([7(3),7(2)])]. given #574 (T,wt=21): 19767 ((x + (y + (z + u)))' + ((y + (x + u))' + z)')' = z. [para(19(a,1),1748(a,1,1,1,1))]. given #575 (T,wt=21): 19842 ((x + (y + (z + u)))' + ((z + (y + u))' + x)')' = x. [para(19(a,1),1755(a,1,1,1,1))]. given #576 (A,wt=24): 270 ((x + y)' + (x + ((x + y)' + (x + y')'')'')')' = x. [para(23(a,1),8(a,1,1,1))]. given #577 (T,wt=21): 20154 ((x + (y + (z + u))')' + (z + (y + (x + u)))')' = x. [para(6(a,1),1923(a,1,1,2,1,2,2))]. given #578 (T,wt=21): 20172 (((x + (y + z))' + u)' + (x + (u + (z + y)))')' = u. [para(6(a,1),1961(a,1,1,2,1,2)),rewrite([7(7)])]. given #579 (T,wt=21): 20173 (((x + (y + z))' + u)' + (y + (u + (z + x)))')' = u. [para(6(a,1),1961(a,1,1,2,1)),rewrite([7(8),7(7)])]. given #580 (T,wt=21): 20177 (((x + (y + z))' + u)' + (y + (x + (u + z)))')' = u. [para(19(a,1),1961(a,1,1,1,1,1,1))]. given #581 (A,wt=28): 271 ((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 #582 (T,wt=21): 20197 (((x + (y + z))' + u)' + (u + (y + (x + z)))')' = u. [para(19(a,1),1965(a,1,1,2,1))]. given #583 (T,wt=21): 20227 ((x + (y + (z + u)))' + (x + (u + (z + y))')')' = x. [para(6(a,1),2114(a,1,1,2,1,2,1,2))]. given #584 (T,wt=21): 20359 ((x + (y + (z + u)))' + (z + (u + (y + x))')')' = z. [para(6(a,1),2191(a,1,1,2,1,2,1,2))]. given #585 (T,wt=21): 20391 ((x + (y + (z + u)))' + (y + (u + (z + x))')')' = y. [para(6(a,1),2192(a,1,1,1,1,2,2))]. given #586 (A,wt=22): 272 ((x + y)' + (x + ((x + y)' + (x + y')''))')' = x. [para(23(a,1),8(a,1,1,2)),rewrite([6(12)])]. given #587 (T,wt=21): 20688 ((x + (y + (z + u))')' + (y + (x + (u + z)))')' = x. [para(6(a,1),2517(a,1,1,2,1,2)),rewrite([7(7)])]. given #588 (T,wt=21): 20689 ((x + (y + (z + u))')' + (z + (x + (u + y)))')' = x. [para(6(a,1),2517(a,1,1,2,1)),rewrite([7(8),7(7)])]. given #589 (T,wt=21): 20709 ((x + (y + (z + u)))' + (u + (z + (y + x))')')' = u. [para(19(a,1),2534(a,1,1,1,1,2))]. given #590 (T,wt=21): 20806 ((x + (y + (z + u)))' + ((u + (z + y))' + x)')' = x. [para(6(a,1),2616(a,1,1,2,1,1,1,2))]. given #591 (A,wt=31): 273 ((x + y)' + (x' + (x + (y' + (x + y)'))')')' = (x + (y' + (x + y)'))'. [para(8(a,1),23(a,1,1,2,1,2,1)),rewrite([6(7),7(7),6(10),6(18),7(18)])]. given #592 (T,wt=21): 20891 ((x + (y + (z + u)))' + ((u + (y + x))' + z)')' = z. [para(6(a,1),2668(a,1,1,2,1,1,1,2))]. given #593 (T,wt=21): 20917 ((x + (y + (z + u)))' + ((u + (z + x))' + y)')' = y. [para(6(a,1),2669(a,1,1,1,1,2,2))]. given #594 (T,wt=21): 21121 ((x + (y + (z + u)))' + ((z + (y + x))' + u)')' = u. [para(19(a,1),2770(a,1,1,1,1,2))]. given #595 (T,wt=21): 21174 ((x + (y + (z + u))')' + (u + (z + (x + y)))')' = x. [para(6(a,1),2803(a,1,1,2,1,2)),rewrite([7(7)])]. given #596 (A,wt=26): 274 (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 #597 (T,wt=21): 21179 ((x + (y + (z + u))')' + (u + (z + (y + x)))')' = x. [para(19(a,1),2803(a,1,1,1,1,2,1))]. given #598 (T,wt=21): 21193 ((x + (y + (z + u))')' + (u + (x + (z + y)))')' = x. [para(6(a,1),2821(a,1,1,2,1,2,2))]. given #599 (T,wt=21): 21248 (((x + (y + z))' + u)' + (z + (u + (y + x)))')' = u. [para(6(a,1),2857(a,1,1,2,1,2,2))]. given #600 (T,wt=21): 21259 (((x + (y + z))' + u)' + (z + (y + (u + x)))')' = u. [para(6(a,1),2859(a,1,1,1,1,1,1,2))]. given #601 (A,wt=34): 275 (x + ((x + (y + (y + (y + g(y)))))' + (x + h(y))'')')' = (x + (y + (y + (y + g(y)))))'. [para(12(a,1),23(a,1,1,2,1,2,1,1,2))]. given #602 (T,wt=21): 21283 (((x + (y + z))' + u)' + (u + (z + (y + x)))')' = u. [para(6(a,1),2876(a,1,1,2,1,2,2))]. given #603 (T,wt=21): 21331 ((x' + y)' + (y + (y + (x + (y + x')')))')' = y. [para(6(a,1),5272(a,1,1,1,1))]. given #604 (T,wt=21): 21332 ((x + y')' + (x + (x + (y + (y' + x)')))')' = x. [para(6(a,1),5272(a,1,1,2,1,2,2,2,1))]. given #605 (T,wt=21): 21364 ((x' + y)' + (y + (x + (y + (y + x')')))')' = y. [para(6(a,1),5284(a,1,1,1,1))]. given #606 (A,wt=26): 276 (x + ((y + (x + z))' + (x + (y + z)')'')')' = (x + (y + z))'. [para(19(a,1),23(a,1,1,2,1,1,1))]. given #607 (T,wt=21): 21365 ((x + y')' + (x + (y + (x + (y' + x)')))')' = x. [para(6(a,1),5284(a,1,1,2,1,2,2,2,1))]. given #608 (T,wt=21): 21379 ((x' + y)' + (x + (y + (y + (y + x')')))')' = y. [para(6(a,1),5900(a,1,1,1,1))]. given #609 (T,wt=21): 21380 ((x + y')' + (y + (x + (x + (y' + x)')))')' = x. [para(6(a,1),5900(a,1,1,2,1,2,2,2,1))]. given #610 (T,wt=21): 21582 (x + (x + (g(x) + (g(x)' + (x + x)')'))')' = g(x). [para(29(a,1),271(a,1,1,1)),rewrite([10(6),6(6),19(9)])]. given #611 (A,wt=31): 278 (x + ((x + (g(y) + (y + y)'))' + (x + y)'')')' = (x + (g(y) + (y + y)'))'. [para(29(a,1),23(a,1,1,2,1,2,1,1,2))]. given #612 (T,wt=22): 290 (x + (g(x) + (x + (x + (x + g(x)))'')'')')' = g(x). [para(40(a,1),23(a,1,1,2,1,1)),rewrite([40(19)])]. given #613 (T,wt=22): 291 (x + (g(x) + (x + (g(x) + h(x)')'')'')')' = g(x). [para(43(a,1),23(a,1,1,2,1,1)),rewrite([43(21)])]. given #614 (T,wt=22): 304 (x + (h(x) + (x + (h(x) + g(x)')'')'')')' = h(x). [para(73(a,1),23(a,1,1,2,1,1)),rewrite([73(21)])]. given #615 (T,wt=22): 312 ((x + g(y + y'))' + (x + (y + (g(y) + y')))')' = x. [para(31(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])]. given #616 (A,wt=27): 279 (x + ((x + (g(y) + h(y)))' + (x + y)'')')' = (x + (g(y) + h(y)))'. [para(42(a,1),23(a,1,1,2,1,2,1,1,2))]. given #617 (T,wt=22): 318 (g(x + x') + (g(x) + (x' + x'))')' = g(x) + x'. [para(31(a,1),20(a,1,1,1)),rewrite([6(8),19(8)])]. given #618 (T,wt=22): 319 ((x + (g(x) + (x' + y)))' + (y + g(x + x'))')' = y. [para(31(a,1),20(a,1,1,2,1,2)),rewrite([7(5),7(4)])]. given #619 (T,wt=22): 320 ((x + (y + (g(y) + y')))' + (g(y + y') + x)')' = x. [para(31(a,1),21(a,1,1,2,1,1))]. given #620 (T,wt=22): 322 ((x + (g(x) + (x' + y)))' + (g(x + x') + y)')' = y. [para(31(a,1),56(a,1,1,2,1,1)),rewrite([7(5),7(4)])]. given #621 (A,wt=35): 281 (x + ((x + (g(y) + (y + y'')'))' + (x + y)'')')' = (x + (g(y) + (y + y'')'))'. [para(27(a,1),23(a,1,1,2,1,2,1,1,2))]. given #622 (T,wt=22): 323 ((x + g(y + y'))' + (y + (g(y) + (y' + x)))')' = x. [para(31(a,1),57(a,1,1,1,1,2)),rewrite([7(10),7(9)])]. given #623 (T,wt=22): 328 ((g(x + x') + y)' + (y + (x + (g(x) + x')))')' = y. [para(31(a,1),79(a,1,1,1,1,1))]. given #624 (T,wt=22): 333 ((x + y)' + (x + (g(g(y) + h(y)) + (y + y)'))')' = x. [para(198(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])]. given #625 (T,wt=22): 337 ((g(g(x) + h(x)) + ((x + x)' + y))' + (y + x)')' = y. [para(198(a,1),20(a,1,1,2,1,2)),rewrite([7(8)])]. given #626 (A,wt=27): 282 (g(x) + (x' + (x + (g(x) + x''))')')' = (x + (g(x) + x''))'. [para(27(a,1),23(a,1,1,2,1,2,1)),rewrite([19(6),6(9),19(17)])]. given #627 (T,wt=22): 338 ((x + (g(g(y) + h(y)) + (y + y)'))' + (y + x)')' = x. [para(198(a,1),21(a,1,1,2,1,1))]. given #628 (T,wt=22): 339 ((x + y)' + (g(g(x) + h(x)) + ((x + x)' + y))')' = y. [para(198(a,1),56(a,1,1,2,1,1)),rewrite([7(8),6(12)])]. given #629 (T,wt=22): 340 ((x + y)' + (g(g(y) + h(y)) + ((y + y)' + x))')' = x. [para(198(a,1),57(a,1,1,1,1,2)),rewrite([7(10)])]. given #630 (T,wt=22): 343 ((x + y)' + (y + (g(g(x) + h(x)) + (x + x)'))')' = y. [para(198(a,1),79(a,1,1,1,1,1))]. given #631 (A,wt=35): 283 ((x + y)' + (x' + ((x + y)' + (x + y')'')')')' = ((x + y)' + (x + y')'')'. [para(23(a,1),20(a,1,1,1)),rewrite([6(12)])]. given #632 (T,wt=22): 349 ((x + g(y + z))' + (x + (y + (z + (z + y)')))')' = x. [para(254(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #633 (T,wt=22): 354 ((x + (y + ((y + x)' + z)))' + (z + g(x + y))')' = z. [para(254(a,1),20(a,1,1,2,1,2)),rewrite([7(5),7(4)])]. given #634 (T,wt=22): 355 ((x + (y + (z + (z + y)')))' + (g(y + z) + x)')' = x. [para(254(a,1),21(a,1,1,2,1,1))]. given #635 (T,wt=22): 357 ((g(x + y) + z)' + (x + (y + ((y + x)' + z)))')' = z. [para(254(a,1),56(a,1,1,2,1,1)),rewrite([7(5),7(4),6(11)])]. given #636 (A,wt=28): 284 ((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 #637 (T,wt=22): 358 ((x + g(y + z))' + (y + (z + ((z + y)' + x)))')' = x. [para(254(a,1),57(a,1,1,1,1,2)),rewrite([7(9),7(8)])]. given #638 (T,wt=22): 363 ((g(x + y) + z)' + (z + (x + (y + (y + x)')))')' = z. [para(254(a,1),79(a,1,1,1,1,1))]. given #639 (T,wt=22): 396 (x + (g(x) + ((h(x) + y)' + (h(x) + y')'))')' = g(x). [para(42(a,1),24(a,1,1,1))]. given #640 (T,wt=22): 477 (g(g(x) + h(x)) + (x + (g(x) + h(x)'))')' = x + g(x). [para(45(a,1),22(a,1,1,1))]. given #641 (A,wt=24): 285 ((x + y)' + (y + ((x + y)' + (y + x')'')'')')' = y. [para(20(a,1),23(a,1,1,2,1,1)),rewrite([20(22)])]. given #642 (T,wt=22): 510 (g(h(x)) + (x + (x + (x + (g(x) + h(x)'))))')' = h(x)'. [para(12(a,1),88(a,1,1,1,1)),rewrite([12(11),7(9),7(8),7(7),12(17)])]. given #643 (T,wt=22): 537 (g(x) + (g(g(x) + h(x)) + (x' + (x + x)'))')' = x'. [para(198(a,1),88(a,1,1,1,1)),rewrite([198(16),6(10),19(10),198(21)])]. given #644 (T,wt=22): 565 ((x + y)' + (x + (x + (y' + (x + y)'))'')')' = x. [para(25(a,1),8(a,1,1,1))]. given #645 (T,wt=22): 578 ((x + y)' + (y + ((x + y)' + (y + x')''))')' = y. [para(20(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),19(10),20(20)])]. given #646 (A,wt=31): 286 ((x + y)' + (y' + (y + (x' + (x + y)'))')')' = (y + (x' + (x + y)'))'. [para(20(a,1),23(a,1,1,2,1,2,1)),rewrite([6(7),7(7),6(10),6(18),7(18)])]. given #647 (T,wt=22): 582 ((x + y)' + (x + ((x + y)' + (y' + x)''))')' = x. [para(21(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),19(10),21(20)])]. given #648 (T,wt=22): 589 ((x + y)' + (y + ((x + y)' + (x' + y)''))')' = y. [para(56(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),19(10),56(20)])]. given #649 (T,wt=22): 613 (x + (x + (g(x) + (g(x) + (x + x)'')''))')' = g(x). [para(38(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),38(21)])]. given #650 (T,wt=22): 619 (x + (x + (g(x) + (x + (g(x) + x''))''))')' = g(x). [para(49(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),49(21)])]. given #651 (A,wt=28): 287 ((x + (y + ((y + z)' + (y + z')'')'))' + ((y + z)' + x)')' = x. [para(23(a,1),21(a,1,1,2,1,1))]. given #652 (T,wt=22): 622 (g(x) + (x + (g(x) + (x + (g(x) + h(x)'))''))')' = x. [para(113(a,1),25(a,1,1,2,1,2,2)),rewrite([6(10),19(11),113(23)])]. given #653 (T,wt=22): 641 (h(x) + (x + (h(x) + (x + (h(x) + g(x)'))''))')' = x. [para(217(a,1),25(a,1,1,2,1,2,2)),rewrite([6(10),19(11),217(23)])]. given #654 (T,wt=22): 643 (x + (x + (y + (y' + (x + g(y))')))')' = (x + g(y))'. [para(28(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #655 (T,wt=22): 661 (g((x + g(y))' + (x + (y + y'))') + (x + x)')' = x. [para(28(a,1),66(a,1,1,2,1,1)),rewrite([28(18),28(22)])]. given #656 (A,wt=24): 288 ((x + y)' + (x + ((x + y)' + (y' + x)'')'')')' = x. [para(21(a,1),23(a,1,1,2,1,1)),rewrite([21(22)])]. given #657 (T,wt=22): 684 ((x + (y + z))' + (y + (g(x + z) + h(x + z)))')' = y. [para(19(a,1),44(a,1,1,1,1))]. given #658 (T,wt=22): 700 (g((x + y)' + (x + (g(y) + h(y)))') + (x + x)')' = x. [para(44(a,1),66(a,1,1,2,1,1)),rewrite([44(18),44(22)])]. given #659 (T,wt=22): 724 ((x + (x' + (y + z)))' + (y + (z + g(x)))')' = y + z. [para(7(a,1),67(a,1,1,2,1))]. given #660 (T,wt=22): 731 ((x + (y + (x' + z)))' + (y + (z + g(x)))')' = y + z. [para(19(a,1),67(a,1,1,1,1,2)),rewrite([7(8)])]. given #661 (A,wt=31): 289 ((x + y)' + (x' + (y' + (x + (x + y)'))')')' = (y' + (x + (x + y)'))'. [para(21(a,1),23(a,1,1,2,1,2,1)),rewrite([6(7),7(7),6(10),6(18),7(18)])]. given #662 (T,wt=22): 738 (x + (y + (y' + (x + (x + g(y))')))')' = (x + g(y))'. [para(67(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #663 (T,wt=22): 747 (g((x + (x' + y))' + (y + g(x))') + (y + y)')' = y. [para(67(a,1),66(a,1,1,2,1,1)),rewrite([67(18),67(22)])]. given #664 (T,wt=22): 797 ((g(x) + (h(x) + (y + z)))' + (y + (z + x))')' = y + z. [para(7(a,1),74(a,1,1,2,1))]. given #665 (T,wt=22): 802 ((g(x) + (y + (h(x) + z)))' + (y + (z + x))')' = y + z. [para(19(a,1),74(a,1,1,1,1,2)),rewrite([7(8)])]. given #666 (A,wt=27): 292 (x + (g(x)' + (x + (g(x) + h(x)'))')')' = (x + (g(x) + h(x)'))'. [para(43(a,1),23(a,1,1,2,1,2,1)),rewrite([6(9)])]. given #667 (T,wt=22): 803 ((g(x + y) + (h(x + y) + z))' + (x + (z + y))')' = z. [para(19(a,1),74(a,1,1,2,1))]. given #668 (T,wt=22): 814 (g((g(x) + (h(x) + y))' + (y + x)') + (y + y)')' = y. [para(74(a,1),66(a,1,1,2,1,1)),rewrite([74(18),74(22)])]. given #669 (T,wt=22): 827 ((x + (y + (z + z')))' + (g(z) + (x + y))')' = x + y. [para(7(a,1),87(a,1,1,1,1))]. given #670 (T,wt=22): 835 ((x + (y + (z + z')))' + (x + (g(z) + y))')' = x + y. [para(19(a,1),87(a,1,1,2,1)),rewrite([7(4)])]. given #671 (A,wt=28): 293 (((x + y)' + z)' + (x + (((x + y)' + (x + y')'')' + z))')' = z. [para(23(a,1),56(a,1,1,2,1,1)),rewrite([7(10),6(16)])]. given #672 (T,wt=22): 843 (x + (x + (y + (y' + (g(y) + x)')))')' = (g(y) + x)'. [para(87(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #673 (T,wt=22): 854 (g((x + (y + y'))' + (g(y) + x)') + (x + x)')' = x. [para(87(a,1),66(a,1,1,2,1,1)),rewrite([87(18),87(22)])]. given #674 (T,wt=22): 882 ((x + h(y))' + (x + (y + (y + (h(y) + y'))'))')' = x. [para(837(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])]. given #675 (T,wt=20): 21970 (x + (x + (g(x) + (x + (h(x) + x'))'))')' = g(x). [para(42(a,1),882(a,1,1,1)),rewrite([19(8)])]. given #676 (A,wt=24): 294 ((x + y)' + (y + ((x + y)' + (x' + y)'')'')')' = y. [para(56(a,1),23(a,1,1,2,1,1)),rewrite([56(22)])]. given #677 (T,wt=22): 888 ((x + ((x + (h(x) + x'))' + y))' + (y + h(x))')' = y. [para(837(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #678 (T,wt=22): 889 ((x + (y + (y + (h(y) + y'))'))' + (h(y) + x)')' = x. [para(837(a,1),21(a,1,1,2,1,1))]. given #679 (T,wt=22): 891 ((h(x) + y)' + (x + ((x + (h(x) + x'))' + y))')' = y. [para(837(a,1),56(a,1,1,2,1,1)),rewrite([7(7),6(12)])]. given #680 (T,wt=22): 892 ((x + h(y))' + (y + ((y + (h(y) + y'))' + x))')' = x. [para(837(a,1),57(a,1,1,1,1,2)),rewrite([7(10)])]. given #681 (A,wt=31): 295 ((x + y)' + (y' + (x' + (y + (x + y)'))')')' = (x' + (y + (x + y)'))'. [para(56(a,1),23(a,1,1,2,1,2,1)),rewrite([6(7),7(7),6(10),6(18),7(18)])]. given #682 (T,wt=22): 894 ((h(x) + h(x))' + g(x + (x + (h(x) + x'))'))' = h(x). [para(837(a,1),66(a,1,1,2,1,1)),rewrite([837(15),6(12),837(20)])]. given #683 (T,wt=22): 895 ((h(x) + y)' + (y + (x + (x + (h(x) + x'))'))')' = y. [para(837(a,1),79(a,1,1,1,1,1))]. given #684 (T,wt=22): 911 ((x + (y + (g(z) + h(z))))' + (z + (x + y))')' = x + y. [para(7(a,1),94(a,1,1,1,1))]. given #685 (T,wt=22): 912 ((x + (g(y + z) + h(y + z)))' + (y + (z + x))')' = x. [para(7(a,1),94(a,1,1,2,1))]. given #686 (A,wt=28): 296 ((x + (y + z)')' + (y + (((y + z)' + (y + z')'')' + x))')' = x. [para(23(a,1),57(a,1,1,1,1,2)),rewrite([7(14)])]. given #687 (T,wt=22): 920 ((x + (y + (g(z) + h(z))))' + (x + (z + y))')' = x + y. [para(19(a,1),94(a,1,1,2,1)),rewrite([7(5)])]. given #688 (T,wt=22): 933 (g((x + (g(y) + h(y)))' + (y + x)') + (x + x)')' = x. [para(94(a,1),66(a,1,1,2,1,1)),rewrite([94(18),94(22)])]. given #689 (T,wt=22): 963 (x + (y + (x + (y + (x + (y + g(y + x)))))))' = h(x + y). [para(6(a,1),32(a,1,1,2,2,2,2,2,2,1))]. given #690 (T,wt=22): 968 (x + (y + (x + (y + (y + (x + g(x + y)))))))' = h(x + y). [para(19(a,1),32(a,1,1,2,2,2,2))]. given #691 (A,wt=25): 297 ((x + y')' + (x + ((x + y')' + (y + x)'')'')')' = x. [para(57(a,1),23(a,1,1,2,1,1)),rewrite([57(23)])]. given #692 (T,wt=22): 969 (x + (y + (x + (x + (y + (y + g(x + y)))))))' = h(x + y). [para(19(a,1),32(a,1,1,2,2,2))]. given #693 (T,wt=22): 970 (x + (y + (y + (x + (x + (y + g(x + y)))))))' = h(x + y). [para(19(a,1),32(a,1,1,2,2))]. given #694 (T,wt=22): 971 (x + (x + (y + (y + (x + (y + g(x + y)))))))' = h(x + y). [para(19(a,1),32(a,1,1,2))]. given #695 (T,wt=22): 972 (x + (y + (y + (x + (y + (x + g(y + x)))))))' = h(y + x). [para(19(a,1),32(a,1,1))]. given #696 (A,wt=32): 298 ((x + y')' + (x' + (y + (x + (x + y')'))')')' = (y + (x + (x + y')'))'. [para(57(a,1),23(a,1,1,2,1,2,1)),rewrite([6(8),7(8),6(11),6(19),7(19)])]. given #697 (T,wt=22): 985 (x + (y + (y' + (x + (g(y) + x)')))')' = (g(y) + x)'. [para(125(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #698 (T,wt=22): 988 ((x + (g(y) + z))' + (y + (y' + (x + z)))')' = x + z. [para(19(a,1),125(a,1,1,1,1))]. given #699 (T,wt=22): 989 ((g(x) + (y + z))' + (x + (y + (x' + z)))')' = y + z. [para(19(a,1),125(a,1,1,2,1,2))]. given #700 (T,wt=22): 1005 (g((g(x) + y)' + (x + (x' + y))') + (y + y)')' = y. [para(125(a,1),66(a,1,1,2,1,1)),rewrite([125(18),125(22)])]. given #701 (A,wt=34): 299 ((x + (y + (z + u)'))' + (x + (y + (z + ((z + u)' + (z + u')'')')))')' = x + y. [para(23(a,1),22(a,1,1,2,1,2,2)),rewrite([6(18)])]. given #702 (T,wt=22): 1025 ((x + (y + z))' + (g(x + y) + (h(x + y) + z))')' = z. [para(7(a,1),130(a,1,1,1,1))]. given #703 (T,wt=22): 1030 ((x + (y + z))' + (g(y) + (h(y) + (x + z)))')' = x + z. [para(19(a,1),130(a,1,1,1,1))]. given #704 (T,wt=22): 1031 ((x + (y + z))' + (g(x) + (y + (h(x) + z)))')' = y + z. [para(19(a,1),130(a,1,1,2,1,2))]. given #705 (T,wt=22): 1039 (g((x + y)' + (g(x) + (h(x) + y))') + (y + y)')' = y. [para(130(a,1),66(a,1,1,2,1,1)),rewrite([130(18),130(22)])]. given #706 (A,wt=34): 300 ((x + (y + z))' + (x + (y + ((x + (y + z))' + (x + (y + z'))'')''))')' = x + y. [para(22(a,1),23(a,1,1,2,1,1)),rewrite([7(16),22(28)])]. given #707 (T,wt=22): 1053 ((x + (y + g(z)))' + (z + (z' + (x + y)))')' = x + y. [para(7(a,1),146(a,1,1,1,1))]. given #708 (T,wt=22): 1056 ((x + (y + g(z)))' + (z + (x + (z' + y)))')' = x + y. [para(19(a,1),146(a,1,1,2,1,2)),rewrite([7(3)])]. given #709 (T,wt=22): 1070 (g((x + g(y))' + (y + (y' + x))') + (x + x)')' = x. [para(146(a,1),66(a,1,1,2,1,1)),rewrite([146(18),146(22)])]. given #710 (T,wt=22): 1088 ((x + (y + z))' + (g(z) + (h(z) + (x + y)))')' = x + y. [para(7(a,1),150(a,1,1,1,1))]. given #711 (A,wt=32): 301 (((x + y)' + (x + y)')' + g(x + ((x + y)' + (x + y')'')'))' = (x + y)'. [para(23(a,1),66(a,1,1,2,1,1)),rewrite([23(22),6(17),23(28)])]. given #712 (T,wt=22): 1090 ((x + (y + z))' + (g(x + z) + (h(x + z) + y))')' = y. [para(19(a,1),150(a,1,1,1,1))]. given #713 (T,wt=22): 1091 ((x + (y + z))' + (g(z) + (x + (h(z) + y)))')' = x + y. [para(19(a,1),150(a,1,1,2,1,2)),rewrite([7(2)])]. given #714 (T,wt=22): 1097 (g((x + y)' + (g(y) + (h(y) + x))') + (x + x)')' = x. [para(150(a,1),66(a,1,1,2,1,1)),rewrite([150(18),150(22)])]. given #715 (T,wt=22): 1122 (g(x) + (g(x) + (g(x) + g(x + x')))')' = g(x + x'). [para(10(a,1),192(a,1,1,1)),rewrite([10(7),10(8),6(8),7(8)])]. given #716 (A,wt=23): 302 (g(x) + (x' + (g(x) + (x' + x')'')'')')' = x'. [para(66(a,1),23(a,1,1,2,1,1)),rewrite([66(22)])]. given #717 (T,wt=22): 1186 ((x + x)' + g((x + x)' + g(g(x) + (x + x)')))' = x. [para(197(a,1),66(a,1,1,2,1,1)),rewrite([197(18),6(12),197(22)])]. given #718 (T,wt=22): 1196 ((g(x) + (y + z))' + (y + (z + (x + x')))')' = y + z. [para(7(a,1),231(a,1,1,2,1))]. given #719 (T,wt=22): 1199 ((x + (g(y) + z))' + (x + (z + (y + y')))')' = x + z. [para(19(a,1),231(a,1,1,1,1)),rewrite([7(8)])]. given #720 (T,wt=22): 1213 (g((g(x) + y)' + (y + (x + x'))') + (y + y)')' = y. [para(231(a,1),66(a,1,1,2,1,1)),rewrite([231(18),231(22)])]. given #721 (A,wt=28): 303 (g(x) + (x'' + (g(x) + (x' + x'))')')' = (g(x) + (x' + x'))'. [para(66(a,1),23(a,1,1,2,1,2,1)),rewrite([6(10)])]. given #722 (T,wt=22): 1235 ((x + (y + z))' + (z + (g(x + y) + h(x + y)))')' = z. [para(7(a,1),236(a,1,1,1,1))]. given #723 (T,wt=22): 1236 ((x + (y + z))' + (y + (z + (g(x) + h(x))))')' = y + z. [para(7(a,1),236(a,1,1,2,1))]. given #724 (T,wt=22): 1238 ((x + (y + z))' + (x + (z + (g(y) + h(y))))')' = x + z. [para(19(a,1),236(a,1,1,1,1)),rewrite([7(8)])]. given #725 (T,wt=22): 1244 (g((x + y)' + (y + (g(x) + h(x)))') + (y + y)')' = y. [para(236(a,1),66(a,1,1,2,1,1)),rewrite([236(18),236(22)])]. given #726 (A,wt=27): 305 (x + (h(x)' + (x + (h(x) + g(x)'))')')' = (x + (h(x) + g(x)'))'. [para(73(a,1),23(a,1,1,2,1,2,1)),rewrite([6(9)])]. given #727 (T,wt=22): 1275 ((x + (y + g(z)))' + (z + (x + (y + z')))')' = x + y. [para(7(a,1),647(a,1,1,1,1)),rewrite([7(7)])]. given #728 (T,wt=22): 1276 ((x + g(y + z))' + (y + (z + (x + (y + z)')))')' = x. [para(7(a,1),647(a,1,1,2,1))]. given #729 (T,wt=22): 1279 (x + (y + (x + (y' + (x + g(y))')))')' = (x + g(y))'. [para(647(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #730 (T,wt=22): 1282 ((x + g(y + y'))' + (y + (y' + (x + g(y))))')' = x. [para(10(a,1),647(a,1,1,2,1,2,2)),rewrite([7(10)])]. given #731 (A,wt=28): 306 (((x + y)' + z)' + (z + (x + ((x + y)' + (x + y')'')'))')' = z. [para(23(a,1),79(a,1,1,1,1,1))]. given #732 (T,wt=22): 1300 (g((x + g(y))' + (y + (x + y'))') + (x + x)')' = x. [para(647(a,1),66(a,1,1,2,1,1)),rewrite([647(18),647(22)])]. given #733 (T,wt=22): 1333 ((x + x)' + g(g(x) + (x + (g(x') + h(x')))'))' = x. [para(682(a,1),66(a,1,1,2,1,1)),rewrite([682(20),6(13),682(24)])]. given #734 (T,wt=22): 1372 ((x + g(y + z))' + (y + (x + (z + (y + z)')))')' = x. [para(26(a,1),36(a,1,1,2,1,2)),rewrite([6(11)])]. given #735 (T,wt=22): 1375 ((x + g(y + y'))' + (y + (x + (g(y) + y')))')' = x. [para(31(a,1),36(a,1,1,2,1,2)),rewrite([6(12)])]. given #736 (A,wt=25): 307 ((x' + y)' + (y + ((x' + y)' + (y + x)'')'')')' = y. [para(79(a,1),23(a,1,1,2,1,1)),rewrite([79(23)])]. given #737 (T,wt=22): 1376 ((x + y)' + (g(g(y) + h(y)) + (x + (y + y)'))')' = x. [para(198(a,1),36(a,1,1,2,1,2)),rewrite([6(12)])]. given #738 (T,wt=22): 1379 ((x + g(y + z))' + (y + (x + (z + (z + y)')))')' = x. [para(254(a,1),36(a,1,1,2,1,2)),rewrite([6(11)])]. given #739 (T,wt=22): 1403 ((x + h(y))' + (y + (x + (y + (h(y) + y'))'))')' = x. [para(837(a,1),36(a,1,1,2,1,2)),rewrite([6(12)])]. given #740 (T,wt=22): 1424 ((x + (y + z))' + (g(z) + (x + (y + h(z))))')' = x + y. [para(7(a,1),685(a,1,1,1,1)),rewrite([7(7)])]. given #741 (A,wt=32): 308 ((x' + y)' + (y' + (y + (x + (x' + y)'))')')' = (y + (x + (x' + y)'))'. [para(79(a,1),23(a,1,1,2,1,2,1)),rewrite([6(8),7(8),6(11),6(19),7(19)])]. given #742 (T,wt=22): 1429 ((x + (y + z))' + (g(x + z) + (y + h(x + z)))')' = y. [para(19(a,1),685(a,1,1,1,1))]. given #743 (T,wt=22): 1440 (g((x + y)' + (g(y) + (x + h(y)))') + (x + x)')' = x. [para(685(a,1),66(a,1,1,2,1,1)),rewrite([685(18),685(22)])]. given #744 (T,wt=22): 1461 ((x + (y + (z + x')))' + (g(x) + (y + z))')' = y + z. [para(7(a,1),834(a,1,1,1,1,2))]. given #745 (T,wt=22): 1462 ((x + (y + (z + (x + y)')))' + (g(x + y) + z)')' = z. [para(7(a,1),834(a,1,1,1,1))]. given #746 (A,wt=25): 309 (x + (g(x + y) + (x + (y + (x + y)')')'')')' = g(x + y). [para(26(a,1),23(a,1,1,2,1,1)),rewrite([26(18)])]. given #747 (T,wt=22): 1468 ((x + (x' + (y + g(x))))' + (g(x + x') + y)')' = y. [para(10(a,1),834(a,1,1,1,1,2,2)),rewrite([7(5)])]. given #748 (T,wt=22): 1470 ((x + (y + (z + x')))' + (y + (g(x) + z))')' = y + z. [para(19(a,1),834(a,1,1,2,1)),rewrite([7(3)])]. given #749 (T,wt=22): 1478 (x + (y + (x + (y' + (g(y) + x)')))')' = (g(y) + x)'. [para(834(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #750 (T,wt=22): 1487 (g((x + (y + x'))' + (g(x) + y)') + (y + y)')' = y. [para(834(a,1),66(a,1,1,2,1,1)),rewrite([834(18),834(22)])]. given #751 (A,wt=31): 310 (x + ((x + y)' + (x + ((x + y)' + (x + y')'')'')'')')' = (x + y)'. [para(23(a,1),23(a,1,1,2,1,1)),rewrite([23(28)])]. given #752 (T,wt=22): 1522 ((x + x)' + g(h(x) + (x + (x + (h(x) + x')))'))' = x. [para(883(a,1),66(a,1,1,2,1,1)),rewrite([883(18),6(12),883(22)])]. given #753 (T,wt=22): 1534 ((x + (y + z))' + (g(x + y) + (z + h(x + y)))')' = z. [para(7(a,1),919(a,1,1,1,1))]. given #754 (T,wt=22): 1535 ((x + (y + z))' + (g(x) + (y + (z + h(x))))')' = y + z. [para(7(a,1),919(a,1,1,2,1,2))]. given #755 (T,wt=22): 1540 ((x + (y + z))' + (g(y) + (x + (z + h(y))))')' = x + z. [para(19(a,1),919(a,1,1,1,1)),rewrite([7(7)])]. given #756 (A,wt=23): 313 (x + (g(x) + (x' + g(x + x'))))' = g(x + (g(x) + x')). [para(31(a,1),10(a,1,1,2)),rewrite([6(8),19(8),19(7),6(6)])]. given #757 (T,wt=22): 1548 (g((x + y)' + (g(x) + (y + h(x)))') + (y + y)')' = y. [para(919(a,1),66(a,1,1,2,1,1)),rewrite([919(18),919(22)])]. given #758 (T,wt=22): 1585 ((g(x) + (y + z))' + (x + (y + (z + x')))')' = y + z. [para(7(a,1),982(a,1,1,2,1,2))]. given #759 (T,wt=22): 1586 ((g(x + y) + z)' + (x + (y + (z + (x + y)')))')' = z. [para(7(a,1),982(a,1,1,2,1))]. given #760 (T,wt=22): 1589 ((g(x + x') + y)' + (x + (x' + (y + g(x))))')' = y. [para(10(a,1),982(a,1,1,2,1,2,2)),rewrite([7(10)])]. given #761 (A,wt=35): 314 (x + (x + (x + (g(x) + (h(x) + g(x + (x + (x + g(x)))))))))' = g(x + (x + (x + (g(x) + h(x))))). [para(12(a,1),31(a,1,1,2,2)),rewrite([6(11),19(12),7(11),7(10),7(9),19(12),19(11),19(10),19(9),12(22),6(19),19(19),19(18),19(17),6(16)])]. given #762 (T,wt=22): 1591 ((x + (g(y) + z))' + (y + (x + (z + y')))')' = x + z. [para(19(a,1),982(a,1,1,1,1)),rewrite([7(7)])]. given #763 (T,wt=22): 1606 (g((g(x) + y)' + (x + (y + x'))') + (y + y)')' = y. [para(982(a,1),66(a,1,1,2,1,1)),rewrite([982(18),982(22)])]. given #764 (T,wt=22): 1778 ((x + (y + (z + (x + z)')))' + (g(x + z) + y)')' = y. [para(26(a,1),91(a,1,1,2,1,1))]. given #765 (T,wt=22): 1782 ((x + (y + (g(x) + x')))' + (g(x + x') + y)')' = y. [para(31(a,1),91(a,1,1,2,1,1))]. given #766 (A,wt=30): 315 (x + (g(x) + ((x + x)' + g(g(x) + (x + x)'))))' = g(x + (g(x) + (x + x)')). [para(29(a,1),31(a,1,1,2,2)),rewrite([6(10),19(11),7(10),29(21),6(17)])]. given #767 (T,wt=22): 1783 ((x + y)' + (g(g(x) + h(x)) + (y + (x + x)'))')' = y. [para(198(a,1),91(a,1,1,2,1,1)),rewrite([6(12)])]. given #768 (T,wt=22): 1785 ((x + (y + (z + (z + x)')))' + (g(x + z) + y)')' = y. [para(254(a,1),91(a,1,1,2,1,1))]. given #769 (T,wt=22): 1808 ((x + (y + (x + (h(x) + x'))'))' + (h(x) + y)')' = y. [para(837(a,1),91(a,1,1,2,1,1))]. given #770 (T,wt=22): 1978 ((g(x + y) + z)' + (x + (z + (y + (x + y)')))')' = z. [para(26(a,1),234(a,1,1,1,1,1))]. given #771 (A,wt=24): 316 (x + (g(x) + (h(x) + g(g(x) + h(x)))))' = g(x + (g(x) + h(x))). [para(42(a,1),31(a,1,1,2,2)),rewrite([6(8),19(9),7(8),42(17),6(14)])]. given #772 (T,wt=22): 1981 ((g(x + x') + y)' + (x + (y + (g(x) + x')))')' = y. [para(31(a,1),234(a,1,1,1,1,1))]. given #773 (T,wt=22): 1982 ((g(x + y) + z)' + (x + (z + (y + (y + x)')))')' = z. [para(254(a,1),234(a,1,1,1,1,1))]. given #774 (T,wt=22): 1994 ((h(x) + y)' + (x + (y + (x + (h(x) + x'))'))')' = y. [para(837(a,1),234(a,1,1,1,1,1))]. given #775 (T,wt=22): 2003 (x + (g(x) + (x + (g(x) + (x + x)''))'')')' = g(x). [para(369(a,1),8(a,1,1,1))]. given #776 (A,wt=33): 317 (g(x + (g(x) + x')) + (x + (g(x) + (x' + g(x + x')')))')' = x + (g(x) + x'). [para(31(a,1),27(a,1,1,2,1,2,1)),rewrite([7(14),7(13)])]. given #777 (T,wt=22): 2045 (x + (g(x) + (x + (x + (g(x) + x'')))'')')' = g(x). [para(485(a,1),8(a,1,1,1))]. given #778 (T,wt=22): 2159 (x + (g(x) + (g(h(x)) + (h(x) + h(x)'')'))')' = g(x). [para(42(a,1),48(a,1,1,1))]. given #779 (T,wt=22): 2221 ((x + ((y + x)' + (z + y)))' + (z + g(y + x))')' = z. [para(26(a,1),1345(a,1,1,2,1,2)),rewrite([7(5)])]. given #780 (T,wt=22): 2224 ((g(x) + (x' + (y + x)))' + (y + g(x + x'))')' = y. [para(31(a,1),1345(a,1,1,2,1,2)),rewrite([7(5)])]. given #781 (A,wt=27): 321 (g(x' + x'') + (x + (g(x') + x''))')' = g(x') + x''. [para(31(a,1),21(a,1,1,2)),rewrite([6(6),6(13)])]. given #782 (T,wt=22): 2225 ((x + y)' + ((y + y)' + (x + g(g(y) + h(y))))')' = x. [para(198(a,1),1345(a,1,1,2,1,2)),rewrite([6(12)])]. given #783 (T,wt=22): 2227 ((x + ((x + y)' + (z + y)))' + (z + g(y + x))')' = z. [para(254(a,1),1345(a,1,1,2,1,2)),rewrite([7(5)])]. given #784 (T,wt=22): 2247 (((x + (h(x) + x'))' + (y + x))' + (y + h(x))')' = y. [para(837(a,1),1345(a,1,1,2,1,2))]. given #785 (T,wt=22): 2295 ((x' + (y + (z + x)))' + (y + (z + g(x)))')' = y + z. [para(7(a,1),2198(a,1,1,1,1,2)),rewrite([7(8)])]. given #786 (A,wt=28): 325 ((x + (y + g(z + z')))' + (x + (y + (z + (g(z) + z'))))')' = x + y. [para(31(a,1),22(a,1,1,2,1,2,2)),rewrite([6(14)])]. given #787 (T,wt=22): 2300 ((g(x) + (y + (x + x')))' + (y + g(x + x'))')' = y. [para(10(a,1),2198(a,1,1,1,1,1))]. given #788 (T,wt=22): 2302 ((x + ((x + y)' + (z + y)))' + (z + g(x + y))')' = z. [para(19(a,1),2198(a,1,1,1,1,2)),rewrite([19(5)])]. given #789 (T,wt=22): 2308 (x + (y' + (x + (y + (x + g(y))')))')' = (x + g(y))'. [para(2198(a,1),21(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #790 (T,wt=22): 2317 (g((x' + (y + x))' + (y + g(x))') + (y + y)')' = y. [para(2198(a,1),66(a,1,1,2,1,1)),rewrite([2198(18),2198(22)])]. given #791 (A,wt=28): 327 (g(x + (g(x) + x')) + (g(x + x') + g(x + x'))')' = g(x + x'). [para(31(a,1),66(a,1,1,2,1,1)),rewrite([31(13),31(20)])]. given #792 (T,wt=22): 2348 ((x + (y + z))' + (h(z) + (x + (y + g(z))))')' = x + y. [para(7(a,1),2203(a,1,1,1,1)),rewrite([7(7)])]. given #793 (T,wt=22): 2353 ((x + (y + z))' + (h(x + z) + (y + g(x + z)))')' = y. [para(19(a,1),2203(a,1,1,1,1))]. given #794 (T,wt=22): 2364 (g((x + y)' + (h(y) + (x + g(y)))') + (x + x)')' = x. [para(2203(a,1),66(a,1,1,2,1,1)),rewrite([2203(18),2203(22)])]. given #795 (T,wt=22): 2395 ((g(x) + (y + z))' + (x' + (y + (z + x)))')' = y + z. [para(7(a,1),2293(a,1,1,2,1,2))]. given #796 (A,wt=26): 329 (x + (g(x + x') + (x + (g(x) + x')')'')')' = g(x + x'). [para(31(a,1),23(a,1,1,2,1,1)),rewrite([31(19)])]. given #797 (T,wt=22): 2398 (x + (y' + (x + (y + (g(y) + x)')))')' = (g(y) + x)'. [para(2293(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. given #798 (T,wt=22): 2400 ((g(x + x') + y)' + (g(x) + (y + (x + x')))')' = y. [para(10(a,1),2293(a,1,1,2,1,1))]. given #799 (T,wt=22): 2402 ((x + (g(y) + z))' + (y' + (x + (z + y)))')' = x + z. [para(19(a,1),2293(a,1,1,1,1)),rewrite([7(7)])]. given #800 (T,wt=22): 2403 ((g(x + y) + z)' + (x + ((x + y)' + (z + y)))')' = z. [para(19(a,1),2293(a,1,1,2,1,2)),rewrite([19(9)])]. given #801 (A,wt=35): 330 (x + ((x + (y + (g(y) + y')))' + (x + g(y + y'))'')')' = (x + (y + (g(y) + y')))'. [para(31(a,1),23(a,1,1,2,1,2,1,1,2))]. given #802 (T,wt=22): 2417 (g((g(x) + y)' + (x' + (y + x))') + (y + y)')' = y. [para(2293(a,1),66(a,1,1,2,1,1)),rewrite([2293(18),2293(22)])]. given #803 (T,wt=22): 2449 ((x + (y + g(z)))' + (z' + (x + (y + z)))')' = x + y. [para(7(a,1),2294(a,1,1,1,1)),rewrite([7(7)])]. given #804 (T,wt=22): 2451 ((x + g(y + y'))' + (g(y) + (x + (y + y')))')' = x. [para(10(a,1),2294(a,1,1,2,1,1))]. given #805 (T,wt=22): 2453 ((x + g(y + z))' + (y + ((y + z)' + (x + z)))')' = x. [para(19(a,1),2294(a,1,1,2,1,2)),rewrite([19(9)])]. given #806 (A,wt=24): 331 (g(g(x + y) + h(x + y)) + (x + (y + (x + y)))')' = x + y. [para(7(a,1),198(a,1,1,2,1))]. given #807 (T,wt=22): 2468 (g((x + g(y))' + (y' + (x + y))') + (x + x)')' = x. [para(2294(a,1),66(a,1,1,2,1,1)),rewrite([2294(18),2294(22)])]. given #808 (T,wt=22): 2488 ((x + (y + z))' + (h(x + y) + (z + g(x + y)))')' = z. [para(7(a,1),2347(a,1,1,1,1))]. given #809 (T,wt=22): 2489 ((x + (y + z))' + (h(x) + (y + (z + g(x))))')' = y + z. [para(7(a,1),2347(a,1,1,2,1,2))]. given #810 (T,wt=22): 2494 ((x + (y + z))' + (h(y) + (x + (z + g(y))))')' = x + z. [para(19(a,1),2347(a,1,1,1,1)),rewrite([7(7)])]. given #811 (A,wt=23): 332 (x + (g(g(x) + h(x)) + (x + x)'')')' = g(g(x) + h(x)). [para(198(a,1),8(a,1,1,1))]. given #812 (T,wt=22): 2502 (g((x + y)' + (h(x) + (y + g(x)))') + (y + y)')' = y. [para(2347(a,1),66(a,1,1,2,1,1)),rewrite([2347(18),2347(22)])]. given #813 (T,wt=22): 2594 (x + (g(x) + (h(x) + g(g(x) + (x + x)')')'))' = h(x). [para(1653(a,1),8(a,1,1,1)),rewrite([7(12)])]. given #814 (T,wt=22): 2610 (x + (g(x) + (x + (g(x) + (h(x) + (x + x)')))'))' = h(x). [para(1653(a,1),28(a,1,1,1)),rewrite([29(12),6(8),19(9),19(8),7(11)])]. given #815 (T,wt=8): 22398 (x + h(x))' = g(x). [para(2610(a,1),36(a,1,1,1)),rewrite([679(12),29(6),6(2)])]. given #816 (A,wt=24): 350 (x + (y + (g(x + y) + (y + x)')))' = g(x + (y + (y + x)')). [para(254(a,1),10(a,1,1,2)),rewrite([6(7),19(7),19(6)])]. given #817 (T,wt=12): 22418 (g(x) + (x + h(x)')')' = x. [para(22398(a,1),8(a,1,1,1))]. Low Water (displace, True_semantics): id=17247, wt=31 given #818 (T,wt=12): 22420 g(g(x) + h(x)) = g(x + h(x)). [para(22398(a,1),10(a,1,1,2)),rewrite([6(4),19(4),45(5)])]. given #819 (T,wt=13): 22399 (g(x) + (h(x) + x')')' = h(x). [para(2610(a,1),276(a,1,1,2,1,1)),rewrite([679(13),29(7),19(18),2610(19)])]. given #820 (T,wt=13): 22478 (g(x + h(x)) + (x + x)')' = x. [para(22398(a,1),256(a,1,1,2,1,2,1,2)),rewrite([6(6),42(7)])]. given #821 (A,wt=35): 352 (g(x + (y + (y + x)')) + (x + (y + ((y + x)' + g(x + y)')))')' = x + (y + (y + x)'). [para(254(a,1),27(a,1,1,2,1,2,1)),rewrite([7(13),7(12)])]. given #822 (T,wt=14): 22417 (x + (y + h(x + y)))' = g(x + y). [para(7(a,1),22398(a,1,1))]. given #823 (T,wt=14): 23018 (x + (g(x) + h(x)))' = g(x + h(x)). [back_rewrite(45),rewrite([22420(9)])]. given #824 (T,wt=14): 23021 (h(x) + (x + (x + g(x))')')' = x. [back_rewrite(21312),rewrite([22493(11)])]. given #825 (T,wt=10): 23594 (x + (x + g(x)))' = h(x). [para(23021(a,1),109(a,1,1,1,1)),rewrite([23021(16),23021(16),23021(16),6(13),19(13),22532(16),23021(9),23021(9),23021(9)]),flip(a)]. given #826 (A,wt=23): 353 (g(x + y) + (x' + (y + (y + x)'))')' = y + (y + x)'. [para(254(a,1),20(a,1,1,1)),rewrite([6(7)])]. given #827 (T,wt=14): 23362 (x + (y + h(y + x)))' = g(x + y). [para(6(a,1),22417(a,1,1,2,2,1))]. given #828 (T,wt=14): 23845 (x + (x + (h(x) + h(x)))')' = h(x). [back_rewrite(570),rewrite([23594(5)])]. given #829 (T,wt=14): 23846 (h(x) + g(x + x'))' = x + g(x). [back_rewrite(326),rewrite([23594(7),6(5)])]. given #830 (T,wt=15): 22424 (g(x') + (x + h(x'))')' = h(x'). [para(22398(a,1),21(a,1,1,2)),rewrite([6(3),6(7)])]. given #831 (A,wt=25): 356 (g(x' + y) + (x + (y + (y + x')'))')' = y + (y + x')'. [para(254(a,1),21(a,1,1,2)),rewrite([6(5),6(10)])]. given #832 (T,wt=15): 22439 (x + (x + (g(x) + h(x)'))')' = g(x). [para(22398(a,1),25(a,1,1,2,1,2,2)),rewrite([6(4),22398(11)])]. given #833 (T,wt=12): 24552 (x + (g(x) + h(x)'))' = h(x). [para(22439(a,1),94(a,1,1,2)),rewrite([6(10),7(10),6(13),24379(14)]),flip(a)]. ============================== PROOF ================================= % Proof 1 at 87.93 (+ 0.26) seconds: Winker2a. % Length of proof is 35. % Level of proof is 12. % Maximum clause weight is 23. % Given clauses 833. 1 (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')'. [assumption]. 10 (x + x')' = g(x). [copy(9),flip(a)]. 11 h(x) = (x + (x + (x + g(x))))'. [assumption]. 12 (x + (x + (x + g(x))))' = h(x). [copy(11),flip(a)]. 13 (x + y)' != x' # answer(Winker2a). [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))]. 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 ((x + g(y))' + (x + (y + y'))')' = x. [para(10(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])]. 29 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. 33 (h(x) + (x + (x + (x + g(x)))')')' = x. [para(12(a,1),8(a,1,1,1))]. 36 ((x + (y + z))' + (y + (x + z)')')' = y. [para(19(a,1),8(a,1,1,1,1))]. 40 (x + (x + (x + g(x)))')' = g(x). [para(29(a,1),8(a,1,1,2)),rewrite([19(3),6(2),6(5)])]. 41 (x + (g(x) + (x + x)'))' = g(g(x) + (x + x)'). [para(29(a,1),10(a,1,1,2)),rewrite([6(5)])]. 42 (g(x) + h(x))' = x. [back_rewrite(33),rewrite([40(7),6(3)])]. 43 (x + (g(x) + h(x)')')' = g(x). [para(42(a,1),8(a,1,1,1))]. 44 ((x + y)' + (x + (g(y) + h(y)))')' = x. [para(42(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])]. 58 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),20(a,1,1,1,1))]. 94 ((x + (g(y) + h(y)))' + (y + x)')' = x. [para(42(a,1),21(a,1,1,2,1,1))]. 113 (g(x) + (x + (g(x) + h(x)'))')' = x. [para(43(a,1),8(a,1,1,2)),rewrite([6(8)])]. 679 (x + (x + (g(y) + (h(y) + (x + y)')))')' = (x + y)'. [para(44(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. 1653 (h(x) + g(g(x) + (x + x)'))' = x + g(x). [para(12(a,1),58(a,1,1,1)),rewrite([7(6),41(7)])]. 2610 (x + (g(x) + (x + (g(x) + (h(x) + (x + x)')))'))' = h(x). [para(1653(a,1),28(a,1,1,1)),rewrite([29(12),6(8),19(9),19(8),7(11)])]. 22398 (x + h(x))' = g(x). [para(2610(a,1),36(a,1,1,1)),rewrite([679(12),29(6),6(2)])]. 22424 (g(x') + (x + h(x'))')' = h(x'). [para(22398(a,1),21(a,1,1,2)),rewrite([6(3),6(7)])]. 22439 (x + (x + (g(x) + h(x)'))')' = g(x). [para(22398(a,1),25(a,1,1,2,1,2,2)),rewrite([6(4),22398(11)])]. 24379 (g(x) + (g(x) + (h(x) + (x + (g(x) + h(x)'))'))')' = h(x). [para(113(a,1),22424(a,1,1,1,1)),rewrite([113(18),6(11),19(11),113(23)])]. 24552 (x + (g(x) + h(x)'))' = h(x). [para(22439(a,1),94(a,1,1,2)),rewrite([6(10),7(10),6(13),24379(14)]),flip(a)]. 24581 (h(x) + (h(x)' + (x + g(x))')')' = h(x)'. [para(24552(a,1),58(a,1,1,1))]. 24582 $F # answer(Winker2a). [resolve(24581,a,13,a)]. ============================== end of proof ========================== % Redundant proof: 24773 $F # answer(Winker2a). [resolve(24772,a,13,a)]. Low Water (displace, True_semantics): id=19074, wt=30 % Disable descendants (x means already disabled): 13 given #834 (T,wt=14): 24560 (h(x) + g(x + h(x)))' = x + g(x). [para(22439(a,1),353(a,1,1,2,1,2,2)),rewrite([24552(6),6(2),24552(9),6(8),7(8),24552(9),6(5),24552(12),22398(9)])]. given #835 (T,wt=16): 22419 ((x + g(y))' + (x + (y + h(y)))')' = x. [para(22398(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])]. given #836 (A,wt=28): 360 ((x + (y + g(z + u)))' + (x + (y + (z + (u + (u + z)'))))')' = x + y. [para(254(a,1),22(a,1,1,2,1,2,2)),rewrite([6(13)])]. given #837 (T,wt=16): 22422 ((x + (h(x) + y))' + (y + g(x))')' = y. [para(22398(a,1),20(a,1,1,2,1,2)),rewrite([7(3)])]. given #838 (T,wt=16): 22423 ((x + (y + h(y)))' + (g(y) + x)')' = x. [para(22398(a,1),21(a,1,1,2,1,1))]. given #839 (T,wt=16): 22425 ((g(x) + y)' + (x + (h(x) + y))')' = y. [para(22398(a,1),56(a,1,1,2,1,1)),rewrite([7(3),6(8)])]. given #840 (T,wt=16): 22426 ((x + g(y))' + (y + (h(y) + x))')' = x. [para(22398(a,1),57(a,1,1,1,1,2)),rewrite([7(6)])]. given #841 (A,wt=26): 362 (g(x + (y + (y + x)')) + (g(x + y) + g(x + y))')' = g(x + y). [para(254(a,1),66(a,1,1,2,1,1)),rewrite([254(12),254(18)])]. given #842 (T,wt=16): 22428 (g(x + h(x)) + (g(x) + g(x))')' = g(x). [para(22398(a,1),66(a,1,1,2,1,1)),rewrite([22398(7),22398(12)])]. given #843 (T,wt=16): 22429 ((g(x) + y)' + (y + (x + h(x)))')' = y. [para(22398(a,1),79(a,1,1,1,1,1))]. given #844 (T,wt=16): 22441 (g(x) + (x + (g(h(x)) + h(h(x))))')' = x. [para(22398(a,1),44(a,1,1,1))]. given #845 (T,wt=16): 22447 (g(x) + (g(x) + (h(x) + h(x)))')' = h(x). [para(22398(a,1),94(a,1,1,2)),rewrite([19(5),6(8)])]. given #846 (A,wt=24): 364 (x + (y + (g(y + x) + (y + x)')))' = g(y + (x + (y + x)')). [para(26(a,1),254(a,1,1,2,2)),rewrite([6(7),19(7),7(6),6(12)])]. given #847 (T,wt=16): 22457 ((x + g(y))' + (y + (x + h(y)))')' = x. [para(22398(a,1),36(a,1,1,2,1,2)),rewrite([6(8)])]. given #848 (T,wt=16): 22461 ((x + (y + h(x)))' + (g(x) + y)')' = y. [para(22398(a,1),91(a,1,1,2,1,1))]. given #849 (T,wt=16): 22463 ((g(x) + y)' + (x + (y + h(x)))')' = y. [para(22398(a,1),234(a,1,1,1,1,1))]. given #850 (T,wt=16): 22465 ((h(x) + (y + x))' + (y + g(x))')' = y. [para(22398(a,1),1345(a,1,1,2,1,2))]. given #851 (A,wt=25): 365 (x + (g(x + y) + (x + (y + (y + x)')')'')')' = g(x + y). [para(254(a,1),23(a,1,1,2,1,1)),rewrite([254(18)])]. given #852 (T,wt=16): 22470 ((g(x) + y)' + (h(x) + (y + x))')' = y. [para(22398(a,1),1746(a,1,1,2,1,1)),rewrite([6(8)])]. given #853 (T,wt=16): 22471 ((x + g(y))' + (h(y) + (x + y))')' = x. [para(22398(a,1),1919(a,1,1,1,1,2))]. given #854 (T,wt=16): 22473 (h(x) + (g(x) + (h(x) + x'))')' = g(x). [para(22398(a,1),62(a,1,1,2,1,2,2)),rewrite([6(5),19(6),22398(12)])]. given #855 (T,wt=16): 23803 (h(x) + (x + (x + (h(x) + h(x))))')' = x. [back_rewrite(10244),rewrite([23594(6)])]. given #856 (A,wt=24): 366 (x + (y + (g(y + x) + (x + y)')))' = g(y + (x + (x + y)')). [para(254(a,1),254(a,1,1,2,2)),rewrite([6(7),19(7),7(6),6(12)])]. given #857 (T,wt=16): 23856 (h(x) + (x + (x + g(x)'))')' = x + x. [para(23594(a,1),22(a,1,1,1))]. given #858 (T,wt=17): 22430 (x + (g(x) + (x + h(x)')'')')' = g(x). [para(22398(a,1),23(a,1,1,2,1,1)),rewrite([22398(13)])]. given #859 (T,wt=17): 22450 (g(x) + (x + (x + (x + (x + g(x)))))')' = x. [para(22398(a,1),34(a,1,1,1))]. given #860 (T,wt=17): 22571 (g(x) + (x + (x + (g(x) + h(x)')))')' = x. [para(22398(a,1),566(a,1,1,1)),rewrite([22398(6),6(5)])]. given #861 (A,wt=25): 367 (x + (y + (g(x + y) + (x + (y + (x + y)))'')'))' = g(x + y). [para(7(a,1),38(a,1,1,2,1,2,1,1)),rewrite([7(11)])]. given #862 (T,wt=17): 23020 (x + (x + (h(x) + (x + g(x))'))')' = h(x). [back_rewrite(21313),rewrite([22493(11)])]. given #863 (T,wt=17): 24006 (h(x) + (x + (x + (x + x')))')' = x + x. [para(23594(a,1),169(a,1,1,1))]. given #864 (T,wt=18): 22437 (g(g(x)) + (x + (h(x) + g(x)'))')' = g(x)'. [para(22398(a,1),88(a,1,1,1,1)),rewrite([22398(7),7(7),22398(13)])]. given #865 (T,wt=18): 22445 (g(g(x)) + (x + (h(g(x)) + x'))')' = h(g(x)). [para(22398(a,1),87(a,1,1,2)),rewrite([19(5),6(9)])]. given #866 (A,wt=23): 368 ((x + g(y))' + (x + (y + (g(y) + (y + y)'')'))')' = x. [para(38(a,1),8(a,1,1,2,1,2)),rewrite([6(13)])]. given #867 (T,wt=18): 22475 (g(x) + (g(x) + (h(x) + (x + x)'))')' = h(x). [para(22398(a,1),93(a,1,1,2)),rewrite([19(6),6(9)])]. given #868 (T,wt=18): 22481 (h(x) + (g(x) + (h(x) + x')'')')' = g(x). [para(22398(a,1),60(a,1,1,2,1,1)),rewrite([22398(14)])]. given #869 (T,wt=18): 22506 ((x + x)' + g(g(x) + (x + h(x)')'))' = x. [para(22398(a,1),193(a,1,1,1,1,1)),rewrite([6(10)])]. given #870 (T,wt=18): 22622 (g(x) + (x + (x + (h(x) + g(x)')'))')' = x. [para(22398(a,1),216(a,1,1,1))]. given #871 (A,wt=28): 370 (x + (g(x) + (g(x) + (x + x)'')'))' = g(x + (g(x) + (x + x)'')'). [para(38(a,1),10(a,1,1,2)),rewrite([6(9),19(9)])]. given #872 (T,wt=18): 23364 (g(x + y) + (x + (y + h(x + y))')')' = x. [para(22417(a,1),8(a,1,1,1))]. given #873 (T,wt=18): 23385 (g(x + y) + (y + (x + h(x + y))')')' = y. [para(22417(a,1),36(a,1,1,1))]. given #874 (T,wt=18): 23632 (g(g(x)) + (x + (h(x) + h(g(x))))')' = h(g(x)). [back_rewrite(22573),rewrite([23594(8),6(6)])]. given #875 (T,wt=18): 23739 (x + (x + (h(x) + (x + x)'))')' = (x + x)'. [back_rewrite(16072),rewrite([23594(6),6(4)])]. given #876 (A,wt=27): 371 (g(x) + (x' + (g(x) + (x + x)'')')')' = (g(x) + (x + x)'')'. [para(38(a,1),20(a,1,1,1)),rewrite([6(9)])]. given #877 (T,wt=18): 23805 (h(x) + (x + (x + (h(x) + h(x)))'')')' = x. [back_rewrite(10242),rewrite([23594(6)])]. Low Water (keep, True_semantics): wt=28 given #878 (T,wt=18): 23847 (x + (y + (x + (y + g(x + y)))))' = h(x + y). [para(7(a,1),23594(a,1,1,2)),rewrite([19(6),19(5),7(4)])]. given #879 (T,wt=18): 23848 ((x + h(y))' + (x + (y + (y + g(y))))')' = x. [para(23594(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. given #880 (T,wt=16): 25450 (x + (x + (x + (g(x) + g(x))))')' = g(x). [para(42(a,1),23848(a,1,1,1)),rewrite([19(5),19(4)])]. given #881 (A,wt=23): 372 ((x + ((g(x) + (x + x)'')' + y))' + (y + g(x))')' = y. [para(38(a,1),20(a,1,1,2,1,2)),rewrite([7(8)])]. given #882 (T,wt=18): 23849 (x + (x + (g(x) + h(x))))' = g(x + (x + g(x))). [para(23594(a,1),10(a,1,1,2)),rewrite([6(5),19(5),19(4),6(3)])]. given #883 (T,wt=18): 23851 ((x + (x + (g(x) + y)))' + (y + h(x))')' = y. [para(23594(a,1),20(a,1,1,2,1,2)),rewrite([7(4),7(3)])]. given #884 (T,wt=18): 23852 ((x + (y + (y + g(y))))' + (h(y) + x)')' = x. [para(23594(a,1),21(a,1,1,2,1,1))]. given #885 (T,wt=18): 23854 ((x + (x + (g(x) + y)))' + (h(x) + y)')' = y. [para(23594(a,1),56(a,1,1,2,1,1)),rewrite([7(4),7(3)])]. given #886 (A,wt=23): 373 ((x + (y + (g(y) + (y + y)'')'))' + (g(y) + x)')' = x. [para(38(a,1),21(a,1,1,2,1,1))]. given #887 (T,wt=18): 23855 ((x + h(y))' + (y + (y + (g(y) + x)))')' = x. [para(23594(a,1),57(a,1,1,1,1,2)),rewrite([7(7),7(6)])]. given #888 (T,wt=18): 23858 (g(x + (x + g(x))) + (h(x) + h(x))')' = h(x). [para(23594(a,1),66(a,1,1,2,1,1)),rewrite([23594(9),23594(14)])]. given #889 (T,wt=18): 23859 ((h(x) + y)' + (y + (x + (x + g(x))))')' = y. [para(23594(a,1),79(a,1,1,1,1,1))]. given #890 (T,wt=18): 23875 ((x + h(y))' + (y + (x + (y + g(y))))')' = x. [para(23594(a,1),36(a,1,1,2,1,2)),rewrite([6(9)])]. given #891 (A,wt=33): 374 (g(x') + (x + (g(x') + (x' + x')'')')')' = (g(x') + (x' + x')'')'. [para(38(a,1),21(a,1,1,2)),rewrite([6(10),6(14)])]. given #892 (T,wt=18): 23879 ((x + (y + (x + g(x))))' + (h(x) + y)')' = y. [para(23594(a,1),91(a,1,1,2,1,1))]. given #893 (T,wt=18): 23880 ((h(x) + y)' + (x + (y + (x + g(x))))')' = y. [para(23594(a,1),234(a,1,1,1,1,1))]. given #894 (T,wt=18): 23882 ((x + (g(x) + (y + x)))' + (y + h(x))')' = y. [para(23594(a,1),1345(a,1,1,2,1,2)),rewrite([7(4)])]. given #895 (T,wt=18): 23886 ((x + (g(x) + (y + x)))' + (h(x) + y)')' = y. [para(23594(a,1),1746(a,1,1,2,1,1)),rewrite([7(4)])]. given #896 (A,wt=23): 375 ((g(x) + y)' + (x + ((g(x) + (x + x)'')' + y))')' = y. [para(38(a,1),56(a,1,1,2,1,1)),rewrite([7(8),6(13)])]. given #897 (T,wt=18): 23887 ((x + h(y))' + (y + (g(y) + (x + y)))')' = x. [para(23594(a,1),1919(a,1,1,1,1,2)),rewrite([7(7)])]. given #898 (T,wt=18): 23888 ((h(x) + y)' + (x + (g(x) + (y + x)))')' = y. [para(23594(a,1),1959(a,1,1,1,1,1)),rewrite([7(7)])]. given #899 (T,wt=18): 24029 ((x + (x + (y + g(x))))' + (y + h(x))')' = y. [para(23594(a,1),1348(a,1,1,2,1,2))]. given #900 (T,wt=18): 24040 ((x + (x + (y + g(x))))' + (h(x) + y)')' = y. [para(23594(a,1),1748(a,1,1,2,1,1))]. given #901 (A,wt=23): 376 ((x + g(y))' + (y + ((g(y) + (y + y)'')' + x))')' = x. [para(38(a,1),57(a,1,1,1,1,2)),rewrite([7(11)])]. given #902 (T,wt=18): 24053 ((h(x) + y)' + (x + (x + (y + g(x))))')' = y. [para(23594(a,1),1961(a,1,1,1,1,1))]. given #903 (T,wt=18): 24055 ((x + h(y))' + (g(y) + (x + (y + y)))')' = x. [para(23594(a,1),2192(a,1,1,2,1,2)),rewrite([6(9)])]. given #904 (T,wt=18): 24060 ((x + h(y))' + (y + (y + (x + g(y))))')' = x. [para(23594(a,1),2517(a,1,1,1,1,2))]. given #905 (T,wt=18): 24061 ((g(x) + (y + (x + x)))' + (h(x) + y)')' = y. [para(23594(a,1),2669(a,1,1,2,1,1))]. given #906 (A,wt=29): 377 ((x + (y + g(z)))' + (x + (y + (z + (g(z) + (z + z)'')')))')' = x + y. [para(38(a,1),22(a,1,1,2,1,2,2)),rewrite([6(15)])]. given #907 (T,wt=18): 24067 ((h(x) + y)' + (g(x) + (y + (x + x)))')' = y. [para(23594(a,1),2857(a,1,1,1,1,1))]. given #908 (T,wt=18): 24114 (g(x + y) + (x + (y + h(y + x))')')' = x. [para(23362(a,1),8(a,1,1,1))]. given #909 (T,wt=18): 24138 (g(x + y) + (y + (x + h(y + x))')')' = y. [para(23362(a,1),36(a,1,1,1))]. given #910 (T,wt=18): 24581 (h(x) + (h(x)' + (x + g(x))')')' = h(x)'. [para(24552(a,1),58(a,1,1,1))]. given #911 (A,wt=23): 378 ((g(x) + g(x))' + g(x + (g(x) + (x + x)'')'))' = g(x). [para(38(a,1),66(a,1,1,2,1,1)),rewrite([38(17),6(13),38(22)])]. given #912 (T,wt=18): 24687 g(h(x) + g(x + h(x))) = g(x + (g(x) + h(x))). [para(24552(a,1),168(a,1,1,2,2,2)),rewrite([23018(6),6(6),22432(9),23018(10),24552(14),6(10)]),flip(a)]. given #913 (T,wt=18): 25388 (x + (y + (x + (y + g(y + x)))))' = h(x + y). [para(6(a,1),23847(a,1,1,2,2,2,2,1))]. given #914 (T,wt=18): 25393 (x + (y + (y + (x + g(x + y)))))' = h(x + y). [para(19(a,1),23847(a,1,1,2,2))]. given #915 (T,wt=18): 25394 (x + (x + (y + (y + g(x + y)))))' = h(x + y). [para(19(a,1),23847(a,1,1,2))]. given #916 (A,wt=23): 379 ((g(x) + y)' + (y + (x + (g(x) + (x + x)'')'))')' = y. [para(38(a,1),79(a,1,1,1,1,1))]. given #917 (T,wt=18): 25395 (x + (y + (y + (x + g(y + x)))))' = h(y + x). [para(19(a,1),23847(a,1,1))]. given #918 (T,wt=18): 25456 (g(x) + (x + (x + (x + (g(x) + g(x)))))')' = x. [para(25450(a,1),8(a,1,1,2)),rewrite([6(9)])]. given #919 (T,wt=15): 25936 (x + (x + (x + (g(x) + g(x)))))' = h(x). [para(25456(a,1),22424(a,1,1,1,1)),rewrite([25456(20),6(12),19(12),2895(15),25456(17)])]. given #920 (T,wt=12): 25950 x + (g(x) + g(x)) = x + g(x). [para(25936(a,1),58(a,1,1,1)),rewrite([7(8),7(7),23892(11)]),flip(a)]. ============================== PROOF ================================= % Proof 2 at 99.69 (+ 0.28) seconds: Winker1b. % Length of proof is 52. % Level of proof is 18. % Maximum clause weight is 32. % Given clauses 920. 4 (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')'. [assumption]. 10 (x + x')' = g(x). [copy(9),flip(a)]. 11 h(x) = (x + (x + (x + g(x))))'. [assumption]. 12 (x + (x + (x + g(x))))' = h(x). [copy(11),flip(a)]. 16 x + y != y # answer(Winker1b). [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)])]. 28 ((x + g(y))' + (x + (y + y'))')' = x. [para(10(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])]. 29 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. 33 (h(x) + (x + (x + (x + g(x)))')')' = x. [para(12(a,1),8(a,1,1,1))]. 36 ((x + (y + z))' + (y + (x + z)')')' = y. [para(19(a,1),8(a,1,1,1,1))]. 40 (x + (x + (x + g(x)))')' = g(x). [para(29(a,1),8(a,1,1,2)),rewrite([19(3),6(2),6(5)])]. 41 (x + (g(x) + (x + x)'))' = g(g(x) + (x + x)'). [para(29(a,1),10(a,1,1,2)),rewrite([6(5)])]. 42 (g(x) + h(x))' = x. [back_rewrite(33),rewrite([40(7),6(3)])]. 44 ((x + y)' + (x + (g(y) + h(y)))')' = x. [para(42(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])]. 58 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),20(a,1,1,1,1))]. 62 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(20(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 84 ((x + ((y + z)' + (y + z')'))' + (y + x)')' = x. [para(8(a,1),21(a,1,1,2,1,1))]. 85 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 87 ((x + (y + y'))' + (g(y) + x)')' = x. [para(10(a,1),21(a,1,1,2,1,1))]. 93 ((x + (g(y) + (y + y)'))' + (y + x)')' = x. [para(29(a,1),21(a,1,1,2,1,1))]. 109 (g(x') + (x + (x' + (x' + g(x')))')')' = (x' + (x' + g(x')))'. [para(40(a,1),21(a,1,1,2)),rewrite([6(8),6(12)])]. 170 (h(x) + (x + (x + (x + g(x))'))')' = x + x. [para(12(a,1),22(a,1,1,1))]. 679 (x + (x + (g(y) + (h(y) + (x + y)')))')' = (x + y)'. [para(44(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. 833 (h(g(x)) + (x + (g(x) + (g(x) + (g(g(x)) + x'))))')' = g(x) + (g(x) + g(g(x))). [para(12(a,1),87(a,1,1,2)),rewrite([19(9),7(8),7(7),6(13)])]. 1653 (h(x) + g(g(x) + (x + x)'))' = x + g(x). [para(12(a,1),58(a,1,1,1)),rewrite([7(6),41(7)])]. 2610 (x + (g(x) + (x + (g(x) + (h(x) + (x + x)')))'))' = h(x). [para(1653(a,1),28(a,1,1,1)),rewrite([29(12),6(8),19(9),19(8),7(11)])]. 2895 (x + (x + (h(y) + (y + (y + (y + (g(y) + x))))'))')' = (y + (y + (y + (g(y) + x))))'. [para(12(a,1),62(a,1,1,2,1,2,1)),rewrite([7(6),7(5),7(4),7(17),7(16),7(15)])]. 3222 (x + (x + (x + (x + (h(x) + (x + g(x))')))'))' = h(x). [para(170(a,1),8(a,1,1,2)),rewrite([19(7),19(6),6(10),7(10)])]. 21312 (h(x) + (x + (x + (x + (x + (h(x) + (x + g(x))')))')')')' = x. [para(3222(a,1),8(a,1,1,1))]. 22398 (x + h(x))' = g(x). [para(2610(a,1),36(a,1,1,1)),rewrite([679(12),29(6),6(2)])]. 22424 (g(x') + (x + h(x'))')' = h(x'). [para(22398(a,1),21(a,1,1,2)),rewrite([6(3),6(7)])]. 22493 (x + (x + (y + (h(y) + (x + g(y))')))')' = (x + g(y))'. [para(22398(a,1),85(a,1,1,2,1,2,2,1,2)),rewrite([7(6),22398(13)])]. 22532 (g(x) + (h(x) + ((x + y)' + (x + y')'))')' = h(x). [para(22398(a,1),84(a,1,1,2)),rewrite([6(11)])]. 23021 (h(x) + (x + (x + g(x))')')' = x. [back_rewrite(21312),rewrite([22493(11)])]. 23594 (x + (x + g(x)))' = h(x). [para(23021(a,1),109(a,1,1,1,1)),rewrite([23021(16),23021(16),23021(16),6(13),19(13),22532(16),23021(9),23021(9),23021(9)]),flip(a)]. 23848 ((x + h(y))' + (x + (y + (y + g(y))))')' = x. [para(23594(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. 23868 (h(g(x)) + (x + (g(x) + (g(g(x)) + x')))')' = g(x) + g(g(x)). [para(23594(a,1),87(a,1,1,2)),rewrite([19(7),7(6),6(11)])]. 23892 (h(x) + (x + (g(x) + (g(x) + (x + x)')))')' = x + g(x). [para(23594(a,1),93(a,1,1,2)),rewrite([19(7),7(6),19(7),6(10)])]. 25450 (x + (x + (x + (g(x) + g(x))))')' = g(x). [para(42(a,1),23848(a,1,1,1)),rewrite([19(5),19(4)])]. 25456 (g(x) + (x + (x + (x + (g(x) + g(x)))))')' = x. [para(25450(a,1),8(a,1,1,2)),rewrite([6(9)])]. 25936 (x + (x + (x + (g(x) + g(x)))))' = h(x). [para(25456(a,1),22424(a,1,1,1,1)),rewrite([25456(20),6(12),19(12),2895(15),25456(17)])]. 25950 x + (g(x) + g(x)) = x + g(x). [para(25936(a,1),58(a,1,1,1)),rewrite([7(8),7(7),23892(11)]),flip(a)]. 25979 x + (g(x) + (g(x) + y)) = x + (g(x) + y). [para(25950(a,1),7(a,1,1)),rewrite([7(3),7(7)]),flip(a)]. 26233 g(x) + (g(x) + g(g(x))) = g(x) + g(g(x)). [back_rewrite(833),rewrite([25979(11),23868(12)]),flip(a)]. 26234 $F # answer(Winker1b). [resolve(26233,a,16,a)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 16 given #921 (A,wt=24): 380 (x + (g(x) + (x + (g(x) + (x + x)'')'')'')')' = g(x). [para(38(a,1),23(a,1,1,2,1,1)),rewrite([38(23)])]. given #922 (T,wt=14): 25996 (h(x) + g(x + g(x)))' = x + g(x). [para(25950(a,1),37(a,1,1,1,1)),rewrite([25950(10),6(9),19(9),6(8),19(8),25950(8),19(7),25950(7),23594(7),6(5),25950(10)])]. given #923 (T,wt=16): 25979 x + (g(x) + (g(x) + y)) = x + (g(x) + y). [para(25950(a,1),7(a,1,1)),rewrite([7(3),7(7)]),flip(a)]. given #924 (T,wt=16): 25983 x + (y + (g(x) + g(x))) = y + (x + g(x)). [para(25950(a,1),19(a,1,2)),flip(a)]. given #925 (T,wt=16): 26028 g(x) + (g(x) + (y + x)) = x + (g(x) + y). [para(25950(a,1),16519(a,1,1,1,1,2)),rewrite([19(9),7(8),25979(9),5523(10),7(8)]),flip(a)]. given #926 (A,wt=31): 381 (x + (g(x)' + (x + (g(x) + (x + x)''))')')' = (x + (g(x) + (x + x)''))'. [para(38(a,1),23(a,1,1,2,1,2,1)),rewrite([6(10)])]. given #927 (T,wt=16): 26233 g(x) + (g(x) + g(g(x))) = g(x) + g(g(x)). [back_rewrite(833),rewrite([25979(11),23868(12)]),flip(a)]. given #928 (T,wt=11): 26374 (g(x) + g(g(x)))' = h(g(x)). [para(26233(a,1),12(a,1,1,2)),rewrite([26233(6)])]. ============================== PROOF ================================= % Proof 3 at 100.42 (+ 0.28) seconds: Winker1a. % Length of proof is 58. % Level of proof is 20. % Maximum clause weight is 32. % Given clauses 928. 3 (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')'. [assumption]. 10 (x + x')' = g(x). [copy(9),flip(a)]. 11 h(x) = (x + (x + (x + g(x))))'. [assumption]. 12 (x + (x + (x + g(x))))' = h(x). [copy(11),flip(a)]. 15 x + y != x # answer(Winker1a). [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))]. 22 ((x + (y + z))' + (x + (y + z'))')' = x + y. [para(7(a,1),8(a,1,1,1,1)),rewrite([7(6)])]. 28 ((x + g(y))' + (x + (y + y'))')' = x. [para(10(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])]. 29 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. 33