%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR049+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 : Thu Sep 24 12:13:09 PM UTC 2026
% Result : Theorem 0.13s 5.41s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 35
% Syntax : Number of formulae : 139 ( 94 unt; 0 def)
% Number of atoms : 196 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 108 ( 51 ~; 48 |; 4 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 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 : 66 ( 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f155,axiom,
! [X,Y,Z] :
( ( genls(Y,Z)
& genls(X,Y) )
=> genls(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f177,conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f178,negated_conjecture,
~ ( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(negated_conjecture,[status(cth)],[f177]) ).
fof(f185,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f188,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f191,plain,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f194,plain,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f197,plain,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f200,plain,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f203,plain,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f206,plain,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f209,plain,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f212,plain,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f215,plain,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f218,plain,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f221,plain,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f224,plain,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f227,plain,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f230,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f233,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f236,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f239,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f242,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f245,plain,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f248,plain,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f251,plain,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f254,plain,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f257,plain,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f260,plain,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f263,plain,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f266,plain,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f269,plain,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f272,plain,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f275,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f323,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f324,plain,
! [ARG1,NEW] :
( disjointwith(ARG1,NEW)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ) ),
inference(miniscoping,[status(thm)],[f323]) ).
fof(f325,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f326,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f327,plain,
! [ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ) ),
inference(miniscoping,[status(thm)],[f326]) ).
fof(f328,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f469,plain,
! [X,Y,Z] :
( genls(X,Z)
| ~ genls(Y,Z)
| ~ genls(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f155]) ).
fof(f470,plain,
! [X,Z] :
( genls(X,Z)
| ! [Y] :
( ~ genls(Y,Z)
| ~ genls(X,Y) ) ),
inference(miniscoping,[status(thm)],[f469]) ).
fof(f471,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f470]) ).
fof(f525,plain,
( ~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)
& mtvisible(c_unitedstatesgeographypeoplemt) ),
inference(pre_NNF_transformation,[status(thm)],[f178]) ).
fof(f527,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(cnf_transformation,[status(thm)],[f525]) ).
fof(f528,plain,
! [X0] :
( disjointwith(X0,c_tptpcol_1_65536)
| ~ genls(X0,c_tptpcol_1_1) ),
inference(resolution,[status(thm)],[f275,f328]) ).
fof(f531,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),
inference(resolution,[status(thm)],[f528,f185]) ).
fof(f538,plain,
! [X0] :
( disjointwith(c_tptpcol_2_2,X0)
| ~ genls(X0,c_tptpcol_1_65536) ),
inference(resolution,[status(thm)],[f531,f325]) ).
fof(f558,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_2_65537),
inference(resolution,[status(thm)],[f538,f230]) ).
fof(f561,plain,
! [X0] :
( disjointwith(c_tptpcol_2_2,X0)
| ~ genls(X0,c_tptpcol_2_65537) ),
inference(resolution,[status(thm)],[f558,f325]) ).
fof(f592,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_3_81921),
inference(resolution,[status(thm)],[f561,f233]) ).
fof(f594,plain,
! [X0] :
( disjointwith(c_tptpcol_2_2,X0)
| ~ genls(X0,c_tptpcol_3_81921) ),
inference(resolution,[status(thm)],[f592,f325]) ).
fof(f642,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_4_90113),
inference(resolution,[status(thm)],[f594,f236]) ).
fof(f645,plain,
! [X0] :
( disjointwith(c_tptpcol_2_2,X0)
| ~ genls(X0,c_tptpcol_4_90113) ),
inference(resolution,[status(thm)],[f642,f325]) ).
fof(f698,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_5_90114),
inference(resolution,[status(thm)],[f645,f239]) ).
fof(f701,plain,
! [X0] :
( disjointwith(c_tptpcol_2_2,X0)
| ~ genls(X0,c_tptpcol_5_90114) ),
inference(resolution,[status(thm)],[f698,f325]) ).
fof(f802,plain,
! [X0] :
( genls(X0,c_tptpcol_14_92264)
| ~ genls(X0,c_tptpcol_15_92268) ),
inference(resolution,[status(thm)],[f471,f269]) ).
fof(f803,plain,
! [X0] :
( genls(X0,c_tptpcol_13_92263)
| ~ genls(X0,c_tptpcol_14_92264) ),
inference(resolution,[status(thm)],[f471,f266]) ).
fof(f804,plain,
! [X0] :
( genls(X0,c_tptpcol_12_92262)
| ~ genls(X0,c_tptpcol_13_92263) ),
inference(resolution,[status(thm)],[f471,f263]) ).
fof(f805,plain,
! [X0] :
( genls(X0,c_tptpcol_11_92230)
| ~ genls(X0,c_tptpcol_12_92262) ),
inference(resolution,[status(thm)],[f471,f260]) ).
fof(f806,plain,
! [X0] :
( genls(X0,c_tptpcol_10_92166)
| ~ genls(X0,c_tptpcol_11_92230) ),
inference(resolution,[status(thm)],[f471,f257]) ).
fof(f807,plain,
! [X0] :
( genls(X0,c_tptpcol_9_92165)
| ~ genls(X0,c_tptpcol_10_92166) ),
inference(resolution,[status(thm)],[f471,f254]) ).
fof(f808,plain,
! [X0] :
( genls(X0,c_tptpcol_8_92164)
| ~ genls(X0,c_tptpcol_9_92165) ),
inference(resolution,[status(thm)],[f471,f251]) ).
fof(f809,plain,
! [X0] :
( genls(X0,c_tptpcol_7_92163)
| ~ genls(X0,c_tptpcol_8_92164) ),
inference(resolution,[status(thm)],[f471,f248]) ).
fof(f810,plain,
! [X0] :
( genls(X0,c_tptpcol_6_92162)
| ~ genls(X0,c_tptpcol_7_92163) ),
inference(resolution,[status(thm)],[f471,f245]) ).
fof(f811,plain,
! [X0] :
( genls(X0,c_tptpcol_5_90114)
| ~ genls(X0,c_tptpcol_6_92162) ),
inference(resolution,[status(thm)],[f471,f242]) ).
fof(f816,plain,
! [X0] :
( genls(X0,c_tptpcol_14_26921)
| ~ genls(X0,c_tptpcol_15_26925) ),
inference(resolution,[status(thm)],[f471,f224]) ).
fof(f817,plain,
! [X0] :
( genls(X0,c_tptpcol_13_26920)
| ~ genls(X0,c_tptpcol_14_26921) ),
inference(resolution,[status(thm)],[f471,f221]) ).
fof(f818,plain,
! [X0] :
( genls(X0,c_tptpcol_12_26919)
| ~ genls(X0,c_tptpcol_13_26920) ),
inference(resolution,[status(thm)],[f471,f218]) ).
fof(f819,plain,
! [X0] :
( genls(X0,c_tptpcol_11_26887)
| ~ genls(X0,c_tptpcol_12_26919) ),
inference(resolution,[status(thm)],[f471,f215]) ).
fof(f820,plain,
! [X0] :
( genls(X0,c_tptpcol_10_26886)
| ~ genls(X0,c_tptpcol_11_26887) ),
inference(resolution,[status(thm)],[f471,f212]) ).
fof(f821,plain,
! [X0] :
( genls(X0,c_tptpcol_9_26885)
| ~ genls(X0,c_tptpcol_10_26886) ),
inference(resolution,[status(thm)],[f471,f209]) ).
fof(f822,plain,
! [X0] :
( genls(X0,c_tptpcol_8_26629)
| ~ genls(X0,c_tptpcol_9_26885) ),
inference(resolution,[status(thm)],[f471,f206]) ).
fof(f823,plain,
! [X0] :
( genls(X0,c_tptpcol_7_26628)
| ~ genls(X0,c_tptpcol_8_26629) ),
inference(resolution,[status(thm)],[f471,f203]) ).
fof(f824,plain,
! [X0] :
( genls(X0,c_tptpcol_6_26627)
| ~ genls(X0,c_tptpcol_7_26628) ),
inference(resolution,[status(thm)],[f471,f200]) ).
fof(f825,plain,
! [X0] :
( genls(X0,c_tptpcol_5_24579)
| ~ genls(X0,c_tptpcol_6_26627) ),
inference(resolution,[status(thm)],[f471,f197]) ).
fof(f826,plain,
! [X0] :
( genls(X0,c_tptpcol_4_24578)
| ~ genls(X0,c_tptpcol_5_24579) ),
inference(resolution,[status(thm)],[f471,f194]) ).
fof(f827,plain,
! [X0] :
( genls(X0,c_tptpcol_3_16386)
| ~ genls(X0,c_tptpcol_4_24578) ),
inference(resolution,[status(thm)],[f471,f191]) ).
fof(f828,plain,
! [X0] :
( genls(X0,c_tptpcol_2_2)
| ~ genls(X0,c_tptpcol_3_16386) ),
inference(resolution,[status(thm)],[f471,f188]) ).
fof(f1078,plain,
genls(c_tptpcol_16_92269,c_tptpcol_14_92264),
inference(resolution,[status(thm)],[f802,f272]) ).
fof(f1110,plain,
genls(c_tptpcol_16_92269,c_tptpcol_13_92263),
inference(resolution,[status(thm)],[f803,f1078]) ).
fof(f1115,plain,
genls(c_tptpcol_16_92269,c_tptpcol_12_92262),
inference(resolution,[status(thm)],[f1110,f804]) ).
fof(f1119,plain,
genls(c_tptpcol_16_92269,c_tptpcol_11_92230),
inference(resolution,[status(thm)],[f1115,f805]) ).
fof(f1147,plain,
genls(c_tptpcol_16_92269,c_tptpcol_10_92166),
inference(resolution,[status(thm)],[f806,f1119]) ).
fof(f1152,plain,
genls(c_tptpcol_16_92269,c_tptpcol_9_92165),
inference(resolution,[status(thm)],[f1147,f807]) ).
fof(f1157,plain,
genls(c_tptpcol_16_92269,c_tptpcol_8_92164),
inference(resolution,[status(thm)],[f1152,f808]) ).
fof(f1204,plain,
genls(c_tptpcol_16_92269,c_tptpcol_7_92163),
inference(resolution,[status(thm)],[f809,f1157]) ).
fof(f1209,plain,
genls(c_tptpcol_16_92269,c_tptpcol_6_92162),
inference(resolution,[status(thm)],[f1204,f810]) ).
fof(f1214,plain,
genls(c_tptpcol_16_92269,c_tptpcol_5_90114),
inference(resolution,[status(thm)],[f1209,f811]) ).
fof(f1222,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_16_92269),
inference(resolution,[status(thm)],[f1214,f701]) ).
fof(f1268,plain,
! [X0] :
( disjointwith(X0,c_tptpcol_16_92269)
| ~ genls(X0,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[f1222,f328]) ).
fof(f1284,plain,
genls(c_tptpcol_16_26926,c_tptpcol_14_26921),
inference(resolution,[status(thm)],[f816,f227]) ).
fof(f1298,plain,
genls(c_tptpcol_16_26926,c_tptpcol_13_26920),
inference(resolution,[status(thm)],[f1284,f817]) ).
fof(f1337,plain,
genls(c_tptpcol_16_26926,c_tptpcol_12_26919),
inference(resolution,[status(thm)],[f818,f1298]) ).
fof(f1368,plain,
genls(c_tptpcol_16_26926,c_tptpcol_11_26887),
inference(resolution,[status(thm)],[f1337,f819]) ).
fof(f1372,plain,
genls(c_tptpcol_16_26926,c_tptpcol_10_26886),
inference(resolution,[status(thm)],[f1368,f820]) ).
fof(f1434,plain,
genls(c_tptpcol_16_26926,c_tptpcol_9_26885),
inference(resolution,[status(thm)],[f1372,f821]) ).
fof(f1493,plain,
genls(c_tptpcol_16_26926,c_tptpcol_8_26629),
inference(resolution,[status(thm)],[f1434,f822]) ).
fof(f1508,plain,
genls(c_tptpcol_16_26926,c_tptpcol_7_26628),
inference(resolution,[status(thm)],[f1493,f823]) ).
fof(f1547,plain,
genls(c_tptpcol_16_26926,c_tptpcol_6_26627),
inference(resolution,[status(thm)],[f1508,f824]) ).
fof(f1553,plain,
genls(c_tptpcol_16_26926,c_tptpcol_5_24579),
inference(resolution,[status(thm)],[f1547,f825]) ).
fof(f1588,plain,
genls(c_tptpcol_16_26926,c_tptpcol_4_24578),
inference(resolution,[status(thm)],[f1553,f826]) ).
fof(f1608,plain,
genls(c_tptpcol_16_26926,c_tptpcol_3_16386),
inference(resolution,[status(thm)],[f1588,f827]) ).
fof(f1701,plain,
genls(c_tptpcol_16_26926,c_tptpcol_2_2),
inference(resolution,[status(thm)],[f1608,f828]) ).
fof(f1942,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(resolution,[status(thm)],[f1701,f1268]) ).
fof(f1958,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1942,f527]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR049+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/5.35 % Computer : n014.cluster.edu
% 0.08/5.35 % Model : x86_64 x86_64
% 0.08/5.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.35 % Memory : 8046.5625MB
% 0.08/5.35 % OS : Linux 6.8.0-71-generic
% 0.08/5.35 % CPULimit : 300
% 0.08/5.35 % WCLimit : 300
% 0.08/5.35 % DateTime : Mon Sep 21 14:34:40 UTC 2026
% 0.08/5.36 % CPUTime :
% 0.08/5.37 % Drodi V4.1.1
% 0.13/5.41 % Refutation found
% 0.13/5.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/5.43 % Elapsed time: 0.066841 seconds
% 0.13/5.43 % CPU time: 0.330565 seconds
% 0.13/5.43 % Total memory used: 66.756 MB
% 0.13/5.43 % Net memory used: 66.552 MB
%------------------------------------------------------------------------------