%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR039+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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 13.41s 2.22s
% Output : CNFRefutation 14.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 32
% Syntax : Number of formulae : 127 ( 83 unt; 0 def)
% Number of atoms : 183 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 136 ( 80 ~; 46 |; 4 &)
% ( 0 <=>; 6 =>; 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 : 68 ( 68 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f14,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f208,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f255,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f285,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f345,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f348,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f351,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f353,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f370,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f372,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f376,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f379,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f385,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f417,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f476,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f483,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1109,axiom,
! [X,Y,Z] :
( ( genls(Y,Z)
& genls(X,Y) )
=> genls(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1120,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1121,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1122,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1132,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f1133,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)],[f1132]) ).
fof(f1154,plain,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f1167,plain,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f1194,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f1197,plain,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f1237,plain,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f1246,plain,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f1292,plain,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f1343,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f1353,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f1389,plain,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f1399,plain,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f1413,plain,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f1438,plain,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f1505,plain,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f1548,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f1636,plain,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
inference(cnf_transformation,[status(thm)],[f345]) ).
fof(f1640,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f1644,plain,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
inference(cnf_transformation,[status(thm)],[f351]) ).
fof(f1647,plain,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
inference(cnf_transformation,[status(thm)],[f353]) ).
fof(f1672,plain,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f1675,plain,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f1681,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f1685,plain,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f1694,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f1741,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f1829,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(cnf_transformation,[status(thm)],[f476]) ).
fof(f1840,plain,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
inference(cnf_transformation,[status(thm)],[f483]) ).
fof(f3146,plain,
! [X,Y,Z] :
( genls(X,Z)
| ~ genls(Y,Z)
| ~ genls(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1109]) ).
fof(f3147,plain,
! [X,Z] :
( genls(X,Z)
| ! [Y] :
( ~ genls(Y,Z)
| ~ genls(X,Y) ) ),
inference(miniscoping,[status(thm)],[f3146]) ).
fof(f3148,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3147]) ).
fof(f3173,plain,
! [X,Y] :
( disjointwith(Y,X)
| ~ disjointwith(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1120]) ).
fof(f3174,plain,
! [X0,X1] :
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3173]) ).
fof(f3175,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(pre_NNF_transformation,[status(thm)],[f1121]) ).
fof(f3176,plain,
! [ARG1,NEW] :
( disjointwith(ARG1,NEW)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ) ),
inference(miniscoping,[status(thm)],[f3175]) ).
fof(f3177,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3176]) ).
fof(f3178,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f1122]) ).
fof(f3179,plain,
! [ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ) ),
inference(miniscoping,[status(thm)],[f3178]) ).
fof(f3180,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3179]) ).
fof(f3204,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)],[f1133]) ).
fof(f3206,plain,
~ disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),
inference(cnf_transformation,[status(thm)],[f3204]) ).
fof(f3207,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_15_93775),
inference(resolution,[status(thm)],[f3174,f3206]) ).
fof(f3209,plain,
! [X0] :
( ~ genls(c_tptpcol_15_93775,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f3177,f3207]) ).
fof(f3213,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_14_93774),
inference(resolution,[status(thm)],[f3209,f1399]) ).
fof(f3216,plain,
! [X0] :
( ~ genls(c_tptpcol_14_93774,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f3213,f3177]) ).
fof(f3307,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_13_93766),
inference(resolution,[status(thm)],[f1413,f3216]) ).
fof(f3313,plain,
! [X0] :
( ~ genls(c_tptpcol_13_93766,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f3307,f3177]) ).
fof(f3334,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_12_93765),
inference(resolution,[status(thm)],[f3313,f1246]) ).
fof(f3338,plain,
! [X0] :
( ~ genls(c_tptpcol_12_93765,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f3334,f3177]) ).
fof(f3354,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_11_93764),
inference(resolution,[status(thm)],[f3338,f1237]) ).
fof(f3361,plain,
! [X0] :
( ~ genls(c_tptpcol_11_93764,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f3354,f3177]) ).
fof(f3583,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_10_93700),
inference(resolution,[status(thm)],[f1675,f3361]) ).
fof(f3588,plain,
! [X0] :
( ~ genls(c_tptpcol_10_93700,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f3583,f3177]) ).
fof(f3612,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_9_93699),
inference(resolution,[status(thm)],[f1685,f3588]) ).
fof(f3623,plain,
! [X0] :
( ~ genls(c_tptpcol_9_93699,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f3612,f3177]) ).
fof(f3637,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_8_93698),
inference(resolution,[status(thm)],[f3623,f1672]) ).
fof(f3640,plain,
! [X0] :
( ~ genls(c_tptpcol_8_93698,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f3637,f3177]) ).
fof(f3684,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_7_93186),
inference(resolution,[status(thm)],[f3640,f1636]) ).
fof(f3693,plain,
! [X0] :
( ~ genls(c_tptpcol_7_93186,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f3684,f3177]) ).
fof(f3772,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_6_92162),
inference(resolution,[status(thm)],[f3693,f1154]) ).
fof(f3777,plain,
! [X0] :
( ~ genls(c_tptpcol_6_92162,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f3772,f3177]) ).
fof(f4038,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_5_90114),
inference(resolution,[status(thm)],[f3777,f1741]) ).
fof(f4040,plain,
! [X0] :
( ~ genls(c_tptpcol_5_90114,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f4038,f3177]) ).
fof(f4308,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_4_90113),
inference(resolution,[status(thm)],[f4040,f1829]) ).
fof(f4313,plain,
! [X0] :
( ~ genls(c_tptpcol_4_90113,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f4308,f3177]) ).
fof(f4578,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_3_81921),
inference(resolution,[status(thm)],[f4313,f1681]) ).
fof(f4580,plain,
! [X0] :
( ~ genls(c_tptpcol_3_81921,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f4578,f3177]) ).
fof(f4875,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_2_65537),
inference(resolution,[status(thm)],[f4580,f1194]) ).
fof(f4880,plain,
! [X0] :
( ~ genls(c_tptpcol_2_65537,X0)
| ~ disjointwith(c_tptpcol_13_18664,X0) ),
inference(resolution,[status(thm)],[f4875,f3177]) ).
fof(f5320,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_1_65536),
inference(resolution,[status(thm)],[f4880,f1640]) ).
fof(f5345,plain,
! [X0] :
( ~ genls(c_tptpcol_13_18664,X0)
| ~ disjointwith(X0,c_tptpcol_1_65536) ),
inference(resolution,[status(thm)],[f5320,f3180]) ).
fof(f6269,plain,
! [X0] :
( genls(X0,c_tptpcol_6_18436)
| ~ genls(X0,c_tptpcol_7_18437) ),
inference(resolution,[status(thm)],[f3148,f1840]) ).
fof(f6302,plain,
! [X0] :
( genls(X0,c_tptpcol_2_2)
| ~ genls(X0,c_tptpcol_3_16386) ),
inference(resolution,[status(thm)],[f3148,f1694]) ).
fof(f6313,plain,
! [X0] :
( genls(X0,c_tptpcol_7_18437)
| ~ genls(X0,c_tptpcol_8_18438) ),
inference(resolution,[status(thm)],[f3148,f1647]) ).
fof(f6314,plain,
! [X0] :
( genls(X0,c_tptpcol_5_16388)
| ~ genls(X0,c_tptpcol_6_18436) ),
inference(resolution,[status(thm)],[f3148,f1644]) ).
fof(f6331,plain,
! [X0] :
( genls(X0,c_tptpcol_3_16386)
| ~ genls(X0,c_tptpcol_4_16387) ),
inference(resolution,[status(thm)],[f3148,f1548]) ).
fof(f6339,plain,
! [X0] :
( genls(X0,c_tptpcol_8_18438)
| ~ genls(X0,c_tptpcol_9_18439) ),
inference(resolution,[status(thm)],[f3148,f1505]) ).
fof(f6365,plain,
! [X0] :
( genls(X0,c_tptpcol_10_18567)
| ~ genls(X0,c_tptpcol_11_18631) ),
inference(resolution,[status(thm)],[f3148,f1389]) ).
fof(f6374,plain,
! [X0] :
( genls(X0,c_tptpcol_1_1)
| ~ genls(X0,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[f3148,f1343]) ).
fof(f6386,plain,
! [X0] :
( genls(X0,c_tptpcol_11_18631)
| ~ genls(X0,c_tptpcol_12_18663) ),
inference(resolution,[status(thm)],[f3148,f1292]) ).
fof(f6404,plain,
! [X0] :
( genls(X0,c_tptpcol_9_18439)
| ~ genls(X0,c_tptpcol_10_18567) ),
inference(resolution,[status(thm)],[f3148,f1197]) ).
fof(f6414,plain,
! [X0] :
( genls(X0,c_tptpcol_4_16387)
| ~ genls(X0,c_tptpcol_5_16388) ),
inference(resolution,[status(thm)],[f3148,f1167]) ).
fof(f9388,plain,
genls(c_tptpcol_13_18664,c_tptpcol_11_18631),
inference(resolution,[status(thm)],[f6386,f1438]) ).
fof(f9431,plain,
genls(c_tptpcol_13_18664,c_tptpcol_10_18567),
inference(resolution,[status(thm)],[f9388,f6365]) ).
fof(f9619,plain,
genls(c_tptpcol_13_18664,c_tptpcol_9_18439),
inference(resolution,[status(thm)],[f6404,f9431]) ).
fof(f10397,plain,
genls(c_tptpcol_13_18664,c_tptpcol_8_18438),
inference(resolution,[status(thm)],[f9619,f6339]) ).
fof(f11269,plain,
genls(c_tptpcol_13_18664,c_tptpcol_7_18437),
inference(resolution,[status(thm)],[f10397,f6313]) ).
fof(f11742,plain,
genls(c_tptpcol_13_18664,c_tptpcol_6_18436),
inference(resolution,[status(thm)],[f11269,f6269]) ).
fof(f11969,plain,
genls(c_tptpcol_13_18664,c_tptpcol_5_16388),
inference(resolution,[status(thm)],[f11742,f6314]) ).
fof(f12131,plain,
genls(c_tptpcol_13_18664,c_tptpcol_4_16387),
inference(resolution,[status(thm)],[f11969,f6414]) ).
fof(f12293,plain,
genls(c_tptpcol_13_18664,c_tptpcol_3_16386),
inference(resolution,[status(thm)],[f12131,f6331]) ).
fof(f12500,plain,
genls(c_tptpcol_13_18664,c_tptpcol_2_2),
inference(resolution,[status(thm)],[f12293,f6302]) ).
fof(f12772,plain,
genls(c_tptpcol_13_18664,c_tptpcol_1_1),
inference(resolution,[status(thm)],[f12500,f6374]) ).
fof(f13146,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(resolution,[status(thm)],[f12772,f5345]) ).
fof(f13178,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f13146,f1353]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR039+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n008.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 14:30:54 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.39 % Drodi V4.1.1
% 13.41/2.22 % Refutation found
% 13.41/2.22 % SZS status Theorem for theBenchmark: Theorem is valid
% 13.41/2.22 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.40/3.47 % Elapsed time: 2.890532 seconds
% 8.40/3.47 % CPU time: 14.219317 seconds
% 8.40/3.47 % Total memory used: 286.830 MB
% 8.40/3.47 % Net memory used: 278.720 MB
%------------------------------------------------------------------------------