Drools how to make theorem prover using RETE?

Drools how to make theorem prover using RETE?

we need a system to prove theorem's like :
(A+B).(C+D) + E + C.(E+D) = A.C + A.D + B.C + B.D + E + C.E + C.D
these may be more complex
how to make a program for this using Drools ...
Tried making search tree using update modify methods but it was not
working out somehow.