%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU305+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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:21 PM UTC 2025 % Result : Theorem 74.18s 74.37s % Output : Proof 74.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU305+1 : TPTP v9.2.0. Released v3.3.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n019.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 05:52:38 EDT 2025 % 0.13/0.34 % CPUTime : % 74.18/74.37 SZS status Theorem for theBenchmark.p % 74.18/74.37 SZS output start Proof for theBenchmark.p % 74.18/74.37 Clause #3 (by assumption #[]): Eq % 74.18/74.37 (∀ (A B C : Iota), % 74.18/74.37 And (And (And (And (Not (empty_carrier A)) (join_commutative A)) (join_semilatt_str A)) (element B (the_carrier A))) % 74.18/74.37 (element C (the_carrier A)) → % 74.18/74.37 Eq (join_commut A B C) (join_commut A C B)) % 74.18/74.37 True % 74.18/74.37 Clause #5 (by assumption #[]): Eq % 74.18/74.37 (∀ (A : Iota), % 74.18/74.37 And (Not (empty_carrier A)) (join_semilatt_str A) → % 74.18/74.37 ∀ (B : Iota), % 74.18/74.37 element B (the_carrier A) → ∀ (C : Iota), element C (the_carrier A) → Iff (below A B C) (Eq (join A B C) C)) % 74.18/74.37 True % 74.18/74.37 Clause #23 (by assumption #[]): Eq % 74.18/74.37 (∀ (A B C : Iota), % 74.18/74.37 And (And (And (And (Not (empty_carrier A)) (join_commutative A)) (join_semilatt_str A)) (element B (the_carrier A))) % 74.18/74.37 (element C (the_carrier A)) → % 74.18/74.37 Eq (join_commut A B C) (join A B C)) % 74.18/74.37 True % 74.18/74.37 Clause #27 (by assumption #[]): Eq % 74.18/74.37 (Not % 74.18/74.37 (∀ (A : Iota), % 74.18/74.37 And (And (Not (empty_carrier A)) (join_commutative A)) (join_semilatt_str A) → % 74.18/74.37 ∀ (B : Iota), % 74.18/74.37 element B (the_carrier A) → % 74.18/74.37 ∀ (C : Iota), element C (the_carrier A) → And (below A B C) (below A C B) → Eq B C)) % 74.18/74.37 True % 74.18/74.37 Clause #85 (by clausification #[3]): ∀ (a : Iota), % 74.18/74.37 Eq % 74.18/74.37 (∀ (B C : Iota), % 74.18/74.37 And % 74.18/74.37 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) % 74.18/74.37 (element B (the_carrier a))) % 74.18/74.37 (element C (the_carrier a)) → % 74.18/74.37 Eq (join_commut a B C) (join_commut a C B)) % 74.18/74.37 True % 74.18/74.37 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), % 74.18/74.37 Eq % 74.18/74.37 (∀ (C : Iota), % 74.18/74.37 And % 74.18/74.37 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) % 74.18/74.37 (element a_1 (the_carrier a))) % 74.18/74.37 (element C (the_carrier a)) → % 74.18/74.37 Eq (join_commut a a_1 C) (join_commut a C a_1)) % 74.18/74.37 True % 74.18/74.37 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 : Iota), % 74.18/74.37 Eq % 74.18/74.37 (And % 74.18/74.37 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) % 74.18/74.37 (element a_1 (the_carrier a))) % 74.18/74.37 (element a_2 (the_carrier a)) → % 74.18/74.37 Eq (join_commut a a_1 a_2) (join_commut a a_2 a_1)) % 74.18/74.37 True % 74.18/74.37 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 : Iota), % 74.18/74.37 Or % 74.18/74.37 (Eq % 74.18/74.37 (And % 74.18/74.37 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) % 74.18/74.37 (element a_1 (the_carrier a))) % 74.18/74.37 (element a_2 (the_carrier a))) % 74.18/74.37 False) % 74.18/74.37 (Eq (Eq (join_commut a a_1 a_2) (join_commut a a_2 a_1)) True) % 74.18/74.37 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 : Iota), % 74.18/74.37 Or (Eq (Eq (join_commut a a_1 a_2) (join_commut a a_2 a_1)) True) % 74.18/74.37 (Or % 74.18/74.37 (Eq % 74.18/74.37 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) % 74.18/74.37 (element a_1 (the_carrier a))) % 74.18/74.37 False) % 74.18/74.37 (Eq (element a_2 (the_carrier a)) False)) % 74.18/74.37 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 : Iota), % 74.18/74.37 Or % 74.18/74.37 (Eq % 74.18/74.37 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) (element a_1 (the_carrier a))) % 74.18/74.37 False) % 74.18/74.37 (Or (Eq (element a_2 (the_carrier a)) False) (Eq (join_commut a a_1 a_2) (join_commut a a_2 a_1))) % 74.18/74.37 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), % 74.18/74.37 Or (Eq (element a (the_carrier a_1)) False) % 74.18/74.37 (Or (Eq (join_commut a_1 a_2 a) (join_commut a_1 a a_2)) % 74.18/74.37 (Or (Eq (And (And (Not (empty_carrier a_1)) (join_commutative a_1)) (join_semilatt_str a_1)) False) % 74.18/74.37 (Eq (element a_2 (the_carrier a_1)) False))) % 74.18/74.37 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), % 74.18/74.37 Or (Eq (element a (the_carrier a_1)) False) % 74.18/74.37 (Or (Eq (join_commut a_1 a_2 a) (join_commut a_1 a a_2)) % 74.18/74.37 (Or (Eq (element a_2 (the_carrier a_1)) False) % 74.18/74.37 (Or (Eq (And (Not (empty_carrier a_1)) (join_commutative a_1)) False) (Eq (join_semilatt_str a_1) False)))) % 74.18/74.37 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 : Iota), % 74.18/74.37 Or (Eq (element a (the_carrier a_1)) False) % 74.18/74.37 (Or (Eq (join_commut a_1 a_2 a) (join_commut a_1 a a_2)) % 74.18/74.37 (Or (Eq (element a_2 (the_carrier a_1)) False) % 74.18/74.37 (Or (Eq (join_semilatt_str a_1) False) % 74.22/74.39 (Or (Eq (Not (empty_carrier a_1)) False) (Eq (join_commutative a_1) False))))) % 74.22/74.39 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 : Iota), % 74.22/74.39 Or (Eq (element a (the_carrier a_1)) False) % 74.22/74.39 (Or (Eq (join_commut a_1 a_2 a) (join_commut a_1 a a_2)) % 74.22/74.39 (Or (Eq (element a_2 (the_carrier a_1)) False) % 74.22/74.39 (Or (Eq (join_semilatt_str a_1) False) (Or (Eq (join_commutative a_1) False) (Eq (empty_carrier a_1) True))))) % 74.22/74.39 Clause #137 (by clausification #[5]): ∀ (a : Iota), % 74.22/74.39 Eq % 74.22/74.39 (And (Not (empty_carrier a)) (join_semilatt_str a) → % 74.22/74.39 ∀ (B : Iota), % 74.22/74.39 element B (the_carrier a) → ∀ (C : Iota), element C (the_carrier a) → Iff (below a B C) (Eq (join a B C) C)) % 74.22/74.39 True % 74.22/74.39 Clause #138 (by clausification #[137]): ∀ (a : Iota), % 74.22/74.39 Or (Eq (And (Not (empty_carrier a)) (join_semilatt_str a)) False) % 74.22/74.39 (Eq % 74.22/74.39 (∀ (B : Iota), % 74.22/74.39 element B (the_carrier a) → ∀ (C : Iota), element C (the_carrier a) → Iff (below a B C) (Eq (join a B C) C)) % 74.22/74.39 True) % 74.22/74.39 Clause #139 (by clausification #[138]): ∀ (a : Iota), % 74.22/74.40 Or % 74.22/74.40 (Eq % 74.22/74.40 (∀ (B : Iota), % 74.22/74.40 element B (the_carrier a) → ∀ (C : Iota), element C (the_carrier a) → Iff (below a B C) (Eq (join a B C) C)) % 74.22/74.40 True) % 74.22/74.40 (Or (Eq (Not (empty_carrier a)) False) (Eq (join_semilatt_str a) False)) % 74.22/74.40 Clause #140 (by clausification #[139]): ∀ (a a_1 : Iota), % 74.22/74.40 Or (Eq (Not (empty_carrier a)) False) % 74.22/74.40 (Or (Eq (join_semilatt_str a) False) % 74.22/74.40 (Eq % 74.22/74.40 (element a_1 (the_carrier a) → % 74.22/74.40 ∀ (C : Iota), element C (the_carrier a) → Iff (below a a_1 C) (Eq (join a a_1 C) C)) % 74.22/74.40 True)) % 74.22/74.40 Clause #141 (by clausification #[140]): ∀ (a a_1 : Iota), % 74.22/74.40 Or (Eq (join_semilatt_str a) False) % 74.22/74.40 (Or % 74.22/74.40 (Eq % 74.22/74.40 (element a_1 (the_carrier a) → % 74.22/74.40 ∀ (C : Iota), element C (the_carrier a) → Iff (below a a_1 C) (Eq (join a a_1 C) C)) % 74.22/74.40 True) % 74.22/74.40 (Eq (empty_carrier a) True)) % 74.22/74.40 Clause #142 (by clausification #[141]): ∀ (a a_1 : Iota), % 74.22/74.40 Or (Eq (join_semilatt_str a) False) % 74.22/74.40 (Or (Eq (empty_carrier a) True) % 74.22/74.40 (Or (Eq (element a_1 (the_carrier a)) False) % 74.22/74.40 (Eq (∀ (C : Iota), element C (the_carrier a) → Iff (below a a_1 C) (Eq (join a a_1 C) C)) True))) % 74.22/74.40 Clause #143 (by clausification #[142]): ∀ (a a_1 a_2 : Iota), % 74.22/74.40 Or (Eq (join_semilatt_str a) False) % 74.22/74.40 (Or (Eq (empty_carrier a) True) % 74.22/74.40 (Or (Eq (element a_1 (the_carrier a)) False) % 74.22/74.40 (Eq (element a_2 (the_carrier a) → Iff (below a a_1 a_2) (Eq (join a a_1 a_2) a_2)) True))) % 74.22/74.40 Clause #144 (by clausification #[143]): ∀ (a a_1 a_2 : Iota), % 74.22/74.40 Or (Eq (join_semilatt_str a) False) % 74.22/74.40 (Or (Eq (empty_carrier a) True) % 74.22/74.40 (Or (Eq (element a_1 (the_carrier a)) False) % 74.22/74.40 (Or (Eq (element a_2 (the_carrier a)) False) (Eq (Iff (below a a_1 a_2) (Eq (join a a_1 a_2) a_2)) True)))) % 74.22/74.40 Clause #146 (by clausification #[144]): ∀ (a a_1 a_2 : Iota), % 74.22/74.40 Or (Eq (join_semilatt_str a) False) % 74.22/74.40 (Or (Eq (empty_carrier a) True) % 74.22/74.40 (Or (Eq (element a_1 (the_carrier a)) False) % 74.22/74.40 (Or (Eq (element a_2 (the_carrier a)) False) % 74.22/74.40 (Or (Eq (below a a_1 a_2) False) (Eq (Eq (join a a_1 a_2) a_2) True))))) % 74.22/74.40 Clause #188 (by clausification #[27]): Eq % 74.22/74.40 (∀ (A : Iota), % 74.22/74.40 And (And (Not (empty_carrier A)) (join_commutative A)) (join_semilatt_str A) → % 74.22/74.40 ∀ (B : Iota), % 74.22/74.40 element B (the_carrier A) → ∀ (C : Iota), element C (the_carrier A) → And (below A B C) (below A C B) → Eq B C) % 74.22/74.40 False % 74.22/74.40 Clause #189 (by clausification #[188]): ∀ (a : Iota), % 74.22/74.40 Eq % 74.22/74.40 (Not % 74.22/74.40 (And (And (Not (empty_carrier (skS.0 6 a))) (join_commutative (skS.0 6 a))) (join_semilatt_str (skS.0 6 a)) → % 74.22/74.40 ∀ (B : Iota), % 74.22/74.40 element B (the_carrier (skS.0 6 a)) → % 74.22/74.40 ∀ (C : Iota), % 74.22/74.40 element C (the_carrier (skS.0 6 a)) → And (below (skS.0 6 a) B C) (below (skS.0 6 a) C B) → Eq B C)) % 74.22/74.40 True % 74.22/74.40 Clause #190 (by clausification #[189]): ∀ (a : Iota), % 74.22/74.40 Eq % 74.22/74.40 (And (And (Not (empty_carrier (skS.0 6 a))) (join_commutative (skS.0 6 a))) (join_semilatt_str (skS.0 6 a)) → % 74.22/74.40 ∀ (B : Iota), % 74.22/74.40 element B (the_carrier (skS.0 6 a)) → % 74.22/74.42 ∀ (C : Iota), % 74.22/74.42 element C (the_carrier (skS.0 6 a)) → And (below (skS.0 6 a) B C) (below (skS.0 6 a) C B) → Eq B C) % 74.22/74.42 False % 74.22/74.42 Clause #191 (by clausification #[190]): ∀ (a : Iota), % 74.22/74.42 Eq (And (And (Not (empty_carrier (skS.0 6 a))) (join_commutative (skS.0 6 a))) (join_semilatt_str (skS.0 6 a))) True % 74.22/74.42 Clause #192 (by clausification #[190]): ∀ (a : Iota), % 74.22/74.42 Eq % 74.22/74.42 (∀ (B : Iota), % 74.22/74.42 element B (the_carrier (skS.0 6 a)) → % 74.22/74.42 ∀ (C : Iota), % 74.22/74.42 element C (the_carrier (skS.0 6 a)) → And (below (skS.0 6 a) B C) (below (skS.0 6 a) C B) → Eq B C) % 74.22/74.42 False % 74.22/74.42 Clause #193 (by clausification #[191]): ∀ (a : Iota), Eq (join_semilatt_str (skS.0 6 a)) True % 74.22/74.42 Clause #194 (by clausification #[191]): ∀ (a : Iota), Eq (And (Not (empty_carrier (skS.0 6 a))) (join_commutative (skS.0 6 a))) True % 74.22/74.42 Clause #200 (by clausification #[192]): ∀ (a a_1 : Iota), % 74.22/74.42 Eq % 74.22/74.42 (Not % 74.22/74.42 (element (skS.0 7 a a_1) (the_carrier (skS.0 6 a)) → % 74.22/74.42 ∀ (C : Iota), % 74.22/74.42 element C (the_carrier (skS.0 6 a)) → % 74.22/74.42 And (below (skS.0 6 a) (skS.0 7 a a_1) C) (below (skS.0 6 a) C (skS.0 7 a a_1)) → Eq (skS.0 7 a a_1) C)) % 74.22/74.42 True % 74.22/74.42 Clause #201 (by clausification #[200]): ∀ (a a_1 : Iota), % 74.22/74.42 Eq % 74.22/74.42 (element (skS.0 7 a a_1) (the_carrier (skS.0 6 a)) → % 74.22/74.42 ∀ (C : Iota), % 74.22/74.42 element C (the_carrier (skS.0 6 a)) → % 74.22/74.42 And (below (skS.0 6 a) (skS.0 7 a a_1) C) (below (skS.0 6 a) C (skS.0 7 a a_1)) → Eq (skS.0 7 a a_1) C) % 74.22/74.42 False % 74.22/74.42 Clause #202 (by clausification #[201]): ∀ (a a_1 : Iota), Eq (element (skS.0 7 a a_1) (the_carrier (skS.0 6 a))) True % 74.22/74.42 Clause #203 (by clausification #[201]): ∀ (a a_1 : Iota), % 74.22/74.42 Eq % 74.22/74.42 (∀ (C : Iota), % 74.22/74.42 element C (the_carrier (skS.0 6 a)) → % 74.22/74.42 And (below (skS.0 6 a) (skS.0 7 a a_1) C) (below (skS.0 6 a) C (skS.0 7 a a_1)) → Eq (skS.0 7 a a_1) C) % 74.22/74.42 False % 74.22/74.42 Clause #204 (by superposition #[202, 94]): ∀ (a a_1 a_2 : Iota), % 74.22/74.42 Or (Eq True False) % 74.22/74.42 (Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join_commut (skS.0 6 a) (skS.0 7 a a_2) a_1)) % 74.22/74.42 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.22/74.42 (Or (Eq (join_semilatt_str (skS.0 6 a)) False) % 74.22/74.42 (Or (Eq (join_commutative (skS.0 6 a)) False) (Eq (empty_carrier (skS.0 6 a)) True))))) % 74.22/74.42 Clause #230 (by clausification #[203]): ∀ (a a_1 a_2 : Iota), % 74.22/74.42 Eq % 74.22/74.42 (Not % 74.22/74.42 (element (skS.0 8 a a_1 a_2) (the_carrier (skS.0 6 a)) → % 74.22/74.42 And (below (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) % 74.22/74.42 (below (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) → % 74.22/74.42 Eq (skS.0 7 a a_1) (skS.0 8 a a_1 a_2))) % 74.22/74.42 True % 74.22/74.42 Clause #231 (by clausification #[230]): ∀ (a a_1 a_2 : Iota), % 74.22/74.42 Eq % 74.22/74.42 (element (skS.0 8 a a_1 a_2) (the_carrier (skS.0 6 a)) → % 74.22/74.42 And (below (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) % 74.22/74.42 (below (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) → % 74.22/74.42 Eq (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) % 74.22/74.42 False % 74.22/74.42 Clause #232 (by clausification #[231]): ∀ (a a_1 a_2 : Iota), Eq (element (skS.0 8 a a_1 a_2) (the_carrier (skS.0 6 a))) True % 74.22/74.42 Clause #233 (by clausification #[231]): ∀ (a a_1 a_2 : Iota), % 74.22/74.42 Eq % 74.22/74.42 (And (below (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) % 74.22/74.42 (below (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) → % 74.22/74.42 Eq (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) % 74.22/74.42 False % 74.22/74.42 Clause #293 (by clausification #[23]): ∀ (a : Iota), % 74.22/74.42 Eq % 74.22/74.42 (∀ (B C : Iota), % 74.22/74.42 And % 74.22/74.42 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) % 74.22/74.42 (element B (the_carrier a))) % 74.22/74.42 (element C (the_carrier a)) → % 74.22/74.42 Eq (join_commut a B C) (join a B C)) % 74.22/74.42 True % 74.22/74.42 Clause #294 (by clausification #[293]): ∀ (a a_1 : Iota), % 74.22/74.42 Eq % 74.22/74.42 (∀ (C : Iota), % 74.22/74.42 And % 74.22/74.42 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) % 74.22/74.42 (element a_1 (the_carrier a))) % 74.22/74.42 (element C (the_carrier a)) → % 74.22/74.42 Eq (join_commut a a_1 C) (join a a_1 C)) % 74.22/74.42 True % 74.22/74.42 Clause #295 (by clausification #[294]): ∀ (a a_1 a_2 : Iota), % 74.22/74.42 Eq % 74.22/74.42 (And % 74.22/74.42 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) % 74.28/74.45 (element a_1 (the_carrier a))) % 74.28/74.45 (element a_2 (the_carrier a)) → % 74.28/74.45 Eq (join_commut a a_1 a_2) (join a a_1 a_2)) % 74.28/74.45 True % 74.28/74.45 Clause #296 (by clausification #[295]): ∀ (a a_1 a_2 : Iota), % 74.28/74.45 Or % 74.28/74.45 (Eq % 74.28/74.45 (And % 74.28/74.45 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) % 74.28/74.45 (element a_1 (the_carrier a))) % 74.28/74.45 (element a_2 (the_carrier a))) % 74.28/74.45 False) % 74.28/74.45 (Eq (Eq (join_commut a a_1 a_2) (join a a_1 a_2)) True) % 74.28/74.45 Clause #297 (by clausification #[296]): ∀ (a a_1 a_2 : Iota), % 74.28/74.45 Or (Eq (Eq (join_commut a a_1 a_2) (join a a_1 a_2)) True) % 74.28/74.45 (Or % 74.28/74.45 (Eq % 74.28/74.45 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) % 74.28/74.45 (element a_1 (the_carrier a))) % 74.28/74.45 False) % 74.28/74.45 (Eq (element a_2 (the_carrier a)) False)) % 74.28/74.45 Clause #298 (by clausification #[297]): ∀ (a a_1 a_2 : Iota), % 74.28/74.45 Or % 74.28/74.45 (Eq % 74.28/74.45 (And (And (And (Not (empty_carrier a)) (join_commutative a)) (join_semilatt_str a)) (element a_1 (the_carrier a))) % 74.28/74.45 False) % 74.28/74.45 (Or (Eq (element a_2 (the_carrier a)) False) (Eq (join_commut a a_1 a_2) (join a a_1 a_2))) % 74.28/74.45 Clause #299 (by clausification #[298]): ∀ (a a_1 a_2 : Iota), % 74.28/74.45 Or (Eq (element a (the_carrier a_1)) False) % 74.28/74.45 (Or (Eq (join_commut a_1 a_2 a) (join a_1 a_2 a)) % 74.28/74.45 (Or (Eq (And (And (Not (empty_carrier a_1)) (join_commutative a_1)) (join_semilatt_str a_1)) False) % 74.28/74.45 (Eq (element a_2 (the_carrier a_1)) False))) % 74.28/74.45 Clause #300 (by clausification #[299]): ∀ (a a_1 a_2 : Iota), % 74.28/74.45 Or (Eq (element a (the_carrier a_1)) False) % 74.28/74.45 (Or (Eq (join_commut a_1 a_2 a) (join a_1 a_2 a)) % 74.28/74.45 (Or (Eq (element a_2 (the_carrier a_1)) False) % 74.28/74.45 (Or (Eq (And (Not (empty_carrier a_1)) (join_commutative a_1)) False) (Eq (join_semilatt_str a_1) False)))) % 74.28/74.45 Clause #301 (by clausification #[300]): ∀ (a a_1 a_2 : Iota), % 74.28/74.45 Or (Eq (element a (the_carrier a_1)) False) % 74.28/74.45 (Or (Eq (join_commut a_1 a_2 a) (join a_1 a_2 a)) % 74.28/74.45 (Or (Eq (element a_2 (the_carrier a_1)) False) % 74.28/74.45 (Or (Eq (join_semilatt_str a_1) False) % 74.28/74.45 (Or (Eq (Not (empty_carrier a_1)) False) (Eq (join_commutative a_1) False))))) % 74.28/74.45 Clause #302 (by clausification #[301]): ∀ (a a_1 a_2 : Iota), % 74.28/74.45 Or (Eq (element a (the_carrier a_1)) False) % 74.28/74.45 (Or (Eq (join_commut a_1 a_2 a) (join a_1 a_2 a)) % 74.28/74.45 (Or (Eq (element a_2 (the_carrier a_1)) False) % 74.28/74.45 (Or (Eq (join_semilatt_str a_1) False) (Or (Eq (join_commutative a_1) False) (Eq (empty_carrier a_1) True))))) % 74.28/74.45 Clause #303 (by superposition #[302, 202]): ∀ (a a_1 a_2 : Iota), % 74.28/74.45 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join (skS.0 6 a) a_1 (skS.0 7 a a_2))) % 74.28/74.45 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.28/74.45 (Or (Eq (join_semilatt_str (skS.0 6 a)) False) % 74.28/74.45 (Or (Eq (join_commutative (skS.0 6 a)) False) (Or (Eq (empty_carrier (skS.0 6 a)) True) (Eq False True))))) % 74.28/74.45 Clause #304 (by superposition #[302, 232]): ∀ (a a_1 a_2 a_3 : Iota), % 74.28/74.45 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3)) (join (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3))) % 74.28/74.45 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.28/74.45 (Or (Eq (join_semilatt_str (skS.0 6 a)) False) % 74.28/74.45 (Or (Eq (join_commutative (skS.0 6 a)) False) (Or (Eq (empty_carrier (skS.0 6 a)) True) (Eq False True))))) % 74.28/74.45 Clause #329 (by clausification #[194]): ∀ (a : Iota), Eq (join_commutative (skS.0 6 a)) True % 74.28/74.45 Clause #330 (by clausification #[194]): ∀ (a : Iota), Eq (Not (empty_carrier (skS.0 6 a))) True % 74.28/74.45 Clause #331 (by clausification #[330]): ∀ (a : Iota), Eq (empty_carrier (skS.0 6 a)) False % 74.28/74.45 Clause #374 (by clausification #[233]): ∀ (a a_1 a_2 : Iota), % 74.28/74.45 Eq % 74.28/74.45 (And (below (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) % 74.28/74.45 (below (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1))) % 74.28/74.45 True % 74.28/74.45 Clause #375 (by clausification #[233]): ∀ (a a_1 a_2 : Iota), Eq (Eq (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) False % 74.28/74.45 Clause #376 (by clausification #[374]): ∀ (a a_1 a_2 : Iota), Eq (below (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) True % 74.28/74.45 Clause #377 (by clausification #[374]): ∀ (a a_1 a_2 : Iota), Eq (below (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) True % 74.29/74.47 Clause #378 (by clausification #[375]): ∀ (a a_1 a_2 : Iota), Ne (skS.0 7 a a_1) (skS.0 8 a a_1 a_2) % 74.29/74.47 Clause #397 (by clausification #[146]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_semilatt_str a) False) % 74.29/74.47 (Or (Eq (empty_carrier a) True) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier a)) False) % 74.29/74.47 (Or (Eq (element a_2 (the_carrier a)) False) (Or (Eq (below a a_1 a_2) False) (Eq (join a a_1 a_2) a_2))))) % 74.29/74.47 Clause #399 (by superposition #[397, 193]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (empty_carrier (skS.0 6 a)) True) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.47 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 74.29/74.47 (Or (Eq (below (skS.0 6 a) a_1 a_2) False) (Or (Eq (join (skS.0 6 a) a_1 a_2) a_2) (Eq False True))))) % 74.29/74.47 Clause #523 (by clausification #[204]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join_commut (skS.0 6 a) (skS.0 7 a a_2) a_1)) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.47 (Or (Eq (join_semilatt_str (skS.0 6 a)) False) % 74.29/74.47 (Or (Eq (join_commutative (skS.0 6 a)) False) (Eq (empty_carrier (skS.0 6 a)) True)))) % 74.29/74.47 Clause #524 (by forward demodulation #[523, 193]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join_commut (skS.0 6 a) (skS.0 7 a a_2) a_1)) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.47 (Or (Eq True False) (Or (Eq (join_commutative (skS.0 6 a)) False) (Eq (empty_carrier (skS.0 6 a)) True)))) % 74.29/74.47 Clause #525 (by clausification #[524]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join_commut (skS.0 6 a) (skS.0 7 a a_2) a_1)) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.47 (Or (Eq (join_commutative (skS.0 6 a)) False) (Eq (empty_carrier (skS.0 6 a)) True))) % 74.29/74.47 Clause #526 (by forward demodulation #[525, 329]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join_commut (skS.0 6 a) (skS.0 7 a a_2) a_1)) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) (Or (Eq True False) (Eq (empty_carrier (skS.0 6 a)) True))) % 74.29/74.47 Clause #527 (by clausification #[526]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join_commut (skS.0 6 a) (skS.0 7 a a_2) a_1)) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) (Eq (empty_carrier (skS.0 6 a)) True)) % 74.29/74.47 Clause #528 (by forward demodulation #[527, 331]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join_commut (skS.0 6 a) (skS.0 7 a a_2) a_1)) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) (Eq False True)) % 74.29/74.47 Clause #529 (by clausification #[528]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join_commut (skS.0 6 a) (skS.0 7 a a_2) a_1)) % 74.29/74.47 (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.47 Clause #531 (by superposition #[529, 232]): ∀ (a a_1 a_2 a_3 : Iota), % 74.29/74.47 Or % 74.29/74.47 (Eq (join_commut (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) % 74.29/74.47 (join_commut (skS.0 6 a) (skS.0 7 a a_3) (skS.0 8 a a_1 a_2))) % 74.29/74.47 (Eq False True) % 74.29/74.47 Clause #1163 (by clausification #[303]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join (skS.0 6 a) a_1 (skS.0 7 a a_2))) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.47 (Or (Eq (join_semilatt_str (skS.0 6 a)) False) % 74.29/74.47 (Or (Eq (join_commutative (skS.0 6 a)) False) (Eq (empty_carrier (skS.0 6 a)) True)))) % 74.29/74.47 Clause #1164 (by forward demodulation #[1163, 193]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join (skS.0 6 a) a_1 (skS.0 7 a a_2))) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.47 (Or (Eq True False) (Or (Eq (join_commutative (skS.0 6 a)) False) (Eq (empty_carrier (skS.0 6 a)) True)))) % 74.29/74.47 Clause #1165 (by clausification #[1164]): ∀ (a a_1 a_2 : Iota), % 74.29/74.47 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join (skS.0 6 a) a_1 (skS.0 7 a a_2))) % 74.29/74.47 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.50 (Or (Eq (join_commutative (skS.0 6 a)) False) (Eq (empty_carrier (skS.0 6 a)) True))) % 74.29/74.50 Clause #1166 (by forward demodulation #[1165, 329]): ∀ (a a_1 a_2 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join (skS.0 6 a) a_1 (skS.0 7 a a_2))) % 74.29/74.50 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) (Or (Eq True False) (Eq (empty_carrier (skS.0 6 a)) True))) % 74.29/74.50 Clause #1167 (by clausification #[1166]): ∀ (a a_1 a_2 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join (skS.0 6 a) a_1 (skS.0 7 a a_2))) % 74.29/74.50 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) (Eq (empty_carrier (skS.0 6 a)) True)) % 74.29/74.50 Clause #1168 (by forward demodulation #[1167, 331]): ∀ (a a_1 a_2 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join (skS.0 6 a) a_1 (skS.0 7 a a_2))) % 74.29/74.50 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) (Eq False True)) % 74.29/74.50 Clause #1169 (by clausification #[1168]): ∀ (a a_1 a_2 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 7 a a_2)) (join (skS.0 6 a) a_1 (skS.0 7 a a_2))) % 74.29/74.50 (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.50 Clause #1171 (by superposition #[1169, 232]): ∀ (a a_1 a_2 a_3 : Iota), % 74.29/74.50 Or % 74.29/74.50 (Eq (join_commut (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) % 74.29/74.50 (join (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3))) % 74.29/74.50 (Eq False True) % 74.29/74.50 Clause #1201 (by clausification #[304]): ∀ (a a_1 a_2 a_3 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3)) (join (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3))) % 74.29/74.50 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.50 (Or (Eq (join_semilatt_str (skS.0 6 a)) False) % 74.29/74.50 (Or (Eq (join_commutative (skS.0 6 a)) False) (Eq (empty_carrier (skS.0 6 a)) True)))) % 74.29/74.50 Clause #1202 (by forward demodulation #[1201, 193]): ∀ (a a_1 a_2 a_3 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3)) (join (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3))) % 74.29/74.50 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.50 (Or (Eq True False) (Or (Eq (join_commutative (skS.0 6 a)) False) (Eq (empty_carrier (skS.0 6 a)) True)))) % 74.29/74.50 Clause #1203 (by clausification #[1202]): ∀ (a a_1 a_2 a_3 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3)) (join (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3))) % 74.29/74.50 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.50 (Or (Eq (join_commutative (skS.0 6 a)) False) (Eq (empty_carrier (skS.0 6 a)) True))) % 74.29/74.50 Clause #1204 (by forward demodulation #[1203, 329]): ∀ (a a_1 a_2 a_3 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3)) (join (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3))) % 74.29/74.50 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) (Or (Eq True False) (Eq (empty_carrier (skS.0 6 a)) True))) % 74.29/74.50 Clause #1205 (by clausification #[1204]): ∀ (a a_1 a_2 a_3 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3)) (join (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3))) % 74.29/74.50 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) (Eq (empty_carrier (skS.0 6 a)) True)) % 74.29/74.50 Clause #1206 (by forward demodulation #[1205, 331]): ∀ (a a_1 a_2 a_3 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3)) (join (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3))) % 74.29/74.50 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) (Eq False True)) % 74.29/74.50 Clause #1207 (by clausification #[1206]): ∀ (a a_1 a_2 a_3 : Iota), % 74.29/74.50 Or (Eq (join_commut (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3)) (join (skS.0 6 a) a_1 (skS.0 8 a a_2 a_3))) % 74.29/74.50 (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.50 Clause #1208 (by superposition #[1207, 202]): ∀ (a a_1 a_2 a_3 : Iota), % 74.29/74.50 Or % 74.29/74.50 (Eq (join_commut (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_2 a_3)) % 74.29/74.50 (join (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_2 a_3))) % 74.29/74.50 (Eq False True) % 74.29/74.50 Clause #1666 (by clausification #[399]): ∀ (a a_1 a_2 : Iota), % 74.29/74.50 Or (Eq (empty_carrier (skS.0 6 a)) True) % 74.29/74.50 (Or (Eq (element a_1 (the_carrier (skS.0 6 a))) False) % 74.29/74.50 (Or (Eq (element a_2 (the_carrier (skS.0 6 a))) False) % 74.29/74.50 (Or (Eq (below (skS.0 6 a) a_1 a_2) False) (Eq (join (skS.0 6 a) a_1 a_2) a_2)))) % 74.29/74.50 Clause #1667 (by forward demodulation #[1666, 331]): ∀ (a a_1 a_2 : Iota), % 74.29/74.50 Or (Eq False True) % 74.34/74.53 (Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 74.34/74.53 (Or (Eq (element a_2 (the_carrier (skS.0 6 a_1))) False) % 74.34/74.53 (Or (Eq (below (skS.0 6 a_1) a a_2) False) (Eq (join (skS.0 6 a_1) a a_2) a_2)))) % 74.34/74.53 Clause #1668 (by clausification #[1667]): ∀ (a a_1 a_2 : Iota), % 74.34/74.53 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 74.34/74.53 (Or (Eq (element a_2 (the_carrier (skS.0 6 a_1))) False) % 74.34/74.53 (Or (Eq (below (skS.0 6 a_1) a a_2) False) (Eq (join (skS.0 6 a_1) a a_2) a_2))) % 74.34/74.53 Clause #1669 (by superposition #[1668, 202]): ∀ (a a_1 a_2 : Iota), % 74.34/74.53 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 74.34/74.53 (Or (Eq (below (skS.0 6 a_1) (skS.0 7 a_1 a_2) a) False) % 74.34/74.53 (Or (Eq (join (skS.0 6 a_1) (skS.0 7 a_1 a_2) a) a) (Eq False True))) % 74.34/74.53 Clause #1670 (by superposition #[1668, 232]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 74.34/74.53 (Or (Eq (below (skS.0 6 a_1) (skS.0 8 a_1 a_2 a_3) a) False) % 74.34/74.53 (Or (Eq (join (skS.0 6 a_1) (skS.0 8 a_1 a_2 a_3) a) a) (Eq False True))) % 74.34/74.53 Clause #1690 (by clausification #[1669]): ∀ (a a_1 a_2 : Iota), % 74.34/74.53 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 74.34/74.53 (Or (Eq (below (skS.0 6 a_1) (skS.0 7 a_1 a_2) a) False) (Eq (join (skS.0 6 a_1) (skS.0 7 a_1 a_2) a) a)) % 74.34/74.53 Clause #1692 (by superposition #[1690, 232]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Or (Eq (below (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_2 a_3)) False) % 74.34/74.53 (Or (Eq (join (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_2 a_3)) (skS.0 8 a a_2 a_3)) (Eq False True)) % 74.34/74.53 Clause #2128 (by clausification #[1670]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Or (Eq (element a (the_carrier (skS.0 6 a_1))) False) % 74.34/74.53 (Or (Eq (below (skS.0 6 a_1) (skS.0 8 a_1 a_2 a_3) a) False) (Eq (join (skS.0 6 a_1) (skS.0 8 a_1 a_2 a_3) a) a)) % 74.34/74.53 Clause #2129 (by superposition #[2128, 202]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Or (Eq (below (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) False) % 74.34/74.53 (Or (Eq (join (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) (skS.0 7 a a_3)) (Eq False True)) % 74.34/74.53 Clause #2690 (by clausification #[1208]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Eq (join_commut (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_2 a_3)) % 74.34/74.53 (join (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_2 a_3)) % 74.34/74.53 Clause #2691 (by clausification #[1171]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Eq (join_commut (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) % 74.34/74.53 (join (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) % 74.34/74.53 Clause #2692 (by clausification #[531]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Eq (join_commut (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) % 74.34/74.53 (join_commut (skS.0 6 a) (skS.0 7 a a_3) (skS.0 8 a a_1 a_2)) % 74.34/74.53 Clause #2693 (by forward demodulation #[2692, 2691]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Eq (join (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) % 74.34/74.53 (join_commut (skS.0 6 a) (skS.0 7 a a_3) (skS.0 8 a a_1 a_2)) % 74.34/74.53 Clause #2694 (by superposition #[2693, 2690]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Eq (join (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) (join (skS.0 6 a) (skS.0 7 a a_3) (skS.0 8 a a_1 a_2)) % 74.34/74.53 Clause #6771 (by clausification #[2129]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Or (Eq (below (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) False) % 74.34/74.53 (Eq (join (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_3)) (skS.0 7 a a_3)) % 74.34/74.53 Clause #6772 (by superposition #[6771, 376]): ∀ (a a_1 a_2 : Iota), Or (Eq (join (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) (skS.0 7 a a_1)) (Eq False True) % 74.34/74.53 Clause #6778 (by clausification #[6772]): ∀ (a a_1 a_2 : Iota), Eq (join (skS.0 6 a) (skS.0 8 a a_1 a_2) (skS.0 7 a a_1)) (skS.0 7 a a_1) % 74.34/74.53 Clause #6779 (by superposition #[6778, 2694]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 7 a a_1) (join (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) % 74.34/74.53 Clause #8850 (by clausification #[1692]): ∀ (a a_1 a_2 a_3 : Iota), % 74.34/74.53 Or (Eq (below (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_2 a_3)) False) % 74.34/74.53 (Eq (join (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_2 a_3)) (skS.0 8 a a_2 a_3)) % 74.34/74.53 Clause #8851 (by superposition #[8850, 377]): ∀ (a a_1 a_2 : Iota), Or (Eq (join (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) (skS.0 8 a a_1 a_2)) (Eq False True) % 74.34/74.53 Clause #8852 (by clausification #[8851]): ∀ (a a_1 a_2 : Iota), Eq (join (skS.0 6 a) (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) (skS.0 8 a a_1 a_2) % 74.39/74.63 Clause #8854 (by superposition #[8852, 6779]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 7 a a_1) (skS.0 8 a a_1 a_2) % 74.39/74.63 Clause #8855 (by forward contextual literal cutting #[8854, 378]): False % 74.39/74.63 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------