%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU261+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n023.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:15 PM UTC 2025 % Result : Theorem 6.90s 7.07s % Output : Proof 7.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU261+1 : TPTP v9.2.0. Released v3.3.0. % 0.03/0.14 % Command : duper %s % 0.13/0.35 % Computer : n023.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 05:10:23 EDT 2025 % 0.13/0.35 % CPUTime : % 6.90/7.07 SZS status Theorem for theBenchmark.p % 6.90/7.07 SZS output start Proof for theBenchmark.p % 6.90/7.07 Clause #0 (by assumption #[]): Eq % 6.90/7.07 (∀ (A : Iota), % 6.90/7.07 relation A → % 6.90/7.07 Iff (well_ordering A) % 6.90/7.07 (And (And (And (And (reflexive A) (transitive A)) (antisymmetric A)) (connected A)) (well_founded_relation A))) % 6.90/7.07 True % 6.90/7.07 Clause #2 (by assumption #[]): Eq % 6.90/7.07 (∀ (A : Iota), % 6.90/7.07 relation A → % 6.90/7.07 ∀ (B : Iota), % 6.90/7.07 relation B → % 6.90/7.07 ∀ (C : Iota), % 6.90/7.07 And (relation C) (function C) → % 6.90/7.07 relation_isomorphism A B C → % 6.90/7.07 And % 6.90/7.07 (And (And (And (reflexive A → reflexive B) (transitive A → transitive B)) (connected A → connected B)) % 6.90/7.07 (antisymmetric A → antisymmetric B)) % 6.90/7.07 (well_founded_relation A → well_founded_relation B)) % 6.90/7.07 True % 6.90/7.07 Clause #3 (by assumption #[]): Eq % 6.90/7.07 (Not % 6.90/7.07 (∀ (A : Iota), % 6.90/7.07 relation A → % 6.90/7.07 ∀ (B : Iota), % 6.90/7.07 relation B → % 6.90/7.07 ∀ (C : Iota), % 6.90/7.07 And (relation C) (function C) → And (well_ordering A) (relation_isomorphism A B C) → well_ordering B)) % 6.90/7.07 True % 6.90/7.07 Clause #7 (by clausification #[3]): Eq % 6.90/7.07 (∀ (A : Iota), % 6.90/7.07 relation A → % 6.90/7.07 ∀ (B : Iota), % 6.90/7.07 relation B → % 6.90/7.07 ∀ (C : Iota), % 6.90/7.07 And (relation C) (function C) → And (well_ordering A) (relation_isomorphism A B C) → well_ordering B) % 6.90/7.07 False % 6.90/7.07 Clause #8 (by clausification #[7]): ∀ (a : Iota), % 6.90/7.07 Eq % 6.90/7.07 (Not % 6.90/7.07 (relation (skS.0 1 a) → % 6.90/7.07 ∀ (B : Iota), % 6.90/7.07 relation B → % 6.90/7.07 ∀ (C : Iota), % 6.90/7.07 And (relation C) (function C) → % 6.90/7.07 And (well_ordering (skS.0 1 a)) (relation_isomorphism (skS.0 1 a) B C) → well_ordering B)) % 6.90/7.07 True % 6.90/7.07 Clause #9 (by clausification #[8]): ∀ (a : Iota), % 6.90/7.07 Eq % 6.90/7.07 (relation (skS.0 1 a) → % 6.90/7.07 ∀ (B : Iota), % 6.90/7.07 relation B → % 6.90/7.07 ∀ (C : Iota), % 6.90/7.07 And (relation C) (function C) → % 6.90/7.07 And (well_ordering (skS.0 1 a)) (relation_isomorphism (skS.0 1 a) B C) → well_ordering B) % 6.90/7.07 False % 6.90/7.07 Clause #10 (by clausification #[9]): ∀ (a : Iota), Eq (relation (skS.0 1 a)) True % 6.90/7.07 Clause #11 (by clausification #[9]): ∀ (a : Iota), % 6.90/7.07 Eq % 6.90/7.07 (∀ (B : Iota), % 6.90/7.07 relation B → % 6.90/7.07 ∀ (C : Iota), % 6.90/7.07 And (relation C) (function C) → % 6.90/7.07 And (well_ordering (skS.0 1 a)) (relation_isomorphism (skS.0 1 a) B C) → well_ordering B) % 6.90/7.07 False % 6.90/7.07 Clause #12 (by clausification #[11]): ∀ (a a_1 : Iota), % 6.90/7.07 Eq % 6.90/7.07 (Not % 6.90/7.07 (relation (skS.0 2 a a_1) → % 6.90/7.07 ∀ (C : Iota), % 6.90/7.07 And (relation C) (function C) → % 6.90/7.07 And (well_ordering (skS.0 1 a)) (relation_isomorphism (skS.0 1 a) (skS.0 2 a a_1) C) → % 6.90/7.07 well_ordering (skS.0 2 a a_1))) % 6.90/7.07 True % 6.90/7.07 Clause #13 (by clausification #[12]): ∀ (a a_1 : Iota), % 6.90/7.07 Eq % 6.90/7.07 (relation (skS.0 2 a a_1) → % 6.90/7.07 ∀ (C : Iota), % 6.90/7.07 And (relation C) (function C) → % 6.90/7.07 And (well_ordering (skS.0 1 a)) (relation_isomorphism (skS.0 1 a) (skS.0 2 a a_1) C) → % 6.90/7.07 well_ordering (skS.0 2 a a_1)) % 6.90/7.07 False % 6.90/7.07 Clause #14 (by clausification #[13]): ∀ (a a_1 : Iota), Eq (relation (skS.0 2 a a_1)) True % 6.90/7.07 Clause #15 (by clausification #[13]): ∀ (a a_1 : Iota), % 6.90/7.07 Eq % 6.90/7.07 (∀ (C : Iota), % 6.90/7.07 And (relation C) (function C) → % 6.90/7.07 And (well_ordering (skS.0 1 a)) (relation_isomorphism (skS.0 1 a) (skS.0 2 a a_1) C) → % 6.90/7.07 well_ordering (skS.0 2 a a_1)) % 6.90/7.07 False % 6.90/7.07 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 : Iota), % 6.90/7.07 Eq % 6.90/7.07 (Not % 6.90/7.07 (And (relation (skS.0 3 a a_1 a_2)) (function (skS.0 3 a a_1 a_2)) → % 6.90/7.07 And (well_ordering (skS.0 1 a)) (relation_isomorphism (skS.0 1 a) (skS.0 2 a a_1) (skS.0 3 a a_1 a_2)) → % 6.90/7.07 well_ordering (skS.0 2 a a_1))) % 6.90/7.07 True % 6.90/7.07 Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 : Iota), % 6.90/7.07 Eq % 6.90/7.07 (And (relation (skS.0 3 a a_1 a_2)) (function (skS.0 3 a a_1 a_2)) → % 6.90/7.07 And (well_ordering (skS.0 1 a)) (relation_isomorphism (skS.0 1 a) (skS.0 2 a a_1) (skS.0 3 a a_1 a_2)) → % 6.90/7.07 well_ordering (skS.0 2 a a_1)) % 6.90/7.07 False % 6.90/7.07 Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), Eq (And (relation (skS.0 3 a a_1 a_2)) (function (skS.0 3 a a_1 a_2))) True % 6.90/7.10 Clause #19 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), % 6.90/7.10 Eq % 6.90/7.10 (And (well_ordering (skS.0 1 a)) (relation_isomorphism (skS.0 1 a) (skS.0 2 a a_1) (skS.0 3 a a_1 a_2)) → % 6.90/7.10 well_ordering (skS.0 2 a a_1)) % 6.90/7.10 False % 6.90/7.10 Clause #20 (by clausification #[18]): ∀ (a a_1 a_2 : Iota), Eq (function (skS.0 3 a a_1 a_2)) True % 6.90/7.10 Clause #21 (by clausification #[18]): ∀ (a a_1 a_2 : Iota), Eq (relation (skS.0 3 a a_1 a_2)) True % 6.90/7.10 Clause #22 (by clausification #[0]): ∀ (a : Iota), % 6.90/7.10 Eq % 6.90/7.10 (relation a → % 6.90/7.10 Iff (well_ordering a) % 6.90/7.10 (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a))) % 6.90/7.10 True % 6.90/7.10 Clause #23 (by clausification #[22]): ∀ (a : Iota), % 6.90/7.10 Or (Eq (relation a) False) % 6.90/7.10 (Eq % 6.90/7.10 (Iff (well_ordering a) % 6.90/7.10 (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a))) % 6.90/7.10 True) % 6.90/7.10 Clause #24 (by clausification #[23]): ∀ (a : Iota), % 6.90/7.10 Or (Eq (relation a) False) % 6.90/7.10 (Or (Eq (well_ordering a) True) % 6.90/7.10 (Eq (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a)) % 6.90/7.10 False)) % 6.90/7.10 Clause #25 (by clausification #[23]): ∀ (a : Iota), % 6.90/7.10 Or (Eq (relation a) False) % 6.90/7.10 (Or (Eq (well_ordering a) False) % 6.90/7.10 (Eq (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a)) % 6.90/7.10 True)) % 6.90/7.10 Clause #26 (by clausification #[24]): ∀ (a : Iota), % 6.90/7.10 Or (Eq (relation a) False) % 6.90/7.10 (Or (Eq (well_ordering a) True) % 6.90/7.10 (Or (Eq (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) False) % 6.90/7.10 (Eq (well_founded_relation a) False))) % 6.90/7.10 Clause #27 (by clausification #[26]): ∀ (a : Iota), % 6.90/7.10 Or (Eq (relation a) False) % 6.90/7.10 (Or (Eq (well_ordering a) True) % 6.90/7.10 (Or (Eq (well_founded_relation a) False) % 6.90/7.10 (Or (Eq (And (And (reflexive a) (transitive a)) (antisymmetric a)) False) (Eq (connected a) False)))) % 6.90/7.10 Clause #28 (by clausification #[27]): ∀ (a : Iota), % 6.90/7.10 Or (Eq (relation a) False) % 6.90/7.10 (Or (Eq (well_ordering a) True) % 6.90/7.10 (Or (Eq (well_founded_relation a) False) % 6.90/7.10 (Or (Eq (connected a) False) (Or (Eq (And (reflexive a) (transitive a)) False) (Eq (antisymmetric a) False))))) % 6.90/7.10 Clause #29 (by clausification #[28]): ∀ (a : Iota), % 6.90/7.10 Or (Eq (relation a) False) % 6.90/7.10 (Or (Eq (well_ordering a) True) % 6.90/7.10 (Or (Eq (well_founded_relation a) False) % 6.90/7.10 (Or (Eq (connected a) False) % 6.90/7.10 (Or (Eq (antisymmetric a) False) (Or (Eq (reflexive a) False) (Eq (transitive a) False)))))) % 6.90/7.10 Clause #32 (by superposition #[29, 14]): ∀ (a a_1 : Iota), % 6.90/7.10 Or (Eq (well_ordering (skS.0 2 a a_1)) True) % 6.90/7.10 (Or (Eq (well_founded_relation (skS.0 2 a a_1)) False) % 6.90/7.10 (Or (Eq (connected (skS.0 2 a a_1)) False) % 6.90/7.10 (Or (Eq (antisymmetric (skS.0 2 a a_1)) False) % 6.90/7.10 (Or (Eq (reflexive (skS.0 2 a a_1)) False) (Or (Eq (transitive (skS.0 2 a a_1)) False) (Eq False True)))))) % 6.90/7.10 Clause #33 (by clausification #[19]): ∀ (a a_1 a_2 : Iota), % 6.90/7.10 Eq (And (well_ordering (skS.0 1 a)) (relation_isomorphism (skS.0 1 a) (skS.0 2 a a_1) (skS.0 3 a a_1 a_2))) True % 6.90/7.10 Clause #34 (by clausification #[19]): ∀ (a a_1 : Iota), Eq (well_ordering (skS.0 2 a a_1)) False % 6.90/7.10 Clause #35 (by clausification #[33]): ∀ (a a_1 a_2 : Iota), Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a a_1) (skS.0 3 a a_1 a_2)) True % 6.90/7.10 Clause #36 (by clausification #[33]): ∀ (a : Iota), Eq (well_ordering (skS.0 1 a)) True % 6.90/7.10 Clause #38 (by clausification #[25]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (well_founded_relation a) True)) % 6.90/7.10 Clause #39 (by clausification #[25]): ∀ (a : Iota), % 6.90/7.10 Or (Eq (relation a) False) % 6.90/7.10 (Or (Eq (well_ordering a) False) % 6.90/7.10 (Eq (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) True)) % 6.90/7.10 Clause #41 (by superposition #[38, 10]): ∀ (a : Iota), % 6.90/7.10 Or (Eq (well_ordering (skS.0 1 a)) False) (Or (Eq (well_founded_relation (skS.0 1 a)) True) (Eq False True)) % 6.90/7.10 Clause #44 (by clausification #[2]): ∀ (a : Iota), % 6.90/7.11 Eq % 6.90/7.11 (relation a → % 6.90/7.11 ∀ (B : Iota), % 6.90/7.11 relation B → % 6.90/7.11 ∀ (C : Iota), % 6.90/7.11 And (relation C) (function C) → % 6.90/7.11 relation_isomorphism a B C → % 6.90/7.11 And % 6.90/7.11 (And (And (And (reflexive a → reflexive B) (transitive a → transitive B)) (connected a → connected B)) % 6.90/7.11 (antisymmetric a → antisymmetric B)) % 6.90/7.11 (well_founded_relation a → well_founded_relation B)) % 6.90/7.11 True % 6.90/7.11 Clause #45 (by clausification #[44]): ∀ (a : Iota), % 6.90/7.11 Or (Eq (relation a) False) % 6.90/7.11 (Eq % 6.90/7.11 (∀ (B : Iota), % 6.90/7.11 relation B → % 6.90/7.11 ∀ (C : Iota), % 6.90/7.11 And (relation C) (function C) → % 6.90/7.11 relation_isomorphism a B C → % 6.90/7.11 And % 6.90/7.11 (And (And (And (reflexive a → reflexive B) (transitive a → transitive B)) (connected a → connected B)) % 6.90/7.11 (antisymmetric a → antisymmetric B)) % 6.90/7.11 (well_founded_relation a → well_founded_relation B)) % 6.90/7.11 True) % 6.90/7.11 Clause #46 (by clausification #[45]): ∀ (a a_1 : Iota), % 6.90/7.11 Or (Eq (relation a) False) % 6.90/7.11 (Eq % 6.90/7.11 (relation a_1 → % 6.90/7.11 ∀ (C : Iota), % 6.90/7.11 And (relation C) (function C) → % 6.90/7.11 relation_isomorphism a a_1 C → % 6.90/7.11 And % 6.90/7.11 (And % 6.90/7.11 (And (And (reflexive a → reflexive a_1) (transitive a → transitive a_1)) % 6.90/7.11 (connected a → connected a_1)) % 6.90/7.11 (antisymmetric a → antisymmetric a_1)) % 6.90/7.11 (well_founded_relation a → well_founded_relation a_1)) % 6.90/7.11 True) % 6.90/7.11 Clause #47 (by clausification #[46]): ∀ (a a_1 : Iota), % 6.90/7.11 Or (Eq (relation a) False) % 6.90/7.11 (Or (Eq (relation a_1) False) % 6.90/7.11 (Eq % 6.90/7.11 (∀ (C : Iota), % 6.90/7.11 And (relation C) (function C) → % 6.90/7.11 relation_isomorphism a a_1 C → % 6.90/7.11 And % 6.90/7.11 (And % 6.90/7.11 (And (And (reflexive a → reflexive a_1) (transitive a → transitive a_1)) % 6.90/7.11 (connected a → connected a_1)) % 6.90/7.11 (antisymmetric a → antisymmetric a_1)) % 6.90/7.11 (well_founded_relation a → well_founded_relation a_1)) % 6.90/7.11 True)) % 6.90/7.11 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 : Iota), % 6.90/7.11 Or (Eq (relation a) False) % 6.90/7.11 (Or (Eq (relation a_1) False) % 6.90/7.11 (Eq % 6.90/7.11 (And (relation a_2) (function a_2) → % 6.90/7.11 relation_isomorphism a a_1 a_2 → % 6.90/7.11 And % 6.90/7.11 (And % 6.90/7.11 (And (And (reflexive a → reflexive a_1) (transitive a → transitive a_1)) (connected a → connected a_1)) % 6.90/7.11 (antisymmetric a → antisymmetric a_1)) % 6.90/7.11 (well_founded_relation a → well_founded_relation a_1)) % 6.90/7.11 True)) % 6.90/7.11 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 : Iota), % 6.90/7.11 Or (Eq (relation a) False) % 6.90/7.11 (Or (Eq (relation a_1) False) % 6.90/7.11 (Or (Eq (And (relation a_2) (function a_2)) False) % 6.90/7.11 (Eq % 6.90/7.11 (relation_isomorphism a a_1 a_2 → % 6.90/7.11 And % 6.90/7.11 (And % 6.90/7.11 (And (And (reflexive a → reflexive a_1) (transitive a → transitive a_1)) (connected a → connected a_1)) % 6.90/7.11 (antisymmetric a → antisymmetric a_1)) % 6.90/7.11 (well_founded_relation a → well_founded_relation a_1)) % 6.90/7.11 True))) % 6.90/7.11 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 : Iota), % 6.90/7.11 Or (Eq (relation a) False) % 6.90/7.11 (Or (Eq (relation a_1) False) % 6.90/7.11 (Or % 6.90/7.11 (Eq % 6.90/7.11 (relation_isomorphism a a_1 a_2 → % 6.90/7.11 And % 6.90/7.11 (And % 6.90/7.11 (And (And (reflexive a → reflexive a_1) (transitive a → transitive a_1)) (connected a → connected a_1)) % 6.90/7.11 (antisymmetric a → antisymmetric a_1)) % 6.90/7.11 (well_founded_relation a → well_founded_relation a_1)) % 6.90/7.11 True) % 6.90/7.11 (Or (Eq (relation a_2) False) (Eq (function a_2) False)))) % 6.90/7.11 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 : Iota), % 6.90/7.11 Or (Eq (relation a) False) % 6.90/7.11 (Or (Eq (relation a_1) False) % 6.90/7.11 (Or (Eq (relation a_2) False) % 6.90/7.11 (Or (Eq (function a_2) False) % 6.90/7.11 (Or (Eq (relation_isomorphism a a_1 a_2) False) % 6.96/7.13 (Eq % 6.96/7.13 (And % 6.96/7.13 (And % 6.96/7.13 (And (And (reflexive a → reflexive a_1) (transitive a → transitive a_1)) % 6.96/7.13 (connected a → connected a_1)) % 6.96/7.13 (antisymmetric a → antisymmetric a_1)) % 6.96/7.13 (well_founded_relation a → well_founded_relation a_1)) % 6.96/7.13 True))))) % 6.96/7.13 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), % 6.96/7.13 Or (Eq (relation a) False) % 6.96/7.13 (Or (Eq (relation a_1) False) % 6.96/7.13 (Or (Eq (relation a_2) False) % 6.96/7.13 (Or (Eq (function a_2) False) % 6.96/7.13 (Or (Eq (relation_isomorphism a a_1 a_2) False) % 6.96/7.13 (Eq (well_founded_relation a → well_founded_relation a_1) True))))) % 6.96/7.13 Clause #53 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), % 6.96/7.13 Or (Eq (relation a) False) % 6.96/7.13 (Or (Eq (relation a_1) False) % 6.96/7.13 (Or (Eq (relation a_2) False) % 6.96/7.13 (Or (Eq (function a_2) False) % 6.96/7.13 (Or (Eq (relation_isomorphism a a_1 a_2) False) % 6.96/7.13 (Eq % 6.96/7.13 (And % 6.96/7.13 (And (And (reflexive a → reflexive a_1) (transitive a → transitive a_1)) (connected a → connected a_1)) % 6.96/7.13 (antisymmetric a → antisymmetric a_1)) % 6.96/7.13 True))))) % 6.96/7.13 Clause #54 (by clausification #[52]): ∀ (a a_1 a_2 : Iota), % 6.96/7.13 Or (Eq (relation a) False) % 6.96/7.13 (Or (Eq (relation a_1) False) % 6.96/7.13 (Or (Eq (relation a_2) False) % 6.96/7.13 (Or (Eq (function a_2) False) % 6.96/7.13 (Or (Eq (relation_isomorphism a a_1 a_2) False) % 6.96/7.13 (Or (Eq (well_founded_relation a) False) (Eq (well_founded_relation a_1) True)))))) % 6.96/7.13 Clause #56 (by superposition #[54, 10]): ∀ (a a_1 a_2 : Iota), % 6.96/7.13 Or (Eq (relation a) False) % 6.96/7.13 (Or (Eq (relation a_1) False) % 6.96/7.13 (Or (Eq (function a_1) False) % 6.96/7.13 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.96/7.13 (Or (Eq (well_founded_relation (skS.0 1 a_2)) False) % 6.96/7.13 (Or (Eq (well_founded_relation a) True) (Eq False True)))))) % 6.96/7.13 Clause #59 (by clausification #[41]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 1 a)) False) (Eq (well_founded_relation (skS.0 1 a)) True) % 6.96/7.13 Clause #60 (by forward demodulation #[59, 36]): ∀ (a : Iota), Or (Eq True False) (Eq (well_founded_relation (skS.0 1 a)) True) % 6.96/7.13 Clause #61 (by clausification #[60]): ∀ (a : Iota), Eq (well_founded_relation (skS.0 1 a)) True % 6.96/7.13 Clause #63 (by clausification #[39]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (connected a) True)) % 6.96/7.13 Clause #64 (by clausification #[39]): ∀ (a : Iota), % 6.96/7.13 Or (Eq (relation a) False) % 6.96/7.13 (Or (Eq (well_ordering a) False) (Eq (And (And (reflexive a) (transitive a)) (antisymmetric a)) True)) % 6.96/7.13 Clause #66 (by superposition #[63, 10]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 1 a)) False) (Or (Eq (connected (skS.0 1 a)) True) (Eq False True)) % 6.96/7.13 Clause #69 (by clausification #[64]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (antisymmetric a) True)) % 6.96/7.13 Clause #70 (by clausification #[64]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (And (reflexive a) (transitive a)) True)) % 6.96/7.13 Clause #72 (by superposition #[69, 10]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 1 a)) False) (Or (Eq (antisymmetric (skS.0 1 a)) True) (Eq False True)) % 6.96/7.13 Clause #75 (by clausification #[70]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (transitive a) True)) % 6.96/7.13 Clause #76 (by clausification #[70]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (reflexive a) True)) % 6.96/7.13 Clause #78 (by superposition #[75, 10]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 1 a)) False) (Or (Eq (transitive (skS.0 1 a)) True) (Eq False True)) % 6.96/7.13 Clause #83 (by superposition #[76, 10]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 1 a)) False) (Or (Eq (reflexive (skS.0 1 a)) True) (Eq False True)) % 6.96/7.13 Clause #87 (by clausification #[66]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 1 a)) False) (Eq (connected (skS.0 1 a)) True) % 6.96/7.13 Clause #88 (by forward demodulation #[87, 36]): ∀ (a : Iota), Or (Eq True False) (Eq (connected (skS.0 1 a)) True) % 6.96/7.13 Clause #89 (by clausification #[88]): ∀ (a : Iota), Eq (connected (skS.0 1 a)) True % 6.99/7.15 Clause #90 (by clausification #[72]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 1 a)) False) (Eq (antisymmetric (skS.0 1 a)) True) % 6.99/7.15 Clause #91 (by forward demodulation #[90, 36]): ∀ (a : Iota), Or (Eq True False) (Eq (antisymmetric (skS.0 1 a)) True) % 6.99/7.15 Clause #92 (by clausification #[91]): ∀ (a : Iota), Eq (antisymmetric (skS.0 1 a)) True % 6.99/7.15 Clause #96 (by clausification #[83]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 1 a)) False) (Eq (reflexive (skS.0 1 a)) True) % 6.99/7.15 Clause #97 (by forward demodulation #[96, 36]): ∀ (a : Iota), Or (Eq True False) (Eq (reflexive (skS.0 1 a)) True) % 6.99/7.15 Clause #98 (by clausification #[97]): ∀ (a : Iota), Eq (reflexive (skS.0 1 a)) True % 6.99/7.15 Clause #99 (by clausification #[78]): ∀ (a : Iota), Or (Eq (well_ordering (skS.0 1 a)) False) (Eq (transitive (skS.0 1 a)) True) % 6.99/7.15 Clause #100 (by forward demodulation #[99, 36]): ∀ (a : Iota), Or (Eq True False) (Eq (transitive (skS.0 1 a)) True) % 6.99/7.15 Clause #101 (by clausification #[100]): ∀ (a : Iota), Eq (transitive (skS.0 1 a)) True % 6.99/7.15 Clause #106 (by clausification #[32]): ∀ (a a_1 : Iota), % 6.99/7.15 Or (Eq (well_ordering (skS.0 2 a a_1)) True) % 6.99/7.15 (Or (Eq (well_founded_relation (skS.0 2 a a_1)) False) % 6.99/7.15 (Or (Eq (connected (skS.0 2 a a_1)) False) % 6.99/7.15 (Or (Eq (antisymmetric (skS.0 2 a a_1)) False) % 6.99/7.15 (Or (Eq (reflexive (skS.0 2 a a_1)) False) (Eq (transitive (skS.0 2 a a_1)) False))))) % 6.99/7.15 Clause #107 (by forward demodulation #[106, 34]): ∀ (a a_1 : Iota), % 6.99/7.15 Or (Eq False True) % 6.99/7.15 (Or (Eq (well_founded_relation (skS.0 2 a a_1)) False) % 6.99/7.15 (Or (Eq (connected (skS.0 2 a a_1)) False) % 6.99/7.15 (Or (Eq (antisymmetric (skS.0 2 a a_1)) False) % 6.99/7.15 (Or (Eq (reflexive (skS.0 2 a a_1)) False) (Eq (transitive (skS.0 2 a a_1)) False))))) % 6.99/7.15 Clause #108 (by clausification #[107]): ∀ (a a_1 : Iota), % 6.99/7.15 Or (Eq (well_founded_relation (skS.0 2 a a_1)) False) % 6.99/7.15 (Or (Eq (connected (skS.0 2 a a_1)) False) % 6.99/7.15 (Or (Eq (antisymmetric (skS.0 2 a a_1)) False) % 6.99/7.15 (Or (Eq (reflexive (skS.0 2 a a_1)) False) (Eq (transitive (skS.0 2 a a_1)) False)))) % 6.99/7.15 Clause #123 (by clausification #[56]): ∀ (a a_1 a_2 : Iota), % 6.99/7.15 Or (Eq (relation a) False) % 6.99/7.15 (Or (Eq (relation a_1) False) % 6.99/7.15 (Or (Eq (function a_1) False) % 6.99/7.15 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.99/7.15 (Or (Eq (well_founded_relation (skS.0 1 a_2)) False) (Eq (well_founded_relation a) True))))) % 6.99/7.15 Clause #124 (by forward demodulation #[123, 61]): ∀ (a a_1 a_2 : Iota), % 6.99/7.15 Or (Eq (relation a) False) % 6.99/7.15 (Or (Eq (relation a_1) False) % 6.99/7.15 (Or (Eq (function a_1) False) % 6.99/7.15 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.99/7.15 (Or (Eq True False) (Eq (well_founded_relation a) True))))) % 6.99/7.15 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), % 6.99/7.15 Or (Eq (relation a) False) % 6.99/7.15 (Or (Eq (relation a_1) False) % 6.99/7.15 (Or (Eq (function a_1) False) % 6.99/7.15 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) (Eq (well_founded_relation a) True)))) % 6.99/7.15 Clause #128 (by superposition #[125, 14]): ∀ (a a_1 a_2 a_3 : Iota), % 6.99/7.15 Or (Eq (relation a) False) % 6.99/7.15 (Or (Eq (function a) False) % 6.99/7.15 (Or (Eq (relation_isomorphism (skS.0 1 a_1) (skS.0 2 a_2 a_3) a) False) % 6.99/7.15 (Or (Eq (well_founded_relation (skS.0 2 a_2 a_3)) True) (Eq False True)))) % 6.99/7.15 Clause #130 (by clausification #[53]): ∀ (a a_1 a_2 : Iota), % 6.99/7.15 Or (Eq (relation a) False) % 6.99/7.15 (Or (Eq (relation a_1) False) % 6.99/7.15 (Or (Eq (relation a_2) False) % 6.99/7.15 (Or (Eq (function a_2) False) % 6.99/7.15 (Or (Eq (relation_isomorphism a a_1 a_2) False) (Eq (antisymmetric a → antisymmetric a_1) True))))) % 6.99/7.15 Clause #131 (by clausification #[53]): ∀ (a a_1 a_2 : Iota), % 6.99/7.15 Or (Eq (relation a) False) % 6.99/7.15 (Or (Eq (relation a_1) False) % 6.99/7.15 (Or (Eq (relation a_2) False) % 6.99/7.15 (Or (Eq (function a_2) False) % 6.99/7.15 (Or (Eq (relation_isomorphism a a_1 a_2) False) % 6.99/7.15 (Eq (And (And (reflexive a → reflexive a_1) (transitive a → transitive a_1)) (connected a → connected a_1)) % 6.99/7.15 True))))) % 6.99/7.15 Clause #132 (by clausification #[130]): ∀ (a a_1 a_2 : Iota), % 6.99/7.15 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (relation a_2) False) % 6.99/7.18 (Or (Eq (function a_2) False) % 6.99/7.18 (Or (Eq (relation_isomorphism a a_1 a_2) False) % 6.99/7.18 (Or (Eq (antisymmetric a) False) (Eq (antisymmetric a_1) True)))))) % 6.99/7.18 Clause #134 (by superposition #[132, 10]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (function a_1) False) % 6.99/7.18 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.99/7.18 (Or (Eq (antisymmetric (skS.0 1 a_2)) False) (Or (Eq (antisymmetric a) True) (Eq False True)))))) % 6.99/7.18 Clause #137 (by clausification #[131]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (relation a_2) False) % 6.99/7.18 (Or (Eq (function a_2) False) % 6.99/7.18 (Or (Eq (relation_isomorphism a a_1 a_2) False) (Eq (connected a → connected a_1) True))))) % 6.99/7.18 Clause #138 (by clausification #[131]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (relation a_2) False) % 6.99/7.18 (Or (Eq (function a_2) False) % 6.99/7.18 (Or (Eq (relation_isomorphism a a_1 a_2) False) % 6.99/7.18 (Eq (And (reflexive a → reflexive a_1) (transitive a → transitive a_1)) True))))) % 6.99/7.18 Clause #139 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (relation a_2) False) % 6.99/7.18 (Or (Eq (function a_2) False) % 6.99/7.18 (Or (Eq (relation_isomorphism a a_1 a_2) False) (Or (Eq (connected a) False) (Eq (connected a_1) True)))))) % 6.99/7.18 Clause #141 (by superposition #[139, 10]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (function a_1) False) % 6.99/7.18 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.99/7.18 (Or (Eq (connected (skS.0 1 a_2)) False) (Or (Eq (connected a) True) (Eq False True)))))) % 6.99/7.18 Clause #144 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (relation a_2) False) % 6.99/7.18 (Or (Eq (function a_2) False) % 6.99/7.18 (Or (Eq (relation_isomorphism a a_1 a_2) False) (Eq (transitive a → transitive a_1) True))))) % 6.99/7.18 Clause #145 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (relation a_2) False) % 6.99/7.18 (Or (Eq (function a_2) False) % 6.99/7.18 (Or (Eq (relation_isomorphism a a_1 a_2) False) (Eq (reflexive a → reflexive a_1) True))))) % 6.99/7.18 Clause #146 (by clausification #[144]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (relation a_2) False) % 6.99/7.18 (Or (Eq (function a_2) False) % 6.99/7.18 (Or (Eq (relation_isomorphism a a_1 a_2) False) (Or (Eq (transitive a) False) (Eq (transitive a_1) True)))))) % 6.99/7.18 Clause #148 (by superposition #[146, 10]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (function a_1) False) % 6.99/7.18 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.99/7.18 (Or (Eq (transitive (skS.0 1 a_2)) False) (Or (Eq (transitive a) True) (Eq False True)))))) % 6.99/7.18 Clause #151 (by clausification #[145]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (relation a_2) False) % 6.99/7.18 (Or (Eq (function a_2) False) % 6.99/7.18 (Or (Eq (relation_isomorphism a a_1 a_2) False) (Or (Eq (reflexive a) False) (Eq (reflexive a_1) True)))))) % 6.99/7.18 Clause #153 (by superposition #[151, 10]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (function a_1) False) % 6.99/7.18 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.99/7.18 (Or (Eq (reflexive (skS.0 1 a_2)) False) (Or (Eq (reflexive a) True) (Eq False True)))))) % 6.99/7.18 Clause #168 (by clausification #[141]): ∀ (a a_1 a_2 : Iota), % 6.99/7.18 Or (Eq (relation a) False) % 6.99/7.18 (Or (Eq (relation a_1) False) % 6.99/7.18 (Or (Eq (function a_1) False) % 6.99/7.18 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.99/7.18 (Or (Eq (connected (skS.0 1 a_2)) False) (Eq (connected a) True))))) % 6.99/7.20 Clause #169 (by forward demodulation #[168, 89]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) (Or (Eq True False) (Eq (connected a) True))))) % 6.99/7.20 Clause #170 (by clausification #[169]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) (Eq (connected a) True)))) % 6.99/7.20 Clause #173 (by superposition #[170, 14]): ∀ (a a_1 a_2 a_3 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (function a) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_1) (skS.0 2 a_2 a_3) a) False) % 6.99/7.20 (Or (Eq (connected (skS.0 2 a_2 a_3)) True) (Eq False True)))) % 6.99/7.20 Clause #181 (by clausification #[153]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.99/7.20 (Or (Eq (reflexive (skS.0 1 a_2)) False) (Eq (reflexive a) True))))) % 6.99/7.20 Clause #182 (by forward demodulation #[181, 98]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) (Or (Eq True False) (Eq (reflexive a) True))))) % 6.99/7.20 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) (Eq (reflexive a) True)))) % 6.99/7.20 Clause #186 (by superposition #[183, 14]): ∀ (a a_1 a_2 a_3 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (function a) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_1) (skS.0 2 a_2 a_3) a) False) % 6.99/7.20 (Or (Eq (reflexive (skS.0 2 a_2 a_3)) True) (Eq False True)))) % 6.99/7.20 Clause #204 (by clausification #[148]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.99/7.20 (Or (Eq (transitive (skS.0 1 a_2)) False) (Eq (transitive a) True))))) % 6.99/7.20 Clause #205 (by forward demodulation #[204, 101]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) (Or (Eq True False) (Eq (transitive a) True))))) % 6.99/7.20 Clause #206 (by clausification #[205]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) (Eq (transitive a) True)))) % 6.99/7.20 Clause #209 (by superposition #[206, 14]): ∀ (a a_1 a_2 a_3 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (function a) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_1) (skS.0 2 a_2 a_3) a) False) % 6.99/7.20 (Or (Eq (transitive (skS.0 2 a_2 a_3)) True) (Eq False True)))) % 6.99/7.20 Clause #227 (by clausification #[134]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) % 6.99/7.20 (Or (Eq (antisymmetric (skS.0 1 a_2)) False) (Eq (antisymmetric a) True))))) % 6.99/7.20 Clause #228 (by forward demodulation #[227, 92]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) (Or (Eq True False) (Eq (antisymmetric a) True))))) % 6.99/7.20 Clause #229 (by clausification #[228]): ∀ (a a_1 a_2 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.20 (Or (Eq (relation a_1) False) % 6.99/7.20 (Or (Eq (function a_1) False) % 6.99/7.20 (Or (Eq (relation_isomorphism (skS.0 1 a_2) a a_1) False) (Eq (antisymmetric a) True)))) % 6.99/7.20 Clause #232 (by superposition #[229, 14]): ∀ (a a_1 a_2 a_3 : Iota), % 6.99/7.20 Or (Eq (relation a) False) % 6.99/7.22 (Or (Eq (function a) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_1) (skS.0 2 a_2 a_3) a) False) % 6.99/7.22 (Or (Eq (antisymmetric (skS.0 2 a_2 a_3)) True) (Eq False True)))) % 6.99/7.22 Clause #245 (by clausification #[128]): ∀ (a a_1 a_2 a_3 : Iota), % 6.99/7.22 Or (Eq (relation a) False) % 6.99/7.22 (Or (Eq (function a) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_1) (skS.0 2 a_2 a_3) a) False) % 6.99/7.22 (Eq (well_founded_relation (skS.0 2 a_2 a_3)) True))) % 6.99/7.22 Clause #249 (by superposition #[245, 21]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.99/7.22 Or (Eq (function (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_3) (skS.0 2 a_4 a_5) (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (well_founded_relation (skS.0 2 a_4 a_5)) True) (Eq False True))) % 6.99/7.22 Clause #255 (by clausification #[173]): ∀ (a a_1 a_2 a_3 : Iota), % 6.99/7.22 Or (Eq (relation a) False) % 6.99/7.22 (Or (Eq (function a) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_1) (skS.0 2 a_2 a_3) a) False) (Eq (connected (skS.0 2 a_2 a_3)) True))) % 6.99/7.22 Clause #259 (by superposition #[255, 21]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.99/7.22 Or (Eq (function (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_3) (skS.0 2 a_4 a_5) (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (connected (skS.0 2 a_4 a_5)) True) (Eq False True))) % 6.99/7.22 Clause #260 (by clausification #[186]): ∀ (a a_1 a_2 a_3 : Iota), % 6.99/7.22 Or (Eq (relation a) False) % 6.99/7.22 (Or (Eq (function a) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_1) (skS.0 2 a_2 a_3) a) False) (Eq (reflexive (skS.0 2 a_2 a_3)) True))) % 6.99/7.22 Clause #264 (by superposition #[260, 21]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.99/7.22 Or (Eq (function (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_3) (skS.0 2 a_4 a_5) (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (reflexive (skS.0 2 a_4 a_5)) True) (Eq False True))) % 6.99/7.22 Clause #265 (by clausification #[232]): ∀ (a a_1 a_2 a_3 : Iota), % 6.99/7.22 Or (Eq (relation a) False) % 6.99/7.22 (Or (Eq (function a) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_1) (skS.0 2 a_2 a_3) a) False) % 6.99/7.22 (Eq (antisymmetric (skS.0 2 a_2 a_3)) True))) % 6.99/7.22 Clause #269 (by superposition #[265, 21]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.99/7.22 Or (Eq (function (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_3) (skS.0 2 a_4 a_5) (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (antisymmetric (skS.0 2 a_4 a_5)) True) (Eq False True))) % 6.99/7.22 Clause #270 (by clausification #[209]): ∀ (a a_1 a_2 a_3 : Iota), % 6.99/7.22 Or (Eq (relation a) False) % 6.99/7.22 (Or (Eq (function a) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_1) (skS.0 2 a_2 a_3) a) False) (Eq (transitive (skS.0 2 a_2 a_3)) True))) % 6.99/7.22 Clause #274 (by superposition #[270, 21]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.99/7.22 Or (Eq (function (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_3) (skS.0 2 a_4 a_5) (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (transitive (skS.0 2 a_4 a_5)) True) (Eq False True))) % 6.99/7.22 Clause #609 (by clausification #[249]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.99/7.22 Or (Eq (function (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a_3) (skS.0 2 a_4 a_5) (skS.0 3 a a_1 a_2)) False) % 6.99/7.22 (Eq (well_founded_relation (skS.0 2 a_4 a_5)) True)) % 6.99/7.22 Clause #610 (by forward demodulation #[609, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.99/7.22 Or (Eq True False) % 6.99/7.22 (Or (Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a_1 a_2) (skS.0 3 a_3 a_4 a_5)) False) % 6.99/7.22 (Eq (well_founded_relation (skS.0 2 a_1 a_2)) True)) % 6.99/7.22 Clause #611 (by clausification #[610]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.99/7.22 Or (Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a_1 a_2) (skS.0 3 a_3 a_4 a_5)) False) % 6.99/7.22 (Eq (well_founded_relation (skS.0 2 a_1 a_2)) True) % 6.99/7.22 Clause #612 (by superposition #[611, 35]): ∀ (a a_1 : Iota), Or (Eq (well_founded_relation (skS.0 2 a a_1)) True) (Eq False True) % 6.99/7.22 Clause #613 (by clausification #[612]): ∀ (a a_1 : Iota), Eq (well_founded_relation (skS.0 2 a a_1)) True % 6.99/7.22 Clause #614 (by backward demodulation #[613, 108]): ∀ (a a_1 : Iota), % 6.99/7.22 Or (Eq True False) % 6.99/7.22 (Or (Eq (connected (skS.0 2 a a_1)) False) % 6.99/7.22 (Or (Eq (antisymmetric (skS.0 2 a a_1)) False) % 7.07/7.24 (Or (Eq (reflexive (skS.0 2 a a_1)) False) (Eq (transitive (skS.0 2 a a_1)) False)))) % 7.07/7.24 Clause #643 (by clausification #[259]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq (function (skS.0 3 a a_1 a_2)) False) % 7.07/7.24 (Or (Eq (relation_isomorphism (skS.0 1 a_3) (skS.0 2 a_4 a_5) (skS.0 3 a a_1 a_2)) False) % 7.07/7.24 (Eq (connected (skS.0 2 a_4 a_5)) True)) % 7.07/7.24 Clause #644 (by forward demodulation #[643, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq True False) % 7.07/7.24 (Or (Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a_1 a_2) (skS.0 3 a_3 a_4 a_5)) False) % 7.07/7.24 (Eq (connected (skS.0 2 a_1 a_2)) True)) % 7.07/7.24 Clause #645 (by clausification #[644]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a_1 a_2) (skS.0 3 a_3 a_4 a_5)) False) % 7.07/7.24 (Eq (connected (skS.0 2 a_1 a_2)) True) % 7.07/7.24 Clause #646 (by superposition #[645, 35]): ∀ (a a_1 : Iota), Or (Eq (connected (skS.0 2 a a_1)) True) (Eq False True) % 7.07/7.24 Clause #647 (by clausification #[646]): ∀ (a a_1 : Iota), Eq (connected (skS.0 2 a a_1)) True % 7.07/7.24 Clause #662 (by clausification #[264]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq (function (skS.0 3 a a_1 a_2)) False) % 7.07/7.24 (Or (Eq (relation_isomorphism (skS.0 1 a_3) (skS.0 2 a_4 a_5) (skS.0 3 a a_1 a_2)) False) % 7.07/7.24 (Eq (reflexive (skS.0 2 a_4 a_5)) True)) % 7.07/7.24 Clause #663 (by forward demodulation #[662, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq True False) % 7.07/7.24 (Or (Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a_1 a_2) (skS.0 3 a_3 a_4 a_5)) False) % 7.07/7.24 (Eq (reflexive (skS.0 2 a_1 a_2)) True)) % 7.07/7.24 Clause #664 (by clausification #[663]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a_1 a_2) (skS.0 3 a_3 a_4 a_5)) False) % 7.07/7.24 (Eq (reflexive (skS.0 2 a_1 a_2)) True) % 7.07/7.24 Clause #665 (by superposition #[664, 35]): ∀ (a a_1 : Iota), Or (Eq (reflexive (skS.0 2 a a_1)) True) (Eq False True) % 7.07/7.24 Clause #666 (by clausification #[665]): ∀ (a a_1 : Iota), Eq (reflexive (skS.0 2 a a_1)) True % 7.07/7.24 Clause #681 (by clausification #[269]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq (function (skS.0 3 a a_1 a_2)) False) % 7.07/7.24 (Or (Eq (relation_isomorphism (skS.0 1 a_3) (skS.0 2 a_4 a_5) (skS.0 3 a a_1 a_2)) False) % 7.07/7.24 (Eq (antisymmetric (skS.0 2 a_4 a_5)) True)) % 7.07/7.24 Clause #682 (by forward demodulation #[681, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq True False) % 7.07/7.24 (Or (Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a_1 a_2) (skS.0 3 a_3 a_4 a_5)) False) % 7.07/7.24 (Eq (antisymmetric (skS.0 2 a_1 a_2)) True)) % 7.07/7.24 Clause #683 (by clausification #[682]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a_1 a_2) (skS.0 3 a_3 a_4 a_5)) False) % 7.07/7.24 (Eq (antisymmetric (skS.0 2 a_1 a_2)) True) % 7.07/7.24 Clause #684 (by superposition #[683, 35]): ∀ (a a_1 : Iota), Or (Eq (antisymmetric (skS.0 2 a a_1)) True) (Eq False True) % 7.07/7.24 Clause #685 (by clausification #[684]): ∀ (a a_1 : Iota), Eq (antisymmetric (skS.0 2 a a_1)) True % 7.07/7.24 Clause #700 (by clausification #[274]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq (function (skS.0 3 a a_1 a_2)) False) % 7.07/7.24 (Or (Eq (relation_isomorphism (skS.0 1 a_3) (skS.0 2 a_4 a_5) (skS.0 3 a a_1 a_2)) False) % 7.07/7.24 (Eq (transitive (skS.0 2 a_4 a_5)) True)) % 7.07/7.24 Clause #701 (by forward demodulation #[700, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq True False) % 7.07/7.24 (Or (Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a_1 a_2) (skS.0 3 a_3 a_4 a_5)) False) % 7.07/7.24 (Eq (transitive (skS.0 2 a_1 a_2)) True)) % 7.07/7.24 Clause #702 (by clausification #[701]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.07/7.24 Or (Eq (relation_isomorphism (skS.0 1 a) (skS.0 2 a_1 a_2) (skS.0 3 a_3 a_4 a_5)) False) % 7.07/7.24 (Eq (transitive (skS.0 2 a_1 a_2)) True) % 7.07/7.24 Clause #703 (by superposition #[702, 35]): ∀ (a a_1 : Iota), Or (Eq (transitive (skS.0 2 a a_1)) True) (Eq False True) % 7.07/7.24 Clause #704 (by clausification #[703]): ∀ (a a_1 : Iota), Eq (transitive (skS.0 2 a a_1)) True % 7.07/7.24 Clause #786 (by clausification #[614]): ∀ (a a_1 : Iota), % 7.07/7.24 Or (Eq (connected (skS.0 2 a a_1)) False) % 7.07/7.24 (Or (Eq (antisymmetric (skS.0 2 a a_1)) False) % 7.07/7.24 (Or (Eq (reflexive (skS.0 2 a a_1)) False) (Eq (transitive (skS.0 2 a a_1)) False))) % 7.07/7.26 Clause #787 (by forward demodulation #[786, 685]): ∀ (a a_1 : Iota), % 7.07/7.26 Or (Eq (connected (skS.0 2 a a_1)) False) % 7.07/7.26 (Or (Eq True False) (Or (Eq (reflexive (skS.0 2 a a_1)) False) (Eq (transitive (skS.0 2 a a_1)) False))) % 7.07/7.26 Clause #788 (by clausification #[787]): ∀ (a a_1 : Iota), % 7.07/7.26 Or (Eq (connected (skS.0 2 a a_1)) False) % 7.07/7.26 (Or (Eq (reflexive (skS.0 2 a a_1)) False) (Eq (transitive (skS.0 2 a a_1)) False)) % 7.07/7.26 Clause #789 (by forward demodulation #[788, 666]): ∀ (a a_1 : Iota), Or (Eq (connected (skS.0 2 a a_1)) False) (Or (Eq True False) (Eq (transitive (skS.0 2 a a_1)) False)) % 7.07/7.26 Clause #790 (by clausification #[789]): ∀ (a a_1 : Iota), Or (Eq (connected (skS.0 2 a a_1)) False) (Eq (transitive (skS.0 2 a a_1)) False) % 7.07/7.26 Clause #791 (by forward demodulation #[790, 704]): ∀ (a a_1 : Iota), Or (Eq (connected (skS.0 2 a a_1)) False) (Eq True False) % 7.07/7.26 Clause #792 (by clausification #[791]): ∀ (a a_1 : Iota), Eq (connected (skS.0 2 a a_1)) False % 7.07/7.26 Clause #793 (by superposition #[792, 647]): Eq False True % 7.07/7.26 Clause #794 (by clausification #[793]): False % 7.07/7.26 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------