fmod WITCH is

    *** Anything can be a thing - duck, person, witch etc.
    sort Thing .
    
    *** Represents the weight of an object
    sort Weight .
  
    *** true if a thing floats
    op floats : Thing -> Bool .
    
    *** true if a thing is made of wood
    op isWood : Thing -> Bool .
    
    *** true is Thing burns
    op burns : Thing -> Bool .
    
    *** true if a Thing is a witch
    op isWitch : Thing -> Bool .

    *** Returns the weight of a Thing
    op weight : Thing -> Weight .
    
    *** Equality operator for Things
    op _===_ : Weight Weight -> Bool .
    
    *** Constant representing the possible witch
    op witch? : -> Thing .

    *** Constant for the duck
    op duck : -> Thing .
    
    var x : Thing .

    *** The assumptions
    eq floats(duck) = true .
    eq weight(witch?) === weight(duck) = true .

    *** The rules
    ceq isWood(x) = true if floats(x) == true .
    ceq burns(x) = true if isWood(x) == true .
    ceq isWitch(x) = true if burns(x) == true .
    ceq floats(x) = true if floats(duck) and
                        (weight(x) === weight(duck)) .
endfm