%--------------------------------------------------------------------------
% File     : HWV004-0 : TPTP v7.2.0. Released v2.5.0.
% Domain   : Hardware Verification
% Axioms   : Axioms from a VHDL design description
% Version  : [Mar02] axioms : Especial.
%            Axiom formulation : Different VHDL -> FO-logic translator
% English  :

% Refs     : [Mar02] Martensson (2002), Email to G. Sutcliffe
% Source   : [Mar02]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of clauses    :  133 (  62 non-Horn;  25 unit;  92 RR)
%            Number of atoms      :  415 (  80 equality)
%            Maximal clause size  :   10 (   3 average)
%            Number of predicates :    4 (   0 propositional; 1-2 arity)
%            Number of functors   :   46 (   8 constant; 0-3 arity)
%            Number of variables  :  225 (  20 singleton)
%            Maximal term depth   :    5 (   2 average)
% SPC      : 

% Comments : Generated by Safelogic's Haskell Library
%--------------------------------------------------------------------------
cnf(axiom_2,axiom,
    ( f__length_(fwork_DOTfifo_DOTrtl_DOTmem_(Vt___)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),n1) )).

cnf(axiom_3,axiom,
    ( f__length_(fwork_DOTfifo_DOTrtl_DOTdata__out_(Vt___)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1),n1) )).

cnf(axiom_4,axiom,
    ( f__length_(fwork_DOTfifo_DOTrtl_DOTdata__in_(Vt___)) = f_ADD_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1),n1) )).

cnf(axiom_5,axiom,
    ( fwork_DOTfifo_DOTrtl_DOTlevel_(T_0) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_0) )).

cnf(axiom_6,axiom,
    ( p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(T_1))
    | fwork_DOTfifo_DOTrtl_DOTint__level_(T_1) != fwork_DOTfifo_DOTrtl_DOTfifo__length_ )).

cnf(axiom_7,axiom,
    ( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(T_2))
    | fwork_DOTfifo_DOTrtl_DOTint__level_(T_2) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ )).

cnf(axiom_8,axiom,
    ( p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_3))
    | fwork_DOTfifo_DOTrtl_DOTint__level_(T_3) != n0 )).

cnf(axiom_9,axiom,
    ( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTempty_(T_4))
    | fwork_DOTfifo_DOTrtl_DOTint__level_(T_4) = n0 )).

cnf(axiom_10,axiom,
    ( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_5,n1)) = n0
    | ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)) )).

cnf(axiom_11,axiom,
    ( fwork_DOTfifo_DOTrtl_DOTwr__level_(f_ADD_(T_5,n1)) = n0
    | ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)) )).

cnf(axiom_12,axiom,
    ( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_5,n1)) = n0
    | ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)) )).

cnf(axiom_13,axiom,
    ( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr__error_(f_ADD_(T_5,n1)))
    | ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)) )).

cnf(axiom_14,axiom,
    ( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd__error_(f_ADD_(T_5,n1)))
    | ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_5)) )).

cnf(axiom_15,axiom,
    ( ~ 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)) )).

cnf(axiom_16,axiom,
    ( ~ 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)) )).

cnf(axiom_17,axiom,
    ( 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)) )).

cnf(axiom_18,axiom,
    ( 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)) )).

cnf(axiom_19,axiom,
    ( 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)) )).

cnf(axiom_20,axiom,
    ( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13))),I1_14) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__in_(T_13),I1_14)
    | ~ p_LES_EQU_(n0,I1_14)
    | ~ p_LES_EQU_(I1_14,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,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)) )).

cnf(axiom_21,axiom,
    ( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),Cindex_16),I1_17) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),Cindex_16),I1_17)
    | ~ p_LES_EQU_(n0,I1_17)
    | ~ p_LES_EQU_(I1_17,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
    | Cindex_16 = f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13))
    | ~ p_LES_EQU_(n0,Cindex_16)
    | ~ p_LES_EQU_(Cindex_16,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,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)) )).

cnf(axiom_22,axiom,
    ( ~ 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)) )).

cnf(axiom_23,axiom,
    ( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(T_13,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(T_13)
    | ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(T_13))
    | p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(T_13))
    | ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
    | p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13)) )).

cnf(axiom_24,axiom,
    ( 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)) )).

cnf(axiom_25,axiom,
    ( 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)) )).

