(set-option :print-success false)
(set-option :produce-proofs false)
(set-option :interpolant-check-mode true)
(set-option :verbosity 3)
(set-logic UF)
(set-info :source |Simple EPR example. Exposed a bug where the registration of already made decision in the ClauseLiterals of a fresh clause was missing. Also uses factorization.|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-sort V 0)
(declare-fun A (V V) Bool)
(declare-fun P (V) Bool)
(declare-fun S () Bool)
(declare-fun a () V)
(declare-fun b () V)
(assert (forall ((x V) (y V)) (or (A x y) S)))
(assert (not (A a b)))
(assert (or (not S) (not (P a))))
(assert (forall ((x V)) (or (P x) (P a))))
(check-sat)
(exit)