%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : AGT015+1 : TPTP v9.2.1. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n018.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:27 PM UTC 2026 % Result : Theorem 0.84s 1.37s % Output : Proof 0.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : AGT015+1 : TPTP v9.2.1. Bugfixed v3.1.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.16/0.34 % Computer : n018.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 14:56:48 EDT 2026 % 0.16/0.34 % CPUTime : % 0.84/1.37 % SZS status Theorem % 0.84/1.38 % SZS output start Proof % 0.84/1.38 % 0.84/1.38 =============================================================== % 0.84/1.38 TPTP Problem: query_15 (conjecture with 555 axiom(s)) % 0.84/1.38 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,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] % 0.84/1.38 =============================================================== % 0.84/1.38 % 0.84/1.38 Combined formula: 555 axiom(s) => conjecture % 0.84/1.38 % 0.84/1.38 % Equality/functions detected -> nanoCoP oracle mode % 0.84/1.38 nanoCoP : % 0.84/1.38 % 200,843 inferences, 0.208 CPU in 0.209 seconds (100% CPU, 963922 Lips) % 0.84/1.38 % 0.84/1.38 % nanoCoP proof (equality/functions) % 0.84/1.38 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 0.84/1.38 % 0.84/1.38 % SZS output end Proof %------------------------------------------------------------------------------