%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR254+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:29 PM UTC 2026
% Result : Theorem 69.43s 9.62s
% Output : CNFRefutation 69.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 17
% Syntax : Number of formulae : 75 ( 38 unt; 0 def)
% Number of atoms : 132 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 104 ( 47 ~; 41 |; 11 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-1 aty)
% Number of variables : 65 ( 57 !; 8 ?)
% 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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f110,axiom,
! [CLASS] :
( p__d__subclass(CLASS,c__Entity)
=> ? [THING] : p__d__instance(THING,CLASS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,axiom,
p__d__subclass(c__SelfConnectedObject,c__Object),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,axiom,
p__d__subclass(c__CorpuscularObject,c__SelfConnectedObject),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f192,axiom,
p__d__subclass(c__ContentBearingObject,c__CorpuscularObject),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f233,axiom,
p__d__subclass(c__Process,c__Physical),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1859,axiom,
p__d__subclass(c__InternalChange,c__Process),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1864,axiom,
! [DEVELOP] :
( p__d__instance(DEVELOP,c__ContentDevelopment)
=> ? [OBJ] :
( p__result(DEVELOP,OBJ)
& p__d__instance(OBJ,c__ContentBearingObject) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1877,axiom,
p__d__subclass(c__Creation,c__InternalChange),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1880,axiom,
p__d__subclass(c__Making,c__Creation),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1884,axiom,
p__d__subclass(c__Manufacture,c__Making),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1885,axiom,
p__d__subclass(c__Publication,c__Manufacture),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1886,axiom,
p__d__subclass(c__Publication,c__ContentDevelopment),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7290,axiom,
! [X1,X2] :
( p__result(X1,X2)
=> p__d__instance(X1,c__Process) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7433,conjecture,
? [X,Y] :
( p__result(X,Y)
& p__d__instance(Y,c__Object)
& p__d__instance(X,c__Manufacture)
& p__d__instance(X,c__Process) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7434,negated_conjecture,
~ ? [X,Y] :
( p__result(X,Y)
& p__d__instance(Y,c__Object)
& p__d__instance(X,c__Manufacture)
& p__d__instance(X,c__Process) ),
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(f7735,plain,
p__d__subclass(c__SelfConnectedObject,c__Object),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f7844,plain,
p__d__subclass(c__CorpuscularObject,c__SelfConnectedObject),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f7885,plain,
p__d__subclass(c__ContentBearingObject,c__CorpuscularObject),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f7942,plain,
p__d__subclass(c__Process,c__Physical),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f10686,plain,
p__d__subclass(c__InternalChange,c__Process),
inference(cnf_transformation,[status(thm)],[f1859]) ).
fof(f10691,plain,
! [DEVELOP] :
( ? [OBJ] :
( p__result(DEVELOP,OBJ)
& p__d__instance(OBJ,c__ContentBearingObject) )
| ~ p__d__instance(DEVELOP,c__ContentDevelopment) ),
inference(pre_NNF_transformation,[status(thm)],[f1864]) ).
fof(f10692,plain,
! [DEVELOP] :
( ( p__result(DEVELOP,sK217_skl(DEVELOP))
& p__d__instance(sK217_skl(DEVELOP),c__ContentBearingObject) )
| ~ p__d__instance(DEVELOP,c__ContentDevelopment) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK217_skl]),skolemize(OBJ,sK217_skl(DEVELOP))],[f10691]) ).
fof(f10693,plain,
! [X0] :
( p__d__instance(sK217_skl(X0),c__ContentBearingObject)
| ~ p__d__instance(X0,c__ContentDevelopment) ),
inference(cnf_transformation,[status(thm)],[f10692]) ).
fof(f10694,plain,
! [X0] :
( p__result(X0,sK217_skl(X0))
| ~ p__d__instance(X0,c__ContentDevelopment) ),
inference(cnf_transformation,[status(thm)],[f10692]) ).
fof(f10724,plain,
p__d__subclass(c__Creation,c__InternalChange),
inference(cnf_transformation,[status(thm)],[f1877]) ).
fof(f10736,plain,
p__d__subclass(c__Making,c__Creation),
inference(cnf_transformation,[status(thm)],[f1880]) ).
fof(f10745,plain,
p__d__subclass(c__Manufacture,c__Making),
inference(cnf_transformation,[status(thm)],[f1884]) ).
fof(f10746,plain,
p__d__subclass(c__Publication,c__Manufacture),
inference(cnf_transformation,[status(thm)],[f1885]) ).
fof(f10747,plain,
p__d__subclass(c__Publication,c__ContentDevelopment),
inference(cnf_transformation,[status(thm)],[f1886]) ).
fof(f22900,plain,
! [X1,X2] :
( p__d__instance(X1,c__Process)
| ~ p__result(X1,X2) ),
inference(pre_NNF_transformation,[status(thm)],[f7290]) ).
fof(f22901,plain,
! [X1] :
( p__d__instance(X1,c__Process)
| ! [X2] : ~ p__result(X1,X2) ),
inference(miniscoping,[status(thm)],[f22900]) ).
fof(f22902,plain,
! [X0,X1] :
( p__d__instance(X0,c__Process)
| ~ p__result(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22901]) ).
fof(f23432,plain,
! [X,Y] :
( ~ p__result(X,Y)
| ~ p__d__instance(Y,c__Object)
| ~ p__d__instance(X,c__Manufacture)
| ~ p__d__instance(X,c__Process) ),
inference(pre_NNF_transformation,[status(thm)],[f7434]) ).
fof(f23433,plain,
! [X0,X1] :
( ~ p__result(X0,X1)
| ~ p__d__instance(X1,c__Object)
| ~ p__d__instance(X0,c__Manufacture)
| ~ p__d__instance(X0,c__Process) ),
inference(cnf_transformation,[status(thm)],[f23432]) ).
fof(f23605,plain,
! [X0,X1] :
( ~ p__result(X0,X1)
| ~ p__d__instance(X1,c__Object)
| ~ p__d__instance(X0,c__Manufacture) ),
inference(backward_subsumption_resolution,[status(thm)],[f23433,f22902]) ).
fof(f23606,plain,
! [X0] :
( p__d__subclass(c__Publication,X0)
| ~ p__d__subclass(c__Manufacture,X0) ),
inference(resolution,[status(thm)],[f7438,f10746]) ).
fof(f23609,plain,
p__d__subclass(c__Publication,c__Making),
inference(resolution,[status(thm)],[f23606,f10745]) ).
fof(f23618,plain,
! [X0] :
( p__d__subclass(c__Publication,X0)
| ~ p__d__subclass(c__Making,X0) ),
inference(resolution,[status(thm)],[f23609,f7438]) ).
fof(f29964,plain,
p__d__subclass(c__Publication,c__Creation),
inference(resolution,[status(thm)],[f10736,f23618]) ).
fof(f29990,plain,
! [X0] :
( p__d__subclass(c__Publication,X0)
| ~ p__d__subclass(c__Creation,X0) ),
inference(resolution,[status(thm)],[f29964,f7438]) ).
fof(f29994,plain,
p__d__subclass(c__Publication,c__InternalChange),
inference(resolution,[status(thm)],[f29990,f10724]) ).
fof(f29997,plain,
! [X0] :
( p__d__subclass(c__Publication,X0)
| ~ p__d__subclass(c__InternalChange,X0) ),
inference(resolution,[status(thm)],[f29994,f7438]) ).
fof(f30043,plain,
p__d__subclass(c__Publication,c__Process),
inference(resolution,[status(thm)],[f29997,f10686]) ).
fof(f30046,plain,
! [X0] :
( p__d__subclass(c__Publication,X0)
| ~ p__d__subclass(c__Process,X0) ),
inference(resolution,[status(thm)],[f30043,f7438]) ).
fof(f30089,plain,
p__d__subclass(c__Publication,c__Physical),
inference(resolution,[status(thm)],[f30046,f7942]) ).
fof(f30092,plain,
! [X0] :
( p__d__subclass(c__Publication,X0)
| ~ p__d__subclass(c__Physical,X0) ),
inference(resolution,[status(thm)],[f30089,f7438]) ).
fof(f30139,plain,
p__d__subclass(c__Publication,c__Entity),
inference(resolution,[status(thm)],[f30092,f7725]) ).
fof(f30142,plain,
p__d__instance(sK13_skl(c__Publication),c__Publication),
inference(resolution,[status(thm)],[f30139,f7720]) ).
fof(f30149,plain,
! [X0] :
( p__d__instance(sK13_skl(c__Publication),X0)
| ~ p__d__subclass(c__Publication,X0) ),
inference(resolution,[status(thm)],[f30142,f7443]) ).
fof(f30401,plain,
p__d__instance(sK13_skl(c__Publication),c__ContentDevelopment),
inference(resolution,[status(thm)],[f30149,f10747]) ).
fof(f30405,plain,
p__d__instance(sK13_skl(c__Publication),c__Manufacture),
inference(resolution,[status(thm)],[f30149,f10746]) ).
fof(f40764,plain,
p__d__instance(sK217_skl(sK13_skl(c__Publication)),c__ContentBearingObject),
inference(resolution,[status(thm)],[f10693,f30401]) ).
fof(f40772,plain,
p__result(sK13_skl(c__Publication),sK217_skl(sK13_skl(c__Publication))),
inference(resolution,[status(thm)],[f10694,f30401]) ).
fof(f40781,plain,
! [X0] :
( p__d__instance(sK217_skl(sK13_skl(c__Publication)),X0)
| ~ p__d__subclass(c__ContentBearingObject,X0) ),
inference(resolution,[status(thm)],[f40764,f7443]) ).
fof(f40792,plain,
( ~ p__d__instance(sK217_skl(sK13_skl(c__Publication)),c__Object)
| ~ p__d__instance(sK13_skl(c__Publication),c__Manufacture) ),
inference(resolution,[status(thm)],[f40772,f23605]) ).
fof(f40797,plain,
~ p__d__instance(sK217_skl(sK13_skl(c__Publication)),c__Object),
inference(forward_subsumption_resolution,[status(thm)],[f40792,f30405]) ).
fof(f40799,plain,
p__d__instance(sK217_skl(sK13_skl(c__Publication)),c__CorpuscularObject),
inference(resolution,[status(thm)],[f40781,f7885]) ).
fof(f40810,plain,
! [X0] :
( p__d__instance(sK217_skl(sK13_skl(c__Publication)),X0)
| ~ p__d__subclass(c__CorpuscularObject,X0) ),
inference(resolution,[status(thm)],[f40799,f7443]) ).
fof(f41016,plain,
p__d__instance(sK217_skl(sK13_skl(c__Publication)),c__SelfConnectedObject),
inference(resolution,[status(thm)],[f40810,f7844]) ).
fof(f41069,plain,
! [X0] :
( p__d__instance(sK217_skl(sK13_skl(c__Publication)),X0)
| ~ p__d__subclass(c__SelfConnectedObject,X0) ),
inference(resolution,[status(thm)],[f41016,f7443]) ).
fof(f41130,plain,
p__d__instance(sK217_skl(sK13_skl(c__Publication)),c__Object),
inference(resolution,[status(thm)],[f41069,f7735]) ).
fof(f41132,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f41130,f40797]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR254+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n005.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 21 15:20:32 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.57/0.85 % Drodi V4.1.1
% 69.43/9.62 % Refutation found
% 69.43/9.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 69.43/9.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.24/9.73 % Elapsed time: 9.293669 seconds
% 8.24/9.73 % CPU time: 69.834420 seconds
% 8.24/9.73 % Total memory used: 707.762 MB
% 8.24/9.73 % Net memory used: 695.642 MB
%------------------------------------------------------------------------------