%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR063+3 : 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 : n009.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:56 PM UTC 2026
% Result : Theorem 0.41s 1.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR063+3 : 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.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % 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:43 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.22/0.53 % Drodi V4.1.1
% 0.41/1.06 % Refutation found
% 0.41/1.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.41/1.06 % SZS output start CNFRefutation for theBenchmark
% 0.41/1.06 fof(f23,axiom,(
% 0.41/1.06 (! [ARG1,ARG2] :( no(ARG1,ARG2)=> few(ARG1,ARG2) ) )),
% 0.41/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/1.06 fof(f220,axiom,(
% 0.41/1.06 (! [OBJ] :~ ( individual(OBJ)& setorcollection(OBJ) ) )),
% 0.41/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/1.06 fof(f374,axiom,(
% 0.41/1.06 (! [ARG1,ARG2] :( disjointwith(ARG1,ARG2)=> no(ARG1,ARG2) ) )),
% 0.41/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/1.06 fof(f2149,axiom,(
% 0.41/1.06 (! [ARG1,ARG2] :( few(ARG1,ARG2)=> setorcollection(ARG2) ) )),
% 0.41/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/1.06 fof(f2866,axiom,(
% 0.41/1.06 individual(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) ),
% 0.41/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/1.06 fof(f7584,axiom,(
% 0.41/1.06 (! [X,Y] :( disjointwith(X,Y)=> disjointwith(Y,X) ) )),
% 0.41/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/1.06 fof(f8006,conjecture,(
% 0.41/1.06 ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) ),
% 0.41/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/1.06 fof(f8007,negated_conjecture,(
% 0.41/1.06 ~(~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) )),
% 0.41/1.06 inference(negated_conjecture,[status(cth)],[f8006])).
% 0.41/1.06 fof(f8035,plain,(
% 0.41/1.06 ![ARG1,ARG2]: (~no(ARG1,ARG2)|few(ARG1,ARG2))),
% 0.41/1.06 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.41/1.06 fof(f8036,plain,(
% 0.41/1.06 ![X0,X1]: (~no(X0,X1)|few(X0,X1))),
% 0.41/1.06 inference(cnf_transformation,[status(thm)],[f8035])).
% 0.41/1.06 fof(f8298,plain,(
% 0.41/1.06 ![OBJ]: (~individual(OBJ)|~setorcollection(OBJ))),
% 0.41/1.06 inference(pre_NNF_transformation,[status(thm)],[f220])).
% 0.41/1.06 fof(f8299,plain,(
% 0.41/1.06 ![X0]: (~individual(X0)|~setorcollection(X0))),
% 0.41/1.06 inference(cnf_transformation,[status(thm)],[f8298])).
% 0.41/1.06 fof(f8511,plain,(
% 0.41/1.06 ![ARG1,ARG2]: (~disjointwith(ARG1,ARG2)|no(ARG1,ARG2))),
% 0.41/1.06 inference(pre_NNF_transformation,[status(thm)],[f374])).
% 0.41/1.06 fof(f8512,plain,(
% 0.41/1.06 ![X0,X1]: (~disjointwith(X0,X1)|no(X0,X1))),
% 0.41/1.06 inference(cnf_transformation,[status(thm)],[f8511])).
% 0.41/1.06 fof(f11023,plain,(
% 0.41/1.06 ![ARG1,ARG2]: (~few(ARG1,ARG2)|setorcollection(ARG2))),
% 0.41/1.06 inference(pre_NNF_transformation,[status(thm)],[f2149])).
% 0.41/1.06 fof(f11024,plain,(
% 0.41/1.06 ![ARG2]: ((![ARG1]: ~few(ARG1,ARG2))|setorcollection(ARG2))),
% 0.41/1.06 inference(miniscoping,[status(thm)],[f11023])).
% 0.41/1.06 fof(f11025,plain,(
% 0.41/1.06 ![X0,X1]: (~few(X0,X1)|setorcollection(X1))),
% 0.41/1.06 inference(cnf_transformation,[status(thm)],[f11024])).
% 0.41/1.06 fof(f12014,plain,(
% 0.41/1.06 individual(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.41/1.06 inference(cnf_transformation,[status(thm)],[f2866])).
% 0.41/1.06 fof(f20546,plain,(
% 0.41/1.06 ![X,Y]: (~disjointwith(X,Y)|disjointwith(Y,X))),
% 0.41/1.06 inference(pre_NNF_transformation,[status(thm)],[f7584])).
% 0.41/1.06 fof(f20547,plain,(
% 0.41/1.06 ![X0,X1]: (~disjointwith(X0,X1)|disjointwith(X1,X0))),
% 0.41/1.06 inference(cnf_transformation,[status(thm)],[f20546])).
% 0.41/1.06 fof(f21391,plain,(
% 0.41/1.06 disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949)),
% 0.41/1.06 inference(cnf_transformation,[status(thm)],[f8007])).
% 0.41/1.06 fof(f21400,plain,(
% 0.41/1.06 disjointwith(c_tptpcol_16_118949,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.41/1.06 inference(resolution,[status(thm)],[f20547,f21391])).
% 0.41/1.06 fof(f21671,plain,(
% 0.41/1.06 no(c_tptpcol_16_118949,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.41/1.06 inference(resolution,[status(thm)],[f8512,f21400])).
% 0.41/1.06 fof(f21682,plain,(
% 0.41/1.06 few(c_tptpcol_16_118949,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.41/1.06 inference(resolution,[status(thm)],[f21671,f8036])).
% 0.41/1.06 fof(f28914,plain,(
% 0.41/1.06 setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.41/1.06 inference(resolution,[status(thm)],[f11025,f21682])).
% 0.41/1.06 fof(f28925,plain,(
% 0.41/1.06 ~individual(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),
% 0.41/1.14 inference(resolution,[status(thm)],[f28914,f8299])).
% 0.41/1.14 fof(f28926,plain,(
% 0.41/1.14 $false),
% 0.41/1.14 inference(forward_subsumption_resolution,[status(thm)],[f28925,f12014])).
% 0.41/1.14 % SZS output end CNFRefutation for theBenchmark.p
% 299.31/300.00
% 299.31/300.00 % SZS status Unknown for theBenchmark.p: SIGTERM
%------------------------------------------------------------------------------