let are_literals_skolem_variants (literal1: literal) (literal2: literal) : bool =
  (literal1.sign == literal2.sign)
  &&
  (are_terms_skolem_variants literal1.atom literal2.atom)