It is very hard, in general, to predict whether a certain automatic prover can or cannot discharge a given proof obligation within a given amount of time. (This is also the case for many other automatic first order theorem provers.) Therefore applying the 11 configurations in a trial and error fashion is often frustrating.
The following guidelines may be useful:
Add PP restricted, P0, and ML to the auto-tactic. If the auto-tactic runs out of memory, remove PP.
If the model is small, add PP after lasso and P1 to the auto-tactic.
Whenever you think that the current proof obligation should be discharged automatically, invoke the auto-tactic (
) instead of some particular automatic prover.
If the auto-tactic fails, it is usually best to simplify the proof obligation in some way. The most important ways of simplifying the proof obligation are:
Remove unnecessary hypotheses; add required hypotheses that have been missing.
Create a case distinction
Instantiate quantifiers.
Apply ae (abstract expression) to replace complicated expressions with fresh variables.
You can also apply one of the automatic provers. They may be more successful than the auto-tactic because they have a longer timeout.
The configurations that act on more than the selected hypotheses (unrestricted P1, PP and ML) become useless when the model grows.
When everything fails, try to solve the proof obligation manually by clicking on the red symbols.
You may discover that some assumption was missing.
You may complete the proof.
If you observe that a valid proof obligation cannot be proved manually, please send a bug report (4.2.9).