%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR040+4 : 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:03 PM UTC 2026
% Result : Theorem 107.15s 14.93s
% Output : CNFRefutation 75.33s
% 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(f318,axiom,
! [OBJ] :
( tptpcol_0_0(OBJ)
=> individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f448,axiom,
! [OBJ] :
( tptpcol_10_109061(OBJ)
=> tptpcol_9_109060(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f733,axiom,
! [OBJ] :
( tptpcol_9_109060(OBJ)
=> tptpcol_8_109059(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1291,axiom,
! [OBJ] :
( tptpcol_8_109059(OBJ)
=> tptpcol_7_108547(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1714,axiom,
! [OBJ] :
( firstordercollection(OBJ)
=> fixedordercollection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3253,axiom,
! [OBJ] :
( tptpcol_6_108546(OBJ)
=> tptpcol_5_106498(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3389,axiom,
! [OBJ] :
( tptpcol_12_109157(OBJ)
=> tptpcol_11_109125(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4028,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5043,axiom,
! [OBJ] :
( tptpcol_1_65536(OBJ)
=> tptpcol_0_0(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5511,axiom,
! [OBJ] :
( tptpcol_2_98304(OBJ)
=> tptpcol_1_65536(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5949,axiom,
! [OBJ] :
( tptpcol_4_106497(OBJ)
=> tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6733,axiom,
! [OBJ] :
( tptpcol_15_109185(OBJ)
=> tptpcol_14_109181(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7614,axiom,
! [OBJ] :
( tptpcol_14_109181(OBJ)
=> tptpcol_13_109173(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9044,axiom,
! [OBJ] :
( tptpcol_7_108547(OBJ)
=> tptpcol_6_108546(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12015,axiom,
! [OBJ] :
( fixedordercollection(OBJ)
=> collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15240,axiom,
! [OBJ] :
( tptpcol_5_106498(OBJ)
=> tptpcol_4_106497(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15564,axiom,
! [OBJ] :
( tptpcol_13_109173(OBJ)
=> tptpcol_12_109157(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20268,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22390,axiom,
! [OBJ] :
( tptpcol_3_98305(OBJ)
=> tptpcol_2_98304(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24107,axiom,
! [OBJ] :
( tptpcol_11_109125(OBJ)
=> tptpcol_10_109061(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44217,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(f44218,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)],[f44217]) ).
fof(f44608,plain,
! [OBJ] :
( individual(OBJ)
| ~ tptpcol_0_0(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f318]) ).
fof(f44609,plain,
! [X0] :
( individual(X0)
| ~ tptpcol_0_0(X0) ),
inference(cnf_transformation,[status(thm)],[f44608]) ).
fof(f44766,plain,
! [OBJ] :
( tptpcol_9_109060(OBJ)
| ~ tptpcol_10_109061(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f448]) ).
fof(f44767,plain,
! [X0] :
( tptpcol_9_109060(X0)
| ~ tptpcol_10_109061(X0) ),
inference(cnf_transformation,[status(thm)],[f44766]) ).
fof(f45128,plain,
! [OBJ] :
( tptpcol_8_109059(OBJ)
| ~ tptpcol_9_109060(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f733]) ).
fof(f45129,plain,
! [X0] :
( tptpcol_8_109059(X0)
| ~ tptpcol_9_109060(X0) ),
inference(cnf_transformation,[status(thm)],[f45128]) ).
fof(f45829,plain,
! [OBJ] :
( tptpcol_7_108547(OBJ)
| ~ tptpcol_8_109059(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f1291]) ).
fof(f45830,plain,
! [X0] :
( tptpcol_7_108547(X0)
| ~ tptpcol_8_109059(X0) ),
inference(cnf_transformation,[status(thm)],[f45829]) ).
fof(f46365,plain,
! [OBJ] :
( fixedordercollection(OBJ)
| ~ firstordercollection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f1714]) ).
fof(f46366,plain,
! [X0] :
( fixedordercollection(X0)
| ~ firstordercollection(X0) ),
inference(cnf_transformation,[status(thm)],[f46365]) ).
fof(f48285,plain,
! [OBJ] :
( tptpcol_5_106498(OBJ)
| ~ tptpcol_6_108546(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f3253]) ).
fof(f48286,plain,
! [X0] :
( tptpcol_5_106498(X0)
| ~ tptpcol_6_108546(X0) ),
inference(cnf_transformation,[status(thm)],[f48285]) ).
fof(f48450,plain,
! [OBJ] :
( tptpcol_11_109125(OBJ)
| ~ tptpcol_12_109157(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f3389]) ).
fof(f48451,plain,
! [X0] :
( tptpcol_11_109125(X0)
| ~ tptpcol_12_109157(X0) ),
inference(cnf_transformation,[status(thm)],[f48450]) ).
fof(f49265,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f4028]) ).
fof(f49266,plain,
! [X0] :
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(thm)],[f49265]) ).
fof(f50535,plain,
! [OBJ] :
( tptpcol_0_0(OBJ)
| ~ tptpcol_1_65536(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f5043]) ).
fof(f50536,plain,
! [X0] :
( tptpcol_0_0(X0)
| ~ tptpcol_1_65536(X0) ),
inference(cnf_transformation,[status(thm)],[f50535]) ).
fof(f51121,plain,
! [OBJ] :
( tptpcol_1_65536(OBJ)
| ~ tptpcol_2_98304(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f5511]) ).
fof(f51122,plain,
! [X0] :
( tptpcol_1_65536(X0)
| ~ tptpcol_2_98304(X0) ),
inference(cnf_transformation,[status(thm)],[f51121]) ).
fof(f51690,plain,
! [OBJ] :
( tptpcol_3_98305(OBJ)
| ~ tptpcol_4_106497(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f5949]) ).
fof(f51691,plain,
! [X0] :
( tptpcol_3_98305(X0)
| ~ tptpcol_4_106497(X0) ),
inference(cnf_transformation,[status(thm)],[f51690]) ).
fof(f52669,plain,
! [OBJ] :
( tptpcol_14_109181(OBJ)
| ~ tptpcol_15_109185(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f6733]) ).
fof(f52670,plain,
! [X0] :
( tptpcol_14_109181(X0)
| ~ tptpcol_15_109185(X0) ),
inference(cnf_transformation,[status(thm)],[f52669]) ).
fof(f53805,plain,
! [OBJ] :
( tptpcol_13_109173(OBJ)
| ~ tptpcol_14_109181(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f7614]) ).
fof(f53806,plain,
! [X0] :
( tptpcol_13_109173(X0)
| ~ tptpcol_14_109181(X0) ),
inference(cnf_transformation,[status(thm)],[f53805]) ).
fof(f55614,plain,
! [OBJ] :
( tptpcol_6_108546(OBJ)
| ~ tptpcol_7_108547(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f9044]) ).
fof(f55615,plain,
! [X0] :
( tptpcol_6_108546(X0)
| ~ tptpcol_7_108547(X0) ),
inference(cnf_transformation,[status(thm)],[f55614]) ).
fof(f59299,plain,
! [OBJ] :
( collection(OBJ)
| ~ fixedordercollection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f12015]) ).
fof(f59300,plain,
! [X0] :
( collection(X0)
| ~ fixedordercollection(X0) ),
inference(cnf_transformation,[status(thm)],[f59299]) ).
fof(f63365,plain,
! [OBJ] :
( tptpcol_4_106497(OBJ)
| ~ tptpcol_5_106498(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f15240]) ).
fof(f63366,plain,
! [X0] :
( tptpcol_4_106497(X0)
| ~ tptpcol_5_106498(X0) ),
inference(cnf_transformation,[status(thm)],[f63365]) ).
fof(f63763,plain,
! [OBJ] :
( tptpcol_12_109157(OBJ)
| ~ tptpcol_13_109173(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f15564]) ).
fof(f63764,plain,
! [X0] :
( tptpcol_12_109157(X0)
| ~ tptpcol_13_109173(X0) ),
inference(cnf_transformation,[status(thm)],[f63763]) ).
fof(f69661,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnf_transformation,[status(thm)],[f20268]) ).
fof(f72325,plain,
! [OBJ] :
( tptpcol_2_98304(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f22390]) ).
fof(f72326,plain,
! [X0] :
( tptpcol_2_98304(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(thm)],[f72325]) ).
fof(f74474,plain,
! [OBJ] :
( tptpcol_10_109061(OBJ)
| ~ tptpcol_11_109125(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f24107]) ).
fof(f74475,plain,
! [X0] :
( tptpcol_10_109061(X0)
| ~ tptpcol_11_109125(X0) ),
inference(cnf_transformation,[status(thm)],[f74474]) ).
fof(f110738,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)],[f44218]) ).
fof(f110740,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnf_transformation,[status(thm)],[f110738]) ).
fof(f110743,plain,
tptpcol_14_109181(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f52670,f110740]) ).
fof(f111580,plain,
fixedordercollection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f46366,f69661]) ).
fof(f115233,plain,
tptpcol_13_109173(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f53806,f110743]) ).
fof(f117449,plain,
collection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f59300,f111580]) ).
fof(f117463,plain,
~ individual(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f117449,f49266]) ).
fof(f119496,plain,
tptpcol_12_109157(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f63764,f115233]) ).
fof(f119497,plain,
tptpcol_11_109125(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f119496,f48451]) ).
fof(f124422,plain,
tptpcol_10_109061(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f74475,f119497]) ).
fof(f124423,plain,
tptpcol_9_109060(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124422,f44767]) ).
fof(f124424,plain,
tptpcol_8_109059(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124423,f45129]) ).
fof(f124425,plain,
tptpcol_7_108547(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124424,f45830]) ).
fof(f124430,plain,
tptpcol_6_108546(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124425,f55615]) ).
fof(f124437,plain,
tptpcol_5_106498(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124430,f48286]) ).
fof(f124441,plain,
tptpcol_4_106497(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124437,f63366]) ).
fof(f124446,plain,
tptpcol_3_98305(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124441,f51691]) ).
fof(f124447,plain,
tptpcol_2_98304(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124446,f72326]) ).
fof(f124448,plain,
tptpcol_1_65536(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124447,f51122]) ).
fof(f124449,plain,
tptpcol_0_0(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124448,f50536]) ).
fof(f124450,plain,
individual(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[f124449,f44609]) ).
fof(f124451,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f124450,f117463]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR040+4 : 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:35:52 UTC 2026
% 0.09/0.36 % CPUTime :
% 1.16/1.40 % Drodi V4.1.1
% 107.15/14.93 % Refutation found
% 107.15/14.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 107.15/14.93 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.18/15.35 % Elapsed time: 14.925552 seconds
% 4.18/15.35 % CPU time: 109.180722 seconds
% 4.18/15.35 % Total memory used: 2.115 GB
% 4.18/15.35 % Net memory used: 2.110 GB
%------------------------------------------------------------------------------