%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR033+6 : TPTP v9.3.1. Bugfixed v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 285.26s 187.83s
% Output : CNFRefutation 285.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 14
% Syntax : Number of formulae : 53 ( 25 unt; 0 def)
% Number of atoms : 89 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 59 ( 23 ~; 20 |; 5 &)
% ( 0 <=>; 11 =>; 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 : 27 ( 0 sgn 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax5_104617,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23) ),
file('theBenchmark.p',ax5_104617) ).
fof(ax5_135525,axiom,
( mtvisible(c_worldgeographymt)
=> geolevel_1(c_georegion_l1_x2_y0) ),
file('theBenchmark.p',ax5_135525) ).
fof(ax5_197843,axiom,
! [ARG1,ARG2] :
( geographicalsubregions(ARG1,ARG2)
=> inregion(ARG2,ARG1) ),
file('theBenchmark.p',ax5_197843) ).
fof(ax5_1324892,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2) ),
file('theBenchmark.p',ax5_1324892) ).
fof(ax5_1634515,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23) ),
file('theBenchmark.p',ax5_1634515) ).
fof(ax5_2098635,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7) ),
file('theBenchmark.p',ax5_2098635) ).
fof(ax5_3337975,axiom,
! [X,Y,Z] :
( ( geographicalsubregions(Y,Z)
& geographicalsubregions(X,Y) )
=> geographicalsubregions(X,Z) ),
file('theBenchmark.p',ax5_3337975) ).
fof(ax5_3340896,axiom,
! [X,Y,Z] :
( ( inregion(Y,Z)
& inregion(X,Y) )
=> inregion(X,Z) ),
file('theBenchmark.p',ax5_3340896) ).
fof(ax5_3342125,axiom,
! [SPECMT,GENLMT] :
( ( genlmt(SPECMT,GENLMT)
& mtvisible(SPECMT) )
=> mtvisible(GENLMT) ),
file('theBenchmark.p',ax5_3342125) ).
fof(query283,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',query283) ).
fof(query283_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)],[query283]) ).
cnf(c_3854,plain,
( inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(clausify,[status(thm)],[ax5_104617]) ).
cnf(c_3858,plain,
( geolevel_1(c_georegion_l1_x2_y0)
| ~ mtvisible(c_worldgeographymt) ),
inference(clausify,[status(thm)],[ax5_135525]) ).
fof(ax5_171714,axiom,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
file('theBenchmark.p',ax5_171714) ).
cnf(c_3864,plain,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
inference(clausify,[status(thm)],[ax5_171714]) ).
cnf(c_3868,plain,
( inregion(B,A)
| ~ geographicalsubregions(A,B) ),
inference(clausify,[status(thm)],[ax5_197843]) ).
fof(ax5_309091,axiom,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member2_mt),
file('theBenchmark.p',ax5_309091) ).
cnf(c_3884,plain,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member2_mt),
inference(clausify,[status(thm)],[ax5_309091]) ).
fof(ax5_1239739,axiom,
genlmt(c_tptpgeo_member3_mt,c_tptpgeo_spindleheadmt),
file('theBenchmark.p',ax5_1239739) ).
cnf(c_3978,plain,
genlmt(c_tptpgeo_member3_mt,c_tptpgeo_spindleheadmt),
inference(clausify,[status(thm)],[ax5_1239739]) ).
cnf(c_3988,plain,
( geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(clausify,[status(thm)],[ax5_1324892]) ).
cnf(c_4030,plain,
( geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(clausify,[status(thm)],[ax5_1634515]) ).
cnf(c_4071,plain,
( geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(clausify,[status(thm)],[ax5_2098635]) ).
fof(ax5_2198877,axiom,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member3_mt),
file('theBenchmark.p',ax5_2198877) ).
cnf(c_4084,plain,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member3_mt),
inference(clausify,[status(thm)],[ax5_2198877]) ).
cnf(c_4159,plain,
( geographicalsubregions(A,C)
| ~ geographicalsubregions(B,C)
| ~ geographicalsubregions(A,B) ),
inference(clausify,[status(thm)],[ax5_3337975]) ).
cnf(c_4161,plain,
( inregion(A,C)
| ~ inregion(B,C)
| ~ inregion(A,B) ),
inference(clausify,[status(thm)],[ax5_3340896]) ).
cnf(c_4163,plain,
( mtvisible(B)
| ~ genlmt(A,B)
| ~ mtvisible(A) ),
inference(clausify,[status(thm)],[ax5_3342125]) ).
cnf(c_4167,negated_conjecture,
mtvisible(c_tptpgeo_spindlecollectormt),
inference(clausify,[status(thm)],[query283_neg]) ).
cnf(c_4168,negated_conjecture,
( ~ geolevel_1(c_georegion_l1_x2_y0)
| ~ inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0) ),
inference(clausify,[status(thm)],[query283_neg]) ).
cnf(c_18896,negated_conjecture,
( mtvisible(A)
| ~ genlmt(c_tptpgeo_spindlecollectormt,A) ),
inference(resolve,[status(thm)],[c_4163,c_4167]) ).
cnf(c_4215,negated_conjecture,
mtvisible(c_tptpgeo_member3_mt),
inference(resolve,[status(thm)],[c_18896,c_4084]) ).
cnf(c_18897,negated_conjecture,
( mtvisible(A)
| ~ genlmt(c_tptpgeo_spindlecollectormt,A) ),
inference(resolve,[status(thm)],[c_4163,c_4167]) ).
cnf(c_4220,negated_conjecture,
mtvisible(c_tptpgeo_member2_mt),
inference(resolve,[status(thm)],[c_18897,c_3884]) ).
cnf(c_4762,plain,
geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7),
inference(resolve,[status(thm)],[c_4220,c_4071]) ).
cnf(c_4776,plain,
geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23),
inference(resolve,[status(thm)],[c_4220,c_4030]) ).
cnf(c_4793,plain,
geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2),
inference(resolve,[status(thm)],[c_4220,c_3988]) ).
cnf(c_4837,plain,
inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23),
inference(resolve,[status(thm)],[c_4220,c_3854]) ).
cnf(c_18898,plain,
( mtvisible(A)
| ~ genlmt(c_tptpgeo_member3_mt,A) ),
inference(resolve,[status(thm)],[c_4163,c_4215]) ).
cnf(c_5944,plain,
mtvisible(c_tptpgeo_spindleheadmt),
inference(resolve,[status(thm)],[c_18898,c_3978]) ).
cnf(c_18899,plain,
( mtvisible(A)
| ~ genlmt(c_tptpgeo_spindleheadmt,A) ),
inference(resolve,[status(thm)],[c_4163,c_5944]) ).
cnf(c_5990,plain,
mtvisible(c_worldgeographymt),
inference(resolve,[status(thm)],[c_18899,c_3864]) ).
cnf(c_6009,plain,
geolevel_1(c_georegion_l1_x2_y0),
inference(resolve,[status(thm)],[c_5990,c_3858]) ).
cnf(c_6168,negated_conjecture,
~ inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0),
inference(resolve,[status(thm)],[c_6009,c_4168]) ).
cnf(c_8199,plain,
inregion(c_georegion_l4_x76_y23,c_georegion_l3_x25_y7),
inference(resolve,[status(thm)],[c_3868,c_4776]) ).
cnf(c_18900,plain,
( geographicalsubregions(c_georegion_l1_x2_y0,A)
| ~ geographicalsubregions(c_georegion_l2_x8_y2,A) ),
inference(resolve,[status(thm)],[c_4159,c_4793]) ).
cnf(c_8264,plain,
geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l3_x25_y7),
inference(resolve,[status(thm)],[c_18900,c_4762]) ).
cnf(c_18901,plain,
( inregion(c_geolocation_x76_y23,A)
| ~ inregion(c_georegion_l4_x76_y23,A) ),
inference(resolve,[status(thm)],[c_4161,c_4837]) ).
cnf(c_13691,plain,
inregion(c_geolocation_x76_y23,c_georegion_l3_x25_y7),
inference(resolve,[status(thm)],[c_18901,c_8199]) ).
cnf(c_13922,plain,
inregion(c_georegion_l3_x25_y7,c_georegion_l1_x2_y0),
inference(resolve,[status(thm)],[c_3868,c_8264]) ).
cnf(c_18902,plain,
( inregion(c_geolocation_x76_y23,A)
| ~ inregion(c_georegion_l3_x25_y7,A) ),
inference(resolve,[status(thm)],[c_4161,c_13691]) ).
cnf(c_18903,plain,
inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0),
inference(resolve,[status(thm)],[c_18902,c_13922]) ).
cnf(c_18895,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_6168,c_18903]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR033+6 : TPTP v9.3.1. Bugfixed v5.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 00:04:01 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 202845 was started by sandbox2 on n014,
% 0.09/0.37 % Sun Sep 27 00:04:01 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 285.26/187.83
% 285.26/187.83 % SInE (scan): 1580 to sos (tol 1.5x), 648 to usable (tol 2.0x), 3339749 zapped, of 3341977 axioms (depth 3).
% 285.26/187.83
% 285.26/187.83 % From the command line: assign(max_seconds, 300).
% 285.26/187.83
% 285.26/187.83 % given #500 (W,wt=2): 6111 geolevel_4(c_georegion_l4_x76_y22). [back_unit_del(2769),unit_del(a,5990)].
% 285.26/187.83
% 285.26/187.83 % given #1000 (T,wt=3): 4414 geographicalsubregions(c_georegion_l2_x4_y2,c_georegion_l3_x12_y6). [back_unit_del(2309),unit_del(a,4216)].
% 285.26/187.83
% 285.26/187.83 % given #1500 (W,wt=2): 7945 geographicalregion(c_georegion_l3_x16_y9). [hyper(3936,a,4692,a)].
% 285.26/187.83
% 285.26/187.83 % given #2000 (T,wt=2): 8884 geographicalregion(c_georegion_l4_x72_y15). [hyper(3936,a,4972,a)].
% 285.26/187.83
% 285.26/187.83 % given #2500 (T,wt=3): 5248 borderson(c_georegion_l3_x25_y0,c_georegion_l3_x26_y0). [back_unit_del(2855),unit_del(a,4220)].
% 285.26/187.83
% 285.26/187.83 % given #3000 (A,wt=3): 5530 geographicalsubregions(c_georegion_l3_x21_y6,c_georegion_l4_x65_y18). [back_unit_del(2195),unit_del(a,4220)].
% 285.26/187.83
% 285.26/187.83 % given #3500 (T,wt=3): 5810 geographicalsubregions(c_georegion_l2_x1_y0,c_georegion_l3_x3_y2). [back_unit_del(2540),unit_del(a,4222)].
% 285.26/187.83
% 285.26/187.83 % given #4000 (W,wt=3): 6507 inregion(c_georegion_l3_x0_y15,c_georegion_l2_x0_y5). [hyper(3868,a,4270,a)].
% 285.26/187.83
% 285.26/187.83 % given #4500 (T,wt=3): 7159 geographicalsubregions(c_georegion_l3_x14_y18,c_georegion_l3_x14_y18). [hyper(4160,a,7157,a)].
% 285.26/187.83
% 285.26/187.83 % given #5000 (W,wt=3): 7813 inregion(c_georegion_l3_x9_y17,c_georegion_l2_x3_y5). [hyper(3868,a,4658,a)].
% 285.26/187.83
% 285.26/187.83 % given #5500 (T,wt=3): 8466 geographicalsubregions(c_georegion_l4_x58_y14,c_georegion_l4_x58_y14). [hyper(4160,a,8464,a)].
% 285.26/187.83
% 285.26/187.83 % given #6000 (T,wt=3): 9122 geographicalsubregions(c_georegion_l2_x7_y0,c_georegion_l4_x64_y4). [hyper(4159,a,4747,a,b,5038,a)].
% 285.26/187.83
% 285.26/187.83 % given #6500 (A,wt=3): 9776 geographicalsubregions(c_georegion_l2_x8_y1,c_georegion_l4_x74_y12). [hyper(4159,a,4779,a,b,5232,a)].
% 285.26/187.83
% 285.26/187.83 % given #7000 (T,wt=3): 10430 geographicalsubregions(c_georegion_l2_x7_y2,c_georegion_l4_x71_y25). [hyper(4159,a,4737,a,b,5422,a)].
% 285.26/187.83
% 285.26/187.83 % given #7500 (W,wt=3): 11081 inregion(c_georegion_l4_x77_y6,c_georegion_l3_x25_y2). [hyper(3868,a,5620,a)].
% 285.26/187.83
% 285.26/187.83 % given #8000 (T,wt=3): 11732 geographicalsubregions(c_georegion_l1_x0_y0,c_georegion_l3_x6_y0). [hyper(4159,a,5740,a,b,5815,a)].
% 285.26/187.83
% 285.26/187.83 % given #8500 (W,wt=3): 12340 inregion(c_georegion_l2_x8_y7,c_georegion_l2_x8_y7). [hyper(3868,a,6309,a)].
% 285.26/187.83
% 285.26/187.83 % given #9000 (T,wt=3): 12840 geographicalsubregions(c_georegion_l0_x0_y0,c_georegion_l3_x15_y0). [hyper(4159,a,5966,a,b,6986,a)].
% 285.26/187.83
% 285.26/187.83 % given #9500 (T,wt=3): 13340 inregion(c_georegion_l3_x25_y26,c_georegion_l1_x2_y2). [hyper(3868,a,7695,a)].
% 285.26/187.83
% 285.26/187.83 % given #10000 (A,wt=3): 13840 geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l4_x58_y17). [hyper(4159,a,8249,a,b,5218,a)].
% 285.26/187.83
% 285.26/187.83 % SZS status Theorem for theBenchmark
% 285.26/187.83
% 285.26/187.83 % Proof 1 at 8.20 (+ 5.52) seconds.
% 285.26/187.83 % Length of proof is 40.
% 285.26/187.83 % Level of proof is 7.
% 285.26/187.83 % Maximum clause weight is 109.000.
% 285.26/187.83 % Given clauses 10082.
% 285.26/187.83
% 285.26/187.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------