%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV021-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 : n013.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:42 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV021-2 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n013.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:48:06 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.41 fof(f7,axiom,(
% 0.14/0.41 (![T_3]: (( p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_3))| fwork_DOTfifo_DOTrtl_DOTint__level_(T_3) != n0 ) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f13,axiom,(
% 0.14/0.41 (![T_5]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_5,n1)))| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f33,axiom,(
% 0.14/0.41 (![T_13]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1)))| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)| ~ 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.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f45,axiom,(
% 0.14/0.41 (![T_13]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1)))| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(T_13),n0)| ~ 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.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f59,axiom,(
% 0.14/0.41 (![X_81]: (~ p_LES_EQU_(f_ADD_(X_81,n1),n0) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f67,axiom,(
% 0.14/0.41 (![Y_93,X_92]: (( Y_93 = X_92| ~ p_LES_EQU_(X_92,Y_93)| p_LES_EQU_(f_ADD_(X_92,n1),Y_93) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f134,negated_conjecture,(
% 0.14/0.41 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(t_206,n1))) ),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f135,negated_conjecture,(
% 0.14/0.41 ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)) ),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f136,negated_conjecture,(
% 0.14/0.41 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f137,negated_conjecture,(
% 0.14/0.41 ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(t_206)) ),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f144,plain,(
% 0.14/0.41 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|~fwork_DOTfifo_DOTrtl_DOTint__level_(X0)=n0)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/0.41 fof(f150,plain,(
% 0.14/0.41 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/0.41 fof(f177,plain,(
% 0.14/0.41 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f33])).
% 0.14/0.41 fof(f193,plain,(
% 0.14/0.41 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.41 fof(f210,plain,(
% 0.14/0.41 ![X0]: (~p_LES_EQU_(f_ADD_(X0,n1),n0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.14/0.41 fof(f218,plain,(
% 0.14/0.41 ![X0,X1]: (X0=X1|~p_LES_EQU_(X1,X0)|p_LES_EQU_(f_ADD_(X1,n1),X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f67])).
% 0.14/0.41 fof(f298,plain,(
% 0.14/0.41 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(t_206,n1)))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f134])).
% 0.14/0.41 fof(f299,plain,(
% 0.14/0.41 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f135])).
% 0.14/0.41 fof(f300,plain,(
% 0.14/0.41 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f136])).
% 0.14/0.41 fof(f301,plain,(
% 0.14/0.41 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(t_206))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f137])).
% 0.14/0.41 fof(f313,definition,(
% 0.14/0.41 sQ1_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f315,plain,(
% 0.14/0.41 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))|sQ1_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f313])).
% 0.14/0.41 fof(f341,definition,(
% 0.14/0.41 sQ8_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n0))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f342,plain,(
% 0.14/0.41 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n0)|~sQ8_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f341])).
% 0.14/0.41 fof(f344,definition,(
% 0.14/0.41 sQ9_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f345,plain,(
% 0.14/0.41 p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))|~sQ9_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f344])).
% 0.14/0.41 fof(f348,plain,(
% 0.14/0.41 $false|~sQ9_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f345,f299])).
% 0.14/0.41 fof(f349,plain,(
% 0.14/0.41 ~sQ9_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f348])).
% 0.14/0.41 fof(f471,plain,(
% 0.14/0.41 n0=fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)|p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1),n0)|~sQ8_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f342,f218])).
% 0.14/0.41 fof(f473,definition,(
% 0.14/0.41 sQ30_spl <=> (n0=fwork_DOTfifo_DOTrtl_DOTint__level_(t_206))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f474,plain,(
% 0.14/0.41 n0=fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)|~sQ30_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f473])).
% 0.14/0.41 fof(f476,definition,(
% 0.14/0.41 sQ31_spl <=> (p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1),n0))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f477,plain,(
% 0.14/0.41 p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1),n0)|~sQ31_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f476])).
% 0.14/0.41 fof(f479,plain,(
% 0.14/0.41 sQ30_spl|sQ31_spl|~sQ8_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f471,f473,f476,f341])).
% 0.14/0.41 fof(f480,plain,(
% 0.14/0.41 p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(t_206))|~sQ30_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f474,f144])).
% 0.14/0.41 fof(f482,plain,(
% 0.14/0.41 $false|~sQ30_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f480,f301])).
% 0.14/0.41 fof(f483,plain,(
% 0.14/0.41 ~sQ30_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f482])).
% 0.14/0.41 fof(f520,plain,(
% 0.14/0.41 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0)))),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f177,f150])).
% 0.14/0.41 fof(f735,plain,(
% 0.14/0.41 $false|~sQ31_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f477,f210])).
% 0.14/0.41 fof(f736,plain,(
% 0.14/0.41 ~sQ31_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f735])).
% 0.14/0.41 fof(f835,plain,(
% 0.14/0.41 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f193,f520])).
% 0.14/0.41 fof(f836,plain,(
% 0.14/0.41 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/0.41 inference(resolution,[status(thm)],[f835,f298])).
% 0.14/0.41 fof(f841,plain,(
% 0.14/0.41 sQ8_spl|~sQ1_spl|sQ9_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f836,f341,f313,f344])).
% 0.14/0.41 fof(f846,plain,(
% 0.14/0.41 $false|sQ1_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f315,f300])).
% 0.14/0.41 fof(f847,plain,(
% 0.14/0.41 sQ1_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f846])).
% 0.14/0.41 fof(f848,plain,(
% 0.14/0.41 $false),
% 0.14/0.41 inference(sat_refutation,[status(thm)],[f349,f479,f483,f736,f841,f847])).
% 0.14/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.43 % Elapsed time: 0.071493 seconds
% 0.14/0.43 % CPU time: 0.215001 seconds
% 0.14/0.43 % Total memory used: 110.939 MB
% 0.14/0.43 % Net memory used: 110.727 MB
%------------------------------------------------------------------------------