%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN869-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:09 EDT 2024
% Result : Unsatisfiable 5.37s 5.57s
% Output : Refutation 5.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 202
% Number of leaves : 26
% Syntax : Number of clauses : 312 ( 22 unt; 126 nHn; 49 RR)
% Number of literals : 2331 ( 0 equ;1818 neg)
% Maximal clause size : 19 ( 7 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 2 prp; 0-15 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 3262 (1587 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssNder1_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(clause2,negated_conjecture,
( ~ ssNder1_0
| ssNder1_1r1(X2) ),
file('/export/starexec/sandbox2/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/sandbox2/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(X9,X10)
| ~ ssNder1_1r1(X9)
| ~ ssNder1_0
| ssNder1_3r1r1r1(X9,X10,X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(c3,plain,
( ~ ssNder1_1r1(X13)
| ~ ssNder1_0
| ssNder1_3r1r1r1(X13,X15,X14) ),
inference(resolution,[status(thm)],[c2,clause4]) ).
cnf(c4,plain,
( ~ ssNder1_0
| ssNder1_3r1r1r1(X17,X18,X16) ),
inference(resolution,[status(thm)],[c3,c0]) ).
cnf(c5,plain,
ssNder1_3r1r1r1(X21,X19,X20),
inference(resolution,[status(thm)],[c4,clause1]) ).
cnf(clause5,negated_conjecture,
( ~ ssNder1_3r1r1r1(X24,X25,X22)
| ~ ssNder1_2r1r1(X24,X25)
| ~ ssNder1_1r1(X24)
| ~ ssNder1_0
| ssNder1_4r1r1r1r1(X24,X25,X22,X23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c6,plain,
( ~ ssNder1_2r1r1(X31,X32)
| ~ ssNder1_1r1(X31)
| ~ ssNder1_0
| ssNder1_4r1r1r1r1(X31,X32,X30,X33) ),
inference(resolution,[status(thm)],[clause5,c5]) ).
cnf(c8,plain,
( ~ ssNder1_1r1(X35)
| ~ ssNder1_0
| ssNder1_4r1r1r1r1(X35,X34,X36,X37) ),
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(X45,X44,X42,X43),
inference(resolution,[status(thm)],[c9,clause1]) ).
cnf(clause8,negated_conjecture,
( ~ ssNder1_4r1r1r1r1(X66,X68,X67,X69)
| ~ ssNder1_3r1r1r1(X66,X68,X67)
| ~ ssNder1_2r1r1(X66,X68)
| ~ ssNder1_1r1(X66)
| ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X66,X68,X67,X69,X70) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(c14,plain,
( ~ ssNder1_3r1r1r1(X73,X72,X74)
| ~ ssNder1_2r1r1(X73,X72)
| ~ ssNder1_1r1(X73)
| ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X73,X72,X74,X71,X75) ),
inference(resolution,[status(thm)],[clause8,c10]) ).
cnf(c15,plain,
( ~ ssNder1_2r1r1(X83,X85)
| ~ ssNder1_1r1(X83)
| ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X83,X85,X81,X84,X82) ),
inference(resolution,[status(thm)],[c14,c5]) ).
cnf(c17,plain,
( ~ ssNder1_1r1(X88)
| ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X88,X89,X90,X87,X86) ),
inference(resolution,[status(thm)],[c15,c2]) ).
cnf(c18,plain,
( ~ ssNder1_0
| ssNder1_5r1r1r1r1r1(X93,X94,X95,X92,X91) ),
inference(resolution,[status(thm)],[c17,c0]) ).
cnf(c19,plain,
ssNder1_5r1r1r1r1r1(X99,X98,X96,X100,X97),
inference(resolution,[status(thm)],[c18,clause1]) ).
cnf(clause11,negated_conjecture,
( ~ ssNder1_5r1r1r1r1r1(X131,X133,X132,X135,X136)
| ~ ssNder1_4r1r1r1r1(X131,X133,X132,X135)
| ~ ssNder1_3r1r1r1(X131,X133,X132)
| ~ ssNder1_2r1r1(X131,X133)
| ~ ssNder1_1r1(X131)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X131,X133,X132,X135,X136,X134) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(c24,plain,
( ~ ssNder1_4r1r1r1r1(X146,X144,X143,X147)
| ~ ssNder1_3r1r1r1(X146,X144,X143)
| ~ ssNder1_2r1r1(X146,X144)
| ~ ssNder1_1r1(X146)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X146,X144,X143,X147,X148,X145) ),
inference(resolution,[status(thm)],[clause11,c19]) ).
cnf(c26,plain,
( ~ ssNder1_3r1r1r1(X152,X151,X153)
| ~ ssNder1_2r1r1(X152,X151)
| ~ ssNder1_1r1(X152)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X152,X151,X153,X150,X149,X154) ),
inference(resolution,[status(thm)],[c24,c10]) ).
cnf(c27,plain,
( ~ ssNder1_2r1r1(X158,X160)
| ~ ssNder1_1r1(X158)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X158,X160,X155,X156,X159,X157) ),
inference(resolution,[status(thm)],[c26,c5]) ).
cnf(c28,plain,
( ~ ssNder1_1r1(X163)
| ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X163,X164,X162,X166,X165,X161) ),
inference(resolution,[status(thm)],[c27,c2]) ).
cnf(c29,plain,
( ~ ssNder1_0
| ssNder1_6r1r1r1r1r1r1(X167,X168,X169,X171,X170,X172) ),
inference(resolution,[status(thm)],[c28,c0]) ).
cnf(c30,plain,
ssNder1_6r1r1r1r1r1r1(X179,X183,X181,X184,X180,X182),
inference(resolution,[status(thm)],[c29,clause1]) ).
cnf(clause14,negated_conjecture,
( ~ ssNder1_6r1r1r1r1r1r1(X210,X212,X211,X214,X215,X213)
| ~ ssNder1_5r1r1r1r1r1(X210,X212,X211,X214,X215)
| ~ ssNder1_4r1r1r1r1(X210,X212,X211,X214)
| ~ ssNder1_3r1r1r1(X210,X212,X211)
| ~ ssNder1_2r1r1(X210,X212)
| ~ ssNder1_1r1(X210)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X210,X212,X211,X214,X215,X213,X209) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(c35,plain,
( ~ ssNder1_5r1r1r1r1r1(X231,X234,X229,X232,X233)
| ~ ssNder1_4r1r1r1r1(X231,X234,X229,X232)
| ~ ssNder1_3r1r1r1(X231,X234,X229)
| ~ ssNder1_2r1r1(X231,X234)
| ~ ssNder1_1r1(X231)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X231,X234,X229,X232,X233,X228,X230) ),
inference(resolution,[status(thm)],[clause14,c30]) ).
cnf(c37,plain,
( ~ ssNder1_4r1r1r1r1(X238,X236,X235,X240)
| ~ ssNder1_3r1r1r1(X238,X236,X235)
| ~ ssNder1_2r1r1(X238,X236)
| ~ ssNder1_1r1(X238)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X238,X236,X235,X240,X241,X237,X239) ),
inference(resolution,[status(thm)],[c35,c19]) ).
cnf(c38,plain,
( ~ ssNder1_3r1r1r1(X245,X244,X247)
| ~ ssNder1_2r1r1(X245,X244)
| ~ ssNder1_1r1(X245)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X245,X244,X247,X242,X246,X243,X248) ),
inference(resolution,[status(thm)],[c37,c10]) ).
cnf(c39,plain,
( ~ ssNder1_2r1r1(X259,X260)
| ~ ssNder1_1r1(X259)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X259,X260,X256,X262,X257,X261,X258) ),
inference(resolution,[status(thm)],[c38,c5]) ).
cnf(c41,plain,
( ~ ssNder1_1r1(X263)
| ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X263,X267,X264,X269,X268,X265,X266) ),
inference(resolution,[status(thm)],[c39,c2]) ).
cnf(c42,plain,
( ~ ssNder1_0
| ssNder1_7r1r1r1r1r1r1r1(X275,X270,X272,X271,X273,X274,X276) ),
inference(resolution,[status(thm)],[c41,c0]) ).
cnf(c43,plain,
ssNder1_7r1r1r1r1r1r1r1(X277,X281,X280,X282,X283,X279,X278),
inference(resolution,[status(thm)],[c42,clause1]) ).
cnf(clause17,negated_conjecture,
( ~ ssNder1_7r1r1r1r1r1r1r1(X335,X337,X336,X339,X340,X338,X333)
| ~ ssNder1_6r1r1r1r1r1r1(X335,X337,X336,X339,X340,X338)
| ~ ssNder1_5r1r1r1r1r1(X335,X337,X336,X339,X340)
| ~ ssNder1_4r1r1r1r1(X335,X337,X336,X339)
| ~ ssNder1_3r1r1r1(X335,X337,X336)
| ~ ssNder1_2r1r1(X335,X337)
| ~ ssNder1_1r1(X335)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X335,X337,X336,X339,X340,X338,X333,X334) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(c50,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X352,X353,X355,X354,X348,X349)
| ~ ssNder1_5r1r1r1r1r1(X352,X353,X355,X354,X348)
| ~ ssNder1_4r1r1r1r1(X352,X353,X355,X354)
| ~ ssNder1_3r1r1r1(X352,X353,X355)
| ~ ssNder1_2r1r1(X352,X353)
| ~ ssNder1_1r1(X352)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X352,X353,X355,X354,X348,X349,X350,X351) ),
inference(resolution,[status(thm)],[clause17,c43]) ).
cnf(c51,plain,
( ~ ssNder1_5r1r1r1r1r1(X358,X363,X357,X359,X361)
| ~ ssNder1_4r1r1r1r1(X358,X363,X357,X359)
| ~ ssNder1_3r1r1r1(X358,X363,X357)
| ~ ssNder1_2r1r1(X358,X363)
| ~ ssNder1_1r1(X358)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X358,X363,X357,X359,X361,X356,X362,X360) ),
inference(resolution,[status(thm)],[c50,c30]) ).
cnf(c52,plain,
( ~ ssNder1_4r1r1r1r1(X369,X367,X366,X370)
| ~ ssNder1_3r1r1r1(X369,X367,X366)
| ~ ssNder1_2r1r1(X369,X367)
| ~ ssNder1_1r1(X369)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X369,X367,X366,X370,X371,X365,X368,X364) ),
inference(resolution,[status(thm)],[c51,c19]) ).
cnf(c53,plain,
( ~ ssNder1_3r1r1r1(X375,X374,X376)
| ~ ssNder1_2r1r1(X375,X374)
| ~ ssNder1_1r1(X375)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X375,X374,X376,X373,X378,X379,X377,X372) ),
inference(resolution,[status(thm)],[c52,c10]) ).
cnf(c54,plain,
( ~ ssNder1_2r1r1(X391,X395)
| ~ ssNder1_1r1(X391)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X391,X395,X389,X393,X390,X392,X394,X396) ),
inference(resolution,[status(thm)],[c53,c5]) ).
cnf(c55,plain,
( ~ ssNder1_1r1(X400)
| ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X400,X401,X398,X404,X399,X402,X403,X397) ),
inference(resolution,[status(thm)],[c54,c2]) ).
cnf(c56,plain,
( ~ ssNder1_0
| ssNder1_8r1r1r1r1r1r1r1r1(X406,X405,X412,X411,X410,X407,X409,X408) ),
inference(resolution,[status(thm)],[c55,c0]) ).
cnf(c57,plain,
ssNder1_8r1r1r1r1r1r1r1r1(X419,X417,X420,X414,X418,X416,X415,X413),
inference(resolution,[status(thm)],[c56,clause1]) ).
cnf(clause18,negated_conjecture,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X383,X385,X384,X387,X388,X386,X380,X382)
| ~ ssNder1_7r1r1r1r1r1r1r1(X383,X385,X384,X387,X388,X386,X380)
| ~ ssNder1_6r1r1r1r1r1r1(X383,X385,X384,X387,X388,X386)
| ~ ssNder1_5r1r1r1r1r1(X383,X385,X384,X387,X388)
| ~ ssNder1_4r1r1r1r1(X383,X385,X384,X387)
| ~ ssNder1_3r1r1r1(X383,X385,X384)
| ~ ssNder1_2r1r1(X383,X385)
| ~ ssNder1_1r1(X383)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X383,X385,X384,X387,X388,X386,X380,X382,X381) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(c58,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X423,X424,X429,X422,X428,X425,X427)
| ~ ssNder1_6r1r1r1r1r1r1(X423,X424,X429,X422,X428,X425)
| ~ ssNder1_5r1r1r1r1r1(X423,X424,X429,X422,X428)
| ~ ssNder1_4r1r1r1r1(X423,X424,X429,X422)
| ~ ssNder1_3r1r1r1(X423,X424,X429)
| ~ ssNder1_2r1r1(X423,X424)
| ~ ssNder1_1r1(X423)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X423,X424,X429,X422,X428,X425,X427,X426,X421) ),
inference(resolution,[status(thm)],[c57,clause18]) ).
cnf(c59,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X444,X445,X448,X446,X441,X442)
| ~ ssNder1_5r1r1r1r1r1(X444,X445,X448,X446,X441)
| ~ ssNder1_4r1r1r1r1(X444,X445,X448,X446)
| ~ ssNder1_3r1r1r1(X444,X445,X448)
| ~ ssNder1_2r1r1(X444,X445)
| ~ ssNder1_1r1(X444)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X444,X445,X448,X446,X441,X442,X443,X447,X440) ),
inference(resolution,[status(thm)],[c58,c43]) ).
cnf(c60,plain,
( ~ ssNder1_5r1r1r1r1r1(X453,X457,X451,X454,X455)
| ~ ssNder1_4r1r1r1r1(X453,X457,X451,X454)
| ~ ssNder1_3r1r1r1(X453,X457,X451)
| ~ ssNder1_2r1r1(X453,X457)
| ~ ssNder1_1r1(X453)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X453,X457,X451,X454,X455,X450,X449,X456,X452) ),
inference(resolution,[status(thm)],[c59,c30]) ).
cnf(c61,plain,
( ~ ssNder1_4r1r1r1r1(X462,X460,X459,X464)
| ~ ssNder1_3r1r1r1(X462,X460,X459)
| ~ ssNder1_2r1r1(X462,X460)
| ~ ssNder1_1r1(X462)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X462,X460,X459,X464,X466,X458,X461,X465,X463) ),
inference(resolution,[status(thm)],[c60,c19]) ).
cnf(c62,plain,
( ~ ssNder1_3r1r1r1(X473,X469,X474)
| ~ ssNder1_2r1r1(X473,X469)
| ~ ssNder1_1r1(X473)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X473,X469,X474,X468,X470,X471,X467,X472,X475) ),
inference(resolution,[status(thm)],[c61,c10]) ).
cnf(c63,plain,
( ~ ssNder1_2r1r1(X481,X484)
| ~ ssNder1_1r1(X481)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X481,X484,X476,X483,X479,X478,X477,X482,X480) ),
inference(resolution,[status(thm)],[c62,c5]) ).
cnf(c64,plain,
( ~ ssNder1_1r1(X500)
| ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X500,X501,X503,X504,X502,X498,X497,X496,X499) ),
inference(resolution,[status(thm)],[c63,c2]) ).
cnf(c65,plain,
( ~ ssNder1_0
| ssNder1_9r1r1r1r1r1r1r1r1r1(X507,X505,X512,X513,X506,X511,X509,X510,X508) ),
inference(resolution,[status(thm)],[c64,c0]) ).
cnf(c66,plain,
ssNder1_9r1r1r1r1r1r1r1r1r1(X520,X518,X522,X521,X516,X517,X514,X515,X519),
inference(resolution,[status(thm)],[c65,clause1]) ).
cnf(clause19,negated_conjecture,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X434,X436,X435,X438,X439,X437,X431,X433,X432)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X434,X436,X435,X438,X439,X437,X431,X433)
| ~ ssNder1_7r1r1r1r1r1r1r1(X434,X436,X435,X438,X439,X437,X431)
| ~ ssNder1_6r1r1r1r1r1r1(X434,X436,X435,X438,X439,X437)
| ~ ssNder1_5r1r1r1r1r1(X434,X436,X435,X438,X439)
| ~ ssNder1_4r1r1r1r1(X434,X436,X435,X438)
| ~ ssNder1_3r1r1r1(X434,X436,X435)
| ~ ssNder1_2r1r1(X434,X436)
| ~ ssNder1_1r1(X434)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X434,X436,X435,X438,X439,X437,X431,X433,X432,X430) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(c67,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X531,X523,X526,X525,X530,X527,X524,X529)
| ~ ssNder1_7r1r1r1r1r1r1r1(X531,X523,X526,X525,X530,X527,X524)
| ~ ssNder1_6r1r1r1r1r1r1(X531,X523,X526,X525,X530,X527)
| ~ ssNder1_5r1r1r1r1r1(X531,X523,X526,X525,X530)
| ~ ssNder1_4r1r1r1r1(X531,X523,X526,X525)
| ~ ssNder1_3r1r1r1(X531,X523,X526)
| ~ ssNder1_2r1r1(X531,X523)
| ~ ssNder1_1r1(X531)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X531,X523,X526,X525,X530,X527,X524,X529,X532,X528) ),
inference(resolution,[status(thm)],[c66,clause19]) ).
cnf(c68,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X540,X535,X538,X541,X533,X542,X537)
| ~ ssNder1_6r1r1r1r1r1r1(X540,X535,X538,X541,X533,X542)
| ~ ssNder1_5r1r1r1r1r1(X540,X535,X538,X541,X533)
| ~ ssNder1_4r1r1r1r1(X540,X535,X538,X541)
| ~ ssNder1_3r1r1r1(X540,X535,X538)
| ~ ssNder1_2r1r1(X540,X535)
| ~ ssNder1_1r1(X540)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X540,X535,X538,X541,X533,X542,X537,X536,X534,X539) ),
inference(resolution,[status(thm)],[c67,c57]) ).
cnf(c69,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X560,X561,X564,X563,X555,X556)
| ~ ssNder1_5r1r1r1r1r1(X560,X561,X564,X563,X555)
| ~ ssNder1_4r1r1r1r1(X560,X561,X564,X563)
| ~ ssNder1_3r1r1r1(X560,X561,X564)
| ~ ssNder1_2r1r1(X560,X561)
| ~ ssNder1_1r1(X560)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X560,X561,X564,X563,X555,X556,X557,X558,X562,X559) ),
inference(resolution,[status(thm)],[c68,c43]) ).
cnf(c70,plain,
( ~ ssNder1_5r1r1r1r1r1(X571,X574,X567,X572,X573)
| ~ ssNder1_4r1r1r1r1(X571,X574,X567,X572)
| ~ ssNder1_3r1r1r1(X571,X574,X567)
| ~ ssNder1_2r1r1(X571,X574)
| ~ ssNder1_1r1(X571)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X571,X574,X567,X572,X573,X566,X570,X569,X568,X565) ),
inference(resolution,[status(thm)],[c69,c30]) ).
cnf(c71,plain,
( ~ ssNder1_4r1r1r1r1(X581,X579,X577,X582)
| ~ ssNder1_3r1r1r1(X581,X579,X577)
| ~ ssNder1_2r1r1(X581,X579)
| ~ ssNder1_1r1(X581)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X581,X579,X577,X582,X584,X583,X576,X580,X578,X575) ),
inference(resolution,[status(thm)],[c70,c19]) ).
cnf(c72,plain,
( ~ ssNder1_3r1r1r1(X592,X591,X593)
| ~ ssNder1_2r1r1(X592,X591)
| ~ ssNder1_1r1(X592)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X592,X591,X593,X589,X588,X585,X586,X590,X587,X594) ),
inference(resolution,[status(thm)],[c71,c10]) ).
cnf(c73,plain,
( ~ ssNder1_2r1r1(X600,X602)
| ~ ssNder1_1r1(X600)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X600,X602,X595,X596,X601,X598,X604,X597,X599,X603) ),
inference(resolution,[status(thm)],[c72,c5]) ).
cnf(c74,plain,
( ~ ssNder1_1r1(X619)
| ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X619,X622,X624,X617,X621,X623,X618,X625,X626,X620) ),
inference(resolution,[status(thm)],[c73,c2]) ).
cnf(c75,plain,
( ~ ssNder1_0
| ssNder1_10r1r1r1r1r1r1r1r1r1r1(X627,X634,X632,X636,X631,X633,X628,X630,X635,X629) ),
inference(resolution,[status(thm)],[c74,c0]) ).
cnf(c76,plain,
ssNder1_10r1r1r1r1r1r1r1r1r1r1(X644,X641,X640,X637,X645,X638,X639,X642,X646,X643),
inference(resolution,[status(thm)],[c75,clause1]) ).
cnf(clause20,negated_conjecture,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X490,X492,X491,X494,X495,X493,X486,X489,X487,X485)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X490,X492,X491,X494,X495,X493,X486,X489,X487)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X490,X492,X491,X494,X495,X493,X486,X489)
| ~ ssNder1_7r1r1r1r1r1r1r1(X490,X492,X491,X494,X495,X493,X486)
| ~ ssNder1_6r1r1r1r1r1r1(X490,X492,X491,X494,X495,X493)
| ~ ssNder1_5r1r1r1r1r1(X490,X492,X491,X494,X495)
| ~ ssNder1_4r1r1r1r1(X490,X492,X491,X494)
| ~ ssNder1_3r1r1r1(X490,X492,X491)
| ~ ssNder1_2r1r1(X490,X492)
| ~ ssNder1_1r1(X490)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X490,X492,X491,X494,X495,X493,X486,X489,X487,X485,X488) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c77,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X657,X647,X652,X655,X651,X648,X653,X649,X650)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X657,X647,X652,X655,X651,X648,X653,X649)
| ~ ssNder1_7r1r1r1r1r1r1r1(X657,X647,X652,X655,X651,X648,X653)
| ~ ssNder1_6r1r1r1r1r1r1(X657,X647,X652,X655,X651,X648)
| ~ ssNder1_5r1r1r1r1r1(X657,X647,X652,X655,X651)
| ~ ssNder1_4r1r1r1r1(X657,X647,X652,X655)
| ~ ssNder1_3r1r1r1(X657,X647,X652)
| ~ ssNder1_2r1r1(X657,X647)
| ~ ssNder1_1r1(X657)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X657,X647,X652,X655,X651,X648,X653,X649,X650,X656,X654) ),
inference(resolution,[status(thm)],[c76,clause20]) ).
cnf(c78,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X665,X668,X661,X660,X666,X659,X662,X664)
| ~ ssNder1_7r1r1r1r1r1r1r1(X665,X668,X661,X660,X666,X659,X662)
| ~ ssNder1_6r1r1r1r1r1r1(X665,X668,X661,X660,X666,X659)
| ~ ssNder1_5r1r1r1r1r1(X665,X668,X661,X660,X666)
| ~ ssNder1_4r1r1r1r1(X665,X668,X661,X660)
| ~ ssNder1_3r1r1r1(X665,X668,X661)
| ~ ssNder1_2r1r1(X665,X668)
| ~ ssNder1_1r1(X665)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X665,X668,X661,X660,X666,X659,X662,X664,X658,X667,X663) ),
inference(resolution,[status(thm)],[c77,c66]) ).
cnf(c79,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X688,X682,X687,X690,X681,X691,X685)
| ~ ssNder1_6r1r1r1r1r1r1(X688,X682,X687,X690,X681,X691)
| ~ ssNder1_5r1r1r1r1r1(X688,X682,X687,X690,X681)
| ~ ssNder1_4r1r1r1r1(X688,X682,X687,X690)
| ~ ssNder1_3r1r1r1(X688,X682,X687)
| ~ ssNder1_2r1r1(X688,X682)
| ~ ssNder1_1r1(X688)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X688,X682,X687,X690,X681,X691,X685,X683,X686,X689,X684) ),
inference(resolution,[status(thm)],[c78,c57]) ).
cnf(c80,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X699,X700,X702,X701,X694,X696)
| ~ ssNder1_5r1r1r1r1r1(X699,X700,X702,X701,X694)
| ~ ssNder1_4r1r1r1r1(X699,X700,X702,X701)
| ~ ssNder1_3r1r1r1(X699,X700,X702)
| ~ ssNder1_2r1r1(X699,X700)
| ~ ssNder1_1r1(X699)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X699,X700,X702,X701,X694,X696,X697,X698,X693,X692,X695) ),
inference(resolution,[status(thm)],[c79,c43]) ).
cnf(c81,plain,
( ~ ssNder1_5r1r1r1r1r1(X709,X713,X704,X710,X711)
| ~ ssNder1_4r1r1r1r1(X709,X713,X704,X710)
| ~ ssNder1_3r1r1r1(X709,X713,X704)
| ~ ssNder1_2r1r1(X709,X713)
| ~ ssNder1_1r1(X709)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X709,X713,X704,X710,X711,X703,X712,X708,X706,X705,X707) ),
inference(resolution,[status(thm)],[c80,c30]) ).
cnf(c82,plain,
( ~ ssNder1_4r1r1r1r1(X717,X716,X714,X719)
| ~ ssNder1_3r1r1r1(X717,X716,X714)
| ~ ssNder1_2r1r1(X717,X716)
| ~ ssNder1_1r1(X717)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X717,X716,X714,X719,X722,X720,X718,X715,X724,X723,X721) ),
inference(resolution,[status(thm)],[c81,c19]) ).
cnf(c83,plain,
( ~ ssNder1_3r1r1r1(X730,X728,X731)
| ~ ssNder1_2r1r1(X730,X728)
| ~ ssNder1_1r1(X730)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X730,X728,X731,X727,X732,X729,X726,X734,X725,X735,X733) ),
inference(resolution,[status(thm)],[c82,c10]) ).
cnf(c84,plain,
( ~ ssNder1_2r1r1(X751,X755)
| ~ ssNder1_1r1(X751)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X751,X755,X747,X753,X748,X752,X749,X754,X757,X756,X750) ),
inference(resolution,[status(thm)],[c83,c5]) ).
cnf(c86,plain,
( ~ ssNder1_1r1(X761)
| ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X761,X763,X768,X766,X759,X758,X764,X765,X762,X767,X760) ),
inference(resolution,[status(thm)],[c84,c2]) ).
cnf(c87,plain,
( ~ ssNder1_0
| ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X771,X776,X779,X769,X775,X774,X777,X773,X778,X770,X772) ),
inference(resolution,[status(thm)],[c86,c0]) ).
cnf(c88,plain,
ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X780,X781,X784,X789,X790,X786,X788,X785,X787,X782,X783),
inference(resolution,[status(thm)],[c87,clause1]) ).
cnf(clause21,negated_conjecture,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X548,X551,X549,X553,X554,X552,X544,X547,X545,X543,X546)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X548,X551,X549,X553,X554,X552,X544,X547,X545,X543)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X548,X551,X549,X553,X554,X552,X544,X547,X545)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X548,X551,X549,X553,X554,X552,X544,X547)
| ~ ssNder1_7r1r1r1r1r1r1r1(X548,X551,X549,X553,X554,X552,X544)
| ~ ssNder1_6r1r1r1r1r1r1(X548,X551,X549,X553,X554,X552)
| ~ ssNder1_5r1r1r1r1r1(X548,X551,X549,X553,X554)
| ~ ssNder1_4r1r1r1r1(X548,X551,X549,X553)
| ~ ssNder1_3r1r1r1(X548,X551,X549)
| ~ ssNder1_2r1r1(X548,X551)
| ~ ssNder1_1r1(X548)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X548,X551,X549,X553,X554,X552,X544,X547,X545,X543,X546,X550) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(c89,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X796,X794,X791,X802,X801,X795,X797,X798,X799,X792)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X796,X794,X791,X802,X801,X795,X797,X798,X799)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X796,X794,X791,X802,X801,X795,X797,X798)
| ~ ssNder1_7r1r1r1r1r1r1r1(X796,X794,X791,X802,X801,X795,X797)
| ~ ssNder1_6r1r1r1r1r1r1(X796,X794,X791,X802,X801,X795)
| ~ ssNder1_5r1r1r1r1r1(X796,X794,X791,X802,X801)
| ~ ssNder1_4r1r1r1r1(X796,X794,X791,X802)
| ~ ssNder1_3r1r1r1(X796,X794,X791)
| ~ ssNder1_2r1r1(X796,X794)
| ~ ssNder1_1r1(X796)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X796,X794,X791,X802,X801,X795,X797,X798,X799,X792,X793,X800) ),
inference(resolution,[status(thm)],[c88,clause21]) ).
cnf(c91,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X827,X822,X823,X820,X825,X817,X821,X816,X818)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X827,X822,X823,X820,X825,X817,X821,X816)
| ~ ssNder1_7r1r1r1r1r1r1r1(X827,X822,X823,X820,X825,X817,X821)
| ~ ssNder1_6r1r1r1r1r1r1(X827,X822,X823,X820,X825,X817)
| ~ ssNder1_5r1r1r1r1r1(X827,X822,X823,X820,X825)
| ~ ssNder1_4r1r1r1r1(X827,X822,X823,X820)
| ~ ssNder1_3r1r1r1(X827,X822,X823)
| ~ ssNder1_2r1r1(X827,X822)
| ~ ssNder1_1r1(X827)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X827,X822,X823,X820,X825,X817,X821,X816,X818,X824,X819,X826) ),
inference(resolution,[status(thm)],[c89,c76]) ).
cnf(c92,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X836,X839,X832,X831,X838,X830,X834,X835)
| ~ ssNder1_7r1r1r1r1r1r1r1(X836,X839,X832,X831,X838,X830,X834)
| ~ ssNder1_6r1r1r1r1r1r1(X836,X839,X832,X831,X838,X830)
| ~ ssNder1_5r1r1r1r1r1(X836,X839,X832,X831,X838)
| ~ ssNder1_4r1r1r1r1(X836,X839,X832,X831)
| ~ ssNder1_3r1r1r1(X836,X839,X832)
| ~ ssNder1_2r1r1(X836,X839)
| ~ ssNder1_1r1(X836)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X836,X839,X832,X831,X838,X830,X834,X835,X828,X837,X833,X829) ),
inference(resolution,[status(thm)],[c91,c66]) ).
cnf(c93,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X848,X841,X845,X849,X840,X850,X843)
| ~ ssNder1_6r1r1r1r1r1r1(X848,X841,X845,X849,X840,X850)
| ~ ssNder1_5r1r1r1r1r1(X848,X841,X845,X849,X840)
| ~ ssNder1_4r1r1r1r1(X848,X841,X845,X849)
| ~ ssNder1_3r1r1r1(X848,X841,X845)
| ~ ssNder1_2r1r1(X848,X841)
| ~ ssNder1_1r1(X848)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X848,X841,X845,X849,X840,X850,X843,X842,X847,X846,X851,X844) ),
inference(resolution,[status(thm)],[c92,c57]) ).
cnf(c94,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X859,X860,X863,X862,X853,X854)
| ~ ssNder1_5r1r1r1r1r1(X859,X860,X863,X862,X853)
| ~ ssNder1_4r1r1r1r1(X859,X860,X863,X862)
| ~ ssNder1_3r1r1r1(X859,X860,X863)
| ~ ssNder1_2r1r1(X859,X860)
| ~ ssNder1_1r1(X859)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X859,X860,X863,X862,X853,X854,X855,X861,X856,X857,X858,X852) ),
inference(resolution,[status(thm)],[c93,c43]) ).
cnf(c95,plain,
( ~ ssNder1_5r1r1r1r1r1(X871,X875,X865,X872,X873)
| ~ ssNder1_4r1r1r1r1(X871,X875,X865,X872)
| ~ ssNder1_3r1r1r1(X871,X875,X865)
| ~ ssNder1_2r1r1(X871,X875)
| ~ ssNder1_1r1(X871)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X871,X875,X865,X872,X873,X864,X874,X867,X866,X868,X869,X870) ),
inference(resolution,[status(thm)],[c94,c30]) ).
cnf(c96,plain,
( ~ ssNder1_4r1r1r1r1(X895,X892,X890,X898)
| ~ ssNder1_3r1r1r1(X895,X892,X890)
| ~ ssNder1_2r1r1(X895,X892)
| ~ ssNder1_1r1(X895)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X895,X892,X890,X898,X899,X891,X897,X896,X893,X900,X889,X894) ),
inference(resolution,[status(thm)],[c95,c19]) ).
cnf(c97,plain,
( ~ ssNder1_3r1r1r1(X907,X905,X908)
| ~ ssNder1_2r1r1(X907,X905)
| ~ ssNder1_1r1(X907)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X907,X905,X908,X904,X912,X911,X901,X902,X903,X906,X909,X910) ),
inference(resolution,[status(thm)],[c96,c10]) ).
cnf(c98,plain,
( ~ ssNder1_2r1r1(X918,X920)
| ~ ssNder1_1r1(X918)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X918,X920,X913,X923,X917,X919,X924,X914,X921,X915,X916,X922) ),
inference(resolution,[status(thm)],[c97,c5]) ).
cnf(c99,plain,
( ~ ssNder1_1r1(X927)
| ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X927,X933,X932,X936,X934,X925,X928,X926,X935,X929,X930,X931) ),
inference(resolution,[status(thm)],[c98,c2]) ).
cnf(c100,plain,
( ~ ssNder1_0
| ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X941,X943,X944,X947,X945,X940,X939,X948,X942,X938,X946,X937) ),
inference(resolution,[status(thm)],[c99,c0]) ).
cnf(c101,plain,
ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X967,X969,X963,X971,X972,X970,X966,X973,X968,X965,X962,X964),
inference(resolution,[status(thm)],[c100,clause1]) ).
cnf(clause25,negated_conjecture,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X808,X812,X810,X814,X815,X813,X804,X807,X805,X803,X806,X811)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X808,X812,X810,X814,X815,X813,X804,X807,X805,X803,X806)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X808,X812,X810,X814,X815,X813,X804,X807,X805,X803)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X808,X812,X810,X814,X815,X813,X804,X807,X805)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X808,X812,X810,X814,X815,X813,X804,X807)
| ~ ssNder1_7r1r1r1r1r1r1r1(X808,X812,X810,X814,X815,X813,X804)
| ~ ssNder1_6r1r1r1r1r1r1(X808,X812,X810,X814,X815,X813)
| ~ ssNder1_5r1r1r1r1r1(X808,X812,X810,X814,X815)
| ~ ssNder1_4r1r1r1r1(X808,X812,X810,X814)
| ~ ssNder1_3r1r1r1(X808,X812,X810)
| ~ ssNder1_2r1r1(X808,X812)
| ~ ssNder1_1r1(X808)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X808,X812,X810,X814,X815,X813,X804,X807,X805,X803,X806,X811,X809) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(c103,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1278,X1285,X1284,X1276,X1277,X1279,X1286,X1283,X1280,X1281,X1287)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1278,X1285,X1284,X1276,X1277,X1279,X1286,X1283,X1280,X1281)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1278,X1285,X1284,X1276,X1277,X1279,X1286,X1283,X1280)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1278,X1285,X1284,X1276,X1277,X1279,X1286,X1283)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1278,X1285,X1284,X1276,X1277,X1279,X1286)
| ~ ssNder1_6r1r1r1r1r1r1(X1278,X1285,X1284,X1276,X1277,X1279)
| ~ ssNder1_5r1r1r1r1r1(X1278,X1285,X1284,X1276,X1277)
| ~ ssNder1_4r1r1r1r1(X1278,X1285,X1284,X1276)
| ~ ssNder1_3r1r1r1(X1278,X1285,X1284)
| ~ ssNder1_2r1r1(X1278,X1285)
| ~ ssNder1_1r1(X1278)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1278,X1285,X1284,X1276,X1277,X1279,X1286,X1283,X1280,X1281,X1287,X1275,X1282) ),
inference(resolution,[status(thm)],[c101,clause25]) ).
cnf(c125,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1300,X1293,X1290,X1288,X1296,X1297,X1299,X1291,X1294,X1295)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1300,X1293,X1290,X1288,X1296,X1297,X1299,X1291,X1294)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1300,X1293,X1290,X1288,X1296,X1297,X1299,X1291)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1300,X1293,X1290,X1288,X1296,X1297,X1299)
| ~ ssNder1_6r1r1r1r1r1r1(X1300,X1293,X1290,X1288,X1296,X1297)
| ~ ssNder1_5r1r1r1r1r1(X1300,X1293,X1290,X1288,X1296)
| ~ ssNder1_4r1r1r1r1(X1300,X1293,X1290,X1288)
| ~ ssNder1_3r1r1r1(X1300,X1293,X1290)
| ~ ssNder1_2r1r1(X1300,X1293)
| ~ ssNder1_1r1(X1300)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1300,X1293,X1290,X1288,X1296,X1297,X1299,X1291,X1294,X1295,X1289,X1298,X1292) ),
inference(resolution,[status(thm)],[c103,c88]) ).
cnf(c126,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1327,X1322,X1323,X1319,X1325,X1316,X1320,X1315,X1317)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1327,X1322,X1323,X1319,X1325,X1316,X1320,X1315)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1327,X1322,X1323,X1319,X1325,X1316,X1320)
| ~ ssNder1_6r1r1r1r1r1r1(X1327,X1322,X1323,X1319,X1325,X1316)
| ~ ssNder1_5r1r1r1r1r1(X1327,X1322,X1323,X1319,X1325)
| ~ ssNder1_4r1r1r1r1(X1327,X1322,X1323,X1319)
| ~ ssNder1_3r1r1r1(X1327,X1322,X1323)
| ~ ssNder1_2r1r1(X1327,X1322)
| ~ ssNder1_1r1(X1327)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1327,X1322,X1323,X1319,X1325,X1316,X1320,X1315,X1317,X1324,X1321,X1326,X1318) ),
inference(resolution,[status(thm)],[c125,c76]) ).
cnf(c127,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X1336,X1340,X1331,X1330,X1338,X1329,X1332,X1333)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1336,X1340,X1331,X1330,X1338,X1329,X1332)
| ~ ssNder1_6r1r1r1r1r1r1(X1336,X1340,X1331,X1330,X1338,X1329)
| ~ ssNder1_5r1r1r1r1r1(X1336,X1340,X1331,X1330,X1338)
| ~ ssNder1_4r1r1r1r1(X1336,X1340,X1331,X1330)
| ~ ssNder1_3r1r1r1(X1336,X1340,X1331)
| ~ ssNder1_2r1r1(X1336,X1340)
| ~ ssNder1_1r1(X1336)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1336,X1340,X1331,X1330,X1338,X1329,X1332,X1333,X1328,X1337,X1334,X1339,X1335) ),
inference(resolution,[status(thm)],[c126,c66]) ).
cnf(c128,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X1348,X1342,X1347,X1349,X1341,X1351,X1344)
| ~ ssNder1_6r1r1r1r1r1r1(X1348,X1342,X1347,X1349,X1341,X1351)
| ~ ssNder1_5r1r1r1r1r1(X1348,X1342,X1347,X1349,X1341)
| ~ ssNder1_4r1r1r1r1(X1348,X1342,X1347,X1349)
| ~ ssNder1_3r1r1r1(X1348,X1342,X1347)
| ~ ssNder1_2r1r1(X1348,X1342)
| ~ ssNder1_1r1(X1348)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1348,X1342,X1347,X1349,X1341,X1351,X1344,X1343,X1345,X1353,X1352,X1350,X1346) ),
inference(resolution,[status(thm)],[c127,c57]) ).
cnf(c129,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X1362,X1363,X1366,X1364,X1355,X1357)
| ~ ssNder1_5r1r1r1r1r1(X1362,X1363,X1366,X1364,X1355)
| ~ ssNder1_4r1r1r1r1(X1362,X1363,X1366,X1364)
| ~ ssNder1_3r1r1r1(X1362,X1363,X1366)
| ~ ssNder1_2r1r1(X1362,X1363)
| ~ ssNder1_1r1(X1362)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1362,X1363,X1366,X1364,X1355,X1357,X1358,X1354,X1360,X1361,X1359,X1356,X1365) ),
inference(resolution,[status(thm)],[c128,c43]) ).
cnf(c130,plain,
( ~ ssNder1_5r1r1r1r1r1(X1375,X1379,X1369,X1376,X1377)
| ~ ssNder1_4r1r1r1r1(X1375,X1379,X1369,X1376)
| ~ ssNder1_3r1r1r1(X1375,X1379,X1369)
| ~ ssNder1_2r1r1(X1375,X1379)
| ~ ssNder1_1r1(X1375)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1375,X1379,X1369,X1376,X1377,X1368,X1372,X1370,X1374,X1367,X1378,X1373,X1371) ),
inference(resolution,[status(thm)],[c129,c30]) ).
cnf(c131,plain,
( ~ ssNder1_4r1r1r1r1(X1403,X1396,X1395,X1404)
| ~ ssNder1_3r1r1r1(X1403,X1396,X1395)
| ~ ssNder1_2r1r1(X1403,X1396)
| ~ ssNder1_1r1(X1403)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1403,X1396,X1395,X1404,X1406,X1397,X1399,X1401,X1407,X1398,X1400,X1405,X1402) ),
inference(resolution,[status(thm)],[c130,c19]) ).
cnf(c132,plain,
( ~ ssNder1_3r1r1r1(X1414,X1411,X1416)
| ~ ssNder1_2r1r1(X1414,X1411)
| ~ ssNder1_1r1(X1414)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1414,X1411,X1416,X1409,X1410,X1412,X1415,X1413,X1418,X1417,X1419,X1420,X1408) ),
inference(resolution,[status(thm)],[c131,c10]) ).
cnf(c133,plain,
( ~ ssNder1_2r1r1(X1426,X1430)
| ~ ssNder1_1r1(X1426)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1426,X1430,X1421,X1425,X1422,X1427,X1423,X1429,X1433,X1428,X1424,X1431,X1432) ),
inference(resolution,[status(thm)],[c132,c5]) ).
cnf(c134,plain,
( ~ ssNder1_1r1(X1437)
| ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1437,X1441,X1439,X1445,X1443,X1435,X1446,X1434,X1440,X1442,X1438,X1436,X1444) ),
inference(resolution,[status(thm)],[c133,c2]) ).
cnf(c135,plain,
( ~ ssNder1_0
| ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1448,X1454,X1459,X1458,X1447,X1450,X1453,X1457,X1456,X1455,X1451,X1452,X1449) ),
inference(resolution,[status(thm)],[c134,c0]) ).
cnf(c136,plain,
ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1479,X1483,X1486,X1484,X1487,X1481,X1485,X1477,X1475,X1476,X1478,X1480,X1482),
inference(resolution,[status(thm)],[c135,clause1]) ).
cnf(clause31,negated_conjecture,
( ~ ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1236,X1241,X1239,X1243,X1244,X1242,X1232,X1235,X1233,X1231,X1234,X1240,X1238,X1237,skc19)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1236,X1241,X1239,X1243,X1244,X1242,X1232,X1235,X1233,X1231,X1234,X1240,X1238)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1236,X1241,X1239,X1243,X1244,X1242,X1232,X1235,X1233,X1231,X1234,X1240)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1236,X1241,X1239,X1243,X1244,X1242,X1232,X1235,X1233,X1231,X1234)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1236,X1241,X1239,X1243,X1244,X1242,X1232,X1235,X1233,X1231)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1236,X1241,X1239,X1243,X1244,X1242,X1232,X1235,X1233)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1236,X1241,X1239,X1243,X1244,X1242,X1232,X1235)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1236,X1241,X1239,X1243,X1244,X1242,X1232)
| ~ ssNder1_6r1r1r1r1r1r1(X1236,X1241,X1239,X1243,X1244,X1242)
| ~ ssNder1_5r1r1r1r1r1(X1236,X1241,X1239,X1243,X1244)
| ~ ssNder1_4r1r1r1r1(X1236,X1241,X1239,X1243)
| ~ ssNder1_3r1r1r1(X1236,X1241,X1239)
| ~ ssNder1_2r1r1(X1236,X1241)
| ~ ssNder1_1r1(X1236)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(clause7,negated_conjecture,
( ~ ssPv16_5r1r1r1r1r1(X52,X53,X50,X51,skc31)
| ~ ssNder1_3r1r1r1(X52,X53,X50)
| ~ ssNder1_2r1r1(X52,X53)
| ~ ssNder1_1r1(X52)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(clause39,negated_conjecture,
( ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854,X1852,X1841,X1844,X1842,X1840,X1843,X1849,X1847,X1846)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854,X1852,X1841,X1844,X1842,X1840,X1843,X1849,X1847)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854,X1852,X1841,X1844,X1842,X1840,X1843,X1849)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854,X1852,X1841,X1844,X1842,X1840,X1843)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854,X1852,X1841,X1844,X1842,X1840)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854,X1852,X1841,X1844,X1842)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854,X1852,X1841,X1844)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854,X1852,X1841)
| ~ ssNder1_6r1r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854,X1852)
| ~ ssNder1_5r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854)
| ~ ssNder1_4r1r1r1r1(X1845,X1851,X1848,X1853)
| ~ ssNder1_3r1r1r1(X1845,X1851,X1848)
| ~ ssNder1_2r1r1(X1845,X1851)
| ~ ssNder1_1r1(X1845)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854,X1852,X1841,X1844,X1842,X1840,X1843,X1849,X1847,X1846,X1850)
| ssPv16_5r1r1r1r1r1(X1845,X1851,X1848,X1853,X1854)
| ssPv19_2r1r1(X1845,X1851)
| ssPv20_1r1(X1845) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
cnf(clause29,negated_conjecture,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1099,X1104,X1102,X1106,X1107,X1105,X1095,X1098,X1096,X1094,X1097,X1103,X1101)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1099,X1104,X1102,X1106,X1107,X1105,X1095,X1098,X1096,X1094,X1097,X1103)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1099,X1104,X1102,X1106,X1107,X1105,X1095,X1098,X1096,X1094,X1097)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1099,X1104,X1102,X1106,X1107,X1105,X1095,X1098,X1096,X1094)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1099,X1104,X1102,X1106,X1107,X1105,X1095,X1098,X1096)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1099,X1104,X1102,X1106,X1107,X1105,X1095,X1098)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1099,X1104,X1102,X1106,X1107,X1105,X1095)
| ~ ssNder1_6r1r1r1r1r1r1(X1099,X1104,X1102,X1106,X1107,X1105)
| ~ ssNder1_5r1r1r1r1r1(X1099,X1104,X1102,X1106,X1107)
| ~ ssNder1_4r1r1r1r1(X1099,X1104,X1102,X1106)
| ~ ssNder1_3r1r1r1(X1099,X1104,X1102)
| ~ ssNder1_2r1r1(X1099,X1104)
| ~ ssNder1_1r1(X1099)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1099,X1104,X1102,X1106,X1107,X1105,X1095,X1098,X1096,X1094,X1097,X1103,X1101,X1100) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
cnf(c139,plain,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X2112,X2102,X2105,X2104,X2103,X2106,X2101,X2109,X2113,X2110,X2114,X2107)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X2112,X2102,X2105,X2104,X2103,X2106,X2101,X2109,X2113,X2110,X2114)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X2112,X2102,X2105,X2104,X2103,X2106,X2101,X2109,X2113,X2110)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2112,X2102,X2105,X2104,X2103,X2106,X2101,X2109,X2113)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2112,X2102,X2105,X2104,X2103,X2106,X2101,X2109)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2112,X2102,X2105,X2104,X2103,X2106,X2101)
| ~ ssNder1_6r1r1r1r1r1r1(X2112,X2102,X2105,X2104,X2103,X2106)
| ~ ssNder1_5r1r1r1r1r1(X2112,X2102,X2105,X2104,X2103)
| ~ ssNder1_4r1r1r1r1(X2112,X2102,X2105,X2104)
| ~ ssNder1_3r1r1r1(X2112,X2102,X2105)
| ~ ssNder1_2r1r1(X2112,X2102)
| ~ ssNder1_1r1(X2112)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2112,X2102,X2105,X2104,X2103,X2106,X2101,X2109,X2113,X2110,X2114,X2107,X2111,X2108) ),
inference(resolution,[status(thm)],[c136,clause29]) ).
cnf(c182,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X2117,X2115,X2125,X2124,X2116,X2119,X2122,X2120,X2123,X2128,X2118)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X2117,X2115,X2125,X2124,X2116,X2119,X2122,X2120,X2123,X2128)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2117,X2115,X2125,X2124,X2116,X2119,X2122,X2120,X2123)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2117,X2115,X2125,X2124,X2116,X2119,X2122,X2120)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2117,X2115,X2125,X2124,X2116,X2119,X2122)
| ~ ssNder1_6r1r1r1r1r1r1(X2117,X2115,X2125,X2124,X2116,X2119)
| ~ ssNder1_5r1r1r1r1r1(X2117,X2115,X2125,X2124,X2116)
| ~ ssNder1_4r1r1r1r1(X2117,X2115,X2125,X2124)
| ~ ssNder1_3r1r1r1(X2117,X2115,X2125)
| ~ ssNder1_2r1r1(X2117,X2115)
| ~ ssNder1_1r1(X2117)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2117,X2115,X2125,X2124,X2116,X2119,X2122,X2120,X2123,X2128,X2118,X2127,X2121,X2126) ),
inference(resolution,[status(thm)],[c139,c101]) ).
cnf(c183,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X2141,X2135,X2132,X2129,X2138,X2139,X2140,X2134,X2136,X2137)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2141,X2135,X2132,X2129,X2138,X2139,X2140,X2134,X2136)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2141,X2135,X2132,X2129,X2138,X2139,X2140,X2134)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2141,X2135,X2132,X2129,X2138,X2139,X2140)
| ~ ssNder1_6r1r1r1r1r1r1(X2141,X2135,X2132,X2129,X2138,X2139)
| ~ ssNder1_5r1r1r1r1r1(X2141,X2135,X2132,X2129,X2138)
| ~ ssNder1_4r1r1r1r1(X2141,X2135,X2132,X2129)
| ~ ssNder1_3r1r1r1(X2141,X2135,X2132)
| ~ ssNder1_2r1r1(X2141,X2135)
| ~ ssNder1_1r1(X2141)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2141,X2135,X2132,X2129,X2138,X2139,X2140,X2134,X2136,X2137,X2131,X2142,X2130,X2133) ),
inference(resolution,[status(thm)],[c182,c88]) ).
cnf(c184,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2171,X2167,X2168,X2162,X2170,X2159,X2165,X2158,X2160)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2171,X2167,X2168,X2162,X2170,X2159,X2165,X2158)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2171,X2167,X2168,X2162,X2170,X2159,X2165)
| ~ ssNder1_6r1r1r1r1r1r1(X2171,X2167,X2168,X2162,X2170,X2159)
| ~ ssNder1_5r1r1r1r1r1(X2171,X2167,X2168,X2162,X2170)
| ~ ssNder1_4r1r1r1r1(X2171,X2167,X2168,X2162)
| ~ ssNder1_3r1r1r1(X2171,X2167,X2168)
| ~ ssNder1_2r1r1(X2171,X2167)
| ~ ssNder1_1r1(X2171)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2171,X2167,X2168,X2162,X2170,X2159,X2165,X2158,X2160,X2169,X2161,X2166,X2163,X2164) ),
inference(resolution,[status(thm)],[c183,c76]) ).
cnf(c185,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X2180,X2185,X2177,X2176,X2183,X2175,X2178,X2179)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2180,X2185,X2177,X2176,X2183,X2175,X2178)
| ~ ssNder1_6r1r1r1r1r1r1(X2180,X2185,X2177,X2176,X2183,X2175)
| ~ ssNder1_5r1r1r1r1r1(X2180,X2185,X2177,X2176,X2183)
| ~ ssNder1_4r1r1r1r1(X2180,X2185,X2177,X2176)
| ~ ssNder1_3r1r1r1(X2180,X2185,X2177)
| ~ ssNder1_2r1r1(X2180,X2185)
| ~ ssNder1_1r1(X2180)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2180,X2185,X2177,X2176,X2183,X2175,X2178,X2179,X2173,X2172,X2184,X2174,X2182,X2181) ),
inference(resolution,[status(thm)],[c184,c66]) ).
cnf(c186,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X2195,X2188,X2193,X2197,X2187,X2199,X2190)
| ~ ssNder1_6r1r1r1r1r1r1(X2195,X2188,X2193,X2197,X2187,X2199)
| ~ ssNder1_5r1r1r1r1r1(X2195,X2188,X2193,X2197,X2187)
| ~ ssNder1_4r1r1r1r1(X2195,X2188,X2193,X2197)
| ~ ssNder1_3r1r1r1(X2195,X2188,X2193)
| ~ ssNder1_2r1r1(X2195,X2188)
| ~ ssNder1_1r1(X2195)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2195,X2188,X2193,X2197,X2187,X2199,X2190,X2189,X2191,X2194,X2192,X2196,X2198,X2186) ),
inference(resolution,[status(thm)],[c185,c57]) ).
cnf(c187,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X2207,X2208,X2211,X2209,X2201,X2204)
| ~ ssNder1_5r1r1r1r1r1(X2207,X2208,X2211,X2209,X2201)
| ~ ssNder1_4r1r1r1r1(X2207,X2208,X2211,X2209)
| ~ ssNder1_3r1r1r1(X2207,X2208,X2211)
| ~ ssNder1_2r1r1(X2207,X2208)
| ~ ssNder1_1r1(X2207)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2207,X2208,X2211,X2209,X2201,X2204,X2205,X2206,X2213,X2202,X2200,X2203,X2210,X2212) ),
inference(resolution,[status(thm)],[c186,c43]) ).
cnf(c188,plain,
( ~ ssNder1_5r1r1r1r1r1(X2218,X2227,X2215,X2219,X2222)
| ~ ssNder1_4r1r1r1r1(X2218,X2227,X2215,X2219)
| ~ ssNder1_3r1r1r1(X2218,X2227,X2215)
| ~ ssNder1_2r1r1(X2218,X2227)
| ~ ssNder1_1r1(X2218)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2218,X2227,X2215,X2219,X2222,X2214,X2217,X2223,X2225,X2224,X2220,X2216,X2221,X2226) ),
inference(resolution,[status(thm)],[c187,c30]) ).
cnf(c189,plain,
( ~ ssNder1_4r1r1r1r1(X2249,X2246,X2245,X2252)
| ~ ssNder1_3r1r1r1(X2249,X2246,X2245)
| ~ ssNder1_2r1r1(X2249,X2246)
| ~ ssNder1_1r1(X2249)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2249,X2246,X2245,X2252,X2256,X2248,X2250,X2251,X2253,X2254,X2255,X2257,X2258,X2247) ),
inference(resolution,[status(thm)],[c188,c19]) ).
cnf(c190,plain,
( ~ ssNder1_3r1r1r1(X2264,X2262,X2267)
| ~ ssNder1_2r1r1(X2264,X2262)
| ~ ssNder1_1r1(X2264)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2264,X2262,X2267,X2260,X2265,X2270,X2268,X2259,X2269,X2261,X2266,X2271,X2272,X2263) ),
inference(resolution,[status(thm)],[c189,c10]) ).
cnf(c191,plain,
( ~ ssNder1_2r1r1(X2275,X2278)
| ~ ssNder1_1r1(X2275)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2275,X2278,X2273,X2279,X2286,X2285,X2281,X2280,X2282,X2276,X2283,X2274,X2277,X2284) ),
inference(resolution,[status(thm)],[c190,c5]) ).
cnf(c192,plain,
( ~ ssNder1_1r1(X2290)
| ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2290,X2293,X2294,X2292,X2291,X2287,X2297,X2300,X2295,X2289,X2288,X2296,X2299,X2298) ),
inference(resolution,[status(thm)],[c191,c2]) ).
cnf(c193,plain,
( ~ ssNder1_0
| ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2303,X2307,X2302,X2305,X2309,X2310,X2311,X2301,X2308,X2312,X2306,X2313,X2304,X2314) ),
inference(resolution,[status(thm)],[c192,c0]) ).
cnf(c194,plain,
ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2343,X2331,X2334,X2344,X2337,X2338,X2335,X2339,X2333,X2340,X2341,X2342,X2336,X2332),
inference(resolution,[status(thm)],[c193,clause1]) ).
cnf(c198,plain,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277,X4280,X4273,X4274,X4285,X4278,X4283,X4287,X4286)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277,X4280,X4273,X4274,X4285,X4278,X4283,X4287)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277,X4280,X4273,X4274,X4285,X4278,X4283)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277,X4280,X4273,X4274,X4285,X4278)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277,X4280,X4273,X4274,X4285)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277,X4280,X4273,X4274)
| ~ ssNder1_7r1r1r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277,X4280,X4273)
| ~ ssNder1_6r1r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277,X4280)
| ~ ssNder1_5r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277)
| ~ ssNder1_4r1r1r1r1(X4281,X4284,X4275,X4282)
| ~ ssNder1_3r1r1r1(X4281,X4284,X4275)
| ~ ssNder1_2r1r1(X4281,X4284)
| ~ ssNder1_1r1(X4281)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277,X4280,X4273,X4274,X4285,X4278,X4283,X4287,X4286,X4276,X4279)
| ssPv16_5r1r1r1r1r1(X4281,X4284,X4275,X4282,X4277)
| ssPv19_2r1r1(X4281,X4284)
| ssPv20_1r1(X4281) ),
inference(resolution,[status(thm)],[c194,clause39]) ).
cnf(c315,plain,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X6424,X6428,X6426,X6427,X6435,X6422,X6425,X6432,X6429,X6423,X6436,X6431)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X6424,X6428,X6426,X6427,X6435,X6422,X6425,X6432,X6429,X6423,X6436)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X6424,X6428,X6426,X6427,X6435,X6422,X6425,X6432,X6429,X6423)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X6424,X6428,X6426,X6427,X6435,X6422,X6425,X6432,X6429)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X6424,X6428,X6426,X6427,X6435,X6422,X6425,X6432)
| ~ ssNder1_7r1r1r1r1r1r1r1(X6424,X6428,X6426,X6427,X6435,X6422,X6425)
| ~ ssNder1_6r1r1r1r1r1r1(X6424,X6428,X6426,X6427,X6435,X6422)
| ~ ssNder1_5r1r1r1r1r1(X6424,X6428,X6426,X6427,X6435)
| ~ ssNder1_4r1r1r1r1(X6424,X6428,X6426,X6427)
| ~ ssNder1_3r1r1r1(X6424,X6428,X6426)
| ~ ssNder1_2r1r1(X6424,X6428)
| ~ ssNder1_1r1(X6424)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6424,X6428,X6426,X6427,X6435,X6422,X6425,X6432,X6429,X6423,X6436,X6431,X6433,X6430,X6434)
| ssPv16_5r1r1r1r1r1(X6424,X6428,X6426,X6427,X6435)
| ssPv19_2r1r1(X6424,X6428)
| ssPv20_1r1(X6424) ),
inference(resolution,[status(thm)],[c198,c136]) ).
cnf(c433,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X6439,X6437,X6448,X6447,X6438,X6441,X6444,X6442,X6446,X6451,X6440)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X6439,X6437,X6448,X6447,X6438,X6441,X6444,X6442,X6446,X6451)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X6439,X6437,X6448,X6447,X6438,X6441,X6444,X6442,X6446)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X6439,X6437,X6448,X6447,X6438,X6441,X6444,X6442)
| ~ ssNder1_7r1r1r1r1r1r1r1(X6439,X6437,X6448,X6447,X6438,X6441,X6444)
| ~ ssNder1_6r1r1r1r1r1r1(X6439,X6437,X6448,X6447,X6438,X6441)
| ~ ssNder1_5r1r1r1r1r1(X6439,X6437,X6448,X6447,X6438)
| ~ ssNder1_4r1r1r1r1(X6439,X6437,X6448,X6447)
| ~ ssNder1_3r1r1r1(X6439,X6437,X6448)
| ~ ssNder1_2r1r1(X6439,X6437)
| ~ ssNder1_1r1(X6439)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6439,X6437,X6448,X6447,X6438,X6441,X6444,X6442,X6446,X6451,X6440,X6450,X6449,X6445,X6443)
| ssPv16_5r1r1r1r1r1(X6439,X6437,X6448,X6447,X6438)
| ssPv19_2r1r1(X6439,X6437)
| ssPv20_1r1(X6439) ),
inference(resolution,[status(thm)],[c315,c101]) ).
cnf(c434,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X6466,X6458,X6456,X6453,X6462,X6463,X6465,X6457,X6459,X6460)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X6466,X6458,X6456,X6453,X6462,X6463,X6465,X6457,X6459)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X6466,X6458,X6456,X6453,X6462,X6463,X6465,X6457)
| ~ ssNder1_7r1r1r1r1r1r1r1(X6466,X6458,X6456,X6453,X6462,X6463,X6465)
| ~ ssNder1_6r1r1r1r1r1r1(X6466,X6458,X6456,X6453,X6462,X6463)
| ~ ssNder1_5r1r1r1r1r1(X6466,X6458,X6456,X6453,X6462)
| ~ ssNder1_4r1r1r1r1(X6466,X6458,X6456,X6453)
| ~ ssNder1_3r1r1r1(X6466,X6458,X6456)
| ~ ssNder1_2r1r1(X6466,X6458)
| ~ ssNder1_1r1(X6466)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6466,X6458,X6456,X6453,X6462,X6463,X6465,X6457,X6459,X6460,X6454,X6452,X6455,X6461,X6464)
| ssPv16_5r1r1r1r1r1(X6466,X6458,X6456,X6453,X6462)
| ssPv19_2r1r1(X6466,X6458)
| ssPv20_1r1(X6466) ),
inference(resolution,[status(thm)],[c433,c88]) ).
cnf(c435,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X6481,X6474,X6475,X6470,X6479,X6468,X6472,X6467,X6469)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X6481,X6474,X6475,X6470,X6479,X6468,X6472,X6467)
| ~ ssNder1_7r1r1r1r1r1r1r1(X6481,X6474,X6475,X6470,X6479,X6468,X6472)
| ~ ssNder1_6r1r1r1r1r1r1(X6481,X6474,X6475,X6470,X6479,X6468)
| ~ ssNder1_5r1r1r1r1r1(X6481,X6474,X6475,X6470,X6479)
| ~ ssNder1_4r1r1r1r1(X6481,X6474,X6475,X6470)
| ~ ssNder1_3r1r1r1(X6481,X6474,X6475)
| ~ ssNder1_2r1r1(X6481,X6474)
| ~ ssNder1_1r1(X6481)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6481,X6474,X6475,X6470,X6479,X6468,X6472,X6467,X6469,X6476,X6480,X6478,X6473,X6471,X6477)
| ssPv16_5r1r1r1r1r1(X6481,X6474,X6475,X6470,X6479)
| ssPv19_2r1r1(X6481,X6474)
| ssPv20_1r1(X6481) ),
inference(resolution,[status(thm)],[c434,c76]) ).
cnf(c436,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X6490,X6496,X6485,X6484,X6493,X6483,X6487,X6488)
| ~ ssNder1_7r1r1r1r1r1r1r1(X6490,X6496,X6485,X6484,X6493,X6483,X6487)
| ~ ssNder1_6r1r1r1r1r1r1(X6490,X6496,X6485,X6484,X6493,X6483)
| ~ ssNder1_5r1r1r1r1r1(X6490,X6496,X6485,X6484,X6493)
| ~ ssNder1_4r1r1r1r1(X6490,X6496,X6485,X6484)
| ~ ssNder1_3r1r1r1(X6490,X6496,X6485)
| ~ ssNder1_2r1r1(X6490,X6496)
| ~ ssNder1_1r1(X6490)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6490,X6496,X6485,X6484,X6493,X6483,X6487,X6488,X6482,X6491,X6494,X6489,X6492,X6495,X6486)
| ssPv16_5r1r1r1r1r1(X6490,X6496,X6485,X6484,X6493)
| ssPv19_2r1r1(X6490,X6496)
| ssPv20_1r1(X6490) ),
inference(resolution,[status(thm)],[c435,c66]) ).
cnf(c437,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X6508,X6499,X6505,X6510,X6497,X6511,X6501)
| ~ ssNder1_6r1r1r1r1r1r1(X6508,X6499,X6505,X6510,X6497,X6511)
| ~ ssNder1_5r1r1r1r1r1(X6508,X6499,X6505,X6510,X6497)
| ~ ssNder1_4r1r1r1r1(X6508,X6499,X6505,X6510)
| ~ ssNder1_3r1r1r1(X6508,X6499,X6505)
| ~ ssNder1_2r1r1(X6508,X6499)
| ~ ssNder1_1r1(X6508)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6508,X6499,X6505,X6510,X6497,X6511,X6501,X6500,X6506,X6507,X6498,X6502,X6504,X6503,X6509)
| ssPv16_5r1r1r1r1r1(X6508,X6499,X6505,X6510,X6497)
| ssPv19_2r1r1(X6508,X6499)
| ssPv20_1r1(X6508) ),
inference(resolution,[status(thm)],[c436,c57]) ).
cnf(c438,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X6533,X6534,X6540,X6537,X6528,X6529)
| ~ ssNder1_5r1r1r1r1r1(X6533,X6534,X6540,X6537,X6528)
| ~ ssNder1_4r1r1r1r1(X6533,X6534,X6540,X6537)
| ~ ssNder1_3r1r1r1(X6533,X6534,X6540)
| ~ ssNder1_2r1r1(X6533,X6534)
| ~ ssNder1_1r1(X6533)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6533,X6534,X6540,X6537,X6528,X6529,X6530,X6526,X6527,X6535,X6539,X6536,X6532,X6538,X6531)
| ssPv16_5r1r1r1r1r1(X6533,X6534,X6540,X6537,X6528)
| ssPv19_2r1r1(X6533,X6534)
| ssPv20_1r1(X6533) ),
inference(resolution,[status(thm)],[c437,c43]) ).
cnf(c439,plain,
( ~ ssNder1_5r1r1r1r1r1(X6548,X6555,X6543,X6549,X6552)
| ~ ssNder1_4r1r1r1r1(X6548,X6555,X6543,X6549)
| ~ ssNder1_3r1r1r1(X6548,X6555,X6543)
| ~ ssNder1_2r1r1(X6548,X6555)
| ~ ssNder1_1r1(X6548)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6548,X6555,X6543,X6549,X6552,X6542,X6544,X6554,X6541,X6551,X6545,X6546,X6553,X6547,X6550)
| ssPv16_5r1r1r1r1r1(X6548,X6555,X6543,X6549,X6552)
| ssPv19_2r1r1(X6548,X6555)
| ssPv20_1r1(X6548) ),
inference(resolution,[status(thm)],[c438,c30]) ).
cnf(c440,plain,
( ~ ssNder1_4r1r1r1r1(X6562,X6557,X6556,X6566)
| ~ ssNder1_3r1r1r1(X6562,X6557,X6556)
| ~ ssNder1_2r1r1(X6562,X6557)
| ~ ssNder1_1r1(X6562)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6562,X6557,X6556,X6566,X6569,X6565,X6561,X6567,X6559,X6563,X6564,X6558,X6560,X6568,X6570)
| ssPv16_5r1r1r1r1r1(X6562,X6557,X6556,X6566,X6569)
| ssPv19_2r1r1(X6562,X6557)
| ssPv20_1r1(X6562) ),
inference(resolution,[status(thm)],[c439,c19]) ).
cnf(c441,plain,
( ~ ssNder1_3r1r1r1(X6579,X6576,X6582)
| ~ ssNder1_2r1r1(X6579,X6576)
| ~ ssNder1_1r1(X6579)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6579,X6576,X6582,X6574,X6583,X6573,X6572,X6581,X6584,X6580,X6575,X6578,X6577,X6585,X6571)
| ssPv16_5r1r1r1r1r1(X6579,X6576,X6582,X6574,X6583)
| ssPv19_2r1r1(X6579,X6576)
| ssPv20_1r1(X6579) ),
inference(resolution,[status(thm)],[c440,c10]) ).
cnf(c442,plain,
( ~ ssNder1_2r1r1(X6593,X6595)
| ~ ssNder1_1r1(X6593)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6593,X6595,X6586,X6589,X6598,X6596,X6597,X6594,X6599,X6592,X6587,X6588,X6600,X6590,X6591)
| ssPv16_5r1r1r1r1r1(X6593,X6595,X6586,X6589,X6598)
| ssPv19_2r1r1(X6593,X6595)
| ssPv20_1r1(X6593) ),
inference(resolution,[status(thm)],[c441,c5]) ).
cnf(c443,plain,
( ~ ssNder1_1r1(X6635)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6635,X6638,X6641,X6633,X6628,X6629,X6636,X6640,X6631,X6634,X6639,X6630,X6632,X6627,X6637)
| ssPv16_5r1r1r1r1r1(X6635,X6638,X6641,X6633,X6628)
| ssPv19_2r1r1(X6635,X6638)
| ssPv20_1r1(X6635) ),
inference(resolution,[status(thm)],[c442,c2]) ).
cnf(c444,plain,
( ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6646,X6645,X6642,X6653,X6654,X6655,X6650,X6643,X6652,X6649,X6651,X6656,X6644,X6647,X6648)
| ssPv16_5r1r1r1r1r1(X6646,X6645,X6642,X6653,X6654)
| ssPv19_2r1r1(X6646,X6645)
| ssPv20_1r1(X6646) ),
inference(resolution,[status(thm)],[c443,c0]) ).
cnf(c445,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X6658,X6665,X6664,X6668,X6661,X6666,X6662,X6670,X6667,X6669,X6657,X6663,X6671,X6659,X6660)
| ssPv16_5r1r1r1r1r1(X6658,X6665,X6664,X6668,X6661)
| ssPv19_2r1r1(X6658,X6665)
| ssPv20_1r1(X6658) ),
inference(resolution,[status(thm)],[c444,clause1]) ).
cnf(c446,plain,
( ssPv16_5r1r1r1r1r1(X8673,X8666,X8676,X8674,X8668)
| ssPv19_2r1r1(X8673,X8666)
| ssPv20_1r1(X8673)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X8673,X8666,X8676,X8674,X8668,X8672,X8677,X8669,X8667,X8675,X8665,X8671,X8670)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X8673,X8666,X8676,X8674,X8668,X8672,X8677,X8669,X8667,X8675,X8665,X8671)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X8673,X8666,X8676,X8674,X8668,X8672,X8677,X8669,X8667,X8675,X8665)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X8673,X8666,X8676,X8674,X8668,X8672,X8677,X8669,X8667,X8675)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X8673,X8666,X8676,X8674,X8668,X8672,X8677,X8669,X8667)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X8673,X8666,X8676,X8674,X8668,X8672,X8677,X8669)
| ~ ssNder1_7r1r1r1r1r1r1r1(X8673,X8666,X8676,X8674,X8668,X8672,X8677)
| ~ ssNder1_6r1r1r1r1r1r1(X8673,X8666,X8676,X8674,X8668,X8672)
| ~ ssNder1_5r1r1r1r1r1(X8673,X8666,X8676,X8674,X8668)
| ~ ssNder1_4r1r1r1r1(X8673,X8666,X8676,X8674)
| ~ ssNder1_3r1r1r1(X8673,X8666,X8676)
| ~ ssNder1_2r1r1(X8673,X8666)
| ~ ssNder1_1r1(X8673)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c445,clause31]) ).
cnf(c590,plain,
( ssPv16_5r1r1r1r1r1(X17725,X17729,X17727,X17728,X17733)
| ssPv19_2r1r1(X17725,X17729)
| ssPv20_1r1(X17725)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X17725,X17729,X17727,X17728,X17733,X17723,X17726,X17732,X17730,X17724,X17734,X17731)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X17725,X17729,X17727,X17728,X17733,X17723,X17726,X17732,X17730,X17724,X17734)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X17725,X17729,X17727,X17728,X17733,X17723,X17726,X17732,X17730,X17724)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X17725,X17729,X17727,X17728,X17733,X17723,X17726,X17732,X17730)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X17725,X17729,X17727,X17728,X17733,X17723,X17726,X17732)
| ~ ssNder1_7r1r1r1r1r1r1r1(X17725,X17729,X17727,X17728,X17733,X17723,X17726)
| ~ ssNder1_6r1r1r1r1r1r1(X17725,X17729,X17727,X17728,X17733,X17723)
| ~ ssNder1_5r1r1r1r1r1(X17725,X17729,X17727,X17728,X17733)
| ~ ssNder1_4r1r1r1r1(X17725,X17729,X17727,X17728)
| ~ ssNder1_3r1r1r1(X17725,X17729,X17727)
| ~ ssNder1_2r1r1(X17725,X17729)
| ~ ssNder1_1r1(X17725)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c446,c136]) ).
cnf(c983,plain,
( ssPv16_5r1r1r1r1r1(X19307,X19305,X19314,X19313,X19306)
| ssPv19_2r1r1(X19307,X19305)
| ssPv20_1r1(X19307)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X19307,X19305,X19314,X19313,X19306,X19309,X19311,X19310,X19312,X19315,X19308)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X19307,X19305,X19314,X19313,X19306,X19309,X19311,X19310,X19312,X19315)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X19307,X19305,X19314,X19313,X19306,X19309,X19311,X19310,X19312)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X19307,X19305,X19314,X19313,X19306,X19309,X19311,X19310)
| ~ ssNder1_7r1r1r1r1r1r1r1(X19307,X19305,X19314,X19313,X19306,X19309,X19311)
| ~ ssNder1_6r1r1r1r1r1r1(X19307,X19305,X19314,X19313,X19306,X19309)
| ~ ssNder1_5r1r1r1r1r1(X19307,X19305,X19314,X19313,X19306)
| ~ ssNder1_4r1r1r1r1(X19307,X19305,X19314,X19313)
| ~ ssNder1_3r1r1r1(X19307,X19305,X19314)
| ~ ssNder1_2r1r1(X19307,X19305)
| ~ ssNder1_1r1(X19307)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c590,c101]) ).
cnf(c1110,plain,
( ssPv16_5r1r1r1r1r1(X19355,X19349,X19347,X19346,X19352)
| ssPv19_2r1r1(X19355,X19349)
| ssPv20_1r1(X19355)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X19355,X19349,X19347,X19346,X19352,X19353,X19354,X19348,X19350,X19351)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X19355,X19349,X19347,X19346,X19352,X19353,X19354,X19348,X19350)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X19355,X19349,X19347,X19346,X19352,X19353,X19354,X19348)
| ~ ssNder1_7r1r1r1r1r1r1r1(X19355,X19349,X19347,X19346,X19352,X19353,X19354)
| ~ ssNder1_6r1r1r1r1r1r1(X19355,X19349,X19347,X19346,X19352,X19353)
| ~ ssNder1_5r1r1r1r1r1(X19355,X19349,X19347,X19346,X19352)
| ~ ssNder1_4r1r1r1r1(X19355,X19349,X19347,X19346)
| ~ ssNder1_3r1r1r1(X19355,X19349,X19347)
| ~ ssNder1_2r1r1(X19355,X19349)
| ~ ssNder1_1r1(X19355)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c983,c88]) ).
cnf(c1112,plain,
( ssPv16_5r1r1r1r1r1(X19364,X19361,X19362,X19359,X19363)
| ssPv19_2r1r1(X19364,X19361)
| ssPv20_1r1(X19364)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X19364,X19361,X19362,X19359,X19363,X19357,X19360,X19356,X19358)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X19364,X19361,X19362,X19359,X19363,X19357,X19360,X19356)
| ~ ssNder1_7r1r1r1r1r1r1r1(X19364,X19361,X19362,X19359,X19363,X19357,X19360)
| ~ ssNder1_6r1r1r1r1r1r1(X19364,X19361,X19362,X19359,X19363,X19357)
| ~ ssNder1_5r1r1r1r1r1(X19364,X19361,X19362,X19359,X19363)
| ~ ssNder1_4r1r1r1r1(X19364,X19361,X19362,X19359)
| ~ ssNder1_3r1r1r1(X19364,X19361,X19362)
| ~ ssNder1_2r1r1(X19364,X19361)
| ~ ssNder1_1r1(X19364)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1110,c76]) ).
cnf(c1113,plain,
( ssPv16_5r1r1r1r1r1(X19370,X19372,X19367,X19366,X19371)
| ssPv19_2r1r1(X19370,X19372)
| ssPv20_1r1(X19370)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X19370,X19372,X19367,X19366,X19371,X19365,X19368,X19369)
| ~ ssNder1_7r1r1r1r1r1r1r1(X19370,X19372,X19367,X19366,X19371,X19365,X19368)
| ~ ssNder1_6r1r1r1r1r1r1(X19370,X19372,X19367,X19366,X19371,X19365)
| ~ ssNder1_5r1r1r1r1r1(X19370,X19372,X19367,X19366,X19371)
| ~ ssNder1_4r1r1r1r1(X19370,X19372,X19367,X19366)
| ~ ssNder1_3r1r1r1(X19370,X19372,X19367)
| ~ ssNder1_2r1r1(X19370,X19372)
| ~ ssNder1_1r1(X19370)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1112,c66]) ).
cnf(c1114,plain,
( ssPv16_5r1r1r1r1r1(X19377,X19374,X19376,X19378,X19373)
| ssPv19_2r1r1(X19377,X19374)
| ssPv20_1r1(X19377)
| ~ ssNder1_7r1r1r1r1r1r1r1(X19377,X19374,X19376,X19378,X19373,X19379,X19375)
| ~ ssNder1_6r1r1r1r1r1r1(X19377,X19374,X19376,X19378,X19373,X19379)
| ~ ssNder1_5r1r1r1r1r1(X19377,X19374,X19376,X19378,X19373)
| ~ ssNder1_4r1r1r1r1(X19377,X19374,X19376,X19378)
| ~ ssNder1_3r1r1r1(X19377,X19374,X19376)
| ~ ssNder1_2r1r1(X19377,X19374)
| ~ ssNder1_1r1(X19377)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1113,c57]) ).
cnf(c1115,plain,
( ssPv16_5r1r1r1r1r1(X19382,X19383,X19385,X19384,X19380)
| ssPv19_2r1r1(X19382,X19383)
| ssPv20_1r1(X19382)
| ~ ssNder1_6r1r1r1r1r1r1(X19382,X19383,X19385,X19384,X19380,X19381)
| ~ ssNder1_5r1r1r1r1r1(X19382,X19383,X19385,X19384,X19380)
| ~ ssNder1_4r1r1r1r1(X19382,X19383,X19385,X19384)
| ~ ssNder1_3r1r1r1(X19382,X19383,X19385)
| ~ ssNder1_2r1r1(X19382,X19383)
| ~ ssNder1_1r1(X19382)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1114,c43]) ).
cnf(c1116,plain,
( ssPv16_5r1r1r1r1r1(X19417,X19420,X19416,X19418,X19419)
| ssPv19_2r1r1(X19417,X19420)
| ssPv20_1r1(X19417)
| ~ ssNder1_5r1r1r1r1r1(X19417,X19420,X19416,X19418,X19419)
| ~ ssNder1_4r1r1r1r1(X19417,X19420,X19416,X19418)
| ~ ssNder1_3r1r1r1(X19417,X19420,X19416)
| ~ ssNder1_2r1r1(X19417,X19420)
| ~ ssNder1_1r1(X19417)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1115,c30]) ).
cnf(c1118,plain,
( ssPv16_5r1r1r1r1r1(X19423,X19422,X19421,X19424,X19425)
| ssPv19_2r1r1(X19423,X19422)
| ssPv20_1r1(X19423)
| ~ ssNder1_4r1r1r1r1(X19423,X19422,X19421,X19424)
| ~ ssNder1_3r1r1r1(X19423,X19422,X19421)
| ~ ssNder1_2r1r1(X19423,X19422)
| ~ ssNder1_1r1(X19423)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1116,c19]) ).
cnf(c1119,plain,
( ssPv16_5r1r1r1r1r1(X19428,X19427,X19429,X19426,X19430)
| ssPv19_2r1r1(X19428,X19427)
| ssPv20_1r1(X19428)
| ~ ssNder1_3r1r1r1(X19428,X19427,X19429)
| ~ ssNder1_2r1r1(X19428,X19427)
| ~ ssNder1_1r1(X19428)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1118,c10]) ).
cnf(c1120,plain,
( ssPv16_5r1r1r1r1r1(X19432,X19434,X19431,X19435,X19433)
| ssPv19_2r1r1(X19432,X19434)
| ssPv20_1r1(X19432)
| ~ ssNder1_2r1r1(X19432,X19434)
| ~ ssNder1_1r1(X19432)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1119,c5]) ).
cnf(c1121,plain,
( ssPv16_5r1r1r1r1r1(X19437,X19439,X19438,X19436,X19440)
| ssPv19_2r1r1(X19437,X19439)
| ssPv20_1r1(X19437)
| ~ ssNder1_1r1(X19437)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1120,c2]) ).
cnf(c1122,plain,
( ssPv16_5r1r1r1r1r1(X19473,X19474,X19472,X19476,X19475)
| ssPv19_2r1r1(X19473,X19474)
| ssPv20_1r1(X19473)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1121,c0]) ).
cnf(c1123,plain,
( ssPv16_5r1r1r1r1r1(X19479,X19477,X19478,X19481,X19480)
| ssPv19_2r1r1(X19479,X19477)
| ssPv20_1r1(X19479) ),
inference(resolution,[status(thm)],[c1122,clause1]) ).
cnf(c1124,plain,
( ssPv19_2r1r1(X19484,X19482)
| ssPv20_1r1(X19484)
| ~ ssNder1_3r1r1r1(X19484,X19482,X19483)
| ~ ssNder1_2r1r1(X19484,X19482)
| ~ ssNder1_1r1(X19484)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1123,clause7]) ).
cnf(c1131,plain,
( ssPv19_2r1r1(X19485,X19486)
| ssPv20_1r1(X19485)
| ~ ssNder1_2r1r1(X19485,X19486)
| ~ ssNder1_1r1(X19485)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1124,c5]) ).
cnf(c1132,plain,
( ssPv19_2r1r1(X19488,X19487)
| ssPv20_1r1(X19488)
| ~ ssNder1_1r1(X19488)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1131,c2]) ).
cnf(c1133,plain,
( ssPv19_2r1r1(X19509,X19508)
| ssPv20_1r1(X19509)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1132,c0]) ).
cnf(c1135,plain,
( ssPv19_2r1r1(X19510,X19511)
| ssPv20_1r1(X19510) ),
inference(resolution,[status(thm)],[c1133,clause1]) ).
cnf(clause12,negated_conjecture,
( ~ ssNder1_5r1r1r1r1r1(X137,X139,X138,X141,X142)
| ~ ssNder1_4r1r1r1r1(X137,X139,X138,X141)
| ~ ssNder1_3r1r1r1(X137,X139,X138)
| ~ ssNder1_2r1r1(X137,X139)
| ~ ssNder1_1r1(X137)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X137,X139,X138,X141,X142,X140,skc26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(c25,plain,
( ~ ssNder1_4r1r1r1r1(X187,X186,X185,X188)
| ~ ssNder1_3r1r1r1(X187,X186,X185)
| ~ ssNder1_2r1r1(X187,X186)
| ~ ssNder1_1r1(X187)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X187,X186,X185,X188,X190,X189,skc26) ),
inference(resolution,[status(thm)],[clause12,c19]) ).
cnf(c31,plain,
( ~ ssNder1_3r1r1r1(X194,X193,X195)
| ~ ssNder1_2r1r1(X194,X193)
| ~ ssNder1_1r1(X194)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X194,X193,X195,X192,X196,X191,skc26) ),
inference(resolution,[status(thm)],[c25,c10]) ).
cnf(c32,plain,
( ~ ssNder1_2r1r1(X199,X200)
| ~ ssNder1_1r1(X199)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X199,X200,X197,X201,X202,X198,skc26) ),
inference(resolution,[status(thm)],[c31,c5]) ).
cnf(c33,plain,
( ~ ssNder1_1r1(X205)
| ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X205,X207,X204,X203,X208,X206,skc26) ),
inference(resolution,[status(thm)],[c32,c2]) ).
cnf(c34,plain,
( ~ ssNder1_0
| ssPv14_7r1r1r1r1r1r1r1(X216,X217,X219,X221,X220,X218,skc26) ),
inference(resolution,[status(thm)],[c33,c0]) ).
cnf(c36,plain,
ssPv14_7r1r1r1r1r1r1r1(X227,X223,X226,X224,X222,X225,skc26),
inference(resolution,[status(thm)],[c34,clause1]) ).
cnf(clause26,negated_conjecture,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X881,X885,X883,X887,X888,X886,X877,X880,X878,X876,X879,X884)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X881,X885,X883,X887,X888,X886,X877,X880,X878,X876,X879)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X881,X885,X883,X887,X888,X886,X877,X880,X878,X876)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X881,X885,X883,X887,X888,X886,X877,X880,X878)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X881,X885,X883,X887,X888,X886,X877,X880)
| ~ ssNder1_7r1r1r1r1r1r1r1(X881,X885,X883,X887,X888,X886,X877)
| ~ ssNder1_6r1r1r1r1r1r1(X881,X885,X883,X887,X888,X886)
| ~ ssNder1_5r1r1r1r1r1(X881,X885,X883,X887,X888)
| ~ ssNder1_4r1r1r1r1(X881,X885,X883,X887)
| ~ ssNder1_3r1r1r1(X881,X885,X883)
| ~ ssNder1_2r1r1(X881,X885)
| ~ ssNder1_1r1(X881)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X881,X885,X883,X887,X888,X886,X877,X880,X878,X876,X879,X884,X882,skc20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(c102,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1499,X1488,X1494,X1493,X1497,X1489,X1490,X1491,X1500,X1496,X1495)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1499,X1488,X1494,X1493,X1497,X1489,X1490,X1491,X1500,X1496)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1499,X1488,X1494,X1493,X1497,X1489,X1490,X1491,X1500)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1499,X1488,X1494,X1493,X1497,X1489,X1490,X1491)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1499,X1488,X1494,X1493,X1497,X1489,X1490)
| ~ ssNder1_6r1r1r1r1r1r1(X1499,X1488,X1494,X1493,X1497,X1489)
| ~ ssNder1_5r1r1r1r1r1(X1499,X1488,X1494,X1493,X1497)
| ~ ssNder1_4r1r1r1r1(X1499,X1488,X1494,X1493)
| ~ ssNder1_3r1r1r1(X1499,X1488,X1494)
| ~ ssNder1_2r1r1(X1499,X1488)
| ~ ssNder1_1r1(X1499)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1499,X1488,X1494,X1493,X1497,X1489,X1490,X1491,X1500,X1496,X1495,X1498,X1492,skc20) ),
inference(resolution,[status(thm)],[c101,clause26]) ).
cnf(c140,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1513,X1506,X1504,X1501,X1509,X1510,X1512,X1505,X1507,X1508)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1513,X1506,X1504,X1501,X1509,X1510,X1512,X1505,X1507)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1513,X1506,X1504,X1501,X1509,X1510,X1512,X1505)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1513,X1506,X1504,X1501,X1509,X1510,X1512)
| ~ ssNder1_6r1r1r1r1r1r1(X1513,X1506,X1504,X1501,X1509,X1510)
| ~ ssNder1_5r1r1r1r1r1(X1513,X1506,X1504,X1501,X1509)
| ~ ssNder1_4r1r1r1r1(X1513,X1506,X1504,X1501)
| ~ ssNder1_3r1r1r1(X1513,X1506,X1504)
| ~ ssNder1_2r1r1(X1513,X1506)
| ~ ssNder1_1r1(X1513)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1513,X1506,X1504,X1501,X1509,X1510,X1512,X1505,X1507,X1508,X1502,X1503,X1511,skc20) ),
inference(resolution,[status(thm)],[c102,c88]) ).
cnf(c141,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1526,X1520,X1521,X1518,X1524,X1516,X1519,X1514,X1517)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1526,X1520,X1521,X1518,X1524,X1516,X1519,X1514)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1526,X1520,X1521,X1518,X1524,X1516,X1519)
| ~ ssNder1_6r1r1r1r1r1r1(X1526,X1520,X1521,X1518,X1524,X1516)
| ~ ssNder1_5r1r1r1r1r1(X1526,X1520,X1521,X1518,X1524)
| ~ ssNder1_4r1r1r1r1(X1526,X1520,X1521,X1518)
| ~ ssNder1_3r1r1r1(X1526,X1520,X1521)
| ~ ssNder1_2r1r1(X1526,X1520)
| ~ ssNder1_1r1(X1526)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1526,X1520,X1521,X1518,X1524,X1516,X1519,X1514,X1517,X1522,X1523,X1515,X1525,skc20) ),
inference(resolution,[status(thm)],[c140,c76]) ).
cnf(c142,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X1536,X1539,X1532,X1531,X1538,X1530,X1533,X1534)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1536,X1539,X1532,X1531,X1538,X1530,X1533)
| ~ ssNder1_6r1r1r1r1r1r1(X1536,X1539,X1532,X1531,X1538,X1530)
| ~ ssNder1_5r1r1r1r1r1(X1536,X1539,X1532,X1531,X1538)
| ~ ssNder1_4r1r1r1r1(X1536,X1539,X1532,X1531)
| ~ ssNder1_3r1r1r1(X1536,X1539,X1532)
| ~ ssNder1_2r1r1(X1536,X1539)
| ~ ssNder1_1r1(X1536)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1536,X1539,X1532,X1531,X1538,X1530,X1533,X1534,X1528,X1529,X1535,X1537,X1527,skc20) ),
inference(resolution,[status(thm)],[c141,c66]) ).
cnf(c143,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X1563,X1556,X1560,X1564,X1554,X1566,X1559)
| ~ ssNder1_6r1r1r1r1r1r1(X1563,X1556,X1560,X1564,X1554,X1566)
| ~ ssNder1_5r1r1r1r1r1(X1563,X1556,X1560,X1564,X1554)
| ~ ssNder1_4r1r1r1r1(X1563,X1556,X1560,X1564)
| ~ ssNder1_3r1r1r1(X1563,X1556,X1560)
| ~ ssNder1_2r1r1(X1563,X1556)
| ~ ssNder1_1r1(X1563)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1563,X1556,X1560,X1564,X1554,X1566,X1559,X1557,X1562,X1565,X1555,X1561,X1558,skc20) ),
inference(resolution,[status(thm)],[c142,c57]) ).
cnf(c145,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X1575,X1576,X1579,X1577,X1568,X1571)
| ~ ssNder1_5r1r1r1r1r1(X1575,X1576,X1579,X1577,X1568)
| ~ ssNder1_4r1r1r1r1(X1575,X1576,X1579,X1577)
| ~ ssNder1_3r1r1r1(X1575,X1576,X1579)
| ~ ssNder1_2r1r1(X1575,X1576)
| ~ ssNder1_1r1(X1575)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1575,X1576,X1579,X1577,X1568,X1571,X1572,X1578,X1570,X1569,X1573,X1574,X1567,skc20) ),
inference(resolution,[status(thm)],[c143,c43]) ).
cnf(c146,plain,
( ~ ssNder1_5r1r1r1r1r1(X1586,X1592,X1582,X1587,X1589)
| ~ ssNder1_4r1r1r1r1(X1586,X1592,X1582,X1587)
| ~ ssNder1_3r1r1r1(X1586,X1592,X1582)
| ~ ssNder1_2r1r1(X1586,X1592)
| ~ ssNder1_1r1(X1586)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1586,X1592,X1582,X1587,X1589,X1581,X1588,X1590,X1580,X1591,X1584,X1585,X1583,skc20) ),
inference(resolution,[status(thm)],[c145,c30]) ).
cnf(c147,plain,
( ~ ssNder1_4r1r1r1r1(X1599,X1595,X1593,X1600)
| ~ ssNder1_3r1r1r1(X1599,X1595,X1593)
| ~ ssNder1_2r1r1(X1599,X1595)
| ~ ssNder1_1r1(X1599)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1599,X1595,X1593,X1600,X1603,X1605,X1602,X1596,X1601,X1594,X1598,X1597,X1604,skc20) ),
inference(resolution,[status(thm)],[c146,c19]) ).
cnf(c148,plain,
( ~ ssNder1_3r1r1r1(X1612,X1611,X1615)
| ~ ssNder1_2r1r1(X1612,X1611)
| ~ ssNder1_1r1(X1612)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1612,X1611,X1615,X1609,X1608,X1607,X1606,X1610,X1618,X1613,X1614,X1617,X1616,skc20) ),
inference(resolution,[status(thm)],[c147,c10]) ).
cnf(c149,plain,
( ~ ssNder1_2r1r1(X1641,X1642)
| ~ ssNder1_1r1(X1641)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1641,X1642,X1634,X1640,X1637,X1636,X1644,X1645,X1638,X1643,X1646,X1639,X1635,skc20) ),
inference(resolution,[status(thm)],[c148,c5]) ).
cnf(c150,plain,
( ~ ssNder1_1r1(X1650)
| ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1650,X1655,X1648,X1654,X1658,X1649,X1647,X1653,X1659,X1651,X1657,X1656,X1652,skc20) ),
inference(resolution,[status(thm)],[c149,c2]) ).
cnf(c151,plain,
( ~ ssNder1_0
| ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1664,X1660,X1669,X1670,X1672,X1666,X1671,X1663,X1661,X1662,X1668,X1667,X1665,skc20) ),
inference(resolution,[status(thm)],[c150,c0]) ).
cnf(c152,plain,
ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1681,X1676,X1673,X1674,X1679,X1678,X1680,X1682,X1675,X1684,X1685,X1683,X1677,skc20),
inference(resolution,[status(thm)],[c151,clause1]) ).
cnf(clause37,negated_conjecture,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709,X1699,X1702,X1700,X1698,X1701,X1707,X1705)
| ~ ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709,X1699,X1702,X1700,X1698,X1701,X1707,X1705,X1704)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709,X1699,X1702,X1700,X1698,X1701,X1707)
| ~ ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709,X1699,X1702,X1700,X1698,X1701)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709,X1699,X1702,X1700,X1698,X1701)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709,X1699,X1702,X1700,X1698)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709,X1699,X1702,X1700)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709,X1699,X1702)
| ~ ssPv14_7r1r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709,X1699)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709,X1699)
| ~ ssNder1_6r1r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711,X1709)
| ~ ssNder1_5r1r1r1r1r1(X1703,X1708,X1706,X1710,X1711)
| ~ ssNder1_4r1r1r1r1(X1703,X1708,X1706,X1710)
| ~ ssNder1_3r1r1r1(X1703,X1708,X1706)
| ~ ssPv19_2r1r1(X1703,X1708)
| ~ ssNder1_2r1r1(X1703,X1708)
| ~ ssNder1_1r1(X1703)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
cnf(c154,plain,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792,X3793,X3798,X3794,X3800,X3801,X3797,X3803,X3802)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792,X3793,X3798,X3794,X3800,X3801,X3797,X3803)
| ~ ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792,X3793,X3798,X3794,X3800,X3801,X3797)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792,X3793,X3798,X3794,X3800,X3801,X3797)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792,X3793,X3798,X3794,X3800,X3801)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792,X3793,X3798,X3794,X3800)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792,X3793,X3798,X3794)
| ~ ssPv14_7r1r1r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792,X3793,X3798)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792,X3793,X3798)
| ~ ssNder1_6r1r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792,X3793)
| ~ ssNder1_5r1r1r1r1r1(X3796,X3791,X3795,X3799,X3792)
| ~ ssNder1_4r1r1r1r1(X3796,X3791,X3795,X3799)
| ~ ssNder1_3r1r1r1(X3796,X3791,X3795)
| ~ ssPv19_2r1r1(X3796,X3791)
| ~ ssNder1_2r1r1(X3796,X3791)
| ~ ssNder1_1r1(X3796)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[clause37,c152]) ).
cnf(c279,plain,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X5795,X5799,X5797,X5798,X5803,X5793,X5796,X5802,X5800,X5794,X5804,X5801)
| ~ ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X5795,X5799,X5797,X5798,X5803,X5793,X5796,X5802,X5800,X5794,X5804)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5795,X5799,X5797,X5798,X5803,X5793,X5796,X5802,X5800,X5794,X5804)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5795,X5799,X5797,X5798,X5803,X5793,X5796,X5802,X5800,X5794)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5795,X5799,X5797,X5798,X5803,X5793,X5796,X5802,X5800)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5795,X5799,X5797,X5798,X5803,X5793,X5796,X5802)
| ~ ssPv14_7r1r1r1r1r1r1r1(X5795,X5799,X5797,X5798,X5803,X5793,X5796)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5795,X5799,X5797,X5798,X5803,X5793,X5796)
| ~ ssNder1_6r1r1r1r1r1r1(X5795,X5799,X5797,X5798,X5803,X5793)
| ~ ssNder1_5r1r1r1r1r1(X5795,X5799,X5797,X5798,X5803)
| ~ ssNder1_4r1r1r1r1(X5795,X5799,X5797,X5798)
| ~ ssNder1_3r1r1r1(X5795,X5799,X5797)
| ~ ssPv19_2r1r1(X5795,X5799)
| ~ ssNder1_2r1r1(X5795,X5799)
| ~ ssNder1_1r1(X5795)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c154,c136]) ).
cnf(c397,plain,
( ~ ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X5924,X5922,X5931,X5930,X5923,X5926,X5928,X5927,X5929,X5932,X5925)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5924,X5922,X5931,X5930,X5923,X5926,X5928,X5927,X5929,X5932,X5925)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5924,X5922,X5931,X5930,X5923,X5926,X5928,X5927,X5929,X5932)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5924,X5922,X5931,X5930,X5923,X5926,X5928,X5927,X5929)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5924,X5922,X5931,X5930,X5923,X5926,X5928,X5927)
| ~ ssPv14_7r1r1r1r1r1r1r1(X5924,X5922,X5931,X5930,X5923,X5926,X5928)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5924,X5922,X5931,X5930,X5923,X5926,X5928)
| ~ ssNder1_6r1r1r1r1r1r1(X5924,X5922,X5931,X5930,X5923,X5926)
| ~ ssNder1_5r1r1r1r1r1(X5924,X5922,X5931,X5930,X5923)
| ~ ssNder1_4r1r1r1r1(X5924,X5922,X5931,X5930)
| ~ ssNder1_3r1r1r1(X5924,X5922,X5931)
| ~ ssPv19_2r1r1(X5924,X5922)
| ~ ssNder1_2r1r1(X5924,X5922)
| ~ ssNder1_1r1(X5924)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c279,c101]) ).
cnf(c405,plain,
( ~ ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X5943,X5937,X5935,X5933,X5940,X5941,X5942,X5936,X5938,X5939,X5934)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5943,X5937,X5935,X5933,X5940,X5941,X5942,X5936,X5938,X5939)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5943,X5937,X5935,X5933,X5940,X5941,X5942,X5936,X5938)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5943,X5937,X5935,X5933,X5940,X5941,X5942,X5936)
| ~ ssPv14_7r1r1r1r1r1r1r1(X5943,X5937,X5935,X5933,X5940,X5941,X5942)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5943,X5937,X5935,X5933,X5940,X5941,X5942)
| ~ ssNder1_6r1r1r1r1r1r1(X5943,X5937,X5935,X5933,X5940,X5941)
| ~ ssNder1_5r1r1r1r1r1(X5943,X5937,X5935,X5933,X5940)
| ~ ssNder1_4r1r1r1r1(X5943,X5937,X5935,X5933)
| ~ ssNder1_3r1r1r1(X5943,X5937,X5935)
| ~ ssPv19_2r1r1(X5943,X5937)
| ~ ssNder1_2r1r1(X5943,X5937)
| ~ ssNder1_1r1(X5943)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c397,c88]) ).
cnf(clause15,negated_conjecture,
( ~ ssNder1_6r1r1r1r1r1r1(X250,X252,X251,X254,X255,X253)
| ~ ssNder1_5r1r1r1r1r1(X250,X252,X251,X254,X255)
| ~ ssNder1_4r1r1r1r1(X250,X252,X251,X254)
| ~ ssNder1_3r1r1r1(X250,X252,X251)
| ~ ssNder1_2r1r1(X250,X252)
| ~ ssNder1_1r1(X250)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X250,X252,X251,X254,X255,X253,X249,skc24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c40,plain,
( ~ ssNder1_5r1r1r1r1r1(X287,X290,X285,X288,X289)
| ~ ssNder1_4r1r1r1r1(X287,X290,X285,X288)
| ~ ssNder1_3r1r1r1(X287,X290,X285)
| ~ ssNder1_2r1r1(X287,X290)
| ~ ssNder1_1r1(X287)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X287,X290,X285,X288,X289,X284,X286,skc24) ),
inference(resolution,[status(thm)],[clause15,c30]) ).
cnf(c44,plain,
( ~ ssNder1_4r1r1r1r1(X301,X299,X298,X302)
| ~ ssNder1_3r1r1r1(X301,X299,X298)
| ~ ssNder1_2r1r1(X301,X299)
| ~ ssNder1_1r1(X301)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X301,X299,X298,X302,X304,X303,X300,skc24) ),
inference(resolution,[status(thm)],[c40,c19]) ).
cnf(c45,plain,
( ~ ssNder1_3r1r1r1(X309,X307,X310)
| ~ ssNder1_2r1r1(X309,X307)
| ~ ssNder1_1r1(X309)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X309,X307,X310,X305,X306,X311,X308,skc24) ),
inference(resolution,[status(thm)],[c44,c10]) ).
cnf(c46,plain,
( ~ ssNder1_2r1r1(X316,X318)
| ~ ssNder1_1r1(X316)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X316,X318,X312,X315,X314,X313,X317,skc24) ),
inference(resolution,[status(thm)],[c45,c5]) ).
cnf(c47,plain,
( ~ ssNder1_1r1(X320)
| ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X320,X322,X321,X325,X319,X324,X323,skc24) ),
inference(resolution,[status(thm)],[c46,c2]) ).
cnf(c48,plain,
( ~ ssNder1_0
| ssPv13_8r1r1r1r1r1r1r1r1(X328,X332,X330,X331,X326,X329,X327,skc24) ),
inference(resolution,[status(thm)],[c47,c0]) ).
cnf(c49,plain,
ssPv13_8r1r1r1r1r1r1r1r1(X346,X342,X343,X344,X345,X341,X347,skc24),
inference(resolution,[status(thm)],[c48,clause1]) ).
cnf(clause24,negated_conjecture,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X741,X743,X742,X745,X746,X744,X737,X740,X738,X736)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X741,X743,X742,X745,X746,X744,X737,X740,X738)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X741,X743,X742,X745,X746,X744,X737,X740)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X741,X743,X742,X745,X746,X744,X737,X740)
| ~ ssNder1_7r1r1r1r1r1r1r1(X741,X743,X742,X745,X746,X744,X737)
| ~ ssNder1_6r1r1r1r1r1r1(X741,X743,X742,X745,X746,X744)
| ~ ssNder1_5r1r1r1r1r1(X741,X743,X742,X745,X746)
| ~ ssNder1_4r1r1r1r1(X741,X743,X742,X745)
| ~ ssNder1_3r1r1r1(X741,X743,X742)
| ~ ssPv19_2r1r1(X741,X743)
| ~ ssNder1_2r1r1(X741,X743)
| ~ ssNder1_1r1(X741)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X741,X743,X742,X745,X746,X744,X737,X740,X738,X736,X739)
| ssPv16_5r1r1r1r1r1(X741,X743,X742,X745,X746) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(c85,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1154,X1149,X1150,X1147,X1152,X1145,X1148,X1144,X1146)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X1154,X1149,X1150,X1147,X1152,X1145,X1148,X1144)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1154,X1149,X1150,X1147,X1152,X1145,X1148,X1144)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1154,X1149,X1150,X1147,X1152,X1145,X1148)
| ~ ssNder1_6r1r1r1r1r1r1(X1154,X1149,X1150,X1147,X1152,X1145)
| ~ ssNder1_5r1r1r1r1r1(X1154,X1149,X1150,X1147,X1152)
| ~ ssNder1_4r1r1r1r1(X1154,X1149,X1150,X1147)
| ~ ssNder1_3r1r1r1(X1154,X1149,X1150)
| ~ ssPv19_2r1r1(X1154,X1149)
| ~ ssNder1_2r1r1(X1154,X1149)
| ~ ssNder1_1r1(X1154)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1154,X1149,X1150,X1147,X1152,X1145,X1148,X1144,X1146,X1151,X1153)
| ssPv16_5r1r1r1r1r1(X1154,X1149,X1150,X1147,X1152) ),
inference(resolution,[status(thm)],[clause24,c76]) ).
cnf(c116,plain,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X1162,X1165,X1158,X1157,X1163,X1156,X1160,X1161)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1162,X1165,X1158,X1157,X1163,X1156,X1160,X1161)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1162,X1165,X1158,X1157,X1163,X1156,X1160)
| ~ ssNder1_6r1r1r1r1r1r1(X1162,X1165,X1158,X1157,X1163,X1156)
| ~ ssNder1_5r1r1r1r1r1(X1162,X1165,X1158,X1157,X1163)
| ~ ssNder1_4r1r1r1r1(X1162,X1165,X1158,X1157)
| ~ ssNder1_3r1r1r1(X1162,X1165,X1158)
| ~ ssPv19_2r1r1(X1162,X1165)
| ~ ssNder1_2r1r1(X1162,X1165)
| ~ ssNder1_1r1(X1162)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1162,X1165,X1158,X1157,X1163,X1156,X1160,X1161,X1155,X1159,X1164)
| ssPv16_5r1r1r1r1r1(X1162,X1165,X1158,X1157,X1163) ),
inference(resolution,[status(thm)],[c85,c66]) ).
cnf(c117,plain,
( ~ ssPv13_8r1r1r1r1r1r1r1r1(X1187,X1181,X1186,X1189,X1180,X1190,X1184,X1182)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1187,X1181,X1186,X1189,X1180,X1190,X1184)
| ~ ssNder1_6r1r1r1r1r1r1(X1187,X1181,X1186,X1189,X1180,X1190)
| ~ ssNder1_5r1r1r1r1r1(X1187,X1181,X1186,X1189,X1180)
| ~ ssNder1_4r1r1r1r1(X1187,X1181,X1186,X1189)
| ~ ssNder1_3r1r1r1(X1187,X1181,X1186)
| ~ ssPv19_2r1r1(X1187,X1181)
| ~ ssNder1_2r1r1(X1187,X1181)
| ~ ssNder1_1r1(X1187)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1187,X1181,X1186,X1189,X1180,X1190,X1184,X1182,X1183,X1185,X1188)
| ssPv16_5r1r1r1r1r1(X1187,X1181,X1186,X1189,X1180) ),
inference(resolution,[status(thm)],[c116,c57]) ).
cnf(c118,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X1194,X1192,X1197,X1193,X1199,X1200,X1195)
| ~ ssNder1_6r1r1r1r1r1r1(X1194,X1192,X1197,X1193,X1199,X1200)
| ~ ssNder1_5r1r1r1r1r1(X1194,X1192,X1197,X1193,X1199)
| ~ ssNder1_4r1r1r1r1(X1194,X1192,X1197,X1193)
| ~ ssNder1_3r1r1r1(X1194,X1192,X1197)
| ~ ssPv19_2r1r1(X1194,X1192)
| ~ ssNder1_2r1r1(X1194,X1192)
| ~ ssNder1_1r1(X1194)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1194,X1192,X1197,X1193,X1199,X1200,X1195,skc24,X1191,X1196,X1198)
| ssPv16_5r1r1r1r1r1(X1194,X1192,X1197,X1193,X1199) ),
inference(resolution,[status(thm)],[c117,c49]) ).
cnf(c119,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X1206,X1207,X1209,X1208,X1201,X1202)
| ~ ssNder1_5r1r1r1r1r1(X1206,X1207,X1209,X1208,X1201)
| ~ ssNder1_4r1r1r1r1(X1206,X1207,X1209,X1208)
| ~ ssNder1_3r1r1r1(X1206,X1207,X1209)
| ~ ssPv19_2r1r1(X1206,X1207)
| ~ ssNder1_2r1r1(X1206,X1207)
| ~ ssNder1_1r1(X1206)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1206,X1207,X1209,X1208,X1201,X1202,X1203,skc24,X1204,X1205,X1210)
| ssPv16_5r1r1r1r1r1(X1206,X1207,X1209,X1208,X1201) ),
inference(resolution,[status(thm)],[c118,c43]) ).
cnf(c120,plain,
( ~ ssNder1_5r1r1r1r1r1(X1217,X1220,X1212,X1218,X1219)
| ~ ssNder1_4r1r1r1r1(X1217,X1220,X1212,X1218)
| ~ ssNder1_3r1r1r1(X1217,X1220,X1212)
| ~ ssPv19_2r1r1(X1217,X1220)
| ~ ssNder1_2r1r1(X1217,X1220)
| ~ ssNder1_1r1(X1217)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1217,X1220,X1212,X1218,X1219,X1211,X1213,skc24,X1214,X1215,X1216)
| ssPv16_5r1r1r1r1r1(X1217,X1220,X1212,X1218,X1219) ),
inference(resolution,[status(thm)],[c119,c30]) ).
cnf(c121,plain,
( ~ ssNder1_4r1r1r1r1(X1226,X1225,X1223,X1228)
| ~ ssNder1_3r1r1r1(X1226,X1225,X1223)
| ~ ssPv19_2r1r1(X1226,X1225)
| ~ ssNder1_2r1r1(X1226,X1225)
| ~ ssNder1_1r1(X1226)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1226,X1225,X1223,X1228,X1229,X1222,X1224,skc24,X1221,X1230,X1227)
| ssPv16_5r1r1r1r1r1(X1226,X1225,X1223,X1228,X1229) ),
inference(resolution,[status(thm)],[c120,c19]) ).
cnf(c122,plain,
( ~ ssNder1_3r1r1r1(X1252,X1251,X1253)
| ~ ssPv19_2r1r1(X1252,X1251)
| ~ ssNder1_2r1r1(X1252,X1251)
| ~ ssNder1_1r1(X1252)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1252,X1251,X1253,X1248,X1250,X1247,X1254,skc24,X1245,X1246,X1249)
| ssPv16_5r1r1r1r1r1(X1252,X1251,X1253,X1248,X1250) ),
inference(resolution,[status(thm)],[c121,c10]) ).
cnf(c123,plain,
( ~ ssPv19_2r1r1(X1259,X1263)
| ~ ssNder1_2r1r1(X1259,X1263)
| ~ ssNder1_1r1(X1259)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1259,X1263,X1255,X1258,X1256,X1264,X1260,skc24,X1262,X1261,X1257)
| ssPv16_5r1r1r1r1r1(X1259,X1263,X1255,X1258,X1256) ),
inference(resolution,[status(thm)],[c122,c5]) ).
cnf(c124,plain,
( ~ ssPv19_2r1r1(X1269,X1271)
| ~ ssNder1_1r1(X1269)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X1269,X1271,X1274,X1266,X1273,X1268,X1265,skc24,X1272,X1270,X1267)
| ssPv16_5r1r1r1r1r1(X1269,X1271,X1274,X1266,X1273) ),
inference(resolution,[status(thm)],[c123,c2]) ).
cnf(c1139,plain,
( ssPv20_1r1(X19521)
| ~ ssNder1_1r1(X19521)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X19521,X19520,X19519,X19514,X19516,X19518,X19515,skc24,X19517,X19512,X19513)
| ssPv16_5r1r1r1r1r1(X19521,X19520,X19519,X19514,X19516) ),
inference(resolution,[status(thm)],[c1135,c124]) ).
cnf(c1142,plain,
( ssPv20_1r1(X19522)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X19522,X19531,X19528,X19524,X19526,X19525,X19527,skc24,X19529,X19530,X19523)
| ssPv16_5r1r1r1r1r1(X19522,X19531,X19528,X19524,X19526) ),
inference(resolution,[status(thm)],[c1139,c0]) ).
cnf(c1143,plain,
( ssPv20_1r1(X19539)
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X19539,X19540,X19533,X19538,X19536,X19537,X19534,skc24,X19541,X19532,X19535)
| ssPv16_5r1r1r1r1r1(X19539,X19540,X19533,X19538,X19536) ),
inference(resolution,[status(thm)],[c1142,clause1]) ).
cnf(c1145,plain,
( ssPv20_1r1(X27923)
| ssPv16_5r1r1r1r1r1(X27923,X27917,X27924,X27921,X27925)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X27923,X27917,X27924,X27921,X27925,X27919,X27918,skc24,X27920,X27922)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X27923,X27917,X27924,X27921,X27925,X27919,X27918,skc24,X27920)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X27923,X27917,X27924,X27921,X27925,X27919,X27918,skc24)
| ~ ssPv14_7r1r1r1r1r1r1r1(X27923,X27917,X27924,X27921,X27925,X27919,X27918)
| ~ ssNder1_7r1r1r1r1r1r1r1(X27923,X27917,X27924,X27921,X27925,X27919,X27918)
| ~ ssNder1_6r1r1r1r1r1r1(X27923,X27917,X27924,X27921,X27925,X27919)
| ~ ssNder1_5r1r1r1r1r1(X27923,X27917,X27924,X27921,X27925)
| ~ ssNder1_4r1r1r1r1(X27923,X27917,X27924,X27921)
| ~ ssNder1_3r1r1r1(X27923,X27917,X27924)
| ~ ssPv19_2r1r1(X27923,X27917)
| ~ ssNder1_2r1r1(X27923,X27917)
| ~ ssNder1_1r1(X27923)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1143,c405]) ).
cnf(c1499,plain,
( ssPv20_1r1(X27933)
| ssPv16_5r1r1r1r1r1(X27933,X27930,X27931,X27928,X27932)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X27933,X27930,X27931,X27928,X27932,X27926,X27929,skc24,X27927)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X27933,X27930,X27931,X27928,X27932,X27926,X27929,skc24)
| ~ ssPv14_7r1r1r1r1r1r1r1(X27933,X27930,X27931,X27928,X27932,X27926,X27929)
| ~ ssNder1_7r1r1r1r1r1r1r1(X27933,X27930,X27931,X27928,X27932,X27926,X27929)
| ~ ssNder1_6r1r1r1r1r1r1(X27933,X27930,X27931,X27928,X27932,X27926)
| ~ ssNder1_5r1r1r1r1r1(X27933,X27930,X27931,X27928,X27932)
| ~ ssNder1_4r1r1r1r1(X27933,X27930,X27931,X27928)
| ~ ssNder1_3r1r1r1(X27933,X27930,X27931)
| ~ ssPv19_2r1r1(X27933,X27930)
| ~ ssNder1_2r1r1(X27933,X27930)
| ~ ssNder1_1r1(X27933)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1145,c76]) ).
cnf(c1500,plain,
( ssPv20_1r1(X27938)
| ssPv16_5r1r1r1r1r1(X27938,X27940,X27936,X27935,X27939)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X27938,X27940,X27936,X27935,X27939,X27934,X27937,skc24)
| ~ ssPv14_7r1r1r1r1r1r1r1(X27938,X27940,X27936,X27935,X27939,X27934,X27937)
| ~ ssNder1_7r1r1r1r1r1r1r1(X27938,X27940,X27936,X27935,X27939,X27934,X27937)
| ~ ssNder1_6r1r1r1r1r1r1(X27938,X27940,X27936,X27935,X27939,X27934)
| ~ ssNder1_5r1r1r1r1r1(X27938,X27940,X27936,X27935,X27939)
| ~ ssNder1_4r1r1r1r1(X27938,X27940,X27936,X27935)
| ~ ssNder1_3r1r1r1(X27938,X27940,X27936)
| ~ ssPv19_2r1r1(X27938,X27940)
| ~ ssNder1_2r1r1(X27938,X27940)
| ~ ssNder1_1r1(X27938)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1499,c66]) ).
cnf(c1501,plain,
( ssPv20_1r1(X27945)
| ssPv16_5r1r1r1r1r1(X27945,X27942,X27944,X27946,X27941)
| ~ ssPv14_7r1r1r1r1r1r1r1(X27945,X27942,X27944,X27946,X27941,X27947,X27943)
| ~ ssNder1_7r1r1r1r1r1r1r1(X27945,X27942,X27944,X27946,X27941,X27947,X27943)
| ~ ssNder1_6r1r1r1r1r1r1(X27945,X27942,X27944,X27946,X27941,X27947)
| ~ ssNder1_5r1r1r1r1r1(X27945,X27942,X27944,X27946,X27941)
| ~ ssNder1_4r1r1r1r1(X27945,X27942,X27944,X27946)
| ~ ssNder1_3r1r1r1(X27945,X27942,X27944)
| ~ ssPv19_2r1r1(X27945,X27942)
| ~ ssNder1_2r1r1(X27945,X27942)
| ~ ssNder1_1r1(X27945)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1500,c57]) ).
cnf(c1502,plain,
( ssPv20_1r1(X27951)
| ssPv16_5r1r1r1r1r1(X27951,X27952,X27954,X27953,X27948)
| ~ ssPv14_7r1r1r1r1r1r1r1(X27951,X27952,X27954,X27953,X27948,X27949,X27950)
| ~ ssNder1_6r1r1r1r1r1r1(X27951,X27952,X27954,X27953,X27948,X27949)
| ~ ssNder1_5r1r1r1r1r1(X27951,X27952,X27954,X27953,X27948)
| ~ ssNder1_4r1r1r1r1(X27951,X27952,X27954,X27953)
| ~ ssNder1_3r1r1r1(X27951,X27952,X27954)
| ~ ssPv19_2r1r1(X27951,X27952)
| ~ ssNder1_2r1r1(X27951,X27952)
| ~ ssNder1_1r1(X27951)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1501,c43]) ).
cnf(c1503,plain,
( ssPv20_1r1(X27993)
| ssPv16_5r1r1r1r1r1(X27993,X27996,X27997,X27992,X27994)
| ~ ssNder1_6r1r1r1r1r1r1(X27993,X27996,X27997,X27992,X27994,X27995)
| ~ ssNder1_5r1r1r1r1r1(X27993,X27996,X27997,X27992,X27994)
| ~ ssNder1_4r1r1r1r1(X27993,X27996,X27997,X27992)
| ~ ssNder1_3r1r1r1(X27993,X27996,X27997)
| ~ ssPv19_2r1r1(X27993,X27996)
| ~ ssNder1_2r1r1(X27993,X27996)
| ~ ssNder1_1r1(X27993)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1502,c36]) ).
cnf(c1504,plain,
( ssPv20_1r1(X27999)
| ssPv16_5r1r1r1r1r1(X27999,X28002,X27998,X28000,X28001)
| ~ ssNder1_5r1r1r1r1r1(X27999,X28002,X27998,X28000,X28001)
| ~ ssNder1_4r1r1r1r1(X27999,X28002,X27998,X28000)
| ~ ssNder1_3r1r1r1(X27999,X28002,X27998)
| ~ ssPv19_2r1r1(X27999,X28002)
| ~ ssNder1_2r1r1(X27999,X28002)
| ~ ssNder1_1r1(X27999)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1503,c30]) ).
cnf(c1505,plain,
( ssPv20_1r1(X28005)
| ssPv16_5r1r1r1r1r1(X28005,X28004,X28003,X28006,X28007)
| ~ ssNder1_4r1r1r1r1(X28005,X28004,X28003,X28006)
| ~ ssNder1_3r1r1r1(X28005,X28004,X28003)
| ~ ssPv19_2r1r1(X28005,X28004)
| ~ ssNder1_2r1r1(X28005,X28004)
| ~ ssNder1_1r1(X28005)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1504,c19]) ).
cnf(c1506,plain,
( ssPv20_1r1(X28010)
| ssPv16_5r1r1r1r1r1(X28010,X28009,X28012,X28008,X28011)
| ~ ssNder1_3r1r1r1(X28010,X28009,X28012)
| ~ ssPv19_2r1r1(X28010,X28009)
| ~ ssNder1_2r1r1(X28010,X28009)
| ~ ssNder1_1r1(X28010)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1505,c10]) ).
cnf(c1507,plain,
( ssPv20_1r1(X28015)
| ssPv16_5r1r1r1r1r1(X28015,X28017,X28013,X28014,X28016)
| ~ ssPv19_2r1r1(X28015,X28017)
| ~ ssNder1_2r1r1(X28015,X28017)
| ~ ssNder1_1r1(X28015)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1506,c5]) ).
cnf(c1508,plain,
( ssPv20_1r1(X28054)
| ssPv16_5r1r1r1r1r1(X28054,X28055,X28053,X28056,X28052)
| ~ ssPv19_2r1r1(X28054,X28055)
| ~ ssNder1_1r1(X28054)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1507,c2]) ).
cnf(c1515,plain,
( ssPv20_1r1(X28059)
| ssPv16_5r1r1r1r1r1(X28059,X28057,X28060,X28061,X28058)
| ~ ssNder1_1r1(X28059)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1508,c1135]) ).
cnf(c1518,plain,
( ssPv20_1r1(X28063)
| ssPv16_5r1r1r1r1r1(X28063,X28066,X28064,X28062,X28065)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1515,c0]) ).
cnf(c1519,plain,
( ssPv20_1r1(X28071)
| ssPv16_5r1r1r1r1r1(X28071,X28070,X28068,X28069,X28067) ),
inference(resolution,[status(thm)],[c1518,clause1]) ).
cnf(c1521,plain,
( ssPv20_1r1(X28074)
| ~ ssNder1_3r1r1r1(X28074,X28072,X28073)
| ~ ssNder1_2r1r1(X28074,X28072)
| ~ ssNder1_1r1(X28074)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1519,clause7]) ).
cnf(c1522,plain,
( ssPv20_1r1(X28109)
| ~ ssNder1_2r1r1(X28109,X28110)
| ~ ssNder1_1r1(X28109)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1521,c5]) ).
cnf(c1524,plain,
( ssPv20_1r1(X28111)
| ~ ssNder1_1r1(X28111)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1522,c2]) ).
cnf(c1525,plain,
( ssPv20_1r1(X28112)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1524,c0]) ).
cnf(c1526,plain,
ssPv20_1r1(X28113),
inference(resolution,[status(thm)],[c1525,clause1]) ).
cnf(clause38,negated_conjecture,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782,X1772,X1775,X1773,X1771,X1774,X1780,X1778)
| ~ ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782,X1772,X1775,X1773,X1771,X1774,X1780,X1778,X1777)
| ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782,X1772,X1775,X1773,X1771,X1774,X1780)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782,X1772,X1775,X1773,X1771,X1774,X1780)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782,X1772,X1775,X1773,X1771,X1774)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782,X1772,X1775,X1773,X1771)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782,X1772,X1775,X1773)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782,X1772,X1775)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782,X1772,X1775)
| ~ ssNder1_7r1r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782,X1772)
| ~ ssNder1_6r1r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784,X1782)
| ~ ssNder1_5r1r1r1r1r1(X1776,X1781,X1779,X1783,X1784)
| ~ ssNder1_4r1r1r1r1(X1776,X1781,X1779,X1783)
| ~ ssNder1_3r1r1r1(X1776,X1781,X1779)
| ~ ssNder1_2r1r1(X1776,X1781)
| ~ ssPv20_1r1(X1776)
| ~ ssNder1_1r1(X1776)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(c160,plain,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870,X3871,X3876,X3872,X3878,X3879,X3875,X3881,X3880)
| ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870,X3871,X3876,X3872,X3878,X3879,X3875,X3881)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870,X3871,X3876,X3872,X3878,X3879,X3875,X3881)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870,X3871,X3876,X3872,X3878,X3879,X3875)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870,X3871,X3876,X3872,X3878,X3879)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870,X3871,X3876,X3872,X3878)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870,X3871,X3876,X3872)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870,X3871,X3876,X3872)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870,X3871,X3876)
| ~ ssNder1_6r1r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870,X3871)
| ~ ssNder1_5r1r1r1r1r1(X3874,X3869,X3873,X3877,X3870)
| ~ ssNder1_4r1r1r1r1(X3874,X3869,X3873,X3877)
| ~ ssNder1_3r1r1r1(X3874,X3869,X3873)
| ~ ssNder1_2r1r1(X3874,X3869)
| ~ ssPv20_1r1(X3874)
| ~ ssNder1_1r1(X3874)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[clause38,c152]) ).
cnf(c285,plain,
( ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X5882,X5886,X5884,X5885,X5890,X5880,X5883,X5889,X5887,X5881,X5891,X5888)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X5882,X5886,X5884,X5885,X5890,X5880,X5883,X5889,X5887,X5881,X5891,X5888)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5882,X5886,X5884,X5885,X5890,X5880,X5883,X5889,X5887,X5881,X5891)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5882,X5886,X5884,X5885,X5890,X5880,X5883,X5889,X5887,X5881)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5882,X5886,X5884,X5885,X5890,X5880,X5883,X5889,X5887)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X5882,X5886,X5884,X5885,X5890,X5880,X5883,X5889)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5882,X5886,X5884,X5885,X5890,X5880,X5883,X5889)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5882,X5886,X5884,X5885,X5890,X5880,X5883)
| ~ ssNder1_6r1r1r1r1r1r1(X5882,X5886,X5884,X5885,X5890,X5880)
| ~ ssNder1_5r1r1r1r1r1(X5882,X5886,X5884,X5885,X5890)
| ~ ssNder1_4r1r1r1r1(X5882,X5886,X5884,X5885)
| ~ ssNder1_3r1r1r1(X5882,X5886,X5884)
| ~ ssNder1_2r1r1(X5882,X5886)
| ~ ssPv20_1r1(X5882)
| ~ ssNder1_1r1(X5882)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c160,c136]) ).
cnf(c403,plain,
( ~ ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X5946,X5944,X5953,X5952,X5945,X5948,X5950,X5949,X5951,X5955,X5947,X5954)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5946,X5944,X5953,X5952,X5945,X5948,X5950,X5949,X5951,X5955,X5947)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5946,X5944,X5953,X5952,X5945,X5948,X5950,X5949,X5951,X5955)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5946,X5944,X5953,X5952,X5945,X5948,X5950,X5949,X5951)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X5946,X5944,X5953,X5952,X5945,X5948,X5950,X5949)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5946,X5944,X5953,X5952,X5945,X5948,X5950,X5949)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5946,X5944,X5953,X5952,X5945,X5948,X5950)
| ~ ssNder1_6r1r1r1r1r1r1(X5946,X5944,X5953,X5952,X5945,X5948)
| ~ ssNder1_5r1r1r1r1r1(X5946,X5944,X5953,X5952,X5945)
| ~ ssNder1_4r1r1r1r1(X5946,X5944,X5953,X5952)
| ~ ssNder1_3r1r1r1(X5946,X5944,X5953)
| ~ ssNder1_2r1r1(X5946,X5944)
| ~ ssPv20_1r1(X5946)
| ~ ssNder1_1r1(X5946)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c285,c101]) ).
cnf(clause23,negated_conjecture,
( ~ ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X674,X677,X675,X679,X680,X678,X670,X673,X671,X669,X672,X676,skc23)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X674,X677,X675,X679,X680,X678,X670,X673,X671,X669,X672)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X674,X677,X675,X679,X680,X678,X670,X673,X671,X669)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X674,X677,X675,X679,X680,X678,X670,X673,X671)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X674,X677,X675,X679,X680,X678,X670,X673)
| ~ ssNder1_7r1r1r1r1r1r1r1(X674,X677,X675,X679,X680,X678,X670)
| ~ ssNder1_6r1r1r1r1r1r1(X674,X677,X675,X679,X680,X678)
| ~ ssNder1_5r1r1r1r1r1(X674,X677,X675,X679,X680)
| ~ ssNder1_4r1r1r1r1(X674,X677,X675,X679)
| ~ ssNder1_3r1r1r1(X674,X677,X675)
| ~ ssNder1_2r1r1(X674,X677)
| ~ ssNder1_1r1(X674)
| ~ ssNder1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
cnf(clause43,negated_conjecture,
( ~ ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144,X2147,X2145,X2143,X2146,X2152,X2150,X2149)
| ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144,X2147,X2145,X2143,X2146,X2152,X2150)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144,X2147,X2145,X2143,X2146,X2152)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144,X2147,X2145,X2143,X2146)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144,X2147,X2145,X2143)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144,X2147,X2145)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144,X2147)
| ~ ssNder1_7r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144)
| ~ ssNder1_6r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155)
| ~ ssNder1_5r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157)
| ~ ssNder1_4r1r1r1r1(X2148,X2154,X2151,X2156)
| ~ ssNder1_3r1r1r1(X2148,X2154,X2151)
| ~ ssNder1_2r1r1(X2148,X2154)
| ~ ssNder1_1r1(X2148)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144,X2147,X2145,X2143,X2146,X2152,X2150,X2149,X2153)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144,X2147,X2145,X2143,X2146,X2152,X2150)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X2148,X2154,X2151,X2156,X2157,X2155,X2144,X2147,X2145,X2143,X2146,X2152)
| ssPv19_2r1r1(X2148,X2154) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
cnf(c195,plain,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953,X3952,X3959,X3960,X3957,X3958,X3955,X3963)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953,X3952,X3959,X3960,X3957,X3958,X3955)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953,X3952,X3959,X3960,X3957,X3958)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953,X3952,X3959,X3960,X3957)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953,X3952,X3959,X3960)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953,X3952,X3959)
| ~ ssNder1_7r1r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953,X3952)
| ~ ssNder1_6r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953)
| ~ ssNder1_5r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962)
| ~ ssNder1_4r1r1r1r1(X3954,X3965,X3964,X3961)
| ~ ssNder1_3r1r1r1(X3954,X3965,X3964)
| ~ ssNder1_2r1r1(X3954,X3965)
| ~ ssNder1_1r1(X3954)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953,X3952,X3959,X3960,X3957,X3958,X3955,X3963,X3956,X3951)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953,X3952,X3959,X3960,X3957,X3958,X3955,X3963)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X3954,X3965,X3964,X3961,X3962,X3953,X3952,X3959,X3960,X3957,X3958,X3955)
| ssPv19_2r1r1(X3954,X3965) ),
inference(resolution,[status(thm)],[c194,clause43]) ).
cnf(c291,plain,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969,X5956,X5959,X5965,X5963,X5957,X5970,X5964)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969,X5956,X5959,X5965,X5963,X5957,X5970)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969,X5956,X5959,X5965,X5963,X5957)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969,X5956,X5959,X5965,X5963)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969,X5956,X5959,X5965)
| ~ ssNder1_7r1r1r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969,X5956,X5959)
| ~ ssNder1_6r1r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969,X5956)
| ~ ssNder1_5r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969)
| ~ ssNder1_4r1r1r1r1(X5958,X5962,X5960,X5961)
| ~ ssNder1_3r1r1r1(X5958,X5962,X5960)
| ~ ssNder1_2r1r1(X5958,X5962)
| ~ ssNder1_1r1(X5958)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969,X5956,X5959,X5965,X5963,X5957,X5970,X5964,X5966,X5968,X5967)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969,X5956,X5959,X5965,X5963,X5957,X5970,X5964,X5966)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X5958,X5962,X5960,X5961,X5969,X5956,X5959,X5965,X5963,X5957,X5970,X5964)
| ssPv19_2r1r1(X5958,X5962) ),
inference(resolution,[status(thm)],[c195,c136]) ).
cnf(c411,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X8486,X8483,X8494,X8493,X8485,X8488,X8490,X8489,X8492,X8497,X8487)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X8486,X8483,X8494,X8493,X8485,X8488,X8490,X8489,X8492,X8497)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X8486,X8483,X8494,X8493,X8485,X8488,X8490,X8489,X8492)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X8486,X8483,X8494,X8493,X8485,X8488,X8490,X8489)
| ~ ssNder1_7r1r1r1r1r1r1r1(X8486,X8483,X8494,X8493,X8485,X8488,X8490)
| ~ ssNder1_6r1r1r1r1r1r1(X8486,X8483,X8494,X8493,X8485,X8488)
| ~ ssNder1_5r1r1r1r1r1(X8486,X8483,X8494,X8493,X8485)
| ~ ssNder1_4r1r1r1r1(X8486,X8483,X8494,X8493)
| ~ ssNder1_3r1r1r1(X8486,X8483,X8494)
| ~ ssNder1_2r1r1(X8486,X8483)
| ~ ssNder1_1r1(X8486)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X8486,X8483,X8494,X8493,X8485,X8488,X8490,X8489,X8492,X8497,X8487,X8496,X8484,X8495,X8491)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X8486,X8483,X8494,X8493,X8485,X8488,X8490,X8489,X8492,X8497,X8487,X8496,X8484)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X8486,X8483,X8494,X8493,X8485,X8488,X8490,X8489,X8492,X8497,X8487,X8496)
| ssPv19_2r1r1(X8486,X8483) ),
inference(resolution,[status(thm)],[c291,c101]) ).
cnf(c576,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X16688,X16679,X16677,X16675,X16684,X16685,X16687,X16678,X16680,X16681)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X16688,X16679,X16677,X16675,X16684,X16685,X16687,X16678,X16680)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X16688,X16679,X16677,X16675,X16684,X16685,X16687,X16678)
| ~ ssNder1_7r1r1r1r1r1r1r1(X16688,X16679,X16677,X16675,X16684,X16685,X16687)
| ~ ssNder1_6r1r1r1r1r1r1(X16688,X16679,X16677,X16675,X16684,X16685)
| ~ ssNder1_5r1r1r1r1r1(X16688,X16679,X16677,X16675,X16684)
| ~ ssNder1_4r1r1r1r1(X16688,X16679,X16677,X16675)
| ~ ssNder1_3r1r1r1(X16688,X16679,X16677)
| ~ ssNder1_2r1r1(X16688,X16679)
| ~ ssNder1_1r1(X16688)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X16688,X16679,X16677,X16675,X16684,X16685,X16687,X16678,X16680,X16681,X16676,X16683,X16686,X16674,X16682)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X16688,X16679,X16677,X16675,X16684,X16685,X16687,X16678,X16680,X16681,X16676,X16683,X16686)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X16688,X16679,X16677,X16675,X16684,X16685,X16687,X16678,X16680,X16681,X16676,X16683)
| ssPv19_2r1r1(X16688,X16679) ),
inference(resolution,[status(thm)],[c411,c88]) ).
cnf(c947,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X17553,X17547,X17548,X17543,X17551,X17541,X17546,X17540,X17542)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X17553,X17547,X17548,X17543,X17551,X17541,X17546,X17540)
| ~ ssNder1_7r1r1r1r1r1r1r1(X17553,X17547,X17548,X17543,X17551,X17541,X17546)
| ~ ssNder1_6r1r1r1r1r1r1(X17553,X17547,X17548,X17543,X17551,X17541)
| ~ ssNder1_5r1r1r1r1r1(X17553,X17547,X17548,X17543,X17551)
| ~ ssNder1_4r1r1r1r1(X17553,X17547,X17548,X17543)
| ~ ssNder1_3r1r1r1(X17553,X17547,X17548)
| ~ ssNder1_2r1r1(X17553,X17547)
| ~ ssNder1_1r1(X17553)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17553,X17547,X17548,X17543,X17551,X17541,X17546,X17540,X17542,X17549,X17552,X17554,X17550,X17544,X17545)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17553,X17547,X17548,X17543,X17551,X17541,X17546,X17540,X17542,X17549,X17552,X17554,X17550)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17553,X17547,X17548,X17543,X17551,X17541,X17546,X17540,X17542,X17549,X17552,X17554)
| ssPv19_2r1r1(X17553,X17547) ),
inference(resolution,[status(thm)],[c576,c76]) ).
cnf(c972,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X17566,X17569,X17558,X17557,X17568,X17556,X17560,X17563)
| ~ ssNder1_7r1r1r1r1r1r1r1(X17566,X17569,X17558,X17557,X17568,X17556,X17560)
| ~ ssNder1_6r1r1r1r1r1r1(X17566,X17569,X17558,X17557,X17568,X17556)
| ~ ssNder1_5r1r1r1r1r1(X17566,X17569,X17558,X17557,X17568)
| ~ ssNder1_4r1r1r1r1(X17566,X17569,X17558,X17557)
| ~ ssNder1_3r1r1r1(X17566,X17569,X17558)
| ~ ssNder1_2r1r1(X17566,X17569)
| ~ ssNder1_1r1(X17566)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17566,X17569,X17558,X17557,X17568,X17556,X17560,X17563,X17555,X17561,X17559,X17562,X17564,X17567,X17565)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17566,X17569,X17558,X17557,X17568,X17556,X17560,X17563,X17555,X17561,X17559,X17562,X17564)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17566,X17569,X17558,X17557,X17568,X17556,X17560,X17563,X17555,X17561,X17559,X17562)
| ssPv19_2r1r1(X17566,X17569) ),
inference(resolution,[status(thm)],[c947,c66]) ).
cnf(c973,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X17578,X17572,X17577,X17582,X17570,X17584,X17575)
| ~ ssNder1_6r1r1r1r1r1r1(X17578,X17572,X17577,X17582,X17570,X17584)
| ~ ssNder1_5r1r1r1r1r1(X17578,X17572,X17577,X17582,X17570)
| ~ ssNder1_4r1r1r1r1(X17578,X17572,X17577,X17582)
| ~ ssNder1_3r1r1r1(X17578,X17572,X17577)
| ~ ssNder1_2r1r1(X17578,X17572)
| ~ ssNder1_1r1(X17578)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17578,X17572,X17577,X17582,X17570,X17584,X17575,X17573,X17574,X17581,X17571,X17583,X17576,X17579,X17580)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17578,X17572,X17577,X17582,X17570,X17584,X17575,X17573,X17574,X17581,X17571,X17583,X17576)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17578,X17572,X17577,X17582,X17570,X17584,X17575,X17573,X17574,X17581,X17571,X17583)
| ssPv19_2r1r1(X17578,X17572) ),
inference(resolution,[status(thm)],[c972,c57]) ).
cnf(c974,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X17593,X17594,X17599,X17596,X17585,X17586)
| ~ ssNder1_5r1r1r1r1r1(X17593,X17594,X17599,X17596,X17585)
| ~ ssNder1_4r1r1r1r1(X17593,X17594,X17599,X17596)
| ~ ssNder1_3r1r1r1(X17593,X17594,X17599)
| ~ ssNder1_2r1r1(X17593,X17594)
| ~ ssNder1_1r1(X17593)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17593,X17594,X17599,X17596,X17585,X17586,X17587,X17592,X17588,X17597,X17595,X17589,X17590,X17598,X17591)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17593,X17594,X17599,X17596,X17585,X17586,X17587,X17592,X17588,X17597,X17595,X17589,X17590)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17593,X17594,X17599,X17596,X17585,X17586,X17587,X17592,X17588,X17597,X17595,X17589)
| ssPv19_2r1r1(X17593,X17594) ),
inference(resolution,[status(thm)],[c973,c43]) ).
cnf(c975,plain,
( ~ ssNder1_5r1r1r1r1r1(X17606,X17614,X17601,X17607,X17610)
| ~ ssNder1_4r1r1r1r1(X17606,X17614,X17601,X17607)
| ~ ssNder1_3r1r1r1(X17606,X17614,X17601)
| ~ ssNder1_2r1r1(X17606,X17614)
| ~ ssNder1_1r1(X17606)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17606,X17614,X17601,X17607,X17610,X17600,X17605,X17608,X17612,X17602,X17611,X17603,X17613,X17609,X17604)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17606,X17614,X17601,X17607,X17610,X17600,X17605,X17608,X17612,X17602,X17611,X17603,X17613)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17606,X17614,X17601,X17607,X17610,X17600,X17605,X17608,X17612,X17602,X17611,X17603)
| ssPv19_2r1r1(X17606,X17614) ),
inference(resolution,[status(thm)],[c974,c30]) ).
cnf(c976,plain,
( ~ ssNder1_4r1r1r1r1(X17655,X17650,X17648,X17658)
| ~ ssNder1_3r1r1r1(X17655,X17650,X17648)
| ~ ssNder1_2r1r1(X17655,X17650)
| ~ ssNder1_1r1(X17655)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17655,X17650,X17648,X17658,X17661,X17649,X17662,X17656,X17659,X17651,X17657,X17660,X17652,X17653,X17654)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17655,X17650,X17648,X17658,X17661,X17649,X17662,X17656,X17659,X17651,X17657,X17660,X17652)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17655,X17650,X17648,X17658,X17661,X17649,X17662,X17656,X17659,X17651,X17657,X17660)
| ssPv19_2r1r1(X17655,X17650) ),
inference(resolution,[status(thm)],[c975,c19]) ).
cnf(c978,plain,
( ~ ssNder1_3r1r1r1(X17669,X17668,X17670)
| ~ ssNder1_2r1r1(X17669,X17668)
| ~ ssNder1_1r1(X17669)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17669,X17668,X17670,X17667,X17671,X17677,X17666,X17672,X17663,X17664,X17673,X17676,X17674,X17675,X17665)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17669,X17668,X17670,X17667,X17671,X17677,X17666,X17672,X17663,X17664,X17673,X17676,X17674)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17669,X17668,X17670,X17667,X17671,X17677,X17666,X17672,X17663,X17664,X17673,X17676)
| ssPv19_2r1r1(X17669,X17668) ),
inference(resolution,[status(thm)],[c976,c10]) ).
cnf(c979,plain,
( ~ ssNder1_2r1r1(X17687,X17690)
| ~ ssNder1_1r1(X17687)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17687,X17690,X17678,X17692,X17682,X17684,X17679,X17691,X17680,X17688,X17681,X17689,X17685,X17686,X17683)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17687,X17690,X17678,X17692,X17682,X17684,X17679,X17691,X17680,X17688,X17681,X17689,X17685)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17687,X17690,X17678,X17692,X17682,X17684,X17679,X17691,X17680,X17688,X17681,X17689)
| ssPv19_2r1r1(X17687,X17690) ),
inference(resolution,[status(thm)],[c978,c5]) ).
cnf(c980,plain,
( ~ ssNder1_1r1(X17699)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17699,X17704,X17693,X17706,X17701,X17702,X17700,X17698,X17695,X17705,X17707,X17694,X17703,X17697,X17696)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17699,X17704,X17693,X17706,X17701,X17702,X17700,X17698,X17695,X17705,X17707,X17694,X17703)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17699,X17704,X17693,X17706,X17701,X17702,X17700,X17698,X17695,X17705,X17707,X17694)
| ssPv19_2r1r1(X17699,X17704) ),
inference(resolution,[status(thm)],[c979,c2]) ).
cnf(c981,plain,
( ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17712,X17708,X17722,X17716,X17711,X17713,X17718,X17720,X17715,X17710,X17721,X17719,X17717,X17709,X17714)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17712,X17708,X17722,X17716,X17711,X17713,X17718,X17720,X17715,X17710,X17721,X17719,X17717)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17712,X17708,X17722,X17716,X17711,X17713,X17718,X17720,X17715,X17710,X17721,X17719)
| ssPv19_2r1r1(X17712,X17708) ),
inference(resolution,[status(thm)],[c980,c0]) ).
cnf(c982,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X17745,X17737,X17749,X17735,X17739,X17741,X17742,X17740,X17743,X17738,X17736,X17746,X17744,X17747,X17748)
| ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X17745,X17737,X17749,X17735,X17739,X17741,X17742,X17740,X17743,X17738,X17736,X17746,X17744)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X17745,X17737,X17749,X17735,X17739,X17741,X17742,X17740,X17743,X17738,X17736,X17746)
| ssPv19_2r1r1(X17745,X17737) ),
inference(resolution,[status(thm)],[c981,clause1]) ).
cnf(c985,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X34999,X34994,X34995,X34998,X34997,X34989,X34991,X35000,X35001,X34996,X34992,X34990,skc23,X34988,X34993)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X34999,X34994,X34995,X34998,X34997,X34989,X34991,X35000,X35001,X34996,X34992,X34990)
| ssPv19_2r1r1(X34999,X34994)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X34999,X34994,X34995,X34998,X34997,X34989,X34991,X35000,X35001,X34996,X34992)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X34999,X34994,X34995,X34998,X34997,X34989,X34991,X35000,X35001,X34996)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X34999,X34994,X34995,X34998,X34997,X34989,X34991,X35000,X35001)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X34999,X34994,X34995,X34998,X34997,X34989,X34991,X35000)
| ~ ssNder1_7r1r1r1r1r1r1r1(X34999,X34994,X34995,X34998,X34997,X34989,X34991)
| ~ ssNder1_6r1r1r1r1r1r1(X34999,X34994,X34995,X34998,X34997,X34989)
| ~ ssNder1_5r1r1r1r1r1(X34999,X34994,X34995,X34998,X34997)
| ~ ssNder1_4r1r1r1r1(X34999,X34994,X34995,X34998)
| ~ ssNder1_3r1r1r1(X34999,X34994,X34995)
| ~ ssNder1_2r1r1(X34999,X34994)
| ~ ssNder1_1r1(X34999)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c982,clause23]) ).
cnf(c1816,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35015,X35006,X35004,X35002,X35011,X35012,X35014,X35005,X35007,X35008,X35003,X35009,skc23,X35013,X35010)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35015,X35006,X35004,X35002,X35011,X35012,X35014,X35005,X35007,X35008,X35003,X35009)
| ssPv19_2r1r1(X35015,X35006)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X35015,X35006,X35004,X35002,X35011,X35012,X35014,X35005,X35007,X35008)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X35015,X35006,X35004,X35002,X35011,X35012,X35014,X35005,X35007)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X35015,X35006,X35004,X35002,X35011,X35012,X35014,X35005)
| ~ ssNder1_7r1r1r1r1r1r1r1(X35015,X35006,X35004,X35002,X35011,X35012,X35014)
| ~ ssNder1_6r1r1r1r1r1r1(X35015,X35006,X35004,X35002,X35011,X35012)
| ~ ssNder1_5r1r1r1r1r1(X35015,X35006,X35004,X35002,X35011)
| ~ ssNder1_4r1r1r1r1(X35015,X35006,X35004,X35002)
| ~ ssNder1_3r1r1r1(X35015,X35006,X35004)
| ~ ssNder1_2r1r1(X35015,X35006)
| ~ ssNder1_1r1(X35015)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c985,c88]) ).
cnf(c1817,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35029,X35023,X35024,X35019,X35028,X35017,X35021,X35016,X35018,X35025,X35020,X35022,skc23,X35027,X35026)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35029,X35023,X35024,X35019,X35028,X35017,X35021,X35016,X35018,X35025,X35020,X35022)
| ssPv19_2r1r1(X35029,X35023)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X35029,X35023,X35024,X35019,X35028,X35017,X35021,X35016,X35018)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X35029,X35023,X35024,X35019,X35028,X35017,X35021,X35016)
| ~ ssNder1_7r1r1r1r1r1r1r1(X35029,X35023,X35024,X35019,X35028,X35017,X35021)
| ~ ssNder1_6r1r1r1r1r1r1(X35029,X35023,X35024,X35019,X35028,X35017)
| ~ ssNder1_5r1r1r1r1r1(X35029,X35023,X35024,X35019,X35028)
| ~ ssNder1_4r1r1r1r1(X35029,X35023,X35024,X35019)
| ~ ssNder1_3r1r1r1(X35029,X35023,X35024)
| ~ ssNder1_2r1r1(X35029,X35023)
| ~ ssNder1_1r1(X35029)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1816,c76]) ).
cnf(c1818,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35040,X35043,X35034,X35033,X35041,X35032,X35035,X35038,X35031,X35030,X35042,X35037,skc23,X35039,X35036)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35040,X35043,X35034,X35033,X35041,X35032,X35035,X35038,X35031,X35030,X35042,X35037)
| ssPv19_2r1r1(X35040,X35043)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X35040,X35043,X35034,X35033,X35041,X35032,X35035,X35038)
| ~ ssNder1_7r1r1r1r1r1r1r1(X35040,X35043,X35034,X35033,X35041,X35032,X35035)
| ~ ssNder1_6r1r1r1r1r1r1(X35040,X35043,X35034,X35033,X35041,X35032)
| ~ ssNder1_5r1r1r1r1r1(X35040,X35043,X35034,X35033,X35041)
| ~ ssNder1_4r1r1r1r1(X35040,X35043,X35034,X35033)
| ~ ssNder1_3r1r1r1(X35040,X35043,X35034)
| ~ ssNder1_2r1r1(X35040,X35043)
| ~ ssNder1_1r1(X35040)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1817,c66]) ).
cnf(c1819,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35087,X35080,X35086,X35088,X35076,X35089,X35082,X35081,X35084,X35078,X35077,X35085,skc23,X35079,X35083)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35087,X35080,X35086,X35088,X35076,X35089,X35082,X35081,X35084,X35078,X35077,X35085)
| ssPv19_2r1r1(X35087,X35080)
| ~ ssNder1_7r1r1r1r1r1r1r1(X35087,X35080,X35086,X35088,X35076,X35089,X35082)
| ~ ssNder1_6r1r1r1r1r1r1(X35087,X35080,X35086,X35088,X35076,X35089)
| ~ ssNder1_5r1r1r1r1r1(X35087,X35080,X35086,X35088,X35076)
| ~ ssNder1_4r1r1r1r1(X35087,X35080,X35086,X35088)
| ~ ssNder1_3r1r1r1(X35087,X35080,X35086)
| ~ ssNder1_2r1r1(X35087,X35080)
| ~ ssNder1_1r1(X35087)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1818,c57]) ).
cnf(c1820,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35096,X35097,X35102,X35100,X35091,X35092,X35093,X35098,X35090,X35099,X35094,X35095,skc23,X35101,X35103)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35096,X35097,X35102,X35100,X35091,X35092,X35093,X35098,X35090,X35099,X35094,X35095)
| ssPv19_2r1r1(X35096,X35097)
| ~ ssNder1_6r1r1r1r1r1r1(X35096,X35097,X35102,X35100,X35091,X35092)
| ~ ssNder1_5r1r1r1r1r1(X35096,X35097,X35102,X35100,X35091)
| ~ ssNder1_4r1r1r1r1(X35096,X35097,X35102,X35100)
| ~ ssNder1_3r1r1r1(X35096,X35097,X35102)
| ~ ssNder1_2r1r1(X35096,X35097)
| ~ ssNder1_1r1(X35096)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1819,c43]) ).
cnf(c1821,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35113,X35117,X35108,X35114,X35116,X35107,X35104,X35105,X35109,X35106,X35111,X35115,skc23,X35112,X35110)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35113,X35117,X35108,X35114,X35116,X35107,X35104,X35105,X35109,X35106,X35111,X35115)
| ssPv19_2r1r1(X35113,X35117)
| ~ ssNder1_5r1r1r1r1r1(X35113,X35117,X35108,X35114,X35116)
| ~ ssNder1_4r1r1r1r1(X35113,X35117,X35108,X35114)
| ~ ssNder1_3r1r1r1(X35113,X35117,X35108)
| ~ ssNder1_2r1r1(X35113,X35117)
| ~ ssNder1_1r1(X35113)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1820,c30]) ).
cnf(c1822,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35125,X35121,X35119,X35128,X35129,X35130,X35131,X35122,X35124,X35127,X35120,X35123,skc23,X35126,X35118)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35125,X35121,X35119,X35128,X35129,X35130,X35131,X35122,X35124,X35127,X35120,X35123)
| ssPv19_2r1r1(X35125,X35121)
| ~ ssNder1_4r1r1r1r1(X35125,X35121,X35119,X35128)
| ~ ssNder1_3r1r1r1(X35125,X35121,X35119)
| ~ ssNder1_2r1r1(X35125,X35121)
| ~ ssNder1_1r1(X35125)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1821,c19]) ).
cnf(c1823,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35140,X35138,X35142,X35137,X35144,X35134,X35133,X35139,X35135,X35141,X35145,X35143,skc23,X35132,X35136)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35140,X35138,X35142,X35137,X35144,X35134,X35133,X35139,X35135,X35141,X35145,X35143)
| ssPv19_2r1r1(X35140,X35138)
| ~ ssNder1_3r1r1r1(X35140,X35138,X35142)
| ~ ssNder1_2r1r1(X35140,X35138)
| ~ ssNder1_1r1(X35140)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1822,c10]) ).
cnf(c1824,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35185,X35189,X35178,X35187,X35181,X35183,X35180,X35182,X35179,X35191,X35184,X35188,skc23,X35186,X35190)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35185,X35189,X35178,X35187,X35181,X35183,X35180,X35182,X35179,X35191,X35184,X35188)
| ssPv19_2r1r1(X35185,X35189)
| ~ ssNder1_2r1r1(X35185,X35189)
| ~ ssNder1_1r1(X35185)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1823,c5]) ).
cnf(c1825,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35195,X35200,X35201,X35205,X35197,X35196,X35194,X35198,X35204,X35203,X35193,X35202,skc23,X35199,X35192)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35195,X35200,X35201,X35205,X35197,X35196,X35194,X35198,X35204,X35203,X35193,X35202)
| ssPv19_2r1r1(X35195,X35200)
| ~ ssNder1_1r1(X35195)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1824,c2]) ).
cnf(c1826,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35207,X35219,X35212,X35214,X35217,X35218,X35206,X35210,X35208,X35213,X35215,X35211,skc23,X35216,X35209)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35207,X35219,X35212,X35214,X35217,X35218,X35206,X35210,X35208,X35213,X35215,X35211)
| ssPv19_2r1r1(X35207,X35219)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1825,c0]) ).
cnf(c1827,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35225,X35232,X35233,X35226,X35221,X35222,X35220,X35229,X35231,X35224,X35223,X35227,skc23,X35228,X35230)
| ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(X35225,X35232,X35233,X35226,X35221,X35222,X35220,X35229,X35231,X35224,X35223,X35227)
| ssPv19_2r1r1(X35225,X35232) ),
inference(resolution,[status(thm)],[c1826,clause1]) ).
cnf(c1829,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35594,X35587,X35597,X35590,X35598,X35591,X35589,X35592,X35593,X35599,X35588,X35586,skc23,X35595,X35596)
| ssPv19_2r1r1(X35594,X35587)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X35594,X35587,X35597,X35590,X35598,X35591,X35589,X35592,X35593,X35599,X35588)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X35594,X35587,X35597,X35590,X35598,X35591,X35589,X35592,X35593,X35599)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X35594,X35587,X35597,X35590,X35598,X35591,X35589,X35592,X35593)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X35594,X35587,X35597,X35590,X35598,X35591,X35589,X35592)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X35594,X35587,X35597,X35590,X35598,X35591,X35589,X35592)
| ~ ssNder1_7r1r1r1r1r1r1r1(X35594,X35587,X35597,X35590,X35598,X35591,X35589)
| ~ ssNder1_6r1r1r1r1r1r1(X35594,X35587,X35597,X35590,X35598,X35591)
| ~ ssNder1_5r1r1r1r1r1(X35594,X35587,X35597,X35590,X35598)
| ~ ssNder1_4r1r1r1r1(X35594,X35587,X35597,X35590)
| ~ ssNder1_3r1r1r1(X35594,X35587,X35597)
| ~ ssNder1_2r1r1(X35594,X35587)
| ~ ssPv20_1r1(X35594)
| ~ ssNder1_1r1(X35594)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1827,c403]) ).
cnf(c1853,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35613,X35606,X35602,X35600,X35609,X35610,X35612,X35603,X35607,X35608,X35601,X35611,skc23,X35605,X35604)
| ssPv19_2r1r1(X35613,X35606)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X35613,X35606,X35602,X35600,X35609,X35610,X35612,X35603,X35607,X35608)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X35613,X35606,X35602,X35600,X35609,X35610,X35612,X35603,X35607)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X35613,X35606,X35602,X35600,X35609,X35610,X35612,X35603)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X35613,X35606,X35602,X35600,X35609,X35610,X35612,X35603)
| ~ ssNder1_7r1r1r1r1r1r1r1(X35613,X35606,X35602,X35600,X35609,X35610,X35612)
| ~ ssNder1_6r1r1r1r1r1r1(X35613,X35606,X35602,X35600,X35609,X35610)
| ~ ssNder1_5r1r1r1r1r1(X35613,X35606,X35602,X35600,X35609)
| ~ ssNder1_4r1r1r1r1(X35613,X35606,X35602,X35600)
| ~ ssNder1_3r1r1r1(X35613,X35606,X35602)
| ~ ssNder1_2r1r1(X35613,X35606)
| ~ ssPv20_1r1(X35613)
| ~ ssNder1_1r1(X35613)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1829,c88]) ).
cnf(c1854,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35627,X35622,X35623,X35619,X35625,X35616,X35621,X35615,X35617,X35624,X35618,X35620,skc23,X35614,X35626)
| ssPv19_2r1r1(X35627,X35622)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X35627,X35622,X35623,X35619,X35625,X35616,X35621,X35615,X35617)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X35627,X35622,X35623,X35619,X35625,X35616,X35621,X35615)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X35627,X35622,X35623,X35619,X35625,X35616,X35621,X35615)
| ~ ssNder1_7r1r1r1r1r1r1r1(X35627,X35622,X35623,X35619,X35625,X35616,X35621)
| ~ ssNder1_6r1r1r1r1r1r1(X35627,X35622,X35623,X35619,X35625,X35616)
| ~ ssNder1_5r1r1r1r1r1(X35627,X35622,X35623,X35619,X35625)
| ~ ssNder1_4r1r1r1r1(X35627,X35622,X35623,X35619)
| ~ ssNder1_3r1r1r1(X35627,X35622,X35623)
| ~ ssNder1_2r1r1(X35627,X35622)
| ~ ssPv20_1r1(X35627)
| ~ ssNder1_1r1(X35627)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1853,c76]) ).
cnf(c1855,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35637,X35640,X35631,X35630,X35639,X35629,X35632,X35634,X35628,X35636,X35638,X35641,skc23,X35633,X35635)
| ssPv19_2r1r1(X35637,X35640)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X35637,X35640,X35631,X35630,X35639,X35629,X35632,X35634)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X35637,X35640,X35631,X35630,X35639,X35629,X35632,X35634)
| ~ ssNder1_7r1r1r1r1r1r1r1(X35637,X35640,X35631,X35630,X35639,X35629,X35632)
| ~ ssNder1_6r1r1r1r1r1r1(X35637,X35640,X35631,X35630,X35639,X35629)
| ~ ssNder1_5r1r1r1r1r1(X35637,X35640,X35631,X35630,X35639)
| ~ ssNder1_4r1r1r1r1(X35637,X35640,X35631,X35630)
| ~ ssNder1_3r1r1r1(X35637,X35640,X35631)
| ~ ssNder1_2r1r1(X35637,X35640)
| ~ ssPv20_1r1(X35637)
| ~ ssNder1_1r1(X35637)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1854,c66]) ).
cnf(c1856,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35681,X35675,X35678,X35682,X35673,X35684,X35677,X35676,X35680,X35685,X35679,X35683,skc23,X35672,X35674)
| ssPv19_2r1r1(X35681,X35675)
| ~ ssPv13_8r1r1r1r1r1r1r1r1(X35681,X35675,X35678,X35682,X35673,X35684,X35677,X35676)
| ~ ssNder1_7r1r1r1r1r1r1r1(X35681,X35675,X35678,X35682,X35673,X35684,X35677)
| ~ ssNder1_6r1r1r1r1r1r1(X35681,X35675,X35678,X35682,X35673,X35684)
| ~ ssNder1_5r1r1r1r1r1(X35681,X35675,X35678,X35682,X35673)
| ~ ssNder1_4r1r1r1r1(X35681,X35675,X35678,X35682)
| ~ ssNder1_3r1r1r1(X35681,X35675,X35678)
| ~ ssNder1_2r1r1(X35681,X35675)
| ~ ssPv20_1r1(X35681)
| ~ ssNder1_1r1(X35681)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1855,c57]) ).
cnf(c1857,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35689,X35686,X35692,X35687,X35696,X35698,X35690,skc24,X35693,X35694,X35691,X35697,skc23,X35695,X35688)
| ssPv19_2r1r1(X35689,X35686)
| ~ ssNder1_7r1r1r1r1r1r1r1(X35689,X35686,X35692,X35687,X35696,X35698,X35690)
| ~ ssNder1_6r1r1r1r1r1r1(X35689,X35686,X35692,X35687,X35696,X35698)
| ~ ssNder1_5r1r1r1r1r1(X35689,X35686,X35692,X35687,X35696)
| ~ ssNder1_4r1r1r1r1(X35689,X35686,X35692,X35687)
| ~ ssNder1_3r1r1r1(X35689,X35686,X35692)
| ~ ssNder1_2r1r1(X35689,X35686)
| ~ ssPv20_1r1(X35689)
| ~ ssNder1_1r1(X35689)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1856,c49]) ).
cnf(c1858,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35705,X35706,X35711,X35708,X35700,X35701,X35702,skc24,X35709,X35699,X35710,X35703,skc23,X35704,X35707)
| ssPv19_2r1r1(X35705,X35706)
| ~ ssNder1_6r1r1r1r1r1r1(X35705,X35706,X35711,X35708,X35700,X35701)
| ~ ssNder1_5r1r1r1r1r1(X35705,X35706,X35711,X35708,X35700)
| ~ ssNder1_4r1r1r1r1(X35705,X35706,X35711,X35708)
| ~ ssNder1_3r1r1r1(X35705,X35706,X35711)
| ~ ssNder1_2r1r1(X35705,X35706)
| ~ ssPv20_1r1(X35705)
| ~ ssNder1_1r1(X35705)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1857,c43]) ).
cnf(c1859,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35716,X35724,X35713,X35717,X35719,X35712,X35721,skc24,X35720,X35714,X35718,X35723,skc23,X35715,X35722)
| ssPv19_2r1r1(X35716,X35724)
| ~ ssNder1_5r1r1r1r1r1(X35716,X35724,X35713,X35717,X35719)
| ~ ssNder1_4r1r1r1r1(X35716,X35724,X35713,X35717)
| ~ ssNder1_3r1r1r1(X35716,X35724,X35713)
| ~ ssNder1_2r1r1(X35716,X35724)
| ~ ssPv20_1r1(X35716)
| ~ ssNder1_1r1(X35716)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1858,c30]) ).
cnf(c1860,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35732,X35726,X35725,X35734,X35736,X35727,X35728,skc24,X35737,X35729,X35731,X35733,skc23,X35730,X35735)
| ssPv19_2r1r1(X35732,X35726)
| ~ ssNder1_4r1r1r1r1(X35732,X35726,X35725,X35734)
| ~ ssNder1_3r1r1r1(X35732,X35726,X35725)
| ~ ssNder1_2r1r1(X35732,X35726)
| ~ ssPv20_1r1(X35732)
| ~ ssNder1_1r1(X35732)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1859,c19]) ).
cnf(c1861,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35776,X35775,X35779,X35773,X35774,X35772,X35777,skc24,X35778,X35769,X35770,X35780,skc23,X35781,X35771)
| ssPv19_2r1r1(X35776,X35775)
| ~ ssNder1_3r1r1r1(X35776,X35775,X35779)
| ~ ssNder1_2r1r1(X35776,X35775)
| ~ ssPv20_1r1(X35776)
| ~ ssNder1_1r1(X35776)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1860,c10]) ).
cnf(c1862,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35787,X35792,X35782,X35784,X35793,X35785,X35789,skc24,X35788,X35791,X35783,X35790,skc23,X35786,X35794)
| ssPv19_2r1r1(X35787,X35792)
| ~ ssNder1_2r1r1(X35787,X35792)
| ~ ssPv20_1r1(X35787)
| ~ ssNder1_1r1(X35787)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1861,c5]) ).
cnf(c1863,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35799,X35803,X35798,X35800,X35802,X35795,X35807,skc24,X35801,X35806,X35804,X35797,skc23,X35805,X35796)
| ssPv19_2r1r1(X35799,X35803)
| ~ ssPv20_1r1(X35799)
| ~ ssNder1_1r1(X35799)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1862,c2]) ).
cnf(c1864,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35810,X35811,X35814,X35820,X35817,X35818,X35809,skc24,X35815,X35813,X35812,X35819,skc23,X35808,X35816)
| ssPv19_2r1r1(X35810,X35811)
| ~ ssPv20_1r1(X35810)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1863,c0]) ).
cnf(c1865,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35829,X35826,X35827,X35833,X35831,X35824,X35822,skc24,X35823,X35830,X35832,X35828,skc23,X35821,X35825)
| ssPv19_2r1r1(X35829,X35826)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1864,c1526]) ).
cnf(c1866,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35867,X35872,X35868,X35875,X35877,X35876,X35865,skc24,X35869,X35871,X35873,X35866,skc23,X35874,X35870)
| ssPv19_2r1r1(X35867,X35872) ),
inference(resolution,[status(thm)],[c1865,clause1]) ).
cnf(c1868,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35895,X35882,X35884,X35878,X35888,X35889,X35887,skc24,X35883,X35886,X35881,X35891,skc23,X35894,X35898)
| ~ ssNder1_1r1(X35895)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X35895,X35882,X35890,X35885,X35879,X35880,X35893,skc24,X35897,X35896,X35892)
| ssPv16_5r1r1r1r1r1(X35895,X35882,X35890,X35885,X35879) ),
inference(resolution,[status(thm)],[c1866,c124]) ).
cnf(c1870,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35900,X35911,X35904,X35909,X35913,X35903,X35918,skc24,X35919,X35912,X35915,X35899,skc23,X35916,X35908)
| ~ ssNder1_0
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X35900,X35911,X35901,X35907,X35914,X35917,X35905,skc24,X35906,X35910,X35902)
| ssPv16_5r1r1r1r1r1(X35900,X35911,X35901,X35907,X35914) ),
inference(resolution,[status(thm)],[c1868,c0]) ).
cnf(c1871,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X35926,X35936,X35928,X35931,X35930,X35938,X35933,skc24,X35932,X35929,X35925,X35921,skc23,X35935,X35937)
| ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(X35926,X35936,X35934,X35920,X35927,X35923,X35940,skc24,X35924,X35939,X35922)
| ssPv16_5r1r1r1r1r1(X35926,X35936,X35934,X35920,X35927) ),
inference(resolution,[status(thm)],[c1870,clause1]) ).
cnf(c1873,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36201,X36189,X36207,X36188,X36191,X36205,X36202,skc24,X36193,X36203,X36194,X36206,skc23,X36190,X36196)
| ssPv16_5r1r1r1r1r1(X36201,X36189,X36204,X36195,X36197)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X36201,X36189,X36204,X36195,X36197,X36198,X36192,skc24,X36199,X36200)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X36201,X36189,X36204,X36195,X36197,X36198,X36192,skc24,X36199)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X36201,X36189,X36204,X36195,X36197,X36198,X36192,skc24)
| ~ ssPv14_7r1r1r1r1r1r1r1(X36201,X36189,X36204,X36195,X36197,X36198,X36192)
| ~ ssNder1_7r1r1r1r1r1r1r1(X36201,X36189,X36204,X36195,X36197,X36198,X36192)
| ~ ssNder1_6r1r1r1r1r1r1(X36201,X36189,X36204,X36195,X36197,X36198)
| ~ ssNder1_5r1r1r1r1r1(X36201,X36189,X36204,X36195,X36197)
| ~ ssNder1_4r1r1r1r1(X36201,X36189,X36204,X36195)
| ~ ssNder1_3r1r1r1(X36201,X36189,X36204)
| ~ ssPv19_2r1r1(X36201,X36189)
| ~ ssNder1_2r1r1(X36201,X36189)
| ~ ssNder1_1r1(X36201)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1871,c405]) ).
cnf(c1887,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36226,X36219,X36209,X36223,X36210,X36224,X36215,skc24,X36218,X36220,X36211,X36213,skc23,X36221,X36212)
| ssPv16_5r1r1r1r1r1(X36226,X36219,X36222,X36214,X36225)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X36226,X36219,X36222,X36214,X36225,X36208,X36216,skc24,X36217)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X36226,X36219,X36222,X36214,X36225,X36208,X36216,skc24)
| ~ ssPv14_7r1r1r1r1r1r1r1(X36226,X36219,X36222,X36214,X36225,X36208,X36216)
| ~ ssNder1_7r1r1r1r1r1r1r1(X36226,X36219,X36222,X36214,X36225,X36208,X36216)
| ~ ssNder1_6r1r1r1r1r1r1(X36226,X36219,X36222,X36214,X36225,X36208)
| ~ ssNder1_5r1r1r1r1r1(X36226,X36219,X36222,X36214,X36225)
| ~ ssNder1_4r1r1r1r1(X36226,X36219,X36222,X36214)
| ~ ssNder1_3r1r1r1(X36226,X36219,X36222)
| ~ ssPv19_2r1r1(X36226,X36219)
| ~ ssNder1_2r1r1(X36226,X36219)
| ~ ssNder1_1r1(X36226)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1873,c76]) ).
cnf(c1888,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36272,X36258,X36275,X36266,X36274,X36269,X36259,skc24,X36260,X36267,X36265,X36273,skc23,X36270,X36268)
| ssPv16_5r1r1r1r1r1(X36272,X36258,X36261,X36262,X36271)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X36272,X36258,X36261,X36262,X36271,X36263,X36264,skc24)
| ~ ssPv14_7r1r1r1r1r1r1r1(X36272,X36258,X36261,X36262,X36271,X36263,X36264)
| ~ ssNder1_7r1r1r1r1r1r1r1(X36272,X36258,X36261,X36262,X36271,X36263,X36264)
| ~ ssNder1_6r1r1r1r1r1r1(X36272,X36258,X36261,X36262,X36271,X36263)
| ~ ssNder1_5r1r1r1r1r1(X36272,X36258,X36261,X36262,X36271)
| ~ ssNder1_4r1r1r1r1(X36272,X36258,X36261,X36262)
| ~ ssNder1_3r1r1r1(X36272,X36258,X36261)
| ~ ssPv19_2r1r1(X36272,X36258)
| ~ ssNder1_2r1r1(X36272,X36258)
| ~ ssNder1_1r1(X36272)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1887,c66]) ).
cnf(c1889,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36288,X36279,X36282,X36293,X36289,X36278,X36277,skc24,X36283,X36285,X36280,X36292,skc23,X36281,X36284)
| ssPv16_5r1r1r1r1r1(X36288,X36279,X36286,X36291,X36276)
| ~ ssPv14_7r1r1r1r1r1r1r1(X36288,X36279,X36286,X36291,X36276,X36290,X36287)
| ~ ssNder1_7r1r1r1r1r1r1r1(X36288,X36279,X36286,X36291,X36276,X36290,X36287)
| ~ ssNder1_6r1r1r1r1r1r1(X36288,X36279,X36286,X36291,X36276,X36290)
| ~ ssNder1_5r1r1r1r1r1(X36288,X36279,X36286,X36291,X36276)
| ~ ssNder1_4r1r1r1r1(X36288,X36279,X36286,X36291)
| ~ ssNder1_3r1r1r1(X36288,X36279,X36286)
| ~ ssPv19_2r1r1(X36288,X36279)
| ~ ssNder1_2r1r1(X36288,X36279)
| ~ ssNder1_1r1(X36288)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1888,c57]) ).
cnf(c1890,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36303,X36309,X36294,X36306,X36311,X36304,X36305,skc24,X36302,X36296,X36299,X36308,skc23,X36298,X36300)
| ssPv16_5r1r1r1r1r1(X36303,X36309,X36310,X36307,X36295)
| ~ ssPv14_7r1r1r1r1r1r1r1(X36303,X36309,X36310,X36307,X36295,X36297,X36301)
| ~ ssNder1_6r1r1r1r1r1r1(X36303,X36309,X36310,X36307,X36295,X36297)
| ~ ssNder1_5r1r1r1r1r1(X36303,X36309,X36310,X36307,X36295)
| ~ ssNder1_4r1r1r1r1(X36303,X36309,X36310,X36307)
| ~ ssNder1_3r1r1r1(X36303,X36309,X36310)
| ~ ssPv19_2r1r1(X36303,X36309)
| ~ ssNder1_2r1r1(X36303,X36309)
| ~ ssNder1_1r1(X36303)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1889,c43]) ).
cnf(c1891,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36318,X36328,X36312,X36322,X36315,X36316,X36321,skc24,X36317,X36313,X36324,X36323,skc23,X36327,X36319)
| ssPv16_5r1r1r1r1r1(X36318,X36328,X36325,X36314,X36320)
| ~ ssNder1_6r1r1r1r1r1r1(X36318,X36328,X36325,X36314,X36320,X36326)
| ~ ssNder1_5r1r1r1r1r1(X36318,X36328,X36325,X36314,X36320)
| ~ ssNder1_4r1r1r1r1(X36318,X36328,X36325,X36314)
| ~ ssNder1_3r1r1r1(X36318,X36328,X36325)
| ~ ssPv19_2r1r1(X36318,X36328)
| ~ ssNder1_2r1r1(X36318,X36328)
| ~ ssNder1_1r1(X36318)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1890,c36]) ).
cnf(c1892,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36333,X36344,X36330,X36331,X36339,X36340,X36335,skc24,X36332,X36336,X36342,X36337,skc23,X36341,X36343)
| ssPv16_5r1r1r1r1r1(X36333,X36344,X36329,X36334,X36338)
| ~ ssNder1_5r1r1r1r1r1(X36333,X36344,X36329,X36334,X36338)
| ~ ssNder1_4r1r1r1r1(X36333,X36344,X36329,X36334)
| ~ ssNder1_3r1r1r1(X36333,X36344,X36329)
| ~ ssPv19_2r1r1(X36333,X36344)
| ~ ssNder1_2r1r1(X36333,X36344)
| ~ ssNder1_1r1(X36333)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1891,c30]) ).
cnf(c1893,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36383,X36378,X36384,X36377,X36381,X36389,X36379,skc24,X36390,X36388,X36376,X36382,skc23,X36391,X36385)
| ssPv16_5r1r1r1r1r1(X36383,X36378,X36380,X36386,X36387)
| ~ ssNder1_4r1r1r1r1(X36383,X36378,X36380,X36386)
| ~ ssNder1_3r1r1r1(X36383,X36378,X36380)
| ~ ssPv19_2r1r1(X36383,X36378)
| ~ ssNder1_2r1r1(X36383,X36378)
| ~ ssNder1_1r1(X36383)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1892,c19]) ).
cnf(c1894,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36402,X36399,X36392,X36395,X36403,X36401,X36393,skc24,X36405,X36396,X36404,X36400,skc23,X36397,X36407)
| ssPv16_5r1r1r1r1r1(X36402,X36399,X36406,X36398,X36394)
| ~ ssNder1_3r1r1r1(X36402,X36399,X36406)
| ~ ssPv19_2r1r1(X36402,X36399)
| ~ ssNder1_2r1r1(X36402,X36399)
| ~ ssNder1_1r1(X36402)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1893,c10]) ).
cnf(c1895,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36410,X36418,X36409,X36415,X36411,X36416,X36423,skc24,X36422,X36417,X36414,X36421,skc23,X36419,X36420)
| ssPv16_5r1r1r1r1r1(X36410,X36418,X36408,X36412,X36413)
| ~ ssPv19_2r1r1(X36410,X36418)
| ~ ssNder1_2r1r1(X36410,X36418)
| ~ ssNder1_1r1(X36410)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1894,c5]) ).
cnf(c1896,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36426,X36433,X36432,X36437,X36439,X36430,X36425,skc24,X36435,X36424,X36434,X36428,skc23,X36431,X36436)
| ssPv16_5r1r1r1r1r1(X36426,X36433,X36429,X36438,X36427)
| ~ ssPv19_2r1r1(X36426,X36433)
| ~ ssNder1_1r1(X36426)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1895,c2]) ).
cnf(c1898,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36450,X36456,X36459,X36466,X36458,X36455,X36451,skc24,X36446,X36464,X36447,X36457,skc23,X36460,X36441)
| ssPv16_5r1r1r1r1r1(X36450,X36456,X36462,X36442,X36463)
| ~ ssNder1_1r1(X36450)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36450,X36456,X36445,X36440,X36452,X36453,X36449,skc24,X36444,X36448,X36443,X36454,skc23,X36461,X36465) ),
inference(resolution,[status(thm)],[c1896,c1866]) ).
cnf(c1900,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36504,X36520,X36516,X36500,X36502,X36522,X36525,skc24,X36511,X36523,X36506,X36510,skc23,X36513,X36519)
| ssPv16_5r1r1r1r1r1(X36504,X36520,X36512,X36524,X36521)
| ~ ssNder1_0
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36504,X36520,X36515,X36509,X36507,X36514,X36501,skc24,X36503,X36517,X36518,X36526,skc23,X36508,X36505) ),
inference(resolution,[status(thm)],[c1898,c0]) ).
cnf(c1901,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36549,X36538,X36540,X36529,X36533,X36550,X36547,skc24,X36537,X36531,X36530,X36532,skc23,X36545,X36535)
| ssPv16_5r1r1r1r1r1(X36549,X36538,X36544,X36536,X36542)
| ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36549,X36538,X36551,X36553,X36534,X36528,X36546,skc24,X36543,X36552,X36548,X36527,skc23,X36539,X36541) ),
inference(resolution,[status(thm)],[c1900,clause1]) ).
cnf(c1902,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36554,X36568,X36556,X36564,X36562,X36569,X36565,skc24,X36561,X36563,X36566,X36557,skc23,X36560,X36555)
| ssPv16_5r1r1r1r1r1(X36554,X36568,X36558,X36559,X36567) ),
inference(factor,[status(thm)],[c1901]) ).
cnf(c1907,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36583,X36571,X36572,X36574,X36582,X36581,X36575,skc24,X36570,X36578,X36580,X36573,skc23,X36576,X36579)
| ~ ssNder1_3r1r1r1(X36583,X36571,X36577)
| ~ ssNder1_2r1r1(X36583,X36571)
| ~ ssNder1_1r1(X36583)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1902,clause7]) ).
cnf(c1908,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36591,X36594,X36586,X36585,X36590,X36592,X36596,skc24,X36595,X36588,X36587,X36589,skc23,X36584,X36593)
| ~ ssNder1_2r1r1(X36591,X36594)
| ~ ssNder1_1r1(X36591)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1907,c5]) ).
cnf(c1909,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36635,X36638,X36641,X36639,X36630,X36636,X36633,skc24,X36634,X36637,X36640,X36631,skc23,X36642,X36632)
| ~ ssNder1_1r1(X36635)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1908,c2]) ).
cnf(c1910,plain,
( ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36647,X36651,X36649,X36648,X36655,X36644,X36650,skc24,X36645,X36646,X36652,X36643,skc23,X36653,X36654)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1909,c0]) ).
cnf(c1911,plain,
ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(X36666,X36668,X36659,X36661,X36660,X36665,X36664,skc24,X36667,X36662,X36663,X36656,skc23,X36657,X36658),
inference(resolution,[status(thm)],[c1910,clause1]) ).
cnf(c1912,plain,
( ~ ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(X36806,X36801,X36809,X36807,X36803,X36805,X36810,skc24,X36802,X36808,X36800,X36804,skc23)
| ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X36806,X36801,X36809,X36807,X36803,X36805,X36810,skc24,X36802,X36808,X36800,X36804)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X36806,X36801,X36809,X36807,X36803,X36805,X36810,skc24,X36802,X36808,X36800)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X36806,X36801,X36809,X36807,X36803,X36805,X36810,skc24,X36802,X36808)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X36806,X36801,X36809,X36807,X36803,X36805,X36810,skc24,X36802)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X36806,X36801,X36809,X36807,X36803,X36805,X36810,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X36806,X36801,X36809,X36807,X36803,X36805,X36810)
| ~ ssNder1_6r1r1r1r1r1r1(X36806,X36801,X36809,X36807,X36803,X36805)
| ~ ssNder1_5r1r1r1r1r1(X36806,X36801,X36809,X36807,X36803)
| ~ ssNder1_4r1r1r1r1(X36806,X36801,X36809,X36807)
| ~ ssNder1_3r1r1r1(X36806,X36801,X36809)
| ~ ssNder1_2r1r1(X36806,X36801)
| ~ ssNder1_1r1(X36806)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1911,clause31]) ).
cnf(c1913,plain,
( ~ ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(X36813,X36817,X36815,X36816,X36820,X36811,X36814,skc24,X36818,X36812,X36821,X36819)
| ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X36813,X36817,X36815,X36816,X36820,X36811,X36814,skc24,X36818,X36812,X36821)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X36813,X36817,X36815,X36816,X36820,X36811,X36814,skc24,X36818,X36812)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X36813,X36817,X36815,X36816,X36820,X36811,X36814,skc24,X36818)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X36813,X36817,X36815,X36816,X36820,X36811,X36814,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X36813,X36817,X36815,X36816,X36820,X36811,X36814)
| ~ ssNder1_6r1r1r1r1r1r1(X36813,X36817,X36815,X36816,X36820,X36811)
| ~ ssNder1_5r1r1r1r1r1(X36813,X36817,X36815,X36816,X36820)
| ~ ssNder1_4r1r1r1r1(X36813,X36817,X36815,X36816)
| ~ ssNder1_3r1r1r1(X36813,X36817,X36815)
| ~ ssNder1_2r1r1(X36813,X36817)
| ~ ssNder1_1r1(X36813)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1912,c136]) ).
cnf(c1914,plain,
( ~ ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(X36824,X36822,X36830,X36829,X36823,X36826,X36827,skc24,X36828,X36831,X36825)
| ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X36824,X36822,X36830,X36829,X36823,X36826,X36827,skc24,X36828,X36831)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X36824,X36822,X36830,X36829,X36823,X36826,X36827,skc24,X36828)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X36824,X36822,X36830,X36829,X36823,X36826,X36827,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X36824,X36822,X36830,X36829,X36823,X36826,X36827)
| ~ ssNder1_6r1r1r1r1r1r1(X36824,X36822,X36830,X36829,X36823,X36826)
| ~ ssNder1_5r1r1r1r1r1(X36824,X36822,X36830,X36829,X36823)
| ~ ssNder1_4r1r1r1r1(X36824,X36822,X36830,X36829)
| ~ ssNder1_3r1r1r1(X36824,X36822,X36830)
| ~ ssNder1_2r1r1(X36824,X36822)
| ~ ssNder1_1r1(X36824)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1913,c101]) ).
cnf(c1915,plain,
( ~ ssNder1_10r1r1r1r1r1r1r1r1r1r1(X36870,X36864,X36863,X36862,X36867,X36868,X36869,skc24,X36865,X36866)
| ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X36870,X36864,X36863,X36862,X36867,X36868,X36869,skc24,X36865)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X36870,X36864,X36863,X36862,X36867,X36868,X36869,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X36870,X36864,X36863,X36862,X36867,X36868,X36869)
| ~ ssNder1_6r1r1r1r1r1r1(X36870,X36864,X36863,X36862,X36867,X36868)
| ~ ssNder1_5r1r1r1r1r1(X36870,X36864,X36863,X36862,X36867)
| ~ ssNder1_4r1r1r1r1(X36870,X36864,X36863,X36862)
| ~ ssNder1_3r1r1r1(X36870,X36864,X36863)
| ~ ssNder1_2r1r1(X36870,X36864)
| ~ ssNder1_1r1(X36870)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1914,c88]) ).
cnf(c1916,plain,
( ~ ssNder1_9r1r1r1r1r1r1r1r1r1(X36878,X36875,X36876,X36873,X36877,X36871,X36874,skc24,X36872)
| ~ ssNder1_8r1r1r1r1r1r1r1r1(X36878,X36875,X36876,X36873,X36877,X36871,X36874,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X36878,X36875,X36876,X36873,X36877,X36871,X36874)
| ~ ssNder1_6r1r1r1r1r1r1(X36878,X36875,X36876,X36873,X36877,X36871)
| ~ ssNder1_5r1r1r1r1r1(X36878,X36875,X36876,X36873,X36877)
| ~ ssNder1_4r1r1r1r1(X36878,X36875,X36876,X36873)
| ~ ssNder1_3r1r1r1(X36878,X36875,X36876)
| ~ ssNder1_2r1r1(X36878,X36875)
| ~ ssNder1_1r1(X36878)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1915,c76]) ).
cnf(c1917,plain,
( ~ ssNder1_8r1r1r1r1r1r1r1r1(X36883,X36885,X36881,X36880,X36884,X36879,X36882,skc24)
| ~ ssNder1_7r1r1r1r1r1r1r1(X36883,X36885,X36881,X36880,X36884,X36879,X36882)
| ~ ssNder1_6r1r1r1r1r1r1(X36883,X36885,X36881,X36880,X36884,X36879)
| ~ ssNder1_5r1r1r1r1r1(X36883,X36885,X36881,X36880,X36884)
| ~ ssNder1_4r1r1r1r1(X36883,X36885,X36881,X36880)
| ~ ssNder1_3r1r1r1(X36883,X36885,X36881)
| ~ ssNder1_2r1r1(X36883,X36885)
| ~ ssNder1_1r1(X36883)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1916,c66]) ).
cnf(c1918,plain,
( ~ ssNder1_7r1r1r1r1r1r1r1(X36890,X36887,X36889,X36891,X36886,X36892,X36888)
| ~ ssNder1_6r1r1r1r1r1r1(X36890,X36887,X36889,X36891,X36886,X36892)
| ~ ssNder1_5r1r1r1r1r1(X36890,X36887,X36889,X36891,X36886)
| ~ ssNder1_4r1r1r1r1(X36890,X36887,X36889,X36891)
| ~ ssNder1_3r1r1r1(X36890,X36887,X36889)
| ~ ssNder1_2r1r1(X36890,X36887)
| ~ ssNder1_1r1(X36890)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1917,c57]) ).
cnf(c1919,plain,
( ~ ssNder1_6r1r1r1r1r1r1(X36895,X36896,X36898,X36897,X36893,X36894)
| ~ ssNder1_5r1r1r1r1r1(X36895,X36896,X36898,X36897,X36893)
| ~ ssNder1_4r1r1r1r1(X36895,X36896,X36898,X36897)
| ~ ssNder1_3r1r1r1(X36895,X36896,X36898)
| ~ ssNder1_2r1r1(X36895,X36896)
| ~ ssNder1_1r1(X36895)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1918,c43]) ).
cnf(c1920,plain,
( ~ ssNder1_5r1r1r1r1r1(X36932,X36935,X36931,X36933,X36934)
| ~ ssNder1_4r1r1r1r1(X36932,X36935,X36931,X36933)
| ~ ssNder1_3r1r1r1(X36932,X36935,X36931)
| ~ ssNder1_2r1r1(X36932,X36935)
| ~ ssNder1_1r1(X36932)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1919,c30]) ).
cnf(c1921,plain,
( ~ ssNder1_4r1r1r1r1(X36939,X36938,X36936,X36937)
| ~ ssNder1_3r1r1r1(X36939,X36938,X36936)
| ~ ssNder1_2r1r1(X36939,X36938)
| ~ ssNder1_1r1(X36939)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1920,c19]) ).
cnf(c1922,plain,
( ~ ssNder1_3r1r1r1(X36940,X36942,X36941)
| ~ ssNder1_2r1r1(X36940,X36942)
| ~ ssNder1_1r1(X36940)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1921,c10]) ).
cnf(c1923,plain,
( ~ ssNder1_2r1r1(X36943,X36944)
| ~ ssNder1_1r1(X36943)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1922,c5]) ).
cnf(c1924,plain,
( ~ ssNder1_1r1(X36945)
| ~ ssNder1_0 ),
inference(resolution,[status(thm)],[c1923,c2]) ).
cnf(c1925,plain,
~ ssNder1_0,
inference(resolution,[status(thm)],[c1924,c0]) ).
cnf(c1926,plain,
$false,
inference(resolution,[status(thm)],[c1925,clause1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : SYN869-1 : TPTP v8.1.2. Released v2.5.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n004.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 19:59:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 5.37/5.57 % Version: 1.5
% 5.37/5.57 % SZS status Unsatisfiable
% 5.37/5.57 % SZS output start CNFRefutation
% See solution above
% 5.37/5.59
% 5.37/5.59 % Initial clauses : 56
% 5.37/5.59 % Processed clauses : 1326
% 5.37/5.59 % Factors computed : 44
% 5.37/5.59 % Resolvents computed: 1883
% 5.37/5.59 % Tautologies deleted: 12
% 5.37/5.59 % Forward subsumed : 367
% 5.37/5.59 % Backward subsumed : 1284
% 5.37/5.59 % -------- CPU Time ---------
% 5.37/5.59 % User time : 5.198 s
% 5.37/5.59 % System time : 0.022 s
% 5.37/5.59 % Total time : 5.220 s
%------------------------------------------------------------------------------