%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR034+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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 : Sun Sep 27 07:06:40 AM UTC 2026
% Result : Theorem 3.01s 0.93s
% Output : CNFRefutation 3.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 18
% Syntax : Number of formulae : 69 ( 47 unt; 0 def)
% Number of atoms : 93 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 45 ( 21 ~; 18 |; 1 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 17 con; 0-1 aty)
% Number of variables : 23 ( 1 sgn 3 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1_321,axiom,
( mtvisible(c_worldgeographymt)
=> state_geopolitical(c_wanica_districtsuriname) ),
file('theBenchmark.p',ax1_321) ).
fof(ax1_629,axiom,
! [X] :
( state_geopolitical(X)
=> isa(X,c_state_geopolitical) ),
file('theBenchmark.p',ax1_629) ).
fof(ax1_1123,axiom,
! [SPECMT,GENLMT] :
( ( genlmt(SPECMT,GENLMT)
& mtvisible(SPECMT) )
=> mtvisible(GENLMT) ),
file('theBenchmark.p',ax1_1123) ).
fof(query84,conjecture,
? [COL] :
( mtvisible(c_tptp_member3515_mt)
=> isa(c_wanica_districtsuriname,COL) ),
file('theBenchmark.p',query84) ).
fof(query84_neg,negated_conjecture,
~ ? [COL] :
( mtvisible(c_tptp_member3515_mt)
=> isa(c_wanica_districtsuriname,COL) ),
inference(assume_negation,[status(cth)],[query84]) ).
fof(ax1_53,axiom,
genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt),
file('theBenchmark.p',ax1_53) ).
cnf(c_869,plain,
genlmt(c_ethnicgroupsmt,c_ethnicgroupsvocabularymt),
inference(clausify,[status(thm)],[ax1_53]) ).
fof(ax1_66,axiom,
genlmt(c_nooescapearchitecturemt,c_organizationdatamt),
file('theBenchmark.p',ax1_66) ).
cnf(c_879,plain,
genlmt(c_nooescapearchitecturemt,c_organizationdatamt),
inference(clausify,[status(thm)],[ax1_66]) ).
fof(ax1_137,axiom,
genlmt(c_worldgeographydualistmt,c_worldgeographymt),
file('theBenchmark.p',ax1_137) ).
cnf(c_908,plain,
genlmt(c_worldgeographydualistmt,c_worldgeographymt),
inference(clausify,[status(thm)],[ax1_137]) ).
fof(ax1_232,axiom,
genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt),
file('theBenchmark.p',ax1_232) ).
cnf(c_938,plain,
genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),c_massmediadatamt),
inference(clausify,[status(thm)],[ax1_232]) ).
fof(ax1_257,axiom,
genlmt(c_keinteractionresourcetestmt,c_testvocabularymt),
file('theBenchmark.p',ax1_257) ).
cnf(c_949,plain,
genlmt(c_keinteractionresourcetestmt,c_testvocabularymt),
inference(clausify,[status(thm)],[ax1_257]) ).
fof(ax1_275,axiom,
genlmt(c_testvocabularymt,c_nooescapearchitecturemt),
file('theBenchmark.p',ax1_275) ).
cnf(c_956,plain,
genlmt(c_testvocabularymt,c_nooescapearchitecturemt),
inference(clausify,[status(thm)],[ax1_275]) ).
fof(ax1_310,axiom,
genlmt(c_cyclistsmt,c_keinteractionresourcetestmt),
file('theBenchmark.p',ax1_310) ).
cnf(c_969,plain,
genlmt(c_cyclistsmt,c_keinteractionresourcetestmt),
inference(clausify,[status(thm)],[ax1_310]) ).
fof(ax1_329,axiom,
genlmt(c_massmediadatamt,c_ethnicgroupsmt),
file('theBenchmark.p',ax1_329) ).
cnf(c_976,plain,
genlmt(c_massmediadatamt,c_ethnicgroupsmt),
inference(clausify,[status(thm)],[ax1_329]) ).
fof(ax1_339,axiom,
genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt),
file('theBenchmark.p',ax1_339) ).
cnf(c_982,plain,
genlmt(c_worldcompletedualistgeographymt,c_unitedstatesgeographydualistmt),
inference(clausify,[status(thm)],[ax1_339]) ).
fof(ax1_367,axiom,
genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt),
file('theBenchmark.p',ax1_367) ).
cnf(c_989,plain,
genlmt(c_ethnicgroupsvocabularymt,c_worldcompletedualistgeographymt),
inference(clausify,[status(thm)],[ax1_367]) ).
fof(ax1_454,axiom,
genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt),
file('theBenchmark.p',ax1_454) ).
cnf(c_1019,plain,
genlmt(c_unitedstatesgeographydualistmt,c_worldgeographydualistmt),
inference(clausify,[status(thm)],[ax1_454]) ).
fof(ax1_486,axiom,
genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)),
file('theBenchmark.p',ax1_486) ).
cnf(c_1032,plain,
genlmt(c_organizationdatamt,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)),
inference(clausify,[status(thm)],[ax1_486]) ).
fof(ax1_147,axiom,
genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt),
file('theBenchmark.p',ax1_147) ).
cnf(c_1321,plain,
genlmt(c_tptp_member3515_mt,c_tptp_spindleheadmt),
inference(clausify,[status(thm)],[ax1_147]) ).
fof(ax1_254,axiom,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt),
file('theBenchmark.p',ax1_254) ).
cnf(c_1391,plain,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt),
inference(clausify,[status(thm)],[ax1_254]) ).
cnf(c_1435,plain,
( state_geopolitical(c_wanica_districtsuriname)
| ~ mtvisible(c_worldgeographymt) ),
inference(clausify,[status(thm)],[ax1_321]) ).
cnf(c_1636,plain,
( isa(A,c_state_geopolitical)
| ~ state_geopolitical(A) ),
inference(clausify,[status(thm)],[ax1_629]) ).
cnf(c_1957,plain,
( mtvisible(B)
| ~ genlmt(A,B)
| ~ mtvisible(A) ),
inference(clausify,[status(thm)],[ax1_1123]) ).
cnf(c_1962,negated_conjecture,
mtvisible(c_tptp_member3515_mt),
inference(clausify,[status(thm)],[query84_neg]) ).
cnf(c_1963,negated_conjecture,
~ isa(c_wanica_districtsuriname,A),
inference(clausify,[status(thm)],[query84_neg]) ).
cnf(c_2109,negated_conjecture,
( mtvisible(A)
| ~ genlmt(c_tptp_member3515_mt,A) ),
inference(resolve,[status(thm)],[c_1957,c_1962]) ).
cnf(c_2016,negated_conjecture,
mtvisible(c_tptp_spindleheadmt),
inference(resolve,[status(thm)],[c_2109,c_1321]) ).
cnf(c_2110,plain,
( mtvisible(A)
| ~ genlmt(c_tptp_spindleheadmt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2016]) ).
cnf(c_2030,plain,
mtvisible(c_cyclistsmt),
inference(resolve,[status(thm)],[c_2110,c_1391]) ).
cnf(c_2111,plain,
( mtvisible(A)
| ~ genlmt(c_cyclistsmt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2030]) ).
cnf(c_2041,plain,
mtvisible(c_keinteractionresourcetestmt),
inference(resolve,[status(thm)],[c_2111,c_969]) ).
cnf(c_2112,plain,
( mtvisible(A)
| ~ genlmt(c_keinteractionresourcetestmt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2041]) ).
cnf(c_2050,plain,
mtvisible(c_testvocabularymt),
inference(resolve,[status(thm)],[c_2112,c_949]) ).
cnf(c_2113,plain,
( mtvisible(A)
| ~ genlmt(c_testvocabularymt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2050]) ).
cnf(c_2055,plain,
mtvisible(c_nooescapearchitecturemt),
inference(resolve,[status(thm)],[c_2113,c_956]) ).
cnf(c_2114,plain,
( mtvisible(A)
| ~ genlmt(c_nooescapearchitecturemt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2055]) ).
cnf(c_2056,plain,
mtvisible(c_organizationdatamt),
inference(resolve,[status(thm)],[c_2114,c_879]) ).
cnf(c_2115,plain,
( mtvisible(A)
| ~ genlmt(c_organizationdatamt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2056]) ).
cnf(c_2057,plain,
mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)),
inference(resolve,[status(thm)],[c_2115,c_1032]) ).
cnf(c_2116,plain,
( mtvisible(A)
| ~ genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),A) ),
inference(resolve,[status(thm)],[c_1957,c_2057]) ).
cnf(c_2063,plain,
mtvisible(c_massmediadatamt),
inference(resolve,[status(thm)],[c_2116,c_938]) ).
cnf(c_2117,plain,
( mtvisible(A)
| ~ genlmt(c_massmediadatamt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2063]) ).
cnf(c_2064,plain,
mtvisible(c_ethnicgroupsmt),
inference(resolve,[status(thm)],[c_2117,c_976]) ).
cnf(c_2118,plain,
( mtvisible(A)
| ~ genlmt(c_ethnicgroupsmt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2064]) ).
cnf(c_2065,plain,
mtvisible(c_ethnicgroupsvocabularymt),
inference(resolve,[status(thm)],[c_2118,c_869]) ).
cnf(c_2119,plain,
( mtvisible(A)
| ~ genlmt(c_ethnicgroupsvocabularymt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2065]) ).
cnf(c_2067,plain,
mtvisible(c_worldcompletedualistgeographymt),
inference(resolve,[status(thm)],[c_2119,c_989]) ).
cnf(c_2120,plain,
( mtvisible(A)
| ~ genlmt(c_worldcompletedualistgeographymt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2067]) ).
cnf(c_2068,plain,
mtvisible(c_unitedstatesgeographydualistmt),
inference(resolve,[status(thm)],[c_2120,c_982]) ).
cnf(c_2121,plain,
( mtvisible(A)
| ~ genlmt(c_unitedstatesgeographydualistmt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2068]) ).
cnf(c_2069,plain,
mtvisible(c_worldgeographydualistmt),
inference(resolve,[status(thm)],[c_2121,c_1019]) ).
cnf(c_2122,plain,
( mtvisible(A)
| ~ genlmt(c_worldgeographydualistmt,A) ),
inference(resolve,[status(thm)],[c_1957,c_2069]) ).
cnf(c_2070,plain,
mtvisible(c_worldgeographymt),
inference(resolve,[status(thm)],[c_2122,c_908]) ).
cnf(c_2072,plain,
state_geopolitical(c_wanica_districtsuriname),
inference(resolve,[status(thm)],[c_2070,c_1435]) ).
cnf(c_2123,negated_conjecture,
~ state_geopolitical(c_wanica_districtsuriname),
inference(resolve,[status(thm)],[c_1636,c_1963]) ).
cnf(c_2108,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_2072,c_2123]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR034+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n013.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 27 00:03:36 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 3854384 was started by sandbox on n013,
% 0.08/0.36 % Sun Sep 27 00:03:36 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.44
% 0.12/0.44 % From the command line: assign(max_seconds, 300).
% 0.12/0.44
% 0.12/0.44 % SInE: 758 to sos, 373 to usable, of 1131 axioms (tolerance 2.00, depth 0 fixpoint).
% 3.01/0.93
% 3.01/0.93 % SZS status Theorem for theBenchmark
% 3.01/0.93
% 3.01/0.93 % Proof 1 at 0.34 (+ 0.04) seconds.
% 3.01/0.93 % Length of proof is 39.
% 3.01/0.93 % Level of proof is 17.
% 3.01/0.93 % Maximum clause weight is 107.000.
% 3.01/0.93 % Given clauses 174.
% 3.01/0.93
% 3.01/0.93 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------