Benchmark results

True properties as (Proved,DontKnow,Disproved): (53, 44, 0) ------- False properties as (Proved,DontKnow,Disproved): (0, 1, 22)

POSITIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal	Unknown	60.0000	38
append_equal_natlist	Unknown	60.1826	49
append_length_commutative	Unknown	73.9468	72
append_length_leq	Unknown	67.9127	82
append_length_leq_natlist	Unknown	60.0007	55
append_not_null	Unknown	60.0000	17
append_not_null2	Unknown	60.0001	17
append_not_null3	Proved	0.2250	15
append_not_null4	Proved	0.2607	16
cons_is_equal	Proved	0.0132	0
cons_not_equal	Proved	0.0239	0
cons_not_null	Proved	0.0386	3
insert_length_eq	Unknown	64.9922	79
insert_length_leq	Unknown	63.0906	100
isaplanner_prop13	Unknown	912.4781	68
isaplanner_prop17	Proved	0.1056	10
isaplanner_prop18	Proved	0.1501	9
isaplanner_prop19	Unknown	66.8800	105
isaplanner_prop21	Proved	0.1099	10
isaplanner_prop22	Proved	0.0478	4
isaplanner_prop23	Proved	0.0648	4
isaplanner_prop24	Proved	0.1576	8
isaplanner_prop25	Proved	0.1454	8
isaplanner_prop26	Proved	34.9565	58
isaplanner_prop31	Proved	0.0466	4
isaplanner_prop32	Proved	0.0796	4
isaplanner_prop33	Proved	0.1709	8
isaplanner_prop34	Proved	0.1025	8
isaplanner_prop4	Unknown	60.0802	92
isaplanner_prop40	Proved	0.1522	12
isaplanner_prop42	Unknown	64.7006	72
isaplanner_prop44	Unknown	60.0001	88
isaplanner_prop45	Proved	0.5846	26
isaplanner_prop46	Proved	0.5846	27
isaplanner_prop49	Unknown	60.0038	75
isaplanner_prop51	Unknown	64.7664	62
isaplanner_prop54	Unknown	65.6476	102
isaplanner_prop65	Proved	0.1854	9
isaplanner_prop69	Proved	1.1346	10
isaplanner_prop70	Proved	0.0387	4
isaplanner_prop79	Unknown	66.6225	78
length_append_cons	Proved	0.3146	21
length_cons_le	Unknown	2104.5856	75
length_cons_le_tsil	Proved	0.0671	6
length_cons_s	Unknown	63.5354	79
length_count	Unknown	64.7765	100
length_delete	Unknown	64.2024	84
length_fun_le_cons	Unknown	60.0002	38
length_fun_le_cons_ab	Unknown	64.1370	93
length_reverse_eq	Unknown	66.8199	78
length_reverse_leq_leq	Unknown	65.1551	100
length_reverse_natlist	Unknown	60.0043	61
leq_leq_eq	Proved	0.0645	6
list_delete_all_count	Unknown	63.6747	99
max_nat	Proved	0.1554	11
mem_reverse	Unknown	64.6289	102
member_append	Proved	30.3498	52
member_equal_ab	Proved	0.6408	27
member_equal_nat	Unknown	60.0012	62
merge_length_leq	Unknown	66.6069	80
mult_leq	Proved	0.6546	33
mult_leq_succ	Proved	0.6539	34
nat_double_is_even	Proved	0.1467	10
nat_double_is_le	Proved	0.1270	10
nat_double_is_zero	Proved	0.0739	5
nat_double_is_zero_ite	Proved	0.1980	5
plus_commutative	Unknown	64.4143	67
plus_even_even	Proved	0.2225	18
plus_le	Proved	0.2937	20
plus_le_le	Proved	0.2548	19
plus_not_zero_implication	Proved	0.0902	9
plus_odd_odd	Proved	0.3601	21
plus_succ1_le	Proved	0.3740	23
plus_succ2_le	Proved	0.2920	19
plus_succ_not_zero	Proved	0.1139	9
prefix_append	Proved	29.3880	31
prefix_count	Unknown	62.5285	98
reverse_not_null	Proved	0.4651	25
sort_append	Unknown	60.0005	81
sort_cons	Unknown	60.0006	86
sort_length_eq	Unknown	66.5879	92
sort_reverse	Unknown	63.8269	97
timbuk_delete	Proved	2.0996	50
timbuk_equalNat	Proved	0.0073	0
timbuk_insertionSort	Proved	0.2134	19
timbuk_memberTree	Unknown	60.0013	16
timbuk_plus_even	Proved	0.3530	21
timbuk_replaceTree	Unknown	60.0024	20
timbuk_reverse	Proved	0.5873	29
timbuk_reverseImplies	Proved	0.7694	39
tree_add_not_eq	Proved	0.0084	0
tree_depth_leq	Unknown	60.0001	39
tree_eq_implies_root_eq	Proved	0.0123	0
tree_height_numnodes	Unknown	63.0455	89
tree_height_subtree	Unknown	65.9132	66
tree_numnodes_member	Unknown	60.0013	24
tree_numnodes_subtree	Unknown	60.0006	68

NEGATIVE INSTANCES

Instance name	Answer	Time (in sec)	ICE iterations
append_equal	Disproved	0.1293	6
append_length_le	Disproved	0.1649	8
cons_is_equal	Disproved	0.0342	1
cons_not_null	Disproved	0.0605	3
insert_length_eq	Disproved	0.2369	11
isaplanner_prop11	Disproved	0.0620	3
list_delete_all_count	Disproved	0.2093	10
max_nat	Disproved	0.2166	10
member_cons	Disproved	0.1149	5
mult_leq	Disproved	0.3545	15
nat_double_is_le	Disproved	0.1229	6
plus_even_implies	Disproved	0.2513	11
plus_le	Disproved	0.1085	5
plus_odd_odd	Disproved	0.2185	10
prefix_append	Disproved	0.6312	19
prefix_count	Disproved	0.2306	11
reverse_not_null	Disproved	0.1294	6
sort_bug_length_eq	Unknown	66.1706	77
successor_is_equal	Disproved	0.0325	1
timbuk_deleteBUG	Disproved	0.1475	7
timbuk_equal	Disproved	0.0330	1
timbuk_reverseBUGimplies	Disproved	0.2950	13
tree_add	Disproved	0.0321	1