Question about the holstep dataset

[AI-coder]

Hi ,I am currently working on premise selection (HOLSTEP : A MACHINE LEARNING DATASET FOR HIGHER - ORDER LOGIC THEOREM PROVING), I questioned about this issue: for a conjecture instance, how did your team generate statements from dependencies listed.
I read through the paper but found that the problem is barely described. Thus, I hope you can give some advice on this issue.
Thanks a lot! :）