0.003 * [progress]: [Phase 1 of 3] Setting up. 0.003 * * * [progress]: [1/2] Preparing points 0.003 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.004 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.031 * * * * [points]: Setting MPFR precision to 64 0.044 * * * * [points]: Setting MPFR precision to 320 0.050 * * * * [points]: Setting MPFR precision to 576 0.054 * * * * [points]: Setting MPFR precision to 832 0.058 * * * * [points]: Setting MPFR precision to 1088 0.063 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.199 * * * * [points]: Setting MPFR precision to 832 0.208 * * * * [points]: Setting MPFR precision to 1088 0.218 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.373 * * * * [points]: Setting MPFR precision to 832 0.381 * * * * [points]: Setting MPFR precision to 1088 0.389 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.503 * * * * [points]: Setting MPFR precision to 832 0.530 * * * * [points]: Setting MPFR precision to 1088 0.557 * * * * [points]: Computing exacts for 256 points 0.720 * * * * [points]: Setting MPFR precision to 832 0.822 * * * * [points]: Setting MPFR precision to 1088 0.909 * * * * [points]: Filtering points with unrepresentable outputs 0.910 * * * * [points]: Sampled 256 points with exact outputs 0.910 * * * [progress]: [2/2] Setting up program. 0.916 * [progress]: [Phase 2 of 3] Improving. 0.916 * * * * [progress]: [ 1 / 1 ] simplifiying candidate # 0.916 * [simplify]: Simplifying: (im (+.c (+.c (+.c (+.c (*.c (*.c (*.c (complex (/ (- 1) 2) (/ (sqrt 3) 2)) (complex (/ (- 1) 2) (/ (sqrt 3) 2))) (complex (/ (- 1) 2) (/ (sqrt 3) 2))) (complex (/ (- 1) 2) (/ (sqrt 3) 2))) (*.c (*.c (*.c (complex (- 2) 0) (complex (/ (- 1) 2) (/ (sqrt 3) 2))) (complex (/ (- 1) 2) (/ (sqrt 3) 2))) (complex (/ (- 1) 2) (/ (sqrt 3) 2)))) (*.c (*.c (complex 5 0) (complex (/ (- 1) 2) (/ (sqrt 3) 2))) (complex (/ (- 1) 2) (/ (sqrt 3) 2)))) (*.c (complex 4 0) (complex (/ (- 1) 2) (/ (sqrt 3) 2)))) (complex 7 0))) 0.917 * * [simplify]: iteration 1: (31 enodes) 0.928 * * [simplify]: iteration 2: (113 enodes) 1.010 * * [simplify]: iteration 3: (346 enodes) 1.216 * * [simplify]: iteration 4: (1292 enodes) 4.231 * * [simplify]: Extracting #0: cost 1 inf + 0 4.231 * * [simplify]: Extracting #1: cost 3 inf + 0 4.231 * * [simplify]: Extracting #2: cost 42 inf + 0 4.234 * * [simplify]: Extracting #3: cost 703 inf + 0 4.244 * * [simplify]: Extracting #4: cost 1092 inf + 683 4.261 * * [simplify]: Extracting #5: cost 1530 inf + 3351 4.286 * * [simplify]: Extracting #6: cost 1292 inf + 30608 4.360 * * [simplify]: Extracting #7: cost 541 inf + 185278 4.553 * * [simplify]: Extracting #8: cost 53 inf + 337335 4.718 * * [simplify]: Extracting #9: cost 0 inf + 352475 4.886 * * [simplify]: Extracting #10: cost 0 inf + 352432 5.089 * [simplify]: Simplified to: (im (+.c (complex 5 (* 2 (sqrt 3))) (complex -5 (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))))) 5.097 * * [progress]: iteration 1 / 4 5.097 * * * [progress]: picking best candidate 5.100 * * * * [pick]: Picked # 5.100 * * * [progress]: localizing error 5.169 * * * [progress]: generating rewritten candidates 5.169 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 2 2 2 2) 5.185 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2 2) 5.646 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 2 2 2) 5.768 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 2 2 2 2) 5.793 * * * [progress]: generating series expansions 5.793 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 2 2 2 2) 5.793 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2 2) 5.793 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 2 2 2) 5.794 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 2 2 2 2) 5.794 * * * [progress]: simplifying candidates 5.794 * * * * [progress]: [ 1 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 2 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 3 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 4 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 5 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 6 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 7 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 8 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 9 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 10 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 11 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 12 / 178 ] simplifiying candidate #real (real->posit16 (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))))))))> 5.794 * * * * [progress]: [ 13 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 14 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 15 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 16 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 17 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 18 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 19 / 178 ] simplifiying candidate # 5.794 * * * * [progress]: [ 20 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 21 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 22 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 23 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 24 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 25 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 26 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 27 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 28 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 29 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 30 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 31 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 32 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 33 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 34 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 35 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 36 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 37 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 38 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 39 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 40 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 41 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 42 / 178 ] simplifiying candidate # 5.795 * * * * [progress]: [ 43 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 44 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 45 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 46 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 47 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 48 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 49 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 50 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 51 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 52 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 53 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 54 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 55 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 56 / 178 ] simplifiying candidate # 5.796 * * * * [progress]: [ 57 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 58 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 59 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 60 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 61 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 62 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 63 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 64 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 65 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 66 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 67 / 178 ] simplifiying candidate # 5.797 * * * * [progress]: [ 68 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 69 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 70 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 71 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 72 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 73 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 74 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 75 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 76 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 77 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 78 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 79 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 80 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 81 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 82 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 83 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 84 / 178 ] simplifiying candidate # 5.798 * * * * [progress]: [ 85 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 86 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 87 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 88 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 89 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 90 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 91 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 92 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 93 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 94 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 95 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 96 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 97 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 98 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 99 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 100 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 101 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 102 / 178 ] simplifiying candidate #real (real->posit16 (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))))))))> 5.799 * * * * [progress]: [ 103 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 104 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 105 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 106 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 107 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 108 / 178 ] simplifiying candidate # 5.799 * * * * [progress]: [ 109 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 110 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 111 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 112 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 113 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 114 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 115 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 116 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 117 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 118 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 119 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 120 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 121 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 122 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 123 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 124 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 125 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 126 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 127 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 128 / 178 ] simplifiying candidate # 5.800 * * * * [progress]: [ 129 / 178 ] simplifiying candidate # 5.801 * * * * [progress]: [ 130 / 178 ] simplifiying candidate #real (real->posit16 (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))))))))> 5.801 * * * * [progress]: [ 131 / 178 ] simplifiying candidate # 5.801 * * * * [progress]: [ 132 / 178 ] simplifiying candidate # 5.801 * * * * [progress]: [ 133 / 178 ] simplifiying candidate # 5.801 * * * * [progress]: [ 134 / 178 ] simplifiying candidate # 5.801 * * * * [progress]: [ 135 / 178 ] simplifiying candidate # 5.801 * * * * [progress]: [ 136 / 178 ] simplifiying candidate # 5.803 * * * * [progress]: [ 137 / 178 ] simplifiying candidate # 5.803 * * * * [progress]: [ 138 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 139 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 140 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 141 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 142 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 143 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 144 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 145 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 146 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 147 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 148 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 149 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 150 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 151 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 152 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 153 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 154 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 155 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 156 / 178 ] simplifiying candidate # 5.804 * * * * [progress]: [ 157 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 158 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 159 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 160 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 161 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 162 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 163 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 164 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 165 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 166 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 167 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 168 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 169 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 170 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 171 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 172 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 173 / 178 ] simplifiying candidate #real (real->posit16 (* (/ (sqrt 3) -4) 10))))))))))> 5.805 * * * * [progress]: [ 174 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 175 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 176 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 177 / 178 ] simplifiying candidate # 5.805 * * * * [progress]: [ 178 / 178 ] simplifiying candidate # 5.809 * [simplify]: Simplifying: (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))) (log (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (cbrt (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (cbrt (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (cbrt (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (sqrt (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (sqrt (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))) (* 2 -4) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (real->posit16 (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (* (/ 1 (exp (/ (sqrt 3) -4))) (/ 1 (exp (/ (sqrt 3) -4)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))))) (* (* (/ 1 (exp (/ (sqrt 3) -4))) (/ 1 (exp (/ (sqrt 3) -4)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (/ 1 (exp (/ (sqrt 3) -4))) (/ 1 (exp (/ (sqrt 3) -4)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))))) (* (* (/ 1 (exp (/ (sqrt 3) -4))) (/ 1 (exp (/ (sqrt 3) -4)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (/ 1 (exp (/ (sqrt 3) -4))) (/ 1 (exp (/ (sqrt 3) -4)))) (exp (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (/ 1 (exp (/ (sqrt 3) -4))) (exp (- (/ (sqrt 3) -4)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))))) (* (* (/ 1 (exp (/ (sqrt 3) -4))) (exp (- (/ (sqrt 3) -4)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (/ 1 (exp (/ (sqrt 3) -4))) (exp (- (/ (sqrt 3) -4)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))))) (* (* (/ 1 (exp (/ (sqrt 3) -4))) (exp (- (/ (sqrt 3) -4)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (/ 1 (exp (/ (sqrt 3) -4))) (exp (- (/ (sqrt 3) -4)))) (exp (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (exp (- (/ (sqrt 3) -4))) (/ 1 (exp (/ (sqrt 3) -4)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))))) (* (* (exp (- (/ (sqrt 3) -4))) (/ 1 (exp (/ (sqrt 3) -4)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (exp (- (/ (sqrt 3) -4))) (/ 1 (exp (/ (sqrt 3) -4)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))))) (* (* (exp (- (/ (sqrt 3) -4))) (/ 1 (exp (/ (sqrt 3) -4)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (exp (- (/ (sqrt 3) -4))) (/ 1 (exp (/ (sqrt 3) -4)))) (exp (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (exp (- (/ (sqrt 3) -4))) (exp (- (/ (sqrt 3) -4)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))))) (* (* (exp (- (/ (sqrt 3) -4))) (exp (- (/ (sqrt 3) -4)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (exp (- (/ (sqrt 3) -4))) (exp (- (/ (sqrt 3) -4)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))))) (* (* (exp (- (/ (sqrt 3) -4))) (exp (- (/ (sqrt 3) -4)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (exp (- (/ (sqrt 3) -4))) (exp (- (/ (sqrt 3) -4)))) (exp (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (exp (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))))) (* (exp (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (exp (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10))))) (* (exp (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (exp (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (exp (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (log (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (exp (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (cbrt (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (cbrt (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (cbrt (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (sqrt (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (sqrt (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (* (* -4 -4) (* 2 -4))) (* (* -4 -4) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (* 2 -4)) (* (* -4 -4) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))))) (* (* -4 -4) (* (* -4 -4) (* 2 -4))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (* (* -4 -4) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (* -4 -4) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* -4 -4) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))))) (* (* -4 -4) (* (* -4 -4) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (* (* -4 -4) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (* -4 -4) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (* -4 -4) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))))) (* (* -4 -4) (* (* -4 -4) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (* 2 -4))) (* (* -4 -4) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (* 2 -4)) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))))) (* (* -4 -4) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (* 2 -4))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (* -4 -4) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))))) (* (* -4 -4) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (* -4 -4) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))))) (* (* -4 -4) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* 2 -4))) (* (* -4 -4) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* 2 -4)) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))))) (* (* -4 -4) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* 2 -4))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (* -4 -4) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))))) (* (* -4 -4) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (* -4 -4) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))))) (* (* -4 -4) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (+ (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (* -4 -4) (+ (pow (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) 3) (pow (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) 3)))) (* (* -4 -4) (+ (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (+ (* (- (sqrt 3)) -4) (* -4 (- (sqrt 3)))) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (* -4 -4) (- (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (* -4 -4) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (* (* -4 -4) (* 2 -4))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (* 2 -4)) (* (* -4 -4) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (* (* -4 -4) (* 2 -4))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (* (* -4 -4) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* -4 -4) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (* (* -4 -4) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (* (* -4 -4) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (* -4 -4) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (* (* -4 -4) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (* 2 -4))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (* 2 -4)) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (* 2 -4))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* 2 -4))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* 2 -4)) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* 2 -4))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (+ (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (pow (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) 3) (pow (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) 3)))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (+ (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (+ (pow (- (/ (sqrt 3) -4)) 3) (pow (- (/ (sqrt 3) -4)) 3)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (- (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (+ (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))))) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (* -4 -4) (* 2 -4))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (* 2 -4)) (* (* -4 -4) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (* -4 -4) (* 2 -4))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (* -4 -4) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* -4 -4) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (* -4 -4) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (* -4 -4) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (* -4 -4) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (* -4 -4) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (* 2 -4))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (* 2 -4)) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (* 2 -4))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* 2 -4))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* 2 -4)) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* 2 -4))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (+ (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (pow (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) 3) (pow (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) 3)))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (+ (* (- (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (* (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (* (- (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (pow (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) 3) (pow (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) 3)) (+ (* (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (- (* (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))))) (- (* (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4)))) (* (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (- (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (+ (- (/ (sqrt 3) -4)) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (- (/ (sqrt 3) -4) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (- (/ (sqrt 3) -4) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (- (- (/ (sqrt 3) -4) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (- (/ (sqrt 3) -4) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (real->posit16 (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10)))) (* (* (exp (/ (sqrt 3) -4)) (exp (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* (exp (/ (sqrt 3) 2)) (exp (* (/ (sqrt 3) -4) 10)))) (* (exp (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (exp (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (log (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (exp (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (cbrt (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (cbrt (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (cbrt (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (* (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (sqrt (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (sqrt (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (* 2 -4)) (* (* -4 -4) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))) (* (* -4 -4) (* 2 -4)) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (* -4 -4) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))) (* (* -4 -4) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (+ (* (+ (* (sqrt 3) -4) (* -4 (sqrt 3))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (* -4 -4) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))) (* (* -4 -4) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (* 2 -4)) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (* 2 -4)) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (+ (* (+ (pow (/ (sqrt 3) -4) 3) (pow (/ (sqrt 3) -4) 3)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))) (* (+ (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* 2 -4)) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (sqrt 3) -4) (* 2 (* (sqrt 3) 10))))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* 2 -4)) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (pow (/ (sqrt 3) 2) 3) (pow (* (/ (sqrt 3) -4) 10) 3)))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (- (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (+ (* (- (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (* (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (* (/ (sqrt 3) 2) (/ (sqrt 3) 2)) (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10))))) (* (- (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (- (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (pow (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) 3) (pow (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) 3)) (+ (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (- (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))) (- (* (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (* (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (/ (sqrt 3) 2)) (+ (/ (sqrt 3) -4) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))) (real->posit16 (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10)))) (* (/ (sqrt 3) -4) 10) (+ (- (log (sqrt 3)) (log -4)) (log 10)) (+ (log (/ (sqrt 3) -4)) (log 10)) (log (* (/ (sqrt 3) -4) 10)) (exp (* (/ (sqrt 3) -4) 10)) (* (/ (* (* (sqrt 3) (sqrt 3)) (sqrt 3)) (* (* -4 -4) -4)) (* (* 10 10) 10)) (* (* (* (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (/ (sqrt 3) -4)) (* (* 10 10) 10)) (* (cbrt (* (/ (sqrt 3) -4) 10)) (cbrt (* (/ (sqrt 3) -4) 10))) (cbrt (* (/ (sqrt 3) -4) 10)) (* (* (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10)) (* (/ (sqrt 3) -4) 10)) (sqrt (* (/ (sqrt 3) -4) 10)) (sqrt (* (/ (sqrt 3) -4) 10)) (* (sqrt (/ (sqrt 3) -4)) (sqrt 10)) (* (sqrt (/ (sqrt 3) -4)) (sqrt 10)) (* (/ (sqrt (sqrt 3)) (sqrt -4)) (sqrt 10)) (* (/ (sqrt (sqrt 3)) (sqrt -4)) (sqrt 10)) (* (/ (sqrt (sqrt 3)) (sqrt -4)) (sqrt 10)) (* (/ (sqrt (sqrt 3)) (sqrt -4)) (sqrt 10)) (* (/ (sqrt 3) -4) (* (cbrt 10) (cbrt 10))) (* (/ (sqrt 3) -4) (sqrt 10)) (* (/ (sqrt 3) -4) 1) (* (cbrt (/ (sqrt 3) -4)) 10) (* (sqrt (/ (sqrt 3) -4)) 10) (* (/ (cbrt (sqrt 3)) (cbrt -4)) 10) (* (/ (cbrt (sqrt 3)) (sqrt -4)) 10) (* (/ (cbrt (sqrt 3)) -4) 10) (* (/ (sqrt (cbrt 3)) (cbrt -4)) 10) (* (/ (sqrt (cbrt 3)) (sqrt -4)) 10) (* (/ (sqrt (cbrt 3)) -4) 10) (* (/ (sqrt (sqrt 3)) (cbrt -4)) 10) (* (/ (sqrt (sqrt 3)) (sqrt -4)) 10) (* (/ (sqrt (sqrt 3)) -4) 10) (* (/ (sqrt 3) (cbrt -4)) 10) (* (/ (sqrt 3) (sqrt -4)) 10) (* (/ (sqrt 3) -4) 10) (* (/ (sqrt (sqrt 3)) (cbrt -4)) 10) (* (/ (sqrt (sqrt 3)) (sqrt -4)) 10) (* (/ (sqrt (sqrt 3)) -4) 10) (* (/ (sqrt 3) (cbrt -4)) 10) (* (/ (sqrt 3) (sqrt -4)) 10) (* (/ (sqrt 3) -4) 10) (* (/ (sqrt 3) -4) 10) (* (/ 1 -4) 10) (* (sqrt 3) 10) (real->posit16 (* (/ (sqrt 3) -4) 10)) (im (+.c (complex 5 (* 2 (sqrt 3))) (complex -5 (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))))) (im (+.c (complex 5 (* 2 (sqrt 3))) (complex -5 (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))))) (im (+.c (complex 5 (* 2 (sqrt 3))) (complex -5 (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))))) (im (+.c (complex 5 (* 2 (sqrt 3))) (complex -5 (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))))) 5.816 * * [simplify]: iteration 1: (379 enodes) 6.063 * * [simplify]: iteration 2: (1937 enodes) 13.394 * * [simplify]: Extracting #0: cost 114 inf + 0 13.396 * * [simplify]: Extracting #1: cost 739 inf + 9 13.402 * * [simplify]: Extracting #2: cost 1704 inf + 1652 13.412 * * [simplify]: Extracting #3: cost 1553 inf + 24456 13.450 * * [simplify]: Extracting #4: cost 874 inf + 152465 13.516 * * [simplify]: Extracting #5: cost 220 inf + 343031 13.638 * * [simplify]: Extracting #6: cost 9 inf + 422712 13.784 * * [simplify]: Extracting #7: cost 0 inf + 423091 13.934 * * [simplify]: Extracting #8: cost 0 inf + 422595 14.088 * [simplify]: Simplified to: (exp (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (log (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (exp (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (* (cbrt (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (cbrt (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)))) (cbrt (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (* (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (+ (+ -15/4 3/4) (+ -15/4 75/4))) (sqrt (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (sqrt (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (+ (* (sqrt 3) 20) (* -4 (sqrt 3))) -8 (+ (* (/ (sqrt 3) -4) 375/2) (/ (* 3 (sqrt 3)) 8)) 93/4 (+ 3/4 -75/4) (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (real->posit16 (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (log (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (* (cbrt (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (cbrt (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))))) (cbrt (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (* (* (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (sqrt (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (sqrt (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (+ (+ (* -128 (- (* (sqrt 3) -8))) (* -128 (* (sqrt 3) -8))) (* (+ (* (sqrt 3) 20) (* -4 (sqrt 3))) 256)) -2048 (+ (* (+ (* 12 (/ (sqrt 3) 2)) (+ (* 300 (/ (sqrt 3) -2/5)) (* 93/4 (* (sqrt 3) -8)))) 16) (* (* (- (* (sqrt 3) -8)) 93/4) 16)) 5952 (+ (* (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (* 16 (- (* (sqrt 3) -8)))) (* (+ (+ 12 (* -75/4 16)) (* (* (sqrt 3) -8) (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)))) 16)) (* 256 (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (+ (* (+ (* -3/64 (sqrt 3)) (* -3/64 (sqrt 3))) -128) (+ (* (+ (* (sqrt 3) 20) (* -4 (sqrt 3))) 3) (* -3/2 (- (* (sqrt 3) -8))))) -24 (+ (+ (* (* 3/16 93/4) (- (* (sqrt 3) -8))) (* (* 16 (+ (* -3/64 (sqrt 3)) (* -3/64 (sqrt 3)))) 93/4)) (* 3 (+ (* (/ (sqrt 3) -4) 375/2) (/ (* 3 (sqrt 3)) 8)))) (* 3 93/4) (+ (* 3/16 (* (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (* (sqrt 3) -8)))) (* (+ (* (+ (* -3/64 (sqrt 3)) (* -3/64 (sqrt 3))) (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (+ 9/64 -225/64)) 16)) (* (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) 3) 0 0 0 0 0 0 (+ (* 16 (+ (* (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (+ (+ -15/4 3/4) (+ -15/4 75/4))) (+ (* 3/4 (/ (sqrt 3) -4)) (* 3/4 (/ (sqrt 3) -4))))) (* (+ (+ (+ -15/4 3/4) (+ (+ -15/4 3/4) (+ -15/4 75/4))) 3/4) (- (* (sqrt 3) -8)))) (* (+ (+ (+ -15/4 3/4) (+ (+ -15/4 3/4) (+ -15/4 75/4))) 3/4) 16) (+ (* (- 3/4 (+ (+ -15/4 3/4) (+ -15/4 75/4))) 16) (* (- (* (sqrt 3) -8)) (+ (/ (sqrt 3) -4) (- (/ (sqrt 3) -4) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)))))) (* (+ (/ (sqrt 3) -4) (- (/ (sqrt 3) -4) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)))) 16) (+ (* (+ (- (* -3/64 (sqrt 3))) (- (* -3/64 (sqrt 3)))) -128) (+ (* -3/2 (* (sqrt 3) -8)) (* (+ (* (sqrt 3) 20) (* -4 (sqrt 3))) 3))) -24 (+ (* 3/16 (+ (* 12 (/ (sqrt 3) 2)) (+ (* 300 (/ (sqrt 3) -2/5)) (* 93/4 (* (sqrt 3) -8))))) (+ (* (+ 12 360) (- (* -3/64 (sqrt 3)))) (* (+ 12 360) (- (* -3/64 (sqrt 3)))))) (* 3 93/4) (+ (+ (* 16 (* (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (+ (- (* -3/64 (sqrt 3))) (- (* -3/64 (sqrt 3)))))) (* (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (* (* (sqrt 3) -8) 3/16))) (* 3 (+ 3/4 -75/4))) (* (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) 3) (+ (* (+ (* -3/64 (sqrt 3)) (* -3/64 (sqrt 3))) -3/2) (+ (* (+ (* (sqrt 3) 20) (* -4 (sqrt 3))) 9/256) (* -3/2 (+ (- (* -3/64 (sqrt 3))) (- (* -3/64 (sqrt 3))))))) (* -3/2 3/16) (+ (+ (* (+ (- (/ (* 3 (sqrt 3)) -64)) (- (/ (* 3 (sqrt 3)) -64))) (* 3/16 93/4)) (* (+ (/ (* 3 (sqrt 3)) -64) (/ (* 3 (sqrt 3)) -64)) (* 3/16 93/4))) (* (+ (* (/ (sqrt 3) -4) 375/2) (/ (* 3 (sqrt 3)) 8)) 9/256)) (+ 27/1024 405/512) (+ (* (+ (* (+ (* -3/64 (sqrt 3)) (* -3/64 (sqrt 3))) (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (+ 9/64 -225/64)) 3/16) (+ (* (* 3/16 (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (- (* -3/64 (sqrt 3)))) (* (* 3/16 (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (- (* -3/64 (sqrt 3)))))) (* 9/256 (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) 0 0 0 0 0 0 (+ (+ (* (- (* -3/64 (sqrt 3))) (+ (+ (+ -15/4 3/4) (+ (+ -15/4 3/4) (+ -15/4 75/4))) 3/4)) (* (- (* -3/64 (sqrt 3))) (+ (+ (+ -15/4 3/4) (+ (+ -15/4 3/4) (+ -15/4 75/4))) 3/4))) (* 3/16 (+ (* (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (+ (+ -15/4 3/4) (+ -15/4 75/4))) (+ (* 3/4 (/ (sqrt 3) -4)) (* 3/4 (/ (sqrt 3) -4)))))) (* 3/16 (+ (+ (+ -15/4 3/4) (+ (+ -15/4 3/4) (+ -15/4 75/4))) 3/4)) (+ (* 3/16 (- 3/4 (+ (+ -15/4 3/4) (+ -15/4 75/4)))) (* (+ (/ (sqrt 3) -4) (- (/ (sqrt 3) -4) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)))) (+ (- (* -3/64 (sqrt 3))) (- (* -3/64 (sqrt 3)))))) (* 3/16 (+ (/ (sqrt 3) -4) (- (/ (sqrt 3) -4) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))))) 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 (+ (pow (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4)) 3) (* (+ (/ (- (sqrt 3)) -4) (/ (- (sqrt 3)) -4)) 3/4)) (+ (+ (+ 3/4 (+ 15/4 -3/4)) (- (+ (+ (+ -15/4 3/4) (+ -15/4 75/4)) (+ 15/4 -3/4)) (+ (+ -15/4 3/4) (- 3/4)))) 3/4) (- (- 3/4 (+ 3/4 (+ 15/4 -3/4))) (+ (+ (+ -15/4 3/4) (+ -15/4 75/4)) (+ 15/4 -3/4))) (- (+ (+ (/ (- (sqrt 3)) -4) (/ (- (sqrt 3)) -4)) (+ (/ (- (sqrt 3)) -4) (/ (- (sqrt 3)) -4))) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (+ (+ (+ (/ (- (sqrt 3)) -4) (/ (sqrt 3) -4)) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (- (/ (sqrt 3) -4) (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (- (/ (sqrt 3) -4) (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (- (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (- (/ (sqrt 3) -4) (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (real->posit16 (+ (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))))) (exp (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (exp (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (exp (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (exp (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (log (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (exp (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (* (cbrt (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (cbrt (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4)))) (cbrt (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (pow (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4)) 3) (sqrt (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (sqrt (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (+ (+ (* -8 (* (sqrt 3) -8)) (* (sqrt 3) -64)) (* (* (sqrt 3) 20) 16)) -128 (+ (* 12 (/ (sqrt 3) 2)) (+ (* 300 (/ (sqrt 3) -2/5)) (* 93/4 (* (sqrt 3) -8)))) (+ 12 360) (+ (+ 12 (* -75/4 16)) (* (* (sqrt 3) -8) (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)))) (* 16 (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (+ (* (sqrt 3) -3/4) (+ (* (* 2 (sqrt 3)) 15/8) (* (+ (* -3/64 (sqrt 3)) (* -3/64 (sqrt 3))) -8))) -3/2 (+ (* 3/16 (+ (* (/ (sqrt 3) -4) 375/2) (/ (* 3 (sqrt 3)) 8))) (* (+ (/ (* 3 (sqrt 3)) -64) (/ (* 3 (sqrt 3)) -64)) 93/4)) (* 3/16 93/4) (+ (* (+ (* -3/64 (sqrt 3)) (* -3/64 (sqrt 3))) (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (+ 9/64 -225/64)) (* 3/16 (- (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) 0 0 0 0 0 0 (+ (* (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)) (+ (+ -15/4 3/4) (+ -15/4 75/4))) (+ (* 3/4 (/ (sqrt 3) -4)) (* 3/4 (/ (sqrt 3) -4)))) (+ (+ (+ -15/4 3/4) (+ (+ -15/4 3/4) (+ -15/4 75/4))) 3/4) (- 3/4 (+ (+ -15/4 3/4) (+ -15/4 75/4))) (+ (/ (sqrt 3) -4) (- (/ (sqrt 3) -4) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5)))) (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4)) (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4))) (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (real->posit16 (+ (+ (/ (sqrt 3) 2) (+ (/ (sqrt 3) -2/5) (/ (sqrt 3) -4))) (/ (sqrt 3) -4))) (/ (sqrt 3) -2/5) (log (/ (sqrt 3) -2/5)) (log (/ (sqrt 3) -2/5)) (log (/ (sqrt 3) -2/5)) (exp (/ (sqrt 3) -2/5)) (* (/ (sqrt 3) -4) 375/2) (* (/ (sqrt 3) -4) 375/2) (* (cbrt (/ (sqrt 3) -2/5)) (cbrt (/ (sqrt 3) -2/5))) (cbrt (/ (sqrt 3) -2/5)) (* (/ (sqrt 3) -4) 375/2) (sqrt (/ (sqrt 3) -2/5)) (sqrt (/ (sqrt 3) -2/5)) (* (sqrt (/ (sqrt 3) -4)) (sqrt 10)) (* (sqrt (/ (sqrt 3) -4)) (sqrt 10)) (/ (* (sqrt 10) (sqrt (sqrt 3))) (sqrt -4)) (/ (* (sqrt 10) (sqrt (sqrt 3))) (sqrt -4)) (/ (* (sqrt 10) (sqrt (sqrt 3))) (sqrt -4)) (/ (* (sqrt 10) (sqrt (sqrt 3))) (sqrt -4)) (/ (* (sqrt 3) (* (cbrt 10) (cbrt 10))) -4) (/ (sqrt 3) (/ -4 (sqrt 10))) (/ (sqrt 3) -4) (* 10 (cbrt (/ (sqrt 3) -4))) (* (sqrt (/ (sqrt 3) -4)) 10) (/ (cbrt (sqrt 3)) (/ (cbrt -4) 10)) (/ (cbrt (sqrt 3)) (/ (sqrt -4) 10)) (/ (cbrt (sqrt 3)) -2/5) (/ (sqrt (cbrt 3)) (/ (cbrt -4) 10)) (* (/ (sqrt (cbrt 3)) (sqrt -4)) 10) (/ (sqrt (cbrt 3)) -2/5) (* 10 (/ (sqrt (sqrt 3)) (cbrt -4))) (* 10 (/ (sqrt (sqrt 3)) (sqrt -4))) (/ (sqrt (sqrt 3)) -2/5) (/ (sqrt 3) (/ (cbrt -4) 10)) (/ 10 (/ (sqrt -4) (sqrt 3))) (/ (sqrt 3) -2/5) (* 10 (/ (sqrt (sqrt 3)) (cbrt -4))) (* 10 (/ (sqrt (sqrt 3)) (sqrt -4))) (/ (sqrt (sqrt 3)) -2/5) (/ (sqrt 3) (/ (cbrt -4) 10)) (/ 10 (/ (sqrt -4) (sqrt 3))) (/ (sqrt 3) -2/5) (/ (sqrt 3) -2/5) -5/2 (* (sqrt 3) 10) (real->posit16 (/ (sqrt 3) -2/5)) (+ (+ (* 2 (sqrt 3)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (+ (+ (* 2 (sqrt 3)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (+ (+ (* 2 (sqrt 3)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) (+ (+ (* 2 (sqrt 3)) (- (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)))) (+ (/ (sqrt 3) 2) (/ (sqrt 3) -2/5))) 14.144 * * * [progress]: adding candidates to table 15.655 * [progress]: [Phase 3 of 3] Extracting. 15.658 * [simplify]: Simplifying: (im (+.c (complex 5 (* 2 (sqrt 3))) (complex -5 (+ (+ (- (/ (sqrt 3) -4)) (- (/ (sqrt 3) -4))) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (/ (sqrt 3) 2) (* (/ (sqrt 3) -4) 10))))))) 15.659 * * [simplify]: iteration 1: (21 enodes) 15.660 * * [simplify]: iteration 2: (30 enodes) 15.661 * * [simplify]: Extracting #0: cost 1 inf + 0 15.661 * * [simplify]: Extracting #1: cost 2 inf + 0 15.661 * * [simplify]: Extracting #2: cost 4 inf + 0 15.661 * * [simplify]: Extracting #3: cost 8 inf + 0 15.661 * * [simplify]: Extracting #4: cost 10 inf + 2 15.661 * * [simplify]: Extracting #5: cost 13 inf + 3 15.662 * * [simplify]: Extracting #6: cost 16 inf + 45 15.662 * * [simplify]: Extracting #7: cost 11 inf + 496 15.662 * * [simplify]: Extracting #8: cost 7 inf + 863 15.662 * * [simplify]: Extracting #9: cost 5 inf + 1190 15.662 * * [simplify]: Extracting #10: cost 4 inf + 1474 15.663 * * [simplify]: Extracting #11: cost 2 inf + 2363 15.663 * * [simplify]: Extracting #12: cost 0 inf + 3495 15.664 * [simplify]: Simplified to: (im (+.c (complex -5 (+ (+ (/ (- (sqrt 3)) -4) (/ (- (sqrt 3)) -4)) (+ (+ (/ (sqrt 3) -4) (/ (sqrt 3) -4)) (+ (* 10 (/ (sqrt 3) -4)) (/ (sqrt 3) 2))))) (complex 5 (* (sqrt 3) 2)))) 15.664 * * * * [points]: Sampling 8000 additional inputs, on iter 0 have 0 / 8000 15.668 * * * * [points]: Computing exacts on every 500 of 8000 points to ramp up precision 15.787 * * * * [points]: Setting MPFR precision to 832 15.792 * * * * [points]: Setting MPFR precision to 1088 15.796 * * * * [points]: Computing exacts on every 250 of 8000 points to ramp up precision 16.317 * * * * [points]: Setting MPFR precision to 832 16.322 * * * * [points]: Setting MPFR precision to 1088 16.327 * * * * [points]: Computing exacts on every 125 of 8000 points to ramp up precision 16.510 * * * * [points]: Setting MPFR precision to 832 16.520 * * * * [points]: Setting MPFR precision to 1088 16.529 * * * * [points]: Computing exacts on every 62 of 8000 points to ramp up precision 16.662 * * * * [points]: Setting MPFR precision to 832 16.681 * * * * [points]: Setting MPFR precision to 1088 16.703 * * * * [points]: Computing exacts on every 31 of 8000 points to ramp up precision 16.892 * * * * [points]: Setting MPFR precision to 832 16.981 * * * * [points]: Setting MPFR precision to 1088 17.056 * * * * [points]: Computing exacts on every 15 of 8000 points to ramp up precision 17.238 * * * * [points]: Setting MPFR precision to 832 17.441 * * * * [points]: Setting MPFR precision to 1088 17.670 * * * * [points]: Computing exacts on every 7 of 8000 points to ramp up precision 17.806 * * * * [points]: Setting MPFR precision to 832 18.068 * * * * [points]: Setting MPFR precision to 1088 18.650 * * * * [points]: Computing exacts on every 3 of 8000 points to ramp up precision 18.781 * * * * [points]: Setting MPFR precision to 832 19.419 * * * * [points]: Setting MPFR precision to 1088 20.299 * * * * [points]: Computing exacts for 8000 points 20.828 * * * * [points]: Setting MPFR precision to 832 23.886 * * * * [points]: Setting MPFR precision to 1088 27.796 * * * * [points]: Filtering points with unrepresentable outputs 27.799 * * * * [points]: Sampled 8000 points with exact outputs 27.960 * [regime-testing]: Baseline error score: 0 27.964 * [regime-testing]: Oracle error score: 0 27.964 * [regime-testing]: End program error score: 0