unary
arity
Herbrand
axiomatisation
unsatisfiable
internalisable
expressivity
subgraphs