%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : AGT015+2 : TPTP v9.2.1. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n021.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 06:54:28 PM UTC 2026 % Result : Theorem 1.07s 1.36s % Output : Proof 1.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : AGT015+2 : TPTP v9.2.1. Bugfixed v3.1.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.15/0.33 % Computer : n021.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 11 14:57:46 EDT 2026 % 0.15/0.33 % CPUTime : % 1.07/1.36 % SZS status Theorem % 1.07/1.36 % SZS output start Proof % 1.07/1.36 % 1.07/1.36 =============================================================== % 1.07/1.36 TPTP Problem: query_15 (conjecture with 922 axiom(s)) % 1.07/1.36 Axioms: [a1_1,a1_2,a1_3,a1_4,a1_5,a1_6,a1_7,a2_1,a2_2,a2_3,a2_4,a2_5,a2_6,a2_7,a2_8,a2_9,a2_10,a2_11,a2_12,a2_13,event_1,event_2,event_3,event_4,event_5,event_6,event_7,event_8,event_9,event_10,event_11,event_12,event_13,event_14,event_15,event_16,event_17,event_18,event_19,event_20,event_21,event_22,event_23,event_24,event_25,event_26,event_27,event_28,event_29,event_30,event_31,event_32,event_33,event_34,event_35,event_36,event_37,event_38,event_39,event_40,event_41,event_42,event_43,event_44,event_45,event_46,event_47,event_48,event_49,event_50,event_51,event_52,event_53,event_54,event_55,event_56,event_57,event_58,event_59,event_60,event_61,event_62,event_63,event_64,event_65,event_66,event_67,event_68,event_69,event_70,event_71,event_72,event_73,event_74,event_75,event_76,event_77,event_78,event_79,event_80,event_81,event_82,event_83,event_84,event_85,event_86,event_87,event_88,event_89,event_90,event_91,event_92,event_93,event_94,event_95,event_96,event_97,event_98,event_99,event_100,event_101,event_102,event_103,event_104,event_105,event_106,event_107,event_108,event_109,event_110,event_111,event_112,event_113,event_114,event_115,event_116,event_117,event_118,event_119,event_120,event_121,event_122,event_123,event_124,event_125,event_126,event_127,event_128,event_129,event_130,event_131,event_132,event_133,event_134,event_135,event_136,event_137,event_138,event_139,event_140,event_141,event_142,event_143,event_144,event_145,event_146,event_147,event_148,event_149,event_150,event_151,event_152,event_153,event_154,event_155,event_156,event_157,event_158,event_159,event_160,event_161,event_162,event_163,event_164,event_165,event_166,event_167,event_168,event_169,event_170,event_171,event_172,event_173,event_174,event_175,event_176,event_177,event_178,event_179,event_180,event_181,event_182,event_183,event_184,event_185,event_186,event_187,event_188,event_189,event_190,event_191,event_192,event_193,event_194,event_195,event_196,event_197,event_198,event_199,event_200,event_201,event_202,event_203,event_204,event_205,event_206,event_207,event_208,event_209,event_210,event_211,event_212,event_213,event_214,event_215,event_216,event_217,event_218,event_219,event_220,event_221,event_222,event_223,event_224,event_225,event_226,event_227,event_228,event_229,event_230,event_231,event_232,event_233,event_234,event_235,event_236,event_237,event_238,event_239,event_240,event_241,event_242,event_243,event_244,event_245,event_246,event_247,event_248,event_249,deduced_1,deduced_2,deduced_3,deduced_4,deduced_5,deduced_6,deduced_7,deduced_8,deduced_9,deduced_10,deduced_11,deduced_12,deduced_13,deduced_14,deduced_15,deduced_16,deduced_17,deduced_18,deduced_19,deduced_20,deduced_21,deduced_22,deduced_23,deduced_24,deduced_25,deduced_26,deduced_27,deduced_28,deduced_29,deduced_30,deduced_31,deduced_32,deduced_33,deduced_34,deduced_35,deduced_36,deduced_37,deduced_38,deduced_39,deduced_40,deduced_41,deduced_42,deduced_43,deduced_44,deduced_45,deduced_46,deduced_47,deduced_48,deduced_49,deduced_50,deduced_51,deduced_52,deduced_53,deduced_54,deduced_55,deduced_56,deduced_57,deduced_58,deduced_59,deduced_60,deduced_61,deduced_62,deduced_63,deduced_64,deduced_65,deduced_66,deduced_67,deduced_68,deduced_69,deduced_70,deduced_71,deduced_72,deduced_73,deduced_74,deduced_75,deduced_76,deduced_77,deduced_78,deduced_79,deduced_80,deduced_81,deduced_82,deduced_83,deduced_84,deduced_85,deduced_86,deduced_87,deduced_88,deduced_89,deduced_90,deduced_91,deduced_92,deduced_93,deduced_94,deduced_95,deduced_96,deduced_97,deduced_98,deduced_99,deduced_100,deduced_101,deduced_102,deduced_103,deduced_104,deduced_105,deduced_106,deduced_107,deduced_108,deduced_109,deduced_110,deduced_111,deduced_112,deduced_113,deduced_114,deduced_115,deduced_116,deduced_117,deduced_118,deduced_119,deduced_120,deduced_121,deduced_122,deduced_123,deduced_124,deduced_125,deduced_126,deduced_127,deduced_128,deduced_129,deduced_130,deduced_131,deduced_132,deduced_133,deduced_134,deduced_135,deduced_136,deduced_137,deduced_138,deduced_139,deduced_140,deduced_141,deduced_142,deduced_143,deduced_144,deduced_145,deduced_146,deduced_147,deduced_148,deduced_149,deduced_150,deduced_151,deduced_152,deduced_153,deduced_154,deduced_155,deduced_156,deduced_157,deduced_158,deduced_159,deduced_160,deduced_161,deduced_162,deduced_163,deduced_164,deduced_165,deduced_166,deduced_167,deduced_168,deduced_169,deduced_170,deduced_171,deduced_172,deduced_173,deduced_174,deduced_175,deduced_176,deduced_177,deduced_178,deduced_179,deduced_180,deduced_181,deduced_182,deduced_183,deduced_184,deduced_185,deduced_186,deduced_187,deduced_188,deduced_189,deduced_190,deduced_191,deduced_192,deduced_193,deduced_194,deduced_195,deduced_196,deduced_197,deduced_198,deduced_199,deduced_200,deduced_201,deduced_202,deduced_203,deduced_204,deduced_205,deduced_206,deduced_207,deduced_208,deduced_209,deduced_210,deduced_211,deduced_212,deduced_213,deduced_214,deduced_215,deduced_216,deduced_217,deduced_218,deduced_219,deduced_220,deduced_221,deduced_222,deduced_223,deduced_224,deduced_225,deduced_226,deduced_227,deduced_228,deduced_229,deduced_230,deduced_231,deduced_232,deduced_233,deduced_234,deduced_235,deduced_236,deduced_237,deduced_238,deduced_239,deduced_240,deduced_241,deduced_242,deduced_243,deduced_244,deduced_245,deduced_246,deduced_247,deduced_248,deduced_249,deduced_250,deduced_251,deduced_252,deduced_253,deduced_254,deduced_255,deduced_256,deduced_257,deduced_258,deduced_259,deduced_260,deduced_261,deduced_262,deduced_263,deduced_264,deduced_265,deduced_266,deduced_267,deduced_268,deduced_269,deduced_270,deduced_271,deduced_272,deduced_273,deduced_274,deduced_275,deduced_276,deduced_277,deduced_278,deduced_279,deduced_280,deduced_281,deduced_282,deduced_283,deduced_284,deduced_285,deduced_286,deduced_287,deduced_288,deduced_289,deduced_290,deduced_291,deduced_292,deduced_293,deduced_294,deduced_295,deduced_296,deduced_297,deduced_298,deduced_299,deduced_300,deduced_301,deduced_302,deduced_303,deduced_304,deduced_305,deduced_306,deduced_307,deduced_308,deduced_309,deduced_310,deduced_311,deduced_312,deduced_313,deduced_314,deduced_315,deduced_316,deduced_317,deduced_318,deduced_319,deduced_320,deduced_321,deduced_322,deduced_323,deduced_324,deduced_325,deduced_326,deduced_327,deduced_328,deduced_329,deduced_330,deduced_331,deduced_332,deduced_333,deduced_334,deduced_335,deduced_336,deduced_337,deduced_338,deduced_339,deduced_340,deduced_341,deduced_342,deduced_343,deduced_344,deduced_345,deduced_346,deduced_347,deduced_348,deduced_349,deduced_350,deduced_351,deduced_352,deduced_353,deduced_354,deduced_355,deduced_356,deduced_357,deduced_358,deduced_359,deduced_360,deduced_361,deduced_362,deduced_363,deduced_364,deduced_365,deduced_366,deduced_367,rdn0,rdn1,rdn2,rdn3,rdn4,rdn5,rdn6,rdn7,rdn8,rdn9,rdn10,rdn11,rdn12,rdn13,rdn14,rdn15,rdn16,rdn17,rdn18,rdn19,rdn20,rdn21,rdn22,rdn23,rdn24,rdn25,rdn26,rdn27,rdn28,rdn29,rdn30,rdn31,rdn32,rdn33,rdn34,rdn35,rdn36,rdn37,rdn38,rdn39,rdn40,rdn41,rdn42,rdn43,rdn44,rdn45,rdn46,rdn47,rdn48,rdn49,rdn50,rdn51,rdn52,rdn53,rdn54,rdn55,rdn56,rdn57,rdn58,rdn59,rdn60,rdn61,rdn62,rdn63,rdn64,rdn65,rdn66,rdn67,rdn68,rdn69,rdn70,rdn71,rdn72,rdn73,rdn74,rdn75,rdn76,rdn77,rdn78,rdn79,rdn80,rdn81,rdn82,rdn83,rdn84,rdn85,rdn86,rdn87,rdn88,rdn89,rdn90,rdn91,rdn92,rdn93,rdn94,rdn95,rdn96,rdn97,rdn98,rdn99,rdn100,rdn101,rdn102,rdn103,rdn104,rdn105,rdn106,rdn107,rdn108,rdn109,rdn110,rdn111,rdn112,rdn113,rdn114,rdn115,rdn116,rdn117,rdn118,rdn119,rdn120,rdn121,rdn122,rdn123,rdn124,rdn125,rdn126,rdn127,rdnn1,rdnn2,rdnn3,rdnn4,rdnn5,rdnn6,rdnn7,rdnn8,rdnn9,rdnn10,rdnn11,rdnn12,rdnn13,rdnn14,rdnn15,rdnn16,rdnn17,rdnn18,rdnn19,rdnn20,rdnn21,rdnn22,rdnn23,rdnn24,rdnn25,rdnn26,rdnn27,rdnn28,rdnn29,rdnn30,rdnn31,rdnn32,rdnn33,rdnn34,rdnn35,rdnn36,rdnn37,rdnn38,rdnn39,rdnn40,rdnn41,rdnn42,rdnn43,rdnn44,rdnn45,rdnn46,rdnn47,rdnn48,rdnn49,rdnn50,rdnn51,rdnn52,rdnn53,rdnn54,rdnn55,rdnn56,rdnn57,rdnn58,rdnn59,rdnn60,rdnn61,rdnn62,rdnn63,rdnn64,rdnn65,rdnn66,rdnn67,rdnn68,rdnn69,rdnn70,rdnn71,rdnn72,rdnn73,rdnn74,rdnn75,rdnn76,rdnn77,rdnn78,rdnn79,rdnn80,rdnn81,rdnn82,rdnn83,rdnn84,rdnn85,rdnn86,rdnn87,rdnn88,rdnn89,rdnn90,rdnn91,rdnn92,rdnn93,rdnn94,rdnn95,rdnn96,rdnn97,rdnn98,rdnn99,rdnn100,rdnn101,rdnn102,rdnn103,rdnn104,rdnn105,rdnn106,rdnn107,rdnn108,rdnn109,rdnn110,rdnn111,rdnn112,rdnn113,rdnn114,rdnn115,rdnn116,rdnn117,rdnn118,rdnn119,rdnn120,rdnn121,rdnn122,rdnn123,rdnn124,rdnn125,rdnn126,rdnn127,rdnn128,rdn_digit1,rdn_digit2,rdn_digit3,rdn_digit4,rdn_digit5,rdn_digit6,rdn_digit7,rdn_digit8,rdn_digit9,rdn_positive_less01,rdn_positive_less12,rdn_positive_less23,rdn_positive_less34,rdn_positive_less45,rdn_positive_less56,rdn_positive_less67,rdn_positive_less78,rdn_positive_less89,rdn_positive_less_transitivity,rdn_positive_less_multi_digit_high,rdn_positive_less_multi_digit_low,rdn_extra_digits_positive_less,rdn_non_zero_by_digit,rdn_non_zero_by_structure,less_entry_point_pos_pos,less_entry_point_neg_pos,less_entry_point_neg_neg,less_property,less_or_equal,less_successor] % 1.07/1.37 =============================================================== % 1.07/1.37 % 1.07/1.37 Combined formula: 922 axiom(s) => conjecture % 1.07/1.37 % 1.07/1.37 % Equality/functions detected -> nanoCoP oracle mode % 1.07/1.37 nanoCoP : % 1.07/1.37 % 274,284 inferences, 0.373 CPU in 0.373 seconds (100% CPU, 735057 Lips) % 1.07/1.37 % 1.07/1.37 % nanoCoP proof (equality/functions) % 1.07/1.37 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 1.07/1.37 % 1.07/1.37 % SZS output end Proof %------------------------------------------------------------------------------