%--------------------------------------------------------------------------
% File     : HWV003-0 : TPTP v7.2.0. Released v2.5.0.
% Domain   : Hardware Verification
% Axioms   : Axioms from a VHDL design description
% Version  : [Mar02] axioms.
% English  :

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

% Status   : Satisfiable
% Syntax   : Number of clauses    :   90 (  64 non-Horn;   6 unit;  81 RR)
%            Number of atoms      :  369 (  50 equality)
%            Maximal clause size  :    7 (   4 average)
%            Number of predicates :   13 (   0 propositional; 1-3 arity)
%            Number of functors   :   10 (   3 constant; 0-2 arity)
%            Number of variables  :  139 (   5 singleton)
%            Maximal term depth   :    3 (   1 average)
% SPC      : 

% Comments : Generated by Safelogic's Haskell Library
%--------------------------------------------------------------------------
cnf(axiom_1,axiom,
    (  plus(X_0,n1) != n0 )).

cnf(axiom_2,axiom,
    ( gt(plus(X_1,n1),n0) )).

cnf(axiom_3,axiom,
    ( ~ gt(X_2,n0)
    | gt(X_2,minus(X_2,n1)) )).

cnf(axiom_4,axiom,
    ( minus(X_3,Y_4) != Z_5
    | plus(Z_5,Y_4) = X_3
    | def_10(Y_4,X_3) )).

cnf(axiom_5,axiom,
    ( minus(X_3,Y_4) = Z_5
    | plus(Z_5,Y_4) != X_3
    | def_10(Y_4,X_3) )).

cnf(axiom_6,axiom,
    ( ~ def_10(Y_4,X_3)
    | ~ gt(X_3,Y_4) )).

cnf(axiom_7,axiom,
    ( ~ def_10(Y_4,X_3)
    | X_3 != Y_4 )).

cnf(axiom_8,axiom,
    ( ~ gt(Y_12,X_11)
    | gt(plus(Y_12,n1),plus(X_11,n1)) )).

cnf(axiom_9,axiom,
    ( gt(Y_12,X_11)
    | ~ gt(plus(Y_12,n1),plus(X_11,n1)) )).

cnf(axiom_10,axiom,
    ( gt(X_13,Y_14)
    | ~ gt(plus(X_13,n1),Y_14)
    | Y_14 = X_13 )).

cnf(axiom_11,axiom,
    ( ~ gt(plus(X_15,n1),Y_16)
    | gt(X_15,Y_16)
    | X_15 = Y_16 )).

cnf(axiom_12,axiom,
    ( gt(Y_18,X_17)
    | X_17 = Y_18
    | gt(X_17,Y_18) )).

cnf(axiom_13,axiom,
    ( ~ gt(Z_21,Y_20)
    | gt(Z_21,X_19)
    | ~ gt(Y_20,X_19) )).

cnf(axiom_14,axiom,
    ( ~ gt(Y_24,X_23)
    | plus(X_23,n1) = Y_24
    | gt(Y_24,plus(X_23,n1)) )).

cnf(axiom_15,axiom,
    ( X_25 = n0
    | gt(X_25,n0) )).

cnf(axiom_16,axiom,
    ( X_26 = n0
    | X_26 = plus(y_27(X_26),n1) )).

cnf(axiom_17,axiom,
    ( ~ gt(X_28,X_28) )).

cnf(axiom_18,axiom,
    ( plus(X_29,n1) != plus(Y_30,n1)
    | X_29 = Y_30 )).

cnf(axiom_19,axiom,
    ( plus(n0,X_31) = X_31 )).

cnf(axiom_20,axiom,
    ( n1 = plus(n0,n1) )).

cnf(axiom_21,axiom,
    ( level(X_t_32) = int_level(X_t_32) )).

cnf(axiom_22,axiom,
    ( int_level(X_t_33) != fifo_length
    | p_Full(X_t_33) )).

