(declare-fun afn ((_ FloatingPoint 11 53)) (_ FloatingPoint 11 53)) (declare-fun reassoc ((_ FloatingPoint 11 53)) (_ FloatingPoint 11 53)) (declare-fun contract ((_ FloatingPoint 11 53)) (_ FloatingPoint 11 53)) (declare-fun arcp ((_ FloatingPoint 11 53)) (_ FloatingPoint 11 53)) (declare-fun %x () (_ FloatingPoint 11 53)) (declare-fun anyzero!12 () Bool) (declare-fun %y () (_ FloatingPoint 11 53)) (declare-fun anyzero!9 () Bool) (declare-fun anyzero!11 () Bool) (assert (let ((a!1 (fp.mul roundNearestTiesToEven (ite (fp.isZero %y) (fp.neg %y) %y) (ite (fp.isZero %x) (fp.neg %x) %x))) (a!8 (fp.sqrt roundNearestTiesToEven (ite (and anyzero!9 (fp.isZero %y)) (fp.neg %y) %y))) (a!10 (reassoc (contract (arcp (fp.abs %x))))) (a!14 (fp.isNaN (fp.mul roundNearestTiesToEven %y (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!15 (fp.isInfinite (fp.mul roundNearestTiesToEven %y (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!16 (arcp (fp.mul roundNearestTiesToEven %y (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!31 (fp.isNaN (fp.mul roundNearestTiesToEven (ite (fp.isZero %y) (fp.neg %y) %y) %x))) (a!32 (fp.isInfinite (fp.mul roundNearestTiesToEven (ite (fp.isZero %y) (fp.neg %y) %y) %x))) (a!33 (arcp (fp.mul roundNearestTiesToEven (ite (fp.isZero %y) (fp.neg %y) %y) %x))) (a!48 (reassoc (contract (arcp (fp.mul roundNearestTiesToEven %y %x)))))) (let ((a!2 (afn (reassoc (contract (arcp a!1))))) (a!9 (afn (reassoc (contract (arcp a!8))))) (a!11 (ite (and anyzero!12 (fp.isZero (afn a!10))) (fp.neg (afn a!10)) (afn a!10))) (a!17 (fp.isNaN (afn (reassoc (contract a!16))))) (a!18 (fp.isZero (afn (reassoc (contract a!16))))) (a!19 (fp.neg (afn (reassoc (contract a!16))))) (a!22 (fp.isInfinite (afn (reassoc (contract a!16))))) (a!34 (fp.isNaN (afn (reassoc (contract a!33))))) (a!35 (fp.isZero (afn (reassoc (contract a!33))))) (a!36 (fp.neg (afn (reassoc (contract a!33))))) (a!39 (fp.isInfinite (afn (reassoc (contract a!33))))) (a!49 (fp.mul roundNearestTiesToEven (ite (fp.isZero (afn a!48)) (fp.neg (afn a!48)) (afn a!48)) (ite (fp.isZero %x) (fp.neg %x) %x))) (a!63 (fp.mul roundNearestTiesToEven (afn (reassoc (contract a!16))) (ite (fp.isZero %x) (fp.neg %x) %x))) (a!68 (fp.mul roundNearestTiesToEven (afn (reassoc (contract a!33))) (ite (fp.isZero %x) (fp.neg %x) %x))) (a!73 (fp.mul roundNearestTiesToEven (afn a!48) (ite (fp.isZero %x) (fp.neg %x) %x))) (a!93 (fp.mul roundNearestTiesToEven (ite (fp.isZero (afn a!48)) (fp.neg (afn a!48)) (afn a!48)) %x)) (a!101 (fp.mul roundNearestTiesToEven (afn (reassoc (contract a!16))) %x)) (a!106 (fp.mul roundNearestTiesToEven (afn (reassoc (contract a!33))) %x)) (a!111 (not (fp.isNaN (fp.mul roundNearestTiesToEven (afn a!48) %x)))) (a!112 (not (fp.isInfinite (fp.mul roundNearestTiesToEven (afn a!48) %x)))) (a!113 (contract (arcp (fp.mul roundNearestTiesToEven (afn a!48) %x))))) (let ((a!3 (fp.mul roundNearestTiesToEven (ite (fp.isZero a!2) (fp.neg a!2) a!2) (ite (fp.isZero %x) (fp.neg %x) %x))) (a!12 (fp.mul roundNearestTiesToEven (ite (and anyzero!11 (fp.isZero a!9)) (fp.neg a!9) a!9) a!11)) (a!20 (ite a!18 a!19 (afn (reassoc (contract a!16))))) (a!37 (ite a!35 a!36 (afn (reassoc (contract a!33))))) (a!50 (afn (reassoc (contract (arcp a!49))))) (a!54 (fp.isNaN (fp.mul roundNearestTiesToEven a!2 (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!55 (fp.isInfinite (fp.mul roundNearestTiesToEven a!2 (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!56 (arcp (fp.mul roundNearestTiesToEven a!2 (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!64 (afn (reassoc (contract (arcp a!63))))) (a!69 (afn (reassoc (contract (arcp a!68))))) (a!74 (afn (reassoc (contract (arcp a!73))))) (a!78 (fp.isNaN (fp.mul roundNearestTiesToEven (ite (fp.isZero a!2) (fp.neg a!2) a!2) %x))) (a!79 (fp.isInfinite (fp.mul roundNearestTiesToEven (ite (fp.isZero a!2) (fp.neg a!2) a!2) %x))) (a!80 (arcp (fp.mul roundNearestTiesToEven (ite (fp.isZero a!2) (fp.neg a!2) a!2) %x))) (a!94 (afn (reassoc (contract (arcp a!93))))) (a!98 (reassoc (contract (arcp (fp.mul roundNearestTiesToEven a!2 %x))))) (a!102 (afn (reassoc (contract (arcp a!101))))) (a!107 (afn (reassoc (contract (arcp a!106))))) (a!114 (not (fp.isNaN (afn (reassoc a!113))))) (a!115 (ite (fp.isZero (afn (reassoc a!113))) (fp.neg (afn (reassoc a!113))) (afn (reassoc a!113)))) (a!116 (not (fp.isInfinite (afn (reassoc a!113))))) (a!143 (fp.isNaN (fp.sqrt roundNearestTiesToEven (afn (reassoc a!113))))) (a!144 (fp.isInfinite (fp.sqrt roundNearestTiesToEven (afn (reassoc a!113)))))) (let ((a!4 (afn (reassoc (contract (arcp a!3))))) (a!13 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isNaN a!8)) (not (fp.isInfinite a!8)) (not (fp.isNaN a!9)) (not (fp.isNaN (afn a!10))) (not (fp.isNaN a!12)) (not (fp.isInfinite a!9)) (not (fp.isInfinite (afn a!10))) (not (fp.isInfinite a!12)))) (a!21 (fp.isNaN (fp.mul roundNearestTiesToEven a!20 (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!23 (fp.isInfinite (fp.mul roundNearestTiesToEven a!20 (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!24 (arcp (fp.mul roundNearestTiesToEven a!20 (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!38 (fp.isNaN (fp.mul roundNearestTiesToEven a!37 (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!40 (fp.isInfinite (fp.mul roundNearestTiesToEven a!37 (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!41 (arcp (fp.mul roundNearestTiesToEven a!37 (ite (fp.isZero %x) (fp.neg %x) %x)))) (a!51 (fp.isNaN (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!50) (fp.neg a!50) a!50)))) (a!52 (fp.isInfinite (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!50) (fp.neg a!50) a!50)))) (a!57 (fp.isNaN (afn (reassoc (contract a!56))))) (a!58 (fp.isZero (afn (reassoc (contract a!56))))) (a!59 (fp.neg (afn (reassoc (contract a!56))))) (a!61 (fp.isInfinite (afn (reassoc (contract a!56))))) (a!65 (fp.isNaN (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!64) (fp.neg a!64) a!64)))) (a!66 (fp.isInfinite (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!64) (fp.neg a!64) a!64)))) (a!70 (fp.isNaN (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!69) (fp.neg a!69) a!69)))) (a!71 (fp.isInfinite (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!69) (fp.neg a!69) a!69)))) (a!75 (fp.isNaN (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!74) (fp.neg a!74) a!74)))) (a!76 (fp.isInfinite (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!74) (fp.neg a!74) a!74)))) (a!81 (fp.isNaN (afn (reassoc (contract a!80))))) (a!82 (fp.isZero (afn (reassoc (contract a!80))))) (a!83 (fp.neg (afn (reassoc (contract a!80))))) (a!85 (fp.isInfinite (afn (reassoc (contract a!80))))) (a!87 (reassoc (contract (arcp (fp.mul roundNearestTiesToEven a!20 %x))))) (a!90 (reassoc (contract (arcp (fp.mul roundNearestTiesToEven a!37 %x))))) (a!95 (fp.isNaN (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!94) (fp.neg a!94) a!94)))) (a!96 (fp.isInfinite (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!94) (fp.neg a!94) a!94)))) (a!99 (fp.sqrt roundNearestTiesToEven (ite (fp.isZero (afn a!98)) (fp.neg (afn a!98)) (afn a!98)))) (a!103 (fp.isNaN (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!102) (fp.neg a!102) a!102)))) (a!104 (fp.isInfinite (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!102) (fp.neg a!102) a!102)))) (a!108 (fp.isNaN (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!107) (fp.neg a!107) a!107)))) (a!109 (fp.isInfinite (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!107) (fp.neg a!107) a!107)))) (a!117 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isNaN (afn a!48))) a!111 (not (fp.isInfinite (afn a!48))) a!112 a!114 (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!115))) a!116 (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!115))))) (a!123 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isNaN (afn a!48))) (not (fp.isNaN a!49)) (not (fp.isInfinite (afn a!48))) (not (fp.isInfinite a!49)) (not (fp.isNaN a!50)) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!50))) (not (fp.isInfinite a!50)) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!50))))) (a!124 (fp.sqrt roundNearestTiesToEven (afn (reassoc (contract a!56))))) (a!126 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!14) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!15) (not a!17) (not (fp.isNaN a!63)) (not a!22) (not (fp.isInfinite a!63)) (not (fp.isNaN a!64)) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!64))) (not (fp.isInfinite a!64)) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!64))))) (a!127 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!31) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!32) (not a!34) (not (fp.isNaN a!68)) (not a!39) (not (fp.isInfinite a!68)) (not (fp.isNaN a!69)) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!69))) (not (fp.isInfinite a!69)) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!69))))) (a!128 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isNaN (afn a!48))) (not (fp.isNaN a!73)) (not (fp.isInfinite (afn a!48))) (not (fp.isInfinite a!73)) (not (fp.isNaN a!74)) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!74))) (not (fp.isInfinite a!74)) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!74))))) (a!129 (fp.sqrt roundNearestTiesToEven (afn (reassoc (contract a!80))))) (a!137 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isNaN (afn a!48))) (not (fp.isNaN a!93)) (not (fp.isInfinite (afn a!48))) (not (fp.isInfinite a!93)) (not (fp.isNaN a!94)) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!94))) (not (fp.isInfinite a!94)) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!94))))) (a!138 (not (fp.isNaN (fp.sqrt roundNearestTiesToEven (afn a!98))))) (a!139 (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven (afn a!98))))) (a!141 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!14) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!15) (not a!17) (not (fp.isNaN a!101)) (not a!22) (not (fp.isInfinite a!101)) (not (fp.isNaN a!102)) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!102))) (not (fp.isInfinite a!102)) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!102))))) (a!142 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!31) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!32) (not a!34) (not (fp.isNaN a!106)) (not a!39) (not (fp.isInfinite a!106)) (not (fp.isNaN a!107)) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!107))) (not (fp.isInfinite a!107)) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!107))))) (a!145 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isNaN (afn a!48))) a!111 (not (fp.isInfinite (afn a!48))) a!112 a!114 (not a!143) a!116 (not a!144)))) (let ((a!5 (fp.isNaN (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!4) (fp.neg a!4) a!4)))) (a!6 (fp.isInfinite (fp.sqrt roundNearestTiesToEven (ite (fp.isZero a!4) (fp.neg a!4) a!4)))) (a!25 (fp.isNaN (afn (reassoc (contract a!24))))) (a!26 (fp.isZero (afn (reassoc (contract a!24))))) (a!27 (fp.neg (afn (reassoc (contract a!24))))) (a!29 (fp.isInfinite (afn (reassoc (contract a!24))))) (a!42 (fp.isNaN (afn (reassoc (contract a!41))))) (a!43 (fp.isZero (afn (reassoc (contract a!41))))) (a!44 (fp.neg (afn (reassoc (contract a!41))))) (a!46 (fp.isInfinite (afn (reassoc (contract a!41))))) (a!53 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isNaN (afn a!48))) (not (fp.isNaN a!49)) (not (fp.isInfinite (afn a!48))) (not (fp.isInfinite a!49)) (not (fp.isNaN a!50)) (not a!51) (not (fp.isInfinite a!50)) (not a!52))) (a!60 (ite a!58 a!59 (afn (reassoc (contract a!56))))) (a!67 (not (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!14) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!15) (not a!17) (not (fp.isNaN a!63)) (not a!22) (not (fp.isInfinite a!63)) (not (fp.isNaN a!64)) (not a!65) (not (fp.isInfinite a!64)) (not a!66)))) (a!72 (not (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!31) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!32) (not a!34) (not (fp.isNaN a!68)) (not a!39) (not (fp.isInfinite a!68)) (not (fp.isNaN a!69)) (not a!70) (not (fp.isInfinite a!69)) (not a!71)))) (a!77 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isNaN (afn a!48))) (not (fp.isNaN a!73)) (not (fp.isInfinite (afn a!48))) (not (fp.isInfinite a!73)) (not (fp.isNaN a!74)) (not a!75) (not (fp.isInfinite a!74)) (not a!76))) (a!84 (ite a!82 a!83 (afn (reassoc (contract a!80))))) (a!88 (fp.sqrt roundNearestTiesToEven (ite (fp.isZero (afn a!87)) (fp.neg (afn a!87)) (afn a!87)))) (a!91 (fp.sqrt roundNearestTiesToEven (ite (fp.isZero (afn a!90)) (fp.neg (afn a!90)) (afn a!90)))) (a!97 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite (fp.mul roundNearestTiesToEven %y %x))) (not (fp.isNaN (afn a!48))) (not (fp.isNaN a!93)) (not (fp.isInfinite (afn a!48))) (not (fp.isInfinite a!93)) (not (fp.isNaN a!94)) (not a!95) (not (fp.isInfinite a!94)) (not a!96))) (a!100 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN a!1)) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite a!1)) (not (fp.isNaN a!2)) (not (fp.isNaN (fp.mul roundNearestTiesToEven a!2 %x))) (not (fp.isInfinite a!2)) (not (fp.isInfinite (fp.mul roundNearestTiesToEven a!2 %x))) (not (fp.isNaN (afn a!98))) (not (fp.isNaN a!99)) (not (fp.isInfinite (afn a!98))) (not (fp.isInfinite a!99)))) (a!105 (not (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!14) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!15) (not a!17) (not (fp.isNaN a!101)) (not a!22) (not (fp.isInfinite a!101)) (not (fp.isNaN a!102)) (not a!103) (not (fp.isInfinite a!102)) (not a!104)))) (a!110 (not (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!31) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!32) (not a!34) (not (fp.isNaN a!106)) (not a!39) (not (fp.isInfinite a!106)) (not (fp.isNaN a!107)) (not a!108) (not (fp.isInfinite a!107)) (not a!109)))) (a!118 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN a!1)) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite a!1)) (not (fp.isNaN a!2)) (not (fp.isNaN a!3)) (not (fp.isInfinite a!2)) (not (fp.isInfinite a!3)) (not (fp.isNaN a!4)) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!4))) (not (fp.isInfinite a!4)) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!4))))) (a!119 (fp.sqrt roundNearestTiesToEven (afn (reassoc (contract a!24))))) (a!121 (fp.sqrt roundNearestTiesToEven (afn (reassoc (contract a!41))))) (a!125 (not (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN a!1)) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite a!1)) (not (fp.isNaN a!2)) (not a!54) (not (fp.isInfinite a!2)) (not a!55) (not a!57) (not (fp.isNaN a!124)) (not a!61) (not (fp.isInfinite a!124))))) (a!130 (not (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN a!1)) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite a!1)) (not (fp.isNaN a!2)) (not a!78) (not (fp.isInfinite a!2)) (not a!79) (not a!81) (not (fp.isNaN a!129)) (not a!85) (not (fp.isInfinite a!129))))) (a!131 (not (fp.isNaN (fp.sqrt roundNearestTiesToEven (afn a!87))))) (a!132 (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven (afn a!87))))) (a!134 (not (fp.isNaN (fp.sqrt roundNearestTiesToEven (afn a!90))))) (a!135 (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven (afn a!90))))) (a!140 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN a!1)) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite a!1)) (not (fp.isNaN a!2)) (not (fp.isNaN (fp.mul roundNearestTiesToEven a!2 %x))) (not (fp.isInfinite a!2)) (not (fp.isInfinite (fp.mul roundNearestTiesToEven a!2 %x))) (not (fp.isNaN (afn a!98))) a!138 (not (fp.isInfinite (afn a!98))) a!139))) (let ((a!7 (not (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN a!1)) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite a!1)) (not (fp.isNaN a!2)) (not (fp.isNaN a!3)) (not (fp.isInfinite a!2)) (not (fp.isInfinite a!3)) (not (fp.isNaN a!4)) (not a!5) (not (fp.isInfinite a!4)) (not a!6)))) (a!28 (ite a!26 a!27 (afn (reassoc (contract a!24))))) (a!45 (ite a!43 a!44 (afn (reassoc (contract a!41))))) (a!62 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN a!1)) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite a!1)) (not (fp.isNaN a!2)) (not a!54) (not (fp.isInfinite a!2)) (not a!55) (not a!57) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!60))) (not a!61) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!60))))) (a!86 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not (fp.isNaN a!1)) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not (fp.isInfinite a!1)) (not (fp.isNaN a!2)) (not a!78) (not (fp.isInfinite a!2)) (not a!79) (not a!81) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!84))) (not a!85) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!84))))) (a!89 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!14) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!15) (not a!17) (not (fp.isNaN (fp.mul roundNearestTiesToEven a!20 %x))) (not a!22) (not (fp.isInfinite (fp.mul roundNearestTiesToEven a!20 %x))) (not (fp.isNaN (afn a!87))) (not (fp.isNaN a!88)) (not (fp.isInfinite (afn a!87))) (not (fp.isInfinite a!88)))) (a!92 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!31) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!32) (not a!34) (not (fp.isNaN (fp.mul roundNearestTiesToEven a!37 %x))) (not a!39) (not (fp.isInfinite (fp.mul roundNearestTiesToEven a!37 %x))) (not (fp.isNaN (afn a!90))) (not (fp.isNaN a!91)) (not (fp.isInfinite (afn a!90))) (not (fp.isInfinite a!91)))) (a!120 (not (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!14) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!15) (not a!17) (not a!21) (not a!22) (not a!23) (not a!25) (not (fp.isNaN a!119)) (not a!29) (not (fp.isInfinite a!119))))) (a!122 (not (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!31) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!32) (not a!34) (not a!38) (not a!39) (not a!40) (not a!42) (not (fp.isNaN a!121)) (not a!46) (not (fp.isInfinite a!121))))) (a!133 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!14) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!15) (not a!17) (not (fp.isNaN (fp.mul roundNearestTiesToEven a!20 %x))) (not a!22) (not (fp.isInfinite (fp.mul roundNearestTiesToEven a!20 %x))) (not (fp.isNaN (afn a!87))) a!131 (not (fp.isInfinite (afn a!87))) a!132)) (a!136 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!31) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!32) (not a!34) (not (fp.isNaN (fp.mul roundNearestTiesToEven a!37 %x))) (not a!39) (not (fp.isInfinite (fp.mul roundNearestTiesToEven a!37 %x))) (not (fp.isNaN (afn a!90))) a!134 (not (fp.isInfinite (afn a!90))) a!135))) (let ((a!30 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!14) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!15) (not a!17) (not a!21) (not a!22) (not a!23) (not a!25) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!28))) (not a!29) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!28))))) (a!47 (and (not (fp.isNaN %y)) (not (fp.isNaN %x)) (not a!31) (not (fp.isInfinite %y)) (not (fp.isInfinite %x)) (not a!32) (not a!34) (not a!38) (not a!39) (not a!40) (not a!42) (not (fp.isNaN (fp.sqrt roundNearestTiesToEven a!45))) (not a!46) (not (fp.isInfinite (fp.sqrt roundNearestTiesToEven a!45)))))) (and (not (or a!7 a!13)) (not (or (not a!30) a!13)) (not (or (not a!47) a!13)) (not (or (not a!53) a!13)) (not (or (not a!62) a!13)) (not (or a!67 a!13)) (not (or a!72 a!13)) (not (or (not a!77) a!13)) (not (or (not a!86) a!13)) (not (or (not a!89) a!13)) (not (or (not a!92) a!13)) (not (or (not a!97) a!13)) (not (or (not a!100) a!13)) (not (or a!105 a!13)) (not (or a!110 a!13)) (not (or (not a!117) a!13)) (not (or (not a!118) a!13)) (not (or a!120 a!13)) (not (or a!122 a!13)) (not (or (not a!123) a!13)) (not (or a!125 a!13)) (not (or (not a!126) a!13)) (not (or (not a!127) a!13)) (not (or (not a!128) a!13)) (not (or a!130 a!13)) (not (or (not a!133) a!13)) (not (or (not a!136) a!13)) (not (or (not a!137) a!13)) (not (or (not a!140) a!13)) (not (or (not a!141) a!13)) (not (or (not a!142) a!13)) (not (or (not a!145) a!13))))))))))) (check-sat)