Vampire---5.0.1.THM-Ref.s

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

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

% Result   : Theorem 15.11s 3.34s
% Output   : Refutation 0.17s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    7
%            Number of leaves      :   13
% Syntax   : Number of formulae    :   46 (  15 unt;   0 typ;   6 def)
%            Number of atoms       :   84 (   5 equ)
%            Maximal formula atoms :    3 (   1 avg)
%            Number of connectives :   70 (  32   ~;  28   |;   1   &)
%                                         (   6 <=>;   3  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    7 (   3 avg)
%            Maximal term depth    :    7 (   2 avg)
%            Number of types       :   19 (  17 usr;   1 ari;   0 dat;   0 cdt)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :   85 (  83 usr;   7 prp; 0-3 aty)
%            Number of functors    :  445 ( 445 usr;  30 con; 0-3 aty)
%            Number of variables   :   44 (  44   !;   0   ?;  44   :)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

tff(func_def_1,type,
    'fun_app$f': ( 'A_ltln_a_ltln_bool_fun_fun$' * 'A_ltln$' ) > 'A_ltln_bool_fun$' ).

tff(func_def_2,type,
    'g_F$': ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'A_ltln_set$' ).

tff(func_def_3,type,
    'weakUntil_ltln$': 'A_ltln$' > 'A_ltln_a_ltln_fun$' ).

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,
    'gF_singleton$': ( 'Nat_a_set_fun$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_7,type,
    'next_ltln$': 'A_ltln_a_ltln_fun$' ).

tff(func_def_8,type,
    'subformulas_nu$': 'A_ltln$' > 'A_ltln_set$' ).

tff(func_def_9,type,
    'suffix$': ( 'Nat$' * 'Nat_a_set_fun$' ) > 'Nat_a_set_fun$' ).

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

tff(func_def_11,type,
    'fun_app$e': ( 'Int_int_int_fun_fun$' * $int ) > 'Int_int_fun$' ).

tff(func_def_12,type,
    'is_mu_LTL$': 'A_ltln_bool_fun$' ).

tff(func_def_13,type,
    'is_nu_LTL$': 'A_ltln_bool_fun$' ).

tff(func_def_14,type,
    'i$': 'Nat$' ).

tff(func_def_15,type,
    'fun_app$h': ( 'Int_a_ltln_set_fun$' * $int ) > 'A_ltln_set$' ).

tff(func_def_16,type,
    'gF_advice$': ( 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

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

tff(func_def_18,type,
    'prop_ltln$': 'A$' > 'A_ltln$' ).

tff(func_def_19,type,
    tltrue: tlbool ).

tff(func_def_20,type,
    'fun_app$g': ( 'A_ltln_set_int_fun$' * 'A_ltln_set$' ) > $int ).

tff(func_def_21,type,
    'strongRelease_ltln$': 'A_ltln$' > 'A_ltln_a_ltln_fun$' ).

tff(func_def_22,type,
    'restricted_subformulas$': 'A_ltln$' > 'A_ltln_set$' ).

tff(func_def_23,type,
    'and_ltln$': 'A_ltln$' > 'A_ltln_a_ltln_fun$' ).

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

tff(func_def_25,type,
    'psi$': 'A_ltln$' ).

tff(func_def_26,type,
    'nprop_ltln$': 'A$' > 'A_ltln$' ).

tff(func_def_27,type,
    'inf$': 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' ).

tff(func_def_28,type,
    'fun_app$b': ( 'A_ltln_set_a_ltln_set_fun$' * 'A_ltln_set$' ) > 'A_ltln_set$' ).

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

tff(func_def_30,type,
    'f_G$': ( 'A_ltln$' * 'Nat_a_set_fun$' ) > 'A_ltln_set$' ).

tff(func_def_31,type,
    'subformulas_mu$': 'A_ltln$' > 'A_ltln_set$' ).

tff(func_def_32,type,
    'fG_advice$': ( 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_33,type,
    'fun_app$j': ( 'Int_int_bool_fun_fun$' * $int ) > 'Int_bool_fun$' ).

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

tff(func_def_35,type,
    'fun_app$c': ( 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' * 'A_ltln_set$' ) > 'A_ltln_set_a_ltln_set_fun$' ).

tff(func_def_36,type,
    'fun_app$d': ( 'Int_int_fun$' * $int ) > $int ).

tff(func_def_37,type,
    'or_ltln$': 'A_ltln$' > 'A_ltln_a_ltln_fun$' ).

tff(func_def_38,type,
    tlfalse: tlbool ).

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

tff(func_def_40,type,
    'inf$a': 'Int_int_int_fun_fun$' ).

tff(func_def_41,type,
    'sup$': 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' ).

tff(func_def_42,type,
    'bot$': 'A_ltln_set$' ).

tff(func_def_43,type,
    'fG_singleton$': ( 'Nat_a_set_fun$' * 'A_ltln$' ) > 'A_ltln_set$' ).

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

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

tff(func_def_46,type,
    'sup$a': 'Int_int_int_fun_fun$' ).

tff(func_def_47,type,
    'fun_app$a': ( 'A_ltln_a_ltln_fun$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_49,type,
    sK71: 'A_ltln_bool_fun$' > 'A_ltln$' ).

tff(func_def_50,type,
    sK72: ( 'A_ltln_bool_fun$' * 'A_ltln_bool_fun$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_51,type,
    sK73: 'A_ltln_set_a_ltln_set_fun$' > 'A_ltln_set$' ).

tff(func_def_52,type,
    sK74: 'A_ltln_set_a_ltln_set_fun$' > 'A_ltln_set$' ).

tff(func_def_53,type,
    sK75: ( 'A_ltln_set$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_54,type,
    sK76: ( 'A_ltln_set$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_55,type,
    sK77: ( tlbool * 'A_ltln$' ) > 'A$' ).

tff(func_def_56,type,
    sK78: ( 'A_ltln$' * tlbool ) > 'A$' ).

tff(func_def_57,type,
    sK79: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_58,type,
    sK80: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_59,type,
    sK81: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_60,type,
    sK82: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_61,type,
    sK83: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_62,type,
    sK84: ( 'A_ltln$' * tlbool ) > 'A_ltln$' ).

tff(func_def_63,type,
    sK85: ( 'A_ltln$' * tlbool ) > 'A_ltln$' ).

tff(func_def_64,type,
    sK86: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_65,type,
    sK87: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_66,type,
    sK88: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_67,type,
    sK89: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_68,type,
    sK90: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_69,type,
    sK91: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_70,type,
    sK92: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_71,type,
    sK93: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_72,type,
    sK94: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_73,type,
    sK95: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A$' ).

tff(func_def_74,type,
    sK96: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_75,type,
    sK97: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat_a_set_fun$' ).

tff(func_def_76,type,
    sK98: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'A_ltln$' ).

tff(func_def_77,type,
    sK99: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'A_ltln$' ).

tff(func_def_78,type,
    sK100: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > 'Nat_a_set_fun$' ).

tff(func_def_79,type,
    sK101: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_80,type,
    sK102: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_81,type,
    sK103: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'A_ltln$' ).

tff(func_def_82,type,
    sK104: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'A_ltln$' ).

tff(func_def_83,type,
    sK105: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat_a_set_fun$' ).

tff(func_def_84,type,
    sK106: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_85,type,
    sK107: ( 'A_ltln$' * 'A_ltln_set$' * 'Nat_a_set_fun$' ) > 'A_ltln$' ).

tff(func_def_86,type,
    sK108: ( 'A_ltln$' * 'A_ltln_set$' * 'Nat_a_set_fun$' ) > 'Nat_a_set_fun$' ).

tff(func_def_87,type,
    sK109: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_88,type,
    sK110: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_89,type,
    sK111: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_90,type,
    sK112: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_91,type,
    sK113: ( 'A_ltln_set$' * 'Nat_a_set_fun$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_92,type,
    sK114: ( 'A_ltln_set$' * 'Nat_a_set_fun$' * 'A_ltln$' ) > 'Nat_a_set_fun$' ).

tff(func_def_93,type,
    sK115: ( 'A_ltln_set$' * 'Nat_a_set_fun$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_94,type,
    sK116: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$' ) > 'A$' ).

tff(func_def_95,type,
    sK117: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_96,type,
    sK118: ( 'A_ltln_set$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_97,type,
    sK119: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_98,type,
    sK120: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A$' ).

tff(func_def_99,type,
    sK121: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_100,type,
    sK122: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_101,type,
    sK123: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_102,type,
    sK124: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_103,type,
    sK125: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_104,type,
    sK126: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_105,type,
    sK127: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln_set$' ).

tff(func_def_106,type,
    sK128: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A$' ).

tff(func_def_107,type,
    sK129: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_108,type,
    sK130: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln_set$' ).

tff(func_def_109,type,
    sK131: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_110,type,
    sK132: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_111,type,
    sK133: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_112,type,
    sK134: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_113,type,
    sK135: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_114,type,
    sK136: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_115,type,
    sK137: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_116,type,
    sK138: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_117,type,
    sK139: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_118,type,
    sK140: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_119,type,
    sK141: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln_set$' ).

tff(func_def_120,type,
    sK142: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_121,type,
    sK143: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_122,type,
    sK144: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_123,type,
    sK145: 'A_ltln_set_int_fun$' > 'A_ltln_set$' ).

tff(func_def_124,type,
    sK146: 'A_ltln_set_int_fun$' > 'A_ltln_set$' ).

tff(func_def_125,type,
    sK147: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_126,type,
    sK148: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_127,type,
    sK149: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_128,type,
    sK150: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_129,type,
    sK151: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_130,type,
    sK152: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_131,type,
    sK153: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_132,type,
    sK154: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_133,type,
    sK155: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_134,type,
    sK156: 'A_ltln$' > 'A$' ).

tff(func_def_135,type,
    sK157: 'A_ltln$' > 'A$' ).

tff(func_def_136,type,
    sK158: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_137,type,
    sK159: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_138,type,
    sK160: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_139,type,
    sK161: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_140,type,
    sK162: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_141,type,
    sK163: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_142,type,
    sK164: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_143,type,
    sK165: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_144,type,
    sK166: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_145,type,
    sK167: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_146,type,
    sK168: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_147,type,
    sK169: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_148,type,
    sK170: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_149,type,
    sK171: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_150,type,
    sK172: $int ).

tff(func_def_151,type,
    sK173: $int ).

tff(func_def_152,type,
    sK174: $int ).

tff(func_def_153,type,
    sK175: 'A_ltln$' > 'A$' ).

tff(func_def_154,type,
    sK176: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_155,type,
    sK177: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_156,type,
    sK178: 'A_ltln$' > 'A$' ).

tff(func_def_157,type,
    sK179: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_158,type,
    sK180: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_159,type,
    sK181: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_160,type,
    sK182: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_161,type,
    sK183: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_162,type,
    sK184: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_163,type,
    sK185: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_164,type,
    sK186: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_165,type,
    sK187: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_166,type,
    sK188: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_167,type,
    sK189: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_168,type,
    sK190: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_169,type,
    sK191: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_170,type,
    sK192: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_171,type,
    sK193: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_172,type,
    sK194: 'A_ltln$' > 'A$' ).

tff(func_def_173,type,
    sK195: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_174,type,
    sK196: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_175,type,
    sK197: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_176,type,
    sK198: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_177,type,
    sK199: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_178,type,
    sK200: 'A_ltln$' > 'A$' ).

tff(func_def_179,type,
    sK201: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_180,type,
    sK202: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_181,type,
    sK203: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_182,type,
    sK204: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_183,type,
    sK205: ( 'A_ltln$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat$' ).

tff(func_def_184,type,
    sK206: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_185,type,
    sK207: ( 'A_ltln_bool_fun$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_186,type,
    sK208: ( 'A_ltln_set$' * 'A_ltln_bool_fun$' ) > 'A_ltln$' ).

tff(func_def_187,type,
    sK209: ( 'A_ltln_set$' * 'A_ltln_bool_fun$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_188,type,
    sK210: 'Nat$' ).

tff(func_def_189,type,
    sK211: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_190,type,
    sK212: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_191,type,
    sK213: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_192,type,
    sK214: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln_set$' ).

tff(func_def_193,type,
    sK215: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A$' ).

tff(func_def_194,type,
    sK216: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln_set$' ).

tff(func_def_195,type,
    sK217: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_196,type,
    sK218: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_197,type,
    sK219: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_198,type,
    sK220: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_199,type,
    sK221: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_200,type,
    sK222: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A$' ).

tff(func_def_201,type,
    sK223: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_202,type,
    sK224: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_203,type,
    sK225: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_204,type,
    sK226: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_205,type,
    sK227: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_206,type,
    sK228: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_207,type,
    sK229: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_208,type,
    sK230: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_209,type,
    sK231: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_210,type,
    sK232: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_211,type,
    sK233: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_212,type,
    sK234: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_213,type,
    sK235: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln_set$' ).

tff(func_def_214,type,
    sK236: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_215,type,
    sK237: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_216,type,
    sK238: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_217,type,
    sK239: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_218,type,
    sK240: 'A_ltln$' > 'A$' ).

tff(func_def_219,type,
    sK241: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_220,type,
    sK242: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_221,type,
    sK243: 'A_ltln$' > 'A$' ).

tff(func_def_222,type,
    sK244: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_223,type,
    sK245: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_224,type,
    sK246: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_225,type,
    sK247: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_226,type,
    sK248: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_227,type,
    sK249: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_228,type,
    sK250: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_229,type,
    sK251: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_230,type,
    sK252: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > 'Nat_a_set_fun$' ).

tff(func_def_231,type,
    sK253: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A$' ).

tff(func_def_232,type,
    sK254: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat_a_set_fun$' ).

tff(func_def_233,type,
    sK255: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'A_ltln$' ).

tff(func_def_234,type,
    sK256: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'A_ltln$' ).

tff(func_def_235,type,
    sK257: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_236,type,
    sK258: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_237,type,
    sK259: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_238,type,
    sK260: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'A$' ).

tff(func_def_239,type,
    sK261: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > 'Nat_a_set_fun$' ).

tff(func_def_240,type,
    sK262: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_241,type,
    sK263: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_242,type,
    sK264: ( 'A_ltln_set$' * 'Nat_a_set_fun$' * 'A_ltln$' ) > 'Nat_a_set_fun$' ).

tff(func_def_243,type,
    sK265: ( 'A_ltln_set$' * 'Nat_a_set_fun$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_244,type,
    sK266: ( 'A_ltln_set$' * 'Nat_a_set_fun$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_245,type,
    sK267: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_246,type,
    sK268: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_247,type,
    sK269: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_248,type,
    sK270: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_249,type,
    sK271: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > 'Nat_a_set_fun$' ).

tff(func_def_250,type,
    sK272: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_251,type,
    sK273: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'Nat_a_set_fun$' ).

tff(func_def_252,type,
    sK274: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_253,type,
    sK275: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > 'Nat_a_set_fun$' ).

tff(func_def_254,type,
    sK276: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_255,type,
    sK277: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_256,type,
    sK278: 'A_ltln_bool_fun$' > 'A_ltln$' ).

tff(func_def_257,type,
    sK279: ( 'A_ltln_set$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_258,type,
    sK280: 'Int_int_fun$' > $int ).

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

tff(func_def_260,type,
    sK282: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_261,type,
    sK283: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_262,type,
    sK284: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_263,type,
    sK285: 'A_ltln$' > 'A$' ).

tff(func_def_264,type,
    sK286: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_265,type,
    sK287: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_266,type,
    sK288: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_267,type,
    sK289: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_268,type,
    sK290: 'A_ltln$' > 'A$' ).

tff(func_def_269,type,
    sK291: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_270,type,
    sK292: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_271,type,
    sK293: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_272,type,
    sK294: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_273,type,
    sK295: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_274,type,
    sK296: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_275,type,
    sK297: ( 'A_ltln_set$' * 'Nat_a_set_fun$' ) > 'A_ltln$' ).

tff(func_def_276,type,
    sK298: 'A_ltln_set$' > 'A_ltln$' ).

tff(func_def_277,type,
    sK299: ( 'A_ltln_bool_fun$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_278,type,
    sK300: ( 'A_ltln_bool_fun$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_279,type,
    sK301: ( 'A_ltln_bool_fun$' * 'A_ltln_set$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_280,type,
    sK302: 'Int_int_fun$' > $int ).

tff(func_def_281,type,
    sK303: 'Int_int_fun$' > $int ).

tff(func_def_282,type,
    sK304: 'A_ltln$' > 'A$' ).

tff(func_def_283,type,
    sK305: 'A_ltln$' > 'A$' ).

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

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

tff(func_def_286,type,
    sK308: 'A_ltln$' > 'A_ltln$' ).

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

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

tff(func_def_289,type,
    sK311: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_290,type,
    sK312: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_291,type,
    sK313: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_292,type,
    sK314: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_293,type,
    sK315: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_294,type,
    sK316: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_295,type,
    sK317: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_296,type,
    sK318: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_297,type,
    sK319: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_298,type,
    sK320: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_299,type,
    sK321: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_300,type,
    sK322: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_301,type,
    sK323: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_302,type,
    sK324: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_303,type,
    sK325: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_304,type,
    sK326: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_305,type,
    sK327: 'A_ltln$' > 'A$' ).

tff(func_def_306,type,
    sK328: 'A_ltln$' > 'A$' ).

tff(func_def_307,type,
    sK329: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_308,type,
    sK330: 'Int_a_ltln_set_fun$' > $int ).

tff(func_def_309,type,
    sK331: 'Int_a_ltln_set_fun$' > $int ).

tff(func_def_310,type,
    sK332: 'A_ltln_set$' > 'A_ltln$' ).

tff(func_def_311,type,
    sK333: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_312,type,
    sK334: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_313,type,
    sK335: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_314,type,
    sK336: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_315,type,
    sK337: ( 'A_ltln_bool_fun$' * 'A_ltln_bool_fun$' ) > 'A_ltln$' ).

tff(func_def_316,type,
    sK338: 'A_ltln$' > 'A$' ).

tff(func_def_317,type,
    sK339: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_318,type,
    sK340: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_319,type,
    sK341: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_320,type,
    sK342: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_321,type,
    sK343: 'A_ltln$' > 'A$' ).

tff(func_def_322,type,
    sK344: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_323,type,
    sK345: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_324,type,
    sK346: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_325,type,
    sK347: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_326,type,
    sK348: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_327,type,
    sK349: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_328,type,
    sK350: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_329,type,
    sK351: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_330,type,
    sK352: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_331,type,
    sK353: 'A_ltln_set$' ).

tff(func_def_332,type,
    sK354: 'A_ltln_set$' ).

tff(func_def_333,type,
    sK355: 'A_ltln_set$' ).

tff(func_def_334,type,
    sK356: 'A_ltln_set_int_fun$' > 'A_ltln_set$' ).

tff(func_def_335,type,
    sK357: 'A_ltln_set_int_fun$' > 'A_ltln_set$' ).

tff(func_def_336,type,
    sK358: ( 'A_ltln_set$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_337,type,
    sK359: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_338,type,
    sK360: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_339,type,
    sK361: 'A_ltln$' > 'A$' ).

tff(func_def_340,type,
    sK362: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_341,type,
    sK363: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_342,type,
    sK364: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_343,type,
    sK365: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_344,type,
    sK366: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_345,type,
    sK367: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_346,type,
    sK368: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_347,type,
    sK369: 'A_ltln$' > 'A$' ).

tff(func_def_348,type,
    sK370: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_349,type,
    sK371: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_350,type,
    sK372: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_351,type,
    sK373: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_352,type,
    sK374: ( 'A_ltln_bool_fun$' * 'A_ltln_bool_fun$' ) > 'A_ltln$' ).

tff(func_def_353,type,
    sK375: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_354,type,
    sK376: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln$' ) > 'Nat$' ).

tff(func_def_355,type,
    sK377: ( 'A_ltln_set$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_356,type,
    sK378: 'A_ltln_set_int_fun$' > 'A_ltln_set$' ).

tff(func_def_357,type,
    sK379: 'A_ltln_set_int_fun$' > 'A_ltln_set$' ).

tff(func_def_358,type,
    sK380: ( 'A_ltln_bool_fun$' * 'A_ltln_bool_fun$' ) > 'A_ltln$' ).

tff(func_def_359,type,
    sK381: 'A_ltln_set_a_ltln_set_fun$' > 'A_ltln_set$' ).

tff(func_def_360,type,
    sK382: 'A_ltln_set_a_ltln_set_fun$' > 'A_ltln_set$' ).

tff(func_def_361,type,
    sK383: $int ).

tff(func_def_362,type,
    sK384: $int ).

tff(func_def_363,type,
    sK385: $int ).

tff(func_def_364,type,
    sK386: 'Int_a_ltln_set_fun$' > $int ).

tff(func_def_365,type,
    sK387: 'Int_a_ltln_set_fun$' > $int ).

tff(func_def_366,type,
    sK388: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_367,type,
    sK389: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_368,type,
    sK390: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_369,type,
    sK391: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_370,type,
    sK392: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_371,type,
    sK393: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_372,type,
    sK394: 'Int_int_int_fun_fun$' > $int ).

tff(func_def_373,type,
    sK395: 'Int_a_ltln_set_fun$' > $int ).

tff(func_def_374,type,
    sK396: 'Int_a_ltln_set_fun$' > $int ).

tff(func_def_375,type,
    sK397: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_376,type,
    sK398: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_377,type,
    sK399: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_378,type,
    sK400: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_379,type,
    sK401: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_380,type,
    sK402: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_381,type,
    sK403: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_382,type,
    sK404: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_383,type,
    sK405: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_384,type,
    sK406: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_385,type,
    sK407: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_386,type,
    sK408: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_387,type,
    sK409: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_388,type,
    sK410: 'A_ltln_set_a_ltln_set_fun$' > 'A_ltln_set$' ).

tff(func_def_389,type,
    sK411: 'A_ltln_set_a_ltln_set_fun$' > 'A_ltln_set$' ).

tff(func_def_390,type,
    sK412: ( 'A_ltln_set$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_391,type,
    sK413: 'A_ltln_set_a_ltln_set_fun$' > 'A_ltln_set$' ).

tff(func_def_392,type,
    sK414: 'A_ltln_set_a_ltln_set_fun$' > 'A_ltln_set$' ).

tff(func_def_393,type,
    sK415: ( 'Nat_a_set_fun$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_394,type,
    sK416: 'A_ltln_set$' > 'A_ltln$' ).

tff(func_def_395,type,
    sK417: 'A_ltln_set$' ).

tff(func_def_396,type,
    sK418: 'A_ltln_set$' ).

tff(func_def_397,type,
    sK419: 'A_ltln_set$' ).

tff(func_def_398,type,
    sK420: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_399,type,
    sK421: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_400,type,
    sK422: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_401,type,
    sK423: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_402,type,
    sK424: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_403,type,
    sK425: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_404,type,
    sK426: 'A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$' > 'A_ltln_set$' ).

tff(func_def_405,type,
    sK427: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_406,type,
    sK428: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_407,type,
    sK429: ( tlbool * 'A_ltln$' ) > 'A$' ).

tff(func_def_408,type,
    sK430: ( tlbool * 'A_ltln$' ) > 'A$' ).

tff(func_def_409,type,
    sK431: ( 'A_ltln$' * tlbool ) > 'A_ltln$' ).

tff(func_def_410,type,
    sK432: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_411,type,
    sK433: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_412,type,
    sK434: ( 'A_ltln$' * tlbool ) > 'A_ltln$' ).

tff(func_def_413,type,
    sK435: ( 'A_ltln$' * tlbool ) > 'A_ltln$' ).

tff(func_def_414,type,
    sK436: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_415,type,
    sK437: ( tlbool * 'A_ltln$' ) > 'A_ltln$' ).

tff(func_def_416,type,
    sK438: ( 'A_ltln$' * tlbool ) > 'A_ltln$' ).

tff(func_def_417,type,
    sK439: ( 'A_ltln$' * tlbool ) > 'A_ltln$' ).

tff(func_def_418,type,
    sK440: ( 'A_ltln$' * tlbool ) > 'A_ltln$' ).

tff(func_def_419,type,
    sK441: ( 'A_ltln$' * tlbool ) > 'A_ltln$' ).

tff(func_def_420,type,
    sK442: ( 'A_ltln_set$' * 'A_ltln_set$' * 'A_ltln_set$' ) > 'A_ltln_set$' ).

tff(func_def_421,type,
    sK443: ( 'A_ltln_set$' * 'A_ltln_set$' * 'A_ltln_set$' ) > 'A_ltln_set$' ).

tff(func_def_422,type,
    sK444: 'A_ltln_set_int_fun$' > 'A_ltln_set$' ).

tff(func_def_423,type,
    sK445: 'A_ltln_set_int_fun$' > 'A_ltln_set$' ).

tff(func_def_424,type,
    sK446: ( 'A_ltln_set$' * 'Nat_a_set_fun$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_425,type,
    sK447: ( 'A_ltln_set$' * 'Nat_a_set_fun$' * 'A_ltln_set$' ) > 'A_ltln$' ).

tff(func_def_426,type,
    sK448: 'Int_a_ltln_set_fun$' > $int ).

tff(func_def_427,type,
    sK449: 'Int_a_ltln_set_fun$' > $int ).

tff(func_def_428,type,
    sK450: 'Int_int_fun$' > $int ).

tff(func_def_429,type,
    sK451: 'Int_int_fun$' > $int ).

tff(func_def_430,type,
    sK452: 'Int_int_fun$' > $int ).

tff(func_def_431,type,
    sK453: 'Int_int_fun$' > $int ).

tff(func_def_432,type,
    sK454: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_433,type,
    sK455: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_434,type,
    sK456: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_435,type,
    sK457: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_436,type,
    sK458: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_437,type,
    sK459: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_438,type,
    sK460: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_439,type,
    sK461: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_440,type,
    sK462: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_441,type,
    sK463: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_442,type,
    sK464: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_443,type,
    sK465: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_444,type,
    sK466: 'A_ltln$' > 'A_ltln$' ).

tff(func_def_447,type,
    '$inst468': $int ).

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

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

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

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

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

tff(pred_def_6,type,
    'mu_stable$': ( 'A_ltln$' * 'Nat_a_set_fun$' ) > $o ).

tff(pred_def_9,type,
    sP0: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_10,type,
    sP1: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_11,type,
    sP2: ( 'A_ltln$' * tlbool ) > $o ).

tff(pred_def_12,type,
    sP3: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_13,type,
    sP4: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_14,type,
    sP5: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_15,type,
    sP6: ( 'A_ltln$' * tlbool ) > $o ).

tff(pred_def_16,type,
    sP7: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_17,type,
    sP8: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_18,type,
    sP9: ( 'A_ltln_set$' * 'Nat_a_set_fun$' * 'A_ltln$' ) > $o ).

tff(pred_def_19,type,
    sP10: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_20,type,
    sP11: ( 'A_ltln$' * 'Nat_a_set_fun$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_21,type,
    sP12: ( 'A_ltln$' * 'A_ltln_set$' * 'Nat_a_set_fun$' ) > $o ).

tff(pred_def_22,type,
    sP13: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_23,type,
    sP14: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > $o ).

tff(pred_def_24,type,
    sP15: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > $o ).

tff(pred_def_25,type,
    sP16: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > $o ).

tff(pred_def_26,type,
    sP17: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_27,type,
    sP18: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_28,type,
    sP19: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_29,type,
    sP20: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > $o ).

tff(pred_def_30,type,
    sP21: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > $o ).

tff(pred_def_31,type,
    sP22: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > $o ).

tff(pred_def_32,type,
    sP23: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_33,type,
    sP24: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > $o ).

tff(pred_def_34,type,
    sP25: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_35,type,
    sP26: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > $o ).

tff(pred_def_36,type,
    sP27: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > $o ).

tff(pred_def_37,type,
    sP28: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > $o ).

tff(pred_def_38,type,
    sP29: 'A_ltln$' > $o ).

tff(pred_def_39,type,
    sP30: 'A_ltln$' > $o ).

tff(pred_def_40,type,
    sP31: 'A_ltln$' > $o ).

tff(pred_def_41,type,
    sP32: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > $o ).

tff(pred_def_42,type,
    sP33: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > $o ).

tff(pred_def_43,type,
    sP34: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > $o ).

tff(pred_def_44,type,
    sP35: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > $o ).

tff(pred_def_45,type,
    sP36: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > $o ).

tff(pred_def_46,type,
    sP37: ( 'A_ltln_set$' * 'A_ltln$' * 'A_ltln$' ) > $o ).

tff(pred_def_47,type,
    sP38: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > $o ).

tff(pred_def_48,type,
    sP39: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_49,type,
    sP40: ( 'A_ltln$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_50,type,
    sP41: ( 'A_ltln$' * 'A_ltln_set$' * 'A_ltln$' ) > $o ).

tff(pred_def_51,type,
    sP42: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_52,type,
    sP43: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > $o ).

tff(pred_def_53,type,
    sP44: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_54,type,
    sP45: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_55,type,
    sP46: ( 'A_ltln_set$' * 'Nat_a_set_fun$' * 'A_ltln$' ) > $o ).

tff(pred_def_56,type,
    sP47: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_57,type,
    sP48: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > $o ).

tff(pred_def_58,type,
    sP49: ( 'Nat_a_set_fun$' * 'A_ltln$' * 'A_ltln_set$' ) > $o ).

tff(pred_def_59,type,
    sP50: ( 'A_ltln_set$' * 'A_ltln$' * 'Nat_a_set_fun$' ) > $o ).

tff(pred_def_60,type,
    sP51: ( 'Nat_a_set_fun$' * 'A_ltln_set$' * 'A_ltln$' ) > $o ).

tff(pred_def_61,type,
    sP52: ( $int * $int * $int ) > $o ).

tff(pred_def_62,type,
    sP53: ( $int * $int * $int ) > $o ).

tff(pred_def_63,type,
    sP54: ( $int * $int * $int ) > $o ).

tff(pred_def_64,type,
    sP55: 'A_ltln$' > $o ).

tff(pred_def_65,type,
    sP56: 'A_ltln$' > $o ).

tff(pred_def_66,type,
    sP57: 'A_ltln$' > $o ).

tff(pred_def_67,type,
    sP58: 'A_ltln$' > $o ).

tff(pred_def_68,type,
    sP59: 'A_ltln$' > $o ).

tff(pred_def_69,type,
    sP60: ( 'A_ltln$' * tlbool ) > $o ).

tff(pred_def_70,type,
    sP61: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_71,type,
    sP62: ( 'A_ltln$' * tlbool ) > $o ).

tff(pred_def_72,type,
    sP63: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_73,type,
    sP64: ( 'A_ltln$' * tlbool ) > $o ).

tff(pred_def_74,type,
    sP65: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_75,type,
    sP66: ( 'A_ltln$' * tlbool ) > $o ).

tff(pred_def_76,type,
    sP67: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_77,type,
    sP68: ( tlbool * 'A_ltln$' ) > $o ).

tff(pred_def_78,type,
    sP69: 'A_ltln$' > $o ).

tff(pred_def_79,type,
    sP70: 'A_ltln$' > $o ).

tff(f2,conjecture,
    'fun_app$'('semantics_ltln$'('w$'),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$','g_F$'('phi$','w$')),'restricted_subformulas$'('phi$')))))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture1) ).

tff(f3,negated_conjecture,
    ~ 'fun_app$'('semantics_ltln$'('w$'),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$','g_F$'('phi$','w$')),'restricted_subformulas$'('phi$')))))),
    inference(negated_conjecture,[status(cth)],[f2]) ).

tff(f4,axiom,
    'member$'('psi$','fun_app$b'('fun_app$c'('inf$','f_G$'('phi$','w$')),'restricted_subformulas$'('phi$'))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis2) ).

tff(f6,axiom,
    ! [X0: 'A_ltln_set$'] :
      ( 'member$'('psi$','restricted_subformulas$'('phi$'))
     => ( 'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$',X0),'restricted_subformulas$'('phi$'))) = 'gF_advice$'('psi$',X0) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom4) ).

tff(f7,axiom,
    ! [X1: 'Nat_a_set_fun$',X0: 'A_ltln$',X2: 'A_ltln$'] :
      ( 'member$'(X2,'f_G$'(X0,X1))
     => 'fun_app$'('semantics_ltln$'(X1),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'(X2,'g_F$'(X0,X1))))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom5) ).

tff(f128,axiom,
    ! [X2: 'A_ltln$',X0: 'A_ltln_set$',X1: 'A_ltln_set$'] :
      ( ( 'less_eq$'(X0,X1)
        & 'member$'(X2,X0) )
     => 'member$'(X2,X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom126) ).

tff(f189,axiom,
    ! [X0: 'A_ltln_set$',X1: 'A_ltln_set$'] : 'less_eq$'('fun_app$b'('fun_app$c'('inf$',X0),X1),X1),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom187) ).

tff(f193,axiom,
    ! [X1: 'A_ltln_set$',X0: 'A_ltln_set$'] : 'less_eq$'('fun_app$b'('fun_app$c'('inf$',X0),X1),X0),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom191) ).

tff(f788,plain,
    ! [X1: 'A_ltln_set$',X0: 'A_ltln_set$'] : 'less_eq$'('fun_app$b'('fun_app$c'('inf$',X1),X0),X1),
    inference(rectify,[],[f193]) ).

tff(f883,plain,
    ~ 'fun_app$'('semantics_ltln$'('w$'),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$','g_F$'('phi$','w$')),'restricted_subformulas$'('phi$')))))),
    inference(flattening,[],[f3]) ).

tff(f1212,plain,
    ! [X0: 'A_ltln$',X2: 'A_ltln$',X1: 'Nat_a_set_fun$'] :
      ( ~ 'member$'(X2,'f_G$'(X0,X1))
      | 'fun_app$'('semantics_ltln$'(X1),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'(X2,'g_F$'(X0,X1))))) ),
    inference(ennf_transformation,[],[f7]) ).

tff(f1382,plain,
    ! [X0: 'A_ltln_set$'] :
      ( ( 'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$',X0),'restricted_subformulas$'('phi$'))) = 'gF_advice$'('psi$',X0) )
      | ~ 'member$'('psi$','restricted_subformulas$'('phi$')) ),
    inference(ennf_transformation,[],[f6]) ).

tff(f1383,plain,
    ! [X2: 'A_ltln$',X0: 'A_ltln_set$',X1: 'A_ltln_set$'] :
      ( 'member$'(X2,X1)
      | ~ 'less_eq$'(X0,X1)
      | ~ 'member$'(X2,X0) ),
    inference(ennf_transformation,[],[f128]) ).

tff(f1384,plain,
    ! [X2: 'A_ltln$',X0: 'A_ltln_set$',X1: 'A_ltln_set$'] :
      ( 'member$'(X2,X1)
      | ~ 'less_eq$'(X0,X1)
      | ~ 'member$'(X2,X0) ),
    inference(flattening,[],[f1383]) ).

tff(f1878,plain,
    ! [X0: 'A_ltln$',X1: 'A_ltln_set$',X2: 'A_ltln_set$'] :
      ( 'member$'(X0,X2)
      | ~ 'less_eq$'(X1,X2)
      | ~ 'member$'(X0,X1) ),
    inference(rectify,[],[f1384]) ).

tff(f2152,plain,
    ! [X0: 'A_ltln_set$',X1: 'A_ltln_set$'] : 'less_eq$'('fun_app$b'('fun_app$c'('inf$',X0),X1),X0),
    inference(rectify,[],[f788]) ).

tff(f2187,plain,
    ! [X0: 'A_ltln$',X1: 'A_ltln$',X2: 'Nat_a_set_fun$'] :
      ( ~ 'member$'(X1,'f_G$'(X0,X2))
      | 'fun_app$'('semantics_ltln$'(X2),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'(X1,'g_F$'(X0,X2))))) ),
    inference(rectify,[],[f1212]) ).

tff(f2783,plain,
    ! [X2: 'A_ltln_set$',X0: 'A_ltln$',X1: 'A_ltln_set$'] :
      ( ~ 'member$'(X0,X1)
      | ~ 'less_eq$'(X1,X2)
      | 'member$'(X0,X2) ),
    inference(cnf_transformation,[],[f1878]) ).

tff(f3007,plain,
    'member$'('psi$','fun_app$b'('fun_app$c'('inf$','f_G$'('phi$','w$')),'restricted_subformulas$'('phi$'))),
    inference(cnf_transformation,[],[f4]) ).

tff(f3090,plain,
    ~ 'fun_app$'('semantics_ltln$'('w$'),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$','g_F$'('phi$','w$')),'restricted_subformulas$'('phi$')))))),
    inference(cnf_transformation,[],[f883]) ).

tff(f3183,plain,
    ! [X0: 'A_ltln_set$',X1: 'A_ltln_set$'] : 'less_eq$'('fun_app$b'('fun_app$c'('inf$',X0),X1),X1),
    inference(cnf_transformation,[],[f189]) ).

tff(f3188,plain,
    ! [X0: 'A_ltln_set$',X1: 'A_ltln_set$'] : 'less_eq$'('fun_app$b'('fun_app$c'('inf$',X0),X1),X0),
    inference(cnf_transformation,[],[f2152]) ).

tff(f3249,plain,
    ! [X2: 'Nat_a_set_fun$',X0: 'A_ltln$',X1: 'A_ltln$'] :
      ( 'fun_app$'('semantics_ltln$'(X2),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'(X1,'g_F$'(X0,X2)))))
      | ~ 'member$'(X1,'f_G$'(X0,X2)) ),
    inference(cnf_transformation,[],[f2187]) ).

tff(f3548,plain,
    ! [X0: 'A_ltln_set$'] :
      ( ~ 'member$'('psi$','restricted_subformulas$'('phi$'))
      | ( 'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$',X0),'restricted_subformulas$'('phi$'))) = 'gF_advice$'('psi$',X0) ) ),
    inference(cnf_transformation,[],[f1382]) ).

tff(f3764,definition,
    ( spl467_6
  <=> ! [X0: 'A_ltln_set$'] : ( 'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$',X0),'restricted_subformulas$'('phi$'))) = 'gF_advice$'('psi$',X0) ) ),
    introduced(definition,[new_symbols(definition,[spl467_6])],[avatar_definition]) ).

tff(f3765,plain,
    ( ! [X0: 'A_ltln_set$'] : ( 'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$',X0),'restricted_subformulas$'('phi$'))) = 'gF_advice$'('psi$',X0) )
    | ~ spl467_6 ),
    inference(avatar_component_clause,[],[f3764]) ).

tff(f3767,definition,
    ( spl467_7
  <=> 'member$'('psi$','restricted_subformulas$'('phi$')) ),
    introduced(definition,[new_symbols(definition,[spl467_7])],[avatar_definition]) ).

tff(f3770,plain,
    ( spl467_6
    | ~ spl467_7 ),
    inference(avatar_split_clause,[],[f3548,f3767,f3764]) ).

tff(f3831,definition,
    ( spl467_14
  <=> 'fun_app$'('semantics_ltln$'('w$'),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$','g_F$'('phi$','w$')),'restricted_subformulas$'('phi$')))))) ),
    introduced(definition,[new_symbols(definition,[spl467_14])],[avatar_definition]) ).

tff(f3833,plain,
    ( ~ 'fun_app$'('semantics_ltln$'('w$'),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'('psi$','fun_app$b'('fun_app$c'('inf$','g_F$'('phi$','w$')),'restricted_subformulas$'('phi$'))))))
    | spl467_14 ),
    inference(avatar_component_clause,[],[f3831]) ).

tff(f3834,plain,
    ~ spl467_14,
    inference(avatar_split_clause,[],[f3090,f3831]) ).

tff(f3853,definition,
    ( spl467_17
  <=> 'member$'('psi$','fun_app$b'('fun_app$c'('inf$','f_G$'('phi$','w$')),'restricted_subformulas$'('phi$'))) ),
    introduced(definition,[new_symbols(definition,[spl467_17])],[avatar_definition]) ).

tff(f3855,plain,
    ( 'member$'('psi$','fun_app$b'('fun_app$c'('inf$','f_G$'('phi$','w$')),'restricted_subformulas$'('phi$')))
    | ~ spl467_17 ),
    inference(avatar_component_clause,[],[f3853]) ).

tff(f3856,plain,
    spl467_17,
    inference(avatar_split_clause,[],[f3007,f3853]) ).

tff(f3935,plain,
    ( 'member$'('psi$','f_G$'('phi$','w$'))
    | ~ spl467_17 ),
    inference(unit_resulting_resolution,[],[f2783,f3188,f3855]) ).

tff(f3937,plain,
    ( 'member$'('psi$','restricted_subformulas$'('phi$'))
    | ~ spl467_17 ),
    inference(unit_resulting_resolution,[],[f2783,f3183,f3855]) ).

tff(f3945,definition,
    ( spl467_21
  <=> 'member$'('psi$','f_G$'('phi$','w$')) ),
    introduced(definition,[new_symbols(definition,[spl467_21])],[avatar_definition]) ).

tff(f3948,plain,
    ( spl467_21
    | ~ spl467_17 ),
    inference(avatar_split_clause,[],[f3935,f3853,f3945]) ).

tff(f3954,plain,
    ( spl467_7
    | ~ spl467_17 ),
    inference(avatar_split_clause,[],[f3937,f3853,f3767]) ).

tff(f4107,definition,
    ( spl467_30
  <=> 'fun_app$'('semantics_ltln$'('w$'),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'('psi$','g_F$'('phi$','w$'))))) ),
    introduced(definition,[new_symbols(definition,[spl467_30])],[avatar_definition]) ).

tff(f4109,plain,
    ( ~ 'fun_app$'('semantics_ltln$'('w$'),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'('psi$','g_F$'('phi$','w$')))))
    | spl467_30 ),
    inference(avatar_component_clause,[],[f4107]) ).

tff(f4532,plain,
    ( ~ 'fun_app$'('semantics_ltln$'('w$'),'fun_app$a'('until_ltln$'('true_ltln$'),'fun_app$a'('release_ltln$'('false_ltln$'),'gF_advice$'('psi$','g_F$'('phi$','w$')))))
    | ~ spl467_6
    | spl467_14 ),
    inference(superposition,[],[f3833,f3765]) ).

tff(f5814,plain,
    ( ~ 'member$'('psi$','f_G$'('phi$','w$'))
    | spl467_30 ),
    inference(unit_resulting_resolution,[],[f3249,f4109]) ).

tff(f5830,plain,
    ( ~ spl467_21
    | spl467_30 ),
    inference(avatar_split_clause,[],[f5814,f4107,f3945]) ).

tff(f5832,plain,
    ( ~ spl467_30
    | ~ spl467_6
    | spl467_14 ),
    inference(avatar_split_clause,[],[f4532,f3831,f3764,f4107]) ).

tff(f5839,plain,
    $false,
    inference(avatar_smt_refutation,[],[f5832,f5830,f3954,f3948,f3856,f3834,f3770]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : ITP371_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.39  % Computer : n026.cluster.edu
% 0.10/0.39  % Model    : x86_64 x86_64
% 0.10/0.39  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39  % Memory   : 8046.5625MB
% 0.10/0.39  % OS       : Linux 6.8.0-71-generic
% 0.10/0.39  % CPULimit : 300
% 0.10/0.39  % WCLimit  : 300
% 0.10/0.39  % DateTime : Sun Sep 27 12:59:12 UTC 2026
% 0.10/0.39  % CPUTime  : 
% 0.10/0.39  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.43  Running first-order theorem proving
% 0.10/0.43  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.48/1.79  % (2822224)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.48/1.79  % (2822286)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3321390759:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.48/1.79  % (2822284)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=377908119:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.48/1.79  % (2822286)Instruction limit reached! 
% 4.48/1.79  % (2822286)------------------------------
% 4.48/1.79  % (2822286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.48/1.79  % (2822286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.48/1.79  % (2822286)CaDiCaL version: 2.1.3
% 4.48/1.79  % (2822286)Termination reason: Instruction limit
% 4.48/1.79  % (2822286)Termination phase: Property scanning
% 4.48/1.79  % (2822286)Time elapsed: 0.005 s
% 4.48/1.79  % (2822286)Peak memory usage: 86 MB
% 4.48/1.79  % (2822286)Instructions burned: 8 (million)
% 4.48/1.79  % (2822282)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1380797949:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.48/1.79  % (2822282)Instruction limit reached! 
% 4.48/1.79  % (2822282)------------------------------
% 4.48/1.79  % (2822282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.48/1.79  % (2822282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.48/1.79  % (2822282)CaDiCaL version: 2.1.3
% 4.48/1.79  % (2822282)Termination reason: Instruction limit
% 4.48/1.79  % (2822282)Termination phase: Property scanning
% 4.48/1.79  % (2822282)Time elapsed: 0.012 s
% 4.48/1.79  % (2822282)Peak memory usage: 85 MB
% 4.48/1.79  % (2822282)Instructions burned: 13 (million)
% 4.48/1.79  % (2822283)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3810191650:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.48/1.79  % (2822289)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1523156033:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.48/1.79  % (2822287)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4091601604:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.48/1.79  % (2822287)Instruction limit reached! 
% 4.48/1.79  % (2822287)------------------------------
% 4.48/1.79  % (2822287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.48/1.79  % (2822287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.48/1.79  % (2822287)CaDiCaL version: 2.1.3
% 4.48/1.79  % (2822287)Termination reason: Instruction limit
% 4.48/1.79  % (2822287)Termination phase: Property scanning
% 4.48/1.79  % (2822287)Time elapsed: 0.005 s
% 4.48/1.79  % (2822287)Peak memory usage: 86 MB
% 4.48/1.79  % (2822287)Instructions burned: 5 (million)
% 4.48/1.79  % (2822290)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=310892718:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.48/1.79  % (2822289)Instruction limit reached! 
% 4.48/1.79  % (2822289)------------------------------
% 4.48/1.79  % (2822289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.48/1.79  % (2822289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.48/1.79  % (2822289)CaDiCaL version: 2.1.3
% 4.48/1.79  % (2822289)Termination reason: Instruction limit
% 4.48/1.79  % (2822289)Termination phase: Property scanning
% 4.48/1.79  % (2822289)Time elapsed: 0.028 s
% 4.48/1.79  % (2822289)Peak memory usage: 88 MB
% 4.48/1.79  % (2822289)Instructions burned: 47 (million)
% 4.48/1.79  % (2822284)Instruction limit reached! 
% 4.48/1.79  % (2822284)------------------------------
% 4.48/1.79  % (2822284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.48/1.79  % (2822284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.48/1.79  % (2822284)CaDiCaL version: 2.1.3
% 4.48/1.79  % (2822284)Termination reason: Instruction limit
% 4.48/1.79  % (2822284)Termination phase: Saturation
% 4.48/1.79  % (2822284)Time elapsed: 0.116 s
% 4.48/1.79  % (2822284)Peak memory usage: 119 MB
% 4.48/1.79  % (2822284)Instructions burned: 203 (million)
% 4.48/1.79  % (2822290)Instruction limit reached! 
% 4.48/1.79  % (2822290)------------------------------
% 4.48/1.79  % (2822290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.48/1.79  % (2822290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.97  % (2822290)CaDiCaL version: 2.1.3
% 6.01/1.97  % (2822290)Termination reason: Instruction limit
% 6.01/1.97  % (2822290)Termination phase: Preprocessing 3
% 6.01/1.97  % (2822290)Time elapsed: 0.033 s
% 6.01/1.97  % (2822290)Peak memory usage: 88 MB
% 6.01/1.97  % (2822290)Instructions burned: 34 (million)
% 6.01/1.97  % (2822295)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2833394105:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 6.01/1.97  % (2822295)Instruction limit reached! 
% 6.01/1.97  % (2822295)------------------------------
% 6.01/1.97  % (2822295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.97  % (2822295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.97  % (2822295)CaDiCaL version: 2.1.3
% 6.01/1.97  % (2822295)Termination reason: Instruction limit
% 6.01/1.97  % (2822295)Termination phase: SInE selection
% 6.01/1.97  % (2822295)Time elapsed: 0.014 s
% 6.01/1.97  % (2822295)Peak memory usage: 86 MB
% 6.01/1.97  % (2822295)Instructions burned: 14 (million)
% 6.01/1.97  % (2822311)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=3437868141:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.01/1.97  % (2822311)Instruction limit reached! 
% 6.01/1.97  % (2822311)------------------------------
% 6.01/1.97  % (2822311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.97  % (2822311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.97  % (2822311)CaDiCaL version: 2.1.3
% 6.01/1.97  % (2822311)Termination reason: Instruction limit
% 6.01/1.97  % (2822311)Termination phase: Naming
% 6.01/1.97  % (2822311)Time elapsed: 0.009 s
% 6.01/1.97  % (2822311)Peak memory usage: 87 MB
% 6.01/1.97  % (2822311)Instructions burned: 29 (million)
% 6.01/1.97  % (2822303)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=2007916810:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.01/1.97  % (2822303)Instruction limit reached! 
% 6.01/1.97  % (2822303)------------------------------
% 6.01/1.97  % (2822303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.97  % (2822303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.97  % (2822303)CaDiCaL version: 2.1.3
% 6.01/1.97  % (2822303)Termination reason: Instruction limit
% 6.01/1.97  % (2822303)Termination phase: Preprocessing 3
% 6.01/1.97  % (2822303)Time elapsed: 0.023 s
% 6.01/1.97  % (2822303)Peak memory usage: 87 MB
% 6.01/1.97  % (2822303)Instructions burned: 29 (million)
% 6.01/1.97  % (2822306)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3737936237:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 6.01/1.97  % (2822309)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2983896109:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 6.01/1.97  % (2822306)Instruction limit reached! 
% 6.01/1.97  % (2822306)------------------------------
% 6.01/1.97  % (2822306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.97  % (2822306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.97  % (2822306)CaDiCaL version: 2.1.3
% 6.01/1.97  % (2822306)Termination reason: Instruction limit
% 6.01/1.97  % (2822306)Termination phase: Preprocessing 1
% 6.01/1.97  % (2822306)Time elapsed: 0.016 s
% 6.01/1.97  % (2822306)Peak memory usage: 86 MB
% 6.01/1.97  % (2822306)Instructions burned: 16 (million)
% 6.01/1.97  % (2822309)Instruction limit reached! 
% 6.01/1.97  % (2822309)------------------------------
% 6.01/1.97  % (2822309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.97  % (2822309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.97  % (2822309)CaDiCaL version: 2.1.3
% 6.01/1.97  % (2822309)Termination reason: Instruction limit
% 6.01/1.97  % (2822309)Termination phase: Preprocessing 1
% 6.01/1.97  % (2822309)Time elapsed: 0.019 s
% 6.01/1.97  % (2822309)Peak memory usage: 86 MB
% 6.01/1.97  % (2822309)Instructions burned: 24 (million)
% 6.01/1.97  % (2822312)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2348631641:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.01/1.97  % (2822320)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2353862456:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 7.89/2.17  % (2822283)Instruction limit reached! 
% 7.89/2.17  % (2822283)------------------------------
% 7.89/2.17  % (2822283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/2.17  % (2822283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/2.17  % (2822283)CaDiCaL version: 2.1.3
% 7.89/2.17  % (2822283)Termination reason: Instruction limit
% 7.89/2.17  % (2822283)Termination phase: Clausification
% 7.89/2.17  % (2822283)Time elapsed: 0.336 s
% 7.89/2.17  % (2822283)Peak memory usage: 176 MB
% 7.89/2.17  % (2822283)Instructions burned: 307 (million)
% 7.89/2.17  % (2822312)Instruction limit reached! 
% 7.89/2.17  % (2822312)------------------------------
% 7.89/2.17  % (2822312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/2.17  % (2822312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/2.17  % (2822312)CaDiCaL version: 2.1.3
% 7.89/2.17  % (2822312)Termination reason: Instruction limit
% 7.89/2.17  % (2822312)Termination phase: Property scanning
% 7.89/2.17  % (2822312)Time elapsed: 0.064 s
% 7.89/2.17  % (2822312)Peak memory usage: 89 MB
% 7.89/2.17  % (2822312)Instructions burned: 86 (million)
% 7.89/2.17  % (2822317)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1177003527:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 7.89/2.17  % (2822317)Instruction limit reached! 
% 7.89/2.17  % (2822317)------------------------------
% 7.89/2.17  % (2822317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/2.17  % (2822317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/2.17  % (2822317)CaDiCaL version: 2.1.3
% 7.89/2.17  % (2822317)Termination reason: Instruction limit
% 7.89/2.17  % (2822317)Termination phase: shuffling
% 7.89/2.17  % (2822317)Time elapsed: 0.003 s
% 7.89/2.17  % (2822317)Peak memory usage: 85 MB
% 7.89/2.17  % (2822317)Instructions burned: 2 (million)
% 7.89/2.17  % (2822323)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=216590572:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 7.89/2.17  % (2822320)Instruction limit reached! 
% 7.89/2.17  % (2822320)------------------------------
% 7.89/2.17  % (2822320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/2.17  % (2822320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/2.17  % (2822320)CaDiCaL version: 2.1.3
% 7.89/2.17  % (2822320)Termination reason: Instruction limit
% 7.89/2.17  % (2822320)Termination phase: Saturation
% 7.89/2.17  % (2822320)Time elapsed: 0.084 s
% 7.89/2.17  % (2822320)Peak memory usage: 92 MB
% 7.89/2.17  % (2822320)Instructions burned: 183 (million)
% 7.89/2.17  % (2822323)Instruction limit reached! 
% 7.89/2.17  % (2822323)------------------------------
% 7.89/2.17  % (2822323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/2.17  % (2822323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/2.17  % (2822323)CaDiCaL version: 2.1.3
% 7.89/2.17  % (2822323)Termination reason: Instruction limit
% 7.89/2.17  % (2822323)Termination phase: Property scanning
% 7.89/2.17  % (2822323)Time elapsed: 0.004 s
% 7.89/2.17  % (2822323)Peak memory usage: 86 MB
% 7.89/2.17  % (2822323)Instructions burned: 4 (million)
% 7.89/2.17  % (2822325)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3616717306:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 7.89/2.17  % (2822325)Instruction limit reached! 
% 7.89/2.17  % (2822325)------------------------------
% 7.89/2.17  % (2822325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/2.17  % (2822325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/2.17  % (2822325)CaDiCaL version: 2.1.3
% 7.89/2.17  % (2822325)Termination reason: Instruction limit
% 7.89/2.17  % (2822325)Termination phase: Property scanning
% 7.89/2.17  % (2822325)Time elapsed: 0.038 s
% 7.89/2.17  % (2822325)Peak memory usage: 88 MB
% 7.89/2.17  % (2822325)Instructions burned: 68 (million)
% 7.89/2.17  % (2822327)lrs+10_1_thi=all:si=on:fd=off:random_seed=1858033702:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 7.89/2.17  % (2822339)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3045360219:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 7.89/2.17  % (2822327)Instruction limit reached! 
% 8.92/2.42  % (2822327)------------------------------
% 8.92/2.42  % (2822327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.42  % (2822327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.42  % (2822327)CaDiCaL version: 2.1.3
% 8.92/2.42  % (2822327)Termination reason: Instruction limit
% 8.92/2.42  % (2822327)Termination phase: Preprocessing 3
% 8.92/2.42  % (2822327)Time elapsed: 0.041 s
% 8.92/2.42  % (2822327)Peak memory usage: 88 MB
% 8.92/2.42  % (2822327)Instructions burned: 53 (million)
% 8.92/2.42  % (2822335)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=659239837:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 8.92/2.42  % (2822335)Instruction limit reached! 
% 8.92/2.42  % (2822335)------------------------------
% 8.92/2.42  % (2822335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.42  % (2822335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.42  % (2822335)CaDiCaL version: 2.1.3
% 8.92/2.42  % (2822335)Termination reason: Instruction limit
% 8.92/2.42  % (2822335)Termination phase: shuffling
% 8.92/2.42  % (2822335)Time elapsed: 0.009 s
% 8.92/2.42  % (2822335)Peak memory usage: 85 MB
% 8.92/2.42  % (2822335)Instructions burned: 9 (million)
% 8.92/2.42  % (2822339)Instruction limit reached! 
% 8.92/2.42  % (2822339)------------------------------
% 8.92/2.42  % (2822339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.42  % (2822339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.42  % (2822339)CaDiCaL version: 2.1.3
% 8.92/2.42  % (2822339)Termination reason: Instruction limit
% 8.92/2.42  % (2822339)Termination phase: Saturation
% 8.92/2.42  % (2822339)Time elapsed: 0.059 s
% 8.92/2.42  % (2822339)Peak memory usage: 118 MB
% 8.92/2.42  % (2822339)Instructions burned: 127 (million)
% 8.92/2.42  % (2822336)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1580774816:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 8.92/2.42  % (2822336)Instruction limit reached! 
% 8.92/2.42  % (2822336)------------------------------
% 8.92/2.42  % (2822336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.42  % (2822336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.42  % (2822336)CaDiCaL version: 2.1.3
% 8.92/2.42  % (2822336)Termination reason: Instruction limit
% 8.92/2.42  % (2822336)Termination phase: shuffling
% 8.92/2.42  % (2822336)Time elapsed: 0.003 s
% 8.92/2.42  % (2822336)Peak memory usage: 85 MB
% 8.92/2.42  % (2822336)Instructions burned: 2 (million)
% 8.92/2.42  % (2822337)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2475328126:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 8.92/2.42  % (2822337)Instruction limit reached! 
% 8.92/2.42  % (2822337)------------------------------
% 8.92/2.42  % (2822337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.42  % (2822337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.42  % (2822337)CaDiCaL version: 2.1.3
% 8.92/2.42  % (2822337)Termination reason: Instruction limit
% 8.92/2.42  % (2822337)Termination phase: shuffling
% 8.92/2.42  % (2822337)Time elapsed: 0.003 s
% 8.92/2.42  % (2822337)Peak memory usage: 85 MB
% 8.92/2.42  % (2822337)Instructions burned: 2 (million)
% 8.92/2.42  % (2822340)dis+10_1_si=on:random_seed=1816958809:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 8.92/2.42  % (2822340)Instruction limit reached! 
% 8.92/2.42  % (2822340)------------------------------
% 8.92/2.42  % (2822340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.42  % (2822340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.42  % (2822340)CaDiCaL version: 2.1.3
% 8.92/2.42  % (2822340)Termination reason: Instruction limit
% 8.92/2.42  % (2822340)Termination phase: Property scanning
% 8.92/2.42  % (2822340)Time elapsed: 0.011 s
% 8.92/2.42  % (2822340)Peak memory usage: 85 MB
% 8.92/2.42  % (2822340)Instructions burned: 11 (million)
% 8.92/2.42  % (2822346)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=426518789:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 8.92/2.42  % (2822355)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3449679709:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 8.92/2.42  % (2822355)Instruction limit reached! 
% 10.56/2.75  % (2822355)------------------------------
% 10.56/2.75  % (2822355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.75  % (2822355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.75  % (2822355)CaDiCaL version: 2.1.3
% 10.56/2.75  % (2822355)Termination reason: Instruction limit
% 10.56/2.75  % (2822355)Termination phase: Property scanning
% 10.56/2.75  % (2822355)Time elapsed: 0.005 s
% 10.56/2.75  % (2822355)Peak memory usage: 86 MB
% 10.56/2.75  % (2822355)Instructions burned: 9 (million)
% 10.56/2.75  % (2822346)Instruction limit reached! 
% 10.56/2.75  % (2822346)------------------------------
% 10.56/2.75  % (2822346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.75  % (2822346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.75  % (2822346)CaDiCaL version: 2.1.3
% 10.56/2.75  % (2822346)Termination reason: Instruction limit
% 10.56/2.75  % (2822346)Termination phase: Preprocessing 2
% 10.56/2.75  % (2822346)Time elapsed: 0.021 s
% 10.56/2.75  % (2822346)Peak memory usage: 87 MB
% 10.56/2.75  % (2822346)Instructions burned: 26 (million)
% 10.56/2.75  % (2822352)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1242053331:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2992 on theBenchmark for (2992ds/35Mi)
% 10.56/2.75  % (2822353)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=822505296:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi)
% 10.56/2.75  % (2822352)Instruction limit reached! 
% 10.56/2.75  % (2822352)------------------------------
% 10.56/2.75  % (2822352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.75  % (2822352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.75  % (2822352)CaDiCaL version: 2.1.3
% 10.56/2.75  % (2822352)Termination reason: Instruction limit
% 10.56/2.75  % (2822352)Termination phase: Preprocessing 3
% 10.56/2.75  % (2822352)Time elapsed: 0.036 s
% 10.56/2.75  % (2822352)Peak memory usage: 88 MB
% 10.56/2.75  % (2822352)Instructions burned: 35 (million)
% 10.56/2.75  % (2822353)Instruction limit reached! 
% 10.56/2.75  % (2822353)------------------------------
% 10.56/2.75  % (2822353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.75  % (2822353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.75  % (2822353)CaDiCaL version: 2.1.3
% 10.56/2.75  % (2822353)Termination reason: Instruction limit
% 10.56/2.75  % (2822353)Termination phase: shuffling
% 10.56/2.75  % (2822353)Time elapsed: 0.003 s
% 10.56/2.75  % (2822353)Peak memory usage: 85 MB
% 10.56/2.75  % (2822353)Instructions burned: 2 (million)
% 10.56/2.75  % (2822357)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=4131709828:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 10.56/2.75  % (2822361)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2174707884:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi)
% 10.56/2.75  % (2822361)Instruction limit reached! 
% 10.56/2.75  % (2822361)------------------------------
% 10.56/2.75  % (2822361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.75  % (2822361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.75  % (2822361)CaDiCaL version: 2.1.3
% 10.56/2.75  % (2822361)Termination reason: Instruction limit
% 10.56/2.75  % (2822361)Termination phase: Property scanning
% 10.56/2.75  % (2822361)Time elapsed: 0.012 s
% 10.56/2.75  % (2822361)Peak memory usage: 85 MB
% 10.56/2.75  % (2822361)Instructions burned: 13 (million)
% 10.56/2.75  % (2822362)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1602929130:i=226:rtra=on:gtg=position:ss=axioms_2991 on theBenchmark for (2991ds/226Mi)
% 10.56/2.75  % (2822368)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=895780093:i=71:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/71Mi)
% 10.56/2.75  % (2822367)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3802873264:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi)
% 10.56/2.75  % (2822367)Instruction limit reached! 
% 10.56/2.75  % (2822367)------------------------------
% 10.56/2.75  % (2822367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.75  % (2822367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/3.04  % (2822367)CaDiCaL version: 2.1.3
% 11.50/3.04  % (2822367)Termination reason: Instruction limit
% 11.50/3.04  % (2822367)Termination phase: Property scanning
% 11.50/3.04  % (2822367)Time elapsed: 0.011 s
% 11.50/3.04  % (2822367)Peak memory usage: 85 MB
% 11.50/3.04  % (2822367)Instructions burned: 11 (million)
% 11.50/3.04  % (2822374)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=2621123387:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2989 on theBenchmark for (2989ds/294Mi)
% 11.50/3.04  % (2822368)Instruction limit reached! 
% 11.50/3.04  % (2822368)------------------------------
% 11.50/3.04  % (2822368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/3.04  % (2822368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/3.04  % (2822368)CaDiCaL version: 2.1.3
% 11.50/3.04  % (2822368)Termination reason: Instruction limit
% 11.50/3.04  % (2822368)Termination phase: Property scanning
% 11.50/3.04  % (2822368)Time elapsed: 0.066 s
% 11.50/3.04  % (2822368)Peak memory usage: 88 MB
% 11.50/3.04  % (2822368)Instructions burned: 72 (million)
% 11.50/3.04  % (2822373)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=3545026840:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi)
% 11.50/3.04  % (2822386)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1371171515:i=131:rtra=on_2988 on theBenchmark for (2988ds/131Mi)
% 11.50/3.04  % (2822373)Instruction limit reached! 
% 11.50/3.04  % (2822373)------------------------------
% 11.50/3.04  % (2822373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/3.04  % (2822373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/3.04  % (2822373)CaDiCaL version: 2.1.3
% 11.50/3.04  % (2822373)Termination reason: Instruction limit
% 11.50/3.04  % (2822373)Termination phase: Saturation
% 11.50/3.04  % (2822373)Time elapsed: 0.057 s
% 11.50/3.04  % (2822373)Peak memory usage: 89 MB
% 11.50/3.04  % (2822373)Instructions burned: 76 (million)
% 11.50/3.04  % (2822379)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3867834885:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/130Mi)
% 11.50/3.04  % (2822362)Instruction limit reached! 
% 11.50/3.04  % (2822362)------------------------------
% 11.50/3.04  % (2822362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/3.04  % (2822362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/3.04  % (2822362)CaDiCaL version: 2.1.3
% 11.50/3.04  % (2822362)Termination reason: Instruction limit
% 11.50/3.04  % (2822362)Termination phase: Saturation
% 11.50/3.04  % (2822362)Time elapsed: 0.238 s
% 11.50/3.04  % (2822362)Peak memory usage: 118 MB
% 11.50/3.04  % (2822362)Instructions burned: 226 (million)
% 11.50/3.04  % (2822386)Instruction limit reached! 
% 11.50/3.04  % (2822386)------------------------------
% 11.50/3.04  % (2822386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/3.04  % (2822386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/3.04  % (2822386)CaDiCaL version: 2.1.3
% 11.50/3.04  % (2822386)Termination reason: Instruction limit
% 11.50/3.04  % (2822386)Termination phase: Saturation
% 11.50/3.04  % (2822386)Time elapsed: 0.069 s
% 11.50/3.04  % (2822386)Peak memory usage: 136 MB
% 11.50/3.04  % (2822386)Instructions burned: 133 (million)
% 11.50/3.04  % (2822357)Instruction limit reached! 
% 11.50/3.04  % (2822357)------------------------------
% 11.50/3.04  % (2822357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/3.04  % (2822357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/3.04  % (2822357)CaDiCaL version: 2.1.3
% 11.50/3.04  % (2822357)Termination reason: Instruction limit
% 11.50/3.04  % (2822357)Termination phase: Saturation
% 11.50/3.04  % (2822357)Time elapsed: 0.318 s
% 11.50/3.04  % (2822357)Peak memory usage: 96 MB
% 11.50/3.04  % (2822357)Instructions burned: 370 (million)
% 11.50/3.04  % (2822387)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=330187907:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/40Mi)
% 11.50/3.04  % (2822379)Instruction limit reached! 
% 11.50/3.04  % (2822379)------------------------------
% 11.50/3.04  % (2822379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/3.04  % (2822379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822379)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822379)Termination reason: Instruction limit
% 15.11/3.34  % (2822379)Termination phase: Clausification
% 15.11/3.34  % (2822379)Time elapsed: 0.125 s
% 15.11/3.34  % (2822379)Peak memory usage: 112 MB
% 15.11/3.34  % (2822379)Instructions burned: 130 (million)
% 15.11/3.34  % (2822387)Instruction limit reached! 
% 15.11/3.34  % (2822387)------------------------------
% 15.11/3.34  % (2822387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822387)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822387)Termination reason: Instruction limit
% 15.11/3.34  % (2822387)Termination phase: Preprocessing 1
% 15.11/3.34  % (2822387)Time elapsed: 0.029 s
% 15.11/3.34  % (2822387)Peak memory usage: 86 MB
% 15.11/3.34  % (2822387)Instructions burned: 40 (million)
% 15.11/3.34  % (2822374)Instruction limit reached! 
% 15.11/3.34  % (2822374)------------------------------
% 15.11/3.34  % (2822374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822374)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822374)Termination reason: Instruction limit
% 15.11/3.34  % (2822374)Termination phase: Clausification
% 15.11/3.34  % (2822374)Time elapsed: 0.304 s
% 15.11/3.34  % (2822374)Peak memory usage: 166 MB
% 15.11/3.34  % (2822374)Instructions burned: 295 (million)
% 15.11/3.34  % (2822400)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=1171341487:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2986 on theBenchmark for (2986ds/259Mi)
% 15.11/3.34  % (2822398)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=168212979:i=131:canc=cautious:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 15.11/3.34  % (2822394)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3890556473:i=307:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/307Mi)
% 15.11/3.34  % (2822396)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1954908441:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/598Mi)
% 15.11/3.34  % (2822404)dis+10_1_si=on:random_seed=1159918280:s2a=on:i=1000:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/1000Mi)
% 15.11/3.34  % (2822400)Instruction limit reached! 
% 15.11/3.34  % (2822400)------------------------------
% 15.11/3.34  % (2822400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822400)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822400)Termination reason: Instruction limit
% 15.11/3.34  % (2822400)Termination phase: Saturation
% 15.11/3.34  % (2822400)Time elapsed: 0.134 s
% 15.11/3.34  % (2822400)Peak memory usage: 119 MB
% 15.11/3.34  % (2822400)Instructions burned: 261 (million)
% 15.11/3.34  % (2822405)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=4077377433:i=383:fsr=off:rtra=on:ev=force_2985 on theBenchmark for (2985ds/383Mi)
% 15.11/3.34  % (2822398)Instruction limit reached! 
% 15.11/3.34  % (2822398)------------------------------
% 15.11/3.34  % (2822398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822398)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822398)Termination reason: Instruction limit
% 15.11/3.34  % (2822398)Termination phase: Saturation
% 15.11/3.34  % (2822398)Time elapsed: 0.153 s
% 15.11/3.34  % (2822398)Peak memory usage: 119 MB
% 15.11/3.34  % (2822398)Instructions burned: 131 (million)
% 15.11/3.34  % (2822406)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1527150118:i=141:doe=on:rtra=on_2985 on theBenchmark for (2985ds/141Mi)
% 15.11/3.34  % (2822394)Instruction limit reached! 
% 15.11/3.34  % (2822394)------------------------------
% 15.11/3.34  % (2822394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822394)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822394)Termination reason: Instruction limit
% 15.11/3.34  % (2822394)Termination phase: Saturation
% 15.11/3.34  % (2822394)Time elapsed: 0.249 s
% 15.11/3.34  % (2822394)Peak memory usage: 93 MB
% 15.11/3.34  % (2822394)Instructions burned: 307 (million)
% 15.11/3.34  % (2822418)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1432769876:i=65:nm=16:rtra=on_2983 on theBenchmark for (2983ds/65Mi)
% 15.11/3.34  % (2822406)Instruction limit reached! 
% 15.11/3.34  % (2822406)------------------------------
% 15.11/3.34  % (2822406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822406)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822406)Termination reason: Instruction limit
% 15.11/3.34  % (2822406)Termination phase: Saturation
% 15.11/3.34  % (2822406)Time elapsed: 0.118 s
% 15.11/3.34  % (2822406)Peak memory usage: 92 MB
% 15.11/3.34  % (2822406)Instructions burned: 141 (million)
% 15.11/3.34  % (2822418)Instruction limit reached! 
% 15.11/3.34  % (2822418)------------------------------
% 15.11/3.34  % (2822418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822418)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822418)Termination reason: Instruction limit
% 15.11/3.34  % (2822418)Termination phase: Property scanning
% 15.11/3.34  % (2822418)Time elapsed: 0.027 s
% 15.11/3.34  % (2822418)Peak memory usage: 88 MB
% 15.11/3.34  % (2822418)Instructions burned: 66 (million)
% 15.11/3.34  % (2822421)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1218758650:i=121:nm=16:rtra=on_2983 on theBenchmark for (2983ds/121Mi)
% 15.11/3.34  % (2822396)First to succeed.
% 15.11/3.34  % (2822396)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2822224"
% 15.11/3.34  % (2822427)dis+1010_1_to=kbo:si=on:random_seed=815771617:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2982 on theBenchmark for (2982ds/175Mi)
% 15.11/3.34  % (2822423)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=1803693025:s2a=on:i=128:s2at=5:ins=3:rtra=on_2982 on theBenchmark for (2982ds/128Mi)
% 15.11/3.34  % (2822421)Instruction limit reached! 
% 15.11/3.34  % (2822421)------------------------------
% 15.11/3.34  % (2822421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822421)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822421)Termination reason: Instruction limit
% 15.11/3.34  % (2822421)Termination phase: Saturation
% 15.11/3.34  % (2822421)Time elapsed: 0.119 s
% 15.11/3.34  % (2822421)Peak memory usage: 91 MB
% 15.11/3.34  % (2822421)Instructions burned: 121 (million)
% 15.11/3.34  % (2822425)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=748385059:i=39:ins=3:rtra=on_2982 on theBenchmark for (2982ds/39Mi)
% 15.11/3.34  % (2822423)Instruction limit reached! 
% 15.11/3.34  % (2822423)------------------------------
% 15.11/3.34  % (2822423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822423)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822423)Termination reason: Instruction limit
% 15.11/3.34  % (2822423)Termination phase: Saturation
% 15.11/3.34  % (2822423)Time elapsed: 0.080 s
% 15.11/3.34  % (2822423)Peak memory usage: 92 MB
% 15.11/3.34  % (2822423)Instructions burned: 129 (million)
% 15.11/3.34  % (2822405)Instruction limit reached! 
% 15.11/3.34  % (2822405)------------------------------
% 15.11/3.34  % (2822405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822405)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822405)Termination reason: Instruction limit
% 15.11/3.34  % (2822405)Termination phase: Saturation
% 15.11/3.34  % (2822405)Time elapsed: 0.410 s
% 15.11/3.34  % (2822405)Peak memory usage: 97 MB
% 15.11/3.34  % (2822405)Instructions burned: 383 (million)
% 15.11/3.34  % (2822427)Instruction limit reached! 
% 15.11/3.34  % (2822427)------------------------------
% 15.11/3.34  % (2822427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822427)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822427)Termination reason: Instruction limit
% 15.11/3.34  % (2822427)Termination phase: Clausification
% 15.11/3.34  % (2822427)Time elapsed: 0.092 s
% 15.11/3.34  % (2822427)Peak memory usage: 126 MB
% 15.11/3.34  % (2822427)Instructions burned: 176 (million)
% 15.11/3.34  % (2822425)Instruction limit reached! 
% 15.11/3.34  % (2822425)------------------------------
% 15.11/3.34  % (2822425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822425)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822425)Termination reason: Instruction limit
% 15.11/3.34  % (2822425)Termination phase: Preprocessing 3
% 15.11/3.34  % (2822425)Time elapsed: 0.039 s
% 15.11/3.34  % (2822425)Peak memory usage: 88 MB
% 15.11/3.34  % (2822425)Instructions burned: 39 (million)
% 15.11/3.34  % (2822440)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=121338265:thitd=on:i=215:nm=0:rtra=on:ev=force_2979 on theBenchmark for (2979ds/215Mi)
% 15.11/3.34  % (2822442)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=747615349:st=2:i=295:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/295Mi)
% 15.11/3.34  % (2822436)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4153614075:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/329Mi)
% 15.11/3.34  % (2822439)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1818056354:s2a=on:i=483:doe=on:nm=32:rtra=on_2979 on theBenchmark for (2979ds/483Mi)
% 15.11/3.34  % (2822441)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2000510547:i=349:rtra=on_2979 on theBenchmark for (2979ds/349Mi)
% 15.11/3.34  % (2822440)Instruction limit reached! 
% 15.11/3.34  % (2822440)------------------------------
% 15.11/3.34  % (2822440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.34  % (2822440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.34  % (2822440)CaDiCaL version: 2.1.3
% 15.11/3.34  % (2822440)Termination reason: Instruction limit
% 15.11/3.34  % (2822440)Termination phase: Clausification
% 15.11/3.34  % (2822440)Time elapsed: 0.139 s
% 15.11/3.34  % (2822440)Peak memory usage: 144 MB
% 15.11/3.34  % (2822440)Instructions burned: 216 (million)
% 15.11/3.34  % (2822396)Refutation found. Thanks to Tanya!
% 15.11/3.34  % SZS status Theorem for theBenchmark
% 15.11/3.34  % SZS output start Proof for theBenchmark
% See solution above
% 0.17/3.61  % (2822396)------------------------------
% 0.17/3.61  % (2822396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/3.61  % (2822396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/3.61  % (2822396)CaDiCaL version: 2.1.3
% 0.17/3.61  % (2822396)Termination reason: Refutation
% 0.17/3.61  % (2822396)Time elapsed: 0.382 s
% 0.17/3.61  % (2822396)Peak memory usage: 139 MB
% 0.17/3.61  % (2822396)Instructions burned: 324 (million)
% 0.17/3.61  % (2822396)------------------------------
% 0.17/3.61  % (2822396)------------------------------
% 0.17/3.61  % (2822224)Success in time 2.33 s
% 0.17/3.61  % Vampire exiting
%------------------------------------------------------------------------------