%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU653^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.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 7.65s 7.82s % Output : Proof 7.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SEU653^2 : TPTP v9.2.0. Released v3.7.0. % 0.08/0.13 % Command : duper %s % 0.12/0.34 % Computer : n010.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Oct 3 05:44:23 EDT 2025 % 0.12/0.34 % CPUTime : % 7.65/7.82 SZS status Theorem for theBenchmark.p % 7.65/7.82 SZS output start Proof for theBenchmark.p % 7.65/7.82 Clause #0 (by assumption #[]): Eq (Eq secondinupair (∀ (Xx Xy : Iota), in Xy (setadjoin Xx (setadjoin Xy emptyset)))) True % 7.65/7.82 Clause #1 (by assumption #[]): Eq (Eq upairset2E (∀ (Xx Xy Xz : Iota), in Xz (setadjoin Xx (setadjoin Xy emptyset)) → Or (Eq Xz Xx) (Eq Xz Xy))) True % 7.65/7.82 Clause #2 (by assumption #[]): Eq % 7.65/7.82 (Eq setukpairinjL2 % 7.65/7.82 (∀ (Xx Xy Xz Xu : Iota), % 7.65/7.82 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.82 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.82 Eq Xx Xz)) % 7.65/7.82 True % 7.65/7.82 Clause #3 (by assumption #[]): Eq % 7.65/7.82 (Eq setukpairinjR1 % 7.65/7.82 (∀ (Xx Xy Xz Xu : Iota), % 7.65/7.82 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.82 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.82 Eq Xz Xu → Eq Xy Xu)) % 7.65/7.82 True % 7.65/7.82 Clause #4 (by assumption #[]): Eq % 7.65/7.82 (Eq upairequniteq (∀ (Xx Xy Xz : Iota), Eq (setadjoin Xx (setadjoin Xy emptyset)) (setadjoin Xz emptyset) → Eq Xx Xy)) % 7.65/7.82 True % 7.65/7.82 Clause #5 (by assumption #[]): Eq % 7.65/7.82 (Not % 7.65/7.82 (secondinupair → % 7.65/7.82 upairset2E → % 7.65/7.82 setukpairinjL2 → % 7.65/7.82 setukpairinjR1 → % 7.65/7.82 upairequniteq → % 7.65/7.82 ∀ (Xx Xy Xz Xu : Iota), % 7.65/7.82 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.82 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.82 Eq Xy Xu)) % 7.65/7.82 True % 7.65/7.82 Clause #6 (by clausification #[4]): Eq upairequniteq (∀ (Xx Xy Xz : Iota), Eq (setadjoin Xx (setadjoin Xy emptyset)) (setadjoin Xz emptyset) → Eq Xx Xy) % 7.65/7.82 Clause #26 (by clausification #[2]): Eq setukpairinjL2 % 7.65/7.82 (∀ (Xx Xy Xz Xu : Iota), % 7.65/7.82 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.82 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.82 Eq Xx Xz) % 7.65/7.82 Clause #30 (by clausification #[0]): Eq secondinupair (∀ (Xx Xy : Iota), in Xy (setadjoin Xx (setadjoin Xy emptyset))) % 7.65/7.82 Clause #32 (by clausify Prop equality #[30]): Or (Eq secondinupair False) (Eq (∀ (Xx Xy : Iota), in Xy (setadjoin Xx (setadjoin Xy emptyset))) True) % 7.65/7.82 Clause #34 (by clausification #[32]): ∀ (a : Iota), Or (Eq secondinupair False) (Eq (∀ (Xy : Iota), in Xy (setadjoin a (setadjoin Xy emptyset))) True) % 7.65/7.82 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), Or (Eq secondinupair False) (Eq (in a (setadjoin a_1 (setadjoin a emptyset))) True) % 7.65/7.82 Clause #58 (by clausification #[1]): Eq upairset2E (∀ (Xx Xy Xz : Iota), in Xz (setadjoin Xx (setadjoin Xy emptyset)) → Or (Eq Xz Xx) (Eq Xz Xy)) % 7.65/7.82 Clause #62 (by clausification #[3]): Eq setukpairinjR1 % 7.65/7.82 (∀ (Xx Xy Xz Xu : Iota), % 7.65/7.82 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.82 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.82 Eq Xz Xu → Eq Xy Xu) % 7.65/7.82 Clause #87 (by clausification #[5]): Eq % 7.65/7.82 (secondinupair → % 7.65/7.82 upairset2E → % 7.65/7.82 setukpairinjL2 → % 7.65/7.82 setukpairinjR1 → % 7.65/7.82 upairequniteq → % 7.65/7.82 ∀ (Xx Xy Xz Xu : Iota), % 7.65/7.82 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.82 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.82 Eq Xy Xu) % 7.65/7.82 False % 7.65/7.82 Clause #88 (by clausification #[87]): Eq secondinupair True % 7.65/7.82 Clause #89 (by clausification #[87]): Eq % 7.65/7.82 (upairset2E → % 7.65/7.82 setukpairinjL2 → % 7.65/7.82 setukpairinjR1 → % 7.65/7.82 upairequniteq → % 7.65/7.82 ∀ (Xx Xy Xz Xu : Iota), % 7.65/7.82 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.82 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.86 Eq Xy Xu) % 7.65/7.86 False % 7.65/7.86 Clause #91 (by backward demodulation #[88, 35]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (in a (setadjoin a_1 (setadjoin a emptyset))) True) % 7.65/7.86 Clause #93 (by clausification #[91]): ∀ (a a_1 : Iota), Eq (in a (setadjoin a_1 (setadjoin a emptyset))) True % 7.65/7.86 Clause #99 (by clausification #[89]): Eq upairset2E True % 7.65/7.86 Clause #100 (by clausification #[89]): Eq % 7.65/7.86 (setukpairinjL2 → % 7.65/7.86 setukpairinjR1 → % 7.65/7.86 upairequniteq → % 7.65/7.86 ∀ (Xx Xy Xz Xu : Iota), % 7.65/7.86 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.86 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.86 Eq Xy Xu) % 7.65/7.86 False % 7.65/7.86 Clause #101 (by backward demodulation #[99, 58]): Eq True (∀ (Xx Xy Xz : Iota), in Xz (setadjoin Xx (setadjoin Xy emptyset)) → Or (Eq Xz Xx) (Eq Xz Xy)) % 7.65/7.86 Clause #102 (by clausification #[100]): Eq setukpairinjL2 True % 7.65/7.86 Clause #103 (by clausification #[100]): Eq % 7.65/7.86 (setukpairinjR1 → % 7.65/7.86 upairequniteq → % 7.65/7.86 ∀ (Xx Xy Xz Xu : Iota), % 7.65/7.86 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.86 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.86 Eq Xy Xu) % 7.65/7.86 False % 7.65/7.86 Clause #104 (by backward demodulation #[102, 26]): Eq True % 7.65/7.86 (∀ (Xx Xy Xz Xu : Iota), % 7.65/7.86 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.86 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.86 Eq Xx Xz) % 7.65/7.86 Clause #107 (by clausification #[104]): ∀ (a : Iota), % 7.65/7.86 Eq % 7.65/7.86 (∀ (Xy Xz Xu : Iota), % 7.65/7.86 Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin Xy emptyset)) emptyset)) % 7.65/7.86 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.86 Eq a Xz) % 7.65/7.86 True % 7.65/7.86 Clause #108 (by clausification #[107]): ∀ (a a_1 : Iota), % 7.65/7.86 Eq % 7.65/7.86 (∀ (Xz Xu : Iota), % 7.65/7.86 Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.65/7.86 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.86 Eq a Xz) % 7.65/7.86 True % 7.65/7.86 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 : Iota), % 7.65/7.86 Eq % 7.65/7.86 (∀ (Xu : Iota), % 7.65/7.86 Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.65/7.86 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.86 Eq a a_2) % 7.65/7.86 True % 7.65/7.86 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Eq % 7.65/7.86 (Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.65/7.86 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin a_3 emptyset)) emptyset)) → % 7.65/7.86 Eq a a_2) % 7.65/7.86 True % 7.65/7.86 Clause #111 (by clausification #[110]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or % 7.65/7.86 (Eq % 7.65/7.86 (Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.65/7.86 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin a_3 emptyset)) emptyset))) % 7.65/7.86 False) % 7.65/7.86 (Eq (Eq a a_2) True) % 7.65/7.86 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or (Eq (Eq a a_1) True) % 7.65/7.86 (Ne (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_2 emptyset)) emptyset)) % 7.65/7.86 (setadjoin (setadjoin a_1 emptyset) (setadjoin (setadjoin a_1 (setadjoin a_3 emptyset)) emptyset))) % 7.65/7.86 Clause #113 (by clausification #[112]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or % 7.65/7.86 (Ne (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.65/7.86 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin a_3 emptyset)) emptyset))) % 7.65/7.86 (Eq a a_2) % 7.65/7.86 Clause #126 (by clausification #[103]): Eq setukpairinjR1 True % 7.65/7.86 Clause #127 (by clausification #[103]): Eq % 7.65/7.86 (upairequniteq → % 7.65/7.86 ∀ (Xx Xy Xz Xu : Iota), % 7.65/7.86 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.90 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.90 Eq Xy Xu) % 7.65/7.90 False % 7.65/7.90 Clause #128 (by backward demodulation #[126, 62]): Eq True % 7.65/7.90 (∀ (Xx Xy Xz Xu : Iota), % 7.65/7.90 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.65/7.90 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.90 Eq Xz Xu → Eq Xy Xu) % 7.65/7.90 Clause #131 (by clausification #[128]): ∀ (a : Iota), % 7.65/7.90 Eq % 7.65/7.90 (∀ (Xy Xz Xu : Iota), % 7.65/7.90 Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin Xy emptyset)) emptyset)) % 7.65/7.90 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.65/7.90 Eq Xz Xu → Eq Xy Xu) % 7.65/7.90 True % 7.65/7.90 Clause #132 (by clausification #[131]): ∀ (a a_1 : Iota), % 7.65/7.90 Eq % 7.65/7.90 (∀ (Xz Xu : Iota), % 7.65/7.90 Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.73/7.90 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.73/7.90 Eq Xz Xu → Eq a_1 Xu) % 7.73/7.90 True % 7.73/7.90 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), % 7.73/7.90 Eq % 7.73/7.90 (∀ (Xu : Iota), % 7.73/7.90 Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.73/7.90 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin Xu emptyset)) emptyset)) → % 7.73/7.90 Eq a_2 Xu → Eq a_1 Xu) % 7.73/7.90 True % 7.73/7.90 Clause #134 (by clausification #[133]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.90 Eq % 7.73/7.90 (Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.73/7.90 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin a_3 emptyset)) emptyset)) → % 7.73/7.90 Eq a_2 a_3 → Eq a_1 a_3) % 7.73/7.90 True % 7.73/7.90 Clause #135 (by clausification #[134]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.90 Or % 7.73/7.90 (Eq % 7.73/7.90 (Eq (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.73/7.90 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin a_3 emptyset)) emptyset))) % 7.73/7.90 False) % 7.73/7.90 (Eq (Eq a_2 a_3 → Eq a_1 a_3) True) % 7.73/7.90 Clause #136 (by clausification #[135]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.90 Or (Eq (Eq a a_1 → Eq a_2 a_1) True) % 7.73/7.90 (Ne (setadjoin (setadjoin a_3 emptyset) (setadjoin (setadjoin a_3 (setadjoin a_2 emptyset)) emptyset)) % 7.73/7.90 (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset))) % 7.73/7.90 Clause #137 (by clausification #[136]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.90 Or % 7.73/7.90 (Ne (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.73/7.90 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin a_3 emptyset)) emptyset))) % 7.73/7.90 (Or (Eq (Eq a_2 a_3) False) (Eq (Eq a_1 a_3) True)) % 7.73/7.90 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.90 Or % 7.73/7.90 (Ne (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.73/7.90 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin a_3 emptyset)) emptyset))) % 7.73/7.90 (Or (Eq (Eq a_1 a_3) True) (Ne a_2 a_3)) % 7.73/7.90 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.90 Or % 7.73/7.90 (Ne (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.73/7.90 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin a_3 emptyset)) emptyset))) % 7.73/7.90 (Or (Ne a_2 a_3) (Eq a_1 a_3)) % 7.73/7.90 Clause #140 (by destructive equality resolution #[139]): ∀ (a a_1 a_2 : Iota), % 7.73/7.90 Or % 7.73/7.90 (Ne (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.73/7.90 (setadjoin (setadjoin a_2 emptyset) (setadjoin (setadjoin a_2 (setadjoin a_2 emptyset)) emptyset))) % 7.73/7.90 (Eq a_1 a_2) % 7.73/7.90 Clause #145 (by clausification #[127]): Eq upairequniteq True % 7.73/7.90 Clause #146 (by clausification #[127]): Eq % 7.73/7.90 (∀ (Xx Xy Xz Xu : Iota), % 7.73/7.90 Eq (setadjoin (setadjoin Xx emptyset) (setadjoin (setadjoin Xx (setadjoin Xy emptyset)) emptyset)) % 7.73/7.90 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.73/7.92 Eq Xy Xu) % 7.73/7.92 False % 7.73/7.92 Clause #147 (by backward demodulation #[145, 6]): Eq True (∀ (Xx Xy Xz : Iota), Eq (setadjoin Xx (setadjoin Xy emptyset)) (setadjoin Xz emptyset) → Eq Xx Xy) % 7.73/7.92 Clause #151 (by clausification #[147]): ∀ (a : Iota), Eq (∀ (Xy Xz : Iota), Eq (setadjoin a (setadjoin Xy emptyset)) (setadjoin Xz emptyset) → Eq a Xy) True % 7.73/7.92 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), Eq (∀ (Xz : Iota), Eq (setadjoin a (setadjoin a_1 emptyset)) (setadjoin Xz emptyset) → Eq a a_1) True % 7.73/7.92 Clause #153 (by clausification #[152]): ∀ (a a_1 a_2 : Iota), Eq (Eq (setadjoin a (setadjoin a_1 emptyset)) (setadjoin a_2 emptyset) → Eq a a_1) True % 7.73/7.92 Clause #154 (by clausification #[153]): ∀ (a a_1 a_2 : Iota), % 7.73/7.92 Or (Eq (Eq (setadjoin a (setadjoin a_1 emptyset)) (setadjoin a_2 emptyset)) False) (Eq (Eq a a_1) True) % 7.73/7.92 Clause #155 (by clausification #[154]): ∀ (a a_1 a_2 : Iota), Or (Eq (Eq a a_1) True) (Ne (setadjoin a (setadjoin a_1 emptyset)) (setadjoin a_2 emptyset)) % 7.73/7.92 Clause #156 (by clausification #[155]): ∀ (a a_1 a_2 : Iota), Or (Ne (setadjoin a (setadjoin a_1 emptyset)) (setadjoin a_2 emptyset)) (Eq a a_1) % 7.73/7.92 Clause #159 (by clausification #[146]): ∀ (a : Iota), % 7.73/7.92 Eq % 7.73/7.92 (Not % 7.73/7.92 (∀ (Xy Xz Xu : Iota), % 7.73/7.92 Eq % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) (setadjoin Xy emptyset)) emptyset)) % 7.73/7.92 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.73/7.92 Eq Xy Xu)) % 7.73/7.92 True % 7.73/7.92 Clause #160 (by clausification #[159]): ∀ (a : Iota), % 7.73/7.92 Eq % 7.73/7.92 (∀ (Xy Xz Xu : Iota), % 7.73/7.92 Eq % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) (setadjoin Xy emptyset)) emptyset)) % 7.73/7.92 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.73/7.92 Eq Xy Xu) % 7.73/7.92 False % 7.73/7.92 Clause #161 (by clausification #[160]): ∀ (a a_1 : Iota), % 7.73/7.92 Eq % 7.73/7.92 (Not % 7.73/7.92 (∀ (Xz Xu : Iota), % 7.73/7.92 Eq % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.92 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.73/7.92 Eq (skS.0 14 a a_1) Xu)) % 7.73/7.92 True % 7.73/7.92 Clause #162 (by clausification #[161]): ∀ (a a_1 : Iota), % 7.73/7.92 Eq % 7.73/7.92 (∀ (Xz Xu : Iota), % 7.73/7.92 Eq % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.92 (setadjoin (setadjoin Xz emptyset) (setadjoin (setadjoin Xz (setadjoin Xu emptyset)) emptyset)) → % 7.73/7.92 Eq (skS.0 14 a a_1) Xu) % 7.73/7.92 False % 7.73/7.92 Clause #163 (by clausification #[162]): ∀ (a a_1 a_2 : Iota), % 7.73/7.92 Eq % 7.73/7.92 (Not % 7.73/7.92 (∀ (Xu : Iota), % 7.73/7.92 Eq % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.92 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) emptyset) % 7.73/7.92 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) (setadjoin Xu emptyset)) emptyset)) → % 7.73/7.92 Eq (skS.0 14 a a_1) Xu)) % 7.73/7.92 True % 7.73/7.92 Clause #164 (by clausification #[163]): ∀ (a a_1 a_2 : Iota), % 7.73/7.92 Eq % 7.73/7.92 (∀ (Xu : Iota), % 7.73/7.92 Eq % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.92 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) emptyset) % 7.73/7.92 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) (setadjoin Xu emptyset)) emptyset)) → % 7.73/7.92 Eq (skS.0 14 a a_1) Xu) % 7.73/7.92 False % 7.73/7.92 Clause #165 (by clausification #[164]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.92 Eq % 7.73/7.92 (Not % 7.73/7.92 (Eq % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.92 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.92 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) emptyset) % 7.73/7.92 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) (setadjoin (skS.0 16 a a_1 a_2 a_3) emptyset)) emptyset)) → % 7.73/7.94 Eq (skS.0 14 a a_1) (skS.0 16 a a_1 a_2 a_3))) % 7.73/7.94 True % 7.73/7.94 Clause #166 (by clausification #[165]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.94 Eq % 7.73/7.94 (Eq % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.94 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) emptyset) % 7.73/7.94 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) (setadjoin (skS.0 16 a a_1 a_2 a_3) emptyset)) emptyset)) → % 7.73/7.94 Eq (skS.0 14 a a_1) (skS.0 16 a a_1 a_2 a_3)) % 7.73/7.94 False % 7.73/7.94 Clause #167 (by clausification #[166]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.94 Eq % 7.73/7.94 (Eq % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.94 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) emptyset) % 7.73/7.94 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) (setadjoin (skS.0 16 a a_1 a_2 a_3) emptyset)) emptyset))) % 7.73/7.94 True % 7.73/7.94 Clause #168 (by clausification #[166]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Eq (skS.0 14 a a_1) (skS.0 16 a a_1 a_2 a_3)) False % 7.73/7.94 Clause #169 (by clausification #[167]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.94 Eq % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.94 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) emptyset) % 7.73/7.94 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) (setadjoin (skS.0 16 a a_1 a_2 a_3) emptyset)) emptyset)) % 7.73/7.94 Clause #171 (by superposition #[169, 113]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.73/7.94 Or % 7.73/7.94 (Ne (setadjoin (setadjoin a emptyset) (setadjoin (setadjoin a (setadjoin a_1 emptyset)) emptyset)) % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a_2) emptyset) % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a_2) (setadjoin (skS.0 14 a_2 a_3) emptyset)) emptyset))) % 7.73/7.94 (Eq a (skS.0 15 a_2 a_3 a_4)) % 7.73/7.94 Clause #176 (by superposition #[169, 140]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.73/7.94 Or % 7.73/7.94 (Ne % 7.73/7.94 (setadjoin (setadjoin (setadjoin (skS.0 15 a a_1 a_2) emptyset) emptyset) % 7.73/7.94 (setadjoin % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.94 emptyset)) % 7.73/7.94 (setadjoin (setadjoin a_3 emptyset) (setadjoin (setadjoin a_3 (setadjoin a_3 emptyset)) emptyset))) % 7.73/7.94 (Eq (setadjoin (skS.0 15 a a_1 a_2) (setadjoin (skS.0 16 a a_1 a_2 a_4) emptyset)) a_3) % 7.73/7.94 Clause #178 (by clausification #[101]): ∀ (a : Iota), Eq (∀ (Xy Xz : Iota), in Xz (setadjoin a (setadjoin Xy emptyset)) → Or (Eq Xz a) (Eq Xz Xy)) True % 7.73/7.94 Clause #179 (by clausification #[178]): ∀ (a a_1 : Iota), Eq (∀ (Xz : Iota), in Xz (setadjoin a (setadjoin a_1 emptyset)) → Or (Eq Xz a) (Eq Xz a_1)) True % 7.73/7.94 Clause #180 (by clausification #[179]): ∀ (a a_1 a_2 : Iota), Eq (in a (setadjoin a_1 (setadjoin a_2 emptyset)) → Or (Eq a a_1) (Eq a a_2)) True % 7.73/7.94 Clause #181 (by clausification #[180]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setadjoin a_1 (setadjoin a_2 emptyset))) False) (Eq (Or (Eq a a_1) (Eq a a_2)) True) % 7.73/7.94 Clause #182 (by clausification #[181]): ∀ (a a_1 a_2 : Iota), % 7.73/7.94 Or (Eq (in a (setadjoin a_1 (setadjoin a_2 emptyset))) False) (Or (Eq (Eq a a_1) True) (Eq (Eq a a_2) True)) % 7.73/7.94 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setadjoin a_1 (setadjoin a_2 emptyset))) False) (Or (Eq (Eq a a_2) True) (Eq a a_1)) % 7.73/7.94 Clause #184 (by clausification #[183]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setadjoin a_1 (setadjoin a_2 emptyset))) False) (Or (Eq a a_1) (Eq a a_2)) % 7.73/7.94 Clause #207 (by clausification #[168]): ∀ (a a_1 a_2 a_3 : Iota), Ne (skS.0 14 a a_1) (skS.0 16 a a_1 a_2 a_3) % 7.73/7.94 Clause #231 (by equality resolution #[171]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 13 a) (skS.0 15 a a_1 a_2) % 7.73/7.94 Clause #234 (by backward demodulation #[231, 169]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.94 Eq % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.94 (setadjoin (setadjoin (skS.0 15 a a_1 a_2) emptyset) % 7.73/7.94 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 16 a a_1 a_2 a_3) emptyset)) emptyset)) % 7.73/7.97 Clause #243 (by forward demodulation #[234, 231]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.97 Eq % 7.73/7.97 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.97 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) emptyset)) % 7.73/7.97 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.73/7.97 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 16 a a_1 a_2 a_3) emptyset)) emptyset)) % 7.73/7.97 Clause #248 (by superposition #[243, 184]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.73/7.97 Or % 7.73/7.97 (Eq % 7.73/7.97 (in a % 7.73/7.97 (setadjoin (setadjoin (skS.0 13 a_1) emptyset) % 7.73/7.97 (setadjoin (setadjoin (skS.0 13 a_1) (setadjoin (skS.0 14 a_1 a_2) emptyset)) emptyset))) % 7.73/7.97 False) % 7.73/7.97 (Or (Eq a (setadjoin (skS.0 13 a_1) emptyset)) % 7.73/7.97 (Eq a (setadjoin (skS.0 13 a_1) (setadjoin (skS.0 16 a_1 a_2 a_3 a_4) emptyset)))) % 7.73/7.97 Clause #251 (by superposition #[248, 93]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.97 Or (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset)) % 7.73/7.97 (Or % 7.73/7.97 (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) % 7.73/7.97 (setadjoin (skS.0 13 a) (setadjoin (skS.0 16 a a_1 a_2 a_3) emptyset))) % 7.73/7.97 (Eq False True)) % 7.73/7.97 Clause #252 (by clausification #[251]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.97 Or (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset)) % 7.73/7.97 (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) % 7.73/7.97 (setadjoin (skS.0 13 a) (setadjoin (skS.0 16 a a_1 a_2 a_3) emptyset))) % 7.73/7.97 Clause #254 (by superposition #[252, 93]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.97 Or (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset)) % 7.73/7.97 (Eq (in (skS.0 16 a a_1 a_2 a_3) (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset))) True) % 7.73/7.97 Clause #259 (by superposition #[252, 184]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.73/7.97 Or (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset)) % 7.73/7.97 (Or (Eq (in a_2 (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset))) False) % 7.73/7.97 (Or (Eq a_2 (skS.0 13 a)) (Eq a_2 (skS.0 16 a a_1 a_3 a_4)))) % 7.73/7.97 Clause #261 (by superposition #[254, 184]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.97 Or (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset)) % 7.73/7.97 (Or (Eq True False) (Or (Eq (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a)) (Eq (skS.0 16 a a_1 a_2 a_3) (skS.0 14 a a_1)))) % 7.73/7.97 Clause #262 (by clausification #[261]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.97 Or (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset)) % 7.73/7.97 (Or (Eq (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a)) (Eq (skS.0 16 a a_1 a_2 a_3) (skS.0 14 a a_1))) % 7.73/7.97 Clause #263 (by forward contextual literal cutting #[262, 207]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.97 Or (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset)) % 7.73/7.97 (Eq (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a)) % 7.73/7.97 Clause #274 (by superposition #[263, 207]): ∀ (a a_1 : Iota), % 7.73/7.97 Or (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset)) % 7.73/7.97 (Ne (skS.0 14 a a_1) (skS.0 13 a)) % 7.73/7.97 Clause #316 (by superposition #[259, 93]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.97 Or (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset)) % 7.73/7.97 (Or (Eq (skS.0 14 a a_1) (skS.0 13 a)) (Or (Eq (skS.0 14 a a_1) (skS.0 16 a a_1 a_2 a_3)) (Eq False True))) % 7.73/7.97 Clause #318 (by clausification #[316]): ∀ (a a_1 a_2 a_3 : Iota), % 7.73/7.97 Or (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset)) % 7.73/7.97 (Or (Eq (skS.0 14 a a_1) (skS.0 13 a)) (Eq (skS.0 14 a a_1) (skS.0 16 a a_1 a_2 a_3))) % 7.73/7.97 Clause #319 (by forward contextual literal cutting #[318, 156]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (skS.0 14 a a_1) (skS.0 13 a)) (Eq (skS.0 14 a a_1) (skS.0 16 a a_1 a_2 a_3)) % 7.73/7.97 Clause #320 (by forward contextual literal cutting #[319, 207]): ∀ (a a_1 : Iota), Eq (skS.0 14 a a_1) (skS.0 13 a) % 7.73/7.97 Clause #321 (by backward demodulation #[320, 207]): ∀ (a a_1 a_2 a_3 : Iota), Ne (skS.0 13 a) (skS.0 16 a a_1 a_2 a_3) % 7.81/7.99 Clause #342 (by backward contextual literal cutting #[320, 274]): ∀ (a a_1 : Iota), Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 14 a a_1) emptyset)) (setadjoin (skS.0 13 a) emptyset) % 7.81/7.99 Clause #347 (by forward demodulation #[342, 320]): ∀ (a : Iota), Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 13 a) emptyset)) (setadjoin (skS.0 13 a) emptyset) % 7.81/7.99 Clause #351 (by superposition #[347, 184]): ∀ (a a_1 : Iota), % 7.81/7.99 Or (Eq (in a (setadjoin (skS.0 13 a_1) emptyset)) False) (Or (Eq a (skS.0 13 a_1)) (Eq a (skS.0 13 a_1))) % 7.81/7.99 Clause #352 (by eliminate duplicate literals #[351]): ∀ (a a_1 : Iota), Or (Eq (in a (setadjoin (skS.0 13 a_1) emptyset)) False) (Eq a (skS.0 13 a_1)) % 7.81/7.99 Clause #354 (by forward demodulation #[176, 320]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.81/7.99 Or % 7.81/7.99 (Ne % 7.81/7.99 (setadjoin (setadjoin (setadjoin (skS.0 15 a a_1 a_2) emptyset) emptyset) % 7.81/7.99 (setadjoin % 7.81/7.99 (setadjoin (setadjoin (skS.0 13 a) emptyset) % 7.81/7.99 (setadjoin (setadjoin (skS.0 13 a) (setadjoin (skS.0 13 a) emptyset)) emptyset)) % 7.81/7.99 emptyset)) % 7.81/7.99 (setadjoin (setadjoin a_3 emptyset) (setadjoin (setadjoin a_3 (setadjoin a_3 emptyset)) emptyset))) % 7.81/7.99 (Eq (setadjoin (skS.0 15 a a_1 a_2) (setadjoin (skS.0 16 a a_1 a_2 a_4) emptyset)) a_3) % 7.81/7.99 Clause #355 (by forward demodulation #[354, 347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.81/7.99 Or % 7.81/7.99 (Ne % 7.81/7.99 (setadjoin (setadjoin (setadjoin (skS.0 15 a a_1 a_2) emptyset) emptyset) % 7.81/7.99 (setadjoin (setadjoin (setadjoin (skS.0 13 a) emptyset) (setadjoin (setadjoin (skS.0 13 a) emptyset) emptyset)) % 7.81/7.99 emptyset)) % 7.81/7.99 (setadjoin (setadjoin a_3 emptyset) (setadjoin (setadjoin a_3 (setadjoin a_3 emptyset)) emptyset))) % 7.81/7.99 (Eq (setadjoin (skS.0 15 a a_1 a_2) (setadjoin (skS.0 16 a a_1 a_2 a_4) emptyset)) a_3) % 7.81/7.99 Clause #356 (by forward demodulation #[355, 231]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.81/7.99 Or % 7.81/7.99 (Ne % 7.81/7.99 (setadjoin (setadjoin (setadjoin (skS.0 13 a) emptyset) emptyset) % 7.81/7.99 (setadjoin (setadjoin (setadjoin (skS.0 13 a) emptyset) (setadjoin (setadjoin (skS.0 13 a) emptyset) emptyset)) % 7.81/7.99 emptyset)) % 7.81/7.99 (setadjoin (setadjoin a_1 emptyset) (setadjoin (setadjoin a_1 (setadjoin a_1 emptyset)) emptyset))) % 7.81/7.99 (Eq (setadjoin (skS.0 15 a a_2 a_3) (setadjoin (skS.0 16 a a_2 a_3 a_4) emptyset)) a_1) % 7.81/7.99 Clause #357 (by forward demodulation #[356, 231]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.81/7.99 Or % 7.81/7.99 (Ne % 7.81/7.99 (setadjoin (setadjoin (setadjoin (skS.0 13 a) emptyset) emptyset) % 7.81/7.99 (setadjoin (setadjoin (setadjoin (skS.0 13 a) emptyset) (setadjoin (setadjoin (skS.0 13 a) emptyset) emptyset)) % 7.81/7.99 emptyset)) % 7.81/7.99 (setadjoin (setadjoin a_1 emptyset) (setadjoin (setadjoin a_1 (setadjoin a_1 emptyset)) emptyset))) % 7.81/7.99 (Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 16 a a_2 a_3 a_4) emptyset)) a_1) % 7.81/7.99 Clause #358 (by equality resolution #[357]): ∀ (a a_1 a_2 a_3 : Iota), % 7.81/7.99 Eq (setadjoin (skS.0 13 a) (setadjoin (skS.0 16 a a_1 a_2 a_3) emptyset)) (setadjoin (skS.0 13 a) emptyset) % 7.81/7.99 Clause #362 (by superposition #[358, 93]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 16 a a_1 a_2 a_3) (setadjoin (skS.0 13 a) emptyset)) True % 7.81/7.99 Clause #365 (by superposition #[362, 352]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a)) % 7.81/7.99 Clause #366 (by clausification #[365]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) % 7.81/7.99 Clause #367 (by forward contextual literal cutting #[366, 321]): False % 7.81/7.99 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------