import Yices.Base

main = do
    c <- empty
    push c
    push c
    push c
    push c
    pop c
    pop c
    pop c
    pop c

    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    push c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    pop c
    dump c