We consider exponentially large finite relational structures (with the universe {0,1}n) whose basic relations are computed by polynomial size (nO(1)) circuits. We study behaviour of such structures when pulled back by 𝒫/poly maps to a bigger or to a smaller universe. In particular, we prove that: ¶ 1. If there exists a 𝒫/poly map g : {0,1}n → {0,1}m, n < m, iterable for a proof system then a tautology (independent of g) expressing that a particular size n set is dominating in a size 2n tournament is hard for the proof system. ¶ 2. The search problem WPHP, decoding RSA or finding a collision in a hashing function can be reduced to finding a size m homogeneous subgraph in a size 22m graph. ¶ Further we reduce the proof complexity of a concrete tautology (expressing a Ramsey property of a graph) in strong systems to the complexity of implicit proofs of implicit formulas in weak proof systems.