let request_skolemized_clause (clause: clause) : clause =
  let var_skolemization, par_normalization =
    List.fold_left
      (fun acc literal ->
        request_skolemized_term' literal.atom acc
      )
      ([], [])
      clause
  in
    match var_skolemization with
      | [] ->
          (* no universal variables in term *)
          clause

      | _ ->
          let mapping =
            List.map
              (fun (var, term) ->
                request_var var, term
              )
              (par_normalization @ var_skolemization)
          in
            List.map
              (fun literal ->
                replace_terms_in_literal literal mapping
              )
              clause