%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP319_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 : n016.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:36 AM UTC 2026
% Result : Theorem 24.06s 4.82s
% Output : Refutation 27.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 12
% Syntax : Number of formulae : 98 ( 31 unt; 0 typ; 0 def)
% Number of atoms : 376 ( 105 equ)
% Maximal formula atoms : 26 ( 3 avg)
% Number of connectives : 456 ( 178 ~; 143 |; 99 &)
% ( 16 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 54 ( 52 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 33 ( 31 usr; 1 prp; 0-3 aty)
% Number of functors : 213 ( 213 usr; 33 con; 0-2 aty)
% Number of variables : 214 ( 177 !; 37 ?; 214 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'C_nat_fun$': $tType ).
tff(type_def_6,type,
'Int_bool_fun$': $tType ).
tff(type_def_7,type,
'Nat_b_vec_b_vec$': $tType ).
tff(type_def_8,type,
'Int_c_fun$': $tType ).
tff(type_def_9,type,
'Nat_nat_bool_fun_fun$': $tType ).
tff(type_def_10,type,
'B_b_fun$': $tType ).
tff(type_def_11,type,
'C_a_b_vec_bool_fun_fun$': $tType ).
tff(type_def_12,type,
'A_b_vec_b_vec_b_vec$': $tType ).
tff(type_def_13,type,
'C_c_fun$': $tType ).
tff(type_def_14,type,
'Int_b_vec_b_vec$': $tType ).
tff(type_def_15,type,
'Int_b_fun$': $tType ).
tff(type_def_16,type,
'Int_set$': $tType ).
tff(type_def_17,type,
'Int_int_fun$': $tType ).
tff(type_def_18,type,
'A_b_vec_b_vec$': $tType ).
tff(type_def_19,type,
'B$': $tType ).
tff(type_def_20,type,
'A_b_vec_c_vec$': $tType ).
tff(type_def_21,type,
'Num_bool_fun$': $tType ).
tff(type_def_22,type,
'A_b_vec_c_vec_b_vec_b_vec$': $tType ).
tff(type_def_23,type,
'C_a_b_vec_fun$': $tType ).
tff(type_def_24,type,
'Int_b_vec_c_vec$': $tType ).
tff(type_def_25,type,
'B_nat_fun$': $tType ).
tff(type_def_26,type,
'Nat_nat_fun$': $tType ).
tff(type_def_27,type,
'Int_nat_fun$': $tType ).
tff(type_def_28,type,
'C$': $tType ).
tff(type_def_29,type,
'A_b_vec_b_vec_c_vec$': $tType ).
tff(type_def_30,type,
'Nat$': $tType ).
tff(type_def_31,type,
'B_int_fun$': $tType ).
tff(type_def_32,type,
'C_b_fun$': $tType ).
tff(type_def_33,type,
'A_b_vec$': $tType ).
tff(type_def_34,type,
'C_int_fun$': $tType ).
tff(type_def_35,type,
'B_a_fun$': $tType ).
tff(type_def_36,type,
'Num$': $tType ).
tff(type_def_37,type,
'Nat_b_vec_c_vec$': $tType ).
tff(type_def_38,type,
'Nat_b_vec$': $tType ).
tff(type_def_39,type,
'Num_set$': $tType ).
tff(type_def_40,type,
tlbool: $tType ).
tff(type_def_41,type,
'A_b_vec_c_vec_b_vec$': $tType ).
tff(type_def_42,type,
'A_bool_fun$': $tType ).
tff(type_def_43,type,
'B_b_bool_fun_fun$': $tType ).
tff(type_def_44,type,
'A$': $tType ).
tff(type_def_45,type,
'Nat_b_fun$': $tType ).
tff(type_def_46,type,
'A_a_fun$': $tType ).
tff(type_def_47,type,
'Int_int_bool_fun_fun$': $tType ).
tff(type_def_48,type,
'Int_b_vec$': $tType ).
tff(type_def_49,type,
'A_b_vec_bool_fun$': $tType ).
tff(type_def_50,type,
'Nat_bool_fun$': $tType ).
tff(type_def_51,type,
'Nat_set$': $tType ).
tff(type_def_52,type,
'B_c_fun$': $tType ).
tff(type_def_53,type,
'Nat_int_fun$': $tType ).
tff(type_def_54,type,
'B_a_bool_fun_fun$': $tType ).
tff(type_def_55,type,
'A_b_vec_c_vec_b_vec_c_vec$': $tType ).
tff(type_def_56,type,
'B_bool_fun$': $tType ).
tff(func_def_0,type,
'less$a': 'B_b_bool_fun_fun$' ).
tff(func_def_1,type,
'vec_nth$m': ( 'Int_b_vec_b_vec$' * 'B$' ) > 'Int_b_vec$' ).
tff(func_def_2,type,
'fun_app$o': ( 'B_int_fun$' * 'B$' ) > $int ).
tff(func_def_3,type,
'fun_app$ab': ( 'Nat_b_fun$' * 'Nat$' ) > 'B$' ).
tff(func_def_4,type,
'dbl_inc$': 'Int_int_fun$' ).
tff(func_def_5,type,
'fun_app$y': ( 'C_b_fun$' * 'C$' ) > 'B$' ).
tff(func_def_6,type,
'vec_nth$f': ( 'A_b_vec_b_vec_c_vec$' * 'C$' ) > 'A_b_vec_b_vec$' ).
tff(func_def_7,type,
'uuc$': ( 'Int_b_vec_c_vec$' * 'C$' ) > 'B_bool_fun$' ).
tff(func_def_8,type,
'zero$e': 'Int_set$' ).
tff(func_def_9,type,
'uua$': ( 'A_b_vec_c_vec$' * 'C$' ) > 'B_bool_fun$' ).
tff(func_def_10,type,
'uub$': ( 'Int_b_vec_c_vec$' * 'C$' ) > 'B_bool_fun$' ).
tff(func_def_11,type,
'vec_nth$l': ( 'Int_b_vec_c_vec$' * 'C$' ) > 'Int_b_vec$' ).
tff(func_def_12,type,
'uuj$': 'Int_b_vec_b_vec$' > 'B_b_bool_fun_fun$' ).
tff(func_def_13,type,
'uur$': 'A_b_vec_b_vec$' > 'B_b_bool_fun_fun$' ).
tff(func_def_14,type,
'fun_app$l': ( 'B_b_bool_fun_fun$' * 'B$' ) > 'B_bool_fun$' ).
tff(func_def_15,type,
'triangle$': 'Nat_nat_fun$' ).
tff(func_def_16,type,
'uuh$': ( 'Nat_b_vec_c_vec$' * 'C$' ) > 'B_bool_fun$' ).
tff(func_def_17,type,
'uu$': 'C$' > 'B_bool_fun$' ).
tff(func_def_18,type,
'fun_app$u': ( 'Nat_nat_bool_fun_fun$' * 'Nat$' ) > 'Nat_bool_fun$' ).
tff(func_def_19,type,
'plus$f': ( 'Num_set$' * 'Num_set$' ) > 'Num_set$' ).
tff(func_def_20,type,
'fun_app$t': ( 'C_a_b_vec_bool_fun_fun$' * 'C$' ) > 'A_b_vec_bool_fun$' ).
tff(func_def_21,type,
'uuo$': 'A_b_vec_b_vec_b_vec$' > 'B_b_bool_fun_fun$' ).
tff(func_def_22,type,
'vec_nth$b': ( 'A_b_vec_c_vec_b_vec$' * 'B$' ) > 'A_b_vec_c_vec$' ).
tff(func_def_23,type,
'fun_app$a': ( 'Int_int_fun$' * $int ) > $int ).
tff(func_def_24,type,
'least$a': 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_25,type,
'axis$a': ( 'B$' * 'A$' ) > 'A_b_vec$' ).
tff(func_def_26,type,
'fun_app$g': ( 'Nat_int_fun$' * 'Nat$' ) > $int ).
tff(func_def_27,type,
'from_nat$': 'Nat_b_fun$' ).
tff(func_def_28,type,
'of_nat$a': 'Nat_nat_fun$' ).
tff(func_def_29,type,
'nat$': 'Int_nat_fun$' ).
tff(func_def_30,type,
'one$c': 'A$' ).
tff(func_def_31,type,
'uux$': 'Int_int_bool_fun_fun$' ).
tff(func_def_32,type,
'fun_app$v': ( 'Int_c_fun$' * $int ) > 'C$' ).
tff(func_def_33,type,
'fun_app$z': ( 'C_nat_fun$' * 'C$' ) > 'Nat$' ).
tff(func_def_34,type,
'of_nat$': 'Nat_int_fun$' ).
tff(func_def_35,type,
'uum$': 'A_b_vec_c_vec_b_vec_b_vec$' > 'B_b_bool_fun_fun$' ).
tff(func_def_36,type,
'fun_app$f': ( 'Int_nat_fun$' * $int ) > 'Nat$' ).
tff(func_def_37,type,
'uuz$': 'Nat_nat_fun$' ).
tff(func_def_38,type,
'plus$d': ( 'Int_set$' * 'Int_set$' ) > 'Int_set$' ).
tff(func_def_39,type,
'of_int$': 'Int_int_fun$' ).
tff(func_def_40,type,
'axis$': ( 'C$' * 'A_b_vec$' ) > 'A_b_vec_c_vec$' ).
tff(func_def_41,type,
'to_nat$': 'B_nat_fun$' ).
tff(func_def_42,type,
'fun_app$i': ( 'B_a_fun$' * 'B$' ) > 'A$' ).
tff(func_def_43,type,
tltrue: tlbool ).
tff(func_def_44,type,
'plus$': 'Nat$' > 'Nat_nat_fun$' ).
tff(func_def_45,type,
'map_matrix$': ( 'A_a_fun$' * 'A_b_vec_c_vec$' ) > 'A_b_vec_c_vec$' ).
tff(func_def_46,type,
'one$b': 'B$' ).
tff(func_def_47,type,
'uva$': 'Int_int_fun$' ).
tff(func_def_48,type,
'one$': 'Nat$' ).
tff(func_def_49,type,
'uug$': ( 'A_b_vec_b_vec_c_vec$' * 'C$' ) > 'B_bool_fun$' ).
tff(func_def_50,type,
'uup$': 'Nat_b_vec_b_vec$' > 'B_b_bool_fun_fun$' ).
tff(func_def_51,type,
'fun_app$x': ( 'C_int_fun$' * 'C$' ) > $int ).
tff(func_def_52,type,
'fun_app$aa': ( 'B_c_fun$' * 'B$' ) > 'C$' ).
tff(func_def_53,type,
'uul$': 'A_b_vec_c_vec_b_vec_b_vec$' > 'B_b_bool_fun_fun$' ).
tff(func_def_54,type,
'uun$': 'A_b_vec_b_vec_b_vec$' > 'B_b_bool_fun_fun$' ).
tff(func_def_55,type,
'collect$': 'Nat_bool_fun$' > 'Nat_set$' ).
tff(func_def_56,type,
'least$': 'B_bool_fun$' > 'B$' ).
tff(func_def_57,type,
'vec_nth$j': ( 'Nat_b_vec_b_vec$' * 'B$' ) > 'Nat_b_vec$' ).
tff(func_def_58,type,
'plus$b': 'B$' > 'B_b_fun$' ).
tff(func_def_59,type,
'ncols$': 'A_b_vec_c_vec$' > 'Nat$' ).
tff(func_def_60,type,
'fun_app$j': ( 'C_a_b_vec_fun$' * 'C$' ) > 'A_b_vec$' ).
tff(func_def_61,type,
'of_nat_aux$a': ( 'Int_int_fun$' * 'Nat$' ) > 'Int_int_fun$' ).
tff(func_def_62,type,
'uui$': ( 'Nat_b_vec_c_vec$' * 'C$' ) > 'B_bool_fun$' ).
tff(func_def_63,type,
'uut$': ( 'A_b_vec_c_vec$' * 'C$' ) > 'B_bool_fun$' ).
tff(func_def_64,type,
'zero$a': 'A_b_vec_c_vec$' ).
tff(func_def_65,type,
'uuv$': 'Num_set$' > 'Num_bool_fun$' ).
tff(func_def_66,type,
'fun_app$k': ( 'C_c_fun$' * 'C$' ) > 'C$' ).
tff(func_def_67,type,
'collect$b': 'Int_bool_fun$' > 'Int_set$' ).
tff(func_def_68,type,
'one$e': 'A_b_vec_c_vec$' ).
tff(func_def_69,type,
'fun_app$': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_70,type,
'plus$a': 'C$' > 'C_c_fun$' ).
tff(func_def_71,type,
'vec_nth$c': ( 'A_b_vec_c_vec_b_vec_c_vec$' * 'C$' ) > 'A_b_vec_c_vec_b_vec$' ).
tff(func_def_72,type,
'of_nat_aux$': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat_nat_fun$' ).
tff(func_def_73,type,
'fun_app$p': ( 'A_a_fun$' * 'A$' ) > 'A$' ).
tff(func_def_74,type,
'reduced_row_echelon_form_upt_k$': 'A_b_vec_c_vec$' > 'Nat_bool_fun$' ).
tff(func_def_75,type,
'uuf$': ( 'A_b_vec_b_vec_c_vec$' * 'C$' ) > 'B_bool_fun$' ).
tff(func_def_76,type,
'fun_app$w': ( 'Int_b_fun$' * $int ) > 'B$' ).
tff(func_def_77,type,
'vec_nth$d': ( 'A_b_vec_c_vec_b_vec_b_vec$' * 'B$' ) > 'A_b_vec_c_vec_b_vec$' ).
tff(func_def_78,type,
'one$d': 'A_b_vec$' ).
tff(func_def_79,type,
'vec_nth$a': 'A_b_vec_c_vec$' > 'C_a_b_vec_fun$' ).
tff(func_def_80,type,
'less_eq$': 'Nat_nat_bool_fun_fun$' ).
tff(func_def_81,type,
'num_of_nat$': 'Nat$' > 'Num$' ).
tff(func_def_82,type,
'zero$b': 'A_b_vec$' ).
tff(func_def_83,type,
'less$b': 'Nat_nat_bool_fun_fun$' ).
tff(func_def_84,type,
'zero$': 'A$' ).
tff(func_def_85,type,
'collect$a': 'Num_bool_fun$' > 'Num_set$' ).
tff(func_def_86,type,
tlfalse: tlbool ).
tff(func_def_87,type,
'vec$a': 'A$' > 'A_b_vec$' ).
tff(func_def_88,type,
'fun_app$c': ( 'Int_int_bool_fun_fun$' * $int ) > 'Int_bool_fun$' ).
tff(func_def_89,type,
'vec_nth$': 'A_b_vec$' > 'B_a_fun$' ).
tff(func_def_90,type,
'row$': ( 'C$' * 'A_b_vec_c_vec$' ) > 'A_b_vec$' ).
tff(func_def_91,type,
'vec$': 'A_b_vec$' > 'A_b_vec_c_vec$' ).
tff(func_def_92,type,
'zero$d': 'Nat_set$' ).
tff(func_def_93,type,
'uuw$': 'Int_set$' > 'Int_bool_fun$' ).
tff(func_def_94,type,
'vec_nth$h': 'Nat_b_vec$' > 'B_nat_fun$' ).
tff(func_def_95,type,
'vec_nth$i': ( 'Nat_b_vec_c_vec$' * 'C$' ) > 'Nat_b_vec$' ).
tff(func_def_96,type,
'fun_app$r': ( 'B_a_bool_fun_fun$' * 'B$' ) > 'A_bool_fun$' ).
tff(func_def_97,type,
'one$a': 'C$' ).
tff(func_def_98,type,
'vec_nth$e': ( 'A_b_vec_b_vec$' * 'B$' ) > 'A_b_vec$' ).
tff(func_def_99,type,
'fun_app$m': ( 'B_b_fun$' * 'B$' ) > 'B$' ).
tff(func_def_100,type,
'suc$': 'Nat_nat_fun$' ).
tff(func_def_101,type,
'uuu$': 'Nat_set$' > 'Nat_bool_fun$' ).
tff(func_def_102,type,
'uuq$': 'Nat_b_vec_b_vec$' > 'B_b_bool_fun_fun$' ).
tff(func_def_103,type,
'uuy$': 'Nat_bool_fun$' > 'Nat_bool_fun$' ).
tff(func_def_104,type,
'uus$': 'A_b_vec_b_vec$' > 'B_b_bool_fun_fun$' ).
tff(func_def_105,type,
'vec_nth$g': ( 'A_b_vec_b_vec_b_vec$' * 'B$' ) > 'A_b_vec_b_vec$' ).
tff(func_def_106,type,
'fun_app$n': ( 'B_nat_fun$' * 'B$' ) > 'Nat$' ).
tff(func_def_107,type,
'dbl_dec$': 'Int_int_fun$' ).
tff(func_def_108,type,
'a$': 'A_b_vec_c_vec$' ).
tff(func_def_109,type,
'uuk$': 'Int_b_vec_b_vec$' > 'B_b_bool_fun_fun$' ).
tff(func_def_110,type,
'zero$c': 'Nat$' ).
tff(func_def_111,type,
'plus$c': ( 'Nat_set$' * 'Nat_set$' ) > 'Nat_set$' ).
tff(func_def_112,type,
'plus$e': ( 'Num$' * 'Num$' ) > 'Num$' ).
tff(func_def_113,type,
'uue$': ( 'A_b_vec_c_vec_b_vec_c_vec$' * 'C$' ) > 'B_bool_fun$' ).
tff(func_def_114,type,
'uud$': ( 'A_b_vec_c_vec_b_vec_c_vec$' * 'C$' ) > 'B_bool_fun$' ).
tff(func_def_115,type,
'vec_nth$k': 'Int_b_vec$' > 'B_int_fun$' ).
tff(func_def_120,type,
sK0: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_121,type,
sK1: 'Nat$' > 'Nat$' ).
tff(func_def_122,type,
sK2: 'C_c_fun$' > 'C$' ).
tff(func_def_123,type,
sK3: 'C_c_fun$' > 'C$' ).
tff(func_def_124,type,
sK4: $int > $int ).
tff(func_def_125,type,
sK5: ( 'Nat_bool_fun$' * $int ) > 'Nat$' ).
tff(func_def_126,type,
sK6: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_127,type,
sK7: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_128,type,
sK8: 'Nat$' > 'Nat$' ).
tff(func_def_129,type,
sK9: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_130,type,
sK10: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_131,type,
sK11: ( 'B_bool_fun$' * 'B_bool_fun$' ) > 'B$' ).
tff(func_def_132,type,
sK12: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_133,type,
sK13: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_134,type,
sK14: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_135,type,
sK15: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_136,type,
sK16: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_137,type,
sK17: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_138,type,
sK18: ( 'B_bool_fun$' * 'B_bool_fun$' ) > 'B$' ).
tff(func_def_139,type,
sK19: $int > 'Nat$' ).
tff(func_def_140,type,
sK20: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_141,type,
sK21: 'Nat_bool_fun$' > $int ).
tff(func_def_142,type,
sK22: 'A_b_vec_c_vec$' > 'C$' ).
tff(func_def_143,type,
sK23: 'A_b_vec_c_vec$' > 'C$' ).
tff(func_def_144,type,
sK24: 'A_b_vec_c_vec$' > 'C$' ).
tff(func_def_145,type,
sK25: 'A_b_vec_c_vec$' > 'C$' ).
tff(func_def_146,type,
sK26: 'A_b_vec_c_vec$' > 'C$' ).
tff(func_def_147,type,
sK27: 'A_b_vec_c_vec$' > 'C$' ).
tff(func_def_148,type,
sK28: ( 'A_b_vec_c_vec$' * 'A_b_vec_c_vec$' ) > 'C$' ).
tff(func_def_149,type,
sK29: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_150,type,
sK30: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_151,type,
sK31: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_152,type,
sK32: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_153,type,
sK33: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_154,type,
sK34: ( 'A_b_vec_c_vec$' * 'Nat$' ) > 'C$' ).
tff(func_def_155,type,
sK35: 'B_bool_fun$' > 'B$' ).
tff(func_def_156,type,
sK36: ( 'B_bool_fun$' * 'B$' ) > 'B$' ).
tff(func_def_157,type,
sK37: 'B_bool_fun$' > 'B$' ).
tff(func_def_158,type,
sK38: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_159,type,
sK39: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_160,type,
sK40: 'Nat$' > 'Nat$' ).
tff(func_def_161,type,
sK41: 'B_b_bool_fun_fun$' > 'B$' ).
tff(func_def_162,type,
sK42: 'B_b_bool_fun_fun$' > 'B$' ).
tff(func_def_163,type,
sK43: 'B_b_bool_fun_fun$' > 'B$' ).
tff(func_def_164,type,
sK44: 'B_b_bool_fun_fun$' > 'B$' ).
tff(func_def_165,type,
sK45: 'B_b_bool_fun_fun$' > 'B$' ).
tff(func_def_166,type,
sK46: 'Nat$' > 'Nat$' ).
tff(func_def_167,type,
sK47: 'C$' ).
tff(func_def_168,type,
sK48: 'C$' ).
tff(func_def_169,type,
sK49: 'B_bool_fun$' > 'B$' ).
tff(func_def_170,type,
sK50: ( $int * $int ) > 'Nat$' ).
tff(func_def_171,type,
sK51: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_172,type,
sK52: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_173,type,
sK53: $int > 'Nat$' ).
tff(func_def_174,type,
sK54: 'C_c_fun$' > 'C$' ).
tff(func_def_175,type,
sK55: 'C_c_fun$' > 'C$' ).
tff(func_def_176,type,
sK56: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_177,type,
sK57: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_178,type,
sK58: ( 'A_b_vec_c_vec$' * 'C$' ) > 'B$' ).
tff(func_def_179,type,
sK59: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_180,type,
sK60: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_181,type,
sK61: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_182,type,
sK62: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_183,type,
sK63: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_184,type,
sK64: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_185,type,
sK65: 'Nat_bool_fun$' > $int ).
tff(func_def_186,type,
sK66: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_187,type,
sK67: $int > 'Nat$' ).
tff(func_def_188,type,
sK68: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_189,type,
sK69: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_190,type,
sK70: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_191,type,
sK71: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_192,type,
sK72: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_193,type,
sK73: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_194,type,
sK74: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_195,type,
sK75: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_196,type,
sK76: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_197,type,
sK77: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_198,type,
sK78: ( 'A_b_vec$' * 'A_b_vec$' ) > 'B$' ).
tff(func_def_199,type,
sK79: 'Nat$' > 'Nat$' ).
tff(func_def_200,type,
sK80: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_201,type,
sK81: $int > $int ).
tff(func_def_202,type,
sK82: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_203,type,
sK83: $int > 'Nat$' ).
tff(func_def_204,type,
sK84: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_205,type,
sK85: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_206,type,
sK86: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_207,type,
sK87: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_208,type,
sK88: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_209,type,
sK89: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_210,type,
sK90: ( $int * $int ) > 'Nat$' ).
tff(func_def_211,type,
sK91: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_212,type,
sK92: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_213,type,
sK93: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_214,type,
sK94: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_215,type,
sK95: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_216,type,
sK96: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(pred_def_1,type,
'reduced_row_echelon_form$': 'A_b_vec_c_vec$' > $o ).
tff(pred_def_2,type,
'reduced_row_echelon_form$a': 'Int_b_vec_c_vec$' > $o ).
tff(pred_def_3,type,
'is_zero_row$i': ( 'B$' * 'A_b_vec_b_vec$' ) > $o ).
tff(pred_def_4,type,
'is_zero_row$a': ( 'C$' * 'Int_b_vec_c_vec$' ) > $o ).
tff(pred_def_5,type,
'member$a': ( 'Nat$' * 'Nat_set$' ) > $o ).
tff(pred_def_6,type,
'fun_app$e': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).
tff(pred_def_7,type,
'is_zero_row_upt_k$': ( 'C$' * 'Nat$' * 'A_b_vec_c_vec$' ) > $o ).
tff(pred_def_8,type,
'is_zero_row$d': ( 'C$' * 'Nat_b_vec_c_vec$' ) > $o ).
tff(pred_def_9,type,
'fun_app$q': ( 'A_bool_fun$' * 'A$' ) > $o ).
tff(pred_def_10,type,
'is_zero_row$g': ( 'B$' * 'A_b_vec_b_vec_b_vec$' ) > $o ).
tff(pred_def_11,type,
'less$': ( 'C$' * 'C$' ) > $o ).
tff(pred_def_12,type,
'reduced_row_echelon_form$g': 'A_b_vec_b_vec_b_vec$' > $o ).
tff(pred_def_13,type,
'fun_app$s': ( 'A_b_vec_bool_fun$' * 'A_b_vec$' ) > $o ).
tff(pred_def_14,type,
'reduced_row_echelon_form$h': 'Nat_b_vec_b_vec$' > $o ).
tff(pred_def_15,type,
'fun_app$h': ( 'B_bool_fun$' * 'B$' ) > $o ).
tff(pred_def_16,type,
'reduced_row_echelon_form$f': 'A_b_vec_c_vec_b_vec_b_vec$' > $o ).
tff(pred_def_17,type,
'is_zero_row$b': ( 'C$' * 'A_b_vec_c_vec_b_vec_c_vec$' ) > $o ).
tff(pred_def_18,type,
'is_zero_row$f': ( 'B$' * 'A_b_vec_c_vec_b_vec_b_vec$' ) > $o ).
tff(pred_def_19,type,
'fun_app$d': ( 'Num_bool_fun$' * 'Num$' ) > $o ).
tff(pred_def_20,type,
'is_zero_row$h': ( 'B$' * 'Nat_b_vec_b_vec$' ) > $o ).
tff(pred_def_21,type,
'reduced_row_echelon_form$c': 'A_b_vec_b_vec_c_vec$' > $o ).
tff(pred_def_22,type,
'reduced_row_echelon_form$i': 'A_b_vec_b_vec$' > $o ).
tff(pred_def_23,type,
'is_zero_row$c': ( 'C$' * 'A_b_vec_b_vec_c_vec$' ) > $o ).
tff(pred_def_24,type,
'is_zero_row$e': ( 'B$' * 'Int_b_vec_b_vec$' ) > $o ).
tff(pred_def_25,type,
'member$': ( 'Num$' * 'Num_set$' ) > $o ).
tff(pred_def_26,type,
'reduced_row_echelon_form$b': 'A_b_vec_c_vec_b_vec_c_vec$' > $o ).
tff(pred_def_27,type,
'member$b': ( $int * 'Int_set$' ) > $o ).
tff(pred_def_28,type,
'reduced_row_echelon_form$e': 'Int_b_vec_b_vec$' > $o ).
tff(pred_def_29,type,
'is_zero_row$': ( 'C$' * 'A_b_vec_c_vec$' ) > $o ).
tff(pred_def_30,type,
'fun_app$b': ( 'Int_bool_fun$' * $int ) > $o ).
tff(pred_def_31,type,
'reduced_row_echelon_form$d': 'Nat_b_vec_c_vec$' > $o ).
tff(f8,axiom,
! [X1: 'B$',X0: 'C$'] :
( ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X0)),X1) != 'zero$' )
<=> 'fun_app$h'('uu$'(X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom7) ).
tff(f27,axiom,
! [X1: 'C$',X0: 'A_b_vec_c_vec$',X2: 'B$'] :
( ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),X2) != 'zero$' )
<=> 'fun_app$h'('uua$'(X0,X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom26) ).
tff(f29,conjecture,
! [X0: 'C$'] :
( ~ 'is_zero_row$'(X0,'a$')
=> ! [X1: 'C$'] :
( ( X0 != X1 )
=> ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X1)),'least$'('uu$'(X0))) = 'zero$' ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture28) ).
tff(f30,negated_conjecture,
~ ! [X0: 'C$'] :
( ~ 'is_zero_row$'(X0,'a$')
=> ! [X1: 'C$'] :
( ( X0 != X1 )
=> ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X1)),'least$'('uu$'(X0))) = 'zero$' ) ) ),
inference(negated_conjecture,[status(cth)],[f29]) ).
tff(f31,axiom,
'reduced_row_echelon_form$'('a$'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom29) ).
tff(f32,axiom,
! [X1: 'A_b_vec_c_vec$',X0: 'C$'] :
( 'is_zero_row$'(X0,X1)
<=> ! [X2: 'B$'] : ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X1),X0)),X2) = 'zero$' ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom30) ).
tff(f36,axiom,
! [X0: 'B_bool_fun$',X1: 'B$'] :
( 'fun_app$h'(X0,X1)
=> 'fun_app$h'(X0,'least$'(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom34) ).
tff(f41,axiom,
! [X0: 'B_bool_fun$'] :
( ? [X1: 'B$'] : 'fun_app$h'(X0,X1)
=> 'fun_app$h'(X0,'least$'(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom39) ).
tff(f79,axiom,
! [X0: 'A_b_vec_c_vec$'] :
( ( ! [X1: 'C$'] :
( 'is_zero_row$'(X1,X0)
=> ~ ? [X2: 'C$'] :
( ~ 'is_zero_row$'(X2,X0)
& 'less$'(X1,X2) ) )
& ! [X1: 'C$'] :
( ~ 'is_zero_row$'(X1,X0)
=> ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),'least$'('uua$'(X0,X1))) = 'one$c' ) )
& ! [X1: 'C$'] :
( ( 'less$'(X1,'fun_app$k'('plus$a'(X1),'one$a'))
& ~ 'is_zero_row$'('fun_app$k'('plus$a'(X1),'one$a'),X0)
& ~ 'is_zero_row$'(X1,X0) )
=> 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X1))),'least$'('uut$'(X0,X1))) )
& ! [X1: 'C$'] :
( ~ 'is_zero_row$'(X1,X0)
=> ! [X2: 'C$'] :
( ( X1 != X2 )
=> ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X2)),'least$'('uua$'(X0,X1))) = 'zero$' ) ) ) )
<=> 'reduced_row_echelon_form$'(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom77) ).
tff(f211,axiom,
! [X0: 'B_bool_fun$'] :
( ? [X1: 'B$'] :
( 'fun_app$h'(X0,X1)
& ! [X2: 'B$'] :
( 'fun_app$h'('fun_app$l'('less$a',X2),X1)
=> ~ 'fun_app$h'(X0,X2) ) )
<=> ? [X1: 'B$'] : 'fun_app$h'(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom209) ).
tff(f226,axiom,
! [X1: 'B$',X0: 'B$'] :
( ( ( X0 = X1 )
| 'fun_app$h'('fun_app$l'('less$a',X1),X0) )
<=> ~ 'fun_app$h'('fun_app$l'('less$a',X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom224) ).
tff(f263,axiom,
! [X1: 'B$',X0: 'B$'] :
( ( X0 != X1 )
<=> ( 'fun_app$h'('fun_app$l'('less$a',X0),X1)
| 'fun_app$h'('fun_app$l'('less$a',X1),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom261) ).
tff(f358,axiom,
! [X1: 'B_bool_fun$',X0: 'B$'] :
( 'fun_app$h'('fun_app$l'('less$a',X0),'least$'(X1))
=> ~ 'fun_app$h'(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom356) ).
tff(f718,plain,
! [X1: 'C$',X0: 'B$'] :
( ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X1)),X0) )
<=> 'fun_app$h'('uu$'(X1),X0) ),
inference(rectify,[],[f8]) ).
tff(f719,plain,
! [X0: 'A_b_vec_c_vec$',X1: 'C$'] :
( ! [X2: 'B$'] : ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),X2) )
<=> 'is_zero_row$'(X1,X0) ),
inference(rectify,[],[f32]) ).
tff(f724,plain,
! [X0: 'B_bool_fun$',X1: 'B$'] :
( 'fun_app$h'('fun_app$l'('less$a',X1),'least$'(X0))
=> ~ 'fun_app$h'(X0,X1) ),
inference(rectify,[],[f358]) ).
tff(f733,plain,
! [X0: 'B_bool_fun$'] :
( ? [X1: 'B$'] :
( 'fun_app$h'(X0,X1)
& ! [X2: 'B$'] :
( 'fun_app$h'('fun_app$l'('less$a',X2),X1)
=> ~ 'fun_app$h'(X0,X2) ) )
<=> ? [X3: 'B$'] : 'fun_app$h'(X0,X3) ),
inference(rectify,[],[f211]) ).
tff(f734,plain,
! [X0: 'B$',X1: 'B$'] :
( ( ( X0 = X1 )
| 'fun_app$h'('fun_app$l'('less$a',X0),X1) )
<=> ~ 'fun_app$h'('fun_app$l'('less$a',X1),X0) ),
inference(rectify,[],[f226]) ).
tff(f753,plain,
! [X0: 'A_b_vec_c_vec$'] :
( 'reduced_row_echelon_form$'(X0)
<=> ( ! [X3: 'C$'] :
( ~ 'is_zero_row$'(X3,X0)
=> ( 'one$c' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X3)),'least$'('uua$'(X0,X3))) ) )
& ! [X4: 'C$'] :
( ( ~ 'is_zero_row$'(X4,X0)
& 'less$'(X4,'fun_app$k'('plus$a'(X4),'one$a'))
& ~ 'is_zero_row$'('fun_app$k'('plus$a'(X4),'one$a'),X0) )
=> 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X4))),'least$'('uut$'(X0,X4))) )
& ! [X1: 'C$'] :
( 'is_zero_row$'(X1,X0)
=> ~ ? [X2: 'C$'] :
( ~ 'is_zero_row$'(X2,X0)
& 'less$'(X1,X2) ) )
& ! [X5: 'C$'] :
( ~ 'is_zero_row$'(X5,X0)
=> ! [X6: 'C$'] :
( ( X5 != X6 )
=> ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X6)),'least$'('uua$'(X0,X5))) ) ) ) ) ),
inference(rectify,[],[f79]) ).
tff(f799,plain,
! [X1: 'A_b_vec_c_vec$',X2: 'B$',X0: 'C$'] :
( ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X1),X0)),X2) )
<=> 'fun_app$h'('uua$'(X1,X0),X2) ),
inference(rectify,[],[f27]) ).
tff(f928,plain,
! [X0: 'B_bool_fun$'] :
( ? [X3: 'B$'] : 'fun_app$h'(X0,X3)
<=> ? [X1: 'B$'] :
( ! [X2: 'B$'] :
( ~ 'fun_app$h'(X0,X2)
| ~ 'fun_app$h'('fun_app$l'('less$a',X2),X1) )
& 'fun_app$h'(X0,X1) ) ),
inference(ennf_transformation,[],[f733]) ).
tff(f931,plain,
? [X0: 'C$'] :
( ? [X1: 'C$'] :
( ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X1)),'least$'('uu$'(X0))) )
& ( X0 != X1 ) )
& ~ 'is_zero_row$'(X0,'a$') ),
inference(ennf_transformation,[],[f30]) ).
tff(f981,plain,
! [X0: 'B_bool_fun$'] :
( ! [X1: 'B$'] : ~ 'fun_app$h'(X0,X1)
| 'fun_app$h'(X0,'least$'(X0)) ),
inference(ennf_transformation,[],[f41]) ).
tff(f991,plain,
! [X0: 'B_bool_fun$',X1: 'B$'] :
( 'fun_app$h'(X0,'least$'(X0))
| ~ 'fun_app$h'(X0,X1) ),
inference(ennf_transformation,[],[f36]) ).
tff(f1015,plain,
! [X0: 'A_b_vec_c_vec$'] :
( 'reduced_row_echelon_form$'(X0)
<=> ( ! [X3: 'C$'] :
( ( 'one$c' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X3)),'least$'('uua$'(X0,X3))) )
| 'is_zero_row$'(X3,X0) )
& ! [X4: 'C$'] :
( 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X4))),'least$'('uut$'(X0,X4)))
| 'is_zero_row$'(X4,X0)
| ~ 'less$'(X4,'fun_app$k'('plus$a'(X4),'one$a'))
| 'is_zero_row$'('fun_app$k'('plus$a'(X4),'one$a'),X0) )
& ! [X1: 'C$'] :
( ! [X2: 'C$'] :
( ~ 'less$'(X1,X2)
| 'is_zero_row$'(X2,X0) )
| ~ 'is_zero_row$'(X1,X0) )
& ! [X5: 'C$'] :
( ! [X6: 'C$'] :
( ( X5 = X6 )
| ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X6)),'least$'('uua$'(X0,X5))) ) )
| 'is_zero_row$'(X5,X0) ) ) ),
inference(ennf_transformation,[],[f753]) ).
tff(f1016,plain,
! [X0: 'A_b_vec_c_vec$'] :
( 'reduced_row_echelon_form$'(X0)
<=> ( ! [X1: 'C$'] :
( ! [X2: 'C$'] :
( ~ 'less$'(X1,X2)
| 'is_zero_row$'(X2,X0) )
| ~ 'is_zero_row$'(X1,X0) )
& ! [X4: 'C$'] :
( 'is_zero_row$'('fun_app$k'('plus$a'(X4),'one$a'),X0)
| 'is_zero_row$'(X4,X0)
| ~ 'less$'(X4,'fun_app$k'('plus$a'(X4),'one$a'))
| 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X4))),'least$'('uut$'(X0,X4))) )
& ! [X5: 'C$'] :
( ! [X6: 'C$'] :
( ( X5 = X6 )
| ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X6)),'least$'('uua$'(X0,X5))) ) )
| 'is_zero_row$'(X5,X0) )
& ! [X3: 'C$'] :
( ( 'one$c' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X3)),'least$'('uua$'(X0,X3))) )
| 'is_zero_row$'(X3,X0) ) ) ),
inference(flattening,[],[f1015]) ).
tff(f1052,plain,
! [X1: 'B$',X0: 'B_bool_fun$'] :
( ~ 'fun_app$h'(X0,X1)
| ~ 'fun_app$h'('fun_app$l'('less$a',X1),'least$'(X0)) ),
inference(ennf_transformation,[],[f724]) ).
tff(f1142,plain,
! [X1: 'B$',X0: 'B$'] :
( ( ( X0 != X1 )
| ( ~ 'fun_app$h'('fun_app$l'('less$a',X0),X1)
& ~ 'fun_app$h'('fun_app$l'('less$a',X1),X0) ) )
& ( 'fun_app$h'('fun_app$l'('less$a',X0),X1)
| 'fun_app$h'('fun_app$l'('less$a',X1),X0)
| ( X0 = X1 ) ) ),
inference(nnf_transformation,[],[f263]) ).
tff(f1143,plain,
! [X1: 'B$',X0: 'B$'] :
( ( ( X0 != X1 )
| ( ~ 'fun_app$h'('fun_app$l'('less$a',X0),X1)
& ~ 'fun_app$h'('fun_app$l'('less$a',X1),X0) ) )
& ( 'fun_app$h'('fun_app$l'('less$a',X0),X1)
| 'fun_app$h'('fun_app$l'('less$a',X1),X0)
| ( X0 = X1 ) ) ),
inference(flattening,[],[f1142]) ).
tff(f1144,plain,
! [X0: 'B$',X1: 'B$'] :
( ( ( X0 != X1 )
| ( ~ 'fun_app$h'('fun_app$l'('less$a',X1),X0)
& ~ 'fun_app$h'('fun_app$l'('less$a',X0),X1) ) )
& ( 'fun_app$h'('fun_app$l'('less$a',X1),X0)
| 'fun_app$h'('fun_app$l'('less$a',X0),X1)
| ( X0 = X1 ) ) ),
inference(rectify,[],[f1143]) ).
tff(f1188,plain,
! [X0: 'A_b_vec_c_vec$'] :
( ( 'reduced_row_echelon_form$'(X0)
| ? [X1: 'C$'] :
( ? [X2: 'C$'] :
( 'less$'(X1,X2)
& ~ 'is_zero_row$'(X2,X0) )
& 'is_zero_row$'(X1,X0) )
| ? [X4: 'C$'] :
( ~ 'is_zero_row$'('fun_app$k'('plus$a'(X4),'one$a'),X0)
& ~ 'is_zero_row$'(X4,X0)
& 'less$'(X4,'fun_app$k'('plus$a'(X4),'one$a'))
& ~ 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X4))),'least$'('uut$'(X0,X4))) )
| ? [X5: 'C$'] :
( ? [X6: 'C$'] :
( ( X5 != X6 )
& ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X6)),'least$'('uua$'(X0,X5))) ) )
& ~ 'is_zero_row$'(X5,X0) )
| ? [X3: 'C$'] :
( ( 'one$c' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X3)),'least$'('uua$'(X0,X3))) )
& ~ 'is_zero_row$'(X3,X0) ) )
& ( ( ! [X1: 'C$'] :
( ! [X2: 'C$'] :
( ~ 'less$'(X1,X2)
| 'is_zero_row$'(X2,X0) )
| ~ 'is_zero_row$'(X1,X0) )
& ! [X4: 'C$'] :
( 'is_zero_row$'('fun_app$k'('plus$a'(X4),'one$a'),X0)
| 'is_zero_row$'(X4,X0)
| ~ 'less$'(X4,'fun_app$k'('plus$a'(X4),'one$a'))
| 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X4))),'least$'('uut$'(X0,X4))) )
& ! [X5: 'C$'] :
( ! [X6: 'C$'] :
( ( X5 = X6 )
| ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X6)),'least$'('uua$'(X0,X5))) ) )
| 'is_zero_row$'(X5,X0) )
& ! [X3: 'C$'] :
( ( 'one$c' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X3)),'least$'('uua$'(X0,X3))) )
| 'is_zero_row$'(X3,X0) ) )
| ~ 'reduced_row_echelon_form$'(X0) ) ),
inference(nnf_transformation,[],[f1016]) ).
tff(f1189,plain,
! [X0: 'A_b_vec_c_vec$'] :
( ( 'reduced_row_echelon_form$'(X0)
| ? [X1: 'C$'] :
( ? [X2: 'C$'] :
( 'less$'(X1,X2)
& ~ 'is_zero_row$'(X2,X0) )
& 'is_zero_row$'(X1,X0) )
| ? [X4: 'C$'] :
( ~ 'is_zero_row$'('fun_app$k'('plus$a'(X4),'one$a'),X0)
& ~ 'is_zero_row$'(X4,X0)
& 'less$'(X4,'fun_app$k'('plus$a'(X4),'one$a'))
& ~ 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X4))),'least$'('uut$'(X0,X4))) )
| ? [X5: 'C$'] :
( ? [X6: 'C$'] :
( ( X5 != X6 )
& ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X6)),'least$'('uua$'(X0,X5))) ) )
& ~ 'is_zero_row$'(X5,X0) )
| ? [X3: 'C$'] :
( ( 'one$c' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X3)),'least$'('uua$'(X0,X3))) )
& ~ 'is_zero_row$'(X3,X0) ) )
& ( ( ! [X1: 'C$'] :
( ! [X2: 'C$'] :
( ~ 'less$'(X1,X2)
| 'is_zero_row$'(X2,X0) )
| ~ 'is_zero_row$'(X1,X0) )
& ! [X4: 'C$'] :
( 'is_zero_row$'('fun_app$k'('plus$a'(X4),'one$a'),X0)
| 'is_zero_row$'(X4,X0)
| ~ 'less$'(X4,'fun_app$k'('plus$a'(X4),'one$a'))
| 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X4))),'least$'('uut$'(X0,X4))) )
& ! [X5: 'C$'] :
( ! [X6: 'C$'] :
( ( X5 = X6 )
| ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X6)),'least$'('uua$'(X0,X5))) ) )
| 'is_zero_row$'(X5,X0) )
& ! [X3: 'C$'] :
( ( 'one$c' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X3)),'least$'('uua$'(X0,X3))) )
| 'is_zero_row$'(X3,X0) ) )
| ~ 'reduced_row_echelon_form$'(X0) ) ),
inference(flattening,[],[f1188]) ).
tff(f1190,plain,
! [X0: 'A_b_vec_c_vec$'] :
( ( 'reduced_row_echelon_form$'(X0)
| ? [X1: 'C$'] :
( ? [X2: 'C$'] :
( 'less$'(X1,X2)
& ~ 'is_zero_row$'(X2,X0) )
& 'is_zero_row$'(X1,X0) )
| ? [X3: 'C$'] :
( ~ 'is_zero_row$'('fun_app$k'('plus$a'(X3),'one$a'),X0)
& ~ 'is_zero_row$'(X3,X0)
& 'less$'(X3,'fun_app$k'('plus$a'(X3),'one$a'))
& ~ 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X3))),'least$'('uut$'(X0,X3))) )
| ? [X4: 'C$'] :
( ? [X5: 'C$'] :
( ( X4 != X5 )
& ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X5)),'least$'('uua$'(X0,X4))) ) )
& ~ 'is_zero_row$'(X4,X0) )
| ? [X6: 'C$'] :
( ( 'one$c' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X6)),'least$'('uua$'(X0,X6))) )
& ~ 'is_zero_row$'(X6,X0) ) )
& ( ( ! [X7: 'C$'] :
( ! [X8: 'C$'] :
( ~ 'less$'(X7,X8)
| 'is_zero_row$'(X8,X0) )
| ~ 'is_zero_row$'(X7,X0) )
& ! [X9: 'C$'] :
( 'is_zero_row$'('fun_app$k'('plus$a'(X9),'one$a'),X0)
| 'is_zero_row$'(X9,X0)
| ~ 'less$'(X9,'fun_app$k'('plus$a'(X9),'one$a'))
| 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X9))),'least$'('uut$'(X0,X9))) )
& ! [X10: 'C$'] :
( ! [X11: 'C$'] :
( ( X10 = X11 )
| ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X11)),'least$'('uua$'(X0,X10))) ) )
| 'is_zero_row$'(X10,X0) )
& ! [X12: 'C$'] :
( ( 'one$c' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X12)),'least$'('uua$'(X0,X12))) )
| 'is_zero_row$'(X12,X0) ) )
| ~ 'reduced_row_echelon_form$'(X0) ) ),
inference(rectify,[],[f1189]) ).
tff(f1191,plain,
! [X0: 'A_b_vec_c_vec$'] :
( ( 'reduced_row_echelon_form$'(X0)
| ( 'less$'(sK22(X0),sK23(X0))
& ~ 'is_zero_row$'(sK23(X0),X0)
& 'is_zero_row$'(sK22(X0),X0) )
| ( ~ 'is_zero_row$'('fun_app$k'('plus$a'(sK24(X0)),'one$a'),X0)
& ~ 'is_zero_row$'(sK24(X0),X0)
& 'less$'(sK24(X0),'fun_app$k'('plus$a'(sK24(X0)),'one$a'))
& ~ 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,sK24(X0)))),'least$'('uut$'(X0,sK24(X0)))) )
| ( ( sK26(X0) != sK25(X0) )
& ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),sK26(X0))),'least$'('uua$'(X0,sK25(X0)))) )
& ~ 'is_zero_row$'(sK25(X0),X0) )
| ( ( 'one$c' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),sK27(X0))),'least$'('uua$'(X0,sK27(X0)))) )
& ~ 'is_zero_row$'(sK27(X0),X0) ) )
& ( ( ! [X7: 'C$'] :
( ! [X8: 'C$'] :
( ~ 'less$'(X7,X8)
| 'is_zero_row$'(X8,X0) )
| ~ 'is_zero_row$'(X7,X0) )
& ! [X9: 'C$'] :
( 'is_zero_row$'('fun_app$k'('plus$a'(X9),'one$a'),X0)
| 'is_zero_row$'(X9,X0)
| ~ 'less$'(X9,'fun_app$k'('plus$a'(X9),'one$a'))
| 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'(X0,X9))),'least$'('uut$'(X0,X9))) )
& ! [X10: 'C$'] :
( ! [X11: 'C$'] :
( ( X10 = X11 )
| ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X11)),'least$'('uua$'(X0,X10))) ) )
| 'is_zero_row$'(X10,X0) )
& ! [X12: 'C$'] :
( ( 'one$c' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X12)),'least$'('uua$'(X0,X12))) )
| 'is_zero_row$'(X12,X0) ) )
| ~ 'reduced_row_echelon_form$'(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24,sK25,sK26,sK27]),skolemize(X1,sK22(X0)),skolemize(X2,sK23(X0)),skolemize(X3,sK24(X0)),skolemize(X4,sK25(X0)),skolemize(X5,sK26(X0)),skolemize(X6,sK27(X0))],[f1190]) ).
tff(f1208,plain,
! [X0: 'B_bool_fun$'] :
( ( ? [X3: 'B$'] : 'fun_app$h'(X0,X3)
| ! [X1: 'B$'] :
( ? [X2: 'B$'] :
( 'fun_app$h'(X0,X2)
& 'fun_app$h'('fun_app$l'('less$a',X2),X1) )
| ~ 'fun_app$h'(X0,X1) ) )
& ( ? [X1: 'B$'] :
( ! [X2: 'B$'] :
( ~ 'fun_app$h'(X0,X2)
| ~ 'fun_app$h'('fun_app$l'('less$a',X2),X1) )
& 'fun_app$h'(X0,X1) )
| ! [X3: 'B$'] : ~ 'fun_app$h'(X0,X3) ) ),
inference(nnf_transformation,[],[f928]) ).
tff(f1209,plain,
! [X0: 'B_bool_fun$'] :
( ( ? [X1: 'B$'] : 'fun_app$h'(X0,X1)
| ! [X2: 'B$'] :
( ? [X3: 'B$'] :
( 'fun_app$h'(X0,X3)
& 'fun_app$h'('fun_app$l'('less$a',X3),X2) )
| ~ 'fun_app$h'(X0,X2) ) )
& ( ? [X4: 'B$'] :
( ! [X5: 'B$'] :
( ~ 'fun_app$h'(X0,X5)
| ~ 'fun_app$h'('fun_app$l'('less$a',X5),X4) )
& 'fun_app$h'(X0,X4) )
| ! [X6: 'B$'] : ~ 'fun_app$h'(X0,X6) ) ),
inference(rectify,[],[f1208]) ).
tff(f1210,plain,
! [X0: 'B_bool_fun$'] :
( ( 'fun_app$h'(X0,sK35(X0))
| ! [X2: 'B$'] :
( ( 'fun_app$h'(X0,sK36(X0,X2))
& 'fun_app$h'('fun_app$l'('less$a',sK36(X0,X2)),X2) )
| ~ 'fun_app$h'(X0,X2) ) )
& ( ( ! [X5: 'B$'] :
( ~ 'fun_app$h'(X0,X5)
| ~ 'fun_app$h'('fun_app$l'('less$a',X5),sK37(X0)) )
& 'fun_app$h'(X0,sK37(X0)) )
| ! [X6: 'B$'] : ~ 'fun_app$h'(X0,X6) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35,sK36,sK37]),skolemize(X1,sK35(X0)),skolemize(X3,sK36(X0,X2)),skolemize(X4,sK37(X0))],[f1209]) ).
tff(f1238,plain,
( ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),sK48)),'least$'('uu$'(sK47))) )
& ( sK48 != sK47 )
& ~ 'is_zero_row$'(sK47,'a$') ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47,sK48]),skolemize(X0,sK47),skolemize(X1,sK48)],[f931]) ).
tff(f1243,plain,
! [X0: 'B$',X1: 'B$'] :
( ( ( X0 = X1 )
| 'fun_app$h'('fun_app$l'('less$a',X0),X1)
| 'fun_app$h'('fun_app$l'('less$a',X1),X0) )
& ( ~ 'fun_app$h'('fun_app$l'('less$a',X1),X0)
| ( ( X0 != X1 )
& ~ 'fun_app$h'('fun_app$l'('less$a',X0),X1) ) ) ),
inference(nnf_transformation,[],[f734]) ).
tff(f1244,plain,
! [X0: 'B$',X1: 'B$'] :
( ( ( X0 = X1 )
| 'fun_app$h'('fun_app$l'('less$a',X0),X1)
| 'fun_app$h'('fun_app$l'('less$a',X1),X0) )
& ( ~ 'fun_app$h'('fun_app$l'('less$a',X1),X0)
| ( ( X0 != X1 )
& ~ 'fun_app$h'('fun_app$l'('less$a',X0),X1) ) ) ),
inference(flattening,[],[f1243]) ).
tff(f1285,plain,
! [X0: 'A_b_vec_c_vec$',X1: 'C$'] :
( ( ! [X2: 'B$'] : ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),X2) )
| ~ 'is_zero_row$'(X1,X0) )
& ( 'is_zero_row$'(X1,X0)
| ? [X2: 'B$'] : ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),X2) ) ) ),
inference(nnf_transformation,[],[f719]) ).
tff(f1286,plain,
! [X0: 'A_b_vec_c_vec$',X1: 'C$'] :
( ( ! [X2: 'B$'] : ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),X2) )
| ~ 'is_zero_row$'(X1,X0) )
& ( 'is_zero_row$'(X1,X0)
| ? [X3: 'B$'] : ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),X3) ) ) ),
inference(rectify,[],[f1285]) ).
tff(f1287,plain,
! [X0: 'A_b_vec_c_vec$',X1: 'C$'] :
( ( ! [X2: 'B$'] : ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),X2) )
| ~ 'is_zero_row$'(X1,X0) )
& ( 'is_zero_row$'(X1,X0)
| ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),sK58(X0,X1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(X3,sK58(X0,X1))],[f1286]) ).
tff(f1358,plain,
! [X1: 'C$',X0: 'B$'] :
( ( ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X1)),X0) )
| ~ 'fun_app$h'('uu$'(X1),X0) )
& ( 'fun_app$h'('uu$'(X1),X0)
| ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X1)),X0) ) ) ),
inference(nnf_transformation,[],[f718]) ).
tff(f1359,plain,
! [X0: 'C$',X1: 'B$'] :
( ( ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X0)),X1) != 'zero$' )
| ~ 'fun_app$h'('uu$'(X0),X1) )
& ( 'fun_app$h'('uu$'(X0),X1)
| ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X0)),X1) = 'zero$' ) ) ),
inference(rectify,[],[f1358]) ).
tff(f1370,plain,
! [X1: 'A_b_vec_c_vec$',X2: 'B$',X0: 'C$'] :
( ( ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X1),X0)),X2) )
| ~ 'fun_app$h'('uua$'(X1,X0),X2) )
& ( 'fun_app$h'('uua$'(X1,X0),X2)
| ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X1),X0)),X2) ) ) ),
inference(nnf_transformation,[],[f799]) ).
tff(f1371,plain,
! [X0: 'A_b_vec_c_vec$',X1: 'B$',X2: 'C$'] :
( ( ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X2)),X1) )
| ~ 'fun_app$h'('uua$'(X0,X2),X1) )
& ( 'fun_app$h'('uua$'(X0,X2),X1)
| ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X2)),X1) ) ) ),
inference(rectify,[],[f1370]) ).
tff(f1433,plain,
! [X0: 'B$',X1: 'B_bool_fun$'] :
( ~ 'fun_app$h'(X1,X0)
| ~ 'fun_app$h'('fun_app$l'('less$a',X0),'least$'(X1)) ),
inference(rectify,[],[f1052]) ).
tff(f1470,plain,
! [X0: 'B$',X1: 'B$'] :
( 'fun_app$h'('fun_app$l'('less$a',X1),X0)
| 'fun_app$h'('fun_app$l'('less$a',X0),X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f1144]) ).
tff(f1606,plain,
! [X0: 'A_b_vec_c_vec$',X12: 'C$'] :
( ( 'one$c' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X12)),'least$'('uua$'(X0,X12))) )
| 'is_zero_row$'(X12,X0)
| ~ 'reduced_row_echelon_form$'(X0) ),
inference(cnf_transformation,[],[f1191]) ).
tff(f1607,plain,
! [X10: 'C$',X0: 'A_b_vec_c_vec$',X11: 'C$'] :
( ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X11)),'least$'('uua$'(X0,X10))) )
| ~ 'reduced_row_echelon_form$'(X0)
| 'is_zero_row$'(X10,X0)
| ( X10 = X11 ) ),
inference(cnf_transformation,[],[f1191]) ).
tff(f1773,plain,
! [X0: 'B_bool_fun$',X6: 'B$'] :
( 'fun_app$h'(X0,sK37(X0))
| ~ 'fun_app$h'(X0,X6) ),
inference(cnf_transformation,[],[f1210]) ).
tff(f1774,plain,
! [X0: 'B_bool_fun$',X6: 'B$',X5: 'B$'] :
( ~ 'fun_app$h'('fun_app$l'('less$a',X5),sK37(X0))
| ~ 'fun_app$h'(X0,X6)
| ~ 'fun_app$h'(X0,X5) ),
inference(cnf_transformation,[],[f1210]) ).
tff(f1820,plain,
~ 'is_zero_row$'(sK47,'a$'),
inference(cnf_transformation,[],[f1238]) ).
tff(f1821,plain,
sK48 != sK47,
inference(cnf_transformation,[],[f1238]) ).
tff(f1822,plain,
'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),sK48)),'least$'('uu$'(sK47))),
inference(cnf_transformation,[],[f1238]) ).
tff(f1831,plain,
! [X0: 'B$',X1: 'B$'] :
( 'fun_app$h'('fun_app$l'('less$a',X1),X0)
| ( X0 = X1 )
| 'fun_app$h'('fun_app$l'('less$a',X0),X1) ),
inference(cnf_transformation,[],[f1244]) ).
tff(f1839,plain,
! [X0: 'B_bool_fun$',X1: 'B$'] :
( 'fun_app$h'(X0,'least$'(X0))
| ~ 'fun_app$h'(X0,X1) ),
inference(cnf_transformation,[],[f981]) ).
tff(f1908,plain,
! [X0: 'A_b_vec_c_vec$',X1: 'C$'] :
( ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),sK58(X0,X1)) )
| 'is_zero_row$'(X1,X0) ),
inference(cnf_transformation,[],[f1287]) ).
tff(f1909,plain,
! [X2: 'B$',X0: 'A_b_vec_c_vec$',X1: 'C$'] :
( ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X1)),X2) )
| ~ 'is_zero_row$'(X1,X0) ),
inference(cnf_transformation,[],[f1287]) ).
tff(f1970,plain,
'reduced_row_echelon_form$'('a$'),
inference(cnf_transformation,[],[f31]) ).
tff(f1986,plain,
! [X0: 'B_bool_fun$',X1: 'B$'] :
( 'fun_app$h'(X0,'least$'(X0))
| ~ 'fun_app$h'(X0,X1) ),
inference(cnf_transformation,[],[f991]) ).
tff(f2039,plain,
! [X0: 'C$',X1: 'B$'] :
( ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X0)),X1) = 'zero$' )
| 'fun_app$h'('uu$'(X0),X1) ),
inference(cnf_transformation,[],[f1359]) ).
tff(f2040,plain,
! [X0: 'C$',X1: 'B$'] :
( ( 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),X0)),X1) != 'zero$' )
| ~ 'fun_app$h'('uu$'(X0),X1) ),
inference(cnf_transformation,[],[f1359]) ).
tff(f2063,plain,
! [X2: 'C$',X0: 'A_b_vec_c_vec$',X1: 'B$'] :
( ( 'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X2)),X1) )
| 'fun_app$h'('uua$'(X0,X2),X1) ),
inference(cnf_transformation,[],[f1371]) ).
tff(f2064,plain,
! [X2: 'C$',X0: 'A_b_vec_c_vec$',X1: 'B$'] :
( ( 'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'(X0),X2)),X1) )
| ~ 'fun_app$h'('uua$'(X0,X2),X1) ),
inference(cnf_transformation,[],[f1371]) ).
tff(f2152,plain,
! [X0: 'B$',X1: 'B_bool_fun$'] :
( ~ 'fun_app$h'('fun_app$l'('less$a',X0),'least$'(X1))
| ~ 'fun_app$h'(X1,X0) ),
inference(cnf_transformation,[],[f1433]) ).
tff(f2252,plain,
'one$c' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),sK47)),'least$'('uua$'('a$',sK47))),
inference(unit_resulting_resolution,[],[f1606,f1970,f1820]) ).
tff(f2254,plain,
'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),sK47)),sK58('a$',sK47)),
inference(unit_resulting_resolution,[],[f1908,f1820]) ).
tff(f2255,plain,
'zero$' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),sK48)),'least$'('uua$'('a$',sK47))),
inference(unit_resulting_resolution,[],[f1607,f1970,f1820,f1821]) ).
tff(f2256,plain,
'fun_app$h'('uua$'('a$',sK48),'least$'('uu$'(sK47))),
inference(unit_resulting_resolution,[],[f2063,f1822]) ).
tff(f2258,plain,
'fun_app$h'('uu$'(sK48),'least$'('uu$'(sK47))),
inference(unit_resulting_resolution,[],[f2039,f1822]) ).
tff(f2261,plain,
( ~ 'is_zero_row$'(sK48,'a$')
| ( 'zero$' != 'zero$' ) ),
inference(constrained_superposition,[],[f1822,f1909]) ).
tff(f2262,plain,
~ 'is_zero_row$'(sK48,'a$'),
inference(trivial_inequality_removal,[],[f2261]) ).
tff(f2265,plain,
'one$c' = 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),sK48)),'least$'('uua$'('a$',sK48))),
inference(unit_resulting_resolution,[],[f1606,f1970,f2262]) ).
tff(f2361,plain,
'fun_app$h'('uua$'('a$',sK48),'least$'('uua$'('a$',sK48))),
inference(unit_resulting_resolution,[],[f1986,f2256]) ).
tff(f2413,plain,
'fun_app$h'('uu$'(sK47),sK58('a$',sK47)),
inference(unit_resulting_resolution,[],[f2039,f2254]) ).
tff(f2469,plain,
( 'fun_app$h'('uu$'(sK47),'least$'('uua$'('a$',sK47)))
| ( 'zero$' = 'one$c' ) ),
inference(constrained_superposition,[],[f2252,f2039]) ).
tff(f2518,plain,
'fun_app$h'('uu$'(sK47),sK37('uu$'(sK47))),
inference(unit_resulting_resolution,[],[f1773,f2413]) ).
tff(f2521,plain,
'fun_app$h'('uu$'(sK47),'least$'('uu$'(sK47))),
inference(unit_resulting_resolution,[],[f1839,f2413]) ).
tff(f2526,plain,
( ( 'zero$' != 'zero$' )
| ~ 'fun_app$h'('uu$'(sK48),'least$'('uua$'('a$',sK47))) ),
inference(constrained_superposition,[],[f2040,f2255]) ).
tff(f2529,plain,
~ 'fun_app$h'('uu$'(sK48),'least$'('uua$'('a$',sK47))),
inference(trivial_inequality_removal,[],[f2526]) ).
tff(f2530,plain,
'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),sK47)),sK37('uu$'(sK47))),
inference(unit_resulting_resolution,[],[f2040,f2518]) ).
tff(f2577,plain,
~ 'fun_app$h'('fun_app$l'('less$a',sK37('uu$'(sK47))),'least$'('uu$'(sK47))),
inference(unit_resulting_resolution,[],[f2152,f2518]) ).
tff(f2670,plain,
~ 'fun_app$h'('fun_app$l'('less$a','least$'('uu$'(sK47))),sK37('uu$'(sK47))),
inference(unit_resulting_resolution,[],[f1774,f2521,f2521]) ).
tff(f2735,plain,
'zero$' != 'fun_app$i'('vec_nth$'('fun_app$j'('vec_nth$a'('a$'),sK48)),'least$'('uua$'('a$',sK48))),
inference(unit_resulting_resolution,[],[f2064,f2361]) ).
tff(f2784,plain,
'zero$' != 'one$c',
inference(forward_demodulation,[],[f2735,f2265]) ).
tff(f3031,plain,
'fun_app$h'('uu$'(sK47),'least$'('uua$'('a$',sK47))),
inference(unit_resulting_resolution,[],[f2469,f2784]) ).
tff(f3081,plain,
~ 'fun_app$h'('fun_app$l'('less$a','least$'('uua$'('a$',sK47))),sK37('uu$'(sK47))),
inference(unit_resulting_resolution,[],[f1774,f3031,f3031]) ).
tff(f3771,plain,
( 'fun_app$h'('fun_app$l'('less$a','least$'('uu$'(sK47))),sK37('uu$'(sK47)))
| ( sK37('uu$'(sK47)) = 'least$'('uu$'(sK47)) ) ),
inference(resolution,[],[f2577,f1831]) ).
tff(f3777,plain,
sK37('uu$'(sK47)) = 'least$'('uu$'(sK47)),
inference(forward_subsumption_resolution,[],[f3771,f2670]) ).
tff(f6649,plain,
( ( 'zero$' != 'zero$' )
| 'fun_app$h'('uua$'('a$',sK47),sK37('uu$'(sK47))) ),
inference(constrained_superposition,[],[f2530,f2063]) ).
tff(f6652,plain,
'fun_app$h'('uua$'('a$',sK47),sK37('uu$'(sK47))),
inference(trivial_inequality_removal,[],[f6649]) ).
tff(f6751,plain,
~ 'fun_app$h'('fun_app$l'('less$a',sK37('uu$'(sK47))),'least$'('uua$'('a$',sK47))),
inference(unit_resulting_resolution,[],[f2152,f6652]) ).
tff(f6877,plain,
sK37('uu$'(sK47)) = 'least$'('uua$'('a$',sK47)),
inference(unit_resulting_resolution,[],[f1470,f3081,f6751]) ).
tff(f6913,plain,
'least$'('uu$'(sK47)) = 'least$'('uua$'('a$',sK47)),
inference(forward_demodulation,[],[f6877,f3777]) ).
tff(f6953,plain,
~ 'fun_app$h'('uu$'(sK48),'least$'('uu$'(sK47))),
inference(constrained_superposition,[],[f2529,f6913]) ).
tff(f6982,plain,
$false,
inference(forward_subsumption_resolution,[],[f6953,f2258]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP319_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 % Computer : n016.cluster.edu
% 0.12/0.41 % Model : x86_64 x86_64
% 0.12/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.41 % Memory : 8046.5625MB
% 0.12/0.41 % OS : Linux 6.8.0-71-generic
% 0.12/0.41 % CPULimit : 300
% 0.12/0.41 % WCLimit : 300
% 0.12/0.41 % DateTime : Sun Sep 27 12:59:02 UTC 2026
% 0.12/0.41 % CPUTime :
% 0.12/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.47 Running first-order theorem proving
% 0.12/0.47 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.85/1.87 % (2614589)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.85/1.87 % (2614598)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3719080489:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.85/1.87 % (2614600)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3602952712:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.85/1.87 % (2614598)Instruction limit reached!
% 4.85/1.87 % (2614598)------------------------------
% 4.85/1.87 % (2614598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.87 % (2614598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.87 % (2614598)CaDiCaL version: 2.1.3
% 4.85/1.87 % (2614598)Termination reason: Instruction limit
% 4.85/1.87 % (2614598)Termination phase: Property scanning
% 4.85/1.87 % (2614598)Time elapsed: 0.003 s
% 4.85/1.87 % (2614598)Peak memory usage: 86 MB
% 4.85/1.87 % (2614598)Instructions burned: 5 (million)
% 4.85/1.87 % (2614600)Instruction limit reached!
% 4.85/1.87 % (2614600)------------------------------
% 4.85/1.87 % (2614600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.87 % (2614600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.87 % (2614600)CaDiCaL version: 2.1.3
% 4.85/1.87 % (2614600)Termination reason: Instruction limit
% 4.85/1.87 % (2614600)Termination phase: Preprocessing 3
% 4.85/1.87 % (2614600)Time elapsed: 0.021 s
% 4.85/1.87 % (2614600)Peak memory usage: 88 MB
% 4.85/1.87 % (2614600)Instructions burned: 33 (million)
% 4.85/1.87 % (2614594)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1939069052:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.85/1.87 % (2614597)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1377023041:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.85/1.87 % (2614596)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2792245503:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.85/1.87 % (2614595)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=73004223:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.85/1.87 % (2614597)Instruction limit reached!
% 4.85/1.87 % (2614597)------------------------------
% 4.85/1.87 % (2614597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.87 % (2614597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.87 % (2614597)CaDiCaL version: 2.1.3
% 4.85/1.87 % (2614597)Termination reason: Instruction limit
% 4.85/1.87 % (2614597)Termination phase: Property scanning
% 4.85/1.87 % (2614597)Time elapsed: 0.005 s
% 4.85/1.87 % (2614597)Peak memory usage: 86 MB
% 4.85/1.87 % (2614597)Instructions burned: 9 (million)
% 4.85/1.87 % (2614594)Instruction limit reached!
% 4.85/1.87 % (2614594)------------------------------
% 4.85/1.87 % (2614594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.87 % (2614594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.87 % (2614594)CaDiCaL version: 2.1.3
% 4.85/1.87 % (2614594)Termination reason: Instruction limit
% 4.85/1.87 % (2614594)Termination phase: Property scanning
% 4.85/1.87 % (2614594)Time elapsed: 0.012 s
% 4.85/1.87 % (2614594)Peak memory usage: 85 MB
% 4.85/1.87 % (2614594)Instructions burned: 13 (million)
% 4.85/1.87 % (2614599)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3955252087:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.85/1.87 % (2614599)Instruction limit reached!
% 4.85/1.87 % (2614599)------------------------------
% 4.85/1.87 % (2614599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.87 % (2614599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.87 % (2614599)CaDiCaL version: 2.1.3
% 4.85/1.87 % (2614599)Termination reason: Instruction limit
% 4.85/1.87 % (2614599)Termination phase: Property scanning
% 4.85/1.87 % (2614599)Time elapsed: 0.046 s
% 4.85/1.87 % (2614599)Peak memory usage: 88 MB
% 4.85/1.87 % (2614599)Instructions burned: 46 (million)
% 4.85/1.87 % (2614611)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=879697408:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.85/1.87 % (2614610)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2309016578:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 7.47/2.14 % (2614605)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=2233956263:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 7.47/2.14 % (2614603)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=4150152979:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 7.47/2.14 % (2614611)Instruction limit reached!
% 7.47/2.14 % (2614611)------------------------------
% 7.47/2.14 % (2614611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.14 % (2614611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.14 % (2614611)CaDiCaL version: 2.1.3
% 7.47/2.14 % (2614611)Termination reason: Instruction limit
% 7.47/2.14 % (2614611)Termination phase: Preprocessing 2
% 7.47/2.14 % (2614611)Time elapsed: 0.013 s
% 7.47/2.14 % (2614611)Peak memory usage: 87 MB
% 7.47/2.14 % (2614611)Instructions burned: 25 (million)
% 7.47/2.14 % (2614610)Instruction limit reached!
% 7.47/2.14 % (2614610)------------------------------
% 7.47/2.14 % (2614610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.14 % (2614610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.14 % (2614610)CaDiCaL version: 2.1.3
% 7.47/2.14 % (2614610)Termination reason: Instruction limit
% 7.47/2.14 % (2614610)Termination phase: Preprocessing 2
% 7.47/2.14 % (2614610)Time elapsed: 0.012 s
% 7.47/2.14 % (2614610)Peak memory usage: 87 MB
% 7.47/2.14 % (2614610)Instructions burned: 17 (million)
% 7.47/2.14 % (2614603)Instruction limit reached!
% 7.47/2.14 % (2614603)------------------------------
% 7.47/2.14 % (2614603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.14 % (2614603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.14 % (2614603)CaDiCaL version: 2.1.3
% 7.47/2.14 % (2614603)Termination reason: Instruction limit
% 7.47/2.14 % (2614603)Termination phase: SInE selection
% 7.47/2.14 % (2614603)Time elapsed: 0.014 s
% 7.47/2.14 % (2614603)Peak memory usage: 86 MB
% 7.47/2.14 % (2614603)Instructions burned: 15 (million)
% 7.47/2.14 % (2614605)Instruction limit reached!
% 7.47/2.14 % (2614605)------------------------------
% 7.47/2.14 % (2614605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.14 % (2614605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.14 % (2614605)CaDiCaL version: 2.1.3
% 7.47/2.14 % (2614605)Termination reason: Instruction limit
% 7.47/2.14 % (2614605)Termination phase: Preprocessing 3
% 7.47/2.14 % (2614605)Time elapsed: 0.028 s
% 7.47/2.14 % (2614605)Peak memory usage: 87 MB
% 7.47/2.14 % (2614605)Instructions burned: 29 (million)
% 7.47/2.14 % (2614596)Instruction limit reached!
% 7.47/2.14 % (2614596)------------------------------
% 7.47/2.14 % (2614596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.14 % (2614596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.14 % (2614596)CaDiCaL version: 2.1.3
% 7.47/2.14 % (2614596)Termination reason: Instruction limit
% 7.47/2.14 % (2614596)Termination phase: Saturation
% 7.47/2.14 % (2614596)Time elapsed: 0.250 s
% 7.47/2.14 % (2614596)Peak memory usage: 119 MB
% 7.47/2.14 % (2614596)Instructions burned: 201 (million)
% 7.47/2.14 % (2614613)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=610510188:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 7.47/2.14 % (2614595)Instruction limit reached!
% 7.47/2.14 % (2614595)------------------------------
% 7.47/2.14 % (2614595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.14 % (2614595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.14 % (2614595)CaDiCaL version: 2.1.3
% 7.47/2.14 % (2614595)Termination reason: Instruction limit
% 7.47/2.14 % (2614595)Termination phase: Saturation
% 7.47/2.14 % (2614595)Time elapsed: 0.339 s
% 7.47/2.14 % (2614595)Peak memory usage: 119 MB
% 7.47/2.14 % (2614595)Instructions burned: 307 (million)
% 7.47/2.14 % (2614613)Instruction limit reached!
% 7.47/2.14 % (2614613)------------------------------
% 7.47/2.14 % (2614613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.14 % (2614613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.45/2.33 % (2614613)CaDiCaL version: 2.1.3
% 8.45/2.33 % (2614613)Termination reason: Instruction limit
% 8.45/2.33 % (2614613)Termination phase: Preprocessing 3
% 8.45/2.33 % (2614613)Time elapsed: 0.027 s
% 8.45/2.33 % (2614613)Peak memory usage: 87 MB
% 8.45/2.33 % (2614613)Instructions burned: 27 (million)
% 8.45/2.33 % (2614619)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3545722237:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi)
% 8.45/2.33 % (2614619)Instruction limit reached!
% 8.45/2.33 % (2614619)------------------------------
% 8.45/2.33 % (2614619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.45/2.33 % (2614619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.45/2.33 % (2614619)CaDiCaL version: 2.1.3
% 8.45/2.33 % (2614619)Termination reason: Instruction limit
% 8.45/2.33 % (2614619)Termination phase: Property scanning
% 8.45/2.33 % (2614619)Time elapsed: 0.042 s
% 8.45/2.33 % (2614619)Peak memory usage: 89 MB
% 8.45/2.33 % (2614619)Instructions burned: 86 (million)
% 8.45/2.33 % (2614620)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1424995473:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 8.45/2.33 % (2614620)Instruction limit reached!
% 8.45/2.33 % (2614620)------------------------------
% 8.45/2.33 % (2614620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.45/2.33 % (2614620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.45/2.33 % (2614620)CaDiCaL version: 2.1.3
% 8.45/2.33 % (2614620)Termination reason: Instruction limit
% 8.45/2.33 % (2614620)Termination phase: shuffling
% 8.45/2.33 % (2614620)Time elapsed: 0.003 s
% 8.45/2.33 % (2614620)Peak memory usage: 85 MB
% 8.45/2.33 % (2614620)Instructions burned: 2 (million)
% 8.45/2.33 % (2614622)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1531011876:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 8.45/2.33 % (2614621)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3920325754:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 8.45/2.33 % (2614622)Instruction limit reached!
% 8.45/2.33 % (2614622)------------------------------
% 8.45/2.33 % (2614622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.45/2.33 % (2614622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.45/2.33 % (2614622)CaDiCaL version: 2.1.3
% 8.45/2.33 % (2614622)Termination reason: Instruction limit
% 8.45/2.33 % (2614622)Termination phase: Property scanning
% 8.45/2.33 % (2614622)Time elapsed: 0.005 s
% 8.45/2.33 % (2614622)Peak memory usage: 86 MB
% 8.45/2.33 % (2614622)Instructions burned: 4 (million)
% 8.45/2.33 % (2614623)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=977027145:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 8.45/2.33 % (2614626)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=647118571:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 8.45/2.33 % (2614626)Instruction limit reached!
% 8.45/2.33 % (2614626)------------------------------
% 8.45/2.33 % (2614626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.45/2.33 % (2614626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.45/2.33 % (2614626)CaDiCaL version: 2.1.3
% 8.45/2.33 % (2614626)Termination reason: Instruction limit
% 8.45/2.33 % (2614626)Termination phase: Property scanning
% 8.45/2.33 % (2614626)Time elapsed: 0.005 s
% 8.45/2.33 % (2614626)Peak memory usage: 85 MB
% 8.45/2.33 % (2614626)Instructions burned: 9 (million)
% 8.45/2.33 % (2614623)Instruction limit reached!
% 8.45/2.33 % (2614623)------------------------------
% 8.45/2.33 % (2614623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.45/2.33 % (2614623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.45/2.33 % (2614623)CaDiCaL version: 2.1.3
% 8.45/2.33 % (2614623)Termination reason: Instruction limit
% 8.45/2.33 % (2614623)Termination phase: Property scanning
% 8.45/2.33 % (2614623)Time elapsed: 0.062 s
% 8.45/2.33 % (2614623)Peak memory usage: 88 MB
% 8.45/2.33 % (2614623)Instructions burned: 66 (million)
% 8.45/2.33 % (2614628)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1096662546:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 10.70/2.75 % (2614628)Instruction limit reached!
% 10.70/2.75 % (2614628)------------------------------
% 10.70/2.75 % (2614628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.75 % (2614628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.75 % (2614628)CaDiCaL version: 2.1.3
% 10.70/2.75 % (2614628)Termination reason: Instruction limit
% 10.70/2.75 % (2614628)Termination phase: Property scanning
% 10.70/2.75 % (2614628)Time elapsed: 0.002 s
% 10.70/2.75 % (2614628)Peak memory usage: 86 MB
% 10.70/2.75 % (2614628)Instructions burned: 3 (million)
% 10.70/2.75 % (2614625)lrs+10_1_thi=all:si=on:fd=off:random_seed=3494867832:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 10.70/2.75 % (2614625)Instruction limit reached!
% 10.70/2.75 % (2614625)------------------------------
% 10.70/2.75 % (2614625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.75 % (2614625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.75 % (2614625)CaDiCaL version: 2.1.3
% 10.70/2.75 % (2614625)Termination reason: Instruction limit
% 10.70/2.75 % (2614625)Termination phase: Preprocessing 3
% 10.70/2.75 % (2614625)Time elapsed: 0.050 s
% 10.70/2.75 % (2614625)Peak memory usage: 88 MB
% 10.70/2.75 % (2614625)Instructions burned: 54 (million)
% 10.70/2.75 % (2614621)Instruction limit reached!
% 10.70/2.75 % (2614621)------------------------------
% 10.70/2.75 % (2614621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.75 % (2614621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.75 % (2614621)CaDiCaL version: 2.1.3
% 10.70/2.75 % (2614621)Termination reason: Instruction limit
% 10.70/2.75 % (2614621)Termination phase: Saturation
% 10.70/2.75 % (2614621)Time elapsed: 0.207 s
% 10.70/2.75 % (2614621)Peak memory usage: 92 MB
% 10.70/2.75 % (2614621)Instructions burned: 181 (million)
% 10.70/2.75 % (2614630)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1831976276:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 10.70/2.75 % (2614630)Instruction limit reached!
% 10.70/2.75 % (2614630)------------------------------
% 10.70/2.75 % (2614630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.75 % (2614630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.75 % (2614630)CaDiCaL version: 2.1.3
% 10.70/2.75 % (2614630)Termination reason: Instruction limit
% 10.70/2.75 % (2614630)Termination phase: shuffling
% 10.70/2.75 % (2614630)Time elapsed: 0.003 s
% 10.70/2.75 % (2614630)Peak memory usage: 85 MB
% 10.70/2.75 % (2614630)Instructions burned: 2 (million)
% 10.70/2.75 % (2614633)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3391309531:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 10.70/2.75 % (2614636)dis+10_1_si=on:random_seed=684465856:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.70/2.75 % (2614636)Instruction limit reached!
% 10.70/2.75 % (2614636)------------------------------
% 10.70/2.75 % (2614636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.75 % (2614636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.75 % (2614636)CaDiCaL version: 2.1.3
% 10.70/2.75 % (2614636)Termination reason: Instruction limit
% 10.70/2.75 % (2614636)Termination phase: Property scanning
% 10.70/2.75 % (2614636)Time elapsed: 0.010 s
% 10.70/2.75 % (2614636)Peak memory usage: 86 MB
% 10.70/2.75 % (2614636)Instructions burned: 11 (million)
% 10.70/2.75 % (2614637)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1326944084:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 10.70/2.75 % (2614640)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1444363918: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.70/2.75 % (2614641)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1708995850:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 10.70/2.75 % (2614637)Instruction limit reached!
% 10.70/2.75 % (2614637)------------------------------
% 10.70/2.75 % (2614637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.75 % (2614637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.15/3.08 % (2614637)CaDiCaL version: 2.1.3
% 14.15/3.08 % (2614637)Termination reason: Instruction limit
% 14.15/3.08 % (2614637)Termination phase: Naming
% 14.15/3.08 % (2614637)Time elapsed: 0.026 s
% 14.15/3.08 % (2614637)Peak memory usage: 87 MB
% 14.15/3.08 % (2614637)Instructions burned: 26 (million)
% 14.15/3.08 % (2614641)Instruction limit reached!
% 14.15/3.08 % (2614641)------------------------------
% 14.15/3.08 % (2614641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.15/3.08 % (2614641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.15/3.08 % (2614641)CaDiCaL version: 2.1.3
% 14.15/3.08 % (2614641)Termination reason: Instruction limit
% 14.15/3.08 % (2614641)Termination phase: Property scanning
% 14.15/3.08 % (2614641)Time elapsed: 0.002 s
% 14.15/3.08 % (2614641)Peak memory usage: 85 MB
% 14.15/3.08 % (2614641)Instructions burned: 3 (million)
% 14.15/3.08 % (2614633)Instruction limit reached!
% 14.15/3.08 % (2614633)------------------------------
% 14.15/3.08 % (2614633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.15/3.08 % (2614633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.15/3.08 % (2614633)CaDiCaL version: 2.1.3
% 14.15/3.08 % (2614633)Termination reason: Instruction limit
% 14.15/3.08 % (2614633)Termination phase: Saturation
% 14.15/3.08 % (2614633)Time elapsed: 0.163 s
% 14.15/3.08 % (2614633)Peak memory usage: 118 MB
% 14.15/3.08 % (2614633)Instructions burned: 128 (million)
% 14.15/3.08 % (2614640)Instruction limit reached!
% 14.15/3.08 % (2614640)------------------------------
% 14.15/3.08 % (2614640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.15/3.08 % (2614640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.15/3.08 % (2614640)CaDiCaL version: 2.1.3
% 14.15/3.08 % (2614640)Termination reason: Instruction limit
% 14.15/3.08 % (2614640)Termination phase: Preprocessing 3
% 14.15/3.08 % (2614640)Time elapsed: 0.036 s
% 14.15/3.08 % (2614640)Peak memory usage: 88 MB
% 14.15/3.08 % (2614640)Instructions burned: 35 (million)
% 14.15/3.08 % (2614644)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2594325822:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi)
% 14.15/3.08 % (2614643)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3105597617:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 14.15/3.08 % (2614643)Instruction limit reached!
% 14.15/3.08 % (2614643)------------------------------
% 14.15/3.08 % (2614643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.15/3.08 % (2614643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.15/3.08 % (2614643)CaDiCaL version: 2.1.3
% 14.15/3.08 % (2614643)Termination reason: Instruction limit
% 14.15/3.08 % (2614643)Termination phase: Property scanning
% 14.15/3.08 % (2614643)Time elapsed: 0.009 s
% 14.15/3.08 % (2614643)Peak memory usage: 85 MB
% 14.15/3.08 % (2614643)Instructions burned: 8 (million)
% 14.15/3.08 % (2614647)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=4029087150:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 14.15/3.08 % (2614647)Instruction limit reached!
% 14.15/3.08 % (2614647)------------------------------
% 14.15/3.08 % (2614647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.15/3.08 % (2614647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.15/3.08 % (2614647)CaDiCaL version: 2.1.3
% 14.15/3.08 % (2614647)Termination reason: Instruction limit
% 14.15/3.08 % (2614647)Termination phase: Property scanning
% 14.15/3.08 % (2614647)Time elapsed: 0.012 s
% 14.15/3.08 % (2614647)Peak memory usage: 85 MB
% 14.15/3.08 % (2614647)Instructions burned: 13 (million)
% 14.15/3.08 % (2614652)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1186904299:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 14.15/3.08 % (2614652)Instruction limit reached!
% 14.15/3.08 % (2614652)------------------------------
% 14.15/3.08 % (2614652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.15/3.08 % (2614652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.15/3.08 % (2614652)CaDiCaL version: 2.1.3
% 14.15/3.08 % (2614652)Termination reason: Instruction limit
% 14.15/3.08 % (2614652)Termination phase: Property scanning
% 14.15/3.08 % (2614652)Time elapsed: 0.005 s
% 14.15/3.08 % (2614652)Peak memory usage: 86 MB
% 14.15/3.08 % (2614652)Instructions burned: 10 (million)
% 16.20/3.46 % (2614654)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=1666977075:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi)
% 16.20/3.46 % (2614651)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=543621312:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 16.20/3.46 % (2614653)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3311234793:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 16.20/3.46 % (2614657)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=3854690802:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 16.20/3.46 % (2614653)Instruction limit reached!
% 16.20/3.46 % (2614653)------------------------------
% 16.20/3.46 % (2614653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/3.46 % (2614653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/3.46 % (2614653)CaDiCaL version: 2.1.3
% 16.20/3.46 % (2614653)Termination reason: Instruction limit
% 16.20/3.46 % (2614653)Termination phase: Property scanning
% 16.20/3.46 % (2614653)Time elapsed: 0.066 s
% 16.20/3.46 % (2614653)Peak memory usage: 88 MB
% 16.20/3.46 % (2614653)Instructions burned: 71 (million)
% 16.20/3.46 % (2614654)Instruction limit reached!
% 16.20/3.46 % (2614654)------------------------------
% 16.20/3.46 % (2614654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/3.46 % (2614654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/3.46 % (2614654)CaDiCaL version: 2.1.3
% 16.20/3.46 % (2614654)Termination reason: Instruction limit
% 16.20/3.46 % (2614654)Termination phase: Saturation
% 16.20/3.46 % (2614654)Time elapsed: 0.069 s
% 16.20/3.46 % (2614654)Peak memory usage: 90 MB
% 16.20/3.46 % (2614654)Instructions burned: 76 (million)
% 16.20/3.46 % (2614659)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=773613994:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi)
% 16.20/3.46 % (2614644)Instruction limit reached!
% 16.20/3.46 % (2614644)------------------------------
% 16.20/3.46 % (2614644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/3.46 % (2614644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/3.46 % (2614644)CaDiCaL version: 2.1.3
% 16.20/3.46 % (2614644)Termination reason: Instruction limit
% 16.20/3.46 % (2614644)Termination phase: Saturation
% 16.20/3.46 % (2614644)Time elapsed: 0.364 s
% 16.20/3.46 % (2614644)Peak memory usage: 96 MB
% 16.20/3.46 % (2614644)Instructions burned: 370 (million)
% 16.20/3.46 % (2614661)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=598636731:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 16.20/3.46 % (2614659)Instruction limit reached!
% 16.20/3.46 % (2614659)------------------------------
% 16.20/3.46 % (2614659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/3.46 % (2614659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/3.46 % (2614659)CaDiCaL version: 2.1.3
% 16.20/3.46 % (2614659)Termination reason: Instruction limit
% 16.20/3.46 % (2614659)Termination phase: Saturation
% 16.20/3.46 % (2614659)Time elapsed: 0.138 s
% 16.20/3.46 % (2614659)Peak memory usage: 111 MB
% 16.20/3.46 % (2614659)Instructions burned: 130 (million)
% 16.20/3.46 % (2614651)Instruction limit reached!
% 16.20/3.46 % (2614651)------------------------------
% 16.20/3.46 % (2614651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/3.46 % (2614651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/3.46 % (2614651)CaDiCaL version: 2.1.3
% 16.20/3.46 % (2614651)Termination reason: Instruction limit
% 16.20/3.46 % (2614651)Termination phase: Saturation
% 16.20/3.46 % (2614651)Time elapsed: 0.250 s
% 16.20/3.46 % (2614651)Peak memory usage: 118 MB
% 16.20/3.46 % (2614651)Instructions burned: 227 (million)
% 16.20/3.46 % (2614667)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3150638384:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi)
% 16.20/3.46 % (2614666)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2019836707:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi)
% 16.20/3.46 % (2614657)Instruction limit reached!
% 18.77/3.95 % (2614657)------------------------------
% 18.77/3.95 % (2614657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.77/3.95 % (2614657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.77/3.95 % (2614657)CaDiCaL version: 2.1.3
% 18.77/3.95 % (2614657)Termination reason: Instruction limit
% 18.77/3.95 % (2614657)Termination phase: Saturation
% 18.77/3.95 % (2614657)Time elapsed: 0.295 s
% 18.77/3.95 % (2614657)Peak memory usage: 92 MB
% 18.77/3.95 % (2614657)Instructions burned: 294 (million)
% 18.77/3.95 % (2614666)Instruction limit reached!
% 18.77/3.95 % (2614666)------------------------------
% 18.77/3.95 % (2614666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.77/3.95 % (2614666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.77/3.95 % (2614666)CaDiCaL version: 2.1.3
% 18.77/3.95 % (2614666)Termination reason: Instruction limit
% 18.77/3.95 % (2614666)Termination phase: Preprocessing 1
% 18.77/3.95 % (2614666)Time elapsed: 0.036 s
% 18.77/3.95 % (2614666)Peak memory usage: 86 MB
% 18.77/3.95 % (2614666)Instructions burned: 40 (million)
% 18.77/3.95 % (2614661)Instruction limit reached!
% 18.77/3.95 % (2614661)------------------------------
% 18.77/3.95 % (2614661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.77/3.95 % (2614661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.77/3.95 % (2614661)CaDiCaL version: 2.1.3
% 18.77/3.95 % (2614661)Termination reason: Instruction limit
% 18.77/3.95 % (2614661)Termination phase: Saturation
% 18.77/3.95 % (2614661)Time elapsed: 0.192 s
% 18.77/3.95 % (2614661)Peak memory usage: 135 MB
% 18.77/3.95 % (2614661)Instructions burned: 131 (million)
% 18.77/3.95 % (2614667)Instruction limit reached!
% 18.77/3.95 % (2614667)------------------------------
% 18.77/3.95 % (2614667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.77/3.95 % (2614667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.77/3.95 % (2614667)CaDiCaL version: 2.1.3
% 18.77/3.95 % (2614667)Termination reason: Instruction limit
% 18.77/3.95 % (2614667)Termination phase: Saturation
% 18.77/3.95 % (2614667)Time elapsed: 0.152 s
% 18.77/3.95 % (2614667)Peak memory usage: 93 MB
% 18.77/3.95 % (2614667)Instructions burned: 309 (million)
% 18.77/3.95 % (2614669)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3332795044:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 18.77/3.95 % (2614673)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=2600091936:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi)
% 18.77/3.95 % (2614671)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1160168588:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi)
% 18.77/3.95 % (2614675)dis+10_1_si=on:random_seed=2408392064:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi)
% 18.77/3.95 % (2614671)Instruction limit reached!
% 18.77/3.95 % (2614671)------------------------------
% 18.77/3.95 % (2614671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.77/3.95 % (2614671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.77/3.95 % (2614671)CaDiCaL version: 2.1.3
% 18.77/3.95 % (2614671)Termination reason: Instruction limit
% 18.77/3.95 % (2614671)Termination phase: Saturation
% 18.77/3.95 % (2614671)Time elapsed: 0.159 s
% 18.77/3.95 % (2614671)Peak memory usage: 118 MB
% 18.77/3.95 % (2614671)Instructions burned: 131 (million)
% 18.77/3.95 % (2614676)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3085331549:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi)
% 18.77/3.95 % (2614673)Instruction limit reached!
% 18.77/3.95 % (2614673)------------------------------
% 18.77/3.95 % (2614673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.77/3.95 % (2614673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.77/3.95 % (2614673)CaDiCaL version: 2.1.3
% 18.77/3.95 % (2614673)Termination reason: Instruction limit
% 18.77/3.95 % (2614673)Termination phase: Saturation
% 18.77/3.95 % (2614673)Time elapsed: 0.207 s
% 18.77/3.95 % (2614673)Peak memory usage: 118 MB
% 18.77/3.95 % (2614673)Instructions burned: 259 (million)
% 18.77/3.95 % (2614677)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1881175731:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi)
% 23.86/4.52 % (2614679)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3906254244:i=65:nm=16:rtra=on_2981 on theBenchmark for (2981ds/65Mi)
% 23.86/4.52 % (2614679)Instruction limit reached!
% 23.86/4.52 % (2614679)------------------------------
% 23.86/4.52 % (2614679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.86/4.52 % (2614679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/4.52 % (2614679)CaDiCaL version: 2.1.3
% 23.86/4.52 % (2614679)Termination reason: Instruction limit
% 23.86/4.52 % (2614679)Termination phase: Saturation
% 23.86/4.52 % (2614679)Time elapsed: 0.062 s
% 23.86/4.52 % (2614679)Peak memory usage: 90 MB
% 23.86/4.52 % (2614679)Instructions burned: 66 (million)
% 23.86/4.52 % (2614677)Instruction limit reached!
% 23.86/4.52 % (2614677)------------------------------
% 23.86/4.52 % (2614677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.86/4.52 % (2614677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/4.52 % (2614677)CaDiCaL version: 2.1.3
% 23.86/4.52 % (2614677)Termination reason: Instruction limit
% 23.86/4.52 % (2614677)Termination phase: Saturation
% 23.86/4.52 % (2614677)Time elapsed: 0.144 s
% 23.86/4.52 % (2614677)Peak memory usage: 92 MB
% 23.86/4.52 % (2614677)Instructions burned: 141 (million)
% 23.86/4.52 % (2614686)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=2275605347:s2a=on:i=128:s2at=5:ins=3:rtra=on_2979 on theBenchmark for (2979ds/128Mi)
% 23.86/4.52 % (2614684)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3799764081:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi)
% 23.86/4.52 % (2614669)Instruction limit reached!
% 23.86/4.52 % (2614669)------------------------------
% 23.86/4.52 % (2614669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.86/4.52 % (2614669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/4.52 % (2614669)CaDiCaL version: 2.1.3
% 23.86/4.52 % (2614669)Termination reason: Instruction limit
% 23.86/4.52 % (2614669)Termination phase: Saturation
% 23.86/4.52 % (2614669)Time elapsed: 0.512 s
% 23.86/4.52 % (2614669)Peak memory usage: 138 MB
% 23.86/4.52 % (2614669)Instructions burned: 598 (million)
% 23.86/4.52 % (2614686)Instruction limit reached!
% 23.86/4.52 % (2614686)------------------------------
% 23.86/4.52 % (2614686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.86/4.52 % (2614686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/4.52 % (2614686)CaDiCaL version: 2.1.3
% 23.86/4.52 % (2614686)Termination reason: Instruction limit
% 23.86/4.52 % (2614686)Termination phase: Saturation
% 23.86/4.52 % (2614686)Time elapsed: 0.088 s
% 23.86/4.52 % (2614686)Peak memory usage: 119 MB
% 23.86/4.52 % (2614686)Instructions burned: 131 (million)
% 23.86/4.52 % (2614684)Instruction limit reached!
% 23.86/4.52 % (2614684)------------------------------
% 23.86/4.52 % (2614684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.86/4.52 % (2614684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/4.52 % (2614684)CaDiCaL version: 2.1.3
% 23.86/4.52 % (2614684)Termination reason: Instruction limit
% 23.86/4.52 % (2614684)Termination phase: Saturation
% 23.86/4.52 % (2614684)Time elapsed: 0.123 s
% 23.86/4.52 % (2614684)Peak memory usage: 91 MB
% 23.86/4.52 % (2614684)Instructions burned: 121 (million)
% 23.86/4.52 % (2614676)Instruction limit reached!
% 23.86/4.52 % (2614676)------------------------------
% 23.86/4.52 % (2614676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.86/4.52 % (2614676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/4.52 % (2614676)CaDiCaL version: 2.1.3
% 23.86/4.52 % (2614676)Termination reason: Instruction limit
% 23.86/4.52 % (2614676)Termination phase: Saturation
% 23.86/4.52 % (2614676)Time elapsed: 0.371 s
% 23.86/4.52 % (2614676)Peak memory usage: 97 MB
% 23.86/4.52 % (2614676)Instructions burned: 383 (million)
% 23.86/4.52 % (2614690)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=3093693352:i=39:ins=3:rtra=on_2978 on theBenchmark for (2978ds/39Mi)
% 23.86/4.52 % (2614690)Instruction limit reached!
% 23.86/4.52 % (2614690)------------------------------
% 23.86/4.52 % (2614690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.86/4.52 % (2614690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614690)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614690)Termination reason: Instruction limit
% 24.06/4.82 % (2614690)Termination phase: Preprocessing 3
% 24.06/4.82 % (2614690)Time elapsed: 0.040 s
% 24.06/4.82 % (2614690)Peak memory usage: 88 MB
% 24.06/4.82 % (2614690)Instructions burned: 39 (million)
% 24.06/4.82 % (2614691)dis+1010_1_to=kbo:si=on:random_seed=2029064357:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi)
% 24.06/4.82 % (2614694)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=279628540:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi)
% 24.06/4.82 % (2614696)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2065985883:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi)
% 24.06/4.82 % (2614699)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=715930161:i=349:rtra=on_2976 on theBenchmark for (2976ds/349Mi)
% 24.06/4.82 % (2614691)Instruction limit reached!
% 24.06/4.82 % (2614691)------------------------------
% 24.06/4.82 % (2614691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614691)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614691)Termination reason: Instruction limit
% 24.06/4.82 % (2614691)Termination phase: Saturation
% 24.06/4.82 % (2614691)Time elapsed: 0.167 s
% 24.06/4.82 % (2614691)Peak memory usage: 92 MB
% 24.06/4.82 % (2614691)Instructions burned: 175 (million)
% 24.06/4.82 % (2614697)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2919655375:thitd=on:i=215:nm=0:rtra=on:ev=force_2976 on theBenchmark for (2976ds/215Mi)
% 24.06/4.82 % (2614700)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3869140759:st=2:i=295:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/295Mi)
% 24.06/4.82 % (2614699)Instruction limit reached!
% 24.06/4.82 % (2614699)------------------------------
% 24.06/4.82 % (2614699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614699)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614699)Termination reason: Instruction limit
% 24.06/4.82 % (2614699)Termination phase: Saturation
% 24.06/4.82 % (2614699)Time elapsed: 0.204 s
% 24.06/4.82 % (2614699)Peak memory usage: 120 MB
% 24.06/4.82 % (2614699)Instructions burned: 349 (million)
% 24.06/4.82 % (2614694)Instruction limit reached!
% 24.06/4.82 % (2614694)------------------------------
% 24.06/4.82 % (2614694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614694)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614694)Termination reason: Instruction limit
% 24.06/4.82 % (2614694)Termination phase: Saturation
% 24.06/4.82 % (2614694)Time elapsed: 0.305 s
% 24.06/4.82 % (2614694)Peak memory usage: 121 MB
% 24.06/4.82 % (2614694)Instructions burned: 330 (million)
% 24.06/4.82 % (2614697)Instruction limit reached!
% 24.06/4.82 % (2614697)------------------------------
% 24.06/4.82 % (2614697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614697)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614697)Termination reason: Instruction limit
% 24.06/4.82 % (2614697)Termination phase: Saturation
% 24.06/4.82 % (2614697)Time elapsed: 0.249 s
% 24.06/4.82 % (2614697)Peak memory usage: 135 MB
% 24.06/4.82 % (2614697)Instructions burned: 215 (million)
% 24.06/4.82 % (2614706)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1050980538:i=328:kws=inv_frequency:nm=20:rtra=on_2973 on theBenchmark for (2973ds/328Mi)
% 24.06/4.82 % (2614675)Instruction limit reached!
% 24.06/4.82 % (2614675)------------------------------
% 24.06/4.82 % (2614675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614675)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614675)Termination reason: Instruction limit
% 24.06/4.82 % (2614675)Termination phase: Saturation
% 24.06/4.82 % (2614675)Time elapsed: 0.960 s
% 24.06/4.82 % (2614675)Peak memory usage: 98 MB
% 24.06/4.82 % (2614675)Instructions burned: 1000 (million)
% 24.06/4.82 % (2614700)Instruction limit reached!
% 24.06/4.82 % (2614700)------------------------------
% 24.06/4.82 % (2614700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614700)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614700)Termination reason: Instruction limit
% 24.06/4.82 % (2614700)Termination phase: Saturation
% 24.06/4.82 % (2614700)Time elapsed: 0.295 s
% 24.06/4.82 % (2614700)Peak memory usage: 92 MB
% 24.06/4.82 % (2614700)Instructions burned: 295 (million)
% 24.06/4.82 % (2614709)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2568043904:i=281:gtgl=2:rtra=on:gtg=all_2972 on theBenchmark for (2972ds/281Mi)
% 24.06/4.82 % (2614710)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=238561904:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/484Mi)
% 24.06/4.82 % (2614709)Instruction limit reached!
% 24.06/4.82 % (2614709)------------------------------
% 24.06/4.82 % (2614709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614709)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614709)Termination reason: Instruction limit
% 24.06/4.82 % (2614709)Termination phase: Saturation
% 24.06/4.82 % (2614709)Time elapsed: 0.163 s
% 24.06/4.82 % (2614709)Peak memory usage: 119 MB
% 24.06/4.82 % (2614709)Instructions burned: 282 (million)
% 24.06/4.82 % (2614714)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3683579941:i=471:thf=on:kws=precedence:rtra=on_2970 on theBenchmark for (2970ds/471Mi)
% 24.06/4.82 % (2614696)Instruction limit reached!
% 24.06/4.82 % (2614696)------------------------------
% 24.06/4.82 % (2614696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614696)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614711)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=598017928:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2970 on theBenchmark for (2970ds/321Mi)
% 24.06/4.82 % (2614696)Termination reason: Instruction limit
% 24.06/4.82 % (2614696)Termination phase: Saturation
% 24.06/4.82 % (2614696)Time elapsed: 0.576 s
% 24.06/4.82 % (2614696)Peak memory usage: 137 MB
% 24.06/4.82 % (2614696)Instructions burned: 484 (million)
% 24.06/4.82 % (2614713)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=984888248:i=416:rtra=on:gtg=position:ss=axioms_2970 on theBenchmark for (2970ds/416Mi)
% 24.06/4.82 % (2614706)Instruction limit reached!
% 24.06/4.82 % (2614706)------------------------------
% 24.06/4.82 % (2614706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614706)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614706)Termination reason: Instruction limit
% 24.06/4.82 % (2614706)Termination phase: Saturation
% 24.06/4.82 % (2614706)Time elapsed: 0.360 s
% 24.06/4.82 % (2614706)Peak memory usage: 119 MB
% 24.06/4.82 % (2614706)Instructions burned: 329 (million)
% 24.06/4.82 % (2614710)First to succeed.
% 24.06/4.82 % (2614710)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2614589"
% 24.06/4.82 % (2614721)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=2784364333:avsq=on:i=276:avsqr=1,2:rtra=on_2968 on theBenchmark for (2968ds/276Mi)
% 24.06/4.82 % (2614722)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=4243139680:i=375:kws=inv_arity_squared:rtra=on_2968 on theBenchmark for (2968ds/375Mi)
% 24.06/4.82 % (2614711)Instruction limit reached!
% 24.06/4.82 % (2614711)------------------------------
% 24.06/4.82 % (2614711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614711)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614711)Termination reason: Instruction limit
% 24.06/4.82 % (2614711)Termination phase: Saturation
% 24.06/4.82 % (2614711)Time elapsed: 0.363 s
% 24.06/4.82 % (2614711)Peak memory usage: 118 MB
% 24.06/4.82 % (2614711)Instructions burned: 321 (million)
% 24.06/4.82 % (2614721)Instruction limit reached!
% 24.06/4.82 % (2614721)------------------------------
% 24.06/4.82 % (2614721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614721)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614721)Termination reason: Instruction limit
% 24.06/4.82 % (2614721)Termination phase: Saturation
% 24.06/4.82 % (2614721)Time elapsed: 0.177 s
% 24.06/4.82 % (2614721)Peak memory usage: 137 MB
% 24.06/4.82 % (2614721)Instructions burned: 276 (million)
% 24.06/4.82 % (2614713)Instruction limit reached!
% 24.06/4.82 % (2614713)------------------------------
% 24.06/4.82 % (2614713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614713)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614713)Termination reason: Instruction limit
% 24.06/4.82 % (2614713)Termination phase: Saturation
% 24.06/4.82 % (2614713)Time elapsed: 0.380 s
% 24.06/4.82 % (2614713)Peak memory usage: 118 MB
% 24.06/4.82 % (2614713)Instructions burned: 416 (million)
% 24.06/4.82 % (2614724)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2335333691:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/387Mi)
% 24.06/4.82 % (2614714)Instruction limit reached!
% 24.06/4.82 % (2614714)------------------------------
% 24.06/4.82 % (2614714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.06/4.82 % (2614714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.06/4.82 % (2614714)CaDiCaL version: 2.1.3
% 24.06/4.82 % (2614714)Termination reason: Instruction limit
% 24.06/4.82 % (2614714)Termination phase: Saturation
% 24.06/4.82 % (2614714)Time elapsed: 0.542 s
% 24.06/4.82 % (2614714)Peak memory usage: 121 MB
% 24.06/4.82 % (2614714)Instructions burned: 471 (million)
% 24.06/4.82 % (2614729)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1823447395:i=334:rtra=on_2964 on theBenchmark for (2964ds/334Mi)
% 24.06/4.82 % (2614728)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3648956782:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2964 on theBenchmark for (2964ds/513Mi)
% 24.06/4.82 % (2614710)Refutation found. Thanks to Tanya!
% 24.06/4.82 % SZS status Theorem for theBenchmark
% 24.06/4.82 % SZS output start Proof for theBenchmark
% See solution above
% 27.16/5.05 % (2614710)------------------------------
% 27.16/5.05 % (2614710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.16/5.05 % (2614710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.16/5.06 % (2614710)CaDiCaL version: 2.1.3
% 27.16/5.06 % (2614710)Termination reason: Refutation
% 27.16/5.06 % (2614710)Time elapsed: 0.220 s
% 27.16/5.06 % (2614710)Peak memory usage: 91 MB
% 27.16/5.06 % (2614710)Instructions burned: 234 (million)
% 27.16/5.06 % (2614710)------------------------------
% 27.16/5.06 % (2614710)------------------------------
% 27.16/5.06 % (2614589)Success in time 3.792 s
% 27.16/5.06 % Vampire exiting
%------------------------------------------------------------------------------