%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : MSC019+1 : TPTP v9.2.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n025.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 : Wed Jun 3 08:36:07 AM UTC 2026 % Result : Theorem 0.41s 0.80s % Output : Proof 0.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : MSC019+1 : TPTP v9.2.1. Released v4.0.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.18/0.34 % Computer : n025.cluster.edu % 0.18/0.34 % Model : x86_64 x86_64 % 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.34 % Memory : 8042.1875MB % 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.34 % CPULimit : 300 % 0.18/0.34 % WCLimit : 300 % 0.18/0.34 % DateTime : Tue Jun 2 09:45:31 EDT 2026 % 0.18/0.34 % CPUTime : % 0.32/0.54 %----Proving TF0_NAR, FOF, or CNF % 0.41/0.80 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.41/0.80 % SZS status Theorem % 0.41/0.80 % SZS output start Proof % 0.41/0.80 ( % 0.41/0.80 (declare-sort $$unsorted 0) % 0.41/0.80 (declare-const tptp.s_WS $$unsorted) % 0.41/0.80 (declare-const tptp.s_WF $$unsorted) % 0.41/0.80 (declare-const tptp.s_TV $$unsorted) % 0.41/0.80 (declare-const tptp.s_TO $$unsorted) % 0.41/0.80 (declare-const tptp.s_TK $$unsorted) % 0.41/0.80 (declare-const tptp.s_PN $$unsorted) % 0.41/0.80 (declare-const tptp.s_PF $$unsorted) % 0.41/0.80 (declare-const tptp.s_NU $$unsorted) % 0.41/0.80 (declare-const tptp.s_CK $$unsorted) % 0.41/0.80 (declare-const tptp.s_AS $$unsorted) % 0.41/0.80 (declare-const tptp.s_PW $$unsorted) % 0.41/0.80 (declare-const tptp.s_NR $$unsorted) % 0.41/0.80 (declare-const tptp.s_MP $$unsorted) % 0.41/0.80 (declare-const tptp.s_MH $$unsorted) % 0.41/0.80 (declare-const tptp.s_KI $$unsorted) % 0.41/0.80 (declare-const tptp.s_GU $$unsorted) % 0.41/0.80 (declare-const tptp.s_FM $$unsorted) % 0.41/0.80 (declare-const tptp.s_VU $$unsorted) % 0.41/0.80 (declare-const tptp.s_SB $$unsorted) % 0.41/0.80 (declare-const tptp.s_PG $$unsorted) % 0.41/0.80 (declare-const tptp.s_NC $$unsorted) % 0.41/0.80 (declare-const tptp.s_FJ $$unsorted) % 0.41/0.80 (declare-const tptp.s_NZ $$unsorted) % 0.41/0.80 (declare-const tptp.s_NF $$unsorted) % 0.41/0.80 (declare-const tptp.s_AU $$unsorted) % 0.41/0.80 (declare-const tptp.s_KZ $$unsorted) % 0.41/0.80 (declare-const tptp.s_g830 $$unsorted) % 0.41/0.80 (declare-const tptp.s_KG $$unsorted) % 0.41/0.80 (declare-const tptp.s_TJ $$unsorted) % 0.41/0.80 (declare-const tptp.s_TM $$unsorted) % 0.41/0.80 (declare-const tptp.s_TP $$unsorted) % 0.41/0.80 (declare-const tptp.s_TL $$unsorted) % 0.41/0.80 (declare-const tptp.s_TH $$unsorted) % 0.41/0.80 (declare-const tptp.s_SG $$unsorted) % 0.41/0.80 (declare-const tptp.s_PH $$unsorted) % 0.41/0.80 (declare-const tptp.s_MY $$unsorted) % 0.41/0.80 (declare-const tptp.s_BU $$unsorted) % 0.41/0.80 (declare-const tptp.s_MM $$unsorted) % 0.41/0.80 (declare-const tptp.s_LA $$unsorted) % 0.41/0.80 (declare-const tptp.s_TW $$unsorted) % 0.41/0.80 (declare-const tptp.s_BE $$unsorted) % 0.41/0.80 (declare-const tptp.s_MO $$unsorted) % 0.41/0.80 (declare-const tptp.s_AT $$unsorted) % 0.41/0.80 (declare-const tptp.s_MN $$unsorted) % 0.41/0.80 (declare-const tptp.s_KR $$unsorted) % 0.41/0.80 (declare-const tptp.s_KP $$unsorted) % 0.41/0.80 (declare-const tptp.s_JP $$unsorted) % 0.41/0.80 (declare-const tptp.s_HK $$unsorted) % 0.41/0.80 (declare-const tptp.s_CN $$unsorted) % 0.41/0.80 (declare-const tptp.s_IN $$unsorted) % 0.41/0.80 (declare-const tptp.s_g145 $$unsorted) % 0.41/0.81 (declare-const tptp.s_ZW $$unsorted) % 0.41/0.81 (declare-const tptp.s_BT $$unsorted) % 0.41/0.81 (declare-const tptp.s_g143 $$unsorted) % 0.41/0.81 (declare-const tptp.s_ZM $$unsorted) % 0.41/0.81 (declare-const tptp.s_BD $$unsorted) % 0.41/0.81 (declare-const tptp.s_g035 $$unsorted) % 0.41/0.81 (declare-const tptp.s_YT $$unsorted) % 0.41/0.81 (declare-const tptp.s_AF $$unsorted) % 0.41/0.81 (declare-const tptp.s_g030 $$unsorted) % 0.41/0.81 (declare-const tptp.s_UG $$unsorted) % 0.41/0.81 (declare-const tptp.s_TZ $$unsorted) % 0.41/0.81 (declare-const tptp.s_YD $$unsorted) % 0.41/0.81 (declare-const tptp.s_SO $$unsorted) % 0.41/0.81 (declare-const tptp.s_PS $$unsorted) % 0.41/0.81 (declare-const tptp.s_g057 $$unsorted) % 0.41/0.81 (declare-const tptp.s_MG $$unsorted) % 0.41/0.81 (declare-const tptp.s_YU $$unsorted) % 0.41/0.81 (declare-const tptp.s_OM $$unsorted) % 0.41/0.81 (declare-const tptp.s_g054 $$unsorted) % 0.41/0.81 (declare-const tptp.s_KM $$unsorted) % 0.41/0.81 (declare-const tptp.s_VA $$unsorted) % 0.41/0.81 (declare-const tptp.s_LB $$unsorted) % 0.41/0.81 (declare-const tptp.s_g053 $$unsorted) % 0.41/0.81 (declare-const tptp.s_g001 $$unsorted) % 0.41/0.81 (declare-const tptp.s_SM $$unsorted) % 0.41/0.81 (declare-const tptp.s_KW $$unsorted) % 0.41/0.81 (declare-const tptp.s_SI $$unsorted) % 0.41/0.81 (declare-const tptp.s_JO $$unsorted) % 0.41/0.81 (declare-const tptp.s_PT $$unsorted) % 0.41/0.81 (declare-const tptp.s_g062 $$unsorted) % 0.41/0.81 (declare-const tptp.s_LK $$unsorted) % 0.41/0.81 (declare-const tptp.s_g034 $$unsorted) % 0.41/0.81 (declare-const tptp.s_IR $$unsorted) % 0.41/0.81 (declare-const tptp.s_YE $$unsorted) % 0.41/0.81 (declare-const tptp.s_SC $$unsorted) % 0.41/0.81 (declare-const tptp.s_g419 $$unsorted) % 0.41/0.81 (declare-const tptp.s_GQ $$unsorted) % 0.41/0.81 (declare-const tptp.s_TR $$unsorted) % 0.41/0.81 (declare-const tptp.s_RW $$unsorted) % 0.41/0.81 (declare-const tptp.s_g003 $$unsorted) % 0.41/0.81 (declare-const tptp.s_GA $$unsorted) % 0.41/0.81 (declare-const tptp.s_SY $$unsorted) % 0.41/0.81 (declare-const tptp.s_RE $$unsorted) % 0.41/0.81 (declare-const tptp.s_g029 $$unsorted) % 0.41/0.81 (declare-const tptp.s_CM $$unsorted) % 0.41/0.81 (declare-const tptp.s_QA $$unsorted) % 0.41/0.81 (declare-const tptp.s_g061 $$unsorted) % 0.41/0.81 (declare-const tptp.s_MU $$unsorted) % 0.41/0.81 (declare-const tptp.s_g005 $$unsorted) % 0.41/0.81 (declare-const tptp.s_ZR $$unsorted) % 0.41/0.81 (declare-const tptp.s_SA $$unsorted) % 0.41/0.81 (declare-const tptp.s_MW $$unsorted) % 0.41/0.81 (declare-const tptp.s_g013 $$unsorted) % 0.41/0.81 (declare-const tptp.s_CF $$unsorted) % 0.41/0.81 (declare-const tptp.s_g019 $$unsorted) % 0.41/0.81 (declare-const tptp.s_GT $$unsorted) % 0.41/0.81 (declare-const tptp.s_GL $$unsorted) % 0.41/0.81 (declare-const tptp.s_ID $$unsorted) % 0.41/0.81 (declare-const tptp.s_SN $$unsorted) % 0.41/0.81 (declare-const tptp.s_GE $$unsorted) % 0.41/0.81 (declare-const tptp.s_g015 $$unsorted) % 0.41/0.81 (declare-const tptp.s_NT $$unsorted) % 0.41/0.81 (declare-const tptp.s_MZ $$unsorted) % 0.41/0.81 (declare-const tptp.s_g021 $$unsorted) % 0.41/0.81 (declare-const tptp.s_CG $$unsorted) % 0.41/0.81 (declare-const tptp.s_AE $$unsorted) % 0.41/0.81 (declare-const tptp.s_g142 $$unsorted) % 0.41/0.81 (declare-const tptp.s_HN $$unsorted) % 0.41/0.81 (declare-const tptp.s_PM $$unsorted) % 0.41/0.81 (declare-const tptp.s_UZ $$unsorted) % 0.41/0.81 (declare-const tptp.s_g009 $$unsorted) % 0.41/0.81 (declare-const tptp.s_CR $$unsorted) % 0.41/0.81 (declare-const tptp.s_CA $$unsorted) % 0.41/0.81 (declare-const tptp.s_AM $$unsorted) % 0.41/0.81 (declare-const tptp.s_g150 $$unsorted) % 0.41/0.81 (declare-const tptp.s_MX $$unsorted) % 0.41/0.81 (declare-const tptp.s_US $$unsorted) % 0.41/0.81 (declare-const tptp.s_AZ $$unsorted) % 0.41/0.81 (declare-const tptp.s_partOf (-> $$unsorted $$unsorted Bool)) % 0.41/0.81 (declare-const tptp.s_NI $$unsorted) % 0.41/0.81 (declare-const tptp.s_BH $$unsorted) % 0.41/0.81 (declare-const tptp.s_g011 $$unsorted) % 0.41/0.81 (declare-const tptp.s_PA $$unsorted) % 0.41/0.81 (declare-const tptp.s_AG $$unsorted) % 0.41/0.81 (declare-const tptp.s_CY $$unsorted) % 0.41/0.81 (declare-const tptp.s_g014 $$unsorted) % 0.41/0.81 (declare-const tptp.s_SV $$unsorted) % 0.41/0.81 (declare-const tptp.s_AI $$unsorted) % 0.41/0.81 (declare-const tptp.s_IL $$unsorted) % 0.41/0.81 (declare-const tptp.s_CS $$unsorted) % 0.41/0.81 (declare-const tptp.s_g017 $$unsorted) % 0.41/0.81 (declare-const tptp.s_IQ $$unsorted) % 0.41/0.81 (declare-const tptp.s_RS $$unsorted) % 0.41/0.81 (declare-const tptp.s_g018 $$unsorted) % 0.41/0.81 (declare-const tptp.s_g039 $$unsorted) % 0.41/0.81 (declare-const tptp.s_g151 $$unsorted) % 0.41/0.81 (declare-const tptp.s_g002 $$unsorted) % 0.41/0.81 (declare-const tptp.s_HT $$unsorted) % 0.41/0.81 (declare-const tptp.s_contains (-> $$unsorted $$unsorted Bool)) % 0.41/0.81 (declare-const tptp.s_JM $$unsorted) % 0.41/0.81 (declare-const tptp.s_NG $$unsorted) % 0.41/0.81 (declare-const tptp.s_SH $$unsorted) % 0.41/0.81 (declare-const tptp.s_BN $$unsorted) % 0.41/0.81 (declare-const tptp.s_SL $$unsorted) % 0.41/0.81 (declare-const tptp.s_KH $$unsorted) % 0.41/0.81 (declare-const tptp.s_TG $$unsorted) % 0.41/0.81 (declare-const tptp.s_VN $$unsorted) % 0.41/0.81 (declare-const tptp.s_BZ $$unsorted) % 0.41/0.81 (declare-const tptp.s_BM $$unsorted) % 0.41/0.81 (declare-const tptp.s_MV $$unsorted) % 0.41/0.81 (declare-const tptp.s_NP $$unsorted) % 0.41/0.81 (declare-const tptp.s_PK $$unsorted) % 0.41/0.81 (declare-const tptp.s_g172 $$unsorted) % 0.41/0.81 (declare-const tptp.s_DZ $$unsorted) % 0.41/0.81 (declare-const tptp.s_EG $$unsorted) % 0.41/0.81 (declare-const tptp.s_EH $$unsorted) % 0.41/0.81 (declare-const tptp.s_LY $$unsorted) % 0.41/0.81 (declare-const tptp.s_MA $$unsorted) % 0.41/0.81 (declare-const tptp.s_SD $$unsorted) % 0.41/0.81 (declare-const tptp.s_TN $$unsorted) % 0.41/0.81 (declare-const tptp.s_AD $$unsorted) % 0.41/0.81 (declare-const tptp.s_AL $$unsorted) % 0.41/0.81 (declare-const tptp.s_BA $$unsorted) % 0.41/0.81 (declare-const tptp.s_ES $$unsorted) % 0.41/0.81 (declare-const tptp.s_GI $$unsorted) % 0.41/0.81 (declare-const tptp.s_GR $$unsorted) % 0.41/0.81 (declare-const tptp.s_HR $$unsorted) % 0.41/0.81 (declare-const tptp.s_IT $$unsorted) % 0.41/0.81 (declare-const tptp.s_ME $$unsorted) % 0.41/0.81 (declare-const tptp.s_MK $$unsorted) % 0.41/0.81 (declare-const tptp.s_MT $$unsorted) % 0.41/0.81 (declare-const tptp.s_BG $$unsorted) % 0.41/0.81 (declare-const tptp.s_KY $$unsorted) % 0.41/0.81 (declare-const tptp.s_BY $$unsorted) % 0.41/0.81 (declare-const tptp.s_LC $$unsorted) % 0.41/0.81 (declare-const tptp.s_CZ $$unsorted) % 0.41/0.81 (declare-const tptp.s_MF $$unsorted) % 0.41/0.81 (declare-const tptp.s_HU $$unsorted) % 0.41/0.81 (declare-const tptp.s_MQ $$unsorted) % 0.41/0.81 (declare-const tptp.s_MD $$unsorted) % 0.41/0.81 (declare-const tptp.s_MS $$unsorted) % 0.41/0.81 (declare-const tptp.s_PL $$unsorted) % 0.41/0.81 (declare-const tptp.s_PR $$unsorted) % 0.41/0.81 (declare-const tptp.s_RO $$unsorted) % 0.41/0.81 (declare-const tptp.s_BI $$unsorted) % 0.41/0.81 (declare-const tptp.s_TC $$unsorted) % 0.41/0.81 (declare-const tptp.s_RU $$unsorted) % 0.41/0.81 (declare-const tptp.s_DJ $$unsorted) % 0.41/0.81 (declare-const tptp.s_TT $$unsorted) % 0.41/0.81 (declare-const tptp.s_SU $$unsorted) % 0.41/0.81 (declare-const tptp.s_ER $$unsorted) % 0.41/0.81 (declare-const tptp.s_VC $$unsorted) % 0.41/0.81 (declare-const tptp.s_SK $$unsorted) % 0.41/0.81 (declare-const tptp.s_ET $$unsorted) % 0.41/0.81 (declare-const tptp.s_VG $$unsorted) % 0.41/0.81 (declare-const tptp.s_UA $$unsorted) % 0.41/0.81 (declare-const tptp.s_KE $$unsorted) % 0.41/0.81 (declare-const tptp.s_VI $$unsorted) % 0.41/0.81 (declare-const tptp.s_GG $$unsorted) % 0.41/0.81 (declare-const tptp.s_IM $$unsorted) % 0.41/0.81 (declare-const tptp.s_JE $$unsorted) % 0.41/0.81 (declare-const tptp.s_AX $$unsorted) % 0.41/0.81 (declare-const tptp.s_DK $$unsorted) % 0.41/0.81 (declare-const tptp.s_EE $$unsorted) % 0.41/0.81 (declare-const tptp.s_FI $$unsorted) % 0.41/0.81 (declare-const tptp.s_FO $$unsorted) % 0.41/0.81 (declare-const tptp.s_GB $$unsorted) % 0.41/0.81 (declare-const tptp.s_IE $$unsorted) % 0.41/0.81 (declare-const tptp.s_IS $$unsorted) % 0.41/0.81 (declare-const tptp.s_LT $$unsorted) % 0.41/0.81 (declare-const tptp.s_LV $$unsorted) % 0.41/0.81 (declare-const tptp.s_NO $$unsorted) % 0.41/0.81 (declare-const tptp.s_SE $$unsorted) % 0.41/0.81 (declare-const tptp.s_SJ $$unsorted) % 0.41/0.81 (declare-const tptp.s_CH $$unsorted) % 0.41/0.81 (declare-const tptp.s_DE $$unsorted) % 0.41/0.81 (declare-const tptp.s_DD $$unsorted) % 0.41/0.81 (declare-const tptp.s_FR $$unsorted) % 0.41/0.81 (declare-const tptp.s_FX $$unsorted) % 0.41/0.81 (declare-const tptp.s_LI $$unsorted) % 0.41/0.81 (declare-const tptp.s_LU $$unsorted) % 0.41/0.81 (declare-const tptp.s_MC $$unsorted) % 0.41/0.81 (declare-const tptp.s_NL $$unsorted) % 0.41/0.81 (declare-const tptp.s_AO $$unsorted) % 0.41/0.81 (declare-const tptp.s_CD $$unsorted) % 0.41/0.81 (declare-const tptp.s_ST $$unsorted) % 0.41/0.81 (declare-const tptp.s_TD $$unsorted) % 0.41/0.81 (declare-const tptp.s_BW $$unsorted) % 0.41/0.81 (declare-const tptp.s_LS $$unsorted) % 0.41/0.81 (declare-const tptp.s_NA $$unsorted) % 0.41/0.81 (declare-const tptp.s_SZ $$unsorted) % 0.41/0.81 (declare-const tptp.s_ZA $$unsorted) % 0.41/0.81 (declare-const tptp.s_g154 $$unsorted) % 0.41/0.81 (declare-const tptp.s_AR $$unsorted) % 0.41/0.81 (declare-const tptp.s_g155 $$unsorted) % 0.41/0.81 (declare-const tptp.s_BO $$unsorted) % 0.41/0.81 (declare-const tptp.s_BF $$unsorted) % 0.41/0.81 (declare-const tptp.s_BR $$unsorted) % 0.41/0.81 (declare-const tptp.s_BJ $$unsorted) % 0.41/0.81 (declare-const tptp.s_CL $$unsorted) % 0.41/0.81 (declare-const tptp.s_CI $$unsorted) % 0.41/0.81 (declare-const tptp.s_CO $$unsorted) % 0.41/0.81 (declare-const tptp.s_CV $$unsorted) % 0.41/0.81 (declare-const tptp.s_EC $$unsorted) % 0.41/0.81 (declare-const tptp.s_GH $$unsorted) % 0.41/0.81 (declare-const tptp.s_FK $$unsorted) % 0.41/0.81 (declare-const tptp.s_GM $$unsorted) % 0.41/0.81 (declare-const tptp.s_GF $$unsorted) % 0.41/0.81 (declare-const tptp.s_GN $$unsorted) % 0.41/0.81 (declare-const tptp.s_GY $$unsorted) % 0.41/0.81 (declare-const tptp.s_GW $$unsorted) % 0.41/0.81 (declare-const tptp.s_PE $$unsorted) % 0.41/0.81 (declare-const tptp.s_LR $$unsorted) % 0.41/0.81 (declare-const tptp.s_PY $$unsorted) % 0.41/0.81 (declare-const tptp.s_ML $$unsorted) % 0.41/0.81 (declare-const tptp.s_SR $$unsorted) % 0.41/0.81 (declare-const tptp.s_MR $$unsorted) % 0.41/0.81 (declare-const tptp.s_UY $$unsorted) % 0.41/0.81 (declare-const tptp.s_NE $$unsorted) % 0.41/0.81 (declare-const tptp.s_VE $$unsorted) % 0.41/0.81 (declare-const tptp.s_AN $$unsorted) % 0.41/0.81 (declare-const tptp.s_AW $$unsorted) % 0.41/0.81 (declare-const tptp.s_BB $$unsorted) % 0.41/0.81 (declare-const tptp.s_BL $$unsorted) % 0.41/0.81 (declare-const tptp.s_BS $$unsorted) % 0.41/0.81 (declare-const tptp.s_CU $$unsorted) % 0.41/0.81 (declare-const tptp.s_DM $$unsorted) % 0.41/0.81 (declare-const tptp.s_DO $$unsorted) % 0.41/0.81 (declare-const tptp.s_GD $$unsorted) % 0.41/0.81 (declare-const tptp.s_GP $$unsorted) % 0.41/0.81 (declare-const tptp.s_KN $$unsorted) % 0.41/0.81 (define @t1 () (tptp.s_contains tptp.s_g019 tptp.s_g013)) % 0.41/0.81 (define @t2 () (tptp.s_contains tptp.s_g013 tptp.s_MX)) % 0.41/0.81 (define @t3 () (@var "Z" $$unsorted)) % 0.41/0.81 (define @t4 () (@var "X" $$unsorted)) % 0.41/0.81 (define @t5 () (tptp.s_contains @t4 @t3)) % 0.41/0.81 (define @t6 () (@var "Y" $$unsorted)) % 0.41/0.81 (define @t7 () (tptp.s_contains @t6 @t3)) % 0.41/0.81 (define @t8 () (tptp.s_contains @t4 @t6)) % 0.41/0.81 (define @t9 () (and @t8 @t7)) % 0.41/0.81 (define @t10 () (@list @t4 @t6 @t3)) % 0.41/0.81 (define @t11 () (forall @t10 (=> @t9 @t5))) % 0.41/0.81 (define @t12 () (@list @t4 @t6)) % 0.41/0.81 (define @t13 () (tptp.s_contains tptp.s_g019 tptp.s_MX)) % 0.41/0.81 (define @t14 () (not @t7)) % 0.41/0.81 (define @t15 () (not @t8)) % 0.41/0.81 (define @t16 () (or @t15 @t14 @t5)) % 0.41/0.81 (define @t17 () (not @t2)) % 0.41/0.81 (define @t18 () (not @t1)) % 0.41/0.81 (define @t19 () (or @t18 @t17 @t13)) % 0.41/0.81 (define @t20 () (not @t19)) % 0.41/0.81 (define @t21 () (forall @t10 @t16)) % 0.41/0.81 (assume @p1 (tptp.s_contains tptp.s_g001 tptp.s_g002)) % 0.41/0.81 (assume @p2 (tptp.s_contains tptp.s_g001 tptp.s_g009)) % 0.41/0.81 (assume @p3 (tptp.s_contains tptp.s_g001 tptp.s_g019)) % 0.41/0.81 (assume @p4 (tptp.s_contains tptp.s_g001 tptp.s_g142)) % 0.41/0.81 (assume @p5 (tptp.s_contains tptp.s_g001 tptp.s_g150)) % 0.41/0.81 (assume @p6 (tptp.s_partOf tptp.s_g002 tptp.s_g001)) % 0.41/0.81 (assume @p7 (tptp.s_contains tptp.s_g002 tptp.s_g011)) % 0.41/0.81 (assume @p8 (tptp.s_contains tptp.s_g002 tptp.s_g014)) % 0.41/0.81 (assume @p9 (tptp.s_contains tptp.s_g002 tptp.s_g015)) % 0.41/0.81 (assume @p10 (tptp.s_contains tptp.s_g002 tptp.s_g017)) % 0.41/0.81 (assume @p11 (tptp.s_contains tptp.s_g002 tptp.s_g018)) % 0.41/0.81 (assume @p12 (tptp.s_partOf tptp.s_g009 tptp.s_g001)) % 0.41/0.81 (assume @p13 (tptp.s_contains tptp.s_g009 tptp.s_g053)) % 0.41/0.81 (assume @p14 (tptp.s_contains tptp.s_g009 tptp.s_g054)) % 0.41/0.81 (assume @p15 (tptp.s_contains tptp.s_g009 tptp.s_g057)) % 0.41/0.81 (assume @p16 (tptp.s_contains tptp.s_g009 tptp.s_g061)) % 0.41/0.81 (assume @p17 (tptp.s_partOf tptp.s_g019 tptp.s_g001)) % 0.41/0.81 (assume @p18 (tptp.s_contains tptp.s_g019 tptp.s_g005)) % 0.41/0.81 (assume @p19 @t1) % 0.41/0.81 (assume @p20 (tptp.s_contains tptp.s_g019 tptp.s_g021)) % 0.41/0.81 (assume @p21 (tptp.s_contains tptp.s_g019 tptp.s_g029)) % 0.41/0.81 (assume @p22 (tptp.s_contains tptp.s_g019 tptp.s_g003)) % 0.41/0.81 (assume @p23 (tptp.s_contains tptp.s_g019 tptp.s_g419)) % 0.41/0.81 (assume @p24 (tptp.s_partOf tptp.s_g142 tptp.s_g001)) % 0.41/0.81 (assume @p25 (tptp.s_contains tptp.s_g142 tptp.s_g030)) % 0.41/0.81 (assume @p26 (tptp.s_contains tptp.s_g142 tptp.s_g035)) % 0.41/0.81 (assume @p27 (tptp.s_contains tptp.s_g142 tptp.s_g143)) % 0.41/0.81 (assume @p28 (tptp.s_contains tptp.s_g142 tptp.s_g145)) % 0.41/0.81 (assume @p29 (tptp.s_contains tptp.s_g142 tptp.s_g034)) % 0.41/0.81 (assume @p30 (tptp.s_contains tptp.s_g142 tptp.s_g062)) % 0.41/0.81 (assume @p31 (tptp.s_partOf tptp.s_g150 tptp.s_g001)) % 0.41/0.81 (assume @p32 (tptp.s_contains tptp.s_g150 tptp.s_g039)) % 0.41/0.81 (assume @p33 (tptp.s_contains tptp.s_g150 tptp.s_g151)) % 0.41/0.81 (assume @p34 (tptp.s_contains tptp.s_g150 tptp.s_g154)) % 0.41/0.81 (assume @p35 (tptp.s_contains tptp.s_g150 tptp.s_g155)) % 0.41/0.81 (assume @p36 (tptp.s_contains tptp.s_g011 tptp.s_BF)) % 0.41/0.81 (assume @p37 (tptp.s_contains tptp.s_g011 tptp.s_BJ)) % 0.41/0.81 (assume @p38 (tptp.s_contains tptp.s_g011 tptp.s_CI)) % 0.41/0.81 (assume @p39 (tptp.s_contains tptp.s_g011 tptp.s_CV)) % 0.41/0.81 (assume @p40 (tptp.s_contains tptp.s_g011 tptp.s_GH)) % 0.41/0.81 (assume @p41 (tptp.s_contains tptp.s_g011 tptp.s_GM)) % 0.41/0.81 (assume @p42 (tptp.s_contains tptp.s_g011 tptp.s_GN)) % 0.41/0.81 (assume @p43 (tptp.s_contains tptp.s_g011 tptp.s_GW)) % 0.41/0.81 (assume @p44 (tptp.s_contains tptp.s_g011 tptp.s_LR)) % 0.41/0.81 (assume @p45 (tptp.s_contains tptp.s_g011 tptp.s_ML)) % 0.41/0.81 (assume @p46 (tptp.s_contains tptp.s_g011 tptp.s_MR)) % 0.41/0.81 (assume @p47 (tptp.s_contains tptp.s_g011 tptp.s_NE)) % 0.41/0.81 (assume @p48 (tptp.s_contains tptp.s_g011 tptp.s_NG)) % 0.41/0.81 (assume @p49 (tptp.s_contains tptp.s_g011 tptp.s_SH)) % 0.41/0.81 (assume @p50 (tptp.s_contains tptp.s_g011 tptp.s_SL)) % 0.41/0.81 (assume @p51 (tptp.s_contains tptp.s_g011 tptp.s_SN)) % 0.41/0.81 (assume @p52 (tptp.s_contains tptp.s_g011 tptp.s_TG)) % 0.41/0.81 (assume @p53 (tptp.s_partOf tptp.s_g011 tptp.s_g002)) % 0.41/0.81 (assume @p54 (tptp.s_partOf tptp.s_BF tptp.s_g011)) % 0.41/0.81 (assume @p55 (tptp.s_partOf tptp.s_BJ tptp.s_g011)) % 0.41/0.81 (assume @p56 (tptp.s_partOf tptp.s_CI tptp.s_g011)) % 0.41/0.81 (assume @p57 (tptp.s_partOf tptp.s_CV tptp.s_g011)) % 0.41/0.81 (assume @p58 (tptp.s_partOf tptp.s_GH tptp.s_g011)) % 0.41/0.81 (assume @p59 (tptp.s_partOf tptp.s_GM tptp.s_g011)) % 0.41/0.81 (assume @p60 (tptp.s_partOf tptp.s_GN tptp.s_g011)) % 0.41/0.81 (assume @p61 (tptp.s_partOf tptp.s_GW tptp.s_g011)) % 0.41/0.81 (assume @p62 (tptp.s_partOf tptp.s_LR tptp.s_g011)) % 0.41/0.81 (assume @p63 (tptp.s_partOf tptp.s_ML tptp.s_g011)) % 0.41/0.81 (assume @p64 (tptp.s_partOf tptp.s_MR tptp.s_g011)) % 0.41/0.81 (assume @p65 (tptp.s_partOf tptp.s_NE tptp.s_g011)) % 0.41/0.81 (assume @p66 (tptp.s_partOf tptp.s_NG tptp.s_g011)) % 0.41/0.81 (assume @p67 (tptp.s_partOf tptp.s_SH tptp.s_g011)) % 0.41/0.81 (assume @p68 (tptp.s_partOf tptp.s_SL tptp.s_g011)) % 0.41/0.81 (assume @p69 (tptp.s_partOf tptp.s_SN tptp.s_g011)) % 0.41/0.81 (assume @p70 (tptp.s_partOf tptp.s_TG tptp.s_g011)) % 0.41/0.81 (assume @p71 (tptp.s_contains tptp.s_g013 tptp.s_BZ)) % 0.41/0.81 (assume @p72 (tptp.s_contains tptp.s_g013 tptp.s_CR)) % 0.41/0.81 (assume @p73 (tptp.s_contains tptp.s_g013 tptp.s_GT)) % 0.41/0.81 (assume @p74 (tptp.s_contains tptp.s_g013 tptp.s_HN)) % 0.41/0.81 (assume @p75 @t2) % 0.41/0.81 (assume @p76 (tptp.s_contains tptp.s_g013 tptp.s_NI)) % 0.41/0.81 (assume @p77 (tptp.s_contains tptp.s_g013 tptp.s_PA)) % 0.41/0.81 (assume @p78 (tptp.s_contains tptp.s_g013 tptp.s_SV)) % 0.41/0.81 (assume @p79 (tptp.s_partOf tptp.s_g013 tptp.s_g019)) % 0.41/0.81 (assume @p80 (tptp.s_partOf tptp.s_g013 tptp.s_g003)) % 0.41/0.81 (assume @p81 (tptp.s_partOf tptp.s_g013 tptp.s_g419)) % 0.41/0.81 (assume @p82 (tptp.s_partOf tptp.s_BZ tptp.s_g013)) % 0.41/0.81 (assume @p83 (tptp.s_partOf tptp.s_CR tptp.s_g013)) % 0.41/0.81 (assume @p84 (tptp.s_partOf tptp.s_GT tptp.s_g013)) % 0.41/0.81 (assume @p85 (tptp.s_partOf tptp.s_HN tptp.s_g013)) % 0.41/0.81 (assume @p86 (tptp.s_partOf tptp.s_MX tptp.s_g013)) % 0.41/0.81 (assume @p87 (tptp.s_partOf tptp.s_NI tptp.s_g013)) % 0.41/0.81 (assume @p88 (tptp.s_partOf tptp.s_PA tptp.s_g013)) % 0.41/0.81 (assume @p89 (tptp.s_partOf tptp.s_SV tptp.s_g013)) % 0.41/0.81 (assume @p90 (tptp.s_contains tptp.s_g014 tptp.s_BI)) % 0.41/0.81 (assume @p91 (tptp.s_contains tptp.s_g014 tptp.s_DJ)) % 0.41/0.81 (assume @p92 (tptp.s_contains tptp.s_g014 tptp.s_ER)) % 0.41/0.81 (assume @p93 (tptp.s_contains tptp.s_g014 tptp.s_ET)) % 0.41/0.81 (assume @p94 (tptp.s_contains tptp.s_g014 tptp.s_KE)) % 0.41/0.81 (assume @p95 (tptp.s_contains tptp.s_g014 tptp.s_KM)) % 0.41/0.81 (assume @p96 (tptp.s_contains tptp.s_g014 tptp.s_MG)) % 0.41/0.81 (assume @p97 (tptp.s_contains tptp.s_g014 tptp.s_MU)) % 0.41/0.81 (assume @p98 (tptp.s_contains tptp.s_g014 tptp.s_MW)) % 0.41/0.81 (assume @p99 (tptp.s_contains tptp.s_g014 tptp.s_MZ)) % 0.41/0.81 (assume @p100 (tptp.s_contains tptp.s_g014 tptp.s_RE)) % 0.41/0.81 (assume @p101 (tptp.s_contains tptp.s_g014 tptp.s_RW)) % 0.41/0.81 (assume @p102 (tptp.s_contains tptp.s_g014 tptp.s_SC)) % 0.41/0.81 (assume @p103 (tptp.s_contains tptp.s_g014 tptp.s_SO)) % 0.41/0.81 (assume @p104 (tptp.s_contains tptp.s_g014 tptp.s_TZ)) % 0.41/0.81 (assume @p105 (tptp.s_contains tptp.s_g014 tptp.s_UG)) % 0.41/0.81 (assume @p106 (tptp.s_contains tptp.s_g014 tptp.s_YT)) % 0.41/0.81 (assume @p107 (tptp.s_contains tptp.s_g014 tptp.s_ZM)) % 0.41/0.81 (assume @p108 (tptp.s_contains tptp.s_g014 tptp.s_ZW)) % 0.41/0.81 (assume @p109 (tptp.s_partOf tptp.s_g014 tptp.s_g002)) % 0.41/0.81 (assume @p110 (tptp.s_partOf tptp.s_BI tptp.s_g014)) % 0.41/0.81 (assume @p111 (tptp.s_partOf tptp.s_DJ tptp.s_g014)) % 0.41/0.81 (assume @p112 (tptp.s_partOf tptp.s_ER tptp.s_g014)) % 0.41/0.81 (assume @p113 (tptp.s_partOf tptp.s_ET tptp.s_g014)) % 0.41/0.81 (assume @p114 (tptp.s_partOf tptp.s_KE tptp.s_g014)) % 0.41/0.81 (assume @p115 (tptp.s_partOf tptp.s_KM tptp.s_g014)) % 0.41/0.81 (assume @p116 (tptp.s_partOf tptp.s_MG tptp.s_g014)) % 0.41/0.81 (assume @p117 (tptp.s_partOf tptp.s_MU tptp.s_g014)) % 0.41/0.81 (assume @p118 (tptp.s_partOf tptp.s_MW tptp.s_g014)) % 0.41/0.81 (assume @p119 (tptp.s_partOf tptp.s_MZ tptp.s_g014)) % 0.41/0.81 (assume @p120 (tptp.s_partOf tptp.s_RE tptp.s_g014)) % 0.41/0.81 (assume @p121 (tptp.s_partOf tptp.s_RW tptp.s_g014)) % 0.41/0.81 (assume @p122 (tptp.s_partOf tptp.s_SC tptp.s_g014)) % 0.41/0.81 (assume @p123 (tptp.s_partOf tptp.s_SO tptp.s_g014)) % 0.41/0.81 (assume @p124 (tptp.s_partOf tptp.s_TZ tptp.s_g014)) % 0.41/0.81 (assume @p125 (tptp.s_partOf tptp.s_UG tptp.s_g014)) % 0.41/0.81 (assume @p126 (tptp.s_partOf tptp.s_YT tptp.s_g014)) % 0.41/0.81 (assume @p127 (tptp.s_partOf tptp.s_ZM tptp.s_g014)) % 0.41/0.81 (assume @p128 (tptp.s_partOf tptp.s_ZW tptp.s_g014)) % 0.41/0.81 (assume @p129 (tptp.s_partOf tptp.s_g030 tptp.s_g142)) % 0.41/0.81 (assume @p130 (tptp.s_contains tptp.s_g030 tptp.s_CN)) % 0.41/0.81 (assume @p131 (tptp.s_contains tptp.s_g030 tptp.s_HK)) % 0.41/0.81 (assume @p132 (tptp.s_contains tptp.s_g030 tptp.s_JP)) % 0.41/0.81 (assume @p133 (tptp.s_contains tptp.s_g030 tptp.s_KP)) % 0.41/0.81 (assume @p134 (tptp.s_contains tptp.s_g030 tptp.s_KR)) % 0.41/0.81 (assume @p135 (tptp.s_contains tptp.s_g030 tptp.s_MN)) % 0.41/0.81 (assume @p136 (tptp.s_contains tptp.s_g030 tptp.s_MO)) % 0.41/0.81 (assume @p137 (tptp.s_contains tptp.s_g030 tptp.s_TW)) % 0.41/0.81 (assume @p138 (tptp.s_partOf tptp.s_g035 tptp.s_g142)) % 0.41/0.81 (assume @p139 (tptp.s_contains tptp.s_g035 tptp.s_BN)) % 0.41/0.81 (assume @p140 (tptp.s_contains tptp.s_g035 tptp.s_ID)) % 0.41/0.81 (assume @p141 (tptp.s_contains tptp.s_g035 tptp.s_KH)) % 0.41/0.81 (assume @p142 (tptp.s_contains tptp.s_g035 tptp.s_LA)) % 0.41/0.81 (assume @p143 (tptp.s_contains tptp.s_g035 tptp.s_MM)) % 0.41/0.81 (assume @p144 (tptp.s_contains tptp.s_g035 tptp.s_BU)) % 0.41/0.81 (assume @p145 (tptp.s_contains tptp.s_g035 tptp.s_MY)) % 0.41/0.81 (assume @p146 (tptp.s_contains tptp.s_g035 tptp.s_PH)) % 0.41/0.81 (assume @p147 (tptp.s_contains tptp.s_g035 tptp.s_SG)) % 0.41/0.81 (assume @p148 (tptp.s_contains tptp.s_g035 tptp.s_TH)) % 0.41/0.81 (assume @p149 (tptp.s_contains tptp.s_g035 tptp.s_TL)) % 0.41/0.81 (assume @p150 (tptp.s_contains tptp.s_g035 tptp.s_TP)) % 0.41/0.81 (assume @p151 (tptp.s_contains tptp.s_g035 tptp.s_VN)) % 0.41/0.81 (assume @p152 (tptp.s_partOf tptp.s_g143 tptp.s_g142)) % 0.41/0.81 (assume @p153 (tptp.s_contains tptp.s_g143 tptp.s_TM)) % 0.41/0.81 (assume @p154 (tptp.s_contains tptp.s_g143 tptp.s_TJ)) % 0.41/0.81 (assume @p155 (tptp.s_contains tptp.s_g143 tptp.s_KG)) % 0.41/0.81 (assume @p156 (tptp.s_contains tptp.s_g143 tptp.s_KZ)) % 0.41/0.81 (assume @p157 (tptp.s_contains tptp.s_g143 tptp.s_UZ)) % 0.41/0.81 (assume @p158 (tptp.s_partOf tptp.s_g143 tptp.s_g062)) % 0.41/0.81 (assume @p159 (tptp.s_partOf tptp.s_g145 tptp.s_g142)) % 0.41/0.81 (assume @p160 (tptp.s_contains tptp.s_g145 tptp.s_AE)) % 0.41/0.81 (assume @p161 (tptp.s_contains tptp.s_g145 tptp.s_AM)) % 0.41/0.81 (assume @p162 (tptp.s_contains tptp.s_g145 tptp.s_AZ)) % 0.41/0.81 (assume @p163 (tptp.s_contains tptp.s_g145 tptp.s_BH)) % 0.41/0.81 (assume @p164 (tptp.s_contains tptp.s_g145 tptp.s_CY)) % 0.41/0.81 (assume @p165 (tptp.s_contains tptp.s_g145 tptp.s_GE)) % 0.41/0.81 (assume @p166 (tptp.s_contains tptp.s_g145 tptp.s_IL)) % 0.41/0.81 (assume @p167 (tptp.s_contains tptp.s_g145 tptp.s_IQ)) % 0.41/0.81 (assume @p168 (tptp.s_contains tptp.s_g145 tptp.s_JO)) % 0.41/0.81 (assume @p169 (tptp.s_contains tptp.s_g145 tptp.s_KW)) % 0.41/0.81 (assume @p170 (tptp.s_contains tptp.s_g145 tptp.s_LB)) % 0.41/0.81 (assume @p171 (tptp.s_contains tptp.s_g145 tptp.s_OM)) % 0.41/0.81 (assume @p172 (tptp.s_contains tptp.s_g145 tptp.s_PS)) % 0.41/0.81 (assume @p173 (tptp.s_contains tptp.s_g145 tptp.s_QA)) % 0.41/0.81 (assume @p174 (tptp.s_contains tptp.s_g145 tptp.s_SA)) % 0.41/0.81 (assume @p175 (tptp.s_contains tptp.s_g145 tptp.s_NT)) % 0.41/0.81 (assume @p176 (tptp.s_contains tptp.s_g145 tptp.s_SY)) % 0.41/0.81 (assume @p177 (tptp.s_contains tptp.s_g145 tptp.s_TR)) % 0.41/0.81 (assume @p178 (tptp.s_contains tptp.s_g145 tptp.s_YE)) % 0.41/0.81 (assume @p179 (tptp.s_contains tptp.s_g145 tptp.s_YD)) % 0.41/0.81 (assume @p180 (tptp.s_partOf tptp.s_g034 tptp.s_g142)) % 0.41/0.81 (assume @p181 (tptp.s_partOf tptp.s_g034 tptp.s_g062)) % 0.41/0.81 (assume @p182 (tptp.s_contains tptp.s_g034 tptp.s_AF)) % 0.41/0.81 (assume @p183 (tptp.s_contains tptp.s_g034 tptp.s_BD)) % 0.41/0.81 (assume @p184 (tptp.s_contains tptp.s_g034 tptp.s_BT)) % 0.41/0.81 (assume @p185 (tptp.s_contains tptp.s_g034 tptp.s_IN)) % 0.41/0.81 (assume @p186 (tptp.s_contains tptp.s_g034 tptp.s_IR)) % 0.41/0.81 (assume @p187 (tptp.s_contains tptp.s_g034 tptp.s_LK)) % 0.41/0.81 (assume @p188 (tptp.s_contains tptp.s_g034 tptp.s_MV)) % 0.41/0.81 (assume @p189 (tptp.s_contains tptp.s_g034 tptp.s_NP)) % 0.41/0.81 (assume @p190 (tptp.s_contains tptp.s_g034 tptp.s_PK)) % 0.41/0.81 (assume @p191 (tptp.s_partOf tptp.s_g062 tptp.s_g142)) % 0.41/0.81 (assume @p192 (tptp.s_contains tptp.s_g062 tptp.s_g034)) % 0.41/0.81 (assume @p193 (tptp.s_contains tptp.s_g062 tptp.s_g143)) % 0.41/0.81 (assume @p194 (tptp.s_partOf tptp.s_TM tptp.s_g143)) % 0.41/0.81 (assume @p195 (tptp.s_partOf tptp.s_TM tptp.s_g172)) % 0.41/0.81 (assume @p196 (tptp.s_partOf tptp.s_TJ tptp.s_g143)) % 0.41/0.81 (assume @p197 (tptp.s_partOf tptp.s_TJ tptp.s_g172)) % 0.41/0.81 (assume @p198 (tptp.s_partOf tptp.s_KG tptp.s_g143)) % 0.41/0.81 (assume @p199 (tptp.s_partOf tptp.s_KG tptp.s_g172)) % 0.41/0.81 (assume @p200 (tptp.s_partOf tptp.s_KZ tptp.s_g143)) % 0.41/0.81 (assume @p201 (tptp.s_partOf tptp.s_KZ tptp.s_g172)) % 0.41/0.81 (assume @p202 (tptp.s_partOf tptp.s_UZ tptp.s_g143)) % 0.41/0.81 (assume @p203 (tptp.s_partOf tptp.s_UZ tptp.s_g172)) % 0.41/0.81 (assume @p204 (tptp.s_partOf tptp.s_AE tptp.s_g145)) % 0.41/0.81 (assume @p205 (tptp.s_partOf tptp.s_AM tptp.s_g145)) % 0.41/0.81 (assume @p206 (tptp.s_partOf tptp.s_AM tptp.s_g172)) % 0.41/0.81 (assume @p207 (tptp.s_partOf tptp.s_AZ tptp.s_g145)) % 0.41/0.81 (assume @p208 (tptp.s_partOf tptp.s_AZ tptp.s_g172)) % 0.41/0.81 (assume @p209 (tptp.s_partOf tptp.s_BH tptp.s_g145)) % 0.41/0.81 (assume @p210 (tptp.s_partOf tptp.s_CY tptp.s_g145)) % 0.41/0.81 (assume @p211 (tptp.s_partOf tptp.s_GE tptp.s_g145)) % 0.41/0.81 (assume @p212 (tptp.s_partOf tptp.s_GE tptp.s_g172)) % 0.41/0.81 (assume @p213 (tptp.s_partOf tptp.s_IL tptp.s_g145)) % 0.41/0.81 (assume @p214 (tptp.s_partOf tptp.s_IQ tptp.s_g145)) % 0.41/0.81 (assume @p215 (tptp.s_partOf tptp.s_JO tptp.s_g145)) % 0.41/0.81 (assume @p216 (tptp.s_partOf tptp.s_KW tptp.s_g145)) % 0.41/0.81 (assume @p217 (tptp.s_partOf tptp.s_LB tptp.s_g145)) % 0.41/0.81 (assume @p218 (tptp.s_partOf tptp.s_OM tptp.s_g145)) % 0.41/0.81 (assume @p219 (tptp.s_partOf tptp.s_PS tptp.s_g145)) % 0.41/0.81 (assume @p220 (tptp.s_partOf tptp.s_QA tptp.s_g145)) % 0.41/0.81 (assume @p221 (tptp.s_partOf tptp.s_SA tptp.s_g145)) % 0.41/0.81 (assume @p222 (tptp.s_partOf tptp.s_NT tptp.s_g145)) % 0.41/0.81 (assume @p223 (tptp.s_partOf tptp.s_SY tptp.s_g145)) % 0.41/0.81 (assume @p224 (tptp.s_partOf tptp.s_TR tptp.s_g145)) % 0.41/0.81 (assume @p225 (tptp.s_partOf tptp.s_YE tptp.s_g145)) % 0.41/0.81 (assume @p226 (tptp.s_partOf tptp.s_YD tptp.s_g145)) % 0.41/0.81 (assume @p227 (tptp.s_contains tptp.s_g015 tptp.s_DZ)) % 0.41/0.81 (assume @p228 (tptp.s_contains tptp.s_g015 tptp.s_EG)) % 0.41/0.81 (assume @p229 (tptp.s_contains tptp.s_g015 tptp.s_EH)) % 0.41/0.81 (assume @p230 (tptp.s_contains tptp.s_g015 tptp.s_LY)) % 0.41/0.81 (assume @p231 (tptp.s_contains tptp.s_g015 tptp.s_MA)) % 0.41/0.81 (assume @p232 (tptp.s_contains tptp.s_g015 tptp.s_SD)) % 0.41/0.81 (assume @p233 (tptp.s_contains tptp.s_g015 tptp.s_TN)) % 0.41/0.81 (assume @p234 (tptp.s_partOf tptp.s_g015 tptp.s_g002)) % 0.41/0.81 (assume @p235 (tptp.s_partOf tptp.s_DZ tptp.s_g015)) % 0.41/0.81 (assume @p236 (tptp.s_partOf tptp.s_EG tptp.s_g015)) % 0.41/0.81 (assume @p237 (tptp.s_partOf tptp.s_EH tptp.s_g015)) % 0.41/0.81 (assume @p238 (tptp.s_partOf tptp.s_LY tptp.s_g015)) % 0.41/0.81 (assume @p239 (tptp.s_partOf tptp.s_MA tptp.s_g015)) % 0.41/0.81 (assume @p240 (tptp.s_partOf tptp.s_SD tptp.s_g015)) % 0.41/0.81 (assume @p241 (tptp.s_partOf tptp.s_TN tptp.s_g015)) % 0.41/0.81 (assume @p242 (tptp.s_partOf tptp.s_g039 tptp.s_g150)) % 0.41/0.81 (assume @p243 (tptp.s_contains tptp.s_g039 tptp.s_AD)) % 0.41/0.81 (assume @p244 (tptp.s_contains tptp.s_g039 tptp.s_AL)) % 0.41/0.81 (assume @p245 (tptp.s_contains tptp.s_g039 tptp.s_BA)) % 0.41/0.81 (assume @p246 (tptp.s_contains tptp.s_g039 tptp.s_ES)) % 0.41/0.81 (assume @p247 (tptp.s_contains tptp.s_g039 tptp.s_GI)) % 0.41/0.81 (assume @p248 (tptp.s_contains tptp.s_g039 tptp.s_GR)) % 0.41/0.81 (assume @p249 (tptp.s_contains tptp.s_g039 tptp.s_HR)) % 0.41/0.81 (assume @p250 (tptp.s_contains tptp.s_g039 tptp.s_IT)) % 0.41/0.81 (assume @p251 (tptp.s_contains tptp.s_g039 tptp.s_ME)) % 0.41/0.81 (assume @p252 (tptp.s_contains tptp.s_g039 tptp.s_MK)) % 0.41/0.81 (assume @p253 (tptp.s_contains tptp.s_g039 tptp.s_MT)) % 0.41/0.81 (assume @p254 (tptp.s_contains tptp.s_g039 tptp.s_CS)) % 0.41/0.81 (assume @p255 (tptp.s_contains tptp.s_g039 tptp.s_RS)) % 0.41/0.81 (assume @p256 (tptp.s_contains tptp.s_g039 tptp.s_PT)) % 0.41/0.81 (assume @p257 (tptp.s_contains tptp.s_g039 tptp.s_SI)) % 0.41/0.81 (assume @p258 (tptp.s_contains tptp.s_g039 tptp.s_SM)) % 0.41/0.81 (assume @p259 (tptp.s_contains tptp.s_g039 tptp.s_VA)) % 0.41/0.81 (assume @p260 (tptp.s_contains tptp.s_g039 tptp.s_YU)) % 0.41/0.81 (assume @p261 (tptp.s_partOf tptp.s_g151 tptp.s_g150)) % 0.41/0.81 (assume @p262 (tptp.s_contains tptp.s_g151 tptp.s_BG)) % 0.41/0.81 (assume @p263 (tptp.s_contains tptp.s_g151 tptp.s_BY)) % 0.41/0.81 (assume @p264 (tptp.s_contains tptp.s_g151 tptp.s_CZ)) % 0.41/0.81 (assume @p265 (tptp.s_contains tptp.s_g151 tptp.s_HU)) % 0.41/0.81 (assume @p266 (tptp.s_contains tptp.s_g151 tptp.s_MD)) % 0.41/0.81 (assume @p267 (tptp.s_contains tptp.s_g151 tptp.s_PL)) % 0.41/0.81 (assume @p268 (tptp.s_contains tptp.s_g151 tptp.s_RO)) % 0.41/0.81 (assume @p269 (tptp.s_contains tptp.s_g151 tptp.s_RU)) % 0.41/0.81 (assume @p270 (tptp.s_contains tptp.s_g151 tptp.s_SU)) % 0.41/0.81 (assume @p271 (tptp.s_contains tptp.s_g151 tptp.s_SK)) % 0.41/0.81 (assume @p272 (tptp.s_contains tptp.s_g151 tptp.s_UA)) % 0.41/0.81 (assume @p273 (tptp.s_partOf tptp.s_g154 tptp.s_g150)) % 0.41/0.81 (assume @p274 (tptp.s_contains tptp.s_g154 tptp.s_GG)) % 0.41/0.81 (assume @p275 (tptp.s_contains tptp.s_g154 tptp.s_IM)) % 0.41/0.81 (assume @p276 (tptp.s_contains tptp.s_g154 tptp.s_JE)) % 0.41/0.81 (assume @p277 (tptp.s_contains tptp.s_g154 tptp.s_AX)) % 0.41/0.81 (assume @p278 (tptp.s_contains tptp.s_g154 tptp.s_DK)) % 0.41/0.81 (assume @p279 (tptp.s_contains tptp.s_g154 tptp.s_EE)) % 0.41/0.81 (assume @p280 (tptp.s_contains tptp.s_g154 tptp.s_FI)) % 0.41/0.81 (assume @p281 (tptp.s_contains tptp.s_g154 tptp.s_FO)) % 0.41/0.81 (assume @p282 (tptp.s_contains tptp.s_g154 tptp.s_GB)) % 0.41/0.81 (assume @p283 (tptp.s_contains tptp.s_g154 tptp.s_IE)) % 0.41/0.81 (assume @p284 (tptp.s_contains tptp.s_g154 tptp.s_IS)) % 0.41/0.81 (assume @p285 (tptp.s_contains tptp.s_g154 tptp.s_LT)) % 0.41/0.81 (assume @p286 (tptp.s_contains tptp.s_g154 tptp.s_LV)) % 0.41/0.81 (assume @p287 (tptp.s_contains tptp.s_g154 tptp.s_NO)) % 0.41/0.81 (assume @p288 (tptp.s_contains tptp.s_g154 tptp.s_SE)) % 0.41/0.81 (assume @p289 (tptp.s_contains tptp.s_g154 tptp.s_SJ)) % 0.41/0.81 (assume @p290 (tptp.s_partOf tptp.s_g155 tptp.s_g150)) % 0.41/0.81 (assume @p291 (tptp.s_contains tptp.s_g155 tptp.s_AT)) % 0.41/0.81 (assume @p292 (tptp.s_contains tptp.s_g155 tptp.s_BE)) % 0.41/0.81 (assume @p293 (tptp.s_contains tptp.s_g155 tptp.s_CH)) % 0.41/0.81 (assume @p294 (tptp.s_contains tptp.s_g155 tptp.s_DE)) % 0.41/0.81 (assume @p295 (tptp.s_contains tptp.s_g155 tptp.s_DD)) % 0.41/0.81 (assume @p296 (tptp.s_contains tptp.s_g155 tptp.s_FR)) % 0.41/0.81 (assume @p297 (tptp.s_contains tptp.s_g155 tptp.s_FX)) % 0.41/0.81 (assume @p298 (tptp.s_contains tptp.s_g155 tptp.s_LI)) % 0.41/0.81 (assume @p299 (tptp.s_contains tptp.s_g155 tptp.s_LU)) % 0.41/0.81 (assume @p300 (tptp.s_contains tptp.s_g155 tptp.s_MC)) % 0.41/0.81 (assume @p301 (tptp.s_contains tptp.s_g155 tptp.s_NL)) % 0.41/0.81 (assume @p302 (tptp.s_partOf tptp.s_BG tptp.s_g151)) % 0.41/0.81 (assume @p303 (tptp.s_partOf tptp.s_BY tptp.s_g151)) % 0.41/0.81 (assume @p304 (tptp.s_partOf tptp.s_BY tptp.s_g172)) % 0.41/0.81 (assume @p305 (tptp.s_partOf tptp.s_CZ tptp.s_g151)) % 0.41/0.81 (assume @p306 (tptp.s_partOf tptp.s_HU tptp.s_g151)) % 0.41/0.81 (assume @p307 (tptp.s_partOf tptp.s_MD tptp.s_g151)) % 0.41/0.81 (assume @p308 (tptp.s_partOf tptp.s_MD tptp.s_g172)) % 0.41/0.81 (assume @p309 (tptp.s_partOf tptp.s_PL tptp.s_g151)) % 0.41/0.81 (assume @p310 (tptp.s_partOf tptp.s_RO tptp.s_g151)) % 0.41/0.81 (assume @p311 (tptp.s_partOf tptp.s_RU tptp.s_g151)) % 0.41/0.81 (assume @p312 (tptp.s_partOf tptp.s_RU tptp.s_g172)) % 0.41/0.81 (assume @p313 (tptp.s_partOf tptp.s_SU tptp.s_g151)) % 0.41/0.81 (assume @p314 (tptp.s_partOf tptp.s_SK tptp.s_g151)) % 0.41/0.81 (assume @p315 (tptp.s_partOf tptp.s_UA tptp.s_g151)) % 0.41/0.81 (assume @p316 (tptp.s_partOf tptp.s_UA tptp.s_g172)) % 0.41/0.81 (assume @p317 (tptp.s_partOf tptp.s_GG tptp.s_g154)) % 0.41/0.81 (assume @p318 (tptp.s_partOf tptp.s_GG tptp.s_g830)) % 0.41/0.81 (assume @p319 (tptp.s_partOf tptp.s_IM tptp.s_g154)) % 0.41/0.81 (assume @p320 (tptp.s_partOf tptp.s_JE tptp.s_g154)) % 0.41/0.81 (assume @p321 (tptp.s_partOf tptp.s_JE tptp.s_g830)) % 0.41/0.81 (assume @p322 (tptp.s_partOf tptp.s_AX tptp.s_g154)) % 0.41/0.81 (assume @p323 (tptp.s_partOf tptp.s_DK tptp.s_g154)) % 0.41/0.81 (assume @p324 (tptp.s_partOf tptp.s_EE tptp.s_g154)) % 0.41/0.81 (assume @p325 (tptp.s_partOf tptp.s_FI tptp.s_g154)) % 0.41/0.81 (assume @p326 (tptp.s_partOf tptp.s_FO tptp.s_g154)) % 0.41/0.81 (assume @p327 (tptp.s_partOf tptp.s_GB tptp.s_g154)) % 0.41/0.81 (assume @p328 (tptp.s_partOf tptp.s_IE tptp.s_g154)) % 0.41/0.81 (assume @p329 (tptp.s_partOf tptp.s_IS tptp.s_g154)) % 0.41/0.81 (assume @p330 (tptp.s_partOf tptp.s_LT tptp.s_g154)) % 0.41/0.81 (assume @p331 (tptp.s_partOf tptp.s_LV tptp.s_g154)) % 0.41/0.81 (assume @p332 (tptp.s_partOf tptp.s_NO tptp.s_g154)) % 0.41/0.81 (assume @p333 (tptp.s_partOf tptp.s_SE tptp.s_g154)) % 0.41/0.81 (assume @p334 (tptp.s_partOf tptp.s_SJ tptp.s_g154)) % 0.41/0.81 (assume @p335 (tptp.s_contains tptp.s_g830 tptp.s_GG)) % 0.41/0.81 (assume @p336 (tptp.s_contains tptp.s_g830 tptp.s_JE)) % 0.41/0.81 (assume @p337 (tptp.s_partOf tptp.s_AT tptp.s_g155)) % 0.41/0.81 (assume @p338 (tptp.s_partOf tptp.s_BE tptp.s_g155)) % 0.41/0.81 (assume @p339 (tptp.s_partOf tptp.s_CH tptp.s_g155)) % 0.41/0.81 (assume @p340 (tptp.s_partOf tptp.s_DE tptp.s_g155)) % 0.41/0.81 (assume @p341 (tptp.s_partOf tptp.s_DD tptp.s_g155)) % 0.41/0.81 (assume @p342 (tptp.s_partOf tptp.s_FR tptp.s_g155)) % 0.41/0.81 (assume @p343 (tptp.s_partOf tptp.s_FX tptp.s_g155)) % 0.41/0.81 (assume @p344 (tptp.s_partOf tptp.s_LI tptp.s_g155)) % 0.41/0.81 (assume @p345 (tptp.s_partOf tptp.s_LU tptp.s_g155)) % 0.41/0.81 (assume @p346 (tptp.s_partOf tptp.s_MC tptp.s_g155)) % 0.41/0.81 (assume @p347 (tptp.s_partOf tptp.s_NL tptp.s_g155)) % 0.41/0.81 (assume @p348 (tptp.s_contains tptp.s_g017 tptp.s_AO)) % 0.41/0.81 (assume @p349 (tptp.s_contains tptp.s_g017 tptp.s_CD)) % 0.41/0.81 (assume @p350 (tptp.s_contains tptp.s_g017 tptp.s_ZR)) % 0.41/0.81 (assume @p351 (tptp.s_contains tptp.s_g017 tptp.s_CF)) % 0.41/0.81 (assume @p352 (tptp.s_contains tptp.s_g017 tptp.s_CG)) % 0.41/0.81 (assume @p353 (tptp.s_contains tptp.s_g017 tptp.s_CM)) % 0.41/0.81 (assume @p354 (tptp.s_contains tptp.s_g017 tptp.s_GA)) % 0.41/0.81 (assume @p355 (tptp.s_contains tptp.s_g017 tptp.s_GQ)) % 0.41/0.81 (assume @p356 (tptp.s_contains tptp.s_g017 tptp.s_ST)) % 0.41/0.81 (assume @p357 (tptp.s_contains tptp.s_g017 tptp.s_TD)) % 0.41/0.81 (assume @p358 (tptp.s_partOf tptp.s_g017 tptp.s_g002)) % 0.41/0.81 (assume @p359 (tptp.s_partOf tptp.s_AO tptp.s_g017)) % 0.41/0.81 (assume @p360 (tptp.s_partOf tptp.s_CD tptp.s_g017)) % 0.41/0.81 (assume @p361 (tptp.s_partOf tptp.s_ZR tptp.s_g017)) % 0.41/0.81 (assume @p362 (tptp.s_partOf tptp.s_CF tptp.s_g017)) % 0.41/0.81 (assume @p363 (tptp.s_partOf tptp.s_CG tptp.s_g017)) % 0.41/0.81 (assume @p364 (tptp.s_partOf tptp.s_CM tptp.s_g017)) % 0.41/0.81 (assume @p365 (tptp.s_partOf tptp.s_GA tptp.s_g017)) % 0.41/0.81 (assume @p366 (tptp.s_partOf tptp.s_GQ tptp.s_g017)) % 0.41/0.81 (assume @p367 (tptp.s_partOf tptp.s_ST tptp.s_g017)) % 0.41/0.81 (assume @p368 (tptp.s_partOf tptp.s_TD tptp.s_g017)) % 0.41/0.81 (assume @p369 (tptp.s_contains tptp.s_g172 tptp.s_AM)) % 0.41/0.81 (assume @p370 (tptp.s_contains tptp.s_g172 tptp.s_AZ)) % 0.41/0.81 (assume @p371 (tptp.s_contains tptp.s_g172 tptp.s_BY)) % 0.41/0.81 (assume @p372 (tptp.s_contains tptp.s_g172 tptp.s_GE)) % 0.41/0.81 (assume @p373 (tptp.s_contains tptp.s_g172 tptp.s_KG)) % 0.41/0.81 (assume @p374 (tptp.s_contains tptp.s_g172 tptp.s_KZ)) % 0.41/0.81 (assume @p375 (tptp.s_contains tptp.s_g172 tptp.s_MD)) % 0.41/0.81 (assume @p376 (tptp.s_contains tptp.s_g172 tptp.s_RU)) % 0.41/0.81 (assume @p377 (tptp.s_contains tptp.s_g172 tptp.s_TJ)) % 0.41/0.81 (assume @p378 (tptp.s_contains tptp.s_g172 tptp.s_TM)) % 0.41/0.81 (assume @p379 (tptp.s_contains tptp.s_g172 tptp.s_UA)) % 0.41/0.81 (assume @p380 (tptp.s_contains tptp.s_g172 tptp.s_UZ)) % 0.41/0.81 (assume @p381 (tptp.s_contains tptp.s_g018 tptp.s_BW)) % 0.41/0.81 (assume @p382 (tptp.s_contains tptp.s_g018 tptp.s_LS)) % 0.41/0.81 (assume @p383 (tptp.s_contains tptp.s_g018 tptp.s_NA)) % 0.41/0.81 (assume @p384 (tptp.s_contains tptp.s_g018 tptp.s_SZ)) % 0.41/0.81 (assume @p385 (tptp.s_contains tptp.s_g018 tptp.s_ZA)) % 0.41/0.81 (assume @p386 (tptp.s_partOf tptp.s_g018 tptp.s_g002)) % 0.41/0.81 (assume @p387 (tptp.s_partOf tptp.s_BW tptp.s_g018)) % 0.41/0.81 (assume @p388 (tptp.s_partOf tptp.s_LS tptp.s_g018)) % 0.41/0.81 (assume @p389 (tptp.s_partOf tptp.s_NA tptp.s_g018)) % 0.41/0.81 (assume @p390 (tptp.s_partOf tptp.s_SZ tptp.s_g018)) % 0.41/0.81 (assume @p391 (tptp.s_partOf tptp.s_ZA tptp.s_g018)) % 0.41/0.81 (assume @p392 (tptp.s_partOf tptp.s_g005 tptp.s_g019)) % 0.41/0.81 (assume @p393 (tptp.s_partOf tptp.s_g005 tptp.s_g419)) % 0.41/0.81 (assume @p394 (tptp.s_contains tptp.s_g005 tptp.s_AR)) % 0.41/0.81 (assume @p395 (tptp.s_contains tptp.s_g005 tptp.s_BO)) % 0.41/0.81 (assume @p396 (tptp.s_contains tptp.s_g005 tptp.s_BR)) % 0.41/0.81 (assume @p397 (tptp.s_contains tptp.s_g005 tptp.s_CL)) % 0.41/0.81 (assume @p398 (tptp.s_contains tptp.s_g005 tptp.s_CO)) % 0.41/0.81 (assume @p399 (tptp.s_contains tptp.s_g005 tptp.s_EC)) % 0.41/0.81 (assume @p400 (tptp.s_contains tptp.s_g005 tptp.s_FK)) % 0.41/0.81 (assume @p401 (tptp.s_contains tptp.s_g005 tptp.s_GF)) % 0.41/0.81 (assume @p402 (tptp.s_contains tptp.s_g005 tptp.s_GY)) % 0.41/0.81 (assume @p403 (tptp.s_contains tptp.s_g005 tptp.s_PE)) % 0.41/0.81 (assume @p404 (tptp.s_contains tptp.s_g005 tptp.s_PY)) % 0.41/0.81 (assume @p405 (tptp.s_contains tptp.s_g005 tptp.s_SR)) % 0.41/0.81 (assume @p406 (tptp.s_contains tptp.s_g005 tptp.s_UY)) % 0.41/0.81 (assume @p407 (tptp.s_contains tptp.s_g005 tptp.s_VE)) % 0.41/0.81 (assume @p408 (tptp.s_partOf tptp.s_g021 tptp.s_g019)) % 0.41/0.81 (assume @p409 (tptp.s_contains tptp.s_g021 tptp.s_BM)) % 0.41/0.81 (assume @p410 (tptp.s_contains tptp.s_g021 tptp.s_CA)) % 0.41/0.81 (assume @p411 (tptp.s_contains tptp.s_g021 tptp.s_GL)) % 0.41/0.81 (assume @p412 (tptp.s_contains tptp.s_g021 tptp.s_PM)) % 0.41/0.81 (assume @p413 (tptp.s_contains tptp.s_g021 tptp.s_US)) % 0.41/0.81 (assume @p414 (tptp.s_partOf tptp.s_g021 tptp.s_g003)) % 0.41/0.81 (assume @p415 (tptp.s_partOf tptp.s_g029 tptp.s_g019)) % 0.41/0.81 (assume @p416 (tptp.s_contains tptp.s_g029 tptp.s_AG)) % 0.41/0.81 (assume @p417 (tptp.s_contains tptp.s_g029 tptp.s_AI)) % 0.41/0.81 (assume @p418 (tptp.s_contains tptp.s_g029 tptp.s_AN)) % 0.41/0.81 (assume @p419 (tptp.s_contains tptp.s_g029 tptp.s_AW)) % 0.41/0.81 (assume @p420 (tptp.s_contains tptp.s_g029 tptp.s_BB)) % 0.41/0.81 (assume @p421 (tptp.s_contains tptp.s_g029 tptp.s_BL)) % 0.41/0.81 (assume @p422 (tptp.s_contains tptp.s_g029 tptp.s_BS)) % 0.41/0.81 (assume @p423 (tptp.s_contains tptp.s_g029 tptp.s_CU)) % 0.41/0.81 (assume @p424 (tptp.s_contains tptp.s_g029 tptp.s_DM)) % 0.41/0.81 (assume @p425 (tptp.s_contains tptp.s_g029 tptp.s_DO)) % 0.41/0.81 (assume @p426 (tptp.s_contains tptp.s_g029 tptp.s_GD)) % 0.41/0.81 (assume @p427 (tptp.s_contains tptp.s_g029 tptp.s_GP)) % 0.41/0.81 (assume @p428 (tptp.s_contains tptp.s_g029 tptp.s_HT)) % 0.41/0.81 (assume @p429 (tptp.s_contains tptp.s_g029 tptp.s_JM)) % 0.41/0.81 (assume @p430 (tptp.s_contains tptp.s_g029 tptp.s_KN)) % 0.41/0.81 (assume @p431 (tptp.s_contains tptp.s_g029 tptp.s_KY)) % 0.41/0.81 (assume @p432 (tptp.s_contains tptp.s_g029 tptp.s_LC)) % 0.41/0.81 (assume @p433 (tptp.s_contains tptp.s_g029 tptp.s_MF)) % 0.41/0.81 (assume @p434 (tptp.s_contains tptp.s_g029 tptp.s_MQ)) % 0.41/0.81 (assume @p435 (tptp.s_contains tptp.s_g029 tptp.s_MS)) % 0.41/0.81 (assume @p436 (tptp.s_contains tptp.s_g029 tptp.s_PR)) % 0.41/0.81 (assume @p437 (tptp.s_contains tptp.s_g029 tptp.s_TC)) % 0.41/0.81 (assume @p438 (tptp.s_contains tptp.s_g029 tptp.s_TT)) % 0.41/0.81 (assume @p439 (tptp.s_contains tptp.s_g029 tptp.s_VC)) % 0.41/0.81 (assume @p440 (tptp.s_contains tptp.s_g029 tptp.s_VG)) % 0.41/0.81 (assume @p441 (tptp.s_contains tptp.s_g029 tptp.s_VI)) % 0.41/0.81 (assume @p442 (tptp.s_partOf tptp.s_g029 tptp.s_g003)) % 0.41/0.81 (assume @p443 (tptp.s_partOf tptp.s_g029 tptp.s_g419)) % 0.41/0.81 (assume @p444 (tptp.s_partOf tptp.s_g003 tptp.s_g019)) % 0.41/0.81 (assume @p445 (tptp.s_contains tptp.s_g003 tptp.s_g013)) % 0.41/0.81 (assume @p446 (tptp.s_contains tptp.s_g003 tptp.s_g021)) % 0.41/0.81 (assume @p447 (tptp.s_contains tptp.s_g003 tptp.s_g029)) % 0.41/0.81 (assume @p448 (tptp.s_partOf tptp.s_g419 tptp.s_g019)) % 0.41/0.81 (assume @p449 (tptp.s_contains tptp.s_g419 tptp.s_g005)) % 0.41/0.81 (assume @p450 (tptp.s_contains tptp.s_g419 tptp.s_g013)) % 0.41/0.81 (assume @p451 (tptp.s_contains tptp.s_g419 tptp.s_g029)) % 0.41/0.81 (assume @p452 (tptp.s_partOf tptp.s_BM tptp.s_g021)) % 0.41/0.81 (assume @p453 (tptp.s_partOf tptp.s_CA tptp.s_g021)) % 0.41/0.81 (assume @p454 (tptp.s_partOf tptp.s_GL tptp.s_g021)) % 0.41/0.81 (assume @p455 (tptp.s_partOf tptp.s_PM tptp.s_g021)) % 0.41/0.81 (assume @p456 (tptp.s_partOf tptp.s_US tptp.s_g021)) % 0.41/0.81 (assume @p457 (tptp.s_partOf tptp.s_AG tptp.s_g029)) % 0.41/0.81 (assume @p458 (tptp.s_partOf tptp.s_AI tptp.s_g029)) % 0.41/0.81 (assume @p459 (tptp.s_partOf tptp.s_AN tptp.s_g029)) % 0.41/0.81 (assume @p460 (tptp.s_partOf tptp.s_AW tptp.s_g029)) % 0.41/0.81 (assume @p461 (tptp.s_partOf tptp.s_BB tptp.s_g029)) % 0.41/0.81 (assume @p462 (tptp.s_partOf tptp.s_BL tptp.s_g029)) % 0.41/0.81 (assume @p463 (tptp.s_partOf tptp.s_BS tptp.s_g029)) % 0.41/0.81 (assume @p464 (tptp.s_partOf tptp.s_CU tptp.s_g029)) % 0.41/0.81 (assume @p465 (tptp.s_partOf tptp.s_DM tptp.s_g029)) % 0.41/0.81 (assume @p466 (tptp.s_partOf tptp.s_DO tptp.s_g029)) % 0.41/0.81 (assume @p467 (tptp.s_partOf tptp.s_GD tptp.s_g029)) % 0.41/0.81 (assume @p468 (tptp.s_partOf tptp.s_GP tptp.s_g029)) % 0.41/0.81 (assume @p469 (tptp.s_partOf tptp.s_HT tptp.s_g029)) % 0.41/0.81 (assume @p470 (tptp.s_partOf tptp.s_JM tptp.s_g029)) % 0.41/0.81 (assume @p471 (tptp.s_partOf tptp.s_KN tptp.s_g029)) % 0.41/0.81 (assume @p472 (tptp.s_partOf tptp.s_KY tptp.s_g029)) % 0.41/0.81 (assume @p473 (tptp.s_partOf tptp.s_LC tptp.s_g029)) % 0.41/0.81 (assume @p474 (tptp.s_partOf tptp.s_MF tptp.s_g029)) % 0.41/0.81 (assume @p475 (tptp.s_partOf tptp.s_MQ tptp.s_g029)) % 0.41/0.81 (assume @p476 (tptp.s_partOf tptp.s_MS tptp.s_g029)) % 0.41/0.81 (assume @p477 (tptp.s_partOf tptp.s_PR tptp.s_g029)) % 0.41/0.81 (assume @p478 (tptp.s_partOf tptp.s_TC tptp.s_g029)) % 0.41/0.81 (assume @p479 (tptp.s_partOf tptp.s_TT tptp.s_g029)) % 0.41/0.81 (assume @p480 (tptp.s_partOf tptp.s_VC tptp.s_g029)) % 0.41/0.81 (assume @p481 (tptp.s_partOf tptp.s_VG tptp.s_g029)) % 0.41/0.81 (assume @p482 (tptp.s_partOf tptp.s_VI tptp.s_g029)) % 0.41/0.81 (assume @p483 (tptp.s_partOf tptp.s_CN tptp.s_g030)) % 0.41/0.81 (assume @p484 (tptp.s_partOf tptp.s_HK tptp.s_g030)) % 0.41/0.81 (assume @p485 (tptp.s_partOf tptp.s_JP tptp.s_g030)) % 0.41/0.81 (assume @p486 (tptp.s_partOf tptp.s_KP tptp.s_g030)) % 0.41/0.81 (assume @p487 (tptp.s_partOf tptp.s_KR tptp.s_g030)) % 0.41/0.81 (assume @p488 (tptp.s_partOf tptp.s_MN tptp.s_g030)) % 0.41/0.81 (assume @p489 (tptp.s_partOf tptp.s_MO tptp.s_g030)) % 0.41/0.81 (assume @p490 (tptp.s_partOf tptp.s_TW tptp.s_g030)) % 0.41/0.81 (assume @p491 (tptp.s_partOf tptp.s_BN tptp.s_g035)) % 0.41/0.81 (assume @p492 (tptp.s_partOf tptp.s_ID tptp.s_g035)) % 0.41/0.81 (assume @p493 (tptp.s_partOf tptp.s_KH tptp.s_g035)) % 0.41/0.81 (assume @p494 (tptp.s_partOf tptp.s_LA tptp.s_g035)) % 0.41/0.81 (assume @p495 (tptp.s_partOf tptp.s_MM tptp.s_g035)) % 0.41/0.81 (assume @p496 (tptp.s_partOf tptp.s_BU tptp.s_g035)) % 0.41/0.81 (assume @p497 (tptp.s_partOf tptp.s_MY tptp.s_g035)) % 0.41/0.81 (assume @p498 (tptp.s_partOf tptp.s_PH tptp.s_g035)) % 0.41/0.81 (assume @p499 (tptp.s_partOf tptp.s_SG tptp.s_g035)) % 0.41/0.81 (assume @p500 (tptp.s_partOf tptp.s_TH tptp.s_g035)) % 0.41/0.81 (assume @p501 (tptp.s_partOf tptp.s_TL tptp.s_g035)) % 0.41/0.81 (assume @p502 (tptp.s_partOf tptp.s_TP tptp.s_g035)) % 0.41/0.81 (assume @p503 (tptp.s_partOf tptp.s_VN tptp.s_g035)) % 0.41/0.81 (assume @p504 (tptp.s_partOf tptp.s_AD tptp.s_g039)) % 0.41/0.81 (assume @p505 (tptp.s_partOf tptp.s_AL tptp.s_g039)) % 0.41/0.81 (assume @p506 (tptp.s_partOf tptp.s_BA tptp.s_g039)) % 0.41/0.81 (assume @p507 (tptp.s_partOf tptp.s_ES tptp.s_g039)) % 0.41/0.81 (assume @p508 (tptp.s_partOf tptp.s_GI tptp.s_g039)) % 0.41/0.81 (assume @p509 (tptp.s_partOf tptp.s_GR tptp.s_g039)) % 0.41/0.81 (assume @p510 (tptp.s_partOf tptp.s_HR tptp.s_g039)) % 0.41/0.81 (assume @p511 (tptp.s_partOf tptp.s_IT tptp.s_g039)) % 0.41/0.81 (assume @p512 (tptp.s_partOf tptp.s_ME tptp.s_g039)) % 0.41/0.81 (assume @p513 (tptp.s_partOf tptp.s_MK tptp.s_g039)) % 0.41/0.81 (assume @p514 (tptp.s_partOf tptp.s_MT tptp.s_g039)) % 0.41/0.81 (assume @p515 (tptp.s_partOf tptp.s_CS tptp.s_g039)) % 0.41/0.81 (assume @p516 (tptp.s_partOf tptp.s_RS tptp.s_g039)) % 0.41/0.81 (assume @p517 (tptp.s_partOf tptp.s_PT tptp.s_g039)) % 0.41/0.81 (assume @p518 (tptp.s_partOf tptp.s_SI tptp.s_g039)) % 0.41/0.81 (assume @p519 (tptp.s_partOf tptp.s_SM tptp.s_g039)) % 0.41/0.81 (assume @p520 (tptp.s_partOf tptp.s_VA tptp.s_g039)) % 0.41/0.81 (assume @p521 (tptp.s_partOf tptp.s_YU tptp.s_g039)) % 0.41/0.81 (assume @p522 (tptp.s_partOf tptp.s_AR tptp.s_g005)) % 0.41/0.81 (assume @p523 (tptp.s_partOf tptp.s_BO tptp.s_g005)) % 0.41/0.81 (assume @p524 (tptp.s_partOf tptp.s_BR tptp.s_g005)) % 0.41/0.81 (assume @p525 (tptp.s_partOf tptp.s_CL tptp.s_g005)) % 0.41/0.81 (assume @p526 (tptp.s_partOf tptp.s_CO tptp.s_g005)) % 0.41/0.81 (assume @p527 (tptp.s_partOf tptp.s_EC tptp.s_g005)) % 0.41/0.81 (assume @p528 (tptp.s_partOf tptp.s_FK tptp.s_g005)) % 0.41/0.81 (assume @p529 (tptp.s_partOf tptp.s_GF tptp.s_g005)) % 0.41/0.81 (assume @p530 (tptp.s_partOf tptp.s_GY tptp.s_g005)) % 0.41/0.81 (assume @p531 (tptp.s_partOf tptp.s_PE tptp.s_g005)) % 0.41/0.81 (assume @p532 (tptp.s_partOf tptp.s_PY tptp.s_g005)) % 0.41/0.81 (assume @p533 (tptp.s_partOf tptp.s_SR tptp.s_g005)) % 0.41/0.81 (assume @p534 (tptp.s_partOf tptp.s_UY tptp.s_g005)) % 0.41/0.81 (assume @p535 (tptp.s_partOf tptp.s_VE tptp.s_g005)) % 0.41/0.81 (assume @p536 (tptp.s_contains tptp.s_g053 tptp.s_AU)) % 0.41/0.81 (assume @p537 (tptp.s_contains tptp.s_g053 tptp.s_NF)) % 0.41/0.81 (assume @p538 (tptp.s_contains tptp.s_g053 tptp.s_NZ)) % 0.41/0.81 (assume @p539 (tptp.s_partOf tptp.s_g053 tptp.s_g009)) % 0.41/0.81 (assume @p540 (tptp.s_partOf tptp.s_AU tptp.s_g053)) % 0.41/0.81 (assume @p541 (tptp.s_partOf tptp.s_NF tptp.s_g053)) % 0.41/0.81 (assume @p542 (tptp.s_partOf tptp.s_NZ tptp.s_g053)) % 0.41/0.81 (assume @p543 (tptp.s_contains tptp.s_g054 tptp.s_FJ)) % 0.41/0.81 (assume @p544 (tptp.s_contains tptp.s_g054 tptp.s_NC)) % 0.41/0.81 (assume @p545 (tptp.s_contains tptp.s_g054 tptp.s_PG)) % 0.41/0.81 (assume @p546 (tptp.s_contains tptp.s_g054 tptp.s_SB)) % 0.41/0.81 (assume @p547 (tptp.s_contains tptp.s_g054 tptp.s_VU)) % 0.41/0.81 (assume @p548 (tptp.s_partOf tptp.s_g054 tptp.s_g009)) % 0.41/0.81 (assume @p549 (tptp.s_partOf tptp.s_FJ tptp.s_g054)) % 0.41/0.81 (assume @p550 (tptp.s_partOf tptp.s_NC tptp.s_g054)) % 0.41/0.81 (assume @p551 (tptp.s_partOf tptp.s_PG tptp.s_g054)) % 0.41/0.81 (assume @p552 (tptp.s_partOf tptp.s_SB tptp.s_g054)) % 0.41/0.81 (assume @p553 (tptp.s_partOf tptp.s_VU tptp.s_g054)) % 0.41/0.81 (assume @p554 (tptp.s_contains tptp.s_g057 tptp.s_FM)) % 0.41/0.81 (assume @p555 (tptp.s_contains tptp.s_g057 tptp.s_GU)) % 0.41/0.81 (assume @p556 (tptp.s_contains tptp.s_g057 tptp.s_KI)) % 0.41/0.81 (assume @p557 (tptp.s_contains tptp.s_g057 tptp.s_MH)) % 0.41/0.81 (assume @p558 (tptp.s_contains tptp.s_g057 tptp.s_MP)) % 0.41/0.81 (assume @p559 (tptp.s_contains tptp.s_g057 tptp.s_NR)) % 0.41/0.81 (assume @p560 (tptp.s_contains tptp.s_g057 tptp.s_PW)) % 0.41/0.81 (assume @p561 (tptp.s_partOf tptp.s_g057 tptp.s_g009)) % 0.41/0.81 (assume @p562 (tptp.s_partOf tptp.s_FM tptp.s_g057)) % 0.41/0.81 (assume @p563 (tptp.s_partOf tptp.s_GU tptp.s_g057)) % 0.41/0.81 (assume @p564 (tptp.s_partOf tptp.s_KI tptp.s_g057)) % 0.41/0.81 (assume @p565 (tptp.s_partOf tptp.s_MH tptp.s_g057)) % 0.41/0.81 (assume @p566 (tptp.s_partOf tptp.s_MP tptp.s_g057)) % 0.41/0.81 (assume @p567 (tptp.s_partOf tptp.s_NR tptp.s_g057)) % 0.41/0.81 (assume @p568 (tptp.s_partOf tptp.s_PW tptp.s_g057)) % 0.41/0.81 (assume @p569 (tptp.s_contains tptp.s_g061 tptp.s_AS)) % 0.41/0.81 (assume @p570 (tptp.s_contains tptp.s_g061 tptp.s_CK)) % 0.41/0.81 (assume @p571 (tptp.s_contains tptp.s_g061 tptp.s_NU)) % 0.41/0.81 (assume @p572 (tptp.s_contains tptp.s_g061 tptp.s_PF)) % 0.41/0.81 (assume @p573 (tptp.s_contains tptp.s_g061 tptp.s_PN)) % 0.41/0.81 (assume @p574 (tptp.s_contains tptp.s_g061 tptp.s_TK)) % 0.41/0.81 (assume @p575 (tptp.s_contains tptp.s_g061 tptp.s_TO)) % 0.41/0.81 (assume @p576 (tptp.s_contains tptp.s_g061 tptp.s_TV)) % 0.41/0.81 (assume @p577 (tptp.s_contains tptp.s_g061 tptp.s_WF)) % 0.41/0.81 (assume @p578 (tptp.s_contains tptp.s_g061 tptp.s_WS)) % 0.41/0.81 (assume @p579 (tptp.s_partOf tptp.s_g061 tptp.s_g009)) % 0.41/0.81 (assume @p580 (tptp.s_partOf tptp.s_AS tptp.s_g061)) % 0.41/0.81 (assume @p581 (tptp.s_partOf tptp.s_CK tptp.s_g061)) % 0.41/0.81 (assume @p582 (tptp.s_partOf tptp.s_NU tptp.s_g061)) % 0.41/0.81 (assume @p583 (tptp.s_partOf tptp.s_PF tptp.s_g061)) % 0.41/0.81 (assume @p584 (tptp.s_partOf tptp.s_PN tptp.s_g061)) % 0.41/0.81 (assume @p585 (tptp.s_partOf tptp.s_TK tptp.s_g061)) % 0.41/0.81 (assume @p586 (tptp.s_partOf tptp.s_TO tptp.s_g061)) % 0.41/0.81 (assume @p587 (tptp.s_partOf tptp.s_TV tptp.s_g061)) % 0.41/0.81 (assume @p588 (tptp.s_partOf tptp.s_WF tptp.s_g061)) % 0.41/0.81 (assume @p589 (tptp.s_partOf tptp.s_WS tptp.s_g061)) % 0.41/0.81 (assume @p590 (tptp.s_partOf tptp.s_AF tptp.s_g034)) % 0.41/0.81 (assume @p591 (tptp.s_partOf tptp.s_BD tptp.s_g034)) % 0.41/0.81 (assume @p592 (tptp.s_partOf tptp.s_BT tptp.s_g034)) % 0.41/0.81 (assume @p593 (tptp.s_partOf tptp.s_IN tptp.s_g034)) % 0.41/0.81 (assume @p594 (tptp.s_partOf tptp.s_IR tptp.s_g034)) % 0.41/0.81 (assume @p595 (tptp.s_partOf tptp.s_LK tptp.s_g034)) % 0.41/0.81 (assume @p596 (tptp.s_partOf tptp.s_MV tptp.s_g034)) % 0.41/0.81 (assume @p597 (tptp.s_partOf tptp.s_NP tptp.s_g034)) % 0.41/0.81 (assume @p598 (tptp.s_partOf tptp.s_PK tptp.s_g034)) % 0.41/0.81 (assume @p599 @t11) % 0.41/0.81 (assume @p600 (forall @t12 (=> (tptp.s_partOf @t4 @t6) (tptp.s_contains @t6 @t4)))) % 0.41/0.81 (assume @p601 (forall @t12 (=> @t8 (tptp.s_partOf @t6 @t4)))) % 0.41/0.81 (assume @p602 (not @t13)) % 0.41/0.81 (assume @p603 true) % 0.41/0.81 (step @p604 :rule aci_norm :args ((= (or (or @t15 @t14) @t5) @t16))) % 0.41/0.81 (step @p605 :rule refl :args (@t5)) % 0.41/0.81 (step @p606 :rule bool-and-de-morgan :args (@t8 @t7 true)) % 0.41/0.81 (step @p607 :rule nary_cong :premises (@p606 @p605) :args ((or (not @t9) @t5))) % 0.41/0.81 (step @p608 :rule trans :premises (@p607 @p604)) % 0.41/0.81 (step @p609 :rule bool-impl-elim :args (@t9 @t5)) % 0.41/0.81 (step @p610 :rule trans :premises (@p609 @p608)) % 0.41/0.81 (step @p611 :rule cong :premises (@p610) :args (@t11)) % 0.41/0.81 (step @p612 :rule eq_resolve :premises (@p599 @p611)) % 0.41/0.81 (step @p613 :rule cnf_or_pos :args (@t19)) % 0.41/0.81 (step @p614 :rule reordering :premises (@p613) :args ((or @t13 @t18 @t17 @t20))) % 0.41/0.81 (step @p615 :rule chain_m_resolution :premises (@p614 @p602 @p19 @p75) :args (@t20 (@list true false false) (@list @t13 @t1 @t2))) % 0.41/0.81 (assume-push @p622 @t21) % 0.41/0.81 (step @p617 :rule instantiate :premises (@p612) :args ((@list tptp.s_g019 tptp.s_g013 tptp.s_MX))) % 0.41/0.81 (step-pop @p623 :rule scope :premises (@p617)) % 0.41/0.81 (step @p618 :rule process_scope :premises (@p623) :args (@t19)) % 0.41/0.81 (step @p620 :rule implies_elim :premises (@p618)) % 0.41/0.81 (step @p621 false :rule chain_m_resolution :premises (@p620 @p615 @p612) :args (false (@list true false) (@list @t19 @t21))) % 0.41/0.81 ) % 0.41/0.81 % SZS output end Proof % 0.41/0.81 % cvc5 exiting %------------------------------------------------------------------------------