Termination proof found.
Execution time: 22.880000 sec

real	0m26.095s
user	0m23.169s
sys	0m0.064s