%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR034+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -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:12:58 PM UTC 2026
% Result : Theorem 0.12s 0.38s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 34
% Syntax : Number of formulae : 97 ( 33 unt; 16 def)
% Number of atoms : 165 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 116 ( 48 ~; 44 |; 3 &)
% ( 16 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 17 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 17 con; 0-1 aty)
% Number of variables : 16 ( 14 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
genlmt(c_worldgeographydualistmt,c_worldgeographymt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
genlmt(c_nooescapearchitecturemt,c_organizationdatamt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
genlmt(c_testvocabularymt,c_nooescapearchitecturemt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
genlmt(c_cyclistsmt,c_keinteractionresourcetestmt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
genlmt(c_keinteractionresourcetestmt,c_testvocabularymt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
genlmt(c_massmediadatamt,c_ethnicgroupsmt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
( mtvisible(c_worldgeographymt)
=> state_geopolitical(c_wanica_districtsuriname) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [X] :
( state_geopolitical(X)
=> isa(X,c_state_geopolitical) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [SPECMT,GENLMT] :
( ( genlmt(SPECMT,GENLMT)
& mtvisible(SPECMT) )
=> mtvisible(GENLMT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,conjecture,
? [COL] :
( mtvisible(c_tptp_member3515_mt)
=> isa(c_wanica_districtsuriname,COL) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,negated_conjecture,
~ ? [COL] :
( mtvisible(c_tptp_member3515_mt)
=> isa(c_wanica_districtsuriname,COL) ),
inference(negated_conjecture,[status(cth)],[f71]) ).
fof(f73,plain,
genlmt(c_worldgeographydualistmt,c_worldgeographymt),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f74,plain,
genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f76,plain,
genlmt(c_nooescapearchitecturemt,c_organizationdatamt),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f77,plain,
genlmt(c_testvocabularymt,c_nooescapearchitecturemt),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f82,plain,
genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f83,plain,
genlmt(c_cyclistsmt,c_keinteractionresourcetestmt),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f84,plain,
genlmt(c_keinteractionresourcetestmt,c_testvocabularymt),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f85,plain,
genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f86,plain,
genlmt(c_massmediadatamt,c_ethnicgroupsmt),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f88,plain,
( state_geopolitical(c_wanica_districtsuriname)
| ~ mtvisible(c_worldgeographymt) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f89,plain,
( state_geopolitical(c_wanica_districtsuriname)
| ~ mtvisible(c_worldgeographymt) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f91,plain,
genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f92,plain,
genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f93,plain,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f94,plain,
genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f175,plain,
! [X] :
( isa(X,c_state_geopolitical)
| ~ state_geopolitical(X) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f176,plain,
! [X0] :
( isa(X0,c_state_geopolitical)
| ~ state_geopolitical(X0) ),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f202,plain,
! [SPECMT,GENLMT] :
( mtvisible(GENLMT)
| ~ genlmt(SPECMT,GENLMT)
| ~ mtvisible(SPECMT) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f203,plain,
! [GENLMT] :
( mtvisible(GENLMT)
| ! [SPECMT] :
( ~ genlmt(SPECMT,GENLMT)
| ~ mtvisible(SPECMT) ) ),
inference(miniscoping,[status(thm)],[f202]) ).
fof(f204,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ genlmt(X0,X1)
| ~ mtvisible(X0) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f225,plain,
! [COL] :
( ~ isa(c_wanica_districtsuriname,COL)
& mtvisible(c_tptp_member3515_mt) ),
inference(pre_NNF_transformation,[status(thm)],[f72]) ).
fof(f226,plain,
( ! [COL] : ~ isa(c_wanica_districtsuriname,COL)
& mtvisible(c_tptp_member3515_mt) ),
inference(miniscoping,[status(thm)],[f225]) ).
fof(f227,plain,
mtvisible(c_tptp_member3515_mt),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f228,plain,
! [X0] : ~ isa(c_wanica_districtsuriname,X0),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f240,definition,
( sQ3_spl
<=> mtvisible(c_worldgeographymt) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f243,definition,
( sQ4_spl
<=> state_geopolitical(c_wanica_districtsuriname) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f244,plain,
( ~ sQ4_spl
| state_geopolitical(c_wanica_districtsuriname) ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f246,plain,
( sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f89,f240,f243]) ).
fof(f329,plain,
( mtvisible(c_massmediadatamt)
| ~ mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) ),
inference(resolution,[status(thm)],[f204,f92]) ).
fof(f331,plain,
( mtvisible(c_tptp_spindleheadmt)
| ~ mtvisible(c_tptp_member3515_mt) ),
inference(resolution,[status(thm)],[f204,f94]) ).
fof(f332,plain,
( mtvisible(c_cyclistsmt)
| ~ mtvisible(c_tptp_spindleheadmt) ),
inference(resolution,[status(thm)],[f204,f93]) ).
fof(f334,plain,
( mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))
| ~ mtvisible(c_organizationdatamt) ),
inference(resolution,[status(thm)],[f204,f91]) ).
fof(f336,plain,
( mtvisible(c_ethnicgroupsvocabularymt)
| ~ mtvisible(c_ethnicgroupsmt) ),
inference(resolution,[status(thm)],[f204,f90]) ).
fof(f337,plain,
( mtvisible(c_ethnicgroupsmt)
| ~ mtvisible(c_massmediadatamt) ),
inference(resolution,[status(thm)],[f204,f86]) ).
fof(f339,plain,
( mtvisible(c_unitedstatesgeographydualistmt)
| ~ mtvisible(c_worldcompletedualistgeographymt) ),
inference(resolution,[status(thm)],[f204,f85]) ).
fof(f341,plain,
( mtvisible(c_testvocabularymt)
| ~ mtvisible(c_keinteractionresourcetestmt) ),
inference(resolution,[status(thm)],[f204,f84]) ).
fof(f343,plain,
( mtvisible(c_worldgeographydualistmt)
| ~ mtvisible(c_unitedstatesgeographydualistmt) ),
inference(resolution,[status(thm)],[f204,f82]) ).
fof(f345,plain,
( mtvisible(c_nooescapearchitecturemt)
| ~ mtvisible(c_testvocabularymt) ),
inference(resolution,[status(thm)],[f204,f77]) ).
fof(f347,plain,
( mtvisible(c_organizationdatamt)
| ~ mtvisible(c_nooescapearchitecturemt) ),
inference(resolution,[status(thm)],[f204,f76]) ).
fof(f348,plain,
( mtvisible(c_keinteractionresourcetestmt)
| ~ mtvisible(c_cyclistsmt) ),
inference(resolution,[status(thm)],[f204,f83]) ).
fof(f351,plain,
( mtvisible(c_worldcompletedualistgeographymt)
| ~ mtvisible(c_ethnicgroupsvocabularymt) ),
inference(resolution,[status(thm)],[f204,f74]) ).
fof(f353,plain,
( mtvisible(c_worldgeographymt)
| ~ mtvisible(c_worldgeographydualistmt) ),
inference(resolution,[status(thm)],[f204,f73]) ).
fof(f356,definition,
( sQ5_spl
<=> mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f359,definition,
( sQ6_spl
<=> mtvisible(c_massmediadatamt) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f362,plain,
( sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f329,f356,f359]) ).
fof(f363,definition,
( sQ7_spl
<=> mtvisible(c_tptp_member3515_mt) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f365,plain,
( sQ7_spl
| ~ mtvisible(c_tptp_member3515_mt) ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f367,definition,
( sQ8_spl
<=> mtvisible(c_tptp_spindleheadmt) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f370,plain,
( sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f331,f363,f367]) ).
fof(f371,definition,
( sQ9_spl
<=> mtvisible(c_cyclistsmt) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f374,plain,
( sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f332,f367,f371]) ).
fof(f375,definition,
( sQ10_spl
<=> mtvisible(c_organizationdatamt) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f379,plain,
( sQ5_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f334,f375,f356]) ).
fof(f380,definition,
( sQ11_spl
<=> mtvisible(c_ethnicgroupsmt) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f384,definition,
( sQ12_spl
<=> mtvisible(c_ethnicgroupsvocabularymt) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f387,plain,
( sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f336,f380,f384]) ).
fof(f388,plain,
( sQ11_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f337,f359,f380]) ).
fof(f389,definition,
( sQ13_spl
<=> mtvisible(c_worldcompletedualistgeographymt) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f393,definition,
( sQ14_spl
<=> mtvisible(c_unitedstatesgeographydualistmt) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f396,plain,
( sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f339,f389,f393]) ).
fof(f397,definition,
( sQ15_spl
<=> mtvisible(c_keinteractionresourcetestmt) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f401,definition,
( sQ16_spl
<=> mtvisible(c_testvocabularymt) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f404,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f341,f397,f401]) ).
fof(f406,definition,
( sQ17_spl
<=> mtvisible(c_worldgeographydualistmt) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f409,plain,
( sQ17_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f343,f393,f406]) ).
fof(f411,definition,
( sQ18_spl
<=> mtvisible(c_nooescapearchitecturemt) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f414,plain,
( sQ18_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f345,f401,f411]) ).
fof(f416,plain,
( sQ10_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f347,f411,f375]) ).
fof(f417,plain,
( sQ15_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f348,f371,f397]) ).
fof(f420,plain,
( sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f351,f384,f389]) ).
fof(f422,plain,
( sQ3_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f353,f406,f240]) ).
fof(f423,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f365,f227]) ).
fof(f424,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f423]) ).
fof(f425,plain,
( ~ sQ4_spl
| isa(c_wanica_districtsuriname,c_state_geopolitical) ),
inference(resolution,[status(thm)],[f244,f176]) ).
fof(f426,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f425,f228]) ).
fof(f427,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f426]) ).
fof(f428,plain,
$false,
inference(sat_refutation,[status(thm)],[f246,f362,f370,f374,f379,f387,f388,f396,f404,f409,f414,f416,f417,f420,f422,f424,f427]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR034+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n018.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:29:29 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % 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
% See solution above
% 0.12/0.40 % Elapsed time: 0.035939 seconds
% 0.12/0.40 % CPU time: 0.101996 seconds
% 0.12/0.40 % Total memory used: 28.980 MB
% 0.12/0.40 % Net memory used: 28.943 MB
%------------------------------------------------------------------------------