Recently, I have proved that Kazhdan's property (T) is theoretically provable 
by computers (<a href="http://arxiv.org/abs/1312.5431">arXiv:1312.5431</a>, 
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]$.