%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SYO580+1 : TPTP v9.2.1. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n015.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:19:56 PM UTC 2026 % Result : Theorem 22.26s 22.04s % Output : Proof 22.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYO580+1 : TPTP v9.2.1. Released v5.5.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.17/0.34 % Computer : n015.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Mon May 11 14:50:17 EDT 2026 % 0.17/0.34 % CPUTime : % 22.26/22.04 % SZS status Theorem % 22.26/22.04 % SZS output start Proof % 22.26/22.04 % 22.26/22.04 =============================================================== % 22.26/22.04 TPTP Problem: goals_886 (conjecture with 885 axiom(s)) % 22.26/22.04 Axioms: [sos_01,sos_02,sos_03,sos_04,sos_05,sos_06,sos_07,sos_08,sos_09,sos_10,sos_11,sos_12,sos_13,sos_14,sos_15,sos_16,sos_17,sos_18,sos_19,sos_20,sos_21,sos_22,sos_23,sos_24,sos_25,sos_26,sos_27,sos_28,sos_29,sos_30,sos_31,sos_32,sos_33,sos_34,sos_35,sos_36,sos_37,sos_38,sos_39,sos_40,sos_41,sos_42,sos_43,sos_44,sos_45,sos_46,sos_47,sos_48,sos_49,sos_50,sos_51,sos_52,sos_53,sos_54,sos_55,sos_56,sos_57,sos_58,sos_59,sos_60,sos_61,sos_62,sos_63,sos_64,sos_65,sos_66,sos_67,sos_68,sos_69,sos_70,sos_71,sos_72,sos_73,sos_74,sos_75,sos_76,sos_77,sos_78,sos_79,sos_80,sos_81,sos_82,sos_83,sos_84,sos_85,sos_86,sos_87,sos_88,sos_89,sos_90,sos_91,sos_92,sos_93,sos_94,sos_95,sos_96,sos_97,sos_98,sos_99,sos_100,sos_101,sos_102,sos_103,sos_104,sos_105,sos_106,sos_107,sos_108,sos_109,sos_110,sos_111,sos_112,sos_113,sos_114,sos_115,sos_116,sos_117,sos_118,sos_119,sos_120,sos_121,sos_122,sos_123,sos_124,sos_125,sos_126,sos_127,sos_128,sos_129,sos_130,sos_131,sos_132,sos_133,sos_134,sos_135,sos_136,sos_137,sos_138,sos_139,sos_140,sos_141,sos_142,sos_143,sos_144,sos_145,sos_146,sos_147,sos_148,sos_149,sos_150,sos_151,sos_152,sos_153,sos_154,sos_155,sos_156,sos_157,sos_158,sos_159,sos_160,sos_161,sos_162,sos_163,sos_164,sos_165,sos_166,sos_167,sos_168,sos_169,sos_170,sos_171,sos_172,sos_173,sos_174,sos_175,sos_176,sos_177,sos_178,sos_179,sos_180,sos_181,sos_182,sos_183,sos_184,sos_185,sos_186,sos_187,sos_188,sos_189,sos_190,sos_191,sos_192,sos_193,sos_194,sos_195,sos_196,sos_197,sos_198,sos_199,sos_200,sos_201,sos_202,sos_203,sos_204,sos_205,sos_206,sos_207,sos_208,sos_209,sos_210,sos_211,sos_212,sos_213,sos_214,sos_215,sos_216,sos_217,sos_218,sos_219,sos_220,sos_221,sos_222,sos_223,sos_224,sos_225,sos_226,sos_227,sos_228,sos_229,sos_230,sos_231,sos_232,sos_233,sos_234,sos_235,sos_236,sos_237,sos_238,sos_239,sos_240,sos_241,sos_242,sos_243,sos_244,sos_245,sos_246,sos_247,sos_248,sos_249,sos_250,sos_251,sos_252,sos_253,sos_254,sos_255,sos_256,sos_257,sos_258,sos_259,sos_260,sos_261,sos_262,sos_263,sos_264,sos_265,sos_266,sos_267,sos_268,sos_269,sos_270,sos_271,sos_272,sos_273,sos_274,sos_275,sos_276,sos_277,sos_278,sos_279,sos_280,sos_281,sos_282,sos_283,sos_284,sos_285,sos_286,sos_287,sos_288,sos_289,sos_290,sos_291,sos_292,sos_293,sos_294,sos_295,sos_296,sos_297,sos_298,sos_299,sos_300,sos_301,sos_302,sos_303,sos_304,sos_305,sos_306,sos_307,sos_308,sos_309,sos_310,sos_311,sos_312,sos_313,sos_314,sos_315,sos_316,sos_317,sos_318,sos_319,sos_320,sos_321,sos_322,sos_323,sos_324,sos_325,sos_326,sos_327,sos_328,sos_329,sos_330,sos_331,sos_332,sos_333,sos_334,sos_335,sos_336,sos_337,sos_338,sos_339,sos_340,sos_341,sos_342,sos_343,sos_344,sos_345,sos_346,sos_347,sos_348,sos_349,sos_350,sos_351,sos_352,sos_353,sos_354,sos_355,sos_356,sos_357,sos_358,sos_359,sos_360,sos_361,sos_362,sos_363,sos_364,sos_365,sos_366,sos_367,sos_368,sos_369,sos_370,sos_371,sos_372,sos_373,sos_374,sos_375,sos_376,sos_377,sos_378,sos_379,sos_380,sos_381,sos_382,sos_383,sos_384,sos_385,sos_386,sos_387,sos_388,sos_389,sos_390,sos_391,sos_392,sos_393,sos_394,sos_395,sos_396,sos_397,sos_398,sos_399,sos_400,sos_401,sos_402,sos_403,sos_404,sos_405,sos_406,sos_407,sos_408,sos_409,sos_410,sos_411,sos_412,sos_413,sos_414,sos_415,sos_416,sos_417,sos_418,sos_419,sos_420,sos_421,sos_422,sos_423,sos_424,sos_425,sos_426,sos_427,sos_428,sos_429,sos_430,sos_431,sos_432,sos_433,sos_434,sos_435,sos_436,sos_437,sos_438,sos_439,sos_440,sos_441,sos_442,sos_443,sos_444,sos_445,sos_446,sos_447,sos_448,sos_449,sos_450,sos_451,sos_452,sos_453,sos_454,sos_455,sos_456,sos_457,sos_458,sos_459,sos_460,sos_461,sos_462,sos_463,sos_464,sos_465,sos_466,sos_467,sos_468,sos_469,sos_470,sos_471,sos_472,sos_473,sos_474,sos_475,sos_476,sos_477,sos_478,sos_479,sos_480,sos_481,sos_482,sos_483,sos_484,sos_485,sos_486,sos_487,sos_488,sos_489,sos_490,sos_491,sos_492,sos_493,sos_494,sos_495,sos_496,sos_497,sos_498,sos_499,sos_500,sos_501,sos_502,sos_503,sos_504,sos_505,sos_506,sos_507,sos_508,sos_509,sos_510,sos_511,sos_512,sos_513,sos_514,sos_515,sos_516,sos_517,sos_518,sos_519,sos_520,sos_521,sos_522,sos_523,sos_524,sos_525,sos_526,sos_527,sos_528,sos_529,sos_530,sos_531,sos_532,sos_533,sos_534,sos_535,sos_536,sos_537,sos_538,sos_539,sos_540,sos_541,sos_542,sos_543,sos_544,sos_545,sos_546,sos_547,sos_548,sos_549,sos_550,sos_551,sos_552,sos_553,sos_554,sos_555,sos_556,sos_557,sos_558,sos_559,sos_560,sos_561,sos_562,sos_563,sos_564,sos_565,sos_566,sos_567,sos_568,sos_569,sos_570,sos_571,sos_572,sos_573,sos_574,sos_575,sos_576,sos_577,sos_578,sos_579,sos_580,sos_581,sos_582,sos_583,sos_584,sos_585,sos_586,sos_587,sos_588,sos_589,sos_590,sos_591,sos_592,sos_593,sos_594,sos_595,sos_596,sos_597,sos_598,sos_599,sos_600,sos_601,sos_602,sos_603,sos_604,sos_605,sos_606,sos_607,sos_608,sos_609,sos_610,sos_611,sos_612,sos_613,sos_614,sos_615,sos_616,sos_617,sos_618,sos_619,sos_620,sos_621,sos_622,sos_623,sos_624,sos_625,sos_626,sos_627,sos_628,sos_629,sos_630,sos_631,sos_632,sos_633,sos_634,sos_635,sos_636,sos_637,sos_638,sos_639,sos_640,sos_641,sos_642,sos_643,sos_644,sos_645,sos_646,sos_647,sos_648,sos_649,sos_650,sos_651,sos_652,sos_653,sos_654,sos_655,sos_656,sos_657,sos_658,sos_659,sos_660,sos_661,sos_662,sos_663,sos_664,sos_665,sos_666,sos_667,sos_668,sos_669,sos_670,sos_671,sos_672,sos_673,sos_674,sos_675,sos_676,sos_677,sos_678,sos_679,sos_680,sos_681,sos_682,sos_683,sos_684,sos_685,sos_686,sos_687,sos_688,sos_689,sos_690,sos_691,sos_692,sos_693,sos_694,sos_695,sos_696,sos_697,sos_698,sos_699,sos_700,sos_701,sos_702,sos_703,sos_704,sos_705,sos_706,sos_707,sos_708,sos_709,sos_710,sos_711,sos_712,sos_713,sos_714,sos_715,sos_716,sos_717,sos_718,sos_719,sos_720,sos_721,sos_722,sos_723,sos_724,sos_725,sos_726,sos_727,sos_728,sos_729,sos_730,sos_731,sos_732,sos_733,sos_734,sos_735,sos_736,sos_737,sos_738,sos_739,sos_740,sos_741,sos_742,sos_743,sos_744,sos_745,sos_746,sos_747,sos_748,sos_749,sos_750,sos_751,sos_752,sos_753,sos_754,sos_755,sos_756,sos_757,sos_758,sos_759,sos_760,sos_761,sos_762,sos_763,sos_764,sos_765,sos_766,sos_767,sos_768,sos_769,sos_770,sos_771,sos_772,sos_773,sos_774,sos_775,sos_776,sos_777,sos_778,sos_779,sos_780,sos_781,sos_782,sos_783,sos_784,sos_785,sos_786,sos_787,sos_788,sos_789,sos_790,sos_791,sos_792,sos_793,sos_794,sos_795,sos_796,sos_797,sos_798,sos_799,sos_800,sos_801,sos_802,sos_803,sos_804,sos_805,sos_806,sos_807,sos_808,sos_809,sos_810,sos_811,sos_812,sos_813,sos_814,sos_815,sos_816,sos_817,sos_818,sos_819,sos_820,sos_821,sos_822,sos_823,sos_824,sos_825,sos_826,sos_827,sos_828,sos_829,sos_830,sos_831,sos_832,sos_833,sos_834,sos_835,sos_836,sos_837,sos_838,sos_839,sos_840,sos_841,sos_842,sos_843,sos_844,sos_845,sos_846,sos_847,sos_848,sos_849,sos_850,sos_851,sos_852,sos_853,sos_854,sos_855,sos_856,sos_857,sos_858,sos_859,sos_860,sos_861,sos_862,sos_863,sos_864,sos_865,sos_866,sos_867,sos_868,sos_869,sos_870,sos_871,sos_872,sos_873,sos_874,sos_875,sos_876,sos_877,sos_878,sos_879,sos_880,sos_881,sos_882,sos_883,sos_884,sos_885] % 22.26/22.04 =============================================================== % 22.26/22.04 % 22.26/22.04 Combined formula: 885 axiom(s) => conjecture % 22.26/22.04 % 22.26/22.04 nanoCoP : % 22.26/22.04 % 502,276 inferences, 0.427 CPU in 0.427 seconds (100% CPU, 1176419 Lips) % 22.26/22.04 g4mic : % 22.26/22.04 % 100,036,305 inferences, 20.378 CPU in 20.378 seconds (100% CPU, 4908933 Lips) % 22.26/22.04 % 22.26/22.04 % Logic level: not determined (G4+ inference limit exceeded) % 22.26/22.04 % To get proofs (sequent calculus G4 and natural deduction), you can use G4+ at https://g4-mic.vidal-rosset.net/wasm/tinker % 22.26/22.04 % 22.26/22.04 % SZS output end Proof %------------------------------------------------------------------------------