Alright, first if we had a complete series of snapshots from a nondeterministic RAM solving SAT on his formula. Well, a nondeterministic RAM can solve SAT in polynomial time, so we can check those in polynomial time as well since we just have a list of these. So once we have those, we can definitely verify that his formula is satisfiable. Now if we had a list of satisfiable clauses, this actually isn’t enough to verify that Bob’s formula is also satisfiable. To see this, let’s take a look at the formula in somewhat pythonic form, X and not X. Now clearly X is a satisfiable clause and so is not X, but the entire Boolean formula is definitely not satisfiable. So a list of satisfiable clauses actually isn’t enough for us to believe Bob. Now if we had a satisfying assignment for all of the variables in the formula, then sure, we can just plug them into the formula and check on a deterministic RAM, and that occurs in polynomial time. Similarly, if add all calls to ifbetter on the Boolean formula,well, ifbetter is the only differencebetween a nondeterministic and a deterministic RAM, so if we had all the calls to ifbetter,we wouldn’t actually have to simulate ifbetter,we would know what the algorithm did at each step of the process. So we could also check Bob’s formula using just this. Not even a complete series of snapshots is necessary just the calls to ifbetter.Now let’s say we had a satisfying assignment for 90% of the variables. Well, 90% of the variables still leaves 10%, and 10% of exponential is, well, exponential. So we would still have exponentially many variables to check. So this actually doesn’t work.