Quotient of products

Time bar (total: 24.2s)

analyze613.0ms (2.5%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.8%0.2%0%0%0%0
0%0%99.8%0.2%0%0%0%1
0%0%99.8%0.2%0%0%0%2
0%0%99.8%0.2%0%0%0%3
0%0%99.8%0.2%0%0%0%4
25%25%74.9%0.2%0%0%0%5
25%25%74.9%0.2%0%0%0%6
25%25%74.9%0.2%0%0%0%7
37.5%37.4%62.4%0.2%0%0%0%8
56.3%56.1%43.7%0.2%0%0%0%9
56.3%56.1%43.7%0.2%0%0%0%10
56.3%56.1%43.7%0.2%0%0%0%11
65.6%65.5%34.3%0.2%0%0%0%12
Compiler

Compiled 12 to 8 computations (33.3% saved)

sample23.1s (95.3%)

Results
2.2s8256×0valid
973.0ms8206×0valid-sollya
41.0ms50×0exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-1.3027767190091439e+163 -3.4605893204963e-185 6.268269213965368e+275 1.2352690051178037e-108)5.822518367356108e-190(5.822518367356108e-190 5.822518367356108e-190)+nan.0validexit00.291811#f
(-4.357546516082745e+152 -1.624994514888149e-197 -1.9765991139987287e-199 -1.6982071604354034e+175)2.1095249539891103e-21(2.1095249539891103e-21 2.1095249539891103e-21)+nan.0validexit00.23287000000000002#f
(1.073720945693644e+166 6.960395232857756e-290 35894741646473840.0 -7670488.7764558485)-2.7143850550257534e-147(-2.7143850550257534e-147 -2.7143850550257534e-147)+nan.0validexit00.13592300000000002#f
(1.5530472818389237e+252 -1.0906604908404645e-305 -179063869084.60587 -5.777422255956158e+301)-0.0(-0.0 -0.0)+nan.0validexit00.327307#f
(-4.1979435054761085e-127 -6.545273750325459e+183 -7.19201985713931e+119 -6.722660193249322e-115)5.682930795105491e+51(5.682930795105491e+51 5.682930795105491e+51)+nan.0validexit00.171215#f
(2.617317214827248e+41 -2.0942008698096907e-304 8.355055099437551e-93 -5.717867063005764e-68)1.1473378605640094e-103(+nan.0 +nan.0)+nan.0validexit05.0#f
(4.539248124937455e+194 -1.6094103363819995e+295 -7.708849807881155e+152 -1.0316184192584105e-284)-inf.0(-inf.0 -inf.0)+nan.0validexit00.273116#f
(-3.4083589212415997e+274 1.1185277523538645e-185 -1.7983386101770274e+131 1.1242391431832984e+80)1.8856536042043564e-122(1.8856536042043564e-122 1.8856536042043564e-122)+nan.0validexit00.142991#f
(-6.929307168485637e-105 -6.874786622043223e-81 -2.6005616758661195e+206 -3.3741497261101795e-288)5.4289710820467625e-104(5.4289710820467625e-104 5.4289710820467625e-104)+nan.0validexit00.295922#f
(-3.560434571990756e-53 -2.616335177542473e+173 -1.2667175508325409e-140 -2.0038769890538478e-125)+inf.0(+inf.0 +inf.0)+nan.0validexit00.29046099999999997#f
(-3.3835178792505724e+298 -4.28845981883674e-159 2.6659622679246012e-114 7.224272594090164e+240)7533932028832.224(+nan.0 +nan.0)+nan.0validexit05.0#f
(-5.8005263617751265e-273 4.946697588813493e-8 -5.773163576420197e+59 6.506748301257397e-129)7.638443940072067e-212(7.638443940072067e-212 7.638443940072067e-212)+nan.0validexit00.243857#f
(2.0076585441402345e-13 -1.268812417421627e+76 -3.257745128442959e-97 -1.0564060179051175e+179)-7.401833320298562e-20(-7.401833320298562e-20 -7.401833320298562e-20)+nan.0validexit00.329405#f
(-2.968556600581127e+49 13416068246.174978 1.8644137811554864e+88 -1.1952171575728254e-247)1.7872342123354777e+218(1.7872342123354777e+218 1.7872342123354777e+218)+nan.0validexit00.20410799999999998#f
(-1.482775801549807e-158 -2.9050602046233626e+299 4.027139836020804e+151 1.2938284514086335e+307)8.267176e-318(8.267176e-318 8.267176e-318)+nan.0validexit00.237703#f
(2.1678592182081286e+302 1.4051930933833821e+191 -1.86289582169636e+128 2.0719507885729466e-200)-inf.0(+nan.0 +nan.0)+nan.0validexit05.0#f
(2.405054055956383e+19 -1.0125790573767589e+56 5.143945064579287e-169 7.665924037871182e-249)-inf.0(-inf.0 -inf.0)+nan.0validexit00.28103500000000003#f
(-4.321163413507758e+99 -1.8460363831341459e+62 1.563029975906824e+169 1.7688835327464306e-182)2.885189882456976e+174(2.885189882456976e+174 2.885189882456976e+174)+nan.0validexit00.146284#f
(-1.6425357759555788e-164 1.256271890442801e+34 -2.1323280188698605e+298 -5.4316663537998653e-269)-1.7816048298938974e-160(-1.7816048298938974e-160 -1.7816048298938974e-160)+nan.0validexit00.242192#f
(-1.1521729404649909e+188 2.885402372264276e-96 -5.947347171817231e-234 -3.3318378474967656e-141)-inf.0(-inf.0 -inf.0)+nan.0validexit00.34502099999999997#f
(4.55586560859188e+32 1.1824839894625634e+82 1.8606297618638283e+306 1.0839334632307701e+102)2.6711826563192642e-294(2.6711826563192642e-294 2.6711826563192642e-294)+nan.0validexit00.142378#f
(-1.0506413648721402e-73 1.6951150388251178e-222 4.5095303606076085e+131 9.474035052023773e+116)-0.0(-0.0 -0.0)+nan.0validexit00.15118#f
(1.0645351074825966e-239 4.999481325664281e+90 -3.560632818749133e+117 6.04688538739031e+174)-0.0(-0.0 -0.0)+nan.0validexit00.27687700000000004#f
(-1.2645205082943793e-229 -1.3872318490942577e-257 -7.240162008394178e-32 3.7302969597334266e-191)-6.495061053651638e-265(-6.495061053651638e-265 -6.495061053651638e-265)+nan.0validexit00.22545900000000002#f
(-4.612885928712139e+109 -1.1029675340300085e-252 7.867369483870775e+235 1.4528593511167066e-302)4.4512534610170576e-77(4.4512534610170576e-77 4.4512534610170576e-77)+nan.0validexit00.278758#f
(-9.184503357623994e+285 -1.6759992432285994e-34 -2.3069569626254364e-304 1.1681977689625798e-207)-inf.0(-inf.0 -inf.0)+nan.0validexit00.23387200000000002#f
(-1.9792824991214042e+33 1.604216170214917e-172 2.09377595387476e+135 2.465786195671836e-84)-6.150140672629305e-191(-6.150140672629305e-191 -6.150140672629305e-191)+nan.0validexit00.137665#f
(1.6300954740746283e+219 -2.2790266915953634e-86 -5.185598692461319e-86 -1.3854968797461835e-15)-5.170803057990607e+233(-5.170803057990607e+233 -5.170803057990607e+233)+nan.0validexit00.23797200000000002#f
(-4.536111047884912e-71 -6.899403366407233e+125 3.0265782916119986e+277 -4.815012537544176e-164)-2.1475628327390735e-59(-2.1475628327390735e-59 -2.1475628327390735e-59)+nan.0validexit00.148159#f
(-2.3006949438366844e-123 6.889820368451317e-155 2.3130692228284313e+187 3.149037430687076e+84)-0.0(-0.0 -0.0)+nan.0validexit00.20921399999999998#f
(-1.8308367629770926e+96 4.415239735413748e-91 -1.572091601047663e-35 8.591607018678297e-103)5.984827845638361e+142(5.984827845638361e+142 5.984827845638361e+142)+nan.0validexit00.268872#f
(-4.881142472418995e-137 4.231362104234234e+83 4.585500429859725e+130 3.7686242596735423e+261)-0.0(-0.0 -0.0)+nan.0validexit00.316066#f
(-1.0045573678171174e+303 2.3136934101885994e+269 -4.6351404364424365e+206 1.0260072868095172e+160)4.887279882416357e+205(+nan.0 +nan.0)+nan.0validexit05.0#f
(-4.401603435634084e+150 1.8962222850833104e+168 8.947916632617553e+59 4.195041933642893e-117)-inf.0(-inf.0 -inf.0)+nan.0validexit00.297904#f
(-8.707018232876891e+241 8.473408871413832e+138 1.5257516923147307e-234 6.0544206004278374e+44)-inf.0(-inf.0 -inf.0)+nan.0validexit00.284337#f
(0.29867343054094314 -4.554216389587352e+285 3.8353148338465756e+40 2.589650385073522e-118)-inf.0(-inf.0 -inf.0)+nan.0validexit00.301355#f
(1.7937023373993904e-32 4.8459129480089994e-179 2.2031274837052077e-142 -1.1290068760765859e-38)-3.4945379972010007e-31(-3.4945379972010007e-31 -3.4945379972010007e-31)+nan.0validexit00.25112700000000004#f
(1.2731405661645887e+224 -9.605778141572085e+206 -6.009198949175199e-146 -3.7936984917657314e+216)-inf.0(-inf.0 -inf.0)+nan.0validexit00.25693299999999997#f
(2.8749114770448545e+100 -2.1406637134279834e+160 -4.6851756301499986e+54 -9.08388297350347e-299)-inf.0(-inf.0 -inf.0)+nan.0validexit00.311121#f
(5.088013485037604e+260 -1.7739631358401172e+176 5.713084342922489e-242 -1.1396949991638154e-204)+inf.0(+nan.0 +nan.0)+nan.0validexit05.0#f
(1.3900772044267745e-254 8.407045680668998e-217 7.197130892761022e-292 -8.816458969208288e+297)-0.0(+nan.0 +nan.0)+nan.0validexit05.0#f
(9.667411343399424e-37 -7.077407479958513e-104 -1.3289702468273663e-138 4352053.321842688)1.1829732737336466e-8(1.1829732737336466e-8 1.1829732737336466e-8)+nan.0validexit00.251305#f
(-5.563828333249245e+260 -6.782266822401644e+208 -6.601572877259247e+182 -7.456566394100035e+201)7.665884684409468e+84(7.665884684409468e+84 7.665884684409468e+84)+nan.0validexit00.308916#f
(1.1763773444809426e+238 2.015561578253032e+86 -2.023442110025886e-223 -2.641140038433685e-153)+inf.0(+inf.0 +inf.0)+nan.0validexit00.281411#f
(1.0649665719722055e+200 4.636584939637131e-202 -1.7718656248597215e-227 -1.3264223390081663e-31)2.1009783932706875e+256(2.1009783932706875e+256 2.1009783932706875e+256)+nan.0validexit00.288612#f
(-7.226510981669396e-259 1.3909723679916952e+217 7.322078612405577e-117 5.1196809643203934e-284)-inf.0(-inf.0 -inf.0)+nan.0validexit00.317285#f
(-1.792286041356109e+68 3.1483599296692366e-112 -8.524025663571054e-300 1.4131612522106594e-56)+inf.0(+inf.0 +inf.0)+nan.0validexit00.146176#f
(-1.6323621251794832e+251 -2.9977234473522907e+264 -2.14211134261383e-293 3.7306259557653486e-250)-inf.0(-inf.0 -inf.0)+nan.0validexit00.322594#f
(-32304.07880544994 5.352481755003207e+156 5.9975347290289356e-195 -2.4557036931689786e+255)1.1739884434940402e+100(1.1739884434940402e+100 1.1739884434940402e+100)+nan.0validexit00.23843399999999998#f
(2.1926079340995736e+226 1.119462013939959e-26 -1.1884906185325906e+231 -2.8951782945498094e+280)7.133444237776e-312(7.133444237776e-312 7.133444237776e-312)+nan.0validexit00.160376#f
Sollya timings
Total time spent in Sollya 1.0s
Bogosity

