ROOTS

included axiom formulas (removing a FIXME) in the imported problem;
turned tests into asserts;
changed problem to one which actually succeeds using z3;

src/Pure
src/FOL
src/HOL
src/ZF
src/CCL
src/CTT
src/Cube
src/FOLP
src/LCF
src/Sequents
src/Doc
src/Tools