%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR063+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 : Thu Sep 24 12:13:19 PM UTC 2026
% Result : Theorem 0.12s 10.48s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 14
% Syntax : Number of formulae : 55 ( 15 unt; 0 def)
% Number of atoms : 95 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 81 ( 41 ~; 28 |; 1 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 68 ( 68 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [OBJ] :
~ ( partiallytangible(OBJ)
& intangible(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [OBJ] :
( inanimateobject(OBJ)
=> partiallytangible(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,axiom,
! [OBJ] :
( setorcollection(OBJ)
=> mathematicalthing(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,axiom,
! [OBJ] :
( mathematicalorcomputationalthing(OBJ)
=> intangible(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f180,axiom,
! [OBJ] :
( mathematicalthing(OBJ)
=> mathematicalorcomputationalthing(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,axiom,
! [OBJ] :
( inanimateobject_nonnatural(OBJ)
=> inanimateobject(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f211,axiom,
! [OBJ] :
( artifact(OBJ)
=> inanimateobject_nonnatural(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f221,axiom,
! [ARG1,ARG2] :
( disjointwith(ARG1,ARG2)
=> no(ARG1,ARG2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f331,axiom,
! [ARG1,ARG2] :
( no(ARG1,ARG2)
=> few(ARG1,ARG2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f435,axiom,
! [ARG1,ARG2] :
( few(ARG1,ARG2)
=> setorcollection(ARG2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f494,axiom,
! [OBJ] :
( computerdataartifact(OBJ)
=> artifact(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1085,axiom,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1120,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1132,conjecture,
~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1133,negated_conjecture,
~ ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(negated_conjecture,[status(cth)],[f1132]) ).
fof(f1136,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f1137,plain,
! [X0] :
( ~ partiallytangible(X0)
| ~ intangible(X0) ),
inference(cnf_transformation,[status(thm)],[f1136]) ).
fof(f1145,plain,
! [OBJ] :
( partiallytangible(OBJ)
| ~ inanimateobject(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f1146,plain,
! [X0] :
( partiallytangible(X0)
| ~ inanimateobject(X0) ),
inference(cnf_transformation,[status(thm)],[f1145]) ).
fof(f1296,plain,
! [OBJ] :
( mathematicalthing(OBJ)
| ~ setorcollection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f112]) ).
fof(f1297,plain,
! [X0] :
( mathematicalthing(X0)
| ~ setorcollection(X0) ),
inference(cnf_transformation,[status(thm)],[f1296]) ).
fof(f1326,plain,
! [OBJ] :
( intangible(OBJ)
| ~ mathematicalorcomputationalthing(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f132]) ).
fof(f1327,plain,
! [X0] :
( intangible(X0)
| ~ mathematicalorcomputationalthing(X0) ),
inference(cnf_transformation,[status(thm)],[f1326]) ).
fof(f1396,plain,
! [OBJ] :
( mathematicalorcomputationalthing(OBJ)
| ~ mathematicalthing(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f180]) ).
fof(f1397,plain,
! [X0] :
( mathematicalorcomputationalthing(X0)
| ~ mathematicalthing(X0) ),
inference(cnf_transformation,[status(thm)],[f1396]) ).
fof(f1420,plain,
! [OBJ] :
( inanimateobject(OBJ)
| ~ inanimateobject_nonnatural(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f196]) ).
fof(f1421,plain,
! [X0] :
( inanimateobject(X0)
| ~ inanimateobject_nonnatural(X0) ),
inference(cnf_transformation,[status(thm)],[f1420]) ).
fof(f1442,plain,
! [OBJ] :
( inanimateobject_nonnatural(OBJ)
| ~ artifact(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f211]) ).
fof(f1443,plain,
! [X0] :
( inanimateobject_nonnatural(X0)
| ~ artifact(X0) ),
inference(cnf_transformation,[status(thm)],[f1442]) ).
fof(f1456,plain,
! [ARG1,ARG2] :
( no(ARG1,ARG2)
| ~ disjointwith(ARG1,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f221]) ).
fof(f1457,plain,
! [X0,X1] :
( no(X0,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1456]) ).
fof(f1617,plain,
! [ARG1,ARG2] :
( few(ARG1,ARG2)
| ~ no(ARG1,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f331]) ).
fof(f1618,plain,
! [X0,X1] :
( few(X0,X1)
| ~ no(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1617]) ).
fof(f1766,plain,
! [ARG1,ARG2] :
( setorcollection(ARG2)
| ~ few(ARG1,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f435]) ).
fof(f1767,plain,
! [ARG2] :
( setorcollection(ARG2)
| ! [ARG1] : ~ few(ARG1,ARG2) ),
inference(miniscoping,[status(thm)],[f1766]) ).
fof(f1768,plain,
! [X0,X1] :
( setorcollection(X1)
| ~ few(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1767]) ).
fof(f1856,plain,
! [OBJ] :
( artifact(OBJ)
| ~ computerdataartifact(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f494]) ).
fof(f1857,plain,
! [X0] :
( artifact(X0)
| ~ computerdataartifact(X0) ),
inference(cnf_transformation,[status(thm)],[f1856]) ).
fof(f3094,plain,
! [X0] : computerdataartifact(f_urlreferentfn(X0)),
inference(cnf_transformation,[status(thm)],[f1085]) ).
fof(f3173,plain,
! [X,Y] :
( disjointwith(Y,X)
| ~ disjointwith(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1120]) ).
fof(f3174,plain,
! [X0,X1] :
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3173]) ).
fof(f3204,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(cnf_transformation,[status(thm)],[f1133]) ).
fof(f3309,plain,
! [X0] :
( intangible(X0)
| ~ mathematicalthing(X0) ),
inference(resolution,[status(thm)],[f1397,f1327]) ).
fof(f4937,plain,
! [X0] :
( inanimateobject_nonnatural(X0)
| ~ computerdataartifact(X0) ),
inference(resolution,[status(thm)],[f1857,f1443]) ).
fof(f5018,plain,
! [X0] :
( inanimateobject(X0)
| ~ computerdataartifact(X0) ),
inference(resolution,[status(thm)],[f4937,f1421]) ).
fof(f5922,plain,
! [X0] : inanimateobject(f_urlreferentfn(X0)),
inference(resolution,[status(thm)],[f5018,f3094]) ).
fof(f5923,plain,
! [X0] : partiallytangible(f_urlreferentfn(X0)),
inference(resolution,[status(thm)],[f5922,f1146]) ).
fof(f5927,plain,
! [X0] : ~ intangible(f_urlreferentfn(X0)),
inference(resolution,[status(thm)],[f5923,f1137]) ).
fof(f5929,plain,
! [X0] : ~ mathematicalthing(f_urlreferentfn(X0)),
inference(resolution,[status(thm)],[f5927,f3309]) ).
fof(f5930,plain,
! [X0] : ~ setorcollection(f_urlreferentfn(X0)),
inference(resolution,[status(thm)],[f5929,f1297]) ).
fof(f5932,plain,
! [X0,X1] : ~ few(X0,f_urlreferentfn(X1)),
inference(resolution,[status(thm)],[f5930,f1768]) ).
fof(f5951,plain,
! [X0,X1] : ~ no(X0,f_urlreferentfn(X1)),
inference(resolution,[status(thm)],[f5932,f1618]) ).
fof(f5969,plain,
! [X0,X1] : ~ disjointwith(X0,f_urlreferentfn(X1)),
inference(resolution,[status(thm)],[f5951,f1457]) ).
fof(f6118,plain,
! [X0,X1] : ~ disjointwith(f_urlreferentfn(X0),X1),
inference(resolution,[status(thm)],[f5969,f3174]) ).
fof(f6120,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f3204,f6118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR063+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/10.36 % Computer : n016.cluster.edu
% 0.07/10.36 % Model : x86_64 x86_64
% 0.07/10.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/10.36 % Memory : 8046.5625MB
% 0.07/10.36 % OS : Linux 6.8.0-71-generic
% 0.07/10.36 % CPULimit : 300
% 0.07/10.36 % WCLimit : 300
% 0.07/10.36 % DateTime : Mon Sep 21 14:46:50 UTC 2026
% 0.07/10.37 % CPUTime :
% 0.12/10.40 % Drodi V4.1.1
% 0.12/10.48 % Refutation found
% 0.12/10.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/10.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.96/11.72 % Elapsed time: 1.134102 seconds
% 1.96/11.72 % CPU time: 0.643247 seconds
% 1.96/11.72 % Total memory used: 108.470 MB
% 1.96/11.72 % Net memory used: 107.895 MB
%------------------------------------------------------------------------------