of
Classifies lhs and rhs into the appropriate Equation subtype: Identity if they are trivially equal (per equalityChecker, or structurally for variables), LeftAssignment/RightAssignment if exactly one side is a Var, Contradiction if they can be told apart at this level (different constants, or structs with different functor/arity), or Comparison if they need further decomposition (e.g. two structs with the same functor/arity, whose arguments are not inspected by this shallow classification — use allOf to recursively decompose down to non-decomposable equations).
Parameters
decides whether two non-variable Terms are equal; defaults to Term.equals but can be swapped (e.g. by AbstractUnificator.checkTermsEquality) to alter what counts as identical
Same as of, but taking the two Terms as a Pair (pair.first = lhs, pair.second = rhs).