Details

sample97.0ms

Algorithm

intervals

Results

31.0ms	98×	body	1280	valid
17.0ms	85×	body	640	valid
15.0ms	259×	body	80	valid
5.0ms	37×	body	320	valid
2.0ms	19×	body	160	valid

simplify20.6s

Counts

1 → 1

Iterations

Useful iterations: 0 (1.0ms)

Iter	Nodes	Cost
0	6	7
1	15	7
2	29	7
3	64	7
4	134	7
5	242	7
6	443	7
7	969	7
8	2045	7
9	2895	7
10	4076	7
11	4567	7
12	4615	7
13	4626	7
done	5001	7

prune3.0ms

Pruning

2 alts after pruning (2 fresh and 0 done)

	Kept	Total
New	1	1
Fresh	1	1
Picked	0	0
Done	0	0
Total	2	2

Merged error: 0.0b

Counts

2 → 1

localize7.0ms

Local error

Found 3 expressions with local error:

0.0b	(sinh y)
0.0b	(* (sin x) (/ (sinh y) y))
0.0b	(/ (sinh y) y)

rewrite18.0ms

Algorithm

rewrite-expression-head

Rules

24×	`add-sqr-sqrt`
19×	`add-cube-cbrt` `*-un-lft-identity` `times-frac`
13×	`associate-r`
10×	`add-exp-log` `add-cbrt-cube`
5×	`pow1`
3×	`associate-l` `associate-/r` `associate-/l` `add-log-exp`
2×	`cbrt-undiv` `sinh-def` `div-exp` `prod-exp` `cbrt-unprod` `div-inv` `unswap-sqr`
1×	`frac-2neg` `associate-r/` `pow-prod-down` `clear-num` `-commutative` `associate-/l/`

Counts

3 → 68

Calls

3 calls:

2.0ms	(sinh y)
8.0ms	(* (sin x) (/ (sinh y) y))
5.0ms	(/ (sinh y) y)

series48.0ms

Counts

3 → 9

Calls

3 calls:

9.0ms	(sinh y)
24.0ms	(* (sin x) (/ (sinh y) y))
15.0ms	(/ (sinh y) y)

simplify4.1min

Counts

77 → 77

Iterations

Useful iterations: 1 (1.0ms)

Iter	Nodes	Cost
0	5	6
1	13	6
2	24	6
3	42	6
4	63	6
5	81	6
6	86	6
7	96	6
8	113	6
9	135	6
10	142	6
done	142	6
0	4	5
1	13	5
2	27	5
3	55	5
4	94	5
5	132	5
6	158	5
7	178	5
8	195	5
9	217	5
10	224	5
done	224	5
0	4	5
1	10	5
2	19	5
3	38	5
4	63	5
5	93	5
6	119	5
7	135	5
8	143	5
9	163	5
10	180	5
11	196	5
12	218	5
13	254	5
14	312	5
15	377	5
16	487	5
17	597	5
18	661	5
19	689	5
20	699	5
21	701	5
22	703	5
23	705	5
done	705	5
0	7	14
1	22	14
2	73	8
3	260	6
4	1058	6
5	4914	6
done	5000	6
0	5	11
1	11	11
2	20	11
3	39	11
4	59	11
5	82	11
6	101	11
7	108	11
done	108	11
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	5	14
1	18	14
2	49	6
3	162	6
4	751	6
5	3522	6
done	5000	6
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	3	3
1	9	3
2	18	3
3	31	3
4	45	3
5	54	3
6	57	3
done	57	3
0	2	2
done	2	2
0	7	13
1	19	13
2	35	13
3	51	13
4	58	13
5	63	13
done	63	13
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	6	10
1	14	10
2	23	10
3	34	10
4	41	10
5	46	10
done	46	10
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	6	9
1	16	7
2	28	7
3	41	7
4	48	7
5	53	7
done	53	7
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	6	9
1	14	9
2	21	9
3	31	9
4	38	9
5	43	9
done	43	9
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	5
1	13	3
2	21	3
3	29	3
4	36	3
5	41	3
done	41	3
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	5	7
1	9	7
done	9	7
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	4	4
1	6	4
done	6	4
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	2	3
1	4	1
done	4	1
0	3	4
1	9	4
2	18	4
3	37	4
4	57	4
5	80	4
6	100	4
7	107	4
done	107	4
0	3	3
1	5	3
done	5	3
0	3	4
1	9	4
2	18	4
3	31	4
4	39	4
5	46	4
6	51	4
7	56	4
8	62	4
9	66	4
done	66	4
0	5	8
1	13	8
2	24	8
3	54	8
4	94	8
5	144	8
6	198	8
7	225	8
done	225	8
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	4	4
1	12	2
2	22	2
3	33	2
4	44	2
5	58	2
6	75	2
7	83	2
8	87	2
9	95	2
10	103	2
11	111	2
12	123	2
13	158	2
14	199	2
15	234	2
16	261	2
17	272	2
18	277	2
19	283	2
done	283	2
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	3	4
1	9	4
2	18	4
3	31	4
4	39	4
5	46	4
6	51	4
7	56	4
8	62	4
9	66	4
done	66	4
0	3	3
1	4	3
done	4	3
0	6	7
1	15	7
2	29	7
3	64	7
4	134	7
5	242	7
6	443	7
7	969	7
8	2045	7
9	2895	7
10	4076	7
11	4567	7
12	4615	7
13	4626	7
done	5001	7
0	9	10
1	20	10
2	37	10
3	72	10
4	138	10
5	256	10
6	297	10
7	386	10
8	537	10
9	559	10
10	560	10
done	560	10
0	8	9
1	18	9
2	36	9
3	76	9
4	154	9
5	290	9
6	366	9
7	450	9
8	584	9
9	685	9
10	695	9
done	695	9
0	7	8
1	19	8
2	39	8
3	91	8
4	209	8
5	433	8
6	783	8
7	1415	8
8	2766	8
9	4316	8
done	5000	8
0	7	8
1	18	8
2	37	8
3	83	8
4	203	8
5	494	8
6	1163	8
7	4150	8
done	5000	8
0	12	23
1	33	23
2	130	13
3	634	11
4	3662	11
done	5000	11
0	10	23
1	29	23
2	93	11
3	345	11
4	1985	9
done	5000	9
0	8	17
1	17	17
2	31	17
3	66	17
4	136	17
5	243	17
6	444	17
7	964	17
8	2018	17
9	2880	17
10	4070	17
11	4551	17
12	4603	17
13	4614	17
done	5001	17
0	7	8
1	16	8
2	30	8
3	65	8
4	135	8
5	243	8
6	441	8
7	959	8
8	2039	8
9	2891	8
10	4120	8
11	4600	8
12	4632	8
13	4643	8
done	5000	8
0	8	23
1	27	23
2	92	9
3	366	9
4	1828	9
done	5000	9
0	7	8
1	16	8
2	30	8
3	65	8
4	135	8
5	243	8
6	441	8
7	959	8
8	2039	8
9	2891	8
10	4120	8
11	4600	8
12	4632	8
13	4643	8
done	5000	8
0	7	8
1	16	8
2	30	8
3	65	8
4	135	8
5	243	8
6	441	8
7	959	8
8	2039	8
9	2891	8
10	4120	8
11	4600	8
12	4632	8
13	4643	8
done	5000	8
0	8	9
1	15	9
2	24	9
3	43	9
4	63	9
5	86	9
6	107	9
7	116	9
done	116	9
0	8	9
1	15	9
2	24	9
3	43	9
4	63	9
5	86	9
6	107	9
7	116	9
done	116	9
0	9	10
1	18	10
2	28	10
3	42	10
4	50	10
5	55	10
done	55	10
0	9	10
1	18	10
2	28	10
3	42	10
4	50	10
5	55	10
done	55	10
0	8	14
1	17	14
2	28	14
3	47	14
4	67	14
5	90	14
6	110	14
7	120	14
done	120	14
0	7	8
1	14	8
2	23	8
3	42	8
4	62	8
5	85	8
6	106	8
7	113	8
done	113	8
0	10	16
1	25	16
2	61	16
3	110	16
4	173	16
5	194	16
done	194	16
0	9	13
1	20	13
2	37	13
3	62	13
4	82	13
5	89	13
done	89	13
0	9	12
1	22	10
2	45	10
3	90	10
4	131	10
5	136	10
done	136	10
0	9	12
1	20	12
2	38	12
3	62	12
4	81	12
5	86	12
done	86	12
0	8	9
1	17	9
2	27	9
3	41	9
4	49	9
5	54	9
done	54	9
0	8	8
1	19	6
2	32	6
3	49	6
4	62	6
5	67	6
done	67	6
0	8	10
1	15	10
2	25	8
3	55	8
4	76	8
5	78	8
done	78	8
0	7	7
1	12	7
2	15	5
3	30	5
4	31	5
done	31	5
0	5	6
1	10	4
2	15	2
3	19	2
done	19	2
0	4	4
1	7	2
2	10	2
done	10	2
0	5	5
1	12	5
2	23	5
3	43	5
4	70	5
5	107	5
6	171	5
7	355	5
8	515	5
9	712	5
10	1085	5
11	1245	5
12	1301	5
done	1301	5
0	7	8
1	16	8
2	30	8
3	65	8
4	135	8
5	243	8
6	441	8
7	959	8
8	2021	8
9	2836	8
10	4007	8
11	4473	8
12	4511	8
13	4522	8
done	5001	8
0	7	8
1	16	8
2	30	8
3	65	8
4	135	8
5	243	8
6	441	8
7	959	8
8	2021	8
9	2836	8
10	4007	8
11	4473	8
12	4511	8
13	4522	8
done	5001	8
0	6	7
1	15	7
2	29	7
3	64	7
4	134	7
5	242	7
6	443	7
7	969	7
8	2045	7
9	2895	7
10	4076	7
11	4567	7
12	4615	7
13	4626	7
done	5001	7
0	5	5
1	12	5
2	23	5
3	43	5
4	70	5
5	107	5
6	171	5
7	355	5
8	515	5
9	712	5
10	1085	5
11	1245	5
12	1301	5
done	1301	5
0	5	6
1	9	6
2	15	6
done	15	6
0	3	3
1	9	3
2	19	3
3	31	3
4	39	3
5	44	3
done	44	3
0	3	3
1	9	3
2	18	3
3	36	3
4	49	3
5	61	3
6	69	3
7	89	3
8	106	3
9	117	3
10	130	3
11	163	3
12	204	3
13	254	3
14	276	3
15	279	3
done	279	3
0	4	7
1	10	7
2	17	7
3	27	7
4	34	7
5	39	7
done	39	7
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	4	8
1	11	8
2	28	4
3	75	4
4	227	4
5	751	4
6	2600	4
done	5000	4
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	12	13
1	27	13
2	65	13
3	151	13
4	409	13
5	907	13
6	3175	13
done	5000	13
0	9	12
1	20	10
2	47	10
3	75	10
4	124	10
5	173	10
6	279	10
7	467	10
8	744	10
9	1056	10
10	1180	10
11	1257	10
12	1269	10
13	1842	10
done	5000	10
0	11	15
1	28	11
2	69	10
3	168	10
4	437	10
5	1214	10
6	3501	10
done	5000	10
0	12	15
1	34	15
2	90	15
3	181	13
4	370	13
5	821	13
6	2477	13
done	5000	13
0	13	18
1	29	16
2	80	13
3	200	13
4	528	13
5	1053	13
6	1896	13
7	3473	13
8	4258	13
9	4423	13
10	4434	13
done	5001	13
0	15	21
1	37	17
2	100	13
3	314	13
4	1016	13
5	3669	13
done	5001	13
0	11	13
1	29	13
2	63	13
3	107	13
4	205	13
5	497	13
6	1548	13
done	5000	13
0	7	8
1	12	8
2	24	8
3	34	8
4	42	8
5	46	8
done	46	8
0	8	9
1	15	8
2	29	8
3	50	8
4	110	8
5	266	8
6	777	8
7	2659	8
done	5000	8

