%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR045+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 : 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 : Fri Sep 25 01:05:27 PM UTC 2026
% Result : Theorem 6.39s 11.32s
% Output : Proof 6.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 17
% Syntax : Number of formulae : 89 ( 53 unt; 0 def)
% Number of atoms : 145 ( 27 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 115 ( 59 ~; 42 |; 8 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-4 aty)
% Number of variables : 96 ( 2 sgn 60 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f75,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& genls(ARG1,OLD) )
=> genls(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just76) ).
fof(f75_nnf,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f75]) ).
fof(f75_sk,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f75_nnf]) ).
cnf(c75,plain,
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f75_sk]) ).
cnf(hi72,axiom,
ifeq(genls(X0,X1),true,ifeq(genls(X1,X2),true,genls(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c75]) ).
fof(f6,axiom,
genls(c_aspatialinformationstore,c_intangibleindividual),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just7) ).
fof(f6_nnf,plain,
genls(c_aspatialinformationstore,c_intangibleindividual),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
genls(c_aspatialinformationstore,c_intangibleindividual),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(hi6,axiom,
genls(c_aspatialinformationstore,c_intangibleindividual) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
fof(f4,axiom,
genls(c_intangibleindividual,c_partiallyintangibleindividual),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just5) ).
fof(f4_nnf,plain,
genls(c_intangibleindividual,c_partiallyintangibleindividual),
inference(nnf_transformation,[status(thm)],[f4]) ).
cnf(c4,plain,
genls(c_intangibleindividual,c_partiallyintangibleindividual),
inference(cnf_transformation,[status(esa)],[f4_nnf]) ).
cnf(hi4,axiom,
genls(c_intangibleindividual,c_partiallyintangibleindividual) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h10,plain,
genls(c_aspatialinformationstore,c_partiallyintangibleindividual) = true,
inference(hyper_resolution,[status(thm)],[hi72,hi6,hi4]) ).
fof(f43,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just44) ).
fof(f43_nnf,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(hi40,axiom,
ifeq(disjointwith(X0,X1),true,ifeq(genls(X2,X1),true,disjointwith(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c43]) ).
fof(f15,axiom,
disjointwith(c_collection,c_individual),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just16) ).
fof(f15_nnf,plain,
disjointwith(c_collection,c_individual),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
disjointwith(c_collection,c_individual),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(hi14,axiom,
disjointwith(c_collection,c_individual) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
fof(f8,axiom,
genls(c_partiallyintangibleindividual,c_individual),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just9) ).
fof(f8_nnf,plain,
genls(c_partiallyintangibleindividual,c_individual),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
genls(c_partiallyintangibleindividual,c_individual),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(hi8,axiom,
genls(c_partiallyintangibleindividual,c_individual) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(h17,plain,
disjointwith(c_collection,c_partiallyintangibleindividual) = true,
inference(hyper_resolution,[status(thm)],[hi40,hi14,hi8]) ).
cnf(h57,plain,
disjointwith(c_collection,c_aspatialinformationstore) = true,
inference(hyper_resolution,[status(thm)],[hi40,h17,h10]) ).
fof(f12,axiom,
genls(c_applicationcontext,c_microtheory),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just13) ).
fof(f12_nnf,plain,
genls(c_applicationcontext,c_microtheory),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
genls(c_applicationcontext,c_microtheory),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(hi12,axiom,
genls(c_applicationcontext,c_microtheory) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
fof(f1,axiom,
genls(c_microtheory,c_aspatialinformationstore),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just2) ).
fof(f1_nnf,plain,
genls(c_microtheory,c_aspatialinformationstore),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
genls(c_microtheory,c_aspatialinformationstore),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(hi1,axiom,
genls(c_microtheory,c_aspatialinformationstore) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(h15,plain,
genls(c_applicationcontext,c_aspatialinformationstore) = true,
inference(hyper_resolution,[status(thm)],[hi72,hi12,hi1]) ).
fof(f77,axiom,
! [X] :
( applicationcontext(X)
=> isa(X,c_applicationcontext) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just78) ).
fof(f77_nnf,plain,
! [X] :
( isa(X,c_applicationcontext)
| ~ applicationcontext(X) ),
inference(nnf_transformation,[status(thm)],[f77]) ).
fof(f77_sk,plain,
! [X] :
( isa(X,c_applicationcontext)
| ~ applicationcontext(X) ),
inference(skolemisation,[status(esa)],[f77_nnf]) ).
cnf(c77,plain,
( isa(X0,c_applicationcontext)
| ~ applicationcontext(X0) ),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(hi74,axiom,
ifeq(applicationcontext(X0),true,isa(X0,c_applicationcontext),true) = true,
inference(equality_encoding,[status(esa)],[c77]) ).
fof(f0,axiom,
applicationcontext(c_wamt_evalinitial_p14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just1) ).
fof(f0_nnf,plain,
applicationcontext(c_wamt_evalinitial_p14),
inference(nnf_transformation,[status(thm)],[f0]) ).
cnf(c0,plain,
applicationcontext(c_wamt_evalinitial_p14),
inference(cnf_transformation,[status(esa)],[f0_nnf]) ).
cnf(hi0,axiom,
applicationcontext(c_wamt_evalinitial_p14) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h0,plain,
isa(c_wamt_evalinitial_p14,c_applicationcontext) = true,
inference(hyper_resolution,[status(thm)],[hi74,hi0]) ).
fof(f82,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& isa(ARG1,OLD) )
=> isa(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just83) ).
fof(f82_nnf,plain,
! [ARG1,OLD,NEW] :
( isa(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ isa(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [ARG1,OLD,NEW] :
( isa(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ isa(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c82,plain,
( isa(X0,X2)
| ~ genls(X1,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(hi79,axiom,
ifeq(isa(X0,X1),true,ifeq(genls(X1,X2),true,isa(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c82]) ).
cnf(h53,plain,
isa(c_wamt_evalinitial_p14,c_aspatialinformationstore) = true,
inference(hyper_resolution,[status(thm)],[hi79,h0,h15]) ).
fof(f70,axiom,
! [INS,ARG2] :
( genls(INS,ARG2)
=> collection(INS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just71) ).
fof(f70_nnf,plain,
! [INS,ARG2] :
( collection(INS)
| ~ genls(INS,ARG2) ),
inference(nnf_transformation,[status(thm)],[f70]) ).
fof(f70_sk,plain,
! [INS,ARG2] :
( collection(INS)
| ~ genls(INS,ARG2) ),
inference(skolemisation,[status(esa)],[f70_nnf]) ).
cnf(c70,plain,
( collection(X0)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f70_sk]) ).
cnf(hi67,axiom,
ifeq(genls(X0,X1),true,collection(X0),true) = true,
inference(equality_encoding,[status(esa)],[c70]) ).
fof(f84,conjecture,
~ genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query45) ).
fof(f84_neg,negated_conjecture,
~ ~ genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
inference(negated_conjecture,[status(cth)],[f84]) ).
fof(f84_nnf,plain,
genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
inference(nnf_transformation,[status(thm)],[f84_neg]) ).
cnf(c84,plain,
genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
inference(cnf_transformation,[status(esa)],[f84_nnf]) ).
cnf(hi81,negated_conjecture,
genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088) = true,
inference(equality_encoding,[status(esa)],[c84]) ).
cnf(h21,plain,
collection(c_wamt_evalinitial_p14) = true,
inference(hyper_resolution,[status(thm)],[hi67,hi81]) ).
fof(f39,axiom,
! [X] :
( collection(X)
=> isa(X,c_collection) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just40) ).
fof(f39_nnf,plain,
! [X] :
( isa(X,c_collection)
| ~ collection(X) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [X] :
( isa(X,c_collection)
| ~ collection(X) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( isa(X0,c_collection)
| ~ collection(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(hi36,axiom,
ifeq(collection(X0),true,isa(X0,c_collection),true) = true,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(h63,plain,
isa(c_wamt_evalinitial_p14,c_collection) = true,
inference(hyper_resolution,[status(thm)],[hi36,h21]) ).
fof(f20,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just21) ).
fof(f20_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(hi84,axiom,
ifeq(isa(X0,X1),true,ifeq(isa(X0,X2),true,ifeq(disjointwith(X1,X2),true,false,true),true),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi84,h63,h53,h57]) ).
cnf(t1182,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f14,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just15) ).
fof(f14_nnf,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
fof(f16,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just17) ).
fof(f16_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c14,c16,c20]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1182]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR045+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/10.38 % Computer : n013.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.39 % CPULimit : 300
% 0.10/10.39 % WCLimit : 300
% 0.10/10.39 % DateTime : Fri Sep 25 08:29:02 UTC 2026
% 0.10/10.39 % CPUTime :
% 0.10/10.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.39/11.32 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.39/11.32 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------