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:

  1. Scrutinize if you have all assumptions and correct controls for your model.
  2. Annotate loops and/or differential equations with appropriate @invariant(...) formulas.
  3. Click to decompose the formula and either find a proof or how to bugfix your model.
  4. Exploit system insights to find an easier decomposition of your formula.
  5. Try other proof strategies or provide a domain-specific tactic performing proof search.