So Red Team's current plans are as follows

* We are working on a prover that combines the inverse method with
focusing as sketched in class

* Goals for next week are

 1) make sure everyone really understands what we're doing
    algorithmically, and come up with an argument for its correctness

    During the meeting we had today we established that we're pretty much
    okay on what's going on propositionally, but not so much what
    has to be altered for first-order

 2) get a start on the simple parts of the implementation.
    a) TPTP parser
    b) the preliminary asynchronous phase that generates the stable
       sequent