As it is intermittent, I was wondering whether certain characteristics of the goal might cause this. Is your example reproducible? Larry > On 28 Nov 2025, at 15:56, Peter Lammich <lammich at in.tum.de> wrote: > > Just happened (on Isabelle2025) ... veriT keeping one CPU busy, and using tons of memory. Manually killing the process helps.