Artificial Intelligence - Old Questions

2. Consider following facts:

Every traffic chases some driver. Every driver who horns is smart. No traffic catches any smart driver. Any traffic who chases some driver but does not catch him is frustated.

Now configure FOPL knowledge base for above statements. Use resolution algorithm to draw a conclusion that "If all drivers horn, then all traffics are frustated".            (3+2+5)