Suppose an agent inhabits a world with two states, S and ¬S, and can do exactly one of two actions, a and b. Action a does nothing and action b flips from one state to the other. Let S^t be the proposition that the agent is in state S at time t, and let a^t be the proposition that the agent does action a at time t (similarly for b^t). 

a. Write a successor-state axiom for S^t+1. 

b. Convert the sentence in (a) into CNF. 

c. Show a resolution refutation proof that if the agent is in ¬S at time t and does a, it will still be in ¬S at time t + 1.