%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GRP642+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 32.85s 33.09s % Output : Proof 33.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : GRP642+1 : TPTP v9.2.0. Released v3.4.0. % 0.10/0.13 % Command : duper %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 17:10:08 EDT 2025 % 0.13/0.34 % CPUTime : % 32.85/33.09 SZS status Theorem for theBenchmark.p % 32.85/33.09 SZS output start Proof for theBenchmark.p % 32.85/33.09 Clause #0 (by assumption #[]): Eq % 32.85/33.09 (Not % 32.85/33.09 (∀ (A : Iota), % 32.85/33.09 And (And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (v4_group_1 A)) (l1_group_1 A) → % 32.85/33.09 ∀ (B : Iota), And (v1_group_1 B) (m1_group_2 B A) → Ne (k1_funct_1 (k1_latsubgr A) B) k1_xboole_0)) % 32.85/33.09 True % 32.85/33.09 Clause #7 (by assumption #[]): Eq % 32.85/33.09 (∀ (A : Iota), % 32.85/33.09 And (And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (v4_group_1 A)) (l1_group_1 A) → % 32.85/33.09 ∀ (B : Iota), % 32.85/33.09 And (And (v1_funct_1 B) (v1_funct_2 B (k1_group_3 A) (k1_zfmisc_1 (u1_struct_0 A)))) % 32.85/33.09 (m2_relset_1 B (k1_group_3 A) (k1_zfmisc_1 (u1_struct_0 A))) → % 32.85/33.09 Iff (Eq B (k1_latsubgr A)) % 32.85/33.09 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C A) → Eq (k1_funct_1 B C) (u1_struct_0 C))) % 32.85/33.09 True % 32.85/33.09 Clause #10 (by assumption #[]): Eq % 32.85/33.09 (∀ (A : Iota), % 32.85/33.09 And (And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (v4_group_1 A)) (l1_group_1 A) → % 32.85/33.09 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)))) % 32.85/33.09 (m2_relset_1 (k1_latsubgr A) (k1_group_3 A) (k1_zfmisc_1 (u1_struct_0 A)))) % 32.85/33.09 True % 32.85/33.09 Clause #11 (by assumption #[]): Eq (∀ (A : Iota), l1_group_1 A → l1_struct_0 A) True % 32.85/33.09 Clause #12 (by assumption #[]): Eq % 32.85/33.09 (∀ (A : Iota), % 32.85/33.09 And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (l1_group_1 A) → % 32.85/33.09 ∀ (B : Iota), m1_group_2 B A → And (And (Not (v3_struct_0 B)) (v3_group_1 B)) (l1_group_1 B)) % 32.85/33.09 True % 32.85/33.09 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 % 32.85/33.09 Clause #24 (by assumption #[]): Eq (v1_xboole_0 k1_xboole_0) True % 32.85/33.09 Clause #45 (by clausification #[11]): ∀ (a : Iota), Eq (l1_group_1 a → l1_struct_0 a) True % 32.85/33.09 Clause #46 (by clausification #[45]): ∀ (a : Iota), Or (Eq (l1_group_1 a) False) (Eq (l1_struct_0 a) True) % 32.85/33.09 Clause #51 (by clausification #[0]): Eq % 32.85/33.09 (∀ (A : Iota), % 32.85/33.09 And (And (And (Not (v3_struct_0 A)) (v3_group_1 A)) (v4_group_1 A)) (l1_group_1 A) → % 32.85/33.09 ∀ (B : Iota), And (v1_group_1 B) (m1_group_2 B A) → Ne (k1_funct_1 (k1_latsubgr A) B) k1_xboole_0) % 32.85/33.09 False % 32.85/33.09 Clause #52 (by clausification #[51]): ∀ (a : Iota), % 32.85/33.09 Eq % 32.85/33.09 (Not % 32.85/33.09 (And (And (And (Not (v3_struct_0 (skS.0 1 a))) (v3_group_1 (skS.0 1 a))) (v4_group_1 (skS.0 1 a))) % 32.85/33.09 (l1_group_1 (skS.0 1 a)) → % 32.85/33.09 ∀ (B : Iota), % 32.85/33.09 And (v1_group_1 B) (m1_group_2 B (skS.0 1 a)) → Ne (k1_funct_1 (k1_latsubgr (skS.0 1 a)) B) k1_xboole_0)) % 32.85/33.09 True % 32.85/33.09 Clause #53 (by clausification #[52]): ∀ (a : Iota), % 32.85/33.09 Eq % 32.85/33.09 (And (And (And (Not (v3_struct_0 (skS.0 1 a))) (v3_group_1 (skS.0 1 a))) (v4_group_1 (skS.0 1 a))) % 32.85/33.09 (l1_group_1 (skS.0 1 a)) → % 32.85/33.09 ∀ (B : Iota), % 32.85/33.09 And (v1_group_1 B) (m1_group_2 B (skS.0 1 a)) → Ne (k1_funct_1 (k1_latsubgr (skS.0 1 a)) B) k1_xboole_0) % 32.85/33.09 False % 32.85/33.09 Clause #54 (by clausification #[53]): ∀ (a : Iota), % 32.85/33.09 Eq % 32.85/33.09 (And (And (And (Not (v3_struct_0 (skS.0 1 a))) (v3_group_1 (skS.0 1 a))) (v4_group_1 (skS.0 1 a))) % 32.85/33.09 (l1_group_1 (skS.0 1 a))) % 32.85/33.09 True % 32.85/33.09 Clause #55 (by clausification #[53]): ∀ (a : Iota), % 32.85/33.09 Eq % 32.85/33.09 (∀ (B : Iota), % 32.85/33.09 And (v1_group_1 B) (m1_group_2 B (skS.0 1 a)) → Ne (k1_funct_1 (k1_latsubgr (skS.0 1 a)) B) k1_xboole_0) % 32.85/33.09 False % 32.85/33.09 Clause #56 (by clausification #[54]): ∀ (a : Iota), Eq (l1_group_1 (skS.0 1 a)) True % 32.85/33.09 Clause #57 (by clausification #[54]): ∀ (a : Iota), Eq (And (And (Not (v3_struct_0 (skS.0 1 a))) (v3_group_1 (skS.0 1 a))) (v4_group_1 (skS.0 1 a))) True % 32.85/33.09 Clause #93 (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 % 32.85/33.09 Clause #94 (by clausification #[93]): ∀ (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) % 32.85/33.09 Clause #95 (by clausification #[94]): ∀ (a : Iota), % 32.85/33.09 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)) % 32.85/33.09 Clause #96 (by clausification #[95]): ∀ (a : Iota), % 32.85/33.09 Or (Eq (Not (v3_struct_0 a)) False) (Or (Eq (l1_struct_0 a) False) (Eq (v1_xboole_0 (u1_struct_0 a)) False)) % 32.94/33.12 Clause #97 (by clausification #[96]): ∀ (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)) % 32.94/33.12 Clause #204 (by clausification #[7]): ∀ (a : Iota), % 32.94/33.12 Eq % 32.94/33.12 (And (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) (l1_group_1 a) → % 32.94/33.12 ∀ (B : Iota), % 32.94/33.12 And (And (v1_funct_1 B) (v1_funct_2 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.12 (m2_relset_1 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) → % 32.94/33.12 Iff (Eq B (k1_latsubgr a)) % 32.94/33.12 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 B C) (u1_struct_0 C))) % 32.94/33.12 True % 32.94/33.12 Clause #205 (by clausification #[204]): ∀ (a : Iota), % 32.94/33.12 Or (Eq (And (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) (l1_group_1 a)) False) % 32.94/33.12 (Eq % 32.94/33.12 (∀ (B : Iota), % 32.94/33.12 And (And (v1_funct_1 B) (v1_funct_2 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.12 (m2_relset_1 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) → % 32.94/33.12 Iff (Eq B (k1_latsubgr a)) % 32.94/33.12 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 B C) (u1_struct_0 C))) % 32.94/33.12 True) % 32.94/33.12 Clause #206 (by clausification #[205]): ∀ (a : Iota), % 32.94/33.12 Or % 32.94/33.12 (Eq % 32.94/33.12 (∀ (B : Iota), % 32.94/33.12 And (And (v1_funct_1 B) (v1_funct_2 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.12 (m2_relset_1 B (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) → % 32.94/33.12 Iff (Eq B (k1_latsubgr a)) % 32.94/33.12 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 B C) (u1_struct_0 C))) % 32.94/33.12 True) % 32.94/33.12 (Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) (Eq (l1_group_1 a) False)) % 32.94/33.12 Clause #207 (by clausification #[206]): ∀ (a a_1 : Iota), % 32.94/33.12 Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) % 32.94/33.12 (Or (Eq (l1_group_1 a) False) % 32.94/33.12 (Eq % 32.94/33.12 (And (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.12 (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) → % 32.94/33.12 Iff (Eq a_1 (k1_latsubgr a)) % 32.94/33.12 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C))) % 32.94/33.12 True)) % 32.94/33.12 Clause #208 (by clausification #[207]): ∀ (a a_1 : Iota), % 32.94/33.12 Or (Eq (l1_group_1 a) False) % 32.94/33.12 (Or % 32.94/33.12 (Eq % 32.94/33.12 (And (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.12 (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) → % 32.94/33.12 Iff (Eq a_1 (k1_latsubgr a)) % 32.94/33.12 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C))) % 32.94/33.12 True) % 32.94/33.12 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) (Eq (v4_group_1 a) False))) % 32.94/33.12 Clause #209 (by clausification #[208]): ∀ (a a_1 : Iota), % 32.94/33.12 Or (Eq (l1_group_1 a) False) % 32.94/33.12 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) % 32.94/33.12 (Or (Eq (v4_group_1 a) False) % 32.94/33.12 (Or % 32.94/33.12 (Eq % 32.94/33.12 (And (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.12 (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.12 False) % 32.94/33.12 (Eq % 32.94/33.12 (Iff (Eq a_1 (k1_latsubgr a)) % 32.94/33.12 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C))) % 32.94/33.12 True)))) % 32.94/33.12 Clause #210 (by clausification #[209]): ∀ (a a_1 : Iota), % 32.94/33.12 Or (Eq (l1_group_1 a) False) % 32.94/33.12 (Or (Eq (v4_group_1 a) False) % 32.94/33.12 (Or % 32.94/33.12 (Eq % 32.94/33.12 (And (And (v1_funct_1 a_1) (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.12 (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.12 False) % 32.94/33.12 (Or % 32.94/33.12 (Eq % 32.94/33.12 (Iff (Eq a_1 (k1_latsubgr a)) % 32.94/33.12 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C))) % 32.94/33.12 True) % 32.94/33.12 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False))))) % 32.94/33.12 Clause #211 (by clausification #[210]): ∀ (a a_1 : Iota), % 32.94/33.15 Or (Eq (l1_group_1 a) False) % 32.94/33.15 (Or (Eq (v4_group_1 a) False) % 32.94/33.15 (Or % 32.94/33.15 (Eq % 32.94/33.15 (Iff (Eq a_1 (k1_latsubgr a)) % 32.94/33.15 (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C))) % 32.94/33.15 True) % 32.94/33.15 (Or (Eq (Not (v3_struct_0 a)) False) % 32.94/33.15 (Or (Eq (v3_group_1 a) False) % 32.94/33.15 (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) % 32.94/33.15 (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False)))))) % 32.94/33.15 Clause #213 (by clausification #[211]): ∀ (a a_1 : Iota), % 32.94/33.15 Or (Eq (l1_group_1 a) False) % 32.94/33.15 (Or (Eq (v4_group_1 a) False) % 32.94/33.15 (Or (Eq (Not (v3_struct_0 a)) False) % 32.94/33.15 (Or (Eq (v3_group_1 a) False) % 32.94/33.15 (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) % 32.94/33.15 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 32.94/33.15 (Or (Eq (Eq a_1 (k1_latsubgr a)) False) % 32.94/33.15 (Eq (∀ (C : Iota), And (v1_group_1 C) (m1_group_2 C a) → Eq (k1_funct_1 a_1 C) (u1_struct_0 C)) % 32.94/33.15 True))))))) % 32.94/33.15 Clause #253 (by clausification #[10]): ∀ (a : Iota), % 32.94/33.15 Eq % 32.94/33.15 (And (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) (l1_group_1 a) → % 32.94/33.15 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)))) % 32.94/33.15 (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.15 True % 32.94/33.15 Clause #254 (by clausification #[253]): ∀ (a : Iota), % 32.94/33.15 Or (Eq (And (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) (l1_group_1 a)) False) % 32.94/33.15 (Eq % 32.94/33.15 (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)))) % 32.94/33.15 (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.15 True) % 32.94/33.15 Clause #255 (by clausification #[254]): ∀ (a : Iota), % 32.94/33.15 Or % 32.94/33.15 (Eq % 32.94/33.15 (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)))) % 32.94/33.15 (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a)))) % 32.94/33.15 True) % 32.94/33.15 (Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) (Eq (l1_group_1 a) False)) % 32.94/33.15 Clause #256 (by clausification #[255]): ∀ (a : Iota), % 32.94/33.15 Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) % 32.94/33.15 (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)) % 32.94/33.15 Clause #257 (by clausification #[255]): ∀ (a : Iota), % 32.94/33.15 Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (v4_group_1 a)) False) % 32.94/33.15 (Or (Eq (l1_group_1 a) False) % 32.94/33.15 (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)))) % 32.94/33.15 True)) % 32.94/33.15 Clause #258 (by clausification #[256]): ∀ (a : Iota), % 32.94/33.15 Or (Eq (l1_group_1 a) False) % 32.94/33.15 (Or (Eq (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True) % 32.94/33.15 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) (Eq (v4_group_1 a) False))) % 32.94/33.15 Clause #259 (by clausification #[258]): ∀ (a : Iota), % 32.94/33.15 Or (Eq (l1_group_1 a) False) % 32.94/33.15 (Or (Eq (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True) % 32.94/33.15 (Or (Eq (v4_group_1 a) False) (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False)))) % 32.94/33.15 Clause #260 (by clausification #[259]): ∀ (a : Iota), % 32.94/33.15 Or (Eq (l1_group_1 a) False) % 32.94/33.15 (Or (Eq (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True) % 32.94/33.15 (Or (Eq (v4_group_1 a) False) (Or (Eq (v3_group_1 a) False) (Eq (v3_struct_0 a) True)))) % 32.94/33.15 Clause #261 (by superposition #[260, 56]): ∀ (a : Iota), % 32.94/33.15 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 32.94/33.15 (Or (Eq (v4_group_1 (skS.0 1 a)) False) % 32.94/33.15 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Or (Eq (v3_struct_0 (skS.0 1 a)) True) (Eq False True)))) % 32.94/33.15 Clause #272 (by clausification #[12]): ∀ (a : Iota), % 32.94/33.15 Eq % 32.94/33.18 (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (l1_group_1 a) → % 32.94/33.18 ∀ (B : Iota), m1_group_2 B a → And (And (Not (v3_struct_0 B)) (v3_group_1 B)) (l1_group_1 B)) % 32.94/33.18 True % 32.94/33.18 Clause #273 (by clausification #[272]): ∀ (a : Iota), % 32.94/33.18 Or (Eq (And (And (Not (v3_struct_0 a)) (v3_group_1 a)) (l1_group_1 a)) False) % 32.94/33.18 (Eq (∀ (B : Iota), m1_group_2 B a → And (And (Not (v3_struct_0 B)) (v3_group_1 B)) (l1_group_1 B)) True) % 32.94/33.18 Clause #274 (by clausification #[273]): ∀ (a : Iota), % 32.94/33.18 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) % 32.94/33.18 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) (Eq (l1_group_1 a) False)) % 32.94/33.18 Clause #275 (by clausification #[274]): ∀ (a a_1 : Iota), % 32.94/33.18 Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) % 32.94/33.18 (Or (Eq (l1_group_1 a) False) % 32.94/33.18 (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)) % 32.94/33.18 Clause #276 (by clausification #[275]): ∀ (a a_1 : Iota), % 32.94/33.18 Or (Eq (l1_group_1 a) False) % 32.94/33.18 (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) % 32.94/33.18 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False))) % 32.94/33.18 Clause #277 (by clausification #[276]): ∀ (a a_1 : Iota), % 32.94/33.18 Or (Eq (l1_group_1 a) False) % 32.94/33.18 (Or (Eq (Not (v3_struct_0 a)) False) % 32.94/33.18 (Or (Eq (v3_group_1 a) False) % 32.94/33.18 (Or (Eq (m1_group_2 a_1 a) False) % 32.94/33.18 (Eq (And (And (Not (v3_struct_0 a_1)) (v3_group_1 a_1)) (l1_group_1 a_1)) True)))) % 32.94/33.18 Clause #278 (by clausification #[277]): ∀ (a a_1 : Iota), % 32.94/33.18 Or (Eq (l1_group_1 a) False) % 32.94/33.18 (Or (Eq (v3_group_1 a) False) % 32.94/33.18 (Or (Eq (m1_group_2 a_1 a) False) % 32.94/33.18 (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)))) % 32.94/33.18 Clause #279 (by clausification #[278]): ∀ (a a_1 : Iota), % 32.94/33.18 Or (Eq (l1_group_1 a) False) % 32.94/33.18 (Or (Eq (v3_group_1 a) False) % 32.94/33.18 (Or (Eq (m1_group_2 a_1 a) False) (Or (Eq (v3_struct_0 a) True) (Eq (l1_group_1 a_1) True)))) % 32.94/33.18 Clause #280 (by clausification #[278]): ∀ (a a_1 : Iota), % 32.94/33.18 Or (Eq (l1_group_1 a) False) % 32.94/33.18 (Or (Eq (v3_group_1 a) False) % 32.94/33.18 (Or (Eq (m1_group_2 a_1 a) False) % 32.94/33.18 (Or (Eq (v3_struct_0 a) True) (Eq (And (Not (v3_struct_0 a_1)) (v3_group_1 a_1)) True)))) % 32.94/33.18 Clause #281 (by superposition #[279, 56]): ∀ (a a_1 : Iota), % 32.94/33.18 Or (Eq (v3_group_1 (skS.0 1 a)) False) % 32.94/33.18 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 32.94/33.18 (Or (Eq (v3_struct_0 (skS.0 1 a)) True) (Or (Eq (l1_group_1 a_1) True) (Eq False True)))) % 32.94/33.18 Clause #314 (by clausification #[55]): ∀ (a a_1 : Iota), % 32.94/33.18 Eq % 32.94/33.18 (Not % 32.94/33.18 (And (v1_group_1 (skS.0 13 a a_1)) (m1_group_2 (skS.0 13 a a_1) (skS.0 1 a)) → % 32.94/33.18 Ne (k1_funct_1 (k1_latsubgr (skS.0 1 a)) (skS.0 13 a a_1)) k1_xboole_0)) % 32.94/33.18 True % 32.94/33.18 Clause #315 (by clausification #[314]): ∀ (a a_1 : Iota), % 32.94/33.18 Eq % 32.94/33.18 (And (v1_group_1 (skS.0 13 a a_1)) (m1_group_2 (skS.0 13 a a_1) (skS.0 1 a)) → % 32.94/33.18 Ne (k1_funct_1 (k1_latsubgr (skS.0 1 a)) (skS.0 13 a a_1)) k1_xboole_0) % 32.94/33.18 False % 32.94/33.18 Clause #316 (by clausification #[315]): ∀ (a a_1 : Iota), Eq (And (v1_group_1 (skS.0 13 a a_1)) (m1_group_2 (skS.0 13 a a_1) (skS.0 1 a))) True % 32.94/33.18 Clause #317 (by clausification #[315]): ∀ (a a_1 : Iota), Eq (Ne (k1_funct_1 (k1_latsubgr (skS.0 1 a)) (skS.0 13 a a_1)) k1_xboole_0) False % 32.94/33.18 Clause #318 (by clausification #[316]): ∀ (a a_1 : Iota), Eq (m1_group_2 (skS.0 13 a a_1) (skS.0 1 a)) True % 32.94/33.18 Clause #319 (by clausification #[316]): ∀ (a a_1 : Iota), Eq (v1_group_1 (skS.0 13 a a_1)) True % 32.94/33.18 Clause #375 (by clausification #[57]): ∀ (a : Iota), Eq (v4_group_1 (skS.0 1 a)) True % 32.94/33.18 Clause #376 (by clausification #[57]): ∀ (a : Iota), Eq (And (Not (v3_struct_0 (skS.0 1 a))) (v3_group_1 (skS.0 1 a))) True % 32.94/33.18 Clause #414 (by clausification #[376]): ∀ (a : Iota), Eq (v3_group_1 (skS.0 1 a)) True % 32.94/33.18 Clause #415 (by clausification #[376]): ∀ (a : Iota), Eq (Not (v3_struct_0 (skS.0 1 a))) True % 32.94/33.18 Clause #417 (by clausification #[415]): ∀ (a : Iota), Eq (v3_struct_0 (skS.0 1 a)) False % 32.94/33.18 Clause #464 (by clausification #[317]): ∀ (a a_1 : Iota), Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) (skS.0 13 a a_1)) k1_xboole_0 % 33.03/33.21 Clause #466 (by clausification #[280]): ∀ (a a_1 : Iota), % 33.03/33.21 Or (Eq (l1_group_1 a) False) % 33.03/33.21 (Or (Eq (v3_group_1 a) False) % 33.03/33.21 (Or (Eq (m1_group_2 a_1 a) False) (Or (Eq (v3_struct_0 a) True) (Eq (Not (v3_struct_0 a_1)) True)))) % 33.03/33.21 Clause #470 (by clausification #[466]): ∀ (a a_1 : Iota), % 33.03/33.21 Or (Eq (l1_group_1 a) False) % 33.03/33.21 (Or (Eq (v3_group_1 a) False) % 33.03/33.21 (Or (Eq (m1_group_2 a_1 a) False) (Or (Eq (v3_struct_0 a) True) (Eq (v3_struct_0 a_1) False)))) % 33.03/33.21 Clause #471 (by superposition #[470, 56]): ∀ (a a_1 : Iota), % 33.03/33.21 Or (Eq (v3_group_1 (skS.0 1 a)) False) % 33.03/33.21 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 33.03/33.21 (Or (Eq (v3_struct_0 (skS.0 1 a)) True) (Or (Eq (v3_struct_0 a_1) False) (Eq False True)))) % 33.03/33.21 Clause #512 (by clausification #[213]): ∀ (a a_1 : Iota), % 33.03/33.21 Or (Eq (l1_group_1 a) False) % 33.03/33.21 (Or (Eq (v4_group_1 a) False) % 33.03/33.21 (Or (Eq (v3_group_1 a) False) % 33.03/33.21 (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) % 33.03/33.21 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.21 (Or (Eq (Eq a_1 (k1_latsubgr a)) False) % 33.03/33.21 (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) % 33.03/33.21 (Eq (v3_struct_0 a) True))))))) % 33.03/33.21 Clause #513 (by clausification #[512]): ∀ (a a_1 : Iota), % 33.03/33.21 Or (Eq (l1_group_1 a) False) % 33.03/33.21 (Or (Eq (v4_group_1 a) False) % 33.03/33.21 (Or (Eq (v3_group_1 a) False) % 33.03/33.21 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.21 (Or (Eq (Eq a_1 (k1_latsubgr a)) False) % 33.03/33.21 (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) % 33.03/33.21 (Or (Eq (v3_struct_0 a) True) % 33.03/33.21 (Or (Eq (v1_funct_1 a_1) False) % 33.03/33.21 (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False)))))))) % 33.03/33.21 Clause #514 (by clausification #[513]): ∀ (a a_1 : Iota), % 33.03/33.21 Or (Eq (l1_group_1 a) False) % 33.03/33.21 (Or (Eq (v4_group_1 a) False) % 33.03/33.21 (Or (Eq (v3_group_1 a) False) % 33.03/33.21 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.21 (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) % 33.03/33.21 (Or (Eq (v3_struct_0 a) True) % 33.03/33.21 (Or (Eq (v1_funct_1 a_1) False) % 33.03/33.21 (Or (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.21 (Ne a_1 (k1_latsubgr a))))))))) % 33.03/33.21 Clause #515 (by clausification #[514]): ∀ (a a_1 a_2 : Iota), % 33.03/33.21 Or (Eq (l1_group_1 a) False) % 33.03/33.21 (Or (Eq (v4_group_1 a) False) % 33.03/33.21 (Or (Eq (v3_group_1 a) False) % 33.03/33.21 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.21 (Or (Eq (v3_struct_0 a) True) % 33.03/33.21 (Or (Eq (v1_funct_1 a_1) False) % 33.03/33.21 (Or (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.21 (Or (Ne a_1 (k1_latsubgr a)) % 33.03/33.21 (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)))))))) % 33.03/33.21 Clause #516 (by clausification #[515]): ∀ (a a_1 a_2 : Iota), % 33.03/33.21 Or (Eq (l1_group_1 a) False) % 33.03/33.21 (Or (Eq (v4_group_1 a) False) % 33.03/33.21 (Or (Eq (v3_group_1 a) False) % 33.03/33.21 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.21 (Or (Eq (v3_struct_0 a) True) % 33.03/33.21 (Or (Eq (v1_funct_1 a_1) False) % 33.03/33.21 (Or (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.21 (Or (Ne a_1 (k1_latsubgr a)) % 33.03/33.21 (Or (Eq (And (v1_group_1 a_2) (m1_group_2 a_2 a)) False) % 33.03/33.21 (Eq (Eq (k1_funct_1 a_1 a_2) (u1_struct_0 a_2)) True))))))))) % 33.03/33.21 Clause #517 (by clausification #[516]): ∀ (a a_1 a_2 : Iota), % 33.03/33.21 Or (Eq (l1_group_1 a) False) % 33.03/33.21 (Or (Eq (v4_group_1 a) False) % 33.03/33.21 (Or (Eq (v3_group_1 a) False) % 33.03/33.21 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.21 (Or (Eq (v3_struct_0 a) True) % 33.03/33.21 (Or (Eq (v1_funct_1 a_1) False) % 33.03/33.23 (Or (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.23 (Or (Ne a_1 (k1_latsubgr a)) % 33.03/33.23 (Or (Eq (Eq (k1_funct_1 a_1 a_2) (u1_struct_0 a_2)) True) % 33.03/33.23 (Or (Eq (v1_group_1 a_2) False) (Eq (m1_group_2 a_2 a) False)))))))))) % 33.03/33.23 Clause #518 (by clausification #[517]): ∀ (a a_1 a_2 : Iota), % 33.03/33.23 Or (Eq (l1_group_1 a) False) % 33.03/33.23 (Or (Eq (v4_group_1 a) False) % 33.03/33.23 (Or (Eq (v3_group_1 a) False) % 33.03/33.23 (Or (Eq (m2_relset_1 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.23 (Or (Eq (v3_struct_0 a) True) % 33.03/33.23 (Or (Eq (v1_funct_1 a_1) False) % 33.03/33.23 (Or (Eq (v1_funct_2 a_1 (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.23 (Or (Ne a_1 (k1_latsubgr a)) % 33.03/33.23 (Or (Eq (v1_group_1 a_2) False) % 33.03/33.23 (Or (Eq (m1_group_2 a_2 a) False) (Eq (k1_funct_1 a_1 a_2) (u1_struct_0 a_2))))))))))) % 33.03/33.23 Clause #519 (by destructive equality resolution #[518]): ∀ (a a_1 : Iota), % 33.03/33.23 Or (Eq (l1_group_1 a) False) % 33.03/33.23 (Or (Eq (v4_group_1 a) False) % 33.03/33.23 (Or (Eq (v3_group_1 a) False) % 33.03/33.23 (Or (Eq (m2_relset_1 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.23 (Or (Eq (v3_struct_0 a) True) % 33.03/33.23 (Or (Eq (v1_funct_1 (k1_latsubgr a)) False) % 33.03/33.23 (Or (Eq (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) False) % 33.03/33.23 (Or (Eq (v1_group_1 a_1) False) % 33.03/33.23 (Or (Eq (m1_group_2 a_1 a) False) (Eq (k1_funct_1 (k1_latsubgr a) a_1) (u1_struct_0 a_1)))))))))) % 33.03/33.23 Clause #520 (by superposition #[519, 56]): ∀ (a a_1 : Iota), % 33.03/33.23 Or (Eq (v4_group_1 (skS.0 1 a)) False) % 33.03/33.23 (Or (Eq (v3_group_1 (skS.0 1 a)) False) % 33.03/33.23 (Or % 33.03/33.23 (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.03/33.23 False) % 33.03/33.23 (Or (Eq (v3_struct_0 (skS.0 1 a)) True) % 33.03/33.23 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) False) % 33.03/33.23 (Or % 33.03/33.23 (Eq % 33.03/33.23 (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.03/33.23 False) % 33.03/33.23 (Or (Eq (v1_group_1 a_1) False) % 33.03/33.23 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 33.03/33.23 (Or (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1)) (Eq False True))))))))) % 33.03/33.23 Clause #584 (by clausification #[257]): ∀ (a : Iota), % 33.03/33.23 Or (Eq (l1_group_1 a) False) % 33.03/33.23 (Or % 33.03/33.23 (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)))) % 33.03/33.23 True) % 33.03/33.23 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) (Eq (v4_group_1 a) False))) % 33.03/33.23 Clause #585 (by clausification #[584]): ∀ (a : Iota), % 33.03/33.23 Or (Eq (l1_group_1 a) False) % 33.03/33.23 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) % 33.03/33.23 (Or (Eq (v4_group_1 a) False) % 33.03/33.23 (Eq (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True))) % 33.03/33.23 Clause #586 (by clausification #[584]): ∀ (a : Iota), % 33.03/33.23 Or (Eq (l1_group_1 a) False) % 33.03/33.23 (Or (Eq (And (Not (v3_struct_0 a)) (v3_group_1 a)) False) % 33.03/33.23 (Or (Eq (v4_group_1 a) False) (Eq (v1_funct_1 (k1_latsubgr a)) True))) % 33.03/33.23 Clause #587 (by clausification #[585]): ∀ (a : Iota), % 33.03/33.23 Or (Eq (l1_group_1 a) False) % 33.03/33.23 (Or (Eq (v4_group_1 a) False) % 33.03/33.23 (Or (Eq (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True) % 33.03/33.23 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False)))) % 33.03/33.23 Clause #588 (by clausification #[587]): ∀ (a : Iota), % 33.03/33.23 Or (Eq (l1_group_1 a) False) % 33.03/33.23 (Or (Eq (v4_group_1 a) False) % 33.03/33.23 (Or (Eq (v1_funct_2 (k1_latsubgr a) (k1_group_3 a) (k1_zfmisc_1 (u1_struct_0 a))) True) % 33.03/33.23 (Or (Eq (v3_group_1 a) False) (Eq (v3_struct_0 a) True)))) % 33.03/33.23 Clause #589 (by superposition #[588, 56]): ∀ (a : Iota), % 33.03/33.23 Or (Eq (v4_group_1 (skS.0 1 a)) False) % 33.03/33.23 (Or % 33.03/33.23 (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.03/33.23 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Or (Eq (v3_struct_0 (skS.0 1 a)) True) (Eq False True)))) % 33.03/33.26 Clause #592 (by clausification #[586]): ∀ (a : Iota), % 33.03/33.26 Or (Eq (l1_group_1 a) False) % 33.03/33.26 (Or (Eq (v4_group_1 a) False) % 33.03/33.26 (Or (Eq (v1_funct_1 (k1_latsubgr a)) True) (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v3_group_1 a) False)))) % 33.03/33.26 Clause #593 (by clausification #[592]): ∀ (a : Iota), % 33.03/33.26 Or (Eq (l1_group_1 a) False) % 33.03/33.26 (Or (Eq (v4_group_1 a) False) % 33.03/33.26 (Or (Eq (v1_funct_1 (k1_latsubgr a)) True) (Or (Eq (v3_group_1 a) False) (Eq (v3_struct_0 a) True)))) % 33.03/33.26 Clause #594 (by superposition #[593, 56]): ∀ (a : Iota), % 33.03/33.26 Or (Eq (v4_group_1 (skS.0 1 a)) False) % 33.03/33.26 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) True) % 33.03/33.26 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Or (Eq (v3_struct_0 (skS.0 1 a)) True) (Eq False True)))) % 33.03/33.26 Clause #606 (by clausification #[471]): ∀ (a a_1 : Iota), % 33.03/33.26 Or (Eq (v3_group_1 (skS.0 1 a)) False) % 33.03/33.26 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) (Or (Eq (v3_struct_0 (skS.0 1 a)) True) (Eq (v3_struct_0 a_1) False))) % 33.03/33.26 Clause #607 (by forward demodulation #[606, 414]): ∀ (a a_1 : Iota), % 33.03/33.26 Or (Eq True False) % 33.03/33.26 (Or (Eq (m1_group_2 a (skS.0 1 a_1)) False) (Or (Eq (v3_struct_0 (skS.0 1 a_1)) True) (Eq (v3_struct_0 a) False))) % 33.03/33.26 Clause #608 (by clausification #[607]): ∀ (a a_1 : Iota), % 33.03/33.26 Or (Eq (m1_group_2 a (skS.0 1 a_1)) False) (Or (Eq (v3_struct_0 (skS.0 1 a_1)) True) (Eq (v3_struct_0 a) False)) % 33.03/33.26 Clause #609 (by forward demodulation #[608, 417]): ∀ (a a_1 : Iota), Or (Eq (m1_group_2 a (skS.0 1 a_1)) False) (Or (Eq False True) (Eq (v3_struct_0 a) False)) % 33.03/33.26 Clause #610 (by clausification #[609]): ∀ (a a_1 : Iota), Or (Eq (m1_group_2 a (skS.0 1 a_1)) False) (Eq (v3_struct_0 a) False) % 33.03/33.26 Clause #611 (by superposition #[610, 318]): ∀ (a a_1 : Iota), Or (Eq (v3_struct_0 (skS.0 13 a a_1)) False) (Eq False True) % 33.03/33.26 Clause #613 (by clausification #[261]): ∀ (a : Iota), % 33.03/33.26 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.03/33.26 (Or (Eq (v4_group_1 (skS.0 1 a)) False) % 33.03/33.26 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Eq (v3_struct_0 (skS.0 1 a)) True))) % 33.03/33.26 Clause #614 (by forward demodulation #[613, 375]): ∀ (a : Iota), % 33.03/33.26 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.03/33.26 (Or (Eq True False) (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Eq (v3_struct_0 (skS.0 1 a)) True))) % 33.03/33.26 Clause #615 (by clausification #[614]): ∀ (a : Iota), % 33.03/33.26 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.03/33.26 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Eq (v3_struct_0 (skS.0 1 a)) True)) % 33.03/33.26 Clause #616 (by forward demodulation #[615, 414]): ∀ (a : Iota), % 33.03/33.26 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.03/33.26 (Or (Eq True False) (Eq (v3_struct_0 (skS.0 1 a)) True)) % 33.03/33.26 Clause #617 (by clausification #[616]): ∀ (a : Iota), % 33.03/33.26 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.03/33.26 (Eq (v3_struct_0 (skS.0 1 a)) True) % 33.03/33.26 Clause #618 (by forward demodulation #[617, 417]): ∀ (a : Iota), % 33.03/33.26 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.03/33.26 (Eq False True) % 33.03/33.26 Clause #619 (by clausification #[618]): ∀ (a : Iota), % 33.03/33.26 Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True % 33.03/33.26 Clause #622 (by clausification #[611]): ∀ (a a_1 : Iota), Eq (v3_struct_0 (skS.0 13 a a_1)) False % 33.03/33.26 Clause #640 (by clausification #[281]): ∀ (a a_1 : Iota), % 33.03/33.26 Or (Eq (v3_group_1 (skS.0 1 a)) False) % 33.03/33.26 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) (Or (Eq (v3_struct_0 (skS.0 1 a)) True) (Eq (l1_group_1 a_1) True))) % 33.03/33.26 Clause #641 (by forward demodulation #[640, 414]): ∀ (a a_1 : Iota), % 33.03/33.26 Or (Eq True False) % 33.03/33.26 (Or (Eq (m1_group_2 a (skS.0 1 a_1)) False) (Or (Eq (v3_struct_0 (skS.0 1 a_1)) True) (Eq (l1_group_1 a) True))) % 33.03/33.26 Clause #642 (by clausification #[641]): ∀ (a a_1 : Iota), % 33.03/33.26 Or (Eq (m1_group_2 a (skS.0 1 a_1)) False) (Or (Eq (v3_struct_0 (skS.0 1 a_1)) True) (Eq (l1_group_1 a) True)) % 33.03/33.28 Clause #643 (by forward demodulation #[642, 417]): ∀ (a a_1 : Iota), Or (Eq (m1_group_2 a (skS.0 1 a_1)) False) (Or (Eq False True) (Eq (l1_group_1 a) True)) % 33.03/33.28 Clause #644 (by clausification #[643]): ∀ (a a_1 : Iota), Or (Eq (m1_group_2 a (skS.0 1 a_1)) False) (Eq (l1_group_1 a) True) % 33.03/33.28 Clause #645 (by superposition #[644, 318]): ∀ (a a_1 : Iota), Or (Eq (l1_group_1 (skS.0 13 a a_1)) True) (Eq False True) % 33.03/33.28 Clause #647 (by clausification #[645]): ∀ (a a_1 : Iota), Eq (l1_group_1 (skS.0 13 a a_1)) True % 33.03/33.28 Clause #648 (by superposition #[647, 46]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (l1_struct_0 (skS.0 13 a a_1)) True) % 33.03/33.28 Clause #665 (by clausification #[648]): ∀ (a a_1 : Iota), Eq (l1_struct_0 (skS.0 13 a a_1)) True % 33.03/33.28 Clause #666 (by superposition #[665, 97]): ∀ (a a_1 : Iota), % 33.03/33.28 Or (Eq True False) % 33.03/33.28 (Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 13 a a_1))) False) (Eq (v3_struct_0 (skS.0 13 a a_1)) True)) % 33.03/33.28 Clause #696 (by clausification #[666]): ∀ (a a_1 : Iota), Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 13 a a_1))) False) (Eq (v3_struct_0 (skS.0 13 a a_1)) True) % 33.03/33.28 Clause #697 (by forward demodulation #[696, 622]): ∀ (a a_1 : Iota), Or (Eq (v1_xboole_0 (u1_struct_0 (skS.0 13 a a_1))) False) (Eq False True) % 33.03/33.28 Clause #698 (by clausification #[697]): ∀ (a a_1 : Iota), Eq (v1_xboole_0 (u1_struct_0 (skS.0 13 a a_1))) False % 33.03/33.28 Clause #876 (by clausification #[594]): ∀ (a : Iota), % 33.03/33.28 Or (Eq (v4_group_1 (skS.0 1 a)) False) % 33.03/33.28 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) True) % 33.03/33.28 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Eq (v3_struct_0 (skS.0 1 a)) True))) % 33.03/33.28 Clause #877 (by forward demodulation #[876, 375]): ∀ (a : Iota), % 33.03/33.28 Or (Eq True False) % 33.03/33.28 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) True) % 33.03/33.28 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Eq (v3_struct_0 (skS.0 1 a)) True))) % 33.03/33.28 Clause #878 (by clausification #[877]): ∀ (a : Iota), % 33.03/33.28 Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) True) % 33.03/33.28 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Eq (v3_struct_0 (skS.0 1 a)) True)) % 33.03/33.28 Clause #879 (by forward demodulation #[878, 414]): ∀ (a : Iota), % 33.03/33.28 Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) True) (Or (Eq True False) (Eq (v3_struct_0 (skS.0 1 a)) True)) % 33.03/33.28 Clause #880 (by clausification #[879]): ∀ (a : Iota), Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) True) (Eq (v3_struct_0 (skS.0 1 a)) True) % 33.03/33.28 Clause #881 (by forward demodulation #[880, 417]): ∀ (a : Iota), Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) True) (Eq False True) % 33.03/33.28 Clause #882 (by clausification #[881]): ∀ (a : Iota), Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) True % 33.03/33.28 Clause #917 (by clausification #[520]): ∀ (a a_1 : Iota), % 33.03/33.28 Or (Eq (v4_group_1 (skS.0 1 a)) False) % 33.03/33.28 (Or (Eq (v3_group_1 (skS.0 1 a)) False) % 33.03/33.28 (Or % 33.03/33.28 (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.03/33.28 False) % 33.03/33.28 (Or (Eq (v3_struct_0 (skS.0 1 a)) True) % 33.03/33.28 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) False) % 33.03/33.28 (Or % 33.03/33.28 (Eq % 33.03/33.28 (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.03/33.28 False) % 33.03/33.28 (Or (Eq (v1_group_1 a_1) False) % 33.03/33.28 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 33.03/33.28 (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1))))))))) % 33.03/33.28 Clause #918 (by forward demodulation #[917, 375]): ∀ (a a_1 : Iota), % 33.03/33.28 Or (Eq True False) % 33.03/33.28 (Or (Eq (v3_group_1 (skS.0 1 a)) False) % 33.03/33.28 (Or % 33.03/33.28 (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.03/33.28 False) % 33.03/33.28 (Or (Eq (v3_struct_0 (skS.0 1 a)) True) % 33.03/33.28 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) False) % 33.03/33.28 (Or % 33.03/33.28 (Eq % 33.03/33.28 (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.03/33.28 False) % 33.03/33.28 (Or (Eq (v1_group_1 a_1) False) % 33.03/33.28 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 33.03/33.28 (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1))))))))) % 33.14/33.31 Clause #919 (by clausification #[918]): ∀ (a a_1 : Iota), % 33.14/33.31 Or (Eq (v3_group_1 (skS.0 1 a)) False) % 33.14/33.31 (Or % 33.14/33.31 (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.14/33.31 False) % 33.14/33.31 (Or (Eq (v3_struct_0 (skS.0 1 a)) True) % 33.14/33.31 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) False) % 33.14/33.31 (Or % 33.14/33.31 (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.14/33.31 False) % 33.14/33.31 (Or (Eq (v1_group_1 a_1) False) % 33.14/33.31 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 33.14/33.31 (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1)))))))) % 33.14/33.31 Clause #920 (by forward demodulation #[919, 414]): ∀ (a a_1 : Iota), % 33.14/33.31 Or (Eq True False) % 33.14/33.31 (Or % 33.14/33.31 (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.14/33.31 False) % 33.14/33.31 (Or (Eq (v3_struct_0 (skS.0 1 a)) True) % 33.14/33.31 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) False) % 33.14/33.31 (Or % 33.14/33.31 (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.14/33.31 False) % 33.14/33.31 (Or (Eq (v1_group_1 a_1) False) % 33.14/33.31 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 33.14/33.31 (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1)))))))) % 33.14/33.31 Clause #921 (by clausification #[920]): ∀ (a a_1 : Iota), % 33.14/33.31 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) False) % 33.14/33.31 (Or (Eq (v3_struct_0 (skS.0 1 a)) True) % 33.14/33.31 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) False) % 33.14/33.31 (Or % 33.14/33.31 (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.14/33.31 False) % 33.14/33.31 (Or (Eq (v1_group_1 a_1) False) % 33.14/33.31 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 33.14/33.31 (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1))))))) % 33.14/33.31 Clause #922 (by forward demodulation #[921, 417]): ∀ (a a_1 : Iota), % 33.14/33.31 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) False) % 33.14/33.31 (Or (Eq False True) % 33.14/33.31 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) False) % 33.14/33.31 (Or % 33.14/33.31 (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.14/33.31 False) % 33.14/33.31 (Or (Eq (v1_group_1 a_1) False) % 33.14/33.31 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 33.14/33.31 (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1))))))) % 33.14/33.31 Clause #923 (by clausification #[922]): ∀ (a a_1 : Iota), % 33.14/33.31 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) False) % 33.14/33.31 (Or (Eq (v1_funct_1 (k1_latsubgr (skS.0 1 a))) False) % 33.14/33.31 (Or % 33.14/33.31 (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.14/33.31 False) % 33.14/33.31 (Or (Eq (v1_group_1 a_1) False) % 33.14/33.31 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 33.14/33.31 (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1)))))) % 33.14/33.31 Clause #924 (by forward demodulation #[923, 882]): ∀ (a a_1 : Iota), % 33.14/33.31 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) False) % 33.14/33.31 (Or (Eq True False) % 33.14/33.31 (Or % 33.14/33.31 (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) % 33.14/33.31 False) % 33.14/33.31 (Or (Eq (v1_group_1 a_1) False) % 33.14/33.31 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) % 33.14/33.31 (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1)))))) % 33.14/33.31 Clause #925 (by clausification #[924]): ∀ (a a_1 : Iota), % 33.14/33.31 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) False) % 33.14/33.31 (Or % 33.14/33.31 (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) False) % 33.14/33.31 (Or (Eq (v1_group_1 a_1) False) % 33.15/33.34 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1))))) % 33.15/33.34 Clause #1123 (by clausification #[589]): ∀ (a : Iota), % 33.15/33.34 Or (Eq (v4_group_1 (skS.0 1 a)) False) % 33.15/33.34 (Or % 33.15/33.34 (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.15/33.34 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Eq (v3_struct_0 (skS.0 1 a)) True))) % 33.15/33.34 Clause #1124 (by forward demodulation #[1123, 375]): ∀ (a : Iota), % 33.15/33.34 Or (Eq True False) % 33.15/33.34 (Or % 33.15/33.34 (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.15/33.34 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Eq (v3_struct_0 (skS.0 1 a)) True))) % 33.15/33.34 Clause #1125 (by clausification #[1124]): ∀ (a : Iota), % 33.15/33.34 Or (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.15/33.34 (Or (Eq (v3_group_1 (skS.0 1 a)) False) (Eq (v3_struct_0 (skS.0 1 a)) True)) % 33.15/33.34 Clause #1126 (by forward demodulation #[1125, 414]): ∀ (a : Iota), % 33.15/33.34 Or (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.15/33.34 (Or (Eq True False) (Eq (v3_struct_0 (skS.0 1 a)) True)) % 33.15/33.34 Clause #1127 (by clausification #[1126]): ∀ (a : Iota), % 33.15/33.34 Or (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.15/33.34 (Eq (v3_struct_0 (skS.0 1 a)) True) % 33.15/33.34 Clause #1128 (by forward demodulation #[1127, 417]): ∀ (a : Iota), % 33.15/33.34 Or (Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True) % 33.15/33.34 (Eq False True) % 33.15/33.34 Clause #1129 (by clausification #[1128]): ∀ (a : Iota), % 33.15/33.34 Eq (v1_funct_2 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) True % 33.15/33.34 Clause #1130 (by backward demodulation #[1129, 925]): ∀ (a a_1 : Iota), % 33.15/33.34 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) False) % 33.15/33.34 (Or (Eq True False) % 33.15/33.34 (Or (Eq (v1_group_1 a_1) False) % 33.15/33.34 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1))))) % 33.15/33.34 Clause #1819 (by clausification #[1130]): ∀ (a a_1 : Iota), % 33.15/33.34 Or (Eq (m2_relset_1 (k1_latsubgr (skS.0 1 a)) (k1_group_3 (skS.0 1 a)) (k1_zfmisc_1 (u1_struct_0 (skS.0 1 a)))) False) % 33.15/33.34 (Or (Eq (v1_group_1 a_1) False) % 33.15/33.34 (Or (Eq (m1_group_2 a_1 (skS.0 1 a)) False) (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) a_1) (u1_struct_0 a_1)))) % 33.15/33.34 Clause #1820 (by superposition #[1819, 619]): ∀ (a a_1 : Iota), % 33.15/33.34 Or (Eq (v1_group_1 a) False) % 33.15/33.34 (Or (Eq (m1_group_2 a (skS.0 1 a_1)) False) % 33.15/33.34 (Or (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a_1)) a) (u1_struct_0 a)) (Eq False True))) % 33.15/33.34 Clause #1836 (by clausification #[1820]): ∀ (a a_1 : Iota), % 33.15/33.34 Or (Eq (v1_group_1 a) False) % 33.15/33.34 (Or (Eq (m1_group_2 a (skS.0 1 a_1)) False) (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a_1)) a) (u1_struct_0 a))) % 33.15/33.34 Clause #1837 (by superposition #[1836, 319]): ∀ (a a_1 a_2 : Iota), % 33.15/33.34 Or (Eq (m1_group_2 (skS.0 13 a a_1) (skS.0 1 a_2)) False) % 33.15/33.34 (Or (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a_2)) (skS.0 13 a a_1)) (u1_struct_0 (skS.0 13 a a_1))) (Eq False True)) % 33.15/33.34 Clause #1840 (by clausification #[1837]): ∀ (a a_1 a_2 : Iota), % 33.15/33.34 Or (Eq (m1_group_2 (skS.0 13 a a_1) (skS.0 1 a_2)) False) % 33.15/33.34 (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a_2)) (skS.0 13 a a_1)) (u1_struct_0 (skS.0 13 a a_1))) % 33.15/33.34 Clause #1841 (by superposition #[1840, 318]): ∀ (a a_1 : Iota), % 33.15/33.34 Or (Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) (skS.0 13 a a_1)) (u1_struct_0 (skS.0 13 a a_1))) (Eq False True) % 33.15/33.34 Clause #1842 (by clausification #[1841]): ∀ (a a_1 : Iota), Eq (k1_funct_1 (k1_latsubgr (skS.0 1 a)) (skS.0 13 a a_1)) (u1_struct_0 (skS.0 13 a a_1)) % 33.15/33.34 Clause #1843 (by superposition #[1842, 464]): ∀ (a a_1 : Iota), Eq (u1_struct_0 (skS.0 13 a a_1)) k1_xboole_0 % 33.15/33.34 Clause #1844 (by backward demodulation #[1843, 698]): Eq (v1_xboole_0 k1_xboole_0) False % 33.15/33.34 Clause #1867 (by superposition #[1844, 24]): Eq False True % 33.15/33.34 Clause #1868 (by clausification #[1867]): False % 33.15/33.34 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------