%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR029+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 : n017.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:38 PM UTC 2026
% Result : Theorem 0.09s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR029+1 : 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.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 14:20:27 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.39 % Refutation found
% 0.09/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.39 fof(f5,axiom,(
% 0.09/0.39 (! [ARG1,ARG2] :( geographicalsubregions(ARG1,ARG2)=> inregion(ARG2,ARG1) ) )),
% 0.09/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f8,axiom,(
% 0.09/0.39 genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt) ),
% 0.09/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f9,axiom,(
% 0.09/0.39 genlmt(c_tptpgeo_member3_mt,c_tptpgeo_spindleheadmt) ),
% 0.09/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f10,axiom,(
% 0.09/0.39 ( mtvisible(c_worldgeographymt)=> geolevel_3(c_georegion_l3_x4_y13) ) ),
% 0.09/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f11,axiom,(
% 0.09/0.39 ( mtvisible(c_tptpgeo_member3_mt)=> geographicalsubregions(c_georegion_l3_x4_y13,c_georegion_l4_x14_y39) ) ),
% 0.09/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f12,axiom,(
% 0.09/0.39 ( mtvisible(c_tptpgeo_member3_mt)=> inregion(c_geolocation_x14_y39,c_georegion_l4_x14_y39) ) ),
% 0.09/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f41,axiom,(
% 0.09/0.39 (! [X,Y,Z] :( ( inregion(X,Y)& inregion(Y,Z) )=> inregion(X,Z) ) )),
% 0.09/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f49,axiom,(
% 0.09/0.39 (! [SPECMT,GENLMT] :( ( mtvisible(SPECMT)& genlmt(SPECMT,GENLMT) )=> mtvisible(GENLMT) ) )),
% 0.09/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f58,conjecture,(
% 0.09/0.39 ( mtvisible(c_tptpgeo_member3_mt)=> ( inregion(c_geolocation_x14_y39,c_georegion_l3_x4_y13)& geolevel_3(c_georegion_l3_x4_y13) ) ) ),
% 0.09/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f59,negated_conjecture,(
% 0.09/0.39 ~(( mtvisible(c_tptpgeo_member3_mt)=> ( inregion(c_geolocation_x14_y39,c_georegion_l3_x4_y13)& geolevel_3(c_georegion_l3_x4_y13) ) ) )),
% 0.09/0.39 inference(negated_conjecture,[status(cth)],[f58])).
% 0.09/0.39 fof(f64,plain,(
% 0.09/0.39 ![ARG1,ARG2]: (~geographicalsubregions(ARG1,ARG2)|inregion(ARG2,ARG1))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.09/0.39 fof(f65,plain,(
% 0.09/0.39 ![X0,X1]: (~geographicalsubregions(X0,X1)|inregion(X1,X0))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f64])).
% 0.09/0.39 fof(f68,plain,(
% 0.09/0.39 genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f8])).
% 0.09/0.39 fof(f69,plain,(
% 0.09/0.39 genlmt(c_tptpgeo_member3_mt,c_tptpgeo_spindleheadmt)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f9])).
% 0.09/0.39 fof(f70,plain,(
% 0.09/0.39 ~mtvisible(c_worldgeographymt)|geolevel_3(c_georegion_l3_x4_y13)),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.09/0.39 fof(f71,plain,(
% 0.09/0.39 ~mtvisible(c_worldgeographymt)|geolevel_3(c_georegion_l3_x4_y13)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f70])).
% 0.09/0.39 fof(f72,plain,(
% 0.09/0.39 ~mtvisible(c_tptpgeo_member3_mt)|geographicalsubregions(c_georegion_l3_x4_y13,c_georegion_l4_x14_y39)),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.09/0.39 fof(f73,plain,(
% 0.09/0.39 ~mtvisible(c_tptpgeo_member3_mt)|geographicalsubregions(c_georegion_l3_x4_y13,c_georegion_l4_x14_y39)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f72])).
% 0.09/0.39 fof(f74,plain,(
% 0.09/0.39 ~mtvisible(c_tptpgeo_member3_mt)|inregion(c_geolocation_x14_y39,c_georegion_l4_x14_y39)),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.09/0.39 fof(f75,plain,(
% 0.09/0.39 ~mtvisible(c_tptpgeo_member3_mt)|inregion(c_geolocation_x14_y39,c_georegion_l4_x14_y39)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f74])).
% 0.09/0.39 fof(f152,plain,(
% 0.09/0.39 ![X,Y,Z]: ((~inregion(X,Y)|~inregion(Y,Z))|inregion(X,Z))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.09/0.39 fof(f153,plain,(
% 0.09/0.39 ![X,Z]: ((![Y]: (~inregion(X,Y)|~inregion(Y,Z)))|inregion(X,Z))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f152])).
% 0.09/0.39 fof(f154,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~inregion(X0,X1)|~inregion(X1,X2)|inregion(X0,X2))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f153])).
% 0.09/0.39 fof(f173,plain,(
% 0.09/0.39 ![SPECMT,GENLMT]: ((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.09/0.39 fof(f174,plain,(
% 0.09/0.39 ![GENLMT]: ((![SPECMT]: (~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT)))|mtvisible(GENLMT))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f173])).
% 0.09/0.39 fof(f175,plain,(
% 0.09/0.39 ![X0,X1]: (~mtvisible(X0)|~genlmt(X0,X1)|mtvisible(X1))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f174])).
% 0.09/0.39 fof(f196,plain,(
% 0.09/0.39 (mtvisible(c_tptpgeo_member3_mt)&(~inregion(c_geolocation_x14_y39,c_georegion_l3_x4_y13)|~geolevel_3(c_georegion_l3_x4_y13)))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.09/0.39 fof(f197,plain,(
% 0.09/0.39 mtvisible(c_tptpgeo_member3_mt)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f196])).
% 0.09/0.39 fof(f198,plain,(
% 0.09/0.39 ~inregion(c_geolocation_x14_y39,c_georegion_l3_x4_y13)|~geolevel_3(c_georegion_l3_x4_y13)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f196])).
% 0.09/0.39 fof(f199,plain,(
% 0.09/0.39 inregion(c_geolocation_x14_y39,c_georegion_l4_x14_y39)),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f75,f197])).
% 0.09/0.39 fof(f200,plain,(
% 0.09/0.39 ![X0]: (~inregion(c_georegion_l4_x14_y39,X0)|inregion(c_geolocation_x14_y39,X0))),
% 0.09/0.39 inference(resolution,[status(thm)],[f154,f199])).
% 0.09/0.39 fof(f204,plain,(
% 0.09/0.39 ~mtvisible(c_tptpgeo_spindleheadmt)|mtvisible(c_worldgeographymt)),
% 0.09/0.39 inference(resolution,[status(thm)],[f68,f175])).
% 0.09/0.39 fof(f205,plain,(
% 0.09/0.39 ~mtvisible(c_tptpgeo_member3_mt)|mtvisible(c_tptpgeo_spindleheadmt)),
% 0.09/0.39 inference(resolution,[status(thm)],[f69,f175])).
% 0.09/0.39 fof(f206,plain,(
% 0.09/0.39 mtvisible(c_tptpgeo_spindleheadmt)),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f205,f197])).
% 0.09/0.39 fof(f208,plain,(
% 0.09/0.39 mtvisible(c_worldgeographymt)),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f204,f206])).
% 0.09/0.39 fof(f209,plain,(
% 0.09/0.39 ~inregion(c_geolocation_x14_y39,c_georegion_l3_x4_y13)),
% 0.09/0.39 inference(backward_subsumption_resolution,[status(thm)],[f198,f210])).
% 0.09/0.39 fof(f210,plain,(
% 0.09/0.39 geolevel_3(c_georegion_l3_x4_y13)),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f71,f208])).
% 0.09/0.39 fof(f211,plain,(
% 0.09/0.39 geographicalsubregions(c_georegion_l3_x4_y13,c_georegion_l4_x14_y39)),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f73,f197])).
% 0.09/0.39 fof(f212,plain,(
% 0.09/0.39 inregion(c_georegion_l4_x14_y39,c_georegion_l3_x4_y13)),
% 0.09/0.39 inference(resolution,[status(thm)],[f211,f65])).
% 0.09/0.39 fof(f213,plain,(
% 0.09/0.39 inregion(c_geolocation_x14_y39,c_georegion_l3_x4_y13)),
% 0.09/0.39 inference(resolution,[status(thm)],[f212,f200])).
% 0.09/0.39 fof(f215,plain,(
% 0.09/0.39 $false),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f213,f209])).
% 0.09/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.42 % Elapsed time: 0.055466 seconds
% 0.14/0.42 % CPU time: 0.145003 seconds
% 0.14/0.42 % Total memory used: 57.059 MB
% 0.14/0.42 % Net memory used: 57.042 MB
%------------------------------------------------------------------------------