Cacher is the code snippet organizer for pro developers

$ ghci Fruits.hs 
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( Fruits.hs, interpreted )
Ok, 1 module loaded.
*Main> sat fruits 
Unknown.
  Reason: smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))

import Data.SBV

fruits :: SInteger -> SInteger -> SInteger -> SBool
fruits a b c = equation &&& positive
    where
        x = sFromIntegral a :: SReal
        y = sFromIntegral b :: SReal
        z = sFromIntegral c :: SReal
    
        equation = x / (y + z) + y / (x + z) + z / (x + y) .== 4

        positive = a .> 0 &&& b .> 0 &&& c .> 0


main :: IO ()
main = sat fruits >>= print