  This paper accompanies a new dataset of non-linear real arithmetic problems
for the SMT-LIB benchmark collection. The problems come from an automated proof
procedure of Gerhold--Kauers, which is well suited for solution by SMT. The
problems of this type have not been tackled by SMT-solvers before. We describe
the proof technique and give one new such proof to illustrate it. We then
describe the dataset and the results of benchmarking. The benchmarks on the new
dataset are quite different to the existing ones. The benchmarking also brings
forward some interesting debate on the use/inclusion of rational functions and
algebraic numbers in the SMT-LIB.
