%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR201+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:15:44 PM UTC 2026
% Result : Theorem 132.73s 22.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR201+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/5.43 % Computer : n009.cluster.edu
% 0.17/5.43 % Model : x86_64 x86_64
% 0.17/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.43 % Memory : 8046.5625MB
% 0.17/5.43 % OS : Linux 6.8.0-71-generic
% 0.17/5.43 % CPULimit : 300
% 0.17/5.43 % WCLimit : 300
% 0.17/5.43 % DateTime : Mon Sep 21 15:17:02 UTC 2026
% 0.17/5.44 % CPUTime :
% 0.21/5.83 % Drodi V4.1.1
% 132.73/22.57 % Refutation found
% 132.73/22.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 132.73/22.57 % SZS output start CNFRefutation for theBenchmark
% 132.73/22.57 fof(f2,axiom,(
% 132.73/22.57 (! [X,Y,Z] :( ( p__d__subclass(X,Y)& p__d__subclass(Y,Z) )=> p__d__subclass(X,Z) ) )),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f3,axiom,(
% 132.73/22.57 (! [X,Y] :( ( p__d__subclass(X,Y)& p__d__subclass(Y,X) )=> X = Y ) )),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f4,axiom,(
% 132.73/22.57 (! [X,Y,Z] :( ( p__d__instance(X,Y)& p__d__subclass(Y,Z) )=> p__d__instance(X,Z) ) )),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f5,axiom,(
% 132.73/22.57 (! [CLASS1,CLASS2] :( p__d__disjoint(CLASS1,CLASS2)<=> (! [INST] :( ~ p__d__instance(INST,CLASS1)| ~ p__d__instance(INST,CLASS2) ) )) )),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f110,axiom,(
% 132.73/22.57 (! [CLASS] :( p__d__subclass(CLASS,c__Entity)=> (? [THING] : p__d__instance(THING,CLASS) )) )),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f112,axiom,(
% 132.73/22.57 p__d__subclass(c__Physical,c__Entity) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f233,axiom,(
% 132.73/22.57 p__d__subclass(c__Process,c__Physical) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f1582,axiom,(
% 132.73/22.57 p__d__subclass(c__BiologicalProcess,c__InternalChange) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f1585,axiom,(
% 132.73/22.57 p__d__subclass(c__PhysiologicProcess,c__BiologicalProcess) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f1591,axiom,(
% 132.73/22.57 p__d__subclass(c__OrganismProcess,c__PhysiologicProcess) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f1607,axiom,(
% 132.73/22.57 p__d__subclass(c__Replication,c__OrganismProcess) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f1610,axiom,(
% 132.73/22.57 p__d__subclass(c__SexualReproduction,c__Replication) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f1611,axiom,(
% 132.73/22.57 p__d__disjoint(c__SexualReproduction,c__AsexualReproduction) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f1613,axiom,(
% 132.73/22.57 p__d__subclass(c__AsexualReproduction,c__Replication) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f1859,axiom,(
% 132.73/22.57 p__d__subclass(c__InternalChange,c__Process) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f7433,conjecture,(
% 132.73/22.57 ~ p__d__subclass(c__Replication,c__SexualReproduction) ),
% 132.73/22.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 132.73/22.57 fof(f7434,negated_conjecture,(
% 132.73/22.57 ~(~ p__d__subclass(c__Replication,c__SexualReproduction) )),
% 132.73/22.57 inference(negated_conjecture,[status(cth)],[f7433])).
% 132.73/22.57 fof(f7436,plain,(
% 132.73/22.57 ![X,Y,Z]: ((~p__d__subclass(X,Y)|~p__d__subclass(Y,Z))|p__d__subclass(X,Z))),
% 132.73/22.57 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 132.73/22.57 fof(f7437,plain,(
% 132.73/22.57 ![X,Z]: ((![Y]: (~p__d__subclass(X,Y)|~p__d__subclass(Y,Z)))|p__d__subclass(X,Z))),
% 132.73/22.57 inference(miniscoping,[status(thm)],[f7436])).
% 132.73/22.57 fof(f7438,plain,(
% 132.73/22.57 ![X0,X1,X2]: (~p__d__subclass(X0,X1)|~p__d__subclass(X1,X2)|p__d__subclass(X0,X2))),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f7437])).
% 132.73/22.57 fof(f7439,plain,(
% 132.73/22.57 ![X,Y]: ((~p__d__subclass(X,Y)|~p__d__subclass(Y,X))|X=Y)),
% 132.73/22.57 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 132.73/22.57 fof(f7440,plain,(
% 132.73/22.57 ![X0,X1]: (~p__d__subclass(X0,X1)|~p__d__subclass(X1,X0)|X0=X1)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f7439])).
% 132.73/22.57 fof(f7441,plain,(
% 132.73/22.57 ![X,Y,Z]: ((~p__d__instance(X,Y)|~p__d__subclass(Y,Z))|p__d__instance(X,Z))),
% 132.73/22.57 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 132.73/22.57 fof(f7442,plain,(
% 132.73/22.57 ![X,Z]: ((![Y]: (~p__d__instance(X,Y)|~p__d__subclass(Y,Z)))|p__d__instance(X,Z))),
% 132.73/22.57 inference(miniscoping,[status(thm)],[f7441])).
% 132.73/22.57 fof(f7443,plain,(
% 132.73/22.57 ![X0,X1,X2]: (~p__d__instance(X0,X1)|~p__d__subclass(X1,X2)|p__d__instance(X0,X2))),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f7442])).
% 132.73/22.57 fof(f7444,plain,(
% 132.73/22.57 ![CLASS1,CLASS2]: ((~p__d__disjoint(CLASS1,CLASS2)|(![INST]: (~p__d__instance(INST,CLASS1)|~p__d__instance(INST,CLASS2))))&(p__d__disjoint(CLASS1,CLASS2)|(?[INST]: (p__d__instance(INST,CLASS1)&p__d__instance(INST,CLASS2)))))),
% 132.73/22.57 inference(NNF_transformation,[status(thm)],[f5])).
% 132.73/22.57 fof(f7445,plain,(
% 132.73/22.57 (![CLASS1,CLASS2]: (~p__d__disjoint(CLASS1,CLASS2)|(![INST]: (~p__d__instance(INST,CLASS1)|~p__d__instance(INST,CLASS2)))))&(![CLASS1,CLASS2]: (p__d__disjoint(CLASS1,CLASS2)|(?[INST]: (p__d__instance(INST,CLASS1)&p__d__instance(INST,CLASS2)))))),
% 132.73/22.57 inference(miniscoping,[status(thm)],[f7444])).
% 132.73/22.57 fof(f7446,plain,(
% 132.73/22.57 (![CLASS1,CLASS2]: (~p__d__disjoint(CLASS1,CLASS2)|(![INST]: (~p__d__instance(INST,CLASS1)|~p__d__instance(INST,CLASS2)))))&(![CLASS1,CLASS2]: (p__d__disjoint(CLASS1,CLASS2)|(p__d__instance(sK0_skl(CLASS2,CLASS1),CLASS1)&p__d__instance(sK0_skl(CLASS2,CLASS1),CLASS2))))),
% 132.73/22.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(INST,sK0_skl(CLASS2,CLASS1))],[f7445])).
% 132.73/22.57 fof(f7447,plain,(
% 132.73/22.57 ![X0,X1,X2]: (~p__d__disjoint(X0,X1)|~p__d__instance(X2,X0)|~p__d__instance(X2,X1))),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f7446])).
% 132.73/22.57 fof(f7718,plain,(
% 132.73/22.57 ![CLASS]: (~p__d__subclass(CLASS,c__Entity)|(?[THING]: p__d__instance(THING,CLASS)))),
% 132.73/22.57 inference(pre_NNF_transformation,[status(thm)],[f110])).
% 132.73/22.57 fof(f7719,plain,(
% 132.73/22.57 ![CLASS]: (~p__d__subclass(CLASS,c__Entity)|p__d__instance(sK13_skl(CLASS),CLASS))),
% 132.73/22.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(THING,sK13_skl(CLASS))],[f7718])).
% 132.73/22.57 fof(f7720,plain,(
% 132.73/22.57 ![X0]: (~p__d__subclass(X0,c__Entity)|p__d__instance(sK13_skl(X0),X0))),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f7719])).
% 132.73/22.57 fof(f7725,plain,(
% 132.73/22.57 p__d__subclass(c__Physical,c__Entity)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f112])).
% 132.73/22.57 fof(f7942,plain,(
% 132.73/22.57 p__d__subclass(c__Process,c__Physical)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f233])).
% 132.73/22.57 fof(f10070,plain,(
% 132.73/22.57 p__d__subclass(c__BiologicalProcess,c__InternalChange)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f1582])).
% 132.73/22.57 fof(f10078,plain,(
% 132.73/22.57 p__d__subclass(c__PhysiologicProcess,c__BiologicalProcess)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f1585])).
% 132.73/22.57 fof(f10088,plain,(
% 132.73/22.57 p__d__subclass(c__OrganismProcess,c__PhysiologicProcess)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f1591])).
% 132.73/22.57 fof(f10119,plain,(
% 132.73/22.57 p__d__subclass(c__Replication,c__OrganismProcess)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f1607])).
% 132.73/22.57 fof(f10127,plain,(
% 132.73/22.57 p__d__subclass(c__SexualReproduction,c__Replication)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f1610])).
% 132.73/22.57 fof(f10128,plain,(
% 132.73/22.57 p__d__disjoint(c__SexualReproduction,c__AsexualReproduction)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f1611])).
% 132.73/22.57 fof(f10136,plain,(
% 132.73/22.57 p__d__subclass(c__AsexualReproduction,c__Replication)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f1613])).
% 132.73/22.57 fof(f10686,plain,(
% 132.73/22.57 p__d__subclass(c__InternalChange,c__Process)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f1859])).
% 132.73/22.57 fof(f23432,plain,(
% 132.73/22.57 p__d__subclass(c__Replication,c__SexualReproduction)),
% 132.73/22.57 inference(cnf_transformation,[status(thm)],[f7434])).
% 132.73/22.57 fof(f23605,plain,(
% 132.73/22.57 ![X0]: (~p__d__subclass(c__OrganismProcess,X0)|p__d__subclass(c__Replication,X0))),
% 132.73/22.57 inference(resolution,[status(thm)],[f7438,f10119])).
% 132.73/22.57 fof(f23613,plain,(
% 132.73/22.57 ~p__d__subclass(c__Replication,c__SexualReproduction)|c__SexualReproduction=c__Replication),
% 132.73/22.57 inference(resolution,[status(thm)],[f7440,f10127])).
% 132.73/22.57 fof(f23622,plain,(
% 132.73/22.57 c__SexualReproduction=c__Replication),
% 132.73/22.57 inference(forward_subsumption_resolution,[status(thm)],[f23613,f23432])).
% 132.73/22.57 fof(f23633,plain,(
% 132.73/22.57 ![X0]: (~p__d__subclass(c__OrganismProcess,X0)|p__d__subclass(c__SexualReproduction,X0))),
% 132.73/22.57 inference(forward_demodulation,[status(thm)],[f23622,f23605])).
% 132.73/22.57 fof(f24075,plain,(
% 132.73/22.57 ![X0]: (~p__d__subclass(X0,c__Physical)|p__d__subclass(X0,c__Entity))),
% 132.73/22.57 inference(resolution,[status(thm)],[f7725,f7438])).
% 132.73/22.57 fof(f25529,plain,(
% 132.73/22.57 ![X0]: (~p__d__subclass(X0,c__Process)|p__d__subclass(X0,c__Physical))),
% 132.73/22.57 inference(resolution,[status(thm)],[f7942,f7438])).
% 132.73/22.57 fof(f48636,plain,(
% 132.73/22.57 p__d__subclass(c__SexualReproduction,c__PhysiologicProcess)),
% 132.73/22.57 inference(resolution,[status(thm)],[f10088,f23633])).
% 132.73/22.57 fof(f49036,plain,(
% 132.73/22.57 ![X0]: (~p__d__subclass(c__PhysiologicProcess,X0)|p__d__subclass(c__SexualReproduction,X0))),
% 79.59/22.69 inference(resolution,[status(thm)],[f48636,f7438])).
% 79.59/22.69 fof(f49301,plain,(
% 79.59/22.69 p__d__subclass(c__AsexualReproduction,c__SexualReproduction)),
% 79.59/22.69 inference(forward_demodulation,[status(thm)],[f23622,f10136])).
% 79.59/22.69 fof(f49310,plain,(
% 79.59/22.69 ![X0]: (~p__d__instance(X0,c__AsexualReproduction)|p__d__instance(X0,c__SexualReproduction))),
% 79.59/22.69 inference(resolution,[status(thm)],[f49301,f7443])).
% 79.59/22.69 fof(f49314,plain,(
% 79.59/22.69 ![X0]: (~p__d__subclass(c__SexualReproduction,X0)|p__d__subclass(c__AsexualReproduction,X0))),
% 79.59/22.69 inference(resolution,[status(thm)],[f49301,f7438])).
% 79.59/22.69 fof(f52641,plain,(
% 79.59/22.69 p__d__subclass(c__SexualReproduction,c__BiologicalProcess)),
% 79.59/22.69 inference(resolution,[status(thm)],[f49036,f10078])).
% 79.59/22.69 fof(f52654,plain,(
% 79.59/22.69 ![X0]: (~p__d__subclass(c__BiologicalProcess,X0)|p__d__subclass(c__SexualReproduction,X0))),
% 79.59/22.69 inference(resolution,[status(thm)],[f52641,f7438])).
% 79.59/22.69 fof(f62418,plain,(
% 79.59/22.69 p__d__subclass(c__SexualReproduction,c__InternalChange)),
% 79.59/22.69 inference(resolution,[status(thm)],[f52654,f10070])).
% 79.59/22.69 fof(f62420,plain,(
% 79.59/22.69 p__d__subclass(c__AsexualReproduction,c__InternalChange)),
% 79.59/22.69 inference(resolution,[status(thm)],[f62418,f49314])).
% 79.59/22.69 fof(f62444,plain,(
% 79.59/22.69 ![X0]: (~p__d__subclass(c__InternalChange,X0)|p__d__subclass(c__AsexualReproduction,X0))),
% 79.59/22.69 inference(resolution,[status(thm)],[f62420,f7438])).
% 79.59/22.69 fof(f64814,plain,(
% 79.59/22.69 p__d__subclass(c__AsexualReproduction,c__Process)),
% 79.59/22.69 inference(resolution,[status(thm)],[f10686,f62444])).
% 79.59/22.69 fof(f64936,plain,(
% 79.59/22.69 p__d__subclass(c__AsexualReproduction,c__Physical)),
% 79.59/22.69 inference(resolution,[status(thm)],[f64814,f25529])).
% 79.59/22.69 fof(f64977,plain,(
% 79.59/22.69 p__d__subclass(c__AsexualReproduction,c__Entity)),
% 79.59/22.69 inference(resolution,[status(thm)],[f64936,f24075])).
% 79.59/22.69 fof(f66562,plain,(
% 79.59/22.69 p__d__instance(sK13_skl(c__AsexualReproduction),c__AsexualReproduction)),
% 79.59/22.69 inference(resolution,[status(thm)],[f64977,f7720])).
% 79.59/22.69 fof(f67037,plain,(
% 79.59/22.69 p__d__instance(sK13_skl(c__AsexualReproduction),c__SexualReproduction)),
% 79.59/22.69 inference(resolution,[status(thm)],[f66562,f49310])).
% 79.59/22.69 fof(f67058,plain,(
% 79.59/22.69 ![X0]: (~p__d__disjoint(X0,c__AsexualReproduction)|~p__d__instance(sK13_skl(c__AsexualReproduction),X0))),
% 79.59/22.69 inference(resolution,[status(thm)],[f66562,f7447])).
% 79.59/22.69 fof(f99767,plain,(
% 79.59/22.69 ~p__d__disjoint(c__SexualReproduction,c__AsexualReproduction)),
% 79.59/22.69 inference(resolution,[status(thm)],[f67058,f67037])).
% 79.59/22.69 fof(f99774,plain,(
% 79.59/22.69 $false),
% 79.59/22.69 inference(forward_subsumption_resolution,[status(thm)],[f99767,f10128])).
% 79.59/22.69 % SZS output end CNFRefutation for theBenchmark.p
% 4.52/22.72 % Elapsed time: 17.252366 seconds
% 4.52/22.72 % CPU time: 133.523156 seconds
% 4.52/22.72 % Total memory used: 1.019 GB
% 4.52/22.72 % Net memory used: 966.702 MB
%------------------------------------------------------------------------------