%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : KRS153+1 : TPTP v9.2.1. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % Computer : n010.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:26 PM UTC 2026 % Result : Theorem 22.98s 23.07s % Output : Proof 22.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS153+1 : TPTP v9.2.1. Released v3.1.0. % 0.00/0.13 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.15/0.34 % Computer : n010.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Mon May 11 12:25:52 EDT 2026 % 0.15/0.34 % CPUTime : % 22.98/23.07 % SZS status Theorem % 22.98/23.07 % SZS output start Proof % 22.98/23.07 % 22.98/23.07 =============================================================== % 22.98/23.07 TPTP Problem: the_axiom (conjecture with 200 axiom(s)) % 22.98/23.07 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] % 22.98/23.07 =============================================================== % 22.98/23.07 % 22.98/23.07 Combined formula: 200 axiom(s) => conjecture % 22.98/23.07 % 22.98/23.07 nanoCoP : % 22.98/23.07 % 1,800,097 inferences, 1.040 CPU in 1.040 seconds (100% CPU, 1730182 Lips) % 22.98/23.07 g4mic : % 22.98/23.07 % 100,009,174 inferences, 20.601 CPU in 20.599 seconds (100% CPU, 4854688 Lips) % 22.98/23.07 % 22.98/23.07 % Logic level: not determined (G4+ inference limit exceeded) % 22.98/23.07 % To get proofs (sequent calculus G4 and natural deduction), you can use G4+ at https://g4-mic.vidal-rosset.net/wasm/tinker % 22.98/23.07 % 22.98/23.07 % SZS output end Proof %------------------------------------------------------------------------------