Prooof out3b1-243

(x + (x + x))' = g(x).   x + (x + g(x))' = h(x). % Problem 243

============================== PROOF =================================

% Proof 1 at 42.43 (+ 0.18) seconds: Winker2a.
% Length of proof is 33.
% Level of proof is 11.
% Maximum clause weight is 27.
% Given clauses 659.

1 (exists a exists b (a + b)' = a') # answer(Winker2a) # label(non_clause) # label(goal).  [goal].
6 x + y = y + x # label(Commutativity).  [assumption].
7 (x + y) + z = x + (y + z) # label(Associativity).  [assumption].
8 ((x + y)' + (x + y')')' = x # label(Robbins).  [assumption].
9 (x + (x + x))' = g(x).  [assumption].
10 x + (x + g(x))' = h(x).  [assumption].
11 (x + y)' != x' # answer(Winker2a).  [deny(1)].
17 x + (y + z) = y + (x + z).  [para(6(a,1),7(a,1,1)),rewrite([7(2)])].
18 ((x + y)' + (y + x')')' = y.  [para(6(a,1),8(a,1,1,1,1))].
19 ((x + y)' + (y' + x)')' = x.  [para(6(a,1),8(a,1,1,2,1))].
20 ((x + (y + z))' + (x + (y + z'))')' = x + y.  [para(7(a,1),8(a,1,1,1,1)),rewrite([7(6)])].
23 (x + (x + (y' + (x + y)'))')' = (x + y)'.  [para(8(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])].
26 x + ((x + g(x))' + y) = h(x) + y.  [para(10(a,1),7(a,1,1)),flip(a)].
29 ((x + (y + z))' + (y + (x + z)')')' = y.  [para(17(a,1),8(a,1,1,1,1))].
30 x + (y + (x + g(x))') = y + h(x).  [para(10(a,1),17(a,1,2)),flip(a)].
43 ((x + (y + z))' + (z + (x + y)')')' = z.  [para(7(a,1),18(a,1,1,1,1))].
53 ((x + (y + z))' + (x + (z + y'))')' = x + z.  [para(17(a,1),18(a,1,1,1,1)),rewrite([7(6)])].
62 ((x' + y)' + (y + x)')' = y.  [para(6(a,1),19(a,1,1))].
67 ((x + ((y + z)' + (y + z')'))' + (y + x)')' = x.  [para(8(a,1),19(a,1,1,2,1,1))].
436 (x + (h(x) + g(x)')')' = (x + g(x))'.  [para(30(a,1),23(a,1,1,2,1)),rewrite([6(4)])].
479 ((x + g(x))' + (x + (h(x) + g(x)'))')' = x.  [para(436(a,1),8(a,1,1,2)),rewrite([6(10)])].
503 ((x + y)' + (y + ((x + g(x))' + (x + (h(x) + g(x)'))'))')' = y.  [para(479(a,1),62(a,1,1,1,1,1))].
548 ((h(x) + y)' + ((x + g(x))' + (x + y)')')' = (x + g(x))'.  [para(26(a,1),29(a,1,1,1,1))].
2545 (x + (y + (x + (z + (y + (x + (y + z'))')))'))' = (x + (y + z'))'.  [para(53(a,1),19(a,1,1,2)),rewrite([6(7),7(7),7(6),6(10),7(10)])].
7274 (g(x) + (x + (x + ((x + y)' + (x + y')')))')' = x + x.  [para(9(a,1),67(a,1,1,2)),rewrite([7(8),6(11)])].
21123 (g(x) + (x + (h(x) + (x + (h(x) + g(x)'))'))')' = x + x.  [para(436(a,1),7274(a,1,1,2,1,2,2,2)),rewrite([6(11),26(12)])].
21221 (x + (x + (x + (g(x) + (h(x) + (x + (h(x) + g(x)'))')))'))' = g(x).  [para(21123(a,1),8(a,1,1,2)),rewrite([17(11),6(14),7(14)])].
21328 ((x + (h(x) + g(x)'))' + (g(x) + (x + g(x))')')' = (x + g(x))'.  [para(21221(a,1),548(a,1,1,2,1,2)),rewrite([17(15),2545(16),6(11)])].
21333 (x + (h(x) + g(x)'))' = g(x).  [para(21328(a,1),8(a,1,1,2)),rewrite([6(12),7(12),6(17),503(18)]),flip(a)].
21467 (g(x) + (x + (g(x) + h(x)))')' = x + x.  [back_rewrite(21123),rewrite([21333(8),6(4)])].
21841 x + h(x) = x + x.  [para(21333(a,1),20(a,1,1,2)),rewrite([6(3),6(7),21467(8)]),flip(a)].
21849 (g(x) + (g(x)' + (x + x)')')' = g(x)'.  [para(21333(a,1),43(a,1,1,1)),rewrite([21841(5)])].
21850 $F # answer(Winker2a).  [resolve(21849,a,11,a)].

============================== end of proof ==========================