%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR033+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:40 PM UTC 2026
% Result : Theorem 0.39s 0.92s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR033+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:31:45 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.23/0.55 % Drodi V4.1.1
% 0.39/0.92 % Refutation found
% 0.39/0.92 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.39/0.92 % SZS output start CNFRefutation for theBenchmark
% 0.39/0.92 fof(f197,axiom,(
% 0.39/0.92 genlmt(c_tptpgeo_member3_mt,c_tptpgeo_spindleheadmt) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f232,axiom,(
% 0.39/0.92 genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member2_mt) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f438,axiom,(
% 0.39/0.92 ( mtvisible(c_tptpgeo_member2_mt)=> geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7) ) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f1039,axiom,(
% 0.39/0.92 ( mtvisible(c_tptpgeo_member2_mt)=> geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2) ) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f1111,axiom,(
% 0.39/0.92 genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f1458,axiom,(
% 0.39/0.92 genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member8_mt) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f1467,axiom,(
% 0.39/0.92 genlmt(c_worldgeographymt,c_geographymt) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f1935,axiom,(
% 0.39/0.92 (! [ARG1,ARG2] :( geographicalsubregions(ARG1,ARG2)=> inregion(ARG2,ARG1) ) )),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f2024,axiom,(
% 0.39/0.92 ( mtvisible(c_worldgeographymt)=> geolevel_1(c_georegion_l1_x2_y0) ) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f2217,axiom,(
% 0.39/0.92 genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member4_mt) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f2388,axiom,(
% 0.39/0.92 genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f2573,axiom,(
% 0.39/0.92 ( mtvisible(c_tptpgeo_member2_mt)=> geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23) ) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f2962,axiom,(
% 0.39/0.92 ( mtvisible(c_tptpgeo_member2_mt)=> inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23) ) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f3432,axiom,(
% 0.39/0.92 genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member3_mt) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f3556,axiom,(
% 0.39/0.92 genlmt(c_geographymt,c_geographyvocabularymt) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f7302,axiom,(
% 0.39/0.92 (! [X,Y,Z] :( ( inregion(X,Y)& inregion(Y,Z) )=> inregion(X,Z) ) )),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f7997,axiom,(
% 0.39/0.92 (! [SPECMT,GENLMT] :( ( mtvisible(SPECMT)& genlmt(SPECMT,GENLMT) )=> mtvisible(GENLMT) ) )),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f8006,conjecture,(
% 0.39/0.92 ( mtvisible(c_tptpgeo_spindlecollectormt)=> ( inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0)& geolevel_1(c_georegion_l1_x2_y0) ) ) ),
% 0.39/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.39/0.92 fof(f8007,negated_conjecture,(
% 0.39/0.92 ~(( mtvisible(c_tptpgeo_spindlecollectormt)=> ( inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0)& geolevel_1(c_georegion_l1_x2_y0) ) ) )),
% 0.39/0.92 inference(negated_conjecture,[status(cth)],[f8006])).
% 0.39/0.92 fof(f8266,plain,(
% 0.39/0.92 genlmt(c_tptpgeo_member3_mt,c_tptpgeo_spindleheadmt)),
% 0.39/0.92 inference(cnf_transformation,[status(thm)],[f197])).
% 0.39/0.92 fof(f8315,plain,(
% 0.39/0.92 genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member2_mt)),
% 0.39/0.92 inference(cnf_transformation,[status(thm)],[f232])).
% 0.39/0.92 fof(f8598,plain,(
% 0.39/0.92 ~mtvisible(c_tptpgeo_member2_mt)|geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7)),
% 0.39/0.92 inference(pre_NNF_transformation,[status(thm)],[f438])).
% 0.39/0.92 fof(f8599,plain,(
% 0.39/0.92 ~mtvisible(c_tptpgeo_member2_mt)|geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7)),
% 0.39/0.92 inference(cnf_transformation,[status(thm)],[f8598])).
% 0.39/0.92 fof(f9458,plain,(
% 0.39/0.92 ~mtvisible(c_tptpgeo_member2_mt)|geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2)),
% 0.39/0.92 inference(pre_NNF_transformation,[status(thm)],[f1039])).
% 0.39/0.92 fof(f9459,plain,(
% 0.39/0.92 ~mtvisible(c_tptpgeo_member2_mt)|geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f9458])).
% 0.39/0.93 fof(f9563,plain,(
% 0.39/0.93 genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f1111])).
% 0.39/0.93 fof(f10051,plain,(
% 0.39/0.93 genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member8_mt)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f1458])).
% 0.39/0.93 fof(f10065,plain,(
% 0.39/0.93 genlmt(c_worldgeographymt,c_geographymt)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f1467])).
% 0.39/0.93 fof(f10720,plain,(
% 0.39/0.93 ![ARG1,ARG2]: (~geographicalsubregions(ARG1,ARG2)|inregion(ARG2,ARG1))),
% 0.39/0.93 inference(pre_NNF_transformation,[status(thm)],[f1935])).
% 0.39/0.93 fof(f10721,plain,(
% 0.39/0.93 ![X0,X1]: (~geographicalsubregions(X0,X1)|inregion(X1,X0))),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f10720])).
% 0.39/0.93 fof(f10845,plain,(
% 0.39/0.93 ~mtvisible(c_worldgeographymt)|geolevel_1(c_georegion_l1_x2_y0)),
% 0.39/0.93 inference(pre_NNF_transformation,[status(thm)],[f2024])).
% 0.39/0.93 fof(f10846,plain,(
% 0.39/0.93 ~mtvisible(c_worldgeographymt)|geolevel_1(c_georegion_l1_x2_y0)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f10845])).
% 0.39/0.93 fof(f11117,plain,(
% 0.39/0.93 genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member4_mt)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f2217])).
% 0.39/0.93 fof(f11351,plain,(
% 0.39/0.93 genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f2388])).
% 0.39/0.93 fof(f11610,plain,(
% 0.39/0.93 ~mtvisible(c_tptpgeo_member2_mt)|geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23)),
% 0.39/0.93 inference(pre_NNF_transformation,[status(thm)],[f2573])).
% 0.39/0.93 fof(f11611,plain,(
% 0.39/0.93 ~mtvisible(c_tptpgeo_member2_mt)|geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f11610])).
% 0.39/0.93 fof(f12153,plain,(
% 0.39/0.93 ~mtvisible(c_tptpgeo_member2_mt)|inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23)),
% 0.39/0.93 inference(pre_NNF_transformation,[status(thm)],[f2962])).
% 0.39/0.93 fof(f12154,plain,(
% 0.39/0.93 ~mtvisible(c_tptpgeo_member2_mt)|inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f12153])).
% 0.39/0.93 fof(f12808,plain,(
% 0.39/0.93 genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member3_mt)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f3432])).
% 0.39/0.93 fof(f12980,plain,(
% 0.39/0.93 genlmt(c_geographymt,c_geographyvocabularymt)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f3556])).
% 0.39/0.93 fof(f19970,plain,(
% 0.39/0.93 ![X,Y,Z]: ((~inregion(X,Y)|~inregion(Y,Z))|inregion(X,Z))),
% 0.39/0.93 inference(pre_NNF_transformation,[status(thm)],[f7302])).
% 0.39/0.93 fof(f19971,plain,(
% 0.39/0.93 ![X,Z]: ((![Y]: (~inregion(X,Y)|~inregion(Y,Z)))|inregion(X,Z))),
% 0.39/0.93 inference(miniscoping,[status(thm)],[f19970])).
% 0.39/0.93 fof(f19972,plain,(
% 0.39/0.93 ![X0,X1,X2]: (~inregion(X0,X1)|~inregion(X1,X2)|inregion(X0,X2))),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f19971])).
% 0.39/0.93 fof(f21368,plain,(
% 0.39/0.93 ![SPECMT,GENLMT]: ((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT))),
% 0.39/0.93 inference(pre_NNF_transformation,[status(thm)],[f7997])).
% 0.39/0.93 fof(f21369,plain,(
% 0.39/0.93 ![GENLMT]: ((![SPECMT]: (~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT)))|mtvisible(GENLMT))),
% 0.39/0.93 inference(miniscoping,[status(thm)],[f21368])).
% 0.39/0.93 fof(f21370,plain,(
% 0.39/0.93 ![X0,X1]: (~mtvisible(X0)|~genlmt(X0,X1)|mtvisible(X1))),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f21369])).
% 0.39/0.93 fof(f21391,plain,(
% 0.39/0.93 (mtvisible(c_tptpgeo_spindlecollectormt)&(~inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0)|~geolevel_1(c_georegion_l1_x2_y0)))),
% 0.39/0.93 inference(pre_NNF_transformation,[status(thm)],[f8007])).
% 0.39/0.93 fof(f21392,plain,(
% 0.39/0.93 mtvisible(c_tptpgeo_spindlecollectormt)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f21391])).
% 0.39/0.93 fof(f21393,plain,(
% 0.39/0.93 ~inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0)|~geolevel_1(c_georegion_l1_x2_y0)),
% 0.39/0.93 inference(cnf_transformation,[status(thm)],[f21391])).
% 0.39/0.93 fof(f21416,definition,(
% 0.39/0.93 sQ6_spl <=> (mtvisible(c_worldgeographymt))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f21418,plain,(
% 0.39/0.93 ~mtvisible(c_worldgeographymt)|sQ6_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f21416])).
% 0.39/0.93 fof(f21434,definition,(
% 0.39/0.93 sQ11_spl <=> (mtvisible(c_tptpgeo_member2_mt))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f21436,plain,(
% 0.39/0.93 ~mtvisible(c_tptpgeo_member2_mt)|sQ11_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f21434])).
% 0.39/0.93 fof(f21513,definition,(
% 0.39/0.93 sQ33_spl <=> (mtvisible(c_tptpgeo_member4_mt))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f21515,plain,(
% 0.39/0.93 ~mtvisible(c_tptpgeo_member4_mt)|sQ33_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f21513])).
% 0.39/0.93 fof(f21716,definition,(
% 0.39/0.93 sQ88_spl <=> (geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f21717,plain,(
% 0.39/0.93 geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7)|~sQ88_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f21716])).
% 0.39/0.93 fof(f21719,plain,(
% 0.39/0.93 ~sQ11_spl|sQ88_spl),
% 0.39/0.93 inference(split_clause,[status(thm)],[f8599,f21434,f21716])).
% 0.39/0.93 fof(f21751,definition,(
% 0.39/0.93 sQ97_spl <=> (mtvisible(c_tptpgeo_member5_mt))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f21753,plain,(
% 0.39/0.93 ~mtvisible(c_tptpgeo_member5_mt)|sQ97_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f21751])).
% 0.39/0.93 fof(f22254,definition,(
% 0.39/0.93 sQ230_spl <=> (geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f22255,plain,(
% 0.39/0.93 geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2)|~sQ230_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f22254])).
% 0.39/0.93 fof(f22257,plain,(
% 0.39/0.93 ~sQ11_spl|sQ230_spl),
% 0.39/0.93 inference(split_clause,[status(thm)],[f9459,f21434,f22254])).
% 0.39/0.93 fof(f22564,definition,(
% 0.39/0.93 sQ310_spl <=> (mtvisible(c_tptpgeo_member8_mt))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f22566,plain,(
% 0.39/0.93 ~mtvisible(c_tptpgeo_member8_mt)|sQ310_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f22564])).
% 0.39/0.93 fof(f22968,definition,(
% 0.39/0.93 sQ416_spl <=> (geolevel_1(c_georegion_l1_x2_y0))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ416_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f22971,plain,(
% 0.39/0.93 ~sQ6_spl|sQ416_spl),
% 0.39/0.93 inference(split_clause,[status(thm)],[f10846,f21416,f22968])).
% 0.39/0.93 fof(f23355,definition,(
% 0.39/0.93 sQ514_spl <=> (geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ514_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f23356,plain,(
% 0.39/0.93 geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23)|~sQ514_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f23355])).
% 0.39/0.93 fof(f23358,plain,(
% 0.39/0.93 ~sQ11_spl|sQ514_spl),
% 0.39/0.93 inference(split_clause,[status(thm)],[f11611,f21434,f23355])).
% 0.39/0.93 fof(f23612,definition,(
% 0.39/0.93 sQ578_spl <=> (inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f23613,plain,(
% 0.39/0.93 inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23)|~sQ578_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f23612])).
% 0.39/0.93 fof(f23615,plain,(
% 0.39/0.93 ~sQ11_spl|sQ578_spl),
% 0.39/0.93 inference(split_clause,[status(thm)],[f12154,f21434,f23612])).
% 0.39/0.93 fof(f24490,definition,(
% 0.39/0.93 sQ799_spl <=> (mtvisible(c_geographyvocabularymt))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ799_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f24492,plain,(
% 0.39/0.93 ~mtvisible(c_geographyvocabularymt)|sQ799_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f24490])).
% 0.39/0.93 fof(f24603,definition,(
% 0.39/0.93 sQ827_spl <=> (inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0))),
% 0.39/0.93 introduced(definition,[new_symbols(definition,[sQ827_spl])],[split_symbol_definition])).
% 0.39/0.93 fof(f24605,plain,(
% 0.39/0.93 ~inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0)|sQ827_spl),
% 0.39/0.93 inference(component_clause,[status(thm)],[f24603])).
% 0.39/0.93 fof(f24606,plain,(
% 0.39/0.93 ~sQ827_spl|~sQ416_spl),
% 0.39/0.93 inference(split_clause,[status(thm)],[f21393,f24603,f22968])).
% 0.39/0.93 fof(f24607,plain,(
% 0.39/0.93 ![X0]: (~genlmt(c_tptpgeo_spindlecollectormt,X0)|mtvisible(X0))),
% 0.39/0.93 inference(resolution,[status(thm)],[f21370,f21392])).
% 0.39/0.93 fof(f24609,plain,(
% 0.39/0.93 mtvisible(c_tptpgeo_member3_mt)),
% 0.39/0.93 inference(resolution,[status(thm)],[f24607,f12808])).
% 0.39/0.93 fof(f24612,plain,(
% 0.39/0.93 mtvisible(c_tptpgeo_member2_mt)),
% 0.39/0.93 inference(resolution,[status(thm)],[f24607,f8315])).
% 0.39/0.93 fof(f24614,plain,(
% 0.39/0.93 ![X0]: (~genlmt(c_tptpgeo_member3_mt,X0)|mtvisible(X0))),
% 0.39/0.93 inference(resolution,[status(thm)],[f24609,f21370])).
% 0.39/0.93 fof(f24625,plain,(
% 0.39/0.93 mtvisible(c_tptpgeo_spindleheadmt)),
% 0.39/0.93 inference(resolution,[status(thm)],[f8266,f24614])).
% 0.39/0.93 fof(f24626,plain,(
% 0.39/0.93 ![X0]: (~genlmt(c_tptpgeo_spindleheadmt,X0)|mtvisible(X0))),
% 0.39/0.93 inference(resolution,[status(thm)],[f24625,f21370])).
% 0.39/0.93 fof(f24632,plain,(
% 0.39/0.93 $false|sQ11_spl),
% 0.39/0.93 inference(forward_subsumption_resolution,[status(thm)],[f21436,f24612])).
% 0.39/0.93 fof(f24633,plain,(
% 0.39/0.93 sQ11_spl),
% 0.39/0.93 inference(contradiction_clause,[status(thm)],[f24632])).
% 0.39/0.93 fof(f25297,plain,(
% 0.39/0.93 mtvisible(c_worldgeographymt)),
% 0.39/0.93 inference(resolution,[status(thm)],[f9563,f24626])).
% 0.39/0.93 fof(f25298,plain,(
% 0.39/0.93 $false|sQ6_spl),
% 0.39/0.93 inference(forward_subsumption_resolution,[status(thm)],[f25297,f21418])).
% 0.39/0.93 fof(f25299,plain,(
% 0.39/0.93 sQ6_spl),
% 0.39/0.93 inference(contradiction_clause,[status(thm)],[f25298])).
% 0.39/0.93 fof(f25300,plain,(
% 0.39/0.93 ![X0]: (~genlmt(c_worldgeographymt,X0)|mtvisible(X0))),
% 0.39/0.93 inference(resolution,[status(thm)],[f25297,f21370])).
% 0.39/0.93 fof(f25467,plain,(
% 0.39/0.93 mtvisible(c_tptpgeo_member8_mt)),
% 0.39/0.93 inference(resolution,[status(thm)],[f10051,f24607])).
% 0.39/0.93 fof(f25468,plain,(
% 0.39/0.93 $false|sQ310_spl),
% 0.39/0.93 inference(forward_subsumption_resolution,[status(thm)],[f25467,f22566])).
% 0.39/0.93 fof(f25469,plain,(
% 0.39/0.93 sQ310_spl),
% 0.39/0.93 inference(contradiction_clause,[status(thm)],[f25468])).
% 0.39/0.93 fof(f25474,plain,(
% 0.39/0.93 mtvisible(c_geographymt)),
% 0.39/0.93 inference(resolution,[status(thm)],[f10065,f25300])).
% 0.39/0.93 fof(f25475,plain,(
% 0.39/0.93 ![X0]: (~genlmt(c_geographymt,X0)|mtvisible(X0))),
% 0.39/0.93 inference(resolution,[status(thm)],[f25474,f21370])).
% 0.39/0.93 fof(f25792,plain,(
% 0.39/0.93 mtvisible(c_tptpgeo_member4_mt)),
% 0.39/0.93 inference(resolution,[status(thm)],[f11117,f24607])).
% 0.39/0.93 fof(f25793,plain,(
% 0.39/0.93 $false|sQ33_spl),
% 0.39/0.93 inference(forward_subsumption_resolution,[status(thm)],[f25792,f21515])).
% 0.39/0.93 fof(f25794,plain,(
% 0.39/0.93 sQ33_spl),
% 0.39/0.93 inference(contradiction_clause,[status(thm)],[f25793])).
% 0.39/0.93 fof(f25869,plain,(
% 0.39/0.93 mtvisible(c_tptpgeo_member5_mt)),
% 0.39/0.93 inference(resolution,[status(thm)],[f11351,f24607])).
% 0.39/0.93 fof(f25870,plain,(
% 0.39/0.93 $false|sQ97_spl),
% 0.39/0.93 inference(forward_subsumption_resolution,[status(thm)],[f25869,f21753])).
% 0.39/0.93 fof(f25871,plain,(
% 0.39/0.93 sQ97_spl),
% 0.39/0.93 inference(contradiction_clause,[status(thm)],[f25870])).
% 0.39/0.93 fof(f28121,plain,(
% 0.39/0.93 mtvisible(c_geographyvocabularymt)),
% 0.39/0.93 inference(resolution,[status(thm)],[f12980,f25475])).
% 0.39/0.93 fof(f28122,plain,(
% 0.39/0.93 $false|sQ799_spl),
% 0.39/0.93 inference(forward_subsumption_resolution,[status(thm)],[f28121,f24492])).
% 0.39/0.93 fof(f28123,plain,(
% 0.39/0.93 sQ799_spl),
% 0.39/0.93 inference(contradiction_clause,[status(thm)],[f28122])).
% 0.39/0.93 fof(f29231,plain,(
% 0.39/0.93 inregion(c_georegion_l3_x25_y7,c_georegion_l2_x8_y2)|~sQ88_spl),
% 0.39/0.93 inference(resolution,[status(thm)],[f21717,f10721])).
% 0.39/0.93 fof(f29246,plain,(
% 0.39/0.93 ![X0]: (~inregion(X0,c_georegion_l3_x25_y7)|inregion(X0,c_georegion_l2_x8_y2)|~sQ88_spl)),
% 0.39/0.93 inference(resolution,[status(thm)],[f29231,f19972])).
% 0.39/0.93 fof(f29255,plain,(
% 0.39/0.93 inregion(c_georegion_l2_x8_y2,c_georegion_l1_x2_y0)|~sQ230_spl),
% 0.39/0.93 inference(resolution,[status(thm)],[f22255,f10721])).
% 0.39/0.93 fof(f29263,plain,(
% 0.39/0.93 ![X0]: (~inregion(X0,c_georegion_l2_x8_y2)|inregion(X0,c_georegion_l1_x2_y0)|~sQ230_spl)),
% 0.39/0.93 inference(resolution,[status(thm)],[f29255,f19972])).
% 0.39/0.93 fof(f29314,plain,(
% 0.39/0.93 inregion(c_georegion_l4_x76_y23,c_georegion_l3_x25_y7)|~sQ514_spl),
% 0.39/0.93 inference(resolution,[status(thm)],[f23356,f10721])).
% 0.39/0.93 fof(f29401,plain,(
% 0.39/0.93 inregion(c_georegion_l4_x76_y23,c_georegion_l2_x8_y2)|~sQ88_spl|~sQ514_spl),
% 0.39/0.93 inference(resolution,[status(thm)],[f29246,f29314])).
% 0.39/0.93 fof(f29447,plain,(
% 0.39/0.93 ![X0]: (~inregion(X0,c_georegion_l4_x76_y23)|inregion(X0,c_georegion_l2_x8_y2)|~sQ88_spl|~sQ514_spl)),
% 0.39/0.93 inference(resolution,[status(thm)],[f29401,f19972])).
% 0.39/0.93 fof(f29541,plain,(
% 0.39/0.93 ~inregion(c_geolocation_x76_y23,c_georegion_l2_x8_y2)|~sQ230_spl|sQ827_spl),
% 0.39/0.93 inference(resolution,[status(thm)],[f29263,f24605])).
% 0.39/0.93 fof(f29803,plain,(
% 0.39/0.93 inregion(c_geolocation_x76_y23,c_georegion_l2_x8_y2)|~sQ88_spl|~sQ514_spl|~sQ578_spl),
% 0.39/0.93 inference(resolution,[status(thm)],[f29447,f23613])).
% 0.39/1.00 fof(f29804,plain,(
% 0.39/1.00 $false|~sQ230_spl|sQ827_spl|~sQ88_spl|~sQ514_spl|~sQ578_spl),
% 0.39/1.00 inference(forward_subsumption_resolution,[status(thm)],[f29803,f29541])).
% 0.39/1.00 fof(f29805,plain,(
% 0.39/1.00 ~sQ230_spl|sQ827_spl|~sQ88_spl|~sQ514_spl|~sQ578_spl),
% 0.39/1.00 inference(contradiction_clause,[status(thm)],[f29804])).
% 0.39/1.00 fof(f29806,plain,(
% 0.39/1.00 $false),
% 0.39/1.00 inference(sat_refutation,[status(thm)],[f21719,f22257,f22971,f23358,f23615,f24606,f24633,f25299,f25469,f25794,f25871,f28123,f29805])).
% 0.39/1.00 % SZS output end CNFRefutation for theBenchmark.p
% 2.61/2.18 % Elapsed time: 1.568750 seconds
% 2.61/2.18 % CPU time: 2.909434 seconds
% 2.61/2.18 % Total memory used: 415.070 MB
% 2.61/2.18 % Net memory used: 414.253 MB
%------------------------------------------------------------------------------