Benchmark results

True properties as (Proved,DontKnow,Disproved): (106, 35, 0) ------- False properties as (Proved,DontKnow,Disproved): (0, 1, 31)

POSITIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal_elt	Proved	5.1674	13
append_equal_nat	Unknown	40.2811	21
append_length_commutative	Unknown	39.4764	28
append_length_leq_elt	Proved	0.2591	13
append_length_leq_nat	Proved	0.2514	13
append_not_null_cons_elt	Proved	0.0352	4
append_not_null_cons_nat	Proved	0.0343	4
append_not_null_elt	Proved	0.0344	4
append_not_null_nat	Proved	0.0351	4
cons_injectivity_1	Proved	0.0063	1
cons_injectivity_2	Proved	0.0062	1
cons_not_null	Proved	0.0133	2
delete_one_insert	Unknown	40.6489	36
drop_length_minus	Unknown	40.4912	22
fst_elist	Proved	4.4251	15
fst_elt	Proved	0.0324	4
fst_nat	Proved	0.0626	6
fst_nlist	Proved	15.2958	18
insert_length_eq	Proved	0.2951	12
insert_length_leq	Proved	0.2853	15
insert_not_nil	Proved	0.0345	4
isaplanner_prop10	Proved	0.0627	7
isaplanner_prop11	Proved	0.1607	8
isaplanner_prop13	Unknown	41.0478	14
isaplanner_prop15	Proved	0.1756	11
isaplanner_prop16	Proved	0.1060	6
isaplanner_prop17	Proved	0.0404	5
isaplanner_prop18	Proved	0.1162	10
isaplanner_prop19	Unknown	40.4116	22
isaplanner_prop20	Proved	0.6895	15
isaplanner_prop21	Proved	0.0667	8
isaplanner_prop22	Proved	0.0922	8
isaplanner_prop23	Proved	0.0835	8
isaplanner_prop24	Proved	0.0918	8
isaplanner_prop25	Proved	0.1159	9
isaplanner_prop26	Proved	16.2387	21
isaplanner_prop27	Unknown	40.0314	15
isaplanner_prop28	Unknown	39.7339	15
isaplanner_prop31	Proved	0.0294	4
isaplanner_prop32	Proved	0.0286	4
isaplanner_prop33	Proved	0.0393	5
isaplanner_prop34	Proved	0.0393	5
isaplanner_prop4	Unknown	40.4782	18
isaplanner_prop40	Proved	0.0233	3
isaplanner_prop42	Proved	0.0526	5
isaplanner_prop44	Unknown	39.6701	26
isaplanner_prop45	Proved	3.3728	16
isaplanner_prop49	Unknown	40.6686	27
isaplanner_prop51	Unknown	40.4399	29
isaplanner_prop54	Unknown	40.8743	25
isaplanner_prop59	Unknown	40.2444	22
isaplanner_prop65	Proved	0.1157	10
isaplanner_prop68	Proved	0.2602	14
isaplanner_prop69	Proved	0.0584	7
isaplanner_prop70	Proved	0.0365	5
isaplanner_prop79	Unknown	40.9009	28
isaplanner_prop80	Unknown	40.7302	26
length_append_le_z	Proved	0.0612	6
length_append_to_plus	Unknown	40.9706	22
length_cons_le	Proved	0.0475	6
length_cons_le_fun_elt	Proved	0.1262	10
length_cons_le_fun_nat	Proved	0.1401	10
length_cons_le_tsil	Proved	0.0456	6
length_cons_s	Proved	0.0283	4
length_count	Proved	0.2129	13
length_delete_leq	Proved	0.1810	12
length_delete_minus_count	Unknown	40.1668	28
length_reverse_eq	Proved	21.0211	27
length_reverse_eq_nat	Proved	31.7784	30
length_reverse_leq_elt	Proved	21.7251	30
length_reverse_leq_nat	Proved	37.7360	31
length_take_if	Proved	0.0606	6
leq_leq_eq	Proved	0.0524	7
list_delete_all_count	Unknown	40.6527	23
max_nat	Proved	0.0564	7
mem_implies_positive_count	Proved	1.2886	15
mem_reverse	Unknown	40.2567	20
member_equal_ab	Proved	0.1489	8
member_equal_nat	Unknown	40.4854	19
merge_length_leq	Proved	0.3476	13
min_of_plus_and_max	Unknown	40.9517	25
mult_leq_not_null	Proved	0.0737	8
mult_leq_succ	Proved	0.0753	8
nat_double_is_even	Proved	0.0405	5
nat_double_is_le	Proved	0.0439	6
nat_double_is_zero	Proved	0.0194	3
nat_double_is_zero_ite	Proved	0.0203	3
not_null_transitive	Proved	0.0126	2
plus_commutative	Unknown	40.9219	30
plus_even_even	Proved	0.2161	12
plus_le	Proved	0.1463	12
plus_le_le	Proved	0.1504	12
plus_not_zero_implication	Proved	0.0297	4
plus_odd_odd_even	Proved	0.0927	9
plus_succ_le_1	Proved	0.0606	7
plus_succ_le_2	Proved	0.1441	12
plus_succ_not_zero	Proved	0.0286	4
prefix_append	Proved	0.2218	10
prefix_count	Unknown	40.3669	20
prefix_nil	Proved	0.0444	5
reverse_not_null	Proved	0.0340	4
sort_append	Unknown	40.0586	26
sort_cons	Unknown	40.9875	28
sort_length_eq	Proved	0.6680	16
sort_reverse	Unknown	40.0002	20
swap_swap_eq_elt	Proved	0.0345	4
swap_swap_eq_nat	Proved	0.0571	6
timbuk_delete_not_member	Unknown	40.8738	30
timbuk_equalNat	Proved	0.0066	1
timbuk_insertionSort_elt	Proved	0.0362	4
timbuk_plus_even	Proved	0.2215	12
timbuk_replaceTree	Unknown	40.5290	13
timbuk_reverse	Unknown	40.0111	21
timbuk_reverseImplies	Unknown	40.0002	26
tree_add_not_eq	Proved	0.0068	1
tree_depth_le_node	Unknown	44.5009	26
tree_depth_leq_size	Proved	1.6891	20
tree_flip_heightRB_heightLB	Proved	0.1570	12
tree_flip_preserves_member	Proved	2.4560	12
tree_flip_preserves_size	Unknown	40.9905	25
tree_flip_preserves_subtree	Proved	2.3790	16
tree_flip_twice	Proved	0.1567	9
tree_heightMIDDLE	Proved	2.0475	19
tree_heightRB_node_le	Proved	0.0500	6
tree_heightRB_subtree	Proved	0.1019	7
tree_height_heightRB	Proved	0.1864	14
tree_height_node_leq	Proved	0.0370	5
tree_height_numnodes_le	Unknown	40.4712	22
tree_higher_leq	Proved	0.3652	12
tree_injectivity_1	Proved	0.0065	1
tree_member_leq_size	Proved	0.6160	10
tree_nat_depth_leq_size	Proved	1.4685	20
tree_nat_flip_twice	Proved	0.2675	10
tree_shallow_leq	Proved	0.1791	11
tree_shallow_max	Proved	0.4541	10
tree_shallow_taller_node	Proved	0.4913	12
tree_shallow_taller_subtree	Proved	3.6771	8
tree_shallower_rec_leq	Proved	0.0402	5
tree_shallower_rec_node_le	Proved	0.0495	6
tree_size_le_node	Unknown	40.8680	23
tree_strict_subtree_trans	Proved	0.3201	10

NEGATIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal	Disproved	0.0382	3
append_length_le	Disproved	0.1625	3
cons_is_equal	Disproved	0.0125	1
cons_not_null	Disproved	0.0299	3
insert_length_eq	Disproved	0.0468	4
isaplanner_prop11	Disproved	0.0370	2
length_take	Disproved	0.0224	2
list_delete_all_count	Disproved	0.0230	2
max_nat	Disproved	0.0681	5
member_cons	Disproved	0.0491	3
mult_leq	Disproved	0.0567	4
nat_double_is_le	Disproved	0.0360	3
plus_even_implies	Disproved	0.0517	5
plus_le	Disproved	0.0421	3
plus_odd_odd	Disproved	0.0392	4
prefix_append	Unknown	40.1902	20
prefix_count	Disproved	0.0743	5
reverse_not_null	Disproved	0.0880	3
sort_bug_length_eq	Disproved	6.1954	23
successor_is_equal	Disproved	0.0123	1
timbuk_deleteBUG	Disproved	0.0582	3
timbuk_equal	Disproved	0.0123	1
timbuk_reverseBUGimplies	Disproved	0.4935	6
tree_depth_le_error	Disproved	0.1040	3
tree_depth_max_error	Disproved	0.0396	4
tree_depth_subtree_error	Disproved	0.0359	3
tree_heightMIDDLE_error	Disproved	0.3203	11
tree_height_numnodes_error	Disproved	0.0594	5
tree_shallow_leq_error	Disproved	0.0452	4
tree_shallow_subtree_error	Disproved	0.6939	4
tree_subtree_height_error	Disproved	0.1902	6
tree_taller_max	Disproved	0.2495	7