%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP412_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:50 AM UTC 2026
% Result : Theorem 25.62s 4.24s
% Output : Refutation 26.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 18
% Syntax : Number of formulae : 78 ( 31 unt; 0 typ; 9 def)
% Number of atoms : 147 ( 64 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 116 ( 47 ~; 46 |; 10 &)
% ( 11 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number arithmetic : 58 ( 0 atm; 29 fun; 29 num; 0 var)
% Number of types : 72 ( 70 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 42 ( 40 usr; 10 prp; 0-3 aty)
% Number of functors : 535 ( 533 usr; 50 con; 0-3 aty)
% Number of variables : 112 ( 111 !; 1 ?; 112 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'A_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_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,
'Int_bool_fun$': $tType ).
tff(type_def_8,type,
'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_fun$': $tType ).
tff(type_def_9,type,
'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$': $tType ).
tff(type_def_10,type,
'A_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_fun_fun$': $tType ).
tff(type_def_11,type,
'Nat_a_run_set_fun$': $tType ).
tff(type_def_12,type,
'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$': $tType ).
tff(type_def_13,type,
'Nat_nat_bool_fun_fun$': $tType ).
tff(type_def_14,type,
'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$': $tType ).
tff(type_def_15,type,
'A_run_set_int_fun$': $tType ).
tff(type_def_16,type,
'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_fun$': $tType ).
tff(type_def_17,type,
'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$': $tType ).
tff(type_def_18,type,
'Clock$': $tType ).
tff(type_def_19,type,
'A_TESL_atomic_list_list$': $tType ).
tff(type_def_20,type,
'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$': $tType ).
tff(type_def_21,type,
'Nat_nat_nat_fun_fun$': $tType ).
tff(type_def_22,type,
'Nat_nat_prod_bool_fun$': $tType ).
tff(type_def_23,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_bool_fun_fun$': $tType ).
tff(type_def_24,type,
'A_constr_list$': $tType ).
tff(type_def_25,type,
'A_TESL_atomic_list_a_constr_list_bool_fun_fun$': $tType ).
tff(type_def_26,type,
'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$': $tType ).
tff(type_def_27,type,
'A_TESL_atomic_list$': $tType ).
tff(type_def_28,type,
'Int_int_fun$': $tType ).
tff(type_def_29,type,
'A_TESL_atomic_list_a_TESL_atomic_list_prod$': $tType ).
tff(type_def_30,type,
'Nat_nat_prod$': $tType ).
tff(type_def_31,type,
'Nat_nat_prod_set$': $tType ).
tff(type_def_32,type,
'Cnt_expr$': $tType ).
tff(type_def_33,type,
'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$': $tType ).
tff(type_def_34,type,
'A_run$': $tType ).
tff(type_def_35,type,
'A_tag_const$': $tType ).
tff(type_def_36,type,
'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$': $tType ).
tff(type_def_37,type,
'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$': $tType ).
tff(type_def_38,type,
'Nat_nat_fun$': $tType ).
tff(type_def_39,type,
'A_TESL_atomic_list_nat_prod$': $tType ).
tff(type_def_40,type,
'Int_nat_fun$': $tType ).
tff(type_def_41,type,
'A_run_set_a_run_set_a_run_set_fun_fun$': $tType ).
tff(type_def_42,type,
'Nat$': $tType ).
tff(type_def_43,type,
'A_constr_list_a_TESL_atomic_list_bool_fun_fun$': $tType ).
tff(type_def_44,type,
'A_constr_list_a_constr_list_prod$': $tType ).
tff(type_def_45,type,
'A_constr$': $tType ).
tff(type_def_46,type,
'A_run_bool_fun_a_run_bool_fun_fun$': $tType ).
tff(type_def_47,type,
'Int_a_run_set_fun$': $tType ).
tff(type_def_48,type,
tlbool: $tType ).
tff(type_def_49,type,
'A_TESL_atomic_a_TESL_atomic_fun$': $tType ).
tff(type_def_50,type,
'A_run_set_a_run_set_fun$': $tType ).
tff(type_def_51,type,
'A_constr_list_a_constr_list_bool_fun_fun$': $tType ).
tff(type_def_52,type,
'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$': $tType ).
tff(type_def_53,type,
'A_TESL_atomic_list_bool_fun$': $tType ).
tff(type_def_54,type,
'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_fun_fun$': $tType ).
tff(type_def_55,type,
'A_constr_a_constr_bool_fun_fun$': $tType ).
tff(type_def_56,type,
'A_run_set_nat_fun$': $tType ).
tff(type_def_57,type,
'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_fun_fun$': $tType ).
tff(type_def_58,type,
'A_run_set$': $tType ).
tff(type_def_59,type,
'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$': $tType ).
tff(type_def_60,type,
'Bool_bool_fun$': $tType ).
tff(type_def_61,type,
'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$': $tType ).
tff(type_def_62,type,
'A_TESL_atomic$': $tType ).
tff(type_def_63,type,
'A_run_bool_fun$': $tType ).
tff(type_def_64,type,
'Int_int_int_fun_fun$': $tType ).
tff(type_def_65,type,
'A_constr_list_bool_fun$': $tType ).
tff(type_def_66,type,
'Int_int_bool_fun_fun$': $tType ).
tff(type_def_67,type,
'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$': $tType ).
tff(type_def_68,type,
'Nat_bool_fun$': $tType ).
tff(type_def_69,type,
'A_constr_list_list$': $tType ).
tff(type_def_70,type,
'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_fun$': $tType ).
tff(type_def_71,type,
'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun_a_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun_fun$': $tType ).
tff(type_def_72,type,
'Nat_int_fun$': $tType ).
tff(type_def_73,type,
'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$': $tType ).
tff(type_def_74,type,
'A_TESL_atomic_list_a_TESL_atomic_list_prod_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_fun$': $tType ).
tff(func_def_0,type,
'fun_app$g': ( 'A_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_fun$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).
tff(func_def_1,type,
'inf$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_fun_fun$' ).
tff(func_def_2,type,
'uuh$': '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_3,type,
'fun_app$l': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_fun_fun$' * 'Nat$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_fun$' ).
tff(func_def_4,type,
'case_prod$a': '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_prod_bool_fun$' ).
tff(func_def_5,type,
'psi_1$': 'A_TESL_atomic_list$' ).
tff(func_def_6,type,
'bot$a': 'A_run_set$' ).
tff(func_def_7,type,
'uuk$': 'A_run_bool_fun$' ).
tff(func_def_8,type,
def_3: ( 'A_run_bool_fun$' * 'A_run$' ) > tlbool ).
tff(func_def_9,type,
'collect$a': 'Nat_nat_prod_bool_fun$' > 'Nat_nat_prod_set$' ).
tff(func_def_10,type,
'fun_app$c': ( '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_fun$' * '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_11,type,
'gamma_1$': 'A_constr_list$' ).
tff(func_def_12,type,
'sup$d': ( '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_13,type,
'inf$m': tlbool > 'Bool_bool_fun$' ).
tff(func_def_14,type,
'implies$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_15,type,
'fun_app$x': ( 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun_a_TESL_atomic_list_a_TESL_atomic_list_bool_fun_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_16,type,
'strictlyPrecedes$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_17,type,
'fun_app$ad': ( 'Int_int_int_fun_fun$' * $int ) > 'Int_int_fun$' ).
tff(func_def_18,type,
'cons$b': ( 'A_TESL_atomic_list$' * 'A_TESL_atomic_list_list$' ) > 'A_TESL_atomic_list_list$' ).
tff(func_def_19,type,
'bot$f': 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ).
tff(func_def_20,type,
def_1: ( 'Nat_nat_bool_fun_fun$' * 'Nat$' * 'Nat$' ) > tlbool ).
tff(func_def_21,type,
'fun_app$ab': ( 'Nat_nat_nat_fun_fun$' * 'Nat$' ) > 'Nat_nat_fun$' ).
tff(func_def_22,type,
'uui$': '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_23,type,
'inf$e': ( 'Nat_nat_bool_fun_fun$' * 'Nat_nat_bool_fun_fun$' ) > 'Nat_nat_bool_fun_fun$' ).
tff(func_def_24,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_25,type,
def_5: ( 'Nat_nat_bool_fun_fun$' * 'Nat$' * 'Nat$' ) > tlbool ).
tff(func_def_26,type,
'collect$': 'A_run_bool_fun$' > 'A_run_set$' ).
tff(func_def_27,type,
'heronConf_interpretation$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_run_set$' ).
tff(func_def_28,type,
'inf$g': 'Int_int_int_fun_fun$' ).
tff(func_def_29,type,
'case_prod$b': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' ).
tff(func_def_30,type,
'fun_app$z': ( '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_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_fun$' ).
tff(func_def_31,type,
'fun_app$k': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ).
tff(func_def_32,type,
'n_1$': 'Nat$' ).
tff(func_def_33,type,
'ticks$': ( 'Clock$' * 'Nat$' ) > 'A_constr$' ).
tff(func_def_34,type,
'n$': 'Nat$' ).
tff(func_def_35,type,
'inf$k': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' ).
tff(func_def_36,type,
'cons$c': ( 'A_constr_list$' * 'A_constr_list_list$' ) > 'A_constr_list_list$' ).
tff(func_def_37,type,
'fun_app$u': ( 'Nat_int_fun$' * 'Nat$' ) > $int ).
tff(func_def_38,type,
'nil$a': 'A_constr_list$' ).
tff(func_def_39,type,
'nat$': 'Int_nat_fun$' ).
tff(func_def_40,type,
'fun_app$ag': ( 'Int_a_run_set_fun$' * $int ) > 'A_run_set$' ).
tff(func_def_41,type,
'tESL_interpretation_stepwise$': 'A_TESL_atomic_list$' > 'Nat_a_run_set_fun$' ).
tff(func_def_42,type,
'case_prod$d': ( '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_fun_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_43,type,
'weaklyPrecedes$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_44,type,
'fun_app$j': ( '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_45,type,
'k_2$': 'Clock$' ).
tff(func_def_46,type,
'sporadicOn$': ( 'Clock$' * 'A_tag_const$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_47,type,
'impliesNot$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_48,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_49,type,
'inf$l': ( 'A_TESL_atomic_list_bool_fun$' * 'A_TESL_atomic_list_bool_fun$' ) > 'A_TESL_atomic_list_bool_fun$' ).
tff(func_def_50,type,
'bot$c': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun_fun$' ).
tff(func_def_51,type,
'collect$b': '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_52,type,
'of_nat$': 'Nat_int_fun$' ).
tff(func_def_53,type,
'pair$d': ( '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_54,type,
'inf$n': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' ).
tff(func_def_55,type,
'pair$': '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_fun_fun$' ).
tff(func_def_56,type,
'pair$a': 'A_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_fun_fun$' ).
tff(func_def_57,type,
'tickCntArith$': ( 'Cnt_expr$' * 'Cnt_expr$' * 'Nat_nat_prod_bool_fun$' ) > 'A_constr$' ).
tff(func_def_58,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_59,type,
'cons$': ( 'A_TESL_atomic$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_60,type,
'accp$': '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_fun$' > 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' ).
tff(func_def_61,type,
'fun_app$ai': ( 'A_run_set_int_fun$' * 'A_run_set$' ) > $int ).
tff(func_def_62,type,
'case_prod$c': 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' ).
tff(func_def_63,type,
'bot$': 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_set$' ).
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_fun$' ).
tff(func_def_65,type,
'inf$': 'A_run_set_a_run_set_a_run_set_fun_fun$' ).
tff(func_def_66,type,
'fun_app$ah': ( 'A_run_set_nat_fun$' * 'A_run_set$' ) > 'Nat$' ).
tff(func_def_67,type,
'phi_1$': 'A_TESL_atomic_list$' ).
tff(func_def_68,type,
'pair$e': ( 'A_constr_a_constr_bool_fun_fun$' * 'A_constr_list$' ) > 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' ).
tff(func_def_69,type,
'inf$c': 'A_run_bool_fun$' > 'A_run_bool_fun_a_run_bool_fun_fun$' ).
tff(func_def_70,type,
'uue$': ( 'A_run_set$' * 'A_run_bool_fun$' ) > 'A_run_bool_fun$' ).
tff(func_def_71,type,
'nil$': 'A_TESL_atomic_list$' ).
tff(func_def_72,type,
'operational_semantics_elim_inv$': '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_73,type,
'psi_2$': 'A_TESL_atomic_list$' ).
tff(func_def_74,type,
tltrue: tlbool ).
tff(func_def_75,type,
'inf$a': '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_fun_fun$' ).
tff(func_def_76,type,
'fun_app$f': ( 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list_bool_fun$' ).
tff(func_def_77,type,
'uuc$': ( 'Bool_bool_fun$' * 'Nat_nat_bool_fun_fun$' ) > 'Nat_nat_bool_fun_fun$' ).
tff(func_def_78,type,
'phi_2$': 'A_TESL_atomic_list$' ).
tff(func_def_79,type,
'n_2$': 'Nat$' ).
tff(func_def_80,type,
'uud$': 'A_run_set$' > 'A_run_bool_fun$' ).
tff(func_def_81,type,
'fun_app$am': ( 'A_constr_list_a_constr_list_bool_fun_fun$' * 'A_constr_list$' ) > 'A_constr_list_bool_fun$' ).
tff(func_def_82,type,
'fun_app$r': ( 'A_run_set_a_run_set_a_run_set_fun_fun$' * 'A_run_set$' ) > 'A_run_set_a_run_set_fun$' ).
tff(func_def_83,type,
'uub$': 'Nat_nat_bool_fun_fun$' ).
tff(func_def_84,type,
'psi$': 'A_TESL_atomic_list$' ).
tff(func_def_85,type,
'inf$h': ( '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_86,type,
'uuf$': ( 'A_run_bool_fun$' * 'A_run_bool_fun$' ) > 'A_run_bool_fun$' ).
tff(func_def_87,type,
'gamma_2$': 'A_constr_list$' ).
tff(func_def_88,type,
'gamma$': 'A_constr_list$' ).
tff(func_def_89,type,
'sup$h': ( '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_90,type,
'bot$g': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ).
tff(func_def_91,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_92,type,
'fun_app$aa': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_93,type,
'case_prod$f': ( 'A_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_fun_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).
tff(func_def_94,type,
'sup$': 'A_run_set_a_run_set_a_run_set_fun_fun$' ).
tff(func_def_95,type,
'fun_app$af': ( 'Int_int_bool_fun_fun$' * $int ) > 'Int_bool_fun$' ).
tff(func_def_96,type,
'pair$f': ( 'A_TESL_atomic_list$' * 'Nat$' ) > 'A_TESL_atomic_list_nat_prod$' ).
tff(func_def_97,type,
'fun_app$w': ( '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_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_fun$' ).
tff(func_def_98,type,
'fun_app$ac': ( 'Int_int_fun$' * $int ) > $int ).
tff(func_def_99,type,
'insert$a': 'A_run$' > 'A_run_set_a_run_set_fun$' ).
tff(func_def_100,type,
'bot$e': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ).
tff(func_def_101,type,
'nil$b': 'A_TESL_atomic_list_list$' ).
tff(func_def_102,type,
'sup$e': ( '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_fun$' ).
tff(func_def_103,type,
'fun_app$n': ( 'Nat_nat_bool_fun_fun$' * 'Nat$' ) > 'Nat_bool_fun$' ).
tff(func_def_104,type,
'sup$g': ( '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_105,type,
tlfalse: tlbool ).
tff(func_def_106,type,
'pair$c': ( 'Nat$' * 'Nat$' ) > 'Nat_nat_prod$' ).
tff(func_def_107,type,
'pair$g': ( 'A_constr_list$' * 'A_constr_list$' ) > 'A_constr_list_a_constr_list_prod$' ).
tff(func_def_108,type,
def_2: ( 'A_run_bool_fun$' * 'A_run$' ) > tlbool ).
tff(func_def_109,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$' ).
tff(func_def_110,type,
'case_prod$': 'Nat_nat_bool_fun_fun$' > 'Nat_nat_prod_bool_fun$' ).
tff(func_def_111,type,
'nil$c': 'A_constr_list_list$' ).
tff(func_def_112,type,
'tickCountLeq$': ( 'Clock$' * 'Nat$' ) > 'Cnt_expr$' ).
tff(func_def_113,type,
'notTicks$': ( 'Clock$' * 'Nat$' ) > 'A_constr$' ).
tff(func_def_114,type,
'bot$d': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' ).
tff(func_def_115,type,
'inf$j': ( '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_116,type,
'uu$': ( tlbool * 'Nat_nat_bool_fun_fun$' ) > 'Nat_nat_bool_fun_fun$' ).
tff(func_def_117,type,
'fun_app$s': ( 'Nat_a_run_set_fun$' * 'Nat$' ) > 'A_run_set$' ).
tff(func_def_118,type,
'fun_app$d': ( '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_fun_fun$' * '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_fun$' ).
tff(func_def_119,type,
'sup$f': ( '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_120,type,
'pair$b': 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_fun_fun$' ).
tff(func_def_121,type,
'fun_app$q': ( 'A_run_set_a_run_set_fun$' * 'A_run_set$' ) > 'A_run_set$' ).
tff(func_def_122,type,
'timestamp$': ( 'Clock$' * 'Nat$' * 'A_tag_const$' ) > 'A_constr$' ).
tff(func_def_123,type,
'fun_app$b': ( '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_124,type,
'k_1$': 'Clock$' ).
tff(func_def_125,type,
'uug$': ( 'A_run_set$' * 'A_run_set$' ) > 'A_run_bool_fun$' ).
tff(func_def_126,type,
def_6: ( 'Nat_nat_bool_fun_fun$' * 'Nat_nat_prod$' ) > tlbool ).
tff(func_def_127,type,
'sup$a': 'Nat_nat_nat_fun_fun$' ).
tff(func_def_128,type,
'inf$f': 'Nat_nat_nat_fun_fun$' ).
tff(func_def_129,type,
'case_prod$e': ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_fun_fun$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ).
tff(func_def_130,type,
'bot$b': 'Nat$' ).
tff(func_def_131,type,
'phi$': 'A_TESL_atomic_list$' ).
tff(func_def_132,type,
def_4: ( 'Nat_nat_bool_fun_fun$' * 'Nat_nat_prod$' ) > tlbool ).
tff(func_def_133,type,
'inf$b': '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_fun$' ).
tff(func_def_134,type,
'inf$i': ( '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_135,type,
'fun_app$ak': ( 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' * 'A_TESL_atomic_list$' ) > 'A_constr_list_bool_fun$' ).
tff(func_def_136,type,
'fun_app$h': ( 'A_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_fun_fun$' * 'A_TESL_atomic_list$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_a_TESL_atomic_list_prod_fun$' ).
tff(func_def_137,type,
'tickCountLess$': ( 'Clock$' * 'Nat$' ) > 'Cnt_expr$' ).
tff(func_def_138,type,
'fun_app$al': ( 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' * 'A_constr_list$' ) > 'A_TESL_atomic_list_bool_fun$' ).
tff(func_def_139,type,
'uuj$': 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' > 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ).
tff(func_def_140,type,
'uua$': 'Nat_nat_prod_bool_fun$' > 'Nat_nat_bool_fun_fun$' ).
tff(func_def_141,type,
'fun_app$t': ( 'Int_nat_fun$' * $int ) > 'Nat$' ).
tff(func_def_142,type,
'sup$b': 'Int_int_int_fun_fun$' ).
tff(func_def_143,type,
'less_eq$f': 'Nat_nat_bool_fun_fun$' ).
tff(func_def_144,type,
'heronConf_interpretation_rel$': '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_fun$' ).
tff(func_def_145,type,
'fun_app$y': ( 'A_run_bool_fun_a_run_bool_fun_fun$' * 'A_run_bool_fun$' ) > 'A_run_bool_fun$' ).
tff(func_def_146,type,
'cons$a': ( 'A_constr$' * 'A_constr_list$' ) > 'A_constr_list$' ).
tff(func_def_147,type,
'symbolic_run_interpretation$': 'A_constr_list$' > 'A_run_set$' ).
tff(func_def_152,type,
sK7: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_run_set$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_153,type,
sK8: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_run_set$' ) > 'A_constr_list$' ).
tff(func_def_154,type,
sK9: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_run_set$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_155,type,
sK10: ( 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' * 'A_run_set$' ) > 'Nat$' ).
tff(func_def_156,type,
sK11: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' > 'Nat$' ).
tff(func_def_157,type,
sK12: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).
tff(func_def_158,type,
sK13: ( 'Nat_nat_prod_bool_fun$' * 'Nat_nat_bool_fun_fun$' ) > 'Nat$' ).
tff(func_def_159,type,
sK14: ( 'Nat_nat_prod_bool_fun$' * 'Nat_nat_bool_fun_fun$' ) > 'Nat$' ).
tff(func_def_160,type,
sK15: 'Int_nat_fun$' > $int ).
tff(func_def_161,type,
sK16: 'Int_nat_fun$' > $int ).
tff(func_def_162,type,
sK17: ( 'A_run_bool_fun$' * 'A_run_bool_fun$' ) > 'A_run$' ).
tff(func_def_163,type,
sK18: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list$' ).
tff(func_def_164,type,
sK19: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'Nat$' ).
tff(func_def_165,type,
sK20: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_166,type,
sK21: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_167,type,
sK22: 'A_run_set$' ).
tff(func_def_168,type,
sK23: 'A_run_set$' ).
tff(func_def_169,type,
sK24: 'A_run_set$' ).
tff(func_def_170,type,
sK25: 'A_TESL_atomic_list$' > 'A_TESL_atomic_list$' ).
tff(func_def_171,type,
sK26: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).
tff(func_def_172,type,
sK27: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).
tff(func_def_173,type,
sK28: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).
tff(func_def_174,type,
sK29: 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' > 'A_constr_list$' ).
tff(func_def_175,type,
sK30: 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' > 'A_constr$' ).
tff(func_def_176,type,
sK31: 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_177,type,
sK32: 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' > 'A_TESL_atomic$' ).
tff(func_def_178,type,
sK33: 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' > 'A_constr$' ).
tff(func_def_179,type,
sK34: 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' > 'A_constr_list$' ).
tff(func_def_180,type,
sK35: 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' > 'A_TESL_atomic$' ).
tff(func_def_181,type,
sK36: 'A_TESL_atomic_list_a_constr_list_bool_fun_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_182,type,
sK37: 'Nat_a_run_set_fun$' > 'Nat$' ).
tff(func_def_183,type,
sK38: 'Nat_a_run_set_fun$' > 'Nat$' ).
tff(func_def_184,type,
sK39: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_185,type,
sK40: ( '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_bool_fun_fun$' ) > 'A_constr_list$' ).
tff(func_def_186,type,
sK41: ( '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_bool_fun_fun$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ).
tff(func_def_187,type,
sK42: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_188,type,
sK43: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_189,type,
sK44: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic$' ).
tff(func_def_190,type,
sK45: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic$' ).
tff(func_def_191,type,
sK46: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_192,type,
sK47: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_193,type,
sK48: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_194,type,
sK49: 'A_run_set$' ).
tff(func_def_195,type,
sK50: 'A_run_set$' ).
tff(func_def_196,type,
sK51: 'A_run_set$' ).
tff(func_def_197,type,
sK52: ( 'A_run_set$' * 'A_run_set$' ) > 'A_run$' ).
tff(func_def_198,type,
sK53: 'Nat_a_run_set_fun$' > 'Nat$' ).
tff(func_def_199,type,
sK54: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_200,type,
sK55: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_201,type,
sK56: ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' * 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_202,type,
sK57: ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' * 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_203,type,
sK58: ( 'A_run_set$' * 'A_run_set$' ) > 'A_run$' ).
tff(func_def_204,type,
sK59: ( 'A_run_set$' * 'A_run_set$' ) > 'A_run$' ).
tff(func_def_205,type,
sK60: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr_a_constr_bool_fun_fun$' ).
tff(func_def_206,type,
sK61: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr_a_constr_bool_fun_fun$' ).
tff(func_def_207,type,
sK62: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr$' ).
tff(func_def_208,type,
sK63: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr_list$' ).
tff(func_def_209,type,
sK64: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_210,type,
sK65: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_211,type,
sK66: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_212,type,
sK67: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_213,type,
sK68: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list$' ).
tff(func_def_214,type,
sK69: '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_215,type,
sK70: '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_216,type,
sK71: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list$' ).
tff(func_def_217,type,
sK72: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'Nat$' ).
tff(func_def_218,type,
sK73: ( 'A_run_set$' * 'A_run_set$' ) > 'A_run$' ).
tff(func_def_219,type,
sK74: ( '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$' ).
tff(func_def_220,type,
sK75: ( '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$' ) > 'Nat$' ).
tff(func_def_221,type,
sK76: ( '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_TESL_atomic_list$' ).
tff(func_def_222,type,
sK77: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'Nat$' ).
tff(func_def_223,type,
sK78: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_224,type,
sK79: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list$' ).
tff(func_def_225,type,
sK80: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_226,type,
sK81: ( 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_227,type,
sK82: ( 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_228,type,
sK83: 'Int_a_run_set_fun$' > $int ).
tff(func_def_229,type,
sK84: 'Int_a_run_set_fun$' > $int ).
tff(func_def_230,type,
sK85: 'A_TESL_atomic_list$' > 'A_TESL_atomic_list$' ).
tff(func_def_231,type,
sK86: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).
tff(func_def_232,type,
sK87: 'Cnt_expr$' > 'Nat$' ).
tff(func_def_233,type,
sK88: 'Cnt_expr$' > 'Clock$' ).
tff(func_def_234,type,
sK89: 'Cnt_expr$' > 'Clock$' ).
tff(func_def_235,type,
sK90: 'Cnt_expr$' > 'Nat$' ).
tff(func_def_236,type,
sK91: ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).
tff(func_def_237,type,
sK92: ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ) > 'Nat$' ).
tff(func_def_238,type,
sK93: ( '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$' ).
tff(func_def_239,type,
sK94: ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_240,type,
sK95: ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_241,type,
sK96: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_242,type,
sK97: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_243,type,
sK98: 'A_constr_list$' > 'A_constr_list$' ).
tff(func_def_244,type,
sK99: 'A_constr_list$' > 'A_constr$' ).
tff(func_def_245,type,
sK100: 'A_constr_list$' > 'A_constr$' ).
tff(func_def_246,type,
sK101: 'A_constr_list$' > 'A_constr$' ).
tff(func_def_247,type,
sK102: ( '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$' ).
tff(func_def_248,type,
sK103: ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_set$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).
tff(func_def_249,type,
sK104: 'A_constr_list$' > 'A_constr_list$' ).
tff(func_def_250,type,
sK105: 'A_constr_list$' > 'A_constr$' ).
tff(func_def_251,type,
sK106: 'Int_a_run_set_fun$' > $int ).
tff(func_def_252,type,
sK107: 'Int_a_run_set_fun$' > $int ).
tff(func_def_253,type,
sK108: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_254,type,
sK109: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'Nat$' ).
tff(func_def_255,type,
sK110: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_256,type,
sK111: 'A_constr_list$' > 'A_constr$' ).
tff(func_def_257,type,
sK112: 'A_constr_list$' > 'A_constr_list$' ).
tff(func_def_258,type,
sK113: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_259,type,
sK114: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_260,type,
sK115: 'Int_int_fun$' > $int ).
tff(func_def_261,type,
sK116: 'Int_int_fun$' > $int ).
tff(func_def_262,type,
sK117: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr_a_constr_bool_fun_fun$' ).
tff(func_def_263,type,
sK118: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr$' ).
tff(func_def_264,type,
sK119: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr_list$' ).
tff(func_def_265,type,
sK120: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr$' ).
tff(func_def_266,type,
sK121: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr_a_constr_bool_fun_fun$' ).
tff(func_def_267,type,
sK122: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr$' ).
tff(func_def_268,type,
sK123: 'A_constr_a_constr_bool_fun_fun_a_constr_list_prod$' > 'A_constr_a_constr_bool_fun_fun$' ).
tff(func_def_269,type,
sK124: '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_270,type,
sK125: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' > 'A_constr_list$' ).
tff(func_def_271,type,
sK126: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_272,type,
sK127: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'Nat$' ).
tff(func_def_273,type,
sK128: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).
tff(func_def_274,type,
sK129: ( 'A_run_bool_fun$' * 'A_run_bool_fun$' * 'A_run_set$' ) > 'A_run$' ).
tff(func_def_275,type,
sK130: 'A_constr_list_bool_fun$' > 'A_constr_list$' ).
tff(func_def_276,type,
sK131: 'A_constr_list_bool_fun$' > 'A_constr$' ).
tff(func_def_277,type,
sK132: 'A_constr_list_bool_fun$' > 'A_constr$' ).
tff(func_def_278,type,
sK133: 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_279,type,
sK134: 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_280,type,
sK135: 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic$' ).
tff(func_def_281,type,
sK136: 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_a_TESL_atomic_fun$' ).
tff(func_def_282,type,
sK137: 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_283,type,
sK138: 'A_TESL_atomic_a_TESL_atomic_fun_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_a_TESL_atomic_fun$' ).
tff(func_def_284,type,
sK139: 'A_TESL_atomic_list$' > 'A_TESL_atomic_list$' ).
tff(func_def_285,type,
sK140: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).
tff(func_def_286,type,
sK141: ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ) > 'Nat$' ).
tff(func_def_287,type,
sK142: ( 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun_fun$' * 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ) > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).
tff(func_def_288,type,
sK143: 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic$' ).
tff(func_def_289,type,
sK144: 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_290,type,
sK145: 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_291,type,
sK146: 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic$' ).
tff(func_def_292,type,
sK147: 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_293,type,
sK148: 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic$' ).
tff(func_def_294,type,
sK149: 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_295,type,
sK150: 'A_TESL_atomic_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic$' ).
tff(func_def_296,type,
sK151: 'A_TESL_atomic_list$' > 'A_TESL_atomic$' ).
tff(func_def_297,type,
sK152: 'A_TESL_atomic_list$' > 'A_TESL_atomic_list$' ).
tff(func_def_298,type,
sK153: 'Int_int_fun$' > $int ).
tff(func_def_299,type,
sK154: 'Int_int_fun$' > $int ).
tff(func_def_300,type,
sK155: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_301,type,
sK156: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_302,type,
sK157: ( 'A_run_bool_fun$' * 'A_run_bool_fun$' ) > 'A_run$' ).
tff(func_def_303,type,
sK158: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_304,type,
sK159: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' > 'Nat$' ).
tff(func_def_305,type,
sK160: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_bool_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_306,type,
sK161: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_307,type,
sK162: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_308,type,
sK163: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_309,type,
sK164: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_310,type,
sK165: ( 'A_run_set$' * 'A_run_set$' ) > 'A_run$' ).
tff(func_def_311,type,
sK166: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_312,type,
sK167: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_313,type,
sK168: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_314,type,
sK169: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_315,type,
sK170: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_316,type,
sK171: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_317,type,
sK172: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_318,type,
sK173: 'A_run_set_nat_fun$' > 'A_run_set$' ).
tff(func_def_319,type,
sK174: 'A_run_set_nat_fun$' > 'A_run_set$' ).
tff(func_def_320,type,
sK175: ( 'Nat_nat_bool_fun_fun$' * 'Nat_nat_prod$' ) > 'Nat$' ).
tff(func_def_321,type,
sK176: ( 'Nat_nat_bool_fun_fun$' * 'Nat_nat_prod$' ) > 'Nat$' ).
tff(func_def_322,type,
sK177: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_323,type,
sK178: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_324,type,
sK179: 'A_TESL_atomic_list_nat_prod$' > 'Nat$' ).
tff(func_def_325,type,
sK180: 'A_TESL_atomic_list_nat_prod$' > 'A_TESL_atomic$' ).
tff(func_def_326,type,
sK181: 'A_TESL_atomic_list_nat_prod$' > 'Nat$' ).
tff(func_def_327,type,
sK182: 'A_TESL_atomic_list_nat_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_328,type,
sK183: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic$' ).
tff(func_def_329,type,
sK184: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_330,type,
sK185: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_331,type,
sK186: 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_332,type,
sK187: 'Nat_a_run_set_fun$' > 'Nat$' ).
tff(func_def_333,type,
sK188: 'Nat_a_run_set_fun$' > 'Nat$' ).
tff(func_def_334,type,
sK189: 'Int_a_run_set_fun$' > $int ).
tff(func_def_335,type,
sK190: 'Int_a_run_set_fun$' > $int ).
tff(func_def_336,type,
sK191: ( 'Nat_nat_prod$' * 'Nat_nat_bool_fun_fun$' ) > 'Nat$' ).
tff(func_def_337,type,
sK192: ( 'Nat_nat_prod$' * 'Nat_nat_bool_fun_fun$' ) > 'Nat$' ).
tff(func_def_338,type,
sK193: ( 'A_run_set$' * 'A_run_set$' * 'A_run_set$' ) > 'A_run_set$' ).
tff(func_def_339,type,
sK194: ( 'A_run_set$' * 'A_run_set$' * 'A_run_set$' ) > 'A_run_set$' ).
tff(func_def_340,type,
sK195: 'A_run_set_nat_fun$' > 'A_run_set$' ).
tff(func_def_341,type,
sK196: 'A_run_set_nat_fun$' > 'A_run_set$' ).
tff(func_def_342,type,
sK197: ( '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_343,type,
sK198: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_344,type,
sK199: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_345,type,
sK200: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_346,type,
sK201: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_347,type,
sK202: 'Nat_a_run_set_fun$' > 'Nat$' ).
tff(func_def_348,type,
sK203: ( 'Nat_nat_prod$' * 'Nat_nat_bool_fun_fun$' * 'Nat_nat_bool_fun_fun$' ) > 'Nat$' ).
tff(func_def_349,type,
sK204: ( 'Nat_nat_prod$' * 'Nat_nat_bool_fun_fun$' * 'Nat_nat_bool_fun_fun$' ) > 'Nat$' ).
tff(func_def_350,type,
sK205: ( 'Bool_bool_fun$' * 'Nat_nat_prod$' * 'Nat_nat_bool_fun_fun$' ) > 'Nat$' ).
tff(func_def_351,type,
sK206: ( 'Bool_bool_fun$' * 'Nat_nat_prod$' * 'Nat_nat_bool_fun_fun$' ) > 'Nat$' ).
tff(func_def_352,type,
sK207: ( '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_TESL_atomic_list$' ).
tff(func_def_353,type,
sK208: ( '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$' ) > 'Nat$' ).
tff(func_def_354,type,
sK209: ( '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$' ).
tff(func_def_355,type,
sK210: 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_356,type,
sK211: 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic$' ).
tff(func_def_357,type,
sK212: 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_constr$' ).
tff(func_def_358,type,
sK213: 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_constr_list$' ).
tff(func_def_359,type,
sK214: 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_constr_list$' ).
tff(func_def_360,type,
sK215: 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_constr$' ).
tff(func_def_361,type,
sK216: 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic$' ).
tff(func_def_362,type,
sK217: 'A_constr_list_a_TESL_atomic_list_bool_fun_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_363,type,
sK218: 'A_run_set_a_run_set_fun$' > 'A_run_set$' ).
tff(func_def_364,type,
sK219: 'A_run_set_a_run_set_fun$' > 'A_run_set$' ).
tff(func_def_365,type,
sK220: 'A_constr_list$' > 'A_constr$' ).
tff(func_def_366,type,
sK221: 'A_constr_list$' > 'A_constr_list$' ).
tff(func_def_367,type,
sK222: ( 'A_run_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_368,type,
sK223: ( 'A_run_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > 'Nat$' ).
tff(func_def_369,type,
sK224: ( 'A_run_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > 'A_constr_list$' ).
tff(func_def_370,type,
sK225: ( 'A_run_set$' * 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod$' ) > 'A_TESL_atomic_list$' ).
tff(func_def_371,type,
sK226: ( '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$' ).
tff(func_def_372,type,
sK227: ( '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$' ) > 'Nat$' ).
tff(func_def_373,type,
sK228: ( '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_TESL_atomic_list$' ).
tff(func_def_374,type,
sK229: ( '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$' ) > 'Nat$' ).
tff(func_def_375,type,
sK230: ( '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_TESL_atomic_list$' ).
tff(func_def_376,type,
sK231: ( '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$' ).
tff(func_def_377,type,
sK232: ( '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_TESL_atomic_list$' ).
tff(func_def_378,type,
sK233: ( '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_TESL_atomic_list$' ).
tff(func_def_379,type,
sK234: ( '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_TESL_atomic_list$' ).
tff(func_def_380,type,
sK235: ( '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_TESL_atomic_list$' ).
tff(func_def_381,type,
sK236: ( '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$' ).
tff(func_def_382,type,
sK237: ( '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$' ) > 'Nat$' ).
tff(func_def_383,type,
sK238: ( '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$' ) > 'Nat$' ).
tff(func_def_384,type,
sK239: ( '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_TESL_atomic_list$' ).
tff(func_def_385,type,
sK240: ( '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_TESL_atomic_list$' ).
tff(func_def_386,type,
sK241: ( '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$' ).
tff(func_def_387,type,
sK242: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_388,type,
sK243: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_389,type,
sK244: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_390,type,
sK245: 'A_TESL_atomic_list_list$' > 'A_TESL_atomic_list_list$' ).
tff(func_def_391,type,
sK246: 'A_TESL_atomic_list_list$' > 'A_TESL_atomic_list$' ).
tff(func_def_392,type,
sK247: 'A_TESL_atomic_list_list$' > 'A_TESL_atomic$' ).
tff(func_def_393,type,
sK248: 'A_TESL_atomic_list_list$' > 'A_TESL_atomic_list_list$' ).
tff(func_def_394,type,
sK249: ( '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_bool_fun_fun$' ) > 'A_constr_list$' ).
tff(func_def_395,type,
sK250: ( '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_bool_fun_fun$' ) > 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' ).
tff(func_def_396,type,
sK251: ( '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$' ).
tff(func_def_397,type,
sK252: 'A_run_set_int_fun$' > 'A_run_set$' ).
tff(func_def_398,type,
sK253: 'A_run_set_int_fun$' > 'A_run_set$' ).
tff(func_def_399,type,
sK254: ( '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_400,type,
sK255: ( '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_401,type,
sK256: 'A_run_set_nat_fun$' > 'A_run_set$' ).
tff(func_def_402,type,
sK257: 'A_run_set_nat_fun$' > 'A_run_set$' ).
tff(func_def_403,type,
sK258: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_404,type,
sK259: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_405,type,
sK260: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_406,type,
sK261: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_407,type,
sK262: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_408,type,
sK263: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_409,type,
sK264: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_410,type,
sK265: 'A_run_set_a_run_set_fun$' > 'A_run_set$' ).
tff(func_def_411,type,
sK266: 'A_run_set_a_run_set_fun$' > 'A_run_set$' ).
tff(func_def_412,type,
sK267: 'A_constr_list_a_constr_list_bool_fun_fun$' > 'A_constr_list$' ).
tff(func_def_413,type,
sK268: 'A_constr_list_a_constr_list_bool_fun_fun$' > 'A_constr$' ).
tff(func_def_414,type,
sK269: 'A_constr_list_a_constr_list_bool_fun_fun$' > 'A_constr_list$' ).
tff(func_def_415,type,
sK270: 'A_constr_list_a_constr_list_bool_fun_fun$' > 'A_constr$' ).
tff(func_def_416,type,
sK271: 'A_constr_list_a_constr_list_bool_fun_fun$' > 'A_constr$' ).
tff(func_def_417,type,
sK272: 'A_constr_list_a_constr_list_bool_fun_fun$' > 'A_constr_list$' ).
tff(func_def_418,type,
sK273: 'A_constr_list_a_constr_list_bool_fun_fun$' > 'A_constr_list$' ).
tff(func_def_419,type,
sK274: 'A_constr_list_a_constr_list_bool_fun_fun$' > 'A_constr$' ).
tff(func_def_420,type,
sK275: 'A_constr_list_a_constr_list_prod$' > 'A_constr_list$' ).
tff(func_def_421,type,
sK276: 'A_constr_list_a_constr_list_prod$' > 'A_constr$' ).
tff(func_def_422,type,
sK277: 'A_constr_list_a_constr_list_prod$' > 'A_constr_list$' ).
tff(func_def_423,type,
sK278: 'A_constr_list_a_constr_list_prod$' > 'A_constr_list$' ).
tff(func_def_424,type,
sK279: 'Int_nat_fun$' > $int ).
tff(func_def_425,type,
sK280: 'Int_nat_fun$' > $int ).
tff(func_def_426,type,
sK281: 'A_run_set_a_run_set_fun$' > 'A_run_set$' ).
tff(func_def_427,type,
sK282: 'A_run_set_a_run_set_fun$' > 'A_run_set$' ).
tff(func_def_428,type,
sK283: 'Nat_a_run_set_fun$' > 'Nat$' ).
tff(func_def_429,type,
sK284: 'Nat_a_run_set_fun$' > 'Nat$' ).
tff(func_def_430,type,
sK285: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_431,type,
sK286: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_432,type,
sK287: 'Int_int_fun$' > $int ).
tff(func_def_433,type,
sK288: 'Int_int_fun$' > $int ).
tff(func_def_434,type,
sK289: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ).
tff(func_def_435,type,
sK290: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$' > 'Nat$' ).
tff(func_def_436,type,
sK291: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_437,type,
sK292: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_438,type,
sK293: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_439,type,
sK294: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_440,type,
sK295: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_constr_list$' ).
tff(func_def_441,type,
sK296: '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_442,type,
sK297: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_443,type,
sK298: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_444,type,
sK299: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_445,type,
sK300: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_446,type,
sK301: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_447,type,
sK302: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_448,type,
sK303: 'Nat_nat_nat_fun_fun$' > 'Nat$' ).
tff(func_def_449,type,
sK304: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic$' ).
tff(func_def_450,type,
sK305: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' ).
tff(func_def_451,type,
sK306: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' ).
tff(func_def_452,type,
sK307: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic$' ).
tff(func_def_453,type,
sK308: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic$' ).
tff(func_def_454,type,
sK309: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_455,type,
sK310: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' ).
tff(func_def_456,type,
sK311: 'Int_nat_fun$' > $int ).
tff(func_def_457,type,
sK312: 'Int_nat_fun$' > $int ).
tff(func_def_458,type,
sK313: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_459,type,
sK314: 'A_run_set_int_fun$' > 'A_run_set$' ).
tff(func_def_460,type,
sK315: 'A_run_set_int_fun$' > 'A_run_set$' ).
tff(func_def_461,type,
sK316: 'A_run_set_nat_fun$' > 'A_run_set$' ).
tff(func_def_462,type,
sK317: 'A_run_set_nat_fun$' > 'A_run_set$' ).
tff(func_def_463,type,
sK318: ( 'A_run_set$' * 'A_run_set$' ) > 'A_run$' ).
tff(func_def_464,type,
sK319: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_465,type,
sK320: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_466,type,
sK321: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_467,type,
sK322: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_468,type,
sK323: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_469,type,
sK324: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_470,type,
sK325: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_471,type,
sK326: ( 'A_run_set$' * 'A_run_set$' ) > 'A_run$' ).
tff(func_def_472,type,
sK327: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_list$' ).
tff(func_def_473,type,
sK328: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic$' ).
tff(func_def_474,type,
sK329: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' ).
tff(func_def_475,type,
sK330: 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun_a_TESL_atomic_list_prod$' > 'A_TESL_atomic_a_TESL_atomic_bool_fun_fun$' ).
tff(func_def_476,type,
sK331: 'A_run_set_int_fun$' > 'A_run_set$' ).
tff(func_def_477,type,
sK332: 'A_run_set_int_fun$' > 'A_run_set$' ).
tff(func_def_478,type,
sK333: 'Nat$' > 'Nat$' ).
tff(func_def_479,type,
sK334: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_480,type,
sK335: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_481,type,
sK336: 'A_run_set_a_run_set_fun$' > 'A_run_set$' ).
tff(func_def_482,type,
sK337: 'A_run_set_a_run_set_fun$' > 'A_run_set$' ).
tff(func_def_483,type,
sK338: 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_484,type,
sK339: 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_485,type,
sK340: 'A_run_set_int_fun$' > 'A_run_set$' ).
tff(func_def_486,type,
sK341: 'A_run_set_int_fun$' > 'A_run_set$' ).
tff(func_def_487,type,
sK342: 'A_constr_list_a_constr_list_prod$' > 'A_constr_list$' ).
tff(func_def_488,type,
sK343: 'A_constr_list_a_constr_list_prod$' > 'A_constr_list$' ).
tff(func_def_489,type,
sK344: 'A_constr_list_a_constr_list_prod$' > 'A_constr$' ).
tff(func_def_490,type,
sK345: 'A_constr_list_a_constr_list_prod$' > 'A_constr$' ).
tff(func_def_491,type,
sK346: 'A_constr_list_a_constr_list_prod$' > 'A_constr_list$' ).
tff(func_def_492,type,
sK347: 'A_constr_list_a_constr_list_prod$' > 'A_constr_list$' ).
tff(func_def_493,type,
sK348: 'A_constr_list_list$' > 'A_constr_list_list$' ).
tff(func_def_494,type,
sK349: 'A_constr_list_list$' > 'A_constr$' ).
tff(func_def_495,type,
sK350: 'A_constr_list_list$' > 'A_constr_list_list$' ).
tff(func_def_496,type,
sK351: 'A_constr_list_list$' > 'A_constr_list$' ).
tff(func_def_497,type,
sK352: 'A_TESL_atomic_list_bool_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_498,type,
sK353: 'A_TESL_atomic_list_bool_fun$' > 'A_TESL_atomic$' ).
tff(func_def_499,type,
sK354: 'A_TESL_atomic_list_bool_fun$' > 'A_TESL_atomic$' ).
tff(func_def_500,type,
sK355: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_501,type,
sK356: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_502,type,
sK357: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_503,type,
sK358: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_504,type,
sK359: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_505,type,
sK360: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_506,type,
sK361: 'A_run_set_a_run_set_a_run_set_fun_fun$' > 'A_run_set$' ).
tff(func_def_507,type,
sK362: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_508,type,
sK363: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_509,type,
sK364: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_510,type,
sK365: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_511,type,
sK366: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_512,type,
sK367: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_513,type,
sK368: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_514,type,
sK369: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_515,type,
sK370: 'Int_a_run_set_fun$' > $int ).
tff(func_def_516,type,
sK371: 'Int_a_run_set_fun$' > $int ).
tff(func_def_517,type,
sK372: 'Int_nat_fun$' > $int ).
tff(func_def_518,type,
sK373: 'Int_nat_fun$' > $int ).
tff(func_def_519,type,
sK374: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_520,type,
sK375: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_521,type,
sK376: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_522,type,
sK377: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_523,type,
sK378: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_524,type,
sK379: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_525,type,
sK380: 'Int_int_int_fun_fun$' > $int ).
tff(func_def_526,type,
sK381: 'Int_int_fun$' > $int ).
tff(func_def_527,type,
sK382: 'Int_int_fun$' > $int ).
tff(func_def_528,type,
sK383: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_529,type,
sK384: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_constr_list$' ).
tff(func_def_530,type,
sK385: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'Nat$' ).
tff(func_def_531,type,
sK386: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'A_TESL_atomic_list$' ).
tff(func_def_532,type,
sK387: 'Nat_a_run_set_fun$' > 'Nat$' ).
tff(func_def_533,type,
sK388: 'Nat_a_run_set_fun$' > 'Nat$' ).
tff(func_def_534,type,
sK389: 'A_constr_list_nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod_prod_bool_fun$' > 'Nat$' ).
tff(func_def_535,type,
sK390: '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_536,type,
sK391: '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,
'fun_app$i': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_bool_fun$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' ) > $o ).
tff(pred_def_2,type,
'less_eq$c': ( 'A_run_bool_fun$' * 'A_run_bool_fun$' ) > $o ).
tff(pred_def_3,type,
'fun_app$p': ( 'Bool_bool_fun$' * tlbool ) > $o ).
tff(pred_def_4,type,
'fun_app$m': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).
tff(pred_def_5,type,
'member$': ( 'A_run$' * 'A_run_set$' ) > $o ).
tff(pred_def_6,type,
'fun_app$o': ( 'Nat_nat_prod_bool_fun$' * 'Nat_nat_prod$' ) > $o ).
tff(pred_def_7,type,
'less_eq$': ( 'A_run_set$' * 'A_run_set$' ) > $o ).
tff(pred_def_8,type,
'less_eq$h': ( '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_9,type,
'less_eq$e': ( 'Nat_nat_bool_fun_fun$' * 'Nat_nat_bool_fun_fun$' ) > $o ).
tff(pred_def_10,type,
'fun_app$a': ( '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_11,type,
'fun_app$ae': ( 'Int_bool_fun$' * $int ) > $o ).
tff(pred_def_12,type,
'less_eq$g': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > $o ).
tff(pred_def_13,type,
'fun_app$v': ( '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_14,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_set$' ) > $o ).
tff(pred_def_15,type,
'less_eq$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$' ) > $o ).
tff(pred_def_16,type,
'less_eq$j': ( 'Nat_nat_prod_set$' * 'Nat_nat_prod_set$' ) > $o ).
tff(pred_def_17,type,
'less_eq$b': ( '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_18,type,
'fun_app$': ( 'A_run_bool_fun$' * 'A_run$' ) > $o ).
tff(pred_def_19,type,
'member$c': ( '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_20,type,
'fun_app$aj': ( 'A_constr_list_bool_fun$' * 'A_constr_list$' ) > $o ).
tff(pred_def_21,type,
'less_eq$i': ( '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_22,type,
'member$b': ( 'A_TESL_atomic_list_a_TESL_atomic_list_prod$' * 'A_TESL_atomic_list_a_TESL_atomic_list_prod_set$' ) > $o ).
tff(pred_def_23,type,
'less_eq$a': ( '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_24,type,
'fun_app$e': ( 'A_TESL_atomic_list_bool_fun$' * 'A_TESL_atomic_list$' ) > $o ).
tff(pred_def_27,type,
sP0: ( $int * $int * $int ) > $o ).
tff(pred_def_28,type,
sP1: ( $int * $int * $int ) > $o ).
tff(pred_def_29,type,
sP2: ( $int * $int * $int ) > $o ).
tff(pred_def_30,type,
sP3: ( '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$' ) > $o ).
tff(pred_def_31,type,
sP4: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).
tff(pred_def_32,type,
sP5: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).
tff(pred_def_33,type,
sP6: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).
tff(f13,conjecture,
'less_eq$'('fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))),'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_1$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_1$'),'n_1$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_1$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_1$'),1))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture12) ).
tff(f14,negated_conjecture,
~ 'less_eq$'('fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))),'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_1$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_1$'),'n_1$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_1$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_1$'),1))))),
inference(negated_conjecture,[status(cth)],[f13]) ).
tff(f17,negated_conjecture,
'fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$'))) = 'fun_app$c'('fun_app$d'('pair$','gamma$'),'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'('k_1$','k_2$'),'psi$')),'phi$'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom15) ).
tff(f66,axiom,
! [X0: 'A_run_set$',X1: 'A_run_set$'] :
( ! [X2: 'A_run$'] :
( 'member$'(X2,X0)
=> 'member$'(X2,X1) )
=> 'less_eq$'(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom64) ).
tff(f96,axiom,
! [X2: 'A_run_set$',X1: 'A_run_set$',X0: 'A_run_set$'] : ( 'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$',X0),X1)),X2) = 'fun_app$q'('fun_app$r'('inf$',X0),'fun_app$q'('fun_app$r'('inf$',X1),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom94) ).
tff(f196,negated_conjecture,
'fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$'))) = 'fun_app$c'('fun_app$d'('pair$','cons$a'('tickCntArith$'('tickCountLeq$'('k_2$','n$'),'tickCountLeq$'('k_1$','n$'),'case_prod$'('less_eq$f')),'gamma$')),'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','psi$'),'cons$'('weaklyPrecedes$'('k_1$','k_2$'),'phi$')))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom194) ).
tff(f204,axiom,
! [X3: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X1: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X0: 'A_constr_list$',X2: 'A_constr_list$'] :
( ( 'fun_app$c'('fun_app$d'('pair$',X0),X1) = 'fun_app$c'('fun_app$d'('pair$',X2),X3) )
<=> ( ( X1 = X3 )
& ( X0 = X2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom202) ).
tff(f236,negated_conjecture,
! [X1: 'A_run_set$',X0: 'A_run_set$'] : ( 'fun_app$q'('fun_app$r'('inf$',X0),X1) = 'collect$'('uug$'(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom234) ).
tff(f259,axiom,
! [X4: 'A_TESL_atomic_list$',X2: 'Clock$',X3: 'Clock$',X5: 'A_TESL_atomic_list$',X1: 'Nat$',X0: 'A_constr_list$'] : ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X0),'fun_app$k'('fun_app$l'('pair$b',X1),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'(X2,X3),X4)),X5)))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','cons$a'('tickCntArith$'('tickCountLeq$'(X3,X1),'tickCountLeq$'(X2,X1),'case_prod$'('less_eq$f')),X0)),'fun_app$k'('fun_app$l'('pair$b',X1),'fun_app$g'('fun_app$h'('pair$a',X4),'cons$'('weaklyPrecedes$'(X2,X3),X5))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom257) ).
tff(f289,axiom,
! [X3: 'A_TESL_atomic_list$',X2: 'A_TESL_atomic_list$',X0: 'A_constr_list$',X1: 'Nat$'] : ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X0),'fun_app$k'('fun_app$l'('pair$b',X1),'fun_app$g'('fun_app$h'('pair$a',X2),X3)))) = 'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'(X0)),'fun_app$s'('tESL_interpretation_stepwise$'(X2),X1))),'fun_app$s'('tESL_interpretation_stepwise$'(X3),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$',X1),1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom287) ).
tff(f961,plain,
! [X2: 'A_constr_list$',X3: 'Nat$',X0: 'A_TESL_atomic_list$',X1: 'A_TESL_atomic_list$'] : ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X2),'fun_app$k'('fun_app$l'('pair$b',X3),'fun_app$g'('fun_app$h'('pair$a',X1),X0)))) = 'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'(X2)),'fun_app$s'('tESL_interpretation_stepwise$'(X1),X3))),'fun_app$s'('tESL_interpretation_stepwise$'(X0),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$',X3),1)))) ),
inference(rectify,[],[f289]) ).
tff(f1101,plain,
! [X0: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X2: 'A_constr_list$',X1: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X3: 'A_constr_list$'] :
( ( ( X0 = X1 )
& ( X2 = X3 ) )
<=> ( 'fun_app$c'('fun_app$d'('pair$',X3),X0) = 'fun_app$c'('fun_app$d'('pair$',X2),X1) ) ),
inference(rectify,[],[f204]) ).
tff(f1110,plain,
! [X2: 'A_run_set$',X0: 'A_run_set$',X1: 'A_run_set$'] : ( 'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$',X2),X1)),X0) = 'fun_app$q'('fun_app$r'('inf$',X2),'fun_app$q'('fun_app$r'('inf$',X1),X0)) ),
inference(rectify,[],[f96]) ).
tff(f1188,plain,
! [X1: 'A_run_set$',X0: 'A_run_set$'] : ( 'fun_app$q'('fun_app$r'('inf$',X1),X0) = 'collect$'('uug$'(X1,X0)) ),
inference(rectify,[],[f236]) ).
tff(f1256,plain,
~ 'less_eq$'('fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))),'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_1$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_1$'),'n_1$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_1$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_1$'),1))))),
inference(flattening,[],[f14]) ).
tff(f1284,plain,
! [X0: 'A_TESL_atomic_list$',X3: 'A_TESL_atomic_list$',X4: 'Nat$',X5: 'A_constr_list$',X2: 'Clock$',X1: 'Clock$'] : ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','cons$a'('tickCntArith$'('tickCountLeq$'(X2,X4),'tickCountLeq$'(X1,X4),'case_prod$'('less_eq$f')),X5)),'fun_app$k'('fun_app$l'('pair$b',X4),'fun_app$g'('fun_app$h'('pair$a',X0),'cons$'('weaklyPrecedes$'(X1,X2),X3))))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X5),'fun_app$k'('fun_app$l'('pair$b',X4),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'(X1,X2),X0)),X3)))) ),
inference(rectify,[],[f259]) ).
tff(f1736,plain,
! [X0: 'A_run_set$',X1: 'A_run_set$'] :
( 'less_eq$'(X0,X1)
| ? [X2: 'A_run$'] :
( ~ 'member$'(X2,X1)
& 'member$'(X2,X0) ) ),
inference(ennf_transformation,[],[f66]) ).
tff(f1841,plain,
! [X0: 'A_TESL_atomic_list$',X1: 'A_TESL_atomic_list$',X2: 'Nat$',X3: 'A_constr_list$',X4: 'Clock$',X5: 'Clock$'] : ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X3),'fun_app$k'('fun_app$l'('pair$b',X2),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'(X5,X4),X0)),X1)))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','cons$a'('tickCntArith$'('tickCountLeq$'(X4,X2),'tickCountLeq$'(X5,X2),'case_prod$'('less_eq$f')),X3)),'fun_app$k'('fun_app$l'('pair$b',X2),'fun_app$g'('fun_app$h'('pair$a',X0),'cons$'('weaklyPrecedes$'(X5,X4),X1))))) ),
inference(rectify,[],[f1284]) ).
tff(f1856,plain,
! [X0: 'A_constr_list$',X1: 'Nat$',X2: 'A_TESL_atomic_list$',X3: 'A_TESL_atomic_list$'] : ( 'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'(X0)),'fun_app$s'('tESL_interpretation_stepwise$'(X3),X1))),'fun_app$s'('tESL_interpretation_stepwise$'(X2),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$',X1),1)))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X0),'fun_app$k'('fun_app$l'('pair$b',X1),'fun_app$g'('fun_app$h'('pair$a',X3),X2)))) ),
inference(rectify,[],[f961]) ).
tff(f1890,plain,
! [X0: 'A_run_set$',X1: 'A_run_set$',X2: 'A_run_set$'] : ( 'fun_app$q'('fun_app$r'('inf$',X0),'fun_app$q'('fun_app$r'('inf$',X2),X1)) = 'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$',X0),X2)),X1) ),
inference(rectify,[],[f1110]) ).
tff(f1964,plain,
! [X0: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X2: 'A_constr_list$',X1: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X3: 'A_constr_list$'] :
( ( ( ( X0 = X1 )
& ( X2 = X3 ) )
| ( 'fun_app$c'('fun_app$d'('pair$',X3),X0) != 'fun_app$c'('fun_app$d'('pair$',X2),X1) ) )
& ( ( 'fun_app$c'('fun_app$d'('pair$',X3),X0) = 'fun_app$c'('fun_app$d'('pair$',X2),X1) )
| ( X0 != X1 )
| ( X2 != X3 ) ) ),
inference(nnf_transformation,[],[f1101]) ).
tff(f1965,plain,
! [X0: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X2: 'A_constr_list$',X1: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X3: 'A_constr_list$'] :
( ( ( ( X0 = X1 )
& ( X2 = X3 ) )
| ( 'fun_app$c'('fun_app$d'('pair$',X3),X0) != 'fun_app$c'('fun_app$d'('pair$',X2),X1) ) )
& ( ( 'fun_app$c'('fun_app$d'('pair$',X3),X0) = 'fun_app$c'('fun_app$d'('pair$',X2),X1) )
| ( X0 != X1 )
| ( X2 != X3 ) ) ),
inference(flattening,[],[f1964]) ).
tff(f1966,plain,
! [X0: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X1: 'A_constr_list$',X2: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X3: 'A_constr_list$'] :
( ( ( ( X0 = X2 )
& ( X1 = X3 ) )
| ( 'fun_app$c'('fun_app$d'('pair$',X1),X2) != 'fun_app$c'('fun_app$d'('pair$',X3),X0) ) )
& ( ( 'fun_app$c'('fun_app$d'('pair$',X1),X2) = 'fun_app$c'('fun_app$d'('pair$',X3),X0) )
| ( X0 != X2 )
| ( X1 != X3 ) ) ),
inference(rectify,[],[f1965]) ).
tff(f2474,plain,
! [X0: 'A_run_set$',X1: 'A_run_set$'] :
( 'less_eq$'(X0,X1)
| ( ~ 'member$'(sK318(X0,X1),X1)
& 'member$'(sK318(X0,X1),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK318]),skolemize(X2,sK318(X0,X1))],[f1736]) ).
tff(f2592,plain,
! [X0: 'A_run_set$',X1: 'A_run_set$'] : ( 'fun_app$q'('fun_app$r'('inf$',X0),X1) = 'collect$'('uug$'(X0,X1)) ),
inference(rectify,[],[f1188]) ).
tff(f2662,plain,
! [X2: 'Nat$',X3: 'A_constr_list$',X0: 'A_TESL_atomic_list$',X1: 'A_TESL_atomic_list$',X4: 'Clock$',X5: 'Clock$'] : ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X3),'fun_app$k'('fun_app$l'('pair$b',X2),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'(X5,X4),X0)),X1)))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','cons$a'('tickCntArith$'('tickCountLeq$'(X4,X2),'tickCountLeq$'(X5,X2),'case_prod$'('less_eq$f')),X3)),'fun_app$k'('fun_app$l'('pair$b',X2),'fun_app$g'('fun_app$h'('pair$a',X0),'cons$'('weaklyPrecedes$'(X5,X4),X1))))) ),
inference(cnf_transformation,[],[f1841]) ).
tff(f2679,plain,
~ 'less_eq$'('fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))),'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_1$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_1$'),'n_1$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_1$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_1$'),1))))),
inference(cnf_transformation,[],[f1256]) ).
tff(f2684,plain,
! [X2: 'A_TESL_atomic_list$',X3: 'A_TESL_atomic_list$',X0: 'A_constr_list$',X1: 'Nat$'] : ( 'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'(X0)),'fun_app$s'('tESL_interpretation_stepwise$'(X3),X1))),'fun_app$s'('tESL_interpretation_stepwise$'(X2),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$',X1),1)))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X0),'fun_app$k'('fun_app$l'('pair$b',X1),'fun_app$g'('fun_app$h'('pair$a',X3),X2)))) ),
inference(cnf_transformation,[],[f1856]) ).
tff(f2721,plain,
! [X2: 'A_run_set$',X0: 'A_run_set$',X1: 'A_run_set$'] : ( 'fun_app$q'('fun_app$r'('inf$',X0),'fun_app$q'('fun_app$r'('inf$',X2),X1)) = 'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$',X0),X2)),X1) ),
inference(cnf_transformation,[],[f1890]) ).
tff(f2821,plain,
! [X2: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X3: 'A_constr_list$',X0: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X1: 'A_constr_list$'] :
( ( 'fun_app$c'('fun_app$d'('pair$',X1),X2) != 'fun_app$c'('fun_app$d'('pair$',X3),X0) )
| ( X1 = X3 ) ),
inference(cnf_transformation,[],[f1966]) ).
tff(f2822,plain,
! [X2: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X3: 'A_constr_list$',X0: 'Nat_a_TESL_atomic_list_a_TESL_atomic_list_prod_prod$',X1: 'A_constr_list$'] :
( ( 'fun_app$c'('fun_app$d'('pair$',X1),X2) != 'fun_app$c'('fun_app$d'('pair$',X3),X0) )
| ( X0 = X2 ) ),
inference(cnf_transformation,[],[f1966]) ).
tff(f3244,plain,
'fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$'))) = 'fun_app$c'('fun_app$d'('pair$','cons$a'('tickCntArith$'('tickCountLeq$'('k_2$','n$'),'tickCountLeq$'('k_1$','n$'),'case_prod$'('less_eq$f')),'gamma$')),'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','psi$'),'cons$'('weaklyPrecedes$'('k_1$','k_2$'),'phi$')))),
inference(cnf_transformation,[],[f196]) ).
tff(f3254,plain,
'fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$'))) = 'fun_app$c'('fun_app$d'('pair$','gamma$'),'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'('k_1$','k_2$'),'psi$')),'phi$'))),
inference(cnf_transformation,[],[f17]) ).
tff(f3469,plain,
! [X0: 'A_run_set$',X1: 'A_run_set$'] :
( 'member$'(sK318(X0,X1),X0)
| 'less_eq$'(X0,X1) ),
inference(cnf_transformation,[],[f2474]) ).
tff(f3470,plain,
! [X0: 'A_run_set$',X1: 'A_run_set$'] :
( ~ 'member$'(sK318(X0,X1),X1)
| 'less_eq$'(X0,X1) ),
inference(cnf_transformation,[],[f2474]) ).
tff(f3627,plain,
! [X0: 'A_run_set$',X1: 'A_run_set$'] : ( 'fun_app$q'('fun_app$r'('inf$',X0),X1) = 'collect$'('uug$'(X0,X1)) ),
inference(cnf_transformation,[],[f2592]) ).
tff(f3995,definition,
( spl392_2
<=> 'less_eq$'('fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))),'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_1$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_1$'),'n_1$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_1$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_1$'),1))))) ),
introduced(definition,[new_symbols(definition,[spl392_2])],[avatar_definition]) ).
tff(f3996,plain,
( ~ 'less_eq$'('fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))),'fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_1$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_1$'),'n_1$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_1$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_1$'),1)))))
| spl392_2 ),
inference(avatar_component_clause,[],[f3995]) ).
tff(f3997,plain,
~ spl392_2,
inference(avatar_split_clause,[],[f2679,f3995]) ).
tff(f4018,definition,
( spl392_6
<=> ( 'fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$'))) = 'fun_app$c'('fun_app$d'('pair$','cons$a'('tickCntArith$'('tickCountLeq$'('k_2$','n$'),'tickCountLeq$'('k_1$','n$'),'case_prod$'('less_eq$f')),'gamma$')),'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','psi$'),'cons$'('weaklyPrecedes$'('k_1$','k_2$'),'phi$')))) ) ),
introduced(definition,[new_symbols(definition,[spl392_6])],[avatar_definition]) ).
tff(f4019,plain,
( ( 'fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$'))) = 'fun_app$c'('fun_app$d'('pair$','cons$a'('tickCntArith$'('tickCountLeq$'('k_2$','n$'),'tickCountLeq$'('k_1$','n$'),'case_prod$'('less_eq$f')),'gamma$')),'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','psi$'),'cons$'('weaklyPrecedes$'('k_1$','k_2$'),'phi$')))) )
| ~ spl392_6 ),
inference(avatar_component_clause,[],[f4018]) ).
tff(f4020,plain,
spl392_6,
inference(avatar_split_clause,[],[f3244,f4018]) ).
tff(f4021,plain,
! [X2: 'A_TESL_atomic_list$',X3: 'A_TESL_atomic_list$',X0: 'A_constr_list$',X1: 'Nat$'] : ( 'fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'(X0)),'fun_app$q'('fun_app$r'('inf$','fun_app$s'('tESL_interpretation_stepwise$'(X3),X1)),'fun_app$s'('tESL_interpretation_stepwise$'(X2),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$',X1),1))))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X0),'fun_app$k'('fun_app$l'('pair$b',X1),'fun_app$g'('fun_app$h'('pair$a',X3),X2)))) ),
inference(forward_demodulation,[],[f2684,f2721]) ).
tff(f4031,definition,
( spl392_8
<=> ( 'fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$'))) = 'fun_app$c'('fun_app$d'('pair$','gamma$'),'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'('k_1$','k_2$'),'psi$')),'phi$'))) ) ),
introduced(definition,[new_symbols(definition,[spl392_8])],[avatar_definition]) ).
tff(f4032,plain,
( ( 'fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$'))) = 'fun_app$c'('fun_app$d'('pair$','gamma$'),'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'('k_1$','k_2$'),'psi$')),'phi$'))) )
| ~ spl392_8 ),
inference(avatar_component_clause,[],[f4031]) ).
tff(f4033,plain,
spl392_8,
inference(avatar_split_clause,[],[f3254,f4031]) ).
tff(f4063,plain,
! [X2: 'A_TESL_atomic_list$',X3: 'A_TESL_atomic_list$',X0: 'A_constr_list$',X1: 'Nat$'] : ( 'collect$'('uug$'('symbolic_run_interpretation$'(X0),'fun_app$q'('fun_app$r'('inf$','fun_app$s'('tESL_interpretation_stepwise$'(X3),X1)),'fun_app$s'('tESL_interpretation_stepwise$'(X2),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$',X1),1)))))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X0),'fun_app$k'('fun_app$l'('pair$b',X1),'fun_app$g'('fun_app$h'('pair$a',X3),X2)))) ),
inference(forward_demodulation,[],[f4021,f3627]) ).
tff(f4079,plain,
! [X2: 'A_TESL_atomic_list$',X3: 'A_TESL_atomic_list$',X0: 'A_constr_list$',X1: 'Nat$'] : ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$',X0),'fun_app$k'('fun_app$l'('pair$b',X1),'fun_app$g'('fun_app$h'('pair$a',X3),X2)))) = 'collect$'('uug$'('symbolic_run_interpretation$'(X0),'collect$'('uug$'('fun_app$s'('tESL_interpretation_stepwise$'(X3),X1),'fun_app$s'('tESL_interpretation_stepwise$'(X2),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$',X1),1))))))) ),
inference(forward_demodulation,[],[f4063,f3627]) ).
tff(f4086,plain,
( ~ 'less_eq$'('fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))),'fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_1$')),'fun_app$q'('fun_app$r'('inf$','fun_app$s'('tESL_interpretation_stepwise$'('psi_1$'),'n_1$')),'fun_app$s'('tESL_interpretation_stepwise$'('phi_1$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_1$'),1))))))
| spl392_2 ),
inference(forward_demodulation,[],[f3996,f2721]) ).
tff(f4087,plain,
( ~ 'less_eq$'('fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))),'collect$'('uug$'('symbolic_run_interpretation$'('gamma_1$'),'fun_app$q'('fun_app$r'('inf$','fun_app$s'('tESL_interpretation_stepwise$'('psi_1$'),'n_1$')),'fun_app$s'('tESL_interpretation_stepwise$'('phi_1$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_1$'),1)))))))
| spl392_2 ),
inference(forward_demodulation,[],[f4086,f3627]) ).
tff(f4088,plain,
( ~ 'less_eq$'('fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))),'collect$'('uug$'('symbolic_run_interpretation$'('gamma_1$'),'collect$'('uug$'('fun_app$s'('tESL_interpretation_stepwise$'('psi_1$'),'n_1$'),'fun_app$s'('tESL_interpretation_stepwise$'('phi_1$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_1$'),1))))))))
| spl392_2 ),
inference(forward_demodulation,[],[f4087,f3627]) ).
tff(f4089,plain,
( ~ 'less_eq$'('fun_app$q'('fun_app$r'('inf$','fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'))),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')))))
| spl392_2 ),
inference(forward_demodulation,[],[f4088,f4079]) ).
tff(f4090,plain,
( ~ 'less_eq$'('fun_app$q'('fun_app$r'('inf$','symbolic_run_interpretation$'('gamma_2$')),'fun_app$q'('fun_app$r'('inf$','fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1))))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')))))
| spl392_2 ),
inference(forward_demodulation,[],[f4089,f2721]) ).
tff(f4091,plain,
( ~ 'less_eq$'('collect$'('uug$'('symbolic_run_interpretation$'('gamma_2$'),'fun_app$q'('fun_app$r'('inf$','fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$')),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1)))))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')))))
| spl392_2 ),
inference(forward_demodulation,[],[f4090,f3627]) ).
tff(f4092,plain,
( ~ 'less_eq$'('collect$'('uug$'('symbolic_run_interpretation$'('gamma_2$'),'collect$'('uug$'('fun_app$s'('tESL_interpretation_stepwise$'('psi_2$'),'n_2$'),'fun_app$s'('tESL_interpretation_stepwise$'('phi_2$'),'fun_app$t'('nat$',$sum('fun_app$u'('of_nat$','n_2$'),1))))))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')))))
| spl392_2 ),
inference(forward_demodulation,[],[f4091,f3627]) ).
tff(f4093,plain,
( ~ 'less_eq$'('heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')))))
| spl392_2 ),
inference(forward_demodulation,[],[f4092,f4079]) ).
tff(f4095,definition,
( spl392_11
<=> 'less_eq$'('heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$'))))) ),
introduced(definition,[new_symbols(definition,[spl392_11])],[avatar_definition]) ).
tff(f4096,plain,
( ~ 'less_eq$'('heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')))))
| spl392_11 ),
inference(avatar_component_clause,[],[f4095]) ).
tff(f4097,plain,
( ~ spl392_11
| spl392_2 ),
inference(avatar_split_clause,[],[f4093,f3995,f4095]) ).
tff(f4560,plain,
( 'member$'(sK318('heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$'))))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))))
| spl392_11 ),
inference(unit_resulting_resolution,[],[f3469,f4096]) ).
tff(f4563,definition,
( spl392_21
<=> 'member$'(sK318('heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$'))))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$'))))) ),
introduced(definition,[new_symbols(definition,[spl392_21])],[avatar_definition]) ).
tff(f4565,plain,
( spl392_21
| spl392_11 ),
inference(avatar_split_clause,[],[f4560,f4095,f4563]) ).
tff(f4566,plain,
( ~ 'member$'(sK318('heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$'))))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')))))
| spl392_11 ),
inference(unit_resulting_resolution,[],[f3470,f4096]) ).
tff(f4571,definition,
( spl392_22
<=> 'member$'(sK318('heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$'))))),'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$'))))) ),
introduced(definition,[new_symbols(definition,[spl392_22])],[avatar_definition]) ).
tff(f4573,plain,
( ~ spl392_22
| spl392_11 ),
inference(avatar_split_clause,[],[f4566,f4095,f4571]) ).
tff(f7586,plain,
( ( 'gamma_1$' = 'gamma$' )
| ~ spl392_8 ),
inference(unit_resulting_resolution,[],[f2821,f4032]) ).
tff(f7612,definition,
( spl392_31
<=> ( 'gamma_1$' = 'gamma$' ) ),
introduced(definition,[new_symbols(definition,[spl392_31])],[avatar_definition]) ).
tff(f7613,plain,
( ( 'gamma_1$' = 'gamma$' )
| ~ spl392_31 ),
inference(avatar_component_clause,[],[f7612]) ).
tff(f7614,plain,
( spl392_31
| ~ spl392_8 ),
inference(avatar_split_clause,[],[f7586,f4031,f7612]) ).
tff(f7620,plain,
( ( 'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')) = 'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'('k_1$','k_2$'),'psi$')),'phi$')) )
| ~ spl392_8 ),
inference(unit_resulting_resolution,[],[f2822,f4032]) ).
tff(f7641,definition,
( spl392_33
<=> ( 'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')) = 'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'('k_1$','k_2$'),'psi$')),'phi$')) ) ),
introduced(definition,[new_symbols(definition,[spl392_33])],[avatar_definition]) ).
tff(f7643,plain,
( spl392_33
| ~ spl392_8 ),
inference(avatar_split_clause,[],[f7620,f4031,f7641]) ).
tff(f21243,plain,
( ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma$'),'fun_app$k'('fun_app$l'('pair$b','n$'),'fun_app$g'('fun_app$h'('pair$a','cons$'('weaklyPrecedes$'('k_1$','k_2$'),'psi$')),'phi$')))) )
| ~ spl392_6 ),
inference(superposition,[],[f2662,f4019]) ).
tff(f21247,plain,
( ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_1$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))) )
| ~ spl392_6
| ~ spl392_8 ),
inference(forward_demodulation,[],[f21243,f4032]) ).
tff(f21249,plain,
( ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))) )
| ~ spl392_6
| ~ spl392_8
| ~ spl392_31 ),
inference(forward_demodulation,[],[f21247,f7613]) ).
tff(f21251,definition,
( spl392_71
<=> ( 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma$'),'fun_app$k'('fun_app$l'('pair$b','n_1$'),'fun_app$g'('fun_app$h'('pair$a','psi_1$'),'phi_1$')))) = 'heronConf_interpretation$'('fun_app$c'('fun_app$d'('pair$','gamma_2$'),'fun_app$k'('fun_app$l'('pair$b','n_2$'),'fun_app$g'('fun_app$h'('pair$a','psi_2$'),'phi_2$')))) ) ),
introduced(definition,[new_symbols(definition,[spl392_71])],[avatar_definition]) ).
tff(f21253,plain,
( spl392_71
| ~ spl392_6
| ~ spl392_8
| ~ spl392_31 ),
inference(avatar_split_clause,[],[f21249,f7612,f4031,f4018,f21251]) ).
tff(f21254,plain,
$false,
inference(avatar_smt_refutation,[],[f21253,f7643,f7614,f4573,f4565,f4097,f4033,f4020,f3997]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ITP412_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.05/0.31 % Computer : n012.cluster.edu
% 0.05/0.31 % Model : x86_64 x86_64
% 0.05/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.31 % Memory : 8046.5625MB
% 0.05/0.31 % OS : Linux 6.8.0-71-generic
% 0.05/0.31 % CPULimit : 300
% 0.05/0.31 % WCLimit : 300
% 0.05/0.31 % DateTime : Sun Sep 27 12:57:19 UTC 2026
% 0.05/0.31 % CPUTime :
% 0.05/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.33 Running first-order theorem proving
% 0.08/0.33 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.46/0.89 % (2370469)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 1.46/0.89 % (2370538)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3500678951:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 1.46/0.89 % (2370536)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=282933552:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 1.46/0.89 % (2370534)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1685481195:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 1.46/0.89 % (2370539)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1105349088:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 1.46/0.89 % (2370535)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=717606454:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 1.46/0.89 % (2370532)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1183480410:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 1.46/0.89 % (2370538)Instruction limit reached!
% 1.46/0.89 % (2370538)------------------------------
% 1.46/0.89 % (2370538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.46/0.89 % (2370538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.89 % (2370538)CaDiCaL version: 2.1.3
% 1.46/0.89 % (2370538)Termination reason: Instruction limit
% 1.46/0.89 % (2370538)Termination phase: Property scanning
% 1.46/0.89 % (2370538)Time elapsed: 0.002 s
% 1.46/0.89 % (2370538)Peak memory usage: 86 MB
% 1.46/0.89 % (2370538)Instructions burned: 6 (million)
% 1.46/0.89 % (2370536)Instruction limit reached!
% 1.46/0.89 % (2370536)------------------------------
% 1.46/0.89 % (2370536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.46/0.89 % (2370536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.89 % (2370536)CaDiCaL version: 2.1.3
% 1.46/0.89 % (2370536)Termination reason: Instruction limit
% 1.46/0.89 % (2370536)Termination phase: Property scanning
% 1.46/0.89 % (2370536)Time elapsed: 0.003 s
% 1.46/0.89 % (2370536)Peak memory usage: 86 MB
% 1.46/0.89 % (2370536)Instructions burned: 11 (million)
% 1.46/0.89 % (2370532)Instruction limit reached!
% 1.46/0.89 % (2370532)------------------------------
% 1.46/0.89 % (2370532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.46/0.89 % (2370532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.89 % (2370532)CaDiCaL version: 2.1.3
% 1.46/0.89 % (2370532)Termination reason: Instruction limit
% 1.46/0.89 % (2370532)Termination phase: Property scanning
% 1.46/0.89 % (2370532)Time elapsed: 0.004 s
% 1.46/0.89 % (2370532)Peak memory usage: 86 MB
% 1.46/0.89 % (2370532)Instructions burned: 16 (million)
% 1.46/0.89 % (2370540)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1334423144:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 1.46/0.89 % (2370539)Instruction limit reached!
% 1.46/0.89 % (2370539)------------------------------
% 1.46/0.89 % (2370539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.46/0.89 % (2370539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.89 % (2370539)CaDiCaL version: 2.1.3
% 1.46/0.89 % (2370539)Termination reason: Instruction limit
% 1.46/0.89 % (2370539)Termination phase: Property scanning
% 1.46/0.89 % (2370539)Time elapsed: 0.015 s
% 1.46/0.89 % (2370539)Peak memory usage: 88 MB
% 1.46/0.89 % (2370539)Instructions burned: 49 (million)
% 1.46/0.89 % (2370540)Instruction limit reached!
% 1.46/0.89 % (2370540)------------------------------
% 1.46/0.89 % (2370540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.46/0.89 % (2370540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.89 % (2370540)CaDiCaL version: 2.1.3
% 1.46/0.89 % (2370540)Termination reason: Instruction limit
% 1.46/0.89 % (2370540)Termination phase: Preprocessing 3
% 1.46/0.89 % (2370540)Time elapsed: 0.011 s
% 1.46/0.89 % (2370540)Peak memory usage: 88 MB
% 1.46/0.89 % (2370540)Instructions burned: 35 (million)
% 1.46/0.89 % (2370535)Instruction limit reached!
% 1.46/0.89 % (2370535)------------------------------
% 1.46/0.89 % (2370535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.46/0.89 % (2370535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.99 % (2370535)CaDiCaL version: 2.1.3
% 2.14/0.99 % (2370535)Termination reason: Instruction limit
% 2.14/0.99 % (2370535)Termination phase: Saturation
% 2.14/0.99 % (2370535)Time elapsed: 0.080 s
% 2.14/0.99 % (2370535)Peak memory usage: 119 MB
% 2.14/0.99 % (2370535)Instructions burned: 201 (million)
% 2.14/0.99 % (2370588)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=2499173193:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 2.14/0.99 % (2370586)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2292978577:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.14/0.99 % (2370590)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1885294966:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 2.14/0.99 % (2370586)Instruction limit reached!
% 2.14/0.99 % (2370586)------------------------------
% 2.14/0.99 % (2370586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.14/0.99 % (2370586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.99 % (2370586)CaDiCaL version: 2.1.3
% 2.14/0.99 % (2370586)Termination reason: Instruction limit
% 2.14/0.99 % (2370586)Termination phase: SInE selection
% 2.14/0.99 % (2370586)Time elapsed: 0.004 s
% 2.14/0.99 % (2370586)Peak memory usage: 86 MB
% 2.14/0.99 % (2370586)Instructions burned: 14 (million)
% 2.14/0.99 % (2370590)Instruction limit reached!
% 2.14/0.99 % (2370590)------------------------------
% 2.14/0.99 % (2370590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.14/0.99 % (2370590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.99 % (2370590)CaDiCaL version: 2.1.3
% 2.14/0.99 % (2370590)Termination reason: Instruction limit
% 2.14/0.99 % (2370590)Termination phase: Preprocessing 1
% 2.14/0.99 % (2370590)Time elapsed: 0.005 s
% 2.14/0.99 % (2370590)Peak memory usage: 86 MB
% 2.14/0.99 % (2370590)Instructions burned: 17 (million)
% 2.14/0.99 % (2370588)Instruction limit reached!
% 2.14/0.99 % (2370588)------------------------------
% 2.14/0.99 % (2370588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.14/0.99 % (2370588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.99 % (2370588)CaDiCaL version: 2.1.3
% 2.14/0.99 % (2370588)Termination reason: Instruction limit
% 2.14/0.99 % (2370588)Termination phase: Preprocessing 3
% 2.14/0.99 % (2370588)Time elapsed: 0.009 s
% 2.14/0.99 % (2370588)Peak memory usage: 87 MB
% 2.14/0.99 % (2370588)Instructions burned: 30 (million)
% 2.14/0.99 % (2370593)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=2070682907:i=27:canc=cautious:fsr=off:rtra=on_2998 on theBenchmark for (2998ds/27Mi)
% 2.14/0.99 % (2370592)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=281410692:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 2.14/0.99 % (2370593)Instruction limit reached!
% 2.14/0.99 % (2370593)------------------------------
% 2.14/0.99 % (2370593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.14/0.99 % (2370593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.99 % (2370593)CaDiCaL version: 2.1.3
% 2.14/0.99 % (2370593)Termination reason: Instruction limit
% 2.14/0.99 % (2370593)Termination phase: Preprocessing 2
% 2.14/0.99 % (2370593)Time elapsed: 0.008 s
% 2.14/0.99 % (2370593)Peak memory usage: 87 MB
% 2.14/0.99 % (2370593)Instructions burned: 27 (million)
% 2.14/0.99 % (2370592)Instruction limit reached!
% 2.14/0.99 % (2370592)------------------------------
% 2.14/0.99 % (2370592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.14/0.99 % (2370592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.99 % (2370592)CaDiCaL version: 2.1.3
% 2.14/0.99 % (2370592)Termination reason: Instruction limit
% 2.14/0.99 % (2370592)Termination phase: Preprocessing 1
% 2.14/0.99 % (2370592)Time elapsed: 0.007 s
% 2.14/0.99 % (2370592)Peak memory usage: 86 MB
% 2.14/0.99 % (2370592)Instructions burned: 24 (million)
% 2.14/0.99 % (2370534)Instruction limit reached!
% 2.14/0.99 % (2370534)------------------------------
% 2.14/0.99 % (2370534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.14/0.99 % (2370534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/1.09 % (2370534)CaDiCaL version: 2.1.3
% 3.25/1.09 % (2370534)Termination reason: Instruction limit
% 3.25/1.09 % (2370534)Termination phase: Saturation
% 3.25/1.09 % (2370534)Time elapsed: 0.123 s
% 3.25/1.09 % (2370534)Peak memory usage: 120 MB
% 3.25/1.09 % (2370534)Instructions burned: 308 (million)
% 3.25/1.09 % (2370611)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3828344440:i=85:gtgl=4:rtra=on:gtg=exists_sym_2998 on theBenchmark for (2998ds/85Mi)
% 3.25/1.09 % (2370622)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=913045368:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi)
% 3.25/1.09 % (2370620)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=70918713:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 3.25/1.09 % (2370620)Instruction limit reached!
% 3.25/1.09 % (2370620)------------------------------
% 3.25/1.09 % (2370620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.25/1.09 % (2370620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/1.09 % (2370620)CaDiCaL version: 2.1.3
% 3.25/1.09 % (2370620)Termination reason: Instruction limit
% 3.25/1.09 % (2370620)Termination phase: Property scanning
% 3.25/1.09 % (2370620)Time elapsed: 0.002 s
% 3.25/1.09 % (2370620)Peak memory usage: 85 MB
% 3.25/1.09 % (2370620)Instructions burned: 6 (million)
% 3.25/1.09 % (2370625)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1967520245:i=4:ep=RST:ins=2:rtra=on_2997 on theBenchmark for (2997ds/4Mi)
% 3.25/1.09 % (2370625)Instruction limit reached!
% 3.25/1.09 % (2370625)------------------------------
% 3.25/1.09 % (2370625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.25/1.09 % (2370625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/1.09 % (2370625)CaDiCaL version: 2.1.3
% 3.25/1.09 % (2370625)Termination reason: Instruction limit
% 3.25/1.09 % (2370625)Termination phase: Property scanning
% 3.25/1.09 % (2370625)Time elapsed: 0.002 s
% 3.25/1.09 % (2370625)Peak memory usage: 86 MB
% 3.25/1.09 % (2370625)Instructions burned: 6 (million)
% 3.25/1.09 % (2370611)Instruction limit reached!
% 3.25/1.09 % (2370611)------------------------------
% 3.25/1.09 % (2370611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.25/1.09 % (2370611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/1.09 % (2370611)CaDiCaL version: 2.1.3
% 3.25/1.09 % (2370611)Termination reason: Instruction limit
% 3.25/1.09 % (2370611)Termination phase: Property scanning
% 3.25/1.09 % (2370611)Time elapsed: 0.025 s
% 3.25/1.09 % (2370611)Peak memory usage: 89 MB
% 3.25/1.09 % (2370611)Instructions burned: 85 (million)
% 3.25/1.09 % (2370629)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2179292459:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2997 on theBenchmark for (2997ds/66Mi)
% 3.25/1.09 % (2370632)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=2472467649:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2997 on theBenchmark for (2997ds/8Mi)
% 3.25/1.09 % (2370632)Instruction limit reached!
% 3.25/1.09 % (2370632)------------------------------
% 3.25/1.09 % (2370632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.25/1.09 % (2370632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/1.09 % (2370632)CaDiCaL version: 2.1.3
% 3.25/1.09 % (2370632)Termination reason: Instruction limit
% 3.25/1.09 % (2370632)Termination phase: shuffling
% 3.25/1.09 % (2370632)Time elapsed: 0.003 s
% 3.25/1.09 % (2370632)Peak memory usage: 86 MB
% 3.25/1.09 % (2370632)Instructions burned: 10 (million)
% 3.25/1.09 % (2370631)lrs+10_1_thi=all:si=on:fd=off:random_seed=1475464825:i=53:rtra=on:gtg=all_2997 on theBenchmark for (2997ds/53Mi)
% 3.25/1.09 % (2370629)Instruction limit reached!
% 3.25/1.09 % (2370629)------------------------------
% 3.25/1.09 % (2370629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.25/1.09 % (2370629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/1.09 % (2370629)CaDiCaL version: 2.1.3
% 3.25/1.09 % (2370629)Termination reason: Instruction limit
% 3.25/1.09 % (2370629)Termination phase: Property scanning
% 3.25/1.09 % (2370629)Time elapsed: 0.021 s
% 3.25/1.09 % (2370629)Peak memory usage: 89 MB
% 3.96/1.22 % (2370629)Instructions burned: 70 (million)
% 3.96/1.22 % (2370631)Instruction limit reached!
% 3.96/1.22 % (2370631)------------------------------
% 3.96/1.22 % (2370631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.22 % (2370631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.22 % (2370631)CaDiCaL version: 2.1.3
% 3.96/1.22 % (2370631)Termination reason: Instruction limit
% 3.96/1.22 % (2370631)Termination phase: Preprocessing 3
% 3.96/1.22 % (2370631)Time elapsed: 0.016 s
% 3.96/1.22 % (2370631)Peak memory usage: 88 MB
% 3.96/1.22 % (2370631)Instructions burned: 54 (million)
% 3.96/1.22 % (2370622)Instruction limit reached!
% 3.96/1.22 % (2370622)------------------------------
% 3.96/1.22 % (2370622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.22 % (2370622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.22 % (2370622)CaDiCaL version: 2.1.3
% 3.96/1.22 % (2370622)Termination reason: Instruction limit
% 3.96/1.22 % (2370622)Termination phase: Saturation
% 3.96/1.22 % (2370622)Time elapsed: 0.067 s
% 3.96/1.22 % (2370622)Peak memory usage: 92 MB
% 3.96/1.22 % (2370622)Instructions burned: 181 (million)
% 3.96/1.22 % (2370651)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3098299012:i=127:doe=on:rtra=on_2996 on theBenchmark for (2996ds/127Mi)
% 3.96/1.22 % (2370648)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3676512077:st=3:i=2:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/2Mi)
% 3.96/1.22 % (2370648)Instruction limit reached!
% 3.96/1.22 % (2370648)------------------------------
% 3.96/1.22 % (2370648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.22 % (2370648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.22 % (2370648)CaDiCaL version: 2.1.3
% 3.96/1.22 % (2370648)Termination reason: Instruction limit
% 3.96/1.22 % (2370648)Termination phase: Property scanning
% 3.96/1.22 % (2370648)Time elapsed: 0.002 s
% 3.96/1.22 % (2370648)Peak memory usage: 86 MB
% 3.96/1.22 % (2370648)Instructions burned: 5 (million)
% 3.96/1.22 % (2370649)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1401698794:i=2:doe=on:canc=force:asg=cautious:rtra=on_2997 on theBenchmark for (2997ds/2Mi)
% 3.96/1.22 % (2370649)Instruction limit reached!
% 3.96/1.22 % (2370649)------------------------------
% 3.96/1.22 % (2370649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.22 % (2370649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.22 % (2370649)CaDiCaL version: 2.1.3
% 3.96/1.22 % (2370649)Termination reason: Instruction limit
% 3.96/1.22 % (2370649)Termination phase: Property scanning
% 3.96/1.22 % (2370649)Time elapsed: 0.002 s
% 3.96/1.22 % (2370649)Peak memory usage: 86 MB
% 3.96/1.22 % (2370649)Instructions burned: 6 (million)
% 3.96/1.22 % (2370655)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=469451027:i=26:canc=cautious:av=off:rtra=on_2996 on theBenchmark for (2996ds/26Mi)
% 3.96/1.22 % (2370654)dis+10_1_si=on:random_seed=957267810:i=10:ep=R:rtra=on_2996 on theBenchmark for (2996ds/10Mi)
% 3.96/1.22 % (2370655)Instruction limit reached!
% 3.96/1.22 % (2370655)------------------------------
% 3.96/1.22 % (2370655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.22 % (2370655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.22 % (2370655)CaDiCaL version: 2.1.3
% 3.96/1.22 % (2370655)Termination reason: Instruction limit
% 3.96/1.22 % (2370655)Termination phase: shuffling
% 3.96/1.22 % (2370655)Time elapsed: 0.008 s
% 3.96/1.22 % (2370655)Peak memory usage: 87 MB
% 3.96/1.22 % (2370655)Instructions burned: 27 (million)
% 3.96/1.22 % (2370654)Instruction limit reached!
% 3.96/1.22 % (2370654)------------------------------
% 3.96/1.22 % (2370654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.22 % (2370654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.22 % (2370654)CaDiCaL version: 2.1.3
% 3.96/1.22 % (2370654)Termination reason: Instruction limit
% 3.96/1.22 % (2370654)Termination phase: Property scanning
% 3.96/1.22 % (2370654)Time elapsed: 0.004 s
% 3.96/1.22 % (2370654)Peak memory usage: 86 MB
% 3.96/1.22 % (2370654)Instructions burned: 14 (million)
% 3.96/1.22 % (2370656)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1128048999: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_2996 on theBenchmark for (2996ds/35Mi)
% 4.90/1.37 % (2370656)Instruction limit reached!
% 4.90/1.37 % (2370656)------------------------------
% 4.90/1.37 % (2370656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.37 % (2370656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.37 % (2370656)CaDiCaL version: 2.1.3
% 4.90/1.37 % (2370656)Termination reason: Instruction limit
% 4.90/1.37 % (2370656)Termination phase: Preprocessing 3
% 4.90/1.37 % (2370656)Time elapsed: 0.013 s
% 4.90/1.37 % (2370656)Peak memory usage: 88 MB
% 4.90/1.37 % (2370656)Instructions burned: 37 (million)
% 4.90/1.37 % (2370657)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3633262328:i=2:fsr=off:rtra=on:inst=on_2996 on theBenchmark for (2996ds/2Mi)
% 4.90/1.37 % (2370651)Instruction limit reached!
% 4.90/1.37 % (2370651)------------------------------
% 4.90/1.37 % (2370651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.37 % (2370651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.37 % (2370651)CaDiCaL version: 2.1.3
% 4.90/1.37 % (2370651)Termination reason: Instruction limit
% 4.90/1.37 % (2370651)Termination phase: Saturation
% 4.90/1.37 % (2370651)Time elapsed: 0.059 s
% 4.90/1.37 % (2370651)Peak memory usage: 118 MB
% 4.90/1.37 % (2370651)Instructions burned: 127 (million)
% 4.90/1.37 % (2370657)Instruction limit reached!
% 4.90/1.37 % (2370657)------------------------------
% 4.90/1.37 % (2370657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.37 % (2370657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.37 % (2370657)CaDiCaL version: 2.1.3
% 4.90/1.37 % (2370657)Termination reason: Instruction limit
% 4.90/1.37 % (2370657)Termination phase: Property scanning
% 4.90/1.37 % (2370657)Time elapsed: 0.002 s
% 4.90/1.37 % (2370657)Peak memory usage: 86 MB
% 4.90/1.37 % (2370657)Instructions burned: 5 (million)
% 4.90/1.37 % (2370667)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=575012978:i=370:ep=RS:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/370Mi)
% 4.90/1.37 % (2370666)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1688801553:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2996 on theBenchmark for (2996ds/8Mi)
% 4.90/1.37 % (2370666)Instruction limit reached!
% 4.90/1.37 % (2370666)------------------------------
% 4.90/1.37 % (2370666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.37 % (2370666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.37 % (2370666)CaDiCaL version: 2.1.3
% 4.90/1.37 % (2370666)Termination reason: Instruction limit
% 4.90/1.37 % (2370666)Termination phase: Property scanning
% 4.90/1.37 % (2370666)Time elapsed: 0.003 s
% 4.90/1.37 % (2370666)Peak memory usage: 86 MB
% 4.90/1.37 % (2370666)Instructions burned: 10 (million)
% 4.90/1.37 % (2370673)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=354683432:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2995 on theBenchmark for (2995ds/13Mi)
% 4.90/1.37 % (2370674)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2598004626:i=226:rtra=on:gtg=position:ss=axioms_2995 on theBenchmark for (2995ds/226Mi)
% 4.90/1.37 % (2370673)Instruction limit reached!
% 4.90/1.37 % (2370673)------------------------------
% 4.90/1.37 % (2370673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.37 % (2370673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.37 % (2370673)CaDiCaL version: 2.1.3
% 4.90/1.37 % (2370673)Termination reason: Instruction limit
% 4.90/1.37 % (2370673)Termination phase: Property scanning
% 4.90/1.37 % (2370673)Time elapsed: 0.004 s
% 4.90/1.37 % (2370673)Peak memory usage: 85 MB
% 4.90/1.37 % (2370673)Instructions burned: 17 (million)
% 4.90/1.37 % (2370688)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=366675534:i=10:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 4.90/1.37 % (2370688)Instruction limit reached!
% 4.90/1.37 % (2370688)------------------------------
% 4.90/1.37 % (2370688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.37 % (2370688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.37 % (2370688)CaDiCaL version: 2.1.3
% 4.90/1.37 % (2370688)Termination reason: Instruction limit
% 6.05/1.50 % (2370688)Termination phase: Preprocessing 1
% 6.05/1.50 % (2370688)Time elapsed: 0.004 s
% 6.05/1.50 % (2370688)Peak memory usage: 86 MB
% 6.05/1.50 % (2370688)Instructions burned: 13 (million)
% 6.05/1.50 % (2370693)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=1857193131:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2995 on theBenchmark for (2995ds/75Mi)
% 6.05/1.50 % (2370692)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2613359116:i=71:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/71Mi)
% 6.05/1.50 % (2370692)Instruction limit reached!
% 6.05/1.50 % (2370692)------------------------------
% 6.05/1.50 % (2370692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.50 % (2370692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.50 % (2370692)CaDiCaL version: 2.1.3
% 6.05/1.50 % (2370692)Termination reason: Instruction limit
% 6.05/1.50 % (2370692)Termination phase: Property scanning
% 6.05/1.50 % (2370692)Time elapsed: 0.020 s
% 6.05/1.50 % (2370692)Peak memory usage: 89 MB
% 6.05/1.50 % (2370692)Instructions burned: 72 (million)
% 6.05/1.50 % (2370693)Instruction limit reached!
% 6.05/1.50 % (2370693)------------------------------
% 6.05/1.50 % (2370693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.50 % (2370693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.50 % (2370693)CaDiCaL version: 2.1.3
% 6.05/1.50 % (2370693)Termination reason: Instruction limit
% 6.05/1.50 % (2370693)Termination phase: Saturation
% 6.05/1.50 % (2370693)Time elapsed: 0.021 s
% 6.05/1.50 % (2370693)Peak memory usage: 90 MB
% 6.05/1.50 % (2370693)Instructions burned: 79 (million)
% 6.05/1.50 % (2370717)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=526911603:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2995 on theBenchmark for (2995ds/294Mi)
% 6.05/1.50 % (2370674)Instruction limit reached!
% 6.05/1.50 % (2370674)------------------------------
% 6.05/1.50 % (2370674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.50 % (2370674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.50 % (2370674)CaDiCaL version: 2.1.3
% 6.05/1.50 % (2370674)Termination reason: Instruction limit
% 6.05/1.50 % (2370674)Termination phase: Saturation
% 6.05/1.50 % (2370674)Time elapsed: 0.076 s
% 6.05/1.50 % (2370674)Peak memory usage: 118 MB
% 6.05/1.50 % (2370674)Instructions burned: 228 (million)
% 6.05/1.50 % (2370667)Instruction limit reached!
% 6.05/1.50 % (2370667)------------------------------
% 6.05/1.50 % (2370667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.50 % (2370667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.50 % (2370667)CaDiCaL version: 2.1.3
% 6.05/1.50 % (2370667)Termination reason: Instruction limit
% 6.05/1.50 % (2370667)Termination phase: Saturation
% 6.05/1.50 % (2370667)Time elapsed: 0.102 s
% 6.05/1.50 % (2370667)Peak memory usage: 94 MB
% 6.05/1.50 % (2370667)Instructions burned: 373 (million)
% 6.05/1.50 % (2370724)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1028520691:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2994 on theBenchmark for (2994ds/130Mi)
% 6.05/1.50 % (2370728)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3065057163:i=131:rtra=on_2994 on theBenchmark for (2994ds/131Mi)
% 6.05/1.50 % (2370729)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1515039111:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/40Mi)
% 6.05/1.50 % (2370730)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2235693570:i=307:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/307Mi)
% 6.05/1.50 % (2370729)Instruction limit reached!
% 6.05/1.50 % (2370729)------------------------------
% 6.05/1.50 % (2370729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.50 % (2370729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.50 % (2370729)CaDiCaL version: 2.1.3
% 6.05/1.50 % (2370729)Termination reason: Instruction limit
% 6.05/1.50 % (2370729)Termination phase: Preprocessing 1
% 6.05/1.50 % (2370729)Time elapsed: 0.010 s
% 6.05/1.50 % (2370729)Peak memory usage: 86 MB
% 6.05/1.50 % (2370729)Instructions burned: 42 (million)
% 6.05/1.50 % (2370724)Instruction limit reached!
% 6.43/1.68 % (2370724)------------------------------
% 6.43/1.68 % (2370724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.43/1.68 % (2370724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.43/1.68 % (2370724)CaDiCaL version: 2.1.3
% 6.43/1.68 % (2370724)Termination reason: Instruction limit
% 6.43/1.68 % (2370724)Termination phase: Saturation
% 6.43/1.68 % (2370724)Time elapsed: 0.053 s
% 6.43/1.68 % (2370724)Peak memory usage: 115 MB
% 6.43/1.68 % (2370724)Instructions burned: 130 (million)
% 6.43/1.68 % (2370733)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3081461598:i=131:canc=cautious:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/131Mi)
% 6.43/1.68 % (2370732)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1590115046:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/598Mi)
% 6.43/1.68 % (2370728)Instruction limit reached!
% 6.43/1.68 % (2370728)------------------------------
% 6.43/1.68 % (2370728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.43/1.68 % (2370728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.43/1.68 % (2370728)CaDiCaL version: 2.1.3
% 6.43/1.68 % (2370728)Termination reason: Instruction limit
% 6.43/1.68 % (2370728)Termination phase: Saturation
% 6.43/1.68 % (2370728)Time elapsed: 0.069 s
% 6.43/1.68 % (2370728)Peak memory usage: 136 MB
% 6.43/1.68 % (2370728)Instructions burned: 132 (million)
% 6.43/1.68 % (2370717)Instruction limit reached!
% 6.43/1.68 % (2370717)------------------------------
% 6.43/1.68 % (2370717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.43/1.68 % (2370717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.43/1.68 % (2370717)CaDiCaL version: 2.1.3
% 6.43/1.68 % (2370717)Termination reason: Instruction limit
% 6.43/1.68 % (2370717)Termination phase: Saturation
% 6.43/1.68 % (2370717)Time elapsed: 0.111 s
% 6.43/1.68 % (2370717)Peak memory usage: 93 MB
% 6.43/1.68 % (2370717)Instructions burned: 295 (million)
% 6.43/1.68 % (2370730)Instruction limit reached!
% 6.43/1.68 % (2370730)------------------------------
% 6.43/1.68 % (2370730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.43/1.68 % (2370730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.43/1.68 % (2370730)CaDiCaL version: 2.1.3
% 6.43/1.68 % (2370730)Termination reason: Instruction limit
% 6.43/1.68 % (2370730)Termination phase: Saturation
% 6.43/1.68 % (2370730)Time elapsed: 0.086 s
% 6.43/1.68 % (2370730)Peak memory usage: 92 MB
% 6.43/1.68 % (2370730)Instructions burned: 310 (million)
% 6.43/1.68 % (2370733)Instruction limit reached!
% 6.43/1.68 % (2370733)------------------------------
% 6.43/1.68 % (2370733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.43/1.68 % (2370733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.43/1.68 % (2370733)CaDiCaL version: 2.1.3
% 6.43/1.68 % (2370733)Termination reason: Instruction limit
% 6.43/1.68 % (2370733)Termination phase: Saturation
% 6.43/1.68 % (2370733)Time elapsed: 0.055 s
% 6.43/1.68 % (2370733)Peak memory usage: 119 MB
% 6.43/1.68 % (2370733)Instructions burned: 131 (million)
% 6.43/1.68 % (2370738)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=2428398630:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2993 on theBenchmark for (2993ds/259Mi)
% 6.43/1.68 % (2370739)dis+10_1_si=on:random_seed=1613003248:s2a=on:i=1000:rtra=on:gtg=exists_all_2993 on theBenchmark for (2993ds/1000Mi)
% 6.43/1.68 % (2370743)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3970894038:i=141:doe=on:rtra=on_2993 on theBenchmark for (2993ds/141Mi)
% 6.43/1.68 % (2370742)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1853419033:i=383:fsr=off:rtra=on:ev=force_2993 on theBenchmark for (2993ds/383Mi)
% 6.43/1.68 % (2370743)Instruction limit reached!
% 6.43/1.68 % (2370743)------------------------------
% 6.43/1.68 % (2370743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.43/1.68 % (2370743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.43/1.68 % (2370743)CaDiCaL version: 2.1.3
% 6.43/1.68 % (2370743)Termination reason: Instruction limit
% 6.43/1.68 % (2370743)Termination phase: Saturation
% 6.43/1.68 % (2370743)Time elapsed: 0.044 s
% 8.19/1.87 % (2370743)Peak memory usage: 92 MB
% 8.19/1.87 % (2370743)Instructions burned: 141 (million)
% 8.19/1.87 % (2370744)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3960432887:i=65:nm=16:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 8.19/1.87 % (2370745)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3148832422:i=121:nm=16:rtra=on_2992 on theBenchmark for (2992ds/121Mi)
% 8.19/1.87 % (2370738)Instruction limit reached!
% 8.19/1.87 % (2370738)------------------------------
% 8.19/1.87 % (2370738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.19/1.87 % (2370738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.87 % (2370738)CaDiCaL version: 2.1.3
% 8.19/1.87 % (2370738)Termination reason: Instruction limit
% 8.19/1.87 % (2370738)Termination phase: Saturation
% 8.19/1.87 % (2370738)Time elapsed: 0.105 s
% 8.19/1.87 % (2370738)Peak memory usage: 119 MB
% 8.19/1.87 % (2370738)Instructions burned: 260 (million)
% 8.19/1.87 % (2370744)Instruction limit reached!
% 8.19/1.87 % (2370744)------------------------------
% 8.19/1.87 % (2370744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.19/1.87 % (2370744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.87 % (2370744)CaDiCaL version: 2.1.3
% 8.19/1.87 % (2370744)Termination reason: Instruction limit
% 8.19/1.87 % (2370744)Termination phase: Saturation
% 8.19/1.87 % (2370744)Time elapsed: 0.019 s
% 8.19/1.87 % (2370744)Peak memory usage: 90 MB
% 8.19/1.87 % (2370744)Instructions burned: 67 (million)
% 8.19/1.87 % (2370745)Instruction limit reached!
% 8.19/1.87 % (2370745)------------------------------
% 8.19/1.87 % (2370745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.19/1.87 % (2370745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.87 % (2370745)CaDiCaL version: 2.1.3
% 8.19/1.87 % (2370745)Termination reason: Instruction limit
% 8.19/1.87 % (2370745)Termination phase: Saturation
% 8.19/1.87 % (2370745)Time elapsed: 0.038 s
% 8.19/1.87 % (2370745)Peak memory usage: 91 MB
% 8.19/1.87 % (2370745)Instructions burned: 122 (million)
% 8.19/1.87 % (2370750)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=1858802368:s2a=on:i=128:s2at=5:ins=3:rtra=on_2991 on theBenchmark for (2991ds/128Mi)
% 8.19/1.87 % (2370742)Instruction limit reached!
% 8.19/1.87 % (2370742)------------------------------
% 8.19/1.87 % (2370742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.19/1.87 % (2370742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.87 % (2370742)CaDiCaL version: 2.1.3
% 8.19/1.87 % (2370742)Termination reason: Instruction limit
% 8.19/1.87 % (2370742)Termination phase: Saturation
% 8.19/1.87 % (2370742)Time elapsed: 0.137 s
% 8.19/1.87 % (2370742)Peak memory usage: 97 MB
% 8.19/1.87 % (2370742)Instructions burned: 384 (million)
% 8.19/1.87 % (2370732)Instruction limit reached!
% 8.19/1.87 % (2370732)------------------------------
% 8.19/1.87 % (2370732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.19/1.87 % (2370732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.87 % (2370732)CaDiCaL version: 2.1.3
% 8.19/1.87 % (2370732)Termination reason: Instruction limit
% 8.19/1.87 % (2370732)Termination phase: Saturation
% 8.19/1.87 % (2370732)Time elapsed: 0.239 s
% 8.19/1.87 % (2370732)Peak memory usage: 139 MB
% 8.19/1.87 % (2370732)Instructions burned: 600 (million)
% 8.19/1.87 % (2370754)dis+1010_1_to=kbo:si=on:random_seed=2171687120:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2991 on theBenchmark for (2991ds/175Mi)
% 8.19/1.87 % (2370753)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=3959214128:i=39:ins=3:rtra=on_2991 on theBenchmark for (2991ds/39Mi)
% 8.19/1.87 % (2370753)Instruction limit reached!
% 8.19/1.87 % (2370753)------------------------------
% 8.19/1.87 % (2370753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.19/1.87 % (2370753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.19/1.87 % (2370753)CaDiCaL version: 2.1.3
% 8.19/1.87 % (2370753)Termination reason: Instruction limit
% 8.19/1.87 % (2370753)Termination phase: Preprocessing 3
% 8.19/1.87 % (2370753)Time elapsed: 0.013 s
% 8.19/1.87 % (2370753)Peak memory usage: 88 MB
% 8.19/1.87 % (2370753)Instructions burned: 41 (million)
% 8.19/1.87 % (2370750)Instruction limit reached!
% 10.31/2.09 % (2370750)------------------------------
% 10.31/2.09 % (2370750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.09 % (2370750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.09 % (2370750)CaDiCaL version: 2.1.3
% 10.31/2.09 % (2370750)Termination reason: Instruction limit
% 10.31/2.09 % (2370750)Termination phase: Saturation
% 10.31/2.09 % (2370750)Time elapsed: 0.042 s
% 10.31/2.09 % (2370750)Peak memory usage: 92 MB
% 10.31/2.09 % (2370750)Instructions burned: 130 (million)
% 10.31/2.09 % (2370755)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1873760036:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/329Mi)
% 10.31/2.09 % (2370754)Instruction limit reached!
% 10.31/2.09 % (2370754)------------------------------
% 10.31/2.09 % (2370754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.09 % (2370754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.09 % (2370754)CaDiCaL version: 2.1.3
% 10.31/2.09 % (2370754)Termination reason: Instruction limit
% 10.31/2.09 % (2370754)Termination phase: Saturation
% 10.31/2.09 % (2370754)Time elapsed: 0.059 s
% 10.31/2.09 % (2370754)Peak memory usage: 92 MB
% 10.31/2.09 % (2370754)Instructions burned: 175 (million)
% 10.31/2.09 % (2370758)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4211928360:thitd=on:i=215:nm=0:rtra=on:ev=force_2990 on theBenchmark for (2990ds/215Mi)
% 10.31/2.09 % (2370757)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=77629871:s2a=on:i=483:doe=on:nm=32:rtra=on_2990 on theBenchmark for (2990ds/483Mi)
% 10.31/2.09 % (2370762)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=286768818:st=2:i=295:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/295Mi)
% 10.31/2.09 % (2370761)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3040535849:i=349:rtra=on_2990 on theBenchmark for (2990ds/349Mi)
% 10.31/2.09 % (2370755)Instruction limit reached!
% 10.31/2.09 % (2370755)------------------------------
% 10.31/2.09 % (2370755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.09 % (2370755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.09 % (2370755)CaDiCaL version: 2.1.3
% 10.31/2.09 % (2370755)Termination reason: Instruction limit
% 10.31/2.09 % (2370755)Termination phase: Saturation
% 10.31/2.09 % (2370755)Time elapsed: 0.124 s
% 10.31/2.09 % (2370755)Peak memory usage: 121 MB
% 10.31/2.09 % (2370755)Instructions burned: 330 (million)
% 10.31/2.09 % (2370764)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3001092692:i=328:kws=inv_frequency:nm=20:rtra=on_2990 on theBenchmark for (2990ds/328Mi)
% 10.31/2.09 % (2370739)Instruction limit reached!
% 10.31/2.09 % (2370739)------------------------------
% 10.31/2.09 % (2370739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.09 % (2370739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.09 % (2370739)CaDiCaL version: 2.1.3
% 10.31/2.09 % (2370739)Termination reason: Instruction limit
% 10.31/2.09 % (2370739)Termination phase: Saturation
% 10.31/2.09 % (2370739)Time elapsed: 0.331 s
% 10.31/2.09 % (2370739)Peak memory usage: 98 MB
% 10.31/2.09 % (2370739)Instructions burned: 1003 (million)
% 10.31/2.09 % (2370758)Instruction limit reached!
% 10.31/2.09 % (2370758)------------------------------
% 10.31/2.09 % (2370758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.09 % (2370758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.09 % (2370758)CaDiCaL version: 2.1.3
% 10.31/2.09 % (2370758)Termination reason: Instruction limit
% 10.31/2.09 % (2370758)Termination phase: Saturation
% 10.31/2.09 % (2370758)Time elapsed: 0.091 s
% 10.31/2.09 % (2370758)Peak memory usage: 139 MB
% 10.31/2.09 % (2370758)Instructions burned: 217 (million)
% 10.31/2.09 % (2370762)Instruction limit reached!
% 10.31/2.09 % (2370762)------------------------------
% 10.31/2.09 % (2370762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.09 % (2370762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.09 % (2370762)CaDiCaL version: 2.1.3
% 10.31/2.09 % (2370762)Termination reason: Instruction limit
% 10.31/2.09 % (2370762)Termination phase: Saturation
% 10.31/2.09 % (2370762)Time elapsed: 0.095 s
% 10.89/2.22 % (2370762)Peak memory usage: 92 MB
% 10.89/2.22 % (2370762)Instructions burned: 298 (million)
% 10.89/2.22 % (2370769)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2999422235:i=281:gtgl=2:rtra=on:gtg=all_2989 on theBenchmark for (2989ds/281Mi)
% 10.89/2.22 % (2370761)Instruction limit reached!
% 10.89/2.22 % (2370761)------------------------------
% 10.89/2.22 % (2370761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.22 % (2370761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.22 % (2370761)CaDiCaL version: 2.1.3
% 10.89/2.22 % (2370761)Termination reason: Instruction limit
% 10.89/2.22 % (2370761)Termination phase: Saturation
% 10.89/2.22 % (2370761)Time elapsed: 0.137 s
% 10.89/2.22 % (2370761)Peak memory usage: 120 MB
% 10.89/2.22 % (2370761)Instructions burned: 352 (million)
% 10.89/2.22 % (2370771)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1914011470:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/484Mi)
% 10.89/2.22 % (2370772)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2219802577:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2989 on theBenchmark for (2989ds/321Mi)
% 10.89/2.22 % (2370757)Instruction limit reached!
% 10.89/2.22 % (2370757)------------------------------
% 10.89/2.22 % (2370757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.22 % (2370757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.22 % (2370757)CaDiCaL version: 2.1.3
% 10.89/2.22 % (2370757)Termination reason: Instruction limit
% 10.89/2.22 % (2370757)Termination phase: Saturation
% 10.89/2.22 % (2370757)Time elapsed: 0.199 s
% 10.89/2.22 % (2370757)Peak memory usage: 139 MB
% 10.89/2.22 % (2370757)Instructions burned: 484 (million)
% 10.89/2.22 % (2370773)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1255670193:i=416:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/416Mi)
% 10.89/2.22 % (2370764)Instruction limit reached!
% 10.89/2.22 % (2370764)------------------------------
% 10.89/2.22 % (2370764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.22 % (2370764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.22 % (2370764)CaDiCaL version: 2.1.3
% 10.89/2.22 % (2370764)Termination reason: Instruction limit
% 10.89/2.22 % (2370764)Termination phase: Saturation
% 10.89/2.22 % (2370764)Time elapsed: 0.122 s
% 10.89/2.22 % (2370764)Peak memory usage: 119 MB
% 10.89/2.22 % (2370764)Instructions burned: 329 (million)
% 10.89/2.22 % (2370775)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=976526123:i=471:thf=on:kws=precedence:rtra=on_2988 on theBenchmark for (2988ds/471Mi)
% 10.89/2.22 % (2370769)Instruction limit reached!
% 10.89/2.22 % (2370769)------------------------------
% 10.89/2.22 % (2370769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.22 % (2370769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.22 % (2370769)CaDiCaL version: 2.1.3
% 10.89/2.22 % (2370769)Termination reason: Instruction limit
% 10.89/2.22 % (2370769)Termination phase: Saturation
% 10.89/2.22 % (2370769)Time elapsed: 0.101 s
% 10.89/2.22 % (2370769)Peak memory usage: 119 MB
% 10.89/2.22 % (2370769)Instructions burned: 281 (million)
% 10.89/2.22 % (2370772)Instruction limit reached!
% 10.89/2.22 % (2370772)------------------------------
% 10.89/2.22 % (2370772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.22 % (2370772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.22 % (2370772)CaDiCaL version: 2.1.3
% 10.89/2.22 % (2370772)Termination reason: Instruction limit
% 10.89/2.22 % (2370772)Termination phase: Saturation
% 10.89/2.22 % (2370772)Time elapsed: 0.091 s
% 10.89/2.22 % (2370772)Peak memory usage: 115 MB
% 10.89/2.22 % (2370772)Instructions burned: 323 (million)
% 10.89/2.22 % (2370780)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2854916203:i=375:kws=inv_arity_squared:rtra=on_2987 on theBenchmark for (2987ds/375Mi)
% 10.89/2.22 % (2370779)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=2585839745:avsq=on:i=276:avsqr=1,2:rtra=on_2987 on theBenchmark for (2987ds/276Mi)
% 10.89/2.22 % (2370771)Instruction limit reached!
% 10.89/2.22 % (2370771)------------------------------
% 10.89/2.22 % (2370771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.50 % (2370771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.50 % (2370771)CaDiCaL version: 2.1.3
% 11.96/2.50 % (2370771)Termination reason: Instruction limit
% 11.96/2.50 % (2370771)Termination phase: Saturation
% 11.96/2.50 % (2370771)Time elapsed: 0.121 s
% 11.96/2.50 % (2370771)Peak memory usage: 91 MB
% 11.96/2.50 % (2370771)Instructions burned: 484 (million)
% 11.96/2.50 % (2370773)Instruction limit reached!
% 11.96/2.50 % (2370773)------------------------------
% 11.96/2.50 % (2370773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.50 % (2370773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.50 % (2370773)CaDiCaL version: 2.1.3
% 11.96/2.50 % (2370773)Termination reason: Instruction limit
% 11.96/2.50 % (2370773)Termination phase: Saturation
% 11.96/2.50 % (2370773)Time elapsed: 0.120 s
% 11.96/2.50 % (2370773)Peak memory usage: 118 MB
% 11.96/2.50 % (2370773)Instructions burned: 419 (million)
% 11.96/2.50 % (2370782)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2804205229:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/387Mi)
% 11.96/2.50 % (2370783)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3923147958:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2987 on theBenchmark for (2987ds/513Mi)
% 11.96/2.50 % (2370786)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=954008782:i=334:rtra=on_2986 on theBenchmark for (2986ds/334Mi)
% 11.96/2.50 % (2370779)Instruction limit reached!
% 11.96/2.50 % (2370779)------------------------------
% 11.96/2.50 % (2370779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.50 % (2370779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.50 % (2370779)CaDiCaL version: 2.1.3
% 11.96/2.50 % (2370779)Termination reason: Instruction limit
% 11.96/2.50 % (2370779)Termination phase: Saturation
% 11.96/2.50 % (2370779)Time elapsed: 0.119 s
% 11.96/2.50 % (2370779)Peak memory usage: 137 MB
% 11.96/2.50 % (2370779)Instructions burned: 277 (million)
% 11.96/2.50 % (2370787)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2403153058:i=359:rtra=on:gtg=exists_top:ss=axioms_2986 on theBenchmark for (2986ds/359Mi)
% 11.96/2.50 % (2370775)Instruction limit reached!
% 11.96/2.50 % (2370775)------------------------------
% 11.96/2.50 % (2370775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.50 % (2370775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.50 % (2370775)CaDiCaL version: 2.1.3
% 11.96/2.50 % (2370775)Termination reason: Instruction limit
% 11.96/2.50 % (2370775)Termination phase: Saturation
% 11.96/2.50 % (2370775)Time elapsed: 0.181 s
% 11.96/2.50 % (2370775)Peak memory usage: 121 MB
% 11.96/2.50 % (2370775)Instructions burned: 473 (million)
% 11.96/2.50 % (2370780)Instruction limit reached!
% 11.96/2.50 % (2370780)------------------------------
% 11.96/2.50 % (2370780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.50 % (2370780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.50 % (2370780)CaDiCaL version: 2.1.3
% 11.96/2.50 % (2370780)Termination reason: Instruction limit
% 11.96/2.50 % (2370780)Termination phase: Saturation
% 11.96/2.50 % (2370780)Time elapsed: 0.142 s
% 11.96/2.50 % (2370780)Peak memory usage: 120 MB
% 11.96/2.50 % (2370780)Instructions burned: 382 (million)
% 11.96/2.50 % (2370791)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=776043622:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2985 on theBenchmark for (2985ds/341Mi)
% 11.96/2.50 % (2370782)Instruction limit reached!
% 11.96/2.50 % (2370782)------------------------------
% 11.96/2.50 % (2370782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.50 % (2370782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.50 % (2370782)CaDiCaL version: 2.1.3
% 11.96/2.50 % (2370782)Termination reason: Instruction limit
% 11.96/2.50 % (2370782)Termination phase: Saturation
% 11.96/2.50 % (2370782)Time elapsed: 0.152 s
% 11.96/2.50 % (2370782)Peak memory usage: 120 MB
% 11.96/2.50 % (2370782)Instructions burned: 390 (million)
% 11.96/2.50 % (2370787)Instruction limit reached!
% 11.96/2.50 % (2370787)------------------------------
% 11.96/2.50 % (2370787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/2.79 % (2370787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/2.79 % (2370787)CaDiCaL version: 2.1.3
% 13.62/2.79 % (2370787)Termination reason: Instruction limit
% 13.62/2.79 % (2370787)Termination phase: Saturation
% 13.62/2.79 % (2370787)Time elapsed: 0.094 s
% 13.62/2.79 % (2370787)Peak memory usage: 92 MB
% 13.62/2.79 % (2370787)Instructions burned: 363 (million)
% 13.62/2.79 % (2370793)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3184793640:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/261Mi)
% 13.62/2.79 % (2370794)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=2613740395:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2985 on theBenchmark for (2985ds/235Mi)
% 13.62/2.79 % (2370786)Instruction limit reached!
% 13.62/2.79 % (2370786)------------------------------
% 13.62/2.79 % (2370786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/2.79 % (2370786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/2.79 % (2370786)CaDiCaL version: 2.1.3
% 13.62/2.79 % (2370786)Termination reason: Instruction limit
% 13.62/2.79 % (2370786)Termination phase: Saturation
% 13.62/2.79 % (2370786)Time elapsed: 0.153 s
% 13.62/2.79 % (2370786)Peak memory usage: 138 MB
% 13.62/2.79 % (2370786)Instructions burned: 336 (million)
% 13.62/2.79 % (2370783)Instruction limit reached!
% 13.62/2.79 % (2370783)------------------------------
% 13.62/2.79 % (2370783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/2.79 % (2370783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/2.79 % (2370783)CaDiCaL version: 2.1.3
% 13.62/2.79 % (2370783)Termination reason: Instruction limit
% 13.62/2.79 % (2370783)Termination phase: Saturation
% 13.62/2.79 % (2370783)Time elapsed: 0.177 s
% 13.62/2.79 % (2370783)Peak memory usage: 94 MB
% 13.62/2.79 % (2370783)Instructions burned: 515 (million)
% 13.62/2.79 % (2370796)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3498864837:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2984 on theBenchmark for (2984ds/273Mi)
% 13.62/2.79 % (2370799)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2990262553:i=146:doe=on:rtra=on_2984 on theBenchmark for (2984ds/146Mi)
% 13.62/2.79 % (2370794)Instruction limit reached!
% 13.62/2.79 % (2370794)------------------------------
% 13.62/2.79 % (2370794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/2.79 % (2370794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/2.79 % (2370794)CaDiCaL version: 2.1.3
% 13.62/2.79 % (2370794)Termination reason: Instruction limit
% 13.62/2.79 % (2370794)Termination phase: Saturation
% 13.62/2.79 % (2370794)Time elapsed: 0.095 s
% 13.62/2.79 % (2370794)Peak memory usage: 118 MB
% 13.62/2.79 % (2370794)Instructions burned: 235 (million)
% 13.62/2.79 % (2370791)Instruction limit reached!
% 13.62/2.79 % (2370791)------------------------------
% 13.62/2.79 % (2370791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/2.79 % (2370791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/2.79 % (2370791)CaDiCaL version: 2.1.3
% 13.62/2.79 % (2370791)Termination reason: Instruction limit
% 13.62/2.79 % (2370791)Termination phase: Saturation
% 13.62/2.79 % (2370791)Time elapsed: 0.128 s
% 13.62/2.79 % (2370791)Peak memory usage: 122 MB
% 13.62/2.79 % (2370791)Instructions burned: 342 (million)
% 13.62/2.79 % (2370793)Instruction limit reached!
% 13.62/2.79 % (2370793)------------------------------
% 13.62/2.79 % (2370793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/2.79 % (2370793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/2.79 % (2370793)CaDiCaL version: 2.1.3
% 13.62/2.79 % (2370793)Termination reason: Instruction limit
% 13.62/2.79 % (2370793)Termination phase: Saturation
% 13.62/2.79 % (2370793)Time elapsed: 0.102 s
% 13.62/2.79 % (2370793)Peak memory usage: 118 MB
% 13.62/2.79 % (2370793)Instructions burned: 261 (million)
% 13.62/2.79 % (2370800)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=986398078:i=4428:doe=on:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/4428Mi)
% 13.62/2.79 % (2370801)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=13095265:avsq=on:i=276:avsqr=1,2:rtra=on_2984 on theBenchmark for (2984ds/276Mi)
% 17.33/3.06 % (2370799)Instruction limit reached!
% 17.33/3.06 % (2370799)------------------------------
% 17.33/3.06 % (2370799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.33/3.06 % (2370799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.33/3.06 % (2370799)CaDiCaL version: 2.1.3
% 17.33/3.06 % (2370799)Termination reason: Instruction limit
% 17.33/3.06 % (2370799)Termination phase: Saturation
% 17.33/3.06 % (2370799)Time elapsed: 0.049 s
% 17.33/3.06 % (2370799)Peak memory usage: 92 MB
% 17.33/3.06 % (2370799)Instructions burned: 148 (million)
% 17.33/3.06 % (2370796)Instruction limit reached!
% 17.33/3.06 % (2370796)------------------------------
% 17.33/3.06 % (2370796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.33/3.06 % (2370796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.33/3.06 % (2370796)CaDiCaL version: 2.1.3
% 17.33/3.06 % (2370796)Termination reason: Instruction limit
% 17.33/3.06 % (2370796)Termination phase: Saturation
% 17.33/3.06 % (2370796)Time elapsed: 0.100 s
% 17.33/3.06 % (2370796)Peak memory usage: 93 MB
% 17.33/3.06 % (2370796)Instructions burned: 274 (million)
% 17.33/3.06 % (2370804)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2603327187:i=1052:rtra=on_2983 on theBenchmark for (2983ds/1052Mi)
% 17.33/3.06 % (2370805)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3274917742:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2983 on theBenchmark for (2983ds/655Mi)
% 17.33/3.06 % (2370806)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2054753430:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2983 on theBenchmark for (2983ds/1054Mi)
% 17.33/3.06 % (2370801)Instruction limit reached!
% 17.33/3.06 % (2370801)------------------------------
% 17.33/3.06 % (2370801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.33/3.06 % (2370801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.33/3.06 % (2370801)CaDiCaL version: 2.1.3
% 17.33/3.06 % (2370801)Termination reason: Instruction limit
% 17.33/3.06 % (2370801)Termination phase: Saturation
% 17.33/3.06 % (2370801)Time elapsed: 0.111 s
% 17.33/3.06 % (2370801)Peak memory usage: 136 MB
% 17.33/3.06 % (2370801)Instructions burned: 278 (million)
% 17.33/3.06 % (2370809)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=369329289:i=107:rtra=on_2983 on theBenchmark for (2983ds/107Mi)
% 17.33/3.06 % (2370810)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1607399043:s2a=on:i=450:doe=on:nm=32:rtra=on_2982 on theBenchmark for (2982ds/450Mi)
% 17.33/3.06 % (2370809)Instruction limit reached!
% 17.33/3.06 % (2370809)------------------------------
% 17.33/3.06 % (2370809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.33/3.06 % (2370809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.33/3.06 % (2370809)CaDiCaL version: 2.1.3
% 17.33/3.06 % (2370809)Termination reason: Instruction limit
% 17.33/3.06 % (2370809)Termination phase: Saturation
% 17.33/3.06 % (2370809)Time elapsed: 0.032 s
% 17.33/3.06 % (2370809)Peak memory usage: 91 MB
% 17.33/3.06 % (2370809)Instructions burned: 108 (million)
% 17.33/3.06 % (2370815)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 17.33/3.06 % (2370815)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1365370784:i=1090:aac=none:nm=0:rtra=on:rawr=on_2982 on theBenchmark for (2982ds/1090Mi)
% 17.33/3.06 % (2370817)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3944048921:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/130Mi)
% 17.33/3.06 % (2370817)Instruction limit reached!
% 17.33/3.06 % (2370817)------------------------------
% 17.33/3.06 % (2370817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.33/3.06 % (2370817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.33/3.06 % (2370817)CaDiCaL version: 2.1.3
% 17.33/3.06 % (2370817)Termination reason: Instruction limit
% 17.33/3.06 % (2370817)Termination phase: Saturation
% 18.73/3.35 % (2370817)Time elapsed: 0.050 s
% 18.73/3.35 % (2370817)Peak memory usage: 115 MB
% 18.73/3.35 % (2370817)Instructions burned: 132 (million)
% 18.73/3.35 % (2370805)Instruction limit reached!
% 18.73/3.35 % (2370805)------------------------------
% 18.73/3.35 % (2370805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.73/3.35 % (2370805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.73/3.35 % (2370805)CaDiCaL version: 2.1.3
% 18.73/3.35 % (2370805)Termination reason: Instruction limit
% 18.73/3.35 % (2370805)Termination phase: Saturation
% 18.73/3.35 % (2370805)Time elapsed: 0.204 s
% 18.73/3.35 % (2370805)Peak memory usage: 97 MB
% 18.73/3.35 % (2370805)Instructions burned: 656 (million)
% 18.73/3.35 % (2370810)Instruction limit reached!
% 18.73/3.35 % (2370810)------------------------------
% 18.73/3.35 % (2370810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.73/3.35 % (2370810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.73/3.35 % (2370810)CaDiCaL version: 2.1.3
% 18.73/3.35 % (2370810)Termination reason: Instruction limit
% 18.73/3.35 % (2370810)Termination phase: Saturation
% 18.73/3.35 % (2370810)Time elapsed: 0.174 s
% 18.73/3.35 % (2370810)Peak memory usage: 137 MB
% 18.73/3.35 % (2370810)Instructions burned: 451 (million)
% 18.73/3.35 % (2370820)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3986506457:i=312:kws=inv_frequency:nm=20:rtra=on_2980 on theBenchmark for (2980ds/312Mi)
% 18.73/3.35 % (2370821)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1171926438:i=491:doe=on:rtra=on:gtg=position_2980 on theBenchmark for (2980ds/491Mi)
% 18.73/3.35 % (2370822)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3873723814:s2a=on:i=835:s2at=2:rtra=on_2980 on theBenchmark for (2980ds/835Mi)
% 18.73/3.35 % (2370804)Instruction limit reached!
% 18.73/3.35 % (2370804)------------------------------
% 18.73/3.35 % (2370804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.73/3.35 % (2370804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.73/3.35 % (2370804)CaDiCaL version: 2.1.3
% 18.73/3.35 % (2370804)Termination reason: Instruction limit
% 18.73/3.35 % (2370804)Termination phase: Saturation
% 18.73/3.35 % (2370804)Time elapsed: 0.377 s
% 18.73/3.35 % (2370804)Peak memory usage: 98 MB
% 18.73/3.35 % (2370804)Instructions burned: 1052 (million)
% 18.73/3.35 % (2370806)Instruction limit reached!
% 18.73/3.35 % (2370806)------------------------------
% 18.73/3.35 % (2370806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.73/3.35 % (2370806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.73/3.35 % (2370806)CaDiCaL version: 2.1.3
% 18.73/3.35 % (2370806)Termination reason: Instruction limit
% 18.73/3.35 % (2370806)Termination phase: Saturation
% 18.73/3.35 % (2370806)Time elapsed: 0.365 s
% 18.73/3.35 % (2370806)Peak memory usage: 97 MB
% 18.73/3.35 % (2370806)Instructions burned: 1057 (million)
% 18.73/3.35 % (2370820)Instruction limit reached!
% 18.73/3.35 % (2370820)------------------------------
% 18.73/3.35 % (2370820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.73/3.35 % (2370820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.73/3.35 % (2370820)CaDiCaL version: 2.1.3
% 18.73/3.35 % (2370820)Termination reason: Instruction limit
% 18.73/3.35 % (2370820)Termination phase: Saturation
% 18.73/3.35 % (2370820)Time elapsed: 0.110 s
% 18.73/3.35 % (2370820)Peak memory usage: 119 MB
% 18.73/3.35 % (2370820)Instructions burned: 312 (million)
% 18.73/3.35 % (2370821)Instruction limit reached!
% 18.73/3.35 % (2370821)------------------------------
% 18.73/3.35 % (2370821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.73/3.35 % (2370821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.73/3.35 % (2370821)CaDiCaL version: 2.1.3
% 18.73/3.35 % (2370821)Termination reason: Instruction limit
% 18.73/3.35 % (2370821)Termination phase: Saturation
% 18.73/3.35 % (2370821)Time elapsed: 0.147 s
% 18.73/3.35 % (2370821)Peak memory usage: 94 MB
% 18.73/3.35 % (2370821)Instructions burned: 495 (million)
% 18.73/3.35 % (2370826)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2813055882:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2979 on theBenchmark for (2979ds/307Mi)
% 18.73/3.35 % (2370827)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4064264142:i=776:doe=on:rtra=on_2978 on theBenchmark for (2978ds/776Mi)
% 18.73/3.35 % (2370828)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1981543326:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2978 on theBenchmark for (2978ds/646Mi)
% 20.57/3.89 % (2370815)Instruction limit reached!
% 20.57/3.89 % (2370815)------------------------------
% 20.57/3.89 % (2370815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/3.89 % (2370815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.89 % (2370815)CaDiCaL version: 2.1.3
% 20.57/3.89 % (2370815)Termination reason: Instruction limit
% 20.57/3.89 % (2370815)Termination phase: Saturation
% 20.57/3.89 % (2370815)Time elapsed: 0.382 s
% 20.57/3.89 % (2370815)Peak memory usage: 125 MB
% 20.57/3.89 % (2370815)Instructions burned: 1092 (million)
% 20.57/3.89 % (2370826)Refutation not found, incomplete strategy
% 20.57/3.89 % (2370826)------------------------------
% 20.57/3.89 % (2370826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/3.89 % (2370826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.89 % (2370826)CaDiCaL version: 2.1.3
% 20.57/3.89 % (2370826)Termination reason: Refutation not found, incomplete strategy
% 20.57/3.89 % (2370826)Time elapsed: 0.064 s
% 20.57/3.89 % (2370826)Peak memory usage: 93 MB
% 20.57/3.89 % (2370826)Instructions burned: 187 (million)
% 20.57/3.89 % (2370830)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=3709345649:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2978 on theBenchmark for (2978ds/784Mi)
% 20.57/3.89 % (2370822)Instruction limit reached!
% 20.57/3.89 % (2370822)------------------------------
% 20.57/3.89 % (2370822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/3.89 % (2370822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.89 % (2370822)CaDiCaL version: 2.1.3
% 20.57/3.89 % (2370822)Termination reason: Instruction limit
% 20.57/3.89 % (2370822)Termination phase: Saturation
% 20.57/3.89 % (2370822)Time elapsed: 0.265 s
% 20.57/3.89 % (2370822)Peak memory usage: 96 MB
% 20.57/3.89 % (2370822)Instructions burned: 837 (million)
% 20.57/3.89 % (2370833)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=266113929:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2977 on theBenchmark for (2977ds/1131Mi)
% 20.57/3.89 % (2370826)------------------------------
% 20.57/3.89 % (2370826)------------------------------
% 20.57/3.89 % (2370835)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=4287826480:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2976 on theBenchmark for (2976ds/246Mi)
% 20.57/3.89 % (2370828)Instruction limit reached!
% 20.57/3.89 % (2370828)------------------------------
% 20.57/3.89 % (2370828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/3.89 % (2370828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.89 % (2370828)CaDiCaL version: 2.1.3
% 20.57/3.89 % (2370828)Termination reason: Instruction limit
% 20.57/3.89 % (2370828)Termination phase: Saturation
% 20.57/3.89 % (2370828)Time elapsed: 0.241 s
% 20.57/3.89 % (2370828)Peak memory usage: 139 MB
% 20.57/3.89 % (2370828)Instructions burned: 649 (million)
% 20.57/3.89 % (2370827)Instruction limit reached!
% 20.57/3.89 % (2370827)------------------------------
% 20.57/3.89 % (2370827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/3.89 % (2370827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.89 % (2370827)CaDiCaL version: 2.1.3
% 20.57/3.89 % (2370827)Termination reason: Instruction limit
% 20.57/3.89 % (2370827)Termination phase: Saturation
% 20.57/3.89 % (2370827)Time elapsed: 0.276 s
% 20.57/3.89 % (2370827)Peak memory usage: 124 MB
% 20.57/3.89 % (2370827)Instructions burned: 779 (million)
% 20.57/3.89 % (2370837)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=619616553:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/775Mi)
% 20.57/3.89 % (2370830)Instruction limit reached!
% 20.57/3.89 % (2370830)------------------------------
% 20.57/3.89 % (2370830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.57/3.89 % (2370830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.57/3.89 % (2370830)CaDiCaL version: 2.1.3
% 20.57/3.89 % (2370830)Termination reason: Instruction limit
% 25.62/4.24 % (2370830)Termination phase: Saturation
% 25.62/4.24 % (2370830)Time elapsed: 0.232 s
% 25.62/4.24 % (2370830)Peak memory usage: 121 MB
% 25.62/4.24 % (2370830)Instructions burned: 787 (million)
% 25.62/4.24 % (2370835)Instruction limit reached!
% 25.62/4.24 % (2370835)------------------------------
% 25.62/4.24 % (2370835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370835)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370835)Termination reason: Instruction limit
% 25.62/4.24 % (2370835)Termination phase: Saturation
% 25.62/4.24 % (2370835)Time elapsed: 0.098 s
% 25.62/4.24 % (2370835)Peak memory usage: 118 MB
% 25.62/4.24 % (2370835)Instructions burned: 246 (million)
% 25.62/4.24 % (2370839)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1088150313:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2975 on theBenchmark for (2975ds/273Mi)
% 25.62/4.24 % (2370840)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1395983353:i=102:nm=16:rtra=on_2975 on theBenchmark for (2975ds/102Mi)
% 25.62/4.24 % (2370842)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=1954080460:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2974 on theBenchmark for (2974ds/1094Mi)
% 25.62/4.24 % (2370840)Instruction limit reached!
% 25.62/4.24 % (2370840)------------------------------
% 25.62/4.24 % (2370840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370840)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370840)Termination reason: Instruction limit
% 25.62/4.24 % (2370840)Termination phase: Saturation
% 25.62/4.24 % (2370840)Time elapsed: 0.029 s
% 25.62/4.24 % (2370840)Peak memory usage: 91 MB
% 25.62/4.24 % (2370840)Instructions burned: 103 (million)
% 25.62/4.24 % (2370843)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=437554062:i=6400:doe=on:fsr=off:rtra=on_2974 on theBenchmark for (2974ds/6400Mi)
% 25.62/4.24 % (2370839)Instruction limit reached!
% 25.62/4.24 % (2370839)------------------------------
% 25.62/4.24 % (2370839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370839)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370839)Termination reason: Instruction limit
% 25.62/4.24 % (2370839)Termination phase: Saturation
% 25.62/4.24 % (2370839)Time elapsed: 0.095 s
% 25.62/4.24 % (2370839)Peak memory usage: 93 MB
% 25.62/4.24 % (2370839)Instructions burned: 273 (million)
% 25.62/4.24 % (2370847)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=2608906715:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2973 on theBenchmark for (2973ds/868Mi)
% 25.62/4.24 % (2370837)Instruction limit reached!
% 25.62/4.24 % (2370837)------------------------------
% 25.62/4.24 % (2370837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370837)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370837)Termination reason: Instruction limit
% 25.62/4.24 % (2370837)Termination phase: Saturation
% 25.62/4.24 % (2370837)Time elapsed: 0.250 s
% 25.62/4.24 % (2370837)Peak memory usage: 95 MB
% 25.62/4.24 % (2370837)Instructions burned: 776 (million)
% 25.62/4.24 % (2370849)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=3559730230:i=1846:canc=cautious:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/1846Mi)
% 25.62/4.24 % (2370833)Instruction limit reached!
% 25.62/4.24 % (2370833)------------------------------
% 25.62/4.24 % (2370833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370833)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370833)Termination reason: Instruction limit
% 25.62/4.24 % (2370833)Termination phase: Saturation
% 25.62/4.24 % (2370833)Time elapsed: 0.415 s
% 25.62/4.24 % (2370833)Peak memory usage: 128 MB
% 25.62/4.24 % (2370833)Instructions burned: 1132 (million)
% 25.62/4.24 % (2370849)Refutation not found, incomplete strategy
% 25.62/4.24 % (2370849)------------------------------
% 25.62/4.24 % (2370849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370849)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370849)Termination reason: Refutation not found, incomplete strategy
% 25.62/4.24 % (2370849)Time elapsed: 0.039 s
% 25.62/4.24 % (2370849)Peak memory usage: 93 MB
% 25.62/4.24 % (2370849)Instructions burned: 127 (million)
% 25.62/4.24 % (2370851)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=65293555:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2972 on theBenchmark for (2972ds/36816Mi)
% 25.62/4.24 % (2370853)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=631112613:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2972 on theBenchmark for (2972ds/273Mi)
% 25.62/4.24 % (2370849)------------------------------
% 25.62/4.24 % (2370849)------------------------------
% 25.62/4.24 % (2370842)Instruction limit reached!
% 25.62/4.24 % (2370842)------------------------------
% 25.62/4.24 % (2370842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370842)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370842)Termination reason: Instruction limit
% 25.62/4.24 % (2370842)Termination phase: Saturation
% 25.62/4.24 % (2370842)Time elapsed: 0.371 s
% 25.62/4.24 % (2370842)Peak memory usage: 98 MB
% 25.62/4.24 % (2370842)Instructions burned: 1094 (million)
% 25.62/4.24 % (2370853)Instruction limit reached!
% 25.62/4.24 % (2370853)------------------------------
% 25.62/4.24 % (2370853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370853)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370853)Termination reason: Instruction limit
% 25.62/4.24 % (2370853)Termination phase: Saturation
% 25.62/4.24 % (2370853)Time elapsed: 0.092 s
% 25.62/4.24 % (2370853)Peak memory usage: 93 MB
% 25.62/4.24 % (2370853)Instructions burned: 275 (million)
% 25.62/4.24 % (2370847)Instruction limit reached!
% 25.62/4.24 % (2370847)------------------------------
% 25.62/4.24 % (2370847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370847)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370847)Termination reason: Instruction limit
% 25.62/4.24 % (2370847)Termination phase: Saturation
% 25.62/4.24 % (2370847)Time elapsed: 0.301 s
% 25.62/4.24 % (2370847)Peak memory usage: 122 MB
% 25.62/4.24 % (2370847)Instructions burned: 870 (million)
% 25.62/4.24 % (2370856)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=3847480691:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2970 on theBenchmark for (2970ds/863Mi)
% 25.62/4.24 % (2370857)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=279297469:i=5811:kws=precedence:nm=0:rtra=on_2970 on theBenchmark for (2970ds/5811Mi)
% 25.62/4.24 % (2370858)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=3962826197:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2970 on theBenchmark for (2970ds/2216Mi)
% 25.62/4.24 % (2370859)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3407864921:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2969 on theBenchmark for (2969ds/801Mi)
% 25.62/4.24 % (2370800)Instruction limit reached!
% 25.62/4.24 % (2370800)------------------------------
% 25.62/4.24 % (2370800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370800)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370800)Termination reason: Instruction limit
% 25.62/4.24 % (2370800)Termination phase: Saturation
% 25.62/4.24 % (2370800)Time elapsed: 1.508 s
% 25.62/4.24 % (2370800)Peak memory usage: 116 MB
% 25.62/4.24 % (2370800)Instructions burned: 4429 (million)
% 25.62/4.24 % (2370864)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1361040829:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2968 on theBenchmark for (2968ds/1026Mi)
% 25.62/4.24 % (2370856)Instruction limit reached!
% 25.62/4.24 % (2370856)------------------------------
% 25.62/4.24 % (2370856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370856)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370856)Termination reason: Instruction limit
% 25.62/4.24 % (2370856)Termination phase: Saturation
% 25.62/4.24 % (2370856)Time elapsed: 0.298 s
% 25.62/4.24 % (2370856)Peak memory usage: 123 MB
% 25.62/4.24 % (2370856)Instructions burned: 867 (million)
% 25.62/4.24 % (2370859)Instruction limit reached!
% 25.62/4.24 % (2370859)------------------------------
% 25.62/4.24 % (2370859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370859)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370859)Termination reason: Instruction limit
% 25.62/4.24 % (2370859)Termination phase: Saturation
% 25.62/4.24 % (2370859)Time elapsed: 0.245 s
% 25.62/4.24 % (2370859)Peak memory usage: 99 MB
% 25.62/4.24 % (2370859)Instructions burned: 802 (million)
% 25.62/4.24 % (2370866)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4219907423:i=3509:rtra=on_2966 on theBenchmark for (2966ds/3509Mi)
% 25.62/4.24 % (2370867)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=531023224:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2966 on theBenchmark for (2966ds/2127Mi)
% 25.62/4.24 % (2370858)First to succeed.
% 25.62/4.24 % (2370858)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2370469"
% 25.62/4.24 % (2370864)Instruction limit reached!
% 25.62/4.24 % (2370864)------------------------------
% 25.62/4.24 % (2370864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.62/4.24 % (2370864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.62/4.24 % (2370864)CaDiCaL version: 2.1.3
% 25.62/4.24 % (2370864)Termination reason: Instruction limit
% 25.62/4.24 % (2370864)Termination phase: Saturation
% 25.62/4.24 % (2370864)Time elapsed: 0.331 s
% 25.62/4.24 % (2370864)Peak memory usage: 97 MB
% 25.62/4.24 % (2370864)Instructions burned: 1027 (million)
% 25.62/4.24 % (2370870)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2818300041:i=1959:rtra=on:fsd=on:proc=on_2964 on theBenchmark for (2964ds/1959Mi)
% 25.62/4.24 % (2370858)Refutation found. Thanks to Tanya!
% 25.62/4.24 % SZS status Theorem for theBenchmark
% 25.62/4.24 % SZS output start Proof for theBenchmark
% See solution above
% 26.06/4.34 % (2370858)------------------------------
% 26.06/4.34 % (2370858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.06/4.34 % (2370858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.06/4.34 % (2370858)CaDiCaL version: 2.1.3
% 26.06/4.34 % (2370858)Termination reason: Refutation
% 26.06/4.34 % (2370858)Time elapsed: 0.464 s
% 26.06/4.34 % (2370858)Peak memory usage: 129 MB
% 26.06/4.34 % (2370858)Instructions burned: 1357 (million)
% 26.06/4.34 % (2370858)------------------------------
% 26.06/4.34 % (2370858)------------------------------
% 26.06/4.34 % (2370469)Success in time 3.676 s
% 26.06/4.34 % Vampire exiting
%------------------------------------------------------------------------------