let cmp_universality (first: pureness) (second: pureness) : int =
  (* as few parameters as possible *)
  if first.pars < second.pars then
    -1
  else if first.pars > second.pars then
    1
  else 
    (* as many variables as possible -
       this check is supposed to be done for terms of equal term weight only,
       so this prefers smaller/shallower predicates/terms *)
    compare second.vars first.vars