%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ANA122^1 : TPTP v9.2.0. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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 07:44:35 PM UTC 2025 % Result : Theorem 173.20s 173.41s % Output : Proof 174.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ANA122^1 : TPTP v9.2.0. Released v7.0.0. % 0.03/0.14 % Command : duper %s % 0.14/0.35 % Computer : n020.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 22:03:08 EDT 2025 % 0.14/0.35 % CPUTime : % 173.20/173.41 SZS status Theorem for theBenchmark.p % 173.20/173.41 SZS output start Proof for theBenchmark.p % 173.20/173.41 Clause #0 (by assumption #[]): Eq % 173.20/173.41 (∀ (A : «type/realax/real»), % 173.20/173.41 Eq % 173.20/173.41 («const/realax/real_mul» A % 173.20/173.41 («const/realax/real_of_num» («const/nums/NUMERAL» («const/nums/BIT1» «const/nums/_0»)))) % 173.20/173.41 A) % 173.20/173.41 True % 173.20/173.41 Clause #1 (by assumption #[]): Eq % 173.20/173.41 (∀ (A : «type/realax/real»), % 173.20/173.41 Eq («const/realax/real_pow» A («const/nums/NUMERAL» «const/nums/_0»)) % 173.20/173.41 («const/realax/real_of_num» («const/nums/NUMERAL» («const/nums/BIT1» «const/nums/_0»)))) % 173.20/173.41 True % 173.20/173.41 Clause #2 (by assumption #[]): Eq % 173.20/173.41 (∀ (A : «type/nums/num» → «type/realax/real») (A0 : «type/nums/num»), % 173.20/173.41 Eq («const/iterate/sum» «type/nums/num» («const/iterate/..» A0 A0) A) (A A0)) % 173.20/173.41 True % 173.20/173.41 Clause #3 (by assumption #[]): Eq % 173.20/173.41 (∀ (A : «type/realax/real» → «type/realax/real»), % 173.20/173.41 Eq («const/iterate/polynomial_function» A) % 173.20/173.41 (Exists fun A0 => % 173.20/173.41 Exists fun A1 => % 173.20/173.41 ∀ (A2 : «type/realax/real»), % 173.20/173.41 Eq (A A2) % 173.20/173.41 («const/iterate/sum» «type/nums/num» («const/iterate/..» («const/nums/NUMERAL» «const/nums/_0») A0) % 173.20/173.41 fun A3 => «const/realax/real_mul» (A1 A3) («const/realax/real_pow» A2 A3)))) % 173.20/173.41 True % 173.20/173.41 Clause #4 (by assumption #[]): Eq (Not (∀ (A : «type/realax/real»), «const/iterate/polynomial_function» fun A0 => A)) True % 173.20/173.41 Clause #5 (by clausification #[4]): Eq (∀ (A : «type/realax/real»), «const/iterate/polynomial_function» fun A0 => A) False % 173.20/173.41 Clause #6 (by clausification #[5]): ∀ (a : «type/realax/real»), Eq (Not («const/iterate/polynomial_function» fun A0 => skS.0 0 a)) True % 173.20/173.41 Clause #7 (by clausification #[6]): ∀ (a : «type/realax/real»), Eq («const/iterate/polynomial_function» fun A0 => skS.0 0 a) False % 173.20/173.41 Clause #8 (by clausification #[0]): ∀ (a : «type/realax/real»), % 173.20/173.41 Eq % 173.20/173.41 (Eq % 173.20/173.41 («const/realax/real_mul» a % 173.20/173.41 («const/realax/real_of_num» («const/nums/NUMERAL» («const/nums/BIT1» «const/nums/_0»)))) % 173.20/173.41 a) % 173.20/173.41 True % 173.20/173.41 Clause #9 (by clausification #[8]): ∀ (a : «type/realax/real»), % 173.20/173.41 Eq («const/realax/real_mul» a («const/realax/real_of_num» («const/nums/NUMERAL» («const/nums/BIT1» «const/nums/_0»)))) % 173.20/173.41 a % 173.20/173.41 Clause #10 (by clausification #[1]): ∀ (a : «type/realax/real»), % 173.20/173.41 Eq % 173.20/173.41 (Eq («const/realax/real_pow» a («const/nums/NUMERAL» «const/nums/_0»)) % 173.20/173.41 («const/realax/real_of_num» («const/nums/NUMERAL» («const/nums/BIT1» «const/nums/_0»)))) % 173.20/173.41 True % 173.20/173.41 Clause #11 (by clausification #[10]): ∀ (a : «type/realax/real»), % 173.20/173.41 Eq («const/realax/real_pow» a («const/nums/NUMERAL» «const/nums/_0»)) % 173.20/173.41 («const/realax/real_of_num» («const/nums/NUMERAL» («const/nums/BIT1» «const/nums/_0»))) % 173.20/173.41 Clause #12 (by superposition #[11, 9]): ∀ (a a_1 : «type/realax/real»), % 173.20/173.41 Eq («const/realax/real_mul» a («const/realax/real_pow» a_1 («const/nums/NUMERAL» «const/nums/_0»))) a % 173.20/173.41 Clause #14 (by clausification #[2]): ∀ (a : «type/nums/num» → «type/realax/real»), % 173.20/173.41 Eq (∀ (A0 : «type/nums/num»), Eq («const/iterate/sum» «type/nums/num» («const/iterate/..» A0 A0) a) (a A0)) True % 173.20/173.41 Clause #15 (by clausification #[14]): ∀ (a : «type/nums/num») (a_1 : «type/nums/num» → «type/realax/real»), % 173.20/173.41 Eq (Eq («const/iterate/sum» «type/nums/num» («const/iterate/..» a a) a_1) (a_1 a)) True % 173.20/173.41 Clause #16 (by clausification #[15]): ∀ (a : «type/nums/num») (a_1 : «type/nums/num» → «type/realax/real»), % 173.20/173.41 Eq («const/iterate/sum» «type/nums/num» («const/iterate/..» a a) a_1) (a_1 a) % 173.20/173.41 Clause #18 (by superposition #[16, 12]): ∀ (a a_1 : «type/nums/num» → «type/realax/real»), % 173.20/173.41 Eq % 173.20/173.41 («const/iterate/sum» «type/nums/num» % 173.20/173.41 («const/iterate/..» («const/nums/NUMERAL» «const/nums/_0») («const/nums/NUMERAL» «const/nums/_0»)) fun x => % 173.20/173.41 «const/realax/real_mul» (a x) («const/realax/real_pow» (a_1 x) x)) % 173.20/173.41 (a («const/nums/NUMERAL» «const/nums/_0»)) % 173.20/173.41 Clause #75 (by clausification #[3]): ∀ (a : «type/realax/real» → «type/realax/real»), % 173.20/173.41 Eq % 173.20/173.41 (Eq («const/iterate/polynomial_function» a) % 174.75/174.96 (Exists fun A0 => % 174.75/174.96 Exists fun A1 => % 174.75/174.96 ∀ (A2 : «type/realax/real»), % 174.75/174.96 Eq (a A2) % 174.75/174.96 («const/iterate/sum» «type/nums/num» («const/iterate/..» («const/nums/NUMERAL» «const/nums/_0») A0) % 174.75/174.96 fun A3 => «const/realax/real_mul» (A1 A3) («const/realax/real_pow» A2 A3)))) % 174.75/174.96 True % 174.75/174.96 Clause #76 (by clausification #[75]): ∀ (a : «type/realax/real» → «type/realax/real»), % 174.75/174.96 Eq («const/iterate/polynomial_function» a) % 174.75/174.96 (Exists fun A0 => % 174.75/174.96 Exists fun A1 => % 174.75/174.96 ∀ (A2 : «type/realax/real»), % 174.75/174.96 Eq (a A2) % 174.75/174.96 («const/iterate/sum» «type/nums/num» («const/iterate/..» («const/nums/NUMERAL» «const/nums/_0») A0) % 174.75/174.96 fun A3 => «const/realax/real_mul» (A1 A3) («const/realax/real_pow» A2 A3))) % 174.75/174.96 Clause #79 (by superposition #[76, 7]): ∀ (a : «type/realax/real»), % 174.75/174.96 Eq % 174.75/174.96 (Exists fun A0 => % 174.75/174.96 Exists fun A1 => % 174.75/174.96 ∀ (A2 : «type/realax/real»), % 174.75/174.96 Eq (skS.0 0 a) % 174.75/174.96 («const/iterate/sum» «type/nums/num» («const/iterate/..» («const/nums/NUMERAL» «const/nums/_0») A0) % 174.75/174.96 fun A3 => «const/realax/real_mul» (A1 A3) («const/realax/real_pow» A2 A3))) % 174.75/174.96 False % 174.75/174.96 Clause #25865 (by clausification #[79]): ∀ (a : «type/realax/real») (a_1 : «type/nums/num»), % 174.75/174.96 Eq % 174.75/174.96 (Exists fun A1 => % 174.75/174.96 ∀ (A2 : «type/realax/real»), % 174.75/174.96 Eq (skS.0 0 a) % 174.75/174.96 («const/iterate/sum» «type/nums/num» («const/iterate/..» («const/nums/NUMERAL» «const/nums/_0») a_1) fun A3 => % 174.75/174.96 «const/realax/real_mul» (A1 A3) («const/realax/real_pow» A2 A3))) % 174.75/174.96 False % 174.75/174.96 Clause #25866 (by clausification #[25865]): ∀ (a : «type/realax/real») (a_1 : «type/nums/num») (a_2 : «type/nums/num» → «type/realax/real»), % 174.75/174.96 Eq % 174.75/174.96 (∀ (A2 : «type/realax/real»), % 174.75/174.96 Eq (skS.0 0 a) % 174.75/174.96 («const/iterate/sum» «type/nums/num» («const/iterate/..» («const/nums/NUMERAL» «const/nums/_0») a_1) fun A3 => % 174.75/174.96 «const/realax/real_mul» (a_2 A3) («const/realax/real_pow» A2 A3))) % 174.75/174.96 False % 174.75/174.96 Clause #25867 (by clausification #[25866]): ∀ (a : «type/realax/real») (a_1 : «type/nums/num») (a_2 : «type/nums/num» → «type/realax/real») % 174.75/174.96 (a_3 : «type/realax/real»), % 174.75/174.96 Eq % 174.75/174.96 (Not % 174.75/174.96 (Eq (skS.0 0 a) % 174.75/174.96 («const/iterate/sum» «type/nums/num» («const/iterate/..» («const/nums/NUMERAL» «const/nums/_0») a_1) fun A3 => % 174.75/174.96 «const/realax/real_mul» (a_2 A3) («const/realax/real_pow» (skS.0 4 a a_1 a_2 a_3) A3)))) % 174.75/174.96 True % 174.75/174.96 Clause #25868 (by clausification #[25867]): ∀ (a : «type/realax/real») (a_1 : «type/nums/num») (a_2 : «type/nums/num» → «type/realax/real») % 174.75/174.96 (a_3 : «type/realax/real»), % 174.75/174.96 Eq % 174.75/174.96 (Eq (skS.0 0 a) % 174.75/174.96 («const/iterate/sum» «type/nums/num» («const/iterate/..» («const/nums/NUMERAL» «const/nums/_0») a_1) fun A3 => % 174.75/174.96 «const/realax/real_mul» (a_2 A3) («const/realax/real_pow» (skS.0 4 a a_1 a_2 a_3) A3))) % 174.75/174.96 False % 174.75/174.96 Clause #25869 (by clausification #[25868]): ∀ (a : «type/realax/real») (a_1 : «type/nums/num») (a_2 : «type/nums/num» → «type/realax/real») % 174.75/174.96 (a_3 : «type/realax/real»), % 174.75/174.96 Ne (skS.0 0 a) % 174.75/174.96 («const/iterate/sum» «type/nums/num» («const/iterate/..» («const/nums/NUMERAL» «const/nums/_0») a_1) fun A3 => % 174.75/174.96 «const/realax/real_mul» (a_2 A3) («const/realax/real_pow» (skS.0 4 a a_1 a_2 a_3) A3)) % 174.75/174.96 Clause #25876 (by superposition #[25869, 18]): ∀ (a : «type/realax/real») (a_1 : «type/nums/num» → «type/realax/real»), % 174.75/174.96 Ne (skS.0 0 a) (a_1 («const/nums/NUMERAL» «const/nums/_0»)) % 174.75/174.96 Clause #26166 (by fluidSup #[25876, 9]): ∀ (a a_1 a_2 : «type/realax/real»), Ne (skS.0 0 a) ((fun _ => a_1) a_2) % 174.75/174.96 Clause #26233 (by betaEtaReduce #[26166]): ∀ (a a_1 : «type/realax/real»), Ne (skS.0 0 a) a_1 % 174.75/174.96 Clause #26234 (by destructive equality resolution #[26233]): False % 174.75/174.96 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------