Vampire---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : ITP408_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n010.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 11:33:49 AM UTC 2026

% Result   : Theorem 23.04s 4.77s
% Output   : Refutation 26.91s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   14
%            Number of leaves      :   11
% Syntax   : Number of formulae    :   65 (  21 unt;   0 typ;   3 def)
%            Number of atoms       :  144 (  35 equ)
%            Maximal formula atoms :    6 (   2 avg)
%            Number of connectives :  142 (  63   ~;  54   |;  15   &)
%                                         (   8 <=>;   2  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   11 (   5 avg)
%            Maximal term depth    :   11 (   3 avg)
%            Number of types       :  108 ( 106 usr;   1 ari;   0 dat;   0 cdt)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :   68 (  66 usr;   4 prp; 0-4 aty)
%            Number of functors    :  318 ( 318 usr;  46 con; 0-4 aty)
%            Number of variables   :  144 (   0 sgn 144   !;   0   ?; 144   :)

% Comments : 
%------------------------------------------------------------------------------
tff(type_def_5,type,
    'A_constr_a_TESL_atomic_fun$': $tType ).

tff(type_def_6,type,
    'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$': $tType ).

tff(type_def_7,type,
    'A_constr_list_a_constr_list_prod_set$': $tType ).

tff(type_def_8,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$': $tType ).

tff(type_def_9,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_bool_fun$': $tType ).

tff(type_def_10,type,
    'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$': $tType ).

tff(type_def_11,type,
    'A_constr_list_a_TESL_atomic_list_prod$': $tType ).

tff(type_def_12,type,
    'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$': $tType ).

tff(type_def_13,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$': $tType ).

tff(type_def_14,type,
    'Clock$': $tType ).

tff(type_def_15,type,
    'A_TESL_atomic_a_constr_prod$': $tType ).

tff(type_def_16,type,
    'A_constr_list_a_constr_list_fun$': $tType ).

tff(type_def_17,type,
    'A_TESL_atomic_list_list$': $tType ).

tff(type_def_18,type,
    'Nat_a_TESL_atomic_prod$': $tType ).

tff(type_def_19,type,
    'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$': $tType ).

tff(type_def_20,type,
    'A_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod_bool_fun$': $tType ).

tff(type_def_21,type,
    'A_TESL_atomic_a_constr_bool_fun_fun$': $tType ).

tff(type_def_22,type,
    'Nat_list$': $tType ).

tff(type_def_23,type,
    'A_TESL_atomic_list_set$': $tType ).

tff(type_def_24,type,
    'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod_bool_fun$': $tType ).

tff(type_def_25,type,
    'Nat_a_constr_prod$': $tType ).

tff(type_def_26,type,
    'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$': $tType ).

tff(type_def_27,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_fun$': $tType ).

tff(type_def_28,type,
    'A_constr_list$': $tType ).

tff(type_def_29,type,
    'A_TESL_atomic_list_a_constr_list_bool_fun_fun$': $tType ).

tff(type_def_30,type,
    'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$': $tType ).

tff(type_def_31,type,
    'A_constr_a_constr_bool_fun_fun_a_constr_list_prod_bool_fun$': $tType ).

tff(type_def_32,type,
    'A_constr_a_TESL_atomic_prod_set$': $tType ).

tff(type_def_33,type,
    'A_TESL_atomic_list$': $tType ).

tff(type_def_34,type,
    'A_constr_a_constr_list_fun$': $tType ).

tff(type_def_35,type,
    'A_TESL_atomic_list_a_TESL_atomic_list_prod$': $tType ).

tff(type_def_36,type,
    'Tag_val$': $tType ).

tff(type_def_37,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$': $tType ).

tff(type_def_38,type,
    'A_tag_const$': $tType ).

tff(type_def_39,type,
    'A_constr_a_TESL_atomic_prod$': $tType ).

tff(type_def_40,type,
    'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$': $tType ).

tff(type_def_41,type,
    'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$': $tType ).

tff(type_def_42,type,
    'A_TESL_atomic_list_a_TESL_atomic_list_fun$': $tType ).

tff(type_def_43,type,
    'A_TESL_atomic_a_TESL_atomic_prod_set$': $tType ).

tff(type_def_44,type,
    'A_constr_set$': $tType ).

tff(type_def_45,type,
    'A_tag_const_a_tag_const_prod_bool_fun$': $tType ).

tff(type_def_46,type,
    'A_TESL_atomic_set$': $tType ).

tff(type_def_47,type,
    'Nat$': $tType ).

tff(type_def_48,type,
    'A_constr_list_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list_prod$': $tType ).

tff(type_def_49,type,
    'A_constr_list_a_TESL_atomic_list_bool_fun_fun$': $tType ).

tff(type_def_50,type,
    'A_constr_list_a_constr_list_prod$': $tType ).

tff(type_def_51,type,
    'A_constr_list_a_constr_list_prod_a_constr_list_a_constr_list_prod_bool_fun_fun$': $tType ).

tff(type_def_52,type,
    'A_constr$': $tType ).

tff(type_def_53,type,
    'Clock_nat_prod$': $tType ).

tff(type_def_54,type,
    'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list$': $tType ).

tff(type_def_55,type,
    'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_a_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$': $tType ).

tff(type_def_56,type,
    'A_constr_a_TESL_atomic_bool_fun_fun$': $tType ).

tff(type_def_57,type,
    'Nat_a_TESL_atomic_prod_list$': $tType ).

tff(type_def_58,type,
    'A_TESL_atomic_a_constr_fun$': $tType ).

tff(type_def_59,type,
    'A_constr_list_a_TESL_atomic_list_prod_set$': $tType ).

tff(type_def_60,type,
    'A_TESL_atomic_bool_fun$': $tType ).

tff(type_def_61,type,
    tlbool: $tType ).

tff(type_def_62,type,
    'A_TESL_atomic_a_TESL_atomic_fun$': $tType ).

tff(type_def_63,type,
    'A_constr_a_constr_fun_a_constr_list_a_constr_list_prod_prod_a_constr_a_constr_fun_a_constr_list_a_constr_list_prod_prod_bool_fun_fun$': $tType ).

tff(type_def_64,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list$': $tType ).

tff(type_def_65,type,
    'A_TESL_atomic_list_a_constr_list_prod_set$': $tType ).

tff(type_def_66,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$': $tType ).

tff(type_def_67,type,
    'A_constr_a_constr_prod_set$': $tType ).

tff(type_def_68,type,
    'A_TESL_atomic_a_TESL_atomic_list_fun$': $tType ).

tff(type_def_69,type,
    'A_constr_list_a_constr_list_bool_fun_fun$': $tType ).

tff(type_def_70,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$': $tType ).

tff(type_def_71,type,
    'A_TESL_atomic_list_bool_fun$': $tType ).

tff(type_def_72,type,
    'Nat_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_list_prod_set$': $tType ).

tff(type_def_73,type,
    'Nat_a_constr_prod_list$': $tType ).

tff(type_def_74,type,
    'A_constr_a_constr_bool_fun_fun$': $tType ).

tff(type_def_75,type,
    'A_TESL_atomic_list_a_TESL_atomic_list_prod_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$': $tType ).

tff(type_def_76,type,
    'A_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod_bool_fun$': $tType ).

tff(type_def_77,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_set$': $tType ).

tff(type_def_78,type,
    'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$': $tType ).

tff(type_def_79,type,
    'A_TESL_atomic_list_list_a_TESL_atomic_list_list_prod$': $tType ).

tff(type_def_80,type,
    'A_constr_a_constr_fun$': $tType ).

tff(type_def_81,type,
    'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$': $tType ).

tff(type_def_82,type,
    'A_TESL_atomic$': $tType ).

tff(type_def_83,type,
    'A_TESL_atomic_list_a_constr_list_prod$': $tType ).

tff(type_def_84,type,
    'A_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod$': $tType ).

tff(type_def_85,type,
    'A_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod$': $tType ).

tff(type_def_86,type,
    'Nat_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$': $tType ).

tff(type_def_87,type,
    'A_constr_list_bool_fun$': $tType ).

tff(type_def_88,type,
    'A_constr_list_set$': $tType ).

tff(type_def_89,type,
    'A_TESL_atomic_list_a_TESL_atomic_list_set_fun$': $tType ).

tff(type_def_90,type,
    'A_constr_bool_fun$': $tType ).

tff(type_def_91,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod$': $tType ).

tff(type_def_92,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$': $tType ).

tff(type_def_93,type,
    'A_constr_a_constr_prod$': $tType ).

tff(type_def_94,type,
    'A_TESL_atomic_list_nat_fun$': $tType ).

tff(type_def_95,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun_fun$': $tType ).

tff(type_def_96,type,
    'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$': $tType ).

tff(type_def_97,type,
    'Nat_bool_fun$': $tType ).

tff(type_def_98,type,
    'A_constr_list_list$': $tType ).

tff(type_def_99,type,
    'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_bool_fun$': $tType ).

tff(type_def_100,type,
    'A_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod_a_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$': $tType ).

tff(type_def_101,type,
    'Nat_set$': $tType ).

tff(type_def_102,type,
    'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$': $tType ).

tff(type_def_103,type,
    'A_TESL_atomic_list_a_TESL_atomic_list_prod_list$': $tType ).

tff(type_def_104,type,
    'Nat_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_list_prod$': $tType ).

tff(type_def_105,type,
    'A_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod_a_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod_bool_fun_fun$': $tType ).

tff(type_def_106,type,
    'A_constr_a_constr_fun_a_constr_list_a_constr_list_prod_prod$': $tType ).

tff(type_def_107,type,
    'A_constr_list_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list_prod_set$': $tType ).

tff(type_def_108,type,
    'A_TESL_atomic_list_list_a_TESL_atomic_list_list_prod_set$': $tType ).

tff(type_def_109,type,
    'A_TESL_atomic_a_constr_prod_set$': $tType ).

tff(type_def_110,type,
    'A_TESL_atomic_a_TESL_atomic_prod$': $tType ).

tff(func_def_0,type,
    'bot$i': 'Nat$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' ).

tff(func_def_1,type,
    'uut$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_2,type,
    'uvb$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_3,type,
    'map_tailrec_rev$b': ( 'A_TESL_atomic_a_constr_fun$' * 'A_TESL_atomic_list$' * 'A_constr_list$' ) > 'A_constr_list$' ).

tff(func_def_4,type,
    'cons$g': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list$' ).

tff(func_def_5,type,
    'is_empty$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_bool_fun$' ).

tff(func_def_6,type,
    'insert$d': ( 'A_TESL_atomic_list$' * 'A_TESL_atomic_list_set$' ) > 'A_TESL_atomic_list_set$' ).

tff(func_def_7,type,
    'uuo$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_8,type,
    'fun_app$ak': ( 'A_TESL_atomic_list_a_TESL_atomic_list_set_fun$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list_set$' ).

tff(func_def_9,type,
    'uu$': 'A_constr_list_a_constr_list_bool_fun_fun$' ).

tff(func_def_10,type,
    'nil$g': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list$' ).

tff(func_def_11,type,
    'bot$a': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ).

tff(func_def_12,type,
    'splice_rel$a': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' ).

tff(func_def_13,type,
    'map_tailrec_rev_rel$b': 'A_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod_a_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod_bool_fun_fun$' ).

tff(func_def_14,type,
    'bot$k': 'A_constr_list$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' ).

tff(func_def_15,type,
    'sup$h': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_16,type,
    'snds$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ).

tff(func_def_17,type,
    'image$a': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_set$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ).

tff(func_def_18,type,
    'pair$e': ( 'A_constr_a_TESL_atomic_fun$' * 'A_constr_list_a_TESL_atomic_list_prod$' ) > 'A_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod$' ).

tff(func_def_19,type,
    'collect$c': 'A_TESL_atomic_list_bool_fun$' > 'A_TESL_atomic_list_set$' ).

tff(func_def_20,type,
    'tagArith$': ( 'Tag_val$' * 'Tag_val$' * 'A_tag_const_a_tag_const_prod_bool_fun$' ) > 'A_constr$' ).

tff(func_def_21,type,
    'uvj$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_22,type,
    'insert$f': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_23,type,
    'pair$v': ( 'A_constr_a_constr_fun$' * 'A_constr_list_a_constr_list_prod$' ) > 'A_constr_a_constr_fun_a_constr_list_a_constr_list_prod_prod$' ).

tff(func_def_24,type,
    'pair$n': ( 'A_constr$' * 'A_constr$' ) > 'A_constr_a_constr_prod$' ).

tff(func_def_25,type,
    'tagRelation$': ( 'Clock$' * 'Clock$' * 'A_tag_const_a_tag_const_prod_bool_fun$' ) > 'A_TESL_atomic$' ).

tff(func_def_26,type,
    'nil$f': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_list$' ).

tff(func_def_27,type,
    'fun_app$y': ( 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' * 'A_constr_list$' ) > 'A_TESL_atomic_list_bool_fun$' ).

tff(func_def_28,type,
    'pair$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod$' ).

tff(func_def_29,type,
    'pair$i': ( 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' ).

tff(func_def_30,type,
    'implies$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).

tff(func_def_31,type,
    'uuz$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_32,type,
    'strictlyPrecedes$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).

tff(func_def_33,type,
    'bot$d': 'A_TESL_atomic_list_set$' ).

tff(func_def_34,type,
    'bot$g': 'A_TESL_atomic_set$' ).

tff(func_def_35,type,
    'positive_atom_rel$': 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' ).

tff(func_def_36,type,
    'collect$e': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ).

tff(func_def_37,type,
    'fun_app$s': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_38,type,
    'bot$c': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_set$' ).

tff(func_def_39,type,
    'fun_app$': ( 'A_constr_a_constr_list_fun$' * 'A_constr$' ) > 'A_constr_list$' ).

tff(func_def_40,type,
    'operational_semantics_elim$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_41,type,
    'lists$a': 'A_constr_set$' > 'A_constr_list_set$' ).

tff(func_def_42,type,
    'rangep$b': 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic_list_bool_fun$' ).

tff(func_def_43,type,
    'uul$': 'Nat$' > 'Nat_bool_fun$' ).

tff(func_def_44,type,
    'uuh$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_bool_fun$' ).

tff(func_def_45,type,
    'less_eq$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_bool_fun$' ).

tff(func_def_46,type,
    'shuffles_rel$a': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' ).

tff(func_def_47,type,
    'fun_app$af': ( 'A_TESL_atomic_a_constr_bool_fun_fun$' * 'A_TESL_atomic$' ) > 'A_constr_bool_fun$' ).

tff(func_def_48,type,
    'pair$p': ( 'A_constr$' * 'A_TESL_atomic$' ) > 'A_constr_a_TESL_atomic_prod$' ).

tff(func_def_49,type,
    'accp$b': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' ).

tff(func_def_50,type,
    'member$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_bool_fun$' ).

tff(func_def_51,type,
    'set_Cons$a': ( 'A_TESL_atomic_set$' * 'A_TESL_atomic_list_set$' ) > 'A_TESL_atomic_list_set$' ).

tff(func_def_52,type,
    'uvd$': 'A_constr_a_constr_list_fun$' ).

tff(func_def_53,type,
    'uux$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_54,type,
    'uuc$': 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' ).

tff(func_def_55,type,
    'image$g': ( 'A_constr_list_a_constr_list_fun$' * 'A_constr_list_set$' ) > 'A_constr_list_set$' ).

tff(func_def_56,type,
    'ticks$': ( 'Clock$' * 'Nat$' ) > 'A_constr$' ).

tff(func_def_57,type,
    'image$d': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' ).

tff(func_def_58,type,
    'listrelp$e': 'A_constr_a_TESL_atomic_bool_fun_fun$' > 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' ).

tff(func_def_59,type,
    'n$': 'Nat$' ).

tff(func_def_60,type,
    'nil$c': 'A_TESL_atomic_list_list$' ).

tff(func_def_61,type,
    'enumerate$': ( 'Nat$' * 'A_constr_list$' ) > 'Nat_a_constr_prod_list$' ).

tff(func_def_62,type,
    'enumerate$b': ( 'Nat$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_list$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list$' ).

tff(func_def_63,type,
    'uub$': 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ).

tff(func_def_64,type,
    'sup$c': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' * 'A_constr_list$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' ).

tff(func_def_65,type,
    'notTicksFrom$': ( 'Clock$' * 'Nat$' ) > 'A_constr$' ).

tff(func_def_66,type,
    'bot$l': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' ).

tff(func_def_67,type,
    'splice$a': ( 'A_TESL_atomic_list$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list$' ).

tff(func_def_68,type,
    'bot$h': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_69,type,
    'fun_app$q': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' * 'A_constr_list$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' ).

tff(func_def_70,type,
    'rangep$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' ).

tff(func_def_71,type,
    'insert$a': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ).

tff(func_def_72,type,
    'accp$f': 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_a_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' > 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' ).

tff(func_def_73,type,
    'fun_app$a': ( 'A_constr_list_a_constr_list_fun$' * 'A_constr_list$' ) > 'A_constr_list$' ).

tff(func_def_74,type,
    'of_nat$': 'Nat$' > $int ).

tff(func_def_75,type,
    'weaklyPrecedes$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).

tff(func_def_76,type,
    'gen_length$a': 'Nat$' > 'A_TESL_atomic_list_nat_fun$' ).

tff(func_def_77,type,
    'lists$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_set$' ).

tff(func_def_78,type,
    'snds$a': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_79,type,
    'k_2$': 'Clock$' ).

tff(func_def_80,type,
    'image$e': ( 'A_constr_a_constr_list_fun$' * 'A_constr_set$' ) > 'A_constr_list_set$' ).

tff(func_def_81,type,
    'sporadicOn$': ( 'Clock$' * 'A_tag_const$' * 'Clock$' ) > 'A_TESL_atomic$' ).

tff(func_def_82,type,
    'mlex_prod$': ( 'A_TESL_atomic_list_nat_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_83,type,
    'impliesNot$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).

tff(func_def_84,type,
    'operational_semantics_step$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_85,type,
    'cons$c': ( 'A_TESL_atomic_list$' * 'A_TESL_atomic_list_list$' ) > 'A_TESL_atomic_list_list$' ).

tff(func_def_86,type,
    'uus$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_87,type,
    'cons$d': ( 'Nat_a_constr_prod$' * 'Nat_a_constr_prod_list$' ) > 'Nat_a_constr_prod_list$' ).

tff(func_def_88,type,
    'fun_app$p': ( 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' * 'A_TESL_atomic$' ) > 'A_TESL_atomic_bool_fun$' ).

tff(func_def_89,type,
    'the_elem$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_90,type,
    'uud$': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' ).

tff(func_def_91,type,
    'cons$a': 'A_TESL_atomic$' > 'A_TESL_atomic_list_a_TESL_atomic_list_fun$' ).

tff(func_def_92,type,
    'listrel$b': 'A_TESL_atomic_a_constr_prod_set$' > 'A_TESL_atomic_list_a_constr_list_prod_set$' ).

tff(func_def_93,type,
    'kills$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).

tff(func_def_94,type,
    'insert$e': ( 'Nat$' * 'Nat_set$' ) > 'Nat_set$' ).

tff(func_def_95,type,
    'operational_semantics_intro$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_96,type,
    'collect$f': 'Nat_bool_fun$' > 'Nat_set$' ).

tff(func_def_97,type,
    'fun_app$ah': ( 'A_constr_a_TESL_atomic_fun$' * 'A_constr$' ) > 'A_TESL_atomic$' ).

tff(func_def_98,type,
    'accp$e': 'A_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod_a_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod_bool_fun_fun$' > 'A_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod_bool_fun$' ).

tff(func_def_99,type,
    'uvg$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_100,type,
    'range$a': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_101,type,
    'bot$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_102,type,
    'fun_app$al': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' ).

tff(func_def_103,type,
    'fun_app$c': ( 'A_TESL_atomic_list_a_TESL_atomic_list_fun$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list$' ).

tff(func_def_104,type,
    'splice$': ( 'A_constr_list$' * 'A_constr_list$' ) > 'A_constr_list$' ).

tff(func_def_105,type,
    'pair$d': ( 'Nat$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ).

tff(func_def_106,type,
    'uuj$': 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' ).

tff(func_def_107,type,
    'pair$m': ( 'Nat$' * 'A_TESL_atomic$' ) > 'Nat_a_TESL_atomic_prod$' ).

tff(func_def_108,type,
    'uuq$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_109,type,
    'listrel$a': 'A_constr_a_TESL_atomic_prod_set$' > 'A_constr_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_110,type,
    'pair$b': ( 'A_constr_list$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_111,type,
    tltrue: tlbool ).

tff(func_def_112,type,
    'bot$j': 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ).

tff(func_def_113,type,
    'uui$': 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ).

tff(func_def_114,type,
    'nil$a': 'A_TESL_atomic_list$' ).

tff(func_def_115,type,
    'map_tailrec_rev_rel$c': 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_a_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' ).

tff(func_def_116,type,
    'sup$b': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun_fun$' ).

tff(func_def_117,type,
    'tSchematic$': 'Clock_nat_prod$' > 'Tag_val$' ).

tff(func_def_118,type,
    'uve$': 'A_TESL_atomic_a_TESL_atomic_list_fun$' ).

tff(func_def_119,type,
    'nil$e': 'Nat_list$' ).

tff(func_def_120,type,
    'collect$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_121,type,
    'listrel$': 'A_constr_a_constr_prod_set$' > 'A_constr_list_a_constr_list_prod_set$' ).

tff(func_def_122,type,
    'listrel$d': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' > 'Nat_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_list_prod_set$' ).

tff(func_def_123,type,
    'fun_app$ab': ( 'A_TESL_atomic_list_nat_fun$' * 'A_TESL_atomic_list$' ) > 'Nat$' ).

tff(func_def_124,type,
    'listrel$e': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' > 'A_TESL_atomic_list_list_a_TESL_atomic_list_list_prod_set$' ).

tff(func_def_125,type,
    'cons$b': ( 'A_constr_list$' * 'A_constr_list_list$' ) > 'A_constr_list_list$' ).

tff(func_def_126,type,
    'shuffles_rel$': 'A_constr_list_a_constr_list_prod_a_constr_list_a_constr_list_prod_bool_fun_fun$' ).

tff(func_def_127,type,
    'nil$b': 'A_constr_list_list$' ).

tff(func_def_128,type,
    'fun_app$j': ( 'A_constr_list_a_constr_list_bool_fun_fun$' * 'A_constr_list$' ) > 'A_constr_list_bool_fun$' ).

tff(func_def_129,type,
    'fun_app$e': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_130,type,
    'psi$': 'A_TESL_atomic_list$' ).

tff(func_def_131,type,
    'fun_app$aj': ( 'A_TESL_atomic_a_TESL_atomic_fun$' * 'A_TESL_atomic$' ) > 'A_TESL_atomic$' ).

tff(func_def_132,type,
    'pair$s': ( 'A_constr_list_list$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list$' ) > 'A_constr_list_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list_prod$' ).

tff(func_def_133,type,
    'insert$c': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_set$' ).

tff(func_def_134,type,
    'fun_app$ae': ( 'A_constr_a_TESL_atomic_bool_fun_fun$' * 'A_constr$' ) > 'A_TESL_atomic_bool_fun$' ).

tff(func_def_135,type,
    'uue$': 'Nat$' > 'Nat_bool_fun$' ).

tff(func_def_136,type,
    'bot$f': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_137,type,
    'uvh$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_138,type,
    'gamma$': 'A_constr_list$' ).

tff(func_def_139,type,
    'pair$u': ( 'A_TESL_atomic_list_list$' * 'A_TESL_atomic_list_list$' ) > 'A_TESL_atomic_list_list_a_TESL_atomic_list_list_prod$' ).

tff(func_def_140,type,
    'timeDelayedBy$': ( 'Clock$' * 'A_tag_const$' * 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).

tff(func_def_141,type,
    'uvc$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_142,type,
    'splice_rel$': 'A_constr_list_a_constr_list_prod_a_constr_list_a_constr_list_prod_bool_fun_fun$' ).

tff(func_def_143,type,
    'aboveS$a': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list_set$' ).

tff(func_def_144,type,
    'cons$e': ( 'Nat_a_TESL_atomic_prod$' * 'Nat_a_TESL_atomic_prod_list$' ) > 'Nat_a_TESL_atomic_prod_list$' ).

tff(func_def_145,type,
    'rangep$a': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' ).

tff(func_def_146,type,
    'bot$b': 'A_constr_list_set$' ).

tff(func_def_147,type,
    'pair$k': ( 'A_constr_list$' * 'A_constr_list$' ) > 'A_constr_list_a_constr_list_prod$' ).

tff(func_def_148,type,
    'collect$b': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_bool_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_set$' ).

tff(func_def_149,type,
    'range$b': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' > 'A_TESL_atomic_list_set$' ).

tff(func_def_150,type,
    'pair$h': ( 'A_TESL_atomic_a_TESL_atomic_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ) > 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ).

tff(func_def_151,type,
    'uuu$': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' ).

tff(func_def_152,type,
    'uum$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_153,type,
    'cons$f': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_list$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_list$' ).

tff(func_def_154,type,
    'sup$d': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' * 'Nat$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' ).

tff(func_def_155,type,
    'map_tailrec_rev$c': ( 'A_TESL_atomic_a_TESL_atomic_fun$' * 'A_TESL_atomic_list$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list$' ).

tff(func_def_156,type,
    'range$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ).

tff(func_def_157,type,
    'insert$g': ( 'A_TESL_atomic$' * 'A_TESL_atomic_set$' ) > 'A_TESL_atomic_set$' ).

tff(func_def_158,type,
    'uvf$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_fun$' ).

tff(func_def_159,type,
    'uuf$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_160,type,
    'map_tailrec_rev$': ( 'A_constr_a_constr_fun$' * 'A_constr_list$' * 'A_constr_list$' ) > 'A_constr_list$' ).

tff(func_def_161,type,
    'uuw$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' ).

tff(func_def_162,type,
    'fun_app$ag': ( 'A_constr_a_constr_fun$' * 'A_constr$' ) > 'A_constr$' ).

tff(func_def_163,type,
    'cons$': 'A_constr$' > 'A_constr_list_a_constr_list_fun$' ).

tff(func_def_164,type,
    'is_singleton$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_bool_fun$' ).

tff(func_def_165,type,
    'timeDelay$': ( 'Clock$' * 'Nat$' * 'A_tag_const$' * 'Clock$' ) > 'A_constr$' ).

tff(func_def_166,type,
    'gen_length$': ( 'Nat$' * 'A_constr_list$' ) > 'Nat$' ).

tff(func_def_167,type,
    'sup$e': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ).

tff(func_def_168,type,
    'nil$d': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list$' ).

tff(func_def_169,type,
    'uvi$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_170,type,
    'collect$a': 'A_constr_list_bool_fun$' > 'A_constr_list_set$' ).

tff(func_def_171,type,
    'pair$c': ( 'A_TESL_atomic_list$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).

tff(func_def_172,type,
    'uur$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_173,type,
    'sup$': ( 'A_constr_list_set$' * 'A_constr_list_set$' ) > 'A_constr_list_set$' ).

tff(func_def_174,type,
    'uva$': 'A_TESL_atomic_a_TESL_atomic_prod_set$' > 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' ).

tff(func_def_175,type,
    'lists$b': 'A_TESL_atomic_set$' > 'A_TESL_atomic_list_set$' ).

tff(func_def_176,type,
    'listrel$f': 'A_TESL_atomic_a_TESL_atomic_prod_set$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_177,type,
    'insert$i': 'A_constr$' > 'A_constr_list_a_constr_list_fun$' ).

tff(func_def_178,type,
    'image$f': ( 'A_TESL_atomic_a_TESL_atomic_list_fun$' * 'A_TESL_atomic_set$' ) > 'A_TESL_atomic_list_set$' ).

tff(func_def_179,type,
    'fsts$a': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'Nat_set$' ).

tff(func_def_180,type,
    'sup$a': ( 'A_TESL_atomic_list_set$' * 'A_TESL_atomic_list_set$' ) > 'A_TESL_atomic_list_set$' ).

tff(func_def_181,type,
    'pair$j': ( 'Clock$' * 'Nat$' ) > 'Clock_nat_prod$' ).

tff(func_def_182,type,
    'pair$t': ( 'Nat_list$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_list$' ) > 'Nat_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_list_prod$' ).

tff(func_def_183,type,
    'insert$h': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' ).

tff(func_def_184,type,
    'map_tailrec_rev_rel$a': 'A_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod_a_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' ).

tff(func_def_185,type,
    'pair$a': ( 'A_TESL_atomic$' * 'A_TESL_atomic$' ) > 'A_TESL_atomic_a_TESL_atomic_prod$' ).

tff(func_def_186,type,
    'uuv$': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' > 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ).

tff(func_def_187,type,
    'insert$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' ).

tff(func_def_188,type,
    'sup$g': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_189,type,
    'bot$e': 'Nat_set$' ).

tff(func_def_190,type,
    'fun_app$b': ( 'A_TESL_atomic_a_TESL_atomic_list_fun$' * 'A_TESL_atomic$' ) > 'A_TESL_atomic_list$' ).

tff(func_def_191,type,
    'fsts$b': 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list_set$' ).

tff(func_def_192,type,
    'uua$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_bool_fun$' ).

tff(func_def_193,type,
    tlfalse: tlbool ).

tff(func_def_194,type,
    'nat$': $int > 'Nat$' ).

tff(func_def_195,type,
    'pair$r': ( 'A_TESL_atomic$' * 'A_constr$' ) > 'A_TESL_atomic_a_constr_prod$' ).

tff(func_def_196,type,
    'image$h': ( 'A_TESL_atomic_list_a_TESL_atomic_list_fun$' * 'A_TESL_atomic_list_set$' ) > 'A_TESL_atomic_list_set$' ).

tff(func_def_197,type,
    'map_tailrec_rev$a': ( 'A_constr_a_TESL_atomic_fun$' * 'A_constr_list$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list$' ).

tff(func_def_198,type,
    'map_tailrec_rev_rel$': 'A_constr_a_constr_fun_a_constr_list_a_constr_list_prod_prod_a_constr_a_constr_fun_a_constr_list_a_constr_list_prod_prod_bool_fun_fun$' ).

tff(func_def_199,type,
    'snds$b': 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list_set$' ).

tff(func_def_200,type,
    'uug$': 'A_constr_list_a_constr_list_bool_fun_fun$' ).

tff(func_def_201,type,
    'notTicks$': ( 'Clock$' * 'Nat$' ) > 'A_constr$' ).

tff(func_def_202,type,
    'insert$b': ( 'A_constr_list$' * 'A_constr_list_set$' ) > 'A_constr_list_set$' ).

tff(func_def_203,type,
    'uuk$': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' ).

tff(func_def_204,type,
    'pair$o': ( 'A_constr_list$' * 'A_TESL_atomic_list$' ) > 'A_constr_list_a_TESL_atomic_list_prod$' ).

tff(func_def_205,type,
    'image$b': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' * 'Nat_set$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_206,type,
    'collect$d': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_207,type,
    'shuffles$': 'A_TESL_atomic_list$' > 'A_TESL_atomic_list_a_TESL_atomic_list_set_fun$' ).

tff(func_def_208,type,
    'sup$f': ( 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ).

tff(func_def_209,type,
    'image$c': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' * 'A_TESL_atomic_list_set$' ) > 'A_TESL_atomic_list_set$' ).

tff(func_def_210,type,
    'fun_app$ad': ( 'A_constr_a_constr_bool_fun_fun$' * 'A_constr$' ) > 'A_constr_bool_fun$' ).

tff(func_def_211,type,
    'cons$h': ( 'Nat$' * 'Nat_list$' ) > 'Nat_list$' ).

tff(func_def_212,type,
    'nil$': 'A_constr_list$' ).

tff(func_def_213,type,
    'fun_app$z': ( 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' * 'A_TESL_atomic_list$' ) > 'A_constr_list_bool_fun$' ).

tff(func_def_214,type,
    'pair$q': ( 'A_TESL_atomic_list$' * 'A_constr_list$' ) > 'A_TESL_atomic_list_a_constr_list_prod$' ).

tff(func_def_215,type,
    'uup$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_216,type,
    'timestamp$': ( 'Clock$' * 'Nat$' * 'A_tag_const$' ) > 'A_constr$' ).

tff(func_def_217,type,
    'pair$l': ( 'Nat$' * 'A_constr$' ) > 'Nat_a_constr_prod$' ).

tff(func_def_218,type,
    'insert$j': 'A_TESL_atomic$' > 'A_TESL_atomic_list_a_TESL_atomic_list_fun$' ).

tff(func_def_219,type,
    'set_Cons$': ( 'A_constr_set$' * 'A_constr_list_set$' ) > 'A_constr_list_set$' ).

tff(func_def_220,type,
    'lexord$': 'A_constr_a_constr_prod_set$' > 'A_constr_list_a_constr_list_prod_set$' ).

tff(func_def_221,type,
    'uuy$': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' > 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ).

tff(func_def_222,type,
    'enumerate$a': ( 'Nat$' * 'A_TESL_atomic_list$' ) > 'Nat_a_TESL_atomic_prod_list$' ).

tff(func_def_223,type,
    'k_1$': 'Clock$' ).

tff(func_def_224,type,
    'listrelp$': 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' > 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ).

tff(func_def_225,type,
    'pair$g': ( 'A_TESL_atomic_a_constr_fun$' * 'A_TESL_atomic_list_a_constr_list_prod$' ) > 'A_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod$' ).

tff(func_def_226,type,
    'aboveS$': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_227,type,
    'listrel$c': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list_prod_set$' ).

tff(func_def_228,type,
    'fun_app$ai': ( 'A_TESL_atomic_a_constr_fun$' * 'A_TESL_atomic$' ) > 'A_constr$' ).

tff(func_def_229,type,
    'pair$f': ( 'A_constr_a_constr_bool_fun_fun$' * 'A_constr_list$' ) > 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' ).

tff(func_def_230,type,
    'listrelp$d': 'A_constr_a_constr_bool_fun_fun$' > 'A_constr_list_a_constr_list_bool_fun_fun$' ).

tff(func_def_231,type,
    'phi$': 'A_TESL_atomic_list$' ).

tff(func_def_232,type,
    'shuffles$a': ( 'A_constr_list$' * 'A_constr_list$' ) > 'A_constr_list_set$' ).

tff(func_def_233,type,
    'lexord$a': 'A_TESL_atomic_a_TESL_atomic_prod_set$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).

tff(func_def_234,type,
    'listrelp$f': 'A_TESL_atomic_a_constr_bool_fun_fun$' > 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' ).

tff(func_def_235,type,
    'fun_app$aa': ( 'Nat_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' * 'Nat$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_236,type,
    'fun_app$m': ( 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list_bool_fun$' ).

tff(func_def_237,type,
    'the$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_238,type,
    'accp$d': 'A_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod_a_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' > 'A_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod_bool_fun$' ).

tff(func_def_239,type,
    'fun_app$r': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' * 'Nat$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' ).

tff(func_def_240,type,
    'uun$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).

tff(func_def_241,type,
    'fsts$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list_set$' ).

tff(func_def_242,type,
    'image$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' ).

tff(func_def_243,type,
    'lexord$b': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' > 'A_TESL_atomic_list_list_a_TESL_atomic_list_list_prod_set$' ).

tff(func_def_248,type,
    sK2: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_249,type,
    sK3: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_250,type,
    sK4: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_251,type,
    sK5: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_252,type,
    sK6: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'Nat$' ).

tff(func_def_253,type,
    sK7: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'Nat$' ).

tff(func_def_254,type,
    sK8: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list$' ).

tff(func_def_255,type,
    sK9: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).

tff(func_def_256,type,
    sK10: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list$' ).

tff(func_def_257,type,
    sK11: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'Nat$' ).

tff(func_def_258,type,
    sK12: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_259,type,
    sK13: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_260,type,
    sK14: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).

tff(func_def_261,type,
    sK15: 'A_TESL_atomic_list$' > 'A_TESL_atomic_list$' ).

tff(func_def_262,type,
    sK16: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_263,type,
    sK17: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_264,type,
    sK18: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).

tff(func_def_265,type,
    sK19: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'Nat$' ).

tff(func_def_266,type,
    sK20: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_267,type,
    sK21: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_268,type,
    sK22: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_269,type,
    sK23: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic$' ).

tff(func_def_270,type,
    sK24: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_271,type,
    sK25: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_272,type,
    sK26: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_273,type,
    sK27: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_274,type,
    sK28: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_275,type,
    sK29: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_276,type,
    sK30: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic$' ).

tff(func_def_277,type,
    sK31: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_278,type,
    sK32: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic$' ).

tff(func_def_279,type,
    sK33: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_280,type,
    sK34: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_281,type,
    sK35: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_282,type,
    sK36: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_283,type,
    sK37: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_284,type,
    sK38: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).

tff(func_def_285,type,
    sK39: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'Nat$' ).

tff(func_def_286,type,
    sK40: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_287,type,
    sK41: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_288,type,
    sK42: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_289,type,
    sK43: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_290,type,
    sK44: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_291,type,
    sK45: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ).

tff(func_def_292,type,
    sK46: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > 'A_constr_list$' ).

tff(func_def_293,type,
    sK47: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).

tff(func_def_294,type,
    sK48: 'A_TESL_atomic_list$' > 'A_TESL_atomic_list$' ).

tff(func_def_295,type,
    sK49: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ).

tff(func_def_296,type,
    sK50: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list$' ).

tff(func_def_297,type,
    sK51: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_298,type,
    sK52: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_299,type,
    sK53: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).

tff(func_def_300,type,
    sK54: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_301,type,
    sK55: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_302,type,
    sK56: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_303,type,
    sK57: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_304,type,
    sK58: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).

tff(func_def_305,type,
    sK59: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list$' ).

tff(func_def_306,type,
    sK60: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ).

tff(func_def_307,type,
    sK61: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_308,type,
    sK62: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).

tff(func_def_309,type,
    sK63: 'A_TESL_atomic_list$' > 'A_TESL_atomic_list$' ).

tff(func_def_310,type,
    sK64: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).

tff(func_def_311,type,
    sK65: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).

tff(func_def_312,type,
    sK66: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_constr_list$' ).

tff(func_def_313,type,
    sK67: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ).

tff(func_def_314,type,
    sK68: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_TESL_atomic_list$' ).

tff(func_def_315,type,
    sK69: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'Nat$' ).

tff(func_def_316,type,
    sK70: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_constr_list$' ).

tff(func_def_317,type,
    sK71: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_TESL_atomic_list$' ).

tff(func_def_318,type,
    sK72: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ).

tff(func_def_319,type,
    sK73: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).

tff(func_def_320,type,
    sK74: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'Nat$' ).

tff(func_def_321,type,
    sK75: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_constr_list$' ).

tff(pred_def_1,type,
    'less_eq$e': ( 'Nat_set$' * 'Nat_set$' ) > $o ).

tff(pred_def_2,type,
    'member$c': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > $o ).

tff(pred_def_3,type,
    'linear_order_on$': ( 'A_TESL_atomic_list_set$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > $o ).

tff(pred_def_4,type,
    'fun_app$l': ( 'A_TESL_atomic_list_bool_fun$' * 'A_TESL_atomic_list$' ) > $o ).

tff(pred_def_5,type,
    'less_eq$a': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ) > $o ).

tff(pred_def_6,type,
    'less_eq$l': ( 'A_constr_list_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list_prod_set$' * 'A_constr_list_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list_prod_set$' ) > $o ).

tff(pred_def_7,type,
    'less_eq$i': ( 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ) > $o ).

tff(pred_def_8,type,
    'fun_app$k': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_bool_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list$' ) > $o ).

tff(pred_def_9,type,
    'member$b': ( 'A_TESL_atomic_a_TESL_atomic_prod$' * 'A_TESL_atomic_a_TESL_atomic_prod_set$' ) > $o ).

tff(pred_def_10,type,
    'uniq$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > $o ).

tff(pred_def_11,type,
    'member$k': ( 'A_constr_a_constr_prod$' * 'A_constr_a_constr_prod_set$' ) > $o ).

tff(pred_def_12,type,
    'less_eq$k': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' ) > $o ).

tff(pred_def_13,type,
    'member$g': ( 'A_constr_list$' * 'A_constr_list_set$' ) > $o ).

tff(pred_def_14,type,
    'member$e': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_set$' ) > $o ).

tff(pred_def_15,type,
    'less_eq$m': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' ) > $o ).

tff(pred_def_16,type,
    'refl_on$': ( 'A_TESL_atomic_list_set$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > $o ).

tff(pred_def_17,type,
    'fun_app$v': ( 'A_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod_bool_fun$' * 'A_TESL_atomic_a_constr_fun_a_TESL_atomic_list_a_constr_list_prod_prod$' ) > $o ).

tff(pred_def_18,type,
    'less_eq$c': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_list_set$' ) > $o ).

tff(pred_def_19,type,
    'refl_on$a': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' ) > $o ).

tff(pred_def_20,type,
    'member$a': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' ) > $o ).

tff(pred_def_21,type,
    'member$h': ( 'A_TESL_atomic_list$' * 'A_TESL_atomic_list_set$' ) > $o ).

tff(pred_def_22,type,
    'member$n': ( 'A_TESL_atomic_list_a_constr_list_prod$' * 'A_TESL_atomic_list_a_constr_list_prod_set$' ) > $o ).

tff(pred_def_23,type,
    'fun_app$g': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ) > $o ).

tff(pred_def_24,type,
    'member$d': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ) > $o ).

tff(pred_def_25,type,
    'member$m': ( 'A_constr_a_TESL_atomic_prod$' * 'A_constr_a_TESL_atomic_prod_set$' ) > $o ).

tff(pred_def_26,type,
    'fun_app$t': ( 'A_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod_bool_fun$' * 'A_constr_a_TESL_atomic_fun_a_constr_list_a_TESL_atomic_list_prod_prod$' ) > $o ).

tff(pred_def_27,type,
    'member$o': ( 'A_TESL_atomic_a_constr_prod$' * 'A_TESL_atomic_a_constr_prod_set$' ) > $o ).

tff(pred_def_28,type,
    'fun_app$n': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).

tff(pred_def_29,type,
    'fun_app$w': ( 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' * 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ) > $o ).

tff(pred_def_30,type,
    'accp$': ( 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' * 'A_TESL_atomic$' ) > $o ).

tff(pred_def_31,type,
    'positive_atom$': 'A_TESL_atomic$' > $o ).

tff(pred_def_32,type,
    'total_on$a': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' ) > $o ).

tff(pred_def_33,type,
    'accp$c': ( 'A_constr_a_constr_fun_a_constr_list_a_constr_list_prod_prod_a_constr_a_constr_fun_a_constr_list_a_constr_list_prod_prod_bool_fun_fun$' * 'A_constr_a_constr_fun_a_constr_list_a_constr_list_prod_prod$' ) > $o ).

tff(pred_def_34,type,
    'fun_app$o': ( 'A_TESL_atomic_bool_fun$' * 'A_TESL_atomic$' ) > $o ).

tff(pred_def_35,type,
    'listrelp$c': ( 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' * 'A_TESL_atomic_list_list$' * 'A_TESL_atomic_list_list$' ) > $o ).

tff(pred_def_36,type,
    'less_eq$g': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ) > $o ).

tff(pred_def_37,type,
    'total_on$': ( 'A_TESL_atomic_list_set$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > $o ).

tff(pred_def_38,type,
    'fun_app$f': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set_bool_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > $o ).

tff(pred_def_39,type,
    'listrelp$b': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' * 'Nat_list$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_list$' ) > $o ).

tff(pred_def_40,type,
    'fun_app$d': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > $o ).

tff(pred_def_41,type,
    'member$j': ( 'A_constr_list_a_constr_list_prod$' * 'A_constr_list_a_constr_list_prod_set$' ) > $o ).

tff(pred_def_42,type,
    'linear_order_on$a': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_a_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_prod_set$' ) > $o ).

tff(pred_def_43,type,
    'member$q': ( 'Nat_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_list_prod$' * 'Nat_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_list_prod_set$' ) > $o ).

tff(pred_def_44,type,
    'less_eq$b': ( 'A_constr_list_set$' * 'A_constr_list_set$' ) > $o ).

tff(pred_def_45,type,
    'fun_app$x': ( 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod_bool_fun$' * 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' ) > $o ).

tff(pred_def_46,type,
    'member$f': ( 'A_TESL_atomic$' * 'A_TESL_atomic_set$' ) > $o ).

tff(pred_def_47,type,
    'fun_app$ac': ( 'A_constr_bool_fun$' * 'A_constr$' ) > $o ).

tff(pred_def_48,type,
    'member$l': ( 'A_constr_list_a_TESL_atomic_list_prod$' * 'A_constr_list_a_TESL_atomic_list_prod_set$' ) > $o ).

tff(pred_def_49,type,
    'member$i': ( 'Nat$' * 'Nat_set$' ) > $o ).

tff(pred_def_50,type,
    'less_eq$f': ( 'A_TESL_atomic_set$' * 'A_TESL_atomic_set$' ) > $o ).

tff(pred_def_51,type,
    'less_eq$h': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' ) > $o ).

tff(pred_def_52,type,
    'fun_app$i': ( 'A_constr_list_bool_fun$' * 'A_constr_list$' ) > $o ).

tff(pred_def_53,type,
    'accp$a': ( 'A_constr_list_a_constr_list_prod_a_constr_list_a_constr_list_prod_bool_fun_fun$' * 'A_constr_list_a_constr_list_prod$' ) > $o ).

tff(pred_def_54,type,
    'member$p': ( 'A_constr_list_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list_prod$' * 'A_constr_list_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list_prod_set$' ) > $o ).

tff(pred_def_55,type,
    'less_eq$j': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > $o ).

tff(pred_def_56,type,
    'member$s': ( 'A_constr$' * 'A_constr_set$' ) > $o ).

tff(pred_def_57,type,
    'fun_app$u': ( 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod_bool_fun$' * 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' ) > $o ).

tff(pred_def_58,type,
    'fun_app$h': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ) > $o ).

tff(pred_def_59,type,
    'listrelp$a': ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' * 'A_constr_list_list$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_list$' ) > $o ).

tff(pred_def_60,type,
    'less_eq$d': ( 'A_TESL_atomic_list_set$' * 'A_TESL_atomic_list_set$' ) > $o ).

tff(pred_def_61,type,
    'member$r': ( 'A_TESL_atomic_list_list_a_TESL_atomic_list_list_prod$' * 'A_TESL_atomic_list_list_a_TESL_atomic_list_list_prod_set$' ) > $o ).

tff(pred_def_64,type,
    sP0: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ) > $o ).

tff(pred_def_65,type,
    sP1: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > $o ).

tff(f38,conjecture,
    'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('notTicks$'('k_1$','n$')),'gamma$'),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$'))),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture37) ).

tff(f39,negated_conjecture,
    ~ 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('notTicks$'('k_1$','n$')),'gamma$'),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$'))),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))))),
    inference(negated_conjecture,[status(cth)],[f38]) ).

tff(f73,axiom,
    ! [X0: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$',X2: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$',X1: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$'] :
      ( 'fun_app$f'('less_eq$'('fun_app$e'('insert$'(X0),X1)),X2)
    <=> ( 'fun_app$f'('member$'(X0),X2)
        & 'fun_app$f'('less_eq$'(X1),X2) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom71) ).

tff(f84,axiom,
    ! [X0: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$'] : 'fun_app$f'('less_eq$'('bot$'),X0),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom82) ).

tff(f85,axiom,
    ! [X3: 'Clock$',X0: 'A_constr_list$',X2: 'Clock$',X1: 'Nat$',X5: 'A_TESL_atomic_list$',X4: 'A_TESL_atomic_list$'] : 'fun_app$d'('operational_semantics_elim$'('pair$b'(X0,'pair$d'(X1,'pair$c'('fun_app$c'('cons$a'('impliesNot$'(X2,X3)),X4),X5)))),'pair$b'('fun_app$a'('cons$'('ticks$'(X2,X1)),'fun_app$a'('cons$'('notTicks$'(X3,X1)),X0)),'pair$d'(X1,'pair$c'(X4,'fun_app$c'('cons$a'('impliesNot$'(X2,X3)),X5))))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom83) ).

tff(f86,axiom,
    ! [X4: 'A_TESL_atomic_list$',X0: 'A_constr_list$',X2: 'Clock$',X3: 'Clock$',X5: 'A_TESL_atomic_list$',X1: 'Nat$'] : 'fun_app$d'('operational_semantics_elim$'('pair$b'(X0,'pair$d'(X1,'pair$c'('fun_app$c'('cons$a'('impliesNot$'(X2,X3)),X4),X5)))),'pair$b'('fun_app$a'('cons$'('notTicks$'(X2,X1)),X0),'pair$d'(X1,'pair$c'(X4,'fun_app$c'('cons$a'('impliesNot$'(X2,X3)),X5))))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom84) ).

tff(f221,axiom,
    ! [X0: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$',X1: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$'] :
      ( 'fun_app$f'('member$'(X0),'collect$'(X1))
    <=> 'fun_app$d'(X1,X0) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom219) ).

tff(f251,axiom,
    ! [X0: 'A_constr_list$',X1: 'Nat$',X5: 'Nat$',X2: 'A_TESL_atomic_list$',X4: 'A_constr_list$',X3: 'A_TESL_atomic_list$',X7: 'A_TESL_atomic_list$',X6: 'A_TESL_atomic_list$'] :
      ( 'fun_app$d'('operational_semantics_elim$'('pair$b'(X0,'pair$d'(X1,'pair$c'(X2,X3)))),'pair$b'(X4,'pair$d'(X5,'pair$c'(X6,X7))))
     => 'fun_app$d'('operational_semantics_step$'('pair$b'(X0,'pair$d'(X1,'pair$c'(X2,X3)))),'pair$b'(X4,'pair$d'(X5,'pair$c'(X6,X7)))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom249) ).

tff(f260,axiom,
    ! [X2: 'Clock$',X0: 'Clock$',X1: 'Nat$',X3: 'Nat$'] :
      ( ( ( X0 = X2 )
        & ( 'of_nat$'(X1) = 'of_nat$'(X3) ) )
    <=> ( 'ticks$'(X0,X1) = 'ticks$'(X2,X3) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom258) ).

tff(f688,plain,
    ~ 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('notTicks$'('k_1$','n$')),'gamma$'),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$'))),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))))),
    inference(flattening,[],[f39]) ).

tff(f709,plain,
    ! [X1: 'Clock$',X2: 'Nat$',X0: 'Clock$',X3: 'Nat$'] :
      ( ( 'ticks$'(X1,X2) = 'ticks$'(X0,X3) )
    <=> ( ( 'of_nat$'(X3) = 'of_nat$'(X2) )
        & ( X0 = X1 ) ) ),
    inference(rectify,[],[f260]) ).

tff(f714,plain,
    ! [X7: 'A_TESL_atomic_list$',X0: 'A_constr_list$',X3: 'A_TESL_atomic_list$',X1: 'Nat$',X6: 'A_TESL_atomic_list$',X4: 'A_constr_list$',X2: 'Nat$',X5: 'A_TESL_atomic_list$'] :
      ( 'fun_app$d'('operational_semantics_elim$'('pair$b'(X0,'pair$d'(X1,'pair$c'(X3,X5)))),'pair$b'(X4,'pair$d'(X2,'pair$c'(X7,X6))))
     => 'fun_app$d'('operational_semantics_step$'('pair$b'(X0,'pair$d'(X1,'pair$c'(X3,X5)))),'pair$b'(X4,'pair$d'(X2,'pair$c'(X7,X6)))) ),
    inference(rectify,[],[f251]) ).

tff(f765,plain,
    ! [X0: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$',X1: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$',X2: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$'] :
      ( 'fun_app$f'('less_eq$'('fun_app$e'('insert$'(X0),X2)),X1)
    <=> ( 'fun_app$f'('member$'(X0),X1)
        & 'fun_app$f'('less_eq$'(X2),X1) ) ),
    inference(rectify,[],[f73]) ).

tff(f771,plain,
    ! [X0: 'A_TESL_atomic_list$',X1: 'A_constr_list$',X4: 'A_TESL_atomic_list$',X5: 'Nat$',X3: 'Clock$',X2: 'Clock$'] : 'fun_app$d'('operational_semantics_elim$'('pair$b'(X1,'pair$d'(X5,'pair$c'('fun_app$c'('cons$a'('impliesNot$'(X2,X3)),X0),X4)))),'pair$b'('fun_app$a'('cons$'('notTicks$'(X2,X5)),X1),'pair$d'(X5,'pair$c'(X0,'fun_app$c'('cons$a'('impliesNot$'(X2,X3)),X4))))),
    inference(rectify,[],[f86]) ).

tff(f772,plain,
    ! [X1: 'A_constr_list$',X0: 'Clock$',X2: 'Clock$',X3: 'Nat$',X5: 'A_TESL_atomic_list$',X4: 'A_TESL_atomic_list$'] : 'fun_app$d'('operational_semantics_elim$'('pair$b'(X1,'pair$d'(X3,'pair$c'('fun_app$c'('cons$a'('impliesNot$'(X2,X0)),X5),X4)))),'pair$b'('fun_app$a'('cons$'('ticks$'(X2,X3)),'fun_app$a'('cons$'('notTicks$'(X0,X3)),X1)),'pair$d'(X3,'pair$c'(X5,'fun_app$c'('cons$a'('impliesNot$'(X2,X0)),X4))))),
    inference(rectify,[],[f85]) ).

tff(f811,plain,
    ! [X4: 'A_constr_list$',X2: 'Nat$',X0: 'A_constr_list$',X6: 'A_TESL_atomic_list$',X3: 'A_TESL_atomic_list$',X7: 'A_TESL_atomic_list$',X5: 'A_TESL_atomic_list$',X1: 'Nat$'] :
      ( ~ 'fun_app$d'('operational_semantics_elim$'('pair$b'(X0,'pair$d'(X1,'pair$c'(X3,X5)))),'pair$b'(X4,'pair$d'(X2,'pair$c'(X7,X6))))
      | 'fun_app$d'('operational_semantics_step$'('pair$b'(X0,'pair$d'(X1,'pair$c'(X3,X5)))),'pair$b'(X4,'pair$d'(X2,'pair$c'(X7,X6)))) ),
    inference(ennf_transformation,[],[f714]) ).

tff(f943,plain,
    ! [X0: 'A_TESL_atomic_list$',X1: 'A_constr_list$',X2: 'A_TESL_atomic_list$',X3: 'Nat$',X4: 'Clock$',X5: 'Clock$'] : 'fun_app$d'('operational_semantics_elim$'('pair$b'(X1,'pair$d'(X3,'pair$c'('fun_app$c'('cons$a'('impliesNot$'(X5,X4)),X0),X2)))),'pair$b'('fun_app$a'('cons$'('notTicks$'(X5,X3)),X1),'pair$d'(X3,'pair$c'(X0,'fun_app$c'('cons$a'('impliesNot$'(X5,X4)),X2))))),
    inference(rectify,[],[f771]) ).

tff(f980,plain,
    ! [X1: 'Clock$',X2: 'Nat$',X0: 'Clock$',X3: 'Nat$'] :
      ( ( ( 'ticks$'(X1,X2) = 'ticks$'(X0,X3) )
        | ( 'of_nat$'(X3) != 'of_nat$'(X2) )
        | ( X0 != X1 ) )
      & ( ( ( 'of_nat$'(X3) = 'of_nat$'(X2) )
          & ( X0 = X1 ) )
        | ( 'ticks$'(X1,X2) != 'ticks$'(X0,X3) ) ) ),
    inference(nnf_transformation,[],[f709]) ).

tff(f981,plain,
    ! [X1: 'Clock$',X2: 'Nat$',X0: 'Clock$',X3: 'Nat$'] :
      ( ( ( 'ticks$'(X1,X2) = 'ticks$'(X0,X3) )
        | ( 'of_nat$'(X3) != 'of_nat$'(X2) )
        | ( X0 != X1 ) )
      & ( ( ( 'of_nat$'(X3) = 'of_nat$'(X2) )
          & ( X0 = X1 ) )
        | ( 'ticks$'(X1,X2) != 'ticks$'(X0,X3) ) ) ),
    inference(flattening,[],[f980]) ).

tff(f982,plain,
    ! [X0: 'Clock$',X1: 'Nat$',X2: 'Clock$',X3: 'Nat$'] :
      ( ( ( 'ticks$'(X0,X1) = 'ticks$'(X2,X3) )
        | ( 'of_nat$'(X1) != 'of_nat$'(X3) )
        | ( X0 != X2 ) )
      & ( ( ( 'of_nat$'(X1) = 'of_nat$'(X3) )
          & ( X0 = X2 ) )
        | ( 'ticks$'(X0,X1) != 'ticks$'(X2,X3) ) ) ),
    inference(rectify,[],[f981]) ).

tff(f988,plain,
    ! [X0: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$',X1: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$',X2: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$'] :
      ( ( 'fun_app$f'('less_eq$'('fun_app$e'('insert$'(X0),X2)),X1)
        | ~ 'fun_app$f'('member$'(X0),X1)
        | ~ 'fun_app$f'('less_eq$'(X2),X1) )
      & ( ( 'fun_app$f'('member$'(X0),X1)
          & 'fun_app$f'('less_eq$'(X2),X1) )
        | ~ 'fun_app$f'('less_eq$'('fun_app$e'('insert$'(X0),X2)),X1) ) ),
    inference(nnf_transformation,[],[f765]) ).

tff(f989,plain,
    ! [X0: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$',X1: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$',X2: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$'] :
      ( ( 'fun_app$f'('less_eq$'('fun_app$e'('insert$'(X0),X2)),X1)
        | ~ 'fun_app$f'('member$'(X0),X1)
        | ~ 'fun_app$f'('less_eq$'(X2),X1) )
      & ( ( 'fun_app$f'('member$'(X0),X1)
          & 'fun_app$f'('less_eq$'(X2),X1) )
        | ~ 'fun_app$f'('less_eq$'('fun_app$e'('insert$'(X0),X2)),X1) ) ),
    inference(flattening,[],[f988]) ).

tff(f994,plain,
    ! [X0: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$',X1: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$'] :
      ( ( 'fun_app$f'('member$'(X0),'collect$'(X1))
        | ~ 'fun_app$d'(X1,X0) )
      & ( 'fun_app$d'(X1,X0)
        | ~ 'fun_app$f'('member$'(X0),'collect$'(X1)) ) ),
    inference(nnf_transformation,[],[f221]) ).

tff(f1022,plain,
    ! [X0: 'A_constr_list$',X1: 'Clock$',X2: 'Clock$',X3: 'Nat$',X4: 'A_TESL_atomic_list$',X5: 'A_TESL_atomic_list$'] : 'fun_app$d'('operational_semantics_elim$'('pair$b'(X0,'pair$d'(X3,'pair$c'('fun_app$c'('cons$a'('impliesNot$'(X2,X1)),X4),X5)))),'pair$b'('fun_app$a'('cons$'('ticks$'(X2,X3)),'fun_app$a'('cons$'('notTicks$'(X1,X3)),X0)),'pair$d'(X3,'pair$c'(X4,'fun_app$c'('cons$a'('impliesNot$'(X2,X1)),X5))))),
    inference(rectify,[],[f772]) ).

tff(f1061,plain,
    ! [X0: 'A_constr_list$',X1: 'Nat$',X2: 'A_constr_list$',X3: 'A_TESL_atomic_list$',X4: 'A_TESL_atomic_list$',X5: 'A_TESL_atomic_list$',X6: 'A_TESL_atomic_list$',X7: 'Nat$'] :
      ( ~ 'fun_app$d'('operational_semantics_elim$'('pair$b'(X2,'pair$d'(X7,'pair$c'(X4,X6)))),'pair$b'(X0,'pair$d'(X1,'pair$c'(X5,X3))))
      | 'fun_app$d'('operational_semantics_step$'('pair$b'(X2,'pair$d'(X7,'pair$c'(X4,X6)))),'pair$b'(X0,'pair$d'(X1,'pair$c'(X5,X3)))) ),
    inference(rectify,[],[f811]) ).

tff(f1090,plain,
    ~ 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('notTicks$'('k_1$','n$')),'gamma$'),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$'))),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))))),
    inference(cnf_transformation,[],[f688]) ).

tff(f1128,plain,
    ! [X2: 'A_TESL_atomic_list$',X3: 'Nat$',X0: 'A_TESL_atomic_list$',X1: 'A_constr_list$',X4: 'Clock$',X5: 'Clock$'] : 'fun_app$d'('operational_semantics_elim$'('pair$b'(X1,'pair$d'(X3,'pair$c'('fun_app$c'('cons$a'('impliesNot$'(X5,X4)),X0),X2)))),'pair$b'('fun_app$a'('cons$'('notTicks$'(X5,X3)),X1),'pair$d'(X3,'pair$c'(X0,'fun_app$c'('cons$a'('impliesNot$'(X5,X4)),X2))))),
    inference(cnf_transformation,[],[f943]) ).

tff(f1176,plain,
    ! [X2: 'Clock$',X3: 'Nat$',X0: 'Clock$',X1: 'Nat$'] :
      ( ( 'ticks$'(X0,X1) = 'ticks$'(X2,X3) )
      | ( 'of_nat$'(X1) != 'of_nat$'(X3) )
      | ( X0 != X2 ) ),
    inference(cnf_transformation,[],[f982]) ).

tff(f1186,plain,
    ! [X2: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$',X0: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$',X1: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$'] :
      ( 'fun_app$f'('less_eq$'('fun_app$e'('insert$'(X0),X2)),X1)
      | ~ 'fun_app$f'('member$'(X0),X1)
      | ~ 'fun_app$f'('less_eq$'(X2),X1) ),
    inference(cnf_transformation,[],[f989]) ).

tff(f1194,plain,
    ! [X0: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$',X1: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$'] :
      ( 'fun_app$f'('member$'(X0),'collect$'(X1))
      | ~ 'fun_app$d'(X1,X0) ),
    inference(cnf_transformation,[],[f994]) ).

tff(f1230,plain,
    ! [X2: 'Clock$',X3: 'Nat$',X0: 'A_constr_list$',X1: 'Clock$',X4: 'A_TESL_atomic_list$',X5: 'A_TESL_atomic_list$'] : 'fun_app$d'('operational_semantics_elim$'('pair$b'(X0,'pair$d'(X3,'pair$c'('fun_app$c'('cons$a'('impliesNot$'(X2,X1)),X4),X5)))),'pair$b'('fun_app$a'('cons$'('ticks$'(X2,X3)),'fun_app$a'('cons$'('notTicks$'(X1,X3)),X0)),'pair$d'(X3,'pair$c'(X4,'fun_app$c'('cons$a'('impliesNot$'(X2,X1)),X5))))),
    inference(cnf_transformation,[],[f1022]) ).

tff(f1273,plain,
    ! [X2: 'A_constr_list$',X3: 'A_TESL_atomic_list$',X0: 'A_constr_list$',X1: 'Nat$',X6: 'A_TESL_atomic_list$',X7: 'Nat$',X4: 'A_TESL_atomic_list$',X5: 'A_TESL_atomic_list$'] :
      ( 'fun_app$d'('operational_semantics_step$'('pair$b'(X2,'pair$d'(X7,'pair$c'(X4,X6)))),'pair$b'(X0,'pair$d'(X1,'pair$c'(X5,X3))))
      | ~ 'fun_app$d'('operational_semantics_elim$'('pair$b'(X2,'pair$d'(X7,'pair$c'(X4,X6)))),'pair$b'(X0,'pair$d'(X1,'pair$c'(X5,X3)))) ),
    inference(cnf_transformation,[],[f1061]) ).

tff(f1292,plain,
    ! [X0: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$'] : 'fun_app$f'('less_eq$'('bot$'),X0),
    inference(cnf_transformation,[],[f84]) ).

tff(f1328,plain,
    ! [X2: 'Clock$',X3: 'Nat$',X1: 'Nat$'] :
      ( ( 'ticks$'(X2,X1) = 'ticks$'(X2,X3) )
      | ( 'of_nat$'(X1) != 'of_nat$'(X3) ) ),
    inference(equality_resolution,[],[f1176]) ).

tff(f1987,plain,
    ! [X0: 'Nat$'] :
      ( ~ 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('notTicks$'('k_1$','n$')),'gamma$'),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$',X0)),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$'))),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$'))))))
      | ( 'of_nat$'(X0) != 'of_nat$'('n$') ) ),
    inference(superposition,[],[f1090,f1328]) ).

tff(f2116,plain,
    ! [X0: 'Nat$'] :
      ( ( 'of_nat$'(X0) != 'of_nat$'('n$') )
      | ~ 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$',X0)),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$')),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$'))))))
      | ~ 'fun_app$f'('member$'('pair$b'('fun_app$a'('cons$'('notTicks$'('k_1$','n$')),'gamma$'),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))))) ),
    inference(resolution,[],[f1186,f1987]) ).

tff(f2125,definition,
    ( spl76_1
  <=> 'fun_app$f'('member$'('pair$b'('fun_app$a'('cons$'('notTicks$'('k_1$','n$')),'gamma$'),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))))) ),
    introduced(definition,[new_symbols(definition,[spl76_1])],[avatar_definition]) ).

tff(f2127,plain,
    ( ~ 'fun_app$f'('member$'('pair$b'('fun_app$a'('cons$'('notTicks$'('k_1$','n$')),'gamma$'),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$'))))))
    | spl76_1 ),
    inference(avatar_component_clause,[],[f2125]) ).

tff(f2141,definition,
    ( spl76_5
  <=> ! [X1: 'Nat$'] :
        ( ( 'of_nat$'(X1) != 'of_nat$'('n$') )
        | ~ 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$',X1)),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$')),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))))) ) ),
    introduced(definition,[new_symbols(definition,[spl76_5])],[avatar_definition]) ).

tff(f2142,plain,
    ( ! [X1: 'Nat$'] :
        ( ( 'of_nat$'(X1) != 'of_nat$'('n$') )
        | ~ 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$',X1)),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$')),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))))) )
    | ~ spl76_5 ),
    inference(avatar_component_clause,[],[f2141]) ).

tff(f2149,definition,
    ( spl76_7
  <=> 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$')),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))))) ),
    introduced(definition,[new_symbols(definition,[spl76_7])],[avatar_definition]) ).

tff(f2150,plain,
    ( 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$')),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$'))))))
    | ~ spl76_7 ),
    inference(avatar_component_clause,[],[f2149]) ).

tff(f2151,plain,
    ( ~ 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$')),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$'))))))
    | spl76_7 ),
    inference(avatar_component_clause,[],[f2149]) ).

tff(f2158,plain,
    ( ~ spl76_1
    | spl76_5 ),
    inference(avatar_split_clause,[],[f2116,f2141,f2125]) ).

tff(f2159,plain,
    ( ~ 'fun_app$d'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))),'pair$b'('fun_app$a'('cons$'('notTicks$'('k_1$','n$')),'gamma$'),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$')))))
    | spl76_1 ),
    inference(resolution,[],[f2127,f1194]) ).

tff(f2223,plain,
    ( ~ 'fun_app$f'('member$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$'))))))
    | ~ 'fun_app$f'('less_eq$'('bot$'),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$'))))))
    | spl76_7 ),
    inference(resolution,[],[f2151,f1186]) ).

tff(f2230,plain,
    ( ~ 'fun_app$f'('member$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$'))))))
    | spl76_7 ),
    inference(forward_subsumption_resolution,[],[f2223,f1292]) ).

tff(f2459,plain,
    ( ~ 'fun_app$d'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))),'pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$')))))
    | spl76_7 ),
    inference(resolution,[],[f2230,f1194]) ).

tff(f2641,plain,
    ( ! [X0: 'Nat$'] :
        ( ( 'of_nat$'(X0) != 'of_nat$'('n$') )
        | 'fun_app$f'('less_eq$'('fun_app$e'('insert$'('pair$b'('fun_app$a'('cons$'('ticks$'('k_1$',X0)),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$'))))),'bot$')),'collect$'('operational_semantics_step$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))))) )
    | ~ spl76_7 ),
    inference(superposition,[],[f2150,f1328]) ).

tff(f2645,plain,
    ( ! [X0: 'Nat$'] : ( 'of_nat$'(X0) != 'of_nat$'('n$') )
    | ~ spl76_5
    | ~ spl76_7 ),
    inference(forward_subsumption_resolution,[],[f2641,f2142]) ).

tff(f2654,plain,
    ( $false
    | ~ spl76_5
    | ~ spl76_7 ),
    inference(equality_resolution,[],[f2645]) ).

tff(f2655,plain,
    ( ~ spl76_5
    | ~ spl76_7 ),
    inference(avatar_contradiction_clause,[],[f2654]) ).

tff(f2703,plain,
    ( ~ 'fun_app$d'('operational_semantics_elim$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))),'pair$b'('fun_app$a'('cons$'('notTicks$'('k_1$','n$')),'gamma$'),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$')))))
    | spl76_1 ),
    inference(resolution,[],[f1273,f2159]) ).

tff(f2724,plain,
    ( $false
    | spl76_1 ),
    inference(forward_subsumption_resolution,[],[f2703,f1128]) ).

tff(f2725,plain,
    spl76_1,
    inference(avatar_contradiction_clause,[],[f2724]) ).

tff(f2772,plain,
    ( ~ 'fun_app$d'('operational_semantics_elim$'('pair$b'('gamma$','pair$d'('n$','pair$c'('fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'psi$'),'phi$')))),'pair$b'('fun_app$a'('cons$'('ticks$'('k_1$','n$')),'fun_app$a'('cons$'('notTicks$'('k_2$','n$')),'gamma$')),'pair$d'('n$','pair$c'('psi$','fun_app$c'('cons$a'('impliesNot$'('k_1$','k_2$')),'phi$')))))
    | spl76_7 ),
    inference(resolution,[],[f2459,f1273]) ).

tff(f2777,plain,
    ( $false
    | spl76_7 ),
    inference(forward_subsumption_resolution,[],[f2772,f1230]) ).

tff(f2778,plain,
    spl76_7,
    inference(avatar_contradiction_clause,[],[f2777]) ).

cnf(s9,plain,
    ( ~ spl76_1
    | spl76_5 ),
    inference(sat_conversion,[],[f2158]) ).

cnf(s22,plain,
    ( ~ spl76_5
    | ~ spl76_7 ),
    inference(sat_conversion,[],[f2655]) ).

cnf(s23,plain,
    spl76_1,
    inference(sat_conversion,[],[f2725]) ).

cnf(s26,plain,
    spl76_7,
    inference(sat_conversion,[],[f2778]) ).

cnf(s29,plain,
    ~ spl76_5,
    inference(rat,[],[s22,s26]) ).

cnf(s33,plain,
    $false,
    inference(rat,[],[s9,s29,s23]) ).

tff(f2779,plain,
    $false,
    inference(avatar_sat_refutation,[],[s33]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP408_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.40  % Computer : n010.cluster.edu
% 0.14/0.40  % Model    : x86_64 x86_64
% 0.14/0.40  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40  % Memory   : 8046.5625MB
% 0.14/0.40  % OS       : Linux 6.8.0-71-generic
% 0.14/0.40  % CPULimit : 300
% 0.14/0.40  % WCLimit  : 300
% 0.14/0.40  % DateTime : Sun Sep 27 12:58:01 UTC 2026
% 0.14/0.40  % CPUTime  : 
% 0.14/0.41  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.46  Running first-order theorem proving
% 0.14/0.46  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.89/1.88  % (946169)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.89/1.88  % (946180)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4012526250:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.89/1.88  % (946180)Instruction limit reached! 
% 4.89/1.88  % (946180)------------------------------
% 4.89/1.88  % (946180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.89/1.88  % (946180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.89/1.88  % (946180)CaDiCaL version: 2.1.3
% 4.89/1.88  % (946180)Termination reason: Instruction limit
% 4.89/1.88  % (946180)Termination phase: Property scanning
% 4.89/1.88  % (946180)Time elapsed: 0.003 s
% 4.89/1.88  % (946180)Peak memory usage: 86 MB
% 4.89/1.88  % (946180)Instructions burned: 9 (million)
% 4.89/1.88  % (946178)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=76677067:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.89/1.88  % (946179)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1716438761:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.89/1.89  % (946181)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2378157400:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.89/1.89  % (946176)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=976516676:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.89/1.89  % (946182)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1078967395:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.89/1.89  % (946177)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1093099605:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.89/1.89  % (946179)Instruction limit reached! 
% 4.89/1.89  % (946179)------------------------------
% 4.89/1.89  % (946179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.89/1.89  % (946179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.89/1.89  % (946179)CaDiCaL version: 2.1.3
% 4.89/1.89  % (946179)Termination reason: Instruction limit
% 4.89/1.89  % (946179)Termination phase: Property scanning
% 4.89/1.89  % (946179)Time elapsed: 0.008 s
% 4.89/1.89  % (946179)Peak memory usage: 86 MB
% 4.89/1.89  % (946179)Instructions burned: 7 (million)
% 4.89/1.89  % (946176)Instruction limit reached! 
% 4.89/1.89  % (946176)------------------------------
% 4.89/1.89  % (946176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.89/1.89  % (946176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.89/1.89  % (946176)CaDiCaL version: 2.1.3
% 4.89/1.89  % (946176)Termination reason: Instruction limit
% 4.89/1.89  % (946176)Termination phase: Property scanning
% 4.89/1.89  % (946176)Time elapsed: 0.012 s
% 4.89/1.89  % (946176)Peak memory usage: 86 MB
% 4.89/1.89  % (946176)Instructions burned: 12 (million)
% 4.89/1.89  % (946182)Instruction limit reached! 
% 4.89/1.89  % (946182)------------------------------
% 4.89/1.89  % (946182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.89/1.89  % (946182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.89/1.89  % (946182)CaDiCaL version: 2.1.3
% 4.89/1.89  % (946182)Termination reason: Instruction limit
% 4.89/1.89  % (946182)Termination phase: Preprocessing 3
% 4.89/1.89  % (946182)Time elapsed: 0.033 s
% 4.89/1.89  % (946182)Peak memory usage: 88 MB
% 4.89/1.89  % (946182)Instructions burned: 33 (million)
% 4.89/1.89  % (946181)Instruction limit reached! 
% 4.89/1.89  % (946181)------------------------------
% 4.89/1.89  % (946181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.89/1.89  % (946181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.89/1.89  % (946181)CaDiCaL version: 2.1.3
% 4.89/1.89  % (946181)Termination reason: Instruction limit
% 4.89/1.89  % (946181)Termination phase: Property scanning
% 4.89/1.89  % (946181)Time elapsed: 0.050 s
% 4.89/1.89  % (946181)Peak memory usage: 89 MB
% 4.89/1.89  % (946181)Instructions burned: 47 (million)
% 4.89/1.89  % (946185)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3686899970:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 4.89/1.89  % (946185)Instruction limit reached! 
% 4.89/1.89  % (946185)------------------------------
% 4.89/1.89  % (946185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.19  % (946185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.19  % (946185)CaDiCaL version: 2.1.3
% 7.93/2.19  % (946185)Termination reason: Instruction limit
% 7.93/2.19  % (946185)Termination phase: SInE selection
% 7.93/2.19  % (946185)Time elapsed: 0.008 s
% 7.93/2.19  % (946185)Peak memory usage: 86 MB
% 7.93/2.19  % (946185)Instructions burned: 14 (million)
% 7.93/2.19  % (946178)Instruction limit reached! 
% 7.93/2.19  % (946178)------------------------------
% 7.93/2.19  % (946178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.19  % (946178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.19  % (946178)CaDiCaL version: 2.1.3
% 7.93/2.19  % (946178)Termination reason: Instruction limit
% 7.93/2.19  % (946178)Termination phase: Saturation
% 7.93/2.19  % (946178)Time elapsed: 0.224 s
% 7.93/2.19  % (946178)Peak memory usage: 116 MB
% 7.93/2.19  % (946178)Instructions burned: 202 (million)
% 7.93/2.19  % (946177)Instruction limit reached! 
% 7.93/2.19  % (946177)------------------------------
% 7.93/2.19  % (946177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.19  % (946177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.19  % (946177)CaDiCaL version: 2.1.3
% 7.93/2.19  % (946177)Termination reason: Instruction limit
% 7.93/2.19  % (946177)Termination phase: Property scanning
% 7.93/2.19  % (946177)Time elapsed: 0.243 s
% 7.93/2.19  % (946177)Peak memory usage: 92 MB
% 7.93/2.19  % (946177)Instructions burned: 308 (million)
% 7.93/2.19  % (946194)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=481275304:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 7.93/2.19  % (946191)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=4109340757:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2996 on theBenchmark for (2996ds/29Mi)
% 7.93/2.19  % (946193)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3016230410:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 7.93/2.19  % (946192)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4175975938:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi)
% 7.93/2.19  % (946192)Instruction limit reached! 
% 7.93/2.19  % (946192)------------------------------
% 7.93/2.19  % (946192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.19  % (946192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.19  % (946192)CaDiCaL version: 2.1.3
% 7.93/2.19  % (946192)Termination reason: Instruction limit
% 7.93/2.19  % (946192)Termination phase: Preprocessing 1
% 7.93/2.19  % (946192)Time elapsed: 0.016 s
% 7.93/2.19  % (946192)Peak memory usage: 86 MB
% 7.93/2.19  % (946192)Instructions burned: 16 (million)
% 7.93/2.19  % (946193)Instruction limit reached! 
% 7.93/2.19  % (946193)------------------------------
% 7.93/2.19  % (946193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.19  % (946193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.19  % (946193)CaDiCaL version: 2.1.3
% 7.93/2.19  % (946193)Termination reason: Instruction limit
% 7.93/2.19  % (946193)Termination phase: Preprocessing 1
% 7.93/2.19  % (946193)Time elapsed: 0.024 s
% 7.93/2.19  % (946193)Peak memory usage: 86 MB
% 7.93/2.19  % (946193)Instructions burned: 24 (million)
% 7.93/2.19  % (946194)Instruction limit reached! 
% 7.93/2.19  % (946194)------------------------------
% 7.93/2.19  % (946194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.19  % (946194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.19  % (946194)CaDiCaL version: 2.1.3
% 7.93/2.19  % (946194)Termination reason: Instruction limit
% 7.93/2.19  % (946194)Termination phase: Preprocessing 2
% 7.93/2.19  % (946194)Time elapsed: 0.028 s
% 7.93/2.19  % (946194)Peak memory usage: 87 MB
% 7.93/2.19  % (946194)Instructions burned: 27 (million)
% 7.93/2.19  % (946191)Instruction limit reached! 
% 7.93/2.19  % (946191)------------------------------
% 7.93/2.19  % (946191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.19  % (946191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.19  % (946191)CaDiCaL version: 2.1.3
% 7.93/2.19  % (946191)Termination reason: Instruction limit
% 8.88/2.41  % (946191)Termination phase: Preprocessing 3
% 8.88/2.41  % (946191)Time elapsed: 0.030 s
% 8.88/2.41  % (946191)Peak memory usage: 87 MB
% 8.88/2.41  % (946191)Instructions burned: 29 (million)
% 8.88/2.41  % (946196)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2070465169:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi)
% 8.88/2.41  % (946196)Instruction limit reached! 
% 8.88/2.41  % (946196)------------------------------
% 8.88/2.41  % (946196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/2.41  % (946196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/2.41  % (946196)CaDiCaL version: 2.1.3
% 8.88/2.41  % (946196)Termination reason: Instruction limit
% 8.88/2.41  % (946196)Termination phase: Property scanning
% 8.88/2.41  % (946196)Time elapsed: 0.045 s
% 8.88/2.41  % (946196)Peak memory usage: 89 MB
% 8.88/2.41  % (946196)Instructions burned: 86 (million)
% 8.88/2.41  % (946197)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2914598567:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 8.88/2.41  % (946197)Instruction limit reached! 
% 8.88/2.41  % (946197)------------------------------
% 8.88/2.41  % (946197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/2.41  % (946197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/2.41  % (946197)CaDiCaL version: 2.1.3
% 8.88/2.41  % (946197)Termination reason: Instruction limit
% 8.88/2.41  % (946197)Termination phase: shuffling
% 8.88/2.41  % (946197)Time elapsed: 0.003 s
% 8.88/2.41  % (946197)Peak memory usage: 85 MB
% 8.88/2.41  % (946197)Instructions burned: 2 (million)
% 8.88/2.41  % (946205)lrs+10_1_thi=all:si=on:fd=off:random_seed=104180423:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 8.88/2.41  % (946198)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3469015896:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 8.88/2.41  % (946203)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4208089484:i=4:ep=RST:ins=2:rtra=on_2993 on theBenchmark for (2993ds/4Mi)
% 8.88/2.41  % (946203)Instruction limit reached! 
% 8.88/2.41  % (946203)------------------------------
% 8.88/2.41  % (946203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/2.41  % (946203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/2.41  % (946203)CaDiCaL version: 2.1.3
% 8.88/2.41  % (946203)Termination reason: Instruction limit
% 8.88/2.41  % (946203)Termination phase: Property scanning
% 8.88/2.41  % (946203)Time elapsed: 0.006 s
% 8.88/2.41  % (946203)Peak memory usage: 86 MB
% 8.88/2.41  % (946203)Instructions burned: 5 (million)
% 8.88/2.41  % (946205)Instruction limit reached! 
% 8.88/2.41  % (946205)------------------------------
% 8.88/2.41  % (946205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/2.41  % (946205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/2.41  % (946205)CaDiCaL version: 2.1.3
% 8.88/2.41  % (946205)Termination reason: Instruction limit
% 8.88/2.41  % (946205)Termination phase: Preprocessing 3
% 8.88/2.41  % (946205)Time elapsed: 0.034 s
% 8.88/2.41  % (946205)Peak memory usage: 88 MB
% 8.88/2.41  % (946205)Instructions burned: 54 (million)
% 8.88/2.41  % (946206)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=2348035285:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 8.88/2.41  % (946204)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2891768333:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi)
% 8.88/2.41  % (946206)Instruction limit reached! 
% 8.88/2.41  % (946206)------------------------------
% 8.88/2.41  % (946206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/2.41  % (946206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/2.41  % (946206)CaDiCaL version: 2.1.3
% 8.88/2.41  % (946206)Termination reason: Instruction limit
% 8.88/2.41  % (946206)Termination phase: Property scanning
% 8.88/2.41  % (946206)Time elapsed: 0.008 s
% 8.88/2.41  % (946206)Peak memory usage: 85 MB
% 8.88/2.41  % (946206)Instructions burned: 8 (million)
% 8.88/2.41  % (946208)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=444993701:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 11.06/2.75  % (946208)Instruction limit reached! 
% 11.06/2.75  % (946208)------------------------------
% 11.06/2.75  % (946208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.06/2.75  % (946208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.06/2.75  % (946208)CaDiCaL version: 2.1.3
% 11.06/2.75  % (946208)Termination reason: Instruction limit
% 11.06/2.75  % (946208)Termination phase: Property scanning
% 11.06/2.75  % (946208)Time elapsed: 0.003 s
% 11.06/2.75  % (946208)Peak memory usage: 86 MB
% 11.06/2.75  % (946208)Instructions burned: 3 (million)
% 11.06/2.75  % (946204)Instruction limit reached! 
% 11.06/2.75  % (946204)------------------------------
% 11.06/2.75  % (946204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.06/2.75  % (946204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.06/2.75  % (946204)CaDiCaL version: 2.1.3
% 11.06/2.75  % (946204)Termination reason: Instruction limit
% 11.06/2.75  % (946204)Termination phase: Property scanning
% 11.06/2.75  % (946204)Time elapsed: 0.067 s
% 11.06/2.75  % (946204)Peak memory usage: 89 MB
% 11.06/2.75  % (946204)Instructions burned: 66 (million)
% 11.06/2.75  % (946210)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1180513428:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 11.06/2.75  % (946210)Instruction limit reached! 
% 11.06/2.75  % (946210)------------------------------
% 11.06/2.75  % (946210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.06/2.75  % (946210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.06/2.75  % (946210)CaDiCaL version: 2.1.3
% 11.06/2.75  % (946210)Termination reason: Instruction limit
% 11.06/2.75  % (946210)Termination phase: shuffling
% 11.06/2.75  % (946210)Time elapsed: 0.004 s
% 11.06/2.75  % (946210)Peak memory usage: 86 MB
% 11.06/2.75  % (946210)Instructions burned: 3 (million)
% 11.06/2.75  % (946198)Instruction limit reached! 
% 11.06/2.75  % (946198)------------------------------
% 11.06/2.75  % (946198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.06/2.75  % (946198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.06/2.75  % (946198)CaDiCaL version: 2.1.3
% 11.06/2.75  % (946198)Termination reason: Instruction limit
% 11.06/2.75  % (946198)Termination phase: Saturation
% 11.06/2.75  % (946198)Time elapsed: 0.200 s
% 11.06/2.75  % (946198)Peak memory usage: 92 MB
% 11.06/2.75  % (946198)Instructions burned: 181 (million)
% 11.06/2.75  % (946215)dis+10_1_si=on:random_seed=3202276147:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 11.06/2.75  % (946215)Instruction limit reached! 
% 11.06/2.75  % (946215)------------------------------
% 11.06/2.75  % (946215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.06/2.75  % (946215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.06/2.75  % (946215)CaDiCaL version: 2.1.3
% 11.06/2.75  % (946215)Termination reason: Instruction limit
% 11.06/2.75  % (946215)Termination phase: Including theory axioms
% 11.06/2.75  % (946215)Time elapsed: 0.006 s
% 11.06/2.75  % (946215)Peak memory usage: 86 MB
% 11.06/2.75  % (946215)Instructions burned: 11 (million)
% 11.06/2.75  % (946214)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1258501865:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi)
% 11.06/2.75  % (946219)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2541773911:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 11.06/2.75  % (946220)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2636359965:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2991 on theBenchmark for (2991ds/35Mi)
% 11.06/2.75  % (946219)Instruction limit reached! 
% 11.06/2.75  % (946219)------------------------------
% 11.06/2.75  % (946219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.06/2.75  % (946219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.06/2.75  % (946219)CaDiCaL version: 2.1.3
% 11.06/2.75  % (946219)Termination reason: Instruction limit
% 11.06/2.75  % (946219)Termination phase: shuffling
% 11.06/2.75  % (946219)Time elapsed: 0.025 s
% 11.06/2.75  % (946219)Peak memory usage: 87 MB
% 11.06/2.75  % (946219)Instructions burned: 26 (million)
% 11.06/2.75  % (946220)Instruction limit reached! 
% 11.06/2.75  % (946220)------------------------------
% 11.06/2.75  % (946220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/3.25  % (946220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/3.25  % (946220)CaDiCaL version: 2.1.3
% 15.25/3.25  % (946220)Termination reason: Instruction limit
% 15.25/3.25  % (946220)Termination phase: Preprocessing 3
% 15.25/3.25  % (946220)Time elapsed: 0.036 s
% 15.25/3.25  % (946220)Peak memory usage: 88 MB
% 15.25/3.25  % (946220)Instructions burned: 35 (million)
% 15.25/3.25  % (946221)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1216061588:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 15.25/3.25  % (946221)Instruction limit reached! 
% 15.25/3.25  % (946221)------------------------------
% 15.25/3.25  % (946221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/3.25  % (946221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/3.25  % (946221)CaDiCaL version: 2.1.3
% 15.25/3.25  % (946221)Termination reason: Instruction limit
% 15.25/3.25  % (946221)Termination phase: shuffling
% 15.25/3.25  % (946221)Time elapsed: 0.004 s
% 15.25/3.25  % (946221)Peak memory usage: 86 MB
% 15.25/3.25  % (946221)Instructions burned: 2 (million)
% 15.25/3.25  % (946226)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1975391877:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 15.25/3.25  % (946226)Instruction limit reached! 
% 15.25/3.25  % (946226)------------------------------
% 15.25/3.25  % (946226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/3.25  % (946226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/3.25  % (946226)CaDiCaL version: 2.1.3
% 15.25/3.25  % (946226)Termination reason: Instruction limit
% 15.25/3.25  % (946226)Termination phase: Property scanning
% 15.25/3.25  % (946226)Time elapsed: 0.013 s
% 15.25/3.25  % (946226)Peak memory usage: 85 MB
% 15.25/3.25  % (946226)Instructions burned: 14 (million)
% 15.25/3.25  % (946223)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3086926574:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi)
% 15.25/3.25  % (946223)Instruction limit reached! 
% 15.25/3.25  % (946223)------------------------------
% 15.25/3.25  % (946223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/3.25  % (946223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/3.25  % (946223)CaDiCaL version: 2.1.3
% 15.25/3.25  % (946223)Termination reason: Instruction limit
% 15.25/3.25  % (946223)Termination phase: Property scanning
% 15.25/3.25  % (946223)Time elapsed: 0.009 s
% 15.25/3.25  % (946223)Peak memory usage: 86 MB
% 15.25/3.25  % (946223)Instructions burned: 8 (million)
% 15.25/3.25  % (946214)Instruction limit reached! 
% 15.25/3.25  % (946214)------------------------------
% 15.25/3.25  % (946214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/3.25  % (946214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/3.25  % (946214)CaDiCaL version: 2.1.3
% 15.25/3.25  % (946214)Termination reason: Instruction limit
% 15.25/3.25  % (946214)Termination phase: Saturation
% 15.25/3.25  % (946214)Time elapsed: 0.150 s
% 15.25/3.25  % (946214)Peak memory usage: 115 MB
% 15.25/3.25  % (946214)Instructions burned: 127 (million)
% 15.25/3.25  % (946224)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1214834420:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi)
% 15.25/3.25  % (946231)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3852381901:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 15.25/3.25  % (946231)Instruction limit reached! 
% 15.25/3.25  % (946231)------------------------------
% 15.25/3.25  % (946231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/3.25  % (946231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/3.25  % (946231)CaDiCaL version: 2.1.3
% 15.25/3.25  % (946231)Termination reason: Instruction limit
% 15.25/3.25  % (946231)Termination phase: Property scanning
% 15.25/3.25  % (946231)Time elapsed: 0.007 s
% 15.25/3.25  % (946231)Peak memory usage: 86 MB
% 15.25/3.25  % (946231)Instructions burned: 11 (million)
% 15.25/3.25  % (946230)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3277052083:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 15.25/3.25  % (946234)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=236502915:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi)
% 16.83/3.51  % (946234)Instruction limit reached! 
% 16.83/3.51  % (946234)------------------------------
% 16.83/3.51  % (946234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.83/3.51  % (946234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.83/3.51  % (946234)CaDiCaL version: 2.1.3
% 16.83/3.51  % (946234)Termination reason: Instruction limit
% 16.83/3.51  % (946234)Termination phase: Equality resolution with deletion
% 16.83/3.51  % (946234)Time elapsed: 0.040 s
% 16.83/3.51  % (946234)Peak memory usage: 90 MB
% 16.83/3.51  % (946234)Instructions burned: 73 (million)
% 16.83/3.51  % (946236)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=460588721:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 16.83/3.51  % (946237)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=371225065:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 16.83/3.51  % (946238)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1916386356:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi)
% 16.83/3.51  % (946236)Instruction limit reached! 
% 16.83/3.51  % (946236)------------------------------
% 16.83/3.51  % (946236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.83/3.51  % (946236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.83/3.51  % (946236)CaDiCaL version: 2.1.3
% 16.83/3.51  % (946236)Termination reason: Instruction limit
% 16.83/3.51  % (946236)Termination phase: Property scanning
% 16.83/3.51  % (946236)Time elapsed: 0.073 s
% 16.83/3.51  % (946236)Peak memory usage: 90 MB
% 16.83/3.51  % (946236)Instructions burned: 75 (million)
% 16.83/3.51  % (946238)Instruction limit reached! 
% 16.83/3.51  % (946238)------------------------------
% 16.83/3.51  % (946238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.83/3.51  % (946238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.83/3.51  % (946238)CaDiCaL version: 2.1.3
% 16.83/3.51  % (946238)Termination reason: Instruction limit
% 16.83/3.51  % (946238)Termination phase: Property scanning
% 16.83/3.51  % (946238)Time elapsed: 0.062 s
% 16.83/3.51  % (946238)Peak memory usage: 92 MB
% 16.83/3.51  % (946238)Instructions burned: 131 (million)
% 16.83/3.51  % (946230)Instruction limit reached! 
% 16.83/3.51  % (946230)------------------------------
% 16.83/3.51  % (946230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.83/3.51  % (946230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.83/3.51  % (946230)CaDiCaL version: 2.1.3
% 16.83/3.51  % (946230)Termination reason: Instruction limit
% 16.83/3.51  % (946230)Termination phase: Saturation
% 16.83/3.51  % (946230)Time elapsed: 0.221 s
% 16.83/3.51  % (946230)Peak memory usage: 118 MB
% 16.83/3.51  % (946230)Instructions burned: 227 (million)
% 16.83/3.51  % (946241)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2210779383:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 16.83/3.51  % (946244)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1740683901:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi)
% 16.83/3.51  % (946244)Instruction limit reached! 
% 16.83/3.51  % (946244)------------------------------
% 16.83/3.51  % (946244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.83/3.51  % (946244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.83/3.51  % (946244)CaDiCaL version: 2.1.3
% 16.83/3.51  % (946244)Termination reason: Instruction limit
% 16.83/3.51  % (946244)Termination phase: Preprocessing 1
% 16.83/3.51  % (946244)Time elapsed: 0.020 s
% 16.83/3.51  % (946244)Peak memory usage: 86 MB
% 16.83/3.51  % (946244)Instructions burned: 41 (million)
% 16.83/3.51  % (946224)Instruction limit reached! 
% 16.83/3.51  % (946224)------------------------------
% 16.83/3.51  % (946224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.83/3.51  % (946224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.83/3.51  % (946224)CaDiCaL version: 2.1.3
% 16.83/3.51  % (946224)Termination reason: Instruction limit
% 16.83/3.51  % (946224)Termination phase: Saturation
% 16.83/3.51  % (946224)Time elapsed: 0.361 s
% 16.83/3.51  % (946224)Peak memory usage: 95 MB
% 16.83/3.51  % (946224)Instructions burned: 370 (million)
% 16.83/3.51  % (946237)Instruction limit reached! 
% 21.58/4.13  % (946237)------------------------------
% 21.58/4.13  % (946237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.58/4.13  % (946237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.58/4.13  % (946237)CaDiCaL version: 2.1.3
% 21.58/4.13  % (946237)Termination reason: Instruction limit
% 21.58/4.13  % (946237)Termination phase: Property scanning
% 21.58/4.13  % (946237)Time elapsed: 0.235 s
% 21.58/4.13  % (946237)Peak memory usage: 92 MB
% 21.58/4.13  % (946237)Instructions burned: 294 (million)
% 21.58/4.13  % (946241)Instruction limit reached! 
% 21.58/4.13  % (946241)------------------------------
% 21.58/4.13  % (946241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.58/4.13  % (946241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.58/4.13  % (946241)CaDiCaL version: 2.1.3
% 21.58/4.13  % (946241)Termination reason: Instruction limit
% 21.58/4.13  % (946241)Termination phase: Saturation
% 21.58/4.13  % (946241)Time elapsed: 0.180 s
% 21.58/4.13  % (946241)Peak memory usage: 132 MB
% 21.58/4.13  % (946241)Instructions burned: 131 (million)
% 21.58/4.13  % (946249)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3978165223:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 21.58/4.13  % (946248)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=902429701:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 21.58/4.13  % (946253)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=2478011769:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi)
% 21.58/4.13  % (946254)dis+10_1_si=on:random_seed=2429583484:s2a=on:i=1000:rtra=on:gtg=exists_all_2983 on theBenchmark for (2983ds/1000Mi)
% 21.58/4.13  % (946252)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2139394224:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi)
% 21.58/4.13  % (946253)Instruction limit reached! 
% 21.58/4.13  % (946253)------------------------------
% 21.58/4.13  % (946253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.58/4.13  % (946253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.58/4.13  % (946253)CaDiCaL version: 2.1.3
% 21.58/4.13  % (946253)Termination reason: Instruction limit
% 21.58/4.13  % (946253)Termination phase: Saturation
% 21.58/4.13  % (946253)Time elapsed: 0.151 s
% 21.58/4.13  % (946253)Peak memory usage: 118 MB
% 21.58/4.13  % (946253)Instructions burned: 260 (million)
% 21.58/4.13  % (946252)Instruction limit reached! 
% 21.58/4.13  % (946252)------------------------------
% 21.58/4.13  % (946252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.58/4.13  % (946252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.58/4.13  % (946252)CaDiCaL version: 2.1.3
% 21.58/4.13  % (946252)Termination reason: Instruction limit
% 21.58/4.13  % (946252)Termination phase: Saturation
% 21.58/4.13  % (946252)Time elapsed: 0.151 s
% 21.58/4.13  % (946252)Peak memory usage: 116 MB
% 21.58/4.13  % (946252)Instructions burned: 131 (million)
% 21.58/4.13  % (946255)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1282853601:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi)
% 21.58/4.13  % (946257)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=594845334:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi)
% 21.58/4.13  % (946248)Instruction limit reached! 
% 21.58/4.13  % (946248)------------------------------
% 21.58/4.13  % (946248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.58/4.13  % (946248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.58/4.13  % (946248)CaDiCaL version: 2.1.3
% 21.58/4.13  % (946248)Termination reason: Instruction limit
% 21.58/4.13  % (946248)Termination phase: Saturation
% 21.58/4.13  % (946248)Time elapsed: 0.273 s
% 21.58/4.13  % (946248)Peak memory usage: 94 MB
% 21.58/4.13  % (946248)Instructions burned: 307 (million)
% 21.58/4.13  % (946263)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2462796384:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi)
% 21.58/4.13  % (946257)Instruction limit reached! 
% 21.58/4.13  % (946257)------------------------------
% 21.58/4.13  % (946257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.95/4.70  % (946257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.95/4.70  % (946257)CaDiCaL version: 2.1.3
% 22.95/4.70  % (946257)Termination reason: Instruction limit
% 22.95/4.70  % (946257)Termination phase: Saturation
% 22.95/4.70  % (946257)Time elapsed: 0.137 s
% 22.95/4.70  % (946257)Peak memory usage: 92 MB
% 22.95/4.70  % (946257)Instructions burned: 142 (million)
% 22.95/4.70  % (946262)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3038812111:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi)
% 22.95/4.70  % (946255)Instruction limit reached! 
% 22.95/4.70  % (946255)------------------------------
% 22.95/4.70  % (946255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.95/4.70  % (946255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.95/4.70  % (946255)CaDiCaL version: 2.1.3
% 22.95/4.70  % (946255)Termination reason: Instruction limit
% 22.95/4.70  % (946255)Termination phase: Saturation
% 22.95/4.70  % (946255)Time elapsed: 0.228 s
% 22.95/4.70  % (946255)Peak memory usage: 98 MB
% 22.95/4.70  % (946255)Instructions burned: 384 (million)
% 22.95/4.70  % (946262)Instruction limit reached! 
% 22.95/4.70  % (946262)------------------------------
% 22.95/4.70  % (946262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.95/4.70  % (946262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.95/4.70  % (946262)CaDiCaL version: 2.1.3
% 22.95/4.70  % (946262)Termination reason: Instruction limit
% 22.95/4.70  % (946262)Termination phase: Equality resolution with deletion
% 22.95/4.70  % (946262)Time elapsed: 0.065 s
% 22.95/4.70  % (946262)Peak memory usage: 89 MB
% 22.95/4.70  % (946262)Instructions burned: 66 (million)
% 22.95/4.70  % (946263)Instruction limit reached! 
% 22.95/4.70  % (946263)------------------------------
% 22.95/4.70  % (946263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.95/4.70  % (946263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.95/4.70  % (946263)CaDiCaL version: 2.1.3
% 22.95/4.70  % (946263)Termination reason: Instruction limit
% 22.95/4.70  % (946263)Termination phase: Saturation
% 22.95/4.70  % (946263)Time elapsed: 0.086 s
% 22.95/4.70  % (946263)Peak memory usage: 91 MB
% 22.95/4.70  % (946263)Instructions burned: 122 (million)
% 22.95/4.70  % (946266)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=1315226158:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi)
% 22.95/4.70  % (946268)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=4038931531:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi)
% 22.95/4.70  % (946268)Instruction limit reached! 
% 22.95/4.70  % (946268)------------------------------
% 22.95/4.70  % (946268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.95/4.70  % (946268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.95/4.70  % (946268)CaDiCaL version: 2.1.3
% 22.95/4.70  % (946268)Termination reason: Instruction limit
% 22.95/4.70  % (946268)Termination phase: Preprocessing 3
% 22.95/4.70  % (946268)Time elapsed: 0.022 s
% 22.95/4.70  % (946268)Peak memory usage: 89 MB
% 22.95/4.70  % (946268)Instructions burned: 40 (million)
% 22.95/4.70  % (946266)Instruction limit reached! 
% 22.95/4.70  % (946266)------------------------------
% 22.95/4.70  % (946266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.95/4.70  % (946266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.95/4.70  % (946266)CaDiCaL version: 2.1.3
% 22.95/4.70  % (946266)Termination reason: Instruction limit
% 22.95/4.70  % (946266)Termination phase: Saturation
% 22.95/4.70  % (946266)Time elapsed: 0.125 s
% 22.95/4.70  % (946266)Peak memory usage: 93 MB
% 22.95/4.70  % (946266)Instructions burned: 128 (million)
% 22.95/4.70  % (946271)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2308239005:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi)
% 22.95/4.70  % (946249)Instruction limit reached! 
% 22.95/4.70  % (946249)------------------------------
% 22.95/4.70  % (946249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.95/4.70  % (946249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.95/4.70  % (946249)CaDiCaL version: 2.1.3
% 22.95/4.70  % (946249)Termination reason: Instruction limit
% 22.95/4.70  % (946249)Termination phase: Saturation
% 22.95/4.70  % (946249)Time elapsed: 0.676 s
% 23.04/4.77  % (946249)Peak memory usage: 140 MB
% 23.04/4.77  % (946249)Instructions burned: 598 (million)
% 23.04/4.77  % (946270)dis+1010_1_to=kbo:si=on:random_seed=240825805:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi)
% 23.04/4.77  % (946272)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1775674201:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi)
% 23.04/4.77  % (946254)Instruction limit reached! 
% 23.04/4.77  % (946254)------------------------------
% 23.04/4.77  % (946254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946254)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946254)Termination reason: Instruction limit
% 23.04/4.77  % (946254)Termination phase: Saturation
% 23.04/4.77  % (946254)Time elapsed: 0.790 s
% 23.04/4.77  % (946254)Peak memory usage: 97 MB
% 23.04/4.77  % (946254)Instructions burned: 1000 (million)
% 23.04/4.77  % (946270)Instruction limit reached! 
% 23.04/4.77  % (946270)------------------------------
% 23.04/4.77  % (946270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946270)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946270)Termination reason: Instruction limit
% 23.04/4.77  % (946270)Termination phase: Saturation
% 23.04/4.77  % (946270)Time elapsed: 0.166 s
% 23.04/4.77  % (946270)Peak memory usage: 92 MB
% 23.04/4.77  % (946270)Instructions burned: 175 (million)
% 23.04/4.77  % (946275)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3474711374:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi)
% 23.04/4.77  % (946276)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=189858056:i=349:rtra=on_2975 on theBenchmark for (2975ds/349Mi)
% 23.04/4.77  % (946275)Instruction limit reached! 
% 23.04/4.77  % (946275)------------------------------
% 23.04/4.77  % (946275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946275)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946275)Termination reason: Instruction limit
% 23.04/4.77  % (946275)Termination phase: Property scanning
% 23.04/4.77  % (946275)Time elapsed: 0.094 s
% 23.04/4.77  % (946275)Peak memory usage: 92 MB
% 23.04/4.77  % (946275)Instructions burned: 218 (million)
% 23.04/4.77  % (946279)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3345955647:st=2:i=295:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/295Mi)
% 23.04/4.77  % (946271)Instruction limit reached! 
% 23.04/4.77  % (946271)------------------------------
% 23.04/4.77  % (946271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946271)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946271)Termination reason: Instruction limit
% 23.04/4.77  % (946271)Termination phase: Saturation
% 23.04/4.77  % (946271)Time elapsed: 0.331 s
% 23.04/4.77  % (946271)Peak memory usage: 117 MB
% 23.04/4.77  % (946271)Instructions burned: 329 (million)
% 23.04/4.77  % (946281)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2341027179:i=328:kws=inv_frequency:nm=20:rtra=on_2973 on theBenchmark for (2973ds/328Mi)
% 23.04/4.77  % (946282)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3629445264:i=281:gtgl=2:rtra=on:gtg=all_2973 on theBenchmark for (2973ds/281Mi)
% 23.04/4.77  % (946285)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=661114774:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/484Mi)
% 23.04/4.77  % (946279)Instruction limit reached! 
% 23.04/4.77  % (946279)------------------------------
% 23.04/4.77  % (946279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946279)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946279)Termination reason: Instruction limit
% 23.04/4.77  % (946279)Termination phase: Saturation
% 23.04/4.77  % (946279)Time elapsed: 0.277 s
% 23.04/4.77  % (946279)Peak memory usage: 91 MB
% 23.04/4.77  % (946279)Instructions burned: 295 (million)
% 23.04/4.77  % (946276)Instruction limit reached! 
% 23.04/4.77  % (946276)------------------------------
% 23.04/4.77  % (946276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946276)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946276)Termination reason: Instruction limit
% 23.04/4.77  % (946276)Termination phase: Saturation
% 23.04/4.77  % (946276)Time elapsed: 0.391 s
% 23.04/4.77  % (946276)Peak memory usage: 121 MB
% 23.04/4.77  % (946276)Instructions burned: 349 (million)
% 23.04/4.77  % (946272)Instruction limit reached! 
% 23.04/4.77  % (946272)------------------------------
% 23.04/4.77  % (946272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946272)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946272)Termination reason: Instruction limit
% 23.04/4.77  % (946272)Termination phase: Saturation
% 23.04/4.77  % (946272)Time elapsed: 0.525 s
% 23.04/4.77  % (946272)Peak memory usage: 139 MB
% 23.04/4.77  % (946272)Instructions burned: 484 (million)
% 23.04/4.77  % (946287)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2369466209:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2971 on theBenchmark for (2971ds/321Mi)
% 23.04/4.77  % (946281)Instruction limit reached! 
% 23.04/4.77  % (946281)------------------------------
% 23.04/4.77  % (946281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946281)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946281)Termination reason: Instruction limit
% 23.04/4.77  % (946281)Termination phase: Saturation
% 23.04/4.77  % (946281)Time elapsed: 0.306 s
% 23.04/4.77  % (946281)Peak memory usage: 120 MB
% 23.04/4.77  % (946281)Instructions burned: 328 (million)
% 23.04/4.77  % (946285)Instruction limit reached! 
% 23.04/4.77  % (946285)------------------------------
% 23.04/4.77  % (946285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946285)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946285)Termination reason: Instruction limit
% 23.04/4.77  % (946285)Termination phase: Saturation
% 23.04/4.77  % (946285)Time elapsed: 0.195 s
% 23.04/4.77  % (946285)Peak memory usage: 91 MB
% 23.04/4.77  % (946285)Instructions burned: 486 (million)
% 23.04/4.77  % (946282)Instruction limit reached! 
% 23.04/4.77  % (946282)------------------------------
% 23.04/4.77  % (946282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946282)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946282)Termination reason: Instruction limit
% 23.04/4.77  % (946282)Termination phase: Saturation
% 23.04/4.77  % (946282)Time elapsed: 0.284 s
% 23.04/4.77  % (946282)Peak memory usage: 121 MB
% 23.04/4.77  % (946282)Instructions burned: 281 (million)
% 23.04/4.77  % (946292)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3230851402:i=471:thf=on:kws=precedence:rtra=on_2968 on theBenchmark for (2968ds/471Mi)
% 23.04/4.77  % (946291)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3100602136:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi)
% 23.04/4.77  % (946287)First to succeed.
% 23.04/4.77  % (946287)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-946169"
% 23.04/4.77  % (946294)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=3717003672:avsq=on:i=276:avsqr=1,2:rtra=on_2968 on theBenchmark for (2968ds/276Mi)
% 23.04/4.77  % (946295)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=875261463:i=375:kws=inv_arity_squared:rtra=on_2968 on theBenchmark for (2968ds/375Mi)
% 23.04/4.77  % (946297)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3369147085:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2967 on theBenchmark for (2967ds/513Mi)
% 23.04/4.77  % (946296)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=507210615:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/387Mi)
% 23.04/4.77  % (946291)Instruction limit reached! 
% 23.04/4.77  % (946291)------------------------------
% 23.04/4.77  % (946291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946291)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946291)Termination reason: Instruction limit
% 23.04/4.77  % (946291)Termination phase: Saturation
% 23.04/4.77  % (946291)Time elapsed: 0.372 s
% 23.04/4.77  % (946291)Peak memory usage: 118 MB
% 23.04/4.77  % (946291)Instructions burned: 418 (million)
% 23.04/4.77  % (946292)Instruction limit reached! 
% 23.04/4.77  % (946292)------------------------------
% 23.04/4.77  % (946292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946292)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946292)Termination reason: Instruction limit
% 23.04/4.77  % (946292)Termination phase: Saturation
% 23.04/4.77  % (946292)Time elapsed: 0.422 s
% 23.04/4.77  % (946292)Peak memory usage: 121 MB
% 23.04/4.77  % (946292)Instructions burned: 471 (million)
% 23.04/4.77  % (946294)Instruction limit reached! 
% 23.04/4.77  % (946294)------------------------------
% 23.04/4.77  % (946294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946294)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946294)Termination reason: Instruction limit
% 23.04/4.77  % (946294)Termination phase: Saturation
% 23.04/4.77  % (946294)Time elapsed: 0.321 s
% 23.04/4.77  % (946294)Peak memory usage: 138 MB
% 23.04/4.77  % (946294)Instructions burned: 276 (million)
% 23.04/4.77  % (946297)Instruction limit reached! 
% 23.04/4.77  % (946297)------------------------------
% 23.04/4.77  % (946297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.77  % (946297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.77  % (946297)CaDiCaL version: 2.1.3
% 23.04/4.77  % (946297)Termination reason: Instruction limit
% 23.04/4.77  % (946297)Termination phase: Saturation
% 23.04/4.77  % (946297)Time elapsed: 0.274 s
% 23.04/4.77  % (946297)Peak memory usage: 96 MB
% 23.04/4.77  % (946297)Instructions burned: 514 (million)
% 23.04/4.77  % (946287)Refutation found. Thanks to Tanya!
% 23.04/4.77  % SZS status Theorem for theBenchmark
% 23.04/4.77  % SZS output start Proof for theBenchmark
% See solution above
% 26.91/5.10  % (946287)------------------------------
% 26.91/5.10  % (946287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.91/5.10  % (946287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.91/5.10  % (946287)CaDiCaL version: 2.1.3
% 26.91/5.10  % (946287)Termination reason: Refutation
% 26.91/5.10  % (946287)Time elapsed: 0.209 s
% 26.91/5.10  % (946287)Peak memory usage: 117 MB
% 26.91/5.10  % (946287)Instructions burned: 174 (million)
% 26.91/5.10  % (946287)------------------------------
% 26.91/5.10  % (946287)------------------------------
% 26.91/5.10  % (946169)Success in time 3.769 s
% 26.91/5.10  % Vampire exiting
%------------------------------------------------------------------------------