X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=3491f40196f9a21d8c522d564a49554a1b71be63;hb=a0ca46dc450ef20ef14365c492d6d701ff153594;hp=f3afc16f46e1047615f089808d648d485623bf34;hpb=72aa8b2087285826b14fc39a389632f0317c51b6;p=helm.git diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index f3afc16f4..3491f4019 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -251,7 +251,7 @@ module Paramod (B : Orderings.Blob) = struct end else raise (Stop (Timeout (maxvar,bag))); - let use_age = weight_picks = (iterno / 6 + 1) in + let use_age = false && (weight_picks = (iterno / 6 + 1)) in let weight_picks = if use_age then 0 else weight_picks+1 in