%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU755^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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 6.24s 6.41s % Output : Proof 6.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU755^2 : TPTP v9.2.0. Released v3.7.0. % 0.03/0.14 % Command : duper %s % 0.13/0.35 % Computer : n016.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 05:14:38 EDT 2025 % 0.13/0.35 % CPUTime : % 6.24/6.41 SZS status Theorem for theBenchmark.p % 6.24/6.41 SZS output start Proof for theBenchmark.p % 6.24/6.41 Clause #0 (by assumption #[]): Eq (Eq setminusI (∀ (A B Xx : Iota), in Xx A → Not (in Xx B) → in Xx (setminus A B))) True % 6.24/6.41 Clause #1 (by assumption #[]): Eq (Eq setminusER (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B))) True % 6.24/6.41 Clause #2 (by assumption #[]): Eq % 6.24/6.41 (Eq binunionTEcontra % 6.24/6.41 (∀ (A X : Iota), % 6.24/6.41 in X (powerset A) → % 6.24/6.41 ∀ (Y : Iota), % 6.24/6.41 in Y (powerset A) → ∀ (Xx : Iota), in Xx A → Not (in Xx X) → Not (in Xx Y) → Not (in Xx (binunion X Y)))) % 6.24/6.41 True % 6.24/6.41 Clause #3 (by assumption #[]): Eq % 6.24/6.41 (Not % 6.24/6.41 (setminusI → % 6.24/6.41 setminusER → % 6.24/6.41 binunionTEcontra → % 6.24/6.41 ∀ (A X : Iota), % 6.24/6.41 in X (powerset A) → % 6.24/6.41 ∀ (Y : Iota), % 6.24/6.41 in Y (powerset A) → % 6.24/6.41 ∀ (Xx : Iota), % 6.24/6.41 in Xx A → in Xx (setminus A X) → in Xx (setminus A Y) → in Xx (setminus A (binunion X Y)))) % 6.24/6.41 True % 6.24/6.41 Clause #4 (by clausification #[1]): Eq setminusER (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B)) % 6.24/6.41 Clause #21 (by clausification #[0]): Eq setminusI (∀ (A B Xx : Iota), in Xx A → Not (in Xx B) → in Xx (setminus A B)) % 6.24/6.41 Clause #25 (by clausification #[2]): Eq binunionTEcontra % 6.24/6.41 (∀ (A X : Iota), % 6.24/6.41 in X (powerset A) → % 6.24/6.41 ∀ (Y : Iota), % 6.24/6.41 in Y (powerset A) → ∀ (Xx : Iota), in Xx A → Not (in Xx X) → Not (in Xx Y) → Not (in Xx (binunion X Y))) % 6.24/6.41 Clause #61 (by clausification #[3]): Eq % 6.24/6.41 (setminusI → % 6.24/6.41 setminusER → % 6.24/6.41 binunionTEcontra → % 6.24/6.41 ∀ (A X : Iota), % 6.24/6.41 in X (powerset A) → % 6.24/6.41 ∀ (Y : Iota), % 6.24/6.41 in Y (powerset A) → % 6.24/6.41 ∀ (Xx : Iota), % 6.24/6.41 in Xx A → in Xx (setminus A X) → in Xx (setminus A Y) → in Xx (setminus A (binunion X Y))) % 6.24/6.41 False % 6.24/6.41 Clause #62 (by clausification #[61]): Eq setminusI True % 6.24/6.41 Clause #63 (by clausification #[61]): Eq % 6.24/6.41 (setminusER → % 6.24/6.41 binunionTEcontra → % 6.24/6.41 ∀ (A X : Iota), % 6.24/6.41 in X (powerset A) → % 6.24/6.41 ∀ (Y : Iota), % 6.24/6.41 in Y (powerset A) → % 6.24/6.41 ∀ (Xx : Iota), in Xx A → in Xx (setminus A X) → in Xx (setminus A Y) → in Xx (setminus A (binunion X Y))) % 6.24/6.41 False % 6.24/6.41 Clause #64 (by backward demodulation #[62, 21]): Eq True (∀ (A B Xx : Iota), in Xx A → Not (in Xx B) → in Xx (setminus A B)) % 6.24/6.41 Clause #67 (by clausification #[64]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), in Xx a → Not (in Xx B) → in Xx (setminus a B)) True % 6.24/6.41 Clause #68 (by clausification #[67]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), in Xx a → Not (in Xx a_1) → in Xx (setminus a a_1)) True % 6.24/6.41 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 : Iota), Eq (in a a_1 → Not (in a a_2) → in a (setminus a_1 a_2)) True % 6.24/6.41 Clause #70 (by clausification #[69]): ∀ (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) % 6.24/6.41 Clause #71 (by clausification #[70]): ∀ (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)) % 6.24/6.41 Clause #72 (by clausification #[71]): ∀ (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)) % 6.24/6.41 Clause #75 (by clausification #[63]): Eq setminusER True % 6.24/6.41 Clause #76 (by clausification #[63]): Eq % 6.24/6.41 (binunionTEcontra → % 6.24/6.41 ∀ (A X : Iota), % 6.24/6.41 in X (powerset A) → % 6.24/6.41 ∀ (Y : Iota), % 6.24/6.41 in Y (powerset A) → % 6.24/6.41 ∀ (Xx : Iota), in Xx A → in Xx (setminus A X) → in Xx (setminus A Y) → in Xx (setminus A (binunion X Y))) % 6.24/6.41 False % 6.24/6.41 Clause #77 (by backward demodulation #[75, 4]): Eq True (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B)) % 6.24/6.41 Clause #80 (by clausification #[77]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), in Xx (setminus a B) → Not (in Xx B)) True % 6.24/6.41 Clause #81 (by clausification #[80]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), in Xx (setminus a a_1) → Not (in Xx a_1)) True % 6.24/6.41 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 : Iota), Eq (in a (setminus a_1 a_2) → Not (in a a_2)) True % 6.24/6.41 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setminus a_1 a_2)) False) (Eq (Not (in a a_2)) True) % 6.24/6.44 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setminus a_1 a_2)) False) (Eq (in a a_2) False) % 6.24/6.44 Clause #87 (by clausification #[76]): Eq binunionTEcontra True % 6.24/6.44 Clause #88 (by clausification #[76]): Eq % 6.24/6.44 (∀ (A X : Iota), % 6.24/6.44 in X (powerset A) → % 6.24/6.44 ∀ (Y : Iota), % 6.24/6.44 in Y (powerset A) → % 6.24/6.44 ∀ (Xx : Iota), in Xx A → in Xx (setminus A X) → in Xx (setminus A Y) → in Xx (setminus A (binunion X Y))) % 6.24/6.44 False % 6.24/6.44 Clause #89 (by backward demodulation #[87, 25]): Eq True % 6.24/6.44 (∀ (A X : Iota), % 6.24/6.44 in X (powerset A) → % 6.24/6.44 ∀ (Y : Iota), % 6.24/6.44 in Y (powerset A) → ∀ (Xx : Iota), in Xx A → Not (in Xx X) → Not (in Xx Y) → Not (in Xx (binunion X Y))) % 6.24/6.44 Clause #92 (by clausification #[89]): ∀ (a : Iota), % 6.24/6.44 Eq % 6.24/6.44 (∀ (X : Iota), % 6.24/6.44 in X (powerset a) → % 6.24/6.44 ∀ (Y : Iota), % 6.24/6.44 in Y (powerset a) → ∀ (Xx : Iota), in Xx a → Not (in Xx X) → Not (in Xx Y) → Not (in Xx (binunion X Y))) % 6.24/6.44 True % 6.24/6.44 Clause #93 (by clausification #[92]): ∀ (a a_1 : Iota), % 6.24/6.44 Eq % 6.24/6.44 (in a (powerset a_1) → % 6.24/6.44 ∀ (Y : Iota), % 6.24/6.44 in Y (powerset a_1) → ∀ (Xx : Iota), in Xx a_1 → Not (in Xx a) → Not (in Xx Y) → Not (in Xx (binunion a Y))) % 6.24/6.44 True % 6.24/6.44 Clause #94 (by clausification #[93]): ∀ (a a_1 : Iota), % 6.24/6.44 Or (Eq (in a (powerset a_1)) False) % 6.24/6.44 (Eq % 6.24/6.44 (∀ (Y : Iota), % 6.24/6.44 in Y (powerset a_1) → ∀ (Xx : Iota), in Xx a_1 → Not (in Xx a) → Not (in Xx Y) → Not (in Xx (binunion a Y))) % 6.24/6.44 True) % 6.24/6.44 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 : Iota), % 6.24/6.44 Or (Eq (in a (powerset a_1)) False) % 6.24/6.44 (Eq % 6.24/6.44 (in a_2 (powerset a_1) → % 6.24/6.44 ∀ (Xx : Iota), in Xx a_1 → Not (in Xx a) → Not (in Xx a_2) → Not (in Xx (binunion a a_2))) % 6.24/6.44 True) % 6.24/6.44 Clause #96 (by clausification #[95]): ∀ (a a_1 a_2 : Iota), % 6.24/6.44 Or (Eq (in a (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_2 (powerset a_1)) False) % 6.24/6.44 (Eq (∀ (Xx : Iota), in Xx a_1 → Not (in Xx a) → Not (in Xx a_2) → Not (in Xx (binunion a a_2))) True)) % 6.24/6.44 Clause #97 (by clausification #[96]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.44 Or (Eq (in a (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_2 (powerset a_1)) False) % 6.24/6.44 (Eq (in a_3 a_1 → Not (in a_3 a) → Not (in a_3 a_2) → Not (in a_3 (binunion a a_2))) True)) % 6.24/6.44 Clause #98 (by clausification #[97]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.44 Or (Eq (in a (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_2 (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_3 a_1) False) (Eq (Not (in a_3 a) → Not (in a_3 a_2) → Not (in a_3 (binunion a a_2))) True))) % 6.24/6.44 Clause #99 (by clausification #[98]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.44 Or (Eq (in a (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_2 (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_3 a_1) False) % 6.24/6.44 (Or (Eq (Not (in a_3 a)) False) (Eq (Not (in a_3 a_2) → Not (in a_3 (binunion a a_2))) True)))) % 6.24/6.44 Clause #100 (by clausification #[99]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.44 Or (Eq (in a (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_2 (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_3 a_1) False) % 6.24/6.44 (Or (Eq (Not (in a_3 a_2) → Not (in a_3 (binunion a a_2))) True) (Eq (in a_3 a) True)))) % 6.24/6.44 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.44 Or (Eq (in a (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_2 (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_3 a_1) False) % 6.24/6.44 (Or (Eq (in a_3 a) True) (Or (Eq (Not (in a_3 a_2)) False) (Eq (Not (in a_3 (binunion a a_2))) True))))) % 6.24/6.44 Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.44 Or (Eq (in a (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_2 (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_3 a_1) False) % 6.24/6.44 (Or (Eq (in a_3 a) True) (Or (Eq (Not (in a_3 (binunion a a_2))) True) (Eq (in a_3 a_2) True))))) % 6.24/6.44 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 a_3 : Iota), % 6.24/6.44 Or (Eq (in a (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_2 (powerset a_1)) False) % 6.24/6.44 (Or (Eq (in a_3 a_1) False) % 6.24/6.44 (Or (Eq (in a_3 a) True) (Or (Eq (in a_3 a_2) True) (Eq (in a_3 (binunion a a_2)) False))))) % 6.24/6.44 Clause #104 (by clausification #[88]): ∀ (a : Iota), % 6.29/6.46 Eq % 6.29/6.46 (Not % 6.29/6.46 (∀ (X : Iota), % 6.29/6.46 in X (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Y : Iota), % 6.29/6.46 in Y (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Xx : Iota), % 6.29/6.46 in Xx (skS.0 8 a) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) X) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) Y) → in Xx (setminus (skS.0 8 a) (binunion X Y)))) % 6.29/6.46 True % 6.29/6.46 Clause #105 (by clausification #[104]): ∀ (a : Iota), % 6.29/6.46 Eq % 6.29/6.46 (∀ (X : Iota), % 6.29/6.46 in X (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Y : Iota), % 6.29/6.46 in Y (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Xx : Iota), % 6.29/6.46 in Xx (skS.0 8 a) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) X) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) Y) → in Xx (setminus (skS.0 8 a) (binunion X Y))) % 6.29/6.46 False % 6.29/6.46 Clause #106 (by clausification #[105]): ∀ (a a_1 : Iota), % 6.29/6.46 Eq % 6.29/6.46 (Not % 6.29/6.46 (in (skS.0 9 a a_1) (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Y : Iota), % 6.29/6.46 in Y (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Xx : Iota), % 6.29/6.46 in Xx (skS.0 8 a) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (skS.0 9 a a_1)) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) Y) → in Xx (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) Y)))) % 6.29/6.46 True % 6.29/6.46 Clause #107 (by clausification #[106]): ∀ (a a_1 : Iota), % 6.29/6.46 Eq % 6.29/6.46 (in (skS.0 9 a a_1) (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Y : Iota), % 6.29/6.46 in Y (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Xx : Iota), % 6.29/6.46 in Xx (skS.0 8 a) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (skS.0 9 a a_1)) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) Y) → in Xx (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) Y))) % 6.29/6.46 False % 6.29/6.46 Clause #108 (by clausification #[107]): ∀ (a a_1 : Iota), Eq (in (skS.0 9 a a_1) (powerset (skS.0 8 a))) True % 6.29/6.46 Clause #109 (by clausification #[107]): ∀ (a a_1 : Iota), % 6.29/6.46 Eq % 6.29/6.46 (∀ (Y : Iota), % 6.29/6.46 in Y (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Xx : Iota), % 6.29/6.46 in Xx (skS.0 8 a) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (skS.0 9 a a_1)) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) Y) → in Xx (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) Y))) % 6.29/6.46 False % 6.29/6.46 Clause #110 (by superposition #[108, 103]): ∀ (a a_1 a_2 a_3 : Iota), % 6.29/6.46 Or (Eq True False) % 6.29/6.46 (Or (Eq (in a (powerset (skS.0 8 a_1))) False) % 6.29/6.46 (Or (Eq (in a_2 (skS.0 8 a_1)) False) % 6.29/6.46 (Or (Eq (in a_2 (skS.0 9 a_1 a_3)) True) % 6.29/6.46 (Or (Eq (in a_2 a) True) (Eq (in a_2 (binunion (skS.0 9 a_1 a_3) a)) False))))) % 6.29/6.46 Clause #121 (by clausification #[109]): ∀ (a a_1 a_2 : Iota), % 6.29/6.46 Eq % 6.29/6.46 (Not % 6.29/6.46 (in (skS.0 11 a a_1 a_2) (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Xx : Iota), % 6.29/6.46 in Xx (skS.0 8 a) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (skS.0 9 a a_1)) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (skS.0 11 a a_1 a_2)) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) (skS.0 11 a a_1 a_2))))) % 6.29/6.46 True % 6.29/6.46 Clause #122 (by clausification #[121]): ∀ (a a_1 a_2 : Iota), % 6.29/6.46 Eq % 6.29/6.46 (in (skS.0 11 a a_1 a_2) (powerset (skS.0 8 a)) → % 6.29/6.46 ∀ (Xx : Iota), % 6.29/6.46 in Xx (skS.0 8 a) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (skS.0 9 a a_1)) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (skS.0 11 a a_1 a_2)) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) (skS.0 11 a a_1 a_2)))) % 6.29/6.46 False % 6.29/6.46 Clause #123 (by clausification #[122]): ∀ (a a_1 a_2 : Iota), Eq (in (skS.0 11 a a_1 a_2) (powerset (skS.0 8 a))) True % 6.29/6.46 Clause #124 (by clausification #[122]): ∀ (a a_1 a_2 : Iota), % 6.29/6.46 Eq % 6.29/6.46 (∀ (Xx : Iota), % 6.29/6.46 in Xx (skS.0 8 a) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (skS.0 9 a a_1)) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (skS.0 11 a a_1 a_2)) → % 6.29/6.46 in Xx (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) (skS.0 11 a a_1 a_2)))) % 6.29/6.46 False % 6.29/6.46 Clause #139 (by clausification #[124]): ∀ (a a_1 a_2 a_3 : Iota), % 6.29/6.46 Eq % 6.29/6.46 (Not % 6.29/6.46 (in (skS.0 13 a a_1 a_2 a_3) (skS.0 8 a) → % 6.29/6.46 in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (skS.0 9 a a_1)) → % 6.29/6.46 in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (skS.0 11 a a_1 a_2)) → % 6.29/6.46 in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) (skS.0 11 a a_1 a_2))))) % 6.29/6.49 True % 6.29/6.49 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 a_3 : Iota), % 6.29/6.49 Eq % 6.29/6.49 (in (skS.0 13 a a_1 a_2 a_3) (skS.0 8 a) → % 6.29/6.49 in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (skS.0 9 a a_1)) → % 6.29/6.49 in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (skS.0 11 a a_1 a_2)) → % 6.29/6.49 in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) (skS.0 11 a a_1 a_2)))) % 6.29/6.49 False % 6.29/6.49 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 8 a)) True % 6.29/6.49 Clause #142 (by clausification #[140]): ∀ (a a_1 a_2 a_3 : Iota), % 6.29/6.49 Eq % 6.29/6.49 (in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (skS.0 9 a a_1)) → % 6.29/6.49 in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (skS.0 11 a a_1 a_2)) → % 6.29/6.49 in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) (skS.0 11 a a_1 a_2)))) % 6.29/6.49 False % 6.29/6.49 Clause #143 (by superposition #[141, 72]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.29/6.49 Or (Eq True False) % 6.29/6.49 (Or (Eq (in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) a_4)) True) (Eq (in (skS.0 13 a a_1 a_2 a_3) a_4) True)) % 6.29/6.49 Clause #160 (by clausification #[110]): ∀ (a a_1 a_2 a_3 : Iota), % 6.29/6.49 Or (Eq (in a (powerset (skS.0 8 a_1))) False) % 6.29/6.49 (Or (Eq (in a_2 (skS.0 8 a_1)) False) % 6.29/6.49 (Or (Eq (in a_2 (skS.0 9 a_1 a_3)) True) % 6.29/6.49 (Or (Eq (in a_2 a) True) (Eq (in a_2 (binunion (skS.0 9 a_1 a_3) a)) False)))) % 6.29/6.49 Clause #162 (by superposition #[160, 123]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.29/6.49 Or (Eq (in a (skS.0 8 a_1)) False) % 6.29/6.49 (Or (Eq (in a (skS.0 9 a_1 a_2)) True) % 6.29/6.49 (Or (Eq (in a (skS.0 11 a_1 a_3 a_4)) True) % 6.29/6.49 (Or (Eq (in a (binunion (skS.0 9 a_1 a_2) (skS.0 11 a_1 a_3 a_4))) False) (Eq False True)))) % 6.29/6.49 Clause #163 (by clausification #[143]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.29/6.49 Or (Eq (in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) a_4)) True) (Eq (in (skS.0 13 a a_1 a_2 a_3) a_4) True) % 6.29/6.49 Clause #167 (by clausification #[142]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (skS.0 9 a a_1))) True % 6.29/6.49 Clause #168 (by clausification #[142]): ∀ (a a_1 a_2 a_3 : Iota), % 6.29/6.49 Eq % 6.29/6.49 (in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (skS.0 11 a a_1 a_2)) → % 6.29/6.49 in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) (skS.0 11 a a_1 a_2)))) % 6.29/6.49 False % 6.29/6.49 Clause #169 (by superposition #[167, 84]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 9 a a_1)) False) % 6.29/6.49 Clause #171 (by clausification #[169]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 9 a a_1)) False % 6.29/6.49 Clause #172 (by clausification #[168]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (skS.0 11 a a_1 a_2))) True % 6.29/6.49 Clause #173 (by clausification #[168]): ∀ (a a_1 a_2 a_3 : Iota), % 6.29/6.49 Eq (in (skS.0 13 a a_1 a_2 a_3) (setminus (skS.0 8 a) (binunion (skS.0 9 a a_1) (skS.0 11 a a_1 a_2)))) False % 6.29/6.49 Clause #174 (by superposition #[172, 84]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2)) False) % 6.29/6.49 Clause #179 (by clausification #[174]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2)) False % 6.29/6.49 Clause #180 (by superposition #[173, 163]): ∀ (a a_1 a_2 a_3 : Iota), % 6.29/6.49 Or (Eq False True) (Eq (in (skS.0 13 a a_1 a_2 a_3) (binunion (skS.0 9 a a_1) (skS.0 11 a a_1 a_2))) True) % 6.29/6.49 Clause #181 (by clausification #[180]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 13 a a_1 a_2 a_3) (binunion (skS.0 9 a a_1) (skS.0 11 a a_1 a_2))) True % 6.29/6.49 Clause #199 (by clausification #[162]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.29/6.49 Or (Eq (in a (skS.0 8 a_1)) False) % 6.29/6.49 (Or (Eq (in a (skS.0 9 a_1 a_2)) True) % 6.29/6.49 (Or (Eq (in a (skS.0 11 a_1 a_3 a_4)) True) % 6.29/6.49 (Eq (in a (binunion (skS.0 9 a_1 a_2) (skS.0 11 a_1 a_3 a_4))) False))) % 6.29/6.49 Clause #200 (by superposition #[199, 141]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 6.29/6.49 Or (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 9 a a_4)) True) % 6.29/6.49 (Or (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 11 a a_5 a_6)) True) % 6.29/6.50 (Or (Eq (in (skS.0 13 a a_1 a_2 a_3) (binunion (skS.0 9 a a_4) (skS.0 11 a a_5 a_6))) False) (Eq False True))) % 6.29/6.50 Clause #232 (by clausification #[200]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 6.29/6.50 Or (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 9 a a_4)) True) % 6.29/6.50 (Or (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 11 a a_5 a_6)) True) % 6.29/6.50 (Eq (in (skS.0 13 a a_1 a_2 a_3) (binunion (skS.0 9 a a_4) (skS.0 11 a a_5 a_6))) False)) % 6.29/6.50 Clause #233 (by superposition #[232, 181]): ∀ (a a_1 a_2 a_3 : Iota), % 6.29/6.50 Or (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 9 a a_1)) True) % 6.29/6.50 (Or (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2)) True) (Eq False True)) % 6.29/6.50 Clause #235 (by clausification #[233]): ∀ (a a_1 a_2 a_3 : Iota), % 6.29/6.50 Or (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 9 a a_1)) True) % 6.29/6.50 (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2)) True) % 6.29/6.50 Clause #236 (by forward demodulation #[235, 171]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq False True) (Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2)) True) % 6.29/6.50 Clause #237 (by clausification #[236]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 13 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2)) True % 6.29/6.50 Clause #238 (by superposition #[237, 179]): Eq True False % 6.29/6.50 Clause #240 (by clausification #[238]): False % 6.29/6.50 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------