cnf(axiom_23,axiom,
    ( int_level(X_t_34) = fifo_length
    | ~ p_Full(X_t_34) )).

cnf(axiom_24,axiom,
    ( int_level(X_t_35) != n0
    | p_Empty(X_t_35) )).

cnf(axiom_25,axiom,
    ( int_level(X_t_36) = n0
    | ~ p_Empty(X_t_36) )).

cnf(axiom_26,axiom,
    ( ~ p_Reset(X_t_37)
    | int_level(plus(X_t_37,n1)) = n0 )).

cnf(axiom_27,axiom,
    ( ~ p_Reset(X_t_37)
    | wr_level(plus(X_t_37,n1)) = n0 )).

cnf(axiom_28,axiom,
    ( ~ p_Reset(X_t_37)
    | rd_level(plus(X_t_37,n1)) = n0 )).

cnf(axiom_29,axiom,
    ( ~ p_Reset(X_t_37)
    | ~ p_Wr_error(plus(X_t_37,n1)) )).

cnf(axiom_30,axiom,
    ( ~ p_Reset(X_t_37)
    | ~ p_Rd_error(plus(X_t_37,n1)) )).

cnf(axiom_31,axiom,
    ( ~ p_Reset(X_t_37)
    | ~ p_Mem(X_k1_38,X_k2_39,plus(X_t_37,n1)) )).

cnf(axiom_32,axiom,
    ( ~ p_Reset(X_t_37)
    | ~ p_Data_out(X_k1_40,plus(X_t_37,n1)) )).

cnf(axiom_33,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | rd_level(plus(X_t_42,n1)) = rd_level(X_t_42) )).

cnf(axiom_34,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ gt(fifo_length,int_level(X_t_42))
    | ~ p_Wr_error(plus(X_t_42,n1)) )).

cnf(axiom_35,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ gt(fifo_length,int_level(X_t_42))
    | int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1) )).

cnf(axiom_36,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ gt(fifo_length,int_level(X_t_42))
    | ~ p_Mem(wr_level(X_t_42),X_k1_43,plus(X_t_42,n1))
    | p_Data_in(X_k1_43,X_t_42) )).

cnf(axiom_37,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ gt(fifo_length,int_level(X_t_42))
    | p_Mem(wr_level(X_t_42),X_k1_43,plus(X_t_42,n1))
    | ~ p_Data_in(X_k1_43,X_t_42) )).

cnf(axiom_38,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ gt(fifo_length,int_level(X_t_42))
    | X_c1_47 = wr_level(X_t_42)
    | ~ p_Mem(X_c1_47,X_k1_48,plus(X_t_42,n1))
    | p_Mem(X_c1_47,X_k1_48,X_t_42) )).

cnf(axiom_39,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ gt(fifo_length,int_level(X_t_42))
    | X_c1_47 = wr_level(X_t_42)
    | p_Mem(X_c1_47,X_k1_48,plus(X_t_42,n1))
    | ~ p_Mem(X_c1_47,X_k1_48,X_t_42) )).

cnf(axiom_40,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ gt(fifo_length,int_level(X_t_42))
    | ~ gt(minus(fifo_length,n1),wr_level(X_t_42))
    | wr_level(plus(X_t_42,n1)) = plus(wr_level(X_t_42),n1) )).

cnf(axiom_41,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ gt(fifo_length,int_level(X_t_42))
    | gt(minus(fifo_length,n1),wr_level(X_t_42))
    | wr_level(plus(X_t_42,n1)) = n0 )).

cnf(axiom_42,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | gt(fifo_length,int_level(X_t_42))
    | p_Wr_error(plus(X_t_42,n1)) )).

cnf(axiom_43,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | gt(fifo_length,int_level(X_t_42))
    | wr_level(plus(X_t_42,n1)) = wr_level(X_t_42) )).

cnf(axiom_44,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | gt(fifo_length,int_level(X_t_42))
    | int_level(plus(X_t_42,n1)) = int_level(X_t_42) )).

