%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU284+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n006.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:18 PM UTC 2025 % Result : Theorem 15.23s 15.39s % Output : Proof 15.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU284+1 : TPTP v9.2.0. Released v3.3.0. % 0.11/0.13 % Command : duper %s % 0.14/0.34 % Computer : n006.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 04:08:38 EDT 2025 % 0.14/0.34 % CPUTime : % 15.23/15.39 SZS status Theorem for theBenchmark.p % 15.23/15.39 SZS output start Proof for theBenchmark.p % 15.23/15.39 Clause #0 (by assumption #[]): Eq % 15.23/15.39 (Not % 15.23/15.39 (∀ (A : Iota), % 15.23/15.39 Exists fun B => % 15.23/15.39 And (And (And (relation B) (function B)) (Eq (relation_dom B) A)) % 15.23/15.39 (∀ (C : Iota), in C A → Eq (apply B C) (singleton C)))) % 15.23/15.39 True % 15.23/15.39 Clause #4 (by assumption #[]): Eq % 15.23/15.39 (∀ (A : Iota), % 15.23/15.39 And (∀ (B C D : Iota), And (And (in B A) (Eq C (singleton B))) (Eq D (singleton B)) → Eq C D) % 15.23/15.39 (∀ (B : Iota), Not (And (in B A) (∀ (C : Iota), Ne C (singleton B)))) → % 15.23/15.39 Exists fun B => % 15.23/15.39 And (And (And (relation B) (function B)) (Eq (relation_dom B) A)) % 15.23/15.39 (∀ (C : Iota), in C A → Eq (apply B C) (singleton C))) % 15.23/15.39 True % 15.23/15.39 Clause #30 (by clausification #[0]): Eq % 15.23/15.39 (∀ (A : Iota), % 15.23/15.39 Exists fun B => % 15.23/15.39 And (And (And (relation B) (function B)) (Eq (relation_dom B) A)) % 15.23/15.39 (∀ (C : Iota), in C A → Eq (apply B C) (singleton C))) % 15.23/15.39 False % 15.23/15.39 Clause #31 (by clausification #[30]): ∀ (a : Iota), % 15.23/15.39 Eq % 15.23/15.39 (Not % 15.23/15.39 (Exists fun B => % 15.23/15.39 And (And (And (relation B) (function B)) (Eq (relation_dom B) (skS.0 0 a))) % 15.23/15.39 (∀ (C : Iota), in C (skS.0 0 a) → Eq (apply B C) (singleton C)))) % 15.23/15.39 True % 15.23/15.39 Clause #32 (by clausification #[31]): ∀ (a : Iota), % 15.23/15.39 Eq % 15.23/15.39 (Exists fun B => % 15.23/15.39 And (And (And (relation B) (function B)) (Eq (relation_dom B) (skS.0 0 a))) % 15.23/15.39 (∀ (C : Iota), in C (skS.0 0 a) → Eq (apply B C) (singleton C))) % 15.23/15.39 False % 15.23/15.39 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), % 15.23/15.39 Eq % 15.23/15.39 (And (And (And (relation a) (function a)) (Eq (relation_dom a) (skS.0 0 a_1))) % 15.23/15.39 (∀ (C : Iota), in C (skS.0 0 a_1) → Eq (apply a C) (singleton C))) % 15.23/15.39 False % 15.23/15.39 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), % 15.23/15.39 Or (Eq (And (And (relation a) (function a)) (Eq (relation_dom a) (skS.0 0 a_1))) False) % 15.23/15.39 (Eq (∀ (C : Iota), in C (skS.0 0 a_1) → Eq (apply a C) (singleton C)) False) % 15.23/15.39 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), % 15.23/15.39 Or (Eq (∀ (C : Iota), in C (skS.0 0 a) → Eq (apply a_1 C) (singleton C)) False) % 15.23/15.39 (Or (Eq (And (relation a_1) (function a_1)) False) (Eq (Eq (relation_dom a_1) (skS.0 0 a)) False)) % 15.23/15.39 Clause #36 (by clausification #[35]): ∀ (a a_1 a_2 : Iota), % 15.23/15.39 Or (Eq (And (relation a) (function a)) False) % 15.23/15.39 (Or (Eq (Eq (relation_dom a) (skS.0 0 a_1)) False) % 15.23/15.39 (Eq % 15.23/15.39 (Not (in (skS.0 1 a_1 a a_2) (skS.0 0 a_1) → Eq (apply a (skS.0 1 a_1 a a_2)) (singleton (skS.0 1 a_1 a a_2)))) % 15.23/15.39 True)) % 15.23/15.39 Clause #37 (by clausification #[36]): ∀ (a a_1 a_2 : Iota), % 15.23/15.39 Or (Eq (Eq (relation_dom a) (skS.0 0 a_1)) False) % 15.23/15.39 (Or % 15.23/15.39 (Eq % 15.23/15.39 (Not (in (skS.0 1 a_1 a a_2) (skS.0 0 a_1) → Eq (apply a (skS.0 1 a_1 a a_2)) (singleton (skS.0 1 a_1 a a_2)))) % 15.23/15.39 True) % 15.23/15.39 (Or (Eq (relation a) False) (Eq (function a) False))) % 15.23/15.39 Clause #38 (by clausification #[37]): ∀ (a a_1 a_2 : Iota), % 15.23/15.39 Or % 15.23/15.39 (Eq (Not (in (skS.0 1 a a_1 a_2) (skS.0 0 a) → Eq (apply a_1 (skS.0 1 a a_1 a_2)) (singleton (skS.0 1 a a_1 a_2)))) % 15.23/15.39 True) % 15.23/15.39 (Or (Eq (relation a_1) False) (Or (Eq (function a_1) False) (Ne (relation_dom a_1) (skS.0 0 a)))) % 15.23/15.39 Clause #39 (by clausification #[38]): ∀ (a a_1 a_2 : Iota), % 15.23/15.39 Or (Eq (relation a) False) % 15.23/15.39 (Or (Eq (function a) False) % 15.23/15.39 (Or (Ne (relation_dom a) (skS.0 0 a_1)) % 15.23/15.39 (Eq (in (skS.0 1 a_1 a a_2) (skS.0 0 a_1) → Eq (apply a (skS.0 1 a_1 a a_2)) (singleton (skS.0 1 a_1 a a_2))) % 15.23/15.39 False))) % 15.23/15.39 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 15.23/15.39 Or (Eq (relation a) False) % 15.23/15.39 (Or (Eq (function a) False) % 15.23/15.39 (Or (Ne (relation_dom a) (skS.0 0 a_1)) (Eq (in (skS.0 1 a_1 a a_2) (skS.0 0 a_1)) True))) % 15.23/15.39 Clause #41 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 15.23/15.39 Or (Eq (relation a) False) % 15.23/15.39 (Or (Eq (function a) False) % 15.23/15.39 (Or (Ne (relation_dom a) (skS.0 0 a_1)) % 15.23/15.39 (Eq (Eq (apply a (skS.0 1 a_1 a a_2)) (singleton (skS.0 1 a_1 a a_2))) False))) % 15.23/15.39 Clause #74 (by clausification #[4]): ∀ (a : Iota), % 15.23/15.39 Eq % 15.23/15.39 (And (∀ (B C D : Iota), And (And (in B a) (Eq C (singleton B))) (Eq D (singleton B)) → Eq C D) % 15.23/15.39 (∀ (B : Iota), Not (And (in B a) (∀ (C : Iota), Ne C (singleton B)))) → % 15.26/15.42 Exists fun B => % 15.26/15.42 And (And (And (relation B) (function B)) (Eq (relation_dom B) a)) % 15.26/15.42 (∀ (C : Iota), in C a → Eq (apply B C) (singleton C))) % 15.26/15.42 True % 15.26/15.42 Clause #75 (by clausification #[74]): ∀ (a : Iota), % 15.26/15.42 Or % 15.26/15.42 (Eq % 15.26/15.42 (And (∀ (B C D : Iota), And (And (in B a) (Eq C (singleton B))) (Eq D (singleton B)) → Eq C D) % 15.26/15.42 (∀ (B : Iota), Not (And (in B a) (∀ (C : Iota), Ne C (singleton B))))) % 15.26/15.42 False) % 15.26/15.42 (Eq % 15.26/15.42 (Exists fun B => % 15.26/15.42 And (And (And (relation B) (function B)) (Eq (relation_dom B) a)) % 15.26/15.42 (∀ (C : Iota), in C a → Eq (apply B C) (singleton C))) % 15.26/15.42 True) % 15.26/15.42 Clause #76 (by clausification #[75]): ∀ (a : Iota), % 15.26/15.42 Or % 15.26/15.42 (Eq % 15.26/15.42 (Exists fun B => % 15.26/15.42 And (And (And (relation B) (function B)) (Eq (relation_dom B) a)) % 15.26/15.42 (∀ (C : Iota), in C a → Eq (apply B C) (singleton C))) % 15.26/15.42 True) % 15.26/15.42 (Or (Eq (∀ (B C D : Iota), And (And (in B a) (Eq C (singleton B))) (Eq D (singleton B)) → Eq C D) False) % 15.26/15.42 (Eq (∀ (B : Iota), Not (And (in B a) (∀ (C : Iota), Ne C (singleton B)))) False)) % 15.26/15.42 Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota), % 15.26/15.42 Or (Eq (∀ (B C D : Iota), And (And (in B a) (Eq C (singleton B))) (Eq D (singleton B)) → Eq C D) False) % 15.26/15.42 (Or (Eq (∀ (B : Iota), Not (And (in B a) (∀ (C : Iota), Ne C (singleton B)))) False) % 15.26/15.42 (Eq % 15.26/15.42 (And (And (And (relation (skS.0 6 a a_1)) (function (skS.0 6 a a_1))) (Eq (relation_dom (skS.0 6 a a_1)) a)) % 15.26/15.42 (∀ (C : Iota), in C a → Eq (apply (skS.0 6 a a_1) C) (singleton C))) % 15.26/15.42 True)) % 15.26/15.42 Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 : Iota), % 15.26/15.42 Or (Eq (∀ (B : Iota), Not (And (in B a) (∀ (C : Iota), Ne C (singleton B)))) False) % 15.26/15.42 (Or % 15.26/15.42 (Eq % 15.26/15.42 (And (And (And (relation (skS.0 6 a a_1)) (function (skS.0 6 a a_1))) (Eq (relation_dom (skS.0 6 a a_1)) a)) % 15.26/15.42 (∀ (C : Iota), in C a → Eq (apply (skS.0 6 a a_1) C) (singleton C))) % 15.26/15.42 True) % 15.26/15.42 (Eq % 15.26/15.42 (Not % 15.26/15.42 (∀ (C D : Iota), % 15.26/15.42 And (And (in (skS.0 7 a a_2) a) (Eq C (singleton (skS.0 7 a a_2)))) (Eq D (singleton (skS.0 7 a a_2))) → % 15.26/15.42 Eq C D)) % 15.26/15.42 True)) % 15.26/15.42 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 a_3 : Iota), % 15.26/15.42 Or % 15.26/15.42 (Eq % 15.26/15.42 (And (And (And (relation (skS.0 6 a a_1)) (function (skS.0 6 a a_1))) (Eq (relation_dom (skS.0 6 a a_1)) a)) % 15.26/15.42 (∀ (C : Iota), in C a → Eq (apply (skS.0 6 a a_1) C) (singleton C))) % 15.26/15.42 True) % 15.26/15.42 (Or % 15.26/15.42 (Eq % 15.26/15.42 (Not % 15.26/15.42 (∀ (C D : Iota), % 15.26/15.42 And (And (in (skS.0 7 a a_2) a) (Eq C (singleton (skS.0 7 a a_2)))) (Eq D (singleton (skS.0 7 a a_2))) → % 15.26/15.42 Eq C D)) % 15.26/15.42 True) % 15.26/15.42 (Eq (Not (Not (And (in (skS.0 8 a a_3) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_3)))))) True)) % 15.26/15.42 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 a_3 : Iota), % 15.26/15.42 Or % 15.26/15.42 (Eq % 15.26/15.42 (Not % 15.26/15.42 (∀ (C D : Iota), % 15.26/15.42 And (And (in (skS.0 7 a a_1) a) (Eq C (singleton (skS.0 7 a a_1)))) (Eq D (singleton (skS.0 7 a a_1))) → % 15.26/15.42 Eq C D)) % 15.26/15.42 True) % 15.26/15.42 (Or (Eq (Not (Not (And (in (skS.0 8 a a_2) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_2)))))) True) % 15.26/15.42 (Eq (∀ (C : Iota), in C a → Eq (apply (skS.0 6 a a_3) C) (singleton C)) True)) % 15.26/15.42 Clause #81 (by clausification #[79]): ∀ (a a_1 a_2 a_3 : Iota), % 15.26/15.42 Or % 15.26/15.42 (Eq % 15.26/15.42 (Not % 15.26/15.42 (∀ (C D : Iota), % 15.26/15.42 And (And (in (skS.0 7 a a_1) a) (Eq C (singleton (skS.0 7 a a_1)))) (Eq D (singleton (skS.0 7 a a_1))) → % 15.26/15.42 Eq C D)) % 15.26/15.42 True) % 15.26/15.42 (Or (Eq (Not (Not (And (in (skS.0 8 a a_2) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_2)))))) True) % 15.26/15.42 (Eq (And (And (relation (skS.0 6 a a_3)) (function (skS.0 6 a a_3))) (Eq (relation_dom (skS.0 6 a a_3)) a)) True)) % 15.26/15.42 Clause #82 (by clausification #[80]): ∀ (a a_1 a_2 a_3 : Iota), % 15.26/15.42 Or (Eq (Not (Not (And (in (skS.0 8 a a_1) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_1)))))) True) % 15.26/15.42 (Or (Eq (∀ (C : Iota), in C a → Eq (apply (skS.0 6 a a_2) C) (singleton C)) True) % 15.26/15.42 (Eq % 15.26/15.42 (∀ (C D : Iota), % 15.26/15.42 And (And (in (skS.0 7 a a_3) a) (Eq C (singleton (skS.0 7 a a_3)))) (Eq D (singleton (skS.0 7 a a_3))) → % 15.28/15.44 Eq C D) % 15.28/15.44 False)) % 15.28/15.44 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : Iota), % 15.28/15.44 Or (Eq (∀ (C : Iota), in C a → Eq (apply (skS.0 6 a a_1) C) (singleton C)) True) % 15.28/15.44 (Or % 15.28/15.44 (Eq % 15.28/15.44 (∀ (C D : Iota), % 15.28/15.44 And (And (in (skS.0 7 a a_2) a) (Eq C (singleton (skS.0 7 a a_2)))) (Eq D (singleton (skS.0 7 a a_2))) → % 15.28/15.44 Eq C D) % 15.28/15.44 False) % 15.28/15.44 (Eq (Not (And (in (skS.0 8 a a_3) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_3))))) False)) % 15.28/15.44 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.28/15.44 Or % 15.28/15.44 (Eq % 15.28/15.44 (∀ (C D : Iota), % 15.28/15.44 And (And (in (skS.0 7 a a_1) a) (Eq C (singleton (skS.0 7 a a_1)))) (Eq D (singleton (skS.0 7 a a_1))) → Eq C D) % 15.28/15.44 False) % 15.28/15.44 (Or (Eq (Not (And (in (skS.0 8 a a_2) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_2))))) False) % 15.28/15.44 (Eq (in a_3 a → Eq (apply (skS.0 6 a a_4) a_3) (singleton a_3)) True)) % 15.28/15.44 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.28/15.44 Or (Eq (Not (And (in (skS.0 8 a a_1) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_1))))) False) % 15.28/15.44 (Or (Eq (in a_2 a → Eq (apply (skS.0 6 a a_3) a_2) (singleton a_2)) True) % 15.28/15.44 (Eq % 15.28/15.44 (Not % 15.28/15.44 (∀ (D : Iota), % 15.28/15.44 And (And (in (skS.0 7 a a_4) a) (Eq (skS.0 9 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.28/15.44 (Eq D (singleton (skS.0 7 a a_4))) → % 15.28/15.44 Eq (skS.0 9 a a_4 a_5) D)) % 15.28/15.44 True)) % 15.28/15.44 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.28/15.44 Or (Eq (in a a_1 → Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) True) % 15.28/15.44 (Or % 15.28/15.44 (Eq % 15.28/15.44 (Not % 15.28/15.44 (∀ (D : Iota), % 15.28/15.44 And (And (in (skS.0 7 a_1 a_3) a_1) (Eq (skS.0 9 a_1 a_3 a_4) (singleton (skS.0 7 a_1 a_3)))) % 15.28/15.44 (Eq D (singleton (skS.0 7 a_1 a_3))) → % 15.28/15.44 Eq (skS.0 9 a_1 a_3 a_4) D)) % 15.28/15.44 True) % 15.28/15.44 (Eq (And (in (skS.0 8 a_1 a_5) a_1) (∀ (C : Iota), Ne C (singleton (skS.0 8 a_1 a_5)))) True)) % 15.28/15.44 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.28/15.44 Or % 15.28/15.44 (Eq % 15.28/15.44 (Not % 15.28/15.44 (∀ (D : Iota), % 15.28/15.44 And (And (in (skS.0 7 a a_1) a) (Eq (skS.0 9 a a_1 a_2) (singleton (skS.0 7 a a_1)))) % 15.28/15.44 (Eq D (singleton (skS.0 7 a a_1))) → % 15.28/15.44 Eq (skS.0 9 a a_1 a_2) D)) % 15.28/15.44 True) % 15.28/15.44 (Or (Eq (And (in (skS.0 8 a a_3) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_3)))) True) % 15.28/15.44 (Or (Eq (in a_4 a) False) (Eq (Eq (apply (skS.0 6 a a_5) a_4) (singleton a_4)) True))) % 15.28/15.44 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.28/15.44 Or (Eq (And (in (skS.0 8 a a_1) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_1)))) True) % 15.28/15.44 (Or (Eq (in a_2 a) False) % 15.28/15.44 (Or (Eq (Eq (apply (skS.0 6 a a_3) a_2) (singleton a_2)) True) % 15.28/15.44 (Eq % 15.28/15.44 (∀ (D : Iota), % 15.28/15.44 And (And (in (skS.0 7 a a_4) a) (Eq (skS.0 9 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.28/15.44 (Eq D (singleton (skS.0 7 a a_4))) → % 15.28/15.44 Eq (skS.0 9 a a_4 a_5) D) % 15.28/15.44 False))) % 15.28/15.44 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.28/15.44 Or (Eq (in a a_1) False) % 15.28/15.44 (Or (Eq (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) True) % 15.28/15.44 (Or % 15.28/15.44 (Eq % 15.28/15.44 (∀ (D : Iota), % 15.28/15.44 And (And (in (skS.0 7 a_1 a_3) a_1) (Eq (skS.0 9 a_1 a_3 a_4) (singleton (skS.0 7 a_1 a_3)))) % 15.28/15.44 (Eq D (singleton (skS.0 7 a_1 a_3))) → % 15.28/15.44 Eq (skS.0 9 a_1 a_3 a_4) D) % 15.28/15.44 False) % 15.28/15.44 (Eq (∀ (C : Iota), Ne C (singleton (skS.0 8 a_1 a_5))) True))) % 15.28/15.44 Clause #91 (by clausification #[89]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.28/15.44 Or (Eq (in a a_1) False) % 15.28/15.44 (Or % 15.28/15.44 (Eq % 15.28/15.44 (∀ (D : Iota), % 15.28/15.44 And (And (in (skS.0 7 a_1 a_2) a_1) (Eq (skS.0 9 a_1 a_2 a_3) (singleton (skS.0 7 a_1 a_2)))) % 15.28/15.44 (Eq D (singleton (skS.0 7 a_1 a_2))) → % 15.28/15.44 Eq (skS.0 9 a_1 a_2 a_3) D) % 15.28/15.44 False) % 15.28/15.44 (Or (Eq (∀ (C : Iota), Ne C (singleton (skS.0 8 a_1 a_4))) True) (Eq (apply (skS.0 6 a_1 a_5) a) (singleton a)))) % 15.28/15.47 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.28/15.47 Or (Eq (in a a_1) False) % 15.28/15.47 (Or (Eq (∀ (C : Iota), Ne C (singleton (skS.0 8 a_1 a_2))) True) % 15.28/15.47 (Or (Eq (apply (skS.0 6 a_1 a_3) a) (singleton a)) % 15.28/15.47 (Eq % 15.28/15.47 (Not % 15.28/15.47 (And (And (in (skS.0 7 a_1 a_4) a_1) (Eq (skS.0 9 a_1 a_4 a_5) (singleton (skS.0 7 a_1 a_4)))) % 15.28/15.47 (Eq (skS.0 10 a_1 a_4 a_5 a_6) (singleton (skS.0 7 a_1 a_4))) → % 15.28/15.47 Eq (skS.0 9 a_1 a_4 a_5) (skS.0 10 a_1 a_4 a_5 a_6))) % 15.28/15.47 True))) % 15.28/15.47 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.28/15.47 Or (Eq (in a a_1) False) % 15.28/15.47 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.28/15.47 (Or % 15.28/15.47 (Eq % 15.28/15.47 (Not % 15.28/15.47 (And (And (in (skS.0 7 a_1 a_3) a_1) (Eq (skS.0 9 a_1 a_3 a_4) (singleton (skS.0 7 a_1 a_3)))) % 15.28/15.47 (Eq (skS.0 10 a_1 a_3 a_4 a_5) (singleton (skS.0 7 a_1 a_3))) → % 15.28/15.47 Eq (skS.0 9 a_1 a_3 a_4) (skS.0 10 a_1 a_3 a_4 a_5))) % 15.28/15.47 True) % 15.28/15.47 (Eq (Ne a_6 (singleton (skS.0 8 a_1 a_7))) True))) % 15.28/15.47 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.28/15.47 Or (Eq (in a a_1) False) % 15.28/15.47 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.28/15.47 (Or (Eq (Ne a_3 (singleton (skS.0 8 a_1 a_4))) True) % 15.28/15.47 (Eq % 15.28/15.47 (And (And (in (skS.0 7 a_1 a_5) a_1) (Eq (skS.0 9 a_1 a_5 a_6) (singleton (skS.0 7 a_1 a_5)))) % 15.28/15.47 (Eq (skS.0 10 a_1 a_5 a_6 a_7) (singleton (skS.0 7 a_1 a_5))) → % 15.28/15.47 Eq (skS.0 9 a_1 a_5 a_6) (skS.0 10 a_1 a_5 a_6 a_7)) % 15.28/15.47 False))) % 15.28/15.47 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.28/15.47 Or (Eq (in a a_1) False) % 15.28/15.47 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.28/15.47 (Or % 15.28/15.47 (Eq % 15.28/15.47 (And (And (in (skS.0 7 a_1 a_3) a_1) (Eq (skS.0 9 a_1 a_3 a_4) (singleton (skS.0 7 a_1 a_3)))) % 15.28/15.47 (Eq (skS.0 10 a_1 a_3 a_4 a_5) (singleton (skS.0 7 a_1 a_3))) → % 15.28/15.47 Eq (skS.0 9 a_1 a_3 a_4) (skS.0 10 a_1 a_3 a_4 a_5)) % 15.28/15.47 False) % 15.28/15.47 (Ne a_6 (singleton (skS.0 8 a_1 a_7))))) % 15.28/15.47 Clause #96 (by clausification #[95]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.28/15.47 Or (Eq (in a a_1) False) % 15.28/15.47 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.28/15.47 (Or (Ne a_3 (singleton (skS.0 8 a_1 a_4))) % 15.28/15.47 (Eq % 15.28/15.47 (And (And (in (skS.0 7 a_1 a_5) a_1) (Eq (skS.0 9 a_1 a_5 a_6) (singleton (skS.0 7 a_1 a_5)))) % 15.28/15.47 (Eq (skS.0 10 a_1 a_5 a_6 a_7) (singleton (skS.0 7 a_1 a_5)))) % 15.28/15.47 True))) % 15.28/15.47 Clause #97 (by clausification #[95]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.28/15.47 Or (Eq (in a a_1) False) % 15.28/15.47 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.28/15.47 (Or (Ne a_3 (singleton (skS.0 8 a_1 a_4))) (Eq (Eq (skS.0 9 a_1 a_5 a_6) (skS.0 10 a_1 a_5 a_6 a_7)) False))) % 15.28/15.47 Clause #98 (by clausification #[96]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.28/15.47 Or (Eq (in a a_1) False) % 15.28/15.47 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.28/15.47 (Or (Ne a_3 (singleton (skS.0 8 a_1 a_4))) % 15.28/15.47 (Eq (Eq (skS.0 10 a_1 a_5 a_6 a_7) (singleton (skS.0 7 a_1 a_5))) True))) % 15.28/15.47 Clause #99 (by clausification #[96]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.28/15.47 Or (Eq (in a a_1) False) % 15.28/15.47 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.28/15.47 (Or (Ne a_3 (singleton (skS.0 8 a_1 a_4))) % 15.28/15.47 (Eq (And (in (skS.0 7 a_1 a_5) a_1) (Eq (skS.0 9 a_1 a_5 a_6) (singleton (skS.0 7 a_1 a_5)))) True))) % 15.28/15.47 Clause #100 (by clausification #[98]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.28/15.47 Or (Eq (in a a_1) False) % 15.28/15.47 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.28/15.47 (Or (Ne a_3 (singleton (skS.0 8 a_1 a_4))) (Eq (skS.0 10 a_1 a_5 a_6 a_7) (singleton (skS.0 7 a_1 a_5))))) % 15.28/15.47 Clause #101 (by destructive equality resolution #[100]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.28/15.47 Or (Eq (in a a_1) False) % 15.28/15.47 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) (Eq (skS.0 10 a_1 a_3 a_4 a_5) (singleton (skS.0 7 a_1 a_3)))) % 15.28/15.47 Clause #168 (by clausification #[41]): ∀ (a a_1 a_2 : Iota), % 15.28/15.47 Or (Eq (relation a) False) % 15.28/15.47 (Or (Eq (function a) False) % 15.28/15.47 (Or (Ne (relation_dom a) (skS.0 0 a_1)) (Ne (apply a (skS.0 1 a_1 a a_2)) (singleton (skS.0 1 a_1 a a_2))))) % 15.28/15.50 Clause #204 (by clausification #[81]): ∀ (a a_1 a_2 a_3 : Iota), % 15.28/15.50 Or (Eq (Not (Not (And (in (skS.0 8 a a_1) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_1)))))) True) % 15.28/15.50 (Or % 15.28/15.50 (Eq (And (And (relation (skS.0 6 a a_2)) (function (skS.0 6 a a_2))) (Eq (relation_dom (skS.0 6 a a_2)) a)) True) % 15.28/15.50 (Eq % 15.28/15.50 (∀ (C D : Iota), % 15.28/15.50 And (And (in (skS.0 7 a a_3) a) (Eq C (singleton (skS.0 7 a a_3)))) (Eq D (singleton (skS.0 7 a a_3))) → % 15.28/15.50 Eq C D) % 15.28/15.50 False)) % 15.28/15.50 Clause #205 (by clausification #[204]): ∀ (a a_1 a_2 a_3 : Iota), % 15.28/15.50 Or (Eq (And (And (relation (skS.0 6 a a_1)) (function (skS.0 6 a a_1))) (Eq (relation_dom (skS.0 6 a a_1)) a)) True) % 15.28/15.50 (Or % 15.28/15.50 (Eq % 15.28/15.50 (∀ (C D : Iota), % 15.28/15.50 And (And (in (skS.0 7 a a_2) a) (Eq C (singleton (skS.0 7 a a_2)))) (Eq D (singleton (skS.0 7 a a_2))) → % 15.28/15.50 Eq C D) % 15.28/15.50 False) % 15.28/15.50 (Eq (Not (And (in (skS.0 8 a a_3) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_3))))) False)) % 15.28/15.50 Clause #206 (by clausification #[205]): ∀ (a a_1 a_2 a_3 : Iota), % 15.28/15.50 Or % 15.28/15.50 (Eq % 15.28/15.50 (∀ (C D : Iota), % 15.28/15.50 And (And (in (skS.0 7 a a_1) a) (Eq C (singleton (skS.0 7 a a_1)))) (Eq D (singleton (skS.0 7 a a_1))) → Eq C D) % 15.28/15.50 False) % 15.28/15.50 (Or (Eq (Not (And (in (skS.0 8 a a_2) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_2))))) False) % 15.28/15.50 (Eq (Eq (relation_dom (skS.0 6 a a_3)) a) True)) % 15.28/15.50 Clause #207 (by clausification #[205]): ∀ (a a_1 a_2 a_3 : Iota), % 15.28/15.50 Or % 15.28/15.50 (Eq % 15.28/15.50 (∀ (C D : Iota), % 15.28/15.50 And (And (in (skS.0 7 a a_1) a) (Eq C (singleton (skS.0 7 a a_1)))) (Eq D (singleton (skS.0 7 a a_1))) → Eq C D) % 15.28/15.50 False) % 15.28/15.50 (Or (Eq (Not (And (in (skS.0 8 a a_2) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_2))))) False) % 15.28/15.50 (Eq (And (relation (skS.0 6 a a_3)) (function (skS.0 6 a a_3))) True)) % 15.28/15.50 Clause #208 (by clausification #[206]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.28/15.50 Or (Eq (Not (And (in (skS.0 8 a a_1) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_1))))) False) % 15.28/15.50 (Or (Eq (Eq (relation_dom (skS.0 6 a a_2)) a) True) % 15.28/15.50 (Eq % 15.28/15.50 (Not % 15.28/15.50 (∀ (D : Iota), % 15.28/15.50 And (And (in (skS.0 7 a a_3) a) (Eq (skS.0 14 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.28/15.50 (Eq D (singleton (skS.0 7 a a_3))) → % 15.28/15.50 Eq (skS.0 14 a a_3 a_4) D)) % 15.28/15.50 True)) % 15.28/15.50 Clause #209 (by clausification #[208]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.28/15.50 Or (Eq (Eq (relation_dom (skS.0 6 a a_1)) a) True) % 15.28/15.50 (Or % 15.28/15.50 (Eq % 15.28/15.50 (Not % 15.28/15.50 (∀ (D : Iota), % 15.28/15.50 And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 14 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.28/15.50 (Eq D (singleton (skS.0 7 a a_2))) → % 15.28/15.50 Eq (skS.0 14 a a_2 a_3) D)) % 15.28/15.50 True) % 15.28/15.50 (Eq (And (in (skS.0 8 a a_4) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_4)))) True)) % 15.28/15.50 Clause #210 (by clausification #[209]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.28/15.50 Or % 15.28/15.50 (Eq % 15.28/15.50 (Not % 15.28/15.50 (∀ (D : Iota), % 15.28/15.50 And (And (in (skS.0 7 a a_1) a) (Eq (skS.0 14 a a_1 a_2) (singleton (skS.0 7 a a_1)))) % 15.28/15.50 (Eq D (singleton (skS.0 7 a a_1))) → % 15.28/15.50 Eq (skS.0 14 a a_1 a_2) D)) % 15.28/15.50 True) % 15.28/15.50 (Or (Eq (And (in (skS.0 8 a a_3) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_3)))) True) % 15.28/15.50 (Eq (relation_dom (skS.0 6 a a_4)) a)) % 15.28/15.50 Clause #211 (by clausification #[210]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.28/15.50 Or (Eq (And (in (skS.0 8 a a_1) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_1)))) True) % 15.28/15.50 (Or (Eq (relation_dom (skS.0 6 a a_2)) a) % 15.28/15.50 (Eq % 15.28/15.50 (∀ (D : Iota), % 15.28/15.50 And (And (in (skS.0 7 a a_3) a) (Eq (skS.0 14 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.28/15.50 (Eq D (singleton (skS.0 7 a a_3))) → % 15.28/15.50 Eq (skS.0 14 a a_3 a_4) D) % 15.28/15.50 False)) % 15.28/15.50 Clause #212 (by clausification #[211]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.28/15.50 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.28/15.50 (Or % 15.28/15.50 (Eq % 15.28/15.50 (∀ (D : Iota), % 15.28/15.50 And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 14 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.28/15.50 (Eq D (singleton (skS.0 7 a a_2))) → % 15.28/15.50 Eq (skS.0 14 a a_2 a_3) D) % 15.37/15.52 False) % 15.37/15.52 (Eq (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_4))) True)) % 15.37/15.52 Clause #214 (by clausification #[212]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or (Eq (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_2))) True) % 15.37/15.52 (Eq % 15.37/15.52 (Not % 15.37/15.52 (And (And (in (skS.0 7 a a_3) a) (Eq (skS.0 14 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.37/15.52 (Eq (skS.0 15 a a_3 a_4 a_5) (singleton (skS.0 7 a a_3))) → % 15.37/15.52 Eq (skS.0 14 a a_3 a_4) (skS.0 15 a a_3 a_4 a_5))) % 15.37/15.52 True)) % 15.37/15.52 Clause #215 (by clausification #[214]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or % 15.37/15.52 (Eq % 15.37/15.52 (Not % 15.37/15.52 (And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 14 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.37/15.52 (Eq (skS.0 15 a a_2 a_3 a_4) (singleton (skS.0 7 a a_2))) → % 15.37/15.52 Eq (skS.0 14 a a_2 a_3) (skS.0 15 a a_2 a_3 a_4))) % 15.37/15.52 True) % 15.37/15.52 (Eq (Ne a_5 (singleton (skS.0 8 a a_6))) True)) % 15.37/15.52 Clause #216 (by clausification #[215]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or (Eq (Ne a_2 (singleton (skS.0 8 a a_3))) True) % 15.37/15.52 (Eq % 15.37/15.52 (And (And (in (skS.0 7 a a_4) a) (Eq (skS.0 14 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.37/15.52 (Eq (skS.0 15 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4))) → % 15.37/15.52 Eq (skS.0 14 a a_4 a_5) (skS.0 15 a a_4 a_5 a_6)) % 15.37/15.52 False)) % 15.37/15.52 Clause #217 (by clausification #[216]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or % 15.37/15.52 (Eq % 15.37/15.52 (And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 14 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.37/15.52 (Eq (skS.0 15 a a_2 a_3 a_4) (singleton (skS.0 7 a a_2))) → % 15.37/15.52 Eq (skS.0 14 a a_2 a_3) (skS.0 15 a a_2 a_3 a_4)) % 15.37/15.52 False) % 15.37/15.52 (Ne a_5 (singleton (skS.0 8 a a_6)))) % 15.37/15.52 Clause #218 (by clausification #[217]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) % 15.37/15.52 (Eq % 15.37/15.52 (And (And (in (skS.0 7 a a_4) a) (Eq (skS.0 14 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.37/15.52 (Eq (skS.0 15 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4)))) % 15.37/15.52 True)) % 15.37/15.52 Clause #219 (by clausification #[217]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (Eq (skS.0 14 a a_4 a_5) (skS.0 15 a a_4 a_5 a_6)) False)) % 15.37/15.52 Clause #220 (by clausification #[218]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (Eq (skS.0 15 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4))) True)) % 15.37/15.52 Clause #221 (by clausification #[218]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) % 15.37/15.52 (Eq (And (in (skS.0 7 a a_4) a) (Eq (skS.0 14 a a_4 a_5) (singleton (skS.0 7 a a_4)))) True)) % 15.37/15.52 Clause #222 (by clausification #[220]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (skS.0 15 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4)))) % 15.37/15.52 Clause #223 (by destructive equality resolution #[222]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) (Eq (skS.0 15 a a_2 a_3 a_4) (singleton (skS.0 7 a a_2))) % 15.37/15.52 Clause #251 (by clausification #[219]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Ne (skS.0 14 a a_4 a_5) (skS.0 15 a a_4 a_5 a_6))) % 15.37/15.52 Clause #252 (by destructive equality resolution #[251]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) (Ne (skS.0 14 a a_2 a_3) (skS.0 15 a a_2 a_3 a_4)) % 15.37/15.52 Clause #253 (by superposition #[252, 223]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.37/15.52 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.52 (Or (Eq (relation_dom (skS.0 6 a a_2)) a) (Ne (skS.0 14 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.37/15.52 Clause #262 (by clausification #[97]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.37/15.52 Or (Eq (in a a_1) False) % 15.37/15.55 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.37/15.55 (Or (Ne a_3 (singleton (skS.0 8 a_1 a_4))) (Ne (skS.0 9 a_1 a_5 a_6) (skS.0 10 a_1 a_5 a_6 a_7)))) % 15.37/15.55 Clause #263 (by destructive equality resolution #[262]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.37/15.55 Or (Eq (in a a_1) False) % 15.37/15.55 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) (Ne (skS.0 9 a_1 a_3 a_4) (skS.0 10 a_1 a_3 a_4 a_5))) % 15.37/15.55 Clause #275 (by clausification #[99]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.55 Or (Eq (in a a_1) False) % 15.37/15.55 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.37/15.55 (Or (Ne a_3 (singleton (skS.0 8 a_1 a_4))) (Eq (Eq (skS.0 9 a_1 a_5 a_6) (singleton (skS.0 7 a_1 a_5))) True))) % 15.37/15.55 Clause #277 (by clausification #[275]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.55 Or (Eq (in a a_1) False) % 15.37/15.55 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) % 15.37/15.55 (Or (Ne a_3 (singleton (skS.0 8 a_1 a_4))) (Eq (skS.0 9 a_1 a_5 a_6) (singleton (skS.0 7 a_1 a_5))))) % 15.37/15.55 Clause #278 (by destructive equality resolution #[277]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.37/15.55 Or (Eq (in a a_1) False) % 15.37/15.55 (Or (Eq (apply (skS.0 6 a_1 a_2) a) (singleton a)) (Eq (skS.0 9 a_1 a_3 a_4) (singleton (skS.0 7 a_1 a_3)))) % 15.37/15.55 Clause #309 (by clausification #[221]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.37/15.55 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.55 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (Eq (skS.0 14 a a_4 a_5) (singleton (skS.0 7 a a_4))) True)) % 15.37/15.55 Clause #311 (by clausification #[309]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.37/15.55 Or (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.55 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (skS.0 14 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.37/15.55 Clause #312 (by destructive equality resolution #[311]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (relation_dom (skS.0 6 a a_1)) a) (Eq (skS.0 14 a a_2 a_3) (singleton (skS.0 7 a a_2))) % 15.37/15.55 Clause #313 (by backward contextual literal cutting #[312, 253]): ∀ (a a_1 a_2 : Iota), Or (Eq (relation_dom (skS.0 6 a a_1)) a) (Eq (relation_dom (skS.0 6 a a_2)) a) % 15.37/15.55 Clause #315 (by equality factoring #[313]): ∀ (a a_1 : Iota), Or (Ne a a) (Eq (relation_dom (skS.0 6 a a_1)) a) % 15.37/15.55 Clause #316 (by eliminate resolved literals #[315]): ∀ (a a_1 : Iota), Eq (relation_dom (skS.0 6 a a_1)) a % 15.37/15.55 Clause #322 (by clausification #[207]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.37/15.55 Or (Eq (Not (And (in (skS.0 8 a a_1) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_1))))) False) % 15.37/15.55 (Or (Eq (And (relation (skS.0 6 a a_2)) (function (skS.0 6 a a_2))) True) % 15.37/15.55 (Eq % 15.37/15.55 (Not % 15.37/15.55 (∀ (D : Iota), % 15.37/15.55 And (And (in (skS.0 7 a a_3) a) (Eq (skS.0 18 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.37/15.55 (Eq D (singleton (skS.0 7 a a_3))) → % 15.37/15.55 Eq (skS.0 18 a a_3 a_4) D)) % 15.37/15.55 True)) % 15.37/15.55 Clause #323 (by clausification #[322]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.37/15.55 Or (Eq (And (relation (skS.0 6 a a_1)) (function (skS.0 6 a a_1))) True) % 15.37/15.55 (Or % 15.37/15.55 (Eq % 15.37/15.55 (Not % 15.37/15.55 (∀ (D : Iota), % 15.37/15.55 And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 18 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.37/15.55 (Eq D (singleton (skS.0 7 a a_2))) → % 15.37/15.55 Eq (skS.0 18 a a_2 a_3) D)) % 15.37/15.55 True) % 15.37/15.55 (Eq (And (in (skS.0 8 a a_4) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_4)))) True)) % 15.37/15.55 Clause #324 (by clausification #[323]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.37/15.55 Or % 15.37/15.55 (Eq % 15.37/15.55 (Not % 15.37/15.55 (∀ (D : Iota), % 15.37/15.55 And (And (in (skS.0 7 a a_1) a) (Eq (skS.0 18 a a_1 a_2) (singleton (skS.0 7 a a_1)))) % 15.37/15.55 (Eq D (singleton (skS.0 7 a a_1))) → % 15.37/15.55 Eq (skS.0 18 a a_1 a_2) D)) % 15.37/15.55 True) % 15.37/15.55 (Or (Eq (And (in (skS.0 8 a a_3) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_3)))) True) % 15.37/15.55 (Eq (function (skS.0 6 a a_4)) True)) % 15.37/15.55 Clause #325 (by clausification #[323]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.37/15.55 Or % 15.37/15.55 (Eq % 15.37/15.55 (Not % 15.37/15.55 (∀ (D : Iota), % 15.37/15.55 And (And (in (skS.0 7 a a_1) a) (Eq (skS.0 18 a a_1 a_2) (singleton (skS.0 7 a a_1)))) % 15.37/15.55 (Eq D (singleton (skS.0 7 a a_1))) → % 15.37/15.55 Eq (skS.0 18 a a_1 a_2) D)) % 15.37/15.55 True) % 15.37/15.55 (Or (Eq (And (in (skS.0 8 a a_3) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_3)))) True) % 15.37/15.58 (Eq (relation (skS.0 6 a a_4)) True)) % 15.37/15.58 Clause #326 (by clausification #[324]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.37/15.58 Or (Eq (And (in (skS.0 8 a a_1) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_1)))) True) % 15.37/15.58 (Or (Eq (function (skS.0 6 a a_2)) True) % 15.37/15.58 (Eq % 15.37/15.58 (∀ (D : Iota), % 15.37/15.58 And (And (in (skS.0 7 a a_3) a) (Eq (skS.0 18 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.37/15.58 (Eq D (singleton (skS.0 7 a a_3))) → % 15.37/15.58 Eq (skS.0 18 a a_3 a_4) D) % 15.37/15.58 False)) % 15.37/15.58 Clause #327 (by clausification #[326]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.37/15.58 Or (Eq (function (skS.0 6 a a_1)) True) % 15.37/15.58 (Or % 15.37/15.58 (Eq % 15.37/15.58 (∀ (D : Iota), % 15.37/15.58 And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 18 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.37/15.58 (Eq D (singleton (skS.0 7 a a_2))) → % 15.37/15.58 Eq (skS.0 18 a a_2 a_3) D) % 15.37/15.58 False) % 15.37/15.58 (Eq (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_4))) True)) % 15.37/15.58 Clause #329 (by clausification #[327]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.37/15.58 Or (Eq (function (skS.0 6 a a_1)) True) % 15.37/15.58 (Or (Eq (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_2))) True) % 15.37/15.58 (Eq % 15.37/15.58 (Not % 15.37/15.58 (And (And (in (skS.0 7 a a_3) a) (Eq (skS.0 18 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.37/15.58 (Eq (skS.0 19 a a_3 a_4 a_5) (singleton (skS.0 7 a a_3))) → % 15.37/15.58 Eq (skS.0 18 a a_3 a_4) (skS.0 19 a a_3 a_4 a_5))) % 15.37/15.58 True)) % 15.37/15.58 Clause #330 (by clausification #[329]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.58 Or (Eq (function (skS.0 6 a a_1)) True) % 15.37/15.58 (Or % 15.37/15.58 (Eq % 15.37/15.58 (Not % 15.37/15.58 (And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 18 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.37/15.58 (Eq (skS.0 19 a a_2 a_3 a_4) (singleton (skS.0 7 a a_2))) → % 15.37/15.58 Eq (skS.0 18 a a_2 a_3) (skS.0 19 a a_2 a_3 a_4))) % 15.37/15.58 True) % 15.37/15.58 (Eq (Ne a_5 (singleton (skS.0 8 a a_6))) True)) % 15.37/15.58 Clause #331 (by clausification #[330]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.58 Or (Eq (function (skS.0 6 a a_1)) True) % 15.37/15.58 (Or (Eq (Ne a_2 (singleton (skS.0 8 a a_3))) True) % 15.37/15.58 (Eq % 15.37/15.58 (And (And (in (skS.0 7 a a_4) a) (Eq (skS.0 18 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.37/15.58 (Eq (skS.0 19 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4))) → % 15.37/15.58 Eq (skS.0 18 a a_4 a_5) (skS.0 19 a a_4 a_5 a_6)) % 15.37/15.58 False)) % 15.37/15.58 Clause #332 (by clausification #[331]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.58 Or (Eq (function (skS.0 6 a a_1)) True) % 15.37/15.58 (Or % 15.37/15.58 (Eq % 15.37/15.58 (And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 18 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.37/15.58 (Eq (skS.0 19 a a_2 a_3 a_4) (singleton (skS.0 7 a a_2))) → % 15.37/15.58 Eq (skS.0 18 a a_2 a_3) (skS.0 19 a a_2 a_3 a_4)) % 15.37/15.58 False) % 15.37/15.58 (Ne a_5 (singleton (skS.0 8 a a_6)))) % 15.37/15.58 Clause #333 (by clausification #[332]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.58 Or (Eq (function (skS.0 6 a a_1)) True) % 15.37/15.58 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) % 15.37/15.58 (Eq % 15.37/15.58 (And (And (in (skS.0 7 a a_4) a) (Eq (skS.0 18 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.37/15.58 (Eq (skS.0 19 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4)))) % 15.37/15.58 True)) % 15.37/15.58 Clause #334 (by clausification #[332]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.58 Or (Eq (function (skS.0 6 a a_1)) True) % 15.37/15.58 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (Eq (skS.0 18 a a_4 a_5) (skS.0 19 a a_4 a_5 a_6)) False)) % 15.37/15.58 Clause #335 (by clausification #[333]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.58 Or (Eq (function (skS.0 6 a a_1)) True) % 15.37/15.58 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (Eq (skS.0 19 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4))) True)) % 15.37/15.58 Clause #336 (by clausification #[333]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.37/15.58 Or (Eq (function (skS.0 6 a a_1)) True) % 15.37/15.58 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) % 15.37/15.58 (Eq (And (in (skS.0 7 a a_4) a) (Eq (skS.0 18 a a_4 a_5) (singleton (skS.0 7 a a_4)))) True)) % 15.37/15.58 Clause #337 (by clausification #[335]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.37/15.58 Or (Eq (function (skS.0 6 a a_1)) True) % 15.37/15.58 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (skS.0 19 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4)))) % 15.37/15.58 Clause #338 (by destructive equality resolution #[337]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.44/15.61 Or (Eq (function (skS.0 6 a a_1)) True) (Eq (skS.0 19 a a_2 a_3 a_4) (singleton (skS.0 7 a a_2))) % 15.44/15.61 Clause #362 (by clausification #[334]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.61 Or (Eq (function (skS.0 6 a a_1)) True) % 15.44/15.61 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Ne (skS.0 18 a a_4 a_5) (skS.0 19 a a_4 a_5 a_6))) % 15.44/15.61 Clause #363 (by destructive equality resolution #[362]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (function (skS.0 6 a a_1)) True) (Ne (skS.0 18 a a_2 a_3) (skS.0 19 a a_2 a_3 a_4)) % 15.44/15.61 Clause #364 (by superposition #[363, 338]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.44/15.61 Or (Eq (function (skS.0 6 a a_1)) True) % 15.44/15.61 (Or (Eq (function (skS.0 6 a a_2)) True) (Ne (skS.0 18 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.44/15.61 Clause #373 (by clausification #[325]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.44/15.61 Or (Eq (And (in (skS.0 8 a a_1) a) (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_1)))) True) % 15.44/15.61 (Or (Eq (relation (skS.0 6 a a_2)) True) % 15.44/15.61 (Eq % 15.44/15.61 (∀ (D : Iota), % 15.44/15.61 And (And (in (skS.0 7 a a_3) a) (Eq (skS.0 18 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.44/15.61 (Eq D (singleton (skS.0 7 a a_3))) → % 15.44/15.61 Eq (skS.0 18 a a_3 a_4) D) % 15.44/15.61 False)) % 15.44/15.61 Clause #374 (by clausification #[373]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.44/15.61 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.61 (Or % 15.44/15.61 (Eq % 15.44/15.61 (∀ (D : Iota), % 15.44/15.61 And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 18 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.44/15.61 (Eq D (singleton (skS.0 7 a a_2))) → % 15.44/15.61 Eq (skS.0 18 a a_2 a_3) D) % 15.44/15.61 False) % 15.44/15.61 (Eq (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_4))) True)) % 15.44/15.61 Clause #376 (by clausification #[374]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.44/15.61 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.61 (Or (Eq (∀ (C : Iota), Ne C (singleton (skS.0 8 a a_2))) True) % 15.44/15.61 (Eq % 15.44/15.61 (Not % 15.44/15.61 (And (And (in (skS.0 7 a a_3) a) (Eq (skS.0 18 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.44/15.61 (Eq (skS.0 21 a a_3 a_4 a_5) (singleton (skS.0 7 a a_3))) → % 15.44/15.61 Eq (skS.0 18 a a_3 a_4) (skS.0 21 a a_3 a_4 a_5))) % 15.44/15.61 True)) % 15.44/15.61 Clause #377 (by clausification #[376]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.61 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.61 (Or % 15.44/15.61 (Eq % 15.44/15.61 (Not % 15.44/15.61 (And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 18 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.44/15.61 (Eq (skS.0 21 a a_2 a_3 a_4) (singleton (skS.0 7 a a_2))) → % 15.44/15.61 Eq (skS.0 18 a a_2 a_3) (skS.0 21 a a_2 a_3 a_4))) % 15.44/15.61 True) % 15.44/15.61 (Eq (Ne a_5 (singleton (skS.0 8 a a_6))) True)) % 15.44/15.61 Clause #378 (by clausification #[377]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.61 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.61 (Or (Eq (Ne a_2 (singleton (skS.0 8 a a_3))) True) % 15.44/15.61 (Eq % 15.44/15.61 (And (And (in (skS.0 7 a a_4) a) (Eq (skS.0 18 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.44/15.61 (Eq (skS.0 21 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4))) → % 15.44/15.61 Eq (skS.0 18 a a_4 a_5) (skS.0 21 a a_4 a_5 a_6)) % 15.44/15.61 False)) % 15.44/15.61 Clause #379 (by clausification #[378]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.61 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.61 (Or % 15.44/15.61 (Eq % 15.44/15.61 (And (And (in (skS.0 7 a a_2) a) (Eq (skS.0 18 a a_2 a_3) (singleton (skS.0 7 a a_2)))) % 15.44/15.61 (Eq (skS.0 21 a a_2 a_3 a_4) (singleton (skS.0 7 a a_2))) → % 15.44/15.61 Eq (skS.0 18 a a_2 a_3) (skS.0 21 a a_2 a_3 a_4)) % 15.44/15.61 False) % 15.44/15.61 (Ne a_5 (singleton (skS.0 8 a a_6)))) % 15.44/15.61 Clause #380 (by clausification #[379]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.61 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.61 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) % 15.44/15.61 (Eq % 15.44/15.61 (And (And (in (skS.0 7 a a_4) a) (Eq (skS.0 18 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.44/15.61 (Eq (skS.0 21 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4)))) % 15.44/15.61 True)) % 15.44/15.61 Clause #381 (by clausification #[379]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.61 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.61 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (Eq (skS.0 18 a a_4 a_5) (skS.0 21 a a_4 a_5 a_6)) False)) % 15.44/15.61 Clause #382 (by clausification #[380]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.61 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.63 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (Eq (skS.0 21 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4))) True)) % 15.44/15.63 Clause #383 (by clausification #[380]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.44/15.63 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.63 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) % 15.44/15.63 (Eq (And (in (skS.0 7 a a_4) a) (Eq (skS.0 18 a a_4 a_5) (singleton (skS.0 7 a a_4)))) True)) % 15.44/15.63 Clause #384 (by clausification #[382]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.63 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.63 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (skS.0 21 a a_4 a_5 a_6) (singleton (skS.0 7 a a_4)))) % 15.44/15.63 Clause #385 (by destructive equality resolution #[384]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.44/15.63 Or (Eq (relation (skS.0 6 a a_1)) True) (Eq (skS.0 21 a a_2 a_3 a_4) (singleton (skS.0 7 a a_2))) % 15.44/15.63 Clause #522 (by clausification #[381]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.63 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.63 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Ne (skS.0 18 a a_4 a_5) (skS.0 21 a a_4 a_5 a_6))) % 15.44/15.63 Clause #523 (by destructive equality resolution #[522]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (relation (skS.0 6 a a_1)) True) (Ne (skS.0 18 a a_2 a_3) (skS.0 21 a a_2 a_3 a_4)) % 15.44/15.63 Clause #524 (by superposition #[523, 385]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.44/15.63 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.63 (Or (Eq (relation (skS.0 6 a a_2)) True) (Ne (skS.0 18 a a_3 a_4) (singleton (skS.0 7 a a_3)))) % 15.44/15.63 Clause #553 (by clausification #[383]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.44/15.63 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.63 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (Eq (skS.0 18 a a_4 a_5) (singleton (skS.0 7 a a_4))) True)) % 15.44/15.63 Clause #555 (by clausification #[553]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.44/15.63 Or (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.63 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (skS.0 18 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.44/15.63 Clause #556 (by destructive equality resolution #[555]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (relation (skS.0 6 a a_1)) True) (Eq (skS.0 18 a a_2 a_3) (singleton (skS.0 7 a a_2))) % 15.44/15.63 Clause #557 (by backward contextual literal cutting #[556, 524]): ∀ (a a_1 a_2 : Iota), Or (Eq (relation (skS.0 6 a a_1)) True) (Eq (relation (skS.0 6 a a_2)) True) % 15.44/15.63 Clause #632 (by equality factoring #[557]): ∀ (a a_1 : Iota), Or (Ne True True) (Eq (relation (skS.0 6 a a_1)) True) % 15.44/15.63 Clause #634 (by clausification #[632]): ∀ (a a_1 : Iota), Or (Eq (relation (skS.0 6 a a_1)) True) (Or (Eq True False) (Eq True False)) % 15.44/15.63 Clause #636 (by clausification #[634]): ∀ (a a_1 : Iota), Or (Eq (relation (skS.0 6 a a_1)) True) (Eq True False) % 15.44/15.63 Clause #637 (by clausification #[636]): ∀ (a a_1 : Iota), Eq (relation (skS.0 6 a a_1)) True % 15.44/15.63 Clause #638 (by superposition #[637, 40]): ∀ (a a_1 a_2 a_3 : Iota), % 15.44/15.63 Or (Eq True False) % 15.44/15.63 (Or (Eq (function (skS.0 6 a a_1)) False) % 15.44/15.63 (Or (Ne (relation_dom (skS.0 6 a a_1)) (skS.0 0 a_2)) % 15.44/15.63 (Eq (in (skS.0 1 a_2 (skS.0 6 a a_1) a_3) (skS.0 0 a_2)) True))) % 15.44/15.63 Clause #640 (by superposition #[637, 168]): ∀ (a a_1 a_2 a_3 : Iota), % 15.44/15.63 Or (Eq True False) % 15.44/15.63 (Or (Eq (function (skS.0 6 a a_1)) False) % 15.44/15.63 (Or (Ne (relation_dom (skS.0 6 a a_1)) (skS.0 0 a_2)) % 15.44/15.63 (Ne (apply (skS.0 6 a a_1) (skS.0 1 a_2 (skS.0 6 a a_1) a_3)) (singleton (skS.0 1 a_2 (skS.0 6 a a_1) a_3))))) % 15.44/15.63 Clause #709 (by clausification #[336]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.44/15.63 Or (Eq (function (skS.0 6 a a_1)) True) % 15.44/15.63 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (Eq (skS.0 18 a a_4 a_5) (singleton (skS.0 7 a a_4))) True)) % 15.44/15.63 Clause #711 (by clausification #[709]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.44/15.63 Or (Eq (function (skS.0 6 a a_1)) True) % 15.44/15.63 (Or (Ne a_2 (singleton (skS.0 8 a a_3))) (Eq (skS.0 18 a a_4 a_5) (singleton (skS.0 7 a a_4)))) % 15.44/15.63 Clause #712 (by destructive equality resolution #[711]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (function (skS.0 6 a a_1)) True) (Eq (skS.0 18 a a_2 a_3) (singleton (skS.0 7 a a_2))) % 15.44/15.63 Clause #713 (by backward contextual literal cutting #[712, 364]): ∀ (a a_1 a_2 : Iota), Or (Eq (function (skS.0 6 a a_1)) True) (Eq (function (skS.0 6 a a_2)) True) % 15.44/15.63 Clause #717 (by equality factoring #[713]): ∀ (a a_1 : Iota), Or (Ne True True) (Eq (function (skS.0 6 a a_1)) True) % 15.44/15.66 Clause #718 (by clausification #[717]): ∀ (a a_1 : Iota), Or (Eq (function (skS.0 6 a a_1)) True) (Or (Eq True False) (Eq True False)) % 15.44/15.66 Clause #720 (by clausification #[718]): ∀ (a a_1 : Iota), Or (Eq (function (skS.0 6 a a_1)) True) (Eq True False) % 15.44/15.66 Clause #721 (by clausification #[720]): ∀ (a a_1 : Iota), Eq (function (skS.0 6 a a_1)) True % 15.44/15.66 Clause #876 (by clausification #[638]): ∀ (a a_1 a_2 a_3 : Iota), % 15.44/15.66 Or (Eq (function (skS.0 6 a a_1)) False) % 15.44/15.66 (Or (Ne (relation_dom (skS.0 6 a a_1)) (skS.0 0 a_2)) % 15.44/15.66 (Eq (in (skS.0 1 a_2 (skS.0 6 a a_1) a_3) (skS.0 0 a_2)) True)) % 15.44/15.66 Clause #877 (by forward demodulation #[876, 721]): ∀ (a a_1 a_2 a_3 : Iota), % 15.44/15.66 Or (Eq True False) % 15.44/15.66 (Or (Ne (relation_dom (skS.0 6 a a_1)) (skS.0 0 a_2)) % 15.44/15.66 (Eq (in (skS.0 1 a_2 (skS.0 6 a a_1) a_3) (skS.0 0 a_2)) True)) % 15.44/15.66 Clause #878 (by clausification #[877]): ∀ (a a_1 a_2 a_3 : Iota), % 15.44/15.66 Or (Ne (relation_dom (skS.0 6 a a_1)) (skS.0 0 a_2)) (Eq (in (skS.0 1 a_2 (skS.0 6 a a_1) a_3) (skS.0 0 a_2)) True) % 15.44/15.66 Clause #879 (by forward demodulation #[878, 316]): ∀ (a a_1 a_2 a_3 : Iota), Or (Ne a (skS.0 0 a_1)) (Eq (in (skS.0 1 a_1 (skS.0 6 a a_2) a_3) (skS.0 0 a_1)) True) % 15.44/15.66 Clause #880 (by destructive equality resolution #[879]): ∀ (a a_1 a_2 : Iota), Eq (in (skS.0 1 a (skS.0 6 (skS.0 0 a) a_1) a_2) (skS.0 0 a)) True % 15.44/15.66 Clause #883 (by superposition #[880, 101]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.66 Or (Eq True False) % 15.44/15.66 (Or % 15.44/15.66 (Eq (apply (skS.0 6 (skS.0 0 a) a_1) (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3)) % 15.44/15.66 (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3))) % 15.44/15.66 (Eq (skS.0 10 (skS.0 0 a) a_4 a_5 a_6) (singleton (skS.0 7 (skS.0 0 a) a_4)))) % 15.44/15.66 Clause #886 (by superposition #[880, 263]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.44/15.66 Or (Eq True False) % 15.44/15.66 (Or % 15.44/15.66 (Eq (apply (skS.0 6 (skS.0 0 a) a_1) (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3)) % 15.44/15.66 (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3))) % 15.44/15.66 (Ne (skS.0 9 (skS.0 0 a) a_4 a_5) (skS.0 10 (skS.0 0 a) a_4 a_5 a_6))) % 15.44/15.66 Clause #887 (by superposition #[880, 278]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.44/15.66 Or (Eq True False) % 15.44/15.66 (Or % 15.44/15.66 (Eq (apply (skS.0 6 (skS.0 0 a) a_1) (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3)) % 15.44/15.66 (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3))) % 15.44/15.66 (Eq (skS.0 9 (skS.0 0 a) a_4 a_5) (singleton (skS.0 7 (skS.0 0 a) a_4)))) % 15.44/15.66 Clause #976 (by clausification #[640]): ∀ (a a_1 a_2 a_3 : Iota), % 15.44/15.66 Or (Eq (function (skS.0 6 a a_1)) False) % 15.44/15.66 (Or (Ne (relation_dom (skS.0 6 a a_1)) (skS.0 0 a_2)) % 15.44/15.66 (Ne (apply (skS.0 6 a a_1) (skS.0 1 a_2 (skS.0 6 a a_1) a_3)) (singleton (skS.0 1 a_2 (skS.0 6 a a_1) a_3)))) % 15.44/15.66 Clause #977 (by forward demodulation #[976, 721]): ∀ (a a_1 a_2 a_3 : Iota), % 15.44/15.66 Or (Eq True False) % 15.44/15.66 (Or (Ne (relation_dom (skS.0 6 a a_1)) (skS.0 0 a_2)) % 15.44/15.66 (Ne (apply (skS.0 6 a a_1) (skS.0 1 a_2 (skS.0 6 a a_1) a_3)) (singleton (skS.0 1 a_2 (skS.0 6 a a_1) a_3)))) % 15.44/15.66 Clause #978 (by clausification #[977]): ∀ (a a_1 a_2 a_3 : Iota), % 15.44/15.66 Or (Ne (relation_dom (skS.0 6 a a_1)) (skS.0 0 a_2)) % 15.44/15.66 (Ne (apply (skS.0 6 a a_1) (skS.0 1 a_2 (skS.0 6 a a_1) a_3)) (singleton (skS.0 1 a_2 (skS.0 6 a a_1) a_3))) % 15.44/15.66 Clause #979 (by forward demodulation #[978, 316]): ∀ (a a_1 a_2 a_3 : Iota), % 15.44/15.66 Or (Ne a (skS.0 0 a_1)) % 15.44/15.66 (Ne (apply (skS.0 6 a a_2) (skS.0 1 a_1 (skS.0 6 a a_2) a_3)) (singleton (skS.0 1 a_1 (skS.0 6 a a_2) a_3))) % 15.44/15.66 Clause #980 (by destructive equality resolution #[979]): ∀ (a a_1 a_2 : Iota), % 15.44/15.66 Ne (apply (skS.0 6 (skS.0 0 a) a_1) (skS.0 1 a (skS.0 6 (skS.0 0 a) a_1) a_2)) % 15.44/15.66 (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_1) a_2)) % 15.44/15.66 Clause #1102 (by clausification #[887]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.44/15.66 Or % 15.44/15.66 (Eq (apply (skS.0 6 (skS.0 0 a) a_1) (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3)) % 15.44/15.66 (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3))) % 15.44/15.66 (Eq (skS.0 9 (skS.0 0 a) a_4 a_5) (singleton (skS.0 7 (skS.0 0 a) a_4))) % 15.44/15.66 Clause #1103 (by superposition #[1102, 980]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.44/15.66 Or (Eq (skS.0 9 (skS.0 0 a) a_1 a_2) (singleton (skS.0 7 (skS.0 0 a) a_1))) % 15.53/15.68 (Ne (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_3) a_4)) (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_3) a_4))) % 15.53/15.68 Clause #1104 (by eliminate resolved literals #[1103]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 9 (skS.0 0 a) a_1 a_2) (singleton (skS.0 7 (skS.0 0 a) a_1)) % 15.53/15.68 Clause #1107 (by clausification #[883]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.53/15.68 Or % 15.53/15.68 (Eq (apply (skS.0 6 (skS.0 0 a) a_1) (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3)) % 15.53/15.68 (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3))) % 15.53/15.68 (Eq (skS.0 10 (skS.0 0 a) a_4 a_5 a_6) (singleton (skS.0 7 (skS.0 0 a) a_4))) % 15.53/15.68 Clause #1108 (by superposition #[1107, 980]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 15.53/15.68 Or (Eq (skS.0 10 (skS.0 0 a) a_1 a_2 a_3) (singleton (skS.0 7 (skS.0 0 a) a_1))) % 15.53/15.68 (Ne (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_4) a_5)) (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_4) a_5))) % 15.53/15.68 Clause #1109 (by eliminate resolved literals #[1108]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 10 (skS.0 0 a) a_1 a_2 a_3) (singleton (skS.0 7 (skS.0 0 a) a_1)) % 15.53/15.68 Clause #1111 (by clausification #[886]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.53/15.68 Or % 15.53/15.68 (Eq (apply (skS.0 6 (skS.0 0 a) a_1) (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3)) % 15.53/15.68 (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3))) % 15.53/15.68 (Ne (skS.0 9 (skS.0 0 a) a_4 a_5) (skS.0 10 (skS.0 0 a) a_4 a_5 a_6)) % 15.53/15.68 Clause #1112 (by forward demodulation #[1111, 1104]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 15.53/15.68 Or % 15.53/15.68 (Eq (apply (skS.0 6 (skS.0 0 a) a_1) (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3)) % 15.53/15.68 (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3))) % 15.53/15.68 (Ne (singleton (skS.0 7 (skS.0 0 a) a_4)) (skS.0 10 (skS.0 0 a) a_4 a_5 a_6)) % 15.53/15.68 Clause #1113 (by forward demodulation #[1112, 1109]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 15.53/15.68 Or % 15.53/15.68 (Eq (apply (skS.0 6 (skS.0 0 a) a_1) (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3)) % 15.53/15.68 (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3))) % 15.53/15.68 (Ne (singleton (skS.0 7 (skS.0 0 a) a_4)) (singleton (skS.0 7 (skS.0 0 a) a_4))) % 15.53/15.68 Clause #1114 (by eliminate resolved literals #[1113]): ∀ (a a_1 a_2 a_3 : Iota), % 15.53/15.68 Eq (apply (skS.0 6 (skS.0 0 a) a_1) (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3)) % 15.53/15.68 (singleton (skS.0 1 a (skS.0 6 (skS.0 0 a) a_2) a_3)) % 15.53/15.68 Clause #1116 (by backward contextual literal cutting #[1114, 980]): False % 15.53/15.68 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------