The first hyper tableau suffers from blind guessing in instancing the clauses, and evolves into the unification-driven style, the second version. However, we found a counterexample of it. We modify the calculus and a new hyper tableau is represented.
['Shasha Feng', 'Jigui Sun', 'Xia Wu']
Hyper tableaux : The third version