blob: 019a935c4db7eb045ee4637cfed3dd70ad89cac0 (
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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
(benchmark eq_diamond14
:logic QF_UF
:extrasorts (V)
:extrafuns ((z9 V))
:extrafuns ((x10 V))
:extrafuns ((x9 V))
:extrafuns ((x13 V))
:extrafuns ((x0 V))
:extrafuns ((z12 V))
:extrafuns ((x12 V))
:extrafuns ((y12 V))
:extrafuns ((z11 V))
:extrafuns ((x11 V))
:extrafuns ((y11 V))
:extrafuns ((z10 V))
:extrafuns ((y10 V))
:extrafuns ((y8 V))
:extrafuns ((x8 V))
:extrafuns ((y7 V))
:extrafuns ((x7 V))
:extrafuns ((z6 V))
:extrafuns ((x6 V))
:extrafuns ((y6 V))
:extrafuns ((z5 V))
:extrafuns ((x5 V))
:extrafuns ((y5 V))
:extrafuns ((y4 V))
:extrafuns ((x4 V))
:extrafuns ((y3 V))
:extrafuns ((x3 V))
:extrafuns ((y2 V))
:extrafuns ((x2 V))
:extrafuns ((y1 V))
:extrafuns ((x1 V))
:extrafuns ((y0 V))
:status unsat
:formula
(flet ($n1 (= x0 y0))
(flet ($n2 (= y0 x1))
(flet ($n3 (and $n1 $n2))
(flet ($n4 (= x1 y1))
(flet ($n5 (= y1 x2))
(flet ($n6 (and $n4 $n5))
(flet ($n7 (= x2 y2))
(flet ($n8 (= y2 x3))
(flet ($n9 (and $n7 $n8))
(flet ($n10 (= x3 y3))
(flet ($n11 (= y3 x4))
(flet ($n12 (and $n10 $n11))
(flet ($n13 (= x4 y4))
(flet ($n14 (= y4 x5))
(flet ($n15 (and $n13 $n14))
(flet ($n16 false)
(flet ($n17 (= y5 x6))
(flet ($n18 (and $n16 $n17))
(flet ($n19 (= x5 z5))
(flet ($n20 (= x6 z5))
(flet ($n21 (and $n19 $n20))
(flet ($n22 (or $n18 $n21))
(flet ($n23 (= x6 y6))
(flet ($n24 (= y6 x7))
(flet ($n25 (and $n23 $n24))
(flet ($n26 (= x6 z6))
(flet ($n27 (= x7 z6))
(flet ($n28 (and $n26 $n27))
(flet ($n29 (or $n25 $n28))
(flet ($n30 (= x7 y7))
(flet ($n31 (= y7 x8))
(flet ($n32 (and $n30 $n31))
(flet ($n33 (= x8 y8))
(flet ($n34 (= y8 x9))
(flet ($n35 (and $n33 $n34))
(flet ($n36 (= x10 y10))
(flet ($n37 (= y10 x11))
(flet ($n38 (and $n36 $n37))
(flet ($n39 (= x10 z10))
(flet ($n40 (= x11 z10))
(flet ($n41 (and $n39 $n40))
(flet ($n42 (or $n38 $n41))
(flet ($n43 (= x11 y11))
(flet ($n44 (= y11 x12))
(flet ($n45 (and $n43 $n44))
(flet ($n46 (= x11 z11))
(flet ($n47 (= x12 z11))
(flet ($n48 (and $n46 $n47))
(flet ($n49 (or $n45 $n48))
(flet ($n50 (= x12 y12))
(flet ($n51 (= y12 x13))
(flet ($n52 (and $n50 $n51))
(flet ($n53 (= x12 z12))
(flet ($n54 (= x13 z12))
(flet ($n55 (and $n53 $n54))
(flet ($n56 (or $n52 $n55))
(flet ($n57 (= x0 x13))
(flet ($n58 (not $n57))
(flet ($n59 (= x9 z9))
(flet ($n60 (= x10 z9))
(flet ($n61 (and $n59 $n60))
(flet ($n62 (or $n16 $n61))
(flet ($n63 (and $n3 $n6 $n9 $n12 $n15 $n22 $n29 $n32 $n35 $n42 $n49 $n56 $n58 $n62))
$n63
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