prune92.0ms

Filtered

67 candidates to 77 candidates (-14.9%)

Pruning

3 alts after pruning (3 fresh and 0 done)

	Pruned	Kept	Total
New	74	3	77
Fresh	0	0	0
Picked	1	0	1
Done	0	0	0
Total	75	3	78

Merged error: 0b

Counts

78 → 3

localize9.0ms

Local error

Found 4 expressions with local error:

0.0b	(sqrt (/ (sinh y) y))
0.0b	(/ (sinh y) y)
0.0b	(/ (sinh y) y)
0.0b	(* (sqrt (/ (sinh y) y)) (sqrt (/ (sinh y) y)))

rewrite37.0ms

Algorithm

rewrite-expression-head

Rules

90×	`add-sqr-sqrt`
79×	`sqrt-prod`
70×	`times-frac`
59×	`add-cube-cbrt` `*-un-lft-identity`
20×	`pow1`
18×	`swap-sqr`
16×	`associate-r` `associate-l`
10×	`add-exp-log` `add-cbrt-cube`
9×	`sqrt-pow1` `pow1/2` `unswap-sqr`
7×	`div-inv`
6×	`associate-/r` `associate-/l`
5×	`sqrt-div` `pow-prod-up`
4×	`add-log-exp`
3×	`pow-prod-down` `pow-sqr`
2×	`cbrt-undiv` `sinh-def` `rem-sqrt-square` `frac-2neg` `div-exp` `clear-num` `associate-/l/`
1×	`pow2` `frac-times` `pow-plus` `sqrt-unprod` `associate-r/` `associate-l/` `prod-exp` `rem-square-sqrt` `*-commutative` `cbrt-unprod`

Counts

4 → 168

Calls

4 calls:

4.0ms	(sqrt (/ (sinh y) y))
5.0ms	(/ (sinh y) y)
4.0ms	(/ (sinh y) y)
16.0ms	(* (sqrt (/ (sinh y) y)) (sqrt (/ (sinh y) y)))

series297.0ms

Counts

4 → 12

Calls

4 calls:

23.0ms	(sqrt (/ (sinh y) y))
13.0ms	(/ (sinh y) y)
13.0ms	(/ (sinh y) y)
248.0ms	(* (sqrt (/ (sinh y) y)) (sqrt (/ (sinh y) y)))

simplify1.4min

Counts

180 → 180

Iterations

Useful iterations: 1 (1.0ms)

