add drat tracing/checking

[wsc1]

to participate in the SAT competition, we need to support proof tracing

also, maybe an in-memory proof xo solver will be useful.