%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV022-2 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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:46:43 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV022-2 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n002.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Sun Sep 20 20:51:16 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 0.14/0.52 % Refutation found
% 0.14/0.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.52 fof(f4,axiom,(
% 0.14/0.52 (![T_0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(T_0) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_0) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f7,axiom,(
% 0.14/0.52 (![T_3]: (( p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_3))| fwork_DOTfifo_DOTrtl_DOTint__level_(T_3) != n0 ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f8,axiom,(
% 0.14/0.52 (![T_4]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_4))| fwork_DOTfifo_DOTrtl_DOTint__level_(T_4) = n0 ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f17,axiom,(
% 0.14/0.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n1)| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13)) ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f22,axiom,(
% 0.14/0.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_13)| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13)) ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f50,axiom,(
% 0.14/0.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_13)| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13)) ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f58,axiom,(
% 0.14/0.52 (![X_80]: (f_ADD_(X_80,n1) != n0 ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f59,axiom,(
% 0.14/0.52 (![X_81]: (~ p_LES_EQU_(f_ADD_(X_81,n1),n0) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f60,axiom,(
% 0.14/0.52 (![X_82]: (( ~ p_LES_EQU_(X_82,f_SUB_(X_82,n1))| p_LES_EQU_(X_82,n0) ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f62,axiom,(
% 0.14/0.52 (![Y_84,X_83,Z_85]: (( def_89(Y_84,X_83)| f_ADD_(Z_85,Y_84) != X_83| f_SUB_(X_83,Y_84) = Z_85 ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f64,axiom,(
% 0.14/0.52 (![X_83,Y_84]: (( p_LES_EQU_(X_83,Y_84)| ~ def_89(Y_84,X_83) ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f71,axiom,(
% 0.14/0.52 (![X_101,Y_102]: (( f_ADD_(X_101,n1) = Y_102| ~ p_LES_EQU_(Y_102,f_ADD_(X_101,n1))| p_LES_EQU_(Y_102,X_101) ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f72,axiom,(
% 0.14/0.52 (![X_103]: (( ~ p_LES_EQU_(X_103,n0)| X_103 = n0 ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f75,axiom,(
% 0.14/0.52 (![X_107,Y_108]: (( X_107 = Y_108| f_ADD_(X_107,n1) != f_ADD_(Y_108,n1) ) ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f76,axiom,(
% 0.14/0.52 (![X_109]: (f_ADD_(n0,X_109) = X_109 ))),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f134,negated_conjecture,(
% 0.14/0.52 f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f135,negated_conjecture,(
% 0.14/0.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)) ),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f136,negated_conjecture,(
% 0.14/0.52 ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)) ),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f137,negated_conjecture,(
% 0.14/0.52 ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f138,negated_conjecture,(
% 0.14/0.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) != fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
% 0.14/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f142,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=fwork_DOTfifo_DOTrtl_DOTint__level_(X0))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.52 fof(f145,plain,(
% 0.14/0.52 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|~fwork_DOTfifo_DOTrtl_DOTint__level_(X0)=n0)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/0.52 fof(f146,plain,(
% 0.14/0.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|fwork_DOTfifo_DOTrtl_DOTint__level_(X0)=n0)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.52 fof(f157,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n1)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f17])).
% 0.14/0.52 fof(f164,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTint__level_(X0)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/0.52 fof(f200,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTint__level_(X0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/0.52 fof(f210,plain,(
% 0.14/0.52 ![X0]: (~f_ADD_(X0,n1)=n0)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f58])).
% 0.14/0.52 fof(f211,plain,(
% 0.14/0.52 ![X0]: (~p_LES_EQU_(f_ADD_(X0,n1),n0))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f59])).
% 0.14/0.52 fof(f212,plain,(
% 0.14/0.52 ![X0]: (~p_LES_EQU_(X0,f_SUB_(X0,n1))|p_LES_EQU_(X0,n0))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f60])).
% 0.14/0.52 fof(f214,plain,(
% 0.14/0.52 ![X0,X1,X2]: (def_89(X0,X1)|~f_ADD_(X2,X0)=X1|f_SUB_(X1,X0)=X2)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f62])).
% 0.14/0.52 fof(f216,plain,(
% 0.14/0.52 ![X0,X1]: (p_LES_EQU_(X0,X1)|~def_89(X1,X0))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f64])).
% 0.14/0.52 fof(f224,plain,(
% 0.14/0.52 ![X0,X1]: (f_ADD_(X0,n1)=X1|~p_LES_EQU_(X1,f_ADD_(X0,n1))|p_LES_EQU_(X1,X0))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f71])).
% 0.14/0.52 fof(f225,plain,(
% 0.14/0.52 ![X0]: (~p_LES_EQU_(X0,n0)|X0=n0)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/0.52 fof(f228,plain,(
% 0.14/0.52 ![X0,X1]: (X0=X1|~f_ADD_(X0,n1)=f_ADD_(X1,n1))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f75])).
% 0.14/0.52 fof(f229,plain,(
% 0.14/0.52 ![X0]: (f_ADD_(n0,X0)=X0)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f76])).
% 0.14/0.52 fof(f299,plain,(
% 0.14/0.52 f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)=fwork_DOTfifo_DOTrtl_DOTfifo__length_),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f134])).
% 0.14/0.52 fof(f300,plain,(
% 0.14/0.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f135])).
% 0.14/0.52 fof(f301,plain,(
% 0.14/0.52 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f136])).
% 0.14/0.52 fof(f302,plain,(
% 0.14/0.52 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f137])).
% 0.14/0.52 fof(f303,plain,(
% 0.14/0.52 ~fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTfifo__length_),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/0.52 fof(f306,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n1)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f142,f157])).
% 0.14/0.52 fof(f307,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(X0),n1)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f142,f306])).
% 0.14/0.52 fof(f308,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(X0),n1)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f142,f307])).
% 0.14/0.52 fof(f309,plain,(
% 0.14/0.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/0.52 inference(resolution,[status(thm)],[f308,f300])).
% 0.14/0.52 fof(f310,definition,(
% 0.14/0.52 sQ0_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f311,plain,(
% 0.14/0.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)|~sQ0_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f310])).
% 0.14/0.52 fof(f313,definition,(
% 0.14/0.52 sQ1_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f314,plain,(
% 0.14/0.52 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))|~sQ1_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f313])).
% 0.14/0.52 fof(f316,definition,(
% 0.14/0.52 sQ2_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f317,plain,(
% 0.14/0.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))|~sQ2_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f316])).
% 0.14/0.52 fof(f319,definition,(
% 0.14/0.52 sQ3_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f320,plain,(
% 0.14/0.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))|~sQ3_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f319])).
% 0.14/0.52 fof(f322,plain,(
% 0.14/0.52 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl),
% 0.14/0.52 inference(split_clause,[status(thm)],[f309,f310,f313,f316,f319])).
% 0.14/0.52 fof(f323,plain,(
% 0.14/0.52 $false|~sQ3_spl),
% 0.14/0.52 inference(forward_subsumption_resolution,[status(thm)],[f320,f301])).
% 0.14/0.52 fof(f324,plain,(
% 0.14/0.52 ~sQ3_spl),
% 0.14/0.52 inference(contradiction_clause,[status(thm)],[f323])).
% 0.14/0.52 fof(f325,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTint__level_(X0)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f142,f164])).
% 0.14/0.52 fof(f326,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(X0)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f142,f325])).
% 0.14/0.52 fof(f327,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(X0)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f142,f326])).
% 0.14/0.52 fof(f333,plain,(
% 0.14/0.52 $false|~sQ2_spl),
% 0.14/0.52 inference(forward_subsumption_resolution,[status(thm)],[f317,f302])).
% 0.14/0.52 fof(f334,plain,(
% 0.14/0.52 ~sQ2_spl),
% 0.14/0.52 inference(contradiction_clause,[status(thm)],[f333])).
% 0.14/0.52 fof(f335,plain,(
% 0.14/0.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTfifo__length_|~sQ0_spl),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f299,f311])).
% 0.14/0.52 fof(f336,plain,(
% 0.14/0.52 $false|~sQ0_spl),
% 0.14/0.52 inference(forward_subsumption_resolution,[status(thm)],[f335,f303])).
% 0.14/0.52 fof(f337,plain,(
% 0.14/0.52 ~sQ0_spl),
% 0.14/0.52 inference(contradiction_clause,[status(thm)],[f336])).
% 0.14/0.52 fof(f340,definition,(
% 0.14/0.52 sQ4_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f341,plain,(
% 0.14/0.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~sQ4_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f340])).
% 0.14/0.52 fof(f360,plain,(
% 0.14/0.52 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|~fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=n0)),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f142,f145])).
% 0.14/0.52 fof(f362,plain,(
% 0.14/0.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(f_ADD_(t_206,n1)))|~fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n0|~sQ4_spl),
% 0.14/0.52 inference(paramodulation,[status(thm)],[f341,f360])).
% 0.14/0.52 fof(f366,definition,(
% 0.14/0.52 sQ7_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(f_ADD_(t_206,n1))))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f367,plain,(
% 0.14/0.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(f_ADD_(t_206,n1)))|~sQ7_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f366])).
% 0.14/0.52 fof(f369,definition,(
% 0.14/0.52 sQ8_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n0)),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f372,plain,(
% 0.14/0.52 sQ7_spl|~sQ8_spl|~sQ4_spl),
% 0.14/0.52 inference(split_clause,[status(thm)],[f362,f366,f369,f340])).
% 0.14/0.52 fof(f409,plain,(
% 0.14/0.52 ~fwork_DOTfifo_DOTrtl_DOTfifo__length_=n0),
% 0.14/0.52 inference(paramodulation,[status(thm)],[f299,f210])).
% 0.14/0.52 fof(f410,plain,(
% 0.14/0.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=n0)),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f142,f146])).
% 0.14/0.52 fof(f411,plain,(
% 0.14/0.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=n0|~sQ7_spl),
% 0.14/0.52 inference(resolution,[status(thm)],[f410,f367])).
% 0.14/0.52 fof(f415,plain,(
% 0.14/0.52 n0=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~sQ7_spl|~sQ4_spl),
% 0.14/0.52 inference(backward_demodulation,[status(thm)],[f411,f341])).
% 0.14/0.52 fof(f430,definition,(
% 0.14/0.52 sQ18_spl <=> (n0=fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f431,plain,(
% 0.14/0.52 n0=fwork_DOTfifo_DOTrtl_DOTfifo__length_|~sQ18_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f430])).
% 0.14/0.52 fof(f435,definition,(
% 0.14/0.52 sQ19_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f436,plain,(
% 0.14/0.52 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)|~sQ19_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f435])).
% 0.14/0.52 fof(f440,plain,(
% 0.14/0.52 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)|~sQ7_spl|~sQ4_spl|~sQ1_spl),
% 0.14/0.52 inference(backward_demodulation,[status(thm)],[f415,f314])).
% 0.14/0.52 fof(f460,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTint__level_(X0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f142,f200])).
% 0.14/0.52 fof(f462,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(X0)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(backward_subsumption_resolution,[status(thm)],[f327,f463])).
% 0.14/0.52 fof(f463,plain,(
% 0.14/0.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(X0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.52 inference(forward_demodulation,[status(thm)],[f142,f460])).
% 0.14/0.52 fof(f533,plain,(
% 0.14/0.52 $false|~sQ18_spl),
% 0.14/0.52 inference(forward_subsumption_resolution,[status(thm)],[f431,f409])).
% 0.14/0.52 fof(f534,plain,(
% 0.14/0.52 ~sQ18_spl),
% 0.14/0.52 inference(contradiction_clause,[status(thm)],[f533])).
% 0.14/0.52 fof(f601,plain,(
% 0.14/0.53 fwork_DOTfifo_DOTrtl_DOTfifo__length_=n0|~sQ7_spl|~sQ4_spl|~sQ1_spl),
% 0.14/0.53 inference(resolution,[status(thm)],[f225,f440])).
% 0.14/0.53 fof(f603,plain,(
% 0.14/0.53 sQ18_spl|~sQ7_spl|~sQ4_spl|~sQ1_spl),
% 0.14/0.53 inference(split_clause,[status(thm)],[f601,f430,f366,f340,f313])).
% 0.14/0.53 fof(f658,plain,(
% 0.14/0.53 ![X0]: (X0=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~f_ADD_(X0,n1)=fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/0.53 inference(paramodulation,[status(thm)],[f299,f228])).
% 0.14/0.53 fof(f673,plain,(
% 0.14/0.53 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))|~sQ1_spl),
% 0.14/0.53 inference(resolution,[status(thm)],[f462,f314])).
% 0.14/0.53 fof(f674,plain,(
% 0.14/0.53 sQ4_spl|sQ2_spl|sQ3_spl|~sQ1_spl),
% 0.14/0.53 inference(split_clause,[status(thm)],[f673,f340,f316,f319,f313])).
% 0.14/0.53 fof(f677,plain,(
% 0.14/0.53 ![X0]: (f_ADD_(n0,n1)=X0|~p_LES_EQU_(X0,n1)|p_LES_EQU_(X0,n0))),
% 0.14/0.53 inference(paramodulation,[status(thm)],[f229,f224])).
% 0.14/0.53 fof(f679,plain,(
% 0.14/0.53 ![X0]: (n1=X0|~p_LES_EQU_(X0,n1)|p_LES_EQU_(X0,n0))),
% 0.14/0.53 inference(forward_demodulation,[status(thm)],[f229,f677])).
% 0.14/0.53 fof(f712,plain,(
% 0.14/0.53 n0=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~n1=fwork_DOTfifo_DOTrtl_DOTfifo__length_),
% 0.14/0.53 inference(paramodulation,[status(thm)],[f229,f658])).
% 0.14/0.53 fof(f717,definition,(
% 0.14/0.53 sQ53_spl <=> (n1=fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/0.53 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.14/0.53 fof(f720,plain,(
% 0.14/0.53 sQ8_spl|~sQ53_spl),
% 0.14/0.53 inference(split_clause,[status(thm)],[f712,f369,f717])).
% 0.14/0.53 fof(f727,plain,(
% 0.14/0.53 ~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)),
% 0.14/0.53 inference(paramodulation,[status(thm)],[f299,f211])).
% 0.14/0.53 fof(f1305,plain,(
% 0.14/0.53 def_89(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)),
% 0.14/0.53 inference(resolution,[status(thm)],[f214,f299])).
% 0.14/0.53 fof(f1312,definition,(
% 0.14/0.53 sQ119_spl <=> (def_89(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_))),
% 0.14/0.53 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.14/0.53 fof(f1313,plain,(
% 0.14/0.53 def_89(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~sQ119_spl),
% 0.14/0.53 inference(component_clause,[status(thm)],[f1312])).
% 0.14/0.53 fof(f1315,definition,(
% 0.14/0.53 sQ120_spl <=> (f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))),
% 0.14/0.53 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.14/0.53 fof(f1316,plain,(
% 0.14/0.53 f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~sQ120_spl),
% 0.14/0.53 inference(component_clause,[status(thm)],[f1315])).
% 0.14/0.53 fof(f1318,plain,(
% 0.14/0.53 sQ119_spl|sQ120_spl),
% 0.14/0.53 inference(split_clause,[status(thm)],[f1305,f1312,f1315])).
% 0.14/0.53 fof(f1334,plain,(
% 0.14/0.53 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)|~sQ119_spl),
% 0.14/0.53 inference(resolution,[status(thm)],[f1313,f216])).
% 0.14/0.53 fof(f1853,plain,(
% 0.14/0.53 ~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)|~sQ120_spl),
% 0.14/0.53 inference(paramodulation,[status(thm)],[f1316,f212])).
% 0.14/0.53 fof(f1857,plain,(
% 0.14/0.53 ~sQ1_spl|sQ19_spl|~sQ120_spl),
% 0.14/0.53 inference(split_clause,[status(thm)],[f1853,f313,f435,f1315])).
% 0.14/0.53 fof(f1868,plain,(
% 0.14/0.53 $false|~sQ19_spl),
% 0.14/0.53 inference(forward_subsumption_resolution,[status(thm)],[f436,f727])).
% 0.14/0.53 fof(f1869,plain,(
% 0.14/0.53 ~sQ19_spl),
% 0.14/0.53 inference(contradiction_clause,[status(thm)],[f1868])).
% 0.14/0.53 fof(f1879,plain,(
% 0.14/0.53 n1=fwork_DOTfifo_DOTrtl_DOTfifo__length_|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)|~sQ119_spl),
% 0.14/0.53 inference(resolution,[status(thm)],[f1334,f679])).
% 0.14/0.53 fof(f1884,plain,(
% 0.14/0.53 sQ53_spl|sQ19_spl|~sQ119_spl),
% 0.14/0.53 inference(split_clause,[status(thm)],[f1879,f717,f435,f1312])).
% 0.14/0.53 fof(f1887,plain,(
% 0.14/0.53 $false),
% 0.14/0.53 inference(sat_refutation,[status(thm)],[f322,f324,f334,f337,f372,f534,f603,f674,f720,f1318,f1857,f1869,f1884])).
% 0.14/0.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.41/0.54 % Elapsed time: 0.169686 seconds
% 0.41/0.54 % CPU time: 1.064022 seconds
% 0.41/0.54 % Total memory used: 125.800 MB
% 0.41/0.54 % Net memory used: 123.472 MB
%------------------------------------------------------------------------------