Iter	Nodes	Cost
0	2	3
1	5	1
2	7	1
done	7	1
0	5	5
1	8	1
done	8	1
0	2	3
1	6	1
done	6	1
0	5	5
1	8	3
done	8	1
0	4	7
1	8	3
2	9	1
done	9	1
0	4	9
1	14	9
2	33	9
3	90	9
4	295	9
5	856	9
6	2462	9
done	5000	9
0	5	11
1	11	4
2	21	4
3	40	4
4	60	4
5	83	4
6	104	4
7	112	4
done	112	4
0	4	9
1	14	9
2	33	9
3	90	9
4	295	9
5	856	9
6	2462	9
done	5000	9
0	2	3
1	6	1
done	6	1
0	6	13
1	13	8
2	23	8
3	42	8
4	62	8
5	85	8
6	106	8
7	113	8
done	113	8
0	6	12
1	14	5
2	28	5
3	55	5
4	87	5
5	127	5
6	160	5
7	175	5
8	188	5
9	202	5
10	218	5
11	230	5
12	240	5
13	247	5
done	247	5
0	6	12
1	14	5
2	27	5
3	51	5
4	94	5
5	163	5
6	291	5
7	683	5
8	2388	5
done	5000	5
0	7	35
1	20	14
2	53	14
3	154	6
4	612	6
5	3389	6
done	5000	6
0	7	25
1	13	11
2	23	11
3	42	11
4	62	11
5	85	11
6	106	11
7	115	11
done	115	11
0	6	12
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	7	35
1	21	14
2	52	6
3	157	6
4	621	6
5	3496	6
done	5000	6
0	4	9
1	14	9
2	33	9
3	90	9
4	295	9
5	856	9
6	2462	9
done	5000	9
0	6	12
1	13	5
2	22	5
3	41	5
4	61	5
5	84	5
6	102	5
7	112	5
done	112	5
0	6	12
1	13	5
2	22	5
3	41	5
4	61	5
5	84	5
6	102	5
7	112	5
done	112	5
0	4	7
1	10	2
2	18	2
3	28	2
4	35	2
5	40	2
done	40	2
0	3	5
done	3	1
0	7	27
1	17	27
2	28	15
3	54	8
4	87	8
5	138	8
6	228	8
7	456	8
8	1356	8
done	5000	8
0	6	13
1	12	13
2	21	13
3	40	13
4	60	13
5	83	13
6	104	13
7	114	13
done	114	13
0	7	25
1	14	11
2	24	11
3	43	11
4	63	11
5	86	11
6	107	11
7	116	11
done	116	11
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	9	29
1	21	13
2	39	13
3	55	13
4	62	13
5	67	13
done	67	13
0	7	15
1	13	6
2	21	6
3	31	6
4	38	6
5	43	6
done	43	6
0	8	23
1	16	10
2	26	10
3	37	10
4	44	10
5	49	10
done	49	10
0	7	15
1	13	6
2	21	6
3	31	6
4	38	6
5	43	6
done	43	6
0	8	21
1	18	7
2	34	7
3	51	7
4	63	7
5	68	7
done	68	7
0	6	13
1	12	5
2	20	5
3	30	5
4	37	5
5	42	5
done	42	5
0	8	21
1	16	9
2	24	9
3	34	9
4	41	9
5	46	9
done	46	9
0	7	15
1	13	6
2	21	6
3	31	6
4	38	6
5	43	6
done	43	6
0	7	15
1	13	6
2	21	6
3	31	6
4	38	6
5	43	6
done	43	6
0	7	15
1	13	6
2	21	6
3	31	6
4	38	6
5	43	6
done	43	6
0	7	13
1	15	3
2	26	3
3	38	3
4	50	3
5	55	3
done	55	3
0	6	13
1	12	5
2	20	5
3	30	5
4	37	5
5	42	5
done	42	5
0	7	17
1	11	7
2	12	7
done	12	7
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	11
1	8	4
2	9	4
done	9	4
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	4	9
1	6	1
done	6	1
0	5	11
1	11	4
2	21	4
3	40	4
4	60	4
5	83	4
6	104	4
7	112	4
done	112	4
0	3	5
1	5	1
done	5	1
0	5	11
1	11	4
2	21	4
3	40	4
4	60	4
5	83	4
6	104	4
7	112	4
done	112	4
0	4	7
1	10	2
2	18	2
3	28	2
4	35	2
5	40	2
done	40	2
0	5	9
1	7	3
2	8	3
done	8	3
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	2	3
1	4	1
done	4	1
0	5	11
1	11	4
2	21	4
3	40	4
4	60	4
5	83	4
6	104	4
7	112	4
done	112	4
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	10	14
1	17	14
2	26	14
3	45	14
4	65	14
5	88	14
6	106	14
7	116	14
done	116	14
0	10	14
1	17	14
2	26	14
3	45	14
4	65	14
5	88	14
6	106	14
7	116	14
done	116	14
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	10	14
1	17	14
2	26	14
3	45	14
4	65	14
5	88	14
6	106	14
7	116	14
done	116	14
0	10	14
1	17	14
2	26	14
3	45	14
4	65	14
5	88	14
6	106	14
7	116	14
done	116	14
0	7	15
1	13	6
2	21	6
3	31	6
4	38	6
5	43	6
done	43	6
0	7	15
1	13	6
2	21	6
3	31	6
4	38	6
5	43	6
done	43	6
0	10	14
1	17	14
2	26	14
3	45	14
4	65	14
5	88	14
6	106	14
7	116	14
done	116	14
0	10	14
1	17	14
2	26	14
3	45	14
4	65	14
5	88	14
6	106	14
7	116	14
done	116	14
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	10	14
1	17	14
2	26	14
3	45	14
4	65	14
5	88	14
6	106	14
7	116	14
done	116	14
0	10	14
1	17	14
2	26	14
3	45	14
4	65	14
5	88	14
6	106	14
7	116	14
done	116	14
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	6	13
1	12	5
2	22	5
3	41	5
4	61	5
5	84	5
6	105	5
7	115	5
done	115	5
0	3	3
1	5	1
2	7	1
done	7	1
0	3	3
1	6	1
done	6	1
0	4	5
1	10	1
done	10	1
0	7	19
1	16	19
2	27	19
3	46	19
4	66	19
5	89	19
6	110	19
7	119	19
done	119	19
0	8	18
1	16	12
2	25	12
3	44	12
4	64	12
5	87	12
6	106	12
7	113	12
done	113	12
0	6	12
1	13	12
2	22	12
3	41	12
4	61	12
5	84	12
6	102	12
7	112	12
done	112	12
0	11	20
1	24	20
2	43	13
3	68	13
4	88	13
5	111	13
6	129	13
7	136	13
done	136	13
0	10	17
1	19	17
2	30	17
3	50	17
4	70	17
5	93	17
6	114	17
7	124	17
done	124	17
0	10	16
1	21	14
2	36	10
3	58	10
4	78	10
5	101	10
6	119	10
7	127	10
done	127	10
0	10	16
1	19	16
2	28	16
3	47	16
4	67	16
5	90	16
6	110	16
7	120	16
done	120	16
0	9	13
1	16	13
2	25	13
3	44	13
4	64	13
5	87	13
6	106	13
7	113	13
done	113	13
0	9	12
1	18	10
2	28	10
3	45	10
4	65	10
5	88	10
6	107	10
7	117	10
done	117	10
0	10	14
1	21	14
2	29	14
3	46	14
4	66	14
5	89	14
6	110	14
7	119	14
done	119	14
0	9	11
1	18	11
2	26	11
3	43	11
4	63	11
5	86	11
6	107	11
7	117	11
done	117	11
0	8	10
1	17	7
2	25	7
3	42	5
4	65	5
5	88	5
6	107	5
7	116	5
done	116	5
0	7	8
1	16	7
2	24	7
3	41	5
4	64	5
5	87	5
6	108	5
7	118	5
done	118	5
0	6	9
1	13	9
2	22	9
3	41	9
4	61	9
5	84	9
6	102	9
7	112	9
done	112	9
0	6	12
1	13	12
2	22	12
3	41	12
4	61	12
5	84	12
6	102	12
7	112	12
done	112	12
0	6	7
1	15	5
2	26	5
3	43	5
4	63	5
5	86	5
6	107	5
7	117	5
done	117	5
0	6	12
1	13	12
2	22	12
3	41	12
4	61	12
5	84	12
6	102	12
7	112	12
done	112	12
0	7	12
1	14	12
2	23	12
3	42	12
4	62	12
5	85	12
6	106	12
7	113	12
done	113	12
0	6	12
1	13	12
2	22	12
3	41	12
4	61	12
5	84	12
6	102	12
7	112	12
done	112	12
0	9	13
1	16	13
2	25	13
3	44	13
4	64	13
5	87	13
6	106	13
7	113	13
done	113	13
0	9	13
1	16	13
2	25	13
3	44	13
4	64	13
5	87	13
6	106	13
7	113	13
done	113	13
0	8	12
1	15	12
2	24	12
3	43	12
4	63	12
5	86	12
6	107	12
7	114	12
done	114	12
0	9	13
1	16	13
2	25	13
3	44	13
4	64	13
5	87	13
6	106	13
7	113	13
done	113	13
0	9	13
1	16	13
2	25	13
3	44	13
4	64	13
5	87	13
6	106	13
7	113	13
done	113	13
0	8	12
1	15	12
2	24	12
3	43	12
4	63	12
5	86	12
6	107	12
7	114	12
done	114	12
0	8	12
1	15	12
2	26	12
3	54	12
4	87	12
5	128	12
6	169	12
7	186	12
done	186	12
0	8	12
1	15	12
2	26	12
3	54	12
4	87	12
5	128	12
6	169	12
7	186	12
done	186	12
0	5	11
1	11	4
2	21	4
3	40	4
4	60	4
5	83	4
6	104	4
7	112	4
done	112	4
0	5	11
1	11	4
2	21	4
3	40	4
4	60	4
5	83	4
6	104	4
7	112	4
done	112	4
0	8	10
1	17	10
2	25	10
3	42	10
4	62	10
5	84	10
6	105	10
7	115	10
done	115	10
0	6	12
1	13	12
2	22	12
3	41	12
4	61	12
5	84	12
6	102	12
7	112	12
done	112	12
0	5	11
1	11	4
2	21	4
3	40	4
4	60	4
5	83	4
6	104	4
7	112	4
done	112	4
0	6	9
1	13	9
2	22	9
3	41	9
4	61	9
5	84	9
6	102	9
7	112	9
done	112	9
0	6	9
1	13	9
2	22	9
3	41	9
4	61	9
5	84	9
6	102	9
7	112	9
done	112	9
0	5	6
1	13	6
2	24	6
3	42	6
4	63	6
5	81	6
6	86	6
7	96	6
8	113	6
9	135	6
10	142	6
done	142	6
0	4	5
1	13	5
2	27	5
3	55	5
4	94	5
5	132	5
6	158	5
7	178	5
8	195	5
9	217	5
10	224	5
done	224	5
0	4	5
1	10	5
2	19	5
3	38	5
4	63	5
5	93	5
6	119	5
7	135	5
8	143	5
9	163	5
10	180	5
11	196	5
12	218	5
13	254	5
14	312	5
15	377	5
16	487	5
17	597	5
18	661	5
19	689	5
20	699	5
21	701	5
22	703	5
23	705	5
done	705	5
0	7	14
1	22	14
2	73	8
3	260	6
4	1058	6
5	4914	6
done	5000	6
0	5	11
1	11	11
2	20	11
3	39	11
4	59	11
5	82	11
6	101	11
7	108	11
done	108	11
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	5	14
1	18	14
2	49	6
3	162	6
4	751	6
5	3522	6
done	5000	6
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	3	3
1	9	3
2	18	3
3	31	3
4	45	3
5	54	3
6	57	3
done	57	3
0	2	2
done	2	2
0	7	13
1	19	13
2	35	13
3	51	13
4	58	13
5	63	13
done	63	13
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	6	10
1	14	10
2	23	10
3	34	10
4	41	10
5	46	10
done	46	10
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	6	9
1	16	7
2	28	7
3	41	7
4	48	7
5	53	7
done	53	7
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	6	9
1	14	9
2	21	9
3	31	9
4	38	9
5	43	9
done	43	9
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	5
1	13	3
2	21	3
3	29	3
4	36	3
5	41	3
done	41	3
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	5	7
1	9	7
done	9	7
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	4	4
1	6	4
done	6	4
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	2	3
1	4	1
done	4	1
0	3	4
1	9	4
2	18	4
3	37	4
4	57	4
5	80	4
6	100	4
7	107	4
done	107	4
0	3	3
1	5	3
done	5	3
0	3	4
1	9	4
2	18	4
3	31	4
4	39	4
5	46	4
6	51	4
7	56	4
8	62	4
9	66	4
done	66	4
0	5	8
1	13	8
2	24	8
3	54	8
4	94	8
5	144	8
6	198	8
7	225	8
done	225	8
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	4	4
1	12	2
2	22	2
3	33	2
4	44	2
5	58	2
6	75	2
7	83	2
8	87	2
9	95	2
10	103	2
11	111	2
12	123	2
13	158	2
14	199	2
15	234	2
16	261	2
17	272	2
18	277	2
19	283	2
done	283	2
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	3	4
1	9	4
2	18	4
3	31	4
4	39	4
5	46	4
6	51	4
7	56	4
8	62	4
9	66	4
done	66	4
0	3	3
1	4	3
done	4	3
0	5	6
1	13	6
2	24	6
3	42	6
4	63	6
5	81	6
6	86	6
7	96	6
8	113	6
9	135	6
10	142	6
done	142	6
0	4	5
1	13	5
2	27	5
3	55	5
4	94	5
5	132	5
6	158	5
7	178	5
8	195	5
9	217	5
10	224	5
done	224	5
0	4	5
1	10	5
2	19	5
3	38	5
4	63	5
5	93	5
6	119	5
7	135	5
8	143	5
9	163	5
10	180	5
11	196	5
12	218	5
13	254	5
14	312	5
15	377	5
16	487	5
17	597	5
18	661	5
19	689	5
20	699	5
21	701	5
22	703	5
23	705	5
done	705	5
0	7	14
1	22	14
2	73	8
3	260	6
4	1058	6
5	4914	6
done	5000	6
0	5	11
1	11	11
2	20	11
3	39	11
4	59	11
5	82	11
6	101	11
7	108	11
done	108	11
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	5	14
1	18	14
2	49	6
3	162	6
4	751	6
5	3522	6
done	5000	6
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	3	3
1	9	3
2	18	3
3	31	3
4	45	3
5	54	3
6	57	3
done	57	3
0	2	2
done	2	2
0	7	13
1	19	13
2	35	13
3	51	13
4	58	13
5	63	13
done	63	13
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	6	10
1	14	10
2	23	10
3	34	10
4	41	10
5	46	10
done	46	10
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	6	9
1	16	7
2	28	7
3	41	7
4	48	7
5	53	7
done	53	7
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	6	9
1	14	9
2	21	9
3	31	9
4	38	9
5	43	9
done	43	9
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	5
1	13	3
2	21	3
3	29	3
4	36	3
5	41	3
done	41	3
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	5	7
1	9	7
done	9	7
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	4	4
1	6	4
done	6	4
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	2	3
1	4	1
done	4	1
0	3	4
1	9	4
2	18	4
3	37	4
4	57	4
5	80	4
6	100	4
7	107	4
done	107	4
0	3	3
1	5	3
done	5	3
0	3	4
1	9	4
2	18	4
3	31	4
4	39	4
5	46	4
6	51	4
7	56	4
8	62	4
9	66	4
done	66	4
0	5	8
1	13	8
2	24	8
3	54	8
4	94	8
5	144	8
6	198	8
7	225	8
done	225	8
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	4	4
1	12	2
2	22	2
3	33	2
4	44	2
5	58	2
6	75	2
7	83	2
8	87	2
9	95	2
10	103	2
11	111	2
12	123	2
13	158	2
14	199	2
15	234	2
16	261	2
17	272	2
18	277	2
19	283	2
done	283	2
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	3	4
1	9	4
2	18	4
3	31	4
4	39	4
5	46	4
6	51	4
7	56	4
8	62	4
9	66	4
done	66	4
0	3	3
1	4	3
done	4	3
0	5	6
1	11	6
2	20	6
3	39	6
4	59	6
5	82	6
6	101	6
7	108	6
done	108	6
0	5	6
1	11	6
2	20	6
3	39	6
4	59	6
5	82	6
6	101	6
7	108	6
done	108	6
0	6	13
1	12	13
2	21	13
3	40	13
4	60	13
5	83	13
6	104	13
7	114	13
done	114	13
0	5	6
1	11	6
2	20	6
3	39	6
4	59	6
5	82	6
6	101	6
7	108	6
done	108	6
0	6	17
1	13	10
2	29	7
3	62	7
4	129	7
5	227	7
6	419	7
7	762	7
8	1811	7
9	3851	7
done	5000	7
0	6	12
1	13	6
2	22	6
3	41	6
4	61	6
5	84	6
6	102	6
7	112	6
done	112	6
0	5	6
1	11	6
2	20	6
3	39	6
4	59	6
5	82	6
6	101	6
7	108	6
done	108	6
0	5	6
1	11	6
2	20	6
3	39	6
4	59	6
5	82	6
6	101	6
7	108	6
done	108	6
0	5	6
1	11	6
2	20	6
3	39	6
4	59	6
5	82	6
6	101	6
7	108	6
done	108	6
0	8	14
1	20	14
2	37	7
3	53	7
4	60	7
5	65	7
done	65	7
0	6	7
1	12	7
2	19	7
3	29	7
4	36	7
5	41	7
done	41	7
0	7	11
1	15	11
2	24	11
3	35	11
4	42	11
5	47	11
done	47	11
0	6	7
1	12	7
2	19	7
3	29	7
4	36	7
5	41	7
done	41	7
0	7	10
1	17	8
2	30	4
3	43	4
4	50	4
5	55	4
done	55	4
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	7	10
1	15	10
2	22	10
3	32	10
4	39	10
5	44	10
done	44	10
0	6	7
1	12	7
2	19	7
3	29	7
4	36	7
5	41	7
done	41	7
0	6	7
1	12	7
2	19	7
3	29	7
4	36	7
5	41	7
done	41	7
0	6	7
1	12	7
2	19	7
3	29	7
4	36	7
5	41	7
done	41	7
0	6	6
1	14	4
2	22	4
3	30	4
4	37	4
5	42	4
done	42	4
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	6	8
1	10	8
done	10	8
0	5	6
1	11	6
2	20	6
3	39	6
4	59	6
5	82	6
6	101	6
7	108	6
done	108	6
0	5	5
1	7	5
done	7	5
0	5	6
1	11	6
2	20	6
3	39	6
4	59	6
5	82	6
6	101	6
7	108	6
done	108	6
0	3	4
1	5	1
done	5	1
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	2	2
1	4	1
done	4	1
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	102	5
7	112	5
done	112	5
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	4	4
1	6	4
done	6	4
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	2	2
done	2	2
0	3	3
1	6	1
done	6	1
0	5	6
1	11	6
2	20	6
3	39	6
4	59	6
5	82	6
6	101	6
7	108	6
done	108	6
0	5	6
1	11	6
2	20	6
3	39	6
4	59	6
5	82	6
6	101	6
7	108	6
done	108	6
0	12	13
1	27	13
2	65	13
3	151	13
4	409	13
5	907	13
6	3175	13
done	5000	13
0	9	12
1	20	10
2	47	10
3	75	10
4	124	10
5	173	10
6	279	10
7	467	10
8	744	10
9	1056	10
10	1180	10
11	1257	10
12	1269	10
13	1842	10
done	5000	10
0	81	215
1	247	206
2	1337	204
done	5001	204
0	12	13
1	27	13
2	65	13
3	151	13
4	409	13
5	907	13
6	3175	13
done	5000	13
0	9	12
1	20	10
2	47	10
3	75	10
4	124	10
5	173	10
6	279	10
7	467	10
8	744	10
9	1056	10
10	1180	10
11	1257	10
12	1269	10
13	1842	10
done	5000	10
0	11	15
1	28	11
2	69	10
3	168	10
4	437	10
5	1214	10
6	3501	10
done	5000	10
0	12	13
1	27	13
2	65	13
3	151	13
4	409	13
5	907	13
6	3175	13
done	5000	13
0	9	12
1	20	10
2	47	10
3	75	10
4	124	10
5	173	10
6	279	10
7	467	10
8	744	10
9	1056	10
10	1180	10
11	1257	10
12	1269	10
13	1842	10
done	5000	10
0	11	15
1	28	11
2	69	10
3	168	10
4	437	10
5	1214	10
6	3501	10
done	5000	10
0	12	13
1	27	13
2	65	13
3	151	13
4	409	13
5	907	13
6	3175	13
done	5000	13
0	57	135
1	177	133
2	926	117
done	5000	108
0	58	141
1	182	135
2	938	133
done	5000	117

