master is trying the default automatic proof strategy of KeYmaera X.
If it does not find a proof, then either your formula has a counterexample or master just was unable to find a proof within the timeouts.
Then:
- Scrutinize if you have all assumptions and correct controls for your model.
- Annotate loops and/or differential equations with appropriate
@invariant(...)
formulas.
- Click to decompose the formula and either find a proof or how to bugfix your model.
- Exploit system insights to find an easier decomposition of your formula.
- Try other proof strategies or provide a domain-specific tactic performing proof search.