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