cnf(axiom_26,axiom,
    ( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),I1_22),I2_23) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),I1_22),I2_23)
    | ~ p_LES_EQU_(n0,I2_23)
    | ~ p_LES_EQU_(I2_23,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
    | ~ p_LES_EQU_(n0,I1_22)
    | ~ p_LES_EQU_(I1_22,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,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)) )).

cnf(axiom_27,axiom,
    ( 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)) )).

cnf(axiom_28,axiom,
    ( ~ 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)) )).

cnf(axiom_29,axiom,
    ( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_31) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(T_13),I1_31)
    | ~ p_LES_EQU_(n0,I1_31)
    | ~ p_LES_EQU_(I1_31,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,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)) )).

cnf(axiom_30,axiom,
    ( 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)) )).

cnf(axiom_31,axiom,
    ( 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)) )).

cnf(axiom_32,axiom,
    ( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
    | 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)) )).

cnf(axiom_33,axiom,
    ( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_35) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13))),I1_35)
    | ~ p_LES_EQU_(n0,I1_35)
    | ~ p_LES_EQU_(I1_35,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,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)) )).

cnf(axiom_34,axiom,
    ( ~ 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)) )).

cnf(axiom_35,axiom,
    ( 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)) )).

cnf(axiom_36,axiom,
    ( 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)) )).

cnf(axiom_37,axiom,
    ( 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)) )).

cnf(axiom_38,axiom,
    ( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_39) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(T_13),I1_39)
    | ~ p_LES_EQU_(n0,I1_39)
    | ~ p_LES_EQU_(I1_39,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,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)) )).

cnf(axiom_39,axiom,
    ( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13))),I1_43) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__in_(T_13),I1_43)
    | ~ p_LES_EQU_(n0,I1_43)
    | ~ p_LES_EQU_(I1_43,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,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)) )).

cnf(axiom_40,axiom,
    ( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),Cindex_45),I1_46) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),Cindex_45),I1_46)
    | ~ p_LES_EQU_(n0,I1_46)
    | ~ p_LES_EQU_(I1_46,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
    | Cindex_45 = f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTwr__level_(T_13))
    | ~ p_LES_EQU_(n0,Cindex_45)
    | ~ p_LES_EQU_(Cindex_45,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,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)) )).

cnf(axiom_41,axiom,
    ( ~ 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)) )).

cnf(axiom_42,axiom,
    ( 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)) )).

cnf(axiom_43,axiom,
    ( 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)) )).

cnf(axiom_44,axiom,
    ( fwork_DOTfifo_DOTrtl_DOTrd__level_(f_ADD_(T_13,n1)) = fstd_DOTstandard_DOTmod_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
    | 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)) )).

cnf(axiom_45,axiom,
    ( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_53) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),f_SUB_(f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1),fwork_DOTfifo_DOTrtl_DOTrd__level_(T_13))),I1_53)
    | ~ p_LES_EQU_(n0,I1_53)
    | ~ p_LES_EQU_(I1_53,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,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)) )).

cnf(axiom_46,axiom,
    ( ~ 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)) )).

cnf(axiom_47,axiom,
    ( 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)) )).

cnf(axiom_48,axiom,
    ( 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)) )).

cnf(axiom_49,axiom,
    ( 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)) )).

cnf(axiom_50,axiom,
    ( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_57) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(T_13),I1_57)
    | ~ p_LES_EQU_(n0,I1_57)
    | ~ p_LES_EQU_(I1_57,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,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)) )).

cnf(axiom_51,axiom,
    ( 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)) )).

cnf(axiom_52,axiom,
    ( 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)) )).

cnf(axiom_53,axiom,
    ( 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)) )).

cnf(axiom_54,axiom,
    ( ~ 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)) )).

cnf(axiom_55,axiom,
    ( f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(f_ADD_(T_13,n1)),I1_66) = f__index_(fwork_DOTfifo_DOTrtl_DOTdata__out_(T_13),I1_66)
    | ~ p_LES_EQU_(n0,I1_66)
    | ~ p_LES_EQU_(I1_66,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,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)) )).

cnf(axiom_56,axiom,
    ( 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)) )).

cnf(axiom_57,axiom,
    ( ~ 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)) )).

