#!/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
# thf1.desc
# thf1.ver1.clauses
# thf1.ver1.in
# thf1.ver1.out
# thf2.desc
# thf2.ver1.clauses
# thf2.ver1.in
# thf2.ver1.out
# thf3.desc
# thf3.ver1.clauses
# thf3.ver1.in
# thf3.ver1.out
# thf4.desc
# thf4.ver1.clauses
# thf4.ver1.in
# thf4.ver1.out
# thf5.desc
# thf5.ver1.clauses
# thf5.ver1.in
# thf5.ver1.out
# thf6.desc
# thf6.ver1.clauses
# thf6.ver1.in
# thf6.ver1.out
# thf7.desc
# thf7.ver1.clauses
# thf7.ver1.in
# thf7.ver1.out
# This archive created: Tue Aug 16 11:21:07 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/pelletier/full.predicate/README
created : 07/25/86
revised : 07/28/88
Contents of 'full.predicate' :
---------------------------
Main File Headings
----------------------------------------------------------------------
README : You are currently here; a description of all the files in
the directory problem-set/.
th.f1 : Problem #38 from the Pelletier paper, in full predicate logic.
The problem is only represented in clause form.
th.f2 : Problem #40 from the Pelletier paper.
If there were a 'anti-Russell set' then not every set has a
complement.
th.f3 : Problem #41 from the Pelletier paper.
The 'restricted comprehension axiom' says: given a set z,
there is a set all of whose members are drawn from z and
which satisfy some property. If there were a universal set
then the Russell set could be formed, using this axiom. So
given the appropriate instance of this axiom, there is no
universal set.
th.f4 : Problem #42 from the Pelletier paper.
A set is 'circular' if it is a member of another set which
in turn is a member of the original. Intuitively all sets
are non-circular. Prove there is no set of noncircular sets.
th.f5 : Problem #43 from the Pelletier paper, this problem is given
by deChampeaux, 1979.
Define set equality ('Q') as having exactly the same members.
Prove set equality is symmetric.
th.f6 : Problem #45 from the Pelletier paper, in full predicate logic.
th.f7 : Problem #46 from the Pelletier paper, in full predicate logic.
----------------------------------------------------------------------
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, as well as 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 % and that clauses terminate with periods.
probname.ver#.out : contains the output from running probname.ver#.in
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#.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 'thf1.desc'
then
echo shar: over-writing existing file "'thf1.desc'"
fi
cat << \SHAR_EOF > 'thf1.desc'
problem-set/pelletier/full.predicate/thf1.desc
created : 07/25/86
revised : 07/28/88
Natural Language Description:
Full Predicate Logic (without Identity and Functions).
This is problem#38 from "Seventy-five Problems for Testing
Automated Theorem Provers", paper by Francis Jeffry Pelletier.
{(Ax)[Pa & (Px -> (Ey)(Py & Rxy)) -> (Ez)(Ew)(Pz & Rxw & Rwz)] <->
(Ax)[-Pa + Px + (Ez)(Ew)Pz & Rxw & Rwz)) &
(-Pa + -(Ey)(Py & Rxy) + (Ez)(Ew)(Pz & Rxw & Rwz))]}
Versions:
thf1.desc - declarative representation.
created by : From Pelletier paper, 1986.
verified for ITP : untested, 07/25/86
translated for OTTER by : K.R.
verified for OTTER : untested
SHAR_EOF
if test -f 'thf1.ver1.clauses'
then
echo shar: over-writing existing file "'thf1.ver1.clauses'"
fi
cat << \SHAR_EOF > 'thf1.ver1.clauses'
% problem-set/pelletier/full.predicate/thf1.ver1.clauses
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identity and Functions).
% This is problem#38 from "Seventy-five Problems for Testing
% Automated Theorem Provers", paper by Francis Jeffry Pelletier.
% {(Ax)[Pa & (Px -> (Ey)(Py & Rxy)) -> (Ez)(Ew)(Pz & Rxw & Rwz)] <->
% (Ax)[-Pa + Px + (Ez)(Ew)Pz & Rxw & Rwz)) &
% (-Pa + -(Ey)(Py & Rxy) + (Ez)(Ew)(Pz & Rxw & Rwz))]}
% representation:
%
% Declarative version
-P(a) | P(xx1) | P(f1(xx1)) | -P(a) | P(xx2) | P(f3(xx2)).
-P(a) | P(xx3) | P(f1(xx3)) | -P(a) | P(xx4) | R(xx4,f4(xx4)).
-P(a) | P(xx5) | P(f1(xx5)) | -P(a) | P(xx6) | R(f4(xx6),f3(xx6)).
-P(a) | P(xx7) | P(f1(xx7)) | -P(a) | P(xx8) | -P(a) | -P(xx9) | -R(xx8,xx9) | P(f5(xx8)).
-P(a) | P(xx10) | P(f1(xx10)) | -P(a) | P(xx11) | -P(a) | -P(xx12) | -R(xx11,xx12) | R(xx11,f6(xx11)).
-P(a) | P(xx13) | P(f1(xx13)) | -P(a) | P(xx14) | -P(a) | -P(xx15) | -R(xx14,xx15) | R(f6(xx14),f5(xx14)).
-P(a) | P(xx16) | R(xx16,f2(xx16)) | -P(a) | P(xx17) | P(f3(xx17)).
-P(a) | P(xx18) | R(xx18,f2(xx18)) | -P(a) | P(xx19) | R(xx19,f4(xx19)).
-P(a) | P(xx20) | R(xx20,f2(xx20)) | -P(a) | P(xx21) | R(f4(xx21),f3(xx21)).
-P(a) | P(xx22) | R(xx22,f2(xx22)) | -P(a) | P(xx23) | -P(a) | -P(xx24) | -R(xx23,xx24) | P(f5(xx23)).
-P(a) | P(xx25) | R(xx25,f2(xx25)) | -P(a) | P(xx26) | -P(a) | -P(xx27) | -R(xx26,xx27) | R(xx26,f6(xx26)).
-P(a) | P(xx28) | R(xx28,f2(xx28)) | -P(a) | P(xx29) | -P(a) | -P(xx30) | -R(xx29,xx30) | R(f6(xx29),f5(xx29)).
-P(a) | P(xx31) | R(f2(xx31),f1(xx31)) | -P(a) | P(xx32) | P(f3(xx32)).
-P(a) | P(xx33) | R(f2(xx33),f1(xx33)) | -P(a) | P(xx34) | R(xx34,f4(xx34)).
-P(a) | P(xx35) | R(f2(xx35),f1(xx35)) | -P(a) | P(xx36) | R(f4(xx36),f3(xx36)).
-P(a) | P(xx37) | R(f2(xx37),f1(xx37)) | -P(a) | P(xx38) | -P(a) | -P(xx39) | -R(xx38,xx39) | P(f5(xx38)).
-P(a) | P(xx40) | R(f2(xx40),f1(xx40)) | -P(a) | P(xx41) | -P(a) | -P(xx42) | -R(xx41,xx42) | R(xx41,f6(xx41)).
-P(a) | P(xx43) | R(f2(xx43),f1(xx43)) | -P(a) | P(xx44) | -P(a) | -P(xx45) | -R(xx44,xx45) | R(f6(xx44),f5(xx44)).
-P(a) | -P(xx46) | -R(xx47,xx46) | P(f1(xx47)) | -P(a) | P(xx48) | P(f3(xx48)).
-P(a) | -P(xx49) | -R(xx50,xx49) | P(f1(xx50)) | -P(a) | P(xx51) | R(xx51,f4(xx51)).
-P(a) | -P(xx52) | -R(xx53,xx52) | P(f1(xx53)) | -P(a) | P(xx54) | R(f4(xx54),f3(xx54)).
-P(a) | -P(xx55) | -R(xx56,xx55) | P(f1(xx56)) | -P(a) | P(xx57) | -P(a) | -P(xx58) | -R(xx57,xx58) | P(f5(xx57)).
-P(a) | -P(xx59) | -R(xx60,xx59) | P(f1(xx60)) | -P(a) | P(xx61) | -P(a) | -P(xx62) | -R(xx61,xx62) | R(xx61,f6(xx61)).
-P(a) | -P(xx63) | -R(xx64,xx63) | P(f1(xx64)) | -P(a) | P(xx65) | -P(a) | -P(xx66) | -R(xx65,xx66) | R(f6(xx65),f5(xx65)).
-P(a) | -P(xx67) | -R(xx68,xx67) | R(xx68,f2(xx68)) | -P(a) | P(xx69) | P(f3(xx69)).
-P(a) | -P(xx70) | -R(xx71,xx70) | R(xx71,f2(xx71)) | -P(a) | P(xx72) | R(xx72,f4(xx72)).
-P(a) | -P(xx73) | -R(xx74,xx73) | R(xx74,f2(xx74)) | -P(a) | P(xx75) | R(f4(xx75),f3(xx75)).
-P(a) | -P(xx76) | -R(xx77,xx76) | R(xx77,f2(xx77)) | -P(a) | P(xx78) | -P(a) | -P(xx79) | -R(xx78,xx79) | P(f5(xx78)).
-P(a) | -P(xx80) | -R(xx81,xx80) | R(xx81,f2(xx81)) | -P(a) | P(xx82) | -P(a) | -P(xx83) | -R(xx82,xx83) | R(xx82,f6(xx82)).
-P(a) | -P(xx84) | -R(xx85,xx84) | R(xx85,f2(xx85)) | -P(a) | P(xx86) | -P(a) | -P(xx87) | -R(xx86,xx87) | R(f6(xx86),f5(xx86)).
-P(a) | -P(xx88) | -R(xx89,xx88) | R(f2(xx89),f1(xx89)) | -P(a) | P(xx90) | P(f3(xx90)).
-P(a) | -P(xx91) | -R(xx92,xx91) | R(f2(xx92),f1(xx92)) | -P(a) | P(xx93) | R(xx93,f4(xx93)).
-P(a) | -P(xx94) | -R(xx95,xx94) | R(f2(xx95),f1(xx95)) | -P(a) | P(xx96) | R(f4(xx96),f3(xx96)).
-P(a) | -P(xx97) | -R(xx98,xx97) | R(f2(xx98),f1(xx98)) | -P(a) | P(xx99) | -P(a) | -P(xx100) | -R(xx99,xx100) | P(f5(xx99)).
-P(a) | -P(xx101) | -R(xx102,xx101) | R(f2(xx102),f1(xx102)) | -P(a) | P(xx103) | -P(a) | -P(xx104) | -R(xx103,xx104) | R(xx103,f6(xx103)).
-P(a) | -P(xx105) | -R(xx106,xx105) | R(f2(xx106),f1(xx106)) | -P(a) | P(xx107) | -P(a) | -P(xx108) | -R(xx107,xx108) | R(f6(xx107),f5(xx107)).
P(a) | P(a).
P(a) | -P(f9).
P(a) | -P(xx109) | -R(f9,xx110) | -R(xx110,xx109) | P(a).
P(a) | -P(xx111) | -R(f9,xx112) | -R(xx112,xx111) | P(f10).
P(a) | -P(xx113) | -R(f9,xx114) | -R(xx114,xx113) | R(f9,f10).
P(a) | -P(xx115) | -R(f9,xx116) | -R(xx116,xx115) | -P(xx117) | -R(f9,xx118) | -R(xx118,xx117).
-P(f7) | P(f8) | P(a).
-P(f7) | P(f8) | -P(f9).
-P(f7) | P(f8) | -P(xx119) | -R(f9,xx120) | -R(xx120,xx119) | P(a).
-P(f7) | P(f8) | -P(xx121) | -R(f9,xx122) | -R(xx122,xx121) | P(f10).
-P(f7) | P(f8) | -P(xx123) | -R(f9,xx124) | -R(xx124,xx123) | R(f9,f10).
-P(f7) | P(f8) | -P(xx125) | -R(f9,xx126) | -R(xx126,xx125) | -P(xx127) | -R(f9,xx128) | -R(xx128,xx127).
-P(f7) | R(f7,f8) | P(a).
-P(f7) | R(f7,f8) | -P(f9).
-P(f7) | R(f7,f8) | -P(xx129) | -R(f9,xx130) | -R(xx130,xx129) | P(a).
-P(f7) | R(f7,f8) | -P(xx131) | -R(f9,xx132) | -R(xx132,xx131) | P(f10).
-P(f7) | R(f7,f8) | -P(xx133) | -R(f9,xx134) | -R(xx134,xx133) | R(f9,f10).
-P(f7) | R(f7,f8) | -P(xx135) | -R(f9,xx136) | -R(xx136,xx135) | -P(xx137) | -R(f9,xx138) | -R(xx138,xx137).
-P(xx139) | -R(f7,xx140) | -R(xx140,xx139) | P(a).
-P(xx141) | -R(f7,xx142) | -R(xx142,xx141) | -P(f9).
-P(xx143) | -R(f7,xx144) | -R(xx144,xx143) | -P(xx145) | -R(f9,xx146) | -R(xx146,xx145) | P(a).
-P(xx147) | -R(f7,xx148) | -R(xx148,xx147) | -P(xx149) | -R(f9,xx150) | -R(xx150,xx149) | P(f10).
-P(xx151) | -R(f7,xx152) | -R(xx152,xx151) | -P(xx153) | -R(f9,xx154) | -R(xx154,xx153) | R(f9,f10).
-P(xx155) | -R(f7,xx156) | -R(xx156,xx155) | -P(xx157) | -R(f9,xx158) | -R(xx158,xx157) | -P(xx159) | -R(f9,xx160) | -R(xx160,xx159).
SHAR_EOF
if test -f 'thf1.ver1.in'
then
echo shar: over-writing existing file "'thf1.ver1.in'"
fi
cat << \SHAR_EOF > 'thf1.ver1.in'
% problem-set/pelletier/full.predicate/thf1.ver1.in
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identity and Functions).
% This is problem#38 from "Seventy-five Problems for Testing
% Automated Theorem Provers", paper by Francis Jeffry Pelletier.
% {(Ax)[Pa & (Px -> (Ey)(Py & Rxy)) -> (Ez)(Ew)(Pz & Rxw & Rwz)] <->
% (Ax)[-Pa + Px + (Ez)(Ew)Pz & Rxw & Rwz)) &
% (-Pa + -(Ey)(Py & Rxy) + (Ez)(Ew)(Pz & Rxw & Rwz))]}
% representation:
%
% Declarative version
set(hyper_res).
list(sos).
-P(a) | P(xx1) | P(f1(xx1)) | -P(a) | P(xx2) | P(f3(xx2)).
-P(a) | P(xx3) | P(f1(xx3)) | -P(a) | P(xx4) | R(xx4,f4(xx4)).
-P(a) | P(xx5) | P(f1(xx5)) | -P(a) | P(xx6) | R(f4(xx6),f3(xx6)).
-P(a) | P(xx7) | P(f1(xx7)) | -P(a) | P(xx8) | -P(a) | -P(xx9) | -R(xx8,xx9) | P(f5(xx8)).
-P(a) | P(xx10) | P(f1(xx10)) | -P(a) | P(xx11) | -P(a) | -P(xx12) | -R(xx11,xx12) | R(xx11,f6(xx11)).
-P(a) | P(xx13) | P(f1(xx13)) | -P(a) | P(xx14) | -P(a) | -P(xx15) | -R(xx14,xx15) | R(f6(xx14),f5(xx14)).
-P(a) | P(xx16) | R(xx16,f2(xx16)) | -P(a) | P(xx17) | P(f3(xx17)).
-P(a) | P(xx18) | R(xx18,f2(xx18)) | -P(a) | P(xx19) | R(xx19,f4(xx19)).
-P(a) | P(xx20) | R(xx20,f2(xx20)) | -P(a) | P(xx21) | R(f4(xx21),f3(xx21)).
-P(a) | P(xx22) | R(xx22,f2(xx22)) | -P(a) | P(xx23) | -P(a) | -P(xx24) | -R(xx23,xx24) | P(f5(xx23)).
-P(a) | P(xx25) | R(xx25,f2(xx25)) | -P(a) | P(xx26) | -P(a) | -P(xx27) | -R(xx26,xx27) | R(xx26,f6(xx26)).
-P(a) | P(xx28) | R(xx28,f2(xx28)) | -P(a) | P(xx29) | -P(a) | -P(xx30) | -R(xx29,xx30) | R(f6(xx29),f5(xx29)).
-P(a) | P(xx31) | R(f2(xx31),f1(xx31)) | -P(a) | P(xx32) | P(f3(xx32)).
-P(a) | P(xx33) | R(f2(xx33),f1(xx33)) | -P(a) | P(xx34) | R(xx34,f4(xx34)).
-P(a) | P(xx35) | R(f2(xx35),f1(xx35)) | -P(a) | P(xx36) | R(f4(xx36),f3(xx36)).
-P(a) | P(xx37) | R(f2(xx37),f1(xx37)) | -P(a) | P(xx38) | -P(a) | -P(xx39) | -R(xx38,xx39) | P(f5(xx38)).
-P(a) | P(xx40) | R(f2(xx40),f1(xx40)) | -P(a) | P(xx41) | -P(a) | -P(xx42) | -R(xx41,xx42) | R(xx41,f6(xx41)).
-P(a) | P(xx43) | R(f2(xx43),f1(xx43)) | -P(a) | P(xx44) | -P(a) | -P(xx45) | -R(xx44,xx45) | R(f6(xx44),f5(xx44)).
-P(a) | -P(xx46) | -R(xx47,xx46) | P(f1(xx47)) | -P(a) | P(xx48) | P(f3(xx48)).
-P(a) | -P(xx49) | -R(xx50,xx49) | P(f1(xx50)) | -P(a) | P(xx51) | R(xx51,f4(xx51)).
-P(a) | -P(xx52) | -R(xx53,xx52) | P(f1(xx53)) | -P(a) | P(xx54) | R(f4(xx54),f3(xx54)).
-P(a) | -P(xx55) | -R(xx56,xx55) | P(f1(xx56)) | -P(a) | P(xx57) | -P(a) | -P(xx58) | -R(xx57,xx58) | P(f5(xx57)).
-P(a) | -P(xx59) | -R(xx60,xx59) | P(f1(xx60)) | -P(a) | P(xx61) | -P(a) | -P(xx62) | -R(xx61,xx62) | R(xx61,f6(xx61)).
-P(a) | -P(xx63) | -R(xx64,xx63) | P(f1(xx64)) | -P(a) | P(xx65) | -P(a) | -P(xx66) | -R(xx65,xx66) | R(f6(xx65),f5(xx65)).
-P(a) | -P(xx67) | -R(xx68,xx67) | R(xx68,f2(xx68)) | -P(a) | P(xx69) | P(f3(xx69)).
-P(a) | -P(xx70) | -R(xx71,xx70) | R(xx71,f2(xx71)) | -P(a) | P(xx72) | R(xx72,f4(xx72)).
-P(a) | -P(xx73) | -R(xx74,xx73) | R(xx74,f2(xx74)) | -P(a) | P(xx75) | R(f4(xx75),f3(xx75)).
-P(a) | -P(xx76) | -R(xx77,xx76) | R(xx77,f2(xx77)) | -P(a) | P(xx78) | -P(a) | -P(xx79) | -R(xx78,xx79) | P(f5(xx78)).
-P(a) | -P(xx80) | -R(xx81,xx80) | R(xx81,f2(xx81)) | -P(a) | P(xx82) | -P(a) | -P(xx83) | -R(xx82,xx83) | R(xx82,f6(xx82)).
-P(a) | -P(xx84) | -R(xx85,xx84) | R(xx85,f2(xx85)) | -P(a) | P(xx86) | -P(a) | -P(xx87) | -R(xx86,xx87) | R(f6(xx86),f5(xx86)).
-P(a) | -P(xx88) | -R(xx89,xx88) | R(f2(xx89),f1(xx89)) | -P(a) | P(xx90) | P(f3(xx90)).
-P(a) | -P(xx91) | -R(xx92,xx91) | R(f2(xx92),f1(xx92)) | -P(a) | P(xx93) | R(xx93,f4(xx93)).
-P(a) | -P(xx94) | -R(xx95,xx94) | R(f2(xx95),f1(xx95)) | -P(a) | P(xx96) | R(f4(xx96),f3(xx96)).
-P(a) | -P(xx97) | -R(xx98,xx97) | R(f2(xx98),f1(xx98)) | -P(a) | P(xx99) | -P(a) | -P(xx100) | -R(xx99,xx100) | P(f5(xx99)).
-P(a) | -P(xx101) | -R(xx102,xx101) | R(f2(xx102),f1(xx102)) | -P(a) | P(xx103) | -P(a) | -P(xx104) | -R(xx103,xx104) | R(xx103,f6(xx103)).
-P(a) | -P(xx105) | -R(xx106,xx105) | R(f2(xx106),f1(xx106)) | -P(a) | P(xx107) | -P(a) | -P(xx108) | -R(xx107,xx108) | R(f6(xx107),f5(xx107)).
P(a) | P(a).
P(a) | -P(f9).
P(a) | -P(xx109) | -R(f9,xx110) | -R(xx110,xx109) | P(a).
P(a) | -P(xx111) | -R(f9,xx112) | -R(xx112,xx111) | P(f10).
P(a) | -P(xx113) | -R(f9,xx114) | -R(xx114,xx113) | R(f9,f10).
P(a) | -P(xx115) | -R(f9,xx116) | -R(xx116,xx115) | -P(xx117) | -R(f9,xx118) | -R(xx118,xx117).
-P(f7) | P(f8) | P(a).
-P(f7) | P(f8) | -P(f9).
-P(f7) | P(f8) | -P(xx119) | -R(f9,xx120) | -R(xx120,xx119) | P(a).
-P(f7) | P(f8) | -P(xx121) | -R(f9,xx122) | -R(xx122,xx121) | P(f10).
-P(f7) | P(f8) | -P(xx123) | -R(f9,xx124) | -R(xx124,xx123) | R(f9,f10).
-P(f7) | P(f8) | -P(xx125) | -R(f9,xx126) | -R(xx126,xx125) | -P(xx127) | -R(f9,xx128) | -R(xx128,xx127).
-P(f7) | R(f7,f8) | P(a).
-P(f7) | R(f7,f8) | -P(f9).
-P(f7) | R(f7,f8) | -P(xx129) | -R(f9,xx130) | -R(xx130,xx129) | P(a).
-P(f7) | R(f7,f8) | -P(xx131) | -R(f9,xx132) | -R(xx132,xx131) | P(f10).
-P(f7) | R(f7,f8) | -P(xx133) | -R(f9,xx134) | -R(xx134,xx133) | R(f9,f10).
-P(f7) | R(f7,f8) | -P(xx135) | -R(f9,xx136) | -R(xx136,xx135) | -P(xx137) | -R(f9,xx138) | -R(xx138,xx137).
-P(xx139) | -R(f7,xx140) | -R(xx140,xx139) | P(a).
-P(xx141) | -R(f7,xx142) | -R(xx142,xx141) | -P(f9).
-P(xx143) | -R(f7,xx144) | -R(xx144,xx143) | -P(xx145) | -R(f9,xx146) | -R(xx146,xx145) | P(a).
-P(xx147) | -R(f7,xx148) | -R(xx148,xx147) | -P(xx149) | -R(f9,xx150) | -R(xx150,xx149) | P(f10).
-P(xx151) | -R(f7,xx152) | -R(xx152,xx151) | -P(xx153) | -R(f9,xx154) | -R(xx154,xx153) | R(f9,f10).
-P(xx155) | -R(f7,xx156) | -R(xx156,xx155) | -P(xx157) | -R(f9,xx158) | -R(xx158,xx157) | -P(xx159) | -R(f9,xx160) | -R(xx160,xx159).
end_of_list.
SHAR_EOF
if test -f 'thf1.ver1.out'
then
echo shar: over-writing existing file "'thf1.ver1.out'"
fi
cat << \SHAR_EOF > 'thf1.ver1.out'
problem-set/pelletier/full.predicate/thf1.ver1.out
created : 07/28/88
revised : 07/28/88
OTTER version 0.91, 14 June 1988.
set(hyper_res).
list(sos).
1 -P(a) | P(xx1) | P(f1(xx1)) | -P(a) | P(xx2) | P(f3(xx2)).
2 -P(a) | P(xx3) | P(f1(xx3)) | -P(a) | P(xx4) | R(xx4,f4(xx4)).
3 -P(a) | P(xx5) | P(f1(xx5)) | -P(a) | P(xx6) | R(f4(xx6),f3(xx6)).
4 -P(a) | P(xx7) | P(f1(xx7)) | -P(a) | P(xx8) | -P(a) | -P(xx9) | -R(xx8,xx9) | P(f5(xx8)).
5 -P(a) | P(xx10) | P(f1(xx10)) | -P(a) | P(xx11) | -P(a) | -P(xx12) | -R(xx11,xx12) | R(xx11,f6(xx11)).
6 -P(a) | P(xx13) | P(f1(xx13)) | -P(a) | P(xx14) | -P(a) | -P(xx15) | -R(xx14,xx15) | R(f6(xx14),f5(xx14)).
7 -P(a) | P(xx16) | R(xx16,f2(xx16)) | -P(a) | P(xx17) | P(f3(xx17)).
8 -P(a) | P(xx18) | R(xx18,f2(xx18)) | -P(a) | P(xx19) | R(xx19,f4(xx19)).
9 -P(a) | P(xx20) | R(xx20,f2(xx20)) | -P(a) | P(xx21) | R(f4(xx21),f3(xx21)).
10 -P(a) | P(xx22) | R(xx22,f2(xx22)) | -P(a) | P(xx23) | -P(a) | -P(xx24) | -R(xx23,xx24) | P(f5(xx23)).
11 -P(a) | P(xx25) | R(xx25,f2(xx25)) | -P(a) | P(xx26) | -P(a) | -P(xx27) | -R(xx26,xx27) | R(xx26,f6(xx26)).
12 -P(a) | P(xx28) | R(xx28,f2(xx28)) | -P(a) | P(xx29) | -P(a) | -P(xx30) | -R(xx29,xx30) | R(f6(xx29),f5(xx29)).
13 -P(a) | P(xx31) | R(f2(xx31),f1(xx31)) | -P(a) | P(xx32) | P(f3(xx32)).
14 -P(a) | P(xx33) | R(f2(xx33),f1(xx33)) | -P(a) | P(xx34) | R(xx34,f4(xx34)).
15 -P(a) | P(xx35) | R(f2(xx35),f1(xx35)) | -P(a) | P(xx36) | R(f4(xx36),f3(xx36)).
16 -P(a) | P(xx37) | R(f2(xx37),f1(xx37)) | -P(a) | P(xx38) | -P(a) | -P(xx39) | -R(xx38,xx39) | P(f5(xx38)).
17 -P(a) | P(xx40) | R(f2(xx40),f1(xx40)) | -P(a) | P(xx41) | -P(a) | -P(xx42) | -R(xx41,xx42) | R(xx41,f6(xx41)).
18 -P(a) | P(xx43) | R(f2(xx43),f1(xx43)) | -P(a) | P(xx44) | -P(a) | -P(xx45) | -R(xx44,xx45) | R(f6(xx44),f5(xx44)).
19 -P(a) | -P(xx46) | -R(xx47,xx46) | P(f1(xx47)) | -P(a) | P(xx48) | P(f3(xx48)).
20 -P(a) | -P(xx49) | -R(xx50,xx49) | P(f1(xx50)) | -P(a) | P(xx51) | R(xx51,f4(xx51)).
21 -P(a) | -P(xx52) | -R(xx53,xx52) | P(f1(xx53)) | -P(a) | P(xx54) | R(f4(xx54),f3(xx54)).
22 -P(a) | -P(xx55) | -R(xx56,xx55) | P(f1(xx56)) | -P(a) | P(xx57) | -P(a) | -P(xx58) | -R(xx57,xx58) | P(f5(xx57)).
23 -P(a) | -P(xx59) | -R(xx60,xx59) | P(f1(xx60)) | -P(a) | P(xx61) | -P(a) | -P(xx62) | -R(xx61,xx62) | R(xx61,f6(xx61)).
24 -P(a) | -P(xx63) | -R(xx64,xx63) | P(f1(xx64)) | -P(a) | P(xx65) | -P(a) | -P(xx66) | -R(xx65,xx66) | R(f6(xx65),f5(xx65)).
25 -P(a) | -P(xx67) | -R(xx68,xx67) | R(xx68,f2(xx68)) | -P(a) | P(xx69) | P(f3(xx69)).
26 -P(a) | -P(xx70) | -R(xx71,xx70) | R(xx71,f2(xx71)) | -P(a) | P(xx72) | R(xx72,f4(xx72)).
27 -P(a) | -P(xx73) | -R(xx74,xx73) | R(xx74,f2(xx74)) | -P(a) | P(xx75) | R(f4(xx75),f3(xx75)).
28 -P(a) | -P(xx76) | -R(xx77,xx76) | R(xx77,f2(xx77)) | -P(a) | P(xx78) | -P(a) | -P(xx79) | -R(xx78,xx79) | P(f5(xx78)).
29 -P(a) | -P(xx80) | -R(xx81,xx80) | R(xx81,f2(xx81)) | -P(a) | P(xx82) | -P(a) | -P(xx83) | -R(xx82,xx83) | R(xx82,f6(xx82)).
30 -P(a) | -P(xx84) | -R(xx85,xx84) | R(xx85,f2(xx85)) | -P(a) | P(xx86) | -P(a) | -P(xx87) | -R(xx86,xx87) | R(f6(xx86),f5(xx86)).
31 -P(a) | -P(xx88) | -R(xx89,xx88) | R(f2(xx89),f1(xx89)) | -P(a) | P(xx90) | P(f3(xx90)).
32 -P(a) | -P(xx91) | -R(xx92,xx91) | R(f2(xx92),f1(xx92)) | -P(a) | P(xx93) | R(xx93,f4(xx93)).
33 -P(a) | -P(xx94) | -R(xx95,xx94) | R(f2(xx95),f1(xx95)) | -P(a) | P(xx96) | R(f4(xx96),f3(xx96)).
34 -P(a) | -P(xx97) | -R(xx98,xx97) | R(f2(xx98),f1(xx98)) | -P(a) | P(xx99) | -P(a) | -P(xx100) | -R(xx99,xx100) | P(f5(xx99)).
35 -P(a) | -P(xx101) | -R(xx102,xx101) | R(f2(xx102),f1(xx102)) | -P(a) | P(xx103) | -P(a) | -P(xx104) | -R(xx103,xx104) | R(xx103,f6(xx103)).
36 -P(a) | -P(xx105) | -R(xx106,xx105) | R(f2(xx106),f1(xx106)) | -P(a) | P(xx107) | -P(a) | -P(xx108) | -R(xx107,xx108) | R(f6(xx107),f5(xx107)).
37 P(a) | P(a).
38 P(a) | -P(f9).
39 P(a) | -P(xx109) | -R(f9,xx110) | -R(xx110,xx109) | P(a).
40 P(a) | -P(xx111) | -R(f9,xx112) | -R(xx112,xx111) | P(f10).
41 P(a) | -P(xx113) | -R(f9,xx114) | -R(xx114,xx113) | R(f9,f10).
42 P(a) | -P(xx115) | -R(f9,xx116) | -R(xx116,xx115) | -P(xx117) | -R(f9,xx118) | -R(xx118,xx117).
43 -P(f7) | P(f8) | P(a).
44 -P(f7) | P(f8) | -P(f9).
45 -P(f7) | P(f8) | -P(xx119) | -R(f9,xx120) | -R(xx120,xx119) | P(a).
46 -P(f7) | P(f8) | -P(xx121) | -R(f9,xx122) | -R(xx122,xx121) | P(f10).
47 -P(f7) | P(f8) | -P(xx123) | -R(f9,xx124) | -R(xx124,xx123) | R(f9,f10).
48 -P(f7) | P(f8) | -P(xx125) | -R(f9,xx126) | -R(xx126,xx125) | -P(xx127) | -R(f9,xx128) | -R(xx128,xx127).
49 -P(f7) | R(f7,f8) | P(a).
50 -P(f7) | R(f7,f8) | -P(f9).
51 -P(f7) | R(f7,f8) | -P(xx129) | -R(f9,xx130) | -R(xx130,xx129) | P(a).
52 -P(f7) | R(f7,f8) | -P(xx131) | -R(f9,xx132) | -R(xx132,xx131) | P(f10).
53 -P(f7) | R(f7,f8) | -P(xx133) | -R(f9,xx134) | -R(xx134,xx133) | R(f9,f10).
54 -P(f7) | R(f7,f8) | -P(xx135) | -R(f9,xx136) | -R(xx136,xx135) | -P(xx137) | -R(f9,xx138) | -R(xx138,xx137).
55 -P(xx139) | -R(f7,xx140) | -R(xx140,xx139) | P(a).
56 -P(xx141) | -R(f7,xx142) | -R(xx142,xx141) | -P(f9).
57 -P(xx143) | -R(f7,xx144) | -R(xx144,xx143) | -P(xx145) | -R(f9,xx146) | -R(xx146,xx145) | P(a).
58 -P(xx147) | -R(f7,xx148) | -R(xx148,xx147) | -P(xx149) | -R(f9,xx150) | -R(xx150,xx149) | P(f10).
59 -P(xx151) | -R(f7,xx152) | -R(xx152,xx151) | -P(xx153) | -R(f9,xx154) | -R(xx154,xx153) | R(f9,f10).
60 -P(xx155) | -R(f7,xx156) | -R(xx156,xx155) | -P(xx157) | -R(f9,xx158) | -R(xx158,xx157) | -P(xx159) | -R(f9,xx160) | -R(xx160,xx159).
end_of_list.
new given clause: 37 P(a) | P(a).
new given clause: 38 P(a) | -P(f9).
new given clause: 43 -P(f7) | P(f8) | P(a).
new given clause: 44 -P(f7) | P(f8) | -P(f9).
new given clause: 49 -P(f7) | R(f7,f8) | P(a).
new given clause: 50 -P(f7) | R(f7,f8) | -P(f9).
new given clause: 55 -P(xx139) | -R(f7,xx140) | -R(xx140,xx139) | P(a).
new given clause: 56 -P(xx141) | -R(f7,xx142) | -R(xx142,xx141) | -P(f9).
new given clause: 39 P(a) | -P(xx109) | -R(f9,xx110) | -R(xx110,xx109) | P(a).
new given clause: 40 P(a) | -P(xx111) | -R(f9,xx112) | -R(xx112,xx111) | P(f10).
new given clause: 41 P(a) | -P(xx113) | -R(f9,xx114) | -R(xx114,xx113) | R(f9,f10).
new given clause: 1 -P(a) | P(xx1) | P(f1(xx1)) | -P(a) | P(xx2) | P(f3(xx2)).
new given clause: 45 -P(f7) | P(f8) | -P(xx119) | -R(f9,xx120) | -R(xx120,xx119) | P(a).
new given clause: 46 -P(f7) | P(f8) | -P(xx121) | -R(f9,xx122) | -R(xx122,xx121) | P(f10).
new given clause: 2 -P(a) | P(xx3) | P(f1(xx3)) | -P(a) | P(xx4) | R(xx4,f4(xx4)).
new given clause: 7 -P(a) | P(xx16) | R(xx16,f2(xx16)) | -P(a) | P(xx17) | P(f3(xx17)).
new given clause: 47 -P(f7) | P(f8) | -P(xx123) | -R(f9,xx124) | -R(xx124,xx123) | R(f9,f10).
new given clause: 51 -P(f7) | R(f7,f8) | -P(xx129) | -R(f9,xx130) | -R(xx130,xx129) | P(a).
new given clause: 52 -P(f7) | R(f7,f8) | -P(xx131) | -R(f9,xx132) | -R(xx132,xx131) | P(f10).
new given clause: 3 -P(a) | P(xx5) | P(f1(xx5)) | -P(a) | P(xx6) | R(f4(xx6),f3(xx6)).
new given clause: 8 -P(a) | P(xx18) | R(xx18,f2(xx18)) | -P(a) | P(xx19) | R(xx19,f4(xx19)).
new given clause: 13 -P(a) | P(xx31) | R(f2(xx31),f1(xx31)) | -P(a) | P(xx32) | P(f3(xx32)).
new given clause: 53 -P(f7) | R(f7,f8) | -P(xx133) | -R(f9,xx134) | -R(xx134,xx133) | R(f9,f10).
new given clause: 9 -P(a) | P(xx20) | R(xx20,f2(xx20)) | -P(a) | P(xx21) | R(f4(xx21),f3(xx21)).
new given clause: 14 -P(a) | P(xx33) | R(f2(xx33),f1(xx33)) | -P(a) | P(xx34) | R(xx34,f4(xx34)).
new given clause: 19 -P(a) | -P(xx46) | -R(xx47,xx46) | P(f1(xx47)) | -P(a) | P(xx48) | P(f3(xx48)).
new given clause: 15 -P(a) | P(xx35) | R(f2(xx35),f1(xx35)) | -P(a) | P(xx36) | R(f4(xx36),f3(xx36)).
new given clause: 20 -P(a) | -P(xx49) | -R(xx50,xx49) | P(f1(xx50)) | -P(a) | P(xx51) | R(xx51,f4(xx51)).
new given clause: 25 -P(a) | -P(xx67) | -R(xx68,xx67) | R(xx68,f2(xx68)) | -P(a) | P(xx69) | P(f3(xx69)).
new given clause: 42 P(a) | -P(xx115) | -R(f9,xx116) | -R(xx116,xx115) | -P(xx117) | -R(f9,xx118) | -R(xx118,xx117).
new given clause: 57 -P(xx143) | -R(f7,xx144) | -R(xx144,xx143) | -P(xx145) | -R(f9,xx146) | -R(xx146,xx145) | P(a).
new given clause: 58 -P(xx147) | -R(f7,xx148) | -R(xx148,xx147) | -P(xx149) | -R(f9,xx150) | -R(xx150,xx149) | P(f10).
new given clause: 21 -P(a) | -P(xx52) | -R(xx53,xx52) | P(f1(xx53)) | -P(a) | P(xx54) | R(f4(xx54),f3(xx54)).
new given clause: 26 -P(a) | -P(xx70) | -R(xx71,xx70) | R(xx71,f2(xx71)) | -P(a) | P(xx72) | R(xx72,f4(xx72)).
new given clause: 31 -P(a) | -P(xx88) | -R(xx89,xx88) | R(f2(xx89),f1(xx89)) | -P(a) | P(xx90) | P(f3(xx90)).
new given clause: 59 -P(xx151) | -R(f7,xx152) | -R(xx152,xx151) | -P(xx153) | -R(f9,xx154) | -R(xx154,xx153) | R(f9,f10).
new given clause: 27 -P(a) | -P(xx73) | -R(xx74,xx73) | R(xx74,f2(xx74)) | -P(a) | P(xx75) | R(f4(xx75),f3(xx75)).
new given clause: 32 -P(a) | -P(xx91) | -R(xx92,xx91) | R(f2(xx92),f1(xx92)) | -P(a) | P(xx93) | R(xx93,f4(xx93)).
new given clause: 48 -P(f7) | P(f8) | -P(xx125) | -R(f9,xx126) | -R(xx126,xx125) | -P(xx127) | -R(f9,xx128) | -R(xx128,xx127).
new given clause: 4 -P(a) | P(xx7) | P(f1(xx7)) | -P(a) | P(xx8) | -P(a) | -P(xx9) | -R(xx8,xx9) | P(f5(xx8)).
new given clause: 33 -P(a) | -P(xx94) | -R(xx95,xx94) | R(f2(xx95),f1(xx95)) | -P(a) | P(xx96) | R(f4(xx96),f3(xx96)).
new given clause: 54 -P(f7) | R(f7,f8) | -P(xx135) | -R(f9,xx136) | -R(xx136,xx135) | -P(xx137) | -R(f9,xx138) | -R(xx138,xx137).
new given clause: 5 -P(a) | P(xx10) | P(f1(xx10)) | -P(a) | P(xx11) | -P(a) | -P(xx12) | -R(xx11,xx12) | R(xx11,f6(xx11)).
new given clause: 10 -P(a) | P(xx22) | R(xx22,f2(xx22)) | -P(a) | P(xx23) | -P(a) | -P(xx24) | -R(xx23,xx24) | P(f5(xx23)).
new given clause: 6 -P(a) | P(xx13) | P(f1(xx13)) | -P(a) | P(xx14) | -P(a) | -P(xx15) | -R(xx14,xx15) | R(f6(xx14),f5(xx14)).
new given clause: 11 -P(a) | P(xx25) | R(xx25,f2(xx25)) | -P(a) | P(xx26) | -P(a) | -P(xx27) | -R(xx26,xx27) | R(xx26,f6(xx26)).
new given clause: 16 -P(a) | P(xx37) | R(f2(xx37),f1(xx37)) | -P(a) | P(xx38) | -P(a) | -P(xx39) | -R(xx38,xx39) | P(f5(xx38)).
new given clause: 12 -P(a) | P(xx28) | R(xx28,f2(xx28)) | -P(a) | P(xx29) | -P(a) | -P(xx30) | -R(xx29,xx30) | R(f6(xx29),f5(xx29)).
new given clause: 17 -P(a) | P(xx40) | R(f2(xx40),f1(xx40)) | -P(a) | P(xx41) | -P(a) | -P(xx42) | -R(xx41,xx42) | R(xx41,f6(xx41)).
new given clause: 22 -P(a) | -P(xx55) | -R(xx56,xx55) | P(f1(xx56)) | -P(a) | P(xx57) | -P(a) | -P(xx58) | -R(xx57,xx58) | P(f5(xx57)).
new given clause: 60 -P(xx155) | -R(f7,xx156) | -R(xx156,xx155) | -P(xx157) | -R(f9,xx158) | -R(xx158,xx157) | -P(xx159) | -R(f9,xx160) | -R(xx160,xx159).
new given clause: 18 -P(a) | P(xx43) | R(f2(xx43),f1(xx43)) | -P(a) | P(xx44) | -P(a) | -P(xx45) | -R(xx44,xx45) | R(f6(xx44),f5(xx44)).
new given clause: 23 -P(a) | -P(xx59) | -R(xx60,xx59) | P(f1(xx60)) | -P(a) | P(xx61) | -P(a) | -P(xx62) | -R(xx61,xx62) | R(xx61,f6(xx61)).
new given clause: 28 -P(a) | -P(xx76) | -R(xx77,xx76) | R(xx77,f2(xx77)) | -P(a) | P(xx78) | -P(a) | -P(xx79) | -R(xx78,xx79) | P(f5(xx78)).
new given clause: 24 -P(a) | -P(xx63) | -R(xx64,xx63) | P(f1(xx64)) | -P(a) | P(xx65) | -P(a) | -P(xx66) | -R(xx65,xx66) | R(f6(xx65),f5(xx65)).
new given clause: 29 -P(a) | -P(xx80) | -R(xx81,xx80) | R(xx81,f2(xx81)) | -P(a) | P(xx82) | -P(a) | -P(xx83) | -R(xx82,xx83) | R(xx82,f6(xx82)).
new given clause: 34 -P(a) | -P(xx97) | -R(xx98,xx97) | R(f2(xx98),f1(xx98)) | -P(a) | P(xx99) | -P(a) | -P(xx100) | -R(xx99,xx100) | P(f5(xx99)).
new given clause: 30 -P(a) | -P(xx84) | -R(xx85,xx84) | R(xx85,f2(xx85)) | -P(a) | P(xx86) | -P(a) | -P(xx87) | -R(xx86,xx87) | R(f6(xx86),f5(xx86)).
new given clause: 35 -P(a) | -P(xx101) | -R(xx102,xx101) | R(f2(xx102),f1(xx102)) | -P(a) | P(xx103) | -P(a) | -P(xx104) | -R(xx103,xx104) | R(xx103,f6(xx103)).
new given clause: 36 -P(a) | -P(xx105) | -R(xx106,xx105) | R(f2(xx106),f1(xx106)) | -P(a) | P(xx107) | -P(a) | -P(xx108) | -R(xx107,xx108) | R(f6(xx107),f5(xx107)).
------------ END OF SEARCH ------------
sos empty.
--------------- 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).
clear(order_eq).
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, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).
------------- memory usage ------------
3 mallocs of 32700 bytes each (95.8+ K)
type (bytes each) gets frees in use avail bytes
sym_ent ( 64) 178 0 178 0 11.1 K
term ( 16) 2841 2164 677 400 16.8 K
rel ( 20) 1731 1073 658 12 13.1 K
term_ptr ( 8) 2825 0 2825 0 22.1 K
fpa_head ( 12) 90 0 90 0 1.1 K
fpa_tree ( 28) 486 486 0 10 0.3 K
context ( 260) 353 353 0 10 2.5 K
trail ( 12) 236 236 0 1 0.0 K
imd_tree ( 24) 0 0 0 0 0.0 K
imd_pos ( 416) 0 0 0 0 0.0 K
is_tree ( 12) 83 0 83 0 1.0 K
is_pos (1216) 732 732 0 2 2.4 K
fsub_pos ( 8) 180 180 0 1 0.0 K
literal ( 16) 792 376 416 10 6.7 K
clause ( 28) 97 37 60 1 1.7 K
list ( 60) 2 0 2 0 0.1 K
clash_nd ( 32) 256 256 0 9 0.3 K
clause_ptr ( 8) 60 0 60 0 0.5 K
int_ptr ( 8) 108 108 0 3 0.0 K
-------------- statistics -------------
clauses input 60
clauses given 60
clauses generated 36
demodulation rewrites 0
clauses wt or lit delete 0
tautologies deleted 0
clauses forward subsumed 36
(clauses subsumed by sos) 0
unit deletions 0
clauses kept 0
empty clauses 0
factors generated 0
clauses back subsumed 0
clauses not processed 0
----------- times (seconds) -----------
run time 4.86
input time 2.31
binary_res time 0.00
hyper_res time 0.92
UR_res time 0.00
para_into time 0.00
para_from time 0.00
pre_process time 0.81
demod time 0.00
weigh time 0.00
for_sub time 0.77
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.38
IS build time 0.08
print_cl time 0.77
cl integrate time 0.07
window time 0.00
SHAR_EOF
if test -f 'thf2.desc'
then
echo shar: over-writing existing file "'thf2.desc'"
fi
cat << \SHAR_EOF > 'thf2.desc'
problem-set/pelletier/full.predicate/thf2.desc
created : 07/25/86
revised : 07/28/88
Natural Language Description:
Full Predicate Logic (without Identity and Functions).
If there were an 'anti-Russell set' (a set which contains exactly those
sets which are members of themselves), then not every set has a
complement.
(Ey)(Ax)(Fxy <-> Fxx) ->
-(Ax)(Ey)(Az)(Fxy <-> -Fzx)
Versions:
thf1.desc - declarative representation.
created by : From Pelletier paper, 1986.
verified for ITP : untested, 07/25/86
translated for OTTER by : K.R.
verified for OTTER : untested
SHAR_EOF
if test -f 'thf2.ver1.clauses'
then
echo shar: over-writing existing file "'thf2.ver1.clauses'"
fi
cat << \SHAR_EOF > 'thf2.ver1.clauses'
% problem-set/pelletier/full.predicate/thf2.ver1.clauses
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identity and Functions)..
% If there were an 'anti-Russell set' (a set which contains exactly .
% those sets which are members of themselves), then not every set has a
% complement..
%
% (Ey)(Ax)(Fxy <-> Fxx) ->.
% -(Ax)(Ey)(Az)(Fxy <-> -Fzx).
% Note: Since in itp, we can factor input clauses we would have to .
% factor it ourselves. Thus F(y,x) | F(x,f(x)) becomes F(x,f(x)) in .
% clause #4.
% representation:
%
% Declarative version
% declare_predicate(2,F).
% declare_function(1,f).
% declare_variables([x,y]).
% declare_constants([a]).
% clause form
-F(x,a) | F(x,x).
-F(x,x) | F(x,a).
-F(x,f(x)) | -F(y,x).
F(x,f(x)).
SHAR_EOF
if test -f 'thf2.ver1.in'
then
echo shar: over-writing existing file "'thf2.ver1.in'"
fi
cat << \SHAR_EOF > 'thf2.ver1.in'
% problem-set/pelletier/full.predicate/thf2.ver1.in
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identity and Functions)..
% If there were an 'anti-Russell set' (a set which contains exactly .
% those sets which are members of themselves), then not every set has a
% complement..
%
% (Ey)(Ax)(Fxy <-> Fxx) ->.
% -(Ax)(Ey)(Az)(Fxy <-> -Fzx).
% Note: Since in itp, we can factor input clauses we would have to .
% factor it ourselves. Thus F(y,x) | F(x,f(x)) becomes F(x,f(x)) in .
% clause #4.
% representation:
%
% Declarative version
% declare_predicate(2,F).
% declare_function(1,f).
% declare_variables([x,y]).
% declare_constants([a]).
set(hyper_res).
list(axioms).
% clause form .
-F(x,a) | F(x,x).
-F(x,x) | F(x,a).
-F(x,f(x)) | -F(y,x).
end_of_list.
list(sos).
F(x,f(x)).
end_of_list.
SHAR_EOF
if test -f 'thf2.ver1.out'
then
echo shar: over-writing existing file "'thf2.ver1.out'"
fi
cat << \SHAR_EOF > 'thf2.ver1.out'
problem-set/pelletier/full.predicate/thf2.ver1.out
created : 07/28/88
revised : 07/28/88
OTTER version 0.91, 14 June 1988.
set(hyper_res).
list(axioms).
1 -F(x,a) | F(x,x).
2 -F(x,x) | F(x,a).
3 -F(x,f(x)) | -F(y,x).
end_of_list.
list(sos).
4 F(x,f(x)).
end_of_list.
new given clause: 4 F(x,f(x)).
** KEPT: 5 (4,3,4) .
** KEPT: 6 (4,3,4) .
------------> EMPTY CLAUSE -----------> 5 (4,3,4) .
------------ END OF SEARCH ------------
---------------- PROOF ----------------
3 -F(x,f(x)) | -F(y,x).
4 F(x,f(x)).
5 (4,3,4) .
--------------- 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).
clear(order_eq).
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, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).
------------- memory usage ------------
1 mallocs of 32700 bytes each (31.9+ K)
type (bytes each) gets frees in use avail bytes
sym_ent ( 64) 11 0 11 0 0.7 K
term ( 16) 40 29 11 11 0.3 K
rel ( 20) 26 11 15 5 0.4 K
term_ptr ( 8) 57 0 57 0 0.4 K
fpa_head ( 12) 24 0 24 0 0.3 K
fpa_tree ( 28) 9 9 0 8 0.2 K
context ( 260) 6 6 0 4 1.0 K
trail ( 12) 7 7 0 3 0.0 K
imd_tree ( 24) 0 0 0 0 0.0 K
imd_pos ( 416) 0 0 0 0 0.0 K
is_tree ( 12) 16 0 16 0 0.2 K
is_pos (1216) 0 0 0 0 0.0 K
fsub_pos ( 8) 0 0 0 0 0.0 K
literal ( 16) 7 0 7 0 0.1 K
clause ( 28) 8 2 6 0 0.2 K
list ( 60) 2 0 2 0 0.1 K
clash_nd ( 32) 2 2 0 1 0.0 K
clause_ptr ( 8) 9 3 6 3 0.1 K
int_ptr ( 8) 6 0 6 0 0.0 K
-------------- statistics -------------
clauses input 4
clauses given 1
clauses generated 2
demodulation rewrites 0
clauses wt or lit delete 0
tautologies deleted 0
clauses forward subsumed 0
(clauses subsumed by sos) 0
unit deletions 0
clauses kept 2
empty clauses 1
factors generated 0
clauses back subsumed 0
clauses not processed 0
----------- times (seconds) -----------
run time 0.15
input time 0.05
binary_res time 0.00
hyper_res time 0.01
UR_res time 0.00
para_into time 0.00
para_from time 0.00
pre_process time 0.00
demod time 0.00
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.01
IS build time 0.00
print_cl time 0.01
cl integrate time 0.00
window time 0.00
SHAR_EOF
if test -f 'thf3.desc'
then
echo shar: over-writing existing file "'thf3.desc'"
fi
cat << \SHAR_EOF > 'thf3.desc'
problem-set/pelletier/full.predicate/thf3.desc
created : 07/25/86
revised : 07/28/88
Natural Language Description:
Full Predicate Logic (without Identity and Functions)
The 'restricted comprehension axiom' says: given a set z, there is a
set all of whose members are drawn form z and which satisfy some
property. If there were a universal set then the Russell set could
be formed, using this axiom. So given the appropriate instance
of this axiom, there is no universal set.
(Az)(Ey)(Ax)(Fxy <->
--------------------
(Fxz & -Fxx))
--------------
-(Ez)(Ax)Fxz
Versions:
thf1.desc - declarative representation.
created by : From Pelletier paper, 1986.
verified for ITP : untested, 07/25/86
translated for OTTER by : K.R.
verified for OTTER : untested
SHAR_EOF
if test -f 'thf3.ver1.clauses'
then
echo shar: over-writing existing file "'thf3.ver1.clauses'"
fi
cat << \SHAR_EOF > 'thf3.ver1.clauses'
% problem-set/pelletier/full.predicate/thf3.ver1.clauses
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identity and Functions).
% The 'restricted comprehension axiom' says: given a set z, there is a.
% set all of whose members are drawn form z and which satisfy some .
% property. If there were a universal set then the Russell set could.
% be formed, using this axiom. So given the appropriate instance.
% of this axiom, there is no universal set..
% (Az)(Ey)(Ax)(Fxy <->.
% --------------------.
% (Fxz & -Fxx)).
% --------------.
% -(Ez)(Ax)Fxz.
% representation:
%
% Declarative version
% declare_predicate(2,F).
% declare_function(1,f).
% declare_variables([x,y]).
% declare_constants([a]).
% hypothesis.
-F(x,f(y)) | F(x,y).
% denial.
-F(x,f(y)) | F(x,x).
-F(x,y) | F(x,x) | F(x,f(y)).
F(x,a).
SHAR_EOF
if test -f 'thf3.ver1.in'
then
echo shar: over-writing existing file "'thf3.ver1.in'"
fi
cat << \SHAR_EOF > 'thf3.ver1.in'
% problem-set/pelletier/full.predicate/thf3.ver1.in
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identity and Functions).
% The 'restricted comprehension axiom' says: given a set z, there is a.
% set all of whose members are drawn form z and which satisfy some .
% property. If there were a universal set then the Russell set could.
% be formed, using this axiom. So given the appropriate instance.
% of this axiom, there is no universal set..
% (Az)(Ey)(Ax)(Fxy <->.
% --------------------.
% (Fxz & -Fxx)).
% --------------.
% -(Ez)(Ax)Fxz.
% representation:
%
% Declarative version
% declare_predicate(2,F).
% declare_function(1,f).
% declare_variables([x,y]).
% declare_constants([a]).
set(hyper_res).
set(factor).
list(sos).
% hypothesis.
-F(x,f(y)) | F(x,y).
% denial.
-F(x,f(y)) | F(x,x).
-F(x,y) | F(x,x) | F(x,f(y)).
F(x,a).
end_of_list.
SHAR_EOF
if test -f 'thf3.ver1.out'
then
echo shar: over-writing existing file "'thf3.ver1.out'"
fi
cat << \SHAR_EOF > 'thf3.ver1.out'
problem-set/pelletier/full.predicate/thf3.ver1.out
created : 07/28/88
revised : 07/28/88
OTTER version 0.91, 14 June 1988.
set(hyper_res).
list(sos).
1 -F(x,f(y)) | F(x,y).
2 -F(x,f(y)) | F(x,x).
3 -F(x,y) | F(x,x) | F(x,f(y)).
4 F(x,a).
end_of_list.
new given clause: 4 F(x,a).
new given clause: 1 -F(x,f(y)) | F(x,y).
new given clause: 2 -F(x,f(y)) | F(x,x).
new given clause: 3 -F(x,y) | F(x,x) | F(x,f(y)).
** KEPT: 5 (3,4) F(x,x) | F(x,f(a)).
new given clause: 5 (3,4) F(x,x) | F(x,f(a)).
** KEPT: 6 (5,1) F(f(x),f(a)) | F(f(x),x).
** KEPT: 7 (5,3) F(x,x) | F(x,f(f(a))).
** KEPT: 8 (5,2) F(x,x).
8 back subsumes: 7 (5,3) F(x,x) | F(x,f(f(a))).
8 back subsumes: 5 (3,4) F(x,x) | F(x,f(a)).
8 back subsumes: 3 -F(x,y) | F(x,x) | F(x,f(y)).
8 back subsumes: 2 -F(x,f(y)) | F(x,x).
new given clause: 8 (5,2) F(x,x).
** KEPT: 9 (8,1) F(f(x),x).
9 back subsumes: 6 (5,1) F(f(x),f(a)) | F(f(x),x).
new given clause: 9 (8,1) F(f(x),x).
** KEPT: 10 (9,1) F(f(f(x)),x).
new given clause: 10 (9,1) F(f(f(x)),x).
** KEPT: 11 (10,1) F(f(f(f(x))),x).
new given clause: 11 (10,1) F(f(f(f(x))),x).
** KEPT: 12 (11,1) F(f(f(f(f(x)))),x).
new given clause: 12 (11,1) F(f(f(f(f(x)))),x).
** KEPT: 13 (12,1) F(f(f(f(f(f(x))))),x).
new given clause: 13 (12,1) F(f(f(f(f(f(x))))),x).
** KEPT: 14 (13,1) F(f(f(f(f(f(f(x)))))),x).
new given clause: 14 (13,1) F(f(f(f(f(f(f(x)))))),x).
** KEPT: 15 (14,1) F(f(f(f(f(f(f(f(x))))))),x).
new given clause: 15 (14,1) F(f(f(f(f(f(f(f(x))))))),x).
** KEPT: 16 (15,1) F(f(f(f(f(f(f(f(f(x)))))))),x).
new given clause: 16 (15,1) F(f(f(f(f(f(f(f(f(x)))))))),x).
** KEPT: 17 (16,1) F(f(f(f(f(f(f(f(f(f(x))))))))),x).
new given clause: 17 (16,1) F(f(f(f(f(f(f(f(f(f(x))))))))),x).
** KEPT: 18 (17,1) F(f(f(f(f(f(f(f(f(f(f(x)))))))))),x).
new given clause: 18 (17,1) F(f(f(f(f(f(f(f(f(f(f(x)))))))))),x).
** KEPT: 19 (18,1) F(f(f(f(f(f(f(f(f(f(f(f(x))))))))))),x).
new given clause: 19 (18,1) F(f(f(f(f(f(f(f(f(f(f(f(x))))))))))),x).
** KEPT: 20 (19,1) F(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))),x).
new given clause: 20 (19,1) F(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))),x).
** KEPT: 21 (20,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))),x).
new given clause: 21 (20,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))),x).
** KEPT: 22 (21,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))),x).
new given clause: 22 (21,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))),x).
** KEPT: 23 (22,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))),x).
new given clause: 23 (22,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))),x).
** KEPT: 24 (23,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))),x).
new given clause: 24 (23,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))),x).
** KEPT: 25 (24,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))),x).
new given clause: 25 (24,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))),x).
** KEPT: 26 (25,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))),x).
new given clause: 26 (25,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))),x).
** KEPT: 27 (26,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))),x).
new given clause: 27 (26,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))),x).
** KEPT: 28 (27,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))),x).
new given clause: 28 (27,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))),x).
** KEPT: 29 (28,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))),x).
new given clause: 29 (28,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))),x).
** KEPT: 30 (29,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))),x).
new given clause: 30 (29,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))),x).
** KEPT: 31 (30,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))),x).
new given clause: 31 (30,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))),x).
** KEPT: 32 (31,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))),x).
new given clause: 32 (31,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))),x).
** KEPT: 33 (32,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))),x).
new given clause: 33 (32,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))),x).
** KEPT: 34 (33,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))),x).
new given clause: 34 (33,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))),x).
** KEPT: 35 (34,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))),x).
new given clause: 35 (34,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))),x).
** KEPT: 36 (35,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))),x).
new given clause: 36 (35,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))),x).
** KEPT: 37 (36,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))),x).
new given clause: 37 (36,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))),x).
** KEPT: 38 (37,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))),x).
new given clause: 38 (37,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))),x).
** KEPT: 39 (38,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))),x).
new given clause: 39 (38,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))),x).
** KEPT: 40 (39,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))),x).
new given clause: 40 (39,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))),x).
** KEPT: 41 (40,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))),x).
new given clause: 41 (40,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))),x).
** KEPT: 42 (41,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))),x).
new given clause: 42 (41,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))),x).
** KEPT: 43 (42,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))),x).
new given clause: 43 (42,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))),x).
** KEPT: 44 (43,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))),x).
new given clause: 44 (43,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))),x).
** KEPT: 45 (44,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))),x).
new given clause: 45 (44,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))),x).
** KEPT: 46 (45,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))),x).
new given clause: 46 (45,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))),x).
** KEPT: 47 (46,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))),x).
new given clause: 47 (46,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 48 (47,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))),x).
new given clause: 48 (47,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 49 (48,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 49 (48,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 50 (49,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 50 (49,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 51 (50,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 51 (50,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 52 (51,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 52 (51,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 53 (52,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 53 (52,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 54 (53,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 54 (53,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 55 (54,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 55 (54,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 56 (55,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 56 (55,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 57 (56,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 57 (56,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 58 (57,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 58 (57,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 59 (58,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 59 (58,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 60 (59,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 60 (59,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 61 (60,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 61 (60,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 62 (61,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 62 (61,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 63 (62,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 63 (62,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 64 (63,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 64 (63,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 65 (64,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 65 (64,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 66 (65,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 66 (65,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 67 (66,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 67 (66,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 68 (67,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 68 (67,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 69 (68,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 69 (68,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 70 (69,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 70 (69,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 71 (70,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 71 (70,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 72 (71,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 72 (71,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 73 (72,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 73 (72,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 74 (73,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 74 (73,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 75 (74,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 75 (74,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 76 (75,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 76 (75,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 77 (76,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 77 (76,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
** KEPT: 78 (77,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
new given clause: 78 (77,1) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),x).
SHAR_EOF
if test -f 'thf4.desc'
then
echo shar: over-writing existing file "'thf4.desc'"
fi
cat << \SHAR_EOF > 'thf4.desc'
problem-set/pelletier/full.predicate/thf4.desc
created : 07/25/86
revised : 07/28/88
Natural Language Description:
Full Predicate Logic (without Identity and Functions)
A set is 'circular' if it is a member of another set which in turn is
a member of the original. Intuitively all sets are non-circular.
Prove there is no set of noncircular sets.
-(Ey)(Ax)(Fxy <-> -(Ez)(Fxz & Fzx)).
Versions:
thf1.desc - declarative representation.
created by : From Pelletier paper, 1986.
verified for ITP : 07/25/86
translated for OTTER by : K.R.
verified for OTTER : 07/28/88
SHAR_EOF
if test -f 'thf4.ver1.clauses'
then
echo shar: over-writing existing file "'thf4.ver1.clauses'"
fi
cat << \SHAR_EOF > 'thf4.ver1.clauses'
% problem-set/pelletier/full.predicate/thf4.ver1.clauses
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identity and Functions).
% A set is 'circular' if it is a member of another set which in turn is.
% a member of the original. Intuitively all sets are non-circular. .
% Prove there is no set of noncircular sets..
% -(Ey)(Ax)(Fxy <-> -(Ez)(Fxz & Fzx))..
% representation:
%
% Declarative version
% hypothesis.
-F(x,a) | -F(x,y) | -F(y,x).
% denial.
F(x,f(x)) | F(x,a).
F(f(x),x) | F(x,a).
SHAR_EOF
if test -f 'thf4.ver1.in'
then
echo shar: over-writing existing file "'thf4.ver1.in'"
fi
cat << \SHAR_EOF > 'thf4.ver1.in'
% problem-set/pelletier/full.predicate/thf4.ver1.in
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identity and Functions).
% A set is 'circular' if it is a member of another set which in turn is.
% a member of the original. Intuitively all sets are non-circular. .
% Prove there is no set of noncircular sets..
% -(Ey)(Ax)(Fxy <-> -(Ez)(Fxz & Fzx))..
% representation:
%
% Declarative version
set(hyper_res).
list(sos).
% hypothesis.
-F(x,a) | -F(x,y) | -F(y,x).
% denial.
F(x,f(x)) | F(x,a).
F(f(x),x) | F(x,a).
end_of_list.
SHAR_EOF
if test -f 'thf4.ver1.out'
then
echo shar: over-writing existing file "'thf4.ver1.out'"
fi
cat << \SHAR_EOF > 'thf4.ver1.out'
problem-set/pelletier/full.predicate/thf4.ver1.out
created : 07/28/88
revised : 07/28/88
OTTER version 0.91, 14 June 1988.
set(hyper_res).
list(sos).
1 -F(x,a) | -F(x,y) | -F(y,x).
2 F(x,f(x)) | F(x,a).
3 F(f(x),x) | F(x,a).
end_of_list.
new given clause: 2 F(x,f(x)) | F(x,a).
new given clause: 3 F(f(x),x) | F(x,a).
new given clause: 1 -F(x,a) | -F(x,y) | -F(y,x).
** KEPT: 4 (1,3,3,3) F(f(a),a).
** KEPT: 5 (1,3,3,2) F(f(f(a)),f(a)) | F(a,a).
** KEPT: 6 (1,3,3,2) F(f(f(x)),f(x)) | F(x,a).
** KEPT: 7 (1,3,3,2) F(a,a).
** KEPT: 8 (1,2,3,2) F(f(x),f(f(x))) | F(x,a).
** KEPT: 9 (1,2,2,2) F(a,f(a)).
6 back subsumes: 5 (1,3,3,2) F(f(f(a)),f(a)) | F(a,a).
new given clause: 7 (1,3,3,2) F(a,a).
** KEPT: 10 (7,1,7,7) .
** KEPT: 11 (7,1,7,7) .
** KEPT: 12 (7,1,7,7) .
------------> EMPTY CLAUSE -----------> 10 (7,1,7,7) .
------------ END OF SEARCH ------------
---------------- PROOF ----------------
1 -F(x,a) | -F(x,y) | -F(y,x).
2 F(x,f(x)) | F(x,a).
3 F(f(x),x) | F(x,a).
7 (1,3,3,2) F(a,a).
10 (7,1,7,7) .
--------------- 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).
clear(order_eq).
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, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).
------------- memory usage ------------
1 mallocs of 32700 bytes each (31.9+ K)
type (bytes each) gets frees in use avail bytes
sym_ent ( 64) 10 0 10 0 0.6 K
term ( 16) 591 566 25 15 0.6 K
rel ( 20) 438 401 37 12 1.0 K
term_ptr ( 8) 112 11 101 8 0.9 K
fpa_head ( 12) 33 1 32 0 0.4 K
fpa_tree ( 28) 169 169 0 19 0.5 K
context ( 260) 82 82 0 5 1.3 K
trail ( 12) 111 111 0 5 0.1 K
imd_tree ( 24) 0 0 0 0 0.0 K
imd_pos ( 416) 0 0 0 0 0.0 K
is_tree ( 12) 32 3 29 3 0.4 K
is_pos (1216) 136 136 0 2 2.4 K
fsub_pos ( 8) 58 58 0 1 0.0 K
literal ( 16) 125 109 16 3 0.3 K
clause ( 28) 58 46 12 1 0.4 K
list ( 60) 2 0 2 0 0.1 K
clash_nd ( 32) 9 9 0 3 0.1 K
clause_ptr ( 8) 18 6 12 5 0.1 K
int_ptr ( 8) 216 180 36 4 0.3 K
-------------- statistics -------------
clauses input 3
clauses given 4
clauses generated 54
demodulation rewrites 0
clauses wt or lit delete 0
tautologies deleted 0
clauses forward subsumed 45
(clauses subsumed by sos) 37
unit deletions 0
clauses kept 9
empty clauses 1
factors generated 0
clauses back subsumed 1
clauses not processed 3
----------- times (seconds) -----------
run time 0.39
input time 0.04
binary_res time 0.00
hyper_res time 0.10
UR_res time 0.00
para_into time 0.00
para_from time 0.00
pre_process time 0.12
demod time 0.00
weigh time 0.00
for_sub time 0.06
unit_del time 0.00
post_process time 0.02
back_sub time 0.00
conflict time 0.00
factor time 0.00
FPA build time 0.01
IS build time 0.00
print_cl time 0.04
cl integrate time 0.01
window time 0.00
SHAR_EOF
if test -f 'thf5.desc'
then
echo shar: over-writing existing file "'thf5.desc'"
fi
cat << \SHAR_EOF > 'thf5.desc'
problem-set/pelletier/full.predicate/thf5.desc
created : 07/25/86
revised : 07/28/88
Natural Language Description:
Full Predicate Logic (without Identity and Functions).
- De Champeaux, 1979.
Define set equality ('Q') as having exactly the same members. Prove
set equality is symmetric.
(Ax)(Ay)(Qxy <-> (Az)(Fzx <-> Fzy))
----------------------------------
(Ax)(Ay)(Qxy <-> Qyx)
Versions:
thf1.desc - declarative representation.
created by : From Pelletier paper, 1986.
verified for ITP : untested, 07/25/86
translated for OTTER by : K.R.
verified for OTTER : untested
SHAR_EOF
if test -f 'thf5.ver1.clauses'
then
echo shar: over-writing existing file "'thf5.ver1.clauses'"
fi
cat << \SHAR_EOF > 'thf5.ver1.clauses'
% problem-set/pelletier/full.predicate/thf5.ver1.clauses
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identity and Functions)..
% - De Champeaux, 1979..
% Define set equality ('Q') as having exactly the same members. Prove.
% set equality is symmetric..
% (Ax)(Ay)(Qxy <-> (Az)(Fzx <-> Fzy)).
% ----------------------------------.
% (Ax)(Ay)(Qxy <-> Qyx).
% representation:
%
% Declarative version
% declare_predicates(2,[Q,F]).
% declare_function(2,f).
% declare_variables([x,y,z]).
% declare_constants([a,b]).
-Q(x,y) | -F(z,x) | F(z,y).
-Q(x,y) | -F(z,y) | F(z,x).
F(f(x,y),x) | F(f(x,y),y) | Q(x,y).
-F(f(x,y),y) | -F(f(x,y),x) | Q(x,y).
Q(a,b) | Q(b,a).
-Q(b,a) | -Q(a,b).
SHAR_EOF
if test -f 'thf5.ver1.in'
then
echo shar: over-writing existing file "'thf5.ver1.in'"
fi
cat << \SHAR_EOF > 'thf5.ver1.in'
% problem-set/pelletier/full.predicate/thf5.ver1.in
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identity and Functions)..
% - De Champeaux, 1979..
% Define set equality ('Q') as having exactly the same members. Prove.
% set equality is symmetric..
% (Ax)(Ay)(Qxy <-> (Az)(Fzx <-> Fzy)).
% ----------------------------------.
% (Ax)(Ay)(Qxy <-> Qyx).
% representation:
%
% Declarative version
% declare_predicates(2,[Q,F]).
% declare_function(2,f).
% declare_variables([x,y,z]).
% declare_constants([a,b]).
set(binary_res).
set(factor).
list(sos).
-Q(x,y) | -F(z,x) | F(z,y).
-Q(x,y) | -F(z,y) | F(z,x).
F(f(x,y),x) | F(f(x,y),y) | Q(x,y).
-F(f(x,y),y) | -F(f(x,y),x) | Q(x,y).
Q(a,b) | Q(b,a).
-Q(b,a) | -Q(a,b).
end_of_list.
SHAR_EOF
if test -f 'thf5.ver1.out'
then
echo shar: over-writing existing file "'thf5.ver1.out'"
fi
cat << \SHAR_EOF > 'thf5.ver1.out'
problem-set/pelletier/full.predicate/thf5.ver1.out
created : 07/28/88
revised : 07/28/88
OTTER version 0.91, 14 June 1988.
set(hyper_res).
list(sos).
1 -Q(x,y) | -F(z,x) | F(z,y).
2 -Q(x,y) | -F(z,y) | F(z,x).
3 F(f(x,y),x) | F(f(x,y),y) | Q(x,y).
4 -F(f(x,y),y) | -F(f(x,y),x) | Q(x,y).
5 Q(a,b) | Q(b,a).
6 -Q(b,a) | -Q(a,b).
end_of_list.
new given clause: 5 Q(a,b) | Q(b,a).
new given clause: 6 -Q(b,a) | -Q(a,b).
new given clause: 1 -Q(x,y) | -F(z,x) | F(z,y).
new given clause: 2 -Q(x,y) | -F(z,y) | F(z,x).
new given clause: 3 F(f(x,y),x) | F(f(x,y),y) | Q(x,y).
** KEPT: 7 (3,2,5) F(f(a,x),x) | Q(a,x) | F(f(a,x),b) | Q(a,b).
** KEPT: 8 (3,2,5) F(f(b,x),x) | Q(b,x) | F(f(b,x),a) | Q(b,a).
** KEPT: 9 (3,2,3) F(f(x,y),y) | Q(x,y) | F(f(x,y),z) | F(f(z,x),z) | F(f(z,x),x).
** KEPT: 10 (3,1,5) F(f(b,x),x) | Q(b,x) | F(f(b,x),a) | Q(a,b).
** KEPT: 11 (3,1,5) F(f(a,x),x) | Q(a,x) | F(f(a,x),b) | Q(b,a).
** KEPT: 12 (3,1,3) F(f(x,y),y) | Q(x,y) | F(f(x,y),z) | F(f(x,z),x) | F(f(x,z),z).
** KEPT: 13 (3,2,5) F(f(x,a),x) | Q(x,a) | F(f(x,a),b) | Q(a,b).
** KEPT: 14 (3,2,5) F(f(x,b),x) | Q(x,b) | F(f(x,b),a) | Q(b,a).
** KEPT: 15 (3,2,3) F(f(x,y),x) | Q(x,y) | F(f(x,y),z) | F(f(z,y),z) | F(f(z,y),y).
** KEPT: 16 (3,1,5) F(f(x,b),x) | Q(x,b) | F(f(x,b),a) | Q(a,b).
** KEPT: 17 (3,1,5) F(f(x,a),x) | Q(x,a) | F(f(x,a),b) | Q(b,a).
** KEPT: 18 (3,1,3) F(f(x,y),x) | Q(x,y) | F(f(x,y),z) | F(f(y,z),y) | F(f(y,z),z).
** KEPT: 19 (3,6,3) F(f(a,b),a) | F(f(a,b),b) | F(f(b,a),b) | F(f(b,a),a).
12 back subsumes: 3 F(f(x,y),x) | F(f(x,y),y) | Q(x,y).
new given clause: 4 -F(f(x,y),y) | -F(f(x,y),x) | Q(x,y).
new given clause: 7 (3,2,5) F(f(a,x),x) | Q(a,x) | F(f(a,x),b) | Q(a,b).
** KEPT: 20 (7,4,7) Q(a,a) | F(f(a,a),b) | Q(a,b).
new given clause: 20 (7,4,7) Q(a,a) | F(f(a,a),b) | Q(a,b).
new given clause: 8 (3,2,5) F(f(b,x),x) | Q(b,x) | F(f(b,x),a) | Q(b,a).
** KEPT: 21 (8,4,8) Q(b,b) | F(f(b,b),a) | Q(b,a).
** KEPT: 22 (8,6,20) F(f(b,x),x) | Q(b,x) | F(f(b,x),a) | Q(a,a) | F(f(a,a),b).
** KEPT: 23 (8,6,7) F(f(b,x),x) | Q(b,x) | F(f(b,x),a) | F(f(a,y),y) | Q(a,y) | F(f(a,y),b).
new given clause: 21 (8,4,8) Q(b,b) | F(f(b,b),a) | Q(b,a).
** KEPT: 24 (21,6,20) Q(b,b) | F(f(b,b),a) | Q(a,a) | F(f(a,a),b).
** KEPT: 25 (21,6,7) Q(b,b) | F(f(b,b),a) | F(f(a,x),x) | Q(a,x) | F(f(a,x),b).
new given clause: 10 (3,1,5) F(f(b,x),x) | Q(b,x) | F(f(b,x),a) | Q(a,b).
SHAR_EOF
if test -f 'thf6.desc'
then
echo shar: over-writing existing file "'thf6.desc'"
fi
cat << \SHAR_EOF > 'thf6.desc'
problem-set/pelletier/full.predicate/thf6.desc
created : 07/25/86
revised : 07/28/88
Natural Language Description:
Full Predicate Logic (without Identities and Functions).
(Ax)(Fx & (Ay)[Gy & Hxy -> Jxy] -> (Ay)(Gy & Hxy -> Ky))
-(Ey)(Ly & Ky)
(Ex)[Fx & (Ay)(Hxy -> Ly) &
---------------------------
(Ay)(Gy & Hxy -> Jxy)]
----------------------
(Ex)(Fx & -(Ey)(Gy & Hxy))
Versions:
thf1.desc - declarative representation.
created by : From Pelletier paper, 1986.
verified for ITP : 07/25/86
translated for OTTER by : K.R.
verified for OTTER : 07/28/88
SHAR_EOF
if test -f 'thf6.ver1.clauses'
then
echo shar: over-writing existing file "'thf6.ver1.clauses'"
fi
cat << \SHAR_EOF > 'thf6.ver1.clauses'
% problem-set/pelletier/full.predicate/thf6.ver1.clauses
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identities and Functions)..
% (Ax)(Fx & (Ay)[Gy & Hxy -> Jxy] -> (Ay)(Gy & Hxy -> Ky)).
% -(Ey)(Ly & Ky).
% (Ex)[Fx & (Ay)(Hxy -> Ly) &.
% ---------------------------.
% (Ay)(Gy & Hxy -> Jxy)].
% ----------------------.
% (Ex)(Fx & -(Ey)(Gy & Hxy)).
% representation:
%
% Declarative version
% declare_predicates(2,[H,J]).
% declare_predicates(1,[F,G,K,L]).
% declare_functions(1,[f,g]).
% declare_variables([x,y]).
% declare_constants([a]).
% clauses
-F(x) | G(f(x)) | -G(y) | -H(x,y) | K(y).
-F(x) | H(x,f(x)) | -G(y) | -H(x,y) | K(y).
-F(x) | -J(x,f(x)) | -G(y) | -H(x,y) | K(y).
-L(x) | -K(x).
F(a).
-H(a,x) | L(x).
-G(x) | -H(a,x) | J(a,x).
-F(x) | G(g(x)).
-F(x) | H(x,g(x)).
SHAR_EOF
if test -f 'thf6.ver1.in'
then
echo shar: over-writing existing file "'thf6.ver1.in'"
fi
cat << \SHAR_EOF > 'thf6.ver1.in'
% problem-set/pelletier/full.predicate/thf6.ver1.in
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identities and Functions)..
% (Ax)(Fx & (Ay)[Gy & Hxy -> Jxy] -> (Ay)(Gy & Hxy -> Ky)).
% -(Ey)(Ly & Ky).
% (Ex)[Fx & (Ay)(Hxy -> Ly) &.
% ---------------------------.
% (Ay)(Gy & Hxy -> Jxy)].
% ----------------------.
% (Ex)(Fx & -(Ey)(Gy & Hxy)).
% representation:
%
% Declarative version
% declare_predicates(2,[H,J]).
% declare_predicates(1,[F,G,K,L]).
% declare_functions(1,[f,g]).
% declare_variables([x,y]).
% declare_constants([a]).
set(hyper_res).
list(sos).
% clauses
-F(x) | G(f(x)) | -G(y) | -H(x,y) | K(y).
-F(x) | H(x,f(x)) | -G(y) | -H(x,y) | K(y).
-F(x) | -J(x,f(x)) | -G(y) | -H(x,y) | K(y).
-L(x) | -K(x).
F(a).
-H(a,x) | L(x).
-G(x) | -H(a,x) | J(a,x).
-F(x) | G(g(x)).
-F(x) | H(x,g(x)).
end_of_list.
SHAR_EOF
if test -f 'thf6.ver1.out'
then
echo shar: over-writing existing file "'thf6.ver1.out'"
fi
cat << \SHAR_EOF > 'thf6.ver1.out'
problem-set/pelletier/full.predicate/thf6.ver1.out
created : 07/28/88
revised : 07/28/88
OTTER version 0.91, 14 June 1988.
set(hyper_res).
list(sos).
1 -F(x) | G(f(x)) | -G(y) | -H(x,y) | K(y).
2 -F(x) | H(x,f(x)) | -G(y) | -H(x,y) | K(y).
3 -F(x) | -J(x,f(x)) | -G(y) | -H(x,y) | K(y).
4 -L(x) | -K(x).
5 F(a).
6 -H(a,x) | L(x).
7 -G(x) | -H(a,x) | J(a,x).
8 -F(x) | G(g(x)).
9 -F(x) | H(x,g(x)).
end_of_list.
new given clause: 5 F(a).
new given clause: 4 -L(x) | -K(x).
new given clause: 6 -H(a,x) | L(x).
new given clause: 8 -F(x) | G(g(x)).
** KEPT: 10 (8,5) G(g(a)).
new given clause: 10 (8,5) G(g(a)).
new given clause: 9 -F(x) | H(x,g(x)).
** KEPT: 11 (9,5) H(a,g(a)).
new given clause: 11 (9,5) H(a,g(a)).
** KEPT: 12 (11,6) L(g(a)).
new given clause: 12 (11,6) L(g(a)).
new given clause: 7 -G(x) | -H(a,x) | J(a,x).
** KEPT: 13 (7,10,11) J(a,g(a)).
new given clause: 13 (7,10,11) J(a,g(a)).
new given clause: 1 -F(x) | G(f(x)) | -G(y) | -H(x,y) | K(y).
** KEPT: 14 (1,5,10,11) G(f(a)) | K(g(a)).
new given clause: 14 (1,5,10,11) G(f(a)) | K(g(a)).
** KEPT: 15 (14,4,12) G(f(a)).
15 back subsumes: 14 (1,5,10,11) G(f(a)) | K(g(a)).
new given clause: 15 (14,4,12) G(f(a)).
new given clause: 2 -F(x) | H(x,f(x)) | -G(y) | -H(x,y) | K(y).
** KEPT: 16 (2,5,10,11) H(a,f(a)) | K(g(a)).
new given clause: 16 (2,5,10,11) H(a,f(a)) | K(g(a)).
** KEPT: 17 (16,7,15) K(g(a)) | J(a,f(a)).
** KEPT: 18 (16,6) K(g(a)) | L(f(a)).
** KEPT: 19 (16,4,12) H(a,f(a)).
19 back subsumes: 16 (2,5,10,11) H(a,f(a)) | K(g(a)).
new given clause: 19 (16,4,12) H(a,f(a)).
** KEPT: 20 (19,7,15) J(a,f(a)).
** KEPT: 21 (19,6) L(f(a)).
20 back subsumes: 17 (16,7,15) K(g(a)) | J(a,f(a)).
21 back subsumes: 18 (16,6) K(g(a)) | L(f(a)).
new given clause: 21 (19,6) L(f(a)).
new given clause: 20 (19,7,15) J(a,f(a)).
new given clause: 3 -F(x) | -J(x,f(x)) | -G(y) | -H(x,y) | K(y).
** KEPT: 22 (3,5,20,15,19) K(f(a)).
** KEPT: 23 (3,5,20,10,11) K(g(a)).
new given clause: 22 (3,5,20,15,19) K(f(a)).
** KEPT: 24 (22,4,21) .
------------> EMPTY CLAUSE -----------> 24 (22,4,21) .
------------ END OF SEARCH ------------
---------------- PROOF ----------------
1 -F(x) | G(f(x)) | -G(y) | -H(x,y) | K(y).
2 -F(x) | H(x,f(x)) | -G(y) | -H(x,y) | K(y).
3 -F(x) | -J(x,f(x)) | -G(y) | -H(x,y) | K(y).
4 -L(x) | -K(x).
5 F(a).
6 -H(a,x) | L(x).
7 -G(x) | -H(a,x) | J(a,x).
8 -F(x) | G(g(x)).
9 -F(x) | H(x,g(x)).
10 (8,5) G(g(a)).
11 (9,5) H(a,g(a)).
12 (11,6) L(g(a)).
14 (1,5,10,11) G(f(a)) | K(g(a)).
15 (14,4,12) G(f(a)).
16 (2,5,10,11) H(a,f(a)) | K(g(a)).
19 (16,4,12) H(a,f(a)).
20 (19,7,15) J(a,f(a)).
21 (19,6) L(f(a)).
22 (3,5,20,15,19) K(f(a)).
24 (22,4,21) .
--------------- 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).
clear(order_eq).
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, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).
------------- memory usage ------------
1 mallocs of 32700 bytes each (31.9+ K)
type (bytes each) gets frees in use avail bytes
sym_ent ( 64) 16 0 16 0 1.0 K
term ( 16) 277 225 52 19 1.1 K
rel ( 20) 180 116 64 3 1.3 K
term_ptr ( 8) 292 47 245 0 1.9 K
fpa_head ( 12) 114 10 104 0 1.2 K
fpa_tree ( 28) 164 164 0 14 0.4 K
context ( 260) 123 123 0 6 1.5 K
trail ( 12) 35 35 0 2 0.0 K
imd_tree ( 24) 0 0 0 0 0.0 K
imd_pos ( 416) 0 0 0 0 0.0 K
is_tree ( 12) 63 4 59 0 0.7 K
is_pos (1216) 27 27 0 2 2.4 K
fsub_pos ( 8) 23 23 0 1 0.0 K
literal ( 16) 87 42 45 2 0.7 K
clause ( 28) 29 5 24 0 0.7 K
list ( 60) 2 0 2 0 0.1 K
clash_nd ( 32) 38 38 0 4 0.1 K
clause_ptr ( 8) 48 24 24 20 0.3 K
int_ptr ( 8) 62 16 46 0 0.4 K
-------------- statistics -------------
clauses input 9
clauses given 20
clauses generated 19
demodulation rewrites 0
clauses wt or lit delete 0
tautologies deleted 0
clauses forward subsumed 4
(clauses subsumed by sos) 0
unit deletions 0
clauses kept 15
empty clauses 1
factors generated 0
clauses back subsumed 4
clauses not processed 1
----------- times (seconds) -----------
run time 0.49
input time 0.10
binary_res time 0.00
hyper_res time 0.07
UR_res time 0.00
para_into time 0.00
para_from time 0.00
pre_process time 0.08
demod time 0.00
weigh time 0.00
for_sub time 0.01
unit_del time 0.00
post_process time 0.04
back_sub time 0.01
conflict time 0.01
factor time 0.00
FPA build time 0.04
IS build time 0.01
print_cl time 0.13
cl integrate time 0.01
window time 0.00
SHAR_EOF
if test -f 'thf7.desc'
then
echo shar: over-writing existing file "'thf7.desc'"
fi
cat << \SHAR_EOF > 'thf7.desc'
problem-set/pelletier/full.predicate/thf7.desc
created : 07/25/86
revised : 07/28/88
Natural Language Description:
Full Predicate Logic (without Identities and Functions).
(Ax)(Fx & (Ay)[Fy & Hyx -> Gy] -> Gx)
{(Ex)(Fx & -Gx) ->
(Ex)(Fx & -Gx & (Ay)(Fy & -Gy -> Jxy)}
(Ax)(Ay)(Fx & Fy & Hxy -> -Jyx)
--------------------------------
(Ax)(Fx -> Gx)
Versions:
thf1.desc - declarative representation.
created by : From Pelletier paper, 1986.
verified for ITP : untested, 07/25/86
translated for OTTER by : K.R.
verified for OTTER : untested
SHAR_EOF
if test -f 'thf7.ver1.clauses'
then
echo shar: over-writing existing file "'thf7.ver1.clauses'"
fi
cat << \SHAR_EOF > 'thf7.ver1.clauses'
% problem-set/pelletier/full.predicate/thf7.ver1.clauses
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identities and Functions)..
% (Ax)(Fx & (Ay)[Fy & Hyx -> Gy] -> Gx).
% {(Ex)(Fx & -Gx) ->.
% (Ex)(Fx & -Gx & (Ay)(Fy & -Gy -> Jxy)}.
% (Ax)(Ay)(Fx & Fy & Hxy -> -Jyx).
% --------------------------------.
% (Ax)(Fx -> Gx).
% representation:
%
% Declarative version
% declare_predicates(2,[H,J]).
% declare_predicates(1,[F,G]).
% declare_function(1,f).
% declare_variables([x,y]).
% declare_constants([a,b]).
% clauses .
-F(x) | F(f(x)) | G(x).
-F(x) | H(f(x),x)| G(x).
-F(x) | -G(f(x)) | G(x).
-F(a) | G(a) | F(b).
-F(a) | G(a) | -G(b).
-F(a) | G(a) | -F(y) | G(y) | J(b,y).
-F(x) | -F(y) | -H(x,y) | J(y,x).
F(c).
-G(c).
SHAR_EOF
if test -f 'thf7.ver1.in'
then
echo shar: over-writing existing file "'thf7.ver1.in'"
fi
cat << \SHAR_EOF > 'thf7.ver1.in'
% problem-set/pelletier/full.predicate/thf7.ver1.in
% created : 07/25/86
% revised : 07/28/88
% description:
%
% Full Predicate Logic (without Identities and Functions)..
% (Ax)(Fx & (Ay)[Fy & Hyx -> Gy] -> Gx).
% {(Ex)(Fx & -Gx) ->.
% (Ex)(Fx & -Gx & (Ay)(Fy & -Gy -> Jxy)}.
% (Ax)(Ay)(Fx & Fy & Hxy -> -Jyx).
% --------------------------------.
% (Ax)(Fx -> Gx).
% representation:
%
% Declarative version
% declare_predicates(2,[H,J]).
% declare_predicates(1,[F,G]).
% declare_function(1,f).
% declare_variables([x,y]).
% declare_constants([a,b]).
% clauses .
set(binary_res).
set(factor).
list(sos).
-F(x) | F(f(x)) | G(x).
-F(x) | H(f(x),x)| G(x).
-F(x) | -G(f(x)) | G(x).
-F(a) | G(a) | F(b).
-F(a) | G(a) | -G(b).
-F(a) | G(a) | -F(y) | G(y) | J(b,y).
-F(x) | -F(y) | -H(x,y) | J(y,x).
F(c).
-G(c).
end_of_list.
SHAR_EOF
if test -f 'thf7.ver1.out'
then
echo shar: over-writing existing file "'thf7.ver1.out'"
fi
cat << \SHAR_EOF > 'thf7.ver1.out'
problem-set/pelletier/full.predicate/thf7.ver1.out
created : 07/28/88
revised : 07/28/88
OTTER version 0.91, 14 June 1988.
set(UR_res).
list(sos).
1 -F(x) | F(f(x)) | G(x).
2 -F(x) | H(f(x),x) | G(x).
3 -F(x) | -G(f(x)) | G(x).
4 -F(a) | G(a) | F(b).
5 -F(a) | G(a) | -G(b).
6 -F(a) | G(a) | -F(y) | G(y) | J(b,y).
7 -F(x) | -F(y) | -H(x,y) | J(y,x).
8 F(c).
9 -G(c).
end_of_list.
new given clause: 8 F(c).
new given clause: 9 -G(c).
new given clause: 4 -F(a) | G(a) | F(b).
new given clause: 5 -F(a) | G(a) | -G(b).
new given clause: 1 -F(x) | F(f(x)) | G(x).
** KEPT: 10 (1,8,9) F(f(c)).
new given clause: 10 (1,8,9) F(f(c)).
new given clause: 3 -F(x) | -G(f(x)) | G(x).
** KEPT: 11 (3,8,9) -G(f(c)).
new given clause: 11 (3,8,9) -G(f(c)).
** KEPT: 12 (11,3,10) -G(f(f(c))).
** KEPT: 13 (11,1,10) F(f(f(c))).
new given clause: 12 (11,3,10) -G(f(f(c))).
new given clause: 13 (11,1,10) F(f(f(c))).
** KEPT: 14 (13,3,12) -G(f(f(f(c)))).
** KEPT: 15 (13,1,12) F(f(f(f(c)))).
new given clause: 14 (13,3,12) -G(f(f(f(c)))).
new given clause: 15 (13,1,12) F(f(f(f(c)))).
** KEPT: 16 (15,3,14) -G(f(f(f(f(c))))).
** KEPT: 17 (15,1,14) F(f(f(f(f(c))))).
new given clause: 16 (15,3,14) -G(f(f(f(f(c))))).
new given clause: 17 (15,1,14) F(f(f(f(f(c))))).
** KEPT: 18 (17,3,16) -G(f(f(f(f(f(c)))))).
** KEPT: 19 (17,1,16) F(f(f(f(f(f(c)))))).
new given clause: 18 (17,3,16) -G(f(f(f(f(f(c)))))).
new given clause: 19 (17,1,16) F(f(f(f(f(f(c)))))).
** KEPT: 20 (19,3,18) -G(f(f(f(f(f(f(c))))))).
** KEPT: 21 (19,1,18) F(f(f(f(f(f(f(c))))))).
new given clause: 2 -F(x) | H(f(x),x) | G(x).
** KEPT: 22 (2,19,18) H(f(f(f(f(f(f(c)))))),f(f(f(f(f(c)))))).
** KEPT: 23 (2,17,16) H(f(f(f(f(f(c))))),f(f(f(f(c))))).
** KEPT: 24 (2,15,14) H(f(f(f(f(c)))),f(f(f(c)))).
** KEPT: 25 (2,13,12) H(f(f(f(c))),f(f(c))).
** KEPT: 26 (2,10,11) H(f(f(c)),f(c)).
** KEPT: 27 (2,8,9) H(f(c),c).
new given clause: 27 (2,8,9) H(f(c),c).
new given clause: 26 (2,10,11) H(f(f(c)),f(c)).
new given clause: 20 (19,3,18) -G(f(f(f(f(f(f(c))))))).
new given clause: 21 (19,1,18) F(f(f(f(f(f(f(c))))))).
** KEPT: 28 (21,3,20) -G(f(f(f(f(f(f(f(c)))))))).
** KEPT: 29 (21,2,20) H(f(f(f(f(f(f(f(c))))))),f(f(f(f(f(f(c))))))).
** KEPT: 30 (21,1,20) F(f(f(f(f(f(f(f(c)))))))).
new given clause: 25 (2,13,12) H(f(f(f(c))),f(f(c))).
new given clause: 28 (21,3,20) -G(f(f(f(f(f(f(f(c)))))))).
new given clause: 30 (21,1,20) F(f(f(f(f(f(f(f(c)))))))).
** KEPT: 31 (30,3,28) -G(f(f(f(f(f(f(f(f(c))))))))).
** KEPT: 32 (30,2,28) H(f(f(f(f(f(f(f(f(c)))))))),f(f(f(f(f(f(f(c)))))))).
** KEPT: 33 (30,1,28) F(f(f(f(f(f(f(f(f(c))))))))).
new given clause: 7 -F(x) | -F(y) | -H(x,y) | J(y,x).
** KEPT: 34 (7,15,13,25) J(f(f(c)),f(f(f(c)))).
** KEPT: 35 (7,13,10,26) J(f(c),f(f(c))).
** KEPT: 36 (7,10,8,27) J(c,f(c)).
new given clause: 36 (7,10,8,27) J(c,f(c)).
new given clause: 35 (7,13,10,26) J(f(c),f(f(c))).
new given clause: 34 (7,15,13,25) J(f(f(c)),f(f(f(c)))).
new given clause: 24 (2,15,14) H(f(f(f(f(c)))),f(f(f(c)))).
** KEPT: 37 (24,7,17,15) J(f(f(f(c))),f(f(f(f(c))))).
new given clause: 31 (30,3,28) -G(f(f(f(f(f(f(f(f(c))))))))).
new given clause: 33 (30,1,28) F(f(f(f(f(f(f(f(f(c))))))))).
** KEPT: 38 (33,3,31) -G(f(f(f(f(f(f(f(f(f(c)))))))))).
** KEPT: 39 (33,2,31) H(f(f(f(f(f(f(f(f(f(c))))))))),f(f(f(f(f(f(f(f(c))))))))).
** KEPT: 40 (33,1,31) F(f(f(f(f(f(f(f(f(f(c)))))))))).
new given clause: 37 (24,7,17,15) J(f(f(f(c))),f(f(f(f(c))))).
new given clause: 6 -F(a) | G(a) | -F(y) | G(y) | J(b,y).
new given clause: 38 (33,3,31) -G(f(f(f(f(f(f(f(f(f(c)))))))))).
new given clause: 40 (33,1,31) F(f(f(f(f(f(f(f(f(f(c)))))))))).
** KEPT: 41 (40,3,38) -G(f(f(f(f(f(f(f(f(f(f(c))))))))))).
** KEPT: 42 (40,2,38) H(f(f(f(f(f(f(f(f(f(f(c)))))))))),f(f(f(f(f(f(f(f(f(c)))))))))).
** KEPT: 43 (40,1,38) F(f(f(f(f(f(f(f(f(f(f(c))))))))))).
new given clause: 23 (2,17,16) H(f(f(f(f(f(c))))),f(f(f(f(c))))).
** KEPT: 44 (23,7,19,17) J(f(f(f(f(c)))),f(f(f(f(f(c)))))).
new given clause: 41 (40,3,38) -G(f(f(f(f(f(f(f(f(f(f(c))))))))))).
new given clause: 43 (40,1,38) F(f(f(f(f(f(f(f(f(f(f(c))))))))))).
** KEPT: 45 (43,3,41) -G(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))).
** KEPT: 46 (43,2,41) H(f(f(f(f(f(f(f(f(f(f(f(c))))))))))),f(f(f(f(f(f(f(f(f(f(c))))))))))).
** KEPT: 47 (43,1,41) F(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))).
new given clause: 44 (23,7,19,17) J(f(f(f(f(c)))),f(f(f(f(f(c)))))).
new given clause: 45 (43,3,41) -G(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))).
new given clause: 47 (43,1,41) F(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))).
** KEPT: 48 (47,3,45) -G(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))).
** KEPT: 49 (47,2,45) H(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))),f(f(f(f(f(f(f(f(f(f(f(c)))))))))))).
** KEPT: 50 (47,1,45) F(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))).
new given clause: 22 (2,19,18) H(f(f(f(f(f(f(c)))))),f(f(f(f(f(c)))))).
** KEPT: 51 (22,7,21,19) J(f(f(f(f(f(c))))),f(f(f(f(f(f(c))))))).
new given clause: 48 (47,3,45) -G(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))).
new given clause: 50 (47,1,45) F(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))).
** KEPT: 52 (50,3,48) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))).
** KEPT: 53 (50,2,48) H(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))).
** KEPT: 54 (50,1,48) F(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))).
new given clause: 51 (22,7,21,19) J(f(f(f(f(f(c))))),f(f(f(f(f(f(c))))))).
new given clause: 52 (50,3,48) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))).
new given clause: 54 (50,1,48) F(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))).
** KEPT: 55 (54,3,52) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))).
** KEPT: 56 (54,2,52) H(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))).
** KEPT: 57 (54,1,52) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))).
new given clause: 29 (21,2,20) H(f(f(f(f(f(f(f(c))))))),f(f(f(f(f(f(c))))))).
** KEPT: 58 (29,7,30,21) J(f(f(f(f(f(f(c)))))),f(f(f(f(f(f(f(c)))))))).
new given clause: 55 (54,3,52) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))).
new given clause: 57 (54,1,52) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))).
** KEPT: 59 (57,3,55) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))).
** KEPT: 60 (57,2,55) H(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))).
** KEPT: 61 (57,1,55) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))).
new given clause: 58 (29,7,30,21) J(f(f(f(f(f(f(c)))))),f(f(f(f(f(f(f(c)))))))).
new given clause: 59 (57,3,55) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))).
new given clause: 61 (57,1,55) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))).
** KEPT: 62 (61,3,59) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))).
** KEPT: 63 (61,2,59) H(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))).
** KEPT: 64 (61,1,59) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))).
new given clause: 32 (30,2,28) H(f(f(f(f(f(f(f(f(c)))))))),f(f(f(f(f(f(f(c)))))))).
** KEPT: 65 (32,7,33,30) J(f(f(f(f(f(f(f(c))))))),f(f(f(f(f(f(f(f(c))))))))).
new given clause: 62 (61,3,59) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))).
new given clause: 64 (61,1,59) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))).
** KEPT: 66 (64,3,62) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))).
** KEPT: 67 (64,2,62) H(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))).
** KEPT: 68 (64,1,62) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))).
new given clause: 65 (32,7,33,30) J(f(f(f(f(f(f(f(c))))))),f(f(f(f(f(f(f(f(c))))))))).
new given clause: 66 (64,3,62) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))).
new given clause: 68 (64,1,62) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))).
** KEPT: 69 (68,3,66) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))).
** KEPT: 70 (68,2,66) H(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))).
** KEPT: 71 (68,1,66) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))).
new given clause: 39 (33,2,31) H(f(f(f(f(f(f(f(f(f(c))))))))),f(f(f(f(f(f(f(f(c))))))))).
** KEPT: 72 (39,7,40,33) J(f(f(f(f(f(f(f(f(c)))))))),f(f(f(f(f(f(f(f(f(c)))))))))).
new given clause: 69 (68,3,66) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))).
new given clause: 71 (68,1,66) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))).
** KEPT: 73 (71,3,69) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))).
** KEPT: 74 (71,2,69) H(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))).
** KEPT: 75 (71,1,69) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))).
new given clause: 72 (39,7,40,33) J(f(f(f(f(f(f(f(f(c)))))))),f(f(f(f(f(f(f(f(f(c)))))))))).
new given clause: 73 (71,3,69) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))).
new given clause: 75 (71,1,69) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))).
** KEPT: 76 (75,3,73) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))).
** KEPT: 77 (75,2,73) H(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))).
** KEPT: 78 (75,1,73) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))).
new given clause: 42 (40,2,38) H(f(f(f(f(f(f(f(f(f(f(c)))))))))),f(f(f(f(f(f(f(f(f(c)))))))))).
** KEPT: 79 (42,7,43,40) J(f(f(f(f(f(f(f(f(f(c))))))))),f(f(f(f(f(f(f(f(f(f(c))))))))))).
new given clause: 76 (75,3,73) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))).
new given clause: 78 (75,1,73) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))).
** KEPT: 80 (78,3,76) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))))).
** KEPT: 81 (78,2,76) H(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))).
** KEPT: 82 (78,1,76) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))))).
new given clause: 79 (42,7,43,40) J(f(f(f(f(f(f(f(f(f(c))))))))),f(f(f(f(f(f(f(f(f(f(c))))))))))).
new given clause: 80 (78,3,76) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))))).
new given clause: 82 (78,1,76) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))))).
** KEPT: 83 (82,3,80) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))))).
** KEPT: 84 (82,2,80) H(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))))).
** KEPT: 85 (82,1,80) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))))).
new given clause: 46 (43,2,41) H(f(f(f(f(f(f(f(f(f(f(f(c))))))))))),f(f(f(f(f(f(f(f(f(f(c))))))))))).
** KEPT: 86 (46,7,47,43) J(f(f(f(f(f(f(f(f(f(f(c)))))))))),f(f(f(f(f(f(f(f(f(f(f(c)))))))))))).
new given clause: 83 (82,3,80) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))))).
new given clause: 85 (82,1,80) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))))).
** KEPT: 87 (85,3,83) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))))))).
** KEPT: 88 (85,2,83) H(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))))),f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c))))))))))))))))))))))).
** KEPT: 89 (85,1,83) F(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))))))).
new given clause: 86 (46,7,47,43) J(f(f(f(f(f(f(f(f(f(f(c)))))))))),f(f(f(f(f(f(f(f(f(f(f(c)))))))))))).
new given clause: 87 (85,3,83) -G(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(c)))))))))))))))))))))))).
SHAR_EOF
# End of shell archive
exit 0