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 if__better on the Boolean formula,__well, if__better is the only difference__between a nondeterministic and a deterministic RAM, so if we had all the calls to if__better,__we wouldn’t actually have to simulate if__better,__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 if__better.__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.