Vampire-SAT---5.0.1.THM-Ref.s

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

% Computer : n005.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:39:28 AM UTC 2026

% Result   : Theorem 136.89s 19.89s
% Output   : Refutation 138.09s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   16
%            Number of leaves      :   15
% Syntax   : Number of formulae    :   94 (  11 unt;   0 typ;   9 def)
%            Number of atoms       :  216 (   0 equ)
%            Maximal formula atoms :    4 (   2 avg)
%            Number of connectives :  251 ( 129   ~;  93   |;   1   &)
%                                         (  15 <=>;  12  =>;   0  <=;   1 <~>)
%            Maximal formula depth :    8 (   4 avg)
%            Maximal term depth    :    6 (   2 avg)
%            Number arithmetic     :   52 (  29 atm;   0 fun;  23 num;   0 var)
%            Number of types       :   38 (  36 usr;   1 ari;   0 dat;   0 cdt)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :   29 (  27 usr;  10 prp; 0-3 aty)
%            Number of functors    :  346 ( 345 usr;  22 con; 0-4 aty)
%            Number of variables   :  130 (   0 sgn 107   !;  23   ?; 130   :)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

tff(func_def_0,type,
    'uua$': 'Int_int_bool_fun_fun$' ).

tff(func_def_1,type,
    'w$': 'Nat_a_set_fun$' ).

tff(func_def_2,type,
    'af_letter$': 'A_ltln_a_set_a_ltln_fun_fun$' ).

tff(func_def_3,type,
    'fun_app$m': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_4,type,
    'uu$': 'A_ltln_set$' > 'A_ltln_bool_fun$' ).

tff(func_def_5,type,
    'false_ltln$': 'A_ltln$' ).

tff(func_def_6,type,
    'fun_app$p': ( 'A_ltln_bool_fun_int_fun$' * 'A_ltln_bool_fun$' ) > $int ).

tff(func_def_7,type,
    'nil$': 'A_set_list$' ).

tff(func_def_8,type,
    'append$': 'A_set_list$' > 'A_set_list_a_set_list_fun$' ).

tff(func_def_9,type,
    'fun_app$g': ( 'Nat_int_fun$' * 'Nat$' ) > $int ).

tff(func_def_10,type,
    'cons$a': ( 'A_set_list$' * 'A_set_list_list$' ) > 'A_set_list_list$' ).

tff(func_def_11,type,
    'fun_app$f': ( 'Nat_a_set_list_fun$' * 'Nat$' ) > 'A_set_list$' ).

tff(func_def_12,type,
    'fun_app$h': ( 'A_ltln_a_ltln_a_set_a_ltln_fun_fun_fun$' * 'A_ltln$' ) > 'A_ltln_a_set_a_ltln_fun_fun$' ).

tff(func_def_13,type,
    'nil$a': 'A_set_list_list$' ).

tff(func_def_14,type,
    'cons$': ( 'A_set$' * 'A_set_list$' ) > 'A_set_list$' ).

tff(func_def_15,type,
    'mu_LTL$': 'A_ltln_set$' ).

tff(func_def_16,type,
    'fun_app$d': ( 'A_set_list_a_ltln_fun$' * 'A_set_list$' ) > 'A_ltln$' ).

tff(func_def_17,type,
    'of_nat$': 'Nat_int_fun$' ).

tff(func_def_18,type,
    'fun_app$a': ( 'Int_int_bool_fun_fun$' * $int ) > 'Int_bool_fun$' ).

tff(func_def_19,type,
    'product_lists$': 'A_set_list_list$' > 'A_set_list_list$' ).

tff(func_def_20,type,
    'collect$': 'A_ltln_bool_fun$' > 'A_ltln_set$' ).

tff(func_def_21,type,
    'fun_app$x': ( 'A_set_list_a_set_list_bool_fun_fun$' * 'A_set_list$' ) > 'A_set_list_bool_fun$' ).

