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