%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU267+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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:16 PM UTC 2025 % Result : Theorem 3.72s 3.91s % Output : Proof 3.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SEU267+1 : TPTP v9.2.0. Released v3.3.0. % 0.12/0.14 % Command : duper %s % 0.14/0.35 % Computer : n007.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 04:25:23 EDT 2025 % 0.14/0.35 % CPUTime : % 3.72/3.91 SZS status Theorem for theBenchmark.p % 3.72/3.91 SZS output start Proof for theBenchmark.p % 3.72/3.91 Clause #12 (by assumption #[]): Eq (Not (∀ (A B : Iota), And (Eq (pair_first (ordered_pair A B)) A) (Eq (pair_second (ordered_pair A B)) B))) True % 3.72/3.91 Clause #13 (by assumption #[]): Eq % 3.72/3.91 (∀ (A : Iota), % 3.72/3.91 (Exists fun B => Exists fun C => Eq A (ordered_pair B C)) → % 3.72/3.91 ∀ (B : Iota), Iff (Eq B (pair_first A)) (∀ (C D : Iota), Eq A (ordered_pair C D) → Eq B C)) % 3.72/3.91 True % 3.72/3.91 Clause #14 (by assumption #[]): Eq % 3.72/3.91 (∀ (A : Iota), % 3.72/3.91 (Exists fun B => Exists fun C => Eq A (ordered_pair B C)) → % 3.72/3.91 ∀ (B : Iota), Iff (Eq B (pair_second A)) (∀ (C D : Iota), Eq A (ordered_pair C D) → Eq B D)) % 3.72/3.91 True % 3.72/3.91 Clause #59 (by clausification #[12]): Eq (∀ (A B : Iota), And (Eq (pair_first (ordered_pair A B)) A) (Eq (pair_second (ordered_pair A B)) B)) False % 3.72/3.91 Clause #60 (by clausification #[59]): ∀ (a : Iota), % 3.72/3.91 Eq % 3.72/3.91 (Not % 3.72/3.91 (∀ (B : Iota), % 3.72/3.91 And (Eq (pair_first (ordered_pair (skS.0 3 a) B)) (skS.0 3 a)) % 3.72/3.91 (Eq (pair_second (ordered_pair (skS.0 3 a) B)) B))) % 3.72/3.91 True % 3.72/3.91 Clause #61 (by clausification #[60]): ∀ (a : Iota), % 3.72/3.91 Eq % 3.72/3.91 (∀ (B : Iota), % 3.72/3.91 And (Eq (pair_first (ordered_pair (skS.0 3 a) B)) (skS.0 3 a)) (Eq (pair_second (ordered_pair (skS.0 3 a) B)) B)) % 3.72/3.91 False % 3.72/3.91 Clause #62 (by clausification #[61]): ∀ (a a_1 : Iota), % 3.72/3.91 Eq % 3.72/3.91 (Not % 3.72/3.91 (And (Eq (pair_first (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 3 a)) % 3.72/3.91 (Eq (pair_second (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 4 a a_1)))) % 3.72/3.91 True % 3.72/3.91 Clause #63 (by clausification #[62]): ∀ (a a_1 : Iota), % 3.72/3.91 Eq % 3.72/3.91 (And (Eq (pair_first (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 3 a)) % 3.72/3.91 (Eq (pair_second (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 4 a a_1))) % 3.72/3.91 False % 3.72/3.91 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), % 3.72/3.91 Or (Eq (Eq (pair_first (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 3 a)) False) % 3.72/3.91 (Eq (Eq (pair_second (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 4 a a_1)) False) % 3.72/3.91 Clause #65 (by clausification #[64]): ∀ (a a_1 : Iota), % 3.72/3.91 Or (Eq (Eq (pair_second (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 4 a a_1)) False) % 3.72/3.91 (Ne (pair_first (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 3 a)) % 3.72/3.91 Clause #66 (by clausification #[65]): ∀ (a a_1 : Iota), % 3.72/3.91 Or (Ne (pair_first (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 3 a)) % 3.72/3.91 (Ne (pair_second (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 4 a a_1)) % 3.72/3.91 Clause #69 (by clausification #[14]): ∀ (a : Iota), % 3.72/3.91 Eq % 3.72/3.91 ((Exists fun B => Exists fun C => Eq a (ordered_pair B C)) → % 3.72/3.91 ∀ (B : Iota), Iff (Eq B (pair_second a)) (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq B D)) % 3.72/3.91 True % 3.72/3.91 Clause #70 (by clausification #[69]): ∀ (a : Iota), % 3.72/3.91 Or (Eq (Exists fun B => Exists fun C => Eq a (ordered_pair B C)) False) % 3.72/3.91 (Eq (∀ (B : Iota), Iff (Eq B (pair_second a)) (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq B D)) True) % 3.72/3.91 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), % 3.72/3.91 Or (Eq (∀ (B : Iota), Iff (Eq B (pair_second a)) (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq B D)) True) % 3.72/3.91 (Eq (Exists fun C => Eq a (ordered_pair a_1 C)) False) % 3.72/3.91 Clause #72 (by clausification #[71]): ∀ (a a_1 a_2 : Iota), % 3.72/3.91 Or (Eq (Exists fun C => Eq a (ordered_pair a_1 C)) False) % 3.72/3.91 (Eq (Iff (Eq a_2 (pair_second a)) (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq a_2 D)) True) % 3.72/3.91 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 a_3 : Iota), % 3.72/3.91 Or (Eq (Iff (Eq a (pair_second a_1)) (∀ (C D : Iota), Eq a_1 (ordered_pair C D) → Eq a D)) True) % 3.72/3.91 (Eq (Eq a_1 (ordered_pair a_2 a_3)) False) % 3.72/3.91 Clause #75 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), % 3.72/3.91 Or (Eq (Eq a (ordered_pair a_1 a_2)) False) % 3.72/3.91 (Or (Eq (Eq a_3 (pair_second a)) False) (Eq (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq a_3 D) True)) % 3.72/3.91 Clause #104 (by clausification #[13]): ∀ (a : Iota), % 3.72/3.91 Eq % 3.72/3.91 ((Exists fun B => Exists fun C => Eq a (ordered_pair B C)) → % 3.72/3.91 ∀ (B : Iota), Iff (Eq B (pair_first a)) (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq B C)) % 3.72/3.91 True % 3.72/3.91 Clause #105 (by clausification #[104]): ∀ (a : Iota), % 3.72/3.93 Or (Eq (Exists fun B => Exists fun C => Eq a (ordered_pair B C)) False) % 3.72/3.93 (Eq (∀ (B : Iota), Iff (Eq B (pair_first a)) (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq B C)) True) % 3.72/3.93 Clause #106 (by clausification #[105]): ∀ (a a_1 : Iota), % 3.72/3.93 Or (Eq (∀ (B : Iota), Iff (Eq B (pair_first a)) (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq B C)) True) % 3.72/3.93 (Eq (Exists fun C => Eq a (ordered_pair a_1 C)) False) % 3.72/3.93 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 3.72/3.93 Or (Eq (Exists fun C => Eq a (ordered_pair a_1 C)) False) % 3.72/3.93 (Eq (Iff (Eq a_2 (pair_first a)) (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq a_2 C)) True) % 3.72/3.93 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 a_3 : Iota), % 3.72/3.93 Or (Eq (Iff (Eq a (pair_first a_1)) (∀ (C D : Iota), Eq a_1 (ordered_pair C D) → Eq a C)) True) % 3.72/3.93 (Eq (Eq a_1 (ordered_pair a_2 a_3)) False) % 3.72/3.93 Clause #110 (by clausification #[108]): ∀ (a a_1 a_2 a_3 : Iota), % 3.72/3.93 Or (Eq (Eq a (ordered_pair a_1 a_2)) False) % 3.72/3.93 (Or (Eq (Eq a_3 (pair_first a)) False) (Eq (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq a_3 C) True)) % 3.72/3.93 Clause #150 (by clausification #[75]): ∀ (a a_1 a_2 a_3 : Iota), % 3.72/3.93 Or (Eq (Eq a (pair_second a_1)) False) % 3.72/3.93 (Or (Eq (∀ (C D : Iota), Eq a_1 (ordered_pair C D) → Eq a D) True) (Ne a_1 (ordered_pair a_2 a_3))) % 3.72/3.93 Clause #151 (by clausification #[150]): ∀ (a a_1 a_2 a_3 : Iota), % 3.72/3.93 Or (Eq (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq a_1 D) True) % 3.72/3.93 (Or (Ne a (ordered_pair a_2 a_3)) (Ne a_1 (pair_second a))) % 3.72/3.93 Clause #152 (by clausification #[151]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.72/3.93 Or (Ne a (ordered_pair a_1 a_2)) % 3.72/3.93 (Or (Ne a_3 (pair_second a)) (Eq (∀ (D : Iota), Eq a (ordered_pair a_4 D) → Eq a_3 D) True)) % 3.72/3.93 Clause #153 (by clausification #[152]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 3.72/3.93 Or (Ne a (ordered_pair a_1 a_2)) (Or (Ne a_3 (pair_second a)) (Eq (Eq a (ordered_pair a_4 a_5) → Eq a_3 a_5) True)) % 3.72/3.93 Clause #154 (by clausification #[153]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 3.72/3.93 Or (Ne a (ordered_pair a_1 a_2)) % 3.72/3.93 (Or (Ne a_3 (pair_second a)) (Or (Eq (Eq a (ordered_pair a_4 a_5)) False) (Eq (Eq a_3 a_5) True))) % 3.72/3.93 Clause #155 (by clausification #[154]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 3.72/3.93 Or (Ne a (ordered_pair a_1 a_2)) % 3.72/3.93 (Or (Ne a_3 (pair_second a)) (Or (Eq (Eq a_3 a_4) True) (Ne a (ordered_pair a_5 a_4)))) % 3.72/3.93 Clause #156 (by clausification #[155]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 3.72/3.93 Or (Ne a (ordered_pair a_1 a_2)) (Or (Ne a_3 (pair_second a)) (Or (Ne a (ordered_pair a_4 a_5)) (Eq a_3 a_5))) % 3.72/3.93 Clause #157 (by destructive equality resolution #[156]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.72/3.93 Or (Ne a (pair_second (ordered_pair a_1 a_2))) (Or (Ne (ordered_pair a_1 a_2) (ordered_pair a_3 a_4)) (Eq a a_4)) % 3.72/3.93 Clause #158 (by destructive equality resolution #[157]): ∀ (a a_1 a_2 a_3 : Iota), % 3.72/3.93 Or (Ne (ordered_pair a a_1) (ordered_pair a_2 a_3)) (Eq (pair_second (ordered_pair a a_1)) a_3) % 3.72/3.93 Clause #159 (by equality resolution #[158]): ∀ (a a_1 : Iota), Eq (pair_second (ordered_pair a a_1)) a_1 % 3.72/3.93 Clause #171 (by backward contextual literal cutting #[159, 66]): ∀ (a a_1 : Iota), Ne (pair_first (ordered_pair (skS.0 3 a) (skS.0 4 a a_1))) (skS.0 3 a) % 3.72/3.93 Clause #193 (by clausification #[110]): ∀ (a a_1 a_2 a_3 : Iota), % 3.72/3.93 Or (Eq (Eq a (pair_first a_1)) False) % 3.72/3.93 (Or (Eq (∀ (C D : Iota), Eq a_1 (ordered_pair C D) → Eq a C) True) (Ne a_1 (ordered_pair a_2 a_3))) % 3.72/3.93 Clause #194 (by clausification #[193]): ∀ (a a_1 a_2 a_3 : Iota), % 3.72/3.93 Or (Eq (∀ (C D : Iota), Eq a (ordered_pair C D) → Eq a_1 C) True) % 3.72/3.93 (Or (Ne a (ordered_pair a_2 a_3)) (Ne a_1 (pair_first a))) % 3.72/3.93 Clause #195 (by clausification #[194]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.72/3.93 Or (Ne a (ordered_pair a_1 a_2)) % 3.72/3.93 (Or (Ne a_3 (pair_first a)) (Eq (∀ (D : Iota), Eq a (ordered_pair a_4 D) → Eq a_3 a_4) True)) % 3.72/3.93 Clause #196 (by clausification #[195]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 3.72/3.93 Or (Ne a (ordered_pair a_1 a_2)) (Or (Ne a_3 (pair_first a)) (Eq (Eq a (ordered_pair a_4 a_5) → Eq a_3 a_4) True)) % 3.72/3.93 Clause #197 (by clausification #[196]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 3.72/3.94 Or (Ne a (ordered_pair a_1 a_2)) % 3.72/3.94 (Or (Ne a_3 (pair_first a)) (Or (Eq (Eq a (ordered_pair a_4 a_5)) False) (Eq (Eq a_3 a_4) True))) % 3.72/3.94 Clause #198 (by clausification #[197]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 3.72/3.94 Or (Ne a (ordered_pair a_1 a_2)) % 3.72/3.94 (Or (Ne a_3 (pair_first a)) (Or (Eq (Eq a_3 a_4) True) (Ne a (ordered_pair a_4 a_5)))) % 3.72/3.94 Clause #199 (by clausification #[198]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 3.72/3.94 Or (Ne a (ordered_pair a_1 a_2)) (Or (Ne a_3 (pair_first a)) (Or (Ne a (ordered_pair a_4 a_5)) (Eq a_3 a_4))) % 3.72/3.94 Clause #200 (by destructive equality resolution #[199]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.72/3.94 Or (Ne a (pair_first (ordered_pair a_1 a_2))) (Or (Ne (ordered_pair a_1 a_2) (ordered_pair a_3 a_4)) (Eq a a_3)) % 3.72/3.94 Clause #201 (by destructive equality resolution #[200]): ∀ (a a_1 a_2 a_3 : Iota), Or (Ne (ordered_pair a a_1) (ordered_pair a_2 a_3)) (Eq (pair_first (ordered_pair a a_1)) a_2) % 3.72/3.94 Clause #202 (by equality resolution #[201]): ∀ (a a_1 : Iota), Eq (pair_first (ordered_pair a a_1)) a % 3.72/3.94 Clause #214 (by forward demodulation #[171, 202]): ∀ (a : Iota), Ne (skS.0 3 a) (skS.0 3 a) % 3.72/3.94 Clause #215 (by eliminate resolved literals #[214]): False % 3.72/3.94 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------