%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LAT382+1 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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 07:53:33 PM UTC 2025 % Result : Theorem 4.50s 4.69s % Output : Proof 4.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : LAT382+1 : TPTP v9.2.0. Released v4.0.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 18:16:08 EDT 2025 % 0.13/0.34 % CPUTime : % 4.50/4.69 SZS status Theorem for theBenchmark.p % 4.50/4.69 SZS output start Proof for theBenchmark.p % 4.50/4.69 Clause #2 (by assumption #[]): Eq (∀ (W0 : Iota), aSet0 W0 → ∀ (W1 : Iota), aElementOf0 W1 W0 → aElement0 W1) True % 4.50/4.69 Clause #7 (by assumption #[]): Eq (∀ (W0 W1 : Iota), And (aElement0 W0) (aElement0 W1) → And (sdtlseqdt0 W0 W1) (sdtlseqdt0 W1 W0) → Eq W0 W1) True % 4.50/4.69 Clause #9 (by assumption #[]): Eq % 4.50/4.69 (∀ (W0 : Iota), % 4.50/4.69 aSet0 W0 → % 4.50/4.69 ∀ (W1 : Iota), % 4.50/4.69 aSubsetOf0 W1 W0 → % 4.50/4.69 ∀ (W2 : Iota), % 4.50/4.69 Iff (aLowerBoundOfIn0 W2 W1 W0) % 4.50/4.69 (And (aElementOf0 W2 W0) (∀ (W3 : Iota), aElementOf0 W3 W1 → sdtlseqdt0 W2 W3))) % 4.50/4.69 True % 4.50/4.69 Clause #11 (by assumption #[]): Eq % 4.50/4.69 (∀ (W0 : Iota), % 4.50/4.69 aSet0 W0 → % 4.50/4.69 ∀ (W1 : Iota), % 4.50/4.69 aSubsetOf0 W1 W0 → % 4.50/4.69 ∀ (W2 : Iota), % 4.50/4.69 Iff (aInfimumOfIn0 W2 W1 W0) % 4.50/4.69 (And (And (aElementOf0 W2 W0) (aLowerBoundOfIn0 W2 W1 W0)) % 4.50/4.69 (∀ (W3 : Iota), aLowerBoundOfIn0 W3 W1 W0 → sdtlseqdt0 W3 W2))) % 4.50/4.69 True % 4.50/4.69 Clause #14 (by assumption #[]): Eq (aSet0 xT) True % 4.50/4.69 Clause #15 (by assumption #[]): Eq (aSubsetOf0 xS xT) True % 4.50/4.69 Clause #16 (by assumption #[]): Eq (And (aInfimumOfIn0 xu xS xT) (aInfimumOfIn0 xv xS xT)) True % 4.50/4.69 Clause #17 (by assumption #[]): Eq (Not (Eq xu xv)) True % 4.50/4.69 Clause #24 (by clausification #[2]): ∀ (a : Iota), Eq (aSet0 a → ∀ (W1 : Iota), aElementOf0 W1 a → aElement0 W1) True % 4.50/4.69 Clause #25 (by clausification #[24]): ∀ (a : Iota), Or (Eq (aSet0 a) False) (Eq (∀ (W1 : Iota), aElementOf0 W1 a → aElement0 W1) True) % 4.50/4.69 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), Or (Eq (aSet0 a) False) (Eq (aElementOf0 a_1 a → aElement0 a_1) True) % 4.50/4.69 Clause #27 (by clausification #[26]): ∀ (a a_1 : Iota), Or (Eq (aSet0 a) False) (Or (Eq (aElementOf0 a_1 a) False) (Eq (aElement0 a_1) True)) % 4.50/4.69 Clause #28 (by superposition #[27, 14]): ∀ (a : Iota), Or (Eq (aElementOf0 a xT) False) (Or (Eq (aElement0 a) True) (Eq False True)) % 4.50/4.69 Clause #34 (by clausification #[17]): Eq (Eq xu xv) False % 4.50/4.69 Clause #35 (by clausification #[34]): Ne xu xv % 4.50/4.69 Clause #36 (by clausification #[7]): ∀ (a : Iota), % 4.50/4.69 Eq (∀ (W1 : Iota), And (aElement0 a) (aElement0 W1) → And (sdtlseqdt0 a W1) (sdtlseqdt0 W1 a) → Eq a W1) True % 4.50/4.69 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), Eq (And (aElement0 a) (aElement0 a_1) → And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) True % 4.50/4.69 Clause #38 (by clausification #[37]): ∀ (a a_1 : Iota), % 4.50/4.69 Or (Eq (And (aElement0 a) (aElement0 a_1)) False) (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) True) % 4.50/4.69 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), % 4.50/4.69 Or (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) True) % 4.50/4.69 (Or (Eq (aElement0 a) False) (Eq (aElement0 a_1) False)) % 4.50/4.69 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), % 4.50/4.69 Or (Eq (aElement0 a) False) % 4.50/4.69 (Or (Eq (aElement0 a_1) False) (Or (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a)) False) (Eq (Eq a a_1) True))) % 4.50/4.69 Clause #41 (by clausification #[40]): ∀ (a a_1 : Iota), % 4.50/4.69 Or (Eq (aElement0 a) False) % 4.50/4.69 (Or (Eq (aElement0 a_1) False) % 4.50/4.69 (Or (Eq (Eq a a_1) True) (Or (Eq (sdtlseqdt0 a a_1) False) (Eq (sdtlseqdt0 a_1 a) False)))) % 4.50/4.69 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), % 4.50/4.69 Or (Eq (aElement0 a) False) % 4.50/4.69 (Or (Eq (aElement0 a_1) False) (Or (Eq (sdtlseqdt0 a a_1) False) (Or (Eq (sdtlseqdt0 a_1 a) False) (Eq a a_1)))) % 4.50/4.69 Clause #43 (by clausification #[28]): ∀ (a : Iota), Or (Eq (aElementOf0 a xT) False) (Eq (aElement0 a) True) % 4.50/4.69 Clause #59 (by clausification #[16]): Eq (aInfimumOfIn0 xv xS xT) True % 4.50/4.69 Clause #60 (by clausification #[16]): Eq (aInfimumOfIn0 xu xS xT) True % 4.50/4.69 Clause #103 (by clausification #[9]): ∀ (a : Iota), % 4.50/4.69 Eq % 4.50/4.69 (aSet0 a → % 4.50/4.69 ∀ (W1 : Iota), % 4.50/4.69 aSubsetOf0 W1 a → % 4.50/4.69 ∀ (W2 : Iota), % 4.50/4.69 Iff (aLowerBoundOfIn0 W2 W1 a) % 4.50/4.69 (And (aElementOf0 W2 a) (∀ (W3 : Iota), aElementOf0 W3 W1 → sdtlseqdt0 W2 W3))) % 4.50/4.69 True % 4.50/4.69 Clause #104 (by clausification #[103]): ∀ (a : Iota), % 4.50/4.69 Or (Eq (aSet0 a) False) % 4.50/4.69 (Eq % 4.50/4.69 (∀ (W1 : Iota), % 4.50/4.69 aSubsetOf0 W1 a → % 4.50/4.69 ∀ (W2 : Iota), % 4.50/4.71 Iff (aLowerBoundOfIn0 W2 W1 a) % 4.50/4.71 (And (aElementOf0 W2 a) (∀ (W3 : Iota), aElementOf0 W3 W1 → sdtlseqdt0 W2 W3))) % 4.50/4.71 True) % 4.50/4.71 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), % 4.50/4.71 Or (Eq (aSet0 a) False) % 4.50/4.71 (Eq % 4.50/4.71 (aSubsetOf0 a_1 a → % 4.50/4.71 ∀ (W2 : Iota), % 4.50/4.71 Iff (aLowerBoundOfIn0 W2 a_1 a) % 4.50/4.71 (And (aElementOf0 W2 a) (∀ (W3 : Iota), aElementOf0 W3 a_1 → sdtlseqdt0 W2 W3))) % 4.50/4.71 True) % 4.50/4.71 Clause #106 (by clausification #[105]): ∀ (a a_1 : Iota), % 4.50/4.71 Or (Eq (aSet0 a) False) % 4.50/4.71 (Or (Eq (aSubsetOf0 a_1 a) False) % 4.50/4.71 (Eq % 4.50/4.71 (∀ (W2 : Iota), % 4.50/4.71 Iff (aLowerBoundOfIn0 W2 a_1 a) % 4.50/4.71 (And (aElementOf0 W2 a) (∀ (W3 : Iota), aElementOf0 W3 a_1 → sdtlseqdt0 W2 W3))) % 4.50/4.71 True)) % 4.50/4.71 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 4.50/4.71 Or (Eq (aSet0 a) False) % 4.50/4.71 (Or (Eq (aSubsetOf0 a_1 a) False) % 4.50/4.71 (Eq % 4.50/4.71 (Iff (aLowerBoundOfIn0 a_2 a_1 a) % 4.50/4.71 (And (aElementOf0 a_2 a) (∀ (W3 : Iota), aElementOf0 W3 a_1 → sdtlseqdt0 a_2 W3))) % 4.50/4.71 True)) % 4.50/4.71 Clause #109 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 4.50/4.71 Or (Eq (aSet0 a) False) % 4.50/4.71 (Or (Eq (aSubsetOf0 a_1 a) False) % 4.50/4.71 (Or (Eq (aLowerBoundOfIn0 a_2 a_1 a) False) % 4.50/4.71 (Eq (And (aElementOf0 a_2 a) (∀ (W3 : Iota), aElementOf0 W3 a_1 → sdtlseqdt0 a_2 W3)) True))) % 4.50/4.71 Clause #151 (by clausification #[11]): ∀ (a : Iota), % 4.50/4.71 Eq % 4.50/4.71 (aSet0 a → % 4.50/4.71 ∀ (W1 : Iota), % 4.50/4.71 aSubsetOf0 W1 a → % 4.50/4.71 ∀ (W2 : Iota), % 4.50/4.71 Iff (aInfimumOfIn0 W2 W1 a) % 4.50/4.71 (And (And (aElementOf0 W2 a) (aLowerBoundOfIn0 W2 W1 a)) % 4.50/4.71 (∀ (W3 : Iota), aLowerBoundOfIn0 W3 W1 a → sdtlseqdt0 W3 W2))) % 4.50/4.71 True % 4.50/4.71 Clause #152 (by clausification #[151]): ∀ (a : Iota), % 4.50/4.71 Or (Eq (aSet0 a) False) % 4.50/4.71 (Eq % 4.50/4.71 (∀ (W1 : Iota), % 4.50/4.71 aSubsetOf0 W1 a → % 4.50/4.71 ∀ (W2 : Iota), % 4.50/4.71 Iff (aInfimumOfIn0 W2 W1 a) % 4.50/4.71 (And (And (aElementOf0 W2 a) (aLowerBoundOfIn0 W2 W1 a)) % 4.50/4.71 (∀ (W3 : Iota), aLowerBoundOfIn0 W3 W1 a → sdtlseqdt0 W3 W2))) % 4.50/4.71 True) % 4.50/4.71 Clause #153 (by clausification #[152]): ∀ (a a_1 : Iota), % 4.50/4.71 Or (Eq (aSet0 a) False) % 4.50/4.71 (Eq % 4.50/4.71 (aSubsetOf0 a_1 a → % 4.50/4.71 ∀ (W2 : Iota), % 4.50/4.71 Iff (aInfimumOfIn0 W2 a_1 a) % 4.50/4.71 (And (And (aElementOf0 W2 a) (aLowerBoundOfIn0 W2 a_1 a)) % 4.50/4.71 (∀ (W3 : Iota), aLowerBoundOfIn0 W3 a_1 a → sdtlseqdt0 W3 W2))) % 4.50/4.71 True) % 4.50/4.71 Clause #154 (by clausification #[153]): ∀ (a a_1 : Iota), % 4.50/4.71 Or (Eq (aSet0 a) False) % 4.50/4.71 (Or (Eq (aSubsetOf0 a_1 a) False) % 4.50/4.71 (Eq % 4.50/4.71 (∀ (W2 : Iota), % 4.50/4.71 Iff (aInfimumOfIn0 W2 a_1 a) % 4.50/4.71 (And (And (aElementOf0 W2 a) (aLowerBoundOfIn0 W2 a_1 a)) % 4.50/4.71 (∀ (W3 : Iota), aLowerBoundOfIn0 W3 a_1 a → sdtlseqdt0 W3 W2))) % 4.50/4.71 True)) % 4.50/4.71 Clause #155 (by clausification #[154]): ∀ (a a_1 a_2 : Iota), % 4.50/4.71 Or (Eq (aSet0 a) False) % 4.50/4.71 (Or (Eq (aSubsetOf0 a_1 a) False) % 4.50/4.71 (Eq % 4.50/4.71 (Iff (aInfimumOfIn0 a_2 a_1 a) % 4.50/4.71 (And (And (aElementOf0 a_2 a) (aLowerBoundOfIn0 a_2 a_1 a)) % 4.50/4.71 (∀ (W3 : Iota), aLowerBoundOfIn0 W3 a_1 a → sdtlseqdt0 W3 a_2))) % 4.50/4.71 True)) % 4.50/4.71 Clause #157 (by clausification #[155]): ∀ (a a_1 a_2 : Iota), % 4.50/4.71 Or (Eq (aSet0 a) False) % 4.50/4.71 (Or (Eq (aSubsetOf0 a_1 a) False) % 4.50/4.71 (Or (Eq (aInfimumOfIn0 a_2 a_1 a) False) % 4.50/4.71 (Eq % 4.50/4.71 (And (And (aElementOf0 a_2 a) (aLowerBoundOfIn0 a_2 a_1 a)) % 4.50/4.71 (∀ (W3 : Iota), aLowerBoundOfIn0 W3 a_1 a → sdtlseqdt0 W3 a_2)) % 4.50/4.71 True))) % 4.50/4.71 Clause #197 (by clausification #[109]): ∀ (a a_1 a_2 : Iota), % 4.50/4.71 Or (Eq (aSet0 a) False) % 4.50/4.71 (Or (Eq (aSubsetOf0 a_1 a) False) (Or (Eq (aLowerBoundOfIn0 a_2 a_1 a) False) (Eq (aElementOf0 a_2 a) True))) % 4.50/4.71 Clause #202 (by superposition #[197, 14]): ∀ (a a_1 : Iota), % 4.50/4.71 Or (Eq (aSubsetOf0 a xT) False) % 4.50/4.71 (Or (Eq (aLowerBoundOfIn0 a_1 a xT) False) (Or (Eq (aElementOf0 a_1 xT) True) (Eq False True))) % 4.50/4.71 Clause #207 (by clausification #[202]): ∀ (a a_1 : Iota), % 4.50/4.71 Or (Eq (aSubsetOf0 a xT) False) (Or (Eq (aLowerBoundOfIn0 a_1 a xT) False) (Eq (aElementOf0 a_1 xT) True)) % 4.50/4.71 Clause #208 (by superposition #[207, 15]): ∀ (a : Iota), Or (Eq (aLowerBoundOfIn0 a xS xT) False) (Or (Eq (aElementOf0 a xT) True) (Eq False True)) % 4.50/4.73 Clause #209 (by clausification #[208]): ∀ (a : Iota), Or (Eq (aLowerBoundOfIn0 a xS xT) False) (Eq (aElementOf0 a xT) True) % 4.50/4.73 Clause #337 (by clausification #[157]): ∀ (a a_1 a_2 : Iota), % 4.50/4.73 Or (Eq (aSet0 a) False) % 4.50/4.73 (Or (Eq (aSubsetOf0 a_1 a) False) % 4.50/4.73 (Or (Eq (aInfimumOfIn0 a_2 a_1 a) False) % 4.50/4.73 (Eq (∀ (W3 : Iota), aLowerBoundOfIn0 W3 a_1 a → sdtlseqdt0 W3 a_2) True))) % 4.50/4.73 Clause #338 (by clausification #[157]): ∀ (a a_1 a_2 : Iota), % 4.50/4.73 Or (Eq (aSet0 a) False) % 4.50/4.73 (Or (Eq (aSubsetOf0 a_1 a) False) % 4.50/4.73 (Or (Eq (aInfimumOfIn0 a_2 a_1 a) False) (Eq (And (aElementOf0 a_2 a) (aLowerBoundOfIn0 a_2 a_1 a)) True))) % 4.50/4.73 Clause #339 (by clausification #[337]): ∀ (a a_1 a_2 a_3 : Iota), % 4.50/4.73 Or (Eq (aSet0 a) False) % 4.50/4.73 (Or (Eq (aSubsetOf0 a_1 a) False) % 4.50/4.73 (Or (Eq (aInfimumOfIn0 a_2 a_1 a) False) (Eq (aLowerBoundOfIn0 a_3 a_1 a → sdtlseqdt0 a_3 a_2) True))) % 4.50/4.73 Clause #340 (by clausification #[339]): ∀ (a a_1 a_2 a_3 : Iota), % 4.50/4.73 Or (Eq (aSet0 a) False) % 4.50/4.73 (Or (Eq (aSubsetOf0 a_1 a) False) % 4.50/4.73 (Or (Eq (aInfimumOfIn0 a_2 a_1 a) False) % 4.50/4.73 (Or (Eq (aLowerBoundOfIn0 a_3 a_1 a) False) (Eq (sdtlseqdt0 a_3 a_2) True)))) % 4.50/4.73 Clause #341 (by superposition #[340, 14]): ∀ (a a_1 a_2 : Iota), % 4.50/4.73 Or (Eq (aSubsetOf0 a xT) False) % 4.50/4.73 (Or (Eq (aInfimumOfIn0 a_1 a xT) False) % 4.50/4.73 (Or (Eq (aLowerBoundOfIn0 a_2 a xT) False) (Or (Eq (sdtlseqdt0 a_2 a_1) True) (Eq False True)))) % 4.50/4.73 Clause #350 (by clausification #[341]): ∀ (a a_1 a_2 : Iota), % 4.50/4.73 Or (Eq (aSubsetOf0 a xT) False) % 4.50/4.73 (Or (Eq (aInfimumOfIn0 a_1 a xT) False) (Or (Eq (aLowerBoundOfIn0 a_2 a xT) False) (Eq (sdtlseqdt0 a_2 a_1) True))) % 4.50/4.73 Clause #351 (by superposition #[350, 15]): ∀ (a a_1 : Iota), % 4.50/4.73 Or (Eq (aInfimumOfIn0 a xS xT) False) % 4.50/4.73 (Or (Eq (aLowerBoundOfIn0 a_1 xS xT) False) (Or (Eq (sdtlseqdt0 a_1 a) True) (Eq False True))) % 4.50/4.73 Clause #354 (by clausification #[351]): ∀ (a a_1 : Iota), % 4.50/4.73 Or (Eq (aInfimumOfIn0 a xS xT) False) (Or (Eq (aLowerBoundOfIn0 a_1 xS xT) False) (Eq (sdtlseqdt0 a_1 a) True)) % 4.50/4.73 Clause #355 (by superposition #[354, 59]): ∀ (a : Iota), Or (Eq (aLowerBoundOfIn0 a xS xT) False) (Or (Eq (sdtlseqdt0 a xv) True) (Eq False True)) % 4.50/4.73 Clause #356 (by superposition #[354, 60]): ∀ (a : Iota), Or (Eq (aLowerBoundOfIn0 a xS xT) False) (Or (Eq (sdtlseqdt0 a xu) True) (Eq False True)) % 4.50/4.73 Clause #357 (by clausification #[356]): ∀ (a : Iota), Or (Eq (aLowerBoundOfIn0 a xS xT) False) (Eq (sdtlseqdt0 a xu) True) % 4.50/4.73 Clause #362 (by clausification #[355]): ∀ (a : Iota), Or (Eq (aLowerBoundOfIn0 a xS xT) False) (Eq (sdtlseqdt0 a xv) True) % 4.50/4.73 Clause #363 (by clausification #[338]): ∀ (a a_1 a_2 : Iota), % 4.50/4.73 Or (Eq (aSet0 a) False) % 4.50/4.73 (Or (Eq (aSubsetOf0 a_1 a) False) (Or (Eq (aInfimumOfIn0 a_2 a_1 a) False) (Eq (aLowerBoundOfIn0 a_2 a_1 a) True))) % 4.50/4.73 Clause #365 (by superposition #[363, 14]): ∀ (a a_1 : Iota), % 4.50/4.73 Or (Eq (aSubsetOf0 a xT) False) % 4.50/4.73 (Or (Eq (aInfimumOfIn0 a_1 a xT) False) (Or (Eq (aLowerBoundOfIn0 a_1 a xT) True) (Eq False True))) % 4.50/4.73 Clause #370 (by clausification #[365]): ∀ (a a_1 : Iota), % 4.50/4.73 Or (Eq (aSubsetOf0 a xT) False) (Or (Eq (aInfimumOfIn0 a_1 a xT) False) (Eq (aLowerBoundOfIn0 a_1 a xT) True)) % 4.50/4.73 Clause #371 (by superposition #[370, 15]): ∀ (a : Iota), Or (Eq (aInfimumOfIn0 a xS xT) False) (Or (Eq (aLowerBoundOfIn0 a xS xT) True) (Eq False True)) % 4.50/4.73 Clause #378 (by clausification #[371]): ∀ (a : Iota), Or (Eq (aInfimumOfIn0 a xS xT) False) (Eq (aLowerBoundOfIn0 a xS xT) True) % 4.50/4.73 Clause #379 (by superposition #[378, 59]): Or (Eq (aLowerBoundOfIn0 xv xS xT) True) (Eq False True) % 4.50/4.73 Clause #380 (by superposition #[378, 60]): Or (Eq (aLowerBoundOfIn0 xu xS xT) True) (Eq False True) % 4.50/4.73 Clause #381 (by clausification #[380]): Eq (aLowerBoundOfIn0 xu xS xT) True % 4.50/4.73 Clause #382 (by superposition #[381, 209]): Or (Eq True False) (Eq (aElementOf0 xu xT) True) % 4.50/4.73 Clause #385 (by superposition #[381, 362]): Or (Eq True False) (Eq (sdtlseqdt0 xu xv) True) % 4.50/4.73 Clause #386 (by clausification #[385]): Eq (sdtlseqdt0 xu xv) True % 4.50/4.73 Clause #390 (by clausification #[382]): Eq (aElementOf0 xu xT) True % 4.57/4.74 Clause #391 (by superposition #[390, 43]): Or (Eq True False) (Eq (aElement0 xu) True) % 4.57/4.74 Clause #396 (by clausification #[391]): Eq (aElement0 xu) True % 4.57/4.74 Clause #403 (by clausification #[379]): Eq (aLowerBoundOfIn0 xv xS xT) True % 4.57/4.74 Clause #404 (by superposition #[403, 209]): Or (Eq True False) (Eq (aElementOf0 xv xT) True) % 4.57/4.74 Clause #406 (by superposition #[403, 357]): Or (Eq True False) (Eq (sdtlseqdt0 xv xu) True) % 4.57/4.74 Clause #409 (by clausification #[406]): Eq (sdtlseqdt0 xv xu) True % 4.57/4.74 Clause #413 (by clausification #[404]): Eq (aElementOf0 xv xT) True % 4.57/4.74 Clause #414 (by superposition #[413, 43]): Or (Eq True False) (Eq (aElement0 xv) True) % 4.57/4.74 Clause #419 (by clausification #[414]): Eq (aElement0 xv) True % 4.57/4.74 Clause #420 (by superposition #[419, 42]): ∀ (a : Iota), % 4.57/4.74 Or (Eq True False) % 4.57/4.74 (Or (Eq (aElement0 a) False) (Or (Eq (sdtlseqdt0 xv a) False) (Or (Eq (sdtlseqdt0 a xv) False) (Eq xv a)))) % 4.57/4.74 Clause #430 (by clausification #[420]): ∀ (a : Iota), Or (Eq (aElement0 a) False) (Or (Eq (sdtlseqdt0 xv a) False) (Or (Eq (sdtlseqdt0 a xv) False) (Eq xv a))) % 4.57/4.74 Clause #434 (by superposition #[430, 396]): Or (Eq (sdtlseqdt0 xv xu) False) (Or (Eq (sdtlseqdt0 xu xv) False) (Or (Eq xv xu) (Eq False True))) % 4.57/4.74 Clause #439 (by clausification #[434]): Or (Eq (sdtlseqdt0 xv xu) False) (Or (Eq (sdtlseqdt0 xu xv) False) (Eq xv xu)) % 4.57/4.74 Clause #440 (by forward demodulation #[439, 386]): Or (Eq (sdtlseqdt0 xv xu) False) (Or (Eq True False) (Eq xv xu)) % 4.57/4.74 Clause #441 (by clausification #[440]): Or (Eq (sdtlseqdt0 xv xu) False) (Eq xv xu) % 4.57/4.74 Clause #442 (by forward contextual literal cutting #[441, 35]): Eq (sdtlseqdt0 xv xu) False % 4.57/4.74 Clause #443 (by superposition #[442, 409]): Eq False True % 4.57/4.74 Clause #444 (by clausification #[443]): False % 4.57/4.74 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------