%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : MSC019+1 : TPTP v9.2.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % Computer : n008.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 May 12 07:06:13 PM UTC 2026 % Result : Theorem 15.94s 15.83s % Output : Proof 15.94s % 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.00/0.12 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.17/0.33 % Computer : n008.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Mon May 11 13:13:14 EDT 2026 % 0.17/0.33 % CPUTime : % 15.94/15.83 % SZS status Theorem % 15.94/15.83 % SZS output start Proof % 15.94/15.83 % 15.94/15.83 =============================================================== % 15.94/15.83 TPTP Problem: mexico_in_america_1 (conjecture with 603 axiom(s)) % 15.94/15.83 Axioms: [kb0,kb1,kb2,kb3,kb4,kb5,kb6,kb7,kb8,kb9,kb10,kb11,kb12,kb13,kb14,kb15,kb16,kb17,kb18,kb19,kb20,kb21,kb22,kb23,kb24,kb25,kb26,kb27,kb28,kb29,kb30,kb31,kb32,kb33,kb34,kb35,kb36,kb37,kb38,kb39,kb40,kb41,kb42,kb43,kb44,kb45,kb46,kb47,kb48,kb49,kb50,kb51,kb52,kb53,kb54,kb55,kb56,kb57,kb58,kb59,kb60,kb61,kb62,kb63,kb64,kb65,kb66,kb67,kb68,kb69,kb70,kb71,kb72,kb73,kb74,kb75,kb76,kb77,kb78,kb79,kb80,kb81,kb82,kb83,kb84,kb85,kb86,kb87,kb88,kb89,kb90,kb91,kb92,kb93,kb94,kb95,kb96,kb97,kb98,kb99,kb100,kb101,kb102,kb103,kb104,kb105,kb106,kb107,kb108,kb109,kb110,kb111,kb112,kb113,kb114,kb115,kb116,kb117,kb118,kb119,kb120,kb121,kb122,kb123,kb124,kb125,kb126,kb127,kb128,kb129,kb130,kb131,kb132,kb133,kb134,kb135,kb136,kb137,kb138,kb139,kb140,kb141,kb142,kb143,kb144,kb145,kb146,kb147,kb148,kb149,kb150,kb151,kb152,kb153,kb154,kb155,kb156,kb157,kb158,kb159,kb160,kb161,kb162,kb163,kb164,kb165,kb166,kb167,kb168,kb169,kb170,kb171,kb172,kb173,kb174,kb175,kb176,kb177,kb178,kb179,kb180,kb181,kb182,kb183,kb184,kb185,kb186,kb187,kb188,kb189,kb190,kb191,kb192,kb193,kb194,kb195,kb196,kb197,kb198,kb199,kb200,kb201,kb202,kb203,kb204,kb205,kb206,kb207,kb208,kb209,kb210,kb211,kb212,kb213,kb214,kb215,kb216,kb217,kb218,kb219,kb220,kb221,kb222,kb223,kb224,kb225,kb226,kb227,kb228,kb229,kb230,kb231,kb232,kb233,kb234,kb235,kb236,kb237,kb238,kb239,kb240,kb241,kb242,kb243,kb244,kb245,kb246,kb247,kb248,kb249,kb250,kb251,kb252,kb253,kb254,kb255,kb256,kb257,kb258,kb259,kb260,kb261,kb262,kb263,kb264,kb265,kb266,kb267,kb268,kb269,kb270,kb271,kb272,kb273,kb274,kb275,kb276,kb277,kb278,kb279,kb280,kb281,kb282,kb283,kb284,kb285,kb286,kb287,kb288,kb289,kb290,kb291,kb292,kb293,kb294,kb295,kb296,kb297,kb298,kb299,kb300,kb301,kb302,kb303,kb304,kb305,kb306,kb307,kb308,kb309,kb310,kb311,kb312,kb313,kb314,kb315,kb316,kb317,kb318,kb319,kb320,kb321,kb322,kb323,kb324,kb325,kb326,kb327,kb328,kb329,kb330,kb331,kb332,kb333,kb334,kb335,kb336,kb337,kb338,kb339,kb340,kb341,kb342,kb343,kb344,kb345,kb346,kb347,kb348,kb349,kb350,kb351,kb352,kb353,kb354,kb355,kb356,kb357,kb358,kb359,kb360,kb361,kb362,kb363,kb364,kb365,kb366,kb367,kb368,kb369,kb370,kb371,kb372,kb373,kb374,kb375,kb376,kb377,kb378,kb379,kb380,kb381,kb382,kb383,kb384,kb385,kb386,kb387,kb388,kb389,kb390,kb391,kb392,kb393,kb394,kb395,kb396,kb397,kb398,kb399,kb400,kb401,kb402,kb403,kb404,kb405,kb406,kb407,kb408,kb409,kb410,kb411,kb412,kb413,kb414,kb415,kb416,kb417,kb418,kb419,kb420,kb421,kb422,kb423,kb424,kb425,kb426,kb427,kb428,kb429,kb430,kb431,kb432,kb433,kb434,kb435,kb436,kb437,kb438,kb439,kb440,kb441,kb442,kb443,kb444,kb445,kb446,kb447,kb448,kb449,kb450,kb451,kb452,kb453,kb454,kb455,kb456,kb457,kb458,kb459,kb460,kb461,kb462,kb463,kb464,kb465,kb466,kb467,kb468,kb469,kb470,kb471,kb472,kb473,kb474,kb475,kb476,kb477,kb478,kb479,kb480,kb481,kb482,kb483,kb484,kb485,kb486,kb487,kb488,kb489,kb490,kb491,kb492,kb493,kb494,kb495,kb496,kb497,kb498,kb499,kb500,kb501,kb502,kb503,kb504,kb505,kb506,kb507,kb508,kb509,kb510,kb511,kb512,kb513,kb514,kb515,kb516,kb517,kb518,kb519,kb520,kb521,kb522,kb523,kb524,kb525,kb526,kb527,kb528,kb529,kb530,kb531,kb532,kb533,kb534,kb535,kb536,kb537,kb538,kb539,kb540,kb541,kb542,kb543,kb544,kb545,kb546,kb547,kb548,kb549,kb550,kb551,kb552,kb553,kb554,kb555,kb556,kb557,kb558,kb559,kb560,kb561,kb562,kb563,kb564,kb565,kb566,kb567,kb568,kb569,kb570,kb571,kb572,kb573,kb574,kb575,kb576,kb577,kb578,kb579,kb580,kb581,kb582,kb583,kb584,kb585,kb586,kb587,kb588,kb589,kb590,kb591,kb592,kb593,kb594,kb595,kb596,kb597,kb598,kb599,axiom1,axiom2,axiom3] % 15.94/15.83 =============================================================== % 15.94/15.83 % 15.94/15.83 Combined formula: 603 axiom(s) => conjecture % 15.94/15.83 % 15.94/15.83 nanoCoP : % 15.94/15.83 % 1,860,564 inferences, 0.690 CPU in 0.690 seconds (100% CPU, 2694559 Lips) % 15.94/15.83 g4mic : % 15.94/15.83 % 100,015,271 inferences, 14.133 CPU in 14.131 seconds (100% CPU, 7076770 Lips) % 15.94/15.83 % 15.94/15.83 % Logic level: not determined (G4+ inference limit exceeded) % 15.94/15.83 % To get proofs (sequent calculus G4 and natural deduction), you can use G4+ at https://g4-mic.vidal-rosset.net/wasm/tinker % 15.94/15.83 % 15.94/15.83 % SZS output end Proof %------------------------------------------------------------------------------