prune199.0ms

Filtered

135 candidates to 180 candidates (-33.3%)

Pruning

3 alts after pruning (2 fresh and 1 done)

	Pruned	Kept	Total
New	180	0	180
Fresh	0	2	2
Picked	0	1	1
Done	0	0	0
Total	180	3	183

Merged error: 0b

Counts

183 → 3

localize8.0ms

Local error

Found 4 expressions with local error:

0.0b	(/ 1 (/ y (sinh y)))
0.0b	(sinh y)
0.0b	(* (sin x) (/ 1 (/ y (sinh y))))
0.0b	(/ y (sinh y))

rewrite41.0ms

Algorithm

rewrite-expression-head

Rules

162×	`times-frac`
106×	`add-sqr-sqrt`
94×	`*-un-lft-identity`
92×	`add-cube-cbrt`
47×	`associate-r`
36×	`add-exp-log`
20×	`add-cbrt-cube`
17×	`associate-/r*`
15×	`div-exp`
10×	`associate-/r/` `div-inv`
9×	`sinh-def`
7×	`pow1` `cbrt-undiv` `prod-exp`
6×	`associate-/l*`
5×	`unswap-sqr`
4×	`rec-exp` `1-exp` `add-log-exp`
3×	`associate-l` `cbrt-unprod`
2×	`frac-2neg` `clear-num`
1×	`pow-flip` `associate-r/` `pow-prod-down` `un-div-inv` `-commutative` `inv-pow`

Counts

4 → 192

Calls

4 calls:

7.0ms	(/ 1 (/ y (sinh y)))
1.0ms	(sinh y)
18.0ms	(* (sin x) (/ 1 (/ y (sinh y))))
4.0ms	(/ y (sinh y))

series70.0ms

Counts

4 → 12

Calls

4 calls:

13.0ms	(/ 1 (/ y (sinh y)))
9.0ms	(sinh y)
29.0ms	(* (sin x) (/ 1 (/ y (sinh y))))
19.0ms	(/ y (sinh y))

simplify6.9min

Counts

204 → 204

Iterations

Useful iterations: 1 (1.0ms)

