%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR040+3 : 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 : n001.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 0.37s 0.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR040+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 14:35:44 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.25/0.55 % Drodi V4.1.1
% 0.37/0.78 % Refutation found
% 0.37/0.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.37/0.78 % SZS output start CNFRefutation for theBenchmark
% 0.37/0.78 fof(f119,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_13_109173(OBJ)=> tptpcol_12_109157(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f179,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_0_0(OBJ)=> individual(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f477,axiom,(
% 0.37/0.78 (! [OBJ] :( fixedordercollection(OBJ)=> collection(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f634,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_15_109185(OBJ)=> tptpcol_14_109181(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f645,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_8_109059(OBJ)=> tptpcol_7_108547(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f678,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_1_65536(OBJ)=> tptpcol_0_0(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f1096,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_5_106498(OBJ)=> tptpcol_4_106497(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f1102,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_11_109125(OBJ)=> tptpcol_10_109061(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f1247,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_7_108547(OBJ)=> tptpcol_6_108546(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f1282,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_2_98304(OBJ)=> tptpcol_1_65536(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f1400,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_14_109181(OBJ)=> tptpcol_13_109173(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f1444,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_3_98305(OBJ)=> tptpcol_2_98304(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f1981,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_9_109060(OBJ)=> tptpcol_8_109059(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f2336,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_12_109157(OBJ)=> tptpcol_11_109125(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f2475,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_4_106497(OBJ)=> tptpcol_3_98305(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f3061,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_6_108546(OBJ)=> tptpcol_5_106498(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f3081,axiom,(
% 0.37/0.78 firstordercollection(c_tptpcol_16_62187) ),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f3089,axiom,(
% 0.37/0.78 (! [OBJ] :~ ( collection(OBJ)& individual(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f3241,axiom,(
% 0.37/0.78 (! [OBJ] :( firstordercollection(OBJ)=> fixedordercollection(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f3252,axiom,(
% 0.37/0.78 (! [OBJ] :( tptpcol_10_109061(OBJ)=> tptpcol_9_109060(OBJ) ) )),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f8006,conjecture,(
% 0.37/0.78 ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ) ),
% 0.37/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.78 fof(f8007,negated_conjecture,(
% 0.37/0.78 ~(( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ) )),
% 0.37/0.78 inference(negated_conjecture,[status(cth)],[f8006])).
% 0.37/0.78 fof(f8162,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_13_109173(OBJ)|tptpcol_12_109157(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f119])).
% 0.37/0.78 fof(f8163,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_13_109173(X0)|tptpcol_12_109157(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f8162])).
% 0.37/0.78 fof(f8243,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_0_0(OBJ)|individual(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f179])).
% 0.37/0.78 fof(f8244,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_0_0(X0)|individual(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f8243])).
% 0.37/0.78 fof(f8651,plain,(
% 0.37/0.78 ![OBJ]: (~fixedordercollection(OBJ)|collection(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f477])).
% 0.37/0.78 fof(f8652,plain,(
% 0.37/0.78 ![X0]: (~fixedordercollection(X0)|collection(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f8651])).
% 0.37/0.78 fof(f8874,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_15_109185(OBJ)|tptpcol_14_109181(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f634])).
% 0.37/0.78 fof(f8875,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_15_109185(X0)|tptpcol_14_109181(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f8874])).
% 0.37/0.78 fof(f8890,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_8_109059(OBJ)|tptpcol_7_108547(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f645])).
% 0.37/0.78 fof(f8891,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_8_109059(X0)|tptpcol_7_108547(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f8890])).
% 0.37/0.78 fof(f8935,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_1_65536(OBJ)|tptpcol_0_0(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f678])).
% 0.37/0.78 fof(f8936,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_1_65536(X0)|tptpcol_0_0(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f8935])).
% 0.37/0.78 fof(f9541,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_5_106498(OBJ)|tptpcol_4_106497(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f1096])).
% 0.37/0.78 fof(f9542,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_5_106498(X0)|tptpcol_4_106497(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f9541])).
% 0.37/0.78 fof(f9550,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_11_109125(OBJ)|tptpcol_10_109061(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f1102])).
% 0.37/0.78 fof(f9551,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_11_109125(X0)|tptpcol_10_109061(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f9550])).
% 0.37/0.78 fof(f9754,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_7_108547(OBJ)|tptpcol_6_108546(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f1247])).
% 0.37/0.78 fof(f9755,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_7_108547(X0)|tptpcol_6_108546(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f9754])).
% 0.37/0.78 fof(f9803,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_2_98304(OBJ)|tptpcol_1_65536(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f1282])).
% 0.37/0.78 fof(f9804,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_2_98304(X0)|tptpcol_1_65536(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f9803])).
% 0.37/0.78 fof(f9968,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_14_109181(OBJ)|tptpcol_13_109173(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f1400])).
% 0.37/0.78 fof(f9969,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_14_109181(X0)|tptpcol_13_109173(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f9968])).
% 0.37/0.78 fof(f10032,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_3_98305(OBJ)|tptpcol_2_98304(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f1444])).
% 0.37/0.78 fof(f10033,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_3_98305(X0)|tptpcol_2_98304(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f10032])).
% 0.37/0.78 fof(f10785,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_9_109060(OBJ)|tptpcol_8_109059(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f1981])).
% 0.37/0.78 fof(f10786,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_9_109060(X0)|tptpcol_8_109059(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f10785])).
% 0.37/0.78 fof(f11277,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_12_109157(OBJ)|tptpcol_11_109125(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f2336])).
% 0.37/0.78 fof(f11278,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_12_109157(X0)|tptpcol_11_109125(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f11277])).
% 0.37/0.78 fof(f11468,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_4_106497(OBJ)|tptpcol_3_98305(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f2475])).
% 0.37/0.78 fof(f11469,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_4_106497(X0)|tptpcol_3_98305(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f11468])).
% 0.37/0.78 fof(f12297,plain,(
% 0.37/0.78 ![OBJ]: (~tptpcol_6_108546(OBJ)|tptpcol_5_106498(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f3061])).
% 0.37/0.78 fof(f12298,plain,(
% 0.37/0.78 ![X0]: (~tptpcol_6_108546(X0)|tptpcol_5_106498(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f12297])).
% 0.37/0.78 fof(f12323,plain,(
% 0.37/0.78 firstordercollection(c_tptpcol_16_62187)),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f3081])).
% 0.37/0.78 fof(f12334,plain,(
% 0.37/0.78 ![OBJ]: (~collection(OBJ)|~individual(OBJ))),
% 0.37/0.78 inference(pre_NNF_transformation,[status(thm)],[f3089])).
% 0.37/0.78 fof(f12335,plain,(
% 0.37/0.78 ![X0]: (~collection(X0)|~individual(X0))),
% 0.37/0.78 inference(cnf_transformation,[status(thm)],[f12334])).
% 0.37/0.78 fof(f12535,plain,(
% 0.39/0.81 ![OBJ]: (~firstordercollection(OBJ)|fixedordercollection(OBJ))),
% 0.39/0.81 inference(pre_NNF_transformation,[status(thm)],[f3241])).
% 0.39/0.81 fof(f12536,plain,(
% 0.39/0.81 ![X0]: (~firstordercollection(X0)|fixedordercollection(X0))),
% 0.39/0.81 inference(cnf_transformation,[status(thm)],[f12535])).
% 0.39/0.81 fof(f12551,plain,(
% 0.39/0.81 ![OBJ]: (~tptpcol_10_109061(OBJ)|tptpcol_9_109060(OBJ))),
% 0.39/0.81 inference(pre_NNF_transformation,[status(thm)],[f3252])).
% 0.39/0.81 fof(f12552,plain,(
% 0.39/0.81 ![X0]: (~tptpcol_10_109061(X0)|tptpcol_9_109060(X0))),
% 0.39/0.81 inference(cnf_transformation,[status(thm)],[f12551])).
% 0.39/0.81 fof(f21391,plain,(
% 0.39/0.81 (mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))&tptpcol_15_109185(c_tptpcol_16_62187))),
% 0.39/0.81 inference(pre_NNF_transformation,[status(thm)],[f8007])).
% 0.39/0.81 fof(f21393,plain,(
% 0.39/0.81 tptpcol_15_109185(c_tptpcol_16_62187)),
% 0.39/0.81 inference(cnf_transformation,[status(thm)],[f21391])).
% 0.39/0.81 fof(f21394,plain,(
% 0.39/0.81 tptpcol_14_109181(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f8875,f21393])).
% 0.39/0.81 fof(f22640,plain,(
% 0.39/0.81 tptpcol_13_109173(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f9969,f21394])).
% 0.39/0.81 fof(f22646,plain,(
% 0.39/0.81 tptpcol_12_109157(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f22640,f8163])).
% 0.39/0.81 fof(f23464,plain,(
% 0.39/0.81 tptpcol_11_109125(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f11278,f22646])).
% 0.39/0.81 fof(f23465,plain,(
% 0.39/0.81 tptpcol_10_109061(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f23464,f9551])).
% 0.39/0.81 fof(f25023,plain,(
% 0.39/0.81 fixedordercollection(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f12536,f12323])).
% 0.39/0.81 fof(f25024,plain,(
% 0.39/0.81 collection(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25023,f8652])).
% 0.39/0.81 fof(f25025,plain,(
% 0.39/0.81 ~individual(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25024,f12335])).
% 0.39/0.81 fof(f25033,plain,(
% 0.39/0.81 tptpcol_9_109060(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f12552,f23465])).
% 0.39/0.81 fof(f25038,plain,(
% 0.39/0.81 tptpcol_8_109059(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25033,f10786])).
% 0.39/0.81 fof(f25039,plain,(
% 0.39/0.81 tptpcol_7_108547(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25038,f8891])).
% 0.39/0.81 fof(f25040,plain,(
% 0.39/0.81 tptpcol_6_108546(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25039,f9755])).
% 0.39/0.81 fof(f25041,plain,(
% 0.39/0.81 tptpcol_5_106498(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25040,f12298])).
% 0.39/0.81 fof(f25042,plain,(
% 0.39/0.81 tptpcol_4_106497(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25041,f9542])).
% 0.39/0.81 fof(f25043,plain,(
% 0.39/0.81 tptpcol_3_98305(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25042,f11469])).
% 0.39/0.81 fof(f25044,plain,(
% 0.39/0.81 tptpcol_2_98304(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25043,f10033])).
% 0.39/0.81 fof(f25045,plain,(
% 0.39/0.81 tptpcol_1_65536(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25044,f9804])).
% 0.39/0.81 fof(f25063,plain,(
% 0.39/0.81 tptpcol_0_0(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25045,f8936])).
% 0.39/0.81 fof(f25077,plain,(
% 0.39/0.81 individual(c_tptpcol_16_62187)),
% 0.39/0.81 inference(resolution,[status(thm)],[f25063,f8244])).
% 0.39/0.81 fof(f25078,plain,(
% 0.39/0.81 $false),
% 0.39/0.81 inference(forward_subsumption_resolution,[status(thm)],[f25077,f25025])).
% 0.39/0.81 % SZS output end CNFRefutation for theBenchmark.p
% 2.52/2.04 % Elapsed time: 1.440386 seconds
% 2.52/2.04 % CPU time: 2.036240 seconds
% 2.52/2.04 % Total memory used: 390.422 MB
% 2.52/2.04 % Net memory used: 389.731 MB
%------------------------------------------------------------------------------