cnf(axiom_58,axiom,
    ( f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(f_ADD_(T_13,n1)),I1_73),I2_74) = f__index_(f__index_(fwork_DOTfifo_DOTrtl_DOTmem_(T_13),I1_73),I2_74)
    | ~ p_LES_EQU_(n0,I2_74)
    | ~ p_LES_EQU_(I2_74,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__width_,n1))
    | ~ p_LES_EQU_(n0,I1_73)
    | ~ p_LES_EQU_(I1_73,f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
    | p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(T_13))
    | p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(T_13)) )).

cnf(axiom_59,axiom,
    (  f_ADD_(X_80,n1) != n0 )).

cnf(axiom_60,axiom,
    ( ~ p_LES_EQU_(f_ADD_(X_81,n1),n0) )).

cnf(axiom_61,axiom,
    ( ~ p_LES_EQU_(X_82,f_SUB_(X_82,n1))
    | p_LES_EQU_(X_82,n0) )).

cnf(axiom_62,axiom,
    ( def_89(Y_84,X_83)
    | f_ADD_(Z_85,Y_84) = X_83
    | f_SUB_(X_83,Y_84) != Z_85 )).

cnf(axiom_63,axiom,
    ( def_89(Y_84,X_83)
    | f_ADD_(Z_85,Y_84) != X_83
    | f_SUB_(X_83,Y_84) = Z_85 )).

cnf(axiom_64,axiom,
    ( X_83 != Y_84
    | ~ def_89(Y_84,X_83) )).

cnf(axiom_65,axiom,
    ( p_LES_EQU_(X_83,Y_84)
    | ~ def_89(Y_84,X_83) )).

cnf(axiom_66,axiom,
    ( ~ p_LES_EQU_(f_ADD_(Y_91,n1),f_ADD_(X_90,n1))
    | p_LES_EQU_(Y_91,X_90) )).

cnf(axiom_67,axiom,
    ( p_LES_EQU_(f_ADD_(Y_91,n1),f_ADD_(X_90,n1))
    | ~ p_LES_EQU_(Y_91,X_90) )).

cnf(axiom_68,axiom,
    ( Y_93 = X_92
    | ~ p_LES_EQU_(X_92,Y_93)
    | p_LES_EQU_(f_ADD_(X_92,n1),Y_93) )).

cnf(axiom_69,axiom,
    ( ~ p_LES_EQU_(X_94,Y_95)
    | X_94 = Y_95
    | p_LES_EQU_(f_ADD_(X_94,n1),Y_95) )).

cnf(axiom_70,axiom,
    ( X_96 = Y_97
    | ~ p_LES_EQU_(X_96,Y_97)
    | ~ p_LES_EQU_(Y_97,X_96) )).

cnf(axiom_71,axiom,
    ( ~ p_LES_EQU_(Z_100,X_98)
    | p_LES_EQU_(Y_99,X_98)
    | p_LES_EQU_(Z_100,Y_99) )).

cnf(axiom_72,axiom,
    ( f_ADD_(X_101,n1) = Y_102
    | ~ p_LES_EQU_(Y_102,f_ADD_(X_101,n1))
    | p_LES_EQU_(Y_102,X_101) )).

cnf(axiom_73,axiom,
    ( ~ p_LES_EQU_(X_103,n0)
    | X_103 = n0 )).

cnf(axiom_74,axiom,
    ( X_104 = f_ADD_(y_105(X_104),n1)
    | X_104 = n0 )).

cnf(axiom_75,axiom,
    ( p_LES_EQU_(X_106,X_106) )).

cnf(axiom_76,axiom,
    ( X_107 = Y_108
    | f_ADD_(X_107,n1) != f_ADD_(Y_108,n1) )).

cnf(axiom_77,axiom,
    ( f_ADD_(n0,X_109) = X_109 )).

cnf(axiom_78,axiom,
    ( n1 = f_ADD_(n0,n1) )).

cnf(axiom_79,axiom,
    ( f__length_(f__cons_(X_110,Xs_111)) = f_ADD_(f__length_(Xs_111),n1) )).

cnf(axiom_80,axiom,
    ( f__length_(f__empty_) = n0 )).

cnf(axiom_81,axiom,
    ( f__length_(f__concat_(A_112,B_113)) = f_ADD_(f__length_(A_112),f__length_(B_113)) )).

cnf(axiom_82,axiom,
    ( f__length_(f__slice_(A_114,I1_115,I2_116)) = f_SUB_(I2_116,f_ADD_(I1_115,n1)) )).

