%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR034+1 : 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 : n026.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.08s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR034+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n026.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 21 14:30:07 UTC 2026
% 0.08/0.38 % CPUTime :
% 0.08/0.39 % Drodi V4.1.1
% 0.08/0.41 % Refutation found
% 0.08/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.41 fof(f1,axiom,(
% 0.08/0.41 genlmt(c_worldgeographydualistmt,c_worldgeographymt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f2,axiom,(
% 0.08/0.41 genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f3,axiom,(
% 0.08/0.41 genlmt(c_cyclistsmt,c_hpkbvocabmt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f4,axiom,(
% 0.08/0.41 genlmt(c_nooescapearchitecturemt,c_organizationdatamt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f5,axiom,(
% 0.08/0.41 genlmt(c_testvocabularymt,c_nooescapearchitecturemt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f7,axiom,(
% 0.08/0.41 (! [OBJ] :( ( mtvisible(c_hpkbvocabmt)& state_geopolitical(OBJ) )=> hpkb_subnationalagent(OBJ) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f8,axiom,(
% 0.08/0.41 genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f9,axiom,(
% 0.08/0.41 genlmt(c_cyclistsmt,c_keinteractionresourcetestmt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f10,axiom,(
% 0.08/0.41 genlmt(c_keinteractionresourcetestmt,c_testvocabularymt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f11,axiom,(
% 0.08/0.41 genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f12,axiom,(
% 0.08/0.41 genlmt(c_massmediadatamt,c_ethnicgroupsmt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f14,axiom,(
% 0.08/0.41 ( mtvisible(c_worldgeographymt)=> state_geopolitical(c_wanica_districtsuriname) ) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f15,axiom,(
% 0.08/0.41 genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f16,axiom,(
% 0.08/0.41 genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f17,axiom,(
% 0.08/0.41 genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f18,axiom,(
% 0.08/0.41 genlmt(c_tptp_spindleheadmt,c_cyclistsmt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f19,axiom,(
% 0.08/0.41 genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f50,axiom,(
% 0.08/0.41 (! [X] :( hpkb_subnationalagent(X)=> isa(X,c_hpkb_subnationalagent) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f62,axiom,(
% 0.08/0.41 (! [SPECMT,GENLMT] :( ( mtvisible(SPECMT)& genlmt(SPECMT,GENLMT) )=> mtvisible(GENLMT) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f71,conjecture,(
% 0.08/0.41 (? [COL] :( mtvisible(c_tptp_member3515_mt)=> isa(c_wanica_districtsuriname,COL) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f72,negated_conjecture,(
% 0.08/0.41 ~((? [COL] :( mtvisible(c_tptp_member3515_mt)=> isa(c_wanica_districtsuriname,COL) ) ))),
% 0.08/0.41 inference(negated_conjecture,[status(cth)],[f71])).
% 0.08/0.41 fof(f73,plain,(
% 0.08/0.41 genlmt(c_worldgeographydualistmt,c_worldgeographymt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f1])).
% 0.08/0.41 fof(f74,plain,(
% 0.08/0.41 genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.08/0.41 fof(f75,plain,(
% 0.08/0.41 genlmt(c_cyclistsmt,c_hpkbvocabmt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.41 fof(f76,plain,(
% 0.08/0.41 genlmt(c_nooescapearchitecturemt,c_organizationdatamt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.08/0.41 fof(f77,plain,(
% 0.08/0.41 genlmt(c_testvocabularymt,c_nooescapearchitecturemt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.08/0.41 fof(f80,plain,(
% 0.08/0.41 ![OBJ]: ((~mtvisible(c_hpkbvocabmt)|~state_geopolitical(OBJ))|hpkb_subnationalagent(OBJ))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.08/0.41 fof(f81,plain,(
% 0.08/0.41 ![X0]: (~mtvisible(c_hpkbvocabmt)|~state_geopolitical(X0)|hpkb_subnationalagent(X0))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f80])).
% 0.08/0.41 fof(f82,plain,(
% 0.08/0.41 genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f8])).
% 0.08/0.41 fof(f83,plain,(
% 0.08/0.41 genlmt(c_cyclistsmt,c_keinteractionresourcetestmt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f9])).
% 0.08/0.41 fof(f84,plain,(
% 0.08/0.41 genlmt(c_keinteractionresourcetestmt,c_testvocabularymt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f10])).
% 0.08/0.41 fof(f85,plain,(
% 0.08/0.41 genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f11])).
% 0.08/0.41 fof(f86,plain,(
% 0.08/0.41 genlmt(c_massmediadatamt,c_ethnicgroupsmt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f12])).
% 0.08/0.41 fof(f88,plain,(
% 0.08/0.41 ~mtvisible(c_worldgeographymt)|state_geopolitical(c_wanica_districtsuriname)),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.08/0.41 fof(f89,plain,(
% 0.08/0.41 ~mtvisible(c_worldgeographymt)|state_geopolitical(c_wanica_districtsuriname)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f88])).
% 0.08/0.41 fof(f90,plain,(
% 0.08/0.41 genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.08/0.41 fof(f91,plain,(
% 0.08/0.41 genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f16])).
% 0.08/0.41 fof(f92,plain,(
% 0.08/0.41 genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f17])).
% 0.08/0.41 fof(f93,plain,(
% 0.08/0.41 genlmt(c_tptp_spindleheadmt,c_cyclistsmt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f18])).
% 0.08/0.41 fof(f94,plain,(
% 0.08/0.41 genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f19])).
% 0.08/0.41 fof(f171,plain,(
% 0.08/0.41 ![X]: (~hpkb_subnationalagent(X)|isa(X,c_hpkb_subnationalagent))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.08/0.41 fof(f172,plain,(
% 0.08/0.41 ![X0]: (~hpkb_subnationalagent(X0)|isa(X0,c_hpkb_subnationalagent))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f171])).
% 0.08/0.41 fof(f202,plain,(
% 0.08/0.41 ![SPECMT,GENLMT]: ((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f62])).
% 0.08/0.41 fof(f203,plain,(
% 0.08/0.41 ![GENLMT]: ((![SPECMT]: (~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT)))|mtvisible(GENLMT))),
% 0.08/0.41 inference(miniscoping,[status(thm)],[f202])).
% 0.08/0.41 fof(f204,plain,(
% 0.08/0.41 ![X0,X1]: (~mtvisible(X0)|~genlmt(X0,X1)|mtvisible(X1))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f203])).
% 0.08/0.41 fof(f225,plain,(
% 0.08/0.41 (![COL]: (mtvisible(c_tptp_member3515_mt)&~isa(c_wanica_districtsuriname,COL)))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f72])).
% 0.08/0.41 fof(f226,plain,(
% 0.08/0.41 mtvisible(c_tptp_member3515_mt)&(![COL]: ~isa(c_wanica_districtsuriname,COL))),
% 0.08/0.41 inference(miniscoping,[status(thm)],[f225])).
% 0.08/0.41 fof(f227,plain,(
% 0.08/0.41 mtvisible(c_tptp_member3515_mt)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f226])).
% 0.08/0.41 fof(f228,plain,(
% 0.08/0.41 ![X0]: (~isa(c_wanica_districtsuriname,X0))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f226])).
% 0.08/0.41 fof(f229,plain,(
% 0.08/0.41 ~mtvisible(c_tptp_member3515_mt)|mtvisible(c_tptp_spindleheadmt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f204,f94])).
% 0.08/0.41 fof(f230,plain,(
% 0.08/0.41 mtvisible(c_tptp_spindleheadmt)),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f229,f227])).
% 0.08/0.41 fof(f231,plain,(
% 0.08/0.41 ~mtvisible(c_worldgeographydualistmt)|mtvisible(c_worldgeographymt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f73,f204])).
% 0.08/0.41 fof(f232,plain,(
% 0.08/0.41 ~mtvisible(c_ethnicgroupsvocabularymt)|mtvisible(c_worldcompletedualistgeographymt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f74,f204])).
% 0.08/0.41 fof(f233,plain,(
% 0.08/0.41 ~mtvisible(c_cyclistsmt)|mtvisible(c_hpkbvocabmt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f75,f204])).
% 0.08/0.41 fof(f234,plain,(
% 0.08/0.41 ~mtvisible(c_nooescapearchitecturemt)|mtvisible(c_organizationdatamt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f76,f204])).
% 0.08/0.41 fof(f235,plain,(
% 0.08/0.41 ~mtvisible(c_testvocabularymt)|mtvisible(c_nooescapearchitecturemt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f77,f204])).
% 0.08/0.41 fof(f236,plain,(
% 0.08/0.41 ~mtvisible(c_unitedstatesgeographydualistmt)|mtvisible(c_worldgeographydualistmt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f82,f204])).
% 0.08/0.41 fof(f237,plain,(
% 0.08/0.41 ~mtvisible(c_cyclistsmt)|mtvisible(c_keinteractionresourcetestmt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f83,f204])).
% 0.08/0.41 fof(f238,plain,(
% 0.08/0.41 ~mtvisible(c_keinteractionresourcetestmt)|mtvisible(c_testvocabularymt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f84,f204])).
% 0.08/0.41 fof(f239,plain,(
% 0.08/0.41 ~mtvisible(c_worldcompletedualistgeographymt)|mtvisible(c_unitedstatesgeographydualistmt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f85,f204])).
% 0.08/0.41 fof(f240,plain,(
% 0.08/0.41 ~mtvisible(c_massmediadatamt)|mtvisible(c_ethnicgroupsmt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f86,f204])).
% 0.08/0.41 fof(f241,plain,(
% 0.08/0.41 ~mtvisible(c_ethnicgroupsmt)|mtvisible(c_ethnicgroupsvocabularymt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f90,f204])).
% 0.08/0.41 fof(f242,plain,(
% 0.08/0.41 ~mtvisible(c_organizationdatamt)|mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))),
% 0.08/0.41 inference(resolution,[status(thm)],[f91,f204])).
% 0.08/0.41 fof(f243,plain,(
% 0.08/0.41 ~mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))|mtvisible(c_massmediadatamt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f92,f204])).
% 0.08/0.41 fof(f244,plain,(
% 0.08/0.41 ~mtvisible(c_tptp_spindleheadmt)|mtvisible(c_cyclistsmt)),
% 0.08/0.41 inference(resolution,[status(thm)],[f93,f204])).
% 0.08/0.41 fof(f245,plain,(
% 0.08/0.41 mtvisible(c_cyclistsmt)),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f244,f230])).
% 0.08/0.41 fof(f246,plain,(
% 0.08/0.41 mtvisible(c_keinteractionresourcetestmt)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f237,f245])).
% 0.08/0.41 fof(f247,plain,(
% 0.08/0.41 mtvisible(c_hpkbvocabmt)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f233,f245])).
% 0.08/0.41 fof(f248,plain,(
% 0.08/0.41 ![X0]: (~state_geopolitical(X0)|hpkb_subnationalagent(X0))),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f81,f247])).
% 0.08/0.41 fof(f250,plain,(
% 0.08/0.41 mtvisible(c_nooescapearchitecturemt)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f235,f251])).
% 0.08/0.41 fof(f251,plain,(
% 0.08/0.41 mtvisible(c_testvocabularymt)),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f238,f246])).
% 0.08/0.41 fof(f252,plain,(
% 0.08/0.41 mtvisible(c_organizationdatamt)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f234,f250])).
% 0.08/0.41 fof(f253,plain,(
% 0.08/0.41 mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f242,f252])).
% 0.08/0.41 fof(f254,plain,(
% 0.08/0.41 mtvisible(c_ethnicgroupsmt)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f240,f255])).
% 0.08/0.41 fof(f255,plain,(
% 0.08/0.41 mtvisible(c_massmediadatamt)),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f243,f253])).
% 0.08/0.41 fof(f256,plain,(
% 0.08/0.41 mtvisible(c_ethnicgroupsvocabularymt)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f241,f254])).
% 0.08/0.41 fof(f257,plain,(
% 0.08/0.41 mtvisible(c_worldcompletedualistgeographymt)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f232,f256])).
% 0.08/0.41 fof(f258,plain,(
% 0.08/0.41 mtvisible(c_unitedstatesgeographydualistmt)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f239,f257])).
% 0.08/0.41 fof(f259,plain,(
% 0.08/0.41 mtvisible(c_worldgeographydualistmt)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f236,f258])).
% 0.08/0.41 fof(f260,plain,(
% 0.08/0.41 mtvisible(c_worldgeographymt)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f231,f259])).
% 0.08/0.41 fof(f261,plain,(
% 0.08/0.41 state_geopolitical(c_wanica_districtsuriname)),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f89,f260])).
% 0.08/0.41 fof(f262,plain,(
% 0.08/0.41 hpkb_subnationalagent(c_wanica_districtsuriname)),
% 0.08/0.41 inference(resolution,[status(thm)],[f261,f248])).
% 0.08/0.41 fof(f264,plain,(
% 0.08/0.41 isa(c_wanica_districtsuriname,c_hpkb_subnationalagent)),
% 0.08/0.41 inference(resolution,[status(thm)],[f172,f262])).
% 0.08/0.41 fof(f265,plain,(
% 0.08/0.41 $false),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f264,f228])).
% 0.08/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 1.34/1.66 % Elapsed time: 1.058191 seconds
% 1.34/1.66 % CPU time: 0.142045 seconds
% 1.34/1.66 % Total memory used: 55.505 MB
% 1.34/1.66 % Net memory used: 55.487 MB
%------------------------------------------------------------------------------