%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR079+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:29 PM UTC 2026
% Result : Theorem 149.46s 24.73s
% Output : CNFRefutation 149.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 29
% Syntax : Number of formulae : 106 ( 51 unt; 10 def)
% Number of atoms : 200 ( 25 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 189 ( 95 ~; 77 |; 4 &)
% ( 10 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 11 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 18 con; 0-0 aty)
% Number of variables : 43 ( 43 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [V__X,V__Y] :
( s__subclass(V__X,V__Y)
=> ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [V__X,V__Y,V__Z] :
( ( s__instance(V__X,s__SetOrClass)
& s__instance(V__Y,s__SetOrClass) )
=> ( ( s__instance(V__Z,V__X)
& s__subclass(V__X,V__Y) )
=> s__instance(V__Z,V__Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5906,axiom,
s__subclass(s__Animal,s__Organism),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5923,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5952,axiom,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6026,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7219,axiom,
s__instance(s__Organism5_1,s__Lizard5_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7240,axiom,
s__Class5_1 = s__Class5_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7241,axiom,
s__Class5_2 = s__Class5_3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7242,axiom,
s__Class5_3 = s__Class5_4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7243,axiom,
s__Class5_4 = s__Class5_5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7244,axiom,
s__Class5_5 = s__Class5_6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7245,axiom,
s__Class5_6 = s__Class5_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7246,axiom,
s__Class5_7 = s__Class5_8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7247,axiom,
s__Class5_8 = s__Class5_9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7248,axiom,
s__Class5_9 = s__Class5_10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7249,axiom,
s__subclass(s__Lizard5_1,s__Class5_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7250,axiom,
s__subclass(s__Class5_10,s__Reptile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7251,conjecture,
s__instance(s__Organism5_1,s__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7252,negated_conjecture,
~ s__instance(s__Organism5_1,s__Animal),
inference(negated_conjecture,[status(cth)],[f7251]) ).
fof(f7292,plain,
! [V__X,V__Y] :
( ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) )
| ~ s__subclass(V__X,V__Y) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f7293,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f7292]) ).
fof(f7294,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7292]) ).
fof(f7295,plain,
! [V__X,V__Y,V__Z] :
( s__instance(V__Z,V__Y)
| ~ s__instance(V__Z,V__X)
| ~ s__subclass(V__X,V__Y)
| ~ s__instance(V__X,s__SetOrClass)
| ~ s__instance(V__Y,s__SetOrClass) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f7296,plain,
! [V__X,V__Y] :
( ! [V__Z] :
( s__instance(V__Z,V__Y)
| ~ s__instance(V__Z,V__X)
| ~ s__subclass(V__X,V__Y) )
| ~ s__instance(V__X,s__SetOrClass)
| ~ s__instance(V__Y,s__SetOrClass) ),
inference(miniscoping,[status(thm)],[f7295]) ).
fof(f7297,plain,
! [X0,X1,X2] :
( s__instance(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__subclass(X0,X2)
| ~ s__instance(X1,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f7296]) ).
fof(f17413,plain,
s__subclass(s__Animal,s__Organism),
inference(cnf_transformation,[status(thm)],[f5906]) ).
fof(f17441,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(cnf_transformation,[status(thm)],[f5923]) ).
fof(f17470,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[status(thm)],[f5952]) ).
fof(f17552,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(cnf_transformation,[status(thm)],[f6026]) ).
fof(f19253,plain,
s__instance(s__Organism5_1,s__Lizard5_1),
inference(cnf_transformation,[status(thm)],[f7219]) ).
fof(f19274,plain,
s__Class5_2 = s__Class5_1,
inference(cnf_transformation,[status(thm)],[f7240]) ).
fof(f19275,plain,
s__Class5_3 = s__Class5_2,
inference(cnf_transformation,[status(thm)],[f7241]) ).
fof(f19276,plain,
s__Class5_4 = s__Class5_3,
inference(cnf_transformation,[status(thm)],[f7242]) ).
fof(f19277,plain,
s__Class5_4 = s__Class5_5,
inference(cnf_transformation,[status(thm)],[f7243]) ).
fof(f19278,plain,
s__Class5_5 = s__Class5_6,
inference(cnf_transformation,[status(thm)],[f7244]) ).
fof(f19279,plain,
s__Class5_6 = s__Class5_7,
inference(cnf_transformation,[status(thm)],[f7245]) ).
fof(f19280,plain,
s__Class5_7 = s__Class5_8,
inference(cnf_transformation,[status(thm)],[f7246]) ).
fof(f19281,plain,
s__Class5_8 = s__Class5_9,
inference(cnf_transformation,[status(thm)],[f7247]) ).
fof(f19282,plain,
s__Class5_9 = s__Class5_10,
inference(cnf_transformation,[status(thm)],[f7248]) ).
fof(f19283,plain,
s__subclass(s__Lizard5_1,s__Class5_1),
inference(cnf_transformation,[status(thm)],[f7249]) ).
fof(f19284,plain,
s__subclass(s__Class5_10,s__Reptile),
inference(cnf_transformation,[status(thm)],[f7250]) ).
fof(f19285,plain,
~ s__instance(s__Organism5_1,s__Animal),
inference(cnf_transformation,[status(thm)],[f7252]) ).
fof(f19940,plain,
s__Class5_1 = s__Class5_3,
inference(backward_demodulation,[status(thm)],[f19274,f19275]) ).
fof(f19941,plain,
s__Class5_3 = s__Class5_5,
inference(forward_demodulation,[status(thm)],[f19276,f19277]) ).
fof(f19943,plain,
s__Class5_6 = s__Class5_3,
inference(forward_demodulation,[status(thm)],[f19278,f19941]) ).
fof(f19944,plain,
s__Class5_6 = s__Class5_8,
inference(forward_demodulation,[status(thm)],[f19279,f19280]) ).
fof(f19946,plain,
s__Class5_10 = s__Class5_6,
inference(backward_demodulation,[status(thm)],[f19947,f19282]) ).
fof(f19947,plain,
s__Class5_6 = s__Class5_9,
inference(forward_demodulation,[status(thm)],[f19281,f19944]) ).
fof(f19949,plain,
s__Class5_6 = s__Class5_1,
inference(forward_demodulation,[status(thm)],[f19943,f19940]) ).
fof(f19950,plain,
s__subclass(s__Class5_6,s__Reptile),
inference(forward_demodulation,[status(thm)],[f19946,f19284]) ).
fof(f19951,plain,
s__subclass(s__Lizard5_1,s__Class5_6),
inference(forward_demodulation,[status(thm)],[f19949,f19283]) ).
fof(f20020,plain,
! [X0,X1,X2] :
( ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| s__instance(X0,X2)
| ~ s__instance(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f7297,f7293]) ).
fof(f20021,plain,
! [X0] :
( ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Animal) ),
inference(resolution,[status(thm)],[f20020,f19285]) ).
fof(f20216,definition,
( sQ89_spl
<=> s__instance(s__Animal,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f20218,plain,
( sQ89_spl
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f20216]) ).
fof(f20861,definition,
! [X0] :
( sQ260_spl
<=> ( ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Animal) ) ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f20862,plain,
! [X0] :
( ~ sQ260_spl
| ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Animal) ),
inference(component_clause,[status(thm)],[f20861]) ).
fof(f20864,plain,
( ~ sQ89_spl
| sQ260_spl ),
inference(split_clause,[status(thm)],[f20021,f20861,f20216]) ).
fof(f20889,plain,
( ~ sQ260_spl
| ~ s__instance(s__Organism5_1,s__Vertebrate) ),
inference(resolution,[status(thm)],[f20862,f17441]) ).
fof(f21432,definition,
( sQ381_spl
<=> s__instance(s__ColdBloodedVertebrate,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ381_spl])],[split_symbol_definition]) ).
fof(f21434,plain,
( sQ381_spl
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f21432]) ).
fof(f22398,plain,
! [X0] :
( sQ89_spl
| ~ s__subclass(s__Animal,X0) ),
inference(resolution,[status(thm)],[f20218,f7293]) ).
fof(f22415,plain,
( sQ89_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f17413,f22398]) ).
fof(f22432,plain,
sQ89_spl,
inference(contradiction_clause,[status(thm)],[f22415]) ).
fof(f22442,plain,
! [X0] :
( ~ sQ260_spl
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Vertebrate) ),
inference(resolution,[status(thm)],[f20889,f20020]) ).
fof(f22443,definition,
! [X0] :
( sQ503_spl
<=> ( ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Vertebrate) ) ),
introduced(definition,[new_symbols(definition,[sQ503_spl])],[split_symbol_definition]) ).
fof(f22444,plain,
! [X0] :
( ~ sQ503_spl
| ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Vertebrate) ),
inference(component_clause,[status(thm)],[f22443]) ).
fof(f22446,definition,
( sQ504_spl
<=> s__instance(s__Vertebrate,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ504_spl])],[split_symbol_definition]) ).
fof(f22448,plain,
( sQ504_spl
| ~ s__instance(s__Vertebrate,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f22446]) ).
fof(f22449,plain,
( ~ sQ260_spl
| ~ sQ504_spl
| sQ503_spl ),
inference(split_clause,[status(thm)],[f22442,f22443,f22446,f20861]) ).
fof(f22589,plain,
! [X0] :
( sQ504_spl
| ~ s__subclass(s__Vertebrate,X0) ),
inference(resolution,[status(thm)],[f22448,f7293]) ).
fof(f22878,plain,
( ~ sQ503_spl
| ~ s__instance(s__Organism5_1,s__ColdBloodedVertebrate) ),
inference(resolution,[status(thm)],[f22444,f17470]) ).
fof(f22940,plain,
( sQ504_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f17441,f22589]) ).
fof(f22945,plain,
sQ504_spl,
inference(contradiction_clause,[status(thm)],[f22940]) ).
fof(f22946,plain,
! [X0] :
( ~ sQ503_spl
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__ColdBloodedVertebrate) ),
inference(resolution,[status(thm)],[f22878,f20020]) ).
fof(f22947,definition,
! [X0] :
( sQ578_spl
<=> ( ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__ColdBloodedVertebrate) ) ),
introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition]) ).
fof(f22948,plain,
! [X0] :
( ~ sQ578_spl
| ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__ColdBloodedVertebrate) ),
inference(component_clause,[status(thm)],[f22947]) ).
fof(f22950,plain,
( ~ sQ503_spl
| ~ sQ381_spl
| sQ578_spl ),
inference(split_clause,[status(thm)],[f22946,f22947,f21432,f22443]) ).
fof(f24749,plain,
( ~ sQ578_spl
| ~ s__instance(s__Organism5_1,s__Reptile) ),
inference(resolution,[status(thm)],[f22948,f17552]) ).
fof(f24797,plain,
! [X0] :
( ~ sQ578_spl
| ~ s__instance(s__Reptile,s__SetOrClass)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Reptile) ),
inference(resolution,[status(thm)],[f24749,f20020]) ).
fof(f24798,definition,
! [X0] :
( sQ828_spl
<=> ( ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Reptile) ) ),
introduced(definition,[new_symbols(definition,[sQ828_spl])],[split_symbol_definition]) ).
fof(f24799,plain,
! [X0] :
( ~ sQ828_spl
| ~ s__subclass(X0,s__Reptile)
| ~ s__instance(s__Organism5_1,X0) ),
inference(component_clause,[status(thm)],[f24798]) ).
fof(f24801,definition,
( sQ829_spl
<=> s__instance(s__Reptile,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ829_spl])],[split_symbol_definition]) ).
fof(f24803,plain,
( sQ829_spl
| ~ s__instance(s__Reptile,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f24801]) ).
fof(f24804,plain,
( ~ sQ578_spl
| ~ sQ829_spl
| sQ828_spl ),
inference(split_clause,[status(thm)],[f24797,f24798,f24801,f22947]) ).
fof(f24918,plain,
! [X0] :
( sQ829_spl
| ~ s__subclass(s__Reptile,X0) ),
inference(resolution,[status(thm)],[f24803,f7293]) ).
fof(f25199,plain,
! [X0] :
( sQ381_spl
| ~ s__subclass(X0,s__ColdBloodedVertebrate) ),
inference(resolution,[status(thm)],[f21434,f7294]) ).
fof(f25215,plain,
( sQ381_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f17552,f25199]) ).
fof(f25246,plain,
sQ381_spl,
inference(contradiction_clause,[status(thm)],[f25215]) ).
fof(f27381,plain,
( ~ sQ828_spl
| ~ s__instance(s__Organism5_1,s__Class5_6) ),
inference(resolution,[status(thm)],[f24799,f19950]) ).
fof(f27434,plain,
( sQ829_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f17552,f24918]) ).
fof(f27447,plain,
sQ829_spl,
inference(contradiction_clause,[status(thm)],[f27434]) ).
fof(f27449,plain,
! [X0] :
( ~ sQ828_spl
| ~ s__instance(s__Class5_6,s__SetOrClass)
| ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Class5_6) ),
inference(resolution,[status(thm)],[f27381,f20020]) ).
fof(f27450,definition,
! [X0] :
( sQ1279_spl
<=> ( ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Class5_6) ) ),
introduced(definition,[new_symbols(definition,[sQ1279_spl])],[split_symbol_definition]) ).
fof(f27451,plain,
! [X0] :
( ~ sQ1279_spl
| ~ s__instance(s__Organism5_1,X0)
| ~ s__subclass(X0,s__Class5_6) ),
inference(component_clause,[status(thm)],[f27450]) ).
fof(f27453,definition,
( sQ1280_spl
<=> s__instance(s__Class5_6,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ1280_spl])],[split_symbol_definition]) ).
fof(f27455,plain,
( sQ1280_spl
| ~ s__instance(s__Class5_6,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f27453]) ).
fof(f27456,plain,
( ~ sQ828_spl
| ~ sQ1280_spl
| sQ1279_spl ),
inference(split_clause,[status(thm)],[f27449,f27450,f27453,f24798]) ).
fof(f27485,plain,
! [X0] :
( sQ1280_spl
| ~ s__subclass(X0,s__Class5_6) ),
inference(resolution,[status(thm)],[f27455,f7294]) ).
fof(f31754,plain,
( ~ sQ1279_spl
| ~ s__instance(s__Organism5_1,s__Lizard5_1) ),
inference(resolution,[status(thm)],[f27451,f19951]) ).
fof(f31755,plain,
( ~ sQ1279_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31754,f19253]) ).
fof(f31756,plain,
~ sQ1279_spl,
inference(contradiction_clause,[status(thm)],[f31755]) ).
fof(f31757,plain,
( sQ1280_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f19951,f27485]) ).
fof(f31758,plain,
sQ1280_spl,
inference(contradiction_clause,[status(thm)],[f31757]) ).
fof(f31759,plain,
$false,
inference(sat_refutation,[status(thm)],[f20864,f22432,f22449,f22945,f22950,f24804,f25246,f27447,f27456,f31756,f31758]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR079+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/5.46 % Computer : n008.cluster.edu
% 0.18/5.46 % Model : x86_64 x86_64
% 0.18/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.46 % Memory : 8046.5625MB
% 0.18/5.46 % OS : Linux 6.8.0-71-generic
% 0.18/5.46 % CPULimit : 300
% 0.18/5.46 % WCLimit : 300
% 0.18/5.46 % DateTime : Mon Sep 21 14:50:32 UTC 2026
% 0.18/5.47 % CPUTime :
% 0.23/5.91 % Drodi V4.1.1
% 149.46/24.73 % Refutation found
% 149.46/24.73 % SZS status Theorem for theBenchmark: Theorem is valid
% 149.46/24.73 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 86.10/24.87 % Elapsed time: 19.390540 seconds
% 86.10/24.87 % CPU time: 150.174992 seconds
% 86.10/24.87 % Total memory used: 873.662 MB
% 86.10/24.87 % Net memory used: 844.184 MB
%------------------------------------------------------------------------------