%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP344_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:39 AM UTC 2026
% Result : Theorem 38.33s 6.62s
% Output : Refutation 40.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 13
% Syntax : Number of formulae : 114 ( 23 unt; 0 typ; 0 def)
% Number of atoms : 345 ( 105 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 403 ( 172 ~; 128 |; 55 &)
% ( 11 <=>; 36 =>; 0 <=; 1 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 266 ( 106 atm; 57 fun; 89 num; 14 var)
% Number of types : 43 ( 41 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 24 ( 20 usr; 1 prp; 0-3 aty)
% Number of functors : 243 ( 240 usr; 32 con; 0-3 aty)
% Number of variables : 192 ( 147 !; 45 ?; 192 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'A_rows_vec_a_fun$': $tType ).
tff(type_def_6,type,
'Int_bool_fun$': $tType ).
tff(type_def_7,type,
'A_rows_vec_rows_vec_set$': $tType ).
tff(type_def_8,type,
'Rows_rows_bool_fun_fun$': $tType ).
tff(type_def_9,type,
'Nat_nat_bool_fun_fun$': $tType ).
tff(type_def_10,type,
'A_set_set$': $tType ).
tff(type_def_11,type,
'Rows$': $tType ).
tff(type_def_12,type,
'A_cols_vec_bool_fun$': $tType ).
tff(type_def_13,type,
'Rows_a_cols_vec_fun$': $tType ).
tff(type_def_14,type,
'Rows_a_cols_vec_bool_fun_fun$': $tType ).
tff(type_def_15,type,
'A_a_cols_vec_fun$': $tType ).
tff(type_def_16,type,
'Rows_a_rows_vec_bool_fun_fun$': $tType ).
tff(type_def_17,type,
'Int_set$': $tType ).
tff(type_def_18,type,
'Int_int_fun$': $tType ).
tff(type_def_19,type,
'Int_set_set$': $tType ).
tff(type_def_20,type,
'A_rows_vec_cols_vec$': $tType ).
tff(type_def_21,type,
'A_rows_vec_rows_vec_rows_vec$': $tType ).
tff(type_def_22,type,
'A_rows_vec_set$': $tType ).
tff(type_def_23,type,
'Nat_nat_fun$': $tType ).
tff(type_def_24,type,
'Nat$': $tType ).
tff(type_def_25,type,
'A_cols_vec_a_fun$': $tType ).
tff(type_def_26,type,
'A_rows_vec$': $tType ).
tff(type_def_27,type,
'Rows_a_rows_vec_fun$': $tType ).
tff(type_def_28,type,
'A_cols_vec_rows_vec_rows_vec$': $tType ).
tff(type_def_29,type,
tlbool: $tType ).
tff(type_def_30,type,
'Rows_bool_fun$': $tType ).
tff(type_def_31,type,
'A_bool_fun$': $tType ).
tff(type_def_32,type,
'A_cols_vec_rows_vec$': $tType ).
tff(type_def_33,type,
'A_set$': $tType ).
tff(type_def_34,type,
'Rows_a_bool_fun_fun$': $tType ).
tff(type_def_35,type,
'A_cols_vec$': $tType ).
tff(type_def_36,type,
'A$': $tType ).
tff(type_def_37,type,
'A_rows_vec_bool_fun$': $tType ).
tff(type_def_38,type,
'A_a_fun$': $tType ).
tff(type_def_39,type,
'Cols$': $tType ).
tff(type_def_40,type,
'A_cols_vec_cols_vec$': $tType ).
tff(type_def_41,type,
'Rows_a_fun$': $tType ).
tff(type_def_42,type,
'A_rows_vec_rows_vec$': $tType ).
tff(type_def_43,type,
'Int_int_bool_fun_fun$': $tType ).
tff(type_def_44,type,
'Nat_bool_fun$': $tType ).
tff(type_def_45,type,
'A_a_rows_vec_fun$': $tType ).
tff(func_def_0,type,
'plus$a': 'A$' > 'A_a_fun$' ).
tff(func_def_1,type,
'fun_app$f': ( 'Rows_rows_bool_fun_fun$' * 'Rows$' ) > 'Rows_bool_fun$' ).
tff(func_def_2,type,
'uud$': 'A_rows_vec_set$' > 'A_rows_vec_bool_fun$' ).
tff(func_def_3,type,
'p_Gauss_Jordan$': 'A_cols_vec_rows_vec$' > 'A_rows_vec_rows_vec$' ).
tff(func_def_4,type,
'one$c': 'A_rows_vec$' ).
tff(func_def_5,type,
'plus$h': ( 'A_cols_vec$' * 'A_cols_vec$' ) > 'A_cols_vec$' ).
tff(func_def_6,type,
'uu$': 'Rows_bool_fun$' ).
tff(func_def_7,type,
'plus$f': ( 'Rows$' * 'Rows$' ) > 'Rows$' ).
tff(func_def_8,type,
'fun_app$g': ( 'Rows_a_rows_vec_fun$' * 'Rows$' ) > 'A_rows_vec$' ).
tff(func_def_9,type,
'inconsistent$': 'A_cols_vec_rows_vec$' > 'A_rows_vec_bool_fun$' ).
tff(func_def_10,type,
'vec_nth$e': ( 'A_rows_vec_rows_vec_rows_vec$' * 'Rows$' ) > 'A_rows_vec_rows_vec$' ).
tff(func_def_11,type,
'gauss_Jordan$': 'A_cols_vec_rows_vec$' > 'A_cols_vec_rows_vec$' ).
tff(func_def_12,type,
'fun_app$r': ( 'Rows_a_cols_vec_bool_fun_fun$' * 'Rows$' ) > 'A_cols_vec_bool_fun$' ).
tff(func_def_13,type,
'collect$b': 'A_rows_vec_bool_fun$' > 'A_rows_vec_set$' ).
tff(func_def_14,type,
'uua$': ( 'A_cols_vec_rows_vec$' * 'A_rows_vec$' ) > 'Rows_bool_fun$' ).
tff(func_def_15,type,
'fun_app$i': ( 'Nat_nat_bool_fun_fun$' * 'Nat$' ) > 'Nat_bool_fun$' ).
tff(func_def_16,type,
'one$a': 'A_cols_vec$' ).
tff(func_def_17,type,
'dbl_inc$': 'A_a_fun$' ).
tff(func_def_18,type,
'one$': 'A_cols_vec_rows_vec$' ).
tff(func_def_19,type,
'map_matrix$d': ( 'A_a_cols_vec_fun$' * 'A_rows_vec_rows_vec$' ) > 'A_cols_vec_rows_vec_rows_vec$' ).
tff(func_def_20,type,
'zero$d': 'A_cols_vec_rows_vec$' ).
tff(func_def_21,type,
'matrix_vector_mult$': ( 'A_rows_vec_rows_vec$' * 'A_rows_vec$' ) > 'A_rows_vec$' ).
tff(func_def_22,type,
'plus$k': ( 'Int_set_set$' * 'Int_set_set$' ) > 'Int_set_set$' ).
tff(func_def_23,type,
'consistent$': 'A_cols_vec_rows_vec$' > 'A_rows_vec_bool_fun$' ).
tff(func_def_24,type,
'fun_app$k': ( 'Rows_a_cols_vec_fun$' * 'Rows$' ) > 'A_cols_vec$' ).
tff(func_def_25,type,
'least$a': 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_26,type,
'least$b': 'Int_bool_fun$' > $int ).
tff(func_def_27,type,
'fun_app$m': ( 'A_cols_vec_a_fun$' * 'A_cols_vec$' ) > 'A$' ).
tff(func_def_28,type,
'row$': ( 'Rows$' * 'A_cols_vec_rows_vec$' ) > 'A_cols_vec$' ).
tff(func_def_29,type,
'vec_nth$a': 'A_rows_vec_rows_vec$' > 'Rows_a_rows_vec_fun$' ).
tff(func_def_30,type,
'matrix_vector_mult$e': ( 'A_cols_vec_cols_vec$' * 'A_cols_vec$' ) > 'A_cols_vec$' ).
tff(func_def_31,type,
'plus$g': ( 'A_cols_vec_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'A_cols_vec_rows_vec$' ).
tff(func_def_32,type,
'zero$b': 'A_rows_vec$' ).
tff(func_def_33,type,
'one$e': 'Rows$' ).
tff(func_def_34,type,
'is_solution$': ( 'A_cols_vec$' * 'A_cols_vec_rows_vec$' ) > 'A_rows_vec_bool_fun$' ).
tff(func_def_35,type,
'matrix_vector_mult$d': ( 'A_cols_vec_rows_vec_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'A_cols_vec_rows_vec$' ).
tff(func_def_36,type,
'of_nat$': 'Nat$' > $int ).
tff(func_def_37,type,
'uui$': 'A_rows_vec_rows_vec$' > 'Rows_rows_bool_fun_fun$' ).
tff(func_def_38,type,
'matrix_vector_mult$a': ( 'A_cols_vec_rows_vec$' * 'A_cols_vec$' ) > 'A_rows_vec$' ).
tff(func_def_39,type,
'basis_left_null_space$': 'A_cols_vec_rows_vec$' > 'A_rows_vec_set$' ).
tff(func_def_40,type,
'matrix_vector_mult$b': ( 'A_rows_vec_rows_vec_rows_vec$' * 'A_rows_vec_rows_vec$' ) > 'A_rows_vec_rows_vec$' ).
tff(func_def_41,type,
'less_eq$a': 'Rows_rows_bool_fun_fun$' ).
tff(func_def_42,type,
'plus$d': ( 'Int_set$' * 'Int_set$' ) > 'Int_set$' ).
tff(func_def_43,type,
'rank$a': 'A_rows_vec_rows_vec$' > 'Nat$' ).
tff(func_def_44,type,
'vec_nth$': 'A_rows_vec$' > 'Rows_a_fun$' ).
tff(func_def_45,type,
'one$b': 'A_rows_vec_rows_vec$' ).
tff(func_def_46,type,
'less$': 'Nat_nat_bool_fun_fun$' ).
tff(func_def_47,type,
'vec_nth$c': ( 'A_cols_vec$' * 'Cols$' ) > 'A$' ).
tff(func_def_48,type,
'one$d': 'A$' ).
tff(func_def_49,type,
'greatest$b': 'Int_bool_fun$' > $int ).
tff(func_def_50,type,
tltrue: tlbool ).
tff(func_def_51,type,
'plus$': 'Nat$' > 'Nat_nat_fun$' ).
tff(func_def_52,type,
'a$': 'A_cols_vec_rows_vec$' ).
tff(func_def_53,type,
'fun_app$s': ( 'Rows_a_rows_vec_bool_fun_fun$' * 'Rows$' ) > 'A_rows_vec_bool_fun$' ).
tff(func_def_54,type,
'fun_app$a': ( 'Rows_a_fun$' * 'Rows$' ) > 'A$' ).
tff(func_def_55,type,
'least$': 'Rows_bool_fun$' > 'Rows$' ).
tff(func_def_56,type,
'column$': ( 'Rows$' * 'A_rows_vec_rows_vec$' ) > 'A_rows_vec$' ).
tff(func_def_57,type,
'plus$i': ( 'A_rows_vec_set$' * 'A_rows_vec_set$' ) > 'A_rows_vec_set$' ).
tff(func_def_58,type,
'fun_app$j': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_59,type,
'zero$f': 'Int_set$' ).
tff(func_def_60,type,
'fun_app$l': ( 'A_a_fun$' * 'A$' ) > 'A$' ).
tff(func_def_61,type,
'zero$h': 'Rows$' ).
tff(func_def_62,type,
'plus$c': ( 'A_rows_vec_rows_vec$' * 'A_rows_vec_rows_vec$' ) > 'A_rows_vec_rows_vec$' ).
tff(func_def_63,type,
'uuc$': 'A_set$' > 'A_bool_fun$' ).
tff(func_def_64,type,
'fun_app$o': ( 'A_a_cols_vec_fun$' * 'A$' ) > 'A_cols_vec$' ).
tff(func_def_65,type,
'map_matrix$c': ( 'A_rows_vec_a_fun$' * 'A_rows_vec_rows_vec_rows_vec$' ) > 'A_rows_vec_rows_vec$' ).
tff(func_def_66,type,
'dbl_inc$a': 'Int_int_fun$' ).
tff(func_def_67,type,
'matrix_vector_mult$c': ( 'A_rows_vec_cols_vec$' * 'A_rows_vec$' ) > 'A_cols_vec$' ).
tff(func_def_68,type,
'map_matrix$': ( 'A_a_fun$' * 'A_cols_vec_rows_vec$' ) > 'A_cols_vec_rows_vec$' ).
tff(func_def_69,type,
'one$f': 'Nat$' ).
tff(func_def_70,type,
'plus$b': ( 'A_rows_vec$' * 'A_rows_vec$' ) > 'A_rows_vec$' ).
tff(func_def_71,type,
'solve_consistent_rref$': ( 'A_cols_vec_rows_vec$' * 'A_rows_vec$' ) > 'A_cols_vec$' ).
tff(func_def_72,type,
'fun_app$n': ( 'A_rows_vec_a_fun$' * 'A_rows_vec$' ) > 'A$' ).
tff(func_def_73,type,
'fun_app$p': ( 'A_a_rows_vec_fun$' * 'A$' ) > 'A_rows_vec$' ).
tff(func_def_74,type,
'vec_nth$d': ( 'A_cols_vec_rows_vec_rows_vec$' * 'Rows$' ) > 'A_cols_vec_rows_vec$' ).
tff(func_def_75,type,
'to_nat$': 'Rows$' > 'Nat$' ).
tff(func_def_76,type,
'zero$a': 'A_cols_vec$' ).
tff(func_def_77,type,
'fun_app$t': ( 'Rows_a_bool_fun_fun$' * 'Rows$' ) > 'A_bool_fun$' ).
tff(func_def_78,type,
'less_eq$': 'Nat_nat_bool_fun_fun$' ).
tff(func_def_79,type,
'zero$e': 'A_rows_vec_rows_vec$' ).
tff(func_def_80,type,
'zero$': 'A$' ).
tff(func_def_81,type,
'map_matrix$e': ( 'A_a_rows_vec_fun$' * 'A_rows_vec_rows_vec$' ) > 'A_rows_vec_rows_vec_rows_vec$' ).
tff(func_def_82,type,
'less$a': 'Rows_rows_bool_fun_fun$' ).
tff(func_def_83,type,
tlfalse: tlbool ).
tff(func_def_84,type,
'nat$': $int > 'Nat$' ).
tff(func_def_85,type,
'fun_app$c': ( 'Int_int_bool_fun_fun$' * $int ) > 'Int_bool_fun$' ).
tff(func_def_86,type,
'row$a': ( 'Rows$' * 'A_rows_vec_rows_vec$' ) > 'A_rows_vec$' ).
tff(func_def_87,type,
'greatest$a': 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_88,type,
'uuj$': 'A_rows_vec_rows_vec$' > 'A_rows_vec_bool_fun$' ).
tff(func_def_89,type,
'plus$l': ( 'A_set_set$' * 'A_set_set$' ) > 'A_set_set$' ).
tff(func_def_90,type,
'uug$': 'A_cols_vec_rows_vec$' > 'A_rows_vec_bool_fun$' ).
tff(func_def_91,type,
'map_matrix$a': ( 'A_a_fun$' * 'A_rows_vec_rows_vec$' ) > 'A_rows_vec_rows_vec$' ).
tff(func_def_92,type,
'uue$': 'A_cols_vec_rows_vec$' > 'Rows_bool_fun$' ).
tff(func_def_93,type,
'map_matrix$b': ( 'A_cols_vec_a_fun$' * 'A_cols_vec_rows_vec_rows_vec$' ) > 'A_rows_vec_rows_vec$' ).
tff(func_def_94,type,
'plus$e': ( 'A_set$' * 'A_set$' ) > 'A_set$' ).
tff(func_def_95,type,
'uuf$': 'A_cols_vec_rows_vec$' > 'Rows_bool_fun$' ).
tff(func_def_96,type,
'fun_app$u': ( 'Int_int_fun$' * $int ) > $int ).
tff(func_def_97,type,
'collect$a': 'A_bool_fun$' > 'A_set$' ).
tff(func_def_98,type,
'zero$g': 'A_set$' ).
tff(func_def_99,type,
'b$': 'A_rows_vec$' ).
tff(func_def_100,type,
'uuh$': 'Int_int_bool_fun_fun$' ).
tff(func_def_101,type,
'rank$': 'A_cols_vec_rows_vec$' > 'Nat$' ).
tff(func_def_102,type,
'is_solution$a': ( 'A_rows_vec$' * 'A_rows_vec_rows_vec$' ) > 'A_rows_vec_bool_fun$' ).
tff(func_def_103,type,
'uub$': 'Int_set$' > 'Int_bool_fun$' ).
tff(func_def_104,type,
'zero$c': 'Nat$' ).
tff(func_def_105,type,
'collect$': 'Int_bool_fun$' > 'Int_set$' ).
tff(func_def_106,type,
'greatest$': 'Rows_bool_fun$' > 'Rows$' ).
tff(func_def_107,type,
'vec_nth$b': 'A_cols_vec_rows_vec$' > 'Rows_a_cols_vec_fun$' ).
tff(func_def_108,type,
'plus$j': ( 'A_rows_vec_rows_vec_set$' * 'A_rows_vec_rows_vec_set$' ) > 'A_rows_vec_rows_vec_set$' ).
tff(func_def_113,type,
sK3: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_114,type,
sK4: $int > $int ).
tff(func_def_115,type,
sK5: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_116,type,
sK6: ( 'A_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_117,type,
sK7: ( 'A_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_118,type,
sK8: ( 'A_rows_vec_rows_vec$' * 'A_rows_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_119,type,
sK9: 'Rows_bool_fun$' > 'Rows$' ).
tff(func_def_120,type,
sK10: ( 'Rows_bool_fun$' * 'Rows$' ) > 'Rows$' ).
tff(func_def_121,type,
sK11: 'Rows_bool_fun$' > 'Rows$' ).
tff(func_def_122,type,
sK12: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_123,type,
sK13: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_124,type,
sK14: $int > $int ).
tff(func_def_125,type,
sK15: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_126,type,
sK16: ( $int * 'Int_bool_fun$' ) > $int ).
tff(func_def_127,type,
sK17: ( 'Int_bool_fun$' * 'Int_bool_fun$' ) > $int ).
tff(func_def_128,type,
sK18: ( 'Rows_bool_fun$' * 'Rows$' ) > 'Rows$' ).
tff(func_def_129,type,
sK19: ( 'Rows_bool_fun$' * 'Rows_bool_fun$' ) > 'Rows$' ).
tff(func_def_130,type,
sK20: ( 'A_rows_vec_rows_vec$' * 'A_rows_vec_rows_vec$' ) > 'A_rows_vec$' ).
tff(func_def_131,type,
sK21: 'Rows_a_bool_fun_fun$' > 'A_rows_vec$' ).
tff(func_def_132,type,
sK22: 'Rows_a_bool_fun_fun$' > 'Rows$' ).
tff(func_def_133,type,
sK23: ( 'Rows_a_bool_fun_fun$' * 'Rows$' ) > 'A$' ).
tff(func_def_134,type,
sK24: ( 'Rows_a_bool_fun_fun$' * 'A_rows_vec$' ) > 'Rows$' ).
tff(func_def_135,type,
sK25: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_136,type,
sK26: 'Int_int_fun$' > $int ).
tff(func_def_137,type,
sK27: 'Int_int_fun$' > $int ).
tff(func_def_138,type,
sK28: 'Int_int_fun$' > $int ).
tff(func_def_139,type,
sK29: 'Int_int_fun$' > $int ).
tff(func_def_140,type,
sK30: ( 'Nat_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_141,type,
sK31: ( 'Nat_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_142,type,
sK32: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_143,type,
sK33: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_144,type,
sK34: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_145,type,
sK35: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_146,type,
sK36: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_147,type,
sK37: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_148,type,
sK38: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_149,type,
sK39: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_150,type,
sK40: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_151,type,
sK41: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_152,type,
sK42: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_153,type,
sK43: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_154,type,
sK44: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_155,type,
sK45: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_156,type,
sK46: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_157,type,
sK47: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_158,type,
sK48: ( 'A_rows_vec$' * 'A_rows_vec$' ) > 'Rows$' ).
tff(func_def_159,type,
sK49: ( 'Rows_bool_fun$' * 'Rows_bool_fun$' ) > 'Rows$' ).
tff(func_def_160,type,
sK50: 'Int_int_fun$' > $int ).
tff(func_def_161,type,
sK51: 'Int_int_fun$' > $int ).
tff(func_def_162,type,
sK52: ( 'A_cols_vec_rows_vec$' * 'A_rows_vec$' ) > 'Rows$' ).
tff(func_def_163,type,
sK53: 'Int_int_fun$' > $int ).
tff(func_def_164,type,
sK54: 'Int_int_fun$' > $int ).
tff(func_def_165,type,
sK55: 'Rows_rows_bool_fun_fun$' > 'Rows$' ).
tff(func_def_166,type,
sK56: 'Rows_rows_bool_fun_fun$' > 'Rows$' ).
tff(func_def_167,type,
sK57: 'Rows_rows_bool_fun_fun$' > 'Rows$' ).
tff(func_def_168,type,
sK58: 'Rows_rows_bool_fun_fun$' > 'Rows$' ).
tff(func_def_169,type,
sK59: 'Rows_rows_bool_fun_fun$' > 'Rows$' ).
tff(func_def_170,type,
sK60: ( 'Rows_bool_fun$' * 'Rows_bool_fun$' ) > 'Rows$' ).
tff(func_def_171,type,
sK61: 'Int_int_fun$' > $int ).
tff(func_def_172,type,
sK62: 'Int_int_fun$' > $int ).
tff(func_def_173,type,
sK63: ( 'A_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_174,type,
sK64: ( 'A_cols_vec_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_175,type,
sK65: ( 'A_cols_vec_rows_vec$' * 'A_rows_vec$' ) > 'Rows$' ).
tff(func_def_176,type,
sK66: ( 'Nat_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_177,type,
sK67: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_178,type,
sK68: 'Int_int_fun$' > $int ).
tff(func_def_179,type,
sK69: 'Int_int_fun$' > $int ).
tff(func_def_180,type,
sK70: ( 'A_cols_vec_rows_vec$' * 'A_rows_vec$' ) > 'Rows$' ).
tff(func_def_181,type,
sK71: ( 'A_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_182,type,
sK72: ( 'Int_bool_fun$' * $int ) > $int ).
tff(func_def_183,type,
sK73: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_184,type,
sK74: ( $int * 'Int_bool_fun$' ) > $int ).
tff(func_def_185,type,
sK75: 'Rows_bool_fun$' > 'Rows$' ).
tff(func_def_186,type,
sK76: ( 'A_cols_vec_rows_vec$' * 'A_rows_vec$' ) > 'Rows$' ).
tff(func_def_187,type,
sK77: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_188,type,
sK78: ( 'Nat_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_189,type,
sK79: ( 'Int_bool_fun$' * $int ) > $int ).
tff(func_def_190,type,
sK80: ( 'Int_bool_fun$' * $int ) > $int ).
tff(func_def_191,type,
sK81: ( 'A_rows_vec$' * 'A_rows_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_192,type,
sK82: ( $int * 'Int_set$' * 'Int_set$' ) > $int ).
tff(func_def_193,type,
sK83: ( $int * 'Int_set$' * 'Int_set$' ) > $int ).
tff(func_def_194,type,
sK84: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_195,type,
sK85: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_196,type,
sK86: ( 'Rows_bool_fun$' * 'Rows_bool_fun$' ) > 'Rows$' ).
tff(func_def_197,type,
sK87: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_198,type,
sK88: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_199,type,
sK89: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_200,type,
sK90: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_201,type,
sK91: 'Int_int_fun$' > $int ).
tff(func_def_202,type,
sK92: 'Int_int_fun$' > $int ).
tff(func_def_203,type,
sK93: 'Int_int_fun$' > $int ).
tff(func_def_204,type,
sK94: 'Int_int_fun$' > $int ).
tff(func_def_205,type,
sK95: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_206,type,
sK96: 'Int_int_fun$' > $int ).
tff(func_def_207,type,
sK97: 'Int_int_fun$' > $int ).
tff(func_def_208,type,
sK98: ( 'Nat_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_209,type,
sK99: 'Rows_a_cols_vec_bool_fun_fun$' > 'A_cols_vec_rows_vec$' ).
tff(func_def_210,type,
sK100: 'Rows_a_cols_vec_bool_fun_fun$' > 'Rows$' ).
tff(func_def_211,type,
sK101: ( 'Rows_a_cols_vec_bool_fun_fun$' * 'Rows$' ) > 'A_cols_vec$' ).
tff(func_def_212,type,
sK102: ( 'Rows_a_cols_vec_bool_fun_fun$' * 'A_cols_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_213,type,
sK103: 'Int_int_fun$' > $int ).
tff(func_def_214,type,
sK104: 'Int_int_fun$' > $int ).
tff(func_def_215,type,
sK105: ( 'Int_bool_fun$' * 'Int_bool_fun$' ) > $int ).
tff(func_def_216,type,
sK106: ( $int * 'Int_bool_fun$' ) > $int ).
tff(func_def_217,type,
sK107: 'Rows$' ).
tff(func_def_218,type,
sK108: 'Rows$' ).
tff(func_def_219,type,
sK109: 'Int_int_fun$' > $int ).
tff(func_def_220,type,
sK110: 'Int_int_fun$' > $int ).
tff(func_def_221,type,
sK111: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_222,type,
sK112: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_223,type,
sK113: ( 'Nat_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_224,type,
sK114: 'Rows_a_rows_vec_bool_fun_fun$' > 'A_rows_vec_rows_vec$' ).
tff(func_def_225,type,
sK115: 'Rows_a_rows_vec_bool_fun_fun$' > 'Rows$' ).
tff(func_def_226,type,
sK116: ( 'Rows_a_rows_vec_bool_fun_fun$' * 'Rows$' ) > 'A_rows_vec$' ).
tff(func_def_227,type,
sK117: ( 'Rows_a_rows_vec_bool_fun_fun$' * 'A_rows_vec_rows_vec$' ) > 'Rows$' ).
tff(func_def_228,type,
sK118: ( 'Int_bool_fun$' * $int ) > $int ).
tff(func_def_229,type,
sK119: ( 'Int_bool_fun$' * $int ) > $int ).
tff(func_def_230,type,
sK120: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_231,type,
sK121: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_232,type,
sK122: ( 'Rows_bool_fun$' * 'Rows$' ) > 'Rows$' ).
tff(func_def_233,type,
sK123: 'Int_int_fun$' > $int ).
tff(func_def_234,type,
sK124: 'Int_int_fun$' > $int ).
tff(func_def_235,type,
sK125: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_236,type,
sK126: ( 'A_rows_vec$' * 'A_cols_vec_rows_vec$' ) > 'A_cols_vec$' ).
tff(func_def_237,type,
sK127: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_238,type,
sK128: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_239,type,
sK129: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_240,type,
sK130: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_241,type,
sK131: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_242,type,
sK132: ( 'A_rows_vec_bool_fun$' * 'A_rows_vec_bool_fun$' ) > 'A_rows_vec$' ).
tff(func_def_243,type,
sK133: 'Nat_bool_fun$' > 'Nat$' ).
tff(pred_def_1,type,
'member$': ( 'A_rows_vec$' * 'A_rows_vec_set$' ) > $o ).
tff(pred_def_2,type,
'fun_app$q': ( 'A_cols_vec_bool_fun$' * 'A_cols_vec$' ) > $o ).
tff(pred_def_3,type,
'member$e': ( 'A_set$' * 'A_set_set$' ) > $o ).
tff(pred_def_4,type,
'reduced_row_echelon_form$': 'A_rows_vec_rows_vec$' > $o ).
tff(pred_def_5,type,
'less_eq$c': ( 'A_set$' * 'A_set$' ) > $o ).
tff(pred_def_6,type,
'fun_app$e': ( 'A_bool_fun$' * 'A$' ) > $o ).
tff(pred_def_7,type,
'member$b': ( 'A$' * 'A_set$' ) > $o ).
tff(pred_def_8,type,
'fun_app$d': ( 'A_rows_vec_bool_fun$' * 'A_rows_vec$' ) > $o ).
tff(pred_def_9,type,
'less_eq$b': ( 'Int_set$' * 'Int_set$' ) > $o ).
tff(pred_def_10,type,
'member$d': ( 'Int_set$' * 'Int_set_set$' ) > $o ).
tff(pred_def_11,type,
'is_zero_row$': ( 'Rows$' * 'A_cols_vec_rows_vec$' ) > $o ).
tff(pred_def_12,type,
'fun_app$': ( 'Rows_bool_fun$' * 'Rows$' ) > $o ).
tff(pred_def_13,type,
'member$c': ( 'A_rows_vec_rows_vec$' * 'A_rows_vec_rows_vec_set$' ) > $o ).
tff(pred_def_14,type,
'fun_app$h': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).
tff(pred_def_15,type,
'less_eq$d': ( 'A_rows_vec_set$' * 'A_rows_vec_set$' ) > $o ).
tff(pred_def_16,type,
'member$a': ( $int * 'Int_set$' ) > $o ).
tff(pred_def_17,type,
'fun_app$b': ( 'Int_bool_fun$' * $int ) > $o ).
tff(pred_def_20,type,
sP0: ( $int * $int * $int ) > $o ).
tff(pred_def_21,type,
sP1: ( $int * $int * $int ) > $o ).
tff(pred_def_22,type,
sP2: ( $int * $int * $int ) > $o ).
tff(f1,axiom,
! [X0: 'Rows$'] :
( ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
<=> 'fun_app$'('uu$',X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom0) ).
tff(f10,axiom,
! [X1: 'A_rows_vec$',X2: 'Rows$',X0: 'A_cols_vec_rows_vec$'] :
( 'fun_app$'('uua$'(X0,X1),X2)
<=> ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) != 'zero$' ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom9) ).
tff(f12,conjecture,
( ( ( ~ ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
=> $lesseq(0,'of_nat$'('rank$'('a$'))) )
& ( ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
=> $lesseq($sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1),'of_nat$'('rank$'('a$'))) ) )
<=> 'fun_app$d'('consistent$'('a$'),'b$') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture11) ).
tff(f13,negated_conjecture,
~ ( ( ( ~ ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
=> $lesseq(0,'of_nat$'('rank$'('a$'))) )
& ( ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
=> $lesseq($sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1),'of_nat$'('rank$'('a$'))) ) )
<=> 'fun_app$d'('consistent$'('a$'),'b$') ),
inference(negated_conjecture,[status(cth)],[f12]) ).
tff(f14,axiom,
! [X1: 'A_rows_vec$',X0: 'A_cols_vec_rows_vec$'] :
( 'fun_app$d'('consistent$'(X0),X1)
=> ( ( ? [X2: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) != 'zero$' )
=> $lesseq($sum('of_nat$'('to_nat$'('greatest$'('uua$'(X0,X1)))),1),'of_nat$'('rank$'(X0))) )
& ( ~ ? [X2: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) != 'zero$' )
=> $lesseq(0,'of_nat$'('rank$'(X0))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom12) ).
tff(f15,axiom,
! [X1: 'A_rows_vec$',X0: 'A_cols_vec_rows_vec$'] :
( ( ( ~ ? [X2: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) != 'zero$' )
=> $lesseq(0,'of_nat$'('rank$'(X0))) )
& ( ? [X2: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) != 'zero$' )
=> $lesseq($sum('of_nat$'('to_nat$'('greatest$'('uua$'(X0,X1)))),1),'of_nat$'('rank$'(X0))) ) )
=> 'fun_app$d'('consistent$'(X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom13) ).
tff(f137,axiom,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom135) ).
tff(f282,axiom,
! [X0: 'Rows$',X1: 'Rows$'] :
( 'fun_app$'('fun_app$f'('less_eq$a',X0),X1)
=> $lesseq('of_nat$'('to_nat$'(X0)),'of_nat$'('to_nat$'(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom280) ).
tff(f312,axiom,
! [X1: 'Rows$',X0: 'Rows_bool_fun$'] :
( 'fun_app$'(X0,X1)
=> 'fun_app$'('fun_app$f'('less_eq$a',X1),'greatest$'(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom310) ).
tff(f327,axiom,
! [X0: 'Nat$'] :
( $false
<=> $less('of_nat$'(X0),0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom325) ).
tff(f380,axiom,
! [X0: 'Rows_bool_fun$'] :
( ? [X1: 'Rows$'] :
( ! [X2: 'Rows$'] :
( 'fun_app$'('fun_app$f'('less$a',X1),X2)
=> ~ 'fun_app$'(X0,X2) )
& 'fun_app$'(X0,X1) )
<=> ? [X1: 'Rows$'] : 'fun_app$'(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom378) ).
tff(f473,axiom,
! [X0: 'Rows_bool_fun$'] :
( ? [X1: 'Rows$'] : 'fun_app$'(X0,X1)
=> 'fun_app$'(X0,'greatest$'(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom471) ).
tff(f476,axiom,
! [X1: 'Rows$',X0: 'Rows_bool_fun$'] :
( 'fun_app$'(X0,X1)
=> 'fun_app$'(X0,'greatest$'(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom474) ).
tff(f547,axiom,
! [X0: $int,X1: $int] :
( ( ( X0 != X1 )
& $lesseq(X0,X1) )
=> $less(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom545) ).
tff(f665,plain,
! [X1: 'A_rows_vec$',X0: 'A_cols_vec_rows_vec$'] :
( 'fun_app$d'('consistent$'(X0),X1)
=> ( ( ? [X2: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) != 'zero$' )
=> ~ $less('of_nat$'('rank$'(X0)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X0,X1)))),1)) )
& ( ~ ? [X2: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) != 'zero$' )
=> ~ $less('of_nat$'('rank$'(X0)),0) ) ) ),
inference(theory_normalization,[],[f14]) ).
tff(f699,plain,
! [X1: 'A_rows_vec$',X0: 'A_cols_vec_rows_vec$'] :
( ( ( ~ ? [X2: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) != 'zero$' )
=> ~ $less('of_nat$'('rank$'(X0)),0) )
& ( ? [X2: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) != 'zero$' )
=> ~ $less('of_nat$'('rank$'(X0)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X0,X1)))),1)) ) )
=> 'fun_app$d'('consistent$'(X0),X1) ),
inference(theory_normalization,[],[f15]) ).
tff(f731,plain,
~ ( ( ( ~ ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
=> ~ $less('of_nat$'('rank$'('a$')),0) )
& ( ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
=> ~ $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) ) )
<=> 'fun_app$d'('consistent$'('a$'),'b$') ),
inference(theory_normalization,[],[f13]) ).
tff(f750,plain,
! [X1: 'Rows$',X0: 'Rows$'] :
( 'fun_app$'('fun_app$f'('less_eq$a',X0),X1)
=> ~ $less('of_nat$'('to_nat$'(X1)),'of_nat$'('to_nat$'(X0))) ),
inference(theory_normalization,[],[f282]) ).
tff(f768,plain,
! [X0: $int,X1: $int] :
( ( ( X0 != X1 )
& ~ $less(X1,X0) )
=> $less(X0,X1) ),
inference(theory_normalization,[],[f547]) ).
tff(f829,plain,
! [X0: 'Rows_bool_fun$'] :
( ? [X3: 'Rows$'] : 'fun_app$'(X0,X3)
<=> ? [X1: 'Rows$'] :
( ! [X2: 'Rows$'] :
( 'fun_app$'('fun_app$f'('less$a',X1),X2)
=> ~ 'fun_app$'(X0,X2) )
& 'fun_app$'(X0,X1) ) ),
inference(rectify,[],[f380]) ).
tff(f874,plain,
! [X0: 'A_rows_vec$',X1: 'A_cols_vec_rows_vec$'] :
( 'fun_app$d'('consistent$'(X1),X0)
=> ( ( ~ ? [X3: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X1),X0)),X3) )
=> ~ $less('of_nat$'('rank$'(X1)),0) )
& ( ? [X2: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X1),X0)),X2) )
=> ~ $less('of_nat$'('rank$'(X1)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X1,X0)))),1)) ) ) ),
inference(rectify,[],[f665]) ).
tff(f888,plain,
! [X1: 'Rows$',X0: 'A_rows_vec$',X2: 'A_cols_vec_rows_vec$'] :
( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X2),X0)),X1) )
<=> 'fun_app$'('uua$'(X2,X0),X1) ),
inference(rectify,[],[f10]) ).
tff(f951,plain,
! [X1: 'A_cols_vec_rows_vec$',X0: 'A_rows_vec$'] :
( ( ( ~ ? [X2: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X1),X0)),X2) )
=> ~ $less('of_nat$'('rank$'(X1)),0) )
& ( ? [X3: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X1),X0)),X3) )
=> ~ $less('of_nat$'('rank$'(X1)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X1,X0)))),1)) ) )
=> 'fun_app$d'('consistent$'(X1),X0) ),
inference(rectify,[],[f699]) ).
tff(f1010,plain,
! [X0: 'Nat$'] : ~ $less('of_nat$'(X0),0),
inference(true_and_false_elimination,[],[f327]) ).
tff(f1011,plain,
! [X0: 'Nat$'] : ~ $less('of_nat$'(X0),0),
inference(flattening,[],[f1010]) ).
tff(f1038,plain,
~ ( 'fun_app$d'('consistent$'('a$'),'b$')
<=> ( ( ~ ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
=> ~ $less('of_nat$'('rank$'('a$')),0) )
& ( ? [X1: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X1) )
=> ~ $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) ) ) ),
inference(rectify,[],[f731]) ).
tff(f1149,plain,
! [X0: 'Rows$',X1: 'Rows_bool_fun$'] :
( 'fun_app$'(X1,X0)
=> 'fun_app$'(X1,'greatest$'(X1)) ),
inference(rectify,[],[f476]) ).
tff(f1284,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| ( X0 = X1 )
| $less(X1,X0) ),
inference(ennf_transformation,[],[f768]) ).
tff(f1285,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| $less(X0,X1)
| ( X0 = X1 ) ),
inference(flattening,[],[f1284]) ).
tff(f1289,plain,
! [X0: 'Rows_bool_fun$'] :
( ? [X3: 'Rows$'] : 'fun_app$'(X0,X3)
<=> ? [X1: 'Rows$'] :
( ! [X2: 'Rows$'] :
( ~ 'fun_app$'(X0,X2)
| ~ 'fun_app$'('fun_app$f'('less$a',X1),X2) )
& 'fun_app$'(X0,X1) ) ),
inference(ennf_transformation,[],[f829]) ).
tff(f1337,plain,
! [X1: 'A_cols_vec_rows_vec$',X0: 'A_rows_vec$'] :
( ( ( ~ $less('of_nat$'('rank$'(X1)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X1,X0)))),1))
| ! [X2: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X1),X0)),X2) ) )
& ( ~ $less('of_nat$'('rank$'(X1)),0)
| ? [X3: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X1),X0)),X3) ) ) )
| ~ 'fun_app$d'('consistent$'(X1),X0) ),
inference(ennf_transformation,[],[f874]) ).
tff(f1392,plain,
! [X0: 'Rows$',X1: 'Rows$'] :
( ~ 'fun_app$'('fun_app$f'('less_eq$a',X0),X1)
| ~ $less('of_nat$'('to_nat$'(X1)),'of_nat$'('to_nat$'(X0))) ),
inference(ennf_transformation,[],[f750]) ).
tff(f1407,plain,
! [X0: 'Rows_bool_fun$',X1: 'Rows$'] :
( ~ 'fun_app$'(X0,X1)
| 'fun_app$'('fun_app$f'('less_eq$a',X1),'greatest$'(X0)) ),
inference(ennf_transformation,[],[f312]) ).
tff(f1418,plain,
! [X0: 'Rows_bool_fun$'] :
( ! [X1: 'Rows$'] : ~ 'fun_app$'(X0,X1)
| 'fun_app$'(X0,'greatest$'(X0)) ),
inference(ennf_transformation,[],[f473]) ).
tff(f1419,plain,
( 'fun_app$d'('consistent$'('a$'),'b$')
<~> ( ( ! [X1: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X1) )
| ~ $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) )
& ( ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
| ~ $less('of_nat$'('rank$'('a$')),0) ) ) ),
inference(ennf_transformation,[],[f1038]) ).
tff(f1503,plain,
! [X1: 'A_cols_vec_rows_vec$',X0: 'A_rows_vec$'] :
( 'fun_app$d'('consistent$'(X1),X0)
| ( $less('of_nat$'('rank$'(X1)),0)
& ! [X2: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X1),X0)),X2) ) )
| ( ? [X3: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X1),X0)),X3) )
& $less('of_nat$'('rank$'(X1)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X1,X0)))),1)) ) ),
inference(ennf_transformation,[],[f951]) ).
tff(f1504,plain,
! [X1: 'A_cols_vec_rows_vec$',X0: 'A_rows_vec$'] :
( ( ? [X3: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X1),X0)),X3) )
& $less('of_nat$'('rank$'(X1)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X1,X0)))),1)) )
| ( $less('of_nat$'('rank$'(X1)),0)
& ! [X2: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X1),X0)),X2) ) )
| 'fun_app$d'('consistent$'(X1),X0) ),
inference(flattening,[],[f1503]) ).
tff(f1508,plain,
! [X0: 'Rows$',X1: 'Rows_bool_fun$'] :
( ~ 'fun_app$'(X1,X0)
| 'fun_app$'(X1,'greatest$'(X1)) ),
inference(ennf_transformation,[],[f1149]) ).
tff(f1666,plain,
! [X0: 'Rows_bool_fun$'] :
( ( ? [X3: 'Rows$'] : 'fun_app$'(X0,X3)
| ! [X1: 'Rows$'] :
( ? [X2: 'Rows$'] :
( 'fun_app$'(X0,X2)
& 'fun_app$'('fun_app$f'('less$a',X1),X2) )
| ~ 'fun_app$'(X0,X1) ) )
& ( ? [X1: 'Rows$'] :
( ! [X2: 'Rows$'] :
( ~ 'fun_app$'(X0,X2)
| ~ 'fun_app$'('fun_app$f'('less$a',X1),X2) )
& 'fun_app$'(X0,X1) )
| ! [X3: 'Rows$'] : ~ 'fun_app$'(X0,X3) ) ),
inference(nnf_transformation,[],[f1289]) ).
tff(f1667,plain,
! [X0: 'Rows_bool_fun$'] :
( ( ? [X1: 'Rows$'] : 'fun_app$'(X0,X1)
| ! [X2: 'Rows$'] :
( ? [X3: 'Rows$'] :
( 'fun_app$'(X0,X3)
& 'fun_app$'('fun_app$f'('less$a',X2),X3) )
| ~ 'fun_app$'(X0,X2) ) )
& ( ? [X4: 'Rows$'] :
( ! [X5: 'Rows$'] :
( ~ 'fun_app$'(X0,X5)
| ~ 'fun_app$'('fun_app$f'('less$a',X4),X5) )
& 'fun_app$'(X0,X4) )
| ! [X6: 'Rows$'] : ~ 'fun_app$'(X0,X6) ) ),
inference(rectify,[],[f1666]) ).
tff(f1668,plain,
! [X0: 'Rows_bool_fun$'] :
( ( 'fun_app$'(X0,sK9(X0))
| ! [X2: 'Rows$'] :
( ( 'fun_app$'(X0,sK10(X0,X2))
& 'fun_app$'('fun_app$f'('less$a',X2),sK10(X0,X2)) )
| ~ 'fun_app$'(X0,X2) ) )
& ( ( ! [X5: 'Rows$'] :
( ~ 'fun_app$'(X0,X5)
| ~ 'fun_app$'('fun_app$f'('less$a',sK11(X0)),X5) )
& 'fun_app$'(X0,sK11(X0)) )
| ! [X6: 'Rows$'] : ~ 'fun_app$'(X0,X6) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11]),skolemize(X1,sK9(X0)),skolemize(X3,sK10(X0,X2)),skolemize(X4,sK11(X0))],[f1667]) ).
tff(f1836,plain,
! [X0: 'A_cols_vec_rows_vec$',X1: 'A_rows_vec$'] :
( ( ? [X2: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) )
& $less('of_nat$'('rank$'(X0)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X0,X1)))),1)) )
| ( $less('of_nat$'('rank$'(X0)),0)
& ! [X3: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X3) ) )
| 'fun_app$d'('consistent$'(X0),X1) ),
inference(rectify,[],[f1504]) ).
tff(f1837,plain,
! [X0: 'A_cols_vec_rows_vec$',X1: 'A_rows_vec$'] :
( ( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),sK52(X0,X1)) )
& $less('of_nat$'('rank$'(X0)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X0,X1)))),1)) )
| ( $less('of_nat$'('rank$'(X0)),0)
& ! [X3: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X3) ) )
| 'fun_app$d'('consistent$'(X0),X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52]),skolemize(X2,sK52(X0,X1))],[f1836]) ).
tff(f1911,plain,
! [X0: 'A_cols_vec_rows_vec$',X1: 'A_rows_vec$'] :
( ( ( ~ $less('of_nat$'('rank$'(X0)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X0,X1)))),1))
| ! [X2: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) ) )
& ( ~ $less('of_nat$'('rank$'(X0)),0)
| ? [X3: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X3) ) ) )
| ~ 'fun_app$d'('consistent$'(X0),X1) ),
inference(rectify,[],[f1337]) ).
tff(f1912,plain,
! [X0: 'A_cols_vec_rows_vec$',X1: 'A_rows_vec$'] :
( ( ( ~ $less('of_nat$'('rank$'(X0)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X0,X1)))),1))
| ! [X2: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) ) )
& ( ~ $less('of_nat$'('rank$'(X0)),0)
| ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),sK70(X0,X1)) ) ) )
| ~ 'fun_app$d'('consistent$'(X0),X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70]),skolemize(X3,sK70(X0,X1))],[f1911]) ).
tff(f2036,plain,
! [X0: 'Rows$'] :
( ( ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
| ~ 'fun_app$'('uu$',X0) )
& ( 'fun_app$'('uu$',X0)
| ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' ) ) ),
inference(nnf_transformation,[],[f1]) ).
tff(f2105,plain,
( ( ( ? [X1: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X1) )
& $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) )
| ( ! [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' )
& $less('of_nat$'('rank$'('a$')),0) )
| ~ 'fun_app$d'('consistent$'('a$'),'b$') )
& ( ( ( ! [X1: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X1) )
| ~ $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) )
& ( ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
| ~ $less('of_nat$'('rank$'('a$')),0) ) )
| 'fun_app$d'('consistent$'('a$'),'b$') ) ),
inference(nnf_transformation,[],[f1419]) ).
tff(f2106,plain,
( ( ( ? [X1: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X1) )
& $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) )
| ( ! [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' )
& $less('of_nat$'('rank$'('a$')),0) )
| ~ 'fun_app$d'('consistent$'('a$'),'b$') )
& ( ( ( ! [X1: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X1) )
| ~ $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) )
& ( ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
| ~ $less('of_nat$'('rank$'('a$')),0) ) )
| 'fun_app$d'('consistent$'('a$'),'b$') ) ),
inference(flattening,[],[f2105]) ).
tff(f2107,plain,
( ( ( ? [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' )
& $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) )
| ( ! [X1: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X1) )
& $less('of_nat$'('rank$'('a$')),0) )
| ~ 'fun_app$d'('consistent$'('a$'),'b$') )
& ( ( ( ! [X2: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X2) )
| ~ $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) )
& ( ? [X3: 'Rows$'] : ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X3) )
| ~ $less('of_nat$'('rank$'('a$')),0) ) )
| 'fun_app$d'('consistent$'('a$'),'b$') ) ),
inference(rectify,[],[f2106]) ).
tff(f2108,plain,
( ( ( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK107) )
& $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) )
| ( ! [X1: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X1) )
& $less('of_nat$'('rank$'('a$')),0) )
| ~ 'fun_app$d'('consistent$'('a$'),'b$') )
& ( ( ( ! [X2: 'Rows$'] : ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X2) )
| ~ $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) )
& ( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK108) )
| ~ $less('of_nat$'('rank$'('a$')),0) ) )
| 'fun_app$d'('consistent$'('a$'),'b$') ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK107,sK108]),skolemize(X0,sK107),skolemize(X3,sK108)],[f2107]) ).
tff(f2127,plain,
! [X1: 'Rows$',X0: 'A_rows_vec$',X2: 'A_cols_vec_rows_vec$'] :
( ( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X2),X0)),X1) )
| ~ 'fun_app$'('uua$'(X2,X0),X1) )
& ( 'fun_app$'('uua$'(X2,X0),X1)
| ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X2),X0)),X1) ) ) ),
inference(nnf_transformation,[],[f888]) ).
tff(f2128,plain,
! [X0: 'Rows$',X1: 'A_rows_vec$',X2: 'A_cols_vec_rows_vec$'] :
( ( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X2),X1)),X0) )
| ~ 'fun_app$'('uua$'(X2,X1),X0) )
& ( 'fun_app$'('uua$'(X2,X1),X0)
| ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X2),X1)),X0) ) ) ),
inference(rectify,[],[f2127]) ).
tff(f2302,plain,
! [X0: 'Rows_bool_fun$',X6: 'Rows$'] :
( ~ 'fun_app$'(X0,X6)
| 'fun_app$'(X0,sK11(X0)) ),
inference(cnf_transformation,[],[f1668]) ).
tff(f2347,plain,
! [X0: 'Rows$',X1: 'Rows$'] :
( ~ 'fun_app$'('fun_app$f'('less_eq$a',X0),X1)
| ~ $less('of_nat$'('to_nat$'(X1)),'of_nat$'('to_nat$'(X0))) ),
inference(cnf_transformation,[],[f1392]) ).
tff(f2560,plain,
! [X0: 'Rows$',X1: 'Rows_bool_fun$'] :
( ~ 'fun_app$'(X1,X0)
| 'fun_app$'(X1,'greatest$'(X1)) ),
inference(cnf_transformation,[],[f1508]) ).
tff(f2575,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
inference(cnf_transformation,[],[f137]) ).
tff(f2577,plain,
! [X0: 'A_cols_vec_rows_vec$',X1: 'A_rows_vec$'] :
( 'fun_app$d'('consistent$'(X0),X1)
| $less('of_nat$'('rank$'(X0)),0)
| $less('of_nat$'('rank$'(X0)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X0,X1)))),1)) ),
inference(cnf_transformation,[],[f1837]) ).
tff(f2579,plain,
! [X0: 'A_cols_vec_rows_vec$',X1: 'A_rows_vec$'] :
( 'fun_app$d'('consistent$'(X0),X1)
| $less('of_nat$'('rank$'(X0)),0)
| ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),sK52(X0,X1)) ) ),
inference(cnf_transformation,[],[f1837]) ).
tff(f2623,plain,
! [X0: 'Nat$'] : ~ $less('of_nat$'(X0),0),
inference(cnf_transformation,[],[f1011]) ).
tff(f2711,plain,
! [X2: 'Rows$',X0: 'A_cols_vec_rows_vec$',X1: 'A_rows_vec$'] :
( ~ 'fun_app$d'('consistent$'(X0),X1)
| ~ $less('of_nat$'('rank$'(X0)),$sum('of_nat$'('to_nat$'('greatest$'('uua$'(X0,X1)))),1))
| ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X0),X1)),X2) ) ),
inference(cnf_transformation,[],[f1912]) ).
tff(f2889,plain,
! [X0: 'Rows_bool_fun$',X1: 'Rows$'] :
( ~ 'fun_app$'(X0,X1)
| 'fun_app$'('fun_app$f'('less_eq$a',X1),'greatest$'(X0)) ),
inference(cnf_transformation,[],[f1407]) ).
tff(f2925,plain,
! [X0: 'Rows$'] :
( ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' )
| 'fun_app$'('uu$',X0) ),
inference(cnf_transformation,[],[f2036]) ).
tff(f2926,plain,
! [X0: 'Rows$'] :
( ~ 'fun_app$'('uu$',X0)
| ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) != 'zero$' ) ),
inference(cnf_transformation,[],[f2036]) ).
tff(f3027,plain,
! [X2: 'Rows$'] :
( ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X2) )
| 'fun_app$d'('consistent$'('a$'),'b$')
| ~ $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) ),
inference(cnf_transformation,[],[f2108]) ).
tff(f3028,plain,
( ~ 'fun_app$d'('consistent$'('a$'),'b$')
| $less('of_nat$'('rank$'('a$')),0)
| $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) ),
inference(cnf_transformation,[],[f2108]) ).
tff(f3030,plain,
( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK107) )
| ~ 'fun_app$d'('consistent$'('a$'),'b$')
| $less('of_nat$'('rank$'('a$')),0) ),
inference(cnf_transformation,[],[f2108]) ).
tff(f3060,plain,
! [X2: 'A_cols_vec_rows_vec$',X0: 'Rows$',X1: 'A_rows_vec$'] :
( ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X2),X1)),X0) )
| 'fun_app$'('uua$'(X2,X1),X0) ),
inference(cnf_transformation,[],[f2128]) ).
tff(f3061,plain,
! [X2: 'A_cols_vec_rows_vec$',X0: 'Rows$',X1: 'A_rows_vec$'] :
( ~ 'fun_app$'('uua$'(X2,X1),X0)
| ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'(X2),X1)),X0) ) ),
inference(cnf_transformation,[],[f2128]) ).
tff(f3101,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| $less(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f1285]) ).
tff(f3149,plain,
! [X0: 'Rows_bool_fun$',X1: 'Rows$'] :
( ~ 'fun_app$'(X0,X1)
| 'fun_app$'(X0,'greatest$'(X0)) ),
inference(cnf_transformation,[],[f1418]) ).
tff(f3400,plain,
( ~ 'fun_app$d'('consistent$'('a$'),'b$')
| $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uu$'))),1)) ),
inference(forward_subsumption_resolution,[],[f3028,f2623]) ).
tff(f3401,plain,
! [X2: 'Rows$'] :
( 'fun_app$d'('consistent$'('a$'),'b$')
| ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X2) )
| ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uu$'))))) ),
inference(forward_demodulation,[],[f3027,f2575]) ).
tff(f3402,plain,
( ~ 'fun_app$d'('consistent$'('a$'),'b$')
| ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK107) ) ),
inference(forward_subsumption_resolution,[],[f3030,f2623]) ).
tff(f3404,plain,
( ~ 'fun_app$d'('consistent$'('a$'),'b$')
| $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uu$'))))) ),
inference(forward_demodulation,[],[f3400,f2575]) ).
tff(f3409,plain,
( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK52('a$','b$')) )
| ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK107) )
| $less('of_nat$'('rank$'('a$')),0) ),
inference(resolution,[],[f3402,f2579]) ).
tff(f3411,plain,
( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK107) )
| ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK52('a$','b$')) ) ),
inference(forward_subsumption_resolution,[],[f3409,f2623]) ).
tff(f3417,plain,
( $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uu$')))))
| $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))),1))
| $less('of_nat$'('rank$'('a$')),0) ),
inference(resolution,[],[f3404,f2577]) ).
tff(f3422,plain,
( $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uu$')))))
| $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))),1)) ),
inference(forward_subsumption_resolution,[],[f3417,f2623]) ).
tff(f3424,plain,
( $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$'))))))
| $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uu$'))))) ),
inference(forward_demodulation,[],[f3422,f2575]) ).
tff(f3471,plain,
! [X0: 'Rows$',X1: 'Rows$'] :
( ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uu$')))))
| ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' )
| ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X1) )
| ~ $less('of_nat$'('rank$'('a$')),$sum('of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))),1)) ),
inference(resolution,[],[f3401,f2711]) ).
tff(f3474,plain,
! [X0: 'Rows$',X1: 'Rows$'] :
( ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' )
| ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uu$')))))
| ( 'zero$' = 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X1) )
| ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))))) ),
inference(forward_demodulation,[],[f3471,f2575]) ).
tff(f3476,plain,
( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK52('a$','b$')) )
| ( 'zero$' != 'zero$' )
| 'fun_app$'('uu$',sK107) ),
inference(superposition,[],[f3411,f2925]) ).
tff(f3478,plain,
( ( 'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK52('a$','b$')) )
| 'fun_app$'('uu$',sK107) ),
inference(trivial_inequality_removal,[],[f3476]) ).
tff(f3480,plain,
( 'fun_app$'('uu$',sK52('a$','b$'))
| 'fun_app$'('uu$',sK107)
| ( 'zero$' != 'zero$' ) ),
inference(superposition,[],[f3478,f2925]) ).
tff(f3481,plain,
( 'fun_app$'('uu$',sK107)
| 'fun_app$'('uu$',sK52('a$','b$')) ),
inference(trivial_inequality_removal,[],[f3480]) ).
tff(f3494,plain,
( 'fun_app$'('uu$',sK52('a$','b$'))
| 'fun_app$'('uu$',sK11('uu$')) ),
inference(resolution,[],[f3481,f2302]) ).
tff(f3512,plain,
( 'fun_app$'('uu$',sK52('a$','b$'))
| 'fun_app$'('uu$','greatest$'('uu$')) ),
inference(resolution,[],[f3481,f3149]) ).
tff(f3514,plain,
'fun_app$'('uu$',sK11('uu$')),
inference(forward_subsumption_resolution,[],[f3494,f2302]) ).
tff(f3516,plain,
'fun_app$'('uu$','greatest$'('uu$')),
inference(forward_subsumption_resolution,[],[f3512,f3149]) ).
tff(f3524,plain,
'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),sK11('uu$')),
inference(resolution,[],[f3514,f2926]) ).
tff(f3549,plain,
'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),'greatest$'('uu$')),
inference(resolution,[],[f3516,f2926]) ).
tff(f3871,plain,
( ( 'zero$' != 'zero$' )
| 'fun_app$'('uua$'('a$','b$'),sK11('uu$')) ),
inference(superposition,[],[f3524,f3060]) ).
tff(f3876,plain,
'fun_app$'('uua$'('a$','b$'),sK11('uu$')),
inference(trivial_inequality_removal,[],[f3871]) ).
tff(f3891,plain,
'fun_app$'('uua$'('a$','b$'),'greatest$'('uua$'('a$','b$'))),
inference(resolution,[],[f3876,f2560]) ).
tff(f3928,plain,
'zero$' != 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),'greatest$'('uua$'('a$','b$'))),
inference(resolution,[],[f3891,f3061]) ).
tff(f4035,plain,
( 'fun_app$'('uua$'('a$','b$'),'greatest$'('uu$'))
| ( 'zero$' != 'zero$' ) ),
inference(superposition,[],[f3549,f3060]) ).
tff(f4043,plain,
'fun_app$'('uua$'('a$','b$'),'greatest$'('uu$')),
inference(trivial_inequality_removal,[],[f4035]) ).
tff(f4060,plain,
'fun_app$'('fun_app$f'('less_eq$a','greatest$'('uu$')),'greatest$'('uua$'('a$','b$'))),
inference(resolution,[],[f4043,f2889]) ).
tff(f4066,plain,
! [X0: 'Rows$'] :
( ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uu$')))))
| ( 'zero$' != 'zero$' )
| ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' )
| ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))))) ),
inference(superposition,[],[f3549,f3474]) ).
tff(f4078,plain,
! [X0: 'Rows$'] :
( ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uu$')))))
| ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$'))))))
| ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' ) ),
inference(trivial_inequality_removal,[],[f4066]) ).
tff(f4087,plain,
~ $less('of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))),'of_nat$'('to_nat$'('greatest$'('uu$')))),
inference(resolution,[],[f4060,f2347]) ).
tff(f5319,plain,
( ( 'zero$' != 'zero$' )
| 'fun_app$'('uu$','greatest$'('uua$'('a$','b$'))) ),
inference(superposition,[],[f3928,f2925]) ).
tff(f5321,plain,
'fun_app$'('uu$','greatest$'('uua$'('a$','b$'))),
inference(trivial_inequality_removal,[],[f5319]) ).
tff(f5342,plain,
'fun_app$'('fun_app$f'('less_eq$a','greatest$'('uua$'('a$','b$'))),'greatest$'('uu$')),
inference(resolution,[],[f5321,f2889]) ).
tff(f5424,plain,
~ $less('of_nat$'('to_nat$'('greatest$'('uu$'))),'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$'))))),
inference(resolution,[],[f5342,f2347]) ).
tff(f5553,plain,
( $less('of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))),'of_nat$'('to_nat$'('greatest$'('uu$'))))
| ( 'of_nat$'('to_nat$'('greatest$'('uu$'))) = 'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))) ) ),
inference(resolution,[],[f5424,f3101]) ).
tff(f5558,plain,
'of_nat$'('to_nat$'('greatest$'('uu$'))) = 'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))),
inference(forward_subsumption_resolution,[],[f5553,f4087]) ).
tff(f5601,plain,
( $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$'))))))
| $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))))) ),
inference(backward_demodulation,[],[f3424,f5558]) ).
tff(f5632,plain,
! [X0: 'Rows$'] :
( ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$'))))))
| ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$'))))))
| ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' ) ),
inference(backward_demodulation,[],[f4078,f5558]) ).
tff(f5741,plain,
$less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$')))))),
inference(duplicate_literal_removal,[],[f5601]) ).
tff(f5743,plain,
! [X0: 'Rows$'] :
( ~ $less('of_nat$'('rank$'('a$')),$sum(1,'of_nat$'('to_nat$'('greatest$'('uua$'('a$','b$'))))))
| ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' ) ),
inference(duplicate_literal_removal,[],[f5632]) ).
tff(f5762,plain,
! [X0: 'Rows$'] : ( 'fun_app$a'('vec_nth$'('matrix_vector_mult$'('p_Gauss_Jordan$'('a$'),'b$')),X0) = 'zero$' ),
inference(forward_subsumption_resolution,[],[f5743,f5741]) ).
tff(f5770,plain,
'zero$' != 'zero$',
inference(backward_demodulation,[],[f3549,f5762]) ).
tff(f5812,plain,
$false,
inference(trivial_inequality_removal,[],[f5770]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP344_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 12:55:00 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.45/1.72 % (2007057)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.45/1.72 % (2007083)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=267486288:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.45/1.72 % (2007087)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3850809715:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.45/1.72 % (2007087)Instruction limit reached!
% 4.45/1.72 % (2007087)------------------------------
% 4.45/1.72 % (2007087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.72 % (2007087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.72 % (2007087)CaDiCaL version: 2.1.3
% 4.45/1.72 % (2007087)Termination reason: Instruction limit
% 4.45/1.72 % (2007087)Termination phase: Property scanning
% 4.45/1.72 % (2007087)Time elapsed: 0.035 s
% 4.45/1.72 % (2007087)Peak memory usage: 88 MB
% 4.45/1.72 % (2007087)Instructions burned: 34 (million)
% 4.45/1.72 % (2007082)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=559260679:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.45/1.72 % (2007085)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=837081808:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.45/1.72 % (2007086)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2692559119:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.45/1.72 % (2007084)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=4276249348:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.45/1.72 % (2007081)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1814353512:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.45/1.72 % (2007085)Instruction limit reached!
% 4.45/1.72 % (2007085)------------------------------
% 4.45/1.72 % (2007085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.72 % (2007085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.72 % (2007085)CaDiCaL version: 2.1.3
% 4.45/1.72 % (2007085)Termination reason: Instruction limit
% 4.45/1.72 % (2007085)Termination phase: Property scanning
% 4.45/1.72 % (2007085)Time elapsed: 0.005 s
% 4.45/1.72 % (2007085)Peak memory usage: 86 MB
% 4.45/1.72 % (2007085)Instructions burned: 5 (million)
% 4.45/1.72 % (2007084)Instruction limit reached!
% 4.45/1.72 % (2007084)------------------------------
% 4.45/1.72 % (2007084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.72 % (2007084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.72 % (2007084)CaDiCaL version: 2.1.3
% 4.45/1.72 % (2007084)Termination reason: Instruction limit
% 4.45/1.72 % (2007084)Termination phase: Property scanning
% 4.45/1.72 % (2007084)Time elapsed: 0.008 s
% 4.45/1.72 % (2007084)Peak memory usage: 86 MB
% 4.45/1.72 % (2007084)Instructions burned: 8 (million)
% 4.45/1.72 % (2007081)Instruction limit reached!
% 4.45/1.72 % (2007081)------------------------------
% 4.45/1.72 % (2007081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.72 % (2007081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.72 % (2007081)CaDiCaL version: 2.1.3
% 4.45/1.72 % (2007081)Termination reason: Instruction limit
% 4.45/1.72 % (2007081)Termination phase: Property scanning
% 4.45/1.72 % (2007081)Time elapsed: 0.012 s
% 4.45/1.72 % (2007081)Peak memory usage: 86 MB
% 4.45/1.72 % (2007081)Instructions burned: 13 (million)
% 4.45/1.72 % (2007083)Instruction limit reached!
% 4.45/1.72 % (2007083)------------------------------
% 4.45/1.72 % (2007083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.72 % (2007083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.72 % (2007083)CaDiCaL version: 2.1.3
% 4.45/1.72 % (2007083)Termination reason: Instruction limit
% 4.45/1.72 % (2007083)Termination phase: Saturation
% 4.45/1.72 % (2007083)Time elapsed: 0.124 s
% 4.45/1.72 % (2007083)Peak memory usage: 119 MB
% 4.45/1.72 % (2007083)Instructions burned: 201 (million)
% 4.45/1.72 % (2007086)Instruction limit reached!
% 4.45/1.72 % (2007086)------------------------------
% 4.45/1.72 % (2007086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.72 % (2007086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/2.00 % (2007086)CaDiCaL version: 2.1.3
% 6.14/2.00 % (2007086)Termination reason: Instruction limit
% 6.14/2.00 % (2007086)Termination phase: Saturation
% 6.14/2.00 % (2007086)Time elapsed: 0.067 s
% 6.14/2.00 % (2007086)Peak memory usage: 105 MB
% 6.14/2.00 % (2007086)Instructions burned: 46 (million)
% 6.14/2.00 % (2007090)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2474225930:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 6.14/2.00 % (2007090)Instruction limit reached!
% 6.14/2.00 % (2007090)------------------------------
% 6.14/2.00 % (2007090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/2.00 % (2007090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/2.00 % (2007090)CaDiCaL version: 2.1.3
% 6.14/2.00 % (2007090)Termination reason: Instruction limit
% 6.14/2.00 % (2007090)Termination phase: shuffling
% 6.14/2.00 % (2007090)Time elapsed: 0.015 s
% 6.14/2.00 % (2007090)Peak memory usage: 86 MB
% 6.14/2.00 % (2007090)Instructions burned: 14 (million)
% 6.14/2.00 % (2007097)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=127572731:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 6.14/2.00 % (2007097)Instruction limit reached!
% 6.14/2.00 % (2007097)------------------------------
% 6.14/2.00 % (2007097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/2.00 % (2007097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/2.00 % (2007097)CaDiCaL version: 2.1.3
% 6.14/2.00 % (2007097)Termination reason: Instruction limit
% 6.14/2.00 % (2007097)Termination phase: Preprocessing 3
% 6.14/2.00 % (2007097)Time elapsed: 0.012 s
% 6.14/2.00 % (2007097)Peak memory usage: 87 MB
% 6.14/2.00 % (2007097)Instructions burned: 17 (million)
% 6.14/2.00 % (2007100)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=1073325356:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.14/2.00 % (2007096)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=2754352157:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.14/2.00 % (2007100)Instruction limit reached!
% 6.14/2.00 % (2007100)------------------------------
% 6.14/2.00 % (2007100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/2.00 % (2007100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/2.00 % (2007100)CaDiCaL version: 2.1.3
% 6.14/2.00 % (2007100)Termination reason: Instruction limit
% 6.14/2.00 % (2007100)Termination phase: Clausification
% 6.14/2.00 % (2007100)Time elapsed: 0.016 s
% 6.14/2.00 % (2007100)Peak memory usage: 87 MB
% 6.14/2.00 % (2007100)Instructions burned: 28 (million)
% 6.14/2.00 % (2007098)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=391884568:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 6.14/2.00 % (2007096)Instruction limit reached!
% 6.14/2.00 % (2007096)------------------------------
% 6.14/2.00 % (2007096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/2.00 % (2007096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/2.00 % (2007096)CaDiCaL version: 2.1.3
% 6.14/2.00 % (2007096)Termination reason: Instruction limit
% 6.14/2.00 % (2007096)Termination phase: Property scanning
% 6.14/2.00 % (2007096)Time elapsed: 0.030 s
% 6.14/2.00 % (2007096)Peak memory usage: 88 MB
% 6.14/2.00 % (2007096)Instructions burned: 29 (million)
% 6.14/2.00 % (2007098)Instruction limit reached!
% 6.14/2.00 % (2007098)------------------------------
% 6.14/2.00 % (2007098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/2.00 % (2007098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/2.00 % (2007098)CaDiCaL version: 2.1.3
% 6.14/2.00 % (2007098)Termination reason: Instruction limit
% 6.14/2.00 % (2007098)Termination phase: Preprocessing 3
% 6.14/2.00 % (2007098)Time elapsed: 0.025 s
% 6.14/2.00 % (2007098)Peak memory usage: 87 MB
% 6.14/2.00 % (2007098)Instructions burned: 24 (million)
% 6.14/2.00 % (2007101)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1598600887:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.14/2.00 % (2007101)Instruction limit reached!
% 6.14/2.00 % (2007101)------------------------------
% 8.13/2.22 % (2007101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.22 % (2007101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.22 % (2007101)CaDiCaL version: 2.1.3
% 8.13/2.22 % (2007101)Termination reason: Instruction limit
% 8.13/2.22 % (2007101)Termination phase: Saturation
% 8.13/2.22 % (2007101)Time elapsed: 0.072 s
% 8.13/2.22 % (2007101)Peak memory usage: 90 MB
% 8.13/2.22 % (2007101)Instructions burned: 85 (million)
% 8.13/2.22 % (2007082)Instruction limit reached!
% 8.13/2.22 % (2007082)------------------------------
% 8.13/2.22 % (2007082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.22 % (2007082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.22 % (2007082)CaDiCaL version: 2.1.3
% 8.13/2.22 % (2007082)Termination reason: Instruction limit
% 8.13/2.22 % (2007082)Termination phase: Saturation
% 8.13/2.22 % (2007082)Time elapsed: 0.354 s
% 8.13/2.22 % (2007082)Peak memory usage: 119 MB
% 8.13/2.22 % (2007082)Instructions burned: 307 (million)
% 8.13/2.22 % (2007108)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=629693645:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 8.13/2.22 % (2007106)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2493928216:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 8.13/2.22 % (2007106)Instruction limit reached!
% 8.13/2.22 % (2007106)------------------------------
% 8.13/2.22 % (2007106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.22 % (2007106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.22 % (2007106)CaDiCaL version: 2.1.3
% 8.13/2.22 % (2007106)Termination reason: Instruction limit
% 8.13/2.22 % (2007106)Termination phase: Property scanning
% 8.13/2.22 % (2007106)Time elapsed: 0.003 s
% 8.13/2.22 % (2007106)Peak memory usage: 86 MB
% 8.13/2.22 % (2007106)Instructions burned: 2 (million)
% 8.13/2.22 % (2007112)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2207328726:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 8.13/2.22 % (2007112)Instruction limit reached!
% 8.13/2.22 % (2007112)------------------------------
% 8.13/2.22 % (2007112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.22 % (2007112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.22 % (2007112)CaDiCaL version: 2.1.3
% 8.13/2.22 % (2007112)Termination reason: Instruction limit
% 8.13/2.22 % (2007112)Termination phase: Property scanning
% 8.13/2.22 % (2007112)Time elapsed: 0.005 s
% 8.13/2.22 % (2007112)Peak memory usage: 85 MB
% 8.13/2.22 % (2007112)Instructions burned: 4 (million)
% 8.13/2.22 % (2007115)lrs+10_1_thi=all:si=on:fd=off:random_seed=1318237700:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 8.13/2.22 % (2007114)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1145486611:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 8.13/2.22 % (2007116)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=2217985312:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 8.13/2.22 % (2007116)Instruction limit reached!
% 8.13/2.22 % (2007116)------------------------------
% 8.13/2.22 % (2007116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.22 % (2007116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.22 % (2007116)CaDiCaL version: 2.1.3
% 8.13/2.22 % (2007116)Termination reason: Instruction limit
% 8.13/2.22 % (2007116)Termination phase: Property scanning
% 8.13/2.22 % (2007116)Time elapsed: 0.005 s
% 8.13/2.22 % (2007116)Peak memory usage: 85 MB
% 8.13/2.22 % (2007116)Instructions burned: 10 (million)
% 8.13/2.22 % (2007115)Instruction limit reached!
% 8.13/2.22 % (2007115)------------------------------
% 8.13/2.22 % (2007115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.22 % (2007115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.22 % (2007115)CaDiCaL version: 2.1.3
% 8.13/2.22 % (2007115)Termination reason: Instruction limit
% 8.13/2.22 % (2007115)Termination phase: Property scanning
% 8.13/2.22 % (2007115)Time elapsed: 0.052 s
% 8.13/2.22 % (2007115)Peak memory usage: 88 MB
% 8.13/2.22 % (2007115)Instructions burned: 53 (million)
% 9.26/2.44 % (2007117)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=406968484:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 9.26/2.44 % (2007117)Instruction limit reached!
% 9.26/2.44 % (2007117)------------------------------
% 9.26/2.44 % (2007117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.44 % (2007117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.44 % (2007117)CaDiCaL version: 2.1.3
% 9.26/2.44 % (2007117)Termination reason: Instruction limit
% 9.26/2.44 % (2007117)Termination phase: Property scanning
% 9.26/2.44 % (2007117)Time elapsed: 0.003 s
% 9.26/2.44 % (2007117)Peak memory usage: 85 MB
% 9.26/2.44 % (2007117)Instructions burned: 2 (million)
% 9.26/2.44 % (2007114)Instruction limit reached!
% 9.26/2.44 % (2007114)------------------------------
% 9.26/2.44 % (2007114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.44 % (2007114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.44 % (2007114)CaDiCaL version: 2.1.3
% 9.26/2.44 % (2007114)Termination reason: Instruction limit
% 9.26/2.44 % (2007114)Termination phase: Saturation
% 9.26/2.44 % (2007114)Time elapsed: 0.118 s
% 9.26/2.44 % (2007114)Peak memory usage: 131 MB
% 9.26/2.44 % (2007114)Instructions burned: 66 (million)
% 9.26/2.44 % (2007108)Instruction limit reached!
% 9.26/2.44 % (2007108)------------------------------
% 9.26/2.44 % (2007108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.44 % (2007108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.44 % (2007108)CaDiCaL version: 2.1.3
% 9.26/2.44 % (2007108)Termination reason: Instruction limit
% 9.26/2.44 % (2007108)Termination phase: Saturation
% 9.26/2.44 % (2007108)Time elapsed: 0.205 s
% 9.26/2.44 % (2007108)Peak memory usage: 91 MB
% 9.26/2.44 % (2007108)Instructions burned: 181 (million)
% 9.26/2.44 % (2007120)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3711152188:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 9.26/2.44 % (2007120)Instruction limit reached!
% 9.26/2.44 % (2007120)------------------------------
% 9.26/2.44 % (2007120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.44 % (2007120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.44 % (2007120)CaDiCaL version: 2.1.3
% 9.26/2.44 % (2007120)Termination reason: Instruction limit
% 9.26/2.44 % (2007120)Termination phase: shuffling
% 9.26/2.44 % (2007120)Time elapsed: 0.003 s
% 9.26/2.44 % (2007120)Peak memory usage: 85 MB
% 9.26/2.44 % (2007120)Instructions burned: 2 (million)
% 9.26/2.44 % (2007127)dis+10_1_si=on:random_seed=2127811760:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 9.26/2.44 % (2007127)Instruction limit reached!
% 9.26/2.44 % (2007127)------------------------------
% 9.26/2.44 % (2007127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.44 % (2007127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.44 % (2007127)CaDiCaL version: 2.1.3
% 9.26/2.44 % (2007127)Termination reason: Instruction limit
% 9.26/2.44 % (2007127)Termination phase: Property scanning
% 9.26/2.44 % (2007127)Time elapsed: 0.005 s
% 9.26/2.44 % (2007127)Peak memory usage: 86 MB
% 9.26/2.44 % (2007127)Instructions burned: 10 (million)
% 9.26/2.44 % (2007122)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1746956739:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 9.26/2.44 % (2007128)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1276831875:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 9.26/2.44 % (2007128)Instruction limit reached!
% 9.26/2.44 % (2007128)------------------------------
% 9.26/2.44 % (2007128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.44 % (2007128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.44 % (2007128)CaDiCaL version: 2.1.3
% 9.26/2.44 % (2007128)Termination reason: Instruction limit
% 9.26/2.44 % (2007128)Termination phase: Preprocessing 3
% 9.26/2.44 % (2007128)Time elapsed: 0.028 s
% 9.26/2.44 % (2007128)Peak memory usage: 87 MB
% 9.26/2.44 % (2007128)Instructions burned: 26 (million)
% 9.26/2.44 % (2007132)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3204960463:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi)
% 9.26/2.44 % (2007132)Instruction limit reached!
% 10.84/2.88 % (2007132)------------------------------
% 10.84/2.88 % (2007132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.88 % (2007132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.88 % (2007132)CaDiCaL version: 2.1.3
% 10.84/2.88 % (2007132)Termination reason: Instruction limit
% 10.84/2.88 % (2007132)Termination phase: Property scanning
% 10.84/2.88 % (2007132)Time elapsed: 0.004 s
% 10.84/2.88 % (2007132)Peak memory usage: 86 MB
% 10.84/2.88 % (2007132)Instructions burned: 3 (million)
% 10.84/2.88 % (2007140)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=4117331386:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi)
% 10.84/2.88 % (2007131)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3591077827: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_2991 on theBenchmark for (2991ds/35Mi)
% 10.84/2.88 % (2007140)Instruction limit reached!
% 10.84/2.88 % (2007140)------------------------------
% 10.84/2.88 % (2007140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.88 % (2007140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.88 % (2007140)CaDiCaL version: 2.1.3
% 10.84/2.88 % (2007140)Termination reason: Instruction limit
% 10.84/2.88 % (2007140)Termination phase: shuffling
% 10.84/2.88 % (2007140)Time elapsed: 0.007 s
% 10.84/2.88 % (2007140)Peak memory usage: 86 MB
% 10.84/2.88 % (2007140)Instructions burned: 14 (million)
% 10.84/2.88 % (2007122)Instruction limit reached!
% 10.84/2.88 % (2007122)------------------------------
% 10.84/2.88 % (2007122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.88 % (2007122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.88 % (2007122)CaDiCaL version: 2.1.3
% 10.84/2.88 % (2007122)Termination reason: Instruction limit
% 10.84/2.88 % (2007122)Termination phase: Saturation
% 10.84/2.88 % (2007122)Time elapsed: 0.168 s
% 10.84/2.88 % (2007122)Peak memory usage: 118 MB
% 10.84/2.88 % (2007122)Instructions burned: 127 (million)
% 10.84/2.88 % (2007134)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3041323197:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 10.84/2.88 % (2007134)Instruction limit reached!
% 10.84/2.88 % (2007134)------------------------------
% 10.84/2.88 % (2007134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.88 % (2007134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.88 % (2007134)CaDiCaL version: 2.1.3
% 10.84/2.88 % (2007134)Termination reason: Instruction limit
% 10.84/2.88 % (2007134)Termination phase: Property scanning
% 10.84/2.88 % (2007134)Time elapsed: 0.009 s
% 10.84/2.88 % (2007134)Peak memory usage: 86 MB
% 10.84/2.88 % (2007134)Instructions burned: 8 (million)
% 10.84/2.88 % (2007131)Instruction limit reached!
% 10.84/2.88 % (2007131)------------------------------
% 10.84/2.88 % (2007131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.88 % (2007131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.88 % (2007131)CaDiCaL version: 2.1.3
% 10.84/2.88 % (2007131)Termination reason: Instruction limit
% 10.84/2.88 % (2007131)Termination phase: Property scanning
% 10.84/2.88 % (2007131)Time elapsed: 0.035 s
% 10.84/2.88 % (2007131)Peak memory usage: 88 MB
% 10.84/2.88 % (2007131)Instructions burned: 36 (million)
% 10.84/2.88 % (2007137)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1080817220:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 10.84/2.88 % (2007147)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1672532475:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi)
% 10.84/2.88 % (2007142)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4098575593:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi)
% 10.84/2.88 % (2007145)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1320281396:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi)
% 10.84/2.88 % (2007150)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=4043093470:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2989 on theBenchmark for (2989ds/294Mi)
% 15.26/3.19 % (2007145)Instruction limit reached!
% 15.26/3.19 % (2007145)------------------------------
% 15.26/3.19 % (2007145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.26/3.19 % (2007145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/3.19 % (2007145)CaDiCaL version: 2.1.3
% 15.26/3.19 % (2007145)Termination reason: Instruction limit
% 15.26/3.19 % (2007145)Termination phase: Preprocessing 1
% 15.26/3.19 % (2007145)Time elapsed: 0.011 s
% 15.26/3.19 % (2007145)Peak memory usage: 86 MB
% 15.26/3.19 % (2007145)Instructions burned: 10 (million)
% 15.26/3.19 % (2007147)Instruction limit reached!
% 15.26/3.19 % (2007147)------------------------------
% 15.26/3.19 % (2007147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.26/3.19 % (2007147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/3.19 % (2007147)CaDiCaL version: 2.1.3
% 15.26/3.19 % (2007147)Termination reason: Instruction limit
% 15.26/3.19 % (2007147)Termination phase: Saturation
% 15.26/3.19 % (2007147)Time elapsed: 0.075 s
% 15.26/3.19 % (2007147)Peak memory usage: 131 MB
% 15.26/3.19 % (2007147)Instructions burned: 79 (million)
% 15.26/3.19 % (2007149)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=3419351124:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi)
% 15.26/3.19 % (2007151)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=797162235:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/130Mi)
% 15.26/3.19 % (2007149)Instruction limit reached!
% 15.26/3.19 % (2007149)------------------------------
% 15.26/3.19 % (2007149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.26/3.19 % (2007149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/3.19 % (2007149)CaDiCaL version: 2.1.3
% 15.26/3.19 % (2007149)Termination reason: Instruction limit
% 15.26/3.19 % (2007149)Termination phase: Saturation
% 15.26/3.19 % (2007149)Time elapsed: 0.075 s
% 15.26/3.19 % (2007149)Peak memory usage: 91 MB
% 15.26/3.19 % (2007149)Instructions burned: 75 (million)
% 15.26/3.19 % (2007158)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3707655509:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/40Mi)
% 15.26/3.19 % (2007137)Instruction limit reached!
% 15.26/3.19 % (2007137)------------------------------
% 15.26/3.19 % (2007137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.26/3.19 % (2007137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/3.19 % (2007137)CaDiCaL version: 2.1.3
% 15.26/3.19 % (2007137)Termination reason: Instruction limit
% 15.26/3.19 % (2007137)Termination phase: Saturation
% 15.26/3.19 % (2007137)Time elapsed: 0.345 s
% 15.26/3.19 % (2007137)Peak memory usage: 98 MB
% 15.26/3.19 % (2007137)Instructions burned: 370 (million)
% 15.26/3.19 % (2007142)Instruction limit reached!
% 15.26/3.19 % (2007142)------------------------------
% 15.26/3.19 % (2007142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.26/3.19 % (2007142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/3.19 % (2007142)CaDiCaL version: 2.1.3
% 15.26/3.19 % (2007142)Termination reason: Instruction limit
% 15.26/3.19 % (2007142)Termination phase: Saturation
% 15.26/3.19 % (2007142)Time elapsed: 0.241 s
% 15.26/3.19 % (2007142)Peak memory usage: 118 MB
% 15.26/3.19 % (2007142)Instructions burned: 226 (million)
% 15.26/3.19 % (2007158)Instruction limit reached!
% 15.26/3.19 % (2007158)------------------------------
% 15.26/3.19 % (2007158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.26/3.19 % (2007158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/3.19 % (2007158)CaDiCaL version: 2.1.3
% 15.26/3.19 % (2007158)Termination reason: Instruction limit
% 15.26/3.19 % (2007158)Termination phase: Clausification
% 15.26/3.19 % (2007158)Time elapsed: 0.021 s
% 15.26/3.19 % (2007158)Peak memory usage: 88 MB
% 15.26/3.19 % (2007158)Instructions burned: 40 (million)
% 15.26/3.19 % (2007151)Instruction limit reached!
% 15.26/3.19 % (2007151)------------------------------
% 15.26/3.19 % (2007151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.26/3.19 % (2007151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/3.19 % (2007151)CaDiCaL version: 2.1.3
% 15.26/3.19 % (2007151)Termination reason: Instruction limit
% 17.10/3.68 % (2007151)Termination phase: Saturation
% 17.10/3.68 % (2007151)Time elapsed: 0.165 s
% 17.10/3.68 % (2007151)Peak memory usage: 119 MB
% 17.10/3.68 % (2007151)Instructions burned: 130 (million)
% 17.10/3.68 % (2007157)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4118509586:i=131:rtra=on_2987 on theBenchmark for (2987ds/131Mi)
% 17.10/3.68 % (2007150)Instruction limit reached!
% 17.10/3.68 % (2007150)------------------------------
% 17.10/3.68 % (2007150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.10/3.68 % (2007150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.10/3.68 % (2007150)CaDiCaL version: 2.1.3
% 17.10/3.68 % (2007150)Termination reason: Instruction limit
% 17.10/3.68 % (2007150)Termination phase: Saturation
% 17.10/3.68 % (2007150)Time elapsed: 0.331 s
% 17.10/3.68 % (2007150)Peak memory usage: 93 MB
% 17.10/3.68 % (2007150)Instructions burned: 294 (million)
% 17.10/3.68 % (2007161)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3320540296:i=307:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/307Mi)
% 17.10/3.68 % (2007163)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2949528138:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/598Mi)
% 17.10/3.68 % (2007165)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=1542706366:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2985 on theBenchmark for (2985ds/259Mi)
% 17.10/3.68 % (2007164)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2891678864:i=131:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 17.10/3.68 % (2007157)Instruction limit reached!
% 17.10/3.68 % (2007157)------------------------------
% 17.10/3.68 % (2007157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.10/3.68 % (2007157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.10/3.68 % (2007157)CaDiCaL version: 2.1.3
% 17.10/3.68 % (2007157)Termination reason: Instruction limit
% 17.10/3.68 % (2007157)Termination phase: Saturation
% 17.10/3.68 % (2007157)Time elapsed: 0.199 s
% 17.10/3.68 % (2007157)Peak memory usage: 135 MB
% 17.10/3.68 % (2007157)Instructions burned: 131 (million)
% 17.10/3.68 % (2007167)dis+10_1_si=on:random_seed=2949223412:s2a=on:i=1000:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/1000Mi)
% 17.10/3.68 % (2007171)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1004733728:i=383:fsr=off:rtra=on:ev=force_2984 on theBenchmark for (2984ds/383Mi)
% 17.10/3.68 % (2007164)Instruction limit reached!
% 17.10/3.68 % (2007164)------------------------------
% 17.10/3.68 % (2007164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.10/3.68 % (2007164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.10/3.68 % (2007164)CaDiCaL version: 2.1.3
% 17.10/3.68 % (2007164)Termination reason: Instruction limit
% 17.10/3.68 % (2007164)Termination phase: Saturation
% 17.10/3.68 % (2007164)Time elapsed: 0.170 s
% 17.10/3.68 % (2007164)Peak memory usage: 119 MB
% 17.10/3.68 % (2007164)Instructions burned: 131 (million)
% 17.10/3.68 % (2007161)Instruction limit reached!
% 17.10/3.68 % (2007161)------------------------------
% 17.10/3.68 % (2007161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.10/3.68 % (2007161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.10/3.68 % (2007161)CaDiCaL version: 2.1.3
% 17.10/3.68 % (2007161)Termination reason: Instruction limit
% 17.10/3.68 % (2007161)Termination phase: Saturation
% 17.10/3.68 % (2007161)Time elapsed: 0.270 s
% 17.10/3.68 % (2007161)Peak memory usage: 93 MB
% 17.10/3.68 % (2007161)Instructions burned: 308 (million)
% 17.10/3.68 % (2007165)Instruction limit reached!
% 17.10/3.68 % (2007165)------------------------------
% 17.10/3.68 % (2007165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.10/3.68 % (2007165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.10/3.68 % (2007165)CaDiCaL version: 2.1.3
% 17.10/3.68 % (2007165)Termination reason: Instruction limit
% 17.10/3.68 % (2007165)Termination phase: Saturation
% 17.10/3.68 % (2007165)Time elapsed: 0.294 s
% 17.10/3.68 % (2007165)Peak memory usage: 118 MB
% 17.10/3.68 % (2007165)Instructions burned: 260 (million)
% 17.10/3.68 % (2007163)Instruction limit reached!
% 17.10/3.68 % (2007163)------------------------------
% 17.10/3.68 % (2007163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.77/4.12 % (2007163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.77/4.12 % (2007163)CaDiCaL version: 2.1.3
% 21.77/4.12 % (2007163)Termination reason: Instruction limit
% 21.77/4.12 % (2007163)Termination phase: Saturation
% 21.77/4.12 % (2007163)Time elapsed: 0.326 s
% 21.77/4.12 % (2007163)Peak memory usage: 139 MB
% 21.77/4.12 % (2007163)Instructions burned: 600 (million)
% 21.77/4.12 % (2007174)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4144009737:i=141:doe=on:rtra=on_2983 on theBenchmark for (2983ds/141Mi)
% 21.77/4.12 % (2007183)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=3946176563:i=39:ins=3:rtra=on_2981 on theBenchmark for (2981ds/39Mi)
% 21.77/4.12 % (2007177)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=786142249:i=65:nm=16:rtra=on_2981 on theBenchmark for (2981ds/65Mi)
% 21.77/4.12 % (2007179)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=333333475:i=121:nm=16:rtra=on_2981 on theBenchmark for (2981ds/121Mi)
% 21.77/4.12 % (2007174)Instruction limit reached!
% 21.77/4.12 % (2007174)------------------------------
% 21.77/4.12 % (2007174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.77/4.12 % (2007174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.77/4.12 % (2007174)CaDiCaL version: 2.1.3
% 21.77/4.12 % (2007174)Termination reason: Instruction limit
% 21.77/4.12 % (2007174)Termination phase: Saturation
% 21.77/4.12 % (2007174)Time elapsed: 0.149 s
% 21.77/4.12 % (2007174)Peak memory usage: 92 MB
% 21.77/4.12 % (2007174)Instructions burned: 141 (million)
% 21.77/4.12 % (2007183)Instruction limit reached!
% 21.77/4.12 % (2007183)------------------------------
% 21.77/4.12 % (2007183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.77/4.12 % (2007183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.77/4.12 % (2007183)CaDiCaL version: 2.1.3
% 21.77/4.12 % (2007183)Termination reason: Instruction limit
% 21.77/4.12 % (2007183)Termination phase: Property scanning
% 21.77/4.12 % (2007183)Time elapsed: 0.021 s
% 21.77/4.12 % (2007183)Peak memory usage: 88 MB
% 21.77/4.12 % (2007183)Instructions burned: 41 (million)
% 21.77/4.12 % (2007181)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=1860611867:s2a=on:i=128:s2at=5:ins=3:rtra=on_2981 on theBenchmark for (2981ds/128Mi)
% 21.77/4.12 % (2007177)Instruction limit reached!
% 21.77/4.12 % (2007177)------------------------------
% 21.77/4.12 % (2007177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.77/4.12 % (2007177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.77/4.12 % (2007177)CaDiCaL version: 2.1.3
% 21.77/4.12 % (2007177)Termination reason: Instruction limit
% 21.77/4.12 % (2007177)Termination phase: Saturation
% 21.77/4.12 % (2007177)Time elapsed: 0.066 s
% 21.77/4.12 % (2007177)Peak memory usage: 90 MB
% 21.77/4.12 % (2007177)Instructions burned: 65 (million)
% 21.77/4.12 % (2007179)Instruction limit reached!
% 21.77/4.12 % (2007179)------------------------------
% 21.77/4.12 % (2007179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.77/4.12 % (2007179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.77/4.12 % (2007179)CaDiCaL version: 2.1.3
% 21.77/4.12 % (2007179)Termination reason: Instruction limit
% 21.77/4.12 % (2007179)Termination phase: Saturation
% 21.77/4.12 % (2007179)Time elapsed: 0.132 s
% 21.77/4.12 % (2007179)Peak memory usage: 91 MB
% 21.77/4.12 % (2007179)Instructions burned: 121 (million)
% 21.77/4.12 % (2007171)Instruction limit reached!
% 21.77/4.12 % (2007171)------------------------------
% 21.77/4.12 % (2007171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.77/4.12 % (2007171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.77/4.12 % (2007171)CaDiCaL version: 2.1.3
% 21.77/4.12 % (2007171)Termination reason: Instruction limit
% 21.77/4.12 % (2007171)Termination phase: Saturation
% 21.77/4.12 % (2007171)Time elapsed: 0.402 s
% 21.77/4.12 % (2007171)Peak memory usage: 95 MB
% 21.77/4.12 % (2007171)Instructions burned: 383 (million)
% 21.77/4.12 % (2007189)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1879891268:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/329Mi)
% 24.88/4.62 % (2007181)Instruction limit reached!
% 24.88/4.62 % (2007181)------------------------------
% 24.88/4.62 % (2007181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.88/4.62 % (2007181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.88/4.62 % (2007181)CaDiCaL version: 2.1.3
% 24.88/4.62 % (2007181)Termination reason: Instruction limit
% 24.88/4.62 % (2007181)Termination phase: Saturation
% 24.88/4.62 % (2007181)Time elapsed: 0.159 s
% 24.88/4.62 % (2007181)Peak memory usage: 119 MB
% 24.88/4.62 % (2007181)Instructions burned: 128 (million)
% 24.88/4.62 % (2007188)dis+1010_1_to=kbo:si=on:random_seed=3904177466:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2979 on theBenchmark for (2979ds/175Mi)
% 24.88/4.62 % (2007191)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2461757794:s2a=on:i=483:doe=on:nm=32:rtra=on_2978 on theBenchmark for (2978ds/483Mi)
% 24.88/4.62 % (2007193)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2729579818:i=349:rtra=on_2978 on theBenchmark for (2978ds/349Mi)
% 24.88/4.62 % (2007189)Instruction limit reached!
% 24.88/4.62 % (2007189)------------------------------
% 24.88/4.62 % (2007189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.88/4.62 % (2007189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.88/4.62 % (2007189)CaDiCaL version: 2.1.3
% 24.88/4.62 % (2007189)Termination reason: Instruction limit
% 24.88/4.62 % (2007189)Termination phase: Saturation
% 24.88/4.62 % (2007189)Time elapsed: 0.185 s
% 24.88/4.62 % (2007189)Peak memory usage: 120 MB
% 24.88/4.62 % (2007189)Instructions burned: 329 (million)
% 24.88/4.62 % (2007192)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3251062143:thitd=on:i=215:nm=0:rtra=on:ev=force_2978 on theBenchmark for (2978ds/215Mi)
% 24.88/4.62 % (2007188)Instruction limit reached!
% 24.88/4.62 % (2007188)------------------------------
% 24.88/4.62 % (2007188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.88/4.62 % (2007188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.88/4.62 % (2007188)CaDiCaL version: 2.1.3
% 24.88/4.62 % (2007188)Termination reason: Instruction limit
% 24.88/4.62 % (2007188)Termination phase: Saturation
% 24.88/4.62 % (2007188)Time elapsed: 0.168 s
% 24.88/4.62 % (2007188)Peak memory usage: 93 MB
% 24.88/4.62 % (2007188)Instructions burned: 175 (million)
% 24.88/4.62 % (2007195)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1653748580:st=2:i=295:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/295Mi)
% 24.88/4.62 % (2007193)Instruction limit reached!
% 24.88/4.62 % (2007193)------------------------------
% 24.88/4.62 % (2007193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.88/4.62 % (2007193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.88/4.62 % (2007193)CaDiCaL version: 2.1.3
% 24.88/4.62 % (2007193)Termination reason: Instruction limit
% 24.88/4.62 % (2007193)Termination phase: Saturation
% 24.88/4.62 % (2007193)Time elapsed: 0.253 s
% 24.88/4.62 % (2007193)Peak memory usage: 120 MB
% 24.88/4.62 % (2007193)Instructions burned: 350 (million)
% 24.88/4.62 % (2007200)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1953225557:i=328:kws=inv_frequency:nm=20:rtra=on_2976 on theBenchmark for (2976ds/328Mi)
% 24.88/4.62 % (2007192)Instruction limit reached!
% 24.88/4.62 % (2007192)------------------------------
% 24.88/4.62 % (2007192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.88/4.62 % (2007192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.88/4.62 % (2007192)CaDiCaL version: 2.1.3
% 24.88/4.62 % (2007192)Termination reason: Instruction limit
% 24.88/4.62 % (2007192)Termination phase: Saturation
% 24.88/4.62 % (2007192)Time elapsed: 0.257 s
% 24.88/4.62 % (2007192)Peak memory usage: 138 MB
% 24.88/4.62 % (2007192)Instructions burned: 216 (million)
% 24.88/4.62 % (2007201)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2818518445:i=281:gtgl=2:rtra=on:gtg=all_2975 on theBenchmark for (2975ds/281Mi)
% 24.88/4.62 % (2007167)Instruction limit reached!
% 24.88/4.62 % (2007167)------------------------------
% 24.88/4.62 % (2007167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.88/4.62 % (2007167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.93/4.96 % (2007167)CaDiCaL version: 2.1.3
% 25.93/4.96 % (2007167)Termination reason: Instruction limit
% 25.93/4.96 % (2007167)Termination phase: Saturation
% 25.93/4.96 % (2007167)Time elapsed: 1.016 s
% 25.93/4.96 % (2007167)Peak memory usage: 99 MB
% 25.93/4.96 % (2007167)Instructions burned: 1000 (million)
% 25.93/4.96 % (2007203)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1609248371:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/484Mi)
% 25.93/4.96 % (2007195)Instruction limit reached!
% 25.93/4.96 % (2007195)------------------------------
% 25.93/4.96 % (2007195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.93/4.96 % (2007195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.93/4.96 % (2007195)CaDiCaL version: 2.1.3
% 25.93/4.96 % (2007195)Termination reason: Instruction limit
% 25.93/4.96 % (2007195)Termination phase: Saturation
% 25.93/4.96 % (2007195)Time elapsed: 0.267 s
% 25.93/4.96 % (2007195)Peak memory usage: 92 MB
% 25.93/4.96 % (2007195)Instructions burned: 295 (million)
% 25.93/4.96 % (2007205)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2049282826:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2973 on theBenchmark for (2973ds/321Mi)
% 25.93/4.96 % (2007191)Instruction limit reached!
% 25.93/4.96 % (2007191)------------------------------
% 25.93/4.96 % (2007191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.93/4.96 % (2007191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.93/4.96 % (2007191)CaDiCaL version: 2.1.3
% 25.93/4.96 % (2007191)Termination reason: Instruction limit
% 25.93/4.96 % (2007191)Termination phase: Saturation
% 25.93/4.96 % (2007191)Time elapsed: 0.580 s
% 25.93/4.96 % (2007191)Peak memory usage: 137 MB
% 25.93/4.96 % (2007191)Instructions burned: 484 (million)
% 25.93/4.96 % (2007207)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3225700809:i=416:rtra=on:gtg=position:ss=axioms_2973 on theBenchmark for (2973ds/416Mi)
% 25.93/4.96 % (2007203)Instruction limit reached!
% 25.93/4.96 % (2007203)------------------------------
% 25.93/4.96 % (2007203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.93/4.96 % (2007203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.93/4.96 % (2007203)CaDiCaL version: 2.1.3
% 25.93/4.96 % (2007203)Termination reason: Instruction limit
% 25.93/4.96 % (2007203)Termination phase: Saturation
% 25.93/4.96 % (2007203)Time elapsed: 0.204 s
% 25.93/4.96 % (2007203)Peak memory usage: 91 MB
% 25.93/4.96 % (2007203)Instructions burned: 485 (million)
% 25.93/4.96 % (2007209)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1011277361:i=471:thf=on:kws=precedence:rtra=on_2972 on theBenchmark for (2972ds/471Mi)
% 25.93/4.96 % (2007201)Instruction limit reached!
% 25.93/4.96 % (2007201)------------------------------
% 25.93/4.96 % (2007201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.93/4.96 % (2007201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.93/4.96 % (2007201)CaDiCaL version: 2.1.3
% 25.93/4.96 % (2007201)Termination reason: Instruction limit
% 25.93/4.96 % (2007201)Termination phase: Saturation
% 25.93/4.96 % (2007201)Time elapsed: 0.308 s
% 25.93/4.96 % (2007201)Peak memory usage: 119 MB
% 25.93/4.96 % (2007201)Instructions burned: 282 (million)
% 25.93/4.96 % (2007200)Instruction limit reached!
% 25.93/4.96 % (2007200)------------------------------
% 25.93/4.96 % (2007200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.93/4.96 % (2007200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.93/4.96 % (2007200)CaDiCaL version: 2.1.3
% 25.93/4.96 % (2007200)Termination reason: Instruction limit
% 25.93/4.96 % (2007200)Termination phase: Saturation
% 25.93/4.96 % (2007200)Time elapsed: 0.375 s
% 25.93/4.96 % (2007200)Peak memory usage: 119 MB
% 25.93/4.96 % (2007200)Instructions burned: 328 (million)
% 25.93/4.96 % (2007214)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1199329493:i=375:kws=inv_arity_squared:rtra=on_2970 on theBenchmark for (2970ds/375Mi)
% 25.93/4.96 % (2007205)Instruction limit reached!
% 25.93/4.96 % (2007205)------------------------------
% 25.93/4.96 % (2007205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.93/4.96 % (2007205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.93/4.96 % (2007205)CaDiCaL version: 2.1.3
% 25.93/4.96 % (2007205)Termination reason: Instruction limit
% 31.79/5.57 % (2007205)Termination phase: Saturation
% 31.79/5.57 % (2007205)Time elapsed: 0.288 s
% 31.79/5.57 % (2007205)Peak memory usage: 120 MB
% 31.79/5.57 % (2007205)Instructions burned: 322 (million)
% 31.79/5.57 % (2007212)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=26662472:avsq=on:i=276:avsqr=1,2:rtra=on_2971 on theBenchmark for (2971ds/276Mi)
% 31.79/5.57 % (2007217)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=355208756:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/387Mi)
% 31.79/5.57 % (2007218)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3885033669:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2970 on theBenchmark for (2970ds/513Mi)
% 31.79/5.57 % (2007221)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=888198527:i=334:rtra=on_2968 on theBenchmark for (2968ds/334Mi)
% 31.79/5.57 % (2007214)Instruction limit reached!
% 31.79/5.57 % (2007214)------------------------------
% 31.79/5.57 % (2007214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/5.57 % (2007214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/5.57 % (2007214)CaDiCaL version: 2.1.3
% 31.79/5.57 % (2007214)Termination reason: Instruction limit
% 31.79/5.57 % (2007214)Termination phase: Saturation
% 31.79/5.57 % (2007214)Time elapsed: 0.224 s
% 31.79/5.57 % (2007214)Peak memory usage: 121 MB
% 31.79/5.57 % (2007214)Instructions burned: 375 (million)
% 31.79/5.57 % (2007207)Instruction limit reached!
% 31.79/5.57 % (2007207)------------------------------
% 31.79/5.57 % (2007207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/5.57 % (2007207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/5.57 % (2007207)CaDiCaL version: 2.1.3
% 31.79/5.57 % (2007207)Termination reason: Instruction limit
% 31.79/5.57 % (2007207)Termination phase: Saturation
% 31.79/5.57 % (2007207)Time elapsed: 0.399 s
% 31.79/5.57 % (2007207)Peak memory usage: 120 MB
% 31.79/5.57 % (2007207)Instructions burned: 418 (million)
% 31.79/5.57 % (2007209)Instruction limit reached!
% 31.79/5.57 % (2007209)------------------------------
% 31.79/5.57 % (2007209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/5.57 % (2007209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/5.57 % (2007209)CaDiCaL version: 2.1.3
% 31.79/5.57 % (2007209)Termination reason: Instruction limit
% 31.79/5.57 % (2007209)Termination phase: Saturation
% 31.79/5.57 % (2007209)Time elapsed: 0.524 s
% 31.79/5.57 % (2007209)Peak memory usage: 120 MB
% 31.79/5.57 % (2007209)Instructions burned: 471 (million)
% 31.79/5.57 % (2007225)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2295533650:i=359:rtra=on:gtg=exists_top:ss=axioms_2967 on theBenchmark for (2967ds/359Mi)
% 31.79/5.57 % (2007212)Instruction limit reached!
% 31.79/5.57 % (2007212)------------------------------
% 31.79/5.57 % (2007212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/5.57 % (2007212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/5.57 % (2007212)CaDiCaL version: 2.1.3
% 31.79/5.57 % (2007212)Termination reason: Instruction limit
% 31.79/5.57 % (2007212)Termination phase: Saturation
% 31.79/5.57 % (2007212)Time elapsed: 0.348 s
% 31.79/5.57 % (2007212)Peak memory usage: 136 MB
% 31.79/5.57 % (2007212)Instructions burned: 276 (million)
% 31.79/5.57 % (2007221)Instruction limit reached!
% 31.79/5.57 % (2007221)------------------------------
% 31.79/5.57 % (2007221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/5.57 % (2007221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/5.57 % (2007221)CaDiCaL version: 2.1.3
% 31.79/5.57 % (2007221)Termination reason: Instruction limit
% 31.79/5.57 % (2007221)Termination phase: Saturation
% 31.79/5.57 % (2007221)Time elapsed: 0.227 s
% 31.79/5.57 % (2007221)Peak memory usage: 136 MB
% 31.79/5.57 % (2007221)Instructions burned: 335 (million)
% 31.79/5.57 % (2007226)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3058328966:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2966 on theBenchmark for (2966ds/341Mi)
% 31.79/5.57 % (2007229)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=1852670741:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2965 on theBenchmark for (2965ds/235Mi)
% 37.63/6.38 % (2007217)Instruction limit reached!
% 37.63/6.38 % (2007217)------------------------------
% 37.63/6.38 % (2007217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.63/6.38 % (2007217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.63/6.38 % (2007217)CaDiCaL version: 2.1.3
% 37.63/6.38 % (2007217)Termination reason: Instruction limit
% 37.63/6.38 % (2007217)Termination phase: Saturation
% 37.63/6.38 % (2007217)Time elapsed: 0.470 s
% 37.63/6.38 % (2007217)Peak memory usage: 120 MB
% 37.63/6.38 % (2007217)Instructions burned: 387 (million)
% 37.63/6.38 % (2007230)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3481231994:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2964 on theBenchmark for (2964ds/273Mi)
% 37.63/6.38 % (2007228)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1681452620:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2965 on theBenchmark for (2965ds/261Mi)
% 37.63/6.38 % (2007218)Instruction limit reached!
% 37.63/6.38 % (2007218)------------------------------
% 37.63/6.38 % (2007218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.63/6.38 % (2007218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.63/6.38 % (2007218)CaDiCaL version: 2.1.3
% 37.63/6.38 % (2007218)Termination reason: Instruction limit
% 37.63/6.38 % (2007218)Termination phase: Saturation
% 37.63/6.38 % (2007218)Time elapsed: 0.528 s
% 37.63/6.38 % (2007218)Peak memory usage: 94 MB
% 37.63/6.38 % (2007218)Instructions burned: 514 (million)
% 37.63/6.38 % (2007225)Instruction limit reached!
% 37.63/6.38 % (2007225)------------------------------
% 37.63/6.38 % (2007225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.63/6.38 % (2007225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.63/6.38 % (2007225)CaDiCaL version: 2.1.3
% 37.63/6.38 % (2007225)Termination reason: Instruction limit
% 37.63/6.38 % (2007225)Termination phase: Saturation
% 37.63/6.38 % (2007225)Time elapsed: 0.323 s
% 37.63/6.38 % (2007225)Peak memory usage: 92 MB
% 37.63/6.38 % (2007225)Instructions burned: 359 (million)
% 37.63/6.38 % (2007230)Instruction limit reached!
% 37.63/6.38 % (2007230)------------------------------
% 37.63/6.38 % (2007230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.63/6.38 % (2007230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.63/6.38 % (2007230)CaDiCaL version: 2.1.3
% 37.63/6.38 % (2007230)Termination reason: Instruction limit
% 37.63/6.38 % (2007230)Termination phase: Saturation
% 37.63/6.38 % (2007230)Time elapsed: 0.139 s
% 37.63/6.38 % (2007230)Peak memory usage: 93 MB
% 37.63/6.38 % (2007230)Instructions burned: 273 (million)
% 37.63/6.38 % (2007235)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1690618135:i=146:doe=on:rtra=on_2963 on theBenchmark for (2963ds/146Mi)
% 37.63/6.38 % (2007229)Instruction limit reached!
% 37.63/6.38 % (2007229)------------------------------
% 37.63/6.38 % (2007229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.63/6.38 % (2007229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.63/6.38 % (2007229)CaDiCaL version: 2.1.3
% 37.63/6.38 % (2007229)Termination reason: Instruction limit
% 37.63/6.38 % (2007229)Termination phase: Saturation
% 37.63/6.38 % (2007229)Time elapsed: 0.286 s
% 37.63/6.38 % (2007229)Peak memory usage: 118 MB
% 37.63/6.38 % (2007229)Instructions burned: 235 (million)
% 37.63/6.38 % (2007240)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3145227571:i=4428:doe=on:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/4428Mi)
% 37.63/6.38 % (2007226)Instruction limit reached!
% 37.63/6.38 % (2007226)------------------------------
% 37.63/6.38 % (2007226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.63/6.38 % (2007226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.63/6.38 % (2007226)CaDiCaL version: 2.1.3
% 37.63/6.38 % (2007226)Termination reason: Instruction limit
% 37.63/6.38 % (2007226)Termination phase: Saturation
% 37.63/6.38 % (2007226)Time elapsed: 0.413 s
% 37.63/6.38 % (2007226)Peak memory usage: 122 MB
% 37.63/6.38 % (2007226)Instructions burned: 341 (million)
% 37.63/6.38 % (2007244)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3772167322:i=1052:rtra=on_2961 on theBenchmark for (2961ds/1052Mi)
% 38.33/6.62 % (2007228)Instruction limit reached!
% 38.33/6.62 % (2007228)------------------------------
% 38.33/6.62 % (2007228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007228)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007228)Termination reason: Instruction limit
% 38.33/6.62 % (2007228)Termination phase: Saturation
% 38.33/6.62 % (2007228)Time elapsed: 0.301 s
% 38.33/6.62 % (2007228)Peak memory usage: 118 MB
% 38.33/6.62 % (2007228)Instructions burned: 261 (million)
% 38.33/6.62 % (2007235)Instruction limit reached!
% 38.33/6.62 % (2007235)------------------------------
% 38.33/6.62 % (2007235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007235)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007235)Termination reason: Instruction limit
% 38.33/6.62 % (2007235)Termination phase: Saturation
% 38.33/6.62 % (2007235)Time elapsed: 0.102 s
% 38.33/6.62 % (2007235)Peak memory usage: 91 MB
% 38.33/6.62 % (2007235)Instructions burned: 146 (million)
% 38.33/6.62 % (2007242)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=1628442331:avsq=on:i=276:avsqr=1,2:rtra=on_2962 on theBenchmark for (2962ds/276Mi)
% 38.33/6.62 % (2007249)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=206084473:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/655Mi)
% 38.33/6.62 % (2007251)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2718463607:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2960 on theBenchmark for (2960ds/1054Mi)
% 38.33/6.62 % (2007254)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4008453989:s2a=on:i=450:doe=on:nm=32:rtra=on_2960 on theBenchmark for (2960ds/450Mi)
% 38.33/6.62 % (2007253)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1025981308:i=107:rtra=on_2960 on theBenchmark for (2960ds/107Mi)
% 38.33/6.62 % (2007242)Instruction limit reached!
% 38.33/6.62 % (2007242)------------------------------
% 38.33/6.62 % (2007242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007242)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007242)Termination reason: Instruction limit
% 38.33/6.62 % (2007242)Termination phase: Saturation
% 38.33/6.62 % (2007242)Time elapsed: 0.324 s
% 38.33/6.62 % (2007242)Peak memory usage: 136 MB
% 38.33/6.62 % (2007242)Instructions burned: 276 (million)
% 38.33/6.62 % (2007253)Instruction limit reached!
% 38.33/6.62 % (2007253)------------------------------
% 38.33/6.62 % (2007253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007253)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007253)Termination reason: Instruction limit
% 38.33/6.62 % (2007253)Termination phase: Saturation
% 38.33/6.62 % (2007253)Time elapsed: 0.138 s
% 38.33/6.62 % (2007253)Peak memory usage: 118 MB
% 38.33/6.62 % (2007253)Instructions burned: 108 (million)
% 38.33/6.62 % (2007244)Instruction limit reached!
% 38.33/6.62 % (2007244)------------------------------
% 38.33/6.62 % (2007244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007244)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007244)Termination reason: Instruction limit
% 38.33/6.62 % (2007244)Termination phase: Saturation
% 38.33/6.62 % (2007244)Time elapsed: 0.572 s
% 38.33/6.62 % (2007244)Peak memory usage: 98 MB
% 38.33/6.62 % (2007244)Instructions burned: 1054 (million)
% 38.33/6.62 % (2007263)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 38.33/6.62 % (2007263)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1927962304:i=1090:aac=none:nm=0:rtra=on:rawr=on_2956 on theBenchmark for (2956ds/1090Mi)
% 38.33/6.62 % (2007264)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3744482735:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2956 on theBenchmark for (2956ds/130Mi)
% 38.33/6.62 % (2007265)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=4149672752:i=312:kws=inv_frequency:nm=20:rtra=on_2954 on theBenchmark for (2954ds/312Mi)
% 38.33/6.62 % (2007254)Instruction limit reached!
% 38.33/6.62 % (2007254)------------------------------
% 38.33/6.62 % (2007254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007254)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007254)Termination reason: Instruction limit
% 38.33/6.62 % (2007254)Termination phase: Saturation
% 38.33/6.62 % (2007254)Time elapsed: 0.517 s
% 38.33/6.62 % (2007254)Peak memory usage: 137 MB
% 38.33/6.62 % (2007254)Instructions burned: 450 (million)
% 38.33/6.62 % (2007264)Instruction limit reached!
% 38.33/6.62 % (2007264)------------------------------
% 38.33/6.62 % (2007264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007264)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007264)Termination reason: Instruction limit
% 38.33/6.62 % (2007264)Termination phase: Saturation
% 38.33/6.62 % (2007264)Time elapsed: 0.162 s
% 38.33/6.62 % (2007264)Peak memory usage: 118 MB
% 38.33/6.62 % (2007264)Instructions burned: 130 (million)
% 38.33/6.62 % (2007249)Instruction limit reached!
% 38.33/6.62 % (2007249)------------------------------
% 38.33/6.62 % (2007249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007249)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007249)Termination reason: Instruction limit
% 38.33/6.62 % (2007249)Termination phase: Saturation
% 38.33/6.62 % (2007249)Time elapsed: 0.621 s
% 38.33/6.62 % (2007249)Peak memory usage: 102 MB
% 38.33/6.62 % (2007249)Instructions burned: 656 (million)
% 38.33/6.62 % (2007265)Instruction limit reached!
% 38.33/6.62 % (2007265)------------------------------
% 38.33/6.62 % (2007265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007265)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007265)Termination reason: Instruction limit
% 38.33/6.62 % (2007265)Termination phase: Saturation
% 38.33/6.62 % (2007265)Time elapsed: 0.190 s
% 38.33/6.62 % (2007265)Peak memory usage: 119 MB
% 38.33/6.62 % (2007265)Instructions burned: 313 (million)
% 38.33/6.62 % (2007269)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1350963722:i=491:doe=on:rtra=on:gtg=position_2952 on theBenchmark for (2952ds/491Mi)
% 38.33/6.62 % (2007270)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=831581864:s2a=on:i=835:s2at=2:rtra=on_2952 on theBenchmark for (2952ds/835Mi)
% 38.33/6.62 % (2007271)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2204571182:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2952 on theBenchmark for (2952ds/307Mi)
% 38.33/6.62 % (2007272)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1983558531:i=776:doe=on:rtra=on_2951 on theBenchmark for (2951ds/776Mi)
% 38.33/6.62 % (2007251)Instruction limit reached!
% 38.33/6.62 % (2007251)------------------------------
% 38.33/6.62 % (2007251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007251)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007251)Termination reason: Instruction limit
% 38.33/6.62 % (2007251)Termination phase: Saturation
% 38.33/6.62 % (2007251)Time elapsed: 0.998 s
% 38.33/6.62 % (2007251)Peak memory usage: 95 MB
% 38.33/6.62 % (2007251)Instructions burned: 1054 (million)
% 38.33/6.62 % (2007271)First to succeed.
% 38.33/6.62 % (2007271)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2007057"
% 38.33/6.62 % (2007279)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2828805141:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2948 on theBenchmark for (2948ds/646Mi)
% 38.33/6.62 % (2007269)Instruction limit reached!
% 38.33/6.62 % (2007269)------------------------------
% 38.33/6.62 % (2007269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007269)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007269)Termination reason: Instruction limit
% 38.33/6.62 % (2007269)Termination phase: Saturation
% 38.33/6.62 % (2007269)Time elapsed: 0.427 s
% 38.33/6.62 % (2007269)Peak memory usage: 93 MB
% 38.33/6.62 % (2007269)Instructions burned: 493 (million)
% 38.33/6.62 % (2007272)Instruction limit reached!
% 38.33/6.62 % (2007272)------------------------------
% 38.33/6.62 % (2007272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.33/6.62 % (2007272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.33/6.62 % (2007272)CaDiCaL version: 2.1.3
% 38.33/6.62 % (2007272)Termination reason: Instruction limit
% 38.33/6.62 % (2007272)Termination phase: Saturation
% 38.33/6.62 % (2007272)Time elapsed: 0.453 s
% 38.33/6.62 % (2007272)Peak memory usage: 123 MB
% 38.33/6.62 % (2007272)Instructions burned: 776 (million)
% 38.33/6.62 % (2007281)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=1554896478:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2946 on theBenchmark for (2946ds/784Mi)
% 38.33/6.62 % (2007271)Refutation found. Thanks to Tanya!
% 38.33/6.62 % SZS status Theorem for theBenchmark
% 38.33/6.62 % SZS output start Proof for theBenchmark
% See solution above
% 40.24/6.95 % (2007271)------------------------------
% 40.24/6.95 % (2007271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.24/6.95 % (2007271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.24/6.95 % (2007271)CaDiCaL version: 2.1.3
% 40.24/6.95 % (2007271)Termination reason: Refutation
% 40.24/6.95 % (2007271)Time elapsed: 0.217 s
% 40.24/6.95 % (2007271)Peak memory usage: 94 MB
% 40.24/6.95 % (2007271)Instructions burned: 299 (million)
% 40.24/6.95 % (2007271)------------------------------
% 40.24/6.95 % (2007271)------------------------------
% 40.24/6.95 % (2007057)Success in time 5.617 s
% 40.24/6.95 % Vampire exiting
%------------------------------------------------------------------------------