Benchmark results

True properties as (Proved,DontKnow,Disproved): (64, 77, 0) ------- False properties as (Proved,DontKnow,Disproved): (0, 1, 31)

POSITIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal_elt	Unknown	40.0000	40
append_equal_nat	Unknown	40.0001	17
append_length_commutative	Unknown	40.0815	73
append_length_leq_elt	Unknown	40.9833	85
append_length_leq_nat	Unknown	40.0002	64
append_not_null_cons_elt	Proved	0.1508	16
append_not_null_cons_nat	Unknown	40.0006	18
append_not_null_elt	Proved	0.1247	16
append_not_null_nat	Unknown	40.0000	19
cons_injectivity_1	Proved	0.0039	0
cons_injectivity_2	Proved	0.0033	0
cons_not_null	Proved	0.0138	3
delete_one_insert	Unknown	40.0005	80
drop_length_minus	Unknown	40.4533	108
fst_elist	Unknown	40.8427	107
fst_elt	Proved	0.0263	5
fst_nat	Proved	0.0403	8
fst_nlist	Unknown	40.0920	108
insert_length_eq	Unknown	40.3832	82
insert_length_leq	Unknown	40.4805	95
insert_not_nil	Proved	0.0820	15
isaplanner_prop10	Proved	0.2058	21
isaplanner_prop11	Proved	0.9071	25
isaplanner_prop13	Unknown	40.5608	80
isaplanner_prop15	Unknown	40.8668	99
isaplanner_prop16	Proved	0.1542	20
isaplanner_prop17	Proved	0.0500	11
isaplanner_prop18	Proved	0.0458	10
isaplanner_prop19	Unknown	40.1762	116
isaplanner_prop20	Unknown	40.0002	24
isaplanner_prop21	Proved	0.0517	10
isaplanner_prop22	Proved	0.0257	5
isaplanner_prop23	Proved	0.0251	5
isaplanner_prop24	Proved	0.0422	9
isaplanner_prop25	Proved	0.0419	9
isaplanner_prop26	Proved	21.9086	54
isaplanner_prop27	Unknown	40.3123	84
isaplanner_prop28	Unknown	40.0009	87
isaplanner_prop31	Proved	0.0255	5
isaplanner_prop32	Proved	0.0231	5
isaplanner_prop33	Proved	0.0533	9
isaplanner_prop34	Proved	0.0414	9
isaplanner_prop4	Unknown	40.0014	88
isaplanner_prop40	Proved	0.0707	13
isaplanner_prop42	Unknown	40.4363	73
isaplanner_prop44	Proved	35.9619	83
isaplanner_prop45	Proved	0.3237	27
isaplanner_prop49	Unknown	40.1165	83
isaplanner_prop51	Unknown	40.2924	64
isaplanner_prop54	Unknown	40.0688	104
isaplanner_prop59	Unknown	40.2692	88
isaplanner_prop65	Proved	0.0445	10
isaplanner_prop68	Unknown	40.0005	35
isaplanner_prop69	Proved	0.0480	11
isaplanner_prop70	Proved	0.0176	4
isaplanner_prop79	Unknown	40.3428	70
isaplanner_prop80	Unknown	40.0002	62
length_append_le_z	Proved	0.1864	22
length_append_to_plus	Unknown	40.0002	75
length_cons_le	Unknown	40.4062	103
length_cons_le_fun_elt	Unknown	40.8876	89
length_cons_le_fun_nat	Unknown	40.0002	35
length_cons_le_tsil	Proved	0.0262	6
length_cons_s	Unknown	40.7230	84
length_count	Unknown	40.8030	97
length_delete_leq	Unknown	40.6509	83
length_delete_minus_count	Unknown	40.2061	118
length_reverse_eq	Unknown	40.8916	76
length_reverse_eq_nat	Unknown	40.0003	49
length_reverse_leq_elt	Unknown	40.4785	105
length_reverse_leq_nat	Unknown	40.0006	48
length_take_if	Unknown	40.5286	105
leq_leq_eq	Proved	0.0489	6
list_delete_all_count	Unknown	40.8551	117
max_nat	Proved	0.0551	12
mem_implies_positive_count	Proved	1.4513	64
mem_reverse	Unknown	40.5546	98
member_equal_ab	Proved	0.4048	28
member_equal_nat	Unknown	40.0009	78
merge_length_leq	Unknown	40.1971	92
min_of_plus_and_max	Unknown	40.4382	124
mult_leq_not_null	Proved	0.3682	34
mult_leq_succ	Proved	0.3116	34
nat_double_is_even	Proved	0.0472	10
nat_double_is_le	Proved	0.0447	10
nat_double_is_zero	Proved	0.0215	5
nat_double_is_zero_ite	Proved	0.0221	5
not_null_transitive	Proved	0.0136	3
plus_commutative	Unknown	40.5570	69
plus_even_even	Proved	0.1074	18
plus_le	Proved	0.1374	21
plus_le_le	Proved	0.1379	22
plus_not_zero_implication	Proved	0.1012	10
plus_odd_odd_even	Proved	0.1341	21
plus_succ_le_1	Proved	0.1536	22
plus_succ_le_2	Proved	0.1201	21
plus_succ_not_zero	Proved	0.0498	10
prefix_append	Proved	21.3547	34
prefix_count	Unknown	40.0644	95
prefix_nil	Proved	0.0322	6
reverse_not_null	Proved	0.2025	25
sort_append	Unknown	40.0003	63
sort_cons	Unknown	40.0001	28
sort_length_eq	Unknown	40.1462	67
sort_reverse	Unknown	40.5130	94
swap_swap_eq_elt	Proved	0.0354	7
swap_swap_eq_nat	Unknown	40.1243	86
timbuk_delete_not_member	Proved	0.9262	51
timbuk_equalNat	Proved	0.0038	0
timbuk_insertionSort_elt	Proved	0.1938	19
timbuk_plus_even	Proved	0.2117	20
timbuk_replaceTree	Unknown	40.3450	62
timbuk_reverse	Proved	0.3568	30
timbuk_reverseImplies	Proved	0.4007	40
tree_add_not_eq	Proved	0.0064	0
tree_depth_le_node	Unknown	40.0004	37
tree_depth_leq_size	Unknown	40.5961	99
tree_flip_heightRB_heightLB	Unknown	40.7942	43
tree_flip_preserves_member	Unknown	40.0009	16
tree_flip_preserves_size	Unknown	41.0321	62
tree_flip_preserves_subtree	Unknown	40.0032	17
tree_flip_twice	Unknown	40.0352	13
tree_heightMIDDLE	Unknown	40.0884	39
tree_heightRB_node_le	Unknown	40.0001	29
tree_heightRB_subtree	Unknown	40.0032	28
tree_height_heightRB	Unknown	40.0003	57
tree_height_node_leq	Proved	0.0872	12
tree_height_numnodes_le	Unknown	40.3358	75
tree_higher_leq	Unknown	40.0662	43
tree_injectivity_1	Proved	0.0387	0
tree_member_leq_size	Unknown	40.0021	103
tree_nat_depth_leq_size	Unknown	40.0455	88
tree_nat_flip_twice	Unknown	40.0004	11
tree_shallow_leq	Unknown	40.9722	54
tree_shallow_max	Unknown	40.0332	54
tree_shallow_taller_node	Unknown	40.0017	28
tree_shallow_taller_subtree	Unknown	40.0029	79
tree_shallower_rec_leq	Unknown	40.0041	21
tree_shallower_rec_node_le	Unknown	40.0040	27
tree_size_le_node	Unknown	40.0003	68
tree_strict_subtree_trans	Proved	1.3524	5

NEGATIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal	Disproved	0.0171	4
append_length_le	Disproved	0.0310	8
cons_is_equal	Disproved	0.0057	1
cons_not_null	Disproved	0.0114	3
insert_length_eq	Disproved	0.0843	11
isaplanner_prop11	Disproved	0.0362	3
length_take	Disproved	0.0720	6
list_delete_all_count	Disproved	0.1162	10
max_nat	Disproved	0.1241	10
member_cons	Disproved	0.0588	5
mult_leq	Disproved	0.1542	14
nat_double_is_le	Disproved	0.0707	6
plus_even_implies	Disproved	0.1164	11
plus_le	Disproved	0.0604	5
plus_odd_odd	Disproved	0.1049	9
prefix_append	Disproved	0.2530	19
prefix_count	Disproved	0.1020	11
reverse_not_null	Disproved	0.0663	6
sort_bug_length_eq	Disproved	28.6298	85
successor_is_equal	Disproved	0.0079	1
timbuk_deleteBUG	Disproved	0.0298	7
timbuk_equal	Disproved	0.0057	1
timbuk_reverseBUGimplies	Disproved	0.0574	13
tree_depth_le_error	Disproved	0.0527	14
tree_depth_max_error	Disproved	0.0375	9
tree_depth_subtree_error	Disproved	0.0430	11
tree_heightMIDDLE_error	Disproved	2.7714	30
tree_height_numnodes_error	Disproved	0.1405	18
tree_shallow_leq_error	Disproved	6.6324	26
tree_shallow_subtree_error	Disproved	0.3844	23
tree_subtree_height_error	Unknown	40.0025	22
tree_taller_max	Disproved	0.2706	29