%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GRP641+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n024.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:49:48 PM UTC 2025 % Result : Theorem 37.33s 37.58s % Output : Proof 37.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP641+1 : TPTP v9.2.0. Released v3.4.0. % 0.06/0.13 % Command : duper %s % 0.12/0.34 % Computer : n024.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 17:50:23 EDT 2025 % 0.12/0.34 % CPUTime : % 37.33/37.58 SZS status Theorem for theBenchmark.p % 37.33/37.58 SZS output start Proof for theBenchmark.p % 37.33/37.58 Clause #0 (by assumption #[]): Eq % 37.33/37.58 (Not % 37.33/37.58 (∀ (A : Iota), % 37.33/37.58 And (And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (v4_group_1 A)) (l1_group_1 A) → % 37.33/37.58 ∀ (B : Iota), And (v1_group_1 B) (m1_group_2 B A) → r2_hidden (k2_group_1 A) (k1_funct_1 (k1_latsubgr A) B))) % 37.33/37.58 True % 37.33/37.58 Clause #7 (by assumption #[]): Eq % 37.33/37.58 (∀ (A : Iota), % 37.33/37.58 And (And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (v4_group_1 A)) (l1_group_1 A) → % 37.33/37.58 ∀ (B : Iota), % 37.33/37.58 And (And (v1_funct_1 B) (v1_funct_2 B (k1_group_3 A) (k1_zfmisc_1 (u1_struct_0 A)))) % 37.33/37.58 (m2_relset_1 B (k1_group_3 A) (k1_zfmisc_1 (u1_struct_0 A))) → % 37.33/37.58 Iff (Eq B (k1_latsubgr A)) % 37.33/37.58 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C A) → Eq (k1_funct_1 B C) (u1_struct_0 C))) % 37.33/37.58 True % 37.33/37.58 Clause #10 (by assumption #[]): Eq % 37.33/37.58 (∀ (A : Iota), % 37.33/37.58 And (And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (v4_group_1 A)) (l1_group_1 A) → % 37.33/37.58 And (And (v1_funct_1 (k1_latsubgr A)) (v1_funct_2 (k1_latsubgr A) (k1_group_3 A) (k1_zfmisc_1 (u1_struct_0 A)))) % 37.33/37.58 (m2_relset_1 (k1_latsubgr A) (k1_group_3 A) (k1_zfmisc_1 (u1_struct_0 A)))) % 37.33/37.58 True % 37.33/37.58 Clause #11 (by assumption #[]): Eq (∀ (A : Iota), And (Not (v3_struct_0 A)) (l1_group_1 A) → m1_subset_1 (k2_group_1 A) (u1_struct_0 A)) True % 37.33/37.58 Clause #12 (by assumption #[]): Eq (∀ (A : Iota), l1_group_1 A → l1_struct_0 A) True % 37.33/37.58 Clause #13 (by assumption #[]): Eq % 37.33/37.58 (∀ (A : Iota), % 37.33/37.58 And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (l1_group_1 A) → % 37.33/37.58 ∀ (B : Iota), m1_group_2 B A → And (And (Not (v3_struct_0 B)) (v3_group_1 B)) (l1_group_1 B)) % 37.33/37.58 True % 37.33/37.58 Clause #23 (by assumption #[]): Eq (∀ (A : Iota), And (Not (v3_struct_0 A)) (l1_struct_0 A) → Not (v1_xboole_0 (u1_struct_0 A))) True % 37.33/37.58 Clause #39 (by assumption #[]): Eq (∀ (A B : Iota), m1_subset_1 A B → Or (v1_xboole_0 B) (r2_hidden A B)) True % 37.33/37.58 Clause #42 (by assumption #[]): Eq % 37.33/37.58 (∀ (A : Iota), % 37.33/37.58 And (And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (v4_group_1 A)) (l1_group_1 A) → % 37.33/37.58 ∀ (B : Iota), m1_group_2 B A → Eq (k2_group_1 B) (k2_group_1 A)) % 37.33/37.58 True % 37.33/37.58 Clause #47 (by clausification #[12]): ∀ (a : Iota), Eq (l1_group_1 a → l1_struct_0 a) True % 37.33/37.58 Clause #48 (by clausification #[47]): ∀ (a : Iota), Or (Eq (l1_group_1 a) False) (Eq (l1_struct_0 a) True) % 37.33/37.58 Clause #53 (by clausification #[0]): Eq % 37.33/37.58 (∀ (A : Iota), % 37.33/37.58 And (And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (v4_group_1 A)) (l1_group_1 A) → % 37.33/37.58 ∀ (B : Iota), And (v1_group_1 B) (m1_group_2 B A) → r2_hidden (k2_group_1 A) (k1_funct_1 (k1_latsubgr A) B)) % 37.33/37.58 False % 37.33/37.58 Clause #54 (by clausification #[53]): ∀ (a : Iota), % 37.33/37.58 Eq % 37.33/37.58 (Not % 37.33/37.58 (And (And (And (Not (v3_struct_0 (skS.0 0 a))) (v3_group_1 (skS.0 0 a))) (v4_group_1 (skS.0 0 a))) % 37.33/37.58 (l1_group_1 (skS.0 0 a)) → % 37.33/37.58 ∀ (B : Iota), % 37.33/37.58 And (v1_group_1 B) (m1_group_2 B (skS.0 0 a)) → % 37.33/37.58 r2_hidden (k2_group_1 (skS.0 0 a)) (k1_funct_1 (k1_latsubgr (skS.0 0 a)) B))) % 37.33/37.58 True % 37.33/37.58 Clause #55 (by clausification #[54]): ∀ (a : Iota), % 37.33/37.58 Eq % 37.33/37.58 (And (And (And (Not (v3_struct_0 (skS.0 0 a))) (v3_group_1 (skS.0 0 a))) (v4_group_1 (skS.0 0 a))) % 37.33/37.58 (l1_group_1 (skS.0 0 a)) → % 37.33/37.58 ∀ (B : Iota), % 37.33/37.58 And (v1_group_1 B) (m1_group_2 B (skS.0 0 a)) → % 37.33/37.58 r2_hidden (k2_group_1 (skS.0 0 a)) (k1_funct_1 (k1_latsubgr (skS.0 0 a)) B)) % 37.33/37.58 False % 37.33/37.58 Clause #56 (by clausification #[55]): ∀ (a : Iota), % 37.33/37.58 Eq % 37.33/37.58 (And (And (And (Not (v3_struct_0 (skS.0 0 a))) (v3_group_1 (skS.0 0 a))) (v4_group_1 (skS.0 0 a))) % 37.33/37.58 (l1_group_1 (skS.0 0 a))) % 37.33/37.58 True % 37.33/37.58 Clause #57 (by clausification #[55]): ∀ (a : Iota), % 37.33/37.58 Eq % 37.33/37.58 (∀ (B : Iota), % 37.33/37.58 And (v1_group_1 B) (m1_group_2 B (skS.0 0 a)) → % 37.33/37.58 r2_hidden (k2_group_1 (skS.0 0 a)) (k1_funct_1 (k1_latsubgr (skS.0 0 a)) B)) % 37.33/37.58 False % 37.33/37.58 Clause #58 (by clausification #[56]): ∀ (a : Iota), Eq (l1_group_1 (skS.0 0 a)) True % 37.33/37.58 Clause #59 (by clausification #[56]): ∀ (a : Iota), Eq (And (And (Not (v3_struct_0 (skS.0 0 a))) (v3_group_1 (skS.0 0 a))) (v4_group_1 (skS.0 0 a))) True % 37.33/37.58 Clause #86 (by clausification #[23]): ∀ (a : Iota), Eq (And (Not (v3_struct_0 a)) (l1_struct_0 a) → Not (v1_xboole_0 (u1_struct_0 a))) True % 37.41/37.60 Clause #87 (by clausification #[86]): ∀ (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) % 37.41/37.60 Clause #88 (by clausification #[87]): ∀ (a : Iota), % 37.41/37.60 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)) % 37.41/37.60 Clause #89 (by clausification #[88]): ∀ (a : Iota), % 37.41/37.60 Or (Eq (Not (v3_struct_0 a)) False) (Or (Eq (l1_struct_0 a) False) (Eq (v1_xboole_0 (u1_struct_0 a)) False)) % 37.41/37.60 Clause #90 (by clausification #[89]): ∀ (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)) % 37.41/37.60 Clause #116 (by clausification #[11]): ∀ (a : Iota), Eq (And (Not (v3_struct_0 a)) (l1_group_1 a) → m1_subset_1 (k2_group_1 a) (u1_struct_0 a)) True % 37.41/37.60 Clause #117 (by clausification #[116]): ∀ (a : Iota), % 37.41/37.60 Or (Eq (And (Not (v3_struct_0 a)) (l1_group_1 a)) False) (Eq (m1_subset_1 (k2_group_1 a) (u1_struct_0 a)) True) % 37.41/37.60 Clause #118 (by clausification #[117]): ∀ (a : Iota), % 37.41/37.60 Or (Eq (m1_subset_1 (k2_group_1 a) (u1_struct_0 a)) True) % 37.41/37.60 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (l1_group_1 a) False)) % 37.41/37.60 Clause #119 (by clausification #[118]): ∀ (a : Iota), % 37.41/37.60 Or (Eq (m1_subset_1 (k2_group_1 a) (u1_struct_0 a)) True) (Or (Eq (l1_group_1 a) False) (Eq (v3_struct_0 a) True)) % 37.41/37.60 Clause #151 (by clausification #[39]): ∀ (a : Iota), Eq (∀ (B : Iota), m1_subset_1 a B → Or (v1_xboole_0 B) (r2_hidden a B)) True % 37.41/37.60 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), Eq (m1_subset_1 a a_1 → Or (v1_xboole_0 a_1) (r2_hidden a a_1)) True % 37.41/37.60 Clause #153 (by clausification #[152]): ∀ (a a_1 : Iota), Or (Eq (m1_subset_1 a a_1) False) (Eq (Or (v1_xboole_0 a_1) (r2_hidden a a_1)) True) % 37.41/37.60 Clause #154 (by clausification #[153]): ∀ (a a_1 : Iota), Or (Eq (m1_subset_1 a a_1) False) (Or (Eq (v1_xboole_0 a_1) True) (Eq (r2_hidden a a_1) True)) % 37.41/37.60 Clause #212 (by clausification #[7]): ∀ (a : Iota), % 37.41/37.60 Eq % 37.41/37.60 (And (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) (l1_group_1 a) → % 37.41/37.60 ∀ (B : Iota), % 37.41/37.60 And (And (v1_funct_1 B) (v1_funct_2 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.60 (m2_relset_1 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) → % 37.41/37.60 Iff (Eq B (k1_latsubgr a)) % 37.41/37.60 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 B C) (u1_struct_0 C))) % 37.41/37.60 True % 37.41/37.60 Clause #213 (by clausification #[212]): ∀ (a : Iota), % 37.41/37.60 Or (Eq (And (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) (l1_group_1 a)) False) % 37.41/37.60 (Eq % 37.41/37.60 (∀ (B : Iota), % 37.41/37.60 And (And (v1_funct_1 B) (v1_funct_2 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.60 (m2_relset_1 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) → % 37.41/37.60 Iff (Eq B (k1_latsubgr a)) % 37.41/37.60 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 B C) (u1_struct_0 C))) % 37.41/37.60 True) % 37.41/37.60 Clause #214 (by clausification #[213]): ∀ (a : Iota), % 37.41/37.60 Or % 37.41/37.60 (Eq % 37.41/37.60 (∀ (B : Iota), % 37.41/37.60 And (And (v1_funct_1 B) (v1_funct_2 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.60 (m2_relset_1 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) → % 37.41/37.60 Iff (Eq B (k1_latsubgr a)) % 37.41/37.60 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 B C) (u1_struct_0 C))) % 37.41/37.60 True) % 37.41/37.60 (Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) (Eq (l1_group_1 a) False)) % 37.41/37.60 Clause #215 (by clausification #[214]): ∀ (a a_1 : Iota), % 37.41/37.60 Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) % 37.41/37.60 (Or (Eq (l1_group_1 a) False) % 37.41/37.60 (Eq % 37.41/37.60 (And (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.60 (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) → % 37.41/37.60 Iff (Eq a_1 (k1_latsubgr a)) % 37.41/37.60 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C))) % 37.41/37.60 True)) % 37.41/37.60 Clause #216 (by clausification #[215]): ∀ (a a_1 : Iota), % 37.41/37.62 Or (Eq (l1_group_1 a) False) % 37.41/37.62 (Or % 37.41/37.62 (Eq % 37.41/37.62 (And (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.62 (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) → % 37.41/37.62 Iff (Eq a_1 (k1_latsubgr a)) % 37.41/37.62 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C))) % 37.41/37.62 True) % 37.41/37.62 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) (Eq (v4_group_1 a) False))) % 37.41/37.62 Clause #217 (by clausification #[216]): ∀ (a a_1 : Iota), % 37.41/37.62 Or (Eq (l1_group_1 a) False) % 37.41/37.62 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) % 37.41/37.62 (Or (Eq (v4_group_1 a) False) % 37.41/37.62 (Or % 37.41/37.62 (Eq % 37.41/37.62 (And (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.62 (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.62 False) % 37.41/37.62 (Eq % 37.41/37.62 (Iff (Eq a_1 (k1_latsubgr a)) % 37.41/37.62 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C))) % 37.41/37.62 True)))) % 37.41/37.62 Clause #218 (by clausification #[217]): ∀ (a a_1 : Iota), % 37.41/37.62 Or (Eq (l1_group_1 a) False) % 37.41/37.62 (Or (Eq (v4_group_1 a) False) % 37.41/37.62 (Or % 37.41/37.62 (Eq % 37.41/37.62 (And (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.62 (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.62 False) % 37.41/37.62 (Or % 37.41/37.62 (Eq % 37.41/37.62 (Iff (Eq a_1 (k1_latsubgr a)) % 37.41/37.62 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C))) % 37.41/37.62 True) % 37.41/37.62 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False))))) % 37.41/37.62 Clause #219 (by clausification #[218]): ∀ (a a_1 : Iota), % 37.41/37.62 Or (Eq (l1_group_1 a) False) % 37.41/37.62 (Or (Eq (v4_group_1 a) False) % 37.41/37.62 (Or % 37.41/37.62 (Eq % 37.41/37.62 (Iff (Eq a_1 (k1_latsubgr a)) % 37.41/37.62 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C))) % 37.41/37.62 True) % 37.41/37.62 (Or (Eq (Not (v3_struct_0 a)) False) % 37.41/37.62 (Or (Eq (v3_group_1 a) False) % 37.41/37.62 (Or (Eq (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) False) % 37.41/37.62 (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False)))))) % 37.41/37.62 Clause #221 (by clausification #[219]): ∀ (a a_1 : Iota), % 37.41/37.62 Or (Eq (l1_group_1 a) False) % 37.41/37.62 (Or (Eq (v4_group_1 a) False) % 37.41/37.62 (Or (Eq (Not (v3_struct_0 a)) False) % 37.41/37.62 (Or (Eq (v3_group_1 a) False) % 37.41/37.62 (Or (Eq (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) False) % 37.41/37.62 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.41/37.62 (Or (Eq (Eq a_1 (k1_latsubgr a)) False) % 37.41/37.62 (Eq (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C)) % 37.41/37.62 True))))))) % 37.41/37.62 Clause #234 (by clausification #[42]): ∀ (a : Iota), % 37.41/37.62 Eq % 37.41/37.62 (And (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) (l1_group_1 a) → % 37.41/37.62 ∀ (B : Iota), m1_group_2 B a → Eq (k2_group_1 B) (k2_group_1 a)) % 37.41/37.62 True % 37.41/37.62 Clause #235 (by clausification #[234]): ∀ (a : Iota), % 37.41/37.62 Or (Eq (And (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) (l1_group_1 a)) False) % 37.41/37.62 (Eq (∀ (B : Iota), m1_group_2 B a → Eq (k2_group_1 B) (k2_group_1 a)) True) % 37.41/37.62 Clause #236 (by clausification #[235]): ∀ (a : Iota), % 37.41/37.62 Or (Eq (∀ (B : Iota), m1_group_2 B a → Eq (k2_group_1 B) (k2_group_1 a)) True) % 37.41/37.62 (Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) (Eq (l1_group_1 a) False)) % 37.41/37.62 Clause #237 (by clausification #[236]): ∀ (a a_1 : Iota), % 37.41/37.62 Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) % 37.41/37.62 (Or (Eq (l1_group_1 a) False) (Eq (m1_group_2 a_1 a → Eq (k2_group_1 a_1) (k2_group_1 a)) True)) % 37.41/37.62 Clause #238 (by clausification #[237]): ∀ (a a_1 : Iota), % 37.41/37.62 Or (Eq (l1_group_1 a) False) % 37.41/37.62 (Or (Eq (m1_group_2 a_1 a → Eq (k2_group_1 a_1) (k2_group_1 a)) True) % 37.41/37.65 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) (Eq (v4_group_1 a) False))) % 37.41/37.65 Clause #239 (by clausification #[238]): ∀ (a a_1 : Iota), % 37.41/37.65 Or (Eq (l1_group_1 a) False) % 37.41/37.65 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) % 37.41/37.65 (Or (Eq (v4_group_1 a) False) (Or (Eq (m1_group_2 a_1 a) False) (Eq (Eq (k2_group_1 a_1) (k2_group_1 a)) True)))) % 37.41/37.65 Clause #240 (by clausification #[239]): ∀ (a a_1 : Iota), % 37.41/37.65 Or (Eq (l1_group_1 a) False) % 37.41/37.65 (Or (Eq (v4_group_1 a) False) % 37.41/37.65 (Or (Eq (m1_group_2 a_1 a) False) % 37.41/37.65 (Or (Eq (Eq (k2_group_1 a_1) (k2_group_1 a)) True) % 37.41/37.65 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False))))) % 37.41/37.65 Clause #241 (by clausification #[240]): ∀ (a a_1 : Iota), % 37.41/37.65 Or (Eq (l1_group_1 a) False) % 37.41/37.65 (Or (Eq (v4_group_1 a) False) % 37.41/37.65 (Or (Eq (m1_group_2 a_1 a) False) % 37.41/37.65 (Or (Eq (Not (v3_struct_0 a)) False) (Or (Eq (v3_group_1 a) False) (Eq (k2_group_1 a_1) (k2_group_1 a)))))) % 37.41/37.65 Clause #242 (by clausification #[241]): ∀ (a a_1 : Iota), % 37.41/37.65 Or (Eq (l1_group_1 a) False) % 37.41/37.65 (Or (Eq (v4_group_1 a) False) % 37.41/37.65 (Or (Eq (m1_group_2 a_1 a) False) % 37.41/37.65 (Or (Eq (v3_group_1 a) False) (Or (Eq (k2_group_1 a_1) (k2_group_1 a)) (Eq (v3_struct_0 a) True))))) % 37.41/37.65 Clause #243 (by superposition #[242, 58]): ∀ (a a_1 : Iota), % 37.41/37.65 Or (Eq (v4_group_1 (skS.0 0 a)) False) % 37.41/37.65 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.41/37.65 (Or (Eq (v3_group_1 (skS.0 0 a)) False) % 37.41/37.65 (Or (Eq (k2_group_1 a_1) (k2_group_1 (skS.0 0 a))) (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq False True))))) % 37.41/37.65 Clause #271 (by clausification #[10]): ∀ (a : Iota), % 37.41/37.65 Eq % 37.41/37.65 (And (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) (l1_group_1 a) → % 37.41/37.65 And (And (v1_funct_1 (k1_latsubgr a)) (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.65 (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.65 True % 37.41/37.65 Clause #272 (by clausification #[271]): ∀ (a : Iota), % 37.41/37.65 Or (Eq (And (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) (l1_group_1 a)) False) % 37.41/37.65 (Eq % 37.41/37.65 (And (And (v1_funct_1 (k1_latsubgr a)) (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.65 (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.65 True) % 37.41/37.65 Clause #273 (by clausification #[272]): ∀ (a : Iota), % 37.41/37.65 Or % 37.41/37.65 (Eq % 37.41/37.65 (And (And (v1_funct_1 (k1_latsubgr a)) (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.65 (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.65 True) % 37.41/37.65 (Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) (Eq (l1_group_1 a) False)) % 37.41/37.65 Clause #274 (by clausification #[273]): ∀ (a : Iota), % 37.41/37.65 Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) % 37.41/37.65 (Or (Eq (l1_group_1 a) False) (Eq (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True)) % 37.41/37.65 Clause #275 (by clausification #[273]): ∀ (a : Iota), % 37.41/37.65 Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) % 37.41/37.65 (Or (Eq (l1_group_1 a) False) % 37.41/37.65 (Eq (And (v1_funct_1 (k1_latsubgr a)) (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.41/37.65 True)) % 37.41/37.65 Clause #276 (by clausification #[274]): ∀ (a : Iota), % 37.41/37.65 Or (Eq (l1_group_1 a) False) % 37.41/37.65 (Or (Eq (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True) % 37.41/37.65 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) (Eq (v4_group_1 a) False))) % 37.41/37.65 Clause #277 (by clausification #[276]): ∀ (a : Iota), % 37.41/37.65 Or (Eq (l1_group_1 a) False) % 37.41/37.65 (Or (Eq (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True) % 37.41/37.65 (Or (Eq (v4_group_1 a) False) (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False)))) % 37.41/37.65 Clause #278 (by clausification #[277]): ∀ (a : Iota), % 37.41/37.65 Or (Eq (l1_group_1 a) False) % 37.41/37.65 (Or (Eq (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True) % 37.41/37.65 (Or (Eq (v4_group_1 a) False) (Or (Eq (v3_group_1 a) False) (Eq (v3_struct_0 a) True)))) % 37.41/37.65 Clause #279 (by superposition #[278, 58]): ∀ (a : Iota), % 37.41/37.67 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.41/37.67 (Or (Eq (v4_group_1 (skS.0 0 a)) False) % 37.41/37.67 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq False True)))) % 37.41/37.67 Clause #290 (by clausification #[13]): ∀ (a : Iota), % 37.41/37.67 Eq % 37.41/37.67 (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (l1_group_1 a) → % 37.41/37.67 ∀ (B : Iota), m1_group_2 B a → And (And (Not (v3_struct_0 B)) (v3_group_1 B)) (l1_group_1 B)) % 37.41/37.67 True % 37.41/37.67 Clause #291 (by clausification #[290]): ∀ (a : Iota), % 37.41/37.67 Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (l1_group_1 a)) False) % 37.41/37.67 (Eq (∀ (B : Iota), m1_group_2 B a → And (And (Not (v3_struct_0 B)) (v3_group_1 B)) (l1_group_1 B)) True) % 37.41/37.67 Clause #292 (by clausification #[291]): ∀ (a : Iota), % 37.41/37.67 Or (Eq (∀ (B : Iota), m1_group_2 B a → And (And (Not (v3_struct_0 B)) (v3_group_1 B)) (l1_group_1 B)) True) % 37.41/37.67 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) (Eq (l1_group_1 a) False)) % 37.41/37.67 Clause #293 (by clausification #[292]): ∀ (a a_1 : Iota), % 37.41/37.67 Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) % 37.41/37.67 (Or (Eq (l1_group_1 a) False) % 37.41/37.67 (Eq (m1_group_2 a_1 a → And (And (Not (v3_struct_0 a_1)) (v3_group_1 a_1)) (l1_group_1 a_1)) True)) % 37.41/37.67 Clause #294 (by clausification #[293]): ∀ (a a_1 : Iota), % 37.41/37.67 Or (Eq (l1_group_1 a) False) % 37.41/37.67 (Or (Eq (m1_group_2 a_1 a → And (And (Not (v3_struct_0 a_1)) (v3_group_1 a_1)) (l1_group_1 a_1)) True) % 37.41/37.67 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False))) % 37.41/37.67 Clause #295 (by clausification #[294]): ∀ (a a_1 : Iota), % 37.41/37.67 Or (Eq (l1_group_1 a) False) % 37.41/37.67 (Or (Eq (Not (v3_struct_0 a)) False) % 37.41/37.67 (Or (Eq (v3_group_1 a) False) % 37.41/37.67 (Or (Eq (m1_group_2 a_1 a) False) % 37.41/37.67 (Eq (And (And (Not (v3_struct_0 a_1)) (v3_group_1 a_1)) (l1_group_1 a_1)) True)))) % 37.41/37.67 Clause #296 (by clausification #[295]): ∀ (a a_1 : Iota), % 37.41/37.67 Or (Eq (l1_group_1 a) False) % 37.41/37.67 (Or (Eq (v3_group_1 a) False) % 37.41/37.67 (Or (Eq (m1_group_2 a_1 a) False) % 37.41/37.67 (Or (Eq (And (And (Not (v3_struct_0 a_1)) (v3_group_1 a_1)) (l1_group_1 a_1)) True) (Eq (v3_struct_0 a) True)))) % 37.41/37.67 Clause #297 (by clausification #[296]): ∀ (a a_1 : Iota), % 37.41/37.67 Or (Eq (l1_group_1 a) False) % 37.41/37.67 (Or (Eq (v3_group_1 a) False) % 37.41/37.67 (Or (Eq (m1_group_2 a_1 a) False) (Or (Eq (v3_struct_0 a) True) (Eq (l1_group_1 a_1) True)))) % 37.41/37.67 Clause #298 (by clausification #[296]): ∀ (a a_1 : Iota), % 37.41/37.67 Or (Eq (l1_group_1 a) False) % 37.41/37.67 (Or (Eq (v3_group_1 a) False) % 37.41/37.67 (Or (Eq (m1_group_2 a_1 a) False) % 37.41/37.67 (Or (Eq (v3_struct_0 a) True) (Eq (And (Not (v3_struct_0 a_1)) (v3_group_1 a_1)) True)))) % 37.41/37.67 Clause #299 (by superposition #[297, 58]): ∀ (a a_1 : Iota), % 37.41/37.67 Or (Eq (v3_group_1 (skS.0 0 a)) False) % 37.41/37.67 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.41/37.67 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Or (Eq (l1_group_1 a_1) True) (Eq False True)))) % 37.41/37.67 Clause #405 (by clausification #[57]): ∀ (a a_1 : Iota), % 37.41/37.67 Eq % 37.41/37.67 (Not % 37.41/37.67 (And (v1_group_1 (skS.0 16 a a_1)) (m1_group_2 (skS.0 16 a a_1) (skS.0 0 a)) → % 37.41/37.67 r2_hidden (k2_group_1 (skS.0 0 a)) (k1_funct_1 (k1_latsubgr (skS.0 0 a)) (skS.0 16 a a_1)))) % 37.41/37.67 True % 37.41/37.67 Clause #406 (by clausification #[405]): ∀ (a a_1 : Iota), % 37.41/37.67 Eq % 37.41/37.67 (And (v1_group_1 (skS.0 16 a a_1)) (m1_group_2 (skS.0 16 a a_1) (skS.0 0 a)) → % 37.41/37.67 r2_hidden (k2_group_1 (skS.0 0 a)) (k1_funct_1 (k1_latsubgr (skS.0 0 a)) (skS.0 16 a a_1))) % 37.41/37.67 False % 37.41/37.67 Clause #407 (by clausification #[406]): ∀ (a a_1 : Iota), Eq (And (v1_group_1 (skS.0 16 a a_1)) (m1_group_2 (skS.0 16 a a_1) (skS.0 0 a))) True % 37.41/37.67 Clause #408 (by clausification #[406]): ∀ (a a_1 : Iota), Eq (r2_hidden (k2_group_1 (skS.0 0 a)) (k1_funct_1 (k1_latsubgr (skS.0 0 a)) (skS.0 16 a a_1))) False % 37.41/37.67 Clause #409 (by clausification #[407]): ∀ (a a_1 : Iota), Eq (m1_group_2 (skS.0 16 a a_1) (skS.0 0 a)) True % 37.41/37.67 Clause #410 (by clausification #[407]): ∀ (a a_1 : Iota), Eq (v1_group_1 (skS.0 16 a a_1)) True % 37.41/37.67 Clause #417 (by clausification #[59]): ∀ (a : Iota), Eq (v4_group_1 (skS.0 0 a)) True % 37.41/37.67 Clause #418 (by clausification #[59]): ∀ (a : Iota), Eq (And (Not (v3_struct_0 (skS.0 0 a))) (v3_group_1 (skS.0 0 a))) True % 37.52/37.70 Clause #429 (by clausification #[418]): ∀ (a : Iota), Eq (v3_group_1 (skS.0 0 a)) True % 37.52/37.70 Clause #430 (by clausification #[418]): ∀ (a : Iota), Eq (Not (v3_struct_0 (skS.0 0 a))) True % 37.52/37.70 Clause #431 (by clausification #[430]): ∀ (a : Iota), Eq (v3_struct_0 (skS.0 0 a)) False % 37.52/37.70 Clause #478 (by clausification #[298]): ∀ (a a_1 : Iota), % 37.52/37.70 Or (Eq (l1_group_1 a) False) % 37.52/37.70 (Or (Eq (v3_group_1 a) False) % 37.52/37.70 (Or (Eq (m1_group_2 a_1 a) False) (Or (Eq (v3_struct_0 a) True) (Eq (Not (v3_struct_0 a_1)) True)))) % 37.52/37.70 Clause #481 (by clausification #[478]): ∀ (a a_1 : Iota), % 37.52/37.70 Or (Eq (l1_group_1 a) False) % 37.52/37.70 (Or (Eq (v3_group_1 a) False) % 37.52/37.70 (Or (Eq (m1_group_2 a_1 a) False) (Or (Eq (v3_struct_0 a) True) (Eq (v3_struct_0 a_1) False)))) % 37.52/37.70 Clause #482 (by superposition #[481, 58]): ∀ (a a_1 : Iota), % 37.52/37.70 Or (Eq (v3_group_1 (skS.0 0 a)) False) % 37.52/37.70 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.52/37.70 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Or (Eq (v3_struct_0 a_1) False) (Eq False True)))) % 37.52/37.70 Clause #579 (by clausification #[221]): ∀ (a a_1 : Iota), % 37.52/37.70 Or (Eq (l1_group_1 a) False) % 37.52/37.70 (Or (Eq (v4_group_1 a) False) % 37.52/37.70 (Or (Eq (v3_group_1 a) False) % 37.52/37.70 (Or (Eq (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) False) % 37.52/37.70 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.52/37.70 (Or (Eq (Eq a_1 (k1_latsubgr a)) False) % 37.52/37.70 (Or (Eq (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C)) True) % 37.52/37.70 (Eq (v3_struct_0 a) True))))))) % 37.52/37.70 Clause #580 (by clausification #[579]): ∀ (a a_1 : Iota), % 37.52/37.70 Or (Eq (l1_group_1 a) False) % 37.52/37.70 (Or (Eq (v4_group_1 a) False) % 37.52/37.70 (Or (Eq (v3_group_1 a) False) % 37.52/37.70 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.52/37.70 (Or (Eq (Eq a_1 (k1_latsubgr a)) False) % 37.52/37.70 (Or (Eq (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C)) True) % 37.52/37.70 (Or (Eq (v3_struct_0 a) True) % 37.52/37.70 (Or (Eq (v1_funct_1 a_1) False) % 37.52/37.70 (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False)))))))) % 37.52/37.70 Clause #581 (by clausification #[580]): ∀ (a a_1 : Iota), % 37.52/37.70 Or (Eq (l1_group_1 a) False) % 37.52/37.70 (Or (Eq (v4_group_1 a) False) % 37.52/37.70 (Or (Eq (v3_group_1 a) False) % 37.52/37.70 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.52/37.70 (Or (Eq (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C)) True) % 37.52/37.70 (Or (Eq (v3_struct_0 a) True) % 37.52/37.70 (Or (Eq (v1_funct_1 a_1) False) % 37.52/37.70 (Or (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.52/37.70 (Ne a_1 (k1_latsubgr a))))))))) % 37.52/37.70 Clause #582 (by clausification #[581]): ∀ (a a_1 a_2 : Iota), % 37.52/37.70 Or (Eq (l1_group_1 a) False) % 37.52/37.70 (Or (Eq (v4_group_1 a) False) % 37.52/37.70 (Or (Eq (v3_group_1 a) False) % 37.52/37.70 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.52/37.70 (Or (Eq (v3_struct_0 a) True) % 37.52/37.70 (Or (Eq (v1_funct_1 a_1) False) % 37.52/37.70 (Or (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.52/37.70 (Or (Ne a_1 (k1_latsubgr a)) % 37.52/37.70 (Eq (And (v1_group_1 a_2) (m1_group_2 a_2 a) → Eq (k1_funct_1 a_1 a_2) (u1_struct_0 a_2)) True)))))))) % 37.52/37.70 Clause #583 (by clausification #[582]): ∀ (a a_1 a_2 : Iota), % 37.52/37.70 Or (Eq (l1_group_1 a) False) % 37.52/37.70 (Or (Eq (v4_group_1 a) False) % 37.52/37.70 (Or (Eq (v3_group_1 a) False) % 37.52/37.70 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.52/37.70 (Or (Eq (v3_struct_0 a) True) % 37.52/37.70 (Or (Eq (v1_funct_1 a_1) False) % 37.52/37.70 (Or (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.52/37.70 (Or (Ne a_1 (k1_latsubgr a)) % 37.52/37.70 (Or (Eq (And (v1_group_1 a_2) (m1_group_2 a_2 a)) False) % 37.52/37.70 (Eq (Eq (k1_funct_1 a_1 a_2) (u1_struct_0 a_2)) True))))))))) % 37.52/37.70 Clause #584 (by clausification #[583]): ∀ (a a_1 a_2 : Iota), % 37.55/37.72 Or (Eq (l1_group_1 a) False) % 37.55/37.72 (Or (Eq (v4_group_1 a) False) % 37.55/37.72 (Or (Eq (v3_group_1 a) False) % 37.55/37.72 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.55/37.72 (Or (Eq (v3_struct_0 a) True) % 37.55/37.72 (Or (Eq (v1_funct_1 a_1) False) % 37.55/37.72 (Or (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.55/37.72 (Or (Ne a_1 (k1_latsubgr a)) % 37.55/37.72 (Or (Eq (Eq (k1_funct_1 a_1 a_2) (u1_struct_0 a_2)) True) % 37.55/37.72 (Or (Eq (v1_group_1 a_2) False) (Eq (m1_group_2 a_2 a) False)))))))))) % 37.55/37.72 Clause #585 (by clausification #[584]): ∀ (a a_1 a_2 : Iota), % 37.55/37.72 Or (Eq (l1_group_1 a) False) % 37.55/37.72 (Or (Eq (v4_group_1 a) False) % 37.55/37.72 (Or (Eq (v3_group_1 a) False) % 37.55/37.72 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.55/37.72 (Or (Eq (v3_struct_0 a) True) % 37.55/37.72 (Or (Eq (v1_funct_1 a_1) False) % 37.55/37.72 (Or (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.55/37.72 (Or (Ne a_1 (k1_latsubgr a)) % 37.55/37.72 (Or (Eq (v1_group_1 a_2) False) % 37.55/37.72 (Or (Eq (m1_group_2 a_2 a) False) (Eq (k1_funct_1 a_1 a_2) (u1_struct_0 a_2))))))))))) % 37.55/37.72 Clause #586 (by destructive equality resolution #[585]): ∀ (a a_1 : Iota), % 37.55/37.72 Or (Eq (l1_group_1 a) False) % 37.55/37.72 (Or (Eq (v4_group_1 a) False) % 37.55/37.72 (Or (Eq (v3_group_1 a) False) % 37.55/37.72 (Or (Eq (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.55/37.72 (Or (Eq (v3_struct_0 a) True) % 37.55/37.72 (Or (Eq (v1_funct_1 (k1_latsubgr a)) False) % 37.55/37.72 (Or (Eq (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 37.55/37.72 (Or (Eq (v1_group_1 a_1) False) % 37.55/37.72 (Or (Eq (m1_group_2 a_1 a) False) (Eq (k1_funct_1 (k1_latsubgr a) a_1) (u1_struct_0 a_1)))))))))) % 37.55/37.72 Clause #587 (by superposition #[586, 58]): ∀ (a a_1 : Iota), % 37.55/37.72 Or (Eq (v4_group_1 (skS.0 0 a)) False) % 37.55/37.72 (Or (Eq (v3_group_1 (skS.0 0 a)) False) % 37.55/37.72 (Or % 37.55/37.72 (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.55/37.72 False) % 37.55/37.72 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 37.55/37.72 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) False) % 37.55/37.72 (Or % 37.55/37.72 (Eq % 37.55/37.72 (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.55/37.72 False) % 37.55/37.72 (Or (Eq (v1_group_1 a_1) False) % 37.55/37.72 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.55/37.72 (Or (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1)) (Eq False True))))))))) % 37.55/37.72 Clause #601 (by clausification #[275]): ∀ (a : Iota), % 37.55/37.72 Or (Eq (l1_group_1 a) False) % 37.55/37.72 (Or % 37.55/37.72 (Eq (And (v1_funct_1 (k1_latsubgr a)) (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 37.55/37.72 True) % 37.55/37.72 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) (Eq (v4_group_1 a) False))) % 37.55/37.72 Clause #602 (by clausification #[601]): ∀ (a : Iota), % 37.55/37.72 Or (Eq (l1_group_1 a) False) % 37.55/37.72 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) % 37.55/37.72 (Or (Eq (v4_group_1 a) False) % 37.55/37.72 (Eq (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True))) % 37.55/37.72 Clause #603 (by clausification #[601]): ∀ (a : Iota), % 37.55/37.72 Or (Eq (l1_group_1 a) False) % 37.55/37.72 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) % 37.55/37.72 (Or (Eq (v4_group_1 a) False) (Eq (v1_funct_1 (k1_latsubgr a)) True))) % 37.55/37.72 Clause #604 (by clausification #[602]): ∀ (a : Iota), % 37.55/37.72 Or (Eq (l1_group_1 a) False) % 37.55/37.72 (Or (Eq (v4_group_1 a) False) % 37.55/37.72 (Or (Eq (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True) % 37.55/37.72 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False)))) % 37.55/37.72 Clause #605 (by clausification #[604]): ∀ (a : Iota), % 37.55/37.72 Or (Eq (l1_group_1 a) False) % 37.55/37.72 (Or (Eq (v4_group_1 a) False) % 37.55/37.72 (Or (Eq (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True) % 37.55/37.72 (Or (Eq (v3_group_1 a) False) (Eq (v3_struct_0 a) True)))) % 37.55/37.72 Clause #606 (by superposition #[605, 58]): ∀ (a : Iota), % 37.56/37.75 Or (Eq (v4_group_1 (skS.0 0 a)) False) % 37.56/37.75 (Or % 37.56/37.75 (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.56/37.75 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq False True)))) % 37.56/37.75 Clause #608 (by clausification #[603]): ∀ (a : Iota), % 37.56/37.75 Or (Eq (l1_group_1 a) False) % 37.56/37.75 (Or (Eq (v4_group_1 a) False) % 37.56/37.75 (Or (Eq (v1_funct_1 (k1_latsubgr a)) True) (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False)))) % 37.56/37.75 Clause #609 (by clausification #[608]): ∀ (a : Iota), % 37.56/37.75 Or (Eq (l1_group_1 a) False) % 37.56/37.75 (Or (Eq (v4_group_1 a) False) % 37.56/37.75 (Or (Eq (v1_funct_1 (k1_latsubgr a)) True) (Or (Eq (v3_group_1 a) False) (Eq (v3_struct_0 a) True)))) % 37.56/37.75 Clause #610 (by superposition #[609, 58]): ∀ (a : Iota), % 37.56/37.75 Or (Eq (v4_group_1 (skS.0 0 a)) False) % 37.56/37.75 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) True) % 37.56/37.75 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq False True)))) % 37.56/37.75 Clause #640 (by clausification #[299]): ∀ (a a_1 : Iota), % 37.56/37.75 Or (Eq (v3_group_1 (skS.0 0 a)) False) % 37.56/37.75 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq (l1_group_1 a_1) True))) % 37.56/37.75 Clause #641 (by forward demodulation #[640, 429]): ∀ (a a_1 : Iota), % 37.56/37.75 Or (Eq True False) % 37.56/37.75 (Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) (Eq (l1_group_1 a) True))) % 37.56/37.75 Clause #642 (by clausification #[641]): ∀ (a a_1 : Iota), % 37.56/37.75 Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) (Eq (l1_group_1 a) True)) % 37.56/37.75 Clause #643 (by forward demodulation #[642, 431]): ∀ (a a_1 : Iota), Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Or (Eq False True) (Eq (l1_group_1 a) True)) % 37.56/37.75 Clause #644 (by clausification #[643]): ∀ (a a_1 : Iota), Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Eq (l1_group_1 a) True) % 37.56/37.75 Clause #645 (by superposition #[644, 409]): ∀ (a a_1 : Iota), Or (Eq (l1_group_1 (skS.0 16 a a_1)) True) (Eq False True) % 37.56/37.75 Clause #647 (by clausification #[645]): ∀ (a a_1 : Iota), Eq (l1_group_1 (skS.0 16 a a_1)) True % 37.56/37.75 Clause #648 (by superposition #[647, 48]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (l1_struct_0 (skS.0 16 a a_1)) True) % 37.56/37.75 Clause #651 (by superposition #[647, 119]): ∀ (a a_1 : Iota), % 37.56/37.75 Or (Eq (m1_subset_1 (k2_group_1 (skS.0 16 a a_1)) (u1_struct_0 (skS.0 16 a a_1))) True) % 37.56/37.75 (Or (Eq True False) (Eq (v3_struct_0 (skS.0 16 a a_1)) True)) % 37.56/37.75 Clause #667 (by clausification #[648]): ∀ (a a_1 : Iota), Eq (l1_struct_0 (skS.0 16 a a_1)) True % 37.56/37.75 Clause #668 (by superposition #[667, 90]): ∀ (a a_1 : Iota), % 37.56/37.75 Or (Eq True False) % 37.56/37.75 (Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 16 a a_1))) False) (Eq (v3_struct_0 (skS.0 16 a a_1)) True)) % 37.56/37.75 Clause #698 (by clausification #[668]): ∀ (a a_1 : Iota), Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 16 a a_1))) False) (Eq (v3_struct_0 (skS.0 16 a a_1)) True) % 37.56/37.75 Clause #701 (by clausification #[243]): ∀ (a a_1 : Iota), % 37.56/37.75 Or (Eq (v4_group_1 (skS.0 0 a)) False) % 37.56/37.75 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.56/37.75 (Or (Eq (v3_group_1 (skS.0 0 a)) False) % 37.56/37.75 (Or (Eq (k2_group_1 a_1) (k2_group_1 (skS.0 0 a))) (Eq (v3_struct_0 (skS.0 0 a)) True)))) % 37.56/37.75 Clause #702 (by forward demodulation #[701, 417]): ∀ (a a_1 : Iota), % 37.56/37.75 Or (Eq True False) % 37.56/37.75 (Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) % 37.56/37.75 (Or (Eq (v3_group_1 (skS.0 0 a_1)) False) % 37.56/37.75 (Or (Eq (k2_group_1 a) (k2_group_1 (skS.0 0 a_1))) (Eq (v3_struct_0 (skS.0 0 a_1)) True)))) % 37.56/37.75 Clause #703 (by clausification #[702]): ∀ (a a_1 : Iota), % 37.56/37.75 Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) % 37.56/37.75 (Or (Eq (v3_group_1 (skS.0 0 a_1)) False) % 37.56/37.75 (Or (Eq (k2_group_1 a) (k2_group_1 (skS.0 0 a_1))) (Eq (v3_struct_0 (skS.0 0 a_1)) True))) % 37.56/37.75 Clause #704 (by forward demodulation #[703, 429]): ∀ (a a_1 : Iota), % 37.56/37.75 Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) % 37.56/37.75 (Or (Eq True False) (Or (Eq (k2_group_1 a) (k2_group_1 (skS.0 0 a_1))) (Eq (v3_struct_0 (skS.0 0 a_1)) True))) % 37.56/37.75 Clause #705 (by clausification #[704]): ∀ (a a_1 : Iota), % 37.56/37.75 Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) % 37.56/37.78 (Or (Eq (k2_group_1 a) (k2_group_1 (skS.0 0 a_1))) (Eq (v3_struct_0 (skS.0 0 a_1)) True)) % 37.56/37.78 Clause #706 (by forward demodulation #[705, 431]): ∀ (a a_1 : Iota), % 37.56/37.78 Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Or (Eq (k2_group_1 a) (k2_group_1 (skS.0 0 a_1))) (Eq False True)) % 37.56/37.78 Clause #707 (by clausification #[706]): ∀ (a a_1 : Iota), Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Eq (k2_group_1 a) (k2_group_1 (skS.0 0 a_1))) % 37.56/37.78 Clause #708 (by superposition #[707, 409]): ∀ (a a_1 : Iota), Or (Eq (k2_group_1 (skS.0 16 a a_1)) (k2_group_1 (skS.0 0 a))) (Eq False True) % 37.56/37.78 Clause #710 (by clausification #[708]): ∀ (a a_1 : Iota), Eq (k2_group_1 (skS.0 16 a a_1)) (k2_group_1 (skS.0 0 a)) % 37.56/37.78 Clause #723 (by clausification #[482]): ∀ (a a_1 : Iota), % 37.56/37.78 Or (Eq (v3_group_1 (skS.0 0 a)) False) % 37.56/37.78 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) (Or (Eq (v3_struct_0 (skS.0 0 a)) True) (Eq (v3_struct_0 a_1) False))) % 37.56/37.78 Clause #724 (by forward demodulation #[723, 429]): ∀ (a a_1 : Iota), % 37.56/37.78 Or (Eq True False) % 37.56/37.78 (Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) (Eq (v3_struct_0 a) False))) % 37.56/37.78 Clause #725 (by clausification #[724]): ∀ (a a_1 : Iota), % 37.56/37.78 Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) (Eq (v3_struct_0 a) False)) % 37.56/37.78 Clause #726 (by forward demodulation #[725, 431]): ∀ (a a_1 : Iota), Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Or (Eq False True) (Eq (v3_struct_0 a) False)) % 37.56/37.78 Clause #727 (by clausification #[726]): ∀ (a a_1 : Iota), Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Eq (v3_struct_0 a) False) % 37.56/37.78 Clause #728 (by superposition #[727, 409]): ∀ (a a_1 : Iota), Or (Eq (v3_struct_0 (skS.0 16 a a_1)) False) (Eq False True) % 37.56/37.78 Clause #730 (by clausification #[728]): ∀ (a a_1 : Iota), Eq (v3_struct_0 (skS.0 16 a a_1)) False % 37.56/37.78 Clause #731 (by backward demodulation #[730, 698]): ∀ (a a_1 : Iota), Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 16 a a_1))) False) (Eq False True) % 37.56/37.78 Clause #733 (by clausification #[731]): ∀ (a a_1 : Iota), Eq (v1_xboole_0 (u1_struct_0 (skS.0 16 a a_1))) False % 37.56/37.78 Clause #745 (by clausification #[651]): ∀ (a a_1 : Iota), % 37.56/37.78 Or (Eq (m1_subset_1 (k2_group_1 (skS.0 16 a a_1)) (u1_struct_0 (skS.0 16 a a_1))) True) % 37.56/37.78 (Eq (v3_struct_0 (skS.0 16 a a_1)) True) % 37.56/37.78 Clause #746 (by forward demodulation #[745, 710]): ∀ (a a_1 : Iota), % 37.56/37.78 Or (Eq (m1_subset_1 (k2_group_1 (skS.0 0 a)) (u1_struct_0 (skS.0 16 a a_1))) True) % 37.56/37.78 (Eq (v3_struct_0 (skS.0 16 a a_1)) True) % 37.56/37.78 Clause #747 (by forward demodulation #[746, 730]): ∀ (a a_1 : Iota), Or (Eq (m1_subset_1 (k2_group_1 (skS.0 0 a)) (u1_struct_0 (skS.0 16 a a_1))) True) (Eq False True) % 37.56/37.78 Clause #748 (by clausification #[747]): ∀ (a a_1 : Iota), Eq (m1_subset_1 (k2_group_1 (skS.0 0 a)) (u1_struct_0 (skS.0 16 a a_1))) True % 37.56/37.78 Clause #749 (by superposition #[748, 154]): ∀ (a a_1 : Iota), % 37.56/37.78 Or (Eq True False) % 37.56/37.78 (Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 16 a a_1))) True) % 37.56/37.78 (Eq (r2_hidden (k2_group_1 (skS.0 0 a)) (u1_struct_0 (skS.0 16 a a_1))) True)) % 37.56/37.78 Clause #750 (by clausification #[749]): ∀ (a a_1 : Iota), % 37.56/37.78 Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 16 a a_1))) True) % 37.56/37.78 (Eq (r2_hidden (k2_group_1 (skS.0 0 a)) (u1_struct_0 (skS.0 16 a a_1))) True) % 37.56/37.78 Clause #751 (by forward demodulation #[750, 733]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (r2_hidden (k2_group_1 (skS.0 0 a)) (u1_struct_0 (skS.0 16 a a_1))) True) % 37.56/37.78 Clause #752 (by clausification #[751]): ∀ (a a_1 : Iota), Eq (r2_hidden (k2_group_1 (skS.0 0 a)) (u1_struct_0 (skS.0 16 a a_1))) True % 37.56/37.78 Clause #758 (by clausification #[279]): ∀ (a : Iota), % 37.56/37.78 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.56/37.78 (Or (Eq (v4_group_1 (skS.0 0 a)) False) % 37.56/37.78 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Eq (v3_struct_0 (skS.0 0 a)) True))) % 37.56/37.78 Clause #759 (by forward demodulation #[758, 417]): ∀ (a : Iota), % 37.56/37.78 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.56/37.78 (Or (Eq True False) (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Eq (v3_struct_0 (skS.0 0 a)) True))) % 37.56/37.81 Clause #760 (by clausification #[759]): ∀ (a : Iota), % 37.56/37.81 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.56/37.81 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Eq (v3_struct_0 (skS.0 0 a)) True)) % 37.56/37.81 Clause #761 (by forward demodulation #[760, 429]): ∀ (a : Iota), % 37.56/37.81 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.56/37.81 (Or (Eq True False) (Eq (v3_struct_0 (skS.0 0 a)) True)) % 37.56/37.81 Clause #762 (by clausification #[761]): ∀ (a : Iota), % 37.56/37.81 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.56/37.81 (Eq (v3_struct_0 (skS.0 0 a)) True) % 37.56/37.81 Clause #763 (by forward demodulation #[762, 431]): ∀ (a : Iota), % 37.56/37.81 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.56/37.81 (Eq False True) % 37.56/37.81 Clause #764 (by clausification #[763]): ∀ (a : Iota), % 37.56/37.81 Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True % 37.56/37.81 Clause #980 (by clausification #[610]): ∀ (a : Iota), % 37.56/37.81 Or (Eq (v4_group_1 (skS.0 0 a)) False) % 37.56/37.81 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) True) % 37.56/37.81 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Eq (v3_struct_0 (skS.0 0 a)) True))) % 37.56/37.81 Clause #981 (by forward demodulation #[980, 417]): ∀ (a : Iota), % 37.56/37.81 Or (Eq True False) % 37.56/37.81 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) True) % 37.56/37.81 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Eq (v3_struct_0 (skS.0 0 a)) True))) % 37.56/37.81 Clause #982 (by clausification #[981]): ∀ (a : Iota), % 37.56/37.81 Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) True) % 37.56/37.81 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Eq (v3_struct_0 (skS.0 0 a)) True)) % 37.56/37.81 Clause #983 (by forward demodulation #[982, 429]): ∀ (a : Iota), % 37.56/37.81 Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) True) (Or (Eq True False) (Eq (v3_struct_0 (skS.0 0 a)) True)) % 37.56/37.81 Clause #984 (by clausification #[983]): ∀ (a : Iota), Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) True) (Eq (v3_struct_0 (skS.0 0 a)) True) % 37.56/37.81 Clause #985 (by forward demodulation #[984, 431]): ∀ (a : Iota), Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) True) (Eq False True) % 37.56/37.81 Clause #986 (by clausification #[985]): ∀ (a : Iota), Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) True % 37.56/37.81 Clause #1066 (by clausification #[587]): ∀ (a a_1 : Iota), % 37.56/37.81 Or (Eq (v4_group_1 (skS.0 0 a)) False) % 37.56/37.81 (Or (Eq (v3_group_1 (skS.0 0 a)) False) % 37.56/37.81 (Or % 37.56/37.81 (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.56/37.81 False) % 37.56/37.81 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 37.56/37.81 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) False) % 37.56/37.81 (Or % 37.56/37.81 (Eq % 37.56/37.81 (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.56/37.81 False) % 37.56/37.81 (Or (Eq (v1_group_1 a_1) False) % 37.56/37.81 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.56/37.81 (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1))))))))) % 37.56/37.81 Clause #1067 (by forward demodulation #[1066, 417]): ∀ (a a_1 : Iota), % 37.56/37.81 Or (Eq True False) % 37.56/37.81 (Or (Eq (v3_group_1 (skS.0 0 a)) False) % 37.56/37.81 (Or % 37.56/37.81 (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.56/37.81 False) % 37.56/37.81 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 37.56/37.81 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) False) % 37.56/37.81 (Or % 37.56/37.81 (Eq % 37.56/37.81 (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.56/37.81 False) % 37.56/37.81 (Or (Eq (v1_group_1 a_1) False) % 37.56/37.81 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.56/37.81 (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1))))))))) % 37.56/37.81 Clause #1068 (by clausification #[1067]): ∀ (a a_1 : Iota), % 37.56/37.81 Or (Eq (v3_group_1 (skS.0 0 a)) False) % 37.56/37.81 (Or % 37.56/37.81 (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.64/37.83 False) % 37.64/37.83 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 37.64/37.83 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) False) % 37.64/37.83 (Or % 37.64/37.83 (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.64/37.83 False) % 37.64/37.83 (Or (Eq (v1_group_1 a_1) False) % 37.64/37.83 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.64/37.83 (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1)))))))) % 37.64/37.83 Clause #1069 (by forward demodulation #[1068, 429]): ∀ (a a_1 : Iota), % 37.64/37.83 Or (Eq True False) % 37.64/37.83 (Or % 37.64/37.83 (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.64/37.83 False) % 37.64/37.83 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 37.64/37.83 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) False) % 37.64/37.83 (Or % 37.64/37.83 (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.64/37.83 False) % 37.64/37.83 (Or (Eq (v1_group_1 a_1) False) % 37.64/37.83 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.64/37.83 (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1)))))))) % 37.64/37.83 Clause #1070 (by clausification #[1069]): ∀ (a a_1 : Iota), % 37.64/37.83 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 37.64/37.83 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 37.64/37.83 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) False) % 37.64/37.83 (Or % 37.64/37.83 (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.64/37.83 False) % 37.64/37.83 (Or (Eq (v1_group_1 a_1) False) % 37.64/37.83 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.64/37.83 (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1))))))) % 37.64/37.83 Clause #1071 (by forward demodulation #[1070, 431]): ∀ (a a_1 : Iota), % 37.64/37.83 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 37.64/37.83 (Or (Eq False True) % 37.64/37.83 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) False) % 37.64/37.83 (Or % 37.64/37.83 (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.64/37.83 False) % 37.64/37.83 (Or (Eq (v1_group_1 a_1) False) % 37.64/37.83 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.64/37.83 (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1))))))) % 37.64/37.83 Clause #1072 (by clausification #[1071]): ∀ (a a_1 : Iota), % 37.64/37.83 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 37.64/37.83 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 0 a))) False) % 37.64/37.83 (Or % 37.64/37.83 (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.64/37.83 False) % 37.64/37.83 (Or (Eq (v1_group_1 a_1) False) % 37.64/37.83 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.64/37.83 (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1)))))) % 37.64/37.83 Clause #1073 (by forward demodulation #[1072, 986]): ∀ (a a_1 : Iota), % 37.64/37.83 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 37.64/37.83 (Or (Eq True False) % 37.64/37.83 (Or % 37.64/37.83 (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) % 37.64/37.83 False) % 37.64/37.83 (Or (Eq (v1_group_1 a_1) False) % 37.64/37.83 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.64/37.83 (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1)))))) % 37.64/37.83 Clause #1074 (by clausification #[1073]): ∀ (a a_1 : Iota), % 37.64/37.83 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 37.64/37.83 (Or % 37.64/37.83 (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 37.64/37.83 (Or (Eq (v1_group_1 a_1) False) % 37.64/37.83 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1))))) % 37.64/37.83 Clause #1075 (by superposition #[1074, 764]): ∀ (a a_1 : Iota), % 37.64/37.83 Or (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 37.64/37.86 (Or (Eq (v1_group_1 a_1) False) % 37.64/37.86 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) % 37.64/37.86 (Or (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1)) (Eq False True)))) % 37.64/37.86 Clause #1183 (by clausification #[606]): ∀ (a : Iota), % 37.64/37.86 Or (Eq (v4_group_1 (skS.0 0 a)) False) % 37.64/37.86 (Or % 37.64/37.86 (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.64/37.86 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Eq (v3_struct_0 (skS.0 0 a)) True))) % 37.64/37.86 Clause #1184 (by forward demodulation #[1183, 417]): ∀ (a : Iota), % 37.64/37.86 Or (Eq True False) % 37.64/37.86 (Or % 37.64/37.86 (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.64/37.86 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Eq (v3_struct_0 (skS.0 0 a)) True))) % 37.64/37.86 Clause #1185 (by clausification #[1184]): ∀ (a : Iota), % 37.64/37.86 Or (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.64/37.86 (Or (Eq (v3_group_1 (skS.0 0 a)) False) (Eq (v3_struct_0 (skS.0 0 a)) True)) % 37.64/37.86 Clause #1186 (by forward demodulation #[1185, 429]): ∀ (a : Iota), % 37.64/37.86 Or (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.64/37.86 (Or (Eq True False) (Eq (v3_struct_0 (skS.0 0 a)) True)) % 37.64/37.86 Clause #1187 (by clausification #[1186]): ∀ (a : Iota), % 37.64/37.86 Or (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.64/37.86 (Eq (v3_struct_0 (skS.0 0 a)) True) % 37.64/37.86 Clause #1188 (by forward demodulation #[1187, 431]): ∀ (a : Iota), % 37.64/37.86 Or (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 37.64/37.86 (Eq False True) % 37.64/37.86 Clause #1189 (by clausification #[1188]): ∀ (a : Iota), % 37.64/37.86 Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True % 37.64/37.86 Clause #2022 (by clausification #[1075]): ∀ (a a_1 : Iota), % 37.64/37.86 Or (Eq (v1_funct_2 (k1_latsubgr (skS.0 0 a)) (k1_group_3 (skS.0 0 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 37.64/37.86 (Or (Eq (v1_group_1 a_1) False) % 37.64/37.86 (Or (Eq (m1_group_2 a_1 (skS.0 0 a)) False) (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) a_1) (u1_struct_0 a_1)))) % 37.64/37.86 Clause #2023 (by superposition #[2022, 1189]): ∀ (a a_1 : Iota), % 37.64/37.86 Or (Eq (v1_group_1 a) False) % 37.64/37.86 (Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) % 37.64/37.86 (Or (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a_1)) a) (u1_struct_0 a)) (Eq False True))) % 37.64/37.86 Clause #2028 (by clausification #[2023]): ∀ (a a_1 : Iota), % 37.64/37.86 Or (Eq (v1_group_1 a) False) % 37.64/37.86 (Or (Eq (m1_group_2 a (skS.0 0 a_1)) False) (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a_1)) a) (u1_struct_0 a))) % 37.64/37.86 Clause #2029 (by superposition #[2028, 410]): ∀ (a a_1 a_2 : Iota), % 37.64/37.86 Or (Eq (m1_group_2 (skS.0 16 a a_1) (skS.0 0 a_2)) False) % 37.64/37.86 (Or (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a_2)) (skS.0 16 a a_1)) (u1_struct_0 (skS.0 16 a a_1))) (Eq False True)) % 37.64/37.86 Clause #2031 (by clausification #[2029]): ∀ (a a_1 a_2 : Iota), % 37.64/37.86 Or (Eq (m1_group_2 (skS.0 16 a a_1) (skS.0 0 a_2)) False) % 37.64/37.86 (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a_2)) (skS.0 16 a a_1)) (u1_struct_0 (skS.0 16 a a_1))) % 37.64/37.86 Clause #2032 (by superposition #[2031, 409]): ∀ (a a_1 : Iota), % 37.64/37.86 Or (Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) (skS.0 16 a a_1)) (u1_struct_0 (skS.0 16 a a_1))) (Eq False True) % 37.64/37.86 Clause #2033 (by clausification #[2032]): ∀ (a a_1 : Iota), Eq (k1_funct_1 (k1_latsubgr (skS.0 0 a)) (skS.0 16 a a_1)) (u1_struct_0 (skS.0 16 a a_1)) % 37.64/37.86 Clause #2034 (by backward demodulation #[2033, 408]): ∀ (a a_1 : Iota), Eq (r2_hidden (k2_group_1 (skS.0 0 a)) (u1_struct_0 (skS.0 16 a a_1))) False % 37.64/37.86 Clause #2035 (by superposition #[2034, 752]): Eq False True % 37.64/37.86 Clause #2036 (by clausification #[2035]): False % 37.64/37.86 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------