%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN785-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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:01 EDT 2024
% Result : Satisfiable 0.81s 0.98s
% Output : Saturation 0.84s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause2,negated_conjecture,
ssRr(X3,skf2(X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause1,negated_conjecture,
ssRr(skf3(X2),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause42,negated_conjecture,
( ~ ssRr(X326,X329)
| ~ ssPv4(X329)
| ~ ssRr(X326,X328)
| ~ ssPv3(X328)
| ~ ssRr(X326,X327)
| ~ ssPv1(X327)
| ~ ssPv2(X326) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c202,plain,
( ~ ssRr(skf3(X612),X610)
| ~ ssPv4(X610)
| ~ ssRr(skf3(X612),X611)
| ~ ssPv3(X611)
| ~ ssPv1(X612)
| ~ ssPv2(skf3(X612)) ),
inference(resolution,[status(thm)],[clause42,clause1]) ).
cnf(c334,plain,
( ~ ssRr(skf3(X685),X684)
| ~ ssPv4(X684)
| ~ ssPv3(skf2(skf3(X685)))
| ~ ssPv1(X685)
| ~ ssPv2(skf3(X685)) ),
inference(resolution,[status(thm)],[c202,clause2]) ).
cnf(clause39,negated_conjecture,
( ~ ssRr(X289,X292)
| ~ ssPv2(X289)
| ~ ssRr(X292,X291)
| ~ ssPv3(X291)
| ~ ssRr(X292,X290)
| ~ ssPv1(X292)
| ssPv2(X290) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c180,plain,
( ~ ssRr(X580,skf3(X579))
| ~ ssPv2(X580)
| ~ ssRr(skf3(X579),X578)
| ~ ssPv3(X578)
| ~ ssPv1(skf3(X579))
| ssPv2(X579) ),
inference(resolution,[status(thm)],[clause39,clause1]) ).
cnf(c322,plain,
( ~ ssRr(skf3(X682),skf3(X682))
| ~ ssPv2(skf3(X682))
| ~ ssPv3(skf3(X682))
| ~ ssPv1(skf3(X682))
| ssPv2(X682) ),
inference(factor,[status(thm)],[c180]) ).
cnf(clause41,negated_conjecture,
( ~ ssRr(X315,X318)
| ~ ssPv2(X315)
| ~ ssRr(X317,X318)
| ~ ssRr(X318,X316)
| ~ ssPv2(X316)
| ~ ssPv2(X318)
| ssPv2(X317) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c195,plain,
( ~ ssRr(X603,skf3(X602))
| ~ ssPv2(X603)
| ~ ssRr(X601,skf3(X602))
| ~ ssPv2(X602)
| ~ ssPv2(skf3(X602))
| ssPv2(X601) ),
inference(resolution,[status(thm)],[clause41,clause1]) ).
cnf(c331,plain,
( ~ ssRr(X680,skf3(X681))
| ~ ssPv2(X680)
| ~ ssPv2(X681)
| ~ ssPv2(skf3(X681))
| ssPv2(skf3(skf3(X681))) ),
inference(resolution,[status(thm)],[c195,clause1]) ).
cnf(clause40,negated_conjecture,
( ~ ssRr(X302,X305)
| ~ ssPv4(X302)
| ~ ssRr(X304,X305)
| ~ ssPv1(X304)
| ~ ssRr(X305,X303)
| ~ ssPv4(X303)
| ssPv2(X305) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c185,plain,
( ~ ssRr(X594,skf3(X593))
| ~ ssPv4(X594)
| ~ ssRr(X592,skf3(X593))
| ~ ssPv1(X592)
| ~ ssPv4(X593)
| ssPv2(skf3(X593)) ),
inference(resolution,[status(thm)],[clause40,clause1]) ).
cnf(c328,plain,
( ~ ssRr(X679,skf3(X678))
| ~ ssPv4(X679)
| ~ ssPv1(skf3(skf3(X678)))
| ~ ssPv4(X678)
| ssPv2(skf3(X678)) ),
inference(resolution,[status(thm)],[c185,clause1]) ).
cnf(c324,plain,
( ~ ssRr(X677,skf3(X676))
| ~ ssPv2(X677)
| ~ ssPv3(skf2(skf3(X676)))
| ~ ssPv1(skf3(X676))
| ssPv2(X676) ),
inference(resolution,[status(thm)],[c180,clause2]) ).
cnf(clause38,negated_conjecture,
( ~ ssRr(X276,X279)
| ~ ssPv4(X279)
| ~ ssRr(X276,X278)
| ~ ssPv1(X278)
| ~ ssRr(X276,X277)
| ~ ssPv1(X276)
| ssPv1(X277) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c172,plain,
( ~ ssRr(skf3(X569),X567)
| ~ ssPv4(X567)
| ~ ssRr(skf3(X569),X568)
| ~ ssPv1(X568)
| ~ ssPv1(skf3(X569))
| ssPv1(X569) ),
inference(resolution,[status(thm)],[clause38,clause1]) ).
cnf(c318,plain,
( ~ ssRr(skf3(X675),X674)
| ~ ssPv4(X674)
| ~ ssPv1(skf2(skf3(X675)))
| ~ ssPv1(skf3(X675))
| ssPv1(X675) ),
inference(resolution,[status(thm)],[c172,clause2]) ).
cnf(c181,plain,
( ~ ssRr(X560,X559)
| ~ ssPv2(X560)
| ~ ssRr(X559,X558)
| ~ ssPv3(X558)
| ~ ssPv1(X559)
| ssPv2(skf2(X559)) ),
inference(resolution,[status(thm)],[clause39,clause2]) ).
cnf(c313,plain,
( ~ ssRr(X671,skf3(X672))
| ~ ssPv2(X671)
| ~ ssPv3(X672)
| ~ ssPv1(skf3(X672))
| ssPv2(skf2(skf3(X672))) ),
inference(resolution,[status(thm)],[c181,clause1]) ).
cnf(c354,plain,
( ~ ssPv2(skf3(skf3(X673)))
| ~ ssPv3(X673)
| ~ ssPv1(skf3(X673))
| ssPv2(skf2(skf3(X673))) ),
inference(resolution,[status(thm)],[c313,clause1]) ).
cnf(clause37,negated_conjecture,
( ~ ssRr(X265,X268)
| ~ ssPv1(X265)
| ~ ssRr(X267,X268)
| ~ ssRr(X268,X266)
| ~ ssPv1(X266)
| ssPv3(X267)
| ssPv4(X268) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c163,plain,
( ~ ssRr(X553,skf3(X555))
| ~ ssPv1(X553)
| ~ ssRr(X554,skf3(X555))
| ~ ssPv1(X555)
| ssPv3(X554)
| ssPv4(skf3(X555)) ),
inference(resolution,[status(thm)],[clause37,clause1]) ).
cnf(c310,plain,
( ~ ssRr(X668,skf3(X669))
| ~ ssPv1(X668)
| ~ ssPv1(X669)
| ssPv3(skf3(skf3(X669)))
| ssPv4(skf3(X669)) ),
inference(resolution,[status(thm)],[c163,clause1]) ).
cnf(clause36,negated_conjecture,
( ~ ssRr(X254,X257)
| ~ ssPv2(X254)
| ~ ssRr(X256,X257)
| ~ ssRr(X257,X255)
| ~ ssPv4(X257)
| ssPv3(X256)
| ssPv1(X255) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c158,plain,
( ~ ssRr(X542,skf3(X543))
| ~ ssPv2(X542)
| ~ ssRr(X544,skf3(X543))
| ~ ssPv4(skf3(X543))
| ssPv3(X544)
| ssPv1(X543) ),
inference(resolution,[status(thm)],[clause36,clause1]) ).
cnf(c305,plain,
( ~ ssRr(X665,skf3(X666))
| ~ ssPv2(X665)
| ~ ssPv4(skf3(X666))
| ssPv3(skf3(skf3(X666)))
| ssPv1(X666) ),
inference(resolution,[status(thm)],[c158,clause1]) ).
cnf(clause35,negated_conjecture,
( ~ ssRr(X241,X244)
| ~ ssPv1(X241)
| ~ ssRr(X244,X243)
| ~ ssPv2(X243)
| ~ ssRr(X244,X242)
| ssPv4(X242)
| ssPv3(X244) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c147,plain,
( ~ ssRr(X523,skf3(X522))
| ~ ssPv1(X523)
| ~ ssRr(skf3(X522),X521)
| ~ ssPv2(X521)
| ssPv4(X522)
| ssPv3(skf3(X522)) ),
inference(resolution,[status(thm)],[clause35,clause1]) ).
cnf(c294,plain,
( ~ ssRr(skf3(X663),skf3(X663))
| ~ ssPv1(skf3(X663))
| ~ ssPv2(skf3(X663))
| ssPv4(X663)
| ssPv3(skf3(X663)) ),
inference(factor,[status(thm)],[c147]) ).
cnf(c173,plain,
( ~ ssRr(X540,X539)
| ~ ssPv4(X539)
| ~ ssRr(X540,X541)
| ~ ssPv1(X541)
| ~ ssPv1(X540)
| ssPv1(skf2(X540)) ),
inference(resolution,[status(thm)],[clause38,clause2]) ).
cnf(c302,plain,
( ~ ssRr(skf3(X661),X660)
| ~ ssPv4(X660)
| ~ ssPv1(X661)
| ~ ssPv1(skf3(X661))
| ssPv1(skf2(skf3(X661))) ),
inference(resolution,[status(thm)],[c173,clause1]) ).
cnf(c296,plain,
( ~ ssRr(X658,skf3(X659))
| ~ ssPv1(X658)
| ~ ssPv2(skf2(skf3(X659)))
| ssPv4(X659)
| ssPv3(skf3(X659)) ),
inference(resolution,[status(thm)],[c147,clause2]) ).
cnf(c159,plain,
( ~ ssRr(X517,X516)
| ~ ssPv2(X517)
| ~ ssRr(X518,X516)
| ~ ssPv4(X516)
| ssPv3(X518)
| ssPv1(skf2(X516)) ),
inference(resolution,[status(thm)],[clause36,clause2]) ).
cnf(c291,plain,
( ~ ssRr(X655,skf2(X654))
| ~ ssPv2(X655)
| ~ ssPv4(skf2(X654))
| ssPv3(X654)
| ssPv1(skf2(skf2(X654))) ),
inference(resolution,[status(thm)],[c159,clause2]) ).
cnf(c348,plain,
( ~ ssPv2(skf3(skf2(X657)))
| ~ ssPv4(skf2(X657))
| ssPv3(X657)
| ssPv1(skf2(skf2(X657))) ),
inference(resolution,[status(thm)],[c291,clause1]) ).
cnf(clause34,negated_conjecture,
( ~ ssRr(X227,X230)
| ~ ssRr(X229,X230)
| ~ ssRr(X230,X228)
| ~ ssPv2(X228)
| ~ ssPv1(X230)
| ssPv4(X227)
| ssPv1(X229) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c140,plain,
( ~ ssRr(X510,skf3(X509))
| ~ ssRr(X508,skf3(X509))
| ~ ssPv2(X509)
| ~ ssPv1(skf3(X509))
| ssPv4(X510)
| ssPv1(X508) ),
inference(resolution,[status(thm)],[clause34,clause1]) ).
cnf(c287,plain,
( ~ ssRr(X651,skf3(X652))
| ~ ssPv2(X652)
| ~ ssPv1(skf3(X652))
| ssPv4(X651)
| ssPv1(skf3(skf3(X652))) ),
inference(resolution,[status(thm)],[c140,clause1]) ).
cnf(c148,plain,
( ~ ssRr(X507,X505)
| ~ ssPv1(X507)
| ~ ssRr(X505,X506)
| ~ ssPv2(X506)
| ssPv4(skf2(X505))
| ssPv3(X505) ),
inference(resolution,[status(thm)],[clause35,clause2]) ).
cnf(c284,plain,
( ~ ssRr(X648,skf3(X649))
| ~ ssPv1(X648)
| ~ ssPv2(X649)
| ssPv4(skf2(skf3(X649)))
| ssPv3(skf3(X649)) ),
inference(resolution,[status(thm)],[c148,clause1]) ).
cnf(c346,plain,
( ~ ssPv1(skf3(skf3(X650)))
| ~ ssPv2(X650)
| ssPv4(skf2(skf3(X650)))
| ssPv3(skf3(X650)) ),
inference(resolution,[status(thm)],[c284,clause1]) ).
cnf(clause33,negated_conjecture,
( ~ ssRr(X216,X219)
| ~ ssRr(X219,X218)
| ~ ssPv3(X218)
| ~ ssRr(X219,X217)
| ssPv2(X216)
| ssPv1(X217)
| ssPv2(X219) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c134,plain,
( ~ ssRr(X497,X495)
| ~ ssRr(X495,X496)
| ~ ssPv3(X496)
| ssPv2(X497)
| ssPv1(skf2(X495))
| ssPv2(X495) ),
inference(resolution,[status(thm)],[clause33,clause2]) ).
cnf(c281,plain,
( ~ ssRr(X645,skf3(X646))
| ~ ssPv3(X646)
| ssPv2(X645)
| ssPv1(skf2(skf3(X646)))
| ssPv2(skf3(X646)) ),
inference(resolution,[status(thm)],[c134,clause1]) ).
cnf(c345,plain,
( ~ ssPv3(X647)
| ssPv2(skf3(skf3(X647)))
| ssPv1(skf2(skf3(X647)))
| ssPv2(skf3(X647)) ),
inference(resolution,[status(thm)],[c281,clause1]) ).
cnf(c133,plain,
( ~ ssRr(X486,skf3(X487))
| ~ ssRr(skf3(X487),X485)
| ~ ssPv3(X485)
| ssPv2(X486)
| ssPv1(X487)
| ssPv2(skf3(X487)) ),
inference(resolution,[status(thm)],[clause33,clause1]) ).
cnf(c277,plain,
( ~ ssRr(X643,skf3(X644))
| ~ ssPv3(skf2(skf3(X644)))
| ssPv2(X643)
| ssPv1(X644)
| ssPv2(skf3(X644)) ),
inference(resolution,[status(thm)],[c133,clause2]) ).
cnf(clause32,negated_conjecture,
( ~ ssRr(X207,X210)
| ~ ssPv2(X207)
| ~ ssRr(X209,X210)
| ~ ssRr(X210,X208)
| ssPv1(X209)
| ssPv2(X208)
| ssPv3(X210) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c130,plain,
( ~ ssRr(X481,X480)
| ~ ssPv2(X481)
| ~ ssRr(X482,X480)
| ssPv1(X482)
| ssPv2(skf2(X480))
| ssPv3(X480) ),
inference(resolution,[status(thm)],[clause32,clause2]) ).
cnf(c272,plain,
( ~ ssRr(X639,skf2(X640))
| ~ ssPv2(X639)
| ssPv1(X640)
| ssPv2(skf2(skf2(X640)))
| ssPv3(skf2(X640)) ),
inference(resolution,[status(thm)],[c130,clause2]) ).
cnf(c343,plain,
( ~ ssPv2(skf3(skf2(X642)))
| ssPv1(X642)
| ssPv2(skf2(skf2(X642)))
| ssPv3(skf2(X642)) ),
inference(resolution,[status(thm)],[c272,clause1]) ).
cnf(c129,plain,
( ~ ssRr(X472,skf3(X474))
| ~ ssPv2(X472)
| ~ ssRr(X473,skf3(X474))
| ssPv1(X473)
| ssPv2(X474)
| ssPv3(skf3(X474)) ),
inference(resolution,[status(thm)],[clause32,clause1]) ).
cnf(c268,plain,
( ~ ssRr(X637,skf3(X636))
| ~ ssPv2(X637)
| ssPv1(skf3(skf3(X636)))
| ssPv2(X636)
| ssPv3(skf3(X636)) ),
inference(resolution,[status(thm)],[c129,clause1]) ).
cnf(clause31,negated_conjecture,
( ~ ssRr(X198,X201)
| ~ ssPv1(X198)
| ~ ssRr(X201,X200)
| ~ ssRr(X201,X199)
| ssPv4(X200)
| ssPv2(X199)
| ssPv4(X201) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c126,plain,
( ~ ssRr(X471,X469)
| ~ ssPv1(X471)
| ~ ssRr(X469,X470)
| ssPv4(X470)
| ssPv2(skf2(X469))
| ssPv4(X469) ),
inference(resolution,[status(thm)],[clause31,clause2]) ).
cnf(c265,plain,
( ~ ssRr(X633,skf3(X634))
| ~ ssPv1(X633)
| ssPv4(X634)
| ssPv2(skf2(skf3(X634)))
| ssPv4(skf3(X634)) ),
inference(resolution,[status(thm)],[c126,clause1]) ).
cnf(c341,plain,
( ~ ssPv1(skf3(skf3(X635)))
| ssPv4(X635)
| ssPv2(skf2(skf3(X635)))
| ssPv4(skf3(X635)) ),
inference(resolution,[status(thm)],[c265,clause1]) ).
cnf(c125,plain,
( ~ ssRr(X462,skf3(X460))
| ~ ssPv1(X462)
| ~ ssRr(skf3(X460),X461)
| ssPv4(X461)
| ssPv2(X460)
| ssPv4(skf3(X460)) ),
inference(resolution,[status(thm)],[clause31,clause1]) ).
cnf(c261,plain,
( ~ ssRr(X628,skf3(X629))
| ~ ssPv1(X628)
| ssPv4(skf2(skf3(X629)))
| ssPv2(X629)
| ssPv4(skf3(X629)) ),
inference(resolution,[status(thm)],[c125,clause2]) ).
cnf(c340,plain,
( ~ ssPv1(skf3(skf3(X632)))
| ssPv4(skf2(skf3(X632)))
| ssPv2(X632)
| ssPv4(skf3(X632)) ),
inference(resolution,[status(thm)],[c261,clause1]) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X189,X192)
| ~ ssRr(X191,X192)
| ~ ssRr(X192,X190)
| ~ ssPv1(X192)
| ssPv4(X189)
| ssPv2(X191)
| ssPv1(X190) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c122,plain,
( ~ ssRr(X454,X453)
| ~ ssRr(X455,X453)
| ~ ssPv1(X453)
| ssPv4(X454)
| ssPv2(X455)
| ssPv1(skf2(X453)) ),
inference(resolution,[status(thm)],[clause30,clause2]) ).
cnf(c256,plain,
( ~ ssRr(X627,skf2(X626))
| ~ ssPv1(skf2(X626))
| ssPv4(X627)
| ssPv2(X626)
| ssPv1(skf2(skf2(X626))) ),
inference(resolution,[status(thm)],[c122,clause2]) ).
cnf(c338,plain,
( ~ ssPv1(skf2(X631))
| ssPv4(skf3(skf2(X631)))
| ssPv2(X631)
| ssPv1(skf2(skf2(X631))) ),
inference(resolution,[status(thm)],[c256,clause1]) ).
cnf(c332,plain,
( ~ ssRr(skf3(X614),X613)
| ~ ssPv4(X613)
| ~ ssPv3(X613)
| ~ ssPv1(X614)
| ~ ssPv2(skf3(X614)) ),
inference(factor,[status(thm)],[c202]) ).
cnf(c336,plain,
( ~ ssPv4(skf2(skf3(X624)))
| ~ ssPv3(skf2(skf3(X624)))
| ~ ssPv1(X624)
| ~ ssPv2(skf3(X624)) ),
inference(resolution,[status(thm)],[c332,clause2]) ).
cnf(c327,plain,
( ~ ssRr(X596,skf3(X595))
| ~ ssPv4(X596)
| ~ ssPv1(X596)
| ~ ssPv4(X595)
| ssPv2(skf3(X595)) ),
inference(factor,[status(thm)],[c185]) ).
cnf(c329,plain,
( ~ ssPv4(skf3(skf3(X623)))
| ~ ssPv1(skf3(skf3(X623)))
| ~ ssPv4(X623)
| ssPv2(skf3(X623)) ),
inference(resolution,[status(thm)],[c327,clause1]) ).
cnf(c316,plain,
( ~ ssRr(skf3(X570),X571)
| ~ ssPv4(X571)
| ~ ssPv1(X571)
| ~ ssPv1(skf3(X570))
| ssPv1(X570) ),
inference(factor,[status(thm)],[c172]) ).
cnf(c320,plain,
( ~ ssPv4(skf2(skf3(X622)))
| ~ ssPv1(skf2(skf3(X622)))
| ~ ssPv1(skf3(X622))
| ssPv1(X622) ),
inference(resolution,[status(thm)],[c316,clause2]) ).
cnf(c121,plain,
( ~ ssRr(X449,skf3(X448))
| ~ ssRr(X450,skf3(X448))
| ~ ssPv1(skf3(X448))
| ssPv4(X449)
| ssPv2(X450)
| ssPv1(X448) ),
inference(resolution,[status(thm)],[clause30,clause1]) ).
cnf(c252,plain,
( ~ ssRr(X620,skf3(X621))
| ~ ssPv1(skf3(X621))
| ssPv4(X620)
| ssPv2(skf3(skf3(X621)))
| ssPv1(X621) ),
inference(resolution,[status(thm)],[c121,clause1]) ).
cnf(c309,plain,
( ~ ssRr(X557,skf3(X556))
| ~ ssPv1(X557)
| ~ ssPv1(X556)
| ssPv3(X557)
| ssPv4(skf3(X556)) ),
inference(factor,[status(thm)],[c163]) ).
cnf(c311,plain,
( ~ ssPv1(skf3(skf3(X619)))
| ~ ssPv1(X619)
| ssPv3(skf3(skf3(X619)))
| ssPv4(skf3(X619)) ),
inference(resolution,[status(thm)],[c309,clause1]) ).
cnf(c304,plain,
( ~ ssRr(X552,skf3(X551))
| ~ ssPv2(X552)
| ~ ssPv4(skf3(X551))
| ssPv3(X552)
| ssPv1(X551) ),
inference(factor,[status(thm)],[c158]) ).
cnf(c308,plain,
( ~ ssPv2(skf3(skf3(X618)))
| ~ ssPv4(skf3(X618))
| ssPv3(skf3(skf3(X618)))
| ssPv1(X618) ),
inference(resolution,[status(thm)],[c304,clause1]) ).
cnf(c290,plain,
( ~ ssRr(X526,X527)
| ~ ssPv2(X526)
| ~ ssPv4(X527)
| ssPv3(skf3(X527))
| ssPv1(skf2(X527)) ),
inference(resolution,[status(thm)],[c159,clause1]) ).
cnf(c298,plain,
( ~ ssPv2(X609)
| ~ ssPv4(skf2(X609))
| ssPv3(skf3(skf2(X609)))
| ssPv1(skf2(skf2(X609))) ),
inference(resolution,[status(thm)],[c290,clause2]) ).
cnf(c286,plain,
( ~ ssRr(X514,skf3(X515))
| ~ ssPv2(X515)
| ~ ssPv1(skf3(X515))
| ssPv4(X514)
| ssPv1(X514) ),
inference(factor,[status(thm)],[c140]) ).
cnf(c288,plain,
( ~ ssPv2(X608)
| ~ ssPv1(skf3(X608))
| ssPv4(skf3(skf3(X608)))
| ssPv1(skf3(skf3(X608))) ),
inference(resolution,[status(thm)],[c286,clause1]) ).
cnf(c271,plain,
( ~ ssRr(X490,X491)
| ~ ssPv2(X490)
| ssPv1(skf3(X491))
| ssPv2(skf2(X491))
| ssPv3(X491) ),
inference(resolution,[status(thm)],[c130,clause1]) ).
cnf(c279,plain,
( ~ ssPv2(X607)
| ssPv1(skf3(skf2(X607)))
| ssPv2(skf2(skf2(X607)))
| ssPv3(skf2(X607)) ),
inference(resolution,[status(thm)],[c271,clause2]) ).
cnf(c267,plain,
( ~ ssRr(X478,skf3(X479))
| ~ ssPv2(X478)
| ssPv1(X478)
| ssPv2(X479)
| ssPv3(skf3(X479)) ),
inference(factor,[status(thm)],[c129]) ).
cnf(c269,plain,
( ~ ssPv2(skf3(skf3(X606)))
| ssPv1(skf3(skf3(X606)))
| ssPv2(X606)
| ssPv3(skf3(X606)) ),
inference(resolution,[status(thm)],[c267,clause1]) ).
cnf(c255,plain,
( ~ ssRr(X463,X464)
| ~ ssPv1(X464)
| ssPv4(X463)
| ssPv2(skf3(X464))
| ssPv1(skf2(X464)) ),
inference(resolution,[status(thm)],[c122,clause1]) ).
cnf(c263,plain,
( ~ ssPv1(skf2(X600))
| ssPv4(X600)
| ssPv2(skf3(skf2(X600)))
| ssPv1(skf2(skf2(X600))) ),
inference(resolution,[status(thm)],[c255,clause2]) ).
cnf(c251,plain,
( ~ ssRr(X451,skf3(X452))
| ~ ssPv1(skf3(X452))
| ssPv4(X451)
| ssPv2(X451)
| ssPv1(X452) ),
inference(factor,[status(thm)],[c121]) ).
cnf(c253,plain,
( ~ ssPv1(skf3(X599))
| ssPv4(skf3(skf3(X599)))
| ssPv2(skf3(skf3(X599)))
| ssPv1(X599) ),
inference(resolution,[status(thm)],[c251,clause1]) ).
cnf(c200,plain,
( ~ ssRr(X357,X355)
| ~ ssPv4(X355)
| ~ ssRr(X357,X356)
| ~ ssPv3(X356)
| ~ ssPv1(X355)
| ~ ssPv2(X357) ),
inference(factor,[status(thm)],[clause42]) ).
cnf(c213,plain,
( ~ ssRr(skf3(X382),X381)
| ~ ssPv4(X381)
| ~ ssPv3(X382)
| ~ ssPv1(X381)
| ~ ssPv2(skf3(X382)) ),
inference(resolution,[status(thm)],[c200,clause1]) ).
cnf(c225,plain,
( ~ ssPv4(skf2(skf3(X598)))
| ~ ssPv3(X598)
| ~ ssPv1(skf2(skf3(X598)))
| ~ ssPv2(skf3(X598)) ),
inference(resolution,[status(thm)],[c213,clause2]) ).
cnf(c170,plain,
( ~ ssRr(X310,X312)
| ~ ssPv4(X312)
| ~ ssRr(X310,X311)
| ~ ssPv1(X311)
| ~ ssPv1(X310)
| ssPv1(X312) ),
inference(factor,[status(thm)],[clause38]) ).
cnf(c191,plain,
( ~ ssRr(skf3(X351),X350)
| ~ ssPv4(X350)
| ~ ssPv1(X351)
| ~ ssPv1(skf3(X351))
| ssPv1(X350) ),
inference(resolution,[status(thm)],[c170,clause1]) ).
cnf(c210,plain,
( ~ ssPv4(skf2(skf3(X597)))
| ~ ssPv1(X597)
| ~ ssPv1(skf3(X597))
| ssPv1(skf2(skf3(X597))) ),
inference(resolution,[status(thm)],[c191,clause2]) ).
cnf(c203,plain,
( ~ ssRr(X589,X591)
| ~ ssPv4(X591)
| ~ ssRr(X589,X590)
| ~ ssPv3(X590)
| ~ ssPv1(skf2(X589))
| ~ ssPv2(X589) ),
inference(resolution,[status(thm)],[clause42,clause2]) ).
cnf(c196,plain,
( ~ ssRr(X585,X583)
| ~ ssPv2(X585)
| ~ ssRr(X584,X583)
| ~ ssPv2(skf2(X583))
| ~ ssPv2(X583)
| ssPv2(X584) ),
inference(resolution,[status(thm)],[clause41,clause2]) ).
cnf(c325,plain,
( ~ ssRr(skf2(X586),X586)
| ~ ssPv2(skf2(X586))
| ~ ssRr(X587,X586)
| ~ ssPv2(X586)
| ssPv2(X587) ),
inference(factor,[status(thm)],[c196]) ).
cnf(c186,plain,
( ~ ssRr(X566,X565)
| ~ ssPv4(X566)
| ~ ssRr(X564,X565)
| ~ ssPv1(X564)
| ~ ssPv4(skf2(X565))
| ssPv2(X565) ),
inference(resolution,[status(thm)],[clause40,clause2]) ).
cnf(c315,plain,
( ~ ssRr(skf2(X575),X575)
| ~ ssPv4(skf2(X575))
| ~ ssRr(X576,X575)
| ~ ssPv1(X576)
| ssPv2(X575) ),
inference(factor,[status(thm)],[c186]) ).
cnf(c321,plain,
( ~ ssRr(skf2(X577),X577)
| ~ ssPv4(skf2(X577))
| ~ ssPv1(skf2(X577))
| ssPv2(X577) ),
inference(factor,[status(thm)],[c315]) ).
cnf(c312,plain,
( ~ ssRr(X561,X561)
| ~ ssPv2(X561)
| ~ ssPv3(X561)
| ~ ssPv1(X561)
| ssPv2(skf2(X561)) ),
inference(factor,[status(thm)],[c181]) ).
cnf(c301,plain,
( ~ ssRr(X545,X546)
| ~ ssPv4(X546)
| ~ ssPv1(X546)
| ~ ssPv1(X545)
| ssPv1(skf2(X545)) ),
inference(factor,[status(thm)],[c173]) ).
cnf(c306,plain,
( ~ ssPv4(X547)
| ~ ssPv1(X547)
| ~ ssPv1(skf3(X547))
| ssPv1(skf2(skf3(X547))) ),
inference(resolution,[status(thm)],[c301,clause1]) ).
cnf(c124,plain,
( ~ ssRr(X236,X235)
| ~ ssPv1(X236)
| ~ ssRr(X235,X237)
| ssPv4(X237)
| ssPv2(X237)
| ssPv4(X235) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c144,plain,
( ~ ssRr(X274,X273)
| ~ ssPv1(X274)
| ssPv4(skf2(X273))
| ssPv2(skf2(X273))
| ssPv4(X273) ),
inference(resolution,[status(thm)],[c124,clause2]) ).
cnf(c169,plain,
( ~ ssPv1(X538)
| ssPv4(skf2(skf2(X538)))
| ssPv2(skf2(skf2(X538)))
| ssPv4(skf2(X538)) ),
inference(resolution,[status(thm)],[c144,clause2]) ).
cnf(c164,plain,
( ~ ssRr(X532,X533)
| ~ ssPv1(X532)
| ~ ssRr(X534,X533)
| ~ ssPv1(skf2(X533))
| ssPv3(X534)
| ssPv4(X533) ),
inference(resolution,[status(thm)],[clause37,clause2]) ).
cnf(c299,plain,
( ~ ssRr(skf2(X536),X536)
| ~ ssPv1(skf2(X536))
| ~ ssRr(X535,X536)
| ssPv3(X535)
| ssPv4(X536) ),
inference(factor,[status(thm)],[c164]) ).
cnf(c300,plain,
( ~ ssRr(skf2(X537),X537)
| ~ ssPv1(skf2(X537))
| ssPv3(skf2(X537))
| ssPv4(X537) ),
inference(factor,[status(thm)],[c299]) ).
cnf(c138,plain,
( ~ ssRr(X253,X253)
| ~ ssRr(X252,X253)
| ~ ssPv2(X253)
| ~ ssPv1(X253)
| ssPv4(X253)
| ssPv1(X252) ),
inference(factor,[status(thm)],[clause34]) ).
cnf(c155,plain,
( ~ ssRr(skf2(X531),skf2(X531))
| ~ ssPv2(skf2(X531))
| ~ ssPv1(skf2(X531))
| ssPv4(skf2(X531))
| ssPv1(X531) ),
inference(resolution,[status(thm)],[c138,clause2]) ).
cnf(c289,plain,
( ~ ssRr(X520,X519)
| ~ ssPv2(X520)
| ~ ssPv4(X519)
| ssPv3(X520)
| ssPv1(skf2(X519)) ),
inference(factor,[status(thm)],[c159]) ).
cnf(c293,plain,
( ~ ssPv2(X525)
| ~ ssPv4(skf2(X525))
| ssPv3(X525)
| ssPv1(skf2(skf2(X525))) ),
inference(resolution,[status(thm)],[c289,clause2]) ).
cnf(c292,plain,
( ~ ssPv2(skf3(X524))
| ~ ssPv4(X524)
| ssPv3(skf3(X524))
| ssPv1(skf2(X524)) ),
inference(resolution,[status(thm)],[c289,clause1]) ).
cnf(c283,plain,
( ~ ssRr(X511,X511)
| ~ ssPv1(X511)
| ~ ssPv2(X511)
| ssPv4(skf2(X511))
| ssPv3(X511) ),
inference(factor,[status(thm)],[c148]) ).
cnf(c141,plain,
( ~ ssRr(X504,X502)
| ~ ssRr(X503,X502)
| ~ ssPv2(skf2(X502))
| ~ ssPv1(X502)
| ssPv4(X504)
| ssPv1(X503) ),
inference(resolution,[status(thm)],[clause34,clause2]) ).
cnf(c275,plain,
( ~ ssRr(skf3(X501),skf3(X501))
| ~ ssPv3(skf3(X501))
| ssPv2(skf3(X501))
| ssPv1(X501) ),
inference(factor,[status(thm)],[c133]) ).
cnf(c280,plain,
( ~ ssRr(X498,X498)
| ~ ssPv3(X498)
| ssPv2(X498)
| ssPv1(skf2(X498)) ),
inference(factor,[status(thm)],[c134]) ).
cnf(c270,plain,
( ~ ssRr(X484,X483)
| ~ ssPv2(X484)
| ssPv1(X484)
| ssPv2(skf2(X483))
| ssPv3(X483) ),
inference(factor,[status(thm)],[c130]) ).
cnf(c274,plain,
( ~ ssPv2(X489)
| ssPv1(X489)
| ssPv2(skf2(skf2(X489)))
| ssPv3(skf2(X489)) ),
inference(resolution,[status(thm)],[c270,clause2]) ).
cnf(c273,plain,
( ~ ssPv2(skf3(X488))
| ssPv1(skf3(X488))
| ssPv2(skf2(X488))
| ssPv3(X488) ),
inference(resolution,[status(thm)],[c270,clause1]) ).
cnf(c264,plain,
( ~ ssRr(X475,X475)
| ~ ssPv1(X475)
| ssPv4(X475)
| ssPv2(skf2(X475)) ),
inference(factor,[status(thm)],[c126]) ).
cnf(c259,plain,
( ~ ssRr(skf3(X468),skf3(X468))
| ~ ssPv1(skf3(X468))
| ssPv4(skf3(X468))
| ssPv2(X468) ),
inference(factor,[status(thm)],[c125]) ).
cnf(c254,plain,
( ~ ssRr(X456,X457)
| ~ ssPv1(X457)
| ssPv4(X456)
| ssPv2(X456)
| ssPv1(skf2(X457)) ),
inference(factor,[status(thm)],[c122]) ).
cnf(c258,plain,
( ~ ssPv1(skf2(X459))
| ssPv4(X459)
| ssPv2(X459)
| ssPv1(skf2(skf2(X459))) ),
inference(resolution,[status(thm)],[c254,clause2]) ).
cnf(c257,plain,
( ~ ssPv1(X458)
| ssPv4(skf3(X458))
| ssPv2(skf3(X458))
| ssPv1(skf2(X458)) ),
inference(resolution,[status(thm)],[c254,clause1]) ).
cnf(clause29,negated_conjecture,
( ~ ssRr(X180,X182)
| ~ ssPv4(X180)
| ~ ssRr(X182,X181)
| ~ ssPv1(X182)
| ~ ssPv3(X182)
| ssPv2(X181) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c115,plain,
( ~ ssRr(X445,skf3(X446))
| ~ ssPv4(X445)
| ~ ssPv1(skf3(X446))
| ~ ssPv3(skf3(X446))
| ssPv2(X446) ),
inference(resolution,[status(thm)],[clause29,clause1]) ).
cnf(c250,plain,
( ~ ssPv4(skf3(skf3(X447)))
| ~ ssPv1(skf3(X447))
| ~ ssPv3(skf3(X447))
| ssPv2(X447) ),
inference(resolution,[status(thm)],[c115,clause1]) ).
cnf(clause28,negated_conjecture,
( ~ ssRr(X170,X172)
| ~ ssPv1(X170)
| ~ ssRr(X172,X171)
| ~ ssPv2(X172)
| ~ ssPv3(X172)
| ssPv1(X171) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c108,plain,
( ~ ssRr(X443,skf3(X442))
| ~ ssPv1(X443)
| ~ ssPv2(skf3(X442))
| ~ ssPv3(skf3(X442))
| ssPv1(X442) ),
inference(resolution,[status(thm)],[clause28,clause1]) ).
cnf(c249,plain,
( ~ ssPv1(skf3(skf3(X444)))
| ~ ssPv2(skf3(X444))
| ~ ssPv3(skf3(X444))
| ssPv1(X444) ),
inference(resolution,[status(thm)],[c108,clause1]) ).
cnf(clause27,negated_conjecture,
( ~ ssRr(X160,X162)
| ~ ssPv4(X160)
| ~ ssRr(X162,X161)
| ~ ssPv2(X162)
| ssPv1(X161)
| ssPv1(X162) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c101,plain,
( ~ ssRr(X439,skf3(X440))
| ~ ssPv4(X439)
| ~ ssPv2(skf3(X440))
| ssPv1(X440)
| ssPv1(skf3(X440)) ),
inference(resolution,[status(thm)],[clause27,clause1]) ).
cnf(c248,plain,
( ~ ssPv4(skf3(skf3(X441)))
| ~ ssPv2(skf3(X441))
| ssPv1(X441)
| ssPv1(skf3(X441)) ),
inference(resolution,[status(thm)],[c101,clause1]) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X157,X159)
| ~ ssPv2(X159)
| ~ ssRr(X157,X158)
| ~ ssPv2(X157)
| ssPv3(X158)
| ssPv1(X157) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c98,plain,
( ~ ssRr(skf3(X436),X435)
| ~ ssPv2(X435)
| ~ ssPv2(skf3(X436))
| ssPv3(X436)
| ssPv1(skf3(X436)) ),
inference(resolution,[status(thm)],[clause26,clause1]) ).
cnf(c247,plain,
( ~ ssPv2(skf2(skf3(X438)))
| ~ ssPv2(skf3(X438))
| ssPv3(X438)
| ssPv1(skf3(X438)) ),
inference(resolution,[status(thm)],[c98,clause2]) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X149,X151)
| ~ ssPv3(X149)
| ~ ssRr(X151,X150)
| ~ ssPv3(X151)
| ssPv3(X150)
| ssPv1(X151) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c93,plain,
( ~ ssRr(X431,skf3(X432))
| ~ ssPv3(X431)
| ~ ssPv3(skf3(X432))
| ssPv3(X432)
| ssPv1(skf3(X432)) ),
inference(resolution,[status(thm)],[clause25,clause1]) ).
cnf(c245,plain,
( ~ ssPv3(skf3(skf3(X434)))
| ~ ssPv3(skf3(X434))
| ssPv3(X434)
| ssPv1(skf3(X434)) ),
inference(resolution,[status(thm)],[c93,clause1]) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X139,X141)
| ~ ssPv2(X139)
| ~ ssRr(X140,X141)
| ~ ssPv3(X141)
| ssPv4(X140)
| ssPv1(X141) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c87,plain,
( ~ ssRr(X429,skf2(X428))
| ~ ssPv2(X429)
| ~ ssPv3(skf2(X428))
| ssPv4(X428)
| ssPv1(skf2(X428)) ),
inference(resolution,[status(thm)],[clause24,clause2]) ).
cnf(c243,plain,
( ~ ssPv2(skf3(skf2(X433)))
| ~ ssPv3(skf2(X433))
| ssPv4(X433)
| ssPv1(skf2(X433)) ),
inference(resolution,[status(thm)],[c87,clause1]) ).
cnf(clause23,negated_conjecture,
( ~ ssRr(X132,X134)
| ~ ssPv4(X134)
| ~ ssRr(X132,X133)
| ~ ssPv1(X132)
| ssPv4(X133)
| ssPv2(X132) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c81,plain,
( ~ ssRr(skf3(X424),X423)
| ~ ssPv4(X423)
| ~ ssPv1(skf3(X424))
| ssPv4(X424)
| ssPv2(skf3(X424)) ),
inference(resolution,[status(thm)],[clause23,clause1]) ).
cnf(c242,plain,
( ~ ssPv4(skf2(skf3(X427)))
| ~ ssPv1(skf3(X427))
| ssPv4(X427)
| ssPv2(skf3(X427)) ),
inference(resolution,[status(thm)],[c81,clause2]) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X126,X128)
| ~ ssRr(X128,X127)
| ~ ssPv1(X127)
| ~ ssPv1(X128)
| ssPv4(X126)
| ssPv2(X128) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c78,plain,
( ~ ssRr(X422,skf3(X421))
| ~ ssPv1(X421)
| ~ ssPv1(skf3(X421))
| ssPv4(X422)
| ssPv2(skf3(X421)) ),
inference(resolution,[status(thm)],[clause22,clause1]) ).
cnf(c240,plain,
( ~ ssPv1(X426)
| ~ ssPv1(skf3(X426))
| ssPv4(skf3(skf3(X426)))
| ssPv2(skf3(X426)) ),
inference(resolution,[status(thm)],[c78,clause1]) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X116,X118)
| ~ ssPv4(X118)
| ~ ssRr(X116,X117)
| ~ ssPv3(X116)
| ssPv3(X117)
| ssPv2(X116) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c71,plain,
( ~ ssRr(skf3(X417),X418)
| ~ ssPv4(X418)
| ~ ssPv3(skf3(X417))
| ssPv3(X417)
| ssPv2(skf3(X417)) ),
inference(resolution,[status(thm)],[clause21,clause1]) ).
cnf(c239,plain,
( ~ ssPv4(skf2(skf3(X420)))
| ~ ssPv3(skf3(X420))
| ssPv3(X420)
| ssPv2(skf3(X420)) ),
inference(resolution,[status(thm)],[c71,clause2]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X106,X108)
| ~ ssPv4(X106)
| ~ ssRr(X108,X107)
| ~ ssPv2(X108)
| ssPv2(X107)
| ssPv3(X108) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c64,plain,
( ~ ssRr(X414,skf3(X415))
| ~ ssPv4(X414)
| ~ ssPv2(skf3(X415))
| ssPv2(X415)
| ssPv3(skf3(X415)) ),
inference(resolution,[status(thm)],[clause20,clause1]) ).
cnf(c237,plain,
( ~ ssPv4(skf3(skf3(X416)))
| ~ ssPv2(skf3(X416))
| ssPv2(X416)
| ssPv3(skf3(X416)) ),
inference(resolution,[status(thm)],[c64,clause1]) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X101,X103)
| ~ ssPv1(X103)
| ~ ssRr(X101,X102)
| ~ ssPv4(X101)
| ssPv1(X102)
| ssPv3(X101) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c61,plain,
( ~ ssRr(skf3(X411),X410)
| ~ ssPv1(X410)
| ~ ssPv4(skf3(X411))
| ssPv1(X411)
| ssPv3(skf3(X411)) ),
inference(resolution,[status(thm)],[clause19,clause1]) ).
cnf(c236,plain,
( ~ ssPv1(skf2(skf3(X413)))
| ~ ssPv4(skf3(X413))
| ssPv1(X413)
| ssPv3(skf3(X413)) ),
inference(resolution,[status(thm)],[c61,clause2]) ).
cnf(c183,plain,
( ~ ssRr(X307,X307)
| ~ ssPv4(X307)
| ~ ssRr(X306,X307)
| ~ ssPv1(X306)
| ssPv2(X307) ),
inference(factor,[status(thm)],[clause40]) ).
cnf(c189,plain,
( ~ ssRr(skf2(X409),skf2(X409))
| ~ ssPv4(skf2(X409))
| ~ ssPv1(X409)
| ssPv2(skf2(X409)) ),
inference(resolution,[status(thm)],[c183,clause2]) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X94,X96)
| ~ ssRr(X96,X95)
| ~ ssPv2(X95)
| ~ ssPv4(X96)
| ssPv3(X94)
| ssPv3(X96) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c58,plain,
( ~ ssRr(X406,skf3(X407))
| ~ ssPv2(X407)
| ~ ssPv4(skf3(X407))
| ssPv3(X406)
| ssPv3(skf3(X407)) ),
inference(resolution,[status(thm)],[clause18,clause1]) ).
cnf(c234,plain,
( ~ ssPv2(X408)
| ~ ssPv4(skf3(X408))
| ssPv3(skf3(skf3(X408)))
| ssPv3(skf3(X408)) ),
inference(resolution,[status(thm)],[c58,clause1]) ).
cnf(c161,plain,
( ~ ssRr(X269,X269)
| ~ ssPv1(X269)
| ~ ssRr(X270,X269)
| ssPv3(X270)
| ssPv4(X269) ),
inference(factor,[status(thm)],[clause37]) ).
cnf(c167,plain,
( ~ ssRr(skf2(X405),skf2(X405))
| ~ ssPv1(skf2(X405))
| ssPv3(X405)
| ssPv4(skf2(X405)) ),
inference(resolution,[status(thm)],[c161,clause2]) ).
cnf(c131,plain,
( ~ ssRr(X221,X221)
| ~ ssRr(X221,X220)
| ~ ssPv3(X220)
| ssPv2(X221)
| ssPv1(X221) ),
inference(factor,[status(thm)],[clause33]) ).
cnf(c136,plain,
( ~ ssRr(skf3(X404),skf3(X404))
| ~ ssPv3(X404)
| ssPv2(skf3(X404))
| ssPv1(skf3(X404)) ),
inference(resolution,[status(thm)],[c131,clause1]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X84,X86)
| ~ ssPv3(X86)
| ~ ssRr(X84,X85)
| ~ ssPv1(X84)
| ssPv4(X85)
| ssPv4(X84) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c51,plain,
( ~ ssRr(skf3(X400),X399)
| ~ ssPv3(X399)
| ~ ssPv1(skf3(X400))
| ssPv4(X400)
| ssPv4(skf3(X400)) ),
inference(resolution,[status(thm)],[clause17,clause1]) ).
cnf(c233,plain,
( ~ ssPv3(skf2(skf3(X403)))
| ~ ssPv1(skf3(X403))
| ssPv4(X403)
| ssPv4(skf3(X403)) ),
inference(resolution,[status(thm)],[c51,clause2]) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X74,X76)
| ~ ssRr(X74,X75)
| ~ ssPv2(X74)
| ~ ssPv3(X74)
| ssPv3(X76)
| ssPv1(X75) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c44,plain,
( ~ ssRr(skf3(X392),X391)
| ~ ssPv2(skf3(X392))
| ~ ssPv3(skf3(X392))
| ssPv3(X391)
| ssPv1(X392) ),
inference(resolution,[status(thm)],[clause16,clause1]) ).
cnf(c231,plain,
( ~ ssPv2(skf3(X402))
| ~ ssPv3(skf3(X402))
| ssPv3(skf2(skf3(X402)))
| ssPv1(X402) ),
inference(resolution,[status(thm)],[c44,clause2]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X64,X66)
| ~ ssRr(X64,X65)
| ~ ssPv2(X64)
| ~ ssPv3(X64)
| ssPv4(X66)
| ssPv2(X65) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c37,plain,
( ~ ssRr(skf3(X384),X383)
| ~ ssPv2(skf3(X384))
| ~ ssPv3(skf3(X384))
| ssPv4(X383)
| ssPv2(X384) ),
inference(resolution,[status(thm)],[clause15,clause1]) ).
cnf(c227,plain,
( ~ ssPv2(skf3(X398))
| ~ ssPv3(skf3(X398))
| ssPv4(skf2(skf3(X398)))
| ssPv2(X398) ),
inference(resolution,[status(thm)],[c37,clause2]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X54,X56)
| ~ ssPv1(X54)
| ~ ssRr(X56,X55)
| ssPv3(X55)
| ssPv2(X56)
| ssPv3(X56) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c30,plain,
( ~ ssRr(X373,skf3(X374))
| ~ ssPv1(X373)
| ssPv3(X374)
| ssPv2(skf3(X374))
| ssPv3(skf3(X374)) ),
inference(resolution,[status(thm)],[clause14,clause1]) ).
cnf(c222,plain,
( ~ ssPv1(skf3(skf3(X397)))
| ssPv3(X397)
| ssPv2(skf3(X397))
| ssPv3(skf3(X397)) ),
inference(resolution,[status(thm)],[c30,clause1]) ).
cnf(c201,plain,
( ~ ssRr(X369,X367)
| ~ ssPv4(X367)
| ~ ssRr(X369,X368)
| ~ ssPv3(X368)
| ~ ssPv1(X368)
| ~ ssPv2(X369) ),
inference(factor,[status(thm)],[clause42]) ).
cnf(c221,plain,
( ~ ssRr(X395,X396)
| ~ ssPv4(X396)
| ~ ssPv3(skf2(X395))
| ~ ssPv1(skf2(X395))
| ~ ssPv2(X395) ),
inference(resolution,[status(thm)],[c201,clause2]) ).
cnf(c220,plain,
( ~ ssRr(skf3(X388),X389)
| ~ ssPv4(X389)
| ~ ssPv3(X388)
| ~ ssPv1(X388)
| ~ ssPv2(skf3(X388)) ),
inference(resolution,[status(thm)],[c201,clause1]) ).
cnf(c229,plain,
( ~ ssPv4(skf2(skf3(X394)))
| ~ ssPv3(X394)
| ~ ssPv1(X394)
| ~ ssPv2(skf3(X394)) ),
inference(resolution,[status(thm)],[c220,clause2]) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X43,X45)
| ~ ssPv1(X45)
| ~ ssRr(X43,X44)
| ssPv1(X44)
| ssPv3(X43)
| ssPv4(X43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c23,plain,
( ~ ssRr(skf3(X364),X363)
| ~ ssPv1(X363)
| ssPv1(X364)
| ssPv3(skf3(X364))
| ssPv4(skf3(X364)) ),
inference(resolution,[status(thm)],[clause13,clause1]) ).
cnf(c218,plain,
( ~ ssPv1(skf2(skf3(X387)))
| ssPv1(X387)
| ssPv3(skf3(X387))
| ssPv4(skf3(X387)) ),
inference(resolution,[status(thm)],[c23,clause2]) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X35,X37)
| ~ ssRr(X37,X36)
| ~ ssPv4(X37)
| ssPv4(X35)
| ssPv3(X36)
| ssPv3(X37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c20,plain,
( ~ ssRr(X352,skf3(X353))
| ~ ssPv4(skf3(X353))
| ssPv4(X352)
| ssPv3(X353)
| ssPv3(skf3(X353)) ),
inference(resolution,[status(thm)],[clause12,clause1]) ).
cnf(c211,plain,
( ~ ssPv4(skf3(X380))
| ssPv4(skf3(skf3(X380)))
| ssPv3(X380)
| ssPv3(skf3(X380)) ),
inference(resolution,[status(thm)],[c20,clause1]) ).
cnf(c179,plain,
( ~ ssRr(X345,X344)
| ~ ssPv2(X345)
| ~ ssRr(X344,X346)
| ~ ssPv3(X346)
| ~ ssPv1(X344)
| ssPv2(X346) ),
inference(factor,[status(thm)],[clause39]) ).
cnf(c208,plain,
( ~ ssRr(X379,X378)
| ~ ssPv2(X379)
| ~ ssPv3(skf2(X378))
| ~ ssPv1(X378)
| ssPv2(skf2(X378)) ),
inference(resolution,[status(thm)],[c179,clause2]) ).
cnf(c207,plain,
( ~ ssRr(X376,skf3(X375))
| ~ ssPv2(X376)
| ~ ssPv3(X375)
| ~ ssPv1(skf3(X375))
| ssPv2(X375) ),
inference(resolution,[status(thm)],[c179,clause1]) ).
cnf(c223,plain,
( ~ ssPv2(skf3(skf3(X377)))
| ~ ssPv3(X377)
| ~ ssPv1(skf3(X377))
| ssPv2(X377) ),
inference(resolution,[status(thm)],[c207,clause1]) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X27,X29)
| ~ ssRr(X29,X28)
| ~ ssPv2(X29)
| ssPv4(X27)
| ssPv3(X28)
| ssPv4(X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c17,plain,
( ~ ssRr(X340,skf3(X341))
| ~ ssPv2(skf3(X341))
| ssPv4(X340)
| ssPv3(X341)
| ssPv4(skf3(X341)) ),
inference(resolution,[status(thm)],[clause11,clause1]) ).
cnf(c205,plain,
( ~ ssPv2(skf3(X372))
| ssPv4(skf3(skf3(X372)))
| ssPv3(X372)
| ssPv4(skf3(X372)) ),
inference(resolution,[status(thm)],[c17,clause1]) ).
cnf(c212,plain,
( ~ ssRr(X359,X358)
| ~ ssPv4(X358)
| ~ ssPv3(X358)
| ~ ssPv1(X358)
| ~ ssPv2(X359) ),
inference(factor,[status(thm)],[c200]) ).
cnf(c216,plain,
( ~ ssPv4(skf2(X366))
| ~ ssPv3(skf2(X366))
| ~ ssPv1(skf2(X366))
| ~ ssPv2(X366) ),
inference(resolution,[status(thm)],[c212,clause2]) ).
cnf(c214,plain,
( ~ ssRr(X361,X362)
| ~ ssPv4(X362)
| ~ ssPv3(skf2(X361))
| ~ ssPv1(X362)
| ~ ssPv2(X361) ),
inference(resolution,[status(thm)],[c200,clause2]) ).
cnf(c215,plain,
( ~ ssPv4(X360)
| ~ ssPv3(X360)
| ~ ssPv1(X360)
| ~ ssPv2(skf3(X360)) ),
inference(resolution,[status(thm)],[c212,clause1]) ).
cnf(c146,plain,
( ~ ssRr(X284,X282)
| ~ ssPv1(X284)
| ~ ssRr(X282,X283)
| ~ ssPv2(X283)
| ssPv4(X283)
| ssPv3(X282) ),
inference(factor,[status(thm)],[clause35]) ).
cnf(c176,plain,
( ~ ssRr(X339,X338)
| ~ ssPv1(X339)
| ~ ssPv2(skf2(X338))
| ssPv4(skf2(X338))
| ssPv3(X338) ),
inference(resolution,[status(thm)],[c146,clause2]) ).
cnf(c175,plain,
( ~ ssRr(X335,skf3(X336))
| ~ ssPv1(X335)
| ~ ssPv2(X336)
| ssPv4(X336)
| ssPv3(skf3(X336)) ),
inference(resolution,[status(thm)],[c146,clause1]) ).
cnf(c204,plain,
( ~ ssPv1(skf3(skf3(X337)))
| ~ ssPv2(X337)
| ssPv4(X337)
| ssPv3(skf3(X337)) ),
inference(resolution,[status(thm)],[c175,clause1]) ).
cnf(c192,plain,
( ~ ssRr(X330,X331)
| ~ ssPv4(X331)
| ~ ssPv1(skf2(X330))
| ~ ssPv1(X330)
| ssPv1(X331) ),
inference(resolution,[status(thm)],[c170,clause2]) ).
cnf(c193,plain,
( ~ ssRr(X320,X320)
| ~ ssPv2(X320)
| ~ ssRr(X319,X320)
| ssPv2(X319) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c199,plain,
( ~ ssRr(skf2(X323),skf2(X323))
| ~ ssPv2(skf2(X323))
| ssPv2(X323) ),
inference(resolution,[status(thm)],[c193,clause2]) ).
cnf(c198,plain,
( ~ ssRr(X322,X322)
| ~ ssPv2(X322)
| ssPv2(skf3(X322)) ),
inference(resolution,[status(thm)],[c193,clause1]) ).
cnf(c188,plain,
( ~ ssRr(X309,X309)
| ~ ssPv4(X309)
| ~ ssPv1(skf3(X309))
| ssPv2(X309) ),
inference(resolution,[status(thm)],[c183,clause1]) ).
cnf(c187,plain,
( ~ ssRr(X308,X308)
| ~ ssPv4(X308)
| ~ ssPv1(X308)
| ssPv2(X308) ),
inference(factor,[status(thm)],[c183]) ).
cnf(c157,plain,
( ~ ssRr(X297,X298)
| ~ ssPv2(X297)
| ~ ssRr(X298,X298)
| ~ ssPv4(X298)
| ssPv3(X298)
| ssPv1(X298) ),
inference(factor,[status(thm)],[clause36]) ).
cnf(c132,plain,
( ~ ssRr(X249,X250)
| ~ ssRr(X250,X248)
| ~ ssPv3(X248)
| ssPv2(X249)
| ssPv1(X248)
| ssPv2(X250) ),
inference(factor,[status(thm)],[clause33]) ).
cnf(c152,plain,
( ~ ssRr(X294,X293)
| ~ ssPv3(skf2(X293))
| ssPv2(X294)
| ssPv1(skf2(X293))
| ssPv2(X293) ),
inference(resolution,[status(thm)],[c132,clause2]) ).
cnf(c151,plain,
( ~ ssRr(X286,skf3(X287))
| ~ ssPv3(X287)
| ssPv2(X286)
| ssPv1(X287)
| ssPv2(skf3(X287)) ),
inference(resolution,[status(thm)],[c132,clause1]) ).
cnf(c177,plain,
( ~ ssPv3(X288)
| ssPv2(skf3(skf3(X288)))
| ssPv1(X288)
| ssPv2(skf3(X288)) ),
inference(resolution,[status(thm)],[c151,clause1]) ).
cnf(c168,plain,
( ~ ssPv1(skf3(X275))
| ssPv4(skf2(X275))
| ssPv2(skf2(X275))
| ssPv4(X275) ),
inference(resolution,[status(thm)],[c144,clause1]) ).
cnf(c166,plain,
( ~ ssRr(X272,X272)
| ~ ssPv1(X272)
| ssPv3(skf3(X272))
| ssPv4(X272) ),
inference(resolution,[status(thm)],[c161,clause1]) ).
cnf(c165,plain,
( ~ ssRr(X271,X271)
| ~ ssPv1(X271)
| ssPv3(X271)
| ssPv4(X271) ),
inference(factor,[status(thm)],[c161]) ).
cnf(c143,plain,
( ~ ssRr(X262,skf3(X263))
| ~ ssPv1(X262)
| ssPv4(X263)
| ssPv2(X263)
| ssPv4(skf3(X263)) ),
inference(resolution,[status(thm)],[c124,clause1]) ).
cnf(c160,plain,
( ~ ssPv1(skf3(skf3(X264)))
| ssPv4(X264)
| ssPv2(X264)
| ssPv4(skf3(X264)) ),
inference(resolution,[status(thm)],[c143,clause1]) ).
cnf(c154,plain,
( ~ ssRr(X259,X259)
| ~ ssPv2(X259)
| ~ ssPv1(X259)
| ssPv4(X259)
| ssPv1(skf3(X259)) ),
inference(resolution,[status(thm)],[c138,clause1]) ).
cnf(c128,plain,
( ~ ssRr(X245,X246)
| ~ ssPv2(X245)
| ~ ssRr(X246,X246)
| ssPv1(X246)
| ssPv2(X246)
| ssPv3(X246) ),
inference(factor,[status(thm)],[clause32]) ).
cnf(c116,plain,
( ~ ssRr(X185,X186)
| ~ ssPv4(X185)
| ~ ssPv1(X186)
| ~ ssPv3(X186)
| ssPv2(skf2(X186)) ),
inference(resolution,[status(thm)],[clause29,clause2]) ).
cnf(c118,plain,
( ~ ssPv4(X224)
| ~ ssPv1(skf2(X224))
| ~ ssPv3(skf2(X224))
| ssPv2(skf2(skf2(X224))) ),
inference(resolution,[status(thm)],[c116,clause2]) ).
cnf(c137,plain,
( ~ ssRr(X223,X223)
| ~ ssPv3(skf2(X223))
| ssPv2(X223)
| ssPv1(X223) ),
inference(resolution,[status(thm)],[c131,clause2]) ).
cnf(c135,plain,
( ~ ssRr(X222,X222)
| ~ ssPv3(X222)
| ssPv2(X222)
| ssPv1(X222) ),
inference(factor,[status(thm)],[c131]) ).
cnf(c109,plain,
( ~ ssRr(X179,X178)
| ~ ssPv1(X179)
| ~ ssPv2(X178)
| ~ ssPv3(X178)
| ssPv1(skf2(X178)) ),
inference(resolution,[status(thm)],[clause28,clause2]) ).
cnf(c113,plain,
( ~ ssPv1(X215)
| ~ ssPv2(skf2(X215))
| ~ ssPv3(skf2(X215))
| ssPv1(skf2(skf2(X215))) ),
inference(resolution,[status(thm)],[c109,clause2]) ).
cnf(c102,plain,
( ~ ssRr(X176,X175)
| ~ ssPv4(X176)
| ~ ssPv2(X175)
| ssPv1(skf2(X175))
| ssPv1(X175) ),
inference(resolution,[status(thm)],[clause27,clause2]) ).
cnf(c111,plain,
( ~ ssPv4(X214)
| ~ ssPv2(skf2(X214))
| ssPv1(skf2(skf2(X214)))
| ssPv1(skf2(X214)) ),
inference(resolution,[status(thm)],[c102,clause2]) ).
cnf(c99,plain,
( ~ ssRr(X169,X168)
| ~ ssPv2(X168)
| ~ ssPv2(X169)
| ssPv3(skf2(X169))
| ssPv1(X169) ),
inference(resolution,[status(thm)],[clause26,clause2]) ).
cnf(c105,plain,
( ~ ssPv2(X213)
| ~ ssPv2(skf3(X213))
| ssPv3(skf2(skf3(X213)))
| ssPv1(skf3(X213)) ),
inference(resolution,[status(thm)],[c99,clause1]) ).
cnf(c94,plain,
( ~ ssRr(X155,X154)
| ~ ssPv3(X155)
| ~ ssPv3(X154)
| ssPv3(skf2(X154))
| ssPv1(X154) ),
inference(resolution,[status(thm)],[clause25,clause2]) ).
cnf(c96,plain,
( ~ ssPv3(X212)
| ~ ssPv3(skf2(X212))
| ssPv3(skf2(skf2(X212)))
| ssPv1(skf2(X212)) ),
inference(resolution,[status(thm)],[c94,clause2]) ).
cnf(c86,plain,
( ~ ssRr(X148,X147)
| ~ ssPv2(X148)
| ~ ssPv3(X147)
| ssPv4(skf3(X147))
| ssPv1(X147) ),
inference(resolution,[status(thm)],[clause24,clause1]) ).
cnf(c91,plain,
( ~ ssPv2(X211)
| ~ ssPv3(skf2(X211))
| ssPv4(skf3(skf2(X211)))
| ssPv1(skf2(X211)) ),
inference(resolution,[status(thm)],[c86,clause2]) ).
cnf(c82,plain,
( ~ ssRr(X137,X138)
| ~ ssPv4(X138)
| ~ ssPv1(X137)
| ssPv4(skf2(X137))
| ssPv2(X137) ),
inference(resolution,[status(thm)],[clause23,clause2]) ).
cnf(c83,plain,
( ~ ssPv4(X206)
| ~ ssPv1(skf3(X206))
| ssPv4(skf2(skf3(X206)))
| ssPv2(skf3(X206)) ),
inference(resolution,[status(thm)],[c82,clause1]) ).
cnf(c72,plain,
( ~ ssRr(X123,X124)
| ~ ssPv4(X124)
| ~ ssPv3(X123)
| ssPv3(skf2(X123))
| ssPv2(X123) ),
inference(resolution,[status(thm)],[clause21,clause2]) ).
cnf(c75,plain,
( ~ ssPv4(X205)
| ~ ssPv3(skf3(X205))
| ssPv3(skf2(skf3(X205)))
| ssPv2(skf3(X205)) ),
inference(resolution,[status(thm)],[c72,clause1]) ).
cnf(c65,plain,
( ~ ssRr(X114,X113)
| ~ ssPv4(X114)
| ~ ssPv2(X113)
| ssPv2(skf2(X113))
| ssPv3(X113) ),
inference(resolution,[status(thm)],[clause20,clause2]) ).
cnf(c69,plain,
( ~ ssPv4(X204)
| ~ ssPv2(skf2(X204))
| ssPv2(skf2(skf2(X204)))
| ssPv3(skf2(X204)) ),
inference(resolution,[status(thm)],[c65,clause2]) ).
cnf(c62,plain,
( ~ ssRr(X111,X110)
| ~ ssPv1(X110)
| ~ ssPv4(X111)
| ssPv1(skf2(X111))
| ssPv3(X111) ),
inference(resolution,[status(thm)],[clause19,clause2]) ).
cnf(c66,plain,
( ~ ssPv1(X203)
| ~ ssPv4(skf3(X203))
| ssPv1(skf2(skf3(X203)))
| ssPv3(skf3(X203)) ),
inference(resolution,[status(thm)],[c62,clause1]) ).
cnf(c52,plain,
( ~ ssRr(X92,X93)
| ~ ssPv3(X93)
| ~ ssPv1(X92)
| ssPv4(skf2(X92))
| ssPv4(X92) ),
inference(resolution,[status(thm)],[clause17,clause2]) ).
cnf(c55,plain,
( ~ ssPv3(X202)
| ~ ssPv1(skf3(X202))
| ssPv4(skf2(skf3(X202)))
| ssPv4(skf3(X202)) ),
inference(resolution,[status(thm)],[c52,clause1]) ).
cnf(c45,plain,
( ~ ssRr(X82,X83)
| ~ ssPv2(X82)
| ~ ssPv3(X82)
| ssPv3(X83)
| ssPv1(skf2(X82)) ),
inference(resolution,[status(thm)],[clause16,clause2]) ).
cnf(c48,plain,
( ~ ssPv2(skf3(X197))
| ~ ssPv3(skf3(X197))
| ssPv3(X197)
| ssPv1(skf2(skf3(X197))) ),
inference(resolution,[status(thm)],[c45,clause1]) ).
cnf(c38,plain,
( ~ ssRr(X72,X73)
| ~ ssPv2(X72)
| ~ ssPv3(X72)
| ssPv4(X73)
| ssPv2(skf2(X72)) ),
inference(resolution,[status(thm)],[clause15,clause2]) ).
cnf(c41,plain,
( ~ ssPv2(skf3(X196))
| ~ ssPv3(skf3(X196))
| ssPv4(X196)
| ssPv2(skf2(skf3(X196))) ),
inference(resolution,[status(thm)],[c38,clause1]) ).
cnf(c31,plain,
( ~ ssRr(X63,X62)
| ~ ssPv1(X63)
| ssPv3(skf2(X62))
| ssPv2(X62)
| ssPv3(X62) ),
inference(resolution,[status(thm)],[clause14,clause2]) ).
cnf(c35,plain,
( ~ ssPv1(X195)
| ssPv3(skf2(skf2(X195)))
| ssPv2(skf2(X195))
| ssPv3(skf2(X195)) ),
inference(resolution,[status(thm)],[c31,clause2]) ).
cnf(c24,plain,
( ~ ssRr(X59,X60)
| ~ ssPv1(X60)
| ssPv1(skf2(X59))
| ssPv3(X59)
| ssPv4(X59) ),
inference(resolution,[status(thm)],[clause13,clause2]) ).
cnf(c32,plain,
( ~ ssPv1(X194)
| ssPv1(skf2(skf3(X194)))
| ssPv3(skf3(X194))
| ssPv4(skf3(X194)) ),
inference(resolution,[status(thm)],[c24,clause1]) ).
cnf(c21,plain,
( ~ ssRr(X53,X52)
| ~ ssPv4(X52)
| ssPv4(X53)
| ssPv3(skf2(X52))
| ssPv3(X52) ),
inference(resolution,[status(thm)],[clause12,clause2]) ).
cnf(c28,plain,
( ~ ssPv4(skf2(X193))
| ssPv4(X193)
| ssPv3(skf2(skf2(X193)))
| ssPv3(skf2(X193)) ),
inference(resolution,[status(thm)],[c21,clause2]) ).
cnf(c18,plain,
( ~ ssRr(X50,X49)
| ~ ssPv2(X49)
| ssPv4(X50)
| ssPv3(skf2(X49))
| ssPv4(X49) ),
inference(resolution,[status(thm)],[clause11,clause2]) ).
cnf(c26,plain,
( ~ ssPv2(skf2(X188))
| ssPv4(X188)
| ssPv3(skf2(skf2(X188)))
| ssPv4(skf2(X188)) ),
inference(resolution,[status(thm)],[c18,clause2]) ).
cnf(c117,plain,
( ~ ssPv4(skf3(X187))
| ~ ssPv1(X187)
| ~ ssPv3(X187)
| ssPv2(skf2(X187)) ),
inference(resolution,[status(thm)],[c116,clause1]) ).
cnf(c112,plain,
( ~ ssPv1(skf3(X183))
| ~ ssPv2(X183)
| ~ ssPv3(X183)
| ssPv1(skf2(X183)) ),
inference(resolution,[status(thm)],[c109,clause1]) ).
cnf(c110,plain,
( ~ ssPv4(skf3(X177))
| ~ ssPv2(X177)
| ssPv1(skf2(X177))
| ssPv1(X177) ),
inference(resolution,[status(thm)],[c102,clause1]) ).
cnf(c97,plain,
( ~ ssRr(X164,X165)
| ~ ssPv2(X165)
| ~ ssPv2(X164)
| ssPv3(X165)
| ssPv1(X164) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c104,plain,
( ~ ssPv2(skf2(X167))
| ~ ssPv2(X167)
| ssPv3(skf2(X167))
| ssPv1(X167) ),
inference(resolution,[status(thm)],[c97,clause2]) ).
cnf(c103,plain,
( ~ ssPv2(X166)
| ~ ssPv2(skf3(X166))
| ssPv3(X166)
| ssPv1(skf3(X166)) ),
inference(resolution,[status(thm)],[c97,clause1]) ).
cnf(c100,plain,
( ~ ssRr(X163,X163)
| ~ ssPv4(X163)
| ~ ssPv2(X163)
| ssPv1(X163) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c95,plain,
( ~ ssPv3(skf3(X156))
| ~ ssPv3(X156)
| ssPv3(skf2(X156))
| ssPv1(X156) ),
inference(resolution,[status(thm)],[c94,clause1]) ).
cnf(c85,plain,
( ~ ssRr(X143,X144)
| ~ ssPv2(X143)
| ~ ssPv3(X144)
| ssPv4(X143)
| ssPv1(X144) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c89,plain,
( ~ ssPv2(X146)
| ~ ssPv3(skf2(X146))
| ssPv4(X146)
| ssPv1(skf2(X146)) ),
inference(resolution,[status(thm)],[c85,clause2]) ).
cnf(c88,plain,
( ~ ssPv2(skf3(X145))
| ~ ssPv3(X145)
| ssPv4(skf3(X145))
| ssPv1(X145) ),
inference(resolution,[status(thm)],[c85,clause1]) ).
cnf(c79,plain,
( ~ ssRr(X131,X130)
| ~ ssPv1(skf2(X130))
| ~ ssPv1(X130)
| ssPv4(X131)
| ssPv2(X130) ),
inference(resolution,[status(thm)],[clause22,clause2]) ).
cnf(c77,plain,
( ~ ssRr(X129,X129)
| ~ ssPv1(X129)
| ssPv4(X129)
| ssPv2(X129) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c70,plain,
( ~ ssRr(X119,X120)
| ~ ssPv4(X120)
| ~ ssPv3(X119)
| ssPv3(X120)
| ssPv2(X119) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c74,plain,
( ~ ssPv4(skf2(X122))
| ~ ssPv3(X122)
| ssPv3(skf2(X122))
| ssPv2(X122) ),
inference(resolution,[status(thm)],[c70,clause2]) ).
cnf(c73,plain,
( ~ ssPv4(X121)
| ~ ssPv3(skf3(X121))
| ssPv3(X121)
| ssPv2(skf3(X121)) ),
inference(resolution,[status(thm)],[c70,clause1]) ).
cnf(c68,plain,
( ~ ssPv4(skf3(X115))
| ~ ssPv2(X115)
| ssPv2(skf2(X115))
| ssPv3(X115) ),
inference(resolution,[status(thm)],[c65,clause1]) ).
cnf(c59,plain,
( ~ ssRr(X100,X99)
| ~ ssPv2(skf2(X99))
| ~ ssPv4(X99)
| ssPv3(X100)
| ssPv3(X99) ),
inference(resolution,[status(thm)],[clause18,clause2]) ).
cnf(c57,plain,
( ~ ssRr(X97,X97)
| ~ ssPv2(X97)
| ~ ssPv4(X97)
| ssPv3(X97) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c50,plain,
( ~ ssRr(X89,X88)
| ~ ssPv3(X88)
| ~ ssPv1(X89)
| ssPv4(X88)
| ssPv4(X89) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c54,plain,
( ~ ssPv3(skf2(X91))
| ~ ssPv1(X91)
| ssPv4(skf2(X91))
| ssPv4(X91) ),
inference(resolution,[status(thm)],[c50,clause2]) ).
cnf(c53,plain,
( ~ ssPv3(X90)
| ~ ssPv1(skf3(X90))
| ssPv4(X90)
| ssPv4(skf3(X90)) ),
inference(resolution,[status(thm)],[c50,clause1]) ).
cnf(c43,plain,
( ~ ssRr(X78,X79)
| ~ ssPv2(X78)
| ~ ssPv3(X78)
| ssPv3(X79)
| ssPv1(X79) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c47,plain,
( ~ ssPv2(X81)
| ~ ssPv3(X81)
| ssPv3(skf2(X81))
| ssPv1(skf2(X81)) ),
inference(resolution,[status(thm)],[c43,clause2]) ).
cnf(c46,plain,
( ~ ssPv2(skf3(X80))
| ~ ssPv3(skf3(X80))
| ssPv3(X80)
| ssPv1(X80) ),
inference(resolution,[status(thm)],[c43,clause1]) ).
cnf(c36,plain,
( ~ ssRr(X68,X69)
| ~ ssPv2(X68)
| ~ ssPv3(X68)
| ssPv4(X69)
| ssPv2(X69) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c40,plain,
( ~ ssPv2(X71)
| ~ ssPv3(X71)
| ssPv4(skf2(X71))
| ssPv2(skf2(X71)) ),
inference(resolution,[status(thm)],[c36,clause2]) ).
cnf(c39,plain,
( ~ ssPv2(skf3(X70))
| ~ ssPv3(skf3(X70))
| ssPv4(X70)
| ssPv2(X70) ),
inference(resolution,[status(thm)],[c36,clause1]) ).
cnf(c34,plain,
( ~ ssPv1(skf3(X67))
| ssPv3(skf2(X67))
| ssPv2(X67)
| ssPv3(X67) ),
inference(resolution,[status(thm)],[c31,clause1]) ).
cnf(c27,plain,
( ~ ssPv4(X58)
| ssPv4(skf3(X58))
| ssPv3(skf2(X58))
| ssPv3(X58) ),
inference(resolution,[status(thm)],[c21,clause1]) ).
cnf(c29,plain,
( ~ ssRr(X57,X57)
| ~ ssPv1(X57)
| ssPv3(X57)
| ssPv2(X57) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c25,plain,
( ~ ssPv2(X51)
| ssPv4(skf3(X51))
| ssPv3(skf2(X51))
| ssPv4(X51) ),
inference(resolution,[status(thm)],[c18,clause1]) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X25,X26)
| ~ ssPv3(X26)
| ~ ssPv1(X25)
| ~ ssPv2(X25)
| ssPv3(X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c14,plain,
( ~ ssPv3(X48)
| ~ ssPv1(skf3(X48))
| ~ ssPv2(skf3(X48))
| ssPv3(skf3(X48)) ),
inference(resolution,[status(thm)],[clause10,clause1]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X22,X23)
| ~ ssPv4(X22)
| ~ ssPv1(X23)
| ~ ssPv3(X23)
| ssPv4(X23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c13,plain,
( ~ ssPv4(X42)
| ~ ssPv1(skf2(X42))
| ~ ssPv3(skf2(X42))
| ssPv4(skf2(X42)) ),
inference(resolution,[status(thm)],[clause9,clause2]) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X18,X19)
| ~ ssPv2(X18)
| ~ ssPv3(X18)
| ssPv1(X19)
| ssPv1(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c10,plain,
( ~ ssPv2(skf3(X41))
| ~ ssPv3(skf3(X41))
| ssPv1(X41)
| ssPv1(skf3(X41)) ),
inference(resolution,[status(thm)],[clause8,clause1]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X16,X17)
| ~ ssPv3(X16)
| ~ ssPv1(X17)
| ssPv2(X17)
| ssPv3(X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c9,plain,
( ~ ssPv3(X40)
| ~ ssPv1(skf2(X40))
| ssPv2(skf2(X40))
| ssPv3(skf2(X40)) ),
inference(resolution,[status(thm)],[clause7,clause2]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X13,X14)
| ~ ssPv3(X14)
| ~ ssPv3(X13)
| ssPv2(X13)
| ssPv4(X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c6,plain,
( ~ ssPv3(X39)
| ~ ssPv3(skf3(X39))
| ssPv2(skf3(X39))
| ssPv4(skf3(X39)) ),
inference(resolution,[status(thm)],[clause6,clause1]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X9,X10)
| ~ ssPv1(X10)
| ~ ssPv3(X10)
| ssPv2(X9)
| ssPv2(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c5,plain,
( ~ ssPv1(skf2(X34))
| ~ ssPv3(skf2(X34))
| ssPv2(X34)
| ssPv2(skf2(X34)) ),
inference(resolution,[status(thm)],[clause5,clause2]) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X7,X8)
| ~ ssPv2(X7)
| ~ ssPv2(X8)
| ssPv3(X8)
| ssPv4(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c3,plain,
( ~ ssPv2(X33)
| ~ ssPv2(skf2(X33))
| ssPv3(skf2(X33))
| ssPv4(skf2(X33)) ),
inference(resolution,[status(thm)],[clause4,clause2]) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssPv2(X4)
| ssPv4(X5)
| ssPv3(X4)
| ssPv4(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c0,plain,
( ~ ssPv2(skf3(X32))
| ssPv4(X32)
| ssPv3(skf3(X32))
| ssPv4(skf3(X32)) ),
inference(resolution,[status(thm)],[clause3,clause1]) ).
cnf(c15,plain,
( ~ ssPv3(skf2(X31))
| ~ ssPv1(X31)
| ~ ssPv2(X31)
| ssPv3(X31) ),
inference(resolution,[status(thm)],[clause10,clause2]) ).
cnf(c16,plain,
( ~ ssRr(X30,X30)
| ~ ssPv2(X30)
| ssPv4(X30)
| ssPv3(X30) ),
inference(factor,[status(thm)],[clause11]) ).
cnf(c12,plain,
( ~ ssPv4(skf3(X24))
| ~ ssPv1(X24)
| ~ ssPv3(X24)
| ssPv4(X24) ),
inference(resolution,[status(thm)],[clause9,clause1]) ).
cnf(c11,plain,
( ~ ssPv2(X21)
| ~ ssPv3(X21)
| ssPv1(skf2(X21))
| ssPv1(X21) ),
inference(resolution,[status(thm)],[clause8,clause2]) ).
cnf(c8,plain,
( ~ ssPv3(skf3(X20))
| ~ ssPv1(X20)
| ssPv2(X20)
| ssPv3(X20) ),
inference(resolution,[status(thm)],[clause7,clause1]) ).
cnf(c7,plain,
( ~ ssPv3(skf2(X15))
| ~ ssPv3(X15)
| ssPv2(X15)
| ssPv4(X15) ),
inference(resolution,[status(thm)],[clause6,clause2]) ).
cnf(c4,plain,
( ~ ssPv1(X12)
| ~ ssPv3(X12)
| ssPv2(skf3(X12))
| ssPv2(X12) ),
inference(resolution,[status(thm)],[clause5,clause1]) ).
cnf(c2,plain,
( ~ ssPv2(skf3(X11))
| ~ ssPv2(X11)
| ssPv3(X11)
| ssPv4(X11) ),
inference(resolution,[status(thm)],[clause4,clause1]) ).
cnf(c1,plain,
( ~ ssPv2(X6)
| ssPv4(skf2(X6))
| ssPv3(X6)
| ssPv4(X6) ),
inference(resolution,[status(thm)],[clause3,clause2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SYN785-1 : TPTP v8.1.2. Released v2.5.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n020.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 20:00:08 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.81/0.98 % Version: 1.5
% 0.81/0.98 % SZS status Satisfiable
% 0.81/0.98 % SZS output start Saturation
% See solution above
% 0.84/1.00
% 0.84/1.00 % Initial clauses : 42
% 0.84/1.00 % Processed clauses : 318
% 0.84/1.00 % Factors computed : 86
% 0.84/1.00 % Resolvents computed: 270
% 0.84/1.00 % Tautologies deleted: 33
% 0.84/1.00 % Forward subsumed : 47
% 0.84/1.00 % Backward subsumed : 1
% 0.84/1.00 % -------- CPU Time ---------
% 0.84/1.00 % User time : 0.621 s
% 0.84/1.00 % System time : 0.015 s
% 0.84/1.00 % Total time : 0.636 s
%------------------------------------------------------------------------------