% COMMAND-LINE: --tlimit 5000
% EXPECT: unsat
% EXIT: 20