%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET600+3 : TPTP v9.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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:13 PM UTC 2025 % Result : Theorem 189.28s 189.50s % Output : Proof 189.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.08 % Problem : SET600+3 : TPTP v9.2.0. Released v2.2.0. % 0.06/0.09 % Command : duper %s % 0.08/0.29 % Computer : n021.cluster.edu % 0.08/0.29 % Model : x86_64 x86_64 % 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.29 % Memory : 8042.1875MB % 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.29 % CPULimit : 300 % 0.08/0.29 % WCLimit : 300 % 0.08/0.29 % DateTime : Thu Oct 2 14:19:08 EDT 2025 % 0.08/0.29 % CPUTime : % 189.28/189.50 SZS status Theorem for theBenchmark.p % 189.28/189.50 SZS output start Proof for theBenchmark.p % 189.28/189.50 Clause #0 (by assumption #[]): Eq (∀ (B C D : Iota), Iff (member D (union B C)) (Or (member D B) (member D C))) True % 189.28/189.50 Clause #1 (by assumption #[]): Eq (∀ (B : Iota), Not (member B empty_set)) True % 189.28/189.50 Clause #2 (by assumption #[]): Eq (∀ (B C : Iota), Iff (Eq B C) (And (subset B C) (subset C B))) True % 189.28/189.50 Clause #3 (by assumption #[]): Eq (∀ (B C : Iota), Eq (union B C) (union C B)) True % 189.28/189.50 Clause #4 (by assumption #[]): Eq (∀ (B C : Iota), Iff (subset B C) (∀ (D : Iota), member D B → member D C)) True % 189.28/189.50 Clause #6 (by assumption #[]): Eq (∀ (B : Iota), Iff (empty B) (∀ (C : Iota), Not (member C B))) True % 189.28/189.50 Clause #7 (by assumption #[]): Eq (∀ (B C : Iota), Iff (Eq B C) (∀ (D : Iota), Iff (member D B) (member D C))) True % 189.28/189.50 Clause #8 (by assumption #[]): Eq (Not (∀ (B C : Iota), Iff (Eq (union B C) empty_set) (And (Eq B empty_set) (Eq C empty_set)))) True % 189.28/189.50 Clause #10 (by clausification #[1]): ∀ (a : Iota), Eq (Not (member a empty_set)) True % 189.28/189.50 Clause #11 (by clausification #[10]): ∀ (a : Iota), Eq (member a empty_set) False % 189.28/189.50 Clause #12 (by clausification #[6]): ∀ (a : Iota), Eq (Iff (empty a) (∀ (C : Iota), Not (member C a))) True % 189.28/189.50 Clause #13 (by clausification #[12]): ∀ (a : Iota), Or (Eq (empty a) True) (Eq (∀ (C : Iota), Not (member C a)) False) % 189.28/189.50 Clause #14 (by clausification #[12]): ∀ (a : Iota), Or (Eq (empty a) False) (Eq (∀ (C : Iota), Not (member C a)) True) % 189.28/189.50 Clause #15 (by clausification #[13]): ∀ (a a_1 : Iota), Or (Eq (empty a) True) (Eq (Not (Not (member (skS.0 0 a a_1) a))) True) % 189.28/189.50 Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota), Or (Eq (empty a) True) (Eq (Not (member (skS.0 0 a a_1) a)) False) % 189.28/189.50 Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota), Or (Eq (empty a) True) (Eq (member (skS.0 0 a a_1) a) True) % 189.28/189.50 Clause #20 (by clausification #[14]): ∀ (a a_1 : Iota), Or (Eq (empty a) False) (Eq (Not (member a_1 a)) True) % 189.28/189.50 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), Or (Eq (empty a) False) (Eq (member a_1 a) False) % 189.28/189.51 Clause #23 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (C D : Iota), Iff (member D (union a C)) (Or (member D a) (member D C))) True % 189.28/189.51 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), Eq (∀ (D : Iota), Iff (member D (union a a_1)) (Or (member D a) (member D a_1))) True % 189.28/189.51 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), Eq (Iff (member a (union a_1 a_2)) (Or (member a a_1) (member a a_2))) True % 189.28/189.51 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), Or (Eq (member a (union a_1 a_2)) True) (Eq (Or (member a a_1) (member a a_2)) False) % 189.28/189.51 Clause #27 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), Or (Eq (member a (union a_1 a_2)) False) (Eq (Or (member a a_1) (member a a_2)) True) % 189.28/189.51 Clause #28 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), Or (Eq (member a (union a_1 a_2)) True) (Eq (member a a_2) False) % 189.28/189.51 Clause #32 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (C : Iota), Eq (union a C) (union C a)) True % 189.28/189.51 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), Eq (Eq (union a a_1) (union a_1 a)) True % 189.28/189.51 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), Eq (union a a_1) (union a_1 a) % 189.28/189.51 Clause #35 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (C : Iota), Iff (subset a C) (∀ (D : Iota), member D a → member D C)) True % 189.28/189.51 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), Eq (Iff (subset a a_1) (∀ (D : Iota), member D a → member D a_1)) True % 189.28/189.51 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), Or (Eq (subset a a_1) True) (Eq (∀ (D : Iota), member D a → member D a_1) False) % 189.28/189.51 Clause #39 (by clausification #[37]): ∀ (a a_1 a_2 : Iota), % 189.28/189.51 Or (Eq (subset a a_1) True) (Eq (Not (member (skS.0 1 a a_1 a_2) a → member (skS.0 1 a a_1 a_2) a_1)) True) % 189.28/189.51 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 189.28/189.51 Or (Eq (subset a a_1) True) (Eq (member (skS.0 1 a a_1 a_2) a → member (skS.0 1 a a_1 a_2) a_1) False) % 189.28/189.51 Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) True) (Eq (member (skS.0 1 a a_1 a_2) a) True) % 189.30/189.53 Clause #42 (by clausification #[40]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) True) (Eq (member (skS.0 1 a a_1 a_2) a_1) False) % 189.30/189.53 Clause #43 (by superposition #[41, 11]): ∀ (a : Iota), Or (Eq (subset empty_set a) True) (Eq True False) % 189.30/189.53 Clause #44 (by superposition #[41, 28]): ∀ (a a_1 a_2 a_3 : Iota), % 189.30/189.53 Or (Eq (subset a a_1) True) (Or (Eq (member (skS.0 1 a a_1 a_2) (union a_3 a)) True) (Eq True False)) % 189.30/189.53 Clause #46 (by clausification #[43]): ∀ (a : Iota), Eq (subset empty_set a) True % 189.30/189.53 Clause #47 (by clausification #[2]): ∀ (a : Iota), Eq (∀ (C : Iota), Iff (Eq a C) (And (subset a C) (subset C a))) True % 189.30/189.53 Clause #48 (by clausification #[47]): ∀ (a a_1 : Iota), Eq (Iff (Eq a a_1) (And (subset a a_1) (subset a_1 a))) True % 189.30/189.53 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), Or (Eq (Eq a a_1) True) (Eq (And (subset a a_1) (subset a_1 a)) False) % 189.30/189.53 Clause #51 (by clausification #[49]): ∀ (a a_1 : Iota), Or (Eq (And (subset a a_1) (subset a_1 a)) False) (Eq a a_1) % 189.30/189.53 Clause #52 (by clausification #[51]): ∀ (a a_1 : Iota), Or (Eq a a_1) (Or (Eq (subset a a_1) False) (Eq (subset a_1 a) False)) % 189.30/189.53 Clause #53 (by superposition #[52, 46]): ∀ (a : Iota), Or (Eq empty_set a) (Or (Eq (subset a empty_set) False) (Eq False True)) % 189.30/189.53 Clause #56 (by clausification #[53]): ∀ (a : Iota), Or (Eq empty_set a) (Eq (subset a empty_set) False) % 189.30/189.53 Clause #64 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (C : Iota), Iff (Eq a C) (∀ (D : Iota), Iff (member D a) (member D C))) True % 189.30/189.53 Clause #65 (by clausification #[64]): ∀ (a a_1 : Iota), Eq (Iff (Eq a a_1) (∀ (D : Iota), Iff (member D a) (member D a_1))) True % 189.30/189.53 Clause #66 (by clausification #[65]): ∀ (a a_1 : Iota), Or (Eq (Eq a a_1) True) (Eq (∀ (D : Iota), Iff (member D a) (member D a_1)) False) % 189.30/189.53 Clause #68 (by clausification #[66]): ∀ (a a_1 : Iota), Or (Eq (∀ (D : Iota), Iff (member D a) (member D a_1)) False) (Eq a a_1) % 189.30/189.53 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 : Iota), % 189.30/189.53 Or (Eq a a_1) (Eq (Not (Iff (member (skS.0 2 a a_1 a_2) a) (member (skS.0 2 a a_1 a_2) a_1))) True) % 189.30/189.53 Clause #70 (by clausification #[69]): ∀ (a a_1 a_2 : Iota), Or (Eq a a_1) (Eq (Iff (member (skS.0 2 a a_1 a_2) a) (member (skS.0 2 a a_1 a_2) a_1)) False) % 189.30/189.53 Clause #72 (by clausification #[70]): ∀ (a a_1 a_2 : Iota), % 189.30/189.53 Or (Eq a a_1) (Or (Eq (member (skS.0 2 a a_1 a_2) a) True) (Eq (member (skS.0 2 a a_1 a_2) a_1) True)) % 189.30/189.53 Clause #82 (by clausification #[8]): Eq (∀ (B C : Iota), Iff (Eq (union B C) empty_set) (And (Eq B empty_set) (Eq C empty_set))) False % 189.30/189.53 Clause #83 (by clausification #[82]): ∀ (a : Iota), % 189.30/189.53 Eq (Not (∀ (C : Iota), Iff (Eq (union (skS.0 3 a) C) empty_set) (And (Eq (skS.0 3 a) empty_set) (Eq C empty_set)))) % 189.30/189.53 True % 189.30/189.53 Clause #84 (by clausification #[83]): ∀ (a : Iota), % 189.30/189.53 Eq (∀ (C : Iota), Iff (Eq (union (skS.0 3 a) C) empty_set) (And (Eq (skS.0 3 a) empty_set) (Eq C empty_set))) False % 189.30/189.53 Clause #85 (by clausification #[84]): ∀ (a a_1 : Iota), % 189.30/189.53 Eq % 189.30/189.53 (Not % 189.30/189.53 (Iff (Eq (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) % 189.30/189.53 (And (Eq (skS.0 3 a) empty_set) (Eq (skS.0 4 a a_1) empty_set)))) % 189.30/189.53 True % 189.30/189.53 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), % 189.30/189.53 Eq % 189.30/189.53 (Iff (Eq (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) % 189.30/189.53 (And (Eq (skS.0 3 a) empty_set) (Eq (skS.0 4 a a_1) empty_set))) % 189.30/189.53 False % 189.30/189.53 Clause #87 (by clausification #[86]): ∀ (a a_1 : Iota), % 189.30/189.53 Or (Eq (Eq (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) False) % 189.30/189.53 (Eq (And (Eq (skS.0 3 a) empty_set) (Eq (skS.0 4 a a_1) empty_set)) False) % 189.30/189.53 Clause #88 (by clausification #[86]): ∀ (a a_1 : Iota), % 189.30/189.53 Or (Eq (Eq (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) True) % 189.30/189.53 (Eq (And (Eq (skS.0 3 a) empty_set) (Eq (skS.0 4 a a_1) empty_set)) True) % 189.30/189.53 Clause #89 (by clausification #[87]): ∀ (a a_1 : Iota), % 189.30/189.53 Or (Eq (And (Eq (skS.0 3 a) empty_set) (Eq (skS.0 4 a a_1) empty_set)) False) % 189.30/189.53 (Ne (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) % 189.30/189.53 Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota), % 189.30/189.53 Or (Ne (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) % 189.30/189.53 (Or (Eq (Eq (skS.0 3 a) empty_set) False) (Eq (Eq (skS.0 4 a a_1) empty_set) False)) % 189.30/189.56 Clause #91 (by clausification #[90]): ∀ (a a_1 : Iota), % 189.30/189.56 Or (Ne (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) % 189.30/189.56 (Or (Eq (Eq (skS.0 4 a a_1) empty_set) False) (Ne (skS.0 3 a) empty_set)) % 189.30/189.56 Clause #92 (by clausification #[91]): ∀ (a a_1 : Iota), % 189.30/189.56 Or (Ne (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) (Or (Ne (skS.0 3 a) empty_set) (Ne (skS.0 4 a a_1) empty_set)) % 189.30/189.56 Clause #93 (by clausification #[27]): ∀ (a a_1 a_2 : Iota), Or (Eq (member a (union a_1 a_2)) False) (Or (Eq (member a a_1) True) (Eq (member a a_2) True)) % 189.30/189.56 Clause #94 (by superposition #[93, 17]): ∀ (a a_1 a_2 : Iota), % 189.30/189.56 Or (Eq (member (skS.0 0 (union a a_1) a_2) a) True) % 189.30/189.56 (Or (Eq (member (skS.0 0 (union a a_1) a_2) a_1) True) (Or (Eq (empty (union a a_1)) True) (Eq False True))) % 189.30/189.56 Clause #119 (by clausification #[44]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (subset a a_1) True) (Eq (member (skS.0 1 a a_1 a_2) (union a_3 a)) True) % 189.30/189.56 Clause #120 (by superposition #[119, 42]): ∀ (a a_1 : Iota), Or (Eq (subset a (union a_1 a)) True) (Or (Eq (subset a (union a_1 a)) True) (Eq True False)) % 189.30/189.56 Clause #124 (by clausification #[120]): ∀ (a a_1 : Iota), Or (Eq (subset a (union a_1 a)) True) (Eq (subset a (union a_1 a)) True) % 189.30/189.56 Clause #125 (by eliminate duplicate literals #[124]): ∀ (a a_1 : Iota), Eq (subset a (union a_1 a)) True % 189.30/189.56 Clause #128 (by superposition #[125, 34]): ∀ (a a_1 : Iota), Eq (subset a (union a a_1)) True % 189.30/189.56 Clause #181 (by superposition #[72, 92]): ∀ (a a_1 a_2 a_3 : Iota), % 189.30/189.56 Or (Eq (member (skS.0 2 a (skS.0 3 a_1) a_2) a) True) % 189.30/189.56 (Or (Eq (member (skS.0 2 a (skS.0 3 a_1) a_2) (skS.0 3 a_1)) True) % 189.30/189.56 (Or (Ne (union a (skS.0 4 a_1 a_3)) empty_set) (Or (Ne a empty_set) (Ne (skS.0 4 a_1 a_3) empty_set)))) % 189.30/189.56 Clause #215 (by superposition #[72, 11]): ∀ (a a_1 : Iota), Or (Eq empty_set a) (Or (Eq (member (skS.0 2 empty_set a a_1) a) True) (Eq True False)) % 189.30/189.56 Clause #259 (by clausification #[88]): ∀ (a a_1 : Iota), % 189.30/189.56 Or (Eq (And (Eq (skS.0 3 a) empty_set) (Eq (skS.0 4 a a_1) empty_set)) True) % 189.30/189.56 (Eq (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) % 189.30/189.56 Clause #260 (by clausification #[259]): ∀ (a a_1 : Iota), Or (Eq (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) (Eq (Eq (skS.0 4 a a_1) empty_set) True) % 189.30/189.56 Clause #261 (by clausification #[259]): ∀ (a a_1 : Iota), Or (Eq (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) (Eq (Eq (skS.0 3 a) empty_set) True) % 189.30/189.56 Clause #262 (by clausification #[260]): ∀ (a a_1 : Iota), Or (Eq (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) (Eq (skS.0 4 a a_1) empty_set) % 189.30/189.56 Clause #271 (by superposition #[262, 125]): ∀ (a a_1 : Iota), Or (Eq (skS.0 4 a a_1) empty_set) (Eq (subset (skS.0 4 a a_1) empty_set) True) % 189.30/189.56 Clause #296 (by clausification #[215]): ∀ (a a_1 : Iota), Or (Eq empty_set a) (Eq (member (skS.0 2 empty_set a a_1) a) True) % 189.30/189.56 Clause #338 (by clausification #[94]): ∀ (a a_1 a_2 : Iota), % 189.30/189.56 Or (Eq (member (skS.0 0 (union a a_1) a_2) a) True) % 189.30/189.56 (Or (Eq (member (skS.0 0 (union a a_1) a_2) a_1) True) (Eq (empty (union a a_1)) True)) % 189.30/189.56 Clause #355 (by equality factoring #[338]): ∀ (a a_1 : Iota), Or (Eq (empty (union a a)) True) (Or (Ne True True) (Eq (member (skS.0 0 (union a a) a_1) a) True)) % 189.30/189.56 Clause #858 (by clausification #[355]): ∀ (a a_1 : Iota), % 189.30/189.56 Or (Eq (empty (union a a)) True) % 189.30/189.56 (Or (Eq (member (skS.0 0 (union a a) a_1) a) True) (Or (Eq True False) (Eq True False))) % 189.30/189.56 Clause #860 (by clausification #[858]): ∀ (a a_1 : Iota), Or (Eq (empty (union a a)) True) (Or (Eq (member (skS.0 0 (union a a) a_1) a) True) (Eq True False)) % 189.30/189.56 Clause #861 (by clausification #[860]): ∀ (a a_1 : Iota), Or (Eq (empty (union a a)) True) (Eq (member (skS.0 0 (union a a) a_1) a) True) % 189.30/189.56 Clause #862 (by superposition #[861, 11]): Or (Eq (empty (union empty_set empty_set)) True) (Eq True False) % 189.30/189.56 Clause #875 (by clausification #[862]): Eq (empty (union empty_set empty_set)) True % 189.30/189.56 Clause #876 (by superposition #[875, 21]): ∀ (a : Iota), Or (Eq True False) (Eq (member a (union empty_set empty_set)) False) % 189.30/189.56 Clause #887 (by clausification #[876]): ∀ (a : Iota), Eq (member a (union empty_set empty_set)) False % 189.30/189.56 Clause #898 (by superposition #[887, 296]): Or (Eq empty_set (union empty_set empty_set)) (Eq False True) % 189.60/189.91 Clause #927 (by clausification #[898]): Eq empty_set (union empty_set empty_set) % 189.60/189.91 Clause #2265 (by superposition #[271, 56]): ∀ (a a_1 : Iota), Or (Eq (skS.0 4 a a_1) empty_set) (Or (Eq empty_set (skS.0 4 a a_1)) (Eq True False)) % 189.60/189.91 Clause #2280 (by clausification #[2265]): ∀ (a a_1 : Iota), Or (Eq (skS.0 4 a a_1) empty_set) (Eq empty_set (skS.0 4 a a_1)) % 189.60/189.91 Clause #2281 (by eliminate duplicate literals #[2280]): ∀ (a a_1 : Iota), Eq (skS.0 4 a a_1) empty_set % 189.60/189.91 Clause #8393 (by destructive equality resolution #[181]): ∀ (a a_1 a_2 : Iota), % 189.60/189.91 Or (Eq (member (skS.0 2 empty_set (skS.0 3 a) a_1) empty_set) True) % 189.60/189.91 (Or (Eq (member (skS.0 2 empty_set (skS.0 3 a) a_1) (skS.0 3 a)) True) % 189.60/189.91 (Or (Ne (union empty_set (skS.0 4 a a_2)) empty_set) (Ne (skS.0 4 a a_2) empty_set))) % 189.60/189.91 Clause #8394 (by forward demodulation #[8393, 11]): ∀ (a a_1 a_2 : Iota), % 189.60/189.91 Or (Eq False True) % 189.60/189.91 (Or (Eq (member (skS.0 2 empty_set (skS.0 3 a) a_1) (skS.0 3 a)) True) % 189.60/189.91 (Or (Ne (union empty_set (skS.0 4 a a_2)) empty_set) (Ne (skS.0 4 a a_2) empty_set))) % 189.60/189.91 Clause #8395 (by clausification #[8394]): ∀ (a a_1 a_2 : Iota), % 189.60/189.91 Or (Eq (member (skS.0 2 empty_set (skS.0 3 a) a_1) (skS.0 3 a)) True) % 189.60/189.91 (Or (Ne (union empty_set (skS.0 4 a a_2)) empty_set) (Ne (skS.0 4 a a_2) empty_set)) % 189.60/189.91 Clause #8396 (by forward demodulation #[8395, 2281]): ∀ (a a_1 a_2 : Iota), % 189.60/189.91 Or (Eq (member (skS.0 2 empty_set (skS.0 3 a) a_1) (skS.0 3 a)) True) % 189.60/189.91 (Or (Ne (union empty_set empty_set) empty_set) (Ne (skS.0 4 a a_2) empty_set)) % 189.60/189.91 Clause #8397 (by forward demodulation #[8396, 927]): ∀ (a a_1 a_2 : Iota), % 189.60/189.91 Or (Eq (member (skS.0 2 empty_set (skS.0 3 a) a_1) (skS.0 3 a)) True) % 189.60/189.91 (Or (Ne empty_set empty_set) (Ne (skS.0 4 a a_2) empty_set)) % 189.60/189.91 Clause #8398 (by eliminate resolved literals #[8397]): ∀ (a a_1 a_2 : Iota), % 189.60/189.91 Or (Eq (member (skS.0 2 empty_set (skS.0 3 a) a_1) (skS.0 3 a)) True) (Ne (skS.0 4 a a_2) empty_set) % 189.60/189.91 Clause #8399 (by forward demodulation #[8398, 2281]): ∀ (a a_1 : Iota), Or (Eq (member (skS.0 2 empty_set (skS.0 3 a) a_1) (skS.0 3 a)) True) (Ne empty_set empty_set) % 189.60/189.91 Clause #8400 (by eliminate resolved literals #[8399]): ∀ (a a_1 : Iota), Eq (member (skS.0 2 empty_set (skS.0 3 a) a_1) (skS.0 3 a)) True % 189.60/189.91 Clause #31088 (by clausification #[261]): ∀ (a a_1 : Iota), Or (Eq (union (skS.0 3 a) (skS.0 4 a a_1)) empty_set) (Eq (skS.0 3 a) empty_set) % 189.60/189.91 Clause #31089 (by forward demodulation #[31088, 2281]): ∀ (a : Iota), Or (Eq (union (skS.0 3 a) empty_set) empty_set) (Eq (skS.0 3 a) empty_set) % 189.60/189.91 Clause #31103 (by superposition #[31089, 128]): ∀ (a : Iota), Or (Eq (skS.0 3 a) empty_set) (Eq (subset (skS.0 3 a) empty_set) True) % 189.60/189.91 Clause #31385 (by superposition #[31103, 56]): ∀ (a : Iota), Or (Eq (skS.0 3 a) empty_set) (Or (Eq empty_set (skS.0 3 a)) (Eq True False)) % 189.60/189.91 Clause #31459 (by clausification #[31385]): ∀ (a : Iota), Or (Eq (skS.0 3 a) empty_set) (Eq empty_set (skS.0 3 a)) % 189.60/189.91 Clause #31460 (by eliminate duplicate literals #[31459]): ∀ (a : Iota), Eq (skS.0 3 a) empty_set % 189.60/189.91 Clause #31461 (by backward demodulation #[31460, 8400]): ∀ (a a_1 : Iota), Eq (member (skS.0 2 empty_set (skS.0 3 a) a_1) empty_set) True % 189.60/189.91 Clause #31472 (by forward demodulation #[31461, 31460]): ∀ (a : Iota), Eq (member (skS.0 2 empty_set empty_set a) empty_set) True % 189.60/189.91 Clause #31473 (by superposition #[31472, 11]): Eq True False % 189.60/189.91 Clause #31558 (by clausification #[31473]): False % 189.60/189.91 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------