%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP317_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:39:21 AM UTC 2026
% Result : Theorem 1.31s 0.55s
% Output : Refutation 1.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 8
% Syntax : Number of formulae : 73 ( 12 unt; 0 typ; 2 def)
% Number of atoms : 205 ( 63 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 228 ( 96 ~; 111 |; 6 &)
% ( 8 <=>; 6 =>; 0 <=; 1 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number arithmetic : 44 ( 15 atm; 0 fun; 0 num; 29 var)
% Number of types : 24 ( 21 usr; 2 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 35 ( 31 usr; 3 prp; 0-4 aty)
% Number of functors : 207 ( 207 usr; 22 con; 0-3 aty)
% Number of variables : 97 ( 0 sgn 95 !; 2 ?; 97 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'Real_real_bool_fun_fun$': $tType ).
tff(type_def_6,type,
'Int_bool_fun$': $tType ).
tff(type_def_7,type,
'Real_a_fun$': $tType ).
tff(type_def_8,type,
'Bool_int_fun$': $tType ).
tff(type_def_9,type,
'Bool_real_fun$': $tType ).
tff(type_def_10,type,
'Int_real_fun$': $tType ).
tff(type_def_11,type,
'Nat_real_fun_bool_fun$': $tType ).
tff(type_def_12,type,
'Int_int_fun$': $tType ).
tff(type_def_13,type,
'Nat_nat_fun$': $tType ).
tff(type_def_14,type,
'Nat$': $tType ).
tff(type_def_15,type,
tlbool: $tType ).
tff(type_def_16,type,
'Real_real_fun$': $tType ).
tff(type_def_17,type,
'Nat_real_fun$': $tType ).
tff(type_def_18,type,
'Real_int_fun$': $tType ).
tff(type_def_19,type,
'Nat_real_fun_nat_nat_fun_fun$': $tType ).
tff(type_def_20,type,
'A$': $tType ).
tff(type_def_21,type,
'Nat_real_fun_nat_real_fun_fun$': $tType ).
tff(type_def_22,type,
'Int_int_bool_fun_fun$': $tType ).
tff(type_def_23,type,
'Nat_bool_fun$': $tType ).
tff(type_def_24,type,
'Real_bool_fun$': $tType ).
tff(type_def_25,type,
'Real_set$': $tType ).
tff(func_def_0,type,
'greatest$a': 'Int_bool_fun$' > $int ).
tff(func_def_1,type,
'n$a': 'Nat$' ).
tff(func_def_2,type,
'round$': 'Real_int_fun$' ).
tff(func_def_3,type,
'dbl_inc$': 'Int_int_fun$' ).
tff(func_def_4,type,
'a$a': $int ).
tff(func_def_5,type,
'eM_remainder_converges$': ( 'Nat$' * 'Real_a_fun$' ) > 'Int_bool_fun$' ).
tff(func_def_6,type,
'artanh$': 'Real_real_fun$' ).
tff(func_def_7,type,
'uub$': 'Int_int_bool_fun_fun$' ).
tff(func_def_8,type,
'dbl_inc$a': 'Real_real_fun$' ).
tff(func_def_9,type,
'arsinh$': 'Real_real_fun$' ).
tff(func_def_10,type,
'a$': $int ).
tff(func_def_11,type,
'n$': 'Nat$' ).
tff(func_def_12,type,
'fun_app$g': ( 'Real_real_fun$' * $real ) > $real ).
tff(func_def_13,type,
'fun_app$a': ( 'Real_real_bool_fun_fun$' * $real ) > 'Real_bool_fun$' ).
tff(func_def_14,type,
'of_nat$': 'Nat$' > $int ).
tff(func_def_15,type,
'g$': 'Real_a_fun$' ).
tff(func_def_16,type,
'f$': 'Real_a_fun$' ).
tff(func_def_17,type,
'times$': $int > 'Int_int_fun$' ).
tff(func_def_18,type,
tltrue: tlbool ).
tff(func_def_19,type,
'uu$': 'Real_set$' > 'Real_bool_fun$' ).
tff(func_def_20,type,
'of_int$': 'Int_real_fun$' ).
tff(func_def_21,type,
'of_int$a': 'Int_int_fun$' ).
tff(func_def_22,type,
'uud$': 'Int_int_bool_fun_fun$' ).
tff(func_def_23,type,
'greatest$': 'Real_bool_fun$' > $real ).
tff(func_def_24,type,
'uua$': 'Real_real_bool_fun_fun$' ).
tff(func_def_25,type,
'fun_app$n': ( 'Nat_real_fun$' * 'Nat$' ) > $real ).
tff(func_def_26,type,
'fun_app$l': ( 'Nat_real_fun_nat_real_fun_fun$' * 'Nat_real_fun$' ) > 'Nat_real_fun$' ).
tff(func_def_27,type,
'fun_app$h': ( 'Real_int_fun$' * $real ) > $int ).
tff(func_def_28,type,
'floor$': 'Real_int_fun$' ).
tff(func_def_29,type,
tlfalse: tlbool ).
tff(func_def_30,type,
'nat$': $int > 'Nat$' ).
tff(func_def_31,type,
'fun_app$c': ( 'Int_int_bool_fun_fun$' * $int ) > 'Int_bool_fun$' ).
tff(func_def_32,type,
'fun_app$p': ( 'Nat_real_fun_nat_nat_fun_fun$' * 'Nat_real_fun$' ) > 'Nat_nat_fun$' ).
tff(func_def_33,type,
'fun_app$e': ( 'Real_a_fun$' * $real ) > 'A$' ).
tff(func_def_34,type,
'arcosh$': 'Real_real_fun$' ).
tff(func_def_35,type,
'power_int$': $real > 'Int_real_fun$' ).
tff(func_def_36,type,
'fun_app$o': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_37,type,
'fun_app$f': ( 'Int_int_fun$' * $int ) > $int ).
tff(func_def_38,type,
'uuc$': 'Real_real_bool_fun_fun$' ).
tff(func_def_39,type,
'fun_app$j': ( 'Bool_int_fun$' * tlbool ) > $int ).
tff(func_def_40,type,
'fun_app$i': ( 'Bool_real_fun$' * tlbool ) > $real ).
tff(func_def_41,type,
'ceiling$': 'Real_int_fun$' ).
tff(func_def_42,type,
'collect$': 'Real_bool_fun$' > 'Real_set$' ).
tff(func_def_43,type,
'fun_app$d': ( 'Int_real_fun$' * $int ) > $real ).
tff(func_def_52,type,
sK0: ( $int * 'Real_a_fun$' * 'Real_a_fun$' ) > $real ).
tff(func_def_53,type,
sK1: $real > $int ).
tff(func_def_54,type,
sK2: 'Real_set$' > $real ).
tff(func_def_55,type,
sK3: ( 'Real_set$' * $real ) > $real ).
tff(func_def_56,type,
sK4: ( 'Real_set$' * $real ) > $real ).
tff(func_def_57,type,
sK9: 'Real_real_fun$' > $real ).
tff(func_def_58,type,
sK10: 'Real_real_fun$' > $real ).
tff(func_def_59,type,
sK11: 'Real_int_fun$' > $real ).
tff(func_def_60,type,
sK12: 'Real_int_fun$' > $real ).
tff(func_def_61,type,
sK13: 'Int_real_fun$' > $int ).
tff(func_def_62,type,
sK14: 'Int_real_fun$' > $int ).
tff(func_def_63,type,
sK15: 'Int_int_fun$' > $int ).
tff(func_def_64,type,
sK16: 'Int_int_fun$' > $int ).
tff(func_def_65,type,
sK17: 'Real_real_fun$' > $real ).
tff(func_def_66,type,
sK18: 'Real_real_fun$' > $real ).
tff(func_def_67,type,
sK19: 'Real_int_fun$' > $real ).
tff(func_def_68,type,
sK20: 'Real_int_fun$' > $real ).
tff(func_def_69,type,
sK21: 'Int_real_fun$' > $int ).
tff(func_def_70,type,
sK22: 'Int_real_fun$' > $int ).
tff(func_def_71,type,
sK23: 'Int_int_fun$' > $int ).
tff(func_def_72,type,
sK24: 'Int_int_fun$' > $int ).
tff(func_def_73,type,
sK25: 'Real_real_fun$' > $real ).
tff(func_def_74,type,
sK26: 'Real_real_fun$' > $real ).
tff(func_def_75,type,
sK27: 'Real_int_fun$' > $real ).
tff(func_def_76,type,
sK28: 'Real_int_fun$' > $real ).
tff(func_def_77,type,
sK29: 'Int_real_fun$' > $int ).
tff(func_def_78,type,
sK30: 'Int_real_fun$' > $int ).
tff(func_def_79,type,
sK31: 'Int_int_fun$' > $int ).
tff(func_def_80,type,
sK32: 'Int_int_fun$' > $int ).
tff(func_def_81,type,
sK33: 'Real_real_fun$' > $real ).
tff(func_def_82,type,
sK34: 'Real_real_fun$' > $real ).
tff(func_def_83,type,
sK35: 'Int_real_fun$' > $int ).
tff(func_def_84,type,
sK36: 'Int_real_fun$' > $int ).
tff(func_def_85,type,
sK37: 'Real_int_fun$' > $real ).
tff(func_def_86,type,
sK38: 'Real_int_fun$' > $real ).
tff(func_def_87,type,
sK39: 'Int_int_fun$' > $int ).
tff(func_def_88,type,
sK40: 'Int_int_fun$' > $int ).
tff(func_def_89,type,
sK41: 'Real_real_bool_fun_fun$' > $real ).
tff(func_def_90,type,
sK42: 'Real_real_bool_fun_fun$' > $real ).
tff(func_def_91,type,
sK43: 'Real_real_bool_fun_fun$' > $real ).
tff(func_def_92,type,
sK44: 'Real_real_bool_fun_fun$' > $real ).
tff(func_def_93,type,
sK45: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_94,type,
sK46: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_95,type,
sK47: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_96,type,
sK48: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_97,type,
sK63: ( 'Real_bool_fun$' * $real ) > $real ).
tff(func_def_98,type,
sK64: ( 'Int_bool_fun$' * $int ) > $int ).
tff(func_def_99,type,
sK65: ( 'Real_bool_fun$' * 'Real_bool_fun$' ) > $real ).
tff(func_def_100,type,
sK66: ( 'Real_bool_fun$' * $real ) > $real ).
tff(func_def_101,type,
sK68: ( 'Int_bool_fun$' * 'Int_bool_fun$' ) > $int ).
tff(func_def_102,type,
sK69: ( 'Int_bool_fun$' * $int ) > $int ).
tff(func_def_103,type,
sK71: $real > $int ).
tff(func_def_104,type,
sK72: $real > $int ).
tff(func_def_105,type,
sK73: 'Real_real_fun$' > $real ).
tff(func_def_106,type,
sK74: 'Real_real_fun$' > $real ).
tff(func_def_107,type,
sK75: 'Real_int_fun$' > $real ).
tff(func_def_108,type,
sK76: 'Real_int_fun$' > $real ).
tff(func_def_109,type,
sK77: 'Int_real_fun$' > $int ).
tff(func_def_110,type,
sK78: 'Int_real_fun$' > $int ).
tff(func_def_111,type,
sK79: 'Int_int_fun$' > $int ).
tff(func_def_112,type,
sK80: 'Int_int_fun$' > $int ).
tff(func_def_113,type,
sK81: 'Real_real_fun$' > $real ).
tff(func_def_114,type,
sK82: 'Real_real_fun$' > $real ).
tff(func_def_115,type,
sK83: 'Real_int_fun$' > $real ).
tff(func_def_116,type,
sK84: 'Real_int_fun$' > $real ).
tff(func_def_117,type,
sK85: 'Int_real_fun$' > $int ).
tff(func_def_118,type,
sK86: 'Int_real_fun$' > $int ).
tff(func_def_119,type,
sK87: 'Int_int_fun$' > $int ).
tff(func_def_120,type,
sK88: 'Int_int_fun$' > $int ).
tff(func_def_121,type,
sK93: $real > $real ).
tff(func_def_122,type,
sK94: $int > $int ).
tff(func_def_123,type,
sK95: $real > $real ).
tff(func_def_124,type,
sK96: $int > $int ).
tff(func_def_125,type,
sK97: ( $real * $real ) > $real ).
tff(func_def_126,type,
sK104: 'Real_real_bool_fun_fun$' > $real ).
tff(func_def_127,type,
sK105: 'Real_real_bool_fun_fun$' > $real ).
tff(func_def_128,type,
sK106: 'Real_real_bool_fun_fun$' > $real ).
tff(func_def_129,type,
sK107: 'Real_real_bool_fun_fun$' > $real ).
tff(func_def_130,type,
sK108: 'Real_real_bool_fun_fun$' > $real ).
tff(func_def_131,type,
sK109: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_132,type,
sK110: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_133,type,
sK111: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_134,type,
sK112: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_135,type,
sK113: 'Int_int_bool_fun_fun$' > $int ).
tff(func_def_136,type,
sK118: 'Real_real_fun$' > $real ).
tff(func_def_137,type,
sK119: 'Real_real_fun$' > $real ).
tff(func_def_138,type,
sK120: 'Real_int_fun$' > $real ).
tff(func_def_139,type,
sK121: 'Real_int_fun$' > $real ).
tff(func_def_140,type,
sK122: 'Int_real_fun$' > $int ).
tff(func_def_141,type,
sK123: 'Int_real_fun$' > $int ).
tff(func_def_142,type,
sK124: 'Int_int_fun$' > $int ).
tff(func_def_143,type,
sK125: 'Int_int_fun$' > $int ).
tff(func_def_144,type,
sK126: 'Real_real_fun$' > $real ).
tff(func_def_145,type,
sK127: 'Real_real_fun$' > $real ).
tff(func_def_146,type,
sK128: 'Real_int_fun$' > $real ).
tff(func_def_147,type,
sK129: 'Real_int_fun$' > $real ).
tff(func_def_148,type,
sK130: 'Int_real_fun$' > $int ).
tff(func_def_149,type,
sK131: 'Int_real_fun$' > $int ).
tff(func_def_150,type,
sK132: 'Int_int_fun$' > $int ).
tff(func_def_151,type,
sK133: 'Int_int_fun$' > $int ).
tff(func_def_152,type,
sK134: 'Real_real_fun$' > $real ).
tff(func_def_153,type,
sK135: 'Real_real_fun$' > $real ).
tff(func_def_154,type,
sK136: 'Int_real_fun$' > $int ).
tff(func_def_155,type,
sK137: 'Int_real_fun$' > $int ).
tff(func_def_156,type,
sK138: 'Real_int_fun$' > $real ).
tff(func_def_157,type,
sK139: 'Real_int_fun$' > $real ).
tff(func_def_158,type,
sK140: 'Int_int_fun$' > $int ).
tff(func_def_159,type,
sK141: 'Int_int_fun$' > $int ).
tff(func_def_160,type,
sK142: 'Real_real_fun$' > $real ).
tff(func_def_161,type,
sK143: 'Real_real_fun$' > $real ).
tff(func_def_162,type,
sK144: 'Real_int_fun$' > $real ).
tff(func_def_163,type,
sK145: 'Real_int_fun$' > $real ).
tff(func_def_164,type,
sK146: 'Int_real_fun$' > $int ).
tff(func_def_165,type,
sK147: 'Int_real_fun$' > $int ).
tff(func_def_166,type,
sK148: 'Int_int_fun$' > $int ).
tff(func_def_167,type,
sK149: 'Int_int_fun$' > $int ).
tff(func_def_168,type,
sK152: ( $real * $real ) > $real ).
tff(func_def_169,type,
sK153: 'Real_real_fun$' > $real ).
tff(func_def_170,type,
sK154: 'Real_real_fun$' > $real ).
tff(func_def_171,type,
sK155: 'Int_real_fun$' > $int ).
tff(func_def_172,type,
sK156: 'Int_real_fun$' > $int ).
tff(func_def_173,type,
sK157: 'Real_int_fun$' > $real ).
tff(func_def_174,type,
sK158: 'Real_int_fun$' > $real ).
tff(func_def_175,type,
sK159: 'Int_int_fun$' > $int ).
tff(func_def_176,type,
sK160: 'Int_int_fun$' > $int ).
tff(func_def_177,type,
sK161: 'Real_real_fun$' > $real ).
tff(func_def_178,type,
sK162: 'Real_real_fun$' > $real ).
tff(func_def_179,type,
sK163: 'Real_int_fun$' > $real ).
tff(func_def_180,type,
sK164: 'Real_int_fun$' > $real ).
tff(func_def_181,type,
sK165: 'Int_real_fun$' > $int ).
tff(func_def_182,type,
sK166: 'Int_real_fun$' > $int ).
tff(func_def_183,type,
sK167: 'Int_int_fun$' > $int ).
tff(func_def_184,type,
sK168: 'Int_int_fun$' > $int ).
tff(func_def_185,type,
sK169: 'Real_real_fun$' > $real ).
tff(func_def_186,type,
sK170: 'Real_real_fun$' > $real ).
tff(func_def_187,type,
sK171: 'Real_int_fun$' > $real ).
tff(func_def_188,type,
sK172: 'Real_int_fun$' > $real ).
tff(func_def_189,type,
sK173: 'Int_real_fun$' > $int ).
tff(func_def_190,type,
sK174: 'Int_real_fun$' > $int ).
tff(func_def_191,type,
sK175: 'Int_int_fun$' > $int ).
tff(func_def_192,type,
sK176: 'Int_int_fun$' > $int ).
tff(func_def_193,type,
sK177: 'Real_real_fun$' > $real ).
tff(func_def_194,type,
sK178: 'Real_real_fun$' > $real ).
tff(func_def_195,type,
sK179: 'Int_real_fun$' > $int ).
tff(func_def_196,type,
sK180: 'Int_real_fun$' > $int ).
tff(func_def_197,type,
sK181: 'Real_int_fun$' > $real ).
tff(func_def_198,type,
sK182: 'Real_int_fun$' > $real ).
tff(func_def_199,type,
sK183: 'Int_int_fun$' > $int ).
tff(func_def_200,type,
sK184: 'Int_int_fun$' > $int ).
tff(func_def_201,type,
sK185: ( $real * $real * $real ) > $real ).
tff(func_def_202,type,
sK186: ( $real * $real * $real ) > $real ).
tff(func_def_203,type,
sK187: ( $real * $real ) > $real ).
tff(func_def_204,type,
sK188: ( $real * $real ) > $real ).
tff(func_def_205,type,
sK189: $real > $int ).
tff(func_def_206,type,
sK190: $real > $int ).
tff(func_def_207,type,
sK191: ( $int * 'Int_bool_fun$' ) > $int ).
tff(func_def_208,type,
sK192: ( $int * 'Int_bool_fun$' ) > $int ).
tff(func_def_209,type,
sK193: ( 'Nat_real_fun_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat_real_fun$' ).
tff(func_def_210,type,
sK194: ( 'Nat_real_fun_bool_fun$' * 'Nat_real_fun_nat_real_fun_fun$' ) > 'Nat_real_fun$' ).
tff(func_def_211,type,
sK195: ( 'Nat_real_fun_bool_fun$' * 'Nat_real_fun_nat_real_fun_fun$' * 'Nat_bool_fun$' ) > 'Nat_real_fun_nat_nat_fun_fun$' ).
tff(func_def_212,type,
sK197: ( 'Nat_real_fun_bool_fun$' * 'Nat_bool_fun$' ) > 'Nat$' ).
tff(func_def_213,type,
sK198: ( 'Nat$' * 'Nat_real_fun$' ) > 'Nat$' ).
tff(func_def_214,type,
sK199: ( 'Nat$' * 'Nat_real_fun$' * 'Nat_real_fun$' ) > 'Nat$' ).
tff(pred_def_1,type,
'antimono$c': 'Int_int_fun$' > $o ).
tff(pred_def_2,type,
'fun_app$m': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).
tff(pred_def_3,type,
'antimono$b': 'Int_real_fun$' > $o ).
tff(pred_def_4,type,
'less_eq$a': ( 'Bool_int_fun$' * 'Bool_int_fun$' ) > $o ).
tff(pred_def_5,type,
'less_eq$': ( 'Bool_real_fun$' * 'Bool_real_fun$' ) > $o ).
tff(pred_def_6,type,
'fun_app$': ( 'Real_bool_fun$' * $real ) > $o ).
tff(pred_def_7,type,
'fun_app$k': ( 'Nat_real_fun_bool_fun$' * 'Nat_real_fun$' ) > $o ).
tff(pred_def_8,type,
'antimono$a': 'Real_int_fun$' > $o ).
tff(pred_def_9,type,
'partial_preordering$': 'Real_real_bool_fun_fun$' > $o ).
tff(pred_def_10,type,
'antimono$': 'Real_real_fun$' > $o ).
tff(pred_def_11,type,
'partial_preordering$a': 'Int_int_bool_fun_fun$' > $o ).
tff(pred_def_12,type,
'member$': ( $real * 'Real_set$' ) > $o ).
tff(pred_def_13,type,
'fun_app$b': ( 'Int_bool_fun$' * $int ) > $o ).
tff(pred_def_22,type,
sP49: ( $real * $real * $real ) > $o ).
tff(pred_def_23,type,
sP50: ( $real * $real * $real ) > $o ).
tff(pred_def_24,type,
sP51: ( $real * $real * $real ) > $o ).
tff(pred_def_25,type,
sP52: ( $real * $real * $real ) > $o ).
tff(pred_def_26,type,
sP53: ( $real * $real * $real ) > $o ).
tff(pred_def_29,type,
sP56: ( $int * $int * $int ) > $o ).
tff(pred_def_30,type,
sP57: ( $int * $int * $int ) > $o ).
tff(pred_def_31,type,
sP58: ( $int * $int * $int ) > $o ).
tff(pred_def_32,type,
sP59: ( $int * $int * $int ) > $o ).
tff(pred_def_33,type,
sP60: ( $int * $int * $int ) > $o ).
tff(pred_def_36,type,
sP67: ( $real * $real * 'Real_bool_fun$' ) > $o ).
tff(pred_def_37,type,
sP70: ( $int * $int * 'Int_bool_fun$' ) > $o ).
tff(pred_def_42,type,
sP98: ( $real * $real ) > $o ).
tff(pred_def_45,type,
sP101: ( $int * $int ) > $o ).
tff(pred_def_54,type,
sP196: ( 'Nat_real_fun_nat_nat_fun_fun$' * 'Nat_bool_fun$' * 'Nat_real_fun_nat_real_fun_fun$' * 'Nat_real_fun_bool_fun$' ) > $o ).
tff(pred_def_55,type,
sP200: ( 'Nat$' * 'Nat_real_fun$' * 'Nat_real_fun$' * 'Nat$' ) > $o ).
tff(f6,conjecture,
( 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$')
<=> 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture5) ).
tff(f7,negated_conjecture,
~ ( 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$')
<=> 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a') ),
inference(negated_conjecture,[status(cth)],[f6]) ).
tff(f8,axiom,
'a$' = 'a$a',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom6) ).
tff(f9,axiom,
'of_nat$'('n$') = 'of_nat$'('n$a'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom7) ).
tff(f10,axiom,
! [X0: $real] :
( $lesseq('fun_app$d'('of_int$','a$'),X0)
=> ( 'fun_app$e'('f$',X0) = 'fun_app$e'('g$',X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom8) ).
tff(f11,axiom,
! [X0: $int,X1: 'Real_a_fun$',X2: 'Real_a_fun$',X3: 'Nat$',X4: 'Nat$',X5: $int] :
( ( ! [X6: $real] :
( $lesseq('fun_app$d'('of_int$',X0),X6)
=> ( 'fun_app$e'(X1,X6) = 'fun_app$e'(X2,X6) ) )
& ( 'of_nat$'(X3) = 'of_nat$'(X4) )
& ( X0 = X5 ) )
=> ( 'fun_app$b'('eM_remainder_converges$'(X3,X1),X0)
<=> 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom9) ).
tff(f622,axiom,
! [X0: 'Nat$'] : ( 'nat$'('of_nat$'(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom620) ).
tff(f628,plain,
! [X0: $real] :
( ~ $less(X0,'fun_app$d'('of_int$','a$'))
=> ( 'fun_app$e'('f$',X0) = 'fun_app$e'('g$',X0) ) ),
inference(theory_normalization,[],[f10]) ).
tff(f629,plain,
! [X0: $int,X1: 'Real_a_fun$',X2: 'Real_a_fun$',X3: 'Nat$',X4: 'Nat$',X5: $int] :
( ( ! [X6: $real] :
( ~ $less(X6,'fun_app$d'('of_int$',X0))
=> ( 'fun_app$e'(X1,X6) = 'fun_app$e'(X2,X6) ) )
& ( 'of_nat$'(X3) = 'of_nat$'(X4) )
& ( X0 = X5 ) )
=> ( 'fun_app$b'('eM_remainder_converges$'(X3,X1),X0)
<=> 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5) ) ),
inference(theory_normalization,[],[f11]) ).
tff(f949,plain,
( 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$')
<~> 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a') ),
inference(ennf_transformation,[],[f7]) ).
tff(f950,plain,
! [X0: $real] :
( ( 'fun_app$e'('f$',X0) = 'fun_app$e'('g$',X0) )
| $less(X0,'fun_app$d'('of_int$','a$')) ),
inference(ennf_transformation,[],[f628]) ).
tff(f951,plain,
! [X0: $int,X1: 'Real_a_fun$',X2: 'Real_a_fun$',X3: 'Nat$',X4: 'Nat$',X5: $int] :
( ( 'fun_app$b'('eM_remainder_converges$'(X3,X1),X0)
<=> 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5) )
| ? [X6: $real] :
( ( 'fun_app$e'(X1,X6) != 'fun_app$e'(X2,X6) )
& ~ $less(X6,'fun_app$d'('of_int$',X0)) )
| ( 'of_nat$'(X3) != 'of_nat$'(X4) )
| ( X0 != X5 ) ),
inference(ennf_transformation,[],[f629]) ).
tff(f952,plain,
! [X0: $int,X1: 'Real_a_fun$',X2: 'Real_a_fun$',X3: 'Nat$',X4: 'Nat$',X5: $int] :
( ( 'fun_app$b'('eM_remainder_converges$'(X3,X1),X0)
<=> 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5) )
| ? [X6: $real] :
( ( 'fun_app$e'(X1,X6) != 'fun_app$e'(X2,X6) )
& ~ $less(X6,'fun_app$d'('of_int$',X0)) )
| ( 'of_nat$'(X3) != 'of_nat$'(X4) )
| ( X0 != X5 ) ),
inference(flattening,[],[f951]) ).
tff(f1365,plain,
( 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a')
| 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$') ),
inference(cnf_transformation,[],[f949]) ).
tff(f1366,plain,
( ~ 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a')
| ~ 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$') ),
inference(cnf_transformation,[],[f949]) ).
tff(f1367,plain,
'a$' = 'a$a',
inference(cnf_transformation,[],[f8]) ).
tff(f1368,plain,
'of_nat$'('n$') = 'of_nat$'('n$a'),
inference(cnf_transformation,[],[f9]) ).
tff(f1369,plain,
! [X0: $real] :
( $less(X0,'fun_app$d'('of_int$','a$'))
| ( 'fun_app$e'('f$',X0) = 'fun_app$e'('g$',X0) ) ),
inference(cnf_transformation,[],[f950]) ).
tff(f1370,plain,
! [X2: 'Real_a_fun$',X3: 'Nat$',X0: $int,X1: 'Real_a_fun$',X4: 'Nat$',X5: $int] :
( ( X0 != X5 )
| ( 'of_nat$'(X3) != 'of_nat$'(X4) )
| ~ $less(sK0(X0,X1,X2),'fun_app$d'('of_int$',X0))
| 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5)
| ~ 'fun_app$b'('eM_remainder_converges$'(X3,X1),X0) ),
inference(cnf_transformation,[],[f952]) ).
tff(f1371,plain,
! [X2: 'Real_a_fun$',X3: 'Nat$',X0: $int,X1: 'Real_a_fun$',X4: 'Nat$',X5: $int] :
( ( X0 != X5 )
| ( 'of_nat$'(X3) != 'of_nat$'(X4) )
| ( 'fun_app$e'(X1,sK0(X0,X1,X2)) != 'fun_app$e'(X2,sK0(X0,X1,X2)) )
| 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5)
| ~ 'fun_app$b'('eM_remainder_converges$'(X3,X1),X0) ),
inference(cnf_transformation,[],[f952]) ).
tff(f1372,plain,
! [X2: 'Real_a_fun$',X3: 'Nat$',X0: $int,X1: 'Real_a_fun$',X4: 'Nat$',X5: $int] :
( ( X0 != X5 )
| ( 'of_nat$'(X3) != 'of_nat$'(X4) )
| ~ $less(sK0(X0,X1,X2),'fun_app$d'('of_int$',X0))
| ~ 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5)
| 'fun_app$b'('eM_remainder_converges$'(X3,X1),X0) ),
inference(cnf_transformation,[],[f952]) ).
tff(f1373,plain,
! [X2: 'Real_a_fun$',X3: 'Nat$',X0: $int,X1: 'Real_a_fun$',X4: 'Nat$',X5: $int] :
( ( X0 != X5 )
| ( 'of_nat$'(X3) != 'of_nat$'(X4) )
| ( 'fun_app$e'(X1,sK0(X0,X1,X2)) != 'fun_app$e'(X2,sK0(X0,X1,X2)) )
| ~ 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5)
| 'fun_app$b'('eM_remainder_converges$'(X3,X1),X0) ),
inference(cnf_transformation,[],[f952]) ).
tff(f2383,plain,
! [X0: 'Nat$'] : ( 'nat$'('of_nat$'(X0)) = X0 ),
inference(cnf_transformation,[],[f622]) ).
tff(f2388,plain,
( ~ 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a')
| ~ 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$a') ),
inference(definition_unfolding,[],[f1366,f1367]) ).
tff(f2389,plain,
( 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a')
| 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$a') ),
inference(definition_unfolding,[],[f1365,f1367]) ).
tff(f2390,plain,
! [X0: $real] :
( $less(X0,'fun_app$d'('of_int$','a$a'))
| ( 'fun_app$e'('f$',X0) = 'fun_app$e'('g$',X0) ) ),
inference(definition_unfolding,[],[f1369,f1367]) ).
tff(f2391,plain,
! [X2: 'Real_a_fun$',X3: 'Nat$',X1: 'Real_a_fun$',X4: 'Nat$',X5: $int] :
( ~ 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5)
| ( 'fun_app$e'(X1,sK0(X5,X1,X2)) != 'fun_app$e'(X2,sK0(X5,X1,X2)) )
| ( 'of_nat$'(X3) != 'of_nat$'(X4) )
| 'fun_app$b'('eM_remainder_converges$'(X3,X1),X5) ),
inference(equality_resolution,[],[f1373]) ).
tff(f2392,plain,
! [X2: 'Real_a_fun$',X3: 'Nat$',X1: 'Real_a_fun$',X4: 'Nat$',X5: $int] :
( ~ 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5)
| ~ $less(sK0(X5,X1,X2),'fun_app$d'('of_int$',X5))
| ( 'of_nat$'(X3) != 'of_nat$'(X4) )
| 'fun_app$b'('eM_remainder_converges$'(X3,X1),X5) ),
inference(equality_resolution,[],[f1372]) ).
tff(f2393,plain,
! [X2: 'Real_a_fun$',X3: 'Nat$',X1: 'Real_a_fun$',X4: 'Nat$',X5: $int] :
( ~ 'fun_app$b'('eM_remainder_converges$'(X3,X1),X5)
| ( 'fun_app$e'(X1,sK0(X5,X1,X2)) != 'fun_app$e'(X2,sK0(X5,X1,X2)) )
| 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5)
| ( 'of_nat$'(X3) != 'of_nat$'(X4) ) ),
inference(equality_resolution,[],[f1371]) ).
tff(f2394,plain,
! [X2: 'Real_a_fun$',X3: 'Nat$',X1: 'Real_a_fun$',X4: 'Nat$',X5: $int] :
( ~ 'fun_app$b'('eM_remainder_converges$'(X3,X1),X5)
| ~ $less(sK0(X5,X1,X2),'fun_app$d'('of_int$',X5))
| 'fun_app$b'('eM_remainder_converges$'(X4,X2),X5)
| ( 'of_nat$'(X3) != 'of_nat$'(X4) ) ),
inference(equality_resolution,[],[f1370]) ).
tff(f2774,definition,
( spl201_13
<=> 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$a') ),
introduced(definition,[new_symbols(definition,[spl201_13])],[avatar_definition]) ).
tff(f2775,plain,
( ~ 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$a')
| spl201_13 ),
inference(avatar_component_clause,[],[f2774]) ).
tff(f2776,plain,
( 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$a')
| ~ spl201_13 ),
inference(avatar_component_clause,[],[f2774]) ).
tff(f2778,definition,
( spl201_14
<=> 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a') ),
introduced(definition,[new_symbols(definition,[spl201_14])],[avatar_definition]) ).
tff(f2779,plain,
( ~ 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a')
| spl201_14 ),
inference(avatar_component_clause,[],[f2778]) ).
tff(f2780,plain,
( 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a')
| ~ spl201_14 ),
inference(avatar_component_clause,[],[f2778]) ).
tff(f2781,plain,
( spl201_13
| spl201_14 ),
inference(avatar_split_clause,[],[f2389,f2778,f2774]) ).
tff(f2782,plain,
( ~ spl201_13
| ~ spl201_14 ),
inference(avatar_split_clause,[],[f2388,f2778,f2774]) ).
tff(f3187,plain,
'n$' = 'nat$'('of_nat$'('n$a')),
inference(superposition,[],[f2383,f1368]) ).
tff(f3188,plain,
'n$' = 'n$a',
inference(forward_demodulation,[],[f3187,f2383]) ).
tff(f3189,plain,
( ~ 'fun_app$b'('eM_remainder_converges$'('n$a','f$'),'a$a')
| spl201_13 ),
inference(superposition,[],[f2775,f3188]) ).
tff(f3228,plain,
( ! [X0: 'Real_a_fun$',X1: 'Nat$'] :
( ~ $less(sK0('a$a',X0,'g$'),'fun_app$d'('of_int$','a$a'))
| ( 'of_nat$'('n$a') != 'of_nat$'(X1) )
| 'fun_app$b'('eM_remainder_converges$'(X1,X0),'a$a') )
| ~ spl201_14 ),
inference(resolution,[],[f2392,f2780]) ).
tff(f3308,plain,
( ! [X0: 'Real_a_fun$',X1: 'Nat$'] :
( ( 'fun_app$e'(X0,sK0('a$a',X0,'g$')) != 'fun_app$e'('g$',sK0('a$a',X0,'g$')) )
| ( 'of_nat$'('n$a') != 'of_nat$'(X1) )
| 'fun_app$b'('eM_remainder_converges$'(X1,X0),'a$a') )
| ~ spl201_14 ),
inference(resolution,[],[f2391,f2780]) ).
tff(f3524,plain,
( ! [X0: 'Nat$',X1: 'Real_a_fun$'] :
( ( 'of_nat$'('n$a') != 'of_nat$'(X0) )
| 'fun_app$b'('eM_remainder_converges$'(X0,X1),'a$a')
| ( 'fun_app$e'('f$',sK0('a$a',X1,'g$')) = 'fun_app$e'('g$',sK0('a$a',X1,'g$')) ) )
| ~ spl201_14 ),
inference(resolution,[],[f3228,f2390]) ).
tff(f3707,plain,
( ! [X0: 'Real_a_fun$'] :
( 'fun_app$b'('eM_remainder_converges$'('n$a',X0),'a$a')
| ( 'fun_app$e'('g$',sK0('a$a',X0,'g$')) = 'fun_app$e'('f$',sK0('a$a',X0,'g$')) ) )
| ~ spl201_14 ),
inference(equality_resolution,[],[f3524]) ).
tff(f3745,plain,
( ( 'fun_app$e'('g$',sK0('a$a','f$','g$')) = 'fun_app$e'('f$',sK0('a$a','f$','g$')) )
| spl201_13
| ~ spl201_14 ),
inference(resolution,[],[f3707,f3189]) ).
tff(f3780,plain,
( ! [X0: 'Nat$'] :
( ( 'fun_app$e'('g$',sK0('a$a','f$','g$')) != 'fun_app$e'('g$',sK0('a$a','f$','g$')) )
| ( 'of_nat$'('n$a') != 'of_nat$'(X0) )
| 'fun_app$b'('eM_remainder_converges$'(X0,'f$'),'a$a') )
| spl201_13
| ~ spl201_14 ),
inference(superposition,[],[f3308,f3745]) ).
tff(f3781,plain,
( ! [X0: 'Nat$'] :
( ( 'of_nat$'('n$a') != 'of_nat$'(X0) )
| 'fun_app$b'('eM_remainder_converges$'(X0,'f$'),'a$a') )
| spl201_13
| ~ spl201_14 ),
inference(trivial_inequality_removal,[],[f3780]) ).
tff(f3789,plain,
( ( 'of_nat$'('n$a') != 'of_nat$'('n$a') )
| 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$a')
| spl201_13
| ~ spl201_14 ),
inference(superposition,[],[f3781,f1368]) ).
tff(f3791,plain,
( 'fun_app$b'('eM_remainder_converges$'('n$','f$'),'a$a')
| spl201_13
| ~ spl201_14 ),
inference(trivial_inequality_removal,[],[f3789]) ).
tff(f3794,plain,
( $false
| spl201_13
| ~ spl201_14 ),
inference(forward_subsumption_resolution,[],[f3791,f2775]) ).
tff(f3795,plain,
( spl201_13
| ~ spl201_14 ),
inference(avatar_contradiction_clause,[],[f3794]) ).
tff(f3796,plain,
( 'fun_app$b'('eM_remainder_converges$'('n$a','f$'),'a$a')
| ~ spl201_13 ),
inference(forward_demodulation,[],[f2776,f3188]) ).
tff(f3871,plain,
( ! [X0: 'Real_a_fun$',X1: 'Nat$'] :
( ( 'fun_app$e'('f$',sK0('a$a','f$',X0)) != 'fun_app$e'(X0,sK0('a$a','f$',X0)) )
| 'fun_app$b'('eM_remainder_converges$'(X1,X0),'a$a')
| ( 'of_nat$'('n$a') != 'of_nat$'(X1) ) )
| ~ spl201_13 ),
inference(resolution,[],[f3796,f2393]) ).
tff(f3873,plain,
( ! [X0: 'Real_a_fun$',X1: 'Nat$'] :
( ~ $less(sK0('a$a','f$',X0),'fun_app$d'('of_int$','a$a'))
| 'fun_app$b'('eM_remainder_converges$'(X1,X0),'a$a')
| ( 'of_nat$'('n$a') != 'of_nat$'(X1) ) )
| ~ spl201_13 ),
inference(resolution,[],[f3796,f2394]) ).
tff(f4024,plain,
( ! [X0: 'Nat$',X1: 'Real_a_fun$'] :
( ( 'of_nat$'('n$a') != 'of_nat$'(X0) )
| 'fun_app$b'('eM_remainder_converges$'(X0,X1),'a$a')
| ( 'fun_app$e'('f$',sK0('a$a','f$',X1)) = 'fun_app$e'('g$',sK0('a$a','f$',X1)) ) )
| ~ spl201_13 ),
inference(resolution,[],[f3873,f2390]) ).
tff(f4621,plain,
( ! [X0: 'Real_a_fun$'] :
( 'fun_app$b'('eM_remainder_converges$'('n$a',X0),'a$a')
| ( 'fun_app$e'('f$',sK0('a$a','f$',X0)) = 'fun_app$e'('g$',sK0('a$a','f$',X0)) ) )
| ~ spl201_13 ),
inference(equality_resolution,[],[f4024]) ).
tff(f4624,plain,
( ( 'fun_app$e'('g$',sK0('a$a','f$','g$')) = 'fun_app$e'('f$',sK0('a$a','f$','g$')) )
| ~ spl201_13
| spl201_14 ),
inference(resolution,[],[f4621,f2779]) ).
tff(f4630,plain,
( ! [X0: 'Nat$'] :
( ( 'fun_app$e'('g$',sK0('a$a','f$','g$')) != 'fun_app$e'('g$',sK0('a$a','f$','g$')) )
| 'fun_app$b'('eM_remainder_converges$'(X0,'g$'),'a$a')
| ( 'of_nat$'('n$a') != 'of_nat$'(X0) ) )
| ~ spl201_13
| spl201_14 ),
inference(superposition,[],[f3871,f4624]) ).
tff(f4631,plain,
( ! [X0: 'Nat$'] :
( ( 'of_nat$'('n$a') != 'of_nat$'(X0) )
| 'fun_app$b'('eM_remainder_converges$'(X0,'g$'),'a$a') )
| ~ spl201_13
| spl201_14 ),
inference(trivial_inequality_removal,[],[f4630]) ).
tff(f4636,plain,
( ( 'of_nat$'('n$a') != 'of_nat$'('n$a') )
| 'fun_app$b'('eM_remainder_converges$'('n$','g$'),'a$a')
| ~ spl201_13
| spl201_14 ),
inference(superposition,[],[f4631,f1368]) ).
tff(f4638,plain,
( 'fun_app$b'('eM_remainder_converges$'('n$','g$'),'a$a')
| ~ spl201_13
| spl201_14 ),
inference(trivial_inequality_removal,[],[f4636]) ).
tff(f4641,plain,
( 'fun_app$b'('eM_remainder_converges$'('n$a','g$'),'a$a')
| ~ spl201_13
| spl201_14 ),
inference(forward_demodulation,[],[f4638,f3188]) ).
tff(f4642,plain,
( $false
| ~ spl201_13
| spl201_14 ),
inference(forward_subsumption_resolution,[],[f4641,f2779]) ).
tff(f4643,plain,
( ~ spl201_13
| spl201_14 ),
inference(avatar_contradiction_clause,[],[f4642]) ).
cnf(s11,plain,
( spl201_13
| spl201_14 ),
inference(sat_conversion,[],[f2781]) ).
cnf(s12,plain,
( ~ spl201_13
| ~ spl201_14 ),
inference(sat_conversion,[],[f2782]) ).
cnf(s102,plain,
( spl201_13
| ~ spl201_14 ),
inference(sat_conversion,[],[f3795]) ).
cnf(s112,plain,
( ~ spl201_13
| spl201_14 ),
inference(sat_conversion,[],[f4643]) ).
cnf(s125,plain,
spl201_13,
inference(rat,[],[s11,s102]) ).
cnf(s126,plain,
spl201_14,
inference(rat,[],[s112,s125]) ).
cnf(s127,plain,
$false,
inference(rat,[],[s12,s126,s125]) ).
tff(f4644,plain,
$false,
inference(avatar_sat_refutation,[],[s127]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ITP317_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Sun Sep 27 12:53:50 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.32 Running first-order model finding
% 0.07/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.31/0.54 % (2362796)Will run a generic schedule for satisfiability detection.
% 1.31/0.54 % (2362802)% WARNING: option uhcvi not known.
% 1.31/0.54 % (2362806)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4254681651:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.31/0.54 % (2362801)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2445835865_2999 on theBenchmark for (2999ds/0Mi)
% 1.31/0.54 % (2362803)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3968801214:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.31/0.54 % (2362802)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2960173986:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.31/0.54 % (2362804)dis+10_1_sil=32000:sp=arity:random_seed=2428470549:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.31/0.54 % (2362805)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3695960026:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.31/0.54 % (2362807)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3480401719:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.31/0.54 % (2362801)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.31/0.54 % (2362801)Terminated due to inappropriate strategy.
% 1.31/0.54 % (2362801)------------------------------
% 1.31/0.54 % (2362801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.54 % (2362801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.54 % (2362801)CaDiCaL version: 2.1.3
% 1.31/0.54 % (2362801)Termination reason: Inappropriate
% 1.31/0.54 % (2362801)Time elapsed: 0.012 s
% 1.31/0.54 % (2362801)Peak memory usage: 12 MB
% 1.31/0.54 % (2362801)Instructions burned: 45 (million)
% 1.31/0.54 % (2362801)------------------------------
% 1.31/0.54 % (2362801)------------------------------
% 1.31/0.54 % (2362815)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=944854845:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.31/0.54 % (2362804)Instruction limit reached!
% 1.31/0.54 % (2362804)------------------------------
% 1.31/0.54 % (2362804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.55 % (2362804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.55 % (2362804)CaDiCaL version: 2.1.3
% 1.31/0.55 % (2362804)Termination reason: Instruction limit
% 1.31/0.55 % (2362804)Termination phase: Saturation
% 1.31/0.55 % (2362804)Time elapsed: 0.033 s
% 1.31/0.55 % (2362804)Peak memory usage: 13 MB
% 1.31/0.55 % (2362804)Instructions burned: 104 (million)
% 1.31/0.55 % (2362815)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.31/0.55 % (2362815)Terminated due to inappropriate strategy.
% 1.31/0.55 % (2362815)------------------------------
% 1.31/0.55 % (2362815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.55 % (2362815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.55 % (2362815)CaDiCaL version: 2.1.3
% 1.31/0.55 % (2362815)Termination reason: Inappropriate
% 1.31/0.55 % (2362815)Time elapsed: 0.011 s
% 1.31/0.55 % (2362815)Peak memory usage: 12 MB
% 1.31/0.55 % (2362815)Instructions burned: 42 (million)
% 1.31/0.55 % (2362815)------------------------------
% 1.31/0.55 % (2362815)------------------------------
% 1.31/0.55 % (2362805)Instruction limit reached!
% 1.31/0.55 % (2362805)------------------------------
% 1.31/0.55 % (2362805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.55 % (2362805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.55 % (2362805)CaDiCaL version: 2.1.3
% 1.31/0.55 % (2362805)Termination reason: Instruction limit
% 1.31/0.55 % (2362805)Termination phase: Saturation
% 1.31/0.55 % (2362805)Time elapsed: 0.038 s
% 1.31/0.55 % (2362805)Peak memory usage: 14 MB
% 1.31/0.55 % (2362805)Instructions burned: 118 (million)
% 1.31/0.55 % (2362806)Instruction limit reached!
% 1.31/0.55 % (2362806)------------------------------
% 1.31/0.55 % (2362806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.55 % (2362806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.55 % (2362806)CaDiCaL version: 2.1.3
% 1.31/0.55 % (2362806)Termination reason: Instruction limit
% 1.31/0.55 % (2362806)Termination phase: Saturation
% 1.31/0.55 % (2362806)Time elapsed: 0.042 s
% 1.31/0.55 % (2362806)Peak memory usage: 14 MB
% 1.31/0.55 % (2362806)Instructions burned: 132 (million)
% 1.31/0.55 % (2362817)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1243058224:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.31/0.55 % (2362818)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1783380178:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.31/0.55 % (2362819)ott-21_1_sil=16000:fs=off:random_seed=916176813:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.31/0.55 % (2362807)Instruction limit reached!
% 1.31/0.55 % (2362807)------------------------------
% 1.31/0.55 % (2362807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.55 % (2362807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.55 % (2362807)CaDiCaL version: 2.1.3
% 1.31/0.55 % (2362807)Termination reason: Instruction limit
% 1.31/0.55 % (2362807)Termination phase: Saturation
% 1.31/0.55 % (2362807)Time elapsed: 0.051 s
% 1.31/0.55 % (2362807)Peak memory usage: 14 MB
% 1.31/0.55 % (2362807)Instructions burned: 160 (million)
% 1.31/0.55 % (2362820)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2160412981:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 1.31/0.55 % (2362824)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3407016099:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 1.31/0.55 % (2362824)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.31/0.55 % (2362824)Terminated due to inappropriate strategy.
% 1.31/0.55 % (2362824)------------------------------
% 1.31/0.55 % (2362824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.55 % (2362824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.55 % (2362824)CaDiCaL version: 2.1.3
% 1.31/0.55 % (2362824)Termination reason: Inappropriate
% 1.31/0.55 % (2362824)Time elapsed: 0.011 s
% 1.31/0.55 % (2362824)Peak memory usage: 11 MB
% 1.31/0.55 % (2362824)Instructions burned: 42 (million)
% 1.31/0.55 % (2362824)------------------------------
% 1.31/0.55 % (2362824)------------------------------
% 1.31/0.55 % (2362827)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4137699346:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.31/0.55 % (2362817)Instruction limit reached!
% 1.31/0.55 % (2362817)------------------------------
% 1.31/0.55 % (2362817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.55 % (2362817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.55 % (2362817)CaDiCaL version: 2.1.3
% 1.31/0.55 % (2362817)Termination reason: Instruction limit
% 1.31/0.55 % (2362817)Termination phase: Saturation
% 1.31/0.55 % (2362817)Time elapsed: 0.043 s
% 1.31/0.55 % (2362817)Peak memory usage: 14 MB
% 1.31/0.55 % (2362817)Instructions burned: 132 (million)
% 1.31/0.55 % (2362819)Instruction limit reached!
% 1.31/0.55 % (2362819)------------------------------
% 1.31/0.55 % (2362819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.55 % (2362819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.55 % (2362819)CaDiCaL version: 2.1.3
% 1.31/0.55 % (2362819)Termination reason: Instruction limit
% 1.31/0.55 % (2362819)Termination phase: Saturation
% 1.31/0.55 % (2362819)Time elapsed: 0.046 s
% 1.31/0.55 % (2362819)Peak memory usage: 14 MB
% 1.31/0.55 % (2362819)Instructions burned: 181 (million)
% 1.31/0.55 % (2362829)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2637744989:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.31/0.55 % (2362830)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2522433619:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 1.31/0.55 % (2362829)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.31/0.55 % (2362829)Terminated due to inappropriate strategy.
% 1.31/0.55 % (2362829)------------------------------
% 1.31/0.55 % (2362829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.55 % (2362829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.55 % (2362829)CaDiCaL version: 2.1.3
% 1.31/0.55 % (2362829)Termination reason: Inappropriate
% 1.31/0.55 % (2362829)Time elapsed: 0.011 s
% 1.31/0.55 % (2362829)Peak memory usage: 11 MB
% 1.31/0.55 % (2362829)Instructions burned: 43 (million)
% 1.31/0.55 % (2362829)------------------------------
% 1.31/0.55 % (2362829)------------------------------
% 1.31/0.55 % (2362833)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4156407591:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 1.31/0.55 % (2362830) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2362796-2362830"...
% 1.31/0.55 % (2362830)...printing done.
% 1.31/0.55 % (2362830)Refutation found. Thanks to Tanya!
% 1.31/0.55 % SZS status Theorem for theBenchmark
% 1.31/0.55 % SZS output start Proof for theBenchmark
% See solution above
% 1.31/0.55 % (2362830)------------------------------
% 1.31/0.55 % (2362830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.55 % (2362830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.55 % (2362830)CaDiCaL version: 2.1.3
% 1.31/0.55 % (2362830)Termination reason: Refutation
% 1.31/0.55 % (2362830)Time elapsed: 0.074 s
% 1.31/0.55 % (2362830)Peak memory usage: 16 MB
% 1.31/0.55 % (2362830)Instructions burned: 221 (million)
% 1.31/0.55 % (2362796)Success in time 0.219 s
% 1.31/0.55 % Vampire exiting
%------------------------------------------------------------------------------