It looks like -> on a line of its own means "everything before this implies everything after it". So, for your second example you want x,Hx->Mx -> Hs->Ms

It looks like -> on a line of its own means "everything before this implies everything after it". So, for your second example you want x,Hx->Mx -> Hs->Ms which returns "The statement is necessarily true."