% problem-set/algebra/boolean/part2_prob2.ver1.clauses
% created: 06/30/86
% revised: 07/31/89

% description:
%
% This problem is designed to prove that x + x = x in boolean
% algebra.  This version is from the McCharen paper [Aug 1976].

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

% 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).

% 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)).

% closure property

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

-EQUAL(f2(x,y), z) | PROD(x,y,z).
-EQUAL(f1(x,y), z) | SUM(x,y,z).

% existence of complements

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

% existence of identities

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

% denial of the theorem 

-SUM(a,a,a).