Could I estimate how long will it take for TLC to finish checking a model?

[jarr...@xxxxxxxxx]

Diego Ongaro presents a TLA+ specification for raft protocol in his PHD thesis. 
The spec is complex so I run it in a linux server with 20 threads in parallel. But it still takes too long to finish. 
Actually, I think it will never stop. I mean it is unacceptable if it takes a month or a year.
Is there any way to know how long will it take for TLC to finish checking a model?
Or how can I decrease the time it takes?

PS: symmetry sets optimization does not help.