KBCV - Knuth Bendix Completion Visualizer

Statistics

	kbcv_1.6	CeTA_2.4	kbcv_1.7	CeTA_2.4
#yes	86	80	86	86
total time	540.2	283.2	604.5	13.4
average time	6.3	3.5	7.0	0.2
#no	0	0	0	0
total time	0.0	0.0	0.0	0.0
average time	-	-	-	-
#maybe	5	0	6	0
total time	26.3	0.0	230.4	0.0
average time	5.3	-	38.4	-
#timeout	24	4	23	0
total time	7200.0	1200.0	6900.0	0.0
average time	300.0	300.0	300.0	-
#error	0	2	0	0
total time	0.0	0.0	0.0	0.0
average time	-	0.0	-	-
#total	115	86	115	86
total time	7766.5	1483.3	7734.9	13.4

Results

	kbcv_1.6	CeTA_2.4	kbcv_1.7	CeTA_2.4
AD93_Z22.trs	300.0		300.0
ASK93_1.trs	1.6	0.0	1.5	0.0
ASK93_2.trs	300.0		300.0
ASK93_5.trs	300.0		300.0
ASK93_6.trs	3.2	0.1	2.7	0.1
BD94_collapse.trs	1.6	0.1	1.4	0.1
BD94_peano.trs	1.3	0.0	2.2	0.1
BD94_sqrt.trs	1.3	0.0	1.4	0.0
BGK94_D08.trs	28.1	5.4	31.9	0.2
BGK94_D10.trs	13.0	3.7	13.6	0.4
BGK94_D12.trs	14.2	3.3	18.6	0.5
BGK94_D16.trs	27.2	8.5	46.3	0.7
BGK94_M08.trs	3.5	0.5	3.5	0.2
BGK94_M10.trs	5.4	2.0	5.1	0.2
BGK94_M12.trs	7.8	1.1	7.3	0.3
BGK94_M14.trs	13.8	3.0	15.1	0.2
BGK94_Z22W.trs	300.0		300.0
BH96_fac8_theory.trs	1.8	0.0	1.5	0.0
Chr89_A2.trs	4.3	0.1	4.0	0.1
Chr89_A24.trs	300.0		300.0
Chr89_A3.trs	5.8	0.1	5.8	0.1
HR94_1.trs	300.0		300.0
HR94_2.trs	300.0		300.0
KK99_linear_assoc.trs	1.6	0.0	1.4	0.0
LS06_CGE4.trs	300.0		300.0
	kbcv_1.6	CeTA_2.4	kbcv_1.7	CeTA_2.4
LS06_CGE5.trs	300.0		300.0
LS94_G0.trs	3.5	0.1	3.8	0.1
LS94_G1.trs	300.0		300.0
LS94_G2.trs	300.0		300.0
LS94_G3.trs	300.0		300.0
LS94_P1.trs	102.5	300.0	129.2	0.8
Les83_fib.trs	2.5	0.1	2.8	0.1
Les83_subset.trs	2.7	0.1	2.1	0.1
OKW95_dt1_theory.trs	2.2	0.1	2.3	0.1
SK90_3.01.trs	3.5	0.5	3.2	0.1
SK90_3.02.trs	1.5	0.1	1.9	0.0
SK90_3.03.trs	9.3	2.8	10.2	0.1
SK90_3.04.trs	22.5	0.7	21.6	0.2
SK90_3.05.trs	7.7	7.4	6.4	0.1
SK90_3.06.trs	9.4	39.1	8.1	0.3
SK90_3.07.trs	8.9	83.8	7.6	0.3
SK90_3.08.trs	1.8	0.1	1.6	0.0
SK90_3.09.trs	300.0		300.0
SK90_3.10.trs	1.9	0.1	1.7	0.1
SK90_3.11.trs	1.5	0.0	1.4	0.0
SK90_3.12.trs	3.8		3.2
SK90_3.13.trs	2.2	0.1	1.9	0.0
SK90_3.14.trs	2.4	0.1	2.2	0.1
SK90_3.15.trs	300.0		300.0
SK90_3.16.trs	1.4	0.0	1.6	0.0
	kbcv_1.6	CeTA_2.4	kbcv_1.7	CeTA_2.4
