%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : KRS154+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 : n027.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 35.15s 34.44s % Output : Proof 35.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS154+1 : TPTP v9.2.1. Released v3.1.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.16/0.34 % Computer : n027.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 11 12:26:20 EDT 2026 % 0.16/0.34 % CPUTime : % 35.15/34.44 % SZS status Theorem % 35.15/34.44 % SZS output start Proof % 35.15/34.44 % 35.15/34.44 =============================================================== % 35.15/34.44 TPTP Problem: the_axiom (conjecture with 169 axiom(s)) % 35.15/34.44 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] % 35.15/34.44 =============================================================== % 35.15/34.44 % 35.15/34.44 Combined formula: 169 axiom(s) => conjecture % 35.15/34.44 % 35.15/34.44 nanoCoP : % 35.15/34.44 % 352,409 inferences, 0.295 CPU in 0.295 seconds (100% CPU, 1194289 Lips) % 35.15/34.44 g4mic : % 35.15/34.44 % 100,008,806 inferences, 33.113 CPU in 33.112 seconds (100% CPU, 3020235 Lips) % 35.15/34.44 % 35.15/34.44 % Logic level: not determined (G4+ inference limit exceeded) % 35.15/34.44 % To get proofs (sequent calculus G4 and natural deduction), you can use G4+ at https://g4-mic.vidal-rosset.net/wasm/tinker % 35.15/34.44 % 35.15/34.44 % SZS output end Proof %------------------------------------------------------------------------------