%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : MSC019+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 7 10:31:57 AM UTC 2026
% Result : Theorem 0.70s 0.30s
% Output : CNFRefutation 0.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 12
% Syntax : Number of formulae : 61 ( 48 unt; 0 typ; 0 def)
% Number of atoms : 225 ( 61 equ; 0 cnn)
% Maximal formula atoms : 3 ( 3 avg)
% Number of connectives : 282 ( 38 ~; 30 |; 3 &; 202 @)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 285 ( 282 usr; 282 con; 0-2 aty)
% Number of variables : 71 ( 0 ^; 71 !; 0 ?; 71 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_s_AD,type,
s_AD: $i ).
thf(tp_s_AE,type,
s_AE: $i ).
thf(tp_s_AF,type,
s_AF: $i ).
thf(tp_s_AG,type,
s_AG: $i ).
thf(tp_s_AI,type,
s_AI: $i ).
thf(tp_s_AL,type,
s_AL: $i ).
thf(tp_s_AM,type,
s_AM: $i ).
thf(tp_s_AN,type,
s_AN: $i ).
thf(tp_s_AO,type,
s_AO: $i ).
thf(tp_s_AR,type,
s_AR: $i ).
thf(tp_s_AS,type,
s_AS: $i ).
thf(tp_s_AT,type,
s_AT: $i ).
thf(tp_s_AU,type,
s_AU: $i ).
thf(tp_s_AW,type,
s_AW: $i ).
thf(tp_s_AX,type,
s_AX: $i ).
thf(tp_s_AZ,type,
s_AZ: $i ).
thf(tp_s_BA,type,
s_BA: $i ).
thf(tp_s_BB,type,
s_BB: $i ).
thf(tp_s_BD,type,
s_BD: $i ).
thf(tp_s_BE,type,
s_BE: $i ).
thf(tp_s_BF,type,
s_BF: $i ).
thf(tp_s_BG,type,
s_BG: $i ).
thf(tp_s_BH,type,
s_BH: $i ).
thf(tp_s_BI,type,
s_BI: $i ).
thf(tp_s_BJ,type,
s_BJ: $i ).
thf(tp_s_BL,type,
s_BL: $i ).
thf(tp_s_BM,type,
s_BM: $i ).
thf(tp_s_BN,type,
s_BN: $i ).
thf(tp_s_BO,type,
s_BO: $i ).
thf(tp_s_BR,type,
s_BR: $i ).
thf(tp_s_BS,type,
s_BS: $i ).
thf(tp_s_BT,type,
s_BT: $i ).
thf(tp_s_BU,type,
s_BU: $i ).
thf(tp_s_BW,type,
s_BW: $i ).
thf(tp_s_BY,type,
s_BY: $i ).
thf(tp_s_BZ,type,
s_BZ: $i ).
thf(tp_s_CA,type,
s_CA: $i ).
thf(tp_s_CD,type,
s_CD: $i ).
thf(tp_s_CF,type,
s_CF: $i ).
thf(tp_s_CG,type,
s_CG: $i ).
thf(tp_s_CH,type,
s_CH: $i ).
thf(tp_s_CI,type,
s_CI: $i ).
thf(tp_s_CK,type,
s_CK: $i ).
thf(tp_s_CL,type,
s_CL: $i ).
thf(tp_s_CM,type,
s_CM: $i ).
thf(tp_s_CN,type,
s_CN: $i ).
thf(tp_s_CO,type,
s_CO: $i ).
thf(tp_s_CR,type,
s_CR: $i ).
thf(tp_s_CS,type,
s_CS: $i ).
thf(tp_s_CU,type,
s_CU: $i ).
thf(tp_s_CV,type,
s_CV: $i ).
thf(tp_s_CY,type,
s_CY: $i ).
thf(tp_s_CZ,type,
s_CZ: $i ).
thf(tp_s_DD,type,
s_DD: $i ).
thf(tp_s_DE,type,
s_DE: $i ).
thf(tp_s_DJ,type,
s_DJ: $i ).
thf(tp_s_DK,type,
s_DK: $i ).
thf(tp_s_DM,type,
s_DM: $i ).
thf(tp_s_DO,type,
s_DO: $i ).
thf(tp_s_DZ,type,
s_DZ: $i ).
thf(tp_s_EC,type,
s_EC: $i ).
thf(tp_s_EE,type,
s_EE: $i ).
thf(tp_s_EG,type,
s_EG: $i ).
thf(tp_s_EH,type,
s_EH: $i ).
thf(tp_s_ER,type,
s_ER: $i ).
thf(tp_s_ES,type,
s_ES: $i ).
thf(tp_s_ET,type,
s_ET: $i ).
thf(tp_s_FI,type,
s_FI: $i ).
thf(tp_s_FJ,type,
s_FJ: $i ).
thf(tp_s_FK,type,
s_FK: $i ).
thf(tp_s_FM,type,
s_FM: $i ).
thf(tp_s_FO,type,
s_FO: $i ).
thf(tp_s_FR,type,
s_FR: $i ).
thf(tp_s_FX,type,
s_FX: $i ).
thf(tp_s_GA,type,
s_GA: $i ).
thf(tp_s_GB,type,
s_GB: $i ).
thf(tp_s_GD,type,
s_GD: $i ).
thf(tp_s_GE,type,
s_GE: $i ).
thf(tp_s_GF,type,
s_GF: $i ).
thf(tp_s_GG,type,
s_GG: $i ).
thf(tp_s_GH,type,
s_GH: $i ).
thf(tp_s_GI,type,
s_GI: $i ).
thf(tp_s_GL,type,
s_GL: $i ).
thf(tp_s_GM,type,
s_GM: $i ).
thf(tp_s_GN,type,
s_GN: $i ).
thf(tp_s_GP,type,
s_GP: $i ).
thf(tp_s_GQ,type,
s_GQ: $i ).
thf(tp_s_GR,type,
s_GR: $i ).
thf(tp_s_GT,type,
s_GT: $i ).
thf(tp_s_GU,type,
s_GU: $i ).
thf(tp_s_GW,type,
s_GW: $i ).
thf(tp_s_GY,type,
s_GY: $i ).
thf(tp_s_HK,type,
s_HK: $i ).
thf(tp_s_HN,type,
s_HN: $i ).
thf(tp_s_HR,type,
s_HR: $i ).
thf(tp_s_HT,type,
s_HT: $i ).
thf(tp_s_HU,type,
s_HU: $i ).
thf(tp_s_ID,type,
s_ID: $i ).
thf(tp_s_IE,type,
s_IE: $i ).
thf(tp_s_IL,type,
s_IL: $i ).
thf(tp_s_IM,type,
s_IM: $i ).
thf(tp_s_IN,type,
s_IN: $i ).
thf(tp_s_IQ,type,
s_IQ: $i ).
thf(tp_s_IR,type,
s_IR: $i ).
thf(tp_s_IS,type,
s_IS: $i ).
thf(tp_s_IT,type,
s_IT: $i ).
thf(tp_s_JE,type,
s_JE: $i ).
thf(tp_s_JM,type,
s_JM: $i ).
thf(tp_s_JO,type,
s_JO: $i ).
thf(tp_s_JP,type,
s_JP: $i ).
thf(tp_s_KE,type,
s_KE: $i ).
thf(tp_s_KG,type,
s_KG: $i ).
thf(tp_s_KH,type,
s_KH: $i ).
thf(tp_s_KI,type,
s_KI: $i ).
thf(tp_s_KM,type,
s_KM: $i ).
thf(tp_s_KN,type,
s_KN: $i ).
thf(tp_s_KP,type,
s_KP: $i ).
thf(tp_s_KR,type,
s_KR: $i ).
thf(tp_s_KW,type,
s_KW: $i ).
thf(tp_s_KY,type,
s_KY: $i ).
thf(tp_s_KZ,type,
s_KZ: $i ).
thf(tp_s_LA,type,
s_LA: $i ).
thf(tp_s_LB,type,
s_LB: $i ).
thf(tp_s_LC,type,
s_LC: $i ).
thf(tp_s_LI,type,
s_LI: $i ).
thf(tp_s_LK,type,
s_LK: $i ).
thf(tp_s_LR,type,
s_LR: $i ).
thf(tp_s_LS,type,
s_LS: $i ).
thf(tp_s_LT,type,
s_LT: $i ).
thf(tp_s_LU,type,
s_LU: $i ).
thf(tp_s_LV,type,
s_LV: $i ).
thf(tp_s_LY,type,
s_LY: $i ).
thf(tp_s_MA,type,
s_MA: $i ).
thf(tp_s_MC,type,
s_MC: $i ).
thf(tp_s_MD,type,
s_MD: $i ).
thf(tp_s_ME,type,
s_ME: $i ).
thf(tp_s_MF,type,
s_MF: $i ).
thf(tp_s_MG,type,
s_MG: $i ).
thf(tp_s_MH,type,
s_MH: $i ).
thf(tp_s_MK,type,
s_MK: $i ).
thf(tp_s_ML,type,
s_ML: $i ).
thf(tp_s_MM,type,
s_MM: $i ).
thf(tp_s_MN,type,
s_MN: $i ).
thf(tp_s_MO,type,
s_MO: $i ).
thf(tp_s_MP,type,
s_MP: $i ).
thf(tp_s_MQ,type,
s_MQ: $i ).
thf(tp_s_MR,type,
s_MR: $i ).
thf(tp_s_MS,type,
s_MS: $i ).
thf(tp_s_MT,type,
s_MT: $i ).
thf(tp_s_MU,type,
s_MU: $i ).
thf(tp_s_MV,type,
s_MV: $i ).
thf(tp_s_MW,type,
s_MW: $i ).
thf(tp_s_MX,type,
s_MX: $i ).
thf(tp_s_MY,type,
s_MY: $i ).
thf(tp_s_MZ,type,
s_MZ: $i ).
thf(tp_s_NA,type,
s_NA: $i ).
thf(tp_s_NC,type,
s_NC: $i ).
thf(tp_s_NE,type,
s_NE: $i ).
thf(tp_s_NF,type,
s_NF: $i ).
thf(tp_s_NG,type,
s_NG: $i ).
thf(tp_s_NI,type,
s_NI: $i ).
thf(tp_s_NL,type,
s_NL: $i ).
thf(tp_s_NO,type,
s_NO: $i ).
thf(tp_s_NP,type,
s_NP: $i ).
thf(tp_s_NR,type,
s_NR: $i ).
thf(tp_s_NT,type,
s_NT: $i ).
thf(tp_s_NU,type,
s_NU: $i ).
thf(tp_s_NZ,type,
s_NZ: $i ).
thf(tp_s_OM,type,
s_OM: $i ).
thf(tp_s_PA,type,
s_PA: $i ).
thf(tp_s_PE,type,
s_PE: $i ).
thf(tp_s_PF,type,
s_PF: $i ).
thf(tp_s_PG,type,
s_PG: $i ).
thf(tp_s_PH,type,
s_PH: $i ).
thf(tp_s_PK,type,
s_PK: $i ).
thf(tp_s_PL,type,
s_PL: $i ).
thf(tp_s_PM,type,
s_PM: $i ).
thf(tp_s_PN,type,
s_PN: $i ).
thf(tp_s_PR,type,
s_PR: $i ).
thf(tp_s_PS,type,
s_PS: $i ).
thf(tp_s_PT,type,
s_PT: $i ).
thf(tp_s_PW,type,
s_PW: $i ).
thf(tp_s_PY,type,
s_PY: $i ).
thf(tp_s_QA,type,
s_QA: $i ).
thf(tp_s_RE,type,
s_RE: $i ).
thf(tp_s_RO,type,
s_RO: $i ).
thf(tp_s_RS,type,
s_RS: $i ).
thf(tp_s_RU,type,
s_RU: $i ).
thf(tp_s_RW,type,
s_RW: $i ).
thf(tp_s_SA,type,
s_SA: $i ).
thf(tp_s_SB,type,
s_SB: $i ).
thf(tp_s_SC,type,
s_SC: $i ).
thf(tp_s_SD,type,
s_SD: $i ).
thf(tp_s_SE,type,
s_SE: $i ).
thf(tp_s_SG,type,
s_SG: $i ).
thf(tp_s_SH,type,
s_SH: $i ).
thf(tp_s_SI,type,
s_SI: $i ).
thf(tp_s_SJ,type,
s_SJ: $i ).
thf(tp_s_SK,type,
s_SK: $i ).
thf(tp_s_SL,type,
s_SL: $i ).
thf(tp_s_SM,type,
s_SM: $i ).
thf(tp_s_SN,type,
s_SN: $i ).
thf(tp_s_SO,type,
s_SO: $i ).
thf(tp_s_SR,type,
s_SR: $i ).
thf(tp_s_ST,type,
s_ST: $i ).
thf(tp_s_SU,type,
s_SU: $i ).
thf(tp_s_SV,type,
s_SV: $i ).
thf(tp_s_SY,type,
s_SY: $i ).
thf(tp_s_SZ,type,
s_SZ: $i ).
thf(tp_s_TC,type,
s_TC: $i ).
thf(tp_s_TD,type,
s_TD: $i ).
thf(tp_s_TG,type,
s_TG: $i ).
thf(tp_s_TH,type,
s_TH: $i ).
thf(tp_s_TJ,type,
s_TJ: $i ).
thf(tp_s_TK,type,
s_TK: $i ).
thf(tp_s_TL,type,
s_TL: $i ).
thf(tp_s_TM,type,
s_TM: $i ).
thf(tp_s_TN,type,
s_TN: $i ).
thf(tp_s_TO,type,
s_TO: $i ).
thf(tp_s_TP,type,
s_TP: $i ).
thf(tp_s_TR,type,
s_TR: $i ).
thf(tp_s_TT,type,
s_TT: $i ).
thf(tp_s_TV,type,
s_TV: $i ).
thf(tp_s_TW,type,
s_TW: $i ).
thf(tp_s_TZ,type,
s_TZ: $i ).
thf(tp_s_UA,type,
s_UA: $i ).
thf(tp_s_UG,type,
s_UG: $i ).
thf(tp_s_US,type,
s_US: $i ).
thf(tp_s_UY,type,
s_UY: $i ).
thf(tp_s_UZ,type,
s_UZ: $i ).
thf(tp_s_VA,type,
s_VA: $i ).
thf(tp_s_VC,type,
s_VC: $i ).
thf(tp_s_VE,type,
s_VE: $i ).
thf(tp_s_VG,type,
s_VG: $i ).
thf(tp_s_VI,type,
s_VI: $i ).
thf(tp_s_VN,type,
s_VN: $i ).
thf(tp_s_VU,type,
s_VU: $i ).
thf(tp_s_WF,type,
s_WF: $i ).
thf(tp_s_WS,type,
s_WS: $i ).
thf(tp_s_YD,type,
s_YD: $i ).
thf(tp_s_YE,type,
s_YE: $i ).
thf(tp_s_YT,type,
s_YT: $i ).
thf(tp_s_YU,type,
s_YU: $i ).
thf(tp_s_ZA,type,
s_ZA: $i ).
thf(tp_s_ZM,type,
s_ZM: $i ).
thf(tp_s_ZR,type,
s_ZR: $i ).
thf(tp_s_ZW,type,
s_ZW: $i ).
thf(tp_s_contains,type,
s_contains: $i > $i > $o ).
thf(tp_s_g001,type,
s_g001: $i ).
thf(tp_s_g002,type,
s_g002: $i ).
thf(tp_s_g003,type,
s_g003: $i ).
thf(tp_s_g005,type,
s_g005: $i ).
thf(tp_s_g009,type,
s_g009: $i ).
thf(tp_s_g011,type,
s_g011: $i ).
thf(tp_s_g013,type,
s_g013: $i ).
thf(tp_s_g014,type,
s_g014: $i ).
thf(tp_s_g015,type,
s_g015: $i ).
thf(tp_s_g017,type,
s_g017: $i ).
thf(tp_s_g018,type,
s_g018: $i ).
thf(tp_s_g019,type,
s_g019: $i ).
thf(tp_s_g021,type,
s_g021: $i ).
thf(tp_s_g029,type,
s_g029: $i ).
thf(tp_s_g030,type,
s_g030: $i ).
thf(tp_s_g034,type,
s_g034: $i ).
thf(tp_s_g035,type,
s_g035: $i ).
thf(tp_s_g039,type,
s_g039: $i ).
thf(tp_s_g053,type,
s_g053: $i ).
thf(tp_s_g054,type,
s_g054: $i ).
thf(tp_s_g057,type,
s_g057: $i ).
thf(tp_s_g061,type,
s_g061: $i ).
thf(tp_s_g062,type,
s_g062: $i ).
thf(tp_s_g142,type,
s_g142: $i ).
thf(tp_s_g143,type,
s_g143: $i ).
thf(tp_s_g145,type,
s_g145: $i ).
thf(tp_s_g150,type,
s_g150: $i ).
thf(tp_s_g151,type,
s_g151: $i ).
thf(tp_s_g154,type,
s_g154: $i ).
thf(tp_s_g155,type,
s_g155: $i ).
thf(tp_s_g172,type,
s_g172: $i ).
thf(tp_s_g419,type,
s_g419: $i ).
thf(tp_s_g830,type,
s_g830: $i ).
thf(tp_s_partOf,type,
s_partOf: $i > $i > $o ).
thf(1,axiom,
! [X: $i,Y: $i] :
( ( s_contains @ X @ Y )
=> ( s_partOf @ Y @ X ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom3) ).
thf(2,axiom,
! [X: $i,Y: $i] :
( ( s_partOf @ X @ Y )
=> ( s_contains @ Y @ X ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom2) ).
thf(3,axiom,
! [X: $i,Y: $i,Z: $i] :
( ( ( s_contains @ X @ Y )
& ( s_contains @ Y @ Z ) )
=> ( s_contains @ X @ Z ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom1) ).
thf(529,axiom,
s_contains @ s_g013 @ s_MX,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb74) ).
thf(581,axiom,
s_contains @ s_g019 @ s_g419,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb22) ).
thf(582,axiom,
s_contains @ s_g019 @ s_g003,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb21) ).
thf(583,axiom,
s_contains @ s_g019 @ s_g029,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb20) ).
thf(584,axiom,
s_contains @ s_g019 @ s_g021,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb19) ).
thf(585,axiom,
s_contains @ s_g019 @ s_g013,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb18) ).
thf(586,axiom,
s_contains @ s_g019 @ s_g005,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb17) ).
thf(601,axiom,
s_contains @ s_g001 @ s_g019,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb2) ).
thf(604,conjecture,
s_contains @ s_g019 @ s_MX,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mexico_in_america_1) ).
thf(605,negated_conjecture,
( ( s_contains @ s_g019 @ s_MX )
= $false ),
inference(negate_conjecture,[status(cth)],[604]) ).
thf(606,plain,
( ( s_contains @ s_g019 @ s_MX )
= $false ),
inference(unfold_def,[status(thm)],[605]) ).
thf(607,plain,
( ( ! [X: $i,Y: $i] :
( ( s_contains @ X @ Y )
=> ( s_partOf @ Y @ X ) ) )
= $true ),
inference(unfold_def,[status(thm)],[1]) ).
thf(608,plain,
( ( ! [X: $i,Y: $i] :
( ( s_partOf @ X @ Y )
=> ( s_contains @ Y @ X ) ) )
= $true ),
inference(unfold_def,[status(thm)],[2]) ).
thf(609,plain,
( ( ! [X: $i,Y: $i,Z: $i] :
( ( ( s_contains @ X @ Y )
& ( s_contains @ Y @ Z ) )
=> ( s_contains @ X @ Z ) ) )
= $true ),
inference(unfold_def,[status(thm)],[3]) ).
thf(610,plain,
( ( s_contains @ s_g013 @ s_MX )
= $true ),
inference(unfold_def,[status(thm)],[529]) ).
thf(611,plain,
( ( s_contains @ s_g019 @ s_g419 )
= $true ),
inference(unfold_def,[status(thm)],[581]) ).
thf(612,plain,
( ( s_contains @ s_g019 @ s_g003 )
= $true ),
inference(unfold_def,[status(thm)],[582]) ).
thf(613,plain,
( ( s_contains @ s_g019 @ s_g029 )
= $true ),
inference(unfold_def,[status(thm)],[583]) ).
thf(614,plain,
( ( s_contains @ s_g019 @ s_g021 )
= $true ),
inference(unfold_def,[status(thm)],[584]) ).
thf(615,plain,
( ( s_contains @ s_g019 @ s_g013 )
= $true ),
inference(unfold_def,[status(thm)],[585]) ).
thf(616,plain,
( ( s_contains @ s_g019 @ s_g005 )
= $true ),
inference(unfold_def,[status(thm)],[586]) ).
thf(617,plain,
( ( s_contains @ s_g001 @ s_g019 )
= $true ),
inference(unfold_def,[status(thm)],[601]) ).
thf(618,plain,
( ( ~ ( s_contains @ s_g019 @ s_MX ) )
= $true ),
inference(polarity_switch,[status(thm)],[606]) ).
thf(619,plain,
( ( s_contains @ s_g001 @ s_g019 )
= $true ),
inference(copy,[status(thm)],[617]) ).
thf(620,plain,
( ( s_contains @ s_g019 @ s_g005 )
= $true ),
inference(copy,[status(thm)],[616]) ).
thf(621,plain,
( ( s_contains @ s_g019 @ s_g013 )
= $true ),
inference(copy,[status(thm)],[615]) ).
thf(622,plain,
( ( s_contains @ s_g019 @ s_g021 )
= $true ),
inference(copy,[status(thm)],[614]) ).
thf(623,plain,
( ( s_contains @ s_g019 @ s_g029 )
= $true ),
inference(copy,[status(thm)],[613]) ).
thf(624,plain,
( ( s_contains @ s_g019 @ s_g003 )
= $true ),
inference(copy,[status(thm)],[612]) ).
thf(625,plain,
( ( s_contains @ s_g019 @ s_g419 )
= $true ),
inference(copy,[status(thm)],[611]) ).
thf(626,plain,
( ( s_contains @ s_g013 @ s_MX )
= $true ),
inference(copy,[status(thm)],[610]) ).
thf(627,plain,
( ( ! [X: $i,Y: $i,Z: $i] :
( ( ( s_contains @ X @ Y )
& ( s_contains @ Y @ Z ) )
=> ( s_contains @ X @ Z ) ) )
= $true ),
inference(copy,[status(thm)],[609]) ).
thf(628,plain,
( ( ! [X: $i,Y: $i] :
( ( s_partOf @ X @ Y )
=> ( s_contains @ Y @ X ) ) )
= $true ),
inference(copy,[status(thm)],[608]) ).
thf(629,plain,
( ( ! [X: $i,Y: $i] :
( ( s_contains @ X @ Y )
=> ( s_partOf @ Y @ X ) ) )
= $true ),
inference(copy,[status(thm)],[607]) ).
thf(630,plain,
( ( ~ ( s_contains @ s_g019 @ s_MX ) )
= $true ),
inference(copy,[status(thm)],[618]) ).
thf(631,plain,
( ( ! [SX0: $i,SX1: $i] :
( ~ ( s_partOf @ SX0 @ SX1 )
| ( s_contains @ SX1 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[628]) ).
thf(632,plain,
( ( ! [SX0: $i,SX1: $i] :
( ~ ( s_contains @ SX0 @ SX1 )
| ( s_partOf @ SX1 @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[629]) ).
thf(633,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( ~ ~ ( ~ ( s_contains @ SX0 @ SX1 )
| ~ ( s_contains @ SX1 @ SX2 ) )
| ( s_contains @ SX0 @ SX2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[627]) ).
thf(634,plain,
( ( s_contains @ s_g019 @ s_MX )
= $false ),
inference(extcnf_not_pos,[status(thm)],[630]) ).
thf(635,plain,
! [SV1: $i] :
( ( ! [SY7: $i] :
( ~ ( s_partOf @ SV1 @ SY7 )
| ( s_contains @ SY7 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[631]) ).
thf(636,plain,
! [SV2: $i] :
( ( ! [SY8: $i] :
( ~ ( s_contains @ SV2 @ SY8 )
| ( s_partOf @ SY8 @ SV2 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[632]) ).
thf(637,plain,
! [SV3: $i] :
( ( ! [SY9: $i,SY10: $i] :
( ~ ~ ( ~ ( s_contains @ SV3 @ SY9 )
| ~ ( s_contains @ SY9 @ SY10 ) )
| ( s_contains @ SV3 @ SY10 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[633]) ).
thf(638,plain,
! [SV4: $i,SV1: $i] :
( ( ~ ( s_partOf @ SV1 @ SV4 )
| ( s_contains @ SV4 @ SV1 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[635]) ).
thf(639,plain,
! [SV5: $i,SV2: $i] :
( ( ~ ( s_contains @ SV2 @ SV5 )
| ( s_partOf @ SV5 @ SV2 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[636]) ).
thf(640,plain,
! [SV6: $i,SV3: $i] :
( ( ! [SY11: $i] :
( ~ ~ ( ~ ( s_contains @ SV3 @ SV6 )
| ~ ( s_contains @ SV6 @ SY11 ) )
| ( s_contains @ SV3 @ SY11 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[637]) ).
thf(641,plain,
! [SV4: $i,SV1: $i] :
( ( ( ~ ( s_partOf @ SV1 @ SV4 ) )
= $true )
| ( ( s_contains @ SV4 @ SV1 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[638]) ).
thf(642,plain,
! [SV5: $i,SV2: $i] :
( ( ( ~ ( s_contains @ SV2 @ SV5 ) )
= $true )
| ( ( s_partOf @ SV5 @ SV2 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[639]) ).
thf(643,plain,
! [SV7: $i,SV6: $i,SV3: $i] :
( ( ~ ~ ( ~ ( s_contains @ SV3 @ SV6 )
| ~ ( s_contains @ SV6 @ SV7 ) )
| ( s_contains @ SV3 @ SV7 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[640]) ).
thf(644,plain,
! [SV4: $i,SV1: $i] :
( ( ( s_partOf @ SV1 @ SV4 )
= $false )
| ( ( s_contains @ SV4 @ SV1 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[641]) ).
thf(645,plain,
! [SV5: $i,SV2: $i] :
( ( ( s_contains @ SV2 @ SV5 )
= $false )
| ( ( s_partOf @ SV5 @ SV2 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[642]) ).
thf(646,plain,
! [SV7: $i,SV6: $i,SV3: $i] :
( ( ( ~ ~ ( ~ ( s_contains @ SV3 @ SV6 )
| ~ ( s_contains @ SV6 @ SV7 ) ) )
= $true )
| ( ( s_contains @ SV3 @ SV7 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[643]) ).
thf(647,plain,
! [SV7: $i,SV6: $i,SV3: $i] :
( ( ( ~ ( ~ ( s_contains @ SV3 @ SV6 )
| ~ ( s_contains @ SV6 @ SV7 ) ) )
= $false )
| ( ( s_contains @ SV3 @ SV7 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[646]) ).
thf(648,plain,
! [SV7: $i,SV6: $i,SV3: $i] :
( ( ( ~ ( s_contains @ SV3 @ SV6 )
| ~ ( s_contains @ SV6 @ SV7 ) )
= $true )
| ( ( s_contains @ SV3 @ SV7 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[647]) ).
thf(649,plain,
! [SV7: $i,SV6: $i,SV3: $i] :
( ( ( ~ ( s_contains @ SV3 @ SV6 ) )
= $true )
| ( ( ~ ( s_contains @ SV6 @ SV7 ) )
= $true )
| ( ( s_contains @ SV3 @ SV7 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[648]) ).
thf(650,plain,
! [SV7: $i,SV6: $i,SV3: $i] :
( ( ( s_contains @ SV3 @ SV6 )
= $false )
| ( ( ~ ( s_contains @ SV6 @ SV7 ) )
= $true )
| ( ( s_contains @ SV3 @ SV7 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[649]) ).
thf(651,plain,
! [SV3: $i,SV7: $i,SV6: $i] :
( ( ( s_contains @ SV6 @ SV7 )
= $false )
| ( ( s_contains @ SV3 @ SV6 )
= $false )
| ( ( s_contains @ SV3 @ SV7 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[650]) ).
thf(652,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[619,651,645,644,634,626,625,624,623,622,621,620]) ).
thf(653,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[652]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MSC019+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.18 % Computer : n004.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Oct 6 12:44:54 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.70/0.30 .
% 0.70/0.30
% 0.70/0.30 No.of.Axioms: 11
% 0.70/0.30
% 0.70/0.30 Length.of.Defs: 0
% 0.70/0.30
% 0.70/0.30 Contains.Choice.Funs: false
% 0.70/0.30 ...
% 0.70/0.30
% 0.70/0.30 ********************************
% 0.70/0.30 * All subproblems solved! *
% 0.70/0.30 ********************************
% 0.70/0.30 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:11,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:299,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:652,loop_count:0,foatp_calls:1,translation:fof_full)
% 0.70/0.30
% 0.70/0.30 %**** Beginning of derivation protocol ****
% 0.70/0.30 % SZS output start CNFRefutation
% See solution above
% 0.70/0.30
% 0.70/0.30 %**** End of derivation protocol ****
% 0.70/0.30 %**** no. of clauses in derivation: 61 ****
% 0.70/0.30 %**** clause counter: 652 ****
% 0.70/0.30
% 0.70/0.30 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:11,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:299,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:652,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------