OBJ0

Tardo

Based on unsorted equational logic.