%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : MSC018+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 0s % DateTime : Sun Jul 17 22:36:23 EDT 2022 % Result : CounterSatisfiable 0.18s 0.54s % Output : Model 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : MSC018+1 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : darwin -pl 0 -pmc true -to %d %s % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Fri Jul 1 14:48:24 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 Defaulting to tptp format. % 0.18/0.54 SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.54 % 0.18/0.54 MODEL (CONTEXT): % 0.18/0.54 SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.54 -__-v__(=0) % 0.18/0.54 +s_contains(s_g001, s_g002) % 0.18/0.54 +s_contains(s_g001, s_g009) % 0.18/0.54 +s_contains(s_g001, s_g019) % 0.18/0.54 +s_contains(s_g001, s_g142) % 0.18/0.54 +s_contains(s_g001, s_g150) % 0.18/0.54 +s_contains(s_g001, s_g011) % 0.18/0.54 +s_contains(s_g001, s_g014) % 0.18/0.54 +s_contains(s_g001, s_g015) % 0.18/0.54 +s_contains(s_g001, s_g017) % 0.18/0.54 +s_contains(s_g001, s_g018) % 0.18/0.54 +s_contains(s_g001, s_g053) % 0.18/0.54 +s_contains(s_g001, s_g054) % 0.18/0.54 +s_contains(s_g001, s_g057) % 0.18/0.54 +s_contains(s_g001, s_g061) % 0.18/0.54 +s_contains(s_g001, s_g005) % 0.18/0.54 +s_contains(s_g001, s_g013) % 0.18/0.54 +s_contains(s_g001, s_g021) % 0.18/0.54 +s_contains(s_g001, s_g029) % 0.18/0.54 +s_contains(s_g001, s_g003) % 0.18/0.54 +s_contains(s_g001, s_g419) % 0.18/0.54 +s_contains(s_g001, s_g030) % 0.18/0.54 +s_contains(s_g001, s_g035) % 0.18/0.54 +s_contains(s_g001, s_g143) % 0.18/0.54 +s_contains(s_g001, s_g145) % 0.18/0.54 +s_contains(s_g001, s_g034) % 0.18/0.54 +s_contains(s_g001, s_g062) % 0.18/0.54 +s_contains(s_g001, s_g039) % 0.18/0.54 +s_contains(s_g001, s_g151) % 0.18/0.54 +s_contains(s_g001, s_g154) % 0.18/0.54 +s_contains(s_g001, s_g155) % 0.18/0.54 +s_contains(s_g001, s_BF) % 0.18/0.54 +s_contains(s_g001, s_BJ) % 0.18/0.54 +s_contains(s_g001, s_CI) % 0.18/0.54 +s_contains(s_g001, s_CV) % 0.18/0.54 +s_contains(s_g001, s_GH) % 0.18/0.54 +s_contains(s_g001, s_GM) % 0.18/0.54 +s_contains(s_g001, s_GN) % 0.18/0.54 +s_contains(s_g001, s_GW) % 0.18/0.54 +s_contains(s_g001, s_LR) % 0.18/0.54 +s_contains(s_g001, s_ML) % 0.18/0.54 +s_contains(s_g001, s_MR) % 0.18/0.54 +s_contains(s_g001, s_NE) % 0.18/0.54 +s_contains(s_g001, s_NG) % 0.18/0.54 +s_contains(s_g001, s_SH) % 0.18/0.54 +s_contains(s_g001, s_SL) % 0.18/0.54 +s_contains(s_g001, s_SN) % 0.18/0.54 +s_contains(s_g001, s_TG) % 0.18/0.54 +s_contains(s_g001, s_BZ) % 0.18/0.54 +s_contains(s_g001, s_CR) % 0.18/0.54 +s_contains(s_g001, s_GT) % 0.18/0.54 +s_contains(s_g001, s_HN) % 0.18/0.54 +s_contains(s_g001, s_MX) % 0.18/0.54 +s_contains(s_g001, s_NI) % 0.18/0.54 +s_contains(s_g001, s_PA) % 0.18/0.54 +s_contains(s_g001, s_SV) % 0.18/0.54 +s_contains(s_g001, s_BI) % 0.18/0.54 +s_contains(s_g001, s_DJ) % 0.18/0.54 +s_contains(s_g001, s_ER) % 0.18/0.54 +s_contains(s_g001, s_ET) % 0.18/0.54 +s_contains(s_g001, s_KE) % 0.18/0.54 +s_contains(s_g001, s_KM) % 0.18/0.54 +s_contains(s_g001, s_MG) % 0.18/0.54 +s_contains(s_g001, s_MU) % 0.18/0.54 +s_contains(s_g001, s_MW) % 0.18/0.54 +s_contains(s_g001, s_MZ) % 0.18/0.54 +s_contains(s_g001, s_RE) % 0.18/0.54 +s_contains(s_g001, s_RW) % 0.18/0.54 +s_contains(s_g001, s_SC) % 0.18/0.54 +s_contains(s_g001, s_SO) % 0.18/0.54 +s_contains(s_g001, s_TZ) % 0.18/0.54 +s_contains(s_g001, s_UG) % 0.18/0.54 +s_contains(s_g001, s_YT) % 0.18/0.54 +s_contains(s_g001, s_ZM) % 0.18/0.54 +s_contains(s_g001, s_ZW) % 0.18/0.54 +s_contains(s_g001, s_CN) % 0.18/0.54 +s_contains(s_g001, s_HK) % 0.18/0.54 +s_contains(s_g001, s_JP) % 0.18/0.54 +s_contains(s_g001, s_KP) % 0.18/0.54 +s_contains(s_g001, s_KR) % 0.18/0.54 +s_contains(s_g001, s_MN) % 0.18/0.54 +s_contains(s_g001, s_MO) % 0.18/0.54 +s_contains(s_g001, s_TW) % 0.18/0.54 +s_contains(s_g001, s_BN) % 0.18/0.54 +s_contains(s_g001, s_ID) % 0.18/0.54 +s_contains(s_g001, s_KH) % 0.18/0.54 +s_contains(s_g001, s_LA) % 0.18/0.54 +s_contains(s_g001, s_MM) % 0.18/0.54 +s_contains(s_g001, s_BU) % 0.18/0.54 +s_contains(s_g001, s_MY) % 0.18/0.54 +s_contains(s_g001, s_PH) % 0.18/0.54 +s_contains(s_g001, s_SG) % 0.18/0.54 +s_contains(s_g001, s_TH) % 0.18/0.54 +s_contains(s_g001, s_TL) % 0.18/0.54 +s_contains(s_g001, s_TP) % 0.18/0.54 +s_contains(s_g001, s_VN) % 0.18/0.54 +s_contains(s_g001, s_TM) % 0.18/0.54 +s_contains(s_g001, s_TJ) % 0.18/0.54 +s_contains(s_g001, s_KG) % 0.18/0.54 +s_contains(s_g001, s_KZ) % 0.18/0.54 +s_contains(s_g001, s_UZ) % 0.18/0.54 +s_contains(s_g001, s_AE) % 0.18/0.54 +s_contains(s_g001, s_AM) % 0.18/0.54 +s_contains(s_g001, s_AZ) % 0.18/0.54 +s_contains(s_g001, s_BH) % 0.18/0.54 +s_contains(s_g001, s_CY) % 0.18/0.54 +s_contains(s_g001, s_GE) % 0.18/0.54 +s_contains(s_g001, s_IL) % 0.18/0.54 +s_contains(s_g001, s_IQ) % 0.18/0.54 +s_contains(s_g001, s_JO) % 0.18/0.54 +s_contains(s_g001, s_KW) % 0.18/0.54 +s_contains(s_g001, s_LB) % 0.18/0.54 +s_contains(s_g001, s_OM) % 0.18/0.54 +s_contains(s_g001, s_PS) % 0.18/0.54 +s_contains(s_g001, s_QA) % 0.18/0.54 +s_contains(s_g001, s_SA) % 0.18/0.54 +s_contains(s_g001, s_NT) % 0.18/0.54 +s_contains(s_g001, s_SY) % 0.18/0.54 +s_contains(s_g001, s_TR) % 0.18/0.54 +s_contains(s_g001, s_YE) % 0.18/0.54 +s_contains(s_g001, s_YD) % 0.18/0.54 +s_contains(s_g001, s_AF) % 0.18/0.54 +s_contains(s_g001, s_BD) % 0.18/0.54 +s_contains(s_g001, s_BT) % 0.18/0.54 +s_contains(s_g001, s_IN) % 0.18/0.54 +s_contains(s_g001, s_IR) % 0.18/0.54 +s_contains(s_g001, s_LK) % 0.18/0.54 +s_contains(s_g001, s_MV) % 0.18/0.54 +s_contains(s_g001, s_NP) % 0.18/0.54 +s_contains(s_g001, s_PK) % 0.18/0.54 +s_contains(s_g001, s_DZ) % 0.18/0.54 +s_contains(s_g001, s_EG) % 0.18/0.54 +s_contains(s_g001, s_EH) % 0.18/0.54 +s_contains(s_g001, s_LY) % 0.18/0.54 +s_contains(s_g001, s_MA) % 0.18/0.54 +s_contains(s_g001, s_SD) % 0.18/0.54 +s_contains(s_g001, s_TN) % 0.18/0.54 +s_contains(s_g001, s_AD) % 0.18/0.54 +s_contains(s_g001, s_AL) % 0.18/0.54 +s_contains(s_g001, s_BA) % 0.18/0.54 +s_contains(s_g001, s_ES) % 0.18/0.54 +s_contains(s_g001, s_GI) % 0.18/0.54 +s_contains(s_g001, s_GR) % 0.18/0.54 +s_contains(s_g001, s_HR) % 0.18/0.54 +s_contains(s_g001, s_IT) % 0.18/0.54 +s_contains(s_g001, s_ME) % 0.18/0.54 +s_contains(s_g001, s_MK) % 0.18/0.54 +s_contains(s_g001, s_MT) % 0.18/0.54 +s_contains(s_g001, s_CS) % 0.18/0.54 +s_contains(s_g001, s_RS) % 0.18/0.54 +s_contains(s_g001, s_PT) % 0.18/0.54 +s_contains(s_g001, s_SI) % 0.18/0.54 +s_contains(s_g001, s_SM) % 0.18/0.54 +s_contains(s_g001, s_VA) % 0.18/0.54 +s_contains(s_g001, s_YU) % 0.18/0.54 +s_contains(s_g001, s_BG) % 0.18/0.54 +s_contains(s_g001, s_BY) % 0.18/0.54 +s_contains(s_g001, s_CZ) % 0.18/0.54 +s_contains(s_g001, s_HU) % 0.18/0.54 +s_contains(s_g001, s_MD) % 0.18/0.54 +s_contains(s_g001, s_PL) % 0.18/0.54 +s_contains(s_g001, s_RO) % 0.18/0.54 +s_contains(s_g001, s_RU) % 0.18/0.54 +s_contains(s_g001, s_SU) % 0.18/0.54 +s_contains(s_g001, s_SK) % 0.18/0.54 +s_contains(s_g001, s_UA) % 0.18/0.54 +s_contains(s_g001, s_GG) % 0.18/0.54 +s_contains(s_g001, s_IM) % 0.18/0.54 +s_contains(s_g001, s_JE) % 0.18/0.54 +s_contains(s_g001, s_AX) % 0.18/0.54 +s_contains(s_g001, s_DK) % 0.18/0.54 +s_contains(s_g001, s_EE) % 0.18/0.54 +s_contains(s_g001, s_FI) % 0.18/0.54 +s_contains(s_g001, s_FO) % 0.18/0.54 +s_contains(s_g001, s_GB) % 0.18/0.54 +s_contains(s_g001, s_IE) % 0.18/0.54 +s_contains(s_g001, s_IS) % 0.18/0.54 +s_contains(s_g001, s_LT) % 0.18/0.54 +s_contains(s_g001, s_LV) % 0.18/0.54 +s_contains(s_g001, s_NO) % 0.18/0.54 +s_contains(s_g001, s_SE) % 0.18/0.54 +s_contains(s_g001, s_SJ) % 0.18/0.54 +s_contains(s_g001, s_AT) % 0.18/0.54 +s_contains(s_g001, s_BE) % 0.18/0.54 +s_contains(s_g001, s_CH) % 0.18/0.54 +s_contains(s_g001, s_DE) % 0.18/0.54 +s_contains(s_g001, s_DD) % 0.18/0.54 +s_contains(s_g001, s_FR) % 0.18/0.54 +s_contains(s_g001, s_FX) % 0.18/0.54 +s_contains(s_g001, s_LI) % 0.18/0.54 +s_contains(s_g001, s_LU) % 0.18/0.54 +s_contains(s_g001, s_MC) % 0.18/0.54 +s_contains(s_g001, s_NL) % 0.18/0.54 +s_contains(s_g001, s_AO) % 0.18/0.54 +s_contains(s_g001, s_CD) % 0.18/0.54 +s_contains(s_g001, s_ZR) % 0.18/0.54 +s_contains(s_g001, s_CF) % 0.18/0.54 +s_contains(s_g001, s_CG) % 0.18/0.54 +s_contains(s_g001, s_CM) % 0.18/0.54 +s_contains(s_g001, s_GA) % 0.18/0.54 +s_contains(s_g001, s_GQ) % 0.18/0.54 +s_contains(s_g001, s_ST) % 0.18/0.54 +s_contains(s_g001, s_TD) % 0.18/0.54 +s_contains(s_g001, s_BW) % 0.18/0.54 +s_contains(s_g001, s_LS) % 0.18/0.54 +s_contains(s_g001, s_NA) % 0.18/0.54 +s_contains(s_g001, s_SZ) % 0.18/0.54 +s_contains(s_g001, s_ZA) % 0.18/0.54 +s_contains(s_g001, s_AR) % 0.18/0.54 +s_contains(s_g001, s_BO) % 0.18/0.54 +s_contains(s_g001, s_BR) % 0.18/0.54 +s_contains(s_g001, s_CL) % 0.18/0.54 +s_contains(s_g001, s_CO) % 0.18/0.54 +s_contains(s_g001, s_EC) % 0.18/0.54 +s_contains(s_g001, s_FK) % 0.18/0.54 +s_contains(s_g001, s_GF) % 0.18/0.54 +s_contains(s_g001, s_GY) % 0.18/0.54 +s_contains(s_g001, s_PE) % 0.18/0.54 +s_contains(s_g001, s_PY) % 0.18/0.54 +s_contains(s_g001, s_SR) % 0.18/0.54 +s_contains(s_g001, s_UY) % 0.18/0.54 +s_contains(s_g001, s_VE) % 0.18/0.54 +s_contains(s_g001, s_BM) % 0.18/0.54 +s_contains(s_g001, s_CA) % 0.18/0.54 +s_contains(s_g001, s_GL) % 0.18/0.54 +s_contains(s_g001, s_PM) % 0.18/0.54 +s_contains(s_g001, s_US) % 0.18/0.54 +s_contains(s_g001, s_AG) % 0.18/0.54 +s_contains(s_g001, s_AI) % 0.18/0.54 +s_contains(s_g001, s_AN) % 0.18/0.54 +s_contains(s_g001, s_AW) % 0.18/0.54 +s_contains(s_g001, s_BB) % 0.18/0.54 +s_contains(s_g001, s_BL) % 0.18/0.54 +s_contains(s_g001, s_BS) % 0.18/0.54 +s_contains(s_g001, s_CU) % 0.18/0.54 +s_contains(s_g001, s_DM) % 0.18/0.54 +s_contains(s_g001, s_DO) % 0.18/0.54 +s_contains(s_g001, s_GD) % 0.18/0.54 +s_contains(s_g001, s_GP) % 0.18/0.54 +s_contains(s_g001, s_HT) % 0.18/0.54 +s_contains(s_g001, s_JM) % 0.18/0.54 +s_contains(s_g001, s_KN) % 0.18/0.54 +s_contains(s_g001, s_KY) % 0.18/0.54 +s_contains(s_g001, s_LC) % 0.18/0.54 +s_contains(s_g001, s_MF) % 0.18/0.54 +s_contains(s_g001, s_MQ) % 0.18/0.54 +s_contains(s_g001, s_MS) % 0.18/0.54 +s_contains(s_g001, s_PR) % 0.18/0.54 +s_contains(s_g001, s_TC) % 0.18/0.54 +s_contains(s_g001, s_TT) % 0.18/0.54 +s_contains(s_g001, s_VC) % 0.18/0.54 +s_contains(s_g001, s_VG) % 0.18/0.54 +s_contains(s_g001, s_VI) % 0.18/0.54 +s_contains(s_g001, s_AU) % 0.18/0.54 +s_contains(s_g001, s_NF) % 0.18/0.54 +s_contains(s_g001, s_NZ) % 0.18/0.54 +s_contains(s_g001, s_FJ) % 0.18/0.54 +s_contains(s_g001, s_NC) % 0.18/0.54 +s_contains(s_g001, s_PG) % 0.18/0.54 +s_contains(s_g001, s_SB) % 0.18/0.54 +s_contains(s_g001, s_VU) % 0.18/0.54 +s_contains(s_g001, s_FM) % 0.18/0.54 +s_contains(s_g001, s_GU) % 0.18/0.54 +s_contains(s_g001, s_KI) % 0.18/0.54 +s_contains(s_g001, s_MH) % 0.18/0.54 +s_contains(s_g001, s_MP) % 0.18/0.54 +s_contains(s_g001, s_NR) % 0.18/0.54 +s_contains(s_g001, s_PW) % 0.18/0.54 +s_contains(s_g001, s_AS) % 0.18/0.54 +s_contains(s_g001, s_CK) % 0.18/0.54 +s_contains(s_g001, s_NU) % 0.18/0.54 +s_contains(s_g001, s_PF) % 0.18/0.54 +s_contains(s_g001, s_PN) % 0.18/0.54 +s_contains(s_g001, s_TK) % 0.18/0.54 +s_contains(s_g001, s_TO) % 0.18/0.54 +s_contains(s_g001, s_TV) % 0.18/0.54 +s_contains(s_g001, s_WF) % 0.18/0.54 +s_contains(s_g001, s_WS) % 0.18/0.54 +s_contains(s_g002, s_g011) % 0.18/0.54 +s_contains(s_g002, s_g014) % 0.18/0.54 +s_contains(s_g002, s_g015) % 0.18/0.54 +s_contains(s_g002, s_g017) % 0.18/0.54 +s_contains(s_g002, s_g018) % 0.18/0.54 +s_contains(s_g002, s_BF) % 0.18/0.54 +s_contains(s_g002, s_BJ) % 0.18/0.54 +s_contains(s_g002, s_CI) % 0.18/0.54 +s_contains(s_g002, s_CV) % 0.18/0.54 +s_contains(s_g002, s_GH) % 0.18/0.54 +s_contains(s_g002, s_GM) % 0.18/0.54 +s_contains(s_g002, s_GN) % 0.18/0.54 +s_contains(s_g002, s_GW) % 0.18/0.54 +s_contains(s_g002, s_LR) % 0.18/0.54 +s_contains(s_g002, s_ML) % 0.18/0.54 +s_contains(s_g002, s_MR) % 0.18/0.54 +s_contains(s_g002, s_NE) % 0.18/0.54 +s_contains(s_g002, s_NG) % 0.18/0.54 +s_contains(s_g002, s_SH) % 0.18/0.54 +s_contains(s_g002, s_SL) % 0.18/0.54 +s_contains(s_g002, s_SN) % 0.18/0.54 +s_contains(s_g002, s_TG) % 0.18/0.54 +s_contains(s_g002, s_BI) % 0.18/0.54 +s_contains(s_g002, s_DJ) % 0.18/0.54 +s_contains(s_g002, s_ER) % 0.18/0.54 +s_contains(s_g002, s_ET) % 0.18/0.54 +s_contains(s_g002, s_KE) % 0.18/0.54 +s_contains(s_g002, s_KM) % 0.18/0.54 +s_contains(s_g002, s_MG) % 0.18/0.54 +s_contains(s_g002, s_MU) % 0.18/0.54 +s_contains(s_g002, s_MW) % 0.18/0.54 +s_contains(s_g002, s_MZ) % 0.18/0.54 +s_contains(s_g002, s_RE) % 0.18/0.54 +s_contains(s_g002, s_RW) % 0.18/0.54 +s_contains(s_g002, s_SC) % 0.18/0.54 +s_contains(s_g002, s_SO) % 0.18/0.54 +s_contains(s_g002, s_TZ) % 0.18/0.54 +s_contains(s_g002, s_UG) % 0.18/0.54 +s_contains(s_g002, s_YT) % 0.18/0.54 +s_contains(s_g002, s_ZM) % 0.18/0.54 +s_contains(s_g002, s_ZW) % 0.18/0.54 +s_contains(s_g002, s_DZ) % 0.18/0.54 +s_contains(s_g002, s_EG) % 0.18/0.54 +s_contains(s_g002, s_EH) % 0.18/0.54 +s_contains(s_g002, s_LY) % 0.18/0.54 +s_contains(s_g002, s_MA) % 0.18/0.54 +s_contains(s_g002, s_SD) % 0.18/0.54 +s_contains(s_g002, s_TN) % 0.18/0.54 +s_contains(s_g002, s_AO) % 0.18/0.54 +s_contains(s_g002, s_CD) % 0.18/0.54 +s_contains(s_g002, s_ZR) % 0.18/0.54 +s_contains(s_g002, s_CF) % 0.18/0.54 +s_contains(s_g002, s_CG) % 0.18/0.54 +s_contains(s_g002, s_CM) % 0.18/0.54 +s_contains(s_g002, s_GA) % 0.18/0.54 +s_contains(s_g002, s_GQ) % 0.18/0.54 +s_contains(s_g002, s_ST) % 0.18/0.54 +s_contains(s_g002, s_TD) % 0.18/0.54 +s_contains(s_g002, s_BW) % 0.18/0.54 +s_contains(s_g002, s_LS) % 0.18/0.54 +s_contains(s_g002, s_NA) % 0.18/0.54 +s_contains(s_g002, s_SZ) % 0.18/0.54 +s_contains(s_g002, s_ZA) % 0.18/0.54 +s_contains(s_g009, s_g053) % 0.18/0.54 +s_contains(s_g009, s_g054) % 0.18/0.54 +s_contains(s_g009, s_g057) % 0.18/0.54 +s_contains(s_g009, s_g061) % 0.18/0.54 +s_contains(s_g009, s_AU) % 0.18/0.54 +s_contains(s_g009, s_NF) % 0.18/0.54 +s_contains(s_g009, s_NZ) % 0.18/0.54 +s_contains(s_g009, s_FJ) % 0.18/0.54 +s_contains(s_g009, s_NC) % 0.18/0.54 +s_contains(s_g009, s_PG) % 0.18/0.54 +s_contains(s_g009, s_SB) % 0.18/0.54 +s_contains(s_g009, s_VU) % 0.18/0.54 +s_contains(s_g009, s_FM) % 0.18/0.54 +s_contains(s_g009, s_GU) % 0.18/0.54 +s_contains(s_g009, s_KI) % 0.18/0.54 +s_contains(s_g009, s_MH) % 0.18/0.54 +s_contains(s_g009, s_MP) % 0.18/0.54 +s_contains(s_g009, s_NR) % 0.18/0.54 +s_contains(s_g009, s_PW) % 0.18/0.54 +s_contains(s_g009, s_AS) % 0.18/0.54 +s_contains(s_g009, s_CK) % 0.18/0.54 +s_contains(s_g009, s_NU) % 0.18/0.54 +s_contains(s_g009, s_PF) % 0.18/0.54 +s_contains(s_g009, s_PN) % 0.18/0.54 +s_contains(s_g009, s_TK) % 0.18/0.54 +s_contains(s_g009, s_TO) % 0.18/0.54 +s_contains(s_g009, s_TV) % 0.18/0.54 +s_contains(s_g009, s_WF) % 0.18/0.54 +s_contains(s_g009, s_WS) % 0.18/0.54 +s_contains(s_g019, s_g005) % 0.18/0.54 +s_contains(s_g019, s_g013) % 0.18/0.54 +s_contains(s_g019, s_g021) % 0.18/0.54 +s_contains(s_g019, s_g029) % 0.18/0.54 +s_contains(s_g019, s_g003) % 0.18/0.54 +s_contains(s_g019, s_g419) % 0.18/0.54 +s_contains(s_g019, s_BZ) % 0.18/0.54 +s_contains(s_g019, s_CR) % 0.18/0.54 +s_contains(s_g019, s_GT) % 0.18/0.54 +s_contains(s_g019, s_HN) % 0.18/0.54 +s_contains(s_g019, s_MX) % 0.18/0.54 +s_contains(s_g019, s_NI) % 0.18/0.54 +s_contains(s_g019, s_PA) % 0.18/0.54 +s_contains(s_g019, s_SV) % 0.18/0.54 +s_contains(s_g019, s_AR) % 0.18/0.54 +s_contains(s_g019, s_BO) % 0.18/0.54 +s_contains(s_g019, s_BR) % 0.18/0.54 +s_contains(s_g019, s_CL) % 0.18/0.54 +s_contains(s_g019, s_CO) % 0.18/0.54 +s_contains(s_g019, s_EC) % 0.18/0.54 +s_contains(s_g019, s_FK) % 0.18/0.54 +s_contains(s_g019, s_GF) % 0.18/0.54 +s_contains(s_g019, s_GY) % 0.18/0.54 +s_contains(s_g019, s_PE) % 0.18/0.54 +s_contains(s_g019, s_PY) % 0.18/0.54 +s_contains(s_g019, s_SR) % 0.18/0.54 +s_contains(s_g019, s_UY) % 0.18/0.54 +s_contains(s_g019, s_VE) % 0.18/0.54 +s_contains(s_g019, s_BM) % 0.18/0.54 +s_contains(s_g019, s_CA) % 0.18/0.54 +s_contains(s_g019, s_GL) % 0.18/0.54 +s_contains(s_g019, s_PM) % 0.18/0.54 +s_contains(s_g019, s_US) % 0.18/0.54 +s_contains(s_g019, s_AG) % 0.18/0.54 +s_contains(s_g019, s_AI) % 0.18/0.54 +s_contains(s_g019, s_AN) % 0.18/0.54 +s_contains(s_g019, s_AW) % 0.18/0.54 +s_contains(s_g019, s_BB) % 0.18/0.54 +s_contains(s_g019, s_BL) % 0.18/0.54 +s_contains(s_g019, s_BS) % 0.18/0.54 +s_contains(s_g019, s_CU) % 0.18/0.54 +s_contains(s_g019, s_DM) % 0.18/0.54 +s_contains(s_g019, s_DO) % 0.18/0.54 +s_contains(s_g019, s_GD) % 0.18/0.54 +s_contains(s_g019, s_GP) % 0.18/0.54 +s_contains(s_g019, s_HT) % 0.18/0.54 +s_contains(s_g019, s_JM) % 0.18/0.54 +s_contains(s_g019, s_KN) % 0.18/0.54 +s_contains(s_g019, s_KY) % 0.18/0.54 +s_contains(s_g019, s_LC) % 0.18/0.54 +s_contains(s_g019, s_MF) % 0.18/0.54 +s_contains(s_g019, s_MQ) % 0.18/0.54 +s_contains(s_g019, s_MS) % 0.18/0.54 +s_contains(s_g019, s_PR) % 0.18/0.54 +s_contains(s_g019, s_TC) % 0.18/0.54 +s_contains(s_g019, s_TT) % 0.18/0.54 +s_contains(s_g019, s_VC) % 0.18/0.54 +s_contains(s_g019, s_VG) % 0.18/0.54 +s_contains(s_g019, s_VI) % 0.18/0.54 +s_contains(s_g142, s_g030) % 0.18/0.54 +s_contains(s_g142, s_g035) % 0.18/0.54 +s_contains(s_g142, s_g143) % 0.18/0.54 +s_contains(s_g142, s_g145) % 0.18/0.54 +s_contains(s_g142, s_g034) % 0.18/0.54 +s_contains(s_g142, s_g062) % 0.18/0.54 +s_contains(s_g142, s_CN) % 0.18/0.54 +s_contains(s_g142, s_HK) % 0.18/0.54 +s_contains(s_g142, s_JP) % 0.18/0.54 +s_contains(s_g142, s_KP) % 0.18/0.54 +s_contains(s_g142, s_KR) % 0.18/0.54 +s_contains(s_g142, s_MN) % 0.18/0.54 +s_contains(s_g142, s_MO) % 0.18/0.54 +s_contains(s_g142, s_TW) % 0.18/0.54 +s_contains(s_g142, s_BN) % 0.18/0.54 +s_contains(s_g142, s_ID) % 0.18/0.54 +s_contains(s_g142, s_KH) % 0.18/0.54 +s_contains(s_g142, s_LA) % 0.18/0.54 +s_contains(s_g142, s_MM) % 0.18/0.54 +s_contains(s_g142, s_BU) % 0.18/0.54 +s_contains(s_g142, s_MY) % 0.18/0.54 +s_contains(s_g142, s_PH) % 0.18/0.54 +s_contains(s_g142, s_SG) % 0.18/0.54 +s_contains(s_g142, s_TH) % 0.18/0.54 +s_contains(s_g142, s_TL) % 0.18/0.54 +s_contains(s_g142, s_TP) % 0.18/0.54 +s_contains(s_g142, s_VN) % 0.18/0.54 +s_contains(s_g142, s_TM) % 0.18/0.54 +s_contains(s_g142, s_TJ) % 0.18/0.54 +s_contains(s_g142, s_KG) % 0.18/0.54 +s_contains(s_g142, s_KZ) % 0.18/0.54 +s_contains(s_g142, s_UZ) % 0.18/0.54 +s_contains(s_g142, s_AE) % 0.18/0.54 +s_contains(s_g142, s_AM) % 0.18/0.54 +s_contains(s_g142, s_AZ) % 0.18/0.54 +s_contains(s_g142, s_BH) % 0.18/0.54 +s_contains(s_g142, s_CY) % 0.18/0.54 +s_contains(s_g142, s_GE) % 0.18/0.54 +s_contains(s_g142, s_IL) % 0.18/0.54 +s_contains(s_g142, s_IQ) % 0.18/0.54 +s_contains(s_g142, s_JO) % 0.18/0.54 +s_contains(s_g142, s_KW) % 0.18/0.54 +s_contains(s_g142, s_LB) % 0.18/0.54 +s_contains(s_g142, s_OM) % 0.18/0.54 +s_contains(s_g142, s_PS) % 0.18/0.54 +s_contains(s_g142, s_QA) % 0.18/0.54 +s_contains(s_g142, s_SA) % 0.18/0.54 +s_contains(s_g142, s_NT) % 0.18/0.54 +s_contains(s_g142, s_SY) % 0.18/0.54 +s_contains(s_g142, s_TR) % 0.18/0.54 +s_contains(s_g142, s_YE) % 0.18/0.54 +s_contains(s_g142, s_YD) % 0.18/0.54 +s_contains(s_g142, s_AF) % 0.18/0.54 +s_contains(s_g142, s_BD) % 0.18/0.54 +s_contains(s_g142, s_BT) % 0.18/0.54 +s_contains(s_g142, s_IN) % 0.18/0.54 +s_contains(s_g142, s_IR) % 0.18/0.54 +s_contains(s_g142, s_LK) % 0.18/0.54 +s_contains(s_g142, s_MV) % 0.18/0.54 +s_contains(s_g142, s_NP) % 0.18/0.54 +s_contains(s_g142, s_PK) % 0.18/0.54 +s_contains(s_g150, s_g039) % 0.18/0.54 +s_contains(s_g150, s_g151) % 0.18/0.54 +s_contains(s_g150, s_g154) % 0.18/0.54 +s_contains(s_g150, s_g155) % 0.18/0.54 +s_contains(s_g150, s_AD) % 0.18/0.54 +s_contains(s_g150, s_AL) % 0.18/0.54 +s_contains(s_g150, s_BA) % 0.18/0.54 +s_contains(s_g150, s_ES) % 0.18/0.54 +s_contains(s_g150, s_GI) % 0.18/0.54 +s_contains(s_g150, s_GR) % 0.18/0.54 +s_contains(s_g150, s_HR) % 0.18/0.54 +s_contains(s_g150, s_IT) % 0.18/0.54 +s_contains(s_g150, s_ME) % 0.18/0.54 +s_contains(s_g150, s_MK) % 0.18/0.54 +s_contains(s_g150, s_MT) % 0.18/0.54 +s_contains(s_g150, s_CS) % 0.18/0.54 +s_contains(s_g150, s_RS) % 0.18/0.54 +s_contains(s_g150, s_PT) % 0.18/0.54 +s_contains(s_g150, s_SI) % 0.18/0.54 +s_contains(s_g150, s_SM) % 0.18/0.54 +s_contains(s_g150, s_VA) % 0.18/0.54 +s_contains(s_g150, s_YU) % 0.18/0.54 +s_contains(s_g150, s_BG) % 0.18/0.54 +s_contains(s_g150, s_BY) % 0.18/0.54 +s_contains(s_g150, s_CZ) % 0.18/0.54 +s_contains(s_g150, s_HU) % 0.18/0.54 +s_contains(s_g150, s_MD) % 0.18/0.54 +s_contains(s_g150, s_PL) % 0.18/0.54 +s_contains(s_g150, s_RO) % 0.18/0.54 +s_contains(s_g150, s_RU) % 0.18/0.54 +s_contains(s_g150, s_SU) % 0.18/0.54 +s_contains(s_g150, s_SK) % 0.18/0.54 +s_contains(s_g150, s_UA) % 0.18/0.54 +s_contains(s_g150, s_GG) % 0.18/0.54 +s_contains(s_g150, s_IM) % 0.18/0.54 +s_contains(s_g150, s_JE) % 0.18/0.54 +s_contains(s_g150, s_AX) % 0.18/0.54 +s_contains(s_g150, s_DK) % 0.18/0.54 +s_contains(s_g150, s_EE) % 0.18/0.54 +s_contains(s_g150, s_FI) % 0.18/0.54 +s_contains(s_g150, s_FO) % 0.18/0.54 +s_contains(s_g150, s_GB) % 0.18/0.54 +s_contains(s_g150, s_IE) % 0.18/0.54 +s_contains(s_g150, s_IS) % 0.18/0.54 +s_contains(s_g150, s_LT) % 0.18/0.54 +s_contains(s_g150, s_LV) % 0.18/0.54 +s_contains(s_g150, s_NO) % 0.18/0.54 +s_contains(s_g150, s_SE) % 0.18/0.54 +s_contains(s_g150, s_SJ) % 0.18/0.54 +s_contains(s_g150, s_AT) % 0.18/0.54 +s_contains(s_g150, s_BE) % 0.18/0.54 +s_contains(s_g150, s_CH) % 0.18/0.54 +s_contains(s_g150, s_DE) % 0.18/0.54 +s_contains(s_g150, s_DD) % 0.18/0.54 +s_contains(s_g150, s_FR) % 0.18/0.54 +s_contains(s_g150, s_FX) % 0.18/0.54 +s_contains(s_g150, s_LI) % 0.18/0.54 +s_contains(s_g150, s_LU) % 0.18/0.54 +s_contains(s_g150, s_MC) % 0.18/0.54 +s_contains(s_g150, s_NL) % 0.18/0.54 +s_contains(s_g011, s_BF) % 0.18/0.54 +s_contains(s_g011, s_BJ) % 0.18/0.54 +s_contains(s_g011, s_CI) % 0.18/0.54 +s_contains(s_g011, s_CV) % 0.18/0.54 +s_contains(s_g011, s_GH) % 0.18/0.54 +s_contains(s_g011, s_GM) % 0.18/0.54 +s_contains(s_g011, s_GN) % 0.18/0.54 +s_contains(s_g011, s_GW) % 0.18/0.54 +s_contains(s_g011, s_LR) % 0.18/0.54 +s_contains(s_g011, s_ML) % 0.18/0.54 +s_contains(s_g011, s_MR) % 0.18/0.54 +s_contains(s_g011, s_NE) % 0.18/0.54 +s_contains(s_g011, s_NG) % 0.18/0.54 +s_contains(s_g011, s_SH) % 0.18/0.54 +s_contains(s_g011, s_SL) % 0.18/0.54 +s_contains(s_g011, s_SN) % 0.18/0.54 +s_contains(s_g011, s_TG) % 0.18/0.54 +s_contains(s_g014, s_BI) % 0.18/0.54 +s_contains(s_g014, s_DJ) % 0.18/0.54 +s_contains(s_g014, s_ER) % 0.18/0.54 +s_contains(s_g014, s_ET) % 0.18/0.54 +s_contains(s_g014, s_KE) % 0.18/0.54 +s_contains(s_g014, s_KM) % 0.18/0.54 +s_contains(s_g014, s_MG) % 0.18/0.54 +s_contains(s_g014, s_MU) % 0.18/0.54 +s_contains(s_g014, s_MW) % 0.18/0.54 +s_contains(s_g014, s_MZ) % 0.18/0.54 +s_contains(s_g014, s_RE) % 0.18/0.54 +s_contains(s_g014, s_RW) % 0.18/0.54 +s_contains(s_g014, s_SC) % 0.18/0.54 +s_contains(s_g014, s_SO) % 0.18/0.54 +s_contains(s_g014, s_TZ) % 0.18/0.54 +s_contains(s_g014, s_UG) % 0.18/0.54 +s_contains(s_g014, s_YT) % 0.18/0.54 +s_contains(s_g014, s_ZM) % 0.18/0.54 +s_contains(s_g014, s_ZW) % 0.18/0.54 +s_contains(s_g015, s_DZ) % 0.18/0.54 +s_contains(s_g015, s_EG) % 0.18/0.54 +s_contains(s_g015, s_EH) % 0.18/0.54 +s_contains(s_g015, s_LY) % 0.18/0.54 +s_contains(s_g015, s_MA) % 0.18/0.54 +s_contains(s_g015, s_SD) % 0.18/0.54 +s_contains(s_g015, s_TN) % 0.18/0.54 +s_contains(s_g017, s_AO) % 0.18/0.54 +s_contains(s_g017, s_CD) % 0.18/0.54 +s_contains(s_g017, s_ZR) % 0.18/0.54 +s_contains(s_g017, s_CF) % 0.18/0.54 +s_contains(s_g017, s_CG) % 0.18/0.54 +s_contains(s_g017, s_CM) % 0.18/0.54 +s_contains(s_g017, s_GA) % 0.18/0.54 +s_contains(s_g017, s_GQ) % 0.18/0.54 +s_contains(s_g017, s_ST) % 0.18/0.54 +s_contains(s_g017, s_TD) % 0.18/0.54 +s_contains(s_g018, s_BW) % 0.18/0.54 +s_contains(s_g018, s_LS) % 0.18/0.54 +s_contains(s_g018, s_NA) % 0.18/0.54 +s_contains(s_g018, s_SZ) % 0.18/0.54 +s_contains(s_g018, s_ZA) % 0.18/0.54 +s_contains(s_g053, s_AU) % 0.18/0.54 +s_contains(s_g053, s_NF) % 0.18/0.54 +s_contains(s_g053, s_NZ) % 0.18/0.54 +s_contains(s_g054, s_FJ) % 0.18/0.54 +s_contains(s_g054, s_NC) % 0.18/0.54 +s_contains(s_g054, s_PG) % 0.18/0.54 +s_contains(s_g054, s_SB) % 0.18/0.54 +s_contains(s_g054, s_VU) % 0.18/0.54 +s_contains(s_g057, s_FM) % 0.18/0.54 +s_contains(s_g057, s_GU) % 0.18/0.54 +s_contains(s_g057, s_KI) % 0.18/0.54 +s_contains(s_g057, s_MH) % 0.18/0.54 +s_contains(s_g057, s_MP) % 0.18/0.54 +s_contains(s_g057, s_NR) % 0.18/0.54 +s_contains(s_g057, s_PW) % 0.18/0.54 +s_contains(s_g061, s_AS) % 0.18/0.54 +s_contains(s_g061, s_CK) % 0.18/0.54 +s_contains(s_g061, s_NU) % 0.18/0.54 +s_contains(s_g061, s_PF) % 0.18/0.54 +s_contains(s_g061, s_PN) % 0.18/0.54 +s_contains(s_g061, s_TK) % 0.18/0.54 +s_contains(s_g061, s_TO) % 0.18/0.54 +s_contains(s_g061, s_TV) % 0.18/0.54 +s_contains(s_g061, s_WF) % 0.18/0.54 +s_contains(s_g061, s_WS) % 0.18/0.54 +s_contains(s_g005, s_AR) % 0.18/0.54 +s_contains(s_g005, s_BO) % 0.18/0.54 +s_contains(s_g005, s_BR) % 0.18/0.54 +s_contains(s_g005, s_CL) % 0.18/0.54 +s_contains(s_g005, s_CO) % 0.18/0.54 +s_contains(s_g005, s_EC) % 0.18/0.54 +s_contains(s_g005, s_FK) % 0.18/0.54 +s_contains(s_g005, s_GF) % 0.18/0.54 +s_contains(s_g005, s_GY) % 0.18/0.54 +s_contains(s_g005, s_PE) % 0.18/0.54 +s_contains(s_g005, s_PY) % 0.18/0.54 +s_contains(s_g005, s_SR) % 0.18/0.54 +s_contains(s_g005, s_UY) % 0.18/0.54 +s_contains(s_g005, s_VE) % 0.18/0.54 +s_contains(s_g013, s_BZ) % 0.18/0.54 +s_contains(s_g013, s_CR) % 0.18/0.54 +s_contains(s_g013, s_GT) % 0.18/0.54 +s_contains(s_g013, s_HN) % 0.18/0.54 +s_contains(s_g013, s_MX) % 0.18/0.54 +s_contains(s_g013, s_NI) % 0.18/0.54 +s_contains(s_g013, s_PA) % 0.18/0.54 +s_contains(s_g013, s_SV) % 0.18/0.54 +s_contains(s_g021, s_BM) % 0.18/0.54 +s_contains(s_g021, s_CA) % 0.18/0.54 +s_contains(s_g021, s_GL) % 0.18/0.54 +s_contains(s_g021, s_PM) % 0.18/0.54 +s_contains(s_g021, s_US) % 0.18/0.54 +s_contains(s_g029, s_AG) % 0.18/0.54 +s_contains(s_g029, s_AI) % 0.18/0.54 +s_contains(s_g029, s_AN) % 0.18/0.54 +s_contains(s_g029, s_AW) % 0.18/0.54 +s_contains(s_g029, s_BB) % 0.18/0.54 +s_contains(s_g029, s_BL) % 0.18/0.54 +s_contains(s_g029, s_BS) % 0.18/0.54 +s_contains(s_g029, s_CU) % 0.18/0.54 +s_contains(s_g029, s_DM) % 0.18/0.54 +s_contains(s_g029, s_DO) % 0.18/0.54 +s_contains(s_g029, s_GD) % 0.18/0.54 +s_contains(s_g029, s_GP) % 0.18/0.54 +s_contains(s_g029, s_HT) % 0.18/0.54 +s_contains(s_g029, s_JM) % 0.18/0.54 +s_contains(s_g029, s_KN) % 0.18/0.54 +s_contains(s_g029, s_KY) % 0.18/0.54 +s_contains(s_g029, s_LC) % 0.18/0.54 +s_contains(s_g029, s_MF) % 0.18/0.54 +s_contains(s_g029, s_MQ) % 0.18/0.54 +s_contains(s_g029, s_MS) % 0.18/0.54 +s_contains(s_g029, s_PR) % 0.18/0.54 +s_contains(s_g029, s_TC) % 0.18/0.54 +s_contains(s_g029, s_TT) % 0.18/0.54 +s_contains(s_g029, s_VC) % 0.18/0.54 +s_contains(s_g029, s_VG) % 0.18/0.54 +s_contains(s_g029, s_VI) % 0.18/0.54 +s_contains(s_g003, s_g013) % 0.18/0.54 +s_contains(s_g003, s_g021) % 0.18/0.54 +s_contains(s_g003, s_g029) % 0.18/0.54 +s_contains(s_g003, s_BZ) % 0.18/0.54 +s_contains(s_g003, s_CR) % 0.18/0.54 +s_contains(s_g003, s_GT) % 0.18/0.54 +s_contains(s_g003, s_HN) % 0.18/0.54 +s_contains(s_g003, s_MX) % 0.18/0.54 +s_contains(s_g003, s_NI) % 0.18/0.54 +s_contains(s_g003, s_PA) % 0.18/0.54 +s_contains(s_g003, s_SV) % 0.18/0.54 +s_contains(s_g003, s_BM) % 0.18/0.54 +s_contains(s_g003, s_CA) % 0.18/0.54 +s_contains(s_g003, s_GL) % 0.18/0.54 +s_contains(s_g003, s_PM) % 0.18/0.54 +s_contains(s_g003, s_US) % 0.18/0.54 +s_contains(s_g003, s_AG) % 0.18/0.54 +s_contains(s_g003, s_AI) % 0.18/0.54 +s_contains(s_g003, s_AN) % 0.18/0.54 +s_contains(s_g003, s_AW) % 0.18/0.54 +s_contains(s_g003, s_BB) % 0.18/0.54 +s_contains(s_g003, s_BL) % 0.18/0.54 +s_contains(s_g003, s_BS) % 0.18/0.54 +s_contains(s_g003, s_CU) % 0.18/0.54 +s_contains(s_g003, s_DM) % 0.18/0.54 +s_contains(s_g003, s_DO) % 0.18/0.54 +s_contains(s_g003, s_GD) % 0.18/0.54 +s_contains(s_g003, s_GP) % 0.18/0.54 +s_contains(s_g003, s_HT) % 0.18/0.54 +s_contains(s_g003, s_JM) % 0.18/0.54 +s_contains(s_g003, s_KN) % 0.18/0.54 +s_contains(s_g003, s_KY) % 0.18/0.54 +s_contains(s_g003, s_LC) % 0.18/0.54 +s_contains(s_g003, s_MF) % 0.18/0.54 +s_contains(s_g003, s_MQ) % 0.18/0.54 +s_contains(s_g003, s_MS) % 0.18/0.54 +s_contains(s_g003, s_PR) % 0.18/0.54 +s_contains(s_g003, s_TC) % 0.18/0.54 +s_contains(s_g003, s_TT) % 0.18/0.54 +s_contains(s_g003, s_VC) % 0.18/0.54 +s_contains(s_g003, s_VG) % 0.18/0.54 +s_contains(s_g003, s_VI) % 0.18/0.54 +s_contains(s_g419, s_g005) % 0.18/0.54 +s_contains(s_g419, s_g013) % 0.18/0.54 +s_contains(s_g419, s_g029) % 0.18/0.54 +s_contains(s_g419, s_BZ) % 0.18/0.54 +s_contains(s_g419, s_CR) % 0.18/0.54 +s_contains(s_g419, s_GT) % 0.18/0.54 +s_contains(s_g419, s_HN) % 0.18/0.54 +s_contains(s_g419, s_MX) % 0.18/0.54 +s_contains(s_g419, s_NI) % 0.18/0.54 +s_contains(s_g419, s_PA) % 0.18/0.54 +s_contains(s_g419, s_SV) % 0.18/0.54 +s_contains(s_g419, s_AR) % 0.18/0.54 +s_contains(s_g419, s_BO) % 0.18/0.54 +s_contains(s_g419, s_BR) % 0.18/0.54 +s_contains(s_g419, s_CL) % 0.18/0.54 +s_contains(s_g419, s_CO) % 0.18/0.54 +s_contains(s_g419, s_EC) % 0.18/0.54 +s_contains(s_g419, s_FK) % 0.18/0.54 +s_contains(s_g419, s_GF) % 0.18/0.54 +s_contains(s_g419, s_GY) % 0.18/0.54 +s_contains(s_g419, s_PE) % 0.18/0.54 +s_contains(s_g419, s_PY) % 0.18/0.54 +s_contains(s_g419, s_SR) % 0.18/0.54 +s_contains(s_g419, s_UY) % 0.18/0.54 +s_contains(s_g419, s_VE) % 0.18/0.54 +s_contains(s_g419, s_AG) % 0.18/0.54 +s_contains(s_g419, s_AI) % 0.18/0.54 +s_contains(s_g419, s_AN) % 0.18/0.54 +s_contains(s_g419, s_AW) % 0.18/0.54 +s_contains(s_g419, s_BB) % 0.18/0.54 +s_contains(s_g419, s_BL) % 0.18/0.54 +s_contains(s_g419, s_BS) % 0.18/0.54 +s_contains(s_g419, s_CU) % 0.18/0.54 +s_contains(s_g419, s_DM) % 0.18/0.54 +s_contains(s_g419, s_DO) % 0.18/0.54 +s_contains(s_g419, s_GD) % 0.18/0.54 +s_contains(s_g419, s_GP) % 0.18/0.54 +s_contains(s_g419, s_HT) % 0.18/0.54 +s_contains(s_g419, s_JM) % 0.18/0.54 +s_contains(s_g419, s_KN) % 0.18/0.54 +s_contains(s_g419, s_KY) % 0.18/0.54 +s_contains(s_g419, s_LC) % 0.18/0.54 +s_contains(s_g419, s_MF) % 0.18/0.54 +s_contains(s_g419, s_MQ) % 0.18/0.54 +s_contains(s_g419, s_MS) % 0.18/0.54 +s_contains(s_g419, s_PR) % 0.18/0.54 +s_contains(s_g419, s_TC) % 0.18/0.54 +s_contains(s_g419, s_TT) % 0.18/0.54 +s_contains(s_g419, s_VC) % 0.18/0.54 +s_contains(s_g419, s_VG) % 0.18/0.54 +s_contains(s_g419, s_VI) % 0.18/0.54 +s_contains(s_g030, s_CN) % 0.18/0.54 +s_contains(s_g030, s_HK) % 0.18/0.54 +s_contains(s_g030, s_JP) % 0.18/0.54 +s_contains(s_g030, s_KP) % 0.18/0.54 +s_contains(s_g030, s_KR) % 0.18/0.54 +s_contains(s_g030, s_MN) % 0.18/0.54 +s_contains(s_g030, s_MO) % 0.18/0.54 +s_contains(s_g030, s_TW) % 0.18/0.54 +s_contains(s_g035, s_BN) % 0.18/0.54 +s_contains(s_g035, s_ID) % 0.18/0.54 +s_contains(s_g035, s_KH) % 0.18/0.54 +s_contains(s_g035, s_LA) % 0.18/0.54 +s_contains(s_g035, s_MM) % 0.18/0.54 +s_contains(s_g035, s_BU) % 0.18/0.54 +s_contains(s_g035, s_MY) % 0.18/0.54 +s_contains(s_g035, s_PH) % 0.18/0.54 +s_contains(s_g035, s_SG) % 0.18/0.54 +s_contains(s_g035, s_TH) % 0.18/0.54 +s_contains(s_g035, s_TL) % 0.18/0.54 +s_contains(s_g035, s_TP) % 0.18/0.54 +s_contains(s_g035, s_VN) % 0.18/0.54 +s_contains(s_g143, s_TM) % 0.18/0.54 +s_contains(s_g143, s_TJ) % 0.18/0.54 +s_contains(s_g143, s_KG) % 0.18/0.54 +s_contains(s_g143, s_KZ) % 0.18/0.54 +s_contains(s_g143, s_UZ) % 0.18/0.54 +s_contains(s_g145, s_AE) % 0.18/0.54 +s_contains(s_g145, s_AM) % 0.18/0.54 +s_contains(s_g145, s_AZ) % 0.18/0.54 +s_contains(s_g145, s_BH) % 0.18/0.54 +s_contains(s_g145, s_CY) % 0.18/0.54 +s_contains(s_g145, s_GE) % 0.18/0.54 +s_contains(s_g145, s_IL) % 0.18/0.54 +s_contains(s_g145, s_IQ) % 0.18/0.54 +s_contains(s_g145, s_JO) % 0.18/0.54 +s_contains(s_g145, s_KW) % 0.18/0.54 +s_contains(s_g145, s_LB) % 0.18/0.54 +s_contains(s_g145, s_OM) % 0.18/0.54 +s_contains(s_g145, s_PS) % 0.18/0.54 +s_contains(s_g145, s_QA) % 0.18/0.54 +s_contains(s_g145, s_SA) % 0.18/0.54 +s_contains(s_g145, s_NT) % 0.18/0.54 +s_contains(s_g145, s_SY) % 0.18/0.54 +s_contains(s_g145, s_TR) % 0.18/0.54 +s_contains(s_g145, s_YE) % 0.18/0.54 +s_contains(s_g145, s_YD) % 0.18/0.54 +s_contains(s_g034, s_AF) % 0.18/0.54 +s_contains(s_g034, s_BD) % 0.18/0.54 +s_contains(s_g034, s_BT) % 0.18/0.54 +s_contains(s_g034, s_IN) % 0.18/0.54 +s_contains(s_g034, s_IR) % 0.18/0.54 +s_contains(s_g034, s_LK) % 0.18/0.54 +s_contains(s_g034, s_MV) % 0.18/0.54 +s_contains(s_g034, s_NP) % 0.18/0.54 +s_contains(s_g034, s_PK) % 0.18/0.54 +s_contains(s_g062, s_g143) % 0.18/0.54 +s_contains(s_g062, s_g034) % 0.18/0.54 +s_contains(s_g062, s_TM) % 0.18/0.54 +s_contains(s_g062, s_TJ) % 0.18/0.54 +s_contains(s_g062, s_KG) % 0.18/0.54 +s_contains(s_g062, s_KZ) % 0.18/0.54 +s_contains(s_g062, s_UZ) % 0.18/0.54 +s_contains(s_g062, s_AF) % 0.18/0.54 +s_contains(s_g062, s_BD) % 0.18/0.54 +s_contains(s_g062, s_BT) % 0.18/0.54 +s_contains(s_g062, s_IN) % 0.18/0.54 +s_contains(s_g062, s_IR) % 0.18/0.54 +s_contains(s_g062, s_LK) % 0.18/0.54 +s_contains(s_g062, s_MV) % 0.18/0.54 +s_contains(s_g062, s_NP) % 0.18/0.54 +s_contains(s_g062, s_PK) % 0.18/0.54 +s_contains(s_g039, s_AD) % 0.18/0.54 +s_contains(s_g039, s_AL) % 0.18/0.54 +s_contains(s_g039, s_BA) % 0.18/0.54 +s_contains(s_g039, s_ES) % 0.18/0.54 +s_contains(s_g039, s_GI) % 0.18/0.54 +s_contains(s_g039, s_GR) % 0.18/0.54 +s_contains(s_g039, s_HR) % 0.18/0.54 +s_contains(s_g039, s_IT) % 0.18/0.54 +s_contains(s_g039, s_ME) % 0.18/0.54 +s_contains(s_g039, s_MK) % 0.18/0.54 +s_contains(s_g039, s_MT) % 0.18/0.54 +s_contains(s_g039, s_CS) % 0.18/0.54 +s_contains(s_g039, s_RS) % 0.18/0.54 +s_contains(s_g039, s_PT) % 0.18/0.54 +s_contains(s_g039, s_SI) % 0.18/0.54 +s_contains(s_g039, s_SM) % 0.18/0.54 +s_contains(s_g039, s_VA) % 0.18/0.54 +s_contains(s_g039, s_YU) % 0.18/0.54 +s_contains(s_g151, s_BG) % 0.18/0.54 +s_contains(s_g151, s_BY) % 0.18/0.54 +s_contains(s_g151, s_CZ) % 0.18/0.54 +s_contains(s_g151, s_HU) % 0.18/0.54 +s_contains(s_g151, s_MD) % 0.18/0.54 +s_contains(s_g151, s_PL) % 0.18/0.54 +s_contains(s_g151, s_RO) % 0.18/0.54 +s_contains(s_g151, s_RU) % 0.18/0.54 +s_contains(s_g151, s_SU) % 0.18/0.54 +s_contains(s_g151, s_SK) % 0.18/0.54 +s_contains(s_g151, s_UA) % 0.18/0.54 +s_contains(s_g154, s_GG) % 0.18/0.54 +s_contains(s_g154, s_IM) % 0.18/0.54 +s_contains(s_g154, s_JE) % 0.18/0.54 +s_contains(s_g154, s_AX) % 0.18/0.54 +s_contains(s_g154, s_DK) % 0.18/0.54 +s_contains(s_g154, s_EE) % 0.18/0.54 +s_contains(s_g154, s_FI) % 0.18/0.54 +s_contains(s_g154, s_FO) % 0.18/0.54 +s_contains(s_g154, s_GB) % 0.18/0.54 +s_contains(s_g154, s_IE) % 0.18/0.54 +s_contains(s_g154, s_IS) % 0.18/0.54 +s_contains(s_g154, s_LT) % 0.18/0.54 +s_contains(s_g154, s_LV) % 0.18/0.54 +s_contains(s_g154, s_NO) % 0.18/0.54 +s_contains(s_g154, s_SE) % 0.18/0.54 +s_contains(s_g154, s_SJ) % 0.18/0.54 +s_contains(s_g155, s_AT) % 0.18/0.54 +s_contains(s_g155, s_BE) % 0.18/0.54 +s_contains(s_g155, s_CH) % 0.18/0.54 +s_contains(s_g155, s_DE) % 0.18/0.54 +s_contains(s_g155, s_DD) % 0.18/0.54 +s_contains(s_g155, s_FR) % 0.18/0.54 +s_contains(s_g155, s_FX) % 0.18/0.54 +s_contains(s_g155, s_LI) % 0.18/0.54 +s_contains(s_g155, s_LU) % 0.18/0.54 +s_contains(s_g155, s_MC) % 0.18/0.54 +s_contains(s_g155, s_NL) % 0.18/0.54 +s_contains(s_g172, s_TM) % 0.18/0.54 +s_contains(s_g172, s_TJ) % 0.18/0.54 +s_contains(s_g172, s_KG) % 0.18/0.54 +s_contains(s_g172, s_KZ) % 0.18/0.54 +s_contains(s_g172, s_UZ) % 0.18/0.54 +s_contains(s_g172, s_AM) % 0.18/0.54 +s_contains(s_g172, s_AZ) % 0.18/0.54 +s_contains(s_g172, s_GE) % 0.18/0.54 +s_contains(s_g172, s_BY) % 0.18/0.54 +s_contains(s_g172, s_MD) % 0.18/0.54 +s_contains(s_g172, s_RU) % 0.18/0.54 +s_contains(s_g172, s_UA) % 0.18/0.54 +s_contains(s_g830, s_GG) % 0.18/0.54 +s_contains(s_g830, s_JE) % 0.18/0.54 -s_contains(s_g030, s_MX) % 0.18/0.54 +s_partOf(s_g002, s_g001) % 0.18/0.54 +s_partOf(s_g009, s_g001) % 0.18/0.54 +s_partOf(s_g019, s_g001) % 0.18/0.54 +s_partOf(s_g142, s_g001) % 0.18/0.54 +s_partOf(s_g150, s_g001) % 0.18/0.54 +s_partOf(s_g011, s_g002) % 0.18/0.54 +s_partOf(s_g014, s_g002) % 0.18/0.54 +s_partOf(s_g015, s_g002) % 0.18/0.54 +s_partOf(s_g017, s_g002) % 0.18/0.54 +s_partOf(s_g018, s_g002) % 0.18/0.54 +s_partOf(s_g053, s_g009) % 0.18/0.54 +s_partOf(s_g054, s_g009) % 0.18/0.54 +s_partOf(s_g057, s_g009) % 0.18/0.54 +s_partOf(s_g061, s_g009) % 0.18/0.54 +s_partOf(s_g005, s_g019) % 0.18/0.54 +s_partOf(s_g005, s_g419) % 0.18/0.54 +s_partOf(s_g013, s_g019) % 0.18/0.54 +s_partOf(s_g013, s_g003) % 0.18/0.54 +s_partOf(s_g013, s_g419) % 0.18/0.54 +s_partOf(s_g021, s_g019) % 0.18/0.55 +s_partOf(s_g021, s_g003) % 0.18/0.55 +s_partOf(s_g029, s_g019) % 0.18/0.55 +s_partOf(s_g029, s_g003) % 0.18/0.55 +s_partOf(s_g029, s_g419) % 0.18/0.55 +s_partOf(s_g003, s_g019) % 0.18/0.55 +s_partOf(s_g419, s_g019) % 0.18/0.55 +s_partOf(s_g030, s_g142) % 0.18/0.55 +s_partOf(s_g035, s_g142) % 0.18/0.55 +s_partOf(s_g143, s_g142) % 0.18/0.55 +s_partOf(s_g143, s_g062) % 0.18/0.55 +s_partOf(s_g145, s_g142) % 0.18/0.55 +s_partOf(s_g034, s_g142) % 0.18/0.55 +s_partOf(s_g034, s_g062) % 0.18/0.55 +s_partOf(s_g062, s_g142) % 0.18/0.55 +s_partOf(s_g039, s_g150) % 0.18/0.55 +s_partOf(s_g151, s_g150) % 0.18/0.55 +s_partOf(s_g154, s_g150) % 0.18/0.55 +s_partOf(s_g155, s_g150) % 0.18/0.55 +s_partOf(s_BF, s_g011) % 0.18/0.55 +s_partOf(s_BJ, s_g011) % 0.18/0.55 +s_partOf(s_CI, s_g011) % 0.18/0.55 +s_partOf(s_CV, s_g011) % 0.18/0.55 +s_partOf(s_GH, s_g011) % 0.18/0.55 +s_partOf(s_GM, s_g011) % 0.18/0.55 +s_partOf(s_GN, s_g011) % 0.18/0.55 +s_partOf(s_GW, s_g011) % 0.18/0.55 +s_partOf(s_LR, s_g011) % 0.18/0.55 +s_partOf(s_ML, s_g011) % 0.18/0.55 +s_partOf(s_MR, s_g011) % 0.18/0.55 +s_partOf(s_NE, s_g011) % 0.18/0.55 +s_partOf(s_NG, s_g011) % 0.18/0.55 +s_partOf(s_SH, s_g011) % 0.18/0.55 +s_partOf(s_SL, s_g011) % 0.18/0.55 +s_partOf(s_SN, s_g011) % 0.18/0.55 +s_partOf(s_TG, s_g011) % 0.18/0.55 +s_partOf(s_BZ, s_g013) % 0.18/0.55 +s_partOf(s_CR, s_g013) % 0.18/0.55 +s_partOf(s_GT, s_g013) % 0.18/0.55 +s_partOf(s_HN, s_g013) % 0.18/0.55 +s_partOf(s_MX, s_g013) % 0.18/0.55 +s_partOf(s_NI, s_g013) % 0.18/0.55 +s_partOf(s_PA, s_g013) % 0.18/0.55 +s_partOf(s_SV, s_g013) % 0.18/0.55 +s_partOf(s_BI, s_g014) % 0.18/0.55 +s_partOf(s_DJ, s_g014) % 0.18/0.55 +s_partOf(s_ER, s_g014) % 0.18/0.55 +s_partOf(s_ET, s_g014) % 0.18/0.55 +s_partOf(s_KE, s_g014) % 0.18/0.55 +s_partOf(s_KM, s_g014) % 0.18/0.55 +s_partOf(s_MG, s_g014) % 0.18/0.55 +s_partOf(s_MU, s_g014) % 0.18/0.55 +s_partOf(s_MW, s_g014) % 0.18/0.55 +s_partOf(s_MZ, s_g014) % 0.18/0.55 +s_partOf(s_RE, s_g014) % 0.18/0.55 +s_partOf(s_RW, s_g014) % 0.18/0.55 +s_partOf(s_SC, s_g014) % 0.18/0.55 +s_partOf(s_SO, s_g014) % 0.18/0.55 +s_partOf(s_TZ, s_g014) % 0.18/0.55 +s_partOf(s_UG, s_g014) % 0.18/0.55 +s_partOf(s_YT, s_g014) % 0.18/0.55 +s_partOf(s_ZM, s_g014) % 0.18/0.55 +s_partOf(s_ZW, s_g014) % 0.18/0.55 +s_partOf(s_CN, s_g030) % 0.18/0.55 +s_partOf(s_HK, s_g030) % 0.18/0.55 +s_partOf(s_JP, s_g030) % 0.18/0.55 +s_partOf(s_KP, s_g030) % 0.18/0.55 +s_partOf(s_KR, s_g030) % 0.18/0.55 +s_partOf(s_MN, s_g030) % 0.18/0.55 +s_partOf(s_MO, s_g030) % 0.18/0.55 +s_partOf(s_TW, s_g030) % 0.18/0.55 +s_partOf(s_BN, s_g035) % 0.18/0.55 +s_partOf(s_ID, s_g035) % 0.18/0.55 +s_partOf(s_KH, s_g035) % 0.18/0.55 +s_partOf(s_LA, s_g035) % 0.18/0.55 +s_partOf(s_MM, s_g035) % 0.18/0.55 +s_partOf(s_BU, s_g035) % 0.18/0.55 +s_partOf(s_MY, s_g035) % 0.18/0.55 +s_partOf(s_PH, s_g035) % 0.18/0.55 +s_partOf(s_SG, s_g035) % 0.18/0.55 +s_partOf(s_TH, s_g035) % 0.18/0.55 +s_partOf(s_TL, s_g035) % 0.18/0.55 +s_partOf(s_TP, s_g035) % 0.18/0.55 +s_partOf(s_VN, s_g035) % 0.18/0.55 +s_partOf(s_TM, s_g143) % 0.18/0.55 +s_partOf(s_TM, s_g172) % 0.18/0.55 +s_partOf(s_TJ, s_g143) % 0.18/0.55 +s_partOf(s_TJ, s_g172) % 0.18/0.55 +s_partOf(s_KG, s_g143) % 0.18/0.55 +s_partOf(s_KG, s_g172) % 0.18/0.55 +s_partOf(s_KZ, s_g143) % 0.18/0.55 +s_partOf(s_KZ, s_g172) % 0.18/0.55 +s_partOf(s_UZ, s_g143) % 0.18/0.55 +s_partOf(s_UZ, s_g172) % 0.18/0.55 +s_partOf(s_AE, s_g145) % 0.18/0.55 +s_partOf(s_AM, s_g145) % 0.18/0.55 +s_partOf(s_AM, s_g172) % 0.18/0.55 +s_partOf(s_AZ, s_g145) % 0.18/0.55 +s_partOf(s_AZ, s_g172) % 0.18/0.55 +s_partOf(s_BH, s_g145) % 0.18/0.55 +s_partOf(s_CY, s_g145) % 0.18/0.55 +s_partOf(s_GE, s_g145) % 0.18/0.55 +s_partOf(s_GE, s_g172) % 0.18/0.55 +s_partOf(s_IL, s_g145) % 0.18/0.55 +s_partOf(s_IQ, s_g145) % 0.18/0.55 +s_partOf(s_JO, s_g145) % 0.18/0.55 +s_partOf(s_KW, s_g145) % 0.18/0.55 +s_partOf(s_LB, s_g145) % 0.18/0.55 +s_partOf(s_OM, s_g145) % 0.18/0.55 +s_partOf(s_PS, s_g145) % 0.18/0.55 +s_partOf(s_QA, s_g145) % 0.18/0.55 +s_partOf(s_SA, s_g145) % 0.18/0.55 +s_partOf(s_NT, s_g145) % 0.18/0.55 +s_partOf(s_SY, s_g145) % 0.18/0.55 +s_partOf(s_TR, s_g145) % 0.18/0.55 +s_partOf(s_YE, s_g145) % 0.18/0.55 +s_partOf(s_YD, s_g145) % 0.18/0.55 +s_partOf(s_AF, s_g034) % 0.18/0.55 +s_partOf(s_BD, s_g034) % 0.18/0.55 +s_partOf(s_BT, s_g034) % 0.18/0.55 +s_partOf(s_IN, s_g034) % 0.18/0.55 +s_partOf(s_IR, s_g034) % 0.18/0.55 +s_partOf(s_LK, s_g034) % 0.18/0.55 +s_partOf(s_MV, s_g034) % 0.18/0.55 +s_partOf(s_NP, s_g034) % 0.18/0.55 +s_partOf(s_PK, s_g034) % 0.18/0.55 +s_partOf(s_DZ, s_g015) % 0.18/0.55 +s_partOf(s_EG, s_g015) % 0.18/0.55 +s_partOf(s_EH, s_g015) % 0.18/0.55 +s_partOf(s_LY, s_g015) % 0.18/0.55 +s_partOf(s_MA, s_g015) % 0.18/0.55 +s_partOf(s_SD, s_g015) % 0.18/0.55 +s_partOf(s_TN, s_g015) % 0.18/0.55 +s_partOf(s_AD, s_g039) % 0.18/0.55 +s_partOf(s_AL, s_g039) % 0.18/0.55 +s_partOf(s_BA, s_g039) % 0.18/0.55 +s_partOf(s_ES, s_g039) % 0.18/0.55 +s_partOf(s_GI, s_g039) % 0.18/0.55 +s_partOf(s_GR, s_g039) % 0.18/0.55 +s_partOf(s_HR, s_g039) % 0.18/0.55 +s_partOf(s_IT, s_g039) % 0.18/0.55 +s_partOf(s_ME, s_g039) % 0.18/0.55 +s_partOf(s_MK, s_g039) % 0.18/0.55 +s_partOf(s_MT, s_g039) % 0.18/0.55 +s_partOf(s_CS, s_g039) % 0.18/0.55 +s_partOf(s_RS, s_g039) % 0.18/0.55 +s_partOf(s_PT, s_g039) % 0.18/0.55 +s_partOf(s_SI, s_g039) % 0.18/0.55 +s_partOf(s_SM, s_g039) % 0.18/0.55 +s_partOf(s_VA, s_g039) % 0.18/0.55 +s_partOf(s_YU, s_g039) % 0.18/0.55 +s_partOf(s_BG, s_g151) % 0.18/0.55 +s_partOf(s_BY, s_g151) % 0.18/0.55 +s_partOf(s_BY, s_g172) % 0.18/0.55 +s_partOf(s_CZ, s_g151) % 0.18/0.55 +s_partOf(s_HU, s_g151) % 0.18/0.55 +s_partOf(s_MD, s_g151) % 0.18/0.55 +s_partOf(s_MD, s_g172) % 0.18/0.55 +s_partOf(s_PL, s_g151) % 0.18/0.55 +s_partOf(s_RO, s_g151) % 0.18/0.55 +s_partOf(s_RU, s_g151) % 0.18/0.55 +s_partOf(s_RU, s_g172) % 0.18/0.55 +s_partOf(s_SU, s_g151) % 0.18/0.55 +s_partOf(s_SK, s_g151) % 0.18/0.55 +s_partOf(s_UA, s_g151) % 0.18/0.55 +s_partOf(s_UA, s_g172) % 0.18/0.55 +s_partOf(s_GG, s_g154) % 0.18/0.55 +s_partOf(s_GG, s_g830) % 0.18/0.55 +s_partOf(s_IM, s_g154) % 0.18/0.55 +s_partOf(s_JE, s_g154) % 0.18/0.55 +s_partOf(s_JE, s_g830) % 0.18/0.55 +s_partOf(s_AX, s_g154) % 0.18/0.55 +s_partOf(s_DK, s_g154) % 0.18/0.55 +s_partOf(s_EE, s_g154) % 0.18/0.55 +s_partOf(s_FI, s_g154) % 0.18/0.55 +s_partOf(s_FO, s_g154) % 0.18/0.55 +s_partOf(s_GB, s_g154) % 0.18/0.55 +s_partOf(s_IE, s_g154) % 0.18/0.55 +s_partOf(s_IS, s_g154) % 0.18/0.55 +s_partOf(s_LT, s_g154) % 0.18/0.55 +s_partOf(s_LV, s_g154) % 0.18/0.55 +s_partOf(s_NO, s_g154) % 0.18/0.55 +s_partOf(s_SE, s_g154) % 0.18/0.55 +s_partOf(s_SJ, s_g154) % 0.18/0.55 +s_partOf(s_AT, s_g155) % 0.18/0.55 +s_partOf(s_BE, s_g155) % 0.18/0.55 +s_partOf(s_CH, s_g155) % 0.18/0.55 +s_partOf(s_DE, s_g155) % 0.18/0.55 +s_partOf(s_DD, s_g155) % 0.18/0.55 +s_partOf(s_FR, s_g155) % 0.18/0.55 +s_partOf(s_FX, s_g155) % 0.18/0.55 +s_partOf(s_LI, s_g155) % 0.18/0.55 +s_partOf(s_LU, s_g155) % 0.18/0.55 +s_partOf(s_MC, s_g155) % 0.18/0.55 +s_partOf(s_NL, s_g155) % 0.18/0.55 +s_partOf(s_AO, s_g017) % 0.18/0.55 +s_partOf(s_CD, s_g017) % 0.18/0.55 +s_partOf(s_ZR, s_g017) % 0.18/0.55 +s_partOf(s_CF, s_g017) % 0.18/0.55 +s_partOf(s_CG, s_g017) % 0.18/0.55 +s_partOf(s_CM, s_g017) % 0.18/0.55 +s_partOf(s_GA, s_g017) % 0.18/0.55 +s_partOf(s_GQ, s_g017) % 0.18/0.55 +s_partOf(s_ST, s_g017) % 0.18/0.55 +s_partOf(s_TD, s_g017) % 0.18/0.55 +s_partOf(s_BW, s_g018) % 0.18/0.55 +s_partOf(s_LS, s_g018) % 0.18/0.55 +s_partOf(s_NA, s_g018) % 0.18/0.55 +s_partOf(s_SZ, s_g018) % 0.18/0.55 +s_partOf(s_ZA, s_g018) % 0.18/0.55 +s_partOf(s_AR, s_g005) % 0.18/0.55 +s_partOf(s_BO, s_g005) % 0.18/0.55 +s_partOf(s_BR, s_g005) % 0.18/0.55 +s_partOf(s_CL, s_g005) % 0.18/0.55 +s_partOf(s_CO, s_g005) % 0.18/0.55 +s_partOf(s_EC, s_g005) % 0.18/0.55 +s_partOf(s_FK, s_g005) % 0.18/0.55 +s_partOf(s_GF, s_g005) % 0.18/0.55 +s_partOf(s_GY, s_g005) % 0.18/0.55 +s_partOf(s_PE, s_g005) % 0.18/0.55 +s_partOf(s_PY, s_g005) % 0.18/0.55 +s_partOf(s_SR, s_g005) % 0.18/0.55 +s_partOf(s_UY, s_g005) % 0.18/0.55 +s_partOf(s_VE, s_g005) % 0.18/0.55 +s_partOf(s_BM, s_g021) % 0.18/0.55 +s_partOf(s_CA, s_g021) % 0.18/0.55 +s_partOf(s_GL, s_g021) % 0.18/0.55 +s_partOf(s_PM, s_g021) % 0.18/0.55 +s_partOf(s_US, s_g021) % 0.18/0.55 +s_partOf(s_AG, s_g029) % 0.18/0.55 +s_partOf(s_AI, s_g029) % 0.18/0.55 +s_partOf(s_AN, s_g029) % 0.18/0.55 +s_partOf(s_AW, s_g029) % 0.18/0.55 +s_partOf(s_BB, s_g029) % 0.18/0.55 +s_partOf(s_BL, s_g029) % 0.18/0.55 +s_partOf(s_BS, s_g029) % 0.18/0.55 +s_partOf(s_CU, s_g029) % 0.18/0.55 +s_partOf(s_DM, s_g029) % 0.18/0.55 +s_partOf(s_DO, s_g029) % 0.18/0.55 +s_partOf(s_GD, s_g029) % 0.18/0.55 +s_partOf(s_GP, s_g029) % 0.18/0.55 +s_partOf(s_HT, s_g029) % 0.18/0.55 +s_partOf(s_JM, s_g029) % 0.18/0.55 +s_partOf(s_KN, s_g029) % 0.18/0.55 +s_partOf(s_KY, s_g029) % 0.18/0.55 +s_partOf(s_LC, s_g029) % 0.18/0.55 +s_partOf(s_MF, s_g029) % 0.18/0.55 +s_partOf(s_MQ, s_g029) % 0.18/0.55 +s_partOf(s_MS, s_g029) % 0.18/0.55 +s_partOf(s_PR, s_g029) % 0.18/0.55 +s_partOf(s_TC, s_g029) % 0.18/0.55 +s_partOf(s_TT, s_g029) % 0.18/0.55 +s_partOf(s_VC, s_g029) % 0.18/0.55 +s_partOf(s_VG, s_g029) % 0.18/0.55 +s_partOf(s_VI, s_g029) % 0.18/0.55 +s_partOf(s_AU, s_g053) % 0.18/0.55 +s_partOf(s_NF, s_g053) % 0.18/0.55 +s_partOf(s_NZ, s_g053) % 0.18/0.55 +s_partOf(s_FJ, s_g054) % 0.18/0.55 +s_partOf(s_NC, s_g054) % 0.18/0.55 +s_partOf(s_PG, s_g054) % 0.18/0.55 +s_partOf(s_SB, s_g054) % 0.18/0.55 +s_partOf(s_VU, s_g054) % 0.18/0.55 +s_partOf(s_FM, s_g057) % 0.18/0.55 +s_partOf(s_GU, s_g057) % 0.18/0.55 +s_partOf(s_KI, s_g057) % 0.18/0.55 +s_partOf(s_MH, s_g057) % 0.18/0.55 +s_partOf(s_MP, s_g057) % 0.18/0.55 +s_partOf(s_NR, s_g057) % 0.18/0.55 +s_partOf(s_PW, s_g057) % 0.18/0.55 +s_partOf(s_AS, s_g061) % 0.18/0.55 +s_partOf(s_CK, s_g061) % 0.18/0.55 +s_partOf(s_NU, s_g061) % 0.18/0.55 +s_partOf(s_PF, s_g061) % 0.18/0.55 +s_partOf(s_PN, s_g061) % 0.18/0.55 +s_partOf(s_TK, s_g061) % 0.18/0.55 +s_partOf(s_TO, s_g061) % 0.18/0.55 +s_partOf(s_TV, s_g061) % 0.18/0.55 +s_partOf(s_WF, s_g061) % 0.18/0.55 +s_partOf(s_WS, s_g061) % 0.18/0.55 SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------