%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP405_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:48 AM UTC 2026
% Result : Theorem 53.86s 8.29s
% Output : Refutation 54.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 20
% Syntax : Number of formulae : 112 ( 49 unt; 0 typ; 4 def)
% Number of atoms : 209 ( 68 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 170 ( 73 ~; 69 |; 16 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number arithmetic : 255 ( 88 atm; 75 fun; 71 num; 21 var)
% Number of types : 24 ( 22 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 27 ( 23 usr; 5 prp; 0-4 aty)
% Number of functors : 322 ( 319 usr; 26 con; 0-4 aty)
% Number of variables : 107 ( 0 sgn 105 !; 2 ?; 107 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'Int_bool_fun$': $tType ).
tff(type_def_6,type,
'Nat_nat_bool_fun_fun$': $tType ).
tff(type_def_7,type,
'A_nat_fun$': $tType ).
tff(type_def_8,type,
'Clock$': $tType ).
tff(type_def_9,type,
'Nat_clock_bool_a_tag_const_prod_fun_fun$': $tType ).
tff(type_def_10,type,
'Int_int_fun$': $tType ).
tff(type_def_11,type,
'Clock_bool_a_tag_const_prod_fun$': $tType ).
tff(type_def_12,type,
'A_run$': $tType ).
tff(type_def_13,type,
'A_tag_const$': $tType ).
tff(type_def_14,type,
'Nat_nat_fun$': $tType ).
tff(type_def_15,type,
'Int_nat_fun$': $tType ).
tff(type_def_16,type,
'A_tag_const_a_tag_const_prod_bool_fun$': $tType ).
tff(type_def_17,type,
'Nat$': $tType ).
tff(type_def_18,type,
tlbool: $tType ).
tff(type_def_19,type,
'Bool_a_tag_const_prod$': $tType ).
tff(type_def_20,type,
'A_run_set$': $tType ).
tff(type_def_21,type,
'A_TESL_atomic$': $tType ).
tff(type_def_22,type,
'A_run_bool_fun$': $tType ).
tff(type_def_23,type,
'Int_int_bool_fun_fun$': $tType ).
tff(type_def_24,type,
'Nat_bool_fun$': $tType ).
tff(type_def_25,type,
'Nat_set$': $tType ).
tff(type_def_26,type,
'Nat_int_fun$': $tType ).
tff(func_def_0,type,
'n_0$': 'Nat$' ).
tff(func_def_1,type,
'tick_count$': ( 'A_run$' * 'Clock$' ) > 'Nat_nat_fun$' ).
tff(func_def_2,type,
'is_subrun$': 'A_run$' > 'A_run_bool_fun$' ).
tff(func_def_3,type,
'tagRelation$': ( 'Clock$' * 'Clock$' * 'A_tag_const_a_tag_const_prod_bool_fun$' ) > 'A_TESL_atomic$' ).
tff(func_def_4,type,
'uuf$': ( 'Clock$' * 'Clock$' ) > 'A_run_bool_fun$' ).
tff(func_def_5,type,
'fun_app$h': ( 'Int_int_fun$' * $int ) > $int ).
tff(func_def_6,type,
'implies$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_7,type,
'uul$': ( 'Clock$' * 'Clock$' ) > 'A_run_bool_fun$' ).
tff(func_def_8,type,
'strictlyPrecedes$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_9,type,
'fun_app$a': ( 'Clock_bool_a_tag_const_prod_fun$' * 'Clock$' ) > 'Bool_a_tag_const_prod$' ).
tff(func_def_10,type,
'zero$': 'Nat$' ).
tff(func_def_11,type,
'tick_count_strict$': ( 'A_run$' * 'Clock$' ) > 'Nat_nat_fun$' ).
tff(func_def_12,type,
'sn_0$': 'Nat$' ).
tff(func_def_13,type,
'size$': 'A_TESL_atomic$' > 'Nat$' ).
tff(func_def_14,type,
'fun_app$d': ( 'Nat_int_fun$' * 'Nat$' ) > $int ).
tff(func_def_15,type,
'uug$': ( 'Nat_nat_fun$' * 'A_run$' * 'Nat$' * 'Clock$' ) > 'Nat_bool_fun$' ).
tff(func_def_16,type,
'n$': 'Nat$' ).
tff(func_def_17,type,
'uue$': ( 'Clock$' * 'Clock$' ) > 'A_run_bool_fun$' ).
tff(func_def_18,type,
'nat$': 'Int_nat_fun$' ).
tff(func_def_19,type,
'run_tick_count_strictly$': ( 'A_run$' * 'Clock$' ) > 'Nat_nat_fun$' ).
tff(func_def_20,type,
'tESL_interpretation_atomic$': 'A_TESL_atomic$' > 'A_run_set$' ).
tff(func_def_21,type,
'weaklyPrecedes$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_22,type,
'dilating$': ( 'Nat_nat_fun$' * 'A_run$' ) > 'A_run_bool_fun$' ).
tff(func_def_23,type,
'sporadicOn$': ( 'Clock$' * 'A_tag_const$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_24,type,
'collect$a': 'A_run_bool_fun$' > 'A_run_set$' ).
tff(func_def_25,type,
'impliesNot$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_26,type,
'of_nat$': 'Nat_int_fun$' ).
tff(func_def_27,type,
'c_1$': 'Clock$' ).
tff(func_def_28,type,
'kills$': ( 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_29,type,
'less$': 'Nat_nat_bool_fun_fun$' ).
tff(func_def_30,type,
'uuc$': 'A_run_bool_fun$' ).
tff(func_def_31,type,
'fun_app$g': ( 'Nat_nat_bool_fun_fun$' * 'Nat$' ) > 'Nat_bool_fun$' ).
tff(func_def_32,type,
tltrue: tlbool ).
tff(func_def_33,type,
'size_TESL_atomic$': ( 'A_nat_fun$' * 'A_TESL_atomic$' ) > 'Nat$' ).
tff(func_def_34,type,
'plus$': 'Nat$' > 'Nat_nat_fun$' ).
tff(func_def_35,type,
'r$': 'A_run$' ).
tff(func_def_36,type,
'greatest$': 'Int_bool_fun$' > $int ).
tff(func_def_37,type,
'one$': 'Nat$' ).
tff(func_def_38,type,
'fun_app$c': ( 'Int_nat_fun$' * $int ) > 'Nat$' ).
tff(func_def_39,type,
'fun_app$e': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_40,type,
'rep_run$': 'A_run$' > 'Nat_clock_bool_a_tag_const_prod_fun_fun$' ).
tff(func_def_41,type,
'f$': 'Nat_nat_fun$' ).
tff(func_def_42,type,
'collect$': 'Nat_bool_fun$' > 'Nat_set$' ).
tff(func_def_43,type,
'sub$': 'A_run$' ).
tff(func_def_44,type,
'timeDelayedBy$': ( 'Clock$' * 'A_tag_const$' * 'Clock$' * 'Clock$' ) > 'A_TESL_atomic$' ).
tff(func_def_45,type,
'uu$': 'Nat_set$' > 'Nat_bool_fun$' ).
tff(func_def_46,type,
'uub$': 'A_run_bool_fun$' ).
tff(func_def_47,type,
'uud$': ( 'Clock$' * 'Clock$' ) > 'A_run_bool_fun$' ).
tff(func_def_48,type,
'fun_app$b': ( 'Nat_clock_bool_a_tag_const_prod_fun_fun$' * 'Nat$' ) > 'Clock_bool_a_tag_const_prod_fun$' ).
tff(func_def_49,type,
'less_eq$': 'Nat_nat_bool_fun_fun$' ).
tff(func_def_50,type,
'uuj$': ( 'Clock$' * 'Clock$' ) > 'A_run_bool_fun$' ).
tff(func_def_51,type,
'fun_app$j': ( 'Int_int_bool_fun_fun$' * $int ) > 'Int_bool_fun$' ).
tff(func_def_52,type,
'dil_inverse$': 'Nat_nat_fun$' > 'Nat_nat_fun$' ).
tff(func_def_53,type,
tlfalse: tlbool ).
tff(func_def_54,type,
'uui$': ( 'Clock$' * 'Clock$' ) > 'A_run_bool_fun$' ).
tff(func_def_55,type,
'greatest$a': 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_56,type,
'dense_run$': 'A_run_bool_fun$' ).
tff(func_def_57,type,
'suc$': 'Nat_nat_fun$' ).
tff(func_def_58,type,
'uuh$': ( 'Nat_nat_fun$' * 'A_run$' * 'Nat$' * 'Clock$' ) > 'Nat_bool_fun$' ).
tff(func_def_59,type,
'uuk$': ( 'Clock$' * 'Clock$' ) > 'A_run_bool_fun$' ).
tff(func_def_60,type,
'uum$': ( 'Clock$' * 'Clock$' ) > 'A_run_bool_fun$' ).
tff(func_def_61,type,
'c_2$': 'Clock$' ).
tff(func_def_62,type,
'run_tick_count$': ( 'A_run$' * 'Clock$' ) > 'Nat_nat_fun$' ).
tff(func_def_63,type,
'uua$': 'A_run_set$' > 'A_run_bool_fun$' ).
tff(func_def_68,type,
sK8: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_69,type,
sK9: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_70,type,
sK10: ( 'Nat_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_71,type,
sK11: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_72,type,
sK12: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_73,type,
sK13: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_74,type,
sK14: $int > $int ).
tff(func_def_75,type,
sK15: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_76,type,
sK16: $int > $int ).
tff(func_def_77,type,
sK17: 'Nat$' > 'Nat$' ).
tff(func_def_78,type,
sK18: 'Int_nat_fun$' > $int ).
tff(func_def_79,type,
sK19: 'Int_nat_fun$' > $int ).
tff(func_def_80,type,
sK20: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_81,type,
sK21: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_82,type,
sK22: ( 'A_run$' * 'Clock$' * 'Clock$' ) > 'Nat$' ).
tff(func_def_83,type,
sK23: ( 'A_run$' * 'A_run$' ) > 'Nat_nat_fun$' ).
tff(func_def_84,type,
sK24: 'Int_int_fun$' > $int ).
tff(func_def_85,type,
sK25: 'Int_int_fun$' > $int ).
tff(func_def_86,type,
sK26: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_87,type,
sK27: 'Nat$' > 'Nat$' ).
tff(func_def_88,type,
sK28: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_89,type,
sK29: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_90,type,
sK30: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_91,type,
sK31: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_92,type,
sK32: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_93,type,
sK33: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_94,type,
sK34: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_95,type,
sK35: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_96,type,
sK36: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_97,type,
sK37: 'Int_int_fun$' > $int ).
tff(func_def_98,type,
sK38: 'Int_int_fun$' > $int ).
tff(func_def_99,type,
sK39: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_100,type,
sK40: ( 'Nat$' * 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_101,type,
sK41: 'Int_int_fun$' > $int ).
tff(func_def_102,type,
sK42: 'Int_int_fun$' > $int ).
tff(func_def_103,type,
sK43: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_104,type,
sK44: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_105,type,
sK45: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_106,type,
sK46: 'Int_nat_fun$' > $int ).
tff(func_def_107,type,
sK47: 'Int_nat_fun$' > $int ).
tff(func_def_108,type,
sK48: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_109,type,
sK49: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_110,type,
sK50: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_111,type,
sK51: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_112,type,
sK52: 'Int_nat_fun$' > $int ).
tff(func_def_113,type,
sK53: 'Int_nat_fun$' > $int ).
tff(func_def_114,type,
sK54: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_115,type,
sK55: 'Int_int_fun$' > $int ).
tff(func_def_116,type,
sK56: 'Int_int_fun$' > $int ).
tff(func_def_117,type,
sK57: ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_118,type,
sK58: 'Nat$' ).
tff(func_def_119,type,
sK59: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_120,type,
sK60: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_121,type,
sK61: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_122,type,
sK62: ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_123,type,
sK63: ( 'Clock$' * 'Clock$' * 'A_run$' ) > 'Nat$' ).
tff(func_def_124,type,
sK64: ( 'A_run$' * 'Clock$' * 'Clock$' ) > 'Nat$' ).
tff(func_def_125,type,
sK65: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_126,type,
sK66: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_127,type,
sK67: ( 'Nat$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_128,type,
sK68: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_129,type,
sK69: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_130,type,
sK70: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_131,type,
sK71: 'Int_nat_fun$' > $int ).
tff(func_def_132,type,
sK72: 'Int_nat_fun$' > $int ).
tff(func_def_133,type,
sK73: ( 'Nat$' * 'Nat$' * 'A_run$' * 'Clock$' ) > 'Nat$' ).
tff(func_def_134,type,
sK74: ( 'Nat$' * 'Nat$' * 'A_run$' * 'Clock$' ) > 'A_run$' ).
tff(func_def_135,type,
sK75: ( 'Nat$' * 'Nat$' * 'A_run$' * 'Clock$' ) > 'Clock$' ).
tff(func_def_136,type,
sK76: ( 'Clock$' * 'Nat$' * 'Nat$' * 'A_run$' ) > 'A_run$' ).
tff(func_def_137,type,
sK77: ( 'Clock$' * 'Nat$' * 'Nat$' * 'A_run$' ) > 'Clock$' ).
tff(func_def_138,type,
sK78: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_139,type,
sK79: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_140,type,
sK80: ( 'Clock$' * 'Clock$' * 'A_run$' ) > 'Nat$' ).
tff(func_def_141,type,
sK81: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_142,type,
sK82: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_143,type,
sK83: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_144,type,
sK84: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_145,type,
sK85: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_146,type,
sK86: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_147,type,
sK87: 'A_run$' > 'Nat$' ).
tff(func_def_148,type,
sK88: ( 'Nat$' * 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_149,type,
sK89: ( 'Nat$' * 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_150,type,
sK90: 'Nat$' ).
tff(func_def_151,type,
sK91: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_152,type,
sK92: 'Nat$' > 'Nat$' ).
tff(func_def_153,type,
sK93: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_154,type,
sK94: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_155,type,
sK95: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_156,type,
sK96: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_157,type,
sK97: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_158,type,
sK98: ( 'A_run_bool_fun$' * 'A_run_bool_fun$' ) > 'A_run$' ).
tff(func_def_159,type,
sK99: 'Int_nat_fun$' > $int ).
tff(func_def_160,type,
sK100: 'Int_nat_fun$' > $int ).
tff(func_def_161,type,
sK101: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_162,type,
sK102: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_163,type,
sK103: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_164,type,
sK104: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_165,type,
sK105: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_166,type,
sK106: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_167,type,
sK107: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_168,type,
sK108: ( 'A_run$' * 'Clock$' * 'Clock$' ) > 'Nat$' ).
tff(func_def_169,type,
sK109: 'Int_int_fun$' > $int ).
tff(func_def_170,type,
sK110: 'Int_int_fun$' > $int ).
tff(func_def_171,type,
sK111: ( 'Clock$' * 'Clock$' * 'A_run$' ) > 'Nat$' ).
tff(func_def_172,type,
sK112: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_173,type,
sK113: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_174,type,
sK114: ( 'Nat_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_175,type,
sK115: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_176,type,
sK116: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_177,type,
sK117: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_178,type,
sK118: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_179,type,
sK119: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_180,type,
sK120: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_181,type,
sK121: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_182,type,
sK122: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_183,type,
sK123: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_184,type,
sK124: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_185,type,
sK125: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_186,type,
sK126: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_187,type,
sK127: 'Int_nat_fun$' > $int ).
tff(func_def_188,type,
sK128: 'Int_nat_fun$' > $int ).
tff(func_def_189,type,
sK129: 'Nat$' ).
tff(func_def_190,type,
sK130: ( 'Clock$' * 'A_run$' * 'Clock$' ) > 'Nat$' ).
tff(func_def_191,type,
sK131: ( 'A_run$' * 'Clock$' * 'Clock$' ) > 'Nat$' ).
tff(func_def_192,type,
sK132: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_193,type,
sK133: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_194,type,
sK134: 'Nat_nat_fun$' ).
tff(func_def_195,type,
sK135: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_196,type,
sK136: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_197,type,
sK137: 'Nat$' > 'Nat$' ).
tff(func_def_198,type,
sK138: 'Nat$' > 'Nat$' ).
tff(func_def_199,type,
sK139: ( 'Int_bool_fun$' * $int ) > $int ).
tff(func_def_200,type,
sK140: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_201,type,
sK141: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_202,type,
sK142: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_203,type,
sK143: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_204,type,
sK144: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_205,type,
sK145: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_206,type,
sK146: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_207,type,
sK147: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_208,type,
sK148: ( 'Nat$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_209,type,
sK149: 'Int_int_fun$' > $int ).
tff(func_def_210,type,
sK150: 'Int_int_fun$' > $int ).
tff(func_def_211,type,
sK151: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_212,type,
sK152: 'Int_int_fun$' > $int ).
tff(func_def_213,type,
sK153: 'Int_int_fun$' > $int ).
tff(func_def_214,type,
sK154: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_215,type,
sK155: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_216,type,
sK156: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_217,type,
sK157: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_218,type,
sK158: 'A_run$' > 'Nat$' ).
tff(func_def_219,type,
sK159: ( 'A_run$' * 'Nat$' ) > 'Clock$' ).
tff(func_def_220,type,
sK160: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_221,type,
sK161: 'Nat$' > 'Nat$' ).
tff(func_def_222,type,
sK162: 'A_run$' > 'Nat$' ).
tff(func_def_223,type,
sK163: ( 'Int_bool_fun$' * 'Int_bool_fun$' ) > $int ).
tff(func_def_224,type,
sK164: ( 'Int_bool_fun$' * $int ) > $int ).
tff(func_def_225,type,
sK165: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_226,type,
sK166: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_227,type,
sK167: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_228,type,
sK168: 'Int_int_fun$' > $int ).
tff(func_def_229,type,
sK169: 'Int_int_fun$' > $int ).
tff(func_def_230,type,
sK170: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_231,type,
sK171: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_232,type,
sK172: 'Int_int_fun$' > $int ).
tff(func_def_233,type,
sK173: 'Int_int_fun$' > $int ).
tff(func_def_234,type,
sK174: 'Int_nat_fun$' > $int ).
tff(func_def_235,type,
sK175: 'Int_nat_fun$' > $int ).
tff(func_def_236,type,
sK176: 'Int_int_fun$' > $int ).
tff(func_def_237,type,
sK177: 'Int_int_fun$' > $int ).
tff(func_def_238,type,
sK178: ( 'Nat$' * 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_239,type,
sK179: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_240,type,
sK180: 'Int_int_fun$' > $int ).
tff(func_def_241,type,
sK181: 'Int_int_fun$' > $int ).
tff(func_def_242,type,
sK182: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_243,type,
sK183: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_244,type,
sK184: 'Int_nat_fun$' > $int ).
tff(func_def_245,type,
sK185: 'Int_nat_fun$' > $int ).
tff(func_def_246,type,
sK186: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_247,type,
sK187: 'Int_nat_fun$' > $int ).
tff(func_def_248,type,
sK188: 'Int_nat_fun$' > $int ).
tff(func_def_249,type,
sK189: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_250,type,
sK190: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_251,type,
sK191: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_252,type,
sK192: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_253,type,
sK193: 'Int_int_fun$' > $int ).
tff(func_def_254,type,
sK194: 'Int_int_fun$' > $int ).
tff(func_def_255,type,
sK195: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_256,type,
sK196: ( 'Nat$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_257,type,
sK197: ( 'Nat$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_258,type,
sK198: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_259,type,
sK199: ( 'Nat$' * 'Nat$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_260,type,
sK200: ( 'Nat$' * 'Nat$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_261,type,
sK201: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_262,type,
sK202: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_263,type,
sK203: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_264,type,
sK204: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_265,type,
sK205: ( 'A_run$' * 'Clock$' ) > 'Nat$' ).
tff(func_def_266,type,
sK206: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_267,type,
sK207: 'A_TESL_atomic$' > 'A_tag_const$' ).
tff(func_def_268,type,
sK208: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_269,type,
sK209: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_270,type,
sK210: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_271,type,
sK211: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_272,type,
sK212: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_273,type,
sK213: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_274,type,
sK214: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_275,type,
sK215: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_276,type,
sK216: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_277,type,
sK217: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_278,type,
sK218: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_279,type,
sK219: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_280,type,
sK220: 'A_TESL_atomic$' > 'A_tag_const$' ).
tff(func_def_281,type,
sK221: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_282,type,
sK222: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_283,type,
sK223: 'A_TESL_atomic$' > 'A_tag_const_a_tag_const_prod_bool_fun$' ).
tff(func_def_284,type,
sK224: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_285,type,
sK225: 'A_TESL_atomic$' > 'Clock$' ).
tff(func_def_286,type,
sK226: ( 'Clock$' * 'Clock$' * 'A_run$' ) > 'Nat$' ).
tff(func_def_287,type,
sK227: ( 'Clock$' * 'Clock$' * 'A_run$' ) > 'Nat$' ).
tff(func_def_288,type,
sK228: 'Int_int_fun$' > $int ).
tff(func_def_289,type,
sK229: 'Int_int_fun$' > $int ).
tff(func_def_290,type,
sK230: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_291,type,
sK231: 'Nat_set$' > 'Nat$' ).
tff(func_def_292,type,
sK232: ( 'Nat$' * 'Nat$' * 'A_run$' * 'Clock$' ) > 'Clock$' ).
tff(func_def_293,type,
sK233: ( 'Nat$' * 'Nat$' * 'A_run$' * 'Clock$' ) > 'A_run$' ).
tff(func_def_294,type,
sK234: ( 'Nat$' * 'Clock$' * 'Nat$' * 'A_run$' ) > 'A_run$' ).
tff(func_def_295,type,
sK235: ( 'Nat$' * 'Clock$' * 'Nat$' * 'A_run$' ) > 'Nat$' ).
tff(func_def_296,type,
sK236: ( 'Nat$' * 'Clock$' * 'Nat$' * 'A_run$' ) > 'Clock$' ).
tff(func_def_297,type,
sK237: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_298,type,
sK238: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_299,type,
sK239: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_300,type,
sK240: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_301,type,
sK241: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_302,type,
sK242: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_303,type,
sK243: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_304,type,
sK244: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_305,type,
sK245: 'Int_nat_fun$' > $int ).
tff(func_def_306,type,
sK246: 'Int_nat_fun$' > $int ).
tff(func_def_307,type,
sK247: ( 'Nat$' * 'Nat_nat_fun$' * 'Clock$' * 'A_run$' ) > 'Nat$' ).
tff(func_def_308,type,
sK248: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_309,type,
sK249: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_310,type,
sK250: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_311,type,
sK251: 'Nat_nat_bool_fun_fun$' > 'Nat$' ).
tff(func_def_312,type,
sK252: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_313,type,
sK253: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_314,type,
sK254: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_315,type,
sK255: 'Nat_int_fun$' > 'Nat$' ).
tff(func_def_316,type,
sK256: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_317,type,
sK257: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_318,type,
sK258: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_319,type,
sK259: 'Int_int_fun$' > $int ).
tff(func_def_320,type,
sK260: 'Int_int_fun$' > $int ).
tff(func_def_321,type,
sK261: 'Nat_nat_fun$' > 'Nat$' ).
tff(func_def_322,type,
sK262: 'Nat_nat_fun$' > 'Nat$' ).
tff(pred_def_1,type,
'antimono$c': 'Int_int_fun$' > $o ).
tff(pred_def_2,type,
'member$': ( 'A_run$' * 'A_run_set$' ) > $o ).
tff(pred_def_3,type,
'member$a': ( 'Nat$' * 'Nat_set$' ) > $o ).
tff(pred_def_4,type,
'fst$': 'Bool_a_tag_const_prod$' > $o ).
tff(pred_def_5,type,
'contracting$': ( 'Nat_nat_fun$' * 'A_run$' * 'A_run$' * 'Nat_nat_fun$' ) > $o ).
tff(pred_def_6,type,
'antimono$': 'Nat_nat_fun$' > $o ).
tff(pred_def_7,type,
'fun_app$': ( 'A_run_bool_fun$' * 'A_run$' ) > $o ).
tff(pred_def_8,type,
'antimono$a': 'Nat_int_fun$' > $o ).
tff(pred_def_9,type,
'fun_app$i': ( 'Int_bool_fun$' * $int ) > $o ).
tff(pred_def_10,type,
'antimono$b': 'Int_nat_fun$' > $o ).
tff(pred_def_11,type,
'fun_app$f': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).
tff(pred_def_14,type,
sP0: ( 'Nat$' * 'Nat$' * 'A_run$' * 'Clock$' ) > $o ).
tff(pred_def_15,type,
sP1: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).
tff(pred_def_16,type,
sP2: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).
tff(pred_def_17,type,
sP3: ( 'Nat$' * 'Nat$' * 'Nat$' ) > $o ).
tff(pred_def_18,type,
sP4: ( $int * $int * $int ) > $o ).
tff(pred_def_19,type,
sP5: ( $int * $int * $int ) > $o ).
tff(pred_def_20,type,
sP6: ( $int * $int * $int ) > $o ).
tff(pred_def_21,type,
sP7: ( 'Nat$' * 'Nat$' * 'A_run$' * 'Clock$' ) > $o ).
tff(f15,conjecture,
$lesseq('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_2$'),'fun_app$c'('nat$',$sum('fun_app$d'('of_nat$','n$'),1)))),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_1$'),'n$'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture14) ).
tff(f16,negated_conjecture,
~ $lesseq('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_2$'),'fun_app$c'('nat$',$sum('fun_app$d'('of_nat$','n$'),1)))),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_1$'),'n$'))),
inference(negated_conjecture,[status(cth)],[f15]) ).
tff(f18,axiom,
$lesseq('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_2$'),'sn_0$')),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_1$'),'n_0$'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom16) ).
tff(f20,axiom,
'fun_app$d'('of_nat$','fun_app$e'('f$','n_0$')) = 'fun_app$d'('of_nat$','n$'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom18) ).
tff(f22,axiom,
'fun_app$d'('of_nat$','fun_app$e'('f$','sn_0$')) = $sum('fun_app$d'('of_nat$','n$'),1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom20) ).
tff(f38,axiom,
'fun_app$'('dilating$'('f$','sub$'),'r$'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom36) ).
tff(f97,axiom,
! [X0: 'Nat$'] : ( 'fun_app$d'('of_nat$',X0) != $sum('fun_app$d'('of_nat$',X0),1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom95) ).
tff(f196,axiom,
! [X4: 'Nat$',X1: 'A_run$',X2: 'A_run$',X0: 'Nat_nat_fun$',X3: 'Clock$'] :
( 'fun_app$'('dilating$'(X0,X1),X2)
=> ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X1,X3),X4)) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X2,X3),'fun_app$e'(X0,X4))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom194) ).
tff(f197,axiom,
! [X2: 'Nat$',X0: 'A_run$',X1: 'Clock$'] : ( 'fun_app$d'('of_nat$','fun_app$e'('tick_count$'(X0,X1),X2)) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X0,X1),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom195) ).
tff(f301,axiom,
! [X0: $int] : ~ $less(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom299) ).
tff(f366,axiom,
! [X0: 'Nat$',X2: 'Nat$',X1: 'Nat$'] :
( ( $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X1))
& $less('fun_app$d'('of_nat$',X1),'fun_app$d'('of_nat$',X2)) )
=> $less($sum('fun_app$d'('of_nat$',X0),1),'fun_app$d'('of_nat$',X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom364) ).
tff(f379,axiom,
! [X0: 'Nat$',X1: 'Nat$'] :
( ( $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X1))
& ( ( 'fun_app$d'('of_nat$',X1) = $sum('fun_app$d'('of_nat$',X0),1) )
=> $false )
& ! [X2: 'Nat$'] :
( ( ( 'fun_app$d'('of_nat$',X1) = $sum('fun_app$d'('of_nat$',X2),1) )
& $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X2)) )
=> $false ) )
=> $false ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom377) ).
tff(f480,axiom,
! [X1: $int,X0: $int] :
( $less($sum(X0,X1),X1)
<=> $less(X0,0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom478) ).
tff(f558,axiom,
! [X1: $int,X0: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom556) ).
tff(f606,axiom,
! [X0: $int] : $less(X0,$sum(X0,1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom604) ).
tff(f644,axiom,
! [X0: 'Nat$'] : ( 'fun_app$c'('nat$','fun_app$d'('of_nat$',X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom642) ).
tff(f714,plain,
~ $less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_1$'),'n_0$')),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_2$'),'sn_0$'))),
inference(theory_normalization,[],[f18]) ).
tff(f774,plain,
~ ~ $less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_1$'),'n$')),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_2$'),'fun_app$c'('nat$',$sum('fun_app$d'('of_nat$','n$'),1))))),
inference(theory_normalization,[],[f16]) ).
tff(f857,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| $less(X0,X1)
| ( X0 = X1 ) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f1080,plain,
! [X1: 'Nat$',X2: 'Nat$',X0: 'Nat$'] :
( ( $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X2))
& $less('fun_app$d'('of_nat$',X2),'fun_app$d'('of_nat$',X1)) )
=> $less($sum('fun_app$d'('of_nat$',X0),1),'fun_app$d'('of_nat$',X1)) ),
inference(rectify,[],[f366]) ).
tff(f1098,plain,
! [X0: 'Nat$',X1: 'Nat$'] :
~ ( $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X1))
& ( ( ~ 'fun_app$d'('of_nat$',X1) ) = $sum('fun_app$d'('of_nat$',X0),1) )
& ! [X2: 'Nat$'] :
~ ( ( 'fun_app$d'('of_nat$',X1) = $sum('fun_app$d'('of_nat$',X2),1) )
& $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X2)) ) ),
inference(true_and_false_elimination,[],[f379]) ).
tff(f1099,plain,
! [X0: 'Nat$',X1: 'Nat$'] :
~ ( ( 'fun_app$d'('of_nat$',X1) != $sum('fun_app$d'('of_nat$',X0),1) )
& $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X1))
& ! [X2: 'Nat$'] :
~ ( ( 'fun_app$d'('of_nat$',X1) = $sum('fun_app$d'('of_nat$',X2),1) )
& $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X2)) ) ),
inference(flattening,[],[f1098]) ).
tff(f1131,plain,
$less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_1$'),'n$')),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_2$'),'fun_app$c'('nat$',$sum('fun_app$d'('of_nat$','n$'),1))))),
inference(flattening,[],[f774]) ).
tff(f1277,plain,
! [X1: 'A_run$',X4: 'Clock$',X0: 'Nat$',X2: 'A_run$',X3: 'Nat_nat_fun$'] :
( 'fun_app$'('dilating$'(X3,X1),X2)
=> ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X2,X4),'fun_app$e'(X3,X0))) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X1,X4),X0)) ) ),
inference(rectify,[],[f196]) ).
tff(f1358,plain,
! [X1: 'Nat$',X0: 'Nat$'] :
( ? [X2: 'Nat$'] :
( ( 'fun_app$d'('of_nat$',X1) = $sum('fun_app$d'('of_nat$',X2),1) )
& $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X2)) )
| ( 'fun_app$d'('of_nat$',X1) = $sum('fun_app$d'('of_nat$',X0),1) )
| ~ $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X1)) ),
inference(ennf_transformation,[],[f1099]) ).
tff(f1638,plain,
! [X0: 'Nat$',X4: 'Clock$',X3: 'Nat_nat_fun$',X1: 'A_run$',X2: 'A_run$'] :
( ~ 'fun_app$'('dilating$'(X3,X1),X2)
| ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X2,X4),'fun_app$e'(X3,X0))) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X1,X4),X0)) ) ),
inference(ennf_transformation,[],[f1277]) ).
tff(f1873,plain,
! [X1: 'Nat$',X2: 'Nat$',X0: 'Nat$'] :
( $less($sum('fun_app$d'('of_nat$',X0),1),'fun_app$d'('of_nat$',X1))
| ~ $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X2))
| ~ $less('fun_app$d'('of_nat$',X2),'fun_app$d'('of_nat$',X1)) ),
inference(ennf_transformation,[],[f1080]) ).
tff(f1874,plain,
! [X0: 'Nat$',X1: 'Nat$',X2: 'Nat$'] :
( ~ $less('fun_app$d'('of_nat$',X2),'fun_app$d'('of_nat$',X1))
| $less($sum('fun_app$d'('of_nat$',X0),1),'fun_app$d'('of_nat$',X1))
| ~ $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X2)) ),
inference(flattening,[],[f1873]) ).
tff(f1892,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
inference(rectify,[],[f558]) ).
tff(f2033,plain,
! [X0: 'Nat$',X1: 'Nat$'] :
( ? [X2: 'Nat$'] :
( ( 'fun_app$d'('of_nat$',X0) = $sum('fun_app$d'('of_nat$',X2),1) )
& $less('fun_app$d'('of_nat$',X1),'fun_app$d'('of_nat$',X2)) )
| ( $sum('fun_app$d'('of_nat$',X1),1) = 'fun_app$d'('of_nat$',X0) )
| ~ $less('fun_app$d'('of_nat$',X1),'fun_app$d'('of_nat$',X0)) ),
inference(rectify,[],[f1358]) ).
tff(f2034,plain,
! [X0: 'Nat$',X1: 'Nat$'] :
( ( ( 'fun_app$d'('of_nat$',X0) = $sum('fun_app$d'('of_nat$',sK50(X0,X1)),1) )
& $less('fun_app$d'('of_nat$',X1),'fun_app$d'('of_nat$',sK50(X0,X1))) )
| ( $sum('fun_app$d'('of_nat$',X1),1) = 'fun_app$d'('of_nat$',X0) )
| ~ $less('fun_app$d'('of_nat$',X1),'fun_app$d'('of_nat$',X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(X2,sK50(X0,X1))],[f2033]) ).
tff(f2291,plain,
! [X0: 'Nat$',X1: 'Clock$',X2: 'Nat_nat_fun$',X3: 'A_run$',X4: 'A_run$'] :
( ~ 'fun_app$'('dilating$'(X2,X3),X4)
| ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X3,X1),X0)) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X4,X1),'fun_app$e'(X2,X0))) ) ),
inference(rectify,[],[f1638]) ).
tff(f2411,plain,
! [X0: 'Nat$',X1: 'A_run$',X2: 'Clock$'] : ( 'fun_app$d'('of_nat$','fun_app$e'('tick_count$'(X1,X2),X0)) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X1,X2),X0)) ),
inference(rectify,[],[f197]) ).
tff(f2626,plain,
! [X1: $int,X0: $int] :
( ( $less($sum(X0,X1),X1)
| ~ $less(X0,0) )
& ( $less(X0,0)
| ~ $less($sum(X0,X1),X1) ) ),
inference(nnf_transformation,[],[f480]) ).
tff(f2627,plain,
! [X0: $int,X1: $int] :
( ( $less($sum(X1,X0),X0)
| ~ $less(X1,0) )
& ( $less(X1,0)
| ~ $less($sum(X1,X0),X0) ) ),
inference(rectify,[],[f2626]) ).
tff(f2673,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
inference(cnf_transformation,[],[f1892]) ).
tff(f2694,plain,
$less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_1$'),'n$')),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_2$'),'fun_app$c'('nat$',$sum('fun_app$d'('of_nat$','n$'),1))))),
inference(cnf_transformation,[],[f1131]) ).
tff(f2732,plain,
! [X0: 'Nat$'] : ( 'fun_app$c'('nat$','fun_app$d'('of_nat$',X0)) = X0 ),
inference(cnf_transformation,[],[f644]) ).
tff(f2859,plain,
! [X0: 'Nat$',X1: 'Nat$'] :
( ( $sum('fun_app$d'('of_nat$',X1),1) = 'fun_app$d'('of_nat$',X0) )
| ~ $less('fun_app$d'('of_nat$',X1),'fun_app$d'('of_nat$',X0))
| ( 'fun_app$d'('of_nat$',X0) = $sum('fun_app$d'('of_nat$',sK50(X0,X1)),1) ) ),
inference(cnf_transformation,[],[f2034]) ).
tff(f3064,plain,
! [X0: 'Nat$'] : ( 'fun_app$d'('of_nat$',X0) != $sum('fun_app$d'('of_nat$',X0),1) ),
inference(cnf_transformation,[],[f97]) ).
tff(f3195,plain,
! [X2: 'Nat_nat_fun$',X3: 'A_run$',X0: 'Nat$',X1: 'Clock$',X4: 'A_run$'] :
( ~ 'fun_app$'('dilating$'(X2,X3),X4)
| ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X3,X1),X0)) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X4,X1),'fun_app$e'(X2,X0))) ) ),
inference(cnf_transformation,[],[f2291]) ).
tff(f3302,plain,
! [X2: 'Nat$',X0: 'Nat$',X1: 'Nat$'] :
( ~ $less('fun_app$d'('of_nat$',X2),'fun_app$d'('of_nat$',X1))
| $less($sum('fun_app$d'('of_nat$',X0),1),'fun_app$d'('of_nat$',X1))
| ~ $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X2)) ),
inference(cnf_transformation,[],[f1874]) ).
tff(f3329,plain,
'fun_app$'('dilating$'('f$','sub$'),'r$'),
inference(cnf_transformation,[],[f38]) ).
tff(f3360,plain,
$sum('fun_app$d'('of_nat$','n$'),1) = 'fun_app$d'('of_nat$','fun_app$e'('f$','sn_0$')),
inference(cnf_transformation,[],[f22]) ).
tff(f3368,plain,
! [X2: 'Clock$',X0: 'Nat$',X1: 'A_run$'] : ( 'fun_app$d'('of_nat$','fun_app$e'('tick_count$'(X1,X2),X0)) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'(X1,X2),X0)) ),
inference(cnf_transformation,[],[f2411]) ).
tff(f3434,plain,
~ $less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_1$'),'n_0$')),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_2$'),'sn_0$'))),
inference(cnf_transformation,[],[f714]) ).
tff(f3437,plain,
! [X0: $int] : $less(X0,$sum(X0,1)),
inference(cnf_transformation,[],[f606]) ).
tff(f3445,plain,
! [X0: $int] : ~ $less(X0,X0),
inference(cnf_transformation,[],[f301]) ).
tff(f3671,plain,
! [X0: $int,X1: $int] :
( ~ $less($sum(X1,X0),X0)
| $less(X1,0) ),
inference(cnf_transformation,[],[f2627]) ).
tff(f3702,plain,
'fun_app$d'('of_nat$','n$') = 'fun_app$d'('of_nat$','fun_app$e'('f$','n_0$')),
inference(cnf_transformation,[],[f20]) ).
tff(f3930,plain,
! [X0: 'Nat$',X1: 'Nat$'] :
( ( 'fun_app$d'('of_nat$',X0) = $sum('fun_app$d'('of_nat$',sK50(X0,X1)),1) )
| ( 'fun_app$d'('of_nat$',X0) = $sum(1,'fun_app$d'('of_nat$',X1)) )
| ~ $less('fun_app$d'('of_nat$',X1),'fun_app$d'('of_nat$',X0)) ),
inference(forward_demodulation,[],[f2859,f2673]) ).
tff(f3944,plain,
! [X2: 'Nat$',X0: 'Nat$',X1: 'Nat$'] :
( ~ $less('fun_app$d'('of_nat$',X2),'fun_app$d'('of_nat$',X1))
| $less($sum(1,'fun_app$d'('of_nat$',X0)),'fun_app$d'('of_nat$',X1))
| ~ $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$',X2)) ),
inference(forward_demodulation,[],[f3302,f2673]) ).
tff(f3946,plain,
! [X0: 'Nat$'] : ( 'fun_app$d'('of_nat$',X0) != $sum(1,'fun_app$d'('of_nat$',X0)) ),
inference(forward_demodulation,[],[f3064,f2673]) ).
tff(f3947,plain,
'fun_app$d'('of_nat$','fun_app$e'('f$','sn_0$')) = $sum(1,'fun_app$d'('of_nat$','n$')),
inference(forward_demodulation,[],[f3360,f2673]) ).
tff(f4005,plain,
$less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_1$'),'n$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$c'('nat$',$sum('fun_app$d'('of_nat$','n$'),1))))),
inference(forward_demodulation,[],[f2694,f3368]) ).
tff(f4026,plain,
! [X0: 'Nat$',X1: 'Nat$'] :
( ~ $less('fun_app$d'('of_nat$',X1),'fun_app$d'('of_nat$',X0))
| ( 'fun_app$d'('of_nat$',X0) = $sum(1,'fun_app$d'('of_nat$',X1)) )
| ( 'fun_app$d'('of_nat$',X0) = $sum(1,'fun_app$d'('of_nat$',sK50(X0,X1))) ) ),
inference(forward_demodulation,[],[f3930,f2673]) ).
tff(f4031,plain,
'fun_app$d'('of_nat$','fun_app$e'('f$','sn_0$')) = $sum(1,'fun_app$d'('of_nat$','fun_app$e'('f$','n_0$'))),
inference(forward_demodulation,[],[f3947,f3702]) ).
tff(f4050,plain,
$less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_1$'),'n$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$c'('nat$',$sum(1,'fun_app$d'('of_nat$','n$')))))),
inference(forward_demodulation,[],[f4005,f2673]) ).
tff(f4066,plain,
$less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_1$'),'n$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$c'('nat$',$sum(1,'fun_app$d'('of_nat$','fun_app$e'('f$','n_0$'))))))),
inference(forward_demodulation,[],[f4050,f3702]) ).
tff(f4073,plain,
$less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_1$'),'n$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$c'('nat$','fun_app$d'('of_nat$','fun_app$e'('f$','sn_0$')))))),
inference(forward_demodulation,[],[f4066,f4031]) ).
tff(f4077,plain,
$less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('r$','c_1$'),'n$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')))),
inference(forward_demodulation,[],[f4073,f2732]) ).
tff(f4078,plain,
$less('fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_1$'),'n$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')))),
inference(forward_demodulation,[],[f4077,f3368]) ).
tff(f4093,plain,
! [X0: $int] : $less(X0,$sum(1,X0)),
inference(superposition,[],[f3437,f2673]) ).
tff(f5063,plain,
'n$' = 'fun_app$c'('nat$','fun_app$d'('of_nat$','fun_app$e'('f$','n_0$'))),
inference(superposition,[],[f2732,f3702]) ).
tff(f5065,plain,
'n$' = 'fun_app$e'('f$','n_0$'),
inference(forward_demodulation,[],[f5063,f2732]) ).
tff(f12127,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_2$'),'sn_0$')) = 'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_1$'),'n_0$')) )
| $less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_2$'),'sn_0$')),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_1$'),'n_0$'))) ),
inference(resolution,[],[f3434,f857]) ).
tff(f12133,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_2$'),'sn_0$')) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$')) )
| $less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_2$'),'sn_0$')),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_1$'),'n_0$'))) ),
inference(forward_demodulation,[],[f12127,f3368]) ).
tff(f12138,plain,
( $less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_2$'),'sn_0$')),'fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_1$'),'n_0$')))
| ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$')) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) ) ),
inference(forward_demodulation,[],[f12133,f3368]) ).
tff(f12141,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$')) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) )
| $less('fun_app$d'('of_nat$','fun_app$e'('tick_count$'('sub$','c_2$'),'sn_0$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))) ),
inference(forward_demodulation,[],[f12138,f3368]) ).
tff(f12144,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$')) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) )
| $less('fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))) ),
inference(forward_demodulation,[],[f12141,f3368]) ).
tff(f12146,definition,
( spl263_94
<=> $less('fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))) ),
introduced(definition,[new_symbols(definition,[spl263_94])],[avatar_definition]) ).
tff(f12150,definition,
( spl263_95
<=> ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$')) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) ) ),
introduced(definition,[new_symbols(definition,[spl263_95])],[avatar_definition]) ).
tff(f12152,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$')) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) )
| ~ spl263_95 ),
inference(avatar_component_clause,[],[f12150]) ).
tff(f12154,plain,
( spl263_95
| spl263_94 ),
inference(avatar_split_clause,[],[f12144,f12146,f12150]) ).
tff(f25907,plain,
! [X0: 'Clock$',X1: 'Nat$'] : ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$',X0),'fun_app$e'('f$',X1))) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$',X0),X1)) ),
inference(resolution,[],[f3195,f3329]) ).
tff(f30646,plain,
! [X0: 'Nat$'] :
( ~ $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_1$'),'n$')))
| $less($sum(1,'fun_app$d'('of_nat$',X0)),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')))) ),
inference(resolution,[],[f3944,f4078]) ).
tff(f30711,plain,
! [X0: 'Nat$'] :
( ~ $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$'))))
| $less($sum(1,'fun_app$d'('of_nat$',X0)),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')))) ),
inference(forward_demodulation,[],[f30646,f5065]) ).
tff(f30716,plain,
! [X0: 'Nat$'] :
( $less($sum(1,'fun_app$d'('of_nat$',X0)),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$'))))
| ~ $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))) ),
inference(forward_demodulation,[],[f30711,f25907]) ).
tff(f30719,plain,
! [X0: 'Nat$'] :
( $less($sum(1,'fun_app$d'('of_nat$',X0)),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')))
| ~ $less('fun_app$d'('of_nat$',X0),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))) ),
inference(forward_demodulation,[],[f30716,f25907]) ).
tff(f36648,plain,
( ( $sum(1,'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_1$'),'n$'))) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$'))) )
| ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$'))) = $sum(1,'fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'n$')))) ) ),
inference(resolution,[],[f4026,f4078]) ).
tff(f36742,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) = $sum(1,'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_1$'),'n$'))) )
| ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$'))) = $sum(1,'fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'n$')))) ) ),
inference(forward_demodulation,[],[f36648,f25907]) ).
tff(f36764,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$'))) = $sum(1,'fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'n$')))) )
| ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) = $sum(1,'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$')))) ) ),
inference(forward_demodulation,[],[f36742,f5065]) ).
tff(f36775,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) = $sum(1,'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$')))) )
| ( $sum(1,'fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$'))))) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$'))) ) ),
inference(forward_demodulation,[],[f36764,f5065]) ).
tff(f36781,plain,
( ( $sum(1,'fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$'))))) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$'))) )
| ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) = $sum(1,'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))) ) ),
inference(forward_demodulation,[],[f36775,f25907]) ).
tff(f36784,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) = $sum(1,'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))) )
| ( $sum(1,'fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$'))))) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) ) ),
inference(forward_demodulation,[],[f36781,f25907]) ).
tff(f47046,definition,
( spl263_649
<=> ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) = $sum(1,'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))) ) ),
introduced(definition,[new_symbols(definition,[spl263_649])],[avatar_definition]) ).
tff(f47048,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) = $sum(1,'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))) )
| ~ spl263_649 ),
inference(avatar_component_clause,[],[f47046]) ).
tff(f47050,definition,
( spl263_650
<=> ( $sum(1,'fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$'))))) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) ) ),
introduced(definition,[new_symbols(definition,[spl263_650])],[avatar_definition]) ).
tff(f47052,plain,
( ( $sum(1,'fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$'))))) = 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) )
| ~ spl263_650 ),
inference(avatar_component_clause,[],[f47050]) ).
tff(f47053,plain,
( spl263_649
| spl263_650 ),
inference(avatar_split_clause,[],[f36784,f47050,f47046]) ).
tff(f48027,plain,
( $less(1,0)
| ~ $less('fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))) ),
inference(resolution,[],[f30719,f3671]) ).
tff(f48066,plain,
~ $less('fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$'))),
inference(evaluation,[],[f48027]) ).
tff(f48116,plain,
~ spl263_94,
inference(avatar_split_clause,[],[f48066,f12146]) ).
tff(f50437,plain,
( $less('fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')))
| ~ $less('fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$')))),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$')))
| ~ spl263_650 ),
inference(superposition,[],[f30719,f47052]) ).
tff(f50439,plain,
( $less('fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$')))),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')))
| ~ spl263_650 ),
inference(superposition,[],[f4093,f47052]) ).
tff(f50495,plain,
( ~ $less('fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$')))),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_1$'),'n_0$')))
| ~ spl263_650 ),
inference(forward_subsumption_resolution,[],[f50437,f3445]) ).
tff(f50513,plain,
( ~ $less('fun_app$d'('of_nat$',sK50('fun_app$e'('run_tick_count$'('r$','c_2$'),'fun_app$e'('f$','sn_0$')),'fun_app$e'('run_tick_count$'('r$','c_1$'),'fun_app$e'('f$','n_0$')))),'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')))
| ~ spl263_95
| ~ spl263_650 ),
inference(forward_demodulation,[],[f50495,f12152]) ).
tff(f50516,plain,
( $false
| ~ spl263_95
| ~ spl263_650 ),
inference(forward_subsumption_resolution,[],[f50513,f50439]) ).
tff(f50517,plain,
( ~ spl263_95
| ~ spl263_650 ),
inference(avatar_contradiction_clause,[],[f50516]) ).
tff(f50518,plain,
( ( 'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$')) = $sum(1,'fun_app$d'('of_nat$','fun_app$e'('run_tick_count$'('sub$','c_2$'),'sn_0$'))) )
| ~ spl263_95
| ~ spl263_649 ),
inference(forward_demodulation,[],[f47048,f12152]) ).
tff(f50519,plain,
( $false
| ~ spl263_95
| ~ spl263_649 ),
inference(forward_subsumption_resolution,[],[f50518,f3946]) ).
tff(f50520,plain,
( ~ spl263_95
| ~ spl263_649 ),
inference(avatar_contradiction_clause,[],[f50519]) ).
cnf(s95,plain,
( spl263_94
| spl263_95 ),
inference(sat_conversion,[],[f12154]) ).
cnf(s826,plain,
( spl263_649
| spl263_650 ),
inference(sat_conversion,[],[f47053]) ).
cnf(s854,plain,
~ spl263_94,
inference(sat_conversion,[],[f48116]) ).
cnf(s859,plain,
( ~ spl263_95
| ~ spl263_650 ),
inference(sat_conversion,[],[f50517]) ).
cnf(s860,plain,
( ~ spl263_95
| ~ spl263_649 ),
inference(sat_conversion,[],[f50520]) ).
cnf(s871,plain,
spl263_95,
inference(rat,[],[s95,s854]) ).
cnf(s872,plain,
~ spl263_649,
inference(rat,[],[s860,s871]) ).
cnf(s873,plain,
~ spl263_650,
inference(rat,[],[s859,s871]) ).
cnf(s875,plain,
$false,
inference(rat,[],[s826,s873,s872]) ).
tff(f50521,plain,
$false,
inference(avatar_sat_refutation,[],[s875]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP405_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 13:03:17 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.13/1.10 % (3552601)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.13/1.10 % (3552611)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3866591465:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.13/1.10 % (3552608)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1586810372:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.13/1.10 % (3552612)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4243725030:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.13/1.10 % (3552609)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1942944000:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.13/1.10 % (3552610)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3622596301:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.13/1.10 % (3552607)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1240511457:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.13/1.10 % (3552606)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1785578721:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.13/1.10 % (3552610)Instruction limit reached!
% 3.13/1.10 % (3552610)------------------------------
% 3.13/1.10 % (3552610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.13/1.10 % (3552610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/1.10 % (3552610)CaDiCaL version: 2.1.3
% 3.13/1.10 % (3552610)Termination reason: Instruction limit
% 3.13/1.10 % (3552610)Termination phase: Property scanning
% 3.13/1.10 % (3552610)Time elapsed: 0.003 s
% 3.13/1.10 % (3552610)Peak memory usage: 86 MB
% 3.13/1.10 % (3552610)Instructions burned: 4 (million)
% 3.13/1.10 % (3552609)Instruction limit reached!
% 3.13/1.10 % (3552609)------------------------------
% 3.13/1.10 % (3552609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.13/1.10 % (3552609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/1.10 % (3552609)CaDiCaL version: 2.1.3
% 3.13/1.10 % (3552609)Termination reason: Instruction limit
% 3.13/1.10 % (3552609)Termination phase: Property scanning
% 3.13/1.10 % (3552609)Time elapsed: 0.004 s
% 3.13/1.10 % (3552609)Peak memory usage: 86 MB
% 3.13/1.10 % (3552609)Instructions burned: 7 (million)
% 3.13/1.10 % (3552611)Instruction limit reached!
% 3.13/1.10 % (3552611)------------------------------
% 3.13/1.10 % (3552611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.13/1.10 % (3552611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/1.10 % (3552611)CaDiCaL version: 2.1.3
% 3.13/1.10 % (3552611)Termination reason: Instruction limit
% 3.13/1.10 % (3552611)Termination phase: Equality resolution with deletion
% 3.13/1.10 % (3552611)Time elapsed: 0.014 s
% 3.13/1.10 % (3552611)Peak memory usage: 88 MB
% 3.13/1.10 % (3552611)Instructions burned: 47 (million)
% 3.13/1.10 % (3552606)Instruction limit reached!
% 3.13/1.10 % (3552606)------------------------------
% 3.13/1.10 % (3552606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.13/1.10 % (3552606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/1.10 % (3552606)CaDiCaL version: 2.1.3
% 3.13/1.10 % (3552606)Termination reason: Instruction limit
% 3.13/1.10 % (3552606)Termination phase: Property scanning
% 3.13/1.10 % (3552606)Time elapsed: 0.006 s
% 3.13/1.10 % (3552606)Peak memory usage: 85 MB
% 3.13/1.10 % (3552606)Instructions burned: 14 (million)
% 3.13/1.10 % (3552612)Instruction limit reached!
% 3.13/1.10 % (3552612)------------------------------
% 3.13/1.10 % (3552612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.13/1.10 % (3552612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/1.10 % (3552612)CaDiCaL version: 2.1.3
% 3.13/1.10 % (3552612)Termination reason: Instruction limit
% 3.13/1.10 % (3552612)Termination phase: Preprocessing 3
% 3.13/1.10 % (3552612)Time elapsed: 0.019 s
% 3.13/1.10 % (3552612)Peak memory usage: 87 MB
% 3.13/1.10 % (3552612)Instructions burned: 34 (million)
% 3.13/1.10 % (3552620)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=299453783:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.13/1.10 % (3552620)Instruction limit reached!
% 3.77/1.23 % (3552620)------------------------------
% 3.77/1.23 % (3552620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.23 % (3552620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.23 % (3552620)CaDiCaL version: 2.1.3
% 3.77/1.23 % (3552620)Termination reason: Instruction limit
% 3.77/1.23 % (3552620)Termination phase: SInE selection
% 3.77/1.23 % (3552620)Time elapsed: 0.004 s
% 3.77/1.23 % (3552620)Peak memory usage: 86 MB
% 3.77/1.23 % (3552620)Instructions burned: 14 (million)
% 3.77/1.23 % (3552621)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=2355126894:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.77/1.23 % (3552622)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1610981300:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 3.77/1.23 % (3552623)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2554771151:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 3.77/1.23 % (3552608)Instruction limit reached!
% 3.77/1.23 % (3552608)------------------------------
% 3.77/1.23 % (3552608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.23 % (3552608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.23 % (3552608)CaDiCaL version: 2.1.3
% 3.77/1.23 % (3552608)Termination reason: Instruction limit
% 3.77/1.23 % (3552608)Termination phase: Saturation
% 3.77/1.23 % (3552608)Time elapsed: 0.150 s
% 3.77/1.23 % (3552608)Peak memory usage: 119 MB
% 3.77/1.23 % (3552608)Instructions burned: 202 (million)
% 3.77/1.23 % (3552622)Instruction limit reached!
% 3.77/1.23 % (3552622)------------------------------
% 3.77/1.23 % (3552622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.23 % (3552622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.23 % (3552622)CaDiCaL version: 2.1.3
% 3.77/1.23 % (3552622)Termination reason: Instruction limit
% 3.77/1.23 % (3552622)Termination phase: shuffling
% 3.77/1.23 % (3552622)Time elapsed: 0.009 s
% 3.77/1.23 % (3552622)Peak memory usage: 86 MB
% 3.77/1.23 % (3552622)Instructions burned: 17 (million)
% 3.77/1.23 % (3552623)Instruction limit reached!
% 3.77/1.23 % (3552623)------------------------------
% 3.77/1.23 % (3552623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.23 % (3552623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.23 % (3552623)CaDiCaL version: 2.1.3
% 3.77/1.23 % (3552623)Termination reason: Instruction limit
% 3.77/1.23 % (3552623)Termination phase: Preprocessing 1
% 3.77/1.23 % (3552623)Time elapsed: 0.013 s
% 3.77/1.23 % (3552623)Peak memory usage: 86 MB
% 3.77/1.23 % (3552623)Instructions burned: 25 (million)
% 3.77/1.23 % (3552624)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=710444160:i=27:canc=cautious:fsr=off:rtra=on_2998 on theBenchmark for (2998ds/27Mi)
% 3.77/1.23 % (3552621)Instruction limit reached!
% 3.77/1.23 % (3552621)------------------------------
% 3.77/1.23 % (3552621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.23 % (3552621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.23 % (3552621)CaDiCaL version: 2.1.3
% 3.77/1.23 % (3552621)Termination reason: Instruction limit
% 3.77/1.23 % (3552621)Termination phase: Preprocessing 3
% 3.77/1.23 % (3552621)Time elapsed: 0.016 s
% 3.77/1.23 % (3552621)Peak memory usage: 87 MB
% 3.77/1.23 % (3552621)Instructions burned: 29 (million)
% 3.77/1.23 % (3552624)Instruction limit reached!
% 3.77/1.23 % (3552624)------------------------------
% 3.77/1.23 % (3552624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.23 % (3552624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.23 % (3552624)CaDiCaL version: 2.1.3
% 3.77/1.23 % (3552624)Termination reason: Instruction limit
% 3.77/1.23 % (3552624)Termination phase: Preprocessing 2
% 3.77/1.23 % (3552624)Time elapsed: 0.015 s
% 3.77/1.23 % (3552624)Peak memory usage: 87 MB
% 3.77/1.23 % (3552624)Instructions burned: 27 (million)
% 3.77/1.23 % (3552626)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=613672439:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 3.77/1.23 % (3552607)Instruction limit reached!
% 3.77/1.23 % (3552607)------------------------------
% 4.63/1.35 % (3552607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3552607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3552607)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3552607)Termination reason: Instruction limit
% 4.63/1.35 % (3552607)Termination phase: Saturation
% 4.63/1.35 % (3552607)Time elapsed: 0.213 s
% 4.63/1.35 % (3552607)Peak memory usage: 119 MB
% 4.63/1.35 % (3552607)Instructions burned: 307 (million)
% 4.63/1.35 % (3552626)Instruction limit reached!
% 4.63/1.35 % (3552626)------------------------------
% 4.63/1.35 % (3552626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3552626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3552626)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3552626)Termination reason: Instruction limit
% 4.63/1.35 % (3552626)Termination phase: Saturation
% 4.63/1.35 % (3552626)Time elapsed: 0.024 s
% 4.63/1.35 % (3552626)Peak memory usage: 89 MB
% 4.63/1.35 % (3552626)Instructions burned: 90 (million)
% 4.63/1.35 % (3552630)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3690143319:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 4.63/1.35 % (3552633)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3003546608:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 4.63/1.35 % (3552630)Instruction limit reached!
% 4.63/1.35 % (3552630)------------------------------
% 4.63/1.35 % (3552630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3552630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3552630)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3552630)Termination reason: Instruction limit
% 4.63/1.35 % (3552630)Termination phase: shuffling
% 4.63/1.35 % (3552630)Time elapsed: 0.002 s
% 4.63/1.35 % (3552630)Peak memory usage: 85 MB
% 4.63/1.35 % (3552630)Instructions burned: 2 (million)
% 4.63/1.35 % (3552633)Instruction limit reached!
% 4.63/1.35 % (3552633)------------------------------
% 4.63/1.35 % (3552633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3552633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3552633)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3552633)Termination reason: Instruction limit
% 4.63/1.35 % (3552633)Termination phase: Property scanning
% 4.63/1.35 % (3552633)Time elapsed: 0.003 s
% 4.63/1.35 % (3552633)Peak memory usage: 85 MB
% 4.63/1.35 % (3552633)Instructions burned: 5 (million)
% 4.63/1.35 % (3552632)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1910552406:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi)
% 4.63/1.35 % (3552638)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1015501265:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 4.63/1.35 % (3552638)Instruction limit reached!
% 4.63/1.35 % (3552638)------------------------------
% 4.63/1.35 % (3552638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3552638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3552638)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3552638)Termination reason: Instruction limit
% 4.63/1.35 % (3552638)Termination phase: Property scanning
% 4.63/1.35 % (3552638)Time elapsed: 0.002 s
% 4.63/1.35 % (3552638)Peak memory usage: 85 MB
% 4.63/1.35 % (3552638)Instructions burned: 6 (million)
% 4.63/1.35 % (3552634)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3269315341:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 4.63/1.35 % (3552635)lrs+10_1_thi=all:si=on:fd=off:random_seed=3977777073:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 4.63/1.35 % (3552634)Instruction limit reached!
% 4.63/1.35 % (3552634)------------------------------
% 4.63/1.35 % (3552634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3552634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3552634)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3552634)Termination reason: Instruction limit
% 4.63/1.35 % (3552634)Termination phase: Property scanning
% 4.63/1.35 % (3552634)Time elapsed: 0.036 s
% 4.63/1.35 % (3552634)Peak memory usage: 88 MB
% 4.63/1.35 % (3552634)Instructions burned: 67 (million)
% 4.63/1.35 % (3552637)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=4079783075:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.81/1.50 % (3552637)Instruction limit reached!
% 5.81/1.50 % (3552637)------------------------------
% 5.81/1.50 % (3552637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.50 % (3552637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.50 % (3552637)CaDiCaL version: 2.1.3
% 5.81/1.50 % (3552637)Termination reason: Instruction limit
% 5.81/1.50 % (3552637)Termination phase: shuffling
% 5.81/1.50 % (3552637)Time elapsed: 0.005 s
% 5.81/1.50 % (3552637)Peak memory usage: 85 MB
% 5.81/1.50 % (3552637)Instructions burned: 9 (million)
% 5.81/1.50 % (3552635)Instruction limit reached!
% 5.81/1.50 % (3552635)------------------------------
% 5.81/1.50 % (3552635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.50 % (3552635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.50 % (3552635)CaDiCaL version: 2.1.3
% 5.81/1.50 % (3552635)Termination reason: Instruction limit
% 5.81/1.50 % (3552635)Termination phase: Preprocessing 3
% 5.81/1.50 % (3552635)Time elapsed: 0.028 s
% 5.81/1.50 % (3552635)Peak memory usage: 88 MB
% 5.81/1.50 % (3552635)Instructions burned: 54 (million)
% 5.81/1.50 % (3552642)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3821044916:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 5.81/1.50 % (3552646)dis+10_1_si=on:random_seed=1267067559:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 5.81/1.50 % (3552646)Instruction limit reached!
% 5.81/1.50 % (3552646)------------------------------
% 5.81/1.50 % (3552646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.50 % (3552646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.50 % (3552646)CaDiCaL version: 2.1.3
% 5.81/1.50 % (3552646)Termination reason: Instruction limit
% 5.81/1.50 % (3552646)Termination phase: Property scanning
% 5.81/1.50 % (3552646)Time elapsed: 0.003 s
% 5.81/1.50 % (3552646)Peak memory usage: 85 MB
% 5.81/1.50 % (3552646)Instructions burned: 11 (million)
% 5.81/1.50 % (3552641)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=229350408:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 5.81/1.50 % (3552641)Instruction limit reached!
% 5.81/1.50 % (3552641)------------------------------
% 5.81/1.50 % (3552641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.50 % (3552641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.50 % (3552641)CaDiCaL version: 2.1.3
% 5.81/1.50 % (3552641)Termination reason: Instruction limit
% 5.81/1.50 % (3552641)Termination phase: shuffling
% 5.81/1.50 % (3552641)Time elapsed: 0.002 s
% 5.81/1.50 % (3552641)Peak memory usage: 85 MB
% 5.81/1.50 % (3552641)Instructions burned: 2 (million)
% 5.81/1.50 % (3552632)Instruction limit reached!
% 5.81/1.50 % (3552632)------------------------------
% 5.81/1.50 % (3552632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.50 % (3552632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.50 % (3552632)CaDiCaL version: 2.1.3
% 5.81/1.50 % (3552632)Termination reason: Instruction limit
% 5.81/1.50 % (3552632)Termination phase: Saturation
% 5.81/1.50 % (3552632)Time elapsed: 0.128 s
% 5.81/1.50 % (3552632)Peak memory usage: 92 MB
% 5.81/1.50 % (3552632)Instructions burned: 182 (million)
% 5.81/1.50 % (3552648)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2262680768:i=26:canc=cautious:av=off:rtra=on_2995 on theBenchmark for (2995ds/26Mi)
% 5.81/1.50 % (3552650)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1590278298:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 5.81/1.50 % (3552648)Instruction limit reached!
% 5.81/1.50 % (3552648)------------------------------
% 5.81/1.50 % (3552648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.50 % (3552648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.50 % (3552648)CaDiCaL version: 2.1.3
% 5.81/1.50 % (3552648)Termination reason: Instruction limit
% 5.81/1.50 % (3552648)Termination phase: Preprocessing 2
% 5.81/1.50 % (3552648)Time elapsed: 0.015 s
% 6.64/1.76 % (3552648)Peak memory usage: 87 MB
% 6.64/1.76 % (3552648)Instructions burned: 27 (million)
% 6.64/1.76 % (3552655)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=528021535:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 6.64/1.76 % (3552655)Instruction limit reached!
% 6.64/1.76 % (3552655)------------------------------
% 6.64/1.76 % (3552655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.64/1.76 % (3552655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.64/1.76 % (3552655)CaDiCaL version: 2.1.3
% 6.64/1.76 % (3552655)Termination reason: Instruction limit
% 6.64/1.76 % (3552655)Termination phase: Property scanning
% 6.64/1.76 % (3552655)Time elapsed: 0.003 s
% 6.64/1.76 % (3552655)Peak memory usage: 85 MB
% 6.64/1.76 % (3552655)Instructions burned: 11 (million)
% 6.64/1.76 % (3552651)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3053875245:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 6.64/1.76 % (3552651)Instruction limit reached!
% 6.64/1.76 % (3552651)------------------------------
% 6.64/1.76 % (3552651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.64/1.76 % (3552651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.64/1.76 % (3552651)CaDiCaL version: 2.1.3
% 6.64/1.76 % (3552651)Termination reason: Instruction limit
% 6.64/1.76 % (3552651)Termination phase: shuffling
% 6.64/1.76 % (3552651)Time elapsed: 0.002 s
% 6.64/1.76 % (3552651)Peak memory usage: 85 MB
% 6.64/1.76 % (3552651)Instructions burned: 2 (million)
% 6.64/1.76 % (3552650)Instruction limit reached!
% 6.64/1.76 % (3552650)------------------------------
% 6.64/1.76 % (3552650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.64/1.76 % (3552650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.64/1.76 % (3552650)CaDiCaL version: 2.1.3
% 6.64/1.76 % (3552650)Termination reason: Instruction limit
% 6.64/1.76 % (3552650)Termination phase: Preprocessing 3
% 6.64/1.76 % (3552650)Time elapsed: 0.021 s
% 6.64/1.76 % (3552650)Peak memory usage: 88 MB
% 6.64/1.76 % (3552650)Instructions burned: 36 (million)
% 6.64/1.76 % (3552642)Instruction limit reached!
% 6.64/1.76 % (3552642)------------------------------
% 6.64/1.76 % (3552642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.64/1.76 % (3552642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.64/1.76 % (3552642)CaDiCaL version: 2.1.3
% 6.64/1.76 % (3552642)Termination reason: Instruction limit
% 6.64/1.76 % (3552642)Termination phase: Saturation
% 6.64/1.76 % (3552642)Time elapsed: 0.103 s
% 6.64/1.76 % (3552642)Peak memory usage: 118 MB
% 6.64/1.76 % (3552642)Instructions burned: 128 (million)
% 6.64/1.76 % (3552656)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=464510496:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi)
% 6.64/1.76 % (3552657)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1817642609:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/13Mi)
% 6.64/1.76 % (3552657)Instruction limit reached!
% 6.64/1.76 % (3552657)------------------------------
% 6.64/1.76 % (3552657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.64/1.76 % (3552657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.64/1.76 % (3552657)CaDiCaL version: 2.1.3
% 6.64/1.76 % (3552657)Termination reason: Instruction limit
% 6.64/1.76 % (3552657)Termination phase: Property scanning
% 6.64/1.76 % (3552657)Time elapsed: 0.007 s
% 6.64/1.76 % (3552657)Peak memory usage: 85 MB
% 6.64/1.76 % (3552657)Instructions burned: 15 (million)
% 6.64/1.76 % (3552663)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3697499509:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 6.64/1.76 % (3552663)Instruction limit reached!
% 6.64/1.76 % (3552663)------------------------------
% 6.64/1.76 % (3552663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.64/1.76 % (3552663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.64/1.76 % (3552663)CaDiCaL version: 2.1.3
% 6.64/1.76 % (3552663)Termination reason: Instruction limit
% 6.64/1.76 % (3552663)Termination phase: Property scanning
% 6.64/1.76 % (3552663)Time elapsed: 0.003 s
% 6.64/1.76 % (3552663)Peak memory usage: 86 MB
% 6.64/1.76 % (3552663)Instructions burned: 11 (million)
% 6.64/1.76 % (3552661)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3961657400:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 7.56/1.99 % (3552666)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=3849212195:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2993 on theBenchmark for (2993ds/294Mi)
% 7.56/1.99 % (3552664)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2050466954:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi)
% 7.56/1.99 % (3552665)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=4107439123:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi)
% 7.56/1.99 % (3552669)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=136815163:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2993 on theBenchmark for (2993ds/130Mi)
% 7.56/1.99 % (3552664)Instruction limit reached!
% 7.56/1.99 % (3552664)------------------------------
% 7.56/1.99 % (3552664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.56/1.99 % (3552664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.99 % (3552664)CaDiCaL version: 2.1.3
% 7.56/1.99 % (3552664)Termination reason: Instruction limit
% 7.56/1.99 % (3552664)Termination phase: Property scanning
% 7.56/1.99 % (3552664)Time elapsed: 0.037 s
% 7.56/1.99 % (3552664)Peak memory usage: 89 MB
% 7.56/1.99 % (3552664)Instructions burned: 73 (million)
% 7.56/1.99 % (3552671)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3471507926:i=131:rtra=on_2992 on theBenchmark for (2992ds/131Mi)
% 7.56/1.99 % (3552665)Instruction limit reached!
% 7.56/1.99 % (3552665)------------------------------
% 7.56/1.99 % (3552665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.56/1.99 % (3552665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.99 % (3552665)CaDiCaL version: 2.1.3
% 7.56/1.99 % (3552665)Termination reason: Instruction limit
% 7.56/1.99 % (3552665)Termination phase: Saturation
% 7.56/1.99 % (3552665)Time elapsed: 0.039 s
% 7.56/1.99 % (3552665)Peak memory usage: 90 MB
% 7.56/1.99 % (3552665)Instructions burned: 77 (million)
% 7.56/1.99 % (3552656)Instruction limit reached!
% 7.56/1.99 % (3552656)------------------------------
% 7.56/1.99 % (3552656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.56/1.99 % (3552656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.99 % (3552656)CaDiCaL version: 2.1.3
% 7.56/1.99 % (3552656)Termination reason: Instruction limit
% 7.56/1.99 % (3552656)Termination phase: Saturation
% 7.56/1.99 % (3552656)Time elapsed: 0.198 s
% 7.56/1.99 % (3552656)Peak memory usage: 94 MB
% 7.56/1.99 % (3552656)Instructions burned: 371 (million)
% 7.56/1.99 % (3552671)Instruction limit reached!
% 7.56/1.99 % (3552671)------------------------------
% 7.56/1.99 % (3552671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.56/1.99 % (3552671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.99 % (3552671)CaDiCaL version: 2.1.3
% 7.56/1.99 % (3552671)Termination reason: Instruction limit
% 7.56/1.99 % (3552671)Termination phase: Saturation
% 7.56/1.99 % (3552671)Time elapsed: 0.068 s
% 7.56/1.99 % (3552671)Peak memory usage: 135 MB
% 7.56/1.99 % (3552671)Instructions burned: 132 (million)
% 7.56/1.99 % (3552661)Instruction limit reached!
% 7.56/1.99 % (3552661)------------------------------
% 7.56/1.99 % (3552661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.56/1.99 % (3552661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.99 % (3552661)CaDiCaL version: 2.1.3
% 7.56/1.99 % (3552661)Termination reason: Instruction limit
% 7.56/1.99 % (3552661)Termination phase: Saturation
% 7.56/1.99 % (3552661)Time elapsed: 0.137 s
% 7.56/1.99 % (3552661)Peak memory usage: 119 MB
% 7.56/1.99 % (3552661)Instructions burned: 226 (million)
% 7.56/1.99 % (3552669)Instruction limit reached!
% 7.56/1.99 % (3552669)------------------------------
% 7.56/1.99 % (3552669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.56/1.99 % (3552669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.56/1.99 % (3552669)CaDiCaL version: 2.1.3
% 7.56/1.99 % (3552669)Termination reason: Instruction limit
% 10.92/2.29 % (3552669)Termination phase: Saturation
% 10.92/2.29 % (3552669)Time elapsed: 0.091 s
% 10.92/2.29 % (3552669)Peak memory usage: 114 MB
% 10.92/2.29 % (3552669)Instructions burned: 130 (million)
% 10.92/2.29 % (3552679)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=975454571:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi)
% 10.92/2.29 % (3552678)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1435354708:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi)
% 10.92/2.29 % (3552678)Instruction limit reached!
% 10.92/2.29 % (3552678)------------------------------
% 10.92/2.29 % (3552678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.92/2.29 % (3552678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.92/2.29 % (3552678)CaDiCaL version: 2.1.3
% 10.92/2.29 % (3552678)Termination reason: Instruction limit
% 10.92/2.29 % (3552678)Termination phase: Preprocessing 1
% 10.92/2.29 % (3552681)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=418934581:i=131:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 10.92/2.29 % (3552678)Time elapsed: 0.019 s
% 10.92/2.29 % (3552678)Peak memory usage: 86 MB
% 10.92/2.29 % (3552678)Instructions burned: 40 (million)
% 10.92/2.29 % (3552666)Instruction limit reached!
% 10.92/2.29 % (3552666)------------------------------
% 10.92/2.29 % (3552666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.92/2.29 % (3552666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.92/2.29 % (3552666)CaDiCaL version: 2.1.3
% 10.92/2.29 % (3552666)Termination reason: Instruction limit
% 10.92/2.29 % (3552666)Termination phase: Saturation
% 10.92/2.29 % (3552666)Time elapsed: 0.196 s
% 10.92/2.29 % (3552666)Peak memory usage: 93 MB
% 10.92/2.29 % (3552666)Instructions burned: 295 (million)
% 10.92/2.29 % (3552680)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1480647771:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/598Mi)
% 10.92/2.29 % (3552681)Instruction limit reached!
% 10.92/2.29 % (3552681)------------------------------
% 10.92/2.29 % (3552681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.92/2.29 % (3552681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.92/2.29 % (3552681)CaDiCaL version: 2.1.3
% 10.92/2.29 % (3552681)Termination reason: Instruction limit
% 10.92/2.29 % (3552681)Termination phase: Saturation
% 10.92/2.29 % (3552681)Time elapsed: 0.055 s
% 10.92/2.29 % (3552681)Peak memory usage: 119 MB
% 10.92/2.29 % (3552681)Instructions burned: 133 (million)
% 10.92/2.29 % (3552682)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=2902861663:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2991 on theBenchmark for (2991ds/259Mi)
% 10.92/2.29 % (3552683)dis+10_1_si=on:random_seed=3863473015:s2a=on:i=1000:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/1000Mi)
% 10.92/2.29 % (3552688)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=981473883:i=141:doe=on:rtra=on_2990 on theBenchmark for (2990ds/141Mi)
% 10.92/2.29 % (3552687)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=736117301:i=383:fsr=off:rtra=on:ev=force_2990 on theBenchmark for (2990ds/383Mi)
% 10.92/2.29 % (3552679)Instruction limit reached!
% 10.92/2.29 % (3552679)------------------------------
% 10.92/2.29 % (3552679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.92/2.29 % (3552679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.92/2.29 % (3552679)CaDiCaL version: 2.1.3
% 10.92/2.29 % (3552679)Termination reason: Instruction limit
% 10.92/2.29 % (3552679)Termination phase: Saturation
% 10.92/2.29 % (3552679)Time elapsed: 0.162 s
% 10.92/2.29 % (3552679)Peak memory usage: 93 MB
% 10.92/2.29 % (3552679)Instructions burned: 308 (million)
% 10.92/2.29 % (3552691)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2389418180:i=65:nm=16:rtra=on_2989 on theBenchmark for (2989ds/65Mi)
% 10.92/2.29 % (3552682)Instruction limit reached!
% 10.92/2.29 % (3552682)------------------------------
% 10.92/2.29 % (3552682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.92/2.29 % (3552682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.16/2.52 % (3552682)CaDiCaL version: 2.1.3
% 12.16/2.52 % (3552682)Termination reason: Instruction limit
% 12.16/2.52 % (3552682)Termination phase: Saturation
% 12.16/2.52 % (3552682)Time elapsed: 0.129 s
% 12.16/2.52 % (3552682)Peak memory usage: 118 MB
% 12.16/2.52 % (3552682)Instructions burned: 259 (million)
% 12.16/2.52 % (3552688)Instruction limit reached!
% 12.16/2.52 % (3552688)------------------------------
% 12.16/2.52 % (3552688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.16/2.52 % (3552688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.16/2.52 % (3552688)CaDiCaL version: 2.1.3
% 12.16/2.52 % (3552688)Termination reason: Instruction limit
% 12.16/2.52 % (3552688)Termination phase: Saturation
% 12.16/2.52 % (3552688)Time elapsed: 0.080 s
% 12.16/2.52 % (3552688)Peak memory usage: 91 MB
% 12.16/2.52 % (3552688)Instructions burned: 142 (million)
% 12.16/2.52 % (3552691)Instruction limit reached!
% 12.16/2.52 % (3552691)------------------------------
% 12.16/2.52 % (3552691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.16/2.52 % (3552691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.16/2.52 % (3552691)CaDiCaL version: 2.1.3
% 12.16/2.52 % (3552691)Termination reason: Instruction limit
% 12.16/2.52 % (3552691)Termination phase: Saturation
% 12.16/2.52 % (3552691)Time elapsed: 0.034 s
% 12.16/2.52 % (3552691)Peak memory usage: 90 MB
% 12.16/2.52 % (3552691)Instructions burned: 66 (million)
% 12.16/2.52 % (3552695)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4009297748:i=121:nm=16:rtra=on_2988 on theBenchmark for (2988ds/121Mi)
% 12.16/2.52 % (3552697)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=2763759495:s2a=on:i=128:s2at=5:ins=3:rtra=on_2988 on theBenchmark for (2988ds/128Mi)
% 12.16/2.52 % (3552698)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=3093955972:i=39:ins=3:rtra=on_2988 on theBenchmark for (2988ds/39Mi)
% 12.16/2.52 % (3552695)Instruction limit reached!
% 12.16/2.52 % (3552695)------------------------------
% 12.16/2.52 % (3552695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.16/2.52 % (3552695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.16/2.52 % (3552695)CaDiCaL version: 2.1.3
% 12.16/2.52 % (3552695)Termination reason: Instruction limit
% 12.16/2.52 % (3552695)Termination phase: Saturation
% 12.16/2.52 % (3552695)Time elapsed: 0.072 s
% 12.16/2.52 % (3552695)Peak memory usage: 91 MB
% 12.16/2.52 % (3552695)Instructions burned: 121 (million)
% 12.16/2.52 % (3552697)Instruction limit reached!
% 12.16/2.52 % (3552697)------------------------------
% 12.16/2.52 % (3552697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.16/2.52 % (3552697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.16/2.52 % (3552697)CaDiCaL version: 2.1.3
% 12.16/2.52 % (3552697)Termination reason: Instruction limit
% 12.16/2.52 % (3552697)Termination phase: Saturation
% 12.16/2.52 % (3552697)Time elapsed: 0.050 s
% 12.16/2.52 % (3552697)Peak memory usage: 107 MB
% 12.16/2.52 % (3552697)Instructions burned: 128 (million)
% 12.16/2.52 % (3552698)Instruction limit reached!
% 12.16/2.52 % (3552698)------------------------------
% 12.16/2.52 % (3552698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.16/2.52 % (3552698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.16/2.52 % (3552698)CaDiCaL version: 2.1.3
% 12.16/2.52 % (3552698)Termination reason: Instruction limit
% 12.16/2.52 % (3552698)Termination phase: Preprocessing 3
% 12.16/2.52 % (3552698)Time elapsed: 0.023 s
% 12.16/2.52 % (3552698)Peak memory usage: 88 MB
% 12.16/2.52 % (3552698)Instructions burned: 40 (million)
% 12.16/2.52 % (3552699)dis+1010_1_to=kbo:si=on:random_seed=611255105:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2988 on theBenchmark for (2988ds/175Mi)
% 12.16/2.52 % (3552687)Instruction limit reached!
% 12.16/2.52 % (3552687)------------------------------
% 12.16/2.52 % (3552687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.16/2.52 % (3552687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.16/2.52 % (3552687)CaDiCaL version: 2.1.3
% 12.16/2.52 % (3552687)Termination reason: Instruction limit
% 12.16/2.52 % (3552687)Termination phase: Saturation
% 12.16/2.52 % (3552687)Time elapsed: 0.236 s
% 12.16/2.52 % (3552687)Peak memory usage: 96 MB
% 12.16/2.52 % (3552687)Instructions burned: 385 (million)
% 12.16/2.52 % (3552703)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2840701359:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi)
% 14.62/2.81 % (3552680)Instruction limit reached!
% 14.62/2.81 % (3552680)------------------------------
% 14.62/2.81 % (3552680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.62/2.81 % (3552680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.62/2.81 % (3552680)CaDiCaL version: 2.1.3
% 14.62/2.81 % (3552680)Termination reason: Instruction limit
% 14.62/2.81 % (3552680)Termination phase: Saturation
% 14.62/2.81 % (3552680)Time elapsed: 0.400 s
% 14.62/2.81 % (3552680)Peak memory usage: 139 MB
% 14.62/2.81 % (3552680)Instructions burned: 598 (million)
% 14.62/2.81 % (3552699)Instruction limit reached!
% 14.62/2.81 % (3552699)------------------------------
% 14.62/2.81 % (3552699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.62/2.81 % (3552699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.62/2.81 % (3552699)CaDiCaL version: 2.1.3
% 14.62/2.81 % (3552699)Termination reason: Instruction limit
% 14.62/2.81 % (3552699)Termination phase: Saturation
% 14.62/2.81 % (3552699)Time elapsed: 0.112 s
% 14.62/2.81 % (3552699)Peak memory usage: 92 MB
% 14.62/2.81 % (3552699)Instructions burned: 175 (million)
% 14.62/2.81 % (3552704)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=528993347:s2a=on:i=483:doe=on:nm=32:rtra=on_2986 on theBenchmark for (2986ds/483Mi)
% 14.62/2.81 % (3552706)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2899507814:thitd=on:i=215:nm=0:rtra=on:ev=force_2986 on theBenchmark for (2986ds/215Mi)
% 14.62/2.81 % (3552707)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=4051603027:i=349:rtra=on_2986 on theBenchmark for (2986ds/349Mi)
% 14.62/2.81 % (3552703)Instruction limit reached!
% 14.62/2.81 % (3552703)------------------------------
% 14.62/2.81 % (3552703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.62/2.81 % (3552703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.62/2.81 % (3552703)CaDiCaL version: 2.1.3
% 14.62/2.81 % (3552703)Termination reason: Instruction limit
% 14.62/2.81 % (3552703)Termination phase: Saturation
% 14.62/2.81 % (3552703)Time elapsed: 0.137 s
% 14.62/2.81 % (3552703)Peak memory usage: 120 MB
% 14.62/2.81 % (3552703)Instructions burned: 331 (million)
% 14.62/2.81 % (3552709)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2006198873:st=2:i=295:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/295Mi)
% 14.62/2.81 % (3552710)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2615160268:i=328:kws=inv_frequency:nm=20:rtra=on_2985 on theBenchmark for (2985ds/328Mi)
% 14.62/2.81 % (3552706)Instruction limit reached!
% 14.62/2.81 % (3552706)------------------------------
% 14.62/2.81 % (3552706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.62/2.81 % (3552706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.62/2.81 % (3552706)CaDiCaL version: 2.1.3
% 14.62/2.81 % (3552706)Termination reason: Instruction limit
% 14.62/2.81 % (3552706)Termination phase: Saturation
% 14.62/2.81 % (3552706)Time elapsed: 0.159 s
% 14.62/2.81 % (3552706)Peak memory usage: 138 MB
% 14.62/2.81 % (3552706)Instructions burned: 216 (million)
% 14.62/2.81 % (3552715)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3289591890:i=281:gtgl=2:rtra=on:gtg=all_2984 on theBenchmark for (2984ds/281Mi)
% 14.62/2.81 % (3552683)Instruction limit reached!
% 14.62/2.81 % (3552683)------------------------------
% 14.62/2.81 % (3552683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.62/2.81 % (3552683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.62/2.81 % (3552683)CaDiCaL version: 2.1.3
% 14.62/2.81 % (3552683)Termination reason: Instruction limit
% 14.62/2.81 % (3552683)Termination phase: Saturation
% 14.62/2.81 % (3552683)Time elapsed: 0.600 s
% 14.62/2.81 % (3552683)Peak memory usage: 96 MB
% 14.62/2.81 % (3552683)Instructions burned: 1000 (million)
% 14.62/2.81 % (3552709)Instruction limit reached!
% 14.62/2.81 % (3552709)------------------------------
% 14.62/2.81 % (3552709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.62/2.81 % (3552709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/3.06 % (3552709)CaDiCaL version: 2.1.3
% 17.18/3.06 % (3552709)Termination reason: Instruction limit
% 17.18/3.06 % (3552709)Termination phase: Saturation
% 17.18/3.06 % (3552709)Time elapsed: 0.167 s
% 17.18/3.06 % (3552709)Peak memory usage: 92 MB
% 17.18/3.06 % (3552709)Instructions burned: 296 (million)
% 17.18/3.06 % (3552707)Instruction limit reached!
% 17.18/3.06 % (3552707)------------------------------
% 17.18/3.06 % (3552707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/3.06 % (3552707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/3.06 % (3552707)CaDiCaL version: 2.1.3
% 17.18/3.06 % (3552707)Termination reason: Instruction limit
% 17.18/3.06 % (3552707)Termination phase: Saturation
% 17.18/3.06 % (3552707)Time elapsed: 0.240 s
% 17.18/3.06 % (3552707)Peak memory usage: 120 MB
% 17.18/3.06 % (3552707)Instructions burned: 350 (million)
% 17.18/3.06 % (3552715)Instruction limit reached!
% 17.18/3.06 % (3552715)------------------------------
% 17.18/3.06 % (3552715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/3.06 % (3552715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/3.06 % (3552715)CaDiCaL version: 2.1.3
% 17.18/3.06 % (3552715)Termination reason: Instruction limit
% 17.18/3.06 % (3552715)Termination phase: Saturation
% 17.18/3.06 % (3552715)Time elapsed: 0.087 s
% 17.18/3.06 % (3552715)Peak memory usage: 118 MB
% 17.18/3.06 % (3552715)Instructions burned: 282 (million)
% 17.18/3.06 % (3552717)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1830344392:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/484Mi)
% 17.18/3.06 % (3552719)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3559355287:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2983 on theBenchmark for (2983ds/321Mi)
% 17.18/3.06 % (3552704)Instruction limit reached!
% 17.18/3.06 % (3552704)------------------------------
% 17.18/3.06 % (3552704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/3.06 % (3552704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/3.06 % (3552704)CaDiCaL version: 2.1.3
% 17.18/3.06 % (3552704)Termination reason: Instruction limit
% 17.18/3.06 % (3552704)Termination phase: Saturation
% 17.18/3.06 % (3552704)Time elapsed: 0.330 s
% 17.18/3.06 % (3552704)Peak memory usage: 137 MB
% 17.18/3.06 % (3552704)Instructions burned: 485 (million)
% 17.18/3.06 % (3552710)Instruction limit reached!
% 17.18/3.06 % (3552710)------------------------------
% 17.18/3.06 % (3552710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/3.06 % (3552710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/3.06 % (3552710)CaDiCaL version: 2.1.3
% 17.18/3.06 % (3552710)Termination reason: Instruction limit
% 17.18/3.06 % (3552710)Termination phase: Saturation
% 17.18/3.06 % (3552710)Time elapsed: 0.219 s
% 17.18/3.06 % (3552710)Peak memory usage: 119 MB
% 17.18/3.06 % (3552710)Instructions burned: 329 (million)
% 17.18/3.06 % (3552722)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=3068364262:avsq=on:i=276:avsqr=1,2:rtra=on_2982 on theBenchmark for (2982ds/276Mi)
% 17.18/3.06 % (3552720)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2850351021:i=416:rtra=on:gtg=position:ss=axioms_2983 on theBenchmark for (2983ds/416Mi)
% 17.18/3.06 % (3552721)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=4026427236:i=471:thf=on:kws=precedence:rtra=on_2982 on theBenchmark for (2982ds/471Mi)
% 17.18/3.06 % (3552725)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=578055573:i=375:kws=inv_arity_squared:rtra=on_2982 on theBenchmark for (2982ds/375Mi)
% 17.18/3.06 % (3552726)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=4265552437:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/387Mi)
% 17.18/3.06 % (3552722)Instruction limit reached!
% 17.18/3.06 % (3552722)------------------------------
% 17.18/3.06 % (3552722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/3.06 % (3552722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/3.06 % (3552722)CaDiCaL version: 2.1.3
% 17.18/3.06 % (3552722)Termination reason: Instruction limit
% 17.18/3.06 % (3552722)Termination phase: Saturation
% 17.18/3.06 % (3552722)Time elapsed: 0.118 s
% 18.96/3.41 % (3552722)Peak memory usage: 136 MB
% 18.96/3.41 % (3552722)Instructions burned: 276 (million)
% 18.96/3.41 % (3552719)Instruction limit reached!
% 18.96/3.41 % (3552719)------------------------------
% 18.96/3.41 % (3552719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.96/3.41 % (3552719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.96/3.41 % (3552719)CaDiCaL version: 2.1.3
% 18.96/3.41 % (3552719)Termination reason: Instruction limit
% 18.96/3.41 % (3552719)Termination phase: Saturation
% 18.96/3.41 % (3552719)Time elapsed: 0.168 s
% 18.96/3.41 % (3552719)Peak memory usage: 116 MB
% 18.96/3.41 % (3552719)Instructions burned: 322 (million)
% 18.96/3.41 % (3552717)Instruction limit reached!
% 18.96/3.41 % (3552717)------------------------------
% 18.96/3.41 % (3552717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.96/3.41 % (3552717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.96/3.41 % (3552717)CaDiCaL version: 2.1.3
% 18.96/3.41 % (3552717)Termination reason: Instruction limit
% 18.96/3.41 % (3552717)Termination phase: Saturation
% 18.96/3.41 % (3552717)Time elapsed: 0.225 s
% 18.96/3.41 % (3552717)Peak memory usage: 92 MB
% 18.96/3.41 % (3552717)Instructions burned: 485 (million)
% 18.96/3.41 % (3552720)Instruction limit reached!
% 18.96/3.41 % (3552720)------------------------------
% 18.96/3.41 % (3552720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.96/3.41 % (3552720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.96/3.41 % (3552720)CaDiCaL version: 2.1.3
% 18.96/3.41 % (3552720)Termination reason: Instruction limit
% 18.96/3.41 % (3552720)Termination phase: Saturation
% 18.96/3.41 % (3552720)Time elapsed: 0.221 s
% 18.96/3.41 % (3552720)Peak memory usage: 120 MB
% 18.96/3.41 % (3552720)Instructions burned: 416 (million)
% 18.96/3.41 % (3552732)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1773289329:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2980 on theBenchmark for (2980ds/513Mi)
% 18.96/3.41 % (3552733)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1056404587:i=334:rtra=on_2980 on theBenchmark for (2980ds/334Mi)
% 18.96/3.41 % (3552734)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2507809914:i=359:rtra=on:gtg=exists_top:ss=axioms_2980 on theBenchmark for (2980ds/359Mi)
% 18.96/3.41 % (3552721)Instruction limit reached!
% 18.96/3.41 % (3552721)------------------------------
% 18.96/3.41 % (3552721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.96/3.41 % (3552721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.96/3.41 % (3552721)CaDiCaL version: 2.1.3
% 18.96/3.41 % (3552721)Termination reason: Instruction limit
% 18.96/3.41 % (3552721)Termination phase: Saturation
% 18.96/3.41 % (3552721)Time elapsed: 0.309 s
% 18.96/3.41 % (3552721)Peak memory usage: 121 MB
% 18.96/3.41 % (3552721)Instructions burned: 471 (million)
% 18.96/3.41 % (3552725)Instruction limit reached!
% 18.96/3.41 % (3552725)------------------------------
% 18.96/3.41 % (3552725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.96/3.41 % (3552725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.96/3.41 % (3552725)CaDiCaL version: 2.1.3
% 18.96/3.41 % (3552725)Termination reason: Instruction limit
% 18.96/3.41 % (3552725)Termination phase: Saturation
% 18.96/3.41 % (3552725)Time elapsed: 0.255 s
% 18.96/3.41 % (3552725)Peak memory usage: 120 MB
% 18.96/3.41 % (3552725)Instructions burned: 376 (million)
% 18.96/3.41 % (3552736)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=372379098:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2979 on theBenchmark for (2979ds/341Mi)
% 18.96/3.41 % (3552726)Instruction limit reached!
% 18.96/3.41 % (3552726)------------------------------
% 18.96/3.41 % (3552726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.96/3.41 % (3552726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.96/3.41 % (3552726)CaDiCaL version: 2.1.3
% 18.96/3.41 % (3552726)Termination reason: Instruction limit
% 18.96/3.41 % (3552726)Termination phase: Saturation
% 18.96/3.41 % (3552726)Time elapsed: 0.273 s
% 18.96/3.41 % (3552726)Peak memory usage: 120 MB
% 18.96/3.41 % (3552726)Instructions burned: 387 (million)
% 18.96/3.41 % (3552732)Instruction limit reached!
% 18.96/3.41 % (3552732)------------------------------
% 18.96/3.41 % (3552732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.59/3.91 % (3552732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.91 % (3552732)CaDiCaL version: 2.1.3
% 21.59/3.91 % (3552732)Termination reason: Instruction limit
% 21.59/3.91 % (3552732)Termination phase: Saturation
% 21.59/3.91 % (3552732)Time elapsed: 0.166 s
% 21.59/3.91 % (3552732)Peak memory usage: 94 MB
% 21.59/3.91 % (3552732)Instructions burned: 515 (million)
% 21.59/3.91 % (3552739)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2834786774:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/261Mi)
% 21.59/3.91 % (3552734)Instruction limit reached!
% 21.59/3.91 % (3552734)------------------------------
% 21.59/3.91 % (3552734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.59/3.91 % (3552734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.91 % (3552734)CaDiCaL version: 2.1.3
% 21.59/3.91 % (3552734)Termination reason: Instruction limit
% 21.59/3.91 % (3552734)Termination phase: Saturation
% 21.59/3.91 % (3552734)Time elapsed: 0.194 s
% 21.59/3.91 % (3552734)Peak memory usage: 93 MB
% 21.59/3.91 % (3552734)Instructions burned: 359 (million)
% 21.59/3.91 % (3552740)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=2554787629:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2978 on theBenchmark for (2978ds/235Mi)
% 21.59/3.91 % (3552743)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3690070862:i=146:doe=on:rtra=on_2977 on theBenchmark for (2977ds/146Mi)
% 21.59/3.91 % (3552742)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3106784413:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2978 on theBenchmark for (2978ds/273Mi)
% 21.59/3.91 % (3552733)Instruction limit reached!
% 21.59/3.91 % (3552733)------------------------------
% 21.59/3.91 % (3552733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.59/3.91 % (3552733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.91 % (3552733)CaDiCaL version: 2.1.3
% 21.59/3.91 % (3552733)Termination reason: Instruction limit
% 21.59/3.91 % (3552733)Termination phase: Saturation
% 21.59/3.91 % (3552733)Time elapsed: 0.263 s
% 21.59/3.91 % (3552733)Peak memory usage: 137 MB
% 21.59/3.91 % (3552733)Instructions burned: 334 (million)
% 21.59/3.91 % (3552743)Instruction limit reached!
% 21.59/3.91 % (3552743)------------------------------
% 21.59/3.91 % (3552743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.59/3.91 % (3552743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.91 % (3552743)CaDiCaL version: 2.1.3
% 21.59/3.91 % (3552743)Termination reason: Instruction limit
% 21.59/3.91 % (3552743)Termination phase: Saturation
% 21.59/3.91 % (3552743)Time elapsed: 0.045 s
% 21.59/3.91 % (3552743)Peak memory usage: 91 MB
% 21.59/3.91 % (3552743)Instructions burned: 149 (million)
% 21.59/3.91 % (3552736)Instruction limit reached!
% 21.59/3.91 % (3552736)------------------------------
% 21.59/3.91 % (3552736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.59/3.91 % (3552736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.91 % (3552736)CaDiCaL version: 2.1.3
% 21.59/3.91 % (3552736)Termination reason: Instruction limit
% 21.59/3.91 % (3552736)Termination phase: Saturation
% 21.59/3.91 % (3552736)Time elapsed: 0.199 s
% 21.59/3.91 % (3552736)Peak memory usage: 121 MB
% 21.59/3.91 % (3552736)Instructions burned: 342 (million)
% 21.59/3.91 % (3552745)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2991767312:i=4428:doe=on:fsr=off:rtra=on_2977 on theBenchmark for (2977ds/4428Mi)
% 21.59/3.91 % (3552750)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=541075505:i=1052:rtra=on_2976 on theBenchmark for (2976ds/1052Mi)
% 21.59/3.91 % (3552739)Instruction limit reached!
% 21.59/3.91 % (3552739)------------------------------
% 21.59/3.91 % (3552739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.59/3.91 % (3552739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/3.91 % (3552739)CaDiCaL version: 2.1.3
% 21.59/3.91 % (3552739)Termination reason: Instruction limit
% 21.59/3.91 % (3552739)Termination phase: Saturation
% 21.59/3.91 % (3552739)Time elapsed: 0.192 s
% 21.59/3.91 % (3552739)Peak memory usage: 119 MB
% 25.68/4.33 % (3552739)Instructions burned: 263 (million)
% 25.68/4.33 % (3552740)Instruction limit reached!
% 25.68/4.33 % (3552740)------------------------------
% 25.68/4.33 % (3552740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.68/4.33 % (3552740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.68/4.33 % (3552740)CaDiCaL version: 2.1.3
% 25.68/4.33 % (3552740)Termination reason: Instruction limit
% 25.68/4.33 % (3552740)Termination phase: Saturation
% 25.68/4.33 % (3552740)Time elapsed: 0.168 s
% 25.68/4.33 % (3552740)Peak memory usage: 118 MB
% 25.68/4.33 % (3552740)Instructions burned: 235 (million)
% 25.68/4.33 % (3552749)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=2545078236:avsq=on:i=276:avsqr=1,2:rtra=on_2976 on theBenchmark for (2976ds/276Mi)
% 25.68/4.33 % (3552751)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3942044220:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2976 on theBenchmark for (2976ds/655Mi)
% 25.68/4.33 % (3552742)Instruction limit reached!
% 25.68/4.33 % (3552742)------------------------------
% 25.68/4.33 % (3552742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.68/4.33 % (3552742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.68/4.33 % (3552742)CaDiCaL version: 2.1.3
% 25.68/4.33 % (3552742)Termination reason: Instruction limit
% 25.68/4.33 % (3552742)Termination phase: Saturation
% 25.68/4.33 % (3552742)Time elapsed: 0.188 s
% 25.68/4.33 % (3552742)Peak memory usage: 93 MB
% 25.68/4.33 % (3552742)Instructions burned: 274 (million)
% 25.68/4.33 % (3552754)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=917517919:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/1054Mi)
% 25.68/4.33 % (3552755)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=4024849241:i=107:rtra=on_2975 on theBenchmark for (2975ds/107Mi)
% 25.68/4.33 % (3552758)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1799010646:s2a=on:i=450:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/450Mi)
% 25.68/4.33 % (3552755)Instruction limit reached!
% 25.68/4.33 % (3552755)------------------------------
% 25.68/4.33 % (3552755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.68/4.33 % (3552755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.68/4.33 % (3552755)CaDiCaL version: 2.1.3
% 25.68/4.33 % (3552755)Termination reason: Instruction limit
% 25.68/4.33 % (3552755)Termination phase: Saturation
% 25.68/4.33 % (3552755)Time elapsed: 0.056 s
% 25.68/4.33 % (3552755)Peak memory usage: 91 MB
% 25.68/4.33 % (3552755)Instructions burned: 107 (million)
% 25.68/4.33 % (3552749)Instruction limit reached!
% 25.68/4.33 % (3552749)------------------------------
% 25.68/4.33 % (3552749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.68/4.33 % (3552749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.68/4.33 % (3552749)CaDiCaL version: 2.1.3
% 25.68/4.33 % (3552749)Termination reason: Instruction limit
% 25.68/4.33 % (3552749)Termination phase: Saturation
% 25.68/4.33 % (3552749)Time elapsed: 0.210 s
% 25.68/4.33 % (3552749)Peak memory usage: 136 MB
% 25.68/4.33 % (3552749)Instructions burned: 278 (million)
% 25.68/4.33 % (3552762)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 25.68/4.33 % (3552762)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2923795379:i=1090:aac=none:nm=0:rtra=on:rawr=on_2973 on theBenchmark for (2973ds/1090Mi)
% 25.68/4.33 % (3552750)Instruction limit reached!
% 25.68/4.33 % (3552750)------------------------------
% 25.68/4.33 % (3552750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.68/4.33 % (3552750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.68/4.33 % (3552750)CaDiCaL version: 2.1.3
% 25.68/4.33 % (3552750)Termination reason: Instruction limit
% 25.68/4.33 % (3552750)Termination phase: Saturation
% 25.68/4.33 % (3552750)Time elapsed: 0.358 s
% 25.68/4.33 % (3552750)Peak memory usage: 98 MB
% 25.68/4.33 % (3552750)Instructions burned: 1056 (million)
% 25.68/4.33 % (3552763)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2943771174:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2973 on theBenchmark for (2973ds/130Mi)
% 28.48/4.80 % (3552765)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=4042349404:i=312:kws=inv_frequency:nm=20:rtra=on_2971 on theBenchmark for (2971ds/312Mi)
% 28.48/4.80 % (3552763)Instruction limit reached!
% 28.48/4.80 % (3552763)------------------------------
% 28.48/4.80 % (3552763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.48/4.80 % (3552763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.48/4.80 % (3552763)CaDiCaL version: 2.1.3
% 28.48/4.80 % (3552763)Termination reason: Instruction limit
% 28.48/4.80 % (3552763)Termination phase: Saturation
% 28.48/4.80 % (3552763)Time elapsed: 0.090 s
% 28.48/4.80 % (3552763)Peak memory usage: 114 MB
% 28.48/4.80 % (3552763)Instructions burned: 131 (million)
% 28.48/4.80 % (3552751)Instruction limit reached!
% 28.48/4.80 % (3552751)------------------------------
% 28.48/4.80 % (3552751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.48/4.80 % (3552751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.48/4.80 % (3552751)CaDiCaL version: 2.1.3
% 28.48/4.80 % (3552751)Termination reason: Instruction limit
% 28.48/4.80 % (3552751)Termination phase: Saturation
% 28.48/4.80 % (3552751)Time elapsed: 0.426 s
% 28.48/4.80 % (3552751)Peak memory usage: 96 MB
% 28.48/4.80 % (3552751)Instructions burned: 655 (million)
% 28.48/4.80 % (3552758)Instruction limit reached!
% 28.48/4.80 % (3552758)------------------------------
% 28.48/4.80 % (3552758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.48/4.80 % (3552758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.48/4.80 % (3552758)CaDiCaL version: 2.1.3
% 28.48/4.80 % (3552758)Termination reason: Instruction limit
% 28.48/4.80 % (3552758)Termination phase: Saturation
% 28.48/4.80 % (3552758)Time elapsed: 0.307 s
% 28.48/4.80 % (3552758)Peak memory usage: 137 MB
% 28.48/4.80 % (3552758)Instructions burned: 450 (million)
% 28.48/4.80 % (3552765)Instruction limit reached!
% 28.48/4.80 % (3552765)------------------------------
% 28.48/4.80 % (3552765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.48/4.80 % (3552765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.48/4.80 % (3552765)CaDiCaL version: 2.1.3
% 28.48/4.80 % (3552765)Termination reason: Instruction limit
% 28.48/4.80 % (3552765)Termination phase: Saturation
% 28.48/4.80 % (3552765)Time elapsed: 0.113 s
% 28.48/4.80 % (3552765)Peak memory usage: 119 MB
% 28.48/4.80 % (3552765)Instructions burned: 314 (million)
% 28.48/4.80 % (3552768)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3836669424:i=491:doe=on:rtra=on:gtg=position_2970 on theBenchmark for (2970ds/491Mi)
% 28.48/4.80 % (3552769)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=910209695:s2a=on:i=835:s2at=2:rtra=on_2970 on theBenchmark for (2970ds/835Mi)
% 28.48/4.80 % (3552770)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3274473389:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2970 on theBenchmark for (2970ds/307Mi)
% 28.48/4.80 % (3552771)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2174405626:i=776:doe=on:rtra=on_2969 on theBenchmark for (2969ds/776Mi)
% 28.48/4.80 % (3552754)Instruction limit reached!
% 28.48/4.80 % (3552754)------------------------------
% 28.48/4.80 % (3552754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.48/4.80 % (3552754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.48/4.80 % (3552754)CaDiCaL version: 2.1.3
% 28.48/4.80 % (3552754)Termination reason: Instruction limit
% 28.48/4.80 % (3552754)Termination phase: Saturation
% 28.48/4.80 % (3552754)Time elapsed: 0.650 s
% 28.48/4.80 % (3552754)Peak memory usage: 96 MB
% 28.48/4.80 % (3552754)Instructions burned: 1054 (million)
% 28.48/4.80 % (3552770)Instruction limit reached!
% 28.48/4.80 % (3552770)------------------------------
% 28.48/4.80 % (3552770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.48/4.80 % (3552770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.48/4.80 % (3552770)CaDiCaL version: 2.1.3
% 28.48/4.80 % (3552770)Termination reason: Instruction limit
% 28.48/4.80 % (3552770)Termination phase: Saturation
% 28.48/4.80 % (3552770)Time elapsed: 0.178 s
% 28.48/4.80 % (3552770)Peak memory usage: 93 MB
% 28.48/4.80 % (3552770)Instructions burned: 307 (million)
% 28.48/4.80 % (3552768)Instruction limit reached!
% 35.58/5.80 % (3552768)------------------------------
% 35.58/5.80 % (3552768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.80 % (3552768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.80 % (3552768)CaDiCaL version: 2.1.3
% 35.58/5.80 % (3552768)Termination reason: Instruction limit
% 35.58/5.80 % (3552768)Termination phase: Saturation
% 35.58/5.80 % (3552768)Time elapsed: 0.279 s
% 35.58/5.80 % (3552768)Peak memory usage: 95 MB
% 35.58/5.80 % (3552768)Instructions burned: 492 (million)
% 35.58/5.80 % (3552771)Instruction limit reached!
% 35.58/5.80 % (3552771)------------------------------
% 35.58/5.80 % (3552771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.80 % (3552771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.80 % (3552771)CaDiCaL version: 2.1.3
% 35.58/5.80 % (3552771)Termination reason: Instruction limit
% 35.58/5.80 % (3552771)Termination phase: Saturation
% 35.58/5.80 % (3552771)Time elapsed: 0.257 s
% 35.58/5.80 % (3552771)Peak memory usage: 124 MB
% 35.58/5.80 % (3552771)Instructions burned: 777 (million)
% 35.58/5.80 % (3552777)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=3261909757:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2967 on theBenchmark for (2967ds/784Mi)
% 35.58/5.80 % (3552776)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2598991478:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2967 on theBenchmark for (2967ds/646Mi)
% 35.58/5.80 % (3552778)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=2356645999:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2966 on theBenchmark for (2966ds/1131Mi)
% 35.58/5.80 % (3552779)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=3414332494:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2966 on theBenchmark for (2966ds/246Mi)
% 35.58/5.80 % (3552762)Instruction limit reached!
% 35.58/5.80 % (3552762)------------------------------
% 35.58/5.80 % (3552762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.80 % (3552762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.80 % (3552762)CaDiCaL version: 2.1.3
% 35.58/5.80 % (3552762)Termination reason: Instruction limit
% 35.58/5.80 % (3552762)Termination phase: Saturation
% 35.58/5.80 % (3552762)Time elapsed: 0.677 s
% 35.58/5.80 % (3552762)Peak memory usage: 122 MB
% 35.58/5.80 % (3552762)Instructions burned: 1091 (million)
% 35.58/5.80 % (3552779)Instruction limit reached!
% 35.58/5.80 % (3552779)------------------------------
% 35.58/5.80 % (3552779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.80 % (3552779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.80 % (3552779)CaDiCaL version: 2.1.3
% 35.58/5.80 % (3552779)Termination reason: Instruction limit
% 35.58/5.80 % (3552779)Termination phase: Saturation
% 35.58/5.80 % (3552779)Time elapsed: 0.093 s
% 35.58/5.80 % (3552779)Peak memory usage: 118 MB
% 35.58/5.80 % (3552779)Instructions burned: 248 (million)
% 35.58/5.80 % (3552769)Instruction limit reached!
% 35.58/5.80 % (3552769)------------------------------
% 35.58/5.80 % (3552769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.58/5.80 % (3552769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.58/5.80 % (3552769)CaDiCaL version: 2.1.3
% 35.58/5.80 % (3552769)Termination reason: Instruction limit
% 35.58/5.80 % (3552769)Termination phase: Saturation
% 35.58/5.80 % (3552769)Time elapsed: 0.528 s
% 35.58/5.80 % (3552769)Peak memory usage: 96 MB
% 35.58/5.80 % (3552769)Instructions burned: 835 (million)
% 35.58/5.80 % (3552784)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3019272192:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2965 on theBenchmark for (2965ds/775Mi)
% 35.58/5.80 % (3552785)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=130229717:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2964 on theBenchmark for (2964ds/273Mi)
% 35.58/5.80 % (3552786)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3958420329:i=102:nm=16:rtra=on_2964 on theBenchmark for (2964ds/102Mi)
% 35.58/5.80 % (3552785)Instruction limit reached!
% 50.20/7.73 % (3552785)------------------------------
% 50.20/7.73 % (3552785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.20/7.73 % (3552785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.73 % (3552785)CaDiCaL version: 2.1.3
% 50.20/7.73 % (3552785)Termination reason: Instruction limit
% 50.20/7.73 % (3552785)Termination phase: Saturation
% 50.20/7.73 % (3552785)Time elapsed: 0.097 s
% 50.20/7.73 % (3552785)Peak memory usage: 93 MB
% 50.20/7.73 % (3552785)Instructions burned: 275 (million)
% 50.20/7.73 % (3552786)Instruction limit reached!
% 50.20/7.73 % (3552786)------------------------------
% 50.20/7.73 % (3552786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.20/7.73 % (3552786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.73 % (3552786)CaDiCaL version: 2.1.3
% 50.20/7.73 % (3552786)Termination reason: Instruction limit
% 50.20/7.73 % (3552786)Termination phase: Saturation
% 50.20/7.73 % (3552786)Time elapsed: 0.054 s
% 50.20/7.73 % (3552786)Peak memory usage: 91 MB
% 50.20/7.73 % (3552786)Instructions burned: 102 (million)
% 50.20/7.73 % (3552776)Instruction limit reached!
% 50.20/7.73 % (3552776)------------------------------
% 50.20/7.73 % (3552776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.20/7.73 % (3552776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.73 % (3552776)CaDiCaL version: 2.1.3
% 50.20/7.73 % (3552776)Termination reason: Instruction limit
% 50.20/7.73 % (3552776)Termination phase: Saturation
% 50.20/7.73 % (3552776)Time elapsed: 0.418 s
% 50.20/7.73 % (3552776)Peak memory usage: 140 MB
% 50.20/7.73 % (3552776)Instructions burned: 646 (million)
% 50.20/7.73 % (3552790)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=551758595:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2962 on theBenchmark for (2962ds/1094Mi)
% 50.20/7.73 % (3552791)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2697144325:i=6400:doe=on:fsr=off:rtra=on_2962 on theBenchmark for (2962ds/6400Mi)
% 50.20/7.73 % (3552777)Instruction limit reached!
% 50.20/7.73 % (3552777)------------------------------
% 50.20/7.73 % (3552777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.20/7.73 % (3552777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.73 % (3552777)CaDiCaL version: 2.1.3
% 50.20/7.73 % (3552777)Termination reason: Instruction limit
% 50.20/7.73 % (3552777)Termination phase: Saturation
% 50.20/7.73 % (3552777)Time elapsed: 0.540 s
% 50.20/7.73 % (3552777)Peak memory usage: 123 MB
% 50.20/7.73 % (3552777)Instructions burned: 785 (million)
% 50.20/7.73 % (3552792)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=3237111307:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2962 on theBenchmark for (2962ds/868Mi)
% 50.20/7.73 % (3552796)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=3195685602:i=1846:canc=cautious:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/1846Mi)
% 50.20/7.73 % (3552784)Instruction limit reached!
% 50.20/7.73 % (3552784)------------------------------
% 50.20/7.73 % (3552784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.20/7.73 % (3552784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.73 % (3552784)CaDiCaL version: 2.1.3
% 50.20/7.73 % (3552784)Termination reason: Instruction limit
% 50.20/7.73 % (3552784)Termination phase: Saturation
% 50.20/7.73 % (3552784)Time elapsed: 0.487 s
% 50.20/7.73 % (3552784)Peak memory usage: 97 MB
% 50.20/7.73 % (3552784)Instructions burned: 776 (million)
% 50.20/7.73 % (3552790)Instruction limit reached!
% 50.20/7.73 % (3552790)------------------------------
% 50.20/7.73 % (3552790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.20/7.73 % (3552790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.73 % (3552790)CaDiCaL version: 2.1.3
% 50.20/7.73 % (3552790)Termination reason: Instruction limit
% 50.20/7.73 % (3552790)Termination phase: Saturation
% 50.20/7.73 % (3552790)Time elapsed: 0.337 s
% 50.20/7.73 % (3552790)Peak memory usage: 95 MB
% 50.20/7.73 % (3552790)Instructions burned: 1097 (million)
% 50.20/7.73 % (3552778)Instruction limit reached!
% 50.20/7.73 % (3552778)------------------------------
% 50.20/7.73 % (3552778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.20/7.73 % (3552778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552778)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552778)Termination reason: Instruction limit
% 53.86/8.29 % (3552778)Termination phase: Saturation
% 53.86/8.29 % (3552778)Time elapsed: 0.767 s
% 53.86/8.29 % (3552778)Peak memory usage: 131 MB
% 53.86/8.29 % (3552778)Instructions burned: 1131 (million)
% 53.86/8.29 % (3552798)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=349087065:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2959 on theBenchmark for (2959ds/36816Mi)
% 53.86/8.29 % (3552799)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1507264565:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi)
% 53.86/8.29 % (3552801)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=3635351822:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/863Mi)
% 53.86/8.29 % (3552799)Instruction limit reached!
% 53.86/8.29 % (3552799)------------------------------
% 53.86/8.29 % (3552799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552799)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552799)Termination reason: Instruction limit
% 53.86/8.29 % (3552799)Termination phase: Saturation
% 53.86/8.29 % (3552799)Time elapsed: 0.098 s
% 53.86/8.29 % (3552799)Peak memory usage: 93 MB
% 53.86/8.29 % (3552799)Instructions burned: 274 (million)
% 53.86/8.29 % (3552804)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1958003434:i=5811:kws=precedence:nm=0:rtra=on_2956 on theBenchmark for (2956ds/5811Mi)
% 53.86/8.29 % (3552792)Instruction limit reached!
% 53.86/8.29 % (3552792)------------------------------
% 53.86/8.29 % (3552792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552792)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552792)Termination reason: Instruction limit
% 53.86/8.29 % (3552792)Termination phase: Saturation
% 53.86/8.29 % (3552792)Time elapsed: 0.552 s
% 53.86/8.29 % (3552792)Peak memory usage: 122 MB
% 53.86/8.29 % (3552792)Instructions burned: 868 (million)
% 53.86/8.29 % (3552806)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=848236518:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2955 on theBenchmark for (2955ds/2216Mi)
% 53.86/8.29 % (3552801)Instruction limit reached!
% 53.86/8.29 % (3552801)------------------------------
% 53.86/8.29 % (3552801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552801)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552801)Termination reason: Instruction limit
% 53.86/8.29 % (3552801)Termination phase: Saturation
% 53.86/8.29 % (3552801)Time elapsed: 0.540 s
% 53.86/8.29 % (3552801)Peak memory usage: 122 MB
% 53.86/8.29 % (3552801)Instructions burned: 863 (million)
% 53.86/8.29 % (3552796)Instruction limit reached!
% 53.86/8.29 % (3552796)------------------------------
% 53.86/8.29 % (3552796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552796)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552796)Termination reason: Instruction limit
% 53.86/8.29 % (3552796)Termination phase: Saturation
% 53.86/8.29 % (3552796)Time elapsed: 0.960 s
% 53.86/8.29 % (3552796)Peak memory usage: 102 MB
% 53.86/8.29 % (3552796)Instructions burned: 1847 (million)
% 53.86/8.29 % (3552808)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2093164600:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2951 on theBenchmark for (2951ds/801Mi)
% 53.86/8.29 % (3552810)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=64991703:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2950 on theBenchmark for (2950ds/1026Mi)
% 53.86/8.29 % (3552745)Instruction limit reached!
% 53.86/8.29 % (3552745)------------------------------
% 53.86/8.29 % (3552745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552745)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552745)Termination reason: Instruction limit
% 53.86/8.29 % (3552745)Termination phase: Saturation
% 53.86/8.29 % (3552745)Time elapsed: 2.802 s
% 53.86/8.29 % (3552745)Peak memory usage: 121 MB
% 53.86/8.29 % (3552745)Instructions burned: 4428 (million)
% 53.86/8.29 % (3552812)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3549533057:i=3509:rtra=on_2947 on theBenchmark for (2947ds/3509Mi)
% 53.86/8.29 % (3552808)Instruction limit reached!
% 53.86/8.29 % (3552808)------------------------------
% 53.86/8.29 % (3552808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552808)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552808)Termination reason: Instruction limit
% 53.86/8.29 % (3552808)Termination phase: Saturation
% 53.86/8.29 % (3552808)Time elapsed: 0.542 s
% 53.86/8.29 % (3552808)Peak memory usage: 98 MB
% 53.86/8.29 % (3552808)Instructions burned: 802 (million)
% 53.86/8.29 % (3552814)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=738462074:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2944 on theBenchmark for (2944ds/2127Mi)
% 53.86/8.29 % (3552810)Instruction limit reached!
% 53.86/8.29 % (3552810)------------------------------
% 53.86/8.29 % (3552810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552810)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552810)Termination reason: Instruction limit
% 53.86/8.29 % (3552810)Termination phase: Saturation
% 53.86/8.29 % (3552810)Time elapsed: 0.620 s
% 53.86/8.29 % (3552810)Peak memory usage: 97 MB
% 53.86/8.29 % (3552810)Instructions burned: 1027 (million)
% 53.86/8.29 % (3552816)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1700363071:i=1959:rtra=on:fsd=on:proc=on_2942 on theBenchmark for (2942ds/1959Mi)
% 53.86/8.29 % (3552806)Instruction limit reached!
% 53.86/8.29 % (3552806)------------------------------
% 53.86/8.29 % (3552806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552806)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552806)Termination reason: Instruction limit
% 53.86/8.29 % (3552806)Termination phase: Saturation
% 53.86/8.29 % (3552806)Time elapsed: 1.368 s
% 53.86/8.29 % (3552806)Peak memory usage: 130 MB
% 53.86/8.29 % (3552806)Instructions burned: 2216 (million)
% 53.86/8.29 % (3552818)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1019440577:s2a=on:i=3553:nm=0:rtra=on_2940 on theBenchmark for (2940ds/3553Mi)
% 53.86/8.29 % (3552804)Instruction limit reached!
% 53.86/8.29 % (3552804)------------------------------
% 53.86/8.29 % (3552804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552804)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552804)Termination reason: Instruction limit
% 53.86/8.29 % (3552804)Termination phase: Saturation
% 53.86/8.29 % (3552804)Time elapsed: 1.728 s
% 53.86/8.29 % (3552804)Peak memory usage: 128 MB
% 53.86/8.29 % (3552804)Instructions burned: 5813 (million)
% 53.86/8.29 % (3552820)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3301985565:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2938 on theBenchmark for (2938ds/3201Mi)
% 53.86/8.29 % (3552814)Instruction limit reached!
% 53.86/8.29 % (3552814)------------------------------
% 53.86/8.29 % (3552814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552814)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552814)Termination reason: Instruction limit
% 53.86/8.29 % (3552814)Termination phase: Saturation
% 53.86/8.29 % (3552814)Time elapsed: 1.302 s
% 53.86/8.29 % (3552814)Peak memory usage: 105 MB
% 53.86/8.29 % (3552814)Instructions burned: 2127 (million)
% 53.86/8.29 % (3552822)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=2354746983:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2930 on theBenchmark for (2930ds/4093Mi)
% 53.86/8.29 % (3552816)Instruction limit reached!
% 53.86/8.29 % (3552816)------------------------------
% 53.86/8.29 % (3552816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552816)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552816)Termination reason: Instruction limit
% 53.86/8.29 % (3552816)Termination phase: Saturation
% 53.86/8.29 % (3552816)Time elapsed: 1.248 s
% 53.86/8.29 % (3552816)Peak memory usage: 129 MB
% 53.86/8.29 % (3552816)Instructions burned: 1959 (million)
% 53.86/8.29 % (3552820)Instruction limit reached!
% 53.86/8.29 % (3552820)------------------------------
% 53.86/8.29 % (3552820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.86/8.29 % (3552820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.86/8.29 % (3552820)CaDiCaL version: 2.1.3
% 53.86/8.29 % (3552820)Termination reason: Instruction limit
% 53.86/8.29 % (3552820)Termination phase: Saturation
% 53.86/8.29 % (3552820)Time elapsed: 0.896 s
% 53.86/8.29 % (3552820)Peak memory usage: 104 MB
% 53.86/8.29 % (3552820)Instructions burned: 3202 (million)
% 53.86/8.29 % (3552825)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=693672617:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2928 on theBenchmark for (2928ds/10544Mi)
% 53.86/8.29 % (3552824)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=1110607700:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2928 on theBenchmark for (2928ds/21173Mi)
% 53.86/8.29 % (3552812)First to succeed.
% 53.86/8.29 % (3552812)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3552601"
% 53.86/8.29 % (3552812)Refutation found. Thanks to Tanya!
% 53.86/8.29 % SZS status Theorem for theBenchmark
% 53.86/8.29 % SZS output start Proof for theBenchmark
% See solution above
% 54.66/8.48 % (3552812)------------------------------
% 54.66/8.48 % (3552812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.66/8.48 % (3552812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.66/8.48 % (3552812)CaDiCaL version: 2.1.3
% 54.66/8.48 % (3552812)Termination reason: Refutation
% 54.66/8.48 % (3552812)Time elapsed: 2.094 s
% 54.66/8.48 % (3552812)Peak memory usage: 111 MB
% 54.66/8.48 % (3552812)Instructions burned: 3227 (million)
% 54.66/8.48 % (3552812)------------------------------
% 54.66/8.48 % (3552812)------------------------------
% 54.66/8.48 % (3552601)Success in time 7.683 s
% 54.66/8.48 % Vampire exiting
%------------------------------------------------------------------------------