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