%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR063+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:14:55 PM UTC 2026
% Result : Theorem 0.13s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR063+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 14:41:51 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.39 % Drodi V4.1.1
% 0.13/0.50 % Refutation found
% 0.13/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.50 fof(f3,axiom,(
% 0.13/0.50 (! [OBJ] :~ ( intangible(OBJ)& partiallytangible(OBJ) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f9,axiom,(
% 0.13/0.50 (! [OBJ] :( inanimateobject(OBJ)=> partiallytangible(OBJ) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f112,axiom,(
% 0.13/0.50 (! [OBJ] :( setorcollection(OBJ)=> mathematicalthing(OBJ) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f132,axiom,(
% 0.13/0.50 (! [OBJ] :( mathematicalorcomputationalthing(OBJ)=> intangible(OBJ) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f180,axiom,(
% 0.13/0.50 (! [OBJ] :( mathematicalthing(OBJ)=> mathematicalorcomputationalthing(OBJ) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f196,axiom,(
% 0.13/0.50 (! [OBJ] :( inanimateobject_nonnatural(OBJ)=> inanimateobject(OBJ) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f211,axiom,(
% 0.13/0.50 (! [OBJ] :( artifact(OBJ)=> inanimateobject_nonnatural(OBJ) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f221,axiom,(
% 0.13/0.50 (! [ARG1,ARG2] :( disjointwith(ARG1,ARG2)=> no(ARG1,ARG2) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f331,axiom,(
% 0.13/0.50 (! [ARG1,ARG2] :( no(ARG1,ARG2)=> few(ARG1,ARG2) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f435,axiom,(
% 0.13/0.50 (! [ARG1,ARG2] :( few(ARG1,ARG2)=> setorcollection(ARG2) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f494,axiom,(
% 0.13/0.50 (! [OBJ] :( computerdataartifact(OBJ)=> artifact(OBJ) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f1085,axiom,(
% 0.13/0.50 (! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f1120,axiom,(
% 0.13/0.50 (! [X,Y] :( disjointwith(X,Y)=> disjointwith(Y,X) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f1132,conjecture,(
% 0.13/0.50 ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f1133,negated_conjecture,(
% 0.13/0.50 ~(~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) )),
% 0.13/0.50 inference(negated_conjecture,[status(cth)],[f1132])).
% 0.13/0.50 fof(f1136,plain,(
% 0.13/0.50 ![OBJ]: (~intangible(OBJ)|~partiallytangible(OBJ))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.13/0.50 fof(f1137,plain,(
% 0.13/0.50 ![X0]: (~intangible(X0)|~partiallytangible(X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1136])).
% 0.13/0.50 fof(f1145,plain,(
% 0.13/0.50 ![OBJ]: (~inanimateobject(OBJ)|partiallytangible(OBJ))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.13/0.50 fof(f1146,plain,(
% 0.13/0.50 ![X0]: (~inanimateobject(X0)|partiallytangible(X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1145])).
% 0.13/0.50 fof(f1296,plain,(
% 0.13/0.50 ![OBJ]: (~setorcollection(OBJ)|mathematicalthing(OBJ))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f112])).
% 0.13/0.50 fof(f1297,plain,(
% 0.13/0.50 ![X0]: (~setorcollection(X0)|mathematicalthing(X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1296])).
% 0.13/0.50 fof(f1326,plain,(
% 0.13/0.50 ![OBJ]: (~mathematicalorcomputationalthing(OBJ)|intangible(OBJ))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f132])).
% 0.13/0.50 fof(f1327,plain,(
% 0.13/0.50 ![X0]: (~mathematicalorcomputationalthing(X0)|intangible(X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1326])).
% 0.13/0.50 fof(f1396,plain,(
% 0.13/0.50 ![OBJ]: (~mathematicalthing(OBJ)|mathematicalorcomputationalthing(OBJ))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f180])).
% 0.13/0.50 fof(f1397,plain,(
% 0.13/0.50 ![X0]: (~mathematicalthing(X0)|mathematicalorcomputationalthing(X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1396])).
% 0.13/0.50 fof(f1420,plain,(
% 0.13/0.50 ![OBJ]: (~inanimateobject_nonnatural(OBJ)|inanimateobject(OBJ))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f196])).
% 0.13/0.50 fof(f1421,plain,(
% 0.13/0.50 ![X0]: (~inanimateobject_nonnatural(X0)|inanimateobject(X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1420])).
% 0.13/0.50 fof(f1442,plain,(
% 0.13/0.50 ![OBJ]: (~artifact(OBJ)|inanimateobject_nonnatural(OBJ))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f211])).
% 0.13/0.50 fof(f1443,plain,(
% 0.13/0.50 ![X0]: (~artifact(X0)|inanimateobject_nonnatural(X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1442])).
% 0.13/0.50 fof(f1456,plain,(
% 0.13/0.50 ![ARG1,ARG2]: (~disjointwith(ARG1,ARG2)|no(ARG1,ARG2))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f221])).
% 0.13/0.50 fof(f1457,plain,(
% 0.13/0.50 ![X0,X1]: (~disjointwith(X0,X1)|no(X0,X1))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1456])).
% 0.13/0.50 fof(f1617,plain,(
% 0.13/0.50 ![ARG1,ARG2]: (~no(ARG1,ARG2)|few(ARG1,ARG2))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f331])).
% 0.13/0.50 fof(f1618,plain,(
% 0.13/0.50 ![X0,X1]: (~no(X0,X1)|few(X0,X1))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1617])).
% 0.13/0.50 fof(f1766,plain,(
% 0.13/0.50 ![ARG1,ARG2]: (~few(ARG1,ARG2)|setorcollection(ARG2))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f435])).
% 0.13/0.50 fof(f1767,plain,(
% 0.13/0.50 ![ARG2]: ((![ARG1]: ~few(ARG1,ARG2))|setorcollection(ARG2))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f1766])).
% 0.13/0.50 fof(f1768,plain,(
% 0.13/0.50 ![X0,X1]: (~few(X0,X1)|setorcollection(X1))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1767])).
% 0.13/0.50 fof(f1856,plain,(
% 0.13/0.50 ![OBJ]: (~computerdataartifact(OBJ)|artifact(OBJ))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f494])).
% 0.13/0.50 fof(f1857,plain,(
% 0.13/0.50 ![X0]: (~computerdataartifact(X0)|artifact(X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1856])).
% 0.13/0.50 fof(f3094,plain,(
% 0.13/0.50 ![X0]: (computerdataartifact(f_urlreferentfn(X0)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1085])).
% 0.13/0.50 fof(f3173,plain,(
% 0.13/0.50 ![X,Y]: (~disjointwith(X,Y)|disjointwith(Y,X))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f1120])).
% 0.13/0.50 fof(f3174,plain,(
% 0.13/0.50 ![X0,X1]: (~disjointwith(X0,X1)|disjointwith(X1,X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f3173])).
% 0.13/0.50 fof(f3204,plain,(
% 0.13/0.50 disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f1133])).
% 0.13/0.50 fof(f3214,plain,(
% 0.13/0.50 disjointwith(c_tptpcol_16_118949,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f3174,f3204])).
% 0.13/0.50 fof(f3225,plain,(
% 0.13/0.50 no(c_tptpcol_16_118949,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f3214,f1457])).
% 0.13/0.50 fof(f3852,plain,(
% 0.13/0.50 few(c_tptpcol_16_118949,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f1618,f3225])).
% 0.13/0.50 fof(f4306,plain,(
% 0.13/0.50 setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f1768,f3852])).
% 0.13/0.50 fof(f4313,plain,(
% 0.13/0.50 mathematicalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f4306,f1297])).
% 0.13/0.50 fof(f4335,plain,(
% 0.13/0.50 mathematicalorcomputationalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f4313,f1397])).
% 0.13/0.50 fof(f4369,plain,(
% 0.13/0.50 intangible(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f4335,f1327])).
% 0.13/0.50 fof(f4370,plain,(
% 0.13/0.50 ~partiallytangible(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f4369,f1137])).
% 0.13/0.50 fof(f4459,plain,(
% 0.13/0.50 ![X0]: (artifact(f_urlreferentfn(X0)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f1857,f3094])).
% 0.13/0.50 fof(f5027,plain,(
% 0.13/0.50 ![X0]: (inanimateobject_nonnatural(f_urlreferentfn(X0)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f4459,f1443])).
% 0.13/0.50 fof(f5041,plain,(
% 0.13/0.50 ![X0]: (inanimateobject(f_urlreferentfn(X0)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f5027,f1421])).
% 0.13/0.50 fof(f5218,plain,(
% 0.13/0.50 ![X0]: (partiallytangible(f_urlreferentfn(X0)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f5041,f1146])).
% 0.13/0.50 fof(f5239,plain,(
% 0.13/0.50 $false),
% 0.13/0.50 inference(backward_subsumption_resolution,[status(thm)],[f4370,f5218])).
% 0.13/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 1.57/1.72 % Elapsed time: 1.134762 seconds
% 1.57/1.72 % CPU time: 0.735585 seconds
% 1.57/1.72 % Total memory used: 113.267 MB
% 1.57/1.72 % Net memory used: 112.975 MB
%------------------------------------------------------------------------------