A proof being valid does not mean the theory is useful or valid. If SAT was used, it means it is internally consistent in first order logic assuming the solver did not have a bug in it. (I bet the program was also verified.)

You can simplify these proofs by extracting subproofs and replacing them from database by substitution. It is like compression but makes more sense.