(set-info :source "contrived")
(set-info :smt-lib-version 2.0)
(set-info :category "check")
(set-info :status unsat)
(set-logic QF_UF)
(set-info :notes |This benchmark simply checks that SMT-LIB v2 can be parsed.|)
(set-info :difficulty 0.000)
(exit)