So the "biggest" model is only as large as any atom in any position for any predicate and that is always finite for a finite number of sorts or predicates.
Is gave is/2 as an example of how Prologo allows you to generate new atoms/terms that have not been facts before.