%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : NUM925+1 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % Computer : n010.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:18 PM UTC 2026 % Result : Theorem 0.71s 1.37s % Output : Proof 0.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM925+1 : TPTP v9.2.1. Released v5.3.0. % 0.13/0.12 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.17/0.33 % Computer : n010.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Mon May 11 13:23:52 EDT 2026 % 0.17/0.33 % CPUTime : % 0.71/1.37 % SZS status Theorem % 0.71/1.37 % SZS output start Proof % 0.71/1.37 % 0.71/1.37 =============================================================== % 0.71/1.37 TPTP Problem: conj_0 (conjecture with 106 axiom(s)) % 0.71/1.37 Axioms: [fact_0_n1pos,fact_1_t1,fact_2_sum__power2__eq__zero__iff,fact_3_one__power2,fact_4_one__power2,fact_5_zero__power2,fact_6_zero__power2,fact_7_zero__eq__power2,fact_8_add__special_I2_J,fact_9_add__special_I3_J,fact_10_one__add__one__is__two,fact_11_semiring__one__add__one__is__two,fact_12_semiring__one__add__one__is__two,fact_13_quartic__square__square,fact_14_power__0__left__number__of,fact_15_power__0__left__number__of,fact_16_semiring__norm_I110_J,fact_17_numeral__1__eq__1,fact_18_n0,fact_19_zless__linear,fact_20_less__number__of__int__code,fact_21_plus__numeral__code_I9_J,fact_22_less__number__of,fact_23_zero__is__num__zero,fact_24_zpower__int,fact_25_int__power,fact_26_zadd__int__left,fact_27_zadd__int,fact_28_int__1,fact_29_nat__number__of__Pls,fact_30_semiring__norm_I113_J,fact_31_int__eq__0__conv,fact_32_int__0,fact_33_nat__1__add__1,fact_34_less__int__code_I16_J,fact_35_rel__simps_I17_J,fact_36_rel__simps_I2_J,fact_37_less__int__code_I13_J,fact_38_rel__simps_I14_J,fact_39_zadd__strict__right__mono,fact_40_add__nat__number__of,fact_41_one__is__num__one,fact_42_nat__numeral__1__eq__1,fact_43_Numeral1__eq1__nat,fact_44_eq__number__of,fact_45_number__of__reorient,fact_46_number__of__reorient,fact_47_rel__simps_I51_J,fact_48_rel__simps_I48_J,fact_49_even__less__0__iff,fact_50_zadd__assoc,fact_51_zadd__left__commute,fact_52_zadd__commute,fact_53_int__int__eq,fact_54_less__special_I3_J,fact_55_less__special_I1_J,fact_56_rel__simps_I12_J,fact_57_less__int__code_I15_J,fact_58_rel__simps_I16_J,fact_59_rel__simps_I10_J,fact_60_rel__simps_I4_J,fact_61_bin__less__0__simps_I4_J,fact_62_bin__less__0__simps_I1_J,fact_63_bin__less__0__simps_I3_J,fact_64_int__0__less__1,fact_65_zless__add1__eq,fact_66_int__less__0__conv,fact_67_less__special_I4_J,fact_68_less__special_I2_J,fact_69_odd__less__0,fact_70_double__eq__0__iff,fact_71_rel__simps_I46_J,fact_72_rel__simps_I39_J,fact_73_rel__simps_I50_J,fact_74_rel__simps_I49_J,fact_75_rel__simps_I44_J,fact_76_rel__simps_I38_J,fact_77_Bit0__Pls,fact_78_Pls__def,fact_79_int__0__neq__1,fact_80_add__Pls__right,fact_81_add__Pls,fact_82_add__Bit0__Bit0,fact_83_Bit0__def,fact_84_zadd__0__right,fact_85_zadd__0,fact_86_semiring__numeral__0__eq__0,fact_87_semiring__numeral__0__eq__0,fact_88_number__of__Pls,fact_89_semiring__norm_I112_J,fact_90_add__numeral__0,fact_91_add__numeral__0__right,fact_92_power__eq__0__iff__number__of,fact_93_power__eq__0__iff__number__of,fact_94_add__number__of__left,fact_95_add__number__of__eq,fact_96_number__of__add,fact_97_add__Bit1__Bit0,fact_98_add__Bit0__Bit1,fact_99_Bit1__def,fact_100_odd__nonzero,fact_101_number__of__int,fact_102_number__of__int,fact_103_zero__less__power2,fact_104_power2__less__0,fact_105_sum__power2__gt__zero__iff] % 0.71/1.37 =============================================================== % 0.71/1.37 % 0.71/1.37 Combined formula: 106 axiom(s) => conjecture % 0.71/1.37 % 0.71/1.37 % Equality/functions detected -> nanoCoP oracle mode % 0.71/1.37 nanoCoP : % 0.71/1.37 % 244,337 inferences, 0.175 CPU in 0.175 seconds (100% CPU, 1394430 Lips) % 0.71/1.37 % 0.71/1.37 % nanoCoP proof (equality/functions) % 0.71/1.37 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 0.71/1.37 % 0.71/1.37 % SZS output end Proof %------------------------------------------------------------------------------