============================== Prover9 =============================== Prover9 (32) version June-2007-, 4 June 2007. Process 10961 was started by mccune on cleo, Mon Jun 11 11:35:28 2007 The command was "prover9 -f s0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file s0.in 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). g(x) = (x + x')' # label(definition_g). h(x) = x + (x + (x + g(x))) # label(definition_h). end_of_list. formulas(goals). (x + y')' + (x' + y')' = y # answer(Huntington). (exists a exists b a + b = a) # answer(Winker1a). (exists a exists b a + b = b) # answer(Winker1b). (exists a exists b (a + b)' = a') # answer(Winker2a). (exists a exists b (a + b)' = b') # answer(Winker2b). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (x + y')' + (x' + y')' = y # answer(Huntington) # label(non_clause) # label(goal). [goal]. 2 (exists a exists b a + b = a) # answer(Winker1a) # label(non_clause) # label(goal). [goal]. 3 (exists a exists b a + b = b) # answer(Winker1b) # label(non_clause) # label(goal). [goal]. 4 (exists a exists b (a + b)' = a') # answer(Winker2a) # label(non_clause) # label(goal). [goal]. 5 (exists a exists b (a + b)' = b') # answer(Winker2b) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x + y = y + x # label(Commutativity). [assumption]. (x + y) + z = x + (y + z) # label(Associativity). [assumption]. ((x + y)' + (x + y')')' = x # label(Robbins). [assumption]. g(x) = (x + x')' # label(definition_g). [assumption]. h(x) = x + (x + (x + g(x))) # label(definition_h). [assumption]. (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [deny(1)]. x + y != x # answer(Winker1a). [deny(2)]. x + y != y # answer(Winker1b). [deny(3)]. (x + y)' != x' # answer(Winker2a). [deny(4)]. (x + y)' != y' # answer(Winker2b). [deny(5)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 5). % (Horn set with more than one neg. clause) Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, +, ', g, h ]). After inverse_order: (no changes). Folding symbols: g/1 h/1. After fold_eq: Function symbol precedence: function_order([ c1, c2, g, h, +, ' ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). % Operation + is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 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)]. 13 (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [deny(1)]. 14 x + y != x # answer(Winker1a). [deny(2)]. 15 x + y != y # answer(Winker1b). [deny(3)]. 16 (x + y)' != x' # answer(Winker2a). [deny(4)]. 17 (x + y)' != y' # answer(Winker2b). [deny(5)]. end_of_list. formulas(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=11): 12 x + (x + (x + g(x))) = h(x). [copy(11),flip(a)]. given #6 (I,wt=14): 13 (c1 + c2')' + (c1' + c2')' != c2 # answer(Huntington). [deny(1)]. given #7 (I,wt=5): 14 x + y != x # answer(Winker1a). [deny(2)]. given #8 (I,wt=5): 15 x + y != y # answer(Winker1b). [deny(3)]. given #9 (I,wt=7): 16 (x + y)' != x' # answer(Winker2a). [deny(4)]. given #10 (I,wt=7): 17 (x + y)' != y' # answer(Winker2b). [deny(5)]. given #11 (A,wt=11): 19 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),rewrite([7(2)])]. given #12 (F,wt=4): 37 h(x) != x # answer(Winker1a). [para(12(a,1),14(a,1))]. given #13 (F,wt=5): 43 x' != g(x) # answer(Winker2a). [para(10(a,1),16(a,1)),flip(a)]. given #14 (F,wt=6): 45 h(x)' != x' # answer(Winker2a). [para(12(a,1),16(a,1,1))]. given #15 (F,wt=6): 48 x'' != g(x) # answer(Winker2b). [para(10(a,1),17(a,1)),flip(a)]. given #16 (T,wt=10): 29 (g(x) + (x + x)')' = x. [para(10(a,1),8(a,1,1,2)),rewrite([6(4)])]. given #17 (T,wt=9): 74 (g(x) + h(x)')' = x. [back_rewrite(35),rewrite([66(8),6(4)])]. given #18 (T,wt=12): 27 (g(x) + (x + x'')')' = x. [para(10(a,1),8(a,1,1,1))]. given #19 (T,wt=12): 77 (x + (g(x) + h(x))')' = g(x). [para(74(a,1),8(a,1,1,2)),rewrite([6(5)])]. given #20 (A,wt=13): 20 ((x + y)' + (y + x')')' = y. [para(6(a,1),8(a,1,1,1,1))]. given #21 (F,wt=5): 68 g(x)' != x # answer(Winker2a). [para(29(a,1),16(a,1)),flip(a)]. given #22 (F,wt=6): 80 h(x)'' != x # answer(Winker2b). [para(74(a,1),17(a,1)),flip(a)]. given #23 (F,wt=7): 38 x + (y + z) != z # answer(Winker1b). [para(7(a,1),15(a,1))]. given #24 (F,wt=7): 41 (x + y)'' != x # answer(Winker2a). [para(8(a,1),16(a,1)),flip(a)]. given #25 (T,wt=13): 21 ((x + y)' + (y' + x)')' = x. [para(6(a,1),8(a,1,1,2,1))]. given #26 (T,wt=13): 66 (x + (x + (x + g(x)))')' = g(x). [para(29(a,1),8(a,1,1,2)),rewrite([19(3),6(2),6(5)])]. given #27 (T,wt=13): 111 ((x + y)' + (x' + y)')' = y. [para(6(a,1),20(a,1,1,2,1))]. given #28 (T,wt=13): 112 ((x + y')' + (y + x)')' = x. [para(6(a,1),20(a,1,1))]. given #29 (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 #30 (F,wt=7): 53 x + (y + z) != y # answer(Winker1a). [para(19(a,1),14(a,1))]. given #31 (F,wt=6): 283 x + h(y) != y # answer(Winker1a). [para(12(a,1),53(a,1,2))]. given #32 (F,wt=7): 124 (x + y)'' != y # answer(Winker2a). [para(20(a,1),16(a,1)),flip(a)]. given #33 (F,wt=6): 286 g(x)' != x' # answer(Winker2a). [para(10(a,1),124(a,1,1))]. given #34 (T,wt=13): 121 (g(x) + (x' + x')')' = x'. [para(10(a,1),20(a,1,1,1))]. given #35 (T,wt=13): 148 ((x' + y)' + (y + x)')' = y. [para(6(a,1),21(a,1,1))]. given #36 (T,wt=14): 26 (x + (y + (x + y)'))' = g(x + y). [para(7(a,1),10(a,1,1))]. given #37 (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 #38 (A,wt=20): 23 (x + ((x + y)' + (x + y')'')')' = (x + y)'. [para(8(a,1),8(a,1,1,1))]. given #39 (F,wt=7): 144 x + g(x) != h(x) # answer(Winker1b). [para(12(a,1),38(a,1)),flip(a)]. given #40 (F,wt=7): 369 g(x + y) != x' # answer(Winker2a). [para(26(a,1),16(a,1))]. given #41 (F,wt=6): 498 x' != g(h(x)) # answer(Winker2a). [para(12(a,1),369(a,1,1)),flip(a)]. given #42 (F,wt=7): 380 g(x + y)' != x # answer(Winker2a). [para(26(a,1),41(a,1,1))]. given #43 (T,wt=14): 75 (x + (g(x) + h(x)'')')' = g(x). [para(74(a,1),8(a,1,1,1))]. given #44 (T,wt=14): 103 (g(x) + (x + (g(x) + h(x)))')' = x. [para(77(a,1),8(a,1,1,2)),rewrite([6(7)])]. given #45 (T,wt=14): 363 (x + (y + (y + x)'))' = g(x + y). [para(6(a,1),26(a,1,1,2,2,1))]. given #46 (T,wt=15): 32 h(x) + y = x + (x + (x + (g(x) + y))). [para(12(a,1),7(a,1,1)),rewrite([7(6),7(5)])]. given #47 (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 #48 (F,wt=6): 534 g(h(x))' != x # answer(Winker2a). [para(12(a,1),380(a,1,1,1))]. given #49 (F,wt=7): 494 g(x + y) != y' # answer(Winker2a). [para(6(a,1),369(a,1,1))]. given #50 (F,wt=7): 532 g(x + y)' != y # answer(Winker2a). [para(6(a,1),380(a,1,1,1))]. given #51 (F,wt=8): 58 g(x + x') != g(x) # answer(Winker2a). [para(10(a,1),43(a,1)),flip(a)]. given #52 (T,wt=15): 34 x + h(y) = y + (y + (g(y) + (x + y))). [para(12(a,1),7(a,2,2)),rewrite([19(5),19(4),6(3)]),flip(a)]. given #53 (T,wt=15): 52 x + (y + (x + (x + g(x)))) = y + h(x). [para(12(a,1),19(a,1,2)),flip(a)]. given #54 (T,wt=15): 64 (x + (g(x) + (x + x)'')')' = g(x). [para(29(a,1),8(a,1,1,1))]. given #55 (T,wt=15): 88 (x + (x + (g(x) + x''))')' = g(x). [para(27(a,1),8(a,1,1,2)),rewrite([19(5),6(7)])]. given #56 (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 #57 (F,wt=8): 284 x + (y + h(z)) != z # answer(Winker1a). [para(7(a,1),283(a,1))]. given #58 (F,wt=8): 824 (x + h(y))' != y' # answer(Winker2a). [para(34(a,2),16(a,1,1))]. given #59 (F,wt=8): 838 (x + h(y))'' != y # answer(Winker2a). [para(34(a,2),41(a,1,1,1))]. given #60 (F,wt=8): 863 g(x + h(y)) != y' # answer(Winker2a). [para(34(a,2),369(a,1,1))]. given #61 (T,wt=15): 133 (x + (g(x)' + h(x)')')' = h(x)'. [para(74(a,1),20(a,1,1,1)),rewrite([6(5)])]. given #62 (T,wt=15): 157 (g(x') + (x + x'')')' = x''. [para(10(a,1),21(a,1,1,2)),rewrite([6(3),6(7)])]. given #63 (T,wt=15): 313 (g(g(x) + h(x)') + (x + x)')' = x. [para(74(a,1),121(a,1,1,2,1,1)),rewrite([74(10),74(14)])]. given #64 (T,wt=15): 620 x + h(y) = y + (y + (y + (g(y) + x))). [para(32(a,1),6(a,1)),flip(a)]. given #65 (A,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 #66 (F,wt=8): 865 g(x + h(y))' != y # answer(Winker2a). [para(34(a,2),380(a,1,1,1))]. given #67 (F,wt=9): 36 x + (y + z) != x + y # answer(Winker1a). [para(7(a,1),14(a,1))]. given #68 (F,wt=6): 1381 x + x != h(x) # answer(Winker1a). [para(12(a,1),36(a,1)),flip(a)]. given #69 (F,wt=8): 1380 x + h(y) != x + y # answer(Winker1a). [para(12(a,1),36(a,1,2))]. given #70 (T,wt=15): 830 x + (x + (y + (x + g(x)))) = y + h(x). [para(19(a,1),34(a,2,2,2)),rewrite([6(4)]),flip(a)]. given #71 (T,wt=15): 1270 x + h(y) = y + (y + (y + (x + g(y)))). [para(6(a,1),620(a,2,2,2,2))]. given #72 (T,wt=16): 101 (g(x) + (x + (g(x) + h(x))'')')' = x. [para(77(a,1),8(a,1,1,1))]. given #73 (T,wt=16): 122 ((x + (x' + y))' + (y + g(x))')' = y. [para(10(a,1),20(a,1,1,2,1,2)),rewrite([7(3)])]. given #74 (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 #75 (F,wt=8): 1389 x + h(y) != y + y # answer(Winker1a). [para(34(a,2),36(a,1))]. given #76 (F,wt=8): 1391 x + h(y) != y + x # answer(Winker1a). [para(52(a,1),36(a,1))]. given #77 (F,wt=9): 39 x + (x + g(x)) != h(x) # answer(Winker1b). [para(12(a,1),15(a,1)),flip(a)]. given #78 (F,wt=9): 46 (x + (y + z))' != z' # answer(Winker2b). [para(7(a,1),17(a,1,1))]. given #79 (T,wt=16): 156 ((x + (y + y'))' + (g(y) + x)')' = x. [para(10(a,1),21(a,1,1,2,1,1))]. given #80 (T,wt=16): 199 ((g(x) + y)' + (x + (x' + y))')' = y. [para(10(a,1),111(a,1,1,2,1,1)),rewrite([7(3),6(8)])]. given #81 (T,wt=16): 225 ((x + g(y))' + (y + (y' + x))')' = x. [para(10(a,1),112(a,1,1,1,1,2)),rewrite([7(6)])]. given #82 (T,wt=16): 303 (x' + (g(x) + (x' + x'))')' = g(x). [para(121(a,1),8(a,1,1,2)),rewrite([6(8)])]. given #83 (A,wt=21): 33 x + (y + (x + (y + (x + (y + g(x + y)))))) = h(x + y). [para(12(a,1),7(a,1)),rewrite([7(7),19(8),19(7),7(6)]),flip(a)]. given #84 (F,wt=6): 2175 h(x + y) != x # answer(Winker1a). [para(33(a,1),14(a,1))]. given #85 (F,wt=5): 2235 h(h(x)) != x # answer(Winker1a). [para(12(a,1),2175(a,1,1))]. given #86 (F,wt=6): 2194 h(x + y) != y # answer(Winker1a). [para(33(a,1),53(a,1))]. given #87 (F,wt=7): 2239 h(x + h(y)) != y # answer(Winker1a). [para(34(a,2),2175(a,1,1))]. given #88 (T,wt=16): 306 (g(x + x') + (g(x) + g(x))')' = g(x). [para(10(a,1),121(a,1,1,2,1,1)),rewrite([10(7),10(12)])]. given #89 (T,wt=16): 312 ((x + x)' + g(g(x) + (x + x)'))' = x. [para(29(a,1),121(a,1,1,2,1,1)),rewrite([29(10),6(8),29(14)])]. given #90 (T,wt=16): 335 ((g(x) + y)' + (y + (x + x'))')' = y. [para(10(a,1),148(a,1,1,1,1,1))]. given #91 (T,wt=16): 538 (g(x) + (x + (g(x) + h(x)''))')' = x. [para(75(a,1),8(a,1,1,2)),rewrite([6(9)])]. given #92 (A,wt=11): 40 (x + (y + z))' != (x + y)' # answer(Winker2a). [para(7(a,1),16(a,1,1))]. given #93 (F,wt=7): 2242 h(h(x + y)) != x # answer(Winker1a). [para(33(a,1),2175(a,1,1))]. given #94 (F,wt=6): 2549 h(h(h(x))) != x # answer(Winker1a). [para(12(a,1),2242(a,1,1,1))]. given #95 (F,wt=7): 2547 h(h(x + y)) != y # answer(Winker1a). [para(6(a,1),2242(a,1,1,1))]. given #96 (F,wt=8): 2177 h(x + y)' != x' # answer(Winker2a). [para(33(a,1),16(a,1,1))]. given #97 (T,wt=16): 1316 ((x + g(y))' + (y + (x + y'))')' = x. [para(19(a,1),28(a,1,1,2,1))]. given #98 (T,wt=16): 1828 ((x + (y + x'))' + (g(x) + y)')' = y. [para(19(a,1),156(a,1,1,1,1))]. given #99 (T,wt=16): 1835 (x + (x + (x' + h(x)'))')' = h(x)'. [para(74(a,1),156(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #100 (T,wt=16): 1924 ((g(x) + y)' + (x + (y + x'))')' = y. [para(6(a,1),199(a,1,1,2,1,2))]. given #101 (A,wt=15): 42 ((x + y)' + ((x + y')' + z))' != x # answer(Winker2a). [para(8(a,1),16(a,2)),rewrite([7(7)])]. given #102 (F,wt=7): 2572 h(h(x))' != x' # answer(Winker2a). [para(12(a,1),2177(a,1,1,1))]. given #103 (F,wt=8): 2188 h(x + y)'' != x # answer(Winker2a). [para(33(a,1),41(a,1,1,1))]. given #104 (F,wt=7): 3181 h(h(x))'' != x # answer(Winker2a). [para(12(a,1),2188(a,1,1,1,1))]. given #105 (F,wt=8): 2193 x + h(y + z) != y # answer(Winker1a). [para(33(a,1),53(a,1,2))]. given #106 (T,wt=17): 51 ((x + (y + z))' + (y + (x + z)')')' = y. [para(19(a,1),8(a,1,1,1,1))]. given #107 (T,wt=17): 76 ((x + y)' + (x + (g(y) + h(y)'))')' = x. [para(74(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. given #108 (T,wt=17): 78 (x + (g(x) + h(x)'))' = g(g(x) + h(x)'). [para(74(a,1),10(a,1,1,2)),rewrite([6(5)])]. given #109 (T,wt=17): 86 (x + (g(x) + (x + x'')'')')' = g(x). [para(27(a,1),8(a,1,1,1))]. given #110 (A,wt=10): 44 (x + (x' + y))' != g(x) # answer(Winker2a). [para(10(a,1),16(a,2)),rewrite([7(3)])]. given #111 (F,wt=7): 3192 x + h(h(y)) != y # answer(Winker1a). [para(12(a,1),2193(a,1,2,1))]. given #112 (F,wt=8): 2198 g(h(x + y)) != x' # answer(Winker2a). [para(33(a,1),369(a,1,1))]. given #113 (F,wt=7): 3651 x' != g(h(h(x))) # answer(Winker2a). [para(12(a,1),2198(a,1,1,1)),flip(a)]. given #114 (F,wt=8): 2199 g(h(x + y))' != x # answer(Winker2a). [para(33(a,1),380(a,1,1,1))]. given #115 (T,wt=17): 113 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),20(a,1,1,1,1))]. given #116 (T,wt=17): 131 (x + (g(x)' + (x + x)')')' = (x + x)'. [para(29(a,1),20(a,1,1,1)),rewrite([6(5)])]. given #117 (T,wt=17): 134 ((g(x) + (h(x)' + y))' + (y + x)')' = y. [para(74(a,1),20(a,1,1,2,1,2)),rewrite([7(5)])]. given #118 (T,wt=17): 161 ((x + (y + z))' + ((x + z)' + y)')' = y. [para(19(a,1),21(a,1,1,1,1))]. given #119 (A,wt=15): 47 (x + ((y + z)' + (y + z')'))' != y # answer(Winker2b). [para(8(a,1),17(a,2))]. given #120 (F,wt=7): 3753 g(h(h(x)))' != x # answer(Winker2a). [para(12(a,1),2199(a,1,1,1,1))]. given #121 (F,wt=8): 2236 h(x + (y + z)) != y # answer(Winker1a). [para(19(a,1),2175(a,1,1))]. given #122 (F,wt=8): 2243 h(x + (y + z)) != z # answer(Winker1a). [para(7(a,1),2194(a,1,1))]. given #123 (F,wt=8): 2524 (x + x)' != h(x)' # answer(Winker2a). [para(12(a,1),40(a,1,1)),flip(a)]. given #124 (T,wt=17): 167 ((x + (g(y) + h(y)'))' + (y + x)')' = x. [para(74(a,1),21(a,1,1,2,1,1))]. given #125 (T,wt=17): 179 (g(x) + (x + (x + (x + g(x)))'')')' = x. [para(66(a,1),8(a,1,1,1))]. given #126 (T,wt=17): 193 ((x + (y + z))' + ((x + y)' + z)')' = z. [para(7(a,1),111(a,1,1,1,1))]. given #127 (T,wt=17): 208 ((x + y)' + (g(x) + (h(x)' + y))')' = y. [para(74(a,1),111(a,1,1,2,1,1)),rewrite([7(5),6(9)])]. given #128 (A,wt=10): 49 (x + (y + y'))' != g(y) # answer(Winker2b). [para(10(a,1),17(a,2))]. given #129 (F,wt=8): 2553 h(h(x + h(y))) != y # answer(Winker1a). [para(34(a,2),2242(a,1,1,1))]. given #130 (F,wt=8): 2556 h(h(h(x + y))) != x # answer(Winker1a). [para(33(a,1),2242(a,1,1,1))]. given #131 (F,wt=7): 4797 h(h(h(h(x)))) != x # answer(Winker1a). [para(12(a,1),2556(a,1,1,1,1))]. given #132 (F,wt=8): 2568 h(x + y)' != y' # answer(Winker2a). [para(6(a,1),2177(a,1,1,1))]. given #133 (T,wt=17): 221 ((x + (y + z)')' + (y + (z + x))')' = x. [para(7(a,1),112(a,1,1,2,1))]. given #134 (T,wt=17): 233 ((x + y)' + (g(y) + (h(y)' + x))')' = x. [para(74(a,1),112(a,1,1,1,1,2)),rewrite([7(7)])]. given #135 (T,wt=17): 339 (((x + y)' + z)' + (x + (z + y))')' = z. [para(19(a,1),148(a,1,1,2,1))]. given #136 (T,wt=17): 344 ((x + y)' + (y + (g(x) + h(x)'))')' = y. [para(74(a,1),148(a,1,1,1,1,1))]. given #137 (A,wt=11): 50 (x + (x + g(x)))' != h(x)' # answer(Winker2b). [para(12(a,1),17(a,1,1)),flip(a)]. given #138 (F,wt=8): 3179 h(x + y)'' != y # answer(Winker2a). [para(6(a,1),2188(a,1,1,1,1))]. given #139 (F,wt=8): 3189 x + h(y + z) != z # answer(Winker1a). [para(6(a,1),2193(a,1,2,1))]. given #140 (F,wt=8): 3647 g(h(x + y)) != y' # answer(Winker2a). [para(6(a,1),2198(a,1,1,1))]. given #141 (F,wt=8): 3751 g(h(x + y))' != y # answer(Winker2a). [para(6(a,1),2199(a,1,1,1,1))]. given #142 (T,wt=17): 368 (x + (x + (x + (g(x) + h(x)'))))' = g(h(x)). [para(12(a,1),26(a,1,1,2,2,1)),rewrite([7(6),7(5),12(12)])]. given #143 (T,wt=17): 565 (x + (x + (g(x) + (g(x) + h(x))))')' = g(x). [para(103(a,1),8(a,1,1,2)),rewrite([19(6),6(8)])]. given #144 (T,wt=17): 856 g(x + h(y)) = g(y + (y + (g(y) + (x + y)))). [para(34(a,1),26(a,2,1)),rewrite([32(5),648(10)])]. given #145 (T,wt=17): 860 (x + h(y))' = (y + (y + (g(y) + (x + y))))'. [para(34(a,1),23(a,2,1)),rewrite([23(12)])]. given #146 (A,wt=9): 54 x + (y + z) != x + z # answer(Winker1b). [para(19(a,1),15(a,1))]. given #147 (F,wt=8): 4338 x + g(x) != h(h(x)) # answer(Winker1a). [para(12(a,1),2243(a,1,1)),flip(a)]. given #148 (F,wt=8): 4795 h(h(h(x + y))) != y # answer(Winker1a). [para(6(a,1),2556(a,1,1,1,1))]. given #149 (F,wt=8): 5356 (x + x)' != g(h(x)) # answer(Winker2a). [para(368(a,1),40(a,1)),flip(a)]. given #150 (F,wt=9): 55 (x + (y + z))' != y' # answer(Winker2a). [para(19(a,1),16(a,1,1))]. given #151 (T,wt=17): 905 (g(x) + (x + (g(x) + (x + x)''))')' = x. [para(64(a,1),8(a,1,1,2)),rewrite([6(9)])]. given #152 (T,wt=17): 938 (g(x) + (x + (x + (g(x) + x'')))')' = x. [para(88(a,1),8(a,1,1,2)),rewrite([6(9)])]. given #153 (T,wt=17): 1131 (h(x)' + (x + (g(x)' + h(x)'))')' = x. [para(133(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #154 (T,wt=17): 1180 (g(x) + (g(x) + (x' + h(x)'))')' = x'. [para(74(a,1),157(a,1,1,1,1)),rewrite([74(10),6(7),19(7),74(15)])]. given #155 (A,wt=11): 56 (x + (y + z))' != (x + z)' # answer(Winker2b). [para(19(a,1),17(a,1,1))]. given #156 (F,wt=9): 60 h(x + x')' != g(x) # answer(Winker2a). [para(10(a,1),45(a,2))]. given #157 (F,wt=9): 62 g(x)' != g(x + x') # answer(Winker2b). [para(10(a,1),48(a,1,1))]. given #158 (F,wt=9): 82 g(g(x) + h(x)') != x # answer(Winker2a). [para(74(a,1),43(a,1)),flip(a)]. given #159 (F,wt=9): 142 x + (y + (z + u)) != u # answer(Winker1b). [para(7(a,1),38(a,1,2))]. given #160 (T,wt=17): 1291 g(x + h(y)) = g(y + (y + (y + (g(y) + x)))). [para(620(a,1),26(a,2,1)),rewrite([32(5),648(10)])]. given #161 (T,wt=17): 1293 (x + h(y))' = (y + (y + (y + (g(y) + x))))'. [para(620(a,1),23(a,2,1)),rewrite([23(12)])]. given #162 (T,wt=17): 1473 g(x + h(y)) = g(y + (y + (y + (x + g(y))))). [para(1270(a,1),26(a,2,1)),rewrite([32(5),648(10)])]. given #163 (T,wt=17): 1477 (x + h(y))' = (y + (y + (y + (x + g(y)))))'. [para(1270(a,1),23(a,2,1)),rewrite([23(12)])]. given #164 (A,wt=13): 57 g((x + y)' + (x + y')') != x # answer(Winker2a). [para(8(a,1),43(a,1)),flip(a)]. given #165 (F,wt=5): 6484 h(x) != g(x) # answer(Winker1b). [para(12(a,1),142(a,1))]. given #166 (F,wt=9): 147 (x + (y + z))'' != y # answer(Winker2a). [para(19(a,1),41(a,1,1,1))]. given #167 (F,wt=9): 282 x + (y + (z + u)) != z # answer(Winker1a). [para(7(a,1),53(a,1))]. given #168 (F,wt=7): 7295 x + h(y) != g(y) # answer(Winker1a). [para(34(a,2),282(a,1))]. given #169 (T,wt=17): 2209 h(x + h(y)) = h(y + (y + (g(y) + (x + y)))). [para(34(a,1),33(a,2,1)),rewrite([32(7),32(12),32(17),2202(21)])]. given #170 (T,wt=17): 2215 h(x + h(y)) = h(y + (y + (y + (g(y) + x)))). [para(620(a,1),33(a,2,1)),rewrite([32(7),32(12),32(17),2202(21)])]. given #171 (T,wt=17): 2223 h(x + h(y)) = h(y + (y + (y + (x + g(y))))). [para(1270(a,1),33(a,2,1)),rewrite([32(7),32(12),32(17),2202(21)])]. given #172 (T,wt=17): 3201 ((x + (y + z))' + (x + (z + y)')')' = x. [para(6(a,1),51(a,1,1,1,1)),rewrite([7(2)])]. given #173 (A,wt=14): 59 h((x + y)' + (x + y')')' != x # answer(Winker2a). [para(8(a,1),45(a,2))]. given #174 (F,wt=9): 285 (x + (y + z))'' != z # answer(Winker2a). [para(7(a,1),124(a,1,1,1))]. given #175 (F,wt=9): 290 g(x + x')' != g(x) # answer(Winker2a). [para(10(a,1),286(a,2))]. given #176 (F,wt=9): 499 g(x + (y + z)) != y' # answer(Winker2a). [para(19(a,1),369(a,1,1))]. given #177 (F,wt=9): 516 g(h(x + x')) != g(x) # answer(Winker2a). [para(10(a,1),498(a,1)),flip(a)]. given #178 (T,wt=17): 3202 ((x + (y + z))' + (y + (z + x)')')' = y. [para(6(a,1),51(a,1,1,2,1,2,1))]. given #179 (T,wt=16): 8264 ((x' + (y + x))' + (y + g(x))')' = y. [para(10(a,1),3202(a,1,1,2,1,2))]. given #180 (T,wt=16): 8424 ((g(x) + y)' + (x' + (y + x))')' = y. [para(6(a,1),8264(a,1,1,2,1)),rewrite([6(8)])]. given #181 (T,wt=16): 8425 ((x + g(y))' + (y' + (x + y))')' = x. [para(6(a,1),8264(a,1,1))]. given #182 (A,wt=14): 61 g((x + y)' + (x + y')') != x' # answer(Winker2b). [para(8(a,1),48(a,1,1)),flip(a)]. given #183 (F,wt=9): 535 g(x + (y + z))' != y # answer(Winker2a). [para(19(a,1),380(a,1,1,1))]. given #184 (F,wt=9): 763 g(x + (y + z)) != z' # answer(Winker2a). [para(7(a,1),494(a,1,1))]. given #185 (F,wt=9): 788 g(x + (y + z))' != z # answer(Winker2a). [para(7(a,1),532(a,1,1,1))]. given #186 (F,wt=9): 1377 x + (y + z) != z + x # answer(Winker1a). [para(6(a,1),36(a,1)),rewrite([7(2)])]. given #187 (T,wt=17): 3203 ((x + (y + z)')' + (y + (x + z))')' = x. [para(6(a,1),51(a,1,1))]. given #188 (T,wt=17): 3212 ((x + y)' + (g(y) + (x + h(y)'))')' = x. [para(74(a,1),51(a,1,1,2,1,2)),rewrite([6(9)])]. given #189 (T,wt=17): 3328 (g(x) + (x + (g(x') + h(x')'))')' = x. [para(10(a,1),76(a,1,1,1))]. given #190 (T,wt=17): 3761 ((x + (y + z))' + (z + (y + x)')')' = z. [para(6(a,1),113(a,1,1,2,1,2,1))]. given #191 (A,wt=18): 63 (g(x + y) + (x + (y + (x + y)))')' = x + y. [para(7(a,1),29(a,1,1,2,1))]. given #192 (F,wt=9): 1378 x + (y + z) != y + x # answer(Winker1a). [para(6(a,1),36(a,2))]. given #193 (F,wt=8): 10014 h(x + y) != y + x # answer(Winker1a). [para(33(a,1),1378(a,1))]. given #194 (F,wt=9): 1772 (x + g(x))' != h(x)' # answer(Winker2b). [para(12(a,1),46(a,1,1)),flip(a)]. given #195 (F,wt=9): 1787 x'' != g(x + x') # answer(Winker2b). [para(31(a,1),46(a,1)),flip(a)]. given #196 (T,wt=17): 4029 ((x + (y + z))' + ((z + y)' + x)')' = x. [para(6(a,1),161(a,1,1,1,1)),rewrite([7(2)])]. given #197 (T,wt=17): 4030 ((x + (y + z))' + ((z + x)' + y)')' = y. [para(6(a,1),161(a,1,1,2,1,1,1))]. given #198 (T,wt=17): 4047 ((x + y)' + (g(x) + (y + h(x)'))')' = y. [para(74(a,1),161(a,1,1,2,1,1)),rewrite([6(9)])]. Low Water (keep, True_semantics): wt=81 Low Water (keep, False_semantics): wt=39 given #199 (T,wt=17): 4544 ((x + (y + z))' + ((y + x)' + z)')' = z. [para(6(a,1),193(a,1,1,2,1,1,1))]. Low Water (keep, True_semantics): wt=68 given #200 (A,wt=18): 65 ((x + y)' + (x + (g(y) + (y + y)'))')' = x. [para(29(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. Low Water (keep, False_semantics): wt=37 given #201 (F,wt=9): 2254 h(x + (y + h(z))) != z # answer(Winker1a). [para(7(a,1),2239(a,1,1))]. given #202 (F,wt=9): 2550 h(h(x + (y + z))) != y # answer(Winker1a). [para(19(a,1),2242(a,1,1,1))]. given #203 (F,wt=9): 2557 h(h(x + (y + z))) != z # answer(Winker1a). [para(7(a,1),2547(a,1,1,1))]. given #204 (F,wt=9): 2595 h(x + h(y))' != y' # answer(Winker2a). [para(34(a,2),2177(a,1,1,1))]. given #205 (T,wt=17): 4871 ((x + (y + z)')' + (z + (y + x))')' = x. [para(6(a,1),221(a,1,1,1,1,2,1))]. Low Water (keep, True_semantics): wt=66 Low Water (keep, False_semantics): wt=35 given #206 (T,wt=17): 4872 ((x + (y + z)')' + (z + (x + y))')' = x. [para(6(a,1),221(a,1,1,2,1)),rewrite([7(6)])]. Low Water (keep, False_semantics): wt=34 given #207 (T,wt=17): 5034 (((x + y)' + z)' + (y + (z + x))')' = z. [para(6(a,1),339(a,1,1,1,1,1,1))]. given #208 (T,wt=17): 5035 (((x + y)' + z)' + (z + (y + x))')' = z. [para(6(a,1),339(a,1,1,2,1)),rewrite([7(6)])]. given #209 (A,wt=19): 67 (x + (g(x) + (x + x)'))' = g(g(x) + (x + x)'). [para(29(a,1),10(a,1,1,2)),rewrite([6(5)])]. Low Water (keep, True_semantics): wt=64 Low Water (keep, True_semantics): wt=63 given #210 (F,wt=9): 2612 h(h(x + y))' != x' # answer(Winker2a). [para(33(a,1),2177(a,1,1,1))]. given #211 (F,wt=8): 11384 h(h(h(x)))' != x' # answer(Winker2a). [para(12(a,1),2612(a,1,1,1,1))]. given #212 (F,wt=9): 3185 h(x + h(y))'' != y # answer(Winker2a). [para(34(a,2),2188(a,1,1,1,1))]. given #213 (F,wt=9): 3188 h(h(x + y))'' != x # answer(Winker2a). [para(33(a,1),2188(a,1,1,1,1))]. given #214 (T,wt=17): 8273 ((x + y)' + (h(y)' + (x + g(y)))')' = x. [para(74(a,1),3202(a,1,1,2,1,2)),rewrite([6(9)])]. Low Water (keep, False_semantics): wt=33 given #215 (T,wt=17): 10222 ((x + y)' + (h(x)' + (y + g(x)))')' = y. [para(74(a,1),4030(a,1,1,2,1,1)),rewrite([6(9)])]. given #216 (T,wt=18): 117 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(20(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. Low Water (keep, False_semantics): wt=32 Low Water (keep, True_semantics): wt=61 given #217 (T,wt=18): 132 ((g(x) + ((x + x)' + y))' + (y + x)')' = y. [para(29(a,1),20(a,1,1,2,1,2)),rewrite([7(5)])]. Low Water (keep, False_semantics): wt=31 Low Water (keep, True_semantics): wt=57 given #218 (A,wt=12): 69 (g(x) + ((x + x)' + y))' != x # answer(Winker2a). [para(29(a,1),16(a,2)),rewrite([7(5)])]. given #219 (F,wt=8): 11582 h(h(h(x)))'' != x # answer(Winker2a). [para(12(a,1),3188(a,1,1,1,1,1))]. given #220 (F,wt=9): 3197 x + h(y + h(z)) != z # answer(Winker1a). [para(34(a,2),2193(a,1,2,1))]. given #221 (F,wt=9): 3200 x + h(h(y + z)) != y # answer(Winker1a). [para(33(a,1),2193(a,1,2,1))]. given #222 (F,wt=8): 12233 x + h(h(h(y))) != y # answer(Winker1a). [para(12(a,1),3200(a,1,2,1,1))]. given #223 (T,wt=18): 152 (x + (y' + (x + (x + y)'))')' = (x + y)'. [para(21(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. Low Water (keep, True_semantics): wt=54 given #224 (T,wt=18): 166 ((x + (g(y) + (y + y)'))' + (y + x)')' = x. [para(29(a,1),21(a,1,1,2,1,1))]. Low Water (keep, False_semantics): wt=30 given #225 (T,wt=18): 196 (x + (y' + (x + (y + x)'))')' = (y + x)'. [para(111(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #226 (T,wt=18): 207 ((x + y)' + (g(x) + ((x + x)' + y))')' = y. [para(29(a,1),111(a,1,1,2,1,1)),rewrite([7(5),6(9)])]. Low Water (keep, True_semantics): wt=53 Low Water (keep, True_semantics): wt=51 given #227 (A,wt=12): 70 (x + (g(y) + (y + y)'))' != y # answer(Winker2b). [para(29(a,1),17(a,2))]. given #228 (F,wt=9): 3592 (x + h(x'))' != g(x) # answer(Winker2a). [para(12(a,1),44(a,1,1,2))]. given #229 (F,wt=9): 3645 x + (y + h(h(z))) != z # answer(Winker1a). [para(7(a,1),3192(a,1))]. given #230 (F,wt=9): 3674 g(h(x + h(y))) != y' # answer(Winker2a). [para(34(a,2),2198(a,1,1,1))]. Low Water (keep, False_semantics): wt=29 given #231 (F,wt=9): 3691 g(h(h(x + y))) != x' # answer(Winker2a). [para(33(a,1),2198(a,1,1,1))]. given #232 (T,wt=18): 232 ((x + y)' + (g(y) + ((y + y)' + x))')' = x. [para(29(a,1),112(a,1,1,1,1,2)),rewrite([7(7)])]. Low Water (keep, False_semantics): wt=28 given #233 (T,wt=18): 301 (x' + (g(x) + (x' + x')'')')' = g(x). [para(121(a,1),8(a,1,1,1))]. Low Water (keep, True_semantics): wt=50 Low Water (keep, True_semantics): wt=49 given #234 (T,wt=18): 315 ((x + x)' + g(g(x) + (x + x'')'))' = x. [para(27(a,1),121(a,1,1,2,1,1)),rewrite([27(14),6(10),27(18)])]. Low Water (keep, False_semantics): wt=27 Low Water (keep, True_semantics): wt=48 given #235 (T,wt=18): 343 ((x + y)' + (y + (g(x) + (x + x)'))')' = y. [para(29(a,1),148(a,1,1,1,1,1))]. given #236 (A,wt=10): 71 g(g(x) + (x + x)') != x # answer(Winker2a). [para(29(a,1),43(a,1)),flip(a)]. given #237 (F,wt=8): 13060 x' != g(h(h(h(x)))) # answer(Winker2a). [para(12(a,1),3691(a,1,1,1,1)),flip(a)]. given #238 (F,wt=9): 3757 g(h(x + h(y)))' != y # answer(Winker2a). [para(34(a,2),2199(a,1,1,1,1))]. given #239 (F,wt=9): 3760 g(h(h(x + y)))' != x # answer(Winker2a). [para(33(a,1),2199(a,1,1,1,1))]. given #240 (F,wt=8): 13693 g(h(h(h(x))))' != x # answer(Winker2a). [para(12(a,1),3760(a,1,1,1,1,1))]. given #241 (T,wt=18): 365 (g(x + y) + (x + (y + (x + y)')')')' = x. [para(26(a,1),8(a,1,1,1))]. Low Water (keep, True_semantics): wt=47 given #242 (T,wt=18): 390 (g(x + x') + (x + (g(x) + x')')')' = x. [para(31(a,1),8(a,1,1,1))]. Low Water (keep, True_semantics): wt=46 Low Water (keep, True_semantics): wt=45 given #243 (T,wt=18): 443 (g(x) + (x + (g(x) + h(x)'')'')')' = x. [para(74(a,1),23(a,1,1,2,1,1)),rewrite([74(17)])]. Low Water (keep, False_semantics): wt=26 given #244 (T,wt=18): 589 (g(x + y) + (x + (y + (y + x)')')')' = x. [para(363(a,1),8(a,1,1,1))]. given #245 (A,wt=11): 72 h(g(x) + (x + x)')' != x # answer(Winker2a). [para(29(a,1),45(a,2))]. given #246 (F,wt=9): 4335 h(x + h(y + z)) != y # answer(Winker1a). [para(33(a,1),2236(a,1,1,2))]. given #247 (F,wt=8): 14176 h(x + h(h(y))) != y # answer(Winker1a). [para(12(a,1),4335(a,1,1,2,1))]. given #248 (F,wt=9): 4801 h(h(h(x + h(y)))) != y # answer(Winker1a). [para(34(a,2),2556(a,1,1,1,1))]. given #249 (F,wt=9): 4804 h(h(h(h(x + y)))) != x # answer(Winker1a). [para(33(a,1),2556(a,1,1,1,1))]. given #250 (T,wt=18): 608 (g(x + y) + (x + (y + (y + x)))')' = x + y. [para(363(a,1),22(a,1,1,2)),rewrite([6(7)])]. Low Water (keep, True_semantics): wt=44 given #251 (T,wt=18): 831 (x + (x + (x + (x + (g(x) + g(x)))))')' = g(x). [para(34(a,1),77(a,1,1,2,1)),rewrite([6(3),19(4)])]. given #252 (T,wt=18): 1173 (g(g(x)) + (x + (x' + g(x)'))')' = g(x)'. [para(10(a,1),157(a,1,1,1,1)),rewrite([10(7),7(7),10(13)])]. given #253 (T,wt=18): 1179 (g(x) + (g(x) + (x' + (x + x)'))')' = x'. [para(29(a,1),157(a,1,1,1,1)),rewrite([29(10),6(7),19(7),29(15)])]. given #254 (A,wt=11): 73 g(g(x) + (x + x)') != x' # answer(Winker2b). [para(29(a,1),48(a,1,1)),flip(a)]. given #255 (F,wt=8): 14203 h(h(h(h(h(x))))) != x # answer(Winker1a). [para(12(a,1),4804(a,1,1,1,1,1))]. given #256 (F,wt=9): 5720 x + (y + z) != z + y # answer(Winker1b). [para(6(a,1),54(a,1)),rewrite([7(2)])]. given #257 (F,wt=9): 6483 x + h(y) != y + g(y) # answer(Winker1b). [para(12(a,1),142(a,1,2))]. given #258 (F,wt=9): 6496 g(x) + y != y + h(x) # answer(Winker1b). [para(620(a,2),142(a,1)),flip(a)]. given #259 (T,wt=18): 2815 (h(x)' + (x + (x + (x' + h(x)')))')' = x. [para(1835(a,1),8(a,1,1,2)),rewrite([6(10)])]. Low Water (keep, True_semantics): wt=43 given #260 (T,wt=18): 3211 ((x + y)' + (g(y) + (x + (y + y)'))')' = x. [para(29(a,1),51(a,1,1,2,1,2)),rewrite([6(9)])]. given #261 (T,wt=18): 3234 (g(x + y) + (y + (x + (x + y)')')')' = y. [para(26(a,1),51(a,1,1,1))]. Low Water (keep, False_semantics): wt=25 given #262 (T,wt=18): 3247 (g(x + y) + (y + (x + (y + x)')')')' = y. [para(363(a,1),51(a,1,1,1))]. given #263 (A,wt=11): 79 (g(x) + (h(x)' + y))' != x # answer(Winker2a). [para(74(a,1),16(a,2)),rewrite([7(5)])]. given #264 (F,wt=9): 6502 x + h(y) != x + g(y) # answer(Winker1b). [para(1270(a,2),142(a,1))]. given #265 (F,wt=9): 7297 x + (y + h(z)) != g(z) # answer(Winker1a). [para(7(a,1),7295(a,1))]. given #266 (F,wt=9): 8008 h(x)'' != x + g(x) # answer(Winker2a). [para(12(a,1),285(a,1,1,1))]. given #267 (F,wt=9): 9236 (x + g(x))' != g(h(x)) # answer(Winker2a). [para(12(a,1),763(a,1,1)),flip(a)]. given #268 (T,wt=18): 3769 (h(x)' + g(g(x) + (x + x)'))' = x + g(x). [para(12(a,1),113(a,1,1,1,1)),rewrite([7(7),67(8)])]. given #269 (T,wt=18): 4046 ((x + y)' + (g(x) + (y + (x + x)'))')' = y. [para(29(a,1),161(a,1,1,2,1,1)),rewrite([6(9)])]. given #270 (T,wt=18): 7729 (g(x + y) + (y + (x + (x + y)))')' = x + y. [para(10(a,1),3201(a,1,1,2)),rewrite([19(3),6(2),6(7)])]. given #271 (T,wt=18): 8272 ((x + y)' + ((y + y)' + (x + g(y)))')' = x. [para(29(a,1),3202(a,1,1,2,1,2)),rewrite([6(9)])]. given #272 (A,wt=11): 81 (x + (g(y) + h(y)'))' != y # answer(Winker2b). [para(74(a,1),17(a,2))]. given #273 (F,wt=9): 9328 g(h(x))' != x + g(x) # answer(Winker2a). [para(12(a,1),788(a,1,1,1))]. given #274 (F,wt=9): 10820 x + g(x) != h(h(h(x))) # answer(Winker1a). [para(12(a,1),2557(a,1,1,1)),flip(a)]. given #275 (F,wt=9): 11380 h(h(x + y))' != y' # answer(Winker2a). [para(6(a,1),2612(a,1,1,1,1))]. given #276 (F,wt=9): 11580 h(h(x + y))'' != y # answer(Winker2a). [para(6(a,1),3188(a,1,1,1,1,1))]. given #277 (T,wt=18): 9892 (g(x + y) + (y + (x + (y + x)))')' = y + x. [para(6(a,1),63(a,1,1,1,1))]. Low Water (keep, True_semantics): wt=42 Low Water (keep, False_semantics): wt=24 given #278 (T,wt=18): 9900 (g(x + y) + (x + (x + (y + y)))')' = x + y. [para(19(a,1),63(a,1,1,2,1,2))]. given #279 (T,wt=18): 10221 ((x + y)' + ((x + x)' + (y + g(x)))')' = y. [para(29(a,1),4030(a,1,1,2,1,1)),rewrite([6(9)])]. given #280 (T,wt=18): 15429 (g(x + y) + (y + (y + (x + x)))')' = y + x. [para(19(a,1),9892(a,1,1,2,1,2))]. given #281 (A,wt=10): 83 h(g(x) + h(x)')' != x # answer(Winker2a). [para(74(a,1),45(a,2))]. given #282 (F,wt=9): 12230 x + h(h(y + z)) != z # answer(Winker1a). [para(6(a,1),3200(a,1,2,1,1))]. given #283 (F,wt=9): 13056 g(h(h(x + y))) != y' # answer(Winker2a). [para(6(a,1),3691(a,1,1,1,1))]. given #284 (F,wt=9): 13691 g(h(h(x + y)))' != y # answer(Winker2a). [para(6(a,1),3760(a,1,1,1,1,1))]. Low Water (keep, False_semantics): wt=23 given #285 (F,wt=9): 14173 h(x + h(y + z)) != z # answer(Winker1a). [para(6(a,1),4335(a,1,1,2,1))]. given #286 (T,wt=19): 114 ((x + (y + z))' + (y + (z + x'))')' = y + z. [para(7(a,1),20(a,1,1,2,1))]. given #287 (T,wt=19): 127 ((x + (y + z))' + (x + (z + y'))')' = x + z. [para(19(a,1),20(a,1,1,1,1)),rewrite([7(6)])]. given #288 (T,wt=19): 149 ((x + (y + z))' + (z' + (x + y))')' = x + y. [para(7(a,1),21(a,1,1,1,1))]. given #289 (T,wt=19): 154 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. Low Water (keep, False_semantics): wt=22 Low Water (keep, True_semantics): wt=41 given #290 (A,wt=10): 84 g(g(x) + h(x)') != x' # answer(Winker2b). [para(74(a,1),48(a,1,1)),flip(a)]. given #291 (F,wt=9): 14201 h(h(h(h(x + y)))) != y # answer(Winker1a). [para(6(a,1),4804(a,1,1,1,1,1))]. given #292 (F,wt=9): 15424 g(x + y)' != y + x # answer(Winker2a). [para(9892(a,1),16(a,1)),flip(a)]. given #293 (F,wt=9): 15435 (x + y)' != g(y + x) # answer(Winker2a). [para(9892(a,1),41(a,1,1))]. given #294 (F,wt=10): 292 g(g(x) + h(x)')' != x # answer(Winker2a). [para(74(a,1),286(a,2))]. given #295 (T,wt=15): 16756 (g(x + y) + h(y + x)')' = y + x. [para(9892(a,1),154(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),2172(10),9892(15)])]. given #296 (T,wt=19): 162 ((x + (y + z))' + (x + (z' + y))')' = x + y. [para(19(a,1),21(a,1,1,2,1)),rewrite([7(2)])]. Low Water (keep, True_semantics): wt=40 given #297 (T,wt=19): 175 (x + (y + (x + (x + y')'))')' = (x + y')'. [para(20(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #298 (T,wt=19): 177 (x + (x + (y + (y' + x)'))')' = (y' + x)'. [para(21(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. Low Water (keep, True_semantics): wt=39 given #299 (A,wt=20): 85 (g(x + y) + (x + (y + (x + y)''))')' = x + y. [para(7(a,1),27(a,1,1,2,1))]. given #300 (F,wt=10): 497 g(x + (x' + y)) != g(x) # answer(Winker2a). [para(10(a,1),369(a,2)),rewrite([7(3)])]. given #301 (F,wt=9): 17532 g(x + h(x')) != g(x) # answer(Winker2a). [para(12(a,1),497(a,1,1,2))]. given #302 (F,wt=10): 518 g(h(g(x) + h(x)')) != x # answer(Winker2a). [para(74(a,1),498(a,1)),flip(a)]. given #303 (F,wt=10): 765 g(x + (y + y')) != g(y) # answer(Winker2a). [para(10(a,1),494(a,2))]. given #304 (T,wt=19): 202 ((x + (y + z))' + (y' + (x + z))')' = x + z. [para(19(a,1),111(a,1,1,1,1))]. given #305 (T,wt=19): 203 ((x + (y + z))' + (y + (x' + z))')' = y + z. [para(19(a,1),111(a,1,1,2,1))]. Low Water (keep, False_semantics): wt=21 Low Water (keep, True_semantics): wt=38 given #306 (T,wt=19): 216 (x + (y + (x + (y' + x)'))')' = (y' + x)'. [para(111(a,1),21(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. given #307 (T,wt=19): 220 ((x + (y + z'))' + (z + (x + y))')' = x + y. [para(7(a,1),112(a,1,1,1,1))]. Low Water (keep, True_semantics): wt=37 given #308 (A,wt=20): 87 ((x + y)' + (x + (g(y) + (y + y'')'))')' = x. [para(27(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #309 (F,wt=10): 1071 x + (y + (z + h(u))) != u # answer(Winker1a). [para(7(a,1),284(a,1,2))]. given #310 (F,wt=10): 1074 (x + (y + h(z)))' != z' # answer(Winker2a). [para(7(a,1),824(a,1,1))]. given #311 (F,wt=10): 1100 (x + (y + h(z)))'' != z # answer(Winker2a). [para(7(a,1),838(a,1,1,1))]. given #312 (F,wt=10): 1102 g(x + (y + h(z))) != z' # answer(Winker2a). [para(7(a,1),863(a,1,1))]. given #313 (T,wt=19): 228 ((x + (y + z'))' + (x + (z + y))')' = x + y. [para(19(a,1),112(a,1,1,2,1)),rewrite([7(3)])]. given #314 (T,wt=19): 245 ((x + (y + z))' + (z + (x + y'))')' = z + x. [para(6(a,1),22(a,1,1,1,1)),rewrite([7(2)])]. Low Water (keep, True_semantics): wt=36 given #315 (T,wt=19): 246 ((x + (y + z))' + (y + (z' + x))')' = x + y. [para(6(a,1),22(a,1,1,2,1)),rewrite([7(6)])]. Low Water (keep, True_semantics): wt=35 given #316 (T,wt=19): 255 (h(x)' + (x + (x + (x + g(x))'))')' = x + x. [para(12(a,1),22(a,1,1,1,1))]. Low Water (keep, True_semantics): wt=34 given #317 (A,wt=38): 89 (g((x + y)' + (x + y')') + (x' + ((x + y)' + (x + y')'))')' = (x + y)' + (x + y')'. [para(8(a,1),27(a,1,1,2,1,2,1)),rewrite([6(15)])]. given #318 (F,wt=8): 18997 h(x)'' != x + x # answer(Winker2a). [para(255(a,1),16(a,1)),flip(a)]. given #319 (F,wt=10): 1375 g(x + (y + h(z)))' != z # answer(Winker2a). [para(7(a,1),865(a,1,1,1))]. given #320 (F,wt=10): 1388 x + (y + h(z)) != x + z # answer(Winker1a). [para(34(a,2),36(a,1,2))]. given #321 (F,wt=10): 1750 x + (y + h(z)) != z + z # answer(Winker1a). [para(7(a,1),1389(a,1))]. given #322 (T,wt=19): 260 ((x + (y + z))' + (y + (x + z'))')' = y + x. [para(19(a,1),22(a,1,1,1,1))]. given #323 (T,wt=19): 304 (g((x + y)' + (x + y')') + (x + x)')' = x. [para(8(a,1),121(a,1,1,2,1,1)),rewrite([8(14),8(18)])]. given #324 (T,wt=19): 319 (g((x + y)' + (y + x')') + (y + y)')' = y. [para(20(a,1),121(a,1,1,2,1,1)),rewrite([20(14),20(18)])]. Low Water (keep, True_semantics): wt=33 given #325 (T,wt=19): 321 (g((x + y)' + (y' + x)') + (x + x)')' = x. [para(21(a,1),121(a,1,1,2,1,1)),rewrite([21(14),21(18)])]. given #326 (A,wt=23): 90 (x + (g(x) + (x + x'')'))' = g(g(x) + (x + x'')'). [para(27(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #327 (F,wt=10): 1792 (x + y)'' != g(y + x) # answer(Winker2b). [para(363(a,1),46(a,1)),flip(a)]. given #328 (F,wt=10): 2218 x + h(y + z) != x + y # answer(Winker1a). [para(33(a,1),36(a,1,2))]. given #329 (F,wt=9): 19819 x + h(h(y)) != x + y # answer(Winker1a). [para(12(a,1),2218(a,1,2,1))]. given #330 (F,wt=9): 19834 x + h(h(y)) != y + x # answer(Winker1a). [para(6(a,1),19819(a,2))]. given #331 (T,wt=19): 324 (g((x + y)' + (x' + y)') + (y + y)')' = y. [para(111(a,1),121(a,1,1,2,1,1)),rewrite([111(14),111(18)])]. given #332 (T,wt=19): 326 (g((x + y')' + (y + x)') + (x + x)')' = x. [para(112(a,1),121(a,1,1,2,1,1)),rewrite([112(14),112(18)])]. given #333 (T,wt=19): 331 ((x' + (y + z))' + (y + (z + x))')' = y + z. [para(7(a,1),148(a,1,1,2,1))]. Low Water (keep, False_semantics): wt=20 Low Water (keep, True_semantics): wt=32 given #334 (T,wt=19): 338 ((x + (y' + z))' + (x + (z + y))')' = x + z. [para(19(a,1),148(a,1,1,1,1)),rewrite([7(6)])]. given #335 (A,wt=21): 91 (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 #336 (F,wt=10): 2234 h(x + (y + z)) != x + y # answer(Winker1a). [para(7(a,1),2175(a,1,1))]. Low Water (displace, False_semantics): id=10368, wt=39 Low Water (displace, False_semantics): id=10774, wt=36 Low Water (displace, False_semantics): id=10663, wt=35 given #337 (F,wt=7): 20354 x + x != h(h(x)) # answer(Winker1a). [para(12(a,1),2234(a,1,1)),flip(a)]. given #338 (F,wt=9): 20353 h(x + h(y)) != x + y # answer(Winker1a). [para(12(a,1),2234(a,1,1,2))]. Low Water (displace, False_semantics): id=11008, wt=34 given #339 (F,wt=9): 20360 h(x + h(y)) != y + y # answer(Winker1a). [para(34(a,2),2234(a,1,1))]. given #340 (T,wt=19): 360 (g((x' + y)' + (y + x)') + (y + y)')' = y. [para(148(a,1),121(a,1,1,2,1,1)),rewrite([148(14),148(18)])]. Low Water (displace, True_semantics): id=10340, wt=81 Low Water (displace, True_semantics): id=10445, wt=68 Low Water (displace, True_semantics): id=10566, wt=67 Low Water (displace, True_semantics): id=10538, wt=66 Low Water (displace, True_semantics): id=10701, wt=58 Low Water (displace, True_semantics): id=11377, wt=57 Low Water (displace, True_semantics): id=11347, wt=55 Low Water (displace, True_semantics): id=12083, wt=54 Low Water (displace, True_semantics): id=12454, wt=53 Low Water (displace, True_semantics): id=12513, wt=52 Low Water (displace, True_semantics): id=12686, wt=51 Low Water (displace, True_semantics): id=11715, wt=50 Low Water (displace, True_semantics): id=12688, wt=49 Low Water (displace, True_semantics): id=13402, wt=48 given #341 (T,wt=19): 418 (g(x + x') + (x + (x + g(x)))')' = x + g(x). [para(31(a,1),22(a,1,1,2)),rewrite([6(2),6(8)])]. Low Water (displace, False_semantics): id=11252, wt=33 given #342 (T,wt=19): 441 (g(x) + (x + (g(x) + (x + x)'')'')')' = x. [para(29(a,1),23(a,1,1,2,1,1)),rewrite([29(17)])]. Low Water (displace, True_semantics): id=13520, wt=47 given #343 (T,wt=19): 563 (x + (g(x) + (x + (g(x) + h(x)))'')')' = g(x). [para(103(a,1),8(a,1,1,1))]. given #344 (A,wt=14): 92 (g(x) + ((x + x'')' + y))' != x # answer(Winker2a). [para(27(a,1),16(a,2)),rewrite([7(7)])]. given #345 (F,wt=9): 20362 h(x + h(y)) != y + x # answer(Winker1a). [para(52(a,1),2234(a,1,1))]. Low Water (displace, False_semantics): id=11355, wt=32 Low Water (displace, False_semantics): id=11368, wt=31 given #346 (F,wt=10): 2244 x + (x + g(x)) != h(h(x)) # answer(Winker1a). [para(12(a,1),2194(a,1,1)),flip(a)]. given #347 (F,wt=10): 2245 h(x + (y + z)) != x + z # answer(Winker1a). [para(19(a,1),2194(a,1,1))]. Low Water (displace, False_semantics): id=12180, wt=30 Low Water (displace, False_semantics): id=12569, wt=29 given #348 (F,wt=10): 2523 (x + h(y))' != (x + y)' # answer(Winker2a). [para(12(a,1),40(a,1,1,2))]. Low Water (displace, False_semantics): id=12946, wt=28 Low Water (displace, False_semantics): id=13388, wt=27 Low Water (displace, False_semantics): id=13949, wt=26 given #349 (T,wt=19): 813 x + (y + h(z)) = z + (z + (g(z) + (x + (y + z)))). [para(34(a,1),7(a,1)),rewrite([7(3)]),flip(a)]. Low Water (displace, True_semantics): id=13777, wt=46 Low Water (displace, False_semantics): id=14728, wt=25 Low Water (displace, True_semantics): id=13883, wt=45 given #350 (T,wt=19): 814 x + (y + h(z)) = x + (z + (z + (g(z) + (y + z)))). [para(34(a,1),7(a,2,2)),rewrite([7(3)])]. Low Water (displace, False_semantics): id=15298, wt=24 Low Water (displace, True_semantics): id=14157, wt=44 Low Water (displace, True_semantics): id=14470, wt=43 given #351 (T,wt=19): 816 x + (g(x) + (y + (x + (z + x)))) = y + (z + h(x)). [para(34(a,2),7(a,2,2)),rewrite([19(6),19(5),7(4)])]. Low Water (displace, False_semantics): id=15839, wt=23 given #352 (T,wt=19): 827 x + (y + h(z)) = y + (z + (z + (g(z) + (x + z)))). [para(34(a,1),19(a,1,2)),flip(a)]. Low Water (displace, False_semantics): id=16481, wt=22 given #353 (A,wt=14): 93 (x + (g(y) + (y + y'')'))' != y # answer(Winker2b). [para(27(a,1),17(a,2))]. given #354 (F,wt=10): 2533 (x + h(y))' != (y + y)' # answer(Winker2a). [para(34(a,2),40(a,1,1))]. given #355 (F,wt=10): 2535 (x + h(y))' != (y + x)' # answer(Winker2a). [para(52(a,1),40(a,1,1))]. given #356 (F,wt=10): 2573 h(x + (y + z))' != y' # answer(Winker2a). [para(19(a,1),2177(a,1,1,1))]. given #357 (F,wt=10): 3137 h(h(x + x'))' != g(x) # answer(Winker2a). [para(10(a,1),2572(a,2))]. given #358 (T,wt=19): 828 x + (y + h(z)) = z + (x + (z + (g(z) + (y + z)))). [para(34(a,2),19(a,1,2))]. given #359 (T,wt=19): 883 x + (y + (z + (x + (x + g(x))))) = y + (z + h(x)). [para(7(a,1),52(a,1,2)),rewrite([7(9)])]. given #360 (T,wt=19): 937 (g(x) + (x + (x + (g(x) + x''))'')')' = x. [para(88(a,1),8(a,1,1,1))]. Low Water (displace, True_semantics): id=15272, wt=42 given #361 (T,wt=19): 1006 (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 #362 (A,wt=12): 94 g(g(x) + (x + x'')') != x # answer(Winker2a). [para(27(a,1),43(a,1)),flip(a)]. given #363 (F,wt=10): 3182 h(x + (y + z))'' != y # answer(Winker2a). [para(19(a,1),2188(a,1,1,1,1))]. given #364 (F,wt=10): 3191 x + (y + h(z + u)) != z # answer(Winker1a). [para(7(a,1),2193(a,1))]. given #365 (F,wt=10): 3193 x + h(y + (z + u)) != z # answer(Winker1a). [para(19(a,1),2193(a,1,2,1))]. given #366 (F,wt=10): 3591 (x + (y + x'))' != g(x) # answer(Winker2a). [para(6(a,1),44(a,1,1,2))]. given #367 (T,wt=19): 1008 (x + (x + (g(x) + (g(x) + h(x))''))')' = g(x). [para(77(a,1),25(a,1,1,2,1,2,2)),rewrite([6(7),77(17)])]. Low Water (keep, True_semantics): wt=31 given #368 (T,wt=19): 1129 (h(x)' + (x + (g(x)' + h(x)')'')')' = x. [para(133(a,1),8(a,1,1,1))]. given #369 (T,wt=19): 1170 (x'' + (x + (g(x') + x''))')' = g(x'). [para(157(a,1),8(a,1,1,2)),rewrite([19(6),6(10)])]. given #370 (T,wt=19): 1271 x + (y + h(z)) = z + (z + (z + (g(z) + (x + y)))). [para(620(a,1),7(a,1)),flip(a)]. given #371 (A,wt=13): 95 h(g(x) + (x + x'')')' != x # answer(Winker2a). [para(27(a,1),45(a,2))]. given #372 (F,wt=10): 3652 g(h(x + (y + z))) != y' # answer(Winker2a). [para(19(a,1),2198(a,1,1,1))]. given #373 (F,wt=10): 3705 g(h(h(x + x'))) != g(x) # answer(Winker2a). [para(10(a,1),3651(a,1)),flip(a)]. given #374 (F,wt=10): 3754 g(h(x + (y + z)))' != y # answer(Winker2a). [para(19(a,1),2199(a,1,1,1,1))]. given #375 (F,wt=10): 4329 h(x + (y + (z + u))) != z # answer(Winker1a). [para(7(a,1),2236(a,1,1))]. given #376 (T,wt=19): 1272 x + (y + h(z)) = x + (z + (z + (z + (g(z) + y)))). [para(620(a,1),7(a,2,2)),rewrite([7(3)])]. Low Water (displace, True_semantics): id=15713, wt=41 given #377 (T,wt=19): 1274 x + (y + h(z)) = z + (z + (g(z) + (x + (z + y)))). [para(620(a,2),7(a,2,2)),rewrite([19(6),19(5),19(4),7(3)]),flip(a)]. given #378 (T,wt=19): 1278 x + (y + h(z)) = y + (z + (z + (z + (g(z) + x)))). [para(620(a,1),19(a,1,2)),flip(a)]. given #379 (T,wt=19): 1279 x + (y + h(z)) = z + (x + (z + (z + (g(z) + y)))). [para(620(a,2),19(a,1,2))]. Low Water (displace, False_semantics): id=17665, wt=21 given #380 (A,wt=13): 96 g(g(x) + (x + x'')') != x' # answer(Winker2b). [para(27(a,1),48(a,1,1)),flip(a)]. given #381 (F,wt=8): 21875 h(x + h(y)) != g(y) # answer(Winker1a). [para(34(a,2),4329(a,1,1))]. given #382 (F,wt=10): 4336 h(x + (y + (z + u))) != u # answer(Winker1a). [para(7(a,1),2243(a,1,1,2))]. given #383 (F,wt=6): 22297 h(h(x)) != g(x) # answer(Winker1a). [para(12(a,1),4336(a,1,1))]. given #384 (F,wt=10): 4793 h(h(x + (y + h(z)))) != z # answer(Winker1a). [para(7(a,1),2553(a,1,1,1))]. given #385 (T,wt=19): 1280 x + (y + h(z)) = z + (z + (z + (x + (g(z) + y)))). [para(19(a,1),620(a,2,2,2,2)),rewrite([7(3)])]. Low Water (keep, False_semantics): wt=19 given #386 (T,wt=19): 1409 x + (y + (x + (z + (x + g(x))))) = y + (z + h(x)). [para(830(a,1),7(a,2,2)),rewrite([19(6),7(5)])]. given #387 (T,wt=19): 1410 x + (x + (y + (z + (x + g(x))))) = y + (z + h(x)). [para(7(a,1),830(a,1,2,2)),rewrite([7(9)])]. given #388 (T,wt=19): 1435 x + (y + h(z)) = z + (z + (z + (x + (y + g(z))))). [para(1270(a,1),7(a,1)),rewrite([7(3)]),flip(a)]. Low Water (displace, True_semantics): id=16840, wt=40 given #389 (A,wt=29): 97 (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 #390 (F,wt=10): 4798 h(h(h(x + (y + z)))) != y # answer(Winker1a). [para(19(a,1),2556(a,1,1,1,1))]. given #391 (F,wt=10): 4805 h(x + (y + z))' != z' # answer(Winker2a). [para(7(a,1),2568(a,1,1,1))]. given #392 (F,wt=10): 5210 h(x + (y + z))'' != z # answer(Winker2a). [para(7(a,1),3179(a,1,1,1,1))]. given #393 (F,wt=10): 5221 x + h(y + (z + u)) != u # answer(Winker1a). [para(7(a,1),3189(a,1,2,1))]. given #394 (T,wt=19): 1436 x + (y + h(z)) = x + (z + (z + (z + (y + g(z))))). [para(1270(a,1),7(a,2,2)),rewrite([7(3)])]. given #395 (T,wt=19): 1438 x + (y + h(z)) = z + (z + (x + (z + (y + g(z))))). [para(1270(a,2),7(a,2,2)),rewrite([19(6),19(5),7(4)]),flip(a)]. given #396 (T,wt=19): 1447 x + (y + h(z)) = y + (z + (z + (z + (x + g(z))))). [para(1270(a,1),19(a,1,2)),flip(a)]. given #397 (T,wt=19): 1448 x + (y + h(z)) = z + (x + (z + (z + (y + g(z))))). [para(1270(a,2),19(a,1,2))]. given #398 (A,wt=26): 98 (g(g(x) + h(x)') + (g(x) + (x' + h(x)'))')' = g(x) + h(x)'. [para(74(a,1),27(a,1,1,2,1,2,1)),rewrite([6(11),19(11)])]. given #399 (F,wt=10): 5222 x + (y + h(z + u)) != u # answer(Winker1a). [para(7(a,1),3189(a,1))]. given #400 (F,wt=10): 5234 g(h(x + (y + z))) != z' # answer(Winker2a). [para(7(a,1),3647(a,1,1,1))]. given #401 (F,wt=10): 5304 g(h(x + (y + z)))' != z # answer(Winker2a). [para(7(a,1),3751(a,1,1,1,1))]. given #402 (F,wt=10): 5744 h(h(h(x + (y + z)))) != z # answer(Winker1a). [para(7(a,1),4795(a,1,1,1,1))]. given #403 (T,wt=19): 1666 ((x + x)' + g((x + y)' + (x + y')'))' = x. [para(30(a,1),148(a,1,1,2)),rewrite([8(7)])]. Low Water (displace, True_semantics): id=17218, wt=39 given #404 (T,wt=19): 2096 (g(x) + (g(x) + (x' + (x' + x')))')' = x'. [para(303(a,1),8(a,1,1,2)),rewrite([19(7),6(10)])]. given #405 (T,wt=19): 2473 (x + (x + (g(x) + (g(x) + h(x)'')))')' = g(x). [para(538(a,1),8(a,1,1,2)),rewrite([19(8),6(10)])]. given #406 (T,wt=19): 3789 (g(x + x') + (x' + (x + g(x))')')' = x'. [para(31(a,1),113(a,1,1,1))]. given #407 (A,wt=35): 99 (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 #408 (F,wt=10): 5798 (x + h(y + z))' != y' # answer(Winker2a). [para(33(a,1),55(a,1,1,2))]. given #409 (F,wt=9): 23373 (x + h(h(y)))' != y' # answer(Winker2a). [para(12(a,1),5798(a,1,1,2,1))]. given #410 (F,wt=10): 7289 (x + h(y + z))'' != y # answer(Winker2a). [para(33(a,1),147(a,1,1,1,2))]. given #411 (F,wt=9): 23417 (x + h(h(y)))'' != y # answer(Winker2a). [para(12(a,1),7289(a,1,1,1,2,1))]. given #412 (T,wt=19): 3866 ((x + x)' + (x + (g(x)' + (x + x)'))')' = x. [para(131(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #413 (T,wt=19): 10617 (g(x) + (x + (g(x') + (x' + x')'))')' = x. [para(10(a,1),65(a,1,1,1))]. given #414 (T,wt=19): 15894 ((x + (y + z))' + (z + (y + x'))')' = z + y. [para(6(a,1),114(a,1,1,1,1,2))]. Low Water (displace, True_semantics): id=17651, wt=38 given #415 (T,wt=19): 15895 ((x + (y + z))' + (z + (x' + y))')' = y + z. [para(6(a,1),114(a,1,1,2,1)),rewrite([7(6)])]. given #416 (A,wt=20): 100 (x + (y + (g(x + y) + h(x + y))'))' = g(x + y). [para(7(a,1),77(a,1,1))]. Low Water (displace, True_semantics): id=18079, wt=37 given #417 (F,wt=10): 8010 g(x + y)' != (y + x)' # answer(Winker2a). [para(363(a,1),285(a,1,1))]. given #418 (F,wt=10): 8143 g(x + h(y + z)) != y' # answer(Winker2a). [para(33(a,1),499(a,1,1,2))]. given #419 (F,wt=9): 23638 g(x + h(h(y))) != y' # answer(Winker2a). [para(12(a,1),8143(a,1,1,2,1))]. Low Water (displace, False_semantics): id=20144, wt=20 given #420 (F,wt=10): 9231 g(x + h(y + z))' != y # answer(Winker2a). [para(33(a,1),535(a,1,1,1,2))]. given #421 (T,wt=19): 16090 ((x + (y + z))' + (x + (y' + z))')' = x + z. [para(6(a,1),127(a,1,1,2,1,2))]. Low Water (displace, True_semantics): id=18331, wt=36 given #422 (T,wt=19): 16091 ((x + (y + z))' + (z + (y' + x))')' = x + z. [para(6(a,1),127(a,1,1,2,1)),rewrite([7(6)])]. given #423 (T,wt=19): 16295 ((x + (y + z))' + (y' + (z + x))')' = z + x. [para(6(a,1),149(a,1,1,1,1)),rewrite([7(2)])]. Low Water (displace, True_semantics): id=18630, wt=35 given #424 (T,wt=19): 16296 ((x + (y + z))' + (z' + (y + x))')' = x + y. [para(6(a,1),149(a,1,1,2,1,2))]. given #425 (A,wt=20): 102 ((x + g(y))' + (x + (y + (g(y) + h(y))'))')' = x. [para(77(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. Low Water (displace, True_semantics): id=18987, wt=34 given #426 (F,wt=9): 23682 g(x + h(h(y)))' != y # answer(Winker2a). [para(12(a,1),9231(a,1,1,1,2,1))]. given #427 (F,wt=10): 10010 x + (y + h(z)) != z + x # answer(Winker1a). [para(34(a,2),1378(a,1,2))]. given #428 (F,wt=10): 10013 x + h(y + z) != y + x # answer(Winker1a). [para(33(a,1),1378(a,1,2))]. given #429 (F,wt=10): 10817 h(h(x + h(y + z))) != y # answer(Winker1a). [para(33(a,1),2550(a,1,1,1,2))]. given #430 (T,wt=19): 17543 ((x + (y + z))' + (x' + (z + y))')' = z + y. [para(6(a,1),202(a,1,1,1,1)),rewrite([7(2)])]. given #431 (T,wt=19): 17544 ((x' + (y + z))' + (y + (x + z))')' = y + z. [para(6(a,1),202(a,1,1))]. Low Water (keep, True_semantics): wt=30 given #432 (T,wt=19): 17752 ((x + (y' + z))' + (y + (x + z))')' = x + z. [para(6(a,1),203(a,1,1))]. given #433 (T,wt=19): 18124 ((x + (y' + z))' + (y + (z + x))')' = z + x. [para(6(a,1),220(a,1,1,1,1)),rewrite([7(3)])]. given #434 (A,wt=22): 104 (x + (g(x) + (g(x) + h(x))'))' = g(x + (g(x) + h(x))'). [para(77(a,1),10(a,1,1,2)),rewrite([6(7),19(7)])]. given #435 (F,wt=9): 24044 h(h(x + h(h(y)))) != y # answer(Winker1a). [para(12(a,1),10817(a,1,1,1,2,1))]. given #436 (F,wt=10): 11407 h(h(x + h(y)))' != y' # answer(Winker2a). [para(34(a,2),2612(a,1,1,1,1))]. given #437 (F,wt=10): 11424 h(h(h(x + y)))' != x' # answer(Winker2a). [para(33(a,1),2612(a,1,1,1,1))]. given #438 (F,wt=9): 24290 h(h(h(h(x))))' != x' # answer(Winker2a). [para(12(a,1),11424(a,1,1,1,1,1))]. given #439 (T,wt=19): 18125 ((x + (y + z'))' + (z + (y + x))')' = x + y. [para(6(a,1),220(a,1,1,2,1,2))]. given #440 (T,wt=19): 18414 ((x + (y' + z))' + (z + (y + x))')' = z + x. [para(6(a,1),228(a,1,1,1,1)),rewrite([7(3)])]. given #441 (T,wt=19): 18420 ((x + (y + z'))' + (y + (z + x))')' = y + x. [para(19(a,1),228(a,1,1,1,1))]. Low Water (displace, True_semantics): id=19499, wt=33 given #442 (T,wt=19): 18784 ((x + (y' + z))' + (z + (x + y))')' = z + x. [para(6(a,1),246(a,1,1))]. given #443 (A,wt=14): 105 (x + ((g(x) + h(x))' + y))' != g(x) # answer(Winker2a). [para(77(a,1),16(a,2)),rewrite([7(6)])]. given #444 (F,wt=10): 11586 h(h(x + h(y)))'' != y # answer(Winker2a). [para(34(a,2),3188(a,1,1,1,1,1))]. given #445 (F,wt=10): 11589 h(h(h(x + y)))'' != x # answer(Winker2a). [para(33(a,1),3188(a,1,1,1,1,1))]. given #446 (F,wt=9): 24491 h(h(h(h(x))))'' != x # answer(Winker2a). [para(12(a,1),11589(a,1,1,1,1,1,1))]. given #447 (F,wt=10): 12238 x + h(h(y + h(z))) != z # answer(Winker1a). [para(34(a,2),3200(a,1,2,1,1))]. given #448 (T,wt=19): 19059 ((x + (y + z'))' + (y + (x + z))')' = x + y. [para(6(a,1),260(a,1,1))]. given #449 (T,wt=19): 19500 ((x + x)' + g((y + x)' + (x + y')'))' = x. [para(6(a,1),319(a,1,1))]. given #450 (T,wt=19): 19645 ((x + x)' + g((x + y)' + (y' + x)'))' = x. [para(6(a,1),321(a,1,1))]. given #451 (T,wt=19): 19850 ((x + x)' + g((y + x)' + (y' + x)'))' = x. [para(6(a,1),324(a,1,1))]. given #452 (A,wt=14): 106 (x + (y + (g(y) + h(y))'))' != g(y) # answer(Winker2b). [para(77(a,1),17(a,2))]. given #453 (F,wt=10): 12241 x + h(h(h(y + z))) != y # answer(Winker1a). [para(33(a,1),3200(a,1,2,1,1))]. given #454 (F,wt=9): 24641 x + h(h(h(h(y)))) != y # answer(Winker1a). [para(12(a,1),12241(a,1,2,1,1,1))]. Demod_limit: v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(v101) + (g(h(v101)) + (g(h(v101)) + (g(h(v101)) + (g(h(v101)) + (g(h(v101)) + (g(h(v101)) + (g(h(h(v101))) + (g(h(h(v101))) + (h(h(v101)) + (h(h(v101)) + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (v101 + (g(v101) + (v101 + (g(v101) + (g(v101) + (g(h(v101)) + (g(h(h(v101))) + (g(h(h(h(v101)))) + v100)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) != v101 # answer(Winker1a). [para(6(a,1),24641(a,1)),rewrite([32(5),32(15),32(22),32(26),19(30),19(29),19(28),19(27),32(26),19(30),19(29),19(28),19(34),19(33),19(32),19(31),19(30),19(29),19(28),19(27),32(26),19(30),19(29),19(28),19(31),19(30),19(29),19(38),19(37),19(36),19(35),19(34),19(33),19(32),19(31),19(30),19(29),19(28),19(27),19(26),32(25),32(29),19(33),19(32),19(31),19(30),32(29),19(33),19(32),19(31),19(37),19(36),19(35),19(34),19(33),19(32),19(31),19(30),32(29),19(33),19(32),19(31),19(34),19(33),19(32),19(41),19(40),19(39),19(38),19(37),19(36),19(35),19(34),19(33),19(32),19(31),19(30),19(42),19(41),19(40),19(39),19(38),19(37),19(36),19(35),19(34),19(43),19(42),19(41),19(40),19(39),19(38),19(37),19(36),19(35),19(44),19(43),19(42),19(41),19(40),19(39),19(38),19(37),19(36),19(54),19(53),19(52),19(51),19(50),19(49),19(48),19(47),19(46),19(45),19(44),19(43),19(42),19(41),19(40),19(39),19(38),19(37),19(36),19(35),19(34),19(33),19(32),19(31),19(30),19(29),32(28),32(32),19(36),19(35),19(34),19(33),32(32),19(36),19(35),19(34),19(40),19(39),19(38),19(37),19(36),19(35),19(34),19(33),32(32),19(36),19(35),19(34),19(37),19(36),19(35),19(44),19(43),19(42),19(41),19(40),19(39),19(38),19(37),19(36),19(35),19(34),19(33),19(45),19(44),19(43),19(42),19(41),19(40),19(39),19(38),19(37),19(36),19(35),19(34),19(46),19(45),19(44),19(43),19(42),19(41),19(40),19(39),19(38),19(47),19(46),19(45),19(44),19(43),19(42),19(41),19(40),19(39),19(48),19(47),19(46),19(45),19(44),19(43),19(42),19(41),19(40),19(49),19(48),19(47),19(46),19(45),19(44),19(43),19(42),19(41),19(50),19(49),19(48),19(47),19(46),19(45),19(44),19(43),19(42),19(51),19(50),19(49),19(48),19(47),19(46),19(45),19(44),19(43),19(70),19(69),19(68),19(67),19(66),19(65),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(52),19(51),19(50),19(49),19(48),19(47),19(46),19(45),19(44),19(43),19(42),19(41),19(40),19(39),19(38),19(37),19(36),19(35),19(34),19(33),19(32),19(31),32(30),32(37),32(41),19(45),19(44),19(43),19(42),32(41),19(45),19(44),19(43),19(49),19(48),19(47),19(46),19(45),19(44),19(43),19(42),32(41),19(45),19(44),19(43),19(46),19(45),19(44),19(53),19(52),19(51),19(50),19(49),19(48),19(47),19(46),19(45),19(44),19(43),19(42),19(41),32(40),32(44),19(48),19(47),19(46),19(45),32(44),19(48),19(47),19(46),19(52),19(51),19(50),19(49),19(48),19(47),19(46),19(45),32(44),19(48),19(47),19(46),19(49),19(48),19(47),19(56),19(55),19(54),19(53),19(52),19(51),19(50),19(49),19(48),19(47),19(46),19(45),19(57),19(56),19(55),19(54),19(53),19(52),19(51),19(50),19(49),19(58),19(57),19(56),19(55),19(54),19(53),19(52),19(51),19(50),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(52),19(51),19(69),19(68),19(67),19(66),19(65),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(52),19(51),19(50),19(49),19(48),19(47),19(46),19(45),19(44),32(43),32(47),19(51),19(50),19(49),19(48),32(47),19(51),19(50),19(49),19(55),19(54),19(53),19(52),19(51),19(50),19(49),19(48),32(47),19(51),19(50),19(49),19(52),19(51),19(50),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(52),19(51),19(50),19(49),19(48),19(60),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(52),19(51),19(50),19(49),19(61),19(60),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(62),19(61),19(60),19(59),19(58),19(57),19(56),19(55),19(54),19(63),19(62),19(61),19(60),19(59),19(58),19(57),19(56),19(55),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(57),19(56),19(65),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(57),19(66),19(65),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(67),19(66),19(65),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(52),19(51),19(50),19(49),19(48),19(47),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(67),19(66),19(65),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(52),19(51),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(67),19(66),19(65),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(52),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(67),19(66),19(65),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(89),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(67),19(66),19(65),19(64),19(63),19(90),19(89),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(67),19(66),19(65),19(64),19(91),19(90),19(89),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(67),19(66),19(65),19(92),19(91),19(90),19(89),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(67),19(66),19(93),19(92),19(91),19(90),19(89),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(67),19(94),19(93),19(92),19(91),19(90),19(89),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(95),19(94),19(93),19(92),19(91),19(90),19(89),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(96),19(95),19(94),19(93),19(92),19(91),19(90),19(89),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(97),19(96),19(95),19(94),19(93),19(92),19(91),19(90),19(89),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(125),19(124),19(123),19(122),19(121),19(120),19(119),19(118),19(117),19(116),19(115),19(114),19(113),19(112),19(111),19(110),19(109),19(108),19(107),19(106),19(105),19(104),19(103),19(102),19(101),19(100),19(99),19(98),19(97),19(96),19(95),19(94),19(93),19(92),19(91),19(90),19(89),19(88),19(87),19(86),19(85),19(84),19(83),19(82),19(81),19(80),19(79),19(78),19(77),19(76),19(75),19(74),19(73),19(72),19(71),19(70),19(69),19(68),19(67),19(66),19(65),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(57),19(56),19(55),19(54),19(53),19(52),19(51),19(50),19(49),19(48),19(47),19(46),32(45),32(52),32(56),19(60),19(59),19(58),19(57),32(56),19(60),19(59),19(58),19(64),19(63),19(62),19(61),19(60),19(59),19(58),19(57),32(56),19(60),19(59),19(58),19(61),19(60)])]. Demod_limit (steps=0, size=249). The most recent kept clause is 24650. From here on, a short message will be printed for each 100 times the limit is hit. given #455 (F,wt=10): 12242 x + (y + h(h(h(z)))) != z # answer(Winker1a). [para(7(a,1),12233(a,1))]. given #456 (F,wt=10): 13083 g(h(h(x + h(y)))) != y' # answer(Winker2a). [para(34(a,2),3691(a,1,1,1,1))]. given #457 (T,wt=19): 19998 ((x + x)' + g((x + y')' + (y + x)'))' = x. [para(6(a,1),326(a,1,1))]. given #458 (T,wt=19): 20145 ((x' + (y + z))' + (z + (y + x))')' = z + y. [para(6(a,1),331(a,1,1,1,1,2))]. given #459 (T,wt=19): 20146 ((x' + (y + z))' + (z + (x + y))')' = y + z. [para(6(a,1),331(a,1,1,2,1)),rewrite([7(6)])]. given #460 (T,wt=19): 20389 ((x + x)' + g((y' + x)' + (x + y)'))' = x. [para(6(a,1),360(a,1,1))]. given #461 (A,wt=13): 108 h(x + (g(x) + h(x))')' != g(x) # answer(Winker2a). [para(77(a,1),45(a,2))]. given #462 (F,wt=10): 13099 g(h(h(h(x + y)))) != x' # answer(Winker2a). [para(33(a,1),3691(a,1,1,1,1))]. given #463 (F,wt=9): 24805 x' != g(h(h(h(h(x))))) # answer(Winker2a). [para(12(a,1),13099(a,1,1,1,1,1)),flip(a)]. given #464 (F,wt=10): 13697 g(h(h(x + h(y))))' != y # answer(Winker2a). [para(34(a,2),3760(a,1,1,1,1,1))]. given #465 (F,wt=10): 13700 g(h(h(h(x + y))))' != x # answer(Winker2a). [para(33(a,1),3760(a,1,1,1,1,1))]. given #466 (T,wt=19): 20701 x + (y + h(z)) = z + (z + (g(z) + (y + (z + x)))). [para(6(a,1),813(a,2,2,2,2)),rewrite([7(6)])]. given #467 (T,wt=19): 20714 x + (y + h(z)) = z + (z + (g(z) + (y + (x + z)))). [para(813(a,1),19(a,1)),flip(a)]. given #468 (T,wt=19): 20717 x + (y + h(z)) = z + (z + (x + (g(z) + (y + z)))). [para(19(a,1),813(a,2,2,2))]. Low Water (displace, True_semantics): id=20143, wt=32 given #469 (T,wt=19): 20953 x + (g(x) + (y + (x + (x + z)))) = y + (z + h(x)). [para(6(a,1),816(a,1,2,2,2,2))]. Low Water (keep, False_semantics): wt=18 given #470 (A,wt=20): 115 (x + ((y + x)' + (x + y')'')')' = (y + x)'. [para(20(a,1),8(a,1,1,1))]. given #471 (F,wt=9): 24846 g(h(h(h(h(x)))))' != x # answer(Winker2a). [para(12(a,1),13700(a,1,1,1,1,1,1))]. given #472 (F,wt=10): 14181 h(x + h(y + h(z))) != z # answer(Winker1a). [para(34(a,2),4335(a,1,1,2,1))]. given #473 (F,wt=10): 14184 h(x + h(h(y + z))) != y # answer(Winker1a). [para(33(a,1),4335(a,1,1,2,1))]. given #474 (F,wt=9): 25331 h(x + h(h(h(y)))) != y # answer(Winker1a). [para(12(a,1),14184(a,1,1,2,1,1))]. given #475 (T,wt=19): 20966 x + (g(x) + (y + (x + (z + x)))) = z + (y + h(x)). [para(816(a,2),19(a,1))]. given #476 (T,wt=19): 20968 x + (g(x) + (y + (z + (x + x)))) = y + (z + h(x)). [para(19(a,1),816(a,1,2,2,2))]. Low Water (keep, True_semantics): wt=29 given #477 (T,wt=19): 21147 x + (y + h(z)) = z + (y + (z + (g(z) + (x + z)))). [para(827(a,2),19(a,1))]. given #478 (T,wt=19): 21472 x + (y + h(z)) = z + (y + (z + (z + (g(z) + x)))). [para(6(a,1),883(a,1,2)),rewrite([7(5),7(4),7(3)]),flip(a)]. given #479 (A,wt=21): 116 ((x + y)' + (x + ((z + y)' + (y + z')'))')' = x. [para(20(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #480 (F,wt=10): 14185 h(x + (y + h(h(z)))) != z # answer(Winker1a). [para(7(a,1),14176(a,1,1))]. given #481 (F,wt=10): 14207 h(h(h(h(x + h(y))))) != y # answer(Winker1a). [para(34(a,2),4804(a,1,1,1,1,1))]. given #482 (F,wt=10): 14210 h(h(h(h(h(x + y))))) != x # answer(Winker1a). [para(33(a,1),4804(a,1,1,1,1,1))]. given #483 (F,wt=9): 25509 h(h(h(h(h(h(x)))))) != x # answer(Winker1a). [para(12(a,1),14210(a,1,1,1,1,1,1))]. given #484 (T,wt=19): 21717 x + (y + h(z)) = z + (z + (z + (g(z) + (y + x)))). [para(6(a,1),1271(a,2,2,2,2,2))]. given #485 (T,wt=19): 21949 x + (y + h(z)) = z + (z + (x + (z + (g(z) + y)))). [para(19(a,1),1274(a,2,2,2)),rewrite([19(6)])]. given #486 (T,wt=19): 22347 x + (y + h(z)) = z + (z + (z + (y + (g(z) + x)))). [para(1280(a,1),19(a,1)),flip(a)]. given #487 (T,wt=19): 22469 x + (y + h(z)) = z + (z + (y + (z + (g(z) + x)))). [para(6(a,1),1409(a,1,2)),rewrite([7(5),7(4),7(3)]),flip(a)]. given #488 (A,wt=21): 118 (x + ((x + y')' + (x + y)'')')' = (x + y')'. [para(8(a,1),20(a,1,1,1))]. given #489 (F,wt=10): 14923 (g(x) + h(h(x)'))' != x # answer(Winker2a). [para(12(a,1),79(a,1,1,2))]. given #490 (F,wt=10): 17531 g(x + (y + x')) != g(x) # answer(Winker2a). [para(6(a,1),497(a,1,1,2))]. given #491 (F,wt=10): 19043 x + (y + h(z)) != y + z # answer(Winker1a). [para(19(a,1),1388(a,1))]. given #492 (F,wt=10): 19816 x + h(y + z) != x + z # answer(Winker1a). [para(6(a,1),2218(a,1,2,1))]. given #493 (T,wt=19): 22520 x + (y + h(z)) = z + (z + (z + (y + (x + g(z))))). [para(1435(a,1),19(a,1)),flip(a)]. given #494 (T,wt=19): 22817 x + (y + h(z)) = z + (z + (y + (z + (x + g(z))))). [para(1438(a,1),19(a,1)),flip(a)]. given #495 (T,wt=19): 22954 x + (y + h(z)) = z + (y + (z + (z + (x + g(z))))). [para(1447(a,2),19(a,1))]. Low Water (displace, False_semantics): id=22269, wt=19 given #496 (T,wt=19): 24054 ((x' + (y + z))' + (x + (z + y))')' = y + z. [para(6(a,1),17543(a,1,1))]. given #497 (A,wt=21): 119 (((x + y)' + ((x + y')' + z))' + (z + x)')' = z. [para(8(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #498 (F,wt=10): 20350 h(x + (y + z)) != z + x # answer(Winker1a). [para(6(a,1),2234(a,1,1)),rewrite([7(2)])]. given #499 (F,wt=10): 20351 h(x + (y + z)) != y + x # answer(Winker1a). [para(6(a,1),2234(a,2))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 719 (0.00 of 66.89 sec). given #500 (F,wt=9): 25921 h(h(x + y)) != y + x # answer(Winker1a). [para(33(a,1),20351(a,1,1))]. given #501 (F,wt=10): 20563 h(x + (y + z)) != z + y # answer(Winker1a). [para(6(a,1),2245(a,1,1)),rewrite([7(2)])]. given #502 (T,wt=19): 24946 x + (y + h(z)) = z + (z + (y + (g(z) + (x + z)))). [para(19(a,1),20714(a,2,2,2))]. given #503 (T,wt=19): 25172 x + (g(x) + (y + (x + (x + z)))) = z + (y + h(x)). [para(20953(a,2),19(a,1))]. given #504 (T,wt=19): 25423 x + (y + (g(x) + (z + (x + x)))) = y + (z + h(x)). [para(19(a,1),20968(a,1,2))]. given #505 (T,wt=15): 26022 x + (g(x) + (y + (x + x))) = y + h(x). [para(25423(a,1),127(a,1,1,1,1)),rewrite([7(10),7(9),7(8),25262(14)]),flip(a)]. given #506 (A,wt=25): 120 (x + ((y + x)' + (x + y')'))' = g((y + x)' + (x + y')'). [para(20(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #507 (F,wt=9): 26062 (x + h(y))' != g(y)' # answer(Winker2a). [para(26022(a,1),55(a,1,1))]. given #508 (F,wt=9): 26064 (x + h(y))'' != g(y) # answer(Winker2a). [para(26022(a,1),147(a,1,1,1))]. given #509 (F,wt=9): 26066 g(x + h(y)) != g(y)' # answer(Winker2a). [para(26022(a,1),499(a,1,1))]. given #510 (F,wt=9): 26068 g(x + h(y))' != g(y) # answer(Winker2a). [para(26022(a,1),535(a,1,1,1))]. given #511 (T,wt=19): 26033 g(x) + (y + (x + (z + (x + x)))) = y + (z + h(x)). [para(26022(a,1),7(a,2,2)),rewrite([19(6),7(5)])]. given #512 (T,wt=19): 26117 g(x) + (y + (x + (x + (x + z)))) = y + (z + h(x)). [para(6(a,1),26033(a,1,2,2,2)),rewrite([7(3)])]. given #513 (T,wt=19): 26121 g(x) + (y + (x + (x + (z + x)))) = y + (z + h(x)). [para(19(a,1),26033(a,1,2,2,2))]. given #514 (T,wt=19): 26122 g(x) + (y + (z + (x + (x + x)))) = y + (z + h(x)). [para(19(a,1),26033(a,1,2,2))]. given #515 (A,wt=22): 123 (h(x)' + (x + (x + (g(x) + x')))')' = x + (x + g(x)). [para(12(a,1),20(a,1,1,1,1)),rewrite([7(7),7(6)])]. given #516 (F,wt=9): 26073 h(h(x + h(y))) != g(y) # answer(Winker1a). [para(26022(a,1),2550(a,1,1,1))]. given #517 (F,wt=10): 21023 h(x + (y + h(z))) != g(z) # answer(Winker1a). [para(816(a,1),2236(a,1,1))]. given #518 (F,wt=10): 21233 x + (y + h(z)) != z + y # answer(Winker1a). [para(827(a,2),1378(a,1))]. given #519 (F,wt=10): 22296 h(x + h(y)) != y + g(y) # answer(Winker1a). [para(12(a,1),4336(a,1,1,2))]. given #520 (T,wt=15): 26410 g(x) + (y + (x + (x + x))) = y + h(x). [para(26122(a,1),127(a,1,1,1,1)),rewrite([7(10),7(9),7(8),26260(14)]),flip(a)]. Low Water (displace, True_semantics): id=21495, wt=31 given #521 (T,wt=19): 26203 g(x) + (y + (x + (x + (x + z)))) = z + (y + h(x)). [para(26117(a,2),19(a,1))]. given #522 (T,wt=19): 26306 g(x) + (y + (x + (x + (z + x)))) = z + (y + h(x)). [para(26121(a,2),19(a,1))]. given #523 (T,wt=19): 26473 (g(h(x)) + (x + (x + (x + x)))')' = x + (x + x). [para(26410(a,1),134(a,1,1,1,1)),rewrite([6(4),32(4),368(8),6(5)])]. given #524 (A,wt=15): 125 ((x + y)' + ((y + x')' + z))' != y # answer(Winker2a). [para(20(a,1),16(a,2)),rewrite([7(7)])]. given #525 (F,wt=5): 26497 g(h(x)) != x # answer(Winker2a). [para(26410(a,1),79(a,1,1)),rewrite([6(4),32(4),368(8)])]. given #526 (F,wt=10): 22306 h(x + h(y)) != g(y) + x # answer(Winker1a). [para(620(a,2),4336(a,1,1))]. given #527 (F,wt=10): 22312 h(x + h(y)) != x + g(y) # answer(Winker1a). [para(1270(a,2),4336(a,1,1))]. given #528 (F,wt=10): 22668 (x + g(x))' != h(h(x))' # answer(Winker2a). [para(12(a,1),4805(a,1,1,1)),flip(a)]. given #529 (T,wt=20): 137 ((g(x) + ((x + x'')' + y))' + (y + x)')' = y. [para(27(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #530 (T,wt=20): 139 ((x + ((g(x) + h(x))' + y))' + (y + g(x))')' = y. [para(77(a,1),20(a,1,1,2,1,2)),rewrite([7(6)])]. given #531 (T,wt=20): 150 (x + ((x + y)' + (y' + x)'')')' = (x + y)'. [para(21(a,1),8(a,1,1,1))]. given #532 (T,wt=20): 169 ((x + (g(y) + (y + y'')'))' + (y + x)')' = x. [para(27(a,1),21(a,1,1,2,1,1))]. given #533 (A,wt=15): 126 (x + ((y + z)' + (z + y')'))' != z # answer(Winker2b). [para(20(a,1),17(a,2))]. given #534 (F,wt=10): 22710 h(h(x))'' != x + g(x) # answer(Winker2a). [para(12(a,1),5210(a,1,1,1,1))]. given #535 (F,wt=10): 22742 x + h(h(y)) != y + g(y) # answer(Winker1a). [para(12(a,1),5221(a,1,2,1))]. given #536 (F,wt=10): 23150 (x + g(x))' != g(h(h(x))) # answer(Winker2a). [para(12(a,1),5234(a,1,1,1)),flip(a)]. given #537 (F,wt=10): 23196 g(h(h(x)))' != x + g(x) # answer(Winker2a). [para(12(a,1),5304(a,1,1,1,1))]. given #538 (T,wt=20): 170 ((x + (y + (g(y) + h(y))'))' + (g(y) + x)')' = x. [para(77(a,1),21(a,1,1,2,1,1))]. given #539 (T,wt=20): 194 (x + ((y + x)' + (y' + x)'')')' = (y + x)'. [para(111(a,1),8(a,1,1,1))]. given #540 (T,wt=20): 210 ((x + y)' + (g(x) + ((x + x'')' + y))')' = y. [para(27(a,1),111(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #541 (T,wt=20): 211 ((g(x) + y)' + (x + ((g(x) + h(x))' + y))')' = y. [para(77(a,1),111(a,1,1,2,1,1)),rewrite([7(6),6(11)])]. given #542 (A,wt=13): 128 g((x + y)' + (y + x')') != y # answer(Winker2a). [para(20(a,1),43(a,1)),flip(a)]. given #543 (F,wt=10): 23231 x + g(x) != h(h(h(h(x)))) # answer(Winker1a). [para(12(a,1),5744(a,1,1,1,1)),flip(a)]. given #544 (F,wt=10): 23368 (x + h(y + z))' != z' # answer(Winker2a). [para(6(a,1),5798(a,1,1,2,1))]. given #545 (F,wt=10): 23414 (x + h(y + z))'' != z # answer(Winker2a). [para(6(a,1),7289(a,1,1,1,2,1))]. given #546 (F,wt=10): 23633 g(x + h(y + z)) != z' # answer(Winker2a). [para(6(a,1),8143(a,1,1,2,1))]. given #547 (T,wt=20): 235 ((x + y)' + (g(y) + ((y + y'')' + x))')' = x. [para(27(a,1),112(a,1,1,1,1,2)),rewrite([7(9)])]. given #548 (T,wt=20): 236 ((x + g(y))' + (y + ((g(y) + h(y))' + x))')' = x. [para(77(a,1),112(a,1,1,1,1,2)),rewrite([7(9)])]. given #549 (T,wt=20): 346 ((x + y)' + (y + (g(x) + (x + x'')'))')' = y. [para(27(a,1),148(a,1,1,1,1,1))]. given #550 (T,wt=20): 347 ((g(x) + y)' + (y + (x + (g(x) + h(x))'))')' = y. [para(77(a,1),148(a,1,1,1,1,1))]. given #551 (A,wt=14): 129 h((x + y)' + (y + x')')' != y # answer(Winker2a). [para(20(a,1),45(a,2))]. given #552 (F,wt=10): 23679 g(x + h(y + z))' != z # answer(Winker2a). [para(6(a,1),9231(a,1,1,1,2,1))]. given #553 (F,wt=10): 24023 x + h(y + z) != z + x # answer(Winker1a). [para(6(a,1),10013(a,1,2,1))]. given #554 (F,wt=10): 24041 h(h(x + h(y + z))) != z # answer(Winker1a). [para(6(a,1),10817(a,1,1,1,2,1))]. given #555 (F,wt=10): 24286 h(h(h(x + y)))' != y' # answer(Winker2a). [para(6(a,1),11424(a,1,1,1,1,1))]. Low Water (displace, False_semantics): id=25150, wt=18 given #556 (T,wt=20): 364 (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 #557 (T,wt=20): 373 (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 #558 (T,wt=20): 579 ((x + x)' + g(g(x) + (x + (g(x) + h(x)))'))' = x. [para(103(a,1),121(a,1,1,2,1,1)),rewrite([103(16),6(11),103(20)])]. given #559 (T,wt=20): 587 (x + (y + (z + (y + (z + x))')))' = g(x + (y + z)). [para(7(a,1),363(a,1,1,2,2,1)),rewrite([7(5)])]. given #560 (A,wt=14): 130 g((x + y)' + (y + x')') != y' # answer(Winker2b). [para(20(a,1),48(a,1,1)),flip(a)]. given #561 (F,wt=10): 24489 h(h(h(x + y)))'' != y # answer(Winker2a). [para(6(a,1),11589(a,1,1,1,1,1,1))]. given #562 (F,wt=10): 24638 x + h(h(h(y + z))) != z # answer(Winker1a). [para(6(a,1),12241(a,1,2,1,1,1))]. given #563 (F,wt=10): 24801 g(h(h(h(x + y)))) != y' # answer(Winker2a). [para(6(a,1),13099(a,1,1,1,1,1))]. given #564 (F,wt=10): 24844 g(h(h(h(x + y))))' != y # answer(Winker2a). [para(6(a,1),13700(a,1,1,1,1,1,1))]. given #565 (T,wt=20): 588 (x + (y + (z + (z + (x + y))')))' = g(x + (y + z)). [para(7(a,1),363(a,1,1)),rewrite([7(9)])]. given #566 (T,wt=20): 595 (x + (y + (z + (x + (z + y))')))' = g(x + (y + z)). [para(19(a,1),363(a,1,1,2,2,1)),rewrite([7(6),7(9)])]. given #567 (T,wt=20): 606 (g(x + y) + (x + (y + (y + x)''))')' = x + y. [para(363(a,1),22(a,1,1,1))]. given #568 (T,wt=20): 627 (g(h(x)) + (x + (x + (x + (g(x) + h(x)))))')' = h(x). [para(32(a,1),29(a,1,1,2,1))]. given #569 (A,wt=38): 135 (g((x + y)' + (y + x')') + (y' + ((x + y)' + (y + x')'))')' = (x + y)' + (y + x')'. [para(20(a,1),27(a,1,1,2,1,2,1)),rewrite([6(15)])]. given #570 (F,wt=10): 25328 h(x + h(h(y + z))) != z # answer(Winker1a). [para(6(a,1),14184(a,1,1,2,1,1))]. given #571 (F,wt=10): 25507 h(h(h(h(h(x + y))))) != y # answer(Winker1a). [para(6(a,1),14210(a,1,1,1,1,1,1))]. given #572 (F,wt=10): 26038 x + (y + y) != x + h(y) # answer(Winker1b). [para(26022(a,1),38(a,1)),flip(a)]. given #573 (F,wt=10): 26092 h(x + h(y))' != g(y)' # answer(Winker2a). [para(26022(a,1),2573(a,1,1,1))]. given #574 (T,wt=20): 866 (g(x) + (x + (x + (x + (x + (g(x) + g(x))))))')' = x. [para(34(a,1),103(a,1,1,2,1,2)),rewrite([6(4),19(5)])]. given #575 (T,wt=20): 992 ((x + y)' + (x + (x + (y' + (x + y)')))')' = x. [para(25(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #576 (T,wt=20): 1017 (x + (x + (g(x) + (x + (x + g(x)))''))')' = g(x). [para(66(a,1),25(a,1,1,2,1,2,2)),rewrite([6(7),66(17)])]. given #577 (T,wt=20): 1182 (g(x) + (g(x) + (x' + (x + x'')'))')' = x'. [para(27(a,1),157(a,1,1,1,1)),rewrite([27(14),6(9),19(9),27(19)])]. given #578 (A,wt=21): 136 (x + (g(x)' + (x + x'')')')' = (x + x'')'. [para(27(a,1),20(a,1,1,1)),rewrite([6(7)])]. given #579 (F,wt=10): 26093 h(x + h(y))'' != g(y) # answer(Winker2a). [para(26022(a,1),3182(a,1,1,1,1))]. given #580 (F,wt=10): 26094 x + h(y + h(z)) != g(z) # answer(Winker1a). [para(26022(a,1),3193(a,1,2,1))]. given #581 (F,wt=10): 26095 g(h(x + h(y))) != g(y)' # answer(Winker2a). [para(26022(a,1),3652(a,1,1,1))]. given #582 (F,wt=10): 26096 g(h(x + h(y)))' != g(y) # answer(Winker2a). [para(26022(a,1),3754(a,1,1,1,1))]. given #583 (T,wt=20): 2813 (h(x)' + (x + (x + (x' + h(x)'))'')')' = x. [para(1835(a,1),8(a,1,1,1))]. given #584 (T,wt=20): 3214 ((x + y)' + (g(y) + (x + (y + y'')'))')' = x. [para(27(a,1),51(a,1,1,2,1,2)),rewrite([6(11)])]. given #585 (T,wt=20): 3215 ((x + g(y))' + (y + (x + (g(y) + h(y))'))')' = x. [para(77(a,1),51(a,1,1,2,1,2)),rewrite([6(11)])]. given #586 (T,wt=20): 3336 (x + (g(x) + (g(h(x)') + h(h(x)')'))')' = g(x). [para(74(a,1),76(a,1,1,1))]. given #587 (A,wt=21): 138 (g(x) + (x' + (g(x) + h(x))')')' = (g(x) + h(x))'. [para(77(a,1),20(a,1,1,1)),rewrite([6(7)])]. given #588 (F,wt=10): 26097 h(h(h(x + h(y)))) != g(y) # answer(Winker1a). [para(26022(a,1),4798(a,1,1,1,1))]. given #589 (F,wt=10): 26455 x + h(y) != y + (y + y) # answer(Winker1b). [para(26410(a,1),38(a,1))]. given #590 (F,wt=10): 26641 g(h(x))' != x + (x + x) # answer(Winker2a). [para(26473(a,1),16(a,1)),flip(a)]. given #591 (F,wt=10): 26643 (x + (x + x))' != g(h(x)) # answer(Winker2a). [para(26473(a,1),41(a,1,1))]. given #592 (T,wt=20): 4049 ((x + y)' + (g(x) + (y + (x + x'')'))')' = y. [para(27(a,1),161(a,1,1,2,1,1)),rewrite([6(11)])]. given #593 (T,wt=20): 4050 ((x + (y + (g(x) + h(x))'))' + (g(x) + y)')' = y. [para(77(a,1),161(a,1,1,2,1,1))]. given #594 (T,wt=20): 4371 (x + (g(g(x)) + (h(x)' + h(g(x))'))')' = h(x)'. [para(74(a,1),167(a,1,1,2)),rewrite([19(9),6(11)])]. given #595 (T,wt=20): 5047 ((g(x) + y)' + (x + (y + (g(x) + h(x))'))')' = y. [para(77(a,1),339(a,1,1,1,1,1))]. given #596 (A,wt=21): 140 (x + ((x + y')' + (y + x)'')')' = (x + y')'. [para(20(a,1),20(a,1,1,1))]. given #597 (F,wt=10): 27047 x + h(y) != y + (y + x) # answer(Winker1b). [para(6(a,1),26038(a,1)),rewrite([7(2)]),flip(a)]. given #598 (F,wt=10): 27050 x + h(y) != y + (x + y) # answer(Winker1b). [para(19(a,1),26038(a,1)),flip(a)]. given #599 (F,wt=11): 143 x + h(y) != y + (y + g(y)) # answer(Winker1b). [para(12(a,1),38(a,1,2))]. given #600 (F,wt=11): 145 x + (y + (z + u)) != y + u # answer(Winker1b). [para(19(a,1),38(a,1,2))]. given #601 (T,wt=20): 5829 (x + (x + (g(x) + (g(x) + (x + x)'')))')' = g(x). [para(905(a,1),8(a,1,1,2)),rewrite([19(8),6(10)])]. given #602 (T,wt=20): 5904 (x + (x + (x + (g(x) + (g(x) + x''))))')' = g(x). [para(938(a,1),8(a,1,1,2)),rewrite([19(8),19(7),6(10)])]. given #603 (T,wt=20): 6117 (x' + (g(x) + (g(x) + (x' + h(x)')))')' = g(x). [para(1180(a,1),8(a,1,1,2)),rewrite([6(11)])]. given #604 (T,wt=20): 8275 ((x + y)' + ((y + y'')' + (x + g(y)))')' = x. [para(27(a,1),3202(a,1,1,2,1,2)),rewrite([6(11)])]. given #605 (A,wt=21): 141 (((x + y)' + ((y + x')' + z))' + (z + y)')' = z. [para(20(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #606 (F,wt=11): 146 (x + (y + z))'' != x + y # answer(Winker2a). [para(7(a,1),41(a,1,1,1))]. given #607 (F,wt=8): 27402 g(h(x))' != x + x # answer(Winker2a). [para(368(a,1),146(a,1,1))]. given #608 (F,wt=10): 27394 (x + h(y))'' != x + y # answer(Winker2a). [para(12(a,1),146(a,1,1,1,2))]. given #609 (F,wt=10): 27398 (x + h(y))'' != y + y # answer(Winker2a). [para(34(a,2),146(a,1,1,1))]. given #610 (T,wt=20): 8276 (((g(x) + h(x))' + (y + x))' + (y + g(x))')' = y. [para(77(a,1),3202(a,1,1,2,1,2))]. given #611 (T,wt=20): 9582 (x + (x + (g(x) + (g(x') + h(x')')))')' = g(x). [para(3328(a,1),8(a,1,1,2)),rewrite([19(9),6(11)])]. given #612 (T,wt=20): 10224 ((x + y)' + ((x + x'')' + (y + g(x)))')' = y. [para(27(a,1),4030(a,1,1,2,1,1)),rewrite([6(11)])]. given #613 (T,wt=20): 10225 ((g(x) + y)' + ((g(x) + h(x))' + (y + x))')' = y. [para(77(a,1),4030(a,1,1,2,1,1)),rewrite([6(11)])]. given #614 (A,wt=21): 151 ((x + y)' + (x + ((y + z)' + (z' + y)'))')' = x. [para(21(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #615 (F,wt=10): 27399 (x + h(y))'' != y + x # answer(Winker2a). [para(52(a,1),146(a,1,1,1))]. given #616 (F,wt=11): 281 x + (y + (z + u)) != y + z # answer(Winker1a). [para(7(a,1),53(a,1,2))]. given #617 (F,wt=11): 287 h(x)'' != x + (x + g(x)) # answer(Winker2a). [para(12(a,1),124(a,1,1,1))]. given #618 (F,wt=11): 288 (x + (y + z))'' != x + z # answer(Winker2a). [para(19(a,1),124(a,1,1,1))]. given #619 (T,wt=20): 11034 ((x + g(y))' + ((g(y) + h(y))' + (x + y))')' = x. [para(77(a,1),4872(a,1,1,1,1,2))]. given #620 (T,wt=20): 11812 ((x + y)' + (y + (y + (x' + (x + y)')))')' = y. [para(117(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #621 (T,wt=20): 12252 ((x + y)' + (x + (y' + (x + (x + y)')))')' = x. [para(152(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #622 (T,wt=20): 12343 ((x + y)' + (y' + (x + (x + (x + y)')))')' = x. [para(152(a,1),51(a,1,1,2)),rewrite([6(10)])]. given #623 (A,wt=21): 153 ((x + ((y + z)' + (y + z')'))' + (y + x)')' = x. [para(8(a,1),21(a,1,1,2,1,1))]. given #624 (F,wt=11): 291 g(g(x) + (x + x)')' != x # answer(Winker2a). [para(29(a,1),286(a,2))]. given #625 (F,wt=11): 495 g(x + (y + z)) != (x + y)' # answer(Winker2a). [para(7(a,1),369(a,1,1))]. given #626 (F,wt=10): 27598 (x + y)' != g(x + h(y)) # answer(Winker2a). [para(12(a,1),495(a,1,1,2)),flip(a)]. given #627 (F,wt=10): 27602 g(x + h(y)) != (y + y)' # answer(Winker2a). [para(34(a,2),495(a,1,1))]. given #628 (T,wt=20): 12614 ((x + y)' + (y + (x' + (y + (x + y)')))')' = y. [para(196(a,1),8(a,1,1,2)),rewrite([6(10)])]. given #629 (T,wt=20): 12718 ((x + y)' + (x' + (y + (y + (x + y)')))')' = y. [para(196(a,1),51(a,1,1,2)),rewrite([6(10)])]. given #630 (T,wt=20): 16799 (x + (y + (g(y + x) + h(x + y))'))' = g(y + x). [para(16756(a,1),8(a,1,1,2)),rewrite([6(8),7(8)])]. Low Water (keep, True_semantics): wt=28 given #631 (T,wt=20): 17489 (g(x + y) + (y + (x + (y + x)''))')' = y + x. [para(6(a,1),85(a,1,1,1,1))]. given #632 (A,wt=25): 155 (x + ((x + y)' + (y' + x)'))' = g((x + y)' + (y' + x)'). [para(21(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #633 (F,wt=10): 27603 (x + y)' != g(y + h(x)) # answer(Winker2a). [para(52(a,1),495(a,1,1)),flip(a)]. given #634 (F,wt=10): 27623 g(g(x) + h(h(x)')) != x # answer(Winker2a). [para(74(a,1),27598(a,1)),flip(a)]. given #635 (F,wt=11): 501 g(g(x) + (h(x)' + y)) != x # answer(Winker2a). [para(74(a,1),369(a,2)),rewrite([7(5)])]. given #636 (F,wt=11): 517 g(h(g(x) + (x + x)')) != x # answer(Winker2a). [para(29(a,1),498(a,1)),flip(a)]. given #637 (T,wt=20): 17495 (g(x + y) + (y + (x + (x + y)''))')' = x + y. [para(19(a,1),85(a,1,1,2,1))]. given #638 (T,wt=20): 23602 (x + (y + (g(x + y) + h(y + x))'))' = g(x + y). [para(6(a,1),100(a,1,1,2,2,1,2,1))]. given #639 (T,wt=20): 23609 (x + (y + (g(y + x) + h(y + x))'))' = g(y + x). [para(19(a,1),100(a,1,1))]. given #640 (T,wt=20): 26755 (x + (x + (h(x)' + (g(x) + h(x))'))')' = h(x)'. [para(74(a,1),170(a,1,1,2)),rewrite([19(8),6(10)])]. given #641 (A,wt=28): 158 (h(x')' + (x + (x' + (x' + g(x'))))')' = x' + (x' + g(x')). [para(12(a,1),21(a,1,1,2,1)),rewrite([6(7),6(12)])]. given #642 (F,wt=11): 533 g(x + (y + z))' != x + y # answer(Winker2a). [para(7(a,1),380(a,1,1,1))]. given #643 (F,wt=10): 27724 g(x + h(y))' != x + y # answer(Winker2a). [para(12(a,1),533(a,1,1,1,2))]. given #644 (F,wt=10): 27728 g(x + h(y))' != y + y # answer(Winker2a). [para(34(a,2),533(a,1,1,1))]. given #645 (F,wt=10): 27729 g(x + h(y))' != y + x # answer(Winker2a). [para(52(a,1),533(a,1,1,1))]. given #646 (T,wt=20): 26942 (x + (y + (z + (z + (y + x))')))' = g(x + (y + z)). [para(19(a,1),587(a,1,1,2,2,2,1))]. given #647 (T,wt=20): 27066 ((x + y)' + (y + (y + (x' + (y + x)')))')' = y. [para(6(a,1),992(a,1,1,1,1))]. given #648 (T,wt=20): 27067 ((x + y)' + (x + (x + (y' + (y + x)')))')' = x. [para(6(a,1),992(a,1,1,2,1,2,2,2,1))]. given #649 (T,wt=20): 27553 ((x + y)' + (y + (x' + (y + (y + x)')))')' = y. [para(6(a,1),12252(a,1,1,1,1))]. given #650 (A,wt=15): 159 ((x + y)' + ((y' + x)' + z))' != x # answer(Winker2a). [para(21(a,1),16(a,2)),rewrite([7(7)])]. given #651 (F,wt=11): 766 (x + (x + g(x)))' != g(h(x)) # answer(Winker2a). [para(12(a,1),494(a,1,1)),flip(a)]. given #652 (F,wt=11): 767 g(x + (y + z)) != (x + z)' # answer(Winker2a). [para(19(a,1),494(a,1,1))]. given #653 (F,wt=11): 769 g(x + (g(y) + h(y)')) != y # answer(Winker2a). [para(74(a,1),494(a,2))]. given #654 (F,wt=11): 789 g(h(x))' != x + (x + g(x)) # answer(Winker2a). [para(12(a,1),532(a,1,1,1))]. given #655 (T,wt=20): 27554 ((x + y)' + (x + (y' + (x + (y + x)')))')' = x. [para(6(a,1),12252(a,1,1,2,1,2,2,2,1))]. given #656 (T,wt=20): 27567 ((x + y)' + (x' + (y + (y + (y + x)')))')' = y. [para(6(a,1),12343(a,1,1,1,1))]. given #657 (T,wt=20): 27568 ((x + y)' + (y' + (x + (x + (y + x)')))')' = x. [para(6(a,1),12343(a,1,1,2,1,2,2,2,1))]. given #658 (T,wt=21): 172 (x + ((y' + x)' + (x + y)'')')' = (y' + x)'. [para(21(a,1),20(a,1,1,1))]. given #659 (A,wt=15): 160 (x + ((y + z)' + (z' + y)'))' != y # answer(Winker2b). [para(21(a,1),17(a,2))]. given #660 (F,wt=11): 790 g(x + (y + z))' != x + z # answer(Winker2a). [para(19(a,1),532(a,1,1,1))]. given #661 (F,wt=11): 836 g(x) + (y + x) != y + h(x) # answer(Winker1b). [para(34(a,2),38(a,1)),flip(a)]. given #662 (F,wt=11): 1076 (x + h(y + y'))' != g(y) # answer(Winker2a). [para(10(a,1),824(a,2))]. given #663 (F,wt=11): 1104 g(x + h(y + y')) != g(y) # answer(Winker2a). [para(10(a,1),863(a,2))]. given #664 (T,wt=21): 173 (((x + y)' + ((y' + x)' + z))' + (z + x)')' = z. [para(21(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #665 (T,wt=21): 174 ((x + ((y + z)' + (z + y')'))' + (z + x)')' = x. [para(20(a,1),21(a,1,1,2,1,1))]. given #666 (T,wt=21): 176 ((x + ((y + z)' + (z' + y)'))' + (y + x)')' = x. [para(21(a,1),21(a,1,1,2,1,1))]. given #667 (T,wt=21): 180 ((x + g(y))' + (x + (y + (y + (y + g(y)))'))')' = x. [para(66(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #668 (A,wt=13): 163 g((x + y)' + (y' + x)') != x # answer(Winker2a). [para(21(a,1),43(a,1)),flip(a)]. given #669 (F,wt=11): 1283 x + h(y) != y + (g(y) + x) # answer(Winker1b). [para(620(a,2),38(a,1))]. given #670 (F,wt=11): 1382 x + (y + (z + u)) != x + z # answer(Winker1a). [para(19(a,1),36(a,1,2))]. given #671 (F,wt=8): 27882 h(x + y) != x + x # answer(Winker1a). [para(33(a,1),1382(a,1))]. given #672 (F,wt=8): 27885 h(x + y) != y + y # answer(Winker1a). [para(6(a,1),27882(a,1,1))]. given #673 (T,wt=21): 190 ((x + ((x + (x + g(x)))' + y))' + (y + g(x))')' = y. [para(66(a,1),20(a,1,1,2,1,2)),rewrite([7(6)])]. given #674 (T,wt=21): 191 ((x + (y + (y + (y + g(y)))'))' + (g(y) + x)')' = x. [para(66(a,1),21(a,1,1,2,1,1))]. given #675 (T,wt=21): 195 ((x + y)' + (x + ((z + y)' + (z' + y)'))')' = x. [para(111(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #676 (T,wt=21): 197 ((x + y)' + ((x + z)' + ((x + z')' + y))')' = y. [para(8(a,1),111(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #677 (A,wt=14): 164 h((x + y)' + (y' + x)')' != x # answer(Winker2a). [para(21(a,1),45(a,2))]. given #678 (F,wt=9): 27891 h(h(x + y)) != x + x # answer(Winker1a). [para(33(a,1),27882(a,1,1))]. given #679 (F,wt=8): 27942 x + x != h(h(h(x))) # answer(Winker1a). [para(12(a,1),27891(a,1,1,1)),flip(a)]. given #680 (F,wt=9): 27940 h(h(x + y)) != y + y # answer(Winker1a). [para(6(a,1),27891(a,1,1,1))]. given #681 (F,wt=10): 27887 h(x + (y + z)) != y + y # answer(Winker1a). [para(19(a,1),27882(a,1,1))]. given #682 (T,wt=21): 212 (x + ((y' + x)' + (y + x)'')')' = (y' + x)'. [para(111(a,1),20(a,1,1,1))]. given #683 (T,wt=21): 213 (((x + y)' + ((x' + y)' + z))' + (z + y)')' = z. [para(111(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #684 (T,wt=21): 214 ((x + y)' + ((z + x)' + ((x + z')' + y))')' = y. [para(20(a,1),111(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #685 (T,wt=21): 215 ((x + ((y + z)' + (y' + z)'))' + (z + x)')' = x. [para(111(a,1),21(a,1,1,2,1,1))]. given #686 (A,wt=14): 165 g((x + y)' + (y' + x)') != x' # answer(Winker2b). [para(21(a,1),48(a,1,1)),flip(a)]. given #687 (F,wt=10): 27922 h(x + (y + z)) != z + z # answer(Winker1a). [para(7(a,1),27885(a,1,1))]. given #688 (F,wt=10): 27945 h(h(x + h(y))) != y + y # answer(Winker1a). [para(34(a,2),27891(a,1,1,1))]. given #689 (F,wt=10): 27948 h(h(h(x + y))) != x + x # answer(Winker1a). [para(33(a,1),27891(a,1,1,1))]. given #690 (F,wt=9): 27987 x + x != h(h(h(h(x)))) # answer(Winker1a). [para(12(a,1),27948(a,1,1,1,1)),flip(a)]. given #691 (T,wt=21): 217 ((x + y)' + ((x + z)' + ((z' + x)' + y))')' = y. [para(21(a,1),111(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #692 (T,wt=21): 218 ((g(x) + y)' + (x + ((x + (x + g(x)))' + y))')' = y. [para(66(a,1),111(a,1,1,2,1,1)),rewrite([7(6),6(11)])]. given #693 (T,wt=21): 219 ((x + y)' + ((z + x)' + ((z' + x)' + y))')' = y. [para(111(a,1),111(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #694 (T,wt=21): 222 ((x + y)' + (x + ((y + z')' + (z + y)'))')' = x. [para(112(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #695 (A,wt=38): 168 (g((x + y)' + (y' + x)') + (x' + ((x + y)' + (y' + x)'))')' = (x + y)' + (y' + x)'. [para(21(a,1),27(a,1,1,2,1,2,1)),rewrite([6(15)])]. given #696 (F,wt=10): 27985 h(h(h(x + y))) != y + y # answer(Winker1a). [para(6(a,1),27948(a,1,1,1,1))]. given #697 (F,wt=11): 1416 x + (y + g(y)) != x + h(y) # answer(Winker1b). [para(830(a,1),38(a,1)),flip(a)]. given #698 (F,wt=11): 1453 x + h(y) != y + (x + g(y)) # answer(Winker1b). [para(1270(a,2),38(a,1))]. given #699 (F,wt=11): 1768 (x + (y + (z + u)))' != u' # answer(Winker2b). [para(7(a,1),46(a,1,1,2))]. given #700 (T,wt=21): 223 ((x + y)' + ((y + z)' + ((y + z')' + x))')' = x. [para(8(a,1),112(a,1,1,1,1,2)),rewrite([7(9)])]. given #701 (T,wt=21): 237 (((x + y')' + ((y + x)' + z))' + (z + x)')' = z. [para(112(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #702 (T,wt=21): 238 ((x + y)' + ((z + y)' + ((y + z')' + x))')' = x. [para(20(a,1),112(a,1,1,1,1,2)),rewrite([7(9)])]. given #703 (T,wt=21): 239 ((x + ((y + z')' + (z + y)'))' + (y + x)')' = x. [para(112(a,1),21(a,1,1,2,1,1))]. given #704 (A,wt=25): 171 (g(x') + (x + (g(x') + h(x'))')')' = (g(x') + h(x'))'. [para(77(a,1),21(a,1,1,2)),rewrite([6(7),6(11)])]. given #705 (F,wt=7): 28029 h(x)' != g(x)' # answer(Winker2b). [para(12(a,1),1768(a,1,1))]. given #706 (F,wt=11): 2520 (x + (y + z))' != (z + x)' # answer(Winker2a). [para(6(a,1),40(a,1,1)),rewrite([7(2)])]. given #707 (F,wt=10): 28076 (x' + (y + x))' != g(x) # answer(Winker2a). [para(10(a,1),2520(a,2))]. given #708 (F,wt=11): 2521 (x + (y + z))' != (y + x)' # answer(Winker2a). [para(6(a,1),40(a,2,1))]. given #709 (T,wt=21): 240 ((x + y)' + ((y + z)' + ((z' + y)' + x))')' = x. [para(21(a,1),112(a,1,1,1,1,2)),rewrite([7(9)])]. given #710 (T,wt=21): 241 ((x + g(y))' + (y + ((y + (y + g(y)))' + x))')' = x. [para(66(a,1),112(a,1,1,1,1,2)),rewrite([7(9)])]. given #711 (T,wt=21): 242 ((x + y)' + ((x + z')' + ((z + x)' + y))')' = y. [para(112(a,1),111(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #712 (T,wt=21): 243 ((x + y)' + ((z + y)' + ((z' + y)' + x))')' = x. [para(111(a,1),112(a,1,1,1,1,2)),rewrite([7(9)])]. given #713 (A,wt=23): 178 (x + (y + (x + (y + (x + (y + g(x + y)))))'))' = g(x + y). [para(7(a,1),66(a,1,1,2,1,2)),rewrite([19(7),19(6),7(5),7(9)])]. given #714 (F,wt=10): 28105 h(x + y)' != (y + x)' # answer(Winker2a). [para(33(a,1),2521(a,1,1))]. given #715 (F,wt=11): 2527 (x + g(x))' != g(x + x') # answer(Winker2a). [para(31(a,1),40(a,1)),flip(a)]. given #716 (F,wt=11): 2548 h(h(x + (y + z))) != x + y # answer(Winker1a). [para(7(a,1),2242(a,1,1,1))]. given #717 (F,wt=10): 28129 h(h(x + h(y))) != x + y # answer(Winker1a). [para(12(a,1),2548(a,1,1,1,2))]. given #718 (T,wt=21): 244 ((x + y)' + ((y + z')' + ((z + y)' + x))')' = x. [para(112(a,1),112(a,1,1,1,1,2)),rewrite([7(9)])]. given #719 (T,wt=21): 302 ((x + y')' + (x + (g(y) + (y' + y')'))')' = x. [para(121(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])]. given #720 (T,wt=18): 28154 (g(x) + (x + (g(x) + (x' + x')'))')' = x. [para(10(a,1),302(a,1,1,1))]. given #721 (T,wt=21): 318 ((g(x) + ((x' + x')' + y))' + (y + x')')' = y. [para(121(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #722 (A,wt=24): 181 (x + (g(x) + (x + (x + g(x)))'))' = g(x + (x + (x + g(x)))'). [para(66(a,1),10(a,1,1,2)),rewrite([6(7),19(7)])]. given #723 (F,wt=10): 28133 h(h(x + h(y))) != y + x # answer(Winker1a). [para(52(a,1),2548(a,1,1,1))]. given #724 (F,wt=11): 2558 x + (x + g(x)) != h(h(h(x))) # answer(Winker1a). [para(12(a,1),2547(a,1,1,1)),flip(a)]. given #725 (F,wt=11): 2559 h(h(x + (y + z))) != x + z # answer(Winker1a). [para(19(a,1),2547(a,1,1,1))]. Low Water (keep, False_semantics): wt=17 given #726 (F,wt=11): 2571 h(x + (x' + y))' != g(x) # answer(Winker2a). [para(10(a,1),2177(a,2)),rewrite([7(3)])]. given #727 (T,wt=21): 320 ((x + (g(y) + (y' + y')'))' + (y' + x)')' = x. [para(121(a,1),21(a,1,1,2,1,1))]. given #728 (T,wt=21): 322 (g(x + (x + (x + g(x)))') + (g(x) + g(x))')' = g(x). [para(66(a,1),121(a,1,1,2,1,1)),rewrite([66(13),66(18)])]. given #729 (T,wt=21): 323 ((x' + y)' + (g(x) + ((x' + x')' + y))')' = y. [para(121(a,1),111(a,1,1,2,1,1)),rewrite([7(7),6(12)])]. given #730 (T,wt=21): 325 ((x + y')' + (g(y) + ((y' + y')' + x))')' = x. [para(121(a,1),112(a,1,1,1,1,2)),rewrite([7(10)])]. given #731 (A,wt=15): 182 (x + ((x + (x + g(x)))' + y))' != g(x) # answer(Winker2a). [para(66(a,1),16(a,2)),rewrite([7(6)])]. given #732 (F,wt=10): 28192 h(x + h(x'))' != g(x) # answer(Winker2a). [para(12(a,1),2571(a,1,1,1,2))]. given #733 (F,wt=11): 3139 h(h(g(x) + h(x)'))' != x # answer(Winker2a). [para(74(a,1),2572(a,2))]. given #734 (F,wt=11): 3614 (x + (y + h(x')))' != g(x) # answer(Winker2a). [para(34(a,2),44(a,1,1,2))]. given #735 (F,wt=11): 3632 (x + h(x' + y))' != g(x) # answer(Winker2a). [para(33(a,1),44(a,1,1,2))]. given #736 (T,wt=21): 330 ((x' + x')' + g(g(x) + (x' + x')'))' = x'. [para(121(a,1),121(a,1,1,2,1,1)),rewrite([121(15),6(12),121(20)])]. given #737 (T,wt=21): 332 ((x + y)' + (x + ((z' + y)' + (y + z)'))')' = x. [para(148(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. given #738 (T,wt=21): 333 ((x + y)' + (y + ((x + z)' + (x + z')'))')' = y. [para(8(a,1),148(a,1,1,1,1,1))]. given #739 (T,wt=21): 348 (((x' + y)' + ((y + x)' + z))' + (z + y)')' = z. [para(148(a,1),20(a,1,1,2,1,2)),rewrite([7(7)])]. given #740 (A,wt=15): 184 (x + (y + (y + (y + g(y)))'))' != g(y) # answer(Winker2b). [para(66(a,1),17(a,2))]. given #741 (F,wt=10): 28211 (x + h(h(x')))' != g(x) # answer(Winker2a). [para(12(a,1),3632(a,1,1,2,1))]. given #742 (F,wt=10): 28229 g(x + (x + g(x))) != g(x) # answer(Winker2b). [para(363(a,1),184(a,1)),rewrite([6(3)])]. given #743 (F,wt=11): 3650 g(h(x + (x' + y))) != g(x) # answer(Winker2a). [para(10(a,1),2198(a,2)),rewrite([7(3)])]. given #744 (F,wt=10): 28232 g(h(x + h(x'))) != g(x) # answer(Winker2a). [para(12(a,1),3650(a,1,1,1,2))]. given #745 (T,wt=21): 349 ((x + y)' + (y + ((z + x)' + (x + z')'))')' = y. [para(20(a,1),148(a,1,1,1,1,1))]. given #746 (T,wt=21): 350 ((x + ((y' + z)' + (z + y)'))' + (z + x)')' = x. [para(148(a,1),21(a,1,1,2,1,1))]. given #747 (T,wt=21): 351 ((x + y)' + (y + ((x + z)' + (z' + x)'))')' = y. [para(21(a,1),148(a,1,1,1,1,1))]. given #748 (T,wt=21): 352 ((g(x) + y)' + (y + (x + (x + (x + g(x)))'))')' = y. [para(66(a,1),148(a,1,1,1,1,1))]. given #749 (A,wt=13): 185 g(x + (x + (x + g(x)))') != g(x) # answer(Winker2a). [para(66(a,1),43(a,1)),flip(a)]. given #750 (F,wt=11): 3707 g(h(h(g(x) + h(x)'))) != x # answer(Winker2a). [para(74(a,1),3651(a,1)),flip(a)]. given #751 (F,wt=11): 4807 h(x + (y + y'))' != g(y) # answer(Winker2a). [para(10(a,1),2568(a,2))]. given #752 (F,wt=11): 5236 g(h(x + (y + y'))) != g(y) # answer(Winker2a). [para(10(a,1),3647(a,2))]. given #753 (F,wt=11): 5347 g(g(x) + h(x)') != g(h(x)) # answer(Winker2b). [para(368(a,1),46(a,1)),rewrite([78(8)]),flip(a)]. given #754 (T,wt=21): 353 ((x + y)' + ((z' + x)' + ((x + z)' + y))')' = y. [para(148(a,1),111(a,1,1,2,1,1)),rewrite([7(7),6(11)])]. given #755 (T,wt=21): 354 ((x + y)' + (y + ((z + x)' + (z' + x)'))')' = y. [para(111(a,1),148(a,1,1,1,1,1))]. given #756 (T,wt=21): 355 ((x + y)' + ((z' + y)' + ((y + z)' + x))')' = x. [para(148(a,1),112(a,1,1,1,1,2)),rewrite([7(9)])]. given #757 (T,wt=21): 356 ((x + y)' + (y + ((x + z')' + (z + x)'))')' = y. [para(112(a,1),148(a,1,1,1,1,1))]. given #758 (A,wt=14): 186 h(x + (x + (x + g(x)))')' != g(x) # answer(Winker2a). [para(66(a,1),45(a,2))]. given #759 (F,wt=11): 5721 x + (y + (z + u)) != x + u # answer(Winker1b). [para(7(a,1),54(a,1,2))]. given #760 (F,wt=11): 5758 (x + (y + (z + u)))' != z' # answer(Winker2a). [para(7(a,1),55(a,1,1))]. given #761 (F,wt=11): 6260 (x + (y + z))' != (z + y)' # answer(Winker2b). [para(6(a,1),56(a,1,1)),rewrite([7(2)])]. given #762 (F,wt=11): 6265 (g(x) + (y + h(x)'))' != x # answer(Winker2b). [para(74(a,1),56(a,2))]. given #763 (T,wt=21): 361 ((x' + y)' + (y + (g(x) + (x' + x')'))')' = y. [para(121(a,1),148(a,1,1,1,1,1))]. given #764 (T,wt=21): 362 ((x + y)' + (y + ((z' + x)' + (x + z)'))')' = y. [para(148(a,1),148(a,1,1,1,1,1))]. given #765 (T,wt=21): 416 (g(x + x') + (x + (g(x) + x''))')' = x + g(x). [para(31(a,1),22(a,1,1,1))]. given #766 (T,wt=21): 446 (g(x) + (x + (g(x) + (x + x'')'')'')')' = x. [para(27(a,1),23(a,1,1,2,1,1)),rewrite([27(21)])]. given #767 (A,wt=14): 187 g(x + (x + (x + g(x)))') != g(x)' # answer(Winker2b). [para(66(a,1),48(a,1,1)),flip(a)]. given #768 (F,wt=11): 6481 x + (y + (z + (u + v))) != v # answer(Winker1b). [para(7(a,1),142(a,1,2,2))]. given #769 (F,wt=11): 7283 (x + (y + (z + u)))'' != z # answer(Winker2a). [para(7(a,1),147(a,1,1,1))]. given #770 (F,wt=11): 7291 x + (y + (z + (u + v))) != u # answer(Winker1a). [para(7(a,1),282(a,1,2))]. given #771 (F,wt=11): 8006 (x + (y + (z + u)))'' != u # answer(Winker2a). [para(7(a,1),285(a,1,1,1,2))]. given #772 (T,wt=21): 449 (x + (g(x) + (x + (g(x) + h(x))'')'')')' = g(x). [para(77(a,1),23(a,1,1,2,1,1)),rewrite([77(19)])]. given #773 (T,wt=21): 630 ((x + (x + (x + (g(x) + y))))' + (y + h(x)')')' = y. [para(32(a,1),20(a,1,1,1,1))]. given #774 (T,wt=21): 637 ((x + (x + (x + (g(x) + y))))' + (h(x)' + y)')' = y. [para(32(a,1),111(a,1,1,1,1))]. given #775 (T,wt=21): 639 ((x + h(y)')' + (y + (y + (y + (g(y) + x))))')' = x. [para(32(a,1),112(a,1,1,2,1))]. given #776 (A,wt=36): 188 (g(x + (x + (x + g(x)))') + (x + (g(x)' + (x + (x + g(x)))'))')' = x + (x + (x + g(x)))'. [para(66(a,1),27(a,1,1,2,1,2,1)),rewrite([6(14),19(14)])]. given #777 (F,wt=7): 28307 h(x)'' != g(x) # answer(Winker2a). [para(12(a,1),8006(a,1,1,1))]. given #778 (F,wt=11): 8102 g(x + (y + (z + u))) != z' # answer(Winker2a). [para(7(a,1),499(a,1,1))]. given #779 (F,wt=11): 9225 g(x + (y + (z + u)))' != z # answer(Winker2a). [para(7(a,1),535(a,1,1,1))]. given #780 (F,wt=11): 9232 g(x + (y + (z + u))) != u' # answer(Winker2a). [para(7(a,1),763(a,1,1,2))]. given #781 (T,wt=21): 664 (g(x) + (x + ((x' + y)' + (x' + y')'))')' = x. [para(10(a,1),24(a,1,1,1))]. given #782 (T,wt=21): 671 ((x + y)' + ((y + z)' + (x + (y + z')'))')' = x. [para(19(a,1),24(a,1,1,2,1))]. given #783 (T,wt=21): 817 ((x + (x + (g(x) + (y + x))))' + (y + h(x)')')' = y. [para(34(a,1),8(a,1,1,1,1))]. given #784 (T,wt=21): 818 ((x + h(y))' + (y + (y + (g(y) + (x + y)))')')' = y. [para(34(a,2),8(a,1,1,1,1))]. given #785 (A,wt=23): 189 (g(x) + (x' + (x + (x + g(x)))')')' = (x + (x + g(x)))'. [para(66(a,1),20(a,1,1,1)),rewrite([6(7)])]. given #786 (F,wt=7): 28354 g(x)' != g(h(x)) # answer(Winker2a). [para(12(a,1),9232(a,1,1)),flip(a)]. given #787 (F,wt=11): 9326 g(x + (y + (z + u)))' != u # answer(Winker2a). [para(7(a,1),788(a,1,1,1,2))]. given #788 (F,wt=7): 28415 g(h(x))' != g(x) # answer(Winker2a). [para(12(a,1),9326(a,1,1,1))]. given #789 (F,wt=11): 9344 x + (y + (z + u)) != u + x # answer(Winker1a). [para(7(a,1),1377(a,1,2))]. given #790 (T,wt=21): 839 ((x + (x + (g(x) + (y + x))))' + (h(x)' + y)')' = y. [para(34(a,1),21(a,1,1,1,1))]. given #791 (T,wt=21): 853 ((h(x)' + y)' + (x + (x + (g(x) + (y + x))))')' = y. [para(34(a,1),148(a,1,1,2,1))]. given #792 (T,wt=21): 884 ((x + h(y))' + (y + (x + (y + (y + g(y))))')')' = y. [para(52(a,1),8(a,1,1,1,1))]. given #793 (T,wt=21): 995 (x + (x + (h(x)' + (x + (x + g(x)))'))')' = h(x)'. [para(12(a,1),25(a,1,1,2,1,2,2,1)),rewrite([6(7),12(15)])]. given #794 (A,wt=29): 192 (g(x') + (x + (x' + (x' + g(x')))')')' = (x' + (x' + g(x')))'. [para(66(a,1),21(a,1,1,2)),rewrite([6(8),6(12)])]. given #795 (F,wt=11): 10006 x + (y + (z + u)) != z + x # answer(Winker1a). [para(19(a,1),1378(a,1,2))]. given #796 (F,wt=11): 10801 h(x + (y + (z + h(u)))) != u # answer(Winker1a). [para(7(a,1),2254(a,1,1,2))]. given #797 (F,wt=11): 10811 h(h(x + (y + (z + u)))) != z # answer(Winker1a). [para(7(a,1),2550(a,1,1,1))]. given #798 (F,wt=11): 10818 h(h(x + (y + (z + u)))) != u # answer(Winker1a). [para(7(a,1),2557(a,1,1,1,2))]. given #799 (T,wt=21): 1030 (g(x) + (g(x) + (x' + (x' + x')''))')' = x'. [para(121(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),121(20)])]. given #800 (T,wt=21): 1047 (x + (x + (g(x) + (g(x) + h(x)'')''))')' = g(x). [para(75(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),75(21)])]. given #801 (T,wt=21): 1049 (g(x) + (x + (g(x) + (x + (g(x) + h(x)))''))')' = x. [para(103(a,1),25(a,1,1,2,1,2,2)),rewrite([6(9),19(10),103(21)])]. given #802 (T,wt=21): 1168 (x'' + (g(x') + (x + x'')'')')' = g(x'). [para(157(a,1),8(a,1,1,1))]. given #803 (A,wt=25): 198 (x + ((y + x)' + (y' + x)'))' = g((y + x)' + (y' + x)'). [para(111(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #804 (F,wt=7): 28462 h(h(h(x))) != g(x) # answer(Winker1a). [para(12(a,1),10818(a,1,1,1))]. given #805 (F,wt=11): 10836 h(x + (y + h(z)))' != z' # answer(Winker2a). [para(7(a,1),2595(a,1,1,1))]. given #806 (F,wt=11): 11385 h(h(x + (y + z)))' != y' # answer(Winker2a). [para(19(a,1),2612(a,1,1,1,1))]. given #807 (F,wt=11): 11482 h(h(h(x + x')))' != g(x) # answer(Winker2a). [para(10(a,1),11384(a,2))]. given #808 (T,wt=21): 1171 (g(x) + (x' + ((x + y)' + (x + y')'))')' = x'. [para(8(a,1),157(a,1,1,1,1)),rewrite([8(14),6(9),8(19)])]. given #809 (T,wt=21): 1186 (g(x) + (x' + ((y + x)' + (x + y')'))')' = x'. [para(20(a,1),157(a,1,1,1,1)),rewrite([20(14),6(9),20(19)])]. given #810 (T,wt=21): 1188 (g(x) + (x' + ((x + y)' + (y' + x)'))')' = x'. [para(21(a,1),157(a,1,1,1,1)),rewrite([21(14),6(9),21(19)])]. given #811 (T,wt=21): 1191 (g(x) + (x' + ((y + x)' + (y' + x)'))')' = x'. [para(111(a,1),157(a,1,1,1,1)),rewrite([111(14),6(9),111(19)])]. given #812 (A,wt=15): 200 ((x + y)' + ((x' + y)' + z))' != y # answer(Winker2a). [para(111(a,1),16(a,2)),rewrite([7(7)])]. given #813 (F,wt=11): 11572 h(x + (y + h(z)))'' != z # answer(Winker2a). [para(7(a,1),3185(a,1,1,1,1))]. given #814 (F,wt=11): 11583 h(h(x + (y + z)))'' != y # answer(Winker2a). [para(19(a,1),3188(a,1,1,1,1,1))]. given #815 (F,wt=11): 12205 (g(x) + h((x + x)'))' != x # answer(Winker2a). [para(12(a,1),69(a,1,1,2))]. given #816 (F,wt=11): 12220 x + h(y + (z + h(u))) != u # answer(Winker1a). [para(7(a,1),3197(a,1,2,1))]. given #817 (T,wt=21): 1193 (g(x) + (x' + ((x + y')' + (y + x)'))')' = x'. [para(112(a,1),157(a,1,1,1,1)),rewrite([112(14),6(9),112(19)])]. given #818 (T,wt=21): 1200 (g(x) + (x' + ((y' + x)' + (x + y)'))')' = x'. [para(148(a,1),157(a,1,1,1,1)),rewrite([148(14),6(9),148(19)])]. given #819 (T,wt=21): 1249 ((x + x)' + g(g(g(x) + h(x)') + (x + x)'))' = x. [para(313(a,1),121(a,1,1,2,1,1)),rewrite([313(18),6(12),313(22)])]. given #820 (T,wt=21): 1275 ((x + h(y))' + (y + (y + (y + (g(y) + x)))')')' = y. [para(620(a,2),8(a,1,1,1,1))]. given #821 (A,wt=15): 201 (x + ((y + z)' + (y' + z)'))' != z # answer(Winker2b). [para(111(a,1),17(a,2))]. given #822 (F,wt=11): 12221 x + (y + h(z + h(u))) != u # answer(Winker1a). [para(7(a,1),3197(a,1))]. given #823 (F,wt=11): 12232 x + (y + h(h(z + u))) != z # answer(Winker1a). [para(7(a,1),3200(a,1))]. given #824 (F,wt=11): 12234 x + h(h(y + (z + u))) != z # answer(Winker1a). [para(19(a,1),3200(a,1,2,1,1))]. given #825 (F,wt=11): 12947 x + (y + (z + h(h(u)))) != u # answer(Winker1a). [para(7(a,1),3645(a,1,2))]. given #826 (T,wt=21): 1411 ((x + h(y))' + (y + (y + (x + (y + g(y))))')')' = y. [para(830(a,1),8(a,1,1,1,1))]. given #827 (T,wt=21): 1439 ((x + (x + (x + (y + g(x)))))' + (y + h(x)')')' = y. [para(1270(a,1),8(a,1,1,1,1))]. given #828 (T,wt=21): 1440 ((x + h(y))' + (y + (y + (y + (x + g(y))))')')' = y. [para(1270(a,2),8(a,1,1,1,1))]. given #829 (T,wt=21): 1455 ((x + (x + (x + (y + g(x)))))' + (h(x)' + y)')' = y. [para(1270(a,1),21(a,1,1,1,1))]. given #830 (A,wt=13): 204 g((x + y)' + (x' + y)') != y # answer(Winker2a). [para(111(a,1),43(a,1)),flip(a)]. given #831 (F,wt=11): 12956 g(h(x + (y + h(z)))) != z' # answer(Winker2a). [para(7(a,1),3674(a,1,1,1))]. given #832 (F,wt=11): 13061 g(h(h(x + (y + z)))) != y' # answer(Winker2a). [para(19(a,1),3691(a,1,1,1,1))]. given #833 (F,wt=11): 13582 g(h(h(h(x + x')))) != g(x) # answer(Winker2a). [para(10(a,1),13060(a,1)),flip(a)]. given #834 (F,wt=11): 13683 g(h(x + (y + h(z))))' != z # answer(Winker2a). [para(7(a,1),3757(a,1,1,1,1))]. given #835 (T,wt=21): 1470 ((h(x)' + y)' + (x + (x + (x + (y + g(x)))))')' = y. [para(1270(a,1),148(a,1,1,2,1))]. given #836 (T,wt=21): 2095 (g(x) + (x' + (g(x) + (x' + x'))'')')' = x'. [para(303(a,1),8(a,1,1,1))]. given #837 (T,wt=21): 2172 x + (y + (x + (y + (x + (y + g(y + x)))))) = h(x + y). [para(6(a,1),33(a,1,2,2,2,2,2,2,1))]. given #838 (T,wt=21): 2180 x + (y + (y + (x + (y + (x + g(y + x)))))) = h(y + x). [para(33(a,1),19(a,1)),flip(a)]. given #839 (A,wt=14): 205 h((x + y)' + (x' + y)')' != y # answer(Winker2a). [para(111(a,1),45(a,2))]. given #840 (F,wt=10): 28600 h(x + y)'' != y + x # answer(Winker2a). [para(2180(a,1),146(a,1,1,1))]. given #841 (F,wt=10): 28602 x + h(y + z) != z + y # answer(Winker1a). [para(2180(a,1),281(a,1,2))]. given #842 (F,wt=10): 28604 (x + y)' != g(h(y + x)) # answer(Winker2a). [para(2180(a,1),495(a,1,1)),flip(a)]. given #843 (F,wt=10): 28607 g(h(x + y))' != y + x # answer(Winker2a). [para(2180(a,1),533(a,1,1,1))]. given #844 (T,wt=21): 2182 x + (y + (x + (y + (y + (x + g(x + y)))))) = h(x + y). [para(19(a,1),33(a,1,2,2,2,2))]. given #845 (T,wt=21): 2183 x + (y + (x + (x + (y + (y + g(x + y)))))) = h(x + y). [para(19(a,1),33(a,1,2,2,2))]. given #846 (T,wt=21): 2184 x + (y + (y + (x + (x + (y + g(x + y)))))) = h(x + y). [para(19(a,1),33(a,1,2,2))]. given #847 (T,wt=21): 2185 x + (x + (y + (y + (x + (y + g(x + y)))))) = h(x + y). [para(19(a,1),33(a,1,2))]. given #848 (A,wt=14): 206 g((x + y)' + (x' + y)') != y' # answer(Winker2b). [para(111(a,1),48(a,1,1)),flip(a)]. given #849 (F,wt=10): 28614 h(h(h(x + y))) != y + x # answer(Winker1a). [para(2180(a,1),2548(a,1,1,1))]. given #850 (F,wt=10): 28659 h(x + y)' != (x + x)' # answer(Winker2a). [para(2185(a,1),40(a,1,1))]. given #851 (F,wt=9): 28669 (x + x)' != h(h(x))' # answer(Winker2a). [para(12(a,1),28659(a,1,1,1)),flip(a)]. given #852 (F,wt=10): 28660 h(x + y)'' != x + x # answer(Winker2a). [para(2185(a,1),146(a,1,1,1))]. given #853 (T,wt=21): 2472 (x + (g(x) + (x + (g(x) + h(x)''))'')')' = g(x). [para(538(a,1),8(a,1,1,1))]. given #854 (T,wt=21): 3205 ((x + (y + (z + u)))' + (z + (x + (y + u))')')' = z. [para(7(a,1),51(a,1,1,1,1)),rewrite([7(6)])]. given #855 (T,wt=21): 3207 ((x + (y + (z + u)))' + (y + (z + (x + u))')')' = y. [para(19(a,1),51(a,1,1,2,1,2,1))]. given #856 (T,wt=21): 3218 ((x + y)' + ((z + y)' + (x + (y + z')'))')' = x. [para(20(a,1),51(a,1,1,2,1,2)),rewrite([6(11)])]. given #857 (A,wt=38): 209 (g((x + y)' + (x' + y)') + (y' + ((x + y)' + (x' + y)'))')' = (x + y)' + (x' + y)'. [para(111(a,1),27(a,1,1,2,1,2,1)),rewrite([6(15)])]. given #858 (F,wt=9): 28680 h(h(x))'' != x + x # answer(Winker2a). [para(12(a,1),28660(a,1,1,1,1))]. given #859 (F,wt=10): 28661 x + h(y + z) != y + y # answer(Winker1a). [para(2185(a,1),281(a,1,2))]. given #860 (F,wt=9): 28770 x + h(h(y)) != y + y # answer(Winker1a). [para(12(a,1),28661(a,1,2,1))]. given #861 (F,wt=10): 28662 g(h(x + y)) != (x + x)' # answer(Winker2a). [para(2185(a,1),495(a,1,1))]. Low Water (displace, False_semantics): id=28096, wt=17 given #862 (T,wt=21): 3221 ((x + y)' + ((y + z)' + (x + (z' + y)'))')' = x. [para(21(a,1),51(a,1,1,2,1,2)),rewrite([6(11)])]. given #863 (T,wt=21): 3222 ((x + g(y))' + (y + (x + (y + (y + g(y)))'))')' = x. [para(66(a,1),51(a,1,1,2,1,2)),rewrite([6(11)])]. given #864 (T,wt=21): 3224 ((x + y)' + ((z + y)' + (x + (z' + y)'))')' = x. [para(111(a,1),51(a,1,1,2,1,2)),rewrite([6(11)])]. given #865 (T,wt=21): 3226 ((x + y)' + ((y + z')' + (x + (z + y)'))')' = x. [para(112(a,1),51(a,1,1,2,1,2)),rewrite([6(11)])]. given #866 (A,wt=25): 224 (x + ((x + y')' + (y + x)'))' = g((x + y')' + (y + x)'). [para(112(a,1),10(a,1,1,2)),rewrite([6(7)])]. given #867 (F,wt=9): 28783 (x + x)' != g(h(h(x))) # answer(Winker2a). [para(12(a,1),28662(a,1,1,1)),flip(a)]. given #868 (F,wt=10): 28663 g(h(x + y))' != x + x # answer(Winker2a). [para(2185(a,1),533(a,1,1,1))]. given #869 (F,wt=9): 28809 g(h(h(x)))' != x + x # answer(Winker2a). [para(12(a,1),28663(a,1,1,1,1))]. given #870 (F,wt=10): 28667 h(x + y)' != (y + y)' # answer(Winker2a). [para(6(a,1),28659(a,1,1,1))]. given #871 (T,wt=21): 3231 ((x + y')' + (g(y) + (x + (y' + y')'))')' = x. [para(121(a,1),51(a,1,1,2,1,2)),rewrite([6(12)])]. given #872 (T,wt=21): 3233 ((x + y)' + ((z' + y)' + (x + (y + z)'))')' = x. [para(148(a,1),51(a,1,1,2,1,2)),rewrite([6(11)])]. given #873 (T,wt=21): 3762 ((x + (y + (z + u)))' + (u + (x + (y + z))')')' = u. [para(7(a,1),113(a,1,1,1,1,2))]. given #874 (T,wt=18): 28829 (h(x)' + (g(x) + (x + (x + x))')')' = g(x). [para(12(a,1),3762(a,1,1,1,1))]. given #875 (A,wt=15): 226 ((x + y')' + ((y + x)' + z))' != x # answer(Winker2a). [para(112(a,1),16(a,2)),rewrite([7(7)])]. given #876 (F,wt=10): 28678 h(x + y)'' != y + y # answer(Winker2a). [para(6(a,1),28660(a,1,1,1,1))]. given #877 (F,wt=10): 28767 x + h(y + z) != z + z # answer(Winker1a). [para(6(a,1),28661(a,1,2,1))]. given #878 (F,wt=10): 28781 g(h(x + y)) != (y + y)' # answer(Winker2a). [para(6(a,1),28662(a,1,1,1))]. given #879 (F,wt=10): 28807 g(h(x + y))' != y + y # answer(Winker2a). [para(6(a,1),28663(a,1,1,1,1))]. given #880 (T,wt=21): 3773 ((x + (y + (z + u)))' + (u + (y + (x + z))')')' = u. [para(19(a,1),113(a,1,1,2,1,2,1)),rewrite([7(2)])]. given #881 (T,wt=21): 3796 (g(x + y) + ((y + x)' + (x + y)')')' = (y + x)'. [para(363(a,1),113(a,1,1,1))]. given #882 (T,wt=21): 3864 ((x + x)' + (x + (g(x)' + (x + x)')'')')' = x. [para(131(a,1),8(a,1,1,1))]. given #883 (T,wt=21): 4032 ((x + (y + (z + u)))' + ((x + (y + u))' + z)')' = z. [para(7(a,1),161(a,1,1,1,1)),rewrite([7(6)])]. given #884 (A,wt=15): 227 (x + ((y + z')' + (z + y)'))' != y # answer(Winker2b). [para(112(a,1),17(a,2))]. given #885 (F,wt=11): 13694 g(h(h(x + (y + z))))' != y # answer(Winker2a). [para(19(a,1),3760(a,1,1,1,1,1))]. given #886 (F,wt=11): 14175 h(x + (y + h(z + u))) != z # answer(Winker1a). [para(7(a,1),4335(a,1,1))]. given #887 (F,wt=11): 14177 h(x + h(y + (z + u))) != z # answer(Winker1a). [para(19(a,1),4335(a,1,1,2,1))]. given #888 (F,wt=11): 14193 h(h(h(x + (y + h(z))))) != z # answer(Winker1a). [para(7(a,1),4801(a,1,1,1,1))]. given #889 (T,wt=21): 4036 ((x + y)' + ((x + z)' + (y + (x + z')'))')' = y. [para(8(a,1),161(a,1,1,2,1,1)),rewrite([6(11)])]. given #890 (T,wt=21): 4041 ((x + (y + (z + u)))' + ((z + (x + u))' + y)')' = y. [para(19(a,1),161(a,1,1,2,1,1,1))]. given #891 (T,wt=21): 4054 ((x + y)' + ((z + x)' + (y + (x + z')'))')' = y. [para(20(a,1),161(a,1,1,2,1,1)),rewrite([6(11)])]. given #892 (T,wt=21): 4057 ((x + y)' + ((x + z)' + (y + (z' + x)'))')' = y. [para(21(a,1),161(a,1,1,2,1,1)),rewrite([6(11)])]. given #893 (A,wt=13): 229 g((x + y')' + (y + x)') != x # answer(Winker2a). [para(112(a,1),43(a,1)),flip(a)]. given #894 (F,wt=11): 14204 h(h(h(h(x + (y + z))))) != y # answer(Winker1a). [para(19(a,1),4804(a,1,1,1,1,1))]. given #895 (F,wt=11): 14572 x + (y + (z + u)) != u + z # answer(Winker1b). [para(7(a,1),5720(a,1))]. given #896 (F,wt=11): 14586 x + g(x) != y + (z + h(x)) # answer(Winker1b). [para(7(a,1),6483(a,1)),flip(a)]. given #897 (F,wt=11): 14941 x + (y + (z + h(u))) != g(u) # answer(Winker1a). [para(7(a,1),7297(a,1,2))]. given #898 (T,wt=21): 4058 ((x + (y + (x + (x + g(x)))'))' + (g(x) + y)')' = y. [para(66(a,1),161(a,1,1,2,1,1))]. given #899 (T,wt=21): 4061 ((x + y)' + ((z + x)' + (y + (z' + x)'))')' = y. [para(111(a,1),161(a,1,1,2,1,1)),rewrite([6(11)])]. given #900 (T,wt=21): 4063 ((x + y)' + ((x + z')' + (y + (z + x)'))')' = y. [para(112(a,1),161(a,1,1,2,1,1)),rewrite([6(11)])]. given #901 (T,wt=21): 4068 ((g(x) + (y + (x' + x')'))' + (x' + y)')' = y. [para(121(a,1),161(a,1,1,2,1,1))]. given #902 (A,wt=14): 230 h((x + y')' + (y + x)')' != x # answer(Winker2a). [para(112(a,1),45(a,2))]. given #903 (F,wt=11): 15279 h(h(x + (y + z)))' != z' # answer(Winker2a). [para(7(a,1),11380(a,1,1,1,1))]. given #904 (F,wt=11): 15407 h(h(x + (y + z)))'' != z # answer(Winker2a). [para(7(a,1),11580(a,1,1,1,1,1))]. given #905 (F,wt=11): 15728 x + h(h(y + (z + u))) != u # answer(Winker1a). [para(7(a,1),12230(a,1,2,1,1))]. given #906 (F,wt=11): 15729 x + (y + h(h(z + u))) != u # answer(Winker1a). [para(7(a,1),12230(a,1))]. given #907 (T,wt=21): 4070 ((x + y)' + ((z' + x)' + (y + (x + z)'))')' = y. [para(148(a,1),161(a,1,1,2,1,1)),rewrite([6(11)])]. given #908 (T,wt=21): 4545 ((x + (y + (z + u)))' + ((x + (y + z))' + u)')' = u. [para(7(a,1),193(a,1,1,1,1,2))]. given #909 (T,wt=21): 4553 ((x + (y + (z + u)))' + ((y + (x + z))' + u)')' = u. [para(19(a,1),193(a,1,1,2,1,1,1)),rewrite([7(2)])]. Low Water (displace, True_semantics): id=24121, wt=30 given #910 (T,wt=21): 4575 (g(x + y) + ((x + y)' + (y + x)')')' = (y + x)'. [para(363(a,1),193(a,1,1,1))]. given #911 (A,wt=14): 231 g((x + y')' + (y + x)') != x' # answer(Winker2b). [para(112(a,1),48(a,1,1)),flip(a)]. given #912 (F,wt=11): 15741 g(h(h(x + (y + z)))) != z' # answer(Winker2a). [para(7(a,1),13056(a,1,1,1,1))]. given #913 (F,wt=11): 15872 g(h(h(x + (y + z))))' != z # answer(Winker2a). [para(7(a,1),13691(a,1,1,1,1,1))]. given #914 (F,wt=11): 15882 h(x + h(y + (z + u))) != u # answer(Winker1a). [para(7(a,1),14173(a,1,1,2,1))]. given #915 (F,wt=11): 15883 h(x + (y + h(z + u))) != u # answer(Winker1a). [para(7(a,1),14173(a,1,1))]. given #916 (T,wt=21): 4873 ((x + (y + (z + u))')' + (y + (z + (u + x)))')' = x. [para(7(a,1),221(a,1,1,1,1,2,1)),rewrite([7(8)])]. given #917 (T,wt=21): 4878 ((x + (y + (z + u))')' + (z + (y + (u + x)))')' = x. [para(19(a,1),221(a,1,1,1,1,2,1)),rewrite([7(7)])]. given #918 (T,wt=21): 5036 (((x + (y + z))' + u)' + (x + (y + (u + z)))')' = u. [para(7(a,1),339(a,1,1,1,1,1,1)),rewrite([7(8)])]. given #919 (T,wt=21): 5041 (((x + (y + z))' + u)' + (y + (u + (x + z)))')' = u. [para(19(a,1),339(a,1,1,1,1,1,1))]. given #920 (A,wt=38): 234 (g((x + y')' + (y + x)') + (x' + ((x + y')' + (y + x)'))')' = (x + y')' + (y + x)'. [para(112(a,1),27(a,1,1,2,1,2,1)),rewrite([6(15)])]. given #921 (F,wt=11): 16776 h(h(h(h(x + (y + z))))) != z # answer(Winker1a). [para(7(a,1),14201(a,1,1,1,1,1))]. given #922 (F,wt=11): 17535 g(x + (y + h(x'))) != g(x) # answer(Winker2a). [para(34(a,2),497(a,1,1,2))]. given #923 (F,wt=11): 17539 g(x + h(x' + y)) != g(x) # answer(Winker2a). [para(33(a,1),497(a,1,1,2))]. given #924 (F,wt=10): 29105 g(x + h(h(x'))) != g(x) # answer(Winker2a). [para(12(a,1),17539(a,1,1,2,1))]. given #925 (T,wt=21): 5050 ((g(x) + y)' + (x + (y + (x + (x + g(x)))'))')' = y. [para(66(a,1),339(a,1,1,1,1,1))]. given #926 (T,wt=21): 5056 ((x' + y)' + (g(x) + (y + (x' + x')'))')' = y. [para(121(a,1),339(a,1,1,1,1,1))]. given #927 (T,wt=21): 5315 (g(h(x)) + (x + (x + (x + (g(x) + h(x)')))')')' = x. [para(368(a,1),8(a,1,1,1))]. given #928 (T,wt=21): 5322 (g(h(x)) + (x + (x + g(g(x) + h(x)')))')' = x + x. [para(368(a,1),22(a,1,1,1)),rewrite([78(8)])]. given #929 (A,wt=25): 247 ((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 #930 (F,wt=11): 18590 (x + (y + z))'' != z + x # answer(Winker2a). [para(245(a,1),16(a,1)),flip(a)]. given #931 (F,wt=11): 19067 (x + (y + z))'' != y + x # answer(Winker2a). [para(260(a,1),16(a,1)),flip(a)]. given #932 (F,wt=11): 19825 x + h(y + h(z)) != x + z # answer(Winker1a). [para(34(a,2),2218(a,1,2,1))]. given #933 (F,wt=11): 19833 x + h(h(y + z)) != x + y # answer(Winker1a). [para(33(a,1),2218(a,1,2,1))]. given #934 (T,wt=21): 5455 g(x + (y + h(z))) = g(z + (z + (g(z) + (x + (y + z))))). [para(7(a,1),856(a,1,1)),rewrite([7(7)])]. given #935 (T,wt=21): 5606 (x + (y + h(z)))' = (z + (z + (g(z) + (x + (y + z)))))'. [para(7(a,1),860(a,1,1)),rewrite([7(7)])]. given #936 (T,wt=21): 6043 (x + (x + (g(x)' + (h(x)' + h(x)')))')' = h(x)'. [para(1131(a,1),8(a,1,1,2)),rewrite([19(9),19(8),6(11)])]. given #937 (T,wt=21): 6506 g(x + (y + h(z))) = g(z + (z + (z + (g(z) + (x + y))))). [para(7(a,1),1291(a,1,1))]. given #938 (A,wt=28): 248 (x + (y + ((x + (y + z))' + (x + (y + z'))'')'))' = (x + (y + z))'. [para(22(a,1),8(a,1,1,1)),rewrite([7(12)])]. given #939 (F,wt=10): 29146 x + h(h(h(y))) != x + y # answer(Winker1a). [para(12(a,1),19833(a,1,2,1,1))]. given #940 (F,wt=10): 29210 x + h(h(h(y))) != y + x # answer(Winker1a). [para(6(a,1),29146(a,2))]. given #941 (F,wt=11): 20359 h(x + (y + h(z))) != x + z # answer(Winker1a). [para(34(a,2),2234(a,1,1,2))]. given #942 (F,wt=11): 20369 h(x + h(y + z)) != x + y # answer(Winker1a). [para(33(a,1),2234(a,1,1,2))]. given #943 (T,wt=21): 6509 g(x + (y + h(z))) = g(z + (z + (z + (x + (g(z) + y))))). [para(19(a,1),1291(a,2,1,2,2,2)),rewrite([7(3)])]. given #944 (T,wt=21): 6551 g(x + (y + h(x))) = g(x + (x + (x + (g(x) + (y + x))))). [para(34(a,2),1291(a,2,1,2)),rewrite([6(3),32(3)]),flip(a)]. given #945 (T,wt=21): 6678 (x + (y + h(z)))' = (z + (z + (z + (g(z) + (x + y)))))'. [para(7(a,1),1293(a,1,1))]. given #946 (T,wt=21): 6684 (x + (y + h(z)))' = (z + (z + (z + (x + (g(z) + y)))))'. [para(19(a,1),1293(a,2,1,2,2,2)),rewrite([7(3)])]. given #947 (A,wt=27): 249 ((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 #948 (F,wt=10): 29222 h(x + h(h(y))) != x + y # answer(Winker1a). [para(12(a,1),20369(a,1,1,2,1))]. given #949 (F,wt=10): 29252 h(x + h(h(y))) != y + x # answer(Winker1a). [para(6(a,1),29222(a,2))]. given #950 (F,wt=11): 20385 h(x + (y + h(z))) != z + z # answer(Winker1a). [para(7(a,1),20360(a,1,1))]. given #951 (F,wt=11): 20502 g(x + x')' != x + g(x) # answer(Winker2a). [para(418(a,1),16(a,1)),flip(a)]. given #952 (T,wt=21): 6804 g(x + (y + h(z))) = g(z + (z + (z + (x + (y + g(z)))))). [para(7(a,1),1473(a,1,1)),rewrite([7(7)])]. given #953 (T,wt=21): 6975 (x + (y + h(z)))' = (z + (z + (z + (x + (y + g(z))))))'. [para(7(a,1),1477(a,1,1)),rewrite([7(7)])]. given #954 (T,wt=21): 7305 h(x + (y + h(z))) = h(z + (z + (g(z) + (x + (y + z))))). [para(7(a,1),2209(a,1,1)),rewrite([7(7)])]. given #955 (T,wt=21): 7444 h(x + (y + h(z))) = h(z + (z + (z + (g(z) + (x + y))))). [para(7(a,1),2215(a,1,1))]. given #956 (A,wt=26): 250 (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 #957 (F,wt=11): 21038 (x + (y + h(z)))' != g(z)' # answer(Winker2a). [para(816(a,1),55(a,1,1))]. given #958 (F,wt=11): 21048 (x + (y + h(z)))'' != g(z) # answer(Winker2a). [para(816(a,1),147(a,1,1,1))]. given #959 (F,wt=11): 21059 g(x + (y + h(z))) != g(z)' # answer(Winker2a). [para(816(a,1),499(a,1,1))]. given #960 (F,wt=11): 21068 g(x + (y + h(z)))' != g(z) # answer(Winker2a). [para(816(a,1),535(a,1,1,1))]. given #961 (T,wt=21): 7446 h(x + (y + h(z))) = h(z + (z + (z + (x + (g(z) + y))))). [para(19(a,1),2215(a,2,1,2,2,2)),rewrite([7(3)])]. given #962 (T,wt=21): 7468 h(x + (y + h(x))) = h(x + (x + (x + (g(x) + (y + x))))). [para(34(a,2),2215(a,2,1,2)),rewrite([6(3),32(3)]),flip(a)]. given #963 (T,wt=21): 7584 h(x + (y + h(z))) = h(z + (z + (z + (x + (y + g(z)))))). [para(7(a,1),2223(a,1,1)),rewrite([7(7)])]. given #964 (T,wt=21): 7722 ((x + (y + (z + u)))' + (x + (u + (y + z))')')' = x. [para(7(a,1),3201(a,1,1,1,1,2))]. given #965 (A,wt=27): 251 ((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 #966 (F,wt=11): 21086 h(h(x + (y + h(z)))) != g(z) # answer(Winker1a). [para(816(a,1),2550(a,1,1,1))]. given #967 (F,wt=11): 21185 (x + (y + h(y')))' != g(y) # answer(Winker2a). [para(827(a,2),44(a,1,1))]. given #968 (F,wt=11): 21268 g(x + (y + h(y'))) != g(y) # answer(Winker2a). [para(827(a,2),497(a,1,1))]. given #969 (F,wt=11): 21292 h(x + (y + h(z))) != y + z # answer(Winker1a). [para(827(a,2),2234(a,1,1))]. given #970 (T,wt=19): 29305 ((x + h(y + z))' + (x + h(z + y)')')' = x. [para(2182(a,1),7722(a,1,1,2,1,2,1)),rewrite([6(7),28560(8)])]. given #971 (T,wt=19): 29313 ((x + h(y + z))' + (h(z + y)' + x)')' = x. [para(6(a,1),29305(a,1,1,2,1))]. given #972 (T,wt=19): 29340 ((h(x + y)' + z)' + (z + h(y + x))')' = z. [para(6(a,1),29313(a,1,1))]. given #973 (T,wt=21): 7724 ((x + (y + (z + u)))' + (x + (z + (u + y))')')' = x. [para(7(a,1),3201(a,1,1,2,1,2,1))]. given #974 (A,wt=35): 252 (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 #975 (F,wt=11): 21332 h(x + h(y + z))' != y' # answer(Winker2a). [para(33(a,1),2573(a,1,1,1,2))]. given #976 (F,wt=10): 29403 h(x + h(h(y)))' != y' # answer(Winker2a). [para(12(a,1),21332(a,1,1,1,2,1))]. given #977 (F,wt=11): 21379 (x' + (y + h(x)))' != g(x) # answer(Winker2a). [para(828(a,2),44(a,1,1))]. given #978 (F,wt=11): 21446 g(x' + (y + h(x))) != g(x) # answer(Winker2a). [para(828(a,2),497(a,1,1))]. given #979 (T,wt=21): 7732 ((x + (y + (z + u)))' + (x + (y + (u + z))')')' = x. [para(19(a,1),3201(a,1,1,1,1,2)),rewrite([7(6)])]. given #980 (T,wt=21): 8257 ((x + (y + (z + u)))' + (z + (u + (x + y))')')' = z. [para(7(a,1),3202(a,1,1,1,1))]. given #981 (T,wt=21): 8258 ((x + (y + (z + u)))' + (y + (z + (u + x))')')' = y. [para(7(a,1),3202(a,1,1,2,1,2,1))]. given #982 (T,wt=21): 8262 ((x + y)' + ((y + z')' + (x + (y + z)'))')' = x. [para(8(a,1),3202(a,1,1,2,1,2)),rewrite([6(11)])]. given #983 (A,wt=22): 253 ((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 #984 (F,wt=11): 21467 h(x + (y + h(z))) != z + x # answer(Winker1a). [para(828(a,2),2234(a,1,1))]. given #985 (F,wt=11): 21533 h(x + h(y + z))'' != y # answer(Winker2a). [para(33(a,1),3182(a,1,1,1,1,2))]. given #986 (F,wt=10): 29462 h(x + h(h(y)))'' != y # answer(Winker2a). [para(12(a,1),21533(a,1,1,1,1,2,1))]. given #987 (F,wt=11): 21562 x + h(y + h(z + u)) != z # answer(Winker1a). [para(33(a,1),3193(a,1,2,1,2))]. given #988 (T,wt=21): 8267 ((x + (y + (z + u)))' + (z + (y + (u + x))')')' = z. [para(19(a,1),3202(a,1,1,1,1,2)),rewrite([7(6)])]. given #989 (T,wt=21): 8268 ((x + (y + (z + u)))' + (z + (x + (u + y))')')' = z. [para(19(a,1),3202(a,1,1,2,1,2,1)),rewrite([7(3)])]. given #990 (T,wt=21): 8281 (((x + (x + g(x)))' + (y + x))' + (y + g(x))')' = y. [para(66(a,1),3202(a,1,1,2,1,2))]. given #991 (T,wt=21): 8284 ((x + y)' + ((z' + y)' + (x + (z + y)'))')' = x. [para(111(a,1),3202(a,1,1,2,1,2)),rewrite([6(11)])]. given #992 (A,wt=23): 254 ((x + h(y))' + (x + (y + (y + (y + g(y)))'))')' = x + y. [para(12(a,1),22(a,1,1,1,1,2))]. given #993 (F,wt=10): 29474 x + h(y + h(h(z))) != z # answer(Winker1a). [para(12(a,1),21562(a,1,2,1,2,1))]. given #994 (F,wt=11): 21844 g(h(x + h(y + z))) != y' # answer(Winker2a). [para(33(a,1),3652(a,1,1,1,2))]. given #995 (F,wt=10): 29517 g(h(x + h(h(y)))) != y' # answer(Winker2a). [para(12(a,1),21844(a,1,1,1,2,1))]. given #996 (F,wt=11): 21860 g(h(x + h(y + z)))' != y # answer(Winker2a). [para(33(a,1),3754(a,1,1,1,1,2))]. given #997 (T,wt=21): 8290 (((x' + x')' + (y + g(x)))' + (y + x')')' = y. [para(121(a,1),3202(a,1,1,2,1,2))]. given #998 (T,wt=21): 9366 ((x + (y + (z + u))')' + (y + (z + (x + u)))')' = x. [para(7(a,1),3203(a,1,1,1,1,2,1)),rewrite([7(8)])]. given #999 (T,wt=21): 9370 ((x + (y + (z + u))')' + (z + (x + (y + u)))')' = x. [para(19(a,1),3203(a,1,1,1,1,2,1))]. given #1000 (T,wt=21): 9766 ((x + (y + (z + u)))' + (u + (y + (z + x))')')' = u. [para(7(a,1),3761(a,1,1,1,1,2)),rewrite([7(6)])]. given #1001 (A,wt=28): 256 ((x + (x + (x + (g(x) + y))))' + (x + (x + (x + (g(x) + y'))))')' = h(x). [para(12(a,1),22(a,2)),rewrite([7(4),7(3),7(11),7(10)])]. given #1002 (F,wt=10): 29533 g(h(x + h(h(y))))' != y # answer(Winker2a). [para(12(a,1),21860(a,1,1,1,1,2,1))]. given #1003 (F,wt=11): 22653 h(h(h(x + h(y + z)))) != y # answer(Winker1a). [para(33(a,1),4798(a,1,1,1,1,2))]. given #1004 (F,wt=10): 29571 h(h(h(x + h(h(y))))) != y # answer(Winker1a). [para(12(a,1),22653(a,1,1,1,1,2,1))]. given #1005 (F,wt=11): 23389 (x + h(y + h(z)))' != z' # answer(Winker2a). [para(34(a,2),5798(a,1,1,2,1))]. given #1006 (T,wt=21): 9767 ((x + (y + (z + u)))' + (u + (z + (x + y))')')' = u. [para(7(a,1),3761(a,1,1,1,1))]. given #1007 (T,wt=21): 9776 ((x + (y + (z + u)))' + (u + (x + (z + y))')')' = u. [para(19(a,1),3761(a,1,1,2,1,2,1)),rewrite([7(3)])]. given #1008 (T,wt=21): 9800 (g(x + y) + ((y + x)' + (y + x)')')' = (y + x)'. [para(363(a,1),3761(a,1,1,1))]. given #1009 (T,wt=21): 10056 ((x + (y + (z + u)))' + ((u + (y + z))' + x)')' = x. [para(7(a,1),4029(a,1,1,1,1,2))]. given #1010 (A,wt=21): 257 ((x + (y + z))' + ((x + (y + z'))' + u))' != x + y # answer(Winker2a). [para(22(a,