% problem-set/circuits/two.inverter.val.ver1.clauses
% created : 08/28/86
% revised : 07/14/88         

% description:
%
% This is made to validate the circuit described in the text, "Automated
% Reasoning" by Larry Wos et al. (chapter 7):
%
% A circuit using as many AND and OR gates as you like, but 
% using only two NOT gates. The circuit should be designed according to
% the following specification:
%
% o1 = not(i1)
% o2 = not(i2)
% o3 = not(i3)
%
% where, o1, o2, o3 are the outputs and i1, i2, i3 are the
% related inputs.  

% representation:
%
% See the above mentioned text. 

lex(0,1,21,20,19,18,17,16,15,14,13,12,10,9,8,7,6,5,4,3,2,a1,inv2,inv1,i3,i2,i1,not(x),and(x,x),or(x,x)).

% original state

CKT(o1).
CKT(o2).
CKT(o3).

% demodulators defining the structure

Equal(o1,13).
Equal(o2,17).
Equal(o3,5).
Equal(a1,and(inv1,i2)).
Equal(2,and(inv1,i3)).
Equal(3,or(a1,24)).
Equal(4,or(15,3)).
Equal(5,or(4,21)).
Equal(6,and(i1,i2)).
Equal(7,and(6,i3)).
Equal(8,or(a1,10)).
Equal(9,or(8,2)).
Equal(10,or(24,7)).
Equal(11,or(a1,2)).
Equal(12,or(11,16)).
Equal(13,or(12,21)).
Equal(14,and(i2,i3)).
Equal(15,and(inv2,6)).
Equal(16,and(14,inv2)).
Equal(17,or(18,21)).
Equal(18,or(19,25)).
Equal(19,and(23,inv2)).
Equal(20,or(22,14)).
Equal(21,and(inv1,inv2)).
Equal(22,or(23,6)).
Equal(23,and(i1,i3)).
Equal(24,and(i1,inv1)).
Equal(25,or(2,24)).
Equal(inv1,not(20)).
Equal(inv2,not(9)).

% Canonicalizing an exclusive-or/and expression with lex-dependent demodulation

Equal(eor(0,x), x).
Equal(eor(x,0), x).
Equal(eor(x,x), 0).
Equal(eor(x,eor(x,y)), y).
Equal(eor(x,y), eor(y,x)).
Equal(eor(y,eor(x,z)), eor(x,eor(y,z))).

Equal(and(0,x), 0).
Equal(and(x,0), 0).
Equal(and(1,x), x).
Equal(and(x,1), x).
Equal(and(x,x), x).
Equal(and(x,and(x,y)), and(x,y)).
Equal(and(x,y), and(y,x)).
Equal(and(y,and(x,z)), and(x,and(y,z))).
Equal(and(x,eor(y,z)),eor(and(x,y),and(x,z))).

Equal(not(x), eor(1,x)).
Equal(or(x,y), eor(and(x,y),eor(x,y))).
