Benchmark results

True properties as (Proved,DontKnow,Disproved): (79, 62, 0) ------- False properties as (Proved,DontKnow,Disproved): (0, 2, 30)

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.3073	60
append_length_leq_elt	Proved	0.3137	19
append_length_leq_nat	Unknown	40.0001	23
append_not_null_cons_elt	Proved	0.1705	16
append_not_null_cons_nat	Unknown	40.0002	19
append_not_null_elt	Proved	0.1574	16
append_not_null_nat	Unknown	40.0002	19
cons_injectivity_1	Proved	0.0037	0
cons_injectivity_2	Proved	0.0032	0
cons_not_null	Proved	0.0151	3
delete_one_insert	Unknown	40.0001	79
drop_length_minus	Unknown	40.6967	85
fst_elist	Unknown	40.9496	108
fst_elt	Proved	0.0259	5
fst_nat	Unknown	40.9907	119
fst_nlist	Unknown	40.4705	111
insert_length_eq	Proved	0.0967	14
insert_length_leq	Proved	0.1833	18
insert_not_nil	Proved	0.1691	15
isaplanner_prop10	Proved	0.2275	21
isaplanner_prop11	Proved	11.1504	24
isaplanner_prop13	Unknown	40.2993	71
isaplanner_prop15	Proved	0.2147	21
isaplanner_prop16	Unknown	40.7645	66
isaplanner_prop17	Proved	0.0932	11
isaplanner_prop18	Proved	0.0898	10
isaplanner_prop19	Unknown	40.3784	90
isaplanner_prop20	Unknown	40.0001	21
isaplanner_prop21	Proved	0.0580	11
isaplanner_prop22	Proved	0.0314	5
isaplanner_prop23	Proved	0.0265	5
isaplanner_prop24	Proved	0.0440	9
isaplanner_prop25	Proved	0.0467	9
isaplanner_prop26	Proved	20.4869	54
isaplanner_prop27	Unknown	40.0016	55
isaplanner_prop28	Unknown	40.0009	70
isaplanner_prop31	Proved	0.0235	5
isaplanner_prop32	Proved	0.0251	5
isaplanner_prop33	Proved	0.0560	8
isaplanner_prop34	Proved	0.0876	9
isaplanner_prop4	Unknown	40.0004	62
isaplanner_prop40	Proved	0.0436	8
isaplanner_prop42	Proved	0.0486	8
isaplanner_prop44	Proved	35.1990	82
isaplanner_prop45	Proved	0.3641	27
isaplanner_prop49	Unknown	40.3472	81
isaplanner_prop51	Unknown	40.8894	65
isaplanner_prop54	Unknown	40.9412	99
isaplanner_prop59	Unknown	40.4865	75
isaplanner_prop65	Proved	0.0892	10
isaplanner_prop68	Unknown	40.0001	22
isaplanner_prop69	Proved	0.0658	11
isaplanner_prop70	Proved	0.0309	4
isaplanner_prop79	Unknown	40.0792	79
isaplanner_prop80	Unknown	40.0819	58
length_append_le_z	Proved	0.2545	18
length_append_to_plus	Unknown	40.4619	78
length_cons_le	Proved	0.0413	6
length_cons_le_fun_elt	Proved	0.1342	13
length_cons_le_fun_nat	Unknown	40.0001	14
length_cons_le_tsil	Unknown	40.8765	88
length_cons_s	Proved	0.0143	3
length_count	Proved	0.1629	16
length_delete_leq	Proved	0.1894	18
length_delete_minus_count	Unknown	40.4772	106
length_reverse_eq	Proved	2.5825	46
length_reverse_eq_nat	Unknown	40.0002	21
length_reverse_leq_elt	Proved	9.6963	62
length_reverse_leq_nat	Unknown	40.0001	39
length_take_if	Proved	0.1007	15
leq_leq_eq	Proved	0.0642	6
list_delete_all_count	Unknown	40.2792	102
max_nat	Proved	0.1125	12
mem_implies_positive_count	Proved	2.6359	72
mem_reverse	Unknown	40.3287	94
member_equal_ab	Proved	0.3399	27
member_equal_nat	Unknown	40.3797	71
merge_length_leq	Proved	1.0969	46
min_of_plus_and_max	Unknown	40.8604	118
mult_leq_not_null	Proved	0.3289	34
mult_leq_succ	Proved	0.4021	34
nat_double_is_even	Proved	0.0801	10
nat_double_is_le	Proved	0.0754	10
nat_double_is_zero	Proved	0.0251	5
nat_double_is_zero_ite	Proved	0.0197	5
not_null_transitive	Proved	0.0129	3
plus_commutative	Unknown	40.8709	68
plus_even_even	Proved	0.1588	18
plus_le	Proved	0.2776	21
plus_le_le	Proved	0.3055	22
plus_not_zero_implication	Proved	0.1129	10
plus_odd_odd_even	Proved	0.2560	21
plus_succ_le_1	Proved	0.2811	22
plus_succ_le_2	Proved	0.2595	21
plus_succ_not_zero	Proved	0.1171	10
prefix_append	Proved	19.5001	34
prefix_count	Unknown	40.0003	72
prefix_nil	Proved	0.0333	6
reverse_not_null	Proved	0.3482	25
sort_append	Unknown	40.0004	51
sort_cons	Unknown	40.0002	50
sort_length_eq	Proved	0.1253	19
sort_reverse	Unknown	40.3028	100
swap_swap_eq_elt	Proved	0.0503	7
swap_swap_eq_nat	Unknown	40.6167	97
timbuk_delete_not_member	Proved	1.0374	50
timbuk_equalNat	Proved	0.0036	0
timbuk_insertionSort_elt	Proved	0.1935	19
timbuk_plus_even	Proved	0.2617	20
timbuk_replaceTree	Unknown	40.0014	21
timbuk_reverse	Proved	0.3376	30
timbuk_reverseImplies	Proved	0.5491	40
tree_add_not_eq	Proved	0.0036	0
tree_depth_le_node	Unknown	40.0004	28
tree_depth_leq_size	Unknown	40.0033	66
tree_flip_heightRB_heightLB	Unknown	40.1914	42
tree_flip_preserves_member	Unknown	40.0010	16
tree_flip_preserves_size	Unknown	40.0003	44
tree_flip_preserves_subtree	Unknown	40.0012	14
tree_flip_twice	Unknown	40.0008	13
tree_heightMIDDLE	Unknown	40.3210	32
tree_heightRB_node_le	Proved	0.0708	11
tree_heightRB_subtree	Proved	0.9007	14
tree_height_heightRB	Proved	0.1780	21
tree_height_node_leq	Proved	0.1514	13
tree_height_numnodes_le	Unknown	40.0002	79
tree_higher_leq	Unknown	40.0024	53
tree_injectivity_1	Proved	0.0041	0
tree_member_leq_size	Unknown	40.0011	25
tree_nat_depth_leq_size	Unknown	40.0027	48
tree_nat_flip_twice	Unknown	40.0031	13
tree_shallow_leq	Unknown	40.0021	41
tree_shallow_max	Unknown	40.0022	54
tree_shallow_taller_node	Unknown	40.0013	20
tree_shallow_taller_subtree	Unknown	40.0117	53
tree_shallower_rec_leq	Unknown	40.0009	26
tree_shallower_rec_node_le	Unknown	40.0006	15
tree_size_le_node	Unknown	40.0175	42
tree_strict_subtree_trans	Proved	1.3890	5

NEGATIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal	Disproved	0.0171	4
append_length_le	Disproved	0.0647	8
cons_is_equal	Disproved	0.0194	1
cons_not_null	Disproved	0.0311	3
insert_length_eq	Disproved	0.1289	11
isaplanner_prop11	Disproved	0.0245	3
length_take	Disproved	0.0238	6
list_delete_all_count	Disproved	0.0392	10
max_nat	Disproved	0.0390	10
member_cons	Disproved	0.0204	5
mult_leq	Disproved	0.0638	14
nat_double_is_le	Disproved	0.0709	6
plus_even_implies	Disproved	0.1292	11
plus_le	Disproved	0.0524	5
plus_odd_odd	Disproved	0.1076	9
prefix_append	Disproved	0.2689	19
prefix_count	Disproved	0.2166	17
reverse_not_null	Disproved	0.0664	6
sort_bug_length_eq	Disproved	0.6628	41
successor_is_equal	Disproved	0.0088	1
timbuk_deleteBUG	Disproved	0.0487	7
timbuk_equal	Disproved	0.0197	1
timbuk_reverseBUGimplies	Disproved	0.1601	13
tree_depth_le_error	Disproved	0.1371	14
tree_depth_max_error	Disproved	0.1065	9
tree_depth_subtree_error	Disproved	0.1202	11
tree_heightMIDDLE_error	Disproved	1.6260	31
tree_height_numnodes_error	Disproved	0.2093	18
tree_shallow_leq_error	Unknown	40.0021	38
tree_shallow_subtree_error	Disproved	1.0498	30
tree_subtree_height_error	Unknown	40.0017	29
tree_taller_max	Disproved	0.2607	23