TIMESTAMP = 1791778209
SHA256 (cvc5-cvc5-cvc5-1.4.2_GH0.tar.gz) = 795099b277bfa79a3c9a11c8d3fec780452031dc89ddcc170003963aa3521343
SIZE (cvc5-cvc5-cvc5-1.4.2_GH0.tar.gz) = 8992756
