Is your feature request related to a problem? Please describe.
@teorth wrote "Anyway this makes me realize that it is far better to use ATPs to test whether various relaxations of laws are possible in order to truncate the iteration, than to simply propose them and then do a very tedious human verification"

I've been running my tests exactly this way and think that we could profit from an agent testing new Vampire scripts based on our continuous input (in natural language).

Describe the solution you'd like

A tool enabling this kind of use case through natural language (via @teorth ): "can you try the same exercise with m(W,t(Y,Z))=t(W,Y) replaced by m(t(Y,Z),t(W,Y))=t(t(Y,Z),W)?"

One would keep asking natural language questions, the LLM would adjust the script, run Vampire, and evaluate the output.

Describe alternatives you've considered

The alternative is manual (or LLM-assisted) creation and then modification of Vampire scripts.

Additional context

It's based on the discussion in 1516->255.