; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf

; --------------------------------------------------------------------------------
; input :
; ( a = b )
; ( b = f(c) )
; ( a != f(c) V a != b )

; theory lemma (by transitivity) :
; ( a != b V b != f(c) V a = f(c) )


;  With the theory lemma, the input is unsatisfiable.
; --------------------------------------------------------------------------------



(check
(% s sort
(% a (term s)
(% b (term s)
(% c (term s)
(% f (term (arrow s s))

; -------------------- declaration of input formula -----------------------------------

(% A1 (th_holds (= s a b))
(% A2 (th_holds (= s b (apply _ _ f c)))
(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b))))


; ------------------- specify that the following is a proof of the empty clause -----------------

(: (holds cln)

; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------

(decl_atom (= s a b) (\ v1 (\ a1
(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2
(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3


; --------------------------- proof of theory lemma ---------------------------------------------

(satlem _ _
(ast _ _ _ a1 (\ l1
(ast _ _ _ a2 (\ l2
(asf _ _ _ a3 (\ l3
(clausify_false

; this should be a proof of l1 ^ l2 ^ ~l3 => false
; this is done by theory proof rules (currently just use "trust")

  trust

))))))) (\ CT
; CT is the clause ( ~v1 V ~v2 V v3 )

; -------------------- clausification of input formulas -----------------------------------------

(satlem _ _
(asf _ _ _ a1 (\ l1
(clausify_false

; input formula A1 is ( ~l1 )
; the following should be a proof of l1 ^ ( ~l1 ) => false
; this is done by natural deduction rules

  (contra _ A1 l1)

))) (\ C1
; C1 is the clause ( v1 )


(satlem _ _
(asf _ _ _ a2 (\ l2
(clausify_false

; input formula A2 is ( ~l2 )
; the following should be a proof of l2 ^ ( ~l2 ) => false
; this is done by natural deduction rules

   (contra _ A2 l2)

))) (\ C2
; C2 is the clause ( v2 )


(satlem _ _
(ast _ _ _ a3 (\ l3
(ast _ _ _ a1 (\ l1
(clausify_false

; input formula A3 is ( ~a3 V ~a1 )
; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false
; this is done by natural deduction rules

  (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3))

))))) (\ C3
; C3 is the clause ( ~v3 V ~v1 )



; -------------------- resolution proof ------------------------------------------------------------

(satlem_simplify _ _ _

(R _ _ C1
(R _ _ C2
(R _ _ CT C3 v3) v2) v1)

(\ x x))

))))))))))))))))))))))))))
)