Iter	Nodes	Cost
0	5	6
1	13	6
2	24	6
3	38	6
4	52	6
5	70	6
6	74	6
7	82	6
8	97	6
9	123	6
10	132	6
done	132	6
0	4	5
1	13	5
2	27	5
3	47	5
4	65	5
5	87	5
6	97	5
7	114	5
8	137	5
9	165	5
10	174	5
done	174	5
0	4	5
1	10	5
2	19	5
3	35	5
4	50	5
5	64	5
6	87	5
7	145	5
8	300	5
9	731	5
10	2794	5
done	5000	5
0	7	14
1	22	14
2	73	8
3	253	6
4	993	6
5	3711	6
done	5000	6
0	5	11
1	11	11
2	20	11
3	33	11
4	41	11
5	48	11
6	53	11
7	58	11
8	64	11
9	68	11
done	68	11
0	4	5
1	10	5
2	19	5
3	32	5
4	40	5
5	47	5
6	52	5
7	57	5
8	63	5
9	67	5
done	67	5
0	5	14
1	18	14
2	47	6
3	163	6
4	661	6
5	2608	6
done	5001	6
0	4	5
1	10	5
2	19	5
3	32	5
4	40	5
5	47	5
6	52	5
7	57	5
8	63	5
9	67	5
done	67	5
0	4	5
1	10	5
2	19	5
3	32	5
4	40	5
5	47	5
6	52	5
7	57	5
8	63	5
9	67	5
done	67	5
0	2	2
done	2	2
0	3	3
1	9	3
2	18	3
3	31	3
4	45	3
5	54	3
6	57	3
done	57	3
0	7	13
1	19	13
2	35	13
3	51	13
4	58	13
5	63	13
done	63	13
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	6	9
1	14	9
2	23	9
3	34	9
4	41	9
5	46	9
done	46	9
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	7
1	9	5
2	15	5
3	20	5
done	20	5
0	4	5
1	10	5
2	19	5
3	32	5
4	40	5
5	47	5
6	52	5
7	57	5
8	63	5
9	67	5
done	67	5
0	6	10
1	14	10
2	21	10
3	31	10
4	38	10
5	43	10
done	43	10
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	5	6
1	11	6
2	18	6
3	28	6
4	35	6
5	40	6
done	40	6
0	4	4
1	6	2
2	8	2
done	8	2
0	4	5
1	10	5
2	19	5
3	32	5
4	40	5
5	47	5
6	52	5
7	57	5
8	63	5
9	67	5
done	67	5
0	6	9
1	16	9
2	22	9
3	30	9
4	37	9
5	42	9
done	42	9
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	5	5
1	13	5
2	19	5
3	27	5
4	34	5
5	39	5
done	39	5
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	2	3
1	4	1
done	4	1
0	3	4
1	9	4
2	18	4
3	31	4
4	39	4
5	46	4
6	51	4
7	56	4
8	62	4
9	66	4
done	66	4
0	4	4
1	12	4
2	20	4
3	31	4
4	40	4
5	45	4
done	45	4
0	3	4
1	9	4
2	18	4
3	37	4
4	57	4
5	80	4
6	100	4
7	107	4
done	107	4
0	5	9
1	13	9
2	20	9
3	30	9
4	37	9
5	42	9
done	42	9
0	4	5
1	10	5
2	17	5
3	27	5
4	34	5
5	39	5
done	39	5
0	3	3
1	5	1
done	5	1
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	4	5
1	10	5
2	19	5
3	38	5
4	58	5
5	81	5
6	101	5
7	108	5
done	108	5
0	3	4
1	9	4
2	18	4
3	37	4
4	57	4
5	80	4
6	100	4
7	107	4
done	107	4
0	6	8
1	10	8
2	16	8
done	16	8
0	8	9
1	21	9
2	43	7
3	123	7
4	310	7
5	735	7
6	1255	7
7	2523	7
8	3711	7
9	4345	7
10	4785	7
11	4846	7
done	5001	7
0	10	11
1	20	10
2	37	10
3	62	10
4	105	10
5	198	10
6	316	10
7	417	10
8	462	10
9	464	10
done	464	10
0	9	10
1	20	9
2	36	9
3	64	9
4	111	9
5	194	9
6	286	9
7	403	9
8	530	9
9	544	9
done	544	9
0	11	12
1	26	11
2	62	10
3	128	10
4	279	10
5	738	10
6	1015	10
7	1080	10
done	1080	10
0	10	11
1	24	10
2	52	9
3	104	9
4	242	9
5	602	9
6	1032	9
7	1209	9
8	1232	9
9	1236	9
done	1236	9
0	12	13
1	29	12
2	59	10
3	134	10
4	284	10
5	742	10
6	1023	10
7	1086	10
done	1086	10
0	11	12
1	27	11
2	51	9
3	110	9
4	248	9
5	607	9
6	1035	9
7	1217	9
8	1240	9
9	1244	9
done	1244	9
0	10	11
1	25	10
2	49	9
3	111	9
4	275	9
5	744	9
6	1412	9
7	2107	9
8	2515	9
9	2677	9
10	2814	9
11	2927	9
12	3500	9
done	5000	9
0	9	10
1	25	10
2	56	8
3	161	8
4	439	8
5	1112	8
6	2412	8
7	4110	8
done	5000	8
0	9	10
1	24	10
2	51	8
3	161	8
4	473	8
5	1353	8
6	3349	8
done	5000	8
0	16	29
1	44	25
2	151	13
3	841	11
done	5000	11
0	14	29
1	42	25
2	126	11
3	651	11
4	4576	11
done	5000	11
0	12	29
1	35	29
2	118	13
3	655	11
4	4714	9
done	5000	9
0	10	21
1	23	21
2	45	17
3	123	17
4	310	17
5	722	17
6	1240	17
7	2500	17
8	3597	17
9	4197	17
10	4649	17
11	4710	17
done	5001	17
0	9	10
1	22	10
2	44	8
3	122	8
4	309	8
5	728	8
6	1247	8
7	2517	8
8	3708	8
9	4359	8
10	4815	8
11	4867	8
done	5000	8
0	10	29
1	33	29
2	119	9
3	633	9
4	4619	9
done	5000	9
0	9	10
1	22	10
2	44	8
3	122	8
4	309	8
5	728	8
6	1247	8
7	2517	8
8	3708	8
9	4359	8
10	4815	8
11	4867	8
done	5000	8
0	9	10
1	22	10
2	44	8
3	122	8
4	309	8
5	728	8
6	1247	8
7	2517	8
8	3708	8
9	4359	8
10	4815	8
11	4867	8
done	5000	8
0	10	11
1	21	11
2	34	11
3	60	9
4	140	9
5	304	9
6	496	9
7	852	9
8	1101	9
9	1200	9
10	1328	9
11	1363	9
12	1936	9
done	5000	9
0	10	11
1	21	11
2	34	11
3	60	9
4	140	9
5	304	9
6	496	9
7	852	9
8	1101	9
9	1200	9
10	1328	9
11	1363	9
12	1936	9
done	5000	9
0	11	12
1	22	11
2	33	11
3	48	9
4	67	9
5	74	9
6	79	9
7	84	9
8	90	9
9	94	9
done	94	9
0	11	12
1	22	11
2	33	11
3	48	9
4	67	9
5	74	9
6	79	9
7	84	9
8	90	9
9	94	9
done	94	9
0	12	13
1	25	12
2	43	12
3	74	10
4	116	10
5	124	10
done	124	10
0	12	13
1	25	12
2	43	12
3	74	10
4	116	10
5	124	10
done	124	10
0	10	11
1	21	11
2	32	9
3	58	9
4	69	9
5	76	9
6	81	9
7	86	9
8	92	9
9	96	9
done	96	9
0	10	11
1	21	11
2	32	9
3	58	9
4	69	9
5	76	9
6	81	9
7	86	9
8	92	9
9	96	9
done	96	9
0	11	12
1	24	12
2	42	10
3	87	10
4	108	10
5	115	10
done	115	10
0	11	12
1	24	12
2	42	10
3	87	10
4	108	10
5	115	10
done	115	10
0	10	18
1	23	18
2	38	18
3	64	14
4	144	14
5	313	14
6	505	14
7	870	14
8	1114	14
9	1208	14
10	1339	14
11	1368	14
12	1941	14
done	5000	14
0	9	10
1	20	10
2	33	10
3	59	8
4	139	8
5	303	8
6	494	8
7	852	8
8	1111	8
9	1204	8
10	1328	8
11	1355	8
12	1928	8
done	5001	8
0	12	20
1	29	18
2	66	16
3	111	14
4	130	14
5	137	14
6	142	14
7	147	14
8	153	14
9	157	14
done	157	14
0	11	14
1	24	12
2	42	10
3	66	8
4	76	8
5	83	8
6	88	8
7	93	8
8	99	8
9	103	8
done	103	8
0	14	22
1	35	20
2	99	18
3	277	16
4	481	16
5	517	16
done	517	16
0	13	18
1	30	16
2	70	14
3	172	12
4	276	12
5	291	12
done	291	12
0	11	16
1	22	10
2	50	8
3	88	8
4	96	8
5	97	8
done	97	8
0	13	19
1	30	17
2	67	15
3	144	13
4	190	13
5	202	13
done	202	13
0	12	15
1	27	13
2	56	11
3	105	9
4	123	9
5	130	9
done	130	9
0	10	13
1	19	7
2	33	5
3	38	5
4	39	5
done	39	5
0	12	18
1	29	16
2	66	12
3	130	10
4	183	10
5	200	10
done	200	10
0	11	14
1	26	12
2	55	8
3	93	6
4	113	6
5	119	6
done	119	6
0	8	12
1	17	4
2	20	4
3	22	2
4	26	2
done	26	2
0	7	10
1	14	6
2	29	4
3	33	2
4	37	2
done	37	2
0	8	10
1	15	8
2	25	6
3	38	4
4	40	4
done	40	4
0	13	17
1	25	15
2	58	13
3	138	11
4	268	11
5	425	11
6	879	11
7	1194	11
8	1314	11
9	1469	11
10	1504	11
11	2149	11
done	5000	11
0	11	17
1	24	16
2	43	16
3	67	14
4	112	14
5	127	14
6	132	14
7	137	14
8	143	14
9	147	14
done	147	14
0	10	11
1	21	10
2	32	10
3	47	8
4	66	8
5	74	8
6	79	8
7	84	8
8	90	8
9	94	8
done	94	8
0	13	19
1	32	18
2	76	18
3	197	16
4	475	16
5	539	16
done	539	16
0	12	15
1	27	14
2	52	14
3	120	12
4	240	12
5	265	12
done	265	12
0	10	13
1	19	10
2	39	8
3	83	8
4	93	8
5	95	8
done	95	8
0	12	16
1	27	15
2	51	15
3	103	13
4	202	13
5	219	13
done	219	13
0	11	12
1	24	11
2	42	11
3	73	9
4	114	9
5	124	9
done	124	9
0	9	10
1	16	7
2	25	5
3	35	5
4	36	5
done	36	5
0	11	15
1	26	14
2	50	12
3	95	10
4	147	10
5	166	10
done	166	10
0	10	11
1	23	10
2	41	8
3	67	6
4	90	6
5	98	6
done	98	6
0	7	9
1	14	4
2	17	4
3	19	2
4	23	2
done	23	2
0	6	7
1	11	4
2	16	2
3	20	2
done	20	2
0	7	7
1	12	6
2	15	6
3	19	4
4	31	4
done	31	4
0	12	14
1	22	13
2	44	13
3	102	11
4	259	11
5	418	11
6	885	11
7	1341	11
8	1459	11
9	1603	11
10	1644	11
11	2289	11
done	5000	11
0	10	16
1	23	16
2	41	14
3	81	14
4	112	14
5	121	14
6	126	14
7	131	14
8	137	14
9	141	14
done	141	14
0	9	10
1	20	10
2	31	8
3	57	8
4	68	8
5	75	8
6	80	8
7	85	8
8	91	8
9	95	8
done	95	8
0	12	18
1	31	18
2	74	16
3	203	16
4	472	16
5	533	16
done	533	16
0	11	14
1	26	14
2	51	12
3	133	12
4	237	12
5	259	12
done	259	12
0	9	12
1	18	10
2	36	8
3	61	8
4	71	8
5	73	8
done	73	8
0	11	15
1	26	15
2	50	13
3	116	13
4	201	13
5	217	13
done	217	13
0	10	11
1	23	11
2	41	9
3	86	9
4	109	9
5	116	9
done	116	9
0	8	9
1	15	7
2	24	5
3	27	5
4	28	5
done	28	5
0	10	14
1	25	10
2	53	10
3	103	10
4	151	10
5	169	10
done	169	10
0	9	10
1	22	6
2	40	6
3	62	6
4	83	6
5	90	6
done	90	6
0	6	8
1	12	4
2	15	2
3	19	2
done	19	2
0	5	6
1	10	4
2	15	2
3	19	2
done	19	2
0	6	6
1	11	6
2	14	4
3	29	4
4	30	4
done	30	4
0	11	13
1	21	13
2	43	11
3	115	11
4	251	11
5	410	11
6	857	11
7	1183	11
8	1305	11
9	1461	11
10	1502	11
11	2147	11
done	5000	11
0	4	4
1	7	2
2	10	2
done	10	2
0	4	4
1	7	2
2	10	2
done	10	2
0	6	6
1	11	6
2	14	4
3	29	4
4	30	4
done	30	4
0	9	10
1	22	10
2	44	8
3	124	8
4	311	8
5	736	8
6	1249	8
7	2497	8
8	3659	8
9	4265	8
10	4730	8
11	4795	8
done	5000	8
0	9	10
1	22	10
2	44	8
3	124	8
4	311	8
5	736	8
6	1249	8
7	2497	8
8	3659	8
9	4265	8
10	4730	8
11	4795	8
done	5000	8
0	8	9
1	21	9
2	43	7
3	123	7
4	310	7
5	735	7
6	1255	7
7	2523	7
8	3711	7
9	4345	7
10	4785	7
11	4846	7
done	5001	7
0	4	4
1	7	2
2	10	2
done	10	2
0	5	6
1	9	6
2	15	6
done	15	6
0	3	3
1	9	3
2	19	3
3	31	3
4	39	3
5	44	3
done	44	3
0	3	3
1	9	3
2	18	3
3	36	3
4	49	3
5	61	3
6	69	3
7	89	3
8	106	3
9	117	3
10	130	3
11	163	3
12	204	3
13	254	3
14	276	3
15	279	3
done	279	3
0	4	7
1	10	7
2	17	7
3	27	7
4	34	7
5	39	7
done	39	7
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	4	8
1	11	8
2	28	4
3	75	4
4	227	4
5	751	4
6	2600	4
done	5000	4
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	2	2
1	5	1
done	5	1
0	6	7
1	14	7
2	28	7
3	44	7
4	68	6
5	107	6
6	129	6
7	135	6
done	135	6
0	5	6
1	14	6
2	28	6
3	51	6
4	75	6
5	117	6
6	146	6
7	170	6
8	183	6
9	187	6
done	187	6
0	7	8
1	19	7
2	42	7
3	78	6
4	154	6
5	324	6
6	407	6
7	422	6
done	422	6
0	6	7
1	17	6
2	37	6
3	70	6
4	137	6
5	278	6
6	413	6
7	476	6
8	494	6
9	498	6
done	498	6
0	8	9
1	22	8
2	39	7
3	80	6
4	156	6
5	326	6
6	410	6
7	426	6
done	426	6
0	7	8
1	20	7
2	36	6
3	72	6
4	139	6
5	280	6
6	420	6
7	482	6
8	500	6
9	504	6
done	504	6
0	6	7
1	20	6
2	39	6
3	85	5
4	207	5
5	493	5
6	833	5
7	1296	5
8	1585	5
9	1721	5
10	1858	5
11	1942	5
12	2515	5
done	5000	5
0	6	7
1	16	7
2	31	7
3	64	5
4	177	5
5	421	5
6	886	5
7	2745	5
done	5000	5
0	11	20
1	33	16
2	107	10
3	441	8
4	2220	8
done	5000	8
0	9	20
1	31	16
2	79	8
3	328	8
4	1595	6
done	5000	6
0	7	15
1	17	15
2	30	15
3	56	11
4	136	11
5	307	11
6	497	11
7	857	11
8	1112	11
9	1215	11
10	1341	11
11	1368	11
12	1941	11
done	5000	11
0	6	7
1	16	7
2	29	7
3	55	5
4	135	5
5	306	5
6	497	5
7	859	5
8	1110	5
9	1210	5
10	1338	5
11	1366	5
12	1939	5
done	5001	5
0	7	20
1	24	20
2	72	8
3	360	6
4	1795	6
done	5001	6
0	6	7
1	16	7
2	29	7
3	55	5
4	135	5
5	306	5
6	497	5
7	859	5
8	1110	5
9	1210	5
10	1338	5
11	1366	5
12	1939	5
done	5001	5
0	6	7
1	16	7
2	29	7
3	55	5
4	135	5
5	306	5
6	497	5
7	859	5
8	1110	5
9	1210	5
10	1338	5
11	1366	5
12	1939	5
done	5001	5
0	2	2
1	5	1
done	5	1
0	4	5
1	11	5
2	22	5
3	42	5
4	56	5
5	68	5
6	81	5
7	99	5
8	120	5
9	139	5
10	145	5
11	149	5
12	158	5
13	165	5
done	165	5
0	9	17
1	23	15
2	40	13
3	57	13
4	65	13
5	72	13
6	77	13
7	82	13
8	88	13
9	92	13
done	92	13
0	7	8
1	15	7
2	23	7
3	34	7
4	42	7
5	49	7
6	54	7
7	59	7
8	65	7
9	69	7
done	69	7
0	8	11
1	18	9
2	28	7
3	40	7
4	48	7
5	55	7
6	60	7
7	65	7
8	71	7
9	75	7
done	75	7
0	7	8
1	15	7
2	23	7
3	34	7
4	42	7
5	49	7
6	54	7
7	59	7
8	65	7
9	69	7
done	69	7
0	11	19
1	29	17
2	71	15
3	149	13
4	202	13
5	207	13
done	207	13
0	8	9
1	18	8
2	27	8
3	36	6
4	56	6
5	66	6
done	66	6
0	10	15
1	24	13
2	48	11
3	89	9
4	120	9
5	125	9
done	125	9
0	8	9
1	18	8
2	27	8
3	36	6
4	56	6
5	66	6
done	66	6
0	8	13
1	16	7
2	30	7
3	39	7
done	39	7
0	7	8
1	17	7
2	30	7
3	56	5
4	136	5
5	307	5
6	495	5
7	854	5
8	1121	5
9	1222	5
10	1235	5
done	1235	5
0	10	16
1	24	14
2	45	12
3	73	10
4	84	10
5	89	10
done	89	10
0	8	9
1	18	8
2	27	8
3	36	6
4	56	6
5	66	6
done	66	6
0	9	12
1	21	10
2	36	8
3	52	6
4	60	6
5	65	6
done	65	6
0	8	9
1	18	8
2	27	8
3	36	6
4	56	6
5	66	6
done	66	6
0	7	10
1	13	4
2	18	4
done	18	4
0	7	8
1	17	7
2	30	7
3	56	5
4	136	5
5	307	5
6	495	5
7	854	5
8	1121	5
9	1222	5
10	1235	5
done	1235	5
0	9	15
1	23	13
2	44	9
3	68	7
4	83	7
5	89	7
done	89	7
0	7	8
1	17	7
2	26	7
3	35	5
4	55	5
5	65	5
done	65	5
0	8	11
1	20	9
2	35	5
3	51	3
4	58	3
5	63	3
done	63	3
0	7	8
1	17	7
2	26	7
3	35	5
4	55	5
5	65	5
done	65	5
0	5	9
1	11	1
done	11	1
0	6	7
1	16	6
2	29	6
3	55	4
4	135	4
5	306	4
6	497	4
7	855	4
8	1106	4
9	1207	4
10	1340	4
11	1367	4
12	1940	4
done	5001	4
0	4	7
1	8	3
2	12	1
done	12	1
0	6	7
1	16	6
2	29	6
3	55	4
4	135	4
5	306	4
6	497	4
7	855	4
8	1106	4
9	1207	4
10	1340	4
11	1367	4
12	1940	4
done	5001	4
0	5	7
1	9	5
2	11	3
3	12	3
done	12	3
0	6	7
1	16	6
2	29	4
3	57	2
4	102	2
5	154	2
6	200	2
7	269	2
8	293	2
9	294	2
10	298	2
done	298	2
0	10	14
1	19	12
2	38	10
3	71	8
4	125	8
5	199	8
6	336	8
7	383	8
8	396	8
9	424	8
10	456	8
11	720	8
12	2403	8
done	5000	8
0	4	4
1	6	3
done	6	3
0	8	14
1	18	13
2	26	13
3	37	13
4	45	13
5	52	13
6	57	13
7	62	13
8	68	13
9	72	13
done	72	13
0	7	8
1	15	7
2	23	7
3	34	7
4	42	7
5	49	7
6	54	7
7	59	7
8	65	7
9	69	7
done	69	7
0	7	8
1	15	7
2	23	7
3	34	7
4	42	7
5	49	7
6	54	7
7	59	7
8	65	7
9	69	7
done	69	7
0	7	8
1	15	7
2	23	7
3	34	7
4	42	7
5	49	7
6	54	7
7	59	7
8	65	7
9	69	7
done	69	7
0	10	16
1	26	15
2	53	15
3	92	13
4	159	13
5	236	13
done	236	13
0	8	9
1	18	8
2	27	8
3	36	6
4	56	6
5	66	6
done	66	6
0	9	12
1	21	11
2	35	11
3	56	9
4	90	9
5	135	9
done	135	9
0	8	9
1	18	8
2	27	8
3	36	6
4	56	6
5	66	6
done	66	6
0	7	10
1	13	7
2	24	7
3	33	7
done	33	7
0	7	8
1	17	7
2	30	7
3	56	5
4	136	5
5	307	5
6	495	5
7	854	5
8	1121	5
9	1222	5
10	1235	5
done	1235	5
0	9	13
1	21	12
2	34	12
3	50	10
4	81	10
5	103	10
done	103	10
0	8	9
1	18	8
2	27	8
3	36	6
4	56	6
5	66	6
done	66	6
0	8	9
1	18	8
2	27	8
3	36	6
4	56	6
5	66	6
done	66	6
0	8	9
1	18	8
2	27	8
3	36	6
4	56	6
5	66	6
done	66	6
0	6	7
1	10	4
2	15	4
done	15	4
0	7	8
1	17	7
2	30	7
3	56	5
4	136	5
5	307	5
6	495	5
7	854	5
8	1121	5
9	1222	5
10	1235	5
done	1235	5
0	8	12
1	20	11
2	33	9
3	50	7
4	70	7
5	77	7
done	77	7
0	7	8
1	17	7
2	26	7
3	35	5
4	55	5
5	65	5
done	65	5
0	7	8
1	17	7
2	26	5
3	39	3
4	50	3
5	55	3
done	55	3
0	7	8
1	17	7
2	26	7
3	35	5
4	55	5
5	65	5
done	65	5
0	4	6
1	8	1
done	8	1
0	6	7
1	16	6
2	29	6
3	55	4
4	135	4
5	306	4
6	497	4
7	855	4
8	1106	4
9	1207	4
10	1340	4
11	1367	4
12	1940	4
done	5001	4
0	3	4
1	5	1
done	5	1
0	6	7
1	16	6
2	29	6
3	55	4
4	135	4
5	306	4
6	497	4
7	855	4
8	1106	4
9	1207	4
10	1340	4
11	1367	4
12	1940	4
done	5001	4
0	4	4
1	6	3
done	6	3
0	6	7
1	16	6
2	29	4
3	57	2
4	102	2
5	154	2
6	200	2
7	269	2
8	293	2
9	294	2
10	298	2
done	298	2
0	9	11
1	16	10
2	29	10
3	51	8
4	110	8
5	186	8
6	312	8
7	414	8
8	427	8
9	456	8
10	488	8
11	755	8
12	2448	8
done	5001	8
0	4	4
1	6	3
done	6	3
0	7	13
1	17	13
2	25	13
3	36	13
4	44	13
5	51	13
6	56	13
7	61	13
8	67	13
9	71	13
done	71	13
0	6	7
1	14	7
2	22	7
3	33	7
4	41	7
5	48	7
6	53	7
7	58	7
8	64	7
9	68	7
done	68	7
0	6	7
1	14	7
2	22	7
3	33	7
4	41	7
5	48	7
6	53	7
7	58	7
8	64	7
9	68	7
done	68	7
0	6	7
1	14	7
2	22	7
3	33	7
4	41	7
5	48	7
6	53	7
7	58	7
8	64	7
9	68	7
done	68	7
0	9	15
1	25	15
2	52	15
3	91	13
4	158	13
5	238	13
done	238	13
0	7	8
1	17	8
2	26	8
3	35	6
4	55	6
5	65	6
done	65	6
0	8	11
1	20	11
2	34	11
3	55	9
4	89	9
5	127	9
done	127	9
0	7	8
1	17	8
2	26	8
3	35	6
4	55	6
5	65	6
done	65	6
0	6	9
1	12	7
2	23	7
3	32	7
done	32	7
0	6	7
1	16	7
2	29	7
3	55	5
4	135	5
5	306	5
6	495	5
7	846	5
8	1108	5
9	1215	5
10	1228	5
done	1228	5
0	8	12
1	20	12
2	33	12
3	49	10
4	80	10
5	100	10
done	100	10
0	7	8
1	17	8
2	26	8
3	35	6
4	55	6
5	65	6
done	65	6
0	7	8
1	17	8
2	26	8
3	35	6
4	55	6
5	65	6
done	65	6
0	7	8
1	17	8
2	26	8
3	35	6
4	55	6
5	65	6
done	65	6
0	5	6
1	9	4
2	14	4
done	14	4
0	6	7
1	16	7
2	29	7
3	55	5
4	135	5
5	306	5
6	495	5
7	846	5
8	1108	5
9	1215	5
10	1228	5
done	1228	5
0	7	11
1	19	7
2	34	7
3	55	7
4	74	7
5	80	7
done	80	7
0	6	7
1	16	7
2	25	7
3	34	5
4	54	5
5	64	5
done	64	5
0	6	7
1	16	3
2	27	3
3	37	3
4	45	3
5	50	3
done	50	3
0	6	7
1	16	7
2	25	7
3	34	5
4	54	5
5	64	5
done	64	5
0	3	5
1	6	1
done	6	1
0	5	6
1	15	6
2	28	6
3	54	4
4	134	4
5	305	4
6	495	4
7	856	4
8	1116	4
9	1216	4
10	1336	4
11	1372	4
12	1945	4
done	5000	4
0	2	3
1	4	1
done	4	1
0	5	6
1	15	6
2	28	6
3	54	4
4	134	4
5	305	4
6	495	4
7	856	4
8	1116	4
9	1216	4
10	1336	4
11	1372	4
12	1945	4
done	5000	4
0	3	3
1	5	3
done	5	3
0	5	6
1	15	2
2	30	2
3	62	2
4	106	2
5	158	2
6	206	2
7	272	2
8	295	2
9	296	2
10	300	2
done	300	2
0	8	10
1	15	10
2	28	10
3	50	8
4	109	8
5	185	8
6	309	8
7	408	8
8	421	8
9	448	8
10	480	8
11	747	8
12	2424	8
done	5000	8
0	3	3
1	6	1
done	6	1
0	5	6
1	15	6
2	28	6
3	54	4
4	134	4
5	305	4
6	495	4
7	856	4
8	1116	4
9	1216	4
10	1336	4
11	1372	4
12	1945	4
done	5000	4
0	5	6
1	15	4
2	32	4
3	67	4
4	109	4
5	165	4
6	227	4
7	326	4
8	435	4
9	521	4
10	546	4
11	569	4
12	635	4
13	1024	4
14	3641	4
done	5000	4
0	7	13
1	17	13
2	25	13
3	36	13
4	44	13
5	51	13
6	56	13
7	61	13
8	67	13
9	71	13
done	71	13
0	6	7
1	14	7
2	22	7
3	33	7
4	41	7
5	48	7
6	53	7
7	58	7
8	64	7
9	68	7
done	68	7
0	9	15
1	25	15
2	52	15
3	91	13
4	158	13
5	238	13
done	238	13
0	8	11
1	20	11
2	34	11
3	55	9
4	89	9
5	127	9
done	127	9
0	6	9
1	12	7
2	23	7
3	32	7
done	32	7
0	8	12
1	20	12
2	33	12
3	49	10
4	80	10
5	100	10
done	100	10
0	7	8
1	17	8
2	26	8
3	35	6
4	55	6
5	65	6
done	65	6
0	5	6
1	9	4
2	14	4
done	14	4
0	7	11
1	19	7
2	34	7
3	55	7
4	74	7
5	80	7
done	80	7
0	6	7
1	16	3
2	27	3
3	37	3
4	45	3
5	50	3
done	50	3
0	3	5
1	6	1
done	6	1
0	2	3
1	4	1
done	4	1
0	3	3
1	5	3
done	5	3
0	8	10
1	15	10
2	28	10
3	50	8
4	109	8
5	185	8
6	309	8
7	408	8
8	421	8
9	448	8
10	480	8
11	747	8
12	2424	8
done	5000	8
0	6	7
1	16	6
2	29	6
3	56	4
4	105	4
5	161	4
6	222	4
7	319	4
8	427	4
9	516	4
10	539	4
11	562	4
12	628	4
13	1014	4
14	3640	4
done	5000	4
0	6	7
1	16	6
2	29	6
3	56	4
4	105	4
5	161	4
6	222	4
7	319	4
8	427	4
9	516	4
10	539	4
11	562	4
12	628	4
13	1014	4
14	3640	4
done	5000	4
0	5	6
1	15	4
2	32	4
3	67	4
4	109	4
5	165	4
6	227	4
7	326	4
8	435	4
9	521	4
10	546	4
11	569	4
12	635	4
13	1024	4
14	3641	4
done	5000	4
0	3	3
1	5	3
done	5	3
0	12	13
1	28	13
2	74	13
3	187	13
4	555	13
5	1331	13
done	5001	13
0	9	12
1	17	10
2	35	10
3	46	10
4	50	10
done	50	10
0	10	13
1	20	10
2	39	10
3	73	10
4	146	10
5	340	10
6	940	10
7	3072	10
done	5001	10
0	12	15
1	34	15
2	90	15
3	181	13
4	370	13
5	821	13
6	2477	13
done	5000	13
0	13	18
1	29	16
2	80	13
3	200	13
4	528	13
5	1053	13
6	1896	13
7	3473	13
8	4258	13
9	4423	13
10	4434	13
done	5001	13
0	15	21
1	37	17
2	100	13
3	314	13
4	1016	13
5	3669	13
done	5001	13
0	11	13
1	29	13
2	63	13
3	107	13
4	205	13
5	497	13
6	1548	13
done	5000	13
0	7	8
1	12	8
2	24	8
3	34	8
4	42	8
5	46	8
done	46	8
0	8	9
1	15	8
2	29	8
3	50	8
4	110	8
5	266	8
6	777	8
7	2659	8
done	5000	8
0	12	13
1	27	13
2	65	13
3	151	13
4	409	13
5	907	13
6	3175	13
done	5000	13
0	9	12
1	20	10
2	47	10
3	75	10
4	124	10
5	173	10
6	279	10
7	467	10
8	744	10
9	1056	10
10	1180	10
11	1257	10
12	1269	10
13	1842	10
done	5000	10
0	11	15
1	28	11
2	69	10
3	168	10
4	437	10
5	1214	10
6	3501	10
done	5000	10

