%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR063+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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:38 PM UTC 2026
% Result : Theorem 215.74s 27.74s
% Output : Proof 215.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 20
% Syntax : Number of formulae : 106 ( 46 unt; 0 def)
% Number of atoms : 170 ( 25 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 153 ( 89 ~; 48 |; 7 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-4 aty)
% Number of variables : 109 ( 8 sgn 69 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f493,axiom,
! [OBJ] :
( computerdataartifact(OBJ)
=> artifact(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_494) ).
fof(f493_nnf,plain,
! [OBJ] :
( artifact(OBJ)
| ~ computerdataartifact(OBJ) ),
inference(nnf_transformation,[status(thm)],[f493]) ).
fof(f493_sk,plain,
! [OBJ] :
( artifact(OBJ)
| ~ computerdataartifact(OBJ) ),
inference(skolemisation,[status(esa)],[f493_nnf]) ).
cnf(c493,plain,
( artifact(X0)
| ~ computerdataartifact(X0) ),
inference(cnf_transformation,[status(esa)],[f493_sk]) ).
cnf(hi487,axiom,
ifeq(computerdataartifact(X0),true,artifact(X0),true) = true,
inference(equality_encoding,[status(esa)],[c493]) ).
fof(f1084,axiom,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_1085) ).
fof(f1084_nnf,plain,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)),
inference(nnf_transformation,[status(thm)],[f1084]) ).
fof(f1084_sk,plain,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)),
inference(skolemisation,[status(esa)],[f1084_nnf]) ).
cnf(c1084,plain,
computerdataartifact(f_urlreferentfn(X0)),
inference(cnf_transformation,[status(esa)],[f1084_sk]) ).
cnf(hi1075,axiom,
computerdataartifact(f_urlreferentfn(X0)) = true,
inference(equality_encoding,[status(esa)],[c1084]) ).
cnf(h2185,plain,
artifact(f_urlreferentfn(V0)) = true,
inference(hyper_resolution,[status(thm)],[hi487,hi1075]) ).
fof(f210,axiom,
! [OBJ] :
( artifact(OBJ)
=> inanimateobject_nonnatural(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_211) ).
fof(f210_nnf,plain,
! [OBJ] :
( inanimateobject_nonnatural(OBJ)
| ~ artifact(OBJ) ),
inference(nnf_transformation,[status(thm)],[f210]) ).
fof(f210_sk,plain,
! [OBJ] :
( inanimateobject_nonnatural(OBJ)
| ~ artifact(OBJ) ),
inference(skolemisation,[status(esa)],[f210_nnf]) ).
cnf(c210,plain,
( inanimateobject_nonnatural(X0)
| ~ artifact(X0) ),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
cnf(hi207,axiom,
ifeq(artifact(X0),true,inanimateobject_nonnatural(X0),true) = true,
inference(equality_encoding,[status(esa)],[c210]) ).
cnf(h4873,plain,
inanimateobject_nonnatural(f_urlreferentfn(V0)) = true,
inference(hyper_resolution,[status(thm)],[hi207,h2185]) ).
fof(f195,axiom,
! [OBJ] :
( inanimateobject_nonnatural(OBJ)
=> inanimateobject(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_196) ).
fof(f195_nnf,plain,
! [OBJ] :
( inanimateobject(OBJ)
| ~ inanimateobject_nonnatural(OBJ) ),
inference(nnf_transformation,[status(thm)],[f195]) ).
fof(f195_sk,plain,
! [OBJ] :
( inanimateobject(OBJ)
| ~ inanimateobject_nonnatural(OBJ) ),
inference(skolemisation,[status(esa)],[f195_nnf]) ).
cnf(c195,plain,
( inanimateobject(X0)
| ~ inanimateobject_nonnatural(X0) ),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
cnf(hi192,axiom,
ifeq(inanimateobject_nonnatural(X0),true,inanimateobject(X0),true) = true,
inference(equality_encoding,[status(esa)],[c195]) ).
cnf(h6566,plain,
inanimateobject(f_urlreferentfn(V0)) = true,
inference(hyper_resolution,[status(thm)],[hi192,h4873]) ).
fof(f8,axiom,
! [OBJ] :
( inanimateobject(OBJ)
=> partiallytangible(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_9) ).
fof(f8_nnf,plain,
! [OBJ] :
( partiallytangible(OBJ)
| ~ inanimateobject(OBJ) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [OBJ] :
( partiallytangible(OBJ)
| ~ inanimateobject(OBJ) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( partiallytangible(X0)
| ~ inanimateobject(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi7,axiom,
ifeq(inanimateobject(X0),true,partiallytangible(X0),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(h11561,plain,
partiallytangible(f_urlreferentfn(V0)) = true,
inference(hyper_resolution,[status(thm)],[hi7,h6566]) ).
fof(f220,axiom,
! [ARG1,ARG2] :
( disjointwith(ARG1,ARG2)
=> no(ARG1,ARG2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_221) ).
fof(f220_nnf,plain,
! [ARG1,ARG2] :
( no(ARG1,ARG2)
| ~ disjointwith(ARG1,ARG2) ),
inference(nnf_transformation,[status(thm)],[f220]) ).
fof(f220_sk,plain,
! [ARG1,ARG2] :
( no(ARG1,ARG2)
| ~ disjointwith(ARG1,ARG2) ),
inference(skolemisation,[status(esa)],[f220_nnf]) ).
cnf(c220,plain,
( no(X0,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f220_sk]) ).
cnf(hi217,axiom,
ifeq(disjointwith(X0,X1),true,no(X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c220]) ).
fof(f1131,conjecture,
~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query113) ).
fof(f1131_neg,negated_conjecture,
~ ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(negated_conjecture,[status(cth)],[f1131]) ).
fof(f1131_nnf,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(nnf_transformation,[status(thm)],[f1131_neg]) ).
cnf(c1131,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(cnf_transformation,[status(esa)],[f1131_nnf]) ).
cnf(hi1122,negated_conjecture,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) = true,
inference(equality_encoding,[status(esa)],[c1131]) ).
cnf(h23529,plain,
no(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) = true,
inference(hyper_resolution,[status(thm)],[hi217,hi1122]) ).
fof(f717,axiom,
! [INS,ARG2] :
( no(INS,ARG2)
=> setorcollection(INS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_718) ).
fof(f717_nnf,plain,
! [INS,ARG2] :
( setorcollection(INS)
| ~ no(INS,ARG2) ),
inference(nnf_transformation,[status(thm)],[f717]) ).
fof(f717_sk,plain,
! [INS,ARG2] :
( setorcollection(INS)
| ~ no(INS,ARG2) ),
inference(skolemisation,[status(esa)],[f717_nnf]) ).
cnf(c717,plain,
( setorcollection(X0)
| ~ no(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f717_sk]) ).
cnf(hi709,axiom,
ifeq(no(X0,X1),true,setorcollection(X0),true) = true,
inference(equality_encoding,[status(esa)],[c717]) ).
cnf(h23547,plain,
setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) = true,
inference(hyper_resolution,[status(thm)],[hi709,h23529]) ).
fof(f111,axiom,
! [OBJ] :
( setorcollection(OBJ)
=> mathematicalthing(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_112) ).
fof(f111_nnf,plain,
! [OBJ] :
( mathematicalthing(OBJ)
| ~ setorcollection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f111]) ).
fof(f111_sk,plain,
! [OBJ] :
( mathematicalthing(OBJ)
| ~ setorcollection(OBJ) ),
inference(skolemisation,[status(esa)],[f111_nnf]) ).
cnf(c111,plain,
( mathematicalthing(X0)
| ~ setorcollection(X0) ),
inference(cnf_transformation,[status(esa)],[f111_sk]) ).
cnf(hi110,axiom,
ifeq(setorcollection(X0),true,mathematicalthing(X0),true) = true,
inference(equality_encoding,[status(esa)],[c111]) ).
cnf(h23552,plain,
mathematicalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) = true,
inference(hyper_resolution,[status(thm)],[hi110,h23547]) ).
fof(f179,axiom,
! [OBJ] :
( mathematicalthing(OBJ)
=> mathematicalorcomputationalthing(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_180) ).
fof(f179_nnf,plain,
! [OBJ] :
( mathematicalorcomputationalthing(OBJ)
| ~ mathematicalthing(OBJ) ),
inference(nnf_transformation,[status(thm)],[f179]) ).
fof(f179_sk,plain,
! [OBJ] :
( mathematicalorcomputationalthing(OBJ)
| ~ mathematicalthing(OBJ) ),
inference(skolemisation,[status(esa)],[f179_nnf]) ).
cnf(c179,plain,
( mathematicalorcomputationalthing(X0)
| ~ mathematicalthing(X0) ),
inference(cnf_transformation,[status(esa)],[f179_sk]) ).
cnf(hi176,axiom,
ifeq(mathematicalthing(X0),true,mathematicalorcomputationalthing(X0),true) = true,
inference(equality_encoding,[status(esa)],[c179]) ).
cnf(h23554,plain,
mathematicalorcomputationalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) = true,
inference(hyper_resolution,[status(thm)],[hi176,h23552]) ).
fof(f131,axiom,
! [OBJ] :
( mathematicalorcomputationalthing(OBJ)
=> intangible(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_132) ).
fof(f131_nnf,plain,
! [OBJ] :
( intangible(OBJ)
| ~ mathematicalorcomputationalthing(OBJ) ),
inference(nnf_transformation,[status(thm)],[f131]) ).
fof(f131_sk,plain,
! [OBJ] :
( intangible(OBJ)
| ~ mathematicalorcomputationalthing(OBJ) ),
inference(skolemisation,[status(esa)],[f131_nnf]) ).
cnf(c131,plain,
( intangible(X0)
| ~ mathematicalorcomputationalthing(X0) ),
inference(cnf_transformation,[status(esa)],[f131_sk]) ).
cnf(hi130,axiom,
ifeq(mathematicalorcomputationalthing(X0),true,intangible(X0),true) = true,
inference(equality_encoding,[status(esa)],[c131]) ).
cnf(h23556,plain,
intangible(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) = true,
inference(hyper_resolution,[status(thm)],[hi130,h23554]) ).
fof(f2,axiom,
! [OBJ] :
~ ( partiallytangible(OBJ)
& intangible(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_3) ).
fof(f2_nnf,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ~ partiallytangible(X0)
| ~ intangible(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi1123,axiom,
ifeq(intangible(X0),true,ifeq(partiallytangible(X0),true,false,true),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi1123,h23556,h11561]) ).
cnf(t478,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f152,axiom,
! [OBJ] :
~ ( tptpcol_1_65536(OBJ)
& tptpcol_1_1(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_153) ).
fof(f152_nnf,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(nnf_transformation,[status(thm)],[f152]) ).
fof(f152_sk,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(skolemisation,[status(esa)],[f152_nnf]) ).
cnf(c152,plain,
( ~ tptpcol_1_65536(X0)
| ~ tptpcol_1_1(X0) ),
inference(cnf_transformation,[status(esa)],[f152_sk]) ).
fof(f166,axiom,
! [OBJ] :
~ ( setorcollection(OBJ)
& individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_167) ).
fof(f166_nnf,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(nnf_transformation,[status(thm)],[f166]) ).
fof(f166_sk,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(skolemisation,[status(esa)],[f166_nnf]) ).
cnf(c166,plain,
( ~ setorcollection(X0)
| ~ individual(X0) ),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
fof(f288,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_289) ).
fof(f288_nnf,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f288]) ).
fof(f288_sk,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(skolemisation,[status(esa)],[f288_nnf]) ).
cnf(c288,plain,
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(esa)],[f288_sk]) ).
fof(f362,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_363) ).
fof(f362_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f362]) ).
fof(f362_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f362_nnf]) ).
cnf(c362,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f362_sk]) ).
fof(f487,axiom,
! [OBJ] :
~ ( tptpcol_3_114688(OBJ)
& tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_488) ).
fof(f487_nnf,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(nnf_transformation,[status(thm)],[f487]) ).
fof(f487_sk,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(skolemisation,[status(esa)],[f487_nnf]) ).
cnf(c487,plain,
( ~ tptpcol_3_114688(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(esa)],[f487_sk]) ).
fof(f520,axiom,
! [X] : ~ affiliatedwith(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_521) ).
fof(f520_nnf,plain,
! [X] : ~ affiliatedwith(X,X),
inference(nnf_transformation,[status(thm)],[f520]) ).
fof(f520_sk,plain,
! [X] : ~ affiliatedwith(X,X),
inference(skolemisation,[status(esa)],[f520_nnf]) ).
cnf(c520,plain,
~ affiliatedwith(X0,X0),
inference(cnf_transformation,[status(esa)],[f520_sk]) ).
fof(f697,axiom,
! [X] : ~ objectfoundinlocation(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_698) ).
fof(f697_nnf,plain,
! [X] : ~ objectfoundinlocation(X,X),
inference(nnf_transformation,[status(thm)],[f697]) ).
fof(f697_sk,plain,
! [X] : ~ objectfoundinlocation(X,X),
inference(skolemisation,[status(esa)],[f697_nnf]) ).
cnf(c697,plain,
~ objectfoundinlocation(X0,X0),
inference(cnf_transformation,[status(esa)],[f697_sk]) ).
fof(f900,axiom,
! [X] : ~ borderson(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_901) ).
fof(f900_nnf,plain,
! [X] : ~ borderson(X,X),
inference(nnf_transformation,[status(thm)],[f900]) ).
fof(f900_sk,plain,
! [X] : ~ borderson(X,X),
inference(skolemisation,[status(esa)],[f900_nnf]) ).
cnf(c900,plain,
~ borderson(X0,X0),
inference(cnf_transformation,[status(esa)],[f900_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c152,c166,c288,c362,c487,c520,c697,c900]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t478]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR063+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.42 % Computer : n007.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Fri Sep 25 08:45:38 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 215.74/27.74 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 215.74/27.74 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------