Prooof out3b1-8 (x + x')' = g(x). x + (x + (x + g(x))) = h(x). % Problem 8 ============================== PROOF ================================= % Proof 1 at 31.74 (+ 0.12) seconds: Winker2b. % Length of proof is 39. % Level of proof is 12. % Maximum clause weight is 32. % Given clauses 535. 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')' = 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)])]. 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))]. 26 (g(x) + (x + x)')' = x. [para(9(a,1),8(a,1,1,2)),rewrite([6(4)])]. 27 h(x) + y = x + (x + (x + (g(x) + y))). [para(10(a,1),7(a,1,1)),rewrite([7(6),7(5)])]. 28 x + h(y) = y + (y + (g(y) + (x + y))). [para(10(a,1),7(a,2,2)),rewrite([17(5),17(4),6(3)]),flip(a)]. 29 (h(x)' + (x + (x + (x + g(x)))')')' = x. [para(10(a,1),8(a,1,1,1,1))]. 30 ((x + (y + z))' + (y + (x + z)')')' = y. [para(17(a,1),8(a,1,1,1,1))]. 34 (x + (x + (x + g(x)))')' = g(x). [para(26(a,1),8(a,1,1,2)),rewrite([17(3),6(2),6(5)])]. 35 (g(x) + h(x)')' = x. [back_rewrite(29),rewrite([34(8),6(4)])]. 37 ((x + y)' + (x + (g(y) + h(y)'))')' = x. [para(35(a,1),8(a,1,1,2,1,2)),rewrite([6(9)])]. 38 (x + (g(x) + h(x))')' = g(x). [para(35(a,1),8(a,1,1,2)),rewrite([6(5)])]. 41 (g(x) + (x + (g(x) + h(x)))')' = x. [para(38(a,1),8(a,1,1,2)),rewrite([6(7)])]. 47 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),18(a,1,1,1,1))]. 49 (x + ((y + x)' + (x + y')'')')' = (y + x)'. [para(18(a,1),8(a,1,1,1))]. 93 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 97 ((x + (g(y) + (y + y)'))' + (y + x)')' = x. [para(26(a,1),19(a,1,1,2,1,1))]. 98 ((x + (g(y) + h(y)'))' + (y + x)')' = x. [para(35(a,1),19(a,1,1,2,1,1))]. 107 ((x + (g(y) + (y + (g(y) + h(y)))'))' + (y + x)')' = x. [para(41(a,1),19(a,1,1,2,1,1))]. 648 (x + (x + (g(y) + (h(y)' + (x + y)')))')' = (x + y)'. [para(37(a,1),8(a,1,1,2)),rewrite([6(8),7(8),7(7),6(10)])]. 1133 (h(x)' + (x + (g(x) + (x + x)'))')' = x + g(x). [para(10(a,1),47(a,1,1,1,1)),rewrite([7(7)])]. 1430 (x + (x + (x + (g(x) + ((y + h(x))' + (x + (x + (x + (g(x) + y'))))'')'))))' = (y + h(x))'. [para(27(a,1),49(a,1,1,2,1,2,1,1)),rewrite([27(15)])]. 2267 (h(x)' + (x + (x + (g(x) + (g(x) + (x + x)'))))')' = x + (x + g(x)). [para(10(a,1),97(a,1,1,2,1)),rewrite([17(8),7(7),7(6),17(8),17(7),6(12)])]. 7055 (x + (g(x) + (x + (g(x) + (h(x)' + (x + x)')))'))' = h(x)'. [para(1133(a,1),8(a,1,1,2)),rewrite([17(8),17(7),6(12),7(12)])]. 21226 (x + h(x)')' = g(x). [para(7055(a,1),30(a,1,1,1)),rewrite([648(14),26(7),6(3)])]. 21290 (x + (x + (g(x) + h(x)))')' = g(x). [para(21226(a,1),93(a,1,1,2,1,2,2)),rewrite([6(3),21226(11)])]. 21297 (g(x) + (g(x) + (h(x)' + (x + (g(x) + h(x)))'))')' = h(x)'. [para(21226(a,1),107(a,1,1,2)),rewrite([17(10),6(13)])]. 21565 (x + (g(x) + h(x)))' = h(x)'. [para(21290(a,1),98(a,1,1,2)),rewrite([6(10),7(10),6(13),21297(14)]),flip(a)]. 21575 (x + (x + (x + (x + (g(x) + g(x))))))' = h(x)'. [para(28(a,1),21565(a,1,1,2)),rewrite([6(3),17(4)])]. 22597 x + (x + (g(x) + g(x))) = x + (x + g(x)). [para(21575(a,1),47(a,1,1,1)),rewrite([7(10),7(9),7(8),2267(13)]),flip(a)]. 22602 (x + h(x))' = h(x)'. [para(21575(a,1),49(a,2)),rewrite([22597(5),10(4),22597(6),10(5),22597(9),10(8),27(7),27(15),1430(19)])]. 22603 $F # answer(Winker2b). [resolve(22602,a,12,a)]. ============================== end of proof ==========================