Vampire---5.0.1.THM-Ref.s

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

% Computer : n018.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:40 AM UTC 2026

% Result   : Theorem 29.96s 5.28s
% Output   : Refutation 30.86s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   14
%            Number of leaves      :   17
% Syntax   : Number of formulae    :   87 (  47 unt;   0 typ;   0 def)
%            Number of atoms       :  187 ( 144 equ)
%            Maximal formula atoms :    7 (   2 avg)
%            Number of connectives :  160 (  60   ~;  53   |;  26   &)
%                                         (   6 <=>;  15  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    8 (   3 avg)
%            Maximal term depth    :    6 (   2 avg)
%            Number of FOOLs       :    1 (   1 fml;   0 var)
%            Number arithmetic     :  304 (  42 atm;  19 fun; 195 num;  48 var)
%            Number of types       :   30 (  27 usr;   2 ari;   0 dat;   0 cdt)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :   35 (  31 usr;   1 prp; 0-3 aty)
%            Number of functors    :  131 ( 119 usr;  31 con; 0-3 aty)
%            Number of variables   :   83 (  83   !;   0   ?;  83   :)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

tff(func_def_0,type,
    'one$b': 'Int_fps$' ).

tff(func_def_1,type,
    'elt_set_times$': ( 'Real_fps$' * 'Real_fps_set$' ) > 'Real_fps_set$' ).

tff(func_def_2,type,
    'times$': 'Real_fps_real_fps_real_fps_fun_fun$' ).

tff(func_def_3,type,
    'divide$': ( 'Real_fps$' * 'Real_fps$' ) > 'Real_fps$' ).

tff(func_def_4,type,
    'elt_set_times$b': ( 'Nat$' * 'Nat_set$' ) > 'Nat_set$' ).

tff(func_def_5,type,
    'minus$': ( 'Real_fps$' * 'Real_fps$' ) > 'Real_fps$' ).

tff(func_def_6,type,
    'fun_app$p': ( 'Real_real_bool_fun_fun$' * $real ) > 'Real_bool_fun$' ).

tff(func_def_7,type,
    'monoid$b': 'Nat_nat_nat_fun_fun$' > 'Nat_bool_fun$' ).

tff(func_def_8,type,
    'fps_compose$': ( 'Real_fps$' * 'Real_fps$' ) > 'Real_fps$' ).

tff(func_def_9,type,
    'bernoulli_fps$a': 'Real_fps$' ).

tff(func_def_10,type,
    'fps_const$': $real > 'Real_fps$' ).

tff(func_def_11,type,
    'elt_set_times$a': ( $int * 'Int_set$' ) > 'Int_set$' ).

tff(func_def_12,type,
    'fun_app$a': ( 'Int_int_fun$' * $int ) > $int ).

tff(func_def_13,type,
    'bernoulli_fps$': 'Real_fps$' ).

tff(func_def_14,type,
    'times$g': ( 'Real_set$' * 'Real_set$' ) > 'Real_set$' ).

tff(func_def_15,type,
    'fps_nth_deriv$': ( 'Nat$' * 'Real_fps$' ) > 'Real_fps$' ).

tff(func_def_16,type,
    'fun_app$': ( 'Real_real_fun$' * $real ) > $real ).

tff(func_def_17,type,
    'fps_tan$': $real > 'Real_fps$' ).

tff(func_def_18,type,
    'less_eq$': 'Nat$' > 'Nat_bool_fun$' ).

tff(func_def_19,type,
    'comm_monoid$b': 'Nat_nat_nat_fun_fun$' > 'Nat_bool_fun$' ).

tff(func_def_20,type,
    'fps_const$a': 'Real_fps$' > 'Real_fps_fps$' ).

tff(func_def_21,type,
    'fun_app$b': ( 'Real_fps_real_fps_fun$' * 'Real_fps$' ) > 'Real_fps$' ).

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

tff(func_def_23,type,
    'fps_X$a': 'Int_fps$' ).

tff(func_def_24,type,
    'times$c': 'Int_int_int_fun_fun$' ).

tff(func_def_25,type,
    'fps_compose$a': ( 'Int_fps$' * 'Int_fps$' ) > 'Int_fps$' ).

tff(func_def_26,type,
    'fps_ln$': $real > 'Real_fps$' ).

tff(func_def_27,type,
    'fps_shift$': ( 'Nat$' * 'Real_fps$' ) > 'Real_fps$' ).

tff(func_def_28,type,
    'fun_app$e': ( 'Nat_nat_nat_fun_fun$' * 'Nat$' ) > 'Nat_nat_fun$' ).

tff(func_def_29,type,
    'fps_nth$c': ( 'Nat_fps$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_30,type,
    tltrue: tlbool ).

tff(func_def_31,type,
    'fps_exp$': $real > 'Real_fps$' ).

tff(func_def_32,type,
    'zero$b': 'Nat$' ).

tff(func_def_33,type,
    'minus$a': ( 'Int_fps$' * 'Int_fps$' ) > 'Int_fps$' ).

tff(func_def_34,type,
    'fun_app$g': ( 'Real_real_real_fun_fun$' * $real ) > 'Real_real_fun$' ).

tff(func_def_35,type,
    'uminus$': 'Real_fps$' > 'Real_fps$' ).

tff(func_def_36,type,
    'one$a': 'Nat$' ).

tff(func_def_37,type,
    'times$d': ( 'Int_set$' * 'Int_set$' ) > 'Int_set$' ).

tff(func_def_38,type,
    'times$e': ( 'Nat_set$' * 'Nat_set$' ) > 'Nat_set$' ).

tff(func_def_39,type,
    'fps_Lambert_W$': 'Real_fps$' ).

tff(func_def_40,type,
    'divide$c': ( 'Nat$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_41,type,
    'fun_app$d': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_42,type,
    'fun_app$c': ( 'Real_fps_real_fps_real_fps_fun_fun$' * 'Real_fps$' ) > 'Real_fps_real_fps_fun$' ).

tff(func_def_43,type,
    'fps_nth$b': ( 'Real_fps_fps$' * 'Nat$' ) > 'Real_fps$' ).

tff(func_def_44,type,
    'times$f': 'Real_real_real_fun_fun$' ).

tff(func_def_45,type,
    'times$a': 'Nat_nat_nat_fun_fun$' ).

tff(func_def_46,type,
    'times$b': ( 'Real_fps_set$' * 'Real_fps_set$' ) > 'Real_fps_set$' ).

tff(func_def_47,type,
    'elt_set_times$c': ( $real * 'Real_set$' ) > 'Real_set$' ).

tff(func_def_48,type,
    'one$c': 'Real_fps_fps$' ).

tff(func_def_49,type,
    'fun_app$n': ( 'Int_int_bool_fun_fun$' * $int ) > 'Int_bool_fun$' ).

tff(func_def_50,type,
    'times$h': ( 'Real_fps_fps$' * 'Real_fps_fps$' ) > 'Real_fps_fps$' ).

tff(func_def_51,type,
    'fun_app$i': ( 'Nat_real_fun$' * 'Nat$' ) > $real ).

tff(func_def_52,type,
    'fps_inv$': 'Real_fps_real_fps_fun$' ).

tff(func_def_53,type,
    'zero$a': 'Int_fps$' ).

tff(func_def_54,type,
    'fps_const$b': $int > 'Int_fps$' ).

tff(func_def_55,type,
    'divide$a': $real > 'Real_real_fun$' ).

tff(func_def_56,type,
    'fps_ginv$': 'Real_fps$' > 'Real_fps_real_fps_fun$' ).

tff(func_def_57,type,
    'times$j': ( 'Nat_fps$' * 'Nat_fps$' ) > 'Nat_fps$' ).

tff(func_def_58,type,
    'fps_nth$a': ( 'Int_fps$' * 'Nat$' ) > $int ).

tff(func_def_59,type,
    'fps_const$c': 'Nat$' > 'Nat_fps$' ).

tff(func_def_60,type,
    tlfalse: tlbool ).

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

tff(func_def_62,type,
    'fun_app$k': ( 'Nat_real_fun_nat_real_fun_fun$' * 'Nat_real_fun$' ) > 'Nat_real_fun$' ).

tff(func_def_63,type,
    'fps_nth$': 'Real_fps$' > 'Nat_real_fun$' ).

tff(func_def_64,type,
    'minus$b': ( 'Nat$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_65,type,
    'fun_app$l': ( 'Nat_real_fun_nat_nat_fun_fun$' * 'Nat_real_fun$' ) > 'Nat_nat_fun$' ).

tff(func_def_66,type,
    'fun_app$f': ( 'Int_int_int_fun_fun$' * $int ) > 'Int_int_fun$' ).

tff(func_def_67,type,
    'times$i': ( 'Int_fps$' * 'Int_fps$' ) > 'Int_fps$' ).

tff(func_def_68,type,
    'uua$': $int > 'Int_int_fun$' ).

tff(func_def_69,type,
    'divide$b': $int > 'Int_int_fun$' ).

tff(func_def_70,type,
    'one$': 'Real_fps$' ).

tff(func_def_71,type,
    'uu$': $real > 'Real_real_fun$' ).

tff(func_def_72,type,
    'fps_X$': 'Real_fps$' ).

tff(func_def_73,type,
    'zero$': 'Real_fps$' ).

tff(func_def_86,type,
    sK17: ( $int * 'Int_set$' * 'Int_set$' ) > $int ).

tff(func_def_87,type,
    sK18: ( $int * 'Int_set$' * 'Int_set$' ) > $int ).

tff(func_def_88,type,
    sK19: ( 'Real_fps$' * 'Real_fps_set$' * 'Real_fps_set$' ) > 'Real_fps$' ).

tff(func_def_89,type,
    sK20: ( 'Real_fps$' * 'Real_fps_set$' * 'Real_fps_set$' ) > 'Real_fps$' ).

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

tff(func_def_91,type,
    sK22: 'Nat_bool_fun$' > 'Nat$' ).

tff(func_def_92,type,
    sK23: 'Real_fps$' > $real ).

tff(func_def_93,type,
    sK24: 'Real_fps$' > 'Real_fps$' ).

tff(func_def_94,type,
    sK25: 'Int_fps$' > $int ).

tff(func_def_95,type,
    sK26: 'Int_fps$' > 'Int_fps$' ).

tff(func_def_96,type,
    sK27: 'Int_fps$' > $int ).

tff(func_def_97,type,
    sK28: 'Int_fps$' > 'Int_fps$' ).

tff(func_def_98,type,
    sK29: 'Real_fps_fps$' > 'Real_fps$' ).

tff(func_def_99,type,
    sK30: 'Real_fps_fps$' > 'Real_fps_fps$' ).

tff(func_def_100,type,
    sK31: 'Real_real_bool_fun_fun$' > $real ).

tff(func_def_101,type,
    sK32: 'Real_real_bool_fun_fun$' > $real ).

tff(func_def_102,type,
    sK33: 'Real_real_bool_fun_fun$' > $real ).

tff(func_def_103,type,
    sK34: 'Real_real_bool_fun_fun$' > $real ).

tff(func_def_104,type,
    sK35: 'Real_fps$' > 'Real_fps$' ).

tff(func_def_105,type,
    sK36: 'Real_fps_fps$' > 'Real_fps_fps$' ).

tff(func_def_106,type,
    sK37: 'Real_fps_fps$' > 'Real_fps$' ).

tff(func_def_107,type,
    sK38: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_108,type,
    sK39: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_109,type,
    sK40: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_110,type,
    sK41: 'Int_int_bool_fun_fun$' > $int ).

tff(func_def_111,type,
    sK42: 'Real_fps$' > 'Real_fps$' ).

tff(func_def_112,type,
    sK43: 'Real_fps$' > $real ).

tff(func_def_113,type,
    sK44: ( 'Nat_set$' * 'Nat_set$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_114,type,
    sK45: ( 'Nat_set$' * 'Nat_set$' * 'Nat$' ) > 'Nat$' ).

tff(func_def_115,type,
    sK46: 'Real_fps$' > 'Real_fps$' ).

tff(func_def_116,type,
    sK47: ( 'Real_set$' * $real * 'Real_set$' ) > $real ).

tff(func_def_117,type,
    sK48: ( 'Real_set$' * $real * 'Real_set$' ) > $real ).

tff(func_def_118,type,
    sK49: ( 'Nat_real_fun_bool_fun$' * 'Nat_bool_fun$' * 'Nat_real_fun_nat_real_fun_fun$' ) > 'Nat_real_fun_nat_nat_fun_fun$' ).

tff(func_def_119,type,
    sK50: ( 'Nat_real_fun_nat_real_fun_fun$' * 'Nat_real_fun_bool_fun$' ) > 'Nat_real_fun$' ).

tff(func_def_120,type,
    sK51: ( 'Nat_bool_fun$' * 'Nat_real_fun_bool_fun$' ) > 'Nat_real_fun$' ).

tff(func_def_121,type,
    sK52: ( 'Nat_bool_fun$' * 'Nat_real_fun_bool_fun$' ) > 'Nat$' ).

tff(func_def_122,type,
    sK53: 'Real_fps$' > 'Nat$' ).

tff(func_def_123,type,
    sK54: 'Int_fps$' > 'Nat$' ).

tff(func_def_124,type,
    -1: $int > $int ).

tff(func_def_125,type,
    2/1: $real > $real ).

tff(func_def_126,type,
    2: $int > $int ).

tff(func_def_129,type,
    -1/1: $real > $real ).

tff(func_def_130,type,
    '$inst55': $real ).

tff(func_def_133,type,
    '$inst56': $real ).

tff(func_def_134,type,
    '$inst57': $int ).

tff(func_def_135,type,
    '$inst58': $int ).

tff(func_def_137,type,
    '$inst59': $real ).

tff(func_def_138,type,
    '$inst60': $int ).

tff(func_def_140,type,
    '$inst61': $int ).

tff(pred_def_1,type,
    'member$c': ( $real * 'Real_set$' ) > $o ).

tff(pred_def_2,type,
    'monoid$c': ( 'Real_real_real_fun_fun$' * $real ) > $o ).

tff(pred_def_3,type,
    'fun_app$o': ( 'Real_bool_fun$' * $real ) > $o ).

tff(pred_def_4,type,
    'comm_monoid$': ( 'Real_fps_real_fps_real_fps_fun_fun$' * 'Real_fps$' ) > $o ).

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

tff(pred_def_6,type,
    'monoid$': ( 'Real_fps_real_fps_real_fps_fun_fun$' * 'Real_fps$' ) > $o ).

tff(pred_def_7,type,
    'monoid$a': ( 'Int_int_int_fun_fun$' * $int ) > $o ).

tff(pred_def_8,type,
    'member$b': ( 'Nat$' * 'Nat_set$' ) > $o ).

tff(pred_def_9,type,
    'member$': ( 'Real_fps$' * 'Real_fps_set$' ) > $o ).

tff(pred_def_10,type,
    'fun_app$h': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).

tff(pred_def_11,type,
    'comm_monoid$a': ( 'Int_int_int_fun_fun$' * $int ) > $o ).

tff(pred_def_12,type,
    'member$a': ( $int * 'Int_set$' ) > $o ).

tff(pred_def_13,type,
    'fun_app$j': ( 'Nat_real_fun_bool_fun$' * 'Nat_real_fun$' ) > $o ).

tff(pred_def_14,type,
    'comm_monoid$c': ( 'Real_real_real_fun_fun$' * $real ) > $o ).

tff(pred_def_19,type,
    sP0: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).

tff(pred_def_20,type,
    sP1: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).

tff(pred_def_21,type,
    sP2: ( 'Nat$' * 'Nat$' ) > $o ).

tff(pred_def_22,type,
    sP3: ( $int * $int * $int ) > $o ).

tff(pred_def_23,type,
    sP4: ( $int * $int * $int ) > $o ).

tff(pred_def_24,type,
    sP5: ( $int * $int * $int ) > $o ).

tff(pred_def_25,type,
    sP6: ( $real * $real * $real ) > $o ).

tff(pred_def_26,type,
    sP7: ( $real * $real * $real ) > $o ).

tff(pred_def_27,type,
    sP8: ( $real * $real * $real ) > $o ).

tff(pred_def_28,type,
    sP9: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).

tff(pred_def_29,type,
    sP10: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).

tff(pred_def_30,type,
    sP11: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).

tff(pred_def_31,type,
    sP12: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).

tff(pred_def_32,type,
    sP13: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).

tff(pred_def_33,type,
    sP14: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).

tff(pred_def_34,type,
    sP15: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).

tff(pred_def_35,type,
    sP16: ( 'Nat_real_fun_bool_fun$' * 'Nat_bool_fun$' * 'Nat_real_fun_nat_real_fun_fun$' ) > $o ).

tff(f3,conjecture,
    'fps_compose$'('fps_Lambert_W$','fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))) = 'fps_X$',
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture2) ).

tff(f4,negated_conjecture,
    ( ( ~ 'fps_compose$'('fps_Lambert_W$','fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))) ) = 'fps_X$' ),
    inference(negated_conjecture,[status(cth)],[f3]) ).

tff(f15,axiom,
    'fps_Lambert_W$' = 'fun_app$b'('fps_inv$','fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom13) ).

tff(f21,axiom,
    ! [X0: 'Real_fps$'] : ( 'fun_app$b'('fun_app$c'('times$','fps_X$'),X0) = 'fun_app$b'('fun_app$c'('times$',X0),'fps_X$') ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom19) ).

tff(f58,axiom,
    ! [X1: $real,X0: $real] : ( 'fps_compose$'('fps_exp$'(X0),'fun_app$b'('fun_app$c'('times$','fps_const$'(X1)),'fps_X$')) = 'fps_exp$'('fun_app$'('fun_app$g'('times$f',X1),X0)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom56) ).

tff(f109,axiom,
    ! [X0: $real] :
      ( ( X0 = 0/1 )
    <=> ( 'fps_exp$'(X0) = 'one$' ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom107) ).

tff(f148,axiom,
    ! [X1: $real,X0: $real] :
      ( ( ( X1 = 1/1 )
        | ( X0 = 0/1 ) )
    <=> ( 'fun_app$'('fun_app$g'('times$f',X0),X1) = X0 ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom146) ).

tff(f196,axiom,
    0/1 != 1/1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom194) ).

tff(f268,axiom,
    ! [X1: 'Real_fps$',X0: 'Real_fps$'] : ( 'fun_app$i'('fps_nth$'('fps_compose$'(X0,X1)),'nat$'(0)) = 'fun_app$i'('fps_nth$'(X0),'nat$'(0)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom266) ).

tff(f288,axiom,
    ! [X0: 'Nat$'] :
      ( ( ( 'of_nat$'(X0) != 0 )
       => ( 'fun_app$i'('fps_nth$'('one$'),X0) = 0/1 ) )
      & ( ( 'of_nat$'(X0) = 0 )
       => ( 'fun_app$i'('fps_nth$'('one$'),X0) = 1/1 ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom286) ).

tff(f296,axiom,
    ! [X0: 'Real_fps$',X1: 'Nat$'] :
      ( ( ( 'of_nat$'(X1) != 0 )
       => ( ( ~ $less('of_nat$'(X1),1)
           => ( 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) = 'fun_app$i'('fps_nth$'(X0),'nat$'($difference('of_nat$'(X1),1))) ) )
          & ( $less('of_nat$'(X1),1)
           => ( 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) = 'fun_app$i'('fps_nth$'(X0),'nat$'(0)) ) ) ) )
      & ( ( 'of_nat$'(X1) = 0 )
       => ( 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) = 0/1 ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom294) ).

tff(f381,axiom,
    $lesseq(0,1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom379) ).

tff(f420,axiom,
    ! [X0: 'Real_fps$'] :
      ( ( ( 'fun_app$i'('fps_nth$'(X0),'nat$'(0)) = 0/1 )
        & ( 'fun_app$i'('fps_nth$'(X0),'nat$'(1)) != 0/1 ) )
     => ( 'fps_compose$'('fun_app$b'('fps_inv$',X0),X0) = 'fps_X$' ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom418) ).

tff(f581,axiom,
    0 != $uminus(1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom579) ).

tff(f621,axiom,
    ! [X1: $int,X0: $int] :
      ( ( X0 = X1 )
    <=> ( $lesseq(X1,X0)
        & $lesseq(X0,X1) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom619) ).

tff(f643,axiom,
    ! [X0: 'Nat$'] : ( 'nat$'('of_nat$'(X0)) = X0 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom641) ).

tff(f644,axiom,
    ! [X0: $int] :
      ( ( $lesseq(0,X0)
       => ( 'of_nat$'('nat$'(X0)) = X0 ) )
      & ( ~ $lesseq(0,X0)
       => ( 'of_nat$'('nat$'(X0)) = 0 ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom642) ).

tff(f656,plain,
    ! [X1: $int,X0: $int] :
      ( ( X0 = X1 )
    <=> ( ~ $less(X0,X1)
        & ~ $less(X1,X0) ) ),
    inference(theory_normalization,[],[f621]) ).

tff(f657,plain,
    ! [X0: $int] :
      ( ( $less(X0,0)
       => ( 'of_nat$'('nat$'(X0)) = 0 ) )
      & ( ~ $less(X0,0)
       => ( 'of_nat$'('nat$'(X0)) = X0 ) ) ),
    inference(theory_normalization,[],[f644]) ).

tff(f751,plain,
    ~ $less(1,0),
    inference(theory_normalization,[],[f381]) ).

tff(f768,plain,
    ! [X0: 'Real_fps$',X1: 'Nat$'] :
      ( ( ( 'of_nat$'(X1) != 0 )
       => ( ( ~ $less('of_nat$'(X1),1)
           => ( 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) = 'fun_app$i'('fps_nth$'(X0),'nat$'($sum('of_nat$'(X1),$uminus(1)))) ) )
          & ( $less('of_nat$'(X1),1)
           => ( 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) = 'fun_app$i'('fps_nth$'(X0),'nat$'(0)) ) ) ) )
      & ( ( 'of_nat$'(X1) = 0 )
       => ( 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) = 0/1 ) ) ),
    inference(theory_normalization,[],[f296]) ).

tff(f889,plain,
    ! [X0: $int] : ( 0 = $sum(X0,$uminus(X0)) ),
    introduced(definition,[],[tha_inverse_op_unit]) ).

tff(f940,plain,
    ! [X1: $int,X0: $int] :
      ( ( ~ $less(X0,X1)
        & ~ $less(X1,X0) )
    <=> ( X0 = X1 ) ),
    inference(rectify,[],[f656]) ).

tff(f1031,plain,
    ! [X0: 'Real_fps$',X1: 'Real_fps$'] : ( 'fun_app$i'('fps_nth$'(X1),'nat$'(0)) = 'fun_app$i'('fps_nth$'('fps_compose$'(X1,X0)),'nat$'(0)) ),
    inference(rectify,[],[f268]) ).

tff(f1122,plain,
    'fps_X$' != 'fps_compose$'('fps_Lambert_W$','fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))),
    inference(flattening,[],[f4]) ).

tff(f1186,plain,
    ! [X0: $real,X1: $real] :
      ( ( 'fun_app$'('fun_app$g'('times$f',X1),X0) = X1 )
    <=> ( ( 0/1 = X1 )
        | ( 1/1 = X0 ) ) ),
    inference(rectify,[],[f148]) ).

tff(f1307,plain,
    ! [X0: 'Nat$'] :
      ( ( ( 0 = 'of_nat$'(X0) )
        | ( 'fun_app$i'('fps_nth$'('one$'),X0) = 0/1 ) )
      & ( ( 0 != 'of_nat$'(X0) )
        | ( 'fun_app$i'('fps_nth$'('one$'),X0) = 1/1 ) ) ),
    inference(ennf_transformation,[],[f288]) ).

tff(f1341,plain,
    ! [X0: $int] :
      ( ( $less(X0,0)
        | ( 'of_nat$'('nat$'(X0)) = X0 ) )
      & ( ~ $less(X0,0)
        | ( 'of_nat$'('nat$'(X0)) = 0 ) ) ),
    inference(ennf_transformation,[],[f657]) ).

tff(f1383,plain,
    ! [X0: 'Real_fps$',X1: 'Nat$'] :
      ( ( ( ( ~ $less('of_nat$'(X1),1)
            | ( 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) = 'fun_app$i'('fps_nth$'(X0),'nat$'(0)) ) )
          & ( ( 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) = 'fun_app$i'('fps_nth$'(X0),'nat$'($sum('of_nat$'(X1),$uminus(1)))) )
            | $less('of_nat$'(X1),1) ) )
        | ( 0 = 'of_nat$'(X1) ) )
      & ( ( 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) = 0/1 )
        | ( 0 != 'of_nat$'(X1) ) ) ),
    inference(ennf_transformation,[],[f768]) ).

tff(f1592,plain,
    ! [X0: 'Real_fps$'] :
      ( ( 'fps_compose$'('fun_app$b'('fps_inv$',X0),X0) = 'fps_X$' )
      | ( 0/1 != 'fun_app$i'('fps_nth$'(X0),'nat$'(0)) )
      | ( 0/1 = 'fun_app$i'('fps_nth$'(X0),'nat$'(1)) ) ),
    inference(ennf_transformation,[],[f420]) ).

tff(f1593,plain,
    ! [X0: 'Real_fps$'] :
      ( ( 'fps_compose$'('fun_app$b'('fps_inv$',X0),X0) = 'fps_X$' )
      | ( 0/1 = 'fun_app$i'('fps_nth$'(X0),'nat$'(1)) )
      | ( 0/1 != 'fun_app$i'('fps_nth$'(X0),'nat$'(0)) ) ),
    inference(flattening,[],[f1592]) ).

tff(f1777,plain,
    ! [X0: $real,X1: $real] :
      ( ( ( 'fun_app$'('fun_app$g'('times$f',X1),X0) = X1 )
        | ( ( 0/1 != X1 )
          & ( 1/1 != X0 ) ) )
      & ( ( 0/1 = X1 )
        | ( 1/1 = X0 )
        | ( 'fun_app$'('fun_app$g'('times$f',X1),X0) != X1 ) ) ),
    inference(nnf_transformation,[],[f1186]) ).

tff(f1778,plain,
    ! [X0: $real,X1: $real] :
      ( ( ( 'fun_app$'('fun_app$g'('times$f',X1),X0) = X1 )
        | ( ( 0/1 != X1 )
          & ( 1/1 != X0 ) ) )
      & ( ( 0/1 = X1 )
        | ( 1/1 = X0 )
        | ( 'fun_app$'('fun_app$g'('times$f',X1),X0) != X1 ) ) ),
    inference(flattening,[],[f1777]) ).

tff(f1903,plain,
    ! [X1: $int,X0: $int] :
      ( ( ( ~ $less(X0,X1)
          & ~ $less(X1,X0) )
        | ( X0 != X1 ) )
      & ( ( X0 = X1 )
        | $less(X0,X1)
        | $less(X1,X0) ) ),
    inference(nnf_transformation,[],[f940]) ).

tff(f1904,plain,
    ! [X1: $int,X0: $int] :
      ( ( ( ~ $less(X0,X1)
          & ~ $less(X1,X0) )
        | ( X0 != X1 ) )
      & ( ( X0 = X1 )
        | $less(X0,X1)
        | $less(X1,X0) ) ),
    inference(flattening,[],[f1903]) ).

tff(f1905,plain,
    ! [X0: $int,X1: $int] :
      ( ( ( ~ $less(X1,X0)
          & ~ $less(X0,X1) )
        | ( X0 != X1 ) )
      & ( ( X0 = X1 )
        | $less(X1,X0)
        | $less(X0,X1) ) ),
    inference(rectify,[],[f1904]) ).

tff(f1943,plain,
    ! [X0: $real] :
      ( ( ( X0 = 0/1 )
        | ( 'one$' != 'fps_exp$'(X0) ) )
      & ( ( 'fps_exp$'(X0) = 'one$' )
        | ( 0/1 != X0 ) ) ),
    inference(nnf_transformation,[],[f109]) ).

tff(f2168,plain,
    ! [X0: $real,X1: $real] : ( 'fps_compose$'('fps_exp$'(X1),'fun_app$b'('fun_app$c'('times$','fps_const$'(X0)),'fps_X$')) = 'fps_exp$'('fun_app$'('fun_app$g'('times$f',X0),X1)) ),
    inference(rectify,[],[f58]) ).

tff(f2336,plain,
    'fps_X$' != 'fps_compose$'('fps_Lambert_W$','fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))),
    inference(cnf_transformation,[],[f1122]) ).

tff(f2455,plain,
    0 != $uminus(1),
    inference(cnf_transformation,[],[f581]) ).

tff(f2469,plain,
    ! [X0: 'Real_fps$'] :
      ( ( 'fps_X$' = 'fps_compose$'('fun_app$b'('fps_inv$',X0),X0) )
      | ( 0/1 != 'fun_app$i'('fps_nth$'(X0),'nat$'(0)) )
      | ( 0/1 = 'fun_app$i'('fps_nth$'(X0),'nat$'(1)) ) ),
    inference(cnf_transformation,[],[f1593]) ).

tff(f2477,plain,
    ! [X0: $real,X1: $real] :
      ( ( 'fun_app$'('fun_app$g'('times$f',X1),X0) = X1 )
      | ( 0/1 != X1 ) ),
    inference(cnf_transformation,[],[f1778]) ).

tff(f2500,plain,
    ! [X0: 'Real_fps$',X1: 'Nat$'] :
      ( ( 0 != 'of_nat$'(X1) )
      | ( 0/1 = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) ) ),
    inference(cnf_transformation,[],[f1383]) ).

tff(f2501,plain,
    ! [X0: 'Real_fps$',X1: 'Nat$'] :
      ( $less('of_nat$'(X1),1)
      | ( 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),X1) = 'fun_app$i'('fps_nth$'(X0),'nat$'($sum('of_nat$'(X1),$uminus(1)))) )
      | ( 0 = 'of_nat$'(X1) ) ),
    inference(cnf_transformation,[],[f1383]) ).

tff(f2699,plain,
    ! [X0: $int,X1: $int] :
      ( ~ $less(X0,X1)
      | ( X0 != X1 ) ),
    inference(cnf_transformation,[],[f1905]) ).

tff(f2767,plain,
    ! [X0: $real] :
      ( ( 'one$' = 'fps_exp$'(X0) )
      | ( 0/1 != X0 ) ),
    inference(cnf_transformation,[],[f1943]) ).

tff(f2797,plain,
    ! [X0: 'Nat$'] :
      ( ( 0 != 'of_nat$'(X0) )
      | ( 1/1 = 'fun_app$i'('fps_nth$'('one$'),X0) ) ),
    inference(cnf_transformation,[],[f1307]) ).

tff(f2855,plain,
    ~ $less(1,0),
    inference(cnf_transformation,[],[f751]) ).

tff(f2924,plain,
    ! [X0: 'Real_fps$'] : ( 'fun_app$b'('fun_app$c'('times$','fps_X$'),X0) = 'fun_app$b'('fun_app$c'('times$',X0),'fps_X$') ),
    inference(cnf_transformation,[],[f21]) ).

tff(f2993,plain,
    ! [X0: 'Nat$'] : ( 'nat$'('of_nat$'(X0)) = X0 ),
    inference(cnf_transformation,[],[f643]) ).

tff(f3068,plain,
    ! [X0: 'Real_fps$',X1: 'Real_fps$'] : ( 'fun_app$i'('fps_nth$'(X1),'nat$'(0)) = 'fun_app$i'('fps_nth$'('fps_compose$'(X1,X0)),'nat$'(0)) ),
    inference(cnf_transformation,[],[f1031]) ).

tff(f3109,plain,
    ! [X0: $int] :
      ( ~ $less(X0,0)
      | ( 0 = 'of_nat$'('nat$'(X0)) ) ),
    inference(cnf_transformation,[],[f1341]) ).

tff(f3110,plain,
    ! [X0: $int] :
      ( $less(X0,0)
      | ( 'of_nat$'('nat$'(X0)) = X0 ) ),
    inference(cnf_transformation,[],[f1341]) ).

tff(f3153,plain,
    1/1 != 0/1,
    inference(cnf_transformation,[],[f196]) ).

tff(f3249,plain,
    'fps_Lambert_W$' = 'fun_app$b'('fps_inv$','fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))),
    inference(cnf_transformation,[],[f15]) ).

tff(f3270,plain,
    ! [X0: $real,X1: $real] : ( 'fps_compose$'('fps_exp$'(X1),'fun_app$b'('fun_app$c'('times$','fps_const$'(X0)),'fps_X$')) = 'fps_exp$'('fun_app$'('fun_app$g'('times$f',X0),X1)) ),
    inference(cnf_transformation,[],[f2168]) ).

tff(f3411,plain,
    ! [X0: $real] : ( 0/1 = 'fun_app$'('fun_app$g'('times$f',0/1),X0) ),
    inference(equality_resolution,[],[f2477]) ).

tff(f3475,plain,
    ! [X1: $int] : ~ $less(X1,X1),
    inference(equality_resolution,[],[f2699]) ).

tff(f3490,plain,
    'one$' = 'fps_exp$'(0/1),
    inference(equality_resolution,[],[f2767]) ).

tff(f3627,plain,
    ~ $less(0,0),
    inference(cancellation,[],[f3475]) ).

tff(f3774,plain,
    1 != 0,
    inference(cancellation,[],[f2455]) ).

tff(f3856,plain,
    ! [X0: $real,X1: $real] : ( 'fps_exp$'('fun_app$'('fun_app$g'('times$f',X0),X1)) = 'fps_compose$'('fps_exp$'(X1),'fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_const$'(X0))) ),
    inference(backward_demodulation,[],[f3270,f2924]) ).

tff(f4188,plain,
    ! [X0: $real,X1: $real] : ( 'fun_app$i'('fps_nth$'('fps_exp$'('fun_app$'('fun_app$g'('times$f',X0),X1))),'nat$'(0)) = 'fun_app$i'('fps_nth$'('fps_exp$'(X1)),'nat$'(0)) ),
    inference(constrained_superposition,[],[f3068,f3856]) ).

tff(f4440,plain,
    ( ~ $less(-1,0)
    | ( 0 = 'of_nat$'('nat$'(-1)) ) ),
    inference(instantiation,[],[f3109]) ).

tff(f4441,plain,
    0 = 'of_nat$'('nat$'(-1)),
    inference(interpreted_simplification,[],[f4440]) ).

tff(f4449,plain,
    1 = 'of_nat$'('nat$'(1)),
    inference(resolution,[],[f3110,f2855]) ).

tff(f5163,plain,
    ! [X0: 'Real_fps$'] :
      ( ( 0/1 = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),'nat$'(-1)) )
      | ( 0 != 0 ) ),
    inference(constrained_superposition,[],[f2500,f4441]) ).

tff(f5170,plain,
    ( ( 0 != 0 )
    | ( 1/1 = 'fun_app$i'('fps_nth$'('one$'),'nat$'(-1)) ) ),
    inference(constrained_superposition,[],[f2797,f4441]) ).

tff(f5173,plain,
    'nat$'(0) = 'nat$'(-1),
    inference(constrained_superposition,[],[f2993,f4441]) ).

tff(f5184,plain,
    1/1 = 'fun_app$i'('fps_nth$'('one$'),'nat$'(-1)),
    inference(trivial_inequality_removal,[],[f5170]) ).

tff(f5185,plain,
    ! [X0: 'Real_fps$'] : ( 0/1 = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),'nat$'(-1)) ),
    inference(trivial_inequality_removal,[],[f5163]) ).

tff(f5192,plain,
    1/1 = 'fun_app$i'('fps_nth$'('one$'),'nat$'(0)),
    inference(backward_demodulation,[],[f5184,f5173]) ).

tff(f5195,plain,
    ! [X0: 'Real_fps$'] : ( 0/1 = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),'nat$'(0)) ),
    inference(forward_demodulation,[],[f5185,f5173]) ).

tff(f5618,plain,
    ! [X0: 'Real_fps$'] :
      ( ( 1 = 0 )
      | $less(1,1)
      | ( 'fun_app$i'('fps_nth$'(X0),'nat$'($sum(1,$uminus(1)))) = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),'nat$'(1)) ) ),
    inference(constrained_superposition,[],[f2501,f4449]) ).

tff(f5649,plain,
    ! [X0: 'Real_fps$'] :
      ( ( 'fun_app$i'('fps_nth$'(X0),'nat$'($sum(1,$uminus(1)))) = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),'nat$'(1)) )
      | $less(0,0)
      | ( 1 = 0 ) ),
    inference(cancellation,[],[f5618]) ).

tff(f5656,plain,
    ! [X0: 'Real_fps$'] :
      ( ( 1 = 0 )
      | ( 'fun_app$i'('fps_nth$'(X0),'nat$'($sum(1,$uminus(1)))) = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),'nat$'(1)) ) ),
    inference(forward_subsumption_resolution,[],[f5649,f3627]) ).

