and([ 
     always(or([not grumpy2,next(happy1)])),
     always(or([not happy1,next(happy2)])),
     always(or([not happy2,next(sleepy1)])),
     always(or([not sleepy1,next(sleepy2)])),
     always(or([not sleepy2,next(dopey1)])),
     always(or([not dopey1,next(dopey2)])),
     always(or([not dopey2,next(sneezy1)])),
     always(or([not sneezy1,next(sneezy2)])),
     always(or([not sneezy2,next(bashful1)])),
     always(or([not bashful1,next(bashful2)])),
     always(or([not bashful2,next(doc1)])),
     always(or([not doc1,next(doc2)])),
     always(or([not doc2,next(snowwhite1)])),
     always(or([not snowwhite1,next(snowwhite2)])),
     always(or([not snowwhite2,next(grumpy1)])),
     always(or([not grumpy1,next(grumpy2)])),
     or([x]),
     always(or([not x,sometime(not work)])),
     or([work]),
     always(or([not grumpy1,not grumpy2,not happy1,not happy2,not sleepy1,not sleepy2,not dopey1,not dopey2,not sneezy1,not sneezy2,not bashful1,not bashful2,not doc1,not doc2,not snowwhite1,not snowwhite2,next(work)])),
     or([grumpy1]),
     or([grumpy2]),
     or([happy1]),
     or([happy2]),
     or([sleepy1]),
     or([sleepy2]),
     or([dopey1]),
     or([dopey2]),
     or([sneezy1]),
     or([sneezy2]),
     or([bashful1]),
     or([bashful2]),
     or([doc1]),
     or([doc2]),
     or([snowwhite1]),
     or([snowwhite2])
]).