mkbTT experiments

	DP+LPO					DP+KBO					none
	(1)	(2)	(3)	(4)		(1)	(2)	(3)	(4)		(1)	(2)	(3)	(4)
AD93-Z22	∞					∞					∞
ASK93-1	0.06	2	5	50		0.07	2	5	43		0.07	2	5	43
ASK93-2	∞					∞					∞
ASK93-5	∞					∞					∞
ASK93-6	36.84	402	915	62		36.29	402	915	61		39.64	402	915	64
BD94-collapse	0.09	3	12	44		0.11	3	12	45		0.11	3	12	45
BD94-peano	0.09	3	8	56		0.09	3	8	56		0.10	3	8	60
BD94-sqrt	0.03	0	4	0		0.03	0	4	0		0.03	0	4	0
BGK94-D08	111.51	64	1627	40		116.01	64	1671	40		121.59	64	1646	43
BGK94-D10	125.31	2	1423	35		119.68	3	1292	32		123.42	3	1282	35
BGK94-D12	151.22	13	1489	35		101.52	14	1170	34		107.32	14	1160	37
BGK94-D16	126.08	17	1304	36		122.05	18	1232	34		128.02	18	1222	36
BGK94-M08	∞					∞					∞
BGK94-M10	∞					∞					∞
BGK94-M12	∞					∞					∞
BGK94-M14	∞					∞					∞
BGK94-Z22W	∞					∞					∞
BH96-fac8_theory	0.32	15	34	69		0.32	15	34	66		0.36	15	34	69
Chr89-A2	37.01	1	431	26		⊥					38.22	1	438	29
Chr89-A24	∞					∞					∞
Chr89-A3	140.34	32	1630	31		150.78	106	1607	28		157.59	106	1607	30
HR94-1	∞					∞					∞
HR94-2	∞					∞					∞
KH11-aufgabe3-2	0.02	1	2	50		0.02	1	2	50		0.02	1	2	50
KH11-aufgabe3-3	0.03	0	3	0		0.02	0	3	0		0.03	0	3	0
KH11-fggx	0.08	2	6	38		0.08	2	6	50		0.08	2	6	38
KH11-fib	2.67	49	157	65		2.66	53	159	65		3.00	49	157	69
KH11-kb-fail	⊥					⊥					⊥
KH11-kb-fail1	⊥					⊥					⊥
KH11-lr-theory	5.01	7	91	29		4.92	8	92	30		5.18	8	92	33
KH11-rl-theory	23.26	7	208	21		408.98	0	490	8		429.91	0	490	10
KK99-linear_assoc	0.10	3	6	50		0.10	3	6	60		0.10	3	6	60
Les83-fib	0.65	14	38	65		0.65	14	38	65		0.70	14	38	67
Les83-subset	0.35	5	27	51		0.35	5	27	51		0.37	5	27	54
LS06-CGE4	∞					∞					∞
LS06-CGE5	∞					∞					∞
LS94-G0	1.59	7	47	47		1.60	7	47	46		1.64	7	47	48
LS94-G1	∞					∞					∞
LS94-G2	∞					∞					∞
LS94-G3	∞					∞					∞
LS94-P1	∞					∞					∞
OKW95-dt1_theory	2.90	55	154	64		2.94	55	154	65		3.12	55	154	66
Sim91-sims2	∞					∞					∞
SK90-3.01	3.94	15	114	38		4.41	17	119	37		4.62	17	119	39
SK90-3.02	0.10	1	7	60		0.10	1	7	60		0.11	1	7	55
SK90-3.03	1.61	4	48	34		2.05	6	56	34		2.19	6	56	37
SK90-3.04	4.33	5	103	34		∞					4.51	5	103	37
SK90-3.05	80.73	7	463	12		189.30	7	682	10		81.99	7	463	13
SK90-3.06	15.08	11	306	39		14.69	11	306	38		16.08	11	306	43
SK90-3.07	69.37	22	699	30		68.37	22	699	30		73.05	22	699	33
SK90-3.08	0.12	2	10	25		0.12	2	10	25		0.13	2	10	31
SK90-3.09	∞					∞					∞
SK90-3.10	0.06	0	8	17		0.06	0	8	17		0.06	0	8	17
SK90-3.11	0.08	0	7	38		0.08	0	7	50		0.08	0	7	50
SK90-3.12	⊥					⊥					⊥
SK90-3.13	0.47	15	33	66		0.48	15	33	67		0.50	15	33	68
SK90-3.14	0.49	9	34	61		0.48	9	34	63		0.51	9	34	63
SK90-3.15	0.26	3	16	46		0.26	3	16	46		0.27	3	16	44
SK90-3.16	0.04	0	5	0		0.04	0	5	0		0.04	0	5	0
SK90-3.17	0.18	3	10	44		0.19	4	10	47		0.20	4	10	45
SK90-3.18	0.77	9	35	53		0.76	10	35	53		0.86	10	35	57
SK90-3.19	2.07	35	89	69		2.04	35	89	68		2.17	35	89	70
SK90-3.20	1.24	31	90	63		1.26	31	90	63		1.35	31	90	65
SK90-3.21	0.61	7	43	56		0.62	7	43	55		0.64	7	43	58
SK90-3.22	⊥					∞					∞
SK90-3.23	1.03	16	48	48		1.04	16	48	47		1.10	16	48	49
SK90-3.24	0.09	3	8	44		0.09	3	8	44		0.09	3	8	44
SK90-3.25	0.07	1	4	57		0.07	1	4	57		0.08	1	4	63
SK90-3.26	∞					∞					∞
SK90-3.27	45.71	2	151	27		34.27	2	121	20		38.16	2	121	26
SK90-3.28	77.52	11	1238	53		198.84	122	2398	48		223.80	122	2410	52
SK90-3.29	3.69	69	170	47		3.71	69	170	47		3.91	69	170	49
SK90-3.30	0.05	0	4	20		0.05	0	4	20		0.05	0	4	20
SK90-3.31	0.04	1	4	25		0.04	1	4	25		0.04	1	4	25
SK90-3.32	0.03	0	4	0		0.03	0	4	0		0.03	0	4	0
SK90-3.33	0.04	0	5	0		0.04	0	5	0		0.04	0	5	0
slothrop-ackermann	0.11	4	8	45		0.10	4	8	50		0.12	4	8	50
slothrop-cge	32.48	14	371	39		30.07	14	370	40		33.45	14	371	41
slothrop-cge3	∞					∞					∞
slothrop-endo	4.41	13	116	46		3.99	10	113	47		4.55	13	116	47
slothrop-equiv_proofs	6.14	4	86	76		6.94	5	96	73		7.34	5	96	74
slothrop-equiv_proofs_or	6.08	4	86	75		6.98	5	96	73		7.32	5	96	74
slothrop-fgh	0.03	0	3	33		0.03	0	3	33		0.03	0	3	33
slothrop-groups	1.14	3	35	38		1.15	3	35	37		1.18	3	35	39
slothrop-groups_conj	0.64	3	26	42		0.64	3	26	42		0.65	3	26	43
slothrop-hard	0.03	1	3	67		0.03	1	3	67		0.03	1	3	67
slothrop-nlp-2b	∞					∞					∞
TPDB-AProVE_07_thiemann27	∞					∞					∞
TPDB-secr10	8.32	7	106	27		∞					∞
TPDB-secr4	22.54	22	325	31		20.14	25	310	35		22.47	26	308	40
TPDB-z115	25.59	44	348	28		84.78	115	690	20		91.06	115	690	25
TPTP-BOO027-1_theory	0.13	0	7	46		0.13	0	7	38		0.14	0	7	50
TPTP-COL053-1_theory	0.03	1	2	33		0.03	1	2	67		0.03	1	2	67
TPTP-COL056-1_theory	0.11	5	10	55		0.11	5	10	55		0.11	5	10	64
TPTP-COL060-1_theory	0.06	0	4	67		0.06	0	4	67		0.07	0	4	71
TPTP-COL085-1_theory	0.01	0	1	0		0.01	0	1	0		0.01	0	1	0
TPTP-GRP010-4_theory	14.41	26	295	34		14.24	28	295	33		14.92	28	295	36
TPTP-GRP011-4_theory	2.37	6	77	49		2.39	6	77	49		2.54	6	77	52
TPTP-GRP012-4_theory	0.81	3	22	21		0.80	3	22	21		0.83	3	22	23
TPTP-GRP393-2_theory	0.04	1	2	25		0.03	1	2	33		0.04	1	2	50
TPTP-GRP394-3_theory	1.14	3	35	37		1.16	3	35	38		1.16	3	35	38
TPTP-GRP454-1_theory	4.72	6	100	33		8.92	15	177	37		9.60	15	177	42
TPTP-GRP457-1_theory	4.68	6	100	33		8.90	15	177	37		9.67	15	177	42
TPTP-GRP460-1_theory	13.82	7	157	16		22.21	22	202	17		22.93	22	202	20
TPTP-GRP463-1_theory	13.91	7	157	16		22.04	22	202	17		23.01	22	202	20
TPTP-GRP481-1_theory	∞					134.24	24	471	13		141.10	24	471	15
TPTP-GRP484-1_theory	∞					449.41	0	1004	35		475.10	0	1004	38
TPTP-GRP487-1_theory	∞					137.49	0	759	19		144.21	0	759	23
TPTP-GRP490-1_theory	∞					371.88	1	1176	12		391.44	1	1176	16
TPTP-GRP493-1_theory	∞					88.23	0	362	20		93.69	0	362	22
TPTP-GRP496-1_theory	457.54	7	722	13		125.13	27	647	20		134.63	27	647	24
TPTP-HWC004-1_theory	0.24	2	16	21		0.24	2	16	21		0.24	2	16	21
TPTP-HWC004-2_theory	0.11	2	12	36		0.11	2	12	45		0.11	2	12	45
TPTP-SWV262-2_theory	0.09	3	7	67		0.10	3	7	60		0.11	3	7	64
WS06-proofreduction	225.26	31	743	90		228.75	31	745	89		237.90	31	763	89
successes	83					85					87
average time	23.16					39.58					40.1
total termination %	36					29					33

Explanation:

(1)	total time
(2)	number of processes
(3)	number of termination checks
(4)	percentage of time spent on termination checks