%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN740-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:48:46 EDT 2024
% Result : Satisfiable 0.59s 0.77s
% Output : Saturation 0.59s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssRr(X2,skf1(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(clause31,negated_conjecture,
( ~ ssRr(X275,X277)
| ~ ssPv2(X277)
| ~ ssRr(X275,X274)
| ~ ssPv1(X274)
| ~ ssRr(X275,X276)
| ~ ssPv2(X275)
| ssPv4(X276) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(c110,plain,
( ~ ssRr(X336,X337)
| ~ ssPv2(X337)
| ~ ssRr(X336,X338)
| ~ ssPv1(X338)
| ~ ssPv2(X336)
| ssPv4(skf1(X336)) ),
inference(resolution,[status(thm)],[clause31,clause1]) ).
cnf(c132,plain,
( ~ ssRr(X339,X340)
| ~ ssPv2(X340)
| ~ ssPv1(X340)
| ~ ssPv2(X339)
| ssPv4(skf1(X339)) ),
inference(factor,[status(thm)],[c110]) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X258,X260)
| ~ ssPv2(X260)
| ~ ssRr(X258,X257)
| ~ ssPv1(X257)
| ~ ssRr(X258,X259)
| ~ ssPv1(X258)
| ssPv1(X259) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
cnf(c103,plain,
( ~ ssRr(X327,X326)
| ~ ssPv2(X326)
| ~ ssRr(X327,X325)
| ~ ssPv1(X325)
| ~ ssPv1(X327)
| ssPv1(skf1(X327)) ),
inference(resolution,[status(thm)],[clause30,clause1]) ).
cnf(c128,plain,
( ~ ssRr(X331,X330)
| ~ ssPv2(X330)
| ~ ssPv1(X330)
| ~ ssPv1(X331)
| ssPv1(skf1(X331)) ),
inference(factor,[status(thm)],[c103]) ).
cnf(clause29,negated_conjecture,
( ~ ssRr(X242,X244)
| ~ ssPv4(X244)
| ~ ssRr(X242,X241)
| ~ ssPv3(X241)
| ~ ssRr(X242,X243)
| ~ ssPv1(X242)
| ssPv4(X243) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
cnf(c98,plain,
( ~ ssRr(X322,X324)
| ~ ssPv4(X324)
| ~ ssRr(X322,X323)
| ~ ssPv3(X323)
| ~ ssPv1(X322)
| ssPv4(skf1(X322)) ),
inference(resolution,[status(thm)],[clause29,clause1]) ).
cnf(c126,plain,
( ~ ssRr(X329,X328)
| ~ ssPv4(X328)
| ~ ssPv3(X328)
| ~ ssPv1(X329)
| ssPv4(skf1(X329)) ),
inference(factor,[status(thm)],[c98]) ).
cnf(clause28,negated_conjecture,
( ~ ssRr(X226,X228)
| ~ ssPv3(X228)
| ~ ssRr(X226,X225)
| ~ ssPv2(X225)
| ~ ssRr(X226,X227)
| ~ ssPv2(X226)
| ssPv3(X227) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
cnf(c93,plain,
( ~ ssRr(X312,X313)
| ~ ssPv3(X313)
| ~ ssRr(X312,X314)
| ~ ssPv2(X314)
| ~ ssPv2(X312)
| ssPv3(skf1(X312)) ),
inference(resolution,[status(thm)],[clause28,clause1]) ).
cnf(c123,plain,
( ~ ssRr(X316,X315)
| ~ ssPv3(X315)
| ~ ssPv2(X315)
| ~ ssPv2(X316)
| ssPv3(skf1(X316)) ),
inference(factor,[status(thm)],[c93]) ).
cnf(c109,plain,
( ~ ssRr(X299,X298)
| ~ ssPv2(X298)
| ~ ssRr(X299,X297)
| ~ ssPv1(X297)
| ~ ssPv2(X299)
| ssPv4(X297) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c119,plain,
( ~ ssRr(X310,X311)
| ~ ssPv2(X311)
| ~ ssPv1(skf1(X310))
| ~ ssPv2(X310)
| ssPv4(skf1(X310)) ),
inference(resolution,[status(thm)],[c109,clause1]) ).
cnf(clause27,negated_conjecture,
( ~ ssRr(X209,X211)
| ~ ssPv2(X211)
| ~ ssRr(X209,X208)
| ~ ssPv1(X208)
| ~ ssRr(X209,X210)
| ssPv2(X210)
| ssPv1(X209) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
cnf(c88,plain,
( ~ ssRr(X300,X302)
| ~ ssPv2(X302)
| ~ ssRr(X300,X301)
| ~ ssPv1(X301)
| ssPv2(skf1(X300))
| ssPv1(X300) ),
inference(resolution,[status(thm)],[clause27,clause1]) ).
cnf(c120,plain,
( ~ ssRr(X305,X306)
| ~ ssPv2(X306)
| ~ ssPv1(X306)
| ssPv2(skf1(X305))
| ssPv1(X305) ),
inference(factor,[status(thm)],[c88]) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X194,X196)
| ~ ssPv3(X196)
| ~ ssRr(X194,X193)
| ~ ssPv1(X193)
| ~ ssRr(X194,X195)
| ssPv1(X195)
| ssPv3(X194) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(c81,plain,
( ~ ssRr(X289,X288)
| ~ ssPv3(X288)
| ~ ssRr(X289,X290)
| ~ ssPv1(X290)
| ssPv1(skf1(X289))
| ssPv3(X289) ),
inference(resolution,[status(thm)],[clause26,clause1]) ).
cnf(c115,plain,
( ~ ssRr(X295,X294)
| ~ ssPv3(X294)
| ~ ssPv1(X294)
| ssPv1(skf1(X295))
| ssPv3(X295) ),
inference(factor,[status(thm)],[c81]) ).
cnf(c108,plain,
( ~ ssRr(X285,X284)
| ~ ssPv2(X284)
| ~ ssRr(X285,X283)
| ~ ssPv1(X283)
| ~ ssPv2(X285)
| ssPv4(X284) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c112,plain,
( ~ ssRr(X287,X286)
| ~ ssPv2(X286)
| ~ ssPv1(X286)
| ~ ssPv2(X287)
| ssPv4(X286) ),
inference(factor,[status(thm)],[c108]) ).
cnf(c114,plain,
( ~ ssPv2(skf1(X293))
| ~ ssPv1(skf1(X293))
| ~ ssPv2(X293)
| ssPv4(skf1(X293)) ),
inference(resolution,[status(thm)],[c112,clause1]) ).
cnf(c113,plain,
( ~ ssRr(X291,X292)
| ~ ssPv2(X292)
| ~ ssPv1(skf1(X291))
| ~ ssPv2(X291)
| ssPv4(X292) ),
inference(resolution,[status(thm)],[c108,clause1]) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X180,X182)
| ~ ssPv4(X182)
| ~ ssRr(X180,X179)
| ~ ssPv2(X179)
| ~ ssRr(X180,X181)
| ssPv3(X181)
| ssPv4(X180) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(c75,plain,
( ~ ssRr(X271,X272)
| ~ ssPv4(X272)
| ~ ssRr(X271,X273)
| ~ ssPv2(X273)
| ssPv3(skf1(X271))
| ssPv4(X271) ),
inference(resolution,[status(thm)],[clause25,clause1]) ).
cnf(c106,plain,
( ~ ssRr(X278,X279)
| ~ ssPv4(X279)
| ~ ssPv2(X279)
| ssPv3(skf1(X278))
| ssPv4(X278) ),
inference(factor,[status(thm)],[c75]) ).
cnf(c101,plain,
( ~ ssRr(X261,X263)
| ~ ssPv2(X263)
| ~ ssRr(X261,X262)
| ~ ssPv1(X262)
| ~ ssPv1(X261)
| ssPv1(X263) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c105,plain,
( ~ ssRr(X266,X267)
| ~ ssPv2(X267)
| ~ ssPv1(skf1(X266))
| ~ ssPv1(X266)
| ssPv1(X267) ),
inference(resolution,[status(thm)],[c101,clause1]) ).
cnf(c97,plain,
( ~ ssRr(X251,X252)
| ~ ssPv4(X252)
| ~ ssRr(X251,X250)
| ~ ssPv3(X250)
| ~ ssPv1(X251)
| ssPv4(X250) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c100,plain,
( ~ ssRr(X255,X256)
| ~ ssPv4(X256)
| ~ ssPv3(skf1(X255))
| ~ ssPv1(X255)
| ssPv4(skf1(X255)) ),
inference(resolution,[status(thm)],[c97,clause1]) ).
cnf(c92,plain,
( ~ ssRr(X238,X237)
| ~ ssPv3(X237)
| ~ ssRr(X238,X236)
| ~ ssPv2(X236)
| ~ ssPv2(X238)
| ssPv3(X236) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c95,plain,
( ~ ssRr(X245,X246)
| ~ ssPv3(X246)
| ~ ssPv2(skf1(X245))
| ~ ssPv2(X245)
| ssPv3(skf1(X245)) ),
inference(resolution,[status(thm)],[c92,clause1]) ).
cnf(c87,plain,
( ~ ssRr(X224,X222)
| ~ ssPv2(X222)
| ~ ssRr(X224,X223)
| ~ ssPv1(X223)
| ssPv2(X223)
| ssPv1(X224) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c90,plain,
( ~ ssRr(X231,X232)
| ~ ssPv2(X232)
| ~ ssPv1(skf1(X231))
| ssPv2(skf1(X231))
| ssPv1(X231) ),
inference(resolution,[status(thm)],[c87,clause1]) ).
cnf(c74,plain,
( ~ ssRr(X198,X200)
| ~ ssPv4(X200)
| ~ ssRr(X198,X199)
| ~ ssPv2(X199)
| ssPv3(X199)
| ssPv4(X198) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c83,plain,
( ~ ssRr(X217,X218)
| ~ ssPv4(X218)
| ~ ssPv2(skf1(X217))
| ssPv3(skf1(X217))
| ssPv4(X217) ),
inference(resolution,[status(thm)],[c74,clause1]) ).
cnf(c79,plain,
( ~ ssRr(X204,X203)
| ~ ssPv3(X203)
| ~ ssRr(X204,X205)
| ~ ssPv1(X205)
| ssPv1(X203)
| ssPv3(X204) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c85,plain,
( ~ ssRr(X212,X213)
| ~ ssPv3(X213)
| ~ ssPv1(skf1(X212))
| ssPv1(X213)
| ssPv3(X212) ),
inference(resolution,[status(thm)],[c79,clause1]) ).
cnf(c73,plain,
( ~ ssRr(X186,X187)
| ~ ssPv4(X187)
| ~ ssRr(X186,X188)
| ~ ssPv2(X188)
| ssPv3(X187)
| ssPv4(X186) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c76,plain,
( ~ ssRr(X189,X190)
| ~ ssPv4(X190)
| ~ ssPv2(X190)
| ssPv3(X190)
| ssPv4(X189) ),
inference(factor,[status(thm)],[c73]) ).
cnf(c78,plain,
( ~ ssPv4(skf1(X197))
| ~ ssPv2(skf1(X197))
| ssPv3(skf1(X197))
| ssPv4(X197) ),
inference(resolution,[status(thm)],[c76,clause1]) ).
cnf(c77,plain,
( ~ ssRr(X192,X191)
| ~ ssPv4(X191)
| ~ ssPv2(skf1(X192))
| ssPv3(X191)
| ssPv4(X192) ),
inference(resolution,[status(thm)],[c73,clause1]) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X175,X176)
| ~ ssPv2(X176)
| ~ ssRr(X175,X174)
| ~ ssPv1(X174)
| ~ ssPv1(X175)
| ~ ssPv2(X175) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(c71,plain,
( ~ ssRr(X185,X184)
| ~ ssPv2(X184)
| ~ ssPv1(skf1(X185))
| ~ ssPv1(X185)
| ~ ssPv2(X185) ),
inference(resolution,[status(thm)],[clause24,clause1]) ).
cnf(c70,plain,
( ~ ssRr(X178,X177)
| ~ ssPv2(X177)
| ~ ssPv1(X177)
| ~ ssPv1(X178)
| ~ ssPv2(X178) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c72,plain,
( ~ ssPv2(skf1(X183))
| ~ ssPv1(skf1(X183))
| ~ ssPv1(X183)
| ~ ssPv2(X183) ),
inference(resolution,[status(thm)],[c70,clause1]) ).
cnf(clause23,negated_conjecture,
( ~ ssRr(X167,X168)
| ~ ssPv4(X168)
| ~ ssRr(X167,X166)
| ~ ssPv2(X166)
| ~ ssPv1(X167)
| ~ ssPv2(X167) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
cnf(c68,plain,
( ~ ssRr(X172,X173)
| ~ ssPv4(X173)
| ~ ssPv2(skf1(X172))
| ~ ssPv1(X172)
| ~ ssPv2(X172) ),
inference(resolution,[status(thm)],[clause23,clause1]) ).
cnf(c67,plain,
( ~ ssRr(X169,X170)
| ~ ssPv4(X170)
| ~ ssPv2(X170)
| ~ ssPv1(X169)
| ~ ssPv2(X169) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c69,plain,
( ~ ssPv4(skf1(X171))
| ~ ssPv2(skf1(X171))
| ~ ssPv1(X171)
| ~ ssPv2(X171) ),
inference(resolution,[status(thm)],[c67,clause1]) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X156,X157)
| ~ ssPv4(X157)
| ~ ssRr(X156,X155)
| ~ ssPv1(X155)
| ~ ssPv1(X156)
| ssPv2(X156) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
cnf(c65,plain,
( ~ ssRr(X164,X165)
| ~ ssPv4(X165)
| ~ ssPv1(skf1(X164))
| ~ ssPv1(X164)
| ssPv2(X164) ),
inference(resolution,[status(thm)],[clause22,clause1]) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X151,X152)
| ~ ssPv4(X152)
| ~ ssRr(X151,X150)
| ~ ssPv2(X150)
| ~ ssPv4(X151)
| ssPv2(X151) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(c62,plain,
( ~ ssRr(X162,X163)
| ~ ssPv4(X163)
| ~ ssPv2(skf1(X162))
| ~ ssPv4(X162)
| ssPv2(X162) ),
inference(resolution,[status(thm)],[clause21,clause1]) ).
cnf(c64,plain,
( ~ ssRr(X160,X159)
| ~ ssPv4(X159)
| ~ ssPv1(X159)
| ~ ssPv1(X160)
| ssPv2(X160) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c66,plain,
( ~ ssPv4(skf1(X161))
| ~ ssPv1(skf1(X161))
| ~ ssPv1(X161)
| ssPv2(X161) ),
inference(resolution,[status(thm)],[c64,clause1]) ).
cnf(c61,plain,
( ~ ssRr(X153,X154)
| ~ ssPv4(X154)
| ~ ssPv2(X154)
| ~ ssPv4(X153)
| ssPv2(X153) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c63,plain,
( ~ ssPv4(skf1(X158))
| ~ ssPv2(skf1(X158))
| ~ ssPv4(X158)
| ssPv2(X158) ),
inference(resolution,[status(thm)],[c61,clause1]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X143,X144)
| ~ ssPv1(X144)
| ~ ssRr(X143,X142)
| ~ ssPv2(X143)
| ~ ssPv3(X143)
| ssPv1(X142) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c59,plain,
( ~ ssRr(X147,X148)
| ~ ssPv1(X148)
| ~ ssPv2(X147)
| ~ ssPv3(X147)
| ssPv1(skf1(X147)) ),
inference(resolution,[status(thm)],[clause20,clause1]) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X133,X134)
| ~ ssPv3(X134)
| ~ ssRr(X133,X132)
| ~ ssPv2(X133)
| ~ ssPv3(X133)
| ssPv1(X132) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(c55,plain,
( ~ ssRr(X139,X140)
| ~ ssPv3(X140)
| ~ ssPv2(X139)
| ~ ssPv3(X139)
| ssPv1(skf1(X139)) ),
inference(resolution,[status(thm)],[clause19,clause1]) ).
cnf(c54,plain,
( ~ ssRr(X136,X137)
| ~ ssPv3(X137)
| ~ ssPv2(X136)
| ~ ssPv3(X136)
| ssPv1(X137) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c56,plain,
( ~ ssPv3(skf1(X138))
| ~ ssPv2(X138)
| ~ ssPv3(X138)
| ssPv1(skf1(X138)) ),
inference(resolution,[status(thm)],[c54,clause1]) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X122,X123)
| ~ ssPv4(X123)
| ~ ssRr(X122,X121)
| ~ ssPv2(X122)
| ~ ssPv3(X122)
| ssPv3(X121) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(c50,plain,
( ~ ssRr(X130,X131)
| ~ ssPv4(X131)
| ~ ssPv2(X130)
| ~ ssPv3(X130)
| ssPv3(skf1(X130)) ),
inference(resolution,[status(thm)],[clause18,clause1]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X112,X113)
| ~ ssPv3(X113)
| ~ ssRr(X112,X111)
| ~ ssPv2(X112)
| ~ ssPv4(X112)
| ssPv1(X111) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(c46,plain,
( ~ ssRr(X127,X128)
| ~ ssPv3(X128)
| ~ ssPv2(X127)
| ~ ssPv4(X127)
| ssPv1(skf1(X127)) ),
inference(resolution,[status(thm)],[clause17,clause1]) ).
cnf(c49,plain,
( ~ ssRr(X125,X124)
| ~ ssPv4(X124)
| ~ ssPv2(X125)
| ~ ssPv3(X125)
| ssPv3(X124) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c51,plain,
( ~ ssPv4(skf1(X126))
| ~ ssPv2(X126)
| ~ ssPv3(X126)
| ssPv3(skf1(X126)) ),
inference(resolution,[status(thm)],[c49,clause1]) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X107,X108)
| ~ ssPv4(X108)
| ~ ssRr(X107,X106)
| ~ ssPv3(X107)
| ssPv2(X106)
| ssPv1(X107) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
cnf(c43,plain,
( ~ ssRr(X118,X119)
| ~ ssPv4(X119)
| ~ ssPv3(X118)
| ssPv2(skf1(X118))
| ssPv1(X118) ),
inference(resolution,[status(thm)],[clause16,clause1]) ).
cnf(c45,plain,
( ~ ssRr(X116,X115)
| ~ ssPv3(X115)
| ~ ssPv2(X116)
| ~ ssPv4(X116)
| ssPv1(X115) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c47,plain,
( ~ ssPv3(skf1(X117))
| ~ ssPv2(X117)
| ~ ssPv4(X117)
| ssPv1(skf1(X117)) ),
inference(resolution,[status(thm)],[c45,clause1]) ).
cnf(c42,plain,
( ~ ssRr(X109,X110)
| ~ ssPv4(X110)
| ~ ssPv3(X109)
| ssPv2(X110)
| ssPv1(X109) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c44,plain,
( ~ ssPv4(skf1(X114))
| ~ ssPv3(X114)
| ssPv2(skf1(X114))
| ssPv1(X114) ),
inference(resolution,[status(thm)],[c42,clause1]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X99,X100)
| ~ ssPv4(X100)
| ~ ssRr(X99,X98)
| ~ ssPv3(X98)
| ssPv2(X99)
| ssPv3(X99) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c40,plain,
( ~ ssRr(X105,X104)
| ~ ssPv4(X104)
| ~ ssPv3(skf1(X105))
| ssPv2(X105)
| ssPv3(X105) ),
inference(resolution,[status(thm)],[clause15,clause1]) ).
cnf(c39,plain,
( ~ ssRr(X102,X101)
| ~ ssPv4(X101)
| ~ ssPv3(X101)
| ssPv2(X102)
| ssPv3(X102) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c41,plain,
( ~ ssPv4(skf1(X103))
| ~ ssPv3(skf1(X103))
| ssPv2(X103)
| ssPv3(X103) ),
inference(resolution,[status(thm)],[c39,clause1]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X88,X89)
| ~ ssPv4(X89)
| ~ ssRr(X88,X87)
| ~ ssPv1(X88)
| ssPv3(X87)
| ssPv2(X88) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(c36,plain,
( ~ ssRr(X95,X96)
| ~ ssPv4(X96)
| ~ ssPv1(X95)
| ssPv3(skf1(X95))
| ssPv2(X95) ),
inference(resolution,[status(thm)],[clause14,clause1]) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X78,X79)
| ~ ssPv4(X79)
| ~ ssRr(X78,X77)
| ~ ssPv2(X77)
| ssPv3(X78)
| ssPv4(X78) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(c32,plain,
( ~ ssRr(X93,X94)
| ~ ssPv4(X94)
| ~ ssPv2(skf1(X93))
| ssPv3(X93)
| ssPv4(X93) ),
inference(resolution,[status(thm)],[clause13,clause1]) ).
cnf(c35,plain,
( ~ ssRr(X90,X91)
| ~ ssPv4(X91)
| ~ ssPv1(X90)
| ssPv3(X91)
| ssPv2(X90) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c37,plain,
( ~ ssPv4(skf1(X92))
| ~ ssPv1(X92)
| ssPv3(skf1(X92))
| ssPv2(X92) ),
inference(resolution,[status(thm)],[c35,clause1]) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X67,X68)
| ~ ssPv2(X68)
| ~ ssRr(X67,X66)
| ~ ssPv1(X67)
| ssPv1(X66)
| ssPv3(X67) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(c27,plain,
( ~ ssRr(X85,X84)
| ~ ssPv2(X84)
| ~ ssPv1(X85)
| ssPv1(skf1(X85))
| ssPv3(X85) ),
inference(resolution,[status(thm)],[clause12,clause1]) ).
cnf(c31,plain,
( ~ ssRr(X81,X82)
| ~ ssPv4(X82)
| ~ ssPv2(X82)
| ssPv3(X81)
| ssPv4(X81) ),
inference(factor,[status(thm)],[clause13]) ).
cnf(c33,plain,
( ~ ssPv4(skf1(X83))
| ~ ssPv2(skf1(X83))
| ssPv3(X83)
| ssPv4(X83) ),
inference(resolution,[status(thm)],[c31,clause1]) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X64,X65)
| ~ ssPv4(X65)
| ~ ssRr(X64,X63)
| ~ ssPv1(X64)
| ssPv3(X63)
| ssPv3(X64) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(c25,plain,
( ~ ssRr(X75,X76)
| ~ ssPv4(X76)
| ~ ssPv1(X75)
| ssPv3(skf1(X75))
| ssPv3(X75) ),
inference(resolution,[status(thm)],[clause11,clause1]) ).
cnf(c26,plain,
( ~ ssRr(X72,X71)
| ~ ssPv2(X71)
| ~ ssPv1(X72)
| ssPv1(X71)
| ssPv3(X72) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(c29,plain,
( ~ ssPv2(skf1(X74))
| ~ ssPv1(X74)
| ssPv1(skf1(X74))
| ssPv3(X74) ),
inference(resolution,[status(thm)],[c26,clause1]) ).
cnf(c24,plain,
( ~ ssRr(X69,X70)
| ~ ssPv4(X70)
| ~ ssPv1(X69)
| ssPv3(X70)
| ssPv3(X69) ),
inference(factor,[status(thm)],[clause11]) ).
cnf(c28,plain,
( ~ ssPv4(skf1(X73))
| ~ ssPv1(X73)
| ssPv3(skf1(X73))
| ssPv3(X73) ),
inference(resolution,[status(thm)],[c24,clause1]) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X55,X56)
| ~ ssPv1(X56)
| ~ ssRr(X55,X54)
| ~ ssPv2(X55)
| ssPv1(X54)
| ssPv3(X55) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(c22,plain,
( ~ ssRr(X60,X61)
| ~ ssPv1(X61)
| ~ ssPv2(X60)
| ssPv1(skf1(X60))
| ssPv3(X60) ),
inference(resolution,[status(thm)],[clause10,clause1]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X44,X45)
| ~ ssPv1(X45)
| ~ ssRr(X44,X43)
| ~ ssPv1(X44)
| ssPv3(X43)
| ssPv4(X44) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(c17,plain,
( ~ ssRr(X53,X52)
| ~ ssPv1(X52)
| ~ ssPv1(X53)
| ssPv3(skf1(X53))
| ssPv4(X53) ),
inference(resolution,[status(thm)],[clause9,clause1]) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X39,X40)
| ~ ssPv1(X40)
| ~ ssRr(X39,X38)
| ~ ssPv3(X39)
| ssPv1(X38)
| ssPv4(X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(c15,plain,
( ~ ssRr(X49,X50)
| ~ ssPv1(X50)
| ~ ssPv3(X49)
| ssPv1(skf1(X49))
| ssPv4(X49) ),
inference(resolution,[status(thm)],[clause8,clause1]) ).
cnf(c16,plain,
( ~ ssRr(X46,X47)
| ~ ssPv1(X47)
| ~ ssPv1(X46)
| ssPv3(X47)
| ssPv4(X46) ),
inference(factor,[status(thm)],[clause9]) ).
cnf(c18,plain,
( ~ ssPv1(skf1(X48))
| ~ ssPv1(X48)
| ssPv3(skf1(X48))
| ssPv4(X48) ),
inference(resolution,[status(thm)],[c16,clause1]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X31,X32)
| ~ ssPv4(X32)
| ~ ssRr(X31,X30)
| ~ ssPv3(X31)
| ssPv4(X30)
| ssPv4(X31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(c12,plain,
( ~ ssRr(X35,X36)
| ~ ssPv4(X36)
| ~ ssPv3(X35)
| ssPv4(skf1(X35))
| ssPv4(X35) ),
inference(resolution,[status(thm)],[clause7,clause1]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X21,X22)
| ~ ssRr(X21,X20)
| ~ ssPv1(X21)
| ~ ssPv4(X21)
| ssPv3(X22)
| ssPv2(X20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(c8,plain,
( ~ ssRr(X28,X27)
| ~ ssPv1(X28)
| ~ ssPv4(X28)
| ssPv3(X27)
| ssPv2(skf1(X28)) ),
inference(resolution,[status(thm)],[clause6,clause1]) ).
cnf(c7,plain,
( ~ ssRr(X25,X24)
| ~ ssPv1(X25)
| ~ ssPv4(X25)
| ssPv3(X24)
| ssPv2(X24) ),
inference(factor,[status(thm)],[clause6]) ).
cnf(c9,plain,
( ~ ssPv1(X26)
| ~ ssPv4(X26)
| ssPv3(skf1(X26))
| ssPv2(skf1(X26)) ),
inference(resolution,[status(thm)],[c7,clause1]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X13,X14)
| ~ ssRr(X13,X12)
| ~ ssPv3(X13)
| ~ ssPv4(X13)
| ssPv4(X14)
| ssPv3(X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c4,plain,
( ~ ssRr(X18,X19)
| ~ ssPv3(X18)
| ~ ssPv4(X18)
| ssPv4(X19)
| ssPv3(skf1(X18)) ),
inference(resolution,[status(thm)],[clause5,clause1]) ).
cnf(c3,plain,
( ~ ssRr(X15,X16)
| ~ ssPv3(X15)
| ~ ssPv4(X15)
| ssPv4(X16)
| ssPv3(X16) ),
inference(factor,[status(thm)],[clause5]) ).
cnf(c5,plain,
( ~ ssPv3(X17)
| ~ ssPv4(X17)
| ssPv4(skf1(X17))
| ssPv3(skf1(X17)) ),
inference(resolution,[status(thm)],[c3,clause1]) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X9,X10)
| ~ ssPv1(X10)
| ~ ssPv1(X9)
| ~ ssPv2(X9)
| ~ ssPv3(X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(c2,plain,
( ~ ssPv1(skf1(X11))
| ~ ssPv1(X11)
| ~ ssPv2(X11)
| ~ ssPv3(X11) ),
inference(resolution,[status(thm)],[clause4,clause1]) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X6,X7)
| ~ ssPv1(X6)
| ~ ssPv3(X6)
| ssPv4(X7)
| ssPv2(X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(c1,plain,
( ~ ssPv1(X8)
| ~ ssPv3(X8)
| ssPv4(skf1(X8))
| ssPv2(X8) ),
inference(resolution,[status(thm)],[clause3,clause1]) ).
cnf(clause2,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssPv3(X3)
| ssPv3(X4)
| ssPv1(X3)
| ssPv2(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(c0,plain,
( ~ ssPv3(X5)
| ssPv3(skf1(X5))
| ssPv1(X5)
| ssPv2(X5) ),
inference(resolution,[status(thm)],[clause2,clause1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SYN740-1 : TPTP v8.1.2. Released v2.5.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n004.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 19:46:53 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.59/0.77 % Version: 1.5
% 0.59/0.77 % SZS status Satisfiable
% 0.59/0.77 % SZS output start Saturation
% See solution above
% 0.59/0.77
% 0.59/0.77 % Initial clauses : 31
% 0.59/0.77 % Processed clauses : 122
% 0.59/0.77 % Factors computed : 50
% 0.59/0.77 % Resolvents computed: 85
% 0.59/0.77 % Tautologies deleted: 25
% 0.59/0.77 % Forward subsumed : 19
% 0.59/0.77 % Backward subsumed : 0
% 0.59/0.77 % -------- CPU Time ---------
% 0.59/0.77 % User time : 0.386 s
% 0.59/0.77 % System time : 0.016 s
% 0.59/0.77 % Total time : 0.402 s
%------------------------------------------------------------------------------