%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU752^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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:22 PM UTC 2025 % Result : Theorem 5.75s 5.96s % Output : Proof 5.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU752^2 : TPTP v9.2.0. Released v3.7.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n012.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 04:47:53 EDT 2025 % 0.13/0.35 % CPUTime : % 5.75/5.96 SZS status Theorem for theBenchmark.p % 5.75/5.96 SZS output start Proof for theBenchmark.p % 5.75/5.96 Clause #0 (by assumption #[]): Eq (Eq binunionE (∀ (A B Xx : Iota), in Xx (binunion A B) → Or (in Xx A) (in Xx B))) True % 5.75/5.96 Clause #1 (by assumption #[]): Eq (Eq setminusI (∀ (A B Xx : Iota), in Xx A → Not (in Xx B) → in Xx (setminus A B))) True % 5.75/5.96 Clause #2 (by assumption #[]): Eq (Eq setminusER (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B))) True % 5.75/5.96 Clause #3 (by assumption #[]): Eq % 5.75/5.96 (Eq binintersectTELcontra % 5.75/5.96 (∀ (A X : Iota), % 5.75/5.96 in X (powerset A) → % 5.75/5.96 ∀ (Y : Iota), in Y (powerset A) → ∀ (Xx : Iota), in Xx A → Not (in Xx X) → Not (in Xx (binintersect X Y)))) % 5.75/5.96 True % 5.75/5.96 Clause #4 (by assumption #[]): Eq % 5.75/5.96 (Eq binintersectTERcontra % 5.75/5.96 (∀ (A X : Iota), % 5.75/5.96 in X (powerset A) → % 5.75/5.96 ∀ (Y : Iota), in Y (powerset A) → ∀ (Xx : Iota), in Xx A → Not (in Xx Y) → Not (in Xx (binintersect X Y)))) % 5.75/5.96 True % 5.75/5.96 Clause #5 (by assumption #[]): Eq % 5.75/5.96 (Not % 5.75/5.96 (binunionE → % 5.75/5.96 setminusI → % 5.75/5.96 setminusER → % 5.75/5.96 binintersectTELcontra → % 5.75/5.96 binintersectTERcontra → % 5.75/5.96 ∀ (A X : Iota), % 5.75/5.96 in X (powerset A) → % 5.75/5.96 ∀ (Y : Iota), % 5.75/5.96 in Y (powerset A) → % 5.75/5.96 ∀ (Xx : Iota), % 5.75/5.96 in Xx A → % 5.75/5.96 in Xx (binunion (setminus A X) (setminus A Y)) → in Xx (setminus A (binintersect X Y)))) % 5.75/5.96 True % 5.75/5.96 Clause #6 (by clausification #[2]): Eq setminusER (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B)) % 5.75/5.96 Clause #23 (by clausification #[1]): Eq setminusI (∀ (A B Xx : Iota), in Xx A → Not (in Xx B) → in Xx (setminus A B)) % 5.75/5.96 Clause #27 (by clausification #[0]): Eq binunionE (∀ (A B Xx : Iota), in Xx (binunion A B) → Or (in Xx A) (in Xx B)) % 5.75/5.96 Clause #58 (by clausification #[3]): Eq binintersectTELcontra % 5.75/5.96 (∀ (A X : Iota), % 5.75/5.96 in X (powerset A) → % 5.75/5.96 ∀ (Y : Iota), in Y (powerset A) → ∀ (Xx : Iota), in Xx A → Not (in Xx X) → Not (in Xx (binintersect X Y))) % 5.75/5.96 Clause #78 (by clausification #[4]): Eq binintersectTERcontra % 5.75/5.96 (∀ (A X : Iota), % 5.75/5.96 in X (powerset A) → % 5.75/5.96 ∀ (Y : Iota), in Y (powerset A) → ∀ (Xx : Iota), in Xx A → Not (in Xx Y) → Not (in Xx (binintersect X Y))) % 5.75/5.96 Clause #92 (by clausification #[5]): Eq % 5.75/5.96 (binunionE → % 5.75/5.96 setminusI → % 5.75/5.96 setminusER → % 5.75/5.96 binintersectTELcontra → % 5.75/5.96 binintersectTERcontra → % 5.75/5.96 ∀ (A X : Iota), % 5.75/5.96 in X (powerset A) → % 5.75/5.96 ∀ (Y : Iota), % 5.75/5.96 in Y (powerset A) → % 5.75/5.96 ∀ (Xx : Iota), % 5.75/5.96 in Xx A → in Xx (binunion (setminus A X) (setminus A Y)) → in Xx (setminus A (binintersect X Y))) % 5.75/5.96 False % 5.75/5.96 Clause #93 (by clausification #[92]): Eq binunionE True % 5.75/5.96 Clause #94 (by clausification #[92]): Eq % 5.75/5.96 (setminusI → % 5.75/5.96 setminusER → % 5.75/5.96 binintersectTELcontra → % 5.75/5.96 binintersectTERcontra → % 5.75/5.96 ∀ (A X : Iota), % 5.75/5.96 in X (powerset A) → % 5.75/5.96 ∀ (Y : Iota), % 5.75/5.96 in Y (powerset A) → % 5.75/5.96 ∀ (Xx : Iota), % 5.75/5.96 in Xx A → in Xx (binunion (setminus A X) (setminus A Y)) → in Xx (setminus A (binintersect X Y))) % 5.75/5.96 False % 5.75/5.96 Clause #95 (by backward demodulation #[93, 27]): Eq True (∀ (A B Xx : Iota), in Xx (binunion A B) → Or (in Xx A) (in Xx B)) % 5.75/5.96 Clause #98 (by clausification #[95]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), in Xx (binunion a B) → Or (in Xx a) (in Xx B)) True % 5.75/5.96 Clause #99 (by clausification #[98]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), in Xx (binunion a a_1) → Or (in Xx a) (in Xx a_1)) True % 5.75/5.96 Clause #100 (by clausification #[99]): ∀ (a a_1 a_2 : Iota), Eq (in a (binunion a_1 a_2) → Or (in a a_1) (in a a_2)) True % 5.75/5.96 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (binunion a_1 a_2)) False) (Eq (Or (in a a_1) (in a a_2)) True) % 5.75/5.96 Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (binunion a_1 a_2)) False) (Or (Eq (in a a_1) True) (Eq (in a a_2) True)) % 5.75/5.96 Clause #110 (by clausification #[94]): Eq setminusI True % 5.82/5.98 Clause #111 (by clausification #[94]): Eq % 5.82/5.98 (setminusER → % 5.82/5.98 binintersectTELcontra → % 5.82/5.98 binintersectTERcontra → % 5.82/5.98 ∀ (A X : Iota), % 5.82/5.98 in X (powerset A) → % 5.82/5.98 ∀ (Y : Iota), % 5.82/5.98 in Y (powerset A) → % 5.82/5.98 ∀ (Xx : Iota), % 5.82/5.98 in Xx A → in Xx (binunion (setminus A X) (setminus A Y)) → in Xx (setminus A (binintersect X Y))) % 5.82/5.98 False % 5.82/5.98 Clause #112 (by backward demodulation #[110, 23]): Eq True (∀ (A B Xx : Iota), in Xx A → Not (in Xx B) → in Xx (setminus A B)) % 5.82/5.98 Clause #115 (by clausification #[112]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), in Xx a → Not (in Xx B) → in Xx (setminus a B)) True % 5.82/5.98 Clause #116 (by clausification #[115]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), in Xx a → Not (in Xx a_1) → in Xx (setminus a a_1)) True % 5.82/5.98 Clause #117 (by clausification #[116]): ∀ (a a_1 a_2 : Iota), Eq (in a a_1 → Not (in a a_2) → in a (setminus a_1 a_2)) True % 5.82/5.98 Clause #118 (by clausification #[117]): ∀ (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) % 5.82/5.98 Clause #119 (by clausification #[118]): ∀ (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)) % 5.82/5.98 Clause #120 (by clausification #[119]): ∀ (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)) % 5.82/5.98 Clause #125 (by clausification #[111]): Eq setminusER True % 5.82/5.98 Clause #126 (by clausification #[111]): Eq % 5.82/5.98 (binintersectTELcontra → % 5.82/5.98 binintersectTERcontra → % 5.82/5.98 ∀ (A X : Iota), % 5.82/5.98 in X (powerset A) → % 5.82/5.98 ∀ (Y : Iota), % 5.82/5.98 in Y (powerset A) → % 5.82/5.98 ∀ (Xx : Iota), % 5.82/5.98 in Xx A → in Xx (binunion (setminus A X) (setminus A Y)) → in Xx (setminus A (binintersect X Y))) % 5.82/5.98 False % 5.82/5.98 Clause #127 (by backward demodulation #[125, 6]): Eq True (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B)) % 5.82/5.98 Clause #131 (by clausification #[127]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), in Xx (setminus a B) → Not (in Xx B)) True % 5.82/5.98 Clause #132 (by clausification #[131]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), in Xx (setminus a a_1) → Not (in Xx a_1)) True % 5.82/5.98 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), Eq (in a (setminus a_1 a_2) → Not (in a a_2)) True % 5.82/5.98 Clause #134 (by clausification #[133]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setminus a_1 a_2)) False) (Eq (Not (in a a_2)) True) % 5.82/5.98 Clause #135 (by clausification #[134]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setminus a_1 a_2)) False) (Eq (in a a_2) False) % 5.82/5.98 Clause #140 (by clausification #[126]): Eq binintersectTELcontra True % 5.82/5.98 Clause #141 (by clausification #[126]): Eq % 5.82/5.98 (binintersectTERcontra → % 5.82/5.98 ∀ (A X : Iota), % 5.82/5.98 in X (powerset A) → % 5.82/5.98 ∀ (Y : Iota), % 5.82/5.98 in Y (powerset A) → % 5.82/5.98 ∀ (Xx : Iota), % 5.82/5.98 in Xx A → in Xx (binunion (setminus A X) (setminus A Y)) → in Xx (setminus A (binintersect X Y))) % 5.82/5.98 False % 5.82/5.98 Clause #142 (by backward demodulation #[140, 58]): Eq True % 5.82/5.98 (∀ (A X : Iota), % 5.82/5.98 in X (powerset A) → % 5.82/5.98 ∀ (Y : Iota), in Y (powerset A) → ∀ (Xx : Iota), in Xx A → Not (in Xx X) → Not (in Xx (binintersect X Y))) % 5.82/5.98 Clause #145 (by clausification #[142]): ∀ (a : Iota), % 5.82/5.98 Eq % 5.82/5.98 (∀ (X : Iota), % 5.82/5.98 in X (powerset a) → % 5.82/5.98 ∀ (Y : Iota), in Y (powerset a) → ∀ (Xx : Iota), in Xx a → Not (in Xx X) → Not (in Xx (binintersect X Y))) % 5.82/5.98 True % 5.82/5.98 Clause #146 (by clausification #[145]): ∀ (a a_1 : Iota), % 5.82/5.98 Eq % 5.82/5.98 (in a (powerset a_1) → % 5.82/5.98 ∀ (Y : Iota), in Y (powerset a_1) → ∀ (Xx : Iota), in Xx a_1 → Not (in Xx a) → Not (in Xx (binintersect a Y))) % 5.82/5.98 True % 5.82/5.98 Clause #147 (by clausification #[146]): ∀ (a a_1 : Iota), % 5.82/5.98 Or (Eq (in a (powerset a_1)) False) % 5.82/5.98 (Eq (∀ (Y : Iota), in Y (powerset a_1) → ∀ (Xx : Iota), in Xx a_1 → Not (in Xx a) → Not (in Xx (binintersect a Y))) % 5.82/5.98 True) % 5.82/5.98 Clause #148 (by clausification #[147]): ∀ (a a_1 a_2 : Iota), % 5.82/5.98 Or (Eq (in a (powerset a_1)) False) % 5.82/5.98 (Eq (in a_2 (powerset a_1) → ∀ (Xx : Iota), in Xx a_1 → Not (in Xx a) → Not (in Xx (binintersect a a_2))) True) % 5.82/6.01 Clause #149 (by clausification #[148]): ∀ (a a_1 a_2 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.01 (Eq (∀ (Xx : Iota), in Xx a_1 → Not (in Xx a) → Not (in Xx (binintersect a a_2))) True)) % 5.82/6.01 Clause #150 (by clausification #[149]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_2 (powerset a_1)) False) (Eq (in a_3 a_1 → Not (in a_3 a) → Not (in a_3 (binintersect a a_2))) True)) % 5.82/6.01 Clause #151 (by clausification #[150]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_3 a_1) False) (Eq (Not (in a_3 a) → Not (in a_3 (binintersect a a_2))) True))) % 5.82/6.01 Clause #152 (by clausification #[151]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_3 a_1) False) (Or (Eq (Not (in a_3 a)) False) (Eq (Not (in a_3 (binintersect a a_2))) True)))) % 5.82/6.01 Clause #153 (by clausification #[152]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_3 a_1) False) (Or (Eq (Not (in a_3 (binintersect a a_2))) True) (Eq (in a_3 a) True)))) % 5.82/6.01 Clause #154 (by clausification #[153]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_3 a_1) False) (Or (Eq (in a_3 a) True) (Eq (in a_3 (binintersect a a_2)) False)))) % 5.82/6.01 Clause #156 (by clausification #[141]): Eq binintersectTERcontra True % 5.82/6.01 Clause #157 (by clausification #[141]): Eq % 5.82/6.01 (∀ (A X : Iota), % 5.82/6.01 in X (powerset A) → % 5.82/6.01 ∀ (Y : Iota), % 5.82/6.01 in Y (powerset A) → % 5.82/6.01 ∀ (Xx : Iota), % 5.82/6.01 in Xx A → in Xx (binunion (setminus A X) (setminus A Y)) → in Xx (setminus A (binintersect X Y))) % 5.82/6.01 False % 5.82/6.01 Clause #158 (by backward demodulation #[156, 78]): Eq True % 5.82/6.01 (∀ (A X : Iota), % 5.82/6.01 in X (powerset A) → % 5.82/6.01 ∀ (Y : Iota), in Y (powerset A) → ∀ (Xx : Iota), in Xx A → Not (in Xx Y) → Not (in Xx (binintersect X Y))) % 5.82/6.01 Clause #161 (by clausification #[158]): ∀ (a : Iota), % 5.82/6.01 Eq % 5.82/6.01 (∀ (X : Iota), % 5.82/6.01 in X (powerset a) → % 5.82/6.01 ∀ (Y : Iota), in Y (powerset a) → ∀ (Xx : Iota), in Xx a → Not (in Xx Y) → Not (in Xx (binintersect X Y))) % 5.82/6.01 True % 5.82/6.01 Clause #162 (by clausification #[161]): ∀ (a a_1 : Iota), % 5.82/6.01 Eq % 5.82/6.01 (in a (powerset a_1) → % 5.82/6.01 ∀ (Y : Iota), in Y (powerset a_1) → ∀ (Xx : Iota), in Xx a_1 → Not (in Xx Y) → Not (in Xx (binintersect a Y))) % 5.82/6.01 True % 5.82/6.01 Clause #163 (by clausification #[162]): ∀ (a a_1 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Eq (∀ (Y : Iota), in Y (powerset a_1) → ∀ (Xx : Iota), in Xx a_1 → Not (in Xx Y) → Not (in Xx (binintersect a Y))) % 5.82/6.01 True) % 5.82/6.01 Clause #164 (by clausification #[163]): ∀ (a a_1 a_2 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Eq (in a_2 (powerset a_1) → ∀ (Xx : Iota), in Xx a_1 → Not (in Xx a_2) → Not (in Xx (binintersect a a_2))) True) % 5.82/6.01 Clause #165 (by clausification #[164]): ∀ (a a_1 a_2 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.01 (Eq (∀ (Xx : Iota), in Xx a_1 → Not (in Xx a_2) → Not (in Xx (binintersect a a_2))) True)) % 5.82/6.01 Clause #166 (by clausification #[165]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.01 (Eq (in a_3 a_1 → Not (in a_3 a_2) → Not (in a_3 (binintersect a a_2))) True)) % 5.82/6.01 Clause #167 (by clausification #[166]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_3 a_1) False) (Eq (Not (in a_3 a_2) → Not (in a_3 (binintersect a a_2))) True))) % 5.82/6.01 Clause #168 (by clausification #[167]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.01 Or (Eq (in a (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.01 (Or (Eq (in a_3 a_1) False) (Or (Eq (Not (in a_3 a_2)) False) (Eq (Not (in a_3 (binintersect a a_2))) True)))) % 5.82/6.03 Clause #169 (by clausification #[168]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.03 Or (Eq (in a (powerset a_1)) False) % 5.82/6.03 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.03 (Or (Eq (in a_3 a_1) False) (Or (Eq (Not (in a_3 (binintersect a a_2))) True) (Eq (in a_3 a_2) True)))) % 5.82/6.03 Clause #170 (by clausification #[169]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.03 Or (Eq (in a (powerset a_1)) False) % 5.82/6.03 (Or (Eq (in a_2 (powerset a_1)) False) % 5.82/6.03 (Or (Eq (in a_3 a_1) False) (Or (Eq (in a_3 a_2) True) (Eq (in a_3 (binintersect a a_2)) False)))) % 5.82/6.03 Clause #174 (by clausification #[157]): ∀ (a : Iota), % 5.82/6.03 Eq % 5.82/6.03 (Not % 5.82/6.03 (∀ (X : Iota), % 5.82/6.03 in X (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Y : Iota), % 5.82/6.03 in Y (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Xx : Iota), % 5.82/6.03 in Xx (skS.0 13 a) → % 5.82/6.03 in Xx (binunion (setminus (skS.0 13 a) X) (setminus (skS.0 13 a) Y)) → % 5.82/6.03 in Xx (setminus (skS.0 13 a) (binintersect X Y)))) % 5.82/6.03 True % 5.82/6.03 Clause #175 (by clausification #[174]): ∀ (a : Iota), % 5.82/6.03 Eq % 5.82/6.03 (∀ (X : Iota), % 5.82/6.03 in X (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Y : Iota), % 5.82/6.03 in Y (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Xx : Iota), % 5.82/6.03 in Xx (skS.0 13 a) → % 5.82/6.03 in Xx (binunion (setminus (skS.0 13 a) X) (setminus (skS.0 13 a) Y)) → % 5.82/6.03 in Xx (setminus (skS.0 13 a) (binintersect X Y))) % 5.82/6.03 False % 5.82/6.03 Clause #176 (by clausification #[175]): ∀ (a a_1 : Iota), % 5.82/6.03 Eq % 5.82/6.03 (Not % 5.82/6.03 (in (skS.0 14 a a_1) (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Y : Iota), % 5.82/6.03 in Y (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Xx : Iota), % 5.82/6.03 in Xx (skS.0 13 a) → % 5.82/6.03 in Xx (binunion (setminus (skS.0 13 a) (skS.0 14 a a_1)) (setminus (skS.0 13 a) Y)) → % 5.82/6.03 in Xx (setminus (skS.0 13 a) (binintersect (skS.0 14 a a_1) Y)))) % 5.82/6.03 True % 5.82/6.03 Clause #177 (by clausification #[176]): ∀ (a a_1 : Iota), % 5.82/6.03 Eq % 5.82/6.03 (in (skS.0 14 a a_1) (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Y : Iota), % 5.82/6.03 in Y (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Xx : Iota), % 5.82/6.03 in Xx (skS.0 13 a) → % 5.82/6.03 in Xx (binunion (setminus (skS.0 13 a) (skS.0 14 a a_1)) (setminus (skS.0 13 a) Y)) → % 5.82/6.03 in Xx (setminus (skS.0 13 a) (binintersect (skS.0 14 a a_1) Y))) % 5.82/6.03 False % 5.82/6.03 Clause #178 (by clausification #[177]): ∀ (a a_1 : Iota), Eq (in (skS.0 14 a a_1) (powerset (skS.0 13 a))) True % 5.82/6.03 Clause #179 (by clausification #[177]): ∀ (a a_1 : Iota), % 5.82/6.03 Eq % 5.82/6.03 (∀ (Y : Iota), % 5.82/6.03 in Y (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Xx : Iota), % 5.82/6.03 in Xx (skS.0 13 a) → % 5.82/6.03 in Xx (binunion (setminus (skS.0 13 a) (skS.0 14 a a_1)) (setminus (skS.0 13 a) Y)) → % 5.82/6.03 in Xx (setminus (skS.0 13 a) (binintersect (skS.0 14 a a_1) Y))) % 5.82/6.03 False % 5.82/6.03 Clause #180 (by superposition #[178, 154]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.03 Or (Eq True False) % 5.82/6.03 (Or (Eq (in a (powerset (skS.0 13 a_1))) False) % 5.82/6.03 (Or (Eq (in a_2 (skS.0 13 a_1)) False) % 5.82/6.03 (Or (Eq (in a_2 (skS.0 14 a_1 a_3)) True) (Eq (in a_2 (binintersect (skS.0 14 a_1 a_3) a)) False)))) % 5.82/6.03 Clause #181 (by superposition #[178, 170]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.03 Or (Eq True False) % 5.82/6.03 (Or (Eq (in a (powerset (skS.0 13 a_1))) False) % 5.82/6.03 (Or (Eq (in a_2 (skS.0 13 a_1)) False) % 5.82/6.03 (Or (Eq (in a_2 a) True) (Eq (in a_2 (binintersect (skS.0 14 a_1 a_3) a)) False)))) % 5.82/6.03 Clause #194 (by clausification #[179]): ∀ (a a_1 a_2 : Iota), % 5.82/6.03 Eq % 5.82/6.03 (Not % 5.82/6.03 (in (skS.0 17 a a_1 a_2) (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Xx : Iota), % 5.82/6.03 in Xx (skS.0 13 a) → % 5.82/6.03 in Xx (binunion (setminus (skS.0 13 a) (skS.0 14 a a_1)) (setminus (skS.0 13 a) (skS.0 17 a a_1 a_2))) → % 5.82/6.03 in Xx (setminus (skS.0 13 a) (binintersect (skS.0 14 a a_1) (skS.0 17 a a_1 a_2))))) % 5.82/6.03 True % 5.82/6.03 Clause #195 (by clausification #[194]): ∀ (a a_1 a_2 : Iota), % 5.82/6.03 Eq % 5.82/6.03 (in (skS.0 17 a a_1 a_2) (powerset (skS.0 13 a)) → % 5.82/6.03 ∀ (Xx : Iota), % 5.82/6.03 in Xx (skS.0 13 a) → % 5.82/6.03 in Xx (binunion (setminus (skS.0 13 a) (skS.0 14 a a_1)) (setminus (skS.0 13 a) (skS.0 17 a a_1 a_2))) → % 5.82/6.03 in Xx (setminus (skS.0 13 a) (binintersect (skS.0 14 a a_1) (skS.0 17 a a_1 a_2)))) % 5.82/6.06 False % 5.82/6.06 Clause #196 (by clausification #[195]): ∀ (a a_1 a_2 : Iota), Eq (in (skS.0 17 a a_1 a_2) (powerset (skS.0 13 a))) True % 5.82/6.06 Clause #197 (by clausification #[195]): ∀ (a a_1 a_2 : Iota), % 5.82/6.06 Eq % 5.82/6.06 (∀ (Xx : Iota), % 5.82/6.06 in Xx (skS.0 13 a) → % 5.82/6.06 in Xx (binunion (setminus (skS.0 13 a) (skS.0 14 a a_1)) (setminus (skS.0 13 a) (skS.0 17 a a_1 a_2))) → % 5.82/6.06 in Xx (setminus (skS.0 13 a) (binintersect (skS.0 14 a a_1) (skS.0 17 a a_1 a_2)))) % 5.82/6.06 False % 5.82/6.06 Clause #218 (by clausification #[197]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.06 Eq % 5.82/6.06 (Not % 5.82/6.06 (in (skS.0 20 a a_1 a_2 a_3) (skS.0 13 a) → % 5.82/6.06 in (skS.0 20 a a_1 a_2 a_3) % 5.82/6.06 (binunion (setminus (skS.0 13 a) (skS.0 14 a a_1)) (setminus (skS.0 13 a) (skS.0 17 a a_1 a_2))) → % 5.82/6.06 in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (binintersect (skS.0 14 a a_1) (skS.0 17 a a_1 a_2))))) % 5.82/6.06 True % 5.82/6.06 Clause #219 (by clausification #[218]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.06 Eq % 5.82/6.06 (in (skS.0 20 a a_1 a_2 a_3) (skS.0 13 a) → % 5.82/6.06 in (skS.0 20 a a_1 a_2 a_3) % 5.82/6.06 (binunion (setminus (skS.0 13 a) (skS.0 14 a a_1)) (setminus (skS.0 13 a) (skS.0 17 a a_1 a_2))) → % 5.82/6.06 in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (binintersect (skS.0 14 a a_1) (skS.0 17 a a_1 a_2)))) % 5.82/6.06 False % 5.82/6.06 Clause #220 (by clausification #[219]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 13 a)) True % 5.82/6.06 Clause #221 (by clausification #[219]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.06 Eq % 5.82/6.06 (in (skS.0 20 a a_1 a_2 a_3) % 5.82/6.06 (binunion (setminus (skS.0 13 a) (skS.0 14 a a_1)) (setminus (skS.0 13 a) (skS.0 17 a a_1 a_2))) → % 5.82/6.06 in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (binintersect (skS.0 14 a a_1) (skS.0 17 a a_1 a_2)))) % 5.82/6.06 False % 5.82/6.06 Clause #222 (by superposition #[220, 120]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.82/6.06 Or (Eq True False) % 5.82/6.06 (Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) a_4)) True) (Eq (in (skS.0 20 a a_1 a_2 a_3) a_4) True)) % 5.82/6.06 Clause #247 (by clausification #[181]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.06 Or (Eq (in a (powerset (skS.0 13 a_1))) False) % 5.82/6.06 (Or (Eq (in a_2 (skS.0 13 a_1)) False) % 5.82/6.06 (Or (Eq (in a_2 a) True) (Eq (in a_2 (binintersect (skS.0 14 a_1 a_3) a)) False))) % 5.82/6.06 Clause #249 (by superposition #[247, 196]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.82/6.06 Or (Eq (in a (skS.0 13 a_1)) False) % 5.82/6.06 (Or (Eq (in a (skS.0 17 a_1 a_2 a_3)) True) % 5.82/6.06 (Or (Eq (in a (binintersect (skS.0 14 a_1 a_4) (skS.0 17 a_1 a_2 a_3))) False) (Eq False True))) % 5.82/6.06 Clause #250 (by clausification #[222]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.82/6.06 Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) a_4)) True) (Eq (in (skS.0 20 a a_1 a_2 a_3) a_4) True) % 5.82/6.06 Clause #257 (by clausification #[221]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.06 Eq % 5.82/6.06 (in (skS.0 20 a a_1 a_2 a_3) % 5.82/6.06 (binunion (setminus (skS.0 13 a) (skS.0 14 a a_1)) (setminus (skS.0 13 a) (skS.0 17 a a_1 a_2)))) % 5.82/6.06 True % 5.82/6.06 Clause #258 (by clausification #[221]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.06 Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (binintersect (skS.0 14 a a_1) (skS.0 17 a a_1 a_2)))) False % 5.82/6.06 Clause #259 (by superposition #[257, 102]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.06 Or (Eq True False) % 5.82/6.06 (Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (skS.0 14 a a_1))) True) % 5.82/6.06 (Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (skS.0 17 a a_1 a_2))) True)) % 5.82/6.06 Clause #261 (by clausification #[180]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.06 Or (Eq (in a (powerset (skS.0 13 a_1))) False) % 5.82/6.06 (Or (Eq (in a_2 (skS.0 13 a_1)) False) % 5.82/6.06 (Or (Eq (in a_2 (skS.0 14 a_1 a_3)) True) (Eq (in a_2 (binintersect (skS.0 14 a_1 a_3) a)) False))) % 5.82/6.06 Clause #263 (by superposition #[261, 196]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.82/6.06 Or (Eq (in a (skS.0 13 a_1)) False) % 5.82/6.06 (Or (Eq (in a (skS.0 14 a_1 a_2)) True) % 5.82/6.06 (Or (Eq (in a (binintersect (skS.0 14 a_1 a_2) (skS.0 17 a_1 a_3 a_4))) False) (Eq False True))) % 5.82/6.06 Clause #264 (by superposition #[258, 250]): ∀ (a a_1 a_2 a_3 : Iota), % 5.82/6.06 Or (Eq False True) (Eq (in (skS.0 20 a a_1 a_2 a_3) (binintersect (skS.0 14 a a_1) (skS.0 17 a a_1 a_2))) True) % 5.92/6.08 Clause #265 (by clausification #[264]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 20 a a_1 a_2 a_3) (binintersect (skS.0 14 a a_1) (skS.0 17 a a_1 a_2))) True % 5.92/6.08 Clause #271 (by clausification #[263]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.92/6.08 Or (Eq (in a (skS.0 13 a_1)) False) % 5.92/6.08 (Or (Eq (in a (skS.0 14 a_1 a_2)) True) (Eq (in a (binintersect (skS.0 14 a_1 a_2) (skS.0 17 a_1 a_3 a_4))) False)) % 5.92/6.08 Clause #272 (by superposition #[271, 220]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 5.92/6.08 Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 14 a a_4)) True) % 5.92/6.08 (Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (binintersect (skS.0 14 a a_4) (skS.0 17 a a_5 a_6))) False) (Eq False True)) % 5.92/6.08 Clause #284 (by clausification #[249]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.92/6.08 Or (Eq (in a (skS.0 13 a_1)) False) % 5.92/6.08 (Or (Eq (in a (skS.0 17 a_1 a_2 a_3)) True) % 5.92/6.08 (Eq (in a (binintersect (skS.0 14 a_1 a_4) (skS.0 17 a_1 a_2 a_3))) False)) % 5.92/6.08 Clause #285 (by superposition #[284, 220]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 5.92/6.08 Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 17 a a_4 a_5)) True) % 5.92/6.08 (Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (binintersect (skS.0 14 a a_6) (skS.0 17 a a_4 a_5))) False) (Eq False True)) % 5.92/6.08 Clause #303 (by clausification #[272]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 5.92/6.08 Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 14 a a_4)) True) % 5.92/6.08 (Eq (in (skS.0 20 a a_1 a_2 a_3) (binintersect (skS.0 14 a a_4) (skS.0 17 a a_5 a_6))) False) % 5.92/6.08 Clause #304 (by superposition #[303, 265]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 14 a a_1)) True) (Eq False True) % 5.92/6.08 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 14 a a_1)) True % 5.92/6.08 Clause #307 (by clausification #[259]): ∀ (a a_1 a_2 a_3 : Iota), % 5.92/6.08 Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (skS.0 14 a a_1))) True) % 5.92/6.08 (Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (skS.0 17 a a_1 a_2))) True) % 5.92/6.08 Clause #308 (by superposition #[307, 135]): ∀ (a a_1 a_2 a_3 : Iota), % 5.92/6.08 Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (skS.0 14 a a_1))) True) % 5.92/6.08 (Or (Eq True False) (Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 17 a a_1 a_2)) False)) % 5.92/6.08 Clause #312 (by clausification #[308]): ∀ (a a_1 a_2 a_3 : Iota), % 5.92/6.08 Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (skS.0 14 a a_1))) True) % 5.92/6.08 (Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 17 a a_1 a_2)) False) % 5.92/6.08 Clause #321 (by clausification #[285]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 5.92/6.08 Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 17 a a_4 a_5)) True) % 5.92/6.08 (Eq (in (skS.0 20 a a_1 a_2 a_3) (binintersect (skS.0 14 a a_6) (skS.0 17 a a_4 a_5))) False) % 5.92/6.08 Clause #322 (by superposition #[321, 265]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 17 a a_1 a_2)) True) (Eq False True) % 5.92/6.08 Clause #323 (by clausification #[322]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 17 a a_1 a_2)) True % 5.92/6.08 Clause #324 (by superposition #[323, 312]): ∀ (a a_1 a_2 a_3 : Iota), % 5.92/6.08 Or (Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (skS.0 14 a a_1))) True) (Eq True False) % 5.92/6.08 Clause #326 (by clausification #[324]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 20 a a_1 a_2 a_3) (setminus (skS.0 13 a) (skS.0 14 a a_1))) True % 5.92/6.08 Clause #328 (by superposition #[326, 135]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 14 a a_1)) False) % 5.92/6.08 Clause #330 (by clausification #[328]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 20 a a_1 a_2 a_3) (skS.0 14 a a_1)) False % 5.92/6.08 Clause #331 (by superposition #[330, 305]): Eq False True % 5.92/6.08 Clause #332 (by clausification #[331]): False % 5.92/6.08 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------