F VzrVyVw(o(a, y, w)Vv(a, y, a))->3. Vy (Vzo(a, y, 2)Vy(, y, a))) F彐 roy Vu(叭(x,y,t)∨v(x,y,co)→彐rvy(zo(x,y,z)Vp(x,y,co), new constant co T 3xVyVw(o(a, y, a)Vy(a, y, co)) F 3rvy(Vap(a, y, a)Vv(a, y, co)) T 3cVyVu(o(c, y, w)V v(a, g, co)) T Vyw(o(c1, y, w)V a(c1, y, co)), new constant Cl F 3rvy(Vap(a, y, a)Vv(a, y, co)) F Vy (Vzo(c1, 3, 2)Vy(c1, y, co)) F Vzo(c1, c2, z)V(c1, c2, co), new constant c2 F V2o(c1, c2, 2) F v(c1, C2, co) F Vzo(c1, c2, z) Fo(C1, C2, C3), new constant C3 T VyVu(o(c1, y, w)V a(c1, y, co)) T Vw(o(c1, c2, w)V a(cl, c2, co)) T o(c1, C2, c3)Vv(c T o(c1, c2, c3) T w(c1, c2, co) Figure 7: Tableau of 4.(cF ∀z(∃x∀y∀w(ϕ(x, y, w) ∨ ψ(x, y, z)) → ∃x∀y(∀zϕ(x, y, z) ∨ ψ(x, y, z))) F ∃x∀y∀w(ϕ(x, y, w) ∨ ψ(x, y, c0)) → ∃x∀y(∀zϕ(x, y, z) ∨ ψ(x, y, c0)), new constant c0 T ∃x∀y∀w(ϕ(x, y, w) ∨ ψ(x, y, c0)) F ∃x∀y(∀zϕ(x, y, z) ∨ ψ(x, y, c0)) T ∃x∀y∀w(ϕ(x, y, w) ∨ ψ(x, y, c0)) T ∀y∀w(ϕ(c1, y, w) ∨ ψ(c1, y, c0)), new constant c1 F ∃x∀y(∀zϕ(x, y, z) ∨ ψ(x, y, c0)) F ∀y(∀zϕ(c1, y, z) ∨ ψ(c1, y, c0)) F ∀zϕ(c1, c2, z) ∨ ψ(c1, c2, c0), new constant c2 F ∀zϕ(c1, c2, z) F ψ(c1, c2, c0) F ∀zϕ(c1, c2, z) F ϕ(c1, c2, c3), new constant c3 T ∀y∀w(ϕ(c1, y, w) ∨ ψ(c1, y, c0)) T ∀w(ϕ(c1, c2, w) ∨ ψ(c1, c2, c0)) T ϕ(c1, c2, c3) ∨ ψ(c1, c2, c0) T ϕ(c1, c2, c3) T ψ(c1, c2, c0) ⊗ ⊗ Figure 7: Tableau of 4.(c) 8