tff(f5661,plain,
    ! [X0: 'Real_fps$'] : ( 'fun_app$i'('fps_nth$'(X0),'nat$'($sum(1,$uminus(1)))) = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),'nat$'(1)) ),
    inference(forward_subsumption_resolution,[],[f5656,f3774]) ).

tff(f5663,plain,
    ! [X0: 'Real_fps$'] : ( 'fun_app$i'('fps_nth$'(X0),'nat$'(0)) = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),X0)),'nat$'(1)) ),
    inference(forward_demodulation,[],[f5661,f889]) ).

tff(f6449,plain,
    ! [X0: $real] : ( 'fun_app$i'('fps_nth$'('fps_exp$'(0/1)),'nat$'(0)) = 'fun_app$i'('fps_nth$'('fps_exp$'(X0)),'nat$'(0)) ),
    inference(constrained_superposition,[],[f4188,f3411]) ).

tff(f6472,plain,
    ! [X0: $real] : ( 'fun_app$i'('fps_nth$'('one$'),'nat$'(0)) = 'fun_app$i'('fps_nth$'('fps_exp$'(X0)),'nat$'(0)) ),
    inference(forward_demodulation,[],[f6449,f3490]) ).

tff(f6476,plain,
    ! [X0: $real] : ( 1/1 = 'fun_app$i'('fps_nth$'('fps_exp$'(X0)),'nat$'(0)) ),
    inference(forward_demodulation,[],[f6472,f5192]) ).

