%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR049+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:06:52 AM UTC 2026
% Result : Theorem 0.06s 5.46s
% Output : CNFRefutation 0.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 36
% Syntax : Number of formulae : 138 ( 98 unt; 0 def)
% Number of atoms : 184 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 103 ( 57 ~; 37 |; 3 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 33 con; 0-0 aty)
% Number of variables : 52 ( 0 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(just84,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('theBenchmark.p',just84) ).
fof(just85,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('theBenchmark.p',just85) ).
fof(just86,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('theBenchmark.p',just86) ).
fof(just155,axiom,
! [X,Y,Z] :
( ( genls(Y,Z)
& genls(X,Y) )
=> genls(X,Z) ),
file('theBenchmark.p',just155) ).
fof(query49,conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
file('theBenchmark.p',query49) ).
fof(query49_neg,negated_conjecture,
~ ( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(assume_negation,[status(cth)],[query49]) ).
fof(just7,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('theBenchmark.p',just7) ).
cnf(c_167,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(clausify,[status(thm)],[just7]) ).
fof(just9,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('theBenchmark.p',just9) ).
cnf(c_169,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(clausify,[status(thm)],[just9]) ).
fof(just11,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('theBenchmark.p',just11) ).
cnf(c_171,plain,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(clausify,[status(thm)],[just11]) ).
fof(just13,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('theBenchmark.p',just13) ).
cnf(c_173,plain,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(clausify,[status(thm)],[just13]) ).
fof(just15,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('theBenchmark.p',just15) ).
cnf(c_175,plain,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(clausify,[status(thm)],[just15]) ).
fof(just17,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('theBenchmark.p',just17) ).
cnf(c_177,plain,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(clausify,[status(thm)],[just17]) ).
fof(just19,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('theBenchmark.p',just19) ).
cnf(c_179,plain,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(clausify,[status(thm)],[just19]) ).
fof(just21,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('theBenchmark.p',just21) ).
cnf(c_181,plain,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(clausify,[status(thm)],[just21]) ).
fof(just23,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('theBenchmark.p',just23) ).
cnf(c_183,plain,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(clausify,[status(thm)],[just23]) ).
fof(just25,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('theBenchmark.p',just25) ).
cnf(c_185,plain,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(clausify,[status(thm)],[just25]) ).
fof(just27,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('theBenchmark.p',just27) ).
cnf(c_187,plain,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(clausify,[status(thm)],[just27]) ).
fof(just29,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('theBenchmark.p',just29) ).
cnf(c_189,plain,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(clausify,[status(thm)],[just29]) ).
fof(just31,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('theBenchmark.p',just31) ).
cnf(c_191,plain,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(clausify,[status(thm)],[just31]) ).
fof(just33,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('theBenchmark.p',just33) ).
cnf(c_193,plain,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(clausify,[status(thm)],[just33]) ).
fof(just35,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('theBenchmark.p',just35) ).
cnf(c_195,plain,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(clausify,[status(thm)],[just35]) ).
fof(just37,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('theBenchmark.p',just37) ).
cnf(c_197,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[just37]) ).
fof(just39,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('theBenchmark.p',just39) ).
cnf(c_199,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(clausify,[status(thm)],[just39]) ).
fof(just41,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('theBenchmark.p',just41) ).
cnf(c_201,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(clausify,[status(thm)],[just41]) ).
fof(just43,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('theBenchmark.p',just43) ).
cnf(c_203,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(clausify,[status(thm)],[just43]) ).
fof(just45,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('theBenchmark.p',just45) ).
cnf(c_205,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(clausify,[status(thm)],[just45]) ).
fof(just47,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('theBenchmark.p',just47) ).
cnf(c_207,plain,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(clausify,[status(thm)],[just47]) ).
fof(just49,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('theBenchmark.p',just49) ).
cnf(c_209,plain,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(clausify,[status(thm)],[just49]) ).
fof(just51,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('theBenchmark.p',just51) ).
cnf(c_211,plain,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(clausify,[status(thm)],[just51]) ).
fof(just53,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('theBenchmark.p',just53) ).
cnf(c_213,plain,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(clausify,[status(thm)],[just53]) ).
fof(just55,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('theBenchmark.p',just55) ).
cnf(c_215,plain,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(clausify,[status(thm)],[just55]) ).
fof(just57,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('theBenchmark.p',just57) ).
cnf(c_217,plain,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(clausify,[status(thm)],[just57]) ).
fof(just59,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('theBenchmark.p',just59) ).
cnf(c_219,plain,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(clausify,[status(thm)],[just59]) ).
fof(just61,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('theBenchmark.p',just61) ).
cnf(c_221,plain,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(clausify,[status(thm)],[just61]) ).
fof(just63,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('theBenchmark.p',just63) ).
cnf(c_223,plain,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(clausify,[status(thm)],[just63]) ).
fof(just65,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('theBenchmark.p',just65) ).
cnf(c_225,plain,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(clausify,[status(thm)],[just65]) ).
fof(just67,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('theBenchmark.p',just67) ).
cnf(c_227,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[just67]) ).
cnf(c_232,plain,
( disjointwith(B,A)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[just84]) ).
cnf(c_233,plain,
( disjointwith(A,C)
| ~ genls(C,B)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[just85]) ).
cnf(c_234,plain,
( disjointwith(C,B)
| ~ genls(C,A)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[just86]) ).
cnf(c_301,plain,
( genls(A,C)
| ~ genls(B,C)
| ~ genls(A,B) ),
inference(clausify,[status(thm)],[just155]) ).
cnf(c_310,negated_conjecture,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(clausify,[status(thm)],[query49_neg]) ).
cnf(c_345,plain,
~ disjointwith(c_tptpcol_16_92269,c_tptpcol_16_26926),
inference(resolve,[status(thm)],[c_232,c_310]) ).
cnf(c_346,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(resolve,[status(thm)],[c_232,c_227]) ).
cnf(c_1378,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_1_1) ),
inference(resolve,[status(thm)],[c_233,c_346]) ).
cnf(c_369,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2),
inference(resolve,[status(thm)],[c_1378,c_167]) ).
cnf(c_1379,plain,
( disjointwith(A,c_tptpcol_16_26926)
| ~ disjointwith(A,c_tptpcol_15_26925) ),
inference(resolve,[status(thm)],[c_233,c_195]) ).
cnf(c_371,plain,
~ disjointwith(c_tptpcol_16_92269,c_tptpcol_15_26925),
inference(resolve,[status(thm)],[c_1379,c_345]) ).
cnf(c_1380,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_2_2) ),
inference(resolve,[status(thm)],[c_233,c_369]) ).
cnf(c_373,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_3_16386),
inference(resolve,[status(thm)],[c_1380,c_169]) ).
cnf(c_377,plain,
disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536),
inference(resolve,[status(thm)],[c_232,c_373]) ).
cnf(c_383,plain,
~ disjointwith(c_tptpcol_15_26925,c_tptpcol_16_92269),
inference(resolve,[status(thm)],[c_371,c_232]) ).
cnf(c_1381,plain,
( disjointwith(A,c_tptpcol_16_92269)
| ~ disjointwith(A,c_tptpcol_15_92268) ),
inference(resolve,[status(thm)],[c_233,c_225]) ).
cnf(c_387,plain,
~ disjointwith(c_tptpcol_15_26925,c_tptpcol_15_92268),
inference(resolve,[status(thm)],[c_1381,c_383]) ).
cnf(c_1382,plain,
( disjointwith(c_tptpcol_15_26925,A)
| ~ disjointwith(c_tptpcol_14_26921,A) ),
inference(resolve,[status(thm)],[c_234,c_193]) ).
cnf(c_416,plain,
~ disjointwith(c_tptpcol_14_26921,c_tptpcol_15_92268),
inference(resolve,[status(thm)],[c_1382,c_387]) ).
cnf(c_1383,plain,
( disjointwith(A,c_tptpcol_1_65536)
| ~ genls(A,c_tptpcol_3_16386) ),
inference(resolve,[status(thm)],[c_234,c_377]) ).
cnf(c_419,plain,
disjointwith(c_tptpcol_4_24578,c_tptpcol_1_65536),
inference(resolve,[status(thm)],[c_1383,c_171]) ).
cnf(c_1384,plain,
( disjointwith(c_tptpcol_4_24578,A)
| ~ genls(A,c_tptpcol_1_65536) ),
inference(resolve,[status(thm)],[c_233,c_419]) ).
cnf(c_433,plain,
disjointwith(c_tptpcol_4_24578,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1384,c_197]) ).
cnf(c_1385,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_4_24578) ),
inference(resolve,[status(thm)],[c_234,c_433]) ).
cnf(c_450,plain,
disjointwith(c_tptpcol_5_24579,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1385,c_173]) ).
cnf(c_1386,plain,
( disjointwith(A,c_tptpcol_15_92268)
| ~ disjointwith(A,c_tptpcol_14_92264) ),
inference(resolve,[status(thm)],[c_233,c_223]) ).
cnf(c_472,plain,
~ disjointwith(c_tptpcol_14_26921,c_tptpcol_14_92264),
inference(resolve,[status(thm)],[c_1386,c_416]) ).
cnf(c_1387,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_5_24579) ),
inference(resolve,[status(thm)],[c_234,c_450]) ).
cnf(c_479,plain,
disjointwith(c_tptpcol_6_26627,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1387,c_175]) ).
cnf(c_1388,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_6_26627) ),
inference(resolve,[status(thm)],[c_234,c_479]) ).
cnf(c_528,plain,
disjointwith(c_tptpcol_7_26628,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1388,c_177]) ).
cnf(c_1389,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_7_26628) ),
inference(resolve,[status(thm)],[c_234,c_528]) ).
cnf(c_555,plain,
disjointwith(c_tptpcol_8_26629,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1389,c_179]) ).
cnf(c_1390,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_8_26629) ),
inference(resolve,[status(thm)],[c_234,c_555]) ).
cnf(c_585,plain,
disjointwith(c_tptpcol_9_26885,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1390,c_181]) ).
cnf(c_1391,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_9_26885) ),
inference(resolve,[status(thm)],[c_234,c_585]) ).
cnf(c_630,plain,
disjointwith(c_tptpcol_10_26886,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1391,c_183]) ).
cnf(c_1392,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_10_26886) ),
inference(resolve,[status(thm)],[c_234,c_630]) ).
cnf(c_671,plain,
disjointwith(c_tptpcol_11_26887,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1392,c_185]) ).
cnf(c_1393,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_11_26887) ),
inference(resolve,[status(thm)],[c_234,c_671]) ).
cnf(c_685,plain,
disjointwith(c_tptpcol_12_26919,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1393,c_187]) ).
cnf(c_1394,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_12_26919) ),
inference(resolve,[status(thm)],[c_234,c_685]) ).
cnf(c_729,plain,
disjointwith(c_tptpcol_13_26920,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1394,c_189]) ).
cnf(c_1395,plain,
( disjointwith(c_tptpcol_14_26921,A)
| ~ disjointwith(c_tptpcol_13_26920,A) ),
inference(resolve,[status(thm)],[c_234,c_191]) ).
cnf(c_769,plain,
~ disjointwith(c_tptpcol_13_26920,c_tptpcol_14_92264),
inference(resolve,[status(thm)],[c_1395,c_472]) ).
cnf(c_1396,plain,
( disjointwith(c_tptpcol_13_26920,A)
| ~ genls(A,c_tptpcol_2_65537) ),
inference(resolve,[status(thm)],[c_233,c_729]) ).
cnf(c_805,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1396,c_769]) ).
cnf(c_1397,plain,
( genls(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_3_81921) ),
inference(resolve,[status(thm)],[c_301,c_199]) ).
cnf(c_969,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_3_81921),
inference(resolve,[status(thm)],[c_1397,c_805]) ).
cnf(c_1398,plain,
( genls(A,c_tptpcol_3_81921)
| ~ genls(A,c_tptpcol_4_90113) ),
inference(resolve,[status(thm)],[c_301,c_201]) ).
cnf(c_1090,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_4_90113),
inference(resolve,[status(thm)],[c_1398,c_969]) ).
cnf(c_1399,plain,
( genls(A,c_tptpcol_4_90113)
| ~ genls(A,c_tptpcol_5_90114) ),
inference(resolve,[status(thm)],[c_301,c_203]) ).
cnf(c_1240,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_5_90114),
inference(resolve,[status(thm)],[c_1399,c_1090]) ).
cnf(c_1400,plain,
( genls(A,c_tptpcol_5_90114)
| ~ genls(A,c_tptpcol_6_92162) ),
inference(resolve,[status(thm)],[c_301,c_205]) ).
cnf(c_1246,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_6_92162),
inference(resolve,[status(thm)],[c_1400,c_1240]) ).
cnf(c_1401,plain,
( genls(A,c_tptpcol_6_92162)
| ~ genls(A,c_tptpcol_7_92163) ),
inference(resolve,[status(thm)],[c_301,c_207]) ).
cnf(c_1259,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_7_92163),
inference(resolve,[status(thm)],[c_1401,c_1246]) ).
cnf(c_1402,plain,
( genls(A,c_tptpcol_7_92163)
| ~ genls(A,c_tptpcol_8_92164) ),
inference(resolve,[status(thm)],[c_301,c_209]) ).
cnf(c_1266,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_8_92164),
inference(resolve,[status(thm)],[c_1402,c_1259]) ).
cnf(c_1403,plain,
( genls(A,c_tptpcol_8_92164)
| ~ genls(A,c_tptpcol_9_92165) ),
inference(resolve,[status(thm)],[c_301,c_211]) ).
cnf(c_1304,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_9_92165),
inference(resolve,[status(thm)],[c_1403,c_1266]) ).
cnf(c_1404,plain,
( genls(A,c_tptpcol_9_92165)
| ~ genls(A,c_tptpcol_10_92166) ),
inference(resolve,[status(thm)],[c_301,c_213]) ).
cnf(c_1310,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_10_92166),
inference(resolve,[status(thm)],[c_1404,c_1304]) ).
cnf(c_1405,plain,
( genls(A,c_tptpcol_10_92166)
| ~ genls(A,c_tptpcol_11_92230) ),
inference(resolve,[status(thm)],[c_301,c_215]) ).
cnf(c_1319,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_11_92230),
inference(resolve,[status(thm)],[c_1405,c_1310]) ).
cnf(c_1406,plain,
( genls(c_tptpcol_14_92264,A)
| ~ genls(c_tptpcol_13_92263,A) ),
inference(resolve,[status(thm)],[c_301,c_221]) ).
cnf(c_1331,plain,
genls(c_tptpcol_14_92264,c_tptpcol_12_92262),
inference(resolve,[status(thm)],[c_1406,c_219]) ).
cnf(c_1407,plain,
( genls(A,c_tptpcol_11_92230)
| ~ genls(A,c_tptpcol_12_92262) ),
inference(resolve,[status(thm)],[c_301,c_217]) ).
cnf(c_1408,plain,
~ genls(c_tptpcol_14_92264,c_tptpcol_12_92262),
inference(resolve,[status(thm)],[c_1407,c_1319]) ).
cnf(c_1377,plain,
$false,
inference(resolve,[status(thm)],[c_1331,c_1408]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR049+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/5.31 % Computer : n012.cluster.edu
% 0.02/5.31 % Model : x86_64 x86_64
% 0.02/5.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/5.31 % Memory : 8046.5625MB
% 0.02/5.31 % OS : Linux 6.8.0-71-generic
% 0.02/5.31 % CPULimit : 300
% 0.02/5.31 % WCLimit : 300
% 0.02/5.31 % DateTime : Sun Sep 27 00:17:11 UTC 2026
% 0.02/5.31 % CPUTime :
% 0.02/5.31 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/5.31 % Process 1806609 was started by sandbox2 on n012,
% 0.02/5.31 % Sun Sep 27 00:17:11 2026
% 0.02/5.31 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.02/5.33
% 0.02/5.33 % From the command line: assign(max_seconds, 300).
% 0.02/5.33
% 0.02/5.33 % SInE: 153 to sos, 23 to usable, of 176 axioms (tolerance 2.00, depth 0 fixpoint).
% 0.06/5.46
% 0.06/5.46 % given #500 (F,wt=3): 1062 -disjointwith(c_tptpcol_1_1,c_tptpcol_16_92269). [ur(234,b,861,a,c,849,a)].
% 0.06/5.46
% 0.06/5.46 % SZS status Theorem for theBenchmark
% 0.06/5.46
% 0.06/5.46 % Proof 1 at 0.08 (+ 0.04) seconds.
% 0.06/5.46 % Length of proof is 75.
% 0.06/5.46 % Level of proof is 27.
% 0.06/5.46 % Maximum clause weight is 703.000.
% 0.06/5.46 % Given clauses 587.
% 0.06/5.46
% 0.06/5.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------