let subsumes (_subsuming: clause) (_subsumed: clause) : bool =
  let unifiers =
    List.map
      (fun general ->
         let unifiers =
           List.fold_left
             (fun acc instance ->
                try
                  let subst =
                    match_literals
                    ~recompute:false
                      general 0
                      instance 1
                  in
                  subst :: acc
                with
                  | (UNIFICATION_FAIL ) ->
                      acc
             )
             []
             _subsumed
         in
           general, unifiers
      )
      _subsuming
  in
  let unifiers =
    List.sort
      (fun (_, x) (_, y) -> Tools.compare_int (List.length x) (List.length y))
      unifiers
  in

  let rec subsumes' unifiers merged =
    match unifiers with
      | [] ->
          raise Exit

      | (_general, head) :: tail ->
          List.iter
            (fun subst ->
               try
                 let merged' =
                   merge_substs merged subst
                 in
                   subsumes' tail merged'
               with
                 | (UNIFICATION_FAIL ) ->
                     ()
            )
            head
  in
    try
      subsumes' unifiers Subst.empty;
      false
    with
      | Exit ->
          true