KeY - Bug?

[hstr]

Hallo,
ich versuche gerade Problem 1, Aufgabe a.) in KeY zu beweisen. Das funktioniert auch bis zu orLeft Regel,
aber dann müsste man ja für jeden der beiden Zweige die allLeft Regel anwenden, was aber nicht funktioniert.
Sobald man auf "\forall s x; p(x)" geht und "allLeft" auswählt, wird der ganze Proof Tree ausgegraut und man kann fast überhaupt nichts mehr machen.
(auch kein "Goal Back")
Interessanterweise funktioniert der Beweis aber mit dem automated proof search, obwohl der genau die gleichen Schritte ausführt.
Was läuft da schief?

[Nathan Wasser]

Es gab auf der Seite "Links, Papers, and Software" leider zwei verschiede Links zum KeY Tool, wobei nur eine korrekt funktioniert. Die Links zeigen nun beide auf die korrekte Version.

[hstr]

Ich habe die neuste Version von key-project.org verwendet.

[Nathan Wasser]

Das ist aber nicht die Version, die für FGdI3 verwendet werden soll.