%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV022-2 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:46:00 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.51s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 36
% Syntax : Number of formulae : 126 ( 36 unt; 20 def)
% Number of atoms : 244 ( 52 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 203 ( 85 ~; 98 |; 0 &)
% ( 20 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 21 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 35 ( 35 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [T_0] : fwork_DOTfifo_DOTrtl_DOTlevel_(T_0) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [T_13] :
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [X_80] : f_ADD_(X_80,n1) != n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [X_81] : ~ p_LES_EQU_(f_ADD_(X_81,n1),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [X_82] :
( p_LES_EQU_(X_82,n0)
| ~ p_LES_EQU_(X_82,f_SUB_(X_82,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [Y_84,X_83,Z_85] :
( f_SUB_(X_83,Y_84) = Z_85
| f_ADD_(Z_85,Y_84) != X_83
| def_89(Y_84,X_83) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [X_83,Y_84] :
( ~ def_89(Y_84,X_83)
| p_LES_EQU_(X_83,Y_84) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [X_101,Y_102] :
( p_LES_EQU_(Y_102,X_101)
| ~ p_LES_EQU_(Y_102,f_ADD_(X_101,n1))
| f_ADD_(X_101,n1) = Y_102 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [X_106] : p_LES_EQU_(X_106,X_106),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [X_107,Y_108] :
( f_ADD_(X_107,n1) != f_ADD_(Y_108,n1)
| X_107 = Y_108 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [X_109] : f_ADD_(n0,X_109) = X_109,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f134,negated_conjecture,
f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f135,negated_conjecture,
p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f136,negated_conjecture,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,negated_conjecture,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f138,negated_conjecture,
fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) != fwork_DOTfifo_DOTrtl_DOTfifo__length_,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,plain,
! [X0] : fwork_DOTfifo_DOTrtl_DOTlevel_(X0) = fwork_DOTfifo_DOTrtl_DOTint__level_(X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f157,plain,
! [X0] :
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n1) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f210,plain,
! [X0] : f_ADD_(X0,n1) != n0,
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f211,plain,
! [X0] : ~ p_LES_EQU_(f_ADD_(X0,n1),n0),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f212,plain,
! [X0] :
( p_LES_EQU_(X0,n0)
| ~ p_LES_EQU_(X0,f_SUB_(X0,n1)) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f214,plain,
! [X0,X1,X2] :
( f_SUB_(X1,X0) = X2
| f_ADD_(X2,X0) != X1
| def_89(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f216,plain,
! [X0,X1] :
( ~ def_89(X1,X0)
| p_LES_EQU_(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f224,plain,
! [X0,X1] :
( p_LES_EQU_(X1,X0)
| ~ p_LES_EQU_(X1,f_ADD_(X0,n1))
| f_ADD_(X0,n1) = X1 ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f227,plain,
! [X0] : p_LES_EQU_(X0,X0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f228,plain,
! [X0,X1] :
( f_ADD_(X0,n1) != f_ADD_(X1,n1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f229,plain,
! [X0] : f_ADD_(n0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f299,plain,
f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f300,plain,
p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f301,plain,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f302,plain,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f303,plain,
fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) != fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f305,plain,
! [X0,X1] :
( f_SUB_(f_ADD_(X1,X0),X0) = X1
| def_89(X0,f_ADD_(X1,X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f214]) ).
fof(f309,plain,
f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(backward_demodulation,[status(thm)],[f142,f299]) ).
fof(f319,definition,
( sQ1_spl
<=> p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f321,plain,
( sQ1_spl
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)) ),
inference(component_clause,[status(thm)],[f319]) ).
fof(f322,definition,
( sQ2_spl
<=> p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f324,plain,
( sQ2_spl
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)) ),
inference(component_clause,[status(thm)],[f322]) ).
fof(f325,definition,
( sQ3_spl
<=> p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f326,plain,
( ~ sQ3_spl
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)) ),
inference(component_clause,[status(thm)],[f325]) ).
fof(f329,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f326,f301]) ).
fof(f330,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f329]) ).
fof(f331,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f324,f300]) ).
fof(f332,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f331]) ).
fof(f333,plain,
fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) != fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(forward_demodulation,[status(thm)],[f142,f303]) ).
fof(f345,plain,
! [X0] :
( f_ADD_(X0,n1) != n1
| X0 = n0 ),
inference(paramodulation,[status(thm)],[f229,f228]) ).
fof(f375,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ != n1
| fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = n0 ),
inference(paramodulation,[status(thm)],[f309,f345]) ).
fof(f386,definition,
( sQ12_spl
<=> fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = n0 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f387,plain,
( ~ sQ12_spl
| fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = n0 ),
inference(component_clause,[status(thm)],[f386]) ).
fof(f389,definition,
( sQ13_spl
<=> fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n1 ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f391,plain,
( sQ13_spl
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ != n1 ),
inference(component_clause,[status(thm)],[f389]) ).
fof(f392,plain,
( ~ sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f375,f386,f389]) ).
fof(f416,plain,
( ~ sQ12_spl
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) ),
inference(paramodulation,[status(thm)],[f387,f157]) ).
fof(f418,definition,
( sQ19_spl
<=> fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f419,plain,
( ~ sQ19_spl
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f421,definition,
( sQ20_spl
<=> p_LES_EQU_(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f423,plain,
( sQ20_spl
| ~ p_LES_EQU_(n0,n0) ),
inference(component_clause,[status(thm)],[f421]) ).
fof(f424,definition,
( sQ21_spl
<=> p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f425,plain,
( ~ sQ21_spl
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
inference(component_clause,[status(thm)],[f424]) ).
fof(f429,definition,
( sQ22_spl
<=> p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f430,plain,
( ~ sQ22_spl
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0) ),
inference(component_clause,[status(thm)],[f429]) ).
fof(f432,plain,
( ~ sQ12_spl
| sQ3_spl
| ~ sQ2_spl
| sQ21_spl
| sQ22_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f416,f418,f429,f424,f322,f325,f386]) ).
fof(f581,definition,
( sQ38_spl
<=> p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f583,plain,
( sQ38_spl
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)) ),
inference(component_clause,[status(thm)],[f581]) ).
fof(f586,plain,
( ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f425,f302]) ).
fof(f587,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f586]) ).
fof(f598,definition,
( sQ41_spl
<=> p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f600,plain,
( sQ41_spl
| ~ p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f612,plain,
( ~ sQ19_spl
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
inference(forward_demodulation,[status(thm)],[f309,f419]) ).
fof(f613,plain,
( sQ1_spl
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) ),
inference(resolution,[status(thm)],[f157,f321]) ).
fof(f614,plain,
( sQ1_spl
| sQ3_spl
| ~ sQ2_spl
| sQ21_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f613,f418,f424,f322,f325,f319]) ).
fof(f625,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f612,f333]) ).
fof(f626,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f625]) ).
fof(f671,plain,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0),
inference(paramodulation,[status(thm)],[f309,f211]) ).
fof(f707,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,f_ADD_(n0,n1))
| f_ADD_(n0,n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
inference(resolution,[status(thm)],[f671,f224]) ).
fof(f709,definition,
( sQ56_spl
<=> f_ADD_(n0,n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f710,plain,
( ~ sQ56_spl
| f_ADD_(n0,n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
inference(component_clause,[status(thm)],[f709]) ).
fof(f712,definition,
( sQ57_spl
<=> p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,f_ADD_(n0,n1)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f714,plain,
( sQ57_spl
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,f_ADD_(n0,n1)) ),
inference(component_clause,[status(thm)],[f712]) ).
fof(f715,plain,
( ~ sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f707,f709,f712]) ).
fof(f717,plain,
( ~ sQ56_spl
| n1 = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
inference(forward_demodulation,[status(thm)],[f229,f710]) ).
fof(f718,plain,
( ~ sQ56_spl
| sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f391]) ).
fof(f719,plain,
( ~ sQ56_spl
| sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f718]) ).
fof(f720,plain,
( sQ57_spl
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(forward_demodulation,[status(thm)],[f229,f714]) ).
fof(f866,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f430,f671]) ).
fof(f867,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f866]) ).
fof(f909,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f600,f227]) ).
fof(f910,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f909]) ).
fof(f911,plain,
( sQ38_spl
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(forward_demodulation,[status(thm)],[f309,f583]) ).
fof(f912,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f911,f227]) ).
fof(f913,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f912]) ).
fof(f995,definition,
( sQ96_spl
<=> p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f996,plain,
( ~ sQ96_spl
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(component_clause,[status(thm)],[f995]) ).
fof(f999,plain,
( ~ sQ96_spl
| sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f996,f720]) ).
fof(f1000,plain,
( ~ sQ96_spl
| sQ57_spl ),
inference(contradiction_clause,[status(thm)],[f999]) ).
fof(f1231,definition,
( sQ118_spl
<=> f_ADD_(n1,n1) = n0 ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1232,plain,
( ~ sQ118_spl
| f_ADD_(n1,n1) = n0 ),
inference(component_clause,[status(thm)],[f1231]) ).
fof(f1239,plain,
( ~ sQ118_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1232,f210]) ).
fof(f1240,plain,
~ sQ118_spl,
inference(contradiction_clause,[status(thm)],[f1239]) ).
fof(f1319,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f423,f227]) ).
fof(f1320,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f1319]) ).
fof(f1405,definition,
( sQ137_spl
<=> f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) = n0 ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1406,plain,
( ~ sQ137_spl
| f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) = n0 ),
inference(component_clause,[status(thm)],[f1405]) ).
fof(f1416,plain,
( ~ sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1406,f210]) ).
fof(f1417,plain,
~ sQ137_spl,
inference(contradiction_clause,[status(thm)],[f1416]) ).
fof(f1422,definition,
( sQ139_spl
<=> f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) = n0 ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1423,plain,
( ~ sQ139_spl
| f_ADD_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) = n0 ),
inference(component_clause,[status(thm)],[f1422]) ).
fof(f1430,plain,
( ~ sQ139_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1423,f210]) ).
fof(f1431,plain,
~ sQ139_spl,
inference(contradiction_clause,[status(thm)],[f1430]) ).
fof(f1497,plain,
( f_SUB_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1),n1) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| def_89(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(paramodulation,[status(thm)],[f309,f305]) ).
fof(f1499,definition,
( sQ148_spl
<=> def_89(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1500,plain,
( ~ sQ148_spl
| def_89(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(component_clause,[status(thm)],[f1499]) ).
fof(f1502,definition,
( sQ149_spl
<=> f_SUB_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1),n1) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1503,plain,
( ~ sQ149_spl
| f_SUB_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1),n1) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) ),
inference(component_clause,[status(thm)],[f1502]) ).
fof(f1505,plain,
( sQ149_spl
| sQ148_spl ),
inference(split_clause,[status(thm)],[f1497,f1499,f1502]) ).
fof(f1508,plain,
( ~ sQ149_spl
| f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) ),
inference(forward_demodulation,[status(thm)],[f309,f1503]) ).
fof(f1553,plain,
( ~ sQ148_spl
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(resolution,[status(thm)],[f1500,f216]) ).
fof(f1554,plain,
( ~ sQ148_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f1553,f995,f1499]) ).
fof(f1700,definition,
( sQ166_spl
<=> p_LES_EQU_(f_ADD_(n0,n1),n1) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f1702,plain,
( sQ166_spl
| ~ p_LES_EQU_(f_ADD_(n0,n1),n1) ),
inference(component_clause,[status(thm)],[f1700]) ).
fof(f1707,plain,
( sQ166_spl
| ~ p_LES_EQU_(n1,n1) ),
inference(forward_demodulation,[status(thm)],[f229,f1702]) ).
fof(f1708,plain,
( sQ166_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1707,f227]) ).
fof(f1709,plain,
sQ166_spl,
inference(contradiction_clause,[status(thm)],[f1708]) ).
fof(f2241,plain,
( ~ sQ149_spl
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)) ),
inference(paramodulation,[status(thm)],[f1508,f212]) ).
fof(f2252,plain,
( ~ sQ149_spl
| sQ22_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f2241,f319,f429,f1502]) ).
fof(f2253,plain,
$false,
inference(sat_refutation,[status(thm)],[f330,f332,f392,f432,f587,f614,f626,f715,f719,f867,f910,f913,f1000,f1240,f1320,f1417,f1431,f1505,f1554,f1709,f2252]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV022-2 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 20:48:34 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.51 % Refutation found
% 0.09/0.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.54 % Elapsed time: 0.165423 seconds
% 0.09/0.54 % CPU time: 1.095168 seconds
% 0.09/0.54 % Total memory used: 127.088 MB
% 0.09/0.54 % Net memory used: 124.031 MB
%------------------------------------------------------------------------------