mkbTT experiments

	none					rename					rename+					perm					perm+					none
	(1)	(2)	(3)	(4)		(1)	(2)	(3)	(4)		(1)	(2)	(3)	(4)		(1)	(2)	(3)	(4)		(1)	(2)	(3)	(4)		(1)	(2)	(3)	(4)
AD93-Z22	∞					∞					∞					∞					∞					∞
ASK93-1	0.06	4	2	5		0.07	4	2	5		0.07	4	2	5		0.06	4	2	5		0.07	4	2	5		0.07	4	2	5
ASK93-2	∞					∞					∞					∞					∞					∞
ASK93-5	∞					∞					∞					∞					∞					∞
ASK93-6	30.36	17	402	915		30.53	17	402	915		37.77	17	402	915		30.41	17	402	915		37.75	17	402	915		39.64	17	402	915
BD94-collapse	0.10	8	3	12		0.07	8	1	9		0.07	8	1	9		0.10	8	3	12		0.11	8	3	12		0.11	8	3	12
BD94-peano	0.10	5	3	8		0.10	5	3	8		0.10	5	3	8		0.11	5	3	8		0.10	5	3	8		0.10	5	3	8
BD94-sqrt	0.03	5	0	4		0.03	5	0	4		0.03	5	0	4		0.03	5	0	4		0.03	5	0	4		0.03	5	0	4
BGK94-D08	120.76	96	64	1646		120.13	96	64	1646		177.15	96	64	1646		119.97	96	64	1646		177.67	96	64	1646		121.59	96	64	1646
BGK94-D10	122.52	221	3	1282		123.66	221	3	1282		170.68	221	3	1282		124.12	221	3	1282		170.39	221	3	1282		123.42	221	3	1282
BGK94-D12	105.78	195	14	1160		106.80	195	14	1160		141.85	195	14	1160		107.04	195	14	1160		142.61	195	14	1160		107.32	195	14	1160
BGK94-D16	127.18	210	18	1222		126.93	210	18	1222		166.20	210	18	1222		127.73	210	18	1222		167.94	210	18	1222		128.02	210	18	1222
BGK94-M08	∞					∞					∞					∞					∞					∞
BGK94-M10	∞					∞					∞					∞					∞					∞
BGK94-M12	∞					∞					∞					∞					∞					∞
BGK94-M14	∞					∞					∞					∞					∞					∞
BGK94-Z22W	∞					∞					∞					∞					∞					∞
BH96-fac8_theory	0.36	7	15	34		0.36	8	15	34		0.36	8	15	34		0.36	7	15	34		0.37	7	15	34		0.36	7	15	34
Chr89-A2	28.82	108	1	422		28.87	108	1	422		38.50	108	1	438		28.88	108	1	422		36.66	108	1	422		38.22	108	1	438
Chr89-A24	∞					∞					∞					∞					∞					∞
Chr89-A3	122.56	63	119	1646		122.23	63	119	1646		157.62	66	106	1607		122.24	63	119	1646		156.67	63	119	1646		157.59	66	106	1607
HR94-1	∞					∞					∞					∞					∞					∞
HR94-2	∞					∞					∞					∞					∞					∞
KH11-aufgabe3-2	0.02	2	1	2		0.02	2	1	2		0.02	2	1	2		0.02	2	1	2		0.02	2	1	2		0.02	2	1	2
KH11-aufgabe3-3	0.02	4	0	3		0.03	4	0	3		0.03	4	0	3		0.02	4	0	3		0.03	4	0	3		0.03	4	0	3
KH11-fggx	0.08	5	2	6		0.08	5	2	6		0.09	5	2	6		0.08	5	2	6		0.09	5	2	6		0.08	5	2	6
KH11-fib	2.93	13	49	157		2.98	13	49	157		3.08	13	49	157		2.93	13	49	157		3.07	13	49	157		3.00	13	49	157
KH11-kb-fail	⊥					⊥					⊥					⊥					⊥					⊥
KH11-kb-fail1	⊥					⊥					⊥					⊥					⊥					⊥
KH11-lr-theory	5.04	37	8	92		4.88	37	8	92		5.39	37	8	92		4.93	37	8	92		5.35	37	8	92		5.18	37	8	92
KH11-rl-theory	438.09	179	0	490		422.54	179	0	490		465.50	179	0	490		395.76	179	0	490		432.47	179	0	490		429.91	179	0	490
KK99-linear_assoc	0.09	3	3	6		0.10	3	3	6		0.10	3	3	6		0.07	3	1	4		0.07	3	1	4		0.10	3	3	6
Les83-fib	0.69	10	14	38		0.69	10	14	38		0.74	10	14	38		0.69	10	14	38		0.72	10	14	38		0.70	10	14	38
Les83-subset	0.36	13	5	27		0.36	13	5	27		0.39	13	5	27		0.38	13	5	27		0.39	13	5	27		0.37	13	5	27
LS06-CGE4	∞					∞					∞					∞					∞					∞
LS06-CGE5	∞					∞					∞					∞					∞					∞
LS94-G0	1.59	23	7	47		1.62	23	7	47		1.67	23	7	47		1.05	20	3	31		1.05	20	3	31		1.64	23	7	47
LS94-G1	∞					∞					∞					∞					∞					∞
LS94-G2	∞					∞					∞					∞					∞					∞
LS94-G3	∞					∞					∞					∞					∞					∞
LS94-P1	∞					∞					∞					∞					∞					∞
OKW95-dt1_theory	3.06	18	55	154		1.26	14	23	68		1.29	14	23	68		3.13	18	55	154		3.25	18	55	154		3.12	18	55	154
Sim91-sims2	∞					∞					∞					∞					∞					∞
SK90-3.01	4.60	36	17	119		4.60	36	17	119		4.96	36	17	119		4.62	36	17	119		5.10	36	17	119		4.62	36	17	119
SK90-3.02	0.11	4	3	7		0.12	4	3	7		0.12	4	3	7		0.10	4	1	7		0.11	4	1	7		0.11	4	1	7
SK90-3.03	2.15	28	6	56		2.10	28	6	56		2.35	28	6	56		2.13	28	6	56		2.28	28	6	56		2.19	28	6	56
SK90-3.04	4.49	40	5	103		4.50	40	5	103		4.82	40	5	103		4.59	40	5	103		4.82	40	5	103		4.51	40	5	103
SK90-3.05	65.60	149	7	463		65.61	149	7	463		80.90	149	7	463		65.26	149	7	463		81.00	149	7	463		81.99	149	7	463
SK90-3.06	15.99	71	11	306		16.16	71	11	306		19.64	71	11	306		16.05	71	11	306		19.82	71	11	306		16.08	71	11	306
SK90-3.07	72.63	134	22	699		72.32	134	22	699		104.07	134	22	699		72.55	134	22	699		104.98	134	22	699		73.05	134	22	699
SK90-3.08	0.12	9	2	10		0.13	9	2	10		0.14	9	2	10		0.12	9	2	10		0.14	9	2	10		0.13	9	2	10
SK90-3.09	∞					∞					∞					∞					∞					∞
SK90-3.10	0.06	9	0	8		0.06	9	0	8		0.07	9	0	8		0.06	9	0	8		0.07	9	0	8		0.06	9	0	8
SK90-3.11	0.09	7	0	7		0.09	7	0	7		0.08	7	0	7		0.08	7	0	7		0.08	7	0	7		0.08	7	0	7
SK90-3.12	⊥					⊥					⊥					⊥					⊥					⊥
SK90-3.13	0.49	7	15	33		0.49	7	15	33		0.51	7	15	33		0.41	7	11	29		0.42	7	11	29		0.50	7	15	33
SK90-3.14	0.50	10	9	34		0.43	11	9	28		0.47	11	9	28		0.53	10	9	34		0.54	10	9	34		0.51	10	9	34
SK90-3.15	0.26	11	3	16		0.26	11	3	16		0.26	11	3	16		0.26	11	3	16		0.27	11	3	16		0.27	11	3	16
SK90-3.16	0.04	6	0	5		0.04	6	0	5		0.04	6	0	5		0.04	6	0	5		0.04	6	0	5		0.04	6	0	5
SK90-3.17	0.21	6	4	10		0.20	6	4	10		0.21	6	4	10		0.20	6	4	10		0.22	6	4	10		0.20	6	4	10
SK90-3.18	0.86	12	10	35		0.84	12	10	35		0.86	12	10	35		0.84	12	10	35		0.87	12	10	35		0.86	12	10	35
SK90-3.19	2.18	11	35	89		2.15	11	35	89		2.25	11	35	89		2.15	11	35	89		2.22	11	35	89		2.17	11	35	89
SK90-3.20	1.33	13	31	90		1.34	13	31	90		1.36	13	31	90		1.27	13	31	90		1.33	13	31	90		1.35	13	31	90
SK90-3.21	0.65	13	7	43		0.63	13	7	43		0.68	13	7	43		0.64	13	7	43		0.66	13	7	43		0.64	13	7	43
SK90-3.22	∞					∞					∞					∞					∞					∞
SK90-3.23	0.92	19	16	48		0.98	19	16	48		1.12	19	16	48		0.96	19	16	48		1.07	19	16	48		1.10	19	16	48
SK90-3.24	0.09	5	3	8		0.06	4	1	5		0.06	4	1	5		0.09	5	3	8		0.09	5	3	8		0.09	5	3	8
SK90-3.25	0.08	3	1	4		0.08	3	1	4		0.08	3	1	4		0.08	3	1	4		0.08	3	1	4		0.08	3	1	4
SK90-3.26	∞					∞					∞					∞					∞					∞
SK90-3.27	31.07	28	2	121		31.55	28	2	121		37.13	28	2	121		31.64	28	2	121		37.90	28	2	121		38.16	28	2	121
SK90-3.28	139.74	30	186	2298		140.16	30	186	2298		222.11	42	122	2410		139.12	30	186	2298		159.05	30	186	2298		223.80	42	122	2410
SK90-3.29	4.40	12	118	262		3.15	10	94	206		3.89	15	69	170		4.44	12	118	262		5.89	12	118	262		3.91	15	69	170
SK90-3.30	0.05	6	0	4		0.05	6	0	4		0.05	6	0	4		0.05	6	0	4		0.05	6	0	4		0.05	6	0	4
SK90-3.31	0.04	4	1	4		0.04	4	1	4		0.04	4	1	4		0.04	4	1	4		0.04	4	1	4		0.04	4	1	4
SK90-3.32	0.03	5	0	4		0.03	5	0	4		0.03	5	0	4		0.03	5	0	4		0.03	5	0	4		0.03	5	0	4
SK90-3.33	0.04	6	0	5		0.04	6	0	5		0.04	6	0	5		0.04	6	0	5		0.04	6	0	5		0.04	6	0	5
slothrop-ackermann	0.12	4	4	8		0.11	4	4	8		0.11	4	4	8		0.12	4	4	8		0.12	4	4	8		0.12	4	4	8
slothrop-cge	73.59	79	35	840		82.05	85	33	780		33.36	70	14	371		73.19	79	35	840		94.19	79	35	840		33.45	70	14	371
slothrop-cge3	∞					⊥					∞					∞					∞					∞
slothrop-endo	4.59	30	13	116		4.58	30	13	116		5.04	30	13	116		4.61	30	13	116		5.08	30	13	116		4.55	30	13	116
slothrop-equiv_proofs	7.44	37	5	96		7.31	37	5	96		7.55	37	5	96		7.24	37	5	96		7.59	37	5	96		7.34	37	5	96
slothrop-equiv_proofs_or	7.48	37	5	96		7.34	37	5	96		7.57	37	5	96		7.36	37	5	96		7.59	37	5	96		7.32	37	5	96
slothrop-fgh	0.03	6	0	3		0.03	6	0	3		0.03	6	0	3		0.03	6	0	3		0.03	6	0	3		0.03	6	0	3
slothrop-groups	1.19	21	3	35		1.17	21	3	35		1.19	21	3	35		1.15	21	3	35		1.20	21	3	35		1.18	21	3	35
slothrop-groups_conj	0.66	13	3	26		0.67	13	3	26		0.67	13	3	26		0.63	13	3	26		0.69	13	3	26		0.65	13	3	26
slothrop-hard	0.04	3	1	3		0.03	3	1	3		0.04	3	1	3		0.03	3	1	3		0.04	3	1	3		0.03	3	1	3
slothrop-nlp-2b	∞					∞					∞					∞					∞					∞
TPDB-AProVE_07_thiemann27	∞					∞					∞					∞					∞					∞
TPDB-secr10	∞					∞					∞					∞					∞					∞
TPDB-secr4	17.51	52	26	308		17.49	52	26	308		22.03	52	26	308		17.56	52	26	308		21.97	52	26	308		22.47	52	26	308
TPDB-z115	58.40	43	115	690		57.80	43	115	690		90.32	43	115	690		58.15	43	115	690		89.50	43	115	690		91.06	43	115	690
TPTP-BOO027-1_theory	0.14	7	0	7		0.13	7	0	7		0.13	7	0	7		0.14	7	0	7		0.14	7	0	7		0.14	7	0	7
TPTP-COL053-1_theory	0.03	2	1	2		0.03	2	1	2		0.03	2	1	2		0.03	2	1	2		0.03	2	1	2		0.03	2	1	2
TPTP-COL056-1_theory	0.13	4	5	10		0.10	4	5	10		0.11	4	5	10		0.11	4	5	10		0.12	4	5	10		0.11	4	5	10
TPTP-COL060-1_theory	0.07	3	0	4		0.07	3	0	4		0.07	3	0	4		0.06	3	0	4		0.07	3	0	4		0.07	3	0	4
TPTP-COL085-1_theory	0.01	2	0	1		0.01	2	0	1		0.01	2	0	1		0.01	2	0	1		0.01	2	0	1		0.01	2	0	1
TPTP-GRP010-4_theory	14.83	77	28	295		14.80	77	28	295		19.61	77	28	295		15.06	77	28	295		19.65	77	28	295		14.92	77	28	295
TPTP-GRP011-4_theory	4.25	26	13	151		2.33	26	6	77		2.52	26	6	77		4.28	26	13	151		4.36	26	13	151		2.54	26	6	77
TPTP-GRP012-4_theory	0.82	17	3	22		0.82	17	3	22		0.82	17	3	22		0.50	14	1	16		0.50	14	1	16		0.83	17	3	22
TPTP-GRP393-2_theory	0.04	2	1	2		0.04	2	1	2		0.04	2	1	2		0.03	2	0	2		0.03	2	0	2		0.04	2	1	2
TPTP-GRP394-3_theory	1.17	21	3	35		1.20	21	3	35		1.20	21	3	35		1.14	21	3	35		1.22	21	3	35		1.16	21	3	35
TPTP-GRP454-1_theory	9.58	53	15	177		9.61	53	15	177		12.34	53	15	177		9.58	53	15	177		12.06	53	15	177		9.60	53	15	177
TPTP-GRP457-1_theory	9.59	53	15	177		9.71	53	15	177		12.27	53	15	177		9.60	53	15	177		12.12	53	15	177		9.67	53	15	177
TPTP-GRP460-1_theory	23.23	89	22	202		22.54	89	22	202		32.59	89	22	202		22.93	89	22	202		33.07	89	22	202		22.93	89	22	202
TPTP-GRP463-1_theory	23.37	89	22	202		22.64	89	22	202		33.54	89	22	202		23.03	89	22	202		33.30	89	22	202		23.01	89	22	202
TPTP-GRP481-1_theory	139.03	162	24	471		140.85	162	24	471		222.38	162	24	471		138.01	162	24	471		220.27	162	24	471		141.10	162	24	471
TPTP-GRP484-1_theory	471.39	328	0	1004		475.47	328	0	1004		∞					474.82	328	0	1004		∞					475.10	328	0	1004
TPTP-GRP487-1_theory	145.73	209	0	759		143.69	209	0	759		265.79	209	0	759		143.65	209	0	759		266.55	209	0	759		144.21	209	0	759
TPTP-GRP490-1_theory	391.17	340	1	1176		390.67	340	1	1176		∞					392.47	340	1	1176		∞					391.44	340	1	1176
TPTP-GRP493-1_theory	94.92	191	0	362		94.37	191	0	362		118.16	191	0	362		93.79	191	0	362		119.34	191	0	362		93.69	191	0	362
TPTP-GRP496-1_theory	133.52	200	27	647		131.81	200	27	647		215.83	200	27	647		133.45	200	27	647		210.09	200	27	647		134.63	200	27	647
TPTP-HWC004-1_theory	0.20	11	2	16		0.21	11	2	16		0.26	11	2	16		0.20	11	2	16		0.25	11	2	16		0.24	11	2	16
TPTP-HWC004-2_theory	0.10	7	2	12		0.10	7	2	12		0.12	7	2	12		0.12	7	2	12		0.11	7	2	12		0.11	7	2	12
TPTP-SWV262-2_theory	0.09	4	3	7		0.10	4	3	7		0.10	4	3	7		0.10	4	3	7		0.10	4	3	7		0.11	4	3	7
WS06-proofreduction	227.23	91	31	763		228.18	91	31	763		236.18	91	31	763		227.57	91	31	763		236.72	91	31	763		237.90	91	31	763
successes	87					87					85					87					85					87
average time	38.17					38.05					37.64					37.69					37.23					40.1

Explanation:

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