%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : NUM926+1 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n008.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:08:19 PM UTC 2026 % Result : Theorem 5.65s 6.54s % Output : Proof 5.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM926+1 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.17/0.34 % Computer : n008.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 13:25:14 EDT 2026 % 0.17/0.34 % CPUTime : % 5.65/6.54 % SZS status Theorem % 5.65/6.54 % SZS output start Proof % 5.65/6.55 % 5.65/6.55 =============================================================== % 5.65/6.55 TPTP Problem: conj_0 (conjecture with 123 axiom(s)) % 5.65/6.55 Axioms: [fact_0_tpos,fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,fact_3_t__l__p,fact_4_p,fact_5_t,fact_6_qf1pt,fact_7_zadd__power2,fact_8_zadd__power3,fact_9_power2__sum,fact_10_power2__sum,fact_11_power2__eq__square__number__of,fact_12_power2__eq__square__number__of,fact_13_cube__square,fact_14_one__power2,fact_15_one__power2,fact_16_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,fact_17_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,fact_18_power2__eq__square,fact_19_power2__eq__square,fact_20_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,fact_21_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,fact_22_add__special_I2_J,fact_23_add__special_I3_J,fact_24_one__add__one__is__two,fact_25__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_,fact_26_zle__refl,fact_27_zle__linear,fact_28_zless__le,fact_29_zless__linear,fact_30_zle__trans,fact_31_zle__antisym,fact_32_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,fact_33_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,fact_34_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,fact_35_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,fact_36_zpower__zpower,fact_37_le__number__of__eq__not__less,fact_38_le__number__of__eq__not__less,fact_39_less__number__of,fact_40_le__number__of,fact_41_zadd__zless__mono,fact_42_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,fact_43_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,fact_44_zpower__zadd__distrib,fact_45_nat__mult__2,fact_46_nat__mult__2__right,fact_47_nat__1__add__1,fact_48_less__int__code_I16_J,fact_49_rel__simps_I17_J,fact_50_less__eq__int__code_I16_J,fact_51_rel__simps_I34_J,fact_52_rel__simps_I2_J,fact_53_less__int__code_I13_J,fact_54_rel__simps_I14_J,fact_55_rel__simps_I19_J,fact_56_less__eq__int__code_I13_J,fact_57_rel__simps_I31_J,fact_58_less__number__of__int__code,fact_59_less__eq__number__of__int__code,fact_60_zadd__strict__right__mono,fact_61_zadd__left__mono,fact_62_add__nat__number__of,fact_63_nat__numeral__1__eq__1,fact_64_Numeral1__eq1__nat,fact_65_rel__simps_I29_J,fact_66_rel__simps_I5_J,fact_67_less__eq__int__code_I15_J,fact_68_rel__simps_I33_J,fact_69_less__int__code_I14_J,fact_70_rel__simps_I15_J,fact_71_zless__imp__add1__zle,fact_72_add1__zle__eq,fact_73_zle__add1__eq__le,fact_74_zprime__2,fact_75_is__mult__sum2sq,fact_76_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,fact_77_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,fact_78_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,fact_79_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,fact_80_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,fact_81_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,fact_82_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,fact_83_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,fact_84_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,fact_85_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,fact_86_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,fact_87_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,fact_88_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,fact_89_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,fact_90_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,fact_91_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,fact_92_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,fact_93_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,fact_94_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,fact_95_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,fact_96_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,fact_97_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,fact_98_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,fact_99_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,fact_100_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,fact_101_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,fact_102_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,fact_103_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,fact_104_eq__number__of,fact_105_number__of__reorient,fact_106_number__of__reorient,fact_107_rel__simps_I51_J,fact_108_rel__simps_I48_J,fact_109_zmult__assoc,fact_110_zmult__commute,fact_111_number__of__is__id,fact_112_zadd__assoc,fact_113_zadd__left__commute,fact_114_zadd__commute,fact_115_rel__simps_I12_J,fact_116_less__int__code_I15_J,fact_117_rel__simps_I16_J,fact_118_rel__simps_I10_J,fact_119_rel__simps_I4_J,fact_120_rel__simps_I22_J,fact_121_less__eq__int__code_I14_J,fact_122_rel__simps_I32_J] % 5.65/6.55 =============================================================== % 5.65/6.55 % 5.65/6.55 Combined formula: 123 axiom(s) => conjecture % 5.65/6.55 % 5.65/6.55 % Equality/functions detected -> nanoCoP oracle mode % 5.65/6.55 nanoCoP : % 5.65/6.55 % 9,667,632 inferences, 4.899 CPU in 4.899 seconds (100% CPU, 1973235 Lips) % 5.65/6.55 % 5.65/6.55 % nanoCoP proof (equality/functions) % 5.65/6.55 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 5.65/6.55 % 5.65/6.55 % SZS output end Proof %------------------------------------------------------------------------------