(set-option :produce-proofs true)

; Some string
(declare-const perm String)

; of this length
(assert (= (str.len perm) 152))

; with these substrings...
(assert (str.prefixof "12345" perm))
(assert (str.contains perm "21345"))
(assert (str.contains perm "32145"))
(assert (str.contains perm "23145"))
(assert (str.contains perm "31245"))
(assert (str.contains perm "13245"))
(assert (str.contains perm "43215"))
(assert (str.contains perm "34215"))
(assert (str.contains perm "32415"))
(assert (str.contains perm "42315"))
(assert (str.contains perm "24315"))
(assert (str.contains perm "23415"))
(assert (str.contains perm "41235"))
(assert (str.contains perm "14235"))
(assert (str.contains perm "12435"))
(assert (str.contains perm "42135"))
(assert (str.contains perm "24135"))
(assert (str.contains perm "21435"))
(assert (str.contains perm "41325"))
(assert (str.contains perm "14325"))
(assert (str.contains perm "13425"))
(assert (str.contains perm "43125"))
(assert (str.contains perm "34125"))
(assert (str.contains perm "31425"))
(assert (str.contains perm "54321"))
(assert (str.contains perm "45321"))
(assert (str.contains perm "43521"))
(assert (str.contains perm "43251"))
(assert (str.contains perm "53421"))
(assert (str.contains perm "35421"))
(assert (str.contains perm "34521"))
(assert (str.contains perm "34251"))
(assert (str.contains perm "52341"))
(assert (str.contains perm "25341"))
(assert (str.contains perm "23541"))
(assert (str.contains perm "23451"))
(assert (str.contains perm "53241"))
(assert (str.contains perm "35241"))
(assert (str.contains perm "32541"))
(assert (str.contains perm "32451"))
(assert (str.contains perm "52431"))
(assert (str.contains perm "25431"))
(assert (str.contains perm "24531"))
(assert (str.contains perm "24351"))
(assert (str.contains perm "54231"))
(assert (str.contains perm "45231"))
(assert (str.contains perm "42531"))
(assert (str.contains perm "42351"))
(assert (str.contains perm "51234"))
(assert (str.contains perm "15234"))
(assert (str.contains perm "12534"))
(assert (str.contains perm "12354"))
(assert (str.contains perm "52134"))
(assert (str.contains perm "25134"))
(assert (str.contains perm "21534"))
(assert (str.contains perm "21354"))
(assert (str.contains perm "52314"))
(assert (str.contains perm "25314"))
(assert (str.contains perm "23514"))
(assert (str.contains perm "23154"))
(assert (str.contains perm "51324"))
(assert (str.contains perm "15324"))
(assert (str.contains perm "13524"))
(assert (str.contains perm "13254"))
(assert (str.contains perm "53124"))
(assert (str.contains perm "35124"))
(assert (str.contains perm "31524"))
(assert (str.contains perm "31254"))
(assert (str.contains perm "53214"))
(assert (str.contains perm "35214"))
(assert (str.contains perm "32514"))
(assert (str.contains perm "32154"))
(assert (str.contains perm "51432"))
(assert (str.contains perm "15432"))
(assert (str.contains perm "14532"))
(assert (str.contains perm "14352"))
(assert (str.contains perm "54132"))
(assert (str.contains perm "45132"))
(assert (str.contains perm "41532"))
(assert (str.contains perm "41352"))
(assert (str.contains perm "54312"))
(assert (str.contains perm "45312"))
(assert (str.contains perm "43512"))
(assert (str.contains perm "43152"))
(assert (str.contains perm "51342"))
(assert (str.contains perm "15342"))
(assert (str.contains perm "13542"))
(assert (str.contains perm "13452"))
(assert (str.contains perm "53142"))
(assert (str.contains perm "35142"))
(assert (str.contains perm "31542"))
(assert (str.contains perm "31452"))
(assert (str.contains perm "53412"))
(assert (str.contains perm "35412"))
(assert (str.contains perm "34512"))
(assert (str.contains perm "34152"))
(assert (str.contains perm "51423"))
(assert (str.contains perm "15423"))
(assert (str.contains perm "14523"))
(assert (str.contains perm "14253"))
(assert (str.contains perm "54123"))
(assert (str.contains perm "45123"))
(assert (str.contains perm "41523"))
(assert (str.contains perm "41253"))
(assert (str.contains perm "54213"))
(assert (str.contains perm "45213"))
(assert (str.contains perm "42513"))
(assert (str.contains perm "42153"))
(assert (str.contains perm "51243"))
(assert (str.contains perm "15243"))
(assert (str.contains perm "12543"))
(assert (str.contains perm "12453"))
(assert (str.contains perm "52143"))
(assert (str.contains perm "25143"))
(assert (str.contains perm "21543"))
(assert (str.contains perm "21453"))
(assert (str.contains perm "52413"))
(assert (str.contains perm "25413"))
(assert (str.contains perm "24513"))
(assert (str.contains perm "24153"))

; Does it exist?
(check-sat)

;(get-model)
(get-proof)