%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : CSR063+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 11:18:57 AM UTC 2025
% Result : Theorem 9.13s 1.50s
% Output : CNFRefutation 9.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 20
% Syntax : Number of formulae : 65 ( 32 unt; 0 def)
% Number of atoms : 116 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 93 ( 42 ~; 36 |; 6 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-1 aty)
% Number of variables : 46 ( 1 sgn 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(query63,plain,
~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query63) ).
fof(query63_negated,plain,
~ ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(negate_conjecture,[status(cth)],[query63]) ).
cnf(115,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(cnf,[status(esa)],[query63_negated]) ).
cnf(l0,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(instantiation,[status(thm)],[115]) ).
fof(just22,plain,
! [ARG1,ARG2] :
( disjointwith(ARG1,ARG2)
=> no(ARG1,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just22) ).
cnf(21,plain,
( ~ disjointwith(X0,X1)
| no(X0,X1) ),
inference(cnf,[status(esa)],[just22]) ).
cnf(l1,plain,
( ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949)
| no(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) ),
inference(instantiation,[status(thm)],[21]) ).
fof(just44,plain,
! [INS,ARG2] :
( no(INS,ARG2)
=> setorcollection(INS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just44) ).
cnf(43,plain,
( ~ no(X0,X1)
| setorcollection(X0) ),
inference(cnf,[status(esa)],[just44]) ).
cnf(l2,plain,
( ~ no(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949)
| setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) ),
inference(instantiation,[status(thm)],[43]) ).
fof(just105,plain,
! [X] :
( setorcollection(X)
=> isa(X,c_setorcollection) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just105) ).
cnf(104,plain,
( ~ setorcollection(X0)
| isa(X0,c_setorcollection) ),
inference(cnf,[status(esa)],[just105]) ).
cnf(l4,plain,
( ~ setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))
| isa(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_setorcollection) ),
inference(instantiation,[status(thm)],[104]) ).
fof(just100,plain,
! [ARG1,OLD,NEW] :
( ( isa(ARG1,OLD)
& genls(OLD,NEW) )
=> isa(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just100) ).
cnf(99,plain,
( ~ genls(X0,X1)
| ~ isa(X2,X0)
| isa(X2,X1) ),
inference(cnf,[status(esa)],[just100]) ).
cnf(l229,plain,
( ~ genls(c_setorcollection,c_intangible)
| ~ isa(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_setorcollection)
| isa(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_intangible) ),
inference(instantiation,[status(thm)],[99]) ).
fof(just113,plain,
! [OLD,ARG2,NEW] :
( ( genls(OLD,ARG2)
& genls(NEW,OLD) )
=> genls(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just113) ).
cnf(112,plain,
( ~ genls(X0,X1)
| ~ genls(X2,X0)
| genls(X2,X1) ),
inference(cnf,[status(esa)],[just113]) ).
cnf(l230,plain,
( ~ genls(c_mathematicalorcomputationalthing,c_intangible)
| ~ genls(c_setorcollection,c_mathematicalorcomputationalthing)
| genls(c_setorcollection,c_intangible) ),
inference(instantiation,[status(thm)],[112]) ).
fof(just114,plain,
! [ARG1,OLD,NEW] :
( ( genls(ARG1,OLD)
& genls(OLD,NEW) )
=> genls(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just114) ).
cnf(113,plain,
( ~ genls(X0,X1)
| ~ genls(X1,X2)
| genls(X0,X2) ),
inference(cnf,[status(esa)],[just114]) ).
cnf(l322,plain,
( ~ genls(c_setorcollection,c_mathematicalthing)
| ~ genls(c_mathematicalthing,c_mathematicalorcomputationalthing)
| genls(c_setorcollection,c_mathematicalorcomputationalthing) ),
inference(instantiation,[status(thm)],[113]) ).
fof(just1,plain,
genls(c_setorcollection,c_mathematicalthing),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just1) ).
cnf(0,plain,
genls(c_setorcollection,c_mathematicalthing),
inference(cnf,[status(esa)],[just1]) ).
cnf(l323,plain,
genls(c_setorcollection,c_mathematicalthing),
inference(instantiation,[status(thm)],[0]) ).
fof(just10,plain,
genls(c_mathematicalthing,c_mathematicalorcomputationalthing),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just10) ).
cnf(9,plain,
genls(c_mathematicalthing,c_mathematicalorcomputationalthing),
inference(cnf,[status(esa)],[just10]) ).
cnf(l325,plain,
genls(c_mathematicalthing,c_mathematicalorcomputationalthing),
inference(instantiation,[status(thm)],[9]) ).
fof(just30,plain,
! [OBJ,COL1,COL2] :
~ ( isa(OBJ,COL1)
& isa(OBJ,COL2)
& disjointwith(COL1,COL2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just30) ).
cnf(29,plain,
( ~ disjointwith(X0,X1)
| ~ isa(X2,X0)
| ~ isa(X2,X1) ),
inference(cnf,[status(esa)],[just30]) ).
cnf(l320,plain,
( ~ disjointwith(c_inanimateobject_nonnatural,c_intangible)
| ~ isa(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_inanimateobject_nonnatural)
| ~ isa(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_intangible) ),
inference(instantiation,[status(thm)],[29]) ).
fof(just4,plain,
genls(c_mathematicalorcomputationalthing,c_intangible),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just4) ).
cnf(3,plain,
genls(c_mathematicalorcomputationalthing,c_intangible),
inference(cnf,[status(esa)],[just4]) ).
cnf(l327,plain,
genls(c_mathematicalorcomputationalthing,c_intangible),
inference(instantiation,[status(thm)],[3]) ).
fof(just83,plain,
! [OLD,ARG2,NEW] :
( ( disjointwith(OLD,ARG2)
& genls(NEW,OLD) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just83) ).
cnf(82,plain,
( ~ genls(X0,X1)
| ~ disjointwith(X1,X2)
| disjointwith(X0,X2) ),
inference(cnf,[status(esa)],[just83]) ).
cnf(l339,plain,
( ~ genls(c_inanimateobject_nonnatural,c_partiallytangible)
| ~ disjointwith(c_partiallytangible,c_intangible)
| disjointwith(c_inanimateobject_nonnatural,c_intangible) ),
inference(instantiation,[status(thm)],[82]) ).
fof(just81,plain,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just81) ).
cnf(80,plain,
( ~ disjointwith(X0,X1)
| disjointwith(X1,X0) ),
inference(cnf,[status(esa)],[just81]) ).
cnf(l341,plain,
( ~ disjointwith(c_intangible,c_partiallytangible)
| disjointwith(c_partiallytangible,c_intangible) ),
inference(instantiation,[status(thm)],[80]) ).
fof(just6,plain,
disjointwith(c_intangible,c_partiallytangible),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just6) ).
cnf(5,plain,
disjointwith(c_intangible,c_partiallytangible),
inference(cnf,[status(esa)],[just6]) ).
cnf(l351,plain,
disjointwith(c_intangible,c_partiallytangible),
inference(instantiation,[status(thm)],[5]) ).
cnf(l342,plain,
( ~ genls(c_inanimateobject_nonnatural,c_inanimateobject)
| ~ genls(c_inanimateobject,c_partiallytangible)
| genls(c_inanimateobject_nonnatural,c_partiallytangible) ),
inference(instantiation,[status(thm)],[113]) ).
fof(just17,plain,
genls(c_inanimateobject,c_partiallytangible),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just17) ).
cnf(16,plain,
genls(c_inanimateobject,c_partiallytangible),
inference(cnf,[status(esa)],[just17]) ).
cnf(l348,plain,
genls(c_inanimateobject,c_partiallytangible),
inference(instantiation,[status(thm)],[16]) ).
fof(just15,plain,
genls(c_inanimateobject_nonnatural,c_inanimateobject),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just15) ).
cnf(14,plain,
genls(c_inanimateobject_nonnatural,c_inanimateobject),
inference(cnf,[status(esa)],[just15]) ).
cnf(l343,plain,
genls(c_inanimateobject_nonnatural,c_inanimateobject),
inference(instantiation,[status(thm)],[14]) ).
cnf(l321,plain,
( ~ genls(c_computerdataartifact,c_inanimateobject_nonnatural)
| ~ isa(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_computerdataartifact)
| isa(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_inanimateobject_nonnatural) ),
inference(instantiation,[status(thm)],[99]) ).
cnf(l354,plain,
( ~ genls(c_computerdataartifact,c_artifact)
| ~ genls(c_artifact,c_inanimateobject_nonnatural)
| genls(c_computerdataartifact,c_inanimateobject_nonnatural) ),
inference(instantiation,[status(thm)],[113]) ).
fof(just13,plain,
genls(c_artifact,c_inanimateobject_nonnatural),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just13) ).
cnf(12,plain,
genls(c_artifact,c_inanimateobject_nonnatural),
inference(cnf,[status(esa)],[just13]) ).
cnf(l356,plain,
genls(c_artifact,c_inanimateobject_nonnatural),
inference(instantiation,[status(thm)],[12]) ).
fof(just8,plain,
genls(c_computerdataartifact,c_artifact),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just8) ).
cnf(7,plain,
genls(c_computerdataartifact,c_artifact),
inference(cnf,[status(esa)],[just8]) ).
cnf(l355,plain,
genls(c_computerdataartifact,c_artifact),
inference(instantiation,[status(thm)],[7]) ).
fof(just89,plain,
! [X] :
( computerdataartifact(X)
=> isa(X,c_computerdataartifact) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just89) ).
cnf(88,plain,
( ~ computerdataartifact(X0)
| isa(X0,c_computerdataartifact) ),
inference(cnf,[status(esa)],[just89]) ).
cnf(l333,plain,
( ~ computerdataartifact(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))
| isa(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_computerdataartifact) ),
inference(instantiation,[status(thm)],[88]) ).
fof(just3,plain,
computerdataartifact(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just3) ).
cnf(2,plain,
computerdataartifact(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(cnf,[status(esa)],[just3]) ).
cnf(l335,plain,
computerdataartifact(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(instantiation,[status(thm)],[2]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l4,l229,l230,l322,l323,l325,l320,l327,l339,l341,l351,l342,l348,l343,l321,l354,l356,l355,l333,l335]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : CSR063+1 : TPTP v9.0.0. Released v3.4.0.
% 0.10/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 07:09:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.12/0.34 % launching worker at depth: 11
% 0.12/0.35 % launching worker at depth: 12
% 0.18/0.42 % launching worker at depth: 13
% 0.18/0.56 % launching worker at depth: 14
% 7.69/1.38 % launching worker at depth: 15
% 9.13/1.50 % SZS status Theorem for theBenchmark
% 9.13/1.50 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------