% problem-set/algebra/boolean/prob1.ver1.clauses
% created: 07/07/86
% revised: 08/08/89

% description:
%
% This problem is designed to prove that addition is associative.
% 
% This version has been taken from: 'Problems and Experiments from and
% with Automated Theorem-Proving Programs' - McCharen, Overbeek and Wos.

% representation:
%
% PROD(a,b,c) means a * b = c.
% SUM(a,b,c) means a + b = c.
%
% declare_predicates(3,[SUM,PROD]).
% declare_predicate(2,EQUAL).
% declare_functions(2,[f1,f2]).
% declare_function(1,comp).
% declare_variables([x,y,z,u,v,v1,v2,v3,v4]).
% declare_constants([0,1,a,b,c,d,e,f,g]).

% commutative property 

-SUM(x,y,v3)  |  SUM(y,x,v3).
-PROD(x,y,v3) |  PROD(y,x,v3).

% distributive property 

-PROD(x,y,v1)  | -PROD(x,z,v2)  | -SUM(y,z,v3)  | -PROD(x,v3,v4)|
 SUM(v1,v2,v4).
-PROD(x,y,v1)  | -PROD(x,z,v2)  | -SUM(y,z,v3)  | -SUM(v1,v2,v4) |
 PROD(x,v3,v4).
-PROD(y,x,v1)  | -PROD(z,x,v2)  | -SUM(y,z,v3)  | -PROD(v3,x,v4) |
 SUM(v1,v2,v4).
-PROD(y,x,v1)  | -PROD(z,x,v2)  | -SUM(y,z,v3)  | -SUM(v1,v2,v4)|
 PROD(v3,x,v4).
-SUM(x,y,v1)   | -SUM(x,z,v2)   | -PROD(y,z,v3) | -SUM(x,v3,v4)|
 PROD(v1,v2,v4).
-SUM(x,y,v1)   | -SUM(x,z,v2)   | -PROD(y,z,v3) | -PROD(v1,v2,v4) |
 SUM(x,v3,v4).
-SUM(y,x,v1)   | -SUM(z,x,v2)   | -PROD(y,z,v3) | -SUM(v3,x,v4) |
 PROD(v1,v2,v4).
-SUM(y,x,v1)   | -SUM(z,x,v2)   | -PROD(y,z,v3) | -PROD(v1,v2,v4) |
 SUM(v3,x,v4).

% existence of complements 

SUM(x,comp(x),1).
SUM(comp(x),x,1).
PROD(x,comp(x),0).
PROD(comp(x),x,0).

% the above operations are well defined 

-SUM(x,y,u)    | -SUM(x,y,v)    | EQUAL(u,v).
-PROD(x,y,u)   | -PROD(x,y,v)   | EQUAL(u,v).
 
% equality axioms

EQUAL(x,x).
-EQUAL(x,y)    |  EQUAL(y,x).
-EQUAL(x,y)    | -EQUAL(y,z)    | EQUAL(x,z).
 
% equality substitution axioms

-EQUAL(x,y)    | -SUM(x,v1,v2) | SUM(y,v1,v2).
-EQUAL(x,y)    | -SUM(v1,x,v2) | SUM(v1,y,v2).
-EQUAL(x,y)    | -SUM(v1,v2,x) | SUM(v1,v2,y).
-EQUAL(x,y)    | -PROD(x,v1,v2) | PROD(y,v1,v2).
-EQUAL(x,y)    | -PROD(v1,x,v2) | PROD(v1,y,v2).
-EQUAL(x,y)    | -PROD(v1,v2,x) | PROD(v1,v2,y).
-EQUAL(x,y)    |  EQUAL(f1(x,v1),f1(y,v1)).
-EQUAL(x,y)    |  EQUAL(f1(v1,x),f1(v1,y)).
-EQUAL(x,y)    |  EQUAL(f2(x,v1),f2(y,v1)).
-EQUAL(x,y)    |  EQUAL(f2(v1,x),f2(v1,y)).
-EQUAL(x,y)    |  EQUAL(comp(x),comp(y)).
 
% existence of identities 

SUM(x,0,x).
SUM(0,x,x).
PROD(x,1,x).
PROD(1,x,x).

% closure property 

SUM(x,y,f1(x,y)).
PROD(x,y,f2(x,y)).

% denial of the theorem

 SUM(b,c,d).
 SUM(a,d,e).
 SUM(a,b,f).
 SUM(f,c,g).
-EQUAL(e,g).