(set-option :incremental false)
(set-info :status unsat)
(set-info :difficulty "unknown")
(set-info :category "crafted")
(set-logic QF_UF)
(declare-sort U 0)
(declare-sort A 0)
(declare-fun x () A)
(declare-fun f (A) A)
(check-sat-assuming ( (let ((_let_0 (f x))) (let ((_let_1 (= (f _let_0) x))) (let ((_let_2 (f (f _let_0)))) (let ((_let_3 (= _let_2 x))) (let ((_let_4 (f _let_2))) (let ((_let_5 (f _let_4))) (not (=> (or (or (or (and _let_1 _let_3) (and _let_1 (= _let_5 x))) (and _let_3 (= _let_4 _let_2))) (and _let_3 (= _let_5 _let_2))) (= _let_0 x))))))))) ))