%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU709^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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:15 PM UTC 2025 % Result : Theorem 182.44s 182.68s % Output : Proof 182.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU709^2 : TPTP v9.2.0. Released v3.7.0. % 0.11/0.14 % Command : duper %s % 0.15/0.35 % Computer : n019.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Fri Oct 3 05:42:38 EDT 2025 % 0.15/0.35 % CPUTime : % 182.44/182.68 SZS status Theorem for theBenchmark.p % 182.44/182.68 SZS output start Proof for theBenchmark.p % 182.44/182.68 Clause #0 (by assumption #[]): Eq (Eq setadjoinIL (∀ (Xx Xy : Iota), in Xx (setadjoin Xx Xy))) True % 182.44/182.68 Clause #2 (by assumption #[]): Eq (Eq secondinupair (∀ (Xx Xy : Iota), in Xy (setadjoin Xx (setadjoin Xy emptyset)))) True % 182.44/182.68 Clause #3 (by assumption #[]): Eq % 182.44/182.68 (Eq iftrue % 182.44/182.68 (∀ (A : Iota) (Xphi : Prop) (Xx : Iota), in Xx A → ∀ (Xy : Iota), in Xy A → Xphi → Eq (if A Xphi Xx Xy) Xx)) % 182.44/182.68 True % 182.44/182.68 Clause #4 (by assumption #[]): Eq % 182.44/182.68 (Eq iffalse % 182.44/182.68 (∀ (A : Iota) (Xphi : Prop) (Xx : Iota), in Xx A → ∀ (Xy : Iota), in Xy A → Not Xphi → Eq (if A Xphi Xx Xy) Xy)) % 182.44/182.68 True % 182.44/182.68 Clause #5 (by assumption #[]): Eq % 182.44/182.68 (Not % 182.44/182.68 (setadjoinIL → % 182.44/182.68 in__Cong → % 182.44/182.68 secondinupair → % 182.44/182.68 iftrue → % 182.44/182.68 iffalse → % 182.44/182.68 ∀ (A : Iota) (Xphi : Prop) (Xx : Iota), % 182.44/182.68 in Xx A → ∀ (Xy : Iota), in Xy A → in (if A Xphi Xx Xy) (setadjoin Xx (setadjoin Xy emptyset)))) % 182.44/182.68 True % 182.44/182.68 Clause #6 (by clausification #[0]): Eq setadjoinIL (∀ (Xx Xy : Iota), in Xx (setadjoin Xx Xy)) % 182.44/182.68 Clause #8 (by clausify Prop equality #[6]): Or (Eq setadjoinIL False) (Eq (∀ (Xx Xy : Iota), in Xx (setadjoin Xx Xy)) True) % 182.44/182.68 Clause #10 (by clausification #[8]): ∀ (a : Iota), Or (Eq setadjoinIL False) (Eq (∀ (Xy : Iota), in a (setadjoin a Xy)) True) % 182.44/182.68 Clause #11 (by clausification #[10]): ∀ (a a_1 : Iota), Or (Eq setadjoinIL False) (Eq (in a (setadjoin a a_1)) True) % 182.44/182.68 Clause #16 (by clausification #[2]): Eq secondinupair (∀ (Xx Xy : Iota), in Xy (setadjoin Xx (setadjoin Xy emptyset))) % 182.44/182.68 Clause #18 (by clausify Prop equality #[16]): Or (Eq secondinupair False) (Eq (∀ (Xx Xy : Iota), in Xy (setadjoin Xx (setadjoin Xy emptyset))) True) % 182.44/182.68 Clause #24 (by clausification #[18]): ∀ (a : Iota), Or (Eq secondinupair False) (Eq (∀ (Xy : Iota), in Xy (setadjoin a (setadjoin Xy emptyset))) True) % 182.44/182.68 Clause #25 (by clausification #[24]): ∀ (a a_1 : Iota), Or (Eq secondinupair False) (Eq (in a (setadjoin a_1 (setadjoin a emptyset))) True) % 182.44/182.68 Clause #44 (by clausification #[3]): Eq iftrue (∀ (A : Iota) (Xphi : Prop) (Xx : Iota), in Xx A → ∀ (Xy : Iota), in Xy A → Xphi → Eq (if A Xphi Xx Xy) Xx) % 182.44/182.68 Clause #77 (by clausification #[4]): Eq iffalse % 182.44/182.68 (∀ (A : Iota) (Xphi : Prop) (Xx : Iota), in Xx A → ∀ (Xy : Iota), in Xy A → Not Xphi → Eq (if A Xphi Xx Xy) Xy) % 182.44/182.68 Clause #79 (by clausify Prop equality #[77]): Or (Eq iffalse False) % 182.44/182.68 (Eq (∀ (A : Iota) (Xphi : Prop) (Xx : Iota), in Xx A → ∀ (Xy : Iota), in Xy A → Not Xphi → Eq (if A Xphi Xx Xy) Xy) % 182.44/182.68 True) % 182.44/182.68 Clause #81 (by clausification #[5]): Eq % 182.44/182.68 (setadjoinIL → % 182.44/182.68 in__Cong → % 182.44/182.68 secondinupair → % 182.44/182.68 iftrue → % 182.44/182.68 iffalse → % 182.44/182.68 ∀ (A : Iota) (Xphi : Prop) (Xx : Iota), % 182.44/182.68 in Xx A → ∀ (Xy : Iota), in Xy A → in (if A Xphi Xx Xy) (setadjoin Xx (setadjoin Xy emptyset))) % 182.44/182.68 False % 182.44/182.68 Clause #82 (by clausification #[81]): Eq setadjoinIL True % 182.44/182.68 Clause #83 (by clausification #[81]): Eq % 182.44/182.68 (in__Cong → % 182.44/182.68 secondinupair → % 182.44/182.68 iftrue → % 182.44/182.68 iffalse → % 182.44/182.68 ∀ (A : Iota) (Xphi : Prop) (Xx : Iota), % 182.44/182.68 in Xx A → ∀ (Xy : Iota), in Xy A → in (if A Xphi Xx Xy) (setadjoin Xx (setadjoin Xy emptyset))) % 182.44/182.68 False % 182.44/182.68 Clause #85 (by backward demodulation #[82, 11]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (in a (setadjoin a a_1)) True) % 182.44/182.68 Clause #87 (by clausification #[85]): ∀ (a a_1 : Iota), Eq (in a (setadjoin a a_1)) True % 182.44/182.68 Clause #89 (by clausification #[79]): ∀ (a : Iota), % 182.44/182.68 Or (Eq iffalse False) % 182.44/182.68 (Eq (∀ (Xphi : Prop) (Xx : Iota), in Xx a → ∀ (Xy : Iota), in Xy a → Not Xphi → Eq (if a Xphi Xx Xy) Xy) True) % 182.44/182.68 Clause #90 (by clausification #[89]): ∀ (a : Iota) (a_1 : Prop), % 182.44/182.68 Or (Eq iffalse False) (Eq (∀ (Xx : Iota), in Xx a → ∀ (Xy : Iota), in Xy a → Not a_1 → Eq (if a a_1 Xx Xy) Xy) True) % 182.44/182.68 Clause #91 (by clausification #[90]): ∀ (a a_1 : Iota) (a_2 : Prop), % 182.44/182.68 Or (Eq iffalse False) (Eq (in a a_1 → ∀ (Xy : Iota), in Xy a_1 → Not a_2 → Eq (if a_1 a_2 a Xy) Xy) True) % 182.44/182.68 Clause #92 (by clausification #[91]): ∀ (a a_1 : Iota) (a_2 : Prop), % 182.44/182.70 Or (Eq iffalse False) % 182.44/182.70 (Or (Eq (in a a_1) False) (Eq (∀ (Xy : Iota), in Xy a_1 → Not a_2 → Eq (if a_1 a_2 a Xy) Xy) True)) % 182.44/182.70 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.70 Or (Eq iffalse False) (Or (Eq (in a a_1) False) (Eq (in a_2 a_1 → Not a_3 → Eq (if a_1 a_3 a a_2) a_2) True)) % 182.44/182.70 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.70 Or (Eq iffalse False) % 182.44/182.70 (Or (Eq (in a a_1) False) (Or (Eq (in a_2 a_1) False) (Eq (Not a_3 → Eq (if a_1 a_3 a a_2) a_2) True))) % 182.44/182.70 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.70 Or (Eq iffalse False) % 182.44/182.70 (Or (Eq (in a a_1) False) % 182.44/182.70 (Or (Eq (in a_2 a_1) False) (Or (Eq (Not a_3) False) (Eq (Eq (if a_1 a_3 a a_2) a_2) True)))) % 182.44/182.70 Clause #96 (by clausification #[95]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.70 Or (Eq iffalse False) % 182.44/182.70 (Or (Eq (in a a_1) False) (Or (Eq (in a_2 a_1) False) (Or (Eq (Eq (if a_1 a_3 a a_2) a_2) True) (Eq a_3 True)))) % 182.44/182.70 Clause #97 (by clausification #[96]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.70 Or (Eq iffalse False) % 182.44/182.70 (Or (Eq (in a a_1) False) (Or (Eq (in a_2 a_1) False) (Or (Eq a_3 True) (Eq (if a_1 a_3 a a_2) a_2)))) % 182.44/182.70 Clause #99 (by identity boolHoist #[97]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.70 Or (Eq iffalse False) % 182.44/182.70 (Or (Eq (in a a_1) False) % 182.44/182.70 (Or (Eq (in a_2 a_1) False) (Or (Eq a_3 True) (Or (Eq (if a_1 False a a_2) a_2) (Eq a_3 True))))) % 182.44/182.70 Clause #112 (by eliminate duplicate literals #[99]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.70 Or (Eq iffalse False) % 182.44/182.70 (Or (Eq (in a a_1) False) (Or (Eq (in a_2 a_1) False) (Or (Eq a_3 True) (Eq (if a_1 False a a_2) a_2)))) % 182.44/182.70 Clause #131 (by clausification #[83]): Eq % 182.44/182.70 (secondinupair → % 182.44/182.70 iftrue → % 182.44/182.70 iffalse → % 182.44/182.70 ∀ (A : Iota) (Xphi : Prop) (Xx : Iota), % 182.44/182.70 in Xx A → ∀ (Xy : Iota), in Xy A → in (if A Xphi Xx Xy) (setadjoin Xx (setadjoin Xy emptyset))) % 182.44/182.70 False % 182.44/182.70 Clause #159 (by clausification #[131]): Eq secondinupair True % 182.44/182.70 Clause #160 (by clausification #[131]): Eq % 182.44/182.70 (iftrue → % 182.44/182.71 iffalse → % 182.44/182.71 ∀ (A : Iota) (Xphi : Prop) (Xx : Iota), % 182.44/182.71 in Xx A → ∀ (Xy : Iota), in Xy A → in (if A Xphi Xx Xy) (setadjoin Xx (setadjoin Xy emptyset))) % 182.44/182.71 False % 182.44/182.71 Clause #162 (by backward demodulation #[159, 25]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (in a (setadjoin a_1 (setadjoin a emptyset))) True) % 182.44/182.71 Clause #164 (by clausification #[162]): ∀ (a a_1 : Iota), Eq (in a (setadjoin a_1 (setadjoin a emptyset))) True % 182.44/182.71 Clause #166 (by clausification #[160]): Eq iftrue True % 182.44/182.71 Clause #167 (by clausification #[160]): Eq % 182.44/182.71 (iffalse → % 182.44/182.71 ∀ (A : Iota) (Xphi : Prop) (Xx : Iota), % 182.44/182.71 in Xx A → ∀ (Xy : Iota), in Xy A → in (if A Xphi Xx Xy) (setadjoin Xx (setadjoin Xy emptyset))) % 182.44/182.71 False % 182.44/182.71 Clause #168 (by backward demodulation #[166, 44]): Eq True (∀ (A : Iota) (Xphi : Prop) (Xx : Iota), in Xx A → ∀ (Xy : Iota), in Xy A → Xphi → Eq (if A Xphi Xx Xy) Xx) % 182.44/182.71 Clause #172 (by clausification #[168]): ∀ (a : Iota), Eq (∀ (Xphi : Prop) (Xx : Iota), in Xx a → ∀ (Xy : Iota), in Xy a → Xphi → Eq (if a Xphi Xx Xy) Xx) True % 182.44/182.71 Clause #173 (by clausification #[172]): ∀ (a : Iota) (a_1 : Prop), Eq (∀ (Xx : Iota), in Xx a → ∀ (Xy : Iota), in Xy a → a_1 → Eq (if a a_1 Xx Xy) Xx) True % 182.44/182.71 Clause #174 (by clausification #[173]): ∀ (a a_1 : Iota) (a_2 : Prop), Eq (in a a_1 → ∀ (Xy : Iota), in Xy a_1 → a_2 → Eq (if a_1 a_2 a Xy) a) True % 182.44/182.71 Clause #175 (by clausification #[174]): ∀ (a a_1 : Iota) (a_2 : Prop), % 182.44/182.71 Or (Eq (in a a_1) False) (Eq (∀ (Xy : Iota), in Xy a_1 → a_2 → Eq (if a_1 a_2 a Xy) a) True) % 182.44/182.71 Clause #176 (by clausification #[175]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), Or (Eq (in a a_1) False) (Eq (in a_2 a_1 → a_3 → Eq (if a_1 a_3 a a_2) a) True) % 182.44/182.71 Clause #177 (by clausification #[176]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.71 Or (Eq (in a a_1) False) (Or (Eq (in a_2 a_1) False) (Eq (a_3 → Eq (if a_1 a_3 a a_2) a) True)) % 182.44/182.71 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.71 Or (Eq (in a a_1) False) (Or (Eq (in a_2 a_1) False) (Or (Eq a_3 False) (Eq (Eq (if a_1 a_3 a a_2) a) True))) % 182.44/182.73 Clause #179 (by clausification #[178]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.73 Or (Eq (in a a_1) False) (Or (Eq (in a_2 a_1) False) (Or (Eq a_3 False) (Eq (if a_1 a_3 a a_2) a))) % 182.44/182.73 Clause #180 (by identity loobHoist #[179]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.73 Or (Eq (in a a_1) False) % 182.44/182.73 (Or (Eq (in a_2 a_1) False) (Or (Eq a_3 False) (Or (Eq (if a_1 True a a_2) a) (Eq a_3 False)))) % 182.44/182.73 Clause #182 (by eliminate duplicate literals #[180]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.73 Or (Eq (in a a_1) False) (Or (Eq (in a_2 a_1) False) (Or (Eq a_3 False) (Eq (if a_1 True a a_2) a))) % 182.44/182.73 Clause #212 (by clausification #[167]): Eq iffalse True % 182.44/182.73 Clause #213 (by clausification #[167]): Eq % 182.44/182.73 (∀ (A : Iota) (Xphi : Prop) (Xx : Iota), % 182.44/182.73 in Xx A → ∀ (Xy : Iota), in Xy A → in (if A Xphi Xx Xy) (setadjoin Xx (setadjoin Xy emptyset))) % 182.44/182.73 False % 182.44/182.73 Clause #215 (by backward demodulation #[212, 112]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.73 Or (Eq True False) % 182.44/182.73 (Or (Eq (in a a_1) False) (Or (Eq (in a_2 a_1) False) (Or (Eq a_3 True) (Eq (if a_1 False a a_2) a_2)))) % 182.44/182.73 Clause #229 (by clausification #[215]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), % 182.44/182.73 Or (Eq (in a a_1) False) (Or (Eq (in a_2 a_1) False) (Or (Eq a_3 True) (Eq (if a_1 False a a_2) a_2))) % 182.44/182.73 Clause #249 (by clausification #[213]): ∀ (a : Iota), % 182.44/182.73 Eq % 182.44/182.73 (Not % 182.44/182.73 (∀ (Xphi : Prop) (Xx : Iota), % 182.44/182.73 in Xx (skS.0 16 a) → % 182.44/182.73 ∀ (Xy : Iota), in Xy (skS.0 16 a) → in (if (skS.0 16 a) Xphi Xx Xy) (setadjoin Xx (setadjoin Xy emptyset)))) % 182.44/182.73 True % 182.44/182.73 Clause #250 (by clausification #[249]): ∀ (a : Iota), % 182.44/182.73 Eq % 182.44/182.73 (∀ (Xphi : Prop) (Xx : Iota), % 182.44/182.73 in Xx (skS.0 16 a) → % 182.44/182.73 ∀ (Xy : Iota), in Xy (skS.0 16 a) → in (if (skS.0 16 a) Xphi Xx Xy) (setadjoin Xx (setadjoin Xy emptyset))) % 182.44/182.73 False % 182.44/182.73 Clause #251 (by clausification #[250]): ∀ (a : Iota) (a_1 : Prop), % 182.44/182.73 Eq % 182.44/182.73 (Not % 182.44/182.73 (∀ (Xx : Iota), % 182.44/182.73 in Xx (skS.0 16 a) → % 182.44/182.73 ∀ (Xy : Iota), % 182.44/182.73 in Xy (skS.0 16 a) → in (if (skS.0 16 a) (skS.0 17 a a_1) Xx Xy) (setadjoin Xx (setadjoin Xy emptyset)))) % 182.44/182.73 True % 182.44/182.73 Clause #252 (by clausification #[251]): ∀ (a : Iota) (a_1 : Prop), % 182.44/182.73 Eq % 182.44/182.73 (∀ (Xx : Iota), % 182.44/182.73 in Xx (skS.0 16 a) → % 182.44/182.73 ∀ (Xy : Iota), % 182.44/182.73 in Xy (skS.0 16 a) → in (if (skS.0 16 a) (skS.0 17 a a_1) Xx Xy) (setadjoin Xx (setadjoin Xy emptyset))) % 182.44/182.73 False % 182.44/182.73 Clause #253 (by clausification #[252]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 182.44/182.73 Eq % 182.44/182.73 (Not % 182.44/182.73 (in (skS.0 18 a a_1 a_2) (skS.0 16 a) → % 182.44/182.73 ∀ (Xy : Iota), % 182.44/182.73 in Xy (skS.0 16 a) → % 182.44/182.73 in (if (skS.0 16 a) (skS.0 17 a a_1) (skS.0 18 a a_1 a_2) Xy) % 182.44/182.73 (setadjoin (skS.0 18 a a_1 a_2) (setadjoin Xy emptyset)))) % 182.44/182.73 True % 182.44/182.73 Clause #254 (by clausification #[253]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 182.44/182.73 Eq % 182.44/182.73 (in (skS.0 18 a a_1 a_2) (skS.0 16 a) → % 182.44/182.73 ∀ (Xy : Iota), % 182.44/182.73 in Xy (skS.0 16 a) → % 182.44/182.73 in (if (skS.0 16 a) (skS.0 17 a a_1) (skS.0 18 a a_1 a_2) Xy) % 182.44/182.73 (setadjoin (skS.0 18 a a_1 a_2) (setadjoin Xy emptyset))) % 182.44/182.73 False % 182.44/182.73 Clause #255 (by clausification #[254]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), Eq (in (skS.0 18 a a_1 a_2) (skS.0 16 a)) True % 182.44/182.73 Clause #256 (by clausification #[254]): ∀ (a : Iota) (a_1 : Prop) (a_2 : Iota), % 182.44/182.73 Eq % 182.44/182.73 (∀ (Xy : Iota), % 182.44/182.73 in Xy (skS.0 16 a) → % 182.44/182.73 in (if (skS.0 16 a) (skS.0 17 a a_1) (skS.0 18 a a_1 a_2) Xy) % 182.44/182.73 (setadjoin (skS.0 18 a a_1 a_2) (setadjoin Xy emptyset))) % 182.44/182.73 False % 182.44/182.73 Clause #257 (by identity loobHoist #[255]): ∀ (a a_1 : Iota) (a_2 : Prop), Or (Eq (in (skS.0 18 a True a_1) (skS.0 16 a)) True) (Eq a_2 False) % 182.44/182.73 Clause #260 (by falseElim #[257]): ∀ (a a_1 : Iota), Eq (in (skS.0 18 a True a_1) (skS.0 16 a)) True % 182.44/182.73 Clause #261 (by superposition #[260, 182]): ∀ (a a_1 : Iota) (a_2 : Prop) (a_3 : Iota), % 182.44/182.73 Or (Eq True False) % 182.44/182.73 (Or (Eq (in a (skS.0 16 a_1)) False) % 182.44/182.73 (Or (Eq a_2 False) (Eq (if (skS.0 16 a_1) True (skS.0 18 a_1 True a_3) a) (skS.0 18 a_1 True a_3)))) % 182.44/182.73 Clause #262 (by superposition #[260, 229]): ∀ (a a_1 : Iota) (a_2 : Prop) (a_3 : Iota), % 182.44/182.76 Or (Eq True False) % 182.44/182.76 (Or (Eq (in a (skS.0 16 a_1)) False) (Or (Eq a_2 True) (Eq (if (skS.0 16 a_1) False (skS.0 18 a_1 True a_3) a) a))) % 182.44/182.76 Clause #354 (by clausification #[262]): ∀ (a a_1 : Iota) (a_2 : Prop) (a_3 : Iota), % 182.44/182.76 Or (Eq (in a (skS.0 16 a_1)) False) (Or (Eq a_2 True) (Eq (if (skS.0 16 a_1) False (skS.0 18 a_1 True a_3) a) a)) % 182.44/182.76 Clause #408 (by clausification #[261]): ∀ (a a_1 : Iota) (a_2 : Prop) (a_3 : Iota), % 182.44/182.76 Or (Eq (in a (skS.0 16 a_1)) False) % 182.44/182.76 (Or (Eq a_2 False) (Eq (if (skS.0 16 a_1) True (skS.0 18 a_1 True a_3) a) (skS.0 18 a_1 True a_3))) % 182.44/182.76 Clause #414 (by clausification #[256]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 182.44/182.76 Eq % 182.44/182.76 (Not % 182.44/182.76 (in (skS.0 19 a a_1 a_2 a_3) (skS.0 16 a) → % 182.44/182.76 in (if (skS.0 16 a) (skS.0 17 a a_1) (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3)) % 182.44/182.76 (setadjoin (skS.0 18 a a_1 a_2) (setadjoin (skS.0 19 a a_1 a_2 a_3) emptyset)))) % 182.44/182.76 True % 182.44/182.76 Clause #415 (by clausification #[414]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 182.44/182.76 Eq % 182.44/182.76 (in (skS.0 19 a a_1 a_2 a_3) (skS.0 16 a) → % 182.44/182.76 in (if (skS.0 16 a) (skS.0 17 a a_1) (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3)) % 182.44/182.76 (setadjoin (skS.0 18 a a_1 a_2) (setadjoin (skS.0 19 a a_1 a_2 a_3) emptyset))) % 182.44/182.76 False % 182.44/182.76 Clause #416 (by clausification #[415]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), Eq (in (skS.0 19 a a_1 a_2 a_3) (skS.0 16 a)) True % 182.44/182.76 Clause #417 (by clausification #[415]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 182.44/182.76 Eq % 182.44/182.76 (in (if (skS.0 16 a) (skS.0 17 a a_1) (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3)) % 182.44/182.76 (setadjoin (skS.0 18 a a_1 a_2) (setadjoin (skS.0 19 a a_1 a_2 a_3) emptyset))) % 182.44/182.76 False % 182.44/182.76 Clause #418 (by identity loobHoist #[416]): ∀ (a a_1 a_2 : Iota) (a_3 : Prop), Or (Eq (in (skS.0 19 a True a_1 a_2) (skS.0 16 a)) True) (Eq a_3 False) % 182.44/182.76 Clause #421 (by falseElim #[418]): ∀ (a a_1 a_2 : Iota), Eq (in (skS.0 19 a True a_1 a_2) (skS.0 16 a)) True % 182.44/182.76 Clause #422 (by superposition #[421, 354]): ∀ (a : Prop) (a_1 a_2 a_3 a_4 : Iota), % 182.44/182.76 Or (Eq True False) % 182.44/182.76 (Or (Eq a True) % 182.44/182.76 (Eq (if (skS.0 16 a_1) False (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_3 a_4)) (skS.0 19 a_1 True a_3 a_4))) % 182.44/182.76 Clause #424 (by superposition #[421, 408]): ∀ (a : Prop) (a_1 a_2 a_3 a_4 : Iota), % 182.44/182.76 Or (Eq True False) % 182.44/182.76 (Or (Eq a False) % 182.44/182.76 (Eq (if (skS.0 16 a_1) True (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_3 a_4)) (skS.0 18 a_1 True a_2))) % 182.44/182.76 Clause #565 (by clausification #[424]): ∀ (a : Prop) (a_1 a_2 a_3 a_4 : Iota), % 182.44/182.76 Or (Eq a False) % 182.44/182.76 (Eq (if (skS.0 16 a_1) True (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_3 a_4)) (skS.0 18 a_1 True a_2)) % 182.44/182.76 Clause #567 (by falseElim #[565]): ∀ (a a_1 a_2 a_3 : Iota), % 182.44/182.76 Eq (if (skS.0 16 a) True (skS.0 18 a True a_1) (skS.0 19 a True a_2 a_3)) (skS.0 18 a True a_1) % 182.44/182.76 Clause #584 (by clausification #[422]): ∀ (a : Prop) (a_1 a_2 a_3 a_4 : Iota), % 182.44/182.76 Or (Eq a True) % 182.44/182.76 (Eq (if (skS.0 16 a_1) False (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_3 a_4)) (skS.0 19 a_1 True a_3 a_4)) % 182.44/182.76 Clause #833 (by identity loobHoist #[417]): ∀ (a : Iota) (a_1 : Prop) (a_2 a_3 : Iota), % 182.44/182.76 Or % 182.44/182.76 (Eq % 182.44/182.76 (in (if (skS.0 16 a) (skS.0 17 a a_1) (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3)) % 182.44/182.76 (setadjoin (skS.0 18 a a_1 a_2) (setadjoin (skS.0 19 a True a_2 a_3) emptyset))) % 182.44/182.76 False) % 182.44/182.76 (Eq a_1 False) % 182.44/182.76 Clause #835 (by identity loobHoist #[833]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.44/182.76 Or (Eq a False) % 182.44/182.76 (Or % 182.44/182.76 (Eq % 182.44/182.76 (in (if (skS.0 16 a_1) (skS.0 17 a_1 a) (skS.0 18 a_1 a a_2) (skS.0 19 a_1 a a_2 a_3)) % 182.44/182.76 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.44/182.76 False) % 182.44/182.76 (Eq a False)) % 182.44/182.76 Clause #837 (by eliminate duplicate literals #[835]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.44/182.76 Or (Eq a False) % 182.44/182.76 (Eq % 182.44/182.76 (in (if (skS.0 16 a_1) (skS.0 17 a_1 a) (skS.0 18 a_1 a a_2) (skS.0 19 a_1 a a_2 a_3)) % 182.44/182.76 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.44/182.76 False) % 182.44/182.76 Clause #838 (by identity loobHoist #[837]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.44/182.76 Or (Eq a False) % 182.44/182.76 (Or % 182.44/182.76 (Eq % 182.44/182.76 (in (if (skS.0 16 a_1) (skS.0 17 a_1 a) (skS.0 18 a_1 a a_2) (skS.0 19 a_1 True a_2 a_3)) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 (Eq a False)) % 182.54/182.78 Clause #840 (by eliminate duplicate literals #[838]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.54/182.78 Or (Eq a False) % 182.54/182.78 (Eq % 182.54/182.78 (in (if (skS.0 16 a_1) (skS.0 17 a_1 a) (skS.0 18 a_1 a a_2) (skS.0 19 a_1 True a_2 a_3)) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 Clause #841 (by identity loobHoist #[840]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.54/182.78 Or (Eq a False) % 182.54/182.78 (Or % 182.54/182.78 (Eq % 182.54/182.78 (in (if (skS.0 16 a_1) (skS.0 17 a_1 a) (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_2 a_3)) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 (Eq a False)) % 182.54/182.78 Clause #843 (by eliminate duplicate literals #[841]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.54/182.78 Or (Eq a False) % 182.54/182.78 (Eq % 182.54/182.78 (in (if (skS.0 16 a_1) (skS.0 17 a_1 a) (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_2 a_3)) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 Clause #844 (by identity loobHoist #[843]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.54/182.78 Or (Eq a False) % 182.54/182.78 (Or % 182.54/182.78 (Eq % 182.54/182.78 (in (if (skS.0 16 a_1) True (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_2 a_3)) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 (Eq (skS.0 17 a_1 a) False)) % 182.54/182.78 Clause #845 (by identity boolHoist #[843]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.54/182.78 Or (Eq a False) % 182.54/182.78 (Or % 182.54/182.78 (Eq % 182.54/182.78 (in (if (skS.0 16 a_1) False (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_2 a_3)) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 (Eq (skS.0 17 a_1 a) True)) % 182.54/182.78 Clause #846 (by forward demodulation #[844, 567]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.54/182.78 Or (Eq a False) % 182.54/182.78 (Or % 182.54/182.78 (Eq % 182.54/182.78 (in (skS.0 18 a_1 True a_2) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 (Eq (skS.0 17 a_1 a) False)) % 182.54/182.78 Clause #847 (by identity loobHoist #[846]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.54/182.78 Or (Eq a False) % 182.54/182.78 (Or % 182.54/182.78 (Eq % 182.54/182.78 (in (skS.0 18 a_1 True a_2) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 (Or (Eq (skS.0 17 a_1 True) False) (Eq a False))) % 182.54/182.78 Clause #849 (by eliminate duplicate literals #[847]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.54/182.78 Or (Eq a False) % 182.54/182.78 (Or % 182.54/182.78 (Eq % 182.54/182.78 (in (skS.0 18 a_1 True a_2) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 (Eq (skS.0 17 a_1 True) False)) % 182.54/182.78 Clause #851 (by falseElim #[849]): ∀ (a a_1 a_2 : Iota), % 182.54/182.78 Or % 182.54/182.78 (Eq (in (skS.0 18 a True a_1) (setadjoin (skS.0 18 a True a_1) (setadjoin (skS.0 19 a True a_1 a_2) emptyset))) % 182.54/182.78 False) % 182.54/182.78 (Eq (skS.0 17 a True) False) % 182.54/182.78 Clause #852 (by superposition #[851, 87]): ∀ (a : Iota), Or (Eq (skS.0 17 a True) False) (Eq False True) % 182.54/182.78 Clause #853 (by clausification #[852]): ∀ (a : Iota), Eq (skS.0 17 a True) False % 182.54/182.78 Clause #1362 (by identity loobHoist #[845]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.54/182.78 Or (Eq a False) % 182.54/182.78 (Or % 182.54/182.78 (Eq % 182.54/182.78 (in (if (skS.0 16 a_1) False (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_2 a_3)) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 (Or (Eq (skS.0 17 a_1 True) True) (Eq a False))) % 182.54/182.78 Clause #1364 (by eliminate duplicate literals #[1362]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.54/182.78 Or (Eq a False) % 182.54/182.78 (Or % 182.54/182.78 (Eq % 182.54/182.78 (in (if (skS.0 16 a_1) False (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_2 a_3)) % 182.54/182.78 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.54/182.78 False) % 182.54/182.78 (Eq (skS.0 17 a_1 True) True)) % 182.54/182.78 Clause #1365 (by forward demodulation #[1364, 853]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.70/182.94 Or (Eq a False) % 182.70/182.94 (Or % 182.70/182.94 (Eq % 182.70/182.94 (in (if (skS.0 16 a_1) False (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_2 a_3)) % 182.70/182.94 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.70/182.94 False) % 182.70/182.94 (Eq False True)) % 182.70/182.94 Clause #1366 (by clausification #[1365]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.70/182.94 Or (Eq a False) % 182.70/182.94 (Eq % 182.70/182.94 (in (if (skS.0 16 a_1) False (skS.0 18 a_1 True a_2) (skS.0 19 a_1 True a_2 a_3)) % 182.70/182.94 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.70/182.94 False) % 182.70/182.94 Clause #1368 (by falseElim #[1366]): ∀ (a a_1 a_2 : Iota), % 182.70/182.94 Eq % 182.70/182.94 (in (if (skS.0 16 a) False (skS.0 18 a True a_1) (skS.0 19 a True a_1 a_2)) % 182.70/182.94 (setadjoin (skS.0 18 a True a_1) (setadjoin (skS.0 19 a True a_1 a_2) emptyset))) % 182.70/182.94 False % 182.70/182.94 Clause #1369 (by superposition #[1368, 584]): ∀ (a : Prop) (a_1 a_2 a_3 : Iota), % 182.70/182.94 Or (Eq a True) % 182.70/182.94 (Eq % 182.70/182.94 (in (skS.0 19 a_1 True a_2 a_3) % 182.70/182.94 (setadjoin (skS.0 18 a_1 True a_2) (setadjoin (skS.0 19 a_1 True a_2 a_3) emptyset))) % 182.70/182.94 False) % 182.70/182.94 Clause #1377 (by superposition #[1369, 164]): ∀ (a : Prop), Or (Eq a True) (Eq False True) % 182.70/182.94 Clause #1378 (by clausification #[1377]): ∀ (a : Prop), Eq a True % 182.70/182.94 Clause #1403 (by falseElim #[1378]): False % 182.70/182.94 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------