%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU730^2 : TPTP v9.2.0. Released v3.7.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:02:19 PM UTC 2025 % Result : Theorem 66.42s 66.62s % Output : Proof 66.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU730^2 : TPTP v9.2.0. Released v3.7.0. % 0.06/0.13 % Command : duper %s % 0.12/0.34 % Computer : n029.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Oct 3 04:08:38 EDT 2025 % 0.12/0.35 % CPUTime : % 66.42/66.62 SZS status Theorem for theBenchmark.p % 66.42/66.62 SZS output start Proof for theBenchmark.p % 66.42/66.62 Clause #0 (by assumption #[]): Eq (Eq complementT_lem (∀ (A X : Iota), in X (powerset A) → in (setminus A X) (powerset A))) True % 66.42/66.62 Clause #1 (by assumption #[]): Eq % 66.42/66.62 (Eq subsetTI % 66.42/66.62 (∀ (A X : Iota), % 66.42/66.62 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → (∀ (Xx : Iota), in Xx A → in Xx X → in Xx Y) → subset X Y)) % 66.42/66.62 True % 66.42/66.62 Clause #2 (by assumption #[]): Eq % 66.42/66.62 (Eq doubleComplementE1 % 66.42/66.62 (∀ (A X : Iota), in X (powerset A) → ∀ (Xx : Iota), in Xx A → in Xx (setminus A (setminus A X)) → in Xx X)) % 66.42/66.62 True % 66.42/66.62 Clause #3 (by assumption #[]): Eq % 66.42/66.62 (Not % 66.42/66.62 (complementT_lem → % 66.42/66.62 subsetTI → doubleComplementE1 → ∀ (A X : Iota), in X (powerset A) → subset (setminus A (setminus A X)) X)) % 66.42/66.62 True % 66.42/66.62 Clause #4 (by clausification #[2]): Eq doubleComplementE1 % 66.42/66.62 (∀ (A X : Iota), in X (powerset A) → ∀ (Xx : Iota), in Xx A → in Xx (setminus A (setminus A X)) → in Xx X) % 66.42/66.62 Clause #20 (by clausification #[1]): Eq subsetTI % 66.42/66.62 (∀ (A X : Iota), % 66.42/66.62 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → (∀ (Xx : Iota), in Xx A → in Xx X → in Xx Y) → subset X Y) % 66.42/66.62 Clause #24 (by clausification #[0]): Eq complementT_lem (∀ (A X : Iota), in X (powerset A) → in (setminus A X) (powerset A)) % 66.42/66.62 Clause #53 (by clausification #[3]): Eq % 66.42/66.62 (complementT_lem → % 66.42/66.62 subsetTI → doubleComplementE1 → ∀ (A X : Iota), in X (powerset A) → subset (setminus A (setminus A X)) X) % 66.42/66.62 False % 66.42/66.62 Clause #54 (by clausification #[53]): Eq complementT_lem True % 66.42/66.62 Clause #55 (by clausification #[53]): Eq (subsetTI → doubleComplementE1 → ∀ (A X : Iota), in X (powerset A) → subset (setminus A (setminus A X)) X) False % 66.42/66.62 Clause #56 (by backward demodulation #[54, 24]): Eq True (∀ (A X : Iota), in X (powerset A) → in (setminus A X) (powerset A)) % 66.42/66.62 Clause #59 (by clausification #[56]): ∀ (a : Iota), Eq (∀ (X : Iota), in X (powerset a) → in (setminus a X) (powerset a)) True % 66.42/66.62 Clause #60 (by clausification #[59]): ∀ (a a_1 : Iota), Eq (in a (powerset a_1) → in (setminus a_1 a) (powerset a_1)) True % 66.42/66.62 Clause #61 (by clausification #[60]): ∀ (a a_1 : Iota), Or (Eq (in a (powerset a_1)) False) (Eq (in (setminus a_1 a) (powerset a_1)) True) % 66.42/66.62 Clause #64 (by clausification #[55]): Eq subsetTI True % 66.42/66.62 Clause #65 (by clausification #[55]): Eq (doubleComplementE1 → ∀ (A X : Iota), in X (powerset A) → subset (setminus A (setminus A X)) X) False % 66.42/66.62 Clause #66 (by backward demodulation #[64, 20]): Eq True % 66.42/66.62 (∀ (A X : Iota), % 66.42/66.62 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → (∀ (Xx : Iota), in Xx A → in Xx X → in Xx Y) → subset X Y) % 66.42/66.62 Clause #69 (by clausification #[66]): ∀ (a : Iota), % 66.42/66.62 Eq % 66.42/66.62 (∀ (X : Iota), % 66.42/66.62 in X (powerset a) → ∀ (Y : Iota), in Y (powerset a) → (∀ (Xx : Iota), in Xx a → in Xx X → in Xx Y) → subset X Y) % 66.42/66.62 True % 66.42/66.62 Clause #70 (by clausification #[69]): ∀ (a a_1 : Iota), % 66.42/66.62 Eq % 66.42/66.62 (in a (powerset a_1) → % 66.42/66.62 ∀ (Y : Iota), in Y (powerset a_1) → (∀ (Xx : Iota), in Xx a_1 → in Xx a → in Xx Y) → subset a Y) % 66.42/66.62 True % 66.42/66.62 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), % 66.42/66.62 Or (Eq (in a (powerset a_1)) False) % 66.42/66.62 (Eq (∀ (Y : Iota), in Y (powerset a_1) → (∀ (Xx : Iota), in Xx a_1 → in Xx a → in Xx Y) → subset a Y) True) % 66.42/66.62 Clause #72 (by clausification #[71]): ∀ (a a_1 a_2 : Iota), % 66.42/66.62 Or (Eq (in a (powerset a_1)) False) % 66.42/66.62 (Eq (in a_2 (powerset a_1) → (∀ (Xx : Iota), in Xx a_1 → in Xx a → in Xx a_2) → subset a a_2) True) % 66.42/66.62 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), % 66.42/66.62 Or (Eq (in a (powerset a_1)) False) % 66.42/66.62 (Or (Eq (in a_2 (powerset a_1)) False) (Eq ((∀ (Xx : Iota), in Xx a_1 → in Xx a → in Xx a_2) → subset a a_2) True)) % 66.42/66.62 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 : Iota), % 66.42/66.62 Or (Eq (in a (powerset a_1)) False) % 66.42/66.62 (Or (Eq (in a_2 (powerset a_1)) False) % 66.42/66.62 (Or (Eq (∀ (Xx : Iota), in Xx a_1 → in Xx a → in Xx a_2) False) (Eq (subset a a_2) True))) % 66.42/66.62 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 a_3 : Iota), % 66.42/66.62 Or (Eq (in a (powerset a_1)) False) % 66.42/66.64 (Or (Eq (in a_2 (powerset a_1)) False) % 66.42/66.64 (Or (Eq (subset a a_2) True) % 66.42/66.64 (Eq (Not (in (skS.0 7 a_1 a a_2 a_3) a_1 → in (skS.0 7 a_1 a a_2 a_3) a → in (skS.0 7 a_1 a a_2 a_3) a_2)) % 66.42/66.64 True))) % 66.42/66.64 Clause #76 (by clausification #[75]): ∀ (a a_1 a_2 a_3 : Iota), % 66.42/66.64 Or (Eq (in a (powerset a_1)) False) % 66.42/66.64 (Or (Eq (in a_2 (powerset a_1)) False) % 66.42/66.64 (Or (Eq (subset a a_2) True) % 66.42/66.64 (Eq (in (skS.0 7 a_1 a a_2 a_3) a_1 → in (skS.0 7 a_1 a a_2 a_3) a → in (skS.0 7 a_1 a a_2 a_3) a_2) False))) % 66.42/66.64 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 : Iota), % 66.42/66.64 Or (Eq (in a (powerset a_1)) False) % 66.42/66.64 (Or (Eq (in a_2 (powerset a_1)) False) (Or (Eq (subset a a_2) True) (Eq (in (skS.0 7 a_1 a a_2 a_3) a_1) True))) % 66.42/66.64 Clause #78 (by clausification #[76]): ∀ (a a_1 a_2 a_3 : Iota), % 66.42/66.64 Or (Eq (in a (powerset a_1)) False) % 66.42/66.64 (Or (Eq (in a_2 (powerset a_1)) False) % 66.42/66.64 (Or (Eq (subset a a_2) True) (Eq (in (skS.0 7 a_1 a a_2 a_3) a → in (skS.0 7 a_1 a a_2 a_3) a_2) False))) % 66.42/66.64 Clause #80 (by clausification #[65]): Eq doubleComplementE1 True % 66.42/66.64 Clause #81 (by clausification #[65]): Eq (∀ (A X : Iota), in X (powerset A) → subset (setminus A (setminus A X)) X) False % 66.42/66.64 Clause #82 (by backward demodulation #[80, 4]): Eq True (∀ (A X : Iota), in X (powerset A) → ∀ (Xx : Iota), in Xx A → in Xx (setminus A (setminus A X)) → in Xx X) % 66.42/66.64 Clause #85 (by clausification #[82]): ∀ (a : Iota), % 66.42/66.64 Eq (∀ (X : Iota), in X (powerset a) → ∀ (Xx : Iota), in Xx a → in Xx (setminus a (setminus a X)) → in Xx X) True % 66.42/66.64 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), % 66.42/66.64 Eq (in a (powerset a_1) → ∀ (Xx : Iota), in Xx a_1 → in Xx (setminus a_1 (setminus a_1 a)) → in Xx a) True % 66.42/66.64 Clause #87 (by clausification #[86]): ∀ (a a_1 : Iota), % 66.42/66.64 Or (Eq (in a (powerset a_1)) False) % 66.42/66.64 (Eq (∀ (Xx : Iota), in Xx a_1 → in Xx (setminus a_1 (setminus a_1 a)) → in Xx a) True) % 66.42/66.64 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 : Iota), % 66.42/66.64 Or (Eq (in a (powerset a_1)) False) (Eq (in a_2 a_1 → in a_2 (setminus a_1 (setminus a_1 a)) → in a_2 a) True) % 66.42/66.64 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 : Iota), % 66.42/66.64 Or (Eq (in a (powerset a_1)) False) % 66.42/66.64 (Or (Eq (in a_2 a_1) False) (Eq (in a_2 (setminus a_1 (setminus a_1 a)) → in a_2 a) True)) % 66.42/66.64 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 : Iota), % 66.42/66.64 Or (Eq (in a (powerset a_1)) False) % 66.42/66.64 (Or (Eq (in a_2 a_1) False) (Or (Eq (in a_2 (setminus a_1 (setminus a_1 a))) False) (Eq (in a_2 a) True))) % 66.42/66.64 Clause #96 (by clausification #[81]): ∀ (a : Iota), % 66.42/66.64 Eq (Not (∀ (X : Iota), in X (powerset (skS.0 9 a)) → subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) X)) X)) True % 66.42/66.64 Clause #97 (by clausification #[96]): ∀ (a : Iota), % 66.42/66.64 Eq (∀ (X : Iota), in X (powerset (skS.0 9 a)) → subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) X)) X) False % 66.42/66.64 Clause #98 (by clausification #[97]): ∀ (a a_1 : Iota), % 66.42/66.64 Eq % 66.42/66.64 (Not % 66.42/66.64 (in (skS.0 10 a a_1) (powerset (skS.0 9 a)) → % 66.42/66.64 subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_1))) % 66.42/66.64 True % 66.42/66.64 Clause #99 (by clausification #[98]): ∀ (a a_1 : Iota), % 66.42/66.64 Eq % 66.42/66.64 (in (skS.0 10 a a_1) (powerset (skS.0 9 a)) → % 66.42/66.64 subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_1)) % 66.42/66.64 False % 66.42/66.64 Clause #100 (by clausification #[99]): ∀ (a a_1 : Iota), Eq (in (skS.0 10 a a_1) (powerset (skS.0 9 a))) True % 66.42/66.64 Clause #101 (by clausification #[99]): ∀ (a a_1 : Iota), Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_1)) False % 66.42/66.64 Clause #102 (by superposition #[100, 61]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (in (setminus (skS.0 9 a) (skS.0 10 a a_1)) (powerset (skS.0 9 a))) True) % 66.42/66.64 Clause #104 (by superposition #[100, 90]): ∀ (a a_1 a_2 : Iota), % 66.42/66.64 Or (Eq True False) % 66.42/66.64 (Or (Eq (in a (skS.0 9 a_1)) False) % 66.42/66.64 (Or (Eq (in a (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2)))) False) % 66.42/66.64 (Eq (in a (skS.0 10 a_1 a_2)) True))) % 66.42/66.64 Clause #127 (by clausification #[102]): ∀ (a a_1 : Iota), Eq (in (setminus (skS.0 9 a) (skS.0 10 a a_1)) (powerset (skS.0 9 a))) True % 66.50/66.67 Clause #128 (by superposition #[127, 61]): ∀ (a a_1 : Iota), % 66.50/66.67 Or (Eq True False) % 66.50/66.67 (Eq (in (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (powerset (skS.0 9 a))) True) % 66.50/66.67 Clause #139 (by clausification #[78]): ∀ (a a_1 a_2 a_3 : Iota), % 66.50/66.67 Or (Eq (in a (powerset a_1)) False) % 66.50/66.67 (Or (Eq (in a_2 (powerset a_1)) False) (Or (Eq (subset a a_2) True) (Eq (in (skS.0 7 a_1 a a_2 a_3) a) True))) % 66.50/66.67 Clause #140 (by clausification #[78]): ∀ (a a_1 a_2 a_3 : Iota), % 66.50/66.67 Or (Eq (in a (powerset a_1)) False) % 66.50/66.67 (Or (Eq (in a_2 (powerset a_1)) False) (Or (Eq (subset a a_2) True) (Eq (in (skS.0 7 a_1 a a_2 a_3) a_2) False))) % 66.50/66.67 Clause #149 (by clausification #[128]): ∀ (a a_1 : Iota), Eq (in (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (powerset (skS.0 9 a))) True % 66.50/66.67 Clause #151 (by superposition #[149, 77]): ∀ (a a_1 a_2 a_3 : Iota), % 66.50/66.67 Or (Eq True False) % 66.50/66.67 (Or (Eq (in a (powerset (skS.0 9 a_1))) False) % 66.50/66.67 (Or (Eq (subset (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a) True) % 66.50/66.67 (Eq % 66.50/66.67 (in (skS.0 7 (skS.0 9 a_1) (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a a_3) % 66.50/66.67 (skS.0 9 a_1)) % 66.50/66.67 True))) % 66.50/66.67 Clause #155 (by superposition #[149, 139]): ∀ (a a_1 a_2 a_3 : Iota), % 66.50/66.67 Or (Eq True False) % 66.50/66.67 (Or (Eq (in a (powerset (skS.0 9 a_1))) False) % 66.50/66.67 (Or (Eq (subset (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a) True) % 66.50/66.67 (Eq % 66.50/66.67 (in (skS.0 7 (skS.0 9 a_1) (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a a_3) % 66.50/66.67 (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2)))) % 66.50/66.67 True))) % 66.50/66.67 Clause #156 (by superposition #[149, 140]): ∀ (a a_1 a_2 a_3 : Iota), % 66.50/66.67 Or (Eq True False) % 66.50/66.67 (Or (Eq (in a (powerset (skS.0 9 a_1))) False) % 66.50/66.67 (Or (Eq (subset (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a) True) % 66.50/66.67 (Eq (in (skS.0 7 (skS.0 9 a_1) (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a a_3) a) % 66.50/66.67 False))) % 66.50/66.67 Clause #178 (by clausification #[104]): ∀ (a a_1 a_2 : Iota), % 66.50/66.67 Or (Eq (in a (skS.0 9 a_1)) False) % 66.50/66.67 (Or (Eq (in a (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2)))) False) % 66.50/66.67 (Eq (in a (skS.0 10 a_1 a_2)) True)) % 66.50/66.67 Clause #371 (by clausification #[151]): ∀ (a a_1 a_2 a_3 : Iota), % 66.50/66.67 Or (Eq (in a (powerset (skS.0 9 a_1))) False) % 66.50/66.67 (Or (Eq (subset (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a) True) % 66.50/66.67 (Eq % 66.50/66.67 (in (skS.0 7 (skS.0 9 a_1) (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a a_3) % 66.50/66.67 (skS.0 9 a_1)) % 66.50/66.67 True)) % 66.50/66.67 Clause #372 (by superposition #[371, 100]): ∀ (a a_1 a_2 a_3 : Iota), % 66.50/66.67 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.50/66.67 (Or % 66.50/66.67 (Eq % 66.50/66.67 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.50/66.67 (skS.0 9 a)) % 66.50/66.67 True) % 66.50/66.67 (Eq False True)) % 66.50/66.67 Clause #393 (by clausification #[156]): ∀ (a a_1 a_2 a_3 : Iota), % 66.50/66.67 Or (Eq (in a (powerset (skS.0 9 a_1))) False) % 66.50/66.67 (Or (Eq (subset (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a) True) % 66.50/66.67 (Eq (in (skS.0 7 (skS.0 9 a_1) (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a a_3) a) % 66.50/66.67 False)) % 66.50/66.67 Clause #394 (by superposition #[393, 100]): ∀ (a a_1 a_2 a_3 : Iota), % 66.50/66.67 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.50/66.67 (Or % 66.50/66.67 (Eq % 66.50/66.67 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.50/66.67 (skS.0 10 a a_2)) % 66.50/66.67 False) % 66.50/66.67 (Eq False True)) % 66.50/66.67 Clause #453 (by clausification #[155]): ∀ (a a_1 a_2 a_3 : Iota), % 66.50/66.67 Or (Eq (in a (powerset (skS.0 9 a_1))) False) % 66.50/66.67 (Or (Eq (subset (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a) True) % 66.50/66.67 (Eq % 66.50/66.67 (in (skS.0 7 (skS.0 9 a_1) (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2))) a a_3) % 66.51/66.69 (setminus (skS.0 9 a_1) (setminus (skS.0 9 a_1) (skS.0 10 a_1 a_2)))) % 66.51/66.69 True)) % 66.51/66.69 Clause #454 (by superposition #[453, 100]): ∀ (a a_1 a_2 a_3 : Iota), % 66.51/66.69 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.51/66.69 (Or % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1)))) % 66.51/66.69 True) % 66.51/66.69 (Eq False True)) % 66.51/66.69 Clause #476 (by clausification #[372]): ∀ (a a_1 a_2 a_3 : Iota), % 66.51/66.69 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (skS.0 9 a)) % 66.51/66.69 True) % 66.51/66.69 Clause #477 (by superposition #[476, 178]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 66.51/66.69 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.51/66.69 (Or (Eq True False) % 66.51/66.69 (Or % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_4)))) % 66.51/66.69 False) % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (skS.0 10 a a_4)) % 66.51/66.69 True))) % 66.51/66.69 Clause #555 (by clausification #[394]): ∀ (a a_1 a_2 a_3 : Iota), % 66.51/66.69 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (skS.0 10 a a_2)) % 66.51/66.69 False) % 66.51/66.69 Clause #768 (by clausification #[454]): ∀ (a a_1 a_2 a_3 : Iota), % 66.51/66.69 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1)))) % 66.51/66.69 True) % 66.51/66.69 Clause #2054 (by clausification #[477]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 66.51/66.69 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.51/66.69 (Or % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_4)))) % 66.51/66.69 False) % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (skS.0 10 a a_4)) % 66.51/66.69 True)) % 66.51/66.69 Clause #2079 (by superposition #[2054, 768]): ∀ (a a_1 a_2 a_3 : Iota), % 66.51/66.69 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.51/66.69 (Or % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (skS.0 10 a a_1)) % 66.51/66.69 True) % 66.51/66.69 (Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.51/66.69 (Eq False True))) % 66.51/66.69 Clause #2080 (by clausification #[2079]): ∀ (a a_1 a_2 a_3 : Iota), % 66.51/66.69 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.51/66.69 (Or % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (skS.0 10 a a_1)) % 66.51/66.69 True) % 66.51/66.69 (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True)) % 66.51/66.69 Clause #2081 (by eliminate duplicate literals #[2080]): ∀ (a a_1 a_2 a_3 : Iota), % 66.51/66.69 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2)) True) % 66.51/66.69 (Eq % 66.51/66.69 (in (skS.0 7 (skS.0 9 a) (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_2) a_3) % 66.51/66.69 (skS.0 10 a a_1)) % 66.51/66.72 True) % 66.51/66.72 Clause #2082 (by superposition #[2081, 555]): ∀ (a a_1 : Iota), % 66.51/66.72 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_1)) True) % 66.51/66.72 (Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_1)) True) % 66.51/66.72 (Eq True False)) % 66.51/66.72 Clause #2083 (by clausification #[2082]): ∀ (a a_1 : Iota), % 66.51/66.72 Or (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_1)) True) % 66.51/66.72 (Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_1)) True) % 66.51/66.72 Clause #2084 (by eliminate duplicate literals #[2083]): ∀ (a a_1 : Iota), Eq (subset (setminus (skS.0 9 a) (setminus (skS.0 9 a) (skS.0 10 a a_1))) (skS.0 10 a a_1)) True % 66.51/66.72 Clause #2085 (by superposition #[2084, 101]): Eq True False % 66.51/66.72 Clause #2107 (by clausification #[2085]): False % 66.51/66.72 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------