%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN102-1.007.007 : TPTP v8.1.2. Bugfixed v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:47:23 EDT 2024
% Result : Unsatisfiable 22.64s 22.86s
% Output : Refutation 22.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 35
% Syntax : Number of clauses : 106 ( 36 unt; 0 nHn; 106 RR)
% Number of literals : 263 ( 0 equ; 159 neg)
% Maximal clause size : 8 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 35 ( 34 usr; 1 prp; 0-7 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 252 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(n_s3_type11_21,axiom,
( p_10(X172,X173,X174,X170,X175,X171,X176)
| ~ p_11(X172,X173,X174,X170,X175,X171,X176)
| ~ p_12(X172,X173,X174,X170,X175,X171,X176) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_21) ).
cnf(n_1,axiom,
nq_1(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_1) ).
cnf(n_3,axiom,
nq_2(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_3) ).
cnf(n_5,axiom,
nq_3(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_5) ).
cnf(n_7,axiom,
nq_4(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_7) ).
cnf(n_9,axiom,
nq_5(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_9) ).
cnf(n_11,axiom,
nq_6(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_11) ).
cnf(n_13,axiom,
nq_7(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_13) ).
cnf(n_t3_1,axiom,
( p_12(X368,X369,X370,X366,X371,X367,X372)
| ~ nq_1(X368)
| ~ nq_2(X369)
| ~ nq_3(X370)
| ~ nq_4(X366)
| ~ nq_5(X371)
| ~ nq_6(X367)
| ~ nq_7(X372) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_t3_1) ).
cnf(c0,plain,
( p_12(X378,X375,X374,X373,X377,X376,a)
| ~ nq_1(X378)
| ~ nq_2(X375)
| ~ nq_3(X374)
| ~ nq_4(X373)
| ~ nq_5(X377)
| ~ nq_6(X376) ),
inference(resolution,[status(thm)],[n_t3_1,n_13]) ).
cnf(c2,plain,
( p_12(X381,X382,X383,X379,X380,a,a)
| ~ nq_1(X381)
| ~ nq_2(X382)
| ~ nq_3(X383)
| ~ nq_4(X379)
| ~ nq_5(X380) ),
inference(resolution,[status(thm)],[c0,n_11]) ).
cnf(c4,plain,
( p_12(X384,X387,X385,X386,a,a,a)
| ~ nq_1(X384)
| ~ nq_2(X387)
| ~ nq_3(X385)
| ~ nq_4(X386) ),
inference(resolution,[status(thm)],[c2,n_9]) ).
cnf(c6,plain,
( p_12(X397,X396,X395,a,a,a,a)
| ~ nq_1(X397)
| ~ nq_2(X396)
| ~ nq_3(X395) ),
inference(resolution,[status(thm)],[c4,n_7]) ).
cnf(c10,plain,
( p_12(X398,X399,a,a,a,a,a)
| ~ nq_1(X398)
| ~ nq_2(X399) ),
inference(resolution,[status(thm)],[c6,n_5]) ).
cnf(c12,plain,
( p_12(X400,a,a,a,a,a,a)
| ~ nq_1(X400) ),
inference(resolution,[status(thm)],[c10,n_3]) ).
cnf(c14,plain,
p_12(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c12,n_1]) ).
cnf(c16,plain,
( p_10(a,a,a,a,a,a,a)
| ~ p_11(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c14,n_s3_type11_21]) ).
cnf(n_s3_type11_23,axiom,
( p_11(X186,X187,X188,X184,X189,X185,X190)
| ~ p_12(X186,X187,X188,X184,X189,X185,X190)
| ~ p_13(X186,X187,X188,X184,X189,X185,X190) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_23) ).
cnf(n_t3_2,axiom,
( p_13(X390,X391,X392,X388,X393,X389,X394)
| ~ nq_1(X390)
| ~ nq_2(X391)
| ~ nq_3(X392)
| ~ nq_4(X388)
| ~ nq_5(X393)
| ~ nq_6(X389)
| ~ nq_7(X394) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_t3_2) ).
cnf(c8,plain,
( p_13(X450,X449,X451,X446,X447,X448,a)
| ~ nq_1(X450)
| ~ nq_2(X449)
| ~ nq_3(X451)
| ~ nq_4(X446)
| ~ nq_5(X447)
| ~ nq_6(X448) ),
inference(resolution,[status(thm)],[n_t3_2,n_13]) ).
cnf(c80,plain,
( p_13(X657,X656,X658,X659,X655,a,a)
| ~ nq_1(X657)
| ~ nq_2(X656)
| ~ nq_3(X658)
| ~ nq_4(X659)
| ~ nq_5(X655) ),
inference(resolution,[status(thm)],[c8,n_11]) ).
cnf(c484,plain,
( p_13(X680,X682,X681,X683,a,a,a)
| ~ nq_1(X680)
| ~ nq_2(X682)
| ~ nq_3(X681)
| ~ nq_4(X683) ),
inference(resolution,[status(thm)],[c80,n_9]) ).
cnf(c532,plain,
( p_13(X684,X686,X685,a,a,a,a)
| ~ nq_1(X684)
| ~ nq_2(X686)
| ~ nq_3(X685) ),
inference(resolution,[status(thm)],[c484,n_7]) ).
cnf(c534,plain,
( p_13(X688,X687,a,a,a,a,a)
| ~ nq_1(X688)
| ~ nq_2(X687) ),
inference(resolution,[status(thm)],[c532,n_5]) ).
cnf(c536,plain,
( p_13(X689,a,a,a,a,a,a)
| ~ nq_1(X689) ),
inference(resolution,[status(thm)],[c534,n_3]) ).
cnf(c538,plain,
p_13(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c536,n_1]) ).
cnf(c540,plain,
( p_11(a,a,a,a,a,a,a)
| ~ p_12(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c538,n_s3_type11_23]) ).
cnf(c2040,plain,
p_11(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c540,c14]) ).
cnf(c2042,plain,
p_10(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c2040,c16]) ).
cnf(n_s3_type11_19,axiom,
( p_9(X158,X159,X160,X156,X161,X157,X162)
| ~ p_10(X158,X159,X160,X156,X161,X157,X162)
| ~ p_11(X158,X159,X160,X156,X161,X157,X162) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_19) ).
cnf(c2043,plain,
( p_9(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c2040,n_s3_type11_19]) ).
cnf(c3579,plain,
p_9(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c2043,c2042]) ).
cnf(n_s3_type11_17,axiom,
( p_8(X144,X145,X146,X142,X147,X143,X148)
| ~ p_9(X144,X145,X146,X142,X147,X143,X148)
| ~ p_10(X144,X145,X146,X142,X147,X143,X148) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_17) ).
cnf(c2044,plain,
( p_8(a,a,a,a,a,a,a)
| ~ p_9(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c2042,n_s3_type11_17]) ).
cnf(c3582,plain,
p_8(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c2044,c3579]) ).
cnf(n_s3_type12_15,axiom,
( q_7(X298,X299,X300,X296,X301,X297,X302)
| ~ p_8(X298,X299,X300,X296,X301,X297,X302)
| ~ q_9(X298,X299,X300,X296,X301,X297,X302) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_15) ).
cnf(n_s3_type12_22,axiom,
( q_10(X347,X348,X349,X345,X350,X346,X351)
| ~ q_11(X347,X348,X349,X345,X350,X346,X351)
| ~ p_12(X347,X348,X349,X345,X350,X346,X351) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_22) ).
cnf(c17,plain,
( q_10(a,a,a,a,a,a,a)
| ~ q_11(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c14,n_s3_type12_22]) ).
cnf(n_t3_3,axiom,
( q_12(X403,X404,X405,X401,X406,X402,X407)
| ~ nq_1(X403)
| ~ nq_2(X404)
| ~ nq_3(X405)
| ~ nq_4(X401)
| ~ nq_5(X406)
| ~ nq_6(X402)
| ~ nq_7(X407) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_t3_3) ).
cnf(c20,plain,
( q_12(X483,X480,X482,X485,X484,X481,a)
| ~ nq_1(X483)
| ~ nq_2(X480)
| ~ nq_3(X482)
| ~ nq_4(X485)
| ~ nq_5(X484)
| ~ nq_6(X481) ),
inference(resolution,[status(thm)],[n_t3_3,n_13]) ).
cnf(c144,plain,
( q_12(X833,X831,X829,X832,X830,a,a)
| ~ nq_1(X833)
| ~ nq_2(X831)
| ~ nq_3(X829)
| ~ nq_4(X832)
| ~ nq_5(X830) ),
inference(resolution,[status(thm)],[c20,n_11]) ).
cnf(c852,plain,
( q_12(X920,X918,X919,X921,a,a,a)
| ~ nq_1(X920)
| ~ nq_2(X918)
| ~ nq_3(X919)
| ~ nq_4(X921) ),
inference(resolution,[status(thm)],[c144,n_9]) ).
cnf(c1040,plain,
( q_12(X923,X922,X924,a,a,a,a)
| ~ nq_1(X923)
| ~ nq_2(X922)
| ~ nq_3(X924) ),
inference(resolution,[status(thm)],[c852,n_7]) ).
cnf(c1042,plain,
( q_12(X925,X926,a,a,a,a,a)
| ~ nq_1(X925)
| ~ nq_2(X926) ),
inference(resolution,[status(thm)],[c1040,n_5]) ).
cnf(c1044,plain,
( q_12(X927,a,a,a,a,a,a)
| ~ nq_1(X927) ),
inference(resolution,[status(thm)],[c1042,n_3]) ).
cnf(c1046,plain,
q_12(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c1044,n_1]) ).
cnf(n_s3_type12_24,axiom,
( q_11(X361,X362,X363,X359,X364,X360,X365)
| ~ q_12(X361,X362,X363,X359,X364,X360,X365)
| ~ p_13(X361,X362,X363,X359,X364,X360,X365) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_24) ).
cnf(c541,plain,
( q_11(a,a,a,a,a,a,a)
| ~ q_12(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c538,n_s3_type12_24]) ).
cnf(c2046,plain,
q_11(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c541,c1046]) ).
cnf(c2049,plain,
q_10(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c2046,c17]) ).
cnf(n_s3_type12_20,axiom,
( q_9(X333,X334,X335,X331,X336,X332,X337)
| ~ q_10(X333,X334,X335,X331,X336,X332,X337)
| ~ p_11(X333,X334,X335,X331,X336,X332,X337) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_20) ).
cnf(c2041,plain,
( q_9(a,a,a,a,a,a,a)
| ~ q_10(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c2040,n_s3_type12_20]) ).
cnf(c3576,plain,
q_9(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c2041,c2049]) ).
cnf(c3578,plain,
( q_7(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c3576,n_s3_type12_15]) ).
cnf(c5116,plain,
q_7(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c3578,c3582]) ).
cnf(n_s3_type12_14,axiom,
( q_6(X291,X292,X293,X289,X294,X290,X295)
| ~ q_7(X291,X292,X293,X289,X294,X290,X295)
| ~ p_8(X291,X292,X293,X289,X294,X290,X295) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_14) ).
cnf(c3584,plain,
( q_6(a,a,a,a,a,a,a)
| ~ q_7(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c3582,n_s3_type12_14]) ).
cnf(c5124,plain,
q_6(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c3584,c5116]) ).
cnf(n_s3_type12_12,axiom,
( q_5(X277,X278,X279,X275,X280,X276,X281)
| ~ q_6(X277,X278,X279,X275,X280,X276,X281)
| ~ p_7(X277,X278,X279,X275,X280,X276,X281) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_12) ).
cnf(n_s3_type12_18,axiom,
( q_8(X319,X320,X321,X317,X322,X318,X323)
| ~ q_9(X319,X320,X321,X317,X322,X318,X323)
| ~ p_10(X319,X320,X321,X317,X322,X318,X323) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_18) ).
cnf(c2045,plain,
( q_8(a,a,a,a,a,a,a)
| ~ q_9(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c2042,n_s3_type12_18]) ).
cnf(c3585,plain,
q_8(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c2045,c3576]) ).
cnf(n_s3_type11_16,axiom,
( p_7(X137,X138,X139,X135,X140,X136,X141)
| ~ q_8(X137,X138,X139,X135,X140,X136,X141)
| ~ q_9(X137,X138,X139,X135,X140,X136,X141) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_16) ).
cnf(c3577,plain,
( p_7(a,a,a,a,a,a,a)
| ~ q_8(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c3576,n_s3_type11_16]) ).
cnf(c5112,plain,
p_7(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c3577,c3585]) ).
cnf(c5113,plain,
( q_5(a,a,a,a,a,a,a)
| ~ q_6(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c5112,n_s3_type12_12]) ).
cnf(c7161,plain,
q_5(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c5113,c5124]) ).
cnf(n_s3_type12_10,axiom,
( q_4(X263,X264,X265,X261,X266,X262,X267)
| ~ q_5(X263,X264,X265,X261,X266,X262,X267)
| ~ p_6(X263,X264,X265,X261,X266,X262,X267) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_10) ).
cnf(n_s3_type11_13,axiom,
( p_6(X116,X117,X118,X114,X119,X115,X120)
| ~ p_7(X116,X117,X118,X114,X119,X115,X120)
| ~ p_8(X116,X117,X118,X114,X119,X115,X120) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_13) ).
cnf(c3583,plain,
( p_6(a,a,a,a,a,a,a)
| ~ p_7(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c3582,n_s3_type11_13]) ).
cnf(c5120,plain,
p_6(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c3583,c5112]) ).
cnf(c5122,plain,
( q_4(a,a,a,a,a,a,a)
| ~ q_5(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c5120,n_s3_type12_10]) ).
cnf(c7168,plain,
q_4(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c5122,c7161]) ).
cnf(n_s3_type11_8,axiom,
( p_3(X81,X82,X83,X79,X84,X80,X85)
| ~ q_4(X81,X82,X83,X79,X84,X80,X85)
| ~ q_5(X81,X82,X83,X79,X84,X80,X85) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_8) ).
cnf(c7163,plain,
( p_3(a,a,a,a,a,a,a)
| ~ q_4(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c7161,n_s3_type11_8]) ).
cnf(c8697,plain,
p_3(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c7163,c7168]) ).
cnf(n_s3_type11_5,axiom,
( p_2(X60,X61,X62,X58,X63,X59,X64)
| ~ p_3(X60,X61,X62,X58,X63,X59,X64)
| ~ p_4(X60,X61,X62,X58,X63,X59,X64) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_5) ).
cnf(n_s3_type11_11,axiom,
( p_5(X102,X103,X104,X100,X105,X101,X106)
| ~ p_6(X102,X103,X104,X100,X105,X101,X106)
| ~ p_7(X102,X103,X104,X100,X105,X101,X106) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_11) ).
cnf(c5114,plain,
( p_5(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c5112,n_s3_type11_11]) ).
cnf(c7162,plain,
p_5(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c5114,c5120]) ).
cnf(n_s3_type11_9,axiom,
( p_4(X88,X89,X90,X86,X91,X87,X92)
| ~ p_5(X88,X89,X90,X86,X91,X87,X92)
| ~ p_6(X88,X89,X90,X86,X91,X87,X92) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_9) ).
cnf(c5121,plain,
( p_4(a,a,a,a,a,a,a)
| ~ p_5(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c5120,n_s3_type11_9]) ).
cnf(c7167,plain,
p_4(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c5121,c7162]) ).
cnf(c7169,plain,
( p_2(a,a,a,a,a,a,a)
| ~ p_3(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c7167,n_s3_type11_5]) ).
cnf(c8703,plain,
p_2(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c7169,c8697]) ).
cnf(n_s3_type11_3,axiom,
( p_1(X46,X47,X48,X44,X49,X45,X50)
| ~ p_2(X46,X47,X48,X44,X49,X45,X50)
| ~ p_3(X46,X47,X48,X44,X49,X45,X50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_3) ).
cnf(c8699,plain,
( p_1(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c8697,n_s3_type11_3]) ).
cnf(c10233,plain,
p_1(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c8699,c8703]) ).
cnf(n_s3_type11_1,axiom,
( p_0(X4,X5,X6,X2,X7,X3,X8)
| ~ p_1(X4,X5,X6,X2,X7,X3,X8)
| ~ p_2(X4,X5,X6,X2,X7,X3,X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type11_1) ).
cnf(c8706,plain,
( p_0(a,a,a,a,a,a,a)
| ~ p_1(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c8703,n_s3_type11_1]) ).
cnf(c10236,plain,
p_0(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c8706,c10233]) ).
cnf(n_s3_goal_1,negated_conjecture,
( ~ p_0(a,a,a,a,a,a,a)
| ~ q_0(a,a,a,a,a,a,a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_goal_1) ).
cnf(n_s3_type12_7,axiom,
( q_3(X242,X243,X244,X240,X245,X241,X246)
| ~ p_4(X242,X243,X244,X240,X245,X241,X246)
| ~ q_5(X242,X243,X244,X240,X245,X241,X246) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_7) ).
cnf(c7164,plain,
( q_3(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c7161,n_s3_type12_7]) ).
cnf(c8698,plain,
q_3(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c7164,c7167]) ).
cnf(n_s3_type12_6,axiom,
( q_2(X235,X236,X237,X233,X238,X234,X239)
| ~ q_3(X235,X236,X237,X233,X238,X234,X239)
| ~ p_4(X235,X236,X237,X233,X238,X234,X239) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_6) ).
cnf(c7170,plain,
( q_2(a,a,a,a,a,a,a)
| ~ q_3(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c7167,n_s3_type12_6]) ).
cnf(c8704,plain,
q_2(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c7170,c8698]) ).
cnf(n_s3_type12_4,axiom,
( q_1(X221,X222,X223,X219,X224,X220,X225)
| ~ q_2(X221,X222,X223,X219,X224,X220,X225)
| ~ p_3(X221,X222,X223,X219,X224,X220,X225) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_4) ).
cnf(c8700,plain,
( q_1(a,a,a,a,a,a,a)
| ~ q_2(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c8697,n_s3_type12_4]) ).
cnf(c10234,plain,
q_1(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c8700,c8704]) ).
cnf(n_s3_type12_2,axiom,
( q_0(X207,X208,X209,X205,X210,X206,X211)
| ~ q_1(X207,X208,X209,X205,X210,X206,X211)
| ~ p_2(X207,X208,X209,X205,X210,X206,X211) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_s3_type12_2) ).
cnf(c8705,plain,
( q_0(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(resolution,[status(thm)],[c8703,n_s3_type12_2]) ).
cnf(c10235,plain,
q_0(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c8705,c10234]) ).
cnf(c10237,plain,
~ p_0(a,a,a,a,a,a,a),
inference(resolution,[status(thm)],[c10235,n_s3_goal_1]) ).
cnf(c10238,plain,
$false,
inference(resolution,[status(thm)],[c10237,c10236]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SYN102-1.007.007 : TPTP v8.1.2. Bugfixed v1.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n023.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 20:16:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 22.64/22.86 % Version: 1.5
% 22.64/22.86 % SZS status Unsatisfiable
% 22.64/22.86 % SZS output start CNFRefutation
% See solution above
% 22.64/22.86
% 22.64/22.86 % Initial clauses : 71
% 22.64/22.86 % Processed clauses : 6473
% 22.64/22.86 % Factors computed : 0
% 22.64/22.86 % Resolvents computed: 10239
% 22.64/22.86 % Tautologies deleted: 0
% 22.64/22.86 % Forward subsumed : 2818
% 22.64/22.86 % Backward subsumed : 2566
% 22.64/22.86 % -------- CPU Time ---------
% 22.64/22.86 % User time : 22.473 s
% 22.64/22.86 % System time : 0.030 s
% 22.64/22.86 % Total time : 22.503 s
%------------------------------------------------------------------------------