%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEV235^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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:02:58 PM UTC 2025 % Result : Theorem 35.35s 35.56s % Output : Proof 35.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SEV235^5 : TPTP v9.2.0. Released v4.0.0. % 0.12/0.14 % Command : duper %s % 0.14/0.36 % Computer : n031.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Fri Oct 3 01:28:38 EDT 2025 % 0.14/0.36 % CPUTime : % 35.35/35.56 SZS status Theorem for theBenchmark.p % 35.35/35.56 SZS output start Proof for theBenchmark.p % 35.35/35.56 Clause #0 (by assumption #[]): Eq % 35.35/35.56 (Not % 35.35/35.56 (∀ (Xx : Iota → Prop), % 35.35/35.56 Iff (∀ (Xx0 : Iota), Xx Xx0 → And (cD Xx0) (cE Xx0)) % 35.35/35.56 (And (∀ (Xx0 : Iota), Xx Xx0 → cD Xx0) (∀ (Xx0 : Iota), Xx Xx0 → cE Xx0)))) % 35.35/35.56 True % 35.35/35.56 Clause #1 (by clausification #[0]): Eq % 35.35/35.56 (∀ (Xx : Iota → Prop), % 35.35/35.56 Iff (∀ (Xx0 : Iota), Xx Xx0 → And (cD Xx0) (cE Xx0)) % 35.35/35.56 (And (∀ (Xx0 : Iota), Xx Xx0 → cD Xx0) (∀ (Xx0 : Iota), Xx Xx0 → cE Xx0))) % 35.35/35.56 False % 35.35/35.56 Clause #2 (by clausification #[1]): ∀ (a : Iota → Prop), % 35.35/35.56 Eq % 35.35/35.56 (Not % 35.35/35.56 (Iff (∀ (Xx0 : Iota), skS.0 0 a Xx0 → And (cD Xx0) (cE Xx0)) % 35.35/35.56 (And (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cD Xx0) (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0)))) % 35.35/35.56 True % 35.35/35.56 Clause #3 (by clausification #[2]): ∀ (a : Iota → Prop), % 35.35/35.56 Eq % 35.35/35.56 (Iff (∀ (Xx0 : Iota), skS.0 0 a Xx0 → And (cD Xx0) (cE Xx0)) % 35.35/35.56 (And (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cD Xx0) (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0))) % 35.35/35.56 False % 35.35/35.56 Clause #4 (by clausification #[3]): ∀ (a : Iota → Prop), % 35.35/35.56 Or (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → And (cD Xx0) (cE Xx0)) False) % 35.35/35.56 (Eq (And (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cD Xx0) (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0)) False) % 35.35/35.56 Clause #5 (by clausification #[3]): ∀ (a : Iota → Prop), % 35.35/35.56 Or (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → And (cD Xx0) (cE Xx0)) True) % 35.35/35.56 (Eq (And (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cD Xx0) (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0)) True) % 35.35/35.56 Clause #6 (by clausification #[4]): ∀ (a : Iota → Prop) (a_1 : Iota), % 35.35/35.56 Or (Eq (And (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cD Xx0) (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0)) False) % 35.35/35.56 (Eq (Not (skS.0 0 a (skS.0 1 a a_1) → And (cD (skS.0 1 a a_1)) (cE (skS.0 1 a a_1)))) True) % 35.35/35.56 Clause #7 (by clausification #[6]): ∀ (a : Iota → Prop) (a_1 : Iota), % 35.35/35.56 Or (Eq (Not (skS.0 0 a (skS.0 1 a a_1) → And (cD (skS.0 1 a a_1)) (cE (skS.0 1 a a_1)))) True) % 35.35/35.56 (Or (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cD Xx0) False) (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0) False)) % 35.35/35.56 Clause #8 (by clausification #[7]): ∀ (a : Iota → Prop) (a_1 : Iota), % 35.35/35.56 Or (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cD Xx0) False) % 35.35/35.56 (Or (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0) False) % 35.35/35.56 (Eq (skS.0 0 a (skS.0 1 a a_1) → And (cD (skS.0 1 a a_1)) (cE (skS.0 1 a a_1))) False)) % 35.35/35.56 Clause #9 (by clausification #[8]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.35/35.56 Or (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0) False) % 35.35/35.56 (Or (Eq (skS.0 0 a (skS.0 1 a a_1) → And (cD (skS.0 1 a a_1)) (cE (skS.0 1 a a_1))) False) % 35.35/35.56 (Eq (Not (skS.0 0 a (skS.0 2 a a_2) → cD (skS.0 2 a a_2))) True)) % 35.35/35.56 Clause #10 (by clausification #[9]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.35/35.56 Or (Eq (skS.0 0 a (skS.0 1 a a_1) → And (cD (skS.0 1 a a_1)) (cE (skS.0 1 a a_1))) False) % 35.35/35.56 (Or (Eq (Not (skS.0 0 a (skS.0 2 a a_2) → cD (skS.0 2 a a_2))) True) % 35.35/35.56 (Eq (Not (skS.0 0 a (skS.0 3 a a_3) → cE (skS.0 3 a a_3))) True)) % 35.35/35.56 Clause #11 (by clausification #[10]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.35/35.56 Or (Eq (Not (skS.0 0 a (skS.0 2 a a_1) → cD (skS.0 2 a a_1))) True) % 35.35/35.56 (Or (Eq (Not (skS.0 0 a (skS.0 3 a a_2) → cE (skS.0 3 a a_2))) True) (Eq (skS.0 0 a (skS.0 1 a a_3)) True)) % 35.35/35.56 Clause #12 (by clausification #[10]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.35/35.56 Or (Eq (Not (skS.0 0 a (skS.0 2 a a_1) → cD (skS.0 2 a a_1))) True) % 35.35/35.56 (Or (Eq (Not (skS.0 0 a (skS.0 3 a a_2) → cE (skS.0 3 a a_2))) True) % 35.35/35.56 (Eq (And (cD (skS.0 1 a a_3)) (cE (skS.0 1 a a_3))) False)) % 35.35/35.56 Clause #13 (by clausification #[11]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.35/35.56 Or (Eq (Not (skS.0 0 a (skS.0 3 a a_1) → cE (skS.0 3 a a_1))) True) % 35.35/35.56 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Eq (skS.0 0 a (skS.0 2 a a_3) → cD (skS.0 2 a a_3)) False)) % 35.35/35.56 Clause #14 (by clausification #[13]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.35/35.56 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.35/35.56 (Or (Eq (skS.0 0 a (skS.0 2 a a_2) → cD (skS.0 2 a a_2)) False) % 35.35/35.56 (Eq (skS.0 0 a (skS.0 3 a a_3) → cE (skS.0 3 a a_3)) False)) % 35.42/35.59 Clause #15 (by clausification #[14]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.42/35.59 (Or (Eq (skS.0 0 a (skS.0 3 a a_2) → cE (skS.0 3 a a_2)) False) (Eq (skS.0 0 a (skS.0 2 a a_3)) True)) % 35.42/35.59 Clause #16 (by clausification #[14]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.42/35.59 (Or (Eq (skS.0 0 a (skS.0 3 a a_2) → cE (skS.0 3 a a_2)) False) (Eq (cD (skS.0 2 a a_3)) False)) % 35.42/35.59 Clause #17 (by clausification #[15]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.42/35.59 (Or (Eq (skS.0 0 a (skS.0 2 a a_2)) True) (Eq (skS.0 0 a (skS.0 3 a a_3)) True)) % 35.42/35.59 Clause #18 (by clausification #[15]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (skS.0 0 a (skS.0 2 a a_2)) True) (Eq (cE (skS.0 3 a a_3)) False)) % 35.42/35.59 Clause #19 (by clausification #[5]): ∀ (a : Iota → Prop) (a_1 : Iota), % 35.42/35.59 Or (Eq (And (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cD Xx0) (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0)) True) % 35.42/35.59 (Eq (skS.0 0 a a_1 → And (cD a_1) (cE a_1)) True) % 35.42/35.59 Clause #20 (by clausification #[19]): ∀ (a : Iota → Prop) (a_1 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a a_1 → And (cD a_1) (cE a_1)) True) (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0) True) % 35.42/35.59 Clause #21 (by clausification #[19]): ∀ (a : Iota → Prop) (a_1 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a a_1 → And (cD a_1) (cE a_1)) True) (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cD Xx0) True) % 35.42/35.59 Clause #22 (by clausification #[20]): ∀ (a : Iota → Prop) (a_1 : Iota), % 35.42/35.59 Or (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cE Xx0) True) % 35.42/35.59 (Or (Eq (skS.0 0 a a_1) False) (Eq (And (cD a_1) (cE a_1)) True)) % 35.42/35.59 Clause #23 (by clausification #[22]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a a_1) False) (Or (Eq (And (cD a_1) (cE a_1)) True) (Eq (skS.0 0 a a_2 → cE a_2) True)) % 35.42/35.59 Clause #24 (by clausification #[23]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a a_1) False) (Or (Eq (skS.0 0 a a_2 → cE a_2) True) (Eq (cE a_1) True)) % 35.42/35.59 Clause #26 (by clausification #[24]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a a_1) False) (Or (Eq (cE a_1) True) (Or (Eq (skS.0 0 a a_2) False) (Eq (cE a_2) True))) % 35.42/35.59 Clause #30 (by clausification #[21]): ∀ (a : Iota → Prop) (a_1 : Iota), % 35.42/35.59 Or (Eq (∀ (Xx0 : Iota), skS.0 0 a Xx0 → cD Xx0) True) % 35.42/35.59 (Or (Eq (skS.0 0 a a_1) False) (Eq (And (cD a_1) (cE a_1)) True)) % 35.42/35.59 Clause #31 (by clausification #[30]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a a_1) False) (Or (Eq (And (cD a_1) (cE a_1)) True) (Eq (skS.0 0 a a_2 → cD a_2) True)) % 35.42/35.59 Clause #33 (by clausification #[31]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a a_1) False) (Or (Eq (skS.0 0 a a_2 → cD a_2) True) (Eq (cD a_1) True)) % 35.42/35.59 Clause #42 (by clausification #[33]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a a_1) False) (Or (Eq (cD a_1) True) (Or (Eq (skS.0 0 a a_2) False) (Eq (cD a_2) True))) % 35.42/35.59 Clause #44 (by superposition #[42, 17]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.42/35.59 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.59 (Or (Eq (skS.0 0 (fun x => a x) a_2) False) % 35.42/35.59 (Or (Eq (cD a_2) True) % 35.42/35.59 (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (skS.0 0 a (skS.0 3 a a_4)) True))))) % 35.42/35.59 Clause #46 (by clausification #[12]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.59 Or (Eq (Not (skS.0 0 a (skS.0 3 a a_1) → cE (skS.0 3 a a_1))) True) % 35.42/35.59 (Or (Eq (And (cD (skS.0 1 a a_2)) (cE (skS.0 1 a a_2))) False) % 35.42/35.59 (Eq (skS.0 0 a (skS.0 2 a a_3) → cD (skS.0 2 a a_3)) False)) % 35.42/35.59 Clause #47 (by clausification #[46]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.59 Or (Eq (And (cD (skS.0 1 a a_1)) (cE (skS.0 1 a a_1))) False) % 35.42/35.59 (Or (Eq (skS.0 0 a (skS.0 2 a a_2) → cD (skS.0 2 a a_2)) False) % 35.42/35.59 (Eq (skS.0 0 a (skS.0 3 a a_3) → cE (skS.0 3 a a_3)) False)) % 35.42/35.59 Clause #48 (by clausification #[47]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.59 Or (Eq (skS.0 0 a (skS.0 2 a a_1) → cD (skS.0 2 a a_1)) False) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 3 a a_2) → cE (skS.0 3 a a_2)) False) % 35.42/35.62 (Or (Eq (cD (skS.0 1 a a_3)) False) (Eq (cE (skS.0 1 a a_3)) False))) % 35.42/35.62 Clause #49 (by clausification #[48]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.62 Or (Eq (skS.0 0 a (skS.0 3 a a_1) → cE (skS.0 3 a a_1)) False) % 35.42/35.62 (Or (Eq (cD (skS.0 1 a a_2)) False) (Or (Eq (cE (skS.0 1 a a_2)) False) (Eq (skS.0 0 a (skS.0 2 a a_3)) True))) % 35.42/35.62 Clause #50 (by clausification #[48]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.62 Or (Eq (skS.0 0 a (skS.0 3 a a_1) → cE (skS.0 3 a a_1)) False) % 35.42/35.62 (Or (Eq (cD (skS.0 1 a a_2)) False) (Or (Eq (cE (skS.0 1 a a_2)) False) (Eq (cD (skS.0 2 a a_3)) False))) % 35.42/35.62 Clause #51 (by clausification #[49]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.62 Or (Eq (cD (skS.0 1 a a_1)) False) % 35.42/35.62 (Or (Eq (cE (skS.0 1 a a_1)) False) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 2 a a_2)) True) (Eq (skS.0 0 a (skS.0 3 a a_3)) True))) % 35.42/35.62 Clause #52 (by clausification #[49]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.62 Or (Eq (cD (skS.0 1 a a_1)) False) % 35.42/35.62 (Or (Eq (cE (skS.0 1 a a_1)) False) (Or (Eq (skS.0 0 a (skS.0 2 a a_2)) True) (Eq (cE (skS.0 3 a a_3)) False))) % 35.42/35.62 Clause #53 (by clausification #[16]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.62 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) False) (Eq (skS.0 0 a (skS.0 3 a a_3)) True)) % 35.42/35.62 Clause #54 (by clausification #[16]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.62 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) False) (Eq (cE (skS.0 3 a a_3)) False)) % 35.42/35.62 Clause #55 (by clausification #[50]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.62 Or (Eq (cD (skS.0 1 a a_1)) False) % 35.42/35.62 (Or (Eq (cE (skS.0 1 a a_1)) False) (Or (Eq (cD (skS.0 2 a a_2)) False) (Eq (skS.0 0 a (skS.0 3 a a_3)) True))) % 35.42/35.62 Clause #56 (by clausification #[50]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.62 Or (Eq (cD (skS.0 1 a a_1)) False) % 35.42/35.62 (Or (Eq (cE (skS.0 1 a a_1)) False) (Or (Eq (cD (skS.0 2 a a_2)) False) (Eq (cE (skS.0 3 a a_3)) False))) % 35.42/35.62 Clause #67 (by betaEtaReduce #[44]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.42/35.62 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a a_2) False) % 35.42/35.62 (Or (Eq (cD a_2) True) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (skS.0 0 a (skS.0 3 a a_4)) True))))) % 35.42/35.62 Clause #68 (by clausification #[67]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.42/35.62 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a a_2) False) % 35.42/35.62 (Or (Eq (cD a_2) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Eq (skS.0 0 a (skS.0 3 a a_4)) True)))) % 35.42/35.62 Clause #70 (by superposition #[68, 17]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 35.42/35.62 Or (Eq (cD (skS.0 2 (fun x => a x) a_1)) True) % 35.42/35.62 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.42/35.62 (Or (Eq (skS.0 0 (fun x => a x) (skS.0 1 (fun x => a x) a_3)) True) % 35.42/35.62 (Or (Eq (skS.0 0 (fun x => a x) (skS.0 3 (fun x => a x) a_4)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 1 a a_5)) True) (Or (Eq False True) (Eq (skS.0 0 a (skS.0 3 a a_6)) True)))))) % 35.42/35.62 Clause #793 (by betaEtaReduce #[70]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 35.42/35.62 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.62 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 3 a a_4)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 1 a a_5)) True) (Or (Eq False True) (Eq (skS.0 0 a (skS.0 3 a a_6)) True)))))) % 35.42/35.62 Clause #794 (by clausification #[793]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 35.42/35.62 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.62 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 3 a a_4)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 1 a a_5)) True) (Eq (skS.0 0 a (skS.0 3 a a_6)) True))))) % 35.42/35.62 Clause #910 (by equality factoring #[794]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 a_5 : Iota), % 35.42/35.62 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.62 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 3 a a_3)) True) % 35.42/35.62 (Or (Eq (skS.0 0 a (skS.0 3 a a_4)) True) (Or (Ne True True) (Eq (skS.0 0 a (skS.0 1 a a_5)) True))))) % 35.42/35.65 Clause #930 (by clausification #[910]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 a_5 : Iota), % 35.42/35.65 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.65 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_3)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_4)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 1 a a_5)) True) (Or (Eq True False) (Eq True False)))))) % 35.42/35.65 Clause #932 (by clausification #[930]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 a_5 : Iota), % 35.42/35.65 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.65 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_3)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_4)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_5)) True) (Eq True False))))) % 35.42/35.65 Clause #933 (by clausification #[932]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 a_5 : Iota), % 35.42/35.65 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.65 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_3)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_4)) True) (Eq (skS.0 0 a (skS.0 1 a a_5)) True)))) % 35.42/35.65 Clause #993 (by equality factoring #[933]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.42/35.65 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.65 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Or (Ne True True) (Eq (skS.0 0 a (skS.0 3 a a_4)) True)))) % 35.42/35.65 Clause #1115 (by clausification #[993]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.42/35.65 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.65 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_4)) True) (Or (Eq True False) (Eq True False))))) % 35.42/35.65 Clause #1117 (by clausification #[1115]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.42/35.65 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.65 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Or (Eq (skS.0 0 a (skS.0 3 a a_4)) True) (Eq True False)))) % 35.42/35.65 Clause #1118 (by clausification #[1117]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.42/35.65 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.42/35.65 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Eq (skS.0 0 a (skS.0 3 a a_4)) True))) % 35.42/35.65 Clause #1177 (by equality factoring #[1118]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.65 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_2)) True) (Or (Ne True True) (Eq (cD (skS.0 2 a a_3)) True))) % 35.42/35.65 Clause #1178 (by clausification #[1177]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.65 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_2)) True) (Or (Eq (cD (skS.0 2 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.42/35.65 Clause #1180 (by clausification #[1178]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.65 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_2)) True) (Or (Eq (cD (skS.0 2 a a_3)) True) (Eq True False))) % 35.42/35.65 Clause #1181 (by clausification #[1180]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.65 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (skS.0 0 a (skS.0 3 a a_2)) True) (Eq (cD (skS.0 2 a a_3)) True)) % 35.42/35.65 Clause #1234 (by superposition #[1181, 53]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.42/35.65 Or (Eq (skS.0 0 (fun x => a x) (skS.0 1 (fun x => a x) a_1)) True) % 35.42/35.65 (Or (Eq (skS.0 0 (fun x => a x) (skS.0 3 (fun x => a x) a_2)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Or (Eq True False) (Eq (skS.0 0 a (skS.0 3 a a_4)) True)))) % 35.42/35.65 Clause #3152 (by betaEtaReduce #[1234]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.42/35.65 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_2)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Or (Eq True False) (Eq (skS.0 0 a (skS.0 3 a a_4)) True)))) % 35.42/35.65 Clause #3153 (by clausification #[3152]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.42/35.65 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 3 a a_2)) True) % 35.42/35.65 (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Eq (skS.0 0 a (skS.0 3 a a_4)) True))) % 35.42/35.65 Clause #3267 (by equality factoring #[3153]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.42/35.65 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.51/35.68 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Ne True True) (Eq (skS.0 0 a (skS.0 3 a a_3)) True))) % 35.51/35.68 Clause #3268 (by clausification #[3267]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.51/35.68 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) % 35.51/35.68 (Or (Eq (skS.0 0 a (skS.0 3 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.51/35.68 Clause #3270 (by clausification #[3268]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.51/35.68 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a (skS.0 3 a a_3)) True) (Eq True False))) % 35.51/35.68 Clause #3271 (by clausification #[3270]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.51/35.68 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Eq (skS.0 0 a (skS.0 3 a a_3)) True)) % 35.51/35.68 Clause #3328 (by equality factoring #[3271]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Or (Ne True True) (Eq (skS.0 0 a (skS.0 1 a a_2)) True)) % 35.51/35.68 Clause #3329 (by clausification #[3328]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) % 35.51/35.68 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.51/35.68 Clause #3331 (by clausification #[3329]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Eq True False)) % 35.51/35.68 Clause #3332 (by clausification #[3331]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Eq (skS.0 0 a (skS.0 1 a a_2)) True) % 35.51/35.68 Clause #3333 (by superposition #[3332, 26]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 (fun x => a x) (skS.0 1 (fun x => a x) a_1)) True) % 35.51/35.68 (Or (Eq True False) (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True)))) % 35.51/35.68 Clause #3389 (by betaEtaReduce #[3333]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.51/35.68 (Or (Eq True False) (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True)))) % 35.51/35.68 Clause #3390 (by clausification #[3389]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.51/35.68 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True))) % 35.51/35.68 Clause #3399 (by superposition #[3390, 3332]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 (fun x => a x) (skS.0 1 (fun x => a x) a_1)) True) % 35.51/35.68 (Or (Eq (cE (skS.0 3 (fun x => a x) a_2)) True) % 35.51/35.68 (Or (Eq (cE (skS.0 3 a a_3)) True) (Or (Eq False True) (Eq (skS.0 0 a (skS.0 1 a a_4)) True)))) % 35.51/35.68 Clause #3626 (by betaEtaReduce #[3399]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.51/35.68 (Or (Eq (cE (skS.0 3 a a_2)) True) % 35.51/35.68 (Or (Eq (cE (skS.0 3 a a_3)) True) (Or (Eq False True) (Eq (skS.0 0 a (skS.0 1 a a_4)) True)))) % 35.51/35.68 Clause #3627 (by clausification #[3626]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.51/35.68 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.51/35.68 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq (cE (skS.0 3 a a_3)) True) (Eq (skS.0 0 a (skS.0 1 a a_4)) True))) % 35.51/35.68 Clause #3677 (by equality factoring #[3627]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.51/35.68 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.51/35.68 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Ne True True) (Eq (skS.0 0 a (skS.0 1 a a_3)) True))) % 35.51/35.68 Clause #3679 (by clausification #[3677]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.51/35.68 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.51/35.68 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.51/35.68 Clause #3681 (by clausification #[3679]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.51/35.68 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.51/35.68 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Eq True False))) % 35.51/35.68 Clause #3682 (by clausification #[3681]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.51/35.68 Or (Eq (cE (skS.0 3 a a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Eq (skS.0 0 a (skS.0 1 a a_3)) True)) % 35.51/35.68 Clause #3708 (by equality factoring #[3682]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.54/35.71 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Ne True True) (Eq (cE (skS.0 3 a a_2)) True)) % 35.54/35.71 Clause #3709 (by clausification #[3708]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.54/35.71 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.54/35.71 Clause #3711 (by clausification #[3709]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.54/35.71 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Eq True False)) % 35.54/35.71 Clause #3712 (by clausification #[3711]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Eq (cE (skS.0 3 a a_2)) True) % 35.54/35.71 Clause #3713 (by superposition #[3712, 26]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 (fun x => a x) a_1)) True) % 35.54/35.71 (Or (Eq True False) (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True)))) % 35.54/35.71 Clause #3716 (by superposition #[3712, 42]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 (fun x => a x) a_1)) True) % 35.54/35.71 (Or (Eq True False) (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True)))) % 35.54/35.71 Clause #3735 (by superposition #[3712, 18]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.54/35.71 Or (Eq (skS.0 0 (fun x => a x) (skS.0 1 (fun x => a x) a_1)) True) % 35.54/35.71 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a (skS.0 2 a a_3)) True) (Eq True False))) % 35.54/35.71 Clause #3736 (by betaEtaReduce #[3716]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.54/35.71 (Or (Eq True False) (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True)))) % 35.54/35.71 Clause #3737 (by clausification #[3736]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.54/35.71 (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True))) % 35.54/35.71 Clause #3746 (by superposition #[3737, 3712]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 (fun x => a x) a_1)) True) % 35.54/35.71 (Or (Eq (cD (skS.0 1 (fun x => a x) a_2)) True) % 35.54/35.71 (Or (Eq (cD (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cE (skS.0 3 a a_4)) True)))) % 35.54/35.71 Clause #3771 (by betaEtaReduce #[3713]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.54/35.71 (Or (Eq True False) (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True)))) % 35.54/35.71 Clause #3772 (by clausification #[3771]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.54/35.71 (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True))) % 35.54/35.71 Clause #3781 (by superposition #[3772, 3712]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 (fun x => a x) a_1)) True) % 35.54/35.71 (Or (Eq (cE (skS.0 1 (fun x => a x) a_2)) True) % 35.54/35.71 (Or (Eq (cE (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cE (skS.0 3 a a_4)) True)))) % 35.54/35.71 Clause #3788 (by betaEtaReduce #[3781]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.54/35.71 (Or (Eq (cE (skS.0 1 a a_2)) True) % 35.54/35.71 (Or (Eq (cE (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cE (skS.0 3 a a_4)) True)))) % 35.54/35.71 Clause #3789 (by clausification #[3788]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.54/35.71 (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (cE (skS.0 1 a a_3)) True) (Eq (cE (skS.0 3 a a_4)) True))) % 35.54/35.71 Clause #3794 (by equality factoring #[3789]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.54/35.71 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Ne True True) (Eq (cE (skS.0 1 a a_3)) True))) % 35.54/35.71 Clause #3795 (by clausification #[3794]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.54/35.71 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq (cE (skS.0 1 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.54/35.71 Clause #3797 (by clausification #[3795]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.54/35.71 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.54/35.71 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq (cE (skS.0 1 a a_3)) True) (Eq True False))) % 35.54/35.71 Clause #3798 (by clausification #[3797]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.74 Or (Eq (cE (skS.0 3 a a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Eq (cE (skS.0 1 a a_3)) True)) % 35.58/35.74 Clause #3801 (by equality factoring #[3798]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.74 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Ne True True) (Eq (cE (skS.0 3 a a_2)) True)) % 35.58/35.74 Clause #3802 (by clausification #[3801]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.74 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.58/35.74 Clause #3804 (by clausification #[3802]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.74 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Eq True False)) % 35.58/35.74 Clause #3805 (by clausification #[3804]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (cE (skS.0 1 a a_1)) True) (Eq (cE (skS.0 3 a a_2)) True) % 35.58/35.74 Clause #3849 (by betaEtaReduce #[3746]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.74 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.58/35.74 (Or (Eq (cD (skS.0 1 a a_2)) True) % 35.58/35.74 (Or (Eq (cD (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cE (skS.0 3 a a_4)) True)))) % 35.58/35.74 Clause #3850 (by clausification #[3849]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.74 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.58/35.74 (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (cD (skS.0 1 a a_3)) True) (Eq (cE (skS.0 3 a a_4)) True))) % 35.58/35.74 Clause #3858 (by equality factoring #[3850]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.74 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.58/35.74 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Ne True True) (Eq (cD (skS.0 1 a a_3)) True))) % 35.58/35.74 Clause #3861 (by clausification #[3858]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.74 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.58/35.74 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq (cD (skS.0 1 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.58/35.74 Clause #3863 (by clausification #[3861]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.74 Or (Eq (cE (skS.0 3 a a_1)) True) % 35.58/35.74 (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq (cD (skS.0 1 a a_3)) True) (Eq True False))) % 35.58/35.74 Clause #3864 (by clausification #[3863]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.74 Or (Eq (cE (skS.0 3 a a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Eq (cD (skS.0 1 a a_3)) True)) % 35.58/35.74 Clause #3870 (by equality factoring #[3864]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.74 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Ne True True) (Eq (cE (skS.0 3 a a_2)) True)) % 35.58/35.74 Clause #3871 (by clausification #[3870]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.74 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.58/35.74 Clause #3873 (by clausification #[3871]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.74 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Eq True False)) % 35.58/35.74 Clause #3874 (by clausification #[3873]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (cD (skS.0 1 a a_1)) True) (Eq (cE (skS.0 3 a a_2)) True) % 35.58/35.74 Clause #3987 (by betaEtaReduce #[3735]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.74 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.58/35.74 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a (skS.0 2 a a_3)) True) (Eq True False))) % 35.58/35.74 Clause #3988 (by clausification #[3987]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.74 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.58/35.74 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Eq (skS.0 0 a (skS.0 2 a a_3)) True)) % 35.58/35.74 Clause #4017 (by equality factoring #[3988]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.74 Or (Eq (skS.0 0 a (skS.0 2 a a_1)) True) (Or (Ne True True) (Eq (skS.0 0 a (skS.0 1 a a_2)) True)) % 35.58/35.74 Clause #4018 (by clausification #[4017]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.74 Or (Eq (skS.0 0 a (skS.0 2 a a_1)) True) % 35.58/35.74 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.58/35.74 Clause #4020 (by clausification #[4018]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.74 Or (Eq (skS.0 0 a (skS.0 2 a a_1)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Eq True False)) % 35.58/35.74 Clause #4021 (by clausification #[4020]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (skS.0 0 a (skS.0 2 a a_1)) True) (Eq (skS.0 0 a (skS.0 1 a a_2)) True) % 35.58/35.77 Clause #4025 (by superposition #[4021, 42]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (skS.0 0 (fun x => a x) (skS.0 1 (fun x => a x) a_1)) True) % 35.58/35.77 (Or (Eq True False) (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True)))) % 35.58/35.77 Clause #4131 (by betaEtaReduce #[4025]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.58/35.77 (Or (Eq True False) (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True)))) % 35.58/35.77 Clause #4132 (by clausification #[4131]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.58/35.77 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True))) % 35.58/35.77 Clause #4140 (by superposition #[4132, 4021]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.77 Or (Eq (skS.0 0 (fun x => a x) (skS.0 1 (fun x => a x) a_1)) True) % 35.58/35.77 (Or (Eq (cD (skS.0 2 (fun x => a x) a_2)) True) % 35.58/35.77 (Or (Eq (cD (skS.0 2 a a_3)) True) (Or (Eq False True) (Eq (skS.0 0 a (skS.0 1 a a_4)) True)))) % 35.58/35.77 Clause #4489 (by betaEtaReduce #[4140]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.77 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.58/35.77 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.58/35.77 (Or (Eq (cD (skS.0 2 a a_3)) True) (Or (Eq False True) (Eq (skS.0 0 a (skS.0 1 a a_4)) True)))) % 35.58/35.77 Clause #4490 (by clausification #[4489]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.77 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) % 35.58/35.77 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (cD (skS.0 2 a a_3)) True) (Eq (skS.0 0 a (skS.0 1 a a_4)) True))) % 35.58/35.77 Clause #4546 (by equality factoring #[4490]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.77 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Ne True True) (Eq (skS.0 0 a (skS.0 1 a a_3)) True))) % 35.58/35.77 Clause #4548 (by clausification #[4546]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.77 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.58/35.77 Clause #4550 (by clausification #[4548]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.77 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_3)) True) (Eq True False))) % 35.58/35.77 Clause #4551 (by clausification #[4550]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (cD (skS.0 2 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Eq (skS.0 0 a (skS.0 1 a a_3)) True)) % 35.58/35.77 Clause #4581 (by equality factoring #[4551]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.77 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Ne True True) (Eq (cD (skS.0 2 a a_2)) True)) % 35.58/35.77 Clause #4584 (by clausification #[4581]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.77 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.58/35.77 Clause #4586 (by clausification #[4584]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.77 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Eq True False)) % 35.58/35.77 Clause #4587 (by clausification #[4586]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Eq (cD (skS.0 2 a a_2)) True) % 35.58/35.77 Clause #4588 (by superposition #[4587, 26]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (cD (skS.0 2 (fun x => a x) a_1)) True) % 35.58/35.77 (Or (Eq True False) (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True)))) % 35.58/35.77 Clause #4591 (by superposition #[4587, 42]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (cD (skS.0 2 (fun x => a x) a_1)) True) % 35.58/35.77 (Or (Eq True False) (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True)))) % 35.58/35.77 Clause #4615 (by betaEtaReduce #[4588]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.77 (Or (Eq True False) (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True)))) % 35.58/35.77 Clause #4616 (by clausification #[4615]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.77 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.77 (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True))) % 35.58/35.79 Clause #4627 (by superposition #[4616, 4587]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.79 Or (Eq (cD (skS.0 2 (fun x => a x) a_1)) True) % 35.58/35.79 (Or (Eq (cE (skS.0 1 (fun x => a x) a_2)) True) % 35.58/35.79 (Or (Eq (cE (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cD (skS.0 2 a a_4)) True)))) % 35.58/35.79 Clause #4628 (by betaEtaReduce #[4591]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.79 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.79 (Or (Eq True False) (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True)))) % 35.58/35.79 Clause #4629 (by clausification #[4628]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.79 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.79 (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True))) % 35.58/35.79 Clause #4640 (by superposition #[4629, 4587]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.79 Or (Eq (cD (skS.0 2 (fun x => a x) a_1)) True) % 35.58/35.79 (Or (Eq (cD (skS.0 1 (fun x => a x) a_2)) True) % 35.58/35.79 (Or (Eq (cD (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cD (skS.0 2 a a_4)) True)))) % 35.58/35.79 Clause #4709 (by betaEtaReduce #[4627]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.79 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.79 (Or (Eq (cE (skS.0 1 a a_2)) True) % 35.58/35.79 (Or (Eq (cE (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cD (skS.0 2 a a_4)) True)))) % 35.58/35.79 Clause #4710 (by clausification #[4709]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.79 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.79 (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (cE (skS.0 1 a a_3)) True) (Eq (cD (skS.0 2 a a_4)) True))) % 35.58/35.79 Clause #4723 (by equality factoring #[4710]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.79 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.79 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Ne True True) (Eq (cE (skS.0 1 a a_3)) True))) % 35.58/35.79 Clause #4724 (by clausification #[4723]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.79 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.79 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (cE (skS.0 1 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.58/35.79 Clause #4726 (by clausification #[4724]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.79 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.79 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (cE (skS.0 1 a a_3)) True) (Eq True False))) % 35.58/35.79 Clause #4727 (by clausification #[4726]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.79 Or (Eq (cD (skS.0 2 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Eq (cE (skS.0 1 a a_3)) True)) % 35.58/35.79 Clause #4736 (by equality factoring #[4727]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.79 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Ne True True) (Eq (cD (skS.0 2 a a_2)) True)) % 35.58/35.79 Clause #4737 (by clausification #[4736]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.79 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.58/35.79 Clause #4739 (by clausification #[4737]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.79 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Eq True False)) % 35.58/35.79 Clause #4740 (by clausification #[4739]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (cE (skS.0 1 a a_1)) True) (Eq (cD (skS.0 2 a a_2)) True) % 35.58/35.79 Clause #4746 (by superposition #[4740, 54]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.79 Or (Eq (cE (skS.0 1 (fun x => a x) a_1)) True) % 35.58/35.79 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq True False) (Eq (cE (skS.0 3 a a_3)) False))) % 35.58/35.79 Clause #4755 (by betaEtaReduce #[4746]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.79 Or (Eq (cE (skS.0 1 a a_1)) True) % 35.58/35.79 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq True False) (Eq (cE (skS.0 3 a a_3)) False))) % 35.58/35.79 Clause #4756 (by clausification #[4755]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.79 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Eq (cE (skS.0 3 a a_3)) False)) % 35.58/35.79 Clause #4758 (by superposition #[4756, 3805]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.79 Or (Eq (cE (skS.0 1 (fun x => a x) a_1)) True) % 35.58/35.79 (Or (Eq (skS.0 0 (fun x => a x) (skS.0 1 (fun x => a x) a_2)) True) % 35.58/35.79 (Or (Eq (cE (skS.0 1 a a_3)) True) (Eq False True))) % 35.58/35.82 Clause #4801 (by betaEtaReduce #[4758]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.82 Or (Eq (cE (skS.0 1 a a_1)) True) % 35.58/35.82 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq (cE (skS.0 1 a a_3)) True) (Eq False True))) % 35.58/35.82 Clause #4802 (by clausification #[4801]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.82 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Eq (cE (skS.0 1 a a_3)) True)) % 35.58/35.82 Clause #4835 (by equality factoring #[4802]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.82 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Ne True True) (Eq (cE (skS.0 1 a a_2)) True)) % 35.58/35.82 Clause #4836 (by clausification #[4835]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.82 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.58/35.82 Clause #4838 (by clausification #[4836]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.82 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 1 a a_2)) True) (Eq True False)) % 35.58/35.82 Clause #4839 (by clausification #[4838]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Eq (cE (skS.0 1 a a_2)) True) % 35.58/35.82 Clause #4840 (by superposition #[4839, 26]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.82 Or (Eq (cE (skS.0 1 (fun x => a x) a_1)) True) % 35.58/35.82 (Or (Eq True False) (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True)))) % 35.58/35.82 Clause #4869 (by betaEtaReduce #[4840]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.82 Or (Eq (cE (skS.0 1 a a_1)) True) % 35.58/35.82 (Or (Eq True False) (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True)))) % 35.58/35.82 Clause #4870 (by clausification #[4869]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.82 Or (Eq (cE (skS.0 1 a a_1)) True) % 35.58/35.82 (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cE a_3) True))) % 35.58/35.82 Clause #4882 (by superposition #[4870, 4839]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.82 Or (Eq (cE (skS.0 1 (fun x => a x) a_1)) True) % 35.58/35.82 (Or (Eq (cE (skS.0 1 (fun x => a x) a_2)) True) % 35.58/35.82 (Or (Eq (cE (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cE (skS.0 1 a a_4)) True)))) % 35.58/35.82 Clause #5004 (by betaEtaReduce #[4640]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.82 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.82 (Or (Eq (cD (skS.0 1 a a_2)) True) % 35.58/35.82 (Or (Eq (cD (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cD (skS.0 2 a a_4)) True)))) % 35.58/35.82 Clause #5005 (by clausification #[5004]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.58/35.82 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.82 (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (cD (skS.0 1 a a_3)) True) (Eq (cD (skS.0 2 a a_4)) True))) % 35.58/35.82 Clause #5019 (by equality factoring #[5005]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.82 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.82 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Ne True True) (Eq (cD (skS.0 1 a a_3)) True))) % 35.58/35.82 Clause #5022 (by clausification #[5019]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.82 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.82 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (cD (skS.0 1 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.58/35.82 Clause #5024 (by clausification #[5022]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.82 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.58/35.82 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (cD (skS.0 1 a a_3)) True) (Eq True False))) % 35.58/35.82 Clause #5025 (by clausification #[5024]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.58/35.82 Or (Eq (cD (skS.0 2 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Eq (cD (skS.0 1 a a_3)) True)) % 35.58/35.82 Clause #5034 (by equality factoring #[5025]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.82 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Ne True True) (Eq (cD (skS.0 2 a a_2)) True)) % 35.58/35.82 Clause #5035 (by clausification #[5034]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.82 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.58/35.82 Clause #5037 (by clausification #[5035]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.58/35.82 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Eq True False)) % 35.58/35.82 Clause #5038 (by clausification #[5037]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (cD (skS.0 1 a a_1)) True) (Eq (cD (skS.0 2 a a_2)) True) % 35.67/35.85 Clause #5043 (by superposition #[5038, 54]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 (fun x => a x) a_1)) True) % 35.67/35.85 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq True False) (Eq (cE (skS.0 3 a a_3)) False))) % 35.67/35.85 Clause #5053 (by betaEtaReduce #[5043]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 a a_1)) True) % 35.67/35.85 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq True False) (Eq (cE (skS.0 3 a a_3)) False))) % 35.67/35.85 Clause #5054 (by clausification #[5053]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Eq (cE (skS.0 3 a a_3)) False)) % 35.67/35.85 Clause #5057 (by superposition #[5054, 3874]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 (fun x => a x) a_1)) True) % 35.67/35.85 (Or (Eq (skS.0 0 (fun x => a x) (skS.0 1 (fun x => a x) a_2)) True) % 35.67/35.85 (Or (Eq (cD (skS.0 1 a a_3)) True) (Eq False True))) % 35.67/35.85 Clause #5065 (by betaEtaReduce #[5057]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 a a_1)) True) % 35.67/35.85 (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Or (Eq (cD (skS.0 1 a a_3)) True) (Eq False True))) % 35.67/35.85 Clause #5066 (by clausification #[5065]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Eq (skS.0 0 a (skS.0 1 a a_2)) True) (Eq (cD (skS.0 1 a a_3)) True)) % 35.67/35.85 Clause #5097 (by equality factoring #[5066]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.67/35.85 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Ne True True) (Eq (cD (skS.0 1 a a_2)) True)) % 35.67/35.85 Clause #5098 (by clausification #[5097]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.67/35.85 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.67/35.85 Clause #5100 (by clausification #[5098]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.67/35.85 Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 1 a a_2)) True) (Eq True False)) % 35.67/35.85 Clause #5101 (by clausification #[5100]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (skS.0 0 a (skS.0 1 a a_1)) True) (Eq (cD (skS.0 1 a a_2)) True) % 35.67/35.85 Clause #5105 (by superposition #[5101, 42]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 (fun x => a x) a_1)) True) % 35.67/35.85 (Or (Eq True False) (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True)))) % 35.67/35.85 Clause #5130 (by betaEtaReduce #[5105]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 a a_1)) True) % 35.67/35.85 (Or (Eq True False) (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True)))) % 35.67/35.85 Clause #5131 (by clausification #[5130]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 a a_1)) True) % 35.67/35.85 (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True))) % 35.67/35.85 Clause #5144 (by superposition #[5131, 5101]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 (fun x => a x) a_1)) True) % 35.67/35.85 (Or (Eq (cD (skS.0 1 (fun x => a x) a_2)) True) % 35.67/35.85 (Or (Eq (cD (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cD (skS.0 1 a a_4)) True)))) % 35.67/35.85 Clause #5178 (by betaEtaReduce #[5144]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 a a_1)) True) % 35.67/35.85 (Or (Eq (cD (skS.0 1 a a_2)) True) % 35.67/35.85 (Or (Eq (cD (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cD (skS.0 1 a a_4)) True)))) % 35.67/35.85 Clause #5179 (by clausification #[5178]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 a a_1)) True) % 35.67/35.85 (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (cD (skS.0 1 a a_3)) True) (Eq (cD (skS.0 1 a a_4)) True))) % 35.67/35.85 Clause #5184 (by equality factoring #[5179]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 a a_1)) True) % 35.67/35.85 (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Ne True True) (Eq (cD (skS.0 1 a a_3)) True))) % 35.67/35.85 Clause #5185 (by clausification #[5184]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.85 Or (Eq (cD (skS.0 1 a a_1)) True) % 35.67/35.85 (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (cD (skS.0 1 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.67/35.88 Clause #5187 (by clausification #[5185]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq (cD (skS.0 1 a a_1)) True) % 35.67/35.88 (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq (cD (skS.0 1 a a_3)) True) (Eq True False))) % 35.67/35.88 Clause #5188 (by clausification #[5187]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 1 a a_2)) True) (Eq (cD (skS.0 1 a a_3)) True)) % 35.67/35.88 Clause #5193 (by equality factoring #[5188]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.67/35.88 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Ne True True) (Eq (cD (skS.0 1 a a_2)) True)) % 35.67/35.88 Clause #5194 (by clausification #[5193]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.67/35.88 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 1 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.67/35.88 Clause #5196 (by clausification #[5194]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.67/35.88 Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Eq (cD (skS.0 1 a a_2)) True) (Eq True False)) % 35.67/35.88 Clause #5197 (by clausification #[5196]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (cD (skS.0 1 a a_1)) True) (Eq (cD (skS.0 1 a a_2)) True) % 35.67/35.88 Clause #5202 (by equality factoring #[5197]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Ne True True) (Eq (cD (skS.0 1 a a_1)) True) % 35.67/35.88 Clause #5203 (by clausification #[5202]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (cD (skS.0 1 a a_1)) True) (Or (Eq True False) (Eq True False)) % 35.67/35.88 Clause #5205 (by clausification #[5203]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (cD (skS.0 1 a a_1)) True) (Eq True False) % 35.67/35.88 Clause #5206 (by clausification #[5205]): ∀ (a : Iota → Prop) (a_1 : Iota), Eq (cD (skS.0 1 a a_1)) True % 35.67/35.88 Clause #5207 (by backward demodulation #[5206, 51]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq True False) % 35.67/35.88 (Or (Eq (cE (skS.0 1 a a_1)) False) % 35.67/35.88 (Or (Eq (skS.0 0 a (skS.0 2 a a_2)) True) (Eq (skS.0 0 a (skS.0 3 a a_3)) True))) % 35.67/35.88 Clause #5208 (by backward demodulation #[5206, 55]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq True False) % 35.67/35.88 (Or (Eq (cE (skS.0 1 a a_1)) False) (Or (Eq (cD (skS.0 2 a a_2)) False) (Eq (skS.0 0 a (skS.0 3 a a_3)) True))) % 35.67/35.88 Clause #5209 (by backward demodulation #[5206, 56]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq True False) % 35.67/35.88 (Or (Eq (cE (skS.0 1 a a_1)) False) (Or (Eq (cD (skS.0 2 a a_2)) False) (Eq (cE (skS.0 3 a a_3)) False))) % 35.67/35.88 Clause #5210 (by backward demodulation #[5206, 52]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq True False) % 35.67/35.88 (Or (Eq (cE (skS.0 1 a a_1)) False) (Or (Eq (skS.0 0 a (skS.0 2 a a_2)) True) (Eq (cE (skS.0 3 a a_3)) False))) % 35.67/35.88 Clause #5213 (by clausification #[5209]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq (cE (skS.0 1 a a_1)) False) (Or (Eq (cD (skS.0 2 a a_2)) False) (Eq (cE (skS.0 3 a a_3)) False)) % 35.67/35.88 Clause #5232 (by clausification #[5208]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq (cE (skS.0 1 a a_1)) False) (Or (Eq (cD (skS.0 2 a a_2)) False) (Eq (skS.0 0 a (skS.0 3 a a_3)) True)) % 35.67/35.88 Clause #5237 (by clausification #[5210]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq (cE (skS.0 1 a a_1)) False) (Or (Eq (skS.0 0 a (skS.0 2 a a_2)) True) (Eq (cE (skS.0 3 a a_3)) False)) % 35.67/35.88 Clause #5260 (by clausification #[5207]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq (cE (skS.0 1 a a_1)) False) (Or (Eq (skS.0 0 a (skS.0 2 a a_2)) True) (Eq (skS.0 0 a (skS.0 3 a a_3)) True)) % 35.67/35.88 Clause #5321 (by betaEtaReduce #[4882]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.67/35.88 Or (Eq (cE (skS.0 1 a a_1)) True) % 35.67/35.88 (Or (Eq (cE (skS.0 1 a a_2)) True) % 35.67/35.88 (Or (Eq (cE (skS.0 1 a a_3)) True) (Or (Eq False True) (Eq (cE (skS.0 1 a a_4)) True)))) % 35.67/35.88 Clause #5322 (by clausification #[5321]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.67/35.88 Or (Eq (cE (skS.0 1 a a_1)) True) % 35.67/35.88 (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (cE (skS.0 1 a a_3)) True) (Eq (cE (skS.0 1 a a_4)) True))) % 35.67/35.88 Clause #5327 (by equality factoring #[5322]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.67/35.88 Or (Eq (cE (skS.0 1 a a_1)) True) % 35.67/35.88 (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Ne True True) (Eq (cE (skS.0 1 a a_3)) True))) % 35.67/35.88 Clause #5328 (by clausification #[5327]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.73/35.91 Or (Eq (cE (skS.0 1 a a_1)) True) % 35.73/35.91 (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (cE (skS.0 1 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.73/35.91 Clause #5330 (by clausification #[5328]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.73/35.91 Or (Eq (cE (skS.0 1 a a_1)) True) % 35.73/35.91 (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq (cE (skS.0 1 a a_3)) True) (Eq True False))) % 35.73/35.91 Clause #5331 (by clausification #[5330]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.73/35.91 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 1 a a_2)) True) (Eq (cE (skS.0 1 a a_3)) True)) % 35.73/35.91 Clause #5336 (by equality factoring #[5331]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.91 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Ne True True) (Eq (cE (skS.0 1 a a_2)) True)) % 35.73/35.91 Clause #5337 (by clausification #[5336]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.91 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 1 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.73/35.91 Clause #5339 (by clausification #[5337]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.91 Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Eq (cE (skS.0 1 a a_2)) True) (Eq True False)) % 35.73/35.91 Clause #5340 (by clausification #[5339]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (cE (skS.0 1 a a_1)) True) (Eq (cE (skS.0 1 a a_2)) True) % 35.73/35.91 Clause #5345 (by equality factoring #[5340]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Ne True True) (Eq (cE (skS.0 1 a a_1)) True) % 35.73/35.91 Clause #5348 (by clausification #[5345]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (cE (skS.0 1 a a_1)) True) (Or (Eq True False) (Eq True False)) % 35.73/35.91 Clause #5350 (by clausification #[5348]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (cE (skS.0 1 a a_1)) True) (Eq True False) % 35.73/35.91 Clause #5351 (by clausification #[5350]): ∀ (a : Iota → Prop) (a_1 : Iota), Eq (cE (skS.0 1 a a_1)) True % 35.73/35.91 Clause #5352 (by superposition #[5351, 5213]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.91 Or (Eq True False) (Or (Eq (cD (skS.0 2 a a_1)) False) (Eq (cE (skS.0 3 a a_2)) False)) % 35.73/35.91 Clause #5353 (by superposition #[5351, 5232]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.91 Or (Eq True False) (Or (Eq (cD (skS.0 2 a a_1)) False) (Eq (skS.0 0 a (skS.0 3 a a_2)) True)) % 35.73/35.91 Clause #5354 (by superposition #[5351, 5237]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.91 Or (Eq True False) (Or (Eq (skS.0 0 a (skS.0 2 a a_1)) True) (Eq (cE (skS.0 3 a a_2)) False)) % 35.73/35.91 Clause #5355 (by superposition #[5351, 5260]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.91 Or (Eq True False) (Or (Eq (skS.0 0 a (skS.0 2 a a_1)) True) (Eq (skS.0 0 a (skS.0 3 a a_2)) True)) % 35.73/35.91 Clause #5356 (by clausification #[5352]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (cD (skS.0 2 a a_1)) False) (Eq (cE (skS.0 3 a a_2)) False) % 35.73/35.91 Clause #5358 (by clausification #[5354]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (skS.0 0 a (skS.0 2 a a_1)) True) (Eq (cE (skS.0 3 a a_2)) False) % 35.73/35.91 Clause #5362 (by clausification #[5353]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (cD (skS.0 2 a a_1)) False) (Eq (skS.0 0 a (skS.0 3 a a_2)) True) % 35.73/35.91 Clause #5367 (by clausification #[5355]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (skS.0 0 a (skS.0 2 a a_1)) True) (Eq (skS.0 0 a (skS.0 3 a a_2)) True) % 35.73/35.91 Clause #5371 (by superposition #[5367, 42]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.73/35.91 Or (Eq (skS.0 0 (fun x => a x) (skS.0 3 (fun x => a x) a_1)) True) % 35.73/35.91 (Or (Eq True False) (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True)))) % 35.73/35.91 Clause #5458 (by betaEtaReduce #[5371]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.73/35.91 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) % 35.73/35.91 (Or (Eq True False) (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True)))) % 35.73/35.91 Clause #5459 (by clausification #[5458]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.73/35.91 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) % 35.73/35.91 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a a_3) False) (Eq (cD a_3) True))) % 35.73/35.91 Clause #5460 (by superposition #[5459, 5367]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.73/35.91 Or (Eq (skS.0 0 (fun x => a x) (skS.0 3 (fun x => a x) a_1)) True) % 35.73/35.93 (Or (Eq (cD (skS.0 2 (fun x => a x) a_2)) True) % 35.73/35.93 (Or (Eq (cD (skS.0 2 a a_3)) True) (Or (Eq False True) (Eq (skS.0 0 a (skS.0 3 a a_4)) True)))) % 35.73/35.93 Clause #6694 (by betaEtaReduce #[5460]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.73/35.93 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) % 35.73/35.93 (Or (Eq (cD (skS.0 2 a a_2)) True) % 35.73/35.93 (Or (Eq (cD (skS.0 2 a a_3)) True) (Or (Eq False True) (Eq (skS.0 0 a (skS.0 3 a a_4)) True)))) % 35.73/35.93 Clause #6695 (by clausification #[6694]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 a_4 : Iota), % 35.73/35.93 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) % 35.73/35.93 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (cD (skS.0 2 a a_3)) True) (Eq (skS.0 0 a (skS.0 3 a a_4)) True))) % 35.73/35.93 Clause #6714 (by equality factoring #[6695]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.73/35.93 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.73/35.93 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Ne True True) (Eq (skS.0 0 a (skS.0 3 a a_3)) True))) % 35.73/35.93 Clause #6718 (by clausification #[6714]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.73/35.93 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.73/35.93 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a (skS.0 3 a a_3)) True) (Or (Eq True False) (Eq True False)))) % 35.73/35.93 Clause #6720 (by clausification #[6718]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.73/35.93 Or (Eq (cD (skS.0 2 a a_1)) True) % 35.73/35.93 (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq (skS.0 0 a (skS.0 3 a a_3)) True) (Eq True False))) % 35.73/35.93 Clause #6721 (by clausification #[6720]): ∀ (a : Iota → Prop) (a_1 a_2 a_3 : Iota), % 35.73/35.93 Or (Eq (cD (skS.0 2 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Eq (skS.0 0 a (skS.0 3 a a_3)) True)) % 35.73/35.93 Clause #6732 (by equality factoring #[6721]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.93 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Or (Ne True True) (Eq (cD (skS.0 2 a a_2)) True)) % 35.73/35.93 Clause #6733 (by clausification #[6732]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.93 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Or (Eq True False) (Eq True False))) % 35.73/35.93 Clause #6735 (by clausification #[6733]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.93 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Eq True False)) % 35.73/35.93 Clause #6736 (by clausification #[6735]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Eq (cD (skS.0 2 a a_2)) True) % 35.73/35.93 Clause #6744 (by superposition #[6736, 5362]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.93 Or (Eq (skS.0 0 (fun x => a x) (skS.0 3 (fun x => a x) a_1)) True) % 35.73/35.93 (Or (Eq True False) (Eq (skS.0 0 a (skS.0 3 a a_2)) True)) % 35.73/35.93 Clause #6771 (by betaEtaReduce #[6744]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.93 Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Or (Eq True False) (Eq (skS.0 0 a (skS.0 3 a a_2)) True)) % 35.73/35.93 Clause #6772 (by clausification #[6771]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Eq (skS.0 0 a (skS.0 3 a a_2)) True) % 35.73/35.93 Clause #6781 (by equality factoring #[6772]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Ne True True) (Eq (skS.0 0 a (skS.0 3 a a_1)) True) % 35.73/35.93 Clause #6782 (by clausification #[6781]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Or (Eq True False) (Eq True False)) % 35.73/35.93 Clause #6784 (by clausification #[6782]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (skS.0 0 a (skS.0 3 a a_1)) True) (Eq True False) % 35.73/35.93 Clause #6785 (by clausification #[6784]): ∀ (a : Iota → Prop) (a_1 : Iota), Eq (skS.0 0 a (skS.0 3 a a_1)) True % 35.73/35.93 Clause #6786 (by superposition #[6785, 26]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.93 Or (Eq True False) (Or (Eq (cE (skS.0 3 a a_1)) True) (Or (Eq (skS.0 0 a a_2) False) (Eq (cE a_2) True))) % 35.73/35.93 Clause #6794 (by clausification #[6786]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.93 Or (Eq (cE (skS.0 3 a a_1)) True) (Or (Eq (skS.0 0 a a_2) False) (Eq (cE a_2) True)) % 35.73/35.93 Clause #6796 (by superposition #[6794, 6785]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.93 Or (Eq (cE (skS.0 3 (fun x => a x) a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Eq False True)) % 35.73/35.93 Clause #6797 (by betaEtaReduce #[6796]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.73/35.93 Or (Eq (cE (skS.0 3 a a_1)) True) (Or (Eq (cE (skS.0 3 a a_2)) True) (Eq False True)) % 35.84/36.00 Clause #6798 (by clausification #[6797]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (cE (skS.0 3 a a_1)) True) (Eq (cE (skS.0 3 a a_2)) True) % 35.84/36.00 Clause #6800 (by equality factoring #[6798]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Ne True True) (Eq (cE (skS.0 3 a a_1)) True) % 35.84/36.00 Clause #6803 (by clausification #[6800]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (cE (skS.0 3 a a_1)) True) (Or (Eq True False) (Eq True False)) % 35.84/36.00 Clause #6805 (by clausification #[6803]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (cE (skS.0 3 a a_1)) True) (Eq True False) % 35.84/36.00 Clause #6806 (by clausification #[6805]): ∀ (a : Iota → Prop) (a_1 : Iota), Eq (cE (skS.0 3 a a_1)) True % 35.84/36.00 Clause #6807 (by superposition #[6806, 5358]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (skS.0 0 a (skS.0 2 a a_1)) True) (Eq True False) % 35.84/36.00 Clause #6808 (by clausification #[6807]): ∀ (a : Iota → Prop) (a_1 : Iota), Eq (skS.0 0 a (skS.0 2 a a_1)) True % 35.84/36.00 Clause #6812 (by superposition #[6808, 42]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.84/36.00 Or (Eq True False) (Or (Eq (cD (skS.0 2 a a_1)) True) (Or (Eq (skS.0 0 a a_2) False) (Eq (cD a_2) True))) % 35.84/36.00 Clause #6826 (by clausification #[6812]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.84/36.00 Or (Eq (cD (skS.0 2 a a_1)) True) (Or (Eq (skS.0 0 a a_2) False) (Eq (cD a_2) True)) % 35.84/36.00 Clause #6829 (by superposition #[6826, 6808]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.84/36.00 Or (Eq (cD (skS.0 2 (fun x => a x) a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Eq False True)) % 35.84/36.00 Clause #6832 (by betaEtaReduce #[6829]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), % 35.84/36.00 Or (Eq (cD (skS.0 2 a a_1)) True) (Or (Eq (cD (skS.0 2 a a_2)) True) (Eq False True)) % 35.84/36.00 Clause #6833 (by clausification #[6832]): ∀ (a : Iota → Prop) (a_1 a_2 : Iota), Or (Eq (cD (skS.0 2 a a_1)) True) (Eq (cD (skS.0 2 a a_2)) True) % 35.84/36.00 Clause #6835 (by equality factoring #[6833]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Ne True True) (Eq (cD (skS.0 2 a a_1)) True) % 35.84/36.00 Clause #6836 (by clausification #[6835]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (cD (skS.0 2 a a_1)) True) (Or (Eq True False) (Eq True False)) % 35.84/36.00 Clause #6838 (by clausification #[6836]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq (cD (skS.0 2 a a_1)) True) (Eq True False) % 35.84/36.00 Clause #6839 (by clausification #[6838]): ∀ (a : Iota → Prop) (a_1 : Iota), Eq (cD (skS.0 2 a a_1)) True % 35.84/36.00 Clause #6840 (by superposition #[6839, 5356]): ∀ (a : Iota → Prop) (a_1 : Iota), Or (Eq True False) (Eq (cE (skS.0 3 a a_1)) False) % 35.84/36.00 Clause #6841 (by clausification #[6840]): ∀ (a : Iota → Prop) (a_1 : Iota), Eq (cE (skS.0 3 a a_1)) False % 35.84/36.00 Clause #6842 (by superposition #[6841, 6806]): Eq False True % 35.84/36.00 Clause #6843 (by clausification #[6842]): False % 35.84/36.00 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------