Changes

Summary

1. obsolete (see 94442fce40a5);
2. optional trace output;
3. prefer commands_accepted: fewer protocol messages;
4. prefer define_commands_bulk: fewer protocol messages;
5. clarified signature;
6. tuned signature -- prefer bulk messages;
7. tuned signature;
8. proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
9. more robust;
10. unused;
11. proper finished_theory status for result;
12. more central checkpoint;