OBJ0
Tardo. Based on unsorted equational logic.