%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR040+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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.08s 0.40s
% Output : CNFRefutation 0.08s
% 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(f4,axiom,
! [OBJ] :
( firstordercollection(OBJ)
=> fixedordercollection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [OBJ] :
( fixedordercollection(OBJ)
=> collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [OBJ] :
( tptpcol_0_0(OBJ)
=> individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [OBJ] :
( tptpcol_1_65536(OBJ)
=> tptpcol_0_0(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [OBJ] :
( tptpcol_2_98304(OBJ)
=> tptpcol_1_65536(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [OBJ] :
( tptpcol_3_98305(OBJ)
=> tptpcol_2_98304(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [OBJ] :
( tptpcol_4_106497(OBJ)
=> tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [OBJ] :
( tptpcol_5_106498(OBJ)
=> tptpcol_4_106497(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [OBJ] :
( tptpcol_6_108546(OBJ)
=> tptpcol_5_106498(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [OBJ] :
( tptpcol_7_108547(OBJ)
=> tptpcol_6_108546(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [OBJ] :
( tptpcol_8_109059(OBJ)
=> tptpcol_7_108547(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [OBJ] :
( tptpcol_9_109060(OBJ)
=> tptpcol_8_109059(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [OBJ] :
( tptpcol_10_109061(OBJ)
=> tptpcol_9_109060(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [OBJ] :
( tptpcol_11_109125(OBJ)
=> tptpcol_10_109061(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [OBJ] :
( tptpcol_12_109157(OBJ)
=> tptpcol_11_109125(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [OBJ] :
( tptpcol_13_109173(OBJ)
=> tptpcol_12_109157(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [OBJ] :
( tptpcol_14_109181(OBJ)
=> tptpcol_13_109173(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [OBJ] :
( tptpcol_15_109185(OBJ)
=> tptpcol_14_109181(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,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(f147,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)],[f146]) ).
fof(f151,plain,
! [OBJ] :
( fixedordercollection(OBJ)
| ~ firstordercollection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f152,plain,
! [X0] :
( fixedordercollection(X0)
| ~ firstordercollection(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f157,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f158,plain,
! [X0] :
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f163,plain,
! [OBJ] :
( collection(OBJ)
| ~ fixedordercollection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f164,plain,
! [X0] :
( collection(X0)
| ~ fixedordercollection(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f166,plain,
! [OBJ] :
( individual(OBJ)
| ~ tptpcol_0_0(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f167,plain,
! [X0] :
( individual(X0)
| ~ tptpcol_0_0(X0) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f168,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f170,plain,
! [OBJ] :
( tptpcol_0_0(OBJ)
| ~ tptpcol_1_65536(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f171,plain,
! [X0] :
( tptpcol_0_0(X0)
| ~ tptpcol_1_65536(X0) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f173,plain,
! [OBJ] :
( tptpcol_1_65536(OBJ)
| ~ tptpcol_2_98304(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f174,plain,
! [X0] :
( tptpcol_1_65536(X0)
| ~ tptpcol_2_98304(X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f176,plain,
! [OBJ] :
( tptpcol_2_98304(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f177,plain,
! [X0] :
( tptpcol_2_98304(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f179,plain,
! [OBJ] :
( tptpcol_3_98305(OBJ)
| ~ tptpcol_4_106497(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f180,plain,
! [X0] :
( tptpcol_3_98305(X0)
| ~ tptpcol_4_106497(X0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f182,plain,
! [OBJ] :
( tptpcol_4_106497(OBJ)
| ~ tptpcol_5_106498(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f183,plain,
! [X0] :
( tptpcol_4_106497(X0)
| ~ tptpcol_5_106498(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f185,plain,
! [OBJ] :
( tptpcol_5_106498(OBJ)
| ~ tptpcol_6_108546(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f186,plain,
! [X0] :
( tptpcol_5_106498(X0)
| ~ tptpcol_6_108546(X0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f188,plain,
! [OBJ] :
( tptpcol_6_108546(OBJ)
| ~ tptpcol_7_108547(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f189,plain,
! [X0] :
( tptpcol_6_108546(X0)
| ~ tptpcol_7_108547(X0) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f191,plain,
! [OBJ] :
( tptpcol_7_108547(OBJ)
| ~ tptpcol_8_109059(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f192,plain,
! [X0] :
( tptpcol_7_108547(X0)
| ~ tptpcol_8_109059(X0) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f194,plain,
! [OBJ] :
( tptpcol_8_109059(OBJ)
| ~ tptpcol_9_109060(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f195,plain,
! [X0] :
( tptpcol_8_109059(X0)
| ~ tptpcol_9_109060(X0) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f197,plain,
! [OBJ] :
( tptpcol_9_109060(OBJ)
| ~ tptpcol_10_109061(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f198,plain,
! [X0] :
( tptpcol_9_109060(X0)
| ~ tptpcol_10_109061(X0) ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f200,plain,
! [OBJ] :
( tptpcol_10_109061(OBJ)
| ~ tptpcol_11_109125(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f201,plain,
! [X0] :
( tptpcol_10_109061(X0)
| ~ tptpcol_11_109125(X0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f203,plain,
! [OBJ] :
( tptpcol_11_109125(OBJ)
| ~ tptpcol_12_109157(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f204,plain,
! [X0] :
( tptpcol_11_109125(X0)
| ~ tptpcol_12_109157(X0) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f206,plain,
! [OBJ] :
( tptpcol_12_109157(OBJ)
| ~ tptpcol_13_109173(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f207,plain,
! [X0] :
( tptpcol_12_109157(X0)
| ~ tptpcol_13_109173(X0) ),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f209,plain,
! [OBJ] :
( tptpcol_13_109173(OBJ)
| ~ tptpcol_14_109181(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f210,plain,
! [X0] :
( tptpcol_13_109173(X0)
| ~ tptpcol_14_109181(X0) ),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f212,plain,
! [OBJ] :
( tptpcol_14_109181(OBJ)
| ~ tptpcol_15_109185(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f213,plain,
! [X0] :
( tptpcol_14_109181(X0)
| ~ tptpcol_15_109185(X0) ),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f429,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)],[f147]) ).
fof(f431,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnf_transformation,[status(thm)],[f429]) ).
fof(f432,plain,
fixedordercollection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f152,f168]) ).
fof(f433,plain,
collection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f164,f432]) ).
fof(f434,plain,
~ individual(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f433,f158]) ).
fof(f435,plain,
tptpcol_14_109181(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f213,f431]) ).
fof(f436,plain,
tptpcol_13_109173(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f435,f210]) ).
fof(f437,plain,
tptpcol_12_109157(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f436,f207]) ).
fof(f438,plain,
tptpcol_11_109125(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f437,f204]) ).
fof(f439,plain,
tptpcol_10_109061(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f438,f201]) ).
fof(f440,plain,
tptpcol_9_109060(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f439,f198]) ).
fof(f441,plain,
tptpcol_8_109059(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f440,f195]) ).
fof(f442,plain,
tptpcol_7_108547(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f441,f192]) ).
fof(f443,plain,
tptpcol_6_108546(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f442,f189]) ).
fof(f445,plain,
tptpcol_5_106498(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f443,f186]) ).
fof(f446,plain,
tptpcol_4_106497(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f445,f183]) ).
fof(f447,plain,
tptpcol_3_98305(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f446,f180]) ).
fof(f448,plain,
tptpcol_2_98304(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f447,f177]) ).
fof(f449,plain,
tptpcol_1_65536(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f448,f174]) ).
fof(f450,plain,
tptpcol_0_0(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f449,f171]) ).
fof(f452,plain,
individual(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f450,f167]) ).
fof(f453,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f452,f434]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR040+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n003.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 21 14:32:01 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.08/0.40 % Refutation found
% 0.08/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.08/0.44 % Elapsed time: 0.052837 seconds
% 0.08/0.44 % CPU time: 0.138399 seconds
% 0.08/0.44 % Total memory used: 60.304 MB
% 0.08/0.44 % Net memory used: 60.283 MB
%------------------------------------------------------------------------------