+let rec kbo t1 t2 =
+(* debug_print (lazy ( *)
+(* Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2))); *)
+(* if t1 = t2 then *)
+(* Eq *)
+(* else *)
+ let aux = aux_ordering ~recursion:false in
+ let w1 = weight_of_term t1
+ and w2 = weight_of_term t2 in
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> Eq
+ | _, [] -> Gt
+ | [], _ -> Lt
+ | hd1::tl1, hd2::tl2 ->
+ let o =
+(* debug_print (lazy ( *)
+(* Printf.sprintf "recursion kbo on %s %s" *)
+(* (CicPp.ppterm hd1) (CicPp.ppterm hd2))); *)
+ kbo hd1 hd2
+ in
+ if o = Eq then cmp tl1 tl2
+ else o
+ in
+ let comparison = compare_weights ~normalize:true w1 w2 in
+(* debug_print (lazy ( *)
+(* Printf.sprintf "Weights are: %s %s: %s" *)
+(* (string_of_weight w1) (string_of_weight w2) *)
+(* (string_of_comparison comparison))); *)
+ match comparison with
+ | Le ->
+ let r = aux t1 t2 in
+(* debug_print (lazy ("HERE! " ^ (string_of_comparison r))); *)
+ if r = Lt then Lt
+ else if r = Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ if cmp tl1 tl2 = Lt then Lt else Incomparable
+ | _, _ -> Incomparable
+ ) else Incomparable
+ | Ge ->
+ let r = aux t1 t2 in
+ if r = Gt then Gt
+ else if r = Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ if cmp tl1 tl2 = Gt then Gt else Incomparable
+ | _, _ -> Incomparable
+ ) else Incomparable
+ | Eq ->
+ let r = aux t1 t2 in
+ if r = Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+(* if cmp tl1 tl2 = Gt then Gt else Incomparable *)
+ cmp tl1 tl2
+ | _, _ -> Incomparable
+ ) else r
+ | res -> res
+;;
+
+