%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO113^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.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:08:36 PM UTC 2025 % Result : Theorem 4.45s 4.62s % Output : Proof 4.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYO113^5 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n013.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 13:31:38 EDT 2025 % 0.13/0.35 % CPUTime : % 4.45/4.62 SZS status Theorem for theBenchmark.p % 4.45/4.62 SZS output start Proof for theBenchmark.p % 4.45/4.62 Clause #0 (by assumption #[]): Eq % 4.45/4.62 (Not % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And (And (And (cEVEN c0) (∀ (Xn : Iota), cEVEN Xn → cEVEN (cS (cS Xn)))) (cODD (cS c0))) % 4.45/4.62 (∀ (Xn : Iota), cODD Xn → cODD (cS (cS Xn)))) % 4.45/4.62 (And (And (cNUMBER c0) (cNUMBER (cS c0))) % 4.45/4.62 (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)) → And (cNUMBER (cS Xx)) (cNUMBER (cS (cS Xx)))) → % 4.45/4.62 ∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)))) % 4.45/4.62 (∀ (Xn : Iota), Iff (cNUMBER Xn) (Or (cEVEN Xn) (cODD Xn))) → % 4.45/4.62 ∀ (Xn : Iota), cNUMBER Xn)) % 4.45/4.62 True % 4.45/4.62 Clause #1 (by clausification #[0]): Eq % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And (And (And (cEVEN c0) (∀ (Xn : Iota), cEVEN Xn → cEVEN (cS (cS Xn)))) (cODD (cS c0))) % 4.45/4.62 (∀ (Xn : Iota), cODD Xn → cODD (cS (cS Xn)))) % 4.45/4.62 (And (And (cNUMBER c0) (cNUMBER (cS c0))) % 4.45/4.62 (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)) → And (cNUMBER (cS Xx)) (cNUMBER (cS (cS Xx)))) → % 4.45/4.62 ∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)))) % 4.45/4.62 (∀ (Xn : Iota), Iff (cNUMBER Xn) (Or (cEVEN Xn) (cODD Xn))) → % 4.45/4.62 ∀ (Xn : Iota), cNUMBER Xn) % 4.45/4.62 False % 4.45/4.62 Clause #2 (by clausification #[1]): Eq % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And (And (And (cEVEN c0) (∀ (Xn : Iota), cEVEN Xn → cEVEN (cS (cS Xn)))) (cODD (cS c0))) % 4.45/4.62 (∀ (Xn : Iota), cODD Xn → cODD (cS (cS Xn)))) % 4.45/4.62 (And (And (cNUMBER c0) (cNUMBER (cS c0))) % 4.45/4.62 (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)) → And (cNUMBER (cS Xx)) (cNUMBER (cS (cS Xx)))) → % 4.45/4.62 ∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)))) % 4.45/4.62 (∀ (Xn : Iota), Iff (cNUMBER Xn) (Or (cEVEN Xn) (cODD Xn)))) % 4.45/4.62 True % 4.45/4.62 Clause #3 (by clausification #[1]): Eq (∀ (Xn : Iota), cNUMBER Xn) False % 4.45/4.62 Clause #4 (by clausification #[2]): Eq (∀ (Xn : Iota), Iff (cNUMBER Xn) (Or (cEVEN Xn) (cODD Xn))) True % 4.45/4.62 Clause #5 (by clausification #[2]): Eq % 4.45/4.62 (And % 4.45/4.62 (And (And (And (cEVEN c0) (∀ (Xn : Iota), cEVEN Xn → cEVEN (cS (cS Xn)))) (cODD (cS c0))) % 4.45/4.62 (∀ (Xn : Iota), cODD Xn → cODD (cS (cS Xn)))) % 4.45/4.62 (And (And (cNUMBER c0) (cNUMBER (cS c0))) % 4.45/4.62 (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)) → And (cNUMBER (cS Xx)) (cNUMBER (cS (cS Xx)))) → % 4.45/4.62 ∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)))) % 4.45/4.62 True % 4.45/4.62 Clause #6 (by clausification #[4]): ∀ (a : Iota), Eq (Iff (cNUMBER a) (Or (cEVEN a) (cODD a))) True % 4.45/4.62 Clause #7 (by clausification #[6]): ∀ (a : Iota), Or (Eq (cNUMBER a) True) (Eq (Or (cEVEN a) (cODD a)) False) % 4.45/4.62 Clause #8 (by clausification #[6]): ∀ (a : Iota), Or (Eq (cNUMBER a) False) (Eq (Or (cEVEN a) (cODD a)) True) % 4.45/4.62 Clause #9 (by clausification #[7]): ∀ (a : Iota), Or (Eq (cNUMBER a) True) (Eq (cODD a) False) % 4.45/4.62 Clause #10 (by clausification #[7]): ∀ (a : Iota), Or (Eq (cNUMBER a) True) (Eq (cEVEN a) False) % 4.45/4.62 Clause #11 (by clausification #[3]): ∀ (a : Iota), Eq (Not (cNUMBER (skS.0 0 a))) True % 4.45/4.62 Clause #12 (by clausification #[11]): ∀ (a : Iota), Eq (cNUMBER (skS.0 0 a)) False % 4.45/4.62 Clause #13 (by clausification #[8]): ∀ (a : Iota), Or (Eq (cNUMBER a) False) (Or (Eq (cEVEN a) True) (Eq (cODD a) True)) % 4.45/4.62 Clause #14 (by clausification #[5]): Eq % 4.45/4.62 (And (And (cNUMBER c0) (cNUMBER (cS c0))) % 4.45/4.62 (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)) → And (cNUMBER (cS Xx)) (cNUMBER (cS (cS Xx)))) → % 4.45/4.62 ∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx))) % 4.45/4.62 True % 4.45/4.62 Clause #15 (by clausification #[5]): Eq % 4.45/4.62 (And (And (And (cEVEN c0) (∀ (Xn : Iota), cEVEN Xn → cEVEN (cS (cS Xn)))) (cODD (cS c0))) % 4.45/4.62 (∀ (Xn : Iota), cODD Xn → cODD (cS (cS Xn)))) % 4.45/4.62 True % 4.45/4.62 Clause #16 (by clausification #[14]): Or % 4.45/4.62 (Eq % 4.45/4.62 (And (And (cNUMBER c0) (cNUMBER (cS c0))) % 4.45/4.62 (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)) → And (cNUMBER (cS Xx)) (cNUMBER (cS (cS Xx))))) % 4.45/4.62 False) % 4.45/4.62 (Eq (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx))) True) % 4.45/4.62 Clause #17 (by clausification #[16]): Or (Eq (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx))) True) % 4.45/4.62 (Or (Eq (And (cNUMBER c0) (cNUMBER (cS c0))) False) % 4.45/4.62 (Eq (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)) → And (cNUMBER (cS Xx)) (cNUMBER (cS (cS Xx)))) False)) % 4.48/4.65 Clause #18 (by clausification #[17]): ∀ (a : Iota), % 4.48/4.65 Or (Eq (And (cNUMBER c0) (cNUMBER (cS c0))) False) % 4.48/4.65 (Or (Eq (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)) → And (cNUMBER (cS Xx)) (cNUMBER (cS (cS Xx)))) False) % 4.48/4.65 (Eq (And (cNUMBER a) (cNUMBER (cS a))) True)) % 4.48/4.65 Clause #19 (by clausification #[18]): ∀ (a : Iota), % 4.48/4.65 Or (Eq (∀ (Xx : Iota), And (cNUMBER Xx) (cNUMBER (cS Xx)) → And (cNUMBER (cS Xx)) (cNUMBER (cS (cS Xx)))) False) % 4.48/4.65 (Or (Eq (And (cNUMBER a) (cNUMBER (cS a))) True) (Or (Eq (cNUMBER c0) False) (Eq (cNUMBER (cS c0)) False))) % 4.48/4.65 Clause #20 (by clausification #[19]): ∀ (a a_1 : Iota), % 4.48/4.65 Or (Eq (And (cNUMBER a) (cNUMBER (cS a))) True) % 4.48/4.65 (Or (Eq (cNUMBER c0) False) % 4.48/4.65 (Or (Eq (cNUMBER (cS c0)) False) % 4.48/4.65 (Eq % 4.48/4.65 (Not % 4.48/4.65 (And (cNUMBER (skS.0 1 a_1)) (cNUMBER (cS (skS.0 1 a_1))) → % 4.48/4.65 And (cNUMBER (cS (skS.0 1 a_1))) (cNUMBER (cS (cS (skS.0 1 a_1)))))) % 4.48/4.65 True))) % 4.48/4.65 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), % 4.48/4.65 Or (Eq (cNUMBER c0) False) % 4.48/4.65 (Or (Eq (cNUMBER (cS c0)) False) % 4.48/4.65 (Or % 4.48/4.65 (Eq % 4.48/4.65 (Not % 4.48/4.65 (And (cNUMBER (skS.0 1 a)) (cNUMBER (cS (skS.0 1 a))) → % 4.48/4.65 And (cNUMBER (cS (skS.0 1 a))) (cNUMBER (cS (cS (skS.0 1 a)))))) % 4.48/4.65 True) % 4.48/4.65 (Eq (cNUMBER (cS a_1)) True))) % 4.48/4.65 Clause #22 (by clausification #[20]): ∀ (a a_1 : Iota), % 4.48/4.65 Or (Eq (cNUMBER c0) False) % 4.48/4.65 (Or (Eq (cNUMBER (cS c0)) False) % 4.48/4.65 (Or % 4.48/4.65 (Eq % 4.48/4.65 (Not % 4.48/4.65 (And (cNUMBER (skS.0 1 a)) (cNUMBER (cS (skS.0 1 a))) → % 4.48/4.65 And (cNUMBER (cS (skS.0 1 a))) (cNUMBER (cS (cS (skS.0 1 a)))))) % 4.48/4.65 True) % 4.48/4.65 (Eq (cNUMBER a_1) True))) % 4.48/4.65 Clause #23 (by clausification #[21]): ∀ (a a_1 : Iota), % 4.48/4.65 Or (Eq (cNUMBER c0) False) % 4.48/4.65 (Or (Eq (cNUMBER (cS c0)) False) % 4.48/4.65 (Or (Eq (cNUMBER (cS a)) True) % 4.48/4.65 (Eq % 4.48/4.65 (And (cNUMBER (skS.0 1 a_1)) (cNUMBER (cS (skS.0 1 a_1))) → % 4.48/4.65 And (cNUMBER (cS (skS.0 1 a_1))) (cNUMBER (cS (cS (skS.0 1 a_1))))) % 4.48/4.65 False))) % 4.48/4.65 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), % 4.48/4.65 Or (Eq (cNUMBER c0) False) % 4.48/4.65 (Or (Eq (cNUMBER (cS c0)) False) % 4.48/4.65 (Or (Eq (cNUMBER (cS a)) True) (Eq (And (cNUMBER (skS.0 1 a_1)) (cNUMBER (cS (skS.0 1 a_1)))) True))) % 4.48/4.65 Clause #26 (by clausification #[24]): ∀ (a a_1 : Iota), % 4.48/4.65 Or (Eq (cNUMBER c0) False) % 4.48/4.65 (Or (Eq (cNUMBER (cS c0)) False) (Or (Eq (cNUMBER (cS a)) True) (Eq (cNUMBER (cS (skS.0 1 a_1))) True))) % 4.48/4.65 Clause #27 (by clausification #[24]): ∀ (a a_1 : Iota), % 4.48/4.65 Or (Eq (cNUMBER c0) False) % 4.48/4.65 (Or (Eq (cNUMBER (cS c0)) False) (Or (Eq (cNUMBER (cS a)) True) (Eq (cNUMBER (skS.0 1 a_1)) True))) % 4.48/4.65 Clause #28 (by clausification #[15]): Eq (∀ (Xn : Iota), cODD Xn → cODD (cS (cS Xn))) True % 4.48/4.65 Clause #29 (by clausification #[15]): Eq (And (And (cEVEN c0) (∀ (Xn : Iota), cEVEN Xn → cEVEN (cS (cS Xn)))) (cODD (cS c0))) True % 4.48/4.65 Clause #30 (by clausification #[28]): ∀ (a : Iota), Eq (cODD a → cODD (cS (cS a))) True % 4.48/4.65 Clause #31 (by clausification #[30]): ∀ (a : Iota), Or (Eq (cODD a) False) (Eq (cODD (cS (cS a))) True) % 4.48/4.65 Clause #32 (by clausification #[29]): Eq (cODD (cS c0)) True % 4.48/4.65 Clause #33 (by clausification #[29]): Eq (And (cEVEN c0) (∀ (Xn : Iota), cEVEN Xn → cEVEN (cS (cS Xn)))) True % 4.48/4.65 Clause #34 (by superposition #[32, 9]): Or (Eq (cNUMBER (cS c0)) True) (Eq True False) % 4.48/4.65 Clause #36 (by clausification #[34]): Eq (cNUMBER (cS c0)) True % 4.48/4.65 Clause #37 (by backward demodulation #[36, 26]): ∀ (a a_1 : Iota), % 4.48/4.65 Or (Eq (cNUMBER c0) False) (Or (Eq True False) (Or (Eq (cNUMBER (cS a)) True) (Eq (cNUMBER (cS (skS.0 1 a_1))) True))) % 4.48/4.65 Clause #44 (by clausification #[33]): Eq (∀ (Xn : Iota), cEVEN Xn → cEVEN (cS (cS Xn))) True % 4.48/4.65 Clause #45 (by clausification #[33]): Eq (cEVEN c0) True % 4.48/4.65 Clause #46 (by clausification #[44]): ∀ (a : Iota), Eq (cEVEN a → cEVEN (cS (cS a))) True % 4.48/4.65 Clause #47 (by clausification #[46]): ∀ (a : Iota), Or (Eq (cEVEN a) False) (Eq (cEVEN (cS (cS a))) True) % 4.48/4.65 Clause #48 (by clausification #[22]): ∀ (a a_1 : Iota), % 4.48/4.65 Or (Eq (cNUMBER c0) False) % 4.48/4.68 (Or (Eq (cNUMBER (cS c0)) False) % 4.48/4.68 (Or (Eq (cNUMBER a) True) % 4.48/4.68 (Eq % 4.48/4.68 (And (cNUMBER (skS.0 1 a_1)) (cNUMBER (cS (skS.0 1 a_1))) → % 4.48/4.68 And (cNUMBER (cS (skS.0 1 a_1))) (cNUMBER (cS (cS (skS.0 1 a_1))))) % 4.48/4.68 False))) % 4.48/4.68 Clause #50 (by clausification #[48]): ∀ (a a_1 : Iota), % 4.48/4.68 Or (Eq (cNUMBER c0) False) % 4.48/4.68 (Or (Eq (cNUMBER (cS c0)) False) % 4.48/4.68 (Or (Eq (cNUMBER a) True) (Eq (And (cNUMBER (cS (skS.0 1 a_1))) (cNUMBER (cS (cS (skS.0 1 a_1))))) False))) % 4.48/4.68 Clause #55 (by superposition #[45, 10]): Or (Eq (cNUMBER c0) True) (Eq True False) % 4.48/4.68 Clause #57 (by clausification #[55]): Eq (cNUMBER c0) True % 4.48/4.68 Clause #83 (by forward demodulation #[27, 57]): ∀ (a a_1 : Iota), % 4.48/4.68 Or (Eq True False) (Or (Eq (cNUMBER (cS c0)) False) (Or (Eq (cNUMBER (cS a)) True) (Eq (cNUMBER (skS.0 1 a_1)) True))) % 4.48/4.68 Clause #84 (by clausification #[83]): ∀ (a a_1 : Iota), Or (Eq (cNUMBER (cS c0)) False) (Or (Eq (cNUMBER (cS a)) True) (Eq (cNUMBER (skS.0 1 a_1)) True)) % 4.48/4.68 Clause #85 (by forward demodulation #[84, 36]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (cNUMBER (cS a)) True) (Eq (cNUMBER (skS.0 1 a_1)) True)) % 4.48/4.68 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), Or (Eq (cNUMBER (cS a)) True) (Eq (cNUMBER (skS.0 1 a_1)) True) % 4.48/4.68 Clause #102 (by clausification #[37]): ∀ (a a_1 : Iota), Or (Eq (cNUMBER c0) False) (Or (Eq (cNUMBER (cS a)) True) (Eq (cNUMBER (cS (skS.0 1 a_1))) True)) % 4.48/4.68 Clause #103 (by forward demodulation #[102, 57]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (cNUMBER (cS a)) True) (Eq (cNUMBER (cS (skS.0 1 a_1))) True)) % 4.48/4.68 Clause #104 (by clausification #[103]): ∀ (a a_1 : Iota), Or (Eq (cNUMBER (cS a)) True) (Eq (cNUMBER (cS (skS.0 1 a_1))) True) % 4.48/4.68 Clause #109 (by equality factoring #[104]): ∀ (a : Iota), Or (Ne True True) (Eq (cNUMBER (cS (skS.0 1 a))) True) % 4.48/4.68 Clause #110 (by clausification #[109]): ∀ (a : Iota), Or (Eq (cNUMBER (cS (skS.0 1 a))) True) (Or (Eq True False) (Eq True False)) % 4.48/4.68 Clause #112 (by clausification #[110]): ∀ (a : Iota), Or (Eq (cNUMBER (cS (skS.0 1 a))) True) (Eq True False) % 4.48/4.68 Clause #113 (by clausification #[112]): ∀ (a : Iota), Eq (cNUMBER (cS (skS.0 1 a))) True % 4.48/4.68 Clause #135 (by clausification #[50]): ∀ (a a_1 : Iota), % 4.48/4.68 Or (Eq (cNUMBER c0) False) % 4.48/4.68 (Or (Eq (cNUMBER (cS c0)) False) % 4.48/4.68 (Or (Eq (cNUMBER a) True) % 4.48/4.68 (Or (Eq (cNUMBER (cS (skS.0 1 a_1))) False) (Eq (cNUMBER (cS (cS (skS.0 1 a_1)))) False)))) % 4.48/4.68 Clause #136 (by forward demodulation #[135, 57]): ∀ (a a_1 : Iota), % 4.48/4.68 Or (Eq True False) % 4.48/4.68 (Or (Eq (cNUMBER (cS c0)) False) % 4.48/4.68 (Or (Eq (cNUMBER a) True) % 4.48/4.68 (Or (Eq (cNUMBER (cS (skS.0 1 a_1))) False) (Eq (cNUMBER (cS (cS (skS.0 1 a_1)))) False)))) % 4.48/4.68 Clause #137 (by clausification #[136]): ∀ (a a_1 : Iota), % 4.48/4.68 Or (Eq (cNUMBER (cS c0)) False) % 4.48/4.68 (Or (Eq (cNUMBER a) True) (Or (Eq (cNUMBER (cS (skS.0 1 a_1))) False) (Eq (cNUMBER (cS (cS (skS.0 1 a_1)))) False))) % 4.48/4.68 Clause #138 (by forward demodulation #[137, 36]): ∀ (a a_1 : Iota), % 4.48/4.68 Or (Eq True False) % 4.48/4.68 (Or (Eq (cNUMBER a) True) (Or (Eq (cNUMBER (cS (skS.0 1 a_1))) False) (Eq (cNUMBER (cS (cS (skS.0 1 a_1)))) False))) % 4.48/4.68 Clause #139 (by clausification #[138]): ∀ (a a_1 : Iota), % 4.48/4.68 Or (Eq (cNUMBER a) True) (Or (Eq (cNUMBER (cS (skS.0 1 a_1))) False) (Eq (cNUMBER (cS (cS (skS.0 1 a_1)))) False)) % 4.48/4.68 Clause #140 (by forward demodulation #[139, 113]): ∀ (a a_1 : Iota), Or (Eq (cNUMBER a) True) (Or (Eq True False) (Eq (cNUMBER (cS (cS (skS.0 1 a_1)))) False)) % 4.48/4.68 Clause #141 (by clausification #[140]): ∀ (a a_1 : Iota), Or (Eq (cNUMBER a) True) (Eq (cNUMBER (cS (cS (skS.0 1 a_1)))) False) % 4.48/4.68 Clause #142 (by superposition #[141, 86]): ∀ (a a_1 : Iota), Or (Eq (cNUMBER a) True) (Or (Eq False True) (Eq (cNUMBER (skS.0 1 a_1)) True)) % 4.48/4.68 Clause #143 (by clausification #[142]): ∀ (a a_1 : Iota), Or (Eq (cNUMBER a) True) (Eq (cNUMBER (skS.0 1 a_1)) True) % 4.48/4.68 Clause #144 (by superposition #[143, 12]): ∀ (a : Iota), Or (Eq (cNUMBER (skS.0 1 a)) True) (Eq True False) % 4.48/4.68 Clause #151 (by clausification #[144]): ∀ (a : Iota), Eq (cNUMBER (skS.0 1 a)) True % 4.48/4.68 Clause #152 (by superposition #[151, 13]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (cEVEN (skS.0 1 a)) True) (Eq (cODD (skS.0 1 a)) True)) % 4.48/4.69 Clause #170 (by clausification #[152]): ∀ (a : Iota), Or (Eq (cEVEN (skS.0 1 a)) True) (Eq (cODD (skS.0 1 a)) True) % 4.48/4.69 Clause #172 (by superposition #[170, 31]): ∀ (a : Iota), Or (Eq (cEVEN (skS.0 1 a)) True) (Or (Eq True False) (Eq (cODD (cS (cS (skS.0 1 a)))) True)) % 4.48/4.69 Clause #202 (by clausification #[172]): ∀ (a : Iota), Or (Eq (cEVEN (skS.0 1 a)) True) (Eq (cODD (cS (cS (skS.0 1 a)))) True) % 4.48/4.69 Clause #203 (by superposition #[202, 9]): ∀ (a : Iota), Or (Eq (cEVEN (skS.0 1 a)) True) (Or (Eq (cNUMBER (cS (cS (skS.0 1 a)))) True) (Eq True False)) % 4.48/4.69 Clause #206 (by clausification #[203]): ∀ (a : Iota), Or (Eq (cEVEN (skS.0 1 a)) True) (Eq (cNUMBER (cS (cS (skS.0 1 a)))) True) % 4.48/4.69 Clause #207 (by superposition #[206, 141]): ∀ (a a_1 : Iota), Or (Eq (cEVEN (skS.0 1 a)) True) (Or (Eq (cNUMBER a_1) True) (Eq True False)) % 4.48/4.69 Clause #209 (by clausification #[207]): ∀ (a a_1 : Iota), Or (Eq (cEVEN (skS.0 1 a)) True) (Eq (cNUMBER a_1) True) % 4.48/4.69 Clause #212 (by superposition #[209, 12]): ∀ (a : Iota), Or (Eq (cEVEN (skS.0 1 a)) True) (Eq True False) % 4.48/4.69 Clause #214 (by clausification #[212]): ∀ (a : Iota), Eq (cEVEN (skS.0 1 a)) True % 4.48/4.69 Clause #217 (by superposition #[214, 47]): ∀ (a : Iota), Or (Eq True False) (Eq (cEVEN (cS (cS (skS.0 1 a)))) True) % 4.48/4.69 Clause #218 (by clausification #[217]): ∀ (a : Iota), Eq (cEVEN (cS (cS (skS.0 1 a)))) True % 4.48/4.69 Clause #219 (by superposition #[218, 10]): ∀ (a : Iota), Or (Eq (cNUMBER (cS (cS (skS.0 1 a)))) True) (Eq True False) % 4.48/4.69 Clause #222 (by clausification #[219]): ∀ (a : Iota), Eq (cNUMBER (cS (cS (skS.0 1 a)))) True % 4.48/4.69 Clause #223 (by superposition #[222, 141]): ∀ (a : Iota), Or (Eq (cNUMBER a) True) (Eq True False) % 4.48/4.69 Clause #225 (by clausification #[223]): ∀ (a : Iota), Eq (cNUMBER a) True % 4.48/4.69 Clause #229 (by superposition #[225, 12]): Eq True False % 4.48/4.69 Clause #230 (by clausification #[229]): False % 4.48/4.69 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------