What if you don't make money from it now, but use what you learned to profit ten minutes later? How about 10 days later? Or 10 years later?

Non-commercial use for something that is directly involved in the production of something else is fairly easy to determine; it depends on whether that something else is sold for money or not.

But for analytical software like this prover, you could indirectly use it to improve something that is sold for money, but the process of improvement is not necessarily a commercial transaction. It could be performed by students at a university, for example. I have in mind formal verification of program invariants, with potential identification of breaks, as an example.

Is there a direct link between you using this software under such a licence and then gaining monetary advantage (if not money directly itself)?

Using your process of improvement for me it is quite clear there would be.

[Perhaps the solver could be used to figure the applicability of the licence]

So if you make money by teaching, is that commercial?

Non-commercial is a terrible term, because it's simply too vague. You can simply say "well, MS will use a bit of discretion, and not sue someone for a marginal infringement". But it does feel a little dodgy.

"Commercial = I make money from using this; Non-commercial = NOT commercial "

False. There are cases where commercial was held to mean "any use by a for profit company, regardless if the use is research, earns money directly or indirectly", etc.

Admittedly with a European viewpoint, either common law based (UK) or administrative law based (France, Belgium), there have been cases where commercial was held to mean has the company benefited in a tangible way from its use of such licenced software.

Although if you speak to a lawyer I'm sure their training would immediately start highlighting this as a concern I don't believe it should be in the vast majority of cases. Wasn't there an article on HN a few days ago basically summarising this type of concern under "so sue me" (minus expletives)

I wonder what would happen here in Scotland - we don't have punitive damages so the most you can be awarded in court is the loss you can demonstrate to have suffered.

So if I use a software package commercially and don't pay for it perhaps the maximum I could be sued for in the local courts would be the license fee I didn't pay. If there is no "commercial" license then could it really be said that a loss has been suffered?

[NB I know contracts and licenses usually have clauses stating the jurisdiction where disputes will be resolved]

I suspect they would say that the commercial value of their solver, for which no publicly available license exists, is some very high dollar amount which they will offer to you as a courtesy.