%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR040+1 : 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 : n007.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:43 PM UTC 2026
% Result : Theorem 0.17s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR040+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.46 % Computer : n007.cluster.edu
% 0.17/0.46 % Model : x86_64 x86_64
% 0.17/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.46 % Memory : 8046.5625MB
% 0.17/0.46 % OS : Linux 6.8.0-71-generic
% 0.17/0.46 % CPULimit : 300
% 0.17/0.46 % WCLimit : 300
% 0.17/0.46 % DateTime : Mon Sep 21 14:28:20 UTC 2026
% 0.17/0.46 % CPUTime :
% 0.17/0.48 % Drodi V4.1.1
% 0.17/0.50 % Refutation found
% 0.17/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.50 fof(f4,axiom,(
% 0.17/0.50 (! [OBJ] :( firstordercollection(OBJ)=> fixedordercollection(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f9,axiom,(
% 0.17/0.50 (! [OBJ] :~ ( collection(OBJ)& individual(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f14,axiom,(
% 0.17/0.50 (! [OBJ] :( fixedordercollection(OBJ)=> collection(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f16,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_0_0(OBJ)=> individual(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f17,axiom,(
% 0.17/0.50 firstordercollection(c_tptpcol_16_62187) ),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f19,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_1_65536(OBJ)=> tptpcol_0_0(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f21,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_2_98304(OBJ)=> tptpcol_1_65536(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f23,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_3_98305(OBJ)=> tptpcol_2_98304(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f25,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_4_106497(OBJ)=> tptpcol_3_98305(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f27,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_5_106498(OBJ)=> tptpcol_4_106497(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f29,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_6_108546(OBJ)=> tptpcol_5_106498(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f31,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_7_108547(OBJ)=> tptpcol_6_108546(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f33,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_8_109059(OBJ)=> tptpcol_7_108547(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f35,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_9_109060(OBJ)=> tptpcol_8_109059(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f37,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_10_109061(OBJ)=> tptpcol_9_109060(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f39,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_11_109125(OBJ)=> tptpcol_10_109061(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f41,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_12_109157(OBJ)=> tptpcol_11_109125(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f43,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_13_109173(OBJ)=> tptpcol_12_109157(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f45,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_14_109181(OBJ)=> tptpcol_13_109173(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f47,axiom,(
% 0.17/0.50 (! [OBJ] :( tptpcol_15_109185(OBJ)=> tptpcol_14_109181(OBJ) ) )),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f146,conjecture,(
% 0.17/0.50 ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ) ),
% 0.17/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.50 fof(f147,negated_conjecture,(
% 0.17/0.50 ~(( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ) )),
% 0.17/0.50 inference(negated_conjecture,[status(cth)],[f146])).
% 0.17/0.50 fof(f151,plain,(
% 0.17/0.50 ![OBJ]: (~firstordercollection(OBJ)|fixedordercollection(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.17/0.50 fof(f152,plain,(
% 0.17/0.50 ![X0]: (~firstordercollection(X0)|fixedordercollection(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f151])).
% 0.17/0.50 fof(f157,plain,(
% 0.17/0.50 ![OBJ]: (~collection(OBJ)|~individual(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.17/0.50 fof(f158,plain,(
% 0.17/0.50 ![X0]: (~collection(X0)|~individual(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f157])).
% 0.17/0.50 fof(f163,plain,(
% 0.17/0.50 ![OBJ]: (~fixedordercollection(OBJ)|collection(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.17/0.50 fof(f164,plain,(
% 0.17/0.50 ![X0]: (~fixedordercollection(X0)|collection(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f163])).
% 0.17/0.50 fof(f166,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_0_0(OBJ)|individual(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.17/0.50 fof(f167,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_0_0(X0)|individual(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f166])).
% 0.17/0.50 fof(f168,plain,(
% 0.17/0.50 firstordercollection(c_tptpcol_16_62187)),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f17])).
% 0.17/0.50 fof(f170,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_1_65536(OBJ)|tptpcol_0_0(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.17/0.50 fof(f171,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_1_65536(X0)|tptpcol_0_0(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f170])).
% 0.17/0.50 fof(f173,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_2_98304(OBJ)|tptpcol_1_65536(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.17/0.50 fof(f174,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_2_98304(X0)|tptpcol_1_65536(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f173])).
% 0.17/0.50 fof(f176,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_3_98305(OBJ)|tptpcol_2_98304(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.17/0.50 fof(f177,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_3_98305(X0)|tptpcol_2_98304(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f176])).
% 0.17/0.50 fof(f179,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_4_106497(OBJ)|tptpcol_3_98305(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.17/0.50 fof(f180,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_4_106497(X0)|tptpcol_3_98305(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f179])).
% 0.17/0.50 fof(f182,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_5_106498(OBJ)|tptpcol_4_106497(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.17/0.50 fof(f183,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_5_106498(X0)|tptpcol_4_106497(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f182])).
% 0.17/0.50 fof(f185,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_6_108546(OBJ)|tptpcol_5_106498(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.17/0.50 fof(f186,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_6_108546(X0)|tptpcol_5_106498(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f185])).
% 0.17/0.50 fof(f188,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_7_108547(OBJ)|tptpcol_6_108546(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.17/0.50 fof(f189,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_7_108547(X0)|tptpcol_6_108546(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f188])).
% 0.17/0.50 fof(f191,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_8_109059(OBJ)|tptpcol_7_108547(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.17/0.50 fof(f192,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_8_109059(X0)|tptpcol_7_108547(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f191])).
% 0.17/0.50 fof(f194,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_9_109060(OBJ)|tptpcol_8_109059(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.17/0.50 fof(f195,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_9_109060(X0)|tptpcol_8_109059(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f194])).
% 0.17/0.50 fof(f197,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_10_109061(OBJ)|tptpcol_9_109060(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.17/0.50 fof(f198,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_10_109061(X0)|tptpcol_9_109060(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.17/0.50 fof(f200,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_11_109125(OBJ)|tptpcol_10_109061(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.17/0.50 fof(f201,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_11_109125(X0)|tptpcol_10_109061(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f200])).
% 0.17/0.50 fof(f203,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_12_109157(OBJ)|tptpcol_11_109125(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.17/0.50 fof(f204,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_12_109157(X0)|tptpcol_11_109125(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f203])).
% 0.17/0.50 fof(f206,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_13_109173(OBJ)|tptpcol_12_109157(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 0.17/0.50 fof(f207,plain,(
% 0.17/0.50 ![X0]: (~tptpcol_13_109173(X0)|tptpcol_12_109157(X0))),
% 0.17/0.50 inference(cnf_transformation,[status(thm)],[f206])).
% 0.17/0.50 fof(f209,plain,(
% 0.17/0.50 ![OBJ]: (~tptpcol_14_109181(OBJ)|tptpcol_13_109173(OBJ))),
% 0.17/0.50 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.17/0.50 fof(f210,plain,(
% 0.17/0.51 ![X0]: (~tptpcol_14_109181(X0)|tptpcol_13_109173(X0))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f209])).
% 0.17/0.51 fof(f212,plain,(
% 0.17/0.51 ![OBJ]: (~tptpcol_15_109185(OBJ)|tptpcol_14_109181(OBJ))),
% 0.17/0.51 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.17/0.51 fof(f213,plain,(
% 0.17/0.51 ![X0]: (~tptpcol_15_109185(X0)|tptpcol_14_109181(X0))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f212])).
% 0.17/0.51 fof(f429,plain,(
% 0.17/0.51 (mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))&tptpcol_15_109185(c_tptpcol_16_62187))),
% 0.17/0.51 inference(pre_NNF_transformation,[status(thm)],[f147])).
% 0.17/0.51 fof(f431,plain,(
% 0.17/0.51 tptpcol_15_109185(c_tptpcol_16_62187)),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f429])).
% 0.17/0.51 fof(f432,plain,(
% 0.17/0.51 tptpcol_14_109181(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f213,f431])).
% 0.17/0.51 fof(f443,plain,(
% 0.17/0.51 tptpcol_13_109173(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f210,f432])).
% 0.17/0.51 fof(f444,plain,(
% 0.17/0.51 tptpcol_12_109157(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f443,f207])).
% 0.17/0.51 fof(f445,plain,(
% 0.17/0.51 tptpcol_11_109125(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f444,f204])).
% 0.17/0.51 fof(f446,plain,(
% 0.17/0.51 tptpcol_10_109061(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f445,f201])).
% 0.17/0.51 fof(f447,plain,(
% 0.17/0.51 tptpcol_9_109060(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f446,f198])).
% 0.17/0.51 fof(f448,plain,(
% 0.17/0.51 tptpcol_8_109059(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f447,f195])).
% 0.17/0.51 fof(f449,plain,(
% 0.17/0.51 tptpcol_7_108547(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f448,f192])).
% 0.17/0.51 fof(f450,plain,(
% 0.17/0.51 tptpcol_6_108546(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f449,f189])).
% 0.17/0.51 fof(f451,plain,(
% 0.17/0.51 tptpcol_5_106498(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f450,f186])).
% 0.17/0.51 fof(f452,plain,(
% 0.17/0.51 tptpcol_4_106497(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f451,f183])).
% 0.17/0.51 fof(f453,plain,(
% 0.17/0.51 tptpcol_3_98305(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f452,f180])).
% 0.17/0.51 fof(f454,plain,(
% 0.17/0.51 tptpcol_2_98304(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f453,f177])).
% 0.17/0.51 fof(f455,plain,(
% 0.17/0.51 tptpcol_1_65536(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f454,f174])).
% 0.17/0.51 fof(f456,plain,(
% 0.17/0.51 tptpcol_0_0(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f455,f171])).
% 0.17/0.51 fof(f457,plain,(
% 0.17/0.51 individual(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f456,f167])).
% 0.17/0.51 fof(f458,plain,(
% 0.17/0.51 ~collection(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f457,f158])).
% 0.17/0.51 fof(f459,plain,(
% 0.17/0.51 ~fixedordercollection(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f458,f164])).
% 0.17/0.51 fof(f460,plain,(
% 0.17/0.51 ~firstordercollection(c_tptpcol_16_62187)),
% 0.17/0.51 inference(resolution,[status(thm)],[f459,f152])).
% 0.17/0.51 fof(f461,plain,(
% 0.17/0.51 $false),
% 0.17/0.51 inference(forward_subsumption_resolution,[status(thm)],[f460,f168])).
% 0.17/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.57 % Elapsed time: 0.094596 seconds
% 0.22/0.57 % CPU time: 0.094455 seconds
% 0.22/0.57 % Total memory used: 1.924 MB
% 0.22/0.57 % Net memory used: 1.923 MB
%------------------------------------------------------------------------------