more detailed proof term output;
tuned signature;