Benchmark results

True properties as (Proved,DontKnow,Disproved): (50, 47, 0) ------- False properties as (Proved,DontKnow,Disproved): (0, 2, 21)

POSITIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal	Unknown	30.0000	18
append_equal_natlist	Unknown	32.1133	14
append_length_commutative	Unknown	30.0250	29
append_length_leq	Unknown	30.0027	29
append_length_leq_natlist	Unknown	30.0000	33
append_not_null	Unknown	30.0308	25
append_not_null2	Unknown	30.0764	26
append_not_null3	Unknown	30.0018	24
append_not_null4	Unknown	30.0012	24
cons_is_equal	Proved	0.0043	0
cons_not_equal	Proved	0.0037	0
cons_not_null	Proved	0.0148	3
insert_length_eq	Unknown	30.0004	19
insert_length_leq	Proved	0.3048	22
isaplanner_prop13	Unknown	42.1543	51
isaplanner_prop17	Proved	0.0621	11
isaplanner_prop18	Proved	0.0543	10
isaplanner_prop19	Unknown	30.0079	91
isaplanner_prop21	Proved	0.0815	11
isaplanner_prop22	Proved	0.0226	5
isaplanner_prop23	Proved	0.0368	5
isaplanner_prop24	Proved	0.1192	9
isaplanner_prop25	Proved	0.1071	9
isaplanner_prop26	Unknown	38.7810	50
isaplanner_prop31	Proved	0.0289	5
isaplanner_prop32	Proved	0.0511	5
isaplanner_prop33	Proved	0.0886	9
isaplanner_prop34	Proved	0.1304	9
isaplanner_prop4	Unknown	30.3122	89
isaplanner_prop40	Proved	1.7521	19
isaplanner_prop42	Proved	1.5268	19
isaplanner_prop44	Unknown	30.0200	33
isaplanner_prop45	Unknown	30.0058	30
isaplanner_prop46	Unknown	30.0034	30
isaplanner_prop49	Unknown	30.0035	23
isaplanner_prop51	Unknown	30.0175	23
isaplanner_prop54	Unknown	30.5690	96
isaplanner_prop65	Proved	0.0849	10
isaplanner_prop69	Proved	0.1201	11
isaplanner_prop70	Proved	0.0527	4
isaplanner_prop79	Unknown	30.8812	71
length_append_cons	Unknown	30.0068	29
length_cons_le	Proved	0.0487	9
length_cons_le_tsil	Proved	0.0927	9
length_cons_s	Proved	0.0631	6
length_count	Proved	0.3145	21
length_delete	Proved	0.3763	23
length_fun_le_cons	Proved	1.4713	34
length_fun_le_cons_ab	Proved	0.2274	17
length_reverse_eq	Unknown	30.0043	39
length_reverse_leq_leq	Unknown	30.0002	47
length_reverse_natlist	Unknown	30.0001	50
leq_leq_eq	Proved	0.0357	6
list_delete_all_count	Unknown	30.0741	47
max_nat	Proved	0.0952	12
mem_reverse	Unknown	30.0006	67
member_append	Unknown	30.4288	46
member_equal_ab	Proved	0.5279	28
member_equal_nat	Unknown	30.0006	47
merge_length_leq	Unknown	30.0087	11
mult_leq	Proved	0.5030	34
mult_leq_succ	Proved	0.5847	34
nat_double_is_even	Proved	0.1005	10
nat_double_is_le	Proved	0.1346	10
nat_double_is_zero	Proved	0.0631	5
nat_double_is_zero_ite	Proved	0.0693	5
plus_commutative	Unknown	30.5549	75
plus_even_even	Proved	0.1987	18
plus_le	Proved	0.3238	21
plus_le_le	Proved	0.2837	22
plus_not_zero_implication	Proved	0.0703	10
plus_odd_odd	Proved	0.2430	21
plus_succ1_le	Proved	0.2007	22
plus_succ2_le	Proved	0.3286	21
plus_succ_not_zero	Proved	0.1062	10
prefix_append	Unknown	30.0001	24
prefix_count	Unknown	30.6025	95
reverse_not_null	Unknown	30.0039	35
sort_append	Unknown	30.4565	39
sort_cons	Unknown	32.9507	28
sort_length_eq	Unknown	30.0350	30
sort_reverse	Unknown	30.0499	41
timbuk_delete	Proved	1.5340	53
timbuk_equalNat	Proved	0.0040	0
timbuk_insertionSort	Proved	0.3579	23
timbuk_memberTree	Unknown	30.0135	16
timbuk_plus_even	Proved	0.1639	20
timbuk_replaceTree	Unknown	30.0250	26
timbuk_reverse	Unknown	30.0052	39
timbuk_reverseImplies	Unknown	30.1886	54
tree_add_not_eq	Proved	0.0042	0
tree_depth_leq	Unknown	30.1778	19
tree_eq_implies_root_eq	Proved	0.0038	0
tree_height_numnodes	Unknown	30.0004	29
tree_height_subtree	Unknown	30.0003	26
tree_numnodes_member	Unknown	30.0010	25
tree_numnodes_subtree	Unknown	30.9015	26

NEGATIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal	Disproved	0.0394	6
append_length_le	Disproved	0.0604	8
cons_is_equal	Disproved	0.0068	1
cons_not_null	Disproved	0.0149	3
insert_length_eq	Disproved	0.0867	11
isaplanner_prop11	Disproved	0.0453	3
list_delete_all_count	Disproved	0.1235	10
max_nat	Disproved	0.1313	10
member_cons	Disproved	0.0679	5
mult_leq	Disproved	0.1491	14
nat_double_is_le	Disproved	0.0625	6
plus_even_implies	Disproved	0.1331	11
plus_le	Disproved	0.0673	5
plus_odd_odd	Disproved	0.0991	9
prefix_append	Unknown	30.0203	24
prefix_count	Disproved	0.0981	11
reverse_not_null	Disproved	0.0794	6
sort_bug_length_eq	Unknown	30.0147	44
successor_is_equal	Disproved	0.0075	1
timbuk_deleteBUG	Disproved	0.0565	7
timbuk_equal	Disproved	0.0181	1
timbuk_reverseBUGimplies	Disproved	0.1758	13
tree_add	Disproved	0.0205	1