tff(func_def_22,type,
    'fun_app$c': ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln$' ) > 'A_ltln_bool_fun$' ).

tff(func_def_23,type,
    'fun_app$s': ( 'Int_int_fun$' * $int ) > $int ).

tff(func_def_24,type,
    tltrue: tlbool ).

tff(func_def_25,type,
    'af_letter_F$': 'A_ltln_a_ltln_bool_fun_fun$' > 'A_ltln_a_ltln_a_set_a_ltln_fun_fun_fun$' ).

tff(func_def_26,type,
    'ltl_prop_equiv$': 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_27,type,
    'ltl_const_equiv$': 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_28,type,
    'fun_app$y': ( 'A_set_list_a_set_list_list_fun$' * 'A_set_list$' ) > 'A_set_list_list$' ).

tff(func_def_29,type,
    'eq$': 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_30,type,
    'until_ltln$': 'A_ltln$' > 'A_ltln_a_ltln_fun$' ).

tff(func_def_31,type,
    'fun_app$j': ( 'A_ltln_a_set_a_ltln_fun_fun$' * 'A_ltln$' ) > 'A_set_a_ltln_fun$' ).

tff(func_def_32,type,
    'foldl$': ( 'A_ltln_a_set_a_ltln_fun_fun$' * 'A_ltln$' ) > 'A_set_list_a_ltln_fun$' ).

tff(func_def_33,type,
    'ltl_lang_equiv$': 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_34,type,
    'fun_app$u': ( 'A_ltln_a_ltln_bool_fun_fun_int_fun$' * 'A_ltln_a_ltln_bool_fun_fun$' ) > $int ).

tff(func_def_35,type,
    'fun_app$k': ( 'A_set_list_a_set_list_fun$' * 'A_set_list$' ) > 'A_set_list$' ).

tff(func_def_36,type,
    'fun_app$e': ( 'A_ltln_a_ltln_fun$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_37,type,
    'true_ltln$': 'A_ltln$' ).

tff(func_def_38,type,
    'fun_app$o': ( 'A_ltln_a_ltln_bool_fun_fun_a_ltln_bool_fun_fun$' * 'A_ltln_a_ltln_bool_fun_fun$' ) > 'A_ltln_bool_fun$' ).

tff(func_def_39,type,
    'ltl_prop_implies$': 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_40,type,
    'semantics_ltln$': 'Nat_a_set_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_41,type,
    'n_lists$': 'Nat$' > 'A_set_list_a_set_list_list_fun$' ).

tff(func_def_42,type,
    tlfalse: tlbool ).

tff(func_def_43,type,
    'fun_app$ab': ( 'Nat_nat_bool_fun_fun$' * 'Nat$' ) > 'Nat_bool_fun$' ).

tff(func_def_44,type,
    'fun_app$v': ( 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' * 'A_ltln_a_ltln_bool_fun_fun$' ) > 'A_ltln_a_ltln_bool_fun_fun$' ).

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

tff(func_def_46,type,
    'fun_app$q': ( 'A_ltln_bool_fun_a_ltln_a_ltln_bool_fun_fun_fun$' * 'A_ltln_bool_fun$' ) > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_47,type,
    'fun_app$aa': ( 'Nat_a_ltln_a_ltln_bool_fun_fun_fun$' * 'Nat$' ) > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_48,type,
    'nu_LTL$': 'A_ltln_set$' ).

tff(func_def_49,type,
    'fun_app$n': ( 'Int_a_ltln_bool_fun_fun$' * $int ) > 'A_ltln_bool_fun$' ).

tff(func_def_50,type,
    'fun_app$z': ( 'Nat_a_set_fun$' * 'Nat$' ) > 'A_set$' ).

tff(func_def_51,type,
    'fun_app$r': ( 'A_ltln_bool_fun_a_ltln_bool_fun_fun$' * 'A_ltln_bool_fun$' ) > 'A_ltln_bool_fun$' ).

tff(func_def_52,type,
    'subsequence$': ( 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat_a_set_list_fun$' ).

tff(func_def_53,type,
    'fun_app$t': ( 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' * $int ) > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_54,type,
    'af_letter_G$': 'A_ltln_a_ltln_bool_fun_fun$' > 'A_ltln_a_ltln_a_set_a_ltln_fun_fun_fun$' ).

tff(func_def_55,type,
    'fun_app$i': ( 'A_set_a_ltln_fun$' * 'A_set$' ) > 'A_ltln$' ).

tff(func_def_56,type,
    'release_ltln$': 'A_ltln$' > 'A_ltln_a_ltln_fun$' ).

tff(func_def_57,type,
    'phi$': 'A_ltln$' ).

tff(func_def_62,type,
    sK0: 'Nat$' ).

tff(func_def_63,type,
    sK1: 'Nat$' ).

tff(func_def_64,type,
    sK2: 'Nat$' > 'Nat$' ).

tff(func_def_65,type,
    sK3: 'Nat$' > 'Nat$' ).

tff(func_def_66,type,
    sK4: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_67,type,
    sK5: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_68,type,
    sK6: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_69,type,
    sK7: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_70,type,
    sK8: ( 'A_set_list$' * 'A_ltln$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_71,type,
    sK9: ( 'A_set_list$' * 'A_ltln$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_72,type,
    sK10: ( 'A_ltln$' * 'A_set_list$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_73,type,
    sK11: ( 'A_ltln$' * 'A_set_list$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_74,type,
    sK12: ( 'A_set_list$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_75,type,
    sK13: ( 'A_set_list$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_76,type,
    sK14: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_77,type,
    sK15: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_78,type,
    sK16: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_79,type,
    sK17: 'Nat_bool_fun$' > 'Nat$' ).

tff(func_def_80,type,
    sK18: ( 'A_ltln_bool_fun$' * 'A_ltln_bool_fun$' ) > 'A_ltln$' ).

tff(func_def_81,type,
    sK19: 'Nat_nat_fun$' > 'Nat$' ).

tff(func_def_82,type,
    sK20: 'Nat_nat_fun$' > 'Nat$' ).

tff(func_def_83,type,
    sK21: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_84,type,
    sK22: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_85,type,
    sK23: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_86,type,
    sK24: 'Nat_bool_fun$' > 'Nat$' ).

tff(func_def_87,type,
    sK25: 'Nat_bool_fun$' > 'Nat$' ).

tff(func_def_88,type,
    sK26: 'Nat_bool_fun$' > 'Nat$' ).

tff(func_def_89,type,
    sK27: 'Nat$' ).

tff(func_def_90,type,
    sK28: 'Nat$' > 'Nat$' ).

tff(func_def_91,type,
    sK29: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_92,type,
    sK30: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_93,type,
    sK31: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_94,type,
    sK32: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_95,type,
    sK33: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_96,type,
    sK34: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_97,type,
    sK35: ( 'A_set_list$' * 'A_set_list$' * 'A_set_list$' * 'A_set_list$' ) > 'A_set_list$' ).

tff(func_def_98,type,
    sK36: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_99,type,
    sK37: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_100,type,
    sK38: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_101,type,
    sK39: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_102,type,
    sK40: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_103,type,
    sK41: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_104,type,
    sK42: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_105,type,
    sK43: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_106,type,
    sK44: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_107,type,
    sK45: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_108,type,
    sK46: ( 'A_set_list$' * 'A_ltln$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_109,type,
    sK47: ( 'A_set_list$' * 'A_ltln$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_110,type,
    sK48: ( 'A_ltln$' * 'A_set_list$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_111,type,
    sK49: ( 'A_ltln$' * 'A_set_list$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_112,type,
    sK50: ( 'A_set_list$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_113,type,
    sK51: ( 'A_set_list$' * 'A_ltln$' ) > 'A_set_list$' ).

tff(func_def_114,type,
    sK52: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_115,type,
    sK53: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_116,type,
    sK54: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_117,type,
    sK55: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_118,type,
    sK56: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_119,type,
    sK57: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_120,type,
    sK58: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_121,type,
    sK59: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_122,type,
    sK60: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln_a_ltln_bool_fun_fun$' ) > 'A_ltln$' ).

tff(func_def_123,type,
    sK61: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln_a_ltln_bool_fun_fun$' ) > 'A_ltln$' ).

tff(func_def_124,type,
    sK62: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_125,type,
    sK63: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_126,type,
    sK64: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_127,type,
    sK65: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_128,type,
    sK66: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_129,type,
    sK67: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_130,type,
    sK68: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_131,type,
    sK69: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_132,type,
    sK70: 'Int_a_ltln_bool_fun_fun$' > $int ).

tff(func_def_133,type,
    sK71: 'Int_a_ltln_bool_fun_fun$' > $int ).

tff(func_def_134,type,
    sK72: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_bool_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_135,type,
    sK73: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_bool_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_136,type,
    sK74: 'A_ltln_bool_fun_int_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_137,type,
    sK75: 'A_ltln_bool_fun_int_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_138,type,
    sK76: 'A_ltln_bool_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_139,type,
    sK77: 'A_ltln_bool_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_140,type,
    sK78: 'A_ltln_bool_fun_a_ltln_bool_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_141,type,
    sK79: 'A_ltln_bool_fun_a_ltln_bool_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_142,type,
    sK80: 'Int_int_fun$' > $int ).

tff(func_def_143,type,
    sK81: 'Int_int_fun$' > $int ).

tff(func_def_144,type,
    sK82: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_145,type,
    sK83: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_146,type,
    sK84: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_147,type,
    sK85: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_148,type,
    sK86: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_149,type,
    sK87: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_150,type,
    sK88: 'Int_a_ltln_bool_fun_fun$' > $int ).

tff(func_def_151,type,
    sK89: 'Int_a_ltln_bool_fun_fun$' > $int ).

tff(func_def_152,type,
    sK90: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_bool_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_153,type,
    sK91: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_bool_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_154,type,
    sK92: 'A_ltln_bool_fun_int_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_155,type,
    sK93: 'A_ltln_bool_fun_int_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_156,type,
    sK94: 'A_ltln_bool_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_157,type,
    sK95: 'A_ltln_bool_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_158,type,
    sK96: 'A_ltln_bool_fun_a_ltln_bool_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_159,type,
    sK97: 'A_ltln_bool_fun_a_ltln_bool_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_160,type,
    sK98: 'Int_int_fun$' > $int ).

tff(func_def_161,type,
    sK99: 'Int_int_fun$' > $int ).

tff(func_def_162,type,
    sK100: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_163,type,
    sK101: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_164,type,
    sK102: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_165,type,
    sK103: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_166,type,
    sK104: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_167,type,
    sK105: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_168,type,
    sK106: 'Int_a_ltln_bool_fun_fun$' > $int ).

tff(func_def_169,type,
    sK107: 'Int_a_ltln_bool_fun_fun$' > $int ).

tff(func_def_170,type,
    sK108: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_bool_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_171,type,
    sK109: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_bool_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_172,type,
    sK110: 'A_ltln_bool_fun_int_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_173,type,
    sK111: 'A_ltln_bool_fun_int_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_174,type,
    sK112: 'A_ltln_bool_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_175,type,
    sK113: 'A_ltln_bool_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_176,type,
    sK114: 'A_ltln_bool_fun_a_ltln_bool_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_177,type,
    sK115: 'A_ltln_bool_fun_a_ltln_bool_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_178,type,
    sK116: 'Int_int_fun$' > $int ).

tff(func_def_179,type,
    sK117: 'Int_int_fun$' > $int ).

tff(func_def_180,type,
    sK118: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_181,type,
    sK119: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_182,type,
    sK120: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_183,type,
    sK121: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_184,type,
    sK122: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_185,type,
    sK123: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_186,type,
    sK124: 'A_ltln_bool_fun_int_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_187,type,
    sK125: 'A_ltln_bool_fun_int_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_188,type,
    sK126: 'A_ltln_bool_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_189,type,
    sK127: 'A_ltln_bool_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_190,type,
    sK128: 'Int_a_ltln_bool_fun_fun$' > $int ).

tff(func_def_191,type,
    sK129: 'Int_a_ltln_bool_fun_fun$' > $int ).

tff(func_def_192,type,
    sK130: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_bool_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_193,type,
    sK131: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_bool_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_194,type,
    sK132: 'A_ltln_bool_fun_a_ltln_bool_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_195,type,
    sK133: 'A_ltln_bool_fun_a_ltln_bool_fun_fun$' > 'A_ltln_bool_fun$' ).

tff(func_def_196,type,
    sK134: 'Int_int_fun$' > $int ).

tff(func_def_197,type,
    sK135: 'Int_int_fun$' > $int ).

tff(func_def_198,type,
    sK136: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_199,type,
    sK137: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_200,type,
    sK138: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_201,type,
    sK139: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_202,type,
    sK140: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_203,type,
    sK141: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_204,type,
    sK142: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_205,type,
    sK143: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_206,type,
    sK144: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_207,type,
    sK145: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_208,type,
    sK151: $int > $int ).

tff(func_def_209,type,
    sK152: $int > $int ).

tff(func_def_210,type,
    sK153: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_211,type,
    sK154: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_212,type,
    sK155: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_213,type,
    sK156: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_214,type,
    sK157: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_215,type,
    sK158: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_216,type,
    sK159: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_217,type,
    sK160: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_218,type,
    sK161: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_219,type,
    sK162: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_220,type,
    sK163: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_221,type,
    sK164: 'Int_int_fun$' > $int ).

tff(func_def_222,type,
    sK165: 'Int_int_fun$' > $int ).

tff(func_def_223,type,
    sK166: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_224,type,
    sK167: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_225,type,
    sK168: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_226,type,
    sK169: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_227,type,
    sK170: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_228,type,
    sK171: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_229,type,
    sK172: 'Int_int_fun$' > $int ).

tff(func_def_230,type,
    sK173: 'Int_int_fun$' > $int ).

tff(func_def_231,type,
    sK174: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_232,type,
    sK175: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_233,type,
    sK176: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_234,type,
    sK177: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_235,type,
    sK178: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_236,type,
    sK179: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_237,type,
    sK180: 'Int_int_fun$' > $int ).

tff(func_def_238,type,
    sK181: 'Int_int_fun$' > $int ).

tff(func_def_239,type,
    sK182: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_240,type,
    sK183: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_241,type,
    sK184: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_242,type,
    sK185: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_243,type,
    sK186: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_244,type,
    sK187: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_245,type,
    sK188: 'Int_int_fun$' > $int ).

tff(func_def_246,type,
    sK189: 'Int_int_fun$' > $int ).

tff(func_def_247,type,
    sK190: 'Int_int_fun$' > $int ).

tff(func_def_248,type,
    sK191: 'Int_int_fun$' > $int ).

tff(func_def_249,type,
    sK192: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_250,type,
    sK193: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_251,type,
    sK194: 'Int_int_fun$' > $int ).

tff(func_def_252,type,
    sK195: 'Int_int_fun$' > $int ).

tff(func_def_253,type,
    sK196: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_254,type,
    sK197: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_255,type,
    sK198: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_256,type,
    sK199: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_257,type,
    sK200: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_258,type,
    sK201: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_259,type,
    sK202: 'Int_int_fun$' > $int ).

tff(func_def_260,type,
    sK203: 'Int_int_fun$' > $int ).

tff(func_def_261,type,
    sK204: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_262,type,
    sK205: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_263,type,
    sK206: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_264,type,
    sK207: 'A_ltln_a_ltln_bool_fun_fun_int_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_265,type,
    sK208: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_266,type,
    sK209: 'A_ltln_a_ltln_bool_fun_fun_a_ltln_a_ltln_bool_fun_fun_fun$' > 'A_ltln_a_ltln_bool_fun_fun$' ).

tff(func_def_267,type,
    sK210: 'Int_int_fun$' > $int ).

tff(func_def_268,type,
    sK211: 'Int_int_fun$' > $int ).

tff(func_def_269,type,
    sK212: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_270,type,
    sK213: 'Int_a_ltln_a_ltln_bool_fun_fun_fun$' > $int ).

tff(func_def_271,type,
    sK214: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_272,type,
    sK215: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_273,type,
    sK216: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_274,type,
    sK217: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_275,type,
    sK218: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_276,type,
    sK219: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_277,type,
    sK220: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_278,type,
    sK221: ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_279,type,
    sK222: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln_a_ltln_bool_fun_fun$' ) > 'A_ltln$' ).

tff(func_def_280,type,
    sK223: ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln_a_ltln_bool_fun_fun$' ) > 'A_ltln$' ).

tff(func_def_281,type,
    sK224: ( 'A_ltln$' * 'A_ltln$' ) > 'Nat_a_set_fun$' ).

tff(func_def_282,type,
    sK225: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).

tff(func_def_283,type,
    sK226: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).

tff(func_def_284,type,
    sK227: 'A_ltln_a_ltln_bool_fun_fun$' > 'A_ltln$' ).

tff(func_def_285,type,
    sK228: 'A_ltln_a_ltln_bool_fun_fun$' > 'A_ltln$' ).

tff(func_def_286,type,
    sK229: 'A_ltln_a_ltln_bool_fun_fun$' > 'A_set$' ).

tff(func_def_287,type,
    sK230: 'A_ltln_a_ltln_bool_fun_fun$' > 'A_ltln$' ).

tff(func_def_288,type,
    sK231: 'A_ltln_a_ltln_bool_fun_fun$' > 'A_ltln$' ).

tff(func_def_289,type,
    sK232: 'A_ltln_a_ltln_bool_fun_fun$' > 'A_set$' ).

tff(func_def_290,type,
    sK233: 'A_set_list$' > 'A_set$' ).

tff(func_def_291,type,
    sK234: 'A_set_list$' > 'A_set_list$' ).

tff(func_def_292,type,
    sK235: 'A_set_list$' > 'A_set$' ).

tff(func_def_293,type,
    sK236: 'A_set_list$' > 'A_set_list$' ).

tff(func_def_294,type,
    sK237: 'A_set_list_list$' > 'A_set$' ).

tff(func_def_295,type,
    sK238: 'A_set_list_list$' > 'A_set_list$' ).

tff(func_def_296,type,
    sK239: 'A_set_list_list$' > 'A_set_list_list$' ).

tff(func_def_297,type,
    sK240: 'A_set_list_list$' > 'A_set_list_list$' ).

tff(func_def_298,type,
    sK241: 'A_set_list$' > 'A_set$' ).

tff(func_def_299,type,
    sK242: 'A_set_list$' > 'A_set$' ).

tff(func_def_300,type,
    sK243: 'A_set_list$' > 'A_set_list$' ).

tff(func_def_301,type,
    sK244: 'A_set_list$' > 'A_set$' ).

tff(func_def_302,type,
    sK245: 'A_set_list$' > 'A_set$' ).

tff(func_def_303,type,
    sK246: 'A_set_list$' > 'A_set_list$' ).

tff(func_def_304,type,
    sK247: 'A_set_list_a_set_list_bool_fun_fun$' > 'A_set$' ).

tff(func_def_305,type,
    sK248: 'A_set_list_a_set_list_bool_fun_fun$' > 'A_set_list$' ).

tff(func_def_306,type,
    sK249: 'A_set_list_a_set_list_bool_fun_fun$' > 'A_set$' ).

tff(func_def_307,type,
    sK250: 'A_set_list_a_set_list_bool_fun_fun$' > 'A_set_list$' ).

tff(func_def_308,type,
    sK251: 'A_set_list_a_set_list_bool_fun_fun$' > 'A_set$' ).

tff(func_def_309,type,
    sK252: 'A_set_list_a_set_list_bool_fun_fun$' > 'A_set_list$' ).

tff(func_def_310,type,
    sK253: 'A_set_list_a_set_list_bool_fun_fun$' > 'A_set$' ).

tff(func_def_311,type,
    sK254: 'A_set_list_a_set_list_bool_fun_fun$' > 'A_set_list$' ).

tff(func_def_312,type,
    sK255: 'A_set_list_bool_fun$' > 'A_set$' ).

tff(func_def_313,type,
    sK256: 'A_set_list_bool_fun$' > 'A_set_list$' ).

tff(func_def_314,type,
    sK257: 'A_set_list_bool_fun$' > 'A_set$' ).

tff(func_def_315,type,
    sK258: 'A_set_list_bool_fun$' > 'A_set$' ).

tff(func_def_316,type,
    sK259: 'A_set_list_bool_fun$' > 'A_set_list$' ).

tff(func_def_317,type,
    sK260: 'A_set_list_bool_fun$' > 'A_set$' ).

tff(func_def_318,type,
    sK261: ( 'A_set_list$' * 'A_set_list$' * 'A_set$' * 'A_set_list$' ) > 'A_set_list$' ).

tff(func_def_319,type,
    sK262: ( 'A_set$' * 'A_set_list$' * 'A_set_list$' * 'A_set_list$' ) > 'A_set_list$' ).

tff(func_def_320,type,
    sK263: 'A_set_list$' > 'A_set_list$' ).

tff(func_def_321,type,
    sK264: 'A_set_list$' > 'A_set$' ).

tff(func_def_322,type,
    sK265: 'A_set_list_bool_fun$' > 'A_set$' ).

tff(func_def_323,type,
    sK266: 'A_set_list_bool_fun$' > 'A_set_list$' ).

tff(func_def_324,type,
    sK267: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_325,type,
    sK268: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).

tff(func_def_326,type,
    sK269: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).

tff(func_def_327,type,
    sK270: 'Nat$' > 'Nat$' ).

tff(func_def_328,type,
    sK271: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).

tff(func_def_329,type,
    sK272: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).

tff(func_def_330,type,
    sK273: 'Nat$' > 'Nat$' ).

tff(func_def_331,type,
    sK274: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_332,type,
    sK275: ( 'Nat$' * 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).

tff(func_def_333,type,
    sK276: ( 'Nat$' * 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).

tff(func_def_334,type,
    sK277: 'Nat_int_fun$' > 'Nat$' ).

tff(func_def_335,type,
    sK278: 'Nat_int_fun$' > 'Nat$' ).

tff(func_def_336,type,
    sK279: 'Nat_int_fun$' > 'Nat$' ).

tff(func_def_337,type,
    sK280: 'Nat_a_ltln_a_ltln_bool_fun_fun_fun$' > 'Nat$' ).

tff(func_def_338,type,
    sK281: 'Nat_int_fun$' > 'Nat$' ).

tff(func_def_339,type,
    sK282: 'Nat_a_ltln_a_ltln_bool_fun_fun_fun$' > 'Nat$' ).

tff(func_def_340,type,
    sK283: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).

tff(func_def_341,type,
    sK284: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).

tff(func_def_342,type,
    sK285: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).

tff(func_def_343,type,
    sK286: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).

tff(func_def_344,type,
    sK287: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).

tff(func_def_345,type,
    sK288: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).

tff(func_def_346,type,
    sK289: 'Nat_bool_fun$' > 'Nat$' ).

tff(func_def_347,type,
    sK290: 'Nat$' > 'Nat$' ).

tff(func_def_348,type,
    sK291: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).

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

tff(pred_def_2,type,
    'less$': ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln_a_ltln_bool_fun_fun$' ) > $o ).

tff(pred_def_3,type,
    'less$a': ( 'A_ltln_bool_fun$' * 'A_ltln_bool_fun$' ) > $o ).

tff(pred_def_4,type,
    'equivp$': 'A_ltln_a_ltln_bool_fun_fun$' > $o ).

tff(pred_def_5,type,
    'fun_app$': ( 'Int_bool_fun$' * $int ) > $o ).

tff(pred_def_6,type,
    'member$': ( 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_7,type,
    'af_congruent$': 'A_ltln_a_ltln_bool_fun_fun$' > $o ).

tff(pred_def_8,type,
    'ltl_equivalence$': 'A_ltln_a_ltln_bool_fun_fun$' > $o ).

tff(pred_def_9,type,
    'fun_app$b': ( 'A_ltln_bool_fun$' * 'A_ltln$' ) > $o ).

tff(pred_def_10,type,
    'transition_functions$': ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln_a_ltln_fun$' ) > $o ).

tff(pred_def_11,type,
    'af_congruent_axioms$': 'A_ltln_a_ltln_bool_fun_fun$' > $o ).

tff(pred_def_12,type,
    'fun_app$l': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).

tff(pred_def_13,type,
    'fun_app$w': ( 'A_set_list_bool_fun$' * 'A_set_list$' ) > $o ).

tff(pred_def_14,type,
    'less_eq$a': ( 'A_ltln_bool_fun$' * 'A_ltln_bool_fun$' ) > $o ).

tff(pred_def_17,type,
    sP146: ( $int * $int * $int ) > $o ).

tff(pred_def_18,type,
    sP147: ( $int * $int * $int ) > $o ).

tff(pred_def_19,type,
    sP148: ( $int * $int * $int ) > $o ).

tff(pred_def_20,type,
    sP149: ( $int * $int * $int ) > $o ).

tff(f3,conjecture,
    ( ? [X0: 'Nat$'] :
      ! [X1: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),X1))),'false_ltln$')
  <=> ? [X0: 'Nat$'] :
      ! [X1: 'Nat$'] :
        ( $less('fun_app$g'('of_nat$',X0),'fun_app$g'('of_nat$',X1))
       => ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),X1))),'false_ltln$') ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture2) ).

tff(f4,negated_conjecture,
    ~ ( ? [X0: 'Nat$'] :
        ! [X1: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),X1))),'false_ltln$')
    <=> ? [X0: 'Nat$'] :
        ! [X1: 'Nat$'] :
          ( $less('fun_app$g'('of_nat$',X0),'fun_app$g'('of_nat$',X1))
         => ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),X1))),'false_ltln$') ) ),
    inference(negated_conjecture,[status(cth)],[f3]) ).

tff(f11,axiom,
    'member$'('phi$','nu_LTL$'),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom9) ).

tff(f14,axiom,
    ! [X0: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( ? [X2: 'Nat$'] :
        ! [X3: 'Nat$'] :
          ( $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',X3))
         => ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),X0),'fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,'nat$'(0)),X3))),'false_ltln$') )
     => ? [X2: 'Nat$'] :
        ! [X3: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X2),X3))),'false_ltln$') ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom12) ).

tff(f15,axiom,
    ! [X0: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( ? [X2: 'Nat$'] :
        ! [X3: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X2),X3))),'false_ltln$')
     => ? [X2: 'Nat$'] :
        ! [X3: 'Nat$'] :
          ( $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',X3))
         => ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),X0),'fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,'nat$'(0)),X3))),'false_ltln$') ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom13) ).

tff(f94,axiom,
    ( 'fun_app$b'('semantics_ltln$'('w$'),'fun_app$e'('until_ltln$'('true_ltln$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')))
  <=> ? [X0: 'Nat$'] :
      ! [X1: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),X1))),'false_ltln$') ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom92) ).

