Prooof out3b1-19

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

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

% Proof 1 at 5.84 (+ 0.06) seconds: Winker2a.
% Length of proof is 31.
% Level of proof is 11.
% Maximum clause weight is 23.
% Given clauses 257.

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')' = 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))].
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.  [para(9(a,1),8(a,1,1,2)),rewrite([6(4)])].
27 (h(x) + (x + (x + (x + g(x)))')')' = x.  [para(10(a,1),8(a,1,1,1))].
29 ((x + (y + z))' + (y + (x + z)')')' = y.  [para(17(a,1),8(a,1,1,1,1))].
32 (x + (x + (x + g(x)))')' = g(x).  [para(26(a,1),8(a,1,1,2)),rewrite([17(3),6(2),6(5)])].
33 (g(x) + h(x))' = x.  [back_rewrite(27),rewrite([32(7),6(3)])].
34 (x + (g(x) + h(x)')')' = g(x).  [para(33(a,1),8(a,1,1,1))].
35 ((x + y)' + (x + (g(y) + h(y)))')' = x.  [para(33(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])].
38 (g(x) + (x + (g(x) + h(x)'))')' = x.  [para(34(a,1),8(a,1,1,2)),rewrite([6(8)])].
44 ((x + (y + z))' + (z + (x + y)')')' = z.  [para(7(a,1),18(a,1,1,1,1))].
97 ((x + (g(y) + h(y)))' + (y + x)')' = x.  [para(33(a,1),19(a,1,1,2,1,1))].
106 ((x + (g(y) + (y + (g(y) + h(y)'))'))' + (y + x)')' = x.  [para(38(a,1),19(a,1,1,2,1,1))].
245 (x + (x + (g(y) + (h(y) + (x + y)')))')' = (x + y)'.  [para(35(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])].
1225 (h(x) + (x + (g(x) + (x + x)'))')' = x + g(x).  [para(10(a,1),44(a,1,1,1)),rewrite([7(6)])].
1398 (x + (g(x) + (x + (g(x) + (h(x) + (x + x)')))'))' = h(x).  [para(1225(a,1),8(a,1,1,2)),rewrite([17(7),17(6),6(11),7(11)])].
5830 (x + h(x))' = g(x).  [para(1398(a,1),29(a,1,1,1)),rewrite([245(12),26(6),6(2)])].
5863 (x + (x + (g(x) + h(x)'))')' = g(x).  [para(5830(a,1),23(a,1,1,2,1,2,2)),rewrite([6(4),5830(11)])].
6069 (g(x) + (g(x) + (h(x) + (x + (g(x) + h(x)'))'))')' = (x + (g(x) + h(x)'))'.  [para(5863(a,1),97(a,1,1,2)),rewrite([6(10),7(10),6(13)])].
11711 (x + (g(x) + h(x)'))' = h(x).  [para(5830(a,1),106(a,1,1,2)),rewrite([17(10),6(13),6069(14)])].
11728 (h(x) + (h(x)' + (x + g(x))')')' = h(x)'.  [para(11711(a,1),44(a,1,1,1))].
11729 $F # answer(Winker2a).  [resolve(11728,a,11,a)].

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