prune175.0ms

Filtered

145 candidates to 204 candidates (-40.7%)

Pruning

3 alts after pruning (1 fresh and 2 done)

	Pruned	Kept	Total
New	204	0	204
Fresh	0	1	1
Picked	0	1	1
Done	0	1	1
Total	204	3	207

Merged error: 0b

Counts

207 → 3

localize12.0ms

Local error

Found 4 expressions with local error:

0.0b	(* (sin x) (exp (- (log (sinh y)) (log y))))
0.0b	(sinh y)
0.0b	(exp (- (log (sinh y)) (log y)))
0.7b	(- (log (sinh y)) (log y))

rewrite30.0ms

Algorithm

rewrite-expression-head

Rules

19×	`*-un-lft-identity`
17×	`add-sqr-sqrt`
14×	`pow1`
12×	`log-prod`
11×	`add-cube-cbrt`
10×	`exp-sum`
9×	`associate--l+`
8×	`exp-prod` `associate-r` `log-pow` `distribute-lft-out--`
6×	`add-cbrt-cube`
5×	`add-exp-log` `add-log-exp`
3×	`sub-neg` `associate-l` `associate--r+`
2×	`sinh-def` `exp-diff` `diff-log` `rem-exp-log` `difference-of-squares`
1×	`associate--l-` `log-div` `flip3--` `associate-r/` `pow-prod-down` `prod-exp` `-commutative` `flip--` `cbrt-unprod` `unswap-sqr`

