%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET988+1 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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:00:46 PM UTC 2025 % Result : Theorem 117.77s 117.97s % Output : Proof 117.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET988+1 : TPTP v9.2.0. Released v3.2.0. % 0.03/0.13 % Command : duper %s % 0.14/0.34 % Computer : n029.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 13:32:38 EDT 2025 % 0.14/0.34 % CPUTime : % 117.77/117.97 SZS status Theorem for theBenchmark.p % 117.77/117.97 SZS output start Proof for theBenchmark.p % 117.77/117.97 Clause #30 (by assumption #[]): Eq % 117.77/117.97 (Not % 117.77/117.97 (∀ (A : Iota), % 117.77/117.97 And (∀ (B : Iota), Not (And (in B A) (∀ (C D : Iota), Ne (ordered_pair C D) B))) % 117.77/117.97 (∀ (B C D : Iota), And (in (ordered_pair B C) A) (in (ordered_pair B D) A) → Eq C D) → % 117.77/117.97 And (relation A) (function A))) % 117.77/117.97 True % 117.77/117.97 Clause #31 (by assumption #[]): Eq (∀ (A : Iota), Iff (function A) (∀ (B C D : Iota), And (in (ordered_pair B C) A) (in (ordered_pair B D) A) → Eq C D)) % 117.77/117.97 True % 117.77/117.97 Clause #32 (by assumption #[]): Eq (∀ (A : Iota), Iff (relation A) (∀ (B : Iota), Not (And (in B A) (∀ (C D : Iota), Ne B (ordered_pair C D))))) True % 117.77/117.97 Clause #91 (by clausification #[30]): Eq % 117.77/117.97 (∀ (A : Iota), % 117.77/117.97 And (∀ (B : Iota), Not (And (in B A) (∀ (C D : Iota), Ne (ordered_pair C D) B))) % 117.77/117.97 (∀ (B C D : Iota), And (in (ordered_pair B C) A) (in (ordered_pair B D) A) → Eq C D) → % 117.77/117.97 And (relation A) (function A)) % 117.77/117.97 False % 117.77/117.97 Clause #92 (by clausification #[91]): ∀ (a : Iota), % 117.77/117.97 Eq % 117.77/117.97 (Not % 117.77/117.97 (And (∀ (B : Iota), Not (And (in B (skS.0 4 a)) (∀ (C D : Iota), Ne (ordered_pair C D) B))) % 117.77/117.97 (∀ (B C D : Iota), And (in (ordered_pair B C) (skS.0 4 a)) (in (ordered_pair B D) (skS.0 4 a)) → Eq C D) → % 117.77/117.97 And (relation (skS.0 4 a)) (function (skS.0 4 a)))) % 117.77/117.97 True % 117.77/117.97 Clause #93 (by clausification #[92]): ∀ (a : Iota), % 117.77/117.97 Eq % 117.77/117.97 (And (∀ (B : Iota), Not (And (in B (skS.0 4 a)) (∀ (C D : Iota), Ne (ordered_pair C D) B))) % 117.77/117.97 (∀ (B C D : Iota), And (in (ordered_pair B C) (skS.0 4 a)) (in (ordered_pair B D) (skS.0 4 a)) → Eq C D) → % 117.77/117.97 And (relation (skS.0 4 a)) (function (skS.0 4 a))) % 117.77/117.97 False % 117.77/117.97 Clause #94 (by clausification #[93]): ∀ (a : Iota), % 117.77/117.97 Eq % 117.77/117.97 (And (∀ (B : Iota), Not (And (in B (skS.0 4 a)) (∀ (C D : Iota), Ne (ordered_pair C D) B))) % 117.77/117.97 (∀ (B C D : Iota), And (in (ordered_pair B C) (skS.0 4 a)) (in (ordered_pair B D) (skS.0 4 a)) → Eq C D)) % 117.77/117.97 True % 117.77/117.97 Clause #95 (by clausification #[93]): ∀ (a : Iota), Eq (And (relation (skS.0 4 a)) (function (skS.0 4 a))) False % 117.77/117.97 Clause #96 (by clausification #[94]): ∀ (a : Iota), % 117.77/117.97 Eq (∀ (B C D : Iota), And (in (ordered_pair B C) (skS.0 4 a)) (in (ordered_pair B D) (skS.0 4 a)) → Eq C D) True % 117.77/117.97 Clause #97 (by clausification #[94]): ∀ (a : Iota), Eq (∀ (B : Iota), Not (And (in B (skS.0 4 a)) (∀ (C D : Iota), Ne (ordered_pair C D) B))) True % 117.77/117.97 Clause #98 (by clausification #[96]): ∀ (a a_1 : Iota), % 117.77/117.97 Eq (∀ (C D : Iota), And (in (ordered_pair a C) (skS.0 4 a_1)) (in (ordered_pair a D) (skS.0 4 a_1)) → Eq C D) True % 117.77/117.97 Clause #99 (by clausification #[98]): ∀ (a a_1 a_2 : Iota), % 117.77/117.97 Eq (∀ (D : Iota), And (in (ordered_pair a a_1) (skS.0 4 a_2)) (in (ordered_pair a D) (skS.0 4 a_2)) → Eq a_1 D) True % 117.77/117.97 Clause #100 (by clausification #[99]): ∀ (a a_1 a_2 a_3 : Iota), % 117.77/117.97 Eq (And (in (ordered_pair a a_1) (skS.0 4 a_2)) (in (ordered_pair a a_3) (skS.0 4 a_2)) → Eq a_1 a_3) True % 117.77/117.97 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 a_3 : Iota), % 117.77/117.97 Or (Eq (And (in (ordered_pair a a_1) (skS.0 4 a_2)) (in (ordered_pair a a_3) (skS.0 4 a_2))) False) % 117.77/117.97 (Eq (Eq a_1 a_3) True) % 117.77/117.97 Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 a_3 : Iota), % 117.77/117.97 Or (Eq (Eq a a_1) True) % 117.77/117.97 (Or (Eq (in (ordered_pair a_2 a) (skS.0 4 a_3)) False) (Eq (in (ordered_pair a_2 a_1) (skS.0 4 a_3)) False)) % 117.77/117.97 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 a_3 : Iota), % 117.77/117.97 Or (Eq (in (ordered_pair a a_1) (skS.0 4 a_2)) False) % 117.77/117.97 (Or (Eq (in (ordered_pair a a_3) (skS.0 4 a_2)) False) (Eq a_1 a_3)) % 117.77/117.97 Clause #202 (by clausification #[31]): ∀ (a : Iota), % 117.77/117.97 Eq (Iff (function a) (∀ (B C D : Iota), And (in (ordered_pair B C) a) (in (ordered_pair B D) a) → Eq C D)) True % 117.77/117.97 Clause #203 (by clausification #[202]): ∀ (a : Iota), % 117.77/117.97 Or (Eq (function a) True) % 117.77/117.97 (Eq (∀ (B C D : Iota), And (in (ordered_pair B C) a) (in (ordered_pair B D) a) → Eq C D) False) % 117.77/117.97 Clause #205 (by clausification #[203]): ∀ (a a_1 : Iota), % 117.77/117.97 Or (Eq (function a) True) % 117.77/117.97 (Eq % 117.77/117.97 (Not % 117.77/117.97 (∀ (C D : Iota), % 117.77/117.97 And (in (ordered_pair (skS.0 10 a a_1) C) a) (in (ordered_pair (skS.0 10 a a_1) D) a) → Eq C D)) % 117.77/117.99 True) % 117.77/117.99 Clause #206 (by clausification #[205]): ∀ (a a_1 : Iota), % 117.77/117.99 Or (Eq (function a) True) % 117.77/117.99 (Eq (∀ (C D : Iota), And (in (ordered_pair (skS.0 10 a a_1) C) a) (in (ordered_pair (skS.0 10 a a_1) D) a) → Eq C D) % 117.77/117.99 False) % 117.77/117.99 Clause #207 (by clausification #[206]): ∀ (a a_1 a_2 : Iota), % 117.77/117.99 Or (Eq (function a) True) % 117.77/117.99 (Eq % 117.77/117.99 (Not % 117.77/117.99 (∀ (D : Iota), % 117.77/117.99 And (in (ordered_pair (skS.0 10 a a_1) (skS.0 11 a a_1 a_2)) a) (in (ordered_pair (skS.0 10 a a_1) D) a) → % 117.77/117.99 Eq (skS.0 11 a a_1 a_2) D)) % 117.77/117.99 True) % 117.77/117.99 Clause #208 (by clausification #[207]): ∀ (a a_1 a_2 : Iota), % 117.77/117.99 Or (Eq (function a) True) % 117.77/117.99 (Eq % 117.77/117.99 (∀ (D : Iota), % 117.77/117.99 And (in (ordered_pair (skS.0 10 a a_1) (skS.0 11 a a_1 a_2)) a) (in (ordered_pair (skS.0 10 a a_1) D) a) → % 117.77/117.99 Eq (skS.0 11 a a_1 a_2) D) % 117.77/117.99 False) % 117.77/117.99 Clause #209 (by clausification #[208]): ∀ (a a_1 a_2 a_3 : Iota), % 117.77/117.99 Or (Eq (function a) True) % 117.77/117.99 (Eq % 117.77/117.99 (Not % 117.77/117.99 (And (in (ordered_pair (skS.0 10 a a_1) (skS.0 11 a a_1 a_2)) a) % 117.77/117.99 (in (ordered_pair (skS.0 10 a a_1) (skS.0 12 a a_1 a_2 a_3)) a) → % 117.77/117.99 Eq (skS.0 11 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3))) % 117.77/117.99 True) % 117.77/117.99 Clause #210 (by clausification #[209]): ∀ (a a_1 a_2 a_3 : Iota), % 117.77/117.99 Or (Eq (function a) True) % 117.77/117.99 (Eq % 117.77/117.99 (And (in (ordered_pair (skS.0 10 a a_1) (skS.0 11 a a_1 a_2)) a) % 117.77/117.99 (in (ordered_pair (skS.0 10 a a_1) (skS.0 12 a a_1 a_2 a_3)) a) → % 117.77/117.99 Eq (skS.0 11 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3)) % 117.77/117.99 False) % 117.77/117.99 Clause #211 (by clausification #[210]): ∀ (a a_1 a_2 a_3 : Iota), % 117.77/117.99 Or (Eq (function a) True) % 117.77/117.99 (Eq % 117.77/117.99 (And (in (ordered_pair (skS.0 10 a a_1) (skS.0 11 a a_1 a_2)) a) % 117.77/117.99 (in (ordered_pair (skS.0 10 a a_1) (skS.0 12 a a_1 a_2 a_3)) a)) % 117.77/117.99 True) % 117.77/117.99 Clause #212 (by clausification #[210]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (function a) True) (Eq (Eq (skS.0 11 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3)) False) % 117.77/117.99 Clause #213 (by clausification #[211]): ∀ (a a_1 a_2 a_3 : Iota), % 117.77/117.99 Or (Eq (function a) True) (Eq (in (ordered_pair (skS.0 10 a a_1) (skS.0 12 a a_1 a_2 a_3)) a) True) % 117.77/117.99 Clause #214 (by clausification #[211]): ∀ (a a_1 a_2 : Iota), Or (Eq (function a) True) (Eq (in (ordered_pair (skS.0 10 a a_1) (skS.0 11 a a_1 a_2)) a) True) % 117.77/117.99 Clause #215 (by superposition #[213, 103]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 117.77/117.99 Or (Eq (function (skS.0 4 a)) True) % 117.77/117.99 (Or (Eq True False) % 117.77/117.99 (Or (Eq (in (ordered_pair (skS.0 10 (skS.0 4 a) a_1) a_2) (skS.0 4 a)) False) % 117.77/117.99 (Eq (skS.0 12 (skS.0 4 a) a_1 a_3 a_4) a_2))) % 117.77/117.99 Clause #231 (by clausification #[32]): ∀ (a : Iota), Eq (Iff (relation a) (∀ (B : Iota), Not (And (in B a) (∀ (C D : Iota), Ne B (ordered_pair C D))))) True % 117.77/117.99 Clause #232 (by clausification #[231]): ∀ (a : Iota), % 117.77/117.99 Or (Eq (relation a) True) (Eq (∀ (B : Iota), Not (And (in B a) (∀ (C D : Iota), Ne B (ordered_pair C D)))) False) % 117.77/117.99 Clause #234 (by clausification #[232]): ∀ (a a_1 : Iota), % 117.77/117.99 Or (Eq (relation a) True) % 117.77/117.99 (Eq (Not (Not (And (in (skS.0 13 a a_1) a) (∀ (C D : Iota), Ne (skS.0 13 a a_1) (ordered_pair C D))))) True) % 117.77/117.99 Clause #235 (by clausification #[234]): ∀ (a a_1 : Iota), % 117.77/117.99 Or (Eq (relation a) True) % 117.77/117.99 (Eq (Not (And (in (skS.0 13 a a_1) a) (∀ (C D : Iota), Ne (skS.0 13 a a_1) (ordered_pair C D)))) False) % 117.77/117.99 Clause #236 (by clausification #[235]): ∀ (a a_1 : Iota), % 117.77/117.99 Or (Eq (relation a) True) % 117.77/117.99 (Eq (And (in (skS.0 13 a a_1) a) (∀ (C D : Iota), Ne (skS.0 13 a a_1) (ordered_pair C D))) True) % 117.77/117.99 Clause #237 (by clausification #[236]): ∀ (a a_1 : Iota), Or (Eq (relation a) True) (Eq (∀ (C D : Iota), Ne (skS.0 13 a a_1) (ordered_pair C D)) True) % 117.77/117.99 Clause #238 (by clausification #[236]): ∀ (a a_1 : Iota), Or (Eq (relation a) True) (Eq (in (skS.0 13 a a_1) a) True) % 117.77/117.99 Clause #239 (by clausification #[237]): ∀ (a a_1 a_2 : Iota), Or (Eq (relation a) True) (Eq (∀ (D : Iota), Ne (skS.0 13 a a_1) (ordered_pair a_2 D)) True) % 117.77/117.99 Clause #240 (by clausification #[239]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (relation a) True) (Eq (Ne (skS.0 13 a a_1) (ordered_pair a_2 a_3)) True) % 117.81/118.02 Clause #241 (by clausification #[240]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (relation a) True) (Ne (skS.0 13 a a_1) (ordered_pair a_2 a_3)) % 117.81/118.02 Clause #269 (by clausification #[95]): ∀ (a : Iota), Or (Eq (relation (skS.0 4 a)) False) (Eq (function (skS.0 4 a)) False) % 117.81/118.02 Clause #281 (by clausification #[97]): ∀ (a a_1 : Iota), Eq (Not (And (in a (skS.0 4 a_1)) (∀ (C D : Iota), Ne (ordered_pair C D) a))) True % 117.81/118.02 Clause #282 (by clausification #[281]): ∀ (a a_1 : Iota), Eq (And (in a (skS.0 4 a_1)) (∀ (C D : Iota), Ne (ordered_pair C D) a)) False % 117.81/118.02 Clause #283 (by clausification #[282]): ∀ (a a_1 : Iota), Or (Eq (in a (skS.0 4 a_1)) False) (Eq (∀ (C D : Iota), Ne (ordered_pair C D) a) False) % 117.81/118.02 Clause #284 (by clausification #[283]): ∀ (a a_1 a_2 : Iota), % 117.81/118.02 Or (Eq (in a (skS.0 4 a_1)) False) (Eq (Not (∀ (D : Iota), Ne (ordered_pair (skS.0 14 a a_2) D) a)) True) % 117.81/118.02 Clause #285 (by clausification #[284]): ∀ (a a_1 a_2 : Iota), % 117.81/118.02 Or (Eq (in a (skS.0 4 a_1)) False) (Eq (∀ (D : Iota), Ne (ordered_pair (skS.0 14 a a_2) D) a) False) % 117.81/118.02 Clause #286 (by clausification #[285]): ∀ (a a_1 a_2 a_3 : Iota), % 117.81/118.02 Or (Eq (in a (skS.0 4 a_1)) False) (Eq (Not (Ne (ordered_pair (skS.0 14 a a_2) (skS.0 15 a a_2 a_3)) a)) True) % 117.81/118.02 Clause #287 (by clausification #[286]): ∀ (a a_1 a_2 a_3 : Iota), % 117.81/118.02 Or (Eq (in a (skS.0 4 a_1)) False) (Eq (Ne (ordered_pair (skS.0 14 a a_2) (skS.0 15 a a_2 a_3)) a) False) % 117.81/118.02 Clause #288 (by clausification #[287]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (in a (skS.0 4 a_1)) False) (Eq (ordered_pair (skS.0 14 a a_2) (skS.0 15 a a_2 a_3)) a) % 117.81/118.02 Clause #325 (by superposition #[238, 288]): ∀ (a a_1 a_2 a_3 : Iota), % 117.81/118.02 Or % 117.81/118.02 (Eq (ordered_pair (skS.0 14 (skS.0 13 (skS.0 4 a) a_1) a_2) (skS.0 15 (skS.0 13 (skS.0 4 a) a_1) a_2 a_3)) % 117.81/118.02 (skS.0 13 (skS.0 4 a) a_1)) % 117.81/118.02 (Or (Eq (relation (skS.0 4 a)) True) (Eq False True)) % 117.81/118.02 Clause #363 (by clausification #[212]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (function a) True) (Ne (skS.0 11 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3)) % 117.81/118.02 Clause #389 (by clausification #[215]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 117.81/118.02 Or (Eq (function (skS.0 4 a)) True) % 117.81/118.02 (Or (Eq (in (ordered_pair (skS.0 10 (skS.0 4 a) a_1) a_2) (skS.0 4 a)) False) % 117.81/118.02 (Eq (skS.0 12 (skS.0 4 a) a_1 a_3 a_4) a_2)) % 117.81/118.02 Clause #391 (by superposition #[389, 214]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 117.81/118.02 Or (Eq (function (skS.0 4 a)) True) % 117.81/118.02 (Or (Eq (skS.0 12 (skS.0 4 a) a_1 a_2 a_3) (skS.0 11 (skS.0 4 a) a_1 a_4)) % 117.81/118.02 (Or (Eq (function (skS.0 4 a)) True) (Eq False True))) % 117.81/118.02 Clause #1075 (by clausification #[325]): ∀ (a a_1 a_2 a_3 : Iota), % 117.81/118.02 Or % 117.81/118.02 (Eq (ordered_pair (skS.0 14 (skS.0 13 (skS.0 4 a) a_1) a_2) (skS.0 15 (skS.0 13 (skS.0 4 a) a_1) a_2 a_3)) % 117.81/118.02 (skS.0 13 (skS.0 4 a) a_1)) % 117.81/118.02 (Eq (relation (skS.0 4 a)) True) % 117.81/118.02 Clause #1076 (by forward contextual literal cutting #[1075, 241]): ∀ (a : Iota), Eq (relation (skS.0 4 a)) True % 117.81/118.02 Clause #1077 (by backward demodulation #[1076, 269]): ∀ (a : Iota), Or (Eq True False) (Eq (function (skS.0 4 a)) False) % 117.81/118.02 Clause #1079 (by clausification #[1077]): ∀ (a : Iota), Eq (function (skS.0 4 a)) False % 117.81/118.02 Clause #2099 (by clausification #[391]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 117.81/118.02 Or (Eq (function (skS.0 4 a)) True) % 117.81/118.02 (Or (Eq (skS.0 12 (skS.0 4 a) a_1 a_2 a_3) (skS.0 11 (skS.0 4 a) a_1 a_4)) (Eq (function (skS.0 4 a)) True)) % 117.81/118.02 Clause #2100 (by eliminate duplicate literals #[2099]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 117.81/118.02 Or (Eq (function (skS.0 4 a)) True) (Eq (skS.0 12 (skS.0 4 a) a_1 a_2 a_3) (skS.0 11 (skS.0 4 a) a_1 a_4)) % 117.81/118.02 Clause #2101 (by forward demodulation #[2100, 1079]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq False True) (Eq (skS.0 12 (skS.0 4 a) a_1 a_2 a_3) (skS.0 11 (skS.0 4 a) a_1 a_4)) % 117.81/118.02 Clause #2102 (by clausification #[2101]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (skS.0 12 (skS.0 4 a) a_1 a_2 a_3) (skS.0 11 (skS.0 4 a) a_1 a_4) % 117.81/118.02 Clause #2104 (by superposition #[2102, 363]): ∀ (a a_1 a_2 a_3 : Iota), % 117.81/118.02 Or (Eq (function (skS.0 4 a)) True) (Ne (skS.0 11 (skS.0 4 a) a_1 a_2) (skS.0 11 (skS.0 4 a) a_1 a_3)) % 117.81/118.02 Clause #2108 (by superposition #[2102, 2102]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 11 (skS.0 4 a) a_1 a_2) (skS.0 11 (skS.0 4 a) a_1 a_3) % 117.96/118.20 Clause #15045 (by forward demodulation #[2104, 1079]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq False True) (Ne (skS.0 11 (skS.0 4 a) a_1 a_2) (skS.0 11 (skS.0 4 a) a_1 a_3)) % 117.96/118.20 Clause #15046 (by clausification #[15045]): ∀ (a a_1 a_2 a_3 : Iota), Ne (skS.0 11 (skS.0 4 a) a_1 a_2) (skS.0 11 (skS.0 4 a) a_1 a_3) % 117.96/118.20 Clause #15047 (by forward contextual literal cutting #[15046, 2108]): False % 117.96/118.20 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------