%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU257+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.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:14 PM UTC 2025 % Result : Theorem 4.74s 4.90s % Output : Proof 4.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU257+1 : TPTP v9.2.0. Released v3.3.0. % 0.07/0.14 % Command : duper %s % 0.13/0.35 % Computer : n010.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 06:44:53 EDT 2025 % 0.13/0.35 % CPUTime : % 4.74/4.90 SZS status Theorem for theBenchmark.p % 4.74/4.90 SZS output start Proof for theBenchmark.p % 4.74/4.90 Clause #1 (by assumption #[]): Eq % 4.74/4.90 (∀ (A : Iota), % 4.74/4.90 relation A → % 4.74/4.90 Iff (well_ordering A) % 4.74/4.90 (And (And (And (And (reflexive A) (transitive A)) (antisymmetric A)) (connected A)) (well_founded_relation A))) % 4.74/4.90 True % 4.74/4.90 Clause #3 (by assumption #[]): Eq (∀ (A B : Iota), relation A → relation (relation_restriction A B)) True % 4.74/4.90 Clause #6 (by assumption #[]): Eq (∀ (A B : Iota), relation B → reflexive B → reflexive (relation_restriction B A)) True % 4.74/4.90 Clause #7 (by assumption #[]): Eq (∀ (A B : Iota), relation B → connected B → connected (relation_restriction B A)) True % 4.74/4.90 Clause #8 (by assumption #[]): Eq (∀ (A B : Iota), relation B → transitive B → transitive (relation_restriction B A)) True % 4.74/4.90 Clause #9 (by assumption #[]): Eq (∀ (A B : Iota), relation B → antisymmetric B → antisymmetric (relation_restriction B A)) True % 4.74/4.90 Clause #10 (by assumption #[]): Eq (∀ (A B : Iota), relation B → well_founded_relation B → well_founded_relation (relation_restriction B A)) True % 4.74/4.90 Clause #11 (by assumption #[]): Eq (Not (∀ (A B : Iota), relation B → well_ordering B → well_ordering (relation_restriction B A))) True % 4.74/4.90 Clause #12 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B : Iota), relation a → relation (relation_restriction a B)) True % 4.74/4.90 Clause #13 (by clausification #[12]): ∀ (a a_1 : Iota), Eq (relation a → relation (relation_restriction a a_1)) True % 4.74/4.90 Clause #14 (by clausification #[13]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Eq (relation (relation_restriction a a_1)) True) % 4.74/4.90 Clause #18 (by clausification #[10]): ∀ (a : Iota), % 4.74/4.90 Eq (∀ (B : Iota), relation B → well_founded_relation B → well_founded_relation (relation_restriction B a)) True % 4.74/4.90 Clause #19 (by clausification #[18]): ∀ (a a_1 : Iota), Eq (relation a → well_founded_relation a → well_founded_relation (relation_restriction a a_1)) True % 4.74/4.90 Clause #20 (by clausification #[19]): ∀ (a a_1 : Iota), % 4.74/4.90 Or (Eq (relation a) False) (Eq (well_founded_relation a → well_founded_relation (relation_restriction a a_1)) True) % 4.74/4.90 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), % 4.74/4.90 Or (Eq (relation a) False) % 4.74/4.90 (Or (Eq (well_founded_relation a) False) (Eq (well_founded_relation (relation_restriction a a_1)) True)) % 4.74/4.90 Clause #22 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B : Iota), relation B → connected B → connected (relation_restriction B a)) True % 4.74/4.90 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), Eq (relation a → connected a → connected (relation_restriction a a_1)) True % 4.74/4.90 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Eq (connected a → connected (relation_restriction a a_1)) True) % 4.74/4.90 Clause #25 (by clausification #[24]): ∀ (a a_1 : Iota), % 4.74/4.90 Or (Eq (relation a) False) (Or (Eq (connected a) False) (Eq (connected (relation_restriction a a_1)) True)) % 4.74/4.90 Clause #29 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B : Iota), relation B → reflexive B → reflexive (relation_restriction B a)) True % 4.74/4.90 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), Eq (relation a → reflexive a → reflexive (relation_restriction a a_1)) True % 4.74/4.90 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Eq (reflexive a → reflexive (relation_restriction a a_1)) True) % 4.74/4.90 Clause #32 (by clausification #[31]): ∀ (a a_1 : Iota), % 4.74/4.90 Or (Eq (relation a) False) (Or (Eq (reflexive a) False) (Eq (reflexive (relation_restriction a a_1)) True)) % 4.74/4.90 Clause #33 (by clausification #[9]): ∀ (a : Iota), Eq (∀ (B : Iota), relation B → antisymmetric B → antisymmetric (relation_restriction B a)) True % 4.74/4.90 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), Eq (relation a → antisymmetric a → antisymmetric (relation_restriction a a_1)) True % 4.74/4.90 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Eq (antisymmetric a → antisymmetric (relation_restriction a a_1)) True) % 4.74/4.90 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), % 4.74/4.90 Or (Eq (relation a) False) (Or (Eq (antisymmetric a) False) (Eq (antisymmetric (relation_restriction a a_1)) True)) % 4.74/4.92 Clause #37 (by clausification #[8]): ∀ (a : Iota), Eq (∀ (B : Iota), relation B → transitive B → transitive (relation_restriction B a)) True % 4.74/4.92 Clause #38 (by clausification #[37]): ∀ (a a_1 : Iota), Eq (relation a → transitive a → transitive (relation_restriction a a_1)) True % 4.74/4.92 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Eq (transitive a → transitive (relation_restriction a a_1)) True) % 4.74/4.92 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), % 4.74/4.92 Or (Eq (relation a) False) (Or (Eq (transitive a) False) (Eq (transitive (relation_restriction a a_1)) True)) % 4.74/4.92 Clause #41 (by clausification #[11]): Eq (∀ (A B : Iota), relation B → well_ordering B → well_ordering (relation_restriction B A)) False % 4.74/4.92 Clause #42 (by clausification #[41]): ∀ (a : Iota), % 4.74/4.92 Eq (Not (∀ (B : Iota), relation B → well_ordering B → well_ordering (relation_restriction B (skS.0 0 a)))) True % 4.74/4.92 Clause #43 (by clausification #[42]): ∀ (a : Iota), Eq (∀ (B : Iota), relation B → well_ordering B → well_ordering (relation_restriction B (skS.0 0 a))) False % 4.74/4.92 Clause #44 (by clausification #[43]): ∀ (a a_1 : Iota), % 4.74/4.92 Eq % 4.74/4.92 (Not % 4.74/4.92 (relation (skS.0 1 a a_1) → % 4.74/4.92 well_ordering (skS.0 1 a a_1) → well_ordering (relation_restriction (skS.0 1 a a_1) (skS.0 0 a)))) % 4.74/4.92 True % 4.74/4.92 Clause #45 (by clausification #[44]): ∀ (a a_1 : Iota), % 4.74/4.92 Eq % 4.74/4.92 (relation (skS.0 1 a a_1) → % 4.74/4.92 well_ordering (skS.0 1 a a_1) → well_ordering (relation_restriction (skS.0 1 a a_1) (skS.0 0 a))) % 4.74/4.92 False % 4.74/4.92 Clause #46 (by clausification #[45]): ∀ (a a_1 : Iota), Eq (relation (skS.0 1 a a_1)) True % 4.74/4.92 Clause #47 (by clausification #[45]): ∀ (a a_1 : Iota), % 4.74/4.92 Eq (well_ordering (skS.0 1 a a_1) → well_ordering (relation_restriction (skS.0 1 a a_1) (skS.0 0 a))) False % 4.74/4.92 Clause #48 (by superposition #[46, 14]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (relation (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.74/4.92 Clause #49 (by superposition #[46, 21]): ∀ (a a_1 a_2 : Iota), % 4.74/4.92 Or (Eq True False) % 4.74/4.92 (Or (Eq (well_founded_relation (skS.0 1 a a_1)) False) % 4.74/4.92 (Eq (well_founded_relation (relation_restriction (skS.0 1 a a_1) a_2)) True)) % 4.74/4.92 Clause #50 (by superposition #[46, 25]): ∀ (a a_1 a_2 : Iota), % 4.74/4.92 Or (Eq True False) % 4.74/4.92 (Or (Eq (connected (skS.0 1 a a_1)) False) (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) True)) % 4.74/4.92 Clause #51 (by superposition #[46, 32]): ∀ (a a_1 a_2 : Iota), % 4.74/4.92 Or (Eq True False) % 4.74/4.92 (Or (Eq (reflexive (skS.0 1 a a_1)) False) (Eq (reflexive (relation_restriction (skS.0 1 a a_1) a_2)) True)) % 4.74/4.92 Clause #52 (by superposition #[46, 36]): ∀ (a a_1 a_2 : Iota), % 4.74/4.92 Or (Eq True False) % 4.74/4.92 (Or (Eq (antisymmetric (skS.0 1 a a_1)) False) (Eq (antisymmetric (relation_restriction (skS.0 1 a a_1) a_2)) True)) % 4.74/4.92 Clause #53 (by superposition #[46, 40]): ∀ (a a_1 a_2 : Iota), % 4.74/4.92 Or (Eq True False) % 4.74/4.92 (Or (Eq (transitive (skS.0 1 a a_1)) False) (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) True)) % 4.74/4.92 Clause #54 (by clausification #[48]): ∀ (a a_1 a_2 : Iota), Eq (relation (relation_restriction (skS.0 1 a a_1) a_2)) True % 4.74/4.92 Clause #61 (by clausification #[1]): ∀ (a : Iota), % 4.74/4.92 Eq % 4.74/4.92 (relation a → % 4.74/4.92 Iff (well_ordering a) % 4.74/4.92 (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a))) % 4.74/4.92 True % 4.74/4.92 Clause #62 (by clausification #[61]): ∀ (a : Iota), % 4.74/4.92 Or (Eq (relation a) False) % 4.74/4.92 (Eq % 4.74/4.92 (Iff (well_ordering a) % 4.74/4.92 (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a))) % 4.74/4.92 True) % 4.74/4.92 Clause #63 (by clausification #[62]): ∀ (a : Iota), % 4.74/4.92 Or (Eq (relation a) False) % 4.74/4.92 (Or (Eq (well_ordering a) True) % 4.74/4.92 (Eq (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a)) % 4.74/4.92 False)) % 4.74/4.92 Clause #64 (by clausification #[62]): ∀ (a : Iota), % 4.74/4.92 Or (Eq (relation a) False) % 4.74/4.92 (Or (Eq (well_ordering a) False) % 4.74/4.92 (Eq (And (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) (well_founded_relation a)) % 4.74/4.95 True)) % 4.74/4.95 Clause #65 (by clausification #[63]): ∀ (a : Iota), % 4.74/4.95 Or (Eq (relation a) False) % 4.74/4.95 (Or (Eq (well_ordering a) True) % 4.74/4.95 (Or (Eq (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) False) % 4.74/4.95 (Eq (well_founded_relation a) False))) % 4.74/4.95 Clause #66 (by clausification #[65]): ∀ (a : Iota), % 4.74/4.95 Or (Eq (relation a) False) % 4.74/4.95 (Or (Eq (well_ordering a) True) % 4.74/4.95 (Or (Eq (well_founded_relation a) False) % 4.74/4.95 (Or (Eq (And (And (reflexive a) (transitive a)) (antisymmetric a)) False) (Eq (connected a) False)))) % 4.74/4.95 Clause #67 (by clausification #[66]): ∀ (a : Iota), % 4.74/4.95 Or (Eq (relation a) False) % 4.74/4.95 (Or (Eq (well_ordering a) True) % 4.74/4.95 (Or (Eq (well_founded_relation a) False) % 4.74/4.95 (Or (Eq (connected a) False) (Or (Eq (And (reflexive a) (transitive a)) False) (Eq (antisymmetric a) False))))) % 4.74/4.95 Clause #68 (by clausification #[67]): ∀ (a : Iota), % 4.74/4.95 Or (Eq (relation a) False) % 4.74/4.95 (Or (Eq (well_ordering a) True) % 4.74/4.95 (Or (Eq (well_founded_relation a) False) % 4.74/4.95 (Or (Eq (connected a) False) % 4.74/4.95 (Or (Eq (antisymmetric a) False) (Or (Eq (reflexive a) False) (Eq (transitive a) False)))))) % 4.74/4.95 Clause #70 (by superposition #[68, 54]): ∀ (a a_1 a_2 : Iota), % 4.74/4.95 Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.74/4.95 (Or (Eq (well_founded_relation (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.74/4.95 (Or (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.74/4.95 (Or (Eq (antisymmetric (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.74/4.95 (Or (Eq (reflexive (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.74/4.95 (Or (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) False) (Eq False True)))))) % 4.74/4.95 Clause #86 (by clausification #[47]): ∀ (a a_1 : Iota), Eq (well_ordering (skS.0 1 a a_1)) True % 4.74/4.95 Clause #87 (by clausification #[47]): ∀ (a a_1 : Iota), Eq (well_ordering (relation_restriction (skS.0 1 a a_1) (skS.0 0 a))) False % 4.74/4.95 Clause #97 (by clausification #[49]): ∀ (a a_1 a_2 : Iota), % 4.74/4.95 Or (Eq (well_founded_relation (skS.0 1 a a_1)) False) % 4.74/4.95 (Eq (well_founded_relation (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.74/4.95 Clause #107 (by clausification #[64]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (well_founded_relation a) True)) % 4.74/4.95 Clause #108 (by clausification #[64]): ∀ (a : Iota), % 4.74/4.95 Or (Eq (relation a) False) % 4.74/4.95 (Or (Eq (well_ordering a) False) % 4.74/4.95 (Eq (And (And (And (reflexive a) (transitive a)) (antisymmetric a)) (connected a)) True)) % 4.74/4.95 Clause #109 (by superposition #[107, 46]): ∀ (a a_1 : Iota), % 4.74/4.95 Or (Eq (well_ordering (skS.0 1 a a_1)) False) (Or (Eq (well_founded_relation (skS.0 1 a a_1)) True) (Eq False True)) % 4.74/4.95 Clause #114 (by clausification #[108]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (connected a) True)) % 4.74/4.95 Clause #115 (by clausification #[108]): ∀ (a : Iota), % 4.74/4.95 Or (Eq (relation a) False) % 4.74/4.95 (Or (Eq (well_ordering a) False) (Eq (And (And (reflexive a) (transitive a)) (antisymmetric a)) True)) % 4.74/4.95 Clause #116 (by superposition #[114, 46]): ∀ (a a_1 : Iota), % 4.74/4.95 Or (Eq (well_ordering (skS.0 1 a a_1)) False) (Or (Eq (connected (skS.0 1 a a_1)) True) (Eq False True)) % 4.74/4.95 Clause #121 (by clausification #[115]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (antisymmetric a) True)) % 4.74/4.95 Clause #122 (by clausification #[115]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (And (reflexive a) (transitive a)) True)) % 4.74/4.95 Clause #123 (by superposition #[121, 46]): ∀ (a a_1 : Iota), % 4.74/4.95 Or (Eq (well_ordering (skS.0 1 a a_1)) False) (Or (Eq (antisymmetric (skS.0 1 a a_1)) True) (Eq False True)) % 4.74/4.95 Clause #128 (by clausification #[122]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (transitive a) True)) % 4.74/4.95 Clause #129 (by clausification #[122]): ∀ (a : Iota), Or (Eq (relation a) False) (Or (Eq (well_ordering a) False) (Eq (reflexive a) True)) % 4.74/4.95 Clause #130 (by superposition #[128, 46]): ∀ (a a_1 : Iota), % 4.83/4.97 Or (Eq (well_ordering (skS.0 1 a a_1)) False) (Or (Eq (transitive (skS.0 1 a a_1)) True) (Eq False True)) % 4.83/4.97 Clause #135 (by clausification #[50]): ∀ (a a_1 a_2 : Iota), % 4.83/4.97 Or (Eq (connected (skS.0 1 a a_1)) False) (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.83/4.97 Clause #136 (by superposition #[129, 46]): ∀ (a a_1 : Iota), % 4.83/4.97 Or (Eq (well_ordering (skS.0 1 a a_1)) False) (Or (Eq (reflexive (skS.0 1 a a_1)) True) (Eq False True)) % 4.83/4.97 Clause #141 (by clausification #[109]): ∀ (a a_1 : Iota), Or (Eq (well_ordering (skS.0 1 a a_1)) False) (Eq (well_founded_relation (skS.0 1 a a_1)) True) % 4.83/4.97 Clause #142 (by forward demodulation #[141, 86]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (well_founded_relation (skS.0 1 a a_1)) True) % 4.83/4.97 Clause #143 (by clausification #[142]): ∀ (a a_1 : Iota), Eq (well_founded_relation (skS.0 1 a a_1)) True % 4.83/4.97 Clause #144 (by backward demodulation #[143, 97]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (well_founded_relation (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.83/4.97 Clause #145 (by clausification #[144]): ∀ (a a_1 a_2 : Iota), Eq (well_founded_relation (relation_restriction (skS.0 1 a a_1) a_2)) True % 4.83/4.97 Clause #160 (by clausification #[136]): ∀ (a a_1 : Iota), Or (Eq (well_ordering (skS.0 1 a a_1)) False) (Eq (reflexive (skS.0 1 a a_1)) True) % 4.83/4.97 Clause #161 (by forward demodulation #[160, 86]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (reflexive (skS.0 1 a a_1)) True) % 4.83/4.97 Clause #162 (by clausification #[161]): ∀ (a a_1 : Iota), Eq (reflexive (skS.0 1 a a_1)) True % 4.83/4.97 Clause #163 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), % 4.83/4.97 Or (Eq (reflexive (skS.0 1 a a_1)) False) (Eq (reflexive (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.83/4.97 Clause #164 (by forward demodulation #[163, 162]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (reflexive (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.83/4.97 Clause #165 (by clausification #[164]): ∀ (a a_1 a_2 : Iota), Eq (reflexive (relation_restriction (skS.0 1 a a_1) a_2)) True % 4.83/4.97 Clause #166 (by clausification #[130]): ∀ (a a_1 : Iota), Or (Eq (well_ordering (skS.0 1 a a_1)) False) (Eq (transitive (skS.0 1 a a_1)) True) % 4.83/4.97 Clause #167 (by forward demodulation #[166, 86]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (transitive (skS.0 1 a a_1)) True) % 4.83/4.97 Clause #168 (by clausification #[167]): ∀ (a a_1 : Iota), Eq (transitive (skS.0 1 a a_1)) True % 4.83/4.97 Clause #169 (by clausification #[116]): ∀ (a a_1 : Iota), Or (Eq (well_ordering (skS.0 1 a a_1)) False) (Eq (connected (skS.0 1 a a_1)) True) % 4.83/4.97 Clause #170 (by forward demodulation #[169, 86]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (connected (skS.0 1 a a_1)) True) % 4.83/4.97 Clause #171 (by clausification #[170]): ∀ (a a_1 : Iota), Eq (connected (skS.0 1 a a_1)) True % 4.83/4.97 Clause #172 (by backward demodulation #[171, 135]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.83/4.97 Clause #173 (by clausification #[172]): ∀ (a a_1 a_2 : Iota), Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) True % 4.83/4.97 Clause #174 (by clausification #[123]): ∀ (a a_1 : Iota), Or (Eq (well_ordering (skS.0 1 a a_1)) False) (Eq (antisymmetric (skS.0 1 a a_1)) True) % 4.83/4.97 Clause #175 (by forward demodulation #[174, 86]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (antisymmetric (skS.0 1 a a_1)) True) % 4.83/4.97 Clause #176 (by clausification #[175]): ∀ (a a_1 : Iota), Eq (antisymmetric (skS.0 1 a a_1)) True % 4.83/4.97 Clause #191 (by clausification #[52]): ∀ (a a_1 a_2 : Iota), % 4.83/4.97 Or (Eq (antisymmetric (skS.0 1 a a_1)) False) (Eq (antisymmetric (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.83/4.97 Clause #192 (by forward demodulation #[191, 176]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (antisymmetric (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.83/4.97 Clause #193 (by clausification #[192]): ∀ (a a_1 a_2 : Iota), Eq (antisymmetric (relation_restriction (skS.0 1 a a_1) a_2)) True % 4.83/4.97 Clause #198 (by clausification #[53]): ∀ (a a_1 a_2 : Iota), % 4.83/4.97 Or (Eq (transitive (skS.0 1 a a_1)) False) (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.83/4.97 Clause #199 (by forward demodulation #[198, 168]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.85/5.00 Clause #200 (by clausification #[199]): ∀ (a a_1 a_2 : Iota), Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) True % 4.85/5.00 Clause #256 (by clausification #[70]): ∀ (a a_1 a_2 : Iota), % 4.85/5.00 Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.85/5.00 (Or (Eq (well_founded_relation (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Or (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Or (Eq (antisymmetric (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Or (Eq (reflexive (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) False))))) % 4.85/5.00 Clause #257 (by forward demodulation #[256, 145]): ∀ (a a_1 a_2 : Iota), % 4.85/5.00 Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.85/5.00 (Or (Eq True False) % 4.85/5.00 (Or (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Or (Eq (antisymmetric (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Or (Eq (reflexive (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) False))))) % 4.85/5.00 Clause #258 (by clausification #[257]): ∀ (a a_1 a_2 : Iota), % 4.85/5.00 Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.85/5.00 (Or (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Or (Eq (antisymmetric (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Or (Eq (reflexive (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) False)))) % 4.85/5.00 Clause #259 (by forward demodulation #[258, 193]): ∀ (a a_1 a_2 : Iota), % 4.85/5.00 Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.85/5.00 (Or (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Or (Eq True False) % 4.85/5.00 (Or (Eq (reflexive (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) False)))) % 4.85/5.00 Clause #260 (by clausification #[259]): ∀ (a a_1 a_2 : Iota), % 4.85/5.00 Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.85/5.00 (Or (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Or (Eq (reflexive (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) False))) % 4.85/5.00 Clause #261 (by forward demodulation #[260, 165]): ∀ (a a_1 a_2 : Iota), % 4.85/5.00 Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.85/5.00 (Or (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Or (Eq True False) (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) False))) % 4.85/5.00 Clause #262 (by clausification #[261]): ∀ (a a_1 a_2 : Iota), % 4.85/5.00 Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.85/5.00 (Or (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 (Eq (transitive (relation_restriction (skS.0 1 a a_1) a_2)) False)) % 4.85/5.00 Clause #263 (by forward demodulation #[262, 200]): ∀ (a a_1 a_2 : Iota), % 4.85/5.00 Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.85/5.00 (Or (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) False) (Eq True False)) % 4.85/5.00 Clause #264 (by clausification #[263]): ∀ (a a_1 a_2 : Iota), % 4.85/5.00 Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) % 4.85/5.00 (Eq (connected (relation_restriction (skS.0 1 a a_1) a_2)) False) % 4.85/5.00 Clause #265 (by superposition #[264, 173]): ∀ (a a_1 a_2 : Iota), Or (Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True) (Eq False True) % 4.85/5.00 Clause #266 (by clausification #[265]): ∀ (a a_1 a_2 : Iota), Eq (well_ordering (relation_restriction (skS.0 1 a a_1) a_2)) True % 4.85/5.00 Clause #268 (by superposition #[266, 87]): Eq True False % 4.85/5.00 Clause #269 (by clausification #[268]): False % 4.85/5.00 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------