Counts

4 → 79

Calls

4 calls:

12.0ms	(* (sin x) (exp (- (log (sinh y)) (log y))))
2.0ms	(sinh y)
7.0ms	(exp (- (log (sinh y)) (log y)))
6.0ms	(- (log (sinh y)) (log y))

series144.0ms

Counts

4 → 12

Calls

4 calls:

43.0ms	(* (sin x) (exp (- (log (sinh y)) (log y))))
9.0ms	(sinh y)
48.0ms	(exp (- (log (sinh y)) (log y)))
44.0ms	(- (log (sinh y)) (log y))

simplify3.7min

Counts

91 → 91

Iterations

Useful iterations: 1 (1.0ms)

Iter	Nodes	Cost
0	3	4
1	9	4
2	18	4
3	37	4
4	57	4
5	80	4
6	100	4
7	107	4
done	107	4
0	6	7
1	14	7
2	25	7
3	43	7
4	64	7
5	82	7
6	87	7
7	97	7
8	114	7
9	136	7
10	143	7
done	143	7
0	6	7
1	17	7
2	30	4
3	60	4
4	119	4
5	217	4
6	427	4
7	729	4
8	1192	4
9	1872	4
10	2467	4
11	2713	4
12	2898	4
13	2950	4
14	3551	4
done	5001	4
0	7	15
1	15	15
2	26	15
3	44	15
4	65	15
5	83	15
6	88	15
7	98	15
8	115	15
9	137	15
10	144	15
done	144	15
0	6	7
1	14	7
2	25	7
3	43	7
4	64	7
5	82	7
6	87	7
7	97	7
8	114	7
9	136	7
10	143	7
done	143	7
0	7	20
1	16	20
2	41	8
3	101	8
4	267	8
5	1128	8
done	5001	8
0	6	7
1	14	7
2	25	7
3	43	7
4	64	7
5	82	7
6	87	7
7	97	7
8	114	7
9	136	7
10	143	7
done	143	7
0	6	7
1	14	7
2	25	7
3	43	7
4	64	7
5	82	7
6	87	7
7	97	7
8	114	7
9	136	7
10	143	7
done	143	7
0	8	10
1	28	10
2	60	10
3	106	10
4	214	10
5	596	10
6	2505	10
done	5001	10
0	9	20
1	22	17
2	40	17
3	57	16
4	86	16
5	179	16
6	467	16
7	1289	16
8	3958	16
done	5000	16
0	3	3
done	3	3
0	7	13
1	18	13
2	35	13
3	70	13
4	142	13
5	444	13
6	1362	13
done	5000	13
0	5	6
1	12	6
2	22	6
3	38	6
4	54	6
5	69	6
6	78	6
7	83	6
8	92	6
9	109	6
10	128	6
11	136	6
done	136	6
0	7	8
1	14	8
2	24	8
3	36	8
4	44	8
5	49	8
done	49	8
0	7	8
1	15	8
2	26	8
3	38	8
4	46	8
5	51	8
done	51	8
0	5	6
1	13	6
2	24	6
3	42	6
4	63	6
5	81	6
6	86	6
7	96	6
8	113	6
9	135	6
10	142	6
done	142	6
0	5	6
1	13	6
2	24	6
3	42	6
4	63	6
5	81	6
6	86	6
7	96	6
8	113	6
9	135	6
10	142	6
done	142	6
0	5	6
1	13	6
2	24	6
3	42	6
4	63	6
5	81	6
6	86	6
7	96	6
8	113	6
9	135	6
10	142	6
done	142	6
0	5	6
1	13	6
2	24	6
3	42	6
4	63	6
5	81	6
6	86	6
7	96	6
8	113	6
9	135	6
10	142	6
done	142	6
0	7	10
1	17	10
2	33	9
3	63	9
4	111	9
5	192	9
6	278	9
7	369	9
8	384	9
9	385	9
done	385	9
0	6	7
1	14	7
2	25	7
3	43	7
4	64	7
5	82	7
6	87	7
7	97	7
8	114	7
9	136	7
10	143	7
done	143	7
0	6	6
1	16	5
2	26	3
3	49	3
4	73	3
5	92	3
6	96	3
7	112	3
8	134	3
9	137	3
done	137	3
0	6	7
1	14	7
2	22	7
3	32	7
4	39	7
5	44	7
done	44	7
0	6	7
1	14	7
2	22	7
3	32	7
4	39	7
5	44	7
done	44	7
0	5	6
1	13	6
2	24	6
3	42	6
4	63	6
5	81	6
6	86	6
7	96	6
8	113	6
9	135	6
10	142	6
done	142	6
0	5	5
1	6	5
done	6	5
0	3	3
done	3	3
0	8	16
1	18	16
2	32	16
3	55	16
4	94	16
5	151	16
6	265	16
7	661	16
8	2378	16
done	5000	16
0	7	8
1	15	8
2	26	8
3	44	8
4	65	8
5	83	8
6	88	8
7	98	8
8	115	8
9	137	8
10	144	8
done	144	8
0	2	2
1	5	1
done	5	1
0	8	9
1	18	9
2	29	9
3	41	9
4	49	9
5	54	9
done	54	9
0	2	2
1	5	1
done	5	1
0	2	2
1	5	1
done	5	1
0	2	2
1	5	1
done	5	1
0	2	2
1	5	1
done	5	1
0	4	4
1	10	2
2	20	2
3	35	2
4	45	2
5	53	2
6	64	2
7	73	2
8	82	2
9	86	2
done	86	2
0	4	4
1	7	4
2	9	3
done	9	3
0	6	9
1	14	7
2	24	7
3	37	7
4	50	5
5	66	5
6	95	5
7	184	5
8	449	5
9	1753	5
done	5001	5
0	7	8
1	18	8
2	28	5
3	40	5
4	51	5
5	60	5
6	77	5
7	90	5
8	99	5
9	109	5
10	124	5
11	152	5
12	191	5
13	229	5
14	248	5
15	260	5
done	260	5
0	5	5
1	11	3
2	18	3
3	28	3
4	35	3
5	40	3
done	40	3
0	7	8
1	18	8
2	28	5
3	40	5
4	51	5
5	60	5
6	77	5
7	90	5
8	99	5
9	109	5
10	124	5
11	152	5
12	191	5
13	229	5
14	248	5
15	260	5
done	260	5
0	3	3
1	5	1
done	5	1
0	6	7
1	17	7
2	30	4
3	60	4
4	119	4
5	217	4
6	427	4
7	729	4
8	1192	4
9	1872	4
10	2467	4
11	2713	4
12	2898	4
13	2950	4
14	3551	4
done	5001	4
0	4	4
1	10	2
2	20	2
3	35	2
4	45	2
5	53	2
6	64	2
7	73	2
8	82	2
9	86	2
done	86	2
0	4	4
1	7	4
2	9	3
done	9	3
0	4	4
1	10	2
2	20	2
3	35	2
4	45	2
5	53	2
6	64	2
7	73	2
8	82	2
9	86	2
done	86	2
0	3	3
done	3	1
0	7	8
1	18	6
2	31	5
3	63	5
4	133	5
5	252	5
6	514	5
7	895	5
8	1508	5
9	2294	5
10	2639	5
11	2755	5
12	2797	5
13	2848	5
14	3451	5
done	5000	5
0	7	8
1	18	8
2	31	5
3	63	5
4	139	5
5	266	5
6	544	5
7	1079	5
8	3122	5
done	5000	5
0	8	17
1	19	17
2	32	11
3	62	11
4	121	11
5	219	11
6	429	11
7	732	11
8	1197	11
9	1869	11
10	2468	11
11	2714	11
12	2910	11
13	2961	11
14	3558	11
done	5000	11
0	7	8
1	18	8
2	31	5
3	61	5
4	120	5
5	218	5
6	428	5
7	735	5
8	1194	5
9	1881	5
10	2467	5
11	2718	5
12	2903	5
13	2954	5
14	3553	5
done	5000	5
0	8	23
1	22	22
2	57	6
3	197	6
4	911	6
done	5001	6
0	7	8
1	18	8
2	31	5
3	61	5
4	120	5
5	218	5
6	428	5
7	735	5
8	1194	5
9	1881	5
10	2467	5
11	2718	5
12	2903	5
13	2954	5
14	3553	5
done	5000	5
0	7	8
1	18	8
2	31	5
3	61	5
4	120	5
5	218	5
6	428	5
7	735	5
8	1194	5
9	1881	5
10	2467	5
11	2718	5
12	2903	5
13	2954	5
14	3553	5
done	5000	5
0	5	6
1	9	6
2	15	6
done	15	6
0	3	3
1	9	3
2	19	3
3	31	3
4	39	3
5	44	3
done	44	3
0	3	3
1	9	3
2	18	3
3	36	3
4	49	3
5	61	3
6	69	3
7	89	3
8	106	3
9	117	3
10	130	3
11	163	3
12	204	3
13	254	3
14	276	3
15	279	3
done	279	3
0	4	7
1	10	7
2	17	7
3	27	7
4	34	7
5	39	7
done	39	7
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	4	8
1	11	8
2	28	4
3	75	4
4	227	4
5	751	4
6	2600	4
done	5000	4
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	3	3
1	9	3
2	16	3
3	26	3
4	33	3
5	38	3
done	38	3
0	9	10
1	21	10
2	38	7
3	79	7
4	191	7
5	426	7
6	987	7
7	1849	7
8	2990	7
9	4999	7
done	5000	7
0	9	10
1	20	10
2	37	10
3	72	10
4	138	10
5	256	10
6	297	10
7	386	10
8	537	10
9	559	10
10	560	10
done	560	10
0	10	11
1	25	11
2	43	8
3	99	8
4	270	8
5	639	8
6	1441	8
7	2622	8
8	4182	8
done	5000	8
0	10	11
1	24	11
2	46	8
3	101	8
4	287	8
5	761	8
6	2183	8
done	5000	8
0	13	32
1	33	31
2	93	11
3	318	11
4	1711	9
done	5000	9
0	11	23
1	23	23
2	40	17
3	81	17
4	193	17
5	428	17
6	994	17
7	1865	17
8	3025	17
done	5000	17
0	10	11
1	22	11
2	39	8
3	80	8
4	192	8
5	427	8
6	988	8
7	1852	8
8	3001	8
done	5000	8
0	11	32
1	33	32
2	91	9
3	311	9
4	1566	9
done	5001	9
0	10	11
1	22	11
2	39	8
3	80	8
4	192	8
5	427	8
6	988	8
7	1852	8
8	3001	8
done	5000	8
0	10	11
1	22	11
2	39	8
3	80	8
4	192	8
5	427	8
6	988	8
7	1852	8
8	3001	8
done	5000	8
0	11	12
1	23	12
2	36	9
3	66	9
4	125	9
5	224	9
6	434	9
7	741	9
8	1215	9
9	1916	9
10	2528	9
11	2782	9
12	2972	9
13	3024	9
14	3625	9
done	5001	9
0	11	12
1	23	12
2	36	9
3	66	9
4	125	9
5	224	9
6	434	9
7	741	9
8	1215	9
9	1916	9
10	2528	9
11	2782	9
12	2972	9
13	3024	9
14	3625	9
done	5001	9
0	7	7
1	14	5
2	28	5
3	53	5
4	87	5
5	130	5
6	205	5
7	418	5
8	564	5
9	765	5
10	1159	5
11	1344	5
12	1425	5
13	1466	5
14	1510	5
15	1572	5
done	1572	5
0	9	12
1	18	10
2	32	10
3	49	10
4	62	8
5	82	8
6	125	8
7	255	8
8	652	8
9	2533	8
done	5000	8
0	8	8
1	15	6
2	22	6
3	32	6
4	39	6
5	44	6
done	44	6
0	6	6
1	9	4
done	9	2
0	7	7
1	14	5
2	28	5
3	53	5
4	87	5
5	130	5
6	205	5
7	418	5
8	564	5
9	765	5
10	1159	5
11	1344	5
12	1425	5
13	1466	5
14	1510	5
15	1572	5
done	1572	5
0	11	20
1	25	20
2	40	14
3	70	14
4	129	14
5	228	14
6	438	14
7	743	14
8	1222	14
9	1921	14
10	2527	14
11	2778	14
12	2968	14
13	3020	14
14	3623	14
done	5000	14
0	10	11
1	22	11
2	35	8
3	65	8
4	124	8
5	223	8
6	433	8
7	741	8
8	1213	8
9	1905	8
10	2497	8
11	2736	8
12	2921	8
13	2973	8
14	3572	8
done	5001	8
0	4	4
1	7	2
2	10	2
done	10	2
0	10	11
1	22	11
2	39	8
3	80	8
4	192	8
5	427	8
6	991	8
7	1850	8
8	3005	8
done	5000	8
0	10	11
1	22	11
2	39	8
3	80	8
4	192	8
5	427	8
6	991	8
7	1850	8
8	3005	8
done	5000	8
0	9	10
1	21	10
2	38	7
3	79	7
4	191	7
5	426	7
6	987	7
7	1849	7
8	2990	7
9	4999	7
done	5000	7
0	7	7
1	14	5
2	28	5
3	53	5
4	87	5
5	130	5
6	205	5
7	418	5
8	564	5
9	765	5
10	1159	5
11	1344	5
12	1425	5
13	1466	5
14	1510	5
15	1572	5
done	1572	5
0	15	17
1	35	17
2	93	17
3	192	17
4	487	17
5	1353	17
done	5000	17
0	14	17
1	31	15
2	62	12
3	165	12
4	282	12
5	381	12
6	427	12
done	427	12
0	14	18
1	31	17
2	67	17
3	170	17
4	421	17
5	981	14
6	2109	12
done	5000	12
0	12	13
1	27	13
2	65	13
3	151	13
4	409	13
5	907	13
6	3175	13
done	5000	13
0	15	18
1	35	16
2	73	13
3	205	12
4	440	10
5	722	10
6	1024	10
7	1643	10
8	2222	10
9	2455	10
10	2598	10
11	2727	10
12	3401	10
done	5001	10
0	15	19
1	35	18
2	79	17
3	216	14
4	654	11
5	1912	10
done	5000	10
0	11	13
1	29	13
2	63	13
3	107	13
4	205	13
5	497	13
6	1548	13
done	5000	13
0	7	8
1	12	8
2	24	8
3	34	8
4	42	8
5	46	8
done	46	8
0	8	9
1	15	8
2	29	8
3	50	8
4	110	8
5	266	8
6	777	8
7	2659	8
done	5000	8
0	12	15
1	34	15
2	90	15
3	181	13
4	370	13
5	821	13
6	2477	13
done	5000	13
0	18	21
1	39	19
2	79	16
3	227	15
4	610	13
5	1335	13
6	2204	13
7	3989	13
done	5000	13
0	18	22
1	39	21
2	87	20
3	242	17
4	824	14
5	2787	13
done	5000	13