tff(f114,axiom,
    ! [X0: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( 'member$'(X0,'nu_LTL$')
     => ( 'fun_app$b'('semantics_ltln$'(X1),'fun_app$e'('until_ltln$'('true_ltln$'),'fun_app$e'('release_ltln$'('false_ltln$'),X0)))
      <=> ? [X2: 'Nat$'] :
          ! [X3: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X2),X3))),'false_ltln$') ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom112) ).

tff(f784,plain,
    ~ ( ? [X0: 'Nat$'] :
        ! [X1: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),X1))),'false_ltln$')
    <=> ? [X2: 'Nat$'] :
        ! [X3: 'Nat$'] :
          ( $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',X3))
         => ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),X3))),'false_ltln$') ) ),
    inference(rectify,[],[f4]) ).

tff(f785,plain,
    ! [X0: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( ? [X2: 'Nat$'] :
        ! [X3: 'Nat$'] :
          ( $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',X3))
         => ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),X0),'fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,'nat$'(0)),X3))),'false_ltln$') )
     => ? [X4: 'Nat$'] :
        ! [X5: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X4),X5))),'false_ltln$') ),
    inference(rectify,[],[f14]) ).

tff(f786,plain,
    ! [X0: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( ? [X2: 'Nat$'] :
        ! [X3: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X2),X3))),'false_ltln$')
     => ? [X4: 'Nat$'] :
        ! [X5: 'Nat$'] :
          ( $less('fun_app$g'('of_nat$',X4),'fun_app$g'('of_nat$',X5))
         => ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),X0),'fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,'nat$'(0)),X5))),'false_ltln$') ) ),
    inference(rectify,[],[f15]) ).

tff(f824,plain,
    ( ? [X0: 'Nat$'] :
      ! [X1: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),X1))),'false_ltln$')
  <~> ? [X2: 'Nat$'] :
      ! [X3: 'Nat$'] :
        ( ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),X3))),'false_ltln$')
        | ~ $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',X3)) ) ),
    inference(ennf_transformation,[],[f784]) ).

tff(f833,plain,
    ! [X0: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( ? [X4: 'Nat$'] :
        ! [X5: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X4),X5))),'false_ltln$')
      | ! [X2: 'Nat$'] :
        ? [X3: 'Nat$'] :
          ( 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),X0),'fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,'nat$'(0)),X3))),'false_ltln$')
          & $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',X3)) ) ),
    inference(ennf_transformation,[],[f785]) ).

tff(f834,plain,
    ! [X0: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( ? [X4: 'Nat$'] :
        ! [X5: 'Nat$'] :
          ( ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),X0),'fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,'nat$'(0)),X5))),'false_ltln$')
          | ~ $less('fun_app$g'('of_nat$',X4),'fun_app$g'('of_nat$',X5)) )
      | ! [X2: 'Nat$'] :
        ? [X3: 'Nat$'] : 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X2),X3))),'false_ltln$') ),
    inference(ennf_transformation,[],[f786]) ).

tff(f911,plain,
    ! [X0: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( ( 'fun_app$b'('semantics_ltln$'(X1),'fun_app$e'('until_ltln$'('true_ltln$'),'fun_app$e'('release_ltln$'('false_ltln$'),X0)))
      <=> ? [X2: 'Nat$'] :
          ! [X3: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X2),X3))),'false_ltln$') )
      | ~ 'member$'(X0,'nu_LTL$') ),
    inference(ennf_transformation,[],[f114]) ).

tff(f1453,plain,
    ! [X2: 'Nat$',X0: 'Nat$'] :
      ( $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',sK3(X2)))
      | 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),sK2(X0)))),'false_ltln$') ),
    inference(cnf_transformation,[],[f824]) ).

tff(f1454,plain,
    ! [X2: 'Nat$',X0: 'Nat$'] :
      ( 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),sK3(X2)))),'false_ltln$')
      | 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),sK2(X0)))),'false_ltln$') ),
    inference(cnf_transformation,[],[f824]) ).

tff(f1455,plain,
    ! [X3: 'Nat$',X1: 'Nat$'] :
      ( ~ $less('fun_app$g'('of_nat$',sK1),'fun_app$g'('of_nat$',X3))
      | ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),X3))),'false_ltln$')
      | ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK0),X1))),'false_ltln$') ),
    inference(cnf_transformation,[],[f824]) ).

