%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV016-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 : n019.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:41 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV016-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.10/0.35 % Computer : n019.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 20:48:49 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.50 % Refutation found
% 0.10/0.50 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.50 fof(f4,axiom,(
% 0.10/0.50 (![T_0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(T_0) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_0) ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f8,axiom,(
% 0.10/0.50 (![T_4]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_4))| fwork_DOTfifo_DOTrtl_DOTint__level_(T_4) = n0 ) ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f17,axiom,(
% 0.10/0.50 (![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.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f22,axiom,(
% 0.10/0.50 (![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.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f30,axiom,(
% 0.10/0.50 (![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_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.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f35,axiom,(
% 0.10/0.50 (![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_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.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f58,axiom,(
% 0.10/0.50 (![X_80]: (f_ADD_(X_80,n1) != n0 ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f59,axiom,(
% 0.10/0.50 (![X_81]: (~ p_LES_EQU_(f_ADD_(X_81,n1),n0) ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f61,axiom,(
% 0.10/0.50 (![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.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f63,axiom,(
% 0.10/0.50 (![X_83,Y_84]: (( X_83 != Y_84| ~ def_89(Y_84,X_83) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f65,axiom,(
% 0.10/0.50 (![Y_91,X_90]: (( ~ p_LES_EQU_(f_ADD_(Y_91,n1),f_ADD_(X_90,n1))| p_LES_EQU_(Y_91,X_90) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f67,axiom,(
% 0.10/0.50 (![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.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f69,axiom,(
% 0.10/0.50 (![X_96,Y_97]: (( X_96 = Y_97| ~ p_LES_EQU_(X_96,Y_97)| ~ p_LES_EQU_(Y_97,X_96) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f74,axiom,(
% 0.10/0.50 (![X_106]: (p_LES_EQU_(X_106,X_106) ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f76,axiom,(
% 0.10/0.50 (![X_109]: (f_ADD_(n0,X_109) = X_109 ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f99,axiom,(
% 0.10/0.50 (![B_156,A_155]: (( ~ p__pred_(B_156)| p__pred_(A_155)| ~ p__pred_(f__equiv_(A_155,B_156)) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f100,axiom,(
% 0.10/0.50 (![B_156,A_155]: (( ~ p__pred_(B_156)| ~ p__pred_(A_155)| p__pred_(f__equiv_(A_155,B_156)) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f116,axiom,(
% 0.10/0.50 (![A_181,B_182]: (( p__pred_(A_181)| p__pred_(f__nand_(A_181,B_182)) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f134,negated_conjecture,(
% 0.10/0.50 p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)) ),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f135,negated_conjecture,(
% 0.10/0.50 ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)) ),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f136,negated_conjecture,(
% 0.10/0.50 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)) ),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f137,negated_conjecture,(
% 0.10/0.50 p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(f_ADD_(t_206,n1))) ),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f138,negated_conjecture,(
% 0.10/0.50 ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0) ),
% 0.10/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f142,plain,(
% 0.10/0.50 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=fwork_DOTfifo_DOTrtl_DOTint__level_(X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.50 fof(f146,plain,(
% 0.10/0.50 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|fwork_DOTfifo_DOTrtl_DOTint__level_(X0)=n0)),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.50 fof(f157,plain,(
% 0.10/0.50 ![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.10/0.50 inference(cnf_transformation,[status(thm)],[f17])).
% 0.10/0.50 fof(f164,plain,(
% 0.10/0.50 ![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.10/0.50 inference(cnf_transformation,[status(thm)],[f22])).
% 0.10/0.50 fof(f174,plain,(
% 0.10/0.50 ![X0]: (fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTint__level_(X0)|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.10/0.50 inference(cnf_transformation,[status(thm)],[f30])).
% 0.10/0.50 fof(f180,plain,(
% 0.10/0.50 ![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_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.10/0.50 inference(cnf_transformation,[status(thm)],[f35])).
% 0.10/0.50 fof(f210,plain,(
% 0.10/0.50 ![X0]: (~f_ADD_(X0,n1)=n0)),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f58])).
% 0.10/0.50 fof(f211,plain,(
% 0.10/0.50 ![X0]: (~p_LES_EQU_(f_ADD_(X0,n1),n0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f59])).
% 0.10/0.50 fof(f213,plain,(
% 0.10/0.50 ![X0,X1,X2]: (def_89(X0,X1)|f_ADD_(X2,X0)=X1|~f_SUB_(X1,X0)=X2)),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f61])).
% 0.10/0.50 fof(f215,plain,(
% 0.10/0.50 ![X0,X1]: (~X0=X1|~def_89(X1,X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f63])).
% 0.10/0.50 fof(f217,plain,(
% 0.10/0.50 ![X0,X1]: (~p_LES_EQU_(f_ADD_(X0,n1),f_ADD_(X1,n1))|p_LES_EQU_(X0,X1))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f65])).
% 0.10/0.50 fof(f219,plain,(
% 0.10/0.50 ![X0,X1]: (X0=X1|~p_LES_EQU_(X1,X0)|p_LES_EQU_(f_ADD_(X1,n1),X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f67])).
% 0.10/0.50 fof(f221,plain,(
% 0.10/0.50 ![X0,X1]: (X0=X1|~p_LES_EQU_(X0,X1)|~p_LES_EQU_(X1,X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f69])).
% 0.10/0.50 fof(f227,plain,(
% 0.10/0.50 ![X0]: (p_LES_EQU_(X0,X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f74])).
% 0.10/0.50 fof(f229,plain,(
% 0.10/0.50 ![X0]: (f_ADD_(n0,X0)=X0)),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f76])).
% 0.10/0.50 fof(f256,plain,(
% 0.10/0.50 ![X0,X1]: (~p__pred_(X0)|p__pred_(X1)|~p__pred_(f__equiv_(X1,X0)))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f99])).
% 0.10/0.50 fof(f257,plain,(
% 0.10/0.50 ![X0,X1]: (~p__pred_(X0)|~p__pred_(X1)|p__pred_(f__equiv_(X1,X0)))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f100])).
% 0.10/0.50 fof(f278,plain,(
% 0.10/0.50 ![A_181]: (p__pred_(A_181)|(![B_182]: p__pred_(f__nand_(A_181,B_182))))),
% 0.10/0.50 inference(miniscoping,[status(thm)],[f116])).
% 0.10/0.50 fof(f279,plain,(
% 0.10/0.50 ![X0,X1]: (p__pred_(X0)|p__pred_(f__nand_(X0,X1)))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f278])).
% 0.10/0.50 fof(f299,plain,(
% 0.10/0.50 p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.10/0.50 fof(f300,plain,(
% 0.10/0.50 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f135])).
% 0.10/0.50 fof(f301,plain,(
% 0.10/0.50 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f136])).
% 0.10/0.50 fof(f302,plain,(
% 0.10/0.50 p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(f_ADD_(t_206,n1)))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f137])).
% 0.10/0.50 fof(f303,plain,(
% 0.10/0.50 ~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f138])).
% 0.10/0.50 fof(f304,plain,(
% 0.10/0.50 ![X0,X1]: (def_89(X0,X1)|f_ADD_(f_SUB_(X1,X0),X0)=X1)),
% 0.10/0.50 inference(destructive_equality_resolution,[status(thm)],[f213])).
% 0.10/0.50 fof(f306,plain,(
% 0.10/0.50 ![X0]: (~def_89(X0,X0))),
% 0.10/0.50 inference(destructive_equality_resolution,[status(thm)],[f215])).
% 0.10/0.50 fof(f309,plain,(
% 0.10/0.50 ~p_LES_EQU_(n1,n0)),
% 0.10/0.50 inference(paramodulation,[status(thm)],[f229,f211])).
% 0.10/0.50 fof(f319,plain,(
% 0.10/0.50 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=n0)),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f146])).
% 0.10/0.50 fof(f320,plain,(
% 0.10/0.50 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=n0),
% 0.10/0.50 inference(resolution,[status(thm)],[f319,f302])).
% 0.10/0.50 fof(f331,plain,(
% 0.10/0.50 ~n1=n0),
% 0.10/0.50 inference(paramodulation,[status(thm)],[f229,f210])).
% 0.10/0.50 fof(f332,plain,(
% 0.10/0.50 ![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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f157])).
% 0.10/0.50 fof(f333,plain,(
% 0.10/0.50 ![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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f332])).
% 0.10/0.50 fof(f334,plain,(
% 0.10/0.50 ![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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f333])).
% 0.10/0.50 fof(f335,plain,(
% 0.10/0.50 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.10/0.50 inference(resolution,[status(thm)],[f334,f301])).
% 0.10/0.50 fof(f336,definition,(
% 0.10/0.50 sQ0_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f337,plain,(
% 0.10/0.50 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)|~sQ0_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f336])).
% 0.10/0.50 fof(f339,definition,(
% 0.10/0.50 sQ1_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f340,plain,(
% 0.10/0.50 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))|~sQ1_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f339])).
% 0.10/0.50 fof(f342,definition,(
% 0.10/0.50 sQ2_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f345,definition,(
% 0.10/0.50 sQ3_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f346,plain,(
% 0.10/0.50 p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))|~sQ3_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f345])).
% 0.10/0.50 fof(f348,plain,(
% 0.10/0.50 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f335,f336,f339,f342,f345])).
% 0.10/0.50 fof(f349,plain,(
% 0.10/0.50 $false|~sQ3_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f346,f300])).
% 0.10/0.50 fof(f350,plain,(
% 0.10/0.50 ~sQ3_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f349])).
% 0.10/0.50 fof(f351,plain,(
% 0.10/0.50 ![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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f164])).
% 0.10/0.50 fof(f352,plain,(
% 0.10/0.50 ![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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f351])).
% 0.10/0.50 fof(f353,plain,(
% 0.10/0.50 ![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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f352])).
% 0.10/0.50 fof(f354,plain,(
% 0.10/0.50 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~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.10/0.50 inference(resolution,[status(thm)],[f353,f301])).
% 0.10/0.50 fof(f355,definition,(
% 0.10/0.50 sQ4_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f356,plain,(
% 0.10/0.50 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~sQ4_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f355])).
% 0.10/0.50 fof(f358,plain,(
% 0.10/0.50 sQ4_spl|~sQ1_spl|sQ2_spl|sQ3_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f354,f355,f339,f342,f345])).
% 0.10/0.50 fof(f360,plain,(
% 0.10/0.50 ![X0]: (f_ADD_(f_SUB_(X0,X0),X0)=X0)),
% 0.10/0.50 inference(resolution,[status(thm)],[f304,f306])).
% 0.10/0.50 fof(f379,plain,(
% 0.10/0.50 ![X0]: (~p_LES_EQU_(f_ADD_(X0,n1),n1)|p_LES_EQU_(X0,f_SUB_(n1,n1)))),
% 0.10/0.50 inference(paramodulation,[status(thm)],[f360,f217])).
% 0.10/0.50 fof(f385,plain,(
% 0.10/0.50 ~p_LES_EQU_(n1,n1)|p_LES_EQU_(f_SUB_(n1,n1),f_SUB_(n1,n1))),
% 0.10/0.50 inference(paramodulation,[status(thm)],[f360,f379])).
% 0.10/0.50 fof(f386,plain,(
% 0.10/0.50 ~p_LES_EQU_(n1,n1)|p_LES_EQU_(n0,f_SUB_(n1,n1))),
% 0.10/0.50 inference(paramodulation,[status(thm)],[f229,f379])).
% 0.10/0.50 fof(f405,definition,(
% 0.10/0.50 sQ10_spl <=> (p_LES_EQU_(n1,n1))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f407,plain,(
% 0.10/0.50 ~p_LES_EQU_(n1,n1)|sQ10_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f405])).
% 0.10/0.50 fof(f408,definition,(
% 0.10/0.50 sQ11_spl <=> (p_LES_EQU_(f_SUB_(n1,n1),f_SUB_(n1,n1)))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f411,plain,(
% 0.10/0.50 ~sQ10_spl|sQ11_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f385,f405,f408])).
% 0.10/0.50 fof(f412,definition,(
% 0.10/0.50 sQ12_spl <=> (p_LES_EQU_(n0,f_SUB_(n1,n1)))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f413,plain,(
% 0.10/0.50 p_LES_EQU_(n0,f_SUB_(n1,n1))|~sQ12_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f412])).
% 0.10/0.50 fof(f415,plain,(
% 0.10/0.50 ~sQ10_spl|sQ12_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f386,f405,f412])).
% 0.10/0.50 fof(f416,plain,(
% 0.10/0.50 $false|sQ10_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f407,f227])).
% 0.10/0.50 fof(f417,plain,(
% 0.10/0.50 sQ10_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f416])).
% 0.10/0.50 fof(f429,plain,(
% 0.10/0.50 f_SUB_(n1,n1)=n0|p_LES_EQU_(f_ADD_(n0,n1),f_SUB_(n1,n1))|~sQ12_spl),
% 0.10/0.50 inference(resolution,[status(thm)],[f219,f413])).
% 0.10/0.50 fof(f430,plain,(
% 0.10/0.50 fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n0|p_LES_EQU_(f_ADD_(n0,n1),fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))),
% 0.10/0.50 inference(resolution,[status(thm)],[f219,f299])).
% 0.10/0.50 fof(f440,definition,(
% 0.10/0.50 sQ15_spl <=> (f_SUB_(n1,n1)=n0)),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f441,plain,(
% 0.10/0.50 f_SUB_(n1,n1)=n0|~sQ15_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f440])).
% 0.10/0.50 fof(f443,definition,(
% 0.10/0.50 sQ16_spl <=> (p_LES_EQU_(f_ADD_(n0,n1),f_SUB_(n1,n1)))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f444,plain,(
% 0.10/0.50 p_LES_EQU_(f_ADD_(n0,n1),f_SUB_(n1,n1))|~sQ16_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f443])).
% 0.10/0.50 fof(f446,plain,(
% 0.10/0.50 sQ15_spl|sQ16_spl|~sQ12_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f429,f440,f443,f412])).
% 0.10/0.50 fof(f447,definition,(
% 0.10/0.50 sQ17_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n0)),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f448,plain,(
% 0.10/0.50 fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n0|~sQ17_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f447])).
% 0.10/0.50 fof(f450,definition,(
% 0.10/0.50 sQ18_spl <=> (p_LES_EQU_(f_ADD_(n0,n1),fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f451,plain,(
% 0.10/0.50 p_LES_EQU_(f_ADD_(n0,n1),fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))|~sQ18_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f450])).
% 0.10/0.50 fof(f453,plain,(
% 0.10/0.50 sQ17_spl|sQ18_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f430,f447,f450])).
% 0.10/0.50 fof(f454,plain,(
% 0.10/0.50 p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))|~sQ18_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f229,f451])).
% 0.10/0.50 fof(f455,plain,(
% 0.10/0.50 p_LES_EQU_(n1,f_SUB_(n1,n1))|~sQ16_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f229,f444])).
% 0.10/0.50 fof(f461,plain,(
% 0.10/0.50 p_LES_EQU_(n1,n0)|~sQ17_spl|~sQ18_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f448,f454])).
% 0.10/0.50 fof(f462,plain,(
% 0.10/0.50 $false|~sQ17_spl|~sQ18_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f461,f309])).
% 0.10/0.50 fof(f463,plain,(
% 0.10/0.50 ~sQ17_spl|~sQ18_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f462])).
% 0.10/0.50 fof(f466,definition,(
% 0.10/0.50 sQ19_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n1)),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f467,plain,(
% 0.10/0.50 fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n1|~sQ19_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f466])).
% 0.10/0.50 fof(f474,plain,(
% 0.10/0.50 p_LES_EQU_(n0,n1)|~sQ19_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f467,f299])).
% 0.10/0.50 fof(f475,plain,(
% 0.10/0.50 n1=n0|p_LES_EQU_(f_ADD_(n0,n1),n1)|~sQ19_spl),
% 0.10/0.50 inference(resolution,[status(thm)],[f474,f219])).
% 0.10/0.50 fof(f477,definition,(
% 0.10/0.50 sQ21_spl <=> (n1=n0)),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f478,plain,(
% 0.10/0.50 n1=n0|~sQ21_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f477])).
% 0.10/0.50 fof(f480,definition,(
% 0.10/0.50 sQ22_spl <=> (p_LES_EQU_(f_ADD_(n0,n1),n1))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f483,plain,(
% 0.10/0.50 sQ21_spl|sQ22_spl|~sQ19_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f475,f477,f480,f466])).
% 0.10/0.50 fof(f486,plain,(
% 0.10/0.50 $false|~sQ21_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f478,f331])).
% 0.10/0.50 fof(f487,plain,(
% 0.10/0.50 ~sQ21_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f486])).
% 0.10/0.50 fof(f510,plain,(
% 0.10/0.50 p_LES_EQU_(n1,n0)|~sQ15_spl|~sQ16_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f441,f455])).
% 0.10/0.50 fof(f511,plain,(
% 0.10/0.50 $false|~sQ15_spl|~sQ16_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f510,f309])).
% 0.10/0.50 fof(f512,plain,(
% 0.10/0.50 ~sQ15_spl|~sQ16_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f511])).
% 0.10/0.50 fof(f536,plain,(
% 0.10/0.50 n1=n0|~p_LES_EQU_(n1,n0)|~sQ19_spl),
% 0.10/0.50 inference(resolution,[status(thm)],[f474,f221])).
% 0.10/0.50 fof(f539,definition,(
% 0.10/0.50 sQ28_spl <=> (p_LES_EQU_(n1,n0))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f542,plain,(
% 0.10/0.50 sQ21_spl|~sQ28_spl|~sQ19_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f536,f477,f539,f466])).
% 0.10/0.50 fof(f572,definition,(
% 0.10/0.50 sQ31_spl <=> (p_LES_EQU_(f_SUB_(n1,n1),n1))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f573,plain,(
% 0.10/0.50 p_LES_EQU_(f_SUB_(n1,n1),n1)|~sQ31_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f572])).
% 0.10/0.50 fof(f576,definition,(
% 0.10/0.50 sQ32_spl <=> (p_LES_EQU_(n0,n1))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f577,plain,(
% 0.10/0.50 p_LES_EQU_(n0,n1)|~sQ32_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f576])).
% 0.10/0.50 fof(f580,plain,(
% 0.10/0.50 p_LES_EQU_(n0,n1)|~sQ15_spl|~sQ31_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f441,f573])).
% 0.10/0.50 fof(f582,plain,(
% 0.10/0.50 fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n0|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0)),
% 0.10/0.50 inference(resolution,[status(thm)],[f299,f221])).
% 0.10/0.50 fof(f585,definition,(
% 0.10/0.50 sQ33_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f587,plain,(
% 0.10/0.50 ~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0)|sQ33_spl),
% 0.10/0.50 inference(component_clause,[status(thm)],[f585])).
% 0.10/0.50 fof(f588,plain,(
% 0.10/0.50 sQ17_spl|~sQ33_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f582,f447,f585])).
% 0.10/0.50 fof(f591,plain,(
% 0.10/0.50 n1=n0|~p_LES_EQU_(n1,n0)|~sQ32_spl),
% 0.10/0.50 inference(resolution,[status(thm)],[f577,f221])).
% 0.10/0.50 fof(f592,plain,(
% 0.10/0.50 n1=n0|p_LES_EQU_(f_ADD_(n0,n1),n1)|~sQ32_spl),
% 0.10/0.50 inference(resolution,[status(thm)],[f577,f219])).
% 0.10/0.50 fof(f594,plain,(
% 0.10/0.50 sQ21_spl|~sQ28_spl|~sQ32_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f591,f477,f539,f576])).
% 0.10/0.50 fof(f595,plain,(
% 0.10/0.50 sQ21_spl|sQ22_spl|~sQ32_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f592,f477,f480,f576])).
% 0.10/0.50 fof(f597,plain,(
% 0.10/0.50 n1=n0|~p_LES_EQU_(n1,n0)|~sQ15_spl|~sQ31_spl),
% 0.10/0.50 inference(resolution,[status(thm)],[f580,f221])).
% 0.10/0.50 fof(f598,plain,(
% 0.10/0.50 n1=n0|p_LES_EQU_(f_ADD_(n0,n1),n1)|~sQ15_spl|~sQ31_spl),
% 0.10/0.50 inference(resolution,[status(thm)],[f580,f219])).
% 0.10/0.50 fof(f600,plain,(
% 0.10/0.50 sQ21_spl|~sQ28_spl|~sQ15_spl|~sQ31_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f597,f477,f539,f440,f572])).
% 0.10/0.50 fof(f601,plain,(
% 0.10/0.50 sQ21_spl|sQ22_spl|~sQ15_spl|~sQ31_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f598,f477,f480,f440,f572])).
% 0.10/0.50 fof(f702,plain,(
% 0.10/0.50 ![X0,X1]: (~p__pred_(X0)|~p__pred_(X1)|~p__pred_(X0)|p__pred_(X1))),
% 0.10/0.50 inference(resolution,[status(thm)],[f257,f256])).
% 0.10/0.50 fof(f704,definition,(
% 0.10/0.50 ![X0]: (sQ44_spl <=> (~p__pred_(X0)|~p__pred_(X0)))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f705,plain,(
% 0.10/0.50 ![X0]: (~p__pred_(X0)|~p__pred_(X0)|~sQ44_spl)),
% 0.10/0.50 inference(component_clause,[status(thm)],[f704])).
% 0.10/0.50 fof(f707,definition,(
% 0.10/0.50 ![X1]: (sQ45_spl <=> (~p__pred_(X1)|p__pred_(X1)))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f710,plain,(
% 0.10/0.50 sQ44_spl|sQ45_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f702,f704,f707])).
% 0.10/0.50 fof(f712,plain,(
% 0.10/0.50 ![X0]: (~p__pred_(X0)|~sQ44_spl)),
% 0.10/0.50 inference(duplicate_literals_removal,[status(thm)],[f705])).
% 0.10/0.50 fof(f755,plain,(
% 0.10/0.50 n0=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~sQ4_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f320,f356])).
% 0.10/0.50 fof(f756,plain,(
% 0.10/0.50 n0=n1|~sQ19_spl|~sQ4_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f467,f755])).
% 0.10/0.50 fof(f757,plain,(
% 0.10/0.50 $false|~sQ19_spl|~sQ4_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f756,f331])).
% 0.10/0.50 fof(f758,plain,(
% 0.10/0.50 ~sQ19_spl|~sQ4_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f757])).
% 0.10/0.50 fof(f759,plain,(
% 0.10/0.50 n0=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)|~sQ0_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f320,f337])).
% 0.10/0.50 fof(f760,plain,(
% 0.10/0.50 $false|~sQ0_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f759,f210])).
% 0.10/0.50 fof(f761,plain,(
% 0.10/0.50 ~sQ0_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f760])).
% 0.10/0.50 fof(f763,plain,(
% 0.10/0.50 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)|~sQ17_spl|~sQ1_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f448,f340])).
% 0.10/0.50 fof(f764,plain,(
% 0.10/0.50 $false|~sQ17_spl|~sQ1_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f763,f303])).
% 0.10/0.50 fof(f765,plain,(
% 0.10/0.50 ~sQ17_spl|~sQ1_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f764])).
% 0.10/0.50 fof(f774,plain,(
% 0.10/0.50 ![X0,X1]: (p__pred_(f__nand_(X0,X1))|~sQ44_spl)),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f279,f712])).
% 0.10/0.50 fof(f782,plain,(
% 0.10/0.50 $false|~sQ44_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f774,f712])).
% 0.10/0.50 fof(f783,plain,(
% 0.10/0.50 ~sQ44_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f782])).
% 0.10/0.50 fof(f847,plain,(
% 0.10/0.50 sQ32_spl|~sQ19_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f474,f576,f466])).
% 0.10/0.50 fof(f856,plain,(
% 0.10/0.50 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTint__level_(X0)|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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f174])).
% 0.10/0.50 fof(f857,plain,(
% 0.10/0.50 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(X0)|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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f856])).
% 0.10/0.50 fof(f858,plain,(
% 0.10/0.50 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(X0)|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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f857])).
% 0.10/0.50 fof(f859,plain,(
% 0.10/0.50 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.10/0.50 inference(resolution,[status(thm)],[f858,f301])).
% 0.10/0.50 fof(f860,plain,(
% 0.10/0.50 sQ4_spl|sQ33_spl|~sQ2_spl|sQ3_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f859,f355,f585,f342,f345])).
% 0.10/0.50 fof(f936,definition,(
% 0.10/0.50 ![X0]: (sQ66_spl <=> (p__pred_(X0)))),
% 0.10/0.50 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.10/0.50 fof(f937,plain,(
% 0.10/0.50 ![X0]: (p__pred_(X0)|~sQ66_spl)),
% 0.10/0.50 inference(component_clause,[status(thm)],[f936])).
% 0.10/0.50 fof(f942,plain,(
% 0.10/0.50 $false|~sQ66_spl),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f300,f937])).
% 0.10/0.50 fof(f943,plain,(
% 0.10/0.50 ~sQ66_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f942])).
% 0.10/0.50 fof(f950,plain,(
% 0.10/0.50 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=f_ADD_(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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f180])).
% 0.10/0.50 fof(f951,plain,(
% 0.10/0.50 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=f_ADD_(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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f950])).
% 0.10/0.50 fof(f952,plain,(
% 0.10/0.50 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(X0,n1))=f_ADD_(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.10/0.50 inference(forward_demodulation,[status(thm)],[f142,f951])).
% 0.10/0.50 fof(f953,plain,(
% 0.10/0.50 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.10/0.51 inference(resolution,[status(thm)],[f952,f301])).
% 0.10/0.51 fof(f954,plain,(
% 0.10/0.51 sQ0_spl|~sQ33_spl|~sQ2_spl|sQ3_spl),
% 0.10/0.51 inference(split_clause,[status(thm)],[f953,f336,f585,f342,f345])).
% 0.10/0.51 fof(f955,plain,(
% 0.10/0.51 ~p_LES_EQU_(n0,n0)|~sQ17_spl|sQ33_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f448,f587])).
% 0.10/0.51 fof(f956,plain,(
% 0.10/0.51 $false|~sQ17_spl|sQ33_spl),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f955,f227])).
% 0.10/0.51 fof(f957,plain,(
% 0.10/0.51 ~sQ17_spl|sQ33_spl),
% 0.10/0.51 inference(contradiction_clause,[status(thm)],[f956])).
% 0.10/0.51 fof(f958,plain,(
% 0.10/0.51 sQ17_spl|~sQ4_spl),
% 0.10/0.51 inference(split_clause,[status(thm)],[f755,f447,f355])).
% 0.10/0.51 fof(f959,plain,(
% 0.10/0.51 $false),
% 0.10/0.51 inference(sat_refutation,[status(thm)],[f348,f350,f358,f411,f415,f417,f446,f453,f463,f483,f487,f512,f542,f588,f594,f595,f600,f601,f710,f758,f761,f765,f783,f847,f860,f943,f954,f957,f958])).
% 0.10/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.55 % Elapsed time: 0.184045 seconds
% 0.10/0.55 % CPU time: 1.020465 seconds
% 0.10/0.55 % Total memory used: 118.392 MB
% 0.10/0.55 % Net memory used: 116.757 MB
%------------------------------------------------------------------------------