let remove_variants (literals: literal list) =
  (* extend an existing variant mapping to two more terms.
     invariant: variable with lower id are bound to variables with higher id.
     avoids cycles in renaming.
  *)
  let rec are_terms_variants mapping (term1: term) (term2: term) =
    match term1, term2 with
      | Var var1, Var var2 ->
          let cmp =
            Var.compare var1 var2
          in
            if cmp = 0 then
              mapping
            else if cmp < 0 then
              (var1, var2) :: mapping
            else
              (var2, var1) :: mapping
              
      | Const symbol1, Const symbol2 when
          Symbol.equal symbol1 symbol2 ->

          mapping
            
      | Func func1, Func func2 when
          Symbol.equal func1.symbol func2.symbol ->
          
          Tools.array_fold2 are_terms_variants mapping func1.subterms func2.subterms
            
      | _ ->
          raise Exit
  in

  (* find a renaming making all variants identical *)
  let rec find_renaming mapping literals =
    match literals with
      | [] ->
          failwith "Lemma: find_renaming"
          
      | _ :: [] ->
          mapping
          
      | l1 :: tail ->
          (* search for a variant for l1 in tail *)
          begin
            let rec find_renaming' mapping tail' =
              match tail' with
                | [] ->
                    (* no variant found *)
                    find_renaming mapping tail
                    
                | l2 :: tail' ->
                    let mapping' =
                      try
                        Some (are_terms_variants mapping l1.atom l2.atom)
                      with
                        | Exit ->
                            None
                    in
                      (* variant found *)
                      match mapping' with
                        | Some mapping ->
                            find_renaming mapping tail

                        | None ->
                            find_renaming' mapping tail'
            in
              find_renaming' mapping tail            

          end
  in
  let mapping =
    find_renaming [] literals
  in

  let rec dereference mapping var =
    try
      let var' =
        Var.VarTable.find mapping var
      in
        dereference mapping var'
    with
      | Not_found ->
          var
  in

    match mapping with
      | [] ->
          (* no variants *)
          literals

      | _ ->
          begin
            (* apply the renaming *)
            let mapping' =
              Var.VarTable.create 61
            in
              List.iter
                (fun (var1, var2) ->
                   Var.VarTable.add mapping' var1 var2
                )
                mapping;

              let mapping =
                Var.VarTable.fold
                  (fun var1 var2 acc ->
                     let var2' =
                       dereference mapping' var2
                     in
                       (request_var var1, request_var var2') :: acc
                  )
                  mapping'
                  []
              in
                
                (* apply unifier - have to use replace to avoid independent normalization *)
                List.map
                  (fun literal ->
                     replace_terms_in_literal literal mapping
                  )
                  literals
          end