%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR108+7 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:13:45 PM UTC 2026
% Result : Theorem 16.73s 6.53s
% Output : CNFRefutation 17.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 8
% Syntax : Number of formulae : 27 ( 12 unt; 3 def)
% Number of atoms : 52 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 43 ( 18 ~; 16 |; 6 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 4 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 4 ( 2 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f55599,axiom,
s__instance(s__Entity44_1,s__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55600,axiom,
s__instance(s__Entity44_2,s__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55607,axiom,
s__instance(s__Entity44_9,s__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55608,axiom,
s__instance(s__Entity44_10,s__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55611,conjecture,
? [X__s__Animal] :
( s__instance(s__Entity44_10,X__s__Animal)
& s__instance(s__Entity44_9,X__s__Animal)
& s__instance(s__Entity44_2,X__s__Animal)
& s__instance(s__Entity44_1,X__s__Animal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55612,negated_conjecture,
~ ? [X__s__Animal] :
( s__instance(s__Entity44_10,X__s__Animal)
& s__instance(s__Entity44_9,X__s__Animal)
& s__instance(s__Entity44_2,X__s__Animal)
& s__instance(s__Entity44_1,X__s__Animal) ),
inference(negated_conjecture,[status(cth)],[f55611]) ).
fof(f156935,plain,
s__instance(s__Entity44_1,s__Entity),
inference(cnf_transformation,[status(thm)],[f55599]) ).
fof(f156936,plain,
s__instance(s__Entity44_2,s__Entity),
inference(cnf_transformation,[status(thm)],[f55600]) ).
fof(f156943,plain,
s__instance(s__Entity44_9,s__Entity),
inference(cnf_transformation,[status(thm)],[f55607]) ).
fof(f156944,plain,
s__instance(s__Entity44_10,s__Entity),
inference(cnf_transformation,[status(thm)],[f55608]) ).
fof(f156952,plain,
! [X__s__Animal] :
( ~ s__instance(s__Entity44_10,X__s__Animal)
| ~ s__instance(s__Entity44_9,X__s__Animal)
| ~ s__instance(s__Entity44_2,X__s__Animal)
| ~ s__instance(s__Entity44_1,X__s__Animal) ),
inference(pre_NNF_transformation,[status(thm)],[f55612]) ).
fof(f156953,plain,
! [X0] :
( ~ s__instance(s__Entity44_10,X0)
| ~ s__instance(s__Entity44_9,X0)
| ~ s__instance(s__Entity44_2,X0)
| ~ s__instance(s__Entity44_1,X0) ),
inference(cnf_transformation,[status(thm)],[f156952]) ).
fof(f167838,plain,
( ~ s__instance(s__Entity44_10,s__Entity)
| ~ s__instance(s__Entity44_9,s__Entity)
| ~ s__instance(s__Entity44_2,s__Entity) ),
inference(resolution,[status(thm)],[f156935,f156953]) ).
fof(f167839,definition,
( sQ808_spl
<=> s__instance(s__Entity44_2,s__Entity) ),
introduced(definition,[new_symbols(definition,[sQ808_spl])],[split_symbol_definition]) ).
fof(f167841,plain,
( sQ808_spl
| ~ s__instance(s__Entity44_2,s__Entity) ),
inference(component_clause,[status(thm)],[f167839]) ).
fof(f167842,definition,
( sQ809_spl
<=> s__instance(s__Entity44_9,s__Entity) ),
introduced(definition,[new_symbols(definition,[sQ809_spl])],[split_symbol_definition]) ).
fof(f167844,plain,
( sQ809_spl
| ~ s__instance(s__Entity44_9,s__Entity) ),
inference(component_clause,[status(thm)],[f167842]) ).
fof(f167845,definition,
( sQ810_spl
<=> s__instance(s__Entity44_10,s__Entity) ),
introduced(definition,[new_symbols(definition,[sQ810_spl])],[split_symbol_definition]) ).
fof(f167847,plain,
( sQ810_spl
| ~ s__instance(s__Entity44_10,s__Entity) ),
inference(component_clause,[status(thm)],[f167845]) ).
fof(f167848,plain,
( ~ sQ810_spl
| ~ sQ809_spl
| ~ sQ808_spl ),
inference(split_clause,[status(thm)],[f167838,f167839,f167842,f167845]) ).
fof(f167849,plain,
( sQ808_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f156936,f167841]) ).
fof(f167850,plain,
sQ808_spl,
inference(contradiction_clause,[status(thm)],[f167849]) ).
fof(f167851,plain,
( sQ809_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f156943,f167844]) ).
fof(f167852,plain,
sQ809_spl,
inference(contradiction_clause,[status(thm)],[f167851]) ).
fof(f167853,plain,
( sQ810_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f156944,f167847]) ).
fof(f167854,plain,
sQ810_spl,
inference(contradiction_clause,[status(thm)],[f167853]) ).
fof(f167855,plain,
$false,
inference(sat_refutation,[status(thm)],[f167848,f167850,f167852,f167854]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR108+7 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n002.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 15:04:33 UTC 2026
% 0.17/0.43 % CPUTime :
% 4.56/4.81 % Drodi V4.1.1
% 16.73/6.53 % Refutation found
% 16.73/6.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.73/6.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.14/7.71 % Elapsed time: 7.141990 seconds
% 5.14/7.71 % CPU time: 18.302053 seconds
% 5.14/7.71 % Total memory used: 3.912 GB
% 5.14/7.71 % Net memory used: 3.874 GB
%------------------------------------------------------------------------------