blob: 08fd6025bcecff1152fa5bc63dddd7fd3059269e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
; COMMAND-LINE: --relational-triggers
; EXPECT: unsat
(set-logic UF)
(declare-sort $$unsorted 0)
(declare-fun in ($$unsorted $$unsorted) Bool)
(declare-fun powerset ($$unsorted) $$unsorted)
(declare-fun subset ($$unsorted $$unsorted) Bool)
(declare-fun empty ($$unsorted) Bool)
(declare-fun element ($$unsorted $$unsorted) Bool)
(declare-fun empty_set () $$unsorted)
(set-info :filename "SEU169+1")
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (in A B)) (not (in B A))) ))
(assert (forall ((A $$unsorted) (B $$unsorted)) (= (= B (powerset A)) (forall ((C $$unsorted)) (= (in C B) (subset C A)) )) ))
(assert (and (forall ((A $$unsorted) (B $$unsorted)) (or (empty A) (= (element B A) (in B A))) ) (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= (element B A) (empty B))) )))
(assert (forall ((A $$unsorted) (B $$unsorted)) (= (subset A B) (forall ((C $$unsorted)) (or (not (in C A)) (in C B)) )) ))
(assert (forall ((A $$unsorted)) (not (forall ((B $$unsorted)) (not (element B A)) )) ))
(assert (forall ((A $$unsorted)) (not (empty (powerset A))) ))
(assert (empty empty_set))
(assert (not (forall ((A $$unsorted) (B $$unsorted) (BOUND_VARIABLE_423 $$unsorted)) (or (not (element B (powerset A))) (not (in BOUND_VARIABLE_423 B)) (in BOUND_VARIABLE_423 A)) )))
(assert (forall ((A $$unsorted)) (or (empty A) (not (forall ((B $$unsorted)) (or (not (element B (powerset A))) (empty B)) ))) ))
(assert (not (forall ((A $$unsorted)) (not (empty A)) )))
(assert (not (forall ((A $$unsorted)) (empty A) )))
(assert (forall ((A $$unsorted)) (subset A A) ))
(assert (forall ((A $$unsorted)) (or (not (empty A)) (= empty_set A)) ))
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (in A B)) (not (empty B))) ))
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= A B) (not (empty B))) ))
(assert true)
(assert (and (forall ((A $$unsorted) (B $$unsorted)) (or (empty A) (= (element B A) (in B A))) ) (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= (element B A) (empty B))) )))
(check-sat)
|
