This paper presents a general implementation by Maude of labelled transition systems specified by SOS (structural operational semantics) with negative premises. The search mechanism of the 'meta-level' in Maude eases the checking of negative premises in SOS rules. Combining a bisimulation equivalence checker with the SOS interpreter, our tool enables to show the semantic equivalence on terms specified by a general class of SOS. We illustrate the use of our tools by checking the equivalence of TPL, a process calculus proposed by Hennessy.