%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN749-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:47 EDT 2024
% Result : Satisfiable 0.61s 0.80s
% Output : Saturation 0.61s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssRr(X2,skf1(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause41,negated_conjecture,
( ~ ssRr(X316,X318)
| ~ ssPv5(X318)
| ~ ssRr(X316,X317)
| ~ ssRr(X316,X315)
| ~ ssPv5(X316)
| ssPv4(X317)
| ssPv2(X315) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c141,plain,
( ~ ssRr(X428,X426)
| ~ ssPv5(X426)
| ~ ssRr(X428,X427)
| ~ ssPv5(X428)
| ssPv4(X427)
| ssPv2(X427) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c189,plain,
( ~ ssRr(X464,X465)
| ~ ssPv5(X465)
| ~ ssPv5(X464)
| ssPv4(skf1(X464))
| ssPv2(skf1(X464)) ),
inference(resolution,[status(thm)],[c141,clause1]) ).
cnf(clause40,negated_conjecture,
( ~ ssRr(X302,X304)
| ~ ssPv3(X304)
| ~ ssRr(X302,X303)
| ~ ssRr(X302,X301)
| ~ ssPv2(X302)
| ssPv3(X303)
| ssPv1(X301) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c133,plain,
( ~ ssRr(X407,X408)
| ~ ssPv3(X408)
| ~ ssRr(X407,X409)
| ~ ssPv2(X407)
| ssPv3(X409)
| ssPv1(X409) ),
inference(factor,[status(thm)],[clause40]) ).
cnf(c181,plain,
( ~ ssRr(X459,X460)
| ~ ssPv3(X460)
| ~ ssPv2(X459)
| ssPv3(skf1(X459))
| ssPv1(skf1(X459)) ),
inference(resolution,[status(thm)],[c133,clause1]) ).
cnf(clause39,negated_conjecture,
( ~ ssRr(X289,X291)
| ~ ssPv8(X291)
| ~ ssRr(X289,X290)
| ~ ssPv6(X290)
| ~ ssRr(X289,X288)
| ssPv3(X288)
| ssPv3(X289) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c127,plain,
( ~ ssRr(X374,X375)
| ~ ssPv8(X375)
| ~ ssRr(X374,X376)
| ~ ssPv6(X376)
| ssPv3(X376)
| ssPv3(X374) ),
inference(factor,[status(thm)],[clause39]) ).
cnf(c167,plain,
( ~ ssRr(X451,X452)
| ~ ssPv8(X452)
| ~ ssPv6(skf1(X451))
| ssPv3(skf1(X451))
| ssPv3(X451) ),
inference(resolution,[status(thm)],[c127,clause1]) ).
cnf(clause38,negated_conjecture,
( ~ ssRr(X275,X277)
| ~ ssPv6(X277)
| ~ ssRr(X275,X276)
| ~ ssRr(X275,X274)
| ssPv6(X276)
| ssPv2(X274)
| ssPv2(X275) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c120,plain,
( ~ ssRr(X349,X351)
| ~ ssPv6(X351)
| ~ ssRr(X349,X350)
| ssPv6(X350)
| ssPv2(X350)
| ssPv2(X349) ),
inference(factor,[status(thm)],[clause38]) ).
cnf(c156,plain,
( ~ ssRr(X444,X445)
| ~ ssPv6(X445)
| ssPv6(skf1(X444))
| ssPv2(skf1(X444))
| ssPv2(X444) ),
inference(resolution,[status(thm)],[c120,clause1]) ).
cnf(c142,plain,
( ~ ssRr(X438,X439)
| ~ ssPv5(X439)
| ~ ssRr(X438,X440)
| ~ ssPv5(X438)
| ssPv4(X440)
| ssPv2(skf1(X438)) ),
inference(resolution,[status(thm)],[clause41,clause1]) ).
cnf(c191,plain,
( ~ ssRr(X442,X441)
| ~ ssPv5(X441)
| ~ ssPv5(X442)
| ssPv4(X441)
| ssPv2(skf1(X442)) ),
inference(factor,[status(thm)],[c142]) ).
cnf(clause37,negated_conjecture,
( ~ ssRr(X262,X264)
| ~ ssPv7(X264)
| ~ ssRr(X262,X263)
| ~ ssRr(X262,X261)
| ssPv6(X263)
| ssPv3(X261)
| ssPv3(X262) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c113,plain,
( ~ ssRr(X322,X323)
| ~ ssPv7(X323)
| ~ ssRr(X322,X321)
| ssPv6(X321)
| ssPv3(X321)
| ssPv3(X322) ),
inference(factor,[status(thm)],[clause37]) ).
cnf(c144,plain,
( ~ ssRr(X431,X432)
| ~ ssPv7(X432)
| ssPv6(skf1(X431))
| ssPv3(skf1(X431))
| ssPv3(X431) ),
inference(resolution,[status(thm)],[c113,clause1]) ).
cnf(c140,plain,
( ~ ssRr(X414,X413)
| ~ ssPv5(X413)
| ~ ssRr(X414,X412)
| ~ ssPv5(X414)
| ssPv4(X412)
| ssPv2(X413) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c182,plain,
( ~ ssRr(X418,X419)
| ~ ssPv5(X419)
| ~ ssPv5(X418)
| ssPv4(X419)
| ssPv2(X419) ),
inference(factor,[status(thm)],[c140]) ).
cnf(c186,plain,
( ~ ssPv5(skf1(X424))
| ~ ssPv5(X424)
| ssPv4(skf1(X424))
| ssPv2(skf1(X424)) ),
inference(resolution,[status(thm)],[c182,clause1]) ).
cnf(c183,plain,
( ~ ssRr(X420,X421)
| ~ ssPv5(X421)
| ~ ssPv5(X420)
| ssPv4(skf1(X420))
| ssPv2(X421) ),
inference(resolution,[status(thm)],[c140,clause1]) ).
cnf(c134,plain,
( ~ ssRr(X415,X416)
| ~ ssPv3(X416)
| ~ ssRr(X415,X417)
| ~ ssPv2(X415)
| ssPv3(X417)
| ssPv1(skf1(X415)) ),
inference(resolution,[status(thm)],[clause40,clause1]) ).
cnf(c128,plain,
( ~ ssRr(X401,X402)
| ~ ssPv8(X402)
| ~ ssRr(X401,X403)
| ~ ssPv6(X403)
| ssPv3(skf1(X401))
| ssPv3(X401) ),
inference(resolution,[status(thm)],[clause39,clause1]) ).
cnf(c177,plain,
( ~ ssRr(X404,X405)
| ~ ssPv8(X405)
| ~ ssPv6(X405)
| ssPv3(skf1(X404))
| ssPv3(X404) ),
inference(factor,[status(thm)],[c128]) ).
cnf(c132,plain,
( ~ ssRr(X393,X394)
| ~ ssPv3(X394)
| ~ ssRr(X393,X395)
| ~ ssPv2(X393)
| ssPv3(X395)
| ssPv1(X394) ),
inference(factor,[status(thm)],[clause40]) ).
cnf(c175,plain,
( ~ ssRr(X398,X399)
| ~ ssPv3(X399)
| ~ ssPv2(X398)
| ssPv3(skf1(X398))
| ssPv1(X399) ),
inference(resolution,[status(thm)],[c132,clause1]) ).
cnf(c121,plain,
( ~ ssRr(X389,X390)
| ~ ssPv6(X390)
| ~ ssRr(X389,X388)
| ssPv6(X388)
| ssPv2(skf1(X389))
| ssPv2(X389) ),
inference(resolution,[status(thm)],[clause38,clause1]) ).
cnf(clause36,negated_conjecture,
( ~ ssRr(X248,X250)
| ~ ssPv6(X250)
| ~ ssRr(X248,X249)
| ~ ssRr(X248,X247)
| ssPv4(X249)
| ssPv1(X247)
| ssPv7(X248) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c106,plain,
( ~ ssRr(X298,X296)
| ~ ssPv6(X296)
| ~ ssRr(X298,X297)
| ssPv4(X297)
| ssPv1(X297)
| ssPv7(X298) ),
inference(factor,[status(thm)],[clause36]) ).
cnf(c131,plain,
( ~ ssRr(X385,X386)
| ~ ssPv6(X386)
| ssPv4(skf1(X385))
| ssPv1(skf1(X385))
| ssPv7(X385) ),
inference(resolution,[status(thm)],[c106,clause1]) ).
cnf(c114,plain,
( ~ ssRr(X378,X379)
| ~ ssPv7(X379)
| ~ ssRr(X378,X377)
| ssPv6(X377)
| ssPv3(skf1(X378))
| ssPv3(X378) ),
inference(resolution,[status(thm)],[clause37,clause1]) ).
cnf(c168,plain,
( ~ ssRr(X382,X383)
| ~ ssPv7(X383)
| ssPv6(X383)
| ssPv3(skf1(X382))
| ssPv3(X382) ),
inference(factor,[status(thm)],[c114]) ).
cnf(c107,plain,
( ~ ssRr(X365,X367)
| ~ ssPv6(X367)
| ~ ssRr(X365,X366)
| ssPv4(X366)
| ssPv1(skf1(X365))
| ssPv7(X365) ),
inference(resolution,[status(thm)],[clause36,clause1]) ).
cnf(c163,plain,
( ~ ssRr(X371,X372)
| ~ ssPv6(X372)
| ssPv4(X372)
| ssPv1(skf1(X371))
| ssPv7(X371) ),
inference(factor,[status(thm)],[c107]) ).
cnf(c126,plain,
( ~ ssRr(X360,X362)
| ~ ssPv8(X362)
| ~ ssRr(X360,X361)
| ~ ssPv6(X361)
| ssPv3(X362)
| ssPv3(X360) ),
inference(factor,[status(thm)],[clause39]) ).
cnf(c160,plain,
( ~ ssRr(X364,X363)
| ~ ssPv8(X363)
| ~ ssPv6(X363)
| ssPv3(X363)
| ssPv3(X364) ),
inference(factor,[status(thm)],[c126]) ).
cnf(c162,plain,
( ~ ssPv8(skf1(X370))
| ~ ssPv6(skf1(X370))
| ssPv3(skf1(X370))
| ssPv3(X370) ),
inference(resolution,[status(thm)],[c160,clause1]) ).
cnf(c161,plain,
( ~ ssRr(X368,X369)
| ~ ssPv8(X369)
| ~ ssPv6(skf1(X368))
| ssPv3(X369)
| ssPv3(X368) ),
inference(resolution,[status(thm)],[c126,clause1]) ).
cnf(clause35,negated_conjecture,
( ~ ssRr(X232,X234)
| ~ ssRr(X232,X233)
| ~ ssRr(X232,X231)
| ~ ssPv2(X232)
| ssPv7(X234)
| ssPv4(X233)
| ssPv3(X231) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c98,plain,
( ~ ssRr(X353,X352)
| ~ ssRr(X353,X354)
| ~ ssPv2(X353)
| ssPv7(X352)
| ssPv4(X354)
| ssPv3(skf1(X353)) ),
inference(resolution,[status(thm)],[clause35,clause1]) ).
cnf(c157,plain,
( ~ ssRr(X357,X358)
| ~ ssPv2(X357)
| ssPv7(X358)
| ssPv4(X358)
| ssPv3(skf1(X357)) ),
inference(factor,[status(thm)],[c98]) ).
cnf(clause34,negated_conjecture,
( ~ ssRr(X219,X221)
| ~ ssRr(X219,X220)
| ~ ssRr(X219,X218)
| ~ ssPv3(X219)
| ssPv6(X221)
| ssPv4(X220)
| ssPv2(X218) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c91,plain,
( ~ ssRr(X340,X342)
| ~ ssRr(X340,X341)
| ~ ssPv3(X340)
| ssPv6(X342)
| ssPv4(X341)
| ssPv2(skf1(X340)) ),
inference(resolution,[status(thm)],[clause34,clause1]) ).
cnf(c151,plain,
( ~ ssRr(X346,X345)
| ~ ssPv3(X346)
| ssPv6(X345)
| ssPv4(X345)
| ssPv2(skf1(X346)) ),
inference(factor,[status(thm)],[c91]) ).
cnf(c119,plain,
( ~ ssRr(X336,X337)
| ~ ssPv6(X337)
| ~ ssRr(X336,X335)
| ssPv6(X335)
| ssPv2(X337)
| ssPv2(X336) ),
inference(factor,[status(thm)],[clause38]) ).
cnf(c150,plain,
( ~ ssRr(X343,X344)
| ~ ssPv6(X344)
| ssPv6(skf1(X343))
| ssPv2(X344)
| ssPv2(X343) ),
inference(resolution,[status(thm)],[c119,clause1]) ).
cnf(clause33,negated_conjecture,
( ~ ssRr(X215,X217)
| ~ ssRr(X215,X216)
| ~ ssRr(X215,X214)
| ~ ssPv3(X215)
| ssPv8(X217)
| ssPv7(X216)
| ssPv6(X214) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c88,plain,
( ~ ssRr(X328,X329)
| ~ ssRr(X328,X330)
| ~ ssPv3(X328)
| ssPv8(X329)
| ssPv7(X330)
| ssPv6(skf1(X328)) ),
inference(resolution,[status(thm)],[clause33,clause1]) ).
cnf(c146,plain,
( ~ ssRr(X333,X332)
| ~ ssPv3(X333)
| ssPv8(X332)
| ssPv7(X332)
| ssPv6(skf1(X333)) ),
inference(factor,[status(thm)],[c88]) ).
cnf(c97,plain,
( ~ ssRr(X271,X272)
| ~ ssRr(X271,X273)
| ~ ssPv2(X271)
| ssPv7(X272)
| ssPv4(X273)
| ssPv3(X273) ),
inference(factor,[status(thm)],[clause35]) ).
cnf(c118,plain,
( ~ ssRr(X326,X327)
| ~ ssPv2(X326)
| ssPv7(X327)
| ssPv4(skf1(X326))
| ssPv3(skf1(X326)) ),
inference(resolution,[status(thm)],[c97,clause1]) ).
cnf(c112,plain,
( ~ ssRr(X309,X308)
| ~ ssPv7(X308)
| ~ ssRr(X309,X310)
| ssPv6(X310)
| ssPv3(X308)
| ssPv3(X309) ),
inference(factor,[status(thm)],[clause37]) ).
cnf(c136,plain,
( ~ ssRr(X312,X311)
| ~ ssPv7(X311)
| ssPv6(X311)
| ssPv3(X311)
| ssPv3(X312) ),
inference(factor,[status(thm)],[c112]) ).
cnf(c138,plain,
( ~ ssPv7(skf1(X319))
| ssPv6(skf1(X319))
| ssPv3(skf1(X319))
| ssPv3(X319) ),
inference(resolution,[status(thm)],[c136,clause1]) ).
cnf(c137,plain,
( ~ ssRr(X313,X314)
| ~ ssPv7(X314)
| ssPv6(skf1(X313))
| ssPv3(X314)
| ssPv3(X313) ),
inference(resolution,[status(thm)],[c112,clause1]) ).
cnf(c90,plain,
( ~ ssRr(X254,X255)
| ~ ssRr(X254,X253)
| ~ ssPv3(X254)
| ssPv6(X255)
| ssPv4(X253)
| ssPv2(X253) ),
inference(factor,[status(thm)],[clause34]) ).
cnf(c109,plain,
( ~ ssRr(X305,X306)
| ~ ssPv3(X305)
| ssPv6(X306)
| ssPv4(skf1(X305))
| ssPv2(skf1(X305)) ),
inference(resolution,[status(thm)],[c90,clause1]) ).
cnf(c105,plain,
( ~ ssRr(X285,X283)
| ~ ssPv6(X283)
| ~ ssRr(X285,X284)
| ssPv4(X284)
| ssPv1(X283)
| ssPv7(X285) ),
inference(factor,[status(thm)],[clause36]) ).
cnf(c123,plain,
( ~ ssRr(X286,X287)
| ~ ssPv6(X287)
| ssPv4(X287)
| ssPv1(X287)
| ssPv7(X286) ),
inference(factor,[status(thm)],[c105]) ).
cnf(c125,plain,
( ~ ssPv6(skf1(X294))
| ssPv4(skf1(X294))
| ssPv1(skf1(X294))
| ssPv7(X294) ),
inference(resolution,[status(thm)],[c123,clause1]) ).
cnf(c124,plain,
( ~ ssRr(X292,X293)
| ~ ssPv6(X293)
| ssPv4(skf1(X292))
| ssPv1(X293)
| ssPv7(X292) ),
inference(resolution,[status(thm)],[c105,clause1]) ).
cnf(c87,plain,
( ~ ssRr(X237,X236)
| ~ ssRr(X237,X235)
| ~ ssPv3(X237)
| ssPv8(X236)
| ssPv7(X235)
| ssPv6(X235) ),
inference(factor,[status(thm)],[clause33]) ).
cnf(c100,plain,
( ~ ssRr(X280,X281)
| ~ ssPv3(X280)
| ssPv8(X281)
| ssPv7(skf1(X280))
| ssPv6(skf1(X280)) ),
inference(resolution,[status(thm)],[c87,clause1]) ).
cnf(c96,plain,
( ~ ssRr(X258,X259)
| ~ ssRr(X258,X260)
| ~ ssPv2(X258)
| ssPv7(X259)
| ssPv4(X260)
| ssPv3(X259) ),
inference(factor,[status(thm)],[clause35]) ).
cnf(c110,plain,
( ~ ssRr(X265,X266)
| ~ ssPv2(X265)
| ssPv7(X266)
| ssPv4(X266)
| ssPv3(X266) ),
inference(factor,[status(thm)],[c96]) ).
cnf(c115,plain,
( ~ ssPv2(X269)
| ssPv7(skf1(X269))
| ssPv4(skf1(X269))
| ssPv3(skf1(X269)) ),
inference(resolution,[status(thm)],[c110,clause1]) ).
cnf(c111,plain,
( ~ ssRr(X267,X268)
| ~ ssPv2(X267)
| ssPv7(X268)
| ssPv4(skf1(X267))
| ssPv3(X268) ),
inference(resolution,[status(thm)],[c96,clause1]) ).
cnf(c89,plain,
( ~ ssRr(X241,X240)
| ~ ssRr(X241,X242)
| ~ ssPv3(X241)
| ssPv6(X240)
| ssPv4(X242)
| ssPv2(X240) ),
inference(factor,[status(thm)],[clause34]) ).
cnf(c101,plain,
( ~ ssRr(X243,X244)
| ~ ssPv3(X243)
| ssPv6(X244)
| ssPv4(X244)
| ssPv2(X244) ),
inference(factor,[status(thm)],[c89]) ).
cnf(c103,plain,
( ~ ssPv3(X251)
| ssPv6(skf1(X251))
| ssPv4(skf1(X251))
| ssPv2(skf1(X251)) ),
inference(resolution,[status(thm)],[c101,clause1]) ).
cnf(c102,plain,
( ~ ssRr(X245,X246)
| ~ ssPv3(X245)
| ssPv6(X246)
| ssPv4(skf1(X245))
| ssPv2(X246) ),
inference(resolution,[status(thm)],[c89,clause1]) ).
cnf(c86,plain,
( ~ ssRr(X223,X222)
| ~ ssRr(X223,X224)
| ~ ssPv3(X223)
| ssPv8(X222)
| ssPv7(X224)
| ssPv6(X222) ),
inference(factor,[status(thm)],[clause33]) ).
cnf(c92,plain,
( ~ ssRr(X225,X226)
| ~ ssPv3(X225)
| ssPv8(X226)
| ssPv7(X226)
| ssPv6(X226) ),
inference(factor,[status(thm)],[c86]) ).
cnf(c94,plain,
( ~ ssPv3(X229)
| ssPv8(skf1(X229))
| ssPv7(skf1(X229))
| ssPv6(skf1(X229)) ),
inference(resolution,[status(thm)],[c92,clause1]) ).
cnf(c93,plain,
( ~ ssRr(X227,X228)
| ~ ssPv3(X227)
| ssPv8(X228)
| ssPv7(skf1(X227))
| ssPv6(X228) ),
inference(resolution,[status(thm)],[c86,clause1]) ).
cnf(clause32,negated_conjecture,
( ~ ssRr(X204,X206)
| ~ ssPv7(X206)
| ~ ssRr(X204,X205)
| ~ ssPv3(X205)
| ~ ssPv4(X204)
| ~ ssPv6(X204) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c84,plain,
( ~ ssRr(X213,X212)
| ~ ssPv7(X212)
| ~ ssPv3(skf1(X213))
| ~ ssPv4(X213)
| ~ ssPv6(X213) ),
inference(resolution,[status(thm)],[clause32,clause1]) ).
cnf(clause31,negated_conjecture,
( ~ ssRr(X193,X195)
| ~ ssPv6(X195)
| ~ ssRr(X193,X194)
| ~ ssPv3(X194)
| ~ ssPv3(X193)
| ssPv2(X193) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c80,plain,
( ~ ssRr(X210,X211)
| ~ ssPv6(X211)
| ~ ssPv3(skf1(X210))
| ~ ssPv3(X210)
| ssPv2(X210) ),
inference(resolution,[status(thm)],[clause31,clause1]) ).
cnf(c83,plain,
( ~ ssRr(X207,X208)
| ~ ssPv7(X208)
| ~ ssPv3(X208)
| ~ ssPv4(X207)
| ~ ssPv6(X207) ),
inference(factor,[status(thm)],[clause32]) ).
cnf(c85,plain,
( ~ ssPv7(skf1(X209))
| ~ ssPv3(skf1(X209))
| ~ ssPv4(X209)
| ~ ssPv6(X209) ),
inference(resolution,[status(thm)],[c83,clause1]) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X190,X192)
| ~ ssPv7(X192)
| ~ ssRr(X190,X191)
| ~ ssPv1(X191)
| ~ ssPv6(X190)
| ssPv3(X190) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c78,plain,
( ~ ssRr(X202,X203)
| ~ ssPv7(X203)
| ~ ssPv1(skf1(X202))
| ~ ssPv6(X202)
| ssPv3(X202) ),
inference(resolution,[status(thm)],[clause30,clause1]) ).
cnf(c79,plain,
( ~ ssRr(X198,X199)
| ~ ssPv6(X199)
| ~ ssPv3(X199)
| ~ ssPv3(X198)
| ssPv2(X198) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c82,plain,
( ~ ssPv6(skf1(X201))
| ~ ssPv3(skf1(X201))
| ~ ssPv3(X201)
| ssPv2(X201) ),
inference(resolution,[status(thm)],[c79,clause1]) ).
cnf(c77,plain,
( ~ ssRr(X197,X196)
| ~ ssPv7(X196)
| ~ ssPv1(X196)
| ~ ssPv6(X197)
| ssPv3(X197) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c81,plain,
( ~ ssPv7(skf1(X200))
| ~ ssPv1(skf1(X200))
| ~ ssPv6(X200)
| ssPv3(X200) ),
inference(resolution,[status(thm)],[c77,clause1]) ).
cnf(clause29,negated_conjecture,
( ~ ssRr(X180,X182)
| ~ ssPv8(X182)
| ~ ssRr(X180,X181)
| ~ ssPv4(X181)
| ~ ssPv5(X180)
| ssPv4(X180) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c75,plain,
( ~ ssRr(X188,X189)
| ~ ssPv8(X189)
| ~ ssPv4(skf1(X188))
| ~ ssPv5(X188)
| ssPv4(X188) ),
inference(resolution,[status(thm)],[clause29,clause1]) ).
cnf(clause28,negated_conjecture,
( ~ ssRr(X169,X171)
| ~ ssPv7(X171)
| ~ ssRr(X169,X170)
| ~ ssPv5(X170)
| ~ ssPv2(X169)
| ssPv6(X169) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c71,plain,
( ~ ssRr(X186,X187)
| ~ ssPv7(X187)
| ~ ssPv5(skf1(X186))
| ~ ssPv2(X186)
| ssPv6(X186) ),
inference(resolution,[status(thm)],[clause28,clause1]) ).
cnf(c74,plain,
( ~ ssRr(X184,X183)
| ~ ssPv8(X183)
| ~ ssPv4(X183)
| ~ ssPv5(X184)
| ssPv4(X184) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c76,plain,
( ~ ssPv8(skf1(X185))
| ~ ssPv4(skf1(X185))
| ~ ssPv5(X185)
| ssPv4(X185) ),
inference(resolution,[status(thm)],[c74,clause1]) ).
cnf(clause27,negated_conjecture,
( ~ ssRr(X166,X168)
| ~ ssPv6(X168)
| ~ ssRr(X166,X167)
| ~ ssPv1(X167)
| ~ ssPv5(X166)
| ssPv7(X166) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c69,plain,
( ~ ssRr(X178,X179)
| ~ ssPv6(X179)
| ~ ssPv1(skf1(X178))
| ~ ssPv5(X178)
| ssPv7(X178) ),
inference(resolution,[status(thm)],[clause27,clause1]) ).
cnf(c70,plain,
( ~ ssRr(X174,X175)
| ~ ssPv7(X175)
| ~ ssPv5(X175)
| ~ ssPv2(X174)
| ssPv6(X174) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c73,plain,
( ~ ssPv7(skf1(X177))
| ~ ssPv5(skf1(X177))
| ~ ssPv2(X177)
| ssPv6(X177) ),
inference(resolution,[status(thm)],[c70,clause1]) ).
cnf(c68,plain,
( ~ ssRr(X173,X172)
| ~ ssPv6(X172)
| ~ ssPv1(X172)
| ~ ssPv5(X173)
| ssPv7(X173) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c72,plain,
( ~ ssPv6(skf1(X176))
| ~ ssPv1(skf1(X176))
| ~ ssPv5(X176)
| ssPv7(X176) ),
inference(resolution,[status(thm)],[c68,clause1]) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X156,X158)
| ~ ssPv8(X158)
| ~ ssRr(X156,X157)
| ~ ssPv7(X157)
| ~ ssPv5(X156)
| ssPv7(X156) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c66,plain,
( ~ ssRr(X164,X165)
| ~ ssPv8(X165)
| ~ ssPv7(skf1(X164))
| ~ ssPv5(X164)
| ssPv7(X164) ),
inference(resolution,[status(thm)],[clause26,clause1]) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X146,X148)
| ~ ssPv8(X148)
| ~ ssRr(X146,X147)
| ~ ssPv2(X147)
| ~ ssPv3(X146)
| ssPv8(X146) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c62,plain,
( ~ ssRr(X162,X163)
| ~ ssPv8(X163)
| ~ ssPv2(skf1(X162))
| ~ ssPv3(X162)
| ssPv8(X162) ),
inference(resolution,[status(thm)],[clause25,clause1]) ).
cnf(c65,plain,
( ~ ssRr(X159,X160)
| ~ ssPv8(X160)
| ~ ssPv7(X160)
| ~ ssPv5(X159)
| ssPv7(X159) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c67,plain,
( ~ ssPv8(skf1(X161))
| ~ ssPv7(skf1(X161))
| ~ ssPv5(X161)
| ssPv7(X161) ),
inference(resolution,[status(thm)],[c65,clause1]) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X135,X137)
| ~ ssPv3(X137)
| ~ ssRr(X135,X136)
| ~ ssPv6(X135)
| ~ ssPv8(X135)
| ssPv7(X136) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c57,plain,
( ~ ssRr(X153,X154)
| ~ ssPv3(X154)
| ~ ssPv6(X153)
| ~ ssPv8(X153)
| ssPv7(skf1(X153)) ),
inference(resolution,[status(thm)],[clause24,clause1]) ).
cnf(c61,plain,
( ~ ssRr(X151,X150)
| ~ ssPv8(X150)
| ~ ssPv2(X150)
| ~ ssPv3(X151)
| ssPv8(X151) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c63,plain,
( ~ ssPv8(skf1(X152))
| ~ ssPv2(skf1(X152))
| ~ ssPv3(X152)
| ssPv8(X152) ),
inference(resolution,[status(thm)],[c61,clause1]) ).
cnf(clause23,negated_conjecture,
( ~ ssRr(X132,X134)
| ~ ssPv1(X134)
| ~ ssRr(X132,X133)
| ~ ssPv2(X132)
| ssPv4(X133)
| ssPv1(X132) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c55,plain,
( ~ ssRr(X144,X145)
| ~ ssPv1(X145)
| ~ ssPv2(X144)
| ssPv4(skf1(X144))
| ssPv1(X144) ),
inference(resolution,[status(thm)],[clause23,clause1]) ).
cnf(c56,plain,
( ~ ssRr(X140,X141)
| ~ ssPv3(X141)
| ~ ssPv6(X140)
| ~ ssPv8(X140)
| ssPv7(X141) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c59,plain,
( ~ ssPv3(skf1(X143))
| ~ ssPv6(X143)
| ~ ssPv8(X143)
| ssPv7(skf1(X143)) ),
inference(resolution,[status(thm)],[c56,clause1]) ).
cnf(c54,plain,
( ~ ssRr(X139,X138)
| ~ ssPv1(X138)
| ~ ssPv2(X139)
| ssPv4(X138)
| ssPv1(X139) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c58,plain,
( ~ ssPv1(skf1(X142))
| ~ ssPv2(X142)
| ssPv4(skf1(X142))
| ssPv1(X142) ),
inference(resolution,[status(thm)],[c54,clause1]) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X123,X125)
| ~ ssPv1(X125)
| ~ ssRr(X123,X124)
| ~ ssPv8(X123)
| ssPv7(X124)
| ssPv5(X123) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c51,plain,
( ~ ssRr(X129,X130)
| ~ ssPv1(X130)
| ~ ssPv8(X129)
| ssPv7(skf1(X129))
| ssPv5(X129) ),
inference(resolution,[status(thm)],[clause22,clause1]) ).
cnf(c50,plain,
( ~ ssRr(X127,X126)
| ~ ssPv1(X126)
| ~ ssPv8(X127)
| ssPv7(X126)
| ssPv5(X127) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c52,plain,
( ~ ssPv1(skf1(X128))
| ~ ssPv8(X128)
| ssPv7(skf1(X128))
| ssPv5(X128) ),
inference(resolution,[status(thm)],[c50,clause1]) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X113,X115)
| ~ ssPv6(X115)
| ~ ssRr(X113,X114)
| ~ ssPv1(X113)
| ssPv2(X114)
| ssPv7(X113) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c47,plain,
( ~ ssRr(X120,X121)
| ~ ssPv6(X121)
| ~ ssPv1(X120)
| ssPv2(skf1(X120))
| ssPv7(X120) ),
inference(resolution,[status(thm)],[clause21,clause1]) ).
cnf(c46,plain,
( ~ ssRr(X118,X117)
| ~ ssPv6(X117)
| ~ ssPv1(X118)
| ssPv2(X117)
| ssPv7(X118) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c48,plain,
( ~ ssPv6(skf1(X119))
| ~ ssPv1(X119)
| ssPv2(skf1(X119))
| ssPv7(X119) ),
inference(resolution,[status(thm)],[c46,clause1]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X102,X104)
| ~ ssRr(X102,X103)
| ~ ssPv3(X102)
| ~ ssPv5(X102)
| ssPv8(X104)
| ssPv7(X103) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c42,plain,
( ~ ssRr(X111,X112)
| ~ ssPv3(X111)
| ~ ssPv5(X111)
| ssPv8(X112)
| ssPv7(skf1(X111)) ),
inference(resolution,[status(thm)],[clause20,clause1]) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X92,X94)
| ~ ssRr(X92,X93)
| ~ ssPv3(X92)
| ~ ssPv7(X92)
| ssPv8(X94)
| ssPv6(X93) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c38,plain,
( ~ ssRr(X108,X109)
| ~ ssPv3(X108)
| ~ ssPv7(X108)
| ssPv8(X109)
| ssPv6(skf1(X108)) ),
inference(resolution,[status(thm)],[clause19,clause1]) ).
cnf(c41,plain,
( ~ ssRr(X106,X105)
| ~ ssPv3(X106)
| ~ ssPv5(X106)
| ssPv8(X105)
| ssPv7(X105) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c43,plain,
( ~ ssPv3(X107)
| ~ ssPv5(X107)
| ssPv8(skf1(X107))
| ssPv7(skf1(X107)) ),
inference(resolution,[status(thm)],[c41,clause1]) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X81,X83)
| ~ ssRr(X81,X82)
| ~ ssPv6(X81)
| ~ ssPv7(X81)
| ssPv5(X83)
| ssPv4(X82) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c33,plain,
( ~ ssRr(X99,X100)
| ~ ssPv6(X99)
| ~ ssPv7(X99)
| ssPv5(X100)
| ssPv4(skf1(X99)) ),
inference(resolution,[status(thm)],[clause18,clause1]) ).
cnf(c37,plain,
( ~ ssRr(X96,X97)
| ~ ssPv3(X96)
| ~ ssPv7(X96)
| ssPv8(X97)
| ssPv6(X97) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c39,plain,
( ~ ssPv3(X98)
| ~ ssPv7(X98)
| ssPv8(skf1(X98))
| ssPv6(skf1(X98)) ),
inference(resolution,[status(thm)],[c37,clause1]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X78,X80)
| ~ ssRr(X78,X79)
| ~ ssPv3(X78)
| ssPv8(X80)
| ssPv5(X79)
| ssPv1(X78) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c31,plain,
( ~ ssRr(X90,X91)
| ~ ssPv3(X90)
| ssPv8(X91)
| ssPv5(skf1(X90))
| ssPv1(X90) ),
inference(resolution,[status(thm)],[clause17,clause1]) ).
cnf(c32,plain,
( ~ ssRr(X87,X86)
| ~ ssPv6(X87)
| ~ ssPv7(X87)
| ssPv5(X86)
| ssPv4(X86) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c35,plain,
( ~ ssPv6(X89)
| ~ ssPv7(X89)
| ssPv5(skf1(X89))
| ssPv4(skf1(X89)) ),
inference(resolution,[status(thm)],[c32,clause1]) ).
cnf(c30,plain,
( ~ ssRr(X84,X85)
| ~ ssPv3(X84)
| ssPv8(X85)
| ssPv5(X85)
| ssPv1(X84) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c34,plain,
( ~ ssPv3(X88)
| ssPv8(skf1(X88))
| ssPv5(skf1(X88))
| ssPv1(X88) ),
inference(resolution,[status(thm)],[c30,clause1]) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X69,X71)
| ~ ssPv4(X71)
| ~ ssRr(X69,X70)
| ssPv3(X70)
| ssPv2(X69)
| ssPv5(X69) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c27,plain,
( ~ ssRr(X75,X76)
| ~ ssPv4(X76)
| ssPv3(skf1(X75))
| ssPv2(X75)
| ssPv5(X75) ),
inference(resolution,[status(thm)],[clause16,clause1]) ).
cnf(c26,plain,
( ~ ssRr(X72,X73)
| ~ ssPv4(X73)
| ssPv3(X73)
| ssPv2(X72)
| ssPv5(X72) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c28,plain,
( ~ ssPv4(skf1(X74))
| ssPv3(skf1(X74))
| ssPv2(X74)
| ssPv5(X74) ),
inference(resolution,[status(thm)],[c26,clause1]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X59,X61)
| ~ ssRr(X59,X60)
| ~ ssPv5(X59)
| ssPv8(X61)
| ssPv5(X60)
| ssPv4(X59) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c23,plain,
( ~ ssRr(X67,X66)
| ~ ssPv5(X67)
| ssPv8(X66)
| ssPv5(skf1(X67))
| ssPv4(X67) ),
inference(resolution,[status(thm)],[clause15,clause1]) ).
cnf(c22,plain,
( ~ ssRr(X63,X64)
| ~ ssPv5(X63)
| ssPv8(X64)
| ssPv5(X64)
| ssPv4(X63) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c24,plain,
( ~ ssPv5(X65)
| ssPv8(skf1(X65))
| ssPv5(skf1(X65))
| ssPv4(X65) ),
inference(resolution,[status(thm)],[c22,clause1]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X48,X50)
| ~ ssPv1(X50)
| ~ ssRr(X48,X49)
| ssPv7(X49)
| ssPv6(X48)
| ssPv7(X48) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c18,plain,
( ~ ssRr(X58,X57)
| ~ ssPv1(X57)
| ssPv7(skf1(X58))
| ssPv6(X58)
| ssPv7(X58) ),
inference(resolution,[status(thm)],[clause14,clause1]) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X38,X40)
| ~ ssRr(X38,X39)
| ~ ssPv7(X38)
| ssPv6(X40)
| ssPv3(X39)
| ssPv6(X38) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c14,plain,
( ~ ssRr(X54,X55)
| ~ ssPv7(X54)
| ssPv6(X55)
| ssPv3(skf1(X54))
| ssPv6(X54) ),
inference(resolution,[status(thm)],[clause13,clause1]) ).
cnf(c17,plain,
( ~ ssRr(X52,X51)
| ~ ssPv1(X51)
| ssPv7(X51)
| ssPv6(X52)
| ssPv7(X52) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c19,plain,
( ~ ssPv1(skf1(X53))
| ssPv7(skf1(X53))
| ssPv6(X53)
| ssPv7(X53) ),
inference(resolution,[status(thm)],[c17,clause1]) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X33,X35)
| ~ ssRr(X33,X34)
| ~ ssPv5(X33)
| ssPv7(X35)
| ssPv5(X34)
| ssPv8(X33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c11,plain,
( ~ ssRr(X45,X46)
| ~ ssPv5(X45)
| ssPv7(X46)
| ssPv5(skf1(X45))
| ssPv8(X45) ),
inference(resolution,[status(thm)],[clause12,clause1]) ).
cnf(c13,plain,
( ~ ssRr(X42,X43)
| ~ ssPv7(X42)
| ssPv6(X43)
| ssPv3(X43)
| ssPv6(X42) ),
inference(factor,[status(thm)],[clause13]) ).
cnf(c15,plain,
( ~ ssPv7(X44)
| ssPv6(skf1(X44))
| ssPv3(skf1(X44))
| ssPv6(X44) ),
inference(resolution,[status(thm)],[c13,clause1]) ).
cnf(c10,plain,
( ~ ssRr(X36,X37)
| ~ ssPv5(X36)
| ssPv7(X37)
| ssPv5(X37)
| ssPv8(X36) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(c12,plain,
( ~ ssPv5(X41)
| ssPv7(skf1(X41))
| ssPv5(skf1(X41))
| ssPv8(X41) ),
inference(resolution,[status(thm)],[c10,clause1]) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X30,X31)
| ~ ssPv5(X31)
| ~ ssPv2(X30)
| ~ ssPv3(X30)
| ssPv1(X30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c9,plain,
( ~ ssPv5(skf1(X32))
| ~ ssPv2(X32)
| ~ ssPv3(X32)
| ssPv1(X32) ),
inference(resolution,[status(thm)],[clause11,clause1]) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X27,X28)
| ~ ssPv6(X28)
| ~ ssPv1(X27)
| ~ ssPv4(X27)
| ssPv2(X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c8,plain,
( ~ ssPv6(skf1(X29))
| ~ ssPv1(X29)
| ~ ssPv4(X29)
| ssPv2(X29) ),
inference(resolution,[status(thm)],[clause10,clause1]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X24,X25)
| ~ ssPv6(X25)
| ~ ssPv4(X24)
| ~ ssPv6(X24)
| ssPv2(X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c7,plain,
( ~ ssPv6(skf1(X26))
| ~ ssPv4(X26)
| ~ ssPv6(X26)
| ssPv2(X26) ),
inference(resolution,[status(thm)],[clause9,clause1]) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X21,X22)
| ~ ssPv2(X21)
| ~ ssPv4(X21)
| ~ ssPv5(X21)
| ssPv3(X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c6,plain,
( ~ ssPv2(X23)
| ~ ssPv4(X23)
| ~ ssPv5(X23)
| ssPv3(skf1(X23)) ),
inference(resolution,[status(thm)],[clause8,clause1]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X18,X19)
| ~ ssPv4(X18)
| ~ ssPv7(X18)
| ~ ssPv8(X18)
| ssPv2(X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c5,plain,
( ~ ssPv4(X20)
| ~ ssPv7(X20)
| ~ ssPv8(X20)
| ssPv2(skf1(X20)) ),
inference(resolution,[status(thm)],[clause7,clause1]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X15,X16)
| ~ ssPv6(X15)
| ~ ssPv7(X15)
| ~ ssPv8(X15)
| ssPv2(X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c4,plain,
( ~ ssPv6(X17)
| ~ ssPv7(X17)
| ~ ssPv8(X17)
| ssPv2(skf1(X17)) ),
inference(resolution,[status(thm)],[clause6,clause1]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X12,X13)
| ~ ssPv8(X13)
| ~ ssPv8(X12)
| ssPv6(X12)
| ssPv7(X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c3,plain,
( ~ ssPv8(skf1(X14))
| ~ ssPv8(X14)
| ssPv6(X14)
| ssPv7(X14) ),
inference(resolution,[status(thm)],[clause5,clause1]) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X9,X10)
| ~ ssPv8(X10)
| ssPv2(X9)
| ssPv4(X9)
| ssPv7(X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c2,plain,
( ~ ssPv8(skf1(X11))
| ssPv2(X11)
| ssPv4(X11)
| ssPv7(X11) ),
inference(resolution,[status(thm)],[clause4,clause1]) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X6,X7)
| ~ ssPv4(X6)
| ssPv3(X7)
| ssPv3(X6)
| ssPv8(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c1,plain,
( ~ ssPv4(X8)
| ssPv3(skf1(X8))
| ssPv3(X8)
| ssPv8(X8) ),
inference(resolution,[status(thm)],[clause3,clause1]) ).
cnf(clause2,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssPv7(X3)
| ssPv8(X4)
| ssPv6(X3)
| ssPv8(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(c0,plain,
( ~ ssPv7(X5)
| ssPv8(skf1(X5))
| ssPv6(X5)
| ssPv8(X5) ),
inference(resolution,[status(thm)],[clause2,clause1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYN749-1 : TPTP v8.1.2. Released v2.5.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.32 % Computer : n027.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Wed May 8 20:08:22 EDT 2024
% 0.14/0.33 % CPUTime :
% 0.61/0.80 % Version: 1.5
% 0.61/0.80 % SZS status Satisfiable
% 0.61/0.80 % SZS output start Saturation
% See solution above
% 0.61/0.80
% 0.61/0.80 % Initial clauses : 41
% 0.61/0.80 % Processed clauses : 180
% 0.61/0.80 % Factors computed : 66
% 0.61/0.80 % Resolvents computed: 131
% 0.61/0.80 % Tautologies deleted: 10
% 0.61/0.80 % Forward subsumed : 48
% 0.61/0.80 % Backward subsumed : 0
% 0.61/0.80 % -------- CPU Time ---------
% 0.61/0.80 % User time : 0.454 s
% 0.61/0.80 % System time : 0.019 s
% 0.61/0.80 % Total time : 0.473 s
%------------------------------------------------------------------------------