%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR040+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 : n016.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 1.92s 0.74s
% Output : CNFRefutation 1.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 21
% Syntax : Number of formulae : 83 ( 23 unt; 0 def)
% Number of atoms : 143 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 105 ( 45 ~; 38 |; 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 : 57 ( 57 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f119,axiom,
! [OBJ] :
( tptpcol_13_109173(OBJ)
=> tptpcol_12_109157(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,axiom,
! [OBJ] :
( tptpcol_0_0(OBJ)
=> individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f477,axiom,
! [OBJ] :
( fixedordercollection(OBJ)
=> collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f634,axiom,
! [OBJ] :
( tptpcol_15_109185(OBJ)
=> tptpcol_14_109181(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f645,axiom,
! [OBJ] :
( tptpcol_8_109059(OBJ)
=> tptpcol_7_108547(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f678,axiom,
! [OBJ] :
( tptpcol_1_65536(OBJ)
=> tptpcol_0_0(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1096,axiom,
! [OBJ] :
( tptpcol_5_106498(OBJ)
=> tptpcol_4_106497(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1102,axiom,
! [OBJ] :
( tptpcol_11_109125(OBJ)
=> tptpcol_10_109061(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1247,axiom,
! [OBJ] :
( tptpcol_7_108547(OBJ)
=> tptpcol_6_108546(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1282,axiom,
! [OBJ] :
( tptpcol_2_98304(OBJ)
=> tptpcol_1_65536(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1400,axiom,
! [OBJ] :
( tptpcol_14_109181(OBJ)
=> tptpcol_13_109173(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1444,axiom,
! [OBJ] :
( tptpcol_3_98305(OBJ)
=> tptpcol_2_98304(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1981,axiom,
! [OBJ] :
( tptpcol_9_109060(OBJ)
=> tptpcol_8_109059(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2336,axiom,
! [OBJ] :
( tptpcol_12_109157(OBJ)
=> tptpcol_11_109125(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2475,axiom,
! [OBJ] :
( tptpcol_4_106497(OBJ)
=> tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3061,axiom,
! [OBJ] :
( tptpcol_6_108546(OBJ)
=> tptpcol_5_106498(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3081,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3089,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3241,axiom,
! [OBJ] :
( firstordercollection(OBJ)
=> fixedordercollection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3252,axiom,
! [OBJ] :
( tptpcol_10_109061(OBJ)
=> tptpcol_9_109060(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8006,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(f8007,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)],[f8006]) ).
fof(f8162,plain,
! [OBJ] :
( tptpcol_12_109157(OBJ)
| ~ tptpcol_13_109173(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f119]) ).
fof(f8163,plain,
! [X0] :
( tptpcol_12_109157(X0)
| ~ tptpcol_13_109173(X0) ),
inference(cnf_transformation,[status(thm)],[f8162]) ).
fof(f8243,plain,
! [OBJ] :
( individual(OBJ)
| ~ tptpcol_0_0(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f179]) ).
fof(f8244,plain,
! [X0] :
( individual(X0)
| ~ tptpcol_0_0(X0) ),
inference(cnf_transformation,[status(thm)],[f8243]) ).
fof(f8651,plain,
! [OBJ] :
( collection(OBJ)
| ~ fixedordercollection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f477]) ).
fof(f8652,plain,
! [X0] :
( collection(X0)
| ~ fixedordercollection(X0) ),
inference(cnf_transformation,[status(thm)],[f8651]) ).
fof(f8874,plain,
! [OBJ] :
( tptpcol_14_109181(OBJ)
| ~ tptpcol_15_109185(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f634]) ).
fof(f8875,plain,
! [X0] :
( tptpcol_14_109181(X0)
| ~ tptpcol_15_109185(X0) ),
inference(cnf_transformation,[status(thm)],[f8874]) ).
fof(f8890,plain,
! [OBJ] :
( tptpcol_7_108547(OBJ)
| ~ tptpcol_8_109059(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f645]) ).
fof(f8891,plain,
! [X0] :
( tptpcol_7_108547(X0)
| ~ tptpcol_8_109059(X0) ),
inference(cnf_transformation,[status(thm)],[f8890]) ).
fof(f8935,plain,
! [OBJ] :
( tptpcol_0_0(OBJ)
| ~ tptpcol_1_65536(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f678]) ).
fof(f8936,plain,
! [X0] :
( tptpcol_0_0(X0)
| ~ tptpcol_1_65536(X0) ),
inference(cnf_transformation,[status(thm)],[f8935]) ).
fof(f9541,plain,
! [OBJ] :
( tptpcol_4_106497(OBJ)
| ~ tptpcol_5_106498(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f1096]) ).
fof(f9542,plain,
! [X0] :
( tptpcol_4_106497(X0)
| ~ tptpcol_5_106498(X0) ),
inference(cnf_transformation,[status(thm)],[f9541]) ).
fof(f9550,plain,
! [OBJ] :
( tptpcol_10_109061(OBJ)
| ~ tptpcol_11_109125(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f1102]) ).
fof(f9551,plain,
! [X0] :
( tptpcol_10_109061(X0)
| ~ tptpcol_11_109125(X0) ),
inference(cnf_transformation,[status(thm)],[f9550]) ).
fof(f9754,plain,
! [OBJ] :
( tptpcol_6_108546(OBJ)
| ~ tptpcol_7_108547(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f1247]) ).
fof(f9755,plain,
! [X0] :
( tptpcol_6_108546(X0)
| ~ tptpcol_7_108547(X0) ),
inference(cnf_transformation,[status(thm)],[f9754]) ).
fof(f9803,plain,
! [OBJ] :
( tptpcol_1_65536(OBJ)
| ~ tptpcol_2_98304(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f1282]) ).
fof(f9804,plain,
! [X0] :
( tptpcol_1_65536(X0)
| ~ tptpcol_2_98304(X0) ),
inference(cnf_transformation,[status(thm)],[f9803]) ).
fof(f9968,plain,
! [OBJ] :
( tptpcol_13_109173(OBJ)
| ~ tptpcol_14_109181(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f1400]) ).
fof(f9969,plain,
! [X0] :
( tptpcol_13_109173(X0)
| ~ tptpcol_14_109181(X0) ),
inference(cnf_transformation,[status(thm)],[f9968]) ).
fof(f10032,plain,
! [OBJ] :
( tptpcol_2_98304(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f1444]) ).
fof(f10033,plain,
! [X0] :
( tptpcol_2_98304(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(thm)],[f10032]) ).
fof(f10785,plain,
! [OBJ] :
( tptpcol_8_109059(OBJ)
| ~ tptpcol_9_109060(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f1981]) ).
fof(f10786,plain,
! [X0] :
( tptpcol_8_109059(X0)
| ~ tptpcol_9_109060(X0) ),
inference(cnf_transformation,[status(thm)],[f10785]) ).
fof(f11277,plain,
! [OBJ] :
( tptpcol_11_109125(OBJ)
| ~ tptpcol_12_109157(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f2336]) ).
fof(f11278,plain,
! [X0] :
( tptpcol_11_109125(X0)
| ~ tptpcol_12_109157(X0) ),
inference(cnf_transformation,[status(thm)],[f11277]) ).
fof(f11468,plain,
! [OBJ] :
( tptpcol_3_98305(OBJ)
| ~ tptpcol_4_106497(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f2475]) ).
fof(f11469,plain,
! [X0] :
( tptpcol_3_98305(X0)
| ~ tptpcol_4_106497(X0) ),
inference(cnf_transformation,[status(thm)],[f11468]) ).
fof(f12297,plain,
! [OBJ] :
( tptpcol_5_106498(OBJ)
| ~ tptpcol_6_108546(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f3061]) ).
fof(f12298,plain,
! [X0] :
( tptpcol_5_106498(X0)
| ~ tptpcol_6_108546(X0) ),
inference(cnf_transformation,[status(thm)],[f12297]) ).
fof(f12323,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnf_transformation,[status(thm)],[f3081]) ).
fof(f12334,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f3089]) ).
fof(f12335,plain,
! [X0] :
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(thm)],[f12334]) ).
fof(f12535,plain,
! [OBJ] :
( fixedordercollection(OBJ)
| ~ firstordercollection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f3241]) ).
fof(f12536,plain,
! [X0] :
( fixedordercollection(X0)
| ~ firstordercollection(X0) ),
inference(cnf_transformation,[status(thm)],[f12535]) ).
fof(f12551,plain,
! [OBJ] :
( tptpcol_9_109060(OBJ)
| ~ tptpcol_10_109061(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f3252]) ).
fof(f12552,plain,
! [X0] :
( tptpcol_9_109060(X0)
| ~ tptpcol_10_109061(X0) ),
inference(cnf_transformation,[status(thm)],[f12551]) ).
fof(f21391,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)],[f8007]) ).
fof(f21393,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnf_transformation,[status(thm)],[f21391]) ).
fof(f21394,plain,
tptpcol_14_109181(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f8875,f21393]) ).
fof(f22738,plain,
tptpcol_13_109173(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f9969,f21394]) ).
fof(f22744,plain,
tptpcol_12_109157(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f22738,f8163]) ).
fof(f23623,plain,
tptpcol_11_109125(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f11278,f22744]) ).
fof(f23624,plain,
tptpcol_10_109061(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f23623,f9551]) ).
fof(f25273,plain,
fixedordercollection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f12536,f12323]) ).
fof(f25277,plain,
collection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25273,f8652]) ).
fof(f25278,plain,
~ individual(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25277,f12335]) ).
fof(f25283,plain,
tptpcol_9_109060(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f12552,f23624]) ).
fof(f25286,plain,
tptpcol_8_109059(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25283,f10786]) ).
fof(f25287,plain,
tptpcol_7_108547(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25286,f8891]) ).
fof(f25288,plain,
tptpcol_6_108546(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25287,f9755]) ).
fof(f25289,plain,
tptpcol_5_106498(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25288,f12298]) ).
fof(f25290,plain,
tptpcol_4_106497(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25289,f9542]) ).
fof(f25291,plain,
tptpcol_3_98305(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25290,f11469]) ).
fof(f25293,plain,
tptpcol_2_98304(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25291,f10033]) ).
fof(f25298,plain,
tptpcol_1_65536(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25293,f9804]) ).
fof(f25299,plain,
tptpcol_0_0(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25298,f8936]) ).
fof(f25300,plain,
individual(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f25299,f8244]) ).
fof(f25301,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f25300,f25278]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR040+3 : 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.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 14:34:52 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.44 % Drodi V4.1.1
% 1.92/0.74 % Refutation found
% 1.92/0.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.92/0.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.43/1.97 % Elapsed time: 1.380808 seconds
% 3.43/1.97 % CPU time: 2.421084 seconds
% 3.43/1.97 % Total memory used: 403.650 MB
% 3.43/1.97 % Net memory used: 402.914 MB
%------------------------------------------------------------------------------