Improved statistics reporting

Improved the way statistics are reported. Previously we might have something like

Serkr 0.1.0, (C) 2015-2016 Mikko Aarnos
Initial clauses: 28
info time 1009 iterations 713 used 51 unused 1331 sp 2176 ef 0 er 0 trivial 160 fs 661 bs 0
info time 2001 iterations 1105 used 56 unused 2624 sp 3889 ef 0 er 0 trivial 188 fs 1048 bs 0
info time 3002 iterations 1391 used 58 unused 3246 sp 4813 ef 0 er 0 trivial 204 fs 1332 bs 0
info time 4003 iterations 1612 used 58 unused 3025 sp 4813 ef 0 er 0 trivial 204 fs 1553 bs 0
info time 5001 iterations 1833 used 58 unused 2804 sp 4813 ef 0 er 0 trivial 204 fs 1774 bs 0
info time 6006 iterations 2045 used 58 unused 2592 sp 4813 ef 0 er 0 trivial 204 fs 1986 bs 0
info time 7005 iterations 2271 used 58 unused 2366 sp 4813 ef 0 er 0 trivial 204 fs 2212 bs 0
info time 8003 iterations 2526 used 58 unused 2111 sp 4813 ef 0 er 0 trivial 204 fs 2467 bs 0
info time 9001 iterations 2875 used 74 unused 2889 sp 6080 ef 0 er 0 trivial 344 fs 2799 bs 1
info time 10001 iterations 3289 used 90 unused 3872 sp 7622 ef 0 er 0 trivial 489 fs 3197 bs 1
info time 11001 iterations 3793 used 128 unused 4934 sp 9216 ef 0 er 0 trivial 517 fs 3663 bs 1
info time 12007 iterations 4231 used 152 unused 6671 sp 11391 ef 0 er 0 trivial 517 fs 4077 bs 1
info time 13002 iterations 4577 used 164 unused 7535 sp 12601 ef 0 er 0 trivial 517 fs 4411 bs 1
info time 14001 iterations 4855 used 164 unused 7257 sp 12601 ef 0 er 0 trivial 517 fs 4689 bs 1
info time 15001 iterations 5199 used 164 unused 6913 sp 12601 ef 0 er 0 trivial 517 fs 5033 bs 1
info time 16007 iterations 5550 used 185 unused 8207 sp 14246 ef 0 er 0 trivial 517 fs 5363 bs 1
info time 17001 iterations 5869 used 193 unused 8581 sp 14939 ef 0 er 0 trivial 517 fs 5674 bs 1
info time 18003 iterations 6167 used 193 unused 8283 sp 14939 ef 0 er 0 trivial 517 fs 5972 bs 1
info time 19001 iterations 6520 used 197 unused 8225 sp 15234 ef 0 er 0 trivial 517 fs 6321 bs 1
info time 20003 iterations 6808 used 200 unused 8152 sp 15449 ef 0 er 0 trivial 517 fs 6606 bs 1
info time 21001 iterations 7129 used 226 unused 10247 sp 17912 ef 0 er 0 trivial 564 fs 6900 bs 2
info time 22003 iterations 7483 used 244 unused 11624 sp 19706 ef 0 er 0 trivial 627 fs 7236 bs 2
info time 23004 iterations 7807 used 268 unused 13504 sp 21910 ef 0 er 0 trivial 627 fs 7536 bs 2
info time 24001 iterations 8103 used 287 unused 14737 sp 23453 ef 0 er 0 trivial 641 fs 7813 bs 2
info time 25002 iterations 8280 used 289 unused 14764 sp 23657 ef 0 er 0 trivial 641 fs 7988 bs 2
info time 26006 iterations 8449 used 290 unused 14629 sp 23691 ef 0 er 0 trivial 641 fs 8156 bs 2
info time 27002 iterations 8680 used 296 unused 14846 sp 24139 ef 0 er 0 trivial 641 fs 8381 bs 2
info time 28002 iterations 8870 used 300 unused 14940 sp 24478 ef 0 er 0 trivial 696 fs 8567 bs 2
info time 29001 iterations 9118 used 307 unused 15096 sp 24907 ef 0 er 0 trivial 721 fs 8808 bs 2
info time 30001 iterations 9339 used 307 unused 14875 sp 24907 ef 0 er 0 trivial 721 fs 9029 bs 2
info time 31010 iterations 9542 used 308 unused 14690 sp 24957 ef 0 er 0 trivial 753 fs 9231 bs 2
info time 32001 iterations 9773 used 325 unused 14946 sp 25768 ef 0 er 0 trivial 1077 fs 9444 bs 3
Theorem
Time elapsed (in ms): 32238

which isn't terribly informative. Now we have

% SZS status Theorem for examples/SWV236+1.p
% SZS output None for examples/SWV236+1.p : Proof output is not yet supported

% Time elapsed (in ms): 22832
% Initial clauses: 28
% Analyzed clauses: 9756
%   Trivial: 973
%   Forward subsumed: 8447
%   Nonredundant: 336
% Backward subsumptions: 5
% Inferred clauses: 26197
%   Superposition: 26197
%   Equality factoring: 0
%   Equality resolution: 0
% Nontrivial inferred clauses: 24894

which should be better. The current output style should also comform (mostly) to the SZS ontology. The only real missing part is the proof output which is going to need some work.

mAarnos / Serkr

Improved statistics reporting #16