%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : MSC018+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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 : Fri Sep 25 02:13:54 PM UTC 2026
% Result : CounterSatisfiable 1.18s 0.91s
% Output : FiniteModel 1.18s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( s_WS = "d1"
& s_WF = "d1"
& s_VU = "d1"
& s_VN = "d0"
& s_ZM = "d0"
& s_ZA = "d0"
& s_g419 = "d0"
& s_YU = "d0"
& s_YT = "d0"
& s_YE = "d0"
& s_YD = "d0"
& s_g830 = "d1"
& s_ZW = "d0"
& s_ZR = "d0"
& s_AS = "d1"
& s_AT = "d0"
& s_AR = "d0"
& s_AO = "d0"
& s_AN = "d0"
& s_AM = "d1"
& s_AL = "d0"
& s_AI = "d0"
& s_AG = "d0"
& s_AE = "d0"
& s_AF = "d0"
& s_AD = "d0"
& s_CU = "d0"
& s_CV = "d0"
& s_CS = "d0"
& s_CR = "d0"
& s_CO = "d0"
& s_CM = "d0"
& s_CN = "d1"
& s_CK = "d1"
& s_CL = "d0"
& s_CI = "d0"
& s_CG = "d0"
& s_CH = "d0"
& s_CF = "d0"
& s_CD = "d0"
& s_CA = "d0"
& s_BZ = "d0"
& s_BY = "d1"
& s_BW = "d0"
& s_BT = "d0"
& s_BU = "d0"
& s_BR = "d0"
& s_BS = "d0"
& s_BN = "d0"
& s_BO = "d0"
& s_BL = "d0"
& s_BM = "d0"
& s_BJ = "d0"
& s_BH = "d0"
& s_BI = "d0"
& s_BF = "d0"
& s_BG = "d0"
& s_BD = "d0"
& s_BE = "d0"
& s_BB = "d0"
& s_BA = "d0"
& s_AZ = "d1"
& s_AW = "d0"
& s_AX = "d0"
& s_AU = "d1"
& s_ES = "d0"
& s_ET = "d0"
& s_ER = "d0"
& s_EG = "d0"
& s_EH = "d0"
& s_EE = "d0"
& s_EC = "d0"
& s_DZ = "d0"
& s_DO = "d0"
& s_DM = "d0"
& s_DJ = "d0"
& s_DK = "d0"
& s_DD = "d0"
& s_DE = "d0"
& s_CY = "d0"
& s_CZ = "d0"
& s_GY = "d0"
& s_GW = "d0"
& s_GU = "d1"
& s_GT = "d1"
& s_GQ = "d0"
& s_GR = "d0"
& s_GP = "d0"
& s_GM = "d0"
& s_GN = "d0"
& s_GL = "d0"
& s_GI = "d0"
& s_GG = "d1"
& s_GH = "d0"
& s_GF = "d0"
& s_GE = "d1"
& s_GD = "d0"
& s_GA = "d0"
& s_GB = "d0"
& s_FX = "d0"
& s_FR = "d0"
& s_FO = "d0"
& s_FM = "d1"
& s_FJ = "d1"
& s_FK = "d0"
& s_FI = "d0"
& s_IS = "d0"
& s_IT = "d0"
& s_IQ = "d0"
& s_IR = "d0"
& s_IM = "d0"
& s_IN = "d0"
& s_IL = "d0"
& s_IE = "d0"
& s_ID = "d0"
& s_HT = "d0"
& s_HU = "d0"
& s_HR = "d0"
& s_HN = "d0"
& s_HK = "d1"
& s_KY = "d0"
& s_KZ = "d1"
& s_KW = "d0"
& s_KR = "d1"
& s_KP = "d1"
& s_KM = "d0"
& s_KN = "d0"
& s_KI = "d1"
& s_KG = "d1"
& s_KH = "d0"
& s_KE = "d0"
& s_JP = "d1"
& s_JO = "d0"
& s_JM = "d0"
& s_g039 = "d0"
& s_JE = "d1"
& s_g154 = "d0"
& s_g155 = "d0"
& s_g034 = "d0"
& s_g035 = "d0"
& s_g150 = "d0"
& s_g151 = "d0"
& s_g030 = "d1"
& s_NA = "d0"
& s_MY = "d0"
& s_MZ = "d0"
& s_MW = "d0"
& s_MX = "d0"
& s_MU = "d0"
& s_MV = "d0"
& s_MS = "d0"
& s_MT = "d0"
& s_MQ = "d0"
& s_MR = "d0"
& s_MP = "d1"
& s_MO = "d1"
& s_MM = "d0"
& s_MN = "d1"
& s_MK = "d0"
& s_ML = "d0"
& s_MH = "d1"
& s_MG = "d0"
& s_ME = "d0"
& s_MF = "d0"
& s_MC = "d0"
& s_MD = "d1"
& s_g062 = "d0"
& s_g061 = "d1"
& s_MA = "d0"
& s_LY = "d0"
& s_LV = "d0"
& s_LT = "d0"
& s_LU = "d0"
& s_LR = "d0"
& s_LS = "d0"
& s_LK = "d0"
& s_LI = "d0"
& s_g054 = "d1"
& s_g057 = "d1"
& s_g172 = "d1"
& s_LB = "d0"
& s_LC = "d0"
& s_g053 = "d1"
& s_LA = "d0"
& s_PA = "d0"
& s_g009 = "d1"
& s_OM = "d0"
& s_g003 = "d0"
& s_g005 = "d0"
& s_g001 = "d0"
& s_g002 = "d0"
& s_NZ = "d1"
& s_NU = "d1"
& s_NT = "d0"
& s_NR = "d1"
& s_NP = "d0"
& s_NO = "d0"
& s_NL = "d0"
& s_NI = "d0"
& s_NF = "d1"
& s_NG = "d0"
& s_NE = "d0"
& s_NC = "d1"
& s_RE = "d0"
& s_g029 = "d0"
& s_g021 = "d0"
& s_g142 = "d0"
& s_g143 = "d0"
& s_g145 = "d0"
& s_QA = "d0"
& s_PY = "d0"
& s_PW = "d1"
& s_PT = "d0"
& s_PR = "d0"
& s_g018 = "d0"
& s_PS = "d0"
& s_g019 = "d0"
& s_g014 = "d0"
& s_PN = "d1"
& s_g015 = "d0"
& s_PL = "d0"
& s_PM = "d0"
& s_g017 = "d0"
& s_PK = "d0"
& s_g011 = "d0"
& s_PH = "d0"
& s_g013 = "d0"
& s_PG = "d1"
& s_PF = "d1"
& s_PE = "d0"
& s_TG = "d0"
& s_TD = "d0"
& s_TC = "d0"
& s_SY = "d0"
& s_SZ = "d0"
& s_SU = "d0"
& s_SV = "d0"
& s_ST = "d0"
& s_SR = "d0"
& s_SO = "d0"
& s_SM = "d0"
& s_SN = "d0"
& s_SK = "d0"
& s_SL = "d0"
& s_SI = "d0"
& s_SJ = "d0"
& s_SG = "d0"
& s_SH = "d0"
& s_SE = "d0"
& s_SD = "d1"
& s_SC = "d1"
& s_SB = "d1"
& s_SA = "d0"
& s_RW = "d0"
& s_RU = "d1"
& s_RS = "d0"
& s_RO = "d0"
& s_VI = "d0"
& s_VG = "d0"
& s_VE = "d0"
& s_VC = "d0"
& s_VA = "d0"
& s_UY = "d0"
& s_UZ = "d1"
& s_US = "d0"
& s_UG = "d0"
& s_UA = "d1"
& s_TZ = "d0"
& s_TW = "d1"
& s_TV = "d1"
& s_TT = "d0"
& s_TR = "d0"
& s_TP = "d0"
& s_TO = "d1"
& s_TN = "d0"
& s_TM = "d1"
& s_TL = "d0"
& s_TK = "d1"
& s_TJ = "d1"
& s_TH = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( ~ s_contains("d1","d0")
& s_contains("d0","d1")
& s_contains("d1","d1")
& s_contains("d0","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MSC018+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.35 % Computer : n005.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 01:31:17 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.14/0.42 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.ITQU63RWq0/theBenchmark.cnf 300
% 0.59/0.75 % domain size: 1
% 0.88/0.85 % domain size: 2
% 1.18/0.90 % model found for domain size 2
% 1.18/0.91 % SZS status CounterSatisfiable for theBenchmark
% 1.18/0.91 % SZS output start FiniteModel for theBenchmark
% See solution above
% 1.18/0.99 % FMB4L exiting
%------------------------------------------------------------------------------