%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SWW229+1 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n032.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 : 600s % DateTime : Thu Jul 21 02:21:23 EDT 2022 % Result : Theorem 2.62s 2.82s % Output : Proof 2.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : SWW229+1 : TPTP v8.1.0. Released v5.2.0. % 0.02/0.09 % Command : run_zenon %s %d % 0.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 600 % 0.08/0.28 % DateTime : Sun Jun 5 19:35:04 EDT 2022 % 0.08/0.28 % CPUTime : % 2.62/2.82 (* PROOF-FOUND *) % 2.62/2.82 % SZS status Theorem % 2.62/2.82 (* BEGIN-PROOF *) % 2.62/2.82 % SZS output start Proof % 2.62/2.82 Theorem conj_0 : (c_Orderings_Oord__class_Oless__eq (tc_RealDef_Oreal) (c_Groups_Oabs__class_Oabs (tc_RealDef_Oreal) (c_Groups_Ominus__class_Ominus (tc_RealDef_Oreal) (c_RealVector_Onorm__class_Onorm (tc_Complex_Ocomplex) (hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_p)) (v_g____ (hAPP (v_f____) (c_Groups_Oplus__class_Oplus (tc_Nat_Onat) (v_N1____) (v_N2____)))))) (c_RealVector_Onorm__class_Onorm (tc_Complex_Ocomplex) (hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_p)) (v_z____))))) (c_RealVector_Onorm__class_Onorm (tc_Complex_Ocomplex) (c_Groups_Ominus__class_Ominus (tc_Complex_Ocomplex) (hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_p)) (v_g____ (hAPP (v_f____) (c_Groups_Oplus__class_Oplus (tc_Nat_Onat) (v_N1____) (v_N2____))))) (hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_p)) (v_z____))))). % 2.62/2.82 Proof. % 2.62/2.82 apply NNPP. intro zenon_G. % 2.62/2.82 generalize (fact_norm__triangle__ineq3 (hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_p)) (v_z____))). zenon_intro zenon_H4be. % 2.62/2.82 generalize (zenon_H4be (hAPP (c_Polynomial_Opoly (tc_Complex_Ocomplex) (v_p)) (v_g____ (hAPP (v_f____) (c_Groups_Oplus__class_Oplus (tc_Nat_Onat) (v_N1____) (v_N2____)))))). zenon_intro zenon_H4bf. % 2.62/2.82 generalize (zenon_H4bf (tc_Complex_Ocomplex)). zenon_intro zenon_H4c0. % 2.62/2.82 apply (zenon_imply_s _ _ zenon_H4c0); [ zenon_intro zenon_H4c2 | zenon_intro zenon_H4c1 ]. % 2.62/2.82 exact (zenon_H4c2 arity_Complex__Ocomplex__RealVector_Oreal__normed__vector). % 2.62/2.82 exact (zenon_G zenon_H4c1). % 2.62/2.82 Qed. % 2.62/2.82 % SZS output end Proof % 2.62/2.82 (* END-PROOF *) % 2.62/2.82 nodes searched: 12457 % 2.62/2.82 max branch formulas: 12847 % 2.62/2.82 proof nodes created: 29 % 2.62/2.82 formulas created: 397732 % 2.62/2.82 %------------------------------------------------------------------------------