%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU360+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.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 40.45s 40.67s % Output : Proof 40.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU360+1 : TPTP v9.2.0. Released v3.3.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n026.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 04:17:08 EDT 2025 % 0.13/0.34 % CPUTime : % 40.45/40.67 SZS status Theorem for theBenchmark.p % 40.45/40.67 SZS output start Proof for theBenchmark.p % 40.45/40.67 Clause #2 (by assumption #[]): Eq % 40.45/40.67 (∀ (A : Iota), % 40.45/40.67 rel_str A → % 40.45/40.67 Iff (lower_bounded_relstr A) % 40.45/40.67 (Exists fun B => And (element B (the_carrier A)) (relstr_element_smaller A (the_carrier A) B))) % 40.45/40.67 True % 40.45/40.67 Clause #3 (by assumption #[]): Eq % 40.45/40.67 (∀ (A : Iota), % 40.45/40.67 rel_str A → % 40.45/40.67 ∀ (B C : Iota), % 40.45/40.67 element C (the_carrier A) → % 40.45/40.67 Iff (relstr_element_smaller A B C) (∀ (D : Iota), element D (the_carrier A) → in D B → related A C D)) % 40.45/40.67 True % 40.45/40.67 Clause #5 (by assumption #[]): Eq (∀ (A : Iota), rel_str A → one_sorted_str A) True % 40.45/40.67 Clause #9 (by assumption #[]): Eq (∀ (A : Iota), And (Not (empty_carrier A)) (one_sorted_str A) → Not (empty (the_carrier A))) True % 40.45/40.67 Clause #15 (by assumption #[]): Eq % 40.45/40.67 (∀ (A : Iota), % 40.45/40.67 And (antisymmetric_relstr A) (rel_str A) → % 40.45/40.67 ∀ (B : Iota), % 40.45/40.67 Iff (ex_sup_of_relstr_set A B) % 40.45/40.67 (Exists fun C => % 40.45/40.67 And (And (element C (the_carrier A)) (relstr_set_smaller A B C)) % 40.45/40.67 (∀ (D : Iota), element D (the_carrier A) → relstr_set_smaller A B D → related A C D))) % 40.45/40.67 True % 40.45/40.67 Clause #16 (by assumption #[]): Eq % 40.45/40.67 (∀ (A : Iota), % 40.45/40.67 And (antisymmetric_relstr A) (rel_str A) → % 40.45/40.67 ∀ (B : Iota), % 40.45/40.67 Iff (ex_inf_of_relstr_set A B) % 40.45/40.67 (Exists fun C => % 40.45/40.67 And (And (element C (the_carrier A)) (relstr_element_smaller A B C)) % 40.45/40.67 (∀ (D : Iota), element D (the_carrier A) → relstr_element_smaller A B D → related A D C))) % 40.45/40.67 True % 40.45/40.67 Clause #18 (by assumption #[]): Eq (∀ (A B : Iota), element A B → Or (empty B) (in A B)) True % 40.45/40.67 Clause #19 (by assumption #[]): Eq % 40.45/40.67 (Not % 40.45/40.67 (∀ (A : Iota), % 40.45/40.67 And (And (And (Not (empty_carrier A)) (antisymmetric_relstr A)) (lower_bounded_relstr A)) (rel_str A) → % 40.45/40.67 And (ex_sup_of_relstr_set A empty_set) (ex_inf_of_relstr_set A (the_carrier A)))) % 40.45/40.67 True % 40.45/40.67 Clause #21 (by assumption #[]): Eq % 40.45/40.67 (∀ (A : Iota), % 40.45/40.67 rel_str A → % 40.45/40.67 ∀ (B : Iota), % 40.45/40.67 element B (the_carrier A) → And (relstr_set_smaller A empty_set B) (relstr_element_smaller A empty_set B)) % 40.45/40.67 True % 40.45/40.67 Clause #24 (by clausification #[5]): ∀ (a : Iota), Eq (rel_str a → one_sorted_str a) True % 40.45/40.67 Clause #25 (by clausification #[24]): ∀ (a : Iota), Or (Eq (rel_str a) False) (Eq (one_sorted_str a) True) % 40.45/40.67 Clause #42 (by clausification #[9]): ∀ (a : Iota), Eq (And (Not (empty_carrier a)) (one_sorted_str a) → Not (empty (the_carrier a))) True % 40.45/40.67 Clause #43 (by clausification #[42]): ∀ (a : Iota), Or (Eq (And (Not (empty_carrier a)) (one_sorted_str a)) False) (Eq (Not (empty (the_carrier a))) True) % 40.45/40.67 Clause #44 (by clausification #[43]): ∀ (a : Iota), % 40.45/40.67 Or (Eq (Not (empty (the_carrier a))) True) (Or (Eq (Not (empty_carrier a)) False) (Eq (one_sorted_str a) False)) % 40.45/40.67 Clause #45 (by clausification #[44]): ∀ (a : Iota), % 40.45/40.67 Or (Eq (Not (empty_carrier a)) False) (Or (Eq (one_sorted_str a) False) (Eq (empty (the_carrier a)) False)) % 40.45/40.67 Clause #46 (by clausification #[45]): ∀ (a : Iota), Or (Eq (one_sorted_str a) False) (Or (Eq (empty (the_carrier a)) False) (Eq (empty_carrier a) True)) % 40.45/40.67 Clause #53 (by clausification #[2]): ∀ (a : Iota), % 40.45/40.67 Eq % 40.45/40.67 (rel_str a → % 40.45/40.67 Iff (lower_bounded_relstr a) % 40.45/40.67 (Exists fun B => And (element B (the_carrier a)) (relstr_element_smaller a (the_carrier a) B))) % 40.45/40.67 True % 40.45/40.67 Clause #54 (by clausification #[53]): ∀ (a : Iota), % 40.45/40.67 Or (Eq (rel_str a) False) % 40.45/40.67 (Eq % 40.45/40.67 (Iff (lower_bounded_relstr a) % 40.45/40.67 (Exists fun B => And (element B (the_carrier a)) (relstr_element_smaller a (the_carrier a) B))) % 40.45/40.67 True) % 40.45/40.67 Clause #56 (by clausification #[54]): ∀ (a : Iota), % 40.45/40.67 Or (Eq (rel_str a) False) % 40.45/40.67 (Or (Eq (lower_bounded_relstr a) False) % 40.45/40.67 (Eq (Exists fun B => And (element B (the_carrier a)) (relstr_element_smaller a (the_carrier a) B)) True)) % 40.45/40.67 Clause #69 (by clausification #[3]): ∀ (a : Iota), % 40.45/40.67 Eq % 40.45/40.67 (rel_str a → % 40.45/40.67 ∀ (B C : Iota), % 40.45/40.67 element C (the_carrier a) → % 40.45/40.67 Iff (relstr_element_smaller a B C) (∀ (D : Iota), element D (the_carrier a) → in D B → related a C D)) % 40.45/40.67 True % 40.45/40.69 Clause #70 (by clausification #[69]): ∀ (a : Iota), % 40.45/40.69 Or (Eq (rel_str a) False) % 40.45/40.69 (Eq % 40.45/40.69 (∀ (B C : Iota), % 40.45/40.69 element C (the_carrier a) → % 40.45/40.69 Iff (relstr_element_smaller a B C) (∀ (D : Iota), element D (the_carrier a) → in D B → related a C D)) % 40.45/40.69 True) % 40.45/40.69 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), % 40.45/40.69 Or (Eq (rel_str a) False) % 40.45/40.69 (Eq % 40.45/40.69 (∀ (C : Iota), % 40.45/40.69 element C (the_carrier a) → % 40.45/40.69 Iff (relstr_element_smaller a a_1 C) (∀ (D : Iota), element D (the_carrier a) → in D a_1 → related a C D)) % 40.45/40.69 True) % 40.45/40.69 Clause #72 (by clausification #[71]): ∀ (a a_1 a_2 : Iota), % 40.45/40.69 Or (Eq (rel_str a) False) % 40.45/40.69 (Eq % 40.45/40.69 (element a_1 (the_carrier a) → % 40.45/40.69 Iff (relstr_element_smaller a a_2 a_1) (∀ (D : Iota), element D (the_carrier a) → in D a_2 → related a a_1 D)) % 40.45/40.69 True) % 40.45/40.69 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), % 40.45/40.69 Or (Eq (rel_str a) False) % 40.45/40.69 (Or (Eq (element a_1 (the_carrier a)) False) % 40.45/40.69 (Eq % 40.45/40.69 (Iff (relstr_element_smaller a a_2 a_1) (∀ (D : Iota), element D (the_carrier a) → in D a_2 → related a a_1 D)) % 40.45/40.69 True)) % 40.45/40.69 Clause #75 (by clausification #[73]): ∀ (a a_1 a_2 : Iota), % 40.45/40.69 Or (Eq (rel_str a) False) % 40.45/40.69 (Or (Eq (element a_1 (the_carrier a)) False) % 40.45/40.69 (Or (Eq (relstr_element_smaller a a_2 a_1) False) % 40.45/40.69 (Eq (∀ (D : Iota), element D (the_carrier a) → in D a_2 → related a a_1 D) True))) % 40.45/40.69 Clause #83 (by clausification #[18]): ∀ (a : Iota), Eq (∀ (B : Iota), element a B → Or (empty B) (in a B)) True % 40.45/40.69 Clause #84 (by clausification #[83]): ∀ (a a_1 : Iota), Eq (element a a_1 → Or (empty a_1) (in a a_1)) True % 40.45/40.69 Clause #85 (by clausification #[84]): ∀ (a a_1 : Iota), Or (Eq (element a a_1) False) (Eq (Or (empty a_1) (in a a_1)) True) % 40.45/40.69 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), Or (Eq (element a a_1) False) (Or (Eq (empty a_1) True) (Eq (in a a_1) True)) % 40.45/40.69 Clause #102 (by clausification #[19]): Eq % 40.45/40.69 (∀ (A : Iota), % 40.45/40.69 And (And (And (Not (empty_carrier A)) (antisymmetric_relstr A)) (lower_bounded_relstr A)) (rel_str A) → % 40.45/40.69 And (ex_sup_of_relstr_set A empty_set) (ex_inf_of_relstr_set A (the_carrier A))) % 40.45/40.69 False % 40.45/40.69 Clause #103 (by clausification #[102]): ∀ (a : Iota), % 40.45/40.69 Eq % 40.45/40.69 (Not % 40.45/40.69 (And % 40.45/40.69 (And (And (Not (empty_carrier (skS.0 8 a))) (antisymmetric_relstr (skS.0 8 a))) % 40.45/40.69 (lower_bounded_relstr (skS.0 8 a))) % 40.45/40.69 (rel_str (skS.0 8 a)) → % 40.45/40.69 And (ex_sup_of_relstr_set (skS.0 8 a) empty_set) (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a))))) % 40.45/40.69 True % 40.45/40.69 Clause #104 (by clausification #[103]): ∀ (a : Iota), % 40.45/40.69 Eq % 40.45/40.69 (And % 40.45/40.69 (And (And (Not (empty_carrier (skS.0 8 a))) (antisymmetric_relstr (skS.0 8 a))) % 40.45/40.69 (lower_bounded_relstr (skS.0 8 a))) % 40.45/40.69 (rel_str (skS.0 8 a)) → % 40.45/40.69 And (ex_sup_of_relstr_set (skS.0 8 a) empty_set) (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a)))) % 40.45/40.69 False % 40.45/40.69 Clause #105 (by clausification #[104]): ∀ (a : Iota), % 40.45/40.69 Eq % 40.45/40.69 (And % 40.45/40.69 (And (And (Not (empty_carrier (skS.0 8 a))) (antisymmetric_relstr (skS.0 8 a))) % 40.45/40.69 (lower_bounded_relstr (skS.0 8 a))) % 40.45/40.69 (rel_str (skS.0 8 a))) % 40.45/40.69 True % 40.45/40.69 Clause #106 (by clausification #[104]): ∀ (a : Iota), % 40.45/40.69 Eq (And (ex_sup_of_relstr_set (skS.0 8 a) empty_set) (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a)))) % 40.45/40.69 False % 40.45/40.69 Clause #107 (by clausification #[105]): ∀ (a : Iota), Eq (rel_str (skS.0 8 a)) True % 40.45/40.69 Clause #108 (by clausification #[105]): ∀ (a : Iota), % 40.45/40.69 Eq (And (And (Not (empty_carrier (skS.0 8 a))) (antisymmetric_relstr (skS.0 8 a))) (lower_bounded_relstr (skS.0 8 a))) % 40.45/40.69 True % 40.45/40.69 Clause #109 (by superposition #[107, 25]): ∀ (a : Iota), Or (Eq True False) (Eq (one_sorted_str (skS.0 8 a)) True) % 40.45/40.69 Clause #112 (by clausification #[109]): ∀ (a : Iota), Eq (one_sorted_str (skS.0 8 a)) True % 40.45/40.69 Clause #113 (by superposition #[112, 46]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (empty (the_carrier (skS.0 8 a))) False) (Eq (empty_carrier (skS.0 8 a)) True)) % 40.45/40.69 Clause #114 (by clausification #[21]): ∀ (a : Iota), % 40.45/40.69 Eq % 40.45/40.69 (rel_str a → % 40.45/40.69 ∀ (B : Iota), % 40.55/40.71 element B (the_carrier a) → And (relstr_set_smaller a empty_set B) (relstr_element_smaller a empty_set B)) % 40.55/40.71 True % 40.55/40.71 Clause #115 (by clausification #[114]): ∀ (a : Iota), % 40.55/40.71 Or (Eq (rel_str a) False) % 40.55/40.71 (Eq % 40.55/40.71 (∀ (B : Iota), % 40.55/40.71 element B (the_carrier a) → And (relstr_set_smaller a empty_set B) (relstr_element_smaller a empty_set B)) % 40.55/40.71 True) % 40.55/40.71 Clause #116 (by clausification #[115]): ∀ (a a_1 : Iota), % 40.55/40.71 Or (Eq (rel_str a) False) % 40.55/40.71 (Eq % 40.55/40.71 (element a_1 (the_carrier a) → And (relstr_set_smaller a empty_set a_1) (relstr_element_smaller a empty_set a_1)) % 40.55/40.71 True) % 40.55/40.71 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), % 40.55/40.71 Or (Eq (rel_str a) False) % 40.55/40.71 (Or (Eq (element a_1 (the_carrier a)) False) % 40.55/40.71 (Eq (And (relstr_set_smaller a empty_set a_1) (relstr_element_smaller a empty_set a_1)) True)) % 40.55/40.71 Clause #119 (by clausification #[117]): ∀ (a a_1 : Iota), % 40.55/40.71 Or (Eq (rel_str a) False) (Or (Eq (element a_1 (the_carrier a)) False) (Eq (relstr_set_smaller a empty_set a_1) True)) % 40.55/40.71 Clause #122 (by clausification #[15]): ∀ (a : Iota), % 40.55/40.71 Eq % 40.55/40.71 (And (antisymmetric_relstr a) (rel_str a) → % 40.55/40.71 ∀ (B : Iota), % 40.55/40.71 Iff (ex_sup_of_relstr_set a B) % 40.55/40.71 (Exists fun C => % 40.55/40.71 And (And (element C (the_carrier a)) (relstr_set_smaller a B C)) % 40.55/40.71 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a B D → related a C D))) % 40.55/40.71 True % 40.55/40.71 Clause #123 (by clausification #[122]): ∀ (a : Iota), % 40.55/40.71 Or (Eq (And (antisymmetric_relstr a) (rel_str a)) False) % 40.55/40.71 (Eq % 40.55/40.71 (∀ (B : Iota), % 40.55/40.71 Iff (ex_sup_of_relstr_set a B) % 40.55/40.71 (Exists fun C => % 40.55/40.71 And (And (element C (the_carrier a)) (relstr_set_smaller a B C)) % 40.55/40.71 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a B D → related a C D))) % 40.55/40.71 True) % 40.55/40.71 Clause #124 (by clausification #[123]): ∀ (a : Iota), % 40.55/40.71 Or % 40.55/40.71 (Eq % 40.55/40.71 (∀ (B : Iota), % 40.55/40.71 Iff (ex_sup_of_relstr_set a B) % 40.55/40.71 (Exists fun C => % 40.55/40.71 And (And (element C (the_carrier a)) (relstr_set_smaller a B C)) % 40.55/40.71 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a B D → related a C D))) % 40.55/40.71 True) % 40.55/40.71 (Or (Eq (antisymmetric_relstr a) False) (Eq (rel_str a) False)) % 40.55/40.71 Clause #125 (by clausification #[124]): ∀ (a a_1 : Iota), % 40.55/40.71 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.71 (Or (Eq (rel_str a) False) % 40.55/40.71 (Eq % 40.55/40.71 (Iff (ex_sup_of_relstr_set a a_1) % 40.55/40.71 (Exists fun C => % 40.55/40.71 And (And (element C (the_carrier a)) (relstr_set_smaller a a_1 C)) % 40.55/40.71 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a C D))) % 40.55/40.71 True)) % 40.55/40.71 Clause #126 (by clausification #[125]): ∀ (a a_1 : Iota), % 40.55/40.71 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.71 (Or (Eq (rel_str a) False) % 40.55/40.71 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 40.55/40.71 (Eq % 40.55/40.71 (Exists fun C => % 40.55/40.71 And (And (element C (the_carrier a)) (relstr_set_smaller a a_1 C)) % 40.55/40.71 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a C D)) % 40.55/40.71 False))) % 40.55/40.71 Clause #128 (by clausification #[126]): ∀ (a a_1 a_2 : Iota), % 40.55/40.71 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.71 (Or (Eq (rel_str a) False) % 40.55/40.71 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 40.55/40.71 (Eq % 40.55/40.71 (And (And (element a_2 (the_carrier a)) (relstr_set_smaller a a_1 a_2)) % 40.55/40.71 (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a a_2 D)) % 40.55/40.71 False))) % 40.55/40.71 Clause #129 (by clausification #[128]): ∀ (a a_1 a_2 : Iota), % 40.55/40.71 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.71 (Or (Eq (rel_str a) False) % 40.55/40.71 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 40.55/40.71 (Or (Eq (And (element a_2 (the_carrier a)) (relstr_set_smaller a a_1 a_2)) False) % 40.55/40.71 (Eq (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a a_2 D) False)))) % 40.55/40.71 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), % 40.55/40.71 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.71 (Or (Eq (rel_str a) False) % 40.55/40.71 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 40.55/40.71 (Or (Eq (∀ (D : Iota), element D (the_carrier a) → relstr_set_smaller a a_1 D → related a a_2 D) False) % 40.55/40.73 (Or (Eq (element a_2 (the_carrier a)) False) (Eq (relstr_set_smaller a a_1 a_2) False))))) % 40.55/40.73 Clause #131 (by clausification #[130]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.73 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.73 (Or (Eq (rel_str a) False) % 40.55/40.73 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 40.55/40.73 (Or (Eq (element a_2 (the_carrier a)) False) % 40.55/40.73 (Or (Eq (relstr_set_smaller a a_1 a_2) False) % 40.55/40.73 (Eq % 40.55/40.73 (Not % 40.55/40.73 (element (skS.0 9 a a_1 a_2 a_3) (the_carrier a) → % 40.55/40.73 relstr_set_smaller a a_1 (skS.0 9 a a_1 a_2 a_3) → related a a_2 (skS.0 9 a a_1 a_2 a_3))) % 40.55/40.73 True))))) % 40.55/40.73 Clause #132 (by clausification #[131]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.73 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.73 (Or (Eq (rel_str a) False) % 40.55/40.73 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 40.55/40.73 (Or (Eq (element a_2 (the_carrier a)) False) % 40.55/40.73 (Or (Eq (relstr_set_smaller a a_1 a_2) False) % 40.55/40.73 (Eq % 40.55/40.73 (element (skS.0 9 a a_1 a_2 a_3) (the_carrier a) → % 40.55/40.73 relstr_set_smaller a a_1 (skS.0 9 a a_1 a_2 a_3) → related a a_2 (skS.0 9 a a_1 a_2 a_3)) % 40.55/40.73 False))))) % 40.55/40.73 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.73 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.73 (Or (Eq (rel_str a) False) % 40.55/40.73 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 40.55/40.73 (Or (Eq (element a_2 (the_carrier a)) False) % 40.55/40.73 (Or (Eq (relstr_set_smaller a a_1 a_2) False) (Eq (element (skS.0 9 a a_1 a_2 a_3) (the_carrier a)) True))))) % 40.55/40.73 Clause #134 (by clausification #[132]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.73 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.73 (Or (Eq (rel_str a) False) % 40.55/40.73 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 40.55/40.73 (Or (Eq (element a_2 (the_carrier a)) False) % 40.55/40.73 (Or (Eq (relstr_set_smaller a a_1 a_2) False) % 40.55/40.73 (Eq (relstr_set_smaller a a_1 (skS.0 9 a a_1 a_2 a_3) → related a a_2 (skS.0 9 a a_1 a_2 a_3)) False))))) % 40.55/40.73 Clause #136 (by superposition #[119, 107]): ∀ (a a_1 : Iota), % 40.55/40.73 Or (Eq (element a (the_carrier (skS.0 8 a_1))) False) % 40.55/40.73 (Or (Eq (relstr_set_smaller (skS.0 8 a_1) empty_set a) True) (Eq False True)) % 40.55/40.73 Clause #149 (by clausification #[16]): ∀ (a : Iota), % 40.55/40.73 Eq % 40.55/40.73 (And (antisymmetric_relstr a) (rel_str a) → % 40.55/40.73 ∀ (B : Iota), % 40.55/40.73 Iff (ex_inf_of_relstr_set a B) % 40.55/40.73 (Exists fun C => % 40.55/40.73 And (And (element C (the_carrier a)) (relstr_element_smaller a B C)) % 40.55/40.73 (∀ (D : Iota), element D (the_carrier a) → relstr_element_smaller a B D → related a D C))) % 40.55/40.73 True % 40.55/40.73 Clause #150 (by clausification #[149]): ∀ (a : Iota), % 40.55/40.73 Or (Eq (And (antisymmetric_relstr a) (rel_str a)) False) % 40.55/40.73 (Eq % 40.55/40.73 (∀ (B : Iota), % 40.55/40.73 Iff (ex_inf_of_relstr_set a B) % 40.55/40.73 (Exists fun C => % 40.55/40.73 And (And (element C (the_carrier a)) (relstr_element_smaller a B C)) % 40.55/40.73 (∀ (D : Iota), element D (the_carrier a) → relstr_element_smaller a B D → related a D C))) % 40.55/40.73 True) % 40.55/40.73 Clause #151 (by clausification #[150]): ∀ (a : Iota), % 40.55/40.73 Or % 40.55/40.73 (Eq % 40.55/40.73 (∀ (B : Iota), % 40.55/40.73 Iff (ex_inf_of_relstr_set a B) % 40.55/40.73 (Exists fun C => % 40.55/40.73 And (And (element C (the_carrier a)) (relstr_element_smaller a B C)) % 40.55/40.73 (∀ (D : Iota), element D (the_carrier a) → relstr_element_smaller a B D → related a D C))) % 40.55/40.73 True) % 40.55/40.73 (Or (Eq (antisymmetric_relstr a) False) (Eq (rel_str a) False)) % 40.55/40.73 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), % 40.55/40.73 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.73 (Or (Eq (rel_str a) False) % 40.55/40.73 (Eq % 40.55/40.73 (Iff (ex_inf_of_relstr_set a a_1) % 40.55/40.73 (Exists fun C => % 40.55/40.73 And (And (element C (the_carrier a)) (relstr_element_smaller a a_1 C)) % 40.55/40.73 (∀ (D : Iota), element D (the_carrier a) → relstr_element_smaller a a_1 D → related a D C))) % 40.55/40.73 True)) % 40.55/40.73 Clause #153 (by clausification #[152]): ∀ (a a_1 : Iota), % 40.55/40.73 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.73 (Or (Eq (rel_str a) False) % 40.55/40.73 (Or (Eq (ex_inf_of_relstr_set a a_1) True) % 40.55/40.73 (Eq % 40.55/40.75 (Exists fun C => % 40.55/40.75 And (And (element C (the_carrier a)) (relstr_element_smaller a a_1 C)) % 40.55/40.75 (∀ (D : Iota), element D (the_carrier a) → relstr_element_smaller a a_1 D → related a D C)) % 40.55/40.75 False))) % 40.55/40.75 Clause #155 (by clausification #[153]): ∀ (a a_1 a_2 : Iota), % 40.55/40.75 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.75 (Or (Eq (rel_str a) False) % 40.55/40.75 (Or (Eq (ex_inf_of_relstr_set a a_1) True) % 40.55/40.75 (Eq % 40.55/40.75 (And (And (element a_2 (the_carrier a)) (relstr_element_smaller a a_1 a_2)) % 40.55/40.75 (∀ (D : Iota), element D (the_carrier a) → relstr_element_smaller a a_1 D → related a D a_2)) % 40.55/40.75 False))) % 40.55/40.75 Clause #156 (by clausification #[155]): ∀ (a a_1 a_2 : Iota), % 40.55/40.75 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.75 (Or (Eq (rel_str a) False) % 40.55/40.75 (Or (Eq (ex_inf_of_relstr_set a a_1) True) % 40.55/40.75 (Or (Eq (And (element a_2 (the_carrier a)) (relstr_element_smaller a a_1 a_2)) False) % 40.55/40.75 (Eq (∀ (D : Iota), element D (the_carrier a) → relstr_element_smaller a a_1 D → related a D a_2) False)))) % 40.55/40.75 Clause #157 (by clausification #[156]): ∀ (a a_1 a_2 : Iota), % 40.55/40.75 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.75 (Or (Eq (rel_str a) False) % 40.55/40.75 (Or (Eq (ex_inf_of_relstr_set a a_1) True) % 40.55/40.75 (Or (Eq (∀ (D : Iota), element D (the_carrier a) → relstr_element_smaller a a_1 D → related a D a_2) False) % 40.55/40.75 (Or (Eq (element a_2 (the_carrier a)) False) (Eq (relstr_element_smaller a a_1 a_2) False))))) % 40.55/40.75 Clause #158 (by clausification #[157]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.75 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.75 (Or (Eq (rel_str a) False) % 40.55/40.75 (Or (Eq (ex_inf_of_relstr_set a a_1) True) % 40.55/40.75 (Or (Eq (element a_2 (the_carrier a)) False) % 40.55/40.75 (Or (Eq (relstr_element_smaller a a_1 a_2) False) % 40.55/40.75 (Eq % 40.55/40.75 (Not % 40.55/40.75 (element (skS.0 10 a a_1 a_2 a_3) (the_carrier a) → % 40.55/40.75 relstr_element_smaller a a_1 (skS.0 10 a a_1 a_2 a_3) → related a (skS.0 10 a a_1 a_2 a_3) a_2)) % 40.55/40.75 True))))) % 40.55/40.75 Clause #159 (by clausification #[158]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.75 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.75 (Or (Eq (rel_str a) False) % 40.55/40.75 (Or (Eq (ex_inf_of_relstr_set a a_1) True) % 40.55/40.75 (Or (Eq (element a_2 (the_carrier a)) False) % 40.55/40.75 (Or (Eq (relstr_element_smaller a a_1 a_2) False) % 40.55/40.75 (Eq % 40.55/40.75 (element (skS.0 10 a a_1 a_2 a_3) (the_carrier a) → % 40.55/40.75 relstr_element_smaller a a_1 (skS.0 10 a a_1 a_2 a_3) → related a (skS.0 10 a a_1 a_2 a_3) a_2) % 40.55/40.75 False))))) % 40.55/40.75 Clause #160 (by clausification #[159]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.75 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.75 (Or (Eq (rel_str a) False) % 40.55/40.75 (Or (Eq (ex_inf_of_relstr_set a a_1) True) % 40.55/40.75 (Or (Eq (element a_2 (the_carrier a)) False) % 40.55/40.75 (Or (Eq (relstr_element_smaller a a_1 a_2) False) % 40.55/40.75 (Eq (element (skS.0 10 a a_1 a_2 a_3) (the_carrier a)) True))))) % 40.55/40.75 Clause #161 (by clausification #[159]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.75 Or (Eq (antisymmetric_relstr a) False) % 40.55/40.75 (Or (Eq (rel_str a) False) % 40.55/40.75 (Or (Eq (ex_inf_of_relstr_set a a_1) True) % 40.55/40.75 (Or (Eq (element a_2 (the_carrier a)) False) % 40.55/40.75 (Or (Eq (relstr_element_smaller a a_1 a_2) False) % 40.55/40.75 (Eq (relstr_element_smaller a a_1 (skS.0 10 a a_1 a_2 a_3) → related a (skS.0 10 a a_1 a_2 a_3) a_2) % 40.55/40.75 False))))) % 40.55/40.75 Clause #168 (by clausification #[113]): ∀ (a : Iota), Or (Eq (empty (the_carrier (skS.0 8 a))) False) (Eq (empty_carrier (skS.0 8 a)) True) % 40.55/40.75 Clause #169 (by clausification #[56]): ∀ (a a_1 : Iota), % 40.55/40.75 Or (Eq (rel_str a) False) % 40.55/40.75 (Or (Eq (lower_bounded_relstr a) False) % 40.55/40.75 (Eq (And (element (skS.0 11 a a_1) (the_carrier a)) (relstr_element_smaller a (the_carrier a) (skS.0 11 a a_1))) % 40.55/40.75 True)) % 40.55/40.75 Clause #170 (by clausification #[169]): ∀ (a a_1 : Iota), % 40.55/40.75 Or (Eq (rel_str a) False) % 40.55/40.75 (Or (Eq (lower_bounded_relstr a) False) (Eq (relstr_element_smaller a (the_carrier a) (skS.0 11 a a_1)) True)) % 40.55/40.75 Clause #171 (by clausification #[169]): ∀ (a a_1 : Iota), % 40.55/40.75 Or (Eq (rel_str a) False) % 40.55/40.75 (Or (Eq (lower_bounded_relstr a) False) (Eq (element (skS.0 11 a a_1) (the_carrier a)) True)) % 40.55/40.77 Clause #173 (by superposition #[170, 107]): ∀ (a a_1 : Iota), % 40.55/40.77 Or (Eq (lower_bounded_relstr (skS.0 8 a)) False) % 40.55/40.77 (Or (Eq (relstr_element_smaller (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1)) True) % 40.55/40.77 (Eq False True)) % 40.55/40.77 Clause #175 (by superposition #[171, 107]): ∀ (a a_1 : Iota), % 40.55/40.77 Or (Eq (lower_bounded_relstr (skS.0 8 a)) False) % 40.55/40.77 (Or (Eq (element (skS.0 11 (skS.0 8 a) a_1) (the_carrier (skS.0 8 a))) True) (Eq False True)) % 40.55/40.77 Clause #177 (by clausification #[75]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.77 Or (Eq (rel_str a) False) % 40.55/40.77 (Or (Eq (element a_1 (the_carrier a)) False) % 40.55/40.77 (Or (Eq (relstr_element_smaller a a_2 a_1) False) % 40.55/40.77 (Eq (element a_3 (the_carrier a) → in a_3 a_2 → related a a_1 a_3) True))) % 40.55/40.77 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.77 Or (Eq (rel_str a) False) % 40.55/40.77 (Or (Eq (element a_1 (the_carrier a)) False) % 40.55/40.77 (Or (Eq (relstr_element_smaller a a_2 a_1) False) % 40.55/40.77 (Or (Eq (element a_3 (the_carrier a)) False) (Eq (in a_3 a_2 → related a a_1 a_3) True)))) % 40.55/40.77 Clause #179 (by clausification #[178]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.77 Or (Eq (rel_str a) False) % 40.55/40.77 (Or (Eq (element a_1 (the_carrier a)) False) % 40.55/40.77 (Or (Eq (relstr_element_smaller a a_2 a_1) False) % 40.55/40.77 (Or (Eq (element a_3 (the_carrier a)) False) (Or (Eq (in a_3 a_2) False) (Eq (related a a_1 a_3) True))))) % 40.55/40.77 Clause #181 (by superposition #[179, 107]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.77 Or (Eq (element a (the_carrier (skS.0 8 a_1))) False) % 40.55/40.77 (Or (Eq (relstr_element_smaller (skS.0 8 a_1) a_2 a) False) % 40.55/40.77 (Or (Eq (element a_3 (the_carrier (skS.0 8 a_1))) False) % 40.55/40.77 (Or (Eq (in a_3 a_2) False) (Or (Eq (related (skS.0 8 a_1) a a_3) True) (Eq False True))))) % 40.55/40.77 Clause #190 (by clausification #[136]): ∀ (a a_1 : Iota), % 40.55/40.77 Or (Eq (element a (the_carrier (skS.0 8 a_1))) False) (Eq (relstr_set_smaller (skS.0 8 a_1) empty_set a) True) % 40.55/40.77 Clause #192 (by clausification #[106]): ∀ (a : Iota), % 40.55/40.77 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) False) % 40.55/40.77 (Eq (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a))) False) % 40.55/40.77 Clause #193 (by clausification #[108]): ∀ (a : Iota), Eq (lower_bounded_relstr (skS.0 8 a)) True % 40.55/40.77 Clause #194 (by clausification #[108]): ∀ (a : Iota), Eq (And (Not (empty_carrier (skS.0 8 a))) (antisymmetric_relstr (skS.0 8 a))) True % 40.55/40.77 Clause #195 (by clausification #[194]): ∀ (a : Iota), Eq (antisymmetric_relstr (skS.0 8 a)) True % 40.55/40.77 Clause #196 (by clausification #[194]): ∀ (a : Iota), Eq (Not (empty_carrier (skS.0 8 a))) True % 40.55/40.77 Clause #197 (by superposition #[195, 133]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.77 Or (Eq True False) % 40.55/40.77 (Or (Eq (rel_str (skS.0 8 a)) False) % 40.55/40.77 (Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.55/40.77 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.55/40.77 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 a_2) False) % 40.55/40.77 (Eq (element (skS.0 9 (skS.0 8 a) a_1 a_2 a_3) (the_carrier (skS.0 8 a))) True))))) % 40.55/40.77 Clause #198 (by superposition #[195, 160]): ∀ (a a_1 a_2 a_3 : Iota), % 40.55/40.77 Or (Eq True False) % 40.55/40.77 (Or (Eq (rel_str (skS.0 8 a)) False) % 40.55/40.77 (Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.55/40.77 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.55/40.77 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.55/40.77 (Eq (element (skS.0 10 (skS.0 8 a) a_1 a_2 a_3) (the_carrier (skS.0 8 a))) True))))) % 40.55/40.77 Clause #203 (by clausification #[196]): ∀ (a : Iota), Eq (empty_carrier (skS.0 8 a)) False % 40.55/40.77 Clause #204 (by backward demodulation #[203, 168]): ∀ (a : Iota), Or (Eq (empty (the_carrier (skS.0 8 a))) False) (Eq False True) % 40.55/40.77 Clause #205 (by clausification #[204]): ∀ (a : Iota), Eq (empty (the_carrier (skS.0 8 a))) False % 40.55/40.77 Clause #228 (by clausification #[175]): ∀ (a a_1 : Iota), % 40.55/40.77 Or (Eq (lower_bounded_relstr (skS.0 8 a)) False) % 40.55/40.77 (Eq (element (skS.0 11 (skS.0 8 a) a_1) (the_carrier (skS.0 8 a))) True) % 40.55/40.77 Clause #229 (by forward demodulation #[228, 193]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (element (skS.0 11 (skS.0 8 a) a_1) (the_carrier (skS.0 8 a))) True) % 40.64/40.80 Clause #230 (by clausification #[229]): ∀ (a a_1 : Iota), Eq (element (skS.0 11 (skS.0 8 a) a_1) (the_carrier (skS.0 8 a))) True % 40.64/40.80 Clause #232 (by superposition #[230, 190]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (relstr_set_smaller (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1)) True) % 40.64/40.80 Clause #233 (by superposition #[230, 86]): ∀ (a a_1 : Iota), % 40.64/40.80 Or (Eq True False) % 40.64/40.80 (Or (Eq (empty (the_carrier (skS.0 8 a))) True) (Eq (in (skS.0 11 (skS.0 8 a) a_1) (the_carrier (skS.0 8 a))) True)) % 40.64/40.80 Clause #236 (by clausification #[232]): ∀ (a a_1 : Iota), Eq (relstr_set_smaller (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1)) True % 40.64/40.80 Clause #239 (by clausification #[233]): ∀ (a a_1 : Iota), % 40.64/40.80 Or (Eq (empty (the_carrier (skS.0 8 a))) True) (Eq (in (skS.0 11 (skS.0 8 a) a_1) (the_carrier (skS.0 8 a))) True) % 40.64/40.80 Clause #240 (by forward demodulation #[239, 205]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (in (skS.0 11 (skS.0 8 a) a_1) (the_carrier (skS.0 8 a))) True) % 40.64/40.80 Clause #241 (by clausification #[240]): ∀ (a a_1 : Iota), Eq (in (skS.0 11 (skS.0 8 a) a_1) (the_carrier (skS.0 8 a))) True % 40.64/40.80 Clause #249 (by clausification #[134]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.80 Or (Eq (antisymmetric_relstr a) False) % 40.64/40.80 (Or (Eq (rel_str a) False) % 40.64/40.80 (Or (Eq (ex_sup_of_relstr_set a a_1) True) % 40.64/40.80 (Or (Eq (element a_2 (the_carrier a)) False) % 40.64/40.80 (Or (Eq (relstr_set_smaller a a_1 a_2) False) (Eq (related a a_2 (skS.0 9 a a_1 a_2 a_3)) False))))) % 40.64/40.80 Clause #251 (by superposition #[249, 195]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.80 Or (Eq (rel_str (skS.0 8 a)) False) % 40.64/40.80 (Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.80 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.80 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.80 (Or (Eq (related (skS.0 8 a) a_2 (skS.0 9 (skS.0 8 a) a_1 a_2 a_3)) False) (Eq False True))))) % 40.64/40.80 Clause #252 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.80 Or (Eq (antisymmetric_relstr a) False) % 40.64/40.80 (Or (Eq (rel_str a) False) % 40.64/40.80 (Or (Eq (ex_inf_of_relstr_set a a_1) True) % 40.64/40.80 (Or (Eq (element a_2 (the_carrier a)) False) % 40.64/40.80 (Or (Eq (relstr_element_smaller a a_1 a_2) False) % 40.64/40.80 (Eq (relstr_element_smaller a a_1 (skS.0 10 a a_1 a_2 a_3)) True))))) % 40.64/40.80 Clause #253 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.80 Or (Eq (antisymmetric_relstr a) False) % 40.64/40.80 (Or (Eq (rel_str a) False) % 40.64/40.80 (Or (Eq (ex_inf_of_relstr_set a a_1) True) % 40.64/40.80 (Or (Eq (element a_2 (the_carrier a)) False) % 40.64/40.80 (Or (Eq (relstr_element_smaller a a_1 a_2) False) (Eq (related a (skS.0 10 a a_1 a_2 a_3) a_2) False))))) % 40.64/40.80 Clause #254 (by superposition #[252, 195]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.80 Or (Eq (rel_str (skS.0 8 a)) False) % 40.64/40.80 (Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.80 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.80 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.80 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 10 (skS.0 8 a) a_1 a_2 a_3)) True) (Eq False True))))) % 40.64/40.80 Clause #255 (by superposition #[253, 195]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.80 Or (Eq (rel_str (skS.0 8 a)) False) % 40.64/40.80 (Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.80 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.80 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.80 (Or (Eq (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) a_1 a_2 a_3) a_2) False) (Eq False True))))) % 40.64/40.80 Clause #265 (by clausification #[173]): ∀ (a a_1 : Iota), % 40.64/40.80 Or (Eq (lower_bounded_relstr (skS.0 8 a)) False) % 40.64/40.80 (Eq (relstr_element_smaller (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1)) True) % 40.64/40.80 Clause #266 (by forward demodulation #[265, 193]): ∀ (a a_1 : Iota), % 40.64/40.80 Or (Eq True False) (Eq (relstr_element_smaller (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1)) True) % 40.64/40.80 Clause #267 (by clausification #[266]): ∀ (a a_1 : Iota), Eq (relstr_element_smaller (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1)) True % 40.64/40.80 Clause #282 (by clausification #[181]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.80 Or (Eq (element a (the_carrier (skS.0 8 a_1))) False) % 40.64/40.82 (Or (Eq (relstr_element_smaller (skS.0 8 a_1) a_2 a) False) % 40.64/40.82 (Or (Eq (element a_3 (the_carrier (skS.0 8 a_1))) False) % 40.64/40.82 (Or (Eq (in a_3 a_2) False) (Eq (related (skS.0 8 a_1) a a_3) True)))) % 40.64/40.82 Clause #283 (by superposition #[282, 230]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.82 Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.64/40.82 (Or (Eq (element a_3 (the_carrier (skS.0 8 a))) False) % 40.64/40.82 (Or (Eq (in a_3 a_1) False) (Or (Eq (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_2) a_3) True) (Eq False True)))) % 40.64/40.82 Clause #300 (by clausification #[197]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.82 Or (Eq (rel_str (skS.0 8 a)) False) % 40.64/40.82 (Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.82 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.82 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.82 (Eq (element (skS.0 9 (skS.0 8 a) a_1 a_2 a_3) (the_carrier (skS.0 8 a))) True)))) % 40.64/40.82 Clause #301 (by forward demodulation #[300, 107]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.82 Or (Eq True False) % 40.64/40.82 (Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.82 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.82 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.82 (Eq (element (skS.0 9 (skS.0 8 a) a_1 a_2 a_3) (the_carrier (skS.0 8 a))) True)))) % 40.64/40.82 Clause #302 (by clausification #[301]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.82 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.82 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.82 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.82 (Eq (element (skS.0 9 (skS.0 8 a) a_1 a_2 a_3) (the_carrier (skS.0 8 a))) True))) % 40.64/40.82 Clause #303 (by superposition #[302, 230]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.82 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.82 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.64/40.82 (Or (Eq (element (skS.0 9 (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2) a_3) (the_carrier (skS.0 8 a))) True) % 40.64/40.82 (Eq False True))) % 40.64/40.82 Clause #328 (by clausification #[198]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.82 Or (Eq (rel_str (skS.0 8 a)) False) % 40.64/40.82 (Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.82 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.82 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.82 (Eq (element (skS.0 10 (skS.0 8 a) a_1 a_2 a_3) (the_carrier (skS.0 8 a))) True)))) % 40.64/40.82 Clause #329 (by forward demodulation #[328, 107]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.82 Or (Eq True False) % 40.64/40.82 (Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.82 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.82 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.82 (Eq (element (skS.0 10 (skS.0 8 a) a_1 a_2 a_3) (the_carrier (skS.0 8 a))) True)))) % 40.64/40.82 Clause #330 (by clausification #[329]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.82 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.82 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.82 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.82 (Eq (element (skS.0 10 (skS.0 8 a) a_1 a_2 a_3) (the_carrier (skS.0 8 a))) True))) % 40.64/40.82 Clause #331 (by superposition #[330, 230]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.82 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.82 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.64/40.82 (Or (Eq (element (skS.0 10 (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2) a_3) (the_carrier (skS.0 8 a))) True) % 40.64/40.82 (Eq False True))) % 40.64/40.82 Clause #386 (by clausification #[283]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.82 Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.64/40.82 (Or (Eq (element a_3 (the_carrier (skS.0 8 a))) False) % 40.64/40.82 (Or (Eq (in a_3 a_1) False) (Eq (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_2) a_3) True))) % 40.64/40.82 Clause #388 (by superposition #[386, 267]): ∀ (a a_1 a_2 : Iota), % 40.64/40.82 Or (Eq (element a (the_carrier (skS.0 8 a_1))) False) % 40.64/40.82 (Or (Eq (in a (the_carrier (skS.0 8 a_1))) False) % 40.64/40.82 (Or (Eq (related (skS.0 8 a_1) (skS.0 11 (skS.0 8 a_1) a_2) a) True) (Eq False True))) % 40.64/40.82 Clause #398 (by clausification #[388]): ∀ (a a_1 a_2 : Iota), % 40.64/40.82 Or (Eq (element a (the_carrier (skS.0 8 a_1))) False) % 40.64/40.85 (Or (Eq (in a (the_carrier (skS.0 8 a_1))) False) (Eq (related (skS.0 8 a_1) (skS.0 11 (skS.0 8 a_1) a_2) a) True)) % 40.64/40.85 Clause #480 (by clausification #[255]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq (rel_str (skS.0 8 a)) False) % 40.64/40.85 (Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.85 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.85 (Eq (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) a_1 a_2 a_3) a_2) False)))) % 40.64/40.85 Clause #481 (by forward demodulation #[480, 107]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq True False) % 40.64/40.85 (Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.85 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.85 (Eq (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) a_1 a_2 a_3) a_2) False)))) % 40.64/40.85 Clause #482 (by clausification #[481]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.85 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.85 (Eq (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) a_1 a_2 a_3) a_2) False))) % 40.64/40.85 Clause #483 (by superposition #[482, 230]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.64/40.85 (Or % 40.64/40.85 (Eq (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2) a_3) (skS.0 11 (skS.0 8 a) a_2)) % 40.64/40.85 False) % 40.64/40.85 (Eq False True))) % 40.64/40.85 Clause #490 (by clausification #[254]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq (rel_str (skS.0 8 a)) False) % 40.64/40.85 (Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.85 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.85 (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 10 (skS.0 8 a) a_1 a_2 a_3)) True)))) % 40.64/40.85 Clause #491 (by forward demodulation #[490, 107]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq True False) % 40.64/40.85 (Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.85 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.85 (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 10 (skS.0 8 a) a_1 a_2 a_3)) True)))) % 40.64/40.85 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.85 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.85 (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 10 (skS.0 8 a) a_1 a_2 a_3)) True))) % 40.64/40.85 Clause #493 (by superposition #[492, 230]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.64/40.85 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 10 (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2) a_3)) True) % 40.64/40.85 (Eq False True))) % 40.64/40.85 Clause #500 (by clausification #[251]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq (rel_str (skS.0 8 a)) False) % 40.64/40.85 (Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.85 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.85 (Eq (related (skS.0 8 a) a_2 (skS.0 9 (skS.0 8 a) a_1 a_2 a_3)) False)))) % 40.64/40.85 Clause #501 (by forward demodulation #[500, 107]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq True False) % 40.64/40.85 (Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.85 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.85 (Eq (related (skS.0 8 a) a_2 (skS.0 9 (skS.0 8 a) a_1 a_2 a_3)) False)))) % 40.64/40.85 Clause #502 (by clausification #[501]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.85 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.85 (Or (Eq (element a_2 (the_carrier (skS.0 8 a))) False) % 40.64/40.85 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 a_2) False) % 40.64/40.85 (Eq (related (skS.0 8 a) a_2 (skS.0 9 (skS.0 8 a) a_1 a_2 a_3)) False))) % 40.64/40.87 Clause #503 (by superposition #[502, 230]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.87 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.87 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.64/40.87 (Or % 40.64/40.87 (Eq (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_2) (skS.0 9 (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2) a_3)) % 40.64/40.87 False) % 40.64/40.87 (Eq False True))) % 40.64/40.87 Clause #510 (by clausification #[303]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.87 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.87 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.64/40.87 (Eq (element (skS.0 9 (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2) a_3) (the_carrier (skS.0 8 a))) True)) % 40.64/40.87 Clause #511 (by superposition #[510, 236]): ∀ (a a_1 a_2 : Iota), % 40.64/40.87 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.64/40.87 (Or (Eq (element (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2) (the_carrier (skS.0 8 a))) True) % 40.64/40.87 (Eq False True)) % 40.64/40.87 Clause #513 (by clausification #[511]): ∀ (a a_1 a_2 : Iota), % 40.64/40.87 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.64/40.87 (Eq (element (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2) (the_carrier (skS.0 8 a))) True) % 40.64/40.87 Clause #523 (by superposition #[513, 398]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.87 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.64/40.87 (Or (Eq True False) % 40.64/40.87 (Or (Eq (in (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2) (the_carrier (skS.0 8 a))) False) % 40.64/40.87 (Eq % 40.64/40.87 (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_3) % 40.64/40.87 (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2)) % 40.64/40.87 True))) % 40.64/40.87 Clause #529 (by superposition #[513, 86]): ∀ (a a_1 a_2 : Iota), % 40.64/40.87 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.64/40.87 (Or (Eq True False) % 40.64/40.87 (Or (Eq (empty (the_carrier (skS.0 8 a))) True) % 40.64/40.87 (Eq (in (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2) (the_carrier (skS.0 8 a))) True))) % 40.64/40.87 Clause #532 (by clausification #[529]): ∀ (a a_1 a_2 : Iota), % 40.64/40.87 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.64/40.87 (Or (Eq (empty (the_carrier (skS.0 8 a))) True) % 40.64/40.87 (Eq (in (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2) (the_carrier (skS.0 8 a))) True)) % 40.64/40.87 Clause #533 (by forward demodulation #[532, 205]): ∀ (a a_1 a_2 : Iota), % 40.64/40.87 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.64/40.87 (Or (Eq False True) % 40.64/40.87 (Eq (in (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2) (the_carrier (skS.0 8 a))) True)) % 40.64/40.87 Clause #534 (by clausification #[533]): ∀ (a a_1 a_2 : Iota), % 40.64/40.87 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.64/40.87 (Eq (in (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2) (the_carrier (skS.0 8 a))) True) % 40.64/40.87 Clause #553 (by clausification #[493]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.87 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.87 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.64/40.87 (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 10 (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2) a_3)) True)) % 40.64/40.87 Clause #555 (by superposition #[553, 267]): ∀ (a a_1 a_2 : Iota), % 40.64/40.87 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a))) True) % 40.64/40.87 (Or % 40.64/40.87 (Eq % 40.64/40.87 (relstr_element_smaller (skS.0 8 a) (the_carrier (skS.0 8 a)) % 40.64/40.87 (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2)) % 40.64/40.87 True) % 40.64/40.87 (Eq False True)) % 40.64/40.87 Clause #585 (by clausification #[555]): ∀ (a a_1 a_2 : Iota), % 40.64/40.87 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a))) True) % 40.64/40.87 (Eq % 40.64/40.87 (relstr_element_smaller (skS.0 8 a) (the_carrier (skS.0 8 a)) % 40.64/40.87 (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2)) % 40.64/40.87 True) % 40.64/40.87 Clause #586 (by clausification #[331]): ∀ (a a_1 a_2 a_3 : Iota), % 40.64/40.87 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.64/40.87 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.64/40.87 (Eq (element (skS.0 10 (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2) a_3) (the_carrier (skS.0 8 a))) True)) % 40.73/40.90 Clause #588 (by superposition #[586, 267]): ∀ (a a_1 a_2 : Iota), % 40.73/40.90 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a))) True) % 40.73/40.90 (Or % 40.73/40.90 (Eq % 40.73/40.90 (element (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2) % 40.73/40.90 (the_carrier (skS.0 8 a))) % 40.73/40.90 True) % 40.73/40.90 (Eq False True)) % 40.73/40.90 Clause #617 (by clausification #[588]): ∀ (a a_1 a_2 : Iota), % 40.73/40.90 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a))) True) % 40.73/40.90 (Eq % 40.73/40.90 (element (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2) % 40.73/40.90 (the_carrier (skS.0 8 a))) % 40.73/40.90 True) % 40.73/40.90 Clause #744 (by clausification #[483]): ∀ (a a_1 a_2 a_3 : Iota), % 40.73/40.90 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) a_1) True) % 40.73/40.90 (Or (Eq (relstr_element_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.73/40.90 (Eq (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2) a_3) (skS.0 11 (skS.0 8 a) a_2)) % 40.73/40.90 False)) % 40.73/40.90 Clause #746 (by superposition #[744, 267]): ∀ (a a_1 a_2 : Iota), % 40.73/40.90 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a))) True) % 40.73/40.90 (Or % 40.73/40.90 (Eq % 40.73/40.90 (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2) % 40.73/40.90 (skS.0 11 (skS.0 8 a) a_1)) % 40.73/40.90 False) % 40.73/40.90 (Eq False True)) % 40.73/40.90 Clause #751 (by clausification #[746]): ∀ (a a_1 a_2 : Iota), % 40.73/40.90 Or (Eq (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a))) True) % 40.73/40.90 (Eq % 40.73/40.90 (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2) % 40.73/40.90 (skS.0 11 (skS.0 8 a) a_1)) % 40.73/40.90 False) % 40.73/40.90 Clause #752 (by clausification #[503]): ∀ (a a_1 a_2 a_3 : Iota), % 40.73/40.90 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) a_1) True) % 40.73/40.90 (Or (Eq (relstr_set_smaller (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2)) False) % 40.73/40.90 (Eq (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_2) (skS.0 9 (skS.0 8 a) a_1 (skS.0 11 (skS.0 8 a) a_2) a_3)) % 40.73/40.90 False)) % 40.73/40.90 Clause #753 (by superposition #[752, 236]): ∀ (a a_1 a_2 : Iota), % 40.73/40.90 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.73/40.90 (Or % 40.73/40.90 (Eq % 40.73/40.90 (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_1) (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2)) % 40.73/40.90 False) % 40.73/40.90 (Eq False True)) % 40.73/40.90 Clause #754 (by clausification #[753]): ∀ (a a_1 a_2 : Iota), % 40.73/40.90 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.73/40.90 (Eq (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_1) (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2)) % 40.73/40.90 False) % 40.73/40.90 Clause #934 (by clausification #[523]): ∀ (a a_1 a_2 a_3 : Iota), % 40.73/40.90 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.73/40.90 (Or (Eq (in (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2) (the_carrier (skS.0 8 a))) False) % 40.73/40.90 (Eq % 40.73/40.90 (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_3) (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_1) a_2)) % 40.73/40.90 True)) % 40.73/40.90 Clause #935 (by superposition #[934, 534]): ∀ (a a_1 a_2 a_3 : Iota), % 40.73/40.90 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.73/40.90 (Or % 40.73/40.90 (Eq % 40.73/40.90 (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_1) (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_2) a_3)) % 40.73/40.90 True) % 40.73/40.90 (Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) (Eq False True))) % 40.73/40.90 Clause #936 (by clausification #[935]): ∀ (a a_1 a_2 a_3 : Iota), % 40.73/40.90 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.73/40.90 (Or % 40.73/40.90 (Eq % 40.73/40.90 (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_1) (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_2) a_3)) % 40.73/40.90 True) % 40.73/40.90 (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True)) % 40.73/40.90 Clause #937 (by eliminate duplicate literals #[936]): ∀ (a a_1 a_2 a_3 : Iota), % 40.73/40.90 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.73/40.90 (Eq (related (skS.0 8 a) (skS.0 11 (skS.0 8 a) a_1) (skS.0 9 (skS.0 8 a) empty_set (skS.0 11 (skS.0 8 a) a_2) a_3)) % 40.73/40.90 True) % 40.73/40.90 Clause #938 (by superposition #[937, 754]): ∀ (a : Iota), % 40.73/40.90 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.73/40.90 (Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) (Eq True False)) % 40.75/40.92 Clause #939 (by clausification #[938]): ∀ (a : Iota), % 40.75/40.92 Or (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) (Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True) % 40.75/40.92 Clause #940 (by eliminate duplicate literals #[939]): ∀ (a : Iota), Eq (ex_sup_of_relstr_set (skS.0 8 a) empty_set) True % 40.75/40.92 Clause #941 (by backward demodulation #[940, 192]): ∀ (a : Iota), Or (Eq True False) (Eq (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a))) False) % 40.75/40.92 Clause #969 (by clausification #[941]): ∀ (a : Iota), Eq (ex_inf_of_relstr_set (skS.0 8 a) (the_carrier (skS.0 8 a))) False % 40.75/40.92 Clause #970 (by backward demodulation #[969, 585]): ∀ (a a_1 a_2 : Iota), % 40.75/40.92 Or (Eq False True) % 40.75/40.92 (Eq % 40.75/40.92 (relstr_element_smaller (skS.0 8 a) (the_carrier (skS.0 8 a)) % 40.75/40.92 (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2)) % 40.75/40.92 True) % 40.75/40.92 Clause #971 (by backward demodulation #[969, 617]): ∀ (a a_1 a_2 : Iota), % 40.75/40.92 Or (Eq False True) % 40.75/40.92 (Eq % 40.75/40.92 (element (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2) % 40.75/40.92 (the_carrier (skS.0 8 a))) % 40.75/40.92 True) % 40.75/40.92 Clause #976 (by backward demodulation #[969, 751]): ∀ (a a_1 a_2 : Iota), % 40.75/40.92 Or (Eq False True) % 40.75/40.92 (Eq % 40.75/40.92 (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2) % 40.75/40.92 (skS.0 11 (skS.0 8 a) a_1)) % 40.75/40.92 False) % 40.75/40.92 Clause #1012 (by clausification #[971]): ∀ (a a_1 a_2 : Iota), % 40.75/40.92 Eq (element (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2) (the_carrier (skS.0 8 a))) % 40.75/40.92 True % 40.75/40.92 Clause #1017 (by superposition #[1012, 282]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 40.75/40.92 Or (Eq True False) % 40.75/40.92 (Or % 40.75/40.92 (Eq % 40.75/40.92 (relstr_element_smaller (skS.0 8 a) a_1 % 40.75/40.92 (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_2) a_3)) % 40.75/40.92 False) % 40.75/40.92 (Or (Eq (element a_4 (the_carrier (skS.0 8 a))) False) % 40.75/40.92 (Or (Eq (in a_4 a_1) False) % 40.75/40.92 (Eq (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_2) a_3) a_4) % 40.75/40.92 True)))) % 40.75/40.92 Clause #1055 (by clausification #[970]): ∀ (a a_1 a_2 : Iota), % 40.75/40.92 Eq % 40.75/40.92 (relstr_element_smaller (skS.0 8 a) (the_carrier (skS.0 8 a)) % 40.75/40.92 (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2)) % 40.75/40.92 True % 40.75/40.92 Clause #1062 (by clausification #[976]): ∀ (a a_1 a_2 : Iota), % 40.75/40.92 Eq % 40.75/40.92 (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2) % 40.75/40.92 (skS.0 11 (skS.0 8 a) a_1)) % 40.75/40.92 False % 40.75/40.92 Clause #1520 (by clausification #[1017]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 40.75/40.92 Or % 40.75/40.92 (Eq % 40.75/40.92 (relstr_element_smaller (skS.0 8 a) a_1 % 40.75/40.92 (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_2) a_3)) % 40.75/40.92 False) % 40.75/40.92 (Or (Eq (element a_4 (the_carrier (skS.0 8 a))) False) % 40.75/40.92 (Or (Eq (in a_4 a_1) False) % 40.75/40.92 (Eq (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_2) a_3) a_4) % 40.75/40.92 True))) % 40.75/40.92 Clause #1522 (by superposition #[1520, 1055]): ∀ (a a_1 a_2 a_3 : Iota), % 40.75/40.92 Or (Eq (element a (the_carrier (skS.0 8 a_1))) False) % 40.75/40.92 (Or (Eq (in a (the_carrier (skS.0 8 a_1))) False) % 40.75/40.92 (Or % 40.75/40.92 (Eq % 40.75/40.92 (related (skS.0 8 a_1) (skS.0 10 (skS.0 8 a_1) (the_carrier (skS.0 8 a_1)) (skS.0 11 (skS.0 8 a_1) a_2) a_3) % 40.75/40.92 a) % 40.75/40.92 True) % 40.75/40.92 (Eq False True))) % 40.75/40.92 Clause #1568 (by clausification #[1522]): ∀ (a a_1 a_2 a_3 : Iota), % 40.75/40.92 Or (Eq (element a (the_carrier (skS.0 8 a_1))) False) % 40.75/40.92 (Or (Eq (in a (the_carrier (skS.0 8 a_1))) False) % 40.75/40.92 (Eq % 40.75/40.92 (related (skS.0 8 a_1) (skS.0 10 (skS.0 8 a_1) (the_carrier (skS.0 8 a_1)) (skS.0 11 (skS.0 8 a_1) a_2) a_3) a) % 40.75/40.92 True)) % 40.75/40.92 Clause #1569 (by superposition #[1568, 230]): ∀ (a a_1 a_2 a_3 : Iota), % 40.75/40.92 Or (Eq (in (skS.0 11 (skS.0 8 a) a_1) (the_carrier (skS.0 8 a))) False) % 40.75/40.92 (Or % 40.75/40.92 (Eq % 40.75/40.92 (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_2) a_3) % 40.75/40.92 (skS.0 11 (skS.0 8 a) a_1)) % 40.75/40.92 True) % 40.75/40.92 (Eq False True)) % 40.75/40.92 Clause #1601 (by clausification #[1569]): ∀ (a a_1 a_2 a_3 : Iota), % 40.75/40.94 Or (Eq (in (skS.0 11 (skS.0 8 a) a_1) (the_carrier (skS.0 8 a))) False) % 40.75/40.94 (Eq % 40.75/40.94 (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_2) a_3) % 40.75/40.94 (skS.0 11 (skS.0 8 a) a_1)) % 40.75/40.94 True) % 40.75/40.94 Clause #1602 (by forward demodulation #[1601, 241]): ∀ (a a_1 a_2 a_3 : Iota), % 40.75/40.94 Or (Eq True False) % 40.75/40.94 (Eq % 40.75/40.94 (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2) % 40.75/40.94 (skS.0 11 (skS.0 8 a) a_3)) % 40.75/40.94 True) % 40.75/40.94 Clause #1603 (by clausification #[1602]): ∀ (a a_1 a_2 a_3 : Iota), % 40.75/40.94 Eq % 40.75/40.94 (related (skS.0 8 a) (skS.0 10 (skS.0 8 a) (the_carrier (skS.0 8 a)) (skS.0 11 (skS.0 8 a) a_1) a_2) % 40.75/40.94 (skS.0 11 (skS.0 8 a) a_3)) % 40.75/40.94 True % 40.75/40.94 Clause #1604 (by superposition #[1603, 1062]): Eq True False % 40.75/40.94 Clause #1605 (by clausification #[1604]): False % 40.75/40.94 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------