%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR074+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 : n018.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:15:01 PM UTC 2026
% Result : Theorem 0.12s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR074+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n018.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 14:48:29 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.38 % Refutation found
% 0.12/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.38 fof(f5,axiom,(
% 0.12/0.38 (! [ARG1,ARG2] :( geographicalsubregions(ARG1,ARG2)=> inregion(ARG2,ARG1) ) )),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f8,axiom,(
% 0.12/0.38 genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt) ),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f9,axiom,(
% 0.12/0.38 genlmt(c_tptpgeo_member7_mt,c_tptpgeo_spindleheadmt) ),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f10,axiom,(
% 0.12/0.38 ( mtvisible(c_worldgeographymt)=> geolevel_3(c_georegion_l3_x17_y24) ) ),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f11,axiom,(
% 0.12/0.38 ( mtvisible(c_tptpgeo_member7_mt)=> geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74) ) ),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f12,axiom,(
% 0.12/0.38 ( mtvisible(c_tptpgeo_member7_mt)=> inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74) ) ),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f41,axiom,(
% 0.12/0.38 (! [X,Y,Z] :( ( inregion(X,Y)& inregion(Y,Z) )=> inregion(X,Z) ) )),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f49,axiom,(
% 0.12/0.38 (! [SPECMT,GENLMT] :( ( mtvisible(SPECMT)& genlmt(SPECMT,GENLMT) )=> mtvisible(GENLMT) ) )),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f58,conjecture,(
% 0.12/0.38 ( mtvisible(c_tptpgeo_member7_mt)=> ( inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)& geolevel_3(c_georegion_l3_x17_y24) ) ) ),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f59,negated_conjecture,(
% 0.12/0.38 ~(( mtvisible(c_tptpgeo_member7_mt)=> ( inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)& geolevel_3(c_georegion_l3_x17_y24) ) ) )),
% 0.12/0.38 inference(negated_conjecture,[status(cth)],[f58])).
% 0.12/0.38 fof(f64,plain,(
% 0.12/0.38 ![ARG1,ARG2]: (~geographicalsubregions(ARG1,ARG2)|inregion(ARG2,ARG1))),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.12/0.38 fof(f65,plain,(
% 0.12/0.38 ![X0,X1]: (~geographicalsubregions(X0,X1)|inregion(X1,X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f64])).
% 0.12/0.38 fof(f68,plain,(
% 0.12/0.38 genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.38 fof(f69,plain,(
% 0.12/0.38 genlmt(c_tptpgeo_member7_mt,c_tptpgeo_spindleheadmt)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.38 fof(f70,plain,(
% 0.12/0.38 ~mtvisible(c_worldgeographymt)|geolevel_3(c_georegion_l3_x17_y24)),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.12/0.38 fof(f71,plain,(
% 0.12/0.38 ~mtvisible(c_worldgeographymt)|geolevel_3(c_georegion_l3_x17_y24)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f70])).
% 0.12/0.38 fof(f72,plain,(
% 0.12/0.38 ~mtvisible(c_tptpgeo_member7_mt)|geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74)),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.12/0.38 fof(f73,plain,(
% 0.12/0.38 ~mtvisible(c_tptpgeo_member7_mt)|geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f72])).
% 0.12/0.38 fof(f74,plain,(
% 0.12/0.38 ~mtvisible(c_tptpgeo_member7_mt)|inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74)),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.12/0.38 fof(f75,plain,(
% 0.12/0.38 ~mtvisible(c_tptpgeo_member7_mt)|inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f74])).
% 0.12/0.38 fof(f152,plain,(
% 0.12/0.38 ![X,Y,Z]: ((~inregion(X,Y)|~inregion(Y,Z))|inregion(X,Z))),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.12/0.38 fof(f153,plain,(
% 0.12/0.38 ![X,Z]: ((![Y]: (~inregion(X,Y)|~inregion(Y,Z)))|inregion(X,Z))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f152])).
% 0.12/0.38 fof(f154,plain,(
% 0.12/0.38 ![X0,X1,X2]: (~inregion(X0,X1)|~inregion(X1,X2)|inregion(X0,X2))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f153])).
% 0.12/0.38 fof(f173,plain,(
% 0.12/0.38 ![SPECMT,GENLMT]: ((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT))),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.12/0.38 fof(f174,plain,(
% 0.12/0.38 ![GENLMT]: ((![SPECMT]: (~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT)))|mtvisible(GENLMT))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f173])).
% 0.12/0.38 fof(f175,plain,(
% 0.12/0.38 ![X0,X1]: (~mtvisible(X0)|~genlmt(X0,X1)|mtvisible(X1))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f174])).
% 0.12/0.38 fof(f196,plain,(
% 0.12/0.38 (mtvisible(c_tptpgeo_member7_mt)&(~inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)|~geolevel_3(c_georegion_l3_x17_y24)))),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.12/0.38 fof(f197,plain,(
% 0.12/0.38 mtvisible(c_tptpgeo_member7_mt)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f196])).
% 0.12/0.38 fof(f198,plain,(
% 0.12/0.38 ~inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)|~geolevel_3(c_georegion_l3_x17_y24)),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f196])).
% 0.12/0.38 fof(f199,plain,(
% 0.12/0.38 inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74)),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f75,f197])).
% 0.12/0.38 fof(f200,plain,(
% 0.12/0.38 ![X0]: (~inregion(c_georegion_l4_x53_y74,X0)|inregion(c_geolocation_x53_y74,X0))),
% 0.12/0.38 inference(resolution,[status(thm)],[f154,f199])).
% 0.12/0.38 fof(f204,plain,(
% 0.12/0.38 ~mtvisible(c_tptpgeo_spindleheadmt)|mtvisible(c_worldgeographymt)),
% 0.12/0.38 inference(resolution,[status(thm)],[f68,f175])).
% 0.12/0.38 fof(f205,plain,(
% 0.12/0.38 ~mtvisible(c_tptpgeo_member7_mt)|mtvisible(c_tptpgeo_spindleheadmt)),
% 0.12/0.38 inference(resolution,[status(thm)],[f69,f175])).
% 0.12/0.38 fof(f206,plain,(
% 0.12/0.38 mtvisible(c_tptpgeo_spindleheadmt)),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f205,f197])).
% 0.12/0.38 fof(f208,plain,(
% 0.12/0.38 mtvisible(c_worldgeographymt)),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f204,f206])).
% 0.12/0.38 fof(f209,plain,(
% 0.12/0.38 ~inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)),
% 0.12/0.38 inference(backward_subsumption_resolution,[status(thm)],[f198,f210])).
% 0.12/0.38 fof(f210,plain,(
% 0.12/0.38 geolevel_3(c_georegion_l3_x17_y24)),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f71,f208])).
% 0.12/0.38 fof(f211,plain,(
% 0.12/0.38 geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74)),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f73,f197])).
% 0.12/0.38 fof(f212,plain,(
% 0.12/0.38 inregion(c_georegion_l4_x53_y74,c_georegion_l3_x17_y24)),
% 0.12/0.38 inference(resolution,[status(thm)],[f211,f65])).
% 0.12/0.38 fof(f213,plain,(
% 0.12/0.38 inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)),
% 0.12/0.38 inference(resolution,[status(thm)],[f212,f200])).
% 0.12/0.38 fof(f215,plain,(
% 0.12/0.38 $false),
% 0.12/0.38 inference(forward_subsumption_resolution,[status(thm)],[f213,f209])).
% 0.12/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 1.27/1.59 % Elapsed time: 1.022826 seconds
% 1.27/1.59 % CPU time: 0.132337 seconds
% 1.27/1.59 % Total memory used: 48.203 MB
% 1.27/1.59 % Net memory used: 48.184 MB
%------------------------------------------------------------------------------