Linear.Projection:infinitePerspective from linear-1.19.1.3, A

Time bar (total: 8.7s)

analyze696.0ms (8%)

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)

sample7.7s (88.9%)

Results
968.0ms8254×0valid-sollya
2.2s8254×0valid-rival
Bogosity

preprocess165.0ms (1.9%)

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)

prune2.0ms (0%)

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

Compiled 30 to 20 computations (33.3% saved)

simplify4.0ms (0%)

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)

preprocess99.0ms (1.1%)

Remove

(negabs z)

(negabs x)

Compiler

Compiled 298 to 166 computations (44.3% saved)

end0.0ms (0%)

Profiling

Loading profile data...