%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU359+1 : TPTP v9.2.0. Released v3.3.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 08:01:27 PM UTC 2025 % Result : Theorem 11.97s 12.17s % Output : Proof 12.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU359+1 : TPTP v9.2.0. Released v3.3.0. % 0.07/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 : Fri Oct 3 06:06:38 EDT 2025 % 0.13/0.34 % CPUTime : % 11.97/12.17 SZS status Theorem for theBenchmark.p % 11.97/12.17 SZS output start Proof for theBenchmark.p % 11.97/12.17 Clause #0 (by assumption #[]): Eq % 11.97/12.17 (∀ (A : Iota), % 11.97/12.17 rel_str A → % 11.97/12.17 ∀ (B C : Iota), % 11.97/12.17 element C (the_carrier A) → % 11.97/12.17 ex_sup_of_relstr_set A B → % 11.97/12.17 Iff (Eq C (join_on_relstr A B)) % 11.97/12.17 (And (relstr_set_smaller A B C) % 11.97/12.17 (∀ (D : Iota), element D (the_carrier A) → relstr_set_smaller A B D → related A C D))) % 11.97/12.17 True % 11.97/12.17 Clause #1 (by assumption #[]): Eq (∀ (A B : Iota), rel_str A → element (join_on_relstr A B) (the_carrier A)) True % 11.97/12.17 Clause #7 (by assumption #[]): Eq % 11.97/12.17 (∀ (A : Iota), % 11.97/12.17 And (antisymmetric_relstr A) (rel_str A) → % 11.97/12.17 ∀ (B : Iota), % 11.97/12.17 Iff (ex_sup_of_relstr_set A B) % 11.97/12.17 (Exists fun C => % 11.97/12.17 And (And (element C (the_carrier A)) (relstr_set_smaller A B C)) % 11.97/12.17 (∀ (D : Iota), element D (the_carrier A) → relstr_set_smaller A B D → related A C D))) % 11.97/12.17 True % 11.97/12.17 Clause #8 (by assumption #[]): Eq % 11.97/12.17 (Not % 11.97/12.17 (∀ (A : Iota), % 11.97/12.17 And (antisymmetric_relstr A) (rel_str A) → % 11.97/12.17 ∀ (B : Iota), % 11.97/12.17 element B (the_carrier A) → % 11.97/12.17 ∀ (C : Iota), % 11.97/12.17 And % 11.97/12.17 (And (Eq B (join_on_relstr A C)) (ex_sup_of_relstr_set A C) → % 11.97/12.17 And (relstr_set_smaller A C B) % 11.97/12.17 (∀ (D : Iota), element D (the_carrier A) → relstr_set_smaller A C D → related A B D)) % 11.97/12.17 (And (relstr_set_smaller A C B) % 11.97/12.17 (∀ (D : Iota), element D (the_carrier A) → relstr_set_smaller A C D → related A B D) → % 11.97/12.17 And (Eq B (join_on_relstr A C)) (ex_sup_of_relstr_set A C)))) % 11.97/12.17 True % 11.97/12.17 Clause #18 (by clausification #[0]): ∀ (a : Iota), % 11.97/12.17 Eq % 11.97/12.17 (rel_str a → % 11.97/12.17 ∀ (B C : Iota), % 11.97/12.17 element C (the_carrier a) → % 11.97/12.17 ex_sup_of_relstr_set a B → % 11.97/12.17 Iff (Eq C (join_on_relstr a B)) % 11.97/12.17 (And (relstr_set_smaller a B C) % 11.97/12.17 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a B D → related a C D))) % 11.97/12.17 True % 11.97/12.17 Clause #19 (by clausification #[18]): ∀ (a : Iota), % 11.97/12.17 Or (Eq (rel_str a) False) % 11.97/12.17 (Eq % 11.97/12.17 (∀ (B C : Iota), % 11.97/12.17 element C (the_carrier a) → % 11.97/12.17 ex_sup_of_relstr_set a B → % 11.97/12.17 Iff (Eq C (join_on_relstr a B)) % 11.97/12.17 (And (relstr_set_smaller a B C) % 11.97/12.17 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a B D → related a C D))) % 11.97/12.17 True) % 11.97/12.17 Clause #20 (by clausification #[19]): ∀ (a a_1 : Iota), % 11.97/12.17 Or (Eq (rel_str a) False) % 11.97/12.17 (Eq % 11.97/12.17 (∀ (C : Iota), % 11.97/12.17 element C (the_carrier a) → % 11.97/12.17 ex_sup_of_relstr_set a a_1 → % 11.97/12.17 Iff (Eq C (join_on_relstr a a_1)) % 11.97/12.17 (And (relstr_set_smaller a a_1 C) % 11.97/12.17 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a C D))) % 11.97/12.17 True) % 11.97/12.17 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 : Iota), % 11.97/12.17 Or (Eq (rel_str a) False) % 11.97/12.17 (Eq % 11.97/12.17 (element a_1 (the_carrier a) → % 11.97/12.17 ex_sup_of_relstr_set a a_2 → % 11.97/12.17 Iff (Eq a_1 (join_on_relstr a a_2)) % 11.97/12.17 (And (relstr_set_smaller a a_2 a_1) % 11.97/12.17 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_2 D → related a a_1 D))) % 11.97/12.17 True) % 11.97/12.17 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 : Iota), % 11.97/12.17 Or (Eq (rel_str a) False) % 11.97/12.17 (Or (Eq (element a_1 (the_carrier a)) False) % 11.97/12.17 (Eq % 11.97/12.17 (ex_sup_of_relstr_set a a_2 → % 11.97/12.17 Iff (Eq a_1 (join_on_relstr a a_2)) % 11.97/12.17 (And (relstr_set_smaller a a_2 a_1) % 11.97/12.17 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_2 D → related a a_1 D))) % 11.97/12.17 True)) % 11.97/12.17 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 : Iota), % 11.97/12.17 Or (Eq (rel_str a) False) % 11.97/12.17 (Or (Eq (element a_1 (the_carrier a)) False) % 11.97/12.17 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 11.97/12.17 (Eq % 11.97/12.17 (Iff (Eq a_1 (join_on_relstr a a_2)) % 11.97/12.17 (And (relstr_set_smaller a a_2 a_1) % 11.97/12.17 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_2 D → related a a_1 D))) % 11.97/12.17 True))) % 11.97/12.19 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 : Iota), % 11.97/12.19 Or (Eq (rel_str a) False) % 11.97/12.19 (Or (Eq (element a_1 (the_carrier a)) False) % 11.97/12.19 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 11.97/12.19 (Or (Eq (Eq a_1 (join_on_relstr a a_2)) True) % 11.97/12.19 (Eq % 11.97/12.19 (And (relstr_set_smaller a a_2 a_1) % 11.97/12.19 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_2 D → related a a_1 D)) % 11.97/12.19 False)))) % 11.97/12.19 Clause #25 (by clausification #[23]): ∀ (a a_1 a_2 : Iota), % 11.97/12.19 Or (Eq (rel_str a) False) % 11.97/12.19 (Or (Eq (element a_1 (the_carrier a)) False) % 11.97/12.19 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 11.97/12.19 (Or (Eq (Eq a_1 (join_on_relstr a a_2)) False) % 11.97/12.19 (Eq % 11.97/12.19 (And (relstr_set_smaller a a_2 a_1) % 11.97/12.19 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_2 D → related a a_1 D)) % 11.97/12.19 True)))) % 11.97/12.19 Clause #26 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), % 11.97/12.19 Or (Eq (rel_str a) False) % 11.97/12.19 (Or (Eq (element a_1 (the_carrier a)) False) % 11.97/12.19 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 11.97/12.19 (Or % 11.97/12.19 (Eq % 11.97/12.19 (And (relstr_set_smaller a a_2 a_1) % 11.97/12.19 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_2 D → related a a_1 D)) % 11.97/12.19 False) % 11.97/12.19 (Eq a_1 (join_on_relstr a a_2))))) % 11.97/12.19 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), % 11.97/12.19 Or (Eq (rel_str a) False) % 11.97/12.19 (Or (Eq (element a_1 (the_carrier a)) False) % 11.97/12.19 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 11.97/12.19 (Or (Eq a_1 (join_on_relstr a a_2)) % 11.97/12.19 (Or (Eq (relstr_set_smaller a a_2 a_1) False) % 11.97/12.19 (Eq (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_2 D → related a a_1 D) False))))) % 11.97/12.19 Clause #28 (by clausification #[27]): ∀ (a a_1 a_2 a_3 : Iota), % 11.97/12.19 Or (Eq (rel_str a) False) % 11.97/12.19 (Or (Eq (element a_1 (the_carrier a)) False) % 11.97/12.19 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 11.97/12.19 (Or (Eq a_1 (join_on_relstr a a_2)) % 11.97/12.19 (Or (Eq (relstr_set_smaller a a_2 a_1) False) % 11.97/12.19 (Eq % 11.97/12.19 (Not % 11.97/12.19 (element (skS.0 3 a a_2 a_1 a_3) (the_carrier a) → % 11.97/12.19 relstr_set_smaller a a_2 (skS.0 3 a a_2 a_1 a_3) → related a a_1 (skS.0 3 a a_2 a_1 a_3))) % 11.97/12.19 True))))) % 11.97/12.19 Clause #29 (by clausification #[28]): ∀ (a a_1 a_2 a_3 : Iota), % 11.97/12.19 Or (Eq (rel_str a) False) % 11.97/12.19 (Or (Eq (element a_1 (the_carrier a)) False) % 11.97/12.19 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 11.97/12.19 (Or (Eq a_1 (join_on_relstr a a_2)) % 11.97/12.19 (Or (Eq (relstr_set_smaller a a_2 a_1) False) % 11.97/12.19 (Eq % 11.97/12.19 (element (skS.0 3 a a_2 a_1 a_3) (the_carrier a) → % 11.97/12.19 relstr_set_smaller a a_2 (skS.0 3 a a_2 a_1 a_3) → related a a_1 (skS.0 3 a a_2 a_1 a_3)) % 11.97/12.19 False))))) % 11.97/12.19 Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 a_3 : Iota), % 11.97/12.19 Or (Eq (rel_str a) False) % 11.97/12.19 (Or (Eq (element a_1 (the_carrier a)) False) % 11.97/12.19 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 11.97/12.19 (Or (Eq a_1 (join_on_relstr a a_2)) % 11.97/12.19 (Or (Eq (relstr_set_smaller a a_2 a_1) False) (Eq (element (skS.0 3 a a_2 a_1 a_3) (the_carrier a)) True))))) % 11.97/12.19 Clause #31 (by clausification #[29]): ∀ (a a_1 a_2 a_3 : Iota), % 11.97/12.19 Or (Eq (rel_str a) False) % 11.97/12.19 (Or (Eq (element a_1 (the_carrier a)) False) % 11.97/12.19 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 11.97/12.19 (Or (Eq a_1 (join_on_relstr a a_2)) % 11.97/12.19 (Or (Eq (relstr_set_smaller a a_2 a_1) False) % 11.97/12.19 (Eq (relstr_set_smaller a a_2 (skS.0 3 a a_2 a_1 a_3) → related a a_1 (skS.0 3 a a_2 a_1 a_3)) False))))) % 11.97/12.19 Clause #34 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B : Iota), rel_str a → element (join_on_relstr a B) (the_carrier a)) True % 11.97/12.19 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), Eq (rel_str a → element (join_on_relstr a a_1) (the_carrier a)) True % 11.97/12.19 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), Or (Eq (rel_str a) False) (Eq (element (join_on_relstr a a_1) (the_carrier a)) True) % 11.97/12.19 Clause #39 (by clausification #[7]): ∀ (a : Iota), % 11.97/12.19 Eq % 11.97/12.19 (And (antisymmetric_relstr a) (rel_str a) → % 11.97/12.19 ∀ (B : Iota), % 11.97/12.19 Iff (ex_sup_of_relstr_set a B) % 12.04/12.21 (Exists fun C => % 12.04/12.21 And (And (element C (the_carrier a)) (relstr_set_smaller a B C)) % 12.04/12.21 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a B D → related a C D))) % 12.04/12.21 True % 12.04/12.21 Clause #40 (by clausification #[39]): ∀ (a : Iota), % 12.04/12.21 Or (Eq (And (antisymmetric_relstr a) (rel_str a)) False) % 12.04/12.21 (Eq % 12.04/12.21 (∀ (B : Iota), % 12.04/12.21 Iff (ex_sup_of_relstr_set a B) % 12.04/12.21 (Exists fun C => % 12.04/12.21 And (And (element C (the_carrier a)) (relstr_set_smaller a B C)) % 12.04/12.21 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a B D → related a C D))) % 12.04/12.21 True) % 12.04/12.21 Clause #41 (by clausification #[40]): ∀ (a : Iota), % 12.04/12.21 Or % 12.04/12.21 (Eq % 12.04/12.21 (∀ (B : Iota), % 12.04/12.21 Iff (ex_sup_of_relstr_set a B) % 12.04/12.21 (Exists fun C => % 12.04/12.21 And (And (element C (the_carrier a)) (relstr_set_smaller a B C)) % 12.04/12.21 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a B D → related a C D))) % 12.04/12.21 True) % 12.04/12.21 (Or (Eq (antisymmetric_relstr a) False) (Eq (rel_str a) False)) % 12.04/12.21 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), % 12.04/12.21 Or (Eq (antisymmetric_relstr a) False) % 12.04/12.21 (Or (Eq (rel_str a) False) % 12.04/12.21 (Eq % 12.04/12.21 (Iff (ex_sup_of_relstr_set a a_1) % 12.04/12.21 (Exists fun C => % 12.04/12.21 And (And (element C (the_carrier a)) (relstr_set_smaller a a_1 C)) % 12.04/12.21 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a C D))) % 12.04/12.21 True)) % 12.04/12.21 Clause #43 (by clausification #[42]): ∀ (a a_1 : Iota), % 12.04/12.21 Or (Eq (antisymmetric_relstr a) False) % 12.04/12.21 (Or (Eq (rel_str a) False) % 12.04/12.21 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 12.04/12.21 (Eq % 12.04/12.21 (Exists fun C => % 12.04/12.21 And (And (element C (the_carrier a)) (relstr_set_smaller a a_1 C)) % 12.04/12.21 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a C D)) % 12.04/12.21 False))) % 12.04/12.21 Clause #45 (by clausification #[43]): ∀ (a a_1 a_2 : Iota), % 12.04/12.21 Or (Eq (antisymmetric_relstr a) False) % 12.04/12.21 (Or (Eq (rel_str a) False) % 12.04/12.21 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 12.04/12.21 (Eq % 12.04/12.21 (And (And (element a_2 (the_carrier a)) (relstr_set_smaller a a_1 a_2)) % 12.04/12.21 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a a_2 D)) % 12.04/12.21 False))) % 12.04/12.21 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 : Iota), % 12.04/12.21 Or (Eq (antisymmetric_relstr a) False) % 12.04/12.21 (Or (Eq (rel_str a) False) % 12.04/12.21 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 12.04/12.21 (Or (Eq (And (element a_2 (the_carrier a)) (relstr_set_smaller a a_1 a_2)) False) % 12.04/12.21 (Eq (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a a_2 D) False)))) % 12.04/12.21 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 : Iota), % 12.04/12.21 Or (Eq (antisymmetric_relstr a) False) % 12.04/12.21 (Or (Eq (rel_str a) False) % 12.04/12.21 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 12.04/12.21 (Or (Eq (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a a_2 D) False) % 12.04/12.21 (Or (Eq (element a_2 (the_carrier a)) False) (Eq (relstr_set_smaller a a_1 a_2) False))))) % 12.04/12.21 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 : Iota), % 12.04/12.21 Or (Eq (antisymmetric_relstr a) False) % 12.04/12.21 (Or (Eq (rel_str a) False) % 12.04/12.21 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 12.04/12.21 (Or (Eq (element a_2 (the_carrier a)) False) % 12.04/12.21 (Or (Eq (relstr_set_smaller a a_1 a_2) False) % 12.04/12.21 (Eq % 12.04/12.21 (Not % 12.04/12.21 (element (skS.0 4 a a_1 a_2 a_3) (the_carrier a) → % 12.04/12.21 relstr_set_smaller a a_1 (skS.0 4 a a_1 a_2 a_3) → related a a_2 (skS.0 4 a a_1 a_2 a_3))) % 12.04/12.21 True))))) % 12.04/12.21 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 : Iota), % 12.04/12.21 Or (Eq (antisymmetric_relstr a) False) % 12.04/12.21 (Or (Eq (rel_str a) False) % 12.04/12.21 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 12.04/12.21 (Or (Eq (element a_2 (the_carrier a)) False) % 12.04/12.21 (Or (Eq (relstr_set_smaller a a_1 a_2) False) % 12.04/12.21 (Eq % 12.04/12.21 (element (skS.0 4 a a_1 a_2 a_3) (the_carrier a) → % 12.04/12.21 relstr_set_smaller a a_1 (skS.0 4 a a_1 a_2 a_3) → related a a_2 (skS.0 4 a a_1 a_2 a_3)) % 12.04/12.23 False))))) % 12.04/12.23 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 a_3 : Iota), % 12.04/12.23 Or (Eq (antisymmetric_relstr a) False) % 12.04/12.23 (Or (Eq (rel_str a) False) % 12.04/12.23 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 12.04/12.23 (Or (Eq (element a_2 (the_carrier a)) False) % 12.04/12.23 (Or (Eq (relstr_set_smaller a a_1 a_2) False) (Eq (element (skS.0 4 a a_1 a_2 a_3) (the_carrier a)) True))))) % 12.04/12.23 Clause #51 (by clausification #[49]): ∀ (a a_1 a_2 a_3 : Iota), % 12.04/12.23 Or (Eq (antisymmetric_relstr a) False) % 12.04/12.23 (Or (Eq (rel_str a) False) % 12.04/12.23 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 12.04/12.23 (Or (Eq (element a_2 (the_carrier a)) False) % 12.04/12.23 (Or (Eq (relstr_set_smaller a a_1 a_2) False) % 12.04/12.23 (Eq (relstr_set_smaller a a_1 (skS.0 4 a a_1 a_2 a_3) → related a a_2 (skS.0 4 a a_1 a_2 a_3)) False))))) % 12.04/12.23 Clause #58 (by clausification #[8]): Eq % 12.04/12.23 (∀ (A : Iota), % 12.04/12.23 And (antisymmetric_relstr A) (rel_str A) → % 12.04/12.23 ∀ (B : Iota), % 12.04/12.23 element B (the_carrier A) → % 12.04/12.23 ∀ (C : Iota), % 12.04/12.23 And % 12.04/12.23 (And (Eq B (join_on_relstr A C)) (ex_sup_of_relstr_set A C) → % 12.04/12.23 And (relstr_set_smaller A C B) % 12.04/12.23 (∀ (D : Iota), element D (the_carrier A) → relstr_set_smaller A C D → related A B D)) % 12.04/12.23 (And (relstr_set_smaller A C B) % 12.04/12.23 (∀ (D : Iota), element D (the_carrier A) → relstr_set_smaller A C D → related A B D) → % 12.04/12.23 And (Eq B (join_on_relstr A C)) (ex_sup_of_relstr_set A C))) % 12.04/12.23 False % 12.04/12.23 Clause #59 (by clausification #[58]): ∀ (a : Iota), % 12.04/12.23 Eq % 12.04/12.23 (Not % 12.04/12.23 (And (antisymmetric_relstr (skS.0 6 a)) (rel_str (skS.0 6 a)) → % 12.04/12.23 ∀ (B : Iota), % 12.04/12.23 element B (the_carrier (skS.0 6 a)) → % 12.04/12.23 ∀ (C : Iota), % 12.04/12.23 And % 12.04/12.23 (And (Eq B (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C) → % 12.04/12.23 And (relstr_set_smaller (skS.0 6 a) C B) % 12.04/12.23 (∀ (D : Iota), % 12.04/12.23 element D (the_carrier (skS.0 6 a)) → % 12.04/12.23 relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) B D)) % 12.04/12.23 (And (relstr_set_smaller (skS.0 6 a) C B) % 12.04/12.23 (∀ (D : Iota), % 12.04/12.23 element D (the_carrier (skS.0 6 a)) → % 12.04/12.23 relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) B D) → % 12.04/12.23 And (Eq B (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C)))) % 12.04/12.23 True % 12.04/12.23 Clause #60 (by clausification #[59]): ∀ (a : Iota), % 12.04/12.23 Eq % 12.04/12.23 (And (antisymmetric_relstr (skS.0 6 a)) (rel_str (skS.0 6 a)) → % 12.04/12.23 ∀ (B : Iota), % 12.04/12.23 element B (the_carrier (skS.0 6 a)) → % 12.04/12.23 ∀ (C : Iota), % 12.04/12.23 And % 12.04/12.23 (And (Eq B (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C) → % 12.04/12.23 And (relstr_set_smaller (skS.0 6 a) C B) % 12.04/12.23 (∀ (D : Iota), % 12.04/12.23 element D (the_carrier (skS.0 6 a)) → relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) B D)) % 12.04/12.23 (And (relstr_set_smaller (skS.0 6 a) C B) % 12.04/12.23 (∀ (D : Iota), % 12.04/12.23 element D (the_carrier (skS.0 6 a)) → % 12.04/12.23 relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) B D) → % 12.04/12.23 And (Eq B (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C))) % 12.04/12.23 False % 12.04/12.23 Clause #61 (by clausification #[60]): ∀ (a : Iota), Eq (And (antisymmetric_relstr (skS.0 6 a)) (rel_str (skS.0 6 a))) True % 12.04/12.23 Clause #62 (by clausification #[60]): ∀ (a : Iota), % 12.04/12.23 Eq % 12.04/12.23 (∀ (B : Iota), % 12.04/12.23 element B (the_carrier (skS.0 6 a)) → % 12.04/12.23 ∀ (C : Iota), % 12.04/12.23 And % 12.04/12.23 (And (Eq B (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C) → % 12.04/12.23 And (relstr_set_smaller (skS.0 6 a) C B) % 12.04/12.23 (∀ (D : Iota), % 12.04/12.23 element D (the_carrier (skS.0 6 a)) → relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) B D)) % 12.04/12.23 (And (relstr_set_smaller (skS.0 6 a) C B) % 12.04/12.23 (∀ (D : Iota), % 12.04/12.23 element D (the_carrier (skS.0 6 a)) → relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) B D) → % 12.04/12.26 And (Eq B (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C))) % 12.04/12.26 False % 12.04/12.26 Clause #63 (by clausification #[61]): ∀ (a : Iota), Eq (rel_str (skS.0 6 a)) True % 12.04/12.26 Clause #64 (by clausification #[61]): ∀ (a : Iota), Eq (antisymmetric_relstr (skS.0 6 a)) True % 12.04/12.26 Clause #66 (by superposition #[63, 30]): ∀ (a a_1 a_2 a_3 : Iota), % 12.04/12.26 Or (Eq True False) % 12.04/12.26 (Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 12.04/12.26 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a_1) a_2) False) % 12.04/12.26 (Or (Eq a (join_on_relstr (skS.0 6 a_1) a_2)) % 12.04/12.26 (Or (Eq (relstr_set_smaller (skS.0 6 a_1) a_2 a) False) % 12.04/12.26 (Eq (element (skS.0 3 (skS.0 6 a_1) a_2 a a_3) (the_carrier (skS.0 6 a_1))) True))))) % 12.04/12.26 Clause #67 (by superposition #[63, 36]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (element (join_on_relstr (skS.0 6 a) a_1) (the_carrier (skS.0 6 a))) True) % 12.04/12.26 Clause #68 (by superposition #[64, 50]): ∀ (a a_1 a_2 a_3 : Iota), % 12.04/12.26 Or (Eq True False) % 12.04/12.26 (Or (Eq (rel_str (skS.0 6 a)) False) % 12.04/12.26 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.04/12.26 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.04/12.26 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.04/12.26 (Eq (element (skS.0 4 (skS.0 6 a) a_1 a_2 a_3) (the_carrier (skS.0 6 a))) True))))) % 12.04/12.26 Clause #71 (by clausification #[67]): ∀ (a a_1 : Iota), Eq (element (join_on_relstr (skS.0 6 a) a_1) (the_carrier (skS.0 6 a))) True % 12.04/12.26 Clause #72 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), % 12.04/12.26 Or (Eq (rel_str a) False) % 12.04/12.26 (Or (Eq (element a_1 (the_carrier a)) False) % 12.04/12.26 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 12.04/12.26 (Or % 12.04/12.26 (Eq % 12.04/12.26 (And (relstr_set_smaller a a_2 a_1) % 12.04/12.26 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_2 D → related a a_1 D)) % 12.04/12.26 True) % 12.04/12.26 (Ne a_1 (join_on_relstr a a_2))))) % 12.04/12.26 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), % 12.04/12.26 Or (Eq (rel_str a) False) % 12.04/12.26 (Or (Eq (element a_1 (the_carrier a)) False) % 12.04/12.26 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 12.04/12.26 (Or (Ne a_1 (join_on_relstr a a_2)) % 12.04/12.26 (Eq (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_2 D → related a a_1 D) True)))) % 12.04/12.26 Clause #74 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), % 12.04/12.26 Or (Eq (rel_str a) False) % 12.04/12.26 (Or (Eq (element a_1 (the_carrier a)) False) % 12.04/12.26 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 12.04/12.26 (Or (Ne a_1 (join_on_relstr a a_2)) (Eq (relstr_set_smaller a a_2 a_1) True)))) % 12.04/12.26 Clause #75 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), % 12.04/12.26 Or (Eq (rel_str a) False) % 12.04/12.26 (Or (Eq (element a_1 (the_carrier a)) False) % 12.04/12.26 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 12.04/12.26 (Or (Ne a_1 (join_on_relstr a a_2)) % 12.04/12.26 (Eq (element a_3 (the_carrier a) → relstr_set_smaller a a_2 a_3 → related a a_1 a_3) True)))) % 12.04/12.26 Clause #76 (by clausification #[75]): ∀ (a a_1 a_2 a_3 : Iota), % 12.04/12.26 Or (Eq (rel_str a) False) % 12.04/12.26 (Or (Eq (element a_1 (the_carrier a)) False) % 12.04/12.26 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 12.04/12.26 (Or (Ne a_1 (join_on_relstr a a_2)) % 12.04/12.26 (Or (Eq (element a_3 (the_carrier a)) False) (Eq (relstr_set_smaller a a_2 a_3 → related a a_1 a_3) True))))) % 12.04/12.26 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 : Iota), % 12.04/12.26 Or (Eq (rel_str a) False) % 12.04/12.26 (Or (Eq (element a_1 (the_carrier a)) False) % 12.04/12.26 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 12.04/12.26 (Or (Ne a_1 (join_on_relstr a a_2)) % 12.04/12.26 (Or (Eq (element a_3 (the_carrier a)) False) % 12.04/12.26 (Or (Eq (relstr_set_smaller a a_2 a_3) False) (Eq (related a a_1 a_3) True)))))) % 12.04/12.26 Clause #78 (by destructive equality resolution #[77]): ∀ (a a_1 a_2 : Iota), % 12.04/12.26 Or (Eq (rel_str a) False) % 12.04/12.26 (Or (Eq (element (join_on_relstr a a_1) (the_carrier a)) False) % 12.04/12.26 (Or (Eq (ex_sup_of_relstr_set a a_1) False) % 12.04/12.26 (Or (Eq (element a_2 (the_carrier a)) False) % 12.04/12.26 (Or (Eq (relstr_set_smaller a a_1 a_2) False) (Eq (related a (join_on_relstr a a_1) a_2) True))))) % 12.04/12.26 Clause #80 (by superposition #[78, 63]): ∀ (a a_1 a_2 : Iota), % 12.10/12.28 Or (Eq (element (join_on_relstr (skS.0 6 a) a_1) (the_carrier (skS.0 6 a))) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.28 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.28 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.28 (Or (Eq (related (skS.0 6 a) (join_on_relstr (skS.0 6 a) a_1) a_2) True) (Eq False True))))) % 12.10/12.28 Clause #81 (by destructive equality resolution #[74]): ∀ (a a_1 : Iota), % 12.10/12.28 Or (Eq (rel_str a) False) % 12.10/12.28 (Or (Eq (element (join_on_relstr a a_1) (the_carrier a)) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set a a_1) False) (Eq (relstr_set_smaller a a_1 (join_on_relstr a a_1)) True))) % 12.10/12.28 Clause #83 (by superposition #[81, 63]): ∀ (a a_1 : Iota), % 12.10/12.28 Or (Eq (element (join_on_relstr (skS.0 6 a) a_1) (the_carrier (skS.0 6 a))) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.28 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (join_on_relstr (skS.0 6 a) a_1)) True) (Eq False True))) % 12.10/12.28 Clause #84 (by clausification #[31]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.28 Or (Eq (rel_str a) False) % 12.10/12.28 (Or (Eq (element a_1 (the_carrier a)) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 12.10/12.28 (Or (Eq a_1 (join_on_relstr a a_2)) % 12.10/12.28 (Or (Eq (relstr_set_smaller a a_2 a_1) False) (Eq (relstr_set_smaller a a_2 (skS.0 3 a a_2 a_1 a_3)) True))))) % 12.10/12.28 Clause #85 (by clausification #[31]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.28 Or (Eq (rel_str a) False) % 12.10/12.28 (Or (Eq (element a_1 (the_carrier a)) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set a a_2) False) % 12.10/12.28 (Or (Eq a_1 (join_on_relstr a a_2)) % 12.10/12.28 (Or (Eq (relstr_set_smaller a a_2 a_1) False) (Eq (related a a_1 (skS.0 3 a a_2 a_1 a_3)) False))))) % 12.10/12.28 Clause #87 (by superposition #[84, 63]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.28 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a_1) a_2) False) % 12.10/12.28 (Or (Eq a (join_on_relstr (skS.0 6 a_1) a_2)) % 12.10/12.28 (Or (Eq (relstr_set_smaller (skS.0 6 a_1) a_2 a) False) % 12.10/12.28 (Or (Eq (relstr_set_smaller (skS.0 6 a_1) a_2 (skS.0 3 (skS.0 6 a_1) a_2 a a_3)) True) (Eq False True))))) % 12.10/12.28 Clause #88 (by clausification #[51]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.28 Or (Eq (antisymmetric_relstr a) False) % 12.10/12.28 (Or (Eq (rel_str a) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 12.10/12.28 (Or (Eq (element a_2 (the_carrier a)) False) % 12.10/12.28 (Or (Eq (relstr_set_smaller a a_1 a_2) False) (Eq (relstr_set_smaller a a_1 (skS.0 4 a a_1 a_2 a_3)) True))))) % 12.10/12.28 Clause #89 (by clausification #[51]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.28 Or (Eq (antisymmetric_relstr a) False) % 12.10/12.28 (Or (Eq (rel_str a) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 12.10/12.28 (Or (Eq (element a_2 (the_carrier a)) False) % 12.10/12.28 (Or (Eq (relstr_set_smaller a a_1 a_2) False) (Eq (related a a_2 (skS.0 4 a a_1 a_2 a_3)) False))))) % 12.10/12.28 Clause #90 (by superposition #[88, 64]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.28 Or (Eq (rel_str (skS.0 6 a)) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.28 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.28 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.28 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 4 (skS.0 6 a) a_1 a_2 a_3)) True) (Eq False True))))) % 12.10/12.28 Clause #91 (by superposition #[89, 64]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.28 Or (Eq (rel_str (skS.0 6 a)) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.28 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.28 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.28 (Or (Eq (related (skS.0 6 a) a_2 (skS.0 4 (skS.0 6 a) a_1 a_2 a_3)) False) (Eq False True))))) % 12.10/12.28 Clause #93 (by superposition #[85, 63]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.28 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 12.10/12.28 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a_1) a_2) False) % 12.10/12.28 (Or (Eq a (join_on_relstr (skS.0 6 a_1) a_2)) % 12.10/12.28 (Or (Eq (relstr_set_smaller (skS.0 6 a_1) a_2 a) False) % 12.10/12.28 (Or (Eq (related (skS.0 6 a_1) a (skS.0 3 (skS.0 6 a_1) a_2 a a_3)) False) (Eq False True))))) % 12.10/12.28 Clause #107 (by clausification #[83]): ∀ (a a_1 : Iota), % 12.10/12.30 Or (Eq (element (join_on_relstr (skS.0 6 a) a_1) (the_carrier (skS.0 6 a))) False) % 12.10/12.30 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.30 (Eq (relstr_set_smaller (skS.0 6 a) a_1 (join_on_relstr (skS.0 6 a) a_1)) True)) % 12.10/12.30 Clause #108 (by forward demodulation #[107, 71]): ∀ (a a_1 : Iota), % 12.10/12.30 Or (Eq True False) % 12.10/12.30 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.30 (Eq (relstr_set_smaller (skS.0 6 a) a_1 (join_on_relstr (skS.0 6 a) a_1)) True)) % 12.10/12.30 Clause #109 (by clausification #[108]): ∀ (a a_1 : Iota), % 12.10/12.30 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.30 (Eq (relstr_set_smaller (skS.0 6 a) a_1 (join_on_relstr (skS.0 6 a) a_1)) True) % 12.10/12.30 Clause #113 (by clausification #[62]): ∀ (a a_1 : Iota), % 12.10/12.30 Eq % 12.10/12.30 (Not % 12.10/12.30 (element (skS.0 7 a a_1) (the_carrier (skS.0 6 a)) → % 12.10/12.30 ∀ (C : Iota), % 12.10/12.30 And % 12.10/12.30 (And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C) → % 12.10/12.30 And (relstr_set_smaller (skS.0 6 a) C (skS.0 7 a a_1)) % 12.10/12.30 (∀ (D : Iota), % 12.10/12.30 element D (the_carrier (skS.0 6 a)) → % 12.10/12.30 relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.10/12.30 (And (relstr_set_smaller (skS.0 6 a) C (skS.0 7 a a_1)) % 12.10/12.30 (∀ (D : Iota), % 12.10/12.30 element D (the_carrier (skS.0 6 a)) → % 12.10/12.30 relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) (skS.0 7 a a_1) D) → % 12.10/12.30 And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C)))) % 12.10/12.30 True % 12.10/12.30 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), % 12.10/12.30 Eq % 12.10/12.30 (element (skS.0 7 a a_1) (the_carrier (skS.0 6 a)) → % 12.10/12.30 ∀ (C : Iota), % 12.10/12.30 And % 12.10/12.30 (And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C) → % 12.10/12.30 And (relstr_set_smaller (skS.0 6 a) C (skS.0 7 a a_1)) % 12.10/12.30 (∀ (D : Iota), % 12.10/12.30 element D (the_carrier (skS.0 6 a)) → % 12.10/12.30 relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.10/12.30 (And (relstr_set_smaller (skS.0 6 a) C (skS.0 7 a a_1)) % 12.10/12.30 (∀ (D : Iota), % 12.10/12.30 element D (the_carrier (skS.0 6 a)) → % 12.10/12.30 relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) (skS.0 7 a a_1) D) → % 12.10/12.30 And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C))) % 12.10/12.30 False % 12.10/12.30 Clause #115 (by clausification #[114]): ∀ (a a_1 : Iota), Eq (element (skS.0 7 a a_1) (the_carrier (skS.0 6 a))) True % 12.10/12.30 Clause #116 (by clausification #[114]): ∀ (a a_1 : Iota), % 12.10/12.30 Eq % 12.10/12.30 (∀ (C : Iota), % 12.10/12.30 And % 12.10/12.30 (And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C) → % 12.10/12.30 And (relstr_set_smaller (skS.0 6 a) C (skS.0 7 a a_1)) % 12.10/12.30 (∀ (D : Iota), % 12.10/12.30 element D (the_carrier (skS.0 6 a)) → % 12.10/12.30 relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.10/12.30 (And (relstr_set_smaller (skS.0 6 a) C (skS.0 7 a a_1)) % 12.10/12.30 (∀ (D : Iota), % 12.10/12.30 element D (the_carrier (skS.0 6 a)) → % 12.10/12.30 relstr_set_smaller (skS.0 6 a) C D → related (skS.0 6 a) (skS.0 7 a a_1) D) → % 12.10/12.30 And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) C)) (ex_sup_of_relstr_set (skS.0 6 a) C))) % 12.10/12.30 False % 12.10/12.30 Clause #117 (by clausification #[66]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.30 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 12.10/12.30 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a_1) a_2) False) % 12.10/12.30 (Or (Eq a (join_on_relstr (skS.0 6 a_1) a_2)) % 12.10/12.30 (Or (Eq (relstr_set_smaller (skS.0 6 a_1) a_2 a) False) % 12.10/12.30 (Eq (element (skS.0 3 (skS.0 6 a_1) a_2 a a_3) (the_carrier (skS.0 6 a_1))) True)))) % 12.10/12.30 Clause #119 (by superposition #[117, 115]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.30 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.30 (Or (Eq (skS.0 7 a a_2) (join_on_relstr (skS.0 6 a) a_1)) % 12.10/12.30 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.10/12.30 (Or (Eq (element (skS.0 3 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3) (the_carrier (skS.0 6 a))) True) % 12.10/12.32 (Eq False True)))) % 12.10/12.32 Clause #124 (by clausification #[68]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.32 Or (Eq (rel_str (skS.0 6 a)) False) % 12.10/12.32 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.32 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.32 (Eq (element (skS.0 4 (skS.0 6 a) a_1 a_2 a_3) (the_carrier (skS.0 6 a))) True)))) % 12.10/12.32 Clause #125 (by forward demodulation #[124, 63]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.32 Or (Eq True False) % 12.10/12.32 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.32 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.32 (Eq (element (skS.0 4 (skS.0 6 a) a_1 a_2 a_3) (the_carrier (skS.0 6 a))) True)))) % 12.10/12.32 Clause #126 (by clausification #[125]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.32 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.32 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.32 (Eq (element (skS.0 4 (skS.0 6 a) a_1 a_2 a_3) (the_carrier (skS.0 6 a))) True))) % 12.10/12.32 Clause #128 (by superposition #[126, 115]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.32 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.10/12.32 (Or (Eq (element (skS.0 4 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3) (the_carrier (skS.0 6 a))) True) (Eq False True))) % 12.10/12.32 Clause #130 (by clausification #[128]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.32 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.10/12.32 (Eq (element (skS.0 4 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3) (the_carrier (skS.0 6 a))) True)) % 12.10/12.32 Clause #132 (by clausification #[80]): ∀ (a a_1 a_2 : Iota), % 12.10/12.32 Or (Eq (element (join_on_relstr (skS.0 6 a) a_1) (the_carrier (skS.0 6 a))) False) % 12.10/12.32 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.32 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.32 (Eq (related (skS.0 6 a) (join_on_relstr (skS.0 6 a) a_1) a_2) True)))) % 12.10/12.32 Clause #133 (by forward demodulation #[132, 71]): ∀ (a a_1 a_2 : Iota), % 12.10/12.32 Or (Eq True False) % 12.10/12.32 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.32 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.32 (Eq (related (skS.0 6 a) (join_on_relstr (skS.0 6 a) a_1) a_2) True)))) % 12.10/12.32 Clause #134 (by clausification #[133]): ∀ (a a_1 a_2 : Iota), % 12.10/12.32 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.32 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.32 (Eq (related (skS.0 6 a) (join_on_relstr (skS.0 6 a) a_1) a_2) True))) % 12.10/12.32 Clause #138 (by clausification #[91]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.32 Or (Eq (rel_str (skS.0 6 a)) False) % 12.10/12.32 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.32 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.32 (Eq (related (skS.0 6 a) a_2 (skS.0 4 (skS.0 6 a) a_1 a_2 a_3)) False)))) % 12.10/12.32 Clause #139 (by forward demodulation #[138, 63]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.32 Or (Eq True False) % 12.10/12.32 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.32 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.32 (Eq (related (skS.0 6 a) a_2 (skS.0 4 (skS.0 6 a) a_1 a_2 a_3)) False)))) % 12.10/12.32 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.32 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.32 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.32 (Eq (related (skS.0 6 a) a_2 (skS.0 4 (skS.0 6 a) a_1 a_2 a_3)) False))) % 12.10/12.32 Clause #142 (by superposition #[140, 115]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.32 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.32 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.10/12.35 (Or (Eq (related (skS.0 6 a) (skS.0 7 a a_2) (skS.0 4 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3)) False) % 12.10/12.35 (Eq False True))) % 12.10/12.35 Clause #144 (by clausification #[90]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.35 Or (Eq (rel_str (skS.0 6 a)) False) % 12.10/12.35 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.35 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.35 (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 4 (skS.0 6 a) a_1 a_2 a_3)) True)))) % 12.10/12.35 Clause #145 (by forward demodulation #[144, 63]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.35 Or (Eq True False) % 12.10/12.35 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.35 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.35 (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 4 (skS.0 6 a) a_1 a_2 a_3)) True)))) % 12.10/12.35 Clause #146 (by clausification #[145]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.35 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.35 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 a_2) False) % 12.10/12.35 (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 4 (skS.0 6 a) a_1 a_2 a_3)) True))) % 12.10/12.35 Clause #148 (by superposition #[146, 115]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.35 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 4 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3)) True) (Eq False True))) % 12.10/12.35 Clause #150 (by clausification #[148]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.35 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.10/12.35 (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 4 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3)) True)) % 12.10/12.35 Clause #155 (by clausification #[87]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.35 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 12.10/12.35 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a_1) a_2) False) % 12.10/12.35 (Or (Eq a (join_on_relstr (skS.0 6 a_1) a_2)) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a_1) a_2 a) False) % 12.10/12.35 (Eq (relstr_set_smaller (skS.0 6 a_1) a_2 (skS.0 3 (skS.0 6 a_1) a_2 a a_3)) True)))) % 12.10/12.35 Clause #157 (by superposition #[155, 115]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.35 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.35 (Or (Eq (skS.0 7 a a_2) (join_on_relstr (skS.0 6 a) a_1)) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 3 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3)) True) % 12.10/12.35 (Eq False True)))) % 12.10/12.35 Clause #159 (by clausification #[93]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.35 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 12.10/12.35 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a_1) a_2) False) % 12.10/12.35 (Or (Eq a (join_on_relstr (skS.0 6 a_1) a_2)) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a_1) a_2 a) False) % 12.10/12.35 (Eq (related (skS.0 6 a_1) a (skS.0 3 (skS.0 6 a_1) a_2 a a_3)) False)))) % 12.10/12.35 Clause #161 (by superposition #[159, 115]): ∀ (a a_1 a_2 a_3 : Iota), % 12.10/12.35 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.10/12.35 (Or (Eq (skS.0 7 a a_2) (join_on_relstr (skS.0 6 a) a_1)) % 12.10/12.35 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.10/12.35 (Or (Eq (related (skS.0 6 a) (skS.0 7 a a_2) (skS.0 3 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3)) False) % 12.10/12.35 (Eq False True)))) % 12.10/12.35 Clause #166 (by clausification #[116]): ∀ (a a_1 a_2 : Iota), % 12.10/12.35 Eq % 12.10/12.35 (Not % 12.10/12.35 (And % 12.10/12.35 (And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.10/12.35 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) → % 12.10/12.35 And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.10/12.35 (∀ (D : Iota), % 12.10/12.35 element D (the_carrier (skS.0 6 a)) → % 12.10/12.35 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.10/12.35 (And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.10/12.35 (∀ (D : Iota), % 12.10/12.35 element D (the_carrier (skS.0 6 a)) → % 12.18/12.37 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D) → % 12.18/12.37 And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2))))) % 12.18/12.37 True % 12.18/12.37 Clause #167 (by clausification #[166]): ∀ (a a_1 a_2 : Iota), % 12.18/12.37 Eq % 12.18/12.37 (And % 12.18/12.37 (And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) → % 12.18/12.37 And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.18/12.37 (∀ (D : Iota), % 12.18/12.37 element D (the_carrier (skS.0 6 a)) → % 12.18/12.37 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.18/12.37 (And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.18/12.37 (∀ (D : Iota), % 12.18/12.37 element D (the_carrier (skS.0 6 a)) → % 12.18/12.37 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D) → % 12.18/12.37 And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)))) % 12.18/12.37 False % 12.18/12.37 Clause #168 (by clausification #[167]): ∀ (a a_1 a_2 : Iota), % 12.18/12.37 Or % 12.18/12.37 (Eq % 12.18/12.37 (And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) → % 12.18/12.37 And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.18/12.37 (∀ (D : Iota), % 12.18/12.37 element D (the_carrier (skS.0 6 a)) → % 12.18/12.37 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.18/12.37 False) % 12.18/12.37 (Eq % 12.18/12.37 (And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.18/12.37 (∀ (D : Iota), % 12.18/12.37 element D (the_carrier (skS.0 6 a)) → % 12.18/12.37 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D) → % 12.18/12.37 And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 False) % 12.18/12.37 Clause #169 (by clausification #[168]): ∀ (a a_1 a_2 : Iota), % 12.18/12.37 Or % 12.18/12.37 (Eq % 12.18/12.37 (And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.18/12.37 (∀ (D : Iota), % 12.18/12.37 element D (the_carrier (skS.0 6 a)) → % 12.18/12.37 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D) → % 12.18/12.37 And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 False) % 12.18/12.37 (Eq % 12.18/12.37 (And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 True) % 12.18/12.37 Clause #170 (by clausification #[168]): ∀ (a a_1 a_2 : Iota), % 12.18/12.37 Or % 12.18/12.37 (Eq % 12.18/12.37 (And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.18/12.37 (∀ (D : Iota), % 12.18/12.37 element D (the_carrier (skS.0 6 a)) → % 12.18/12.37 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D) → % 12.18/12.37 And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 False) % 12.18/12.37 (Eq % 12.18/12.37 (And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.18/12.37 (∀ (D : Iota), % 12.18/12.37 element D (the_carrier (skS.0 6 a)) → % 12.18/12.37 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.18/12.37 False) % 12.18/12.37 Clause #171 (by clausification #[169]): ∀ (a a_1 a_2 : Iota), % 12.18/12.37 Or % 12.18/12.37 (Eq % 12.18/12.37 (And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.18/12.37 True) % 12.18/12.37 (Eq % 12.18/12.37 (And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.18/12.37 (∀ (D : Iota), % 12.18/12.37 element D (the_carrier (skS.0 6 a)) → % 12.18/12.37 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.21/12.39 True) % 12.21/12.39 Clause #173 (by clausification #[171]): ∀ (a a_1 a_2 : Iota), % 12.21/12.39 Or % 12.21/12.39 (Eq % 12.21/12.39 (And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.21/12.39 (∀ (D : Iota), % 12.21/12.39 element D (the_carrier (skS.0 6 a)) → % 12.21/12.39 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.21/12.39 True) % 12.21/12.39 (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 Clause #174 (by clausification #[171]): ∀ (a a_1 a_2 : Iota), % 12.21/12.39 Or % 12.21/12.39 (Eq % 12.21/12.39 (And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.21/12.39 (∀ (D : Iota), % 12.21/12.39 element D (the_carrier (skS.0 6 a)) → % 12.21/12.39 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.21/12.39 True) % 12.21/12.39 (Eq (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) True) % 12.21/12.39 Clause #175 (by clausification #[173]): ∀ (a a_1 a_2 : Iota), % 12.21/12.39 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 (Eq % 12.21/12.39 (∀ (D : Iota), % 12.21/12.39 element D (the_carrier (skS.0 6 a)) → % 12.21/12.39 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D) % 12.21/12.39 True) % 12.21/12.39 Clause #176 (by clausification #[173]): ∀ (a a_1 a_2 : Iota), % 12.21/12.39 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) True) % 12.21/12.39 Clause #177 (by clausification #[175]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.39 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 (Eq % 12.21/12.39 (element a_3 (the_carrier (skS.0 6 a)) → % 12.21/12.39 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) a_3 → related (skS.0 6 a) (skS.0 7 a a_1) a_3) % 12.21/12.39 True) % 12.21/12.39 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.39 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 (Or (Eq (element a_3 (the_carrier (skS.0 6 a))) False) % 12.21/12.39 (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) a_3 → related (skS.0 6 a) (skS.0 7 a a_1) a_3) True)) % 12.21/12.39 Clause #179 (by clausification #[178]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.39 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 (Or (Eq (element a_3 (the_carrier (skS.0 6 a))) False) % 12.21/12.39 (Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) a_3) False) % 12.21/12.39 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) a_3) True))) % 12.21/12.39 Clause #183 (by superposition #[176, 130]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.39 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 (Or (Eq True False) % 12.21/12.39 (Eq (element (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3) (the_carrier (skS.0 6 a))) True))) % 12.21/12.39 Clause #184 (by superposition #[176, 150]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.39 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 (Or (Eq True False) % 12.21/12.39 (Eq % 12.21/12.39 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) % 12.21/12.39 (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) % 12.21/12.39 True))) % 12.21/12.39 Clause #185 (by clausification #[142]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.39 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) True) % 12.21/12.39 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.21/12.39 (Eq (related (skS.0 6 a) (skS.0 7 a a_2) (skS.0 4 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3)) False)) % 12.21/12.39 Clause #186 (by superposition #[185, 176]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.39 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.39 (Or (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) False) % 12.21/12.39 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) (Eq False True))) % 12.21/12.39 Clause #216 (by clausification #[174]): ∀ (a a_1 a_2 : Iota), % 12.21/12.39 Or (Eq (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) True) % 12.21/12.39 (Eq % 12.21/12.39 (∀ (D : Iota), % 12.21/12.39 element D (the_carrier (skS.0 6 a)) → % 12.21/12.42 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D) % 12.21/12.42 True) % 12.21/12.42 Clause #217 (by clausification #[174]): ∀ (a a_1 a_2 : Iota), % 12.21/12.42 Or (Eq (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) True) % 12.21/12.42 (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) True) % 12.21/12.42 Clause #218 (by clausification #[216]): ∀ (a a_1 a_2 : Iota), % 12.21/12.42 Or % 12.21/12.42 (Eq % 12.21/12.42 (∀ (D : Iota), % 12.21/12.42 element D (the_carrier (skS.0 6 a)) → % 12.21/12.42 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D) % 12.21/12.42 True) % 12.21/12.42 (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.21/12.42 Clause #219 (by clausification #[218]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.42 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.21/12.42 (Eq % 12.21/12.42 (element a_3 (the_carrier (skS.0 6 a)) → % 12.21/12.42 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) a_3 → related (skS.0 6 a) (skS.0 7 a a_1) a_3) % 12.21/12.42 True) % 12.21/12.42 Clause #220 (by clausification #[219]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.42 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.21/12.42 (Or (Eq (element a_3 (the_carrier (skS.0 6 a))) False) % 12.21/12.42 (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) a_3 → related (skS.0 6 a) (skS.0 7 a a_1) a_3) True)) % 12.21/12.42 Clause #221 (by clausification #[220]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.42 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.21/12.42 (Or (Eq (element a_3 (the_carrier (skS.0 6 a))) False) % 12.21/12.42 (Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) a_3) False) % 12.21/12.42 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) a_3) True))) % 12.21/12.42 Clause #228 (by clausification #[217]): ∀ (a a_1 a_2 : Iota), % 12.21/12.42 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) True) % 12.21/12.42 (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.21/12.42 Clause #239 (by clausification #[119]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.42 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.21/12.42 (Or (Eq (skS.0 7 a a_2) (join_on_relstr (skS.0 6 a) a_1)) % 12.21/12.42 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.21/12.42 (Eq (element (skS.0 3 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3) (the_carrier (skS.0 6 a))) True))) % 12.21/12.42 Clause #241 (by clausification #[157]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.42 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.21/12.42 (Or (Eq (skS.0 7 a a_2) (join_on_relstr (skS.0 6 a) a_1)) % 12.21/12.42 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.21/12.42 (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 3 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3)) True))) % 12.21/12.42 Clause #270 (by clausification #[183]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.42 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.42 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.42 (Eq (element (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3) (the_carrier (skS.0 6 a))) True)) % 12.21/12.42 Clause #271 (by eliminate duplicate literals #[270]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.42 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.42 (Eq (element (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3) (the_carrier (skS.0 6 a))) True) % 12.21/12.42 Clause #278 (by superposition #[271, 179]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.21/12.42 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.21/12.42 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_3 a_4)) True) % 12.21/12.42 (Or (Eq True False) % 12.21/12.42 (Or % 12.21/12.42 (Eq % 12.21/12.42 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_3 a_4) % 12.21/12.42 (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_5)) % 12.21/12.42 False) % 12.21/12.42 (Eq (related (skS.0 6 a) (skS.0 7 a a_3) (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_5)) % 12.21/12.42 True)))) % 12.21/12.42 Clause #292 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 12.21/12.42 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) a_1) False) % 12.21/12.42 (Or (Eq (skS.0 7 a a_2) (join_on_relstr (skS.0 6 a) a_1)) % 12.21/12.42 (Or (Eq (relstr_set_smaller (skS.0 6 a) a_1 (skS.0 7 a a_2)) False) % 12.21/12.42 (Eq (related (skS.0 6 a) (skS.0 7 a a_2) (skS.0 3 (skS.0 6 a) a_1 (skS.0 7 a a_2) a_3)) False))) % 12.27/12.44 Clause #318 (by clausification #[186]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.44 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.44 (Or (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) False) % 12.27/12.44 (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True)) % 12.27/12.44 Clause #319 (by eliminate duplicate literals #[318]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.44 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.44 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) False) % 12.27/12.44 Clause #322 (by clausification #[184]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.44 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.44 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.44 (Eq % 12.27/12.44 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) % 12.27/12.44 (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) % 12.27/12.44 True)) % 12.27/12.44 Clause #323 (by eliminate duplicate literals #[322]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.44 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.44 (Eq % 12.27/12.44 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) % 12.27/12.44 True) % 12.27/12.44 Clause #326 (by clausification #[170]): ∀ (a a_1 a_2 : Iota), % 12.27/12.44 Or % 12.27/12.44 (Eq % 12.27/12.44 (And (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) % 12.27/12.44 (∀ (D : Iota), % 12.27/12.44 element D (the_carrier (skS.0 6 a)) → % 12.27/12.44 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D)) % 12.27/12.44 False) % 12.27/12.44 (Eq % 12.27/12.44 (And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.44 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.44 False) % 12.27/12.44 Clause #358 (by clausification #[326]): ∀ (a a_1 a_2 : Iota), % 12.27/12.44 Or % 12.27/12.44 (Eq % 12.27/12.44 (And (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.44 (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.44 False) % 12.27/12.44 (Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.44 (Eq % 12.27/12.44 (∀ (D : Iota), % 12.27/12.44 element D (the_carrier (skS.0 6 a)) → % 12.27/12.44 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D) % 12.27/12.44 False)) % 12.27/12.44 Clause #359 (by clausification #[358]): ∀ (a a_1 a_2 : Iota), % 12.27/12.44 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.44 (Or % 12.27/12.44 (Eq % 12.27/12.44 (∀ (D : Iota), % 12.27/12.44 element D (the_carrier (skS.0 6 a)) → % 12.27/12.44 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) D → related (skS.0 6 a) (skS.0 7 a a_1) D) % 12.27/12.44 False) % 12.27/12.44 (Or (Eq (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) False) % 12.27/12.44 (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) False))) % 12.27/12.44 Clause #360 (by clausification #[359]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.44 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.44 (Or (Eq (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) False) % 12.27/12.44 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) False) % 12.27/12.44 (Eq % 12.27/12.44 (Not % 12.27/12.44 (element (skS.0 11 a a_1 a_2 a_3) (the_carrier (skS.0 6 a)) → % 12.27/12.44 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3) → % 12.27/12.44 related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3))) % 12.27/12.44 True))) % 12.27/12.44 Clause #361 (by clausification #[360]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.44 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.44 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) False) % 12.27/12.44 (Or % 12.27/12.44 (Eq % 12.27/12.44 (Not % 12.27/12.44 (element (skS.0 11 a a_1 a_2 a_3) (the_carrier (skS.0 6 a)) → % 12.27/12.44 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3) → % 12.27/12.44 related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3))) % 12.27/12.44 True) % 12.27/12.44 (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))))) % 12.27/12.46 Clause #362 (by clausification #[361]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.46 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.46 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) False) % 12.27/12.46 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.46 (Eq % 12.27/12.46 (element (skS.0 11 a a_1 a_2 a_3) (the_carrier (skS.0 6 a)) → % 12.27/12.46 relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3) → % 12.27/12.46 related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3)) % 12.27/12.46 False))) % 12.27/12.46 Clause #363 (by clausification #[362]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.46 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.46 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) False) % 12.27/12.46 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.46 (Eq (element (skS.0 11 a a_1 a_2 a_3) (the_carrier (skS.0 6 a))) True))) % 12.27/12.46 Clause #364 (by clausification #[362]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.46 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.46 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) False) % 12.27/12.46 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.46 (Eq % 12.27/12.46 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3) → % 12.27/12.46 related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3)) % 12.27/12.46 False))) % 12.27/12.46 Clause #382 (by clausification #[364]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.46 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.46 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) False) % 12.27/12.46 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.46 (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) True))) % 12.27/12.46 Clause #383 (by clausification #[364]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.46 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.46 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) False) % 12.27/12.46 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.46 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3)) False))) % 12.27/12.46 Clause #434 (by clausification #[278]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.27/12.46 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.46 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_3 a_4)) True) % 12.27/12.46 (Or % 12.27/12.46 (Eq % 12.27/12.46 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_3 a_4) % 12.27/12.46 (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_5)) % 12.27/12.46 False) % 12.27/12.46 (Eq (related (skS.0 6 a) (skS.0 7 a a_3) (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_5)) True))) % 12.27/12.46 Clause #435 (by superposition #[434, 323]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.46 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.46 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.46 (Or (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) True) % 12.27/12.46 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) (Eq False True)))) % 12.27/12.46 Clause #436 (by clausification #[435]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.46 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.46 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.46 (Or (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) True) % 12.27/12.46 (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True))) % 12.27/12.46 Clause #437 (by eliminate duplicate literals #[436]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.46 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.46 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 4 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) True) % 12.27/12.46 Clause #438 (by superposition #[437, 319]): ∀ (a a_1 a_2 : Iota), % 12.27/12.46 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.46 (Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) (Eq True False)) % 12.27/12.49 Clause #440 (by clausification #[438]): ∀ (a a_1 a_2 : Iota), % 12.27/12.49 Or (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.49 (Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True) % 12.27/12.49 Clause #441 (by eliminate duplicate literals #[440]): ∀ (a a_1 a_2 : Iota), Eq (ex_sup_of_relstr_set (skS.0 6 a) (skS.0 8 a a_1 a_2)) True % 12.27/12.49 Clause #449 (by backward demodulation #[441, 363]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.49 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.49 (Or (Eq True False) % 12.27/12.49 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.49 (Eq (element (skS.0 11 a a_1 a_2 a_3) (the_carrier (skS.0 6 a))) True))) % 12.27/12.49 Clause #450 (by backward demodulation #[441, 382]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.49 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.49 (Or (Eq True False) % 12.27/12.49 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.49 (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) True))) % 12.27/12.49 Clause #451 (by backward demodulation #[441, 383]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.49 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.49 (Or (Eq True False) % 12.27/12.49 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.49 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3)) False))) % 12.27/12.49 Clause #461 (by superposition #[441, 109]): ∀ (a a_1 a_2 : Iota), % 12.27/12.49 Or (Eq True False) % 12.27/12.49 (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) True) % 12.27/12.49 Clause #463 (by superposition #[441, 134]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.49 Or (Eq True False) % 12.27/12.49 (Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 12.27/12.49 (Or (Eq (relstr_set_smaller (skS.0 6 a_1) (skS.0 8 a_1 a_2 a_3) a) False) % 12.27/12.49 (Eq (related (skS.0 6 a_1) (join_on_relstr (skS.0 6 a_1) (skS.0 8 a_1 a_2 a_3)) a) True))) % 12.27/12.49 Clause #466 (by superposition #[441, 239]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.27/12.49 Or (Eq True False) % 12.27/12.49 (Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_2 a_3))) % 12.27/12.49 (Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1)) False) % 12.27/12.49 (Eq (element (skS.0 3 (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1) a_4) (the_carrier (skS.0 6 a))) True))) % 12.27/12.49 Clause #467 (by superposition #[441, 241]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.27/12.49 Or (Eq True False) % 12.27/12.49 (Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_2 a_3))) % 12.27/12.49 (Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1)) False) % 12.27/12.49 (Eq % 12.27/12.49 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_2 a_3) % 12.27/12.49 (skS.0 3 (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1) a_4)) % 12.27/12.49 True))) % 12.27/12.49 Clause #470 (by superposition #[441, 292]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.27/12.49 Or (Eq True False) % 12.27/12.49 (Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_2 a_3))) % 12.27/12.49 (Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1)) False) % 12.27/12.49 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1) a_4)) False))) % 12.27/12.49 Clause #481 (by clausification #[461]): ∀ (a a_1 a_2 : Iota), % 12.27/12.49 Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) True % 12.27/12.49 Clause #491 (by clausification #[463]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.49 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 12.27/12.49 (Or (Eq (relstr_set_smaller (skS.0 6 a_1) (skS.0 8 a_1 a_2 a_3) a) False) % 12.27/12.49 (Eq (related (skS.0 6 a_1) (join_on_relstr (skS.0 6 a_1) (skS.0 8 a_1 a_2 a_3)) a) True)) % 12.27/12.49 Clause #522 (by clausification #[449]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.49 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.27/12.49 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.27/12.49 (Eq (element (skS.0 11 a a_1 a_2 a_3) (the_carrier (skS.0 6 a))) True)) % 12.27/12.49 Clause #530 (by clausification #[451]): ∀ (a a_1 a_2 a_3 : Iota), % 12.27/12.49 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.34/12.51 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.51 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3)) False)) % 12.34/12.51 Clause #533 (by clausification #[450]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.51 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.34/12.51 (Or (Ne (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.51 (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) True)) % 12.34/12.51 Clause #553 (by clausification #[466]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.34/12.51 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_2 a_3))) % 12.34/12.51 (Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1)) False) % 12.34/12.51 (Eq (element (skS.0 3 (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1) a_4) (the_carrier (skS.0 6 a))) True)) % 12.34/12.51 Clause #554 (by superposition #[553, 228]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.51 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.51 (Or (Eq (element (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3) (the_carrier (skS.0 6 a))) True) % 12.34/12.51 (Or (Eq False True) (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))))) % 12.34/12.51 Clause #555 (by clausification #[554]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.51 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.51 (Or (Eq (element (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3) (the_carrier (skS.0 6 a))) True) % 12.34/12.51 (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2)))) % 12.34/12.51 Clause #556 (by eliminate duplicate literals #[555]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.51 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.51 (Eq (element (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3) (the_carrier (skS.0 6 a))) True) % 12.34/12.51 Clause #563 (by superposition #[556, 221]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.34/12.51 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.51 (Or (Eq (skS.0 7 a a_3) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_3 a_4))) % 12.34/12.51 (Or (Eq True False) % 12.34/12.51 (Or % 12.34/12.51 (Eq % 12.34/12.51 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_3 a_4) % 12.34/12.51 (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_5)) % 12.34/12.51 False) % 12.34/12.51 (Eq (related (skS.0 6 a) (skS.0 7 a a_3) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_5)) % 12.34/12.51 True)))) % 12.34/12.51 Clause #574 (by clausification #[470]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.34/12.51 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_2 a_3))) % 12.34/12.51 (Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1)) False) % 12.34/12.51 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1) a_4)) False)) % 12.34/12.51 Clause #575 (by superposition #[574, 228]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.51 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.51 (Or (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) False) % 12.34/12.51 (Or (Eq False True) (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))))) % 12.34/12.51 Clause #576 (by clausification #[575]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.51 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.51 (Or (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) False) % 12.34/12.51 (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2)))) % 12.34/12.51 Clause #577 (by eliminate duplicate literals #[576]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.51 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.51 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) False) % 12.34/12.51 Clause #583 (by clausification #[467]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.34/12.51 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_2 a_3))) % 12.34/12.51 (Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1)) False) % 12.34/12.51 (Eq % 12.34/12.51 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_2 a_3) % 12.34/12.51 (skS.0 3 (skS.0 6 a) (skS.0 8 a a_2 a_3) (skS.0 7 a a_1) a_4)) % 12.34/12.54 True)) % 12.34/12.54 Clause #584 (by superposition #[583, 228]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.54 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Or % 12.34/12.54 (Eq % 12.34/12.54 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) % 12.34/12.54 (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) % 12.34/12.54 True) % 12.34/12.54 (Or (Eq False True) (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))))) % 12.34/12.54 Clause #585 (by clausification #[584]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.54 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Or % 12.34/12.54 (Eq % 12.34/12.54 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) % 12.34/12.54 (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) % 12.34/12.54 True) % 12.34/12.54 (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2)))) % 12.34/12.54 Clause #586 (by eliminate duplicate literals #[585]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.54 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Eq % 12.34/12.54 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) % 12.34/12.54 True) % 12.34/12.54 Clause #646 (by clausification #[563]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.34/12.54 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Or (Eq (skS.0 7 a a_3) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_3 a_4))) % 12.34/12.54 (Or % 12.34/12.54 (Eq % 12.34/12.54 (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_3 a_4) % 12.34/12.54 (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_5)) % 12.34/12.54 False) % 12.34/12.54 (Eq (related (skS.0 6 a) (skS.0 7 a a_3) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_5)) True))) % 12.34/12.54 Clause #647 (by superposition #[646, 586]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.54 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Or (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) True) % 12.34/12.54 (Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) (Eq False True)))) % 12.34/12.54 Clause #648 (by clausification #[647]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.54 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Or (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) True) % 12.34/12.54 (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))))) % 12.34/12.54 Clause #649 (by eliminate duplicate literals #[648]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.54 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 3 (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1) a_3)) True) % 12.34/12.54 Clause #650 (by superposition #[649, 577]): ∀ (a a_1 a_2 : Iota), % 12.34/12.54 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) (Eq True False)) % 12.34/12.54 Clause #651 (by clausification #[650]): ∀ (a a_1 a_2 : Iota), % 12.34/12.54 Or (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 (Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2))) % 12.34/12.54 Clause #652 (by eliminate duplicate literals #[651]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 7 a a_1) (join_on_relstr (skS.0 6 a) (skS.0 8 a a_1 a_2)) % 12.34/12.54 Clause #658 (by backward demodulation #[652, 481]): ∀ (a a_1 a_2 : Iota), Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) True % 12.34/12.54 Clause #659 (by backward demodulation #[652, 491]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.54 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 12.34/12.54 (Or (Eq (relstr_set_smaller (skS.0 6 a_1) (skS.0 8 a_1 a_2 a_3) a) False) % 12.34/12.54 (Eq (related (skS.0 6 a_1) (skS.0 7 a_1 a_2) a) True)) % 12.34/12.54 Clause #696 (by backward contextual literal cutting #[652, 522]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.54 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.34/12.54 (Eq (element (skS.0 11 a a_1 a_2 a_3) (the_carrier (skS.0 6 a))) True) % 12.34/12.54 Clause #697 (by backward contextual literal cutting #[652, 530]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.56 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.34/12.56 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3)) False) % 12.34/12.56 Clause #698 (by backward contextual literal cutting #[652, 533]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.56 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) False) % 12.34/12.56 (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) True) % 12.34/12.56 Clause #712 (by superposition #[696, 658]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (element (skS.0 11 a a_1 a_2 a_3) (the_carrier (skS.0 6 a))) True) (Eq False True) % 12.34/12.56 Clause #715 (by clausification #[712]): ∀ (a a_1 a_2 a_3 : Iota), Eq (element (skS.0 11 a a_1 a_2 a_3) (the_carrier (skS.0 6 a))) True % 12.34/12.56 Clause #723 (by superposition #[715, 659]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.34/12.56 Or (Eq True False) % 12.34/12.56 (Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_3 a_4 a_5)) False) % 12.34/12.56 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_3 a_4 a_5)) True)) % 12.34/12.56 Clause #727 (by forward demodulation #[697, 658]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3)) False) % 12.34/12.56 Clause #728 (by clausification #[727]): ∀ (a a_1 a_2 a_3 : Iota), Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3)) False % 12.34/12.56 Clause #729 (by forward demodulation #[698, 658]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.56 Or (Eq True False) (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) True) % 12.34/12.56 Clause #730 (by clausification #[729]): ∀ (a a_1 a_2 a_3 : Iota), Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) True % 12.34/12.56 Clause #733 (by clausification #[723]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.34/12.56 Or (Eq (relstr_set_smaller (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 11 a a_3 a_4 a_5)) False) % 12.34/12.56 (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_3 a_4 a_5)) True) % 12.34/12.56 Clause #734 (by superposition #[733, 730]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3)) True) (Eq False True) % 12.34/12.56 Clause #735 (by clausification #[734]): ∀ (a a_1 a_2 a_3 : Iota), Eq (related (skS.0 6 a) (skS.0 7 a a_1) (skS.0 11 a a_1 a_2 a_3)) True % 12.34/12.56 Clause #736 (by superposition #[735, 728]): Eq True False % 12.34/12.56 Clause #737 (by clausification #[736]): False % 12.34/12.56 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------