%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR033+3 : 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 : n012.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 0.03s 15.37s
% Output : CNFRefutation 0.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 13
% Syntax : Number of formulae : 52 ( 26 unt; 0 def)
% Number of atoms : 84 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 53 ( 21 ~; 18 |; 4 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 21 ( 0 sgn 7 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax2_438,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7) ),
file('theBenchmark.p',ax2_438) ).
fof(ax2_1935,axiom,
! [ARG1,ARG2] :
( geographicalsubregions(ARG1,ARG2)
=> inregion(ARG2,ARG1) ),
file('theBenchmark.p',ax2_1935) ).
fof(ax2_2024,axiom,
( mtvisible(c_worldgeographymt)
=> geolevel_1(c_georegion_l1_x2_y0) ),
file('theBenchmark.p',ax2_2024) ).
fof(ax2_2573,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23) ),
file('theBenchmark.p',ax2_2573) ).
fof(ax2_2962,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23) ),
file('theBenchmark.p',ax2_2962) ).
fof(ax2_7302,axiom,
! [X,Y,Z] :
( ( inregion(Y,Z)
& inregion(X,Y) )
=> inregion(X,Z) ),
file('theBenchmark.p',ax2_7302) ).
fof(ax2_7997,axiom,
! [SPECMT,GENLMT] :
( ( genlmt(SPECMT,GENLMT)
& mtvisible(SPECMT) )
=> mtvisible(GENLMT) ),
file('theBenchmark.p',ax2_7997) ).
fof(ax2_2684,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2) ),
file('theBenchmark.p',ax2_2684) ).
fof(query133,conjecture,
( mtvisible(c_tptpgeo_spindlecollectormt)
=> ( geolevel_1(c_georegion_l1_x2_y0)
& inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0) ) ),
file('theBenchmark.p',query133) ).
fof(query133_neg,negated_conjecture,
~ ( mtvisible(c_tptpgeo_spindlecollectormt)
=> ( geolevel_1(c_georegion_l1_x2_y0)
& inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0) ) ),
inference(assume_negation,[status(cth)],[query133]) ).
fof(ax2_2324,axiom,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
file('theBenchmark.p',ax2_2324) ).
cnf(c_58,plain,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
inference(clausify,[status(thm)],[ax2_2324]) ).
cnf(c_60,plain,
( geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(clausify,[status(thm)],[ax2_2684]) ).
fof(ax2_197,axiom,
genlmt(c_tptpgeo_member3_mt,c_tptpgeo_spindleheadmt),
file('theBenchmark.p',ax2_197) ).
cnf(c_80,plain,
genlmt(c_tptpgeo_member3_mt,c_tptpgeo_spindleheadmt),
inference(clausify,[status(thm)],[ax2_197]) ).
fof(ax2_232,axiom,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member2_mt),
file('theBenchmark.p',ax2_232) ).
cnf(c_81,plain,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member2_mt),
inference(clausify,[status(thm)],[ax2_232]) ).
cnf(c_82,plain,
( geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(clausify,[status(thm)],[ax2_438]) ).
cnf(c_86,plain,
( inregion(B,A)
| ~ geographicalsubregions(A,B) ),
inference(clausify,[status(thm)],[ax2_1935]) ).
cnf(c_87,plain,
( geolevel_1(c_georegion_l1_x2_y0)
| ~ mtvisible(c_worldgeographymt) ),
inference(clausify,[status(thm)],[ax2_2024]) ).
cnf(c_89,plain,
( geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(clausify,[status(thm)],[ax2_2573]) ).
cnf(c_94,plain,
( inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(clausify,[status(thm)],[ax2_2962]) ).
fof(ax2_3432,axiom,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member3_mt),
file('theBenchmark.p',ax2_3432) ).
cnf(c_95,plain,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member3_mt),
inference(clausify,[status(thm)],[ax2_3432]) ).
cnf(c_102,plain,
( inregion(A,C)
| ~ inregion(B,C)
| ~ inregion(A,B) ),
inference(clausify,[status(thm)],[ax2_7302]) ).
cnf(c_109,plain,
( mtvisible(B)
| ~ genlmt(A,B)
| ~ mtvisible(A) ),
inference(clausify,[status(thm)],[ax2_7997]) ).
cnf(c_111,negated_conjecture,
mtvisible(c_tptpgeo_spindlecollectormt),
inference(clausify,[status(thm)],[query133_neg]) ).
cnf(c_112,negated_conjecture,
( ~ geolevel_1(c_georegion_l1_x2_y0)
| ~ inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0) ),
inference(clausify,[status(thm)],[query133_neg]) ).
cnf(c_150,negated_conjecture,
( mtvisible(A)
| ~ genlmt(c_tptpgeo_spindlecollectormt,A) ),
inference(resolve,[status(thm)],[c_109,c_111]) ).
cnf(c_113,negated_conjecture,
mtvisible(c_tptpgeo_member3_mt),
inference(resolve,[status(thm)],[c_150,c_95]) ).
cnf(c_151,negated_conjecture,
( mtvisible(A)
| ~ genlmt(c_tptpgeo_spindlecollectormt,A) ),
inference(resolve,[status(thm)],[c_109,c_111]) ).
cnf(c_116,negated_conjecture,
mtvisible(c_tptpgeo_member2_mt),
inference(resolve,[status(thm)],[c_151,c_81]) ).
cnf(c_118,plain,
inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23),
inference(resolve,[status(thm)],[c_116,c_94]) ).
cnf(c_119,plain,
geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23),
inference(resolve,[status(thm)],[c_116,c_89]) ).
cnf(c_120,plain,
geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7),
inference(resolve,[status(thm)],[c_116,c_82]) ).
cnf(c_121,plain,
geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2),
inference(resolve,[status(thm)],[c_116,c_60]) ).
cnf(c_152,plain,
( mtvisible(A)
| ~ genlmt(c_tptpgeo_member3_mt,A) ),
inference(resolve,[status(thm)],[c_109,c_113]) ).
cnf(c_122,plain,
mtvisible(c_tptpgeo_spindleheadmt),
inference(resolve,[status(thm)],[c_152,c_80]) ).
cnf(c_153,plain,
( mtvisible(A)
| ~ genlmt(c_tptpgeo_spindleheadmt,A) ),
inference(resolve,[status(thm)],[c_109,c_122]) ).
cnf(c_123,plain,
mtvisible(c_worldgeographymt),
inference(resolve,[status(thm)],[c_153,c_58]) ).
cnf(c_124,plain,
geolevel_1(c_georegion_l1_x2_y0),
inference(resolve,[status(thm)],[c_123,c_87]) ).
cnf(c_125,negated_conjecture,
~ inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0),
inference(resolve,[status(thm)],[c_124,c_112]) ).
cnf(c_132,plain,
inregion(c_georegion_l4_x76_y23,c_georegion_l3_x25_y7),
inference(resolve,[status(thm)],[c_86,c_119]) ).
cnf(c_133,plain,
inregion(c_georegion_l3_x25_y7,c_georegion_l2_x8_y2),
inference(resolve,[status(thm)],[c_86,c_120]) ).
cnf(c_134,plain,
inregion(c_georegion_l2_x8_y2,c_georegion_l1_x2_y0),
inference(resolve,[status(thm)],[c_86,c_121]) ).
cnf(c_154,plain,
( inregion(c_georegion_l3_x25_y7,A)
| ~ inregion(c_georegion_l2_x8_y2,A) ),
inference(resolve,[status(thm)],[c_102,c_133]) ).
cnf(c_144,plain,
inregion(c_georegion_l3_x25_y7,c_georegion_l1_x2_y0),
inference(resolve,[status(thm)],[c_154,c_134]) ).
cnf(c_155,plain,
( inregion(c_geolocation_x76_y23,A)
| ~ inregion(c_georegion_l4_x76_y23,A) ),
inference(resolve,[status(thm)],[c_102,c_118]) ).
cnf(c_146,plain,
inregion(c_geolocation_x76_y23,c_georegion_l3_x25_y7),
inference(resolve,[status(thm)],[c_155,c_132]) ).
cnf(c_156,plain,
( inregion(c_geolocation_x76_y23,A)
| ~ inregion(c_georegion_l3_x25_y7,A) ),
inference(resolve,[status(thm)],[c_102,c_146]) ).
cnf(c_157,plain,
inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0),
inference(resolve,[status(thm)],[c_156,c_144]) ).
cnf(c_149,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_125,c_157]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR033+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/15.32 % Computer : n012.cluster.edu
% 0.03/15.32 % Model : x86_64 x86_64
% 0.03/15.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/15.32 % Memory : 8046.5625MB
% 0.03/15.32 % OS : Linux 6.8.0-71-generic
% 0.03/15.32 % CPULimit : 300
% 0.03/15.32 % WCLimit : 300
% 0.03/15.32 % DateTime : Sun Sep 27 00:03:36 UTC 2026
% 0.03/15.32 % CPUTime :
% 0.03/15.32 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/15.32 % Process 1792969 was started by sandbox on n012,
% 0.03/15.32 % Sun Sep 27 00:03:36 2026
% 0.03/15.32 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.03/15.37
% 0.03/15.37 % SInE (scan): 63 to sos (tol 1.5x), 11 to usable (tol 2.0x), 7931 zapped, of 8005 axioms (depth 3).
% 0.03/15.37
% 0.03/15.37 % From the command line: assign(max_seconds, 300).
% 0.03/15.37
% 0.03/15.37 % SZS status Theorem for theBenchmark
% 0.03/15.37
% 0.03/15.37 % Proof 1 at 0.01 (+ 0.01) seconds.
% 0.03/15.37 % Length of proof is 39.
% 0.03/15.37 % Level of proof is 7.
% 0.03/15.37 % Maximum clause weight is 105.000.
% 0.03/15.37 % Given clauses 58.
% 0.03/15.37
% 0.03/15.37 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------