+ let superpose_literal id vl table is_pos (bag,maxvar,pre,post,acc) (lit,sel) =
+ let clause_ctx =
+ if is_pos then fun l -> [],pre@[l,true]@post
+ else fun l -> pre@[l,true]@post,[]
+ in
+ let bag, maxvar, newc =
+ superposition_with_table bag maxvar id vl lit is_pos clause_ctx table
+ in
+ if post = [] then bag,maxvar,pre@[lit,sel],[],newc@acc
+ else bag,maxvar,pre@[lit,sel],List.tl post,newc@acc
+ ;;
+
+