(read ‘setlog’) was born as a Constraint Logic Programming (CLP) language where sets and binary relations are first-class citizens, thus fostering set programming. Internally, is a constraint satisfiability solver implementing decision procedures for several fragments of set theory. Hence, can be used as a declarative, set, logic programming language and as an automated theorem prover for set theory. Over time has been extended with some components integrated to the satisfiability solver thus pr