Let T = {1, 2, . . . , tmax} be a set of times (measured in minutes, let’s say), and let J be a set of jobs. Let scheduledAt be a predicate so that scheduledAt(j, t) is true if and only if job j is scheduled at time t. (Assume that jobs do not last more than one minute.) Formalize the following conditions using only standard quantifiers, arithmetic operators, logical connectives, and the scheduledAt predicat
1There is never more than one job scheduled at the same time.
2. Every job is scheduled at least once.
3. Job A is never run twice within two minutes.
4. Job B is run at least three times.
5. Job C is run at most twice.
6. Job D is run sometime after the last time that Job E is run.
7. Job F is run at least once between consecutive executions of Job G.
8. Job H is run at most once between consecutive executions of Job I.