Resolution Algorithm for FOL