%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR039+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:02 PM UTC 2026
% Result : Theorem 5.96s 16.39s
% Output : CNFRefutation 6.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 31
% Syntax : Number of formulae : 123 ( 83 unt; 0 def)
% Number of atoms : 171 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 144 ( 96 ~; 40 |; 3 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 30 con; 0-2 aty)
% Number of variables : 56 ( 56 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f276,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f281,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f460,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f481,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f537,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f539,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f593,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f635,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f661,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f668,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f740,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f783,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f867,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f910,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1248,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1694,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1859,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1942,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2137,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2210,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2762,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2958,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2964,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3253,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3301,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3518,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3629,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7584,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7585,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7586,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8006,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8007,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
inference(negated_conjecture,[status(cth)],[f8006]) ).
fof(f8378,plain,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f8384,plain,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f8626,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f8656,plain,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
inference(cnf_transformation,[status(thm)],[f481]) ).
fof(f8736,plain,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
inference(cnf_transformation,[status(thm)],[f537]) ).
fof(f8739,plain,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
inference(cnf_transformation,[status(thm)],[f539]) ).
fof(f8814,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f8876,plain,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
inference(cnf_transformation,[status(thm)],[f635]) ).
fof(f8911,plain,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
inference(cnf_transformation,[status(thm)],[f661]) ).
fof(f8921,plain,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
inference(cnf_transformation,[status(thm)],[f668]) ).
fof(f9027,plain,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
inference(cnf_transformation,[status(thm)],[f740]) ).
fof(f9088,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[status(thm)],[f783]) ).
fof(f9214,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f867]) ).
fof(f9277,plain,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
inference(cnf_transformation,[status(thm)],[f910]) ).
fof(f9756,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f1248]) ).
fof(f10387,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(cnf_transformation,[status(thm)],[f1694]) ).
fof(f10615,plain,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
inference(cnf_transformation,[status(thm)],[f1859]) ).
fof(f10729,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(cnf_transformation,[status(thm)],[f1942]) ).
fof(f11006,plain,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
inference(cnf_transformation,[status(thm)],[f2137]) ).
fof(f11106,plain,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
inference(cnf_transformation,[status(thm)],[f2210]) ).
fof(f11877,plain,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
inference(cnf_transformation,[status(thm)],[f2762]) ).
fof(f12148,plain,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
inference(cnf_transformation,[status(thm)],[f2958]) ).
fof(f12156,plain,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
inference(cnf_transformation,[status(thm)],[f2964]) ).
fof(f12553,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[status(thm)],[f3253]) ).
fof(f12617,plain,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
inference(cnf_transformation,[status(thm)],[f3301]) ).
fof(f12931,plain,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
inference(cnf_transformation,[status(thm)],[f3518]) ).
fof(f13077,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(cnf_transformation,[status(thm)],[f3629]) ).
fof(f20546,plain,
! [X,Y] :
( disjointwith(Y,X)
| ~ disjointwith(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f7584]) ).
fof(f20547,plain,
! [X0,X1] :
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20546]) ).
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_15_93775,c_tptpcol_13_18664)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7)) ),
inference(pre_NNF_transformation,[status(thm)],[f8007]) ).
fof(f21393,plain,
~ disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),
inference(cnf_transformation,[status(thm)],[f21391]) ).
fof(f21397,plain,
! [X0] :
( ~ genls(c_tptpcol_13_18664,X0)
| ~ disjointwith(c_tptpcol_15_93775,X0) ),
inference(resolution,[status(thm)],[f20550,f21393]) ).
fof(f21400,plain,
~ disjointwith(c_tptpcol_15_93775,c_tptpcol_12_18663),
inference(resolution,[status(thm)],[f21397,f11006]) ).
fof(f21401,plain,
! [X0] :
( ~ genls(c_tptpcol_15_93775,X0)
| ~ disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[status(thm)],[f21400,f20553]) ).
fof(f21416,plain,
~ disjointwith(c_tptpcol_14_93774,c_tptpcol_12_18663),
inference(resolution,[status(thm)],[f21401,f11877]) ).
fof(f21418,plain,
! [X0] :
( ~ genls(c_tptpcol_12_18663,X0)
| ~ disjointwith(c_tptpcol_14_93774,X0) ),
inference(resolution,[status(thm)],[f21416,f20550]) ).
fof(f21444,plain,
~ disjointwith(c_tptpcol_14_93774,c_tptpcol_11_18631),
inference(resolution,[status(thm)],[f8921,f21418]) ).
fof(f21456,plain,
! [X0] :
( ~ genls(c_tptpcol_14_93774,X0)
| ~ disjointwith(X0,c_tptpcol_11_18631) ),
inference(resolution,[status(thm)],[f21444,f20553]) ).
fof(f21608,plain,
~ disjointwith(c_tptpcol_13_93766,c_tptpcol_11_18631),
inference(resolution,[status(thm)],[f11106,f21456]) ).
fof(f21614,plain,
! [X0] :
( ~ genls(c_tptpcol_13_93766,X0)
| ~ disjointwith(X0,c_tptpcol_11_18631) ),
inference(resolution,[status(thm)],[f21608,f20553]) ).
fof(f21643,plain,
~ disjointwith(c_tptpcol_12_93765,c_tptpcol_11_18631),
inference(resolution,[status(thm)],[f21614,f8911]) ).
fof(f21644,plain,
! [X0] :
( ~ genls(c_tptpcol_12_93765,X0)
| ~ disjointwith(X0,c_tptpcol_11_18631) ),
inference(resolution,[status(thm)],[f21643,f20553]) ).
fof(f21680,plain,
~ disjointwith(c_tptpcol_11_93764,c_tptpcol_11_18631),
inference(resolution,[status(thm)],[f21644,f8739]) ).
fof(f21683,plain,
! [X0] :
( ~ genls(c_tptpcol_11_93764,X0)
| ~ disjointwith(X0,c_tptpcol_11_18631) ),
inference(resolution,[status(thm)],[f21680,f20553]) ).
fof(f21719,plain,
~ disjointwith(c_tptpcol_10_93700,c_tptpcol_11_18631),
inference(resolution,[status(thm)],[f21683,f8876]) ).
fof(f21722,plain,
! [X0] :
( ~ genls(c_tptpcol_10_93700,X0)
| ~ disjointwith(X0,c_tptpcol_11_18631) ),
inference(resolution,[status(thm)],[f21719,f20553]) ).
fof(f21811,plain,
~ disjointwith(c_tptpcol_9_93699,c_tptpcol_11_18631),
inference(resolution,[status(thm)],[f12148,f21722]) ).
fof(f21823,plain,
! [X0] :
( ~ genls(c_tptpcol_11_18631,X0)
| ~ disjointwith(c_tptpcol_9_93699,X0) ),
inference(resolution,[status(thm)],[f21811,f20550]) ).
fof(f22085,plain,
~ disjointwith(c_tptpcol_9_93699,c_tptpcol_10_18567),
inference(resolution,[status(thm)],[f12617,f21823]) ).
fof(f22151,plain,
! [X0] :
( ~ genls(c_tptpcol_10_18567,X0)
| ~ disjointwith(c_tptpcol_9_93699,X0) ),
inference(resolution,[status(thm)],[f22085,f20550]) ).
fof(f22298,plain,
~ disjointwith(c_tptpcol_9_93699,c_tptpcol_9_18439),
inference(resolution,[status(thm)],[f22151,f9027]) ).
fof(f22300,plain,
! [X0] :
( ~ genls(c_tptpcol_9_18439,X0)
| ~ disjointwith(c_tptpcol_9_93699,X0) ),
inference(resolution,[status(thm)],[f22298,f20550]) ).
fof(f22499,plain,
~ disjointwith(c_tptpcol_9_93699,c_tptpcol_8_18438),
inference(resolution,[status(thm)],[f22300,f12931]) ).
fof(f22502,plain,
! [X0] :
( ~ genls(c_tptpcol_8_18438,X0)
| ~ disjointwith(c_tptpcol_9_93699,X0) ),
inference(resolution,[status(thm)],[f22499,f20550]) ).
fof(f22813,plain,
~ disjointwith(c_tptpcol_9_93699,c_tptpcol_7_18437),
inference(resolution,[status(thm)],[f22502,f10615]) ).
fof(f22817,plain,
! [X0] :
( ~ genls(c_tptpcol_7_18437,X0)
| ~ disjointwith(c_tptpcol_9_93699,X0) ),
inference(resolution,[status(thm)],[f22813,f20550]) ).
fof(f22912,plain,
~ disjointwith(c_tptpcol_9_93699,c_tptpcol_6_18436),
inference(resolution,[status(thm)],[f22817,f8378]) ).
fof(f22913,plain,
! [X0] :
( ~ genls(c_tptpcol_9_93699,X0)
| ~ disjointwith(X0,c_tptpcol_6_18436) ),
inference(resolution,[status(thm)],[f22912,f20553]) ).
fof(f23043,plain,
~ disjointwith(c_tptpcol_8_93698,c_tptpcol_6_18436),
inference(resolution,[status(thm)],[f22913,f8384]) ).
fof(f23045,plain,
! [X0] :
( ~ genls(c_tptpcol_6_18436,X0)
| ~ disjointwith(c_tptpcol_8_93698,X0) ),
inference(resolution,[status(thm)],[f23043,f20550]) ).
fof(f23166,plain,
~ disjointwith(c_tptpcol_8_93698,c_tptpcol_5_16388),
inference(resolution,[status(thm)],[f23045,f8656]) ).
fof(f23172,plain,
! [X0] :
( ~ genls(c_tptpcol_5_16388,X0)
| ~ disjointwith(c_tptpcol_8_93698,X0) ),
inference(resolution,[status(thm)],[f23166,f20550]) ).
fof(f23332,plain,
~ disjointwith(c_tptpcol_8_93698,c_tptpcol_4_16387),
inference(resolution,[status(thm)],[f23172,f9277]) ).
fof(f23334,plain,
! [X0] :
( ~ genls(c_tptpcol_8_93698,X0)
| ~ disjointwith(X0,c_tptpcol_4_16387) ),
inference(resolution,[status(thm)],[f23332,f20553]) ).
fof(f23504,plain,
~ disjointwith(c_tptpcol_7_93186,c_tptpcol_4_16387),
inference(resolution,[status(thm)],[f23334,f12156]) ).
fof(f23513,plain,
! [X0] :
( ~ genls(c_tptpcol_4_16387,X0)
| ~ disjointwith(c_tptpcol_7_93186,X0) ),
inference(resolution,[status(thm)],[f23504,f20550]) ).
fof(f23724,plain,
~ disjointwith(c_tptpcol_7_93186,c_tptpcol_3_16386),
inference(resolution,[status(thm)],[f23513,f9088]) ).
fof(f23736,plain,
! [X0] :
( ~ genls(c_tptpcol_7_93186,X0)
| ~ disjointwith(X0,c_tptpcol_3_16386) ),
inference(resolution,[status(thm)],[f23724,f20553]) ).
fof(f23975,plain,
~ disjointwith(c_tptpcol_6_92162,c_tptpcol_3_16386),
inference(resolution,[status(thm)],[f23736,f8736]) ).
fof(f23982,plain,
! [X0] :
( ~ genls(c_tptpcol_3_16386,X0)
| ~ disjointwith(c_tptpcol_6_92162,X0) ),
inference(resolution,[status(thm)],[f23975,f20550]) ).
fof(f24228,plain,
~ disjointwith(c_tptpcol_6_92162,c_tptpcol_2_2),
inference(resolution,[status(thm)],[f23982,f8626]) ).
fof(f24233,plain,
! [X0] :
( ~ genls(c_tptpcol_6_92162,X0)
| ~ disjointwith(X0,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[f24228,f20553]) ).
fof(f24437,plain,
~ disjointwith(c_tptpcol_5_90114,c_tptpcol_2_2),
inference(resolution,[status(thm)],[f24233,f10387]) ).
fof(f24439,plain,
! [X0] :
( ~ genls(c_tptpcol_5_90114,X0)
| ~ disjointwith(X0,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[f24437,f20553]) ).
fof(f24585,plain,
~ disjointwith(c_tptpcol_4_90113,c_tptpcol_2_2),
inference(resolution,[status(thm)],[f24439,f10729]) ).
fof(f24586,plain,
! [X0] :
( ~ genls(c_tptpcol_4_90113,X0)
| ~ disjointwith(X0,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[f24585,f20553]) ).
fof(f24775,plain,
~ disjointwith(c_tptpcol_3_81921,c_tptpcol_2_2),
inference(resolution,[status(thm)],[f24586,f13077]) ).
fof(f24788,plain,
! [X0] :
( ~ genls(c_tptpcol_3_81921,X0)
| ~ disjointwith(X0,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[f24775,f20553]) ).
fof(f24984,plain,
~ disjointwith(c_tptpcol_2_65537,c_tptpcol_2_2),
inference(resolution,[status(thm)],[f24788,f8814]) ).
fof(f24992,plain,
! [X0] :
( ~ genls(c_tptpcol_2_65537,X0)
| ~ disjointwith(X0,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[f24984,f20553]) ).
fof(f25168,plain,
~ disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2),
inference(resolution,[status(thm)],[f24992,f9214]) ).
fof(f25173,plain,
! [X0] :
( ~ genls(c_tptpcol_2_2,X0)
| ~ disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[status(thm)],[f25168,f20550]) ).
fof(f25343,plain,
~ disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(resolution,[status(thm)],[f25173,f12553]) ).
fof(f25358,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(resolution,[status(thm)],[f25343,f20547]) ).
fof(f25359,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f25358,f9756]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR039+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/15.38 % Computer : n008.cluster.edu
% 0.10/15.38 % Model : x86_64 x86_64
% 0.10/15.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/15.38 % Memory : 8046.5625MB
% 0.10/15.38 % OS : Linux 6.8.0-71-generic
% 0.10/15.38 % CPULimit : 300
% 0.10/15.38 % WCLimit : 300
% 0.10/15.38 % DateTime : Mon Sep 21 14:31:41 UTC 2026
% 0.10/15.38 % CPUTime :
% 0.13/15.56 % Drodi V4.1.1
% 5.96/16.39 % Refutation found
% 5.96/16.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.96/16.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.96/17.65 % Elapsed time: 2.037798 seconds
% 6.96/17.65 % CPU time: 6.835780 seconds
% 6.96/17.65 % Total memory used: 462.258 MB
% 6.96/17.65 % Net memory used: 460.120 MB
%------------------------------------------------------------------------------