+{"flags":["precision:double","setup:simplify","reduce:regimes","reduce:taylor","reduce:simplify","reduce:avg-error","rules:arithmetic","rules:polynomials","rules:fractions","rules:exponents","rules:trigonometry","rules:hyperbolic","generate:rr","generate:taylor","generate:simplify"],"seed":"#(772101555 1905824529 294602591 2478279198 2123125427 4197813737)","points":256,"date":1493418730,"commit":"a6770931126e0702f83b80fffb3cdf362d9e07c9","branch":"develop","iterations":3,"note":false,"bit_width":64,"tests":[{"bits":1408,"start":39.78563602870575,"input":"(sqrt (/ (- (exp (* 2 x)) 1) (- (exp x) 1)))","output":"(sqrt (/ (+ (exp x) 1) 1))","link":"0-sqrtexpproblem344","ninf":0,"pinf":0,"end-est":0.0078125,"name":"sqrtexp (problem 3.4.4)","samplers":["default"],"time":53697.2470703125,"status":"imp-start","vars":["x"],"target":false,"end":0.014412722522414014},{"bits":2432,"start":31.277522201292555,"input":"(/ (- x (sin x)) (- x (tan x)))","output":"(if (<= x -9.950485992669078e-09) (- (/ x (- x (tan x))) (/ (sin x) (- x (tan x)))) (if (<= x 0.16631490308113306) (- (* 9/40 (sqr x)) (+ (* 27/2800 (pow x 4)) 1/2)) (/ (- x (sin x)) (- x (tan x)))))","link":"1-sintanproblem345","ninf":0,"pinf":0,"end-est":0.36733237039018785,"name":"sintan (problem 3.4.5)","samplers":["default"],"time":135208.11889648438,"status":"imp-start","vars":["x"],"target":false,"end":0.1040637469913252},{"bits":2432,"start":36.53944527020705,"input":"(/ (+ (- b/2) (sqrt (- (sqr b/2) (* a c)))) a)","output":"(if (<= b/2 -1.751131060884064e+136) (* -2 (/ b/2 a)) (if (<= b/2 8.548826144111727e-60) (/ 1 (/ a (+ (- b/2) (sqrt (- (sqr b/2) (* a c)))))) (- (/ (+ b/2 (- b/2)) a) (/ (* 1/2 c) b/2))))","link":"2-quad2pproblem321positive","ninf":0,"pinf":0,"end-est":8.759031935807828,"name":"quad2p (problem 3.2.1, positive)","samplers":["default","default","default"],"time":119061.97412109375,"status":"imp-start","vars":["a","b/2","c"],"target":false,"end":5.966762651991987},{"bits":2944,"start":37.82838784287472,"input":"(/ (- (- b/2) (sqrt (- (sqr b/2) (* a c)))) a)","output":"(if (<= b/2 -3.093544874321455e-77) (* (/ -1/2 b/2) c) (if (<= b/2 5.845042913155354e+61) (/ 1 (/ a (- (- b/2) (sqrt (- (sqr b/2) (* a c)))))) (+ (* (/ c b/2) 1/2) (/ (- (- b/2) b/2) a))))","link":"3-quad2mproblem321negative","ninf":0,"pinf":0,"end-est":8.241281491524308,"name":"quad2m (problem 3.2.1, negative)","samplers":["default","default","default"],"time":126471.29907226562,"status":"imp-start","vars":["a","b/2","c"],"target":false,"end":5.326392364138352},{"bits":2432,"start":31.059705602958424,"input":"(/ (- 1 (cos x)) (sqr x))","output":"(* (/ (sin x) x) (/ (/ (sin x) (+ 1 (cos x))) x))","link":"4-cos2problem341","ninf":0,"pinf":0,"end-est":0.3600447888363383,"name":"cos2 (problem 3.4.1)","samplers":["default"],"time":82701.72485351562,"status":"imp-start","vars":["x"],"target":false,"end":0.27141353358701925},{"bits":1408,"start":31.55214583076247,"input":"(- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n)))","output":"(if (<= n -2.672258838309128e-11) (- (- (/ (/ 1 x) n) (/ (/ 1/2 n) (sqr x))) (/ (log x) (* n (* n x)))) (if (<= n 19699878403.887928) (exp (cube (cbrt (log (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))))))) (- (- (/ (/ 1 x) n) (/ (/ 1/2 n) (sqr x))) (/ (log x) (* n (* n x))))))","link":"5-2nthrtproblem346","ninf":0,"pinf":0,"end-est":21.21301382692941,"name":"2nthrt (problem 3.4.6)","samplers":["default","default"],"time":143232.169921875,"status":"imp-start","vars":["x","n"],"target":false,"end":6.774720844192645},{"bits":1408,"start":40.755841804999065,"input":"(- (log (+ N 1)) (log N))","output":"(if (<= N 9328.390986348908) (log (/ (+ N 1) N)) (+ (/ (- (/ 1/3 N) 1/2) (sqr N)) (/ 1 N)))","link":"6-2logproblem336","ninf":0,"pinf":0,"end-est":0.11448705279133702,"name":"2log (problem 3.3.6)","samplers":["default"],"time":41444.029052734375,"status":"imp-start","vars":["N"],"target":false,"end":19.49352325492048},{"bits":896,"start":14.049500988425633,"input":"(- (/ 1 (+ x 1)) (/ 1 x))","output":"(if (<= x -209135036385.79047) (- (/ 1 (pow x 3)) (+ (pow x (- 2)) (/ 1 (pow x 4)))) (if (<= x 290639.63932394225) (/ (- x (+ 1 x)) (* (+ x 1) x)) (- (/ 1 (pow x 3)) (+ (pow x (- 2)) (/ 1 (pow x 4))))))","link":"7-2fracproblem331","ninf":0,"pinf":0,"end-est":0.0234375,"name":"2frac (problem 3.3.1)","samplers":["default"],"time":30894.91796875,"status":"imp-start","vars":["x"],"target":false,"end":0.014198120312590145},{"bits":2432,"start":38.890098631337246,"input":"(- (cos (+ x eps)) (cos x))","output":"(if (<= eps -3.645937152382937e+19) (- (- (* (cos x) (cos eps)) (* (sin x) (sin eps))) (cos x)) (if (<= eps 4.729663737457019e-05) (* -2 (* (sin (/ eps 2)) (sin (/ (+ (+ x eps) x) 2)))) (- (* (cos x) (cos eps)) (+ (* (sin x) (sin eps)) (cos x)))))","link":"8-2cosproblem335","ninf":0,"pinf":0,"end-est":0.6303043448114194,"name":"2cos (problem 3.3.5)","samplers":["default","default"],"time":104279.31079101562,"status":"imp-start","vars":["x","eps"],"target":false,"end":1.2578573335845715},{"bits":1408,"start":29.805220676286638,"input":"(- (pow (+ x 1) (/ 1 3)) (pow x (/ 1 3)))","output":"(/ 1 (+ (sqr (pow (+ x 1) (/ 1 3))) (+ (sqr (exp (/ (log x) 3))) (* (pow (+ x 1) (/ 1 3)) (pow x (/ 1 3))))))","link":"9-2cbrtproblem334","ninf":0,"pinf":0,"end-est":2.8592450383022707,"name":"2cbrt (problem 3.3.4)","samplers":["default"],"time":86841.42700195312,"status":"imp-start","vars":["x"],"target":false,"end":2.63051098758136},{"bits":2432,"start":30.222464775570813,"input":"(/ (- 1 (cos x)) (sin x))","output":"(* 1 (/ (sin x) (+ (cos x) 1)))","link":"10-tanhfexample34","ninf":0,"pinf":0,"end-est":0.5284202760025005,"name":"tanhf (example 3.4)","samplers":["default"],"time":51172.2109375,"status":"eq-target","vars":["x"],"target":0.000625,"end":0.4384920000497587},{"bits":2432,"start":34.16168973131298,"input":"(/ (+ (- b) (sqrt (- (sqr b) (* 4 (* a c))))) (* 2 a))","output":"(if (<= b -1.751131060884064e+136) (/ (- b) a) (if (<= b -5.335815531470738e-240) (/ 1 (/ (* 2 a) (+ (- b) (sqrt (- (sqr b) (* 4 (* a c))))))) (if (<= b 5.845042913155354e+61) (/ 1 (* (- (- b) (sqrt (- (* b b) (* (* 4 a) c)))) (/ (/ 2 4) c))) (- (/ (+ b (- b)) (+ a a)) (/ c b)))))","link":"11-quadpp42positive","ninf":0,"pinf":0,"end-est":6.078206418658915,"name":"quadp (p42, positive)","samplers":["default","default","default"],"time":124200.916015625,"status":"gt-target","vars":["a","b","c"],"target":21.51568349447677,"end":5.376176978102462},{"bits":2944,"start":34.438091592742474,"input":"(/ (- (- b) (sqrt (- (sqr b) (* 4 (* a c))))) (* 2 a))","output":"(if (<= b -2.049536640230252e+150) (/ (* (/ c 2) 4) (- (/ (+ c c) (/ b a)) (- b (- b)))) (if (<= b 3.902728914492509e-158) (* (/ 4 2) (/ c (+ (- b) (sqrt (- (* b b) (* a (* c 4))))))) (if (<= b 5.845042913155354e+61) (/ 1 (/ (* 2 a) (- (- b) (sqrt (- (sqr b) (* 4 (* a c))))))) (- (/ c b) (/ b a)))))","link":"12-quadmp42negative","ninf":0,"pinf":0,"end-est":5.090534681871955,"name":"quadm (p42, negative)","samplers":["default","default","default"],"time":127442.75390625,"status":"gt-target","vars":["a","b","c"],"target":21.537857357826326,"end":5.5027912650509085},{"bits":1408,"start":61.40424674064236,"input":"(/ (log (- 1 x)) (log (+ 1 x)))","output":"(- (+ (* 1/2 (sqr x)) (+ 1 x)))","link":"13-qlogexample310","ninf":0,"pinf":0,"end-est":0.5716777813221573,"name":"qlog (example 3.10)","samplers":["default"],"time":22658.823974609375,"status":"eq-target","vars":["x"],"target":0.4463297341631591,"end":0.008125},{"bits":1408,"start":63.323661641605746,"input":"(- (- (* (+ n 1) (log (+ n 1))) (* n (log n))) 1)","output":"(- (* (log (+ n 1)) (+ n 1)) (+ (* (log n) (- n)) 1))","link":"14-logsexample38","ninf":0,"pinf":0,"end-est":60.73435355682203,"name":"logs (example 3.8)","samplers":["default"],"time":43125.350830078125,"status":"gt-target","vars":["n"],"target":60.78763823817359,"end":0.2685},{"bits":1408,"start":59.443513693513,"input":"(log (/ (- 1 eps) (+ 1 eps)))","output":"(- (+ (* 2/3 (pow eps 3)) (+ (* 2/5 (pow eps 5)) (* 2 eps))))","link":"15-logqproblem343","ninf":0,"pinf":0,"end-est":0.13714055965779817,"name":"logq (problem 3.4.3)","samplers":["default"],"time":91070.09790039062,"status":"eq-target","vars":["eps"],"target":0.06565423716474932,"end":0.08804107935288033},{"bits":2432,"start":59.91793067942972,"input":"(- (/ 1 x) (/ 1 (tan x)))","output":"(+ (* 2/945 (pow x 5)) (+ (* 1/3 x) (* 1/45 (pow x 3))))","link":"16-invcotexample39","ninf":0,"pinf":0,"end-est":0.34765625,"name":"invcot (example 3.9)","samplers":["default"],"time":26213.670166015625,"status":"eq-target","vars":["x"],"target":0.0759660601543468,"end":0.3295731203125902},{"bits":2432,"start":61.9783442604534,"input":"(/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1)))","output":"(if (<= (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) -1.4449365230670285e-180) (+ (/ 1 b) (/ 1 a)) (if (<= (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) 2.5007607876802412e-113) (+ (/ 1 b) (/ 1 a)) (+ (/ 1 b) (/ 1 a))))","link":"17-expq3problem342","ninf":0,"pinf":0,"end-est":4.24688513434934,"name":"expq3 (problem 3.4.2)","samplers":["default","default","default"],"time":233948.95581054688,"status":"gt-target","vars":["a","b","eps"],"target":14.651067317747806,"end":0.014198120312590145},{"bits":1408,"start":45.739517733726835,"input":"(/ (exp x) (- (exp x) 1))","output":"(if (<= x -9.950485992669078e-09) (/ 1 (- 1 (exp (- x)))) (if (<= x 0.16631490308113306) (+ (/ 1 x) (+ 1/2 (* 1/12 x))) (/ 1 (- 1 (exp (- x))))))","link":"18-expq2section311","ninf":0,"pinf":0,"end-est":0.22577593043685318,"name":"expq2 (section 3.11)","samplers":["default"],"time":20018.59912109375,"status":"gt-target","vars":["x"],"target":30.12948710533904,"end":0.05791712397806687},{"bits":1408,"start":59.33343129621902,"input":"(- (exp x) 1)","output":"(+ (* (* x x) (+ 1/2 (* x 1/6))) x)","link":"19-expm1example37","ninf":0,"pinf":0,"end-est":0.3642608971118385,"name":"expm1 (example 3.7)","samplers":["default"],"time":35543.492919921875,"status":"eq-target","vars":["x"],"target":0.06436560156295071,"end":0.06598364687698317},{"bits":1408,"start":33.44360243099122,"input":"(- (exp (* a x)) 1)","output":"(if (<= (* a x) -1.6665755921255327e-09) (- (exp (* a x)) 1) (+ (* x a) (* 1/2 (* (* x a) (* x a)))))","link":"20-expaxsection35","ninf":0,"pinf":0,"end-est":0.30826629080627144,"name":"expax (section 3.5)","samplers":["default","default"],"time":31542.9580078125,"status":"gt-target","vars":["a","x"],"target":7.952127997421758,"end":0.18645915544792366},{"bits":1408,"start":33.99583817370671,"input":"(+ (- (exp x) 2) (exp (- x)))","output":"(+ (* 1/12 (pow x 4)) (+ (* 1/360 (pow x 6)) (sqr x)))","link":"21-exp2problem337","ninf":0,"pinf":0,"end-est":0.7811424888959018,"name":"exp2 (problem 3.3.7)","samplers":["default"],"time":51116.8779296875,"status":"gt-target","vars":["x"],"target":8.659910873648657,"end":0.11144644300676601},{"bits":1152,"start":9.49656829978195,"input":"(+ (- (/ 1 (+ x 1)) (/ 2 x)) (/ 1 (- x 1)))","output":"(/ (/ (- (/ 2 x) 0) (- x 1)) (+ 1 x))","link":"22-3fracproblem333","ninf":0,"pinf":0,"end-est":0.060878759768442016,"name":"3frac (problem 3.3.3)","samplers":["default"],"time":139599.76000976562,"status":"eq-target","vars":["x"],"target":0.23795078190808433,"end":0.06871936093777044},{"bits":2432,"start":36.40936010427848,"input":"(- (tan (+ x eps)) (tan x))","output":"(if (<= eps -2.4610266585566768e-113) (/ (- (sqr (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps))))) (sqr (tan x))) (+ (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (tan x))) (if (<= eps 3.1547769921923584e-35) (+ (* (sqr x) (cube eps)) (+ eps (* (cube x) (pow eps 4)))) (- (* (/ (+ (tan eps) (tan x)) (- 1 (/ (cube (* (tan eps) (sin x))) (cube (cos x))))) (+ (sqr 1) (+ (sqr (* (tan x) (tan eps))) (* 1 (* (tan x) (tan eps)))))) (tan x))))","link":"23-2tanproblem332","ninf":0,"pinf":0,"end-est":16.79675543908866,"name":"2tan (problem 3.3.2)","samplers":["default","default"],"time":153829.44311523438,"status":"gt-target","vars":["x","eps"],"target":24.868488975311955,"end":11.1570419418963},{"bits":1408,"start":29.901471078747512,"input":"(- (sqrt (+ x 1)) (sqrt x))","output":"(/ 1 (+ (sqrt (+ x 1)) (sqrt x)))","link":"24-2sqrtexample31","ninf":0,"pinf":0,"end-est":0.19988251953688405,"name":"2sqrt (example 3.1)","samplers":["default"],"time":20755.375,"status":"eq-target","vars":["x"],"target":0.16316052656439306,"end":0.16316052656439306},{"bits":2432,"start":36.71325510564527,"input":"(- (sin (+ x eps)) (sin x))","output":"(if (<= eps -3.645937152382937e+19) (- (+ (* (sin x) (cos eps)) (* (cos x) (sin eps))) (sin x)) (if (<= eps 6.326235572596747e-15) (* 2 (* (sin (/ eps 2)) (cos (/ (+ (+ x eps) x) 2)))) (- (+ (* (sin x) (cos eps)) (* (cos x) (sin eps))) (sin x))))","link":"25-2sinexample33","ninf":0,"pinf":0,"end-est":0.40463013074677723,"name":"2sin (example 3.3)","samplers":["default","default"],"time":82629.40185546875,"status":"gt-target","vars":["x","eps"],"target":14.900038199925003,"end":1.0798819096901375},{"bits":1152,"start":19.330732255826693,"input":"(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))","output":"(* (/ 1 (+ (sqrt (+ 1 x)) (sqrt x))) (/ 1 (* (sqrt x) (sqrt (+ x 1)))))","link":"26-2isqrtexample36","ninf":0,"pinf":0,"end-est":0.3721339476841681,"name":"2isqrt (example 3.6)","samplers":["default"],"time":35296.56103515625,"status":"eq-target","vars":["x"],"target":0.714170361427429,"end":0.3941741281572718},{"bits":1408,"start":14.541859386925417,"input":"(- (atan (+ N 1)) (atan N))","output":"(atan2 (+ 1 0) (+ (* (+ N 1) N) 1))","link":"27-2atanexample35","ninf":0,"pinf":0,"end-est":0.29506882110978144,"name":"2atan (example 3.5)","samplers":["default"],"time":15547.489990234375,"status":"eq-target","vars":["N"],"target":0.39299853686879893,"end":0.39174853686879885}]}
0 commit comments