Bug#812755: RFA: spass -- An automated theorem prover for first-order logic with equality

[Ralf Treinen <treinen@free.fr>]

Hi Roland,

I am not using spass directly but it is a suggestion of one the packages
I maintain (why3), and in fact I am glad to have spass in debian as it is
quite good at reasoning about quantified formulas, in contrast to most
SMT solvers.

So, I would be interested in helping out maintaining the spass package.
I think it would fit well into debian-science, so as a first step I 
would suggest to check it into the debian-science git repo.

Cheers -Ralf.