The authors show how to incorporate efficient ordering-based equality inference rules and redundancy elimination techniques into a tableau calculus. This approach is based on splitting of positive clauses and an adapted version of the superposition inference rules.
The soundness and completeness of the calculus are proved. This calculus is a non-trivial decision procedure for function-free clause logic with equality, which captures the complexity class NEXPTIME.