The validator part of the program almost uses backward-chaining implementation. The "list" of goals" for the backward-chaining is created by the definer part of the program which uses a recursive function.
Very interesting! Do you know how is the constraint solver library implemented? Does it use a different general implementation than the regular prolog statements?