let simplify (regressed: literal list list) : literal list =

  let rec simplify (simplified: literal list) (classes: literal list list) =
    match classes with
      | [] ->
          simplified
            
      | literals :: tail ->
          begin
            try
              (* try to unify all literals in this class by unifying its literals pairwise *)
              let unifier =
                let rec unify' unifier literals =
                  match literals with
                    | [] ->
                        failwith "Lemma: simplifying empty class"
                        
                    | _ :: [] ->
                        unifier
                        
                    | l1 :: l2 :: tail ->
                        let unifier' =
                          Unification.unify_literals_ ~recompute:false unifier l1 0 l2 0
                        in
                          unify' unifier' (l2 :: tail)
                in
                  unify' Subst.empty literals
              in
                (* already a singleton, or only constants *)
                if Subst.is_empty unifier then begin
                  simplify (literals @ simplified) tail
                end
                  
                (* apply unifier to all literals -
                   have to avoid independent normalization *)
                else begin
                  (* only need to use one literal of the unified class *)
                  let simplified' =
                    List.map
                      (fun literal ->
                         Subst.apply_to_literal ~normalize:false unifier literal 0
                      )
                      ((List.hd literals) :: simplified)
                  in

                  let classes' =
                    List.map
                      (fun literals ->
                         List.map
                           (fun literal ->
                              Subst.apply_to_literal ~normalize:false unifier literal 0
                           )
                           literals
                      )
                      tail
                  in
                    simplify simplified' classes'
                end
                  
            with
              | Unification.UNIFICATION_FAIL ->
                  (* simplification of this class failed *)
                  simplify (literals @ simplified) tail
          end
  in
    
    simplify [] regressed