I read the caption before the introduction, which provides better context:
QQQ
Next we use a symbolic deduction engine on the sampled premises.
The engine quickly deduces new true statements by following forward inference rules as shown in Fig. 3b. This returns a directed acyclic graph of all reachable conclusions.
Each node in the directed acyclic graph is a reachable conclusion, with edges connecting to its
parent nodes thanks to the traceback algorithm described in Methods. This allows a traceback process to run recursively starting from any node N, at the end returning its dependency subgraph G(N), with its
root being N and its leaves being a subset of the sampled premises.
Denoting this subset as P, we obtained a synthetic training example
(premises, conclusion, proof) = (P, N, G(N)).
QQQ
Edward