%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : KRS149+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 : n001.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 11.67s 11.70s % Output : Proof 11.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS149+1 : TPTP v9.2.1. Released v3.1.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.17/0.34 % Computer : n001.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 12:26:34 EDT 2026 % 0.17/0.34 % CPUTime : % 11.67/11.70 % SZS status Theorem % 11.67/11.70 % SZS output start Proof % 11.67/11.71 % 11.67/11.71 =============================================================== % 11.67/11.71 TPTP Problem: the_axiom (conjecture with 125 axiom(s)) % 11.67/11.71 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] % 11.67/11.71 =============================================================== % 11.67/11.71 % 11.67/11.71 Combined formula: 125 axiom(s) => conjecture % 11.67/11.71 % 11.67/11.71 nanoCoP : % 11.67/11.71 % 208,891 inferences, 0.195 CPU in 0.195 seconds (100% CPU, 1068794 Lips) % 11.67/11.71 g4mic : % 11.67/11.71 % 32,091,852 inferences, 10.563 CPU in 10.563 seconds (100% CPU, 3038269 Lips) % 11.67/11.71 % 11.67/11.71 % Logic level: valid in classical logic. % 11.67/11.71 % To get proofs (sequent calculus G4 and natural deduction), you can use G4+ at https://g4-mic.vidal-rosset.net/wasm/tinker % 11.67/11.71 % 11.67/11.71 % SZS output end Proof %------------------------------------------------------------------------------