cnf(axiom_45,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | gt(fifo_length,int_level(X_t_42))
    | ~ p_Mem(X_k1_57,X_k2_58,plus(X_t_42,n1))
    | p_Mem(X_k1_57,X_k2_58,X_t_42) )).

cnf(axiom_46,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | gt(fifo_length,int_level(X_t_42))
    | p_Mem(X_k1_57,X_k2_58,plus(X_t_42,n1))
    | ~ p_Mem(X_k1_57,X_k2_58,X_t_42) )).

cnf(axiom_47,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ p_Data_out(X_k1_64,plus(X_t_42,n1))
    | p_Data_out(X_k1_64,X_t_42) )).

cnf(axiom_48,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | p_Data_out(X_k1_64,plus(X_t_42,n1))
    | ~ p_Data_out(X_k1_64,X_t_42) )).

cnf(axiom_49,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ p_Rd_error(plus(X_t_42,n1))
    | p_Rd_error(X_t_42) )).

cnf(axiom_50,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | p_Rd_error(plus(X_t_42,n1))
    | ~ p_Rd_error(X_t_42) )).

cnf(axiom_51,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ p_Wr_error(plus(X_t_42,n1)) )).

cnf(axiom_52,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | ~ p_Rd_error(plus(X_t_42,n1)) )).

cnf(axiom_53,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | int_level(plus(X_t_42,n1)) = int_level(X_t_42) )).

cnf(axiom_54,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | ~ p_Data_out(X_k1_73,plus(X_t_42,n1))
    | p_Mem(rd_level(X_t_42),X_k1_73,X_t_42) )).

cnf(axiom_55,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | p_Data_out(X_k1_73,plus(X_t_42,n1))
    | ~ p_Mem(rd_level(X_t_42),X_k1_73,X_t_42) )).

cnf(axiom_56,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | ~ gt(minus(fifo_length,n1),rd_level(X_t_42))
    | rd_level(plus(X_t_42,n1)) = plus(rd_level(X_t_42),n1) )).

cnf(axiom_57,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | gt(minus(fifo_length,n1),rd_level(X_t_42))
    | rd_level(plus(X_t_42,n1)) = n0 )).

cnf(axiom_58,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(int_level(X_t_42),n0)
    | p_Rd_error(plus(X_t_42,n1)) )).

cnf(axiom_59,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(int_level(X_t_42),n0)
    | int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1) )).

cnf(axiom_60,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(int_level(X_t_42),n0)
    | rd_level(plus(X_t_42,n1)) = rd_level(X_t_42) )).

cnf(axiom_61,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(int_level(X_t_42),n0)
    | ~ p_Data_out(X_k1_81,plus(X_t_42,n1))
    | p_Data_out(X_k1_81,X_t_42) )).

cnf(axiom_62,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(int_level(X_t_42),n0)
    | p_Data_out(X_k1_81,plus(X_t_42,n1))
    | ~ p_Data_out(X_k1_81,X_t_42) )).

cnf(axiom_63,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ p_Mem(wr_level(X_t_42),X_k1_87,plus(X_t_42,n1))
    | p_Data_in(X_k1_87,X_t_42) )).

cnf(axiom_64,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | p_Mem(wr_level(X_t_42),X_k1_87,plus(X_t_42,n1))
    | ~ p_Data_in(X_k1_87,X_t_42) )).

cnf(axiom_65,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | X_c1_91 = wr_level(X_t_42)
    | ~ p_Mem(X_c1_91,X_k1_92,plus(X_t_42,n1))
    | p_Mem(X_c1_91,X_k1_92,X_t_42) )).

cnf(axiom_66,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | X_c1_91 = wr_level(X_t_42)
    | p_Mem(X_c1_91,X_k1_92,plus(X_t_42,n1))
    | ~ p_Mem(X_c1_91,X_k1_92,X_t_42) )).

cnf(axiom_67,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(minus(fifo_length,n1),wr_level(X_t_42))
    | wr_level(plus(X_t_42,n1)) = plus(wr_level(X_t_42),n1) )).