cnf(axiom_83,axiom,
    ( f__index_(f__others_(E_117),I_118) = E_117 )).

cnf(axiom_84,axiom,
    ( I_119 != n0
    | f__index_(f__cons_(X_120,Xs_121),I_119) = X_120 )).

cnf(axiom_85,axiom,
    ( p_LES_EQU_(I_122,n0)
    | f__index_(f__cons_(X_123,Xs_124),I_122) = f__index_(Xs_124,f_SUB_(I_122,n1)) )).

cnf(axiom_86,axiom,
    ( p_LES_EQU_(length(A_126),I_125)
    | f__index_(f__concat_(A_126,B_127),I_125) = f__index_(A_126,I_125) )).

cnf(axiom_87,axiom,
    ( ~ p_LES_EQU_(length(A_129),I_128)
    | f__index_(f__concat_(A_129,B_130),I_128) = f__index_(B_130,f_SUB_(I_128,length(A_129))) )).

cnf(axiom_88,axiom,
    ( f__index_(f__slice_(A_131,I1_132,I2_133),I_134) = f__index_(A_131,f_ADD_(I_134,I1_132)) )).

cnf(axiom_89,axiom,
    ( f__index_(f__and_(A_135,B_136),X_137) = f__and_(f__index_(A_135,X_137),f__index_(B_136,X_137)) )).

cnf(axiom_90,axiom,
    ( f__index_(f__or_(A_138,B_139),X_140) = f__or_(f__index_(A_138,X_140),f__index_(B_139,X_140)) )).

cnf(axiom_91,axiom,
    ( f__index_(f__xor_(A_141,B_142),X_143) = f__xor_(f__index_(A_141,X_143),f__index_(B_142,X_143)) )).

cnf(axiom_92,axiom,
    ( f__index_(f__nand_(A_144,B_145),X_146) = f__nand_(f__index_(A_144,X_146),f__index_(B_145,X_146)) )).

cnf(axiom_93,axiom,
    ( f__index_(f__nor_(A_147,B_148),X_149) = f__nor_(f__index_(A_147,X_149),f__index_(B_148,X_149)) )).

cnf(axiom_94,axiom,
    ( f__index_(f__xnor_(A_150,B_151),X_152) = f__xnor_(f__index_(A_150,X_152),f__index_(B_151,X_152)) )).

cnf(axiom_95,axiom,
    ( f__index_(f__not_(A_153),X_154) = f__not_(f__index_(A_153,X_154)) )).

cnf(axiom_96,axiom,
    ( p__pred_(f__true_) )).

cnf(axiom_97,axiom,
    ( ~ p__pred_(f__false_) )).

cnf(axiom_98,axiom,
    (  f__false_ != f__true_ )).

cnf(axiom_99,axiom,
    ( p__pred_(B_156)
    | ~ p__pred_(A_155)
    | ~ p__pred_(f__equiv_(A_155,B_156)) )).

cnf(axiom_100,axiom,
    ( ~ p__pred_(B_156)
    | p__pred_(A_155)
    | ~ p__pred_(f__equiv_(A_155,B_156)) )).

cnf(axiom_101,axiom,
    ( ~ p__pred_(B_156)
    | ~ p__pred_(A_155)
    | p__pred_(f__equiv_(A_155,B_156)) )).

cnf(axiom_102,axiom,
    ( p__pred_(B_156)
    | p__pred_(A_155)
    | p__pred_(f__equiv_(A_155,B_156)) )).

cnf(axiom_103,axiom,
    ( A_163 = B_164
    | ~ p__pred_(f__equal_(A_163,B_164)) )).

cnf(axiom_104,axiom,
    ( A_163 != B_164
    | p__pred_(f__equal_(A_163,B_164)) )).

cnf(axiom_105,axiom,
    ( p__pred_(B_166)
    | ~ p__pred_(f__and_(A_165,B_166)) )).

cnf(axiom_106,axiom,
    ( p__pred_(A_165)
    | ~ p__pred_(f__and_(A_165,B_166)) )).

cnf(axiom_107,axiom,
    ( ~ p__pred_(A_165)
    | ~ p__pred_(B_166)
    | p__pred_(f__and_(A_165,B_166)) )).

cnf(axiom_108,axiom,
    ( p__pred_(A_169)
    | p__pred_(B_170)
    | ~ p__pred_(f__or_(A_169,B_170)) )).

