%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV017-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 : n009.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.14s 5.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV017-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.10/5.37 % Computer : n009.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Sun Sep 20 20:48:32 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.39 % Drodi V4.1.1
% 0.14/5.52 % Refutation found
% 0.14/5.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/5.52 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.52 fof(f4,axiom,(
% 0.14/5.52 (![T_0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(T_0) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_0) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f5,axiom,(
% 0.14/5.52 (![T_1]: (( p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(T_1))| fwork_DOTfifo_DOTrtl_DOTint__level_(T_1) != fwork_DOTfifo_DOTrtl_DOTfifo__length_ ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f6,axiom,(
% 0.14/5.52 (![T_2]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(T_2))| fwork_DOTfifo_DOTrtl_DOTint__level_(T_2) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f7,axiom,(
% 0.14/5.52 (![T_3]: (( p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_3))| fwork_DOTfifo_DOTrtl_DOTint__level_(T_3) != n0 ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f8,axiom,(
% 0.14/5.52 (![T_4]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_4))| fwork_DOTfifo_DOTrtl_DOTint__level_(T_4) = n0 ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f12,axiom,(
% 0.14/5.52 (![T_5]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_5,n1)))| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)) ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f13,axiom,(
% 0.14/5.52 (![T_5]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_5,n1)))| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)) ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f14,axiom,(
% 0.14/5.52 (![T_5,I1_6,I2_7]: (( ~ p__pred_(f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_5,n1)),I1_6),I2_7))| ~ p_LES_EQU_(n0,I2_7)| ~ p_LES_EQU_(I2_7,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))| ~ p_LES_EQU_(n0,I1_6)| ~ p_LES_EQU_(I1_6,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)) ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f15,axiom,(
% 0.14/5.52 (![T_5,I1_10]: (( ~ p__pred_(f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_5,n1)),I1_10))| ~ p_LES_EQU_(n0,I1_10)| ~ p_LES_EQU_(I1_10,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)) ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f16,axiom,(
% 0.14/5.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f17,axiom,(
% 0.14/5.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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f18,axiom,(
% 0.14/5.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(T_13,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)| 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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f21,axiom,(
% 0.14/5.52 (![T_13]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f23,axiom,(
% 0.14/5.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTwr__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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f26,axiom,(
% 0.14/5.52 (![T_13]: (( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(T_13))| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1)))| 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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f27,axiom,(
% 0.14/5.52 (![T_13]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1)))| 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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f29,axiom,(
% 0.14/5.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(T_13,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)| ~ 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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f33,axiom,(
% 0.14/5.52 (![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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f34,axiom,(
% 0.14/5.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__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.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f35,axiom,(
% 0.14/5.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_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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f36,axiom,(
% 0.14/5.52 (![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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f40,axiom,(
% 0.14/5.52 (![T_13]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_13,n1)))| ~ 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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f41,axiom,(
% 0.14/5.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13)| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13)) ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f42,axiom,(
% 0.14/5.52 (![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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f45,axiom,(
% 0.14/5.52 (![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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f46,axiom,(
% 0.14/5.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_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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f47,axiom,(
% 0.14/5.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__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.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f48,axiom,(
% 0.14/5.52 (![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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f50,axiom,(
% 0.14/5.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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f51,axiom,(
% 0.14/5.52 (![T_13]: (( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTrd__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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f52,axiom,(
% 0.14/5.52 (![T_13]: (( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(T_13))| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_13,n1)))| 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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f55,axiom,(
% 0.14/5.52 (![T_13]: (( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(T_13))| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_13,n1)))| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13)) ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f56,axiom,(
% 0.14/5.52 (![T_13]: (( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_13,n1)))| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13)) ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f58,axiom,(
% 0.14/5.52 (![X_80]: (f_ADD_(X_80,n1) != n0 ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f59,axiom,(
% 0.14/5.52 (![X_81]: (~ p_LES_EQU_(f_ADD_(X_81,n1),n0) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f60,axiom,(
% 0.14/5.52 (![X_82]: (( ~ p_LES_EQU_(X_82,f_SUB_(X_82,n1))| p_LES_EQU_(X_82,n0) ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f67,axiom,(
% 0.14/5.52 (![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/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f69,axiom,(
% 0.14/5.52 (![X_96,Y_97]: (( X_96 = Y_97| ~ p_LES_EQU_(X_96,Y_97)| ~ p_LES_EQU_(Y_97,X_96) ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f70,axiom,(
% 0.14/5.52 (![Z_100,X_98,Y_99]: (( ~ p_LES_EQU_(Z_100,X_98)| p_LES_EQU_(Y_99,X_98)| p_LES_EQU_(Z_100,Y_99) ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f72,axiom,(
% 0.14/5.52 (![X_103]: (( ~ p_LES_EQU_(X_103,n0)| X_103 = n0 ) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f74,axiom,(
% 0.14/5.52 (![X_106]: (p_LES_EQU_(X_106,X_106) ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f76,axiom,(
% 0.14/5.52 (![X_109]: (f_ADD_(n0,X_109) = X_109 ))),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f134,negated_conjecture,(
% 0.14/5.52 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f135,negated_conjecture,(
% 0.14/5.52 ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)) ),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f136,negated_conjecture,(
% 0.14/5.52 ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)) ),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f137,negated_conjecture,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f138,negated_conjecture,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(f_ADD_(t_206,n1))) ),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f139,negated_conjecture,(
% 0.14/5.52 ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0) ),
% 0.14/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f143,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=fwork_DOTfifo_DOTrtl_DOTint__level_(X0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.52 fof(f144,plain,(
% 0.14/5.52 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X0))|~fwork_DOTfifo_DOTrtl_DOTint__level_(X0)=fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.52 fof(f145,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X0))|fwork_DOTfifo_DOTrtl_DOTint__level_(X0)=fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/5.52 fof(f146,plain,(
% 0.14/5.52 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|~fwork_DOTfifo_DOTrtl_DOTint__level_(X0)=n0)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/5.52 fof(f147,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|fwork_DOTfifo_DOTrtl_DOTint__level_(X0)=n0)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/5.52 fof(f151,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X0,n1)))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.52 fof(f152,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/5.52 fof(f153,plain,(
% 0.14/5.52 ![T_5]: ((![I1_6]: (((![I2_7]: ((~p__pred_(f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_5,n1)),I1_6),I2_7))|~p_LES_EQU_(n0,I2_7))|~p_LES_EQU_(I2_7,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))))|~p_LES_EQU_(n0,I1_6))|~p_LES_EQU_(I1_6,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f14])).
% 0.14/5.52 fof(f154,plain,(
% 0.14/5.52 ![X0,X1,X2]: (~p__pred_(f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),X1),X2))|~p_LES_EQU_(n0,X2)|~p_LES_EQU_(X2,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|~p_LES_EQU_(n0,X1)|~p_LES_EQU_(X1,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f153])).
% 0.14/5.52 fof(f155,plain,(
% 0.14/5.52 ![T_5]: ((![I1_10]: ((~p__pred_(f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_5,n1)),I1_10))|~p_LES_EQU_(n0,I1_10))|~p_LES_EQU_(I1_10,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f15])).
% 0.14/5.52 fof(f156,plain,(
% 0.14/5.52 ![X0,X1]: (~p__pred_(f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(X0,n1)),X1))|~p_LES_EQU_(n0,X1)|~p_LES_EQU_(X1,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f155])).
% 0.14/5.52 fof(f157,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__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/5.52 inference(cnf_transformation,[status(thm)],[f16])).
% 0.14/5.52 fof(f158,plain,(
% 0.14/5.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/5.52 inference(cnf_transformation,[status(thm)],[f17])).
% 0.14/5.52 fof(f159,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X0,n1))=fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(X0),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)|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/5.52 inference(cnf_transformation,[status(thm)],[f18])).
% 0.14/5.52 fof(f164,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(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/5.52 inference(cnf_transformation,[status(thm)],[f21])).
% 0.14/5.52 fof(f166,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTwr__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/5.52 inference(cnf_transformation,[status(thm)],[f23])).
% 0.14/5.52 fof(f170,plain,(
% 0.14/5.52 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f26])).
% 0.14/5.52 fof(f171,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f27])).
% 0.14/5.52 fof(f174,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X0,n1))=fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(X0),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f29])).
% 0.14/5.52 fof(f179,plain,(
% 0.14/5.52 ![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/5.52 inference(cnf_transformation,[status(thm)],[f33])).
% 0.14/5.52 fof(f180,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__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.14/5.52 inference(cnf_transformation,[status(thm)],[f34])).
% 0.14/5.52 fof(f181,plain,(
% 0.14/5.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_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/5.52 inference(cnf_transformation,[status(thm)],[f35])).
% 0.14/5.52 fof(f182,plain,(
% 0.14/5.52 ![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/5.52 inference(cnf_transformation,[status(thm)],[f36])).
% 0.14/5.52 fof(f189,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X0,n1)))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f40])).
% 0.14/5.52 fof(f190,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTwr__level_(X0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f41])).
% 0.14/5.52 fof(f191,plain,(
% 0.14/5.52 ![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/5.52 inference(cnf_transformation,[status(thm)],[f42])).
% 0.14/5.52 fof(f195,plain,(
% 0.14/5.52 ![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/5.52 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/5.52 fof(f196,plain,(
% 0.14/5.52 ![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.14/5.52 inference(cnf_transformation,[status(thm)],[f46])).
% 0.14/5.52 fof(f197,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__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.14/5.52 inference(cnf_transformation,[status(thm)],[f47])).
% 0.14/5.52 fof(f198,plain,(
% 0.14/5.52 ![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/5.52 inference(cnf_transformation,[status(thm)],[f48])).
% 0.14/5.52 fof(f201,plain,(
% 0.14/5.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/5.52 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/5.52 fof(f202,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__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/5.52 inference(cnf_transformation,[status(thm)],[f51])).
% 0.14/5.52 fof(f203,plain,(
% 0.14/5.52 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f52])).
% 0.14/5.52 fof(f207,plain,(
% 0.14/5.52 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X0,n1)))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/5.52 fof(f208,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X0,n1)))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f56])).
% 0.14/5.52 fof(f211,plain,(
% 0.14/5.52 ![X0]: (~f_ADD_(X0,n1)=n0)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f58])).
% 0.14/5.52 fof(f212,plain,(
% 0.14/5.52 ![X0]: (~p_LES_EQU_(f_ADD_(X0,n1),n0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f59])).
% 0.14/5.52 fof(f213,plain,(
% 0.14/5.52 ![X0]: (~p_LES_EQU_(X0,f_SUB_(X0,n1))|p_LES_EQU_(X0,n0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f60])).
% 0.14/5.52 fof(f220,plain,(
% 0.14/5.52 ![X0,X1]: (X0=X1|~p_LES_EQU_(X1,X0)|p_LES_EQU_(f_ADD_(X1,n1),X0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f67])).
% 0.14/5.52 fof(f222,plain,(
% 0.14/5.52 ![X0,X1]: (X0=X1|~p_LES_EQU_(X0,X1)|~p_LES_EQU_(X1,X0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f69])).
% 0.14/5.52 fof(f223,plain,(
% 0.14/5.52 ![Z_100,Y_99]: ((![X_98]: (~p_LES_EQU_(Z_100,X_98)|p_LES_EQU_(Y_99,X_98)))|p_LES_EQU_(Z_100,Y_99))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f70])).
% 0.14/5.52 fof(f224,plain,(
% 0.14/5.52 ![X0,X1,X2]: (~p_LES_EQU_(X0,X1)|p_LES_EQU_(X2,X1)|p_LES_EQU_(X0,X2))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f223])).
% 0.14/5.52 fof(f226,plain,(
% 0.14/5.52 ![X0]: (~p_LES_EQU_(X0,n0)|X0=n0)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f72])).
% 0.14/5.52 fof(f228,plain,(
% 0.14/5.52 ![X0]: (p_LES_EQU_(X0,X0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f74])).
% 0.14/5.52 fof(f230,plain,(
% 0.14/5.52 ![X0]: (f_ADD_(n0,X0)=X0)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f76])).
% 0.14/5.52 fof(f300,plain,(
% 0.14/5.52 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f134])).
% 0.14/5.52 fof(f301,plain,(
% 0.14/5.52 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f135])).
% 0.14/5.52 fof(f302,plain,(
% 0.14/5.52 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f136])).
% 0.14/5.52 fof(f303,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f137])).
% 0.14/5.52 fof(f304,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(f_ADD_(t_206,n1)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/5.52 fof(f305,plain,(
% 0.14/5.52 ~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f139])).
% 0.14/5.52 fof(f308,plain,(
% 0.14/5.52 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X0))|~fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f143,f144])).
% 0.14/5.52 fof(f309,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X0))|fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f143,f145])).
% 0.14/5.52 fof(f315,plain,(
% 0.14/5.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/5.52 inference(forward_demodulation,[status(thm)],[f143,f158])).
% 0.14/5.52 fof(f316,plain,(
% 0.14/5.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/5.52 inference(forward_demodulation,[status(thm)],[f143,f315])).
% 0.14/5.52 fof(f317,plain,(
% 0.14/5.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/5.52 inference(forward_demodulation,[status(thm)],[f143,f316])).
% 0.14/5.52 fof(f321,plain,(
% 0.14/5.52 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|~fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=n0)),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f143,f146])).
% 0.14/5.52 fof(f322,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(X0))|fwork_DOTfifo_DOTrtl_DOTlevel_(X0)=n0)),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f143,f147])).
% 0.14/5.52 fof(f323,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTfifo__length_),
% 0.14/5.52 inference(resolution,[status(thm)],[f304,f309])).
% 0.14/5.52 fof(f325,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(f_ADD_(t_206,n1)))|~fwork_DOTfifo_DOTrtl_DOTfifo__length_=n0),
% 0.14/5.52 inference(paramodulation,[status(thm)],[f323,f321])).
% 0.14/5.52 fof(f327,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(f_ADD_(t_206,n1)))|~fwork_DOTfifo_DOTrtl_DOTfifo__length_=fwork_DOTfifo_DOTrtl_DOTfifo__length_),
% 0.14/5.52 inference(paramodulation,[status(thm)],[f323,f308])).
% 0.14/5.52 fof(f328,definition,(
% 0.14/5.52 sQ0_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(f_ADD_(t_206,n1))))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f329,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(f_ADD_(t_206,n1)))|~sQ0_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f328])).
% 0.14/5.52 fof(f331,definition,(
% 0.14/5.52 sQ1_spl <=> (fwork_DOTfifo_DOTrtl_DOTfifo__length_=n0)),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f333,plain,(
% 0.14/5.52 ~fwork_DOTfifo_DOTrtl_DOTfifo__length_=n0|sQ1_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f331])).
% 0.14/5.52 fof(f334,plain,(
% 0.14/5.52 sQ0_spl|~sQ1_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f325,f328,f331])).
% 0.14/5.52 fof(f338,definition,(
% 0.14/5.52 sQ3_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTfifo__length_))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f340,plain,(
% 0.14/5.52 ~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|sQ3_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f338])).
% 0.14/5.52 fof(f351,definition,(
% 0.14/5.52 sQ7_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(f_ADD_(t_206,n1))))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f354,definition,(
% 0.14/5.52 sQ8_spl <=> (fwork_DOTfifo_DOTrtl_DOTfifo__length_=fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f356,plain,(
% 0.14/5.52 ~fwork_DOTfifo_DOTrtl_DOTfifo__length_=fwork_DOTfifo_DOTrtl_DOTfifo__length_|sQ8_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f354])).
% 0.14/5.52 fof(f357,plain,(
% 0.14/5.52 sQ7_spl|~sQ8_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f327,f351,f354])).
% 0.14/5.52 fof(f358,plain,(
% 0.14/5.52 $false|sQ8_spl),
% 0.14/5.52 inference(trivial_equality_resolution,[status(thm)],[f356])).
% 0.14/5.52 fof(f359,plain,(
% 0.14/5.52 sQ8_spl),
% 0.14/5.52 inference(contradiction_clause,[status(thm)],[f358])).
% 0.14/5.52 fof(f360,plain,(
% 0.14/5.52 ~n1=n0),
% 0.14/5.52 inference(paramodulation,[status(thm)],[f230,f211])).
% 0.14/5.52 fof(f367,plain,(
% 0.14/5.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_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/5.52 inference(forward_demodulation,[status(thm)],[f143,f181])).
% 0.14/5.52 fof(f368,plain,(
% 0.14/5.52 ![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.14/5.52 inference(forward_demodulation,[status(thm)],[f143,f367])).
% 0.14/5.52 fof(f369,plain,(
% 0.14/5.52 ![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.14/5.52 inference(forward_demodulation,[status(thm)],[f143,f368])).
% 0.14/5.52 fof(f374,definition,(
% 0.14/5.52 sQ10_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f381,plain,(
% 0.14/5.52 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(n1))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))),
% 0.14/5.52 inference(paramodulation,[status(thm)],[f230,f151])).
% 0.14/5.52 fof(f385,definition,(
% 0.14/5.52 sQ11_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(n1)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f387,plain,(
% 0.14/5.52 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(n1))|sQ11_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f385])).
% 0.14/5.52 fof(f388,definition,(
% 0.14/5.52 sQ12_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f391,plain,(
% 0.14/5.52 ~sQ11_spl|~sQ12_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f381,f385,f388])).
% 0.14/5.52 fof(f410,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=n0|~sQ0_spl),
% 0.14/5.52 inference(resolution,[status(thm)],[f329,f322])).
% 0.14/5.52 fof(f411,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTfifo__length_=n0|~sQ0_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f323,f410])).
% 0.14/5.52 fof(f427,plain,(
% 0.14/5.52 ~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~sQ0_spl),
% 0.14/5.52 inference(backward_demodulation,[status(thm)],[f411,f305])).
% 0.14/5.52 fof(f429,plain,(
% 0.14/5.52 $false|~sQ0_spl),
% 0.14/5.52 inference(forward_subsumption_resolution,[status(thm)],[f427,f228])).
% 0.14/5.52 fof(f430,plain,(
% 0.14/5.52 ~sQ0_spl),
% 0.14/5.52 inference(contradiction_clause,[status(thm)],[f429])).
% 0.14/5.52 fof(f431,plain,(
% 0.14/5.52 ![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/5.52 inference(forward_demodulation,[status(thm)],[f143,f191])).
% 0.14/5.52 fof(f432,plain,(
% 0.14/5.52 ![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/5.52 inference(forward_demodulation,[status(thm)],[f143,f431])).
% 0.14/5.52 fof(f433,plain,(
% 0.14/5.52 ![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/5.52 inference(forward_demodulation,[status(thm)],[f143,f432])).
% 0.14/5.52 fof(f434,plain,(
% 0.14/5.52 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/5.52 inference(resolution,[status(thm)],[f433,f303])).
% 0.14/5.52 fof(f435,definition,(
% 0.14/5.52 sQ18_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_SUB_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f436,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=f_SUB_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)|~sQ18_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f435])).
% 0.14/5.52 fof(f438,definition,(
% 0.14/5.52 sQ19_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f439,plain,(
% 0.14/5.52 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0)|~sQ19_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f438])).
% 0.14/5.52 fof(f441,definition,(
% 0.14/5.52 sQ20_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f442,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))|~sQ20_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f441])).
% 0.14/5.52 fof(f444,definition,(
% 0.14/5.52 sQ21_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f445,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))|~sQ21_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f444])).
% 0.14/5.52 fof(f447,plain,(
% 0.14/5.52 sQ18_spl|sQ19_spl|sQ20_spl|sQ21_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f434,f435,f438,f441,f444])).
% 0.14/5.52 fof(f448,plain,(
% 0.14/5.52 $false|~sQ21_spl),
% 0.14/5.52 inference(forward_subsumption_resolution,[status(thm)],[f445,f302])).
% 0.14/5.52 fof(f449,plain,(
% 0.14/5.52 ~sQ21_spl),
% 0.14/5.52 inference(contradiction_clause,[status(thm)],[f448])).
% 0.14/5.52 fof(f450,plain,(
% 0.14/5.52 $false|~sQ20_spl),
% 0.14/5.52 inference(forward_subsumption_resolution,[status(thm)],[f442,f301])).
% 0.14/5.52 fof(f451,plain,(
% 0.14/5.52 ~sQ20_spl),
% 0.14/5.52 inference(contradiction_clause,[status(thm)],[f450])).
% 0.14/5.52 fof(f452,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTfifo__length_=f_SUB_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1)|~sQ18_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f323,f436])).
% 0.14/5.52 fof(f453,plain,(
% 0.14/5.52 ![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.14/5.52 inference(forward_demodulation,[status(thm)],[f143,f196])).
% 0.14/5.52 fof(f454,plain,(
% 0.14/5.52 ![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.14/5.52 inference(forward_demodulation,[status(thm)],[f143,f453])).
% 0.14/5.52 fof(f455,plain,(
% 0.14/5.52 ![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.14/5.52 inference(forward_demodulation,[status(thm)],[f143,f454])).
% 0.14/5.52 fof(f503,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(n1),X0))|~p_LES_EQU_(n0,X0)|~p_LES_EQU_(X0,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0)))),
% 0.14/5.52 inference(paramodulation,[status(thm)],[f230,f156])).
% 0.14/5.52 fof(f504,plain,(
% 0.14/5.52 ![X0,X1]: (~p__pred_(f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(n1),X0),X1))|~p_LES_EQU_(n0,X1)|~p_LES_EQU_(X1,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|~p_LES_EQU_(n0,X0)|~p_LES_EQU_(X0,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0)))),
% 0.14/5.52 inference(paramodulation,[status(thm)],[f230,f154])).
% 0.14/5.52 fof(f505,plain,(
% 0.14/5.52 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n1))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))),
% 0.14/5.52 inference(paramodulation,[status(thm)],[f230,f152])).
% 0.14/5.52 fof(f507,definition,(
% 0.14/5.52 ![X0]: (sQ31_spl <=> (~p__pred_(f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(n1),X0))|~p_LES_EQU_(n0,X0)|~p_LES_EQU_(X0,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f510,plain,(
% 0.14/5.52 sQ31_spl|~sQ12_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f503,f507,f388])).
% 0.14/5.52 fof(f511,definition,(
% 0.14/5.52 ![X0,X1]: (sQ32_spl <=> (~p__pred_(f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(n1),X0),X1))|~p_LES_EQU_(n0,X1)|~p_LES_EQU_(X1,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|~p_LES_EQU_(n0,X0)|~p_LES_EQU_(X0,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f514,plain,(
% 0.14/5.52 sQ32_spl|~sQ12_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f504,f511,f388])).
% 0.14/5.52 fof(f515,definition,(
% 0.14/5.52 sQ33_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n1)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f517,plain,(
% 0.14/5.52 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n1))|sQ33_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f515])).
% 0.14/5.52 fof(f518,plain,(
% 0.14/5.52 ~sQ33_spl|~sQ12_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f505,f515,f388])).
% 0.14/5.52 fof(f520,plain,(
% 0.14/5.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/5.52 inference(forward_demodulation,[status(thm)],[f143,f201])).
% 0.14/5.52 fof(f521,plain,(
% 0.14/5.52 ![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_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(backward_subsumption_resolution,[status(thm)],[f455,f523])).
% 0.14/5.52 fof(f523,plain,(
% 0.14/5.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/5.52 inference(forward_demodulation,[status(thm)],[f143,f520])).
% 0.14/5.52 fof(f526,definition,(
% 0.14/5.52 sQ34_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f527,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~sQ34_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f526])).
% 0.14/5.52 fof(f534,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTfifo__length_=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~sQ34_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f323,f527])).
% 0.14/5.52 fof(f535,plain,(
% 0.14/5.52 ~p_LES_EQU_(n1,n0)),
% 0.14/5.52 inference(paramodulation,[status(thm)],[f230,f212])).
% 0.14/5.52 fof(f542,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(t_206))|~fwork_DOTfifo_DOTrtl_DOTfifo__length_=fwork_DOTfifo_DOTrtl_DOTfifo__length_|~sQ34_spl),
% 0.14/5.52 inference(paramodulation,[status(thm)],[f534,f308])).
% 0.14/5.52 fof(f543,definition,(
% 0.14/5.52 sQ36_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(t_206)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f544,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(t_206))|~sQ36_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f543])).
% 0.14/5.52 fof(f546,plain,(
% 0.14/5.52 sQ36_spl|~sQ8_spl|~sQ34_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f542,f543,f354,f526])).
% 0.14/5.52 fof(f547,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=fwork_DOTfifo_DOTrtl_DOTfifo__length_|~sQ36_spl),
% 0.14/5.52 inference(resolution,[status(thm)],[f544,f309])).
% 0.14/5.52 fof(f550,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X0,n1))=fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(X0),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)|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/5.52 inference(forward_demodulation,[status(thm)],[f143,f159])).
% 0.14/5.52 fof(f589,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(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/5.52 inference(forward_demodulation,[status(thm)],[f143,f164])).
% 0.14/5.52 fof(f590,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(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)))),
% 0.14/5.52 inference(forward_subsumption_resolution,[status(thm)],[f589,f151])).
% 0.14/5.52 fof(f595,definition,(
% 0.14/5.52 sQ40_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(n0)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f596,plain,(
% 0.14/5.52 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(n0))|~sQ40_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f595])).
% 0.14/5.52 fof(f598,definition,(
% 0.14/5.52 sQ41_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f599,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|~sQ41_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f598])).
% 0.14/5.52 fof(f601,definition,(
% 0.14/5.52 sQ42_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f602,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))|~sQ42_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f601])).
% 0.14/5.52 fof(f603,plain,(
% 0.14/5.52 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))|sQ42_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f601])).
% 0.14/5.52 fof(f626,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTwr__level_(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/5.52 inference(forward_demodulation,[status(thm)],[f143,f166])).
% 0.14/5.52 fof(f629,definition,(
% 0.14/5.52 sQ49_spl <=> (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTwr__level_(t_206))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f637,plain,(
% 0.14/5.52 $false|sQ3_spl),
% 0.14/5.52 inference(forward_subsumption_resolution,[status(thm)],[f340,f228])).
% 0.14/5.52 fof(f638,plain,(
% 0.14/5.52 sQ3_spl),
% 0.14/5.52 inference(contradiction_clause,[status(thm)],[f637])).
% 0.14/5.52 fof(f666,plain,(
% 0.14/5.52 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)|~sQ36_spl|~sQ19_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f547,f439])).
% 0.14/5.52 fof(f667,plain,(
% 0.14/5.52 $false|~sQ36_spl|~sQ19_spl),
% 0.14/5.52 inference(forward_subsumption_resolution,[status(thm)],[f666,f305])).
% 0.14/5.52 fof(f668,plain,(
% 0.14/5.52 ~sQ36_spl|~sQ19_spl),
% 0.14/5.52 inference(contradiction_clause,[status(thm)],[f667])).
% 0.14/5.52 fof(f671,plain,(
% 0.14/5.52 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0)))),
% 0.14/5.52 inference(forward_subsumption_resolution,[status(thm)],[f170,f152])).
% 0.14/5.52 fof(f672,plain,(
% 0.14/5.52 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n1))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))),
% 0.14/5.52 inference(paramodulation,[status(thm)],[f230,f671])).
% 0.14/5.52 fof(f675,definition,(
% 0.14/5.52 sQ54_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n0)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f678,plain,(
% 0.14/5.52 sQ54_spl|~sQ33_spl|sQ41_spl|~sQ42_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f672,f675,f515,f598,f601])).
% 0.14/5.52 fof(f689,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(n0,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(n0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|sQ42_spl),
% 0.14/5.52 inference(resolution,[status(thm)],[f603,f523])).
% 0.14/5.52 fof(f690,definition,(
% 0.14/5.52 sQ57_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(n0,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(n0))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f691,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(n0,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(n0)|~sQ57_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f690])).
% 0.14/5.52 fof(f693,plain,(
% 0.14/5.52 sQ57_spl|sQ41_spl|sQ12_spl|sQ42_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f689,f690,f598,f388,f601])).
% 0.14/5.52 fof(f694,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(n0,n1))=f_SUB_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n1)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ41_spl),
% 0.14/5.52 inference(resolution,[status(thm)],[f599,f433])).
% 0.14/5.52 fof(f695,definition,(
% 0.14/5.52 sQ58_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(n0,n1))=f_SUB_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n1))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f698,definition,(
% 0.14/5.52 sQ59_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n0))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f699,plain,(
% 0.14/5.52 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n0)|~sQ59_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f698])).
% 0.14/5.52 fof(f701,plain,(
% 0.14/5.52 sQ58_spl|sQ59_spl|sQ42_spl|sQ12_spl|~sQ41_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f694,f695,f698,f601,f388,f598])).
% 0.14/5.52 fof(f704,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTlevel_(n1)=fwork_DOTfifo_DOTrtl_DOTlevel_(n0)|~sQ57_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f230,f691])).
% 0.14/5.52 fof(f706,plain,(
% 0.14/5.52 ![X0,X1]: (p_LES_EQU_(X0,X1)|p_LES_EQU_(X1,X0))),
% 0.14/5.52 inference(resolution,[status(thm)],[f224,f228])).
% 0.14/5.52 fof(f715,plain,(
% 0.14/5.52 ![X0]: (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X0,n1))=fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(X0),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.52 inference(backward_subsumption_resolution,[status(thm)],[f550,f174])).
% 0.14/5.52 fof(f784,plain,(
% 0.14/5.52 n0=fwork_DOTfifo_DOTrtl_DOTlevel_(n0)|p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n1),n0)|~sQ59_spl),
% 0.14/5.52 inference(resolution,[status(thm)],[f699,f220])).
% 0.14/5.52 fof(f786,definition,(
% 0.14/5.52 sQ70_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(n0)=n0)),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f787,plain,(
% 0.14/5.52 fwork_DOTfifo_DOTrtl_DOTlevel_(n0)=n0|~sQ70_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f786])).
% 0.14/5.52 fof(f789,definition,(
% 0.14/5.52 sQ71_spl <=> (p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTlevel_(n0)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f791,plain,(
% 0.14/5.52 ~p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTlevel_(n0))|sQ71_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f789])).
% 0.14/5.52 fof(f793,definition,(
% 0.14/5.52 sQ72_spl <=> (p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n1),n0))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.14/5.52 fof(f794,plain,(
% 0.14/5.52 p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n1),n0)|~sQ72_spl),
% 0.14/5.52 inference(component_clause,[status(thm)],[f793])).
% 0.14/5.52 fof(f796,plain,(
% 0.14/5.52 sQ70_spl|sQ72_spl|~sQ59_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f784,f786,f793,f698])).
% 0.14/5.52 fof(f798,plain,(
% 0.14/5.52 $false|~sQ72_spl),
% 0.14/5.52 inference(forward_subsumption_resolution,[status(thm)],[f794,f212])).
% 0.14/5.52 fof(f799,plain,(
% 0.14/5.52 ~sQ72_spl),
% 0.14/5.52 inference(contradiction_clause,[status(thm)],[f798])).
% 0.14/5.52 fof(f809,plain,(
% 0.14/5.52 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(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/5.52 inference(forward_demodulation,[status(thm)],[f143,f179])).
% 0.14/5.53 fof(f810,plain,(
% 0.14/5.53 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(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)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f809,f152])).
% 0.14/5.53 fof(f812,plain,(
% 0.14/5.53 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n1))|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f230,f810])).
% 0.14/5.53 fof(f816,plain,(
% 0.14/5.53 ~sQ33_spl|sQ59_spl|~sQ41_spl|~sQ42_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f812,f515,f698,f598,f601])).
% 0.14/5.53 fof(f870,definition,(
% 0.14/5.53 sQ84_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(n0,n1))))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f871,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(n0,n1)))|~sQ84_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f870])).
% 0.14/5.53 fof(f874,definition,(
% 0.14/5.53 sQ85_spl <=> (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(n0,n1))=fwork_DOTfifo_DOTrtl_DOTwr__level_(n0))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f878,definition,(
% 0.14/5.53 sQ86_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(n0)))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f879,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(n0))|~sQ86_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f878])).
% 0.14/5.53 fof(f884,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(n1))|~sQ84_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f230,f871])).
% 0.14/5.53 fof(f885,plain,(
% 0.14/5.53 $false|sQ11_spl|~sQ84_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f884,f387])).
% 0.14/5.53 fof(f886,plain,(
% 0.14/5.53 sQ11_spl|~sQ84_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f885])).
% 0.14/5.53 fof(f890,plain,(
% 0.14/5.53 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)|~sQ70_spl|~sQ40_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f787,f596])).
% 0.14/5.53 fof(f891,plain,(
% 0.14/5.53 $false|~sQ70_spl|~sQ40_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f890,f305])).
% 0.14/5.53 fof(f892,plain,(
% 0.14/5.53 ~sQ70_spl|~sQ40_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f891])).
% 0.14/5.53 fof(f906,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(n0,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n1)|~p_LES_EQU_(n0,n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ70_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f787,f369])).
% 0.14/5.53 fof(f909,definition,(
% 0.14/5.53 sQ88_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(n0,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n1))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f910,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(n0,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n1)|~sQ88_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f909])).
% 0.14/5.53 fof(f912,definition,(
% 0.14/5.53 sQ89_spl <=> (p_LES_EQU_(n0,n0))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f914,plain,(
% 0.14/5.53 ~p_LES_EQU_(n0,n0)|sQ89_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f912])).
% 0.14/5.53 fof(f915,plain,(
% 0.14/5.53 sQ88_spl|~sQ89_spl|~sQ41_spl|~sQ42_spl|sQ12_spl|~sQ70_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f906,f909,f912,f598,f601,f388,f786])).
% 0.14/5.53 fof(f923,plain,(
% 0.14/5.53 $false|sQ89_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f914,f228])).
% 0.14/5.53 fof(f924,plain,(
% 0.14/5.53 sQ89_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f923])).
% 0.14/5.53 fof(f925,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(n1)=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n1)|~sQ88_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f230,f910])).
% 0.14/5.53 fof(f926,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(n1)=f_ADD_(n0,n1)|~sQ70_spl|~sQ88_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f787,f925])).
% 0.14/5.53 fof(f927,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(n1)=n1|~sQ70_spl|~sQ88_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f230,f926])).
% 0.14/5.53 fof(f928,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(n0)=fwork_DOTfifo_DOTrtl_DOTfifo__length_|~sQ86_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f879,f309])).
% 0.14/5.53 fof(f929,plain,(
% 0.14/5.53 ![X0]: (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__level_(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.14/5.53 inference(forward_demodulation,[status(thm)],[f143,f180])).
% 0.14/5.53 fof(f930,plain,(
% 0.14/5.53 ![X0]: (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__level_(X0)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X0),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f929,f157])).
% 0.14/5.53 fof(f931,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(n0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__level_(n0)|~p_LES_EQU_(n0,n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ70_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f787,f930])).
% 0.14/5.53 fof(f934,definition,(
% 0.14/5.53 sQ91_spl <=> (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(n0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__level_(n0))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f937,plain,(
% 0.14/5.53 sQ91_spl|~sQ89_spl|~sQ42_spl|sQ12_spl|~sQ70_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f931,f934,f912,f601,f388,f786])).
% 0.14/5.53 fof(f947,plain,(
% 0.14/5.53 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(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/5.53 inference(forward_demodulation,[status(thm)],[f143,f182])).
% 0.14/5.53 fof(f948,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(n0,n1)))|~p_LES_EQU_(n0,n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ70_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f787,f947])).
% 0.14/5.53 fof(f951,definition,(
% 0.14/5.53 sQ94_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(n0,n1))))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f952,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(n0,n1)))|~sQ94_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f951])).
% 0.14/5.53 fof(f954,plain,(
% 0.14/5.53 sQ94_spl|~sQ89_spl|~sQ41_spl|~sQ42_spl|sQ12_spl|~sQ70_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f948,f951,f912,f598,f601,f388,f786])).
% 0.14/5.53 fof(f963,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n1))|~sQ94_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f230,f952])).
% 0.14/5.53 fof(f964,plain,(
% 0.14/5.53 $false|sQ33_spl|~sQ94_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f963,f517])).
% 0.14/5.53 fof(f965,plain,(
% 0.14/5.53 sQ33_spl|~sQ94_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f964])).
% 0.14/5.53 fof(f982,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(n1))|~n1=fwork_DOTfifo_DOTrtl_DOTfifo__length_|~sQ70_spl|~sQ88_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f927,f308])).
% 0.14/5.53 fof(f986,definition,(
% 0.14/5.53 sQ99_spl <=> (p_LES_EQU_(n1,n0))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1010,definition,(
% 0.14/5.53 sQ106_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1018,definition,(
% 0.14/5.53 sQ108_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(n1)))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1021,definition,(
% 0.14/5.53 sQ109_spl <=> (n1=fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1024,plain,(
% 0.14/5.53 sQ108_spl|~sQ109_spl|~sQ70_spl|~sQ88_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f982,f1018,f1021,f786,f909])).
% 0.14/5.53 fof(f1026,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTfifo__length_=n0|~sQ86_spl|~sQ70_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f928,f787])).
% 0.14/5.53 fof(f1034,plain,(
% 0.14/5.53 $false|sQ1_spl|~sQ86_spl|~sQ70_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1026,f333])).
% 0.14/5.53 fof(f1035,plain,(
% 0.14/5.53 sQ1_spl|~sQ86_spl|~sQ70_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1034])).
% 0.14/5.53 fof(f1048,definition,(
% 0.14/5.53 ![X0,X1]: (sQ111_spl <=> (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),X1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),X1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|X1=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p_LES_EQU_(n0,X1)|~p_LES_EQU_(X1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1049,plain,(
% 0.14/5.53 ![X0,X1]: (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),X1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),X1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|X1=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p_LES_EQU_(n0,X1)|~p_LES_EQU_(X1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))|~sQ111_spl)),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1048])).
% 0.14/5.53 fof(f1052,plain,(
% 0.14/5.53 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X0,n1)))|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0)))),
% 0.14/5.53 inference(backward_subsumption_resolution,[status(thm)],[f590,f1053])).
% 0.14/5.53 fof(f1053,plain,(
% 0.14/5.53 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X0,n1)))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f189,f151])).
% 0.14/5.53 fof(f1087,definition,(
% 0.14/5.53 ![X0,X1]: (sQ115_spl <=> (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),X1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),X1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|X1=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p_LES_EQU_(n0,X1)|~p_LES_EQU_(X1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1088,plain,(
% 0.14/5.53 ![X0,X1]: (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),X1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),X1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|X1=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p_LES_EQU_(n0,X1)|~p_LES_EQU_(X1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))|~sQ115_spl)),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1087])).
% 0.14/5.53 fof(f1115,plain,(
% 0.14/5.53 ![X0]: (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTwr__level_(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/5.53 inference(backward_subsumption_resolution,[status(thm)],[f626,f190])).
% 0.14/5.53 fof(f1116,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(n0,n1))=fwork_DOTfifo_DOTrtl_DOTwr__level_(n0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|sQ42_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f190,f603])).
% 0.14/5.53 fof(f1117,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTwr__level_(t_206)|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/5.53 inference(resolution,[status(thm)],[f190,f301])).
% 0.14/5.53 fof(f1124,plain,(
% 0.14/5.53 sQ85_spl|sQ12_spl|sQ42_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1116,f874,f388,f601])).
% 0.14/5.53 fof(f1125,plain,(
% 0.14/5.53 sQ49_spl|sQ21_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1117,f629,f444])).
% 0.14/5.53 fof(f1155,plain,(
% 0.14/5.53 ![X0]: (p_LES_EQU_(X0,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),X0))),
% 0.14/5.53 inference(resolution,[status(thm)],[f300,f224])).
% 0.14/5.53 fof(f1186,plain,(
% 0.14/5.53 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(n0,n1)))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ42_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f602,f171])).
% 0.14/5.53 fof(f1188,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(n0,n1))=f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n1)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ42_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f602,f317])).
% 0.14/5.53 fof(f1190,definition,(
% 0.14/5.53 sQ125_spl <=> (fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(n0,n1))=fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(n0),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1194,plain,(
% 0.14/5.53 ~sQ54_spl|sQ94_spl|sQ41_spl|sQ12_spl|~sQ42_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1186,f675,f951,f598,f388,f601])).
% 0.14/5.53 fof(f1196,plain,(
% 0.14/5.53 sQ88_spl|sQ40_spl|sQ41_spl|sQ12_spl|~sQ42_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1188,f909,f595,f598,f388,f601])).
% 0.14/5.53 fof(f1198,plain,(
% 0.14/5.53 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(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/5.53 inference(forward_demodulation,[status(thm)],[f143,f195])).
% 0.14/5.53 fof(f1199,plain,(
% 0.14/5.53 ![X0]: (~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X0),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1198,f810])).
% 0.14/5.53 fof(f1200,plain,(
% 0.14/5.53 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n1))|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f230,f1199])).
% 0.14/5.53 fof(f1203,plain,(
% 0.14/5.53 ~sQ33_spl|sQ59_spl|~sQ41_spl|sQ12_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1200,f515,f698,f598,f388])).
% 0.14/5.53 fof(f1208,plain,(
% 0.14/5.53 ![X0]: (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__level_(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.14/5.53 inference(forward_demodulation,[status(thm)],[f143,f197])).
% 0.14/5.53 fof(f1209,plain,(
% 0.14/5.53 ![X0]: (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__level_(X0)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X0),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1208,f930])).
% 0.14/5.53 fof(f1212,plain,(
% 0.14/5.53 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(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/5.53 inference(forward_demodulation,[status(thm)],[f143,f198])).
% 0.14/5.53 fof(f1213,plain,(
% 0.14/5.53 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X0),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1212,f947])).
% 0.14/5.53 fof(f1231,plain,(
% 0.14/5.53 ![X0]: (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__level_(X0)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(X0),n0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.53 inference(backward_subsumption_resolution,[status(thm)],[f1209,f1232])).
% 0.14/5.53 fof(f1232,plain,(
% 0.14/5.53 ![X0]: (fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(X0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__level_(X0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f202,f157])).
% 0.14/5.53 fof(f1237,plain,(
% 0.14/5.53 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(X0,n1)))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f203,f671])).
% 0.14/5.53 fof(f1238,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(n1))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f230,f1237])).
% 0.14/5.53 fof(f1241,plain,(
% 0.14/5.53 sQ54_spl|~sQ33_spl|sQ41_spl|sQ12_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1238,f675,f515,f598,f388])).
% 0.14/5.53 fof(f1246,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(n0,n1))=fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTwr__level_(n0),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ42_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f715,f602])).
% 0.14/5.53 fof(f1249,plain,(
% 0.14/5.53 sQ125_spl|sQ40_spl|sQ12_spl|~sQ42_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1246,f1190,f595,f388,f601])).
% 0.14/5.53 fof(f1253,plain,(
% 0.14/5.53 ~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(n1))|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(n0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f230,f1052])).
% 0.14/5.53 fof(f1256,plain,(
% 0.14/5.53 ~sQ11_spl|sQ40_spl|~sQ42_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1253,f385,f595,f601])).
% 0.14/5.53 fof(f1288,plain,(
% 0.14/5.53 ![X0]: (p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(X0,n1)))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f207,f151])).
% 0.14/5.53 fof(f1289,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(n0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(n1))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f230,f1288])).
% 0.14/5.53 fof(f1292,definition,(
% 0.14/5.53 sQ130_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(n0)))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1293,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(n0))|~sQ130_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1292])).
% 0.14/5.53 fof(f1295,plain,(
% 0.14/5.53 sQ130_spl|~sQ11_spl|sQ42_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1289,f1292,f385,f601])).
% 0.14/5.53 fof(f1304,plain,(
% 0.14/5.53 p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))),
% 0.14/5.53 inference(resolution,[status(thm)],[f1155,f521])).
% 0.14/5.53 fof(f1318,definition,(
% 0.14/5.53 sQ132_spl <=> (p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTfifo__length_))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1319,plain,(
% 0.14/5.53 p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~sQ132_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1318])).
% 0.14/5.53 fof(f1322,plain,(
% 0.14/5.53 sQ132_spl|sQ34_spl|sQ20_spl|sQ21_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1304,f1318,f526,f441,f444])).
% 0.14/5.53 fof(f1351,definition,(
% 0.14/5.53 sQ140_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n0)),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1352,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n0|~sQ140_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1351])).
% 0.14/5.53 fof(f1393,plain,(
% 0.14/5.53 ~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_)|p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n0)|~sQ18_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f452,f213])).
% 0.14/5.53 fof(f1398,definition,(
% 0.14/5.53 sQ147_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1400,plain,(
% 0.14/5.53 ~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_)|sQ147_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1398])).
% 0.14/5.53 fof(f1401,plain,(
% 0.14/5.53 ~sQ147_spl|sQ19_spl|~sQ18_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1393,f1398,f438,f435])).
% 0.14/5.53 fof(f1402,plain,(
% 0.14/5.53 $false|sQ147_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1400,f300])).
% 0.14/5.53 fof(f1403,plain,(
% 0.14/5.53 sQ147_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1402])).
% 0.14/5.53 fof(f1406,plain,(
% 0.14/5.53 n0=fwork_DOTfifo_DOTrtl_DOTfifo__length_|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)|~sQ132_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f1319,f222])).
% 0.14/5.53 fof(f1407,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTfifo__length_=n0|p_LES_EQU_(f_ADD_(n0,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~sQ132_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f1319,f220])).
% 0.14/5.53 fof(f1409,plain,(
% 0.14/5.53 sQ1_spl|~sQ10_spl|~sQ132_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1406,f331,f374,f1318])).
% 0.14/5.53 fof(f1410,definition,(
% 0.14/5.53 sQ148_spl <=> (p_LES_EQU_(f_ADD_(n0,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1411,plain,(
% 0.14/5.53 p_LES_EQU_(f_ADD_(n0,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~sQ148_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1410])).
% 0.14/5.53 fof(f1413,plain,(
% 0.14/5.53 sQ1_spl|sQ148_spl|~sQ132_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1407,f331,f1410,f1318])).
% 0.14/5.53 fof(f1415,plain,(
% 0.14/5.53 p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~sQ148_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f230,f1411])).
% 0.14/5.53 fof(f1453,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(n0,n1)))|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ130_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f1293,f208])).
% 0.14/5.53 fof(f1454,plain,(
% 0.14/5.53 sQ84_spl|sQ42_spl|sQ12_spl|~sQ130_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1453,f870,f601,f388,f1292])).
% 0.14/5.53 fof(f1465,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1))=fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)|~p_LES_EQU_(n0,n0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))|~sQ140_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f1352,f521])).
% 0.14/5.53 fof(f1475,plain,(
% 0.14/5.53 sQ34_spl|~sQ89_spl|sQ20_spl|sQ21_spl|~sQ140_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1465,f526,f912,f441,f444,f1351])).
% 0.14/5.53 fof(f1476,definition,(
% 0.14/5.53 sQ154_spl <=> (n0=n0)),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1478,plain,(
% 0.14/5.53 ~n0=n0|sQ154_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1476])).
% 0.14/5.53 fof(f1483,plain,(
% 0.14/5.53 $false|sQ154_spl),
% 0.14/5.53 inference(trivial_equality_resolution,[status(thm)],[f1478])).
% 0.14/5.53 fof(f1484,plain,(
% 0.14/5.53 sQ154_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1483])).
% 0.14/5.53 fof(f1553,plain,(
% 0.14/5.53 n1=fwork_DOTfifo_DOTrtl_DOTfifo__length_|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1)|~sQ148_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f1415,f222])).
% 0.14/5.53 fof(f1554,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTfifo__length_=n1|p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~sQ148_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f1415,f220])).
% 0.14/5.53 fof(f1556,plain,(
% 0.14/5.53 sQ109_spl|~sQ106_spl|~sQ148_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1553,f1021,f1010,f1410])).
% 0.14/5.53 fof(f1557,definition,(
% 0.14/5.53 sQ155_spl <=> (p_LES_EQU_(f_ADD_(n1,n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1560,plain,(
% 0.14/5.53 sQ109_spl|sQ155_spl|~sQ148_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1554,f1021,f1557,f1410])).
% 0.14/5.53 fof(f1772,plain,(
% 0.14/5.53 p_LES_EQU_(n0,n1)),
% 0.14/5.53 inference(resolution,[status(thm)],[f706,f535])).
% 0.14/5.53 fof(f1811,plain,(
% 0.14/5.53 n0=n1|~p_LES_EQU_(n1,n0)),
% 0.14/5.53 inference(resolution,[status(thm)],[f1772,f222])).
% 0.14/5.53 fof(f1812,definition,(
% 0.14/5.53 sQ163_spl <=> (n0=n1)),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1813,plain,(
% 0.14/5.53 n0=n1|~sQ163_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1812])).
% 0.14/5.53 fof(f1815,plain,(
% 0.14/5.53 sQ163_spl|~sQ99_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1811,f1812,f986])).
% 0.14/5.53 fof(f1816,plain,(
% 0.14/5.53 $false|~sQ163_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1813,f360])).
% 0.14/5.53 fof(f1817,plain,(
% 0.14/5.53 ~sQ163_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1816])).
% 0.14/5.53 fof(f1859,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(n0,n1)))|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(n1),n0)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ57_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f704,f1213])).
% 0.14/5.53 fof(f1860,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(n0,n1))=fwork_DOTfifo_DOTrtl_DOTwr__level_(n0)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(n1))|p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(n0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ57_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f704,f1115])).
% 0.14/5.53 fof(f1861,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(n0,n1))=fwork_DOTfifo_DOTrtl_DOTrd__level_(n0)|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(n1),n0)|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(n0))|~sQ57_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f704,f1231])).
% 0.14/5.53 fof(f1862,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(n0))|~fwork_DOTfifo_DOTrtl_DOTlevel_(n1)=n0|~sQ57_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f704,f321])).
% 0.14/5.53 fof(f1863,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(n0))|~fwork_DOTfifo_DOTrtl_DOTlevel_(n1)=fwork_DOTfifo_DOTrtl_DOTfifo__length_|~sQ57_spl),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f704,f308])).
% 0.14/5.53 fof(f1864,definition,(
% 0.14/5.53 sQ166_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(n1),n0))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1867,plain,(
% 0.14/5.53 sQ94_spl|~sQ166_spl|~sQ41_spl|sQ12_spl|~sQ57_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1859,f951,f1864,f598,f388,f690])).
% 0.14/5.53 fof(f1868,definition,(
% 0.14/5.53 sQ167_spl <=> (p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTlevel_(n1)))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1871,plain,(
% 0.14/5.53 sQ85_spl|~sQ167_spl|sQ41_spl|sQ12_spl|~sQ57_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1860,f874,f1868,f598,f388,f690])).
% 0.14/5.53 fof(f1872,plain,(
% 0.14/5.53 sQ91_spl|~sQ166_spl|sQ12_spl|~sQ57_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1861,f934,f1864,f388,f690])).
% 0.14/5.53 fof(f1873,definition,(
% 0.14/5.53 sQ168_spl <=> (p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(n0)))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1874,plain,(
% 0.14/5.53 p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(n0))|~sQ168_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1873])).
% 0.14/5.53 fof(f1876,definition,(
% 0.14/5.53 sQ169_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(n1)=n0)),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1879,plain,(
% 0.14/5.53 sQ168_spl|~sQ169_spl|~sQ57_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1862,f1873,f1876,f690])).
% 0.14/5.53 fof(f1880,definition,(
% 0.14/5.53 sQ170_spl <=> (fwork_DOTfifo_DOTrtl_DOTlevel_(n1)=fwork_DOTfifo_DOTrtl_DOTfifo__length_)),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1883,plain,(
% 0.14/5.53 sQ86_spl|~sQ170_spl|~sQ57_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1863,f878,f1880,f690])).
% 0.14/5.53 fof(f1891,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(n0)=n0|~sQ168_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f1874,f322])).
% 0.14/5.53 fof(f1892,plain,(
% 0.14/5.53 sQ70_spl|~sQ168_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1891,f786,f1873])).
% 0.14/5.53 fof(f1917,plain,(
% 0.14/5.53 ![X0]: (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),n1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),n1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|n1=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))|~sQ115_spl)),
% 0.14/5.53 inference(resolution,[status(thm)],[f1088,f1772])).
% 0.14/5.53 fof(f1918,plain,(
% 0.14/5.53 ![X0]: (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),fwork_DOTfifo_DOTrtl_DOTfifo__length_),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),fwork_DOTfifo_DOTrtl_DOTfifo__length_),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|fwork_DOTfifo_DOTrtl_DOTfifo__length_=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))|~sQ115_spl|~sQ132_spl)),
% 0.14/5.53 inference(resolution,[status(thm)],[f1088,f1319])).
% 0.14/5.53 fof(f1920,plain,(
% 0.14/5.53 ![X0]: (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),n0),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),n0),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|n0=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))|~sQ115_spl)),
% 0.14/5.53 inference(resolution,[status(thm)],[f1088,f706])).
% 0.14/5.53 fof(f1925,definition,(
% 0.14/5.53 ![X0]: (sQ171_spl <=> (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),n1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),n1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|n1=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1928,definition,(
% 0.14/5.53 sQ172_spl <=> (p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1930,plain,(
% 0.14/5.53 ~p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|sQ172_spl),
% 0.14/5.53 inference(component_clause,[status(thm)],[f1928])).
% 0.14/5.53 fof(f1931,plain,(
% 0.14/5.53 sQ171_spl|~sQ172_spl|~sQ115_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1917,f1925,f1928,f1087])).
% 0.14/5.53 fof(f1932,definition,(
% 0.14/5.53 ![X0]: (sQ173_spl <=> (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),fwork_DOTfifo_DOTrtl_DOTfifo__length_),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),fwork_DOTfifo_DOTrtl_DOTfifo__length_),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|fwork_DOTfifo_DOTrtl_DOTfifo__length_=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1935,plain,(
% 0.14/5.53 sQ173_spl|~sQ3_spl|~sQ115_spl|~sQ132_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1918,f1932,f338,f1087,f1318])).
% 0.14/5.53 fof(f1936,definition,(
% 0.14/5.53 ![X0]: (sQ174_spl <=> (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),n0),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),n0),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|n0=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))))),
% 0.14/5.53 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1943,plain,(
% 0.14/5.53 sQ174_spl|~sQ132_spl|~sQ115_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1920,f1936,f1318,f1087])).
% 0.14/5.53 fof(f1946,plain,(
% 0.14/5.53 $false|~sQ148_spl|sQ172_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1930,f1415])).
% 0.14/5.53 fof(f1947,plain,(
% 0.14/5.53 ~sQ148_spl|sQ172_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1946])).
% 0.14/5.53 fof(f1962,plain,(
% 0.14/5.53 ![X0]: (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),n1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),n1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|n1=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))|~sQ111_spl)),
% 0.14/5.53 inference(resolution,[status(thm)],[f1049,f1772])).
% 0.14/5.53 fof(f1963,plain,(
% 0.14/5.53 ![X0]: (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),fwork_DOTfifo_DOTrtl_DOTfifo__length_),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),fwork_DOTfifo_DOTrtl_DOTfifo__length_),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|fwork_DOTfifo_DOTrtl_DOTfifo__length_=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))|~sQ111_spl|~sQ132_spl)),
% 0.14/5.53 inference(resolution,[status(thm)],[f1049,f1319])).
% 0.14/5.53 fof(f1965,plain,(
% 0.14/5.53 ![X0]: (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),n0),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),n0),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|n0=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__level_(X0))|~p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTfifo__length_)|~p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))|~p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))|p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))|~sQ111_spl)),
% 0.14/5.53 inference(resolution,[status(thm)],[f1049,f706])).
% 0.14/5.53 fof(f1970,definition,(
% 0.14/5.53 ![X0]: (sQ176_spl <=> (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),n1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),n1),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|n1=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__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/5.53 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1973,plain,(
% 0.14/5.53 sQ176_spl|~sQ172_spl|~sQ111_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1962,f1970,f1928,f1048])).
% 0.14/5.53 fof(f1974,definition,(
% 0.14/5.53 ![X0]: (sQ177_spl <=> (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),fwork_DOTfifo_DOTrtl_DOTfifo__length_),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),fwork_DOTfifo_DOTrtl_DOTfifo__length_),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|fwork_DOTfifo_DOTrtl_DOTfifo__length_=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__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/5.53 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1977,plain,(
% 0.14/5.53 sQ177_spl|~sQ3_spl|~sQ111_spl|~sQ132_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1963,f1974,f338,f1048,f1318])).
% 0.14/5.53 fof(f1978,definition,(
% 0.14/5.53 ![X0]: (sQ178_spl <=> (f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(X0,n1)),n0),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))=f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(X0),n0),f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))|n0=f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTwr__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/5.53 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 0.14/5.53 fof(f1982,plain,(
% 0.14/5.53 sQ178_spl|~sQ132_spl|~sQ111_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1965,f1978,f1318,f1048])).
% 0.14/5.53 fof(f1991,plain,(
% 0.14/5.53 p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(n0),n0)|sQ71_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f791,f706])).
% 0.14/5.53 fof(f1993,plain,(
% 0.14/5.53 sQ59_spl|sQ71_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1991,f698,f789])).
% 0.14/5.53 fof(f2025,plain,(
% 0.14/5.53 fwork_DOTfifo_DOTrtl_DOTlevel_(t_206)=n0|~sQ19_spl),
% 0.14/5.53 inference(resolution,[status(thm)],[f439,f226])).
% 0.14/5.53 fof(f2031,plain,(
% 0.14/5.53 sQ140_spl|~sQ19_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2025,f1351,f438])).
% 0.14/5.53 fof(f2033,plain,(
% 0.14/5.53 $false),
% 0.14/5.53 inference(sat_refutation,[status(thm)],[f334,f357,f359,f391,f430,f447,f449,f451,f510,f514,f518,f546,f638,f668,f678,f693,f701,f796,f799,f816,f886,f892,f915,f924,f937,f954,f965,f1024,f1035,f1124,f1125,f1194,f1196,f1203,f1241,f1249,f1256,f1295,f1322,f1401,f1403,f1409,f1413,f1454,f1475,f1484,f1556,f1560,f1815,f1817,f1867,f1871,f1872,f1879,f1883,f1892,f1931,f1935,f1943,f1947,f1973,f1977,f1982,f1993,f2031])).
% 0.14/5.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.55 % Elapsed time: 0.160757 seconds
% 0.14/5.55 % CPU time: 0.966535 seconds
% 0.14/5.55 % Total memory used: 123.590 MB
% 0.14/5.55 % Net memory used: 121.194 MB
%------------------------------------------------------------------------------