I am getting an error message that I cannot understand. I am trying to prove a seemingly simple formula where I have, among others, yp < 0 and yp >= 0 on the left hand side. When I try to close the branch with QE, I get an error saying Input {48, MemoryConstrained[...]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]}. What does this error message mean? If I hide some of the sequents, then I can close the branch with QE, but I am a bit suprised that I have to. I think that I have managed to close similar branched before; what is special about this formula?

KeYmaera X version 5.0.1
Operating System:
Windows 10 10.0
Java JVM:
Oracle Corporation 17.0.1 with 64 bits
Java Home:
C:\Program Files\Java\jdk-17.0.1

Input {48, MemoryConstrained[TimeConstrained[Reduce[ForAll[{kyxyp, kyxxp, kyxx, kyxwl, kyxvpMax, kyxv, kyxt$u$, kyxrange, kyxptol, kyxle, kyxaMin, kyxaMax, kyxa, kyxT}, Implies[And[Greater[kyxwl, 0], And[Greater[kyxle, 0], And[Greater[kyxvpMax, 0], And[Greater[kyxrange, 0], And[Greater[kyxptol, 0], And[Less[kyxaMin, 0], And[Greater[kyxaMax, 0], And[Less[Times[kyxT, kyxvpMax], kyxwl], And[Less[Times[kyxT, Minus[0]], kyxwl], And[Greater[kyxxp, kyxrange], And[Greater[kyxT, 0], And[Less[kyxyp, 0], And[GreaterEqual[kyxt$u$, 0], And[ForAll[{kyxs$u$}, Implies[And[LessEqual[0, kyxs$u$], LessEqual[kyxs$u$, kyxt$u$]], And[LessEqual[Plus[kyxs$u$, 0], kyxT], GreaterEqual[Plus[Times[kyxaMax, kyxs$u$], kyxv], 0]]]], And[LessEqual[Subtract[kyxx, kyxle], kyxxp], And[GreaterEqual[kyxyp, 0], And[LessEqual[kyxyp, kyxwl], And[Greater[kyxyp, kyxwl], And[Implies[Less[kyxyp, 0], Greater[Plus[Divide[Times[Times[kyxaMax, Minus[Divide[kyxyp, kyxvpMax]]], Minus[Divide[kyxyp, kyxvpMax]]], 2], Times[kyxv, Minus[Divide[kyxyp, kyxvpMax]]]], Plus[Subtract[kyxxp, kyxx], kyxle]]], And[Greater[0, 0], And[Less[0, kyxvpMax], And[LessEqual[kyxaMin, kyxa], And[LessEqual[kyxa, kyxaMax], And[Implies[Greater[kyxyp, kyxwl], Greater[Plus[Divide[Times[Times[kyxaMax, Divide[Subtract[kyxyp, kyxwl], Minus[0]]], Divide[Subtract[kyxyp, kyxwl], Minus[0]]], 2], Times[kyxv, Divide[Subtract[kyxyp, kyxwl], Minus[0]]]], Plus[Subtract[kyxxp, kyxx], kyxle]]], Implies[And[GreaterEqual[kyxyp, 0], LessEqual[kyxyp, kyxwl]], Greater[Subtract[kyxx, kyxle], kyxxp]]]]]]]]]]]]]]]]]]]]]]]]]], Greater[Plus[Divide[Times[Times[kyxaMax, Divide[Subtract[kyxyp, kyxwl], Minus[0]]], Divide[Subtract[kyxyp, kyxwl], Minus[0]]], 2], Times[Plus[Times[kyxaMax, kyxt$u$], kyxv], Divide[Subtract[kyxyp, kyxwl], Minus[0]]]], Plus[Subtract[kyxxp, Plus[Plus[Times[kyxaMax, Divide[Power[kyxt$u$, 2], 2]], Times[kyxv, kyxt$u$]], kyxx]], kyxle]]]], {}, Reals], 5], 8000000000]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]} in _QE in _QE at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.runExpr(SequentialInterpreter.scala:296) at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter.runExpr(SequentialInterpreter.scala:773) at edu.cmu.cs.ls.keymaerax.bellerophon.ExhaustiveSequentialInterpreter.runExpr(SequentialInterpreter.scala:813) at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.apply(SequentialInterpreter.scala:45) at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.runExpr(SequentialInterpreter.scala:291) at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter.runExpr(SequentialInterpreter.scala:773) at edu.cmu.cs.ls.keymaerax.bellerophon.ExhaustiveSequentialInterpreter.runExpr(SequentialInterpreter.scala:813) at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.apply(SequentialInterpreter.scala:45) at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.runExpr(SequentialInterpreter.scala:308) at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter.runExpr(SequentialInterpreter.scala:773) at edu.cmu.cs.ls.keymaerax.bellerophon.ExhaustiveSequentialInterpreter.runExpr(SequentialInterpreter.scala:813) at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.apply(SequentialInterpreter.scala:45) at edu.cmu.cs.ls.keymaerax.hydra.BellerophonTacticExecutor$$anon$1.call(BellerophonTacticExecutor.scala:128) at edu.cmu.cs.ls.keymaerax.hydra.BellerophonTacticExecutor$$anon$1.call(BellerophonTacticExecutor.scala:125) at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264) at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:539) at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264) at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136) at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635) at java.base/java.lang.Thread.run(Thread.java:833) Caused by: Input {48, MemoryConstrained[TimeConstrained[Reduce[ForAll[{kyxyp, kyxxp, kyxx, kyxwl, kyxvpMax, kyxv, kyxt$u$, kyxrange, kyxptol, kyxle, kyxaMin, kyxaMax, kyxa, kyxT}, Implies[And[Greater[kyxwl, 0], And[Greater[kyxle, 0], And[Greater[kyxvpMax, 0], And[Greater[kyxrange, 0], And[Greater[kyxptol, 0], And[Less[kyxaMin, 0], And[Greater[kyxaMax, 0], And[Less[Times[kyxT, kyxvpMax], kyxwl], And[Less[Times[kyxT, Minus[0]], kyxwl], And[Greater[kyxxp, kyxrange], And[Greater[kyxT, 0], And[Less[kyxyp, 0], And[GreaterEqual[kyxt$u$, 0], And[ForAll[{kyxs$u$}, Implies[And[LessEqual[0, kyxs$u$], LessEqual[kyxs$u$, kyxt$u$]], And[LessEqual[Plus[kyxs$u$, 0], kyxT], GreaterEqual[Plus[Times[kyxaMax, kyxs$u$], kyxv], 0]]]], And[LessEqual[Subtract[kyxx, kyxle], kyxxp], And[GreaterEqual[kyxyp, 0], And[LessEqual[kyxyp, kyxwl], And[Greater[kyxyp, kyxwl], And[Implies[Less[kyxyp, 0], Greater[Plus[Divide[Times[Times[kyxaMax, Minus[Divide[kyxyp, kyxvpMax]]], Minus[Divide[kyxyp, kyxvpMax]]], 2], Times[kyxv, Minus[Divide[kyxyp, kyxvpMax]]]], Plus[Subtract[kyxxp, kyxx], kyxle]]], And[Greater[0, 0], And[Less[0, kyxvpMax], And[LessEqual[kyxaMin, kyxa], And[LessEqual[kyxa, kyxaMax], And[Implies[Greater[kyxyp, kyxwl], Greater[Plus[Divide[Times[Times[kyxaMax, Divide[Subtract[kyxyp, kyxwl], Minus[0]]], Divide[Subtract[kyxyp, kyxwl], Minus[0]]], 2], Times[kyxv, Divide[Subtract[kyxyp, kyxwl], Minus[0]]]], Plus[Subtract[kyxxp, kyxx], kyxle]]], Implies[And[GreaterEqual[kyxyp, 0], LessEqual[kyxyp, kyxwl]], Greater[Subtract[kyxx, kyxle], kyxxp]]]]]]]]]]]]]]]]]]]]]]]]]], Greater[Plus[Divide[Times[Times[kyxaMax, Divide[Subtract[kyxyp, kyxwl], Minus[0]]], Divide[Subtract[kyxyp, kyxwl], Minus[0]]], 2], Times[Plus[Times[kyxaMax, kyxt$u$], kyxv], Divide[Subtract[kyxyp, kyxwl], Minus[0]]]], Plus[Subtract[kyxxp, Plus[Plus[Times[kyxaMax, Divide[Power[kyxt$u$, 2], 2]], Times[kyxv, kyxt$u$]], kyxx]], kyxle]]]], {}, Reals], 5], 8000000000]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]}
at edu.cmu.cs.ls.keymaerax.tools.qe.JLinkMathematicaCommandRunner.$anonfun$getAnswer$1(MathematicaCommandRunner.scala:150)
at edu.cmu.cs.ls.keymaerax.tools.qe.MathematicaConversion$.importResult(MathematicaConversion.scala:33)
at edu.cmu.cs.ls.keymaerax.tools.qe.JLinkMathematicaCommandRunner.getAnswer(MathematicaCommandRunner.scala:137)
at edu.cmu.cs.ls.keymaerax.tools.qe.JLinkMathematicaCommandRunner.doRun(MathematicaCommandRunner.scala:87)
at edu.cmu.cs.ls.keymaerax.tools.qe.BaseMathematicaCommandRunner.run(MathematicaCommandRunner.scala:51)
at edu.cmu.cs.ls.keymaerax.tools.qe.MathematicaQETool.singleQE(MathematicaQETool.scala:49)
at edu.cmu.cs.ls.keymaerax.tools.qe.MathematicaQETool.quantifierElimination(MathematicaQETool.scala:34)
at edu.cmu.cs.ls.keymaerax.core.Provable$.proveArithmetic(Proof.scala:521)
at edu.cmu.cs.ls.keymaerax.pt.ElidingProvable$.proveArithmetic(TermProvable.scala:439)
at edu.cmu.cs.ls.keymaerax.pt.ElidingProvable$.proveArithmeticLemma(TermProvable.scala:442)
at edu.cmu.cs.ls.keymaerax.pt.ProvableSig$.proveArithmeticLemma(TermProvable.scala:371)
at edu.cmu.cs.ls.keymaerax.tools.ext.Mathematica.$anonfun$qe$1(Mathematica.scala:132)
at edu.cmu.cs.ls.keymaerax.tools.ext.MathematicaQEToolBridge.$anonfun$run$1(MathematicaQEToolBridge.scala:29)
at edu.cmu.cs.ls.keymaerax.tools.ext.JLinkMathematicaLink.$anonfun$run$2(MathematicaLink.scala:316)
at edu.cmu.cs.ls.keymaerax.tools.ext.ToolExecutor.$anonfun$makeFuture$1(ToolExecutor.scala:111)
... 6 more