#!/bin/sh
# This is a shell archive, meaning:
# 1. Remove everything above the #!/bin/sh line.
# 2. Save the resulting text in a file.
# 3. Execute the file with /bin/sh (not csh) to create the files:
# README
# design_or.desc
# design_or.ver1
# design_or.ver1.clauses
# design_or.ver1.out
# intchg_val.desc
# intchg_val.ver1
# intchg_val.ver1.clauses
# intchg_val.ver1.out
# interchange.desc
# interchange.ver1.clauses
# interchange.ver1.in
# interchange.ver1.out
# two.inverter.desc
# two.inverter.val.desc
# two.inverter.val.ver1.clauses
# two.inverter.val.ver1.in
# two.inverter.val.ver1.out
# two.inverter.ver1.clauses
# two.inverter.ver1.in
# two.inverter.ver1.out
# two.inverter.ver2.clauses
# two.inverter.ver2.in
# two.inverter.ver2.out
# This archive created: Tue Aug 16 11:14:10 1988
export PATH; PATH=/bin:$PATH
if test -f 'README'
then
echo shar: over-writing existing file "'README'"
fi
cat << \SHAR_EOF > 'README'
problem-set/circuits/README
created: 09/02/86
revised: 07/15/88
Contents of 'circuits':
----------------------
Main File Headings
------------------------------------------------------------------------
README : You are currently in this file.
design_or : To design an OR-gate from NAND-gates.
interchange : To design a circuit which interchanges the
given inputs.
intchg_val : The ciruit validation of circuit which
interchanges the inputs.
two_inverter : To design a specific ciruit using only two
NOT-gates, and any number of AND-gates and
OR-gates.
two_inverter_val : The circuit validation of the circuit
described by the two_inverter problem.
------------------------------------------------------------------------
For each problem, there are several standard files, which include one
probname.desc file and at least one of each of probname.ver#.in,
probname.ver#.clauses, and probname.ver#.out. These contain the
following:
probname.desc : contains the Natural Language Description of the
problem, where available, credits for problem formulation,
and complete details on each formulation and each version.
probname.ver#.in : contains the problem specification, input clauses, and
strategy for OTTER; this file is ready to run.
probname.ver#.clauses : contains the description, commentary, and the
actual clauses (including the denial of the conclusion) used for
probname.ver#.in, without any strategy; note that comments always are
on lines beginning with a %, preceding the clauses to which they
refer, and that clauses terminate with periods.
probname.ver#.out : contains the output from running probname.ver#.in
with OTTER, with proof if one is found, and with statistics on
the clauses generated and CPU time used.
HOW TO RUN :
----------------------------------------------------------------------
Invoke OTTER by using the following command :
otter < probname.ver#.in [ > outfile ] [ & ]
NOTE : '> outfile' may be used to send all output to a file named outfile;
'&' may be used to run the program in the background.
SHAR_EOF
if test -f 'design_or.desc'
then
echo shar: over-writing existing file "'design_or.desc'"
fi
cat << \SHAR_EOF > 'design_or.desc'
problem-set/circuits/design_or.desc
created: 08/28/86
revised: 07/11/88
Natural Language Description:
The files beginning with design_or concern the designing
of an OR gate using NAND gates.
Versions:
design_or.ver1 - Nonequality bases axioms are used, hyper
resolution is the inference rule, and demodulators are
included.
created by: E. Lusk
verified for ITP: 09/03/86
translated for OTTER: SLM
verified for OTTER: 07/11/88
SHAR_EOF
if test -f 'design_or.ver1'
then
echo shar: over-writing existing file "'design_or.ver1'"
fi
cat << \SHAR_EOF > 'design_or.ver1'
% problem-set/circuits/design_or.ver1
% created : 08/28/86
% revised : 07/11/88
% description:
%
% This run designs an OR gate, using NAND gates.
% representation:
%
% This input file came with no explanation of
% the representation.
set(hyper_res).
list(axioms).
-Tab(x1,x2,x3,x4) | -Tab(y1,y2,y3,y4) |
Tab(nand(x1,y1),nand(x2,y2),nand(x3,y3),nand(x4,y4)).
-Tab(0,1,1,1).
end_of_list.
list(sos).
Tab(0,0,1,1).
Tab(0,1,0,1).
end_of_list.
list(demodulators).
Equal(nand(x,y),not(and(x,y))).
Equal(and(x,0),0).
Equal(and(x,1),x).
Equal(not(0),1).
Equal(not(1),0).
end_of_list.
SHAR_EOF
if test -f 'design_or.ver1.clauses'
then
echo shar: over-writing existing file "'design_or.ver1.clauses'"
fi
cat << \SHAR_EOF > 'design_or.ver1.clauses'
% problem-set/circuits/design_or.ver1.clauses
% created : 08/28/86
% revised : 07/11/88
% description:
%
% This run designs an OR gate, using NAND gates.
% representation:
%
% This input file came with no explanation of
% the representation.
-Tab(x1,x2,x3,x4) | -Tab(y1,y2,y3,y4) |
Tab(nand(x1,y1),nand(x2,y2),nand(x3,y3),nand(x4,y4)).
-Tab(0,1,1,1).
Tab(0,0,1,1).
Tab(0,1,0,1).
Equal(nand(x,y),not(and(x,y))).
Equal(and(x,0),0).
Equal(and(x,1),x).
Equal(not(0),1).
Equal(not(1),0).
SHAR_EOF
if test -f 'design_or.ver1.out'
then
echo shar: over-writing existing file "'design_or.ver1.out'"
fi
cat << \SHAR_EOF > 'design_or.ver1.out'
problem-set/circuits/design_or.ver1.out
created: 08/28/86
revised: 07/11/88
OTTER release 0.9, 19 May 1988
set(hyper_res).
list(axioms).
1 -Tab(x1,x2,x3,x4) | -Tab(y1,y2,y3,y4) | Tab(nand(x1,y1),nand(x2,y2),nand(x3,y3),nand(x4,y4)).
2 -Tab(0,1,1,1).
end_of_list.
list(sos).
3 Tab(0,0,1,1).
4 Tab(0,1,0,1).
end_of_list.
list(demodulators).
5 Equal(nand(x,y),not(and(x,y))).
6 Equal(and(x,0),0).
7 Equal(and(x,1),x).
8 Equal(not(0),1).
9 Equal(not(1),0).
end_of_list.
----> UNIT CONFLICT at 0.35 sec ----> 17 (15,2) .
------------ END OF SEARCH ------------
---------------- PROOF ----------------
1 -Tab(x1,x2,x3,x4) | -Tab(y1,y2,y3,y4) | Tab(nand(x1,y1),nand(x2,y2),nand(x3,y3),nand(x4,y4)).
2 -Tab(0,1,1,1).
3 Tab(0,0,1,1).
4 Tab(0,1,0,1).
5 Equal(nand(x,y),not(and(x,y))).
6 Equal(and(x,0),0).
7 Equal(and(x,1),x).
8 Equal(not(0),1).
9 Equal(not(1),0).
10 (3,1,3,5,6,8,5,6,8,5,7,9,5,7,9) Tab(1,1,0,0).
11 (4,1,4,5,6,8,5,7,9,5,6,8,5,7,9) Tab(1,0,1,0).
15 (11,1,10,5,7,9,5,6,8,5,7,8,5,6,8) Tab(0,1,1,1).
17 (15,2) .
--------------- options ---------------
set(hyper_res).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).
clear(binary_res).
clear(UR_res).
clear(para_from).
clear(para_into).
clear(demod_inf).
clear(para_from_left).
clear(para_from_right).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 0).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 4).
assign(fpa_terms, 4).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).
-------------- statistics -------------
clauses input 9
clauses given 4
clauses generated 21
demodulation rewrites 240
clauses wt or lit delete 0
tautologies deleted 0
clauses forward subsumed 13
(clauses subsumed by sos) 9
unit deletions 0
clauses kept 8
empty clauses 1
factors generated 0
clauses back subsumed 0
clauses not processed 3
----------- times (seconds) -----------
run time 0.46
input time 0.10
binary_res time 0.00
hyper_res time 0.05
UR_res time 0.00
para_into time 0.00
para_from time 0.00
pre_process time 0.16
demod time 0.10
weigh time 0.00
for_sub time 0.01
unit_del time 0.00
post_process time 0.02
back_sub time 0.01
conflict time 0.01
factor time 0.00
FPA build time 0.02
IS build time 0.01
print_cl time 0.08
cl integrate time 0.01
window time 0.00
SHAR_EOF
if test -f 'intchg_val.desc'
then
echo shar: over-writing existing file "'intchg_val.desc'"
fi
cat << \SHAR_EOF > 'intchg_val.desc'
problem-set/circuits/intchg_val.desc
Natural Language Description:
The files beginning with intchg_val concern the validation
of a circuit which takes as input x and y and outputs y and x
without crossing any wires.
Versions:
intchg_val.ver1 - The clauses include the 1nput to the circuit
and the demodulators required to retrace the flow to validate
the circuit. Demodultion is the inference rule.
created by: E. Lusk
verified for ITP: not yet
translated for OTTER: SLM
verified for OTTER: not yet
SHAR_EOF
if test -f 'intchg_val.ver1'
then
echo shar: over-writing existing file "'intchg_val.ver1'"
fi
cat << \SHAR_EOF > 'intchg_val.ver1'
% problem-set/circuits/intchg_val.ver1
% created : 09/02/86
% revised : 07/11/88
% description:
%
% This run validates one of the circuit designs that will take
% x and y as input and output y and x without crossing any wires.
% representation:
%
% This input file came with no explanation of
% the representation.
set(demod_inf).
assign(max_given, 1).
assign(demod_limit, 5000).
clear(demod_hist).
lex(And(x,x), Or(x,x) ,i2,i1,f3,f2,f1,e2,e1,d3,d2,d1,c2,c1,b3,b2,b1,a2,a1,Not(x)).
list(sos).
ckt(Input(i1,i2),Output(a1,a2)).
end_of_list.
list(demodulators).
Equal(a1,And(b1,b3)).
Equal(a2,And(b2,b3)).
Equal(b1,Not(d1)).
Equal(b2,Not(d2)).
Equal(b3,Or(c1,c2)).
Equal(c1,Or(d1,d3)).
Equal(c2,Or(d2,d3)).
Equal(d3,f3).
Equal(d1,Not(e1)).
Equal(d2,Not(e2)).
Equal(e1,Or(f1,f3)).
Equal(e2,Or(f2,f3)).
Equal(f1,Not(i1)).
Equal(f2,Not(i2)).
Equal(f3,And(i1,i2)).
% commutativity and associativity
Equal(And(x,y),And(y,x)).
Equal(Or(x,y),Or(y,x)).
Equal(And(x,And(y,z)),And(And(x,y),z)).
Equal(Or(x,Or(y,z)),Or(Or(x,y),z)).
% sorting
Equal(Or(Or(x,y),z),Or(Or(x,z),y)).
Equal(And(And(x,y),z),And(And(x,z),y)).
% canonicalization to move Not to inside
Equal(Not(And(x,y)),Or(Not(x),Not(y))).
Equal(Not(Or(x,y)),And(Not(x),Not(y))).
% canonicalization to sum-of-products
Equal(And(Or(x,y),z),Or(And(x,z),And(y,z))).
% simplifiers
Equal(And(x,x),x).
Equal(And(And(x,y),y),And(x,y)).
Equal(And(And(x,y),x),And(x,y)).
Equal(Or(x,x),x).
Equal(Or(Or(x,y),y),Or(x,y)).
Equal(Or(Or(x,y),x),Or(x,y)).
Equal(And(x,Not(x)),0).
Equal(And(And(x,y),Not(y)),0).
Equal(And(And(x,y),Not(x)),0).
Equal(Or(x,Not(x)),1).
Equal(Or(Or(x,y),Not(y)),1).
Equal(Or(Or(x,y),Not(x)),1).
Equal(Not(Not(x)),x).
Equal(Or(And(x,y),And(x,Not(y))),x).
Equal(Or(And(x,y),And(y,Not(x))),y).
% evaluators
Equal(And(x,0),0).
Equal(And(x,1),x).
Equal(Or(x,0),x).
Equal(Or(x,1),1).
Equal(Not(0),1).
Equal(Not(1),0).
end_of_list.
SHAR_EOF
if test -f 'intchg_val.ver1.clauses'
then
echo shar: over-writing existing file "'intchg_val.ver1.clauses'"
fi
cat << \SHAR_EOF > 'intchg_val.ver1.clauses'
% problem-set/circuits/intchg_val.ver1.clauses
% created : 09/02/86
% revised : 07/11/88
% description:
%
% This run validates one of the circuit designs that will take
% x and y as input and output y and x without crossing any wires.
% representation:
%
% This input file came with no explanation of
% the representation.
lex(And(x,x), Or(x,x) ,i2,i1,f3,f2,f1,e2,e1,d3,d2,d1,c2,c1,b3,b2,b1,a2,a1,Not(x)).
ckt(Input(i1,i2),Output(a1,a2)).
Equal(a1,And(b1,b3)).
Equal(a2,And(b2,b3)).
Equal(b1,Not(d1)).
Equal(b2,Not(d2)).
Equal(b3,Or(c1,c2)).
Equal(c1,Or(d1,d3)).
Equal(c2,Or(d2,d3)).
Equal(d3,f3).
Equal(d1,Not(e1)).
Equal(d2,Not(e2)).
Equal(e1,Or(f1,f3)).
Equal(e2,Or(f2,f3)).
Equal(f1,Not(i1)).
Equal(f2,Not(i2)).
Equal(f3,And(i1,i2)).
% commutativity and associativity
Equal(And(x,y),And(y,x)).
Equal(Or(x,y),Or(y,x)).
Equal(And(x,And(y,z)),And(And(x,y),z)).
Equal(Or(x,Or(y,z)),Or(Or(x,y),z)).
% sorting
Equal(Or(Or(x,y),z),Or(Or(x,z),y)).
Equal(And(And(x,y),z),And(And(x,z),y)).
% canonicalization to move Not to inside
Equal(Not(And(x,y)),Or(Not(x),Not(y))).
Equal(Not(Or(x,y)),And(Not(x),Not(y))).
% canonicalization to sum-of-products
Equal(And(Or(x,y),z),Or(And(x,z),And(y,z))).
% simplifiers
Equal(And(x,x),x).
Equal(And(And(x,y),y),And(x,y)).
Equal(And(And(x,y),x),And(x,y)).
Equal(Or(x,x),x).
Equal(Or(Or(x,y),y),Or(x,y)).
Equal(Or(Or(x,y),x),Or(x,y)).
Equal(And(x,Not(x)),0).
Equal(And(And(x,y),Not(y)),0).
Equal(And(And(x,y),Not(x)),0).
Equal(Or(x,Not(x)),1).
Equal(Or(Or(x,y),Not(y)),1).
Equal(Or(Or(x,y),Not(x)),1).
Equal(Not(Not(x)),x).
Equal(Or(And(x,y),And(x,Not(y))),x).
Equal(Or(And(x,y),And(y,Not(x))),y).
% evaluators
Equal(And(x,0),0).
Equal(And(x,1),x).
Equal(Or(x,0),x).
Equal(Or(x,1),1).
Equal(Not(0),1).
Equal(Not(1),0).
SHAR_EOF
if test -f 'intchg_val.ver1.out'
then
echo shar: over-writing existing file "'intchg_val.ver1.out'"
fi
cat << \SHAR_EOF > 'intchg_val.ver1.out'
problem-set/circuits/intchg_val.ver1.out
created: 09/02/86
revised: 07/14/88
OTTER version 0.9, 19 May 1988.
set(demod_inf).
assign(max_given,1).
assign(demod_limit,5000).
clear(demod_hist).
lex(And(x,x),Or(x,x),i2,i1,f3,f2,f1,e2,e1,d3,d2,d1,c2,c1,b3,b2,b1,a2,a1,Not(x)).
list(sos).
1 ckt(Input(i1,i2),Output(a1,a2)).
end_of_list.
list(demodulators).
lex-dependent demodulator: Equal(And(x,y),And(y,x))
lex-dependent demodulator: Equal(Or(x,y),Or(y,x))
lex-dependent demodulator: Equal(Or(Or(x,y),z),Or(Or(x,z),y))
lex-dependent demodulator: Equal(And(And(x,y),z),And(And(x,z),y))
2 Equal(a1,And(b1,b3)).
3 Equal(a2,And(b2,b3)).
4 Equal(b1,Not(d1)).
5 Equal(b2,Not(d2)).
6 Equal(b3,Or(c1,c2)).
7 Equal(c1,Or(d1,d3)).
8 Equal(c2,Or(d2,d3)).
9 Equal(d3,f3).
10 Equal(d1,Not(e1)).
11 Equal(d2,Not(e2)).
12 Equal(e1,Or(f1,f3)).
13 Equal(e2,Or(f2,f3)).
14 Equal(f1,Not(i1)).
15 Equal(f2,Not(i2)).
16 Equal(f3,And(i1,i2)).
17 Equal(And(x,y),And(y,x)).
18 Equal(Or(x,y),Or(y,x)).
19 Equal(And(x,And(y,z)),And(And(x,y),z)).
20 Equal(Or(x,Or(y,z)),Or(Or(x,y),z)).
21 Equal(Or(Or(x,y),z),Or(Or(x,z),y)).
22 Equal(And(And(x,y),z),And(And(x,z),y)).
23 Equal(Not(And(x,y)),Or(Not(x),Not(y))).
24 Equal(Not(Or(x,y)),And(Not(x),Not(y))).
25 Equal(And(Or(x,y),z),Or(And(x,z),And(y,z))).
26 Equal(And(x,x),x).
27 Equal(And(And(x,y),y),And(x,y)).
28 Equal(And(And(x,y),x),And(x,y)).
29 Equal(Or(x,x),x).
30 Equal(Or(Or(x,y),y),Or(x,y)).
31 Equal(Or(Or(x,y),x),Or(x,y)).
32 Equal(And(x,Not(x)),0).
33 Equal(And(And(x,y),Not(y)),0).
34 Equal(And(And(x,y),Not(x)),0).
35 Equal(Or(x,Not(x)),1).
36 Equal(Or(Or(x,y),Not(y)),1).
37 Equal(Or(Or(x,y),Not(x)),1).
38 Equal(Not(Not(x)),x).
39 Equal(Or(And(x,y),And(x,Not(y))),x).
40 Equal(Or(And(x,y),And(y,Not(x))),y).
41 Equal(And(x,0),0).
42 Equal(And(x,1),x).
43 Equal(Or(x,0),x).
44 Equal(Or(x,1),1).
45 Equal(Not(0),1).
46 Equal(Not(1),0).
end_of_list.
new given clause: 1 ckt(Input(i1,i2),Output(a1,a2)).
** KEPT: 47 (1) ckt(Input(i1,i2),Output(i2,i1)).
------------ END OF SEARCH ------------
search stopped by max_given option.
--------------- options ---------------
set(demod_inf).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).
clear(binary_res).
clear(hyper_res).
clear(UR_res).
clear(para_from).
clear(para_into).
clear(para_from_left).
clear(para_from_right).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(demod_hist).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 1).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 4).
assign(fpa_terms, 4).
assign(demod_limit, 5000).
assign(max_proofs, 1).
assign(neg_weight, 0).
-------------- statistics -------------
clauses input 46
clauses given 1
clauses generated 1
demodulation rewrites 157
clauses wt or lit delete 0
tautologies deleted 0
clauses forward subsumed 0
(clauses subsumed by sos) 0
unit deletions 0
clauses kept 1
empty clauses 0
factors generated 0
clauses back subsumed 0
clauses not processed 0
----------- times (seconds) -----------
run time 1.61
input time 1.21
binary_res time 0.00
hyper_res time 0.00
UR_res time 0.00
para_into time 0.00
para_from time 0.00
pre_process time 0.27
demod time 0.27
weigh time 0.00
for_sub time 0.00
unit_del time 0.00
post_process time 0.00
back_sub time 0.00
conflict time 0.00
factor time 0.00
FPA build time 0.00
IS build time 0.01
print_cl time 0.18
cl integrate time 0.03
window time 0.00
SHAR_EOF
if test -f 'interchange.desc'
then
echo shar: over-writing existing file "'interchange.desc'"
fi
cat << \SHAR_EOF > 'interchange.desc'
problem-set/circuits/interchange.desc
created : 08/28/86
revised : 07/11/88
Natural Language Description:
The files beginning with interchange concern the designing
of a circuit with inputs x and y and outputs y and x
containing no crossing of wires (interchanging of inputs).
Versions:
interchange.ver1 - Nonequality based axioms are used, hyper
resolution is the inference rule, and demodulators
are included.
created by: E. Lusk
verified for ITP: 09/03/86
translated for OTTER by: SLM
verified for OTTER: 07/11/88
SHAR_EOF
if test -f 'interchange.ver1.clauses'
then
echo shar: over-writing existing file "'interchange.ver1.clauses'"
fi
cat << \SHAR_EOF > 'interchange.ver1.clauses'
% problem-set/circuits/interchange.ver1.clauses
% created : 08/28/86
% revised : 07/11/88
% description:
%
% Design a circuit with inputs x and y whose outputs are
% y and x, and contains no crossings of wires.
% representation:
%
% We represent the circuit built up so far by
% ckt(Top(x),Middle(y),Bottom(z)), where Top and Bottom are lists
% of outputs, counting outward from the middle.
% split the middle, keeping the middle
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(and(y,x1),x2)),Middle(y),Bot(C(and(y,z1),z2))).
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(or(y,x1),x2)),Middle(y),Bot(C(or(y,z1),z2))).
% split the middle, omitting the middle
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(and(y,x1),x2)),NIL,Bot(C(and(y,z1),z2))).
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(or(y,x1),x2)),NIL,Bot(C(or(y,z1),z2))).
% join across the middle if it is empty, not keeping the sides
-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) |
ckt(Top(x2),Middle(and(x1,y1)),Bot(y2)).
-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) |
ckt(Top(x2),Middle(or(x1,y1)),Bot(y2)).
% join across the middle, keeping the sides
-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) |
ckt(Top(C(x1,x2)),Middle(and(x1,y1)),Bot(C(y1,y2))).
-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) |
ckt(Top(C(x1,x2)),Middle(or(x1,y1)),Bot(C(y1,y2))).
% join to middle, keeping the sides
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(and(y,x1),C(x1,x2))),NIL,Bot(C(and(y,z1),C(z1,z2)))).
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(or(y,x1),C(x1,x2))),NIL,Bot(C(or(y,z1),C(z1,z2)))).
% split the wire nearest the middle
% this clause is superseded by the previous four
% -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
% ckt(Top(C(x1,C(x1,x2))),Middle(y),Bot(C(z1,C(z1,z2)))).
% join the two wires nearest the middle
-ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) |
ckt(Top(C(and(x1,x2),x3)),Middle(y),Bot(C(and(z1,z2),z3))).
-ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) |
ckt(Top(C(or(x1,x2),x3)),Middle(y),Bot(C(or(z1,z2),z3))).
% put inverter on the middle wire
-ckt(Top(x),Middle(y),Bot(z)) |
ckt(Top(x),Middle(not(y)),Bot(z)).
% put inverter on the adjacent wires
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(not(x1),x2)),Middle(y),Bot(C(not(z1),z2))).
-ckt(Top(C(x1,x2)),NIL,Bot(C(z1,z2))) |
ckt(Top(C(not(x1),x2)),NIL,Bot(C(not(z1),z2))).
% cannot construct the answer
-ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))).
% subsumer to get rid of circuits which are the
% same on top and bottom
ckt(Top(x),y,Bot(x)).
% input configuration
ckt(Top(C(Tab(0,0,1,1),NIL)),NIL,Bot(C(Tab(0,1,0,1),NIL))).
Equal(and(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4))).
Equal(and(0,0),0).
Equal(and(0,1),0).
Equal(and(1,0),0).
Equal(and(1,1),1).
Equal(and(NIL,x),x).
Equal(or(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4))).
Equal(or(0,0),0).
Equal(or(0,1),1).
Equal(or(1,0),1).
Equal(or(1,1),1).
Equal(or(NIL,x),x).
Equal(not(Tab(x1,x2,x3,x4)),Tab(not(x1),not(x2),not(x3),not(x4))).
Equal(not(0),1).
Equal(not(1),0).
Equal(not(NIL),NIL).
Equal(Tab(0,0,0,0),NIL).
Equal(Tab(1,1,1,1),NIL).
Equal(C(NIL,x),x).
Equal(C(x,C(x,y)),C(x,y)).
SHAR_EOF
if test -f 'interchange.ver1.in'
then
echo shar: over-writing existing file "'interchange.ver1.in'"
fi
cat << \SHAR_EOF > 'interchange.ver1.in'
% problem-set/circuits/interchange.ver1
% created : 08/28/86
% revised : 07/11/88
% description:
%
% Design a circuit with inputs x and y whose outputs are
% y and x, and contains no crossings of wires.
% representation:
%
% We represent the circuit built up so far by
% ckt(Top(x),Middle(y),Bottom(z)), where Top and Bottom are lists
% of outputs, counting outward from the middle.
set(hyper_res).
list(axioms).
% split the middle, keeping the middle
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(and(y,x1),x2)),Middle(y),Bot(C(and(y,z1),z2))).
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(or(y,x1),x2)),Middle(y),Bot(C(or(y,z1),z2))).
% split the middle, omitting the middle
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(and(y,x1),x2)),NIL,Bot(C(and(y,z1),z2))).
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(or(y,x1),x2)),NIL,Bot(C(or(y,z1),z2))).
% join across the middle if it is empty, not keeping the sides
-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) |
ckt(Top(x2),Middle(and(x1,y1)),Bot(y2)).
-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) |
ckt(Top(x2),Middle(or(x1,y1)),Bot(y2)).
% join across the middle, keeping the sides
-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) |
ckt(Top(C(x1,x2)),Middle(and(x1,y1)),Bot(C(y1,y2))).
-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) |
ckt(Top(C(x1,x2)),Middle(or(x1,y1)),Bot(C(y1,y2))).
% join to middle, keeping the sides
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(and(y,x1),C(x1,x2))),NIL,Bot(C(and(y,z1),C(z1,z2)))).
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(or(y,x1),C(x1,x2))),NIL,Bot(C(or(y,z1),C(z1,z2)))).
% split the wire nearest the middle
% this clause is superseded by the previous four
% -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
% ckt(Top(C(x1,C(x1,x2))),Middle(y),Bot(C(z1,C(z1,z2)))).
% join the two wires nearest the middle
-ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) |
ckt(Top(C(and(x1,x2),x3)),Middle(y),Bot(C(and(z1,z2),z3))).
-ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) |
ckt(Top(C(or(x1,x2),x3)),Middle(y),Bot(C(or(z1,z2),z3))).
% put inverter on the middle wire
-ckt(Top(x),Middle(y),Bot(z)) |
ckt(Top(x),Middle(not(y)),Bot(z)).
% put inverter on the adjacent wires
-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |
ckt(Top(C(not(x1),x2)),Middle(y),Bot(C(not(z1),z2))).
-ckt(Top(C(x1,x2)),NIL,Bot(C(z1,z2))) |
ckt(Top(C(not(x1),x2)),NIL,Bot(C(not(z1),z2))).
% cannot construct the answer
-ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))).
% subsumer to get rid of circuits which are the
% same on top and bottom
ckt(Top(x),y,Bot(x)).
end_of_list.
list(sos).
% input configuration
ckt(Top(C(Tab(0,0,1,1),NIL)),NIL,Bot(C(Tab(0,1,0,1),NIL))).
end_of_list.
list(demodulators).
Equal(and(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4))).
Equal(and(0,0),0).
Equal(and(0,1),0).
Equal(and(1,0),0).
Equal(and(1,1),1).
Equal(and(NIL,x),x).
Equal(or(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4))).
Equal(or(0,0),0).
Equal(or(0,1),1).
Equal(or(1,0),1).
Equal(or(1,1),1).
Equal(or(NIL,x),x).
Equal(not(Tab(x1,x2,x3,x4)),Tab(not(x1),not(x2),not(x3),not(x4))).
Equal(not(0),1).
Equal(not(1),0).
Equal(not(NIL),NIL).
Equal(Tab(0,0,0,0),NIL).
Equal(Tab(1,1,1,1),NIL).
Equal(C(NIL,x),x).
Equal(C(x,C(x,y)),C(x,y)).
end_of_list.
SHAR_EOF
if test -f 'interchange.ver1.out'
then
echo shar: over-writing existing file "'interchange.ver1.out'"
fi
cat << \SHAR_EOF > 'interchange.ver1.out'
problem-set/circuits/interchange.ver1.out
created : 08/28/86
revised : 07/11/88
OTTER release 0.9, 19 May 1988
set(hyper_res).
list(axioms).
1 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),x2)),Middle(y),Bot(C(and(y,z1),z2))).
2 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),x2)),Middle(y),Bot(C(or(y,z1),z2))).
3 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),x2)),NIL,Bot(C(and(y,z1),z2))).
4 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),x2)),NIL,Bot(C(or(y,z1),z2))).
5 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(x2),Middle(and(x1,y1)),Bot(y2)).
6 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(x2),Middle(or(x1,y1)),Bot(y2)).
7 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(C(x1,x2)),Middle(and(x1,y1)),Bot(C(y1,y2))).
8 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(C(x1,x2)),Middle(or(x1,y1)),Bot(C(y1,y2))).
9 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),C(x1,x2))),NIL,Bot(C(and(y,z1),C(z1,z2)))).
10 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),C(x1,x2))),NIL,Bot(C(or(y,z1),C(z1,z2)))).
11 -ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) | ckt(Top(C(and(x1,x2),x3)),Middle(y),Bot(C(and(z1,z2),z3))).
12 -ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) | ckt(Top(C(or(x1,x2),x3)),Middle(y),Bot(C(or(z1,z2),z3))).
13 -ckt(Top(x),Middle(y),Bot(z)) | ckt(Top(x),Middle(not(y)),Bot(z)).
14 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(not(x1),x2)),Middle(y),Bot(C(not(z1),z2))).
15 -ckt(Top(C(x1,x2)),NIL,Bot(C(z1,z2))) | ckt(Top(C(not(x1),x2)),NIL,Bot(C(not(z1),z2))).
16 -ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))).
17 ckt(Top(x),y,Bot(x)).
end_of_list.
list(sos).
18 ckt(Top(C(Tab(0,0,1,1),NIL)),NIL,Bot(C(Tab(0,1,0,1),NIL))).
end_of_list.
list(demodulators).
19 Equal(and(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4))).
20 Equal(and(0,0),0).
21 Equal(and(0,1),0).
22 Equal(and(1,0),0).
23 Equal(and(1,1),1).
24 Equal(and(NIL,x),x).
25 Equal(or(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4))).
26 Equal(or(0,0),0).
27 Equal(or(0,1),1).
28 Equal(or(1,0),1).
29 Equal(or(1,1),1).
30 Equal(or(NIL,x),x).
31 Equal(not(Tab(x1,x2,x3,x4)),Tab(not(x1),not(x2),not(x3),not(x4))).
32 Equal(not(0),1).
33 Equal(not(1),0).
34 Equal(not(NIL),NIL).
35 Equal(Tab(0,0,0,0),NIL).
36 Equal(Tab(1,1,1,1),NIL).
37 Equal(C(NIL,x),x).
38 Equal(C(x,C(x,y)),C(x,y)).
end_of_list.
----> UNIT CONFLICT at 10.95 sec ----> 149 (147,16) .
------------ END OF SEARCH ------------
---------------- PROOF ----------------
1 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),x2)),Middle(y),Bot(C(and(y,z1),z2))).
4 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),x2)),NIL,Bot(C(or(y,z1),z2))).
5 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(x2),Middle(and(x1,y1)),Bot(y2)).
8 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(C(x1,x2)),Middle(or(x1,y1)),Bot(C(y1,y2))).
9 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),C(x1,x2))),NIL,Bot(C(and(y,z1),C(z1,z2)))).
14 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(not(x1),x2)),Middle(y),Bot(C(not(z1),z2))).
16 -ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))).
18 ckt(Top(C(Tab(0,0,1,1),NIL)),NIL,Bot(C(Tab(0,1,0,1),NIL))).
19 Equal(and(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4))).
20 Equal(and(0,0),0).
21 Equal(and(0,1),0).
22 Equal(and(1,0),0).
23 Equal(and(1,1),1).
25 Equal(or(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4))).
26 Equal(or(0,0),0).
27 Equal(or(0,1),1).
28 Equal(or(1,0),1).
29 Equal(or(1,1),1).
31 Equal(not(Tab(x1,x2,x3,x4)),Tab(not(x1),not(x2),not(x3),not(x4))).
32 Equal(not(0),1).
33 Equal(not(1),0).
40 (18,8,25,26,27,28,29) ckt(Top(C(Tab(0,0,1,1),NIL)),Middle(Tab(0,1,1,1)),Bot(C(Tab(0,1,0,1),NIL))).
44 (40,14,31,32,32,33,33,31,32,33,32,33) ckt(Top(C(Tab(1,1,0,0),NIL)),Middle(Tab(0,1,1,1)),Bot(C(Tab(1,0,1,0),NIL))).
54 (44,1,19,21,23,22,22,19,21,22,23,22) ckt(Top(C(Tab(0,1,0,0),NIL)),Middle(Tab(0,1,1,1)),Bot(C(Tab(0,0,1,0),NIL))).
72 (54,14,31,32,33,32,32,31,32,32,33,32) ckt(Top(C(Tab(1,0,1,1),NIL)),Middle(Tab(0,1,1,1)),Bot(C(Tab(1,1,0,1),NIL))).
88 (72,9,19,21,22,23,23,19,21,23,22,23) ckt(Top(C(Tab(0,0,1,1),C(Tab(1,0,1,1),NIL))),NIL,Bot(C(Tab(0,1,0,1),C(Tab(1,1,0,1),NIL)))).
141 (88,5,19,20,21,22,23) ckt(Top(C(Tab(1,0,1,1),NIL)),Middle(Tab(0,0,0,1)),Bot(C(Tab(1,1,0,1),NIL))).
142 (141,14,31,33,32,33,33,31,33,33,32,33) ckt(Top(C(Tab(0,1,0,0),NIL)),Middle(Tab(0,0,0,1)),Bot(C(Tab(0,0,1,0),NIL))).
147 (142,4,25,26,27,26,28,25,26,26,27,28) ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))).
149 (147,16) .
--------------- options ---------------
set(hyper_res).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).
clear(binary_res).
clear(UR_res).
clear(para_from).
clear(para_into).
clear(demod_inf).
clear(para_from_left).
clear(para_from_right).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 0).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 4).
assign(fpa_terms, 4).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).
-------------- statistics -------------
clauses input 38
clauses given 59
clauses generated 404
demodulation rewrites 3300
clauses wt or lit delete 0
tautologies deleted 0
clauses forward subsumed 293
(clauses subsumed by sos) 30
unit deletions 0
clauses kept 111
empty clauses 1
factors generated 0
clauses back subsumed 0
clauses not processed 5
----------- times (seconds) -----------
run time 11.19
input time 0.73
binary_res time 0.00
hyper_res time 1.64
UR_res time 0.00
para_into time 0.00
para_from time 0.00
pre_process time 5.81
demod time 3.11
weigh time 0.08
for_sub time 0.54
unit_del time 0.00
post_process time 2.03
back_sub time 1.11
conflict time 0.90
factor time 0.00
FPA build time 0.54
IS build time 0.19
print_cl time 1.63
cl integrate time 0.35
window time 0.00
SHAR_EOF
if test -f 'two.inverter.desc'
then
echo shar: over-writing existing file "'two.inverter.desc'"
fi
cat << \SHAR_EOF > 'two.inverter.desc'
problem-set/circuits/two.inverter.desc
created : 09/02/86
revised : 07/14/88
Natural Language Description:
The files beginning with two_inverter concern the two inverter
puzzle given in the text, "Automated Reasoning" by Larry Wos
et al. (page 186 - 219). It involves 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 specifications:
o1 = not(i1)
o2 = not(i2)
o3 = not(i3)
where, o1, o2, o3 are the outputs and i1, i2, i3 are the
related inputs.
Versions:
two_inverter.ver1 - Nonequality based axioms are used, hyper
resolution is the inference rule, and demodulators
are included.
created by: E. Lusk
verified for ITP: no proof
translated for OTTER by: SLM
verified for OTTER: no proof
two_inverter.ver2 - Nonequality based axioms are used, hyper
resolution is the inference rule, and demodulators
are included.
created by: E. Lusk
verified for ITP: 08/28/86
translated for OTTER by: SLM
verified for OTTER: no proof
SHAR_EOF
if test -f 'two.inverter.val.desc'
then
echo shar: over-writing existing file "'two.inverter.val.desc'"
fi
cat << \SHAR_EOF > 'two.inverter.val.desc'
problem-set/circuits/two.inverter.val.desc
created : 09/03/86
revised : 07/15/88
Natural Language Description:
The files beginning with two_inverter_val concern the validation
of a solution to the two_inverter_val given in the text,
"Automated Reasoning" by Larry Wos et al. (chapter 7).
The puzzle involves 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 specifications:
o1 = not(i1)
o2 = not(i2)
o3 = not(i3)
where, o1, o2, o3 are the outputs and i1, i2, i3 are the
related inputs.
Versions:
two_inverter_val.ver1 - Nonequality based axioms are used, forward
demodulation is the inference rule, and demodulators
are included.
created by: E. Lusk
verified for ITP: no proof
translated for OTTER by: SLM
verified for OTTER: 07/15/88
SHAR_EOF
if test -f 'two.inverter.val.ver1.clauses'
then
echo shar: over-writing existing file "'two.inverter.val.ver1.clauses'"
fi
cat << \SHAR_EOF > 'two.inverter.val.ver1.clauses'
% 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))).
SHAR_EOF
if test -f 'two.inverter.val.ver1.in'
then
echo shar: over-writing existing file "'two.inverter.val.ver1.in'"
fi
cat << \SHAR_EOF > 'two.inverter.val.ver1.in'
% problem-set/circuits/two.inverter.val.ver1
% 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)).
set(demod_inf).
set(sos_fifo).
assign(max_given,3).
assign(demod_limit,3000).
clear(demod_hist).
list(sos).
CKT(o1).
CKT(o2).
CKT(o3).
end_of_list.
list(demodulators).
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))).
end_of_list.
SHAR_EOF
if test -f 'two.inverter.val.ver1.out'
then
echo shar: over-writing existing file "'two.inverter.val.ver1.out'"
fi
cat << \SHAR_EOF > 'two.inverter.val.ver1.out'
problem-set/circuits/two.inverter.val.ver1.out
created : 09/03/86
revised : 07/15/88
OTTER version 0.9, 19 May 1988.
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)).
set(demod_inf).
set(sos_fifo).
assign(max_given,3).
assign(demod_limit,3000).
clear(demod_hist).
list(sos).
1 CKT(o1).
2 CKT(o2).
3 CKT(o3).
end_of_list.
list(demodulators).
lex-dependent demodulator: Equal(eor(x,y),eor(y,x))
lex-dependent demodulator: Equal(eor(y,eor(x,z)),eor(x,eor(y,z)))
lex-dependent demodulator: Equal(and(x,y),and(y,x))
lex-dependent demodulator: Equal(and(y,and(x,z)),and(x,and(y,z)))
4 Equal(o1,13).
5 Equal(o2,17).
6 Equal(o3,5).
7 Equal(a1,and(inv1,i2)).
8 Equal(2,and(inv1,i3)).
9 Equal(3,or(a1,24)).
10 Equal(4,or(15,3)).
11 Equal(5,or(4,21)).
12 Equal(6,and(i1,i2)).
13 Equal(7,and(6,i3)).
14 Equal(8,or(a1,10)).
15 Equal(9,or(8,2)).
16 Equal(10,or(24,7)).
17 Equal(11,or(a1,2)).
18 Equal(12,or(11,16)).
19 Equal(13,or(12,21)).
20 Equal(14,and(i2,i3)).
21 Equal(15,and(inv2,6)).
22 Equal(16,and(14,inv2)).
23 Equal(17,or(18,21)).
24 Equal(18,or(19,25)).
25 Equal(19,and(23,inv2)).
26 Equal(20,or(22,14)).
27 Equal(21,and(inv1,inv2)).
28 Equal(22,or(23,6)).
29 Equal(23,and(i1,i3)).
30 Equal(24,and(i1,inv1)).
31 Equal(25,or(2,24)).
32 Equal(inv1,not(20)).
33 Equal(inv2,not(9)).
34 Equal(eor(0,x),x).
35 Equal(eor(x,0),x).
36 Equal(eor(x,x),0).
37 Equal(eor(x,eor(x,y)),y).
38 Equal(eor(x,y),eor(y,x)).
39 Equal(eor(y,eor(x,z)),eor(x,eor(y,z))).
40 Equal(and(0,x),0).
41 Equal(and(x,0),0).
42 Equal(and(1,x),x).
43 Equal(and(x,1),x).
44 Equal(and(x,x),x).
45 Equal(and(x,and(x,y)),and(x,y)).
46 Equal(and(x,y),and(y,x)).
47 Equal(and(y,and(x,z)),and(x,and(y,z))).
48 Equal(and(x,eor(y,z)),eor(and(x,y),and(x,z))).
49 Equal(not(x),eor(1,x)).
50 Equal(or(x,y),eor(and(x,y),eor(x,y))).
end_of_list.
new given clause: 1 CKT(o1).
** KEPT: 51 (1) CKT(eor(1,i1)).
new given clause: 2 CKT(o2).
** KEPT: 52 (2) CKT(eor(1,i2)).
new given clause: 3 CKT(o3).
** KEPT: 53 (3) CKT(eor(1,i3)).
------------ END OF SEARCH ------------
search stopped by max_given option.
--------------- options ---------------
set(demod_inf).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).
set(sos_fifo).
clear(binary_res).
clear(hyper_res).
clear(UR_res).
clear(para_from).
clear(para_into).
clear(para_from_left).
clear(para_from_right).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(demod_hist).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 3).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 4).
assign(fpa_terms, 4).
assign(demod_limit, 3000).
assign(max_proofs, 1).
assign(neg_weight, 0).
-------------- statistics -------------
clauses input 50
clauses given 3
clauses generated 3
demodulation rewrites 4994
clauses wt or lit delete 0
tautologies deleted 0
clauses forward subsumed 0
(clauses subsumed by sos) 0
unit deletions 0
clauses kept 3
empty clauses 0
factors generated 0
clauses back subsumed 0
clauses not processed 0
----------- times (seconds) -----------
run time 15.93
input time 1.08
binary_res time 0.00
hyper_res time 0.00
UR_res time 0.00
para_into time 0.00
para_from time 0.00
pre_process time 14.68
demod time 14.63
weigh time 0.02
for_sub time 0.00
unit_del time 0.00
post_process time 0.02
back_sub time 0.01
conflict time 0.00
factor time 0.00
FPA build time 0.00
IS build time 0.00
print_cl time 0.18
cl integrate time 0.03
window time 0.00
SHAR_EOF
if test -f 'two.inverter.ver1.clauses'
then
echo shar: over-writing existing file "'two.inverter.ver1.clauses'"
fi
cat << \SHAR_EOF > 'two.inverter.ver1.clauses'
% problem-set/circuits/two.inverter.ver1.clauses
% created : 08/28/86
% revised : 07/14/88
% description:
%
% The two inverter puzzle given in the text, "Automated
% Reasoning" by Larry Wos et al.(page 186 - 219).
%
% To design 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 pages 186 - 219 in the above mentioned text.
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
-OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) |
OUTPUT(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4),
and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),v).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
-OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) |
OUTPUT(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4),
or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),v).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
TEST(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),
not(x7),not(x8),addinv(v,invtab(not(x1),not(x2),not(x3),
not(x4),not(x5),not(x6),not(x7),not(x8))),
makerevlist(l(invtab(not(x1),not(x2),not(x3),not(x4),
not(x5),not(x6),not(x7),not(x8)),v))).
-TEST(x1,x2,x3,x4,x5,x6,x7,x8,v,xrevlist) |
OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
OUTPUT(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7),not(x8),
addinv(v,invtab(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7),
not(x8)))).
OUTPUT(0,0,0,0,1,1,1,1,x).
OUTPUT(0,0,1,1,0,0,1,1,x).
OUTPUT(0,1,0,1,0,1,0,1,x).
-OUTPUT(1,1,1,1,0,0,0,0,v) | -OUTPUT(1,1,0,0,1,1,0,0,v) |
-OUTPUT(1,0,1,0,1,0,1,0,v).
Equal(and(x,0),0).
Equal(and(x,1),x).
Equal(or(x,0),x).
Equal(or(x,1),1).
Equal(not(0),1).
Equal(not(1),0).
% list handling
Equal(addinv(l(x,y),z),l(x,addinv(y,z))).
Equal(addinv(x,y),l(y,x)).
Equal(makerevlist(l(invtab(x000,x001,x010,x011,x100,x101,x110,x111),v)),
lr(possrev(R00m,x000,x001),
lr(possrev(R01m,x010,x011),
lr(possrev(R10m,x100,x101),
lr(possrev(R11m,x110,x111),
lr(possrev(R0m0,x000,x010),
lr(possrev(R0m1,x001,x011),
lr(possrev(R1m0,x100,x110),
lr(possrev(R1m1,x101,x111),
lr(possrev(Rm00,x000,x100),
lr(possrev(Rm01,x001,x101),
lr(possrev(Rm10,x010,x110),
lr(possrev(Rm11,x011,x111),
makerevlist(v)))))))))))))).
Equal(makerevlist(v),end).
Equal(possrev(xname,1,0),xname).
Equal(possrev(xname,0,1),notrev).
Equal(possrev(xname,x,x),notrev).
Equal(lr(notrev,x),x).
Equal(lr(x,lr(y,z)),lr(y,lr(x,z))).
Equal(lr(x,lr(x,y)),lr(x,y)).
SHAR_EOF
if test -f 'two.inverter.ver1.in'
then
echo shar: over-writing existing file "'two.inverter.ver1.in'"
fi
cat << \SHAR_EOF > 'two.inverter.ver1.in'
% problem-set/circuits/two.inverter.ver1
% created : 08/28/86
% revised : 07/14/88
% description:
%
% The two inverter puzzle given in the text, "Automated
% Reasoning" by Larry Wos et al.(page 186 - 219).
%
% To design 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 pages 186 - 219 in the above mentioned text.
set(hyper_res).
list(axioms).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
-OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) |
OUTPUT(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4),
and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),v).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
-OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) |
OUTPUT(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4),
or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),v).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
TEST(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),
not(x7),not(x8),addinv(v,invtab(not(x1),not(x2),not(x3),
not(x4),not(x5),not(x6),not(x7),not(x8))),
makerevlist(l(invtab(not(x1),not(x2),not(x3),not(x4),
not(x5),not(x6),not(x7),not(x8)),v))).
-TEST(x1,x2,x3,x4,x5,x6,x7,x8,v,xrevlist) |
OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v).
% -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
% OUTPUT(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7),not(x8),
% addinv(v,invtab(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7),
% not(x8)))).
end_of_list.
list(sos).
OUTPUT(0,0,0,0,1,1,1,1,x).
OUTPUT(0,0,1,1,0,0,1,1,x).
OUTPUT(0,1,0,1,0,1,0,1,x).
-OUTPUT(1,1,1,1,0,0,0,0,v) | -OUTPUT(1,1,0,0,1,1,0,0,v) |
-OUTPUT(1,0,1,0,1,0,1,0,v).
end_of_list.
list(demodulators).
Equal(and(x,0),0).
Equal(and(x,1),x).
Equal(or(x,0),x).
Equal(or(x,1),1).
Equal(not(0),1).
Equal(not(1),0).
% list handling
Equal(addinv(l(x,y),z),l(x,addinv(y,z))).
Equal(addinv(x,y),l(y,x)).
Equal(makerevlist(l(invtab(x000,x001,x010,x011,x100,x101,x110,x111),v)),
lr(possrev(R00m,x000,x001),
lr(possrev(R01m,x010,x011),
lr(possrev(R10m,x100,x101),
lr(possrev(R11m,x110,x111),
lr(possrev(R0m0,x000,x010),
lr(possrev(R0m1,x001,x011),
lr(possrev(R1m0,x100,x110),
lr(possrev(R1m1,x101,x111),
lr(possrev(Rm00,x000,x100),
lr(possrev(Rm01,x001,x101),
lr(possrev(Rm10,x010,x110),
lr(possrev(Rm11,x011,x111),
makerevlist(v)))))))))))))).
Equal(makerevlist(v),end).
Equal(possrev(xname,1,0),xname).
Equal(possrev(xname,0,1),notrev).
Equal(possrev(xname,x,x),notrev).
Equal(lr(notrev,x),x).
Equal(lr(x,lr(y,z)),lr(y,lr(x,z))).
Equal(lr(x,lr(x,y)),lr(x,y)).
end_of_list.
SHAR_EOF
if test -f 'two.inverter.ver1.out'
then
echo shar: over-writing existing file "'two.inverter.ver1.out'"
fi
cat << \SHAR_EOF > 'two.inverter.ver1.out'
problem-set/circuits/two.inverter.ver1.out
created : 08/28/86
revised : 07/14/88
This version has no output file, because no proof was found.
SHAR_EOF
if test -f 'two.inverter.ver2.clauses'
then
echo shar: over-writing existing file "'two.inverter.ver2.clauses'"
fi
cat << \SHAR_EOF > 'two.inverter.ver2.clauses'
% problem-set/circuits/two.inverter.ver2.clauses
% created : 08/28/86
% revised : 07/14/88
% description:
%
% The two inverter puzzle given in the text, "Automated
% Reasoning" by Larry Wos et al.(page 186 - 219).
%
% To design 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 pages 186 - 219 in the above mentioned text.
-BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
-BOUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) |
BOUTPUT(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4),
and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),v).
-BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
-OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) |
OUTPUT(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4),
or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),v).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
TEST(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),
not(x7),not(x8),addinv(v,invtab(not(x1),not(x2),not(x3),
not(x4),not(x5),not(x6),not(x7),not(x8))),
makerevlist(l(invtab(not(x1),not(x2),not(x3),not(x4),
not(x5),not(x6),not(x7),not(x8)),v))).
-BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v).
-TEST(x1,x2,x3,x4,x5,x6,x7,x8,v,xrevlist) |
BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v).
BOUTPUT(0,0,0,0,1,1,1,1,x).
BOUTPUT(0,0,1,1,0,0,1,1,x).
BOUTPUT(0,1,0,1,0,1,0,1,x).
-OUTPUT(1,1,1,1,0,0,0,0,v) | -OUTPUT(1,1,0,0,1,1,0,0,v) | -OUTPUT(1,0,1,0,1,0,1,0,v).
Equal(and(x,0),0).
Equal(and(x,1),x).
Equal(or(x,0),x).
Equal(or(x,1),1).
Equal(not(0),1).
Equal(not(1),0).
% List handling.
Equal(addinv(l(x,y),z),l(x,addinv(y,z))).
Equal(addinv(x,y),l(y,x)).
Equal(makerevlist(l(invtab(x000,x001,x010,x011,x100,x101,x110,x111),v)),
lr(possrev(R00m,x000,x001),
lr(possrev(R01m,x010,x011),
lr(possrev(R10m,x100,x101),
lr(possrev(R11m,x110,x111),
lr(possrev(R0m0,x000,x010),
lr(possrev(R0m1,x001,x011),
lr(possrev(R1m0,x100,x110),
lr(possrev(R1m1,x101,x111),
lr(possrev(Rm00,x000,x100),
lr(possrev(Rm01,x001,x101),
lr(possrev(Rm10,x010,x110),
lr(possrev(Rm11,x011,x111),
makerevlist(v)))))))))))))).
Equal(makerevlist(v),end).
Equal(possrev(xname,1,0),xname).
Equal(possrev(xname,0,1),notrev).
Equal(possrev(xname,x,x),notrev).
Equal(lr(notrev,x),x).
Equal(lr(x,lr(y,z)),lr(y,lr(x,z))).
Equal(lr(x,lr(x,y)),lr(x,y)).
SHAR_EOF
if test -f 'two.inverter.ver2.in'
then
echo shar: over-writing existing file "'two.inverter.ver2.in'"
fi
cat << \SHAR_EOF > 'two.inverter.ver2.in'
% problem-set/circuits/two.inverter.ver2
% created : 08/28/86
% revised : 07/14/88
% description:
%
% The two inverter puzzle given in the text, "Automated
% Reasoning" by Larry Wos et al.(page 186 - 219).
%
% To design 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 pages 186 - 219 in the above mentioned text.
set(hyper_res).
list(axioms).
-BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
-BOUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) |
BOUTPUT(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4),
and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),v).
-BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
-OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) |
OUTPUT(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4),
or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),v).
-OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
TEST(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),
not(x7),not(x8),addinv(v,invtab(not(x1),not(x2),not(x3),
not(x4),not(x5),not(x6),not(x7),not(x8))),
makerevlist(l(invtab(not(x1),not(x2),not(x3),not(x4),
not(x5),not(x6),not(x7),not(x8)),v))).
-BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) |
OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v).
-TEST(x1,x2,x3,x4,x5,x6,x7,x8,v,xrevlist) |
BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v).
end_of_list.
list(sos).
BOUTPUT(0,0,0,0,1,1,1,1,x).
BOUTPUT(0,0,1,1,0,0,1,1,x).
BOUTPUT(0,1,0,1,0,1,0,1,x).
-OUTPUT(1,1,1,1,0,0,0,0,v) | -OUTPUT(1,1,0,0,1,1,0,0,v) | -OUTPUT(1,0,1,0,1,0,1,0,v).
end_of_list.
list(demodulators).
Equal(and(x,0),0).
Equal(and(x,1),x).
Equal(or(x,0),x).
Equal(or(x,1),1).
Equal(not(0),1).
Equal(not(1),0).
% List handling.
Equal(addinv(l(x,y),z),l(x,addinv(y,z))).
Equal(addinv(x,y),l(y,x)).
Equal(makerevlist(l(invtab(x000,x001,x010,x011,x100,x101,x110,x111),v)),
lr(possrev(R00m,x000,x001),
lr(possrev(R01m,x010,x011),
lr(possrev(R10m,x100,x101),
lr(possrev(R11m,x110,x111),
lr(possrev(R0m0,x000,x010),
lr(possrev(R0m1,x001,x011),
lr(possrev(R1m0,x100,x110),
lr(possrev(R1m1,x101,x111),
lr(possrev(Rm00,x000,x100),
lr(possrev(Rm01,x001,x101),
lr(possrev(Rm10,x010,x110),
lr(possrev(Rm11,x011,x111),
makerevlist(v)))))))))))))).
Equal(makerevlist(v),end).
Equal(possrev(xname,1,0),xname).
Equal(possrev(xname,0,1),notrev).
Equal(possrev(xname,x,x),notrev).
Equal(lr(notrev,x),x).
Equal(lr(x,lr(y,z)),lr(y,lr(x,z))).
Equal(lr(x,lr(x,y)),lr(x,y)).
end_of_list.
SHAR_EOF
if test -f 'two.inverter.ver2.out'
then
echo shar: over-writing existing file "'two.inverter.ver2.out'"
fi
cat << \SHAR_EOF > 'two.inverter.ver2.out'
problem-set/circuits/two.inverter.ver2.out
created : 08/28/86
revised : 07/14/88
This version has no output file, because no proof was found.
SHAR_EOF
# End of shell archive
exit 0