%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR057+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n007.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 : Fri Sep 25 01:05:34 PM UTC 2026
% Result : Theorem 6.69s 1.46s
% Output : Proof 6.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 14
% Syntax : Number of formulae : 81 ( 33 unt; 0 def)
% Number of atoms : 149 ( 24 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 134 ( 66 ~; 48 |; 10 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-4 aty)
% Number of variables : 92 ( 2 sgn 59 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f97,axiom,
! [X,Y,Z] :
( ( genlmt(Y,Z)
& genlmt(X,Y) )
=> genlmt(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just98) ).
fof(f97_nnf,plain,
! [X,Y,Z] :
( genlmt(X,Z)
| ~ genlmt(Y,Z)
| ~ genlmt(X,Y) ),
inference(nnf_transformation,[status(thm)],[f97]) ).
fof(f97_sk,plain,
! [X,Y,Z] :
( genlmt(X,Z)
| ~ genlmt(Y,Z)
| ~ genlmt(X,Y) ),
inference(skolemisation,[status(esa)],[f97_nnf]) ).
cnf(c97,plain,
( genlmt(X0,X2)
| ~ genlmt(X1,X2)
| ~ genlmt(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
cnf(hi94,axiom,
ifeq(genlmt(X0,X1),true,ifeq(genlmt(X1,X2),true,genlmt(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c97]) ).
fof(f6,axiom,
genlmt(c_tptpgeo_member8_mt,c_tptpgeo_spindleheadmt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just7) ).
fof(f6_nnf,plain,
genlmt(c_tptpgeo_member8_mt,c_tptpgeo_spindleheadmt),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
genlmt(c_tptpgeo_member8_mt,c_tptpgeo_spindleheadmt),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(hi6,axiom,
genlmt(c_tptpgeo_member8_mt,c_tptpgeo_spindleheadmt) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
fof(f5,axiom,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just6) ).
fof(f5_nnf,plain,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(hi5,axiom,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(h10,plain,
genlmt(c_tptpgeo_member8_mt,c_worldgeographymt) = true,
inference(hyper_resolution,[status(thm)],[hi94,hi6,hi5]) ).
fof(f92,axiom,
! [SPECMT,GENLMT] :
( ( genlmt(SPECMT,GENLMT)
& mtvisible(SPECMT) )
=> mtvisible(GENLMT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just93) ).
fof(f92_nnf,plain,
! [SPECMT,GENLMT] :
( mtvisible(GENLMT)
| ~ genlmt(SPECMT,GENLMT)
| ~ mtvisible(SPECMT) ),
inference(nnf_transformation,[status(thm)],[f92]) ).
fof(f92_sk,plain,
! [SPECMT,GENLMT] :
( mtvisible(GENLMT)
| ~ genlmt(SPECMT,GENLMT)
| ~ mtvisible(SPECMT) ),
inference(skolemisation,[status(esa)],[f92_nnf]) ).
cnf(c92,plain,
( mtvisible(X1)
| ~ genlmt(X0,X1)
| ~ mtvisible(X0) ),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(hi89,axiom,
ifeq(mtvisible(X0),true,ifeq(genlmt(X0,X1),true,mtvisible(X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c92]) ).
fof(f101,conjecture,
? [X] :
( mtvisible(c_tptpgeo_member8_mt)
=> inregion(X,c_georegion_l4_x75_y75) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query57) ).
fof(f101_neg,negated_conjecture,
~ ? [X] :
( mtvisible(c_tptpgeo_member8_mt)
=> inregion(X,c_georegion_l4_x75_y75) ),
inference(negated_conjecture,[status(cth)],[f101]) ).
fof(f101_nnf,plain,
! [X] :
( ~ inregion(X,c_georegion_l4_x75_y75)
& mtvisible(c_tptpgeo_member8_mt) ),
inference(nnf_transformation,[status(thm)],[f101_neg]) ).
fof(f101_sk,plain,
! [X] :
( ~ inregion(X,c_georegion_l4_x75_y75)
& mtvisible(c_tptpgeo_member8_mt) ),
inference(skolemisation,[status(esa)],[f101_nnf]) ).
cnf(c101,plain,
mtvisible(c_tptpgeo_member8_mt),
inference(cnf_transformation,[status(esa)],[f101_sk]) ).
cnf(hi98,negated_conjecture,
mtvisible(c_tptpgeo_member8_mt) = true,
inference(equality_encoding,[status(esa)],[c101]) ).
cnf(h36,plain,
mtvisible(c_worldgeographymt) = true,
inference(hyper_resolution,[status(thm)],[hi89,hi98,h10]) ).
fof(f26,axiom,
( mtvisible(c_worldgeographymt)
=> geolevel_4(c_georegion_l4_x75_y75) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just27) ).
fof(f26_nnf,plain,
( geolevel_4(c_georegion_l4_x75_y75)
| ~ mtvisible(c_worldgeographymt) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
( geolevel_4(c_georegion_l4_x75_y75)
| ~ mtvisible(c_worldgeographymt) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( geolevel_4(c_georegion_l4_x75_y75)
| ~ mtvisible(c_worldgeographymt) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(hi24,axiom,
ifeq(mtvisible(c_worldgeographymt),true,geolevel_4(c_georegion_l4_x75_y75),true) = true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(h49,plain,
geolevel_4(c_georegion_l4_x75_y75) = true,
inference(hyper_resolution,[status(thm)],[hi24,h36]) ).
fof(f28,axiom,
! [OBJ] :
( geolevel_4(OBJ)
=> geographicalregion(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just29) ).
fof(f28_nnf,plain,
! [OBJ] :
( geographicalregion(OBJ)
| ~ geolevel_4(OBJ) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [OBJ] :
( geographicalregion(OBJ)
| ~ geolevel_4(OBJ) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( geographicalregion(X0)
| ~ geolevel_4(X0) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(hi26,axiom,
ifeq(geolevel_4(X0),true,geographicalregion(X0),true) = true,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(h51,plain,
geographicalregion(c_georegion_l4_x75_y75) = true,
inference(hyper_resolution,[status(thm)],[hi26,h49]) ).
fof(f39,axiom,
! [OBJ] :
( geographicalregion(OBJ)
=> partiallytangible(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just40) ).
fof(f39_nnf,plain,
! [OBJ] :
( partiallytangible(OBJ)
| ~ geographicalregion(OBJ) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [OBJ] :
( partiallytangible(OBJ)
| ~ geographicalregion(OBJ) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( partiallytangible(X0)
| ~ geographicalregion(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(hi37,axiom,
ifeq(geographicalregion(X0),true,partiallytangible(X0),true) = true,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(h53,plain,
partiallytangible(c_georegion_l4_x75_y75) = true,
inference(hyper_resolution,[status(thm)],[hi37,h51]) ).
fof(f35,axiom,
! [OBJ] :
( partiallytangible(OBJ)
=> enduringthing_localized(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just36) ).
fof(f35_nnf,plain,
! [OBJ] :
( enduringthing_localized(OBJ)
| ~ partiallytangible(OBJ) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [OBJ] :
( enduringthing_localized(OBJ)
| ~ partiallytangible(OBJ) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( enduringthing_localized(X0)
| ~ partiallytangible(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(hi33,axiom,
ifeq(partiallytangible(X0),true,enduringthing_localized(X0),true) = true,
inference(equality_encoding,[status(esa)],[c35]) ).
cnf(h55,plain,
enduringthing_localized(c_georegion_l4_x75_y75) = true,
inference(hyper_resolution,[status(thm)],[hi33,h53]) ).
fof(f33,axiom,
! [OBJ] :
( enduringthing_localized(OBJ)
=> spatialthing_nonsituational(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just34) ).
fof(f33_nnf,plain,
! [OBJ] :
( spatialthing_nonsituational(OBJ)
| ~ enduringthing_localized(OBJ) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [OBJ] :
( spatialthing_nonsituational(OBJ)
| ~ enduringthing_localized(OBJ) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( spatialthing_nonsituational(X0)
| ~ enduringthing_localized(X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(hi31,axiom,
ifeq(enduringthing_localized(X0),true,spatialthing_nonsituational(X0),true) = true,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(h57,plain,
spatialthing_nonsituational(c_georegion_l4_x75_y75) = true,
inference(hyper_resolution,[status(thm)],[hi31,h55]) ).
fof(f83,axiom,
! [X] :
( spatialthing_nonsituational(X)
=> inregion(X,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just84) ).
fof(f83_nnf,plain,
! [X] :
( inregion(X,X)
| ~ spatialthing_nonsituational(X) ),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [X] :
( inregion(X,X)
| ~ spatialthing_nonsituational(X) ),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c83,plain,
( inregion(X0,X0)
| ~ spatialthing_nonsituational(X0) ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(hi80,axiom,
ifeq(spatialthing_nonsituational(X0),true,inregion(X0,X0),true) = true,
inference(equality_encoding,[status(esa)],[c83]) ).
cnf(h60,plain,
inregion(c_georegion_l4_x75_y75,c_georegion_l4_x75_y75) = true,
inference(hyper_resolution,[status(thm)],[hi80,h57]) ).
cnf(c102,plain,
~ inregion(X0,c_georegion_l4_x75_y75),
inference(cnf_transformation,[status(esa)],[f101_sk]) ).
cnf(hi102,negated_conjecture,
ifeq(inregion(X0,c_georegion_l4_x75_y75),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c102]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi102,h60]) ).
cnf(t742,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f8,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just9) ).
fof(f8_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
fof(f25,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just26) ).
fof(f25_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
fof(f41,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just42) ).
fof(f41_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c8,c25,c41,c102]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t742]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR057+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n007.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 : Fri Sep 25 08:39:38 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.69/1.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.69/1.46 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------