%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR040+2 : 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 : n006.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.03s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR040+2 : 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.11/0.36 % Computer : n006.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.03/0.36 % CPULimit : 300
% 0.03/0.36 % WCLimit : 300
% 0.03/0.36 % DateTime : Mon Sep 21 14:30:11 UTC 2026
% 0.03/0.36 % CPUTime :
% 0.03/0.39 % Drodi V4.1.1
% 0.03/0.42 % Refutation found
% 0.03/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.03/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.42 fof(f50,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_2_98304(OBJ)=> tptpcol_1_65536(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f69,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_4_106497(OBJ)=> tptpcol_3_98305(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f96,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_10_109061(OBJ)=> tptpcol_9_109060(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f114,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_13_109173(OBJ)=> tptpcol_12_109157(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f117,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_5_106498(OBJ)=> tptpcol_4_106497(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f124,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_1_65536(OBJ)=> tptpcol_0_0(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f151,axiom,(
% 0.03/0.42 (! [OBJ] :( fixedordercollection(OBJ)=> collection(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f185,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_8_109059(OBJ)=> tptpcol_7_108547(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f205,axiom,(
% 0.03/0.42 (! [OBJ] :( firstordercollection(OBJ)=> fixedordercollection(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f234,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_3_98305(OBJ)=> tptpcol_2_98304(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f242,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_9_109060(OBJ)=> tptpcol_8_109059(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f251,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_14_109181(OBJ)=> tptpcol_13_109173(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f266,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_15_109185(OBJ)=> tptpcol_14_109181(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f289,axiom,(
% 0.03/0.42 (! [OBJ] :~ ( collection(OBJ)& individual(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f341,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_7_108547(OBJ)=> tptpcol_6_108546(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f343,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_11_109125(OBJ)=> tptpcol_10_109061(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f360,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_12_109157(OBJ)=> tptpcol_11_109125(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f445,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_0_0(OBJ)=> individual(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f459,axiom,(
% 0.03/0.42 (! [OBJ] :( tptpcol_6_108546(OBJ)=> tptpcol_5_106498(OBJ) ) )),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f475,axiom,(
% 0.03/0.42 firstordercollection(c_tptpcol_16_62187) ),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f1132,conjecture,(
% 0.03/0.42 ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ) ),
% 0.03/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.42 fof(f1133,negated_conjecture,(
% 0.03/0.42 ~(( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ) )),
% 0.03/0.42 inference(negated_conjecture,[status(cth)],[f1132])).
% 0.03/0.42 fof(f1207,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_2_98304(OBJ)|tptpcol_1_65536(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.03/0.42 fof(f1208,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_2_98304(X0)|tptpcol_1_65536(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1207])).
% 0.03/0.42 fof(f1232,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_4_106497(OBJ)|tptpcol_3_98305(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 0.03/0.42 fof(f1233,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_4_106497(X0)|tptpcol_3_98305(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1232])).
% 0.03/0.42 fof(f1271,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_10_109061(OBJ)|tptpcol_9_109060(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 0.03/0.42 fof(f1272,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_10_109061(X0)|tptpcol_9_109060(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1271])).
% 0.03/0.42 fof(f1299,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_13_109173(OBJ)|tptpcol_12_109157(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f114])).
% 0.03/0.42 fof(f1300,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_13_109173(X0)|tptpcol_12_109157(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1299])).
% 0.03/0.42 fof(f1303,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_5_106498(OBJ)|tptpcol_4_106497(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f117])).
% 0.03/0.42 fof(f1304,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_5_106498(X0)|tptpcol_4_106497(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1303])).
% 0.03/0.42 fof(f1314,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_1_65536(OBJ)|tptpcol_0_0(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f124])).
% 0.03/0.42 fof(f1315,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_1_65536(X0)|tptpcol_0_0(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1314])).
% 0.03/0.42 fof(f1351,plain,(
% 0.03/0.42 ![OBJ]: (~fixedordercollection(OBJ)|collection(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f151])).
% 0.03/0.42 fof(f1352,plain,(
% 0.03/0.42 ![X0]: (~fixedordercollection(X0)|collection(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1351])).
% 0.03/0.42 fof(f1403,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_8_109059(OBJ)|tptpcol_7_108547(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f185])).
% 0.03/0.42 fof(f1404,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_8_109059(X0)|tptpcol_7_108547(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1403])).
% 0.03/0.42 fof(f1433,plain,(
% 0.03/0.42 ![OBJ]: (~firstordercollection(OBJ)|fixedordercollection(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f205])).
% 0.03/0.42 fof(f1434,plain,(
% 0.03/0.42 ![X0]: (~firstordercollection(X0)|fixedordercollection(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1433])).
% 0.03/0.42 fof(f1475,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_3_98305(OBJ)|tptpcol_2_98304(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f234])).
% 0.03/0.42 fof(f1476,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_3_98305(X0)|tptpcol_2_98304(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1475])).
% 0.03/0.42 fof(f1487,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_9_109060(OBJ)|tptpcol_8_109059(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f242])).
% 0.03/0.42 fof(f1488,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_9_109060(X0)|tptpcol_8_109059(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1487])).
% 0.03/0.42 fof(f1499,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_14_109181(OBJ)|tptpcol_13_109173(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f251])).
% 0.03/0.42 fof(f1500,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_14_109181(X0)|tptpcol_13_109173(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1499])).
% 0.03/0.42 fof(f1521,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_15_109185(OBJ)|tptpcol_14_109181(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f266])).
% 0.03/0.42 fof(f1522,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_15_109185(X0)|tptpcol_14_109181(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1521])).
% 0.03/0.42 fof(f1554,plain,(
% 0.03/0.42 ![OBJ]: (~collection(OBJ)|~individual(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f289])).
% 0.03/0.42 fof(f1555,plain,(
% 0.03/0.42 ![X0]: (~collection(X0)|~individual(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1554])).
% 0.03/0.42 fof(f1630,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_7_108547(OBJ)|tptpcol_6_108546(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f341])).
% 0.03/0.42 fof(f1631,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_7_108547(X0)|tptpcol_6_108546(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1630])).
% 0.03/0.42 fof(f1633,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_11_109125(OBJ)|tptpcol_10_109061(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 0.03/0.42 fof(f1634,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_11_109125(X0)|tptpcol_10_109061(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1633])).
% 0.03/0.42 fof(f1657,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_12_109157(OBJ)|tptpcol_11_109125(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f360])).
% 0.03/0.42 fof(f1658,plain,(
% 0.03/0.42 ![X0]: (~tptpcol_12_109157(X0)|tptpcol_11_109125(X0))),
% 0.03/0.42 inference(cnf_transformation,[status(thm)],[f1657])).
% 0.03/0.42 fof(f1783,plain,(
% 0.03/0.42 ![OBJ]: (~tptpcol_0_0(OBJ)|individual(OBJ))),
% 0.03/0.42 inference(pre_NNF_transformation,[status(thm)],[f445])).
% 0.03/0.42 fof(f1784,plain,(
% 0.03/0.44 ![X0]: (~tptpcol_0_0(X0)|individual(X0))),
% 0.03/0.44 inference(cnf_transformation,[status(thm)],[f1783])).
% 0.03/0.44 fof(f1802,plain,(
% 0.03/0.44 ![OBJ]: (~tptpcol_6_108546(OBJ)|tptpcol_5_106498(OBJ))),
% 0.03/0.44 inference(pre_NNF_transformation,[status(thm)],[f459])).
% 0.03/0.44 fof(f1803,plain,(
% 0.03/0.44 ![X0]: (~tptpcol_6_108546(X0)|tptpcol_5_106498(X0))),
% 0.03/0.44 inference(cnf_transformation,[status(thm)],[f1802])).
% 0.03/0.44 fof(f1828,plain,(
% 0.03/0.44 firstordercollection(c_tptpcol_16_62187)),
% 0.03/0.44 inference(cnf_transformation,[status(thm)],[f475])).
% 0.03/0.44 fof(f3204,plain,(
% 0.03/0.44 (mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))&tptpcol_15_109185(c_tptpcol_16_62187))),
% 0.03/0.44 inference(pre_NNF_transformation,[status(thm)],[f1133])).
% 0.03/0.44 fof(f3206,plain,(
% 0.03/0.44 tptpcol_15_109185(c_tptpcol_16_62187)),
% 0.03/0.44 inference(cnf_transformation,[status(thm)],[f3204])).
% 0.03/0.44 fof(f3207,plain,(
% 0.03/0.44 tptpcol_14_109181(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f1522,f3206])).
% 0.03/0.44 fof(f3254,plain,(
% 0.03/0.44 fixedordercollection(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f1434,f1828])).
% 0.03/0.44 fof(f3256,plain,(
% 0.03/0.44 collection(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3254,f1352])).
% 0.03/0.44 fof(f3339,plain,(
% 0.03/0.44 tptpcol_13_109173(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f1500,f3207])).
% 0.03/0.44 fof(f3340,plain,(
% 0.03/0.44 tptpcol_12_109157(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3339,f1300])).
% 0.03/0.44 fof(f3410,plain,(
% 0.03/0.44 tptpcol_11_109125(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f1658,f3340])).
% 0.03/0.44 fof(f3411,plain,(
% 0.03/0.44 tptpcol_10_109061(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3410,f1634])).
% 0.03/0.44 fof(f3424,plain,(
% 0.03/0.44 tptpcol_9_109060(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3411,f1272])).
% 0.03/0.44 fof(f3425,plain,(
% 0.03/0.44 tptpcol_8_109059(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3424,f1488])).
% 0.03/0.44 fof(f3426,plain,(
% 0.03/0.44 tptpcol_7_108547(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3425,f1404])).
% 0.03/0.44 fof(f3427,plain,(
% 0.03/0.44 tptpcol_6_108546(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3426,f1631])).
% 0.03/0.44 fof(f3613,plain,(
% 0.03/0.44 tptpcol_5_106498(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f1803,f3427])).
% 0.03/0.44 fof(f3614,plain,(
% 0.03/0.44 tptpcol_4_106497(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3613,f1304])).
% 0.03/0.44 fof(f3615,plain,(
% 0.03/0.44 tptpcol_3_98305(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3614,f1233])).
% 0.03/0.44 fof(f3620,plain,(
% 0.03/0.44 tptpcol_2_98304(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3615,f1476])).
% 0.03/0.44 fof(f3621,plain,(
% 0.03/0.44 tptpcol_1_65536(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3620,f1208])).
% 0.03/0.44 fof(f3622,plain,(
% 0.03/0.44 tptpcol_0_0(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3621,f1315])).
% 0.03/0.44 fof(f3623,plain,(
% 0.03/0.44 individual(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3622,f1784])).
% 0.03/0.44 fof(f3625,plain,(
% 0.03/0.44 ~collection(c_tptpcol_16_62187)),
% 0.03/0.44 inference(resolution,[status(thm)],[f3623,f1555])).
% 0.03/0.44 fof(f3627,plain,(
% 0.03/0.44 $false),
% 0.03/0.44 inference(forward_subsumption_resolution,[status(thm)],[f3625,f3256])).
% 0.03/0.44 % SZS output end CNFRefutation for theBenchmark.p
% 1.42/1.66 % Elapsed time: 1.080059 seconds
% 1.42/1.66 % CPU time: 0.214796 seconds
% 1.42/1.66 % Total memory used: 68.099 MB
% 1.42/1.66 % Net memory used: 68.041 MB
%------------------------------------------------------------------------------