The connectivity constraint provides only marginal improvement as our model mostly predicts connected proofs without any explicit supervision.
only 57 examples have disconnected proofs without this constraint.