S77    $x(Gx & ~Fx), @x(Gx -> Hx) |- $x(Hx & ~Fx)    

S78    $x(Gx & Fx), @x(Fx -> ~Hx) |- $x~Hx    

S79    @x(Gx -> ~Fx), @x(~Fx -> ~Hx) |- @x(Gx -> ~Hx)  

S80    @x(Gx -> $y(Fy & Hy)) |- @x~Fx -> ~$zGz    

S81    @x(Gx -> Hx & Jx), @x(Fx v ~Jx -> Gx)|- @x(Fx -> Hx)  

S82    @x(Gx & Kx <-> Hx), ~$x(Fx & Gx)|- @x~(Fx & Hx)    

S83    @x(Gx -> Hx), $x((Fx & Gx) & Mx)|- $x(Fx & (Hx & Mx))    

S84    @x(~Gx v ~Hx), @x((Jx -> Fx) -> Hx)|- ~$x(Fx & Gx)  

S85    ~$x(~Gx & Hx), @x(Fx -> ~Hx)|- @x(Fx v ~Gx -> ~Hx)    

S86    @x~(Gx & Hx), $x(Fx & Gx) |- $x(Fx & ~Hx)    

S87    $x(Fx & ~Hx), ~$x(Fx & ~Gx) |- ~@x(Gx -> Hx)

S88    @x(Hx -> Hx & Gx), $x(~Gx & Fx)|- $x(Fx & ~Hx)    

S89    @x(Hx -> ~Gx), ~$x(Fx & ~Gx) |- @x~(Fx & Hx)  

S90    @x(Fx <-> Gx) |- @xFx <-> @xGx      

S91    $xFx -> @y(Gy -> Hy), $xJx -> $xGx|- $x(Fx & Jx) -> $zHz    

S92    $xFx v $xGx, @x(Fx -> Gx) |- $xGx  

S93    @x(Fx -> ~Gx) |- ~$x(Fx & Gx)

S94    @x(Fx v Hx -> Gx & Kx), ~@x(Kx & Gx) |- $x~Hx    

S95    @x(Fx & Gx -> Hx), Ga & @xFx |- Fa & Ha  

S96    @x(Fx <-> @yGy) |- @xFx v @x~Fx    

S97    @y(Fa -> ($xGx -> Gy)),@x(Gx -> Hx), @x(~Jx -> ~Hx) |- $x~Jx -> ~Fa v @x~Gx  

S98    @x(Dx -> Fx) |- @z(Dz -> (@y(Fy -> Gy) -> Gz))    

S99    $xFx <-> @y(Fy v Gy -> Hy), $xHx, ~@z~Fz|- $x(Fx & Hx)    

S100    @xFx |- ~$xGx <-> ~($x(Fx & Gx) & @y(Gy -> Fy))  

S101    @x($yFyx -> @zFxz) |- @yx(Fyx -> Fxy)    

S102    $x(Fx & @yGxy), @xy(Gxy -> Gyx)|- $x(Fx & @yGyx)    

S103    $x~@y(Gxy -> Gyx) |- $x$y(Gxy & ~Gyx)    

S104    @x(Gx -> @y(Fy -> Hxy)), $x(Fx & @z~Hxz)|- ~@xGx  

S105    @xy(Fxy -> Gxy) |- @x(Fxx -> $y(Gxy & Fyx))