%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR063+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 : n001.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 5.55s 1.26s
% Output : Proof 5.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 23
% Syntax : Number of formulae : 121 ( 69 unt; 0 def)
% Number of atoms : 201 ( 36 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 161 ( 81 ~; 60 |; 11 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 13 con; 0-4 aty)
% Number of variables : 150 ( 6 sgn 93 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f113,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& genls(ARG1,OLD) )
=> genls(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just114) ).
fof(f113_nnf,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f113]) ).
fof(f113_sk,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f113_nnf]) ).
cnf(c113,plain,
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f113_sk]) ).
cnf(hi109,axiom,
ifeq(genls(X0,X1),true,ifeq(genls(X1,X2),true,genls(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c113]) ).
fof(f0,axiom,
genls(c_setorcollection,c_mathematicalthing),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just1) ).
fof(f0_nnf,plain,
genls(c_setorcollection,c_mathematicalthing),
inference(nnf_transformation,[status(thm)],[f0]) ).
cnf(c0,plain,
genls(c_setorcollection,c_mathematicalthing),
inference(cnf_transformation,[status(esa)],[f0_nnf]) ).
cnf(hi0,axiom,
genls(c_setorcollection,c_mathematicalthing) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
fof(f9,axiom,
genls(c_mathematicalthing,c_mathematicalorcomputationalthing),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just10) ).
fof(f9_nnf,plain,
genls(c_mathematicalthing,c_mathematicalorcomputationalthing),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
genls(c_mathematicalthing,c_mathematicalorcomputationalthing),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(hi8,axiom,
genls(c_mathematicalthing,c_mathematicalorcomputationalthing) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(h13,plain,
genls(c_setorcollection,c_mathematicalorcomputationalthing) = true,
inference(hyper_resolution,[status(thm)],[hi109,hi0,hi8]) ).
fof(f82,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just83) ).
fof(f82_nnf,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c82,plain,
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(hi78,axiom,
ifeq(disjointwith(X0,X1),true,ifeq(genls(X2,X0),true,disjointwith(X2,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c82]) ).
fof(f5,axiom,
disjointwith(c_intangible,c_partiallytangible),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just6) ).
fof(f5_nnf,plain,
disjointwith(c_intangible,c_partiallytangible),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
disjointwith(c_intangible,c_partiallytangible),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(hi5,axiom,
disjointwith(c_intangible,c_partiallytangible) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
fof(f3,axiom,
genls(c_mathematicalorcomputationalthing,c_intangible),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just4) ).
fof(f3_nnf,plain,
genls(c_mathematicalorcomputationalthing,c_intangible),
inference(nnf_transformation,[status(thm)],[f3]) ).
cnf(c3,plain,
genls(c_mathematicalorcomputationalthing,c_intangible),
inference(cnf_transformation,[status(esa)],[f3_nnf]) ).
cnf(hi3,axiom,
genls(c_mathematicalorcomputationalthing,c_intangible) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(h7,plain,
disjointwith(c_mathematicalorcomputationalthing,c_partiallytangible) = true,
inference(hyper_resolution,[status(thm)],[hi78,hi5,hi3]) ).
fof(f80,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just81) ).
fof(f80_nnf,plain,
! [X,Y] :
( disjointwith(Y,X)
| ~ disjointwith(X,Y) ),
inference(nnf_transformation,[status(thm)],[f80]) ).
fof(f80_sk,plain,
! [X,Y] :
( disjointwith(Y,X)
| ~ disjointwith(X,Y) ),
inference(skolemisation,[status(esa)],[f80_nnf]) ).
cnf(c80,plain,
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f80_sk]) ).
cnf(hi76,axiom,
ifeq(disjointwith(X0,X1),true,disjointwith(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c80]) ).
cnf(h47,plain,
disjointwith(c_partiallytangible,c_mathematicalorcomputationalthing) = true,
inference(hyper_resolution,[status(thm)],[hi76,h7]) ).
fof(f81,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just82) ).
fof(f81_nnf,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f81]) ).
fof(f81_sk,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f81_nnf]) ).
cnf(c81,plain,
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f81_sk]) ).
cnf(hi77,axiom,
ifeq(disjointwith(X0,X1),true,ifeq(genls(X2,X1),true,disjointwith(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c81]) ).
cnf(h105,plain,
disjointwith(c_partiallytangible,c_setorcollection) = true,
inference(hyper_resolution,[status(thm)],[hi77,h47,h13]) ).
fof(f21,axiom,
! [ARG1,ARG2] :
( disjointwith(ARG1,ARG2)
=> no(ARG1,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just22) ).
fof(f21_nnf,plain,
! [ARG1,ARG2] :
( no(ARG1,ARG2)
| ~ disjointwith(ARG1,ARG2) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [ARG1,ARG2] :
( no(ARG1,ARG2)
| ~ disjointwith(ARG1,ARG2) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( no(X0,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(hi19,axiom,
ifeq(disjointwith(X0,X1),true,no(X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
fof(f115,conjecture,
~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query63) ).
fof(f115_neg,negated_conjecture,
~ ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(negated_conjecture,[status(cth)],[f115]) ).
fof(f115_nnf,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(nnf_transformation,[status(thm)],[f115_neg]) ).
cnf(c115,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(cnf_transformation,[status(esa)],[f115_nnf]) ).
cnf(hi111,negated_conjecture,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) = true,
inference(equality_encoding,[status(esa)],[c115]) ).
cnf(h38,plain,
no(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) = true,
inference(hyper_resolution,[status(thm)],[hi19,hi111]) ).
fof(f43,axiom,
! [INS,ARG2] :
( no(INS,ARG2)
=> setorcollection(INS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just44) ).
fof(f43_nnf,plain,
! [INS,ARG2] :
( setorcollection(INS)
| ~ no(INS,ARG2) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [INS,ARG2] :
( setorcollection(INS)
| ~ no(INS,ARG2) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
( setorcollection(X0)
| ~ no(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(hi39,axiom,
ifeq(no(X0,X1),true,setorcollection(X0),true) = true,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(h87,plain,
setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) = true,
inference(hyper_resolution,[status(thm)],[hi39,h38]) ).
fof(f104,axiom,
! [X] :
( setorcollection(X)
=> isa(X,c_setorcollection) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just105) ).
fof(f104_nnf,plain,
! [X] :
( isa(X,c_setorcollection)
| ~ setorcollection(X) ),
inference(nnf_transformation,[status(thm)],[f104]) ).
fof(f104_sk,plain,
! [X] :
( isa(X,c_setorcollection)
| ~ setorcollection(X) ),
inference(skolemisation,[status(esa)],[f104_nnf]) ).
cnf(c104,plain,
( isa(X0,c_setorcollection)
| ~ setorcollection(X0) ),
inference(cnf_transformation,[status(esa)],[f104_sk]) ).
cnf(hi100,axiom,
ifeq(setorcollection(X0),true,isa(X0,c_setorcollection),true) = true,
inference(equality_encoding,[status(esa)],[c104]) ).
cnf(h179,plain,
isa(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_setorcollection) = true,
inference(hyper_resolution,[status(thm)],[hi100,h87]) ).
fof(f14,axiom,
genls(c_inanimateobject_nonnatural,c_inanimateobject),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just15) ).
fof(f14_nnf,plain,
genls(c_inanimateobject_nonnatural,c_inanimateobject),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
genls(c_inanimateobject_nonnatural,c_inanimateobject),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(hi13,axiom,
genls(c_inanimateobject_nonnatural,c_inanimateobject) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
fof(f16,axiom,
genls(c_inanimateobject,c_partiallytangible),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just17) ).
fof(f16_nnf,plain,
genls(c_inanimateobject,c_partiallytangible),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
genls(c_inanimateobject,c_partiallytangible),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(hi15,axiom,
genls(c_inanimateobject,c_partiallytangible) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(h22,plain,
genls(c_inanimateobject_nonnatural,c_partiallytangible) = true,
inference(hyper_resolution,[status(thm)],[hi109,hi13,hi15]) ).
fof(f7,axiom,
genls(c_computerdataartifact,c_artifact),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just8) ).
fof(f7_nnf,plain,
genls(c_computerdataartifact,c_artifact),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
genls(c_computerdataartifact,c_artifact),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(hi6,axiom,
genls(c_computerdataartifact,c_artifact) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
fof(f12,axiom,
genls(c_artifact,c_inanimateobject_nonnatural),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just13) ).
fof(f12_nnf,plain,
genls(c_artifact,c_inanimateobject_nonnatural),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
genls(c_artifact,c_inanimateobject_nonnatural),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(hi11,axiom,
genls(c_artifact,c_inanimateobject_nonnatural) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(h17,plain,
genls(c_computerdataartifact,c_inanimateobject_nonnatural) = true,
inference(hyper_resolution,[status(thm)],[hi109,hi6,hi11]) ).
cnf(h70,plain,
genls(c_computerdataartifact,c_partiallytangible) = true,
inference(hyper_resolution,[status(thm)],[hi109,h17,h22]) ).
fof(f88,axiom,
! [X] :
( computerdataartifact(X)
=> isa(X,c_computerdataartifact) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just89) ).
fof(f88_nnf,plain,
! [X] :
( isa(X,c_computerdataartifact)
| ~ computerdataartifact(X) ),
inference(nnf_transformation,[status(thm)],[f88]) ).
fof(f88_sk,plain,
! [X] :
( isa(X,c_computerdataartifact)
| ~ computerdataartifact(X) ),
inference(skolemisation,[status(esa)],[f88_nnf]) ).
cnf(c88,plain,
( isa(X0,c_computerdataartifact)
| ~ computerdataartifact(X0) ),
inference(cnf_transformation,[status(esa)],[f88_sk]) ).
cnf(hi84,axiom,
ifeq(computerdataartifact(X0),true,isa(X0,c_computerdataartifact),true) = true,
inference(equality_encoding,[status(esa)],[c88]) ).
fof(f94,axiom,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just95) ).
fof(f94_nnf,plain,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)),
inference(nnf_transformation,[status(thm)],[f94]) ).
fof(f94_sk,plain,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)),
inference(skolemisation,[status(esa)],[f94_nnf]) ).
cnf(c94,plain,
computerdataartifact(f_urlreferentfn(X0)),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi90,axiom,
computerdataartifact(f_urlreferentfn(X0)) = true,
inference(equality_encoding,[status(esa)],[c94]) ).
cnf(h33,plain,
isa(f_urlreferentfn(V0),c_computerdataartifact) = true,
inference(hyper_resolution,[status(thm)],[hi84,hi90]) ).
fof(f99,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& isa(ARG1,OLD) )
=> isa(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just100) ).
fof(f99_nnf,plain,
! [ARG1,OLD,NEW] :
( isa(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ isa(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f99]) ).
fof(f99_sk,plain,
! [ARG1,OLD,NEW] :
( isa(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ isa(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f99_nnf]) ).
cnf(c99,plain,
( isa(X0,X2)
| ~ genls(X1,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f99_sk]) ).
cnf(hi95,axiom,
ifeq(isa(X0,X1),true,ifeq(genls(X1,X2),true,isa(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c99]) ).
cnf(h156,plain,
isa(f_urlreferentfn(V0),c_partiallytangible) = true,
inference(hyper_resolution,[status(thm)],[hi95,h33,h70]) ).
fof(f29,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just30) ).
fof(f29_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(hi115,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)],[c29]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi115,h156,h179,h105]) ).
cnf(t1422,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f6,axiom,
! [OBJ] :
~ ( partiallytangible(OBJ)
& intangible(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just7) ).
fof(f6_nnf,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( ~ partiallytangible(X0)
| ~ intangible(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
fof(f18,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just19) ).
fof(f18_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f18_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]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c6,c18,c25,c29]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1422]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR063+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.15/0.39 % Computer : n001.cluster.edu
% 0.15/0.39 % Model : x86_64 x86_64
% 0.15/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.39 % Memory : 8046.5625MB
% 0.15/0.39 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Fri Sep 25 08:53:40 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.15/0.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.55/1.26 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.55/1.26 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------