blob: 7a324952eeaa36ead1f78af9489a6cfd52496e45 (
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
; COMMAND-LINE: --produce-proofs
; EXIT: 0
; SCRUBBER: grep -v -E '.*'
(set-logic AUFLIA)
(declare-sort A$ 0)
(declare-sort B$ 0)
(declare-sort C$ 0)
(declare-sort D$ 0)
(declare-sort E$ 0)
(declare-sort F$ 0)
(declare-sort G$ 0)
(declare-sort H$ 0)
(declare-sort I$ 0)
(declare-sort J$ 0)
(declare-sort K$ 0)
(declare-sort L$ 0)
(declare-sort M$ 0)
(declare-sort N$ 0)
(declare-sort O$ 0)
(declare-sort P$ 0)
(declare-fun f1$ (M$ J$) L$)
(declare-fun f2$ (N$ C$) L$)
(declare-fun f3$ (C$ A$) B$)
(declare-fun f4$ (D$ E$) B$)
(declare-fun f5$ (F$ G$) D$)
(declare-fun f6$ (A$) F$)
(declare-fun f7$ (A$) G$)
(declare-fun f8$ (A$) E$)
(declare-fun f9$ (A$) E$)
(declare-fun x1$ () M$)
(declare-fun x2$ () N$)
(declare-fun x3$ () C$)
(declare-fun x4$ () C$)
(declare-fun x5$ () D$)
(declare-fun x6$ () J$)
(declare-fun x7$ () J$)
(declare-fun x8$ () M$)
(declare-fun x9$ () O$)
(declare-fun f10$ (H$ A$) K$)
(declare-fun f3a$ (E$ H$) I$)
(declare-fun f3b$ (J$ K$) I$)
(declare-fun f5a$ (O$ P$) N$)
(declare-fun x10$ () P$)
(assert (! (forall ((?v0 A$)) (not (= (f3$ x3$ ?v0) (f4$ (f5$ (f6$ ?v0) (f7$ ?v0)) (f8$ ?v0))))) :named a0))
(assert (! (forall ((?v0 A$)) (not (= (f3$ x4$ ?v0) (f4$ x5$ (f9$ ?v0))))) :named a1))
(assert (! (forall ((?v0 A$) (?v1 H$)) (not (= (f3a$ (f8$ ?v0) ?v1) (f3b$ x6$ (f10$ ?v1 ?v0))))) :named a2))
(assert (! (forall ((?v0 A$) (?v1 H$)) (not (= (f3a$ (f9$ ?v0) ?v1) (f3b$ x7$ (f10$ ?v1 ?v0))))) :named a3))
(assert (! (not (= (f1$ x8$ x6$) (f2$ (f5a$ x9$ x10$) x3$))) :named a4))
(assert (! (= (f1$ x1$ x7$) (f1$ x8$ x6$)) :named a5))
(assert (! (= (f1$ x1$ x7$) (f2$ x2$ x4$)) :named a6))
(assert (! (= (f2$ x2$ x4$) (f2$ (f5a$ x9$ x10$) x3$)) :named a7))
(assert (! (not false) :named a8))
(check-sat)
(get-proof)
|
