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! :）