Prooof out3b2-117

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

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

% Proof 1 at 141.05 (+ 0.60) seconds: Winker2b.
% Length of proof is 30.
% Level of proof is 9.
% Maximum clause weight is 34.
% Given clauses 1148.

2 (exists a exists b (a + b)' = b') # answer(Winker2b) # label(non_clause) # label(goal).  [goal].
6 x + y = y + x # label(Commutativity).  [assumption].
7 (x + y) + z = x + (y + z) # label(Associativity).  [assumption].
8 ((x + y)' + (x + y')')' = x # label(Robbins).  [assumption].
9 (x + (x + x)')' = g(x).  [assumption].
10 x + (x + (x + g(x))') = h(x).  [assumption].
12 (x + y)' != y' # answer(Winker2b).  [deny(2)].
17 x + (y + z) = y + (x + z).  [para(6(a,1),7(a,1,1)),rewrite([7(2)])].
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)])].
22 ((x + y)' + (x + ((y + z)' + (y + z')'))')' = x.  [para(8(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])].
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 (g(x) + (x + (x + x))')' = x.  [para(9(a,1),8(a,1,1,2)),rewrite([6(5)])].
27 x + (x + ((x + g(x))' + y)) = h(x) + y.  [para(10(a,1),7(a,1,1)),rewrite([7(7)]),flip(a)].
30 ((x + (y + z))' + (y + (x + z)')')' = y.  [para(17(a,1),8(a,1,1,1,1))].
33 (x + (x + (x + (x + g(x))))')' = g(x).  [para(26(a,1),8(a,1,1,2)),rewrite([17(4),17(3),6(2),6(6)])].
84 (h(x)' + (x + (x + (x + g(x))))')' = x + x.  [para(10(a,1),20(a,1,1,2,1)),rewrite([6(8)])].
97 ((x + g(y))' + (x + (y + (y + (y + (y + g(y))))'))')' = x.  [para(33(a,1),8(a,1,1,2,1,2)),rewrite([6(12)])].
259 ((x + (y + (z + u))')' + (x + (y + (z + (y + (z + (u' + (y + (z + u))')))')))')' = x.  [para(20(a,1),22(a,1,1,2,1,2,2)),rewrite([6(12),7(12),7(11),6(15),7(15)])].
349 ((x + y)' + (x + (x + (y' + (x + y)')))')' = x.  [para(23(a,1),8(a,1,1,2)),rewrite([6(10)])].
397 (x + (x + (h(x) + (x + (x + (x + g(x))))')'))' = (x + (x + (x + g(x))))'.  [para(84(a,1),19(a,1,1,2)),rewrite([6(7),6(10),7(10)])].
428 ((x + (y + (z + u)))' + (z + (x + (y + u))')')' = z.  [para(7(a,1),30(a,1,1,1,1)),rewrite([7(6)])].
15052 ((h(x) + y)' + ((x + g(x))' + (x + (x + y))')')' = (x + g(x))'.  [para(27(a,1),428(a,1,1,1,1))].
21314 (g(x) + (x + (x + (x + (h(x) + (x + (x + (x + g(x))))')')))')' = x.  [para(33(a,1),259(a,1,1,1)),rewrite([27(12)])].
21935 (x + (h(x) + (x + (x + (x + g(x))))')')' = (x + g(x))'.  [para(97(a,1),15052(a,1,1,2)),rewrite([6(9)])].
22975 (x + (x + (x + (x + (g(x) + (h(x) + (x + (x + (x + g(x))))')'))))')' = g(x).  [para(21314(a,1),8(a,1,1,2)),rewrite([17(13),17(12),17(11),6(15)])].
23535 ((x + (x + (x + g(x))))' + (h(x) + (x + (x + (x + g(x))))')')' = x.  [para(397(a,1),349(a,1,1,1)),rewrite([21935(15),397(19),27(16)])].
23547 (h(x) + (x + (x + (x + g(x))))')' = g(x).  [para(23535(a,1),19(a,1,1,2)),rewrite([6(13),7(13),7(12),7(11),6(15),22975(16)]),flip(a)].
23786 (x + (x + (x + g(x))))' = (x + (x + g(x)))'.  [back_rewrite(397),rewrite([23547(8)]),flip(a)].
23787 $F # answer(Winker2b).  [resolve(23786,a,12,a)].

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