tff(f1462,plain,
    'member$'('phi$','nu_LTL$'),
    inference(cnf_transformation,[],[f11]) ).

tff(f1466,plain,
    ! [X2: 'Nat$',X0: 'A_ltln$',X1: 'Nat_a_set_fun$',X5: 'Nat$'] :
      ( $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',sK5(X0,X1,X2)))
      | ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,sK4(X0,X1)),X5))),'false_ltln$') ),
    inference(cnf_transformation,[],[f833]) ).

tff(f1467,plain,
    ! [X2: 'Nat$',X0: 'A_ltln$',X1: 'Nat_a_set_fun$',X5: 'Nat$'] :
      ( 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),X0),'fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,'nat$'(0)),sK5(X0,X1,X2)))),'false_ltln$')
      | ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,sK4(X0,X1)),X5))),'false_ltln$') ),
    inference(cnf_transformation,[],[f833]) ).

tff(f1468,plain,
    ! [X2: 'Nat$',X0: 'A_ltln$',X1: 'Nat_a_set_fun$',X5: 'Nat$'] :
      ( 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X2),sK7(X0,X1,X2)))),'false_ltln$')
      | ~ $less('fun_app$g'('of_nat$',sK6(X0,X1)),'fun_app$g'('of_nat$',X5))
      | ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),X0),'fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,'nat$'(0)),X5))),'false_ltln$') ),
    inference(cnf_transformation,[],[f834]) ).

tff(f1577,plain,
    ! [X1: 'Nat$'] :
      ( ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK27),X1))),'false_ltln$')
      | ~ 'fun_app$b'('semantics_ltln$'('w$'),'fun_app$e'('until_ltln$'('true_ltln$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$'))) ),
    inference(cnf_transformation,[],[f94]) ).

tff(f1611,plain,
    ! [X2: 'Nat$',X0: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( ~ 'member$'(X0,'nu_LTL$')
      | 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X2),sK32(X0,X1,X2)))),'false_ltln$')
      | 'fun_app$b'('semantics_ltln$'(X1),'fun_app$e'('until_ltln$'('true_ltln$'),'fun_app$e'('release_ltln$'('false_ltln$'),X0))) ),
    inference(cnf_transformation,[],[f911]) ).

tff(f2561,plain,
    ! [X3: 'Nat$',X1: 'Nat$'] :
      ( ~ $less('fun_app$g'('of_nat$',sK1),'fun_app$g'('of_nat$',X3))
      | 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),X3))),'false_ltln$')
      | 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK0),X1))),'false_ltln$') ),
    inference(consistent_polarity_flipping,[],[f1455]) ).

tff(f2562,plain,
    ! [X2: 'Nat$',X0: 'Nat$'] :
      ( ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),sK3(X2)))),'false_ltln$')
      | ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),sK2(X0)))),'false_ltln$') ),
    inference(consistent_polarity_flipping,[],[f1454]) ).

tff(f2563,plain,
    ! [X2: 'Nat$',X0: 'Nat$'] :
      ( $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',sK3(X2)))
      | ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),sK2(X0)))),'false_ltln$') ),
    inference(consistent_polarity_flipping,[],[f1453]) ).

tff(f2573,plain,
    ! [X2: 'Nat$',X0: 'A_ltln$',X1: 'Nat_a_set_fun$',X5: 'Nat$'] :
      ( ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),X0),'fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,'nat$'(0)),sK5(X0,X1,X2)))),'false_ltln$')
      | 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,sK4(X0,X1)),X5))),'false_ltln$') ),
    inference(consistent_polarity_flipping,[],[f1467]) ).

tff(f2574,plain,
    ! [X2: 'Nat$',X0: 'A_ltln$',X1: 'Nat_a_set_fun$',X5: 'Nat$'] :
      ( 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,sK4(X0,X1)),X5))),'false_ltln$')
      | $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',sK5(X0,X1,X2))) ),
    inference(consistent_polarity_flipping,[],[f1466]) ).

tff(f2575,plain,
    ! [X2: 'Nat$',X0: 'A_ltln$',X1: 'Nat_a_set_fun$',X5: 'Nat$'] :
      ( ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X2),sK7(X0,X1,X2)))),'false_ltln$')
      | ~ $less('fun_app$g'('of_nat$',sK6(X0,X1)),'fun_app$g'('of_nat$',X5))
      | 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),X0),'fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,'nat$'(0)),X5))),'false_ltln$') ),
    inference(consistent_polarity_flipping,[],[f1468]) ).

tff(f2614,plain,
    ! [X1: 'Nat$'] :
      ( 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK27),X1))),'false_ltln$')
      | 'fun_app$b'('semantics_ltln$'('w$'),'fun_app$e'('until_ltln$'('true_ltln$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$'))) ),
    inference(consistent_polarity_flipping,[],[f1577]) ).

tff(f2635,plain,
    ! [X2: 'Nat$',X0: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( ~ 'fun_app$b'('semantics_ltln$'(X1),'fun_app$e'('until_ltln$'('true_ltln$'),'fun_app$e'('release_ltln$'('false_ltln$'),X0)))
      | ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),X0)),'fun_app$f'('subsequence$'(X1,X2),sK32(X0,X1,X2)))),'false_ltln$')
      | ~ 'member$'(X0,'nu_LTL$') ),
    inference(consistent_polarity_flipping,[],[f1611]) ).

tff(f2993,definition,
    ( spl292_16
  <=> 'fun_app$b'('semantics_ltln$'('w$'),'fun_app$e'('until_ltln$'('true_ltln$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$'))) ),
    introduced(definition,[new_symbols(definition,[spl292_16])],[avatar_definition]) ).

tff(f2994,plain,
    ( 'fun_app$b'('semantics_ltln$'('w$'),'fun_app$e'('until_ltln$'('true_ltln$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')))
    | ~ spl292_16 ),
    inference(avatar_component_clause,[],[f2993]) ).

tff(f3001,definition,
    ( spl292_18
  <=> ! [X1: 'Nat$'] : 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK27),X1))),'false_ltln$') ),
    introduced(definition,[new_symbols(definition,[spl292_18])],[avatar_definition]) ).

tff(f3002,plain,
    ( ! [X1: 'Nat$'] : 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK27),X1))),'false_ltln$')
    | ~ spl292_18 ),
    inference(avatar_component_clause,[],[f3001]) ).

tff(f3003,plain,
    ( spl292_16
    | spl292_18 ),
    inference(avatar_split_clause,[],[f2614,f3001,f2993]) ).

tff(f3006,definition,
    ( spl292_19
  <=> ! [X0: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),sK2(X0)))),'false_ltln$') ),
    introduced(definition,[new_symbols(definition,[spl292_19])],[avatar_definition]) ).

tff(f3007,plain,
    ( ! [X0: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),sK2(X0)))),'false_ltln$')
    | ~ spl292_19 ),
    inference(avatar_component_clause,[],[f3006]) ).

tff(f3009,definition,
    ( spl292_20
  <=> ! [X2: 'Nat$'] : $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',sK3(X2))) ),
    introduced(definition,[new_symbols(definition,[spl292_20])],[avatar_definition]) ).

tff(f3010,plain,
    ( ! [X2: 'Nat$'] : $less('fun_app$g'('of_nat$',X2),'fun_app$g'('of_nat$',sK3(X2)))
    | ~ spl292_20 ),
    inference(avatar_component_clause,[],[f3009]) ).

tff(f3011,plain,
    ( spl292_19
    | spl292_20 ),
    inference(avatar_split_clause,[],[f2563,f3009,f3006]) ).

tff(f3013,definition,
    ( spl292_21
  <=> ! [X2: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),sK3(X2)))),'false_ltln$') ),
    introduced(definition,[new_symbols(definition,[spl292_21])],[avatar_definition]) ).

tff(f3014,plain,
    ( ! [X2: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),sK3(X2)))),'false_ltln$')
    | ~ spl292_21 ),
    inference(avatar_component_clause,[],[f3013]) ).

tff(f3015,plain,
    ( spl292_19
    | spl292_21 ),
    inference(avatar_split_clause,[],[f2562,f3013,f3006]) ).

tff(f3017,definition,
    ( spl292_22
  <=> ! [X1: 'Nat$'] : 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK0),X1))),'false_ltln$') ),
    introduced(definition,[new_symbols(definition,[spl292_22])],[avatar_definition]) ).

tff(f3018,plain,
    ( ! [X1: 'Nat$'] : 'fun_app$b'('fun_app$c'('ltl_lang_equiv$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK0),X1))),'false_ltln$')
    | ~ spl292_22 ),
    inference(avatar_component_clause,[],[f3017]) ).

tff(f3020,definition,
    ( spl292_23
  <=> ! [X3: 'Nat$'] :
        ( ~ $less('fun_app$g'('of_nat$',sK1),'fun_app$g'('of_nat$',X3))
        | 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),X3))),'false_ltln$') ) ),
    introduced(definition,[new_symbols(definition,[spl292_23])],[avatar_definition]) ).

tff(f3021,plain,
    ( ! [X3: 'Nat$'] :
        ( 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),X3))),'false_ltln$')
        | ~ $less('fun_app$g'('of_nat$',sK1),'fun_app$g'('of_nat$',X3)) )
    | ~ spl292_23 ),
    inference(avatar_component_clause,[],[f3020]) ).

tff(f3022,plain,
    ( spl292_22
    | spl292_23 ),
    inference(avatar_split_clause,[],[f2561,f3020,f3017]) ).

tff(f3024,plain,
    ( $false
    | ~ spl292_19
    | ~ spl292_22 ),
    inference(resolution,[],[f3007,f3018]) ).

tff(f3025,plain,
    ( ~ spl292_19
    | ~ spl292_22 ),
    inference(avatar_contradiction_clause,[],[f3024]) ).

tff(f4412,plain,
    ( ! [X0: 'Nat$'] : ~ $less('fun_app$g'('of_nat$',sK1),'fun_app$g'('of_nat$',sK3(X0)))
    | ~ spl292_21
    | ~ spl292_23 ),
    inference(resolution,[],[f3021,f3014]) ).

tff(f4437,plain,
    ( $false
    | ~ spl292_20
    | ~ spl292_21
    | ~ spl292_23 ),
    inference(resolution,[],[f4412,f3010]) ).

tff(f4451,plain,
    ( ~ spl292_20
    | ~ spl292_21
    | ~ spl292_23 ),
    inference(avatar_contradiction_clause,[],[f4437]) ).

tff(f5523,plain,
    ( $false
    | ~ spl292_18
    | ~ spl292_19 ),
    inference(resolution,[],[f3007,f3002]) ).

tff(f5525,plain,
    ( ~ spl292_18
    | ~ spl292_19 ),
    inference(avatar_contradiction_clause,[],[f5523]) ).

tff(f7612,plain,
    ( ! [X0: 'Nat$'] :
        ( 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('fun_app$h'('af_letter_G$'('eq$'),'phi$'),'fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$','nat$'(0)),X0))),'false_ltln$')
        | ~ $less('fun_app$g'('of_nat$',sK6('phi$','w$')),'fun_app$g'('of_nat$',X0)) )
    | ~ spl292_22 ),
    inference(resolution,[],[f2575,f3018]) ).

tff(f8082,plain,
    ( ! [X0: 'Nat$'] : ~ $less('fun_app$g'('of_nat$',sK6('phi$','w$')),'fun_app$g'('of_nat$',sK3(X0)))
    | ~ spl292_21
    | ~ spl292_22 ),
    inference(resolution,[],[f7612,f3014]) ).

