%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR040+2 : 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 0.09s 0.43s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 21
% Syntax : Number of formulae : 83 ( 20 unt; 0 def)
% Number of atoms : 146 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 128 ( 65 ~; 41 |; 2 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 60 ( 60 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f50,axiom,
! [OBJ] :
( tptpcol_2_98304(OBJ)
=> tptpcol_1_65536(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [OBJ] :
( tptpcol_4_106497(OBJ)
=> tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,axiom,
! [OBJ] :
( tptpcol_10_109061(OBJ)
=> tptpcol_9_109060(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,axiom,
! [OBJ] :
( tptpcol_13_109173(OBJ)
=> tptpcol_12_109157(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,axiom,
! [OBJ] :
( tptpcol_5_106498(OBJ)
=> tptpcol_4_106497(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,axiom,
! [OBJ] :
( tptpcol_1_65536(OBJ)
=> tptpcol_0_0(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [OBJ] :
( fixedordercollection(OBJ)
=> collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f185,axiom,
! [OBJ] :
( tptpcol_8_109059(OBJ)
=> tptpcol_7_108547(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f205,axiom,
! [OBJ] :
( firstordercollection(OBJ)
=> fixedordercollection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f234,axiom,
! [OBJ] :
( tptpcol_3_98305(OBJ)
=> tptpcol_2_98304(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f242,axiom,
! [OBJ] :
( tptpcol_9_109060(OBJ)
=> tptpcol_8_109059(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f251,axiom,
! [OBJ] :
( tptpcol_14_109181(OBJ)
=> tptpcol_13_109173(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f266,axiom,
! [OBJ] :
( tptpcol_15_109185(OBJ)
=> tptpcol_14_109181(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f289,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f341,axiom,
! [OBJ] :
( tptpcol_7_108547(OBJ)
=> tptpcol_6_108546(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f343,axiom,
! [OBJ] :
( tptpcol_11_109125(OBJ)
=> tptpcol_10_109061(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f360,axiom,
! [OBJ] :
( tptpcol_12_109157(OBJ)
=> tptpcol_11_109125(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f445,axiom,
! [OBJ] :
( tptpcol_0_0(OBJ)
=> individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f459,axiom,
! [OBJ] :
( tptpcol_6_108546(OBJ)
=> tptpcol_5_106498(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f475,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1132,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1133,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(negated_conjecture,[status(cth)],[f1132]) ).
fof(f1207,plain,
! [OBJ] :
( tptpcol_1_65536(OBJ)
| ~ tptpcol_2_98304(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f1208,plain,
! [X0] :
( tptpcol_1_65536(X0)
| ~ tptpcol_2_98304(X0) ),
inference(cnf_transformation,[status(thm)],[f1207]) ).
fof(f1232,plain,
! [OBJ] :
( tptpcol_3_98305(OBJ)
| ~ tptpcol_4_106497(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f1233,plain,
! [X0] :
( tptpcol_3_98305(X0)
| ~ tptpcol_4_106497(X0) ),
inference(cnf_transformation,[status(thm)],[f1232]) ).
fof(f1271,plain,
! [OBJ] :
( tptpcol_9_109060(OBJ)
| ~ tptpcol_10_109061(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f96]) ).
fof(f1272,plain,
! [X0] :
( tptpcol_9_109060(X0)
| ~ tptpcol_10_109061(X0) ),
inference(cnf_transformation,[status(thm)],[f1271]) ).
fof(f1299,plain,
! [OBJ] :
( tptpcol_12_109157(OBJ)
| ~ tptpcol_13_109173(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f114]) ).
fof(f1300,plain,
! [X0] :
( tptpcol_12_109157(X0)
| ~ tptpcol_13_109173(X0) ),
inference(cnf_transformation,[status(thm)],[f1299]) ).
fof(f1303,plain,
! [OBJ] :
( tptpcol_4_106497(OBJ)
| ~ tptpcol_5_106498(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f117]) ).
fof(f1304,plain,
! [X0] :
( tptpcol_4_106497(X0)
| ~ tptpcol_5_106498(X0) ),
inference(cnf_transformation,[status(thm)],[f1303]) ).
fof(f1314,plain,
! [OBJ] :
( tptpcol_0_0(OBJ)
| ~ tptpcol_1_65536(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f124]) ).
fof(f1315,plain,
! [X0] :
( tptpcol_0_0(X0)
| ~ tptpcol_1_65536(X0) ),
inference(cnf_transformation,[status(thm)],[f1314]) ).
fof(f1351,plain,
! [OBJ] :
( collection(OBJ)
| ~ fixedordercollection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f151]) ).
fof(f1352,plain,
! [X0] :
( collection(X0)
| ~ fixedordercollection(X0) ),
inference(cnf_transformation,[status(thm)],[f1351]) ).
fof(f1403,plain,
! [OBJ] :
( tptpcol_7_108547(OBJ)
| ~ tptpcol_8_109059(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f185]) ).
fof(f1404,plain,
! [X0] :
( tptpcol_7_108547(X0)
| ~ tptpcol_8_109059(X0) ),
inference(cnf_transformation,[status(thm)],[f1403]) ).
fof(f1433,plain,
! [OBJ] :
( fixedordercollection(OBJ)
| ~ firstordercollection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f205]) ).
fof(f1434,plain,
! [X0] :
( fixedordercollection(X0)
| ~ firstordercollection(X0) ),
inference(cnf_transformation,[status(thm)],[f1433]) ).
fof(f1475,plain,
! [OBJ] :
( tptpcol_2_98304(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f234]) ).
fof(f1476,plain,
! [X0] :
( tptpcol_2_98304(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(thm)],[f1475]) ).
fof(f1487,plain,
! [OBJ] :
( tptpcol_8_109059(OBJ)
| ~ tptpcol_9_109060(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f242]) ).
fof(f1488,plain,
! [X0] :
( tptpcol_8_109059(X0)
| ~ tptpcol_9_109060(X0) ),
inference(cnf_transformation,[status(thm)],[f1487]) ).
fof(f1499,plain,
! [OBJ] :
( tptpcol_13_109173(OBJ)
| ~ tptpcol_14_109181(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f251]) ).
fof(f1500,plain,
! [X0] :
( tptpcol_13_109173(X0)
| ~ tptpcol_14_109181(X0) ),
inference(cnf_transformation,[status(thm)],[f1499]) ).
fof(f1521,plain,
! [OBJ] :
( tptpcol_14_109181(OBJ)
| ~ tptpcol_15_109185(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f266]) ).
fof(f1522,plain,
! [X0] :
( tptpcol_14_109181(X0)
| ~ tptpcol_15_109185(X0) ),
inference(cnf_transformation,[status(thm)],[f1521]) ).
fof(f1554,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f289]) ).
fof(f1555,plain,
! [X0] :
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(thm)],[f1554]) ).
fof(f1630,plain,
! [OBJ] :
( tptpcol_6_108546(OBJ)
| ~ tptpcol_7_108547(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f341]) ).
fof(f1631,plain,
! [X0] :
( tptpcol_6_108546(X0)
| ~ tptpcol_7_108547(X0) ),
inference(cnf_transformation,[status(thm)],[f1630]) ).
fof(f1633,plain,
! [OBJ] :
( tptpcol_10_109061(OBJ)
| ~ tptpcol_11_109125(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f343]) ).
fof(f1634,plain,
! [X0] :
( tptpcol_10_109061(X0)
| ~ tptpcol_11_109125(X0) ),
inference(cnf_transformation,[status(thm)],[f1633]) ).
fof(f1657,plain,
! [OBJ] :
( tptpcol_11_109125(OBJ)
| ~ tptpcol_12_109157(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f360]) ).
fof(f1658,plain,
! [X0] :
( tptpcol_11_109125(X0)
| ~ tptpcol_12_109157(X0) ),
inference(cnf_transformation,[status(thm)],[f1657]) ).
fof(f1783,plain,
! [OBJ] :
( individual(OBJ)
| ~ tptpcol_0_0(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f445]) ).
fof(f1784,plain,
! [X0] :
( individual(X0)
| ~ tptpcol_0_0(X0) ),
inference(cnf_transformation,[status(thm)],[f1783]) ).
fof(f1802,plain,
! [OBJ] :
( tptpcol_5_106498(OBJ)
| ~ tptpcol_6_108546(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f459]) ).
fof(f1803,plain,
! [X0] :
( tptpcol_5_106498(X0)
| ~ tptpcol_6_108546(X0) ),
inference(cnf_transformation,[status(thm)],[f1802]) ).
fof(f1828,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f3204,plain,
( tptpcol_15_109185(c_tptpcol_16_62187)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14)) ),
inference(pre_NNF_transformation,[status(thm)],[f1133]) ).
fof(f3206,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnf_transformation,[status(thm)],[f3204]) ).
fof(f3214,plain,
! [X0] :
( ~ fixedordercollection(X0)
| ~ individual(X0) ),
inference(resolution,[status(thm)],[f1555,f1352]) ).
fof(f3221,plain,
! [X0] :
( tptpcol_10_109061(X0)
| ~ tptpcol_12_109157(X0) ),
inference(resolution,[status(thm)],[f1658,f1634]) ).
fof(f3249,plain,
! [X0] :
( ~ firstordercollection(X0)
| ~ individual(X0) ),
inference(resolution,[status(thm)],[f3214,f1434]) ).
fof(f3267,plain,
~ individual(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3249,f1828]) ).
fof(f3268,plain,
~ tptpcol_0_0(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3267,f1784]) ).
fof(f3270,plain,
~ tptpcol_1_65536(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3268,f1315]) ).
fof(f3272,plain,
~ tptpcol_2_98304(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3270,f1208]) ).
fof(f3275,plain,
~ tptpcol_3_98305(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3272,f1476]) ).
fof(f3277,plain,
~ tptpcol_4_106497(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3275,f1233]) ).
fof(f3280,plain,
~ tptpcol_5_106498(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3277,f1304]) ).
fof(f3283,plain,
~ tptpcol_6_108546(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3280,f1803]) ).
fof(f3287,plain,
~ tptpcol_7_108547(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3283,f1631]) ).
fof(f3290,plain,
~ tptpcol_8_109059(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3287,f1404]) ).
fof(f3292,plain,
~ tptpcol_9_109060(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3290,f1488]) ).
fof(f3294,plain,
~ tptpcol_10_109061(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3292,f1272]) ).
fof(f3296,plain,
~ tptpcol_12_109157(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3294,f3221]) ).
fof(f3298,plain,
~ tptpcol_13_109173(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3296,f1300]) ).
fof(f3300,plain,
~ tptpcol_14_109181(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3298,f1500]) ).
fof(f3302,plain,
~ tptpcol_15_109185(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f3300,f1522]) ).
fof(f3303,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f3302,f3206]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR040+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 14:31:09 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.40 % Drodi V4.1.1
% 0.09/0.43 % Refutation found
% 0.09/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.48 % Elapsed time: 0.098420 seconds
% 0.09/0.48 % CPU time: 0.261825 seconds
% 0.09/0.48 % Total memory used: 102.936 MB
% 0.09/0.48 % Net memory used: 102.869 MB
%------------------------------------------------------------------------------