SK90_3.17.trs	2.0	0.1	1.5	0.1
SK90_3.18.trs	2.2	0.0	2.1	0.0
SK90_3.19.trs	2.6	0.1	2.0	0.1
SK90_3.20.trs	2.5	0.1	2.9	0.1
SK90_3.21.trs	2.2	0.1	1.9	0.1
SK90_3.22.trs	3.9	2.3	3.2	0.2
SK90_3.23.trs	300.0		300.0
SK90_3.24.trs	1.3	0.0	1.6	0.0
SK90_3.25.trs	1.8	0.0	1.2	0.0
SK90_3.26.trs	18.9	13.5	18.8	0.3
SK90_3.27.trs	3.7	6.8	3.1	0.3
SK90_3.28.trs	300.0		300.0
SK90_3.29.trs	2.7	0.1	2.4	0.1
SK90_3.30.trs	1.4	0.0	1.1	0.1
SK90_3.31.trs	1.6	0.0	1.1	0.0
SK90_3.32.trs	1.6	0.0	1.8	0.0
SK90_3.33.trs	1.2	0.0	1.3	0.0
Sim91_sims2.trs	300.0		300.0
TPDB_secret2006_torpa_secr10.trs	4.9	0.5	6.6	0.3
TPDB_secret2006_torpa_secr4.trs	3.5	0.2	3.4	0.1
TPDB_thiemann27.trs	300.0		300.0
TPDB_zantema_z115.trs	9.9	8.2	13.3	0.4
TPTP_BOO027-1_theory.trs	1.6	0.0	1.9	0.1
TPTP_COL053-1_theory.trs	1.5	0.0	1.2	0.0
TPTP_COL056-1_theory.trs	1.3	0.0	1.6	0.0
	kbcv_1.6	CeTA_2.4	kbcv_1.7	CeTA_2.4
TPTP_COL060-1_theory.trs	2.8	0.1	3.4	0.0
TPTP_COL085-1_theory.trs	1.5	0.0	1.4	0.0
TPTP_GRP010-4_theory.trs	11.8	3.2	11.2	0.2
TPTP_GRP011-4_theory.trs	5.0	0.7	4.0	0.1
TPTP_GRP012-4_theory.trs	4.1	0.2	3.6	0.1
TPTP_GRP393-2_theory.trs	1.7	0.0	1.6	0.0
TPTP_GRP394-3_theory.trs	3.0	0.2	3.4	0.2
TPTP_GRP454-1_theory.trs	8.3	15.6	7.4	0.3
TPTP_GRP457-1_theory.trs	7.3	17.5	6.9	0.4
TPTP_GRP460-1_theory.trs	5.2	6.5	6.5	0.2
TPTP_GRP463-1_theory.trs	5.9	5.3	6.6	0.3
TPTP_GRP481-1_theory.trs	6.3	300.0	8.3	0.4
TPTP_GRP484-1_theory.trs	7.2	300.0	9.5	0.4
TPTP_GRP487-1_theory.trs	16.6	0.0	21.4	0.3
TPTP_GRP490-1_theory.trs	12.9	300.0	14.0	0.5
TPTP_GRP493-1_theory.trs	7.7	36.4	6.4	0.4
TPTP_GRP496-1_theory.trs	6.5	0.0	7.7	0.3
TPTP_HWC004-1_theory.trs	2.0	0.1	2.1	0.1
TPTP_HWC004-2_theory.trs	2.2	0.0	1.8	0.0
TPTP_SWV262-2_theory.trs	300.0		300.0
WS06_proofreduction.trs	300.0		300.0
aufgabe3_2.trs	1.6	0.0	1.6	0.0
aufgabe3_3.trs	1.4	0.0	1.3	0.0
fggx.trs	1.3	0.0	1.8	0.0
fib.trs	2.6	0.1	2.8	0.1
	kbcv_1.6	CeTA_2.4	kbcv_1.7	CeTA_2.4
kb_fail.trs	1.8		1.2
kb_fail1.trs	2.8		2.4
lr_theory.trs	3.3	0.2	5.1	0.1
rl_theory.trs	5.9	0.2	6.7	0.2
slothrop_ackermann.trs	1.3	0.1	1.5	0.0
slothrop_cge.trs	300.0		206.5
slothrop_cge3.trs	300.0		300.0
slothrop_endo.trs	300.0		300.0
slothrop_equiv_proofs.trs	9.1		8.4
slothrop_equiv_proofs_or.trs	8.7		8.6
slothrop_fgh.trs	1.5	0.0	1.2	0.0
slothrop_groups.trs	3.6	0.9	3.7	0.1
slothrop_groups_conj.trs	2.6	0.1	2.6	0.1
slothrop_hard.trs	1.8	0.0	2.2	0.0
slothrop_nlp-2b.trs	300.0		300.0