A family of hard satisfiable instances in conjunctive normal form based
on random regular graphs is introduced. Instances in the family have the
structure of a system of linear equations.  Schemes for introducing
nonlinearity to the instances are developed, making the instances
suitable for benchmarking solvers with equivalence reasoning
techniques. An extensive experimental evaluation shows that the
computational hardness of the instances increases faster than in other
well-known families of hard satisfiable instances, with already small
instances being very challenging.