%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MSC018-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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 12:05:47 PM UTC 2026
% Result : Satisfiable 0.28s 0.50s
% Output : FiniteModel 0.28s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_s_g001,type,
s_g001: $i ).
tff(s_g001_definition,axiom,
s_g001 = 'fmb_$i_1' ).
tff(declare_s_g002,type,
s_g002: $i ).
tff(s_g002_definition,axiom,
s_g002 = 'fmb_$i_2' ).
tff(declare_true,type,
true: $i ).
tff(true_definition,axiom,
true = 'fmb_$i_1' ).
tff(declare_s_g009,type,
s_g009: $i ).
tff(s_g009_definition,axiom,
s_g009 = 'fmb_$i_2' ).
tff(declare_s_g019,type,
s_g019: $i ).
tff(s_g019_definition,axiom,
s_g019 = 'fmb_$i_1' ).
tff(declare_s_g142,type,
s_g142: $i ).
tff(s_g142_definition,axiom,
s_g142 = 'fmb_$i_2' ).
tff(declare_s_g150,type,
s_g150: $i ).
tff(s_g150_definition,axiom,
s_g150 = 'fmb_$i_2' ).
tff(declare_s_g011,type,
s_g011: $i ).
tff(s_g011_definition,axiom,
s_g011 = 'fmb_$i_2' ).
tff(declare_s_g014,type,
s_g014: $i ).
tff(s_g014_definition,axiom,
s_g014 = 'fmb_$i_2' ).
tff(declare_s_g015,type,
s_g015: $i ).
tff(s_g015_definition,axiom,
s_g015 = 'fmb_$i_2' ).
tff(declare_s_g017,type,
s_g017: $i ).
tff(s_g017_definition,axiom,
s_g017 = 'fmb_$i_2' ).
tff(declare_s_g018,type,
s_g018: $i ).
tff(s_g018_definition,axiom,
s_g018 = 'fmb_$i_2' ).
tff(declare_s_g053,type,
s_g053: $i ).
tff(s_g053_definition,axiom,
s_g053 = 'fmb_$i_2' ).
tff(declare_s_g054,type,
s_g054: $i ).
tff(s_g054_definition,axiom,
s_g054 = 'fmb_$i_2' ).
tff(declare_s_g057,type,
s_g057: $i ).
tff(s_g057_definition,axiom,
s_g057 = 'fmb_$i_2' ).
tff(declare_s_g061,type,
s_g061: $i ).
tff(s_g061_definition,axiom,
s_g061 = 'fmb_$i_2' ).
tff(declare_s_g005,type,
s_g005: $i ).
tff(s_g005_definition,axiom,
s_g005 = 'fmb_$i_2' ).
tff(declare_s_g013,type,
s_g013: $i ).
tff(s_g013_definition,axiom,
s_g013 = 'fmb_$i_1' ).
tff(declare_s_g021,type,
s_g021: $i ).
tff(s_g021_definition,axiom,
s_g021 = 'fmb_$i_2' ).
tff(declare_s_g029,type,
s_g029: $i ).
tff(s_g029_definition,axiom,
s_g029 = 'fmb_$i_2' ).
tff(declare_s_g003,type,
s_g003: $i ).
tff(s_g003_definition,axiom,
s_g003 = 'fmb_$i_1' ).
tff(declare_s_g419,type,
s_g419: $i ).
tff(s_g419_definition,axiom,
s_g419 = 'fmb_$i_1' ).
tff(declare_s_g030,type,
s_g030: $i ).
tff(s_g030_definition,axiom,
s_g030 = 'fmb_$i_2' ).
tff(declare_s_g035,type,
s_g035: $i ).
tff(s_g035_definition,axiom,
s_g035 = 'fmb_$i_2' ).
tff(declare_s_g143,type,
s_g143: $i ).
tff(s_g143_definition,axiom,
s_g143 = 'fmb_$i_2' ).
tff(declare_s_g145,type,
s_g145: $i ).
tff(s_g145_definition,axiom,
s_g145 = 'fmb_$i_2' ).
tff(declare_s_g034,type,
s_g034: $i ).
tff(s_g034_definition,axiom,
s_g034 = 'fmb_$i_2' ).
tff(declare_s_g062,type,
s_g062: $i ).
tff(s_g062_definition,axiom,
s_g062 = 'fmb_$i_2' ).
tff(declare_s_g039,type,
s_g039: $i ).
tff(s_g039_definition,axiom,
s_g039 = 'fmb_$i_2' ).
tff(declare_s_g151,type,
s_g151: $i ).
tff(s_g151_definition,axiom,
s_g151 = 'fmb_$i_2' ).
tff(declare_s_g154,type,
s_g154: $i ).
tff(s_g154_definition,axiom,
s_g154 = 'fmb_$i_2' ).
tff(declare_s_g155,type,
s_g155: $i ).
tff(s_g155_definition,axiom,
s_g155 = 'fmb_$i_2' ).
tff(declare_s_BF,type,
s_BF: $i ).
tff(s_BF_definition,axiom,
s_BF = 'fmb_$i_2' ).
tff(declare_s_BJ,type,
s_BJ: $i ).
tff(s_BJ_definition,axiom,
s_BJ = 'fmb_$i_2' ).
tff(declare_s_CI,type,
s_CI: $i ).
tff(s_CI_definition,axiom,
s_CI = 'fmb_$i_2' ).
tff(declare_s_CV,type,
s_CV: $i ).
tff(s_CV_definition,axiom,
s_CV = 'fmb_$i_2' ).
tff(declare_s_GH,type,
s_GH: $i ).
tff(s_GH_definition,axiom,
s_GH = 'fmb_$i_2' ).
tff(declare_s_GM,type,
s_GM: $i ).
tff(s_GM_definition,axiom,
s_GM = 'fmb_$i_2' ).
tff(declare_s_GN,type,
s_GN: $i ).
tff(s_GN_definition,axiom,
s_GN = 'fmb_$i_2' ).
tff(declare_s_GW,type,
s_GW: $i ).
tff(s_GW_definition,axiom,
s_GW = 'fmb_$i_2' ).
tff(declare_s_LR,type,
s_LR: $i ).
tff(s_LR_definition,axiom,
s_LR = 'fmb_$i_2' ).
tff(declare_s_ML,type,
s_ML: $i ).
tff(s_ML_definition,axiom,
s_ML = 'fmb_$i_2' ).
tff(declare_s_MR,type,
s_MR: $i ).
tff(s_MR_definition,axiom,
s_MR = 'fmb_$i_2' ).
tff(declare_s_NE,type,
s_NE: $i ).
tff(s_NE_definition,axiom,
s_NE = 'fmb_$i_2' ).
tff(declare_s_NG,type,
s_NG: $i ).
tff(s_NG_definition,axiom,
s_NG = 'fmb_$i_2' ).
tff(declare_s_SH,type,
s_SH: $i ).
tff(s_SH_definition,axiom,
s_SH = 'fmb_$i_2' ).
tff(declare_s_SL,type,
s_SL: $i ).
tff(s_SL_definition,axiom,
s_SL = 'fmb_$i_2' ).
tff(declare_s_SN,type,
s_SN: $i ).
tff(s_SN_definition,axiom,
s_SN = 'fmb_$i_2' ).
tff(declare_s_TG,type,
s_TG: $i ).
tff(s_TG_definition,axiom,
s_TG = 'fmb_$i_2' ).
tff(declare_s_BZ,type,
s_BZ: $i ).
tff(s_BZ_definition,axiom,
s_BZ = 'fmb_$i_2' ).
tff(declare_s_CR,type,
s_CR: $i ).
tff(s_CR_definition,axiom,
s_CR = 'fmb_$i_2' ).
tff(declare_s_GT,type,
s_GT: $i ).
tff(s_GT_definition,axiom,
s_GT = 'fmb_$i_2' ).
tff(declare_s_HN,type,
s_HN: $i ).
tff(s_HN_definition,axiom,
s_HN = 'fmb_$i_2' ).
tff(declare_s_MX,type,
s_MX: $i ).
tff(s_MX_definition,axiom,
s_MX = 'fmb_$i_1' ).
tff(declare_s_NI,type,
s_NI: $i ).
tff(s_NI_definition,axiom,
s_NI = 'fmb_$i_2' ).
tff(declare_s_PA,type,
s_PA: $i ).
tff(s_PA_definition,axiom,
s_PA = 'fmb_$i_2' ).
tff(declare_s_SV,type,
s_SV: $i ).
tff(s_SV_definition,axiom,
s_SV = 'fmb_$i_2' ).
tff(declare_s_BI,type,
s_BI: $i ).
tff(s_BI_definition,axiom,
s_BI = 'fmb_$i_2' ).
tff(declare_s_DJ,type,
s_DJ: $i ).
tff(s_DJ_definition,axiom,
s_DJ = 'fmb_$i_2' ).
tff(declare_s_ER,type,
s_ER: $i ).
tff(s_ER_definition,axiom,
s_ER = 'fmb_$i_2' ).
tff(declare_s_ET,type,
s_ET: $i ).
tff(s_ET_definition,axiom,
s_ET = 'fmb_$i_2' ).
tff(declare_s_KE,type,
s_KE: $i ).
tff(s_KE_definition,axiom,
s_KE = 'fmb_$i_2' ).
tff(declare_s_KM,type,
s_KM: $i ).
tff(s_KM_definition,axiom,
s_KM = 'fmb_$i_2' ).
tff(declare_s_MG,type,
s_MG: $i ).
tff(s_MG_definition,axiom,
s_MG = 'fmb_$i_2' ).
tff(declare_s_MU,type,
s_MU: $i ).
tff(s_MU_definition,axiom,
s_MU = 'fmb_$i_2' ).
tff(declare_s_MW,type,
s_MW: $i ).
tff(s_MW_definition,axiom,
s_MW = 'fmb_$i_2' ).
tff(declare_s_MZ,type,
s_MZ: $i ).
tff(s_MZ_definition,axiom,
s_MZ = 'fmb_$i_2' ).
tff(declare_s_RE,type,
s_RE: $i ).
tff(s_RE_definition,axiom,
s_RE = 'fmb_$i_2' ).
tff(declare_s_RW,type,
s_RW: $i ).
tff(s_RW_definition,axiom,
s_RW = 'fmb_$i_2' ).
tff(declare_s_SC,type,
s_SC: $i ).
tff(s_SC_definition,axiom,
s_SC = 'fmb_$i_2' ).
tff(declare_s_SO,type,
s_SO: $i ).
tff(s_SO_definition,axiom,
s_SO = 'fmb_$i_2' ).
tff(declare_s_TZ,type,
s_TZ: $i ).
tff(s_TZ_definition,axiom,
s_TZ = 'fmb_$i_2' ).
tff(declare_s_UG,type,
s_UG: $i ).
tff(s_UG_definition,axiom,
s_UG = 'fmb_$i_2' ).
tff(declare_s_YT,type,
s_YT: $i ).
tff(s_YT_definition,axiom,
s_YT = 'fmb_$i_2' ).
tff(declare_s_ZM,type,
s_ZM: $i ).
tff(s_ZM_definition,axiom,
s_ZM = 'fmb_$i_2' ).
tff(declare_s_ZW,type,
s_ZW: $i ).
tff(s_ZW_definition,axiom,
s_ZW = 'fmb_$i_2' ).
tff(declare_s_CN,type,
s_CN: $i ).
tff(s_CN_definition,axiom,
s_CN = 'fmb_$i_2' ).
tff(declare_s_HK,type,
s_HK: $i ).
tff(s_HK_definition,axiom,
s_HK = 'fmb_$i_2' ).
tff(declare_s_JP,type,
s_JP: $i ).
tff(s_JP_definition,axiom,
s_JP = 'fmb_$i_2' ).
tff(declare_s_KP,type,
s_KP: $i ).
tff(s_KP_definition,axiom,
s_KP = 'fmb_$i_2' ).
tff(declare_s_KR,type,
s_KR: $i ).
tff(s_KR_definition,axiom,
s_KR = 'fmb_$i_2' ).
tff(declare_s_MN,type,
s_MN: $i ).
tff(s_MN_definition,axiom,
s_MN = 'fmb_$i_2' ).
tff(declare_s_MO,type,
s_MO: $i ).
tff(s_MO_definition,axiom,
s_MO = 'fmb_$i_2' ).
tff(declare_s_TW,type,
s_TW: $i ).
tff(s_TW_definition,axiom,
s_TW = 'fmb_$i_2' ).
tff(declare_s_BN,type,
s_BN: $i ).
tff(s_BN_definition,axiom,
s_BN = 'fmb_$i_2' ).
tff(declare_s_ID,type,
s_ID: $i ).
tff(s_ID_definition,axiom,
s_ID = 'fmb_$i_2' ).
tff(declare_s_KH,type,
s_KH: $i ).
tff(s_KH_definition,axiom,
s_KH = 'fmb_$i_2' ).
tff(declare_s_LA,type,
s_LA: $i ).
tff(s_LA_definition,axiom,
s_LA = 'fmb_$i_2' ).
tff(declare_s_MM,type,
s_MM: $i ).
tff(s_MM_definition,axiom,
s_MM = 'fmb_$i_2' ).
tff(declare_s_BU,type,
s_BU: $i ).
tff(s_BU_definition,axiom,
s_BU = 'fmb_$i_2' ).
tff(declare_s_MY,type,
s_MY: $i ).
tff(s_MY_definition,axiom,
s_MY = 'fmb_$i_2' ).
tff(declare_s_PH,type,
s_PH: $i ).
tff(s_PH_definition,axiom,
s_PH = 'fmb_$i_2' ).
tff(declare_s_SG,type,
s_SG: $i ).
tff(s_SG_definition,axiom,
s_SG = 'fmb_$i_2' ).
tff(declare_s_TH,type,
s_TH: $i ).
tff(s_TH_definition,axiom,
s_TH = 'fmb_$i_2' ).
tff(declare_s_TL,type,
s_TL: $i ).
tff(s_TL_definition,axiom,
s_TL = 'fmb_$i_2' ).
tff(declare_s_TP,type,
s_TP: $i ).
tff(s_TP_definition,axiom,
s_TP = 'fmb_$i_2' ).
tff(declare_s_VN,type,
s_VN: $i ).
tff(s_VN_definition,axiom,
s_VN = 'fmb_$i_2' ).
tff(declare_s_TM,type,
s_TM: $i ).
tff(s_TM_definition,axiom,
s_TM = 'fmb_$i_2' ).
tff(declare_s_TJ,type,
s_TJ: $i ).
tff(s_TJ_definition,axiom,
s_TJ = 'fmb_$i_2' ).
tff(declare_s_KG,type,
s_KG: $i ).
tff(s_KG_definition,axiom,
s_KG = 'fmb_$i_2' ).
tff(declare_s_KZ,type,
s_KZ: $i ).
tff(s_KZ_definition,axiom,
s_KZ = 'fmb_$i_2' ).
tff(declare_s_UZ,type,
s_UZ: $i ).
tff(s_UZ_definition,axiom,
s_UZ = 'fmb_$i_2' ).
tff(declare_s_AE,type,
s_AE: $i ).
tff(s_AE_definition,axiom,
s_AE = 'fmb_$i_2' ).
tff(declare_s_AM,type,
s_AM: $i ).
tff(s_AM_definition,axiom,
s_AM = 'fmb_$i_2' ).
tff(declare_s_AZ,type,
s_AZ: $i ).
tff(s_AZ_definition,axiom,
s_AZ = 'fmb_$i_2' ).
tff(declare_s_BH,type,
s_BH: $i ).
tff(s_BH_definition,axiom,
s_BH = 'fmb_$i_2' ).
tff(declare_s_CY,type,
s_CY: $i ).
tff(s_CY_definition,axiom,
s_CY = 'fmb_$i_2' ).
tff(declare_s_GE,type,
s_GE: $i ).
tff(s_GE_definition,axiom,
s_GE = 'fmb_$i_2' ).
tff(declare_s_IL,type,
s_IL: $i ).
tff(s_IL_definition,axiom,
s_IL = 'fmb_$i_2' ).
tff(declare_s_IQ,type,
s_IQ: $i ).
tff(s_IQ_definition,axiom,
s_IQ = 'fmb_$i_2' ).
tff(declare_s_JO,type,
s_JO: $i ).
tff(s_JO_definition,axiom,
s_JO = 'fmb_$i_2' ).
tff(declare_s_KW,type,
s_KW: $i ).
tff(s_KW_definition,axiom,
s_KW = 'fmb_$i_2' ).
tff(declare_s_LB,type,
s_LB: $i ).
tff(s_LB_definition,axiom,
s_LB = 'fmb_$i_2' ).
tff(declare_s_OM,type,
s_OM: $i ).
tff(s_OM_definition,axiom,
s_OM = 'fmb_$i_2' ).
tff(declare_s_PS,type,
s_PS: $i ).
tff(s_PS_definition,axiom,
s_PS = 'fmb_$i_2' ).
tff(declare_s_QA,type,
s_QA: $i ).
tff(s_QA_definition,axiom,
s_QA = 'fmb_$i_2' ).
tff(declare_s_SA,type,
s_SA: $i ).
tff(s_SA_definition,axiom,
s_SA = 'fmb_$i_2' ).
tff(declare_s_NT,type,
s_NT: $i ).
tff(s_NT_definition,axiom,
s_NT = 'fmb_$i_2' ).
tff(declare_s_SY,type,
s_SY: $i ).
tff(s_SY_definition,axiom,
s_SY = 'fmb_$i_2' ).
tff(declare_s_TR,type,
s_TR: $i ).
tff(s_TR_definition,axiom,
s_TR = 'fmb_$i_2' ).
tff(declare_s_YE,type,
s_YE: $i ).
tff(s_YE_definition,axiom,
s_YE = 'fmb_$i_2' ).
tff(declare_s_YD,type,
s_YD: $i ).
tff(s_YD_definition,axiom,
s_YD = 'fmb_$i_2' ).
tff(declare_s_AF,type,
s_AF: $i ).
tff(s_AF_definition,axiom,
s_AF = 'fmb_$i_2' ).
tff(declare_s_BD,type,
s_BD: $i ).
tff(s_BD_definition,axiom,
s_BD = 'fmb_$i_2' ).
tff(declare_s_BT,type,
s_BT: $i ).
tff(s_BT_definition,axiom,
s_BT = 'fmb_$i_2' ).
tff(declare_s_IN,type,
s_IN: $i ).
tff(s_IN_definition,axiom,
s_IN = 'fmb_$i_2' ).
tff(declare_s_IR,type,
s_IR: $i ).
tff(s_IR_definition,axiom,
s_IR = 'fmb_$i_2' ).
tff(declare_s_LK,type,
s_LK: $i ).
tff(s_LK_definition,axiom,
s_LK = 'fmb_$i_2' ).
tff(declare_s_MV,type,
s_MV: $i ).
tff(s_MV_definition,axiom,
s_MV = 'fmb_$i_2' ).
tff(declare_s_NP,type,
s_NP: $i ).
tff(s_NP_definition,axiom,
s_NP = 'fmb_$i_2' ).
tff(declare_s_PK,type,
s_PK: $i ).
tff(s_PK_definition,axiom,
s_PK = 'fmb_$i_2' ).
tff(declare_s_g172,type,
s_g172: $i ).
tff(s_g172_definition,axiom,
s_g172 = 'fmb_$i_2' ).
tff(declare_s_DZ,type,
s_DZ: $i ).
tff(s_DZ_definition,axiom,
s_DZ = 'fmb_$i_2' ).
tff(declare_s_EG,type,
s_EG: $i ).
tff(s_EG_definition,axiom,
s_EG = 'fmb_$i_2' ).
tff(declare_s_EH,type,
s_EH: $i ).
tff(s_EH_definition,axiom,
s_EH = 'fmb_$i_2' ).
tff(declare_s_LY,type,
s_LY: $i ).
tff(s_LY_definition,axiom,
s_LY = 'fmb_$i_2' ).
tff(declare_s_MA,type,
s_MA: $i ).
tff(s_MA_definition,axiom,
s_MA = 'fmb_$i_2' ).
tff(declare_s_SD,type,
s_SD: $i ).
tff(s_SD_definition,axiom,
s_SD = 'fmb_$i_2' ).
tff(declare_s_TN,type,
s_TN: $i ).
tff(s_TN_definition,axiom,
s_TN = 'fmb_$i_2' ).
tff(declare_s_AD,type,
s_AD: $i ).
tff(s_AD_definition,axiom,
s_AD = 'fmb_$i_2' ).
tff(declare_s_AL,type,
s_AL: $i ).
tff(s_AL_definition,axiom,
s_AL = 'fmb_$i_2' ).
tff(declare_s_BA,type,
s_BA: $i ).
tff(s_BA_definition,axiom,
s_BA = 'fmb_$i_2' ).
tff(declare_s_ES,type,
s_ES: $i ).
tff(s_ES_definition,axiom,
s_ES = 'fmb_$i_2' ).
tff(declare_s_GI,type,
s_GI: $i ).
tff(s_GI_definition,axiom,
s_GI = 'fmb_$i_2' ).
tff(declare_s_GR,type,
s_GR: $i ).
tff(s_GR_definition,axiom,
s_GR = 'fmb_$i_2' ).
tff(declare_s_HR,type,
s_HR: $i ).
tff(s_HR_definition,axiom,
s_HR = 'fmb_$i_2' ).
tff(declare_s_IT,type,
s_IT: $i ).
tff(s_IT_definition,axiom,
s_IT = 'fmb_$i_2' ).
tff(declare_s_ME,type,
s_ME: $i ).
tff(s_ME_definition,axiom,
s_ME = 'fmb_$i_2' ).
tff(declare_s_MK,type,
s_MK: $i ).
tff(s_MK_definition,axiom,
s_MK = 'fmb_$i_2' ).
tff(declare_s_MT,type,
s_MT: $i ).
tff(s_MT_definition,axiom,
s_MT = 'fmb_$i_2' ).
tff(declare_s_CS,type,
s_CS: $i ).
tff(s_CS_definition,axiom,
s_CS = 'fmb_$i_2' ).
tff(declare_s_RS,type,
s_RS: $i ).
tff(s_RS_definition,axiom,
s_RS = 'fmb_$i_2' ).
tff(declare_s_PT,type,
s_PT: $i ).
tff(s_PT_definition,axiom,
s_PT = 'fmb_$i_2' ).
tff(declare_s_SI,type,
s_SI: $i ).
tff(s_SI_definition,axiom,
s_SI = 'fmb_$i_2' ).
tff(declare_s_SM,type,
s_SM: $i ).
tff(s_SM_definition,axiom,
s_SM = 'fmb_$i_2' ).
tff(declare_s_VA,type,
s_VA: $i ).
tff(s_VA_definition,axiom,
s_VA = 'fmb_$i_2' ).
tff(declare_s_YU,type,
s_YU: $i ).
tff(s_YU_definition,axiom,
s_YU = 'fmb_$i_2' ).
tff(declare_s_BG,type,
s_BG: $i ).
tff(s_BG_definition,axiom,
s_BG = 'fmb_$i_2' ).
tff(declare_s_BY,type,
s_BY: $i ).
tff(s_BY_definition,axiom,
s_BY = 'fmb_$i_2' ).
tff(declare_s_CZ,type,
s_CZ: $i ).
tff(s_CZ_definition,axiom,
s_CZ = 'fmb_$i_2' ).
tff(declare_s_HU,type,
s_HU: $i ).
tff(s_HU_definition,axiom,
s_HU = 'fmb_$i_2' ).
tff(declare_s_MD,type,
s_MD: $i ).
tff(s_MD_definition,axiom,
s_MD = 'fmb_$i_2' ).
tff(declare_s_PL,type,
s_PL: $i ).
tff(s_PL_definition,axiom,
s_PL = 'fmb_$i_2' ).
tff(declare_s_RO,type,
s_RO: $i ).
tff(s_RO_definition,axiom,
s_RO = 'fmb_$i_2' ).
tff(declare_s_RU,type,
s_RU: $i ).
tff(s_RU_definition,axiom,
s_RU = 'fmb_$i_2' ).
tff(declare_s_SU,type,
s_SU: $i ).
tff(s_SU_definition,axiom,
s_SU = 'fmb_$i_2' ).
tff(declare_s_SK,type,
s_SK: $i ).
tff(s_SK_definition,axiom,
s_SK = 'fmb_$i_2' ).
tff(declare_s_UA,type,
s_UA: $i ).
tff(s_UA_definition,axiom,
s_UA = 'fmb_$i_2' ).
tff(declare_s_GG,type,
s_GG: $i ).
tff(s_GG_definition,axiom,
s_GG = 'fmb_$i_2' ).
tff(declare_s_IM,type,
s_IM: $i ).
tff(s_IM_definition,axiom,
s_IM = 'fmb_$i_2' ).
tff(declare_s_JE,type,
s_JE: $i ).
tff(s_JE_definition,axiom,
s_JE = 'fmb_$i_2' ).
tff(declare_s_AX,type,
s_AX: $i ).
tff(s_AX_definition,axiom,
s_AX = 'fmb_$i_2' ).
tff(declare_s_DK,type,
s_DK: $i ).
tff(s_DK_definition,axiom,
s_DK = 'fmb_$i_2' ).
tff(declare_s_EE,type,
s_EE: $i ).
tff(s_EE_definition,axiom,
s_EE = 'fmb_$i_2' ).
tff(declare_s_FI,type,
s_FI: $i ).
tff(s_FI_definition,axiom,
s_FI = 'fmb_$i_2' ).
tff(declare_s_FO,type,
s_FO: $i ).
tff(s_FO_definition,axiom,
s_FO = 'fmb_$i_2' ).
tff(declare_s_GB,type,
s_GB: $i ).
tff(s_GB_definition,axiom,
s_GB = 'fmb_$i_2' ).
tff(declare_s_IE,type,
s_IE: $i ).
tff(s_IE_definition,axiom,
s_IE = 'fmb_$i_2' ).
tff(declare_s_IS,type,
s_IS: $i ).
tff(s_IS_definition,axiom,
s_IS = 'fmb_$i_2' ).
tff(declare_s_LT,type,
s_LT: $i ).
tff(s_LT_definition,axiom,
s_LT = 'fmb_$i_2' ).
tff(declare_s_LV,type,
s_LV: $i ).
tff(s_LV_definition,axiom,
s_LV = 'fmb_$i_2' ).
tff(declare_s_NO,type,
s_NO: $i ).
tff(s_NO_definition,axiom,
s_NO = 'fmb_$i_2' ).
tff(declare_s_SE,type,
s_SE: $i ).
tff(s_SE_definition,axiom,
s_SE = 'fmb_$i_2' ).
tff(declare_s_SJ,type,
s_SJ: $i ).
tff(s_SJ_definition,axiom,
s_SJ = 'fmb_$i_2' ).
tff(declare_s_AT,type,
s_AT: $i ).
tff(s_AT_definition,axiom,
s_AT = 'fmb_$i_2' ).
tff(declare_s_BE,type,
s_BE: $i ).
tff(s_BE_definition,axiom,
s_BE = 'fmb_$i_2' ).
tff(declare_s_CH,type,
s_CH: $i ).
tff(s_CH_definition,axiom,
s_CH = 'fmb_$i_2' ).
tff(declare_s_DE,type,
s_DE: $i ).
tff(s_DE_definition,axiom,
s_DE = 'fmb_$i_2' ).
tff(declare_s_DD,type,
s_DD: $i ).
tff(s_DD_definition,axiom,
s_DD = 'fmb_$i_2' ).
tff(declare_s_FR,type,
s_FR: $i ).
tff(s_FR_definition,axiom,
s_FR = 'fmb_$i_2' ).
tff(declare_s_FX,type,
s_FX: $i ).
tff(s_FX_definition,axiom,
s_FX = 'fmb_$i_2' ).
tff(declare_s_LI,type,
s_LI: $i ).
tff(s_LI_definition,axiom,
s_LI = 'fmb_$i_2' ).
tff(declare_s_LU,type,
s_LU: $i ).
tff(s_LU_definition,axiom,
s_LU = 'fmb_$i_2' ).
tff(declare_s_MC,type,
s_MC: $i ).
tff(s_MC_definition,axiom,
s_MC = 'fmb_$i_2' ).
tff(declare_s_NL,type,
s_NL: $i ).
tff(s_NL_definition,axiom,
s_NL = 'fmb_$i_2' ).
tff(declare_s_g830,type,
s_g830: $i ).
tff(s_g830_definition,axiom,
s_g830 = 'fmb_$i_2' ).
tff(declare_s_AO,type,
s_AO: $i ).
tff(s_AO_definition,axiom,
s_AO = 'fmb_$i_2' ).
tff(declare_s_CD,type,
s_CD: $i ).
tff(s_CD_definition,axiom,
s_CD = 'fmb_$i_2' ).
tff(declare_s_ZR,type,
s_ZR: $i ).
tff(s_ZR_definition,axiom,
s_ZR = 'fmb_$i_2' ).
tff(declare_s_CF,type,
s_CF: $i ).
tff(s_CF_definition,axiom,
s_CF = 'fmb_$i_2' ).
tff(declare_s_CG,type,
s_CG: $i ).
tff(s_CG_definition,axiom,
s_CG = 'fmb_$i_2' ).
tff(declare_s_CM,type,
s_CM: $i ).
tff(s_CM_definition,axiom,
s_CM = 'fmb_$i_2' ).
tff(declare_s_GA,type,
s_GA: $i ).
tff(s_GA_definition,axiom,
s_GA = 'fmb_$i_2' ).
tff(declare_s_GQ,type,
s_GQ: $i ).
tff(s_GQ_definition,axiom,
s_GQ = 'fmb_$i_2' ).
tff(declare_s_ST,type,
s_ST: $i ).
tff(s_ST_definition,axiom,
s_ST = 'fmb_$i_2' ).
tff(declare_s_TD,type,
s_TD: $i ).
tff(s_TD_definition,axiom,
s_TD = 'fmb_$i_2' ).
tff(declare_s_BW,type,
s_BW: $i ).
tff(s_BW_definition,axiom,
s_BW = 'fmb_$i_2' ).
tff(declare_s_LS,type,
s_LS: $i ).
tff(s_LS_definition,axiom,
s_LS = 'fmb_$i_2' ).
tff(declare_s_NA,type,
s_NA: $i ).
tff(s_NA_definition,axiom,
s_NA = 'fmb_$i_2' ).
tff(declare_s_SZ,type,
s_SZ: $i ).
tff(s_SZ_definition,axiom,
s_SZ = 'fmb_$i_2' ).
tff(declare_s_ZA,type,
s_ZA: $i ).
tff(s_ZA_definition,axiom,
s_ZA = 'fmb_$i_2' ).
tff(declare_s_AR,type,
s_AR: $i ).
tff(s_AR_definition,axiom,
s_AR = 'fmb_$i_2' ).
tff(declare_s_BO,type,
s_BO: $i ).
tff(s_BO_definition,axiom,
s_BO = 'fmb_$i_2' ).
tff(declare_s_BR,type,
s_BR: $i ).
tff(s_BR_definition,axiom,
s_BR = 'fmb_$i_2' ).
tff(declare_s_CL,type,
s_CL: $i ).
tff(s_CL_definition,axiom,
s_CL = 'fmb_$i_2' ).
tff(declare_s_CO,type,
s_CO: $i ).
tff(s_CO_definition,axiom,
s_CO = 'fmb_$i_2' ).
tff(declare_s_EC,type,
s_EC: $i ).
tff(s_EC_definition,axiom,
s_EC = 'fmb_$i_2' ).
tff(declare_s_FK,type,
s_FK: $i ).
tff(s_FK_definition,axiom,
s_FK = 'fmb_$i_2' ).
tff(declare_s_GF,type,
s_GF: $i ).
tff(s_GF_definition,axiom,
s_GF = 'fmb_$i_2' ).
tff(declare_s_GY,type,
s_GY: $i ).
tff(s_GY_definition,axiom,
s_GY = 'fmb_$i_2' ).
tff(declare_s_PE,type,
s_PE: $i ).
tff(s_PE_definition,axiom,
s_PE = 'fmb_$i_2' ).
tff(declare_s_PY,type,
s_PY: $i ).
tff(s_PY_definition,axiom,
s_PY = 'fmb_$i_2' ).
tff(declare_s_SR,type,
s_SR: $i ).
tff(s_SR_definition,axiom,
s_SR = 'fmb_$i_2' ).
tff(declare_s_UY,type,
s_UY: $i ).
tff(s_UY_definition,axiom,
s_UY = 'fmb_$i_2' ).
tff(declare_s_VE,type,
s_VE: $i ).
tff(s_VE_definition,axiom,
s_VE = 'fmb_$i_2' ).
tff(declare_s_BM,type,
s_BM: $i ).
tff(s_BM_definition,axiom,
s_BM = 'fmb_$i_2' ).
tff(declare_s_CA,type,
s_CA: $i ).
tff(s_CA_definition,axiom,
s_CA = 'fmb_$i_2' ).
tff(declare_s_GL,type,
s_GL: $i ).
tff(s_GL_definition,axiom,
s_GL = 'fmb_$i_2' ).
tff(declare_s_PM,type,
s_PM: $i ).
tff(s_PM_definition,axiom,
s_PM = 'fmb_$i_2' ).
tff(declare_s_US,type,
s_US: $i ).
tff(s_US_definition,axiom,
s_US = 'fmb_$i_2' ).
tff(declare_s_AG,type,
s_AG: $i ).
tff(s_AG_definition,axiom,
s_AG = 'fmb_$i_2' ).
tff(declare_s_AI,type,
s_AI: $i ).
tff(s_AI_definition,axiom,
s_AI = 'fmb_$i_2' ).
tff(declare_s_AN,type,
s_AN: $i ).
tff(s_AN_definition,axiom,
s_AN = 'fmb_$i_2' ).
tff(declare_s_AW,type,
s_AW: $i ).
tff(s_AW_definition,axiom,
s_AW = 'fmb_$i_2' ).
tff(declare_s_BB,type,
s_BB: $i ).
tff(s_BB_definition,axiom,
s_BB = 'fmb_$i_2' ).
tff(declare_s_BL,type,
s_BL: $i ).
tff(s_BL_definition,axiom,
s_BL = 'fmb_$i_2' ).
tff(declare_s_BS,type,
s_BS: $i ).
tff(s_BS_definition,axiom,
s_BS = 'fmb_$i_2' ).
tff(declare_s_CU,type,
s_CU: $i ).
tff(s_CU_definition,axiom,
s_CU = 'fmb_$i_2' ).
tff(declare_s_DM,type,
s_DM: $i ).
tff(s_DM_definition,axiom,
s_DM = 'fmb_$i_2' ).
tff(declare_s_DO,type,
s_DO: $i ).
tff(s_DO_definition,axiom,
s_DO = 'fmb_$i_2' ).
tff(declare_s_GD,type,
s_GD: $i ).
tff(s_GD_definition,axiom,
s_GD = 'fmb_$i_2' ).
tff(declare_s_GP,type,
s_GP: $i ).
tff(s_GP_definition,axiom,
s_GP = 'fmb_$i_2' ).
tff(declare_s_HT,type,
s_HT: $i ).
tff(s_HT_definition,axiom,
s_HT = 'fmb_$i_2' ).
tff(declare_s_JM,type,
s_JM: $i ).
tff(s_JM_definition,axiom,
s_JM = 'fmb_$i_2' ).
tff(declare_s_KN,type,
s_KN: $i ).
tff(s_KN_definition,axiom,
s_KN = 'fmb_$i_2' ).
tff(declare_s_KY,type,
s_KY: $i ).
tff(s_KY_definition,axiom,
s_KY = 'fmb_$i_2' ).
tff(declare_s_LC,type,
s_LC: $i ).
tff(s_LC_definition,axiom,
s_LC = 'fmb_$i_2' ).
tff(declare_s_MF,type,
s_MF: $i ).
tff(s_MF_definition,axiom,
s_MF = 'fmb_$i_2' ).
tff(declare_s_MQ,type,
s_MQ: $i ).
tff(s_MQ_definition,axiom,
s_MQ = 'fmb_$i_2' ).
tff(declare_s_MS,type,
s_MS: $i ).
tff(s_MS_definition,axiom,
s_MS = 'fmb_$i_2' ).
tff(declare_s_PR,type,
s_PR: $i ).
tff(s_PR_definition,axiom,
s_PR = 'fmb_$i_2' ).
tff(declare_s_TC,type,
s_TC: $i ).
tff(s_TC_definition,axiom,
s_TC = 'fmb_$i_2' ).
tff(declare_s_TT,type,
s_TT: $i ).
tff(s_TT_definition,axiom,
s_TT = 'fmb_$i_2' ).
tff(declare_s_VC,type,
s_VC: $i ).
tff(s_VC_definition,axiom,
s_VC = 'fmb_$i_2' ).
tff(declare_s_VG,type,
s_VG: $i ).
tff(s_VG_definition,axiom,
s_VG = 'fmb_$i_2' ).
tff(declare_s_VI,type,
s_VI: $i ).
tff(s_VI_definition,axiom,
s_VI = 'fmb_$i_2' ).
tff(declare_s_AU,type,
s_AU: $i ).
tff(s_AU_definition,axiom,
s_AU = 'fmb_$i_2' ).
tff(declare_s_NF,type,
s_NF: $i ).
tff(s_NF_definition,axiom,
s_NF = 'fmb_$i_2' ).
tff(declare_s_NZ,type,
s_NZ: $i ).
tff(s_NZ_definition,axiom,
s_NZ = 'fmb_$i_2' ).
tff(declare_s_FJ,type,
s_FJ: $i ).
tff(s_FJ_definition,axiom,
s_FJ = 'fmb_$i_2' ).
tff(declare_s_NC,type,
s_NC: $i ).
tff(s_NC_definition,axiom,
s_NC = 'fmb_$i_2' ).
tff(declare_s_PG,type,
s_PG: $i ).
tff(s_PG_definition,axiom,
s_PG = 'fmb_$i_2' ).
tff(declare_s_SB,type,
s_SB: $i ).
tff(s_SB_definition,axiom,
s_SB = 'fmb_$i_2' ).
tff(declare_s_VU,type,
s_VU: $i ).
tff(s_VU_definition,axiom,
s_VU = 'fmb_$i_2' ).
tff(declare_s_FM,type,
s_FM: $i ).
tff(s_FM_definition,axiom,
s_FM = 'fmb_$i_2' ).
tff(declare_s_GU,type,
s_GU: $i ).
tff(s_GU_definition,axiom,
s_GU = 'fmb_$i_2' ).
tff(declare_s_KI,type,
s_KI: $i ).
tff(s_KI_definition,axiom,
s_KI = 'fmb_$i_2' ).
tff(declare_s_MH,type,
s_MH: $i ).
tff(s_MH_definition,axiom,
s_MH = 'fmb_$i_2' ).
tff(declare_s_MP,type,
s_MP: $i ).
tff(s_MP_definition,axiom,
s_MP = 'fmb_$i_2' ).
tff(declare_s_NR,type,
s_NR: $i ).
tff(s_NR_definition,axiom,
s_NR = 'fmb_$i_2' ).
tff(declare_s_PW,type,
s_PW: $i ).
tff(s_PW_definition,axiom,
s_PW = 'fmb_$i_2' ).
tff(declare_s_AS,type,
s_AS: $i ).
tff(s_AS_definition,axiom,
s_AS = 'fmb_$i_2' ).
tff(declare_s_CK,type,
s_CK: $i ).
tff(s_CK_definition,axiom,
s_CK = 'fmb_$i_2' ).
tff(declare_s_NU,type,
s_NU: $i ).
tff(s_NU_definition,axiom,
s_NU = 'fmb_$i_2' ).
tff(declare_s_PF,type,
s_PF: $i ).
tff(s_PF_definition,axiom,
s_PF = 'fmb_$i_2' ).
tff(declare_s_PN,type,
s_PN: $i ).
tff(s_PN_definition,axiom,
s_PN = 'fmb_$i_2' ).
tff(declare_s_TK,type,
s_TK: $i ).
tff(s_TK_definition,axiom,
s_TK = 'fmb_$i_2' ).
tff(declare_s_TO,type,
s_TO: $i ).
tff(s_TO_definition,axiom,
s_TO = 'fmb_$i_2' ).
tff(declare_s_TV,type,
s_TV: $i ).
tff(s_TV_definition,axiom,
s_TV = 'fmb_$i_2' ).
tff(declare_s_WF,type,
s_WF: $i ).
tff(s_WF_definition,axiom,
s_WF = 'fmb_$i_2' ).
tff(declare_s_WS,type,
s_WS: $i ).
tff(s_WS_definition,axiom,
s_WS = 'fmb_$i_2' ).
tff(declare_ifeq,type,
ifeq: ( $i * $i * $i * $i ) > $i ).
tff(function_ifeq,axiom,
( ( ifeq('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_s_contains,type,
s_contains: ( $i * $i ) > $i ).
tff(function_s_contains,axiom,
( ( s_contains('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( s_contains('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( s_contains('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( s_contains('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
tff(declare_s_partOf,type,
s_partOf: ( $i * $i ) > $i ).
tff(function_s_partOf,axiom,
( ( s_partOf('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( s_partOf('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( s_partOf('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( s_partOf('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MSC018-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 17:43:31 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.28/0.50 % (1193598)Will run a generic schedule for satisfiability detection.
% 0.28/0.50 % (1193605)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3396823238:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.28/0.50 % (1193604)% WARNING: option uhcvi not known.
% 0.28/0.50 % (1193606)dis+10_1_sil=32000:sp=arity:random_seed=2773692497:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.28/0.50 % (1193603)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3277003919_2999 on theBenchmark for (2999ds/0Mi)
% 0.28/0.50 % (1193604)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3832281085:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.28/0.50 % (1193607)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1210351508:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.28/0.50 % (1193608)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2714223940:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.28/0.50 % (1193609)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=487329875:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.28/0.50 % TRYING [1]
% 0.28/0.50 % TRYING [2]
% 0.28/0.50 % Finite Model Found!
% 0.28/0.50 % SZS status Satisfiable for theBenchmark
% 0.28/0.50 % (1193603) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1193598-1193603"...
% 0.28/0.50 % (1193606)Instruction limit reached!
% 0.28/0.50 % (1193606)------------------------------
% 0.28/0.50 % (1193606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/0.50 % (1193606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/0.50 % (1193606)CaDiCaL version: 2.1.3
% 0.28/0.50 % (1193606)Termination reason: Instruction limit
% 0.28/0.50 % (1193606)Termination phase: Saturation
% 0.28/0.50 % (1193606)Time elapsed: 0.049 s
% 0.28/0.50 % (1193606)Peak memory usage: 13 MB
% 0.28/0.50 % (1193606)Instructions burned: 104 (million)
% 0.28/0.50 % (1193603)...printing done.
% 0.28/0.50 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.28/0.50 % (1193603)------------------------------
% 0.28/0.50 % (1193603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/0.50 % (1193603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/0.50 % (1193603)CaDiCaL version: 2.1.3
% 0.28/0.50 % (1193603)Termination reason: Satisfiable
% 0.28/0.50 % (1193603)Time elapsed: 0.049 s
% 0.28/0.50 % (1193603)Peak memory usage: 15 MB
% 0.28/0.50 % (1193603)Instructions burned: 115 (million)
% 0.28/0.50 % (1193598)Success in time 0.092 s
% 0.28/0.50 % Vampire exiting
%------------------------------------------------------------------------------