tff(f8097,definition,
    ( spl292_113
  <=> ! [X1: 'Nat$'] : 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK4('phi$','w$')),X1))),'false_ltln$') ),
    introduced(definition,[new_symbols(definition,[spl292_113])],[avatar_definition]) ).

tff(f8098,plain,
    ( ! [X1: 'Nat$'] : 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK4('phi$','w$')),X1))),'false_ltln$')
    | ~ spl292_113 ),
    inference(avatar_component_clause,[],[f8097]) ).

tff(f8128,definition,
    ( spl292_115
  <=> ! [X0: 'Nat$'] : ~ $less('fun_app$g'('of_nat$',sK1),'fun_app$g'('of_nat$',sK5('phi$','w$',X0))) ),
    introduced(definition,[new_symbols(definition,[spl292_115])],[avatar_definition]) ).

tff(f8129,plain,
    ( ! [X0: 'Nat$'] : ~ $less('fun_app$g'('of_nat$',sK1),'fun_app$g'('of_nat$',sK5('phi$','w$',X0)))
    | ~ spl292_115 ),
    inference(avatar_component_clause,[],[f8128]) ).

tff(f8135,plain,
    ( ! [X0: 'Nat$'] :
        ( ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),sK32('phi$','w$',X0)))),'false_ltln$')
        | ~ 'member$'('phi$','nu_LTL$') )
    | ~ spl292_16 ),
    inference(resolution,[],[f2994,f2635]) ).

tff(f8150,plain,
    ( ! [X0: 'Nat$'] : ~ 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',X0),sK32('phi$','w$',X0)))),'false_ltln$')
    | ~ spl292_16 ),
    inference(forward_subsumption_resolution,[],[f8135,f1462]) ).

tff(f8375,plain,
    ( ! [X0: 'Nat$',X1: 'Nat$'] :
        ( ~ $less('fun_app$g'('of_nat$',sK1),'fun_app$g'('of_nat$',sK5('phi$','w$',X0)))
        | 'fun_app$b'('fun_app$c'('eq$','fun_app$d'('foldl$'('af_letter$','fun_app$e'('release_ltln$'('false_ltln$'),'phi$')),'fun_app$f'('subsequence$'('w$',sK4('phi$','w$')),X1))),'false_ltln$') )
    | ~ spl292_23 ),
    inference(resolution,[],[f3021,f2573]) ).

tff(f8384,plain,
    ( spl292_113
    | spl292_115
    | ~ spl292_23 ),
    inference(avatar_split_clause,[],[f8375,f3020,f8128,f8097]) ).

tff(f26582,plain,
    ( ! [X0: 'Nat$'] : $less('fun_app$g'('of_nat$',X0),'fun_app$g'('of_nat$',sK5('phi$','w$',X0)))
    | ~ spl292_16 ),
    inference(resolution,[],[f8150,f2574]) ).

tff(f171899,plain,
    ( $false
    | ~ spl292_16
    | ~ spl292_113 ),
    inference(resolution,[],[f8098,f8150]) ).

tff(f171914,plain,
    ( ~ spl292_16
    | ~ spl292_113 ),
    inference(avatar_contradiction_clause,[],[f171899]) ).

tff(f350823,plain,
    ( $false
    | ~ spl292_16
    | ~ spl292_115 ),
    inference(resolution,[],[f26582,f8129]) ).

tff(f350968,plain,
    ( ~ spl292_16
    | ~ spl292_115 ),
    inference(avatar_contradiction_clause,[],[f350823]) ).

tff(f359128,plain,
    ( $false
    | ~ spl292_20
    | ~ spl292_21
    | ~ spl292_22 ),
    inference(resolution,[],[f8082,f3010]) ).

tff(f359220,plain,
    ( ~ spl292_20
    | ~ spl292_21
    | ~ spl292_22 ),
    inference(avatar_contradiction_clause,[],[f359128]) ).

cnf(s31,plain,
    ( spl292_16
    | spl292_18 ),
    inference(sat_conversion,[],[f3003]) ).

cnf(s34,plain,
    ( spl292_19
    | spl292_20 ),
    inference(sat_conversion,[],[f3011]) ).

cnf(s35,plain,
    ( spl292_19
    | spl292_21 ),
    inference(sat_conversion,[],[f3015]) ).

cnf(s36,plain,
    ( spl292_22
    | spl292_23 ),
    inference(sat_conversion,[],[f3022]) ).

cnf(s38,plain,
    ( ~ spl292_19
    | ~ spl292_22 ),
    inference(sat_conversion,[],[f3025]) ).

cnf(s74,plain,
    ( ~ spl292_20
    | ~ spl292_21
    | ~ spl292_23 ),
    inference(sat_conversion,[],[f4451]) ).

cnf(s118,plain,
    ( ~ spl292_18
    | ~ spl292_19 ),
    inference(sat_conversion,[],[f5525]) ).

cnf(s170,plain,
    ( ~ spl292_23
    | spl292_113
    | spl292_115 ),
    inference(sat_conversion,[],[f8384]) ).

cnf(s3285,plain,
    ( ~ spl292_16
    | ~ spl292_113 ),
    inference(sat_conversion,[],[f171914]) ).

cnf(s21477,plain,
    ( ~ spl292_16
    | ~ spl292_115 ),
    inference(sat_conversion,[],[f350968]) ).

cnf(s23425,plain,
    ( ~ spl292_20
    | ~ spl292_21
    | ~ spl292_22 ),
    inference(sat_conversion,[],[f359220]) ).

cnf(s24094,plain,
    ( ~ spl292_20
    | ~ spl292_21 ),
    inference(rat,[],[s36,s74,s23425]) ).

cnf(s24095,plain,
    spl292_19,
    inference(rat,[],[s24094,s34,s35]) ).

cnf(s24098,plain,
    ~ spl292_18,
    inference(rat,[],[s118,s24095]) ).

cnf(s24099,plain,
    ~ spl292_22,
    inference(rat,[],[s38,s24095]) ).

cnf(s24100,plain,
    spl292_16,
    inference(rat,[],[s31,s24098]) ).

cnf(s24101,plain,
    spl292_23,
    inference(rat,[],[s36,s24099]) ).

cnf(s24102,plain,
    ~ spl292_115,
    inference(rat,[],[s21477,s24100]) ).

cnf(s24103,plain,
    ~ spl292_113,
    inference(rat,[],[s3285,s24100]) ).

cnf(s24107,plain,
    $false,
    inference(rat,[],[s170,s24101,s24102,s24103]) ).

