Well, as benjamincburns says in another comment, Z3 is basically equivalent to the finite domain solver of a Prolog. Since mini-Kanren is a Prolog, it is not su

Well, as benjamincburns says in another comment, Z3 is basically equivalent to the finite domain solver of a Prolog. Since mini-Kanren is a Prolog, it is not surprising that it is more powerful. Otherwise Z3 would also be a Prolog :).