blob: 3f3d40b44fa6168b27506d60bf6ac948334ff4f7 (
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
|
(benchmark PEQ012_size3_segsat.smt
:source {
CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
for more information.
This benchmark was obtained by trying to find a finite model of a first-order
formula (Albert Oliveras).
Original source is QF_UF/PEQ/PEQ012_size3.smt
Mucked up by Tim
}
:status sat
:category { crafted }
:difficulty { 0 }
:logic QF_UF
:extrafuns ((f1 U U U))
:extrafuns ((c6 U))
:extrafuns ((c3 U))
:extrafuns ((c7 U))
:extrafuns ((c5 U))
:extrafuns ((c2 U))
:extrafuns ((c4 U))
:extrafuns ((c8 U))
:extrafuns ((c9 U))
:extrafuns ((c_0 U))
:extrafuns ((c_1 U))
:extrafuns ((c_2 U))
:formula
( and
(not (= c_0 c_1))
(not (= c_0 c_2))
(not (= c_1 c_2))
(or (not (= (f1 c_0 c_1) (f1 c_0 c_1))) (= c_1 c_1) )
(or (not (= (f1 c_0 c_2) (f1 c_0 c_0))) (= c_2 c_0) )
(or (not (= (f1 c_0 c_2) (f1 c_0 c_2))) (= c_2 c_2) )
(or (not (= (f1 c_1 c_0) (f1 c_1 c_0))) (= c_0 c_0) )
(or (not (= (f1 c_1 c_0) (f1 c_1 c_2))) (= c_0 c_2) )
(or (not (= (f1 c_1 c_1) (f1 c_1 c_0))) (= c_1 c_0) )
(= (f1 (f1 c_0 c_0) c_0) (f1 c_0 (f1 c_0 c_0)))
(= (f1 (f1 c_0 c_0) c_2) (f1 c_0 (f1 c_0 c_2)))
(= (f1 (f1 c_0 c_1) c_1) (f1 c_0 (f1 c_1 c_1)))
(= (f1 (f1 c_0 c_1) c_2) (f1 c_0 (f1 c_1 c_2)))
(= (f1 (f1 c_2 c_1) c_2) (f1 c_2 (f1 c_1 c_2)))
(= (f1 (f1 c_2 c_2) c_0) (f1 c_2 (f1 c_2 c_0)))
(= (f1 (f1 c_2 c_2) c_1) (f1 c_2 (f1 c_2 c_1)))
(= (f1 c_0 (f1 c_2 (f1 c_2 (f1 c_2 c_0)))) (f1 c_2 (f1 c_0 (f1 c_2 (f1 c_0 c_2)))))
(= (f1 c2 c8) (f1 c4 c9))
(not (= (f1 c6 c8) (f1 c7 c9)))
(or (= (f1 c_0 c_0) c_0)(= (f1 c_0 c_0) c_1)(= (f1 c_0 c_0) c_2))
(or (= (f1 c_0 c_1) c_0)(= (f1 c_0 c_1) c_1)(= (f1 c_0 c_1) c_2))
(or (= (f1 c_1 c_0) c_0)(= (f1 c_1 c_0) c_1)(= (f1 c_1 c_0) c_2))
(or (= (f1 c_1 c_1) c_0)(= (f1 c_1 c_1) c_1)(= (f1 c_1 c_1) c_2))
(or (= (f1 c_1 c_2) c_0)(= (f1 c_1 c_2) c_1)(= (f1 c_1 c_2) c_2))
(or (= (f1 c_2 c_0) c_0)(= (f1 c_2 c_0) c_1)(= (f1 c_2 c_0) c_2))
(or (= (f1 c_2 c_1) c_0)(= (f1 c_2 c_1) c_1)(= (f1 c_2 c_1) c_2))
(or (= (f1 c_2 c_2) c_0)(= (f1 c_2 c_2) c_1)(= (f1 c_2 c_2) c_2))
(or (= c6 c_0)(= c6 c_1)(= c6 c_2))
(or (= c3 c_0)(= c3 c_1)(= c3 c_2))
(or (= c7 c_0)(= c7 c_1)(= c7 c_2))
(or (= c5 c_0)(= c5 c_1)(= c5 c_2))
(or (= c2 c_0)(= c2 c_1)(= c2 c_2))
(or (= c4 c_0)(= c4 c_1)(= c4 c_2))
(or (= c8 c_0)(= c8 c_1)(= c8 c_2))
(or (= c9 c_0)(= c9 c_1)(= c9 c_2))
))
|
