The engine proves a query by unifying the query's structures with facts in a program. Queries can contain a series of structures, each of which must be true for the query to succeed. When a query has multiple structures, its first structure unifies with some axiom in the program, which typically establishes values for some of the query's variables. The remaining structures attempt to establish their truth with these variable values in place.
Consider a collection of facts about construction companies and a supplier's fees (in drachmas) for delivery to their locations:
charge(athens, 23); charge(sparta, 13); charge(milos, 17); customer("Marathon Marble", sparta); customer("Acropolis Construction", athens); customer("Agora Imports", ...