%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU444+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 08:01:41 PM UTC 2025 % Result : Theorem 48.02s 48.25s % Output : Proof 48.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : SEU444+1 : TPTP v9.2.0. Released v3.4.0. % 0.09/0.11 % Command : duper %s % 0.09/0.31 % Computer : n023.cluster.edu % 0.09/0.31 % Model : x86_64 x86_64 % 0.09/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.31 % Memory : 8042.1875MB % 0.09/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.31 % CPULimit : 300 % 0.09/0.31 % WCLimit : 300 % 0.09/0.31 % DateTime : Fri Oct 3 04:44:53 EDT 2025 % 0.09/0.31 % CPUTime : % 48.02/48.25 SZS status Theorem for theBenchmark.p % 48.02/48.25 SZS output start Proof for theBenchmark.p % 48.02/48.25 Clause #0 (by assumption #[]): Eq % 48.02/48.25 (Not % 48.02/48.25 (∀ (A B C : Iota), % 48.02/48.25 m2_relset_1 C B A → % 48.02/48.25 And (Eq (k1_funct_5 C) (k10_relset_1 A B (k6_relset_1 B A C) A)) % 48.02/48.25 (Eq (k10_relset_1 A B (k6_relset_1 B A C) (k10_relset_1 B A C B)) % 48.02/48.25 (k10_relset_1 A B (k6_relset_1 B A C) (k2_funct_5 C))))) % 48.02/48.25 True % 48.02/48.25 Clause #32 (by assumption #[]): Eq (∀ (A B C : Iota), m1_relset_1 C A B → Eq (k6_relset_1 A B C) (k4_relat_1 C)) True % 48.02/48.25 Clause #33 (by assumption #[]): Eq (∀ (A B C : Iota), Iff (m2_relset_1 C A B) (m1_relset_1 C A B)) True % 48.02/48.25 Clause #37 (by assumption #[]): Eq % 48.02/48.25 (∀ (A B C : Iota), % 48.02/48.25 m2_relset_1 C B A → % 48.02/48.25 And (Eq (k1_funct_5 C) (k10_relset_1 A B (k6_relset_1 B A C) A)) (Eq (k2_funct_5 C) (k10_relset_1 B A C B))) % 48.02/48.25 True % 48.02/48.25 Clause #46 (by clausification #[0]): Eq % 48.02/48.25 (∀ (A B C : Iota), % 48.02/48.25 m2_relset_1 C B A → % 48.02/48.25 And (Eq (k1_funct_5 C) (k10_relset_1 A B (k6_relset_1 B A C) A)) % 48.02/48.25 (Eq (k10_relset_1 A B (k6_relset_1 B A C) (k10_relset_1 B A C B)) % 48.02/48.25 (k10_relset_1 A B (k6_relset_1 B A C) (k2_funct_5 C)))) % 48.02/48.25 False % 48.02/48.25 Clause #47 (by clausification #[46]): ∀ (a : Iota), % 48.02/48.25 Eq % 48.02/48.25 (Not % 48.02/48.25 (∀ (B C : Iota), % 48.02/48.25 m2_relset_1 C B (skS.0 0 a) → % 48.02/48.25 And (Eq (k1_funct_5 C) (k10_relset_1 (skS.0 0 a) B (k6_relset_1 B (skS.0 0 a) C) (skS.0 0 a))) % 48.02/48.25 (Eq (k10_relset_1 (skS.0 0 a) B (k6_relset_1 B (skS.0 0 a) C) (k10_relset_1 B (skS.0 0 a) C B)) % 48.02/48.25 (k10_relset_1 (skS.0 0 a) B (k6_relset_1 B (skS.0 0 a) C) (k2_funct_5 C))))) % 48.02/48.25 True % 48.02/48.25 Clause #48 (by clausification #[47]): ∀ (a : Iota), % 48.02/48.25 Eq % 48.02/48.25 (∀ (B C : Iota), % 48.02/48.25 m2_relset_1 C B (skS.0 0 a) → % 48.02/48.25 And (Eq (k1_funct_5 C) (k10_relset_1 (skS.0 0 a) B (k6_relset_1 B (skS.0 0 a) C) (skS.0 0 a))) % 48.02/48.25 (Eq (k10_relset_1 (skS.0 0 a) B (k6_relset_1 B (skS.0 0 a) C) (k10_relset_1 B (skS.0 0 a) C B)) % 48.02/48.25 (k10_relset_1 (skS.0 0 a) B (k6_relset_1 B (skS.0 0 a) C) (k2_funct_5 C)))) % 48.02/48.25 False % 48.02/48.25 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), % 48.02/48.25 Eq % 48.02/48.25 (Not % 48.02/48.25 (∀ (C : Iota), % 48.02/48.25 m2_relset_1 C (skS.0 1 a a_1) (skS.0 0 a) → % 48.02/48.25 And % 48.02/48.25 (Eq (k1_funct_5 C) % 48.02/48.25 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) C) (skS.0 0 a))) % 48.02/48.25 (Eq % 48.02/48.25 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) C) % 48.02/48.25 (k10_relset_1 (skS.0 1 a a_1) (skS.0 0 a) C (skS.0 1 a a_1))) % 48.02/48.25 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) C) (k2_funct_5 C))))) % 48.02/48.25 True % 48.02/48.25 Clause #50 (by clausification #[49]): ∀ (a a_1 : Iota), % 48.02/48.25 Eq % 48.02/48.25 (∀ (C : Iota), % 48.02/48.25 m2_relset_1 C (skS.0 1 a a_1) (skS.0 0 a) → % 48.02/48.25 And % 48.02/48.25 (Eq (k1_funct_5 C) % 48.02/48.25 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) C) (skS.0 0 a))) % 48.02/48.25 (Eq % 48.02/48.25 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) C) % 48.02/48.25 (k10_relset_1 (skS.0 1 a a_1) (skS.0 0 a) C (skS.0 1 a a_1))) % 48.02/48.25 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) C) (k2_funct_5 C)))) % 48.02/48.25 False % 48.02/48.25 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 : Iota), % 48.02/48.25 Eq % 48.02/48.25 (Not % 48.02/48.25 (m2_relset_1 (skS.0 2 a a_1 a_2) (skS.0 1 a a_1) (skS.0 0 a) → % 48.02/48.25 And % 48.02/48.25 (Eq (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.02/48.25 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.02/48.25 (skS.0 0 a))) % 48.02/48.25 (Eq % 48.02/48.25 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.02/48.25 (k10_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 1 a a_1))) % 48.02/48.25 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.02/48.25 (k2_funct_5 (skS.0 2 a a_1 a_2)))))) % 48.02/48.25 True % 48.02/48.25 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), % 48.02/48.25 Eq % 48.02/48.25 (m2_relset_1 (skS.0 2 a a_1 a_2) (skS.0 1 a a_1) (skS.0 0 a) → % 48.02/48.27 And % 48.02/48.27 (Eq (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.02/48.27 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.02/48.27 (skS.0 0 a))) % 48.02/48.27 (Eq % 48.02/48.27 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.02/48.27 (k10_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 1 a a_1))) % 48.02/48.27 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.02/48.27 (k2_funct_5 (skS.0 2 a a_1 a_2))))) % 48.02/48.27 False % 48.02/48.27 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 : Iota), Eq (m2_relset_1 (skS.0 2 a a_1 a_2) (skS.0 1 a a_1) (skS.0 0 a)) True % 48.02/48.27 Clause #54 (by clausification #[52]): ∀ (a a_1 a_2 : Iota), % 48.02/48.27 Eq % 48.02/48.27 (And % 48.02/48.27 (Eq (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.02/48.27 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.02/48.27 (skS.0 0 a))) % 48.02/48.27 (Eq % 48.02/48.27 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.02/48.27 (k10_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 1 a a_1))) % 48.02/48.27 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.02/48.27 (k2_funct_5 (skS.0 2 a a_1 a_2))))) % 48.02/48.27 False % 48.02/48.27 Clause #251 (by clausification #[32]): ∀ (a : Iota), Eq (∀ (B C : Iota), m1_relset_1 C a B → Eq (k6_relset_1 a B C) (k4_relat_1 C)) True % 48.02/48.27 Clause #252 (by clausification #[251]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), m1_relset_1 C a a_1 → Eq (k6_relset_1 a a_1 C) (k4_relat_1 C)) True % 48.02/48.27 Clause #253 (by clausification #[252]): ∀ (a a_1 a_2 : Iota), Eq (m1_relset_1 a a_1 a_2 → Eq (k6_relset_1 a_1 a_2 a) (k4_relat_1 a)) True % 48.02/48.27 Clause #254 (by clausification #[253]): ∀ (a a_1 a_2 : Iota), Or (Eq (m1_relset_1 a a_1 a_2) False) (Eq (Eq (k6_relset_1 a_1 a_2 a) (k4_relat_1 a)) True) % 48.02/48.27 Clause #255 (by clausification #[254]): ∀ (a a_1 a_2 : Iota), Or (Eq (m1_relset_1 a a_1 a_2) False) (Eq (k6_relset_1 a_1 a_2 a) (k4_relat_1 a)) % 48.02/48.27 Clause #270 (by clausification #[33]): ∀ (a : Iota), Eq (∀ (B C : Iota), Iff (m2_relset_1 C a B) (m1_relset_1 C a B)) True % 48.02/48.27 Clause #271 (by clausification #[270]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), Iff (m2_relset_1 C a a_1) (m1_relset_1 C a a_1)) True % 48.02/48.27 Clause #272 (by clausification #[271]): ∀ (a a_1 a_2 : Iota), Eq (Iff (m2_relset_1 a a_1 a_2) (m1_relset_1 a a_1 a_2)) True % 48.02/48.27 Clause #274 (by clausification #[272]): ∀ (a a_1 a_2 : Iota), Or (Eq (m2_relset_1 a a_1 a_2) False) (Eq (m1_relset_1 a a_1 a_2) True) % 48.02/48.27 Clause #276 (by superposition #[274, 53]): ∀ (a a_1 a_2 : Iota), Or (Eq (m1_relset_1 (skS.0 2 a a_1 a_2) (skS.0 1 a a_1) (skS.0 0 a)) True) (Eq False True) % 48.02/48.27 Clause #302 (by clausification #[37]): ∀ (a : Iota), % 48.02/48.27 Eq % 48.02/48.27 (∀ (B C : Iota), % 48.02/48.27 m2_relset_1 C B a → % 48.02/48.27 And (Eq (k1_funct_5 C) (k10_relset_1 a B (k6_relset_1 B a C) a)) (Eq (k2_funct_5 C) (k10_relset_1 B a C B))) % 48.02/48.27 True % 48.02/48.27 Clause #303 (by clausification #[302]): ∀ (a a_1 : Iota), % 48.02/48.27 Eq % 48.02/48.27 (∀ (C : Iota), % 48.02/48.27 m2_relset_1 C a a_1 → % 48.02/48.27 And (Eq (k1_funct_5 C) (k10_relset_1 a_1 a (k6_relset_1 a a_1 C) a_1)) % 48.02/48.27 (Eq (k2_funct_5 C) (k10_relset_1 a a_1 C a))) % 48.02/48.27 True % 48.02/48.27 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 : Iota), % 48.02/48.27 Eq % 48.02/48.27 (m2_relset_1 a a_1 a_2 → % 48.02/48.27 And (Eq (k1_funct_5 a) (k10_relset_1 a_2 a_1 (k6_relset_1 a_1 a_2 a) a_2)) % 48.02/48.27 (Eq (k2_funct_5 a) (k10_relset_1 a_1 a_2 a a_1))) % 48.02/48.27 True % 48.02/48.27 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 : Iota), % 48.02/48.27 Or (Eq (m2_relset_1 a a_1 a_2) False) % 48.02/48.27 (Eq % 48.02/48.27 (And (Eq (k1_funct_5 a) (k10_relset_1 a_2 a_1 (k6_relset_1 a_1 a_2 a) a_2)) % 48.02/48.27 (Eq (k2_funct_5 a) (k10_relset_1 a_1 a_2 a a_1))) % 48.02/48.27 True) % 48.02/48.27 Clause #306 (by clausification #[305]): ∀ (a a_1 a_2 : Iota), Or (Eq (m2_relset_1 a a_1 a_2) False) (Eq (Eq (k2_funct_5 a) (k10_relset_1 a_1 a_2 a a_1)) True) % 48.02/48.27 Clause #307 (by clausification #[305]): ∀ (a a_1 a_2 : Iota), % 48.02/48.27 Or (Eq (m2_relset_1 a a_1 a_2) False) (Eq (Eq (k1_funct_5 a) (k10_relset_1 a_2 a_1 (k6_relset_1 a_1 a_2 a) a_2)) True) % 48.12/48.29 Clause #308 (by clausification #[306]): ∀ (a a_1 a_2 : Iota), Or (Eq (m2_relset_1 a a_1 a_2) False) (Eq (k2_funct_5 a) (k10_relset_1 a_1 a_2 a a_1)) % 48.12/48.29 Clause #309 (by superposition #[308, 53]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Or % 48.12/48.29 (Eq (k2_funct_5 (skS.0 2 a a_1 a_2)) (k10_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 1 a a_1))) % 48.12/48.29 (Eq False True) % 48.12/48.29 Clause #318 (by clausification #[54]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Or % 48.12/48.29 (Eq % 48.12/48.29 (Eq (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.12/48.29 (skS.0 0 a))) % 48.12/48.29 False) % 48.12/48.29 (Eq % 48.12/48.29 (Eq % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k10_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 1 a a_1))) % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k2_funct_5 (skS.0 2 a a_1 a_2)))) % 48.12/48.29 False) % 48.12/48.29 Clause #319 (by clausification #[318]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Or % 48.12/48.29 (Eq % 48.12/48.29 (Eq % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k10_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 1 a a_1))) % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k2_funct_5 (skS.0 2 a a_1 a_2)))) % 48.12/48.29 False) % 48.12/48.29 (Ne (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.12/48.29 (skS.0 0 a))) % 48.12/48.29 Clause #320 (by clausification #[319]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Or % 48.12/48.29 (Ne (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.12/48.29 (skS.0 0 a))) % 48.12/48.29 (Ne % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k10_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 1 a a_1))) % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k2_funct_5 (skS.0 2 a a_1 a_2)))) % 48.12/48.29 Clause #486 (by clausification #[307]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Or (Eq (m2_relset_1 a a_1 a_2) False) (Eq (k1_funct_5 a) (k10_relset_1 a_2 a_1 (k6_relset_1 a_1 a_2 a) a_2)) % 48.12/48.29 Clause #487 (by superposition #[486, 53]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Or % 48.12/48.29 (Eq (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 48.12/48.29 (skS.0 0 a))) % 48.12/48.29 (Eq False True) % 48.12/48.29 Clause #519 (by clausification #[276]): ∀ (a a_1 a_2 : Iota), Eq (m1_relset_1 (skS.0 2 a a_1 a_2) (skS.0 1 a a_1) (skS.0 0 a)) True % 48.12/48.29 Clause #522 (by superposition #[519, 255]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Or (Eq True False) (Eq (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) (k4_relat_1 (skS.0 2 a a_1 a_2))) % 48.12/48.29 Clause #571 (by clausification #[309]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Eq (k2_funct_5 (skS.0 2 a a_1 a_2)) (k10_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 1 a a_1)) % 48.12/48.29 Clause #573 (by backward positive simplify reflect #[571, 320]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Ne (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) (skS.0 0 a)) % 48.12/48.29 Clause #1063 (by clausification #[487]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Eq (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) (skS.0 0 a)) % 48.12/48.29 Clause #1218 (by clausification #[522]): ∀ (a a_1 a_2 : Iota), Eq (k6_relset_1 (skS.0 1 a a_1) (skS.0 0 a) (skS.0 2 a a_1 a_2)) (k4_relat_1 (skS.0 2 a a_1 a_2)) % 48.12/48.29 Clause #1219 (by backward demodulation #[1218, 1063]): ∀ (a a_1 a_2 : Iota), % 48.12/48.29 Eq (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.12/48.29 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k4_relat_1 (skS.0 2 a a_1 a_2)) (skS.0 0 a)) % 48.12/48.30 Clause #1374 (by forward demodulation #[573, 1218]): ∀ (a a_1 a_2 : Iota), % 48.12/48.30 Ne (k1_funct_5 (skS.0 2 a a_1 a_2)) % 48.12/48.30 (k10_relset_1 (skS.0 0 a) (skS.0 1 a a_1) (k4_relat_1 (skS.0 2 a a_1 a_2)) (skS.0 0 a)) % 48.12/48.30 Clause #2668 (by forward contextual literal cutting #[1219, 1374]): False % 48.12/48.30 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------