Prooof out3b2-38 x + (x + x')' = g(x). (x + (x + g(x)))' = h(x). % Problem 38 ============================== PROOF ================================= % Proof 1 at 109.75 (+ 0.40) seconds: Winker2a. % Length of proof is 40. % Level of proof is 11. % Maximum clause weight is 32. % Given clauses 897. 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))]. 22 ((x + y)' + (x + ((y + z)' + (y + z')'))')' = x. [para(8(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. 24 x + ((x + x')' + y) = g(x) + y. [para(9(a,1),7(a,1,1)),flip(a)]. 27 (h(x) + (x + (x + g(x))')')' = x. [para(10(a,1),8(a,1,1,1))]. 30 x + (y + (x + x')') = y + g(x). [para(9(a,1),17(a,1,2)),flip(a)]. 33 (x + (x + (h(x) + (x + g(x))'))')' = h(x). [para(27(a,1),8(a,1,1,2)),rewrite([17(6),6(8)])]. 35 ((x + y')' + (y + x)')' = x. [para(6(a,1),18(a,1,1))]. 36 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),18(a,1,1,1,1))]. 40 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(18(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 57 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 59 ((x + (y + z))' + ((x + z)' + y)')' = y. [para(17(a,1),19(a,1,1,1,1))]. 197 (h(x) + (x + (x + (h(x) + (x + g(x))')))')' = x. [para(33(a,1),8(a,1,1,2)),rewrite([6(10)])]. 234 ((x + (y + z)')' + (x + (y + (y + (z' + (y + z)'))'))')' = x. [para(8(a,1),22(a,1,1,2,1,2,2)),rewrite([6(9),7(9),6(11)])]. 276 (x + ((x + y')' + (((y + x)' + z)' + ((y + x)' + z')'))')' = (x + y')'. [para(35(a,1),22(a,1,1,1))]. 678 (h(x) + (g(x) + (x + x)')')' = g(x). [para(10(a,1),36(a,1,1,1))]. 700 (g(x) + (g(x) + (h(x) + (x + x)'))')' = h(x). [para(678(a,1),8(a,1,1,2)),rewrite([17(6),6(9)])]. 970 ((x + y)' + (h(x) + (y + (x + (x + g(x))')'))')' = y. [para(27(a,1),59(a,1,1,2,1,1)),rewrite([6(12)])]. 1278 ((x + (x + g(x))')' + (x + (h(x)' + (x + (x + g(x))')'))')' = x. [para(27(a,1),40(a,1,1,2,1,2,2)),rewrite([6(13),6(14),7(14),27(25)])]. 3153 (x + (x + g(x))')' = (x + x')'. [para(9(a,1),57(a,1,1,2,1,2))]. 3155 (h(x) + (x + x')')' = x. [para(27(a,1),57(a,1,1,2,1,2,2)),rewrite([6(7),17(8),17(7),197(11),3153(6)]),flip(a)]. 3441 ((x + x')' + (g(x) + h(x)')')' = x. [back_rewrite(1278),rewrite([3153(5),3153(10),30(10),6(7)])]. 3451 ((x + y)' + (h(x) + (y + (x + x')'))')' = y. [back_rewrite(970),rewrite([3153(8)])]. 5005 ((x + x)' + (g(x) + h(x))')' = x. [para(9(a,1),3451(a,1,1,2,1,2)),rewrite([6(5)])]. 23085 (x + x')' = (x + h(x))'. [para(5005(a,1),276(a,1,1,2,1,2,2)),rewrite([6(9),7(9),6(11),17(12),24(12),700(10)]),flip(a)]. 26373 ((x + h(x))' + (g(x) + h(x)')')' = x. [back_rewrite(3441),rewrite([23085(3)])]. 26466 (h(x) + (x + h(x))')' = x. [back_rewrite(3155),rewrite([23085(4)])]. 26736 x + (y + (x + h(x))') = y + g(x). [back_rewrite(30),rewrite([23085(3)])]. 26867 (x + (x + (h(x) + (g(x) + h(x)')'))')' = h(x). [para(26466(a,1),234(a,1,1,1)),rewrite([26736(8),6(5),17(8)])]. 27962 (g(x) + h(x)')' = h(x). [para(26373(a,1),19(a,1,1,2)),rewrite([6(8),7(8),6(10),26867(11)]),flip(a)]. 27990 (h(x) + (g(x)' + h(x)')')' = h(x)'. [para(27962(a,1),18(a,1,1,1)),rewrite([6(6)])]. 27991 $F # answer(Winker2a). [resolve(27990,a,11,a)]. ============================== end of proof ==========================