A. {1} 1. (x)(Ax -> -Cx) P /Wa -> ((x)(Wx -> Cx) -> -Aa) B. {1} 1. (x)(Px -> Gx) P /
(x)(((Dx & Ex) & (y)((Py & Ey) -> -Gy)) -> -Px) C. {1} 1. (x)(Ax -> Gx) P {2} 2. (x)(Cx -> Hx) P /
(x)(Gx -> Cx) -> (x)(Ax -> Hx) D. {1} 1. (
x)Gx -> (x)(Cx -> Gx) P {2} 2. (
x)Tx -> (x)(Gx -> Tx) P /
(
x)(Tx & Gx) -> (x)(Cx -> Tx) E. {1} 1. (x)(Sxi -> Vxj) P {2} 2. (x)(-Fhx -> -Vax) P {3} 3. (x)(Fxk -> -Fxj) P /
Fhk -> -Sai F. {1} 1. (x)(y)((
z)Fzy -> Gx) P {2} 2. (
x)Hx P /
(x)(Hx -> -Gx) -> -Fac G. {1} 1. (x)(Rx -> (Sx v Mx)) P {2} 2. (x)((Ux & Rx) -> -Sx) P /
(x)(Ux -> Rx) -> (y)(Uy -> My) H. {1} 1. (x)(Lx -> ((y)(Py -> Vy) -> Mx)) P {2} 2. (
z)(Pz & Vz) -> (y)(Py -> Vy) P /
(
x)Lx -> ((
z)(Pz & Vz) -> (
y)My) I. {1} 1. (x)(Fxa -> Fxb) P /
(x)(y)((Kxy & Fya) -> Fyb) J. {1} 1. (x)((
y)(Byb & Lxyb) -> Fx) P {2} 2. (
x)(Cxb & Lxab) P /
(x)(Cxb -> -Fx) -> -Bab K. {1} 1. (x)((
y)(
z)((Gz & -Rz) & Sxzy) -> Cx) P {2} 2. (z)((Wz & Orz) -> (Slzr v Smzr)) P /
(
z)((Wz & Orz) & (Gz & -Rz)) -> ((u)-Smur -> Cl) L. {1) 1. (x)((Px & -Rxx) -> (y)(Py -> -Ryx)) P {2} 2. (y)(Py -> (x)((Px & -Ryx) -> -Hyx)) P /
(x)((Px & (z)(Pz -> -Rxz)) -> (y)(Py -> -Hyx))