Arne Keller

> I nearly always get a dialog listing (only) the nodes where the caching failed (in the screenshot, actually two of the three goals are closed via cache): I changed...

> And there is a strange class `Watchdog`, which says it tries to detect deadlocks, but this makes no sense because Java has a built-in mechanism for deadlock detection. The...

I think the other bug you are referring to is fixed by #3438

I really don't understand the test failure. None of the changes in this PR change anything relevant to normal proof search. I'll do a no-op commit and push again.

I am confused by the save abbreviations dialog. It suggests to save this data as a `.proof`: ``` p::==i_arr_5 d::==i_arr_2 l::==i_arr_8 ```

How does the load abbreviations functionality work? I selected my previously saved file, but no abbreviations were restored.

The abbreviations transfer does not work for program variables. I think they would need to be compared by name, not by identity.

> How is determined which is the "main" branch and which are the "side" branches. Currently only the "Normal Execution [...]" branch is considered the main branch.

The implementation has been updated to also consider e.g. the TRUE branch of `cut_direct` as the main branch:  This is achieved using a new goal template tagging mechanism.

I agree that selecting an open goal is more useful than selecting the root node. Don't know why it was changed. I think the fix would be a call to...