%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN756-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:48 EDT 2024
% Result : Satisfiable 0.70s 0.89s
% Output : Saturation 0.70s
% 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(clause51,negated_conjecture,
( ~ ssRr(X426,X423)
| ~ ssPv4(X423)
| ~ ssRr(X426,X425)
| ~ ssPv3(X425)
| ~ ssRr(X426,X424)
| ~ ssPv2(X426)
| ssPv2(X424) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(c184,plain,
( ~ ssRr(X587,X588)
| ~ ssPv4(X588)
| ~ ssRr(X587,X586)
| ~ ssPv3(X586)
| ~ ssPv2(X587)
| ssPv2(skf1(X587)) ),
inference(resolution,[status(thm)],[clause51,clause1]) ).
cnf(c240,plain,
( ~ ssRr(X589,X590)
| ~ ssPv4(X590)
| ~ ssPv3(X590)
| ~ ssPv2(X589)
| ssPv2(skf1(X589)) ),
inference(factor,[status(thm)],[c184]) ).
cnf(c183,plain,
( ~ ssRr(X533,X535)
| ~ ssPv4(X535)
| ~ ssRr(X533,X534)
| ~ ssPv3(X534)
| ~ ssPv2(X533)
| ssPv2(X534) ),
inference(factor,[status(thm)],[clause51]) ).
cnf(c229,plain,
( ~ ssRr(X584,X585)
| ~ ssPv4(X585)
| ~ ssPv3(skf1(X584))
| ~ ssPv2(X584)
| ssPv2(skf1(X584)) ),
inference(resolution,[status(thm)],[c183,clause1]) ).
cnf(clause50,negated_conjecture,
( ~ ssRr(X412,X409)
| ~ ssPv4(X409)
| ~ ssRr(X412,X411)
| ~ ssPv1(X411)
| ~ ssRr(X412,X410)
| ~ ssPv1(X412)
| ssPv2(X410) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c177,plain,
( ~ ssRr(X574,X575)
| ~ ssPv4(X575)
| ~ ssRr(X574,X576)
| ~ ssPv1(X576)
| ~ ssPv1(X574)
| ssPv2(skf1(X574)) ),
inference(resolution,[status(thm)],[clause50,clause1]) ).
cnf(c237,plain,
( ~ ssRr(X578,X577)
| ~ ssPv4(X577)
| ~ ssPv1(X577)
| ~ ssPv1(X578)
| ssPv2(skf1(X578)) ),
inference(factor,[status(thm)],[c177]) ).
cnf(c176,plain,
( ~ ssRr(X510,X509)
| ~ ssPv4(X509)
| ~ ssRr(X510,X508)
| ~ ssPv1(X508)
| ~ ssPv1(X510)
| ssPv2(X508) ),
inference(factor,[status(thm)],[clause50]) ).
cnf(c218,plain,
( ~ ssRr(X572,X573)
| ~ ssPv4(X573)
| ~ ssPv1(skf1(X572))
| ~ ssPv1(X572)
| ssPv2(skf1(X572)) ),
inference(resolution,[status(thm)],[c176,clause1]) ).
cnf(clause49,negated_conjecture,
( ~ ssRr(X398,X395)
| ~ ssPv4(X395)
| ~ ssRr(X398,X397)
| ~ ssPv2(X397)
| ~ ssRr(X398,X396)
| ~ ssPv1(X396)
| ssPv1(X398) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c170,plain,
( ~ ssRr(X482,X481)
| ~ ssPv4(X481)
| ~ ssRr(X482,X483)
| ~ ssPv2(X483)
| ~ ssPv1(X483)
| ssPv1(X482) ),
inference(factor,[status(thm)],[clause49]) ).
cnf(c207,plain,
( ~ ssRr(X567,X566)
| ~ ssPv4(X566)
| ~ ssPv2(skf1(X567))
| ~ ssPv1(skf1(X567))
| ssPv1(X567) ),
inference(resolution,[status(thm)],[c170,clause1]) ).
cnf(c171,plain,
( ~ ssRr(X562,X561)
| ~ ssPv4(X561)
| ~ ssRr(X562,X563)
| ~ ssPv2(X563)
| ~ ssPv1(skf1(X562))
| ssPv1(X562) ),
inference(resolution,[status(thm)],[clause49,clause1]) ).
cnf(clause48,negated_conjecture,
( ~ ssRr(X383,X380)
| ~ ssPv2(X380)
| ~ ssRr(X383,X382)
| ~ ssRr(X383,X381)
| ~ ssPv3(X383)
| ssPv4(X382)
| ssPv3(X381) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
cnf(c163,plain,
( ~ ssRr(X457,X455)
| ~ ssPv2(X455)
| ~ ssRr(X457,X456)
| ~ ssPv3(X457)
| ssPv4(X456)
| ssPv3(X456) ),
inference(factor,[status(thm)],[clause48]) ).
cnf(c197,plain,
( ~ ssRr(X556,X557)
| ~ ssPv2(X557)
| ~ ssPv3(X556)
| ssPv4(skf1(X556))
| ssPv3(skf1(X556)) ),
inference(resolution,[status(thm)],[c163,clause1]) ).
cnf(c164,plain,
( ~ ssRr(X550,X552)
| ~ ssPv2(X552)
| ~ ssRr(X550,X551)
| ~ ssPv3(X550)
| ssPv4(X551)
| ssPv3(skf1(X550)) ),
inference(resolution,[status(thm)],[clause48,clause1]) ).
cnf(c233,plain,
( ~ ssRr(X554,X553)
| ~ ssPv2(X553)
| ~ ssPv3(X554)
| ssPv4(X553)
| ssPv3(skf1(X554)) ),
inference(factor,[status(thm)],[c164]) ).
cnf(clause47,negated_conjecture,
( ~ ssRr(X367,X364)
| ~ ssPv4(X364)
| ~ ssRr(X367,X366)
| ~ ssPv1(X366)
| ~ ssRr(X367,X365)
| ssPv2(X365)
| ssPv1(X367) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
cnf(c155,plain,
( ~ ssRr(X430,X429)
| ~ ssPv4(X429)
| ~ ssRr(X430,X428)
| ~ ssPv1(X428)
| ssPv2(X428)
| ssPv1(X430) ),
inference(factor,[status(thm)],[clause47]) ).
cnf(c186,plain,
( ~ ssRr(X544,X545)
| ~ ssPv4(X545)
| ~ ssPv1(skf1(X544))
| ssPv2(skf1(X544))
| ssPv1(X544) ),
inference(resolution,[status(thm)],[c155,clause1]) ).
cnf(c156,plain,
( ~ ssRr(X538,X539)
| ~ ssPv4(X539)
| ~ ssRr(X538,X540)
| ~ ssPv1(X540)
| ssPv2(skf1(X538))
| ssPv1(X538) ),
inference(resolution,[status(thm)],[clause47,clause1]) ).
cnf(c230,plain,
( ~ ssRr(X541,X542)
| ~ ssPv4(X542)
| ~ ssPv1(X542)
| ssPv2(skf1(X541))
| ssPv1(X541) ),
inference(factor,[status(thm)],[c156]) ).
cnf(clause46,negated_conjecture,
( ~ ssRr(X352,X349)
| ~ ssPv4(X349)
| ~ ssRr(X352,X351)
| ~ ssPv3(X351)
| ~ ssRr(X352,X350)
| ssPv2(X350)
| ssPv1(X352) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(c150,plain,
( ~ ssRr(X527,X528)
| ~ ssPv4(X528)
| ~ ssRr(X527,X526)
| ~ ssPv3(X526)
| ssPv2(skf1(X527))
| ssPv1(X527) ),
inference(resolution,[status(thm)],[clause46,clause1]) ).
cnf(c225,plain,
( ~ ssRr(X530,X531)
| ~ ssPv4(X531)
| ~ ssPv3(X531)
| ssPv2(skf1(X530))
| ssPv1(X530) ),
inference(factor,[status(thm)],[c150]) ).
cnf(c182,plain,
( ~ ssRr(X519,X520)
| ~ ssPv4(X520)
| ~ ssRr(X519,X521)
| ~ ssPv3(X521)
| ~ ssPv2(X519)
| ssPv2(X520) ),
inference(factor,[status(thm)],[clause51]) ).
cnf(c222,plain,
( ~ ssRr(X522,X523)
| ~ ssPv4(X523)
| ~ ssPv3(X523)
| ~ ssPv2(X522)
| ssPv2(X523) ),
inference(factor,[status(thm)],[c182]) ).
cnf(c224,plain,
( ~ ssPv4(skf1(X529))
| ~ ssPv3(skf1(X529))
| ~ ssPv2(X529)
| ssPv2(skf1(X529)) ),
inference(resolution,[status(thm)],[c222,clause1]) ).
cnf(c223,plain,
( ~ ssRr(X524,X525)
| ~ ssPv4(X525)
| ~ ssPv3(skf1(X524))
| ~ ssPv2(X524)
| ssPv2(X525) ),
inference(resolution,[status(thm)],[c182,clause1]) ).
cnf(clause45,negated_conjecture,
( ~ ssRr(X337,X334)
| ~ ssPv4(X334)
| ~ ssRr(X337,X336)
| ~ ssPv1(X336)
| ~ ssRr(X337,X335)
| ssPv3(X335)
| ssPv1(X337) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(c144,plain,
( ~ ssRr(X513,X515)
| ~ ssPv4(X515)
| ~ ssRr(X513,X514)
| ~ ssPv1(X514)
| ssPv3(skf1(X513))
| ssPv1(X513) ),
inference(resolution,[status(thm)],[clause45,clause1]) ).
cnf(c219,plain,
( ~ ssRr(X516,X517)
| ~ ssPv4(X517)
| ~ ssPv1(X517)
| ssPv3(skf1(X516))
| ssPv1(X516) ),
inference(factor,[status(thm)],[c144]) ).
cnf(clause44,negated_conjecture,
( ~ ssRr(X324,X321)
| ~ ssPv3(X321)
| ~ ssRr(X324,X323)
| ~ ssPv2(X323)
| ~ ssRr(X324,X322)
| ssPv3(X322)
| ssPv1(X324) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(c138,plain,
( ~ ssRr(X501,X502)
| ~ ssPv3(X502)
| ~ ssRr(X501,X503)
| ~ ssPv2(X503)
| ssPv3(skf1(X501))
| ssPv1(X501) ),
inference(resolution,[status(thm)],[clause44,clause1]) ).
cnf(c214,plain,
( ~ ssRr(X505,X506)
| ~ ssPv3(X506)
| ~ ssPv2(X506)
| ssPv3(skf1(X505))
| ssPv1(X505) ),
inference(factor,[status(thm)],[c138]) ).
cnf(c175,plain,
( ~ ssRr(X496,X494)
| ~ ssPv4(X494)
| ~ ssRr(X496,X495)
| ~ ssPv1(X495)
| ~ ssPv1(X496)
| ssPv2(X494) ),
inference(factor,[status(thm)],[clause50]) ).
cnf(c211,plain,
( ~ ssRr(X497,X498)
| ~ ssPv4(X498)
| ~ ssPv1(X498)
| ~ ssPv1(X497)
| ssPv2(X498) ),
inference(factor,[status(thm)],[c175]) ).
cnf(c213,plain,
( ~ ssPv4(skf1(X504))
| ~ ssPv1(skf1(X504))
| ~ ssPv1(X504)
| ssPv2(skf1(X504)) ),
inference(resolution,[status(thm)],[c211,clause1]) ).
cnf(c212,plain,
( ~ ssRr(X499,X500)
| ~ ssPv4(X500)
| ~ ssPv1(skf1(X499))
| ~ ssPv1(X499)
| ssPv2(X500) ),
inference(resolution,[status(thm)],[c175,clause1]) ).
cnf(clause43,negated_conjecture,
( ~ ssRr(X310,X307)
| ~ ssPv2(X307)
| ~ ssRr(X310,X309)
| ~ ssRr(X310,X308)
| ~ ssPv2(X310)
| ssPv3(X309)
| ssPv2(X308) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(c131,plain,
( ~ ssRr(X488,X489)
| ~ ssPv2(X489)
| ~ ssRr(X488,X490)
| ~ ssPv2(X488)
| ssPv3(X490)
| ssPv2(skf1(X488)) ),
inference(resolution,[status(thm)],[clause43,clause1]) ).
cnf(c208,plain,
( ~ ssRr(X492,X491)
| ~ ssPv2(X491)
| ~ ssPv2(X492)
| ssPv3(X491)
| ssPv2(skf1(X492)) ),
inference(factor,[status(thm)],[c131]) ).
cnf(c149,plain,
( ~ ssRr(X404,X405)
| ~ ssPv4(X405)
| ~ ssRr(X404,X406)
| ~ ssPv3(X406)
| ssPv2(X406)
| ssPv1(X404) ),
inference(factor,[status(thm)],[clause46]) ).
cnf(c174,plain,
( ~ ssRr(X486,X487)
| ~ ssPv4(X487)
| ~ ssPv3(skf1(X486))
| ssPv2(skf1(X486))
| ssPv1(X486) ),
inference(resolution,[status(thm)],[c149,clause1]) ).
cnf(clause42,negated_conjecture,
( ~ ssRr(X295,X292)
| ~ ssPv2(X292)
| ~ ssRr(X295,X294)
| ~ ssPv1(X294)
| ~ ssRr(X295,X293)
| ssPv3(X293)
| ssPv3(X295) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c124,plain,
( ~ ssRr(X475,X477)
| ~ ssPv2(X477)
| ~ ssRr(X475,X476)
| ~ ssPv1(X476)
| ssPv3(skf1(X475))
| ssPv3(X475) ),
inference(resolution,[status(thm)],[clause42,clause1]) ).
cnf(c203,plain,
( ~ ssRr(X478,X479)
| ~ ssPv2(X479)
| ~ ssPv1(X479)
| ssPv3(skf1(X478))
| ssPv3(X478) ),
inference(factor,[status(thm)],[c124]) ).
cnf(c169,plain,
( ~ ssRr(X468,X467)
| ~ ssPv4(X467)
| ~ ssRr(X468,X469)
| ~ ssPv2(X469)
| ~ ssPv1(X467)
| ssPv1(X468) ),
inference(factor,[status(thm)],[clause49]) ).
cnf(c200,plain,
( ~ ssRr(X470,X471)
| ~ ssPv4(X471)
| ~ ssPv2(X471)
| ~ ssPv1(X471)
| ssPv1(X470) ),
inference(factor,[status(thm)],[c169]) ).
cnf(c202,plain,
( ~ ssPv4(skf1(X474))
| ~ ssPv2(skf1(X474))
| ~ ssPv1(skf1(X474))
| ssPv1(X474) ),
inference(resolution,[status(thm)],[c200,clause1]) ).
cnf(c201,plain,
( ~ ssRr(X472,X473)
| ~ ssPv4(X473)
| ~ ssPv2(skf1(X472))
| ~ ssPv1(X473)
| ssPv1(X472) ),
inference(resolution,[status(thm)],[c169,clause1]) ).
cnf(clause41,negated_conjecture,
( ~ ssRr(X279,X276)
| ~ ssPv3(X276)
| ~ ssRr(X279,X278)
| ~ ssRr(X279,X277)
| ssPv3(X278)
| ssPv2(X277)
| ssPv1(X279) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c116,plain,
( ~ ssRr(X462,X464)
| ~ ssPv3(X464)
| ~ ssRr(X462,X463)
| ssPv3(X463)
| ssPv2(skf1(X462))
| ssPv1(X462) ),
inference(resolution,[status(thm)],[clause41,clause1]) ).
cnf(c143,plain,
( ~ ssRr(X385,X387)
| ~ ssPv4(X387)
| ~ ssRr(X385,X386)
| ~ ssPv1(X386)
| ssPv3(X386)
| ssPv1(X385) ),
inference(factor,[status(thm)],[clause45]) ).
cnf(c166,plain,
( ~ ssRr(X460,X461)
| ~ ssPv4(X461)
| ~ ssPv1(skf1(X460))
| ssPv3(skf1(X460))
| ssPv1(X460) ),
inference(resolution,[status(thm)],[c143,clause1]) ).
cnf(clause40,negated_conjecture,
( ~ ssRr(X266,X263)
| ~ ssPv2(X263)
| ~ ssRr(X266,X265)
| ~ ssRr(X266,X264)
| ssPv2(X265)
| ssPv1(X264)
| ssPv3(X266) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c109,plain,
( ~ ssRr(X450,X451)
| ~ ssPv2(X451)
| ~ ssRr(X450,X449)
| ssPv2(X449)
| ssPv1(skf1(X450))
| ssPv3(X450) ),
inference(resolution,[status(thm)],[clause40,clause1]) ).
cnf(c162,plain,
( ~ ssRr(X437,X436)
| ~ ssPv2(X436)
| ~ ssRr(X437,X435)
| ~ ssPv3(X437)
| ssPv4(X435)
| ssPv3(X436) ),
inference(factor,[status(thm)],[clause48]) ).
cnf(c187,plain,
( ~ ssRr(X442,X441)
| ~ ssPv2(X441)
| ~ ssPv3(X442)
| ssPv4(X441)
| ssPv3(X441) ),
inference(factor,[status(thm)],[c162]) ).
cnf(c191,plain,
( ~ ssPv2(skf1(X447))
| ~ ssPv3(X447)
| ssPv4(skf1(X447))
| ssPv3(skf1(X447)) ),
inference(resolution,[status(thm)],[c187,clause1]) ).
cnf(clause39,negated_conjecture,
( ~ ssRr(X262,X259)
| ~ ssPv2(X259)
| ~ ssRr(X262,X261)
| ~ ssRr(X262,X260)
| ssPv3(X261)
| ssPv1(X260)
| ssPv4(X262) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c106,plain,
( ~ ssRr(X439,X440)
| ~ ssPv2(X440)
| ~ ssRr(X439,X438)
| ssPv3(X438)
| ssPv1(skf1(X439))
| ssPv4(X439) ),
inference(resolution,[status(thm)],[clause39,clause1]) ).
cnf(c189,plain,
( ~ ssRr(X446,X445)
| ~ ssPv2(X445)
| ssPv3(X445)
| ssPv1(skf1(X446))
| ssPv4(X446) ),
inference(factor,[status(thm)],[c106]) ).
cnf(c188,plain,
( ~ ssRr(X443,X444)
| ~ ssPv2(X444)
| ~ ssPv3(X443)
| ssPv4(skf1(X443))
| ssPv3(X444) ),
inference(resolution,[status(thm)],[c162,clause1]) ).
cnf(c137,plain,
( ~ ssRr(X370,X369)
| ~ ssPv3(X369)
| ~ ssRr(X370,X368)
| ~ ssPv2(X368)
| ssPv3(X368)
| ssPv1(X370) ),
inference(factor,[status(thm)],[clause44]) ).
cnf(c158,plain,
( ~ ssRr(X433,X434)
| ~ ssPv3(X434)
| ~ ssPv2(skf1(X433))
| ssPv3(skf1(X433))
| ssPv1(X433) ),
inference(resolution,[status(thm)],[c137,clause1]) ).
cnf(c154,plain,
( ~ ssRr(X417,X416)
| ~ ssPv4(X416)
| ~ ssRr(X417,X418)
| ~ ssPv1(X418)
| ssPv2(X416)
| ssPv1(X417) ),
inference(factor,[status(thm)],[clause47]) ).
cnf(c179,plain,
( ~ ssRr(X420,X419)
| ~ ssPv4(X419)
| ~ ssPv1(X419)
| ssPv2(X419)
| ssPv1(X420) ),
inference(factor,[status(thm)],[c154]) ).
cnf(c181,plain,
( ~ ssPv4(skf1(X427))
| ~ ssPv1(skf1(X427))
| ssPv2(skf1(X427))
| ssPv1(X427) ),
inference(resolution,[status(thm)],[c179,clause1]) ).
cnf(c180,plain,
( ~ ssRr(X421,X422)
| ~ ssPv4(X422)
| ~ ssPv1(skf1(X421))
| ssPv2(X422)
| ssPv1(X421) ),
inference(resolution,[status(thm)],[c154,clause1]) ).
cnf(c130,plain,
( ~ ssRr(X355,X353)
| ~ ssPv2(X353)
| ~ ssRr(X355,X354)
| ~ ssPv2(X355)
| ssPv3(X354)
| ssPv2(X354) ),
inference(factor,[status(thm)],[clause43]) ).
cnf(c152,plain,
( ~ ssRr(X413,X414)
| ~ ssPv2(X414)
| ~ ssPv2(X413)
| ssPv3(skf1(X413))
| ssPv2(skf1(X413)) ),
inference(resolution,[status(thm)],[c130,clause1]) ).
cnf(c148,plain,
( ~ ssRr(X393,X394)
| ~ ssPv4(X394)
| ~ ssRr(X393,X392)
| ~ ssPv3(X392)
| ssPv2(X394)
| ssPv1(X393) ),
inference(factor,[status(thm)],[clause46]) ).
cnf(c167,plain,
( ~ ssRr(X400,X399)
| ~ ssPv4(X399)
| ~ ssPv3(X399)
| ssPv2(X399)
| ssPv1(X400) ),
inference(factor,[status(thm)],[c148]) ).
cnf(c172,plain,
( ~ ssPv4(skf1(X403))
| ~ ssPv3(skf1(X403))
| ssPv2(skf1(X403))
| ssPv1(X403) ),
inference(resolution,[status(thm)],[c167,clause1]) ).
cnf(c168,plain,
( ~ ssRr(X401,X402)
| ~ ssPv4(X402)
| ~ ssPv3(skf1(X401))
| ssPv2(X402)
| ssPv1(X401) ),
inference(resolution,[status(thm)],[c148,clause1]) ).
cnf(c123,plain,
( ~ ssRr(X338,X340)
| ~ ssPv2(X340)
| ~ ssRr(X338,X339)
| ~ ssPv1(X339)
| ssPv3(X339)
| ssPv3(X338) ),
inference(factor,[status(thm)],[clause42]) ).
cnf(c146,plain,
( ~ ssRr(X391,X390)
| ~ ssPv2(X390)
| ~ ssPv1(skf1(X391))
| ssPv3(skf1(X391))
| ssPv3(X391) ),
inference(resolution,[status(thm)],[c123,clause1]) ).
cnf(c142,plain,
( ~ ssRr(X373,X375)
| ~ ssPv4(X375)
| ~ ssRr(X373,X374)
| ~ ssPv1(X374)
| ssPv3(X375)
| ssPv1(X373) ),
inference(factor,[status(thm)],[clause45]) ).
cnf(c159,plain,
( ~ ssRr(X376,X377)
| ~ ssPv4(X377)
| ~ ssPv1(X377)
| ssPv3(X377)
| ssPv1(X376) ),
inference(factor,[status(thm)],[c142]) ).
cnf(c161,plain,
( ~ ssPv4(skf1(X384))
| ~ ssPv1(skf1(X384))
| ssPv3(skf1(X384))
| ssPv1(X384) ),
inference(resolution,[status(thm)],[c159,clause1]) ).
cnf(c160,plain,
( ~ ssRr(X378,X379)
| ~ ssPv4(X379)
| ~ ssPv1(skf1(X378))
| ssPv3(X379)
| ssPv1(X378) ),
inference(resolution,[status(thm)],[c142,clause1]) ).
cnf(c115,plain,
( ~ ssRr(X314,X316)
| ~ ssPv3(X316)
| ~ ssRr(X314,X315)
| ssPv3(X315)
| ssPv2(X315)
| ssPv1(X314) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c134,plain,
( ~ ssRr(X359,X358)
| ~ ssPv3(X358)
| ssPv3(skf1(X359))
| ssPv2(skf1(X359))
| ssPv1(X359) ),
inference(resolution,[status(thm)],[c115,clause1]) ).
cnf(c108,plain,
( ~ ssRr(X299,X298)
| ~ ssPv2(X298)
| ~ ssRr(X299,X297)
| ssPv2(X297)
| ssPv1(X297)
| ssPv3(X299) ),
inference(factor,[status(thm)],[clause40]) ).
cnf(c126,plain,
( ~ ssRr(X343,X344)
| ~ ssPv2(X344)
| ssPv2(skf1(X343))
| ssPv1(skf1(X343))
| ssPv3(X343) ),
inference(resolution,[status(thm)],[c108,clause1]) ).
cnf(c122,plain,
( ~ ssRr(X326,X327)
| ~ ssPv2(X327)
| ~ ssRr(X326,X328)
| ~ ssPv1(X328)
| ssPv3(X327)
| ssPv3(X326) ),
inference(factor,[status(thm)],[clause42]) ).
cnf(c139,plain,
( ~ ssRr(X330,X329)
| ~ ssPv2(X329)
| ~ ssPv1(X329)
| ssPv3(X329)
| ssPv3(X330) ),
inference(factor,[status(thm)],[c122]) ).
cnf(c141,plain,
( ~ ssPv2(skf1(X333))
| ~ ssPv1(skf1(X333))
| ssPv3(skf1(X333))
| ssPv3(X333) ),
inference(resolution,[status(thm)],[c139,clause1]) ).
cnf(c140,plain,
( ~ ssRr(X331,X332)
| ~ ssPv2(X332)
| ~ ssPv1(skf1(X331))
| ssPv3(X332)
| ssPv3(X331) ),
inference(resolution,[status(thm)],[c122,clause1]) ).
cnf(c105,plain,
( ~ ssRr(X282,X281)
| ~ ssPv2(X281)
| ~ ssRr(X282,X280)
| ssPv3(X280)
| ssPv1(X280)
| ssPv4(X282) ),
inference(factor,[status(thm)],[clause39]) ).
cnf(c118,plain,
( ~ ssRr(X319,X320)
| ~ ssPv2(X320)
| ssPv3(skf1(X319))
| ssPv1(skf1(X319))
| ssPv4(X319) ),
inference(resolution,[status(thm)],[c105,clause1]) ).
cnf(c114,plain,
( ~ ssRr(X302,X303)
| ~ ssPv3(X303)
| ~ ssRr(X302,X304)
| ssPv3(X304)
| ssPv2(X303)
| ssPv1(X302) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c128,plain,
( ~ ssRr(X311,X312)
| ~ ssPv3(X312)
| ssPv3(skf1(X311))
| ssPv2(X312)
| ssPv1(X311) ),
inference(resolution,[status(thm)],[c114,clause1]) ).
cnf(c107,plain,
( ~ ssRr(X287,X286)
| ~ ssPv2(X286)
| ~ ssRr(X287,X285)
| ssPv2(X285)
| ssPv1(X286)
| ssPv3(X287) ),
inference(factor,[status(thm)],[clause40]) ).
cnf(c120,plain,
( ~ ssRr(X290,X291)
| ~ ssPv2(X291)
| ssPv2(skf1(X290))
| ssPv1(X291)
| ssPv3(X290) ),
inference(resolution,[status(thm)],[c107,clause1]) ).
cnf(c104,plain,
( ~ ssRr(X269,X268)
| ~ ssPv2(X268)
| ~ ssRr(X269,X267)
| ssPv3(X267)
| ssPv1(X268)
| ssPv4(X269) ),
inference(factor,[status(thm)],[clause39]) ).
cnf(c110,plain,
( ~ ssRr(X271,X270)
| ~ ssPv2(X270)
| ssPv3(X270)
| ssPv1(X270)
| ssPv4(X271) ),
inference(factor,[status(thm)],[c104]) ).
cnf(c112,plain,
( ~ ssPv2(skf1(X274))
| ssPv3(skf1(X274))
| ssPv1(skf1(X274))
| ssPv4(X274) ),
inference(resolution,[status(thm)],[c110,clause1]) ).
cnf(c111,plain,
( ~ ssRr(X273,X272)
| ~ ssPv2(X272)
| ssPv3(skf1(X273))
| ssPv1(X272)
| ssPv4(X273) ),
inference(resolution,[status(thm)],[c104,clause1]) ).
cnf(clause38,negated_conjecture,
( ~ ssRr(X251,X249)
| ~ ssPv4(X249)
| ~ ssRr(X251,X250)
| ~ ssPv1(X250)
| ~ ssPv1(X251)
| ~ ssPv2(X251) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c102,plain,
( ~ ssRr(X257,X258)
| ~ ssPv4(X258)
| ~ ssPv1(skf1(X257))
| ~ ssPv1(X257)
| ~ ssPv2(X257) ),
inference(resolution,[status(thm)],[clause38,clause1]) ).
cnf(clause37,negated_conjecture,
( ~ ssRr(X240,X238)
| ~ ssPv4(X238)
| ~ ssRr(X240,X239)
| ~ ssPv1(X239)
| ~ ssPv1(X240)
| ~ ssPv3(X240) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c98,plain,
( ~ ssRr(X255,X256)
| ~ ssPv4(X256)
| ~ ssPv1(skf1(X255))
| ~ ssPv1(X255)
| ~ ssPv3(X255) ),
inference(resolution,[status(thm)],[clause37,clause1]) ).
cnf(c101,plain,
( ~ ssRr(X252,X253)
| ~ ssPv4(X253)
| ~ ssPv1(X253)
| ~ ssPv1(X252)
| ~ ssPv2(X252) ),
inference(factor,[status(thm)],[clause38]) ).
cnf(c103,plain,
( ~ ssPv4(skf1(X254))
| ~ ssPv1(skf1(X254))
| ~ ssPv1(X254)
| ~ ssPv2(X254) ),
inference(resolution,[status(thm)],[c101,clause1]) ).
cnf(clause36,negated_conjecture,
( ~ ssRr(X237,X235)
| ~ ssPv4(X235)
| ~ ssRr(X237,X236)
| ~ ssPv3(X236)
| ~ ssPv3(X237)
| ~ ssPv4(X237) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c96,plain,
( ~ ssRr(X247,X248)
| ~ ssPv4(X248)
| ~ ssPv3(skf1(X247))
| ~ ssPv3(X247)
| ~ ssPv4(X247) ),
inference(resolution,[status(thm)],[clause36,clause1]) ).
cnf(c97,plain,
( ~ ssRr(X244,X243)
| ~ ssPv4(X243)
| ~ ssPv1(X243)
| ~ ssPv1(X244)
| ~ ssPv3(X244) ),
inference(factor,[status(thm)],[clause37]) ).
cnf(c100,plain,
( ~ ssPv4(skf1(X246))
| ~ ssPv1(skf1(X246))
| ~ ssPv1(X246)
| ~ ssPv3(X246) ),
inference(resolution,[status(thm)],[c97,clause1]) ).
cnf(c95,plain,
( ~ ssRr(X241,X242)
| ~ ssPv4(X242)
| ~ ssPv3(X242)
| ~ ssPv3(X241)
| ~ ssPv4(X241) ),
inference(factor,[status(thm)],[clause36]) ).
cnf(c99,plain,
( ~ ssPv4(skf1(X245))
| ~ ssPv3(skf1(X245))
| ~ ssPv3(X245)
| ~ ssPv4(X245) ),
inference(resolution,[status(thm)],[c95,clause1]) ).
cnf(clause35,negated_conjecture,
( ~ ssRr(X227,X225)
| ~ ssPv4(X225)
| ~ ssRr(X227,X226)
| ~ ssPv3(X226)
| ~ ssPv3(X227)
| ssPv1(X227) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c93,plain,
( ~ ssRr(X233,X234)
| ~ ssPv4(X234)
| ~ ssPv3(skf1(X233))
| ~ ssPv3(X233)
| ssPv1(X233) ),
inference(resolution,[status(thm)],[clause35,clause1]) ).
cnf(clause34,negated_conjecture,
( ~ ssRr(X216,X214)
| ~ ssPv3(X214)
| ~ ssRr(X216,X215)
| ~ ssPv2(X215)
| ~ ssPv3(X216)
| ssPv2(X216) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c89,plain,
( ~ ssRr(X231,X232)
| ~ ssPv3(X232)
| ~ ssPv2(skf1(X231))
| ~ ssPv3(X231)
| ssPv2(X231) ),
inference(resolution,[status(thm)],[clause34,clause1]) ).
cnf(c92,plain,
( ~ ssRr(X228,X229)
| ~ ssPv4(X229)
| ~ ssPv3(X229)
| ~ ssPv3(X228)
| ssPv1(X228) ),
inference(factor,[status(thm)],[clause35]) ).
cnf(c94,plain,
( ~ ssPv4(skf1(X230))
| ~ ssPv3(skf1(X230))
| ~ ssPv3(X230)
| ssPv1(X230) ),
inference(resolution,[status(thm)],[c92,clause1]) ).
cnf(clause33,negated_conjecture,
( ~ ssRr(X213,X211)
| ~ ssPv2(X211)
| ~ ssRr(X213,X212)
| ~ ssPv1(X212)
| ~ ssPv4(X213)
| ssPv3(X213) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c87,plain,
( ~ ssRr(X223,X224)
| ~ ssPv2(X224)
| ~ ssPv1(skf1(X223))
| ~ ssPv4(X223)
| ssPv3(X223) ),
inference(resolution,[status(thm)],[clause33,clause1]) ).
cnf(c88,plain,
( ~ ssRr(X220,X219)
| ~ ssPv3(X219)
| ~ ssPv2(X219)
| ~ ssPv3(X220)
| ssPv2(X220) ),
inference(factor,[status(thm)],[clause34]) ).
cnf(c91,plain,
( ~ ssPv3(skf1(X222))
| ~ ssPv2(skf1(X222))
| ~ ssPv3(X222)
| ssPv2(X222) ),
inference(resolution,[status(thm)],[c88,clause1]) ).
cnf(c86,plain,
( ~ ssRr(X218,X217)
| ~ ssPv2(X217)
| ~ ssPv1(X217)
| ~ ssPv4(X218)
| ssPv3(X218) ),
inference(factor,[status(thm)],[clause33]) ).
cnf(c90,plain,
( ~ ssPv2(skf1(X221))
| ~ ssPv1(skf1(X221))
| ~ ssPv4(X221)
| ssPv3(X221) ),
inference(resolution,[status(thm)],[c86,clause1]) ).
cnf(clause32,negated_conjecture,
( ~ ssRr(X204,X202)
| ~ ssPv3(X202)
| ~ ssRr(X204,X203)
| ~ ssPv2(X204)
| ~ ssPv3(X204)
| ssPv3(X203) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c84,plain,
( ~ ssRr(X208,X209)
| ~ ssPv3(X209)
| ~ ssPv2(X208)
| ~ ssPv3(X208)
| ssPv3(skf1(X208)) ),
inference(resolution,[status(thm)],[clause32,clause1]) ).
cnf(clause31,negated_conjecture,
( ~ ssRr(X193,X191)
| ~ ssPv4(X191)
| ~ ssRr(X193,X192)
| ~ ssPv3(X193)
| ~ ssPv4(X193)
| ssPv3(X192) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c79,plain,
( ~ ssRr(X200,X201)
| ~ ssPv4(X201)
| ~ ssPv3(X200)
| ~ ssPv4(X200)
| ssPv3(skf1(X200)) ),
inference(resolution,[status(thm)],[clause31,clause1]) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X182,X180)
| ~ ssPv2(X180)
| ~ ssRr(X182,X181)
| ~ ssPv3(X182)
| ~ ssPv4(X182)
| ssPv4(X181) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c75,plain,
( ~ ssRr(X198,X197)
| ~ ssPv2(X197)
| ~ ssPv3(X198)
| ~ ssPv4(X198)
| ssPv4(skf1(X198)) ),
inference(resolution,[status(thm)],[clause30,clause1]) ).
cnf(c78,plain,
( ~ ssRr(X195,X194)
| ~ ssPv4(X194)
| ~ ssPv3(X195)
| ~ ssPv4(X195)
| ssPv3(X194) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c80,plain,
( ~ ssPv4(skf1(X196))
| ~ ssPv3(X196)
| ~ ssPv4(X196)
| ssPv3(skf1(X196)) ),
inference(resolution,[status(thm)],[c78,clause1]) ).
cnf(clause29,negated_conjecture,
( ~ ssRr(X179,X177)
| ~ ssPv4(X177)
| ~ ssRr(X179,X178)
| ~ ssPv2(X178)
| ssPv1(X179)
| ssPv2(X179) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c73,plain,
( ~ ssRr(X189,X190)
| ~ ssPv4(X190)
| ~ ssPv2(skf1(X189))
| ssPv1(X189)
| ssPv2(X189) ),
inference(resolution,[status(thm)],[clause29,clause1]) ).
cnf(c74,plain,
( ~ ssRr(X185,X186)
| ~ ssPv2(X186)
| ~ ssPv3(X185)
| ~ ssPv4(X185)
| ssPv4(X186) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c77,plain,
( ~ ssPv2(skf1(X188))
| ~ ssPv3(X188)
| ~ ssPv4(X188)
| ssPv4(skf1(X188)) ),
inference(resolution,[status(thm)],[c74,clause1]) ).
cnf(c72,plain,
( ~ ssRr(X184,X183)
| ~ ssPv4(X183)
| ~ ssPv2(X183)
| ssPv1(X184)
| ssPv2(X184) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c76,plain,
( ~ ssPv4(skf1(X187))
| ~ ssPv2(skf1(X187))
| ssPv1(X187)
| ssPv2(X187) ),
inference(resolution,[status(thm)],[c72,clause1]) ).
cnf(clause28,negated_conjecture,
( ~ ssRr(X170,X168)
| ~ ssPv3(X168)
| ~ ssRr(X170,X169)
| ~ ssPv1(X170)
| ssPv3(X169)
| ssPv2(X170) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c70,plain,
( ~ ssRr(X174,X175)
| ~ ssPv3(X175)
| ~ ssPv1(X174)
| ssPv3(skf1(X174))
| ssPv2(X174) ),
inference(resolution,[status(thm)],[clause28,clause1]) ).
cnf(clause27,negated_conjecture,
( ~ ssRr(X159,X157)
| ~ ssPv2(X157)
| ~ ssRr(X159,X158)
| ~ ssPv3(X159)
| ssPv2(X158)
| ssPv2(X159) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c66,plain,
( ~ ssRr(X166,X167)
| ~ ssPv2(X167)
| ~ ssPv3(X166)
| ssPv2(skf1(X166))
| ssPv2(X166) ),
inference(resolution,[status(thm)],[clause27,clause1]) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X148,X146)
| ~ ssPv4(X146)
| ~ ssRr(X148,X147)
| ~ ssPv4(X148)
| ssPv3(X147)
| ssPv2(X148) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c61,plain,
( ~ ssRr(X163,X164)
| ~ ssPv4(X164)
| ~ ssPv4(X163)
| ssPv3(skf1(X163))
| ssPv2(X163) ),
inference(resolution,[status(thm)],[clause26,clause1]) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X145,X143)
| ~ ssPv4(X143)
| ~ ssRr(X145,X144)
| ~ ssPv1(X145)
| ssPv2(X144)
| ssPv3(X145) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c59,plain,
( ~ ssRr(X155,X156)
| ~ ssPv4(X156)
| ~ ssPv1(X155)
| ssPv2(skf1(X155))
| ssPv3(X155) ),
inference(resolution,[status(thm)],[clause25,clause1]) ).
cnf(c60,plain,
( ~ ssRr(X151,X152)
| ~ ssPv4(X152)
| ~ ssPv4(X151)
| ssPv3(X152)
| ssPv2(X151) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c63,plain,
( ~ ssPv4(skf1(X154))
| ~ ssPv4(X154)
| ssPv3(skf1(X154))
| ssPv2(X154) ),
inference(resolution,[status(thm)],[c60,clause1]) ).
cnf(c58,plain,
( ~ ssRr(X150,X149)
| ~ ssPv4(X149)
| ~ ssPv1(X150)
| ssPv2(X149)
| ssPv3(X150) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c62,plain,
( ~ ssPv4(skf1(X153))
| ~ ssPv1(X153)
| ssPv2(skf1(X153))
| ssPv3(X153) ),
inference(resolution,[status(thm)],[c58,clause1]) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X136,X134)
| ~ ssPv2(X134)
| ~ ssRr(X136,X135)
| ~ ssPv2(X136)
| ssPv2(X135)
| ssPv3(X136) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c56,plain,
( ~ ssRr(X140,X141)
| ~ ssPv2(X141)
| ~ ssPv2(X140)
| ssPv2(skf1(X140))
| ssPv3(X140) ),
inference(resolution,[status(thm)],[clause24,clause1]) ).
cnf(clause23,negated_conjecture,
( ~ ssRr(X125,X123)
| ~ ssPv3(X123)
| ~ ssRr(X125,X124)
| ~ ssPv2(X125)
| ssPv2(X124)
| ssPv3(X125) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c51,plain,
( ~ ssRr(X132,X133)
| ~ ssPv3(X133)
| ~ ssPv2(X132)
| ssPv2(skf1(X132))
| ssPv3(X132) ),
inference(resolution,[status(thm)],[clause23,clause1]) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X115,X113)
| ~ ssPv4(X113)
| ~ ssRr(X115,X114)
| ~ ssPv4(X115)
| ssPv1(X114)
| ssPv3(X115) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c47,plain,
( ~ ssRr(X129,X130)
| ~ ssPv4(X130)
| ~ ssPv4(X129)
| ssPv1(skf1(X129))
| ssPv3(X129) ),
inference(resolution,[status(thm)],[clause22,clause1]) ).
cnf(c50,plain,
( ~ ssRr(X126,X127)
| ~ ssPv3(X127)
| ~ ssPv2(X126)
| ssPv2(X127)
| ssPv3(X126) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c52,plain,
( ~ ssPv3(skf1(X128))
| ~ ssPv2(X128)
| ssPv2(skf1(X128))
| ssPv3(X128) ),
inference(resolution,[status(thm)],[c50,clause1]) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X104,X102)
| ~ ssPv3(X102)
| ~ ssRr(X104,X103)
| ~ ssPv3(X104)
| ssPv2(X103)
| ssPv4(X104) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c42,plain,
( ~ ssRr(X120,X121)
| ~ ssPv3(X121)
| ~ ssPv3(X120)
| ssPv2(skf1(X120))
| ssPv4(X120) ),
inference(resolution,[status(thm)],[clause21,clause1]) ).
cnf(c46,plain,
( ~ ssRr(X118,X117)
| ~ ssPv4(X117)
| ~ ssPv4(X118)
| ssPv1(X117)
| ssPv3(X118) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c48,plain,
( ~ ssPv4(skf1(X119))
| ~ ssPv4(X119)
| ssPv1(skf1(X119))
| ssPv3(X119) ),
inference(resolution,[status(thm)],[c46,clause1]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X101,X99)
| ~ ssRr(X101,X100)
| ~ ssPv1(X101)
| ~ ssPv3(X101)
| ssPv4(X99)
| ssPv3(X100) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c40,plain,
( ~ ssRr(X111,X112)
| ~ ssPv1(X111)
| ~ ssPv3(X111)
| ssPv4(X112)
| ssPv3(skf1(X111)) ),
inference(resolution,[status(thm)],[clause20,clause1]) ).
cnf(c41,plain,
( ~ ssRr(X108,X107)
| ~ ssPv3(X107)
| ~ ssPv3(X108)
| ssPv2(X107)
| ssPv4(X108) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c44,plain,
( ~ ssPv3(skf1(X110))
| ~ ssPv3(X110)
| ssPv2(skf1(X110))
| ssPv4(X110) ),
inference(resolution,[status(thm)],[c41,clause1]) ).
cnf(c39,plain,
( ~ ssRr(X105,X106)
| ~ ssPv1(X105)
| ~ ssPv3(X105)
| ssPv4(X106)
| ssPv3(X106) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c43,plain,
( ~ ssPv1(X109)
| ~ ssPv3(X109)
| ssPv4(skf1(X109))
| ssPv3(skf1(X109)) ),
inference(resolution,[status(thm)],[c39,clause1]) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X92,X90)
| ~ ssRr(X92,X91)
| ~ ssPv1(X92)
| ~ ssPv4(X92)
| ssPv3(X90)
| ssPv1(X91) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c36,plain,
( ~ ssRr(X96,X97)
| ~ ssPv1(X96)
| ~ ssPv4(X96)
| ssPv3(X97)
| ssPv1(skf1(X96)) ),
inference(resolution,[status(thm)],[clause19,clause1]) ).
cnf(c35,plain,
( ~ ssRr(X94,X93)
| ~ ssPv1(X94)
| ~ ssPv4(X94)
| ssPv3(X93)
| ssPv1(X93) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c37,plain,
( ~ ssPv1(X95)
| ~ ssPv4(X95)
| ssPv3(skf1(X95))
| ssPv1(skf1(X95)) ),
inference(resolution,[status(thm)],[c35,clause1]) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X82,X80)
| ~ ssRr(X82,X81)
| ~ ssPv2(X82)
| ~ ssPv4(X82)
| ssPv4(X80)
| ssPv1(X81) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c32,plain,
( ~ ssRr(X87,X88)
| ~ ssPv2(X87)
| ~ ssPv4(X87)
| ssPv4(X88)
| ssPv1(skf1(X87)) ),
inference(resolution,[status(thm)],[clause18,clause1]) ).
cnf(c31,plain,
( ~ ssRr(X85,X84)
| ~ ssPv2(X85)
| ~ ssPv4(X85)
| ssPv4(X84)
| ssPv1(X84) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c33,plain,
( ~ ssPv2(X86)
| ~ ssPv4(X86)
| ssPv4(skf1(X86))
| ssPv1(skf1(X86)) ),
inference(resolution,[status(thm)],[c31,clause1]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X71,X69)
| ~ ssRr(X71,X70)
| ~ ssPv3(X71)
| ~ ssPv4(X71)
| ssPv4(X69)
| ssPv1(X70) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c27,plain,
( ~ ssRr(X78,X79)
| ~ ssPv3(X78)
| ~ ssPv4(X78)
| ssPv4(X79)
| ssPv1(skf1(X78)) ),
inference(resolution,[status(thm)],[clause17,clause1]) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X61,X59)
| ~ ssPv2(X59)
| ~ ssRr(X61,X60)
| ssPv1(X60)
| ssPv1(X61)
| ssPv3(X61) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c23,plain,
( ~ ssRr(X75,X76)
| ~ ssPv2(X76)
| ssPv1(skf1(X75))
| ssPv1(X75)
| ssPv3(X75) ),
inference(resolution,[status(thm)],[clause16,clause1]) ).
cnf(c26,plain,
( ~ ssRr(X73,X72)
| ~ ssPv3(X73)
| ~ ssPv4(X73)
| ssPv4(X72)
| ssPv1(X72) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c28,plain,
( ~ ssPv3(X74)
| ~ ssPv4(X74)
| ssPv4(skf1(X74))
| ssPv1(skf1(X74)) ),
inference(resolution,[status(thm)],[c26,clause1]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X50,X48)
| ~ ssRr(X50,X49)
| ~ ssPv3(X50)
| ssPv4(X48)
| ssPv1(X49)
| ssPv1(X50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c18,plain,
( ~ ssRr(X66,X67)
| ~ ssPv3(X66)
| ssPv4(X67)
| ssPv1(skf1(X66))
| ssPv1(X66) ),
inference(resolution,[status(thm)],[clause15,clause1]) ).
cnf(c22,plain,
( ~ ssRr(X64,X63)
| ~ ssPv2(X63)
| ssPv1(X63)
| ssPv1(X64)
| ssPv3(X64) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c24,plain,
( ~ ssPv2(skf1(X65))
| ssPv1(skf1(X65))
| ssPv1(X65)
| ssPv3(X65) ),
inference(resolution,[status(thm)],[c22,clause1]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X47,X45)
| ~ ssRr(X47,X46)
| ~ ssPv1(X47)
| ssPv3(X45)
| ssPv1(X46)
| ssPv3(X47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c16,plain,
( ~ ssRr(X57,X58)
| ~ ssPv1(X57)
| ssPv3(X58)
| ssPv1(skf1(X57))
| ssPv3(X57) ),
inference(resolution,[status(thm)],[clause14,clause1]) ).
cnf(c17,plain,
( ~ ssRr(X54,X53)
| ~ ssPv3(X54)
| ssPv4(X53)
| ssPv1(X53)
| ssPv1(X54) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c20,plain,
( ~ ssPv3(X56)
| ssPv4(skf1(X56))
| ssPv1(skf1(X56))
| ssPv1(X56) ),
inference(resolution,[status(thm)],[c17,clause1]) ).
cnf(c15,plain,
( ~ ssRr(X51,X52)
| ~ ssPv1(X51)
| ssPv3(X52)
| ssPv1(X52)
| ssPv3(X51) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c19,plain,
( ~ ssPv1(X55)
| ssPv3(skf1(X55))
| ssPv1(skf1(X55))
| ssPv3(X55) ),
inference(resolution,[status(thm)],[c15,clause1]) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X38,X36)
| ~ ssRr(X38,X37)
| ~ ssPv2(X38)
| ssPv4(X36)
| ssPv2(X37)
| ssPv3(X38) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c12,plain,
( ~ ssRr(X42,X43)
| ~ ssPv2(X42)
| ssPv4(X43)
| ssPv2(skf1(X42))
| ssPv3(X42) ),
inference(resolution,[status(thm)],[clause13,clause1]) ).
cnf(c11,plain,
( ~ ssRr(X39,X40)
| ~ ssPv2(X39)
| ssPv4(X40)
| ssPv2(X40)
| ssPv3(X39) ),
inference(factor,[status(thm)],[clause13]) ).
cnf(c13,plain,
( ~ ssPv2(X41)
| ssPv4(skf1(X41))
| ssPv2(skf1(X41))
| ssPv3(X41) ),
inference(resolution,[status(thm)],[c11,clause1]) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X34,X33)
| ~ ssPv1(X33)
| ~ ssPv2(X34)
| ~ ssPv3(X34)
| ~ ssPv4(X34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c10,plain,
( ~ ssPv1(skf1(X35))
| ~ ssPv2(X35)
| ~ ssPv3(X35)
| ~ ssPv4(X35) ),
inference(resolution,[status(thm)],[clause12,clause1]) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X31,X30)
| ~ ssPv2(X30)
| ~ ssPv2(X31)
| ~ ssPv3(X31)
| ssPv1(X31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c9,plain,
( ~ ssPv2(skf1(X32))
| ~ ssPv2(X32)
| ~ ssPv3(X32)
| ssPv1(X32) ),
inference(resolution,[status(thm)],[clause11,clause1]) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X28,X27)
| ~ ssPv2(X27)
| ~ ssPv2(X28)
| ~ ssPv4(X28)
| ssPv1(X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c8,plain,
( ~ ssPv2(skf1(X29))
| ~ ssPv2(X29)
| ~ ssPv4(X29)
| ssPv1(X29) ),
inference(resolution,[status(thm)],[clause10,clause1]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X25,X24)
| ~ ssPv4(X24)
| ~ ssPv1(X25)
| ~ ssPv4(X25)
| ssPv3(X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c7,plain,
( ~ ssPv4(skf1(X26))
| ~ ssPv1(X26)
| ~ ssPv4(X26)
| ssPv3(X26) ),
inference(resolution,[status(thm)],[clause9,clause1]) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X22,X21)
| ~ ssPv1(X22)
| ~ ssPv2(X22)
| ~ ssPv4(X22)
| ssPv4(X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c6,plain,
( ~ ssPv1(X23)
| ~ ssPv2(X23)
| ~ ssPv4(X23)
| ssPv4(skf1(X23)) ),
inference(resolution,[status(thm)],[clause8,clause1]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X19,X18)
| ~ ssPv2(X19)
| ~ ssPv3(X19)
| ssPv2(X18)
| ssPv1(X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c5,plain,
( ~ ssPv2(X20)
| ~ ssPv3(X20)
| ssPv2(skf1(X20))
| ssPv1(X20) ),
inference(resolution,[status(thm)],[clause7,clause1]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X16,X15)
| ~ ssPv2(X15)
| ~ ssPv1(X16)
| ssPv2(X16)
| ssPv3(X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c4,plain,
( ~ ssPv2(skf1(X17))
| ~ ssPv1(X17)
| ssPv2(X17)
| ssPv3(X17) ),
inference(resolution,[status(thm)],[clause6,clause1]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X13,X12)
| ~ ssPv1(X13)
| ~ ssPv2(X13)
| ssPv2(X12)
| ssPv3(X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c3,plain,
( ~ ssPv1(X14)
| ~ ssPv2(X14)
| ssPv2(skf1(X14))
| ssPv3(X14) ),
inference(resolution,[status(thm)],[clause5,clause1]) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X10,X9)
| ~ ssPv1(X9)
| ssPv1(X10)
| ssPv2(X10)
| ssPv3(X10) ),
file('/export/starexec/sandbox/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(X7,X6)
| ~ ssPv2(X7)
| ssPv1(X6)
| ssPv1(X7)
| ssPv4(X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c1,plain,
( ~ ssPv2(X8)
| ssPv1(skf1(X8))
| ssPv1(X8)
| ssPv4(X8) ),
inference(resolution,[status(thm)],[clause3,clause1]) ).
cnf(clause2,negated_conjecture,
( ~ ssRr(X4,X3)
| ~ ssPv4(X4)
| ssPv3(X3)
| ssPv2(X4)
| ssPv3(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(c0,plain,
( ~ ssPv4(X5)
| ssPv3(skf1(X5))
| ssPv2(X5)
| ssPv3(X5) ),
inference(resolution,[status(thm)],[clause2,clause1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYN756-1 : TPTP v8.1.2. Released v2.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n004.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 20:13:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.70/0.89 % Version: 1.5
% 0.70/0.89 % SZS status Satisfiable
% 0.70/0.89 % SZS output start Saturation
% See solution above
% 0.70/0.90
% 0.70/0.90 % Initial clauses : 51
% 0.70/0.90 % Processed clauses : 221
% 0.70/0.90 % Factors computed : 88
% 0.70/0.90 % Resolvents computed: 155
% 0.70/0.90 % Tautologies deleted: 25
% 0.70/0.90 % Forward subsumed : 48
% 0.70/0.90 % Backward subsumed : 0
% 0.70/0.90 % -------- CPU Time ---------
% 0.70/0.90 % User time : 0.528 s
% 0.70/0.90 % System time : 0.016 s
% 0.70/0.90 % Total time : 0.544 s
%------------------------------------------------------------------------------