A Benchmark Method for the Propositional Modal Logics K, KT, S4
Single Step Tableaux for Modal Logics
A Hyperbase for Binary Lattice Hyperidentities
The CADE-16 ATP System Competition