We describe an implementation of gradient boosting and neural guidance of\nsaturation-style automated theorem provers that does not depend on consistent\nsymbol names across problems. For the gradient-boosting guidance, we manually\ncreate abstracted features by considering arity-based encodings of formulas.\nFor the neural guidance, we use symbol-independent graph neural networks (GNNs)\nand their embedding of the terms and clauses. The two methods are efficiently\nimplemented in the E prover and its ENIGMA learning-guided framework.\n To provide competitive real-time performance of the GNNs, we have developed a\nnew context-based approach to evaluation of generated clauses in E. Clauses are\nevaluated jointly in larger batches and with respect to a large number of\nalready selected clauses (context) by the GNN that estimates their collectively\nmost useful subset in several rounds of message passing. This means that\napproximative inference rounds done by the GNN are efficiently interleaved with\nprecise symbolic inference rounds done inside E. The methods are evaluated on\nthe MPTP large-theory benchmark and shown to achieve comparable real-time\nperformance to state-of-the-art symbol-based methods. The methods also show\nhigh complementarity, solving a large number of hard Mizar problems.\n