Propに対しては、そのdown形の各wordを対応するprover単語に置き換えていくとprover入力用の文字列が得られます。
例 【\(\neg ⊤\)】→【- $T】
普通は( )が大量に付きます。要らないものもありますが…
Proverではx,y,z,u,v,wで始まるものが変数のようです。
テスト用input例
P xr Q Xe not P or Q
not (P & Q & R)
{all x in R . {all y in C . y = x } }
X %= \{ x \| x in X \}