%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LAT313+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n002.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:53:17 PM UTC 2025 % Result : Theorem 28.71s 28.90s % Output : Proof 28.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : LAT313+1 : TPTP v9.2.0. Released v3.4.0. % 0.07/0.13 % Command : duper %s % 0.12/0.34 % Computer : n002.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 18:34:08 EDT 2025 % 0.12/0.34 % CPUTime : % 28.71/28.90 SZS status Theorem for theBenchmark.p % 28.71/28.90 SZS output start Proof for theBenchmark.p % 28.71/28.90 Clause #0 (by assumption #[]): Eq % 28.71/28.90 (Not % 28.71/28.90 (∀ (A : Iota), % 28.71/28.90 And (And (Not (v3_struct_0 A)) (v10_lattices A)) (l3_lattices A) → % 28.71/28.90 ∀ (B : Iota), % 28.71/28.90 m2_filter_2 B A → % 28.71/28.90 And (v14_lattices A) (r2_hidden (k6_lattices A) B) → % 28.71/28.90 And (r1_filter_2 (u1_struct_0 A) B (k17_filter_2 A)) (Eq B (u1_struct_0 A)))) % 28.71/28.90 True % 28.71/28.90 Clause #5 (by assumption #[]): Eq % 28.71/28.90 (∀ (A : Iota), And (And (Not (v3_struct_0 A)) (v10_lattices A)) (l3_lattices A) → Eq (k17_filter_2 A) (u1_struct_0 A)) % 28.71/28.90 True % 28.71/28.90 Clause #10 (by assumption #[]): Eq (∀ (A : Iota), l1_lattices A → l1_struct_0 A) True % 28.71/28.90 Clause #12 (by assumption #[]): Eq (∀ (A : Iota), l3_lattices A → And (l1_lattices A) (l2_lattices A)) True % 28.71/28.90 Clause #13 (by assumption #[]): Eq % 28.71/28.90 (∀ (A : Iota), % 28.71/28.90 And (And (Not (v3_struct_0 A)) (v10_lattices A)) (l3_lattices A) → % 28.71/28.90 ∀ (B : Iota), m2_filter_2 B A → And (Not (v1_xboole_0 B)) (m2_lattice4 B A)) % 28.71/28.90 True % 28.71/28.90 Clause #14 (by assumption #[]): Eq % 28.71/28.90 (∀ (A : Iota), % 28.71/28.90 And (And (Not (v3_struct_0 A)) (v10_lattices A)) (l3_lattices A) → % 28.71/28.90 ∀ (B : Iota), m2_lattice4 B A → m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) % 28.71/28.90 True % 28.71/28.90 Clause #22 (by assumption #[]): Eq (∀ (A : Iota), And (Not (v3_struct_0 A)) (l1_struct_0 A) → Not (v1_xboole_0 (u1_struct_0 A))) True % 28.71/28.90 Clause #32 (by assumption #[]): Eq % 28.71/28.90 (∀ (A B C : Iota), % 28.71/28.90 And (And (Not (v1_xboole_0 A)) (m1_subset_1 B (k1_zfmisc_1 A))) (m1_subset_1 C (k1_zfmisc_1 A)) → % 28.71/28.90 Iff (r1_filter_2 A B C) (Eq B C)) % 28.71/28.90 True % 28.71/28.90 Clause #33 (by assumption #[]): Eq % 28.71/28.90 (∀ (A B C : Iota), % 28.71/28.90 And (And (Not (v1_xboole_0 A)) (m1_subset_1 B (k1_zfmisc_1 A))) (m1_subset_1 C (k1_zfmisc_1 A)) → r1_filter_2 A B B) % 28.71/28.90 True % 28.71/28.90 Clause #34 (by assumption #[]): Eq (∀ (A : Iota), Iota → r1_tarski A A) True % 28.71/28.90 Clause #38 (by assumption #[]): Eq % 28.71/28.90 (∀ (A : Iota), % 28.71/28.90 And (And (Not (v3_struct_0 A)) (v10_lattices A)) (l3_lattices A) → % 28.71/28.90 ∀ (B : Iota), m2_filter_2 B A → r1_filter_2 (u1_struct_0 A) (k19_filter_2 A B) B) % 28.71/28.90 True % 28.71/28.90 Clause #39 (by assumption #[]): Eq (∀ (A B : Iota), Iff (m1_subset_1 A (k1_zfmisc_1 B)) (r1_tarski A B)) True % 28.71/28.90 Clause #40 (by assumption #[]): Eq % 28.71/28.90 (∀ (A : Iota), % 28.71/28.90 And (And (Not (v3_struct_0 A)) (v10_lattices A)) (l3_lattices A) → % 28.71/28.90 ∀ (B : Iota), % 28.71/28.90 And (Not (v1_xboole_0 B)) (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) → % 28.71/28.90 And (v14_lattices A) (r2_hidden (k6_lattices A) B) → % 28.71/28.90 And (r1_filter_2 (u1_struct_0 A) (k19_filter_2 A B) (k17_filter_2 A)) % 28.71/28.90 (Eq (k19_filter_2 A B) (u1_struct_0 A))) % 28.71/28.90 True % 28.71/28.90 Clause #48 (by clausification #[10]): ∀ (a : Iota), Eq (l1_lattices a → l1_struct_0 a) True % 28.71/28.90 Clause #49 (by clausification #[48]): ∀ (a : Iota), Or (Eq (l1_lattices a) False) (Eq (l1_struct_0 a) True) % 28.71/28.90 Clause #53 (by clausification #[0]): Eq % 28.71/28.90 (∀ (A : Iota), % 28.71/28.90 And (And (Not (v3_struct_0 A)) (v10_lattices A)) (l3_lattices A) → % 28.71/28.90 ∀ (B : Iota), % 28.71/28.90 m2_filter_2 B A → % 28.71/28.90 And (v14_lattices A) (r2_hidden (k6_lattices A) B) → % 28.71/28.90 And (r1_filter_2 (u1_struct_0 A) B (k17_filter_2 A)) (Eq B (u1_struct_0 A))) % 28.71/28.90 False % 28.71/28.90 Clause #54 (by clausification #[53]): ∀ (a : Iota), % 28.71/28.90 Eq % 28.71/28.90 (Not % 28.71/28.90 (And (And (Not (v3_struct_0 (skS.0 0 a))) (v10_lattices (skS.0 0 a))) (l3_lattices (skS.0 0 a)) → % 28.71/28.90 ∀ (B : Iota), % 28.71/28.90 m2_filter_2 B (skS.0 0 a) → % 28.71/28.90 And (v14_lattices (skS.0 0 a)) (r2_hidden (k6_lattices (skS.0 0 a)) B) → % 28.71/28.90 And (r1_filter_2 (u1_struct_0 (skS.0 0 a)) B (k17_filter_2 (skS.0 0 a))) % 28.71/28.90 (Eq B (u1_struct_0 (skS.0 0 a))))) % 28.71/28.90 True % 28.71/28.90 Clause #55 (by clausification #[54]): ∀ (a : Iota), % 28.71/28.90 Eq % 28.71/28.90 (And (And (Not (v3_struct_0 (skS.0 0 a))) (v10_lattices (skS.0 0 a))) (l3_lattices (skS.0 0 a)) → % 28.71/28.90 ∀ (B : Iota), % 28.71/28.90 m2_filter_2 B (skS.0 0 a) → % 28.71/28.90 And (v14_lattices (skS.0 0 a)) (r2_hidden (k6_lattices (skS.0 0 a)) B) → % 28.71/28.90 And (r1_filter_2 (u1_struct_0 (skS.0 0 a)) B (k17_filter_2 (skS.0 0 a))) (Eq B (u1_struct_0 (skS.0 0 a)))) % 28.71/28.90 False % 28.71/28.93 Clause #56 (by clausification #[55]): ∀ (a : Iota), Eq (And (And (Not (v3_struct_0 (skS.0 0 a))) (v10_lattices (skS.0 0 a))) (l3_lattices (skS.0 0 a))) True % 28.71/28.93 Clause #57 (by clausification #[55]): ∀ (a : Iota), % 28.71/28.93 Eq % 28.71/28.93 (∀ (B : Iota), % 28.71/28.93 m2_filter_2 B (skS.0 0 a) → % 28.71/28.93 And (v14_lattices (skS.0 0 a)) (r2_hidden (k6_lattices (skS.0 0 a)) B) → % 28.71/28.93 And (r1_filter_2 (u1_struct_0 (skS.0 0 a)) B (k17_filter_2 (skS.0 0 a))) (Eq B (u1_struct_0 (skS.0 0 a)))) % 28.71/28.93 False % 28.71/28.93 Clause #58 (by clausification #[56]): ∀ (a : Iota), Eq (l3_lattices (skS.0 0 a)) True % 28.71/28.93 Clause #59 (by clausification #[56]): ∀ (a : Iota), Eq (And (Not (v3_struct_0 (skS.0 0 a))) (v10_lattices (skS.0 0 a))) True % 28.71/28.93 Clause #74 (by clausification #[34]): ∀ (a : Iota), Eq (Iota → r1_tarski a a) True % 28.71/28.93 Clause #75 (by clausification #[74]): ∀ (a : Iota), Iota → Eq (r1_tarski a a) True % 28.71/28.93 Clause #100 (by clausification #[22]): ∀ (a : Iota), Eq (And (Not (v3_struct_0 a)) (l1_struct_0 a) → Not (v1_xboole_0 (u1_struct_0 a))) True % 28.71/28.93 Clause #101 (by clausification #[100]): ∀ (a : Iota), Or (Eq (And (Not (v3_struct_0 a)) (l1_struct_0 a)) False) (Eq (Not (v1_xboole_0 (u1_struct_0 a))) True) % 28.71/28.93 Clause #102 (by clausification #[101]): ∀ (a : Iota), % 28.71/28.93 Or (Eq (Not (v1_xboole_0 (u1_struct_0 a))) True) (Or (Eq (Not (v3_struct_0 a)) False) (Eq (l1_struct_0 a) False)) % 28.71/28.93 Clause #103 (by clausification #[102]): ∀ (a : Iota), % 28.71/28.93 Or (Eq (Not (v3_struct_0 a)) False) (Or (Eq (l1_struct_0 a) False) (Eq (v1_xboole_0 (u1_struct_0 a)) False)) % 28.71/28.93 Clause #104 (by clausification #[103]): ∀ (a : Iota), Or (Eq (l1_struct_0 a) False) (Or (Eq (v1_xboole_0 (u1_struct_0 a)) False) (Eq (v3_struct_0 a) True)) % 28.71/28.93 Clause #115 (by clausification #[12]): ∀ (a : Iota), Eq (l3_lattices a → And (l1_lattices a) (l2_lattices a)) True % 28.71/28.93 Clause #116 (by clausification #[115]): ∀ (a : Iota), Or (Eq (l3_lattices a) False) (Eq (And (l1_lattices a) (l2_lattices a)) True) % 28.71/28.93 Clause #118 (by clausification #[116]): ∀ (a : Iota), Or (Eq (l3_lattices a) False) (Eq (l1_lattices a) True) % 28.71/28.93 Clause #135 (by superposition #[118, 58]): ∀ (a : Iota), Or (Eq (l1_lattices (skS.0 0 a)) True) (Eq False True) % 28.71/28.93 Clause #159 (by clausification #[5]): ∀ (a : Iota), % 28.71/28.93 Eq (And (And (Not (v3_struct_0 a)) (v10_lattices a)) (l3_lattices a) → Eq (k17_filter_2 a) (u1_struct_0 a)) True % 28.71/28.93 Clause #160 (by clausification #[159]): ∀ (a : Iota), % 28.71/28.93 Or (Eq (And (And (Not (v3_struct_0 a)) (v10_lattices a)) (l3_lattices a)) False) % 28.71/28.93 (Eq (Eq (k17_filter_2 a) (u1_struct_0 a)) True) % 28.71/28.93 Clause #161 (by clausification #[160]): ∀ (a : Iota), % 28.71/28.93 Or (Eq (Eq (k17_filter_2 a) (u1_struct_0 a)) True) % 28.71/28.93 (Or (Eq (And (Not (v3_struct_0 a)) (v10_lattices a)) False) (Eq (l3_lattices a) False)) % 28.71/28.93 Clause #162 (by clausification #[161]): ∀ (a : Iota), % 28.71/28.93 Or (Eq (And (Not (v3_struct_0 a)) (v10_lattices a)) False) % 28.71/28.93 (Or (Eq (l3_lattices a) False) (Eq (k17_filter_2 a) (u1_struct_0 a))) % 28.71/28.93 Clause #163 (by clausification #[162]): ∀ (a : Iota), % 28.71/28.93 Or (Eq (l3_lattices a) False) % 28.71/28.93 (Or (Eq (k17_filter_2 a) (u1_struct_0 a)) (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v10_lattices a) False))) % 28.71/28.93 Clause #164 (by clausification #[163]): ∀ (a : Iota), % 28.71/28.93 Or (Eq (l3_lattices a) False) % 28.71/28.93 (Or (Eq (k17_filter_2 a) (u1_struct_0 a)) (Or (Eq (v10_lattices a) False) (Eq (v3_struct_0 a) True))) % 28.71/28.93 Clause #165 (by superposition #[164, 58]): ∀ (a : Iota), % 28.71/28.93 Or (Eq (k17_filter_2 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a))) % 28.71/28.93 (Or (Eq (v10_lattices (skS.0 0 a)) False) (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq False True))) % 28.71/28.93 Clause #183 (by clausification #[33]): ∀ (a : Iota), % 28.71/28.93 Eq % 28.71/28.93 (∀ (B C : Iota), % 28.71/28.93 And (And (Not (v1_xboole_0 a)) (m1_subset_1 B (k1_zfmisc_1 a))) (m1_subset_1 C (k1_zfmisc_1 a)) → % 28.71/28.93 r1_filter_2 a B B) % 28.71/28.93 True % 28.71/28.93 Clause #184 (by clausification #[183]): ∀ (a a_1 : Iota), % 28.71/28.93 Eq % 28.71/28.93 (∀ (C : Iota), % 28.71/28.93 And (And (Not (v1_xboole_0 a)) (m1_subset_1 a_1 (k1_zfmisc_1 a))) (m1_subset_1 C (k1_zfmisc_1 a)) → % 28.71/28.93 r1_filter_2 a a_1 a_1) % 28.71/28.93 True % 28.71/28.93 Clause #185 (by clausification #[184]): ∀ (a a_1 a_2 : Iota), % 28.71/28.93 Eq % 28.71/28.93 (And (And (Not (v1_xboole_0 a)) (m1_subset_1 a_1 (k1_zfmisc_1 a))) (m1_subset_1 a_2 (k1_zfmisc_1 a)) → % 28.79/28.95 r1_filter_2 a a_1 a_1) % 28.79/28.95 True % 28.79/28.95 Clause #186 (by clausification #[185]): ∀ (a a_1 a_2 : Iota), % 28.79/28.95 Or (Eq (And (And (Not (v1_xboole_0 a)) (m1_subset_1 a_1 (k1_zfmisc_1 a))) (m1_subset_1 a_2 (k1_zfmisc_1 a))) False) % 28.79/28.95 (Eq (r1_filter_2 a a_1 a_1) True) % 28.79/28.95 Clause #187 (by clausification #[186]): ∀ (a a_1 a_2 : Iota), % 28.79/28.95 Or (Eq (r1_filter_2 a a_1 a_1) True) % 28.79/28.95 (Or (Eq (And (Not (v1_xboole_0 a)) (m1_subset_1 a_1 (k1_zfmisc_1 a))) False) % 28.79/28.95 (Eq (m1_subset_1 a_2 (k1_zfmisc_1 a)) False)) % 28.79/28.95 Clause #188 (by clausification #[187]): ∀ (a a_1 a_2 : Iota), % 28.79/28.95 Or (Eq (r1_filter_2 a a_1 a_1) True) % 28.79/28.95 (Or (Eq (m1_subset_1 a_2 (k1_zfmisc_1 a)) False) % 28.79/28.95 (Or (Eq (Not (v1_xboole_0 a)) False) (Eq (m1_subset_1 a_1 (k1_zfmisc_1 a)) False))) % 28.79/28.95 Clause #189 (by clausification #[188]): ∀ (a a_1 a_2 : Iota), % 28.79/28.95 Or (Eq (r1_filter_2 a a_1 a_1) True) % 28.79/28.95 (Or (Eq (m1_subset_1 a_2 (k1_zfmisc_1 a)) False) % 28.79/28.95 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 a)) False) (Eq (v1_xboole_0 a) True))) % 28.79/28.95 Clause #197 (by clausification #[13]): ∀ (a : Iota), % 28.79/28.95 Eq % 28.79/28.95 (And (And (Not (v3_struct_0 a)) (v10_lattices a)) (l3_lattices a) → % 28.79/28.95 ∀ (B : Iota), m2_filter_2 B a → And (Not (v1_xboole_0 B)) (m2_lattice4 B a)) % 28.79/28.95 True % 28.79/28.95 Clause #198 (by clausification #[197]): ∀ (a : Iota), % 28.79/28.95 Or (Eq (And (And (Not (v3_struct_0 a)) (v10_lattices a)) (l3_lattices a)) False) % 28.79/28.95 (Eq (∀ (B : Iota), m2_filter_2 B a → And (Not (v1_xboole_0 B)) (m2_lattice4 B a)) True) % 28.79/28.95 Clause #199 (by clausification #[198]): ∀ (a : Iota), % 28.79/28.95 Or (Eq (∀ (B : Iota), m2_filter_2 B a → And (Not (v1_xboole_0 B)) (m2_lattice4 B a)) True) % 28.79/28.95 (Or (Eq (And (Not (v3_struct_0 a)) (v10_lattices a)) False) (Eq (l3_lattices a) False)) % 28.79/28.95 Clause #200 (by clausification #[199]): ∀ (a a_1 : Iota), % 28.79/28.95 Or (Eq (And (Not (v3_struct_0 a)) (v10_lattices a)) False) % 28.79/28.95 (Or (Eq (l3_lattices a) False) (Eq (m2_filter_2 a_1 a → And (Not (v1_xboole_0 a_1)) (m2_lattice4 a_1 a)) True)) % 28.79/28.95 Clause #201 (by clausification #[200]): ∀ (a a_1 : Iota), % 28.79/28.95 Or (Eq (l3_lattices a) False) % 28.79/28.95 (Or (Eq (m2_filter_2 a_1 a → And (Not (v1_xboole_0 a_1)) (m2_lattice4 a_1 a)) True) % 28.79/28.95 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v10_lattices a) False))) % 28.79/28.95 Clause #202 (by clausification #[201]): ∀ (a a_1 : Iota), % 28.79/28.95 Or (Eq (l3_lattices a) False) % 28.79/28.95 (Or (Eq (Not (v3_struct_0 a)) False) % 28.79/28.95 (Or (Eq (v10_lattices a) False) % 28.79/28.95 (Or (Eq (m2_filter_2 a_1 a) False) (Eq (And (Not (v1_xboole_0 a_1)) (m2_lattice4 a_1 a)) True)))) % 28.79/28.95 Clause #203 (by clausification #[202]): ∀ (a a_1 : Iota), % 28.79/28.95 Or (Eq (l3_lattices a) False) % 28.79/28.95 (Or (Eq (v10_lattices a) False) % 28.79/28.95 (Or (Eq (m2_filter_2 a_1 a) False) % 28.79/28.95 (Or (Eq (And (Not (v1_xboole_0 a_1)) (m2_lattice4 a_1 a)) True) (Eq (v3_struct_0 a) True)))) % 28.79/28.95 Clause #204 (by clausification #[203]): ∀ (a a_1 : Iota), % 28.79/28.95 Or (Eq (l3_lattices a) False) % 28.79/28.95 (Or (Eq (v10_lattices a) False) % 28.79/28.95 (Or (Eq (m2_filter_2 a_1 a) False) (Or (Eq (v3_struct_0 a) True) (Eq (m2_lattice4 a_1 a) True)))) % 28.79/28.95 Clause #205 (by clausification #[203]): ∀ (a a_1 : Iota), % 28.79/28.95 Or (Eq (l3_lattices a) False) % 28.79/28.95 (Or (Eq (v10_lattices a) False) % 28.79/28.95 (Or (Eq (m2_filter_2 a_1 a) False) (Or (Eq (v3_struct_0 a) True) (Eq (Not (v1_xboole_0 a_1)) True)))) % 28.79/28.95 Clause #206 (by superposition #[204, 58]): ∀ (a a_1 : Iota), % 28.79/28.95 Or (Eq (v10_lattices (skS.0 0 a)) False) % 28.79/28.95 (Or (Eq (m2_filter_2 a_1 (skS.0 0 a)) False) % 28.79/28.95 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Or (Eq (m2_lattice4 a_1 (skS.0 0 a)) True) (Eq False True)))) % 28.79/28.95 Clause #211 (by clausification #[14]): ∀ (a : Iota), % 28.79/28.95 Eq % 28.79/28.95 (And (And (Not (v3_struct_0 a)) (v10_lattices a)) (l3_lattices a) → % 28.79/28.95 ∀ (B : Iota), m2_lattice4 B a → m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a))) % 28.79/28.95 True % 28.79/28.95 Clause #212 (by clausification #[211]): ∀ (a : Iota), % 28.79/28.95 Or (Eq (And (And (Not (v3_struct_0 a)) (v10_lattices a)) (l3_lattices a)) False) % 28.79/28.95 (Eq (∀ (B : Iota), m2_lattice4 B a → m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a))) True) % 28.79/28.95 Clause #213 (by clausification #[212]): ∀ (a : Iota), % 28.79/28.95 Or (Eq (∀ (B : Iota), m2_lattice4 B a → m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a))) True) % 28.81/28.98 (Or (Eq (And (Not (v3_struct_0 a)) (v10_lattices a)) False) (Eq (l3_lattices a) False)) % 28.81/28.98 Clause #214 (by clausification #[213]): ∀ (a a_1 : Iota), % 28.81/28.98 Or (Eq (And (Not (v3_struct_0 a)) (v10_lattices a)) False) % 28.81/28.98 (Or (Eq (l3_lattices a) False) (Eq (m2_lattice4 a_1 a → m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) True)) % 28.81/28.98 Clause #215 (by clausification #[214]): ∀ (a a_1 : Iota), % 28.81/28.98 Or (Eq (l3_lattices a) False) % 28.81/28.98 (Or (Eq (m2_lattice4 a_1 a → m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) True) % 28.81/28.98 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v10_lattices a) False))) % 28.81/28.98 Clause #216 (by clausification #[215]): ∀ (a a_1 : Iota), % 28.81/28.98 Or (Eq (l3_lattices a) False) % 28.81/28.98 (Or (Eq (Not (v3_struct_0 a)) False) % 28.81/28.98 (Or (Eq (v10_lattices a) False) % 28.81/28.98 (Or (Eq (m2_lattice4 a_1 a) False) (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) True)))) % 28.81/28.98 Clause #217 (by clausification #[216]): ∀ (a a_1 : Iota), % 28.81/28.98 Or (Eq (l3_lattices a) False) % 28.81/28.98 (Or (Eq (v10_lattices a) False) % 28.81/28.98 (Or (Eq (m2_lattice4 a_1 a) False) % 28.81/28.98 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) True) (Eq (v3_struct_0 a) True)))) % 28.81/28.98 Clause #218 (by superposition #[217, 58]): ∀ (a a_1 : Iota), % 28.81/28.98 Or (Eq (v10_lattices (skS.0 0 a)) False) % 28.81/28.98 (Or (Eq (m2_lattice4 a_1 (skS.0 0 a)) False) % 28.81/28.98 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 28.81/28.98 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq False True)))) % 28.81/28.98 Clause #247 (by clausification #[135]): ∀ (a : Iota), Eq (l1_lattices (skS.0 0 a)) True % 28.81/28.98 Clause #248 (by superposition #[247, 49]): ∀ (a : Iota), Or (Eq True False) (Eq (l1_struct_0 (skS.0 0 a)) True) % 28.81/28.98 Clause #249 (by clausification #[248]): ∀ (a : Iota), Eq (l1_struct_0 (skS.0 0 a)) True % 28.81/28.98 Clause #250 (by superposition #[249, 104]): ∀ (a : Iota), % 28.81/28.98 Or (Eq True False) (Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 0 a))) False) (Eq (v3_struct_0 (skS.0 0 a)) True)) % 28.81/28.98 Clause #270 (by clausification #[39]): ∀ (a : Iota), Eq (∀ (B : Iota), Iff (m1_subset_1 a (k1_zfmisc_1 B)) (r1_tarski a B)) True % 28.81/28.98 Clause #271 (by clausification #[270]): ∀ (a a_1 : Iota), Eq (Iff (m1_subset_1 a (k1_zfmisc_1 a_1)) (r1_tarski a a_1)) True % 28.81/28.98 Clause #272 (by clausification #[271]): ∀ (a a_1 : Iota), Or (Eq (m1_subset_1 a (k1_zfmisc_1 a_1)) True) (Eq (r1_tarski a a_1) False) % 28.81/28.98 Clause #274 (by superposition #[272, 75]): ∀ (a : Iota), Or (Eq (m1_subset_1 a (k1_zfmisc_1 a)) True) (Eq False True) % 28.81/28.98 Clause #281 (by clausification #[274]): ∀ (a : Iota), Eq (m1_subset_1 a (k1_zfmisc_1 a)) True % 28.81/28.98 Clause #313 (by clausification #[38]): ∀ (a : Iota), % 28.81/28.98 Eq % 28.81/28.98 (And (And (Not (v3_struct_0 a)) (v10_lattices a)) (l3_lattices a) → % 28.81/28.98 ∀ (B : Iota), m2_filter_2 B a → r1_filter_2 (u1_struct_0 a) (k19_filter_2 a B) B) % 28.81/28.98 True % 28.81/28.98 Clause #314 (by clausification #[313]): ∀ (a : Iota), % 28.81/28.98 Or (Eq (And (And (Not (v3_struct_0 a)) (v10_lattices a)) (l3_lattices a)) False) % 28.81/28.98 (Eq (∀ (B : Iota), m2_filter_2 B a → r1_filter_2 (u1_struct_0 a) (k19_filter_2 a B) B) True) % 28.81/28.98 Clause #315 (by clausification #[314]): ∀ (a : Iota), % 28.81/28.98 Or (Eq (∀ (B : Iota), m2_filter_2 B a → r1_filter_2 (u1_struct_0 a) (k19_filter_2 a B) B) True) % 28.81/28.98 (Or (Eq (And (Not (v3_struct_0 a)) (v10_lattices a)) False) (Eq (l3_lattices a) False)) % 28.81/28.98 Clause #316 (by clausification #[315]): ∀ (a a_1 : Iota), % 28.81/28.98 Or (Eq (And (Not (v3_struct_0 a)) (v10_lattices a)) False) % 28.81/28.98 (Or (Eq (l3_lattices a) False) (Eq (m2_filter_2 a_1 a → r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) a_1) True)) % 28.81/28.98 Clause #317 (by clausification #[316]): ∀ (a a_1 : Iota), % 28.81/28.98 Or (Eq (l3_lattices a) False) % 28.81/28.98 (Or (Eq (m2_filter_2 a_1 a → r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) a_1) True) % 28.81/28.98 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v10_lattices a) False))) % 28.81/28.98 Clause #318 (by clausification #[317]): ∀ (a a_1 : Iota), % 28.81/28.98 Or (Eq (l3_lattices a) False) % 28.81/28.98 (Or (Eq (Not (v3_struct_0 a)) False) % 28.81/28.98 (Or (Eq (v10_lattices a) False) % 28.81/28.98 (Or (Eq (m2_filter_2 a_1 a) False) (Eq (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) a_1) True)))) % 28.81/28.98 Clause #319 (by clausification #[318]): ∀ (a a_1 : Iota), % 28.81/29.00 Or (Eq (l3_lattices a) False) % 28.81/29.00 (Or (Eq (v10_lattices a) False) % 28.81/29.00 (Or (Eq (m2_filter_2 a_1 a) False) % 28.81/29.00 (Or (Eq (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) a_1) True) (Eq (v3_struct_0 a) True)))) % 28.81/29.00 Clause #320 (by superposition #[319, 58]): ∀ (a a_1 : Iota), % 28.81/29.00 Or (Eq (v10_lattices (skS.0 0 a)) False) % 28.81/29.00 (Or (Eq (m2_filter_2 a_1 (skS.0 0 a)) False) % 28.81/29.00 (Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (k19_filter_2 (skS.0 0 a) a_1) a_1) True) % 28.81/29.00 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq False True)))) % 28.81/29.00 Clause #322 (by clausification #[32]): ∀ (a : Iota), % 28.81/29.00 Eq % 28.81/29.00 (∀ (B C : Iota), % 28.81/29.00 And (And (Not (v1_xboole_0 a)) (m1_subset_1 B (k1_zfmisc_1 a))) (m1_subset_1 C (k1_zfmisc_1 a)) → % 28.81/29.00 Iff (r1_filter_2 a B C) (Eq B C)) % 28.81/29.00 True % 28.81/29.00 Clause #323 (by clausification #[322]): ∀ (a a_1 : Iota), % 28.81/29.00 Eq % 28.81/29.00 (∀ (C : Iota), % 28.81/29.00 And (And (Not (v1_xboole_0 a)) (m1_subset_1 a_1 (k1_zfmisc_1 a))) (m1_subset_1 C (k1_zfmisc_1 a)) → % 28.81/29.00 Iff (r1_filter_2 a a_1 C) (Eq a_1 C)) % 28.81/29.00 True % 28.81/29.00 Clause #324 (by clausification #[323]): ∀ (a a_1 a_2 : Iota), % 28.81/29.00 Eq % 28.81/29.00 (And (And (Not (v1_xboole_0 a)) (m1_subset_1 a_1 (k1_zfmisc_1 a))) (m1_subset_1 a_2 (k1_zfmisc_1 a)) → % 28.81/29.00 Iff (r1_filter_2 a a_1 a_2) (Eq a_1 a_2)) % 28.81/29.00 True % 28.81/29.00 Clause #325 (by clausification #[324]): ∀ (a a_1 a_2 : Iota), % 28.81/29.00 Or (Eq (And (And (Not (v1_xboole_0 a)) (m1_subset_1 a_1 (k1_zfmisc_1 a))) (m1_subset_1 a_2 (k1_zfmisc_1 a))) False) % 28.81/29.00 (Eq (Iff (r1_filter_2 a a_1 a_2) (Eq a_1 a_2)) True) % 28.81/29.00 Clause #326 (by clausification #[325]): ∀ (a a_1 a_2 : Iota), % 28.81/29.00 Or (Eq (Iff (r1_filter_2 a a_1 a_2) (Eq a_1 a_2)) True) % 28.81/29.00 (Or (Eq (And (Not (v1_xboole_0 a)) (m1_subset_1 a_1 (k1_zfmisc_1 a))) False) % 28.81/29.00 (Eq (m1_subset_1 a_2 (k1_zfmisc_1 a)) False)) % 28.81/29.00 Clause #328 (by clausification #[326]): ∀ (a a_1 a_2 : Iota), % 28.81/29.00 Or (Eq (And (Not (v1_xboole_0 a)) (m1_subset_1 a_1 (k1_zfmisc_1 a))) False) % 28.81/29.00 (Or (Eq (m1_subset_1 a_2 (k1_zfmisc_1 a)) False) (Or (Eq (r1_filter_2 a a_1 a_2) False) (Eq (Eq a_1 a_2) True))) % 28.81/29.00 Clause #346 (by clausification #[40]): ∀ (a : Iota), % 28.81/29.00 Eq % 28.81/29.00 (And (And (Not (v3_struct_0 a)) (v10_lattices a)) (l3_lattices a) → % 28.81/29.00 ∀ (B : Iota), % 28.81/29.00 And (Not (v1_xboole_0 B)) (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a))) → % 28.81/29.00 And (v14_lattices a) (r2_hidden (k6_lattices a) B) → % 28.81/29.00 And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a B) (k17_filter_2 a)) % 28.81/29.00 (Eq (k19_filter_2 a B) (u1_struct_0 a))) % 28.81/29.00 True % 28.81/29.00 Clause #347 (by clausification #[346]): ∀ (a : Iota), % 28.81/29.00 Or (Eq (And (And (Not (v3_struct_0 a)) (v10_lattices a)) (l3_lattices a)) False) % 28.81/29.00 (Eq % 28.81/29.00 (∀ (B : Iota), % 28.81/29.00 And (Not (v1_xboole_0 B)) (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a))) → % 28.81/29.00 And (v14_lattices a) (r2_hidden (k6_lattices a) B) → % 28.81/29.00 And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a B) (k17_filter_2 a)) % 28.81/29.00 (Eq (k19_filter_2 a B) (u1_struct_0 a))) % 28.81/29.00 True) % 28.81/29.00 Clause #348 (by clausification #[347]): ∀ (a : Iota), % 28.81/29.00 Or % 28.81/29.00 (Eq % 28.81/29.00 (∀ (B : Iota), % 28.81/29.00 And (Not (v1_xboole_0 B)) (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a))) → % 28.81/29.00 And (v14_lattices a) (r2_hidden (k6_lattices a) B) → % 28.81/29.00 And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a B) (k17_filter_2 a)) % 28.81/29.00 (Eq (k19_filter_2 a B) (u1_struct_0 a))) % 28.81/29.00 True) % 28.81/29.00 (Or (Eq (And (Not (v3_struct_0 a)) (v10_lattices a)) False) (Eq (l3_lattices a) False)) % 28.81/29.00 Clause #349 (by clausification #[348]): ∀ (a a_1 : Iota), % 28.81/29.00 Or (Eq (And (Not (v3_struct_0 a)) (v10_lattices a)) False) % 28.81/29.00 (Or (Eq (l3_lattices a) False) % 28.81/29.00 (Eq % 28.81/29.00 (And (Not (v1_xboole_0 a_1)) (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) → % 28.81/29.00 And (v14_lattices a) (r2_hidden (k6_lattices a) a_1) → % 28.81/29.00 And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) (k17_filter_2 a)) % 28.81/29.00 (Eq (k19_filter_2 a a_1) (u1_struct_0 a))) % 28.81/29.00 True)) % 28.81/29.00 Clause #350 (by clausification #[349]): ∀ (a a_1 : Iota), % 28.81/29.00 Or (Eq (l3_lattices a) False) % 28.81/29.00 (Or % 28.81/29.00 (Eq % 28.81/29.00 (And (Not (v1_xboole_0 a_1)) (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) → % 28.81/29.02 And (v14_lattices a) (r2_hidden (k6_lattices a) a_1) → % 28.81/29.02 And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) (k17_filter_2 a)) % 28.81/29.02 (Eq (k19_filter_2 a a_1) (u1_struct_0 a))) % 28.81/29.02 True) % 28.81/29.02 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v10_lattices a) False))) % 28.81/29.02 Clause #351 (by clausification #[350]): ∀ (a a_1 : Iota), % 28.81/29.02 Or (Eq (l3_lattices a) False) % 28.81/29.02 (Or (Eq (Not (v3_struct_0 a)) False) % 28.81/29.02 (Or (Eq (v10_lattices a) False) % 28.81/29.02 (Or (Eq (And (Not (v1_xboole_0 a_1)) (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)))) False) % 28.81/29.02 (Eq % 28.81/29.02 (And (v14_lattices a) (r2_hidden (k6_lattices a) a_1) → % 28.81/29.02 And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) (k17_filter_2 a)) % 28.81/29.02 (Eq (k19_filter_2 a a_1) (u1_struct_0 a))) % 28.81/29.02 True)))) % 28.81/29.02 Clause #352 (by clausification #[351]): ∀ (a a_1 : Iota), % 28.81/29.02 Or (Eq (l3_lattices a) False) % 28.81/29.02 (Or (Eq (v10_lattices a) False) % 28.81/29.02 (Or (Eq (And (Not (v1_xboole_0 a_1)) (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)))) False) % 28.81/29.02 (Or % 28.81/29.02 (Eq % 28.81/29.02 (And (v14_lattices a) (r2_hidden (k6_lattices a) a_1) → % 28.81/29.02 And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) (k17_filter_2 a)) % 28.81/29.02 (Eq (k19_filter_2 a a_1) (u1_struct_0 a))) % 28.81/29.02 True) % 28.81/29.02 (Eq (v3_struct_0 a) True)))) % 28.81/29.02 Clause #353 (by clausification #[352]): ∀ (a a_1 : Iota), % 28.81/29.02 Or (Eq (l3_lattices a) False) % 28.81/29.02 (Or (Eq (v10_lattices a) False) % 28.81/29.02 (Or % 28.81/29.02 (Eq % 28.81/29.02 (And (v14_lattices a) (r2_hidden (k6_lattices a) a_1) → % 28.81/29.02 And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) (k17_filter_2 a)) % 28.81/29.02 (Eq (k19_filter_2 a a_1) (u1_struct_0 a))) % 28.81/29.02 True) % 28.81/29.02 (Or (Eq (v3_struct_0 a) True) % 28.81/29.02 (Or (Eq (Not (v1_xboole_0 a_1)) False) (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False))))) % 28.81/29.02 Clause #354 (by clausification #[353]): ∀ (a a_1 : Iota), % 28.81/29.02 Or (Eq (l3_lattices a) False) % 28.81/29.02 (Or (Eq (v10_lattices a) False) % 28.81/29.02 (Or (Eq (v3_struct_0 a) True) % 28.81/29.02 (Or (Eq (Not (v1_xboole_0 a_1)) False) % 28.81/29.02 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 28.81/29.02 (Or (Eq (And (v14_lattices a) (r2_hidden (k6_lattices a) a_1)) False) % 28.81/29.02 (Eq % 28.81/29.02 (And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) (k17_filter_2 a)) % 28.81/29.02 (Eq (k19_filter_2 a a_1) (u1_struct_0 a))) % 28.81/29.02 True)))))) % 28.81/29.02 Clause #355 (by clausification #[354]): ∀ (a a_1 : Iota), % 28.81/29.02 Or (Eq (l3_lattices a) False) % 28.81/29.02 (Or (Eq (v10_lattices a) False) % 28.81/29.02 (Or (Eq (v3_struct_0 a) True) % 28.81/29.02 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 28.81/29.02 (Or (Eq (And (v14_lattices a) (r2_hidden (k6_lattices a) a_1)) False) % 28.81/29.02 (Or % 28.81/29.02 (Eq % 28.81/29.02 (And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) (k17_filter_2 a)) % 28.81/29.02 (Eq (k19_filter_2 a a_1) (u1_struct_0 a))) % 28.81/29.02 True) % 28.81/29.02 (Eq (v1_xboole_0 a_1) True)))))) % 28.81/29.02 Clause #356 (by clausification #[355]): ∀ (a a_1 : Iota), % 28.86/29.02 Or (Eq (l3_lattices a) False) % 28.86/29.02 (Or (Eq (v10_lattices a) False) % 28.86/29.02 (Or (Eq (v3_struct_0 a) True) % 28.86/29.02 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 28.86/29.02 (Or % 28.86/29.02 (Eq % 28.86/29.02 (And (r1_filter_2 (u1_struct_0 a) (k19_filter_2 a a_1) (k17_filter_2 a)) % 28.86/29.02 (Eq (k19_filter_2 a a_1) (u1_struct_0 a))) % 28.86/29.02 True) % 28.86/29.02 (Or (Eq (v1_xboole_0 a_1) True) % 28.86/29.02 (Or (Eq (v14_lattices a) False) (Eq (r2_hidden (k6_lattices a) a_1) False))))))) % 28.86/29.02 Clause #357 (by clausification #[356]): ∀ (a a_1 : Iota), % 28.86/29.02 Or (Eq (l3_lattices a) False) % 28.86/29.02 (Or (Eq (v10_lattices a) False) % 28.86/29.02 (Or (Eq (v3_struct_0 a) True) % 28.86/29.02 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 28.86/29.02 (Or (Eq (v1_xboole_0 a_1) True) % 28.86/29.02 (Or (Eq (v14_lattices a) False) % 28.86/29.02 (Or (Eq (r2_hidden (k6_lattices a) a_1) False) (Eq (Eq (k19_filter_2 a a_1) (u1_struct_0 a)) True))))))) % 28.86/29.02 Clause #359 (by clausification #[357]): ∀ (a a_1 : Iota), % 28.86/29.04 Or (Eq (l3_lattices a) False) % 28.86/29.04 (Or (Eq (v10_lattices a) False) % 28.86/29.04 (Or (Eq (v3_struct_0 a) True) % 28.86/29.04 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 28.86/29.04 (Or (Eq (v1_xboole_0 a_1) True) % 28.86/29.04 (Or (Eq (v14_lattices a) False) % 28.86/29.04 (Or (Eq (r2_hidden (k6_lattices a) a_1) False) (Eq (k19_filter_2 a a_1) (u1_struct_0 a)))))))) % 28.86/29.04 Clause #360 (by superposition #[359, 58]): ∀ (a a_1 : Iota), % 28.86/29.04 Or (Eq (v10_lattices (skS.0 0 a)) False) % 28.86/29.04 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 28.86/29.04 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.86/29.04 (Or (Eq (v1_xboole_0 a_1) True) % 28.86/29.04 (Or (Eq (v14_lattices (skS.0 0 a)) False) % 28.86/29.04 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a)) a_1) False) % 28.86/29.04 (Or (Eq (k19_filter_2 (skS.0 0 a) a_1) (u1_struct_0 (skS.0 0 a))) (Eq False True))))))) % 28.86/29.04 Clause #389 (by clausification #[57]): ∀ (a a_1 : Iota), % 28.86/29.04 Eq % 28.86/29.04 (Not % 28.86/29.04 (m2_filter_2 (skS.0 15 a a_1) (skS.0 0 a) → % 28.86/29.04 And (v14_lattices (skS.0 0 a)) (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1)) → % 28.86/29.04 And (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1) (k17_filter_2 (skS.0 0 a))) % 28.86/29.04 (Eq (skS.0 15 a a_1) (u1_struct_0 (skS.0 0 a))))) % 28.86/29.04 True % 28.86/29.04 Clause #390 (by clausification #[389]): ∀ (a a_1 : Iota), % 28.86/29.04 Eq % 28.86/29.04 (m2_filter_2 (skS.0 15 a a_1) (skS.0 0 a) → % 28.86/29.04 And (v14_lattices (skS.0 0 a)) (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1)) → % 28.86/29.04 And (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1) (k17_filter_2 (skS.0 0 a))) % 28.86/29.04 (Eq (skS.0 15 a a_1) (u1_struct_0 (skS.0 0 a)))) % 28.86/29.04 False % 28.86/29.04 Clause #391 (by clausification #[390]): ∀ (a a_1 : Iota), Eq (m2_filter_2 (skS.0 15 a a_1) (skS.0 0 a)) True % 28.86/29.04 Clause #392 (by clausification #[390]): ∀ (a a_1 : Iota), % 28.86/29.04 Eq % 28.86/29.04 (And (v14_lattices (skS.0 0 a)) (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1)) → % 28.86/29.04 And (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1) (k17_filter_2 (skS.0 0 a))) % 28.86/29.04 (Eq (skS.0 15 a a_1) (u1_struct_0 (skS.0 0 a)))) % 28.86/29.04 False % 28.86/29.04 Clause #403 (by clausification #[59]): ∀ (a : Iota), Eq (v10_lattices (skS.0 0 a)) True % 28.86/29.04 Clause #404 (by clausification #[59]): ∀ (a : Iota), Eq (Not (v3_struct_0 (skS.0 0 a))) True % 28.86/29.04 Clause #405 (by clausification #[404]): ∀ (a : Iota), Eq (v3_struct_0 (skS.0 0 a)) False % 28.86/29.04 Clause #450 (by clausification #[205]): ∀ (a a_1 : Iota), % 28.86/29.04 Or (Eq (l3_lattices a) False) % 28.86/29.04 (Or (Eq (v10_lattices a) False) % 28.86/29.04 (Or (Eq (m2_filter_2 a_1 a) False) (Or (Eq (v3_struct_0 a) True) (Eq (v1_xboole_0 a_1) False)))) % 28.86/29.04 Clause #451 (by superposition #[450, 58]): ∀ (a a_1 : Iota), % 28.86/29.04 Or (Eq (v10_lattices (skS.0 0 a)) False) % 28.86/29.04 (Or (Eq (m2_filter_2 a_1 (skS.0 0 a)) False) % 28.86/29.04 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Or (Eq (v1_xboole_0 a_1) False) (Eq False True)))) % 28.86/29.04 Clause #471 (by clausification #[250]): ∀ (a : Iota), Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 0 a))) False) (Eq (v3_struct_0 (skS.0 0 a)) True) % 28.86/29.04 Clause #472 (by forward demodulation #[471, 405]): ∀ (a : Iota), Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 0 a))) False) (Eq False True) % 28.86/29.04 Clause #473 (by clausification #[472]): ∀ (a : Iota), Eq (v1_xboole_0 (u1_struct_0 (skS.0 0 a))) False % 28.86/29.04 Clause #534 (by clausification #[328]): ∀ (a a_1 a_2 : Iota), % 28.86/29.04 Or (Eq (m1_subset_1 a (k1_zfmisc_1 a_1)) False) % 28.86/29.04 (Or (Eq (r1_filter_2 a_1 a_2 a) False) % 28.86/29.04 (Or (Eq (Eq a_2 a) True) (Or (Eq (Not (v1_xboole_0 a_1)) False) (Eq (m1_subset_1 a_2 (k1_zfmisc_1 a_1)) False)))) % 28.86/29.04 Clause #535 (by clausification #[534]): ∀ (a a_1 a_2 : Iota), % 28.86/29.04 Or (Eq (m1_subset_1 a (k1_zfmisc_1 a_1)) False) % 28.86/29.04 (Or (Eq (r1_filter_2 a_1 a_2 a) False) % 28.86/29.04 (Or (Eq (Not (v1_xboole_0 a_1)) False) (Or (Eq (m1_subset_1 a_2 (k1_zfmisc_1 a_1)) False) (Eq a_2 a)))) % 28.86/29.04 Clause #536 (by clausification #[535]): ∀ (a a_1 a_2 : Iota), % 28.86/29.04 Or (Eq (m1_subset_1 a (k1_zfmisc_1 a_1)) False) % 28.86/29.04 (Or (Eq (r1_filter_2 a_1 a_2 a) False) % 28.86/29.04 (Or (Eq (m1_subset_1 a_2 (k1_zfmisc_1 a_1)) False) (Or (Eq a_2 a) (Eq (v1_xboole_0 a_1) True)))) % 28.86/29.04 Clause #564 (by clausification #[165]): ∀ (a : Iota), % 28.86/29.04 Or (Eq (k17_filter_2 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a))) % 28.88/29.07 (Or (Eq (v10_lattices (skS.0 0 a)) False) (Eq (v3_struct_0 (skS.0 0 a)) True)) % 28.88/29.07 Clause #565 (by forward demodulation #[564, 403]): ∀ (a : Iota), % 28.88/29.07 Or (Eq (k17_filter_2 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a))) (Or (Eq True False) (Eq (v3_struct_0 (skS.0 0 a)) True)) % 28.88/29.07 Clause #566 (by clausification #[565]): ∀ (a : Iota), Or (Eq (k17_filter_2 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a))) (Eq (v3_struct_0 (skS.0 0 a)) True) % 28.88/29.07 Clause #567 (by forward demodulation #[566, 405]): ∀ (a : Iota), Or (Eq (k17_filter_2 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a))) (Eq False True) % 28.88/29.07 Clause #568 (by clausification #[567]): ∀ (a : Iota), Eq (k17_filter_2 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a)) % 28.88/29.07 Clause #649 (by clausification #[206]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq (v10_lattices (skS.0 0 a)) False) % 28.88/29.07 (Or (Eq (m2_filter_2 a_1 (skS.0 0 a)) False) % 28.88/29.07 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq (m2_lattice4 a_1 (skS.0 0 a)) True))) % 28.88/29.07 Clause #650 (by forward demodulation #[649, 403]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq True False) % 28.88/29.07 (Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) % 28.88/29.07 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) (Eq (m2_lattice4 a (skS.0 0 a_1)) True))) % 28.88/29.07 Clause #651 (by clausification #[650]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) % 28.88/29.07 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) (Eq (m2_lattice4 a (skS.0 0 a_1)) True)) % 28.88/29.07 Clause #652 (by forward demodulation #[651, 405]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) (Or (Eq False True) (Eq (m2_lattice4 a (skS.0 0 a_1)) True)) % 28.88/29.07 Clause #653 (by clausification #[652]): ∀ (a a_1 : Iota), Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) (Eq (m2_lattice4 a (skS.0 0 a_1)) True) % 28.88/29.07 Clause #654 (by superposition #[653, 391]): ∀ (a a_1 : Iota), Or (Eq (m2_lattice4 (skS.0 15 a a_1) (skS.0 0 a)) True) (Eq False True) % 28.88/29.07 Clause #658 (by clausification #[654]): ∀ (a a_1 : Iota), Eq (m2_lattice4 (skS.0 15 a a_1) (skS.0 0 a)) True % 28.88/29.07 Clause #660 (by clausification #[451]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq (v10_lattices (skS.0 0 a)) False) % 28.88/29.07 (Or (Eq (m2_filter_2 a_1 (skS.0 0 a)) False) (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq (v1_xboole_0 a_1) False))) % 28.88/29.07 Clause #661 (by forward demodulation #[660, 403]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq True False) % 28.88/29.07 (Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) (Eq (v1_xboole_0 a) False))) % 28.88/29.07 Clause #662 (by clausification #[661]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) (Eq (v1_xboole_0 a) False)) % 28.88/29.07 Clause #663 (by forward demodulation #[662, 405]): ∀ (a a_1 : Iota), Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) (Or (Eq False True) (Eq (v1_xboole_0 a) False)) % 28.88/29.07 Clause #664 (by clausification #[663]): ∀ (a a_1 : Iota), Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) (Eq (v1_xboole_0 a) False) % 28.88/29.07 Clause #665 (by superposition #[664, 391]): ∀ (a a_1 : Iota), Or (Eq (v1_xboole_0 (skS.0 15 a a_1)) False) (Eq False True) % 28.88/29.07 Clause #667 (by clausification #[665]): ∀ (a a_1 : Iota), Eq (v1_xboole_0 (skS.0 15 a a_1)) False % 28.88/29.07 Clause #692 (by clausification #[218]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq (v10_lattices (skS.0 0 a)) False) % 28.88/29.07 (Or (Eq (m2_lattice4 a_1 (skS.0 0 a)) False) % 28.88/29.07 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) (Eq (v3_struct_0 (skS.0 0 a)) True))) % 28.88/29.07 Clause #693 (by forward demodulation #[692, 403]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq True False) % 28.88/29.07 (Or (Eq (m2_lattice4 a (skS.0 0 a_1)) False) % 28.88/29.07 (Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) True) (Eq (v3_struct_0 (skS.0 0 a_1)) True))) % 28.88/29.07 Clause #694 (by clausification #[693]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq (m2_lattice4 a (skS.0 0 a_1)) False) % 28.88/29.07 (Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) True) (Eq (v3_struct_0 (skS.0 0 a_1)) True)) % 28.88/29.07 Clause #695 (by forward demodulation #[694, 405]): ∀ (a a_1 : Iota), % 28.88/29.07 Or (Eq (m2_lattice4 a (skS.0 0 a_1)) False) % 28.88/29.07 (Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) True) (Eq False True)) % 28.88/29.07 Clause #696 (by clausification #[695]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq (m2_lattice4 a (skS.0 0 a_1)) False) (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) True) % 28.88/29.09 Clause #699 (by superposition #[696, 658]): ∀ (a a_1 : Iota), Or (Eq (m1_subset_1 (skS.0 15 a a_1) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) (Eq False True) % 28.88/29.09 Clause #702 (by clausification #[699]): ∀ (a a_1 : Iota), Eq (m1_subset_1 (skS.0 15 a a_1) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True % 28.88/29.09 Clause #704 (by superposition #[702, 189]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) a_1 a_1) True) % 28.88/29.09 (Or (Eq True False) % 28.88/29.09 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.88/29.09 (Eq (v1_xboole_0 (u1_struct_0 (skS.0 0 a))) True))) % 28.88/29.09 Clause #709 (by superposition #[702, 536]): ∀ (a a_1 a_2 : Iota), % 28.88/29.09 Or (Eq True False) % 28.88/29.09 (Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) a_1 (skS.0 15 a a_2)) False) % 28.88/29.09 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.88/29.09 (Or (Eq a_1 (skS.0 15 a a_2)) (Eq (v1_xboole_0 (u1_struct_0 (skS.0 0 a))) True)))) % 28.88/29.09 Clause #781 (by clausification #[320]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq (v10_lattices (skS.0 0 a)) False) % 28.88/29.09 (Or (Eq (m2_filter_2 a_1 (skS.0 0 a)) False) % 28.88/29.09 (Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (k19_filter_2 (skS.0 0 a) a_1) a_1) True) % 28.88/29.09 (Eq (v3_struct_0 (skS.0 0 a)) True))) % 28.88/29.09 Clause #782 (by forward demodulation #[781, 403]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq True False) % 28.88/29.09 (Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) % 28.88/29.09 (Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a_1)) (k19_filter_2 (skS.0 0 a_1) a) a) True) % 28.88/29.09 (Eq (v3_struct_0 (skS.0 0 a_1)) True))) % 28.88/29.09 Clause #783 (by clausification #[782]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) % 28.88/29.09 (Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a_1)) (k19_filter_2 (skS.0 0 a_1) a) a) True) % 28.88/29.09 (Eq (v3_struct_0 (skS.0 0 a_1)) True)) % 28.88/29.09 Clause #784 (by forward demodulation #[783, 405]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) % 28.88/29.09 (Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a_1)) (k19_filter_2 (skS.0 0 a_1) a) a) True) (Eq False True)) % 28.88/29.09 Clause #785 (by clausification #[784]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq (m2_filter_2 a (skS.0 0 a_1)) False) % 28.88/29.09 (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a_1)) (k19_filter_2 (skS.0 0 a_1) a) a) True) % 28.88/29.09 Clause #786 (by superposition #[785, 391]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (k19_filter_2 (skS.0 0 a) (skS.0 15 a a_1)) (skS.0 15 a a_1)) True) % 28.88/29.09 (Eq False True) % 28.88/29.09 Clause #840 (by clausification #[360]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq (v10_lattices (skS.0 0 a)) False) % 28.88/29.09 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 28.88/29.09 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.88/29.09 (Or (Eq (v1_xboole_0 a_1) True) % 28.88/29.09 (Or (Eq (v14_lattices (skS.0 0 a)) False) % 28.88/29.09 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a)) a_1) False) % 28.88/29.09 (Eq (k19_filter_2 (skS.0 0 a) a_1) (u1_struct_0 (skS.0 0 a)))))))) % 28.88/29.09 Clause #841 (by forward demodulation #[840, 403]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq True False) % 28.88/29.09 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 28.88/29.09 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.88/29.09 (Or (Eq (v1_xboole_0 a_1) True) % 28.88/29.09 (Or (Eq (v14_lattices (skS.0 0 a)) False) % 28.88/29.09 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a)) a_1) False) % 28.88/29.09 (Eq (k19_filter_2 (skS.0 0 a) a_1) (u1_struct_0 (skS.0 0 a)))))))) % 28.88/29.09 Clause #842 (by clausification #[841]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 28.88/29.09 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.88/29.09 (Or (Eq (v1_xboole_0 a_1) True) % 28.88/29.09 (Or (Eq (v14_lattices (skS.0 0 a)) False) % 28.88/29.09 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a)) a_1) False) % 28.88/29.09 (Eq (k19_filter_2 (skS.0 0 a) a_1) (u1_struct_0 (skS.0 0 a))))))) % 28.88/29.09 Clause #843 (by forward demodulation #[842, 405]): ∀ (a a_1 : Iota), % 28.88/29.09 Or (Eq False True) % 28.88/29.09 (Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 28.88/29.09 (Or (Eq (v1_xboole_0 a) True) % 28.88/29.09 (Or (Eq (v14_lattices (skS.0 0 a_1)) False) % 28.88/29.09 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a_1)) a) False) % 28.88/29.11 (Eq (k19_filter_2 (skS.0 0 a_1) a) (u1_struct_0 (skS.0 0 a_1))))))) % 28.88/29.11 Clause #844 (by clausification #[843]): ∀ (a a_1 : Iota), % 28.88/29.11 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 28.88/29.11 (Or (Eq (v1_xboole_0 a) True) % 28.88/29.11 (Or (Eq (v14_lattices (skS.0 0 a_1)) False) % 28.88/29.11 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a_1)) a) False) % 28.88/29.11 (Eq (k19_filter_2 (skS.0 0 a_1) a) (u1_struct_0 (skS.0 0 a_1)))))) % 28.88/29.11 Clause #847 (by superposition #[844, 702]): ∀ (a a_1 : Iota), % 28.88/29.11 Or (Eq (v1_xboole_0 (skS.0 15 a a_1)) True) % 28.88/29.11 (Or (Eq (v14_lattices (skS.0 0 a)) False) % 28.88/29.11 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1)) False) % 28.88/29.11 (Or (Eq (k19_filter_2 (skS.0 0 a) (skS.0 15 a a_1)) (u1_struct_0 (skS.0 0 a))) (Eq False True)))) % 28.88/29.11 Clause #882 (by clausification #[704]): ∀ (a a_1 : Iota), % 28.88/29.11 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) a_1 a_1) True) % 28.88/29.11 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.88/29.11 (Eq (v1_xboole_0 (u1_struct_0 (skS.0 0 a))) True)) % 28.88/29.11 Clause #883 (by forward demodulation #[882, 473]): ∀ (a a_1 : Iota), % 28.88/29.11 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) a_1 a_1) True) % 28.88/29.11 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) (Eq False True)) % 28.88/29.11 Clause #884 (by clausification #[883]): ∀ (a a_1 : Iota), % 28.88/29.11 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) a_1 a_1) True) % 28.88/29.11 (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.88/29.11 Clause #891 (by superposition #[884, 281]): ∀ (a : Iota), % 28.88/29.11 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a))) True) % 28.88/29.11 (Eq False True) % 28.88/29.11 Clause #896 (by clausification #[891]): ∀ (a : Iota), Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a))) True % 28.88/29.11 Clause #907 (by clausification #[392]): ∀ (a a_1 : Iota), Eq (And (v14_lattices (skS.0 0 a)) (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1))) True % 28.88/29.11 Clause #908 (by clausification #[392]): ∀ (a a_1 : Iota), % 28.88/29.11 Eq % 28.88/29.11 (And (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1) (k17_filter_2 (skS.0 0 a))) % 28.88/29.11 (Eq (skS.0 15 a a_1) (u1_struct_0 (skS.0 0 a)))) % 28.88/29.11 False % 28.88/29.11 Clause #909 (by clausification #[907]): ∀ (a a_1 : Iota), Eq (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1)) True % 28.88/29.11 Clause #910 (by clausification #[907]): ∀ (a : Iota), Eq (v14_lattices (skS.0 0 a)) True % 28.88/29.11 Clause #940 (by clausification #[786]): ∀ (a a_1 : Iota), % 28.88/29.11 Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (k19_filter_2 (skS.0 0 a) (skS.0 15 a a_1)) (skS.0 15 a a_1)) True % 28.88/29.11 Clause #1262 (by clausification #[709]): ∀ (a a_1 a_2 : Iota), % 28.88/29.11 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) a_1 (skS.0 15 a a_2)) False) % 28.88/29.11 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.88/29.11 (Or (Eq a_1 (skS.0 15 a a_2)) (Eq (v1_xboole_0 (u1_struct_0 (skS.0 0 a))) True))) % 28.88/29.11 Clause #1263 (by forward demodulation #[1262, 473]): ∀ (a a_1 a_2 : Iota), % 28.88/29.11 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) a_1 (skS.0 15 a a_2)) False) % 28.88/29.11 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.88/29.11 (Or (Eq a_1 (skS.0 15 a a_2)) (Eq False True))) % 28.88/29.11 Clause #1264 (by clausification #[1263]): ∀ (a a_1 a_2 : Iota), % 28.88/29.11 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) a_1 (skS.0 15 a a_2)) False) % 28.88/29.11 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) (Eq a_1 (skS.0 15 a a_2))) % 28.88/29.11 Clause #1741 (by clausification #[908]): ∀ (a a_1 : Iota), % 28.88/29.11 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1) (k17_filter_2 (skS.0 0 a))) False) % 28.88/29.11 (Eq (Eq (skS.0 15 a a_1) (u1_struct_0 (skS.0 0 a))) False) % 28.88/29.11 Clause #1742 (by clausification #[1741]): ∀ (a a_1 : Iota), % 28.88/29.11 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1) (k17_filter_2 (skS.0 0 a))) False) % 28.88/29.11 (Ne (skS.0 15 a a_1) (u1_struct_0 (skS.0 0 a))) % 28.88/29.11 Clause #1743 (by forward demodulation #[1742, 568]): ∀ (a a_1 : Iota), % 28.88/29.11 Or (Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1) (u1_struct_0 (skS.0 0 a))) False) % 28.88/29.11 (Ne (skS.0 15 a a_1) (u1_struct_0 (skS.0 0 a))) % 28.96/29.14 Clause #1879 (by clausification #[847]): ∀ (a a_1 : Iota), % 28.96/29.14 Or (Eq (v1_xboole_0 (skS.0 15 a a_1)) True) % 28.96/29.14 (Or (Eq (v14_lattices (skS.0 0 a)) False) % 28.96/29.14 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1)) False) % 28.96/29.14 (Eq (k19_filter_2 (skS.0 0 a) (skS.0 15 a a_1)) (u1_struct_0 (skS.0 0 a))))) % 28.96/29.14 Clause #1880 (by forward demodulation #[1879, 667]): ∀ (a a_1 : Iota), % 28.96/29.14 Or (Eq False True) % 28.96/29.14 (Or (Eq (v14_lattices (skS.0 0 a)) False) % 28.96/29.14 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1)) False) % 28.96/29.14 (Eq (k19_filter_2 (skS.0 0 a) (skS.0 15 a a_1)) (u1_struct_0 (skS.0 0 a))))) % 28.96/29.14 Clause #1881 (by clausification #[1880]): ∀ (a a_1 : Iota), % 28.96/29.14 Or (Eq (v14_lattices (skS.0 0 a)) False) % 28.96/29.14 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1)) False) % 28.96/29.14 (Eq (k19_filter_2 (skS.0 0 a) (skS.0 15 a a_1)) (u1_struct_0 (skS.0 0 a)))) % 28.96/29.14 Clause #1882 (by forward demodulation #[1881, 910]): ∀ (a a_1 : Iota), % 28.96/29.14 Or (Eq True False) % 28.96/29.14 (Or (Eq (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1)) False) % 28.96/29.14 (Eq (k19_filter_2 (skS.0 0 a) (skS.0 15 a a_1)) (u1_struct_0 (skS.0 0 a)))) % 28.96/29.14 Clause #1883 (by clausification #[1882]): ∀ (a a_1 : Iota), % 28.96/29.14 Or (Eq (r2_hidden (k6_lattices (skS.0 0 a)) (skS.0 15 a a_1)) False) % 28.96/29.14 (Eq (k19_filter_2 (skS.0 0 a) (skS.0 15 a a_1)) (u1_struct_0 (skS.0 0 a))) % 28.96/29.14 Clause #1884 (by superposition #[1883, 909]): ∀ (a a_1 : Iota), Or (Eq (k19_filter_2 (skS.0 0 a) (skS.0 15 a a_1)) (u1_struct_0 (skS.0 0 a))) (Eq False True) % 28.96/29.14 Clause #1885 (by clausification #[1884]): ∀ (a a_1 : Iota), Eq (k19_filter_2 (skS.0 0 a) (skS.0 15 a a_1)) (u1_struct_0 (skS.0 0 a)) % 28.96/29.14 Clause #1886 (by backward demodulation #[1885, 940]): ∀ (a a_1 : Iota), Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1)) True % 28.96/29.14 Clause #1890 (by superposition #[1886, 1264]): ∀ (a a_1 : Iota), % 28.96/29.14 Or (Eq True False) % 28.96/29.14 (Or (Eq (m1_subset_1 (u1_struct_0 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.96/29.14 (Eq (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1))) % 28.96/29.14 Clause #1891 (by clausification #[1890]): ∀ (a a_1 : Iota), % 28.96/29.14 Or (Eq (m1_subset_1 (u1_struct_0 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 28.96/29.14 (Eq (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1)) % 28.96/29.14 Clause #1892 (by superposition #[1891, 281]): ∀ (a a_1 : Iota), Or (Eq (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1)) (Eq False True) % 28.96/29.14 Clause #1898 (by clausification #[1892]): ∀ (a a_1 : Iota), Eq (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1) % 28.96/29.14 Clause #1907 (by backward contextual literal cutting #[1898, 1743]): ∀ (a a_1 : Iota), Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (skS.0 15 a a_1) (u1_struct_0 (skS.0 0 a))) False % 28.96/29.14 Clause #1915 (by forward demodulation #[1907, 1898]): ∀ (a : Iota), Eq (r1_filter_2 (u1_struct_0 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a)) (u1_struct_0 (skS.0 0 a))) False % 28.96/29.14 Clause #1916 (by superposition #[1915, 896]): Eq False True % 28.96/29.14 Clause #1918 (by clausification #[1916]): False % 28.96/29.14 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------