Theorem 5. Grail 3.0 echo '0*10(10+01+1100+0011)*+0*1(10+01)*0+0*' | retofm | fmdeterm | fmmin | fmcomp | fmrenum > e1 produces the output automaton e1 as follows: (START) |- 0 0 0 0 0 1 1 1 0 2 1 1 3 2 0 4 2 1 5 3 0 6 3 1 7 4 0 8 4 1 9 5 0 2 5 1 10 6 0 11 6 1 3 7 0 7 8 0 7 8 1 12 9 0 4 9 1 13 10 0 1 10 1 7 11 0 7 11 1 6 12 0 7 12 1 9 13 0 9 13 1 14 14 0 15 14 1 7 15 0 9 15 1 7 7 1 7 0 -| (FINAL) 2 -| (FINAL) 9 -| (FINAL) 11 -| (FINAL) This corresponds to the QQ.txt file for Walnut as follows: msd_2 0 1 0 -> 0 1 -> 1 1 0 0 -> 2 1 -> 3 2 1 0 -> 4 1 -> 5 3 0 0 -> 6 1 -> 7 4 0 0 -> 8 1 -> 9 5 0 0 -> 2 1 -> 10 6 0 0 -> 11 1 -> 3 7 0 0 -> 7 1 -> 7 8 0 0 -> 7 1 -> 12 9 1 0 -> 4 1 -> 13 10 0 0 -> 1 1 -> 7 11 1 0 -> 7 1 -> 6 12 0 0 -> 7 1 -> 9 13 0 0 -> 9 1 -> 14 14 0 0 -> 15 1 -> 7 15 0 0 -> 9 1 -> 7 The Walnut command is eval eqq "E x,y,z (n=x+y+z)&(QQ[x]=@1)&(QQ[y]=@1)&(QQ[z]=@1)": and before issuing that command, Walnut needs to be invoked with the following command line (in order to have enough space) java -Xmx11000M -d64 Main.prover The output log is eval eqq "E x,y,z (n=x+y+z)&(QQ[x]=@1)&(QQ[y]=@1)&(QQ[z]=@1)": n=((x+y)+z):3 states - 8ms QQ[x]=@1:15 states - 3ms (n=((x+y)+z)&QQ[x]=@1):45 states - 14ms QQ[y]=@1:15 states - 2ms ((n=((x+y)+z)&QQ[x]=@1)&QQ[y]=@1):331 states - 85ms QQ[z]=@1:15 states - 1ms (((n=((x+y)+z)&QQ[x]=@1)&QQ[y]=@1)&QQ[z]=@1):1790 states - 270ms (E x , y , z (((n=((x+y)+z)&QQ[x]=@1)&QQ[y]=@1)&QQ[z]=@1)):12 states - 176594ms total computation time: 177016ms and the output automaton is msd_2 0 1 0 -> 0 1 -> 1 1 0 0 -> 2 1 -> 3 2 1 0 -> 4 1 -> 5 3 0 0 -> 6 1 -> 7 4 1 0 -> 8 1 -> 9 5 0 0 -> 9 1 -> 9 6 1 0 -> 10 1 -> 9 7 0 0 -> 9 1 -> 5 8 0 0 -> 11 1 -> 5 9 1 0 -> 9 1 -> 9 10 1 0 -> 9 1 -> 5 11 1 0 -> 9 1 -> 10