%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV023-2 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV023-2 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.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:52:05 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.40 fof(f4,axiom,(
% 0.14/0.40 (![T_0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(T_0) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_0) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f7,axiom,(
% 0.14/0.40 (![T_3]: (( p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_3))| fwork_DOTfifo_DOTrtl_DOTint__level_(T_3) != n0 ) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f42,axiom,(
% 0.14/0.40 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(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.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f58,axiom,(
% 0.14/0.40 (![X_80]: (f_ADD_(X_80,n1) != n0 ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f62,axiom,(
% 0.14/0.40 (![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.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f63,axiom,(
% 0.14/0.40 (![X_83,Y_84]: (( X_83 != Y_84| ~ def_89(Y_84,X_83) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f72,axiom,(
% 0.14/0.40 (![X_103]: (( ~ p_LES_EQU_(X_103,n0)| X_103 = n0 ) ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f76,axiom,(
% 0.14/0.40 (![X_109]: (f_ADD_(n0,X_109) = X_109 ))),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f134,negated_conjecture,(
% 0.14/0.40 fwork_DOTfifo_DOTrtl_DOTlevel_(t_206) = n1 ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f135,negated_conjecture,(
% 0.14/0.40 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f136,negated_conjecture,(
% 0.14/0.40 ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f137,negated_conjecture,(
% 0.14/0.40 ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f138,negated_conjecture,(
% 0.14/0.40 ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(f_ADD_(t_206,n1))) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f142,plain,(
% 0.14/0.40 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=fwork_DOTfifo_DOTrtl_DOTint__level_(X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.40 fof(f145,plain,(
% 0.14/0.40 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|~fwork_DOTfifo_DOTrtl_DOTint__level_(X0)=n0)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/0.40 fof(f190,plain,(
% 0.14/0.40 ![X0]: (fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))=f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(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.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.14/0.40 fof(f210,plain,(
% 0.14/0.40 ![X0]: (~f_ADD_(X0,n1)=n0)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f58])).
% 0.14/0.40 fof(f214,plain,(
% 0.14/0.40 ![X0,X1,X2]: (def_89(X0,X1)|~f_ADD_(X2,X0)=X1|f_SUB_(X1,X0)=X2)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f62])).
% 0.14/0.40 fof(f215,plain,(
% 0.14/0.40 ![X0,X1]: (~X0=X1|~def_89(X1,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.14/0.40 fof(f225,plain,(
% 0.14/0.40 ![X0]: (~p_LES_EQU_(X0,n0)|X0=n0)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/0.40 fof(f229,plain,(
% 0.14/0.40 ![X0]: (f_ADD_(n0,X0)=X0)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f76])).
% 0.14/0.40 fof(f299,plain,(
% 0.14/0.40 fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n1),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f134])).
% 0.14/0.40 fof(f300,plain,(
% 0.14/0.40 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f135])).
% 0.14/0.40 fof(f301,plain,(
% 0.14/0.40 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f136])).
% 0.14/0.40 fof(f302,plain,(
% 0.14/0.40 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f137])).
% 0.14/0.40 fof(f303,plain,(
% 0.14/0.40 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(f_ADD_(t_206,n1)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/0.40 fof(f305,plain,(
% 0.14/0.40 ![X0,X1]: (def_89(X0,f_ADD_(X1,X0))|f_SUB_(f_ADD_(X1,X0),X0)=X1)),
% 0.14/0.40 inference(destructive_equality_resolution,[status(thm)],[f214])).
% 0.14/0.40 fof(f306,plain,(
% 0.14/0.40 ![X0]: (~def_89(X0,X0))),
% 0.14/0.40 inference(destructive_equality_resolution,[status(thm)],[f215])).
% 0.14/0.40 fof(f309,plain,(
% 0.14/0.40 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|~fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=n0)),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f142,f145])).
% 0.14/0.40 fof(f326,plain,(
% 0.14/0.40 ~fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=n0),
% 0.14/0.40 inference(resolution,[status(thm)],[f303,f309])).
% 0.14/0.40 fof(f327,plain,(
% 0.14/0.40 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(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.40 inference(forward_demodulation,[status(thm)],[f142,f190])).
% 0.14/0.40 fof(f328,plain,(
% 0.14/0.40 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=f_SUB_(fwork_DOTfifo_DOTrtl_DOTlevel_(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.40 inference(forward_demodulation,[status(thm)],[f142,f327])).
% 0.14/0.40 fof(f329,plain,(
% 0.14/0.40 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=f_SUB_(fwork_DOTfifo_DOTrtl_DOTlevel_(X0),n1)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(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.40 inference(forward_demodulation,[status(thm)],[f142,f328])).
% 0.14/0.40 fof(f330,plain,(
% 0.14/0.40 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_SUB_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/0.40 inference(resolution,[status(thm)],[f329,f300])).
% 0.14/0.40 fof(f331,plain,(
% 0.14/0.40 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_SUB_(n1,n1)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f299,f330])).
% 0.14/0.40 fof(f332,plain,(
% 0.14/0.40 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_SUB_(n1,n1)|p_LES_EQU_(n1,n0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f299,f331])).
% 0.14/0.40 fof(f333,plain,(
% 0.14/0.40 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_SUB_(n1,n1)|p_LES_EQU_(n1,n0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f332,f302])).
% 0.14/0.40 fof(f370,plain,(
% 0.14/0.40 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_SUB_(n1,n1)|p_LES_EQU_(n1,n0)),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f333,f301])).
% 0.14/0.40 fof(f396,plain,(
% 0.14/0.40 ~n1=n0),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f229,f210])).
% 0.14/0.40 fof(f534,plain,(
% 0.14/0.40 n1=n0|fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_SUB_(n1,n1)),
% 0.14/0.40 inference(resolution,[status(thm)],[f225,f370])).
% 0.14/0.40 fof(f537,plain,(
% 0.14/0.40 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_SUB_(n1,n1)),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f534,f396])).
% 0.14/0.40 fof(f604,plain,(
% 0.14/0.40 ~f_SUB_(n1,n1)=n0),
% 0.14/0.40 inference(backward_demodulation,[status(thm)],[f537,f326])).
% 0.14/0.40 fof(f758,plain,(
% 0.14/0.40 ![X0]: (def_89(X0,X0)|f_SUB_(f_ADD_(n0,X0),X0)=n0)),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f229,f305])).
% 0.14/0.40 fof(f762,plain,(
% 0.14/0.40 ![X0]: (def_89(X0,X0)|f_SUB_(X0,X0)=n0)),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f229,f758])).
% 0.14/0.40 fof(f763,plain,(
% 0.14/0.40 ![X0]: (f_SUB_(X0,X0)=n0)),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f762,f306])).
% 0.14/0.40 fof(f773,plain,(
% 0.14/0.40 ~n0=n0),
% 0.14/0.40 inference(backward_demodulation,[status(thm)],[f763,f604])).
% 0.14/0.40 fof(f776,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(trivial_equality_resolution,[status(thm)],[f773])).
% 0.14/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.43 % Elapsed time: 0.064168 seconds
% 0.14/0.43 % CPU time: 0.233111 seconds
% 0.14/0.43 % Total memory used: 47.359 MB
% 0.14/0.43 % Net memory used: 47.052 MB
%------------------------------------------------------------------------------