cnf(axiom_68,axiom,
    ( p_Reset(X_t_42)
    | ~ p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(minus(fifo_length,n1),wr_level(X_t_42))
    | wr_level(plus(X_t_42,n1)) = n0 )).

cnf(axiom_69,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | wr_level(plus(X_t_42,n1)) = wr_level(X_t_42) )).

cnf(axiom_70,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | ~ p_Rd_error(plus(X_t_42,n1)) )).

cnf(axiom_71,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | int_level(plus(X_t_42,n1)) = minus(int_level(X_t_42),n1) )).

cnf(axiom_72,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | ~ p_Data_out(X_k1_103,plus(X_t_42,n1))
    | p_Mem(rd_level(X_t_42),X_k1_103,X_t_42) )).

cnf(axiom_73,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | p_Data_out(X_k1_103,plus(X_t_42,n1))
    | ~ p_Mem(rd_level(X_t_42),X_k1_103,X_t_42) )).

cnf(axiom_74,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | ~ gt(minus(fifo_length,n1),rd_level(X_t_42))
    | rd_level(plus(X_t_42,n1)) = plus(rd_level(X_t_42),n1) )).

cnf(axiom_75,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | ~ gt(int_level(X_t_42),n0)
    | gt(minus(fifo_length,n1),rd_level(X_t_42))
    | rd_level(plus(X_t_42,n1)) = n0 )).

cnf(axiom_76,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(int_level(X_t_42),n0)
    | p_Rd_error(plus(X_t_42,n1)) )).

cnf(axiom_77,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(int_level(X_t_42),n0)
    | rd_level(plus(X_t_42,n1)) = rd_level(X_t_42) )).

cnf(axiom_78,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(int_level(X_t_42),n0)
    | int_level(plus(X_t_42,n1)) = int_level(X_t_42) )).

cnf(axiom_79,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(int_level(X_t_42),n0)
    | ~ p_Data_out(X_k1_111,plus(X_t_42,n1))
    | p_Data_out(X_k1_111,X_t_42) )).

cnf(axiom_80,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Rd(X_t_42)
    | gt(int_level(X_t_42),n0)
    | p_Data_out(X_k1_111,plus(X_t_42,n1))
    | ~ p_Data_out(X_k1_111,X_t_42) )).

cnf(axiom_81,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | rd_level(plus(X_t_42,n1)) = rd_level(X_t_42) )).

cnf(axiom_82,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | int_level(plus(X_t_42,n1)) = int_level(X_t_42) )).

cnf(axiom_83,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ p_Data_out(X_k1_119,plus(X_t_42,n1))
    | p_Data_out(X_k1_119,X_t_42) )).

cnf(axiom_84,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | p_Data_out(X_k1_119,plus(X_t_42,n1))
    | ~ p_Data_out(X_k1_119,X_t_42) )).

cnf(axiom_85,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | ~ p_Rd_error(plus(X_t_42,n1))
    | p_Rd_error(X_t_42) )).

cnf(axiom_86,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | p_Rd(X_t_42)
    | p_Rd_error(plus(X_t_42,n1))
    | ~ p_Rd_error(X_t_42) )).

cnf(axiom_87,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Mem(X_k1_128,X_k2_129,plus(X_t_42,n1))
    | p_Mem(X_k1_128,X_k2_129,X_t_42) )).

cnf(axiom_88,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | p_Mem(X_k1_128,X_k2_129,plus(X_t_42,n1))
    | ~ p_Mem(X_k1_128,X_k2_129,X_t_42) )).

cnf(axiom_89,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | ~ p_Wr_error(plus(X_t_42,n1))
    | p_Wr_error(X_t_42) )).

cnf(axiom_90,axiom,
    ( p_Reset(X_t_42)
    | p_Wr(X_t_42)
    | p_Wr_error(plus(X_t_42,n1))
    | ~ p_Wr_error(X_t_42) )).

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