%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : NUM328+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:07:10 PM UTC 2026 % Result : Theorem 0.77s 1.38s % Output : Proof 0.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM328+1 : TPTP v9.2.1. Released v3.1.0. % 0.12/0.13 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.16/0.34 % Computer : n001.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 13:18:19 EDT 2026 % 0.16/0.34 % CPUTime : % 0.77/1.38 % SZS status Theorem % 0.77/1.38 % SZS output start Proof % 0.77/1.38 % 0.77/1.38 =============================================================== % 0.77/1.38 TPTP Problem: sum_something_anotherthing_firstthing (conjecture with 401 axiom(s)) % 0.77/1.38 Axioms: [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,sum_entry_point_pos_pos,sum_entry_point_neg_neg,sum_entry_point_pos_neg_1,sum_entry_point_pos_neg_2,sum_entry_point_posx_negx,sum_entry_point_neg_pos,unique_sum,unique_LHS,unique_RHS,minus_entry_point,add_digit_digit_digit,add_digit_digit_rdn,add_digit_rdn_rdn,add_rdn_rdn_rdn,add_rdn_digit_rdn,rdn_digit_add_n0_n0_n0_n0,rdn_digit_add_n0_n1_n1_n0,rdn_digit_add_n0_n2_n2_n0,rdn_digit_add_n0_n3_n3_n0,rdn_digit_add_n0_n4_n4_n0,rdn_digit_add_n0_n5_n5_n0,rdn_digit_add_n0_n6_n6_n0,rdn_digit_add_n0_n7_n7_n0,rdn_digit_add_n0_n8_n8_n0,rdn_digit_add_n0_n9_n9_n0,rdn_digit_add_n1_n0_n1_n0,rdn_digit_add_n1_n1_n2_n0,rdn_digit_add_n1_n2_n3_n0,rdn_digit_add_n1_n3_n4_n0,rdn_digit_add_n1_n4_n5_n0,rdn_digit_add_n1_n5_n6_n0,rdn_digit_add_n1_n6_n7_n0,rdn_digit_add_n1_n7_n8_n0,rdn_digit_add_n1_n8_n9_n0,rdn_digit_add_n1_n9_n0_n1,rdn_digit_add_n2_n0_n2_n0,rdn_digit_add_n2_n1_n3_n0,rdn_digit_add_n2_n2_n4_n0,rdn_digit_add_n2_n3_n5_n0,rdn_digit_add_n2_n4_n6_n0,rdn_digit_add_n2_n5_n7_n0,rdn_digit_add_n2_n6_n8_n0,rdn_digit_add_n2_n7_n9_n0,rdn_digit_add_n2_n8_n0_n1,rdn_digit_add_n2_n9_n1_n1,rdn_digit_add_n3_n0_n3_n0,rdn_digit_add_n3_n1_n4_n0,rdn_digit_add_n3_n2_n5_n0,rdn_digit_add_n3_n3_n6_n0,rdn_digit_add_n3_n4_n7_n0,rdn_digit_add_n3_n5_n8_n0,rdn_digit_add_n3_n6_n9_n0,rdn_digit_add_n3_n7_n0_n1,rdn_digit_add_n3_n8_n1_n1,rdn_digit_add_n3_n9_n2_n1,rdn_digit_add_n4_n0_n4_n0,rdn_digit_add_n4_n1_n5_n0,rdn_digit_add_n4_n2_n6_n0,rdn_digit_add_n4_n3_n7_n0,rdn_digit_add_n4_n4_n8_n0,rdn_digit_add_n4_n5_n9_n0,rdn_digit_add_n4_n6_n0_n1,rdn_digit_add_n4_n7_n1_n1,rdn_digit_add_n4_n8_n2_n1,rdn_digit_add_n4_n9_n3_n1,rdn_digit_add_n5_n0_n5_n0,rdn_digit_add_n5_n1_n6_n0,rdn_digit_add_n5_n2_n7_n0,rdn_digit_add_n5_n3_n8_n0,rdn_digit_add_n5_n4_n9_n0,rdn_digit_add_n5_n5_n0_n1,rdn_digit_add_n5_n6_n1_n1,rdn_digit_add_n5_n7_n2_n1,rdn_digit_add_n5_n8_n3_n1,rdn_digit_add_n5_n9_n4_n1,rdn_digit_add_n6_n0_n6_n0,rdn_digit_add_n6_n1_n7_n0,rdn_digit_add_n6_n2_n8_n0,rdn_digit_add_n6_n3_n9_n0,rdn_digit_add_n6_n4_n0_n1,rdn_digit_add_n6_n5_n1_n1,rdn_digit_add_n6_n6_n2_n1,rdn_digit_add_n6_n7_n3_n1,rdn_digit_add_n6_n8_n4_n1,rdn_digit_add_n6_n9_n5_n1,rdn_digit_add_n7_n0_n7_n0,rdn_digit_add_n7_n1_n8_n0,rdn_digit_add_n7_n2_n9_n0,rdn_digit_add_n7_n3_n0_n1,rdn_digit_add_n7_n4_n1_n1,rdn_digit_add_n7_n5_n2_n1,rdn_digit_add_n7_n6_n3_n1,rdn_digit_add_n7_n7_n4_n1,rdn_digit_add_n7_n8_n5_n1,rdn_digit_add_n7_n9_n6_n1,rdn_digit_add_n8_n0_n8_n0,rdn_digit_add_n8_n1_n9_n0,rdn_digit_add_n8_n2_n0_n1,rdn_digit_add_n8_n3_n1_n1,rdn_digit_add_n8_n4_n2_n1,rdn_digit_add_n8_n5_n3_n1,rdn_digit_add_n8_n6_n4_n1,rdn_digit_add_n8_n7_n5_n1,rdn_digit_add_n8_n8_n6_n1,rdn_digit_add_n8_n9_n7_n1,rdn_digit_add_n9_n0_n9_n0,rdn_digit_add_n9_n1_n0_n1,rdn_digit_add_n9_n2_n1_n1,rdn_digit_add_n9_n3_n2_n1,rdn_digit_add_n9_n4_n3_n1,rdn_digit_add_n9_n5_n4_n1,rdn_digit_add_n9_n6_n5_n1,rdn_digit_add_n9_n7_n6_n1,rdn_digit_add_n9_n8_n7_n1,rdn_digit_add_n9_n9_n8_n1] % 0.77/1.38 =============================================================== % 0.77/1.38 % 0.77/1.38 Combined formula: 401 axiom(s) => conjecture % 0.77/1.38 % 0.77/1.38 % Equality/functions detected -> nanoCoP oracle mode % 0.77/1.38 nanoCoP : % 0.77/1.38 % 212,981 inferences, 0.152 CPU in 0.152 seconds (100% CPU, 1399719 Lips) % 0.77/1.38 % 0.77/1.38 % nanoCoP proof (equality/functions) % 0.77/1.38 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 0.77/1.38 % 0.77/1.38 % SZS output end Proof %------------------------------------------------------------------------------