#!/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