+ let infer_left bag maxvar goal (_alist, atable) =
+ (* We superpose the goal with active clauses *)
+ let bag, maxvar, new_goals =
+ superposition_with_table bag maxvar goal atable
+ in
+ (* We demodulate the goal with active clauses *)
+ let bag, new_goals =
+ List.fold_left
+ (fun (bag, acc) g ->
+ let bag, g = demodulate bag g atable in
+ bag, g :: acc)
+ (bag, []) new_goals
+ in
+ bag, maxvar, List.rev new_goals
+ ;;
+