cnf(axiom_109,axiom,
    ( ~ p__pred_(B_170)
    | p__pred_(f__or_(A_169,B_170)) )).

cnf(axiom_110,axiom,
    ( ~ p__pred_(A_169)
    | p__pred_(f__or_(A_169,B_170)) )).

cnf(axiom_111,axiom,
    ( ~ p__pred_(B_174)
    | ~ p__pred_(A_173)
    | ~ p__pred_(f__xor_(A_173,B_174)) )).

cnf(axiom_112,axiom,
    ( p__pred_(B_174)
    | p__pred_(A_173)
    | ~ p__pred_(f__xor_(A_173,B_174)) )).

cnf(axiom_113,axiom,
    ( p__pred_(B_174)
    | ~ p__pred_(A_173)
    | p__pred_(f__xor_(A_173,B_174)) )).

cnf(axiom_114,axiom,
    ( ~ p__pred_(B_174)
    | p__pred_(A_173)
    | p__pred_(f__xor_(A_173,B_174)) )).

cnf(axiom_115,axiom,
    ( ~ p__pred_(A_181)
    | ~ p__pred_(B_182)
    | ~ p__pred_(f__nand_(A_181,B_182)) )).

cnf(axiom_116,axiom,
    ( p__pred_(B_182)
    | p__pred_(f__nand_(A_181,B_182)) )).

cnf(axiom_117,axiom,
    ( p__pred_(A_181)
    | p__pred_(f__nand_(A_181,B_182)) )).

cnf(axiom_118,axiom,
    ( ~ p__pred_(B_186)
    | ~ p__pred_(f__nor_(A_185,B_186)) )).

cnf(axiom_119,axiom,
    ( ~ p__pred_(A_185)
    | ~ p__pred_(f__nor_(A_185,B_186)) )).

cnf(axiom_120,axiom,
    ( p__pred_(A_185)
    | p__pred_(B_186)
    | p__pred_(f__nor_(A_185,B_186)) )).

cnf(axiom_121,axiom,
    ( p__pred_(B_190)
    | ~ p__pred_(A_189)
    | ~ p__pred_(f__xnor_(A_189,B_190)) )).

cnf(axiom_122,axiom,
    ( ~ p__pred_(B_190)
    | p__pred_(A_189)
    | ~ p__pred_(f__xnor_(A_189,B_190)) )).

cnf(axiom_123,axiom,
    ( ~ p__pred_(B_190)
    | ~ p__pred_(A_189)
    | p__pred_(f__xnor_(A_189,B_190)) )).

cnf(axiom_124,axiom,
    ( p__pred_(B_190)
    | p__pred_(A_189)
    | p__pred_(f__xnor_(A_189,B_190)) )).

cnf(axiom_125,axiom,
    ( ~ p__pred_(A_197)
    | ~ p__pred_(f__not_(A_197)) )).

cnf(axiom_126,axiom,
    ( p__pred_(A_197)
    | p__pred_(f__not_(A_197)) )).

cnf(axiom_127,axiom,
    ( ~ p_LES_EQU_(B_199,A_198)
    | ~ p__pred_(f__lt_(A_198,B_199)) )).

cnf(axiom_128,axiom,
    ( p_LES_EQU_(B_199,A_198)
    | p__pred_(f__lt_(A_198,B_199)) )).

cnf(axiom_129,axiom,
    ( p_LES_EQU_(A_200,B_201)
    | ~ p__pred_(f__leq_(A_200,B_201)) )).

cnf(axiom_130,axiom,
    ( ~ p_LES_EQU_(A_200,B_201)
    | p__pred_(f__leq_(A_200,B_201)) )).

cnf(axiom_131,axiom,
    ( ~ p_LES_EQU_(A_202,B_203)
    | ~ p__pred_(f__gt_(A_202,B_203)) )).

cnf(axiom_132,axiom,
    ( p_LES_EQU_(A_202,B_203)
    | p__pred_(f__gt_(A_202,B_203)) )).

cnf(axiom_133,axiom,
    ( p_LES_EQU_(B_205,A_204)
    | ~ p__pred_(f__geq_(A_204,B_205)) )).

cnf(axiom_134,axiom,
    ( ~ p_LES_EQU_(B_205,A_204)
    | p__pred_(f__geq_(A_204,B_205)) )).

%--------------------------------------------------------------------------