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