%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU635^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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:06 PM UTC 2025 % Result : Theorem 4.51s 4.72s % Output : Proof 4.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU635^2 : TPTP v9.2.0. Released v3.7.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n008.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 05:31:53 EDT 2025 % 0.13/0.34 % CPUTime : % 4.51/4.72 SZS status Theorem for theBenchmark.p % 4.51/4.72 SZS output start Proof for theBenchmark.p % 4.51/4.72 Clause #0 (by assumption #[]): Eq (Eq setadjoinIL (∀ (Xx Xy : Iota), in Xx (setadjoin Xx Xy))) True % 4.51/4.72 Clause #1 (by assumption #[]): Eq (Eq setunionI (∀ (A Xx B : Iota), in Xx B → in B A → in Xx (setunion A))) True % 4.51/4.72 Clause #2 (by assumption #[]): Eq (Eq subsetI2 (∀ (A B : Iota), (∀ (Xx : Iota), in Xx A → in Xx B) → subset A B)) True % 4.51/4.72 Clause #3 (by assumption #[]): Eq (Not (setadjoinIL → setunionI → subsetI2 → ∀ (A : Iota), subset A (setunion (setadjoin A emptyset)))) True % 4.51/4.72 Clause #4 (by clausification #[2]): Eq subsetI2 (∀ (A B : Iota), (∀ (Xx : Iota), in Xx A → in Xx B) → subset A B) % 4.51/4.72 Clause #23 (by clausification #[0]): Eq setadjoinIL (∀ (Xx Xy : Iota), in Xx (setadjoin Xx Xy)) % 4.51/4.72 Clause #25 (by clausify Prop equality #[23]): Or (Eq setadjoinIL False) (Eq (∀ (Xx Xy : Iota), in Xx (setadjoin Xx Xy)) True) % 4.51/4.72 Clause #27 (by clausification #[1]): Eq setunionI (∀ (A Xx B : Iota), in Xx B → in B A → in Xx (setunion A)) % 4.51/4.72 Clause #31 (by clausification #[25]): ∀ (a : Iota), Or (Eq setadjoinIL False) (Eq (∀ (Xy : Iota), in a (setadjoin a Xy)) True) % 4.51/4.72 Clause #32 (by clausification #[31]): ∀ (a a_1 : Iota), Or (Eq setadjoinIL False) (Eq (in a (setadjoin a a_1)) True) % 4.51/4.72 Clause #50 (by clausification #[3]): Eq (setadjoinIL → setunionI → subsetI2 → ∀ (A : Iota), subset A (setunion (setadjoin A emptyset))) False % 4.51/4.72 Clause #51 (by clausification #[50]): Eq setadjoinIL True % 4.51/4.72 Clause #52 (by clausification #[50]): Eq (setunionI → subsetI2 → ∀ (A : Iota), subset A (setunion (setadjoin A emptyset))) False % 4.51/4.72 Clause #54 (by backward demodulation #[51, 32]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (in a (setadjoin a a_1)) True) % 4.51/4.72 Clause #56 (by clausification #[54]): ∀ (a a_1 : Iota), Eq (in a (setadjoin a a_1)) True % 4.51/4.72 Clause #58 (by clausification #[52]): Eq setunionI True % 4.51/4.72 Clause #59 (by clausification #[52]): Eq (subsetI2 → ∀ (A : Iota), subset A (setunion (setadjoin A emptyset))) False % 4.51/4.72 Clause #60 (by backward demodulation #[58, 27]): Eq True (∀ (A Xx B : Iota), in Xx B → in B A → in Xx (setunion A)) % 4.51/4.72 Clause #63 (by clausification #[59]): Eq subsetI2 True % 4.51/4.72 Clause #64 (by clausification #[59]): Eq (∀ (A : Iota), subset A (setunion (setadjoin A emptyset))) False % 4.51/4.72 Clause #65 (by backward demodulation #[63, 4]): Eq True (∀ (A B : Iota), (∀ (Xx : Iota), in Xx A → in Xx B) → subset A B) % 4.51/4.72 Clause #68 (by clausification #[65]): ∀ (a : Iota), Eq (∀ (B : Iota), (∀ (Xx : Iota), in Xx a → in Xx B) → subset a B) True % 4.51/4.72 Clause #69 (by clausification #[68]): ∀ (a a_1 : Iota), Eq ((∀ (Xx : Iota), in Xx a → in Xx a_1) → subset a a_1) True % 4.51/4.72 Clause #70 (by clausification #[69]): ∀ (a a_1 : Iota), Or (Eq (∀ (Xx : Iota), in Xx a → in Xx a_1) False) (Eq (subset a a_1) True) % 4.51/4.72 Clause #71 (by clausification #[70]): ∀ (a a_1 a_2 : Iota), % 4.51/4.72 Or (Eq (subset a a_1) True) (Eq (Not (in (skS.0 8 a a_1 a_2) a → in (skS.0 8 a a_1 a_2) a_1)) True) % 4.51/4.72 Clause #72 (by clausification #[71]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) True) (Eq (in (skS.0 8 a a_1 a_2) a → in (skS.0 8 a a_1 a_2) a_1) False) % 4.51/4.72 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) True) (Eq (in (skS.0 8 a a_1 a_2) a) True) % 4.51/4.72 Clause #74 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) True) (Eq (in (skS.0 8 a a_1 a_2) a_1) False) % 4.51/4.72 Clause #77 (by clausification #[64]): ∀ (a : Iota), Eq (Not (subset (skS.0 9 a) (setunion (setadjoin (skS.0 9 a) emptyset)))) True % 4.51/4.72 Clause #78 (by clausification #[77]): ∀ (a : Iota), Eq (subset (skS.0 9 a) (setunion (setadjoin (skS.0 9 a) emptyset))) False % 4.51/4.72 Clause #79 (by clausification #[60]): ∀ (a : Iota), Eq (∀ (Xx B : Iota), in Xx B → in B a → in Xx (setunion a)) True % 4.51/4.72 Clause #80 (by clausification #[79]): ∀ (a a_1 : Iota), Eq (∀ (B : Iota), in a B → in B a_1 → in a (setunion a_1)) True % 4.51/4.72 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 : Iota), Eq (in a a_1 → in a_1 a_2 → in a (setunion a_2)) True % 4.51/4.72 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a a_1) False) (Eq (in a_1 a_2 → in a (setunion a_2)) True) % 4.57/4.73 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a a_1) False) (Or (Eq (in a_1 a_2) False) (Eq (in a (setunion a_2)) True)) % 4.57/4.73 Clause #85 (by superposition #[83, 73]): ∀ (a a_1 a_2 a_3 : Iota), % 4.57/4.73 Or (Eq (in a a_1) False) % 4.57/4.73 (Or (Eq (in (skS.0 8 a a_2 a_3) (setunion a_1)) True) (Or (Eq (subset a a_2) True) (Eq False True))) % 4.57/4.73 Clause #207 (by clausification #[85]): ∀ (a a_1 a_2 a_3 : Iota), % 4.57/4.73 Or (Eq (in a a_1) False) (Or (Eq (in (skS.0 8 a a_2 a_3) (setunion a_1)) True) (Eq (subset a a_2) True)) % 4.57/4.73 Clause #208 (by superposition #[207, 56]): ∀ (a a_1 a_2 a_3 : Iota), % 4.57/4.73 Or (Eq (in (skS.0 8 a a_1 a_2) (setunion (setadjoin a a_3))) True) (Or (Eq (subset a a_1) True) (Eq False True)) % 4.57/4.73 Clause #407 (by clausification #[208]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (in (skS.0 8 a a_1 a_2) (setunion (setadjoin a a_3))) True) (Eq (subset a a_1) True) % 4.57/4.73 Clause #408 (by superposition #[407, 74]): ∀ (a a_1 : Iota), % 4.57/4.73 Or (Eq (subset a (setunion (setadjoin a a_1))) True) % 4.57/4.73 (Or (Eq (subset a (setunion (setadjoin a a_1))) True) (Eq True False)) % 4.57/4.73 Clause #411 (by clausification #[408]): ∀ (a a_1 : Iota), Or (Eq (subset a (setunion (setadjoin a a_1))) True) (Eq (subset a (setunion (setadjoin a a_1))) True) % 4.57/4.73 Clause #412 (by eliminate duplicate literals #[411]): ∀ (a a_1 : Iota), Eq (subset a (setunion (setadjoin a a_1))) True % 4.57/4.73 Clause #413 (by superposition #[412, 78]): Eq True False % 4.57/4.73 Clause #414 (by clausification #[413]): False % 4.57/4.73 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------