%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU692^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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:13 PM UTC 2025 % Result : Theorem 11.66s 11.86s % Output : Proof 11.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU692^2 : TPTP v9.2.0. Released v3.7.0. % 0.03/0.13 % Command : duper %s % 0.14/0.34 % Computer : n028.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 05:24:53 EDT 2025 % 0.14/0.34 % CPUTime : % 11.66/11.86 SZS status Theorem for theBenchmark.p % 11.66/11.86 SZS output start Proof for theBenchmark.p % 11.66/11.86 Clause #0 (by assumption #[]): Eq (Eq infuncsetfunc (∀ (A B Xf : Iota), in Xf (funcSet A B) → func A B Xf)) True % 11.66/11.86 Clause #1 (by assumption #[]): Eq % 11.66/11.86 (Eq funcext % 11.66/11.86 (∀ (A B Xf : Iota), % 11.66/11.86 func A B Xf → % 11.66/11.86 ∀ (Xg : Iota), func A B Xg → (∀ (Xx : Iota), in Xx A → Eq (ap A B Xf Xx) (ap A B Xg Xx)) → Eq Xf Xg)) % 11.66/11.86 True % 11.66/11.86 Clause #2 (by assumption #[]): Eq % 11.66/11.86 (Not % 11.66/11.86 (infuncsetfunc → % 11.66/11.86 funcext → % 11.66/11.86 ∀ (A B Xf : Iota), % 11.66/11.86 in Xf (funcSet A B) → % 11.66/11.86 ∀ (Xg : Iota), % 11.66/11.86 in Xg (funcSet A B) → (∀ (Xx : Iota), in Xx A → Eq (ap A B Xf Xx) (ap A B Xg Xx)) → Eq Xf Xg)) % 11.66/11.86 True % 11.66/11.86 Clause #3 (by clausification #[0]): Eq infuncsetfunc (∀ (A B Xf : Iota), in Xf (funcSet A B) → func A B Xf) % 11.66/11.86 Clause #19 (by clausification #[1]): Eq funcext % 11.66/11.86 (∀ (A B Xf : Iota), % 11.66/11.86 func A B Xf → ∀ (Xg : Iota), func A B Xg → (∀ (Xx : Iota), in Xx A → Eq (ap A B Xf Xx) (ap A B Xg Xx)) → Eq Xf Xg) % 11.66/11.86 Clause #21 (by clausify Prop equality #[19]): Or (Eq funcext False) % 11.66/11.86 (Eq % 11.66/11.86 (∀ (A B Xf : Iota), % 11.66/11.86 func A B Xf → ∀ (Xg : Iota), func A B Xg → (∀ (Xx : Iota), in Xx A → Eq (ap A B Xf Xx) (ap A B Xg Xx)) → Eq Xf Xg) % 11.66/11.86 True) % 11.66/11.86 Clause #23 (by clausification #[2]): Eq % 11.66/11.86 (infuncsetfunc → % 11.66/11.86 funcext → % 11.66/11.86 ∀ (A B Xf : Iota), % 11.66/11.86 in Xf (funcSet A B) → % 11.66/11.86 ∀ (Xg : Iota), in Xg (funcSet A B) → (∀ (Xx : Iota), in Xx A → Eq (ap A B Xf Xx) (ap A B Xg Xx)) → Eq Xf Xg) % 11.66/11.86 False % 11.66/11.86 Clause #24 (by clausification #[23]): Eq infuncsetfunc True % 11.66/11.86 Clause #25 (by clausification #[23]): Eq % 11.66/11.86 (funcext → % 11.66/11.86 ∀ (A B Xf : Iota), % 11.66/11.86 in Xf (funcSet A B) → % 11.66/11.86 ∀ (Xg : Iota), in Xg (funcSet A B) → (∀ (Xx : Iota), in Xx A → Eq (ap A B Xf Xx) (ap A B Xg Xx)) → Eq Xf Xg) % 11.66/11.86 False % 11.66/11.86 Clause #26 (by backward demodulation #[24, 3]): Eq True (∀ (A B Xf : Iota), in Xf (funcSet A B) → func A B Xf) % 11.66/11.86 Clause #29 (by clausification #[26]): ∀ (a : Iota), Eq (∀ (B Xf : Iota), in Xf (funcSet a B) → func a B Xf) True % 11.66/11.86 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), Eq (∀ (Xf : Iota), in Xf (funcSet a a_1) → func a a_1 Xf) True % 11.66/11.86 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 : Iota), Eq (in a (funcSet a_1 a_2) → func a_1 a_2 a) True % 11.66/11.86 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (funcSet a_1 a_2)) False) (Eq (func a_1 a_2 a) True) % 11.66/11.86 Clause #33 (by clausification #[25]): Eq funcext True % 11.66/11.86 Clause #34 (by clausification #[25]): Eq % 11.66/11.86 (∀ (A B Xf : Iota), % 11.66/11.86 in Xf (funcSet A B) → % 11.66/11.86 ∀ (Xg : Iota), in Xg (funcSet A B) → (∀ (Xx : Iota), in Xx A → Eq (ap A B Xf Xx) (ap A B Xg Xx)) → Eq Xf Xg) % 11.66/11.86 False % 11.66/11.86 Clause #48 (by clausification #[34]): ∀ (a : Iota), % 11.66/11.86 Eq % 11.66/11.86 (Not % 11.66/11.86 (∀ (B Xf : Iota), % 11.66/11.86 in Xf (funcSet (skS.0 4 a) B) → % 11.66/11.86 ∀ (Xg : Iota), % 11.66/11.86 in Xg (funcSet (skS.0 4 a) B) → % 11.66/11.86 (∀ (Xx : Iota), in Xx (skS.0 4 a) → Eq (ap (skS.0 4 a) B Xf Xx) (ap (skS.0 4 a) B Xg Xx)) → Eq Xf Xg)) % 11.66/11.86 True % 11.66/11.86 Clause #49 (by clausification #[48]): ∀ (a : Iota), % 11.66/11.86 Eq % 11.66/11.86 (∀ (B Xf : Iota), % 11.66/11.86 in Xf (funcSet (skS.0 4 a) B) → % 11.66/11.86 ∀ (Xg : Iota), % 11.66/11.86 in Xg (funcSet (skS.0 4 a) B) → % 11.66/11.86 (∀ (Xx : Iota), in Xx (skS.0 4 a) → Eq (ap (skS.0 4 a) B Xf Xx) (ap (skS.0 4 a) B Xg Xx)) → Eq Xf Xg) % 11.66/11.86 False % 11.66/11.86 Clause #50 (by clausification #[49]): ∀ (a a_1 : Iota), % 11.66/11.86 Eq % 11.66/11.86 (Not % 11.66/11.86 (∀ (Xf : Iota), % 11.66/11.86 in Xf (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.66/11.86 ∀ (Xg : Iota), % 11.66/11.86 in Xg (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.66/11.86 (∀ (Xx : Iota), % 11.66/11.86 in Xx (skS.0 4 a) → % 11.66/11.86 Eq (ap (skS.0 4 a) (skS.0 5 a a_1) Xf Xx) (ap (skS.0 4 a) (skS.0 5 a a_1) Xg Xx)) → % 11.66/11.86 Eq Xf Xg)) % 11.66/11.86 True % 11.66/11.86 Clause #51 (by clausification #[50]): ∀ (a a_1 : Iota), % 11.66/11.86 Eq % 11.66/11.86 (∀ (Xf : Iota), % 11.66/11.86 in Xf (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.66/11.86 ∀ (Xg : Iota), % 11.66/11.86 in Xg (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.66/11.86 (∀ (Xx : Iota), % 11.72/11.89 in Xx (skS.0 4 a) → Eq (ap (skS.0 4 a) (skS.0 5 a a_1) Xf Xx) (ap (skS.0 4 a) (skS.0 5 a a_1) Xg Xx)) → % 11.72/11.89 Eq Xf Xg) % 11.72/11.89 False % 11.72/11.89 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), % 11.72/11.89 Eq % 11.72/11.89 (Not % 11.72/11.89 (in (skS.0 6 a a_1 a_2) (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.72/11.89 ∀ (Xg : Iota), % 11.72/11.89 in Xg (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.72/11.89 (∀ (Xx : Iota), % 11.72/11.89 in Xx (skS.0 4 a) → % 11.72/11.89 Eq (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) Xx) (ap (skS.0 4 a) (skS.0 5 a a_1) Xg Xx)) → % 11.72/11.89 Eq (skS.0 6 a a_1 a_2) Xg)) % 11.72/11.89 True % 11.72/11.89 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 : Iota), % 11.72/11.89 Eq % 11.72/11.89 (in (skS.0 6 a a_1 a_2) (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.72/11.89 ∀ (Xg : Iota), % 11.72/11.89 in Xg (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.72/11.89 (∀ (Xx : Iota), % 11.72/11.89 in Xx (skS.0 4 a) → % 11.72/11.89 Eq (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) Xx) (ap (skS.0 4 a) (skS.0 5 a a_1) Xg Xx)) → % 11.72/11.89 Eq (skS.0 6 a a_1 a_2) Xg) % 11.72/11.89 False % 11.72/11.89 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 : Iota), Eq (in (skS.0 6 a a_1 a_2) (funcSet (skS.0 4 a) (skS.0 5 a a_1))) True % 11.72/11.89 Clause #55 (by clausification #[53]): ∀ (a a_1 a_2 : Iota), % 11.72/11.89 Eq % 11.72/11.89 (∀ (Xg : Iota), % 11.72/11.89 in Xg (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.72/11.89 (∀ (Xx : Iota), % 11.72/11.89 in Xx (skS.0 4 a) → % 11.72/11.89 Eq (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) Xx) (ap (skS.0 4 a) (skS.0 5 a a_1) Xg Xx)) → % 11.72/11.89 Eq (skS.0 6 a a_1 a_2) Xg) % 11.72/11.89 False % 11.72/11.89 Clause #56 (by superposition #[54, 32]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (func (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) True) % 11.72/11.89 Clause #67 (by clausification #[21]): ∀ (a : Iota), % 11.72/11.89 Or (Eq funcext False) % 11.72/11.89 (Eq % 11.72/11.89 (∀ (B Xf : Iota), % 11.72/11.89 func a B Xf → % 11.72/11.89 ∀ (Xg : Iota), func a B Xg → (∀ (Xx : Iota), in Xx a → Eq (ap a B Xf Xx) (ap a B Xg Xx)) → Eq Xf Xg) % 11.72/11.89 True) % 11.72/11.89 Clause #68 (by clausification #[67]): ∀ (a a_1 : Iota), % 11.72/11.89 Or (Eq funcext False) % 11.72/11.89 (Eq % 11.72/11.89 (∀ (Xf : Iota), % 11.72/11.89 func a a_1 Xf → % 11.72/11.89 ∀ (Xg : Iota), func a a_1 Xg → (∀ (Xx : Iota), in Xx a → Eq (ap a a_1 Xf Xx) (ap a a_1 Xg Xx)) → Eq Xf Xg) % 11.72/11.89 True) % 11.72/11.89 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 : Iota), % 11.72/11.89 Or (Eq funcext False) % 11.72/11.89 (Eq % 11.72/11.89 (func a a_1 a_2 → % 11.72/11.89 ∀ (Xg : Iota), func a a_1 Xg → (∀ (Xx : Iota), in Xx a → Eq (ap a a_1 a_2 Xx) (ap a a_1 Xg Xx)) → Eq a_2 Xg) % 11.72/11.89 True) % 11.72/11.89 Clause #70 (by clausification #[69]): ∀ (a a_1 a_2 : Iota), % 11.72/11.89 Or (Eq funcext False) % 11.72/11.89 (Or (Eq (func a a_1 a_2) False) % 11.72/11.89 (Eq (∀ (Xg : Iota), func a a_1 Xg → (∀ (Xx : Iota), in Xx a → Eq (ap a a_1 a_2 Xx) (ap a a_1 Xg Xx)) → Eq a_2 Xg) % 11.72/11.89 True)) % 11.72/11.89 Clause #71 (by clausification #[70]): ∀ (a a_1 a_2 a_3 : Iota), % 11.72/11.89 Or (Eq funcext False) % 11.72/11.89 (Or (Eq (func a a_1 a_2) False) % 11.72/11.89 (Eq (func a a_1 a_3 → (∀ (Xx : Iota), in Xx a → Eq (ap a a_1 a_2 Xx) (ap a a_1 a_3 Xx)) → Eq a_2 a_3) True)) % 11.72/11.89 Clause #72 (by clausification #[71]): ∀ (a a_1 a_2 a_3 : Iota), % 11.72/11.89 Or (Eq funcext False) % 11.72/11.89 (Or (Eq (func a a_1 a_2) False) % 11.72/11.89 (Or (Eq (func a a_1 a_3) False) % 11.72/11.89 (Eq ((∀ (Xx : Iota), in Xx a → Eq (ap a a_1 a_2 Xx) (ap a a_1 a_3 Xx)) → Eq a_2 a_3) True))) % 11.72/11.89 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 a_3 : Iota), % 11.72/11.89 Or (Eq funcext False) % 11.72/11.89 (Or (Eq (func a a_1 a_2) False) % 11.72/11.89 (Or (Eq (func a a_1 a_3) False) % 11.72/11.89 (Or (Eq (∀ (Xx : Iota), in Xx a → Eq (ap a a_1 a_2 Xx) (ap a a_1 a_3 Xx)) False) (Eq (Eq a_2 a_3) True)))) % 11.72/11.89 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.89 Or (Eq funcext False) % 11.72/11.89 (Or (Eq (func a a_1 a_2) False) % 11.72/11.89 (Or (Eq (func a a_1 a_3) False) % 11.72/11.89 (Or (Eq (Eq a_2 a_3) True) % 11.72/11.89 (Eq % 11.72/11.89 (Not % 11.72/11.89 (in (skS.0 10 a a_1 a_2 a_3 a_4) a → % 11.72/11.89 Eq (ap a a_1 a_2 (skS.0 10 a a_1 a_2 a_3 a_4)) (ap a a_1 a_3 (skS.0 10 a a_1 a_2 a_3 a_4)))) % 11.72/11.89 True)))) % 11.72/11.89 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.91 Or (Eq funcext False) % 11.72/11.91 (Or (Eq (func a a_1 a_2) False) % 11.72/11.91 (Or (Eq (func a a_1 a_3) False) % 11.72/11.91 (Or % 11.72/11.91 (Eq % 11.72/11.91 (Not % 11.72/11.91 (in (skS.0 10 a a_1 a_2 a_3 a_4) a → % 11.72/11.91 Eq (ap a a_1 a_2 (skS.0 10 a a_1 a_2 a_3 a_4)) (ap a a_1 a_3 (skS.0 10 a a_1 a_2 a_3 a_4)))) % 11.72/11.91 True) % 11.72/11.91 (Eq a_2 a_3)))) % 11.72/11.91 Clause #76 (by clausification #[75]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.91 Or (Eq funcext False) % 11.72/11.91 (Or (Eq (func a a_1 a_2) False) % 11.72/11.91 (Or (Eq (func a a_1 a_3) False) % 11.72/11.91 (Or (Eq a_2 a_3) % 11.72/11.91 (Eq % 11.72/11.91 (in (skS.0 10 a a_1 a_2 a_3 a_4) a → % 11.72/11.91 Eq (ap a a_1 a_2 (skS.0 10 a a_1 a_2 a_3 a_4)) (ap a a_1 a_3 (skS.0 10 a a_1 a_2 a_3 a_4))) % 11.72/11.91 False)))) % 11.72/11.91 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.91 Or (Eq funcext False) % 11.72/11.91 (Or (Eq (func a a_1 a_2) False) % 11.72/11.91 (Or (Eq (func a a_1 a_3) False) (Or (Eq a_2 a_3) (Eq (in (skS.0 10 a a_1 a_2 a_3 a_4) a) True)))) % 11.72/11.91 Clause #78 (by clausification #[76]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.91 Or (Eq funcext False) % 11.72/11.91 (Or (Eq (func a a_1 a_2) False) % 11.72/11.91 (Or (Eq (func a a_1 a_3) False) % 11.72/11.91 (Or (Eq a_2 a_3) % 11.72/11.91 (Eq (Eq (ap a a_1 a_2 (skS.0 10 a a_1 a_2 a_3 a_4)) (ap a a_1 a_3 (skS.0 10 a a_1 a_2 a_3 a_4))) False)))) % 11.72/11.91 Clause #79 (by forward demodulation #[77, 33]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.91 Or (Eq True False) % 11.72/11.91 (Or (Eq (func a a_1 a_2) False) % 11.72/11.91 (Or (Eq (func a a_1 a_3) False) (Or (Eq a_2 a_3) (Eq (in (skS.0 10 a a_1 a_2 a_3 a_4) a) True)))) % 11.72/11.91 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.91 Or (Eq (func a a_1 a_2) False) % 11.72/11.91 (Or (Eq (func a a_1 a_3) False) (Or (Eq a_2 a_3) (Eq (in (skS.0 10 a a_1 a_2 a_3 a_4) a) True))) % 11.72/11.91 Clause #81 (by clausification #[55]): ∀ (a a_1 a_2 a_3 : Iota), % 11.72/11.91 Eq % 11.72/11.91 (Not % 11.72/11.91 (in (skS.0 11 a a_1 a_2 a_3) (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.72/11.91 (∀ (Xx : Iota), % 11.72/11.91 in Xx (skS.0 4 a) → % 11.72/11.91 Eq (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) Xx) % 11.72/11.91 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 11 a a_1 a_2 a_3) Xx)) → % 11.72/11.91 Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3))) % 11.72/11.91 True % 11.72/11.91 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 a_3 : Iota), % 11.72/11.91 Eq % 11.72/11.91 (in (skS.0 11 a a_1 a_2 a_3) (funcSet (skS.0 4 a) (skS.0 5 a a_1)) → % 11.72/11.91 (∀ (Xx : Iota), % 11.72/11.91 in Xx (skS.0 4 a) → % 11.72/11.91 Eq (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) Xx) % 11.72/11.91 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 11 a a_1 a_2 a_3) Xx)) → % 11.72/11.91 Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) % 11.72/11.91 False % 11.72/11.91 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 11 a a_1 a_2 a_3) (funcSet (skS.0 4 a) (skS.0 5 a a_1))) True % 11.72/11.91 Clause #84 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : Iota), % 11.72/11.91 Eq % 11.72/11.91 ((∀ (Xx : Iota), % 11.72/11.91 in Xx (skS.0 4 a) → % 11.72/11.91 Eq (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) Xx) % 11.72/11.91 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 11 a a_1 a_2 a_3) Xx)) → % 11.72/11.91 Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) % 11.72/11.91 False % 11.72/11.91 Clause #85 (by superposition #[83, 32]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (func (skS.0 4 a) (skS.0 5 a a_1) (skS.0 11 a a_1 a_2 a_3)) True) % 11.72/11.91 Clause #91 (by clausification #[84]): ∀ (a a_1 a_2 a_3 : Iota), % 11.72/11.91 Eq % 11.72/11.91 (∀ (Xx : Iota), % 11.72/11.91 in Xx (skS.0 4 a) → % 11.72/11.91 Eq (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) Xx) % 11.72/11.91 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 11 a a_1 a_2 a_3) Xx)) % 11.72/11.91 True % 11.72/11.91 Clause #92 (by clausification #[84]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) False % 11.72/11.91 Clause #93 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.91 Eq % 11.72/11.91 (in a (skS.0 4 a_1) → % 11.72/11.91 Eq (ap (skS.0 4 a_1) (skS.0 5 a_1 a_2) (skS.0 6 a_1 a_2 a_3) a) % 11.72/11.91 (ap (skS.0 4 a_1) (skS.0 5 a_1 a_2) (skS.0 11 a_1 a_2 a_3 a_4) a)) % 11.72/11.91 True % 11.72/11.91 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.91 Or (Eq (in a (skS.0 4 a_1)) False) % 11.72/11.91 (Eq % 11.72/11.91 (Eq (ap (skS.0 4 a_1) (skS.0 5 a_1 a_2) (skS.0 6 a_1 a_2 a_3) a) % 11.72/11.91 (ap (skS.0 4 a_1) (skS.0 5 a_1 a_2) (skS.0 11 a_1 a_2 a_3 a_4) a)) % 11.72/11.94 True) % 11.72/11.94 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.94 Or (Eq (in a (skS.0 4 a_1)) False) % 11.72/11.94 (Eq (ap (skS.0 4 a_1) (skS.0 5 a_1 a_2) (skS.0 6 a_1 a_2 a_3) a) % 11.72/11.94 (ap (skS.0 4 a_1) (skS.0 5 a_1 a_2) (skS.0 11 a_1 a_2 a_3 a_4) a)) % 11.72/11.94 Clause #96 (by clausification #[92]): ∀ (a a_1 a_2 a_3 : Iota), Ne (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3) % 11.72/11.94 Clause #97 (by clausification #[56]): ∀ (a a_1 a_2 : Iota), Eq (func (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) True % 11.72/11.94 Clause #99 (by superposition #[97, 80]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.94 Or (Eq True False) % 11.72/11.94 (Or (Eq (func (skS.0 4 a) (skS.0 5 a a_1) a_2) False) % 11.72/11.94 (Or (Eq (skS.0 6 a a_1 a_3) a_2) % 11.72/11.94 (Eq (in (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_3) a_2 a_4) (skS.0 4 a)) True))) % 11.72/11.94 Clause #110 (by clausification #[85]): ∀ (a a_1 a_2 a_3 : Iota), Eq (func (skS.0 4 a) (skS.0 5 a a_1) (skS.0 11 a a_1 a_2 a_3)) True % 11.72/11.94 Clause #114 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.94 Or (Eq funcext False) % 11.72/11.94 (Or (Eq (func a a_1 a_2) False) % 11.72/11.94 (Or (Eq (func a a_1 a_3) False) % 11.72/11.94 (Or (Eq a_2 a_3) (Ne (ap a a_1 a_2 (skS.0 10 a a_1 a_2 a_3 a_4)) (ap a a_1 a_3 (skS.0 10 a a_1 a_2 a_3 a_4)))))) % 11.72/11.94 Clause #115 (by forward demodulation #[114, 33]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.94 Or (Eq True False) % 11.72/11.94 (Or (Eq (func a a_1 a_2) False) % 11.72/11.94 (Or (Eq (func a a_1 a_3) False) % 11.72/11.94 (Or (Eq a_2 a_3) (Ne (ap a a_1 a_2 (skS.0 10 a a_1 a_2 a_3 a_4)) (ap a a_1 a_3 (skS.0 10 a a_1 a_2 a_3 a_4)))))) % 11.72/11.94 Clause #116 (by clausification #[115]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.94 Or (Eq (func a a_1 a_2) False) % 11.72/11.94 (Or (Eq (func a a_1 a_3) False) % 11.72/11.94 (Or (Eq a_2 a_3) (Ne (ap a a_1 a_2 (skS.0 10 a a_1 a_2 a_3 a_4)) (ap a a_1 a_3 (skS.0 10 a a_1 a_2 a_3 a_4))))) % 11.72/11.94 Clause #117 (by superposition #[116, 97]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.94 Or (Eq (func (skS.0 4 a) (skS.0 5 a a_1) a_2) False) % 11.72/11.94 (Or (Eq (skS.0 6 a a_1 a_3) a_2) % 11.72/11.94 (Or % 11.72/11.94 (Ne % 11.72/11.94 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_3) % 11.72/11.94 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_3) a_2 a_4)) % 11.72/11.94 (ap (skS.0 4 a) (skS.0 5 a a_1) a_2 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_3) a_2 a_4))) % 11.72/11.94 (Eq False True))) % 11.72/11.94 Clause #119 (by clausification #[99]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.94 Or (Eq (func (skS.0 4 a) (skS.0 5 a a_1) a_2) False) % 11.72/11.94 (Or (Eq (skS.0 6 a a_1 a_3) a_2) % 11.72/11.94 (Eq (in (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_3) a_2 a_4) (skS.0 4 a)) True)) % 11.72/11.94 Clause #121 (by superposition #[119, 110]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.72/11.94 Or (Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) % 11.72/11.94 (Or % 11.72/11.94 (Eq (in (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_5) (skS.0 4 a)) True) % 11.72/11.94 (Eq False True)) % 11.72/11.94 Clause #140 (by clausification #[121]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.72/11.94 Or (Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) % 11.72/11.94 (Eq (in (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_5) (skS.0 4 a)) True) % 11.72/11.94 Clause #141 (by superposition #[140, 95]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.72/11.94 Or (Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) % 11.72/11.94 (Or (Eq True False) % 11.72/11.94 (Eq % 11.72/11.94 (ap (skS.0 4 a) (skS.0 5 a a_5) (skS.0 6 a a_5 a_6) % 11.72/11.94 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_7)) % 11.72/11.94 (ap (skS.0 4 a) (skS.0 5 a a_5) (skS.0 11 a a_5 a_6 a_8) % 11.72/11.94 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_7)))) % 11.72/11.94 Clause #153 (by clausification #[117]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.72/11.94 Or (Eq (func (skS.0 4 a) (skS.0 5 a a_1) a_2) False) % 11.72/11.94 (Or (Eq (skS.0 6 a a_1 a_3) a_2) % 11.72/11.94 (Ne % 11.72/11.94 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_3) % 11.72/11.94 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_3) a_2 a_4)) % 11.72/11.94 (ap (skS.0 4 a) (skS.0 5 a a_1) a_2 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_3) a_2 a_4)))) % 11.72/11.94 Clause #155 (by superposition #[153, 110]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.72/11.95 Or (Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) % 11.72/11.95 (Or % 11.72/11.95 (Ne % 11.72/11.95 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 11.72/11.95 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_5)) % 11.72/11.95 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 11 a a_1 a_3 a_4) % 11.72/11.95 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_5))) % 11.72/11.95 (Eq False True)) % 11.72/11.95 Clause #168 (by clausification #[155]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.72/11.95 Or (Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) % 11.72/11.95 (Ne % 11.72/11.95 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 11.72/11.95 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_5)) % 11.72/11.95 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 11 a a_1 a_3 a_4) % 11.72/11.95 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_5))) % 11.72/11.95 Clause #170 (by clausification #[141]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.72/11.95 Or (Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) % 11.72/11.95 (Eq % 11.72/11.95 (ap (skS.0 4 a) (skS.0 5 a a_5) (skS.0 6 a a_5 a_6) % 11.72/11.95 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_7)) % 11.72/11.95 (ap (skS.0 4 a) (skS.0 5 a a_5) (skS.0 11 a a_5 a_6 a_8) % 11.72/11.95 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_7))) % 11.72/11.95 Clause #171 (by superposition #[170, 168]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.72/11.95 Or (Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) % 11.72/11.95 (Or (Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) % 11.72/11.95 (Ne % 11.72/11.95 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 11.72/11.95 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_5)) % 11.72/11.95 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_3) % 11.72/11.95 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_5)))) % 11.72/11.95 Clause #185 (by eliminate duplicate literals #[171]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.72/11.95 Or (Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) % 11.72/11.95 (Ne % 11.72/11.95 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 11.72/11.95 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_5)) % 11.72/11.95 (ap (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_3) % 11.72/11.95 (skS.0 10 (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4) a_5))) % 11.72/11.95 Clause #186 (by equality resolution #[185]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3) % 11.72/11.95 Clause #187 (by forward contextual literal cutting #[186, 96]): False % 11.72/11.95 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------