Prooof out3b1-242

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

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

% Proof 1 at 96.35 (+ 0.33) seconds: Winker2a.
% Length of proof is 29.
% Level of proof is 10.
% Maximum clause weight is 23.
% Given clauses 949.

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 + (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)])].
26 x + (x + ((x + g(x))' + y)) = h(x) + y.  [para(10(a,1),7(a,1,1)),rewrite([7(7)]),flip(a)].
27 x + (y + (x + (x + g(x))')) = y + h(x).  [para(10(a,1),7(a,2,2)),rewrite([17(6),7(5)])].
29 ((x + (y + z))' + (y + (x + z)')')' = y.  [para(17(a,1),8(a,1,1,1,1))].
50 ((x' + y)' + (y + x)')' = y.  [para(6(a,1),19(a,1,1))].
54 (x + (y' + (x + (x + y)'))')' = (x + y)'.  [para(19(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])].
64 (x + (y + (x + (x + y')'))')' = (x + y')'.  [para(18(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])].
146 ((h(x) + y)' + (x + (x + ((x + g(x))' + y)'))')' = x + x.  [para(26(a,1),20(a,1,1,1,1))].
149 ((x + h(y))' + (y + (x + (y + (y + g(y))'))')')' = y.  [para(27(a,1),8(a,1,1,1,1))].
475 ((x + (y + (z + u)))' + (z + (x + (y + u))')')' = z.  [para(7(a,1),29(a,1,1,1,1)),rewrite([7(6)])].
8478 ((x + g(x))' + (h(x) + g(x)')')' = x.  [para(54(a,1),149(a,1,1,2)),rewrite([6(4),6(9)])].
8533 ((x + y)' + (y + ((x + g(x))' + (h(x) + g(x)')'))')' = y.  [para(8478(a,1),50(a,1,1,1,1,1))].
15801 ((h(x) + y)' + ((x + g(x))' + (x + (x + y))')')' = (x + g(x))'.  [para(26(a,1),475(a,1,1,1,1))].
18039 (g(x) + (h(x) + (h(x) + g(x)')')')' = x + x.  [para(8478(a,1),146(a,1,1,2,1,2,2)),rewrite([9(11),6(10)])].
18062 (x + (x + (g(x) + (h(x) + (h(x) + g(x)')'))'))' = g(x).  [para(18039(a,1),8(a,1,1,2)),rewrite([6(12),7(12)])].
23483 ((h(x) + g(x)')' + (g(x) + (x + g(x))')')' = (x + g(x))'.  [para(18062(a,1),15801(a,1,1,2,1,2)),rewrite([64(13),6(10)])].
23492 (h(x) + g(x)')' = g(x).  [para(23483(a,1),8(a,1,1,2)),rewrite([6(11),7(11),6(16),8533(17)]),flip(a)].
24432 (g(x) + (g(x)' + h(x)')')' = g(x)'.  [para(23492(a,1),18(a,1,1,1))].
24433 $F # answer(Winker2a).  [resolve(24432,a,11,a)].

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