-- This line, and those below, will be ignored--
M tactics/paramodulation/saturation.ml
(* equality-selection related globals *)
let use_fullred = ref true;;
(* equality-selection related globals *)
let use_fullred = ref true;;
-let weight_age_ratio = ref 5 (* 5 *);; (* settable by the user *)
+let weight_age_ratio = ref 4 (* 5 *);; (* settable by the user *)
let weight_age_counter = ref !weight_age_ratio ;;
let symbols_ratio = ref 0 (* 3 *);;
let symbols_counter = ref 0;;
let weight_age_counter = ref !weight_age_ratio ;;
let symbols_ratio = ref 0 (* 3 *);;
let symbols_counter = ref 0;;