Linear.Projection:infinitePerspective from linear-1.19.1.3, A

Time bar (total: 13.8s)

analyze736.0ms (5.3%)

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
37.5%37.4%62.4%0.2%0%0%0%9
37.5%37.4%62.4%0.2%0%0%0%10
37.5%37.4%62.4%0.2%0%0%0%11
48.4%48.3%51.5%0.2%0%0%0%12
Compiler

Compiled 16 to 11 computations (31.3% saved)

sample12.6s (91.1%)

Results
1.8s8256×0valid-rival
1.0s8194×0valid-sollya
310.0ms62×0exit-sollya
Bogosity

preprocess334.0ms (2.4%)

Algorithm
egg-herbie
Rules
523×div-sub
424×associate-/r*
362×associate-*r/
358×distribute-lft-neg-in
347×times-frac
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
060620
1204592
2534592
31938592
44993592
57203592
Stop Event
node limit
Calls
Call 1
Inputs
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z)))
(/.f64 (*.f64 (neg.f64 x) #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 (neg.f64 y) z) (*.f64 t z)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y (neg.f64 z)) (*.f64 t (neg.f64 z))))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 (neg.f64 t) z)))
(neg.f64 (/.f64 (*.f64 (neg.f64 x) #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z))))
(neg.f64 (/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 (neg.f64 y) z) (*.f64 t z))))
(neg.f64 (/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y (neg.f64 z)) (*.f64 t (neg.f64 z)))))
(neg.f64 (/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 (neg.f64 t) z))))
(/.f64 (*.f64 y #s(literal 2 binary64)) (-.f64 (*.f64 x z) (*.f64 t z)))
(/.f64 (*.f64 z #s(literal 2 binary64)) (-.f64 (*.f64 y x) (*.f64 t x)))
(/.f64 (*.f64 t #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 x z)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 z y) (*.f64 t y)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 t z) (*.f64 y z)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y t) (*.f64 z t)))
Outputs
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (*.f64 z (-.f64 y t)))
(*.f64 #s(literal 2 binary64) (/.f64 x (*.f64 z (-.f64 y t))))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (*.f64 z (-.f64 y t)))
(*.f64 #s(literal 2 binary64) (/.f64 x (*.f64 z (-.f64 y t))))
(/.f64 (*.f64 (neg.f64 x) #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z)))
(*.f64 (neg.f64 x) (/.f64 #s(literal 2 binary64) (*.f64 z (-.f64 y t))))
(/.f64 (*.f64 x #s(literal -2 binary64)) (*.f64 z (-.f64 y t)))
(*.f64 x (/.f64 #s(literal -2 binary64) (*.f64 z (-.f64 y t))))
(/.f64 (*.f64 #s(literal -2 binary64) (/.f64 x (-.f64 y t))) z)
(/.f64 (*.f64 (/.f64 x (-.f64 y t)) #s(literal -2 binary64)) z)
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 (neg.f64 y) z) (*.f64 t z)))
(*.f64 x (/.f64 #s(literal 2 binary64) (*.f64 z (-.f64 (neg.f64 y) t))))
(/.f64 (*.f64 x #s(literal -2 binary64)) (*.f64 z (+.f64 y t)))
(/.f64 (*.f64 x (/.f64 #s(literal -2 binary64) z)) (+.f64 y t))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y (neg.f64 z)) (*.f64 t (neg.f64 z))))
(*.f64 (neg.f64 x) (/.f64 #s(literal 2 binary64) (*.f64 z (-.f64 y t))))
(/.f64 (*.f64 x #s(literal -2 binary64)) (*.f64 z (-.f64 y t)))
(*.f64 x (/.f64 #s(literal -2 binary64) (*.f64 z (-.f64 y t))))
(/.f64 (*.f64 #s(literal -2 binary64) (/.f64 x (-.f64 y t))) z)
(/.f64 (*.f64 (/.f64 x (-.f64 y t)) #s(literal -2 binary64)) z)
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 (neg.f64 t) z)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (*.f64 z (-.f64 y (neg.f64 t))))
(*.f64 x (/.f64 #s(literal 2 binary64) (*.f64 z (+.f64 y t))))
(*.f64 x (/.f64 (/.f64 #s(literal 2 binary64) z) (+.f64 y t)))
(neg.f64 (/.f64 (*.f64 (neg.f64 x) #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z))))
(/.f64 (*.f64 x #s(literal 2 binary64)) (*.f64 z (-.f64 y t)))
(*.f64 #s(literal 2 binary64) (/.f64 x (*.f64 z (-.f64 y t))))
(neg.f64 (/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 (neg.f64 y) z) (*.f64 t z))))
(/.f64 (*.f64 x #s(literal 2 binary64)) (*.f64 z (-.f64 y (neg.f64 t))))
(*.f64 x (/.f64 #s(literal 2 binary64) (*.f64 z (+.f64 y t))))
(*.f64 x (/.f64 (/.f64 #s(literal 2 binary64) z) (+.f64 y t)))
(neg.f64 (/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y (neg.f64 z)) (*.f64 t (neg.f64 z)))))
(/.f64 (*.f64 x #s(literal 2 binary64)) (*.f64 z (-.f64 y t)))
(*.f64 #s(literal 2 binary64) (/.f64 x (*.f64 z (-.f64 y t))))
(neg.f64 (/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 (neg.f64 t) z))))
(*.f64 x (/.f64 #s(literal 2 binary64) (*.f64 z (-.f64 (neg.f64 y) t))))
(/.f64 (*.f64 x #s(literal -2 binary64)) (*.f64 z (+.f64 y t)))
(/.f64 (*.f64 x (/.f64 #s(literal -2 binary64) z)) (+.f64 y t))
(/.f64 (*.f64 y #s(literal 2 binary64)) (-.f64 (*.f64 x z) (*.f64 t z)))
(/.f64 (*.f64 #s(literal 2 binary64) y) (*.f64 z (-.f64 x t)))
(*.f64 y (/.f64 (/.f64 #s(literal 2 binary64) z) (-.f64 x t)))
(*.f64 (/.f64 y z) (/.f64 #s(literal 2 binary64) (-.f64 x t)))
(/.f64 (*.f64 z #s(literal 2 binary64)) (-.f64 (*.f64 y x) (*.f64 t x)))
(/.f64 (*.f64 #s(literal 2 binary64) z) (*.f64 x (-.f64 y t)))
(*.f64 z (/.f64 (/.f64 #s(literal 2 binary64) x) (-.f64 y t)))
(*.f64 #s(literal 2 binary64) (/.f64 z (*.f64 x (-.f64 y t))))
(/.f64 (*.f64 t #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 x z)))
(/.f64 (*.f64 #s(literal 2 binary64) t) (*.f64 z (-.f64 y x)))
(*.f64 #s(literal 2 binary64) (/.f64 t (*.f64 z (-.f64 y x))))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 z y) (*.f64 t y)))
(*.f64 x (/.f64 #s(literal 2 binary64) (*.f64 y (-.f64 z t))))
(*.f64 (/.f64 #s(literal 2 binary64) y) (/.f64 x (-.f64 z t)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 t z) (*.f64 y z)))
(*.f64 (neg.f64 x) (/.f64 #s(literal 2 binary64) (*.f64 z (-.f64 y t))))
(/.f64 (*.f64 x #s(literal -2 binary64)) (*.f64 z (-.f64 y t)))
(*.f64 x (/.f64 #s(literal -2 binary64) (*.f64 z (-.f64 y t))))
(/.f64 (*.f64 #s(literal -2 binary64) (/.f64 x (-.f64 y t))) z)
(/.f64 (*.f64 (/.f64 x (-.f64 y t)) #s(literal -2 binary64)) z)
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y t) (*.f64 z t)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (*.f64 t (-.f64 y z)))
(*.f64 x (/.f64 (/.f64 #s(literal 2 binary64) t) (-.f64 y z)))
(/.f64 (*.f64 #s(literal 2 binary64) (/.f64 x t)) (-.f64 y z))
Symmetry

(negabs x)

(negabs z)

Compiler

Compiled 15 to 10 computations (33.3% saved)

eval0.0ms (0%)

Compiler

Compiled 4 to 4 computations (0% saved)

prune3.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
90.1%
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z)))
Compiler

Compiled 30 to 20 computations (33.3% saved)

simplify19.0ms (0.1%)

Algorithm
egg-herbie
Rules
*-commutative
sub-neg
+-commutative
neg-sub0
neg-mul-1
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01746
12646
23846
34446
44846
54946
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z)))
Outputs
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 t z)))
(/.f64 (*.f64 x #s(literal 2 binary64)) (-.f64 (*.f64 y z) (*.f64 z t)))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 15 to 10 computations (33.3% saved)

preprocess139.0ms (1%)

Remove

(negabs z)

(negabs x)

Compiler

Compiled 298 to 166 computations (44.3% saved)

end0.0ms (0%)

Profiling

Loading profile data...