@InProceedings{McC88,
    Author       = "McCune, W.W.",
    Year         = "1988",
    Title        = "{Challenge Equality Problems in Lattice Theory}",
    BookTitle    = "{Proceedings of the 9th International Conference on
                    Automated Deduction - Argonne Ilinois, USA, May 1988}",
    Place        = "Berlin",
    Pages        = "704-709",
    Publisher    = "Springer",
    Comment      = "TPTPRef"
}