the Unificator whose results are being cached
the maximum number of entries the LRU cache may hold, shared between mgu and merge