%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW485_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % 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 : Fri Oct 3 08:06:21 PM UTC 2025 % Result : Theorem 12.56s 12.79s % Output : Proof 12.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.15 % Problem : SWW485_5 : TPTP v9.2.0. Released v6.0.0. % 0.07/0.17 % Command : duper %s % 0.13/0.41 % Computer : n001.cluster.edu % 0.13/0.41 % Model : x86_64 x86_64 % 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.41 % Memory : 8042.1875MB % 0.13/0.41 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.41 % CPULimit : 300 % 0.13/0.41 % WCLimit : 300 % 0.13/0.41 % DateTime : Thu Oct 2 10:46:38 EDT 2025 % 0.13/0.41 % CPUTime : % 12.56/12.79 SZS status Theorem for theBenchmark.p % 12.56/12.79 SZS output start Proof for theBenchmark.p % 12.56/12.79 Clause #0 (by assumption #[]): Eq % 12.56/12.79 (Exists fun M3 => % 12.56/12.79 And (ord_less real (zero_zero real) M3) % 12.56/12.79 (∀ (Z2 : complex), % 12.56/12.79 ord_less_eq real (norm_norm complex Z2) r → % 12.56/12.79 ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) Z2)) M3)) % 12.56/12.79 True % 12.56/12.79 Clause #130 (by assumption #[]): Eq % 12.56/12.79 (∀ (M : real), % 12.56/12.79 (∀ (Z : complex), % 12.56/12.79 ord_less_eq real (norm_norm complex Z) r → % 12.56/12.79 ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) Z)) M) → % 12.56/12.79 thesis) % 12.56/12.79 True % 12.56/12.79 Clause #131 (by assumption #[]): Eq (Not thesis) True % 12.56/12.79 Clause #132 (by clausification #[131]): Eq thesis False % 12.56/12.79 Clause #133 (by clausification #[0]): ∀ (a : real), % 12.56/12.79 Eq % 12.56/12.79 (And (ord_less real (zero_zero real) (skS.0 0 a)) % 12.56/12.79 (∀ (Z2 : complex), % 12.56/12.79 ord_less_eq real (norm_norm complex Z2) r → % 12.56/12.79 ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) Z2)) (skS.0 0 a))) % 12.56/12.79 True % 12.56/12.79 Clause #134 (by clausification #[133]): ∀ (a : real), % 12.56/12.79 Eq % 12.56/12.79 (∀ (Z2 : complex), % 12.56/12.79 ord_less_eq real (norm_norm complex Z2) r → % 12.56/12.79 ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) Z2)) (skS.0 0 a)) % 12.56/12.79 True % 12.56/12.79 Clause #136 (by clausification #[134]): ∀ (a : complex) (a_1 : real), % 12.56/12.79 Eq % 12.56/12.79 (ord_less_eq real (norm_norm complex a) r → % 12.56/12.79 ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) a)) (skS.0 0 a_1)) % 12.56/12.79 True % 12.56/12.79 Clause #137 (by clausification #[136]): ∀ (a : complex) (a_1 : real), % 12.56/12.79 Or (Eq (ord_less_eq real (norm_norm complex a) r) False) % 12.56/12.79 (Eq (ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) a)) (skS.0 0 a_1)) True) % 12.56/12.79 Clause #169 (by clausification #[130]): ∀ (a : real), % 12.56/12.79 Eq % 12.56/12.79 ((∀ (Z : complex), % 12.56/12.79 ord_less_eq real (norm_norm complex Z) r → % 12.56/12.79 ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) Z)) a) → % 12.56/12.79 thesis) % 12.56/12.79 True % 12.56/12.79 Clause #170 (by clausification #[169]): ∀ (a : real), % 12.56/12.79 Or % 12.56/12.79 (Eq % 12.56/12.79 (∀ (Z : complex), % 12.56/12.79 ord_less_eq real (norm_norm complex Z) r → % 12.56/12.79 ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) Z)) a) % 12.56/12.79 False) % 12.56/12.79 (Eq thesis True) % 12.56/12.79 Clause #171 (by clausification #[170]): ∀ (a : real) (a_1 : complex), % 12.56/12.79 Or (Eq thesis True) % 12.56/12.79 (Eq % 12.56/12.79 (Not % 12.56/12.79 (ord_less_eq real (norm_norm complex (skS.0 1 a a_1)) r → % 12.56/12.79 ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) (skS.0 1 a a_1))) a)) % 12.56/12.79 True) % 12.56/12.79 Clause #172 (by clausification #[171]): ∀ (a : real) (a_1 : complex), % 12.56/12.79 Or (Eq thesis True) % 12.56/12.79 (Eq % 12.56/12.79 (ord_less_eq real (norm_norm complex (skS.0 1 a a_1)) r → % 12.56/12.79 ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) (skS.0 1 a a_1))) a) % 12.56/12.79 False) % 12.56/12.79 Clause #173 (by clausification #[172]): ∀ (a : real) (a_1 : complex), Or (Eq thesis True) (Eq (ord_less_eq real (norm_norm complex (skS.0 1 a a_1)) r) True) % 12.56/12.79 Clause #174 (by clausification #[172]): ∀ (a : real) (a_1 : complex), % 12.56/12.79 Or (Eq thesis True) % 12.56/12.79 (Eq (ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) (skS.0 1 a a_1))) a) False) % 12.56/12.79 Clause #175 (by forward demodulation #[173, 132]): ∀ (a : real) (a_1 : complex), Or (Eq False True) (Eq (ord_less_eq real (norm_norm complex (skS.0 1 a a_1)) r) True) % 12.56/12.79 Clause #176 (by clausification #[175]): ∀ (a : real) (a_1 : complex), Eq (ord_less_eq real (norm_norm complex (skS.0 1 a a_1)) r) True % 12.56/12.79 Clause #177 (by superposition #[176, 137]): ∀ (a : real) (a_1 : complex) (a_2 : real), % 12.56/12.79 Or (Eq True False) % 12.56/12.79 (Eq (ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) (skS.0 1 a a_1))) (skS.0 0 a_2)) % 12.56/12.79 True) % 12.56/12.79 Clause #2027 (by forward demodulation #[174, 132]): ∀ (a : real) (a_1 : complex), % 12.56/12.79 Or (Eq False True) % 12.56/12.79 (Eq (ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) (skS.0 1 a a_1))) a) False) % 12.56/12.79 Clause #2028 (by clausification #[2027]): ∀ (a : real) (a_1 : complex), % 12.56/12.79 Eq (ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) (skS.0 1 a a_1))) a) False % 12.56/12.80 Clause #2060 (by clausification #[177]): ∀ (a : real) (a_1 : complex) (a_2 : real), % 12.56/12.80 Eq (ord_less_eq real (norm_norm complex (aa complex complex (poly complex cs) (skS.0 1 a a_1))) (skS.0 0 a_2)) True % 12.56/12.80 Clause #2061 (by superposition #[2060, 2028]): Eq True False % 12.56/12.80 Clause #2063 (by clausification #[2061]): False % 12.56/12.80 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------