blob: 6af6ac5be10623622fc2c5e052923182a32ca096 (
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
|
(benchmark eq_diamond14_reduced
:logic QF_UF
:source { Reduced by delta debugger from eq_diamond14 to fix a UF bug. }
:status unsat
:extrasorts (V)
:extrafuns ((x13 V))
:extrafuns ((x0 V))
:extrafuns ((y12 V))
:extrafuns ((x12 V))
:extrafuns ((z11 V))
:extrafuns ((x11 V))
:extrafuns ((y11 V))
:extrafuns ((z10 V))
:extrafuns ((x10 V))
:extrafuns ((y10 V))
:extrafuns ((y9 V))
:extrafuns ((x9 V))
:extrafuns ((y8 V))
:extrafuns ((x8 V))
:extrafuns ((y7 V))
:extrafuns ((x7 V))
:extrafuns ((y6 V))
:extrafuns ((x6 V))
:extrafuns ((y5 V))
:extrafuns ((x5 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))
: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 (= x5 y5))
(flet ($n17 (= y5 x6))
(flet ($n18 (and $n16 $n17))
(flet ($n19 (= x6 y6))
(flet ($n20 (= y6 x7))
(flet ($n21 (and $n19 $n20))
(flet ($n22 (= x7 y7))
(flet ($n23 (= y7 x8))
(flet ($n24 (and $n22 $n23))
(flet ($n25 (= x8 y8))
(flet ($n26 (= y8 x9))
(flet ($n27 (and $n25 $n26))
(flet ($n28 (= x9 y9))
(flet ($n29 (= y9 x10))
(flet ($n30 (and $n28 $n29))
(flet ($n31 false)
(flet ($n32 (= y10 x11))
(flet ($n33 (and $n31 $n32))
(flet ($n34 (= x10 z10))
(flet ($n35 (= x11 z10))
(flet ($n36 (and $n34 $n35))
(flet ($n37 (or $n33 $n36))
(flet ($n38 (= x11 y11))
(flet ($n39 (= y11 x12))
(flet ($n40 (and $n38 $n39))
(flet ($n41 (= x11 z11))
(flet ($n42 (= x12 z11))
(flet ($n43 (and $n41 $n42))
(flet ($n44 (or $n40 $n43))
(flet ($n45 (= x12 y12))
(flet ($n46 (= y12 x13))
(flet ($n47 (and $n45 $n46))
(flet ($n48 (= x0 x13))
(flet ($n49 (not $n48))
(flet ($n50 (and $n3 $n6 $n9 $n12 $n15 $n18 $n21 $n24 $n27 $n30 $n37 $n44 $n47 $n49))
$n50
)))))))))))))))))))))))))))))))))))))))))))))))))))
|
