%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN890-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:49:31 EDT 2024
% Result : Unsatisfiable 5.12s 5.34s
% Output : Refutation 5.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 175
% Number of leaves : 32
% Syntax : Number of clauses : 346 ( 25 unt; 119 nHn; 60 RR)
% Number of literals : 2415 ( 0 equ;1904 neg)
% Maximal clause size : 19 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 2 prp; 0-15 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 3105 (1446 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssNder1_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause2,negated_conjecture,
( ~ ssNder1_0
| ssNder1_1r1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(c0,plain,
ssNder1_1r1(X3),
inference(resolution,[status(thm)],[clause2,clause1]) ).
cnf(clause3,negated_conjecture,
( ~ ssNder1_1r1(X4)
| ~ ssNder1_0
| ssNder1_2r1r1(X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c1,plain,
( ~ ssNder1_0
| ssNder1_2r1r1(X7,X6) ),
inference(resolution,[status(thm)],[clause3,c0]) ).
cnf(c2,plain,
ssNder1_2r1r1(X12,X11),
inference(resolution,[status(thm)],[c1,clause1]) ).
cnf(clause4,negated_conjecture,
( ~ ssNder1_2r1r1(X8,X9)
| ~ ssNder1_1r1(X8)
| ~ ssNder1_0
| ssNder1_3r1r1r1(X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c3,plain,
( ~ ssNder1_1r1(X14)
| ~ ssNder1_0
| ssNder1_3r1r1r1(X14,X15,X13) ),
inference(resolution,[status(thm)],[c2,clause4]) ).
cnf(c4,plain,
( ~ ssNder1_0
| ssNder1_3r1r1r1(X18,X16,X17) ),
inference(resolution,[status(thm)],[c3,c0]) ).
cnf(c5,plain,
ssNder1_3r1r1r1(X19,X21,X20),
inference(resolution,[status(thm)],[c4,clause1]) ).
cnf(clause5,negated_conjecture,
( ~ ssNder1_3r1r1r1(X23,X24,X25)
| ~ ssNder1_2r1r1(X23,X24)
| ~ ssNder1_1r1(X23)
| ~ ssNder1_0
| ssNder1_4r1r1r1r1(X23,X24,X25,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c6,plain,
( ~ ssNder1_2r1r1(X33,X31)
| ~ ssNder1_1r1(X33)
| ~ ssNder1_0
| ssNder1_4r1r1r1r1(X33,X31,X32,X30) ),
inference(resolution,[status(thm)],[clause5,c5]) ).
cnf(c8,plain,
( ~ ssNder1_1r1(X35)
| ~ ssNder1_0
| ssNder1_4r1r1r1r1(X35,X37,X36,X34) ),
inference(resolution,[status(thm)],[c6,c2]) ).
cnf(c9,plain,
( ~ ssNder1_0
| ssNder1_4r1r1r1r1(X41,X38,X40,X39) ),
inference(resolution,[status(thm)],[c8,c0]) ).
cnf(c10,plain,
ssNder1_4r1r1r1r1(X44,X45,X42,X43),
inference(resolution,[status(thm)],[c9,clause1]) ).
cnf(clause8,negated_conjecture,
( ~ ssNder1_4r1r1r1r1(X68,X66,X70,X69)
| ~ ssNder1_3r1r1r1(X68,X66,X70)
| ~ ssNder1_2r1r1(X68,X66)
| ~ ssNder1_1r1(X68)
| ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X68,X66,X70,X69,X67) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c14,plain,
( ~ ssNder1_3r1r1r1(X71,X72,X74)
| ~ ssNder1_2r1r1(X71,X72)
| ~ ssNder1_1r1(X71)
| ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X71,X72,X74,X75,X73) ),
inference(resolution,[status(thm)],[clause8,c10]) ).
cnf(c15,plain,
( ~ ssNder1_2r1r1(X83,X81)
| ~ ssNder1_1r1(X83)
| ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X83,X81,X82,X84,X85) ),
inference(resolution,[status(thm)],[c14,c5]) ).
cnf(c17,plain,
( ~ ssNder1_1r1(X87)
| ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X87,X89,X90,X88,X86) ),
inference(resolution,[status(thm)],[c15,c2]) ).
cnf(c18,plain,
( ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X92,X93,X95,X94,X91) ),
inference(resolution,[status(thm)],[c17,c0]) ).
cnf(c19,plain,
ssNder1_5r1r1r1r1r1(X96,X97,X99,X100,X98),
inference(resolution,[status(thm)],[c18,clause1]) ).
cnf(clause13,negated_conjecture,
( ~ ssPv14_7r1r1r1r1r1r1r1(X176,X174,X178,X177,X175,X173,skc27)
| ~ ssNder1_5r1r1r1r1r1(X176,X174,X178,X177,X175)
| ~ ssNder1_4r1r1r1r1(X176,X174,X178,X177)
| ~ ssNder1_3r1r1r1(X176,X174,X178)
| ~ ssNder1_2r1r1(X176,X174)
| ~ ssNder1_1r1(X176)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(clause10,negated_conjecture,
( ~ ssPv15_6r1r1r1r1r1r1(X108,X106,X110,X109,X107,skc29)
| ~ ssNder1_4r1r1r1r1(X108,X106,X110,X109)
| ~ ssNder1_3r1r1r1(X108,X106,X110)
| ~ ssNder1_2r1r1(X108,X106)
| ~ ssNder1_1r1(X108)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(clause7,negated_conjecture,
( ~ ssPv16_5r1r1r1r1r1(X51,X52,X53,X50,skc31)
| ~ ssNder1_3r1r1r1(X51,X52,X53)
| ~ ssNder1_2r1r1(X51,X52)
| ~ ssNder1_1r1(X51)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(clause11,negated_conjecture,
( ~ ssNder1_5r1r1r1r1r1(X134,X132,X136,X135,X133)
| ~ ssNder1_4r1r1r1r1(X134,X132,X136,X135)
| ~ ssNder1_3r1r1r1(X134,X132,X136)
| ~ ssNder1_2r1r1(X134,X132)
| ~ ssNder1_1r1(X134)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X134,X132,X136,X135,X133,X131) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c24,plain,
( ~ ssNder1_4r1r1r1r1(X147,X144,X145,X148)
| ~ ssNder1_3r1r1r1(X147,X144,X145)
| ~ ssNder1_2r1r1(X147,X144)
| ~ ssNder1_1r1(X147)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X147,X144,X145,X148,X146,X143) ),
inference(resolution,[status(thm)],[clause11,c19]) ).
cnf(c26,plain,
( ~ ssNder1_3r1r1r1(X151,X152,X153)
| ~ ssNder1_2r1r1(X151,X152)
| ~ ssNder1_1r1(X151)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X151,X152,X153,X154,X150,X149) ),
inference(resolution,[status(thm)],[c24,c10]) ).
cnf(c27,plain,
( ~ ssNder1_2r1r1(X158,X156)
| ~ ssNder1_1r1(X158)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X158,X156,X157,X155,X159,X160) ),
inference(resolution,[status(thm)],[c26,c5]) ).
cnf(c28,plain,
( ~ ssNder1_1r1(X162)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X162,X164,X163,X166,X165,X161) ),
inference(resolution,[status(thm)],[c27,c2]) ).
cnf(c29,plain,
( ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X168,X172,X169,X167,X171,X170) ),
inference(resolution,[status(thm)],[c28,c0]) ).
cnf(c30,plain,
ssNder1_6r1r1r1r1r1r1(X180,X181,X183,X179,X184,X182),
inference(resolution,[status(thm)],[c29,clause1]) ).
cnf(clause14,negated_conjecture,
( ~ ssNder1_6r1r1r1r1r1r1(X213,X210,X215,X214,X212,X209)
| ~ ssNder1_5r1r1r1r1r1(X213,X210,X215,X214,X212)
| ~ ssNder1_4r1r1r1r1(X213,X210,X215,X214)
| ~ ssNder1_3r1r1r1(X213,X210,X215)
| ~ ssNder1_2r1r1(X213,X210)
| ~ ssNder1_1r1(X213)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X213,X210,X215,X214,X212,X209,X211) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c35,plain,
( ~ ssNder1_5r1r1r1r1r1(X232,X228,X231,X234,X230)
| ~ ssNder1_4r1r1r1r1(X232,X228,X231,X234)
| ~ ssNder1_3r1r1r1(X232,X228,X231)
| ~ ssNder1_2r1r1(X232,X228)
| ~ ssNder1_1r1(X232)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X232,X228,X231,X234,X230,X229,X233) ),
inference(resolution,[status(thm)],[clause14,c30]) ).
cnf(c37,plain,
( ~ ssNder1_4r1r1r1r1(X240,X236,X237,X241)
| ~ ssNder1_3r1r1r1(X240,X236,X237)
| ~ ssNder1_2r1r1(X240,X236)
| ~ ssNder1_1r1(X240)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X240,X236,X237,X241,X238,X235,X239) ),
inference(resolution,[status(thm)],[c35,c19]) ).
cnf(c38,plain,
( ~ ssNder1_3r1r1r1(X243,X244,X246)
| ~ ssNder1_2r1r1(X243,X244)
| ~ ssNder1_1r1(X243)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X243,X244,X246,X247,X248,X242,X245) ),
inference(resolution,[status(thm)],[c37,c10]) ).
cnf(c39,plain,
( ~ ssNder1_2r1r1(X259,X256)
| ~ ssNder1_1r1(X259)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X259,X256,X258,X257,X262,X261,X260) ),
inference(resolution,[status(thm)],[c38,c5]) ).
cnf(c41,plain,
( ~ ssNder1_1r1(X265)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X265,X266,X263,X269,X264,X267,X268) ),
inference(resolution,[status(thm)],[c39,c2]) ).
cnf(c42,plain,
( ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X270,X276,X271,X274,X272,X275,X273) ),
inference(resolution,[status(thm)],[c41,c0]) ).
cnf(c43,plain,
ssNder1_7r1r1r1r1r1r1r1(X277,X280,X279,X282,X278,X283,X281),
inference(resolution,[status(thm)],[c42,clause1]) ).
cnf(clause15,negated_conjecture,
( ~ ssNder1_6r1r1r1r1r1r1(X253,X250,X255,X254,X252,X249)
| ~ ssNder1_5r1r1r1r1r1(X253,X250,X255,X254,X252)
| ~ ssNder1_4r1r1r1r1(X253,X250,X255,X254)
| ~ ssNder1_3r1r1r1(X253,X250,X255)
| ~ ssNder1_2r1r1(X253,X250)
| ~ ssNder1_1r1(X253)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X253,X250,X255,X254,X252,X249,X251,skc24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c40,plain,
( ~ ssNder1_5r1r1r1r1r1(X289,X284,X287,X290,X286)
| ~ ssNder1_4r1r1r1r1(X289,X284,X287,X290)
| ~ ssNder1_3r1r1r1(X289,X284,X287)
| ~ ssNder1_2r1r1(X289,X284)
| ~ ssNder1_1r1(X289)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X289,X284,X287,X290,X286,X285,X288,skc24) ),
inference(resolution,[status(thm)],[clause15,c30]) ).
cnf(c44,plain,
( ~ ssNder1_4r1r1r1r1(X303,X298,X299,X304)
| ~ ssNder1_3r1r1r1(X303,X298,X299)
| ~ ssNder1_2r1r1(X303,X298)
| ~ ssNder1_1r1(X303)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X303,X298,X299,X304,X301,X302,X300,skc24) ),
inference(resolution,[status(thm)],[c40,c19]) ).
cnf(c45,plain,
( ~ ssNder1_3r1r1r1(X306,X307,X310)
| ~ ssNder1_2r1r1(X306,X307)
| ~ ssNder1_1r1(X306)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X306,X307,X310,X311,X308,X309,X305,skc24) ),
inference(resolution,[status(thm)],[c44,c10]) ).
cnf(c46,plain,
( ~ ssNder1_2r1r1(X316,X312)
| ~ ssNder1_1r1(X316)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X316,X312,X315,X317,X318,X314,X313,skc24) ),
inference(resolution,[status(thm)],[c45,c5]) ).
cnf(c47,plain,
( ~ ssNder1_1r1(X320)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X320,X321,X325,X324,X319,X322,X323,skc24) ),
inference(resolution,[status(thm)],[c46,c2]) ).
cnf(c48,plain,
( ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X327,X332,X329,X326,X330,X331,X328,skc24) ),
inference(resolution,[status(thm)],[c47,c0]) ).
cnf(c49,plain,
ssPv13_8r1r1r1r1r1r1r1r1(X346,X342,X343,X344,X341,X345,X347,skc24),
inference(resolution,[status(thm)],[c48,clause1]) ).
cnf(clause20,negated_conjecture,
( ~ ssNder1_7r1r1r1r1r1r1r1(X463,X460,X466,X465,X462,X459,X461)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X463,X460,X466,X465,X462,X459,X461,X464)
| ~ ssNder1_6r1r1r1r1r1r1(X463,X460,X466,X465,X462,X459)
| ~ ssNder1_5r1r1r1r1r1(X463,X460,X466,X465,X462)
| ~ ssNder1_4r1r1r1r1(X463,X460,X466,X465)
| ~ ssNder1_3r1r1r1(X463,X460,X466)
| ~ ssNder1_2r1r1(X463,X460)
| ~ ssNder1_1r1(X463)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(X463,X460,X466,X465,X462)
| ssPv19_2r1r1(X463,X460)
| ssPv20_1r1(X463) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c65,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X560,X562,X558,X564,X563,X559,X561)
| ~ ssNder1_6r1r1r1r1r1r1(X560,X562,X558,X564,X563,X559)
| ~ ssNder1_5r1r1r1r1r1(X560,X562,X558,X564,X563)
| ~ ssNder1_4r1r1r1r1(X560,X562,X558,X564)
| ~ ssNder1_3r1r1r1(X560,X562,X558)
| ~ ssNder1_2r1r1(X560,X562)
| ~ ssNder1_1r1(X560)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(X560,X562,X558,X564,X563)
| ssPv19_2r1r1(X560,X562)
| ssPv20_1r1(X560) ),
inference(resolution,[status(thm)],[clause20,c49]) ).
cnf(c75,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X577,X576,X578,X579,X574,X575)
| ~ ssNder1_5r1r1r1r1r1(X577,X576,X578,X579,X574)
| ~ ssNder1_4r1r1r1r1(X577,X576,X578,X579)
| ~ ssNder1_3r1r1r1(X577,X576,X578)
| ~ ssNder1_2r1r1(X577,X576)
| ~ ssNder1_1r1(X577)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(X577,X576,X578,X579,X574)
| ssPv19_2r1r1(X577,X576)
| ssPv20_1r1(X577) ),
inference(resolution,[status(thm)],[c65,c43]) ).
cnf(c76,plain,
( ~ ssNder1_5r1r1r1r1r1(X583,X580,X582,X584,X581)
| ~ ssNder1_4r1r1r1r1(X583,X580,X582,X584)
| ~ ssNder1_3r1r1r1(X583,X580,X582)
| ~ ssNder1_2r1r1(X583,X580)
| ~ ssNder1_1r1(X583)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(X583,X580,X582,X584,X581)
| ssPv19_2r1r1(X583,X580)
| ssPv20_1r1(X583) ),
inference(resolution,[status(thm)],[c75,c30]) ).
cnf(c77,plain,
( ~ ssNder1_4r1r1r1r1(X588,X585,X586,X589)
| ~ ssNder1_3r1r1r1(X588,X585,X586)
| ~ ssNder1_2r1r1(X588,X585)
| ~ ssNder1_1r1(X588)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(X588,X585,X586,X589,X587)
| ssPv19_2r1r1(X588,X585)
| ssPv20_1r1(X588) ),
inference(resolution,[status(thm)],[c76,c19]) ).
cnf(c78,plain,
( ~ ssNder1_3r1r1r1(X591,X592,X593)
| ~ ssNder1_2r1r1(X591,X592)
| ~ ssNder1_1r1(X591)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(X591,X592,X593,X594,X590)
| ssPv19_2r1r1(X591,X592)
| ssPv20_1r1(X591) ),
inference(resolution,[status(thm)],[c77,c10]) ).
cnf(c79,plain,
( ~ ssNder1_2r1r1(X598,X596)
| ~ ssNder1_1r1(X598)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(X598,X596,X597,X599,X595)
| ssPv19_2r1r1(X598,X596)
| ssPv20_1r1(X598) ),
inference(resolution,[status(thm)],[c78,c5]) ).
cnf(c80,plain,
( ~ ssNder1_1r1(X611)
| ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(X611,X613,X612,X610,X609)
| ssPv19_2r1r1(X611,X613)
| ssPv20_1r1(X611) ),
inference(resolution,[status(thm)],[c79,c2]) ).
cnf(c82,plain,
( ~ ssNder1_0
| ssPv16_5r1r1r1r1r1(X615,X617,X614,X616,X618)
| ssPv19_2r1r1(X615,X617)
| ssPv20_1r1(X615) ),
inference(resolution,[status(thm)],[c80,c0]) ).
cnf(c83,plain,
( ssPv16_5r1r1r1r1r1(X623,X619,X620,X622,X621)
| ssPv19_2r1r1(X623,X619)
| ssPv20_1r1(X623) ),
inference(resolution,[status(thm)],[c82,clause1]) ).
cnf(c84,plain,
( ssPv19_2r1r1(X626,X625)
| ssPv20_1r1(X626)
| ~ ssNder1_3r1r1r1(X626,X625,X624)
| ~ ssNder1_2r1r1(X626,X625)
| ~ ssNder1_1r1(X626)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c83,clause7]) ).
cnf(c86,plain,
( ssPv19_2r1r1(X628,X627)
| ssPv20_1r1(X628)
| ~ ssNder1_2r1r1(X628,X627)
| ~ ssNder1_1r1(X628)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c84,c5]) ).
cnf(c87,plain,
( ssPv19_2r1r1(X640,X641)
| ssPv20_1r1(X640)
| ~ ssNder1_1r1(X640)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c86,c2]) ).
cnf(c88,plain,
( ssPv19_2r1r1(X643,X642)
| ssPv20_1r1(X643)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c87,c0]) ).
cnf(c89,plain,
( ssPv19_2r1r1(X644,X645)
| ssPv20_1r1(X644) ),
inference(resolution,[status(thm)],[c88,clause1]) ).
cnf(clause17,negated_conjecture,
( ~ ssNder1_7r1r1r1r1r1r1r1(X337,X334,X340,X339,X336,X333,X335)
| ~ ssNder1_6r1r1r1r1r1r1(X337,X334,X340,X339,X336,X333)
| ~ ssNder1_5r1r1r1r1r1(X337,X334,X340,X339,X336)
| ~ ssNder1_4r1r1r1r1(X337,X334,X340,X339)
| ~ ssNder1_3r1r1r1(X337,X334,X340)
| ~ ssNder1_2r1r1(X337,X334)
| ~ ssNder1_1r1(X337)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X337,X334,X340,X339,X336,X333,X335,X338) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c50,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X353,X350,X354,X355,X348,X349)
| ~ ssNder1_5r1r1r1r1r1(X353,X350,X354,X355,X348)
| ~ ssNder1_4r1r1r1r1(X353,X350,X354,X355)
| ~ ssNder1_3r1r1r1(X353,X350,X354)
| ~ ssNder1_2r1r1(X353,X350)
| ~ ssNder1_1r1(X353)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X353,X350,X354,X355,X348,X349,X352,X351) ),
inference(resolution,[status(thm)],[clause17,c43]) ).
cnf(c51,plain,
( ~ ssNder1_5r1r1r1r1r1(X362,X356,X359,X363,X358)
| ~ ssNder1_4r1r1r1r1(X362,X356,X359,X363)
| ~ ssNder1_3r1r1r1(X362,X356,X359)
| ~ ssNder1_2r1r1(X362,X356)
| ~ ssNder1_1r1(X362)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X362,X356,X359,X363,X358,X357,X360,X361) ),
inference(resolution,[status(thm)],[c50,c30]) ).
cnf(c52,plain,
( ~ ssNder1_4r1r1r1r1(X370,X364,X366,X371)
| ~ ssNder1_3r1r1r1(X370,X364,X366)
| ~ ssNder1_2r1r1(X370,X364)
| ~ ssNder1_1r1(X370)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X370,X364,X366,X371,X369,X368,X367,X365) ),
inference(resolution,[status(thm)],[c51,c19]) ).
cnf(c53,plain,
( ~ ssNder1_3r1r1r1(X373,X374,X377)
| ~ ssNder1_2r1r1(X373,X374)
| ~ ssNder1_1r1(X373)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X373,X374,X377,X378,X379,X375,X376,X372) ),
inference(resolution,[status(thm)],[c52,c10]) ).
cnf(c54,plain,
( ~ ssNder1_2r1r1(X390,X387)
| ~ ssNder1_1r1(X390)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X390,X387,X389,X391,X394,X393,X388,X392) ),
inference(resolution,[status(thm)],[c53,c5]) ).
cnf(c56,plain,
( ~ ssNder1_1r1(X397)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X397,X400,X402,X398,X396,X399,X395,X401) ),
inference(resolution,[status(thm)],[c54,c2]) ).
cnf(c57,plain,
( ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X403,X405,X410,X409,X407,X404,X406,X408) ),
inference(resolution,[status(thm)],[c56,c0]) ).
cnf(c58,plain,
ssNder1_8r1r1r1r1r1r1r1r1(X418,X411,X415,X417,X413,X412,X416,X414),
inference(resolution,[status(thm)],[c57,clause1]) ).
cnf(clause19,negated_conjecture,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X430,X426,X433,X432,X429,X425,X428,X431)
| ~ ssNder1_7r1r1r1r1r1r1r1(X430,X426,X433,X432,X429,X425,X428)
| ~ ssNder1_6r1r1r1r1r1r1(X430,X426,X433,X432,X429,X425)
| ~ ssNder1_5r1r1r1r1r1(X430,X426,X433,X432,X429)
| ~ ssNder1_4r1r1r1r1(X430,X426,X433,X432)
| ~ ssNder1_3r1r1r1(X430,X426,X433)
| ~ ssNder1_2r1r1(X430,X426)
| ~ ssNder1_1r1(X430)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X430,X426,X433,X432,X429,X425,X428,X431,X427) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c60,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X471,X470,X473,X472,X475,X468,X469)
| ~ ssNder1_6r1r1r1r1r1r1(X471,X470,X473,X472,X475,X468)
| ~ ssNder1_5r1r1r1r1r1(X471,X470,X473,X472,X475)
| ~ ssNder1_4r1r1r1r1(X471,X470,X473,X472)
| ~ ssNder1_3r1r1r1(X471,X470,X473)
| ~ ssNder1_2r1r1(X471,X470)
| ~ ssNder1_1r1(X471)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X471,X470,X473,X472,X475,X468,X469,X467,X474) ),
inference(resolution,[status(thm)],[clause19,c58]) ).
cnf(c66,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X481,X478,X483,X484,X476,X477)
| ~ ssNder1_5r1r1r1r1r1(X481,X478,X483,X484,X476)
| ~ ssNder1_4r1r1r1r1(X481,X478,X483,X484)
| ~ ssNder1_3r1r1r1(X481,X478,X483)
| ~ ssNder1_2r1r1(X481,X478)
| ~ ssNder1_1r1(X481)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X481,X478,X483,X484,X476,X477,X479,X482,X480) ),
inference(resolution,[status(thm)],[c60,c43]) ).
cnf(c67,plain,
( ~ ssNder1_5r1r1r1r1r1(X491,X487,X490,X493,X489)
| ~ ssNder1_4r1r1r1r1(X491,X487,X490,X493)
| ~ ssNder1_3r1r1r1(X491,X487,X490)
| ~ ssNder1_2r1r1(X491,X487)
| ~ ssNder1_1r1(X491)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X491,X487,X490,X493,X489,X488,X492,X486,X485) ),
inference(resolution,[status(thm)],[c66,c30]) ).
cnf(c68,plain,
( ~ ssNder1_4r1r1r1r1(X501,X495,X497,X502)
| ~ ssNder1_3r1r1r1(X501,X495,X497)
| ~ ssNder1_2r1r1(X501,X495)
| ~ ssNder1_1r1(X501)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X501,X495,X497,X502,X499,X494,X496,X500,X498) ),
inference(resolution,[status(thm)],[c67,c19]) ).
cnf(c69,plain,
( ~ ssNder1_3r1r1r1(X507,X508,X509)
| ~ ssNder1_2r1r1(X507,X508)
| ~ ssNder1_1r1(X507)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X507,X508,X509,X510,X505,X511,X503,X504,X506) ),
inference(resolution,[status(thm)],[c68,c10]) ).
cnf(c70,plain,
( ~ ssNder1_2r1r1(X526,X523)
| ~ ssNder1_1r1(X526)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X526,X523,X525,X530,X522,X528,X529,X524,X527) ),
inference(resolution,[status(thm)],[c69,c5]) ).
cnf(c71,plain,
( ~ ssNder1_1r1(X534)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X534,X536,X533,X532,X531,X537,X538,X539,X535) ),
inference(resolution,[status(thm)],[c70,c2]) ).
cnf(c72,plain,
( ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X540,X547,X541,X544,X545,X542,X543,X548,X546) ),
inference(resolution,[status(thm)],[c71,c0]) ).
cnf(c73,plain,
ssNder1_9r1r1r1r1r1r1r1r1r1(X555,X550,X557,X549,X551,X554,X553,X552,X556),
inference(resolution,[status(thm)],[c72,clause1]) ).
cnf(clause21,negated_conjecture,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X517,X513,X520,X519,X516,X512,X515,X518,X514)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X517,X513,X520,X519,X516,X512,X515,X518)
| ~ ssNder1_7r1r1r1r1r1r1r1(X517,X513,X520,X519,X516,X512,X515)
| ~ ssNder1_6r1r1r1r1r1r1(X517,X513,X520,X519,X516,X512)
| ~ ssNder1_5r1r1r1r1r1(X517,X513,X520,X519,X516)
| ~ ssNder1_4r1r1r1r1(X517,X513,X520,X519)
| ~ ssNder1_3r1r1r1(X517,X513,X520)
| ~ ssNder1_2r1r1(X517,X513)
| ~ ssNder1_1r1(X517)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X517,X513,X520,X519,X516,X512,X515,X518,X514,X521) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c74,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X713,X718,X717,X709,X711,X710,X716,X712)
| ~ ssNder1_7r1r1r1r1r1r1r1(X713,X718,X717,X709,X711,X710,X716)
| ~ ssNder1_6r1r1r1r1r1r1(X713,X718,X717,X709,X711,X710)
| ~ ssNder1_5r1r1r1r1r1(X713,X718,X717,X709,X711)
| ~ ssNder1_4r1r1r1r1(X713,X718,X717,X709)
| ~ ssNder1_3r1r1r1(X713,X718,X717)
| ~ ssNder1_2r1r1(X713,X718)
| ~ ssNder1_1r1(X713)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X713,X718,X717,X709,X711,X710,X716,X712,X715,X714) ),
inference(resolution,[status(thm)],[c73,clause21]) ).
cnf(c98,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X724,X723,X726,X725,X728,X720,X721)
| ~ ssNder1_6r1r1r1r1r1r1(X724,X723,X726,X725,X728,X720)
| ~ ssNder1_5r1r1r1r1r1(X724,X723,X726,X725,X728)
| ~ ssNder1_4r1r1r1r1(X724,X723,X726,X725)
| ~ ssNder1_3r1r1r1(X724,X723,X726)
| ~ ssNder1_2r1r1(X724,X723)
| ~ ssNder1_1r1(X724)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X724,X723,X726,X725,X728,X720,X721,X719,X722,X727) ),
inference(resolution,[status(thm)],[c74,c58]) ).
cnf(c99,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X736,X732,X737,X738,X729,X730)
| ~ ssNder1_5r1r1r1r1r1(X736,X732,X737,X738,X729)
| ~ ssNder1_4r1r1r1r1(X736,X732,X737,X738)
| ~ ssNder1_3r1r1r1(X736,X732,X737)
| ~ ssNder1_2r1r1(X736,X732)
| ~ ssNder1_1r1(X736)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X736,X732,X737,X738,X729,X730,X735,X731,X734,X733) ),
inference(resolution,[status(thm)],[c98,c43]) ).
cnf(c100,plain,
( ~ ssNder1_5r1r1r1r1r1(X758,X751,X755,X760,X753)
| ~ ssNder1_4r1r1r1r1(X758,X751,X755,X760)
| ~ ssNder1_3r1r1r1(X758,X751,X755)
| ~ ssNder1_2r1r1(X758,X751)
| ~ ssNder1_1r1(X758)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X758,X751,X755,X760,X753,X752,X759,X757,X754,X756) ),
inference(resolution,[status(thm)],[c99,c30]) ).
cnf(c101,plain,
( ~ ssNder1_4r1r1r1r1(X769,X763,X765,X770)
| ~ ssNder1_3r1r1r1(X769,X763,X765)
| ~ ssNder1_2r1r1(X769,X763)
| ~ ssNder1_1r1(X769)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X769,X763,X765,X770,X768,X766,X767,X764,X762,X761) ),
inference(resolution,[status(thm)],[c100,c19]) ).
cnf(c102,plain,
( ~ ssNder1_3r1r1r1(X772,X773,X778)
| ~ ssNder1_2r1r1(X772,X773)
| ~ ssNder1_1r1(X772)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X772,X773,X778,X779,X774,X771,X775,X776,X777,X780) ),
inference(resolution,[status(thm)],[c101,c10]) ).
cnf(c103,plain,
( ~ ssNder1_2r1r1(X788,X782)
| ~ ssNder1_1r1(X788)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X788,X782,X787,X785,X783,X786,X784,X790,X781,X789) ),
inference(resolution,[status(thm)],[c102,c5]) ).
cnf(c104,plain,
( ~ ssNder1_1r1(X793)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X793,X794,X800,X792,X798,X796,X795,X797,X791,X799) ),
inference(resolution,[status(thm)],[c103,c2]) ).
cnf(c105,plain,
( ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X814,X822,X815,X817,X821,X819,X820,X813,X816,X818) ),
inference(resolution,[status(thm)],[c104,c0]) ).
cnf(c106,plain,
ssNder1_10r1r1r1r1r1r1r1r1r1r1(X832,X828,X825,X827,X824,X831,X829,X830,X823,X826),
inference(resolution,[status(thm)],[c105,clause1]) ).
cnf(clause24,negated_conjecture,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X635,X631,X638,X637,X634,X630,X633,X636,X632,X639)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X635,X631,X638,X637,X634,X630,X633,X636,X632)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X635,X631,X638,X637,X634,X630,X633,X636)
| ~ ssNder1_7r1r1r1r1r1r1r1(X635,X631,X638,X637,X634,X630,X633)
| ~ ssNder1_6r1r1r1r1r1r1(X635,X631,X638,X637,X634,X630)
| ~ ssNder1_5r1r1r1r1r1(X635,X631,X638,X637,X634)
| ~ ssNder1_4r1r1r1r1(X635,X631,X638,X637)
| ~ ssNder1_3r1r1r1(X635,X631,X638)
| ~ ssNder1_2r1r1(X635,X631)
| ~ ssNder1_1r1(X635)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X635,X631,X638,X637,X634,X630,X633,X636,X632,X639,X629) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c107,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1002,X999,X1000,X998,X995,X996,X997,X1005,X1001)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1002,X999,X1000,X998,X995,X996,X997,X1005)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1002,X999,X1000,X998,X995,X996,X997)
| ~ ssNder1_6r1r1r1r1r1r1(X1002,X999,X1000,X998,X995,X996)
| ~ ssNder1_5r1r1r1r1r1(X1002,X999,X1000,X998,X995)
| ~ ssNder1_4r1r1r1r1(X1002,X999,X1000,X998)
| ~ ssNder1_3r1r1r1(X1002,X999,X1000)
| ~ ssNder1_2r1r1(X1002,X999)
| ~ ssNder1_1r1(X1002)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1002,X999,X1000,X998,X995,X996,X997,X1005,X1001,X1003,X1004) ),
inference(resolution,[status(thm)],[c106,clause24]) ).
cnf(c126,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X1016,X1015,X1007,X1011,X1009,X1006,X1012,X1010)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1016,X1015,X1007,X1011,X1009,X1006,X1012)
| ~ ssNder1_6r1r1r1r1r1r1(X1016,X1015,X1007,X1011,X1009,X1006)
| ~ ssNder1_5r1r1r1r1r1(X1016,X1015,X1007,X1011,X1009)
| ~ ssNder1_4r1r1r1r1(X1016,X1015,X1007,X1011)
| ~ ssNder1_3r1r1r1(X1016,X1015,X1007)
| ~ ssNder1_2r1r1(X1016,X1015)
| ~ ssNder1_1r1(X1016)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1016,X1015,X1007,X1011,X1009,X1006,X1012,X1010,X1008,X1014,X1013) ),
inference(resolution,[status(thm)],[c107,c73]) ).
cnf(c127,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X1035,X1034,X1038,X1036,X1040,X1032,X1033)
| ~ ssNder1_6r1r1r1r1r1r1(X1035,X1034,X1038,X1036,X1040,X1032)
| ~ ssNder1_5r1r1r1r1r1(X1035,X1034,X1038,X1036,X1040)
| ~ ssNder1_4r1r1r1r1(X1035,X1034,X1038,X1036)
| ~ ssNder1_3r1r1r1(X1035,X1034,X1038)
| ~ ssNder1_2r1r1(X1035,X1034)
| ~ ssNder1_1r1(X1035)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1035,X1034,X1038,X1036,X1040,X1032,X1033,X1031,X1037,X1030,X1039) ),
inference(resolution,[status(thm)],[c126,c58]) ).
cnf(c128,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X1049,X1045,X1050,X1051,X1041,X1043)
| ~ ssNder1_5r1r1r1r1r1(X1049,X1045,X1050,X1051,X1041)
| ~ ssNder1_4r1r1r1r1(X1049,X1045,X1050,X1051)
| ~ ssNder1_3r1r1r1(X1049,X1045,X1050)
| ~ ssNder1_2r1r1(X1049,X1045)
| ~ ssNder1_1r1(X1049)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1049,X1045,X1050,X1051,X1041,X1043,X1048,X1046,X1047,X1044,X1042) ),
inference(resolution,[status(thm)],[c127,c43]) ).
cnf(c129,plain,
( ~ ssNder1_5r1r1r1r1r1(X1060,X1053,X1058,X1062,X1055)
| ~ ssNder1_4r1r1r1r1(X1060,X1053,X1058,X1062)
| ~ ssNder1_3r1r1r1(X1060,X1053,X1058)
| ~ ssNder1_2r1r1(X1060,X1053)
| ~ ssNder1_1r1(X1060)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1060,X1053,X1058,X1062,X1055,X1054,X1059,X1061,X1056,X1052,X1057) ),
inference(resolution,[status(thm)],[c128,c30]) ).
cnf(c130,plain,
( ~ ssNder1_4r1r1r1r1(X1072,X1065,X1066,X1073)
| ~ ssNder1_3r1r1r1(X1072,X1065,X1066)
| ~ ssNder1_2r1r1(X1072,X1065)
| ~ ssNder1_1r1(X1072)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1072,X1065,X1066,X1073,X1069,X1067,X1068,X1071,X1064,X1070,X1063) ),
inference(resolution,[status(thm)],[c129,c19]) ).
cnf(c131,plain,
( ~ ssNder1_3r1r1r1(X1077,X1078,X1082)
| ~ ssNder1_2r1r1(X1077,X1078)
| ~ ssNder1_1r1(X1077)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1077,X1078,X1082,X1083,X1079,X1084,X1075,X1081,X1080,X1074,X1076) ),
inference(resolution,[status(thm)],[c130,c10]) ).
cnf(c132,plain,
( ~ ssNder1_2r1r1(X1103,X1098)
| ~ ssNder1_1r1(X1103)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1103,X1098,X1102,X1099,X1100,X1107,X1101,X1106,X1104,X1108,X1105) ),
inference(resolution,[status(thm)],[c131,c5]) ).
cnf(c133,plain,
( ~ ssNder1_1r1(X1112)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1112,X1113,X1118,X1109,X1114,X1110,X1115,X1117,X1119,X1116,X1111) ),
inference(resolution,[status(thm)],[c132,c2]) ).
cnf(c134,plain,
( ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1124,X1120,X1121,X1130,X1129,X1128,X1127,X1122,X1123,X1125,X1126) ),
inference(resolution,[status(thm)],[c133,c0]) ).
cnf(c135,plain,
ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1139,X1140,X1131,X1134,X1133,X1138,X1136,X1141,X1137,X1135,X1132),
inference(resolution,[status(thm)],[c134,clause1]) ).
cnf(clause27,negated_conjecture,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X745,X741,X748,X747,X744,X740,X743,X746,X742,X750,X739)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X745,X741,X748,X747,X744,X740,X743,X746,X742,X750)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X745,X741,X748,X747,X744,X740,X743,X746,X742)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X745,X741,X748,X747,X744,X740,X743,X746)
| ~ ssNder1_7r1r1r1r1r1r1r1(X745,X741,X748,X747,X744,X740,X743)
| ~ ssNder1_6r1r1r1r1r1r1(X745,X741,X748,X747,X744,X740)
| ~ ssNder1_5r1r1r1r1r1(X745,X741,X748,X747,X744)
| ~ ssNder1_4r1r1r1r1(X745,X741,X748,X747)
| ~ ssNder1_3r1r1r1(X745,X741,X748)
| ~ ssNder1_2r1r1(X745,X741)
| ~ ssNder1_1r1(X745)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X745,X741,X748,X747,X744,X740,X743,X746,X742,X750,X739,X749) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c136,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1165,X1169,X1161,X1164,X1168,X1166,X1167,X1163,X1170,X1160)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1165,X1169,X1161,X1164,X1168,X1166,X1167,X1163,X1170)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1165,X1169,X1161,X1164,X1168,X1166,X1167,X1163)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1165,X1169,X1161,X1164,X1168,X1166,X1167)
| ~ ssNder1_6r1r1r1r1r1r1(X1165,X1169,X1161,X1164,X1168,X1166)
| ~ ssNder1_5r1r1r1r1r1(X1165,X1169,X1161,X1164,X1168)
| ~ ssNder1_4r1r1r1r1(X1165,X1169,X1161,X1164)
| ~ ssNder1_3r1r1r1(X1165,X1169,X1161)
| ~ ssNder1_2r1r1(X1165,X1169)
| ~ ssNder1_1r1(X1165)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1165,X1169,X1161,X1164,X1168,X1166,X1167,X1163,X1170,X1160,X1171,X1162) ),
inference(resolution,[status(thm)],[c135,clause27]) ).
cnf(c138,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1175,X1180,X1181,X1176,X1173,X1172,X1174,X1179,X1177)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1175,X1180,X1181,X1176,X1173,X1172,X1174,X1179)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1175,X1180,X1181,X1176,X1173,X1172,X1174)
| ~ ssNder1_6r1r1r1r1r1r1(X1175,X1180,X1181,X1176,X1173,X1172)
| ~ ssNder1_5r1r1r1r1r1(X1175,X1180,X1181,X1176,X1173)
| ~ ssNder1_4r1r1r1r1(X1175,X1180,X1181,X1176)
| ~ ssNder1_3r1r1r1(X1175,X1180,X1181)
| ~ ssNder1_2r1r1(X1175,X1180)
| ~ ssNder1_1r1(X1175)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1175,X1180,X1181,X1176,X1173,X1172,X1174,X1179,X1177,X1183,X1182,X1178) ),
inference(resolution,[status(thm)],[c136,c106]) ).
cnf(c139,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X1195,X1194,X1185,X1190,X1188,X1184,X1191,X1189)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1195,X1194,X1185,X1190,X1188,X1184,X1191)
| ~ ssNder1_6r1r1r1r1r1r1(X1195,X1194,X1185,X1190,X1188,X1184)
| ~ ssNder1_5r1r1r1r1r1(X1195,X1194,X1185,X1190,X1188)
| ~ ssNder1_4r1r1r1r1(X1195,X1194,X1185,X1190)
| ~ ssNder1_3r1r1r1(X1195,X1194,X1185)
| ~ ssNder1_2r1r1(X1195,X1194)
| ~ ssNder1_1r1(X1195)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1195,X1194,X1185,X1190,X1188,X1184,X1191,X1189,X1186,X1192,X1193,X1187) ),
inference(resolution,[status(thm)],[c138,c73]) ).
cnf(c140,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X1201,X1200,X1204,X1202,X1207,X1198,X1199)
| ~ ssNder1_6r1r1r1r1r1r1(X1201,X1200,X1204,X1202,X1207,X1198)
| ~ ssNder1_5r1r1r1r1r1(X1201,X1200,X1204,X1202,X1207)
| ~ ssNder1_4r1r1r1r1(X1201,X1200,X1204,X1202)
| ~ ssNder1_3r1r1r1(X1201,X1200,X1204)
| ~ ssNder1_2r1r1(X1201,X1200)
| ~ ssNder1_1r1(X1201)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1201,X1200,X1204,X1202,X1207,X1198,X1199,X1197,X1205,X1196,X1206,X1203) ),
inference(resolution,[status(thm)],[c139,c58]) ).
cnf(c141,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X1216,X1213,X1218,X1219,X1208,X1211)
| ~ ssNder1_5r1r1r1r1r1(X1216,X1213,X1218,X1219,X1208)
| ~ ssNder1_4r1r1r1r1(X1216,X1213,X1218,X1219)
| ~ ssNder1_3r1r1r1(X1216,X1213,X1218)
| ~ ssNder1_2r1r1(X1216,X1213)
| ~ ssNder1_1r1(X1216)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1216,X1213,X1218,X1219,X1208,X1211,X1214,X1217,X1212,X1209,X1210,X1215) ),
inference(resolution,[status(thm)],[c140,c43]) ).
cnf(c142,plain,
( ~ ssNder1_5r1r1r1r1r1(X1239,X1232,X1235,X1243,X1234)
| ~ ssNder1_4r1r1r1r1(X1239,X1232,X1235,X1243)
| ~ ssNder1_3r1r1r1(X1239,X1232,X1235)
| ~ ssNder1_2r1r1(X1239,X1232)
| ~ ssNder1_1r1(X1239)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1239,X1232,X1235,X1243,X1234,X1233,X1236,X1238,X1237,X1241,X1240,X1242) ),
inference(resolution,[status(thm)],[c141,c30]) ).
cnf(c143,plain,
( ~ ssNder1_4r1r1r1r1(X1254,X1245,X1246,X1255)
| ~ ssNder1_3r1r1r1(X1254,X1245,X1246)
| ~ ssNder1_2r1r1(X1254,X1245)
| ~ ssNder1_1r1(X1254)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1254,X1245,X1246,X1255,X1252,X1247,X1250,X1244,X1248,X1251,X1253,X1249) ),
inference(resolution,[status(thm)],[c142,c19]) ).
cnf(c144,plain,
( ~ ssNder1_3r1r1r1(X1259,X1260,X1263)
| ~ ssNder1_2r1r1(X1259,X1260)
| ~ ssNder1_1r1(X1259)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1259,X1260,X1263,X1264,X1266,X1256,X1261,X1262,X1267,X1257,X1265,X1258) ),
inference(resolution,[status(thm)],[c143,c10]) ).
cnf(c145,plain,
( ~ ssNder1_2r1r1(X1277,X1268)
| ~ ssNder1_1r1(X1277)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1277,X1268,X1276,X1269,X1270,X1278,X1275,X1272,X1273,X1279,X1271,X1274) ),
inference(resolution,[status(thm)],[c144,c5]) ).
cnf(c146,plain,
( ~ ssNder1_1r1(X1283)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1283,X1285,X1286,X1288,X1290,X1282,X1287,X1280,X1291,X1281,X1289,X1284) ),
inference(resolution,[status(thm)],[c145,c2]) ).
cnf(c147,plain,
( ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1310,X1317,X1316,X1307,X1308,X1311,X1309,X1314,X1313,X1315,X1306,X1312) ),
inference(resolution,[status(thm)],[c146,c0]) ).
cnf(c148,plain,
ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1325,X1318,X1323,X1326,X1324,X1319,X1322,X1329,X1321,X1327,X1320,X1328),
inference(resolution,[status(thm)],[c147,clause1]) ).
cnf(clause31,negated_conjecture,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X968,X963,X971,X970,X967,X962,X966,X969,X964,X973,X961,X972)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X968,X963,X971,X970,X967,X962,X966,X969,X964,X973,X961)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X968,X963,X971,X970,X967,X962,X966,X969,X964,X973)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X968,X963,X971,X970,X967,X962,X966,X969,X964)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X968,X963,X971,X970,X967,X962,X966,X969)
| ~ ssNder1_7r1r1r1r1r1r1r1(X968,X963,X971,X970,X967,X962,X966)
| ~ ssNder1_6r1r1r1r1r1r1(X968,X963,X971,X970,X967,X962)
| ~ ssNder1_5r1r1r1r1r1(X968,X963,X971,X970,X967)
| ~ ssNder1_4r1r1r1r1(X968,X963,X971,X970)
| ~ ssNder1_3r1r1r1(X968,X963,X971)
| ~ ssNder1_2r1r1(X968,X963)
| ~ ssNder1_1r1(X968)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X968,X963,X971,X970,X967,X962,X966,X969,X964,X973,X961,X972,X965) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c149,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X2793,X2787,X2790,X2784,X2792,X2785,X2789,X2783,X2781,X2791,X2782)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X2793,X2787,X2790,X2784,X2792,X2785,X2789,X2783,X2781,X2791)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2793,X2787,X2790,X2784,X2792,X2785,X2789,X2783,X2781)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2793,X2787,X2790,X2784,X2792,X2785,X2789,X2783)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2793,X2787,X2790,X2784,X2792,X2785,X2789)
| ~ ssNder1_6r1r1r1r1r1r1(X2793,X2787,X2790,X2784,X2792,X2785)
| ~ ssNder1_5r1r1r1r1r1(X2793,X2787,X2790,X2784,X2792)
| ~ ssNder1_4r1r1r1r1(X2793,X2787,X2790,X2784)
| ~ ssNder1_3r1r1r1(X2793,X2787,X2790)
| ~ ssNder1_2r1r1(X2793,X2787)
| ~ ssNder1_1r1(X2793)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2793,X2787,X2790,X2784,X2792,X2785,X2789,X2783,X2781,X2791,X2782,X2786,X2788) ),
inference(resolution,[status(thm)],[c148,clause31]) ).
cnf(c244,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X2796,X2802,X2801,X2797,X2799,X2804,X2803,X2794,X2795,X2805)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2796,X2802,X2801,X2797,X2799,X2804,X2803,X2794,X2795)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2796,X2802,X2801,X2797,X2799,X2804,X2803,X2794)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2796,X2802,X2801,X2797,X2799,X2804,X2803)
| ~ ssNder1_6r1r1r1r1r1r1(X2796,X2802,X2801,X2797,X2799,X2804)
| ~ ssNder1_5r1r1r1r1r1(X2796,X2802,X2801,X2797,X2799)
| ~ ssNder1_4r1r1r1r1(X2796,X2802,X2801,X2797)
| ~ ssNder1_3r1r1r1(X2796,X2802,X2801)
| ~ ssNder1_2r1r1(X2796,X2802)
| ~ ssNder1_1r1(X2796)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2796,X2802,X2801,X2797,X2799,X2804,X2803,X2794,X2795,X2805,X2798,X2800,X2806) ),
inference(resolution,[status(thm)],[c149,c135]) ).
cnf(c245,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2810,X2816,X2818,X2812,X2808,X2807,X2809,X2815,X2813)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2810,X2816,X2818,X2812,X2808,X2807,X2809,X2815)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2810,X2816,X2818,X2812,X2808,X2807,X2809)
| ~ ssNder1_6r1r1r1r1r1r1(X2810,X2816,X2818,X2812,X2808,X2807)
| ~ ssNder1_5r1r1r1r1r1(X2810,X2816,X2818,X2812,X2808)
| ~ ssNder1_4r1r1r1r1(X2810,X2816,X2818,X2812)
| ~ ssNder1_3r1r1r1(X2810,X2816,X2818)
| ~ ssNder1_2r1r1(X2810,X2816)
| ~ ssNder1_1r1(X2810)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2810,X2816,X2818,X2812,X2808,X2807,X2809,X2815,X2813,X2819,X2817,X2814,X2811) ),
inference(resolution,[status(thm)],[c244,c106]) ).
cnf(c246,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X2832,X2831,X2823,X2829,X2827,X2820,X2830,X2828)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2832,X2831,X2823,X2829,X2827,X2820,X2830)
| ~ ssNder1_6r1r1r1r1r1r1(X2832,X2831,X2823,X2829,X2827,X2820)
| ~ ssNder1_5r1r1r1r1r1(X2832,X2831,X2823,X2829,X2827)
| ~ ssNder1_4r1r1r1r1(X2832,X2831,X2823,X2829)
| ~ ssNder1_3r1r1r1(X2832,X2831,X2823)
| ~ ssNder1_2r1r1(X2832,X2831)
| ~ ssNder1_1r1(X2832)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2832,X2831,X2823,X2829,X2827,X2820,X2830,X2828,X2826,X2821,X2822,X2825,X2824) ),
inference(resolution,[status(thm)],[c245,c73]) ).
cnf(c247,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X2854,X2853,X2859,X2855,X2862,X2851,X2852)
| ~ ssNder1_6r1r1r1r1r1r1(X2854,X2853,X2859,X2855,X2862,X2851)
| ~ ssNder1_5r1r1r1r1r1(X2854,X2853,X2859,X2855,X2862)
| ~ ssNder1_4r1r1r1r1(X2854,X2853,X2859,X2855)
| ~ ssNder1_3r1r1r1(X2854,X2853,X2859)
| ~ ssNder1_2r1r1(X2854,X2853)
| ~ ssNder1_1r1(X2854)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2854,X2853,X2859,X2855,X2862,X2851,X2852,X2850,X2860,X2861,X2856,X2857,X2858) ),
inference(resolution,[status(thm)],[c246,c58]) ).
cnf(c248,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X2872,X2867,X2874,X2875,X2863,X2865)
| ~ ssNder1_5r1r1r1r1r1(X2872,X2867,X2874,X2875,X2863)
| ~ ssNder1_4r1r1r1r1(X2872,X2867,X2874,X2875)
| ~ ssNder1_3r1r1r1(X2872,X2867,X2874)
| ~ ssNder1_2r1r1(X2872,X2867)
| ~ ssNder1_1r1(X2872)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2872,X2867,X2874,X2875,X2863,X2865,X2871,X2873,X2866,X2870,X2869,X2868,X2864) ),
inference(resolution,[status(thm)],[c247,c43]) ).
cnf(c249,plain,
( ~ ssNder1_5r1r1r1r1r1(X2883,X2877,X2880,X2888,X2879)
| ~ ssNder1_4r1r1r1r1(X2883,X2877,X2880,X2888)
| ~ ssNder1_3r1r1r1(X2883,X2877,X2880)
| ~ ssNder1_2r1r1(X2883,X2877)
| ~ ssNder1_1r1(X2883)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2883,X2877,X2880,X2888,X2879,X2878,X2884,X2881,X2887,X2876,X2882,X2886,X2885) ),
inference(resolution,[status(thm)],[c248,c30]) ).
cnf(c250,plain,
( ~ ssNder1_4r1r1r1r1(X2899,X2890,X2892,X2900)
| ~ ssNder1_3r1r1r1(X2899,X2890,X2892)
| ~ ssNder1_2r1r1(X2899,X2890)
| ~ ssNder1_1r1(X2899)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2899,X2890,X2892,X2900,X2898,X2889,X2901,X2891,X2894,X2895,X2893,X2897,X2896) ),
inference(resolution,[status(thm)],[c249,c19]) ).
cnf(c251,plain,
( ~ ssNder1_3r1r1r1(X2903,X2904,X2912)
| ~ ssNder1_2r1r1(X2903,X2904)
| ~ ssNder1_1r1(X2903)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2903,X2904,X2912,X2913,X2909,X2902,X2911,X2910,X2914,X2908,X2906,X2905,X2907) ),
inference(resolution,[status(thm)],[c250,c10]) ).
cnf(c252,plain,
( ~ ssNder1_2r1r1(X2939,X2934)
| ~ ssNder1_1r1(X2939)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2939,X2934,X2938,X2941,X2945,X2943,X2944,X2942,X2935,X2940,X2937,X2933,X2936) ),
inference(resolution,[status(thm)],[c251,c5]) ).
cnf(c253,plain,
( ~ ssNder1_1r1(X2952)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2952,X2953,X2947,X2958,X2951,X2946,X2957,X2954,X2956,X2948,X2949,X2950,X2955) ),
inference(resolution,[status(thm)],[c252,c2]) ).
cnf(c254,plain,
( ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2959,X2968,X2966,X2961,X2971,X2970,X2965,X2967,X2960,X2964,X2969,X2962,X2963) ),
inference(resolution,[status(thm)],[c253,c0]) ).
cnf(c255,plain,
ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2973,X2982,X2972,X2978,X2975,X2983,X2976,X2984,X2979,X2980,X2981,X2977,X2974),
inference(resolution,[status(thm)],[c254,clause1]) ).
cnf(clause46,negated_conjecture,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020,X2025,X2028,X2023,X2032,X2019,X2031,X2024)
| ~ ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020,X2025,X2028,X2023,X2032,X2019,X2031,X2024,X2021)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020,X2025,X2028,X2023,X2032,X2019,X2031)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020,X2025,X2028,X2023,X2032,X2019)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020,X2025,X2028,X2023,X2032)
| ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020,X2025,X2028,X2023)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020,X2025,X2028,X2023)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020,X2025,X2028)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020,X2025)
| ~ ssNder1_6r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020)
| ~ ssNder1_5r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026)
| ~ ssNder1_4r1r1r1r1(X2027,X2022,X2030,X2029)
| ~ ssNder1_3r1r1r1(X2027,X2022,X2030)
| ~ ssPv19_2r1r1(X2027,X2022)
| ~ ssNder1_2r1r1(X2027,X2022)
| ~ ssNder1_1r1(X2027)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X2027,X2022,X2030,X2029,X2026,X2020,X2025) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(clause32,negated_conjecture,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1024,X1019,X1027,X1026,X1023,X1018,X1022,X1025,X1020,X1029,X1017,X1028)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1024,X1019,X1027,X1026,X1023,X1018,X1022,X1025,X1020,X1029,X1017)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1024,X1019,X1027,X1026,X1023,X1018,X1022,X1025,X1020,X1029)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1024,X1019,X1027,X1026,X1023,X1018,X1022,X1025,X1020)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1024,X1019,X1027,X1026,X1023,X1018,X1022,X1025)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1024,X1019,X1027,X1026,X1023,X1018,X1022)
| ~ ssNder1_6r1r1r1r1r1r1(X1024,X1019,X1027,X1026,X1023,X1018)
| ~ ssNder1_5r1r1r1r1r1(X1024,X1019,X1027,X1026,X1023)
| ~ ssNder1_4r1r1r1r1(X1024,X1019,X1027,X1026)
| ~ ssNder1_3r1r1r1(X1024,X1019,X1027)
| ~ ssNder1_2r1r1(X1024,X1019)
| ~ ssNder1_1r1(X1024)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1024,X1019,X1027,X1026,X1023,X1018,X1022,X1025,X1020,X1029,X1017,X1028,X1021,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c150,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X2992,X2995,X2990,X2997,X2991,X2996,X2986,X2985,X2987,X2993,X2994)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X2992,X2995,X2990,X2997,X2991,X2996,X2986,X2985,X2987,X2993)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2992,X2995,X2990,X2997,X2991,X2996,X2986,X2985,X2987)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2992,X2995,X2990,X2997,X2991,X2996,X2986,X2985)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2992,X2995,X2990,X2997,X2991,X2996,X2986)
| ~ ssNder1_6r1r1r1r1r1r1(X2992,X2995,X2990,X2997,X2991,X2996)
| ~ ssNder1_5r1r1r1r1r1(X2992,X2995,X2990,X2997,X2991)
| ~ ssNder1_4r1r1r1r1(X2992,X2995,X2990,X2997)
| ~ ssNder1_3r1r1r1(X2992,X2995,X2990)
| ~ ssNder1_2r1r1(X2992,X2995)
| ~ ssNder1_1r1(X2992)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2992,X2995,X2990,X2997,X2991,X2996,X2986,X2985,X2987,X2993,X2994,X2988,X2989,skc20) ),
inference(resolution,[status(thm)],[c148,clause32]) ).
cnf(c258,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3017,X3022,X3021,X3018,X3020,X3025,X3024,X3014,X3015,X3026)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3017,X3022,X3021,X3018,X3020,X3025,X3024,X3014,X3015)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3017,X3022,X3021,X3018,X3020,X3025,X3024,X3014)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3017,X3022,X3021,X3018,X3020,X3025,X3024)
| ~ ssNder1_6r1r1r1r1r1r1(X3017,X3022,X3021,X3018,X3020,X3025)
| ~ ssNder1_5r1r1r1r1r1(X3017,X3022,X3021,X3018,X3020)
| ~ ssNder1_4r1r1r1r1(X3017,X3022,X3021,X3018)
| ~ ssNder1_3r1r1r1(X3017,X3022,X3021)
| ~ ssNder1_2r1r1(X3017,X3022)
| ~ ssNder1_1r1(X3017)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3017,X3022,X3021,X3018,X3020,X3025,X3024,X3014,X3015,X3026,X3019,X3023,X3016,skc20) ),
inference(resolution,[status(thm)],[c150,c135]) ).
cnf(c259,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3030,X3034,X3036,X3031,X3028,X3027,X3029,X3033,X3032)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3030,X3034,X3036,X3031,X3028,X3027,X3029,X3033)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3030,X3034,X3036,X3031,X3028,X3027,X3029)
| ~ ssNder1_6r1r1r1r1r1r1(X3030,X3034,X3036,X3031,X3028,X3027)
| ~ ssNder1_5r1r1r1r1r1(X3030,X3034,X3036,X3031,X3028)
| ~ ssNder1_4r1r1r1r1(X3030,X3034,X3036,X3031)
| ~ ssNder1_3r1r1r1(X3030,X3034,X3036)
| ~ ssNder1_2r1r1(X3030,X3034)
| ~ ssNder1_1r1(X3030)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3030,X3034,X3036,X3031,X3028,X3027,X3029,X3033,X3032,X3038,X3039,X3037,X3035,skc20) ),
inference(resolution,[status(thm)],[c258,c106]) ).
cnf(c260,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X3052,X3051,X3042,X3048,X3046,X3040,X3049,X3047)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3052,X3051,X3042,X3048,X3046,X3040,X3049)
| ~ ssNder1_6r1r1r1r1r1r1(X3052,X3051,X3042,X3048,X3046,X3040)
| ~ ssNder1_5r1r1r1r1r1(X3052,X3051,X3042,X3048,X3046)
| ~ ssNder1_4r1r1r1r1(X3052,X3051,X3042,X3048)
| ~ ssNder1_3r1r1r1(X3052,X3051,X3042)
| ~ ssNder1_2r1r1(X3052,X3051)
| ~ ssNder1_1r1(X3052)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3052,X3051,X3042,X3048,X3046,X3040,X3049,X3047,X3044,X3050,X3043,X3041,X3045,skc20) ),
inference(resolution,[status(thm)],[c259,c73]) ).
cnf(c261,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X3059,X3058,X3063,X3060,X3065,X3056,X3057)
| ~ ssNder1_6r1r1r1r1r1r1(X3059,X3058,X3063,X3060,X3065,X3056)
| ~ ssNder1_5r1r1r1r1r1(X3059,X3058,X3063,X3060,X3065)
| ~ ssNder1_4r1r1r1r1(X3059,X3058,X3063,X3060)
| ~ ssNder1_3r1r1r1(X3059,X3058,X3063)
| ~ ssNder1_2r1r1(X3059,X3058)
| ~ ssNder1_1r1(X3059)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3059,X3058,X3063,X3060,X3065,X3056,X3057,X3054,X3053,X3064,X3062,X3055,X3061,skc20) ),
inference(resolution,[status(thm)],[c260,c58]) ).
cnf(c262,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X3074,X3068,X3076,X3078,X3066,X3067)
| ~ ssNder1_5r1r1r1r1r1(X3074,X3068,X3076,X3078,X3066)
| ~ ssNder1_4r1r1r1r1(X3074,X3068,X3076,X3078)
| ~ ssNder1_3r1r1r1(X3074,X3068,X3076)
| ~ ssNder1_2r1r1(X3074,X3068)
| ~ ssNder1_1r1(X3074)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3074,X3068,X3076,X3078,X3066,X3067,X3073,X3077,X3069,X3070,X3071,X3072,X3075,skc20) ),
inference(resolution,[status(thm)],[c261,c43]) ).
cnf(c263,plain,
( ~ ssNder1_5r1r1r1r1r1(X3104,X3096,X3100,X3108,X3098)
| ~ ssNder1_4r1r1r1r1(X3104,X3096,X3100,X3108)
| ~ ssNder1_3r1r1r1(X3104,X3096,X3100)
| ~ ssNder1_2r1r1(X3104,X3096)
| ~ ssNder1_1r1(X3104)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3104,X3096,X3100,X3108,X3098,X3097,X3102,X3099,X3103,X3107,X3101,X3106,X3105,skc20) ),
inference(resolution,[status(thm)],[c262,c30]) ).
cnf(c264,plain,
( ~ ssNder1_4r1r1r1r1(X3120,X3112,X3113,X3121)
| ~ ssNder1_3r1r1r1(X3120,X3112,X3113)
| ~ ssNder1_2r1r1(X3120,X3112)
| ~ ssNder1_1r1(X3120)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3120,X3112,X3113,X3121,X3118,X3109,X3115,X3119,X3110,X3117,X3111,X3114,X3116,skc20) ),
inference(resolution,[status(thm)],[c263,c19]) ).
cnf(c265,plain,
( ~ ssNder1_3r1r1r1(X3124,X3125,X3131)
| ~ ssNder1_2r1r1(X3124,X3125)
| ~ ssNder1_1r1(X3124)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3124,X3125,X3131,X3132,X3123,X3129,X3122,X3126,X3127,X3128,X3133,X3130,X3134,skc20) ),
inference(resolution,[status(thm)],[c264,c10]) ).
cnf(c266,plain,
( ~ ssNder1_2r1r1(X3143,X3135)
| ~ ssNder1_1r1(X3143)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3143,X3135,X3142,X3145,X3146,X3139,X3136,X3141,X3138,X3137,X3144,X3147,X3140,skc20) ),
inference(resolution,[status(thm)],[c265,c5]) ).
cnf(c267,plain,
( ~ ssNder1_1r1(X3154)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3154,X3156,X3151,X3149,X3160,X3148,X3157,X3152,X3155,X3153,X3158,X3159,X3150,skc20) ),
inference(resolution,[status(thm)],[c266,c2]) ).
cnf(c268,plain,
( ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3182,X3180,X3183,X3179,X3190,X3185,X3189,X3187,X3186,X3178,X3181,X3188,X3184,skc20) ),
inference(resolution,[status(thm)],[c267,c0]) ).
cnf(c269,plain,
ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3200,X3194,X3199,X3193,X3191,X3196,X3195,X3197,X3203,X3201,X3198,X3202,X3192,skc20),
inference(resolution,[status(thm)],[c268,clause1]) ).
cnf(c270,plain,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168,X5165,X5170,X5162,X5161,X5159,X5169,X5158,X5163)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168,X5165,X5170,X5162,X5161,X5159,X5169,X5158)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168,X5165,X5170,X5162,X5161,X5159,X5169)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168,X5165,X5170,X5162,X5161,X5159)
| ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168,X5165,X5170,X5162,X5161)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168,X5165,X5170,X5162,X5161)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168,X5165,X5170,X5162)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168,X5165,X5170)
| ~ ssNder1_6r1r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168,X5165)
| ~ ssNder1_5r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168)
| ~ ssNder1_4r1r1r1r1(X5166,X5167,X5164,X5160)
| ~ ssNder1_3r1r1r1(X5166,X5167,X5164)
| ~ ssPv19_2r1r1(X5166,X5167)
| ~ ssNder1_2r1r1(X5166,X5167)
| ~ ssNder1_1r1(X5166)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X5166,X5167,X5164,X5160,X5168,X5165,X5170) ),
inference(resolution,[status(thm)],[c269,clause46]) ).
cnf(c413,plain,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X5718,X5719,X5726,X5716,X5721,X5723,X5720,X5724,X5725,X5717,X5722,X5715)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5718,X5719,X5726,X5716,X5721,X5723,X5720,X5724,X5725,X5717,X5722)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5718,X5719,X5726,X5716,X5721,X5723,X5720,X5724,X5725,X5717)
| ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X5718,X5719,X5726,X5716,X5721,X5723,X5720,X5724,X5725)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5718,X5719,X5726,X5716,X5721,X5723,X5720,X5724,X5725)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5718,X5719,X5726,X5716,X5721,X5723,X5720,X5724)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5718,X5719,X5726,X5716,X5721,X5723,X5720)
| ~ ssNder1_6r1r1r1r1r1r1(X5718,X5719,X5726,X5716,X5721,X5723)
| ~ ssNder1_5r1r1r1r1r1(X5718,X5719,X5726,X5716,X5721)
| ~ ssNder1_4r1r1r1r1(X5718,X5719,X5726,X5716)
| ~ ssNder1_3r1r1r1(X5718,X5719,X5726)
| ~ ssPv19_2r1r1(X5718,X5719)
| ~ ssNder1_2r1r1(X5718,X5719)
| ~ ssNder1_1r1(X5718)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X5718,X5719,X5726,X5716,X5721,X5723,X5720) ),
inference(resolution,[status(thm)],[c270,c255]) ).
cnf(c456,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5775,X5774,X5773,X5781,X5772,X5778,X5779,X5782,X5780,X5777,X5776)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5775,X5774,X5773,X5781,X5772,X5778,X5779,X5782,X5780,X5777)
| ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X5775,X5774,X5773,X5781,X5772,X5778,X5779,X5782,X5780)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5775,X5774,X5773,X5781,X5772,X5778,X5779,X5782,X5780)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5775,X5774,X5773,X5781,X5772,X5778,X5779,X5782)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5775,X5774,X5773,X5781,X5772,X5778,X5779)
| ~ ssNder1_6r1r1r1r1r1r1(X5775,X5774,X5773,X5781,X5772,X5778)
| ~ ssNder1_5r1r1r1r1r1(X5775,X5774,X5773,X5781,X5772)
| ~ ssNder1_4r1r1r1r1(X5775,X5774,X5773,X5781)
| ~ ssNder1_3r1r1r1(X5775,X5774,X5773)
| ~ ssPv19_2r1r1(X5775,X5774)
| ~ ssNder1_2r1r1(X5775,X5774)
| ~ ssNder1_1r1(X5775)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X5775,X5774,X5773,X5781,X5772,X5778,X5779) ),
inference(resolution,[status(thm)],[c413,c148]) ).
cnf(c464,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5785,X5789,X5788,X5786,X5787,X5791,X5790,X5783,X5784,X5792)
| ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X5785,X5789,X5788,X5786,X5787,X5791,X5790,X5783,X5784)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5785,X5789,X5788,X5786,X5787,X5791,X5790,X5783,X5784)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5785,X5789,X5788,X5786,X5787,X5791,X5790,X5783)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5785,X5789,X5788,X5786,X5787,X5791,X5790)
| ~ ssNder1_6r1r1r1r1r1r1(X5785,X5789,X5788,X5786,X5787,X5791)
| ~ ssNder1_5r1r1r1r1r1(X5785,X5789,X5788,X5786,X5787)
| ~ ssNder1_4r1r1r1r1(X5785,X5789,X5788,X5786)
| ~ ssNder1_3r1r1r1(X5785,X5789,X5788)
| ~ ssPv19_2r1r1(X5785,X5789)
| ~ ssNder1_2r1r1(X5785,X5789)
| ~ ssNder1_1r1(X5785)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X5785,X5789,X5788,X5786,X5787,X5791,X5790) ),
inference(resolution,[status(thm)],[c456,c135]) ).
cnf(c465,plain,
( ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X5811,X5815,X5816,X5812,X5809,X5808,X5810,X5814,X5813)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5811,X5815,X5816,X5812,X5809,X5808,X5810,X5814,X5813)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5811,X5815,X5816,X5812,X5809,X5808,X5810,X5814)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5811,X5815,X5816,X5812,X5809,X5808,X5810)
| ~ ssNder1_6r1r1r1r1r1r1(X5811,X5815,X5816,X5812,X5809,X5808)
| ~ ssNder1_5r1r1r1r1r1(X5811,X5815,X5816,X5812,X5809)
| ~ ssNder1_4r1r1r1r1(X5811,X5815,X5816,X5812)
| ~ ssNder1_3r1r1r1(X5811,X5815,X5816)
| ~ ssPv19_2r1r1(X5811,X5815)
| ~ ssNder1_2r1r1(X5811,X5815)
| ~ ssNder1_1r1(X5811)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X5811,X5815,X5816,X5812,X5809,X5808,X5810) ),
inference(resolution,[status(thm)],[c464,c106]) ).
cnf(c467,plain,
( ~ ssPv12_9r1r1r1r1r1r1r1r1r1(X5825,X5824,X5818,X5822,X5820,X5817,X5823,X5821,X5819)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5825,X5824,X5818,X5822,X5820,X5817,X5823,X5821)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5825,X5824,X5818,X5822,X5820,X5817,X5823)
| ~ ssNder1_6r1r1r1r1r1r1(X5825,X5824,X5818,X5822,X5820,X5817)
| ~ ssNder1_5r1r1r1r1r1(X5825,X5824,X5818,X5822,X5820)
| ~ ssNder1_4r1r1r1r1(X5825,X5824,X5818,X5822)
| ~ ssNder1_3r1r1r1(X5825,X5824,X5818)
| ~ ssPv19_2r1r1(X5825,X5824)
| ~ ssNder1_2r1r1(X5825,X5824)
| ~ ssNder1_1r1(X5825)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X5825,X5824,X5818,X5822,X5820,X5817,X5823) ),
inference(resolution,[status(thm)],[c465,c73]) ).
cnf(clause16,negated_conjecture,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X295,X292,X297,X296,X294,X291,X293,skc25)
| ~ ssNder1_6r1r1r1r1r1r1(X295,X292,X297,X296,X294,X291)
| ~ ssNder1_5r1r1r1r1r1(X295,X292,X297,X296,X294)
| ~ ssNder1_4r1r1r1r1(X295,X292,X297,X296)
| ~ ssNder1_3r1r1r1(X295,X292,X297)
| ~ ssNder1_2r1r1(X295,X292)
| ~ ssNder1_1r1(X295)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(clause36,negated_conjecture,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1300,X1295,X1303,X1302,X1299,X1293,X1298,X1301,X1296,X1305,X1292,X1304,X1297)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1300,X1295,X1303,X1302,X1299,X1293,X1298,X1301,X1296,X1305,X1292,X1304)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1300,X1295,X1303,X1302,X1299,X1293,X1298,X1301,X1296,X1305,X1292)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1300,X1295,X1303,X1302,X1299,X1293,X1298,X1301,X1296,X1305)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1300,X1295,X1303,X1302,X1299,X1293,X1298,X1301,X1296)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1300,X1295,X1303,X1302,X1299,X1293,X1298,X1301)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1300,X1295,X1303,X1302,X1299,X1293,X1298)
| ~ ssNder1_6r1r1r1r1r1r1(X1300,X1295,X1303,X1302,X1299,X1293)
| ~ ssNder1_5r1r1r1r1r1(X1300,X1295,X1303,X1302,X1299)
| ~ ssNder1_4r1r1r1r1(X1300,X1295,X1303,X1302)
| ~ ssNder1_3r1r1r1(X1300,X1295,X1303)
| ~ ssNder1_2r1r1(X1300,X1295)
| ~ ssNder1_1r1(X1300)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1300,X1295,X1303,X1302,X1299,X1293,X1298,X1301,X1296,X1305,X1292,X1304,X1297,X1294) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c257,plain,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X3460,X3457,X3459,X3464,X3463,X3458,X3461,X3462,X3456,X3465,X3466,X3469)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X3460,X3457,X3459,X3464,X3463,X3458,X3461,X3462,X3456,X3465,X3466)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3460,X3457,X3459,X3464,X3463,X3458,X3461,X3462,X3456,X3465)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3460,X3457,X3459,X3464,X3463,X3458,X3461,X3462,X3456)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3460,X3457,X3459,X3464,X3463,X3458,X3461,X3462)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3460,X3457,X3459,X3464,X3463,X3458,X3461)
| ~ ssNder1_6r1r1r1r1r1r1(X3460,X3457,X3459,X3464,X3463,X3458)
| ~ ssNder1_5r1r1r1r1r1(X3460,X3457,X3459,X3464,X3463)
| ~ ssNder1_4r1r1r1r1(X3460,X3457,X3459,X3464)
| ~ ssNder1_3r1r1r1(X3460,X3457,X3459)
| ~ ssNder1_2r1r1(X3460,X3457)
| ~ ssNder1_1r1(X3460)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3460,X3457,X3459,X3464,X3463,X3458,X3461,X3462,X3456,X3465,X3466,X3469,X3467,X3468) ),
inference(resolution,[status(thm)],[c255,clause36]) ).
cnf(c289,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X3493,X3492,X3491,X3500,X3489,X3497,X3498,X3501,X3499,X3496,X3494)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3493,X3492,X3491,X3500,X3489,X3497,X3498,X3501,X3499,X3496)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3493,X3492,X3491,X3500,X3489,X3497,X3498,X3501,X3499)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3493,X3492,X3491,X3500,X3489,X3497,X3498,X3501)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3493,X3492,X3491,X3500,X3489,X3497,X3498)
| ~ ssNder1_6r1r1r1r1r1r1(X3493,X3492,X3491,X3500,X3489,X3497)
| ~ ssNder1_5r1r1r1r1r1(X3493,X3492,X3491,X3500,X3489)
| ~ ssNder1_4r1r1r1r1(X3493,X3492,X3491,X3500)
| ~ ssNder1_3r1r1r1(X3493,X3492,X3491)
| ~ ssNder1_2r1r1(X3493,X3492)
| ~ ssNder1_1r1(X3493)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3493,X3492,X3491,X3500,X3489,X3497,X3498,X3501,X3499,X3496,X3494,X3495,X3490,X3502) ),
inference(resolution,[status(thm)],[c257,c148]) ).
cnf(c290,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3506,X3513,X3512,X3507,X3510,X3515,X3514,X3504,X3505,X3516)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3506,X3513,X3512,X3507,X3510,X3515,X3514,X3504,X3505)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3506,X3513,X3512,X3507,X3510,X3515,X3514,X3504)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3506,X3513,X3512,X3507,X3510,X3515,X3514)
| ~ ssNder1_6r1r1r1r1r1r1(X3506,X3513,X3512,X3507,X3510,X3515)
| ~ ssNder1_5r1r1r1r1r1(X3506,X3513,X3512,X3507,X3510)
| ~ ssNder1_4r1r1r1r1(X3506,X3513,X3512,X3507)
| ~ ssNder1_3r1r1r1(X3506,X3513,X3512)
| ~ ssNder1_2r1r1(X3506,X3513)
| ~ ssNder1_1r1(X3506)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3506,X3513,X3512,X3507,X3510,X3515,X3514,X3504,X3505,X3516,X3509,X3503,X3511,X3508) ),
inference(resolution,[status(thm)],[c289,c135]) ).
cnf(c291,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3520,X3525,X3527,X3522,X3518,X3517,X3519,X3524,X3523)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3520,X3525,X3527,X3522,X3518,X3517,X3519,X3524)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3520,X3525,X3527,X3522,X3518,X3517,X3519)
| ~ ssNder1_6r1r1r1r1r1r1(X3520,X3525,X3527,X3522,X3518,X3517)
| ~ ssNder1_5r1r1r1r1r1(X3520,X3525,X3527,X3522,X3518)
| ~ ssNder1_4r1r1r1r1(X3520,X3525,X3527,X3522)
| ~ ssNder1_3r1r1r1(X3520,X3525,X3527)
| ~ ssNder1_2r1r1(X3520,X3525)
| ~ ssNder1_1r1(X3520)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3520,X3525,X3527,X3522,X3518,X3517,X3519,X3524,X3523,X3530,X3529,X3521,X3528,X3526) ),
inference(resolution,[status(thm)],[c290,c106]) ).
cnf(c292,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X3544,X3543,X3534,X3540,X3538,X3531,X3541,X3539)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3544,X3543,X3534,X3540,X3538,X3531,X3541)
| ~ ssNder1_6r1r1r1r1r1r1(X3544,X3543,X3534,X3540,X3538,X3531)
| ~ ssNder1_5r1r1r1r1r1(X3544,X3543,X3534,X3540,X3538)
| ~ ssNder1_4r1r1r1r1(X3544,X3543,X3534,X3540)
| ~ ssNder1_3r1r1r1(X3544,X3543,X3534)
| ~ ssNder1_2r1r1(X3544,X3543)
| ~ ssNder1_1r1(X3544)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3544,X3543,X3534,X3540,X3538,X3531,X3541,X3539,X3536,X3532,X3533,X3535,X3542,X3537) ),
inference(resolution,[status(thm)],[c291,c73]) ).
cnf(c293,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X3550,X3549,X3555,X3551,X3558,X3546,X3547)
| ~ ssNder1_6r1r1r1r1r1r1(X3550,X3549,X3555,X3551,X3558,X3546)
| ~ ssNder1_5r1r1r1r1r1(X3550,X3549,X3555,X3551,X3558)
| ~ ssNder1_4r1r1r1r1(X3550,X3549,X3555,X3551)
| ~ ssNder1_3r1r1r1(X3550,X3549,X3555)
| ~ ssNder1_2r1r1(X3550,X3549)
| ~ ssNder1_1r1(X3550)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3550,X3549,X3555,X3551,X3558,X3546,X3547,X3545,X3552,X3556,X3557,X3553,X3554,X3548) ),
inference(resolution,[status(thm)],[c292,c58]) ).
cnf(c294,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X3586,X3581,X3588,X3590,X3577,X3579)
| ~ ssNder1_5r1r1r1r1r1(X3586,X3581,X3588,X3590,X3577)
| ~ ssNder1_4r1r1r1r1(X3586,X3581,X3588,X3590)
| ~ ssNder1_3r1r1r1(X3586,X3581,X3588)
| ~ ssNder1_2r1r1(X3586,X3581)
| ~ ssNder1_1r1(X3586)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3586,X3581,X3588,X3590,X3577,X3579,X3584,X3582,X3585,X3583,X3589,X3580,X3587,X3578) ),
inference(resolution,[status(thm)],[c293,c43]) ).
cnf(c295,plain,
( ~ ssNder1_5r1r1r1r1r1(X3601,X3592,X3597,X3604,X3596)
| ~ ssNder1_4r1r1r1r1(X3601,X3592,X3597,X3604)
| ~ ssNder1_3r1r1r1(X3601,X3592,X3597)
| ~ ssNder1_2r1r1(X3601,X3592)
| ~ ssNder1_1r1(X3601)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3601,X3592,X3597,X3604,X3596,X3595,X3600,X3593,X3599,X3602,X3603,X3591,X3598,X3594) ),
inference(resolution,[status(thm)],[c294,c30]) ).
cnf(c296,plain,
( ~ ssNder1_4r1r1r1r1(X3617,X3608,X3609,X3618)
| ~ ssNder1_3r1r1r1(X3617,X3608,X3609)
| ~ ssNder1_2r1r1(X3617,X3608)
| ~ ssNder1_1r1(X3617)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3617,X3608,X3609,X3618,X3615,X3605,X3607,X3616,X3614,X3606,X3612,X3610,X3611,X3613) ),
inference(resolution,[status(thm)],[c295,c19]) ).
cnf(c297,plain,
( ~ ssNder1_3r1r1r1(X3622,X3623,X3630)
| ~ ssNder1_2r1r1(X3622,X3623)
| ~ ssNder1_1r1(X3622)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3622,X3623,X3630,X3631,X3626,X3621,X3629,X3625,X3627,X3632,X3628,X3624,X3619,X3620) ),
inference(resolution,[status(thm)],[c296,c10]) ).
cnf(c298,plain,
( ~ ssNder1_2r1r1(X3638,X3633)
| ~ ssNder1_1r1(X3638)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3638,X3633,X3637,X3640,X3639,X3636,X3642,X3634,X3645,X3646,X3635,X3641,X3643,X3644) ),
inference(resolution,[status(thm)],[c297,c5]) ).
cnf(c299,plain,
( ~ ssNder1_1r1(X3671)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3671,X3672,X3664,X3673,X3677,X3674,X3675,X3665,X3676,X3666,X3668,X3667,X3669,X3670) ),
inference(resolution,[status(thm)],[c298,c2]) ).
cnf(c300,plain,
( ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3680,X3691,X3687,X3682,X3678,X3690,X3684,X3689,X3683,X3685,X3679,X3686,X3688,X3681) ),
inference(resolution,[status(thm)],[c299,c0]) ).
cnf(c301,plain,
ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3704,X3697,X3693,X3698,X3699,X3702,X3705,X3694,X3692,X3701,X3695,X3696,X3700,X3703),
inference(resolution,[status(thm)],[c300,clause1]) ).
cnf(clause50,negated_conjecture,
( ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381,X2384,X2379,X2389,X2375,X2388,X2380,X2377)
| ~ ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381,X2384,X2379,X2389,X2375,X2388,X2380,X2377,X2385)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381,X2384,X2379,X2389,X2375,X2388,X2380)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381,X2384,X2379,X2389,X2375,X2388)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381,X2384,X2379,X2389,X2375)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381,X2384,X2379,X2389)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381,X2384,X2379)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381,X2384)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381)
| ~ ssNder1_6r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376)
| ~ ssNder1_5r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382)
| ~ ssNder1_4r1r1r1r1(X2383,X2378,X2387,X2386)
| ~ ssNder1_3r1r1r1(X2383,X2378,X2387)
| ~ ssPv19_2r1r1(X2383,X2378)
| ~ ssNder1_2r1r1(X2383,X2378)
| ~ ssNder1_1r1(X2383)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381,X2384,X2379)
| ssPv13_8r1r1r1r1r1r1r1r1(X2383,X2378,X2387,X2386,X2382,X2376,X2381,X2384) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(clause38,negated_conjecture,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1442,X1437,X1445,X1444,X1441,X1435,X1440,X1443,X1438,X1447,X1434,X1446,X1439)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1442,X1437,X1445,X1444,X1441,X1435,X1440,X1443,X1438,X1447,X1434,X1446)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1442,X1437,X1445,X1444,X1441,X1435,X1440,X1443,X1438,X1447,X1434)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1442,X1437,X1445,X1444,X1441,X1435,X1440,X1443,X1438,X1447)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1442,X1437,X1445,X1444,X1441,X1435,X1440,X1443,X1438)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1442,X1437,X1445,X1444,X1441,X1435,X1440,X1443)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1442,X1437,X1445,X1444,X1441,X1435,X1440)
| ~ ssNder1_6r1r1r1r1r1r1(X1442,X1437,X1445,X1444,X1441,X1435)
| ~ ssNder1_5r1r1r1r1r1(X1442,X1437,X1445,X1444,X1441)
| ~ ssNder1_4r1r1r1r1(X1442,X1437,X1445,X1444)
| ~ ssNder1_3r1r1r1(X1442,X1437,X1445)
| ~ ssNder1_2r1r1(X1442,X1437)
| ~ ssNder1_1r1(X1442)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1442,X1437,X1445,X1444,X1441,X1435,X1440,X1443,X1438,X1447,X1434,X1446,X1439,X1436,skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c256,plain,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X3714,X3706,X3716,X3710,X3712,X3719,X3709,X3715,X3717,X3708,X3711,X3713)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X3714,X3706,X3716,X3710,X3712,X3719,X3709,X3715,X3717,X3708,X3711)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3714,X3706,X3716,X3710,X3712,X3719,X3709,X3715,X3717,X3708)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3714,X3706,X3716,X3710,X3712,X3719,X3709,X3715,X3717)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3714,X3706,X3716,X3710,X3712,X3719,X3709,X3715)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3714,X3706,X3716,X3710,X3712,X3719,X3709)
| ~ ssNder1_6r1r1r1r1r1r1(X3714,X3706,X3716,X3710,X3712,X3719)
| ~ ssNder1_5r1r1r1r1r1(X3714,X3706,X3716,X3710,X3712)
| ~ ssNder1_4r1r1r1r1(X3714,X3706,X3716,X3710)
| ~ ssNder1_3r1r1r1(X3714,X3706,X3716)
| ~ ssNder1_2r1r1(X3714,X3706)
| ~ ssNder1_1r1(X3714)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3714,X3706,X3716,X3710,X3712,X3719,X3709,X3715,X3717,X3708,X3711,X3713,X3718,X3707,skc18) ),
inference(resolution,[status(thm)],[c255,clause38]) ).
cnf(c306,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X3724,X3723,X3721,X3731,X3720,X3728,X3729,X3733,X3730,X3727,X3725)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3724,X3723,X3721,X3731,X3720,X3728,X3729,X3733,X3730,X3727)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3724,X3723,X3721,X3731,X3720,X3728,X3729,X3733,X3730)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3724,X3723,X3721,X3731,X3720,X3728,X3729,X3733)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3724,X3723,X3721,X3731,X3720,X3728,X3729)
| ~ ssNder1_6r1r1r1r1r1r1(X3724,X3723,X3721,X3731,X3720,X3728)
| ~ ssNder1_5r1r1r1r1r1(X3724,X3723,X3721,X3731,X3720)
| ~ ssNder1_4r1r1r1r1(X3724,X3723,X3721,X3731)
| ~ ssNder1_3r1r1r1(X3724,X3723,X3721)
| ~ ssNder1_2r1r1(X3724,X3723)
| ~ ssNder1_1r1(X3724)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3724,X3723,X3721,X3731,X3720,X3728,X3729,X3733,X3730,X3727,X3725,X3726,X3732,X3722,skc18) ),
inference(resolution,[status(thm)],[c256,c148]) ).
cnf(c307,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3755,X3762,X3761,X3756,X3760,X3764,X3763,X3753,X3754,X3765)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3755,X3762,X3761,X3756,X3760,X3764,X3763,X3753,X3754)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3755,X3762,X3761,X3756,X3760,X3764,X3763,X3753)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3755,X3762,X3761,X3756,X3760,X3764,X3763)
| ~ ssNder1_6r1r1r1r1r1r1(X3755,X3762,X3761,X3756,X3760,X3764)
| ~ ssNder1_5r1r1r1r1r1(X3755,X3762,X3761,X3756,X3760)
| ~ ssNder1_4r1r1r1r1(X3755,X3762,X3761,X3756)
| ~ ssNder1_3r1r1r1(X3755,X3762,X3761)
| ~ ssNder1_2r1r1(X3755,X3762)
| ~ ssNder1_1r1(X3755)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3755,X3762,X3761,X3756,X3760,X3764,X3763,X3753,X3754,X3765,X3758,X3752,X3759,X3757,skc18) ),
inference(resolution,[status(thm)],[c306,c135]) ).
cnf(c308,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3770,X3775,X3776,X3771,X3768,X3766,X3769,X3774,X3773)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3770,X3775,X3776,X3771,X3768,X3766,X3769,X3774)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3770,X3775,X3776,X3771,X3768,X3766,X3769)
| ~ ssNder1_6r1r1r1r1r1r1(X3770,X3775,X3776,X3771,X3768,X3766)
| ~ ssNder1_5r1r1r1r1r1(X3770,X3775,X3776,X3771,X3768)
| ~ ssNder1_4r1r1r1r1(X3770,X3775,X3776,X3771)
| ~ ssNder1_3r1r1r1(X3770,X3775,X3776)
| ~ ssNder1_2r1r1(X3770,X3775)
| ~ ssNder1_1r1(X3770)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3770,X3775,X3776,X3771,X3768,X3766,X3769,X3774,X3773,X3778,X3779,X3777,X3767,X3772,skc18) ),
inference(resolution,[status(thm)],[c307,c106]) ).
cnf(c309,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X3792,X3791,X3782,X3789,X3787,X3780,X3790,X3788)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3792,X3791,X3782,X3789,X3787,X3780,X3790)
| ~ ssNder1_6r1r1r1r1r1r1(X3792,X3791,X3782,X3789,X3787,X3780)
| ~ ssNder1_5r1r1r1r1r1(X3792,X3791,X3782,X3789,X3787)
| ~ ssNder1_4r1r1r1r1(X3792,X3791,X3782,X3789)
| ~ ssNder1_3r1r1r1(X3792,X3791,X3782)
| ~ ssNder1_2r1r1(X3792,X3791)
| ~ ssNder1_1r1(X3792)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3792,X3791,X3782,X3789,X3787,X3780,X3790,X3788,X3785,X3783,X3786,X3793,X3781,X3784,skc18) ),
inference(resolution,[status(thm)],[c308,c73]) ).
cnf(c310,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X3799,X3798,X3803,X3800,X3807,X3795,X3796)
| ~ ssNder1_6r1r1r1r1r1r1(X3799,X3798,X3803,X3800,X3807,X3795)
| ~ ssNder1_5r1r1r1r1r1(X3799,X3798,X3803,X3800,X3807)
| ~ ssNder1_4r1r1r1r1(X3799,X3798,X3803,X3800)
| ~ ssNder1_3r1r1r1(X3799,X3798,X3803)
| ~ ssNder1_2r1r1(X3799,X3798)
| ~ ssNder1_1r1(X3799)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3799,X3798,X3803,X3800,X3807,X3795,X3796,X3794,X3797,X3801,X3802,X3805,X3806,X3804,skc18) ),
inference(resolution,[status(thm)],[c309,c58]) ).
cnf(c311,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X3818,X3810,X3820,X3821,X3808,X3809)
| ~ ssNder1_5r1r1r1r1r1(X3818,X3810,X3820,X3821,X3808)
| ~ ssNder1_4r1r1r1r1(X3818,X3810,X3820,X3821)
| ~ ssNder1_3r1r1r1(X3818,X3810,X3820)
| ~ ssNder1_2r1r1(X3818,X3810)
| ~ ssNder1_1r1(X3818)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3818,X3810,X3820,X3821,X3808,X3809,X3817,X3811,X3813,X3814,X3812,X3816,X3815,X3819,skc18) ),
inference(resolution,[status(thm)],[c310,c43]) ).
cnf(c312,plain,
( ~ ssNder1_5r1r1r1r1r1(X3852,X3842,X3847,X3853,X3844)
| ~ ssNder1_4r1r1r1r1(X3852,X3842,X3847,X3853)
| ~ ssNder1_3r1r1r1(X3852,X3842,X3847)
| ~ ssNder1_2r1r1(X3852,X3842)
| ~ ssNder1_1r1(X3852)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3852,X3842,X3847,X3853,X3844,X3843,X3845,X3846,X3848,X3851,X3840,X3841,X3849,X3850,skc18) ),
inference(resolution,[status(thm)],[c311,c30]) ).
cnf(c313,plain,
( ~ ssNder1_4r1r1r1r1(X3866,X3854,X3856,X3867)
| ~ ssNder1_3r1r1r1(X3866,X3854,X3856)
| ~ ssNder1_2r1r1(X3866,X3854)
| ~ ssNder1_1r1(X3866)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3866,X3854,X3856,X3867,X3865,X3857,X3859,X3863,X3855,X3860,X3858,X3861,X3864,X3862,skc18) ),
inference(resolution,[status(thm)],[c312,c19]) ).
cnf(c314,plain,
( ~ ssNder1_3r1r1r1(X3872,X3873,X3879)
| ~ ssNder1_2r1r1(X3872,X3873)
| ~ ssNder1_1r1(X3872)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3872,X3873,X3879,X3880,X3876,X3874,X3881,X3877,X3870,X3878,X3869,X3871,X3868,X3875,skc18) ),
inference(resolution,[status(thm)],[c313,c10]) ).
cnf(c315,plain,
( ~ ssNder1_2r1r1(X3888,X3883)
| ~ ssNder1_1r1(X3888)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3888,X3883,X3886,X3885,X3894,X3889,X3884,X3893,X3895,X3891,X3890,X3892,X3882,X3887,skc18) ),
inference(resolution,[status(thm)],[c314,c5]) ).
cnf(c316,plain,
( ~ ssNder1_1r1(X3902)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3902,X3904,X3908,X3899,X3896,X3905,X3901,X3897,X3898,X3906,X3909,X3907,X3903,X3900,skc18) ),
inference(resolution,[status(thm)],[c315,c2]) ).
cnf(c317,plain,
( ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3928,X3937,X3935,X3939,X3938,X3931,X3932,X3936,X3940,X3933,X3934,X3941,X3929,X3930,skc18) ),
inference(resolution,[status(thm)],[c316,c0]) ).
cnf(c318,plain,
ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3944,X3949,X3951,X3942,X3950,X3945,X3943,X3953,X3946,X3954,X3952,X3947,X3948,X3955,skc18),
inference(resolution,[status(thm)],[c317,clause1]) ).
cnf(c319,plain,
( ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541,X5543,X5540,X5550,X5551,X5542,X5545,X5547,X5539)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541,X5543,X5540,X5550,X5551,X5542,X5545,X5547)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541,X5543,X5540,X5550,X5551,X5542,X5545)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541,X5543,X5540,X5550,X5551,X5542)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541,X5543,X5540,X5550,X5551)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541,X5543,X5540,X5550)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541,X5543,X5540)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541,X5543)
| ~ ssNder1_6r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541)
| ~ ssNder1_5r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544)
| ~ ssNder1_4r1r1r1r1(X5538,X5548,X5546,X5549)
| ~ ssNder1_3r1r1r1(X5538,X5548,X5546)
| ~ ssPv19_2r1r1(X5538,X5548)
| ~ ssNder1_2r1r1(X5538,X5548)
| ~ ssNder1_1r1(X5538)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541,X5543,X5540,X5550)
| ssPv13_8r1r1r1r1r1r1r1r1(X5538,X5548,X5546,X5549,X5544,X5541,X5543,X5540) ),
inference(resolution,[status(thm)],[c318,clause50]) ).
cnf(c441,plain,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942,X5945,X5946,X5940,X5948,X5947,X5950,X5944,X5941)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942,X5945,X5946,X5940,X5948,X5947,X5950,X5944)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942,X5945,X5946,X5940,X5948,X5947,X5950)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942,X5945,X5946,X5940,X5948,X5947)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942,X5945,X5946,X5940,X5948)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942,X5945,X5946,X5940)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942,X5945,X5946)
| ~ ssNder1_6r1r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942,X5945)
| ~ ssNder1_5r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942)
| ~ ssNder1_4r1r1r1r1(X5949,X5939,X5943,X5951)
| ~ ssNder1_3r1r1r1(X5949,X5939,X5943)
| ~ ssPv19_2r1r1(X5949,X5939)
| ~ ssNder1_2r1r1(X5949,X5939)
| ~ ssNder1_1r1(X5949)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942,X5945,X5946,X5940,X5948)
| ssPv13_8r1r1r1r1r1r1r1r1(X5949,X5939,X5943,X5951,X5942,X5945,X5946,X5940) ),
inference(resolution,[status(thm)],[c319,c301]) ).
cnf(c477,plain,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X7071,X7072,X7079,X7069,X7074,X7076,X7073,X7077,X7078,X7070,X7075,X7068)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X7071,X7072,X7079,X7069,X7074,X7076,X7073,X7077,X7078,X7070,X7075)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X7071,X7072,X7079,X7069,X7074,X7076,X7073,X7077,X7078,X7070)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X7071,X7072,X7079,X7069,X7074,X7076,X7073,X7077,X7078)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X7071,X7072,X7079,X7069,X7074,X7076,X7073,X7077)
| ~ ssNder1_7r1r1r1r1r1r1r1(X7071,X7072,X7079,X7069,X7074,X7076,X7073)
| ~ ssNder1_6r1r1r1r1r1r1(X7071,X7072,X7079,X7069,X7074,X7076)
| ~ ssNder1_5r1r1r1r1r1(X7071,X7072,X7079,X7069,X7074)
| ~ ssNder1_4r1r1r1r1(X7071,X7072,X7079,X7069)
| ~ ssNder1_3r1r1r1(X7071,X7072,X7079)
| ~ ssPv19_2r1r1(X7071,X7072)
| ~ ssNder1_2r1r1(X7071,X7072)
| ~ ssNder1_1r1(X7071)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X7071,X7072,X7079,X7069,X7074,X7076,X7073,X7077,X7078)
| ssPv13_8r1r1r1r1r1r1r1r1(X7071,X7072,X7079,X7069,X7074,X7076,X7073,X7077) ),
inference(resolution,[status(thm)],[c441,c255]) ).
cnf(c557,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X9634,X9633,X9632,X9640,X9631,X9637,X9638,X9641,X9639,X9636,X9635)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X9634,X9633,X9632,X9640,X9631,X9637,X9638,X9641,X9639,X9636)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X9634,X9633,X9632,X9640,X9631,X9637,X9638,X9641,X9639)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X9634,X9633,X9632,X9640,X9631,X9637,X9638,X9641)
| ~ ssNder1_7r1r1r1r1r1r1r1(X9634,X9633,X9632,X9640,X9631,X9637,X9638)
| ~ ssNder1_6r1r1r1r1r1r1(X9634,X9633,X9632,X9640,X9631,X9637)
| ~ ssNder1_5r1r1r1r1r1(X9634,X9633,X9632,X9640,X9631)
| ~ ssNder1_4r1r1r1r1(X9634,X9633,X9632,X9640)
| ~ ssNder1_3r1r1r1(X9634,X9633,X9632)
| ~ ssPv19_2r1r1(X9634,X9633)
| ~ ssNder1_2r1r1(X9634,X9633)
| ~ ssNder1_1r1(X9634)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X9634,X9633,X9632,X9640,X9631,X9637,X9638,X9641,X9639)
| ssPv13_8r1r1r1r1r1r1r1r1(X9634,X9633,X9632,X9640,X9631,X9637,X9638,X9641) ),
inference(resolution,[status(thm)],[c477,c148]) ).
cnf(c779,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X14539,X14543,X14542,X14540,X14541,X14545,X14544,X14537,X14538,X14546)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X14539,X14543,X14542,X14540,X14541,X14545,X14544,X14537,X14538)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X14539,X14543,X14542,X14540,X14541,X14545,X14544,X14537)
| ~ ssNder1_7r1r1r1r1r1r1r1(X14539,X14543,X14542,X14540,X14541,X14545,X14544)
| ~ ssNder1_6r1r1r1r1r1r1(X14539,X14543,X14542,X14540,X14541,X14545)
| ~ ssNder1_5r1r1r1r1r1(X14539,X14543,X14542,X14540,X14541)
| ~ ssNder1_4r1r1r1r1(X14539,X14543,X14542,X14540)
| ~ ssNder1_3r1r1r1(X14539,X14543,X14542)
| ~ ssPv19_2r1r1(X14539,X14543)
| ~ ssNder1_2r1r1(X14539,X14543)
| ~ ssNder1_1r1(X14539)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14539,X14543,X14542,X14540,X14541,X14545,X14544,X14537,X14538)
| ssPv13_8r1r1r1r1r1r1r1r1(X14539,X14543,X14542,X14540,X14541,X14545,X14544,X14537) ),
inference(resolution,[status(thm)],[c557,c135]) ).
cnf(c1080,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X14550,X14554,X14555,X14551,X14548,X14547,X14549,X14553,X14552)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X14550,X14554,X14555,X14551,X14548,X14547,X14549,X14553)
| ~ ssNder1_7r1r1r1r1r1r1r1(X14550,X14554,X14555,X14551,X14548,X14547,X14549)
| ~ ssNder1_6r1r1r1r1r1r1(X14550,X14554,X14555,X14551,X14548,X14547)
| ~ ssNder1_5r1r1r1r1r1(X14550,X14554,X14555,X14551,X14548)
| ~ ssNder1_4r1r1r1r1(X14550,X14554,X14555,X14551)
| ~ ssNder1_3r1r1r1(X14550,X14554,X14555)
| ~ ssPv19_2r1r1(X14550,X14554)
| ~ ssNder1_2r1r1(X14550,X14554)
| ~ ssNder1_1r1(X14550)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14550,X14554,X14555,X14551,X14548,X14547,X14549,X14553,X14552)
| ssPv13_8r1r1r1r1r1r1r1r1(X14550,X14554,X14555,X14551,X14548,X14547,X14549,X14553) ),
inference(resolution,[status(thm)],[c779,c106]) ).
cnf(c1081,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X14582,X14581,X14575,X14579,X14577,X14574,X14580,X14578)
| ~ ssNder1_7r1r1r1r1r1r1r1(X14582,X14581,X14575,X14579,X14577,X14574,X14580)
| ~ ssNder1_6r1r1r1r1r1r1(X14582,X14581,X14575,X14579,X14577,X14574)
| ~ ssNder1_5r1r1r1r1r1(X14582,X14581,X14575,X14579,X14577)
| ~ ssNder1_4r1r1r1r1(X14582,X14581,X14575,X14579)
| ~ ssNder1_3r1r1r1(X14582,X14581,X14575)
| ~ ssPv19_2r1r1(X14582,X14581)
| ~ ssNder1_2r1r1(X14582,X14581)
| ~ ssNder1_1r1(X14582)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14582,X14581,X14575,X14579,X14577,X14574,X14580,X14578,X14576)
| ssPv13_8r1r1r1r1r1r1r1r1(X14582,X14581,X14575,X14579,X14577,X14574,X14580,X14578) ),
inference(resolution,[status(thm)],[c1080,c73]) ).
cnf(c1083,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X14587,X14586,X14590,X14588,X14591,X14584,X14585)
| ~ ssNder1_6r1r1r1r1r1r1(X14587,X14586,X14590,X14588,X14591,X14584)
| ~ ssNder1_5r1r1r1r1r1(X14587,X14586,X14590,X14588,X14591)
| ~ ssNder1_4r1r1r1r1(X14587,X14586,X14590,X14588)
| ~ ssNder1_3r1r1r1(X14587,X14586,X14590)
| ~ ssPv19_2r1r1(X14587,X14586)
| ~ ssNder1_2r1r1(X14587,X14586)
| ~ ssNder1_1r1(X14587)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14587,X14586,X14590,X14588,X14591,X14584,X14585,X14583,X14589)
| ssPv13_8r1r1r1r1r1r1r1r1(X14587,X14586,X14590,X14588,X14591,X14584,X14585,X14583) ),
inference(resolution,[status(thm)],[c1081,c58]) ).
cnf(c1084,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X14597,X14595,X14599,X14600,X14592,X14593)
| ~ ssNder1_5r1r1r1r1r1(X14597,X14595,X14599,X14600,X14592)
| ~ ssNder1_4r1r1r1r1(X14597,X14595,X14599,X14600)
| ~ ssNder1_3r1r1r1(X14597,X14595,X14599)
| ~ ssPv19_2r1r1(X14597,X14595)
| ~ ssNder1_2r1r1(X14597,X14595)
| ~ ssNder1_1r1(X14597)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14597,X14595,X14599,X14600,X14592,X14593,X14596,X14594,X14598)
| ssPv13_8r1r1r1r1r1r1r1r1(X14597,X14595,X14599,X14600,X14592,X14593,X14596,X14594) ),
inference(resolution,[status(thm)],[c1083,c43]) ).
cnf(c1085,plain,
( ~ ssNder1_5r1r1r1r1r1(X14607,X14601,X14605,X14609,X14603)
| ~ ssNder1_4r1r1r1r1(X14607,X14601,X14605,X14609)
| ~ ssNder1_3r1r1r1(X14607,X14601,X14605)
| ~ ssPv19_2r1r1(X14607,X14601)
| ~ ssNder1_2r1r1(X14607,X14601)
| ~ ssNder1_1r1(X14607)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14607,X14601,X14605,X14609,X14603,X14602,X14606,X14604,X14608)
| ssPv13_8r1r1r1r1r1r1r1r1(X14607,X14601,X14605,X14609,X14603,X14602,X14606,X14604) ),
inference(resolution,[status(thm)],[c1084,c30]) ).
cnf(c1086,plain,
( ~ ssNder1_4r1r1r1r1(X14617,X14611,X14612,X14618)
| ~ ssNder1_3r1r1r1(X14617,X14611,X14612)
| ~ ssPv19_2r1r1(X14617,X14611)
| ~ ssNder1_2r1r1(X14617,X14611)
| ~ ssNder1_1r1(X14617)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14617,X14611,X14612,X14618,X14615,X14613,X14614,X14610,X14616)
| ssPv13_8r1r1r1r1r1r1r1r1(X14617,X14611,X14612,X14618,X14615,X14613,X14614,X14610) ),
inference(resolution,[status(thm)],[c1085,c19]) ).
cnf(c1087,plain,
( ~ ssNder1_3r1r1r1(X14644,X14645,X14647)
| ~ ssPv19_2r1r1(X14644,X14645)
| ~ ssNder1_2r1r1(X14644,X14645)
| ~ ssNder1_1r1(X14644)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14644,X14645,X14647,X14648,X14643,X14646,X14642,X14641,X14640)
| ssPv13_8r1r1r1r1r1r1r1r1(X14644,X14645,X14647,X14648,X14643,X14646,X14642,X14641) ),
inference(resolution,[status(thm)],[c1086,c10]) ).
cnf(c1089,plain,
( ~ ssPv19_2r1r1(X14653,X14649)
| ~ ssNder1_2r1r1(X14653,X14649)
| ~ ssNder1_1r1(X14653)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14653,X14649,X14651,X14654,X14656,X14655,X14652,X14657,X14650)
| ssPv13_8r1r1r1r1r1r1r1r1(X14653,X14649,X14651,X14654,X14656,X14655,X14652,X14657) ),
inference(resolution,[status(thm)],[c1087,c5]) ).
cnf(c1090,plain,
( ~ ssPv19_2r1r1(X14662,X14663)
| ~ ssNder1_1r1(X14662)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14662,X14663,X14658,X14661,X14664,X14666,X14665,X14660,X14659)
| ssPv13_8r1r1r1r1r1r1r1r1(X14662,X14663,X14658,X14661,X14664,X14666,X14665,X14660) ),
inference(resolution,[status(thm)],[c1089,c2]) ).
cnf(c1091,plain,
( ~ ssNder1_1r1(X14670)
| ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14670,X14672,X14667,X14675,X14668,X14674,X14673,X14669,X14671)
| ssPv13_8r1r1r1r1r1r1r1r1(X14670,X14672,X14667,X14675,X14668,X14674,X14673,X14669)
| ssPv20_1r1(X14670) ),
inference(resolution,[status(thm)],[c1090,c89]) ).
cnf(c1116,plain,
( ~ ssNder1_0
| ssPv12_9r1r1r1r1r1r1r1r1r1(X14676,X14680,X14679,X14683,X14677,X14682,X14681,X14684,X14678)
| ssPv13_8r1r1r1r1r1r1r1r1(X14676,X14680,X14679,X14683,X14677,X14682,X14681,X14684)
| ssPv20_1r1(X14676) ),
inference(resolution,[status(thm)],[c1091,c0]) ).
cnf(c1117,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X14709,X14710,X14713,X14715,X14714,X14716,X14711,X14712,X14708)
| ssPv13_8r1r1r1r1r1r1r1r1(X14709,X14710,X14713,X14715,X14714,X14716,X14711,X14712)
| ssPv20_1r1(X14709) ),
inference(resolution,[status(thm)],[c1116,clause1]) ).
cnf(c1120,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X15288,X15289,X15287,X15291,X15290,X15286,X15293,skc25,X15292)
| ssPv20_1r1(X15288)
| ~ ssNder1_6r1r1r1r1r1r1(X15288,X15289,X15287,X15291,X15290,X15286)
| ~ ssNder1_5r1r1r1r1r1(X15288,X15289,X15287,X15291,X15290)
| ~ ssNder1_4r1r1r1r1(X15288,X15289,X15287,X15291)
| ~ ssNder1_3r1r1r1(X15288,X15289,X15287)
| ~ ssNder1_2r1r1(X15288,X15289)
| ~ ssNder1_1r1(X15288)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1117,clause16]) ).
cnf(c1221,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X15300,X15294,X15298,X15301,X15296,X15295,X15297,skc25,X15299)
| ssPv20_1r1(X15300)
| ~ ssNder1_5r1r1r1r1r1(X15300,X15294,X15298,X15301,X15296)
| ~ ssNder1_4r1r1r1r1(X15300,X15294,X15298,X15301)
| ~ ssNder1_3r1r1r1(X15300,X15294,X15298)
| ~ ssNder1_2r1r1(X15300,X15294)
| ~ ssNder1_1r1(X15300)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1120,c30]) ).
cnf(c1222,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X15308,X15303,X15304,X15309,X15306,X15305,X15302,skc25,X15307)
| ssPv20_1r1(X15308)
| ~ ssNder1_4r1r1r1r1(X15308,X15303,X15304,X15309)
| ~ ssNder1_3r1r1r1(X15308,X15303,X15304)
| ~ ssNder1_2r1r1(X15308,X15303)
| ~ ssNder1_1r1(X15308)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1221,c19]) ).
cnf(c1223,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X15330,X15331,X15336,X15337,X15333,X15334,X15335,skc25,X15332)
| ssPv20_1r1(X15330)
| ~ ssNder1_3r1r1r1(X15330,X15331,X15336)
| ~ ssNder1_2r1r1(X15330,X15331)
| ~ ssNder1_1r1(X15330)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1222,c10]) ).
cnf(c1225,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X15342,X15338,X15341,X15343,X15345,X15344,X15339,skc25,X15340)
| ssPv20_1r1(X15342)
| ~ ssNder1_2r1r1(X15342,X15338)
| ~ ssNder1_1r1(X15342)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1223,c5]) ).
cnf(c1226,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X15349,X15351,X15348,X15353,X15352,X15347,X15350,skc25,X15346)
| ssPv20_1r1(X15349)
| ~ ssNder1_1r1(X15349)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1225,c2]) ).
cnf(c1227,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X15356,X15355,X15357,X15354,X15359,X15360,X15361,skc25,X15358)
| ssPv20_1r1(X15356)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1226,c0]) ).
cnf(c1228,plain,
( ssPv12_9r1r1r1r1r1r1r1r1r1(X15364,X15369,X15367,X15362,X15365,X15368,X15363,skc25,X15366)
| ssPv20_1r1(X15364) ),
inference(resolution,[status(thm)],[c1227,clause1]) ).
cnf(c1229,plain,
( ssPv20_1r1(X18118)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X18118,X18116,X18117,X18114,X18113,X18112,X18115,skc25)
| ~ ssNder1_7r1r1r1r1r1r1r1(X18118,X18116,X18117,X18114,X18113,X18112,X18115)
| ~ ssNder1_6r1r1r1r1r1r1(X18118,X18116,X18117,X18114,X18113,X18112)
| ~ ssNder1_5r1r1r1r1r1(X18118,X18116,X18117,X18114,X18113)
| ~ ssNder1_4r1r1r1r1(X18118,X18116,X18117,X18114)
| ~ ssNder1_3r1r1r1(X18118,X18116,X18117)
| ~ ssPv19_2r1r1(X18118,X18116)
| ~ ssNder1_2r1r1(X18118,X18116)
| ~ ssNder1_1r1(X18118)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X18118,X18116,X18117,X18114,X18113,X18112,X18115) ),
inference(resolution,[status(thm)],[c1228,c467]) ).
cnf(c1535,plain,
( ssPv20_1r1(X18122)
| ~ ssNder1_7r1r1r1r1r1r1r1(X18122,X18121,X18124,X18123,X18125,X18119,X18120)
| ~ ssNder1_6r1r1r1r1r1r1(X18122,X18121,X18124,X18123,X18125,X18119)
| ~ ssNder1_5r1r1r1r1r1(X18122,X18121,X18124,X18123,X18125)
| ~ ssNder1_4r1r1r1r1(X18122,X18121,X18124,X18123)
| ~ ssNder1_3r1r1r1(X18122,X18121,X18124)
| ~ ssPv19_2r1r1(X18122,X18121)
| ~ ssNder1_2r1r1(X18122,X18121)
| ~ ssNder1_1r1(X18122)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X18122,X18121,X18124,X18123,X18125,X18119,X18120) ),
inference(resolution,[status(thm)],[c1229,c58]) ).
cnf(c1536,plain,
( ssPv20_1r1(X18130)
| ~ ssNder1_6r1r1r1r1r1r1(X18130,X18128,X18131,X18132,X18126,X18127)
| ~ ssNder1_5r1r1r1r1r1(X18130,X18128,X18131,X18132,X18126)
| ~ ssNder1_4r1r1r1r1(X18130,X18128,X18131,X18132)
| ~ ssNder1_3r1r1r1(X18130,X18128,X18131)
| ~ ssPv19_2r1r1(X18130,X18128)
| ~ ssNder1_2r1r1(X18130,X18128)
| ~ ssNder1_1r1(X18130)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X18130,X18128,X18131,X18132,X18126,X18127,X18129) ),
inference(resolution,[status(thm)],[c1535,c43]) ).
cnf(c1537,plain,
( ssPv20_1r1(X18138)
| ~ ssNder1_5r1r1r1r1r1(X18138,X18133,X18137,X18139,X18136)
| ~ ssNder1_4r1r1r1r1(X18138,X18133,X18137,X18139)
| ~ ssNder1_3r1r1r1(X18138,X18133,X18137)
| ~ ssPv19_2r1r1(X18138,X18133)
| ~ ssNder1_2r1r1(X18138,X18133)
| ~ ssNder1_1r1(X18138)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X18138,X18133,X18137,X18139,X18136,X18135,X18134) ),
inference(resolution,[status(thm)],[c1536,c30]) ).
cnf(c1538,plain,
( ssPv20_1r1(X18145)
| ~ ssNder1_4r1r1r1r1(X18145,X18141,X18142,X18146)
| ~ ssNder1_3r1r1r1(X18145,X18141,X18142)
| ~ ssPv19_2r1r1(X18145,X18141)
| ~ ssNder1_2r1r1(X18145,X18141)
| ~ ssNder1_1r1(X18145)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X18145,X18141,X18142,X18146,X18144,X18140,X18143) ),
inference(resolution,[status(thm)],[c1537,c19]) ).
cnf(c1539,plain,
( ssPv20_1r1(X18159)
| ~ ssNder1_3r1r1r1(X18159,X18160,X18163)
| ~ ssPv19_2r1r1(X18159,X18160)
| ~ ssNder1_2r1r1(X18159,X18160)
| ~ ssNder1_1r1(X18159)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X18159,X18160,X18163,X18164,X18162,X18161,X18165) ),
inference(resolution,[status(thm)],[c1538,c10]) ).
cnf(c1541,plain,
( ssPv20_1r1(X18171)
| ~ ssPv19_2r1r1(X18171,X18166)
| ~ ssNder1_2r1r1(X18171,X18166)
| ~ ssNder1_1r1(X18171)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X18171,X18166,X18170,X18168,X18169,X18167,X18172) ),
inference(resolution,[status(thm)],[c1539,c5]) ).
cnf(c1542,plain,
( ssPv20_1r1(X18177)
| ~ ssPv19_2r1r1(X18177,X18178)
| ~ ssNder1_1r1(X18177)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X18177,X18178,X18179,X18175,X18173,X18174,X18176) ),
inference(resolution,[status(thm)],[c1541,c2]) ).
cnf(c1543,plain,
( ssPv20_1r1(X18183)
| ~ ssNder1_1r1(X18183)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X18183,X18184,X18181,X18185,X18182,X18180,X18186) ),
inference(resolution,[status(thm)],[c1542,c89]) ).
cnf(c1568,plain,
( ssPv20_1r1(X18189)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X18189,X18193,X18188,X18187,X18190,X18191,X18192) ),
inference(resolution,[status(thm)],[c1543,c0]) ).
cnf(c1569,plain,
( ssPv20_1r1(X18210)
| ssPv14_7r1r1r1r1r1r1r1(X18210,X18211,X18214,X18215,X18212,X18213,X18209) ),
inference(resolution,[status(thm)],[c1568,clause1]) ).
cnf(c1595,plain,
( ssPv20_1r1(X18371)
| ~ ssNder1_5r1r1r1r1r1(X18371,X18370,X18369,X18367,X18368)
| ~ ssNder1_4r1r1r1r1(X18371,X18370,X18369,X18367)
| ~ ssNder1_3r1r1r1(X18371,X18370,X18369)
| ~ ssNder1_2r1r1(X18371,X18370)
| ~ ssNder1_1r1(X18371)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1569,clause13]) ).
cnf(c1615,plain,
( ssPv20_1r1(X18373)
| ~ ssNder1_4r1r1r1r1(X18373,X18375,X18372,X18374)
| ~ ssNder1_3r1r1r1(X18373,X18375,X18372)
| ~ ssNder1_2r1r1(X18373,X18375)
| ~ ssNder1_1r1(X18373)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1595,c19]) ).
cnf(c1616,plain,
( ssPv20_1r1(X18378)
| ~ ssNder1_3r1r1r1(X18378,X18377,X18376)
| ~ ssNder1_2r1r1(X18378,X18377)
| ~ ssNder1_1r1(X18378)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1615,c10]) ).
cnf(c1617,plain,
( ssPv20_1r1(X18380)
| ~ ssNder1_2r1r1(X18380,X18379)
| ~ ssNder1_1r1(X18380)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1616,c5]) ).
cnf(c1618,plain,
( ssPv20_1r1(X18381)
| ~ ssNder1_1r1(X18381)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1617,c2]) ).
cnf(c1619,plain,
( ssPv20_1r1(X18393)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1618,c0]) ).
cnf(c1621,plain,
ssPv20_1r1(X18394),
inference(resolution,[status(thm)],[c1619,clause1]) ).
cnf(clause25,negated_conjecture,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X661,X657,X664,X663,X660,X656,X659,X662,X658)
| ~ ssPv11_10r1r1r1r1r1r1r1r1r1r1(X661,X657,X664,X663,X660,X656,X659,X662,X658,X665)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X661,X657,X664,X663,X660,X656,X659,X662)
| ~ ssNder1_7r1r1r1r1r1r1r1(X661,X657,X664,X663,X660,X656,X659)
| ~ ssNder1_6r1r1r1r1r1r1(X661,X657,X664,X663,X660,X656)
| ~ ssNder1_5r1r1r1r1r1(X661,X657,X664,X663,X660)
| ~ ssNder1_4r1r1r1r1(X661,X657,X664,X663)
| ~ ssNder1_3r1r1r1(X661,X657,X664)
| ~ ssNder1_2r1r1(X661,X657)
| ~ ssPv20_1r1(X661)
| ~ ssNder1_1r1(X661)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X661,X657,X664,X663,X660,X656,X659)
| ssPv15_6r1r1r1r1r1r1(X661,X657,X664,X663,X660,X656) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(clause12,negated_conjecture,
( ~ ssNder1_5r1r1r1r1r1(X140,X138,X142,X141,X139)
| ~ ssNder1_4r1r1r1r1(X140,X138,X142,X141)
| ~ ssNder1_3r1r1r1(X140,X138,X142)
| ~ ssNder1_2r1r1(X140,X138)
| ~ ssNder1_1r1(X140)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X140,X138,X142,X141,X139,X137,skc26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c25,plain,
( ~ ssNder1_4r1r1r1r1(X188,X185,X186,X189)
| ~ ssNder1_3r1r1r1(X188,X185,X186)
| ~ ssNder1_2r1r1(X188,X185)
| ~ ssNder1_1r1(X188)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X188,X185,X186,X189,X187,X190,skc26) ),
inference(resolution,[status(thm)],[clause12,c19]) ).
cnf(c31,plain,
( ~ ssNder1_3r1r1r1(X192,X193,X195)
| ~ ssNder1_2r1r1(X192,X193)
| ~ ssNder1_1r1(X192)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X192,X193,X195,X196,X194,X191,skc26) ),
inference(resolution,[status(thm)],[c25,c10]) ).
cnf(c32,plain,
( ~ ssNder1_2r1r1(X199,X197)
| ~ ssNder1_1r1(X199)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X199,X197,X198,X200,X202,X201,skc26) ),
inference(resolution,[status(thm)],[c31,c5]) ).
cnf(c33,plain,
( ~ ssNder1_1r1(X204)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X204,X206,X205,X208,X207,X203,skc26) ),
inference(resolution,[status(thm)],[c32,c2]) ).
cnf(c34,plain,
( ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X218,X217,X220,X216,X221,X219,skc26) ),
inference(resolution,[status(thm)],[c33,c0]) ).
cnf(c36,plain,
ssPv14_7r1r1r1r1r1r1r1(X222,X225,X223,X227,X226,X224,skc26),
inference(resolution,[status(thm)],[c34,clause1]) ).
cnf(clause37,negated_conjecture,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1368,X1363,X1371,X1370,X1367,X1362,X1366,X1369,X1364,X1373,X1361,X1372)
| ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1368,X1363,X1371,X1370,X1367,X1362,X1366,X1369,X1364,X1373,X1361,X1372,X1365)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1368,X1363,X1371,X1370,X1367,X1362,X1366,X1369,X1364,X1373,X1361)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1368,X1363,X1371,X1370,X1367,X1362,X1366,X1369,X1364,X1373)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1368,X1363,X1371,X1370,X1367,X1362,X1366,X1369,X1364)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1368,X1363,X1371,X1370,X1367,X1362,X1366,X1369)
| ~ ssPv14_7r1r1r1r1r1r1r1(X1368,X1363,X1371,X1370,X1367,X1362,X1366)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1368,X1363,X1371,X1370,X1367,X1362,X1366)
| ~ ssNder1_6r1r1r1r1r1r1(X1368,X1363,X1371,X1370,X1367,X1362)
| ~ ssNder1_5r1r1r1r1r1(X1368,X1363,X1371,X1370,X1367)
| ~ ssNder1_4r1r1r1r1(X1368,X1363,X1371,X1370)
| ~ ssNder1_3r1r1r1(X1368,X1363,X1371)
| ~ ssPv19_2r1r1(X1368,X1363)
| ~ ssNder1_2r1r1(X1368,X1363)
| ~ ssPv20_1r1(X1368)
| ~ ssNder1_1r1(X1368)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(clause28,negated_conjecture,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X807,X803,X810,X809,X806,X802,X805,X808,X804,X812,X801)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X807,X803,X810,X809,X806,X802,X805,X808,X804,X812)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X807,X803,X810,X809,X806,X802,X805,X808,X804)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X807,X803,X810,X809,X806,X802,X805,X808)
| ~ ssNder1_7r1r1r1r1r1r1r1(X807,X803,X810,X809,X806,X802,X805)
| ~ ssNder1_6r1r1r1r1r1r1(X807,X803,X810,X809,X806,X802)
| ~ ssNder1_5r1r1r1r1r1(X807,X803,X810,X809,X806)
| ~ ssNder1_4r1r1r1r1(X807,X803,X810,X809)
| ~ ssNder1_3r1r1r1(X807,X803,X810)
| ~ ssNder1_2r1r1(X807,X803)
| ~ ssNder1_1r1(X807)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X807,X803,X810,X809,X806,X802,X805,X808,X804,X812,X801,X811,skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c137,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1341,X1347,X1337,X1338,X1342,X1348,X1340,X1339,X1346,X1344)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1341,X1347,X1337,X1338,X1342,X1348,X1340,X1339,X1346)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1341,X1347,X1337,X1338,X1342,X1348,X1340,X1339)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1341,X1347,X1337,X1338,X1342,X1348,X1340)
| ~ ssNder1_6r1r1r1r1r1r1(X1341,X1347,X1337,X1338,X1342,X1348)
| ~ ssNder1_5r1r1r1r1r1(X1341,X1347,X1337,X1338,X1342)
| ~ ssNder1_4r1r1r1r1(X1341,X1347,X1337,X1338)
| ~ ssNder1_3r1r1r1(X1341,X1347,X1337)
| ~ ssNder1_2r1r1(X1341,X1347)
| ~ ssNder1_1r1(X1341)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1341,X1347,X1337,X1338,X1342,X1348,X1340,X1339,X1346,X1344,X1345,X1343,skc22) ),
inference(resolution,[status(thm)],[c135,clause28]) ).
cnf(c151,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1353,X1358,X1359,X1355,X1351,X1349,X1352,X1357,X1356)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1353,X1358,X1359,X1355,X1351,X1349,X1352,X1357)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1353,X1358,X1359,X1355,X1351,X1349,X1352)
| ~ ssNder1_6r1r1r1r1r1r1(X1353,X1358,X1359,X1355,X1351,X1349)
| ~ ssNder1_5r1r1r1r1r1(X1353,X1358,X1359,X1355,X1351)
| ~ ssNder1_4r1r1r1r1(X1353,X1358,X1359,X1355)
| ~ ssNder1_3r1r1r1(X1353,X1358,X1359)
| ~ ssNder1_2r1r1(X1353,X1358)
| ~ ssNder1_1r1(X1353)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1353,X1358,X1359,X1355,X1351,X1349,X1352,X1357,X1356,X1360,X1354,X1350,skc22) ),
inference(resolution,[status(thm)],[c137,c106]) ).
cnf(c152,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X1384,X1383,X1375,X1379,X1377,X1374,X1380,X1378)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1384,X1383,X1375,X1379,X1377,X1374,X1380)
| ~ ssNder1_6r1r1r1r1r1r1(X1384,X1383,X1375,X1379,X1377,X1374)
| ~ ssNder1_5r1r1r1r1r1(X1384,X1383,X1375,X1379,X1377)
| ~ ssNder1_4r1r1r1r1(X1384,X1383,X1375,X1379)
| ~ ssNder1_3r1r1r1(X1384,X1383,X1375)
| ~ ssNder1_2r1r1(X1384,X1383)
| ~ ssNder1_1r1(X1384)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1384,X1383,X1375,X1379,X1377,X1374,X1380,X1378,X1376,X1382,X1385,X1381,skc22) ),
inference(resolution,[status(thm)],[c151,c73]) ).
cnf(c153,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X1391,X1390,X1394,X1392,X1397,X1387,X1388)
| ~ ssNder1_6r1r1r1r1r1r1(X1391,X1390,X1394,X1392,X1397,X1387)
| ~ ssNder1_5r1r1r1r1r1(X1391,X1390,X1394,X1392,X1397)
| ~ ssNder1_4r1r1r1r1(X1391,X1390,X1394,X1392)
| ~ ssNder1_3r1r1r1(X1391,X1390,X1394)
| ~ ssNder1_2r1r1(X1391,X1390)
| ~ ssNder1_1r1(X1391)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1391,X1390,X1394,X1392,X1397,X1387,X1388,X1386,X1389,X1393,X1395,X1396,skc22) ),
inference(resolution,[status(thm)],[c152,c58]) ).
cnf(c154,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X1405,X1401,X1408,X1409,X1398,X1400)
| ~ ssNder1_5r1r1r1r1r1(X1405,X1401,X1408,X1409,X1398)
| ~ ssNder1_4r1r1r1r1(X1405,X1401,X1408,X1409)
| ~ ssNder1_3r1r1r1(X1405,X1401,X1408)
| ~ ssNder1_2r1r1(X1405,X1401)
| ~ ssNder1_1r1(X1405)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1405,X1401,X1408,X1409,X1398,X1400,X1404,X1407,X1399,X1406,X1402,X1403,skc22) ),
inference(resolution,[status(thm)],[c153,c43]) ).
cnf(c155,plain,
( ~ ssNder1_5r1r1r1r1r1(X1418,X1410,X1416,X1421,X1414)
| ~ ssNder1_4r1r1r1r1(X1418,X1410,X1416,X1421)
| ~ ssNder1_3r1r1r1(X1418,X1410,X1416)
| ~ ssNder1_2r1r1(X1418,X1410)
| ~ ssNder1_1r1(X1418)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1418,X1410,X1416,X1421,X1414,X1413,X1415,X1420,X1411,X1419,X1412,X1417,skc22) ),
inference(resolution,[status(thm)],[c154,c30]) ).
cnf(c156,plain,
( ~ ssNder1_4r1r1r1r1(X1432,X1424,X1425,X1433)
| ~ ssNder1_3r1r1r1(X1432,X1424,X1425)
| ~ ssNder1_2r1r1(X1432,X1424)
| ~ ssNder1_1r1(X1432)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1432,X1424,X1425,X1433,X1430,X1427,X1431,X1428,X1426,X1423,X1429,X1422,skc22) ),
inference(resolution,[status(thm)],[c155,c19]) ).
cnf(c157,plain,
( ~ ssNder1_3r1r1r1(X1451,X1452,X1457)
| ~ ssNder1_2r1r1(X1451,X1452)
| ~ ssNder1_1r1(X1451)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1451,X1452,X1457,X1458,X1455,X1448,X1459,X1453,X1456,X1450,X1449,X1454,skc22) ),
inference(resolution,[status(thm)],[c156,c10]) ).
cnf(c158,plain,
( ~ ssNder1_2r1r1(X1468,X1460)
| ~ ssNder1_1r1(X1468)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1468,X1460,X1466,X1471,X1470,X1463,X1469,X1465,X1464,X1461,X1467,X1462,skc22) ),
inference(resolution,[status(thm)],[c157,c5]) ).
cnf(c159,plain,
( ~ ssNder1_1r1(X1474)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1474,X1475,X1477,X1483,X1479,X1480,X1476,X1478,X1481,X1482,X1472,X1473,skc22) ),
inference(resolution,[status(thm)],[c158,c2]) ).
cnf(c160,plain,
( ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1488,X1486,X1495,X1494,X1485,X1489,X1484,X1487,X1491,X1492,X1493,X1490,skc22) ),
inference(resolution,[status(thm)],[c159,c0]) ).
cnf(c161,plain,
ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1502,X1504,X1500,X1497,X1496,X1499,X1507,X1506,X1503,X1498,X1505,X1501,skc22),
inference(resolution,[status(thm)],[c160,clause1]) ).
cnf(c162,plain,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X3268,X3274,X3270,X3279,X3276,X3277,X3272,X3269,X3273,X3275,X3271,X3278)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X3268,X3274,X3270,X3279,X3276,X3277,X3272,X3269,X3273,X3275,X3271)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3268,X3274,X3270,X3279,X3276,X3277,X3272,X3269,X3273,X3275)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3268,X3274,X3270,X3279,X3276,X3277,X3272,X3269,X3273)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3268,X3274,X3270,X3279,X3276,X3277,X3272,X3269)
| ~ ssPv14_7r1r1r1r1r1r1r1(X3268,X3274,X3270,X3279,X3276,X3277,X3272)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3268,X3274,X3270,X3279,X3276,X3277,X3272)
| ~ ssNder1_6r1r1r1r1r1r1(X3268,X3274,X3270,X3279,X3276,X3277)
| ~ ssNder1_5r1r1r1r1r1(X3268,X3274,X3270,X3279,X3276)
| ~ ssNder1_4r1r1r1r1(X3268,X3274,X3270,X3279)
| ~ ssNder1_3r1r1r1(X3268,X3274,X3270)
| ~ ssPv19_2r1r1(X3268,X3274)
| ~ ssNder1_2r1r1(X3268,X3274)
| ~ ssPv20_1r1(X3268)
| ~ ssNder1_1r1(X3268)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c161,clause37]) ).
cnf(c271,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X3283,X3282,X3281,X3289,X3280,X3286,X3287,X3290,X3288,X3285,X3284)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3283,X3282,X3281,X3289,X3280,X3286,X3287,X3290,X3288,X3285)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3283,X3282,X3281,X3289,X3280,X3286,X3287,X3290,X3288)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3283,X3282,X3281,X3289,X3280,X3286,X3287,X3290)
| ~ ssPv14_7r1r1r1r1r1r1r1(X3283,X3282,X3281,X3289,X3280,X3286,X3287)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3283,X3282,X3281,X3289,X3280,X3286,X3287)
| ~ ssNder1_6r1r1r1r1r1r1(X3283,X3282,X3281,X3289,X3280,X3286)
| ~ ssNder1_5r1r1r1r1r1(X3283,X3282,X3281,X3289,X3280)
| ~ ssNder1_4r1r1r1r1(X3283,X3282,X3281,X3289)
| ~ ssNder1_3r1r1r1(X3283,X3282,X3281)
| ~ ssPv19_2r1r1(X3283,X3282)
| ~ ssNder1_2r1r1(X3283,X3282)
| ~ ssPv20_1r1(X3283)
| ~ ssNder1_1r1(X3283)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c162,c148]) ).
cnf(c272,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3293,X3297,X3296,X3294,X3295,X3299,X3298,X3291,X3292,X3300)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3293,X3297,X3296,X3294,X3295,X3299,X3298,X3291,X3292)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3293,X3297,X3296,X3294,X3295,X3299,X3298,X3291)
| ~ ssPv14_7r1r1r1r1r1r1r1(X3293,X3297,X3296,X3294,X3295,X3299,X3298)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3293,X3297,X3296,X3294,X3295,X3299,X3298)
| ~ ssNder1_6r1r1r1r1r1r1(X3293,X3297,X3296,X3294,X3295,X3299)
| ~ ssNder1_5r1r1r1r1r1(X3293,X3297,X3296,X3294,X3295)
| ~ ssNder1_4r1r1r1r1(X3293,X3297,X3296,X3294)
| ~ ssNder1_3r1r1r1(X3293,X3297,X3296)
| ~ ssPv19_2r1r1(X3293,X3297)
| ~ ssNder1_2r1r1(X3293,X3297)
| ~ ssPv20_1r1(X3293)
| ~ ssNder1_1r1(X3293)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c271,c135]) ).
cnf(c273,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3304,X3308,X3309,X3305,X3302,X3301,X3303,X3307,X3306)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3304,X3308,X3309,X3305,X3302,X3301,X3303,X3307)
| ~ ssPv14_7r1r1r1r1r1r1r1(X3304,X3308,X3309,X3305,X3302,X3301,X3303)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3304,X3308,X3309,X3305,X3302,X3301,X3303)
| ~ ssNder1_6r1r1r1r1r1r1(X3304,X3308,X3309,X3305,X3302,X3301)
| ~ ssNder1_5r1r1r1r1r1(X3304,X3308,X3309,X3305,X3302)
| ~ ssNder1_4r1r1r1r1(X3304,X3308,X3309,X3305)
| ~ ssNder1_3r1r1r1(X3304,X3308,X3309)
| ~ ssPv19_2r1r1(X3304,X3308)
| ~ ssNder1_2r1r1(X3304,X3308)
| ~ ssPv20_1r1(X3304)
| ~ ssNder1_1r1(X3304)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c272,c106]) ).
cnf(c274,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X3317,X3316,X3311,X3314,X3312,X3310,X3315,X3313)
| ~ ssPv14_7r1r1r1r1r1r1r1(X3317,X3316,X3311,X3314,X3312,X3310,X3315)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3317,X3316,X3311,X3314,X3312,X3310,X3315)
| ~ ssNder1_6r1r1r1r1r1r1(X3317,X3316,X3311,X3314,X3312,X3310)
| ~ ssNder1_5r1r1r1r1r1(X3317,X3316,X3311,X3314,X3312)
| ~ ssNder1_4r1r1r1r1(X3317,X3316,X3311,X3314)
| ~ ssNder1_3r1r1r1(X3317,X3316,X3311)
| ~ ssPv19_2r1r1(X3317,X3316)
| ~ ssNder1_2r1r1(X3317,X3316)
| ~ ssPv20_1r1(X3317)
| ~ ssNder1_1r1(X3317)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c273,c73]) ).
cnf(c275,plain,
( ~ ssPv14_7r1r1r1r1r1r1r1(X3338,X3337,X3340,X3339,X3341,X3335,X3336)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3338,X3337,X3340,X3339,X3341,X3335,X3336)
| ~ ssNder1_6r1r1r1r1r1r1(X3338,X3337,X3340,X3339,X3341,X3335)
| ~ ssNder1_5r1r1r1r1r1(X3338,X3337,X3340,X3339,X3341)
| ~ ssNder1_4r1r1r1r1(X3338,X3337,X3340,X3339)
| ~ ssNder1_3r1r1r1(X3338,X3337,X3340)
| ~ ssPv19_2r1r1(X3338,X3337)
| ~ ssNder1_2r1r1(X3338,X3337)
| ~ ssPv20_1r1(X3338)
| ~ ssNder1_1r1(X3338)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c274,c58]) ).
cnf(c276,plain,
( ~ ssPv14_7r1r1r1r1r1r1r1(X3346,X3344,X3347,X3348,X3342,X3343,X3345)
| ~ ssNder1_6r1r1r1r1r1r1(X3346,X3344,X3347,X3348,X3342,X3343)
| ~ ssNder1_5r1r1r1r1r1(X3346,X3344,X3347,X3348,X3342)
| ~ ssNder1_4r1r1r1r1(X3346,X3344,X3347,X3348)
| ~ ssNder1_3r1r1r1(X3346,X3344,X3347)
| ~ ssPv19_2r1r1(X3346,X3344)
| ~ ssNder1_2r1r1(X3346,X3344)
| ~ ssPv20_1r1(X3346)
| ~ ssNder1_1r1(X3346)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c275,c43]) ).
cnf(c277,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X3349,X3352,X3351,X3350,X3353,X3354)
| ~ ssNder1_5r1r1r1r1r1(X3349,X3352,X3351,X3350,X3353)
| ~ ssNder1_4r1r1r1r1(X3349,X3352,X3351,X3350)
| ~ ssNder1_3r1r1r1(X3349,X3352,X3351)
| ~ ssPv19_2r1r1(X3349,X3352)
| ~ ssNder1_2r1r1(X3349,X3352)
| ~ ssPv20_1r1(X3349)
| ~ ssNder1_1r1(X3349)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c276,c36]) ).
cnf(c278,plain,
( ~ ssNder1_5r1r1r1r1r1(X3358,X3355,X3357,X3359,X3356)
| ~ ssNder1_4r1r1r1r1(X3358,X3355,X3357,X3359)
| ~ ssNder1_3r1r1r1(X3358,X3355,X3357)
| ~ ssPv19_2r1r1(X3358,X3355)
| ~ ssNder1_2r1r1(X3358,X3355)
| ~ ssPv20_1r1(X3358)
| ~ ssNder1_1r1(X3358)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c277,c30]) ).
cnf(c279,plain,
( ~ ssNder1_4r1r1r1r1(X3361,X3363,X3360,X3362)
| ~ ssNder1_3r1r1r1(X3361,X3363,X3360)
| ~ ssPv19_2r1r1(X3361,X3363)
| ~ ssNder1_2r1r1(X3361,X3363)
| ~ ssPv20_1r1(X3361)
| ~ ssNder1_1r1(X3361)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c278,c19]) ).
cnf(c280,plain,
( ~ ssNder1_3r1r1r1(X3383,X3382,X3381)
| ~ ssPv19_2r1r1(X3383,X3382)
| ~ ssNder1_2r1r1(X3383,X3382)
| ~ ssPv20_1r1(X3383)
| ~ ssNder1_1r1(X3383)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c279,c10]) ).
cnf(c281,plain,
( ~ ssPv19_2r1r1(X3385,X3384)
| ~ ssNder1_2r1r1(X3385,X3384)
| ~ ssPv20_1r1(X3385)
| ~ ssNder1_1r1(X3385)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c280,c5]) ).
cnf(c282,plain,
( ~ ssPv19_2r1r1(X3386,X3387)
| ~ ssPv20_1r1(X3386)
| ~ ssNder1_1r1(X3386)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c281,c2]) ).
cnf(clause29,negated_conjecture,
( ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X866,X862,X869,X868,X865,X861,X864,X867,X863,X871,X860,X870,skc23)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X866,X862,X869,X868,X865,X861,X864,X867,X863,X871,X860)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X866,X862,X869,X868,X865,X861,X864,X867,X863,X871)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X866,X862,X869,X868,X865,X861,X864,X867,X863)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X866,X862,X869,X868,X865,X861,X864,X867)
| ~ ssNder1_7r1r1r1r1r1r1r1(X866,X862,X869,X868,X865,X861,X864)
| ~ ssNder1_6r1r1r1r1r1r1(X866,X862,X869,X868,X865,X861)
| ~ ssNder1_5r1r1r1r1r1(X866,X862,X869,X868,X865)
| ~ ssNder1_4r1r1r1r1(X866,X862,X869,X868)
| ~ ssNder1_3r1r1r1(X866,X862,X869)
| ~ ssNder1_2r1r1(X866,X862)
| ~ ssNder1_1r1(X866)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(clause30,negated_conjecture,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X919,X915,X922,X921,X918,X914,X917,X920,X916,X923)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X919,X915,X922,X921,X918,X914,X917,X920,X916)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X919,X915,X922,X921,X918,X914,X917,X920)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X919,X915,X922,X921,X918,X914,X917,X920)
| ~ ssNder1_7r1r1r1r1r1r1r1(X919,X915,X922,X921,X918,X914,X917)
| ~ ssNder1_6r1r1r1r1r1r1(X919,X915,X922,X921,X918,X914)
| ~ ssNder1_5r1r1r1r1r1(X919,X915,X922,X921,X918)
| ~ ssNder1_4r1r1r1r1(X919,X915,X922,X921)
| ~ ssNder1_3r1r1r1(X919,X915,X922)
| ~ ssNder1_2r1r1(X919,X915)
| ~ ssPv20_1r1(X919)
| ~ ssNder1_1r1(X919)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X919,X915,X922,X921,X918,X914,X917,X920,X916,X923,X913)
| ssPv16_5r1r1r1r1r1(X919,X915,X922,X921,X918) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c116,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1525,X1529,X1530,X1526,X1523,X1522,X1524,X1528,X1527)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X1525,X1529,X1530,X1526,X1523,X1522,X1524,X1528)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1525,X1529,X1530,X1526,X1523,X1522,X1524,X1528)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1525,X1529,X1530,X1526,X1523,X1522,X1524)
| ~ ssNder1_6r1r1r1r1r1r1(X1525,X1529,X1530,X1526,X1523,X1522)
| ~ ssNder1_5r1r1r1r1r1(X1525,X1529,X1530,X1526,X1523)
| ~ ssNder1_4r1r1r1r1(X1525,X1529,X1530,X1526)
| ~ ssNder1_3r1r1r1(X1525,X1529,X1530)
| ~ ssNder1_2r1r1(X1525,X1529)
| ~ ssPv20_1r1(X1525)
| ~ ssNder1_1r1(X1525)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1525,X1529,X1530,X1526,X1523,X1522,X1524,X1528,X1527,X1532,X1531)
| ssPv16_5r1r1r1r1r1(X1525,X1529,X1530,X1526,X1523) ),
inference(resolution,[status(thm)],[clause30,c106]) ).
cnf(c163,plain,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X1543,X1542,X1534,X1540,X1538,X1533,X1541,X1539)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1543,X1542,X1534,X1540,X1538,X1533,X1541,X1539)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1543,X1542,X1534,X1540,X1538,X1533,X1541)
| ~ ssNder1_6r1r1r1r1r1r1(X1543,X1542,X1534,X1540,X1538,X1533)
| ~ ssNder1_5r1r1r1r1r1(X1543,X1542,X1534,X1540,X1538)
| ~ ssNder1_4r1r1r1r1(X1543,X1542,X1534,X1540)
| ~ ssNder1_3r1r1r1(X1543,X1542,X1534)
| ~ ssNder1_2r1r1(X1543,X1542)
| ~ ssPv20_1r1(X1543)
| ~ ssNder1_1r1(X1543)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1543,X1542,X1534,X1540,X1538,X1533,X1541,X1539,X1535,X1536,X1537)
| ssPv16_5r1r1r1r1r1(X1543,X1542,X1534,X1540,X1538) ),
inference(resolution,[status(thm)],[c116,c73]) ).
cnf(c164,plain,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X1549,X1548,X1552,X1550,X1554,X1546,X1547,X1545)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1549,X1548,X1552,X1550,X1554,X1546,X1547)
| ~ ssNder1_6r1r1r1r1r1r1(X1549,X1548,X1552,X1550,X1554,X1546)
| ~ ssNder1_5r1r1r1r1r1(X1549,X1548,X1552,X1550,X1554)
| ~ ssNder1_4r1r1r1r1(X1549,X1548,X1552,X1550)
| ~ ssNder1_3r1r1r1(X1549,X1548,X1552)
| ~ ssNder1_2r1r1(X1549,X1548)
| ~ ssPv20_1r1(X1549)
| ~ ssNder1_1r1(X1549)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1549,X1548,X1552,X1550,X1554,X1546,X1547,X1545,X1551,X1544,X1553)
| ssPv16_5r1r1r1r1r1(X1549,X1548,X1552,X1550,X1554) ),
inference(resolution,[status(thm)],[c163,c58]) ).
cnf(c165,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X1559,X1562,X1555,X1564,X1563,X1558,X1561)
| ~ ssNder1_6r1r1r1r1r1r1(X1559,X1562,X1555,X1564,X1563,X1558)
| ~ ssNder1_5r1r1r1r1r1(X1559,X1562,X1555,X1564,X1563)
| ~ ssNder1_4r1r1r1r1(X1559,X1562,X1555,X1564)
| ~ ssNder1_3r1r1r1(X1559,X1562,X1555)
| ~ ssNder1_2r1r1(X1559,X1562)
| ~ ssPv20_1r1(X1559)
| ~ ssNder1_1r1(X1559)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1559,X1562,X1555,X1564,X1563,X1558,X1561,skc24,X1560,X1556,X1557)
| ssPv16_5r1r1r1r1r1(X1559,X1562,X1555,X1564,X1563) ),
inference(resolution,[status(thm)],[c164,c49]) ).
cnf(c166,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X1572,X1567,X1573,X1574,X1565,X1566)
| ~ ssNder1_5r1r1r1r1r1(X1572,X1567,X1573,X1574,X1565)
| ~ ssNder1_4r1r1r1r1(X1572,X1567,X1573,X1574)
| ~ ssNder1_3r1r1r1(X1572,X1567,X1573)
| ~ ssNder1_2r1r1(X1572,X1567)
| ~ ssPv20_1r1(X1572)
| ~ ssNder1_1r1(X1572)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1572,X1567,X1573,X1574,X1565,X1566,X1570,skc24,X1569,X1568,X1571)
| ssPv16_5r1r1r1r1r1(X1572,X1567,X1573,X1574,X1565) ),
inference(resolution,[status(thm)],[c165,c43]) ).
cnf(c167,plain,
( ~ ssNder1_5r1r1r1r1r1(X1595,X1589,X1593,X1597,X1591)
| ~ ssNder1_4r1r1r1r1(X1595,X1589,X1593,X1597)
| ~ ssNder1_3r1r1r1(X1595,X1589,X1593)
| ~ ssNder1_2r1r1(X1595,X1589)
| ~ ssPv20_1r1(X1595)
| ~ ssNder1_1r1(X1595)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1595,X1589,X1593,X1597,X1591,X1590,X1596,skc24,X1592,X1594,X1588)
| ssPv16_5r1r1r1r1r1(X1595,X1589,X1593,X1597,X1591) ),
inference(resolution,[status(thm)],[c166,c30]) ).
cnf(c169,plain,
( ~ ssNder1_4r1r1r1r1(X1606,X1602,X1603,X1607)
| ~ ssNder1_3r1r1r1(X1606,X1602,X1603)
| ~ ssNder1_2r1r1(X1606,X1602)
| ~ ssPv20_1r1(X1606)
| ~ ssNder1_1r1(X1606)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1606,X1602,X1603,X1607,X1604,X1598,X1601,skc24,X1599,X1600,X1605)
| ssPv16_5r1r1r1r1r1(X1606,X1602,X1603,X1607,X1604) ),
inference(resolution,[status(thm)],[c167,c19]) ).
cnf(c170,plain,
( ~ ssNder1_3r1r1r1(X1610,X1611,X1615)
| ~ ssNder1_2r1r1(X1610,X1611)
| ~ ssPv20_1r1(X1610)
| ~ ssNder1_1r1(X1610)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1610,X1611,X1615,X1616,X1617,X1613,X1612,skc24,X1608,X1614,X1609)
| ssPv16_5r1r1r1r1r1(X1610,X1611,X1615,X1616,X1617) ),
inference(resolution,[status(thm)],[c169,c10]) ).
cnf(c171,plain,
( ~ ssNder1_2r1r1(X1622,X1618)
| ~ ssPv20_1r1(X1622)
| ~ ssNder1_1r1(X1622)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1622,X1618,X1620,X1621,X1625,X1623,X1624,skc24,X1619,X1627,X1626)
| ssPv16_5r1r1r1r1r1(X1622,X1618,X1620,X1621,X1625) ),
inference(resolution,[status(thm)],[c170,c5]) ).
cnf(c172,plain,
( ~ ssPv20_1r1(X1630)
| ~ ssNder1_1r1(X1630)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1630,X1632,X1629,X1637,X1636,X1635,X1631,skc24,X1633,X1628,X1634)
| ssPv16_5r1r1r1r1r1(X1630,X1632,X1629,X1637,X1636) ),
inference(resolution,[status(thm)],[c171,c2]) ).
cnf(c173,plain,
( ~ ssPv20_1r1(X1651)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1651,X1659,X1655,X1657,X1654,X1658,X1652,skc24,X1660,X1653,X1656)
| ssPv16_5r1r1r1r1r1(X1651,X1659,X1655,X1657,X1654) ),
inference(resolution,[status(thm)],[c172,c0]) ).
cnf(c175,plain,
( ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1664,X1661,X1662,X1671,X1663,X1665,X1670,skc24,X1666,X1669,X1667)
| ssPv16_5r1r1r1r1r1(X1664,X1661,X1662,X1671,X1663)
| ssPv19_2r1r1(X1664,X1668) ),
inference(resolution,[status(thm)],[c173,c89]) ).
cnf(c177,plain,
( ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1672,X1674,X1678,X1679,X1677,X1681,X1680,skc24,X1675,X1676,X1682)
| ssPv16_5r1r1r1r1r1(X1672,X1674,X1678,X1679,X1677)
| ssPv19_2r1r1(X1672,X1673) ),
inference(resolution,[status(thm)],[c175,clause1]) ).
cnf(clause42,negated_conjecture,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710,X1714,X1717,X1712,X1721,X1709,X1720)
| ~ ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710,X1714,X1717,X1712,X1721,X1709)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710,X1714,X1717,X1712,X1721,X1709)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710,X1714,X1717,X1712,X1721)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710,X1714,X1717,X1712)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710,X1714,X1717)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710,X1714)
| ~ ssNder1_6r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710)
| ~ ssNder1_5r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715)
| ~ ssNder1_4r1r1r1r1(X1716,X1711,X1719,X1718)
| ~ ssNder1_3r1r1r1(X1716,X1711,X1719)
| ~ ssNder1_2r1r1(X1716,X1711)
| ~ ssNder1_1r1(X1716)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710,X1714,X1717,X1712,X1721,X1709,X1720,X1713)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710,X1714,X1717,X1712,X1721)
| ssPv14_7r1r1r1r1r1r1r1(X1716,X1711,X1719,X1718,X1715,X1710,X1714) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c184,plain,
( ~ ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100,X5108,X5109,X5112,X5110,X5107,X5105)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100,X5108,X5109,X5112,X5110,X5107,X5105)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100,X5108,X5109,X5112,X5110,X5107)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100,X5108,X5109,X5112,X5110)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100,X5108,X5109,X5112)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100,X5108,X5109)
| ~ ssNder1_6r1r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100,X5108)
| ~ ssNder1_5r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100)
| ~ ssNder1_4r1r1r1r1(X5104,X5103,X5102,X5111)
| ~ ssNder1_3r1r1r1(X5104,X5103,X5102)
| ~ ssNder1_2r1r1(X5104,X5103)
| ~ ssNder1_1r1(X5104)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100,X5108,X5109,X5112,X5110,X5107,X5105,X5106,X5101)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100,X5108,X5109,X5112,X5110,X5107)
| ssPv14_7r1r1r1r1r1r1r1(X5104,X5103,X5102,X5111,X5100,X5108,X5109) ),
inference(resolution,[status(thm)],[clause42,c148]) ).
cnf(c407,plain,
( ~ ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X5631,X5636,X5635,X5632,X5634,X5638,X5637,X5628,X5629,X5639,X5633)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5631,X5636,X5635,X5632,X5634,X5638,X5637,X5628,X5629,X5639)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5631,X5636,X5635,X5632,X5634,X5638,X5637,X5628,X5629)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5631,X5636,X5635,X5632,X5634,X5638,X5637,X5628)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5631,X5636,X5635,X5632,X5634,X5638,X5637)
| ~ ssNder1_6r1r1r1r1r1r1(X5631,X5636,X5635,X5632,X5634,X5638)
| ~ ssNder1_5r1r1r1r1r1(X5631,X5636,X5635,X5632,X5634)
| ~ ssNder1_4r1r1r1r1(X5631,X5636,X5635,X5632)
| ~ ssNder1_3r1r1r1(X5631,X5636,X5635)
| ~ ssNder1_2r1r1(X5631,X5636)
| ~ ssNder1_1r1(X5631)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X5631,X5636,X5635,X5632,X5634,X5638,X5637,X5628,X5629,X5639,X5633,X5627,X5630)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X5631,X5636,X5635,X5632,X5634,X5638,X5637,X5628,X5629,X5639)
| ssPv14_7r1r1r1r1r1r1r1(X5631,X5636,X5635,X5632,X5634,X5638,X5637) ),
inference(resolution,[status(thm)],[c184,c135]) ).
cnf(c449,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X6205,X6209,X6203,X6204,X6200,X6207,X6201,skc24,X6210,X6206)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X6205,X6209,X6203,X6204,X6200,X6207,X6201,skc24,X6210)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X6205,X6209,X6203,X6204,X6200,X6207,X6201,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X6205,X6209,X6203,X6204,X6200,X6207,X6201)
| ~ ssNder1_6r1r1r1r1r1r1(X6205,X6209,X6203,X6204,X6200,X6207)
| ~ ssNder1_5r1r1r1r1r1(X6205,X6209,X6203,X6204,X6200)
| ~ ssNder1_4r1r1r1r1(X6205,X6209,X6203,X6204)
| ~ ssNder1_3r1r1r1(X6205,X6209,X6203)
| ~ ssNder1_2r1r1(X6205,X6209)
| ~ ssNder1_1r1(X6205)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X6205,X6209,X6203,X6204,X6200,X6207,X6201,skc24,X6210,X6206,X6202,X6208,X6212)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X6205,X6209,X6203,X6204,X6200,X6207,X6201,skc24,X6210,X6206)
| ssPv14_7r1r1r1r1r1r1r1(X6205,X6209,X6203,X6204,X6200,X6207,X6201)
| ssPv16_5r1r1r1r1r1(X6205,X6209,X6203,X6204,X6200)
| ssPv19_2r1r1(X6205,X6211) ),
inference(resolution,[status(thm)],[c407,c177]) ).
cnf(c504,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X6939,X6942,X6943,X6940,X6937,X6936,X6938,skc24,X6941)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X6939,X6942,X6943,X6940,X6937,X6936,X6938,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X6939,X6942,X6943,X6940,X6937,X6936,X6938)
| ~ ssNder1_6r1r1r1r1r1r1(X6939,X6942,X6943,X6940,X6937,X6936)
| ~ ssNder1_5r1r1r1r1r1(X6939,X6942,X6943,X6940,X6937)
| ~ ssNder1_4r1r1r1r1(X6939,X6942,X6943,X6940)
| ~ ssNder1_3r1r1r1(X6939,X6942,X6943)
| ~ ssNder1_2r1r1(X6939,X6942)
| ~ ssNder1_1r1(X6939)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X6939,X6942,X6943,X6940,X6937,X6936,X6938,skc24,X6941,X6946,X6947,X6944,X6948)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X6939,X6942,X6943,X6940,X6937,X6936,X6938,skc24,X6941,X6946)
| ssPv14_7r1r1r1r1r1r1r1(X6939,X6942,X6943,X6940,X6937,X6936,X6938)
| ssPv16_5r1r1r1r1r1(X6939,X6942,X6943,X6940,X6937)
| ssPv19_2r1r1(X6939,X6945) ),
inference(resolution,[status(thm)],[c449,c106]) ).
cnf(c547,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X6961,X6960,X6950,X6958,X6956,X6949,X6959,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X6961,X6960,X6950,X6958,X6956,X6949,X6959)
| ~ ssNder1_6r1r1r1r1r1r1(X6961,X6960,X6950,X6958,X6956,X6949)
| ~ ssNder1_5r1r1r1r1r1(X6961,X6960,X6950,X6958,X6956)
| ~ ssNder1_4r1r1r1r1(X6961,X6960,X6950,X6958)
| ~ ssNder1_3r1r1r1(X6961,X6960,X6950)
| ~ ssNder1_2r1r1(X6961,X6960)
| ~ ssNder1_1r1(X6961)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X6961,X6960,X6950,X6958,X6956,X6949,X6959,skc24,X6953,X6952,X6954,X6951,X6957)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X6961,X6960,X6950,X6958,X6956,X6949,X6959,skc24,X6953,X6952)
| ssPv14_7r1r1r1r1r1r1r1(X6961,X6960,X6950,X6958,X6956,X6949,X6959)
| ssPv16_5r1r1r1r1r1(X6961,X6960,X6950,X6958,X6956)
| ssPv19_2r1r1(X6961,X6955) ),
inference(resolution,[status(thm)],[c504,c73]) ).
cnf(c548,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X6967,X6966,X6970,X6968,X6974,X6964,X6965)
| ~ ssNder1_6r1r1r1r1r1r1(X6967,X6966,X6970,X6968,X6974,X6964)
| ~ ssNder1_5r1r1r1r1r1(X6967,X6966,X6970,X6968,X6974)
| ~ ssNder1_4r1r1r1r1(X6967,X6966,X6970,X6968)
| ~ ssNder1_3r1r1r1(X6967,X6966,X6970)
| ~ ssNder1_2r1r1(X6967,X6966)
| ~ ssNder1_1r1(X6967)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X6967,X6966,X6970,X6968,X6974,X6964,X6965,skc24,X6972,X6971,X6963,X6962,X6969)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X6967,X6966,X6970,X6968,X6974,X6964,X6965,skc24,X6972,X6971)
| ssPv14_7r1r1r1r1r1r1r1(X6967,X6966,X6970,X6968,X6974,X6964,X6965)
| ssPv16_5r1r1r1r1r1(X6967,X6966,X6970,X6968,X6974)
| ssPv19_2r1r1(X6967,X6973) ),
inference(resolution,[status(thm)],[c547,c58]) ).
cnf(c549,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X6985,X6979,X6986,X6987,X6975,X6976)
| ~ ssNder1_5r1r1r1r1r1(X6985,X6979,X6986,X6987,X6975)
| ~ ssNder1_4r1r1r1r1(X6985,X6979,X6986,X6987)
| ~ ssNder1_3r1r1r1(X6985,X6979,X6986)
| ~ ssNder1_2r1r1(X6985,X6979)
| ~ ssNder1_1r1(X6985)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X6985,X6979,X6986,X6987,X6975,X6976,X6983,skc24,X6980,X6977,X6981,X6978,X6984)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X6985,X6979,X6986,X6987,X6975,X6976,X6983,skc24,X6980,X6977)
| ssPv14_7r1r1r1r1r1r1r1(X6985,X6979,X6986,X6987,X6975,X6976,X6983)
| ssPv16_5r1r1r1r1r1(X6985,X6979,X6986,X6987,X6975)
| ssPv19_2r1r1(X6985,X6982) ),
inference(resolution,[status(thm)],[c548,c43]) ).
cnf(c550,plain,
( ~ ssNder1_5r1r1r1r1r1(X7014,X7003,X7008,X7015,X7005)
| ~ ssNder1_4r1r1r1r1(X7014,X7003,X7008,X7015)
| ~ ssNder1_3r1r1r1(X7014,X7003,X7008)
| ~ ssNder1_2r1r1(X7014,X7003)
| ~ ssNder1_1r1(X7014)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7014,X7003,X7008,X7015,X7005,X7004,X7009,skc24,X7007,X7011,X7006,X7012,X7010)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7014,X7003,X7008,X7015,X7005,X7004,X7009,skc24,X7007,X7011)
| ssPv14_7r1r1r1r1r1r1r1(X7014,X7003,X7008,X7015,X7005,X7004,X7009)
| ssPv16_5r1r1r1r1r1(X7014,X7003,X7008,X7015,X7005)
| ssPv19_2r1r1(X7014,X7013) ),
inference(resolution,[status(thm)],[c549,c30]) ).
cnf(c552,plain,
( ~ ssNder1_4r1r1r1r1(X7026,X7017,X7019,X7027)
| ~ ssNder1_3r1r1r1(X7026,X7017,X7019)
| ~ ssNder1_2r1r1(X7026,X7017)
| ~ ssNder1_1r1(X7026)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7026,X7017,X7019,X7027,X7024,X7016,X7025,skc24,X7023,X7028,X7020,X7018,X7021)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7026,X7017,X7019,X7027,X7024,X7016,X7025,skc24,X7023,X7028)
| ssPv14_7r1r1r1r1r1r1r1(X7026,X7017,X7019,X7027,X7024,X7016,X7025)
| ssPv16_5r1r1r1r1r1(X7026,X7017,X7019,X7027,X7024)
| ssPv19_2r1r1(X7026,X7022) ),
inference(resolution,[status(thm)],[c550,c19]) ).
cnf(c553,plain,
( ~ ssNder1_3r1r1r1(X7032,X7033,X7038)
| ~ ssNder1_2r1r1(X7032,X7033)
| ~ ssNder1_1r1(X7032)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7032,X7033,X7038,X7039,X7030,X7037,X7041,skc24,X7031,X7034,X7036,X7029,X7035)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7032,X7033,X7038,X7039,X7030,X7037,X7041,skc24,X7031,X7034)
| ssPv14_7r1r1r1r1r1r1r1(X7032,X7033,X7038,X7039,X7030,X7037,X7041)
| ssPv16_5r1r1r1r1r1(X7032,X7033,X7038,X7039,X7030)
| ssPv19_2r1r1(X7032,X7040) ),
inference(resolution,[status(thm)],[c552,c10]) ).
cnf(c554,plain,
( ~ ssNder1_2r1r1(X7047,X7043)
| ~ ssNder1_1r1(X7047)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7047,X7043,X7046,X7052,X7049,X7042,X7048,skc24,X7044,X7051,X7053,X7054,X7050)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7047,X7043,X7046,X7052,X7049,X7042,X7048,skc24,X7044,X7051)
| ssPv14_7r1r1r1r1r1r1r1(X7047,X7043,X7046,X7052,X7049,X7042,X7048)
| ssPv16_5r1r1r1r1r1(X7047,X7043,X7046,X7052,X7049)
| ssPv19_2r1r1(X7047,X7045) ),
inference(resolution,[status(thm)],[c553,c5]) ).
cnf(c555,plain,
( ~ ssNder1_1r1(X7059)
| ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7059,X7062,X7055,X7060,X7066,X7058,X7065,skc24,X7067,X7056,X7061,X7057,X7064)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7059,X7062,X7055,X7060,X7066,X7058,X7065,skc24,X7067,X7056)
| ssPv14_7r1r1r1r1r1r1r1(X7059,X7062,X7055,X7060,X7066,X7058,X7065)
| ssPv16_5r1r1r1r1r1(X7059,X7062,X7055,X7060,X7066)
| ssPv19_2r1r1(X7059,X7063) ),
inference(resolution,[status(thm)],[c554,c2]) ).
cnf(c556,plain,
( ~ ssNder1_0
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7083,X7092,X7088,X7085,X7080,X7086,X7082,skc24,X7089,X7087,X7091,X7081,X7090)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7083,X7092,X7088,X7085,X7080,X7086,X7082,skc24,X7089,X7087)
| ssPv14_7r1r1r1r1r1r1r1(X7083,X7092,X7088,X7085,X7080,X7086,X7082)
| ssPv16_5r1r1r1r1r1(X7083,X7092,X7088,X7085,X7080)
| ssPv19_2r1r1(X7083,X7084) ),
inference(resolution,[status(thm)],[c555,c0]) ).
cnf(c558,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7102,X7097,X7100,X7101,X7093,X7094,X7099,skc24,X7104,X7095,X7098,X7105,X7103)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7102,X7097,X7100,X7101,X7093,X7094,X7099,skc24,X7104,X7095)
| ssPv14_7r1r1r1r1r1r1r1(X7102,X7097,X7100,X7101,X7093,X7094,X7099)
| ssPv16_5r1r1r1r1r1(X7102,X7097,X7100,X7101,X7093)
| ssPv19_2r1r1(X7102,X7096) ),
inference(resolution,[status(thm)],[c556,clause1]) ).
cnf(c564,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7220,X7217,X7216,X7218,skc31,X7226,X7224,skc24,X7223,X7225,X7227,X7222,X7219)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7220,X7217,X7216,X7218,skc31,X7226,X7224,skc24,X7223,X7225)
| ssPv14_7r1r1r1r1r1r1r1(X7220,X7217,X7216,X7218,skc31,X7226,X7224)
| ssPv19_2r1r1(X7220,X7221)
| ~ ssNder1_3r1r1r1(X7220,X7217,X7216)
| ~ ssNder1_2r1r1(X7220,X7217)
| ~ ssNder1_1r1(X7220)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c558,clause7]) ).
cnf(c579,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7247,X7241,X7245,X7250,skc31,X7244,X7240,skc24,X7249,X7251,X7242,X7246,X7248)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7247,X7241,X7245,X7250,skc31,X7244,X7240,skc24,X7249,X7251)
| ssPv14_7r1r1r1r1r1r1r1(X7247,X7241,X7245,X7250,skc31,X7244,X7240)
| ssPv19_2r1r1(X7247,X7243)
| ~ ssNder1_2r1r1(X7247,X7241)
| ~ ssNder1_1r1(X7247)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c564,c5]) ).
cnf(c581,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7257,X7260,X7255,X7254,skc31,X7263,X7256,skc24,X7258,X7252,X7253,X7262,X7261)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7257,X7260,X7255,X7254,skc31,X7263,X7256,skc24,X7258,X7252)
| ssPv14_7r1r1r1r1r1r1r1(X7257,X7260,X7255,X7254,skc31,X7263,X7256)
| ssPv19_2r1r1(X7257,X7259)
| ~ ssNder1_1r1(X7257)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c579,c2]) ).
cnf(c582,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7266,X7270,X7268,X7273,skc31,X7271,X7275,skc24,X7264,X7265,X7274,X7272,X7267)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7266,X7270,X7268,X7273,skc31,X7271,X7275,skc24,X7264,X7265)
| ssPv14_7r1r1r1r1r1r1r1(X7266,X7270,X7268,X7273,skc31,X7271,X7275)
| ssPv19_2r1r1(X7266,X7269)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c581,c0]) ).
cnf(c583,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7286,X7281,X7276,X7284,skc31,X7285,X7280,skc24,X7282,X7279,X7278,X7283,X7287)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7286,X7281,X7276,X7284,skc31,X7285,X7280,skc24,X7282,X7279)
| ssPv14_7r1r1r1r1r1r1r1(X7286,X7281,X7276,X7284,skc31,X7285,X7280)
| ssPv19_2r1r1(X7286,X7277) ),
inference(resolution,[status(thm)],[c582,clause1]) ).
cnf(c587,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7426,X7425,X7420,X7417,skc31,X7423,skc27,skc24,X7418,X7422,X7427,X7424,X7419)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7426,X7425,X7420,X7417,skc31,X7423,skc27,skc24,X7418,X7422)
| ssPv19_2r1r1(X7426,X7421)
| ~ ssNder1_5r1r1r1r1r1(X7426,X7425,X7420,X7417,skc31)
| ~ ssNder1_4r1r1r1r1(X7426,X7425,X7420,X7417)
| ~ ssNder1_3r1r1r1(X7426,X7425,X7420)
| ~ ssNder1_2r1r1(X7426,X7425)
| ~ ssNder1_1r1(X7426)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c583,clause13]) ).
cnf(c601,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7437,X7429,X7430,X7438,skc31,X7431,skc27,skc24,X7433,X7436,X7432,X7428,X7434)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7437,X7429,X7430,X7438,skc31,X7431,skc27,skc24,X7433,X7436)
| ssPv19_2r1r1(X7437,X7435)
| ~ ssNder1_4r1r1r1r1(X7437,X7429,X7430,X7438)
| ~ ssNder1_3r1r1r1(X7437,X7429,X7430)
| ~ ssNder1_2r1r1(X7437,X7429)
| ~ ssNder1_1r1(X7437)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c587,c19]) ).
cnf(c602,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7442,X7443,X7448,X7449,skc31,X7444,skc27,skc24,X7445,X7447,X7441,X7446,X7440)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7442,X7443,X7448,X7449,skc31,X7444,skc27,skc24,X7445,X7447)
| ssPv19_2r1r1(X7442,X7439)
| ~ ssNder1_3r1r1r1(X7442,X7443,X7448)
| ~ ssNder1_2r1r1(X7442,X7443)
| ~ ssNder1_1r1(X7442)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c601,c10]) ).
cnf(c603,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7472,X7466,X7471,X7473,skc31,X7475,skc27,skc24,X7467,X7465,X7470,X7468,X7474)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7472,X7466,X7471,X7473,skc31,X7475,skc27,skc24,X7467,X7465)
| ssPv19_2r1r1(X7472,X7469)
| ~ ssNder1_2r1r1(X7472,X7466)
| ~ ssNder1_1r1(X7472)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c602,c5]) ).
cnf(c605,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7480,X7481,X7486,X7477,skc31,X7484,skc27,skc24,X7482,X7478,X7479,X7483,X7476)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7480,X7481,X7486,X7477,skc31,X7484,skc27,skc24,X7482,X7478)
| ssPv19_2r1r1(X7480,X7485)
| ~ ssNder1_1r1(X7480)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c603,c2]) ).
cnf(c606,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7489,X7494,X7497,X7493,skc31,X7488,skc27,skc24,X7490,X7495,X7487,X7496,X7492)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7489,X7494,X7497,X7493,skc31,X7488,skc27,skc24,X7490,X7495)
| ssPv19_2r1r1(X7489,X7491)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c605,c0]) ).
cnf(c607,plain,
( ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X7508,X7507,X7499,X7503,skc31,X7504,skc27,skc24,X7501,X7498,X7506,X7502,X7505)
| ssPv11_10r1r1r1r1r1r1r1r1r1r1(X7508,X7507,X7499,X7503,skc31,X7504,skc27,skc24,X7501,X7498)
| ssPv19_2r1r1(X7508,X7500) ),
inference(resolution,[status(thm)],[c606,clause1]) ).
cnf(c608,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X10725,X10728,X10731,X10729,skc31,X10730,skc27,skc24,X10724,X10723)
| ssPv19_2r1r1(X10725,X10727)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X10725,X10728,X10731,X10729,skc31,X10730,skc27,skc24,X10724,X10723,X10726)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X10725,X10728,X10731,X10729,skc31,X10730,skc27,skc24,X10724,X10723)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X10725,X10728,X10731,X10729,skc31,X10730,skc27,skc24,X10724)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X10725,X10728,X10731,X10729,skc31,X10730,skc27,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X10725,X10728,X10731,X10729,skc31,X10730,skc27)
| ~ ssNder1_6r1r1r1r1r1r1(X10725,X10728,X10731,X10729,skc31,X10730)
| ~ ssNder1_5r1r1r1r1r1(X10725,X10728,X10731,X10729,skc31)
| ~ ssNder1_4r1r1r1r1(X10725,X10728,X10731,X10729)
| ~ ssNder1_3r1r1r1(X10725,X10728,X10731)
| ~ ssNder1_2r1r1(X10725,X10728)
| ~ ssNder1_1r1(X10725)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c607,clause29]) ).
cnf(c868,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X18995,X18998,X18997,X18996,skc31,X19000,skc27,skc24,X18999,X19001)
| ssPv19_2r1r1(X18995,X19002)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X18995,X18998,X18997,X18996,skc31,X19000,skc27,skc24,X18999,X19001)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X18995,X18998,X18997,X18996,skc31,X19000,skc27,skc24,X18999)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X18995,X18998,X18997,X18996,skc31,X19000,skc27,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X18995,X18998,X18997,X18996,skc31,X19000,skc27)
| ~ ssNder1_6r1r1r1r1r1r1(X18995,X18998,X18997,X18996,skc31,X19000)
| ~ ssNder1_5r1r1r1r1r1(X18995,X18998,X18997,X18996,skc31)
| ~ ssNder1_4r1r1r1r1(X18995,X18998,X18997,X18996)
| ~ ssNder1_3r1r1r1(X18995,X18998,X18997)
| ~ ssNder1_2r1r1(X18995,X18998)
| ~ ssNder1_1r1(X18995)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c608,c135]) ).
cnf(c1708,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24007,X24011,X24012,X24009,skc31,X24006,skc27,skc24,X24010,X24013)
| ssPv19_2r1r1(X24007,X24008)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X24007,X24011,X24012,X24009,skc31,X24006,skc27,skc24,X24010)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X24007,X24011,X24012,X24009,skc31,X24006,skc27,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X24007,X24011,X24012,X24009,skc31,X24006,skc27)
| ~ ssNder1_6r1r1r1r1r1r1(X24007,X24011,X24012,X24009,skc31,X24006)
| ~ ssNder1_5r1r1r1r1r1(X24007,X24011,X24012,X24009,skc31)
| ~ ssNder1_4r1r1r1r1(X24007,X24011,X24012,X24009)
| ~ ssNder1_3r1r1r1(X24007,X24011,X24012)
| ~ ssNder1_2r1r1(X24007,X24011)
| ~ ssNder1_1r1(X24007)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c868,c106]) ).
cnf(c1887,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24021,X24020,X24016,X24019,skc31,X24014,skc27,skc24,X24017,X24015)
| ssPv19_2r1r1(X24021,X24018)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X24021,X24020,X24016,X24019,skc31,X24014,skc27,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X24021,X24020,X24016,X24019,skc31,X24014,skc27)
| ~ ssNder1_6r1r1r1r1r1r1(X24021,X24020,X24016,X24019,skc31,X24014)
| ~ ssNder1_5r1r1r1r1r1(X24021,X24020,X24016,X24019,skc31)
| ~ ssNder1_4r1r1r1r1(X24021,X24020,X24016,X24019)
| ~ ssNder1_3r1r1r1(X24021,X24020,X24016)
| ~ ssNder1_2r1r1(X24021,X24020)
| ~ ssNder1_1r1(X24021)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1708,c73]) ).
cnf(c1888,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24024,X24023,X24029,X24025,skc31,X24022,skc27,skc24,X24027,X24026)
| ssPv19_2r1r1(X24024,X24028)
| ~ ssNder1_7r1r1r1r1r1r1r1(X24024,X24023,X24029,X24025,skc31,X24022,skc27)
| ~ ssNder1_6r1r1r1r1r1r1(X24024,X24023,X24029,X24025,skc31,X24022)
| ~ ssNder1_5r1r1r1r1r1(X24024,X24023,X24029,X24025,skc31)
| ~ ssNder1_4r1r1r1r1(X24024,X24023,X24029,X24025)
| ~ ssNder1_3r1r1r1(X24024,X24023,X24029)
| ~ ssNder1_2r1r1(X24024,X24023)
| ~ ssNder1_1r1(X24024)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1887,c58]) ).
cnf(c1889,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24034,X24031,X24036,X24037,skc31,X24030,skc27,skc24,X24032,X24035)
| ssPv19_2r1r1(X24034,X24033)
| ~ ssNder1_6r1r1r1r1r1r1(X24034,X24031,X24036,X24037,skc31,X24030)
| ~ ssNder1_5r1r1r1r1r1(X24034,X24031,X24036,X24037,skc31)
| ~ ssNder1_4r1r1r1r1(X24034,X24031,X24036,X24037)
| ~ ssNder1_3r1r1r1(X24034,X24031,X24036)
| ~ ssNder1_2r1r1(X24034,X24031)
| ~ ssNder1_1r1(X24034)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1888,c43]) ).
cnf(c1890,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24064,X24060,X24063,X24062,skc31,X24066,skc27,skc24,X24061,X24059)
| ssPv19_2r1r1(X24064,X24065)
| ~ ssNder1_5r1r1r1r1r1(X24064,X24060,X24063,X24062,skc31)
| ~ ssNder1_4r1r1r1r1(X24064,X24060,X24063,X24062)
| ~ ssNder1_3r1r1r1(X24064,X24060,X24063)
| ~ ssNder1_2r1r1(X24064,X24060)
| ~ ssNder1_1r1(X24064)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1889,c30]) ).
cnf(c1891,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24073,X24068,X24070,X24074,skc31,X24072,skc27,skc24,X24069,X24067)
| ssPv19_2r1r1(X24073,X24071)
| ~ ssNder1_4r1r1r1r1(X24073,X24068,X24070,X24074)
| ~ ssNder1_3r1r1r1(X24073,X24068,X24070)
| ~ ssNder1_2r1r1(X24073,X24068)
| ~ ssNder1_1r1(X24073)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1890,c19]) ).
cnf(c1892,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24076,X24077,X24081,X24082,skc31,X24075,skc27,skc24,X24079,X24080)
| ssPv19_2r1r1(X24076,X24078)
| ~ ssNder1_3r1r1r1(X24076,X24077,X24081)
| ~ ssNder1_2r1r1(X24076,X24077)
| ~ ssNder1_1r1(X24076)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1891,c10]) ).
cnf(c1893,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24086,X24083,X24084,X24088,skc31,X24090,skc27,skc24,X24085,X24087)
| ssPv19_2r1r1(X24086,X24089)
| ~ ssNder1_2r1r1(X24086,X24083)
| ~ ssNder1_1r1(X24086)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1892,c5]) ).
cnf(c1894,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24093,X24095,X24096,X24094,skc31,X24098,skc27,skc24,X24097,X24092)
| ssPv19_2r1r1(X24093,X24091)
| ~ ssNder1_1r1(X24093)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1893,c2]) ).
cnf(c1895,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24122,X24124,X24127,X24126,skc31,X24120,skc27,skc24,X24123,X24121)
| ssPv19_2r1r1(X24122,X24125)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1894,c0]) ).
cnf(c1896,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24129,X24134,X24131,X24128,skc31,X24132,skc27,skc24,X24130,X24135)
| ssPv19_2r1r1(X24129,X24133) ),
inference(resolution,[status(thm)],[c1895,clause1]) ).
cnf(c1901,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24140,X24138,X24142,X24139,skc31,X24141,skc27,skc24,X24137,X24136)
| ~ ssPv20_1r1(X24140)
| ~ ssNder1_1r1(X24140)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1896,c282]) ).
cnf(c1904,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24143,X24146,X24148,X24145,skc31,X24149,skc27,skc24,X24147,X24144)
| ~ ssPv20_1r1(X24143)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1901,c0]) ).
cnf(c1905,plain,
( ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24155,X24154,X24151,X24153,skc31,X24150,skc27,skc24,X24152,X24156)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1904,c1621]) ).
cnf(c1906,plain,
ssPv11_10r1r1r1r1r1r1r1r1r1r1(X24186,X24182,X24185,X24181,skc31,X24184,skc27,skc24,X24180,X24183),
inference(resolution,[status(thm)],[c1905,clause1]) ).
cnf(c1907,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X25155,X25153,X25150,X25154,skc31,X25151,skc27,skc24,X25152)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X25155,X25153,X25150,X25154,skc31,X25151,skc27,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X25155,X25153,X25150,X25154,skc31,X25151,skc27)
| ~ ssNder1_6r1r1r1r1r1r1(X25155,X25153,X25150,X25154,skc31,X25151)
| ~ ssNder1_5r1r1r1r1r1(X25155,X25153,X25150,X25154,skc31)
| ~ ssNder1_4r1r1r1r1(X25155,X25153,X25150,X25154)
| ~ ssNder1_3r1r1r1(X25155,X25153,X25150)
| ~ ssNder1_2r1r1(X25155,X25153)
| ~ ssPv20_1r1(X25155)
| ~ ssNder1_1r1(X25155)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25155,X25153,X25150,X25154,skc31,X25151,skc27)
| ssPv15_6r1r1r1r1r1r1(X25155,X25153,X25150,X25154,skc31,X25151) ),
inference(resolution,[status(thm)],[c1906,clause25]) ).
cnf(c1949,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X25160,X25159,X25157,X25158,skc31,X25156,skc27,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X25160,X25159,X25157,X25158,skc31,X25156,skc27)
| ~ ssNder1_6r1r1r1r1r1r1(X25160,X25159,X25157,X25158,skc31,X25156)
| ~ ssNder1_5r1r1r1r1r1(X25160,X25159,X25157,X25158,skc31)
| ~ ssNder1_4r1r1r1r1(X25160,X25159,X25157,X25158)
| ~ ssNder1_3r1r1r1(X25160,X25159,X25157)
| ~ ssNder1_2r1r1(X25160,X25159)
| ~ ssPv20_1r1(X25160)
| ~ ssNder1_1r1(X25160)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25160,X25159,X25157,X25158,skc31,X25156,skc27)
| ssPv15_6r1r1r1r1r1r1(X25160,X25159,X25157,X25158,skc31,X25156) ),
inference(resolution,[status(thm)],[c1907,c73]) ).
cnf(c1950,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X25178,X25177,X25180,X25179,skc31,X25176,skc27)
| ~ ssNder1_6r1r1r1r1r1r1(X25178,X25177,X25180,X25179,skc31,X25176)
| ~ ssNder1_5r1r1r1r1r1(X25178,X25177,X25180,X25179,skc31)
| ~ ssNder1_4r1r1r1r1(X25178,X25177,X25180,X25179)
| ~ ssNder1_3r1r1r1(X25178,X25177,X25180)
| ~ ssNder1_2r1r1(X25178,X25177)
| ~ ssPv20_1r1(X25178)
| ~ ssNder1_1r1(X25178)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25178,X25177,X25180,X25179,skc31,X25176,skc27)
| ssPv15_6r1r1r1r1r1r1(X25178,X25177,X25180,X25179,skc31,X25176) ),
inference(resolution,[status(thm)],[c1949,c58]) ).
cnf(c1952,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X25183,X25182,X25184,X25185,skc31,X25181)
| ~ ssNder1_5r1r1r1r1r1(X25183,X25182,X25184,X25185,skc31)
| ~ ssNder1_4r1r1r1r1(X25183,X25182,X25184,X25185)
| ~ ssNder1_3r1r1r1(X25183,X25182,X25184)
| ~ ssNder1_2r1r1(X25183,X25182)
| ~ ssPv20_1r1(X25183)
| ~ ssNder1_1r1(X25183)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25183,X25182,X25184,X25185,skc31,X25181,skc27)
| ssPv15_6r1r1r1r1r1r1(X25183,X25182,X25184,X25185,skc31,X25181) ),
inference(resolution,[status(thm)],[c1950,c43]) ).
cnf(c1953,plain,
( ~ ssNder1_5r1r1r1r1r1(X25189,X25186,X25188,X25187,skc31)
| ~ ssNder1_4r1r1r1r1(X25189,X25186,X25188,X25187)
| ~ ssNder1_3r1r1r1(X25189,X25186,X25188)
| ~ ssNder1_2r1r1(X25189,X25186)
| ~ ssPv20_1r1(X25189)
| ~ ssNder1_1r1(X25189)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25189,X25186,X25188,X25187,skc31,X25190,skc27)
| ssPv15_6r1r1r1r1r1r1(X25189,X25186,X25188,X25187,skc31,X25190) ),
inference(resolution,[status(thm)],[c1952,c30]) ).
cnf(c1954,plain,
( ~ ssNder1_4r1r1r1r1(X25194,X25191,X25192,X25195)
| ~ ssNder1_3r1r1r1(X25194,X25191,X25192)
| ~ ssNder1_2r1r1(X25194,X25191)
| ~ ssPv20_1r1(X25194)
| ~ ssNder1_1r1(X25194)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25194,X25191,X25192,X25195,skc31,X25193,skc27)
| ssPv15_6r1r1r1r1r1r1(X25194,X25191,X25192,X25195,skc31,X25193) ),
inference(resolution,[status(thm)],[c1953,c19]) ).
cnf(c1955,plain,
( ~ ssNder1_3r1r1r1(X25196,X25197,X25199)
| ~ ssNder1_2r1r1(X25196,X25197)
| ~ ssPv20_1r1(X25196)
| ~ ssNder1_1r1(X25196)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25196,X25197,X25199,X25200,skc31,X25198,skc27)
| ssPv15_6r1r1r1r1r1r1(X25196,X25197,X25199,X25200,skc31,X25198) ),
inference(resolution,[status(thm)],[c1954,c10]) ).
cnf(c1956,plain,
( ~ ssNder1_2r1r1(X25223,X25221)
| ~ ssPv20_1r1(X25223)
| ~ ssNder1_1r1(X25223)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25223,X25221,X25222,X25225,skc31,X25224,skc27)
| ssPv15_6r1r1r1r1r1r1(X25223,X25221,X25222,X25225,skc31,X25224) ),
inference(resolution,[status(thm)],[c1955,c5]) ).
cnf(c1957,plain,
( ~ ssPv20_1r1(X25228)
| ~ ssNder1_1r1(X25228)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25228,X25229,X25226,X25230,skc31,X25227,skc27)
| ssPv15_6r1r1r1r1r1r1(X25228,X25229,X25226,X25230,skc31,X25227) ),
inference(resolution,[status(thm)],[c1956,c2]) ).
cnf(c1958,plain,
( ~ ssPv20_1r1(X25231)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25231,X25235,X25234,X25233,skc31,X25232,skc27)
| ssPv15_6r1r1r1r1r1r1(X25231,X25235,X25234,X25233,skc31,X25232) ),
inference(resolution,[status(thm)],[c1957,c0]) ).
cnf(c1959,plain,
( ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X25238,X25239,X25240,X25236,skc31,X25237,skc27)
| ssPv15_6r1r1r1r1r1r1(X25238,X25239,X25240,X25236,skc31,X25237) ),
inference(resolution,[status(thm)],[c1958,c1621]) ).
cnf(c1960,plain,
( ssPv14_7r1r1r1r1r1r1r1(X25243,X25245,X25241,X25242,skc31,X25244,skc27)
| ssPv15_6r1r1r1r1r1r1(X25243,X25245,X25241,X25242,skc31,X25244) ),
inference(resolution,[status(thm)],[c1959,clause1]) ).
cnf(c1962,plain,
( ssPv14_7r1r1r1r1r1r1r1(X25263,X25264,X25262,X25265,skc31,skc29,skc27)
| ~ ssNder1_4r1r1r1r1(X25263,X25264,X25262,X25265)
| ~ ssNder1_3r1r1r1(X25263,X25264,X25262)
| ~ ssNder1_2r1r1(X25263,X25264)
| ~ ssNder1_1r1(X25263)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1960,clause10]) ).
cnf(c1963,plain,
( ssPv14_7r1r1r1r1r1r1r1(X25269,X25268,X25266,X25267,skc31,skc29,skc27)
| ~ ssNder1_3r1r1r1(X25269,X25268,X25266)
| ~ ssNder1_2r1r1(X25269,X25268)
| ~ ssNder1_1r1(X25269)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1962,c10]) ).
cnf(c1964,plain,
( ssPv14_7r1r1r1r1r1r1r1(X25273,X25270,X25272,X25271,skc31,skc29,skc27)
| ~ ssNder1_2r1r1(X25273,X25270)
| ~ ssNder1_1r1(X25273)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1963,c5]) ).
cnf(c1965,plain,
( ssPv14_7r1r1r1r1r1r1r1(X25275,X25277,X25276,X25274,skc31,skc29,skc27)
| ~ ssNder1_1r1(X25275)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1964,c2]) ).
cnf(c1966,plain,
( ssPv14_7r1r1r1r1r1r1r1(X25280,X25278,X25281,X25279,skc31,skc29,skc27)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1965,c0]) ).
cnf(c1967,plain,
ssPv14_7r1r1r1r1r1r1r1(X25298,X25301,X25299,X25300,skc31,skc29,skc27),
inference(resolution,[status(thm)],[c1966,clause1]) ).
cnf(c1968,plain,
( ~ ssNder1_5r1r1r1r1r1(X25303,X25302,X25304,X25305,skc31)
| ~ ssNder1_4r1r1r1r1(X25303,X25302,X25304,X25305)
| ~ ssNder1_3r1r1r1(X25303,X25302,X25304)
| ~ ssNder1_2r1r1(X25303,X25302)
| ~ ssNder1_1r1(X25303)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1967,clause13]) ).
cnf(c1969,plain,
( ~ ssNder1_4r1r1r1r1(X25307,X25309,X25306,X25308)
| ~ ssNder1_3r1r1r1(X25307,X25309,X25306)
| ~ ssNder1_2r1r1(X25307,X25309)
| ~ ssNder1_1r1(X25307)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1968,c19]) ).
cnf(c1970,plain,
( ~ ssNder1_3r1r1r1(X25312,X25311,X25310)
| ~ ssNder1_2r1r1(X25312,X25311)
| ~ ssNder1_1r1(X25312)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1969,c10]) ).
cnf(c1971,plain,
( ~ ssNder1_2r1r1(X25314,X25313)
| ~ ssNder1_1r1(X25314)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1970,c5]) ).
cnf(c1972,plain,
( ~ ssNder1_1r1(X25332)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1971,c2]) ).
cnf(c1973,plain,
~ ssNder1_0,
inference(resolution,[status(thm)],[c1972,c0]) ).
cnf(c1974,plain,
$false,
inference(resolution,[status(thm)],[c1973,clause1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYN890-1 : TPTP v8.1.2. Released v2.5.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n004.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:07:38 EDT 2024
% 0.13/0.36 % CPUTime :
% 5.12/5.34 % Version: 1.5
% 5.12/5.34 % SZS status Unsatisfiable
% 5.12/5.34 % SZS output start CNFRefutation
% See solution above
% 5.12/5.35
% 5.12/5.35 % Initial clauses : 86
% 5.12/5.35 % Processed clauses : 1199
% 5.12/5.35 % Factors computed : 14
% 5.12/5.35 % Resolvents computed: 1961
% 5.12/5.35 % Tautologies deleted: 19
% 5.12/5.35 % Forward subsumed : 554
% 5.12/5.35 % Backward subsumed : 1153
% 5.12/5.35 % -------- CPU Time ---------
% 5.12/5.35 % User time : 4.951 s
% 5.12/5.35 % System time : 0.028 s
% 5.12/5.35 % Total time : 4.979 s
%------------------------------------------------------------------------------