pure memory logic tableau prover