%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : KRS161+1 : TPTP v9.2.1. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n005.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:03:27 PM UTC 2026 % Result : Theorem 29.62s 29.26s % Output : Proof 29.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : KRS161+1 : TPTP v9.2.1. Released v3.1.0. % 0.00/0.11 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.15/0.32 % Computer : n005.cluster.edu % 0.15/0.32 % Model : x86_64 x86_64 % 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.32 % Memory : 8042.1875MB % 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.32 % CPULimit : 300 % 0.15/0.32 % WCLimit : 300 % 0.15/0.32 % DateTime : Mon May 11 12:26:01 EDT 2026 % 0.15/0.32 % CPUTime : % 29.62/29.26 % SZS status Theorem % 29.62/29.26 % SZS output start Proof % 29.62/29.26 % 29.62/29.26 =============================================================== % 29.62/29.26 TPTP Problem: the_axiom (conjecture with 286 axiom(s)) % 29.62/29.26 Axioms: [axiom_0,axiom_1,axiom_2,axiom_3,axiom_4,axiom_5,axiom_6,axiom_7,axiom_8,axiom_9,axiom_10,axiom_11,axiom_12,axiom_13,axiom_14,axiom_15,axiom_16,axiom_17,axiom_18,axiom_19,axiom_20,axiom_21,axiom_22,axiom_23,axiom_24,axiom_25,axiom_26,axiom_27,axiom_28,axiom_29,axiom_30,axiom_31,axiom_32,axiom_33,axiom_34,axiom_35,axiom_36,axiom_37,axiom_38,axiom_39,axiom_40,axiom_41,axiom_42,axiom_43,axiom_44,axiom_45,axiom_46,axiom_47,axiom_48,axiom_49,axiom_50,axiom_51,axiom_52,axiom_53,axiom_54,axiom_55,axiom_56,axiom_57,axiom_58,axiom_59,axiom_60,axiom_61,axiom_62,axiom_63,axiom_64,axiom_65,axiom_66,axiom_67,axiom_68,axiom_69,axiom_70,axiom_71,axiom_72,axiom_73,axiom_74,axiom_75,axiom_76,axiom_77,axiom_78,axiom_79,axiom_80,axiom_81,axiom_82,axiom_83,axiom_84,axiom_85,axiom_86,axiom_87,axiom_88,axiom_89,axiom_90,axiom_91,axiom_92,axiom_93,axiom_94,axiom_95,axiom_96,axiom_97,axiom_98,axiom_99,axiom_100,axiom_101,axiom_102,axiom_103,axiom_104,axiom_105,axiom_106,axiom_107,axiom_108,axiom_109,axiom_110,axiom_111,axiom_112,axiom_113,axiom_114,axiom_115,axiom_116,axiom_117,axiom_118,axiom_119,axiom_120,axiom_121,axiom_122,axiom_123,axiom_124,axiom_125,axiom_126,axiom_127,axiom_128,axiom_129,axiom_130,axiom_131,axiom_132,axiom_133,axiom_134,axiom_135,axiom_136,axiom_137,axiom_138,axiom_139,axiom_140,axiom_141,axiom_142,axiom_143,axiom_144,axiom_145,axiom_146,axiom_147,axiom_148,axiom_149,axiom_150,axiom_151,axiom_152,axiom_153,axiom_154,axiom_155,axiom_156,axiom_157,axiom_158,axiom_159,axiom_160,axiom_161,axiom_162,axiom_163,axiom_164,axiom_165,axiom_166,axiom_167,axiom_168,axiom_169,axiom_170,axiom_171,axiom_172,axiom_173,axiom_174,axiom_175,axiom_176,axiom_177,axiom_178,axiom_179,axiom_180,axiom_181,axiom_182,axiom_183,axiom_184,axiom_185,axiom_186,axiom_187,axiom_188,axiom_189,axiom_190,axiom_191,axiom_192,axiom_193,axiom_194,axiom_195,axiom_196,axiom_197,axiom_198,axiom_199,axiom_200,axiom_201,axiom_202,axiom_203,axiom_204,axiom_205,axiom_206,axiom_207,axiom_208,axiom_209,axiom_210,axiom_211,axiom_212,axiom_213,axiom_214,axiom_215,axiom_216,axiom_217,axiom_218,axiom_219,axiom_220,axiom_221,axiom_222,axiom_223,axiom_224,axiom_225,axiom_226,axiom_227,axiom_228,axiom_229,axiom_230,axiom_231,axiom_232,axiom_233,axiom_234,axiom_235,axiom_236,axiom_237,axiom_238,axiom_239,axiom_240,axiom_241,axiom_242,axiom_243,axiom_244,axiom_245,axiom_246,axiom_247,axiom_248,axiom_249,axiom_250,axiom_251,axiom_252,axiom_253,axiom_254,axiom_255,axiom_256,axiom_257,axiom_258,axiom_259,axiom_260,axiom_261,axiom_262,axiom_263,axiom_264,axiom_265,axiom_266,axiom_267,axiom_268,axiom_269,axiom_270,axiom_271,axiom_272,axiom_273,axiom_274,axiom_275,axiom_276,axiom_277,axiom_278,axiom_279,axiom_280,axiom_281,axiom_282,axiom_283,axiom_284,axiom_285] % 29.62/29.26 =============================================================== % 29.62/29.26 % 29.62/29.26 Combined formula: 286 axiom(s) => conjecture % 29.62/29.26 % 29.62/29.26 nanoCoP : % 29.62/29.26 % 2,328,536 inferences, 1.418 CPU in 1.419 seconds (100% CPU, 1642125 Lips) % 29.62/29.26 g4mic : % 29.62/29.26 % 100,012,918 inferences, 26.659 CPU in 26.658 seconds (100% CPU, 3751542 Lips) % 29.62/29.26 % 29.62/29.26 % Logic level: not determined (G4+ inference limit exceeded) % 29.62/29.26 % To get proofs (sequent calculus G4 and natural deduction), you can use G4+ at https://g4-mic.vidal-rosset.net/wasm/tinker % 29.62/29.26 % 29.62/29.26 % SZS output end Proof %------------------------------------------------------------------------------