Bliksem---1.12.UNS-Ref.s

%------------------------------------------------------------------------------
% File     : Bliksem---1.12
% Problem  : HWV021-2 : TPTP v8.1.0. Released v2.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : bliksem %s

% Computer : n026.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 0s
% DateTime : Sat Jul 16 13:11:49 EDT 2022

% Result   : Unsatisfiable 0.96s 1.32s
% Output   : Refutation 0.96s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12  % Problem  : HWV021-2 : TPTP v8.1.0. Released v2.5.0.
% 0.10/0.13  % Command  : bliksem %s
% 0.13/0.34  % Computer : n026.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % DateTime : Fri Jun 17 09:01:53 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.42/1.12  *** allocated 10000 integers for termspace/termends
% 0.42/1.12  *** allocated 10000 integers for clauses
% 0.42/1.12  *** allocated 10000 integers for justifications
% 0.42/1.12  Bliksem 1.12
% 0.42/1.12  
% 0.42/1.12  
% 0.42/1.12  Automatic Strategy Selection
% 0.42/1.12  
% 0.42/1.12  Clauses:
% 0.42/1.12  [
% 0.42/1.12     [ =( 'f__length_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( X ) ), 'f_ADD_'( 
% 0.42/1.12    'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), n1 ) ) ],
% 0.42/1.12     [ =( 'f__length_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( X ) ), 'f_ADD_'( 
% 0.42/1.12    'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ), n1 ) ) ],
% 0.42/1.12     [ =( 'f__length_'( 'fwork_DOTfifo_DOTrtl_DOTdata__in_'( X ) ), 'f_ADD_'( 
% 0.42/1.12    'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ), n1 ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ],
% 0.42/1.12     [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTfull_'( X ) ), ~( =( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTfull_'( X ) ) ), =( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ],
% 0.42/1.12     [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ), ~( =( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ) ), =( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1 ) ), n0 ), 
% 0.42/1.12    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( 'f_ADD_'( X, n1 ) ), n0 ), 
% 0.42/1.12    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1 ) ), n0 ), 
% 0.42/1.12    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 'f_ADD_'( X, n1 )
% 0.42/1.12     ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 )
% 0.42/1.12     ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'f__index_'( 'f__index_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( X, n1 ) ), Y ), Z ) ) ), ~( 
% 0.42/1.12    'p_LES_EQU_'( n0, Z ) ), ~( 'p_LES_EQU_'( Z, 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), ~( 'p_LES_EQU_'( n0, Y
% 0.42/1.12     ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ) ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 
% 0.42/1.12    'f_ADD_'( X, n1 ) ), Y ) ) ), ~( 'p_LES_EQU_'( n0, Y ) ), ~( 'p_LES_EQU_'( 
% 0.42/1.12    Y, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), ~( 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'f_ADD_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n1 ) ), 
% 0.42/1.12    'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fstd_DOTstandard_DOTmod_'( 'f_ADD_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ), n1 ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ), 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( 
% 0.42/1.12    X, n1 ) ), 'f_SUB_'( 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    n1 ), 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ) ), Y ), 'f__index_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTdata__in_'( X ), Y ) ), ~( 'p_LES_EQU_'( n0, Y )
% 0.42/1.12     ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_'
% 0.42/1.12    , n1 ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( 
% 0.42/1.12    X, n1 ) ), Y ), Z ), 'f__index_'( 'f__index_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTmem_'( X ), Y ), Z ) ), ~( 'p_LES_EQU_'( n0, Z )
% 0.42/1.12     ), ~( 'p_LES_EQU_'( Z, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_'
% 0.42/1.12    , n1 ) ) ), =( Y, 'f_SUB_'( 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ) ), ~( 'p_LES_EQU_'( n0, Y ) )
% 0.42/1.12    , ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    n1 ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 'f_ADD_'( X, n1 )
% 0.42/1.12     ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), ~( 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ), ~( 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 'f_ADD_'( X, n1 ) )
% 0.42/1.12     ), ~( 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( 
% 0.42/1.12    X, n1 ) ), Y ), Z ), 'f__index_'( 'f__index_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTmem_'( X ), Y ), Z ) ), ~( 'p_LES_EQU_'( n0, Z )
% 0.42/1.12     ), ~( 'p_LES_EQU_'( Z, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_'
% 0.42/1.12    , n1 ) ) ), ~( 'p_LES_EQU_'( n0, Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ) ) ), ~( 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 ) ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( X ) ) ), 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 ) ) ), 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 'f_ADD_'( X, n1
% 0.42/1.12     ) ), Y ), 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( X ), Y ) )
% 0.42/1.12    , ~( 'p_LES_EQU_'( n0, Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fstd_DOTstandard_DOTmod_'( 'f_ADD_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ), n1 ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fstd_DOTstandard_DOTmod_'( 'f_ADD_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ), n1 ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ), 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 'f_ADD_'( X, n1
% 0.42/1.12     ) ), Y ), 'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( X )
% 0.42/1.12    , 'f_SUB_'( 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ) ), Y ) ), ~( 'p_LES_EQU_'( n0
% 0.42/1.12    , Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 )
% 0.42/1.12     ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), 
% 0.42/1.12    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ), ~( 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'f_ADD_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n1 ) ), ~( 
% 0.42/1.12    'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 ) )
% 0.42/1.12     ), ~( 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), 
% 0.42/1.12    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 'f_ADD_'( X, n1
% 0.42/1.12     ) ), Y ), 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( X ), Y ) )
% 0.42/1.12    , ~( 'p_LES_EQU_'( n0, Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), ~( 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( 
% 0.42/1.12    X, n1 ) ), 'f_SUB_'( 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    n1 ), 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ) ), Y ), 'f__index_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTdata__in_'( X ), Y ) ), ~( 'p_LES_EQU_'( n0, Y )
% 0.42/1.12     ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_'
% 0.42/1.12    , n1 ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( 
% 0.42/1.12    X, n1 ) ), Y ), Z ), 'f__index_'( 'f__index_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTmem_'( X ), Y ), Z ) ), ~( 'p_LES_EQU_'( n0, Z )
% 0.42/1.12     ), ~( 'p_LES_EQU_'( Z, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_'
% 0.42/1.12    , n1 ) ) ), =( Y, 'f_SUB_'( 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ) ), ~( 'p_LES_EQU_'( n0, Y ) )
% 0.42/1.12    , ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.42/1.12    n1 ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 'f_ADD_'( X, n1 )
% 0.42/1.12     ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n1 ) ), 
% 0.42/1.12    'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fstd_DOTstandard_DOTmod_'( 'f_ADD_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ), n1 ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ), 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 'f_ADD_'( X, n1
% 0.42/1.12     ) ), Y ), 'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( X )
% 0.42/1.12    , 'f_SUB_'( 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ) ), Y ) ), ~( 'p_LES_EQU_'( n0
% 0.42/1.12    , Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 )
% 0.42/1.12     ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), 
% 0.42/1.12    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), ~( 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ), ~( 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 ) )
% 0.42/1.12     ), ~( 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), 
% 0.42/1.12    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 'f_ADD_'( X, n1
% 0.42/1.12     ) ), Y ), 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( X ), Y ) )
% 0.42/1.12    , ~( 'p_LES_EQU_'( n0, Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), ~( 'p_LES_EQU_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1 ) ), 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 ) ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( X ) ) ), 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 ) ) ), 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 'f_ADD_'( X, n1
% 0.42/1.12     ) ), Y ), 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( X ), Y ) )
% 0.42/1.12    , ~( 'p_LES_EQU_'( n0, Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( X ) ), ~( 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 'f_ADD_'( X, n1 ) ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( X ) ) ), 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 'f_ADD_'( X, n1 ) ) ), 
% 0.42/1.12    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( 
% 0.42/1.12    X, n1 ) ), Y ), Z ), 'f__index_'( 'f__index_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTmem_'( X ), Y ), Z ) ), ~( 'p_LES_EQU_'( n0, Z )
% 0.42/1.12     ), ~( 'p_LES_EQU_'( Z, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_'
% 0.42/1.12    , n1 ) ) ), ~( 'p_LES_EQU_'( n0, Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ) ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.42/1.12    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ],
% 0.42/1.12     [ ~( =( 'f_ADD_'( X, n1 ), n0 ) ) ],
% 0.42/1.12     [ ~( 'p_LES_EQU_'( 'f_ADD_'( X, n1 ), n0 ) ) ],
% 0.42/1.12     [ ~( 'p_LES_EQU_'( X, 'f_SUB_'( X, n1 ) ) ), 'p_LES_EQU_'( X, n0 ) ]
% 0.42/1.12    ,
% 0.42/1.12     [ 'def_89'( X, Y ), =( 'f_ADD_'( Z, X ), Y ), ~( =( 'f_SUB_'( Y, X ), Z
% 0.42/1.12     ) ) ],
% 0.42/1.12     [ 'def_89'( X, Y ), ~( =( 'f_ADD_'( Z, X ), Y ) ), =( 'f_SUB_'( Y, X ), 
% 0.42/1.12    Z ) ],
% 0.42/1.12     [ ~( =( X, Y ) ), ~( 'def_89'( Y, X ) ) ],
% 0.42/1.12     [ 'p_LES_EQU_'( X, Y ), ~( 'def_89'( Y, X ) ) ],
% 0.42/1.12     [ ~( 'p_LES_EQU_'( 'f_ADD_'( X, n1 ), 'f_ADD_'( Y, n1 ) ) ), 
% 0.42/1.12    'p_LES_EQU_'( X, Y ) ],
% 0.42/1.12     [ 'p_LES_EQU_'( 'f_ADD_'( X, n1 ), 'f_ADD_'( Y, n1 ) ), ~( 'p_LES_EQU_'( 
% 0.42/1.12    X, Y ) ) ],
% 0.42/1.12     [ =( X, Y ), ~( 'p_LES_EQU_'( Y, X ) ), 'p_LES_EQU_'( 'f_ADD_'( Y, n1 )
% 0.42/1.12    , X ) ],
% 0.42/1.12     [ ~( 'p_LES_EQU_'( X, Y ) ), =( X, Y ), 'p_LES_EQU_'( 'f_ADD_'( X, n1 )
% 0.42/1.12    , Y ) ],
% 0.42/1.12     [ =( X, Y ), ~( 'p_LES_EQU_'( X, Y ) ), ~( 'p_LES_EQU_'( Y, X ) ) ],
% 0.42/1.12     [ ~( 'p_LES_EQU_'( X, Y ) ), 'p_LES_EQU_'( Z, Y ), 'p_LES_EQU_'( X, Z )
% 0.42/1.12     ],
% 0.42/1.12     [ =( 'f_ADD_'( X, n1 ), Y ), ~( 'p_LES_EQU_'( Y, 'f_ADD_'( X, n1 ) ) ), 
% 0.42/1.12    'p_LES_EQU_'( Y, X ) ],
% 0.42/1.12     [ ~( 'p_LES_EQU_'( X, n0 ) ), =( X, n0 ) ],
% 0.42/1.12     [ =( X, 'f_ADD_'( 'y_105'( X ), n1 ) ), =( X, n0 ) ],
% 0.42/1.12     [ 'p_LES_EQU_'( X, X ) ],
% 0.42/1.12     [ =( X, Y ), ~( =( 'f_ADD_'( X, n1 ), 'f_ADD_'( Y, n1 ) ) ) ],
% 0.42/1.12     [ =( 'f_ADD_'( n0, X ), X ) ],
% 0.42/1.12     [ =( n1, 'f_ADD_'( n0, n1 ) ) ],
% 0.42/1.12     [ =( 'f__length_'( 'f__cons_'( X, Y ) ), 'f_ADD_'( 'f__length_'( Y ), n1
% 0.42/1.12     ) ) ],
% 0.42/1.12     [ =( 'f__length_'( 'f__empty_' ), n0 ) ],
% 0.42/1.12     [ =( 'f__length_'( 'f__concat_'( X, Y ) ), 'f_ADD_'( 'f__length_'( X ), 
% 0.42/1.12    'f__length_'( Y ) ) ) ],
% 0.42/1.12     [ =( 'f__length_'( 'f__slice_'( X, Y, Z ) ), 'f_SUB_'( Z, 'f_ADD_'( Y, 
% 0.42/1.12    n1 ) ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__others_'( X ), Y ), X ) ],
% 0.42/1.12     [ ~( =( X, n0 ) ), =( 'f__index_'( 'f__cons_'( Y, Z ), X ), Y ) ],
% 0.42/1.12     [ 'p_LES_EQU_'( X, n0 ), =( 'f__index_'( 'f__cons_'( Y, Z ), X ), 
% 0.42/1.12    'f__index_'( Z, 'f_SUB_'( X, n1 ) ) ) ],
% 0.42/1.12     [ 'p_LES_EQU_'( length( X ), Y ), =( 'f__index_'( 'f__concat_'( X, Z ), 
% 0.42/1.12    Y ), 'f__index_'( X, Y ) ) ],
% 0.42/1.12     [ ~( 'p_LES_EQU_'( length( X ), Y ) ), =( 'f__index_'( 'f__concat_'( X, 
% 0.42/1.12    Z ), Y ), 'f__index_'( Z, 'f_SUB_'( Y, length( X ) ) ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__slice_'( X, Y, Z ), T ), 'f__index_'( X, 'f_ADD_'( 
% 0.42/1.12    T, Y ) ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__and_'( X, Y ), Z ), 'f__and_'( 'f__index_'( X, Z )
% 0.42/1.12    , 'f__index_'( Y, Z ) ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__or_'( X, Y ), Z ), 'f__or_'( 'f__index_'( X, Z ), 
% 0.42/1.12    'f__index_'( Y, Z ) ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__xor_'( X, Y ), Z ), 'f__xor_'( 'f__index_'( X, Z )
% 0.42/1.12    , 'f__index_'( Y, Z ) ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__nand_'( X, Y ), Z ), 'f__nand_'( 'f__index_'( X, Z
% 0.42/1.12     ), 'f__index_'( Y, Z ) ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__nor_'( X, Y ), Z ), 'f__nor_'( 'f__index_'( X, Z )
% 0.42/1.12    , 'f__index_'( Y, Z ) ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__xnor_'( X, Y ), Z ), 'f__xnor_'( 'f__index_'( X, Z
% 0.42/1.12     ), 'f__index_'( Y, Z ) ) ) ],
% 0.42/1.12     [ =( 'f__index_'( 'f__not_'( X ), Y ), 'f__not_'( 'f__index_'( X, Y ) )
% 0.42/1.12     ) ],
% 0.42/1.12     [ 'p__pred_'( 'f__true_' ) ],
% 0.42/1.12     [ ~( 'p__pred_'( 'f__false_' ) ) ],
% 0.42/1.12     [ ~( =( 'f__false_', 'f__true_' ) ) ],
% 0.42/1.12     [ 'p__pred_'( X ), ~( 'p__pred_'( Y ) ), ~( 'p__pred_'( 'f__equiv_'( Y, 
% 0.42/1.12    X ) ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( X ) ), 'p__pred_'( Y ), ~( 'p__pred_'( 'f__equiv_'( Y, 
% 0.42/1.12    X ) ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( Y ) ), 'p__pred_'( 'f__equiv_'( Y
% 0.42/1.12    , X ) ) ],
% 0.42/1.12     [ 'p__pred_'( X ), 'p__pred_'( Y ), 'p__pred_'( 'f__equiv_'( Y, X ) ) ]
% 0.42/1.12    ,
% 0.42/1.12     [ =( X, Y ), ~( 'p__pred_'( 'f__equal_'( X, Y ) ) ) ],
% 0.42/1.12     [ ~( =( X, Y ) ), 'p__pred_'( 'f__equal_'( X, Y ) ) ],
% 0.42/1.12     [ 'p__pred_'( X ), ~( 'p__pred_'( 'f__and_'( Y, X ) ) ) ],
% 0.42/1.12     [ 'p__pred_'( X ), ~( 'p__pred_'( 'f__and_'( X, Y ) ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( Y ) ), 'p__pred_'( 'f__and_'( X, 
% 0.42/1.12    Y ) ) ],
% 0.42/1.12     [ 'p__pred_'( X ), 'p__pred_'( Y ), ~( 'p__pred_'( 'f__or_'( X, Y ) ) )
% 0.42/1.12     ],
% 0.42/1.12     [ ~( 'p__pred_'( X ) ), 'p__pred_'( 'f__or_'( Y, X ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( X ) ), 'p__pred_'( 'f__or_'( X, Y ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( Y ) ), ~( 'p__pred_'( 'f__xor_'( 
% 0.42/1.12    Y, X ) ) ) ],
% 0.42/1.12     [ 'p__pred_'( X ), 'p__pred_'( Y ), ~( 'p__pred_'( 'f__xor_'( Y, X ) ) )
% 0.42/1.12     ],
% 0.42/1.12     [ 'p__pred_'( X ), ~( 'p__pred_'( Y ) ), 'p__pred_'( 'f__xor_'( Y, X ) )
% 0.42/1.12     ],
% 0.42/1.12     [ ~( 'p__pred_'( X ) ), 'p__pred_'( Y ), 'p__pred_'( 'f__xor_'( Y, X ) )
% 0.42/1.12     ],
% 0.42/1.12     [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( Y ) ), ~( 'p__pred_'( 'f__nand_'( 
% 0.42/1.12    X, Y ) ) ) ],
% 0.42/1.12     [ 'p__pred_'( X ), 'p__pred_'( 'f__nand_'( Y, X ) ) ],
% 0.42/1.12     [ 'p__pred_'( X ), 'p__pred_'( 'f__nand_'( X, Y ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( 'f__nor_'( Y, X ) ) ) ],
% 0.42/1.12     [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( 'f__nor_'( X, Y ) ) ) ],
% 0.96/1.32     [ 'p__pred_'( X ), 'p__pred_'( Y ), 'p__pred_'( 'f__nor_'( X, Y ) ) ]
% 0.96/1.32    ,
% 0.96/1.32     [ 'p__pred_'( X ), ~( 'p__pred_'( Y ) ), ~( 'p__pred_'( 'f__xnor_'( Y, X
% 0.96/1.32     ) ) ) ],
% 0.96/1.32     [ ~( 'p__pred_'( X ) ), 'p__pred_'( Y ), ~( 'p__pred_'( 'f__xnor_'( Y, X
% 0.96/1.32     ) ) ) ],
% 0.96/1.32     [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( Y ) ), 'p__pred_'( 'f__xnor_'( Y
% 0.96/1.32    , X ) ) ],
% 0.96/1.32     [ 'p__pred_'( X ), 'p__pred_'( Y ), 'p__pred_'( 'f__xnor_'( Y, X ) ) ]
% 0.96/1.32    ,
% 0.96/1.32     [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( 'f__not_'( X ) ) ) ],
% 0.96/1.32     [ 'p__pred_'( X ), 'p__pred_'( 'f__not_'( X ) ) ],
% 0.96/1.32     [ ~( 'p_LES_EQU_'( X, Y ) ), ~( 'p__pred_'( 'f__lt_'( Y, X ) ) ) ],
% 0.96/1.32     [ 'p_LES_EQU_'( X, Y ), 'p__pred_'( 'f__lt_'( Y, X ) ) ],
% 0.96/1.32     [ 'p_LES_EQU_'( X, Y ), ~( 'p__pred_'( 'f__leq_'( X, Y ) ) ) ],
% 0.96/1.32     [ ~( 'p_LES_EQU_'( X, Y ) ), 'p__pred_'( 'f__leq_'( X, Y ) ) ],
% 0.96/1.32     [ ~( 'p_LES_EQU_'( X, Y ) ), ~( 'p__pred_'( 'f__gt_'( X, Y ) ) ) ],
% 0.96/1.32     [ 'p_LES_EQU_'( X, Y ), 'p__pred_'( 'f__gt_'( X, Y ) ) ],
% 0.96/1.32     [ 'p_LES_EQU_'( X, Y ), ~( 'p__pred_'( 'f__geq_'( Y, X ) ) ) ],
% 0.96/1.32     [ ~( 'p_LES_EQU_'( X, Y ) ), 'p__pred_'( 'f__geq_'( Y, X ) ) ],
% 0.96/1.32     [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 't_206', 
% 0.96/1.32    n1 ) ) ) ],
% 0.96/1.32     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( 't_206' ) ) ) ],
% 0.96/1.32     [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) ],
% 0.96/1.32     [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( 't_206' ) ) ) ]
% 0.96/1.32  ] .
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  percentage equality = 0.190931, percentage horn = 0.547445
% 0.96/1.32  This is a problem with some equality
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  Options Used:
% 0.96/1.32  
% 0.96/1.32  useres =            1
% 0.96/1.32  useparamod =        1
% 0.96/1.32  useeqrefl =         1
% 0.96/1.32  useeqfact =         1
% 0.96/1.32  usefactor =         1
% 0.96/1.32  usesimpsplitting =  0
% 0.96/1.32  usesimpdemod =      5
% 0.96/1.32  usesimpres =        3
% 0.96/1.32  
% 0.96/1.32  resimpinuse      =  1000
% 0.96/1.32  resimpclauses =     20000
% 0.96/1.32  substype =          eqrewr
% 0.96/1.32  backwardsubs =      1
% 0.96/1.32  selectoldest =      5
% 0.96/1.32  
% 0.96/1.32  litorderings [0] =  split
% 0.96/1.32  litorderings [1] =  extend the termordering, first sorting on arguments
% 0.96/1.32  
% 0.96/1.32  termordering =      kbo
% 0.96/1.32  
% 0.96/1.32  litapriori =        0
% 0.96/1.32  termapriori =       1
% 0.96/1.32  litaposteriori =    0
% 0.96/1.32  termaposteriori =   0
% 0.96/1.32  demodaposteriori =  0
% 0.96/1.32  ordereqreflfact =   0
% 0.96/1.32  
% 0.96/1.32  litselect =         negord
% 0.96/1.32  
% 0.96/1.32  maxweight =         15
% 0.96/1.32  maxdepth =          30000
% 0.96/1.32  maxlength =         115
% 0.96/1.32  maxnrvars =         195
% 0.96/1.32  excuselevel =       1
% 0.96/1.32  increasemaxweight = 1
% 0.96/1.32  
% 0.96/1.32  maxselected =       10000000
% 0.96/1.32  maxnrclauses =      10000000
% 0.96/1.32  
% 0.96/1.32  showgenerated =    0
% 0.96/1.32  showkept =         0
% 0.96/1.32  showselected =     0
% 0.96/1.32  showdeleted =      0
% 0.96/1.32  showresimp =       1
% 0.96/1.32  showstatus =       2000
% 0.96/1.32  
% 0.96/1.32  prologoutput =     1
% 0.96/1.32  nrgoals =          5000000
% 0.96/1.32  totalproof =       1
% 0.96/1.32  
% 0.96/1.32  Symbols occurring in the translation:
% 0.96/1.32  
% 0.96/1.32  {}  [0, 0]      (w:1, o:2, a:1, s:1, b:0), 
% 0.96/1.32  .  [1, 2]      (w:1, o:164, a:1, s:1, b:0), 
% 0.96/1.32  !  [4, 1]      (w:0, o:139, a:1, s:1, b:0), 
% 0.96/1.32  =  [13, 2]      (w:1, o:0, a:0, s:1, b:0), 
% 0.96/1.32  ==>  [14, 2]      (w:1, o:0, a:0, s:1, b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTmem_'  [40, 1]      (w:1, o:145, a:1, s:1, b:0), 
% 0.96/1.32  'f__length_'  [41, 1]      (w:1, o:146, a:1, s:1, b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTfifo__length_'  [42, 0]      (w:1, o:10, a:1, s:1
% 0.96/1.32    , b:0), 
% 0.96/1.32  n1  [43, 0]      (w:1, o:12, a:1, s:1, b:0), 
% 0.96/1.32  'f_SUB_'  [44, 2]      (w:1, o:189, a:1, s:1, b:0), 
% 0.96/1.32  'f_ADD_'  [45, 2]      (w:1, o:190, a:1, s:1, b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTdata__out_'  [46, 1]      (w:1, o:147, a:1, s:1
% 0.96/1.32    , b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTfifo__width_'  [47, 0]      (w:1, o:13, a:1, s:1
% 0.96/1.32    , b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTdata__in_'  [48, 1]      (w:1, o:148, a:1, s:1, b:
% 0.96/1.32    0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTlevel_'  [50, 1]      (w:1, o:144, a:1, s:1, b:0)
% 0.96/1.32    , 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTint__level_'  [51, 1]      (w:1, o:149, a:1, s:1
% 0.96/1.32    , b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTfull_'  [53, 1]      (w:1, o:151, a:1, s:1, b:0), 
% 0.96/1.32    
% 0.96/1.32  'p__pred_'  [54, 1]      (w:1, o:152, a:1, s:1, b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTempty_'  [57, 1]      (w:1, o:150, a:1, s:1, b:0)
% 0.96/1.32    , 
% 0.96/1.32  n0  [58, 0]      (w:1, o:11, a:1, s:1, b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTrd__level_'  [61, 1]      (w:1, o:153, a:1, s:1
% 0.96/1.32    , b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTreset_'  [62, 1]      (w:1, o:156, a:1, s:1, b:0)
% 0.96/1.32    , 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTwr__level_'  [63, 1]      (w:1, o:157, a:1, s:1
% 0.96/1.32    , b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTwr__error_'  [64, 1]      (w:1, o:158, a:1, s:1
% 0.96/1.32    , b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTrd__error_'  [65, 1]      (w:1, o:154, a:1, s:1
% 0.96/1.32    , b:0), 
% 0.96/1.32  'f__index_'  [67, 2]      (w:1, o:191, a:1, s:1, b:0), 
% 0.96/1.32  'p_LES_EQU_'  [69, 2]      (w:1, o:192, a:1, s:1, b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTrd_'  [72, 1]      (w:1, o:155, a:1, s:1, b:0), 
% 0.96/1.32  'fwork_DOTfifo_DOTrtl_DOTwr_'  [73, 1]      (w:1, o:159, a:1, s:1, b:0), 
% 0.96/1.32  'fstd_DOTstandard_DOTmod_'  [74, 2]      (w:1, o:193, a:1, s:1, b:0), 
% 0.96/1.32  'def_89'  [96, 2]      (w:1, o:194, a:1, s:1, b:0), 
% 0.96/1.32  'y_105'  [113, 1]      (w:1, o:160, a:1, s:1, b:0), 
% 0.96/1.32  'f__cons_'  [120, 2]      (w:1, o:195, a:1, s:1, b:0), 
% 0.96/1.32  'f__empty_'  [121, 0]      (w:1, o:127, a:1, s:1, b:0), 
% 0.96/1.32  'f__concat_'  [124, 2]      (w:1, o:196, a:1, s:1, b:0), 
% 0.96/1.32  'f__slice_'  [128, 3]      (w:1, o:209, a:1, s:1, b:0), 
% 0.96/1.32  'f__others_'  [130, 1]      (w:1, o:162, a:1, s:1, b:0), 
% 0.96/1.32  length  [139, 1]      (w:1, o:163, a:1, s:1, b:0), 
% 0.96/1.32  'f__and_'  [151, 2]      (w:1, o:197, a:1, s:1, b:0), 
% 0.96/1.32  'f__or_'  [155, 2]      (w:1, o:200, a:1, s:1, b:0), 
% 0.96/1.32  'f__xor_'  [159, 2]      (w:1, o:202, a:1, s:1, b:0), 
% 0.96/1.32  'f__nand_'  [163, 2]      (w:1, o:198, a:1, s:1, b:0), 
% 0.96/1.32  'f__nor_'  [167, 2]      (w:1, o:199, a:1, s:1, b:0), 
% 0.96/1.32  'f__xnor_'  [171, 2]      (w:1, o:201, a:1, s:1, b:0), 
% 0.96/1.32  'f__not_'  [174, 1]      (w:1, o:161, a:1, s:1, b:0), 
% 0.96/1.32  'f__true_'  [176, 0]      (w:1, o:136, a:1, s:1, b:0), 
% 0.96/1.32  'f__false_'  [177, 0]      (w:1, o:137, a:1, s:1, b:0), 
% 0.96/1.32  'f__equiv_'  [180, 2]      (w:1, o:203, a:1, s:1, b:0), 
% 0.96/1.32  'f__equal_'  [183, 2]      (w:1, o:204, a:1, s:1, b:0), 
% 0.96/1.32  'f__lt_'  [199, 2]      (w:1, o:205, a:1, s:1, b:0), 
% 0.96/1.32  'f__leq_'  [202, 2]      (w:1, o:206, a:1, s:1, b:0), 
% 0.96/1.32  'f__gt_'  [205, 2]      (w:1, o:207, a:1, s:1, b:0), 
% 0.96/1.32  'f__geq_'  [208, 2]      (w:1, o:208, a:1, s:1, b:0), 
% 0.96/1.32  't_206'  [209, 0]      (w:1, o:138, a:1, s:1, b:0).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  Starting Search:
% 0.96/1.32  
% 0.96/1.32  Resimplifying inuse:
% 0.96/1.32  Done
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  Intermediate Status:
% 0.96/1.32  Generated:    6270
% 0.96/1.32  Kept:         2005
% 0.96/1.32  Inuse:        195
% 0.96/1.32  Deleted:      14
% 0.96/1.32  Deletedinuse: 5
% 0.96/1.32  
% 0.96/1.32  Resimplifying inuse:
% 0.96/1.32  Done
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  Bliksems!, er is een bewijs:
% 0.96/1.32  % SZS status Unsatisfiable
% 0.96/1.32  % SZS output start Refutation
% 0.96/1.32  
% 0.96/1.32  clause( 3, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ) ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 6, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ), ~( =( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 12, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.32    X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ]
% 0.96/1.32     )
% 0.96/1.32  .
% 0.96/1.32  clause( 32, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.32    X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 44, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.32    X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 70, [ ~( 'p_LES_EQU_'( X, n0 ) ), =( X, n0 ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 131, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.32    't_206', n1 ) ) ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 133, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 134, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( 't_206' ) )
% 0.96/1.32     ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 194, [ ~( =( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' ), n0 ) ) ]
% 0.96/1.32     )
% 0.96/1.32  .
% 0.96/1.32  clause( 288, [ ~( 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' )
% 0.96/1.32    , n0 ) ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 1455, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) )
% 0.96/1.32    , ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 1459, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) )
% 0.96/1.32     ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 2216, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) )
% 0.96/1.32    , 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ] )
% 0.96/1.32  .
% 0.96/1.32  clause( 2220, [] )
% 0.96/1.32  .
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  % SZS output end Refutation
% 0.96/1.32  found a proof!
% 0.96/1.32  
% 0.96/1.32  % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 0.96/1.32  
% 0.96/1.32  initialclauses(
% 0.96/1.32  [ clause( 2222, [ =( 'f__length_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( X ) ), 
% 0.96/1.32    'f_ADD_'( 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), n1 ) )
% 0.96/1.32     ] )
% 0.96/1.32  , clause( 2223, [ =( 'f__length_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( X
% 0.96/1.32     ) ), 'f_ADD_'( 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ), 
% 0.96/1.32    n1 ) ) ] )
% 0.96/1.32  , clause( 2224, [ =( 'f__length_'( 'fwork_DOTfifo_DOTrtl_DOTdata__in_'( X )
% 0.96/1.32     ), 'f_ADD_'( 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ), n1
% 0.96/1.32     ) ) ] )
% 0.96/1.32  , clause( 2225, [ =( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ] )
% 0.96/1.32  , clause( 2226, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTfull_'( X ) ), ~( 
% 0.96/1.32    =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ) ] )
% 0.96/1.32  , clause( 2227, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTfull_'( X ) ) ), 
% 0.96/1.32    =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ] )
% 0.96/1.32  , clause( 2228, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ), ~( 
% 0.96/1.32    =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ) ] )
% 0.96/1.32  , clause( 2229, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ) )
% 0.96/1.32    , =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ] )
% 0.96/1.32  , clause( 2230, [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ] )
% 0.96/1.32  , clause( 2231, [ =( 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ] )
% 0.96/1.32  , clause( 2232, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ] )
% 0.96/1.32  , clause( 2233, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( 
% 0.96/1.32    X ) ) ) ] )
% 0.96/1.32  , clause( 2234, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( 
% 0.96/1.32    X ) ) ) ] )
% 0.96/1.32  , clause( 2235, [ ~( 'p__pred_'( 'f__index_'( 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( X, n1 ) ), Y ), Z ) ) ), ~( 
% 0.96/1.32    'p_LES_EQU_'( n0, Z ) ), ~( 'p_LES_EQU_'( Z, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), ~( 'p_LES_EQU_'( n0, Y
% 0.96/1.32     ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ] )
% 0.96/1.32  , clause( 2236, [ ~( 'p__pred_'( 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 'f_ADD_'( X, n1 ) ), Y ) ) ), ~( 
% 0.96/1.32    'p_LES_EQU_'( n0, Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ] )
% 0.96/1.32  , clause( 2237, [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2238, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'f_ADD_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n1 ) ), 
% 0.96/1.32    'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2239, [ =( 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fstd_DOTstandard_DOTmod_'( 'f_ADD_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ), n1 ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2240, [ =( 'f__index_'( 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( X, n1 ) ), 'f_SUB_'( 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ) ), Y ), 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTdata__in_'( X ), Y ) ), ~( 'p_LES_EQU_'( n0, Y )
% 0.96/1.32     ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_'
% 0.96/1.32    , n1 ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2241, [ =( 'f__index_'( 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( X, n1 ) ), Y ), Z ), 
% 0.96/1.32    'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( X ), Y ), Z ) )
% 0.96/1.32    , ~( 'p_LES_EQU_'( n0, Z ) ), ~( 'p_LES_EQU_'( Z, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), =( Y, 'f_SUB_'( 
% 0.96/1.32    'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ) ), ~( 'p_LES_EQU_'( n0, Y ) )
% 0.96/1.32    , ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    n1 ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2242, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2243, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2244, [ =( 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2245, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2246, [ =( 'f__index_'( 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( X, n1 ) ), Y ), Z ), 
% 0.96/1.32    'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( X ), Y ), Z ) )
% 0.96/1.32    , ~( 'p_LES_EQU_'( n0, Z ) ), ~( 'p_LES_EQU_'( Z, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), ~( 'p_LES_EQU_'( n0, Y
% 0.96/1.32     ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ) ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2247, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( X ) ), 
% 0.96/1.32    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 ) )
% 0.96/1.32     ) ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2248, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( X )
% 0.96/1.32     ) ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 )
% 0.96/1.32     ) ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2249, [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ), Y ), 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTdata__out_'( X ), Y ) ), ~( 'p_LES_EQU_'( n0, Y
% 0.96/1.32     ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2250, [ =( 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fstd_DOTstandard_DOTmod_'( 'f_ADD_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ), n1 ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2251, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2252, [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fstd_DOTstandard_DOTmod_'( 'f_ADD_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ), n1 ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2253, [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ), Y ), 'f__index_'( 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTmem_'( X ), 'f_SUB_'( 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ) ), Y ) ), ~( 'p_LES_EQU_'( n0
% 0.96/1.32    , Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2254, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2255, [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2256, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'f_ADD_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n1 ) ), ~( 
% 0.96/1.32    'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2257, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2258, [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ), Y ), 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTdata__out_'( X ), Y ) ), ~( 'p_LES_EQU_'( n0, Y
% 0.96/1.32     ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2259, [ =( 'f__index_'( 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( X, n1 ) ), 'f_SUB_'( 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ) ), Y ), 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTdata__in_'( X ), Y ) ), ~( 'p_LES_EQU_'( n0, Y )
% 0.96/1.32     ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__width_'
% 0.96/1.32    , n1 ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2260, [ =( 'f__index_'( 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( X, n1 ) ), Y ), Z ), 
% 0.96/1.32    'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( X ), Y ), Z ) )
% 0.96/1.32    , ~( 'p_LES_EQU_'( n0, Z ) ), ~( 'p_LES_EQU_'( Z, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), =( Y, 'f_SUB_'( 
% 0.96/1.32    'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ) ), ~( 'p_LES_EQU_'( n0, Y ) )
% 0.96/1.32    , ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTfifo__length_', 
% 0.96/1.32    n1 ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2261, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X
% 0.96/1.32     ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2262, [ =( 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fwork_DOTfifo_DOTrtl_DOTwr__level_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2263, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'f_SUB_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n1 ) ), 
% 0.96/1.32    'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2264, [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fstd_DOTstandard_DOTmod_'( 'f_ADD_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ), n1 ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_' ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2265, [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ), Y ), 'f__index_'( 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTmem_'( X ), 'f_SUB_'( 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ) ), Y ) ), ~( 'p_LES_EQU_'( n0
% 0.96/1.32    , Y ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2266, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2267, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2268, [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2269, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2270, [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ), Y ), 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTdata__out_'( X ), Y ) ), ~( 'p_LES_EQU_'( n0, Y
% 0.96/1.32     ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), ~( 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2271, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2272, [ =( 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( 'f_ADD_'( X, n1
% 0.96/1.32     ) ), 'fwork_DOTfifo_DOTrtl_DOTrd__level_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2273, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( X ) ), 
% 0.96/1.32    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 ) )
% 0.96/1.32     ) ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2274, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( X )
% 0.96/1.32     ) ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 )
% 0.96/1.32     ) ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2275, [ =( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTdata__out_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ), Y ), 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTdata__out_'( X ), Y ) ), ~( 'p_LES_EQU_'( n0, Y
% 0.96/1.32     ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2276, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( X ) ), 
% 0.96/1.32    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 'f_ADD_'( X, n1 ) )
% 0.96/1.32     ) ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2277, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( X )
% 0.96/1.32     ) ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr__error_'( 'f_ADD_'( X, n1 )
% 0.96/1.32     ) ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2278, [ =( 'f__index_'( 'f__index_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTmem_'( 'f_ADD_'( X, n1 ) ), Y ), Z ), 
% 0.96/1.32    'f__index_'( 'f__index_'( 'fwork_DOTfifo_DOTrtl_DOTmem_'( X ), Y ), Z ) )
% 0.96/1.32    , ~( 'p_LES_EQU_'( n0, Z ) ), ~( 'p_LES_EQU_'( Z, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__width_', n1 ) ) ), ~( 'p_LES_EQU_'( n0, Y
% 0.96/1.32     ) ), ~( 'p_LES_EQU_'( Y, 'f_SUB_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTfifo__length_', n1 ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 2279, [ ~( =( 'f_ADD_'( X, n1 ), n0 ) ) ] )
% 0.96/1.32  , clause( 2280, [ ~( 'p_LES_EQU_'( 'f_ADD_'( X, n1 ), n0 ) ) ] )
% 0.96/1.32  , clause( 2281, [ ~( 'p_LES_EQU_'( X, 'f_SUB_'( X, n1 ) ) ), 'p_LES_EQU_'( 
% 0.96/1.32    X, n0 ) ] )
% 0.96/1.32  , clause( 2282, [ 'def_89'( X, Y ), =( 'f_ADD_'( Z, X ), Y ), ~( =( 
% 0.96/1.32    'f_SUB_'( Y, X ), Z ) ) ] )
% 0.96/1.32  , clause( 2283, [ 'def_89'( X, Y ), ~( =( 'f_ADD_'( Z, X ), Y ) ), =( 
% 0.96/1.32    'f_SUB_'( Y, X ), Z ) ] )
% 0.96/1.32  , clause( 2284, [ ~( =( X, Y ) ), ~( 'def_89'( Y, X ) ) ] )
% 0.96/1.32  , clause( 2285, [ 'p_LES_EQU_'( X, Y ), ~( 'def_89'( Y, X ) ) ] )
% 0.96/1.32  , clause( 2286, [ ~( 'p_LES_EQU_'( 'f_ADD_'( X, n1 ), 'f_ADD_'( Y, n1 ) ) )
% 0.96/1.32    , 'p_LES_EQU_'( X, Y ) ] )
% 0.96/1.32  , clause( 2287, [ 'p_LES_EQU_'( 'f_ADD_'( X, n1 ), 'f_ADD_'( Y, n1 ) ), ~( 
% 0.96/1.32    'p_LES_EQU_'( X, Y ) ) ] )
% 0.96/1.32  , clause( 2288, [ =( X, Y ), ~( 'p_LES_EQU_'( Y, X ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'f_ADD_'( Y, n1 ), X ) ] )
% 0.96/1.32  , clause( 2289, [ ~( 'p_LES_EQU_'( X, Y ) ), =( X, Y ), 'p_LES_EQU_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ), Y ) ] )
% 0.96/1.32  , clause( 2290, [ =( X, Y ), ~( 'p_LES_EQU_'( X, Y ) ), ~( 'p_LES_EQU_'( Y
% 0.96/1.32    , X ) ) ] )
% 0.96/1.32  , clause( 2291, [ ~( 'p_LES_EQU_'( X, Y ) ), 'p_LES_EQU_'( Z, Y ), 
% 0.96/1.32    'p_LES_EQU_'( X, Z ) ] )
% 0.96/1.32  , clause( 2292, [ =( 'f_ADD_'( X, n1 ), Y ), ~( 'p_LES_EQU_'( Y, 'f_ADD_'( 
% 0.96/1.32    X, n1 ) ) ), 'p_LES_EQU_'( Y, X ) ] )
% 0.96/1.32  , clause( 2293, [ ~( 'p_LES_EQU_'( X, n0 ) ), =( X, n0 ) ] )
% 0.96/1.32  , clause( 2294, [ =( X, 'f_ADD_'( 'y_105'( X ), n1 ) ), =( X, n0 ) ] )
% 0.96/1.32  , clause( 2295, [ 'p_LES_EQU_'( X, X ) ] )
% 0.96/1.32  , clause( 2296, [ =( X, Y ), ~( =( 'f_ADD_'( X, n1 ), 'f_ADD_'( Y, n1 ) ) )
% 0.96/1.32     ] )
% 0.96/1.32  , clause( 2297, [ =( 'f_ADD_'( n0, X ), X ) ] )
% 0.96/1.32  , clause( 2298, [ =( n1, 'f_ADD_'( n0, n1 ) ) ] )
% 0.96/1.32  , clause( 2299, [ =( 'f__length_'( 'f__cons_'( X, Y ) ), 'f_ADD_'( 
% 0.96/1.32    'f__length_'( Y ), n1 ) ) ] )
% 0.96/1.32  , clause( 2300, [ =( 'f__length_'( 'f__empty_' ), n0 ) ] )
% 0.96/1.32  , clause( 2301, [ =( 'f__length_'( 'f__concat_'( X, Y ) ), 'f_ADD_'( 
% 0.96/1.32    'f__length_'( X ), 'f__length_'( Y ) ) ) ] )
% 0.96/1.32  , clause( 2302, [ =( 'f__length_'( 'f__slice_'( X, Y, Z ) ), 'f_SUB_'( Z, 
% 0.96/1.32    'f_ADD_'( Y, n1 ) ) ) ] )
% 0.96/1.32  , clause( 2303, [ =( 'f__index_'( 'f__others_'( X ), Y ), X ) ] )
% 0.96/1.32  , clause( 2304, [ ~( =( X, n0 ) ), =( 'f__index_'( 'f__cons_'( Y, Z ), X )
% 0.96/1.32    , Y ) ] )
% 0.96/1.32  , clause( 2305, [ 'p_LES_EQU_'( X, n0 ), =( 'f__index_'( 'f__cons_'( Y, Z )
% 0.96/1.32    , X ), 'f__index_'( Z, 'f_SUB_'( X, n1 ) ) ) ] )
% 0.96/1.32  , clause( 2306, [ 'p_LES_EQU_'( length( X ), Y ), =( 'f__index_'( 
% 0.96/1.32    'f__concat_'( X, Z ), Y ), 'f__index_'( X, Y ) ) ] )
% 0.96/1.32  , clause( 2307, [ ~( 'p_LES_EQU_'( length( X ), Y ) ), =( 'f__index_'( 
% 0.96/1.32    'f__concat_'( X, Z ), Y ), 'f__index_'( Z, 'f_SUB_'( Y, length( X ) ) ) )
% 0.96/1.32     ] )
% 0.96/1.32  , clause( 2308, [ =( 'f__index_'( 'f__slice_'( X, Y, Z ), T ), 'f__index_'( 
% 0.96/1.32    X, 'f_ADD_'( T, Y ) ) ) ] )
% 0.96/1.32  , clause( 2309, [ =( 'f__index_'( 'f__and_'( X, Y ), Z ), 'f__and_'( 
% 0.96/1.32    'f__index_'( X, Z ), 'f__index_'( Y, Z ) ) ) ] )
% 0.96/1.32  , clause( 2310, [ =( 'f__index_'( 'f__or_'( X, Y ), Z ), 'f__or_'( 
% 0.96/1.32    'f__index_'( X, Z ), 'f__index_'( Y, Z ) ) ) ] )
% 0.96/1.32  , clause( 2311, [ =( 'f__index_'( 'f__xor_'( X, Y ), Z ), 'f__xor_'( 
% 0.96/1.32    'f__index_'( X, Z ), 'f__index_'( Y, Z ) ) ) ] )
% 0.96/1.32  , clause( 2312, [ =( 'f__index_'( 'f__nand_'( X, Y ), Z ), 'f__nand_'( 
% 0.96/1.32    'f__index_'( X, Z ), 'f__index_'( Y, Z ) ) ) ] )
% 0.96/1.32  , clause( 2313, [ =( 'f__index_'( 'f__nor_'( X, Y ), Z ), 'f__nor_'( 
% 0.96/1.32    'f__index_'( X, Z ), 'f__index_'( Y, Z ) ) ) ] )
% 0.96/1.32  , clause( 2314, [ =( 'f__index_'( 'f__xnor_'( X, Y ), Z ), 'f__xnor_'( 
% 0.96/1.32    'f__index_'( X, Z ), 'f__index_'( Y, Z ) ) ) ] )
% 0.96/1.32  , clause( 2315, [ =( 'f__index_'( 'f__not_'( X ), Y ), 'f__not_'( 
% 0.96/1.32    'f__index_'( X, Y ) ) ) ] )
% 0.96/1.32  , clause( 2316, [ 'p__pred_'( 'f__true_' ) ] )
% 0.96/1.32  , clause( 2317, [ ~( 'p__pred_'( 'f__false_' ) ) ] )
% 0.96/1.32  , clause( 2318, [ ~( =( 'f__false_', 'f__true_' ) ) ] )
% 0.96/1.32  , clause( 2319, [ 'p__pred_'( X ), ~( 'p__pred_'( Y ) ), ~( 'p__pred_'( 
% 0.96/1.32    'f__equiv_'( Y, X ) ) ) ] )
% 0.96/1.32  , clause( 2320, [ ~( 'p__pred_'( X ) ), 'p__pred_'( Y ), ~( 'p__pred_'( 
% 0.96/1.32    'f__equiv_'( Y, X ) ) ) ] )
% 0.96/1.32  , clause( 2321, [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( Y ) ), 'p__pred_'( 
% 0.96/1.32    'f__equiv_'( Y, X ) ) ] )
% 0.96/1.32  , clause( 2322, [ 'p__pred_'( X ), 'p__pred_'( Y ), 'p__pred_'( 'f__equiv_'( 
% 0.96/1.32    Y, X ) ) ] )
% 0.96/1.32  , clause( 2323, [ =( X, Y ), ~( 'p__pred_'( 'f__equal_'( X, Y ) ) ) ] )
% 0.96/1.32  , clause( 2324, [ ~( =( X, Y ) ), 'p__pred_'( 'f__equal_'( X, Y ) ) ] )
% 0.96/1.32  , clause( 2325, [ 'p__pred_'( X ), ~( 'p__pred_'( 'f__and_'( Y, X ) ) ) ]
% 0.96/1.32     )
% 0.96/1.32  , clause( 2326, [ 'p__pred_'( X ), ~( 'p__pred_'( 'f__and_'( X, Y ) ) ) ]
% 0.96/1.32     )
% 0.96/1.32  , clause( 2327, [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( Y ) ), 'p__pred_'( 
% 0.96/1.32    'f__and_'( X, Y ) ) ] )
% 0.96/1.32  , clause( 2328, [ 'p__pred_'( X ), 'p__pred_'( Y ), ~( 'p__pred_'( 'f__or_'( 
% 0.96/1.32    X, Y ) ) ) ] )
% 0.96/1.32  , clause( 2329, [ ~( 'p__pred_'( X ) ), 'p__pred_'( 'f__or_'( Y, X ) ) ] )
% 0.96/1.32  , clause( 2330, [ ~( 'p__pred_'( X ) ), 'p__pred_'( 'f__or_'( X, Y ) ) ] )
% 0.96/1.32  , clause( 2331, [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( Y ) ), ~( 'p__pred_'( 
% 0.96/1.32    'f__xor_'( Y, X ) ) ) ] )
% 0.96/1.32  , clause( 2332, [ 'p__pred_'( X ), 'p__pred_'( Y ), ~( 'p__pred_'( 
% 0.96/1.32    'f__xor_'( Y, X ) ) ) ] )
% 0.96/1.32  , clause( 2333, [ 'p__pred_'( X ), ~( 'p__pred_'( Y ) ), 'p__pred_'( 
% 0.96/1.32    'f__xor_'( Y, X ) ) ] )
% 0.96/1.32  , clause( 2334, [ ~( 'p__pred_'( X ) ), 'p__pred_'( Y ), 'p__pred_'( 
% 0.96/1.32    'f__xor_'( Y, X ) ) ] )
% 0.96/1.32  , clause( 2335, [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( Y ) ), ~( 'p__pred_'( 
% 0.96/1.32    'f__nand_'( X, Y ) ) ) ] )
% 0.96/1.32  , clause( 2336, [ 'p__pred_'( X ), 'p__pred_'( 'f__nand_'( Y, X ) ) ] )
% 0.96/1.32  , clause( 2337, [ 'p__pred_'( X ), 'p__pred_'( 'f__nand_'( X, Y ) ) ] )
% 0.96/1.32  , clause( 2338, [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( 'f__nor_'( Y, X ) )
% 0.96/1.32     ) ] )
% 0.96/1.32  , clause( 2339, [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( 'f__nor_'( X, Y ) )
% 0.96/1.32     ) ] )
% 0.96/1.32  , clause( 2340, [ 'p__pred_'( X ), 'p__pred_'( Y ), 'p__pred_'( 'f__nor_'( 
% 0.96/1.32    X, Y ) ) ] )
% 0.96/1.32  , clause( 2341, [ 'p__pred_'( X ), ~( 'p__pred_'( Y ) ), ~( 'p__pred_'( 
% 0.96/1.32    'f__xnor_'( Y, X ) ) ) ] )
% 0.96/1.32  , clause( 2342, [ ~( 'p__pred_'( X ) ), 'p__pred_'( Y ), ~( 'p__pred_'( 
% 0.96/1.32    'f__xnor_'( Y, X ) ) ) ] )
% 0.96/1.32  , clause( 2343, [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( Y ) ), 'p__pred_'( 
% 0.96/1.32    'f__xnor_'( Y, X ) ) ] )
% 0.96/1.32  , clause( 2344, [ 'p__pred_'( X ), 'p__pred_'( Y ), 'p__pred_'( 'f__xnor_'( 
% 0.96/1.32    Y, X ) ) ] )
% 0.96/1.32  , clause( 2345, [ ~( 'p__pred_'( X ) ), ~( 'p__pred_'( 'f__not_'( X ) ) ) ]
% 0.96/1.32     )
% 0.96/1.32  , clause( 2346, [ 'p__pred_'( X ), 'p__pred_'( 'f__not_'( X ) ) ] )
% 0.96/1.32  , clause( 2347, [ ~( 'p_LES_EQU_'( X, Y ) ), ~( 'p__pred_'( 'f__lt_'( Y, X
% 0.96/1.32     ) ) ) ] )
% 0.96/1.32  , clause( 2348, [ 'p_LES_EQU_'( X, Y ), 'p__pred_'( 'f__lt_'( Y, X ) ) ] )
% 0.96/1.32  , clause( 2349, [ 'p_LES_EQU_'( X, Y ), ~( 'p__pred_'( 'f__leq_'( X, Y ) )
% 0.96/1.32     ) ] )
% 0.96/1.32  , clause( 2350, [ ~( 'p_LES_EQU_'( X, Y ) ), 'p__pred_'( 'f__leq_'( X, Y )
% 0.96/1.32     ) ] )
% 0.96/1.32  , clause( 2351, [ ~( 'p_LES_EQU_'( X, Y ) ), ~( 'p__pred_'( 'f__gt_'( X, Y
% 0.96/1.32     ) ) ) ] )
% 0.96/1.32  , clause( 2352, [ 'p_LES_EQU_'( X, Y ), 'p__pred_'( 'f__gt_'( X, Y ) ) ] )
% 0.96/1.32  , clause( 2353, [ 'p_LES_EQU_'( X, Y ), ~( 'p__pred_'( 'f__geq_'( Y, X ) )
% 0.96/1.32     ) ] )
% 0.96/1.32  , clause( 2354, [ ~( 'p_LES_EQU_'( X, Y ) ), 'p__pred_'( 'f__geq_'( Y, X )
% 0.96/1.32     ) ] )
% 0.96/1.32  , clause( 2355, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( 't_206', n1 ) ) ) ] )
% 0.96/1.32  , clause( 2356, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( 't_206'
% 0.96/1.32     ) ) ) ] )
% 0.96/1.32  , clause( 2357, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) ]
% 0.96/1.32     )
% 0.96/1.32  , clause( 2358, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( 't_206'
% 0.96/1.32     ) ) ) ] )
% 0.96/1.32  ] ).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  eqswap(
% 0.96/1.32  clause( 2362, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ) ) ] )
% 0.96/1.32  , clause( 2225, [ =( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ) ) ] )
% 0.96/1.32  , 0, substitution( 0, [ :=( X, X )] )).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  subsumption(
% 0.96/1.32  clause( 3, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ) ) ] )
% 0.96/1.32  , clause( 2362, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ) ) ] )
% 0.96/1.32  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  paramod(
% 0.96/1.32  clause( 2387, [ ~( =( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ), 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ) ] )
% 0.96/1.32  , clause( 3, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ) ) ] )
% 0.96/1.32  , 0, clause( 2228, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ), 
% 0.96/1.32    ~( =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ) ) ] )
% 0.96/1.32  , 1, 2, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 0.96/1.32    ).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  subsumption(
% 0.96/1.32  clause( 6, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ), ~( =( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ) ] )
% 0.96/1.32  , clause( 2387, [ ~( =( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ), 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ) ] )
% 0.96/1.32  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 
% 0.96/1.32    0 )] ) ).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  subsumption(
% 0.96/1.32  clause( 12, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.32    X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ) ]
% 0.96/1.32     )
% 0.96/1.32  , clause( 2234, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( 
% 0.96/1.32    X ) ) ) ] )
% 0.96/1.32  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 
% 0.96/1.32    1 )] ) ).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  paramod(
% 0.96/1.32  clause( 2894, [ 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ), 
% 0.96/1.32    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 ) )
% 0.96/1.32     ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , clause( 3, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ) ) ] )
% 0.96/1.32  , 0, clause( 2254, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , 1, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 0.96/1.32    ).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  resolution(
% 0.96/1.32  clause( 2895, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 
% 0.96/1.32    X ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.32    X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ) ] )
% 0.96/1.32  , clause( 12, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( 
% 0.96/1.32    X ) ) ) ] )
% 0.96/1.32  , 1, clause( 2894, [ 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), 
% 0.96/1.32    n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, 
% 0.96/1.32    n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p__pred_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.32  , 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 0.96/1.32    ).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  factor(
% 0.96/1.32  clause( 2896, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 
% 0.96/1.32    X ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ) ] )
% 0.96/1.32  , clause( 2895, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 
% 0.96/1.32    X ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.32    X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ) ] )
% 0.96/1.32  , 0, 2, substitution( 0, [ :=( X, X )] )).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  subsumption(
% 0.96/1.32  clause( 32, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.32    X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 'p_LES_EQU_'( 
% 0.96/1.32    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ] )
% 0.96/1.32  , clause( 2896, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.32    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 
% 0.96/1.32    X ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), ~( 
% 0.96/1.32    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ) ] )
% 0.96/1.32  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 
% 0.96/1.32    3 ), ==>( 2, 1 ), ==>( 3, 2 )] ) ).
% 0.96/1.32  
% 0.96/1.32  
% 0.96/1.32  paramod(
% 0.96/1.32  clause( 3540, [ 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ), 
% 0.96/1.32    ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, n1 ) )
% 0.96/1.33     ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.96/1.33    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.33    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.33  , clause( 3, [ =( 'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), 
% 0.96/1.33    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ) ) ] )
% 0.96/1.33  , 0, clause( 2266, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.33    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 
% 0.96/1.33    'fwork_DOTfifo_DOTrtl_DOTint__level_'( X ), n0 ), ~( 'p__pred_'( 
% 0.96/1.33    'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 'p__pred_'( 
% 0.96/1.33    'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.33    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.33  , 1, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 0.96/1.33    ).
% 0.96/1.33  
% 0.96/1.33  
% 0.96/1.33  resolution(
% 0.96/1.33  clause( 3541, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.33    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 
% 0.96/1.33    X ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.33    X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 
% 0.96/1.33    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ] )
% 0.96/1.33  , clause( 12, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.33    'f_ADD_'( X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTreset_'( 
% 0.96/1.33    X ) ) ) ] )
% 0.96/1.33  , 1, clause( 3540, [ 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), 
% 0.96/1.33    n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( X, 
% 0.96/1.33    n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 
% 0.96/1.33    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p__pred_'( 
% 0.96/1.33    'fwork_DOTfifo_DOTrtl_DOTreset_'( X ) ) ] )
% 0.96/1.33  , 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 0.96/1.33    ).
% 0.96/1.33  
% 0.96/1.33  
% 0.96/1.33  factor(
% 0.96/1.33  clause( 3542, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.33    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 
% 0.96/1.33    X ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 
% 0.96/1.33    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ] )
% 0.96/1.33  , clause( 3541, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.33    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 
% 0.96/1.33    X ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.33    X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 
% 0.96/1.33    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ] )
% 0.96/1.33  , 0, 2, substitution( 0, [ :=( X, X )] )).
% 0.96/1.33  
% 0.96/1.33  
% 0.96/1.33  subsumption(
% 0.96/1.33  clause( 44, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.33    X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 
% 0.96/1.33    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p_LES_EQU_'( 
% 0.96/1.33    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ] )
% 0.96/1.33  , clause( 3542, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.33    'f_ADD_'( X, n1 ) ) ) ), 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 
% 0.96/1.33    X ), n0 ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X ) ) ), 
% 0.96/1.33    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ] )
% 0.96/1.33  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 
% 0.96/1.33    3 ), ==>( 2, 1 ), ==>( 3, 2 )] ) ).
% 0.96/1.33  
% 0.96/1.33  
% 0.96/1.33  subsumption(
% 0.96/1.33  clause( 70, [ ~( 'p_LES_EQU_'( X, n0 ) ), =( X, n0 ) ] )
% 0.96/1.33  , clause( 2293, [ ~( 'p_LES_EQU_'( X, n0 ) ), =( X, n0 ) ] )
% 0.96/1.33  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 
% 0.96/1.33    1 )] ) ).
% 0.96/1.33  
% 0.96/1.33  
% 0.96/1.33  subsumption(
% 0.96/1.33  clause( 131, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 'f_ADD_'( 
% 0.96/1.33    't_206', n1 ) ) ) ] )
% 0.96/1.33  , clause( 2355, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 0.96/1.33    'f_ADD_'( 't_206', n1 ) ) ) ] )
% 0.96/1.33  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.96/1.33  
% 0.96/1.33  
% 0.96/1.33  subsumption(
% 0.96/1.33  clause( 133, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) ] )
% 0.96/1.33  , clause( 2357, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) ]
% 0.96/1.33     )
% 0.96/1.33  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.96/1.33  
% 0.96/1.33  
% 0.96/1.33  subsumption(
% 0.96/1.33  clause( 134, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( 't_206' ) )
% 0.96/1.33     ) ] )
% 0.96/1.33  , clause( 2358, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( 't_206'
% 0.96/1.33     ) ) ) ] )
% 0.96/1.33  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.96/1.33  
% 0.96/1.33  
% 0.96/1.33  eqswap(
% 0.96/1.33  clause( 4045, [ ~( =( n0, 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ) ) ), 
% 1.76/2.16    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ) ] )
% 1.76/2.16  , clause( 6, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ), ~( =( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ) ] )
% 1.76/2.16  , 1, substitution( 0, [ :=( X, X )] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  resolution(
% 1.76/2.16  clause( 4046, [ ~( =( n0, 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' ) ) ) ]
% 1.76/2.16     )
% 1.76/2.16  , clause( 134, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( 't_206' )
% 1.76/2.16     ) ) ] )
% 1.76/2.16  , 0, clause( 4045, [ ~( =( n0, 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ) ) ), 
% 1.76/2.16    'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTempty_'( X ) ) ] )
% 1.76/2.16  , 1, substitution( 0, [] ), substitution( 1, [ :=( X, 't_206' )] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  eqswap(
% 1.76/2.16  clause( 4047, [ ~( =( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' ), n0 ) ) ]
% 1.76/2.16     )
% 1.76/2.16  , clause( 4046, [ ~( =( n0, 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' ) ) )
% 1.76/2.16     ] )
% 1.76/2.16  , 0, substitution( 0, [] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  subsumption(
% 1.76/2.16  clause( 194, [ ~( =( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' ), n0 ) ) ]
% 1.76/2.16     )
% 1.76/2.16  , clause( 4047, [ ~( =( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' ), n0 ) )
% 1.76/2.16     ] )
% 1.76/2.16  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  eqswap(
% 1.76/2.16  clause( 4049, [ ~( =( n0, 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' ) ) ) ]
% 1.76/2.16     )
% 1.76/2.16  , clause( 194, [ ~( =( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' ), n0 ) )
% 1.76/2.16     ] )
% 1.76/2.16  , 0, substitution( 0, [] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  paramod(
% 1.76/2.16  clause( 5517, [ ~( =( n0, n0 ) ), ~( 'p_LES_EQU_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' ), n0 ) ) ] )
% 1.76/2.16  , clause( 70, [ ~( 'p_LES_EQU_'( X, n0 ) ), =( X, n0 ) ] )
% 1.76/2.16  , 1, clause( 4049, [ ~( =( n0, 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' )
% 1.76/2.16     ) ) ] )
% 1.76/2.16  , 0, 3, substitution( 0, [ :=( X, 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206'
% 1.76/2.16     ) )] ), substitution( 1, [] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  eqrefl(
% 1.76/2.16  clause( 5576, [ ~( 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206'
% 1.76/2.16     ), n0 ) ) ] )
% 1.76/2.16  , clause( 5517, [ ~( =( n0, n0 ) ), ~( 'p_LES_EQU_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' ), n0 ) ) ] )
% 1.76/2.16  , 0, substitution( 0, [] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  subsumption(
% 1.76/2.16  clause( 288, [ ~( 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206' )
% 1.76/2.16    , n0 ) ) ] )
% 1.76/2.16  , clause( 5576, [ ~( 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 
% 1.76/2.16    't_206' ), n0 ) ) ] )
% 1.76/2.16  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  resolution(
% 1.76/2.16  clause( 5577, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 1.76/2.16    'f_ADD_'( 't_206', n1 ) ) ) ), ~( 'p__pred_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) ), ~( 'p__pred_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ) ] )
% 1.76/2.16  , clause( 288, [ ~( 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206'
% 1.76/2.16     ), n0 ) ) ] )
% 1.76/2.16  , 0, clause( 32, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 1.76/2.16    'f_ADD_'( X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X
% 1.76/2.16     ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ) ), 
% 1.76/2.16    'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ] )
% 1.76/2.16  , 3, substitution( 0, [] ), substitution( 1, [ :=( X, 't_206' )] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  resolution(
% 1.76/2.16  clause( 5578, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) )
% 1.76/2.16    , ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ) ] )
% 1.76/2.16  , clause( 5577, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 1.76/2.16    'f_ADD_'( 't_206', n1 ) ) ) ), ~( 'p__pred_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) ), ~( 'p__pred_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ) ] )
% 1.76/2.16  , 0, clause( 131, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 1.76/2.16    'f_ADD_'( 't_206', n1 ) ) ) ] )
% 1.76/2.16  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  subsumption(
% 1.76/2.16  clause( 1455, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) )
% 1.76/2.16    , ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ) ] )
% 1.76/2.16  , clause( 5578, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) )
% 1.76/2.16     ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ) ] )
% 1.76/2.16  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 1.76/2.16     ).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  resolution(
% 1.76/2.16  clause( 5579, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) )
% 1.76/2.16     ] )
% 1.76/2.16  , clause( 1455, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) )
% 1.76/2.16     ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ) ] )
% 1.76/2.16  , 0, clause( 133, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) )
% 1.76/2.16     ] )
% 1.76/2.16  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  subsumption(
% 1.76/2.16  clause( 1459, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) )
% 1.76/2.16     ] )
% 1.76/2.16  , clause( 5579, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) )
% 1.76/2.16     ) ] )
% 1.76/2.16  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  resolution(
% 1.76/2.16  clause( 5580, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 1.76/2.16    'f_ADD_'( 't_206', n1 ) ) ) ), ~( 'p__pred_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) ), 'p__pred_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ] )
% 1.76/2.16  , clause( 288, [ ~( 'p_LES_EQU_'( 'fwork_DOTfifo_DOTrtl_DOTlevel_'( 't_206'
% 1.76/2.16     ), n0 ) ) ] )
% 1.76/2.16  , 0, clause( 44, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 1.76/2.16    'f_ADD_'( X, n1 ) ) ) ), ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( X
% 1.76/2.16     ) ) ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( X ) ), 'p_LES_EQU_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTlevel_'( X ), n0 ) ] )
% 1.76/2.16  , 3, substitution( 0, [] ), substitution( 1, [ :=( X, 't_206' )] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  resolution(
% 1.76/2.16  clause( 5581, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) )
% 1.76/2.16    , 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ] )
% 1.76/2.16  , clause( 5580, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 1.76/2.16    'f_ADD_'( 't_206', n1 ) ) ) ), ~( 'p__pred_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) ), 'p__pred_'( 
% 1.76/2.16    'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ] )
% 1.76/2.16  , 0, clause( 131, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd__error_'( 
% 1.76/2.16    'f_ADD_'( 't_206', n1 ) ) ) ] )
% 1.76/2.16  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  subsumption(
% 1.76/2.16  clause( 2216, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) ) )
% 1.76/2.16    , 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ] )
% 1.76/2.16  , clause( 5581, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) )
% 1.76/2.16     ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ] )
% 1.76/2.16  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 1.76/2.16     ).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  resolution(
% 1.76/2.16  clause( 5582, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ] )
% 1.76/2.16  , clause( 2216, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) )
% 1.76/2.16     ), 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) ) ] )
% 1.76/2.16  , 0, clause( 133, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTrd_'( 't_206' ) )
% 1.76/2.16     ] )
% 1.76/2.16  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  resolution(
% 1.76/2.16  clause( 5583, [] )
% 1.76/2.16  , clause( 1459, [ ~( 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) )
% 1.76/2.16     ) ] )
% 1.76/2.16  , 0, clause( 5582, [ 'p__pred_'( 'fwork_DOTfifo_DOTrtl_DOTwr_'( 't_206' ) )
% 1.76/2.16     ] )
% 1.76/2.16  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  subsumption(
% 1.76/2.16  clause( 2220, [] )
% 1.76/2.16  , clause( 5583, [] )
% 1.76/2.16  , substitution( 0, [] ), permutation( 0, [] ) ).
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  end.
% 1.76/2.16  
% 1.76/2.16  % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 1.76/2.16  
% 1.76/2.16  Memory use:
% 1.76/2.16  
% 1.76/2.16  space for terms:        44345
% 1.76/2.16  space for clauses:      128663
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  clauses generated:      7123
% 1.76/2.16  clauses kept:           2221
% 1.76/2.16  clauses selected:       217
% 1.76/2.16  clauses deleted:        16
% 1.76/2.16  clauses inuse deleted:  6
% 1.76/2.16  
% 1.76/2.16  subsentry:          274544
% 1.76/2.16  literals s-matched: 211903
% 1.76/2.16  literals matched:   200241
% 1.76/2.16  full subsumption:   195596
% 1.76/2.16  
% 1.76/2.16  checksum:           -1182941818
% 1.76/2.16  
% 1.76/2.16  
% 1.76/2.16  Bliksem ended
%------------------------------------------------------------------------------