%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR063+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 : Sun Sep 27 07:07:02 AM UTC 2026
% Result : Theorem 9.32s 2.14s
% Output : CNFRefutation 9.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 20
% Syntax : Number of formulae : 63 ( 35 unt; 0 def)
% Number of atoms : 101 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 68 ( 30 ~; 23 |; 6 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 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 : 61 ( 7 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1_221,axiom,
! [ARG1,ARG2] :
( disjointwith(ARG1,ARG2)
=> no(ARG1,ARG2) ),
file('theBenchmark.p',ax1_221) ).
fof(ax1_363,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('theBenchmark.p',ax1_363) ).
fof(ax1_717,axiom,
! [ARG1,INS] :
( no(ARG1,INS)
=> setorcollection(INS) ),
file('theBenchmark.p',ax1_717) ).
fof(ax1_886,axiom,
! [X] :
( setorcollection(X)
=> isa(X,c_setorcollection) ),
file('theBenchmark.p',ax1_886) ).
fof(ax1_928,axiom,
! [X] :
( computerdataartifact(X)
=> isa(X,c_computerdataartifact) ),
file('theBenchmark.p',ax1_928) ).
fof(ax1_1085,axiom,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)),
file('theBenchmark.p',ax1_1085) ).
fof(ax1_1094,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& isa(ARG1,OLD) )
=> isa(ARG1,NEW) ),
file('theBenchmark.p',ax1_1094) ).
fof(ax1_1109,axiom,
! [X,Y,Z] :
( ( genls(Y,Z)
& genls(X,Y) )
=> genls(X,Z) ),
file('theBenchmark.p',ax1_1109) ).
fof(ax1_1120,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('theBenchmark.p',ax1_1120) ).
fof(ax1_1121,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('theBenchmark.p',ax1_1121) ).
fof(ax1_1122,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('theBenchmark.p',ax1_1122) ).
fof(query113,conjecture,
~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
file('theBenchmark.p',query113) ).
fof(query113_neg,negated_conjecture,
~ ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(assume_negation,[status(cth)],[query113]) ).
fof(ax1_2,axiom,
disjointwith(c_intangible,c_partiallytangible),
file('theBenchmark.p',ax1_2) ).
cnf(c_1256,plain,
disjointwith(c_intangible,c_partiallytangible),
inference(clausify,[status(thm)],[ax1_2]) ).
fof(ax1_8,axiom,
genls(c_inanimateobject,c_partiallytangible),
file('theBenchmark.p',ax1_8) ).
cnf(c_1260,plain,
genls(c_inanimateobject,c_partiallytangible),
inference(clausify,[status(thm)],[ax1_8]) ).
fof(ax1_111,axiom,
genls(c_setorcollection,c_mathematicalthing),
file('theBenchmark.p',ax1_111) ).
cnf(c_1320,plain,
genls(c_setorcollection,c_mathematicalthing),
inference(clausify,[status(thm)],[ax1_111]) ).
fof(ax1_131,axiom,
genls(c_mathematicalorcomputationalthing,c_intangible),
file('theBenchmark.p',ax1_131) ).
cnf(c_1334,plain,
genls(c_mathematicalorcomputationalthing,c_intangible),
inference(clausify,[status(thm)],[ax1_131]) ).
fof(ax1_179,axiom,
genls(c_mathematicalthing,c_mathematicalorcomputationalthing),
file('theBenchmark.p',ax1_179) ).
cnf(c_1361,plain,
genls(c_mathematicalthing,c_mathematicalorcomputationalthing),
inference(clausify,[status(thm)],[ax1_179]) ).
fof(ax1_195,axiom,
genls(c_inanimateobject_nonnatural,c_inanimateobject),
file('theBenchmark.p',ax1_195) ).
cnf(c_1373,plain,
genls(c_inanimateobject_nonnatural,c_inanimateobject),
inference(clausify,[status(thm)],[ax1_195]) ).
fof(ax1_210,axiom,
genls(c_artifact,c_inanimateobject_nonnatural),
file('theBenchmark.p',ax1_210) ).
cnf(c_1382,plain,
genls(c_artifact,c_inanimateobject_nonnatural),
inference(clausify,[status(thm)],[ax1_210]) ).
cnf(c_1387,plain,
( no(A,B)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[ax1_221]) ).
cnf(c_1471,plain,
( ~ disjointwith(B,C)
| ~ isa(A,C)
| ~ isa(A,B) ),
inference(clausify,[status(thm)],[ax1_363]) ).
fof(ax1_493,axiom,
genls(c_computerdataartifact,c_artifact),
file('theBenchmark.p',ax1_493) ).
cnf(c_1552,plain,
genls(c_computerdataartifact,c_artifact),
inference(clausify,[status(thm)],[ax1_493]) ).
cnf(c_1692,plain,
( setorcollection(B)
| ~ no(A,B) ),
inference(clausify,[status(thm)],[ax1_717]) ).
cnf(c_1793,plain,
( isa(A,c_setorcollection)
| ~ setorcollection(A) ),
inference(clausify,[status(thm)],[ax1_886]) ).
cnf(c_1821,plain,
( isa(A,c_computerdataartifact)
| ~ computerdataartifact(A) ),
inference(clausify,[status(thm)],[ax1_928]) ).
cnf(c_1933,plain,
computerdataartifact(f_urlreferentfn(A)),
inference(clausify,[status(thm)],[ax1_1085]) ).
cnf(c_1939,plain,
( isa(A,C)
| ~ genls(B,C)
| ~ isa(A,B) ),
inference(clausify,[status(thm)],[ax1_1094]) ).
cnf(c_1947,plain,
( genls(A,C)
| ~ genls(B,C)
| ~ genls(A,B) ),
inference(clausify,[status(thm)],[ax1_1109]) ).
cnf(c_1954,plain,
( disjointwith(B,A)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[ax1_1120]) ).
cnf(c_1955,plain,
( disjointwith(A,C)
| ~ genls(C,B)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[ax1_1121]) ).
cnf(c_1956,plain,
( disjointwith(C,B)
| ~ genls(C,A)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[ax1_1122]) ).
cnf(c_1962,negated_conjecture,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(clausify,[status(thm)],[query113_neg]) ).
cnf(c_13755,plain,
( disjointwith(c_intangible,A)
| ~ genls(A,c_partiallytangible) ),
inference(resolve,[status(thm)],[c_1955,c_1256]) ).
cnf(c_2068,plain,
disjointwith(c_intangible,c_inanimateobject),
inference(resolve,[status(thm)],[c_13755,c_1260]) ).
cnf(c_2109,negated_conjecture,
disjointwith(c_tptpcol_16_118949,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolve,[status(thm)],[c_1954,c_1962]) ).
cnf(c_2127,plain,
no(c_tptpcol_16_118949,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolve,[status(thm)],[c_1387,c_2109]) ).
cnf(c_2208,plain,
setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolve,[status(thm)],[c_1692,c_2127]) ).
cnf(c_2521,plain,
isa(f_urlreferentfn(A),c_computerdataartifact),
inference(resolve,[status(thm)],[c_1821,c_1933]) ).
cnf(c_13756,plain,
( isa(f_urlreferentfn(B),A)
| ~ genls(c_computerdataartifact,A) ),
inference(resolve,[status(thm)],[c_1939,c_2521]) ).
cnf(c_2974,plain,
isa(f_urlreferentfn(A),c_artifact),
inference(resolve,[status(thm)],[c_13756,c_1552]) ).
cnf(c_13757,plain,
( disjointwith(A,c_inanimateobject)
| ~ genls(A,c_intangible) ),
inference(resolve,[status(thm)],[c_1956,c_2068]) ).
cnf(c_3812,plain,
disjointwith(c_mathematicalorcomputationalthing,c_inanimateobject),
inference(resolve,[status(thm)],[c_13757,c_1334]) ).
cnf(c_13758,plain,
( genls(c_setorcollection,A)
| ~ genls(c_mathematicalthing,A) ),
inference(resolve,[status(thm)],[c_1947,c_1320]) ).
cnf(c_4455,plain,
genls(c_setorcollection,c_mathematicalorcomputationalthing),
inference(resolve,[status(thm)],[c_13758,c_1361]) ).
cnf(c_13759,plain,
( genls(c_artifact,A)
| ~ genls(c_inanimateobject_nonnatural,A) ),
inference(resolve,[status(thm)],[c_1947,c_1382]) ).
cnf(c_4829,plain,
genls(c_artifact,c_inanimateobject),
inference(resolve,[status(thm)],[c_13759,c_1373]) ).
cnf(c_13760,plain,
( disjointwith(A,c_inanimateobject)
| ~ genls(A,c_mathematicalorcomputationalthing) ),
inference(resolve,[status(thm)],[c_1956,c_3812]) ).
cnf(c_6807,plain,
disjointwith(c_setorcollection,c_inanimateobject),
inference(resolve,[status(thm)],[c_13760,c_4455]) ).
cnf(c_13761,plain,
( disjointwith(c_setorcollection,A)
| ~ genls(A,c_inanimateobject) ),
inference(resolve,[status(thm)],[c_1955,c_6807]) ).
cnf(c_9207,plain,
disjointwith(c_setorcollection,c_artifact),
inference(resolve,[status(thm)],[c_13761,c_4829]) ).
cnf(c_12702,plain,
isa(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_setorcollection),
inference(resolve,[status(thm)],[c_1793,c_2208]) ).
cnf(c_13762,plain,
( ~ disjointwith(B,c_artifact)
| ~ isa(f_urlreferentfn(A),B) ),
inference(resolve,[status(thm)],[c_1471,c_2974]) ).
cnf(c_13753,plain,
~ isa(f_urlreferentfn(A),c_setorcollection),
inference(resolve,[status(thm)],[c_13762,c_9207]) ).
cnf(c_13754,plain,
$false,
inference(resolve,[status(thm)],[c_13753,c_12702]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR063+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n015.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Sun Sep 27 00:34:01 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.09/0.57 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.57 % Process 1101980 was started by sandbox2 on n015,
% 0.09/0.57 % Sun Sep 27 00:34:01 2026
% 0.09/0.57 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.73
% 0.12/0.73 % From the command line: assign(max_seconds, 300).
% 0.12/0.73
% 0.12/0.73 % SInE: 732 to sos, 399 to usable, of 1131 axioms (tolerance 2.00, depth 0 fixpoint).
% 9.32/2.14
% 9.32/2.14 % given #500 (F,wt=11): 2823 -disjointwith(A,c_tptpcol_16_7738) | -genls(c_tptpcol_16_7738,A). [resolve(2819,a,1956,c)].
% 9.32/2.14
% 9.32/2.14 % given #1000 (W,wt=8): 3239 subsetof(c_tptpcol_15_40430,c_tptpcol_15_40430). [ur(1509,a,2316,a)].
% 9.32/2.14
% 9.32/2.14 % given #1500 (F,wt=7): 4706 -inanimateobject(c_inanimateobject). [resolve(4512,a,3850,a)].
% 9.32/2.14
% 9.32/2.14 % given #2000 (T,wt=8): 3739 most(c_tptpcol_15_40430,c_tptpcol_12_40420). [ur(1264,a,3192,a)].
% 9.32/2.14
% 9.32/2.14 % given #2500 (F,wt=7): 5919 -intangibleindividual(c_tptpcol_16_130924). [resolve(1447,b,4412,a)].
% 9.32/2.14
% 9.32/2.14 % given #3000 (T,wt=8): 4965 genls(c_tptpcol_5_69635,c_tptpcol_5_69635). [ur(1948,a,4885,a)].
% 9.32/2.14
% 9.32/2.14 % given #3500 (F,wt=7): 7245 -tptpcol_0_0(c_tptpcol_3_98305). [resolve(1526,b,4334,a)].
% 9.32/2.14
% 9.32/2.14 % given #4000 (T,wt=8): 6629 subsetof(c_tptpcol_9_118019,c_tptpcol_8_117763). [ur(1509,a,1488,a)].
% 9.32/2.14
% 9.32/2.14 % given #4500 (A,wt=710): 1677 -objectfoundinlocation(A,B) | spatialthing_nonsituational(A) # tptp_name(ax1_695) # sine_depth(8). [clausify(278)].
% 9.32/2.14
% 9.32/2.14 % given #5000 (T,wt=8): 7907 genls(c_tptpcol_6_18436,c_tptpcol_3_16386). [ur(1947,a,1461,a,b,5311,a)].
% 9.32/2.14
% 9.32/2.14 % given #5500 (W,wt=7): 9748 -aspatialinformationstore(c_tptpcol_6_71683). [resolve(8424,a,1485,b)].
% 9.32/2.14
% 9.32/2.14 % SZS status Theorem for theBenchmark
% 9.32/2.14
% 9.32/2.14 % Proof 1 at 1.00 (+ 0.30) seconds.
% 9.32/2.14 % Length of proof is 46.
% 9.32/2.14 % Level of proof is 7.
% 9.32/2.14 % Maximum clause weight is 708.000.
% 9.32/2.14 % Given clauses 5959.
% 9.32/2.14
% 9.32/2.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------