Recently, I have proved that Kazhdan's property (T) is theoretically provable by computers (arXiv:1312.5431, explained below), but I'm quite lame with computers and have no idea what they actually can do. So, my question is how feasible is it to prove property (T) of a given group, say $\mathrm{Out}(F_{r>3})$ (a famous open problem), by solving the equation below by a computer? Even the case of $\mathrm{SL}_{r>2}({\mathbb Z})$ where property (T) is known is unclear.

A group $\Gamma$, generated by a finite subset $S$ and with its non-normalized Laplacian denoted by $$\Delta=\sum_{x\in S} (1-x)^*(1-x)=\sum_{x\in S} (2-x-x^{-1})\in{\mathbb Z}[\Gamma],$$ has property (T) iff the equation in ${\mathbb Z}[\Gamma]$, $$ m \Delta^2 = n \Delta + \sum_{i=1}^k l_i \xi_i^*\xi_i $$ has a solution in $k,m,n,l_i\in{\mathbb Z}_{>0}$ and $\xi_i\in{\mathbb Z}[\Gamma]$.