%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : MSC018+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n003.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 : 300s % DateTime : Tue Jun 25 02:03:02 EDT 2024 % Result : Unknown 0.75s 0.96s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.13 % Problem : MSC018+1 : TPTP v8.2.0. Released v4.0.0. % 0.06/0.13 % Command : run_zenon_modulo %d %s % 0.11/0.33 % Computer : n003.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 00:39:08 EDT 2024 % 0.11/0.34 % CPUTime : % 0.75/0.95 Zenon error: exhausted search space without finding a proof % 0.75/0.95 (* Current branch: % 0.75/0.95 (s_partOf (s_ST) (s_g017)) % 0.75/0.95 (s_partOf (s_TJ) (s_g172)) % 0.75/0.95 ((s_LC) != (s_MX)) % 0.75/0.95 ((s_g143) != (s_g019)) % 0.75/0.95 ((s_g143) != (s_g419)) % 0.75/0.95 ((s_TC) != (s_g019)) % 0.75/0.95 ((s_CO) != (s_MX)) % 0.75/0.95 ((s_MG) != (s_g419)) % 0.75/0.95 ((s_KW) != (s_g001)) % 0.75/0.95 ((s_ET) != (s_g001)) % 0.75/0.95 ((s_LA) != (s_g003)) % 0.75/0.95 (s_partOf (s_NG) (s_g011)) % 0.75/0.95 ((s_ER) != (s_g003)) % 0.75/0.95 ((s_MH) != (s_g003)) % 0.75/0.95 ((s_PW) != (s_g419)) % 0.75/0.95 ((s_FX) != (s_g019)) % 0.75/0.95 ((s_DK) != (s_g003)) % 0.75/0.95 ((s_g061) != (s_g019)) % 0.75/0.95 (s_partOf (s_PK) (s_g034)) % 0.75/0.95 ((s_TV) != (s_g419)) % 0.75/0.95 ((s_SJ) != (s_g013)) % 0.75/0.95 ((s_SN) != (s_MX)) % 0.75/0.95 ((s_BY) != (s_g001)) % 0.75/0.95 ((s_LV) != (s_MX)) % 0.75/0.95 ((s_g039) != (s_MX)) % 0.75/0.95 ((s_AX) != (s_g019)) % 0.75/0.95 (s_partOf (s_BJ) (s_g011)) % 0.75/0.95 (s_contains (s_g011) (s_GW)) % 0.75/0.95 ((s_YD) != (s_MX)) % 0.75/0.95 ((s_LY) != (s_g001)) % 0.75/0.95 ((s_GL) != (s_g001)) % 0.75/0.95 ((s_TV) != (s_g001)) % 0.75/0.95 ((s_AU) != (s_g001)) % 0.75/0.95 ((s_CS) != (s_g019)) % 0.75/0.95 ((s_SY) != (s_g001)) % 0.75/0.95 (s_contains (s_g005) (s_CL)) % 0.75/0.95 ((s_CA) != (s_g019)) % 0.75/0.95 (s_partOf (s_MY) (s_g035)) % 0.75/0.95 ((s_PK) != (s_g001)) % 0.75/0.95 (s_partOf (s_MW) (s_g014)) % 0.75/0.95 ((s_TC) != (s_g003)) % 0.75/0.95 (s_partOf (s_NE) (s_g011)) % 0.75/0.95 ((s_DJ) != (s_g013)) % 0.75/0.95 ((s_AF) != (s_g013)) % 0.75/0.95 ((s_VI) != (s_g001)) % 0.75/0.95 (s_partOf (s_VG) (s_g029)) % 0.75/0.95 ((s_KY) != (s_g003)) % 0.75/0.95 (s_partOf (s_EE) (s_g154)) % 0.75/0.95 ((s_BG) != (s_MX)) % 0.75/0.95 ((s_g057) != (s_g013)) % 0.75/0.95 ((s_CN) != (s_g013)) % 0.75/0.95 ((s_BL) != (s_g419)) % 0.75/0.95 ((s_DD) != (s_g019)) % 0.75/0.95 (s_partOf (s_LI) (s_g155)) % 0.75/0.95 ((s_GW) != (s_MX)) % 0.75/0.95 ((s_PW) != (s_g001)) % 0.75/0.95 ((s_BN) != (s_MX)) % 0.75/0.95 ((s_EE) != (s_g019)) % 0.75/0.95 (s_contains (s_g057) (s_GU)) % 0.75/0.95 ((s_MK) != (s_MX)) % 0.75/0.95 ((s_KG) != (s_g003)) % 0.75/0.95 ((s_LV) != (s_g003)) % 0.75/0.95 ((s_KH) != (s_g013)) % 0.75/0.95 (s_partOf (s_GD) (s_g029)) % 0.75/0.95 ((s_IT) != (s_g419)) % 0.75/0.95 ((s_KR) != (s_g019)) % 0.75/0.95 ((s_AR) != (s_MX)) % 0.75/0.95 ((s_GM) != (s_g019)) % 0.75/0.95 (s_contains (s_g014) (s_BI)) % 0.75/0.95 (-. (s_contains (s_MN) (s_g001))) % 0.75/0.95 ((s_KR) != (s_g003)) % 0.75/0.95 ((s_EH) != (s_g013)) % 0.75/0.95 ((s_LS) != (s_g003)) % 0.75/0.95 ((s_PG) != (s_g003)) % 0.75/0.95 (s_contains (s_g013) (s_PA)) % 0.75/0.95 ((s_AI) != (s_g001)) % 0.75/0.95 ((s_g061) != (s_g003)) % 0.75/0.95 ((s_TD) != (s_g003)) % 0.75/0.95 ((s_TO) != (s_g001)) % 0.75/0.95 (-. (s_contains (s_KR) (s_g003))) % 0.75/0.95 ((s_OM) != (s_g001)) % 0.75/0.95 (s_partOf (s_IQ) (s_g145)) % 0.75/0.95 (s_partOf (s_GN) (s_g011)) % 0.75/0.95 ((s_SR) != (s_MX)) % 0.75/0.95 ((s_AI) != (s_g019)) % 0.75/0.95 ((s_AM) != (s_g019)) % 0.75/0.95 (s_contains (s_g017) (s_CM)) % 0.75/0.95 ((s_MM) != (s_g019)) % 0.75/0.95 ((s_IS) != (s_MX)) % 0.75/0.95 ((s_g035) != (s_g013)) % 0.75/0.95 ((s_CN) != (s_g001)) % 0.75/0.95 ((s_CM) != (s_g003)) % 0.75/0.95 ((s_PM) != (s_g001)) % 0.75/0.95 ((s_g155) != (s_g001)) % 0.75/0.95 (s_partOf (s_g034) (s_g142)) % 0.75/0.95 ((s_LB) != (s_g019)) % 0.75/0.95 ((s_TP) != (s_g019)) % 0.75/0.95 ((s_TD) != (s_MX)) % 0.75/0.95 ((s_BW) != (s_g013)) % 0.75/0.95 ((s_RW) != (s_g001)) % 0.75/0.95 (s_partOf (s_LU) (s_g155)) % 0.75/0.95 ((s_IQ) != (s_g001)) % 0.75/0.95 ((s_AO) != (s_g019)) % 0.75/0.95 ((s_BM) != (s_g003)) % 0.75/0.95 ((s_NA) != (s_g003)) % 0.75/0.95 ((s_TZ) != (s_g419)) % 0.75/0.95 ((s_KP) != (s_g001)) % 0.75/0.95 ((s_EC) != (s_g019)) % 0.75/0.95 ((s_MW) != (s_MX)) % 0.75/0.95 ((s_MF) != (s_MX)) % 0.75/0.95 ((s_NE) != (s_MX)) % 0.75/0.95 ((s_DM) != (s_g419)) % 0.75/0.95 ((s_PF) != (s_MX)) % 0.75/0.95 (s_partOf (s_g150) (s_g001)) % 0.75/0.95 ((s_EH) != (s_g419)) % 0.75/0.95 ((s_PL) != (s_g419)) % 0.75/0.95 ((s_GH) != (s_g019)) % 0.75/0.95 (s_partOf (s_BY) (s_g172)) % 0.75/0.95 ((s_MO) != (s_g013)) % 0.75/0.95 (s_partOf (s_AE) (s_g145)) % 0.75/0.95 ((s_TL) != (s_MX)) % 0.75/0.95 ((s_GM) != (s_g003)) % 0.75/0.95 ((s_BO) != (s_g419)) % 0.75/0.95 ((s_CU) != (s_g419)) % 0.75/0.95 ((s_UG) != (s_g419)) % 0.75/0.95 (s_contains (s_g150) (s_g154)) % 0.75/0.95 ((s_MZ) != (s_g419)) % 0.75/0.95 (s_contains (s_g155) (s_DD)) % 0.75/0.95 ((s_AT) != (s_MX)) % 0.75/0.95 ((s_RU) != (s_g013)) % 0.75/0.95 ((s_RS) != (s_MX)) % 0.75/0.95 ((s_SZ) != (s_g019)) % 0.75/0.95 ((s_JE) != (s_g003)) % 0.75/0.95 ((s_BI) != (s_g019)) % 0.75/0.95 ((s_TJ) != (s_g003)) % 0.75/0.95 (s_contains (s_g001) (s_g009)) % 0.75/0.95 ((s_MN) != (s_MX)) % 0.75/0.95 (-. (s_contains (s_HK) (s_g013))) % 0.75/0.95 ((s_GQ) != (s_MX)) % 0.75/0.95 ((s_BM) != (s_g019)) % 0.75/0.95 (s_contains (s_g029) (s_TC)) % 0.75/0.95 ((s_g034) != (s_g003)) % 0.75/0.95 (s_contains (s_g039) (s_AD)) % 0.75/0.95 ((s_MN) != (s_g019)) % 0.75/0.95 ((s_KH) != (s_g003)) % 0.75/0.95 (s_contains (s_g172) (s_TM)) % 0.75/0.95 ((s_BD) != (s_g419)) % 0.75/0.95 ((s_SI) != (s_g003)) % 0.75/0.95 ((s_MC) != (s_g019)) % 0.75/0.95 ((s_NF) != (s_g019)) % 0.75/0.95 ((s_BF) != (s_g001)) % 0.75/0.95 (s_contains (s_g035) (s_VN)) % 0.75/0.95 (s_partOf (s_MH) (s_g057)) % 0.75/0.95 ((s_JO) != (s_g001)) % 0.75/0.95 ((s_TN) != (s_g003)) % 0.75/0.95 (s_contains (s_g151) (s_PL)) % 0.75/0.95 ((s_BW) != (s_MX)) % 0.75/0.95 ((s_NA) != (s_g013)) % 0.75/0.95 ((s_YT) != (s_g003)) % 0.75/0.95 ((s_HR) != (s_g013)) % 0.75/0.95 ((s_JO) != (s_g019)) % 0.75/0.95 ((s_LT) != (s_g001)) % 0.75/0.95 ((s_BG) != (s_g019)) % 0.75/0.95 (s_partOf (s_CG) (s_g017)) % 0.75/0.95 ((s_YD) != (s_g003)) % 0.75/0.95 (s_contains (s_g014) (s_MZ)) % 0.75/0.95 ((s_TZ) != (s_g003)) % 0.75/0.95 ((s_US) != (s_g003)) % 0.75/0.95 ((s_VA) != (s_g001)) % 0.75/0.95 ((s_TD) != (s_g001)) % 0.75/0.95 (s_partOf (s_CS) (s_g039)) % 0.75/0.95 (s_contains (s_g005) (s_EC)) % 0.75/0.95 ((s_MP) != (s_MX)) % 0.75/0.95 ((s_AN) != (s_g019)) % 0.75/0.95 ((s_HT) != (s_g003)) % 0.75/0.95 ((s_g030) != (s_g001)) % 0.75/0.95 ((s_MH) != (s_g019)) % 0.75/0.95 (s_partOf (s_NT) (s_g145)) % 0.75/0.95 ((s_DK) != (s_MX)) % 0.75/0.95 ((s_TO) != (s_g003)) % 0.75/0.95 (s_partOf (s_BM) (s_g021)) % 0.75/0.95 ((s_MU) != (s_MX)) % 0.75/0.95 ((s_GR) != (s_g001)) % 0.75/0.95 (s_contains (s_g035) (s_TH)) % 0.75/0.95 ((s_IS) != (s_g003)) % 0.75/0.95 ((s_g057) != (s_MX)) % 0.75/0.95 ((s_AX) != (s_g003)) % 0.75/0.95 ((s_HU) != (s_g003)) % 0.75/0.95 ((s_MW) != (s_g003)) % 0.75/0.95 (-. (s_contains (s_CN) (s_g019))) % 0.75/0.95 (s_partOf (s_JE) (s_g830)) % 0.75/0.95 ((s_CY) != (s_g019)) % 0.75/0.95 (s_contains (s_g002) (s_g011)) % 0.75/0.95 ((s_CI) != (s_g419)) % 0.75/0.95 ((s_VN) != (s_g419)) % 0.75/0.95 ((s_LT) != (s_MX)) % 0.75/0.95 (s_contains (s_g061) (s_AS)) % 0.75/0.95 ((s_PH) != (s_g019)) % 0.75/0.95 ((s_IL) != (s_MX)) % 0.75/0.95 ((s_AT) != (s_g419)) % 0.75/0.95 (s_contains (s_g019) (s_g021)) % 0.75/0.95 ((s_MG) != (s_MX)) % 0.75/0.95 ((s_DD) != (s_g013)) % 0.75/0.95 (s_partOf (s_NR) (s_g057)) % 0.75/0.95 (s_contains (s_g154) (s_DK)) % 0.75/0.95 ((s_AZ) != (s_g001)) % 0.75/0.95 ((s_IQ) != (s_MX)) % 0.75/0.95 ((s_AE) != (s_g419)) % 0.75/0.95 ((s_g035) != (s_g003)) % 0.75/0.95 (s_contains (s_g029) (s_BL)) % 0.75/0.95 ((s_SR) != (s_g001)) % 0.75/0.95 (s_partOf (s_OM) (s_g145)) % 0.75/0.95 ((s_MD) != (s_g013)) % 0.75/0.95 (s_partOf (s_BO) (s_g005)) % 0.75/0.95 (s_contains (s_g034) (s_IR)) % 0.75/0.95 ((s_PL) != (s_MX)) % 0.75/0.95 ((s_MS) != (s_g001)) % 0.75/0.95 ((s_g061) != (s_MX)) % 0.75/0.95 ((s_MV) != (s_g001)) % 0.75/0.95 ((s_LI) != (s_g013)) % 0.75/0.95 (s_partOf (s_NF) (s_g053)) % 0.75/0.95 (-. (s_contains (s_KR) (s_g419))) % 0.75/0.95 ((s_TG) != (s_MX)) % 0.75/0.95 (s_partOf (s_IM) (s_g154)) % 0.75/0.95 ((s_PG) != (s_g013)) % 0.75/0.95 ((s_ZA) != (s_g001)) % 0.75/0.95 (s_contains (s_g154) (s_IS)) % 0.75/0.95 ((s_MT) != (s_g019)) % 0.75/0.95 ((s_GR) != (s_g003)) % 0.75/0.95 (s_contains (s_g003) (s_g013)) % 0.75/0.95 ((s_EC) != (s_g003)) % 0.75/0.95 ((s_MT) != (s_g419)) % 0.75/0.95 (s_contains (s_g015) (s_DZ)) % 0.75/0.95 ((s_GA) != (s_MX)) % 0.75/0.95 ((s_CG) != (s_g419)) % 0.75/0.95 (s_contains (s_g145) (s_IL)) % 0.75/0.95 ((s_SD) != (s_g001)) % 0.75/0.95 ((s_WF) != (s_g003)) % 0.75/0.95 ((s_NT) != (s_g001)) % 0.75/0.95 ((s_ZM) != (s_g003)) % 0.75/0.95 (s_contains (s_g142) (s_g143)) % 0.75/0.95 ((s_SY) != (s_g419)) % 0.75/0.95 ((s_g154) != (s_g013)) % 0.75/0.95 ((s_FR) != (s_MX)) % 0.75/0.95 ((s_SJ) != (s_g419)) % 0.75/0.95 ((s_SN) != (s_g001)) % 0.75/0.95 ((s_MN) != (s_g419)) % 0.75/0.95 ((s_BW) != (s_g419)) % 0.75/0.95 ((s_LB) != (s_g001)) % 0.75/0.95 ((s_ET) != (s_g019)) % 0.75/0.95 (s_contains (s_g142) (s_g035)) % 0.75/0.95 ((s_VG) != (s_g001)) % 0.75/0.95 ((s_TP) != (s_MX)) % 0.75/0.95 ((s_MM) != (s_MX)) % 0.75/0.95 ((s_GN) != (s_g019)) % 0.75/0.95 ((s_HT) != (s_g013)) % 0.75/0.95 (s_contains (s_g019) (s_g005)) % 0.75/0.95 ((s_IL) != (s_g013)) % 0.75/0.95 (s_partOf (s_LA) (s_g035)) % 0.75/0.95 (s_contains (s_g145) (s_KW)) % 0.75/0.95 ((s_AX) != (s_g013)) % 0.75/0.95 ((s_CN) != (s_MX)) % 0.75/0.95 ((s_GP) != (s_g013)) % 0.75/0.95 ((s_PR) != (s_g003)) % 0.75/0.95 ((s_BT) != (s_MX)) % 0.75/0.95 (-. (s_contains (s_g030) (s_g003))) % 0.75/0.95 (s_partOf (s_KG) (s_g172)) % 0.75/0.95 ((s_PW) != (s_MX)) % 0.75/0.95 ((s_KH) != (s_g419)) % 0.75/0.95 ((s_SE) != (s_g003)) % 0.75/0.95 ((s_VA) != (s_g419)) % 0.75/0.95 ((s_IT) != (s_MX)) % 0.75/0.95 ((s_KG) != (s_g419)) % 0.75/0.95 ((s_GQ) != (s_g013)) % 0.75/0.95 ((s_KH) != (s_g019)) % 0.75/0.95 ((s_GH) != (s_g003)) % 0.75/0.95 (s_partOf (s_MT) (s_g039)) % 0.75/0.95 (s_contains (s_g062) (s_g034)) % 0.75/0.95 (s_partOf (s_AF) (s_g034)) % 0.75/0.95 ((s_WF) != (s_g013)) % 0.75/0.95 ((s_g155) != (s_g019)) % 0.75/0.95 (s_contains (s_g021) (s_GL)) % 0.75/0.95 (s_contains (s_g035) (s_SG)) % 0.75/0.95 ((s_NO) != (s_g001)) % 0.75/0.95 ((s_g151) != (s_g001)) % 0.75/0.95 (s_partOf (s_TM) (s_g172)) % 0.75/0.95 ((s_PG) != (s_MX)) % 0.75/0.95 ((s_AR) != (s_g003)) % 0.75/0.95 ((s_MT) != (s_g013)) % 0.75/0.95 ((s_PL) != (s_g013)) % 0.75/0.95 (-. (s_contains (s_KP) (s_g019))) % 0.75/0.95 ((s_VA) != (s_MX)) % 0.75/0.95 ((s_YU) != (s_g013)) % 0.75/0.95 ((s_KW) != (s_g013)) % 0.75/0.95 ((s_BA) != (s_g013)) % 0.75/0.95 (s_contains (s_g145) (s_YD)) % 0.75/0.95 ((s_TZ) != (s_g013)) % 0.75/0.95 ((s_MF) != (s_g013)) % 0.75/0.95 ((s_KP) != (s_g003)) % 0.75/0.95 ((s_SL) != (s_MX)) % 0.75/0.95 ((s_TL) != (s_g013)) % 0.75/0.95 (s_partOf (s_MV) (s_g034)) % 0.75/0.95 ((s_GD) != (s_g001)) % 0.75/0.95 ((s_FK) != (s_MX)) % 0.75/0.95 ((s_AM) != (s_g013)) % 0.75/0.95 (s_contains (s_g014) (s_RE)) % 0.75/0.95 ((s_MY) != (s_g419)) % 0.75/0.95 (s_contains (s_g154) (s_IE)) % 0.75/0.95 (s_contains (s_g013) (s_CR)) % 0.75/0.95 ((s_BS) != (s_g001)) % 0.75/0.95 ((s_g018) != (s_g003)) % 0.75/0.95 (-. (s_contains (s_KR) (s_g019))) % 0.75/0.95 (s_contains (s_g142) (s_g034)) % 0.75/0.95 ((s_FK) != (s_g419)) % 0.75/0.95 ((s_PY) != (s_g419)) % 0.75/0.95 (s_partOf (s_VA) (s_g039)) % 0.75/0.95 (s_partOf (s_KP) (s_g030)) % 0.75/0.95 (s_contains (s_g029) (s_VI)) % 0.75/0.95 ((s_KP) != (s_MX)) % 0.75/0.95 ((s_EG) != (s_g419)) % 0.75/0.95 ((s_CY) != (s_g001)) % 0.75/0.95 ((s_g061) != (s_g001)) % 0.75/0.95 (s_partOf (s_FO) (s_g154)) % 0.75/0.95 (s_contains (s_g155) (s_NL)) % 0.75/0.95 ((s_SN) != (s_g019)) % 0.75/0.95 (s_contains (s_g039) (s_YU)) % 0.75/0.95 ((s_MN) != (s_g001)) % 0.75/0.95 ((s_DJ) != (s_g001)) % 0.75/0.95 (s_partOf (s_IL) (s_g145)) % 0.75/0.95 ((s_ZM) != (s_g419)) % 0.75/0.95 ((s_FO) != (s_g019)) % 0.75/0.95 (-. (s_contains (s_CN) (s_g419))) % 0.75/0.95 ((s_HK) != (s_g003)) % 0.75/0.95 ((s_TM) != (s_MX)) % 0.75/0.95 ((s_EC) != (s_g013)) % 0.75/0.95 (s_contains (s_g005) (s_SR)) % 0.75/0.95 ((s_SL) != (s_g003)) % 0.75/0.95 ((s_TM) != (s_g013)) % 0.75/0.95 ((s_IR) != (s_g003)) % 0.75/0.95 ((s_US) != (s_MX)) % 0.75/0.95 ((s_g030) != (s_g019)) % 0.75/0.95 ((s_GY) != (s_g419)) % 0.75/0.95 (s_partOf (s_AX) (s_g154)) % 0.75/0.95 (s_contains (s_g143) (s_KZ)) % 0.75/0.95 ((s_BS) != (s_MX)) % 0.75/0.95 ((s_IN) != (s_g013)) % 0.75/0.95 (-. (s_contains (s_MN) (s_g419))) % 0.75/0.95 ((s_VN) != (s_MX)) % 0.75/0.95 ((s_BL) != (s_g019)) % 0.75/0.95 ((s_FO) != (s_MX)) % 0.75/0.95 ((s_LK) != (s_g019)) % 0.75/0.95 (s_partOf (s_BL) (s_g029)) % 0.75/0.95 (s_partOf (s_KE) (s_g014)) % 0.75/0.95 ((s_GU) != (s_g419)) % 0.75/0.95 ((s_JP) != (s_g003)) % 0.75/0.95 ((s_OM) != (s_g419)) % 0.75/0.95 ((s_g018) != (s_MX)) % 0.75/0.95 ((s_BR) != (s_g003)) % 0.75/0.95 ((s_MS) != (s_g019)) % 0.75/0.95 ((s_RU) != (s_g019)) % 0.75/0.95 ((s_TW) != (s_g419)) % 0.75/0.95 (s_contains (s_g155) (s_DE)) % 0.75/0.95 ((s_MZ) != (s_g001)) % 0.75/0.95 (s_partOf (s_g030) (s_g142)) % 0.75/0.95 (s_contains (s_g061) (s_TK)) % 0.75/0.95 (s_contains (s_g035) (s_BU)) % 0.75/0.95 ((s_AD) != (s_g001)) % 0.75/0.95 (s_contains (s_g014) (s_TZ)) % 0.75/0.95 ((s_GM) != (s_g001)) % 0.75/0.95 ((s_GR) != (s_MX)) % 0.75/0.95 (s_contains (s_g057) (s_KI)) % 0.75/0.95 ((s_PT) != (s_g419)) % 0.75/0.95 (s_partOf (s_RE) (s_g014)) % 0.75/0.95 (s_partOf (s_KH) (s_g035)) % 0.75/0.95 (s_partOf (s_g021) (s_g003)) % 0.75/0.95 ((s_CD) != (s_g003)) % 0.75/0.95 ((s_TW) != (s_g003)) % 0.75/0.95 (s_partOf (s_g053) (s_g009)) % 0.75/0.95 ((s_MY) != (s_MX)) % 0.75/0.95 ((s_SH) != (s_g419)) % 0.75/0.95 ((s_NU) != (s_g013)) % 0.75/0.95 ((s_BA) != (s_g019)) % 0.75/0.95 ((s_g034) != (s_g001)) % 0.75/0.95 ((s_AO) != (s_g003)) % 0.75/0.95 ((s_AE) != (s_g013)) % 0.75/0.95 ((s_TT) != (s_g001)) % 0.75/0.95 ((s_ME) != (s_MX)) % 0.75/0.95 (s_partOf (s_LS) (s_g018)) % 0.75/0.95 ((s_GG) != (s_g013)) % 0.75/0.95 ((s_BJ) != (s_g019)) % 0.75/0.95 ((s_IE) != (s_g003)) % 0.75/0.95 ((s_g015) != (s_MX)) % 0.75/0.95 ((s_BI) != (s_MX)) % 0.75/0.95 ((s_PR) != (s_g019)) % 0.75/0.95 (s_partOf (s_PM) (s_g021)) % 0.75/0.95 ((s_MS) != (s_MX)) % 0.75/0.95 ((s_GF) != (s_g419)) % 0.75/0.95 ((s_BG) != (s_g001)) % 0.75/0.95 ((s_QA) != (s_g003)) % 0.75/0.95 ((s_SD) != (s_g019)) % 0.75/0.95 (s_partOf (s_g143) (s_g062)) % 0.75/0.95 (s_contains (s_g014) (s_ZM)) % 0.75/0.95 ((s_MC) != (s_MX)) % 0.75/0.95 (s_partOf (s_HT) (s_g029)) % 0.75/0.95 ((s_g011) != (s_g001)) % 0.75/0.95 (s_partOf (s_JO) (s_g145)) % 0.75/0.95 ((s_TM) != (s_g419)) % 0.75/0.95 ((s_TP) != (s_g003)) % 0.75/0.95 (s_partOf (s_NU) (s_g061)) % 0.75/0.95 (s_contains (s_g029) (s_TT)) % 0.75/0.95 ((s_JP) != (s_MX)) % 0.75/0.95 ((s_JM) != (s_MX)) % 0.75/0.95 (s_partOf (s_CN) (s_g030)) % 0.75/0.95 ((s_ET) != (s_MX)) % 0.75/0.95 ((s_GA) != (s_g013)) % 0.75/0.95 ((s_SC) != (s_g001)) % 0.75/0.95 ((s_MK) != (s_g003)) % 0.75/0.95 ((s_LK) != (s_MX)) % 0.75/0.95 ((s_TK) != (s_g419)) % 0.75/0.95 ((s_CH) != (s_g003)) % 0.75/0.95 (s_partOf (s_SY) (s_g145)) % 0.75/0.95 (s_contains (s_g053) (s_NF)) % 0.75/0.95 ((s_SA) != (s_MX)) % 0.75/0.95 ((s_ZM) != (s_MX)) % 0.75/0.95 ((s_SZ) != (s_g001)) % 0.75/0.95 ((s_ZW) != (s_g019)) % 0.75/0.95 (s_partOf (s_g013) (s_g419)) % 0.75/0.95 ((s_EC) != (s_g419)) % 0.75/0.95 (s_contains (s_g145) (s_NT)) % 0.75/0.95 ((s_ET) != (s_g013)) % 0.75/0.95 ((s_LR) != (s_g003)) % 0.75/0.95 (s_contains (s_g142) (s_g062)) % 0.75/0.95 ((s_VU) != (s_MX)) % 0.75/0.95 ((s_g017) != (s_g001)) % 0.75/0.95 ((s_MP) != (s_g003)) % 0.75/0.95 ((s_EG) != (s_g003)) % 0.75/0.95 ((s_SA) != (s_g013)) % 0.75/0.95 ((s_VA) != (s_g019)) % 0.75/0.95 (s_partOf (s_BG) (s_g151)) % 0.75/0.95 ((s_QA) != (s_MX)) % 0.75/0.95 (s_partOf (s_BS) (s_g029)) % 0.75/0.95 ((s_SZ) != (s_MX)) % 0.75/0.95 ((s_PH) != (s_MX)) % 0.75/0.95 (s_partOf (s_MD) (s_g151)) % 0.75/0.95 ((s_IT) != (s_g019)) % 0.75/0.95 ((s_TN) != (s_g419)) % 0.75/0.95 (s_partOf (s_TV) (s_g061)) % 0.75/0.95 ((s_NZ) != (s_g019)) % 0.75/0.95 ((s_UY) != (s_g019)) % 0.75/0.95 (s_partOf (s_SG) (s_g035)) % 0.75/0.95 ((s_CO) != (s_g419)) % 0.75/0.95 ((s_g154) != (s_g001)) % 0.75/0.95 (s_contains (s_g057) (s_MP)) % 0.75/0.95 (s_contains (s_g172) (s_GE)) % 0.75/0.95 ((s_GQ) != (s_g419)) % 0.75/0.95 ((s_AN) != (s_g419)) % 0.75/0.95 ((s_VN) != (s_g001)) % 0.75/0.95 (s_partOf (s_SK) (s_g151)) % 0.75/0.95 ((s_BL) != (s_g013)) % 0.75/0.95 (s_partOf (s_GT) (s_g013)) % 0.75/0.95 ((s_ZR) != (s_g019)) % 0.75/0.95 (s_partOf (s_RU) (s_g151)) % 0.75/0.95 ((s_NL) != (s_g001)) % 0.75/0.95 ((s_DD) != (s_g003)) % 0.75/0.95 ((s_DJ) != (s_MX)) % 0.75/0.95 (s_partOf (s_MA) (s_g015)) % 0.75/0.95 (s_contains (s_g002) (s_g014)) % 0.75/0.95 ((s_DE) != (s_g001)) % 0.75/0.95 (s_partOf (s_LB) (s_g145)) % 0.75/0.95 ((s_GI) != (s_g013)) % 0.75/0.95 (s_partOf (s_KW) (s_g145)) % 0.75/0.95 (s_partOf (s_GE) (s_g145)) % 0.75/0.95 (s_partOf (s_MO) (s_g030)) % 0.75/0.95 (s_partOf (s_AO) (s_g017)) % 0.75/0.95 ((s_g062) != (s_g419)) % 0.75/0.95 (s_contains (s_g039) (s_IT)) % 0.75/0.95 ((s_CZ) != (s_g003)) % 0.75/0.95 ((s_BB) != (s_g019)) % 0.75/0.95 ((s_CI) != (s_g003)) % 0.75/0.95 ((s_BW) != (s_g003)) % 0.75/0.95 (s_contains (s_g001) (s_g150)) % 0.75/0.95 ((s_GI) != (s_g001)) % 0.75/0.95 ((s_FJ) != (s_g419)) % 0.75/0.95 (s_contains (s_g029) (s_MQ)) % 0.75/0.95 ((s_LK) != (s_g003)) % 0.75/0.95 ((s_AG) != (s_g419)) % 0.75/0.96 ((s_SG) != (s_g001)) % 0.75/0.96 (s_contains (s_g057) (s_MH)) % 0.75/0.96 ((s_ML) != (s_MX)) % 0.75/0.96 ((s_AL) != (s_g419)) % 0.75/0.96 ((s_GP) != (s_g003)) % 0.75/0.96 (s_partOf (s_TW) (s_g030)) % 0.75/0.96 (-. (s_contains (s_MO) (s_g419))) % 0.75/0.96 ((s_GN) != (s_g003)) % 0.75/0.96 ((s_MH) != (s_g013)) % 0.75/0.96 (-. (s_contains (s_HK) (s_g019))) % 0.75/0.96 ((s_BB) != (s_MX)) % 0.75/0.96 (s_contains (s_g143) (s_KG)) % 0.75/0.96 ((s_ME) != (s_g013)) % 0.75/0.96 (s_partOf (s_GG) (s_g154)) % 0.75/0.96 (-. (s_contains (s_TW) (s_g419))) % 0.75/0.96 ((s_GY) != (s_g013)) % 0.75/0.96 (-. (s_contains (s_CN) (s_MX))) % 0.75/0.96 (s_contains (s_g035) (s_PH)) % 0.75/0.96 ((s_ID) != (s_MX)) % 0.75/0.96 ((s_SY) != (s_MX)) % 0.75/0.96 ((s_PF) != (s_g013)) % 0.75/0.96 ((s_MD) != (s_g419)) % 0.75/0.96 ((s_KP) != (s_g013)) % 0.75/0.96 ((s_AF) != (s_g419)) % 0.75/0.96 ((s_BO) != (s_g001)) % 0.75/0.96 ((s_AN) != (s_g001)) % 0.75/0.96 ((s_BG) != (s_g003)) % 0.75/0.96 (s_partOf (s_GW) (s_g011)) % 0.75/0.96 ((s_ZR) != (s_g419)) % 0.75/0.96 ((s_AD) != (s_g019)) % 0.75/0.96 ((s_CA) != (s_g419)) % 0.75/0.96 (s_contains (s_g029) (s_MS)) % 0.75/0.96 (-. (s_contains (s_g030) (s_g001))) % 0.75/0.96 ((s_NG) != (s_g001)) % 0.75/0.96 ((s_IL) != (s_g019)) % 0.75/0.96 (s_contains (s_g015) (s_LY)) % 0.75/0.96 (s_contains (s_g061) (s_TV)) % 0.75/0.96 (s_contains (s_g011) (s_CV)) % 0.75/0.96 ((s_AO) != (s_MX)) % 0.75/0.96 (s_contains (s_g062) (s_g143)) % 0.75/0.96 ((s_SM) != (s_g013)) % 0.75/0.96 ((s_LS) != (s_g019)) % 0.75/0.96 (s_contains (s_g039) (s_ES)) % 0.75/0.96 ((s_MS) != (s_g419)) % 0.75/0.96 (s_partOf (s_QA) (s_g145)) % 0.75/0.96 (s_partOf (s_g057) (s_g009)) % 0.75/0.96 (s_contains (s_g039) (s_RS)) % 0.75/0.96 ((s_FX) != (s_g003)) % 0.75/0.96 ((s_SC) != (s_g419)) % 0.75/0.96 ((s_BH) != (s_g003)) % 0.75/0.96 ((s_FO) != (s_g003)) % 0.75/0.96 ((s_CA) != (s_g013)) % 0.75/0.96 (s_contains (s_g172) (s_KG)) % 0.75/0.96 (s_contains (s_g154) (s_NO)) % 0.75/0.96 (s_partOf (s_LC) (s_g029)) % 0.75/0.96 ((s_VE) != (s_g419)) % 0.75/0.96 ((s_SJ) != (s_MX)) % 0.75/0.96 ((s_NZ) != (s_g013)) % 0.75/0.96 (s_contains (s_g029) (s_KY)) % 0.75/0.96 (s_partOf (s_AL) (s_g039)) % 0.75/0.96 (s_partOf (s_GE) (s_g172)) % 0.75/0.96 ((s_PN) != (s_MX)) % 0.75/0.96 (s_contains (s_g029) (s_AN)) % 0.75/0.96 (s_contains (s_g150) (s_g039)) % 0.75/0.96 ((s_AU) != (s_g003)) % 0.75/0.96 (s_partOf (s_JE) (s_g154)) % 0.75/0.96 ((s_YU) != (s_g001)) % 0.75/0.96 ((s_AG) != (s_g003)) % 0.75/0.96 ((s_TZ) != (s_MX)) % 0.75/0.96 ((s_MR) != (s_g001)) % 0.75/0.96 ((s_KH) != (s_g001)) % 0.75/0.96 ((s_EE) != (s_g013)) % 0.75/0.96 ((s_PK) != (s_g419)) % 0.75/0.96 ((s_AT) != (s_g003)) % 0.75/0.96 ((s_g039) != (s_g013)) % 0.75/0.96 (s_contains (s_g035) (s_LA)) % 0.75/0.96 (s_partOf (s_g143) (s_g142)) % 0.75/0.96 ((s_DM) != (s_g001)) % 0.75/0.96 (s_partOf (s_ME) (s_g039)) % 0.75/0.96 (s_contains (s_g011) (s_NG)) % 0.75/0.96 ((s_MZ) != (s_g013)) % 0.75/0.96 ((s_RW) != (s_g013)) % 0.75/0.96 (s_contains (s_g013) (s_SV)) % 0.75/0.96 ((s_SG) != (s_g013)) % 0.75/0.96 (s_contains (s_g061) (s_PF)) % 0.75/0.96 ((s_BY) != (s_g003)) % 0.75/0.96 ((s_g011) != (s_g003)) % 0.75/0.96 ((s_g057) != (s_g001)) % 0.75/0.96 ((s_KI) != (s_g003)) % 0.75/0.96 ((s_g154) != (s_MX)) % 0.75/0.96 ((s_g011) != (s_g013)) % 0.75/0.96 ((s_TP) != (s_g001)) % 0.75/0.96 ((s_KZ) != (s_g001)) % 0.75/0.96 ((s_ZA) != (s_g013)) % 0.75/0.96 ((s_CV) != (s_g003)) % 0.75/0.96 (s_partOf (s_SH) (s_g011)) % 0.75/0.96 ((s_AU) != (s_g419)) % 0.75/0.96 ((s_SD) != (s_g003)) % 0.75/0.96 ((s_AM) != (s_MX)) % 0.75/0.96 ((s_HU) != (s_g001)) % 0.75/0.96 (s_partOf (s_g151) (s_g150)) % 0.75/0.96 (s_partOf (s_BF) (s_g011)) % 0.75/0.96 (-. (s_contains (s_TW) (s_g013))) % 0.75/0.96 ((s_BB) != (s_g419)) % 0.75/0.96 ((s_PF) != (s_g419)) % 0.75/0.96 ((s_AT) != (s_g001)) % 0.75/0.96 (s_contains (s_g029) (s_JM)) % 0.75/0.96 (s_contains (s_g172) (s_KZ)) % 0.75/0.96 (s_partOf (s_AZ) (s_g172)) % 0.75/0.96 ((s_BR) != (s_g013)) % 0.75/0.96 (-. (s_contains (s_KP) (s_g419))) % 0.75/0.96 (s_partOf (s_MG) (s_g014)) % 0.75/0.96 ((s_CD) != (s_g013)) % 0.75/0.96 ((s_ID) != (s_g419)) % 0.75/0.96 ((s_SI) != (s_g419)) % 0.75/0.96 ((s_NA) != (s_g019)) % 0.75/0.96 ((s_PF) != (s_g003)) % 0.75/0.96 (s_partOf (s_MC) (s_g155)) % 0.75/0.96 ((s_BO) != (s_g013)) % 0.75/0.96 ((s_CH) != (s_g419)) % 0.75/0.96 ((s_BS) != (s_g003)) % 0.75/0.96 ((s_GI) != (s_MX)) % 0.75/0.96 ((s_GD) != (s_g013)) % 0.75/0.96 ((s_EE) != (s_g001)) % 0.75/0.96 ((s_RW) != (s_g003)) % 0.75/0.96 ((s_GA) != (s_g003)) % 0.75/0.96 (s_contains (s_g005) (s_UY)) % 0.75/0.96 ((s_CF) != (s_g419)) % 0.75/0.96 ((s_PH) != (s_g001)) % 0.75/0.96 ((s_KM) != (s_g013)) % 0.75/0.96 ((s_DO) != (s_g001)) % 0.75/0.96 (s_partOf (s_TZ) (s_g014)) % 0.75/0.96 ((s_LU) != (s_MX)) % 0.75/0.96 ((s_DO) != (s_g019)) % 0.75/0.96 ((s_KR) != (s_g419)) % 0.75/0.96 ((s_SB) != (s_g013)) % 0.75/0.96 (s_contains (s_g145) (s_AE)) % 0.75/0.96 (s_contains (s_g009) (s_g057)) % 0.75/0.96 ((s_BL) != (s_g001)) % 0.75/0.96 ((s_KE) != (s_g003)) % 0.75/0.96 (s_contains (s_g145) (s_OM)) % 0.75/0.96 (s_partOf (s_SN) (s_g011)) % 0.75/0.96 ((s_VU) != (s_g419)) % 0.75/0.96 (s_partOf (s_EH) (s_g015)) % 0.75/0.96 (s_partOf (s_RW) (s_g014)) % 0.75/0.96 ((s_g039) != (s_g001)) % 0.75/0.96 ((s_LU) != (s_g003)) % 0.75/0.96 ((s_ZR) != (s_g013)) % 0.75/0.96 ((s_AG) != (s_g019)) % 0.75/0.96 (s_contains (s_g005) (s_VE)) % 0.75/0.96 ((s_SJ) != (s_g001)) % 0.75/0.96 (s_partOf (s_BH) (s_g145)) % 0.75/0.96 ((s_TT) != (s_g019)) % 0.75/0.96 (s_partOf (s_DM) (s_g029)) % 0.75/0.96 (s_contains (s_g017) (s_CG)) % 0.75/0.96 ((s_NL) != (s_g019)) % 0.75/0.96 (s_contains (s_g145) (s_SY)) % 0.75/0.96 ((s_TT) != (s_g003)) % 0.75/0.96 (s_partOf (s_KM) (s_g014)) % 0.75/0.96 ((s_CD) != (s_g019)) % 0.75/0.96 ((s_LT) != (s_g003)) % 0.75/0.96 ((s_FJ) != (s_MX)) % 0.75/0.96 (s_contains (s_g015) (s_EG)) % 0.75/0.96 (s_partOf (s_g011) (s_g002)) % 0.75/0.96 ((s_TK) != (s_g003)) % 0.75/0.96 ((s_AW) != (s_g003)) % 0.75/0.96 (s_partOf (s_VC) (s_g029)) % 0.75/0.96 ((s_g014) != (s_g419)) % 0.75/0.96 ((s_TC) != (s_g419)) % 0.75/0.96 ((s_ES) != (s_MX)) % 0.75/0.96 (s_contains (s_g014) (s_UG)) % 0.75/0.96 ((s_BU) != (s_MX)) % 0.75/0.96 ((s_PE) != (s_g003)) % 0.75/0.96 (s_contains (s_g005) (s_FK)) % 0.75/0.96 ((s_ZW) != (s_g003)) % 0.75/0.96 (s_contains (s_g039) (s_GI)) % 0.75/0.96 (s_partOf (s_HR) (s_g039)) % 0.75/0.96 ((s_NC) != (s_MX)) % 0.75/0.96 ((s_WS) != (s_g013)) % 0.75/0.96 ((s_RS) != (s_g419)) % 0.75/0.96 ((s_BN) != (s_g003)) % 0.75/0.96 (s_partOf (s_ZA) (s_g018)) % 0.75/0.96 (s_partOf (s_SZ) (s_g018)) % 0.75/0.96 ((s_FK) != (s_g001)) % 0.75/0.96 ((s_SN) != (s_g013)) % 0.75/0.96 ((s_ZA) != (s_g419)) % 0.75/0.96 ((s_PF) != (s_g019)) % 0.75/0.96 (s_contains (s_g035) (s_MY)) % 0.75/0.96 ((s_g035) != (s_MX)) % 0.75/0.96 ((s_GW) != (s_g003)) % 0.75/0.96 (s_contains (s_g029) (s_MF)) % 0.75/0.96 ((s_IS) != (s_g019)) % 0.75/0.96 ((s_EH) != (s_g003)) % 0.75/0.96 ((s_BT) != (s_g013)) % 0.75/0.96 ((s_FK) != (s_g013)) % 0.75/0.96 (s_partOf (s_DK) (s_g154)) % 0.75/0.96 (s_partOf (s_TJ) (s_g143)) % 0.75/0.96 ((s_LI) != (s_g001)) % 0.75/0.96 ((s_MZ) != (s_MX)) % 0.75/0.96 ((s_IN) != (s_MX)) % 0.75/0.96 ((s_TM) != (s_g019)) % 0.75/0.96 ((s_TK) != (s_g019)) % 0.75/0.96 ((s_UA) != (s_g013)) % 0.75/0.96 (s_contains (s_g014) (s_ZW)) % 0.75/0.96 ((s_KI) != (s_g019)) % 0.75/0.96 (s_partOf (s_AD) (s_g039)) % 0.75/0.96 ((s_JO) != (s_MX)) % 0.75/0.96 ((s_YT) != (s_g013)) % 0.75/0.96 ((s_MW) != (s_g419)) % 0.75/0.96 ((s_GD) != (s_g019)) % 0.75/0.96 (s_contains (s_g054) (s_VU)) % 0.75/0.96 ((s_BE) != (s_g001)) % 0.75/0.96 (s_contains (s_g034) (s_MV)) % 0.75/0.96 (s_contains (s_g145) (s_SA)) % 0.75/0.96 ((s_MK) != (s_g019)) % 0.75/0.96 ((s_LS) != (s_g001)) % 0.75/0.96 ((s_DJ) != (s_g003)) % 0.75/0.96 ((s_SG) != (s_g003)) % 0.75/0.96 ((s_RE) != (s_g419)) % 0.75/0.96 ((s_GF) != (s_g001)) % 0.75/0.96 ((s_KR) != (s_MX)) % 0.75/0.96 ((s_NC) != (s_g013)) % 0.75/0.96 ((s_YT) != (s_g419)) % 0.75/0.96 ((s_NC) != (s_g419)) % 0.75/0.96 (s_contains (s_g154) (s_IM)) % 0.75/0.96 ((s_HT) != (s_g419)) % 0.75/0.96 (s_contains (s_g150) (s_g155)) % 0.75/0.96 ((s_GH) != (s_g419)) % 0.75/0.96 ((s_DE) != (s_g419)) % 0.75/0.96 (s_partOf (s_DZ) (s_g015)) % 0.75/0.96 ((s_AM) != (s_g001)) % 0.75/0.96 (s_contains (s_g039) (s_SM)) % 0.75/0.96 ((s_CG) != (s_g003)) % 0.75/0.96 ((s_US) != (s_g019)) % 0.75/0.96 ((s_KY) != (s_MX)) % 0.75/0.96 (s_partOf (s_SV) (s_g013)) % 0.75/0.96 ((s_BD) != (s_g003)) % 0.75/0.96 (-. (s_contains (s_CN) (s_g003))) % 0.75/0.96 ((s_AG) != (s_g013)) % 0.75/0.96 ((s_MR) != (s_g003)) % 0.75/0.96 ((s_CD) != (s_MX)) % 0.75/0.96 (s_contains (s_g142) (s_g145)) % 0.75/0.96 (-. (s_contains (s_KP) (s_g003))) % 0.75/0.96 ((s_GM) != (s_g419)) % 0.75/0.96 ((s_MP) != (s_g013)) % 0.75/0.96 ((s_SY) != (s_g013)) % 0.75/0.96 ((s_BY) != (s_MX)) % 0.75/0.96 ((s_GW) != (s_g419)) % 0.75/0.96 (s_contains (s_g034) (s_BT)) % 0.75/0.96 ((s_MP) != (s_g001)) % 0.75/0.96 ((s_TG) != (s_g003)) % 0.75/0.96 ((s_IM) != (s_MX)) % 0.75/0.96 ((s_UA) != (s_g019)) % 0.75/0.96 ((s_KP) != (s_g019)) % 0.75/0.96 ((s_NA) != (s_g419)) % 0.75/0.96 ((s_AZ) != (s_g019)) % 0.75/0.96 ((s_QA) != (s_g019)) % 0.75/0.96 (s_contains (s_g019) (s_g029)) % 0.75/0.96 ((s_BH) != (s_g419)) % 0.75/0.96 (s_contains (s_g015) (s_SD)) % 0.75/0.96 ((s_MS) != (s_g013)) % 0.75/0.96 (s_partOf (s_MX) (s_g013)) % 0.75/0.96 (s_partOf (s_PF) (s_g061)) % 0.75/0.96 (s_partOf (s_GP) (s_g029)) % 0.75/0.96 ((s_KZ) != (s_g019)) % 0.75/0.96 (s_partOf (s_RO) (s_g151)) % 0.75/0.96 ((s_LA) != (s_g013)) % 0.75/0.96 (s_contains (s_g039) (s_CS)) % 0.75/0.96 (-. (s_contains (s_MO) (s_MX))) % 0.75/0.96 ((s_VE) != (s_g019)) % 0.75/0.96 ((s_TT) != (s_MX)) % 0.75/0.96 ((s_GB) != (s_g013)) % 0.75/0.96 ((s_KY) != (s_g419)) % 0.75/0.96 ((s_YU) != (s_g003)) % 0.75/0.96 ((s_g030) != (s_g003)) % 0.75/0.96 ((s_WS) != (s_MX)) % 0.75/0.96 ((s_RU) != (s_MX)) % 0.75/0.96 ((s_CH) != (s_MX)) % 0.75/0.96 ((s_ST) != (s_g001)) % 0.75/0.96 ((s_KG) != (s_g013)) % 0.75/0.96 ((s_AI) != (s_g013)) % 0.75/0.96 (s_partOf (s_g019) (s_g001)) % 0.75/0.96 (-. (s_contains (s_CN) (s_g001))) % 0.75/0.96 ((s_AG) != (s_MX)) % 0.75/0.96 ((s_ID) != (s_g003)) % 0.75/0.96 ((s_MK) != (s_g419)) % 0.75/0.96 ((s_JM) != (s_g003)) % 0.75/0.96 (s_partOf (s_SJ) (s_g154)) % 0.75/0.96 (s_contains (s_g017) (s_CD)) % 0.75/0.96 (s_partOf (s_g013) (s_g019)) % 0.75/0.96 ((s_GU) != (s_MX)) % 0.75/0.96 ((s_CU) != (s_g013)) % 0.75/0.96 (s_partOf (s_g054) (s_g009)) % 0.75/0.96 ((s_DK) != (s_g019)) % 0.75/0.96 ((s_BN) != (s_g001)) % 0.75/0.96 (s_contains (s_g154) (s_GB)) % 0.75/0.96 ((s_g145) != (s_g013)) % 0.75/0.96 (s_contains (s_g014) (s_KE)) % 0.75/0.96 ((s_AW) != (s_g019)) % 0.75/0.96 (s_contains (s_g151) (s_CZ)) % 0.75/0.96 ((s_ME) != (s_g001)) % 0.75/0.96 ((s_PR) != (s_g001)) % 0.75/0.96 (s_contains (s_g017) (s_TD)) % 0.75/0.96 ((s_UA) != (s_MX)) % 0.75/0.96 ((s_VI) != (s_g013)) % 0.75/0.96 (s_contains (s_g061) (s_CK)) % 0.75/0.96 ((s_KZ) != (s_g003)) % 0.75/0.96 ((s_SL) != (s_g419)) % 0.75/0.96 ((s_AI) != (s_g419)) % 0.75/0.96 ((s_BF) != (s_g019)) % 0.75/0.96 ((s_MQ) != (s_g019)) % 0.75/0.96 ((s_MG) != (s_g013)) % 0.75/0.96 (s_partOf (s_TO) (s_g061)) % 0.75/0.96 ((s_CL) != (s_g019)) % 0.75/0.96 (s_contains (s_g018) (s_ZA)) % 0.75/0.96 ((s_IR) != (s_MX)) % 0.75/0.96 (s_contains (s_g151) (s_RU)) % 0.75/0.96 ((s_GE) != (s_g013)) % 0.75/0.96 (s_contains (s_g172) (s_TJ)) % 0.75/0.96 (s_contains (s_g011) (s_MR)) % 0.75/0.96 (-. (s_contains (s_MN) (s_g019))) % 0.75/0.96 ((s_IN) != (s_g019)) % 0.75/0.96 ((s_NR) != (s_g419)) % 0.75/0.96 ((s_TG) != (s_g001)) % 0.75/0.96 ((s_BT) != (s_g003)) % 0.75/0.96 ((s_KN) != (s_g003)) % 0.75/0.96 (s_partOf (s_GU) (s_g057)) % 0.75/0.96 ((s_JE) != (s_g013)) % 0.75/0.96 ((s_BA) != (s_g419)) % 0.75/0.96 ((s_CM) != (s_g419)) % 0.75/0.96 ((s_AI) != (s_MX)) % 0.75/0.96 ((s_CF) != (s_g001)) % 0.75/0.96 ((s_NP) != (s_g003)) % 0.75/0.96 ((s_BM) != (s_MX)) % 0.75/0.96 ((s_KG) != (s_MX)) % 0.75/0.96 ((s_g145) != (s_g001)) % 0.75/0.96 ((s_LT) != (s_g019)) % 0.75/0.96 ((s_g035) != (s_g001)) % 0.75/0.96 (s_contains (s_g005) (s_BO)) % 0.75/0.96 ((s_PS) != (s_g013)) % 0.75/0.96 ((s_NZ) != (s_g001)) % 0.75/0.96 (s_partOf (s_KG) (s_g143)) % 0.75/0.96 (s_partOf (s_TC) (s_g029)) % 0.75/0.96 ((s_PT) != (s_g001)) % 0.75/0.96 ((s_SZ) != (s_g003)) % 0.75/0.96 ((s_SE) != (s_g419)) % 0.75/0.96 (s_partOf (s_g061) (s_g009)) % 0.75/0.96 ((s_VG) != (s_g019)) % 0.75/0.96 ((s_IE) != (s_g419)) % 0.75/0.96 (-. (s_contains (s_TW) (s_g003))) % 0.75/0.96 ((s_RO) != (s_g419)) % 0.75/0.96 ((s_PL) != (s_g001)) % 0.75/0.96 ((s_CL) != (s_g001)) % 0.75/0.96 ((s_MZ) != (s_g019)) % 0.75/0.96 ((s_AE) != (s_g019)) % 0.75/0.96 ((s_NZ) != (s_MX)) % 0.75/0.96 ((s_MC) != (s_g419)) % 0.75/0.96 (s_contains (s_g002) (s_g018)) % 0.75/0.96 (s_contains (s_g054) (s_FJ)) % 0.75/0.96 ((s_GN) != (s_g001)) % 0.75/0.96 (s_partOf (s_JM) (s_g029)) % 0.75/0.96 ((s_NE) != (s_g001)) % 0.75/0.96 ((s_CZ) != (s_g019)) % 0.75/0.96 (s_contains (s_g419) (s_g013)) % 0.75/0.96 (s_contains (s_g419) (s_g005)) % 0.75/0.96 ((s_LR) != (s_g419)) % 0.75/0.96 ((s_NA) != (s_g001)) % 0.75/0.96 ((s_g018) != (s_g013)) % 0.75/0.96 ((s_LU) != (s_g013)) % 0.75/0.96 ((s_YU) != (s_g019)) % 0.75/0.96 ((s_UG) != (s_g003)) % 0.75/0.96 ((s_BD) != (s_MX)) % 0.75/0.96 ((s_MM) != (s_g003)) % 0.75/0.96 ((s_IR) != (s_g013)) % 0.75/0.96 (s_partOf (s_TK) (s_g061)) % 0.75/0.96 (s_contains (s_g172) (s_AM)) % 0.75/0.96 ((s_GU) != (s_g013)) % 0.75/0.96 (s_contains (s_g011) (s_ML)) % 0.75/0.96 (s_contains (s_g035) (s_BN)) % 0.75/0.96 ((s_CS) != (s_g419)) % 0.75/0.96 ((s_UZ) != (s_g419)) % 0.75/0.96 (s_partOf (s_MN) (s_g030)) % 0.75/0.96 ((s_LC) != (s_g419)) % 0.75/0.96 ((s_NR) != (s_g003)) % 0.75/0.96 (s_contains (s_g030) (s_JP)) % 0.75/0.96 (s_contains (s_g029) (s_DM)) % 0.75/0.96 ((s_LC) != (s_g019)) % 0.75/0.96 (s_partOf (s_CK) (s_g061)) % 0.75/0.96 (s_contains (s_g011) (s_SH)) % 0.75/0.96 ((s_MV) != (s_g419)) % 0.75/0.96 ((s_AO) != (s_g419)) % 0.75/0.96 (s_contains (s_g029) (s_AI)) % 0.75/0.96 ((s_DK) != (s_g013)) % 0.75/0.96 (-. (s_contains (s_HK) (s_g003))) % 0.75/0.96 (s_partOf (s_FJ) (s_g054)) % 0.75/0.96 (s_contains (s_g830) (s_GG)) % 0.75/0.96 ((s_g015) != (s_g019)) % 0.75/0.96 (s_partOf (s_AW) (s_g029)) % 0.75/0.96 (s_partOf (s_g005) (s_g419)) % 0.75/0.96 (s_contains (s_g039) (s_VA)) % 0.75/0.96 (s_partOf (s_NC) (s_g054)) % 0.75/0.96 (s_contains (s_g002) (s_g015)) % 0.75/0.96 ((s_LT) != (s_g419)) % 0.75/0.96 (s_partOf (s_AN) (s_g029)) % 0.75/0.96 ((s_LI) != (s_g419)) % 0.75/0.96 (s_contains (s_g005) (s_CO)) % 0.75/0.96 ((s_GN) != (s_MX)) % 0.75/0.96 ((s_BJ) != (s_g013)) % 0.75/0.96 ((s_AZ) != (s_g419)) % 0.75/0.96 (s_partOf (s_g018) (s_g002)) % 0.75/0.96 ((s_SK) != (s_MX)) % 0.75/0.96 ((s_SN) != (s_g419)) % 0.75/0.96 ((s_VN) != (s_g019)) % 0.75/0.96 ((s_GF) != (s_g019)) % 0.75/0.96 ((s_CU) != (s_MX)) % 0.75/0.96 ((s_TR) != (s_g019)) % 0.75/0.96 ((s_BO) != (s_g019)) % 0.75/0.96 ((s_KN) != (s_g019)) % 0.75/0.96 ((s_BA) != (s_g001)) % 0.75/0.96 ((s_JP) != (s_g419)) % 0.75/0.96 ((s_CG) != (s_g013)) % 0.75/0.96 ((s_SZ) != (s_g013)) % 0.75/0.96 ((s_CN) != (s_g003)) % 0.75/0.96 ((s_JE) != (s_MX)) % 0.75/0.96 (s_partOf (s_AT) (s_g155)) % 0.75/0.96 (s_partOf (s_ID) (s_g035)) % 0.75/0.96 (s_contains (s_g005) (s_PE)) % 0.75/0.96 ((s_IE) != (s_g019)) % 0.75/0.96 ((s_PY) != (s_g003)) % 0.75/0.96 ((s_CS) != (s_MX)) % 0.75/0.96 ((s_ES) != (s_g019)) % 0.75/0.96 ((s_PK) != (s_MX)) % 0.75/0.96 ((s_g053) != (s_g419)) % 0.75/0.96 ((s_YD) != (s_g019)) % 0.75/0.96 ((s_g018) != (s_g001)) % 0.75/0.96 ((s_TV) != (s_MX)) % 0.75/0.96 ((s_PW) != (s_g013)) % 0.75/0.96 ((s_CV) != (s_g419)) % 0.75/0.96 ((s_SI) != (s_g001)) % 0.75/0.96 ((s_CZ) != (s_g013)) % 0.75/0.96 ((s_LK) != (s_g419)) % 0.75/0.96 ((s_MG) != (s_g019)) % 0.75/0.96 (s_contains (s_g054) (s_PG)) % 0.75/0.96 (s_partOf (s_TH) (s_g035)) % 0.75/0.96 (s_partOf (s_IE) (s_g154)) % 0.75/0.96 (s_contains (s_g011) (s_LR)) % 0.75/0.96 ((s_FM) != (s_MX)) % 0.75/0.96 ((s_g154) != (s_g003)) % 0.75/0.96 ((s_SA) != (s_g001)) % 0.75/0.96 ((s_TW) != (s_g001)) % 0.75/0.96 ((s_PG) != (s_g019)) % 0.75/0.96 ((s_OM) != (s_g019)) % 0.75/0.96 (s_partOf (s_VN) (s_g035)) % 0.75/0.96 (s_contains (s_g014) (s_RW)) % 0.75/0.96 (s_partOf (s_ES) (s_g039)) % 0.75/0.96 ((s_PY) != (s_MX)) % 0.75/0.96 ((s_g151) != (s_g019)) % 0.75/0.96 ((s_SU) != (s_MX)) % 0.75/0.96 ((s_DJ) != (s_g419)) % 0.75/0.96 ((s_ID) != (s_g013)) % 0.75/0.96 ((s_AI) != (s_g003)) % 0.75/0.96 ((s_MA) != (s_g013)) % 0.75/0.96 ((s_GR) != (s_g019)) % 0.75/0.96 (s_contains (s_g015) (s_MA)) % 0.75/0.96 ((s_g061) != (s_g419)) % 0.75/0.96 (s_contains (s_g029) (s_GD)) % 0.75/0.96 (s_partOf (s_g029) (s_g419)) % 0.75/0.96 (-. (s_contains (s_KR) (s_g001))) % 0.75/0.96 ((s_NT) != (s_MX)) % 0.75/0.96 ((s_HK) != (s_g013)) % 0.75/0.96 ((s_YD) != (s_g013)) % 0.75/0.96 ((s_g151) != (s_g013)) % 0.75/0.96 (s_partOf (s_TP) (s_g035)) % 0.75/0.96 ((s_KN) != (s_MX)) % 0.75/0.96 ((s_JO) != (s_g013)) % 0.75/0.96 (s_partOf (s_BR) (s_g005)) % 0.75/0.96 ((s_MM) != (s_g013)) % 0.75/0.96 ((s_NG) != (s_g019)) % 0.75/0.96 (s_contains (s_g172) (s_UZ)) % 0.75/0.96 (s_partOf (s_PW) (s_g057)) % 0.75/0.96 ((s_KR) != (s_g001)) % 0.75/0.96 ((s_GI) != (s_g003)) % 0.75/0.96 (s_partOf (s_g015) (s_g002)) % 0.75/0.96 ((s_g151) != (s_g419)) % 0.75/0.96 (-. (s_contains (s_KP) (s_g001))) % 0.75/0.96 ((s_AD) != (s_g013)) % 0.75/0.96 ((s_AU) != (s_g013)) % 0.75/0.96 (s_contains (s_g034) (s_IN)) % 0.75/0.96 ((s_GQ) != (s_g001)) % 0.75/0.96 ((s_PW) != (s_g003)) % 0.75/0.96 (s_partOf (s_CA) (s_g021)) % 0.75/0.96 ((s_CG) != (s_g019)) % 0.75/0.96 ((s_BA) != (s_MX)) % 0.75/0.96 ((s_WS) != (s_g019)) % 0.75/0.96 (s_contains (s_g014) (s_SC)) % 0.75/0.96 (s_partOf (s_CV) (s_g011)) % 0.75/0.96 ((s_DO) != (s_g013)) % 0.75/0.96 (s_partOf (s_CZ) (s_g151)) % 0.75/0.96 ((s_NL) != (s_MX)) % 0.75/0.96 ((s_YE) != (s_g013)) % 0.75/0.96 (s_partOf (s_BW) (s_g018)) % 0.75/0.96 (s_contains (s_g029) (s_CU)) % 0.75/0.96 ((s_HK) != (s_g019)) % 0.75/0.96 ((s_SL) != (s_g001)) % 0.75/0.96 ((s_TJ) != (s_g001)) % 0.75/0.96 (s_contains (s_g011) (s_BJ)) % 0.75/0.96 ((s_GL) != (s_g019)) % 0.75/0.96 (s_contains (s_g145) (s_AZ)) % 0.75/0.96 ((s_ZW) != (s_MX)) % 0.75/0.96 ((s_SU) != (s_g019)) % 0.75/0.96 ((s_GF) != (s_g013)) % 0.75/0.96 (s_contains (s_g155) (s_BE)) % 0.75/0.96 ((s_IS) != (s_g419)) % 0.75/0.96 ((s_BS) != (s_g419)) % 0.75/0.96 ((s_GE) != (s_g003)) % 0.75/0.96 ((s_TK) != (s_g001)) % 0.75/0.96 (s_partOf (s_TN) (s_g015)) % 0.75/0.96 (s_partOf (s_KZ) (s_g172)) % 0.75/0.96 (s_partOf (s_g003) (s_g019)) % 0.75/0.96 ((s_CL) != (s_g003)) % 0.75/0.96 (s_contains (s_g029) (s_DO)) % 0.75/0.96 (s_contains (s_g143) (s_TJ)) % 0.75/0.96 (s_partOf (s_VE) (s_g005)) % 0.75/0.96 (s_partOf (s_ZR) (s_g017)) % 0.75/0.96 ((s_ME) != (s_g019)) % 0.75/0.96 ((s_DK) != (s_g419)) % 0.75/0.96 ((s_CO) != (s_g001)) % 0.75/0.96 ((s_RO) != (s_MX)) % 0.75/0.96 ((s_BR) != (s_g419)) % 0.75/0.96 (s_contains (s_g830) (s_JE)) % 0.75/0.96 ((s_AS) != (s_g013)) % 0.75/0.96 ((s_MQ) != (s_g419)) % 0.75/0.96 (s_partOf (s_NL) (s_g155)) % 0.75/0.96 ((s_JP) != (s_g013)) % 0.75/0.96 (s_partOf (s_MQ) (s_g029)) % 0.75/0.96 (s_contains (s_g145) (s_AM)) % 0.75/0.96 ((s_KW) != (s_g019)) % 0.75/0.96 ((s_PN) != (s_g019)) % 0.75/0.96 ((s_TG) != (s_g019)) % 0.75/0.96 (s_partOf (s_AG) (s_g029)) % 0.75/0.96 ((s_HT) != (s_MX)) % 0.75/0.96 ((s_TJ) != (s_g419)) % 0.75/0.96 ((s_MO) != (s_g003)) % 0.75/0.96 ((s_AX) != (s_g001)) % 0.75/0.96 ((s_AS) != (s_g001)) % 0.75/0.96 (s_contains (s_g057) (s_PW)) % 0.75/0.96 ((s_KE) != (s_MX)) % 0.75/0.96 (s_partOf (s_CY) (s_g145)) % 0.75/0.96 ((s_AZ) != (s_MX)) % 0.75/0.96 ((s_BE) != (s_MX)) % 0.75/0.96 ((s_RS) != (s_g013)) % 0.75/0.96 ((s_FX) != (s_g001)) % 0.75/0.96 ((s_VG) != (s_g419)) % 0.75/0.96 ((s_MF) != (s_g001)) % 0.75/0.96 (s_contains (s_g039) (s_ME)) % 0.75/0.96 ((s_BD) != (s_g013)) % 0.75/0.96 ((s_BN) != (s_g019)) % 0.75/0.96 ((s_PL) != (s_g003)) % 0.75/0.96 ((s_BH) != (s_g019)) % 0.75/0.96 ((s_SM) != (s_g019)) % 0.75/0.96 ((s_MD) != (s_g001)) % 0.75/0.96 ((s_AZ) != (s_g013)) % 0.75/0.96 ((s_NR) != (s_g001)) % 0.75/0.96 (s_contains (s_g061) (s_WS)) % 0.75/0.96 (s_contains (s_g029) (s_KN)) % 0.75/0.96 ((s_EE) != (s_g003)) % 0.75/0.96 ((s_KW) != (s_g419)) % 0.75/0.96 ((s_ET) != (s_g003)) % 0.75/0.96 ((s_g034) != (s_g419)) % 0.75/0.96 ((s_NE) != (s_g013)) % 0.75/0.96 ((s_ZA) != (s_g019)) % 0.75/0.96 ((s_TR) != (s_MX)) % 0.75/0.96 ((s_SI) != (s_g013)) % 0.75/0.96 ((s_SH) != (s_g003)) % 0.75/0.96 ((s_PS) != (s_g419)) % 0.75/0.96 ((s_BE) != (s_g003)) % 0.75/0.96 ((s_CU) != (s_g019)) % 0.75/0.96 ((s_GW) != (s_g013)) % 0.75/0.96 (s_partOf (s_IN) (s_g034)) % 0.75/0.96 ((s_BT) != (s_g001)) % 0.75/0.96 ((s_KR) != (s_g013)) % 0.75/0.96 ((s_TN) != (s_g019)) % 0.75/0.96 ((s_SN) != (s_g003)) % 0.75/0.96 ((s_BN) != (s_g419)) % 0.75/0.96 (s_partOf (s_MF) (s_g029)) % 0.75/0.96 ((s_CK) != (s_g013)) % 0.75/0.96 ((s_TO) != (s_g013)) % 0.75/0.96 ((s_BI) != (s_g419)) % 0.75/0.96 (s_contains (s_g014) (s_ER)) % 0.75/0.96 ((s_WF) != (s_g001)) % 0.75/0.96 ((s_ID) != (s_g001)) % 0.75/0.96 ((s_CK) != (s_g001)) % 0.75/0.96 ((s_SC) != (s_g003)) % 0.75/0.96 ((s_NT) != (s_g019)) % 0.75/0.96 ((s_RO) != (s_g013)) % 0.75/0.96 ((s_LV) != (s_g013)) % 0.75/0.96 ((s_GE) != (s_g019)) % 0.75/0.96 ((s_IR) != (s_g019)) % 0.75/0.96 (s_contains (s_g151) (s_RO)) % 0.75/0.96 (s_contains (s_g011) (s_BF)) % 0.75/0.96 (s_contains (s_g019) (s_g013)) % 0.75/0.96 (s_contains (s_g151) (s_HU)) % 0.75/0.96 ((s_QA) != (s_g001)) % 0.75/0.96 ((s_IE) != (s_g013)) % 0.75/0.96 ((s_LY) != (s_g419)) % 0.75/0.96 ((s_HK) != (s_g419)) % 0.75/0.96 ((s_AL) != (s_g013)) % 0.75/0.96 ((s_KG) != (s_g019)) % 0.75/0.96 ((s_NP) != (s_g001)) % 0.75/0.96 ((s_MK) != (s_g013)) % 0.75/0.96 ((s_BF) != (s_g419)) % 0.75/0.96 ((s_FM) != (s_g001)) % 0.75/0.96 (s_contains (s_g011) (s_GM)) % 0.75/0.96 (-. (s_contains (s_JP) (s_MX))) % 0.75/0.96 ((s_PY) != (s_g001)) % 0.75/0.96 (s_contains (s_g029) (s_HT)) % 0.75/0.96 ((s_MT) != (s_MX)) % 0.75/0.96 ((s_BY) != (s_g019)) % 0.75/0.96 (s_partOf (s_CU) (s_g029)) % 0.75/0.96 (s_contains (s_g154) (s_LT)) % 0.75/0.96 ((s_GN) != (s_g419)) % 0.75/0.96 ((s_VI) != (s_g003)) % 0.75/0.96 ((s_ZW) != (s_g419)) % 0.75/0.96 ((s_CI) != (s_g001)) % 0.75/0.96 ((s_g057) != (s_g003)) % 0.75/0.96 ((s_SM) != (s_g003)) % 0.75/0.96 ((s_MC) != (s_g003)) % 0.75/0.96 ((s_BO) != (s_MX)) % 0.75/0.96 ((s_BE) != (s_g419)) % 0.75/0.96 ((s_g018) != (s_g419)) % 0.75/0.96 (-. (s_contains (s_KR) (s_g013))) % 0.75/0.96 ((s_MU) != (s_g013)) % 0.75/0.96 (s_contains (s_g145) (s_LB)) % 0.75/0.96 ((s_LI) != (s_MX)) % 0.75/0.96 ((s_MV) != (s_g019)) % 0.75/0.96 ((s_BR) != (s_MX)) % 0.75/0.96 ((s_VG) != (s_g003)) % 0.75/0.96 (s_partOf (s_GB) (s_g154)) % 0.75/0.96 ((s_BH) != (s_g001)) % 0.75/0.96 ((s_ZM) != (s_g019)) % 0.75/0.96 (s_contains (s_g013) (s_HN)) % 0.75/0.96 ((s_LT) != (s_g013)) % 0.75/0.96 ((s_GH) != (s_MX)) % 0.75/0.96 ((s_BF) != (s_g013)) % 0.75/0.96 ((s_MT) != (s_g003)) % 0.75/0.96 ((s_SJ) != (s_g003)) % 0.75/0.96 ((s_CK) != (s_g003)) % 0.75/0.96 ((s_TL) != (s_g419)) % 0.75/0.96 ((s_GH) != (s_g013)) % 0.75/0.96 ((s_JE) != (s_g419)) % 0.75/0.96 ((s_UA) != (s_g419)) % 0.75/0.96 ((s_ID) != (s_g019)) % 0.75/0.96 ((s_ZA) != (s_g003)) % 0.75/0.96 (s_partOf (s_SM) (s_g039)) % 0.75/0.96 ((s_BB) != (s_g013)) % 0.75/0.96 (s_contains (s_g005) (s_BR)) % 0.75/0.96 ((s_LV) != (s_g419)) % 0.75/0.96 (s_contains (s_g021) (s_CA)) % 0.75/0.96 (s_partOf (s_g062) (s_g142)) % 0.75/0.96 (s_contains (s_g011) (s_TG)) % 0.75/0.96 ((s_AF) != (s_g001)) % 0.75/0.96 ((s_PS) != (s_MX)) % 0.75/0.96 ((s_g053) != (s_g019)) % 0.75/0.96 (s_partOf (s_BD) (s_g034)) % 0.75/0.96 ((s_TW) != (s_MX)) % 0.75/0.96 ((s_SI) != (s_MX)) % 0.75/0.96 (s_contains (s_g151) (s_BY)) % 0.75/0.96 ((s_VU) != (s_g001)) % 0.75/0.96 ((s_JO) != (s_g419)) % 0.75/0.96 ((s_AO) != (s_g001)) % 0.75/0.96 ((s_UZ) != (s_MX)) % 0.75/0.96 ((s_DK) != (s_g001)) % 0.75/0.96 ((s_CM) != (s_MX)) % 0.75/0.96 ((s_DJ) != (s_g019)) % 0.75/0.96 ((s_WF) != (s_g019)) % 0.75/0.96 ((s_RS) != (s_g003)) % 0.75/0.96 ((s_IT) != (s_g013)) % 0.75/0.96 ((s_GG) != (s_g419)) % 0.75/0.96 ((s_ML) != (s_g419)) % 0.75/0.96 ((s_ER) != (s_g419)) % 0.75/0.96 (s_contains (s_g061) (s_WF)) % 0.75/0.96 ((s_WF) != (s_g419)) % 0.75/0.96 ((s_AF) != (s_g019)) % 0.75/0.96 (-. (s_contains (s_TW) (s_g019))) % 0.75/0.96 ((s_NU) != (s_g001)) % 0.75/0.96 ((s_LB) != (s_g419)) % 0.75/0.96 (s_partOf (s_HU) (s_g151)) % 0.75/0.96 ((s_TL) != (s_g001)) % 0.75/0.96 (s_contains (s_g145) (s_TR)) % 0.75/0.96 (s_contains (s_g145) (s_PS)) % 0.75/0.96 (s_contains (s_g009) (s_g053)) % 0.75/0.96 ((s_SO) != (s_g019)) % 0.75/0.96 ((s_DD) != (s_MX)) % 0.75/0.96 ((s_VA) != (s_g013)) % 0.75/0.96 ((s_PK) != (s_g019)) % 0.75/0.96 ((s_GQ) != (s_g003)) % 0.75/0.96 (s_partOf (s_LY) (s_g015)) % 0.75/0.96 ((s_BB) != (s_g001)) % 0.75/0.96 (s_partOf (s_GL) (s_g021)) % 0.75/0.96 ((s_JM) != (s_g001)) % 0.75/0.96 ((s_MA) != (s_g419)) % 0.75/0.96 (s_partOf (s_CH) (s_g155)) % 0.75/0.96 (-. (s_contains (s_MO) (s_g003))) % 0.75/0.96 (s_partOf (s_PG) (s_g054)) % 0.75/0.96 ((s_g034) != (s_MX)) % 0.75/0.96 ((s_CY) != (s_MX)) % 0.75/0.96 (s_contains (s_g005) (s_AR)) % 0.75/0.96 ((s_PG) != (s_g001)) % 0.75/0.96 ((s_BB) != (s_g003)) % 0.75/0.96 (s_contains (s_g021) (s_US)) % 0.75/0.96 (s_partOf (s_LR) (s_g011)) % 0.75/0.96 (s_contains (s_g003) (s_g021)) % 0.75/0.96 ((s_GL) != (s_g003)) % 0.75/0.96 (s_partOf (s_g021) (s_g019)) % 0.75/0.96 ((s_ZR) != (s_MX)) % 0.75/0.96 ((s_g145) != (s_g019)) % 0.75/0.96 ((s_g053) != (s_g003)) % 0.75/0.96 ((s_g155) != (s_g003)) % 0.75/0.96 (s_contains (s_g172) (s_AZ)) % 0.75/0.96 (s_partOf (s_SC) (s_g014)) % 0.75/0.96 ((s_LI) != (s_g019)) % 0.75/0.96 ((s_FJ) != (s_g003)) % 0.75/0.96 ((s_AU) != (s_MX)) % 0.75/0.96 (s_contains (s_g019) (s_g419)) % 0.75/0.96 (-. (s_contains (s_JP) (s_g013))) % 0.75/0.96 ((s_SB) != (s_g001)) % 0.75/0.96 ((s_CA) != (s_MX)) % 0.75/0.96 ((s_CY) != (s_g003)) % 0.75/0.96 (-. (s_contains (s_KP) (s_MX))) % 0.75/0.96 ((s_MD) != (s_MX)) % 0.75/0.96 (s_partOf (s_LV) (s_g154)) % 0.75/0.96 ((s_IE) != (s_g001)) % 0.75/0.96 (s_partOf (s_GA) (s_g017)) % 0.75/0.96 (s_contains (s_g011) (s_CI)) % 0.75/0.96 (s_partOf (s_MU) (s_g014)) % 0.75/0.96 ((s_AN) != (s_g003)) % 0.75/0.96 (s_contains (s_g001) (s_g019)) % 0.75/0.96 (s_contains (s_g030) (s_KP)) % 0.75/0.96 (s_partOf (s_MK) (s_g039)) % 0.75/0.96 (s_contains (s_g155) (s_FR)) % 0.75/0.96 ((s_ZA) != (s_MX)) % 0.75/0.96 (s_partOf (s_FM) (s_g057)) % 0.75/0.96 ((s_SD) != (s_g419)) % 0.75/0.96 ((s_EG) != (s_g001)) % 0.75/0.96 ((s_DE) != (s_g013)) % 0.75/0.96 ((s_BU) != (s_g001)) % 0.75/0.96 ((s_NO) != (s_g013)) % 0.75/0.96 ((s_MY) != (s_g013)) % 0.75/0.96 ((s_KE) != (s_g419)) % 0.75/0.96 ((s_HU) != (s_g419)) % 0.75/0.96 ((s_RE) != (s_g001)) % 0.75/0.96 ((s_g018) != (s_g019)) % 0.75/0.96 ((s_NF) != (s_g001)) % 0.75/0.96 ((s_g054) != (s_g013)) % 0.75/0.96 (s_partOf (s_BA) (s_g039)) % 0.75/0.96 (s_partOf (s_PL) (s_g151)) % 0.75/0.96 (s_contains (s_g154) (s_FI)) % 0.75/0.96 (-. (s_contains (s_MN) (s_g003))) % 0.75/0.96 ((s_VG) != (s_MX)) % 0.75/0.96 ((s_SE) != (s_g001)) % 0.75/0.96 ((s_NG) != (s_MX)) % 0.75/0.96 ((s_AS) != (s_MX)) % 0.75/0.96 (s_contains (s_g053) (s_NZ)) % 0.75/0.96 ((s_IN) != (s_g419)) % 0.75/0.96 ((s_IM) != (s_g419)) % 0.75/0.96 ((s_SZ) != (s_g419)) % 0.75/0.96 ((s_PT) != (s_g003)) % 0.75/0.96 ((s_g145) != (s_g003)) % 0.75/0.96 ((s_DM) != (s_g013)) % 0.75/0.96 ((s_KI) != (s_g001)) % 0.75/0.96 (s_contains (s_g039) (s_MK)) % 0.75/0.96 (s_partOf (s_JP) (s_g030)) % 0.75/0.96 ((s_MG) != (s_g001)) % 0.75/0.96 ((s_YU) != (s_MX)) % 0.75/0.96 ((s_AW) != (s_g001)) % 0.75/0.96 ((s_NR) != (s_MX)) % 0.75/0.96 (-. (s_contains (s_JP) (s_g001))) % 0.75/0.96 ((s_GA) != (s_g001)) % 0.75/0.96 (s_contains (s_g034) (s_AF)) % 0.75/0.96 (s_contains (s_g039) (s_MT)) % 0.75/0.96 (s_partOf (s_MZ) (s_g014)) % 0.75/0.96 ((s_HK) != (s_MX)) % 0.75/0.96 ((s_LR) != (s_g019)) % 0.75/0.96 ((s_VE) != (s_g003)) % 0.75/0.96 (s_contains (s_g145) (s_IQ)) % 0.75/0.96 ((s_QA) != (s_g419)) % 0.75/0.96 ((s_GD) != (s_MX)) % 0.75/0.96 ((s_DZ) != (s_g003)) % 0.75/0.96 ((s_NC) != (s_g001)) % 0.75/0.96 (s_contains (s_g145) (s_JO)) % 0.75/0.96 (s_contains (s_g002) (s_g017)) % 0.75/0.96 (s_contains (s_g017) (s_CF)) % 0.75/0.96 (s_partOf (s_GH) (s_g011)) % 0.75/0.96 ((s_AE) != (s_MX)) % 0.75/0.96 ((s_VC) != (s_g019)) % 0.75/0.96 ((s_g017) != (s_MX)) % 0.75/0.96 ((s_g062) != (s_g019)) % 0.75/0.96 ((s_BM) != (s_g419)) % 0.75/0.96 ((s_g011) != (s_g419)) % 0.75/0.96 ((s_KI) != (s_g419)) % 0.75/0.96 ((s_BD) != (s_g019)) % 0.75/0.96 ((s_TK) != (s_g013)) % 0.75/0.96 (s_contains (s_g017) (s_AO)) % 0.75/0.96 ((s_PK) != (s_g013)) % 0.75/0.96 ((s_IE) != (s_MX)) % 0.75/0.96 ((s_LY) != (s_MX)) % 0.75/0.96 ((s_CI) != (s_g019)) % 0.75/0.96 (s_partOf (s_ZW) (s_g014)) % 0.75/0.96 ((s_TR) != (s_g419)) % 0.75/0.96 ((s_g053) != (s_g001)) % 0.75/0.96 ((s_NO) != (s_g003)) % 0.75/0.96 (s_partOf (s_FK) (s_g005)) % 0.75/0.96 (s_contains (s_g155) (s_LI)) % 0.75/0.96 (s_partOf (s_TR) (s_g145)) % 0.75/0.96 ((s_UA) != (s_g001)) % 0.75/0.96 ((s_NC) != (s_g003)) % 0.75/0.96 ((s_MY) != (s_g019)) % 0.75/0.96 ((s_ST) != (s_g419)) % 0.75/0.96 (s_contains (s_g014) (s_MU)) % 0.75/0.96 ((s_GN) != (s_g013)) % 0.75/0.96 ((s_BJ) != (s_g419)) % 0.75/0.96 ((s_LA) != (s_g001)) % 0.75/0.96 (s_contains (s_g172) (s_RU)) % 0.75/0.96 ((s_IQ) != (s_g003)) % 0.75/0.96 ((s_TD) != (s_g419)) % 0.75/0.96 ((s_BM) != (s_g001)) % 0.75/0.96 (s_contains (s_g014) (s_KM)) % 0.75/0.96 ((s_AD) != (s_MX)) % 0.75/0.96 (s_contains (s_g005) (s_GF)) % 0.75/0.96 (s_contains (s_g151) (s_MD)) % 0.75/0.96 ((s_FR) != (s_g013)) % 0.75/0.96 ((s_US) != (s_g419)) % 0.75/0.96 (s_partOf (s_CR) (s_g013)) % 0.75/0.96 ((s_GQ) != (s_g019)) % 0.75/0.96 ((s_TO) != (s_g019)) % 0.75/0.96 (s_partOf (s_ZM) (s_g014)) % 0.75/0.96 (s_contains (s_g021) (s_PM)) % 0.75/0.96 (s_partOf (s_YE) (s_g145)) % 0.75/0.96 ((s_TW) != (s_g013)) % 0.75/0.96 ((s_NP) != (s_g013)) % 0.75/0.96 (s_partOf (s_PY) (s_g005)) % 0.75/0.96 ((s_YT) != (s_g001)) % 0.75/0.96 ((s_BD) != (s_g001)) % 0.75/0.96 ((s_PN) != (s_g003)) % 0.75/0.96 ((s_GL) != (s_g419)) % 0.75/0.96 ((s_AU) != (s_g019)) % 0.75/0.96 (s_contains (s_g145) (s_YE)) % 0.75/0.96 ((s_AX) != (s_g419)) % 0.75/0.96 ((s_g014) != (s_g019)) % 0.75/0.96 (s_partOf (s_PN) (s_g061)) % 0.75/0.96 ((s_VI) != (s_MX)) % 0.75/0.96 (s_partOf (s_ER) (s_g014)) % 0.75/0.96 ((s_CI) != (s_MX)) % 0.75/0.96 ((s_AW) != (s_MX)) % 0.75/0.96 ((s_AL) != (s_g001)) % 0.75/0.96 (s_contains (s_g039) (s_SI)) % 0.75/0.96 (s_partOf (s_g035) (s_g142)) % 0.75/0.96 ((s_TH) != (s_g003)) % 0.75/0.96 (s_contains (s_g143) (s_UZ)) % 0.75/0.96 ((s_PM) != (s_MX)) % 0.75/0.96 ((s_UG) != (s_g013)) % 0.75/0.96 (s_contains (s_g419) (s_g029)) % 0.75/0.96 ((s_ML) != (s_g001)) % 0.75/0.96 ((s_MW) != (s_g019)) % 0.75/0.96 (s_partOf (s_TL) (s_g035)) % 0.75/0.96 ((s_RE) != (s_g013)) % 0.75/0.96 ((s_PT) != (s_g013)) % 0.75/0.96 ((s_TN) != (s_MX)) % 0.75/0.96 ((s_g054) != (s_g001)) % 0.75/0.96 (s_partOf (s_SD) (s_g015)) % 0.75/0.96 (s_partOf (s_SO) (s_g014)) % 0.75/0.96 (s_partOf (s_SU) (s_g151)) % 0.75/0.96 (-. (s_contains (s_TW) (s_g001))) % 0.75/0.96 ((s_SK) != (s_g013)) % 0.75/0.96 (s_partOf (s_AS) (s_g061)) % 0.75/0.96 ((s_g015) != (s_g013)) % 0.75/0.96 ((s_SA) != (s_g003)) % 0.75/0.96 (-. (s_contains (s_MN) (s_g013))) % 0.75/0.96 ((s_LA) != (s_g419)) % 0.75/0.96 ((s_CS) != (s_g001)) % 0.75/0.96 (s_contains (s_g150) (s_g151)) % 0.75/0.96 ((s_BG) != (s_g419)) % 0.75/0.96 ((s_BJ) != (s_g001)) % 0.75/0.96 ((s_SC) != (s_g019)) % 0.75/0.96 ((s_TP) != (s_g013)) % 0.75/0.96 (s_partOf (s_UZ) (s_g143)) % 0.75/0.96 ((s_LB) != (s_MX)) % 0.75/0.96 ((s_g062) != (s_g001)) % 0.75/0.96 ((s_BS) != (s_g013)) % 0.75/0.96 ((s_g039) != (s_g419)) % 0.75/0.96 (s_partOf (s_BN) (s_g035)) % 0.75/0.96 (s_contains (s_g029) (s_BS)) % 0.75/0.96 ((s_TV) != (s_g013)) % 0.75/0.96 ((s_PW) != (s_g019)) % 0.75/0.96 ((s_NT) != (s_g419)) % 0.75/0.96 ((s_PE) != (s_g001)) % 0.75/0.96 ((s_MG) != (s_g003)) % 0.75/0.96 (s_partOf (s_g154) (s_g150)) % 0.75/0.96 ((s_EC) != (s_g001)) % 0.75/0.96 (s_partOf (s_WS) (s_g061)) % 0.75/0.96 ((s_ST) != (s_MX)) % 0.75/0.96 ((s_TH) != (s_g419)) % 0.75/0.96 (s_partOf (s_RU) (s_g172)) % 0.75/0.96 ((s_MZ) != (s_g003)) % 0.75/0.96 ((s_SG) != (s_g019)) % 0.75/0.96 (-. (s_contains (s_HK) (s_g001))) % 0.75/0.96 ((s_DZ) != (s_g001)) % 0.75/0.96 ((s_NA) != (s_MX)) % 0.75/0.96 ((s_GE) != (s_MX)) % 0.75/0.96 ((s_JE) != (s_g019)) % 0.75/0.96 ((s_BR) != (s_g001)) % 0.75/0.96 ((s_g151) != (s_MX)) % 0.75/0.96 ((s_TP) != (s_g419)) % 0.75/0.96 ((s_SB) != (s_g419)) % 0.75/0.96 ((s_CV) != (s_g019)) % 0.75/0.96 ((s_VE) != (s_g001)) % 0.75/0.96 (-. (s_contains (s_g030) (s_MX))) % 0.75/0.96 ((s_NF) != (s_MX)) % 0.75/0.96 ((s_GP) != (s_g019)) % 0.75/0.96 (s_partOf (s_g002) (s_g001)) % 0.75/0.96 ((s_PS) != (s_g019)) % 0.75/0.96 ((s_WS) != (s_g001)) % 0.75/0.96 (s_contains (s_g011) (s_GN)) % 0.75/0.96 ((s_CV) != (s_g013)) % 0.75/0.96 ((s_DE) != (s_g003)) % 0.75/0.96 ((s_g011) != (s_MX)) % 0.75/0.96 ((s_HU) != (s_MX)) % 0.75/0.96 ((s_GE) != (s_g419)) % 0.75/0.96 ((s_g034) != (s_g019)) % 0.75/0.96 ((s_g034) != (s_g013)) % 0.75/0.96 ((s_GB) != (s_g019)) % 0.75/0.96 ((s_IL) != (s_g001)) % 0.75/0.96 ((s_g039) != (s_g003)) % 0.75/0.96 ((s_MR) != (s_g419)) % 0.75/0.96 ((s_PE) != (s_MX)) % 0.75/0.96 ((s_SK) != (s_g019)) % 0.75/0.96 ((s_SH) != (s_g019)) % 0.75/0.96 ((s_HR) != (s_g003)) % 0.75/0.96 ((s_SB) != (s_g019)) % 0.75/0.96 ((s_LK) != (s_g001)) % 0.75/0.96 (s_contains (s_g039) (s_GR)) % 0.75/0.96 ((s_LU) != (s_g419)) % 0.75/0.96 (s_contains (s_g029) (s_GP)) % 0.75/0.96 (s_partOf (s_SA) (s_g145)) % 0.75/0.96 ((s_CK) != (s_g019)) % 0.75/0.96 (s_partOf (s_PS) (s_g145)) % 0.75/0.96 (s_contains (s_g039) (s_PT)) % 0.75/0.96 ((s_MV) != (s_g013)) % 0.75/0.96 ((s_BI) != (s_g003)) % 0.75/0.96 ((s_SK) != (s_g003)) % 0.75/0.96 ((s_MU) != (s_g419)) % 0.75/0.96 ((s_FI) != (s_g019)) % 0.75/0.96 ((s_EE) != (s_g419)) % 0.75/0.96 ((s_IQ) != (s_g019)) % 0.75/0.96 ((s_GI) != (s_g019)) % 0.75/0.96 ((s_KZ) != (s_MX)) % 0.75/0.96 ((s_VU) != (s_g013)) % 0.75/0.96 ((s_MP) != (s_g419)) % 0.75/0.96 ((s_TL) != (s_g003)) % 0.75/0.96 ((s_MR) != (s_g013)) % 0.75/0.96 (s_partOf (s_KR) (s_g030)) % 0.75/0.96 ((s_SR) != (s_g013)) % 0.75/0.96 ((s_g015) != (s_g003)) % 0.75/0.96 (s_partOf (s_ML) (s_g011)) % 0.75/0.96 ((s_NG) != (s_g003)) % 0.75/0.96 (s_partOf (s_AI) (s_g029)) % 0.75/0.96 (s_partOf (s_IR) (s_g034)) % 0.75/0.96 ((s_NT) != (s_g013)) % 0.75/0.96 ((s_YD) != (s_g001)) % 0.75/0.96 ((s_ZR) != (s_g003)) % 0.75/0.96 ((s_PS) != (s_g003)) % 0.75/0.96 ((s_LR) != (s_g001)) % 0.75/0.96 ((s_CS) != (s_g013)) % 0.75/0.96 (s_partOf (s_BU) (s_g035)) % 0.75/0.96 (s_contains (s_g011) (s_GH)) % 0.75/0.96 ((s_TG) != (s_g013)) % 0.75/0.96 ((s_MQ) != (s_g003)) % 0.75/0.96 (s_partOf (s_CI) (s_g011)) % 0.75/0.96 (s_partOf (s_EG) (s_g015)) % 0.75/0.96 (s_partOf (s_SL) (s_g011)) % 0.75/0.96 ((s_CM) != (s_g019)) % 0.75/0.96 ((s_SE) != (s_MX)) % 0.75/0.96 (s_contains (s_g155) (s_FX)) % 0.75/0.96 ((s_CN) != (s_g019)) % 0.75/0.96 ((s_IM) != (s_g003)) % 0.75/0.96 (s_partOf (s_UZ) (s_g172)) % 0.75/0.96 (s_partOf (s_HN) (s_g013)) % 0.75/0.96 ((s_TO) != (s_g419)) % 0.75/0.96 ((s_NE) != (s_g419)) % 0.75/0.96 (s_partOf (s_MS) (s_g029)) % 0.75/0.96 ((s_BU) != (s_g013)) % 0.75/0.96 (s_contains (s_g030) (s_HK)) % 0.75/0.96 ((s_CA) != (s_g001)) % 0.75/0.96 ((s_SB) != (s_MX)) % 0.75/0.96 ((s_MW) != (s_g013)) % 0.75/0.96 ((s_BH) != (s_MX)) % 0.75/0.96 ((s_NR) != (s_g013)) % 0.75/0.96 ((s_MH) != (s_MX)) % 0.75/0.96 ((s_VC) != (s_g419)) % 0.75/0.96 ((s_SJ) != (s_g019)) % 0.75/0.96 ((s_TN) != (s_g001)) % 0.75/0.96 (s_partOf (s_MM) (s_g035)) % 0.75/0.96 ((s_HR) != (s_g001)) % 0.75/0.96 ((s_LY) != (s_g013)) % 0.75/0.96 ((s_PS) != (s_g001)) % 0.75/0.96 (s_partOf (s_UA) (s_g172)) % 0.75/0.96 (s_contains (s_g154) (s_JE)) % 0.75/0.96 ((s_CZ) != (s_g001)) % 0.75/0.96 ((s_JE) != (s_g001)) % 0.75/0.96 ((s_KE) != (s_g019)) % 0.75/0.96 ((s_FK) != (s_g003)) % 0.75/0.96 ((s_MV) != (s_MX)) % 0.75/0.96 ((s_MT) != (s_g001)) % 0.75/0.96 ((s_MF) != (s_g019)) % 0.75/0.96 ((s_MA) != (s_MX)) % 0.75/0.96 ((s_RE) != (s_MX)) % 0.75/0.96 ((s_AR) != (s_g013)) % 0.75/0.96 ((s_AW) != (s_g419)) % 0.75/0.96 (s_contains (s_g014) (s_MG)) % 0.75/0.96 (s_contains (s_g013) (s_NI)) % 0.75/0.96 (s_contains (s_g001) (s_g002)) % 0.75/0.96 ((s_g017) != (s_g419)) % 0.75/0.96 ((s_NZ) != (s_g003)) % 0.75/0.96 ((s_ER) != (s_g013)) % 0.75/0.96 (-. (s_contains (s_TW) (s_MX))) % 0.75/0.96 ((s_TK) != (s_MX)) % 0.75/0.96 ((s_MU) != (s_g001)) % 0.75/0.96 ((s_CM) != (s_g001)) % 0.75/0.96 ((s_g057) != (s_g419)) % 0.75/0.96 ((s_ZM) != (s_g001)) % 0.75/0.96 ((s_KI) != (s_MX)) % 0.75/0.96 ((s_LC) != (s_g003)) % 0.75/0.96 (s_contains (s_g029) (s_VC)) % 0.75/0.96 ((s_NU) != (s_g019)) % 0.75/0.96 ((s_SY) != (s_g003)) % 0.75/0.96 ((s_MO) != (s_g419)) % 0.75/0.96 (s_partOf (s_GI) (s_g039)) % 0.75/0.96 ((s_SL) != (s_g013)) % 0.75/0.96 ((s_SO) != (s_g013)) % 0.75/0.96 ((s_HR) != (s_g419)) % 0.75/0.96 ((s_EH) != (s_g019)) % 0.75/0.96 ((s_NF) != (s_g013)) % 0.75/0.96 ((s_NO) != (s_g419)) % 0.75/0.96 (s_partOf (s_AZ) (s_g145)) % 0.75/0.96 ((s_NG) != (s_g013)) % 0.75/0.96 ((s_g054) != (s_g019)) % 0.75/0.96 ((s_ML) != (s_g019)) % 0.75/0.96 (s_partOf (s_VI) (s_g029)) % 0.75/0.96 ((s_NT) != (s_g003)) % 0.75/0.96 ((s_AN) != (s_MX)) % 0.75/0.96 ((s_GL) != (s_MX)) % 0.75/0.96 (s_partOf (s_GF) (s_g005)) % 0.75/0.96 (s_partOf (s_KN) (s_g029)) % 0.75/0.96 (s_contains (s_g017) (s_ZR)) % 0.75/0.96 (-. (s_contains (s_JP) (s_g019))) % 0.75/0.96 (s_contains (s_g030) (s_KR)) % 0.75/0.96 ((s_RE) != (s_g019)) % 0.75/0.96 (s_contains (s_g018) (s_LS)) % 0.75/0.96 ((s_KW) != (s_g003)) % 0.75/0.96 (s_partOf (s_TD) (s_g017)) % 0.75/0.96 ((s_RE) != (s_g003)) % 0.75/0.96 (s_partOf (s_AU) (s_g053)) % 0.75/0.96 ((s_AX) != (s_MX)) % 0.75/0.96 ((s_LV) != (s_g019)) % 0.75/0.96 ((s_RS) != (s_g001)) % 0.75/0.96 ((s_AS) != (s_g019)) % 0.75/0.96 ((s_g062) != (s_MX)) % 0.75/0.96 ((s_PM) != (s_g419)) % 0.75/0.96 ((s_g035) != (s_g019)) % 0.75/0.96 ((s_HU) != (s_g013)) % 0.75/0.96 ((s_CL) != (s_g419)) % 0.75/0.96 ((s_g143) != (s_g003)) % 0.75/0.96 ((s_MO) != (s_MX)) % 0.75/0.96 (s_partOf (s_g029) (s_g003)) % 0.75/0.96 (s_contains (s_g154) (s_GG)) % 0.75/0.96 ((s_MP) != (s_g019)) % 0.75/0.96 ((s_BU) != (s_g419)) % 0.75/0.96 ((s_PR) != (s_MX)) % 0.75/0.96 ((s_SE) != (s_g013)) % 0.75/0.96 ((s_GU) != (s_g001)) % 0.75/0.96 (s_contains (s_g003) (s_g029)) % 0.75/0.96 (s_contains (s_g154) (s_FO)) % 0.75/0.96 (s_partOf (s_SR) (s_g005)) % 0.75/0.96 ((s_CF) != (s_g003)) % 0.75/0.96 ((s_UY) != (s_g001)) % 0.75/0.96 ((s_BF) != (s_g003)) % 0.75/0.96 ((s_OM) != (s_g003)) % 0.75/0.96 ((s_KN) != (s_g013)) % 0.75/0.96 ((s_TG) != (s_g419)) % 0.75/0.96 ((s_MF) != (s_g419)) % 0.75/0.96 ((s_TD) != (s_g019)) % 0.75/0.96 (s_partOf (s_PH) (s_g035)) % 0.75/0.96 ((s_g154) != (s_g419)) % 0.75/0.96 ((s_g017) != (s_g003)) % 0.75/0.96 ((s_TC) != (s_MX)) % 0.75/0.96 ((s_g011) != (s_g019)) % 0.75/0.96 ((s_CH) != (s_g001)) % 0.75/0.96 (s_contains (s_g014) (s_YT)) % 0.75/0.96 ((s_WS) != (s_g419)) % 0.75/0.96 (s_contains (s_g017) (s_GQ)) % 0.75/0.96 ((s_YE) != (s_g001)) % 0.75/0.96 ((s_YT) != (s_MX)) % 0.75/0.96 ((s_TH) != (s_g013)) % 0.75/0.96 ((s_EG) != (s_g013)) % 0.75/0.96 ((s_MK) != (s_g001)) % 0.75/0.96 (s_partOf (s_DJ) (s_g014)) % 0.75/0.96 ((s_AF) != (s_MX)) % 0.75/0.96 ((s_TT) != (s_g419)) % 0.75/0.96 ((s_FR) != (s_g001)) % 0.75/0.96 ((s_SM) != (s_MX)) % 0.75/0.96 ((s_YE) != (s_g019)) % 0.75/0.96 ((s_BR) != (s_g019)) % 0.75/0.96 ((s_KM) != (s_g419)) % 0.75/0.96 (s_partOf (s_KI) (s_g057)) % 0.75/0.96 (s_partOf (s_TG) (s_g011)) % 0.75/0.96 ((s_GM) != (s_g013)) % 0.75/0.96 ((s_IR) != (s_g419)) % 0.75/0.96 ((s_ST) != (s_g019)) % 0.75/0.96 ((s_CH) != (s_g013)) % 0.75/0.96 ((s_EE) != (s_MX)) % 0.75/0.96 (-. (s_contains (s_CN) (s_g013))) % 0.75/0.96 (s_contains (s_g011) (s_SL)) % 0.75/0.96 ((s_SI) != (s_g019)) % 0.75/0.96 ((s_NO) != (s_MX)) % 0.75/0.96 ((s_UY) != (s_g013)) % 0.75/0.96 (s_contains (s_g001) (s_g142)) % 0.75/0.96 ((s_g054) != (s_g419)) % 0.75/0.96 ((s_VI) != (s_g019)) % 0.75/0.96 ((s_SO) != (s_g001)) % 0.75/0.96 ((s_GL) != (s_g013)) % 0.75/0.96 ((s_FR) != (s_g019)) % 0.75/0.96 ((s_ME) != (s_g419)) % 0.75/0.96 (s_partOf (s_BE) (s_g155)) % 0.75/0.96 (s_contains (s_g034) (s_PK)) % 0.75/0.96 (s_partOf (s_g013) (s_g003)) % 0.75/0.96 ((s_ZM) != (s_g013)) % 0.75/0.96 ((s_IM) != (s_g013)) % 0.75/0.96 ((s_DD) != (s_g001)) % 0.75/0.96 ((s_DO) != (s_g003)) % 0.75/0.96 (s_partOf (s_KZ) (s_g143)) % 0.75/0.96 (s_contains (s_g145) (s_BH)) % 0.75/0.96 ((s_PE) != (s_g013)) % 0.75/0.96 ((s_AM) != (s_g419)) % 0.75/0.96 ((s_SB) != (s_g003)) % 0.75/0.96 ((s_ML) != (s_g013)) % 0.75/0.96 ((s_ZR) != (s_g001)) % 0.75/0.96 (s_partOf (s_LT) (s_g154)) % 0.75/0.96 (s_contains (s_g017) (s_GA)) % 0.75/0.96 ((s_LR) != (s_MX)) % 0.75/0.96 (s_contains (s_g151) (s_BG)) % 0.75/0.96 ((s_UZ) != (s_g001)) % 0.75/0.96 ((s_PH) != (s_g013)) % 0.75/0.96 ((s_UY) != (s_g003)) % 0.75/0.96 (s_contains (s_g013) (s_GT)) % 0.75/0.96 (-. (s_contains (s_JP) (s_g003))) % 0.75/0.96 ((s_LB) != (s_g013)) % 0.75/0.96 (s_partOf (s_g142) (s_g001)) % 0.75/0.96 ((s_AR) != (s_g019)) % 0.75/0.96 ((s_AN) != (s_g013)) % 0.75/0.96 ((s_ZW) != (s_g001)) % 0.75/0.96 (s_partOf (s_MR) (s_g011)) % 0.75/0.96 ((s_YD) != (s_g419)) % 0.75/0.96 ((s_MH) != (s_g419)) % 0.75/0.96 ((s_FM) != (s_g419)) % 0.75/0.96 ((s_FJ) != (s_g013)) % 0.75/0.96 (s_partOf (s_LK) (s_g034)) % 0.75/0.96 ((s_MD) != (s_g019)) % 0.75/0.96 ((s_CD) != (s_g001)) % 0.75/0.96 (s_contains (s_g057) (s_FM)) % 0.75/0.96 (s_contains (s_g018) (s_NA)) % 0.75/0.96 (s_contains (s_g035) (s_KH)) % 0.75/0.96 ((s_NP) != (s_g419)) % 0.75/0.96 (s_contains (s_g061) (s_TO)) % 0.75/0.96 (s_partOf (s_FI) (s_g154)) % 0.75/0.96 ((s_SG) != (s_g419)) % 0.75/0.96 ((s_SA) != (s_g019)) % 0.75/0.96 (-. (s_contains (s_KR) (s_MX))) % 0.75/0.96 ((s_YE) != (s_MX)) % 0.75/0.96 (s_partOf (s_TM) (s_g143)) % 0.75/0.96 ((s_LC) != (s_g013)) % 0.75/0.96 ((s_FM) != (s_g019)) % 0.75/0.96 ((s_GP) != (s_g001)) % 0.75/0.96 (s_contains (s_g057) (s_NR)) % 0.75/0.96 (s_partOf (s_YU) (s_g039)) % 0.75/0.96 ((s_TJ) != (s_MX)) % 0.75/0.96 ((s_CN) != (s_g419)) % 0.75/0.96 ((s_HR) != (s_MX)) % 0.75/0.96 ((s_CO) != (s_g019)) % 0.75/0.96 ((s_LY) != (s_g003)) % 0.75/0.96 ((s_MM) != (s_g419)) % 0.75/0.96 ((s_FX) != (s_MX)) % 0.75/0.96 ((s_KP) != (s_g419)) % 0.75/0.96 ((s_BJ) != (s_MX)) % 0.75/0.96 ((s_FR) != (s_g003)) % 0.75/0.96 ((s_g143) != (s_MX)) % 0.75/0.96 ((s_KM) != (s_MX)) % 0.75/0.96 ((s_TM) != (s_g003)) % 0.75/0.96 ((s_RU) != (s_g003)) % 0.75/0.96 ((s_UG) != (s_MX)) % 0.75/0.96 (s_contains (s_g035) (s_TL)) % 0.75/0.96 (-. (s_contains (s_g030) (s_g019))) % 0.75/0.96 ((s_PF) != (s_g001)) % 0.75/0.96 (s_partOf (s_AM) (s_g172)) % 0.75/0.96 ((s_CG) != (s_MX)) % 0.75/0.96 ((s_MW) != (s_g001)) % 0.75/0.96 ((s_g014) != (s_g013)) % 0.75/0.96 ((s_PY) != (s_g013)) % 0.75/0.96 ((s_YT) != (s_g019)) % 0.75/0.96 (s_contains (s_g021) (s_BM)) % 0.75/0.96 ((s_GY) != (s_g019)) % 0.75/0.96 ((s_UA) != (s_g003)) % 0.75/0.96 ((s_ST) != (s_g003)) % 0.75/0.96 (s_contains (s_g155) (s_CH)) % 0.75/0.96 ((s_ME) != (s_g003)) % 0.75/0.96 (s_partOf (s_g034) (s_g062)) % 0.75/0.96 ((s_CF) != (s_g013)) % 0.75/0.96 ((s_CF) != (s_g019)) % 0.75/0.96 ((s_MO) != (s_g001)) % 0.75/0.96 ((s_AL) != (s_g019)) % 0.75/0.96 (s_partOf (s_GG) (s_g830)) % 0.75/0.96 ((s_DM) != (s_MX)) % 0.75/0.96 ((s_DZ) != (s_g013)) % 0.75/0.96 ((s_KZ) != (s_g419)) % 0.75/0.96 ((s_NU) != (s_g419)) % 0.75/0.96 ((s_LS) != (s_g419)) % 0.75/0.96 ((s_NF) != (s_g003)) % 0.75/0.96 (-. (s_contains (s_JP) (s_g419))) % 0.75/0.96 (s_partOf (s_YD) (s_g145)) % 0.75/0.96 ((s_SG) != (s_MX)) % 0.75/0.96 ((s_ES) != (s_g419)) % 0.75/0.96 ((s_TR) != (s_g013)) % 0.75/0.96 ((s_g014) != (s_g003)) % 0.75/0.96 (s_contains (s_g015) (s_TN)) % 0.75/0.96 ((s_VC) != (s_MX)) % 0.75/0.96 ((s_OM) != (s_MX)) % 0.75/0.96 ((s_NL) != (s_g013)) % 0.75/0.96 ((s_FR) != (s_g419)) % 0.75/0.96 (s_contains (s_g142) (s_g030)) % 0.75/0.96 ((s_SM) != (s_g419)) % 0.75/0.96 ((s_DE) != (s_g019)) % 0.75/0.96 ((s_EG) != (s_MX)) % 0.75/0.96 ((s_g155) != (s_g013)) % 0.75/0.96 ((s_UZ) != (s_g019)) % 0.75/0.96 ((s_PE) != (s_g419)) % 0.75/0.96 ((s_g057) != (s_g019)) % 0.75/0.96 ((s_AL) != (s_MX)) % 0.75/0.96 ((s_SR) != (s_g419)) % 0.75/0.96 (s_contains (s_g029) (s_BB)) % 0.75/0.96 ((s_g015) != (s_g001)) % 0.75/0.96 ((s_GA) != (s_g019)) % 0.75/0.96 ((s_GB) != (s_MX)) % 0.75/0.96 ((s_ES) != (s_g001)) % 0.75/0.96 (s_contains (s_g145) (s_CY)) % 0.75/0.96 ((s_MR) != (s_MX)) % 0.75/0.96 ((s_SK) != (s_g419)) % 0.75/0.96 (s_contains (s_g145) (s_QA)) % 0.75/0.96 ((s_LK) != (s_g013)) % 0.75/0.96 (s_contains (s_g029) (s_PR)) % 0.75/0.96 ((s_g151) != (s_g003)) % 0.75/0.96 (s_partOf (s_NA) (s_g018)) % 0.75/0.96 ((s_FM) != (s_g003)) % 0.75/0.96 (s_partOf (s_NZ) (s_g053)) % 0.75/0.96 (s_partOf (s_g014) (s_g002)) % 0.75/0.96 ((s_SU) != (s_g013)) % 0.75/0.96 ((s_NE) != (s_g019)) % 0.75/0.96 ((s_AR) != (s_g001)) % 0.75/0.96 ((s_GP) != (s_g419)) % 0.75/0.96 (s_contains (s_g143) (s_TM)) % 0.75/0.96 ((s_KG) != (s_g001)) % 0.75/0.96 ((s_RW) != (s_MX)) % 0.75/0.96 ((s_g155) != (s_MX)) % 0.75/0.96 ((s_BO) != (s_g003)) % 0.75/0.96 ((s_SU) != (s_g003)) % 0.75/0.96 (s_contains (s_g018) (s_SZ)) % 0.75/0.96 ((s_ST) != (s_g013)) % 0.75/0.96 ((s_GG) != (s_g019)) % 0.75/0.96 ((s_LA) != (s_g019)) % 0.75/0.96 ((s_NF) != (s_g419)) % 0.75/0.96 ((s_CA) != (s_g003)) % 0.75/0.96 ((s_UY) != (s_g419)) % 0.75/0.96 (s_contains (s_g034) (s_BD)) % 0.75/0.96 (s_partOf (s_CO) (s_g005)) % 0.75/0.96 ((s_KI) != (s_g013)) % 0.75/0.96 ((s_AE) != (s_g001)) % 0.75/0.96 (s_partOf (s_GR) (s_g039)) % 0.75/0.96 ((s_RW) != (s_g019)) % 0.75/0.96 ((s_RS) != (s_g019)) % 0.75/0.96 ((s_LU) != (s_g019)) % 0.75/0.96 ((s_FX) != (s_g419)) % 0.75/0.96 ((s_NP) != (s_g019)) % 0.75/0.96 ((s_CU) != (s_g001)) % 0.75/0.96 ((s_SC) != (s_MX)) % 0.75/0.96 (s_contains (s_g015) (s_EH)) % 0.75/0.96 (s_contains (s_g035) (s_ID)) % 0.75/0.96 ((s_TH) != (s_MX)) % 0.75/0.96 ((s_g143) != (s_g013)) % 0.75/0.96 ((s_SD) != (s_g013)) % 0.75/0.96 ((s_MC) != (s_g013)) % 0.75/0.96 ((s_TJ) != (s_g013)) % 0.75/0.96 ((s_HR) != (s_g019)) % 0.75/0.96 ((s_KE) != (s_g001)) % 0.75/0.96 ((s_IS) != (s_g001)) % 0.75/0.96 ((s_FJ) != (s_g001)) % 0.75/0.96 ((s_VU) != (s_g019)) % 0.75/0.96 ((s_SY) != (s_g019)) % 0.75/0.96 ((s_FO) != (s_g001)) % 0.75/0.96 ((s_GD) != (s_g003)) % 0.75/0.96 ((s_ET) != (s_g419)) % 0.75/0.96 ((s_RW) != (s_g419)) % 0.75/0.96 ((s_LI) != (s_g003)) % 0.75/0.96 (s_partOf (s_SB) (s_g054)) % 0.75/0.96 ((s_BU) != (s_g003)) % 0.75/0.96 ((s_FK) != (s_g019)) % 0.75/0.96 ((s_KY) != (s_g001)) % 0.75/0.96 (s_contains (s_g172) (s_BY)) % 0.75/0.96 ((s_CZ) != (s_g419)) % 0.75/0.96 ((s_DZ) != (s_g019)) % 0.75/0.96 ((s_BI) != (s_g013)) % 0.75/0.96 ((s_ES) != (s_g013)) % 0.75/0.96 ((s_VE) != (s_g013)) % 0.75/0.96 ((s_g054) != (s_g003)) % 0.75/0.96 ((s_g062) != (s_g003)) % 0.75/0.96 (s_contains (s_g035) (s_TP)) % 0.75/0.96 ((s_GW) != (s_g019)) % 0.75/0.96 (-. (s_contains (s_MO) (s_g001))) % 0.75/0.96 ((s_WF) != (s_MX)) % 0.75/0.96 ((s_JO) != (s_g003)) % 0.75/0.96 ((s_VN) != (s_g013)) % 0.75/0.96 ((s_VE) != (s_MX)) % 0.75/0.96 ((s_GW) != (s_g001)) % 0.75/0.96 ((s_FI) != (s_MX)) % 0.75/0.96 ((s_g155) != (s_g419)) % 0.75/0.96 ((s_BS) != (s_g019)) % 0.75/0.96 ((s_AT) != (s_g013)) % 0.75/0.96 ((s_NL) != (s_g003)) % 0.75/0.96 ((s_MM) != (s_g001)) % 0.75/0.96 ((s_HT) != (s_g019)) % 0.75/0.96 (s_contains (s_g009) (s_g054)) % 0.75/0.96 ((s_BG) != (s_g013)) % 0.75/0.96 (s_contains (s_g154) (s_SJ)) % 0.75/0.96 (-. (s_contains (s_MO) (s_g013))) % 0.75/0.96 ((s_NL) != (s_g419)) % 0.75/0.96 ((s_SK) != (s_g001)) % 0.75/0.96 ((s_SO) != (s_MX)) % 0.75/0.96 ((s_LV) != (s_g001)) % 0.75/0.96 (s_contains (s_g154) (s_LV)) % 0.75/0.96 (s_partOf (s_DD) (s_g155)) % 0.75/0.96 ((s_KW) != (s_MX)) % 0.75/0.96 ((s_US) != (s_g013)) % 0.75/0.96 ((s_PN) != (s_g001)) % 0.75/0.96 (s_partOf (s_HK) (s_g030)) % 0.75/0.96 ((s_CO) != (s_g013)) % 0.75/0.96 ((s_LC) != (s_g001)) % 0.75/0.96 (s_contains (s_g054) (s_NC)) % 0.75/0.96 ((s_FJ) != (s_g019)) % 0.75/0.96 ((s_JM) != (s_g419)) % 0.75/0.96 ((s_CV) != (s_g001)) % 0.75/0.96 (-. (s_contains (s_MO) (s_g019))) % 0.75/0.96 ((s_MU) != (s_g003)) % 0.75/0.96 ((s_NU) != (s_g003)) % 0.75/0.96 ((s_KN) != (s_g001)) % 0.75/0.96 (s_partOf (s_EC) (s_g005)) % 0.75/0.96 (s_partOf (s_BB) (s_g029)) % 0.75/0.96 ((s_KE) != (s_g013)) % 0.75/0.96 ((s_BN) != (s_g013)) % 0.75/0.96 ((s_TV) != (s_g019)) % 0.75/0.96 (s_partOf (s_YT) (s_g014)) % 0.75/0.96 (s_partOf (s_BY) (s_g151)) % 0.75/0.96 ((s_CO) != (s_g003)) % 0.75/0.96 (-. (s_contains (s_HK) (s_g419))) % 0.75/0.96 ((s_MV) != (s_g003)) % 0.75/0.96 ((s_IL) != (s_g003)) % 0.75/0.96 (s_contains (s_g061) (s_NU)) % 0.75/0.96 (s_partOf (s_CM) (s_g017)) % 0.75/0.96 (s_contains (s_g151) (s_SU)) % 0.75/0.96 ((s_GB) != (s_g419)) % 0.75/0.96 ((s_MH) != (s_g001)) % 0.75/0.96 ((s_BA) != (s_g003)) % 0.75/0.96 ((s_NE) != (s_g003)) % 0.75/0.96 ((s_JM) != (s_g013)) % 0.75/0.96 (s_partOf (s_CD) (s_g017)) % 0.75/0.96 ((s_IT) != (s_g001)) % 0.75/0.96 (s_partOf (s_KY) (s_g029)) % 0.75/0.96 (s_contains (s_g030) (s_TW)) % 0.75/0.96 ((s_BE) != (s_g019)) % 0.75/0.96 ((s_ER) != (s_MX)) % 0.75/0.96 ((s_AR) != (s_g419)) % 0.75/0.96 (s_partOf (s_PR) (s_g029)) % 0.75/0.96 (s_partOf (s_BT) (s_g034)) % 0.75/0.96 (s_partOf (s_g155) (s_g150)) % 0.75/0.96 ((s_AW) != (s_g013)) % 0.75/0.96 ((s_GB) != (s_g003)) % 0.75/0.96 (s_partOf (s_UY) (s_g005)) % 0.75/0.96 ((s_CG) != (s_g001)) % 0.75/0.96 ((s_CL) != (s_g013)) % 0.75/0.96 ((s_SU) != (s_g419)) % 0.75/0.96 ((s_VC) != (s_g001)) % 0.75/0.96 ((s_IQ) != (s_g013)) % 0.75/0.96 ((s_SL) != (s_g019)) % 0.75/0.96 ((s_AL) != (s_g003)) % 0.75/0.96 ((s_AF) != (s_g003)) % 0.75/0.96 ((s_GI) != (s_g419)) % 0.75/0.96 ((s_SR) != (s_g019)) % 0.75/0.96 ((s_BH) != (s_g013)) % 0.75/0.96 ((s_CM) != (s_g013)) % 0.75/0.96 ((s_BT) != (s_g019)) % 0.75/0.96 ((s_GU) != (s_g003)) % 0.75/0.96 ((s_CV) != (s_MX)) % 0.75/0.96 ((s_BI) != (s_g001)) % 0.75/0.96 ((s_TV) != (s_g003)) % 0.75/0.96 ((s_TR) != (s_g003)) % 0.75/0.96 ((s_TT) != (s_g013)) % 0.75/0.96 ((s_FI) != (s_g013)) % 0.75/0.96 ((s_ES) != (s_g003)) % 0.75/0.96 ((s_EH) != (s_g001)) % 0.75/0.96 (s_contains (s_g029) (s_VG)) % 0.75/0.96 ((s_AT) != (s_g019)) % 0.75/0.96 ((s_MA) != (s_g001)) % 0.75/0.96 ((s_MS) != (s_g003)) % 0.75/0.96 ((s_g039) != (s_g019)) % 0.75/0.96 ((s_VN) != (s_g003)) % 0.75/0.96 (s_partOf (s_UG) (s_g014)) % 0.75/0.96 (s_partOf (s_US) (s_g021)) % 0.75/0.96 ((s_LA) != (s_MX)) % 0.75/0.96 (s_partOf (s_NP) (s_g034)) % 0.75/0.96 ((s_MY) != (s_g001)) % 0.75/0.96 ((s_JM) != (s_g019)) % 0.75/0.96 ((s_AM) != (s_g003)) % 0.75/0.96 (s_partOf (s_SE) (s_g154)) % 0.75/0.96 ((s_FM) != (s_g013)) % 0.75/0.96 ((s_g143) != (s_g001)) % 0.75/0.96 ((s_GG) != (s_g003)) % 0.75/0.96 ((s_RU) != (s_g001)) % 0.75/0.96 (s_partOf (s_WF) (s_g061)) % 0.75/0.96 ((s_UZ) != (s_g003)) % 0.75/0.96 ((s_GG) != (s_MX)) % 0.75/0.96 ((s_GE) != (s_g001)) % 0.75/0.96 (s_contains (s_g014) (s_MW)) % 0.75/0.96 (s_partOf (s_g419) (s_g019)) % 0.75/0.96 ((s_AS) != (s_g003)) % 0.75/0.96 (s_contains (s_g054) (s_SB)) % 0.75/0.96 (-. (s_contains (s_MN) (s_MX))) % 0.75/0.96 ((s_SC) != (s_g013)) % 0.75/0.96 ((s_IM) != (s_g001)) % 0.75/0.96 ((s_IM) != (s_g019)) % 0.75/0.96 ((s_PR) != (s_g419)) % 0.75/0.96 ((s_DD) != (s_g419)) % 0.75/0.96 ((s_GY) != (s_g003)) % 0.75/0.96 ((s_RO) != (s_g001)) % 0.75/0.96 (s_partOf (s_IS) (s_g154)) % 0.75/0.96 ((s_AE) != (s_g003)) % 0.75/0.96 ((s_DM) != (s_g003)) % 0.75/0.96 ((s_LS) != (s_g013)) % 0.75/0.96 (s_contains (s_g061) (s_PN)) % 0.75/0.96 (s_partOf (s_NO) (s_g154)) % 0.75/0.96 ((s_YE) != (s_g003)) % 0.75/0.96 ((s_BF) != (s_MX)) % 0.75/0.96 ((s_PM) != (s_g013)) % 0.75/0.96 (s_partOf (s_BI) (s_g014)) % 0.75/0.96 ((s_FX) != (s_g013)) % 0.75/0.96 ((s_CH) != (s_g019)) % 0.75/0.96 ((s_LR) != (s_g013)) % 0.75/0.96 (s_contains (s_g005) (s_PY)) % 0.75/0.96 ((s_GU) != (s_g019)) % 0.75/0.96 ((s_TM) != (s_g001)) % 0.75/0.96 ((s_CS) != (s_g003)) % 0.75/0.96 (s_contains (s_g009) (s_g061)) % 0.75/0.96 (s_partOf (s_FX) (s_g155)) % 0.75/0.96 ((s_YE) != (s_g419)) % 0.75/0.96 ((s_g061) != (s_g013)) % 0.75/0.96 ((s_ZW) != (s_g013)) % 0.75/0.96 ((s_MQ) != (s_g013)) % 0.75/0.96 ((s_JP) != (s_g001)) % 0.75/0.96 ((s_GR) != (s_g419)) % 0.75/0.96 (s_partOf (s_DE) (s_g155)) % 0.75/0.96 (s_contains (s_g151) (s_UA)) % 0.75/0.96 (s_partOf (s_PE) (s_g005)) % 0.75/0.96 ((s_KM) != (s_g019)) % 0.75/0.96 ((s_VI) != (s_g419)) % 0.75/0.96 ((s_SU) != (s_g001)) % 0.75/0.96 ((s_CK) != (s_g419)) % 0.75/0.96 ((s_NO) != (s_g019)) % 0.75/0.96 ((s_MN) != (s_g013)) % 0.75/0.96 (s_contains (s_g013) (s_BZ)) % 0.75/0.96 (-. (s_contains (s_KP) (s_g013))) % 0.75/0.96 ((s_SH) != (s_g001)) % 0.75/0.96 ((s_SH) != (s_g013)) % 0.75/0.96 ((s_CY) != (s_g419)) % 0.75/0.96 ((s_DZ) != (s_MX)) % 0.75/0.96 (s_partOf (s_PT) (s_g039)) % 0.75/0.96 ((s_LS) != (s_MX)) % 0.75/0.96 ((s_SE) != (s_g019)) % 0.75/0.96 ((s_BT) != (s_g419)) % 0.75/0.96 ((s_GG) != (s_g001)) % 0.75/0.96 ((s_NP) != (s_MX)) % 0.75/0.96 ((s_RU) != (s_g419)) % 0.75/0.96 ((s_TZ) != (s_g019)) % 0.75/0.96 ((s_MO) != (s_g019)) % 0.75/0.96 ((s_SH) != (s_MX)) % 0.75/0.96 ((s_KY) != (s_g013)) % 0.75/0.96 (s_contains (s_g017) (s_ST)) % 0.75/0.96 ((s_g053) != (s_g013)) % 0.75/0.96 (s_contains (s_g145) (s_GE)) % 0.75/0.96 ((s_RO) != (s_g019)) % 0.75/0.96 (s_contains (s_g035) (s_MM)) % 0.75/0.96 ((s_g030) != (s_g419)) % 0.75/0.96 ((s_IN) != (s_g003)) % 0.75/0.96 ((s_TN) != (s_g013)) % 0.75/0.96 ((s_SR) != (s_g003)) % 0.75/0.96 ((s_GD) != (s_g419)) % 0.75/0.96 ((s_TC) != (s_g001)) % 0.75/0.96 ((s_KH) != (s_MX)) % 0.75/0.96 ((s_CU) != (s_g003)) % 0.75/0.96 ((s_PM) != (s_g019)) % 0.75/0.96 ((s_AZ) != (s_g003)) % 0.75/0.96 ((s_GB) != (s_g001)) % 0.75/0.96 ((s_PN) != (s_g013)) % 0.75/0.96 ((s_KM) != (s_g003)) % 0.75/0.96 (s_contains (s_g039) (s_AL)) % 0.75/0.96 ((s_DE) != (s_MX)) % 0.75/0.96 (s_contains (s_g151) (s_SK)) % 0.75/0.96 ((s_AS) != (s_g419)) % 0.75/0.96 (s_contains (s_g013) (s_MX)) % 0.75/0.96 (s_contains (s_g019) (s_g003)) % 0.75/0.96 (-. (s_contains (s_HK) (s_MX))) % 0.75/0.96 ((s_TC) != (s_g013)) % 0.75/0.96 ((s_SA) != (s_g419)) % 0.75/0.96 (s_contains (s_g155) (s_MC)) % 0.75/0.96 (-. (s_contains (s_g030) (s_g013))) % 0.75/0.96 ((s_BL) != (s_MX)) % 0.75/0.96 ((s_PY) != (s_g019)) % 0.75/0.96 ((s_SM) != (s_g001)) % 0.75/0.96 (s_contains (s_g029) (s_LC)) % 0.75/0.96 ((s_DO) != (s_MX)) % 0.75/0.96 (s_contains (s_g030) (s_MO)) % 0.75/0.96 (s_partOf (s_g009) (s_g001)) % 0.75/0.96 (s_partOf (s_g005) (s_g019)) % 0.75/0.96 ((s_DZ) != (s_g419)) % 0.75/0.96 ((s_PK) != (s_g003)) % 0.75/0.96 (s_partOf (s_UA) (s_g151)) % 0.75/0.96 ((s_IS) != (s_g013)) % 0.75/0.96 ((s_PH) != (s_g003)) % 0.75/0.96 (s_contains (s_g018) (s_BW)) % 0.75/0.96 (s_contains (s_g154) (s_SE)) % 0.75/0.96 ((s_PR) != (s_g013)) % 0.75/0.96 ((s_GA) != (s_g419)) % 0.75/0.96 (s_partOf (s_g145) (s_g142)) % 0.75/0.96 ((s_TH) != (s_g019)) % 0.75/0.96 ((s_TH) != (s_g001)) % 0.75/0.96 ((s_BY) != (s_g013)) % 0.75/0.96 (s_contains (s_g039) (s_BA)) % 0.75/0.96 ((s_FI) != (s_g001)) % 0.75/0.96 ((s_BY) != (s_g419)) % 0.75/0.96 ((s_NR) != (s_g019)) % 0.75/0.96 ((s_UZ) != (s_g013)) % 0.75/0.96 ((s_VC) != (s_g003)) % 0.75/0.96 (s_contains (s_g014) (s_ET)) % 0.75/0.96 ((s_EG) != (s_g019)) % 0.75/0.96 ((s_GP) != (s_MX)) % 0.75/0.96 ((s_SO) != (s_g419)) % 0.75/0.96 (s_partOf (s_SI) (s_g039)) % 0.75/0.96 ((s_MQ) != (s_g001)) % 0.75/0.96 ((s_TO) != (s_MX)) % 0.75/0.96 ((s_g017) != (s_g019)) % 0.75/0.96 ((s_FI) != (s_g419)) % 0.75/0.96 ((s_TW) != (s_g019)) % 0.75/0.96 ((s_BM) != (s_g013)) % 0.75/0.96 (s_partOf (s_AR) (s_g005)) % 0.75/0.96 ((s_RO) != (s_g003)) % 0.75/0.96 (s_contains (s_g172) (s_MD)) % 0.75/0.96 ((s_g145) != (s_g419)) % 0.75/0.96 ((s_WS) != (s_g003)) % 0.75/0.96 ((s_PT) != (s_MX)) % 0.75/0.96 (-. (s_contains (s_g030) (s_g419))) % 0.75/0.96 ((s_SO) != (s_g003)) % 0.75/0.96 ((s_UG) != (s_g019)) % 0.75/0.96 ((s_VA) != (s_g003)) % 0.75/0.96 ((s_MF) != (s_g003)) % 0.75/0.96 (s_contains (s_g053) (s_AU)) % 0.75/0.96 ((s_PM) != (s_g003)) % 0.75/0.96 ((s_MN) != (s_g003)) % 0.75/0.96 (s_contains (s_g155) (s_LU)) % 0.75/0.96 ((s_g054) != (s_MX)) % 0.75/0.96 ((s_HT) != (s_g001)) % 0.75/0.96 ((s_FO) != (s_g013)) % 0.75/0.96 ((s_g062) != (s_g013)) % 0.75/0.96 ((s_g030) != (s_g013)) % 0.75/0.96 ((s_GM) != (s_MX)) % 0.75/0.96 ((s_UG) != (s_g001)) % 0.75/0.96 (s_contains (s_g154) (s_AX)) % 0.75/0.96 ((s_MQ) != (s_MX)) % 0.75/0.96 ((s_IQ) != (s_g419)) % 0.75/0.96 ((s_ML) != (s_g003)) % 0.75/0.96 (s_contains (s_g014) (s_SO)) % 0.75/0.96 (s_partOf (s_g017) (s_g002)) % 0.75/0.96 (s_partOf (s_g039) (s_g150)) % 0.75/0.96 ((s_NU) != (s_MX)) % 0.75/0.96 (s_partOf (s_NI) (s_g013)) % 0.75/0.96 ((s_MA) != (s_g019)) % 0.75/0.96 (s_partOf (s_MD) (s_g172)) % 0.75/0.96 (s_contains (s_g155) (s_AT)) % 0.75/0.96 ((s_FO) != (s_g419)) % 0.75/0.96 (s_partOf (s_PA) (s_g013)) % 0.75/0.96 ((s_YU) != (s_g419)) % 0.75/0.96 (s_partOf (s_DO) (s_g029)) % 0.75/0.96 ((s_TJ) != (s_g019)) % 0.75/0.96 (s_partOf (s_GQ) (s_g017)) % 0.75/0.96 (s_contains (s_g030) (s_CN)) % 0.75/0.96 ((s_MR) != (s_g019)) % 0.75/0.96 ((s_MU) != (s_g019)) % 0.75/0.96 ((s_IR) != (s_g001)) % 0.75/0.96 ((s_GF) != (s_MX)) % 0.75/0.96 ((s_g030) != (s_MX)) % 0.75/0.96 ((s_LU) != (s_g001)) % 0.75/0.96 (s_partOf (s_BZ) (s_g013)) % 0.75/0.96 (s_partOf (s_CF) (s_g017)) % 0.75/0.96 ((s_GY) != (s_MX)) % 0.75/0.96 ((s_AD) != (s_g419)) % 0.75/0.96 ((s_g154) != (s_g019)) % 0.75/0.96 ((s_LY) != (s_g019)) % 0.75/0.96 ((s_US) != (s_g001)) % 0.75/0.96 ((s_IT) != (s_g003)) % 0.75/0.96 (s_contains (s_g014) (s_DJ)) % 0.75/0.96 ((s_VG) != (s_g013)) % 0.75/0.96 ((s_PG) != (s_g419)) % 0.75/0.96 ((s_IN) != (s_g001)) % 0.75/0.96 (s_contains (s_g034) (s_LK)) % 0.75/0.96 ((s_MD) != (s_g003)) % 0.75/0.96 ((s_TZ) != (s_g001)) % 0.75/0.96 (s_partOf (s_ET) (s_g014)) % 0.75/0.96 ((s_UY) != (s_MX)) % 0.75/0.96 ((s_ER) != (s_g001)) % 0.75/0.96 ((s_BL) != (s_g003)) % 0.75/0.96 (s_partOf (s_g029) (s_g019)) % 0.75/0.96 (s_contains (s_g154) (s_EE)) % 0.75/0.96 ((s_BJ) != (s_g003)) % 0.75/0.96 ((s_CI) != (s_g013)) % 0.75/0.96 ((s_VC) != (s_g013)) % 0.75/0.96 (s_partOf (s_RS) (s_g039)) % 0.75/0.96 ((s_g053) != (s_MX)) % 0.75/0.96 ((s_NZ) != (s_g419)) % 0.75/0.96 ((s_GY) != (s_g001)) % 0.75/0.96 (s_partOf (s_GY) (s_g005)) % 0.75/0.96 (s_partOf (s_TT) (s_g029)) % 0.75/0.96 ((s_KN) != (s_g419)) % 0.75/0.96 ((s_MY) != (s_g003)) % 0.75/0.96 ((s_CY) != (s_g013)) % 0.75/0.96 ((s_AO) != (s_g013)) % 0.75/0.96 (s_contains (s_g034) (s_NP)) % 0.75/0.96 ((s_CD) != (s_g419)) % 0.75/0.96 ((s_DO) != (s_g419)) % 0.75/0.96 ((s_NC) != (s_g019)) % 0.75/0.96 ((s_PN) != (s_g419)) % 0.75/0.96 ((s_PT) != (s_g019)) % 0.75/0.96 ((s_HU) != (s_g019)) % 0.75/0.96 ((s_OM) != (s_g013)) % 0.75/0.96 ((s_GH) != (s_g001)) % 0.75/0.96 ((s_VU) != (s_g003)) % 0.75/0.96 (s_partOf (s_CL) (s_g005)) % 0.75/0.96 (s_partOf (s_GM) (s_g011)) % 0.75/0.96 ((s_JP) != (s_g019)) % 0.75/0.96 (s_contains (s_g011) (s_NE)) % 0.75/0.96 ((s_CK) != (s_MX)) % 0.75/0.96 ((s_EC) != (s_MX)) % 0.75/0.96 ((s_MA) != (s_g003)) % 0.75/0.96 ((s_QA) != (s_g013)) % 0.75/0.96 ((s_TD) != (s_g013)) % 0.75/0.96 ((s_PL) != (s_g019)) % 0.75/0.96 (s_partOf (s_MP) (s_g057)) % 0.75/0.96 (s_partOf (s_FR) (s_g155)) % 0.75/0.96 ((s_IL) != (s_g419)) % 0.75/0.96 ((s_LB) != (s_g003)) % 0.75/0.96 ((s_AD) != (s_g003)) % 0.75/0.96 ((s_EH) != (s_MX)) % 0.75/0.96 ((s_BU) != (s_g019)) % 0.75/0.96 ((s_HK) != (s_g001)) % 0.75/0.96 (s_partOf (s_AM) (s_g145)) % 0.75/0.96 ((s_TR) != (s_g001)) % 0.75/0.96 (s_contains (s_g029) (s_AW)) % 0.75/0.96 (s_contains (s_g039) (s_HR)) % 0.75/0.96 ((s_BW) != (s_g001)) % 0.75/0.96 ((s_TL) != (s_g019)) % 0.75/0.96 (s_contains (s_g011) (s_SN)) % 0.75/0.96 ((s_CF) != (s_MX)) % 0.75/0.96 (s_partOf (s_IT) (s_g039)) % 0.75/0.96 ((s_GR) != (s_g013)) % 0.75/0.96 ((s_BW) != (s_g019)) % 0.75/0.96 ((s_AG) != (s_g001)) % 0.75/0.96 ((s_PE) != (s_g019)) % 0.75/0.96 ((s_KY) != (s_g019)) % 0.75/0.96 (s_contains (s_g005) (s_GY)) % 0.75/0.96 ((s_PH) != (s_g419)) % 0.75/0.96 ((s_g014) != (s_g001)) % 0.75/0.96 ((s_CL) != (s_MX)) % 0.75/0.96 ((s_KZ) != (s_g013)) % 0.75/0.96 ((s_g015) != (s_g419)) % 0.75/0.96 ((s_DM) != (s_g019)) % 0.75/0.96 ((s_g014) != (s_MX)) % 0.75/0.96 (s_partOf (s_VU) (s_g054)) % 0.75/0.96 ((s_g145) != (s_MX)) % 0.75/0.96 ((s_BE) != (s_g013)) % 0.75/0.96 ((s_FI) != (s_g003)) % 0.75/0.96 (s_contains (s_g029) (s_AG)) % 0.75/0.96 ((s_g035) != (s_g419)) % 0.75/0.96 ((s_g017) != (s_g013)) % 0.75/0.96 (s_contains (s_g030) (s_MN)) % 0.75/0.96 ((s_SD) != (s_MX)) % 0.75/0.96 ((s_ER) != (s_g019)) % 0.75/0.96 ((s_CZ) != (s_MX)) % 0.75/0.96 (s_contains (s_g172) (s_UA)) % 0.75/0.96 ((s_MC) != (s_g001)) % 0.75/0.96 ((s_NG) != (s_g419)) % 0.75/0.96 ((s_KM) != (s_g001)) % 0.75/0.96 ((s_GF) != (s_g003)) % 0.75/0.96 *) % 0.75/0.96 (* NO-PROOF *) % 0.75/0.96 % SZS status GaveUp % 0.75/0.96 Number of rewrites on terms: 0 % 0.75/0.96 Number of rewrites on props: 0 % 0.75/0.96 nodes searched: 16263 % 0.75/0.96 max branch formulas: 2200 % 0.75/0.96 proof nodes created: 5 % 0.75/0.96 formulas created: 27603 % 0.75/0.96 %------------------------------------------------------------------------------