%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU726^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n009.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:18 PM UTC 2025 % Result : Theorem 20.83s 21.08s % Output : Proof 20.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : SEU726^2 : TPTP v9.2.0. Released v3.7.0. % 0.00/0.08 % Command : duper %s % 0.09/0.29 % Computer : n009.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Fri Oct 3 04:23:08 EDT 2025 % 0.09/0.29 % CPUTime : % 20.83/21.08 SZS status Theorem for theBenchmark.p % 20.83/21.08 SZS output start Proof for theBenchmark.p % 20.83/21.08 Clause #0 (by assumption #[]): Eq (Eq subsetE (∀ (A B Xx : Iota), subset A B → in Xx A → in Xx B)) True % 20.83/21.08 Clause #1 (by assumption #[]): Eq (Eq setminusI (∀ (A B Xx : Iota), in Xx A → Not (in Xx B) → in Xx (setminus A B))) True % 20.83/21.08 Clause #2 (by assumption #[]): Eq (Eq setminusER (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B))) True % 20.83/21.08 Clause #3 (by assumption #[]): Eq % 20.83/21.08 (Eq subsetTI % 20.83/21.08 (∀ (A X : Iota), % 20.83/21.08 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → (∀ (Xx : Iota), in Xx A → in Xx X → in Xx Y) → subset X Y)) % 20.83/21.08 True % 20.83/21.08 Clause #4 (by assumption #[]): Eq % 20.83/21.08 (Not % 20.83/21.08 (subsetE → % 20.83/21.08 setminusI → % 20.83/21.08 setminusER → % 20.83/21.08 subsetTI → % 20.83/21.08 ∀ (A X : Iota), % 20.83/21.08 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → subset (setminus A Y) (setminus A X) → subset X Y)) % 20.83/21.08 True % 20.83/21.08 Clause #5 (by clausification #[2]): Eq setminusER (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B)) % 20.83/21.08 Clause #22 (by clausification #[0]): Eq subsetE (∀ (A B Xx : Iota), subset A B → in Xx A → in Xx B) % 20.83/21.08 Clause #26 (by clausification #[1]): Eq setminusI (∀ (A B Xx : Iota), in Xx A → Not (in Xx B) → in Xx (setminus A B)) % 20.83/21.08 Clause #43 (by clausification #[3]): Eq subsetTI % 20.83/21.08 (∀ (A X : Iota), % 20.83/21.08 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → (∀ (Xx : Iota), in Xx A → in Xx X → in Xx Y) → subset X Y) % 20.83/21.08 Clause #57 (by clausification #[4]): Eq % 20.83/21.08 (subsetE → % 20.83/21.08 setminusI → % 20.83/21.08 setminusER → % 20.83/21.08 subsetTI → % 20.83/21.08 ∀ (A X : Iota), % 20.83/21.08 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → subset (setminus A Y) (setminus A X) → subset X Y) % 20.83/21.08 False % 20.83/21.08 Clause #58 (by clausification #[57]): Eq subsetE True % 20.83/21.08 Clause #59 (by clausification #[57]): Eq % 20.83/21.08 (setminusI → % 20.83/21.08 setminusER → % 20.83/21.08 subsetTI → % 20.83/21.08 ∀ (A X : Iota), % 20.83/21.08 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → subset (setminus A Y) (setminus A X) → subset X Y) % 20.83/21.08 False % 20.83/21.08 Clause #60 (by backward demodulation #[58, 22]): Eq True (∀ (A B Xx : Iota), subset A B → in Xx A → in Xx B) % 20.83/21.08 Clause #63 (by clausification #[60]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), subset a B → in Xx a → in Xx B) True % 20.83/21.08 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), subset a a_1 → in Xx a → in Xx a_1) True % 20.83/21.08 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 : Iota), Eq (subset a a_1 → in a_2 a → in a_2 a_1) True % 20.83/21.08 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) False) (Eq (in a_2 a → in a_2 a_1) True) % 20.83/21.08 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) False) (Or (Eq (in a_2 a) False) (Eq (in a_2 a_1) True)) % 20.83/21.08 Clause #74 (by clausification #[59]): Eq setminusI True % 20.83/21.08 Clause #75 (by clausification #[59]): Eq % 20.83/21.08 (setminusER → % 20.83/21.08 subsetTI → % 20.83/21.08 ∀ (A X : Iota), % 20.83/21.08 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → subset (setminus A Y) (setminus A X) → subset X Y) % 20.83/21.08 False % 20.83/21.08 Clause #76 (by backward demodulation #[74, 26]): Eq True (∀ (A B Xx : Iota), in Xx A → Not (in Xx B) → in Xx (setminus A B)) % 20.83/21.08 Clause #77 (by clausification #[76]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), in Xx a → Not (in Xx B) → in Xx (setminus a B)) True % 20.83/21.08 Clause #78 (by clausification #[77]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), in Xx a → Not (in Xx a_1) → in Xx (setminus a a_1)) True % 20.83/21.08 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 : Iota), Eq (in a a_1 → Not (in a a_2) → in a (setminus a_1 a_2)) True % 20.83/21.08 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a a_1) False) (Eq (Not (in a a_2) → in a (setminus a_1 a_2)) True) % 20.83/21.08 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a a_1) False) (Or (Eq (Not (in a a_2)) False) (Eq (in a (setminus a_1 a_2)) True)) % 20.83/21.08 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a a_1) False) (Or (Eq (in a (setminus a_1 a_2)) True) (Eq (in a a_2) True)) % 20.83/21.08 Clause #85 (by clausification #[75]): Eq setminusER True % 20.94/21.11 Clause #86 (by clausification #[75]): Eq % 20.94/21.11 (subsetTI → % 20.94/21.11 ∀ (A X : Iota), % 20.94/21.11 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → subset (setminus A Y) (setminus A X) → subset X Y) % 20.94/21.11 False % 20.94/21.11 Clause #87 (by backward demodulation #[85, 5]): Eq True (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B)) % 20.94/21.11 Clause #92 (by clausification #[87]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), in Xx (setminus a B) → Not (in Xx B)) True % 20.94/21.11 Clause #93 (by clausification #[92]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), in Xx (setminus a a_1) → Not (in Xx a_1)) True % 20.94/21.11 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 : Iota), Eq (in a (setminus a_1 a_2) → Not (in a a_2)) True % 20.94/21.11 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setminus a_1 a_2)) False) (Eq (Not (in a a_2)) True) % 20.94/21.11 Clause #96 (by clausification #[95]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setminus a_1 a_2)) False) (Eq (in a a_2) False) % 20.94/21.11 Clause #97 (by clausification #[86]): Eq subsetTI True % 20.94/21.11 Clause #98 (by clausification #[86]): Eq % 20.94/21.11 (∀ (A X : Iota), % 20.94/21.11 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → subset (setminus A Y) (setminus A X) → subset X Y) % 20.94/21.11 False % 20.94/21.11 Clause #99 (by backward demodulation #[97, 43]): Eq True % 20.94/21.11 (∀ (A X : Iota), % 20.94/21.11 in X (powerset A) → ∀ (Y : Iota), in Y (powerset A) → (∀ (Xx : Iota), in Xx A → in Xx X → in Xx Y) → subset X Y) % 20.94/21.11 Clause #102 (by clausification #[99]): ∀ (a : Iota), % 20.94/21.11 Eq % 20.94/21.11 (∀ (X : Iota), % 20.94/21.11 in X (powerset a) → ∀ (Y : Iota), in Y (powerset a) → (∀ (Xx : Iota), in Xx a → in Xx X → in Xx Y) → subset X Y) % 20.94/21.11 True % 20.94/21.11 Clause #103 (by clausification #[102]): ∀ (a a_1 : Iota), % 20.94/21.11 Eq % 20.94/21.11 (in a (powerset a_1) → % 20.94/21.11 ∀ (Y : Iota), in Y (powerset a_1) → (∀ (Xx : Iota), in Xx a_1 → in Xx a → in Xx Y) → subset a Y) % 20.94/21.11 True % 20.94/21.11 Clause #104 (by clausification #[103]): ∀ (a a_1 : Iota), % 20.94/21.11 Or (Eq (in a (powerset a_1)) False) % 20.94/21.11 (Eq (∀ (Y : Iota), in Y (powerset a_1) → (∀ (Xx : Iota), in Xx a_1 → in Xx a → in Xx Y) → subset a Y) True) % 20.94/21.11 Clause #105 (by clausification #[104]): ∀ (a a_1 a_2 : Iota), % 20.94/21.11 Or (Eq (in a (powerset a_1)) False) % 20.94/21.11 (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) % 20.94/21.11 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 : Iota), % 20.94/21.11 Or (Eq (in a (powerset a_1)) False) % 20.94/21.11 (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)) % 20.94/21.11 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 20.94/21.11 Or (Eq (in a (powerset a_1)) False) % 20.94/21.11 (Or (Eq (in a_2 (powerset a_1)) False) % 20.94/21.11 (Or (Eq (∀ (Xx : Iota), in Xx a_1 → in Xx a → in Xx a_2) False) (Eq (subset a a_2) True))) % 20.94/21.11 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 a_3 : Iota), % 20.94/21.11 Or (Eq (in a (powerset a_1)) False) % 20.94/21.11 (Or (Eq (in a_2 (powerset a_1)) False) % 20.94/21.11 (Or (Eq (subset a a_2) True) % 20.94/21.11 (Eq (Not (in (skS.0 9 a_1 a a_2 a_3) a_1 → in (skS.0 9 a_1 a a_2 a_3) a → in (skS.0 9 a_1 a a_2 a_3) a_2)) % 20.94/21.11 True))) % 20.94/21.11 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 a_3 : Iota), % 20.94/21.11 Or (Eq (in a (powerset a_1)) False) % 20.94/21.11 (Or (Eq (in a_2 (powerset a_1)) False) % 20.94/21.11 (Or (Eq (subset a a_2) True) % 20.94/21.11 (Eq (in (skS.0 9 a_1 a a_2 a_3) a_1 → in (skS.0 9 a_1 a a_2 a_3) a → in (skS.0 9 a_1 a a_2 a_3) a_2) False))) % 20.94/21.11 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 a_3 : Iota), % 20.94/21.11 Or (Eq (in a (powerset a_1)) False) % 20.94/21.11 (Or (Eq (in a_2 (powerset a_1)) False) (Or (Eq (subset a a_2) True) (Eq (in (skS.0 9 a_1 a a_2 a_3) a_1) True))) % 20.94/21.11 Clause #111 (by clausification #[109]): ∀ (a a_1 a_2 a_3 : Iota), % 20.94/21.11 Or (Eq (in a (powerset a_1)) False) % 20.94/21.11 (Or (Eq (in a_2 (powerset a_1)) False) % 20.94/21.11 (Or (Eq (subset a a_2) True) (Eq (in (skS.0 9 a_1 a a_2 a_3) a → in (skS.0 9 a_1 a a_2 a_3) a_2) False))) % 20.94/21.11 Clause #112 (by clausification #[98]): ∀ (a : Iota), % 20.94/21.11 Eq % 20.94/21.11 (Not % 20.94/21.11 (∀ (X : Iota), % 20.94/21.11 in X (powerset (skS.0 10 a)) → % 20.94/21.11 ∀ (Y : Iota), % 20.94/21.11 in Y (powerset (skS.0 10 a)) → subset (setminus (skS.0 10 a) Y) (setminus (skS.0 10 a) X) → subset X Y)) % 20.95/21.14 True % 20.95/21.14 Clause #113 (by clausification #[112]): ∀ (a : Iota), % 20.95/21.14 Eq % 20.95/21.14 (∀ (X : Iota), % 20.95/21.14 in X (powerset (skS.0 10 a)) → % 20.95/21.14 ∀ (Y : Iota), % 20.95/21.14 in Y (powerset (skS.0 10 a)) → subset (setminus (skS.0 10 a) Y) (setminus (skS.0 10 a) X) → subset X Y) % 20.95/21.14 False % 20.95/21.14 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), % 20.95/21.14 Eq % 20.95/21.14 (Not % 20.95/21.14 (in (skS.0 11 a a_1) (powerset (skS.0 10 a)) → % 20.95/21.14 ∀ (Y : Iota), % 20.95/21.14 in Y (powerset (skS.0 10 a)) → % 20.95/21.14 subset (setminus (skS.0 10 a) Y) (setminus (skS.0 10 a) (skS.0 11 a a_1)) → subset (skS.0 11 a a_1) Y)) % 20.95/21.14 True % 20.95/21.14 Clause #115 (by clausification #[114]): ∀ (a a_1 : Iota), % 20.95/21.14 Eq % 20.95/21.14 (in (skS.0 11 a a_1) (powerset (skS.0 10 a)) → % 20.95/21.14 ∀ (Y : Iota), % 20.95/21.14 in Y (powerset (skS.0 10 a)) → % 20.95/21.14 subset (setminus (skS.0 10 a) Y) (setminus (skS.0 10 a) (skS.0 11 a a_1)) → subset (skS.0 11 a a_1) Y) % 20.95/21.14 False % 20.95/21.14 Clause #116 (by clausification #[115]): ∀ (a a_1 : Iota), Eq (in (skS.0 11 a a_1) (powerset (skS.0 10 a))) True % 20.95/21.14 Clause #117 (by clausification #[115]): ∀ (a a_1 : Iota), % 20.95/21.14 Eq % 20.95/21.14 (∀ (Y : Iota), % 20.95/21.14 in Y (powerset (skS.0 10 a)) → % 20.95/21.14 subset (setminus (skS.0 10 a) Y) (setminus (skS.0 10 a) (skS.0 11 a a_1)) → subset (skS.0 11 a a_1) Y) % 20.95/21.14 False % 20.95/21.14 Clause #118 (by superposition #[116, 110]): ∀ (a a_1 a_2 a_3 : Iota), % 20.95/21.14 Or (Eq True False) % 20.95/21.14 (Or (Eq (in a (powerset (skS.0 10 a_1))) False) % 20.95/21.14 (Or (Eq (subset (skS.0 11 a_1 a_2) a) True) % 20.95/21.14 (Eq (in (skS.0 9 (skS.0 10 a_1) (skS.0 11 a_1 a_2) a a_3) (skS.0 10 a_1)) True))) % 20.95/21.14 Clause #136 (by clausification #[117]): ∀ (a a_1 a_2 : Iota), % 20.95/21.14 Eq % 20.95/21.14 (Not % 20.95/21.14 (in (skS.0 15 a a_1 a_2) (powerset (skS.0 10 a)) → % 20.95/21.14 subset (setminus (skS.0 10 a) (skS.0 15 a a_1 a_2)) (setminus (skS.0 10 a) (skS.0 11 a a_1)) → % 20.95/21.14 subset (skS.0 11 a a_1) (skS.0 15 a a_1 a_2))) % 20.95/21.14 True % 20.95/21.14 Clause #137 (by clausification #[136]): ∀ (a a_1 a_2 : Iota), % 20.95/21.14 Eq % 20.95/21.14 (in (skS.0 15 a a_1 a_2) (powerset (skS.0 10 a)) → % 20.95/21.14 subset (setminus (skS.0 10 a) (skS.0 15 a a_1 a_2)) (setminus (skS.0 10 a) (skS.0 11 a a_1)) → % 20.95/21.14 subset (skS.0 11 a a_1) (skS.0 15 a a_1 a_2)) % 20.95/21.14 False % 20.95/21.14 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), Eq (in (skS.0 15 a a_1 a_2) (powerset (skS.0 10 a))) True % 20.95/21.14 Clause #139 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 20.95/21.14 Eq % 20.95/21.14 (subset (setminus (skS.0 10 a) (skS.0 15 a a_1 a_2)) (setminus (skS.0 10 a) (skS.0 11 a a_1)) → % 20.95/21.14 subset (skS.0 11 a a_1) (skS.0 15 a a_1 a_2)) % 20.95/21.14 False % 20.95/21.14 Clause #150 (by clausification #[139]): ∀ (a a_1 a_2 : Iota), % 20.95/21.14 Eq (subset (setminus (skS.0 10 a) (skS.0 15 a a_1 a_2)) (setminus (skS.0 10 a) (skS.0 11 a a_1))) True % 20.95/21.14 Clause #151 (by clausification #[139]): ∀ (a a_1 a_2 : Iota), Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_1 a_2)) False % 20.95/21.14 Clause #152 (by superposition #[150, 67]): ∀ (a a_1 a_2 a_3 : Iota), % 20.95/21.14 Or (Eq True False) % 20.95/21.14 (Or (Eq (in a (setminus (skS.0 10 a_1) (skS.0 15 a_1 a_2 a_3))) False) % 20.95/21.14 (Eq (in a (setminus (skS.0 10 a_1) (skS.0 11 a_1 a_2))) True)) % 20.95/21.14 Clause #174 (by clausification #[111]): ∀ (a a_1 a_2 a_3 : Iota), % 20.95/21.14 Or (Eq (in a (powerset a_1)) False) % 20.95/21.14 (Or (Eq (in a_2 (powerset a_1)) False) (Or (Eq (subset a a_2) True) (Eq (in (skS.0 9 a_1 a a_2 a_3) a) True))) % 20.95/21.14 Clause #175 (by clausification #[111]): ∀ (a a_1 a_2 a_3 : Iota), % 20.95/21.14 Or (Eq (in a (powerset a_1)) False) % 20.95/21.14 (Or (Eq (in a_2 (powerset a_1)) False) (Or (Eq (subset a a_2) True) (Eq (in (skS.0 9 a_1 a a_2 a_3) a_2) False))) % 20.95/21.14 Clause #176 (by superposition #[174, 116]): ∀ (a a_1 a_2 a_3 : Iota), % 20.95/21.14 Or (Eq (in a (powerset (skS.0 10 a_1))) False) % 20.95/21.14 (Or (Eq (subset (skS.0 11 a_1 a_2) a) True) % 20.95/21.14 (Or (Eq (in (skS.0 9 (skS.0 10 a_1) (skS.0 11 a_1 a_2) a a_3) (skS.0 11 a_1 a_2)) True) (Eq False True))) % 20.95/21.14 Clause #178 (by superposition #[175, 116]): ∀ (a a_1 a_2 a_3 : Iota), % 20.95/21.14 Or (Eq (in a (powerset (skS.0 10 a_1))) False) % 20.95/21.14 (Or (Eq (subset (skS.0 11 a_1 a_2) a) True) % 20.95/21.14 (Or (Eq (in (skS.0 9 (skS.0 10 a_1) (skS.0 11 a_1 a_2) a a_3) a) False) (Eq False True))) % 20.95/21.17 Clause #197 (by clausification #[152]): ∀ (a a_1 a_2 a_3 : Iota), % 20.95/21.17 Or (Eq (in a (setminus (skS.0 10 a_1) (skS.0 15 a_1 a_2 a_3))) False) % 20.95/21.17 (Eq (in a (setminus (skS.0 10 a_1) (skS.0 11 a_1 a_2))) True) % 20.95/21.17 Clause #198 (by clausification #[118]): ∀ (a a_1 a_2 a_3 : Iota), % 20.95/21.17 Or (Eq (in a (powerset (skS.0 10 a_1))) False) % 20.95/21.17 (Or (Eq (subset (skS.0 11 a_1 a_2) a) True) % 20.95/21.17 (Eq (in (skS.0 9 (skS.0 10 a_1) (skS.0 11 a_1 a_2) a a_3) (skS.0 10 a_1)) True)) % 20.95/21.17 Clause #200 (by superposition #[198, 138]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.17 (Or (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (skS.0 10 a)) True) (Eq False True)) % 20.95/21.17 Clause #208 (by clausification #[178]): ∀ (a a_1 a_2 a_3 : Iota), % 20.95/21.17 Or (Eq (in a (powerset (skS.0 10 a_1))) False) % 20.95/21.17 (Or (Eq (subset (skS.0 11 a_1 a_2) a) True) (Eq (in (skS.0 9 (skS.0 10 a_1) (skS.0 11 a_1 a_2) a a_3) a) False)) % 20.95/21.17 Clause #210 (by superposition #[208, 138]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.17 (Or (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (skS.0 15 a a_2 a_3)) False) % 20.95/21.17 (Eq False True)) % 20.95/21.17 Clause #233 (by clausification #[176]): ∀ (a a_1 a_2 a_3 : Iota), % 20.95/21.17 Or (Eq (in a (powerset (skS.0 10 a_1))) False) % 20.95/21.17 (Or (Eq (subset (skS.0 11 a_1 a_2) a) True) % 20.95/21.17 (Eq (in (skS.0 9 (skS.0 10 a_1) (skS.0 11 a_1 a_2) a a_3) (skS.0 11 a_1 a_2)) True)) % 20.95/21.17 Clause #235 (by superposition #[233, 138]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.17 (Or (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (skS.0 11 a a_1)) True) % 20.95/21.17 (Eq False True)) % 20.95/21.17 Clause #258 (by clausification #[200]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.17 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (skS.0 10 a)) True) % 20.95/21.17 Clause #259 (by superposition #[258, 82]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.17 (Or (Eq True False) % 20.95/21.17 (Or (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (setminus (skS.0 10 a) a_5)) True) % 20.95/21.17 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) a_5) True))) % 20.95/21.17 Clause #271 (by clausification #[235]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.17 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (skS.0 11 a a_1)) True) % 20.95/21.17 Clause #277 (by clausification #[210]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.17 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (skS.0 15 a a_2 a_3)) False) % 20.95/21.17 Clause #336 (by clausification #[259]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.17 (Or (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (setminus (skS.0 10 a) a_5)) True) % 20.95/21.17 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) a_5) True)) % 20.95/21.17 Clause #338 (by superposition #[336, 197]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.17 (Or (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (skS.0 15 a a_5 a_6)) True) % 20.95/21.17 (Or (Eq True False) % 20.95/21.17 (Eq % 20.95/21.17 (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (setminus (skS.0 10 a) (skS.0 11 a a_5))) % 20.95/21.17 True))) % 20.95/21.17 Clause #416 (by clausification #[338]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.17 (Or (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (skS.0 15 a a_5 a_6)) True) % 20.95/21.17 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (setminus (skS.0 10 a) (skS.0 11 a a_5))) % 20.95/21.17 True)) % 20.95/21.17 Clause #417 (by superposition #[416, 277]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.17 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.18 (Or % 20.95/21.18 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (setminus (skS.0 10 a) (skS.0 11 a a_2))) % 20.95/21.18 True) % 20.95/21.18 (Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) (Eq True False))) % 20.95/21.18 Clause #421 (by clausification #[417]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.18 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.18 (Or % 20.95/21.18 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (setminus (skS.0 10 a) (skS.0 11 a a_2))) % 20.95/21.18 True) % 20.95/21.18 (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True)) % 20.95/21.18 Clause #422 (by eliminate duplicate literals #[421]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.18 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.18 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (setminus (skS.0 10 a) (skS.0 11 a a_2))) % 20.95/21.18 True) % 20.95/21.18 Clause #423 (by superposition #[422, 96]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.18 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.18 (Or (Eq True False) % 20.95/21.18 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (skS.0 11 a a_2)) False)) % 20.95/21.18 Clause #425 (by clausification #[423]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.95/21.18 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_2 a_3)) True) % 20.95/21.18 (Eq (in (skS.0 9 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_2 a_3) a_4) (skS.0 11 a a_2)) False) % 20.95/21.18 Clause #426 (by superposition #[425, 271]): ∀ (a a_1 a_2 : Iota), % 20.95/21.18 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_1 a_2)) True) % 20.95/21.18 (Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_1 a_2)) True) (Eq False True)) % 20.95/21.18 Clause #430 (by clausification #[426]): ∀ (a a_1 a_2 : Iota), % 20.95/21.18 Or (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_1 a_2)) True) (Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_1 a_2)) True) % 20.95/21.18 Clause #431 (by eliminate duplicate literals #[430]): ∀ (a a_1 a_2 : Iota), Eq (subset (skS.0 11 a a_1) (skS.0 15 a a_1 a_2)) True % 20.95/21.18 Clause #432 (by superposition #[431, 151]): Eq True False % 20.95/21.18 Clause #434 (by clausification #[432]): False % 20.95/21.18 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------