Output File Format

Variants of the --verify command can produce problem files that can be passed to an ATP. For example, the command

anthem verify --equivalence external res/examples/external_equivalence/primes/simple/primes.{1.lp,2.lp,ug} --no-proof-search --save-problems ./

produces a set of TPTP problems files in the current directory (./) without invoking an ATP to verify them. In this case, verifying each problem file amounts to proving the external equivalence of the programs primes.1.lp and primes.2.lp under the assumptions of primes.ug.