We present several calculi that integrate equality handling
by superposition and ordered paramodulation into a free
variable tableau calculus. We prove completeness of this
calculus by an adaptation of the model generation technique
commonly used for completeness proofs of resolution calculi.
The calculi and the completeness proof are compared to earlier
results of Degtyarev and Voronkov.