%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR174+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:24 PM UTC 2026
% Result : Theorem 24.70s 3.81s
% Output : CNFRefutation 2.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 11
% Syntax : Number of formulae : 46 ( 23 unt; 0 def)
% Number of atoms : 81 ( 4 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 66 ( 31 ~; 26 |; 6 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-1 aty)
% Number of variables : 45 ( 39 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X,Y,Z] :
( ( p__d__subclass(Y,Z)
& p__d__subclass(X,Y) )
=> p__d__subclass(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y,Z] :
( ( p__d__subclass(Y,Z)
& p__d__instance(X,Y) )
=> p__d__instance(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f110,axiom,
! [CLASS] :
( p__d__subclass(CLASS,c__Entity)
=> ? [THING] : p__d__instance(THING,CLASS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,axiom,
p__d__subclass(c__ContentBearingProcess,c__Process),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f233,axiom,
p__d__subclass(c__Process,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1694,axiom,
p__d__subclass(c__Speaking,c__LinguisticCommunication),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1695,axiom,
p__d__subclass(c__Speaking,c__Vocalizing),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1901,axiom,
p__d__subclass(c__Communication,c__ContentBearingProcess),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1914,axiom,
p__d__subclass(c__LinguisticCommunication,c__Communication),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7433,conjecture,
? [X,Y] :
( X = Y
& p__d__instance(X,c__Vocalizing)
& p__d__instance(Y,c__Speaking) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7434,negated_conjecture,
~ ? [X,Y] :
( X = Y
& p__d__instance(X,c__Vocalizing)
& p__d__instance(Y,c__Speaking) ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7436,plain,
! [X,Y,Z] :
( p__d__subclass(X,Z)
| ~ p__d__subclass(Y,Z)
| ~ p__d__subclass(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f7437,plain,
! [X,Z] :
( p__d__subclass(X,Z)
| ! [Y] :
( ~ p__d__subclass(Y,Z)
| ~ p__d__subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f7436]) ).
fof(f7438,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X1,X2)
| ~ p__d__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7437]) ).
fof(f7441,plain,
! [X,Y,Z] :
( p__d__instance(X,Z)
| ~ p__d__subclass(Y,Z)
| ~ p__d__instance(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f7442,plain,
! [X,Z] :
( p__d__instance(X,Z)
| ! [Y] :
( ~ p__d__subclass(Y,Z)
| ~ p__d__instance(X,Y) ) ),
inference(miniscoping,[status(thm)],[f7441]) ).
fof(f7443,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__subclass(X1,X2)
| ~ p__d__instance(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7442]) ).
fof(f7718,plain,
! [CLASS] :
( ? [THING] : p__d__instance(THING,CLASS)
| ~ p__d__subclass(CLASS,c__Entity) ),
inference(pre_NNF_transformation,[status(thm)],[f110]) ).
fof(f7719,plain,
! [CLASS] :
( p__d__instance(sK13_skl(CLASS),CLASS)
| ~ p__d__subclass(CLASS,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(THING,sK13_skl(CLASS))],[f7718]) ).
fof(f7720,plain,
! [X0] :
( p__d__instance(sK13_skl(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[status(thm)],[f7719]) ).
fof(f7725,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f7884,plain,
p__d__subclass(c__ContentBearingProcess,c__Process),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f7942,plain,
p__d__subclass(c__Process,c__Physical),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f10295,plain,
p__d__subclass(c__Speaking,c__LinguisticCommunication),
inference(cnf_transformation,[status(thm)],[f1694]) ).
fof(f10296,plain,
p__d__subclass(c__Speaking,c__Vocalizing),
inference(cnf_transformation,[status(thm)],[f1695]) ).
fof(f10778,plain,
p__d__subclass(c__Communication,c__ContentBearingProcess),
inference(cnf_transformation,[status(thm)],[f1901]) ).
fof(f10812,plain,
p__d__subclass(c__LinguisticCommunication,c__Communication),
inference(cnf_transformation,[status(thm)],[f1914]) ).
fof(f23432,plain,
! [X,Y] :
( X != Y
| ~ p__d__instance(X,c__Vocalizing)
| ~ p__d__instance(Y,c__Speaking) ),
inference(pre_NNF_transformation,[status(thm)],[f7434]) ).
fof(f23433,plain,
! [X0,X1] :
( X1 != X0
| ~ p__d__instance(X1,c__Vocalizing)
| ~ p__d__instance(X0,c__Speaking) ),
inference(cnf_transformation,[status(thm)],[f23432]) ).
fof(f23601,plain,
! [X0] :
( ~ p__d__instance(X0,c__Vocalizing)
| ~ p__d__instance(X0,c__Speaking) ),
inference(destructive_equality_resolution,[status(thm)],[f23433]) ).
fof(f23607,plain,
! [X0] :
( p__d__subclass(c__Speaking,X0)
| ~ p__d__subclass(c__LinguisticCommunication,X0) ),
inference(resolution,[status(thm)],[f7438,f10295]) ).
fof(f30189,plain,
p__d__subclass(c__Speaking,c__Communication),
inference(resolution,[status(thm)],[f10812,f23607]) ).
fof(f30193,plain,
! [X0] :
( p__d__subclass(c__Speaking,X0)
| ~ p__d__subclass(c__Communication,X0) ),
inference(resolution,[status(thm)],[f30189,f7438]) ).
fof(f30194,plain,
p__d__subclass(c__Speaking,c__ContentBearingProcess),
inference(resolution,[status(thm)],[f30193,f10778]) ).
fof(f30198,plain,
! [X0] :
( p__d__subclass(c__Speaking,X0)
| ~ p__d__subclass(c__ContentBearingProcess,X0) ),
inference(resolution,[status(thm)],[f30194,f7438]) ).
fof(f30227,plain,
p__d__subclass(c__Speaking,c__Process),
inference(resolution,[status(thm)],[f30198,f7884]) ).
fof(f30231,plain,
! [X0] :
( p__d__subclass(c__Speaking,X0)
| ~ p__d__subclass(c__Process,X0) ),
inference(resolution,[status(thm)],[f30227,f7438]) ).
fof(f30238,plain,
p__d__subclass(c__Speaking,c__Physical),
inference(resolution,[status(thm)],[f30231,f7942]) ).
fof(f30267,plain,
! [X0] :
( p__d__subclass(c__Speaking,X0)
| ~ p__d__subclass(c__Physical,X0) ),
inference(resolution,[status(thm)],[f30238,f7438]) ).
fof(f30272,plain,
p__d__subclass(c__Speaking,c__Entity),
inference(resolution,[status(thm)],[f30267,f7725]) ).
fof(f30275,plain,
p__d__instance(sK13_skl(c__Speaking),c__Speaking),
inference(resolution,[status(thm)],[f30272,f7720]) ).
fof(f30314,plain,
~ p__d__instance(sK13_skl(c__Speaking),c__Vocalizing),
inference(resolution,[status(thm)],[f30275,f23601]) ).
fof(f30316,plain,
! [X0] :
( p__d__instance(sK13_skl(c__Speaking),X0)
| ~ p__d__subclass(c__Speaking,X0) ),
inference(resolution,[status(thm)],[f30275,f7443]) ).
fof(f30372,plain,
p__d__instance(sK13_skl(c__Speaking),c__Vocalizing),
inference(resolution,[status(thm)],[f30316,f10296]) ).
fof(f30375,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f30372,f30314]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR174+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 15:20:15 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.38/0.63 % Drodi V4.1.1
% 24.70/3.81 % Refutation found
% 24.70/3.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 24.70/3.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.57/3.94 % Elapsed time: 3.544435 seconds
% 2.57/3.94 % CPU time: 25.537309 seconds
% 2.57/3.94 % Total memory used: 654.625 MB
% 2.57/3.94 % Net memory used: 646.051 MB
%------------------------------------------------------------------------------