%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU651^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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:08 PM UTC 2025 % Result : Theorem 4.30s 4.55s % Output : Proof 4.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SEU651^2 : TPTP v9.2.0. Released v3.7.0. % 0.08/0.13 % Command : duper %s % 0.13/0.34 % Computer : n014.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:15:08 EDT 2025 % 0.13/0.34 % CPUTime : % 4.30/4.55 SZS status Theorem for theBenchmark.p % 4.30/4.55 SZS output start Proof for theBenchmark.p % 4.30/4.55 Clause #0 (by assumption #[]): Eq (Eq uniqinunit (∀ (Xx Xy : Iota), in Xx (setadjoin Xy emptyset) → Eq Xx Xy)) True % 4.30/4.55 Clause #1 (by assumption #[]): Eq (Eq secondinupair (∀ (Xx Xy : Iota), in Xy (setadjoin Xx (setadjoin Xy emptyset)))) True % 4.30/4.55 Clause #2 (by assumption #[]): Eq % 4.30/4.55 (Eq setukpairinjR12 % 4.30/4.55 (∀ (Xx Xy : Iota), % 4.30/4.55 Eq Xx Xy → % 4.30/4.55 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 4.30/4.55 (setadjoin (setadjoin Xx emptyset) emptyset))) % 4.30/4.55 True % 4.30/4.55 Clause #3 (by assumption #[]): Eq % 4.30/4.55 (Not % 4.30/4.55 (uniqinunit → % 4.30/4.55 secondinupair → % 4.30/4.55 setukpairinjR12 → % 4.30/4.55 ∀ (Xx Xy Xz Xu : Iota), % 4.30/4.55 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 4.30/4.55 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 4.30/4.55 Eq Xz Xu → Eq Xy Xu)) % 4.30/4.55 True % 4.30/4.55 Clause #4 (by clausification #[0]): Eq uniqinunit (∀ (Xx Xy : Iota), in Xx (setadjoin Xy emptyset) → Eq Xx Xy) % 4.30/4.55 Clause #18 (by clausification #[1]): Eq secondinupair (∀ (Xx Xy : Iota), in Xy (setadjoin Xx (setadjoin Xy emptyset))) % 4.30/4.55 Clause #20 (by clausify Prop equality #[18]): Or (Eq secondinupair False) (Eq (∀ (Xx Xy : Iota), in Xy (setadjoin Xx (setadjoin Xy emptyset))) True) % 4.30/4.55 Clause #22 (by clausification #[2]): Eq setukpairinjR12 % 4.30/4.55 (∀ (Xx Xy : Iota), % 4.30/4.55 Eq Xx Xy → % 4.30/4.55 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 4.30/4.55 (setadjoin (setadjoin Xx emptyset) emptyset)) % 4.30/4.55 Clause #26 (by clausification #[20]): ∀ (a : Iota), Or (Eq secondinupair False) (Eq (∀ (Xy : Iota), in Xy (setadjoin a (setadjoin Xy emptyset))) True) % 4.30/4.55 Clause #27 (by clausification #[26]): ∀ (a a_1 : Iota), Or (Eq secondinupair False) (Eq (in a (setadjoin a_1 (setadjoin a emptyset))) True) % 4.30/4.55 Clause #32 (by clausification #[3]): Eq % 4.30/4.55 (uniqinunit → % 4.30/4.55 secondinupair → % 4.30/4.55 setukpairinjR12 → % 4.30/4.55 ∀ (Xx Xy Xz Xu : Iota), % 4.30/4.55 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 4.30/4.55 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 4.30/4.55 Eq Xz Xu → Eq Xy Xu) % 4.30/4.55 False % 4.30/4.55 Clause #33 (by clausification #[32]): Eq uniqinunit True % 4.30/4.55 Clause #34 (by clausification #[32]): Eq % 4.30/4.55 (secondinupair → % 4.30/4.55 setukpairinjR12 → % 4.30/4.55 ∀ (Xx Xy Xz Xu : Iota), % 4.30/4.55 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 4.30/4.55 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 4.30/4.55 Eq Xz Xu → Eq Xy Xu) % 4.30/4.55 False % 4.30/4.55 Clause #35 (by backward demodulation #[33, 4]): Eq True (∀ (Xx Xy : Iota), in Xx (setadjoin Xy emptyset) → Eq Xx Xy) % 4.30/4.55 Clause #38 (by clausification #[35]): ∀ (a : Iota), Eq (∀ (Xy : Iota), in a (setadjoin Xy emptyset) → Eq a Xy) True % 4.30/4.55 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), Eq (in a (setadjoin a_1 emptyset) → Eq a a_1) True % 4.30/4.55 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), Or (Eq (in a (setadjoin a_1 emptyset)) False) (Eq (Eq a a_1) True) % 4.30/4.55 Clause #41 (by clausification #[40]): ∀ (a a_1 : Iota), Or (Eq (in a (setadjoin a_1 emptyset)) False) (Eq a a_1) % 4.30/4.55 Clause #44 (by clausification #[34]): Eq secondinupair True % 4.30/4.55 Clause #45 (by clausification #[34]): Eq % 4.30/4.55 (setukpairinjR12 → % 4.30/4.55 ∀ (Xx Xy Xz Xu : Iota), % 4.30/4.55 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 4.30/4.55 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 4.30/4.55 Eq Xz Xu → Eq Xy Xu) % 4.30/4.55 False % 4.30/4.55 Clause #47 (by backward demodulation #[44, 27]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (in a (setadjoin a_1 (setadjoin a emptyset))) True) % 4.30/4.55 Clause #49 (by clausification #[47]): ∀ (a a_1 : Iota), Eq (in a (setadjoin a_1 (setadjoin a emptyset))) True % 4.30/4.55 Clause #51 (by clausification #[45]): Eq setukpairinjR12 True % 4.40/4.57 Clause #52 (by clausification #[45]): Eq % 4.40/4.57 (∀ (Xx Xy Xz Xu : Iota), % 4.40/4.57 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 4.40/4.57 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 4.40/4.57 Eq Xz Xu → Eq Xy Xu) % 4.40/4.57 False % 4.40/4.57 Clause #53 (by backward demodulation #[51, 22]): Eq True % 4.40/4.57 (∀ (Xx Xy : Iota), % 4.40/4.57 Eq Xx Xy → % 4.40/4.57 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 4.40/4.57 (setadjoin (setadjoin Xx emptyset) emptyset)) % 4.40/4.57 Clause #62 (by clausification #[52]): ∀ (a : Iota), % 4.40/4.57 Eq % 4.40/4.57 (Not % 4.40/4.57 (∀ (Xy Xz Xu : Iota), % 4.40/4.57 Eq % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) (setadjoin Xy emptyset)) emptyset)) % 4.40/4.57 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 4.40/4.57 Eq Xz Xu → Eq Xy Xu)) % 4.40/4.57 True % 4.40/4.57 Clause #63 (by clausification #[62]): ∀ (a : Iota), % 4.40/4.57 Eq % 4.40/4.57 (∀ (Xy Xz Xu : Iota), % 4.40/4.57 Eq % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) (setadjoin Xy emptyset)) emptyset)) % 4.40/4.57 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 4.40/4.57 Eq Xz Xu → Eq Xy Xu) % 4.40/4.57 False % 4.40/4.57 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), % 4.40/4.57 Eq % 4.40/4.57 (Not % 4.40/4.57 (∀ (Xz Xu : Iota), % 4.40/4.57 Eq % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.57 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 4.40/4.57 Eq Xz Xu → Eq (skS.0 7 a a_1) Xu)) % 4.40/4.57 True % 4.40/4.57 Clause #65 (by clausification #[64]): ∀ (a a_1 : Iota), % 4.40/4.57 Eq % 4.40/4.57 (∀ (Xz Xu : Iota), % 4.40/4.57 Eq % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.57 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 4.40/4.57 Eq Xz Xu → Eq (skS.0 7 a a_1) Xu) % 4.40/4.57 False % 4.40/4.57 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 : Iota), % 4.40/4.57 Eq % 4.40/4.57 (Not % 4.40/4.57 (∀ (Xu : Iota), % 4.40/4.57 Eq % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.57 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) (setadjoin Xu emptyset)) emptyset)) → % 4.40/4.57 Eq (skS.0 8 a a_1 a_2) Xu → Eq (skS.0 7 a a_1) Xu)) % 4.40/4.57 True % 4.40/4.57 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 : Iota), % 4.40/4.57 Eq % 4.40/4.57 (∀ (Xu : Iota), % 4.40/4.57 Eq % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.57 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) (setadjoin Xu emptyset)) emptyset)) → % 4.40/4.57 Eq (skS.0 8 a a_1 a_2) Xu → Eq (skS.0 7 a a_1) Xu) % 4.40/4.57 False % 4.40/4.57 Clause #68 (by clausification #[67]): ∀ (a a_1 a_2 a_3 : Iota), % 4.40/4.57 Eq % 4.40/4.57 (Not % 4.40/4.57 (Eq % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.57 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) (setadjoin (skS.0 9 a a_1 a_2 a_3) emptyset)) emptyset)) → % 4.40/4.57 Eq (skS.0 8 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3) → Eq (skS.0 7 a a_1) (skS.0 9 a a_1 a_2 a_3))) % 4.40/4.57 True % 4.40/4.57 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 a_3 : Iota), % 4.40/4.57 Eq % 4.40/4.57 (Eq % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.57 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) % 4.40/4.57 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) (setadjoin (skS.0 9 a a_1 a_2 a_3) emptyset)) emptyset)) → % 4.40/4.59 Eq (skS.0 8 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3) → Eq (skS.0 7 a a_1) (skS.0 9 a a_1 a_2 a_3)) % 4.40/4.59 False % 4.40/4.59 Clause #70 (by clausification #[69]): ∀ (a a_1 a_2 a_3 : Iota), % 4.40/4.59 Eq % 4.40/4.59 (Eq % 4.40/4.59 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.59 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.59 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) % 4.40/4.59 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) (setadjoin (skS.0 9 a a_1 a_2 a_3) emptyset)) emptyset))) % 4.40/4.59 True % 4.40/4.59 Clause #71 (by clausification #[69]): ∀ (a a_1 a_2 a_3 : Iota), % 4.40/4.59 Eq (Eq (skS.0 8 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3) → Eq (skS.0 7 a a_1) (skS.0 9 a a_1 a_2 a_3)) False % 4.40/4.59 Clause #72 (by clausification #[70]): ∀ (a a_1 a_2 a_3 : Iota), % 4.40/4.59 Eq % 4.40/4.59 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.59 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.59 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) % 4.40/4.59 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) (setadjoin (skS.0 9 a a_1 a_2 a_3) emptyset)) emptyset)) % 4.40/4.59 Clause #74 (by clausification #[53]): ∀ (a : Iota), % 4.40/4.59 Eq % 4.40/4.59 (∀ (Xy : Iota), % 4.40/4.59 Eq a Xy → % 4.40/4.59 Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin Xy emptyset)) emptyset)) % 4.40/4.59 (setadjoin (setadjoin a emptyset) emptyset)) % 4.40/4.59 True % 4.40/4.59 Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota), % 4.40/4.59 Eq % 4.40/4.59 (Eq a a_1 → % 4.40/4.59 Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 4.40/4.59 (setadjoin (setadjoin a emptyset) emptyset)) % 4.40/4.59 True % 4.40/4.59 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), % 4.40/4.59 Or (Eq (Eq a a_1) False) % 4.40/4.59 (Eq % 4.40/4.59 (Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 4.40/4.59 (setadjoin (setadjoin a emptyset) emptyset)) % 4.40/4.59 True) % 4.40/4.59 Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota), % 4.40/4.59 Or % 4.40/4.59 (Eq % 4.40/4.59 (Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 4.40/4.59 (setadjoin (setadjoin a emptyset) emptyset)) % 4.40/4.59 True) % 4.40/4.59 (Ne a a_1) % 4.40/4.59 Clause #78 (by clausification #[77]): ∀ (a a_1 : Iota), % 4.40/4.59 Or (Ne a a_1) % 4.40/4.59 (Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 4.40/4.59 (setadjoin (setadjoin a emptyset) emptyset)) % 4.40/4.59 Clause #79 (by destructive equality resolution #[78]): ∀ (a : Iota), % 4.40/4.59 Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a emptyset)) emptyset)) % 4.40/4.59 (setadjoin (setadjoin a emptyset) emptyset) % 4.40/4.59 Clause #80 (by superposition #[79, 49]): ∀ (a : Iota), Eq (in (setadjoin a (setadjoin a emptyset)) (setadjoin (setadjoin a emptyset) emptyset)) True % 4.40/4.59 Clause #81 (by superposition #[80, 41]): ∀ (a : Iota), Or (Eq True False) (Eq (setadjoin a (setadjoin a emptyset)) (setadjoin a emptyset)) % 4.40/4.59 Clause #82 (by clausification #[81]): ∀ (a : Iota), Eq (setadjoin a (setadjoin a emptyset)) (setadjoin a emptyset) % 4.40/4.59 Clause #93 (by clausification #[71]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Eq (skS.0 8 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3)) True % 4.40/4.59 Clause #94 (by clausification #[71]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Eq (skS.0 7 a a_1) (skS.0 9 a a_1 a_2 a_3)) False % 4.40/4.59 Clause #95 (by clausification #[93]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 8 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3) % 4.40/4.59 Clause #96 (by backward demodulation #[95, 72]): ∀ (a a_1 a_2 : Iota), % 4.40/4.59 Eq % 4.40/4.59 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.59 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.59 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) % 4.40/4.59 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) (setadjoin (skS.0 8 a a_1 a_2) emptyset)) emptyset)) % 4.40/4.59 Clause #97 (by clausification #[94]): ∀ (a a_1 a_2 a_3 : Iota), Ne (skS.0 7 a a_1) (skS.0 9 a a_1 a_2 a_3) % 4.40/4.59 Clause #98 (by forward demodulation #[97, 95]): ∀ (a a_1 a_2 : Iota), Ne (skS.0 7 a a_1) (skS.0 8 a a_1 a_2) % 4.40/4.59 Clause #103 (by forward demodulation #[96, 82]): ∀ (a a_1 a_2 : Iota), % 4.40/4.59 Eq % 4.40/4.59 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.59 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.60 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) emptyset)) % 4.40/4.60 Clause #104 (by forward demodulation #[103, 82]): ∀ (a a_1 a_2 : Iota), % 4.40/4.60 Eq % 4.40/4.60 (setadjoin (setadjoin (skS.0 6 a) emptyset) % 4.40/4.60 (setadjoin (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) emptyset)) % 4.40/4.60 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) emptyset) % 4.40/4.60 Clause #106 (by superposition #[104, 104]): ∀ (a a_1 a_2 a_3 : Iota), % 4.40/4.60 Eq (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) emptyset) % 4.40/4.60 (setadjoin (setadjoin (skS.0 8 a a_1 a_3) emptyset) emptyset) % 4.40/4.60 Clause #107 (by superposition #[104, 49]): ∀ (a a_1 a_2 : Iota), % 4.40/4.60 Eq % 4.40/4.60 (in (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) % 4.40/4.60 (setadjoin (setadjoin (skS.0 8 a a_1 a_2) emptyset) emptyset)) % 4.40/4.60 True % 4.40/4.60 Clause #111 (by superposition #[106, 41]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 4.40/4.60 Or (Eq (in a (setadjoin (setadjoin (skS.0 8 a_1 a_2 a_3) emptyset) emptyset)) False) % 4.40/4.60 (Eq a (setadjoin (skS.0 8 a_1 a_2 a_4) emptyset)) % 4.40/4.60 Clause #126 (by superposition #[111, 107]): ∀ (a a_1 a_2 : Iota), % 4.40/4.60 Or (Eq (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) (setadjoin (skS.0 8 a a_1 a_2) emptyset)) % 4.40/4.60 (Eq False True) % 4.40/4.60 Clause #127 (by clausification #[126]): ∀ (a a_1 a_2 : Iota), % 4.40/4.60 Eq (setadjoin (skS.0 6 a) (setadjoin (skS.0 7 a a_1) emptyset)) (setadjoin (skS.0 8 a a_1 a_2) emptyset) % 4.40/4.60 Clause #130 (by superposition #[127, 49]): ∀ (a a_1 a_2 : Iota), Eq (in (skS.0 7 a a_1) (setadjoin (skS.0 8 a a_1 a_2) emptyset)) True % 4.40/4.60 Clause #142 (by superposition #[130, 41]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (skS.0 7 a a_1) (skS.0 8 a a_1 a_2)) % 4.40/4.60 Clause #144 (by clausification #[142]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 7 a a_1) (skS.0 8 a a_1 a_2) % 4.40/4.60 Clause #145 (by forward contextual literal cutting #[144, 98]): False % 4.40/4.60 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------