preprocess291.0ms (1.2%)

Algorithm
egg-herbie
Rules
1205×fma-define
591×div-sub
554×unsub-neg
342×times-frac
320×associate-/r*
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
045512
1143512
2419512
31300512
43246512
56593512
Stop Event
node limit
Calls
Call 1
Inputs
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2))
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2))
(/.f64 (*.f64 (neg.f64 a1) a2) (*.f64 b1 b2))
(/.f64 (*.f64 a1 (neg.f64 a2)) (*.f64 b1 b2))
(/.f64 (*.f64 a1 a2) (*.f64 (neg.f64 b1) b2))
(/.f64 (*.f64 a1 a2) (*.f64 b1 (neg.f64 b2)))
(neg.f64 (/.f64 (*.f64 (neg.f64 a1) a2) (*.f64 b1 b2)))
(neg.f64 (/.f64 (*.f64 a1 (neg.f64 a2)) (*.f64 b1 b2)))
(neg.f64 (/.f64 (*.f64 a1 a2) (*.f64 (neg.f64 b1) b2)))
(neg.f64 (/.f64 (*.f64 a1 a2) (*.f64 b1 (neg.f64 b2))))
(/.f64 (*.f64 a2 a1) (*.f64 b1 b2))
(/.f64 (*.f64 b1 a2) (*.f64 a1 b2))
(/.f64 (*.f64 b2 a2) (*.f64 b1 a1))
(/.f64 (*.f64 a1 b1) (*.f64 a2 b2))
(/.f64 (*.f64 a1 b2) (*.f64 b1 a2))
(/.f64 (*.f64 a1 a2) (*.f64 b2 b1))
Outputs
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2))
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2))
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2)))
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2))
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2))
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2))
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2)))
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2))
(/.f64 (*.f64 (neg.f64 a1) a2) (*.f64 b1 b2))
(*.f64 (neg.f64 a1) (/.f64 a2 (*.f64 b1 b2)))
(*.f64 (neg.f64 a2) (/.f64 (/.f64 a1 b2) b1))
(*.f64 (neg.f64 a1) (/.f64 (/.f64 a2 b1) b2))
(/.f64 (*.f64 a1 (neg.f64 a2)) (*.f64 b1 b2))
(*.f64 (neg.f64 a1) (/.f64 a2 (*.f64 b1 b2)))
(*.f64 (neg.f64 a2) (/.f64 (/.f64 a1 b2) b1))
(*.f64 (neg.f64 a1) (/.f64 (/.f64 a2 b1) b2))
(/.f64 (*.f64 a1 a2) (*.f64 (neg.f64 b1) b2))
(*.f64 (neg.f64 a1) (/.f64 a2 (*.f64 b1 b2)))
(*.f64 (neg.f64 a2) (/.f64 (/.f64 a1 b2) b1))
(*.f64 (neg.f64 a1) (/.f64 (/.f64 a2 b1) b2))
(/.f64 (*.f64 a1 a2) (*.f64 b1 (neg.f64 b2)))
(*.f64 (neg.f64 a1) (/.f64 a2 (*.f64 b1 b2)))
(*.f64 (neg.f64 a2) (/.f64 (/.f64 a1 b2) b1))
(*.f64 (neg.f64 a1) (/.f64 (/.f64 a2 b1) b2))
(neg.f64 (/.f64 (*.f64 (neg.f64 a1) a2) (*.f64 b1 b2)))
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2))
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2)))
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2))
(neg.f64 (/.f64 (*.f64 a1 (neg.f64 a2)) (*.f64 b1 b2)))
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2))
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2)))
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2))
(neg.f64 (/.f64 (*.f64 a1 a2) (*.f64 (neg.f64 b1) b2)))
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2))
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2)))
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2))
(neg.f64 (/.f64 (*.f64 a1 a2) (*.f64 b1 (neg.f64 b2))))
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2))
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2)))
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2))
(/.f64 (*.f64 a2 a1) (*.f64 b1 b2))
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2))
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2)))
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2))
(/.f64 (*.f64 b1 a2) (*.f64 a1 b2))
(*.f64 b1 (/.f64 a2 (*.f64 a1 b2)))
(*.f64 b1 (/.f64 (/.f64 a2 b2) a1))
(*.f64 a2 (/.f64 b1 (*.f64 a1 b2)))
(/.f64 (*.f64 b2 a2) (*.f64 b1 a1))
(*.f64 (/.f64 b2 b1) (/.f64 a2 a1))
(/.f64 (*.f64 a2 b2) (*.f64 a1 b1))
(*.f64 b2 (/.f64 a2 (*.f64 a1 b1)))
(*.f64 b2 (/.f64 (/.f64 a2 b1) a1))
(/.f64 (*.f64 a1 b1) (*.f64 a2 b2))
(*.f64 (/.f64 a1 a2) (/.f64 b1 b2))
(*.f64 a1 (/.f64 b1 (*.f64 a2 b2)))
(*.f64 b1 (/.f64 a1 (*.f64 a2 b2)))
(/.f64 (*.f64 a1 b2) (*.f64 b1 a2))
(*.f64 (/.f64 a1 b1) (/.f64 b2 a2))
(*.f64 a1 (/.f64 (/.f64 b2 b1) a2))
(*.f64 a1 (/.f64 b2 (*.f64 a2 b1)))
(/.f64 (*.f64 a1 a2) (*.f64 b2 b1))
(*.f64 (/.f64 a1 b1) (/.f64 a2 b2))
(*.f64 a1 (/.f64 a2 (*.f64 b1 b2)))
(*.f64 a1 (/.f64 (/.f64 a2 b1) b2))
Symmetry

(negabs a1)

(negabs a2)

(negabs b1)

(negabs b2)

(sort a1 a2)

(sort b1 b2)

Compiler

Compiled 11 to 7 computations (36.4% saved)

eval0.0ms (0%)

Compiler

Compiled 4 to 4 computations (0% saved)

prune3.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
84.1%
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2))
Compiler

Compiled 22 to 14 computations (36.4% saved)

simplify6.0ms (0%)

Algorithm
egg-herbie
Rules
*-commutative
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01431
11631
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2))
Outputs
(/.f64 (*.f64 a1 a2) (*.f64 b1 b2))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 11 to 7 computations (36.4% saved)

preprocess234.0ms (1%)

Remove

(sort b1 b2)

(sort a1 a2)

(negabs b2)

(negabs b1)

(negabs a2)

(negabs a1)

Compiler

Compiled 330 to 210 computations (36.4% saved)

end0.0ms (0%)

Profiling

Loading profile data...