%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR034+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:41 PM UTC 2026
% Result : Theorem 4.85s 1.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR034+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.35 % Computer : n004.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8046.5625MB
% 0.12/0.35 % OS : Linux 6.8.0-71-generic
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Mon Sep 21 14:27:34 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.23/0.53 % Drodi V4.1.1
% 4.85/1.23 % Refutation found
% 4.85/1.23 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.85/1.23 % SZS output start CNFRefutation for theBenchmark
% 4.85/1.23 fof(f1059,axiom,(
% 4.85/1.23 genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt) ),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f2492,axiom,(
% 4.85/1.23 ( mtvisible(c_worldgeographymt)=> state_geopolitical(c_wanica_districtsuriname) ) ),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f2826,axiom,(
% 4.85/1.23 genlmt(c_worldgeographydualistmt,c_worldgeographymt) ),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f3401,axiom,(
% 4.85/1.23 genlmt(c_cyclistsmt,c_austinareamt) ),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f3681,axiom,(
% 4.85/1.23 genlmt(c_austinareamt,c_unitedstatesgeographydualistmt) ),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f3734,axiom,(
% 4.85/1.23 genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt) ),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f3888,axiom,(
% 4.85/1.23 (! [OBJ] :( state_geopolitical(OBJ)=> firstorderadministrativedivision(OBJ) ) )),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f4288,axiom,(
% 4.85/1.23 genlmt(c_tptp_spindleheadmt,c_cyclistsmt) ),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f6228,axiom,(
% 4.85/1.23 (! [X] :( firstorderadministrativedivision(X)=> isa(X,c_firstorderadministrativedivision) ) )),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f7997,axiom,(
% 4.85/1.23 (! [SPECMT,GENLMT] :( ( mtvisible(SPECMT)& genlmt(SPECMT,GENLMT) )=> mtvisible(GENLMT) ) )),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f8006,conjecture,(
% 4.85/1.23 (? [COL] :( mtvisible(c_tptp_member3515_mt)=> isa(c_wanica_districtsuriname,COL) ) )),
% 4.85/1.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.85/1.23 fof(f8007,negated_conjecture,(
% 4.85/1.23 ~((? [COL] :( mtvisible(c_tptp_member3515_mt)=> isa(c_wanica_districtsuriname,COL) ) ))),
% 4.85/1.23 inference(negated_conjecture,[status(cth)],[f8006])).
% 4.85/1.23 fof(f9486,plain,(
% 4.85/1.23 genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt)),
% 4.85/1.23 inference(cnf_transformation,[status(thm)],[f1059])).
% 4.85/1.23 fof(f11493,plain,(
% 4.85/1.23 ~mtvisible(c_worldgeographymt)|state_geopolitical(c_wanica_districtsuriname)),
% 4.85/1.23 inference(pre_NNF_transformation,[status(thm)],[f2492])).
% 4.85/1.23 fof(f11494,plain,(
% 4.85/1.23 ~mtvisible(c_worldgeographymt)|state_geopolitical(c_wanica_districtsuriname)),
% 4.85/1.23 inference(cnf_transformation,[status(thm)],[f11493])).
% 4.85/1.23 fof(f11960,plain,(
% 4.85/1.23 genlmt(c_worldgeographydualistmt,c_worldgeographymt)),
% 4.85/1.23 inference(cnf_transformation,[status(thm)],[f2826])).
% 4.85/1.23 fof(f12766,plain,(
% 4.85/1.23 genlmt(c_cyclistsmt,c_austinareamt)),
% 4.85/1.23 inference(cnf_transformation,[status(thm)],[f3401])).
% 4.85/1.23 fof(f13147,plain,(
% 4.85/1.23 genlmt(c_austinareamt,c_unitedstatesgeographydualistmt)),
% 4.85/1.23 inference(cnf_transformation,[status(thm)],[f3681])).
% 4.85/1.23 fof(f13224,plain,(
% 4.85/1.23 genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt)),
% 4.85/1.23 inference(cnf_transformation,[status(thm)],[f3734])).
% 4.85/1.23 fof(f13433,plain,(
% 4.85/1.23 ![OBJ]: (~state_geopolitical(OBJ)|firstorderadministrativedivision(OBJ))),
% 4.85/1.23 inference(pre_NNF_transformation,[status(thm)],[f3888])).
% 4.85/1.23 fof(f13434,plain,(
% 4.85/1.23 ![X0]: (~state_geopolitical(X0)|firstorderadministrativedivision(X0))),
% 4.85/1.23 inference(cnf_transformation,[status(thm)],[f13433])).
% 4.85/1.23 fof(f14003,plain,(
% 4.85/1.23 genlmt(c_tptp_spindleheadmt,c_cyclistsmt)),
% 4.85/1.23 inference(cnf_transformation,[status(thm)],[f4288])).
% 4.85/1.23 fof(f17816,plain,(
% 4.85/1.23 ![X]: (~firstorderadministrativedivision(X)|isa(X,c_firstorderadministrativedivision))),
% 4.85/1.23 inference(pre_NNF_transformation,[status(thm)],[f6228])).
% 4.85/1.23 fof(f17817,plain,(
% 4.85/1.23 ![X0]: (~firstorderadministrativedivision(X0)|isa(X0,c_firstorderadministrativedivision))),
% 4.85/1.23 inference(cnf_transformation,[status(thm)],[f17816])).
% 4.85/1.23 fof(f21368,plain,(
% 4.85/1.23 ![SPECMT,GENLMT]: ((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT))),
% 4.85/1.23 inference(pre_NNF_transformation,[status(thm)],[f7997])).
% 4.85/1.23 fof(f21369,plain,(
% 4.85/1.23 ![GENLMT]: ((![SPECMT]: (~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT)))|mtvisible(GENLMT))),
% 4.85/1.23 inference(miniscoping,[status(thm)],[f21368])).
% 4.85/1.23 fof(f21370,plain,(
% 4.85/1.23 ![X0,X1]: (~mtvisible(X0)|~genlmt(X0,X1)|mtvisible(X1))),
% 3.53/1.33 inference(cnf_transformation,[status(thm)],[f21369])).
% 3.53/1.33 fof(f21391,plain,(
% 3.53/1.33 (![COL]: (mtvisible(c_tptp_member3515_mt)&~isa(c_wanica_districtsuriname,COL)))),
% 3.53/1.33 inference(pre_NNF_transformation,[status(thm)],[f8007])).
% 3.53/1.33 fof(f21392,plain,(
% 3.53/1.33 mtvisible(c_tptp_member3515_mt)&(![COL]: ~isa(c_wanica_districtsuriname,COL))),
% 3.53/1.33 inference(miniscoping,[status(thm)],[f21391])).
% 3.53/1.33 fof(f21393,plain,(
% 3.53/1.33 mtvisible(c_tptp_member3515_mt)),
% 3.53/1.33 inference(cnf_transformation,[status(thm)],[f21392])).
% 3.53/1.33 fof(f21394,plain,(
% 3.53/1.33 ![X0]: (~isa(c_wanica_districtsuriname,X0))),
% 3.53/1.33 inference(cnf_transformation,[status(thm)],[f21392])).
% 3.53/1.33 fof(f21417,definition,(
% 3.53/1.33 sQ6_spl <=> (mtvisible(c_worldgeographymt))),
% 3.53/1.33 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 3.53/1.33 fof(f21419,plain,(
% 3.53/1.33 ~mtvisible(c_worldgeographymt)|sQ6_spl),
% 3.53/1.33 inference(component_clause,[status(thm)],[f21417])).
% 3.53/1.33 fof(f22916,definition,(
% 3.53/1.33 sQ402_spl <=> (state_geopolitical(c_wanica_districtsuriname))),
% 3.53/1.33 introduced(definition,[new_symbols(definition,[sQ402_spl])],[split_symbol_definition])).
% 3.53/1.33 fof(f22917,plain,(
% 3.53/1.33 state_geopolitical(c_wanica_districtsuriname)|~sQ402_spl),
% 3.53/1.33 inference(component_clause,[status(thm)],[f22916])).
% 3.53/1.33 fof(f23300,plain,(
% 3.53/1.33 ~sQ6_spl|sQ402_spl),
% 3.53/1.33 inference(split_clause,[status(thm)],[f11494,f21417,f22916])).
% 3.53/1.33 fof(f24604,plain,(
% 3.53/1.33 ![X0]: (~genlmt(c_tptp_member3515_mt,X0)|mtvisible(X0))),
% 3.53/1.33 inference(resolution,[status(thm)],[f21370,f21393])).
% 3.53/1.33 fof(f24605,plain,(
% 3.53/1.33 mtvisible(c_tptp_spindleheadmt)),
% 3.53/1.33 inference(resolution,[status(thm)],[f24604,f13224])).
% 3.53/1.33 fof(f24607,plain,(
% 3.53/1.33 ![X0]: (~genlmt(c_tptp_spindleheadmt,X0)|mtvisible(X0))),
% 3.53/1.33 inference(resolution,[status(thm)],[f24605,f21370])).
% 3.53/1.33 fof(f28230,plain,(
% 3.53/1.33 mtvisible(c_cyclistsmt)),
% 3.53/1.33 inference(resolution,[status(thm)],[f14003,f24607])).
% 3.53/1.33 fof(f28235,plain,(
% 3.53/1.33 ![X0]: (~genlmt(c_cyclistsmt,X0)|mtvisible(X0))),
% 3.53/1.33 inference(resolution,[status(thm)],[f28230,f21370])).
% 3.53/1.33 fof(f28237,plain,(
% 3.53/1.33 mtvisible(c_austinareamt)),
% 3.53/1.33 inference(resolution,[status(thm)],[f28235,f12766])).
% 3.53/1.33 fof(f28253,plain,(
% 3.53/1.33 ![X0]: (~genlmt(c_austinareamt,X0)|mtvisible(X0))),
% 3.53/1.33 inference(resolution,[status(thm)],[f28237,f21370])).
% 3.53/1.33 fof(f28267,plain,(
% 3.53/1.33 mtvisible(c_unitedstatesgeographydualistmt)),
% 3.53/1.33 inference(resolution,[status(thm)],[f28253,f13147])).
% 3.53/1.33 fof(f28287,plain,(
% 3.53/1.33 ![X0]: (~genlmt(c_unitedstatesgeographydualistmt,X0)|mtvisible(X0))),
% 3.53/1.33 inference(resolution,[status(thm)],[f28267,f21370])).
% 3.53/1.33 fof(f28347,plain,(
% 3.53/1.33 mtvisible(c_worldgeographydualistmt)),
% 3.53/1.33 inference(resolution,[status(thm)],[f28287,f9486])).
% 3.53/1.33 fof(f28369,plain,(
% 3.53/1.33 ![X0]: (~genlmt(c_worldgeographydualistmt,X0)|mtvisible(X0))),
% 3.53/1.33 inference(resolution,[status(thm)],[f28347,f21370])).
% 3.53/1.33 fof(f28479,plain,(
% 3.53/1.33 mtvisible(c_worldgeographymt)),
% 3.53/1.33 inference(resolution,[status(thm)],[f28369,f11960])).
% 3.53/1.33 fof(f28482,plain,(
% 3.53/1.33 $false|sQ6_spl),
% 3.53/1.33 inference(forward_subsumption_resolution,[status(thm)],[f28479,f21419])).
% 3.53/1.33 fof(f28483,plain,(
% 3.53/1.33 sQ6_spl),
% 3.53/1.33 inference(contradiction_clause,[status(thm)],[f28482])).
% 3.53/1.33 fof(f28484,plain,(
% 3.53/1.33 firstorderadministrativedivision(c_wanica_districtsuriname)|~sQ402_spl),
% 3.53/1.33 inference(resolution,[status(thm)],[f22917,f13434])).
% 3.53/1.33 fof(f28846,plain,(
% 3.53/1.33 isa(c_wanica_districtsuriname,c_firstorderadministrativedivision)|~sQ402_spl),
% 3.53/1.33 inference(resolution,[status(thm)],[f17817,f28484])).
% 3.53/1.33 fof(f28847,plain,(
% 3.53/1.33 $false|~sQ402_spl),
% 3.53/1.33 inference(forward_subsumption_resolution,[status(thm)],[f28846,f21394])).
% 3.53/1.33 fof(f28848,plain,(
% 3.53/1.33 ~sQ402_spl),
% 3.53/1.33 inference(contradiction_clause,[status(thm)],[f28847])).
% 3.53/1.33 fof(f28849,plain,(
% 3.53/1.33 $false),
% 3.53/1.33 inference(sat_refutation,[status(thm)],[f23300,f28483,f28848])).
% 3.53/1.33 % SZS output end CNFRefutation for theBenchmark.p
% 3.22/2.49 % Elapsed time: 1.907419 seconds
% 3.22/2.49 % CPU time: 5.176463 seconds
% 3.22/2.49 % Total memory used: 458.012 MB
% 3.22/2.49 % Net memory used: 456.006 MB
%------------------------------------------------------------------------------