Changing switch -R <num> in &gla to mean the max allowed size of abstraction. Adding switch -Q <num> to stop when the number of objects exceeds num % _during_refinement_.

Adding resource limit to stop &gla when the number of remaining objects is less than R/2 during refinement.

Adding resource limit to stop &gla when the number of remaining objects is less than R/2 during refinement.

Changing dynamic CNF loading code to perform loading before propagate() as opposed to when the literal first implied in enqueue().