#!/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
# SAMslemma.desc
# SAMslemma.ver1.clauses
# SAMslemma.ver1.in
# SAMslemma.ver1.out
# This archive created: Tue Aug 16 11:17:09 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/algebra/lattices/README
created : 07/15/86
revised : 07/20/88
Contents of 'lattices' :
------------------------
Main File Headings
----------------------------------------------------------------------
README : You are currently here; a description of all the files in
the directory problem-set/algebra/lattices.
SAMslemma : the problem is to prove SAM's lemma, a lemma in modular
lattice theory.
----------------------------------------------------------------------
For each problem, there are several standard files, which include one
probname.desc file and at least one of each of probname.ver#,
probname.ver#.clauses, and probname.ver#.out. These contain the
following:
probname.desc : contains the Natural Language Description of the
problem, where available, as well as complete details on each
formulation and each version.
probname.ver# : 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#, without any strategy; note that comments always are
on lines beginning with a % and that clauses terminate with periods.
probname.ver#.out : contains the output from running probname.ver#
through 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# [ > 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 'SAMslemma.desc'
then
echo shar: over-writing existing file "'SAMslemma.desc'"
fi
cat << \SHAR_EOF > 'SAMslemma.desc'
problem-set/algebra/lattices/SAMslemma.desc
created : 07/09/86
revised : 07/11/88
Natural Language Description:
NOTE : The clauses are described in the form of Algebraic formulae, where:
"v" stands for union
"^" stands for intersection
"'" stands for complement
Sam's Lemma may be stated as follows:
Let L be a modular lattice with 0 and 1. Suppose that
A and B are elements of L such that (A v B) and (A ^ B)
both have not necessarily unique complements.
Then, one can prove
((A v B)' v ((A ^ B)' ^ B)) ^
((A v B)' v ((A ^ B)' ^ A)) = (A v B)'
Axioms to define Sams Lemma
Union of 1 and x is equal to 1 : (1 v X) = 1
Union of x with itself is equal to x : (X v X) = X
Union of 0 and x is equal to x : (0 v X) = X
Intersection of 0 and x is equal to 0 : (0 ^ X) = 0
Intersection of x and itself is equal to x : (X ^ X) = X
Intersection of 1 and x is equal to itself : (1 ^ X) = X
Intersection of x and y , is the same as intersection of y and x.
(X ^ Y) = (Y ^ X)
Union of x and y is the same as union of y and x. (X v Y) = (Y v X)
Union of x with the intersection of x and y is the same as x.
X v (X ^ Y) = X
Intersection of x with the union of x and y is the same as x.
X ^ (X v Y) = X
The operation '^', intersection ,is associative X ^ (Y ^ Z) = (X ^ Y) ^ Z
The operation 'v' is associative X v (Y v Z) = (X v Y) v Z
(X ^ Z) = X implies that (Z ^ (X v Y)) = (X v (Y ^ Z))
(X ^ Z) = Z implies that (X ^ (Y v Z)) = (Z v (X ^ Y))
Negation of Sams Lemma
The following can be obtained by using the fact that
if x v y = 1 and x ^ y = 0 then x = y'
a intersection b is equal to c : a ^ b = c
The union of d and c is equal to 1 : d v c = c1
b union d is equal to e : b v d = e
a union e is equal to 0 : a v e = c0
b union a2 is equal to b2 : b v a2 = b2
a union b2 is equal to c1 : (a v b2) = c1
a union b is equal to c2 : (a v b) = c2
a2 intersection c2 is equal to c0 : a2 ^ c2 = c0
d intersection a is equal to d2 : (d ^ a) = d2
a2 union d2 is equal to e2 : (a2 v d2) = e2
b intersection d is equal to a3 : (b ^ d) = a3
a2 union a3 is equal to b3 : (a2 v a3) = b3
the intersection of b3 and e2 is not equal to a2 : (b3 ^ e2) <> a2
Versions:
SAMslemma.ver1.in: a clause formulation using hyperresolution with the
p-formulation of the problem.
created by : E. Lusk.
verified for ITP : 07/15/86.
translated for OTTER by : caw.
verified for OTTER : 07/01/88.
SHAR_EOF
if test -f 'SAMslemma.ver1.clauses'
then
echo shar: over-writing existing file "'SAMslemma.ver1.clauses'"
fi
cat << \SHAR_EOF > 'SAMslemma.ver1.clauses'
% problem-set/algebra/lattices/SAMslemma.ver1.clauses
% created : 07/09/86
% revised : 07/08/88
% description:
%
% Sam's Lemma may be stated as follows:
%
% Let L be a modular lattice with 0 and 1. Suppose that
% A and B are elements of L such that (A v B) and (A ^ B)
% both have not necessarily unique complements.
%
% Then, one can prove
%
% ((A v B)' v ((A ^ B)' ^ B)) ^
% ((A v B)' v ((A ^ B)' ^ A)) = (A v B)'
% representation:
%
% declare_predicates(3,[MAX,MIN]).
% declare_constants([a,a2,a3,b,b2,b3,c,c2,c3,d,e,d2,e2,a3,b3,c1,c0]).
% declare_variables([x,y,z,x1,y1,z1,xy,yz,xyz]).
%
% Meanings of predicates and functions used in the following clauses :
% MAX(x,y,z) : means z as the union of x and y
% MIN(x,y,z) : means z as the intersection of x and y
% c0 : is the constant used to represent the number '0'
% c1 : is the constant used to represent the number '1'
% Union of 1 and x is equal to 1 : (1 v X) = 1
MAX(c1,x,c1).
% Union of x with itself is equal to x : (X v X) = X
MAX(x,x,x).
% Union of 0 and x is equal to x : (0 v X) = X
MAX(c0,x,x).
% Intersection of 0 and x is equal to 0 : (0 ^ X) = 0
MIN(c0,x,c0).
% Intersection of x and itself is equal to x : (X ^ X) = X
MIN(x,x,x).
% Intersection of 1 and x is equal to itself : (1 ^ X) = X
MIN(c1,x,x).
% Intersection of x and y , is the same as intersection of y and x. %
% (X ^ Y) = (Y ^ X)
-MIN(x,y,z) | MIN(y,x,z).
% Union of x and y is the same as union of y and x. (X v Y) = (Y v X)
-MAX(x,y,z) | MAX(y,x,z).
% Union of x with the intersection of x and y is the same as x.
% X v (X ^ Y) = X
-MIN(x,y,z) | MAX(x,z,x).
% Intersection of x with the union of x and y is the same as x.
% X ^ (X v Y) = X
-MAX(x,y,z) | MIN(x,z,x).
% The operation '^', intersection ,is associative X ^ (Y ^ Z) = (X ^ Y) ^ Z
-MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(x,yz,xyz) | MIN(xy,z,xyz).
-MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(xy,z,xyz) | MIN(x,yz,xyz).
% The operation 'v' is associative X v (Y v Z) = (X v Y) v Z
-MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(x,yz,xyz) | MAX(xy,z,xyz).
-MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(xy,z,xyz) | MAX(x,yz,xyz).
% (X ^ Z) = X implies that (Z ^ (X v Y)) = (X v (Y ^ Z))
-MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MIN(z,x1,z1) | MAX(x,y1,z1).
-MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MAX(x,y1,z1) | MIN(z,x1,z1).
% (X ^ Z) = Z implies that (X ^ (Y v Z)) = (Z v (X ^ Y))
-MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MIN(x,y1,z1) | MAX(z,x1,z1).
-MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MAX(z,x1,z1) | MIN(x,y1,z1).
% Negation of Sams Lemma :
% The following can be obtained by using the fact that
% if x v y = 1 and x ^ y = 0 then x = y'
% a intersection b is equal to c : a ^ b = c
MIN(a,b,c).
% The union of d and c is equal to 1 : d v c = c1
MAX(d,c,c1).
% b union d is equal to e : b v d = e
MIN(b,d,e).
% a union e is equal to 0 : a v e = c0
MIN(a,e,c0).
% b union a2 is equal to b2 : b v a2 = b2
MAX(b,a2,b2).
% a union b2 is equal to c1 : (a v b2) = c1
MAX(a,b2,c1).
% a union b is equal to c2 : (a v b) = c2
MAX(a,b,c2).
% a2 intersection c2 is equal to c0 : a2 ^ c2 = c0
MIN(a2,c2,c0).
% d intersection a is equal to d2 : (d ^ a) = d2
MIN(d,a,d2).
% a2 union d2 is equal to e2 : (a2 v d2) = e2
MAX(a2,d2,e2).
% b intersection d is equal to a3 : (b ^ d) = a3
MIN(d,b,a3).
% a2 union a3 is equal to b3 : (a2 v a3) = b3
MAX(a2,a3,b3).
% the intersection of b3 and e2 is not equal to a2 : (b3 ^ e2) <> a2
-MIN(b3,e2,a2).
SHAR_EOF
if test -f 'SAMslemma.ver1.in'
then
echo shar: over-writing existing file "'SAMslemma.ver1.in'"
fi
cat << \SHAR_EOF > 'SAMslemma.ver1.in'
% problem-set/algebra/lattices/SAMslemma.ver1.in
% created : 07/09/86
% revised : 07/08/88
% description:
%
% Sam's Lemma may be stated as follows:
%
% Let L be a modular lattice with 0 and 1. Suppose that
% A and B are elements of L such that (A v B) and (A ^ B)
% both have not necessarily unique complements.
%
% Then, one can prove
%
% ((A v B)' v ((A ^ B)' ^ B)) ^
% ((A v B)' v ((A ^ B)' ^ A)) = (A v B)'
% representation:
%
% declare_predicates(3,[MAX,MIN]).
% declare_constants([a,a2,a3,b,b2,b3,c,c2,c3,d,e,d2,e2,a3,b3,c1,c0]).
% declare_variables([x,y,z,x1,y1,z1,xy,yz,xyz]).
%
% Meanings of predicates and functions used in the following clauses :
% MAX(x,y,z) : means z as the union of x and y
% MIN(x,y,z) : means z as the intersection of x and y
% c0 : is the constant used to represent the number '0'
% c1 : is the constant used to represent the number '1'
set(hyper_res).
clear(back_sub).
list(axioms).
% Union of 1 and x is equal to 1 : (1 v X) = 1
MAX(c1,x,c1).
% Union of x with itself is equal to x : (X v X) = X
MAX(x,x,x).
% Union of 0 and x is equal to x : (0 v X) = X
MAX(c0,x,x).
% Intersection of 0 and x is equal to 0 : (0 ^ X) = 0
MIN(c0,x,c0).
% Intersection of x and itself is equal to x : (X ^ X) = X
MIN(x,x,x).
% Intersection of 1 and x is equal to itself : (1 ^ X) = X
MIN(c1,x,x).
% Intersection of x and y , is the same as intersection of y and x. %
% (X ^ Y) = (Y ^ X)
-MIN(x,y,z) | MIN(y,x,z).
% Union of x and y is the same as union of y and x. (X v Y) = (Y v X)
-MAX(x,y,z) | MAX(y,x,z).
% Union of x with the intersection of x and y is the same as x.
% X v (X ^ Y) = X
-MIN(x,y,z) | MAX(x,z,x).
% Intersection of x with the union of x and y is the same as x.
% X ^ (X v Y) = X
-MAX(x,y,z) | MIN(x,z,x).
% The operation '^', intersection ,is associative X ^ (Y ^ Z) = (X ^ Y) ^ Z
-MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(x,yz,xyz) | MIN(xy,z,xyz).
-MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(xy,z,xyz) | MIN(x,yz,xyz).
% The operation 'v' is associative X v (Y v Z) = (X v Y) v Z
-MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(x,yz,xyz) | MAX(xy,z,xyz).
-MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(xy,z,xyz) | MAX(x,yz,xyz).
% (X ^ Z) = X implies that (Z ^ (X v Y)) = (X v (Y ^ Z))
-MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MIN(z,x1,z1) | MAX(x,y1,z1).
-MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MAX(x,y1,z1) | MIN(z,x1,z1).
% (X ^ Z) = Z implies that (X ^ (Y v Z)) = (Z v (X ^ Y))
-MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MIN(x,y1,z1) | MAX(z,x1,z1).
-MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MAX(z,x1,z1) | MIN(x,y1,z1).
end_of_list.
list(sos).
% Negation of Sams Lemma :
% The following can be obtained by using the fact that
% if x v y = 1 and x ^ y = 0 then x = y'
% a intersection b is equal to c : a ^ b = c
MIN(a,b,c).
% The union of d and c is equal to 1 : d v c = c1
MAX(d,c,c1).
% b union d is equal to e : b v d = e
MIN(b,d,e).
% a union e is equal to 0 : a v e = c0
MIN(a,e,c0).
% b union a2 is equal to b2 : b v a2 = b2
MAX(b,a2,b2).
% a union b2 is equal to c1 : (a v b2) = c1
MAX(a,b2,c1).
% a union b is equal to c2 : (a v b) = c2
MAX(a,b,c2).
% a2 intersection c2 is equal to c0 : a2 ^ c2 = c0
MIN(a2,c2,c0).
% d intersection a is equal to d2 : (d ^ a) = d2
MIN(d,a,d2).
% a2 union d2 is equal to e2 : (a2 v d2) = e2
MAX(a2,d2,e2).
% b intersection d is equal to a3 : (b ^ d) = a3
MIN(d,b,a3).
% a2 union a3 is equal to b3 : (a2 v a3) = b3
MAX(a2,a3,b3).
% the intersection of b3 and e2 is not equal to a2 : (b3 ^ e2) <> a2
-MIN(b3,e2,a2).
end_of_list.
SHAR_EOF
if test -f 'SAMslemma.ver1.out'
then
echo shar: over-writing existing file "'SAMslemma.ver1.out'"
fi
cat << \SHAR_EOF > 'SAMslemma.ver1.out'
% problem-set/lattices/SAMslemma.ver1.out
% created : 07/09/86
% revised : 07/08/88
OTTER release 0.9, 19 May 1988
set(hyper_res).
clear(back_sub).
list(axioms).
1 MAX(c1,x,c1).
2 MAX(x,x,x).
3 MAX(c0,x,x).
4 MIN(c0,x,c0).
5 MIN(x,x,x).
6 MIN(c1,x,x).
7 -MIN(x,y,z) | MIN(y,x,z).
8 -MAX(x,y,z) | MAX(y,x,z).
9 -MIN(x,y,z) | MAX(x,z,x).
10 -MAX(x,y,z) | MIN(x,z,x).
11 -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(x,yz,xyz) | MIN(xy,z,xyz).
12 -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(xy,z,xyz) | MIN(x,yz,xyz).
13 -MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(x,yz,xyz) | MAX(xy,z,xyz).
14 -MAX(x,y,xy) | -MAX(y,z,yz) | -MAX(xy,z,xyz) | MAX(x,yz,xyz).
15 -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MIN(z,x1,z1) | MAX(x,y1,z1).
16 -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MAX(x,y1,z1) | MIN(z,x1,z1).
17 -MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MIN(x,y1,z1) | MAX(z,x1,z1).
18 -MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MAX(z,x1,z1) | MIN(x,y1,z1).
end_of_list.
list(sos).
19 MIN(a,b,c).
20 MAX(d,c,c1).
21 MIN(b,d,e).
22 MIN(a,e,c0).
23 MAX(b,a2,b2).
24 MAX(a,b2,c1).
25 MAX(a,b,c2).
26 MIN(a2,c2,c0).
27 MIN(d,a,d2).
28 MAX(a2,d2,e2).
29 MIN(d,b,a3).
30 MAX(a2,a3,b3).
31 -MIN(b3,e2,a2).
end_of_list.
---------------- PROOF ----------------
3 MAX(c0,x,x).
4 MIN(c0,x,c0).
5 MIN(x,x,x).
6 MIN(c1,x,x).
9 -MIN(x,y,z) | MAX(x,z,x).
10 -MAX(x,y,z) | MIN(x,z,x).
11 -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(x,yz,xyz) | MIN(xy,z,xyz).
12 -MIN(x,y,xy) | -MIN(y,z,yz) | -MIN(xy,z,xyz) | MIN(x,yz,xyz).
15 -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MIN(z,x1,z1) | MAX(x,y1,z1).
16 -MIN(x,z,x) | -MAX(x,y,x1) | -MIN(y,z,y1) | -MAX(x,y1,z1) | MIN(z,x1,z1).
17 -MIN(x,z,z) | -MAX(y,z,y1) | -MIN(x,y,x1) | -MIN(x,y1,z1) | MAX(z,x1,z1).
21 MIN(b,d,e).
22 MIN(a,e,c0).
25 MAX(a,b,c2).
26 MIN(a2,c2,c0).
27 MIN(d,a,d2).
28 MAX(a2,d2,e2).
29 MIN(d,b,a3).
30 MAX(a2,a3,b3).
31 -MIN(b3,e2,a2).
39 (21,16,4,3,3) MIN(d,b,e).
54 (25,17,6,6,6) MAX(b,a,c2).
58 (25,10) MIN(a,c2,a).
61 (26,9) MAX(a2,c0,a2).
62 (27,16,4,3,3) MIN(a,d,d2).
72 (29,15,4,3,21) MAX(c0,a3,e).
76 (30,17,6,6,6) MAX(a3,a2,b3).
79 (30,10) MIN(a2,b3,a2).
89 (39,12,5,29) MIN(d,a3,e).
90 (39,12,6,29) MIN(c1,e,a3).
94 (39,11,5,29) MIN(e,b,a3).
133 (54,10) MIN(b,c2,b).
140 (58,11,27,27) MIN(d2,c2,d2).
196 (89,11,62,22) MIN(d2,a3,c0).
197 (90,17,6,72,6) MAX(a3,c0,a3).
224 (133,11,94,94) MIN(a3,c2,a3).
279 (224,16,76,26,197) MIN(c2,b3,a3).
307 (279,11,140,196) MIN(d2,b3,c0).
330 (307,16,79,28,61) MIN(b3,e2,a2).
331 (330,31) .
--------------- options ---------------
set(hyper_res).
set(demod_hist).
set(for_sub).
set(print_kept).
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(back_sub).
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 31
clauses given 289
clauses generated 20182
demodulation rewrites 0
clauses wt or lit delete 0
tautologies deleted 0
clauses forward subsumed 19882
(clauses subsumed by sos) 2575
unit deletions 0
clauses kept 300
empty clauses 1
factors generated 0
clauses back subsumed 0
clauses not processed 2
----------- times (seconds) -----------
run time 223.49
input time 0.41
binary_res time 0.00
hyper_res time 172.37
UR_res time 0.00
para_into time 0.00
para_from time 0.00
pre_process time 45.10
demod time 0.00
weigh time 0.06
for_sub time 36.20
unit_del time 0.00
post_process time 1.28
back_sub time 0.00
conflict time 1.22
factor time 0.00
FPA build time 0.40
IS build time 0.13
print_cl time 1.62
cl integrate time 0.15
window time 0.00
SHAR_EOF
# End of shell archive
exit 0