If you are working on the challenge of synthesizing xpose for data sizes larger than 4x4, you may find this file useful, for scaability comparisons between your solver and the Sketch system. In this file, the input has been fixed to the single matrix that the human knows is sufficient for successful synthesis. As a result, the Sketch synthesizer does not make multiple calls to the synthesizer, each time with a larger set of inputs. It just makes one call.
--Ras