mkbTT experiments

	(1)	(2)	(3)	(4)
AD93-Z22	∞
ASK93-1	0.07	4	2	5	proof
ASK93-2	∞
ASK93-5	∞
ASK93-6	30.06	17	402	915	proof
BD94-collapse	0.08	8	3	12	proof
BD94-peano	0.08	5	3	8	proof
BD94-sqrt	0.02	5	0	4	proof
BGK94-D08	71.52	116	31	1696	proof
BGK94-D10	21.77	97	2	709	proof
BGK94-D12	22.78	97	11	724	proof
BGK94-D16	24.06	98	11	732	proof
BGK94-M08	∞
BGK94-M10	∞
BGK94-M12	∞
BGK94-M14	∞
BGK94-Z22W	∞
BH96-fac8_theory	0.26	7	15	34	proof
Chr89-A2	23.50	106	1	439	proof
Chr89-A24	∞
Chr89-A3	64.96	70	42	1357	proof
HR94-1	∞
HR94-2	∞
KK99-linear_assoc	0.07	3	3	6	proof
KH11-aufgabe3-2	0.02	2	3	3	proof
KH11-aufgabe3-3	0.03	4	1	4	proof
KH11-fggx	0.13	5	2	11	proof
KH11-fib	7.92	13	49	124	proof
KH11-kb-fail1	⊥
KH11-kb-fail	⊥
KH11-rl-theory	∞
KH11-lr-theory	9.93	37	8	659	proof
Les83-fib	0.49	10	14	38	proof
Les83-subset	0.27	13	5	27	proof
LS06-CGE4	⊥
LS06-CGE5	∞
LS94-G0	1.05	23	7	47	proof
LS94-G1	∞
LS94-G2	∞
LS94-G3	∞
LS94-P1	∞
OKW95-dt1_theory	2.09	18	55	154	proof
Sim91-sims2	∞
SK90-3.01	4.32	46	17	159	proof
SK90-3.02	0.08	4	1	7	proof
SK90-3.03	20.50	75	14	246	proof
SK90-3.04	2.60	40	5	103	proof
SK90-3.05	9.27	67	12	255	proof
SK90-3.06	10.15	71	11	306	proof
SK90-3.07	∞
SK90-3.08	0.09	9	2	10	proof
SK90-3.09	∞
SK90-3.10	0.04	9	0	8	proof
SK90-3.11	0.06	7	0	7	proof
SK90-3.12	0.58	15	5	25	proof
SK90-3.13	0.37	7	15	33	proof
SK90-3.14	0.39	10	9	34	proof
SK90-3.15	0.18	11	3	16	proof
SK90-3.16	0.03	6	0	5	proof
SK90-3.17	0.14	6	3	10	proof
SK90-3.18	0.55	12	9	35	proof
SK90-3.19	1.48	11	35	89	proof
SK90-3.20	0.93	13	31	90	proof
SK90-3.21	0.49	13	7	43	proof
SK90-3.22	⊥
SK90-3.23	0.81	19	16	48	proof
SK90-3.24	0.07	5	3	8	proof
SK90-3.25	0.06	3	1	4	proof
SK90-3.26	∞
SK90-3.27	34.82	52	2	157	proof
SK90-3.28	56.08	44	10	1230	proof
SK90-3.29	2.74	15	69	170	proof
SK90-3.30	0.04	6	0	4	proof
SK90-3.31	0.03	4	1	4	proof
SK90-3.32	0.02	5	0	4	proof
SK90-3.33	0.03	6	0	5	proof
slothrop-ackermann	0.08	4	4	8	proof
slothrop-cge	6.72	38	11	170	proof
slothrop-cge3	43.70	49	35	694	proof
slothrop-endo	2.96	30	13	116	proof
slothrop-equiv_proofs	4.69	37	4	86	proof
slothrop-equiv_proofs_or	4.69	37	4	86	proof
slothrop-fgh	0.02	6	0	3	proof
slothrop-groups	0.74	21	3	35	proof
slothrop-groups_conj	0.40	13	3	25	proof
slothrop-hard	0.03	3	1	3	proof
slothrop-nlp-2b	∞
TPDB-secret2006-torpa-secr4	63.66	51	965	19	proof
TPDB-secret2006-torpa-secr10	0.09	6	0	6	proof
TPDB-zantema-z115	274.64	42	1781	67	proof
TPDB-thiemann27	∞
TPTP-BOO027-1_theory	0.09	6	0	6	proof
TPTP-COL053-1_theory	0.03	2	1	2	proof
TPTP-COL056-1_theory	0.10	4	5	10	proof
TPTP-COL060-1_theory	0.05	3	0	4	proof
TPTP-COL085-1_theory	0.01	2	0	1	proof
TPTP-GRP010-4_theory	7.23	64	24	272	proof
TPTP-GRP011-4_theory	1.68	26	6	77	proof
TPTP-GRP012-4_theory	0.45	17	3	22	proof
TPTP-GRP393-2_theory	0.04	2	1	2	proof
TPTP-GRP394-3_theory	0.74	21	3	35	proof
TPTP-GRP454-1_theory	2.17	36	6	71	proof
TPTP-GRP457-1_theory	2.20	36	6	71	proof
TPTP-GRP460-1_theory	44.77	141	9	340	proof
TPTP-GRP463-1_theory	44.11	141	9	340	proof
TPTP-GRP481-1_theory	49.63	184	9	339	proof
TPTP-GRP484-1_theory	134.41	327	2	745	proof
TPTP-GRP487-1_theory	144.21	209	2	759	proof
TPTP-GRP490-1_theory	391.44	340	1	1176	proof
TPTP-GRP493-1_theory	92.40	1	463	129	proof
TPTP-GRP496-1_theory	134.63	200	27	647	proof
TPTP-HWC004-1_theory	0.21	11	2	16	proof
TPTP-HWC004-2_theory	0.10	7	2	12	proof
TPTP-SWV262-2_theory	0.08	4	3	7	proof
WS06-proofreduction	174.90	91	31	743	proof
successes	87
average time	13.17

Explanation:

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