prune100.0ms

Filtered

70 candidates to 91 candidates (-30.0%)

Pruning

3 alts after pruning (0 fresh and 3 done)

	Pruned	Kept	Total
New	91	0	91
Fresh	0	0	0
Picked	0	1	1
Done	0	2	2
Total	91	3	94

Merged error: 0b

Counts

94 → 3

regimes165.0ms

Accuracy

0% (0.0b remaining)

Error of 0.1b against oracle of 0.0b and baseline of 0.1b

bsearch0.0ms

simplify1.0ms

Iterations

Useful iterations: 0 (0.0ms)

Iter	Nodes	Cost
0	8	14
1	9	14
done	9	14

end0.0ms

sample2.8s

Algorithm

intervals

Results

955.0ms	2997×	body	1280	valid
511.0ms	2436×	body	640	valid
461.0ms	8524×	body	80	valid
194.0ms	1228×	body	320	valid
62.0ms	600×	body	160	valid

Details

sample97.0ms

simplify20.6s

prune3.0ms

localize7.0ms

rewrite18.0ms

series48.0ms

simplify4.1min

prune92.0ms

localize9.0ms

rewrite37.0ms

series297.0ms

simplify1.4min

prune199.0ms

localize8.0ms

rewrite41.0ms

series70.0ms

simplify6.9min

prune175.0ms

localize12.0ms

rewrite30.0ms

series144.0ms

simplify3.7min

prune100.0ms

regimes165.0ms

bsearch0.0ms

simplify1.0ms

end0.0ms

sample2.8s

Profiling