tff(f8451,plain,
    ( ( 'fps_X$' = 'fps_compose$'('fps_Lambert_W$','fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))) )
    | ( 0/1 != 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))),'nat$'(0)) )
    | ( 0/1 = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))),'nat$'(1)) ) ),
    inference(constrained_superposition,[],[f2469,f3249]) ).

tff(f8458,plain,
    ( ( 0/1 != 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))),'nat$'(0)) )
    | ( 0/1 = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))),'nat$'(1)) ) ),
    inference(forward_subsumption_resolution,[],[f8451,f2336]) ).

tff(f8461,plain,
    0/1 = 'fun_app$i'('fps_nth$'('fun_app$b'('fun_app$c'('times$','fps_X$'),'fps_exp$'(1/1))),'nat$'(1)),
    inference(forward_subsumption_resolution,[],[f8458,f5195]) ).

tff(f8464,plain,
    0/1 = 'fun_app$i'('fps_nth$'('fps_exp$'(1/1)),'nat$'(0)),
    inference(forward_demodulation,[],[f8461,f5663]) ).

tff(f8467,plain,
    1/1 = 0/1,
    inference(forward_demodulation,[],[f8464,f6476]) ).

tff(f8468,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f8467,f3153]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP351_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38  % Computer : n018.cluster.edu
% 0.11/0.38  % Model    : x86_64 x86_64
% 0.11/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38  % Memory   : 8046.5625MB
% 0.11/0.38  % OS       : Linux 6.8.0-71-generic
% 0.11/0.38  % CPULimit : 300
% 0.11/0.38  % WCLimit  : 300
% 0.11/0.38  % DateTime : Sun Sep 27 12:57:38 UTC 2026
% 0.11/0.38  % CPUTime  : 
% 0.11/0.38  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.44  Running first-order theorem proving
% 0.11/0.44  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.45/1.56  % (2326329)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.45/1.56  % (2326378)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=445894928:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.45/1.56  % (2326383)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2633286649:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.45/1.56  % (2326381)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3599255227:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.45/1.56  % (2326383)Instruction limit reached! 
% 3.45/1.56  % (2326383)------------------------------
% 3.45/1.56  % (2326383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.45/1.56  % (2326383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.45/1.56  % (2326383)CaDiCaL version: 2.1.3
% 3.45/1.56  % (2326383)Termination reason: Instruction limit
% 3.45/1.56  % (2326383)Termination phase: Property scanning
% 3.45/1.56  % (2326383)Time elapsed: 0.008 s
% 3.45/1.56  % (2326383)Peak memory usage: 86 MB
% 3.45/1.56  % (2326383)Instructions burned: 7 (million)
% 3.45/1.56  % (2326378)Instruction limit reached! 
% 3.45/1.56  % (2326378)------------------------------
% 3.45/1.56  % (2326378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.45/1.56  % (2326378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.45/1.56  % (2326378)CaDiCaL version: 2.1.3
% 3.45/1.56  % (2326378)Termination reason: Instruction limit
% 3.45/1.56  % (2326378)Termination phase: shuffling
% 3.45/1.56  % (2326378)Time elapsed: 0.011 s
% 3.45/1.56  % (2326378)Peak memory usage: 85 MB
% 3.45/1.56  % (2326378)Instructions burned: 12 (million)
% 3.45/1.56  % (2326385)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1040828669:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.45/1.56  % (2326379)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3596843962:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.45/1.56  % (2326384)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3420922886:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.45/1.56  % (2326384)Instruction limit reached! 
% 3.45/1.56  % (2326384)------------------------------
% 3.45/1.56  % (2326384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.45/1.56  % (2326384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.45/1.56  % (2326384)CaDiCaL version: 2.1.3
% 3.45/1.56  % (2326384)Termination reason: Instruction limit
% 3.45/1.56  % (2326384)Termination phase: Property scanning
% 3.45/1.56  % (2326384)Time elapsed: 0.003 s
% 3.45/1.56  % (2326384)Peak memory usage: 86 MB
% 3.45/1.56  % (2326384)Instructions burned: 8 (million)
% 3.45/1.56  % (2326385)Instruction limit reached! 
% 3.45/1.56  % (2326385)------------------------------
% 3.45/1.56  % (2326385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.45/1.56  % (2326385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.45/1.56  % (2326385)CaDiCaL version: 2.1.3
% 3.45/1.56  % (2326385)Termination reason: Instruction limit
% 3.45/1.56  % (2326385)Termination phase: Equality resolution with deletion
% 3.45/1.56  % (2326385)Time elapsed: 0.030 s
% 3.45/1.56  % (2326385)Peak memory usage: 88 MB
% 3.45/1.56  % (2326385)Instructions burned: 46 (million)
% 3.45/1.56  % (2326387)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2456912952:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.45/1.56  % (2326387)Instruction limit reached! 
% 3.45/1.56  % (2326387)------------------------------
% 3.45/1.56  % (2326387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.45/1.56  % (2326387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.45/1.56  % (2326387)CaDiCaL version: 2.1.3
% 3.45/1.56  % (2326387)Termination reason: Instruction limit
% 3.45/1.56  % (2326387)Termination phase: Preprocessing 3
% 3.45/1.56  % (2326387)Time elapsed: 0.018 s
% 3.45/1.56  % (2326387)Peak memory usage: 87 MB
% 3.45/1.56  % (2326387)Instructions burned: 33 (million)
% 3.45/1.56  % (2326381)Instruction limit reached! 
% 3.45/1.56  % (2326381)------------------------------
% 3.45/1.56  % (2326381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.45/1.56  % (2326381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.71  % (2326381)CaDiCaL version: 2.1.3
% 4.58/1.71  % (2326381)Termination reason: Instruction limit
% 4.58/1.71  % (2326381)Termination phase: Saturation
% 4.58/1.71  % (2326381)Time elapsed: 0.134 s
% 4.58/1.71  % (2326381)Peak memory usage: 119 MB
% 4.58/1.71  % (2326381)Instructions burned: 203 (million)
% 4.58/1.71  % (2326397)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1723538694:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 4.58/1.71  % (2326397)Instruction limit reached! 
% 4.58/1.71  % (2326397)------------------------------
% 4.58/1.71  % (2326397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.71  % (2326398)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=1158712812:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 4.58/1.71  % (2326397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.71  % (2326397)CaDiCaL version: 2.1.3
% 4.58/1.71  % (2326397)Termination reason: Instruction limit
% 4.58/1.71  % (2326397)Termination phase: SInE selection
% 4.58/1.71  % (2326397)Time elapsed: 0.008 s
% 4.58/1.71  % (2326397)Peak memory usage: 86 MB
% 4.58/1.71  % (2326397)Instructions burned: 14 (million)
% 4.58/1.71  % (2326398)Instruction limit reached! 
% 4.58/1.71  % (2326398)------------------------------
% 4.58/1.71  % (2326398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.71  % (2326398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.71  % (2326398)CaDiCaL version: 2.1.3
% 4.58/1.71  % (2326398)Termination reason: Instruction limit
% 4.58/1.71  % (2326398)Termination phase: shuffling
% 4.58/1.71  % (2326398)Time elapsed: 0.016 s
% 4.58/1.71  % (2326398)Peak memory usage: 87 MB
% 4.58/1.71  % (2326398)Instructions burned: 29 (million)
% 4.58/1.71  % (2326404)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=936120244:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.58/1.71  % (2326404)Instruction limit reached! 
% 4.58/1.71  % (2326404)------------------------------
% 4.58/1.71  % (2326404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.71  % (2326404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.71  % (2326404)CaDiCaL version: 2.1.3
% 4.58/1.71  % (2326404)Termination reason: Instruction limit
% 4.58/1.71  % (2326404)Termination phase: Preprocessing 1
% 4.58/1.71  % (2326404)Time elapsed: 0.009 s
% 4.58/1.71  % (2326404)Peak memory usage: 86 MB
% 4.58/1.71  % (2326404)Instructions burned: 17 (million)
% 4.58/1.71  % (2326406)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4255450908:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.58/1.71  % (2326406)Instruction limit reached! 
% 4.58/1.71  % (2326406)------------------------------
% 4.58/1.71  % (2326406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.71  % (2326406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.71  % (2326406)CaDiCaL version: 2.1.3
% 4.58/1.71  % (2326406)Termination reason: Instruction limit
% 4.58/1.71  % (2326406)Termination phase: Preprocessing 1
% 4.58/1.71  % (2326406)Time elapsed: 0.013 s
% 4.58/1.71  % (2326406)Peak memory usage: 86 MB
% 4.58/1.71  % (2326406)Instructions burned: 25 (million)
% 4.58/1.71  % (2326407)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=3411792140:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.58/1.71  % (2326409)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2233574527:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 4.58/1.71  % (2326407)Instruction limit reached! 
% 4.58/1.71  % (2326407)------------------------------
% 4.58/1.71  % (2326407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.71  % (2326407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.71  % (2326407)CaDiCaL version: 2.1.3
% 4.58/1.71  % (2326407)Termination reason: Instruction limit
% 4.58/1.71  % (2326407)Termination phase: shuffling
% 4.58/1.71  % (2326407)Time elapsed: 0.015 s
% 4.58/1.71  % (2326407)Peak memory usage: 86 MB
% 4.58/1.71  % (2326407)Instructions burned: 27 (million)
% 4.58/1.71  % (2326379)Instruction limit reached! 
% 4.58/1.71  % (2326379)------------------------------
% 5.47/1.82  % (2326379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.82  % (2326379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.82  % (2326379)CaDiCaL version: 2.1.3
% 5.47/1.82  % (2326379)Termination reason: Instruction limit
% 5.47/1.82  % (2326379)Termination phase: Saturation
% 5.47/1.82  % (2326379)Time elapsed: 0.217 s
% 5.47/1.82  % (2326379)Peak memory usage: 119 MB
% 5.47/1.82  % (2326379)Instructions burned: 308 (million)
% 5.47/1.82  % (2326409)Instruction limit reached! 
% 5.47/1.82  % (2326409)------------------------------
% 5.47/1.82  % (2326409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.82  % (2326409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.82  % (2326409)CaDiCaL version: 2.1.3
% 5.47/1.82  % (2326409)Termination reason: Instruction limit
% 5.47/1.82  % (2326409)Termination phase: Property scanning
% 5.47/1.82  % (2326409)Time elapsed: 0.024 s
% 5.47/1.82  % (2326409)Peak memory usage: 88 MB
% 5.47/1.82  % (2326409)Instructions burned: 89 (million)
% 5.47/1.82  % (2326411)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3912057469:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.47/1.82  % (2326411)Instruction limit reached! 
% 5.47/1.82  % (2326411)------------------------------
% 5.47/1.82  % (2326411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.82  % (2326411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.82  % (2326411)CaDiCaL version: 2.1.3
% 5.47/1.82  % (2326411)Termination reason: Instruction limit
% 5.47/1.82  % (2326411)Termination phase: shuffling
% 5.47/1.82  % (2326411)Time elapsed: 0.002 s
% 5.47/1.82  % (2326411)Peak memory usage: 85 MB
% 5.47/1.82  % (2326411)Instructions burned: 2 (million)
% 5.47/1.82  % (2326413)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2592033777:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.47/1.82  % (2326414)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1049419925:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.47/1.82  % (2326414)Instruction limit reached! 
% 5.47/1.82  % (2326414)------------------------------
% 5.47/1.82  % (2326414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.82  % (2326414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.82  % (2326414)CaDiCaL version: 2.1.3
% 5.47/1.82  % (2326414)Termination reason: Instruction limit
% 5.47/1.82  % (2326414)Termination phase: Property scanning
% 5.47/1.82  % (2326414)Time elapsed: 0.006 s
% 5.47/1.82  % (2326414)Peak memory usage: 86 MB
% 5.47/1.82  % (2326414)Instructions burned: 5 (million)
% 5.47/1.82  % (2326417)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1607446450:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 5.47/1.82  % (2326420)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=4028501869:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 5.47/1.82  % (2326420)Instruction limit reached! 
% 5.47/1.82  % (2326420)------------------------------
% 5.47/1.82  % (2326420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.82  % (2326420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.82  % (2326420)CaDiCaL version: 2.1.3
% 5.47/1.82  % (2326420)Termination reason: Instruction limit
% 5.47/1.82  % (2326420)Termination phase: shuffling
% 5.47/1.82  % (2326420)Time elapsed: 0.003 s
% 5.47/1.82  % (2326420)Peak memory usage: 86 MB
% 5.47/1.82  % (2326420)Instructions burned: 11 (million)
% 5.47/1.82  % (2326419)lrs+10_1_thi=all:si=on:fd=off:random_seed=3184661623:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 5.47/1.82  % (2326417)Instruction limit reached! 
% 5.47/1.82  % (2326417)------------------------------
% 5.47/1.82  % (2326417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.82  % (2326417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.82  % (2326417)CaDiCaL version: 2.1.3
% 5.47/1.82  % (2326417)Termination reason: Instruction limit
% 5.47/1.82  % (2326417)Termination phase: Property scanning
% 5.47/1.82  % (2326417)Time elapsed: 0.035 s
% 5.47/1.82  % (2326417)Peak memory usage: 88 MB
% 5.47/1.82  % (2326417)Instructions burned: 68 (million)
% 5.88/1.98  % (2326421)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2673594654:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.88/1.98  % (2326421)Instruction limit reached! 
% 5.88/1.98  % (2326421)------------------------------
% 5.88/1.98  % (2326421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.98  % (2326421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.98  % (2326421)CaDiCaL version: 2.1.3
% 5.88/1.98  % (2326421)Termination reason: Instruction limit
% 5.88/1.98  % (2326421)Termination phase: Property scanning
% 5.88/1.98  % (2326421)Time elapsed: 0.004 s
% 5.88/1.98  % (2326421)Peak memory usage: 86 MB
% 5.88/1.98  % (2326421)Instructions burned: 4 (million)
% 5.88/1.98  % (2326419)Instruction limit reached! 
% 5.88/1.98  % (2326419)------------------------------
% 5.88/1.98  % (2326419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.98  % (2326419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.98  % (2326419)CaDiCaL version: 2.1.3
% 5.88/1.98  % (2326419)Termination reason: Instruction limit
% 5.88/1.98  % (2326419)Termination phase: Preprocessing 3
% 5.88/1.98  % (2326419)Time elapsed: 0.027 s
% 5.88/1.98  % (2326419)Peak memory usage: 87 MB
% 5.88/1.98  % (2326419)Instructions burned: 54 (million)
% 5.88/1.98  % (2326423)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3458345829:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 5.88/1.98  % (2326423)Instruction limit reached! 
% 5.88/1.98  % (2326423)------------------------------
% 5.88/1.98  % (2326423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.98  % (2326423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.98  % (2326423)CaDiCaL version: 2.1.3
% 5.88/1.98  % (2326423)Termination reason: Instruction limit
% 5.88/1.98  % (2326423)Termination phase: shuffling
% 5.88/1.98  % (2326423)Time elapsed: 0.003 s
% 5.88/1.98  % (2326423)Peak memory usage: 85 MB
% 5.88/1.98  % (2326423)Instructions burned: 3 (million)
% 5.88/1.98  % (2326413)Instruction limit reached! 
% 5.88/1.98  % (2326413)------------------------------
% 5.88/1.98  % (2326413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.98  % (2326413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.98  % (2326413)CaDiCaL version: 2.1.3
% 5.88/1.98  % (2326413)Termination reason: Instruction limit
% 5.88/1.98  % (2326413)Termination phase: Saturation
% 5.88/1.98  % (2326413)Time elapsed: 0.125 s
% 5.88/1.98  % (2326413)Peak memory usage: 92 MB
% 5.88/1.98  % (2326413)Instructions burned: 183 (million)
% 5.88/1.98  % (2326430)dis+10_1_si=on:random_seed=924783198:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 5.88/1.98  % (2326427)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3561067934:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 5.88/1.98  % (2326430)Instruction limit reached! 
% 5.88/1.98  % (2326430)------------------------------
% 5.88/1.98  % (2326430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.98  % (2326430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.98  % (2326430)CaDiCaL version: 2.1.3
% 5.88/1.98  % (2326430)Termination reason: Instruction limit
% 5.88/1.98  % (2326430)Termination phase: Property scanning
% 5.88/1.98  % (2326430)Time elapsed: 0.003 s
% 5.88/1.98  % (2326430)Peak memory usage: 86 MB
% 5.88/1.98  % (2326430)Instructions burned: 10 (million)
% 5.88/1.98  % (2326432)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=500903718:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 5.88/1.98  % (2326435)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=192606880: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_2994 on theBenchmark for (2994ds/35Mi)
% 5.88/1.98  % (2326437)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2177263527:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 5.88/1.98  % (2326440)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1924130520:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 5.88/1.98  % (2326432)Instruction limit reached! 
% 5.88/1.98  % (2326432)------------------------------
% 8.32/2.18  % (2326432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/2.18  % (2326432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/2.18  % (2326432)CaDiCaL version: 2.1.3
% 8.32/2.18  % (2326432)Termination reason: Instruction limit
% 8.32/2.18  % (2326432)Termination phase: Preprocessing 1
% 8.32/2.18  % (2326432)Time elapsed: 0.014 s
% 8.32/2.18  % (2326432)Peak memory usage: 86 MB
% 8.32/2.18  % (2326432)Instructions burned: 26 (million)
% 8.32/2.18  % (2326457)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=4268719902:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 8.32/2.18  % (2326437)Instruction limit reached! 
% 8.32/2.18  % (2326437)------------------------------
% 8.32/2.18  % (2326437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/2.18  % (2326437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/2.18  % (2326437)CaDiCaL version: 2.1.3
% 8.32/2.18  % (2326437)Termination reason: Instruction limit
% 8.32/2.18  % (2326437)Termination phase: shuffling
% 8.32/2.18  % (2326437)Time elapsed: 0.003 s
% 8.32/2.18  % (2326437)Peak memory usage: 85 MB
% 8.32/2.18  % (2326437)Instructions burned: 4 (million)
% 8.32/2.18  % (2326440)Instruction limit reached! 
% 8.32/2.18  % (2326440)------------------------------
% 8.32/2.18  % (2326440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/2.18  % (2326440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/2.18  % (2326440)CaDiCaL version: 2.1.3
% 8.32/2.18  % (2326440)Termination reason: Instruction limit
% 8.32/2.18  % (2326440)Termination phase: Property scanning
% 8.32/2.18  % (2326440)Time elapsed: 0.005 s
% 8.32/2.18  % (2326440)Peak memory usage: 85 MB
% 8.32/2.18  % (2326440)Instructions burned: 9 (million)
% 8.32/2.18  % (2326457)Instruction limit reached! 
% 8.32/2.18  % (2326457)------------------------------
% 8.32/2.18  % (2326457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/2.18  % (2326457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/2.18  % (2326457)CaDiCaL version: 2.1.3
% 8.32/2.18  % (2326457)Termination reason: Instruction limit
% 8.32/2.18  % (2326457)Termination phase: Property scanning
% 8.32/2.18  % (2326457)Time elapsed: 0.004 s
% 8.32/2.18  % (2326457)Peak memory usage: 85 MB
% 8.32/2.18  % (2326457)Instructions burned: 17 (million)
% 8.32/2.18  % (2326435)Instruction limit reached! 
% 8.32/2.18  % (2326435)------------------------------
% 8.32/2.18  % (2326435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/2.18  % (2326435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/2.18  % (2326435)CaDiCaL version: 2.1.3
% 8.32/2.18  % (2326435)Termination reason: Instruction limit
% 8.32/2.18  % (2326435)Termination phase: Preprocessing 3
% 8.32/2.18  % (2326435)Time elapsed: 0.021 s
% 8.32/2.18  % (2326435)Peak memory usage: 87 MB
% 8.32/2.18  % (2326435)Instructions burned: 36 (million)
% 8.32/2.18  % (2326427)Instruction limit reached! 
% 8.32/2.18  % (2326427)------------------------------
% 8.32/2.18  % (2326427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/2.18  % (2326427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/2.18  % (2326427)CaDiCaL version: 2.1.3
% 8.32/2.18  % (2326427)Termination reason: Instruction limit
% 8.32/2.18  % (2326427)Termination phase: Saturation
% 8.32/2.18  % (2326427)Time elapsed: 0.105 s
% 8.32/2.18  % (2326427)Peak memory usage: 118 MB
% 8.32/2.18  % (2326427)Instructions burned: 127 (million)
% 8.32/2.18  % (2326448)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3800565230:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 8.32/2.18  % (2326496)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=969099173:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 8.32/2.18  % (2326496)Instruction limit reached! 
% 8.32/2.18  % (2326496)------------------------------
% 8.32/2.18  % (2326496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.32/2.18  % (2326496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.32/2.18  % (2326496)CaDiCaL version: 2.1.3
% 8.32/2.18  % (2326496)Termination reason: Instruction limit
% 8.32/2.18  % (2326496)Termination phase: Saturation
% 8.32/2.18  % (2326496)Time elapsed: 0.022 s
% 8.32/2.18  % (2326496)Peak memory usage: 90 MB
% 9.80/2.42  % (2326496)Instructions burned: 78 (million)
% 9.80/2.42  % (2326493)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1910531650:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 9.80/2.42  % (2326492)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3513709503:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 9.80/2.42  % (2326497)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=2962012600:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 9.80/2.42  % (2326494)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1493341722:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 9.80/2.42  % (2326493)Instruction limit reached! 
% 9.80/2.42  % (2326493)------------------------------
% 9.80/2.42  % (2326493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.42  % (2326493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.42  % (2326493)CaDiCaL version: 2.1.3
% 9.80/2.42  % (2326493)Termination reason: Instruction limit
% 9.80/2.42  % (2326493)Termination phase: Property scanning
% 9.80/2.42  % (2326493)Time elapsed: 0.006 s
% 9.80/2.42  % (2326493)Peak memory usage: 85 MB
% 9.80/2.42  % (2326493)Instructions burned: 11 (million)
% 9.80/2.42  % (2326506)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3678589932:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi)
% 9.80/2.42  % (2326494)Instruction limit reached! 
% 9.80/2.42  % (2326494)------------------------------
% 9.80/2.42  % (2326494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.42  % (2326494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.42  % (2326494)CaDiCaL version: 2.1.3
% 9.80/2.42  % (2326494)Termination reason: Instruction limit
% 9.80/2.42  % (2326494)Termination phase: Saturation
% 9.80/2.42  % (2326494)Time elapsed: 0.036 s
% 9.80/2.42  % (2326494)Peak memory usage: 89 MB
% 9.80/2.42  % (2326494)Instructions burned: 71 (million)
% 9.80/2.42  % (2326534)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3346575787:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 9.80/2.42  % (2326448)Instruction limit reached! 
% 9.80/2.42  % (2326448)------------------------------
% 9.80/2.42  % (2326448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.42  % (2326448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.42  % (2326448)CaDiCaL version: 2.1.3
% 9.80/2.42  % (2326448)Termination reason: Instruction limit
% 9.80/2.42  % (2326448)Termination phase: Saturation
% 9.80/2.42  % (2326448)Time elapsed: 0.203 s
% 9.80/2.42  % (2326448)Peak memory usage: 93 MB
% 9.80/2.42  % (2326448)Instructions burned: 372 (million)
% 9.80/2.42  % (2326506)Instruction limit reached! 
% 9.80/2.42  % (2326506)------------------------------
% 9.80/2.42  % (2326506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.42  % (2326506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.42  % (2326506)CaDiCaL version: 2.1.3
% 9.80/2.42  % (2326506)Termination reason: Instruction limit
% 9.80/2.42  % (2326506)Termination phase: Saturation
% 9.80/2.42  % (2326506)Time elapsed: 0.089 s
% 9.80/2.42  % (2326506)Peak memory usage: 114 MB
% 9.80/2.42  % (2326506)Instructions burned: 131 (million)
% 9.80/2.42  % (2326548)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2816854196:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi)
% 9.80/2.42  % (2326534)Instruction limit reached! 
% 9.80/2.42  % (2326534)------------------------------
% 9.80/2.42  % (2326534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.42  % (2326534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.42  % (2326534)CaDiCaL version: 2.1.3
% 9.80/2.42  % (2326534)Termination reason: Instruction limit
% 9.80/2.42  % (2326534)Termination phase: Saturation
% 9.80/2.42  % (2326534)Time elapsed: 0.068 s
% 9.80/2.42  % (2326534)Peak memory usage: 135 MB
% 9.80/2.42  % (2326534)Instructions burned: 132 (million)
% 9.80/2.42  % (2326492)Instruction limit reached! 
% 9.80/2.42  % (2326492)------------------------------
% 9.80/2.42  % (2326492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.42  % (2326492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.74  % (2326492)CaDiCaL version: 2.1.3
% 11.23/2.74  % (2326492)Termination reason: Instruction limit
% 11.23/2.74  % (2326492)Termination phase: Saturation
% 11.23/2.74  % (2326492)Time elapsed: 0.143 s
% 11.23/2.74  % (2326492)Peak memory usage: 117 MB
% 11.23/2.74  % (2326492)Instructions burned: 228 (million)
% 11.23/2.74  % (2326548)Instruction limit reached! 
% 11.23/2.74  % (2326548)------------------------------
% 11.23/2.74  % (2326548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.74  % (2326548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.74  % (2326548)CaDiCaL version: 2.1.3
% 11.23/2.74  % (2326548)Termination reason: Instruction limit
% 11.23/2.74  % (2326548)Termination phase: Property scanning
% 11.23/2.74  % (2326548)Time elapsed: 0.020 s
% 11.23/2.74  % (2326548)Peak memory usage: 86 MB
% 11.23/2.74  % (2326548)Instructions burned: 41 (million)
% 11.23/2.74  % (2326556)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=723752744:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi)
% 11.23/2.74  % (2326497)Instruction limit reached! 
% 11.23/2.74  % (2326497)------------------------------
% 11.23/2.74  % (2326497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.74  % (2326497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.74  % (2326497)CaDiCaL version: 2.1.3
% 11.23/2.74  % (2326497)Termination reason: Instruction limit
% 11.23/2.74  % (2326497)Termination phase: Saturation
% 11.23/2.74  % (2326497)Time elapsed: 0.190 s
% 11.23/2.74  % (2326497)Peak memory usage: 92 MB
% 11.23/2.74  % (2326497)Instructions burned: 295 (million)
% 11.23/2.74  % (2326572)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=2217878447:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi)
% 11.23/2.74  % (2326570)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1532206186:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 11.23/2.74  % (2326569)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1451402409:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 11.23/2.74  % (2326573)dis+10_1_si=on:random_seed=3579880557:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi)
% 11.23/2.74  % (2326574)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=839746384:i=383:fsr=off:rtra=on:ev=force_2989 on theBenchmark for (2989ds/383Mi)
% 11.23/2.74  % (2326572)Instruction limit reached! 
% 11.23/2.74  % (2326572)------------------------------
% 11.23/2.74  % (2326572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.74  % (2326572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.74  % (2326572)CaDiCaL version: 2.1.3
% 11.23/2.74  % (2326572)Termination reason: Instruction limit
% 11.23/2.74  % (2326572)Termination phase: Saturation
% 11.23/2.74  % (2326572)Time elapsed: 0.107 s
% 11.23/2.74  % (2326572)Peak memory usage: 118 MB
% 11.23/2.74  % (2326572)Instructions burned: 261 (million)
% 11.23/2.74  % (2326570)Instruction limit reached! 
% 11.23/2.74  % (2326570)------------------------------
% 11.23/2.74  % (2326570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.74  % (2326570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.74  % (2326570)CaDiCaL version: 2.1.3
% 11.23/2.74  % (2326570)Termination reason: Instruction limit
% 11.23/2.74  % (2326570)Termination phase: Saturation
% 11.23/2.74  % (2326570)Time elapsed: 0.097 s
% 11.23/2.74  % (2326570)Peak memory usage: 118 MB
% 11.23/2.74  % (2326570)Instructions burned: 131 (million)
% 11.23/2.74  % (2326581)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=961400625:i=141:doe=on:rtra=on_2989 on theBenchmark for (2989ds/141Mi)
% 11.23/2.74  % (2326556)Instruction limit reached! 
% 11.23/2.74  % (2326556)------------------------------
% 11.23/2.74  % (2326556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.74  % (2326556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.74  % (2326556)CaDiCaL version: 2.1.3
% 11.23/2.74  % (2326556)Termination reason: Instruction limit
% 11.23/2.74  % (2326556)Termination phase: Saturation
% 11.23/2.74  % (2326556)Time elapsed: 0.179 s
% 11.23/2.74  % (2326556)Peak memory usage: 92 MB
% 14.74/3.03  % (2326556)Instructions burned: 307 (million)
% 14.74/3.03  % (2326581)Instruction limit reached! 
% 14.74/3.03  % (2326581)------------------------------
% 14.74/3.03  % (2326581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.74/3.03  % (2326581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/3.03  % (2326581)CaDiCaL version: 2.1.3
% 14.74/3.03  % (2326581)Termination reason: Instruction limit
% 14.74/3.03  % (2326581)Termination phase: Saturation
% 14.74/3.03  % (2326581)Time elapsed: 0.084 s
% 14.74/3.03  % (2326581)Peak memory usage: 91 MB
% 14.74/3.03  % (2326581)Instructions burned: 142 (million)
% 14.74/3.03  % (2326630)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=246046741:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi)
% 14.74/3.03  % (2326630)Instruction limit reached! 
% 14.74/3.03  % (2326630)------------------------------
% 14.74/3.03  % (2326630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.74/3.03  % (2326630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/3.03  % (2326630)CaDiCaL version: 2.1.3
% 14.74/3.03  % (2326630)Termination reason: Instruction limit
% 14.74/3.03  % (2326630)Termination phase: Saturation
% 14.74/3.03  % (2326630)Time elapsed: 0.018 s
% 14.74/3.03  % (2326630)Peak memory usage: 90 MB
% 14.74/3.03  % (2326630)Instructions burned: 65 (million)
% 14.74/3.03  % (2326631)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2175228299:i=121:nm=16:rtra=on_2988 on theBenchmark for (2988ds/121Mi)
% 14.74/3.03  % (2326632)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=68897358:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi)
% 14.74/3.03  % (2326574)Instruction limit reached! 
% 14.74/3.03  % (2326574)------------------------------
% 14.74/3.03  % (2326574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.74/3.03  % (2326574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/3.03  % (2326574)CaDiCaL version: 2.1.3
% 14.74/3.03  % (2326574)Termination reason: Instruction limit
% 14.74/3.03  % (2326574)Termination phase: Saturation
% 14.74/3.03  % (2326574)Time elapsed: 0.244 s
% 14.74/3.03  % (2326574)Peak memory usage: 96 MB
% 14.74/3.03  % (2326574)Instructions burned: 383 (million)
% 14.74/3.03  % (2326631)Instruction limit reached! 
% 14.74/3.03  % (2326631)------------------------------
% 14.74/3.03  % (2326631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.74/3.03  % (2326631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/3.03  % (2326631)CaDiCaL version: 2.1.3
% 14.74/3.03  % (2326631)Termination reason: Instruction limit
% 14.74/3.03  % (2326631)Termination phase: Saturation
% 14.74/3.03  % (2326631)Time elapsed: 0.070 s
% 14.74/3.03  % (2326631)Peak memory usage: 91 MB
% 14.74/3.03  % (2326631)Instructions burned: 122 (million)
% 14.74/3.03  % (2326635)dis+1010_1_to=kbo:si=on:random_seed=3200966732:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2987 on theBenchmark for (2987ds/175Mi)
% 14.74/3.03  % (2326634)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=1494761684:i=39:ins=3:rtra=on_2987 on theBenchmark for (2987ds/39Mi)
% 14.74/3.03  % (2326634)Instruction limit reached! 
% 14.74/3.03  % (2326634)------------------------------
% 14.74/3.03  % (2326634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.74/3.03  % (2326634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/3.03  % (2326634)CaDiCaL version: 2.1.3
% 14.74/3.03  % (2326634)Termination reason: Instruction limit
% 14.74/3.03  % (2326634)Termination phase: Preprocessing 3
% 14.74/3.03  % (2326634)Time elapsed: 0.022 s
% 14.74/3.03  % (2326634)Peak memory usage: 87 MB
% 14.74/3.03  % (2326634)Instructions burned: 39 (million)
% 14.74/3.03  % (2326632)Instruction limit reached! 
% 14.74/3.03  % (2326632)------------------------------
% 14.74/3.03  % (2326632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.74/3.03  % (2326632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/3.03  % (2326632)CaDiCaL version: 2.1.3
% 14.74/3.03  % (2326632)Termination reason: Instruction limit
% 14.74/3.03  % (2326632)Termination phase: Saturation
% 14.74/3.03  % (2326632)Time elapsed: 0.100 s
% 14.74/3.03  % (2326632)Peak memory usage: 118 MB
% 14.74/3.03  % (2326632)Instructions burned: 129 (million)
% 14.74/3.03  % (2326635)Instruction limit reached! 
% 14.74/3.03  % (2326635)------------------------------
% 15.42/3.27  % (2326635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.42/3.27  % (2326635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/3.27  % (2326635)CaDiCaL version: 2.1.3
% 15.42/3.27  % (2326635)Termination reason: Instruction limit
% 15.42/3.27  % (2326635)Termination phase: Saturation
% 15.42/3.27  % (2326635)Time elapsed: 0.054 s
% 15.42/3.27  % (2326635)Peak memory usage: 92 MB
% 15.42/3.27  % (2326635)Instructions burned: 177 (million)
% 15.42/3.27  % (2326638)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2722800776:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi)
% 15.42/3.27  % (2326640)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1401587194:s2a=on:i=483:doe=on:nm=32:rtra=on_2986 on theBenchmark for (2986ds/483Mi)
% 15.42/3.27  % (2326569)Instruction limit reached! 
% 15.42/3.27  % (2326569)------------------------------
% 15.42/3.27  % (2326569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.42/3.27  % (2326569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/3.27  % (2326569)CaDiCaL version: 2.1.3
% 15.42/3.27  % (2326569)Termination reason: Instruction limit
% 15.42/3.27  % (2326569)Termination phase: Saturation
% 15.42/3.27  % (2326569)Time elapsed: 0.436 s
% 15.42/3.27  % (2326569)Peak memory usage: 138 MB
% 15.42/3.27  % (2326569)Instructions burned: 599 (million)
% 15.42/3.27  % (2326642)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1908360395:thitd=on:i=215:nm=0:rtra=on:ev=force_2985 on theBenchmark for (2985ds/215Mi)
% 15.42/3.27  % (2326644)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=240957093:st=2:i=295:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/295Mi)
% 15.42/3.27  % (2326643)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=4015487236:i=349:rtra=on_2985 on theBenchmark for (2985ds/349Mi)
% 15.42/3.27  % (2326644)Instruction limit reached! 
% 15.42/3.27  % (2326644)------------------------------
% 15.42/3.27  % (2326644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.42/3.27  % (2326644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/3.27  % (2326644)CaDiCaL version: 2.1.3
% 15.42/3.27  % (2326644)Termination reason: Instruction limit
% 15.42/3.27  % (2326644)Termination phase: Saturation
% 15.42/3.27  % (2326644)Time elapsed: 0.096 s
% 15.42/3.27  % (2326644)Peak memory usage: 92 MB
% 15.42/3.27  % (2326644)Instructions burned: 296 (million)
% 15.42/3.27  % (2326649)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2483400666:i=328:kws=inv_frequency:nm=20:rtra=on_2984 on theBenchmark for (2984ds/328Mi)
% 15.42/3.27  % (2326642)Instruction limit reached! 
% 15.42/3.27  % (2326642)------------------------------
% 15.42/3.27  % (2326642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.42/3.27  % (2326642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/3.27  % (2326642)CaDiCaL version: 2.1.3
% 15.42/3.27  % (2326642)Termination reason: Instruction limit
% 15.42/3.27  % (2326642)Termination phase: Saturation
% 15.42/3.27  % (2326642)Time elapsed: 0.152 s
% 15.42/3.27  % (2326642)Peak memory usage: 137 MB
% 15.42/3.27  % (2326642)Instructions burned: 215 (million)
% 15.42/3.27  % (2326651)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1903539040:i=281:gtgl=2:rtra=on:gtg=all_2983 on theBenchmark for (2983ds/281Mi)
% 15.42/3.27  % (2326638)Instruction limit reached! 
% 15.42/3.27  % (2326638)------------------------------
% 15.42/3.27  % (2326638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.42/3.27  % (2326638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/3.27  % (2326638)CaDiCaL version: 2.1.3
% 15.42/3.27  % (2326638)Termination reason: Instruction limit
% 15.42/3.27  % (2326638)Termination phase: Saturation
% 15.42/3.27  % (2326638)Time elapsed: 0.233 s
% 15.42/3.27  % (2326638)Peak memory usage: 120 MB
% 15.42/3.27  % (2326638)Instructions burned: 330 (million)
% 15.42/3.27  % (2326573)Instruction limit reached! 
% 15.42/3.27  % (2326573)------------------------------
% 15.42/3.27  % (2326573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.42/3.27  % (2326573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/3.27  % (2326573)CaDiCaL version: 2.1.3
% 17.34/3.56  % (2326573)Termination reason: Instruction limit
% 17.34/3.56  % (2326573)Termination phase: Saturation
% 17.34/3.56  % (2326573)Time elapsed: 0.636 s
% 17.34/3.56  % (2326573)Peak memory usage: 95 MB
% 17.34/3.56  % (2326573)Instructions burned: 1000 (million)
% 17.34/3.56  % (2326643)Instruction limit reached! 
% 17.34/3.56  % (2326643)------------------------------
% 17.34/3.56  % (2326643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.34/3.56  % (2326643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.34/3.56  % (2326643)CaDiCaL version: 2.1.3
% 17.34/3.56  % (2326643)Termination reason: Instruction limit
% 17.34/3.56  % (2326643)Termination phase: Saturation
% 17.34/3.56  % (2326643)Time elapsed: 0.240 s
% 17.34/3.56  % (2326643)Peak memory usage: 120 MB
% 17.34/3.56  % (2326643)Instructions burned: 349 (million)
% 17.34/3.56  % (2326653)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2287283714:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/484Mi)
% 17.34/3.56  % (2326651)Instruction limit reached! 
% 17.34/3.56  % (2326651)------------------------------
% 17.34/3.56  % (2326651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.34/3.56  % (2326651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.34/3.56  % (2326651)CaDiCaL version: 2.1.3
% 17.34/3.56  % (2326651)Termination reason: Instruction limit
% 17.34/3.56  % (2326651)Termination phase: Saturation
% 17.34/3.56  % (2326651)Time elapsed: 0.103 s
% 17.34/3.56  % (2326651)Peak memory usage: 119 MB
% 17.34/3.56  % (2326651)Instructions burned: 284 (million)
% 17.34/3.56  % (2326655)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2551398363:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2982 on theBenchmark for (2982ds/321Mi)
% 17.34/3.56  % (2326649)Instruction limit reached! 
% 17.34/3.56  % (2326649)------------------------------
% 17.34/3.56  % (2326649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.34/3.56  % (2326649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.34/3.56  % (2326649)CaDiCaL version: 2.1.3
% 17.34/3.56  % (2326649)Termination reason: Instruction limit
% 17.34/3.56  % (2326649)Termination phase: Saturation
% 17.34/3.56  % (2326649)Time elapsed: 0.224 s
% 17.34/3.56  % (2326649)Peak memory usage: 119 MB
% 17.34/3.56  % (2326649)Instructions burned: 329 (million)
% 17.34/3.56  % (2326656)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4028600099:i=416:rtra=on:gtg=position:ss=axioms_2982 on theBenchmark for (2982ds/416Mi)
% 17.34/3.56  % (2326640)Instruction limit reached! 
% 17.34/3.56  % (2326640)------------------------------
% 17.34/3.56  % (2326640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.34/3.56  % (2326640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.34/3.56  % (2326640)CaDiCaL version: 2.1.3
% 17.34/3.56  % (2326640)Termination reason: Instruction limit
% 17.34/3.56  % (2326640)Termination phase: Saturation
% 17.34/3.56  % (2326640)Time elapsed: 0.388 s
% 17.34/3.56  % (2326640)Peak memory usage: 137 MB
% 17.34/3.56  % (2326640)Instructions burned: 484 (million)
% 17.34/3.56  % (2326659)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=1109514153:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi)
% 17.34/3.56  % (2326657)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1579920485:i=471:thf=on:kws=precedence:rtra=on_2981 on theBenchmark for (2981ds/471Mi)
% 17.34/3.56  % (2326661)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=859728032:i=375:kws=inv_arity_squared:rtra=on_2981 on theBenchmark for (2981ds/375Mi)
% 17.34/3.56  % (2326659)Instruction limit reached! 
% 17.34/3.56  % (2326659)------------------------------
% 17.34/3.56  % (2326659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.34/3.56  % (2326659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.34/3.56  % (2326659)CaDiCaL version: 2.1.3
% 17.34/3.56  % (2326659)Termination reason: Instruction limit
% 17.34/3.56  % (2326659)Termination phase: Saturation
% 17.34/3.56  % (2326659)Time elapsed: 0.121 s
% 17.34/3.56  % (2326659)Peak memory usage: 136 MB
% 17.34/3.56  % (2326659)Instructions burned: 276 (million)
% 17.34/3.56  % (2326664)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3994616624:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/387Mi)
% 18.40/3.89  % (2326653)Instruction limit reached! 
% 18.40/3.89  % (2326653)------------------------------
% 18.40/3.89  % (2326653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.89  % (2326653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.89  % (2326653)CaDiCaL version: 2.1.3
% 18.40/3.89  % (2326653)Termination reason: Instruction limit
% 18.40/3.89  % (2326653)Termination phase: Saturation
% 18.40/3.89  % (2326653)Time elapsed: 0.229 s
% 18.40/3.89  % (2326653)Peak memory usage: 91 MB
% 18.40/3.89  % (2326653)Instructions burned: 486 (million)
% 18.40/3.89  % (2326655)Instruction limit reached! 
% 18.40/3.89  % (2326655)------------------------------
% 18.40/3.89  % (2326655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.89  % (2326655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.89  % (2326655)CaDiCaL version: 2.1.3
% 18.40/3.89  % (2326655)Termination reason: Instruction limit
% 18.40/3.89  % (2326655)Termination phase: Saturation
% 18.40/3.89  % (2326655)Time elapsed: 0.209 s
% 18.40/3.89  % (2326655)Peak memory usage: 120 MB
% 18.40/3.89  % (2326655)Instructions burned: 321 (million)
% 18.40/3.89  % (2326667)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2924178532:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2979 on theBenchmark for (2979ds/513Mi)
% 18.40/3.89  % (2326656)Instruction limit reached! 
% 18.40/3.89  % (2326656)------------------------------
% 18.40/3.89  % (2326656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.89  % (2326656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.89  % (2326656)CaDiCaL version: 2.1.3
% 18.40/3.89  % (2326656)Termination reason: Instruction limit
% 18.40/3.89  % (2326656)Termination phase: Saturation
% 18.40/3.89  % (2326656)Time elapsed: 0.228 s
% 18.40/3.89  % (2326656)Peak memory usage: 119 MB
% 18.40/3.89  % (2326656)Instructions burned: 417 (million)
% 18.40/3.89  % (2326669)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1530385680:i=334:rtra=on_2979 on theBenchmark for (2979ds/334Mi)
% 18.40/3.89  % (2326670)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1918277950:i=359:rtra=on:gtg=exists_top:ss=axioms_2979 on theBenchmark for (2979ds/359Mi)
% 18.40/3.89  % (2326672)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=4059019438:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2978 on theBenchmark for (2978ds/341Mi)
% 18.40/3.89  % (2326670)Refutation not found, incomplete strategy
% 18.40/3.89  % (2326670)------------------------------
% 18.40/3.89  % (2326670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.89  % (2326670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.89  % (2326670)CaDiCaL version: 2.1.3
% 18.40/3.89  % (2326670)Termination reason: Refutation not found, incomplete strategy
% 18.40/3.89  % (2326670)Time elapsed: 0.054 s
% 18.40/3.89  % (2326670)Peak memory usage: 91 MB
% 18.40/3.89  % (2326670)Instructions burned: 105 (million)
% 18.40/3.89  % (2326657)Instruction limit reached! 
% 18.40/3.89  % (2326657)------------------------------
% 18.40/3.89  % (2326657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.89  % (2326657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.89  % (2326657)CaDiCaL version: 2.1.3
% 18.40/3.89  % (2326657)Termination reason: Instruction limit
% 18.40/3.89  % (2326657)Termination phase: Saturation
% 18.40/3.89  % (2326657)Time elapsed: 0.322 s
% 18.40/3.89  % (2326657)Peak memory usage: 121 MB
% 18.40/3.89  % (2326657)Instructions burned: 473 (million)
% 18.40/3.89  % (2326661)Instruction limit reached! 
% 18.40/3.89  % (2326661)------------------------------
% 18.40/3.89  % (2326661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.89  % (2326661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.89  % (2326661)CaDiCaL version: 2.1.3
% 18.40/3.89  % (2326661)Termination reason: Instruction limit
% 18.40/3.89  % (2326661)Termination phase: Saturation
% 18.40/3.89  % (2326661)Time elapsed: 0.262 s
% 18.40/3.89  % (2326661)Peak memory usage: 120 MB
% 18.40/3.89  % (2326661)Instructions burned: 375 (million)
% 18.40/3.89  % (2326667)Instruction limit reached! 
% 18.40/3.89  % (2326667)------------------------------
% 18.40/3.89  % (2326667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.86/4.31  % (2326667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.86/4.31  % (2326667)CaDiCaL version: 2.1.3
% 22.86/4.31  % (2326667)Termination reason: Instruction limit
% 22.86/4.31  % (2326667)Termination phase: Saturation
% 22.86/4.31  % (2326667)Time elapsed: 0.171 s
% 22.86/4.31  % (2326667)Peak memory usage: 94 MB
% 22.86/4.31  % (2326667)Instructions burned: 514 (million)
% 22.86/4.31  % (2326664)Instruction limit reached! 
% 22.86/4.31  % (2326664)------------------------------
% 22.86/4.31  % (2326664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.86/4.31  % (2326664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.86/4.31  % (2326664)CaDiCaL version: 2.1.3
% 22.86/4.31  % (2326664)Termination reason: Instruction limit
% 22.86/4.31  % (2326664)Termination phase: Saturation
% 22.86/4.31  % (2326664)Time elapsed: 0.276 s
% 22.86/4.31  % (2326664)Peak memory usage: 120 MB
% 22.86/4.31  % (2326664)Instructions burned: 387 (million)
% 22.86/4.31  % (2326677)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=3041716595:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2977 on theBenchmark for (2977ds/235Mi)
% 22.86/4.31  % (2326676)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3447936335:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/261Mi)
% 22.86/4.31  % (2326678)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4012699377:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2977 on theBenchmark for (2977ds/273Mi)
% 22.86/4.31  % (2326669)Instruction limit reached! 
% 22.86/4.31  % (2326669)------------------------------
% 22.86/4.31  % (2326669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.86/4.31  % (2326669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.86/4.31  % (2326669)CaDiCaL version: 2.1.3
% 22.86/4.31  % (2326669)Termination reason: Instruction limit
% 22.86/4.31  % (2326669)Termination phase: Saturation
% 22.86/4.31  % (2326669)Time elapsed: 0.267 s
% 22.86/4.31  % (2326669)Peak memory usage: 136 MB
% 22.86/4.31  % (2326669)Instructions burned: 334 (million)
% 22.86/4.31  % (2326679)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=614612172:i=146:doe=on:rtra=on_2976 on theBenchmark for (2976ds/146Mi)
% 22.86/4.31  % (2326672)Instruction limit reached! 
% 22.86/4.31  % (2326672)------------------------------
% 22.86/4.31  % (2326672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.86/4.31  % (2326672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.86/4.31  % (2326672)CaDiCaL version: 2.1.3
% 22.86/4.31  % (2326672)Termination reason: Instruction limit
% 22.86/4.31  % (2326672)Termination phase: Saturation
% 22.86/4.31  % (2326672)Time elapsed: 0.207 s
% 22.86/4.31  % (2326672)Peak memory usage: 122 MB
% 22.86/4.31  % (2326672)Instructions burned: 341 (million)
% 22.86/4.31  % (2326677)Instruction limit reached! 
% 22.86/4.31  % (2326677)------------------------------
% 22.86/4.31  % (2326677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.86/4.31  % (2326677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.86/4.31  % (2326677)CaDiCaL version: 2.1.3
% 22.86/4.31  % (2326677)Termination reason: Instruction limit
% 22.86/4.31  % (2326677)Termination phase: Saturation
% 22.86/4.31  % (2326677)Time elapsed: 0.095 s
% 22.86/4.31  % (2326677)Peak memory usage: 118 MB
% 22.86/4.31  % (2326677)Instructions burned: 237 (million)
% 22.86/4.31  % (2326670)------------------------------
% 22.86/4.31  % (2326670)------------------------------
% 22.86/4.31  % (2326679)Instruction limit reached! 
% 22.86/4.31  % (2326679)------------------------------
% 22.86/4.31  % (2326679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.86/4.31  % (2326679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.86/4.31  % (2326679)CaDiCaL version: 2.1.3
% 22.86/4.31  % (2326679)Termination reason: Instruction limit
% 22.86/4.31  % (2326679)Termination phase: Saturation
% 22.86/4.31  % (2326679)Time elapsed: 0.087 s
% 22.86/4.31  % (2326679)Peak memory usage: 91 MB
% 22.86/4.31  % (2326679)Instructions burned: 146 (million)
% 22.86/4.31  % (2326686)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3629809583:i=1052:rtra=on_2975 on theBenchmark for (2975ds/1052Mi)
% 22.86/4.31  % (2326683)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4025834921:i=4428:doe=on:fsr=off:rtra=on_2975 on theBenchmark for (2975ds/4428Mi)
% 25.69/4.85  % (2326676)Instruction limit reached! 
% 25.69/4.85  % (2326676)------------------------------
% 25.69/4.85  % (2326676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.69/4.85  % (2326676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.69/4.85  % (2326676)CaDiCaL version: 2.1.3
% 25.69/4.85  % (2326676)Termination reason: Instruction limit
% 25.69/4.85  % (2326676)Termination phase: Saturation
% 25.69/4.85  % (2326676)Time elapsed: 0.184 s
% 25.69/4.85  % (2326676)Peak memory usage: 118 MB
% 25.69/4.85  % (2326676)Instructions burned: 261 (million)
% 25.69/4.85  % (2326685)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=386819283:avsq=on:i=276:avsqr=1,2:rtra=on_2975 on theBenchmark for (2975ds/276Mi)
% 25.69/4.85  % (2326678)Instruction limit reached! 
% 25.69/4.85  % (2326678)------------------------------
% 25.69/4.85  % (2326678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.69/4.85  % (2326678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.69/4.85  % (2326678)CaDiCaL version: 2.1.3
% 25.69/4.85  % (2326678)Termination reason: Instruction limit
% 25.69/4.85  % (2326678)Termination phase: Saturation
% 25.69/4.85  % (2326678)Time elapsed: 0.187 s
% 25.69/4.85  % (2326678)Peak memory usage: 93 MB
% 25.69/4.85  % (2326678)Instructions burned: 273 (million)
% 25.69/4.85  % (2326687)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4102925703:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2974 on theBenchmark for (2974ds/655Mi)
% 25.69/4.85  % (2326688)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=315207649:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2974 on theBenchmark for (2974ds/1054Mi)
% 25.69/4.85  % (2326691)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1725290065:i=107:rtra=on_2974 on theBenchmark for (2974ds/107Mi)
% 25.69/4.85  % (2326693)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2228197682:s2a=on:i=450:doe=on:nm=32:rtra=on_2973 on theBenchmark for (2973ds/450Mi)
% 25.69/4.85  % (2326691)Instruction limit reached! 
% 25.69/4.85  % (2326691)------------------------------
% 25.69/4.85  % (2326691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.69/4.85  % (2326691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.69/4.85  % (2326691)CaDiCaL version: 2.1.3
% 25.69/4.85  % (2326691)Termination reason: Instruction limit
% 25.69/4.85  % (2326691)Termination phase: Saturation
% 25.69/4.85  % (2326691)Time elapsed: 0.058 s
% 25.69/4.85  % (2326691)Peak memory usage: 91 MB
% 25.69/4.85  % (2326691)Instructions burned: 107 (million)
% 25.69/4.85  % (2326685)Instruction limit reached! 
% 25.69/4.85  % (2326685)------------------------------
% 25.69/4.85  % (2326685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.69/4.85  % (2326685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.69/4.85  % (2326685)CaDiCaL version: 2.1.3
% 25.69/4.85  % (2326685)Termination reason: Instruction limit
% 25.69/4.85  % (2326685)Termination phase: Saturation
% 25.69/4.85  % (2326685)Time elapsed: 0.221 s
% 25.69/4.85  % (2326685)Peak memory usage: 136 MB
% 25.69/4.85  % (2326685)Instructions burned: 277 (million)
% 25.69/4.85  % (2326698)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 25.69/4.85  % (2326698)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1546649305:i=1090:aac=none:nm=0:rtra=on:rawr=on_2972 on theBenchmark for (2972ds/1090Mi)
% 25.69/4.85  % (2326686)Instruction limit reached! 
% 25.69/4.85  % (2326686)------------------------------
% 25.69/4.85  % (2326686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.69/4.85  % (2326686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.69/4.85  % (2326686)CaDiCaL version: 2.1.3
% 25.69/4.85  % (2326686)Termination reason: Instruction limit
% 25.69/4.85  % (2326686)Termination phase: Saturation
% 25.69/4.85  % (2326686)Time elapsed: 0.348 s
% 25.69/4.85  % (2326686)Peak memory usage: 97 MB
% 25.69/4.85  % (2326686)Instructions burned: 1052 (million)
% 29.96/5.28  % (2326699)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1808664380:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2971 on theBenchmark for (2971ds/130Mi)
% 29.96/5.28  % (2326701)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1608818156:i=312:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/312Mi)
% 29.96/5.28  % (2326699)Instruction limit reached! 
% 29.96/5.28  % (2326699)------------------------------
% 29.96/5.28  % (2326699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326699)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326699)Termination reason: Instruction limit
% 29.96/5.28  % (2326699)Termination phase: Saturation
% 29.96/5.28  % (2326699)Time elapsed: 0.086 s
% 29.96/5.28  % (2326699)Peak memory usage: 114 MB
% 29.96/5.28  % (2326699)Instructions burned: 130 (million)
% 29.96/5.28  % (2326693)Instruction limit reached! 
% 29.96/5.28  % (2326693)------------------------------
% 29.96/5.28  % (2326693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326693)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326693)Termination reason: Instruction limit
% 29.96/5.28  % (2326693)Termination phase: Saturation
% 29.96/5.28  % (2326693)Time elapsed: 0.357 s
% 29.96/5.28  % (2326693)Peak memory usage: 136 MB
% 29.96/5.28  % (2326693)Instructions burned: 450 (million)
% 29.96/5.28  % (2326687)Instruction limit reached! 
% 29.96/5.28  % (2326687)------------------------------
% 29.96/5.28  % (2326687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326687)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326687)Termination reason: Instruction limit
% 29.96/5.28  % (2326687)Termination phase: Saturation
% 29.96/5.28  % (2326687)Time elapsed: 0.450 s
% 29.96/5.28  % (2326687)Peak memory usage: 98 MB
% 29.96/5.28  % (2326687)Instructions burned: 656 (million)
% 29.96/5.28  % (2326701)Instruction limit reached! 
% 29.96/5.28  % (2326701)------------------------------
% 29.96/5.28  % (2326701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326701)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326701)Termination reason: Instruction limit
% 29.96/5.28  % (2326701)Termination phase: Saturation
% 29.96/5.28  % (2326701)Time elapsed: 0.115 s
% 29.96/5.28  % (2326701)Peak memory usage: 119 MB
% 29.96/5.28  % (2326701)Instructions burned: 315 (million)
% 29.96/5.28  % (2326704)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2385248068:i=491:doe=on:rtra=on:gtg=position_2969 on theBenchmark for (2969ds/491Mi)
% 29.96/5.28  % (2326707)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2632281527:i=776:doe=on:rtra=on_2968 on theBenchmark for (2968ds/776Mi)
% 29.96/5.28  % (2326705)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=330345068:s2a=on:i=835:s2at=2:rtra=on_2969 on theBenchmark for (2969ds/835Mi)
% 29.96/5.28  % (2326706)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2915522396:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2969 on theBenchmark for (2969ds/307Mi)
% 29.96/5.28  % (2326704)Refutation not found, incomplete strategy
% 29.96/5.28  % (2326704)------------------------------
% 29.96/5.28  % (2326704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326704)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326704)Termination reason: Refutation not found, incomplete strategy
% 29.96/5.28  % (2326704)Time elapsed: 0.067 s
% 29.96/5.28  % (2326704)Peak memory usage: 91 MB
% 29.96/5.28  % (2326704)Instructions burned: 118 (million)
% 29.96/5.28  % (2326706)Refutation not found, incomplete strategy
% 29.96/5.28  % (2326706)------------------------------
% 29.96/5.28  % (2326706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326706)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326706)Termination reason: Refutation not found, incomplete strategy
% 29.96/5.28  % (2326706)Time elapsed: 0.116 s
% 29.96/5.28  % (2326706)Peak memory usage: 92 MB
% 29.96/5.28  % (2326706)Instructions burned: 190 (million)
% 29.96/5.28  % (2326688)Instruction limit reached! 
% 29.96/5.28  % (2326688)------------------------------
% 29.96/5.28  % (2326688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326688)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326688)Termination reason: Instruction limit
% 29.96/5.28  % (2326688)Termination phase: Saturation
% 29.96/5.28  % (2326688)Time elapsed: 0.709 s
% 29.96/5.28  % (2326688)Peak memory usage: 96 MB
% 29.96/5.28  % (2326688)Instructions burned: 1055 (million)
% 29.96/5.28  % (2326707)Instruction limit reached! 
% 29.96/5.28  % (2326707)------------------------------
% 29.96/5.28  % (2326707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326707)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326707)Termination reason: Instruction limit
% 29.96/5.28  % (2326707)Termination phase: Saturation
% 29.96/5.28  % (2326707)Time elapsed: 0.278 s
% 29.96/5.28  % (2326707)Peak memory usage: 123 MB
% 29.96/5.28  % (2326707)Instructions burned: 778 (million)
% 29.96/5.28  % (2326704)------------------------------
% 29.96/5.28  % (2326704)------------------------------
% 29.96/5.28  % (2326712)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1146199496:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2966 on theBenchmark for (2966ds/646Mi)
% 29.96/5.28  % (2326713)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=152786484:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2965 on theBenchmark for (2965ds/784Mi)
% 29.96/5.28  % (2326706)------------------------------
% 29.96/5.28  % (2326706)------------------------------
% 29.96/5.28  % (2326698)Instruction limit reached! 
% 29.96/5.28  % (2326698)------------------------------
% 29.96/5.28  % (2326698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326698)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326698)Termination reason: Instruction limit
% 29.96/5.28  % (2326698)Termination phase: Saturation
% 29.96/5.28  % (2326698)Time elapsed: 0.675 s
% 29.96/5.28  % (2326698)Peak memory usage: 123 MB
% 29.96/5.28  % (2326698)Instructions burned: 1092 (million)
% 29.96/5.28  % (2326714)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=2300218011:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2965 on theBenchmark for (2965ds/1131Mi)
% 29.96/5.28  % (2326717)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=1194985338:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2964 on theBenchmark for (2964ds/246Mi)
% 29.96/5.28  % (2326718)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2653018415:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2964 on theBenchmark for (2964ds/775Mi)
% 29.96/5.28  % (2326705)Instruction limit reached! 
% 29.96/5.28  % (2326705)------------------------------
% 29.96/5.28  % (2326705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326705)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326705)Termination reason: Instruction limit
% 29.96/5.28  % (2326705)Termination phase: Saturation
% 29.96/5.28  % (2326705)Time elapsed: 0.526 s
% 29.96/5.28  % (2326705)Peak memory usage: 96 MB
% 29.96/5.28  % (2326705)Instructions burned: 835 (million)
% 29.96/5.28  % (2326713)Instruction limit reached! 
% 29.96/5.28  % (2326713)------------------------------
% 29.96/5.28  % (2326713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326713)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326713)Termination reason: Instruction limit
% 29.96/5.28  % (2326713)Termination phase: Saturation
% 29.96/5.28  % (2326713)Time elapsed: 0.290 s
% 29.96/5.28  % (2326713)Peak memory usage: 122 MB
% 29.96/5.28  % (2326713)Instructions burned: 784 (million)
% 29.96/5.28  % (2326722)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3005843469:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi)
% 29.96/5.28  % (2326717)Instruction limit reached! 
% 29.96/5.28  % (2326717)------------------------------
% 29.96/5.28  % (2326717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326717)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326717)Termination reason: Instruction limit
% 29.96/5.28  % (2326717)Termination phase: Saturation
% 29.96/5.28  % (2326717)Time elapsed: 0.179 s
% 29.96/5.28  % (2326717)Peak memory usage: 118 MB
% 29.96/5.28  % (2326717)Instructions burned: 246 (million)
% 29.96/5.28  % (2326723)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=952570587:i=102:nm=16:rtra=on_2961 on theBenchmark for (2961ds/102Mi)
% 29.96/5.28  % (2326712)Instruction limit reached! 
% 29.96/5.28  % (2326712)------------------------------
% 29.96/5.28  % (2326712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326712)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326712)Termination reason: Instruction limit
% 29.96/5.28  % (2326712)Termination phase: Saturation
% 29.96/5.28  % (2326712)Time elapsed: 0.450 s
% 29.96/5.28  % (2326712)Peak memory usage: 139 MB
% 29.96/5.28  % (2326712)Instructions burned: 646 (million)
% 29.96/5.28  % (2326723)Instruction limit reached! 
% 29.96/5.28  % (2326723)------------------------------
% 29.96/5.28  % (2326723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326723)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326723)Termination reason: Instruction limit
% 29.96/5.28  % (2326723)Termination phase: Saturation
% 29.96/5.28  % (2326723)Time elapsed: 0.031 s
% 29.96/5.28  % (2326723)Peak memory usage: 90 MB
% 29.96/5.28  % (2326723)Instructions burned: 104 (million)
% 29.96/5.28  % (2326725)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2236626716:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2961 on theBenchmark for (2961ds/1094Mi)
% 29.96/5.28  % (2326714)First to succeed.
% 29.96/5.28  % (2326714)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2326329"
% 29.96/5.28  % (2326722)Instruction limit reached! 
% 29.96/5.28  % (2326722)------------------------------
% 29.96/5.28  % (2326722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326722)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326722)Termination reason: Instruction limit
% 29.96/5.28  % (2326722)Termination phase: Saturation
% 29.96/5.28  % (2326722)Time elapsed: 0.185 s
% 29.96/5.28  % (2326722)Peak memory usage: 93 MB
% 29.96/5.28  % (2326722)Instructions burned: 273 (million)
% 29.96/5.28  % (2326728)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=3714531827:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/868Mi)
% 29.96/5.28  % (2326718)Also succeeded, but the first one will report.
% 29.96/5.28  % (2326727)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2805435644:i=6400:doe=on:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/6400Mi)
% 29.96/5.28  % (2326730)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=1259586924:i=1846:canc=cautious:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/1846Mi)
% 29.96/5.28  % (2326730)Refutation not found, incomplete strategy
% 29.96/5.28  % (2326730)------------------------------
% 29.96/5.28  % (2326730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/5.28  % (2326730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/5.28  % (2326730)CaDiCaL version: 2.1.3
% 29.96/5.28  % (2326730)Termination reason: Refutation not found, incomplete strategy
% 29.96/5.28  % (2326730)Time elapsed: 0.068 s
% 29.96/5.28  % (2326730)Peak memory usage: 92 MB
% 29.96/5.28  % (2326730)Instructions burned: 122 (million)
% 29.96/5.28  % (2326714)Refutation found. Thanks to Tanya!
% 29.96/5.28  % SZS status Theorem for theBenchmark
% 29.96/5.28  % SZS output start Proof for theBenchmark
% See solution above
% 30.86/5.47  % (2326714)------------------------------
% 30.86/5.47  % (2326714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.86/5.47  % (2326714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.86/5.47  % (2326714)CaDiCaL version: 2.1.3
% 30.86/5.47  % (2326714)Termination reason: Refutation
% 30.86/5.47  % (2326714)Time elapsed: 0.412 s
% 30.86/5.47  % (2326714)Peak memory usage: 124 MB
% 30.86/5.47  % (2326714)Instructions burned: 610 (million)
% 30.86/5.47  % (2326714)------------------------------
% 30.86/5.47  % (2326714)------------------------------
% 30.86/5.47  % (2326329)Success in time 4.303 s
% 30.86/5.47  % Vampire exiting
%------------------------------------------------------------------------------