Alter csv header to be only one line, add CongruenceCompressor variants (Array, Fibonacci PQ), implement first version of ProofForest datastructure (BarceLogic)