  {log} ('setlog') is a satisfiability solver for formulas of the theory of
finite sets and finite set relation algebra (FSTRA). As such, it can be used as
an automated theorem prover (ATP) for this theory. {log} is able to
automatically prove a number of FSTRA theorems, but not all of them.
Nevertheless, we have observed that many theorems that {log} cannot
automatically prove can be divided into a few subgoals automatically
dischargeable by {log}. The purpose of this work is to present a prototype
interactive theorem prover (ITP), called {log}-ITP, providing evidence that a
proper integration of {log} into world-class ITP's can deliver a great deal of
proof automation concerning FSTRA. An empirical evaluation based on 210
theorems from the TPTP and Coq's SSReflect libraries shows a noticeable
reduction in the size and complexity of the proofs with respect to Coq.
