let symbols_counter = ref 0;;
(* non-recursive Knuth-Bendix term ordering by default *)
-(* Utils.compare_terms := Utils.nonrec_kbo;; *)
-Utils.compare_terms := Utils.ao;;
+Utils.compare_terms := Utils.nonrec_kbo;;
+(* Utils.compare_terms := Utils.ao;; *)
(* statistics... *)
let derived_clauses = ref 0;;