tff(f359280,plain,
    $false,
    inference(avatar_sat_refutation,[],[s24107]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : ITP375_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.36  % Computer : n005.cluster.edu
% 0.09/0.36  % Model    : x86_64 x86_64
% 0.09/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36  % Memory   : 8046.5625MB
% 0.09/0.36  % OS       : Linux 6.8.0-71-generic
% 0.09/0.36  % CPULimit : 300
% 0.09/0.36  % WCLimit  : 300
% 0.09/0.36  % DateTime : Sun Sep 27 12:56:02 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 0.09/0.36  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.40  Running first-order model finding
% 0.09/0.40  Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.16/1.09  % (3966783)Will run a generic schedule for satisfiability detection.
% 4.16/1.09  % (3966792)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2900786302:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.16/1.09  % (3966789)% WARNING: option uhcvi not known.
% 4.16/1.09  % (3966788)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4148985519_2999 on theBenchmark for (2999ds/0Mi)
% 4.16/1.09  % (3966789)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3091913420:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.16/1.09  % (3966790)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1640375450:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.16/1.09  % (3966791)dis+10_1_sil=32000:sp=arity:random_seed=4096833088:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.16/1.09  % (3966793)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2651186639:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.16/1.09  % (3966794)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3875169747:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.16/1.09  % (3966792)Instruction limit reached! 
% 4.16/1.09  % (3966792)------------------------------
% 4.16/1.09  % (3966792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.09  % (3966792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.09  % (3966792)CaDiCaL version: 2.1.3
% 4.16/1.09  % (3966792)Termination reason: Instruction limit
% 4.16/1.09  % (3966792)Termination phase: Saturation
% 4.16/1.09  % (3966792)Time elapsed: 0.031 s
% 4.16/1.09  % (3966792)Peak memory usage: 13 MB
% 4.16/1.09  % (3966792)Instructions burned: 116 (million)
% 4.16/1.09  % (3966802)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=399762208:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.16/1.09  % (3966788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.16/1.09  % (3966788)Terminated due to inappropriate strategy.
% 4.16/1.09  % (3966788)------------------------------
% 4.16/1.09  % (3966788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.09  % (3966788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.09  % (3966788)CaDiCaL version: 2.1.3
% 4.16/1.09  % (3966788)Termination reason: Inappropriate
% 4.16/1.09  % (3966788)Time elapsed: 0.036 s
% 4.16/1.09  % (3966788)Peak memory usage: 12 MB
% 4.16/1.09  % (3966788)Instructions burned: 76 (million)
% 4.16/1.09  % (3966788)------------------------------
% 4.16/1.09  % (3966788)------------------------------
% 4.16/1.09  % (3966802)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.16/1.09  % (3966802)Terminated due to inappropriate strategy.
% 4.16/1.09  % (3966802)------------------------------
% 4.16/1.09  % (3966802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.09  % (3966802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.09  % (3966802)CaDiCaL version: 2.1.3
% 4.16/1.09  % (3966802)Termination reason: Inappropriate
% 4.16/1.09  % (3966802)Time elapsed: 0.017 s
% 4.16/1.09  % (3966802)Peak memory usage: 12 MB
% 4.16/1.09  % (3966802)Instructions burned: 65 (million)
% 4.16/1.09  % (3966802)------------------------------
% 4.16/1.09  % (3966802)------------------------------
% 4.16/1.09  % (3966791)Instruction limit reached! 
% 4.16/1.09  % (3966791)------------------------------
% 4.16/1.09  % (3966791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.09  % (3966791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.09  % (3966791)CaDiCaL version: 2.1.3
% 4.16/1.09  % (3966791)Termination reason: Instruction limit
% 4.16/1.09  % (3966791)Termination phase: Saturation
% 4.16/1.09  % (3966791)Time elapsed: 0.055 s
% 4.16/1.09  % (3966791)Peak memory usage: 14 MB
% 4.16/1.09  % (3966791)Instructions burned: 103 (million)
% 4.16/1.09  % (3966804)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=849576677:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 4.16/1.09  % (3966805)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1072088665:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.16/1.09  % (3966793)Instruction limit reached! 
% 4.16/1.09  % (3966793)------------------------------
% 4.16/1.09  % (3966793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.35/1.29  % (3966793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.29  % (3966793)CaDiCaL version: 2.1.3
% 5.35/1.29  % (3966793)Termination reason: Instruction limit
% 5.35/1.29  % (3966793)Termination phase: Saturation
% 5.35/1.29  % (3966793)Time elapsed: 0.074 s
% 5.35/1.29  % (3966793)Peak memory usage: 14 MB
% 5.35/1.29  % (3966793)Instructions burned: 131 (million)
% 5.35/1.29  % (3966807)ott-21_1_sil=16000:fs=off:random_seed=4038998196:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.35/1.29  % (3966794)Instruction limit reached! 
% 5.35/1.29  % (3966794)------------------------------
% 5.35/1.29  % (3966794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.35/1.29  % (3966794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.29  % (3966794)CaDiCaL version: 2.1.3
% 5.35/1.29  % (3966794)Termination reason: Instruction limit
% 5.35/1.29  % (3966794)Termination phase: Saturation
% 5.35/1.29  % (3966794)Time elapsed: 0.091 s
% 5.35/1.29  % (3966794)Peak memory usage: 15 MB
% 5.35/1.29  % (3966794)Instructions burned: 159 (million)
% 5.35/1.29  % (3966809)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=525523500:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.35/1.29  % (3966811)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=147984877:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 5.35/1.29  % (3966804)Instruction limit reached! 
% 5.35/1.29  % (3966804)------------------------------
% 5.35/1.29  % (3966804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.35/1.29  % (3966804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.29  % (3966804)CaDiCaL version: 2.1.3
% 5.35/1.29  % (3966804)Termination reason: Instruction limit
% 5.35/1.29  % (3966804)Termination phase: Saturation
% 5.35/1.29  % (3966804)Time elapsed: 0.065 s
% 5.35/1.29  % (3966804)Peak memory usage: 14 MB
% 5.35/1.29  % (3966804)Instructions burned: 131 (million)
% 5.35/1.29  % (3966811)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.35/1.29  % (3966811)Terminated due to inappropriate strategy.
% 5.35/1.29  % (3966811)------------------------------
% 5.35/1.29  % (3966811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.35/1.29  % (3966811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.29  % (3966811)CaDiCaL version: 2.1.3
% 5.35/1.29  % (3966811)Termination reason: Inappropriate
% 5.35/1.29  % (3966811)Time elapsed: 0.025 s
% 5.35/1.29  % (3966811)Peak memory usage: 12 MB
% 5.35/1.29  % (3966811)Instructions burned: 53 (million)
% 5.35/1.29  % (3966811)------------------------------
% 5.35/1.29  % (3966811)------------------------------
% 5.35/1.29  % (3966814)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3160508566:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 5.35/1.29  % (3966815)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1051346101:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 5.35/1.29  % (3966807)Instruction limit reached! 
% 5.35/1.29  % (3966807)------------------------------
% 5.35/1.29  % (3966807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.35/1.29  % (3966807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.29  % (3966807)CaDiCaL version: 2.1.3
% 5.35/1.29  % (3966807)Termination reason: Instruction limit
% 5.35/1.29  % (3966807)Termination phase: Saturation
% 5.35/1.29  % (3966807)Time elapsed: 0.084 s
% 5.35/1.29  % (3966807)Peak memory usage: 14 MB
% 5.35/1.29  % (3966807)Instructions burned: 180 (million)
% 5.35/1.29  % (3966818)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4204898025:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 5.35/1.29  % (3966815)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.35/1.29  % (3966815)Terminated due to inappropriate strategy.
% 5.35/1.29  % (3966815)------------------------------
% 5.35/1.29  % (3966815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.35/1.29  % (3966815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.29  % (3966815)CaDiCaL version: 2.1.3
% 5.35/1.29  % (3966815)Termination reason: Inappropriate
% 5.35/1.29  % (3966815)Time elapsed: 0.030 s
% 5.35/1.29  % (3966815)Peak memory usage: 12 MB
% 20.99/3.50  % (3966815)Instructions burned: 64 (million)
% 20.99/3.50  % (3966815)------------------------------
% 20.99/3.50  % (3966815)------------------------------
% 20.99/3.50  % (3966820)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1659912392:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 20.99/3.50  % (3966805)Instruction limit reached! 
% 20.99/3.50  % (3966805)------------------------------
% 20.99/3.50  % (3966805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.99/3.50  % (3966805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.50  % (3966805)CaDiCaL version: 2.1.3
% 20.99/3.50  % (3966805)Termination reason: Instruction limit
% 20.99/3.50  % (3966805)Termination phase: Saturation
% 20.99/3.50  % (3966805)Time elapsed: 0.228 s
% 20.99/3.50  % (3966805)Peak memory usage: 18 MB
% 20.99/3.50  % (3966805)Instructions burned: 687 (million)
% 20.99/3.50  % (3966822)fmb+10_1_sil=64000:random_seed=2714327379:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 20.99/3.50  % (3966822)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 20.99/3.50  % (3966822)Terminated due to inappropriate strategy.
% 20.99/3.50  % (3966822)------------------------------
% 20.99/3.50  % (3966822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.99/3.50  % (3966822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.50  % (3966822)CaDiCaL version: 2.1.3
% 20.99/3.50  % (3966822)Termination reason: Inappropriate
% 20.99/3.50  % (3966822)Time elapsed: 0.017 s
% 20.99/3.50  % (3966822)Peak memory usage: 12 MB
% 20.99/3.50  % (3966822)Instructions burned: 70 (million)
% 20.99/3.50  % (3966822)------------------------------
% 20.99/3.50  % (3966822)------------------------------
% 20.99/3.50  % (3966824)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3154155435:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 20.99/3.50  % (3966824)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 20.99/3.50  % (3966824)Terminated due to inappropriate strategy.
% 20.99/3.50  % (3966824)------------------------------
% 20.99/3.50  % (3966824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.99/3.50  % (3966824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.50  % (3966824)CaDiCaL version: 2.1.3
% 20.99/3.50  % (3966824)Termination reason: Inappropriate
% 20.99/3.50  % (3966824)Time elapsed: 0.030 s
% 20.99/3.50  % (3966824)Peak memory usage: 12 MB
% 20.99/3.50  % (3966824)Instructions burned: 65 (million)
% 20.99/3.50  % (3966824)------------------------------
% 20.99/3.50  % (3966824)------------------------------
% 20.99/3.50  % (3966826)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=752853081:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 20.99/3.50  % (3966809)Instruction limit reached! 
% 20.99/3.50  % (3966809)------------------------------
% 20.99/3.50  % (3966809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.99/3.50  % (3966809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.50  % (3966809)CaDiCaL version: 2.1.3
% 20.99/3.50  % (3966809)Termination reason: Instruction limit
% 20.99/3.50  % (3966809)Termination phase: Saturation
% 20.99/3.50  % (3966809)Time elapsed: 0.301 s
% 20.99/3.50  % (3966809)Peak memory usage: 16 MB
% 20.99/3.50  % (3966809)Instructions burned: 478 (million)
% 20.99/3.50  % (3966828)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1284567618:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 20.99/3.50  % (3966826)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 20.99/3.50  % (3966826)Terminated due to inappropriate strategy.
% 20.99/3.50  % (3966826)------------------------------
% 20.99/3.50  % (3966826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.99/3.50  % (3966826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.50  % (3966826)CaDiCaL version: 2.1.3
% 20.99/3.50  % (3966826)Termination reason: Inappropriate
% 20.99/3.50  % (3966826)Time elapsed: 0.030 s
% 20.99/3.50  % (3966826)Peak memory usage: 12 MB
% 20.99/3.50  % (3966826)Instructions burned: 65 (million)
% 20.99/3.50  % (3966826)------------------------------
% 20.99/3.50  % (3966826)------------------------------
% 20.99/3.50  % (3966830)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1899825001:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 20.99/3.50  % (3966818)Instruction limit reached! 
% 20.99/3.50  % (3966818)------------------------------
% 22.30/3.67  % (3966818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.67  % (3966818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.67  % (3966818)CaDiCaL version: 2.1.3
% 22.30/3.67  % (3966818)Termination reason: Instruction limit
% 22.30/3.67  % (3966818)Termination phase: Saturation
% 22.30/3.67  % (3966818)Time elapsed: 0.438 s
% 22.30/3.67  % (3966818)Peak memory usage: 21 MB
% 22.30/3.67  % (3966818)Instructions burned: 693 (million)
% 22.30/3.67  % (3966832)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3486493778:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 22.30/3.67  % (3966820)Instruction limit reached! 
% 22.30/3.67  % (3966820)------------------------------
% 22.30/3.67  % (3966820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.67  % (3966820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.67  % (3966820)CaDiCaL version: 2.1.3
% 22.30/3.67  % (3966820)Termination reason: Instruction limit
% 22.30/3.67  % (3966820)Termination phase: Saturation
% 22.30/3.67  % (3966820)Time elapsed: 0.446 s
% 22.30/3.67  % (3966820)Peak memory usage: 19 MB
% 22.30/3.67  % (3966820)Instructions burned: 879 (million)
% 22.30/3.67  % (3966834)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2221810068:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 22.30/3.67  % (3966832)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 22.30/3.67  % (3966832)Terminated due to inappropriate strategy.
% 22.30/3.67  % (3966832)------------------------------
% 22.30/3.67  % (3966832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.67  % (3966832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.67  % (3966832)CaDiCaL version: 2.1.3
% 22.30/3.67  % (3966832)Termination reason: Inappropriate
% 22.30/3.67  % (3966832)Time elapsed: 0.037 s
% 22.30/3.67  % (3966832)Peak memory usage: 12 MB
% 22.30/3.67  % (3966832)Instructions burned: 76 (million)
% 22.30/3.67  % (3966832)------------------------------
% 22.30/3.67  % (3966832)------------------------------
% 22.30/3.67  % (3966836)ott-2_1_sil=16000:newcnf=on:random_seed=1497245070:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 22.30/3.67  % (3966834)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 22.30/3.67  % (3966834)Terminated due to inappropriate strategy.
% 22.30/3.67  % (3966834)------------------------------
% 22.30/3.67  % (3966834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.67  % (3966834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.67  % (3966834)CaDiCaL version: 2.1.3
% 22.30/3.67  % (3966834)Termination reason: Inappropriate
% 22.30/3.67  % (3966834)Time elapsed: 0.030 s
% 22.30/3.67  % (3966834)Peak memory usage: 12 MB
% 22.30/3.67  % (3966834)Instructions burned: 65 (million)
% 22.30/3.67  % (3966834)------------------------------
% 22.30/3.67  % (3966834)------------------------------
% 22.30/3.67  % (3966838)ott+10_1_sil=32000:tgt=ground:random_seed=424737027:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 22.30/3.67  % (3966830)Instruction limit reached! 
% 22.30/3.67  % (3966830)------------------------------
% 22.30/3.67  % (3966830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.67  % (3966830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.67  % (3966830)CaDiCaL version: 2.1.3
% 22.30/3.67  % (3966830)Termination reason: Instruction limit
% 22.30/3.67  % (3966830)Termination phase: Saturation
% 22.30/3.67  % (3966830)Time elapsed: 0.344 s
% 22.30/3.67  % (3966830)Peak memory usage: 22 MB
% 22.30/3.67  % (3966830)Instructions burned: 1477 (million)
% 22.30/3.67  % (3966840)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=22216907:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 22.30/3.67  % (3966840)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 22.30/3.67  % (3966840)Terminated due to inappropriate strategy.
% 22.30/3.67  % (3966840)------------------------------
% 22.30/3.67  % (3966840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.30/3.67  % (3966840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.30/3.67  % (3966840)CaDiCaL version: 2.1.3
% 22.30/3.67  % (3966840)Termination reason: Inappropriate
% 22.30/3.67  % (3966840)Time elapsed: 0.019 s
% 22.30/3.67  % (3966840)Peak memory usage: 12 MB
% 22.30/3.67  % (3966840)Instructions burned: 76 (million)
% 98.35/14.34  % (3966840)------------------------------
% 98.35/14.34  % (3966840)------------------------------
% 98.35/14.34  % (3966842)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2485112654:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 98.35/14.34  % (3966814)Instruction limit reached! 
% 98.35/14.34  % (3966814)------------------------------
% 98.35/14.34  % (3966814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.35/14.34  % (3966814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.35/14.34  % (3966814)CaDiCaL version: 2.1.3
% 98.35/14.34  % (3966814)Termination reason: Instruction limit
% 98.35/14.34  % (3966814)Termination phase: Saturation
% 98.35/14.34  % (3966814)Time elapsed: 0.694 s
% 98.35/14.34  % (3966814)Peak memory usage: 21 MB
% 98.35/14.34  % (3966814)Instructions burned: 1180 (million)
% 98.35/14.34  % (3966844)dis+21_1_sil=32000:sas=cadical:random_seed=3427891079:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 98.35/14.34  % (3966836)Instruction limit reached! 
% 98.35/14.34  % (3966836)------------------------------
% 98.35/14.34  % (3966836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.35/14.34  % (3966836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.35/14.34  % (3966836)CaDiCaL version: 2.1.3
% 98.35/14.34  % (3966836)Termination reason: Instruction limit
% 98.35/14.34  % (3966836)Termination phase: Saturation
% 98.35/14.34  % (3966836)Time elapsed: 0.321 s
% 98.35/14.34  % (3966836)Peak memory usage: 14 MB
% 98.35/14.34  % (3966836)Instructions burned: 871 (million)
% 98.35/14.34  % (3966846)ott+11_1_sil=16000:gs=on:random_seed=2043032765:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi)
% 98.35/14.34  % (3966842)Instruction limit reached! 
% 98.35/14.34  % (3966842)------------------------------
% 98.35/14.34  % (3966842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.35/14.34  % (3966842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.35/14.34  % (3966842)CaDiCaL version: 2.1.3
% 98.35/14.34  % (3966842)Termination reason: Instruction limit
% 98.35/14.34  % (3966842)Termination phase: Saturation
% 98.35/14.34  % (3966842)Time elapsed: 1.064 s
% 98.35/14.34  % (3966842)Peak memory usage: 30 MB
% 98.35/14.34  % (3966842)Instructions burned: 3513 (million)
% 98.35/14.34  % (3966849)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1642319645:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi)
% 98.35/14.34  % (3966849)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 98.35/14.34  % (3966849)Terminated due to inappropriate strategy.
% 98.35/14.34  % (3966849)------------------------------
% 98.35/14.34  % (3966849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.35/14.34  % (3966849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.35/14.34  % (3966849)CaDiCaL version: 2.1.3
% 98.35/14.34  % (3966849)Termination reason: Inappropriate
% 98.35/14.34  % (3966849)Time elapsed: 0.016 s
% 98.35/14.34  % (3966849)Peak memory usage: 12 MB
% 98.35/14.34  % (3966849)Instructions burned: 65 (million)
% 98.35/14.34  % (3966849)------------------------------
% 98.35/14.34  % (3966849)------------------------------
% 98.35/14.34  % (3966851)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2098342735:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi)
% 98.35/14.34  % (3966846)Instruction limit reached! 
% 98.35/14.34  % (3966846)------------------------------
% 98.35/14.34  % (3966846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.35/14.34  % (3966846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.35/14.34  % (3966846)CaDiCaL version: 2.1.3
% 98.35/14.34  % (3966846)Termination reason: Instruction limit
% 98.35/14.34  % (3966846)Termination phase: Saturation
% 98.35/14.34  % (3966846)Time elapsed: 1.282 s
% 98.35/14.34  % (3966846)Peak memory usage: 24 MB
% 98.35/14.34  % (3966846)Instructions burned: 2252 (million)
% 98.35/14.34  % (3966853)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3259095561:i=29340_2976 on theBenchmark for (2976ds/29340Mi)
% 98.35/14.34  % (3966844)Instruction limit reached! 
% 98.35/14.34  % (3966844)------------------------------
% 98.35/14.34  % (3966844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.35/14.34  % (3966844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.35/14.34  % (3966844)CaDiCaL version: 2.1.3
% 98.35/14.34  % (3966844)Termination reason: Instruction limit
% 126.80/18.35  % (3966844)Termination phase: Saturation
% 126.80/18.35  % (3966844)Time elapsed: 2.164 s
% 126.80/18.35  % (3966844)Peak memory usage: 36 MB
% 126.80/18.35  % (3966844)Instructions burned: 3774 (million)
% 126.80/18.35  % (3966851)Instruction limit reached! 
% 126.80/18.35  % (3966851)------------------------------
% 126.80/18.35  % (3966851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.80/18.35  % (3966851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.80/18.35  % (3966851)CaDiCaL version: 2.1.3
% 126.80/18.35  % (3966851)Termination reason: Instruction limit
% 126.80/18.35  % (3966851)Termination phase: Saturation
% 126.80/18.35  % (3966851)Time elapsed: 1.112 s
% 126.80/18.35  % (3966851)Peak memory usage: 21 MB
% 126.80/18.35  % (3966851)Instructions burned: 4592 (million)
% 126.80/18.35  % (3966855)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3655022881:i=5211_2969 on theBenchmark for (2969ds/5211Mi)
% 126.80/18.35  % (3966857)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1486819710:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi)
% 126.80/18.35  % (3966857)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 126.80/18.35  % (3966857)Terminated due to inappropriate strategy.
% 126.80/18.35  % (3966857)------------------------------
% 126.80/18.35  % (3966857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.80/18.35  % (3966857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.80/18.35  % (3966857)CaDiCaL version: 2.1.3
% 126.80/18.35  % (3966857)Termination reason: Inappropriate
% 126.80/18.35  % (3966857)Time elapsed: 0.019 s
% 126.80/18.35  % (3966857)Peak memory usage: 12 MB
% 126.80/18.35  % (3966857)Instructions burned: 74 (million)
% 126.80/18.35  % (3966857)------------------------------
% 126.80/18.35  % (3966857)------------------------------
% 126.80/18.35  % (3966859)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3537048244:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi)
% 126.80/18.35  % (3966859)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 126.80/18.35  % (3966859)Terminated due to inappropriate strategy.
% 126.80/18.35  % (3966859)------------------------------
% 126.80/18.35  % (3966859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.80/18.35  % (3966859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.80/18.35  % (3966859)CaDiCaL version: 2.1.3
% 126.80/18.35  % (3966859)Termination reason: Inappropriate
% 126.80/18.35  % (3966859)Time elapsed: 0.030 s
% 126.80/18.35  % (3966859)Peak memory usage: 12 MB
% 126.80/18.35  % (3966859)Instructions burned: 65 (million)
% 126.80/18.35  % (3966859)------------------------------
% 126.80/18.35  % (3966859)------------------------------
% 126.80/18.35  % (3966861)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2376680050:i=14071_2968 on theBenchmark for (2968ds/14071Mi)
% 126.80/18.35  % (3966861)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 126.80/18.35  % (3966861)Terminated due to inappropriate strategy.
% 126.80/18.35  % (3966861)------------------------------
% 126.80/18.35  % (3966861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.80/18.35  % (3966861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.80/18.35  % (3966861)CaDiCaL version: 2.1.3
% 126.80/18.35  % (3966861)Termination reason: Inappropriate
% 126.80/18.35  % (3966861)Time elapsed: 0.016 s
% 126.80/18.35  % (3966861)Peak memory usage: 12 MB
% 126.80/18.35  % (3966861)Instructions burned: 65 (million)
% 126.80/18.35  % (3966861)------------------------------
% 126.80/18.35  % (3966861)------------------------------
% 126.80/18.35  % (3966863)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3786721653:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi)
% 126.80/18.35  % (3966828)Instruction limit reached! 
% 126.80/18.35  % (3966828)------------------------------
% 126.80/18.35  % (3966828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.80/18.35  % (3966828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.80/18.35  % (3966828)CaDiCaL version: 2.1.3
% 126.80/18.35  % (3966828)Termination reason: Instruction limit
% 126.80/18.35  % (3966828)Termination phase: Saturation
% 126.80/18.35  % (3966828)Time elapsed: 2.754 s
% 126.80/18.35  % (3966828)Peak memory usage: 34 MB
% 126.80/18.35  % (3966828)Instructions burned: 5131 (million)
% 126.80/18.35  % (3966865)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3398944709:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi)
% 130.32/18.80  % (3966838)Instruction limit reached! 
% 130.32/18.80  % (3966838)------------------------------
% 130.32/18.80  % (3966838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.80  % (3966838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.80  % (3966838)CaDiCaL version: 2.1.3
% 130.32/18.80  % (3966838)Termination reason: Instruction limit
% 130.32/18.80  % (3966838)Termination phase: Saturation
% 130.32/18.80  % (3966838)Time elapsed: 2.982 s
% 130.32/18.80  % (3966838)Peak memory usage: 33 MB
% 130.32/18.80  % (3966838)Instructions burned: 5116 (million)
% 130.32/18.80  % (3966867)dis+10_16:1_sil=16000:random_seed=2058954754:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi)
% 130.32/18.80  % (3966855)Instruction limit reached! 
% 130.32/18.80  % (3966855)------------------------------
% 130.32/18.80  % (3966855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.80  % (3966855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.80  % (3966855)CaDiCaL version: 2.1.3
% 130.32/18.80  % (3966855)Termination reason: Instruction limit
% 130.32/18.80  % (3966855)Termination phase: Saturation
% 130.32/18.81  % (3966855)Time elapsed: 2.426 s
% 130.32/18.81  % (3966855)Peak memory usage: 42 MB
% 130.32/18.81  % (3966855)Instructions burned: 5212 (million)
% 130.32/18.81  % (3966869)ott-3_8_sil=64000:random_seed=282893256:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi)
% 130.32/18.81  % (3966865)Instruction limit reached! 
% 130.32/18.81  % (3966865)------------------------------
% 130.32/18.81  % (3966865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.81  % (3966865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.81  % (3966865)CaDiCaL version: 2.1.3
% 130.32/18.81  % (3966865)Termination reason: Instruction limit
% 130.32/18.81  % (3966865)Termination phase: Saturation
% 130.32/18.81  % (3966865)Time elapsed: 4.906 s
% 130.32/18.81  % (3966865)Peak memory usage: 60 MB
% 130.32/18.81  % (3966865)Instructions burned: 8174 (million)
% 130.32/18.81  % (3966871)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1498296928:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi)
% 130.32/18.81  % (3966871)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 130.32/18.81  % (3966871)Terminated due to inappropriate strategy.
% 130.32/18.81  % (3966871)------------------------------
% 130.32/18.81  % (3966871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.81  % (3966871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.81  % (3966871)CaDiCaL version: 2.1.3
% 130.32/18.81  % (3966871)Termination reason: Inappropriate
% 130.32/18.81  % (3966871)Time elapsed: 0.036 s
% 130.32/18.81  % (3966871)Peak memory usage: 12 MB
% 130.32/18.81  % (3966871)Instructions burned: 76 (million)
% 130.32/18.81  % (3966871)------------------------------
% 130.32/18.81  % (3966871)------------------------------
% 130.32/18.81  % (3966873)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=986813019:i=11404_2917 on theBenchmark for (2917ds/11404Mi)
% 130.32/18.81  % (3966867)Instruction limit reached! 
% 130.32/18.81  % (3966867)------------------------------
% 130.32/18.81  % (3966867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.81  % (3966867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.81  % (3966867)CaDiCaL version: 2.1.3
% 130.32/18.81  % (3966867)Termination reason: Instruction limit
% 130.32/18.81  % (3966867)Termination phase: Saturation
% 130.32/18.81  % (3966867)Time elapsed: 4.871 s
% 130.32/18.81  % (3966867)Peak memory usage: 62 MB
% 130.32/18.81  % (3966867)Instructions burned: 9156 (million)
% 130.32/18.81  % (3966875)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4277706159:i=14134_2913 on theBenchmark for (2913ds/14134Mi)
% 130.32/18.81  % (3966863)Instruction limit reached! 
% 130.32/18.81  % (3966863)------------------------------
% 130.32/18.81  % (3966863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.81  % (3966863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.81  % (3966863)CaDiCaL version: 2.1.3
% 130.32/18.81  % (3966863)Termination reason: Instruction limit
% 130.32/18.81  % (3966863)Termination phase: Saturation
% 130.32/18.81  % (3966863)Time elapsed: 6.415 s
% 130.32/18.81  % (3966863)Peak memory usage: 154 MB
% 130.32/18.81  % (3966863)Instructions burned: 22567 (million)
% 130.32/18.81  % (3966877)dis+33_16_sil=32000:sac=on:random_seed=203024061:i=15851:nm=0_2903 on theBenchmark for (2903ds/15851Mi)
% 130.32/18.81  % (3966877)Instruction limit reached! 
% 130.32/18.81  % (3966877)------------------------------
% 130.32/18.81  % (3966877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3966877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3966877)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3966877)Termination reason: Instruction limit
% 136.89/19.89  % (3966877)Termination phase: Saturation
% 136.89/19.89  % (3966877)Time elapsed: 4.256 s
% 136.89/19.89  % (3966877)Peak memory usage: 122 MB
% 136.89/19.89  % (3966877)Instructions burned: 15852 (million)
% 136.89/19.89  % (3966972)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3016643633:avsq=on:i=17627:add=on:amm=off_2860 on theBenchmark for (2860ds/17627Mi)
% 136.89/19.89  % (3966869)Instruction limit reached! 
% 136.89/19.89  % (3966869)------------------------------
% 136.89/19.89  % (3966869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3966869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3966869)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3966869)Termination reason: Instruction limit
% 136.89/19.89  % (3966869)Termination phase: Saturation
% 136.89/19.89  % (3966869)Time elapsed: 9.595 s
% 136.89/19.89  % (3966869)Peak memory usage: 51 MB
% 136.89/19.89  % (3966869)Instructions burned: 20141 (million)
% 136.89/19.89  % (3967112)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1923593586:s2a=on:i=53295_2848 on theBenchmark for (2848ds/53295Mi)
% 136.89/19.89  % (3966873)Instruction limit reached! 
% 136.89/19.89  % (3966873)------------------------------
% 136.89/19.89  % (3966873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3966873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3966873)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3966873)Termination reason: Instruction limit
% 136.89/19.89  % (3966873)Termination phase: Saturation
% 136.89/19.89  % (3966873)Time elapsed: 7.239 s
% 136.89/19.89  % (3966873)Peak memory usage: 89 MB
% 136.89/19.89  % (3966873)Instructions burned: 11405 (million)
% 136.89/19.89  % (3967114)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=491566390:i=26857:ins=20_2844 on theBenchmark for (2844ds/26857Mi)
% 136.89/19.89  % (3967114)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 136.89/19.89  % (3967114)Terminated due to inappropriate strategy.
% 136.89/19.89  % (3967114)------------------------------
% 136.89/19.89  % (3967114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3967114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3967114)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3967114)Termination reason: Inappropriate
% 136.89/19.89  % (3967114)Time elapsed: 0.030 s
% 136.89/19.89  % (3967114)Peak memory usage: 12 MB
% 136.89/19.89  % (3967114)Instructions burned: 65 (million)
% 136.89/19.89  % (3967114)------------------------------
% 136.89/19.89  % (3967114)------------------------------
% 136.89/19.89  % (3967117)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4093590681:i=28120:bs=on:fsr=off_2844 on theBenchmark for (2844ds/28120Mi)
% 136.89/19.89  % (3966875)Instruction limit reached! 
% 136.89/19.89  % (3966875)------------------------------
% 136.89/19.89  % (3966875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3966875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3966875)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3966875)Termination reason: Instruction limit
% 136.89/19.89  % (3966875)Termination phase: Saturation
% 136.89/19.89  % (3966875)Time elapsed: 9.134 s
% 136.89/19.89  % (3966875)Peak memory usage: 79 MB
% 136.89/19.89  % (3966875)Instructions burned: 14134 (million)
% 136.89/19.89  % (3967159)fmb+10_1_sil=256000:fmbss=7:random_seed=2940134185:fmbsr=1.6:i=182295_2821 on theBenchmark for (2821ds/182295Mi)
% 136.89/19.89  % (3967159)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 136.89/19.89  % (3967159)Terminated due to inappropriate strategy.
% 136.89/19.89  % (3967159)------------------------------
% 136.89/19.89  % (3967159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3967159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3967159)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3967159)Termination reason: Inappropriate
% 136.89/19.89  % (3967159)Time elapsed: 0.047 s
% 136.89/19.89  % (3967159)Peak memory usage: 12 MB
% 136.89/19.89  % (3967159)Instructions burned: 65 (million)
% 136.89/19.89  % (3967159)------------------------------
% 136.89/19.89  % (3967159)------------------------------
% 136.89/19.89  % (3967162)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3047346342:i=44625:gsp=on_2820 on theBenchmark for (2820ds/44625Mi)
% 136.89/19.89  % (3967162)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 136.89/19.89  % (3967162)Terminated due to inappropriate strategy.
% 136.89/19.89  % (3967162)------------------------------
% 136.89/19.89  % (3967162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3967162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3967162)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3967162)Termination reason: Inappropriate
% 136.89/19.89  % (3967162)Time elapsed: 0.036 s
% 136.89/19.89  % (3967162)Peak memory usage: 12 MB
% 136.89/19.89  % (3967162)Instructions burned: 68 (million)
% 136.89/19.89  % (3967162)------------------------------
% 136.89/19.89  % (3967162)------------------------------
% 136.89/19.89  % (3967164)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=185173451:i=160505_2820 on theBenchmark for (2820ds/160505Mi)
% 136.89/19.89  % (3967164)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 136.89/19.89  % (3967164)Terminated due to inappropriate strategy.
% 136.89/19.89  % (3967164)------------------------------
% 136.89/19.89  % (3967164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3967164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3967164)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3967164)Termination reason: Inappropriate
% 136.89/19.89  % (3967164)Time elapsed: 0.058 s
% 136.89/19.89  % (3967164)Peak memory usage: 12 MB
% 136.89/19.89  % (3967164)Instructions burned: 65 (million)
% 136.89/19.89  % (3967164)------------------------------
% 136.89/19.89  % (3967164)------------------------------
% 136.89/19.89  % (3967168)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1538287414:fmbsr=1.3:i=225729_2819 on theBenchmark for (2819ds/225729Mi)
% 136.89/19.89  % (3967168)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 136.89/19.89  % (3967168)Terminated due to inappropriate strategy.
% 136.89/19.89  % (3967168)------------------------------
% 136.89/19.89  % (3967168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3967168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3967168)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3967168)Termination reason: Inappropriate
% 136.89/19.89  % (3967168)Time elapsed: 0.038 s
% 136.89/19.89  % (3967168)Peak memory usage: 12 MB
% 136.89/19.89  % (3967168)Instructions burned: 65 (million)
% 136.89/19.89  % (3967168)------------------------------
% 136.89/19.89  % (3967168)------------------------------
% 136.89/19.89  % (3967170)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2176592992:fmbsr=2:i=185024:ins=7_2818 on theBenchmark for (2818ds/185024Mi)
% 136.89/19.89  % (3967170)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 136.89/19.89  % (3967170)Terminated due to inappropriate strategy.
% 136.89/19.89  % (3967170)------------------------------
% 136.89/19.89  % (3967170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3967170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3967170)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3967170)Termination reason: Inappropriate
% 136.89/19.89  % (3967170)Time elapsed: 0.042 s
% 136.89/19.89  % (3967170)Peak memory usage: 12 MB
% 136.89/19.89  % (3967170)Instructions burned: 65 (million)
% 136.89/19.89  % (3967170)------------------------------
% 136.89/19.89  % (3967170)------------------------------
% 136.89/19.89  % (3967172)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=963153846:rtra=on_2817 on theBenchmark for (2817ds/0Mi)
% 136.89/19.89  % (3967172)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 136.89/19.89  % (3967172)Terminated due to inappropriate strategy.
% 136.89/19.89  % (3967172)------------------------------
% 136.89/19.89  % (3967172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3967172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3967172)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3967172)Termination reason: Inappropriate
% 136.89/19.89  % (3967172)Time elapsed: 0.077 s
% 136.89/19.89  % (3967172)Peak memory usage: 13 MB
% 136.89/19.89  % (3967172)Instructions burned: 84 (million)
% 136.89/19.89  % (3967172)------------------------------
% 136.89/19.89  % (3967172)------------------------------
% 136.89/19.89  % (3967176)% WARNING: option uhcvi not known.
% 136.89/19.89  % (3967176)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1308494172:i=271062:add=off:rtra=on:rawr=on_2816 on theBenchmark for (2816ds/271062Mi)
% 136.89/19.89  % (3966972)Instruction limit reached! 
% 136.89/19.89  % (3966972)------------------------------
% 136.89/19.89  % (3966972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3966972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3966972)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3966972)Termination reason: Instruction limit
% 136.89/19.89  % (3966972)Termination phase: Saturation
% 136.89/19.89  % (3966972)Time elapsed: 4.912 s
% 136.89/19.89  % (3966972)Peak memory usage: 77 MB
% 136.89/19.89  % (3966972)Instructions burned: 17628 (million)
% 136.89/19.89  % (3967178)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2638650267:i=176048:add=on:rtra=on:rawr=on_2811 on theBenchmark for (2811ds/176048Mi)
% 136.89/19.89  % (3966853)Instruction limit reached! 
% 136.89/19.89  % (3966853)------------------------------
% 136.89/19.89  % (3966853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3966853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3966853)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3966853)Termination reason: Instruction limit
% 136.89/19.89  % (3966853)Termination phase: Saturation
% 136.89/19.89  % (3966853)Time elapsed: 16.754 s
% 136.89/19.89  % (3966853)Peak memory usage: 98 MB
% 136.89/19.89  % (3966853)Instructions burned: 29340 (million)
% 136.89/19.89  % (3967181)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1192170338:i=206:fgj=on:rtra=on_2808 on theBenchmark for (2808ds/206Mi)
% 136.89/19.89  % (3967181)Instruction limit reached! 
% 136.89/19.89  % (3967181)------------------------------
% 136.89/19.89  % (3967181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.89/19.89  % (3967181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.89/19.89  % (3967181)CaDiCaL version: 2.1.3
% 136.89/19.89  % (3967181)Termination reason: Instruction limit
% 136.89/19.89  % (3967181)Termination phase: Saturation
% 136.89/19.89  % (3967181)Time elapsed: 0.123 s
% 136.89/19.89  % (3967181)Peak memory usage: 15 MB
% 136.89/19.89  % (3967181)Instructions burned: 207 (million)
% 136.89/19.89  % (3967201)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1616132650:i=232:rtra=on_2806 on theBenchmark for (2806ds/232Mi)
% 136.89/19.89  % (3966789) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3966783-3966789"...
% 136.89/19.89  % (3966789)...printing done.
% 136.89/19.89  % (3966789)Refutation found. Thanks to Tanya!
% 136.89/19.89  % SZS status Theorem for theBenchmark
% 136.89/19.89  % SZS output start Proof for theBenchmark
% See solution above
% 138.09/19.90  % (3966789)------------------------------
% 138.09/19.90  % (3966789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.09/19.90  % (3966789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.09/19.90  % (3966789)CaDiCaL version: 2.1.3
% 138.09/19.90  % (3966789)Termination reason: Refutation
% 138.09/19.90  % (3966789)Time elapsed: 19.372 s
% 138.09/19.90  % (3966789)Peak memory usage: 137 MB
% 138.09/19.90  % (3966789)Instructions burned: 33716 (million)
% 138.09/19.90  % (3966783)Success in time 19.487 s
% 138.09/19.90  % Vampire exiting
%------------------------------------------------------------------------------