%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU244+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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:13 PM UTC 2025 % Result : Theorem 5.15s 5.34s % Output : Proof 5.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU244+1 : TPTP v9.2.0. Released v3.3.0. % 0.06/0.14 % Command : duper %s % 0.12/0.35 % Computer : n020.cluster.edu % 0.12/0.35 % Model : x86_64 x86_64 % 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.35 % Memory : 8042.1875MB % 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 300 % 0.12/0.35 % DateTime : Fri Oct 3 04:55:38 EDT 2025 % 0.12/0.35 % CPUTime : % 5.15/5.34 SZS status Theorem for theBenchmark.p % 5.15/5.34 SZS output start Proof for theBenchmark.p % 5.15/5.34 Clause #1 (by assumption #[]): Eq (∀ (A : Iota), relation A → Iff (antisymmetric A) (is_antisymmetric_in A (relation_field A))) True % 5.15/5.34 Clause #2 (by assumption #[]): Eq (∀ (A : Iota), relation A → Iff (connected A) (is_connected_in A (relation_field A))) True % 5.15/5.34 Clause #3 (by assumption #[]): Eq (∀ (A : Iota), relation A → Iff (transitive A) (is_transitive_in A (relation_field A))) True % 5.15/5.34 Clause #4 (by assumption #[]): Eq % 5.15/5.34 (∀ (A : Iota), % 5.15/5.34 relation A → % 5.15/5.34 Iff (well_ordering A) % 5.15/5.34 (And (And (And (And (reflexive A) (transitive A)) (antisymmetric A)) (connected A)) (well_founded_relation A))) % 5.15/5.34 True % 5.15/5.34 Clause #5 (by assumption #[]): Eq % 5.15/5.34 (∀ (A : Iota), % 5.15/5.34 relation A → % 5.15/5.34 ∀ (B : Iota), % 5.15/5.34 Iff (well_orders A B) % 5.15/5.34 (And % 5.15/5.34 (And (And (And (is_reflexive_in A B) (is_transitive_in A B)) (is_antisymmetric_in A B)) % 5.15/5.34 (is_connected_in A B)) % 5.15/5.34 (is_well_founded_in A B))) % 5.15/5.34 True % 5.15/5.34 Clause #7 (by assumption #[]): Eq (∀ (A : Iota), relation A → Iff (reflexive A) (is_reflexive_in A (relation_field A))) True % 5.15/5.34 Clause #10 (by assumption #[]): Eq (∀ (A : Iota), relation A → Iff (well_founded_relation A) (is_well_founded_in A (relation_field A))) True % 5.15/5.34 Clause #11 (by assumption #[]): Eq (Not (∀ (A : Iota), relation A → Iff (well_orders A (relation_field A)) (well_ordering A))) True % 5.15/5.34 Clause #15 (by clausification #[10]): ∀ (a : Iota), Eq (relation a → Iff (well_founded_relation a) (is_well_founded_in a (relation_field a))) True % 5.15/5.34 Clause #16 (by clausification #[15]): ∀ (a : Iota), % 5.15/5.34 Or (Eq (relation a) False) (Eq (Iff (well_founded_relation a) (is_well_founded_in a (relation_field a))) True) % 5.15/5.34 Clause #17 (by clausification #[16]): ∀ (a : Iota), % 5.15/5.34 Or (Eq (relation a) False) % 5.15/5.34 (Or (Eq (well_founded_relation a) True) (Eq (is_well_founded_in a (relation_field a)) False)) % 5.15/5.34 Clause #18 (by clausification #[16]): ∀ (a : Iota), % 5.15/5.34 Or (Eq (relation a) False) % 5.15/5.34 (Or (Eq (well_founded_relation a) False) (Eq (is_well_founded_in a (relation_field a)) True)) % 5.15/5.34 Clause #19 (by clausification #[7]): ∀ (a : Iota), Eq (relation a → Iff (reflexive a) (is_reflexive_in a (relation_field a))) True % 5.15/5.34 Clause #20 (by clausification #[19]): ∀ (a : Iota), Or (Eq (relation a) False) (Eq (Iff (reflexive a) (is_reflexive_in a (relation_field a))) True) % 5.15/5.34 Clause #21 (by clausification #[20]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (reflexive a) True) (Eq (is_reflexive_in a (relation_field a)) False)) % 5.15/5.34 Clause #22 (by clausification #[20]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (reflexive a) False) (Eq (is_reflexive_in a (relation_field a)) True)) % 5.15/5.34 Clause #23 (by clausification #[3]): ∀ (a : Iota), Eq (relation a → Iff (transitive a) (is_transitive_in a (relation_field a))) True % 5.15/5.34 Clause #24 (by clausification #[23]): ∀ (a : Iota), Or (Eq (relation a) False) (Eq (Iff (transitive a) (is_transitive_in a (relation_field a))) True) % 5.15/5.34 Clause #25 (by clausification #[24]): ∀ (a : Iota), % 5.15/5.34 Or (Eq (relation a) False) (Or (Eq (transitive a) True) (Eq (is_transitive_in a (relation_field a)) False)) % 5.15/5.34 Clause #26 (by clausification #[24]): ∀ (a : Iota), % 5.15/5.34 Or (Eq (relation a) False) (Or (Eq (transitive a) False) (Eq (is_transitive_in a (relation_field a)) True)) % 5.15/5.34 Clause #30 (by clausification #[2]): ∀ (a : Iota), Eq (relation a → Iff (connected a) (is_connected_in a (relation_field a))) True % 5.15/5.34 Clause #31 (by clausification #[30]): ∀ (a : Iota), Or (Eq (relation a) False) (Eq (Iff (connected a) (is_connected_in a (relation_field a))) True) % 5.15/5.34 Clause #32 (by clausification #[31]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (connected a) True) (Eq (is_connected_in a (relation_field a)) False)) % 5.15/5.34 Clause #33 (by clausification #[31]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (connected a) False) (Eq (is_connected_in a (relation_field a)) True)) % 5.15/5.34 Clause #34 (by clausification #[1]): ∀ (a : Iota), Eq (relation a → Iff (antisymmetric a) (is_antisymmetric_in a (relation_field a))) True % 5.15/5.34 Clause #35 (by clausification #[34]): ∀ (a : Iota), Or (Eq (relation a) False) (Eq (Iff (antisymmetric a) (is_antisymmetric_in a (relation_field a))) True) % 5.15/5.36 Clause #36 (by clausification #[35]): ∀ (a : Iota), % 5.15/5.36 Or (Eq (relation a) False) (Or (Eq (antisymmetric a) True) (Eq (is_antisymmetric_in a (relation_field a)) False)) % 5.15/5.36 Clause #37 (by clausification #[35]): ∀ (a : Iota), % 5.15/5.36 Or (Eq (relation a) False) (Or (Eq (antisymmetric a) False) (Eq (is_antisymmetric_in a (relation_field a)) True)) % 5.15/5.36 Clause #38 (by clausification #[11]): Eq (∀ (A : Iota), relation A → Iff (well_orders A (relation_field A)) (well_ordering A)) False % 5.15/5.36 Clause #39 (by clausification #[38]): ∀ (a : Iota), % 5.15/5.36 Eq % 5.15/5.36 (Not % 5.15/5.36 (relation (skS.0 0 a) → Iff (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) (well_ordering (skS.0 0 a)))) % 5.15/5.36 True % 5.15/5.36 Clause #40 (by clausification #[39]): ∀ (a : Iota), % 5.15/5.36 Eq (relation (skS.0 0 a) → Iff (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) (well_ordering (skS.0 0 a))) % 5.15/5.36 False % 5.15/5.36 Clause #41 (by clausification #[40]): ∀ (a : Iota), Eq (relation (skS.0 0 a)) True % 5.15/5.36 Clause #42 (by clausification #[40]): ∀ (a : Iota), Eq (Iff (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) (well_ordering (skS.0 0 a))) False % 5.15/5.36 Clause #43 (by superposition #[41, 17]): ∀ (a : Iota), % 5.15/5.36 Or (Eq True False) % 5.15/5.36 (Or (Eq (well_founded_relation (skS.0 0 a)) True) % 5.15/5.36 (Eq (is_well_founded_in (skS.0 0 a) (relation_field (skS.0 0 a))) False)) % 5.15/5.36 Clause #44 (by superposition #[41, 21]): ∀ (a : Iota), % 5.15/5.36 Or (Eq True False) % 5.15/5.36 (Or (Eq (reflexive (skS.0 0 a)) True) (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False)) % 5.15/5.36 Clause #45 (by superposition #[41, 25]): ∀ (a : Iota), % 5.15/5.36 Or (Eq True False) % 5.15/5.36 (Or (Eq (transitive (skS.0 0 a)) True) (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False)) % 5.15/5.36 Clause #46 (by superposition #[41, 32]): ∀ (a : Iota), % 5.15/5.36 Or (Eq True False) % 5.15/5.36 (Or (Eq (connected (skS.0 0 a)) True) (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False)) % 5.15/5.36 Clause #47 (by superposition #[41, 36]): ∀ (a : Iota), % 5.15/5.36 Or (Eq True False) % 5.15/5.36 (Or (Eq (antisymmetric (skS.0 0 a)) True) (Eq (is_antisymmetric_in (skS.0 0 a) (relation_field (skS.0 0 a))) False)) % 5.15/5.36 Clause #48 (by superposition #[41, 37]): ∀ (a : Iota), % 5.15/5.36 Or (Eq True False) % 5.15/5.36 (Or (Eq (antisymmetric (skS.0 0 a)) False) (Eq (is_antisymmetric_in (skS.0 0 a) (relation_field (skS.0 0 a))) True)) % 5.15/5.36 Clause #49 (by superposition #[18, 41]): ∀ (a : Iota), % 5.15/5.36 Or (Eq True False) % 5.15/5.36 (Or (Eq (well_founded_relation (skS.0 0 a)) False) % 5.15/5.36 (Eq (is_well_founded_in (skS.0 0 a) (relation_field (skS.0 0 a))) True)) % 5.15/5.36 Clause #50 (by clausification #[4]): ∀ (a : Iota), % 5.15/5.36 Eq % 5.15/5.36 (relation a → % 5.15/5.36 Iff (well_ordering a) % 5.15/5.36 (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a))) % 5.15/5.36 True % 5.15/5.36 Clause #51 (by clausification #[50]): ∀ (a : Iota), % 5.15/5.36 Or (Eq (relation a) False) % 5.15/5.36 (Eq % 5.15/5.36 (Iff (well_ordering a) % 5.15/5.36 (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a))) % 5.15/5.36 True) % 5.15/5.36 Clause #52 (by clausification #[51]): ∀ (a : Iota), % 5.15/5.36 Or (Eq (relation a) False) % 5.15/5.36 (Or (Eq (well_ordering a) True) % 5.15/5.36 (Eq (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a)) % 5.15/5.36 False)) % 5.15/5.36 Clause #53 (by clausification #[51]): ∀ (a : Iota), % 5.15/5.36 Or (Eq (relation a) False) % 5.15/5.36 (Or (Eq (well_ordering a) False) % 5.15/5.36 (Eq (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a)) % 5.15/5.36 True)) % 5.15/5.36 Clause #54 (by clausification #[52]): ∀ (a : Iota), % 5.15/5.36 Or (Eq (relation a) False) % 5.15/5.36 (Or (Eq (well_ordering a) True) % 5.15/5.36 (Or (Eq (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) False) % 5.15/5.36 (Eq (well_founded_relation a) False))) % 5.15/5.36 Clause #55 (by clausification #[54]): ∀ (a : Iota), % 5.15/5.36 Or (Eq (relation a) False) % 5.15/5.36 (Or (Eq (well_ordering a) True) % 5.15/5.36 (Or (Eq (well_founded_relation a) False) % 5.15/5.36 (Or (Eq (And (And (reflexive a) (transitive a)) (antisymmetric a)) False) (Eq (connected a) False)))) % 5.15/5.39 Clause #56 (by clausification #[55]): ∀ (a : Iota), % 5.15/5.39 Or (Eq (relation a) False) % 5.15/5.39 (Or (Eq (well_ordering a) True) % 5.15/5.39 (Or (Eq (well_founded_relation a) False) % 5.15/5.39 (Or (Eq (connected a) False) (Or (Eq (And (reflexive a) (transitive a)) False) (Eq (antisymmetric a) False))))) % 5.15/5.39 Clause #57 (by clausification #[56]): ∀ (a : Iota), % 5.15/5.39 Or (Eq (relation a) False) % 5.15/5.39 (Or (Eq (well_ordering a) True) % 5.15/5.39 (Or (Eq (well_founded_relation a) False) % 5.15/5.39 (Or (Eq (connected a) False) % 5.15/5.39 (Or (Eq (antisymmetric a) False) (Or (Eq (reflexive a) False) (Eq (transitive a) False)))))) % 5.15/5.39 Clause #58 (by superposition #[57, 41]): ∀ (a : Iota), % 5.15/5.39 Or (Eq (well_ordering (skS.0 0 a)) True) % 5.15/5.39 (Or (Eq (well_founded_relation (skS.0 0 a)) False) % 5.15/5.39 (Or (Eq (connected (skS.0 0 a)) False) % 5.15/5.39 (Or (Eq (antisymmetric (skS.0 0 a)) False) % 5.15/5.39 (Or (Eq (reflexive (skS.0 0 a)) False) (Or (Eq (transitive (skS.0 0 a)) False) (Eq False True)))))) % 5.15/5.39 Clause #59 (by superposition #[22, 41]): ∀ (a : Iota), % 5.15/5.39 Or (Eq True False) % 5.15/5.39 (Or (Eq (reflexive (skS.0 0 a)) False) (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True)) % 5.15/5.39 Clause #60 (by superposition #[26, 41]): ∀ (a : Iota), % 5.15/5.39 Or (Eq True False) % 5.15/5.39 (Or (Eq (transitive (skS.0 0 a)) False) (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True)) % 5.15/5.39 Clause #61 (by superposition #[33, 41]): ∀ (a : Iota), % 5.15/5.39 Or (Eq True False) % 5.15/5.39 (Or (Eq (connected (skS.0 0 a)) False) (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) True)) % 5.15/5.39 Clause #66 (by clausification #[53]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (well_founded_relation a) True)) % 5.15/5.39 Clause #67 (by clausification #[53]): ∀ (a : Iota), % 5.15/5.39 Or (Eq (relation a) False) % 5.15/5.39 (Or (Eq (well_ordering a) False) % 5.15/5.39 (Eq (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) True)) % 5.15/5.39 Clause #68 (by superposition #[66, 41]): ∀ (a : Iota), % 5.15/5.39 Or (Eq (well_ordering (skS.0 0 a)) False) (Or (Eq (well_founded_relation (skS.0 0 a)) True) (Eq False True)) % 5.15/5.39 Clause #69 (by clausification #[5]): ∀ (a : Iota), % 5.15/5.39 Eq % 5.15/5.39 (relation a → % 5.15/5.39 ∀ (B : Iota), % 5.15/5.39 Iff (well_orders a B) % 5.15/5.39 (And % 5.15/5.39 (And (And (And (is_reflexive_in a B) (is_transitive_in a B)) (is_antisymmetric_in a B)) % 5.15/5.39 (is_connected_in a B)) % 5.15/5.39 (is_well_founded_in a B))) % 5.15/5.39 True % 5.15/5.39 Clause #70 (by clausification #[69]): ∀ (a : Iota), % 5.15/5.39 Or (Eq (relation a) False) % 5.15/5.39 (Eq % 5.15/5.39 (∀ (B : Iota), % 5.15/5.39 Iff (well_orders a B) % 5.15/5.39 (And % 5.15/5.39 (And (And (And (is_reflexive_in a B) (is_transitive_in a B)) (is_antisymmetric_in a B)) % 5.15/5.39 (is_connected_in a B)) % 5.15/5.39 (is_well_founded_in a B))) % 5.15/5.39 True) % 5.15/5.39 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), % 5.15/5.39 Or (Eq (relation a) False) % 5.15/5.39 (Eq % 5.15/5.39 (Iff (well_orders a a_1) % 5.15/5.39 (And % 5.15/5.39 (And (And (And (is_reflexive_in a a_1) (is_transitive_in a a_1)) (is_antisymmetric_in a a_1)) % 5.15/5.39 (is_connected_in a a_1)) % 5.15/5.39 (is_well_founded_in a a_1))) % 5.15/5.39 True) % 5.15/5.39 Clause #72 (by clausification #[71]): ∀ (a a_1 : Iota), % 5.15/5.39 Or (Eq (relation a) False) % 5.15/5.39 (Or (Eq (well_orders a a_1) True) % 5.15/5.39 (Eq % 5.15/5.39 (And % 5.15/5.39 (And (And (And (is_reflexive_in a a_1) (is_transitive_in a a_1)) (is_antisymmetric_in a a_1)) % 5.15/5.39 (is_connected_in a a_1)) % 5.15/5.39 (is_well_founded_in a a_1)) % 5.15/5.39 False)) % 5.15/5.39 Clause #73 (by clausification #[71]): ∀ (a a_1 : Iota), % 5.15/5.39 Or (Eq (relation a) False) % 5.15/5.39 (Or (Eq (well_orders a a_1) False) % 5.15/5.39 (Eq % 5.15/5.39 (And % 5.15/5.39 (And (And (And (is_reflexive_in a a_1) (is_transitive_in a a_1)) (is_antisymmetric_in a a_1)) % 5.15/5.39 (is_connected_in a a_1)) % 5.15/5.39 (is_well_founded_in a a_1)) % 5.15/5.39 True)) % 5.15/5.39 Clause #74 (by clausification #[72]): ∀ (a a_1 : Iota), % 5.15/5.39 Or (Eq (relation a) False) % 5.15/5.39 (Or (Eq (well_orders a a_1) True) % 5.15/5.39 (Or % 5.15/5.39 (Eq % 5.15/5.39 (And (And (And (is_reflexive_in a a_1) (is_transitive_in a a_1)) (is_antisymmetric_in a a_1)) % 5.15/5.39 (is_connected_in a a_1)) % 5.25/5.41 False) % 5.25/5.41 (Eq (is_well_founded_in a a_1) False))) % 5.25/5.41 Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota), % 5.25/5.41 Or (Eq (relation a) False) % 5.25/5.41 (Or (Eq (well_orders a a_1) True) % 5.25/5.41 (Or (Eq (is_well_founded_in a a_1) False) % 5.25/5.41 (Or (Eq (And (And (is_reflexive_in a a_1) (is_transitive_in a a_1)) (is_antisymmetric_in a a_1)) False) % 5.25/5.41 (Eq (is_connected_in a a_1) False)))) % 5.25/5.41 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), % 5.25/5.41 Or (Eq (relation a) False) % 5.25/5.41 (Or (Eq (well_orders a a_1) True) % 5.25/5.41 (Or (Eq (is_well_founded_in a a_1) False) % 5.25/5.41 (Or (Eq (is_connected_in a a_1) False) % 5.25/5.41 (Or (Eq (And (is_reflexive_in a a_1) (is_transitive_in a a_1)) False) % 5.25/5.41 (Eq (is_antisymmetric_in a a_1) False))))) % 5.25/5.41 Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota), % 5.25/5.41 Or (Eq (relation a) False) % 5.25/5.41 (Or (Eq (well_orders a a_1) True) % 5.25/5.41 (Or (Eq (is_well_founded_in a a_1) False) % 5.25/5.41 (Or (Eq (is_connected_in a a_1) False) % 5.25/5.41 (Or (Eq (is_antisymmetric_in a a_1) False) % 5.25/5.41 (Or (Eq (is_reflexive_in a a_1) False) (Eq (is_transitive_in a a_1) False)))))) % 5.25/5.41 Clause #78 (by superposition #[77, 41]): ∀ (a a_1 : Iota), % 5.25/5.41 Or (Eq (well_orders (skS.0 0 a) a_1) True) % 5.25/5.41 (Or (Eq (is_well_founded_in (skS.0 0 a) a_1) False) % 5.25/5.41 (Or (Eq (is_connected_in (skS.0 0 a) a_1) False) % 5.25/5.41 (Or (Eq (is_antisymmetric_in (skS.0 0 a) a_1) False) % 5.25/5.41 (Or (Eq (is_reflexive_in (skS.0 0 a) a_1) False) % 5.25/5.41 (Or (Eq (is_transitive_in (skS.0 0 a) a_1) False) (Eq False True)))))) % 5.25/5.41 Clause #79 (by clausification #[68]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) False) (Eq (well_founded_relation (skS.0 0 a)) True) % 5.25/5.41 Clause #80 (by clausification #[67]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (connected a) True)) % 5.25/5.41 Clause #81 (by clausification #[67]): ∀ (a : Iota), % 5.25/5.41 Or (Eq (relation a) False) % 5.25/5.41 (Or (Eq (well_ordering a) False) (Eq (And (And (reflexive a) (transitive a)) (antisymmetric a)) True)) % 5.25/5.41 Clause #82 (by superposition #[80, 41]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) False) (Or (Eq (connected (skS.0 0 a)) True) (Eq False True)) % 5.25/5.41 Clause #83 (by clausification #[81]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (antisymmetric a) True)) % 5.25/5.41 Clause #84 (by clausification #[81]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (And (reflexive a) (transitive a)) True)) % 5.25/5.41 Clause #85 (by superposition #[83, 41]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) False) (Or (Eq (antisymmetric (skS.0 0 a)) True) (Eq False True)) % 5.25/5.41 Clause #86 (by clausification #[84]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (transitive a) True)) % 5.25/5.41 Clause #87 (by clausification #[84]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (reflexive a) True)) % 5.25/5.41 Clause #88 (by superposition #[86, 41]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) False) (Or (Eq (transitive (skS.0 0 a)) True) (Eq False True)) % 5.25/5.41 Clause #89 (by superposition #[87, 41]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) False) (Or (Eq (reflexive (skS.0 0 a)) True) (Eq False True)) % 5.25/5.41 Clause #90 (by clausification #[42]): ∀ (a : Iota), % 5.25/5.41 Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) False) (Eq (well_ordering (skS.0 0 a)) False) % 5.25/5.41 Clause #91 (by clausification #[42]): ∀ (a : Iota), Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) True) (Eq (well_ordering (skS.0 0 a)) True) % 5.25/5.41 Clause #92 (by clausification #[82]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) False) (Eq (connected (skS.0 0 a)) True) % 5.25/5.41 Clause #93 (by clausification #[89]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) False) (Eq (reflexive (skS.0 0 a)) True) % 5.25/5.41 Clause #94 (by clausification #[85]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) False) (Eq (antisymmetric (skS.0 0 a)) True) % 5.25/5.41 Clause #95 (by clausification #[88]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) False) (Eq (transitive (skS.0 0 a)) True) % 5.25/5.41 Clause #97 (by clausification #[43]): ∀ (a : Iota), % 5.25/5.44 Or (Eq (well_founded_relation (skS.0 0 a)) True) % 5.25/5.44 (Eq (is_well_founded_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.25/5.44 Clause #100 (by clausification #[59]): ∀ (a : Iota), Or (Eq (reflexive (skS.0 0 a)) False) (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.44 Clause #101 (by clausification #[60]): ∀ (a : Iota), % 5.25/5.44 Or (Eq (transitive (skS.0 0 a)) False) (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.44 Clause #102 (by clausification #[48]): ∀ (a : Iota), % 5.25/5.44 Or (Eq (antisymmetric (skS.0 0 a)) False) (Eq (is_antisymmetric_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.44 Clause #103 (by clausification #[44]): ∀ (a : Iota), Or (Eq (reflexive (skS.0 0 a)) True) (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.25/5.44 Clause #104 (by clausification #[61]): ∀ (a : Iota), Or (Eq (connected (skS.0 0 a)) False) (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.44 Clause #105 (by clausification #[45]): ∀ (a : Iota), % 5.25/5.44 Or (Eq (transitive (skS.0 0 a)) True) (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.25/5.44 Clause #106 (by clausification #[47]): ∀ (a : Iota), % 5.25/5.44 Or (Eq (antisymmetric (skS.0 0 a)) True) (Eq (is_antisymmetric_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.25/5.44 Clause #107 (by clausification #[46]): ∀ (a : Iota), Or (Eq (connected (skS.0 0 a)) True) (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.25/5.44 Clause #108 (by clausification #[49]): ∀ (a : Iota), % 5.25/5.44 Or (Eq (well_founded_relation (skS.0 0 a)) False) % 5.25/5.44 (Eq (is_well_founded_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.44 Clause #109 (by clausification #[58]): ∀ (a : Iota), % 5.25/5.44 Or (Eq (well_ordering (skS.0 0 a)) True) % 5.25/5.44 (Or (Eq (well_founded_relation (skS.0 0 a)) False) % 5.25/5.44 (Or (Eq (connected (skS.0 0 a)) False) % 5.25/5.44 (Or (Eq (antisymmetric (skS.0 0 a)) False) % 5.25/5.44 (Or (Eq (reflexive (skS.0 0 a)) False) (Eq (transitive (skS.0 0 a)) False))))) % 5.25/5.44 Clause #110 (by clausification #[73]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Or (Eq (well_orders a a_1) False) (Eq (is_well_founded_in a a_1) True)) % 5.25/5.44 Clause #111 (by clausification #[73]): ∀ (a a_1 : Iota), % 5.25/5.44 Or (Eq (relation a) False) % 5.25/5.44 (Or (Eq (well_orders a a_1) False) % 5.25/5.44 (Eq % 5.25/5.44 (And (And (And (is_reflexive_in a a_1) (is_transitive_in a a_1)) (is_antisymmetric_in a a_1)) % 5.25/5.44 (is_connected_in a a_1)) % 5.25/5.44 True)) % 5.25/5.44 Clause #112 (by superposition #[110, 41]): ∀ (a a_1 : Iota), % 5.25/5.44 Or (Eq (well_orders (skS.0 0 a) a_1) False) (Or (Eq (is_well_founded_in (skS.0 0 a) a_1) True) (Eq False True)) % 5.25/5.44 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Or (Eq (well_orders (skS.0 0 a) a_1) False) (Eq (is_well_founded_in (skS.0 0 a) a_1) True) % 5.25/5.44 Clause #114 (by superposition #[113, 91]): ∀ (a : Iota), % 5.25/5.44 Or (Eq (is_well_founded_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.44 (Or (Eq False True) (Eq (well_ordering (skS.0 0 a)) True)) % 5.25/5.44 Clause #115 (by clausification #[111]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Or (Eq (well_orders a a_1) False) (Eq (is_connected_in a a_1) True)) % 5.25/5.44 Clause #116 (by clausification #[111]): ∀ (a a_1 : Iota), % 5.25/5.44 Or (Eq (relation a) False) % 5.25/5.44 (Or (Eq (well_orders a a_1) False) % 5.25/5.44 (Eq (And (And (is_reflexive_in a a_1) (is_transitive_in a a_1)) (is_antisymmetric_in a a_1)) True)) % 5.25/5.44 Clause #117 (by superposition #[115, 41]): ∀ (a a_1 : Iota), % 5.25/5.44 Or (Eq (well_orders (skS.0 0 a) a_1) False) (Or (Eq (is_connected_in (skS.0 0 a) a_1) True) (Eq False True)) % 5.25/5.44 Clause #118 (by clausification #[116]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Or (Eq (well_orders a a_1) False) (Eq (is_antisymmetric_in a a_1) True)) % 5.25/5.44 Clause #119 (by clausification #[116]): ∀ (a a_1 : Iota), % 5.25/5.44 Or (Eq (relation a) False) % 5.25/5.44 (Or (Eq (well_orders a a_1) False) (Eq (And (is_reflexive_in a a_1) (is_transitive_in a a_1)) True)) % 5.25/5.44 Clause #120 (by superposition #[118, 41]): ∀ (a a_1 : Iota), % 5.25/5.44 Or (Eq (well_orders (skS.0 0 a) a_1) False) (Or (Eq (is_antisymmetric_in (skS.0 0 a) a_1) True) (Eq False True)) % 5.25/5.47 Clause #121 (by clausification #[119]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Or (Eq (well_orders a a_1) False) (Eq (is_transitive_in a a_1) True)) % 5.25/5.47 Clause #122 (by clausification #[119]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Or (Eq (well_orders a a_1) False) (Eq (is_reflexive_in a a_1) True)) % 5.25/5.47 Clause #123 (by superposition #[121, 41]): ∀ (a a_1 : Iota), % 5.25/5.47 Or (Eq (well_orders (skS.0 0 a) a_1) False) (Or (Eq (is_transitive_in (skS.0 0 a) a_1) True) (Eq False True)) % 5.25/5.47 Clause #124 (by clausification #[78]): ∀ (a a_1 : Iota), % 5.25/5.47 Or (Eq (well_orders (skS.0 0 a) a_1) True) % 5.25/5.47 (Or (Eq (is_well_founded_in (skS.0 0 a) a_1) False) % 5.25/5.47 (Or (Eq (is_connected_in (skS.0 0 a) a_1) False) % 5.25/5.47 (Or (Eq (is_antisymmetric_in (skS.0 0 a) a_1) False) % 5.25/5.47 (Or (Eq (is_reflexive_in (skS.0 0 a) a_1) False) (Eq (is_transitive_in (skS.0 0 a) a_1) False))))) % 5.25/5.47 Clause #125 (by superposition #[122, 41]): ∀ (a a_1 : Iota), % 5.25/5.47 Or (Eq (well_orders (skS.0 0 a) a_1) False) (Or (Eq (is_reflexive_in (skS.0 0 a) a_1) True) (Eq False True)) % 5.25/5.47 Clause #126 (by clausification #[125]): ∀ (a a_1 : Iota), Or (Eq (well_orders (skS.0 0 a) a_1) False) (Eq (is_reflexive_in (skS.0 0 a) a_1) True) % 5.25/5.47 Clause #127 (by superposition #[126, 91]): ∀ (a : Iota), % 5.25/5.47 Or (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.47 (Or (Eq False True) (Eq (well_ordering (skS.0 0 a)) True)) % 5.25/5.47 Clause #128 (by clausification #[123]): ∀ (a a_1 : Iota), Or (Eq (well_orders (skS.0 0 a) a_1) False) (Eq (is_transitive_in (skS.0 0 a) a_1) True) % 5.25/5.47 Clause #129 (by superposition #[128, 91]): ∀ (a : Iota), % 5.25/5.47 Or (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.47 (Or (Eq False True) (Eq (well_ordering (skS.0 0 a)) True)) % 5.25/5.47 Clause #130 (by clausification #[117]): ∀ (a a_1 : Iota), Or (Eq (well_orders (skS.0 0 a) a_1) False) (Eq (is_connected_in (skS.0 0 a) a_1) True) % 5.25/5.47 Clause #131 (by superposition #[130, 91]): ∀ (a : Iota), % 5.25/5.47 Or (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.47 (Or (Eq False True) (Eq (well_ordering (skS.0 0 a)) True)) % 5.25/5.47 Clause #132 (by clausification #[120]): ∀ (a a_1 : Iota), Or (Eq (well_orders (skS.0 0 a) a_1) False) (Eq (is_antisymmetric_in (skS.0 0 a) a_1) True) % 5.25/5.47 Clause #133 (by superposition #[132, 91]): ∀ (a : Iota), % 5.25/5.47 Or (Eq (is_antisymmetric_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.47 (Or (Eq False True) (Eq (well_ordering (skS.0 0 a)) True)) % 5.25/5.47 Clause #134 (by clausification #[114]): ∀ (a : Iota), % 5.25/5.47 Or (Eq (is_well_founded_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) (Eq (well_ordering (skS.0 0 a)) True) % 5.25/5.47 Clause #135 (by superposition #[134, 97]): ∀ (a : Iota), % 5.25/5.47 Or (Eq (well_ordering (skS.0 0 a)) True) (Or (Eq (well_founded_relation (skS.0 0 a)) True) (Eq True False)) % 5.25/5.47 Clause #137 (by clausification #[135]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Eq (well_founded_relation (skS.0 0 a)) True) % 5.25/5.47 Clause #138 (by superposition #[137, 79]): ∀ (a : Iota), % 5.25/5.47 Or (Eq (well_founded_relation (skS.0 0 a)) True) (Or (Eq True False) (Eq (well_founded_relation (skS.0 0 a)) True)) % 5.25/5.47 Clause #152 (by clausification #[127]): ∀ (a : Iota), % 5.25/5.47 Or (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) (Eq (well_ordering (skS.0 0 a)) True) % 5.25/5.47 Clause #153 (by superposition #[152, 103]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Or (Eq (reflexive (skS.0 0 a)) True) (Eq True False)) % 5.25/5.47 Clause #154 (by clausification #[153]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Eq (reflexive (skS.0 0 a)) True) % 5.25/5.47 Clause #157 (by superposition #[154, 93]): ∀ (a : Iota), Or (Eq (reflexive (skS.0 0 a)) True) (Or (Eq True False) (Eq (reflexive (skS.0 0 a)) True)) % 5.25/5.47 Clause #163 (by clausification #[157]): ∀ (a : Iota), Or (Eq (reflexive (skS.0 0 a)) True) (Eq (reflexive (skS.0 0 a)) True) % 5.25/5.47 Clause #164 (by eliminate duplicate literals #[163]): ∀ (a : Iota), Eq (reflexive (skS.0 0 a)) True % 5.25/5.47 Clause #166 (by backward demodulation #[164, 100]): ∀ (a : Iota), Or (Eq True False) (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.25/5.47 Clause #168 (by backward demodulation #[164, 109]): ∀ (a : Iota), % 5.32/5.49 Or (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.49 (Or (Eq (well_founded_relation (skS.0 0 a)) False) % 5.32/5.49 (Or (Eq (connected (skS.0 0 a)) False) % 5.32/5.49 (Or (Eq (antisymmetric (skS.0 0 a)) False) (Or (Eq True False) (Eq (transitive (skS.0 0 a)) False))))) % 5.32/5.49 Clause #171 (by clausification #[129]): ∀ (a : Iota), % 5.32/5.49 Or (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.49 Clause #172 (by superposition #[171, 105]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Or (Eq (transitive (skS.0 0 a)) True) (Eq True False)) % 5.32/5.49 Clause #173 (by clausification #[166]): ∀ (a : Iota), Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True % 5.32/5.49 Clause #176 (by clausification #[131]): ∀ (a : Iota), % 5.32/5.49 Or (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.49 Clause #177 (by superposition #[176, 107]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Or (Eq (connected (skS.0 0 a)) True) (Eq True False)) % 5.32/5.49 Clause #178 (by clausification #[177]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Eq (connected (skS.0 0 a)) True) % 5.32/5.49 Clause #180 (by clausification #[172]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Eq (transitive (skS.0 0 a)) True) % 5.32/5.49 Clause #183 (by clausification #[138]): ∀ (a : Iota), Or (Eq (well_founded_relation (skS.0 0 a)) True) (Eq (well_founded_relation (skS.0 0 a)) True) % 5.32/5.49 Clause #184 (by eliminate duplicate literals #[183]): ∀ (a : Iota), Eq (well_founded_relation (skS.0 0 a)) True % 5.32/5.49 Clause #186 (by backward demodulation #[184, 108]): ∀ (a : Iota), Or (Eq True False) (Eq (is_well_founded_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.49 Clause #187 (by clausification #[186]): ∀ (a : Iota), Eq (is_well_founded_in (skS.0 0 a) (relation_field (skS.0 0 a))) True % 5.32/5.49 Clause #188 (by superposition #[187, 124]): ∀ (a : Iota), % 5.32/5.49 Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.49 (Or (Eq True False) % 5.32/5.49 (Or (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.49 (Or (Eq (is_antisymmetric_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.49 (Or (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.49 (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False))))) % 5.32/5.49 Clause #189 (by clausification #[133]): ∀ (a : Iota), % 5.32/5.49 Or (Eq (is_antisymmetric_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.49 Clause #190 (by superposition #[189, 106]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Or (Eq (antisymmetric (skS.0 0 a)) True) (Eq True False)) % 5.32/5.49 Clause #191 (by clausification #[190]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Eq (antisymmetric (skS.0 0 a)) True) % 5.32/5.49 Clause #193 (by superposition #[191, 94]): ∀ (a : Iota), Or (Eq (antisymmetric (skS.0 0 a)) True) (Or (Eq True False) (Eq (antisymmetric (skS.0 0 a)) True)) % 5.32/5.49 Clause #197 (by clausification #[193]): ∀ (a : Iota), Or (Eq (antisymmetric (skS.0 0 a)) True) (Eq (antisymmetric (skS.0 0 a)) True) % 5.32/5.49 Clause #198 (by eliminate duplicate literals #[197]): ∀ (a : Iota), Eq (antisymmetric (skS.0 0 a)) True % 5.32/5.49 Clause #199 (by backward demodulation #[198, 102]): ∀ (a : Iota), Or (Eq True False) (Eq (is_antisymmetric_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.49 Clause #204 (by clausification #[199]): ∀ (a : Iota), Eq (is_antisymmetric_in (skS.0 0 a) (relation_field (skS.0 0 a))) True % 5.32/5.49 Clause #219 (by clausification #[168]): ∀ (a : Iota), % 5.32/5.49 Or (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.49 (Or (Eq (well_founded_relation (skS.0 0 a)) False) % 5.32/5.49 (Or (Eq (connected (skS.0 0 a)) False) % 5.32/5.49 (Or (Eq (antisymmetric (skS.0 0 a)) False) (Eq (transitive (skS.0 0 a)) False)))) % 5.32/5.49 Clause #220 (by forward demodulation #[219, 184]): ∀ (a : Iota), % 5.32/5.49 Or (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.49 (Or (Eq True False) % 5.32/5.49 (Or (Eq (connected (skS.0 0 a)) False) % 5.32/5.49 (Or (Eq (antisymmetric (skS.0 0 a)) False) (Eq (transitive (skS.0 0 a)) False)))) % 5.32/5.52 Clause #221 (by clausification #[220]): ∀ (a : Iota), % 5.32/5.52 Or (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.52 (Or (Eq (connected (skS.0 0 a)) False) % 5.32/5.52 (Or (Eq (antisymmetric (skS.0 0 a)) False) (Eq (transitive (skS.0 0 a)) False))) % 5.32/5.52 Clause #222 (by forward demodulation #[221, 198]): ∀ (a : Iota), % 5.32/5.52 Or (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.52 (Or (Eq (connected (skS.0 0 a)) False) (Or (Eq True False) (Eq (transitive (skS.0 0 a)) False))) % 5.32/5.52 Clause #223 (by clausification #[222]): ∀ (a : Iota), % 5.32/5.52 Or (Eq (well_ordering (skS.0 0 a)) True) (Or (Eq (connected (skS.0 0 a)) False) (Eq (transitive (skS.0 0 a)) False)) % 5.32/5.52 Clause #224 (by superposition #[223, 178]): ∀ (a : Iota), % 5.32/5.52 Or (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.52 (Or (Eq (transitive (skS.0 0 a)) False) (Or (Eq (well_ordering (skS.0 0 a)) True) (Eq False True))) % 5.32/5.52 Clause #225 (by clausification #[224]): ∀ (a : Iota), % 5.32/5.52 Or (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.52 (Or (Eq (transitive (skS.0 0 a)) False) (Eq (well_ordering (skS.0 0 a)) True)) % 5.32/5.52 Clause #226 (by eliminate duplicate literals #[225]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Eq (transitive (skS.0 0 a)) False) % 5.32/5.52 Clause #227 (by superposition #[226, 180]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Or (Eq (well_ordering (skS.0 0 a)) True) (Eq False True)) % 5.32/5.52 Clause #228 (by clausification #[227]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 0 a)) True) (Eq (well_ordering (skS.0 0 a)) True) % 5.32/5.52 Clause #229 (by eliminate duplicate literals #[228]): ∀ (a : Iota), Eq (well_ordering (skS.0 0 a)) True % 5.32/5.52 Clause #230 (by backward demodulation #[229, 90]): ∀ (a : Iota), Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) False) (Eq True False) % 5.32/5.52 Clause #231 (by backward demodulation #[229, 92]): ∀ (a : Iota), Or (Eq True False) (Eq (connected (skS.0 0 a)) True) % 5.32/5.52 Clause #232 (by backward demodulation #[229, 95]): ∀ (a : Iota), Or (Eq True False) (Eq (transitive (skS.0 0 a)) True) % 5.32/5.52 Clause #237 (by clausification #[232]): ∀ (a : Iota), Eq (transitive (skS.0 0 a)) True % 5.32/5.52 Clause #238 (by backward demodulation #[237, 101]): ∀ (a : Iota), Or (Eq True False) (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.52 Clause #240 (by clausification #[231]): ∀ (a : Iota), Eq (connected (skS.0 0 a)) True % 5.32/5.52 Clause #241 (by backward demodulation #[240, 104]): ∀ (a : Iota), Or (Eq True False) (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.52 Clause #243 (by clausification #[188]): ∀ (a : Iota), % 5.32/5.52 Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.52 (Or (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.52 (Or (Eq (is_antisymmetric_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.52 (Or (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.52 (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False)))) % 5.32/5.52 Clause #244 (by forward demodulation #[243, 204]): ∀ (a : Iota), % 5.32/5.52 Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.52 (Or (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.52 (Or (Eq True False) % 5.32/5.52 (Or (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.52 (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False)))) % 5.32/5.52 Clause #245 (by clausification #[244]): ∀ (a : Iota), % 5.32/5.52 Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.52 (Or (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.52 (Or (Eq (is_reflexive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.52 (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False))) % 5.32/5.52 Clause #246 (by forward demodulation #[245, 173]): ∀ (a : Iota), % 5.32/5.52 Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.52 (Or (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.52 (Or (Eq True False) (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False))) % 5.32/5.52 Clause #247 (by clausification #[246]): ∀ (a : Iota), % 5.32/5.52 Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.53 (Or (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.53 (Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) False)) % 5.32/5.53 Clause #248 (by clausification #[238]): ∀ (a : Iota), Eq (is_transitive_in (skS.0 0 a) (relation_field (skS.0 0 a))) True % 5.32/5.53 Clause #249 (by backward demodulation #[248, 247]): ∀ (a : Iota), % 5.32/5.53 Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.53 (Or (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) (Eq True False)) % 5.32/5.53 Clause #250 (by clausification #[230]): ∀ (a : Iota), Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) False % 5.32/5.53 Clause #251 (by clausification #[241]): ∀ (a : Iota), Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) True % 5.32/5.53 Clause #252 (by clausification #[249]): ∀ (a : Iota), % 5.32/5.53 Or (Eq (well_orders (skS.0 0 a) (relation_field (skS.0 0 a))) True) % 5.32/5.53 (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.53 Clause #253 (by forward demodulation #[252, 250]): ∀ (a : Iota), Or (Eq False True) (Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False) % 5.32/5.53 Clause #254 (by clausification #[253]): ∀ (a : Iota), Eq (is_connected_in (skS.0 0 a) (relation_field (skS.0 0 a))) False % 5.32/5.53 Clause #255 (by superposition #[254, 251]): Eq False True % 5.32/5.53 Clause #256 (by clausification #[255]): False % 5.32/5.53 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------