%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR174+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:15:42 PM UTC 2026
% Result : Theorem 8.78s 7.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR174+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/5.50 % Computer : n016.cluster.edu
% 0.19/5.50 % Model : x86_64 x86_64
% 0.19/5.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.50 % Memory : 8046.5625MB
% 0.19/5.50 % OS : Linux 6.8.0-71-generic
% 0.19/5.50 % CPULimit : 300
% 0.19/5.50 % WCLimit : 300
% 0.19/5.50 % DateTime : Mon Sep 21 15:19:29 UTC 2026
% 0.19/5.50 % CPUTime :
% 0.23/5.91 % Drodi V4.1.1
% 8.78/7.03 % Refutation found
% 8.78/7.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.78/7.03 % SZS output start CNFRefutation for theBenchmark
% 8.78/7.03 fof(f2,axiom,(
% 8.78/7.03 (! [X,Y,Z] :( ( p__d__subclass(X,Y)& p__d__subclass(Y,Z) )=> p__d__subclass(X,Z) ) )),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f4,axiom,(
% 8.78/7.03 (! [X,Y,Z] :( ( p__d__instance(X,Y)& p__d__subclass(Y,Z) )=> p__d__instance(X,Z) ) )),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f110,axiom,(
% 8.78/7.03 (! [CLASS] :( p__d__subclass(CLASS,c__Entity)=> (? [THING] : p__d__instance(THING,CLASS) )) )),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f112,axiom,(
% 8.78/7.03 p__d__subclass(c__Physical,c__Entity) ),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f191,axiom,(
% 8.78/7.03 p__d__subclass(c__ContentBearingProcess,c__Process) ),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f233,axiom,(
% 8.78/7.03 p__d__subclass(c__Process,c__Physical) ),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f1694,axiom,(
% 8.78/7.03 p__d__subclass(c__Speaking,c__LinguisticCommunication) ),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f1695,axiom,(
% 8.78/7.03 p__d__subclass(c__Speaking,c__Vocalizing) ),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f1901,axiom,(
% 8.78/7.03 p__d__subclass(c__Communication,c__ContentBearingProcess) ),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f1914,axiom,(
% 8.78/7.03 p__d__subclass(c__LinguisticCommunication,c__Communication) ),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f7433,conjecture,(
% 8.78/7.03 (? [X,Y] :( p__d__instance(Y,c__Speaking)& p__d__instance(X,c__Vocalizing)& X = Y ) )),
% 8.78/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.78/7.03 fof(f7434,negated_conjecture,(
% 8.78/7.03 ~((? [X,Y] :( p__d__instance(Y,c__Speaking)& p__d__instance(X,c__Vocalizing)& X = Y ) ))),
% 8.78/7.03 inference(negated_conjecture,[status(cth)],[f7433])).
% 8.78/7.03 fof(f7436,plain,(
% 8.78/7.03 ![X,Y,Z]: ((~p__d__subclass(X,Y)|~p__d__subclass(Y,Z))|p__d__subclass(X,Z))),
% 8.78/7.03 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 8.78/7.03 fof(f7437,plain,(
% 8.78/7.03 ![X,Z]: ((![Y]: (~p__d__subclass(X,Y)|~p__d__subclass(Y,Z)))|p__d__subclass(X,Z))),
% 8.78/7.03 inference(miniscoping,[status(thm)],[f7436])).
% 8.78/7.03 fof(f7438,plain,(
% 8.78/7.03 ![X0,X1,X2]: (~p__d__subclass(X0,X1)|~p__d__subclass(X1,X2)|p__d__subclass(X0,X2))),
% 8.78/7.03 inference(cnf_transformation,[status(thm)],[f7437])).
% 8.78/7.03 fof(f7441,plain,(
% 8.78/7.03 ![X,Y,Z]: ((~p__d__instance(X,Y)|~p__d__subclass(Y,Z))|p__d__instance(X,Z))),
% 8.78/7.03 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 8.78/7.03 fof(f7442,plain,(
% 8.78/7.03 ![X,Z]: ((![Y]: (~p__d__instance(X,Y)|~p__d__subclass(Y,Z)))|p__d__instance(X,Z))),
% 8.78/7.03 inference(miniscoping,[status(thm)],[f7441])).
% 8.78/7.03 fof(f7443,plain,(
% 8.78/7.03 ![X0,X1,X2]: (~p__d__instance(X0,X1)|~p__d__subclass(X1,X2)|p__d__instance(X0,X2))),
% 8.78/7.03 inference(cnf_transformation,[status(thm)],[f7442])).
% 8.78/7.03 fof(f7718,plain,(
% 8.78/7.03 ![CLASS]: (~p__d__subclass(CLASS,c__Entity)|(?[THING]: p__d__instance(THING,CLASS)))),
% 8.78/7.03 inference(pre_NNF_transformation,[status(thm)],[f110])).
% 8.78/7.03 fof(f7719,plain,(
% 8.78/7.03 ![CLASS]: (~p__d__subclass(CLASS,c__Entity)|p__d__instance(sK13_skl(CLASS),CLASS))),
% 8.78/7.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(THING,sK13_skl(CLASS))],[f7718])).
% 8.78/7.03 fof(f7720,plain,(
% 8.78/7.03 ![X0]: (~p__d__subclass(X0,c__Entity)|p__d__instance(sK13_skl(X0),X0))),
% 8.78/7.03 inference(cnf_transformation,[status(thm)],[f7719])).
% 8.78/7.03 fof(f7725,plain,(
% 8.78/7.03 p__d__subclass(c__Physical,c__Entity)),
% 8.78/7.03 inference(cnf_transformation,[status(thm)],[f112])).
% 8.78/7.03 fof(f7884,plain,(
% 8.78/7.03 p__d__subclass(c__ContentBearingProcess,c__Process)),
% 8.78/7.03 inference(cnf_transformation,[status(thm)],[f191])).
% 8.78/7.03 fof(f7942,plain,(
% 8.78/7.03 p__d__subclass(c__Process,c__Physical)),
% 8.78/7.03 inference(cnf_transformation,[status(thm)],[f233])).
% 8.78/7.03 fof(f10295,plain,(
% 8.78/7.03 p__d__subclass(c__Speaking,c__LinguisticCommunication)),
% 8.78/7.03 inference(cnf_transformation,[status(thm)],[f1694])).
% 8.78/7.03 fof(f10296,plain,(
% 8.78/7.03 p__d__subclass(c__Speaking,c__Vocalizing)),
% 8.78/7.03 inference(cnf_transformation,[status(thm)],[f1695])).
% 8.78/7.03 fof(f10778,plain,(
% 8.78/7.03 p__d__subclass(c__Communication,c__ContentBearingProcess)),
% 6.22/7.12 inference(cnf_transformation,[status(thm)],[f1901])).
% 6.22/7.12 fof(f10812,plain,(
% 6.22/7.12 p__d__subclass(c__LinguisticCommunication,c__Communication)),
% 6.22/7.12 inference(cnf_transformation,[status(thm)],[f1914])).
% 6.22/7.12 fof(f23432,plain,(
% 6.22/7.12 (![X,Y]: ((~p__d__instance(Y,c__Speaking)|~p__d__instance(X,c__Vocalizing))|~X=Y))),
% 6.22/7.12 inference(pre_NNF_transformation,[status(thm)],[f7434])).
% 6.22/7.12 fof(f23433,plain,(
% 6.22/7.12 ![X0,X1]: (~p__d__instance(X0,c__Speaking)|~p__d__instance(X1,c__Vocalizing)|~X1=X0)),
% 6.22/7.12 inference(cnf_transformation,[status(thm)],[f23432])).
% 6.22/7.12 fof(f23601,plain,(
% 6.22/7.12 ![X0]: (~p__d__instance(X0,c__Speaking)|~p__d__instance(X0,c__Vocalizing))),
% 6.22/7.12 inference(destructive_equality_resolution,[status(thm)],[f23433])).
% 6.22/7.12 fof(f23607,plain,(
% 6.22/7.12 ![X0]: (~p__d__subclass(c__LinguisticCommunication,X0)|p__d__subclass(c__Speaking,X0))),
% 6.22/7.12 inference(resolution,[status(thm)],[f7438,f10295])).
% 6.22/7.12 fof(f26997,plain,(
% 6.22/7.12 p__d__subclass(c__Speaking,c__Communication)),
% 6.22/7.12 inference(resolution,[status(thm)],[f10812,f23607])).
% 6.22/7.12 fof(f27001,plain,(
% 6.22/7.12 ![X0]: (~p__d__subclass(c__Communication,X0)|p__d__subclass(c__Speaking,X0))),
% 6.22/7.12 inference(resolution,[status(thm)],[f26997,f7438])).
% 6.22/7.12 fof(f27002,plain,(
% 6.22/7.12 p__d__subclass(c__Speaking,c__ContentBearingProcess)),
% 6.22/7.12 inference(resolution,[status(thm)],[f27001,f10778])).
% 6.22/7.12 fof(f27006,plain,(
% 6.22/7.12 ![X0]: (~p__d__subclass(c__ContentBearingProcess,X0)|p__d__subclass(c__Speaking,X0))),
% 6.22/7.12 inference(resolution,[status(thm)],[f27002,f7438])).
% 6.22/7.12 fof(f27009,plain,(
% 6.22/7.12 p__d__subclass(c__Speaking,c__Process)),
% 6.22/7.12 inference(resolution,[status(thm)],[f27006,f7884])).
% 6.22/7.12 fof(f27013,plain,(
% 6.22/7.12 ![X0]: (~p__d__subclass(c__Process,X0)|p__d__subclass(c__Speaking,X0))),
% 6.22/7.12 inference(resolution,[status(thm)],[f27009,f7438])).
% 6.22/7.12 fof(f27020,plain,(
% 6.22/7.12 p__d__subclass(c__Speaking,c__Physical)),
% 6.22/7.12 inference(resolution,[status(thm)],[f27013,f7942])).
% 6.22/7.12 fof(f27023,plain,(
% 6.22/7.12 ![X0]: (~p__d__subclass(c__Physical,X0)|p__d__subclass(c__Speaking,X0))),
% 6.22/7.12 inference(resolution,[status(thm)],[f27020,f7438])).
% 6.22/7.12 fof(f27068,plain,(
% 6.22/7.12 p__d__subclass(c__Speaking,c__Entity)),
% 6.22/7.12 inference(resolution,[status(thm)],[f27023,f7725])).
% 6.22/7.12 fof(f27071,plain,(
% 6.22/7.12 p__d__instance(sK13_skl(c__Speaking),c__Speaking)),
% 6.22/7.12 inference(resolution,[status(thm)],[f27068,f7720])).
% 6.22/7.12 fof(f27076,plain,(
% 6.22/7.12 ~p__d__instance(sK13_skl(c__Speaking),c__Vocalizing)),
% 6.22/7.12 inference(resolution,[status(thm)],[f27071,f23601])).
% 6.22/7.12 fof(f27077,plain,(
% 6.22/7.12 ![X0]: (~p__d__subclass(c__Speaking,X0)|p__d__instance(sK13_skl(c__Speaking),X0))),
% 6.22/7.12 inference(resolution,[status(thm)],[f27071,f7443])).
% 6.22/7.12 fof(f27098,plain,(
% 6.22/7.12 p__d__instance(sK13_skl(c__Speaking),c__Vocalizing)),
% 6.22/7.12 inference(resolution,[status(thm)],[f27077,f10296])).
% 6.22/7.12 fof(f27101,plain,(
% 6.22/7.12 $false),
% 6.22/7.12 inference(forward_subsumption_resolution,[status(thm)],[f27098,f27076])).
% 6.22/7.12 % SZS output end CNFRefutation for theBenchmark.p
% 6.22/7.16 % Elapsed time: 1.638368 seconds
% 6.22/7.16 % CPU time: 9.213366 seconds
% 6.22/7.16 % Total memory used: 592.504 MB
% 6.22/7.16 % Net memory used: 588.371 MB
%------------------------------------------------------------------------------