% problem-set/algebra/boolean/prob_10.ver1.clauses 
% created: 07/09/86
% revised: 07/27/89

% description:
%
% This problem is designed to prove that -(x + y) = (-x) + (-y).
% 
% This version was taken from: 'Problems and Experiments from and
% with Automated Theorem-Proving Programs' - McCharen, Overbeek, and Wos.

% Representation:
%
% 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]).

% 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)).
 
% Denial of the theorem

 SUM(a,b,c).
 SUM(comp(a),comp(b),d).
-EQUAL(comp(c),d).