%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR040+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:14:44 PM UTC 2026
% Result : Theorem 128.73s 18.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR040+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n004.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 14:31:04 UTC 2026
% 0.17/0.44 % CPUTime :
% 1.47/1.80 % Drodi V4.1.1
% 128.73/18.01 % Refutation found
% 128.73/18.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 128.73/18.01 % SZS output start CNFRefutation for theBenchmark
% 128.73/18.01 fof(f318,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_0_0(OBJ)=> individual(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f448,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_10_109061(OBJ)=> tptpcol_9_109060(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f733,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_9_109060(OBJ)=> tptpcol_8_109059(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f1291,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_8_109059(OBJ)=> tptpcol_7_108547(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f1714,axiom,(
% 128.73/18.01 (! [OBJ] :( firstordercollection(OBJ)=> fixedordercollection(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f3253,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_6_108546(OBJ)=> tptpcol_5_106498(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f3389,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_12_109157(OBJ)=> tptpcol_11_109125(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f4028,axiom,(
% 128.73/18.01 (! [OBJ] :~ ( collection(OBJ)& individual(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f5043,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_1_65536(OBJ)=> tptpcol_0_0(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f5511,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_2_98304(OBJ)=> tptpcol_1_65536(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f5949,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_4_106497(OBJ)=> tptpcol_3_98305(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f6733,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_15_109185(OBJ)=> tptpcol_14_109181(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f7614,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_14_109181(OBJ)=> tptpcol_13_109173(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f9044,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_7_108547(OBJ)=> tptpcol_6_108546(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f12015,axiom,(
% 128.73/18.01 (! [OBJ] :( fixedordercollection(OBJ)=> collection(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f15240,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_5_106498(OBJ)=> tptpcol_4_106497(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f15564,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_13_109173(OBJ)=> tptpcol_12_109157(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f20268,axiom,(
% 128.73/18.01 firstordercollection(c_tptpcol_16_62187) ),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f22390,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_3_98305(OBJ)=> tptpcol_2_98304(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f24107,axiom,(
% 128.73/18.01 (! [OBJ] :( tptpcol_11_109125(OBJ)=> tptpcol_10_109061(OBJ) ) )),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f44217,conjecture,(
% 128.73/18.01 ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ) ),
% 128.73/18.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 128.73/18.01 fof(f44218,negated_conjecture,(
% 128.73/18.01 ~(( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ) )),
% 128.73/18.01 inference(negated_conjecture,[status(cth)],[f44217])).
% 128.73/18.01 fof(f44608,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_0_0(OBJ)|individual(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f318])).
% 128.73/18.01 fof(f44609,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_0_0(X0)|individual(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f44608])).
% 128.73/18.01 fof(f44766,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_10_109061(OBJ)|tptpcol_9_109060(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f448])).
% 128.73/18.01 fof(f44767,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_10_109061(X0)|tptpcol_9_109060(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f44766])).
% 128.73/18.01 fof(f45128,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_9_109060(OBJ)|tptpcol_8_109059(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f733])).
% 128.73/18.01 fof(f45129,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_9_109060(X0)|tptpcol_8_109059(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f45128])).
% 128.73/18.01 fof(f45829,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_8_109059(OBJ)|tptpcol_7_108547(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f1291])).
% 128.73/18.01 fof(f45830,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_8_109059(X0)|tptpcol_7_108547(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f45829])).
% 128.73/18.01 fof(f46365,plain,(
% 128.73/18.01 ![OBJ]: (~firstordercollection(OBJ)|fixedordercollection(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f1714])).
% 128.73/18.01 fof(f46366,plain,(
% 128.73/18.01 ![X0]: (~firstordercollection(X0)|fixedordercollection(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f46365])).
% 128.73/18.01 fof(f48285,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_6_108546(OBJ)|tptpcol_5_106498(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f3253])).
% 128.73/18.01 fof(f48286,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_6_108546(X0)|tptpcol_5_106498(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f48285])).
% 128.73/18.01 fof(f48450,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_12_109157(OBJ)|tptpcol_11_109125(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f3389])).
% 128.73/18.01 fof(f48451,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_12_109157(X0)|tptpcol_11_109125(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f48450])).
% 128.73/18.01 fof(f49265,plain,(
% 128.73/18.01 ![OBJ]: (~collection(OBJ)|~individual(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f4028])).
% 128.73/18.01 fof(f49266,plain,(
% 128.73/18.01 ![X0]: (~collection(X0)|~individual(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f49265])).
% 128.73/18.01 fof(f50535,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_1_65536(OBJ)|tptpcol_0_0(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f5043])).
% 128.73/18.01 fof(f50536,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_1_65536(X0)|tptpcol_0_0(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f50535])).
% 128.73/18.01 fof(f51121,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_2_98304(OBJ)|tptpcol_1_65536(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f5511])).
% 128.73/18.01 fof(f51122,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_2_98304(X0)|tptpcol_1_65536(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f51121])).
% 128.73/18.01 fof(f51690,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_4_106497(OBJ)|tptpcol_3_98305(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f5949])).
% 128.73/18.01 fof(f51691,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_4_106497(X0)|tptpcol_3_98305(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f51690])).
% 128.73/18.01 fof(f52669,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_15_109185(OBJ)|tptpcol_14_109181(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f6733])).
% 128.73/18.01 fof(f52670,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_15_109185(X0)|tptpcol_14_109181(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f52669])).
% 128.73/18.01 fof(f53805,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_14_109181(OBJ)|tptpcol_13_109173(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f7614])).
% 128.73/18.01 fof(f53806,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_14_109181(X0)|tptpcol_13_109173(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f53805])).
% 128.73/18.01 fof(f55614,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_7_108547(OBJ)|tptpcol_6_108546(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f9044])).
% 128.73/18.01 fof(f55615,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_7_108547(X0)|tptpcol_6_108546(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f55614])).
% 128.73/18.01 fof(f59299,plain,(
% 128.73/18.01 ![OBJ]: (~fixedordercollection(OBJ)|collection(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f12015])).
% 128.73/18.01 fof(f59300,plain,(
% 128.73/18.01 ![X0]: (~fixedordercollection(X0)|collection(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f59299])).
% 128.73/18.01 fof(f63365,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_5_106498(OBJ)|tptpcol_4_106497(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f15240])).
% 128.73/18.01 fof(f63366,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_5_106498(X0)|tptpcol_4_106497(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f63365])).
% 128.73/18.01 fof(f63763,plain,(
% 128.73/18.01 ![OBJ]: (~tptpcol_13_109173(OBJ)|tptpcol_12_109157(OBJ))),
% 128.73/18.01 inference(pre_NNF_transformation,[status(thm)],[f15564])).
% 128.73/18.01 fof(f63764,plain,(
% 128.73/18.01 ![X0]: (~tptpcol_13_109173(X0)|tptpcol_12_109157(X0))),
% 128.73/18.01 inference(cnf_transformation,[status(thm)],[f63763])).
% 128.73/18.01 fof(f69661,plain,(
% 128.73/18.01 firstordercollection(c_tptpcol_16_62187)),
% 118.75/18.25 inference(cnf_transformation,[status(thm)],[f20268])).
% 118.75/18.25 fof(f72325,plain,(
% 118.75/18.25 ![OBJ]: (~tptpcol_3_98305(OBJ)|tptpcol_2_98304(OBJ))),
% 118.75/18.25 inference(pre_NNF_transformation,[status(thm)],[f22390])).
% 118.75/18.25 fof(f72326,plain,(
% 118.75/18.25 ![X0]: (~tptpcol_3_98305(X0)|tptpcol_2_98304(X0))),
% 118.75/18.25 inference(cnf_transformation,[status(thm)],[f72325])).
% 118.75/18.25 fof(f74474,plain,(
% 118.75/18.25 ![OBJ]: (~tptpcol_11_109125(OBJ)|tptpcol_10_109061(OBJ))),
% 118.75/18.25 inference(pre_NNF_transformation,[status(thm)],[f24107])).
% 118.75/18.25 fof(f74475,plain,(
% 118.75/18.25 ![X0]: (~tptpcol_11_109125(X0)|tptpcol_10_109061(X0))),
% 118.75/18.25 inference(cnf_transformation,[status(thm)],[f74474])).
% 118.75/18.25 fof(f110738,plain,(
% 118.75/18.25 (mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))&tptpcol_15_109185(c_tptpcol_16_62187))),
% 118.75/18.25 inference(pre_NNF_transformation,[status(thm)],[f44218])).
% 118.75/18.25 fof(f110740,plain,(
% 118.75/18.25 tptpcol_15_109185(c_tptpcol_16_62187)),
% 118.75/18.25 inference(cnf_transformation,[status(thm)],[f110738])).
% 118.75/18.25 fof(f110743,plain,(
% 118.75/18.25 tptpcol_14_109181(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f52670,f110740])).
% 118.75/18.25 fof(f111550,plain,(
% 118.75/18.25 fixedordercollection(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f46366,f69661])).
% 118.75/18.25 fof(f115201,plain,(
% 118.75/18.25 tptpcol_13_109173(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f53806,f110743])).
% 118.75/18.25 fof(f117586,plain,(
% 118.75/18.25 collection(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f59300,f111550])).
% 118.75/18.25 fof(f119379,plain,(
% 118.75/18.25 tptpcol_12_109157(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f63764,f115201])).
% 118.75/18.25 fof(f119380,plain,(
% 118.75/18.25 tptpcol_11_109125(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f119379,f48451])).
% 118.75/18.25 fof(f124445,plain,(
% 118.75/18.25 tptpcol_10_109061(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f74475,f119380])).
% 118.75/18.25 fof(f124446,plain,(
% 118.75/18.25 tptpcol_9_109060(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124445,f44767])).
% 118.75/18.25 fof(f124447,plain,(
% 118.75/18.25 tptpcol_8_109059(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124446,f45129])).
% 118.75/18.25 fof(f124448,plain,(
% 118.75/18.25 tptpcol_7_108547(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124447,f45830])).
% 118.75/18.25 fof(f124449,plain,(
% 118.75/18.25 tptpcol_6_108546(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124448,f55615])).
% 118.75/18.25 fof(f124450,plain,(
% 118.75/18.25 tptpcol_5_106498(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124449,f48286])).
% 118.75/18.25 fof(f124451,plain,(
% 118.75/18.25 tptpcol_4_106497(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124450,f63366])).
% 118.75/18.25 fof(f124452,plain,(
% 118.75/18.25 tptpcol_3_98305(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124451,f51691])).
% 118.75/18.25 fof(f124453,plain,(
% 118.75/18.25 tptpcol_2_98304(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124452,f72326])).
% 118.75/18.25 fof(f124455,plain,(
% 118.75/18.25 tptpcol_1_65536(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124453,f51122])).
% 118.75/18.25 fof(f124457,plain,(
% 118.75/18.25 tptpcol_0_0(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124455,f50536])).
% 118.75/18.25 fof(f124458,plain,(
% 118.75/18.25 individual(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124457,f44609])).
% 118.75/18.25 fof(f124460,plain,(
% 118.75/18.25 ~collection(c_tptpcol_16_62187)),
% 118.75/18.25 inference(resolution,[status(thm)],[f124458,f49266])).
% 118.75/18.25 fof(f124462,plain,(
% 118.75/18.25 $false),
% 118.75/18.25 inference(forward_subsumption_resolution,[status(thm)],[f124460,f117586])).
% 118.75/18.25 % SZS output end CNFRefutation for theBenchmark.p
% 42.23/18.39 % Elapsed time: 17.907273 seconds
% 42.23/18.39 % CPU time: 130.318480 seconds
% 42.23/18.39 % Total memory used: 2.186 GB
% 42.23/18.39 % Net memory used: 2.170 GB
%------------------------------------------------------------------------------