61.24/60.05	sh: line 1: 64335 Alarm clock             /export/starexec/sandbox/solver/bin/yices 2> /dev/null
61.24/60.06	EOF