mkbTT experiments

	NV					PI					DT					none
	(1)	(2)	(3)	(4)		(1)	(2)	(3)	(4)		(1)	(2)	(3)	(4)		(1)	(2)	(3)	(4)
AD93-Z22	∞					∞					∞					∞
ASK93-1	0.06	0	0	17		0.07	0	0	14		0.06	0	0	17		0.07	0	0	14
ASK93-2	∞					∞					∞					∞
ASK93-5	∞					∞					∞					∞
ASK93-6	37.75	0	0	6		38.08	0	0	7		37.64	0	0	6		39.64	0	0	6
BD94-collapse	0.10	0	0	20		0.11	0	0	18		0.11	0	0	18		0.11	0	0	18
BD94-peano	0.10	0	0	10		0.11	0	0	9		0.10	0	0	10		0.10	0	0	10
BD94-sqrt	0.03	0	0	0		0.03	0	0	0		0.03	0	0	0		0.03	0	0	0
BGK94-D08	127.85	0	3	16		130.26	0	0	17		122.08	0	0	12		121.59	0	0	11
BGK94-D10	144.55	0	7	29		148.39	0	0	31		125.74	0	0	20		123.42	0	0	18
BGK94-D12	124.92	0	8	28		128.42	0	0	31		110.27	0	0	20		107.32	0	0	17
BGK94-D16	150.35	0	9	31		159.90	0	0	35		132.80	0	0	22		128.02	0	0	19
BGK94-M08	∞					∞					∞					∞
BGK94-M10	∞					∞					∞					∞
BGK94-M12	∞					∞					∞					∞
BGK94-M14	∞					∞					∞					∞
BGK94-Z22W	∞					∞					∞					∞
BH96-fac8_theory	0.34	0	0	6		0.35	0	0	6		0.34	0	0	6		0.36	0	0	6
Chr89-A2	42.50	0	4	23		41.93	0	0	22		38.81	0	0	16		38.22	0	0	15
Chr89-A24	∞					∞					∞					∞
Chr89-A3	160.87	0	1	9		160.25	0	0	9		159.43	0	0	9		157.59	0	0	8
HR94-1	∞					∞					∞					∞
HR94-2	∞					∞					∞					∞
KH11-aufgabe3-2	0.02	0	0	0		0.02	0	0	0		0.02	0	0	0		0.02	0	0	0
KH11-aufgabe3-3	0.03	0	0	0		0.03	0	0	0		0.03	0	0	0		0.03	0	0	0
KH11-fggx	0.08	0	0	13		0.09	0	0	11		0.08	0	0	13		0.08	0	0	13
KH11-fib	2.93	0	1	8		2.99	0	0	9		2.93	0	0	7		3.00	0	0	7
KH11-kb-fail	⊥					⊥					⊥					⊥
KH11-kb-fail1	⊥					⊥					⊥					⊥
KH11-lr-theory	5.65	0	5	32		5.74	0	0	33		5.03	0	0	25		5.18	0	1	22
KH11-rl-theory	∞					∞					440.25	0	0	64		429.91	0	0	63
KK99-linear_assoc	0.09	0	0	11		0.10	0	0	10		0.10	0	0	10		0.10	0	0	10
Les83-fib	0.71	0	1	8		0.70	0	0	10		0.69	0	0	7		0.70	0	0	7
Les83-subset	0.37	0	3	14		0.38	0	0	16		0.36	0	0	14		0.37	0	0	14
LS06-CGE4	∞					∞					∞					∞
LS06-CGE5	∞					∞					∞					∞
LS94-G0	1.72	1	3	20		1.77	1	0	23		1.65	1	0	18		1.64	1	1	15
LS94-G1	∞					∞					∞					∞
LS94-G2	∞					∞					∞					∞
LS94-G3	∞					∞					∞					∞
LS94-P1	∞					∞					∞					∞
OKW95-dt1_theory	3.14	0	1	7		3.11	0	0	7		3.06	0	0	6		3.12	0	0	6
Sim91-sims2	∞					∞					∞					∞
SK90-3.01	4.87	0	4	27		7.18	0	0	27		6.85	0	0	22		4.62	0	0	21
SK90-3.02	0.10	0	0	10		0.11	0	0	9		0.10	0	0	10		0.11	0	0	9
SK90-3.03	2.34	0	3	26		2.37	0	0	29		2.23	0	0	23		2.19	0	0	20
SK90-3.04	5.09	0	4	26		5.19	0	0	28		4.63	0	0	21		4.51	0	0	18
SK90-3.05	102.31	0	6	35		26.67	0	0	27		23.90	0	0	20		81.99	0	0	19
SK90-3.06	17.27	0	6	27		17.71	0	0	28		16.28	0	0	23		16.08	0	0	21
SK90-3.07	81.69	0	7	33		81.88	0	0	33		75.06	0	0	26		73.05	0	0	23
SK90-3.08	0.13	0	0	23		0.13	0	0	23		0.12	0	0	25		0.13	0	0	23
SK90-3.09	∞					∞					∞					∞
SK90-3.10	0.07	0	0	14		0.07	0	0	14		0.06	0	0	17		0.06	0	0	17
SK90-3.11	0.08	0	0	13		0.08	0	0	13		0.08	0	0	13		0.08	0	0	13
SK90-3.12	⊥					⊥					⊥					⊥
SK90-3.13	0.48	0	0	8		0.48	0	0	8		0.48	0	0	6		0.50	0	0	6
SK90-3.14	0.52	0	2	12		0.52	0	0	12		0.50	0	0	10		0.51	0	0	10
SK90-3.15	0.29	0	0	14		0.29	0	0	14		0.27	0	0	11		0.27	0	0	11
SK90-3.16	0.04	0	0	25		0.04	0	0	25		0.04	0	0	25		0.04	0	0	0
SK90-3.17	0.21	0	0	10		0.22	0	0	18		0.22	0	0	14		0.20	0	0	10
SK90-3.18	0.86	0	2	15		0.87	0	0	17		0.84	0	0	13		0.86	0	0	12
SK90-3.19	2.14	0	0	6		2.15	0	0	7		2.15	0	0	5		2.17	0	0	5
SK90-3.20	1.31	0	1	7		1.29	0	0	8		1.29	0	0	7		1.35	0	0	5
SK90-3.21	0.64	0	2	16		0.64	0	0	17		0.61	0	0	15		0.64	0	0	14
SK90-3.22	∞					∞					∞					∞
SK90-3.23	1.10	0	2	15		1.13	0	0	17		1.06	0	0	15		1.10	0	1	15
SK90-3.24	0.09	0	0	22		0.09	0	0	22		0.09	0	0	22		0.09	0	0	22
SK90-3.25	0.08	0	0	13		0.09	0	0	11		0.08	0	0	13		0.08	0	0	0
SK90-3.26	∞					∞					∞					∞
SK90-3.27	37.87	0	4	28		45.45	0	0	40		38.07	0	0	27		38.16	0	0	26
SK90-3.28	223.75	0	0	5		224.13	0	0	5		221.31	0	0	5		223.80	0	0	5
SK90-3.29	3.77	0	1	8		3.86	0	0	9		3.83	0	0	8		3.91	0	0	7
SK90-3.30	0.05	0	0	20		0.06	0	0	17		0.05	0	0	20		0.05	0	0	20
SK90-3.31	0.04	0	0	0		0.04	0	0	0		0.04	0	0	0		0.04	0	0	0
SK90-3.32	0.03	0	0	0		0.03	0	0	0		0.03	0	0	0		0.03	0	0	0
SK90-3.33	0.04	0	0	25		0.04	0	0	25		0.04	0	0	25		0.04	0	0	25
slothrop-ackermann	0.11	0	0	9		0.12	0	0	17		0.11	0	0	9		0.12	0	0	8
slothrop-cge	35.02	0	4	20		35.91	0	0	21		33.64	0	0	16		33.45	0	0	15
slothrop-cge3	∞					∞					∞					∞
slothrop-endo	4.83	0	4	24		5.07	0	0	26		4.57	0	0	21		4.55	0	0	18
slothrop-equiv_proofs	7.66	0	3	14		7.91	0	0	16		7.39	0	0	10		7.34	0	0	10
slothrop-equiv_proofs_or	7.77	0	3	14		7.80	0	0	16		7.29	0	0	10		7.32	0	0	10
slothrop-fgh	0.03	0	0	33		0.04	0	0	25		0.03	0	0	33		0.03	0	0	33
slothrop-groups	1.26	0	3	25		1.30	0	0	28		1.19	0	0	22		1.18	1	1	19
slothrop-groups_conj	0.69	0	3	20		0.70	0	0	23		0.65	0	0	20		0.65	0	0	17
slothrop-hard	0.04	0	0	0		0.04	0	0	0		0.03	0	0	0		0.03	0	0	0
slothrop-nlp-2b	∞					∞					∞					∞
TPDB-AProVE_07_thiemann27	∞					∞					∞					∞
TPDB-secr10	∞					∞					∞					∞
TPDB-secr4	22.33	0	2	16		22.73	0	0	16		21.99	0	0	14		22.47	0	0	14
TPDB-z115	92.26	0	1	13		92.60	0	0	13		89.63	0	0	12		91.06	0	0	12
TPTP-BOO027-1_theory	0.14	0	0	7		0.12	0	0	8		0.12	0	0	8		0.14	0	0	7
TPTP-COL053-1_theory	0.03	0	0	0		0.04	0	0	0		0.03	0	0	0		0.03	0	0	0
TPTP-COL056-1_theory	0.12	0	0	8		0.11	0	0	9		0.11	0	0	9		0.11	0	0	9
TPTP-COL060-1_theory	0.07	0	0	0		0.08	0	0	0		0.07	0	0	0		0.07	0	0	0
TPTP-COL085-1_theory	0.01	0	0	0		0.01	0	0	0		0.01	0	0	0		0.01	0	0	0
TPTP-GRP010-4_theory	16.39	0	4	26		16.48	0	0	27		15.34	0	0	21		14.92	0	1	19
TPTP-GRP011-4_theory	2.62	0	3	20		2.63	0	0	22		2.50	0	0	17		2.54	0	0	15
TPTP-GRP012-4_theory	0.91	0	4	32		0.95	0	0	36		0.86	0	0	29		0.83	0	0	24
TPTP-GRP393-2_theory	0.05	0	0	20		0.04	0	0	25		0.04	0	0	0		0.04	0	0	0
TPTP-GRP394-3_theory	1.27	1	3	24		1.30	0	0	28		1.19	0	0	23		1.16	0	1	20
TPTP-GRP454-1_theory	10.21	0	5	27		12.70	0	0	28		11.99	0	0	24		9.60	1	1	22
TPTP-GRP457-1_theory	10.24	0	5	27		12.38	0	0	28		12.00	0	0	24		9.67	1	1	22
TPTP-GRP460-1_theory	25.74	0	6	37		26.24	0	0	37		23.46	0	0	32		22.93	1	1	29
TPTP-GRP463-1_theory	25.78	0	6	37		26.17	0	0	37		23.99	0	0	32		23.01	1	1	29
TPTP-GRP481-1_theory	163.31	0	8	47		141.57	0	0	49		129.40	0	0	41		141.10	0	1	38
TPTP-GRP484-1_theory	∞					388.61	0	0	33		348.25	0	0	24		475.10	0	0	22
TPTP-GRP487-1_theory	160.35	0	6	35		147.33	0	0	36		133.08	0	0	30		144.21	0	1	28
TPTP-GRP490-1_theory	428.30	0	6	37		435.14	0	0	36		398.44	0	0	30		391.44	0	0	29
TPTP-GRP493-1_theory	119.98	0	9	45		130.32	0	0	48		98.68	0	0	31		93.69	0	0	28
TPTP-GRP496-1_theory	145.23	0	7	38		148.33	0	0	39		136.26	0	0	33		134.63	0	1	31
TPTP-HWC004-1_theory	0.25	0	4	24		0.24	0	0	25		0.24	0	0	25		0.24	0	0	25
TPTP-HWC004-2_theory	0.11	0	0	18		0.11	0	0	18		0.12	0	0	17		0.11	0	0	18
TPTP-SWV262-2_theory	0.10	0	0	10		0.10	0	0	10		0.10	0	0	0		0.11	0	0	0
WS06-proofreduction	241.30	0	1	3		238.63	0	0	3		236.96	0	0	2		237.90	0	0	2
successes	85					86					87					87
average time	33.13					36.62					38.18					40.1
time/variants	6.78					7.6					8.17					8.79
time/encompassments	135.89					6.67					7.2					10.5
time/maintenance	1.16					1.79					1.26					0.83
time/rewriting	734.57					865.35					876.76					854.61

Explanation:

(1)	total time
(2)	time for variant retrieval
(3)	time for encompassment retrieval
(4)	time for rewriting