%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN774-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:49:00 EDT 2024
% Result : Satisfiable 0.48s 0.69s
% Output : Saturation 0.48s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssRr(skf3(X2),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause28,negated_conjecture,
( ~ ssRr(X200,X202)
| ~ ssPv4(X200)
| ~ ssRr(X202,X203)
| ~ ssPv1(X203)
| ~ ssRr(X202,X201)
| ~ ssPv2(X202)
| ssPv4(X201) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c118,plain,
( ~ ssRr(X420,skf3(X419))
| ~ ssPv4(X420)
| ~ ssRr(skf3(X419),X418)
| ~ ssPv1(X418)
| ~ ssPv2(skf3(X419))
| ssPv4(X419) ),
inference(resolution,[status(thm)],[clause28,clause1]) ).
cnf(c219,plain,
( ~ ssRr(skf3(X487),skf3(X487))
| ~ ssPv4(skf3(X487))
| ~ ssPv1(skf3(X487))
| ~ ssPv2(skf3(X487))
| ssPv4(X487) ),
inference(factor,[status(thm)],[c118]) ).
cnf(clause2,negated_conjecture,
ssRr(X3,skf2(X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause32,negated_conjecture,
( ~ ssRr(X251,X253)
| ~ ssPv2(X251)
| ~ ssRr(X253,X254)
| ~ ssPv4(X254)
| ~ ssRr(X253,X252)
| ~ ssPv3(X252)
| ~ ssPv3(X253) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c148,plain,
( ~ ssRr(X468,skf3(X470))
| ~ ssPv2(X468)
| ~ ssRr(skf3(X470),X469)
| ~ ssPv4(X469)
| ~ ssPv3(X470)
| ~ ssPv3(skf3(X470)) ),
inference(resolution,[status(thm)],[clause32,clause1]) ).
cnf(c240,plain,
( ~ ssRr(X485,skf3(X486))
| ~ ssPv2(X485)
| ~ ssPv4(skf2(skf3(X486)))
| ~ ssPv3(X486)
| ~ ssPv3(skf3(X486)) ),
inference(resolution,[status(thm)],[c148,clause2]) ).
cnf(clause31,negated_conjecture,
( ~ ssRr(X237,X239)
| ~ ssPv2(X237)
| ~ ssRr(X240,X239)
| ~ ssRr(X239,X238)
| ~ ssPv4(X238)
| ~ ssPv1(X239)
| ssPv1(X240) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c141,plain,
( ~ ssRr(X450,skf3(X451))
| ~ ssPv2(X450)
| ~ ssRr(X452,skf3(X451))
| ~ ssPv4(X451)
| ~ ssPv1(skf3(X451))
| ssPv1(X452) ),
inference(resolution,[status(thm)],[clause31,clause1]) ).
cnf(c233,plain,
( ~ ssRr(X483,skf3(X482))
| ~ ssPv2(X483)
| ~ ssPv4(X482)
| ~ ssPv1(skf3(X482))
| ssPv1(skf3(skf3(X482))) ),
inference(resolution,[status(thm)],[c141,clause1]) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X225,X227)
| ~ ssPv2(X225)
| ~ ssRr(X228,X227)
| ~ ssPv1(X228)
| ~ ssRr(X227,X226)
| ~ ssPv3(X227)
| ssPv1(X226) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c135,plain,
( ~ ssRr(X441,skf3(X439))
| ~ ssPv2(X441)
| ~ ssRr(X440,skf3(X439))
| ~ ssPv1(X440)
| ~ ssPv3(skf3(X439))
| ssPv1(X439) ),
inference(resolution,[status(thm)],[clause30,clause1]) ).
cnf(c229,plain,
( ~ ssRr(X479,skf3(X480))
| ~ ssPv2(X479)
| ~ ssPv1(skf3(skf3(X480)))
| ~ ssPv3(skf3(X480))
| ssPv1(X480) ),
inference(resolution,[status(thm)],[c135,clause1]) ).
cnf(clause29,negated_conjecture,
( ~ ssRr(X214,X216)
| ~ ssPv2(X214)
| ~ ssRr(X216,X217)
| ~ ssPv1(X217)
| ~ ssRr(X216,X215)
| ~ ssPv2(X216)
| ssPv1(X215) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c128,plain,
( ~ ssRr(X430,skf3(X429))
| ~ ssPv2(X430)
| ~ ssRr(skf3(X429),X428)
| ~ ssPv1(X428)
| ~ ssPv2(skf3(X429))
| ssPv1(X429) ),
inference(resolution,[status(thm)],[clause29,clause1]) ).
cnf(c224,plain,
( ~ ssRr(X478,skf3(X477))
| ~ ssPv2(X478)
| ~ ssPv1(skf2(skf3(X477)))
| ~ ssPv2(skf3(X477))
| ssPv1(X477) ),
inference(resolution,[status(thm)],[c128,clause2]) ).
cnf(c220,plain,
( ~ ssRr(X475,skf3(X476))
| ~ ssPv4(X475)
| ~ ssPv1(skf2(skf3(X476)))
| ~ ssPv2(skf3(X476))
| ssPv4(X476) ),
inference(resolution,[status(thm)],[c118,clause2]) ).
cnf(clause27,negated_conjecture,
( ~ ssRr(X189,X191)
| ~ ssPv1(X189)
| ~ ssRr(X191,X192)
| ~ ssPv3(X192)
| ~ ssRr(X191,X190)
| ~ ssPv4(X191)
| ssPv2(X190) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c111,plain,
( ~ ssRr(X399,skf3(X400))
| ~ ssPv1(X399)
| ~ ssRr(skf3(X400),X401)
| ~ ssPv3(X401)
| ~ ssPv4(skf3(X400))
| ssPv2(X400) ),
inference(resolution,[status(thm)],[clause27,clause1]) ).
cnf(c214,plain,
( ~ ssRr(X473,skf3(X474))
| ~ ssPv1(X473)
| ~ ssPv3(skf2(skf3(X474)))
| ~ ssPv4(skf3(X474))
| ssPv2(X474) ),
inference(resolution,[status(thm)],[c111,clause2]) ).
cnf(c134,plain,
( ~ ssRr(X387,X388)
| ~ ssPv2(X387)
| ~ ssRr(X386,X388)
| ~ ssPv1(X386)
| ~ ssPv3(X388)
| ssPv1(skf2(X388)) ),
inference(resolution,[status(thm)],[clause30,clause2]) ).
cnf(c209,plain,
( ~ ssRr(X464,skf2(X465))
| ~ ssPv2(X464)
| ~ ssPv1(X465)
| ~ ssPv3(skf2(X465))
| ssPv1(skf2(skf2(X465))) ),
inference(resolution,[status(thm)],[c134,clause2]) ).
cnf(c238,plain,
( ~ ssPv2(skf3(skf2(X467)))
| ~ ssPv1(X467)
| ~ ssPv3(skf2(X467))
| ssPv1(skf2(skf2(X467))) ),
inference(resolution,[status(thm)],[c209,clause1]) ).
cnf(c127,plain,
( ~ ssRr(X381,X382)
| ~ ssPv2(X381)
| ~ ssRr(X382,X380)
| ~ ssPv1(X380)
| ~ ssPv2(X382)
| ssPv1(skf2(X382)) ),
inference(resolution,[status(thm)],[clause29,clause2]) ).
cnf(c207,plain,
( ~ ssRr(X461,skf3(X462))
| ~ ssPv2(X461)
| ~ ssPv1(X462)
| ~ ssPv2(skf3(X462))
| ssPv1(skf2(skf3(X462))) ),
inference(resolution,[status(thm)],[c127,clause1]) ).
cnf(c236,plain,
( ~ ssPv2(skf3(skf3(X463)))
| ~ ssPv1(X463)
| ~ ssPv2(skf3(X463))
| ssPv1(skf2(skf3(X463))) ),
inference(resolution,[status(thm)],[c207,clause1]) ).
cnf(c138,plain,
( ~ ssRr(X249,X249)
| ~ ssPv2(X249)
| ~ ssRr(X248,X249)
| ~ ssPv4(X249)
| ~ ssPv1(X249)
| ssPv1(X248) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c143,plain,
( ~ ssRr(skf2(X460),skf2(X460))
| ~ ssPv2(skf2(X460))
| ~ ssPv4(skf2(X460))
| ~ ssPv1(skf2(X460))
| ssPv1(X460) ),
inference(resolution,[status(thm)],[c138,clause2]) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X177,X179)
| ~ ssPv2(X177)
| ~ ssRr(X180,X179)
| ~ ssRr(X179,X178)
| ~ ssPv4(X178)
| ssPv4(X180)
| ssPv1(X179) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c103,plain,
( ~ ssRr(X376,skf3(X375))
| ~ ssPv2(X376)
| ~ ssRr(X377,skf3(X375))
| ~ ssPv4(X375)
| ssPv4(X377)
| ssPv1(skf3(X375)) ),
inference(resolution,[status(thm)],[clause26,clause1]) ).
cnf(c203,plain,
( ~ ssRr(X457,skf3(X458))
| ~ ssPv2(X457)
| ~ ssPv4(X458)
| ssPv4(skf3(skf3(X458)))
| ssPv1(skf3(X458)) ),
inference(resolution,[status(thm)],[c103,clause1]) ).
cnf(c232,plain,
( ~ ssRr(X454,skf3(X453))
| ~ ssPv2(X454)
| ~ ssPv4(X453)
| ~ ssPv1(skf3(X453))
| ssPv1(X454) ),
inference(factor,[status(thm)],[c141]) ).
cnf(c234,plain,
( ~ ssPv2(skf3(skf3(X456)))
| ~ ssPv4(X456)
| ~ ssPv1(skf3(X456))
| ssPv1(skf3(skf3(X456))) ),
inference(resolution,[status(thm)],[c232,clause1]) ).
cnf(c117,plain,
( ~ ssRr(X370,X371)
| ~ ssPv4(X370)
| ~ ssRr(X371,X369)
| ~ ssPv1(X369)
| ~ ssPv2(X371)
| ssPv4(skf2(X371)) ),
inference(resolution,[status(thm)],[clause28,clause2]) ).
cnf(c201,plain,
( ~ ssRr(X449,skf3(X448))
| ~ ssPv4(X449)
| ~ ssPv1(X448)
| ~ ssPv2(skf3(X448))
| ssPv4(skf2(skf3(X448))) ),
inference(resolution,[status(thm)],[c117,clause1]) ).
cnf(c231,plain,
( ~ ssPv4(skf3(skf3(X455)))
| ~ ssPv1(X455)
| ~ ssPv2(skf3(X455))
| ssPv4(skf2(skf3(X455))) ),
inference(resolution,[status(thm)],[c201,clause1]) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X162,X164)
| ~ ssRr(X164,X165)
| ~ ssPv3(X165)
| ~ ssRr(X164,X163)
| ~ ssPv2(X163)
| ssPv2(X162)
| ssPv2(X164) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c96,plain,
( ~ ssRr(X364,skf3(X363))
| ~ ssRr(skf3(X363),X365)
| ~ ssPv3(X365)
| ~ ssPv2(X363)
| ssPv2(X364)
| ssPv2(skf3(X363)) ),
inference(resolution,[status(thm)],[clause25,clause1]) ).
cnf(c197,plain,
( ~ ssRr(X447,skf3(X446))
| ~ ssPv3(skf2(skf3(X446)))
| ~ ssPv2(X446)
| ssPv2(X447)
| ssPv2(skf3(X446)) ),
inference(resolution,[status(thm)],[c96,clause2]) ).
cnf(c228,plain,
( ~ ssRr(X442,skf3(X443))
| ~ ssPv2(X442)
| ~ ssPv1(X442)
| ~ ssPv3(skf3(X443))
| ssPv1(X443) ),
inference(factor,[status(thm)],[c135]) ).
cnf(c230,plain,
( ~ ssPv2(skf3(skf3(X445)))
| ~ ssPv1(skf3(skf3(X445)))
| ~ ssPv3(skf3(X445))
| ssPv1(X445) ),
inference(resolution,[status(thm)],[c228,clause1]) ).
cnf(c110,plain,
( ~ ssRr(X357,X359)
| ~ ssPv1(X357)
| ~ ssRr(X359,X358)
| ~ ssPv3(X358)
| ~ ssPv4(X359)
| ssPv2(skf2(X359)) ),
inference(resolution,[status(thm)],[clause27,clause2]) ).
cnf(c195,plain,
( ~ ssRr(X438,skf3(X437))
| ~ ssPv1(X438)
| ~ ssPv3(X437)
| ~ ssPv4(skf3(X437))
| ssPv2(skf2(skf3(X437))) ),
inference(resolution,[status(thm)],[c110,clause1]) ).
cnf(c227,plain,
( ~ ssPv1(skf3(skf3(X444)))
| ~ ssPv3(X444)
| ~ ssPv4(skf3(X444))
| ssPv2(skf2(skf3(X444))) ),
inference(resolution,[status(thm)],[c195,clause1]) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X152,X154)
| ~ ssPv2(X152)
| ~ ssRr(X155,X154)
| ~ ssRr(X154,X153)
| ~ ssPv3(X154)
| ssPv4(X155)
| ssPv3(X153) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c92,plain,
( ~ ssRr(X350,skf3(X349))
| ~ ssPv2(X350)
| ~ ssRr(X351,skf3(X349))
| ~ ssPv3(skf3(X349))
| ssPv4(X351)
| ssPv3(X349) ),
inference(resolution,[status(thm)],[clause24,clause1]) ).
cnf(c191,plain,
( ~ ssRr(X435,skf3(X434))
| ~ ssPv2(X435)
| ~ ssPv3(skf3(X434))
| ssPv4(skf3(skf3(X434)))
| ssPv3(X434) ),
inference(resolution,[status(thm)],[c92,clause1]) ).
cnf(c223,plain,
( ~ ssRr(skf3(X433),skf3(X433))
| ~ ssPv2(skf3(X433))
| ~ ssPv1(skf3(X433))
| ssPv1(X433) ),
inference(factor,[status(thm)],[c128]) ).
cnf(clause23,negated_conjecture,
( ~ ssRr(X142,X144)
| ~ ssPv1(X142)
| ~ ssRr(X145,X144)
| ~ ssRr(X144,X143)
| ~ ssPv4(X143)
| ssPv3(X145)
| ssPv3(X144) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c87,plain,
( ~ ssRr(X338,skf3(X337))
| ~ ssPv1(X338)
| ~ ssRr(X339,skf3(X337))
| ~ ssPv4(X337)
| ssPv3(X339)
| ssPv3(skf3(X337)) ),
inference(resolution,[status(thm)],[clause23,clause1]) ).
cnf(c186,plain,
( ~ ssRr(X425,skf3(X426))
| ~ ssPv1(X425)
| ~ ssPv4(X426)
| ssPv3(skf3(skf3(X426)))
| ssPv3(skf3(X426)) ),
inference(resolution,[status(thm)],[c87,clause1]) ).
cnf(c91,plain,
( ~ ssRr(X331,X333)
| ~ ssPv2(X331)
| ~ ssRr(X332,X333)
| ~ ssPv3(X333)
| ssPv4(X332)
| ssPv3(skf2(X333)) ),
inference(resolution,[status(thm)],[clause24,clause2]) ).
cnf(c181,plain,
( ~ ssRr(X416,skf2(X417))
| ~ ssPv2(X416)
| ~ ssPv3(skf2(X417))
| ssPv4(X417)
| ssPv3(skf2(skf2(X417))) ),
inference(resolution,[status(thm)],[c91,clause2]) ).
cnf(c218,plain,
( ~ ssPv2(skf3(skf2(X424)))
| ~ ssPv3(skf2(X424))
| ssPv4(X424)
| ssPv3(skf2(skf2(X424))) ),
inference(resolution,[status(thm)],[c181,clause1]) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X130,X132)
| ~ ssRr(X133,X132)
| ~ ssRr(X132,X131)
| ~ ssPv2(X131)
| ssPv3(X130)
| ssPv2(X133)
| ssPv2(X132) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c81,plain,
( ~ ssRr(X325,skf3(X323))
| ~ ssRr(X324,skf3(X323))
| ~ ssPv2(X323)
| ssPv3(X325)
| ssPv2(X324)
| ssPv2(skf3(X323)) ),
inference(resolution,[status(thm)],[clause22,clause1]) ).
cnf(c178,plain,
( ~ ssRr(X414,skf3(X413))
| ~ ssPv2(X413)
| ssPv3(X414)
| ssPv2(skf3(skf3(X413)))
| ssPv2(skf3(X413)) ),
inference(resolution,[status(thm)],[c81,clause1]) ).
cnf(c202,plain,
( ~ ssRr(X379,skf3(X378))
| ~ ssPv2(X379)
| ~ ssPv4(X378)
| ssPv4(X379)
| ssPv1(skf3(X378)) ),
inference(factor,[status(thm)],[c103]) ).
cnf(c204,plain,
( ~ ssPv2(skf3(skf3(X412)))
| ~ ssPv4(X412)
| ssPv4(skf3(skf3(X412)))
| ssPv1(skf3(X412)) ),
inference(resolution,[status(thm)],[c202,clause1]) ).
cnf(c190,plain,
( ~ ssRr(X353,skf3(X352))
| ~ ssPv2(X353)
| ~ ssPv3(skf3(X352))
| ssPv4(X353)
| ssPv3(X352) ),
inference(factor,[status(thm)],[c92]) ).
cnf(c192,plain,
( ~ ssPv2(skf3(skf3(X411)))
| ~ ssPv3(skf3(X411))
| ssPv4(skf3(skf3(X411)))
| ssPv3(X411) ),
inference(resolution,[status(thm)],[c190,clause1]) ).
cnf(c108,plain,
( ~ ssRr(X198,X198)
| ~ ssPv1(X198)
| ~ ssRr(X198,X197)
| ~ ssPv3(X197)
| ~ ssPv4(X198)
| ssPv2(X198) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c114,plain,
( ~ ssRr(skf3(X410),skf3(X410))
| ~ ssPv1(skf3(X410))
| ~ ssPv3(X410)
| ~ ssPv4(skf3(X410))
| ssPv2(skf3(X410)) ),
inference(resolution,[status(thm)],[c108,clause1]) ).
cnf(c185,plain,
( ~ ssRr(X344,skf3(X345))
| ~ ssPv1(X344)
| ~ ssPv4(X345)
| ssPv3(X344)
| ssPv3(skf3(X345)) ),
inference(factor,[status(thm)],[c87]) ).
cnf(c189,plain,
( ~ ssPv1(skf3(skf3(X409)))
| ~ ssPv4(X409)
| ssPv3(skf3(skf3(X409)))
| ssPv3(skf3(X409)) ),
inference(resolution,[status(thm)],[c185,clause1]) ).
cnf(c182,plain,
( ~ ssRr(X341,X342)
| ~ ssPv2(X341)
| ~ ssPv3(X342)
| ssPv4(skf3(X342))
| ssPv3(skf2(X342)) ),
inference(resolution,[status(thm)],[c91,clause1]) ).
cnf(c187,plain,
( ~ ssPv2(X408)
| ~ ssPv3(skf2(X408))
| ssPv4(skf3(skf2(X408)))
| ssPv3(skf2(skf2(X408))) ),
inference(resolution,[status(thm)],[c182,clause2]) ).
cnf(c177,plain,
( ~ ssRr(X326,skf3(X327))
| ~ ssPv2(X327)
| ssPv3(X326)
| ssPv2(X326)
| ssPv2(skf3(X327)) ),
inference(factor,[status(thm)],[c81]) ).
cnf(c179,plain,
( ~ ssPv2(X407)
| ssPv3(skf3(skf3(X407)))
| ssPv2(skf3(skf3(X407)))
| ssPv2(skf3(X407)) ),
inference(resolution,[status(thm)],[c177,clause1]) ).
cnf(c147,plain,
( ~ ssRr(X404,X406)
| ~ ssPv2(X404)
| ~ ssRr(X406,X405)
| ~ ssPv4(X405)
| ~ ssPv3(skf2(X406))
| ~ ssPv3(X406) ),
inference(resolution,[status(thm)],[clause32,clause2]) ).
cnf(c140,plain,
( ~ ssRr(X396,X398)
| ~ ssPv2(X396)
| ~ ssRr(X397,X398)
| ~ ssPv4(skf2(X398))
| ~ ssPv1(X398)
| ssPv1(X397) ),
inference(resolution,[status(thm)],[clause31,clause2]) ).
cnf(c210,plain,
( ~ ssRr(X395,X394)
| ~ ssPv2(X395)
| ~ ssPv1(skf3(X394))
| ~ ssPv3(X394)
| ssPv1(skf2(X394)) ),
inference(resolution,[status(thm)],[c134,clause1]) ).
cnf(c208,plain,
( ~ ssRr(X391,X390)
| ~ ssPv2(X391)
| ~ ssPv1(X391)
| ~ ssPv3(X390)
| ssPv1(skf2(X390)) ),
inference(factor,[status(thm)],[c134]) ).
cnf(c212,plain,
( ~ ssPv2(skf3(X393))
| ~ ssPv1(skf3(X393))
| ~ ssPv3(X393)
| ssPv1(skf2(X393)) ),
inference(resolution,[status(thm)],[c208,clause1]) ).
cnf(c211,plain,
( ~ ssPv2(X392)
| ~ ssPv1(X392)
| ~ ssPv3(skf2(X392))
| ssPv1(skf2(skf2(X392))) ),
inference(resolution,[status(thm)],[c208,clause2]) ).
cnf(c100,plain,
( ~ ssRr(X187,X187)
| ~ ssPv2(X187)
| ~ ssRr(X188,X187)
| ~ ssPv4(X187)
| ssPv4(X188)
| ssPv1(X187) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c106,plain,
( ~ ssRr(skf2(X389),skf2(X389))
| ~ ssPv2(skf2(X389))
| ~ ssPv4(skf2(X389))
| ssPv4(X389)
| ssPv1(skf2(X389)) ),
inference(resolution,[status(thm)],[c100,clause2]) ).
cnf(c205,plain,
( ~ ssRr(X383,X383)
| ~ ssPv2(X383)
| ~ ssPv1(X383)
| ssPv1(skf2(X383)) ),
inference(factor,[status(thm)],[c127]) ).
cnf(c199,plain,
( ~ ssRr(X372,X372)
| ~ ssPv4(X372)
| ~ ssPv1(X372)
| ~ ssPv2(X372)
| ssPv4(skf2(X372)) ),
inference(factor,[status(thm)],[c117]) ).
cnf(c196,plain,
( ~ ssRr(skf3(X368),skf3(X368))
| ~ ssPv3(skf3(X368))
| ~ ssPv2(X368)
| ssPv2(skf3(X368)) ),
inference(factor,[status(thm)],[c96]) ).
cnf(c102,plain,
( ~ ssRr(X354,X356)
| ~ ssPv2(X354)
| ~ ssRr(X355,X356)
| ~ ssPv4(skf2(X356))
| ssPv4(X355)
| ssPv1(X356) ),
inference(resolution,[status(thm)],[clause26,clause2]) ).
cnf(c95,plain,
( ~ ssRr(X346,X348)
| ~ ssRr(X348,X347)
| ~ ssPv3(X347)
| ~ ssPv2(skf2(X348))
| ssPv2(X346)
| ssPv2(X348) ),
inference(resolution,[status(thm)],[clause25,clause2]) ).
cnf(c180,plain,
( ~ ssRr(X334,X335)
| ~ ssPv2(X334)
| ~ ssPv3(X335)
| ssPv4(X334)
| ssPv3(skf2(X335)) ),
inference(factor,[status(thm)],[c91]) ).
cnf(c184,plain,
( ~ ssPv2(skf3(X340))
| ~ ssPv3(X340)
| ssPv4(skf3(X340))
| ssPv3(skf2(X340)) ),
inference(resolution,[status(thm)],[c180,clause1]) ).
cnf(c183,plain,
( ~ ssPv2(X336)
| ~ ssPv3(skf2(X336))
| ssPv4(X336)
| ssPv3(skf2(skf2(X336))) ),
inference(resolution,[status(thm)],[c180,clause2]) ).
cnf(c86,plain,
( ~ ssRr(X329,X330)
| ~ ssPv1(X329)
| ~ ssRr(X328,X330)
| ~ ssPv4(skf2(X330))
| ssPv3(X328)
| ssPv3(X330) ),
inference(resolution,[status(thm)],[clause23,clause2]) ).
cnf(c80,plain,
( ~ ssRr(X321,X322)
| ~ ssRr(X320,X322)
| ~ ssPv2(skf2(X322))
| ssPv3(X321)
| ssPv2(X320)
| ssPv2(X322) ),
inference(resolution,[status(thm)],[clause22,clause2]) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X127,X128)
| ~ ssPv3(X128)
| ~ ssRr(X127,X129)
| ~ ssPv1(X129)
| ~ ssPv1(X127)
| ~ ssPv3(X127) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c77,plain,
( ~ ssRr(skf3(X314),X315)
| ~ ssPv3(X315)
| ~ ssPv1(X314)
| ~ ssPv1(skf3(X314))
| ~ ssPv3(skf3(X314)) ),
inference(resolution,[status(thm)],[clause21,clause1]) ).
cnf(c175,plain,
( ~ ssPv3(skf2(skf3(X319)))
| ~ ssPv1(X319)
| ~ ssPv1(skf3(X319))
| ~ ssPv3(skf3(X319)) ),
inference(resolution,[status(thm)],[c77,clause2]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X118,X119)
| ~ ssPv2(X119)
| ~ ssRr(X118,X120)
| ~ ssPv1(X120)
| ~ ssPv2(X118)
| ~ ssPv3(X118) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c72,plain,
( ~ ssRr(skf3(X312),X313)
| ~ ssPv2(X313)
| ~ ssPv1(X312)
| ~ ssPv2(skf3(X312))
| ~ ssPv3(skf3(X312)) ),
inference(resolution,[status(thm)],[clause20,clause1]) ).
cnf(c173,plain,
( ~ ssPv2(skf2(skf3(X318)))
| ~ ssPv1(X318)
| ~ ssPv2(skf3(X318))
| ~ ssPv3(skf3(X318)) ),
inference(resolution,[status(thm)],[c72,clause2]) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X108,X109)
| ~ ssPv4(X108)
| ~ ssRr(X109,X110)
| ~ ssPv4(X110)
| ~ ssPv3(X109)
| ~ ssPv4(X109) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c68,plain,
( ~ ssRr(X310,skf3(X309))
| ~ ssPv4(X310)
| ~ ssPv4(X309)
| ~ ssPv3(skf3(X309))
| ~ ssPv4(skf3(X309)) ),
inference(resolution,[status(thm)],[clause19,clause1]) ).
cnf(c172,plain,
( ~ ssPv4(skf3(skf3(X311)))
| ~ ssPv4(X311)
| ~ ssPv3(skf3(X311))
| ~ ssPv4(skf3(X311)) ),
inference(resolution,[status(thm)],[c68,clause1]) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X102,X103)
| ~ ssPv3(X102)
| ~ ssRr(X104,X103)
| ~ ssPv2(X104)
| ~ ssPv4(X103)
| ssPv2(X103) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c62,plain,
( ~ ssRr(X305,skf2(X306))
| ~ ssPv3(X305)
| ~ ssPv2(X306)
| ~ ssPv4(skf2(X306))
| ssPv2(skf2(X306)) ),
inference(resolution,[status(thm)],[clause18,clause2]) ).
cnf(c171,plain,
( ~ ssPv3(skf3(skf2(X308)))
| ~ ssPv2(X308)
| ~ ssPv4(skf2(X308))
| ssPv2(skf2(X308)) ),
inference(resolution,[status(thm)],[c62,clause1]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X96,X97)
| ~ ssPv2(X96)
| ~ ssRr(X97,X98)
| ~ ssPv3(X98)
| ~ ssPv3(X97)
| ssPv4(X97) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c60,plain,
( ~ ssRr(X303,skf3(X302))
| ~ ssPv2(X303)
| ~ ssPv3(X302)
| ~ ssPv3(skf3(X302))
| ssPv4(skf3(X302)) ),
inference(resolution,[status(thm)],[clause17,clause1]) ).
cnf(c169,plain,
( ~ ssPv2(skf3(skf3(X304)))
| ~ ssPv3(X304)
| ~ ssPv3(skf3(X304))
| ssPv4(skf3(X304)) ),
inference(resolution,[status(thm)],[c60,clause1]) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X86,X87)
| ~ ssPv2(X86)
| ~ ssRr(X87,X88)
| ~ ssPv1(X87)
| ~ ssPv3(X87)
| ssPv3(X88) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c53,plain,
( ~ ssRr(X298,skf3(X297))
| ~ ssPv2(X298)
| ~ ssPv1(skf3(X297))
| ~ ssPv3(skf3(X297))
| ssPv3(X297) ),
inference(resolution,[status(thm)],[clause16,clause1]) ).
cnf(c168,plain,
( ~ ssPv2(skf3(skf3(X301)))
| ~ ssPv1(skf3(X301))
| ~ ssPv3(skf3(X301))
| ssPv3(X301) ),
inference(resolution,[status(thm)],[c53,clause1]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X76,X77)
| ~ ssPv3(X76)
| ~ ssRr(X78,X77)
| ~ ssPv1(X77)
| ~ ssPv4(X77)
| ssPv4(X78) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c47,plain,
( ~ ssRr(X295,skf2(X296))
| ~ ssPv3(X295)
| ~ ssPv1(skf2(X296))
| ~ ssPv4(skf2(X296))
| ssPv4(X296) ),
inference(resolution,[status(thm)],[clause15,clause2]) ).
cnf(c167,plain,
( ~ ssPv3(skf3(skf2(X300)))
| ~ ssPv1(skf2(X300))
| ~ ssPv4(skf2(X300))
| ssPv4(X300) ),
inference(resolution,[status(thm)],[c47,clause1]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X73,X74)
| ~ ssRr(X74,X75)
| ~ ssPv2(X75)
| ~ ssPv2(X74)
| ~ ssPv3(X74)
| ssPv1(X73) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c45,plain,
( ~ ssRr(X293,skf3(X292))
| ~ ssPv2(X292)
| ~ ssPv2(skf3(X292))
| ~ ssPv3(skf3(X292))
| ssPv1(X293) ),
inference(resolution,[status(thm)],[clause14,clause1]) ).
cnf(c165,plain,
( ~ ssPv2(X294)
| ~ ssPv2(skf3(X294))
| ~ ssPv3(skf3(X294))
| ssPv1(skf3(skf3(X294))) ),
inference(resolution,[status(thm)],[c45,clause1]) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X64,X65)
| ~ ssPv4(X65)
| ~ ssRr(X64,X66)
| ~ ssPv3(X64)
| ~ ssPv4(X64)
| ssPv4(X66) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c40,plain,
( ~ ssRr(skf3(X288),X289)
| ~ ssPv4(X289)
| ~ ssPv3(skf3(X288))
| ~ ssPv4(skf3(X288))
| ssPv4(X288) ),
inference(resolution,[status(thm)],[clause13,clause1]) ).
cnf(c163,plain,
( ~ ssPv4(skf2(skf3(X291)))
| ~ ssPv3(skf3(X291))
| ~ ssPv4(skf3(X291))
| ssPv4(X291) ),
inference(resolution,[status(thm)],[c40,clause2]) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X54,X55)
| ~ ssRr(X54,X56)
| ~ ssPv1(X54)
| ssPv4(X55)
| ssPv2(X56)
| ssPv2(X54) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c33,plain,
( ~ ssRr(skf3(X284),X285)
| ~ ssPv1(skf3(X284))
| ssPv4(X285)
| ssPv2(X284)
| ssPv2(skf3(X284)) ),
inference(resolution,[status(thm)],[clause12,clause1]) ).
cnf(c161,plain,
( ~ ssPv1(skf3(X287))
| ssPv4(skf2(skf3(X287)))
| ssPv2(X287)
| ssPv2(skf3(X287)) ),
inference(resolution,[status(thm)],[c33,clause2]) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X44,X45)
| ~ ssPv4(X45)
| ~ ssRr(X44,X46)
| ssPv3(X46)
| ssPv3(X44)
| ssPv4(X44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c26,plain,
( ~ ssRr(skf3(X280),X281)
| ~ ssPv4(X281)
| ssPv3(X280)
| ssPv3(skf3(X280))
| ssPv4(skf3(X280)) ),
inference(resolution,[status(thm)],[clause11,clause1]) ).
cnf(c159,plain,
( ~ ssPv4(skf2(skf3(X283)))
| ssPv3(X283)
| ssPv3(skf3(X283))
| ssPv4(skf3(X283)) ),
inference(resolution,[status(thm)],[c26,clause2]) ).
cnf(c145,plain,
( ~ ssRr(X256,X256)
| ~ ssPv2(X256)
| ~ ssRr(X256,X255)
| ~ ssPv4(X255)
| ~ ssPv3(X256) ),
inference(factor,[status(thm)],[clause32]) ).
cnf(c151,plain,
( ~ ssRr(skf3(X279),skf3(X279))
| ~ ssPv2(skf3(X279))
| ~ ssPv4(X279)
| ~ ssPv3(skf3(X279)) ),
inference(resolution,[status(thm)],[c145,clause1]) ).
cnf(c125,plain,
( ~ ssRr(X219,X219)
| ~ ssPv2(X219)
| ~ ssRr(X219,X220)
| ~ ssPv1(X220)
| ssPv1(X219) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c131,plain,
( ~ ssRr(skf3(X278),skf3(X278))
| ~ ssPv2(skf3(X278))
| ~ ssPv1(X278)
| ssPv1(skf3(X278)) ),
inference(resolution,[status(thm)],[c125,clause1]) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X34,X35)
| ~ ssRr(X36,X35)
| ~ ssPv4(X35)
| ssPv2(X34)
| ssPv1(X36)
| ssPv3(X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c18,plain,
( ~ ssRr(X273,skf2(X274))
| ~ ssPv4(skf2(X274))
| ssPv2(X273)
| ssPv1(X274)
| ssPv3(skf2(X274)) ),
inference(resolution,[status(thm)],[clause10,clause2]) ).
cnf(c158,plain,
( ~ ssPv4(skf2(X277))
| ssPv2(skf3(skf2(X277)))
| ssPv1(X277)
| ssPv3(skf2(X277)) ),
inference(resolution,[status(thm)],[c18,clause1]) ).
cnf(c146,plain,
( ~ ssRr(X264,X265)
| ~ ssPv2(X264)
| ~ ssRr(X265,X266)
| ~ ssPv4(X266)
| ~ ssPv3(X266)
| ~ ssPv3(X265) ),
inference(factor,[status(thm)],[clause32]) ).
cnf(c155,plain,
( ~ ssRr(X271,skf3(X272))
| ~ ssPv2(X271)
| ~ ssPv4(X272)
| ~ ssPv3(X272)
| ~ ssPv3(skf3(X272)) ),
inference(resolution,[status(thm)],[c146,clause1]) ).
cnf(c156,plain,
( ~ ssPv2(skf3(skf3(X276)))
| ~ ssPv4(X276)
| ~ ssPv3(X276)
| ~ ssPv3(skf3(X276)) ),
inference(resolution,[status(thm)],[c155,clause1]) ).
cnf(c154,plain,
( ~ ssRr(X269,X270)
| ~ ssPv2(X269)
| ~ ssPv4(skf2(X270))
| ~ ssPv3(skf2(X270))
| ~ ssPv3(X270) ),
inference(resolution,[status(thm)],[c146,clause2]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X25,X26)
| ~ ssRr(X26,X27)
| ~ ssPv3(X26)
| ssPv3(X25)
| ssPv4(X27)
| ssPv4(X26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c14,plain,
( ~ ssRr(X263,skf3(X262))
| ~ ssPv3(skf3(X262))
| ssPv3(X263)
| ssPv4(X262)
| ssPv4(skf3(X262)) ),
inference(resolution,[status(thm)],[clause9,clause1]) ).
cnf(c152,plain,
( ~ ssPv3(skf3(X268))
| ssPv3(skf3(skf3(X268)))
| ssPv4(X268)
| ssPv4(skf3(X268)) ),
inference(resolution,[status(thm)],[c14,clause1]) ).
cnf(c144,plain,
( ~ ssRr(X259,X259)
| ~ ssPv2(X259)
| ~ ssPv4(X259)
| ~ ssPv1(X259)
| ssPv1(skf3(X259)) ),
inference(resolution,[status(thm)],[c138,clause1]) ).
cnf(c150,plain,
( ~ ssRr(X258,X258)
| ~ ssPv2(X258)
| ~ ssPv4(skf2(X258))
| ~ ssPv3(X258) ),
inference(resolution,[status(thm)],[c145,clause2]) ).
cnf(c116,plain,
( ~ ssRr(X212,X213)
| ~ ssPv4(X212)
| ~ ssRr(X213,X211)
| ~ ssPv1(X211)
| ~ ssPv2(X213)
| ssPv4(X211) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c124,plain,
( ~ ssRr(X235,skf3(X234))
| ~ ssPv4(X235)
| ~ ssPv1(X234)
| ~ ssPv2(skf3(X234))
| ssPv4(X234) ),
inference(resolution,[status(thm)],[c116,clause1]) ).
cnf(c137,plain,
( ~ ssPv4(skf3(skf3(X236)))
| ~ ssPv1(X236)
| ~ ssPv2(skf3(X236))
| ssPv4(X236) ),
inference(resolution,[status(thm)],[c124,clause1]) ).
cnf(c123,plain,
( ~ ssRr(X232,X233)
| ~ ssPv4(X232)
| ~ ssPv1(skf2(X233))
| ~ ssPv2(X233)
| ssPv4(skf2(X233)) ),
inference(resolution,[status(thm)],[c116,clause2]) ).
cnf(c109,plain,
( ~ ssRr(X205,X206)
| ~ ssPv1(X205)
| ~ ssRr(X206,X207)
| ~ ssPv3(X207)
| ~ ssPv4(X206)
| ssPv2(X207) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c121,plain,
( ~ ssRr(X230,skf3(X229))
| ~ ssPv1(X230)
| ~ ssPv3(X229)
| ~ ssPv4(skf3(X229))
| ssPv2(X229) ),
inference(resolution,[status(thm)],[c109,clause1]) ).
cnf(c136,plain,
( ~ ssPv1(skf3(skf3(X231)))
| ~ ssPv3(X231)
| ~ ssPv4(skf3(X231))
| ssPv2(X231) ),
inference(resolution,[status(thm)],[c121,clause1]) ).
cnf(c120,plain,
( ~ ssRr(X223,X224)
| ~ ssPv1(X223)
| ~ ssPv3(skf2(X224))
| ~ ssPv4(X224)
| ssPv2(skf2(X224)) ),
inference(resolution,[status(thm)],[c109,clause2]) ).
cnf(c130,plain,
( ~ ssRr(X222,X222)
| ~ ssPv2(X222)
| ~ ssPv1(skf2(X222))
| ssPv1(X222) ),
inference(resolution,[status(thm)],[c125,clause2]) ).
cnf(c113,plain,
( ~ ssRr(X204,X204)
| ~ ssPv1(X204)
| ~ ssPv3(skf2(X204))
| ~ ssPv4(X204)
| ssPv2(X204) ),
inference(resolution,[status(thm)],[c108,clause2]) ).
cnf(c107,plain,
( ~ ssRr(X194,X194)
| ~ ssPv2(X194)
| ~ ssPv4(X194)
| ssPv4(skf3(X194))
| ssPv1(X194) ),
inference(resolution,[status(thm)],[c100,clause1]) ).
cnf(c94,plain,
( ~ ssRr(X174,X176)
| ~ ssRr(X176,X175)
| ~ ssPv3(X175)
| ~ ssPv2(X175)
| ssPv2(X174)
| ssPv2(X176) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c99,plain,
( ~ ssRr(X185,skf3(X184))
| ~ ssPv3(X184)
| ~ ssPv2(X184)
| ssPv2(X185)
| ssPv2(skf3(X184)) ),
inference(resolution,[status(thm)],[c94,clause1]) ).
cnf(c104,plain,
( ~ ssPv3(X186)
| ~ ssPv2(X186)
| ssPv2(skf3(skf3(X186)))
| ssPv2(skf3(X186)) ),
inference(resolution,[status(thm)],[c99,clause1]) ).
cnf(c98,plain,
( ~ ssRr(X182,X183)
| ~ ssPv3(skf2(X183))
| ~ ssPv2(skf2(X183))
| ssPv2(X182)
| ssPv2(X183) ),
inference(resolution,[status(thm)],[c94,clause2]) ).
cnf(c52,plain,
( ~ ssRr(X93,X94)
| ~ ssPv2(X93)
| ~ ssPv1(X94)
| ~ ssPv3(X94)
| ssPv3(skf2(X94)) ),
inference(resolution,[status(thm)],[clause16,clause2]) ).
cnf(c56,plain,
( ~ ssPv2(X159)
| ~ ssPv1(skf2(X159))
| ~ ssPv3(skf2(X159))
| ssPv3(skf2(skf2(X159))) ),
inference(resolution,[status(thm)],[c52,clause2]) ).
cnf(c48,plain,
( ~ ssRr(X90,X91)
| ~ ssPv3(X90)
| ~ ssPv1(X91)
| ~ ssPv4(X91)
| ssPv4(skf3(X91)) ),
inference(resolution,[status(thm)],[clause15,clause1]) ).
cnf(c54,plain,
( ~ ssPv3(X158)
| ~ ssPv1(skf2(X158))
| ~ ssPv4(skf2(X158))
| ssPv4(skf3(skf2(X158))) ),
inference(resolution,[status(thm)],[c48,clause2]) ).
cnf(c39,plain,
( ~ ssRr(X71,X70)
| ~ ssPv4(X70)
| ~ ssPv3(X71)
| ~ ssPv4(X71)
| ssPv4(skf2(X71)) ),
inference(resolution,[status(thm)],[clause13,clause2]) ).
cnf(c42,plain,
( ~ ssPv4(X157)
| ~ ssPv3(skf3(X157))
| ~ ssPv4(skf3(X157))
| ssPv4(skf2(skf3(X157))) ),
inference(resolution,[status(thm)],[c39,clause1]) ).
cnf(c32,plain,
( ~ ssRr(X63,X62)
| ~ ssPv1(X63)
| ssPv4(X62)
| ssPv2(skf2(X63))
| ssPv2(X63) ),
inference(resolution,[status(thm)],[clause12,clause2]) ).
cnf(c37,plain,
( ~ ssPv1(skf3(X156))
| ssPv4(X156)
| ssPv2(skf2(skf3(X156)))
| ssPv2(skf3(X156)) ),
inference(resolution,[status(thm)],[c32,clause1]) ).
cnf(c25,plain,
( ~ ssRr(X53,X52)
| ~ ssPv4(X52)
| ssPv3(skf2(X53))
| ssPv3(X53)
| ssPv4(X53) ),
inference(resolution,[status(thm)],[clause11,clause2]) ).
cnf(c30,plain,
( ~ ssPv4(X151)
| ssPv3(skf2(skf3(X151)))
| ssPv3(skf3(X151))
| ssPv4(skf3(X151)) ),
inference(resolution,[status(thm)],[c25,clause1]) ).
cnf(c19,plain,
( ~ ssRr(X43,X42)
| ~ ssPv4(X42)
| ssPv2(X43)
| ssPv1(skf3(X42))
| ssPv3(X42) ),
inference(resolution,[status(thm)],[clause10,clause1]) ).
cnf(c22,plain,
( ~ ssPv4(skf2(X150))
| ssPv2(X150)
| ssPv1(skf3(skf2(X150)))
| ssPv3(skf2(X150)) ),
inference(resolution,[status(thm)],[c19,clause2]) ).
cnf(c13,plain,
( ~ ssRr(X32,X33)
| ~ ssPv3(X33)
| ssPv3(X32)
| ssPv4(skf2(X33))
| ssPv4(X33) ),
inference(resolution,[status(thm)],[clause9,clause2]) ).
cnf(c15,plain,
( ~ ssPv3(skf2(X149))
| ssPv3(X149)
| ssPv4(skf2(skf2(X149)))
| ssPv4(skf2(X149)) ),
inference(resolution,[status(thm)],[c13,clause2]) ).
cnf(c85,plain,
( ~ ssRr(X147,X146)
| ~ ssPv1(X147)
| ~ ssRr(X146,X146)
| ~ ssPv4(X146)
| ssPv3(X146) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c88,plain,
( ~ ssRr(X148,X148)
| ~ ssPv1(X148)
| ~ ssPv4(X148)
| ssPv3(X148) ),
inference(factor,[status(thm)],[c85]) ).
cnf(c76,plain,
( ~ ssRr(X141,X140)
| ~ ssPv3(X140)
| ~ ssPv1(skf2(X141))
| ~ ssPv1(X141)
| ~ ssPv3(X141) ),
inference(resolution,[status(thm)],[clause21,clause2]) ).
cnf(c75,plain,
( ~ ssRr(X134,X135)
| ~ ssPv3(X135)
| ~ ssPv1(X135)
| ~ ssPv1(X134)
| ~ ssPv3(X134) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c83,plain,
( ~ ssPv3(X137)
| ~ ssPv1(X137)
| ~ ssPv1(skf3(X137))
| ~ ssPv3(skf3(X137)) ),
inference(resolution,[status(thm)],[c75,clause1]) ).
cnf(c82,plain,
( ~ ssPv3(skf2(X136))
| ~ ssPv1(skf2(X136))
| ~ ssPv1(X136)
| ~ ssPv3(X136) ),
inference(resolution,[status(thm)],[c75,clause2]) ).
cnf(c71,plain,
( ~ ssRr(X126,X125)
| ~ ssPv2(X125)
| ~ ssPv1(skf2(X126))
| ~ ssPv2(X126)
| ~ ssPv3(X126) ),
inference(resolution,[status(thm)],[clause20,clause2]) ).
cnf(c70,plain,
( ~ ssRr(X121,X122)
| ~ ssPv2(X122)
| ~ ssPv1(X122)
| ~ ssPv2(X121)
| ~ ssPv3(X121) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c74,plain,
( ~ ssPv2(X124)
| ~ ssPv1(X124)
| ~ ssPv2(skf3(X124))
| ~ ssPv3(skf3(X124)) ),
inference(resolution,[status(thm)],[c70,clause1]) ).
cnf(c73,plain,
( ~ ssPv2(skf2(X123))
| ~ ssPv1(skf2(X123))
| ~ ssPv2(X123)
| ~ ssPv3(X123) ),
inference(resolution,[status(thm)],[c70,clause2]) ).
cnf(c67,plain,
( ~ ssRr(X115,X116)
| ~ ssPv4(X115)
| ~ ssPv4(skf2(X116))
| ~ ssPv3(X116)
| ~ ssPv4(X116) ),
inference(resolution,[status(thm)],[clause19,clause2]) ).
cnf(c69,plain,
( ~ ssRr(skf2(X117),X117)
| ~ ssPv4(skf2(X117))
| ~ ssPv3(X117)
| ~ ssPv4(X117) ),
inference(factor,[status(thm)],[c67]) ).
cnf(c63,plain,
( ~ ssRr(X114,X113)
| ~ ssPv3(X114)
| ~ ssPv2(skf3(X113))
| ~ ssPv4(X113)
| ssPv2(X113) ),
inference(resolution,[status(thm)],[clause18,clause1]) ).
cnf(c61,plain,
( ~ ssRr(X105,X106)
| ~ ssPv3(X105)
| ~ ssPv2(X105)
| ~ ssPv4(X106)
| ssPv2(X106) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c65,plain,
( ~ ssPv3(skf3(X112))
| ~ ssPv2(skf3(X112))
| ~ ssPv4(X112)
| ssPv2(X112) ),
inference(resolution,[status(thm)],[c61,clause1]) ).
cnf(c66,plain,
( ~ ssRr(X111,X111)
| ~ ssPv4(X111)
| ~ ssPv3(X111) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c64,plain,
( ~ ssPv3(X107)
| ~ ssPv2(X107)
| ~ ssPv4(skf2(X107))
| ssPv2(skf2(X107)) ),
inference(resolution,[status(thm)],[c61,clause2]) ).
cnf(c59,plain,
( ~ ssRr(X100,X101)
| ~ ssPv2(X100)
| ~ ssPv3(skf2(X101))
| ~ ssPv3(X101)
| ssPv4(X101) ),
inference(resolution,[status(thm)],[clause17,clause2]) ).
cnf(c58,plain,
( ~ ssRr(X99,X99)
| ~ ssPv2(X99)
| ~ ssPv3(X99)
| ssPv4(X99) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c57,plain,
( ~ ssPv2(skf3(X95))
| ~ ssPv1(X95)
| ~ ssPv3(X95)
| ssPv3(skf2(X95)) ),
inference(resolution,[status(thm)],[c52,clause1]) ).
cnf(c44,plain,
( ~ ssRr(X84,X85)
| ~ ssPv2(skf2(X85))
| ~ ssPv2(X85)
| ~ ssPv3(X85)
| ssPv1(X84) ),
inference(resolution,[status(thm)],[clause14,clause2]) ).
cnf(c46,plain,
( ~ ssRr(X81,X80)
| ~ ssPv3(X81)
| ~ ssPv1(X80)
| ~ ssPv4(X80)
| ssPv4(X81) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c50,plain,
( ~ ssPv3(skf3(X83))
| ~ ssPv1(X83)
| ~ ssPv4(X83)
| ssPv4(skf3(X83)) ),
inference(resolution,[status(thm)],[c46,clause1]) ).
cnf(c49,plain,
( ~ ssPv3(X82)
| ~ ssPv1(skf2(X82))
| ~ ssPv4(skf2(X82))
| ssPv4(X82) ),
inference(resolution,[status(thm)],[c46,clause2]) ).
cnf(c43,plain,
( ~ ssRr(X79,X79)
| ~ ssPv2(X79)
| ~ ssPv3(X79)
| ssPv1(X79) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c31,plain,
( ~ ssRr(X58,X59)
| ~ ssPv1(X58)
| ssPv4(X59)
| ssPv2(X59)
| ssPv2(X58) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(c35,plain,
( ~ ssPv1(skf3(X61))
| ssPv4(X61)
| ssPv2(X61)
| ssPv2(skf3(X61)) ),
inference(resolution,[status(thm)],[c31,clause1]) ).
cnf(c34,plain,
( ~ ssPv1(X60)
| ssPv4(skf2(X60))
| ssPv2(skf2(X60))
| ssPv2(X60) ),
inference(resolution,[status(thm)],[c31,clause2]) ).
cnf(c24,plain,
( ~ ssRr(X48,X49)
| ~ ssPv4(X49)
| ssPv3(X49)
| ssPv3(X48)
| ssPv4(X48) ),
inference(factor,[status(thm)],[clause11]) ).
cnf(c28,plain,
( ~ ssPv4(X51)
| ssPv3(X51)
| ssPv3(skf3(X51))
| ssPv4(skf3(X51)) ),
inference(resolution,[status(thm)],[c24,clause1]) ).
cnf(c27,plain,
( ~ ssPv4(skf2(X50))
| ssPv3(skf2(X50))
| ssPv3(X50)
| ssPv4(X50) ),
inference(resolution,[status(thm)],[c24,clause2]) ).
cnf(c17,plain,
( ~ ssRr(X39,X38)
| ~ ssPv4(X38)
| ssPv2(X39)
| ssPv1(X39)
| ssPv3(X38) ),
inference(factor,[status(thm)],[clause10]) ).
cnf(c21,plain,
( ~ ssPv4(X41)
| ssPv2(skf3(X41))
| ssPv1(skf3(X41))
| ssPv3(X41) ),
inference(resolution,[status(thm)],[c17,clause1]) ).
cnf(c20,plain,
( ~ ssPv4(skf2(X40))
| ssPv2(X40)
| ssPv1(X40)
| ssPv3(skf2(X40)) ),
inference(resolution,[status(thm)],[c17,clause2]) ).
cnf(c16,plain,
( ~ ssPv3(X37)
| ssPv3(skf3(X37))
| ssPv4(skf2(X37))
| ssPv4(X37) ),
inference(resolution,[status(thm)],[c13,clause1]) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X18,X19)
| ~ ssPv1(X18)
| ~ ssPv1(X19)
| ~ ssPv2(X19)
| ~ ssPv4(X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c10,plain,
( ~ ssPv1(X31)
| ~ ssPv1(skf2(X31))
| ~ ssPv2(skf2(X31))
| ~ ssPv4(skf2(X31)) ),
inference(resolution,[status(thm)],[clause8,clause2]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X16,X17)
| ~ ssPv4(X16)
| ~ ssPv1(X17)
| ~ ssPv3(X17)
| ssPv2(X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c8,plain,
( ~ ssPv4(X30)
| ~ ssPv1(skf2(X30))
| ~ ssPv3(skf2(X30))
| ssPv2(skf2(X30)) ),
inference(resolution,[status(thm)],[clause7,clause2]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X13,X14)
| ~ ssPv3(X14)
| ~ ssPv4(X14)
| ssPv1(X13)
| ssPv1(X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c6,plain,
( ~ ssPv3(skf2(X29))
| ~ ssPv4(skf2(X29))
| ssPv1(X29)
| ssPv1(skf2(X29)) ),
inference(resolution,[status(thm)],[clause6,clause2]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X9,X10)
| ~ ssPv3(X9)
| ~ ssPv4(X10)
| ssPv2(X10)
| ssPv3(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c4,plain,
( ~ ssPv3(X24)
| ~ ssPv4(skf2(X24))
| ssPv2(skf2(X24))
| ssPv3(skf2(X24)) ),
inference(resolution,[status(thm)],[clause5,clause2]) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X7,X8)
| ~ ssPv1(X8)
| ~ ssPv3(X8)
| ssPv2(X7)
| ssPv4(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c2,plain,
( ~ ssPv1(skf2(X23))
| ~ ssPv3(skf2(X23))
| ssPv2(X23)
| ssPv4(skf2(X23)) ),
inference(resolution,[status(thm)],[clause4,clause2]) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssPv3(X4)
| ssPv1(X5)
| ssPv3(X5)
| ssPv4(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c0,plain,
( ~ ssPv3(X22)
| ssPv1(skf2(X22))
| ssPv3(skf2(X22))
| ssPv4(skf2(X22)) ),
inference(resolution,[status(thm)],[clause3,clause2]) ).
cnf(c11,plain,
( ~ ssPv1(skf3(X21))
| ~ ssPv1(X21)
| ~ ssPv2(X21)
| ~ ssPv4(X21) ),
inference(resolution,[status(thm)],[clause8,clause1]) ).
cnf(c9,plain,
( ~ ssPv4(skf3(X20))
| ~ ssPv1(X20)
| ~ ssPv3(X20)
| ssPv2(X20) ),
inference(resolution,[status(thm)],[clause7,clause1]) ).
cnf(c7,plain,
( ~ ssPv3(X15)
| ~ ssPv4(X15)
| ssPv1(skf3(X15))
| ssPv1(X15) ),
inference(resolution,[status(thm)],[clause6,clause1]) ).
cnf(c5,plain,
( ~ ssPv3(skf3(X12))
| ~ ssPv4(X12)
| ssPv2(X12)
| ssPv3(X12) ),
inference(resolution,[status(thm)],[clause5,clause1]) ).
cnf(c3,plain,
( ~ ssPv1(X11)
| ~ ssPv3(X11)
| ssPv2(skf3(X11))
| ssPv4(X11) ),
inference(resolution,[status(thm)],[clause4,clause1]) ).
cnf(c1,plain,
( ~ ssPv3(skf3(X6))
| ssPv1(X6)
| ssPv3(X6)
| ssPv4(X6) ),
inference(resolution,[status(thm)],[clause3,clause1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SYN774-1 : TPTP v8.1.2. Released v2.5.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.31 % Computer : n032.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.31 % CPULimit : 300
% 0.16/0.31 % WCLimit : 300
% 0.16/0.31 % DateTime : Wed May 8 19:59:37 EDT 2024
% 0.16/0.31 % CPUTime :
% 0.48/0.69 % Version: 1.5
% 0.48/0.69 % SZS status Satisfiable
% 0.48/0.69 % SZS output start Saturation
% See solution above
% 0.48/0.69
% 0.48/0.69 % Initial clauses : 32
% 0.48/0.69 % Processed clauses : 219
% 0.48/0.69 % Factors computed : 62
% 0.48/0.69 % Resolvents computed: 181
% 0.48/0.69 % Tautologies deleted: 22
% 0.48/0.69 % Forward subsumed : 34
% 0.48/0.69 % Backward subsumed : 0
% 0.48/0.69 % -------- CPU Time ---------
% 0.48/0.69 % User time : 0.357 s
% 0.48/0.69 % System time : 0.010 s
% 0.48/0.69 % Total time : 0.367 s
%------------------------------------------------------------------------------