[andrepd]

I read both those papers ;)

I guess that you can think of our algorithm as lazy SAT modulo quantified first order logic, with the crucial difference that first order logic is undecidable. But anyway in this case the "decision procedure for T" would just be checking whether any two complementary literals which are true in the model are unifiable, which is decidable.

Paper: http://www.cs.man.ac.uk/~korovink/my_pub/inst_gen_modular.pd...