mkbTT					MaxComp		Slothrop
	dt					LPO
	(1)	(2)	(3)	(4)		(1)		(1)
AD93-Z22	∞					⊥		∞
ASK93-1	0.06	4	2	5		0.03		1.16
ASK93-2	∞					∞		∞
ASK93-5	∞					⊥		∞
ASK93-6	31.15	17	402	915		0.69		21.82
BD94-collapse	0.08	8	3	12		0.01		1.19
BD94-peano	0.08	5	3	8		0.00		1.39
BD94-sqrt	0.02	5	0	4		0.00		1.01
BGK94-D08	75.86	116	30	1710		0.49		∞
BGK94-D10	21.92	95	2	707		0.61		∞
BGK94-D12	22.73	95	11	722		0.85		∞
BGK94-D16	23.74	96	11	730		34.01		∞
BGK94-M08	∞					0.17		12.14
BGK94-M10	∞					0.57		29.41
BGK94-M12	∞					39.57		39.39
BGK94-M14	∞					∞		38.85
BGK94-Z22W	∞					⊥		∞
BH96-fac8_theory	0.27	7	15	34		0.00		3.17
Chr89-A2	24.16	109	1	442		0.72		266.22
Chr89-A24	∞					∞		∞
Chr89-A3	76.52	65	75	1467		2.34		450.40
HR94-1	∞					⊥		∞
HR94-2	∞					⊥		∞
KK99-linear_assoc	0.08	3	3	6		0.00		0.68
Les83-fib	0.50	10	14	38		0.00		3.82
Les83-subset	0.27	13	5	27		0.01		4.94
LS06-CGE4	⊥					∞		∞
LS06-CGE5	∞					∞		∞
LS94-G0	1.04	23	7	47		0.03		8.42
LS94-G1	∞					∞		∞
LS94-G2	∞					⊥		∞
LS94-G3	∞					⊥		∞
LS94-P1	∞					∞		∞
OKW95-dt1_theory	2.10	18	55	154		40.76		8.36
Sim91-sims2	∞					⊥		∞
SK90-3.01	4.51	46	19	161		0.06		27.48
SK90-3.02	0.08	4	1	7		0.01		1.04
SK90-3.03	34.03	89	15	318		0.75		6.91
SK90-3.04	2.72	40	5	103		1.40		∞
SK90-3.05	9.54	67	12	255		0.24		451.55
SK90-3.06	10.70	71	11	306		0.63		∞
SK90-3.07	70.75	160	17	680		2.18		∞
SK90-3.08	0.09	9	2	10		0.01		1.13
SK90-3.09	∞					⊥		∞
SK90-3.10	0.04	9	0	8		0.00		0.77
SK90-3.11	0.06	7	0	7		0.01		1.10
SK90-3.12	0.61	15	5	25		⊥		⊥
SK90-3.13	0.37	7	15	33		0.01		1.35
SK90-3.14	0.40	10	9	34		0.01		1.85
SK90-3.15	0.19	11	3	16		⊥		1.51
SK90-3.16	0.03	6	0	5		0.00		0.63
SK90-3.17	0.14	6	4	10		0.01		1.36
SK90-3.18	0.57	12	10	35		0.01		4.81
SK90-3.19	1.46	11	35	89		0.06		3.27
SK90-3.20	0.96	13	31	90		0.95		3.46
SK90-3.21	0.49	13	7	43		0.02		132.89
SK90-3.22	∞					3.20		∞
SK90-3.23	0.81	19	16	48		92.83		6.69
SK90-3.24	0.07	5	3	8		0.01		1.50
SK90-3.25	0.06	3	1	4		0.30		1.22
SK90-3.26	∞					∞		∞
SK90-3.27	30.36	39	5	138		17.71		446.21
SK90-3.28	154.06	42	121	2402		15.93		229.29
SK90-3.29	2.81	15	69	170		0.54		6.81
SK90-3.30	0.04	6	0	4		0.01		0.63
SK90-3.31	0.03	4	1	4		0.00		0.63
SK90-3.32	0.02	5	0	4		0.00		0.58
SK90-3.33	0.03	6	0	5		0.00		1.09
slothrop-ackermann	0.09	4	4	8		0.00		1.45
slothrop-cge	6.69	38	11	170		∞		460.40
slothrop-cge3	45.17	49	35	694		∞		∞
slothrop-endo	3.04	30	13	116		0.46		9.96
slothrop-equiv_proofs	5.59	37	5	96		⊥		352.94
slothrop-fgh	0.03	6	0	3		0.00		0.55
slothrop-groups	0.73	21	3	35		0.05		2.73
slothrop-groups_conj	0.41	13	3	25		0.02		3.05
slothrop-hard	0.03	3	1	3		0.00		0.53
slothrop-nlp-2b	∞					⊥		∞
TPTP-BOO027-1_theory	0.09	6	0	6		0.01		1.35
TPTP-COL053-1_theory	0.03	2	1	2		0.00		0.52
TPTP-COL056-1_theory	0.10	4	5	10		0.00		0.66
TPTP-COL060-1_theory	0.06	3	0	4		⊥		1.27
TPTP-COL085-1_theory	0.01	2	0	1		0.00		0.49
TPTP-GRP010-4_theory	7.43	64	24	272		0.20		315.08
TPTP-GRP011-4_theory	1.72	26	6	77		0.06		42.81
TPTP-GRP012-4_theory	0.47	17	3	22		0.02		2.54
TPTP-GRP393-2_theory	0.04	2	1	2		0.00		0.51
TPTP-GRP394-3_theory	0.76	21	3	35		0.04		2.83
TPTP-GRP454-1_theory	4.03	41	12	120		2.04		∞
TPTP-GRP457-1_theory	4.01	41	12	120		2.04		∞
TPTP-GRP460-1_theory	40.66	131	11	380		0.69		∞
TPTP-GRP463-1_theory	40.86	131	11	380		1.41		∞
TPTP-GRP481-1_theory	30.16	125	19	278		1.87		130.81
TPTP-GRP484-1_theory	103.09	234	3	946		0.38		∞
TPTP-GRP487-1_theory	127.66	273	0	929		0.76		⊥
TPTP-GRP490-1_theory	87.93	229	29	648		0.63		∞
TPTP-GRP493-1_theory	97.48	221	0	463		4.19		562.93
TPTP-GRP496-1_theory	63.59	178	26	561		0.70		281.06
TPTP-HWC004-1_theory	0.21	11	2	16		0.02		1.56
TPTP-HWC004-2_theory	0.10	7	2	12		0.00		1.19
TPTP-SWV262-2_theory	0.08	4	3	7		0.02		0.75
WS06-proofreduction	183.39	91	31	763		⊥		∞
successes	80					77		67
average time	18.28					3.55		65.76

Explanation:

(1)	total time
(2)	control loop iterations
(3)	processes
(4)	termination checks