%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP347_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 : n006.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 24.96s 4.84s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 37
% Syntax : Number of formulae : 134 ( 39 unt; 0 typ; 25 def)
% Number of atoms : 303 ( 99 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 309 ( 140 ~; 134 |; 7 &)
% ( 23 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number arithmetic : 12 ( 12 atm; 0 fun; 0 num; 0 var)
% Number of types : 91 ( 89 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 83 ( 79 usr; 20 prp; 0-3 aty)
% Number of functors : 285 ( 285 usr; 66 con; 0-4 aty)
% Number of variables : 66 ( 66 !; 0 ?; 66 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'Num1$': $tType ).
tff(type_def_6,type,
'Unit_set$': $tType ).
tff(type_def_7,type,
'Int_bool_fun$': $tType ).
tff(type_def_8,type,
'Int_iarray$': $tType ).
tff(type_def_9,type,
'Rows_num1_sum_set$': $tType ).
tff(type_def_10,type,
'Num0_literal_sum_set$': $tType ).
tff(type_def_11,type,
'Cols_a_fun_set$': $tType ).
tff(type_def_12,type,
'A_a_prod$': $tType ).
tff(type_def_13,type,
'Nat_a_fun$': $tType ).
tff(type_def_14,type,
'Num1_num0_sum_set$': $tType ).
tff(type_def_15,type,
'Rows$': $tType ).
tff(type_def_16,type,
'A_iarray_iarray$': $tType ).
tff(type_def_17,type,
'A_cols_vec_bool_fun$': $tType ).
tff(type_def_18,type,
'Int_int_prod$': $tType ).
tff(type_def_19,type,
'Cols_cols_fun$': $tType ).
tff(type_def_20,type,
'A_cols_vec_rows_vec_cols_vec$': $tType ).
tff(type_def_21,type,
'Rows_a_cols_vec_fun$': $tType ).
tff(type_def_22,type,
'Cols_a_prod$': $tType ).
tff(type_def_23,type,
'Cols_cols_vec_cols_vec$': $tType ).
tff(type_def_24,type,
'Literal$': $tType ).
tff(type_def_25,type,
'Rows_set$': $tType ).
tff(type_def_26,type,
'Int_set$': $tType ).
tff(type_def_27,type,
'Int_int_fun$': $tType ).
tff(type_def_28,type,
'Num1_rows_sum_set$': $tType ).
tff(type_def_29,type,
'Num0$': $tType ).
tff(type_def_30,type,
'A_rows_vec_cols_vec$': $tType ).
tff(type_def_31,type,
'Rows_option_set$': $tType ).
tff(type_def_32,type,
'A_rows_vec_set$': $tType ).
tff(type_def_33,type,
'Rows_rows_sum_set$': $tType ).
tff(type_def_34,type,
'Cols_cols_vec_rows_vec$': $tType ).
tff(type_def_35,type,
'Num0_num1_sum_set$': $tType ).
tff(type_def_36,type,
'Num1_literal_sum_set$': $tType ).
tff(type_def_37,type,
'Nat_nat_fun$': $tType ).
tff(type_def_38,type,
'A_cols_vec_set$': $tType ).
tff(type_def_39,type,
'Nat$': $tType ).
tff(type_def_40,type,
'A_cols_vec_iarray$': $tType ).
tff(type_def_41,type,
'Num0_num0_sum_set$': $tType ).
tff(type_def_42,type,
'A_cols_prod$': $tType ).
tff(type_def_43,type,
'Cols_iarray$': $tType ).
tff(type_def_44,type,
'Literal_set$': $tType ).
tff(type_def_45,type,
'Cols_bool_fun$': $tType ).
tff(type_def_46,type,
'Num1_nat_sum_set$': $tType ).
tff(type_def_47,type,
'A_rows_vec$': $tType ).
tff(type_def_48,type,
'Cols_cols_bool_fun_fun$': $tType ).
tff(type_def_49,type,
'A_cols_vec_rows_vec_rows_vec$': $tType ).
tff(type_def_50,type,
tlbool: $tType ).
tff(type_def_51,type,
'Num1_option_set$': $tType ).
tff(type_def_52,type,
'Rows_a_cols_vec_fun_bool_fun$': $tType ).
tff(type_def_53,type,
'Rows_bool_fun$': $tType ).
tff(type_def_54,type,
'Int_cols_vec_cols_vec$': $tType ).
tff(type_def_55,type,
'Int_cols_vec$': $tType ).
tff(type_def_56,type,
'A_cols_vec_rows_vec$': $tType ).
tff(type_def_57,type,
'A_int_prod$': $tType ).
tff(type_def_58,type,
'A_set$': $tType ).
tff(type_def_59,type,
'Cols_int_fun$': $tType ).
tff(type_def_60,type,
'Int_cols_fun$': $tType ).
tff(type_def_61,type,
'A_cols_vec$': $tType ).
tff(type_def_62,type,
'Nat_a_cols_vec_fun$': $tType ).
tff(type_def_63,type,
'Int_cols_prod$': $tType ).
tff(type_def_64,type,
'A$': $tType ).
tff(type_def_65,type,
'A_rows_vec_bool_fun$': $tType ).
tff(type_def_66,type,
'Int_a_prod$': $tType ).
tff(type_def_67,type,
'Cols_set$': $tType ).
tff(type_def_68,type,
'Num1_set$': $tType ).
tff(type_def_69,type,
'Literal_option_set$': $tType ).
tff(type_def_70,type,
'Nat_int_iarray_prod$': $tType ).
tff(type_def_71,type,
'Nat_option_set$': $tType ).
tff(type_def_72,type,
'Rows_a_cols_vec_fun_set$': $tType ).
tff(type_def_73,type,
'A_a_fun$': $tType ).
tff(type_def_74,type,
'Nat_a_cols_vec_iarray_prod$': $tType ).
tff(type_def_75,type,
'Cols$': $tType ).
tff(type_def_76,type,
'A_cols_vec_cols_vec$': $tType ).
tff(type_def_77,type,
'Nat_cols_iarray_prod$': $tType ).
tff(type_def_78,type,
'Num0_option_set$': $tType ).
tff(type_def_79,type,
'Int_int_bool_fun_fun$': $tType ).
tff(type_def_80,type,
'A_iarray$': $tType ).
tff(type_def_81,type,
'Num0_rows_sum_set$': $tType ).
tff(type_def_82,type,
'Nat_a_iarray_prod$': $tType ).
tff(type_def_83,type,
'Nat_bool_fun$': $tType ).
tff(type_def_84,type,
'Cols_a_fun_bool_fun$': $tType ).
tff(type_def_85,type,
'Cols_a_fun$': $tType ).
tff(type_def_86,type,
'Num0_set$': $tType ).
tff(type_def_87,type,
'Cols_int_prod$': $tType ).
tff(type_def_88,type,
'Nat_set$': $tType ).
tff(type_def_89,type,
'Cols_cols_vec$': $tType ).
tff(type_def_90,type,
'Int_cols_vec_rows_vec$': $tType ).
tff(type_def_91,type,
'Num0_nat_sum_set$': $tType ).
tff(type_def_92,type,
'Cols_cols_prod$': $tType ).
tff(type_def_93,type,
'Num1_num1_sum_set$': $tType ).
tff(func_def_0,type,
'matrix_to_iarray$a': 'A_cols_vec_cols_vec$' > 'A_iarray_iarray$' ).
tff(func_def_1,type,
'plus$a': 'A$' > 'A_a_fun$' ).
tff(func_def_2,type,
'uuj$': ( 'Cols$' * 'Cols$' * 'A_cols_vec_cols_vec$' ) > 'Cols_bool_fun$' ).
tff(func_def_3,type,
'least_non_zero_position_of_vector_from_index$c': 'A_cols_vec_iarray$' > 'Nat_nat_fun$' ).
tff(func_def_4,type,
'uut$': ( 'A_cols_vec_rows_vec$' * 'Rows$' ) > 'Cols_bool_fun$' ).
tff(func_def_5,type,
'uus$': ( 'A_cols_vec_rows_vec_rows_vec$' * 'Nat$' ) > 'Rows_bool_fun$' ).
tff(func_def_6,type,
'nrows$': 'Cols_cols_vec_rows_vec$' > 'Nat$' ).
tff(func_def_7,type,
'least$': 'Cols_bool_fun$' > 'Cols$' ).
tff(func_def_8,type,
'uug$': ( 'Rows$' * 'A_cols_vec_rows_vec$' ) > 'Rows_bool_fun$' ).
tff(func_def_9,type,
'uun$': 'A_cols_vec_rows_vec$' > 'A_rows_vec_bool_fun$' ).
tff(func_def_10,type,
'pair$g': ( 'Cols$' * 'A$' ) > 'Cols_a_prod$' ).
tff(func_def_11,type,
'uum$': 'A_cols_vec_cols_vec$' > 'A_cols_vec_bool_fun$' ).
tff(func_def_12,type,
'pair$h': ( 'Cols$' * 'Cols$' ) > 'Cols_cols_prod$' ).
tff(func_def_13,type,
'column$e': ( 'Rows$' * 'A_rows_vec_cols_vec$' ) > 'A_cols_vec$' ).
tff(func_def_14,type,
'plus$i': ( 'A_set$' * 'A_set$' ) > 'A_set$' ).
tff(func_def_15,type,
'col_rank$': 'A_cols_vec_rows_vec$' > 'Nat$' ).
tff(func_def_16,type,
'top$j': 'Rows_num1_sum_set$' ).
tff(func_def_17,type,
'uuc$': ( 'Cols$' * 'Rows$' * 'A_cols_vec_rows_vec$' ) > 'Cols_bool_fun$' ).
tff(func_def_18,type,
'top$r': 'Num1_literal_sum_set$' ).
tff(func_def_19,type,
'less_eq$': 'Cols_cols_bool_fun_fun$' ).
tff(func_def_20,type,
'less$a': 'Cols_cols_bool_fun_fun$' ).
tff(func_def_21,type,
'card$o': 'Rows_option_set$' > 'Nat$' ).
tff(func_def_22,type,
'fun_app$b': ( 'Rows_a_cols_vec_fun$' * 'Rows$' ) > 'A_cols_vec$' ).
tff(func_def_23,type,
'pair$k': ( $int * 'Cols$' ) > 'Int_cols_prod$' ).
tff(func_def_24,type,
'zero$l': 'Cols_a_prod$' ).
tff(func_def_25,type,
'row_add_iterate$': ( 'A_cols_vec_cols_vec$' * 'Nat$' * 'Cols$' * 'Cols$' ) > 'A_cols_vec_cols_vec$' ).
tff(func_def_26,type,
'collect$b': 'A_rows_vec_bool_fun$' > 'A_rows_vec_set$' ).
tff(func_def_27,type,
'one$': 'Rows$' ).
tff(func_def_28,type,
'card$h': 'Num1_option_set$' > 'Nat$' ).
tff(func_def_29,type,
'card$r': 'Num1_nat_sum_set$' > 'Nat$' ).
tff(func_def_30,type,
'top$a': 'Cols_set$' ).
tff(func_def_31,type,
'less_eq$b': 'Nat$' > 'Nat_bool_fun$' ).
tff(func_def_32,type,
'vec_nth$j': ( 'Int_cols_vec_cols_vec$' * 'Cols$' ) > 'Int_cols_vec$' ).
tff(func_def_33,type,
'uup$': ( 'Cols_cols_vec_rows_vec$' * 'Nat$' ) > 'Cols_bool_fun$' ).
tff(func_def_34,type,
'vec_nth$i': ( 'Cols_cols_vec_cols_vec$' * 'Cols$' ) > 'Cols_cols_vec$' ).
tff(func_def_35,type,
'vec_nth$b': 'Int_cols_vec$' > 'Cols_int_fun$' ).
tff(func_def_36,type,
'pair$i': ( 'Cols$' * $int ) > 'Cols_int_prod$' ).
tff(func_def_37,type,
'card$a': 'Rows_set$' > 'Nat$' ).
tff(func_def_38,type,
'zero$k': 'A_int_prod$' ).
tff(func_def_39,type,
'uuh$': ( 'Cols$' * 'A_cols_vec$' ) > 'Cols_bool_fun$' ).
tff(func_def_40,type,
'one$a': 'A$' ).
tff(func_def_41,type,
'vec_to_iarray$d': 'A_rows_vec$' > 'A_iarray$' ).
tff(func_def_42,type,
'vec_nth$h': ( 'A_cols_vec_rows_vec_cols_vec$' * 'Cols$' ) > 'A_cols_vec_rows_vec$' ).
tff(func_def_43,type,
'vec_nth$': 'A_cols_vec$' > 'Cols_a_fun$' ).
tff(func_def_44,type,
'zero$b': 'A_cols_vec$' ).
tff(func_def_45,type,
'card$d': 'Num1_set$' > 'Nat$' ).
tff(func_def_46,type,
'row_iarray$': ( 'Nat$' * 'A_iarray_iarray$' ) > 'A_iarray$' ).
tff(func_def_47,type,
'least$c': 'Rows_bool_fun$' > 'Rows$' ).
tff(func_def_48,type,
'plus$h': ( 'Int_set$' * 'Int_set$' ) > 'Int_set$' ).
tff(func_def_49,type,
'top$': 'Rows_set$' ).
tff(func_def_50,type,
'top$x': 'Num0_rows_sum_set$' ).
tff(func_def_51,type,
'least$a': 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_52,type,
'top$w': 'Num0_nat_sum_set$' ).
tff(func_def_53,type,
'uuu$': 'Rows_bool_fun$' ).
tff(func_def_54,type,
'least$b': 'Int_bool_fun$' > $int ).
tff(func_def_55,type,
'least_non_zero_position_of_vector_from_index$b': 'Int_iarray$' > 'Nat_nat_fun$' ).
tff(func_def_56,type,
'of_fun$a': ( 'Nat_a_cols_vec_fun$' * 'Nat$' ) > 'A_cols_vec_iarray$' ).
tff(func_def_57,type,
'top$g': 'Nat_set$' ).
tff(func_def_58,type,
'to_nat$a': 'Rows$' > 'Nat$' ).
tff(func_def_59,type,
'fun_app$c': ( 'Cols_cols_bool_fun_fun$' * 'Cols$' ) > 'Cols_bool_fun$' ).
tff(func_def_60,type,
'zero$q': 'Int_int_prod$' ).
tff(func_def_61,type,
'vec_to_iarray$e': 'A_cols_vec_cols_vec$' > 'A_cols_vec_iarray$' ).
tff(func_def_62,type,
'vec_to_iarray$a': 'A_cols_vec_rows_vec$' > 'A_cols_vec_iarray$' ).
tff(func_def_63,type,
'pair$l': ( $int * $int ) > 'Int_int_prod$' ).
tff(func_def_64,type,
'fun_app$g': ( 'Nat_a_fun$' * 'Nat$' ) > 'A$' ).
tff(func_def_65,type,
'plus$b': 'Cols$' > 'Cols_cols_fun$' ).
tff(func_def_66,type,
'card$j': 'Num0_set$' > 'Nat$' ).
tff(func_def_67,type,
'zero$i': 'A_a_prod$' ).
tff(func_def_68,type,
'card$g': 'Rows_rows_sum_set$' > 'Nat$' ).
tff(func_def_69,type,
'of_nat$': 'Nat$' > $int ).
tff(func_def_70,type,
'top$s': 'Num1_nat_sum_set$' ).
tff(func_def_71,type,
'fun_app$l': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_72,type,
'card$w': 'Num0_rows_sum_set$' > 'Nat$' ).
tff(func_def_73,type,
'fun_app$f': ( 'Nat_a_cols_vec_fun$' * 'Nat$' ) > 'A_cols_vec$' ).
tff(func_def_74,type,
'least_non_zero_position_of_vector$': 'A_iarray$' > 'Nat$' ).
tff(func_def_75,type,
'i$': 'Nat$' ).
tff(func_def_76,type,
'uul$': 'A_cols_vec_cols_vec$' > 'Cols_cols_bool_fun_fun$' ).
tff(func_def_77,type,
'zero$m': 'Cols_cols_prod$' ).
tff(func_def_78,type,
'plus$d': ( 'A_cols_vec$' * 'A_cols_vec$' ) > 'A_cols_vec$' ).
tff(func_def_79,type,
'vec_nth$e': ( 'Int_cols_vec_rows_vec$' * 'Rows$' ) > 'Int_cols_vec$' ).
tff(func_def_80,type,
'plus$': ( 'Rows$' * 'Rows$' ) > 'Rows$' ).
tff(func_def_81,type,
'matrix_to_iarray$b': 'A_rows_vec_cols_vec$' > 'A_iarray_iarray$' ).
tff(func_def_82,type,
'zero$p': 'Int_cols_prod$' ).
tff(func_def_83,type,
'least_non_zero_position_of_vector_from_index$a': 'Cols_iarray$' > 'Nat_nat_fun$' ).
tff(func_def_84,type,
'less$': 'Rows$' > 'Rows_bool_fun$' ).
tff(func_def_85,type,
'uuy$': 'A_cols_vec_rows_vec$' > 'Nat_a_cols_vec_fun$' ).
tff(func_def_86,type,
'card$b': 'Cols_set$' > 'Nat$' ).
tff(func_def_87,type,
'card$q': 'Num1_literal_sum_set$' > 'Nat$' ).
tff(func_def_88,type,
'top$l': 'Num1_option_set$' ).
tff(func_def_89,type,
'top$p': 'Rows_option_set$' ).
tff(func_def_90,type,
'card$p': 'Num1_num0_sum_set$' > 'Nat$' ).
tff(func_def_91,type,
'vec_nth$g': ( 'A_cols_vec_cols_vec$' * 'Cols$' ) > 'A_cols_vec$' ).
tff(func_def_92,type,
'one$b': 'A_cols_vec$' ).
tff(func_def_93,type,
'less_eq$a': 'Rows$' > 'Rows_bool_fun$' ).
tff(func_def_94,type,
'one$c': 'A_cols_vec_rows_vec$' ).
tff(func_def_95,type,
tltrue: tlbool ).
tff(func_def_96,type,
'uub$': 'Nat_set$' > 'Nat_bool_fun$' ).
tff(func_def_97,type,
'fun_app$q': ( 'A_a_fun$' * 'A$' ) > 'A$' ).
tff(func_def_98,type,
'to_nat$': 'Cols$' > 'Nat$' ).
tff(func_def_99,type,
'one$d': 'Cols$' ).
tff(func_def_100,type,
'card$n': 'Nat_set$' > 'Nat$' ).
tff(func_def_101,type,
'a$': 'A_cols_vec_rows_vec$' ).
tff(func_def_102,type,
'top$n': 'Literal_option_set$' ).
tff(func_def_103,type,
'pair$f': ( 'A$' * $int ) > 'A_int_prod$' ).
tff(func_def_104,type,
'card$u': 'Num0_literal_sum_set$' > 'Nat$' ).
tff(func_def_105,type,
'j$': 'Cols$' ).
tff(func_def_106,type,
'top$o': 'Nat_option_set$' ).
tff(func_def_107,type,
'nrows$a': 'Int_cols_vec_rows_vec$' > 'Nat$' ).
tff(func_def_108,type,
'fun_app$j': ( 'Cols_int_fun$' * 'Cols$' ) > $int ).
tff(func_def_109,type,
'row$': ( 'Cols$' * 'A_cols_vec_cols_vec$' ) > 'A_cols_vec$' ).
tff(func_def_110,type,
'ncols$a': 'A_cols_vec_rows_vec$' > 'Nat$' ).
tff(func_def_111,type,
'zero$a': 'Cols$' ).
tff(func_def_112,type,
'column$a': ( 'Cols$' * 'A_cols_vec_rows_vec$' ) > 'A_rows_vec$' ).
tff(func_def_113,type,
'vec_to_iarray$': 'A_cols_vec$' > 'A_iarray$' ).
tff(func_def_114,type,
'card$i': 'Num0_option_set$' > 'Nat$' ).
tff(func_def_115,type,
'uur$': ( 'A_cols_vec_rows_vec$' * 'Nat$' ) > 'Cols_bool_fun$' ).
tff(func_def_116,type,
'collect$': 'Nat_bool_fun$' > 'Nat_set$' ).
tff(func_def_117,type,
'card$x': 'Unit_set$' > 'Nat$' ).
tff(func_def_118,type,
'zero$f': 'Int_cols_vec$' ).
tff(func_def_119,type,
'card$s': 'Num0_num1_sum_set$' > 'Nat$' ).
tff(func_def_120,type,
'card$t': 'Num0_num0_sum_set$' > 'Nat$' ).
tff(func_def_121,type,
'top$h': 'Num1_num1_sum_set$' ).
tff(func_def_122,type,
'uud$': ( 'A_cols_vec_rows_vec$' * 'Rows$' ) > 'Cols_bool_fun$' ).
tff(func_def_123,type,
'fun_app$n': ( 'Int_int_fun$' * $int ) > $int ).
tff(func_def_124,type,
'collect$a': 'A_cols_vec_bool_fun$' > 'A_cols_vec_set$' ).
tff(func_def_125,type,
'zero$e': 'Cols_cols_vec$' ).
tff(func_def_126,type,
'pair$j': ( $int * 'A$' ) > 'Int_a_prod$' ).
tff(func_def_127,type,
'zero$d': 'Rows$' ).
tff(func_def_128,type,
'vec_to_iarray$b': 'Cols_cols_vec$' > 'Cols_iarray$' ).
tff(func_def_129,type,
'of_fun$': ( 'Nat_a_fun$' * 'Nat$' ) > 'A_iarray$' ).
tff(func_def_130,type,
'fun_app$a': ( 'Cols_a_fun$' * 'Cols$' ) > 'A$' ).
tff(func_def_131,type,
'card$l': 'Literal_set$' > 'Nat$' ).
tff(func_def_132,type,
'vec_nth$f': ( 'Cols_cols_vec_rows_vec$' * 'Rows$' ) > 'Cols_cols_vec$' ).
tff(func_def_133,type,
'plus$g': ( 'A_iarray$' * 'A_iarray$' ) > 'A_iarray$' ).
tff(func_def_134,type,
'map_matrix$': ( 'A_a_fun$' * 'A_cols_vec_rows_vec$' ) > 'A_cols_vec_rows_vec$' ).
tff(func_def_135,type,
'uuv$': 'Cols_bool_fun$' ).
tff(func_def_136,type,
'card$k': 'Literal_option_set$' > 'Nat$' ).
tff(func_def_137,type,
'top$c': 'Rows_a_cols_vec_fun_set$' ).
tff(func_def_138,type,
'column$d': ( 'Rows$' * 'A_cols_vec_rows_vec_cols_vec$' ) > 'A_cols_vec_cols_vec$' ).
tff(func_def_139,type,
'less$b': 'Nat$' > 'Nat_bool_fun$' ).
tff(func_def_140,type,
'top$i': 'Num1_rows_sum_set$' ).
tff(func_def_141,type,
'card$': 'A_rows_vec_set$' > 'Nat$' ).
tff(func_def_142,type,
'top$q': 'Num1_num0_sum_set$' ).
tff(func_def_143,type,
'top$k': 'Rows_rows_sum_set$' ).
tff(func_def_144,type,
'matrix_to_iarray$': 'A_cols_vec_rows_vec$' > 'A_iarray_iarray$' ).
tff(func_def_145,type,
'card$m': 'Nat_option_set$' > 'Nat$' ).
tff(func_def_146,type,
'from_nat$a': 'Nat$' > 'Cols$' ).
tff(func_def_147,type,
'vec_nth$d': ( 'A_cols_vec_rows_vec_rows_vec$' * 'Rows$' ) > 'A_cols_vec_rows_vec$' ).
tff(func_def_148,type,
'fun_app$m': ( 'Int_cols_fun$' * $int ) > 'Cols$' ).
tff(func_def_149,type,
'column_iarray$': ( 'Nat$' * 'A_iarray_iarray$' ) > 'A_iarray$' ).
tff(func_def_150,type,
'pair$d': ( 'A$' * 'A$' ) > 'A_a_prod$' ).
tff(func_def_151,type,
'top$m': 'Num0_option_set$' ).
tff(func_def_152,type,
'vec_nth$a': 'A_cols_vec_rows_vec$' > 'Rows_a_cols_vec_fun$' ).
tff(func_def_153,type,
'card$f': 'Rows_num1_sum_set$' > 'Nat$' ).
tff(func_def_154,type,
'uuw$': 'Nat$' > 'Nat_bool_fun$' ).
tff(func_def_155,type,
'nrows$e': 'A_cols_vec_rows_vec_cols_vec$' > 'Nat$' ).
tff(func_def_156,type,
'nrows$d': 'A_cols_vec_cols_vec$' > 'Nat$' ).
tff(func_def_157,type,
'plus$e': ( 'A_cols_vec_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'A_cols_vec_rows_vec$' ).
tff(func_def_158,type,
'uu$': 'Cols_bool_fun$' ).
tff(func_def_159,type,
'zero$o': 'Int_a_prod$' ).
tff(func_def_160,type,
'uui$': ( 'Cols$' * 'Rows$' * 'A_cols_vec_rows_vec_cols_vec$' ) > 'Cols_bool_fun$' ).
tff(func_def_161,type,
'zero$': 'A$' ).
tff(func_def_162,type,
'uuq$': ( 'Int_cols_vec_rows_vec$' * 'Nat$' ) > 'Cols_bool_fun$' ).
tff(func_def_163,type,
'card$e': 'Num1_rows_sum_set$' > 'Nat$' ).
tff(func_def_164,type,
'uuk$': ( 'Rows$' * 'Cols$' * 'A_cols_vec_rows_vec$' ) > 'Rows_bool_fun$' ).
tff(func_def_165,type,
'top$e': 'Num0_set$' ).
tff(func_def_166,type,
'zero$h': 'A_cols_vec_cols_vec$' ).
tff(func_def_167,type,
'top$v': 'Num0_literal_sum_set$' ).
tff(func_def_168,type,
tlfalse: tlbool ).
tff(func_def_169,type,
'uue$': ( 'Cols$' * 'Cols_cols_vec$' ) > 'Cols_bool_fun$' ).
tff(func_def_170,type,
'nat$': $int > 'Nat$' ).
tff(func_def_171,type,
'column$b': ( 'Cols$' * 'Cols_cols_vec_cols_vec$' ) > 'Cols_cols_vec$' ).
tff(func_def_172,type,
'top$d': 'Num1_set$' ).
tff(func_def_173,type,
'pair$e': ( 'A$' * 'Cols$' ) > 'A_cols_prod$' ).
tff(func_def_174,type,
'zero$n': 'Cols_int_prod$' ).
tff(func_def_175,type,
'vec_to_iarray$c': 'Int_cols_vec$' > 'Int_iarray$' ).
tff(func_def_176,type,
'row$a': ( 'Rows$' * 'A_cols_vec_rows_vec$' ) > 'A_cols_vec$' ).
tff(func_def_177,type,
'vec_nth$k': ( 'A_rows_vec$' * 'Rows$' ) > 'A$' ).
tff(func_def_178,type,
'nrows$b': 'A_cols_vec_rows_vec$' > 'Nat$' ).
tff(func_def_179,type,
'top$b': 'Cols_a_fun_set$' ).
tff(func_def_180,type,
'pair$a': ( 'Nat$' * 'Cols_iarray$' ) > 'Nat_cols_iarray_prod$' ).
tff(func_def_181,type,
'top$u': 'Num0_num0_sum_set$' ).
tff(func_def_182,type,
'vec_nth$c': 'Cols_cols_vec$' > 'Cols_cols_fun$' ).
tff(func_def_183,type,
'plus$c': ( 'Int_int_prod$' * 'Int_int_prod$' ) > 'Int_int_prod$' ).
tff(func_def_184,type,
'column$c': ( 'Cols$' * 'Int_cols_vec_cols_vec$' ) > 'Int_cols_vec$' ).
tff(func_def_185,type,
'row_add_iterate$a': ( 'A_cols_vec_rows_vec$' * 'Nat$' * 'Rows$' * 'Cols$' ) > 'A_cols_vec_rows_vec$' ).
tff(func_def_186,type,
'top$y': 'Unit_set$' ).
tff(func_def_187,type,
'top$f': 'Literal_set$' ).
tff(func_def_188,type,
'row_add_iterate$b': ( 'A_cols_vec_rows_vec_cols_vec$' * 'Nat$' * 'Cols$' * 'Rows$' ) > 'A_cols_vec_rows_vec_cols_vec$' ).
tff(func_def_189,type,
'zero$g': 'A_rows_vec$' ).
tff(func_def_190,type,
'zero$c': 'A_cols_vec_rows_vec$' ).
tff(func_def_191,type,
'top$t': 'Num0_num1_sum_set$' ).
tff(func_def_192,type,
'nrows$c': 'A_cols_vec_rows_vec_rows_vec$' > 'Nat$' ).
tff(func_def_193,type,
'card$c': 'Num1_num1_sum_set$' > 'Nat$' ).
tff(func_def_194,type,
'zero$j': 'A_cols_prod$' ).
tff(func_def_195,type,
'uua$': 'Cols_bool_fun$' ).
tff(func_def_196,type,
'column$': ( 'Cols$' * 'A_cols_vec_cols_vec$' ) > 'A_cols_vec$' ).
tff(func_def_197,type,
'card$v': 'Num0_nat_sum_set$' > 'Nat$' ).
tff(func_def_198,type,
'pair$c': ( 'Nat$' * 'A_cols_vec_iarray$' ) > 'Nat_a_cols_vec_iarray_prod$' ).
tff(func_def_199,type,
'row_rank$': 'A_cols_vec_rows_vec$' > 'Nat$' ).
tff(func_def_200,type,
'uuf$': ( 'Cols$' * 'Int_cols_vec$' ) > 'Cols_bool_fun$' ).
tff(func_def_201,type,
'pair$': ( 'Nat$' * 'A_iarray$' ) > 'Nat_a_iarray_prod$' ).
tff(func_def_202,type,
'least_non_zero_position_of_vector_from_index$': 'A_iarray$' > 'Nat_nat_fun$' ).
tff(func_def_203,type,
'pair$b': ( 'Nat$' * 'Int_iarray$' ) > 'Nat_int_iarray_prod$' ).
tff(func_def_204,type,
'uuo$': 'A_cols_vec_rows_vec$' > 'A_cols_vec_bool_fun$' ).
tff(func_def_205,type,
'fun_app$p': ( 'Int_int_bool_fun_fun$' * $int ) > 'Int_bool_fun$' ).
tff(func_def_206,type,
'from_nat$': 'Nat$' > 'Rows$' ).
tff(func_def_207,type,
'plus$f': ( 'A_iarray_iarray$' * 'A_iarray_iarray$' ) > 'A_iarray_iarray$' ).
tff(func_def_208,type,
'fun_app$k': ( 'Cols_cols_fun$' * 'Cols$' ) > 'Cols$' ).
tff(func_def_209,type,
'uux$': 'A_cols_vec$' > 'Nat_a_fun$' ).
tff(func_def_210,type,
'ncols$': 'A_rows_vec_cols_vec$' > 'Nat$' ).
tff(func_def_215,type,
sK9: ( 'Cols_bool_fun$' * 'Cols_bool_fun$' ) > 'Cols$' ).
tff(func_def_216,type,
sK10: 'Rows_set$' > 'Rows$' ).
tff(func_def_217,type,
sK11: ( 'Rows_set$' * 'Rows$' ) > 'Rows$' ).
tff(func_def_218,type,
sK12: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_219,type,
sK13: ( 'A_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_220,type,
sK14: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_221,type,
sK15: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_222,type,
sK16: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_223,type,
sK17: 'Cols_cols_bool_fun_fun$' > 'Cols$' ).
tff(func_def_224,type,
sK18: 'Cols_cols_bool_fun_fun$' > 'Cols$' ).
tff(func_def_225,type,
sK19: 'Cols_cols_bool_fun_fun$' > 'Cols$' ).
tff(func_def_226,type,
sK20: 'Cols_cols_bool_fun_fun$' > 'Cols$' ).
tff(func_def_227,type,
sK21: 'Cols_bool_fun$' > 'Cols$' ).
tff(func_def_228,type,
sK22: 'Cols_bool_fun$' > 'Cols$' ).
tff(func_def_229,type,
sK23: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_230,type,
sK24: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_231,type,
sK25: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_232,type,
sK26: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_233,type,
sK27: ( 'Cols_bool_fun$' * 'Cols_bool_fun$' ) > 'Cols$' ).
tff(func_def_234,type,
sK28: ( 'A_cols_vec$' * 'A_cols_vec$' ) > 'Cols$' ).
tff(func_def_235,type,
sK29: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_236,type,
sK30: ( 'Rows$' * 'Cols$' * 'A_cols_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_237,type,
sK31: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_238,type,
sK32: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_239,type,
sK33: ( 'Cols_bool_fun$' * 'Cols_bool_fun$' ) > 'Cols$' ).
tff(func_def_240,type,
sK34: ( 'Cols_bool_fun$' * 'Cols$' ) > 'Cols$' ).
tff(func_def_241,type,
sK35: 'Rows_bool_fun$' > 'Rows$' ).
tff(func_def_242,type,
sK36: 'Rows_bool_fun$' > 'Rows$' ).
tff(func_def_243,type,
sK37: ( 'A_cols_vec_rows_vec$' * 'A_cols_vec$' ) > 'Rows$' ).
tff(func_def_244,type,
sK38: ( 'Cols_bool_fun$' * 'Cols_bool_fun$' ) > 'Cols$' ).
tff(func_def_245,type,
sK39: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_246,type,
sK40: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_247,type,
sK41: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_248,type,
sK42: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_249,type,
sK43: ( 'Rows$' * 'A_cols_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_250,type,
sK44: $int > $int ).
tff(func_def_251,type,
sK45: ( 'A_cols_vec_rows_vec$' * 'Rows$' ) > 'Cols$' ).
tff(func_def_252,type,
sK46: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_253,type,
sK47: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_254,type,
sK48: ( 'Rows$' * 'A_cols_vec_rows_vec_cols_vec$' * 'Cols$' ) > 'Cols$' ).
tff(func_def_255,type,
sK49: 'Cols_cols_bool_fun_fun$' > 'Cols$' ).
tff(func_def_256,type,
sK50: 'Cols_cols_bool_fun_fun$' > 'Cols$' ).
tff(func_def_257,type,
sK51: 'Cols_cols_bool_fun_fun$' > 'Cols$' ).
tff(func_def_258,type,
sK52: 'Cols_cols_bool_fun_fun$' > 'Cols$' ).
tff(func_def_259,type,
sK53: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_260,type,
sK54: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_261,type,
sK55: ( 'Nat_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_262,type,
sK56: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_263,type,
sK57: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_264,type,
sK58: ( 'A_cols_vec$' * 'Cols$' ) > 'Cols$' ).
tff(func_def_265,type,
sK59: ( 'Cols_bool_fun$' * 'Cols$' ) > 'Cols$' ).
tff(func_def_266,type,
sK60: ( 'Cols_bool_fun$' * 'Cols_bool_fun$' ) > 'Cols$' ).
tff(func_def_267,type,
sK61: 'A_cols_vec_rows_vec$' > 'Rows$' ).
tff(func_def_268,type,
sK62: ( 'Cols$' * 'Cols$' * 'A_cols_vec_cols_vec$' ) > 'Cols$' ).
tff(func_def_269,type,
sK63: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_270,type,
sK64: ( 'A_cols_vec_cols_vec$' * 'A_cols_vec$' ) > 'Cols$' ).
tff(func_def_271,type,
sK65: ( 'Cols_bool_fun$' * 'Cols$' ) > 'Cols$' ).
tff(func_def_272,type,
sK66: ( 'Cols_bool_fun$' * 'Cols$' ) > 'Cols$' ).
tff(func_def_273,type,
sK67: $int > $int ).
tff(func_def_274,type,
sK68: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_275,type,
sK69: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_276,type,
sK70: ( 'Cols_bool_fun$' * 'Cols$' ) > 'Cols$' ).
tff(func_def_277,type,
sK71: ( 'Cols_bool_fun$' * 'Cols$' ) > 'Cols$' ).
tff(func_def_278,type,
sK72: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_279,type,
sK73: ( 'A_cols_vec_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_280,type,
sK74: ( 'Nat_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_281,type,
sK75: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_282,type,
sK76: 'Cols_cols_fun$' > 'Cols$' ).
tff(func_def_283,type,
sF77: 'Cols$' ).
tff(func_def_284,type,
sF78: 'Nat$' ).
tff(func_def_285,type,
sF79: $int ).
tff(func_def_286,type,
sF80: 'Cols$' ).
tff(func_def_287,type,
sF81: 'Nat$' ).
tff(func_def_288,type,
sF82: $int ).
tff(pred_def_1,type,
'member$f': ( 'Rows_a_cols_vec_fun$' * 'Rows_a_cols_vec_fun_set$' ) > $o ).
tff(pred_def_2,type,
'fun_app$o': ( 'Int_bool_fun$' * $int ) > $o ).
tff(pred_def_3,type,
'reduced_row_echelon_form$a': 'Cols_cols_vec_cols_vec$' > $o ).
tff(pred_def_4,type,
'member$h': ( 'Num1$' * 'Num1_set$' ) > $o ).
tff(pred_def_5,type,
'is_zero_iarray$a': 'A_cols_vec_iarray$' > $o ).
tff(pred_def_6,type,
'member$c': ( 'A_cols_vec$' * 'A_cols_vec_set$' ) > $o ).
tff(pred_def_7,type,
'less_eq$c': ( 'Num1_set$' * 'Num1_set$' ) > $o ).
tff(pred_def_8,type,
'is_zero_iarray$': 'A_iarray$' > $o ).
tff(pred_def_9,type,
'is_zero_row$b': ( 'Rows$' * 'Int_cols_vec_rows_vec$' ) > $o ).
tff(pred_def_10,type,
'is_zero_row$a': ( 'Rows$' * 'Cols_cols_vec_rows_vec$' ) > $o ).
tff(pred_def_11,type,
'reduced_row_echelon_form$g': 'A_cols_vec_rows_vec_rows_vec$' > $o ).
tff(pred_def_12,type,
'fun_app$e': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).
tff(pred_def_13,type,
'divides_aux$': 'Int_int_prod$' > $o ).
tff(pred_def_14,type,
'less$g': ( 'Rows_set$' * 'Rows_set$' ) > $o ).
tff(pred_def_15,type,
'reduced_row_echelon_form$c': 'A_cols_vec_cols_vec$' > $o ).
tff(pred_def_16,type,
'less$c': ( 'Num1_set$' * 'Num1_set$' ) > $o ).
tff(pred_def_17,type,
'member$g': ( $int * 'Int_set$' ) > $o ).
tff(pred_def_18,type,
'member$j': ( 'Literal$' * 'Literal_set$' ) > $o ).
tff(pred_def_19,type,
'fun_app$i': ( 'A_rows_vec_bool_fun$' * 'A_rows_vec$' ) > $o ).
tff(pred_def_20,type,
'member$d': ( 'A_rows_vec$' * 'A_rows_vec_set$' ) > $o ).
tff(pred_def_21,type,
'member$i': ( 'Num0$' * 'Num0_set$' ) > $o ).
tff(pred_def_22,type,
'reduced_row_echelon_form$e': 'Cols_cols_vec_rows_vec$' > $o ).
tff(pred_def_23,type,
'less_eq$g': ( 'Rows_set$' * 'Rows_set$' ) > $o ).
tff(pred_def_24,type,
'fun_app$r': ( 'Cols_a_fun_bool_fun$' * 'Cols_a_fun$' ) > $o ).
tff(pred_def_25,type,
'reduced_row_echelon_form$b': 'Int_cols_vec_cols_vec$' > $o ).
tff(pred_def_26,type,
'reduced_row_echelon_form$d': 'A_cols_vec_rows_vec_cols_vec$' > $o ).
tff(pred_def_27,type,
'fun_app$h': ( 'A_cols_vec_bool_fun$' * 'A_cols_vec$' ) > $o ).
tff(pred_def_28,type,
'less_eq$e': ( 'Literal_set$' * 'Literal_set$' ) > $o ).
tff(pred_def_29,type,
'member$e': ( 'Cols_a_fun$' * 'Cols_a_fun_set$' ) > $o ).
tff(pred_def_30,type,
'fun_app$d': ( 'Rows_bool_fun$' * 'Rows$' ) > $o ).
tff(pred_def_31,type,
'vector_all_zero_from_index$b': 'Nat_int_iarray_prod$' > $o ).
tff(pred_def_32,type,
'vector_all_zero_from_index$a': 'Nat_cols_iarray_prod$' > $o ).
tff(pred_def_33,type,
'vector_all_zero_from_index$c': 'Nat_a_cols_vec_iarray_prod$' > $o ).
tff(pred_def_34,type,
'less_eq$f': ( 'Nat_set$' * 'Nat_set$' ) > $o ).
tff(pred_def_35,type,
'is_zero_row$': ( 'Rows$' * 'A_cols_vec_rows_vec$' ) > $o ).
tff(pred_def_36,type,
'reduced_row_echelon_form$f': 'Int_cols_vec_rows_vec$' > $o ).
tff(pred_def_37,type,
'less_eq$i': ( 'Int_set$' * 'Int_set$' ) > $o ).
tff(pred_def_38,type,
'member$': ( 'Rows$' * 'Rows_set$' ) > $o ).
tff(pred_def_39,type,
'member$k': ( 'A$' * 'A_set$' ) > $o ).
tff(pred_def_40,type,
'less$e': ( 'Literal_set$' * 'Literal_set$' ) > $o ).
tff(pred_def_41,type,
'reduced_row_echelon_form$': 'A_cols_vec_rows_vec$' > $o ).
tff(pred_def_42,type,
'member$b': ( 'Nat$' * 'Nat_set$' ) > $o ).
tff(pred_def_43,type,
'less_eq$d': ( 'Num0_set$' * 'Num0_set$' ) > $o ).
tff(pred_def_44,type,
'less$d': ( 'Num0_set$' * 'Num0_set$' ) > $o ).
tff(pred_def_45,type,
'less$f': ( 'Nat_set$' * 'Nat_set$' ) > $o ).
tff(pred_def_46,type,
'fun_app$s': ( 'Rows_a_cols_vec_fun_bool_fun$' * 'Rows_a_cols_vec_fun$' ) > $o ).
tff(pred_def_47,type,
'fun_app$': ( 'Cols_bool_fun$' * 'Cols$' ) > $o ).
tff(pred_def_48,type,
'less_eq$h': ( 'A_set$' * 'A_set$' ) > $o ).
tff(pred_def_49,type,
'is_zero_row$c': ( 'Rows$' * 'A_cols_vec_rows_vec_rows_vec$' ) > $o ).
tff(pred_def_50,type,
'member$a': ( 'Cols$' * 'Cols_set$' ) > $o ).
tff(pred_def_51,type,
'vector_all_zero_from_index$': 'Nat_a_iarray_prod$' > $o ).
tff(pred_def_54,type,
sP0: ( 'Cols$' * 'Cols$' * 'Cols$' ) > $o ).
tff(pred_def_55,type,
sP1: ( 'Cols$' * 'Cols$' * 'Cols$' ) > $o ).
tff(pred_def_56,type,
sP2: ( 'Cols$' * 'Cols$' * 'Cols$' ) > $o ).
tff(pred_def_57,type,
sP3: ( 'Cols$' * 'Cols$' * 'Cols$' ) > $o ).
tff(pred_def_58,type,
sP4: ( 'Cols$' * 'Cols$' * 'Cols$' ) > $o ).
tff(pred_def_59,type,
sP5: ( 'Cols$' * 'Cols$' * 'Cols$' ) > $o ).
tff(pred_def_60,type,
sP6: ( $int * $int * $int ) > $o ).
tff(pred_def_61,type,
sP7: ( $int * $int * $int ) > $o ).
tff(pred_def_62,type,
sP8: ( $int * $int * $int ) > $o ).
tff(f1,axiom,
! [X0: 'Cols$'] :
( ( ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) != 'zero$' )
& 'fun_app$'('fun_app$c'('less_eq$','zero$a'),X0) )
<=> 'fun_app$'('uu$',X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom0) ).
tff(f4,axiom,
! [X0: 'Cols$'] :
( ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) != 'zero$' )
<=> 'fun_app$'('uua$',X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom3) ).
tff(f6,axiom,
! [X1: 'Nat$',X0: 'A_cols_vec_rows_vec$'] : ( 'fun_app$f'('uuy$'(X0),X1) = 'fun_app$b'('vec_nth$a'(X0),'from_nat$'(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom5) ).
tff(f27,conjecture,
'of_nat$'('to_nat$'('least$'('uu$'))) = 'of_nat$'('to_nat$'('least$'('uua$'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture26) ).
tff(f28,negated_conjecture,
( ( ~ 'of_nat$'('to_nat$'('least$'('uu$'))) ) = 'of_nat$'('to_nat$'('least$'('uua$'))) ),
inference(negated_conjecture,[status(cth)],[f27]) ).
tff(f29,axiom,
! [X0: 'Cols$'] : 'fun_app$'('fun_app$c'('less_eq$','zero$a'),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom27) ).
tff(f31,axiom,
'of_nat$'('to_nat$'('j$')) = 'of_nat$'('to_nat$'('least$'('uu$'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom29) ).
tff(f37,axiom,
! [X1: 'Cols$',X0: 'Cols$'] :
( ( 'of_nat$'('to_nat$'(X0)) = 'of_nat$'('to_nat$'(X1)) )
<=> ( X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom35) ).
tff(f39,axiom,
! [X1: 'Cols$',X0: 'Cols_bool_fun$'] :
( 'fun_app$'(X0,X1)
=> 'fun_app$'('fun_app$c'('less_eq$','least$'(X0)),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom37) ).
tff(f127,axiom,
! [X1: 'Cols$',X0: 'Cols_bool_fun$'] :
( 'fun_app$'(X0,X1)
=> 'fun_app$'(X0,'least$'(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom125) ).
tff(f129,axiom,
! [X0: 'Cols$',X1: 'Cols$'] :
( 'fun_app$'('fun_app$c'('less_eq$',X0),X1)
=> $lesseq('of_nat$'('to_nat$'(X0)),'of_nat$'('to_nat$'(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom127) ).
tff(f152,axiom,
'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),'j$') = 'one$a',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom150) ).
tff(f212,axiom,
'zero$' != 'one$a',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom210) ).
tff(f699,plain,
! [X1: 'Cols$',X0: 'Cols$'] :
( 'fun_app$'('fun_app$c'('less_eq$',X0),X1)
=> ~ $less('of_nat$'('to_nat$'(X1)),'of_nat$'('to_nat$'(X0))) ),
inference(theory_normalization,[],[f129]) ).
tff(f829,plain,
'of_nat$'('to_nat$'('least$'('uu$'))) != 'of_nat$'('to_nat$'('least$'('uua$'))),
inference(flattening,[],[f28]) ).
tff(f835,plain,
! [X1: 'Cols_bool_fun$',X0: 'Cols$'] :
( 'fun_app$'(X1,X0)
=> 'fun_app$'('fun_app$c'('less_eq$','least$'(X1)),X0) ),
inference(rectify,[],[f39]) ).
tff(f849,plain,
! [X0: 'Cols$',X1: 'Cols$'] :
( ( 'of_nat$'('to_nat$'(X0)) = 'of_nat$'('to_nat$'(X1)) )
<=> ( X0 = X1 ) ),
inference(rectify,[],[f37]) ).
tff(f1106,plain,
! [X0: 'Nat$',X1: 'A_cols_vec_rows_vec$'] : ( 'fun_app$f'('uuy$'(X1),X0) = 'fun_app$b'('vec_nth$a'(X1),'from_nat$'(X0)) ),
inference(rectify,[],[f6]) ).
tff(f1225,plain,
! [X0: 'Cols$',X1: 'Cols$'] :
( ~ 'fun_app$'('fun_app$c'('less_eq$',X0),X1)
| ~ $less('of_nat$'('to_nat$'(X1)),'of_nat$'('to_nat$'(X0))) ),
inference(ennf_transformation,[],[f699]) ).
tff(f1323,plain,
! [X0: 'Cols_bool_fun$',X1: 'Cols$'] :
( ~ 'fun_app$'(X0,X1)
| 'fun_app$'(X0,'least$'(X0)) ),
inference(ennf_transformation,[],[f127]) ).
tff(f1422,plain,
! [X0: 'Cols$',X1: 'Cols_bool_fun$'] :
( ~ 'fun_app$'(X1,X0)
| 'fun_app$'('fun_app$c'('less_eq$','least$'(X1)),X0) ),
inference(ennf_transformation,[],[f835]) ).
tff(f1660,plain,
! [X0: 'Cols$',X1: 'Cols$'] :
( ( ( 'of_nat$'('to_nat$'(X0)) = 'of_nat$'('to_nat$'(X1)) )
| ( X0 != X1 ) )
& ( ( X0 = X1 )
| ( 'of_nat$'('to_nat$'(X0)) != 'of_nat$'('to_nat$'(X1)) ) ) ),
inference(nnf_transformation,[],[f849]) ).
tff(f1766,plain,
! [X0: 'Cols$'] :
( ( ( ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) != 'zero$' )
& 'fun_app$'('fun_app$c'('less_eq$','zero$a'),X0) )
| ~ 'fun_app$'('uu$',X0) )
& ( 'fun_app$'('uu$',X0)
| ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) = 'zero$' )
| ~ 'fun_app$'('fun_app$c'('less_eq$','zero$a'),X0) ) ),
inference(nnf_transformation,[],[f1]) ).
tff(f1767,plain,
! [X0: 'Cols$'] :
( ( ( ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) != 'zero$' )
& 'fun_app$'('fun_app$c'('less_eq$','zero$a'),X0) )
| ~ 'fun_app$'('uu$',X0) )
& ( 'fun_app$'('uu$',X0)
| ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) = 'zero$' )
| ~ 'fun_app$'('fun_app$c'('less_eq$','zero$a'),X0) ) ),
inference(flattening,[],[f1766]) ).
tff(f1798,plain,
! [X0: 'Cols$'] :
( ( ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) != 'zero$' )
| ~ 'fun_app$'('uua$',X0) )
& ( 'fun_app$'('uua$',X0)
| ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) = 'zero$' ) ) ),
inference(nnf_transformation,[],[f4]) ).
tff(f2089,plain,
! [X0: 'Cols$',X1: 'Cols$'] :
( ~ $less('of_nat$'('to_nat$'(X1)),'of_nat$'('to_nat$'(X0)))
| ~ 'fun_app$'('fun_app$c'('less_eq$',X0),X1) ),
inference(cnf_transformation,[],[f1225]) ).
tff(f2090,plain,
'of_nat$'('to_nat$'('least$'('uu$'))) = 'of_nat$'('to_nat$'('j$')),
inference(cnf_transformation,[],[f31]) ).
tff(f2129,plain,
'of_nat$'('to_nat$'('least$'('uu$'))) != 'of_nat$'('to_nat$'('least$'('uua$'))),
inference(cnf_transformation,[],[f829]) ).
tff(f2226,plain,
! [X0: 'Cols$',X1: 'Cols$'] :
( ( 'of_nat$'('to_nat$'(X0)) != 'of_nat$'('to_nat$'(X1)) )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f1660]) ).
tff(f2230,plain,
! [X0: 'Cols$'] : 'fun_app$'('fun_app$c'('less_eq$','zero$a'),X0),
inference(cnf_transformation,[],[f29]) ).
tff(f2398,plain,
! [X0: 'Cols$'] :
( ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) = 'zero$' )
| ~ 'fun_app$'('fun_app$c'('less_eq$','zero$a'),X0)
| 'fun_app$'('uu$',X0) ),
inference(cnf_transformation,[],[f1767]) ).
tff(f2449,plain,
! [X0: 'Cols$'] :
( 'fun_app$'('uua$',X0)
| ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) = 'zero$' ) ),
inference(cnf_transformation,[],[f1798]) ).
tff(f2450,plain,
! [X0: 'Cols$'] :
( ~ 'fun_app$'('uua$',X0)
| ( 'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),X0) != 'zero$' ) ),
inference(cnf_transformation,[],[f1798]) ).
tff(f2460,plain,
! [X0: 'Cols_bool_fun$',X1: 'Cols$'] :
( ~ 'fun_app$'(X0,X1)
| 'fun_app$'(X0,'least$'(X0)) ),
inference(cnf_transformation,[],[f1323]) ).
tff(f2574,plain,
'fun_app$a'('vec_nth$'('fun_app$b'('vec_nth$a'('a$'),'from_nat$'('i$'))),'j$') = 'one$a',
inference(cnf_transformation,[],[f152]) ).
tff(f2675,plain,
'zero$' != 'one$a',
inference(cnf_transformation,[],[f212]) ).
tff(f2722,plain,
! [X0: 'Nat$',X1: 'A_cols_vec_rows_vec$'] : ( 'fun_app$f'('uuy$'(X1),X0) = 'fun_app$b'('vec_nth$a'(X1),'from_nat$'(X0)) ),
inference(cnf_transformation,[],[f1106]) ).
tff(f2740,plain,
! [X0: 'Cols$',X1: 'Cols_bool_fun$'] :
( 'fun_app$'('fun_app$c'('less_eq$','least$'(X1)),X0)
| ~ 'fun_app$'(X1,X0) ),
inference(cnf_transformation,[],[f1422]) ).
tff(f2916,definition,
sF77 = 'least$'('uu$'),
introduced(definition,[new_symbols(definition,[sF77])],[function_definition]) ).
tff(f2917,plain,
'least$'('uu$') = sF77,
inference(reorient_equations,[],[f2916]) ).
tff(f2918,definition,
sF78 = 'to_nat$'(sF77),
introduced(definition,[new_symbols(definition,[sF78])],[function_definition]) ).
tff(f2919,plain,
'to_nat$'(sF77) = sF78,
inference(reorient_equations,[],[f2918]) ).
tff(f2920,definition,
sF79 = 'of_nat$'(sF78),
introduced(definition,[new_symbols(definition,[sF79])],[function_definition]) ).
tff(f2921,plain,
'of_nat$'(sF78) = sF79,
inference(reorient_equations,[],[f2920]) ).
tff(f2922,definition,
sF80 = 'least$'('uua$'),
introduced(definition,[new_symbols(definition,[sF80])],[function_definition]) ).
tff(f2923,plain,
'least$'('uua$') = sF80,
inference(reorient_equations,[],[f2922]) ).
tff(f2924,definition,
sF81 = 'to_nat$'(sF80),
introduced(definition,[new_symbols(definition,[sF81])],[function_definition]) ).
tff(f2925,plain,
'to_nat$'(sF80) = sF81,
inference(reorient_equations,[],[f2924]) ).
tff(f2926,definition,
sF82 = 'of_nat$'(sF81),
introduced(definition,[new_symbols(definition,[sF82])],[function_definition]) ).
tff(f2927,plain,
sF82 != sF79,
inference(definition_folding,[],[f2129,f2926,f2925,f2923,f2921,f2919,f2917]) ).
tff(f2962,definition,
( spl83_5
<=> ( 'to_nat$'(sF80) = sF81 ) ),
introduced(definition,[new_symbols(definition,[spl83_5])],[avatar_definition]) ).
tff(f2964,plain,
( ( 'to_nat$'(sF80) = sF81 )
| ~ spl83_5 ),
inference(avatar_component_clause,[],[f2962]) ).
tff(f2965,plain,
spl83_5,
inference(avatar_split_clause,[],[f2925,f2962]) ).
tff(f2969,definition,
( spl83_6
<=> ( sF82 = sF79 ) ),
introduced(definition,[new_symbols(definition,[spl83_6])],[avatar_definition]) ).
tff(f2972,plain,
~ spl83_6,
inference(avatar_split_clause,[],[f2927,f2969]) ).
tff(f2979,plain,
! [X0: 'Cols$'] :
( ~ 'fun_app$'('fun_app$c'('less_eq$','zero$a'),X0)
| 'fun_app$'('uu$',X0)
| ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) ) ),
inference(backward_demodulation,[],[f2398,f2722]) ).
tff(f2982,definition,
( spl83_8
<=> ( 'of_nat$'(sF78) = sF79 ) ),
introduced(definition,[new_symbols(definition,[spl83_8])],[avatar_definition]) ).
tff(f2984,plain,
( ( 'of_nat$'(sF78) = sF79 )
| ~ spl83_8 ),
inference(avatar_component_clause,[],[f2982]) ).
tff(f2985,plain,
spl83_8,
inference(avatar_split_clause,[],[f2921,f2982]) ).
tff(f2986,plain,
'one$a' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),'j$'),
inference(forward_demodulation,[],[f2574,f2722]) ).
tff(f2988,definition,
( spl83_9
<=> ( 'zero$' = 'one$a' ) ),
introduced(definition,[new_symbols(definition,[spl83_9])],[avatar_definition]) ).
tff(f2990,plain,
( ( 'zero$' != 'one$a' )
| spl83_9 ),
inference(avatar_component_clause,[],[f2988]) ).
tff(f2991,plain,
~ spl83_9,
inference(avatar_split_clause,[],[f2675,f2988]) ).
tff(f2999,definition,
( spl83_11
<=> ( sF82 = 'of_nat$'(sF81) ) ),
introduced(definition,[new_symbols(definition,[spl83_11])],[avatar_definition]) ).
tff(f3001,plain,
( ( sF82 = 'of_nat$'(sF81) )
| ~ spl83_11 ),
inference(avatar_component_clause,[],[f2999]) ).
tff(f3002,plain,
spl83_11,
inference(avatar_split_clause,[],[f2926,f2999]) ).
tff(f3004,definition,
( spl83_12
<=> ( 'of_nat$'('to_nat$'('least$'('uu$'))) = 'of_nat$'('to_nat$'('j$')) ) ),
introduced(definition,[new_symbols(definition,[spl83_12])],[avatar_definition]) ).
tff(f3006,plain,
( ( 'of_nat$'('to_nat$'('least$'('uu$'))) = 'of_nat$'('to_nat$'('j$')) )
| ~ spl83_12 ),
inference(avatar_component_clause,[],[f3004]) ).
tff(f3007,plain,
spl83_12,
inference(avatar_split_clause,[],[f2090,f3004]) ).
tff(f3032,plain,
! [X0: 'Cols$'] :
( ( 'zero$' != 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) )
| ~ 'fun_app$'('uua$',X0) ),
inference(forward_demodulation,[],[f2450,f2722]) ).
tff(f3034,definition,
( spl83_16
<=> ( 'least$'('uu$') = sF77 ) ),
introduced(definition,[new_symbols(definition,[spl83_16])],[avatar_definition]) ).
tff(f3036,plain,
( ( 'least$'('uu$') = sF77 )
| ~ spl83_16 ),
inference(avatar_component_clause,[],[f3034]) ).
tff(f3037,plain,
spl83_16,
inference(avatar_split_clause,[],[f2917,f3034]) ).
tff(f3045,definition,
( spl83_18
<=> ( 'to_nat$'(sF77) = sF78 ) ),
introduced(definition,[new_symbols(definition,[spl83_18])],[avatar_definition]) ).
tff(f3047,plain,
( ( 'to_nat$'(sF77) = sF78 )
| ~ spl83_18 ),
inference(avatar_component_clause,[],[f3045]) ).
tff(f3048,plain,
spl83_18,
inference(avatar_split_clause,[],[f2919,f3045]) ).
tff(f3056,definition,
( spl83_20
<=> ( 'least$'('uua$') = sF80 ) ),
introduced(definition,[new_symbols(definition,[spl83_20])],[avatar_definition]) ).
tff(f3058,plain,
( ( 'least$'('uua$') = sF80 )
| ~ spl83_20 ),
inference(avatar_component_clause,[],[f3056]) ).
tff(f3059,plain,
spl83_20,
inference(avatar_split_clause,[],[f2923,f3056]) ).
tff(f3060,plain,
! [X0: 'Cols$'] :
( 'fun_app$'('uua$',X0)
| ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) ) ),
inference(forward_demodulation,[],[f2449,f2722]) ).
tff(f3063,plain,
! [X0: 'Cols$'] :
( 'fun_app$'('uu$',X0)
| ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) ) ),
inference(forward_subsumption_resolution,[],[f2979,f2230]) ).
tff(f3065,definition,
( spl83_21
<=> ( 'one$a' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),'j$') ) ),
introduced(definition,[new_symbols(definition,[spl83_21])],[avatar_definition]) ).
tff(f3067,plain,
( ( 'one$a' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),'j$') )
| ~ spl83_21 ),
inference(avatar_component_clause,[],[f3065]) ).
tff(f3068,plain,
spl83_21,
inference(avatar_split_clause,[],[f2986,f3065]) ).
tff(f3072,plain,
( ( 'of_nat$'('to_nat$'('j$')) = 'of_nat$'('to_nat$'(sF77)) )
| ~ spl83_12
| ~ spl83_16 ),
inference(forward_demodulation,[],[f3006,f3036]) ).
tff(f3084,plain,
( ( 'of_nat$'('to_nat$'('j$')) = 'of_nat$'(sF78) )
| ~ spl83_12
| ~ spl83_16
| ~ spl83_18 ),
inference(forward_demodulation,[],[f3072,f3047]) ).
tff(f3086,plain,
( ( 'of_nat$'('to_nat$'('j$')) = sF79 )
| ~ spl83_8
| ~ spl83_12
| ~ spl83_16
| ~ spl83_18 ),
inference(forward_demodulation,[],[f3084,f2984]) ).
tff(f3093,definition,
( spl83_25
<=> ( 'of_nat$'('to_nat$'('j$')) = sF79 ) ),
introduced(definition,[new_symbols(definition,[spl83_25])],[avatar_definition]) ).
tff(f3095,plain,
( ( 'of_nat$'('to_nat$'('j$')) = sF79 )
| ~ spl83_25 ),
inference(avatar_component_clause,[],[f3093]) ).
tff(f3096,plain,
( spl83_25
| ~ spl83_8
| ~ spl83_12
| ~ spl83_16
| ~ spl83_18 ),
inference(avatar_split_clause,[],[f3086,f3045,f3034,f3004,f2982,f3093]) ).
tff(f3141,plain,
( ! [X0: 'Cols$'] :
( ~ 'fun_app$'('uu$',X0)
| 'fun_app$'('fun_app$c'('less_eq$',sF77),X0) )
| ~ spl83_16 ),
inference(constrained_superposition,[],[f2740,f3036]) ).
tff(f3143,plain,
( ! [X0: 'Cols$'] :
( 'fun_app$'('fun_app$c'('less_eq$',sF77),X0)
| ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) ) )
| ~ spl83_16 ),
inference(forward_literal_rewriting,[],[f3141,f3063]) ).
tff(f3148,plain,
( ! [X0: 'Cols$'] :
( ( 'of_nat$'('to_nat$'(X0)) != 'of_nat$'(sF78) )
| ( sF77 = X0 ) )
| ~ spl83_18 ),
inference(constrained_superposition,[],[f2226,f3047]) ).
tff(f3149,plain,
( ! [X0: 'Cols$'] :
( ( 'of_nat$'('to_nat$'(X0)) != sF79 )
| ( sF77 = X0 ) )
| ~ spl83_8
| ~ spl83_18 ),
inference(forward_demodulation,[],[f3148,f2984]) ).
tff(f3152,plain,
( ! [X0: 'Cols$'] :
( ~ 'fun_app$'('fun_app$c'('less_eq$',X0),sF80)
| ~ $less('of_nat$'(sF81),'of_nat$'('to_nat$'(X0))) )
| ~ spl83_5 ),
inference(constrained_superposition,[],[f2089,f2964]) ).
tff(f3154,plain,
( ! [X0: 'Cols$'] :
( ~ 'fun_app$'('fun_app$c'('less_eq$',sF80),X0)
| ~ $less('of_nat$'('to_nat$'(X0)),'of_nat$'(sF81)) )
| ~ spl83_5 ),
inference(constrained_superposition,[],[f2089,f2964]) ).
tff(f3156,plain,
( ! [X0: 'Cols$'] :
( ~ $less(sF82,'of_nat$'('to_nat$'(X0)))
| ~ 'fun_app$'('fun_app$c'('less_eq$',X0),sF80) )
| ~ spl83_5
| ~ spl83_11 ),
inference(forward_demodulation,[],[f3152,f3001]) ).
tff(f3157,plain,
( ! [X0: 'Cols$'] :
( ~ $less('of_nat$'('to_nat$'(X0)),sF82)
| ~ 'fun_app$'('fun_app$c'('less_eq$',sF80),X0) )
| ~ spl83_5
| ~ spl83_11 ),
inference(forward_demodulation,[],[f3154,f3001]) ).
tff(f3160,plain,
( ! [X0: 'Cols$'] :
( 'fun_app$'('fun_app$c'('less_eq$',sF80),X0)
| ~ 'fun_app$'('uua$',X0) )
| ~ spl83_20 ),
inference(constrained_superposition,[],[f2740,f3058]) ).
tff(f3163,plain,
( ! [X0: 'Cols$'] :
( 'fun_app$'('fun_app$c'('less_eq$',sF80),X0)
| ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) ) )
| ~ spl83_20 ),
inference(forward_literal_rewriting,[],[f3160,f3060]) ).
tff(f3329,definition,
( spl83_45
<=> $less(sF82,sF79) ),
introduced(definition,[new_symbols(definition,[spl83_45])],[avatar_definition]) ).
tff(f3351,definition,
( spl83_48
<=> $less(sF79,sF82) ),
introduced(definition,[new_symbols(definition,[spl83_48])],[avatar_definition]) ).
tff(f3364,plain,
( ( sF79 != sF79 )
| ( 'j$' = sF77 )
| ~ spl83_8
| ~ spl83_18
| ~ spl83_25 ),
inference(constrained_superposition,[],[f3149,f3095]) ).
tff(f3365,plain,
( ~ 'fun_app$'('fun_app$c'('less_eq$','j$'),sF80)
| ~ $less(sF82,sF79)
| ~ spl83_5
| ~ spl83_11
| ~ spl83_25 ),
inference(constrained_superposition,[],[f3156,f3095]) ).
tff(f3366,plain,
( ~ $less(sF79,sF82)
| ~ 'fun_app$'('fun_app$c'('less_eq$',sF80),'j$')
| ~ spl83_5
| ~ spl83_11
| ~ spl83_25 ),
inference(constrained_superposition,[],[f3157,f3095]) ).
tff(f3375,plain,
( ( 'j$' = sF77 )
| ~ spl83_8
| ~ spl83_18
| ~ spl83_25 ),
inference(trivial_inequality_removal,[],[f3364]) ).
tff(f3379,definition,
( spl83_50
<=> ( 'j$' = sF77 ) ),
introduced(definition,[new_symbols(definition,[spl83_50])],[avatar_definition]) ).
tff(f3381,plain,
( ( 'j$' = sF77 )
| ~ spl83_50 ),
inference(avatar_component_clause,[],[f3379]) ).
tff(f3382,plain,
( spl83_50
| ~ spl83_8
| ~ spl83_18
| ~ spl83_25 ),
inference(avatar_split_clause,[],[f3375,f3093,f3045,f2982,f3379]) ).
tff(f3384,definition,
( spl83_51
<=> 'fun_app$'('fun_app$c'('less_eq$','j$'),sF80) ),
introduced(definition,[new_symbols(definition,[spl83_51])],[avatar_definition]) ).
tff(f3386,plain,
( ~ 'fun_app$'('fun_app$c'('less_eq$','j$'),sF80)
| spl83_51 ),
inference(avatar_component_clause,[],[f3384]) ).
tff(f3387,plain,
( ~ spl83_45
| ~ spl83_51
| ~ spl83_5
| ~ spl83_11
| ~ spl83_25 ),
inference(avatar_split_clause,[],[f3365,f3093,f2999,f2962,f3384,f3329]) ).
tff(f3390,definition,
( spl83_52
<=> 'fun_app$'('fun_app$c'('less_eq$',sF80),'j$') ),
introduced(definition,[new_symbols(definition,[spl83_52])],[avatar_definition]) ).
tff(f3392,plain,
( ~ 'fun_app$'('fun_app$c'('less_eq$',sF80),'j$')
| spl83_52 ),
inference(avatar_component_clause,[],[f3390]) ).
tff(f3393,plain,
( ~ spl83_48
| ~ spl83_52
| ~ spl83_5
| ~ spl83_11
| ~ spl83_25 ),
inference(avatar_split_clause,[],[f3366,f3093,f2999,f2962,f3390,f3351]) ).
tff(f3401,plain,
( ! [X0: 'Cols$'] :
( 'fun_app$'('fun_app$c'('less_eq$','j$'),X0)
| ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) ) )
| ~ spl83_16
| ~ spl83_50 ),
inference(backward_demodulation,[],[f3143,f3381]) ).
tff(f3447,plain,
! [X0: 'Cols$'] :
( ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) )
| 'fun_app$'('uua$','least$'('uua$')) ),
inference(resolution,[],[f3060,f2460]) ).
tff(f3453,plain,
( ! [X0: 'Cols$'] :
( 'fun_app$'('uua$',sF80)
| ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) ) )
| ~ spl83_20 ),
inference(forward_demodulation,[],[f3447,f3058]) ).
tff(f3462,plain,
( ! [X0: 'Cols$'] :
( ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) )
| ( 'zero$' != 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),sF80) ) )
| ~ spl83_20 ),
inference(forward_literal_rewriting,[],[f3453,f3032]) ).
tff(f3470,definition,
( spl83_57
<=> ! [X0: 'Cols$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) ) ),
introduced(definition,[new_symbols(definition,[spl83_57])],[avatar_definition]) ).
tff(f3471,plain,
( ! [X0: 'Cols$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),X0) )
| ~ spl83_57 ),
inference(avatar_component_clause,[],[f3470]) ).
tff(f3474,definition,
( spl83_58
<=> ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),sF80) ) ),
introduced(definition,[new_symbols(definition,[spl83_58])],[avatar_definition]) ).
tff(f3476,plain,
( ( 'zero$' != 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),sF80) )
| spl83_58 ),
inference(avatar_component_clause,[],[f3474]) ).
tff(f3477,plain,
( spl83_57
| ~ spl83_58
| ~ spl83_20 ),
inference(avatar_split_clause,[],[f3462,f3056,f3474,f3470]) ).
tff(f3496,plain,
( ( 'zero$' = 'one$a' )
| ~ spl83_21
| ~ spl83_57 ),
inference(backward_demodulation,[],[f3067,f3471]) ).
tff(f3503,plain,
( $false
| spl83_9
| ~ spl83_21
| ~ spl83_57 ),
inference(forward_subsumption_resolution,[],[f3496,f2990]) ).
tff(f3504,plain,
( spl83_9
| ~ spl83_21
| ~ spl83_57 ),
inference(avatar_contradiction_clause,[],[f3503]) ).
tff(f4564,plain,
( ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),'j$') )
| ~ spl83_20
| spl83_52 ),
inference(resolution,[],[f3163,f3392]) ).
tff(f4598,definition,
( spl83_105
<=> ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),'j$') ) ),
introduced(definition,[new_symbols(definition,[spl83_105])],[avatar_definition]) ).
tff(f4601,plain,
( spl83_105
| ~ spl83_20
| spl83_52 ),
inference(avatar_split_clause,[],[f4564,f3390,f3056,f4598]) ).
tff(f4625,plain,
( ( 'zero$' = 'fun_app$a'('vec_nth$'('fun_app$f'('uuy$'('a$'),'i$')),sF80) )
| ~ spl83_16
| ~ spl83_50
| spl83_51 ),
inference(resolution,[],[f3401,f3386]) ).
tff(f4657,plain,
( $false
| ~ spl83_16
| ~ spl83_50
| spl83_51
| spl83_58 ),
inference(forward_subsumption_resolution,[],[f4625,f3476]) ).
tff(f4658,plain,
( ~ spl83_16
| ~ spl83_50
| spl83_51
| spl83_58 ),
inference(avatar_contradiction_clause,[],[f4657]) ).
tff(f4672,plain,
$false,
inference(avatar_smt_refutation,[],[f4658,f4601,f3504,f3477,f3393,f3387,f3382,f3096,f3068,f3059,f3048,f3037,f3007,f3002,f2991,f2985,f2972,f2965]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP347_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.37 % Computer : n006.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Sun Sep 27 12:54:55 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 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
% 5.16/1.84 % (2953558)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.16/1.84 % (2953614)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2608273845:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.16/1.84 % (2953612)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1740005643:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.16/1.84 % (2953615)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1830929485:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.16/1.84 % (2953616)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3377727377:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.16/1.84 % (2953613)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1955174737:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.16/1.84 % (2953616)Instruction limit reached!
% 5.16/1.84 % (2953616)------------------------------
% 5.16/1.84 % (2953616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.84 % (2953616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.16/1.84 % (2953616)CaDiCaL version: 2.1.3
% 5.16/1.84 % (2953616)Termination reason: Instruction limit
% 5.16/1.84 % (2953616)Termination phase: Property scanning
% 5.16/1.84 % (2953616)Time elapsed: 0.005 s
% 5.16/1.84 % (2953616)Peak memory usage: 86 MB
% 5.16/1.84 % (2953616)Instructions burned: 4 (million)
% 5.16/1.84 % (2953615)Instruction limit reached!
% 5.16/1.84 % (2953615)------------------------------
% 5.16/1.84 % (2953615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.84 % (2953615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.16/1.84 % (2953615)CaDiCaL version: 2.1.3
% 5.16/1.84 % (2953615)Termination reason: Instruction limit
% 5.16/1.84 % (2953615)Termination phase: Property scanning
% 5.16/1.84 % (2953615)Time elapsed: 0.008 s
% 5.16/1.84 % (2953615)Peak memory usage: 86 MB
% 5.16/1.84 % (2953615)Instructions burned: 7 (million)
% 5.16/1.84 % (2953612)Instruction limit reached!
% 5.16/1.84 % (2953612)------------------------------
% 5.16/1.84 % (2953612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.84 % (2953612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.16/1.84 % (2953612)CaDiCaL version: 2.1.3
% 5.16/1.84 % (2953612)Termination reason: Instruction limit
% 5.16/1.84 % (2953612)Termination phase: Property scanning
% 5.16/1.84 % (2953612)Time elapsed: 0.012 s
% 5.16/1.84 % (2953612)Peak memory usage: 86 MB
% 5.16/1.84 % (2953612)Instructions burned: 12 (million)
% 5.16/1.84 % (2953617)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1595120804:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.16/1.84 % (2953619)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1857912091:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.16/1.84 % (2953619)Instruction limit reached!
% 5.16/1.84 % (2953619)------------------------------
% 5.16/1.84 % (2953619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.84 % (2953619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.16/1.84 % (2953619)CaDiCaL version: 2.1.3
% 5.16/1.84 % (2953619)Termination reason: Instruction limit
% 5.16/1.84 % (2953619)Termination phase: Preprocessing 3
% 5.16/1.84 % (2953619)Time elapsed: 0.025 s
% 5.16/1.84 % (2953619)Peak memory usage: 88 MB
% 5.16/1.84 % (2953619)Instructions burned: 33 (million)
% 5.16/1.84 % (2953614)Instruction limit reached!
% 5.16/1.84 % (2953614)------------------------------
% 5.16/1.84 % (2953614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.84 % (2953614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.16/1.84 % (2953614)CaDiCaL version: 2.1.3
% 5.16/1.84 % (2953614)Termination reason: Instruction limit
% 5.16/1.84 % (2953614)Termination phase: Saturation
% 5.16/1.84 % (2953614)Time elapsed: 0.135 s
% 5.16/1.84 % (2953614)Peak memory usage: 120 MB
% 5.16/1.84 % (2953614)Instructions burned: 202 (million)
% 5.16/1.84 % (2953617)Instruction limit reached!
% 5.16/1.84 % (2953617)------------------------------
% 5.16/1.84 % (2953617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.16/1.84 % (2953617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.11 % (2953617)CaDiCaL version: 2.1.3
% 7.93/2.11 % (2953617)Termination reason: Instruction limit
% 7.93/2.11 % (2953617)Termination phase: Property scanning
% 7.93/2.11 % (2953617)Time elapsed: 0.047 s
% 7.93/2.11 % (2953617)Peak memory usage: 88 MB
% 7.93/2.11 % (2953617)Instructions burned: 47 (million)
% 7.93/2.11 % (2953632)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3547769513:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2996 on theBenchmark for (2996ds/14Mi)
% 7.93/2.11 % (2953632)Instruction limit reached!
% 7.93/2.11 % (2953632)------------------------------
% 7.93/2.11 % (2953632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.11 % (2953632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.11 % (2953632)CaDiCaL version: 2.1.3
% 7.93/2.11 % (2953632)Termination reason: Instruction limit
% 7.93/2.11 % (2953632)Termination phase: Preprocessing 1
% 7.93/2.11 % (2953632)Time elapsed: 0.013 s
% 7.93/2.11 % (2953632)Peak memory usage: 86 MB
% 7.93/2.11 % (2953632)Instructions burned: 14 (million)
% 7.93/2.11 % (2953633)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=2950642019:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2996 on theBenchmark for (2996ds/29Mi)
% 7.93/2.11 % (2953634)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3281153808:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi)
% 7.93/2.11 % (2953638)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=856923776:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 7.93/2.11 % (2953634)Instruction limit reached!
% 7.93/2.11 % (2953634)------------------------------
% 7.93/2.11 % (2953634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.11 % (2953634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.11 % (2953634)CaDiCaL version: 2.1.3
% 7.93/2.11 % (2953634)Termination reason: Instruction limit
% 7.93/2.11 % (2953634)Termination phase: Naming
% 7.93/2.11 % (2953634)Time elapsed: 0.010 s
% 7.93/2.11 % (2953634)Peak memory usage: 87 MB
% 7.93/2.11 % (2953634)Instructions burned: 16 (million)
% 7.93/2.11 % (2953633)Instruction limit reached!
% 7.93/2.11 % (2953633)------------------------------
% 7.93/2.11 % (2953633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.11 % (2953633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.11 % (2953633)CaDiCaL version: 2.1.3
% 7.93/2.11 % (2953633)Termination reason: Instruction limit
% 7.93/2.11 % (2953633)Termination phase: Preprocessing 3
% 7.93/2.11 % (2953633)Time elapsed: 0.021 s
% 7.93/2.11 % (2953633)Peak memory usage: 88 MB
% 7.93/2.11 % (2953633)Instructions burned: 32 (million)
% 7.93/2.11 % (2953638)Instruction limit reached!
% 7.93/2.11 % (2953638)------------------------------
% 7.93/2.11 % (2953638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.11 % (2953638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.11 % (2953638)CaDiCaL version: 2.1.3
% 7.93/2.11 % (2953638)Termination reason: Instruction limit
% 7.93/2.11 % (2953638)Termination phase: Preprocessing 3
% 7.93/2.11 % (2953638)Time elapsed: 0.025 s
% 7.93/2.11 % (2953638)Peak memory usage: 87 MB
% 7.93/2.11 % (2953638)Instructions burned: 24 (million)
% 7.93/2.11 % (2953641)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2673156223:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 7.93/2.11 % (2953639)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=14082274:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 7.93/2.11 % (2953613)Instruction limit reached!
% 7.93/2.11 % (2953613)------------------------------
% 7.93/2.11 % (2953613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.11 % (2953613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.11 % (2953613)CaDiCaL version: 2.1.3
% 7.93/2.11 % (2953613)Termination reason: Instruction limit
% 7.93/2.11 % (2953613)Termination phase: Saturation
% 7.93/2.11 % (2953613)Time elapsed: 0.347 s
% 7.93/2.11 % (2953613)Peak memory usage: 119 MB
% 7.93/2.11 % (2953613)Instructions burned: 307 (million)
% 7.93/2.11 % (2953639)Instruction limit reached!
% 7.93/2.11 % (2953639)------------------------------
% 9.03/2.35 % (2953639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.03/2.35 % (2953639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.03/2.35 % (2953639)CaDiCaL version: 2.1.3
% 9.03/2.35 % (2953639)Termination reason: Instruction limit
% 9.03/2.35 % (2953639)Termination phase: Preprocessing 3
% 9.03/2.35 % (2953639)Time elapsed: 0.028 s
% 9.03/2.35 % (2953639)Peak memory usage: 87 MB
% 9.03/2.35 % (2953639)Instructions burned: 27 (million)
% 9.03/2.35 % (2953641)Instruction limit reached!
% 9.03/2.35 % (2953641)------------------------------
% 9.03/2.35 % (2953641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.03/2.35 % (2953641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.03/2.35 % (2953641)CaDiCaL version: 2.1.3
% 9.03/2.35 % (2953641)Termination reason: Instruction limit
% 9.03/2.35 % (2953641)Termination phase: Saturation
% 9.03/2.35 % (2953641)Time elapsed: 0.079 s
% 9.03/2.35 % (2953641)Peak memory usage: 90 MB
% 9.03/2.35 % (2953641)Instructions burned: 85 (million)
% 9.03/2.35 % (2953653)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3368116867:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 9.03/2.35 % (2953649)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=767412518:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi)
% 9.03/2.35 % (2953649)Instruction limit reached!
% 9.03/2.35 % (2953649)------------------------------
% 9.03/2.35 % (2953649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.03/2.35 % (2953649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.03/2.35 % (2953649)CaDiCaL version: 2.1.3
% 9.03/2.35 % (2953649)Termination reason: Instruction limit
% 9.03/2.35 % (2953649)Termination phase: Property scanning
% 9.03/2.35 % (2953649)Time elapsed: 0.005 s
% 9.03/2.35 % (2953649)Peak memory usage: 86 MB
% 9.03/2.35 % (2953649)Instructions burned: 3 (million)
% 9.03/2.35 % (2953654)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1722300018:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 9.03/2.35 % (2953654)Instruction limit reached!
% 9.03/2.35 % (2953654)------------------------------
% 9.03/2.35 % (2953654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.03/2.35 % (2953654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.03/2.35 % (2953654)CaDiCaL version: 2.1.3
% 9.03/2.35 % (2953654)Termination reason: Instruction limit
% 9.03/2.35 % (2953654)Termination phase: Property scanning
% 9.03/2.35 % (2953654)Time elapsed: 0.005 s
% 9.03/2.35 % (2953654)Peak memory usage: 86 MB
% 9.03/2.35 % (2953654)Instructions burned: 4 (million)
% 9.03/2.35 % (2953655)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2237721345:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 9.03/2.35 % (2953653)Instruction limit reached!
% 9.03/2.35 % (2953653)------------------------------
% 9.03/2.35 % (2953653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.03/2.35 % (2953653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.03/2.35 % (2953653)CaDiCaL version: 2.1.3
% 9.03/2.35 % (2953653)Termination reason: Instruction limit
% 9.03/2.35 % (2953653)Termination phase: Saturation
% 9.03/2.35 % (2953653)Time elapsed: 0.112 s
% 9.03/2.35 % (2953653)Peak memory usage: 92 MB
% 9.03/2.35 % (2953653)Instructions burned: 182 (million)
% 9.03/2.35 % (2953658)lrs+10_1_thi=all:si=on:fd=off:random_seed=2869901938:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 9.03/2.35 % (2953659)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=543713624:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 9.03/2.35 % (2953659)Instruction limit reached!
% 9.03/2.35 % (2953659)------------------------------
% 9.03/2.35 % (2953659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.03/2.35 % (2953659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.03/2.35 % (2953659)CaDiCaL version: 2.1.3
% 9.03/2.35 % (2953659)Termination reason: Instruction limit
% 9.03/2.35 % (2953659)Termination phase: shuffling
% 9.03/2.35 % (2953659)Time elapsed: 0.008 s
% 9.03/2.35 % (2953659)Peak memory usage: 85 MB
% 9.03/2.35 % (2953659)Instructions burned: 8 (million)
% 10.89/2.70 % (2953658)Instruction limit reached!
% 10.89/2.70 % (2953658)------------------------------
% 10.89/2.70 % (2953658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.70 % (2953658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.70 % (2953658)CaDiCaL version: 2.1.3
% 10.89/2.70 % (2953658)Termination reason: Instruction limit
% 10.89/2.70 % (2953658)Termination phase: Property scanning
% 10.89/2.70 % (2953658)Time elapsed: 0.051 s
% 10.89/2.70 % (2953658)Peak memory usage: 88 MB
% 10.89/2.70 % (2953658)Instructions burned: 53 (million)
% 10.89/2.70 % (2953655)Instruction limit reached!
% 10.89/2.70 % (2953655)------------------------------
% 10.89/2.70 % (2953655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.70 % (2953655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.70 % (2953655)CaDiCaL version: 2.1.3
% 10.89/2.70 % (2953655)Termination reason: Instruction limit
% 10.89/2.70 % (2953655)Termination phase: Saturation
% 10.89/2.70 % (2953655)Time elapsed: 0.096 s
% 10.89/2.70 % (2953655)Peak memory usage: 116 MB
% 10.89/2.70 % (2953655)Instructions burned: 66 (million)
% 10.89/2.71 % (2953660)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=898326433:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi)
% 10.89/2.71 % (2953660)Instruction limit reached!
% 10.89/2.71 % (2953660)------------------------------
% 10.89/2.71 % (2953660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.71 % (2953660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.71 % (2953660)CaDiCaL version: 2.1.3
% 10.89/2.71 % (2953660)Termination reason: Instruction limit
% 10.89/2.71 % (2953660)Termination phase: shuffling
% 10.89/2.71 % (2953660)Time elapsed: 0.004 s
% 10.89/2.71 % (2953660)Peak memory usage: 85 MB
% 10.89/2.71 % (2953660)Instructions burned: 2 (million)
% 10.89/2.71 % (2953663)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2521572251:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 10.89/2.71 % (2953663)Instruction limit reached!
% 10.89/2.71 % (2953663)------------------------------
% 10.89/2.71 % (2953663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.71 % (2953663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.71 % (2953663)CaDiCaL version: 2.1.3
% 10.89/2.71 % (2953663)Termination reason: Instruction limit
% 10.89/2.71 % (2953663)Termination phase: shuffling
% 10.89/2.71 % (2953663)Time elapsed: 0.004 s
% 10.89/2.71 % (2953663)Peak memory usage: 85 MB
% 10.89/2.71 % (2953663)Instructions burned: 2 (million)
% 10.89/2.71 % (2953670)dis+10_1_si=on:random_seed=3778396934:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 10.89/2.71 % (2953667)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1547613516:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 10.89/2.71 % (2953670)Instruction limit reached!
% 10.89/2.71 % (2953670)------------------------------
% 10.89/2.71 % (2953670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.71 % (2953670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.71 % (2953670)CaDiCaL version: 2.1.3
% 10.89/2.71 % (2953670)Termination reason: Instruction limit
% 10.89/2.71 % (2953670)Termination phase: Property scanning
% 10.89/2.71 % (2953670)Time elapsed: 0.006 s
% 10.89/2.71 % (2953670)Peak memory usage: 86 MB
% 10.89/2.71 % (2953670)Instructions burned: 11 (million)
% 10.89/2.71 % (2953674)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=693458793:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 10.89/2.71 % (2953674)Instruction limit reached!
% 10.89/2.71 % (2953674)------------------------------
% 10.89/2.71 % (2953674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.71 % (2953674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.71 % (2953674)CaDiCaL version: 2.1.3
% 10.89/2.71 % (2953674)Termination reason: Instruction limit
% 10.89/2.71 % (2953674)Termination phase: Preprocessing 3
% 10.89/2.71 % (2953674)Time elapsed: 0.027 s
% 10.89/2.71 % (2953674)Peak memory usage: 88 MB
% 10.89/2.71 % (2953674)Instructions burned: 26 (million)
% 10.89/2.71 % (2953675)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1310674335: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_2990 on theBenchmark for (2990ds/35Mi)
% 14.90/3.07 % (2953676)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2422392694:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 14.90/3.07 % (2953678)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1302726494:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 14.90/3.07 % (2953676)Instruction limit reached!
% 14.90/3.07 % (2953676)------------------------------
% 14.90/3.07 % (2953676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.07 % (2953676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.07 % (2953676)CaDiCaL version: 2.1.3
% 14.90/3.07 % (2953676)Termination reason: Instruction limit
% 14.90/3.07 % (2953676)Termination phase: Property scanning
% 14.90/3.07 % (2953676)Time elapsed: 0.004 s
% 14.90/3.07 % (2953676)Peak memory usage: 86 MB
% 14.90/3.07 % (2953676)Instructions burned: 3 (million)
% 14.90/3.07 % (2953678)Instruction limit reached!
% 14.90/3.07 % (2953678)------------------------------
% 14.90/3.07 % (2953678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.07 % (2953678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.07 % (2953678)CaDiCaL version: 2.1.3
% 14.90/3.07 % (2953678)Termination reason: Instruction limit
% 14.90/3.07 % (2953678)Termination phase: Property scanning
% 14.90/3.07 % (2953678)Time elapsed: 0.008 s
% 14.90/3.07 % (2953678)Peak memory usage: 86 MB
% 14.90/3.07 % (2953678)Instructions burned: 8 (million)
% 14.90/3.07 % (2953667)Instruction limit reached!
% 14.90/3.07 % (2953667)------------------------------
% 14.90/3.07 % (2953667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.07 % (2953667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.07 % (2953667)CaDiCaL version: 2.1.3
% 14.90/3.07 % (2953667)Termination reason: Instruction limit
% 14.90/3.07 % (2953667)Termination phase: Saturation
% 14.90/3.07 % (2953667)Time elapsed: 0.168 s
% 14.90/3.07 % (2953667)Peak memory usage: 119 MB
% 14.90/3.07 % (2953667)Instructions burned: 129 (million)
% 14.90/3.07 % (2953675)Instruction limit reached!
% 14.90/3.07 % (2953675)------------------------------
% 14.90/3.07 % (2953675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.07 % (2953675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.07 % (2953675)CaDiCaL version: 2.1.3
% 14.90/3.07 % (2953675)Termination reason: Instruction limit
% 14.90/3.07 % (2953675)Termination phase: Property scanning
% 14.90/3.07 % (2953675)Time elapsed: 0.040 s
% 14.90/3.07 % (2953675)Peak memory usage: 88 MB
% 14.90/3.07 % (2953675)Instructions burned: 39 (million)
% 14.90/3.07 % (2953683)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=4104277753:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 14.90/3.07 % (2953680)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=534604261:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi)
% 14.90/3.07 % (2953683)Instruction limit reached!
% 14.90/3.07 % (2953683)------------------------------
% 14.90/3.07 % (2953683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.07 % (2953683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.07 % (2953683)CaDiCaL version: 2.1.3
% 14.90/3.07 % (2953683)Termination reason: Instruction limit
% 14.90/3.07 % (2953683)Termination phase: Property scanning
% 14.90/3.07 % (2953683)Time elapsed: 0.007 s
% 14.90/3.07 % (2953683)Peak memory usage: 85 MB
% 14.90/3.07 % (2953683)Instructions burned: 15 (million)
% 14.90/3.07 % (2953690)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=271707514:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi)
% 14.90/3.07 % (2953686)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1275110869:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 14.90/3.07 % (2953690)Instruction limit reached!
% 14.90/3.07 % (2953690)------------------------------
% 14.90/3.07 % (2953690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.07 % (2953690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.07 % (2953690)CaDiCaL version: 2.1.3
% 14.90/3.07 % (2953690)Termination reason: Instruction limit
% 14.90/3.07 % (2953690)Termination phase: Preprocessing 1
% 16.66/3.48 % (2953690)Time elapsed: 0.006 s
% 16.66/3.48 % (2953690)Peak memory usage: 85 MB
% 16.66/3.48 % (2953690)Instructions burned: 12 (million)
% 16.66/3.48 % (2953697)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1030626413:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi)
% 16.66/3.48 % (2953692)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=1118054132:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 16.66/3.48 % (2953691)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3311176953:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi)
% 16.66/3.48 % (2953694)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=3831485604:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 16.66/3.48 % (2953697)Instruction limit reached!
% 16.66/3.48 % (2953697)------------------------------
% 16.66/3.48 % (2953697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.66/3.48 % (2953697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.66/3.48 % (2953697)CaDiCaL version: 2.1.3
% 16.66/3.48 % (2953697)Termination reason: Instruction limit
% 16.66/3.48 % (2953697)Termination phase: Saturation
% 16.66/3.48 % (2953697)Time elapsed: 0.086 s
% 16.66/3.48 % (2953697)Peak memory usage: 115 MB
% 16.66/3.48 % (2953697)Instructions burned: 130 (million)
% 16.66/3.48 % (2953692)Instruction limit reached!
% 16.66/3.48 % (2953692)------------------------------
% 16.66/3.48 % (2953692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.66/3.48 % (2953692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.66/3.48 % (2953692)CaDiCaL version: 2.1.3
% 16.66/3.48 % (2953692)Termination reason: Instruction limit
% 16.66/3.48 % (2953692)Termination phase: Saturation
% 16.66/3.48 % (2953692)Time elapsed: 0.071 s
% 16.66/3.48 % (2953692)Peak memory usage: 91 MB
% 16.66/3.48 % (2953692)Instructions burned: 75 (million)
% 16.66/3.48 % (2953691)Instruction limit reached!
% 16.66/3.48 % (2953691)------------------------------
% 16.66/3.48 % (2953691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.66/3.48 % (2953691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.66/3.48 % (2953691)CaDiCaL version: 2.1.3
% 16.66/3.48 % (2953691)Termination reason: Instruction limit
% 16.66/3.48 % (2953691)Termination phase: Saturation
% 16.66/3.48 % (2953691)Time elapsed: 0.122 s
% 16.66/3.48 % (2953691)Peak memory usage: 130 MB
% 16.66/3.48 % (2953691)Instructions burned: 71 (million)
% 16.66/3.48 % (2953680)Instruction limit reached!
% 16.66/3.48 % (2953680)------------------------------
% 16.66/3.48 % (2953680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.66/3.48 % (2953680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.66/3.48 % (2953680)CaDiCaL version: 2.1.3
% 16.66/3.48 % (2953680)Termination reason: Instruction limit
% 16.66/3.48 % (2953680)Termination phase: Saturation
% 16.66/3.48 % (2953680)Time elapsed: 0.342 s
% 16.66/3.48 % (2953680)Peak memory usage: 96 MB
% 16.66/3.48 % (2953680)Instructions burned: 370 (million)
% 16.66/3.48 % (2953686)Instruction limit reached!
% 16.66/3.48 % (2953686)------------------------------
% 16.66/3.48 % (2953686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.66/3.48 % (2953686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.66/3.48 % (2953686)CaDiCaL version: 2.1.3
% 16.66/3.48 % (2953686)Termination reason: Instruction limit
% 16.66/3.48 % (2953686)Termination phase: Saturation
% 16.66/3.48 % (2953686)Time elapsed: 0.235 s
% 16.66/3.48 % (2953686)Peak memory usage: 119 MB
% 16.66/3.48 % (2953686)Instructions burned: 226 (million)
% 16.66/3.48 % (2953702)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3909639052:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 16.66/3.48 % (2953708)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3865269947:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 16.66/3.48 % (2953707)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3556032910:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi)
% 16.66/3.48 % (2953694)Instruction limit reached!
% 16.66/3.48 % (2953694)------------------------------
% 18.63/3.94 % (2953694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/3.94 % (2953694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/3.94 % (2953694)CaDiCaL version: 2.1.3
% 18.63/3.94 % (2953694)Termination reason: Instruction limit
% 18.63/3.94 % (2953694)Termination phase: Saturation
% 18.63/3.94 % (2953694)Time elapsed: 0.318 s
% 18.63/3.94 % (2953694)Peak memory usage: 93 MB
% 18.63/3.94 % (2953694)Instructions burned: 294 (million)
% 18.63/3.94 % (2953707)Instruction limit reached!
% 18.63/3.94 % (2953707)------------------------------
% 18.63/3.94 % (2953707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/3.94 % (2953707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/3.94 % (2953707)CaDiCaL version: 2.1.3
% 18.63/3.94 % (2953707)Termination reason: Instruction limit
% 18.63/3.94 % (2953707)Termination phase: Preprocessing 3
% 18.63/3.94 % (2953707)Time elapsed: 0.036 s
% 18.63/3.94 % (2953707)Peak memory usage: 87 MB
% 18.63/3.94 % (2953707)Instructions burned: 40 (million)
% 18.63/3.94 % (2953709)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=353070813:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 18.63/3.94 % (2953702)Instruction limit reached!
% 18.63/3.94 % (2953702)------------------------------
% 18.63/3.94 % (2953702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/3.94 % (2953702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/3.94 % (2953702)CaDiCaL version: 2.1.3
% 18.63/3.94 % (2953702)Termination reason: Instruction limit
% 18.63/3.94 % (2953702)Termination phase: Saturation
% 18.63/3.94 % (2953702)Time elapsed: 0.195 s
% 18.63/3.94 % (2953702)Peak memory usage: 135 MB
% 18.63/3.94 % (2953702)Instructions burned: 131 (million)
% 18.63/3.94 % (2953710)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=223113099:i=131:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/131Mi)
% 18.63/3.94 % (2953708)Instruction limit reached!
% 18.63/3.94 % (2953708)------------------------------
% 18.63/3.94 % (2953708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/3.94 % (2953708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/3.94 % (2953708)CaDiCaL version: 2.1.3
% 18.63/3.94 % (2953708)Termination reason: Instruction limit
% 18.63/3.94 % (2953708)Termination phase: Saturation
% 18.63/3.94 % (2953708)Time elapsed: 0.146 s
% 18.63/3.94 % (2953708)Peak memory usage: 92 MB
% 18.63/3.94 % (2953708)Instructions burned: 307 (million)
% 18.63/3.94 % (2953711)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=668957567:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi)
% 18.63/3.94 % (2953716)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3235767300:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi)
% 18.63/3.94 % (2953715)dis+10_1_si=on:random_seed=4239097356:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi)
% 18.63/3.94 % (2953710)Instruction limit reached!
% 18.63/3.94 % (2953710)------------------------------
% 18.63/3.94 % (2953710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/3.94 % (2953710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/3.94 % (2953710)CaDiCaL version: 2.1.3
% 18.63/3.94 % (2953710)Termination reason: Instruction limit
% 18.63/3.94 % (2953710)Termination phase: Saturation
% 18.63/3.94 % (2953710)Time elapsed: 0.160 s
% 18.63/3.94 % (2953710)Peak memory usage: 119 MB
% 18.63/3.94 % (2953710)Instructions burned: 131 (million)
% 18.63/3.94 % (2953721)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1876963111:i=65:nm=16:rtra=on_2981 on theBenchmark for (2981ds/65Mi)
% 18.63/3.94 % (2953721)Instruction limit reached!
% 18.63/3.94 % (2953721)------------------------------
% 18.63/3.94 % (2953721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/3.94 % (2953721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/3.94 % (2953721)CaDiCaL version: 2.1.3
% 18.63/3.94 % (2953721)Termination reason: Instruction limit
% 18.63/3.94 % (2953721)Termination phase: Saturation
% 18.63/3.94 % (2953721)Time elapsed: 0.035 s
% 18.63/3.94 % (2953721)Peak memory usage: 90 MB
% 23.92/4.58 % (2953721)Instructions burned: 66 (million)
% 23.92/4.58 % (2953719)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3372955770:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi)
% 23.92/4.58 % (2953711)Instruction limit reached!
% 23.92/4.58 % (2953711)------------------------------
% 23.92/4.58 % (2953711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.92/4.58 % (2953711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.92/4.58 % (2953711)CaDiCaL version: 2.1.3
% 23.92/4.58 % (2953711)Termination reason: Instruction limit
% 23.92/4.58 % (2953711)Termination phase: Saturation
% 23.92/4.58 % (2953711)Time elapsed: 0.319 s
% 23.92/4.58 % (2953711)Peak memory usage: 119 MB
% 23.92/4.58 % (2953711)Instructions burned: 261 (million)
% 23.92/4.58 % (2953719)Instruction limit reached!
% 23.92/4.58 % (2953719)------------------------------
% 23.92/4.58 % (2953719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.92/4.58 % (2953719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.92/4.58 % (2953719)CaDiCaL version: 2.1.3
% 23.92/4.58 % (2953719)Termination reason: Instruction limit
% 23.92/4.58 % (2953719)Termination phase: Saturation
% 23.92/4.58 % (2953719)Time elapsed: 0.077 s
% 23.92/4.58 % (2953719)Peak memory usage: 92 MB
% 23.92/4.58 % (2953719)Instructions burned: 143 (million)
% 23.92/4.58 % (2953724)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2890234287:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi)
% 23.92/4.58 % (2953716)Instruction limit reached!
% 23.92/4.58 % (2953716)------------------------------
% 23.92/4.58 % (2953716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.92/4.58 % (2953716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.92/4.58 % (2953716)CaDiCaL version: 2.1.3
% 23.92/4.58 % (2953716)Termination reason: Instruction limit
% 23.92/4.58 % (2953716)Termination phase: Saturation
% 23.92/4.58 % (2953716)Time elapsed: 0.390 s
% 23.92/4.58 % (2953716)Peak memory usage: 95 MB
% 23.92/4.58 % (2953716)Instructions burned: 384 (million)
% 23.92/4.58 % (2953727)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=2438716309:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi)
% 23.92/4.58 % (2953729)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=2155066075:i=39:ins=3:rtra=on_2978 on theBenchmark for (2978ds/39Mi)
% 23.92/4.58 % (2953730)dis+1010_1_to=kbo:si=on:random_seed=215786160:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi)
% 23.92/4.58 % (2953724)Instruction limit reached!
% 23.92/4.58 % (2953724)------------------------------
% 23.92/4.58 % (2953724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.92/4.58 % (2953724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.92/4.58 % (2953724)CaDiCaL version: 2.1.3
% 23.92/4.58 % (2953724)Termination reason: Instruction limit
% 23.92/4.58 % (2953724)Termination phase: Saturation
% 23.92/4.58 % (2953724)Time elapsed: 0.128 s
% 23.92/4.58 % (2953724)Peak memory usage: 91 MB
% 23.92/4.58 % (2953724)Instructions burned: 121 (million)
% 23.92/4.58 % (2953729)Instruction limit reached!
% 23.92/4.58 % (2953729)------------------------------
% 23.92/4.58 % (2953729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.92/4.58 % (2953729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.92/4.58 % (2953729)CaDiCaL version: 2.1.3
% 23.92/4.58 % (2953729)Termination reason: Instruction limit
% 23.92/4.58 % (2953729)Termination phase: Property scanning
% 23.92/4.58 % (2953729)Time elapsed: 0.040 s
% 23.92/4.58 % (2953729)Peak memory usage: 88 MB
% 23.92/4.58 % (2953729)Instructions burned: 40 (million)
% 23.92/4.58 % (2953709)Instruction limit reached!
% 23.92/4.58 % (2953709)------------------------------
% 23.92/4.58 % (2953709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.92/4.58 % (2953709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.92/4.58 % (2953709)CaDiCaL version: 2.1.3
% 23.92/4.58 % (2953709)Termination reason: Instruction limit
% 23.92/4.58 % (2953709)Termination phase: Saturation
% 23.92/4.58 % (2953709)Time elapsed: 0.686 s
% 23.92/4.58 % (2953709)Peak memory usage: 139 MB
% 23.92/4.58 % (2953709)Instructions burned: 598 (million)
% 23.92/4.58 % (2953730)Instruction limit reached!
% 23.92/4.58 % (2953730)------------------------------
% 24.96/4.84 % (2953730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953730)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953730)Termination reason: Instruction limit
% 24.96/4.84 % (2953730)Termination phase: Saturation
% 24.96/4.84 % (2953730)Time elapsed: 0.101 s
% 24.96/4.84 % (2953730)Peak memory usage: 92 MB
% 24.96/4.84 % (2953730)Instructions burned: 177 (million)
% 24.96/4.84 % (2953727)Instruction limit reached!
% 24.96/4.84 % (2953727)------------------------------
% 24.96/4.84 % (2953727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953727)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953727)Termination reason: Instruction limit
% 24.96/4.84 % (2953727)Termination phase: Saturation
% 24.96/4.84 % (2953727)Time elapsed: 0.164 s
% 24.96/4.84 % (2953727)Peak memory usage: 119 MB
% 24.96/4.84 % (2953727)Instructions burned: 129 (million)
% 24.96/4.84 % (2953732)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3048772046:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi)
% 24.96/4.84 % (2953736)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2767122131:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi)
% 24.96/4.84 % (2953737)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2951299775:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi)
% 24.96/4.84 % (2953739)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=476313709:st=2:i=295:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/295Mi)
% 24.96/4.84 % (2953738)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2396800689:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi)
% 24.96/4.84 % (2953740)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2395620523:i=328:kws=inv_frequency:nm=20:rtra=on_2974 on theBenchmark for (2974ds/328Mi)
% 24.96/4.84 % (2953739)Instruction limit reached!
% 24.96/4.84 % (2953739)------------------------------
% 24.96/4.84 % (2953739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953739)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953739)Termination reason: Instruction limit
% 24.96/4.84 % (2953739)Termination phase: Saturation
% 24.96/4.84 % (2953739)Time elapsed: 0.158 s
% 24.96/4.84 % (2953739)Peak memory usage: 92 MB
% 24.96/4.84 % (2953739)Instructions burned: 297 (million)
% 24.96/4.84 % (2953732)Instruction limit reached!
% 24.96/4.84 % (2953732)------------------------------
% 24.96/4.84 % (2953732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953732)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953732)Termination reason: Instruction limit
% 24.96/4.84 % (2953732)Termination phase: Saturation
% 24.96/4.84 % (2953732)Time elapsed: 0.376 s
% 24.96/4.84 % (2953732)Peak memory usage: 120 MB
% 24.96/4.84 % (2953732)Instructions burned: 329 (million)
% 24.96/4.84 % (2953737)Instruction limit reached!
% 24.96/4.84 % (2953737)------------------------------
% 24.96/4.84 % (2953737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953737)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953737)Termination reason: Instruction limit
% 24.96/4.84 % (2953737)Termination phase: Saturation
% 24.96/4.84 % (2953737)Time elapsed: 0.265 s
% 24.96/4.84 % (2953737)Peak memory usage: 138 MB
% 24.96/4.84 % (2953737)Instructions burned: 215 (million)
% 24.96/4.84 % (2953715)Instruction limit reached!
% 24.96/4.84 % (2953715)------------------------------
% 24.96/4.84 % (2953715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953715)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953715)Termination reason: Instruction limit
% 24.96/4.84 % (2953715)Termination phase: Saturation
% 24.96/4.84 % (2953715)Time elapsed: 1.006 s
% 24.96/4.84 % (2953715)Peak memory usage: 98 MB
% 24.96/4.84 % (2953715)Instructions burned: 1000 (million)
% 24.96/4.84 % (2953747)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1473179890:i=281:gtgl=2:rtra=on:gtg=all_2971 on theBenchmark for (2971ds/281Mi)
% 24.96/4.84 % (2953738)Instruction limit reached!
% 24.96/4.84 % (2953738)------------------------------
% 24.96/4.84 % (2953738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953738)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953738)Termination reason: Instruction limit
% 24.96/4.84 % (2953738)Termination phase: Saturation
% 24.96/4.84 % (2953738)Time elapsed: 0.385 s
% 24.96/4.84 % (2953738)Peak memory usage: 120 MB
% 24.96/4.84 % (2953738)Instructions burned: 349 (million)
% 24.96/4.84 % (2953736)Instruction limit reached!
% 24.96/4.84 % (2953736)------------------------------
% 24.96/4.84 % (2953736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953736)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953736)Termination reason: Instruction limit
% 24.96/4.84 % (2953736)Termination phase: Saturation
% 24.96/4.84 % (2953736)Time elapsed: 0.559 s
% 24.96/4.84 % (2953736)Peak memory usage: 137 MB
% 24.96/4.84 % (2953736)Instructions burned: 483 (million)
% 24.96/4.84 % (2953740)Instruction limit reached!
% 24.96/4.84 % (2953740)------------------------------
% 24.96/4.84 % (2953740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953740)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953740)Termination reason: Instruction limit
% 24.96/4.84 % (2953740)Termination phase: Saturation
% 24.96/4.84 % (2953740)Time elapsed: 0.352 s
% 24.96/4.84 % (2953740)Peak memory usage: 119 MB
% 24.96/4.84 % (2953740)Instructions burned: 328 (million)
% 24.96/4.84 % (2953747)Instruction limit reached!
% 24.96/4.84 % (2953747)------------------------------
% 24.96/4.84 % (2953747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953747)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953747)Termination reason: Instruction limit
% 24.96/4.84 % (2953747)Termination phase: Saturation
% 24.96/4.84 % (2953747)Time elapsed: 0.175 s
% 24.96/4.84 % (2953747)Peak memory usage: 120 MB
% 24.96/4.84 % (2953747)Instructions burned: 282 (million)
% 24.96/4.84 % (2953750)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1480848886:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/484Mi)
% 24.96/4.84 % (2953753)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2106502913:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi)
% 24.96/4.84 % (2953752)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1219411924:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2970 on theBenchmark for (2970ds/321Mi)
% 24.96/4.84 % (2953756)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2278848114:i=471:thf=on:kws=precedence:rtra=on_2968 on theBenchmark for (2968ds/471Mi)
% 24.96/4.84 % (2953759)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=758542738:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/387Mi)
% 24.96/4.84 % (2953758)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3730238236:i=375:kws=inv_arity_squared:rtra=on_2967 on theBenchmark for (2967ds/375Mi)
% 24.96/4.84 % (2953757)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=3038525128:avsq=on:i=276:avsqr=1,2:rtra=on_2967 on theBenchmark for (2967ds/276Mi)
% 24.96/4.84 % (2953752)Instruction limit reached!
% 24.96/4.84 % (2953752)------------------------------
% 24.96/4.84 % (2953752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953752)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953752)Termination reason: Instruction limit
% 24.96/4.84 % (2953752)Termination phase: Saturation
% 24.96/4.84 % (2953752)Time elapsed: 0.360 s
% 24.96/4.84 % (2953752)Peak memory usage: 121 MB
% 24.96/4.84 % (2953752)Instructions burned: 322 (million)
% 24.96/4.84 % (2953759)First to succeed.
% 24.96/4.84 % (2953759)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2953558"
% 24.96/4.84 % (2953753)Instruction limit reached!
% 24.96/4.84 % (2953753)------------------------------
% 24.96/4.84 % (2953753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953753)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953753)Termination reason: Instruction limit
% 24.96/4.84 % (2953753)Termination phase: Saturation
% 24.96/4.84 % (2953753)Time elapsed: 0.401 s
% 24.96/4.84 % (2953753)Peak memory usage: 120 MB
% 24.96/4.84 % (2953753)Instructions burned: 416 (million)
% 24.96/4.84 % (2953750)Instruction limit reached!
% 24.96/4.84 % (2953750)------------------------------
% 24.96/4.84 % (2953750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953750)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953750)Termination reason: Instruction limit
% 24.96/4.84 % (2953750)Termination phase: Saturation
% 24.96/4.84 % (2953750)Time elapsed: 0.438 s
% 24.96/4.84 % (2953750)Peak memory usage: 92 MB
% 24.96/4.84 % (2953750)Instructions burned: 485 (million)
% 24.96/4.84 % (2953757)Instruction limit reached!
% 24.96/4.84 % (2953757)------------------------------
% 24.96/4.84 % (2953757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953757)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953757)Termination reason: Instruction limit
% 24.96/4.84 % (2953757)Termination phase: Saturation
% 24.96/4.84 % (2953757)Time elapsed: 0.338 s
% 24.96/4.84 % (2953757)Peak memory usage: 137 MB
% 24.96/4.84 % (2953757)Instructions burned: 276 (million)
% 24.96/4.84 % (2953770)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1548337302:i=334:rtra=on_2963 on theBenchmark for (2963ds/334Mi)
% 24.96/4.84 % (2953758)Instruction limit reached!
% 24.96/4.84 % (2953758)------------------------------
% 24.96/4.84 % (2953758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/4.84 % (2953758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/4.84 % (2953758)CaDiCaL version: 2.1.3
% 24.96/4.84 % (2953758)Termination reason: Instruction limit
% 24.96/4.84 % (2953758)Termination phase: Saturation
% 24.96/4.84 % (2953758)Time elapsed: 0.408 s
% 24.96/4.84 % (2953758)Peak memory usage: 120 MB
% 24.96/4.84 % (2953758)Instructions burned: 376 (million)
% 24.96/4.84 % (2953759)Refutation found. Thanks to Tanya!
% 24.96/4.84 % SZS status Theorem for theBenchmark
% 24.96/4.84 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/5.16 % (2953759)------------------------------
% 0.18/5.16 % (2953759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/5.16 % (2953759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/5.16 % (2953759)CaDiCaL version: 2.1.3
% 0.18/5.16 % (2953759)Termination reason: Refutation
% 0.18/5.16 % (2953759)Time elapsed: 0.189 s
% 0.18/5.16 % (2953759)Peak memory usage: 120 MB
% 0.18/5.16 % (2953759)Instructions burned: 289 (million)
% 0.18/5.16 % (2953759)------------------------------
% 0.18/5.16 % (2953759)------------------------------
% 0.18/5.16 % (2953558)Success in time 3.893 s
% 0.18/5.16 % Vampire exiting
%------------------------------------------------------------------------------