Benchmark results

True properties as (Proved,DontKnow,Disproved): (65, 32, 0) ------- False properties as (Proved,DontKnow,Disproved): (0, 0, 23)

POSITIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal	Unknown	60.0000	44
append_equal_natlist	Unknown	60.0001	23
append_length_commutative	Unknown	65.7668	69
append_length_leq	Proved	0.3859	18
append_length_leq_natlist	Unknown	60.0001	21
append_not_null	Unknown	60.0000	17
append_not_null2	Unknown	60.0000	17
append_not_null3	Proved	0.3088	15
append_not_null4	Proved	0.1536	15
cons_is_equal	Proved	0.0100	0
cons_not_equal	Proved	0.0043	0
cons_not_null	Proved	0.0423	3
insert_length_eq	Proved	0.1944	14
insert_length_leq	Proved	0.2128	18
isaplanner_prop13	Unknown	65.2782	77
isaplanner_prop17	Proved	0.1041	10
isaplanner_prop18	Proved	0.1124	9
isaplanner_prop19	Unknown	64.4325	97
isaplanner_prop21	Proved	0.1368	10
isaplanner_prop22	Proved	0.0256	4
isaplanner_prop23	Proved	0.0246	4
isaplanner_prop24	Proved	0.0590	8
isaplanner_prop25	Proved	0.1074	8
isaplanner_prop26	Proved	24.6951	59
isaplanner_prop31	Proved	0.0394	4
isaplanner_prop32	Proved	0.0475	4
isaplanner_prop33	Proved	0.1022	8
isaplanner_prop34	Proved	0.1118	8
isaplanner_prop4	Unknown	60.0003	38
isaplanner_prop40	Proved	0.0971	7
isaplanner_prop42	Proved	0.0936	7
isaplanner_prop44	Unknown	60.0001	84
isaplanner_prop45	Proved	0.8418	27
isaplanner_prop46	Proved	0.8759	27
isaplanner_prop49	Unknown	63.9677	96
isaplanner_prop51	Unknown	68.1205	65
isaplanner_prop54	Unknown	67.3096	95
isaplanner_prop65	Proved	0.1370	9
isaplanner_prop69	Proved	0.0599	10
isaplanner_prop70	Proved	0.0544	4
isaplanner_prop79	Unknown	63.1842	84
length_append_cons	Proved	0.2775	17
length_cons_le	Proved	0.0338	6
length_cons_le_tsil	Unknown	63.6386	100
length_cons_s	Proved	0.0226	3
length_count	Proved	0.1114	16
length_delete	Proved	0.1740	18
length_fun_le_cons	Unknown	60.0000	12
length_fun_le_cons_ab	Proved	0.1788	13
length_reverse_eq	Proved	6.8019	52
length_reverse_leq_leq	Proved	8.6256	59
length_reverse_natlist	Unknown	60.5706	37
leq_leq_eq	Proved	0.0767	6
list_delete_all_count	Unknown	63.8749	99
max_nat	Proved	0.1439	11
mem_reverse	Unknown	65.6042	104
member_append	Proved	25.1814	59
member_equal_ab	Proved	0.6482	27
member_equal_nat	Unknown	60.0004	37
merge_length_leq	Proved	1.5967	43
mult_leq	Proved	0.8648	33
mult_leq_succ	Proved	0.6593	34
nat_double_is_even	Proved	0.0732	10
nat_double_is_le	Proved	0.1318	10
nat_double_is_zero	Proved	0.0657	5
nat_double_is_zero_ite	Proved	0.0673	5
plus_commutative	Unknown	62.7491	78
plus_even_even	Proved	0.1469	18
plus_le	Proved	0.3381	20
plus_le_le	Proved	0.3477	19
plus_not_zero_implication	Proved	0.0808	9
plus_odd_odd	Proved	0.3730	21
plus_succ1_le	Proved	0.4762	23
plus_succ2_le	Proved	0.2831	19
plus_succ_not_zero	Proved	0.0648	9
prefix_append	Proved	20.9104	28
prefix_count	Unknown	65.1667	116
reverse_not_null	Proved	0.3331	25
sort_append	Unknown	60.0004	86
sort_cons	Unknown	60.0004	82
sort_length_eq	Proved	0.2565	19
sort_reverse	Unknown	60.0004	61
timbuk_delete	Proved	2.1582	49
timbuk_equalNat	Proved	0.0050	0
timbuk_insertionSort	Proved	0.2850	19
timbuk_memberTree	Unknown	60.0009	16
timbuk_plus_even	Proved	0.3915	21
timbuk_replaceTree	Unknown	60.0014	19
timbuk_reverse	Proved	0.3487	29
timbuk_reverseImplies	Proved	0.9940	39
tree_add_not_eq	Proved	0.0087	0
tree_depth_leq	Unknown	60.0002	42
tree_eq_implies_root_eq	Proved	0.0049	0
tree_height_numnodes	Unknown	60.0024	52
tree_height_subtree	Unknown	60.0001	34
tree_numnodes_member	Unknown	60.0009	35
tree_numnodes_subtree	Unknown	60.0003	53

NEGATIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal	Disproved	0.0819	6
append_length_le	Disproved	0.0979	8
cons_is_equal	Disproved	0.0201	1
cons_not_null	Disproved	0.0419	3
insert_length_eq	Disproved	0.1327	11
isaplanner_prop11	Disproved	0.0425	3
list_delete_all_count	Disproved	0.1295	10
max_nat	Disproved	0.1364	10
member_cons	Disproved	0.0534	5
mult_leq	Disproved	0.1948	15
nat_double_is_le	Disproved	0.0781	6
plus_even_implies	Disproved	0.1469	11
plus_le	Disproved	0.0634	5
plus_odd_odd	Disproved	0.0690	10
prefix_append	Disproved	0.3786	19
prefix_count	Disproved	0.2437	17
reverse_not_null	Disproved	0.0766	6
sort_bug_length_eq	Disproved	2.4621	54
successor_is_equal	Disproved	0.0194	1
timbuk_deleteBUG	Disproved	0.0906	7
timbuk_equal	Disproved	0.0201	1
timbuk_reverseBUGimplies	Disproved	0.1787	13
tree_add	Disproved	0.0203	1