%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR049+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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 20.16s 3.17s
% Output : CNFRefutation 10.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 34
% Syntax : Number of formulae : 135 ( 94 unt; 0 def)
% Number of atoms : 184 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 154 ( 105 ~; 42 |; 3 &)
% ( 0 <=>; 4 =>; 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 : 54 ( 54 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f79,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f244,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f416,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f460,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f504,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f569,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f593,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f696,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f742,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f867,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1009,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1073,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1145,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1180,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1200,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1248,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1553,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1694,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1715,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1917,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1942,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2008,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2022,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2202,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3013,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3214,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3253,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3436,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3513,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3629,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7585,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7586,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8006,conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8007,negated_conjecture,
~ ( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(negated_conjecture,[status(cth)],[f8006]) ).
fof(f8106,plain,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f8111,plain,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f8330,plain,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f8569,plain,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f8626,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f8689,plain,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(cnf_transformation,[status(thm)],[f504]) ).
fof(f8778,plain,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(cnf_transformation,[status(thm)],[f569]) ).
fof(f8814,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f8961,plain,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(cnf_transformation,[status(thm)],[f696]) ).
fof(f9030,plain,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(cnf_transformation,[status(thm)],[f742]) ).
fof(f9214,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f867]) ).
fof(f9417,plain,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(cnf_transformation,[status(thm)],[f1009]) ).
fof(f9507,plain,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(cnf_transformation,[status(thm)],[f1073]) ).
fof(f9611,plain,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(cnf_transformation,[status(thm)],[f1145]) ).
fof(f9659,plain,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(cnf_transformation,[status(thm)],[f1180]) ).
fof(f9689,plain,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(cnf_transformation,[status(thm)],[f1200]) ).
fof(f9756,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f1248]) ).
fof(f10187,plain,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(cnf_transformation,[status(thm)],[f1553]) ).
fof(f10387,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(cnf_transformation,[status(thm)],[f1694]) ).
fof(f10418,plain,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(cnf_transformation,[status(thm)],[f1715]) ).
fof(f10695,plain,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(cnf_transformation,[status(thm)],[f1917]) ).
fof(f10729,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(cnf_transformation,[status(thm)],[f1942]) ).
fof(f10824,plain,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(cnf_transformation,[status(thm)],[f2008]) ).
fof(f10842,plain,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(cnf_transformation,[status(thm)],[f2022]) ).
fof(f11095,plain,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(cnf_transformation,[status(thm)],[f2202]) ).
fof(f12225,plain,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(cnf_transformation,[status(thm)],[f3013]) ).
fof(f12501,plain,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(cnf_transformation,[status(thm)],[f3214]) ).
fof(f12553,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[status(thm)],[f3253]) ).
fof(f12812,plain,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(cnf_transformation,[status(thm)],[f3436]) ).
fof(f12924,plain,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(cnf_transformation,[status(thm)],[f3513]) ).
fof(f13077,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(cnf_transformation,[status(thm)],[f3629]) ).
fof(f20548,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(pre_NNF_transformation,[status(thm)],[f7585]) ).
fof(f20549,plain,
! [ARG1,NEW] :
( disjointwith(ARG1,NEW)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ) ),
inference(miniscoping,[status(thm)],[f20548]) ).
fof(f20550,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20549]) ).
fof(f20551,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f7586]) ).
fof(f20552,plain,
! [ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ) ),
inference(miniscoping,[status(thm)],[f20551]) ).
fof(f20553,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20552]) ).
fof(f21391,plain,
( ~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)
& mtvisible(c_unitedstatesgeographypeoplemt) ),
inference(pre_NNF_transformation,[status(thm)],[f8007]) ).
fof(f21393,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(cnf_transformation,[status(thm)],[f21391]) ).
fof(f21397,plain,
! [X0] :
( ~ genls(c_tptpcol_16_92269,X0)
| ~ disjointwith(c_tptpcol_16_26926,X0) ),
inference(resolution,[status(thm)],[f20550,f21393]) ).
fof(f21400,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_15_92268),
inference(resolution,[status(thm)],[f21397,f9659]) ).
fof(f21401,plain,
! [X0] :
( ~ genls(c_tptpcol_16_26926,X0)
| ~ disjointwith(X0,c_tptpcol_15_92268) ),
inference(resolution,[status(thm)],[f21400,f20553]) ).
fof(f21416,plain,
~ disjointwith(c_tptpcol_15_26925,c_tptpcol_15_92268),
inference(resolution,[status(thm)],[f21401,f9689]) ).
fof(f21417,plain,
! [X0] :
( ~ genls(c_tptpcol_15_26925,X0)
| ~ disjointwith(X0,c_tptpcol_15_92268) ),
inference(resolution,[status(thm)],[f21416,f20553]) ).
fof(f21428,plain,
~ disjointwith(c_tptpcol_14_26921,c_tptpcol_15_92268),
inference(resolution,[status(thm)],[f8330,f21417]) ).
fof(f21438,plain,
! [X0] :
( ~ genls(c_tptpcol_15_92268,X0)
| ~ disjointwith(c_tptpcol_14_26921,X0) ),
inference(resolution,[status(thm)],[f21428,f20550]) ).
fof(f21559,plain,
~ disjointwith(c_tptpcol_14_26921,c_tptpcol_14_92264),
inference(resolution,[status(thm)],[f10418,f21438]) ).
fof(f21568,plain,
! [X0] :
( ~ genls(c_tptpcol_14_26921,X0)
| ~ disjointwith(X0,c_tptpcol_14_92264) ),
inference(resolution,[status(thm)],[f21559,f20553]) ).
fof(f21641,plain,
~ disjointwith(c_tptpcol_13_26920,c_tptpcol_14_92264),
inference(resolution,[status(thm)],[f10695,f21568]) ).
fof(f21662,plain,
! [X0] :
( ~ genls(c_tptpcol_13_26920,X0)
| ~ disjointwith(X0,c_tptpcol_14_92264) ),
inference(resolution,[status(thm)],[f21641,f20553]) ).
fof(f21704,plain,
~ disjointwith(c_tptpcol_12_26919,c_tptpcol_14_92264),
inference(resolution,[status(thm)],[f21662,f8961]) ).
fof(f21708,plain,
! [X0] :
( ~ genls(c_tptpcol_12_26919,X0)
| ~ disjointwith(X0,c_tptpcol_14_92264) ),
inference(resolution,[status(thm)],[f21704,f20553]) ).
fof(f21740,plain,
~ disjointwith(c_tptpcol_11_26887,c_tptpcol_14_92264),
inference(resolution,[status(thm)],[f21708,f8689]) ).
fof(f21741,plain,
! [X0] :
( ~ genls(c_tptpcol_11_26887,X0)
| ~ disjointwith(X0,c_tptpcol_14_92264) ),
inference(resolution,[status(thm)],[f21740,f20553]) ).
fof(f21826,plain,
~ disjointwith(c_tptpcol_10_26886,c_tptpcol_14_92264),
inference(resolution,[status(thm)],[f21741,f9507]) ).
fof(f21827,plain,
! [X0] :
( ~ genls(c_tptpcol_10_26886,X0)
| ~ disjointwith(X0,c_tptpcol_14_92264) ),
inference(resolution,[status(thm)],[f21826,f20553]) ).
fof(f21856,plain,
~ disjointwith(c_tptpcol_9_26885,c_tptpcol_14_92264),
inference(resolution,[status(thm)],[f21827,f8106]) ).
fof(f21861,plain,
! [X0] :
( ~ genls(c_tptpcol_14_92264,X0)
| ~ disjointwith(c_tptpcol_9_26885,X0) ),
inference(resolution,[status(thm)],[f21856,f20550]) ).
fof(f21882,plain,
~ disjointwith(c_tptpcol_9_26885,c_tptpcol_13_92263),
inference(resolution,[status(thm)],[f21861,f9030]) ).
fof(f21884,plain,
! [X0] :
( ~ genls(c_tptpcol_13_92263,X0)
| ~ disjointwith(c_tptpcol_9_26885,X0) ),
inference(resolution,[status(thm)],[f21882,f20550]) ).
fof(f21902,plain,
~ disjointwith(c_tptpcol_9_26885,c_tptpcol_12_92262),
inference(resolution,[status(thm)],[f21884,f10824]) ).
fof(f21904,plain,
! [X0] :
( ~ genls(c_tptpcol_12_92262,X0)
| ~ disjointwith(c_tptpcol_9_26885,X0) ),
inference(resolution,[status(thm)],[f21902,f20550]) ).
fof(f22154,plain,
~ disjointwith(c_tptpcol_9_26885,c_tptpcol_11_92230),
inference(resolution,[status(thm)],[f12812,f21904]) ).
fof(f22175,plain,
! [X0] :
( ~ genls(c_tptpcol_9_26885,X0)
| ~ disjointwith(X0,c_tptpcol_11_92230) ),
inference(resolution,[status(thm)],[f22154,f20553]) ).
fof(f22309,plain,
~ disjointwith(c_tptpcol_8_26629,c_tptpcol_11_92230),
inference(resolution,[status(thm)],[f12924,f22175]) ).
fof(f22321,plain,
! [X0] :
( ~ genls(c_tptpcol_8_26629,X0)
| ~ disjointwith(X0,c_tptpcol_11_92230) ),
inference(resolution,[status(thm)],[f22309,f20553]) ).
fof(f22510,plain,
~ disjointwith(c_tptpcol_7_26628,c_tptpcol_11_92230),
inference(resolution,[status(thm)],[f22321,f8111]) ).
fof(f22512,plain,
! [X0] :
( ~ genls(c_tptpcol_7_26628,X0)
| ~ disjointwith(X0,c_tptpcol_11_92230) ),
inference(resolution,[status(thm)],[f22510,f20553]) ).
fof(f22890,plain,
~ disjointwith(c_tptpcol_6_26627,c_tptpcol_11_92230),
inference(resolution,[status(thm)],[f22512,f10187]) ).
fof(f22891,plain,
! [X0] :
( ~ genls(c_tptpcol_6_26627,X0)
| ~ disjointwith(X0,c_tptpcol_11_92230) ),
inference(resolution,[status(thm)],[f22890,f20553]) ).
fof(f23177,plain,
~ disjointwith(c_tptpcol_5_24579,c_tptpcol_11_92230),
inference(resolution,[status(thm)],[f22891,f12225]) ).
fof(f23178,plain,
! [X0] :
( ~ genls(c_tptpcol_5_24579,X0)
| ~ disjointwith(X0,c_tptpcol_11_92230) ),
inference(resolution,[status(thm)],[f23177,f20553]) ).
fof(f23384,plain,
~ disjointwith(c_tptpcol_4_24578,c_tptpcol_11_92230),
inference(resolution,[status(thm)],[f23178,f9417]) ).
fof(f23385,plain,
! [X0] :
( ~ genls(c_tptpcol_4_24578,X0)
| ~ disjointwith(X0,c_tptpcol_11_92230) ),
inference(resolution,[status(thm)],[f23384,f20553]) ).
fof(f23579,plain,
~ disjointwith(c_tptpcol_3_16386,c_tptpcol_11_92230),
inference(resolution,[status(thm)],[f23385,f12501]) ).
fof(f23585,plain,
! [X0] :
( ~ genls(c_tptpcol_3_16386,X0)
| ~ disjointwith(X0,c_tptpcol_11_92230) ),
inference(resolution,[status(thm)],[f23579,f20553]) ).
fof(f23824,plain,
~ disjointwith(c_tptpcol_2_2,c_tptpcol_11_92230),
inference(resolution,[status(thm)],[f23585,f8626]) ).
fof(f23825,plain,
! [X0] :
( ~ genls(c_tptpcol_2_2,X0)
| ~ disjointwith(X0,c_tptpcol_11_92230) ),
inference(resolution,[status(thm)],[f23824,f20553]) ).
fof(f24154,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_11_92230),
inference(resolution,[status(thm)],[f23825,f12553]) ).
fof(f24164,plain,
! [X0] :
( ~ genls(c_tptpcol_11_92230,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f24154,f20550]) ).
fof(f24424,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_10_92166),
inference(resolution,[status(thm)],[f24164,f8569]) ).
fof(f24430,plain,
! [X0] :
( ~ genls(c_tptpcol_10_92166,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f24424,f20550]) ).
fof(f24736,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_9_92165),
inference(resolution,[status(thm)],[f24430,f9611]) ).
fof(f24741,plain,
! [X0] :
( ~ genls(c_tptpcol_9_92165,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f24736,f20550]) ).
fof(f25028,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_8_92164),
inference(resolution,[status(thm)],[f24741,f11095]) ).
fof(f25047,plain,
! [X0] :
( ~ genls(c_tptpcol_8_92164,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f25028,f20550]) ).
fof(f25299,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_7_92163),
inference(resolution,[status(thm)],[f25047,f10842]) ).
fof(f25311,plain,
! [X0] :
( ~ genls(c_tptpcol_7_92163,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f25299,f20550]) ).
fof(f25557,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_6_92162),
inference(resolution,[status(thm)],[f25311,f8778]) ).
fof(f25559,plain,
! [X0] :
( ~ genls(c_tptpcol_6_92162,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f25557,f20550]) ).
fof(f25729,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_5_90114),
inference(resolution,[status(thm)],[f25559,f10387]) ).
fof(f25731,plain,
! [X0] :
( ~ genls(c_tptpcol_5_90114,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f25729,f20550]) ).
fof(f25893,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_4_90113),
inference(resolution,[status(thm)],[f25731,f10729]) ).
fof(f25895,plain,
! [X0] :
( ~ genls(c_tptpcol_4_90113,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f25893,f20550]) ).
fof(f26062,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_3_81921),
inference(resolution,[status(thm)],[f25895,f13077]) ).
fof(f26064,plain,
! [X0] :
( ~ genls(c_tptpcol_3_81921,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f26062,f20550]) ).
fof(f26198,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_2_65537),
inference(resolution,[status(thm)],[f26064,f8814]) ).
fof(f26200,plain,
! [X0] :
( ~ genls(c_tptpcol_2_65537,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f26198,f20550]) ).
fof(f26329,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(resolution,[status(thm)],[f26200,f9214]) ).
fof(f26330,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f26329,f9756]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR049+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 14:35:20 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.44 % Drodi V4.1.1
% 20.16/3.17 % Refutation found
% 20.16/3.17 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.16/3.17 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 16.73/4.42 % Elapsed time: 3.836027 seconds
% 16.73/4.42 % CPU time: 21.479107 seconds
% 16.73/4.42 % Total memory used: 603.953 MB
% 16.73/4.42 % Net memory used: 592.071 MB
%------------------------------------------------------------------------------