Benchmark results

True properties as (Proved,DontKnow,Disproved): (63, 78, 0) ------- False properties as (Proved,DontKnow,Disproved): (0, 7, 25)

POSITIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal_elt	Unknown	21.3639	18
append_equal_nat	Unknown	20.2576	15
append_length_commutative	Unknown	20.0096	37
append_length_leq_elt	Unknown	20.0031	29
append_length_leq_nat	Unknown	20.1682	32
append_not_null_cons_elt	Unknown	20.0033	23
append_not_null_cons_nat	Unknown	20.0001	25
append_not_null_elt	Unknown	20.0087	23
append_not_null_nat	Unknown	20.0001	22
cons_injectivity_1	Proved	0.0038	0
cons_injectivity_2	Proved	0.0030	0
cons_not_null	Proved	0.0142	3
delete_one_insert	Unknown	20.0081	30
drop_length_minus	Unknown	20.6538	74
fst_elist	Unknown	20.0005	45
fst_elt	Proved	0.0220	5
fst_nat	Proved	0.1333	14
fst_nlist	Unknown	20.7109	34
insert_length_eq	Unknown	20.0061	20
insert_length_leq	Proved	0.2604	22
insert_not_nil	Proved	0.2392	16
isaplanner_prop10	Proved	0.2851	21
isaplanner_prop11	Proved	17.2825	36
isaplanner_prop13	Unknown	20.0577	46
isaplanner_prop15	Proved	0.2794	25
isaplanner_prop16	Unknown	21.0107	19
isaplanner_prop17	Proved	0.0600	11
isaplanner_prop18	Proved	0.0941	10
isaplanner_prop19	Unknown	20.5892	88
isaplanner_prop20	Unknown	20.0008	54
isaplanner_prop21	Proved	0.0688	11
isaplanner_prop22	Proved	0.0587	5
isaplanner_prop23	Proved	0.0634	5
isaplanner_prop24	Proved	0.1174	9
isaplanner_prop25	Proved	0.1150	9
isaplanner_prop26	Unknown	30.5603	46
isaplanner_prop27	Unknown	20.0087	52
isaplanner_prop28	Unknown	20.0320	44
isaplanner_prop31	Proved	0.0238	5
isaplanner_prop32	Proved	0.0402	5
isaplanner_prop33	Proved	0.0960	9
isaplanner_prop34	Proved	0.1022	9
isaplanner_prop4	Unknown	20.0004	80
isaplanner_prop40	Proved	1.5712	19
isaplanner_prop42	Proved	1.4492	19
isaplanner_prop44	Unknown	20.0178	33
isaplanner_prop45	Unknown	20.1768	28
isaplanner_prop49	Unknown	20.0035	23
isaplanner_prop51	Unknown	20.0073	23
isaplanner_prop54	Unknown	20.1625	92
isaplanner_prop59	Unknown	20.5044	30
isaplanner_prop65	Proved	0.0569	10
isaplanner_prop68	Unknown	20.0001	38
isaplanner_prop69	Proved	0.0675	11
isaplanner_prop70	Proved	0.0339	4
isaplanner_prop79	Unknown	20.3353	67
isaplanner_prop80	Unknown	25.9940	61
length_append_le_z	Unknown	20.0016	28
length_append_to_plus	Unknown	20.0001	55
length_cons_le	Proved	0.0548	9
length_cons_le_fun_elt	Proved	0.2414	17
length_cons_le_fun_nat	Proved	1.4736	34
length_cons_le_tsil	Proved	0.0603	9
length_cons_s	Proved	0.0886	6
length_count	Proved	0.2900	21
length_delete_leq	Proved	0.3913	23
length_delete_minus_count	Unknown	20.0562	74
length_reverse_eq	Unknown	20.0003	38
length_reverse_eq_nat	Unknown	20.0372	40
length_reverse_leq_elt	Unknown	20.0016	43
length_reverse_leq_nat	Unknown	20.2297	50
length_take_if	Proved	1.4752	29
leq_leq_eq	Proved	0.0324	6
list_delete_all_count	Unknown	20.0013	62
max_nat	Proved	0.0784	12
mem_implies_positive_count	Proved	2.5078	68
mem_reverse	Unknown	35.2894	55
member_equal_ab	Proved	0.4731	28
member_equal_nat	Unknown	20.0006	43
merge_length_leq	Unknown	20.0077	11
min_of_plus_and_max	Unknown	20.0290	107
mult_leq_not_null	Proved	0.4366	34
mult_leq_succ	Proved	0.3826	34
nat_double_is_even	Proved	0.0988	10
nat_double_is_le	Proved	0.1137	10
nat_double_is_zero	Proved	0.0569	5
nat_double_is_zero_ite	Proved	0.0564	5
not_null_transitive	Proved	0.0402	3
plus_commutative	Unknown	20.1176	67
plus_even_even	Proved	0.1306	18
plus_le	Proved	0.2857	21
plus_le_le	Proved	0.2950	22
plus_not_zero_implication	Proved	0.1184	10
plus_odd_odd_even	Proved	0.2258	21
plus_succ_le_1	Proved	0.5064	22
plus_succ_le_2	Proved	0.2444	21
plus_succ_not_zero	Proved	0.0771	10
prefix_append	Unknown	45.1703	30
prefix_count	Unknown	20.0004	79
prefix_nil	Proved	0.1201	10
reverse_not_null	Unknown	20.0037	35
sort_append	Unknown	21.2864	39
sort_cons	Unknown	20.0559	28
sort_length_eq	Unknown	20.0068	28
sort_reverse	Unknown	20.0124	37
swap_swap_eq_elt	Proved	0.0218	4
swap_swap_eq_nat	Proved	0.1510	10
timbuk_delete_not_member	Proved	2.3752	60
timbuk_equalNat	Proved	0.0038	0
timbuk_insertionSort_elt	Proved	0.3239	23
timbuk_plus_even	Proved	0.2157	20
timbuk_replaceTree	Unknown	20.0383	12
timbuk_reverse	Unknown	20.0065	39
timbuk_reverseImplies	Unknown	20.1973	53
tree_add_not_eq	Proved	0.0037	0
tree_depth_le_node	Unknown	20.1788	26
tree_depth_leq_size	Unknown	20.0005	30
tree_flip_heightRB_heightLB	Unknown	20.0397	20
tree_flip_preserves_member	Unknown	20.0269	17
tree_flip_preserves_size	Unknown	20.0294	20
tree_flip_preserves_subtree	Unknown	20.0122	4
tree_flip_twice	Unknown	20.0493	5
tree_heightMIDDLE	Unknown	20.0139	21
tree_heightRB_node_le	Proved	0.5119	21
tree_heightRB_subtree	Unknown	20.0077	6
tree_height_heightRB	Unknown	20.0002	25
tree_height_node_leq	Unknown	20.0031	12
tree_height_numnodes_le	Unknown	20.0003	45
tree_higher_leq	Unknown	25.2493	27
tree_injectivity_1	Proved	0.0049	0
tree_member_leq_size	Unknown	20.0009	25
tree_nat_depth_leq_size	Unknown	20.0207	29
tree_nat_flip_twice	Unknown	20.0000	6
tree_shallow_leq	Unknown	20.0013	13
tree_shallow_max	Unknown	20.0087	17
tree_shallow_taller_node	Unknown	24.6793	14
tree_shallow_taller_subtree	Unknown	20.0082	17
tree_shallower_rec_leq	Unknown	20.0003	8
tree_shallower_rec_node_le	Unknown	20.0003	10
tree_size_le_node	Unknown	22.3506	23
tree_strict_subtree_trans	Unknown	20.0129	3

NEGATIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal	Disproved	0.0442	6
append_length_le	Disproved	0.0670	8
cons_is_equal	Disproved	0.0195	1
cons_not_null	Disproved	0.0382	3
insert_length_eq	Disproved	0.1445	11
isaplanner_prop11	Disproved	0.0382	3
length_take	Disproved	0.0754	6
list_delete_all_count	Disproved	0.1253	10
max_nat	Disproved	0.1239	10
member_cons	Disproved	0.0597	5
mult_leq	Disproved	0.1747	14
nat_double_is_le	Disproved	0.0521	6
plus_even_implies	Disproved	0.1388	11
plus_le	Disproved	0.0638	5
plus_odd_odd	Disproved	0.1087	9
prefix_append	Unknown	20.0103	24
prefix_count	Disproved	0.0748	11
reverse_not_null	Disproved	0.0599	6
sort_bug_length_eq	Unknown	20.0009	54
successor_is_equal	Disproved	0.0068	1
timbuk_deleteBUG	Disproved	0.0329	7
timbuk_equal	Disproved	0.0168	1
timbuk_reverseBUGimplies	Disproved	0.1663	13
tree_depth_le_error	Disproved	0.1285	14
tree_depth_max_error	Disproved	0.1085	9
tree_depth_subtree_error	Disproved	0.1191	11
tree_heightMIDDLE_error	Unknown	20.0458	22
tree_height_numnodes_error	Disproved	0.1332	18
tree_shallow_leq_error	Unknown	20.0012	15
tree_shallow_subtree_error	Unknown	20.0081	13
tree_subtree_height_error	Unknown	20.0100	11
tree_taller_max	Unknown	20.0080	19