% Prover9 input and proofs for % % 677 + Associativity ==> 255 % 677 + existence of a single "middle associative" element ==> 255 % % G.Passmore formulas(assumptions). all x all y (x = f(y, f(x, f(f(y, x), y)))). all x all y all z (f(x,f(y,z)) = f(f(x,y),z)). end_of_list. formulas(goals). all x (f(f(f(x,x),x),x) = x). end_of_list. Proof: 1 (all x all y x = f(y,f(x,f(f(y,x),y)))) # label(non_clause). [assumption]. 2 (all x all y all z f(x,f(y,z)) = f(f(x,y),z)) # label(non_clause). [assumption]. 3 (all x f(f(f(x,x),x),x) = x) # label(non_clause) # label(goal). [goal]. 4 f(x,f(y,f(f(x,y),x))) = y. [clausify(1)]. 5 f(f(x,y),z) = f(x,f(y,z)). [clausify(2)]. 6 f(f(f(c1,c1),c1),c1) != c1. [deny(3)]. 7 f(c1,f(c1,f(c1,c1))) != c1. [copy(6),rewrite([5(5),5(7),5(6)])]. 8 f(x,f(y,f(x,f(y,x)))) = y. [back_rewrite(4),rewrite([5(2)])]. 11 f(x,f(y,f(z,f(x,f(y,f(z,x)))))) = f(y,z). [para(5(a,1),8(a,1,2,2,2)),rewrite([5(5)])]. 12 f(x,f(y,x)) = y. [para(5(a,1),8(a,1,2,2)),rewrite([5(7),11(6)])]. 13 f(x,y) = y. [para(8(a,1),8(a,1,2,2,2)),rewrite([12(2),12(3),5(3),12(3),5(3),12(2)])]. 14 x = y. [para(8(a,1),8(a,1,2,2,2)),rewrite([13(1),13(1),13(1),13(1),13(1),13(1),13(1),13(1),13(1)])]. 15 $F. [resolve(14,a,7,a)]. -- assign(max_weight, 100). formulas(assumptions). all x all y (x = f(y, f(x, f(f(y, x), y)))). exists c all y all z (f(y,f(c,z)) = f(f(y,c),z)). end_of_list. formulas(goals). all x (f(f(f(x,x),x),x) = x). end_of_list. Proof: 1 (all x all y x = f(y,f(x,f(f(y,x),y)))) # label(non_clause). [assumption]. 2 (exists c all y all z f(y,f(c,z)) = f(f(y,c),z)) # label(non_clause). [assumption]. 3 (all x f(f(f(x,x),x),x) = x) # label(non_clause) # label(goal). [goal]. 4 f(x,f(y,f(f(x,y),x))) = y. [clausify(1)]. 5 f(f(x,c1),y) = f(x,f(c1,y)). [clausify(2)]. 6 f(f(f(c2,c2),c2),c2) != c2. [deny(3)]. 7 f(x,f(f(y,f(f(x,y),x)),f(y,x))) = f(y,f(f(x,y),x)). [para(4(a,1),4(a,1,2,2,1))]. 9 f(x,f(c1,f(x,f(c1,x)))) = c1. [para(5(a,1),4(a,1,2,2))]. 11 f(f(x,f(c1,c1)),y) = f(x,f(c1,f(c1,y))). [para(5(a,1),5(a,1,1)),rewrite([5(10)])]. 16 f(x,f(f(y,f(c1,f(f(x,f(y,c1)),x))),f(y,f(c1,x)))) = f(y,f(c1,f(f(x,f(y,c1)),x))). [para(5(a,1),7(a,1,2,1)),rewrite([5(10),5(19)])]. 21 f(x,f(f(f(c1,f(x,f(c1,x))),f(c1,x)),f(f(c1,f(x,f(c1,x))),x))) = f(f(c1,f(x,f(c1,x))),f(c1,x)). [para(9(a,1),7(a,1,2,1,2,1)),rewrite([9(27)])]. 23 f(f(f(x,f(f(c1,x),c1)),f(x,c1)),f(c1,f(f(f(x,f(f(c1,x),c1)),f(x,c1)),f(x,f(f(c1,x),c1))))) = c1. [para(7(a,1),9(a,1,2,2,2))]. 24 f(f(c1,f(c1,f(c1,c1))),f(c1,f(f(c1,f(c1,f(c1,c1))),c1))) = c1. [para(9(a,1),9(a,1,2,2,2))]. 28 f(f(x,f(c1,f(c1,c1))),y) = f(x,f(c1,f(c1,f(c1,y)))). [para(11(a,1),5(a,1,1)),rewrite([11(14)])]. 32 f(x,f(c1,f(c1,f(c1,f(x,f(c1,f(c1,f(c1,f(x,f(c1,c1)))))))))) = c1. [para(11(a,1),9(a,1,2,2)),rewrite([11(18)])]. 34 f(c1,c1) = c1. [back_rewrite(24),rewrite([28(17),9(17),28(11),9(10)])]. 36 f(x,f(c1,f(c1,f(c1,f(x,f(c1,f(c1,f(c1,f(x,c1))))))))) = c1. [back_rewrite(32),rewrite([34(9)])]. 43 f(x,f(c1,f(c1,y))) = f(x,f(c1,y)). [back_rewrite(11),rewrite([34(3),5(3)]),flip(a)]. 44 f(x,f(c1,f(x,f(c1,f(x,c1))))) = c1. [back_rewrite(36),rewrite([43(11),43(10),43(11),43(10)])]. 46 f(c1,f(c1,x)) = f(c1,x). [para(34(a,1),5(a,1,1)),flip(a)]. 48 f(c1,x) = x. [para(4(a,1),46(a,1,2)),rewrite([4(9)])]. 49 f(x,f(x,c1)) = x. [para(4(a,1),46(a,2)),rewrite([48(4),48(6),48(5)])]. 52 f(x,x) = c1. [back_rewrite(44),rewrite([48(5),49(4),48(2)])]. 53 f(x,c1) = c1. [back_rewrite(23),rewrite([48(2),49(3),49(3),48(3),49(4),49(4),48(3),49(4),52(2),52(3)])]. 54 c1 = x. [back_rewrite(21),rewrite([48(3),52(2),52(3),48(3),48(2),48(3),52(2),52(3),48(2),52(1),53(2),48(4),52(3),52(4),48(4),48(3)])]. 55 f(x,y) = c1. [back_rewrite(16),rewrite([53(3),53(3),48(3),48(2),48(3),52(3),53(2),53(4),53(4),48(4),48(3)]),flip(a)]. 56 c2 != c1. [back_rewrite(6),rewrite([52(3),55(3),55(3)]),flip(a)]. 57 $F. [resolve(56,a,54,a(flip))].