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))